<commit_before>(*  Title:      Tools/solve_direct.ML
    Author:     <NAME> and <NAME>, NICTA

Check whether a newly stated theorem can be solved directly by an
existing theorem.  Duplicate lemmas can be detected in this way.

The implementation relies critically on the Find_Theorems solves
feature.
*)

signature SOLVE_DIRECT =
sig
  val auto : bool Unsynchronized.ref
  val max_solutions : int Unsynchronized.ref
  val setup : theory -> theory
end;

structure Solve_Direct : SOLVE_DIRECT =
struct

val solve_directN = "solve_direct";


(* preferences *)

val auto = Unsynchronized.ref false;
val max_solutions = Unsynchronized.ref 5;

val _ =
  ProofGeneralPgip.add_preference Preferences.category_tracing
  (Unsynchronized.setmp auto true (fn () =>
    Preferences.bool_pref auto
      ("Auto " ^ solve_directN)
      ("Run " ^ quote solve_directN ^ " automatically.")) ());


(* solve_direct command *)

fun solve_direct auto state =
  let
    val ctxt = Proof.context_of state;

    val crits = [(true, Find_Theorems.Solves)];
    fun find g =
      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);

    fun prt_result (goal, results) =
      let
        val msg =
          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
          (case goal of
            NONE => "The current goal"
          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
      in
        Pretty.big_list
          (msg ^ " can be solved directly with")
          (map (Find_Theorems.pretty_thm ctxt) results)
      end;

    fun seek_against_goal () =
      (case try Proof.simple_goal state of
        NONE => NONE
      | SOME {goal = st, ...} =>
          let
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
            val rs =
              if length subgoals = 1
              then [(NONE, find st)]
              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
            val results = filter_out (null o snd) rs;
          in if null results then NONE else SOME results end);
    fun message results = separate (Pretty.brk 0) (map prt_result results);
  in
    (case try seek_against_goal () of
      SOME (SOME results) =>
        (true,
          state |>
           (if auto then
             Proof.goal_message
               (fn () =>
                 Pretty.chunks
                  [Pretty.str "",
                   Pretty.markup Markup.hilite (message results)])
            else
              tap (fn _ =>
                priority (Pretty.string_of (Pretty.chunks (message results))))))
    | _ => (false, state))
  end;

val invoke_solve_direct = fst o solve_direct false;

val _ =
  Outer_Syntax.improper_command solve_directN
    "try to solve conjectures directly with existing theorems" Keyword.diag
    (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct o Toplevel.proof_of)));


(* hook *)

fun auto_solve_direct state =
  if not (! auto) then (false, state) else solve_direct true state;

val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);

end;<commit_msg>export main ML entry by default; observe elisp format for preferences; clarified command setup;<commit_after>(*  Title:      Tools/solve_direct.ML
    Author:     <NAME> and <NAME>, NICTA

Check whether a newly stated theorem can be solved directly by an
existing theorem.  Duplicate lemmas can be detected in this way.

The implementation relies critically on the Find_Theorems solves
feature.
*)

signature SOLVE_DIRECT =
sig
  val auto: bool Unsynchronized.ref
  val max_solutions: int Unsynchronized.ref
  val solve_direct: bool -> Proof.state -> bool * Proof.state
  val setup: theory -> theory
end;

structure Solve_Direct: SOLVE_DIRECT =
struct

val solve_directN = "solve_direct";


(* preferences *)

val auto = Unsynchronized.ref false;
val max_solutions = Unsynchronized.ref 5;

val _ =
  ProofGeneralPgip.add_preference Preferences.category_tracing
  (Unsynchronized.setmp auto true (fn () =>
    Preferences.bool_pref auto
      "auto-solve-direct"
      ("Run " ^ quote solve_directN ^ " automatically.")) ());


(* solve_direct command *)

fun solve_direct auto state =
  let
    val ctxt = Proof.context_of state;

    val crits = [(true, Find_Theorems.Solves)];
    fun find g =
      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);

    fun prt_result (goal, results) =
      let
        val msg =
          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
          (case goal of
            NONE => "The current goal"
          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
      in
        Pretty.big_list
          (msg ^ " can be solved directly with")
          (map (Find_Theorems.pretty_thm ctxt) results)
      end;

    fun seek_against_goal () =
      (case try Proof.simple_goal state of
        NONE => NONE
      | SOME {goal = st, ...} =>
          let
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
            val rs =
              if length subgoals = 1
              then [(NONE, find st)]
              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
            val results = filter_out (null o snd) rs;
          in if null results then NONE else SOME results end);
    fun message results = separate (Pretty.brk 0) (map prt_result results);
  in
    (case try seek_against_goal () of
      SOME (SOME results) =>
        (true,
          state |>
           (if auto then
             Proof.goal_message
               (fn () =>
                 Pretty.chunks
                  [Pretty.str "",
                   Pretty.markup Markup.hilite (message results)])
            else
              tap (fn _ =>
                priority (Pretty.string_of (Pretty.chunks (message results))))))
    | _ => (false, state))
  end;

val _ =
  Outer_Syntax.improper_command solve_directN
    "try to solve conjectures directly with existing theorems" Keyword.diag
    (Scan.succeed
      (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));


(* hook *)

fun auto_solve_direct state =
  if not (! auto) then (false, state) else solve_direct true state;

val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);

end;
{'fraction_non_alphanumeric': 0.0941589530801149, 'fraction_numerical': 0.000957548675390999, 'mean_word_length': 2.4171210468920394, 'pattern_counts': {'":': 2, '<': 7, '<?xml version=': 0, '>': 34, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1174651', 'n_tokens_mistral': 2009, 'n_tokens_neox': 1881, 'n_words': 599}