src/Pure/Tools/find_theorems.ML

 
 signature FIND_THEOREMS =
 sig
   datatype 'term criterion =
     Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
-
-  datatype theorem =
-    Internal of Facts.ref * thm | External of Facts.ref * term
-
   type 'term query = {
     goal: thm option,
     limit: int option,
     rem_dups: bool,
     criteria: (bool * 'term criterion) list
   }
-
-  val read_criterion: Proof.context -> string criterion -> term criterion
   val read_query: Position.T -> string -> (bool * string criterion) list
-
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * term criterion) list -> int option * (Facts.ref * thm) list
   val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> int option * (Facts.ref * thm) list
-
-  val filter_theorems: Proof.context -> theorem list -> term query ->
-    int option * theorem list
-  val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
-    int option * theorem list
-
-  val pretty_theorem: Proof.context -> theorem -> Pretty.T
   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
 end;
 
 structure Find_Theorems: FIND_THEOREMS =
 struct

     fun subst_size pat =
       let val (_, subst) =
         Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
 
-    fun bestmatch [] = NONE
-      | bestmatch xs = SOME (foldl1 Int.min xs);
+    fun best_match [] = NONE
+      | best_match xs = SOME (foldl1 Int.min xs);
 
     val match_thm = matches o refine_term;
   in
     map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
-    |> bestmatch
+    |> best_match
   end;
 
 
 (* filter_name *)
 

       val rule = prop_of theorem;
       val prems = Logic.prems_of_goal goal 1;
       val goal_concl = Logic.concl_of_goal goal 1;
       val rule_mp = hd (Logic.strip_imp_prems rule);
       val rule_concl = Logic.strip_imp_concl rule;
-      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
+      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?? *)
       val rule_tree = combine rule_mp rule_concl;
       fun goal_tree prem = combine prem goal_concl;
       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
       val successful = prems |> map_filter try_subst;
     in

       Proof_Context.theory_of ctxt
       |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
     val ctxt' = Proof_Context.transfer thy' ctxt;
     val goal' = Thm.transfer thy' goal;
 
-    fun etacn thm i =
+    fun limited_etac thm i =
       Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal'
-      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
+      else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
   in
     fn Internal (_, thm) =>
         if is_some (Seq.pull (try_thm thm))
         then SOME (Thm.nprems_of thm, 0) else NONE
      | External _ => NONE

   |> map #1;
 
 end;
 
 
-(* pretty_theorems *)
+
+(** main operations **)
+
+(* filter_theorems *)
 
 fun all_facts_of ctxt =
   let
     fun visible_facts facts =
       Facts.dest_static [] facts

       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
 
   in find theorems end;
 
 fun filter_theorems_cmd ctxt theorems raw_query =
-  filter_theorems ctxt theorems (map_criteria
-    (map (apsnd (read_criterion ctxt))) raw_query);
+  filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
+
+
+(* find_theorems *)
+
+local
 
 fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val assms =
       Proof_Context.get_fact ctxt (Facts.named "local.assms")

     filter ctxt (map Internal (all_facts_of ctxt))
       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
     |> apsnd (map (fn Internal f => f))
   end;
 
+in
+
 val find_theorems = gen_find_theorems filter_theorems;
 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
+
+end;
+
+
+(* pretty_theorems *)
+
+local
 
 fun pretty_ref ctxt thmref =
   let
     val (name, sel) =
       (case thmref of

 fun pretty_theorem ctxt (Internal (thmref, thm)) =
       Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
   | pretty_theorem ctxt (External (thmref, prop)) =
       Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
 
+in
+
 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
 
-fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
-  let
+fun pretty_theorems state opt_limit rem_dups raw_criteria =
+  let
+    val ctxt = Proof.context_of state;
+    val opt_goal = try Proof.simple_goal state |> Option.map #goal;
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
+
     val (opt_found, theorems) =
       filter_theorems ctxt (map Internal (all_facts_of ctxt))
         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
     val returned = length theorems;
 

      else
       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
         grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems)
   end |> Pretty.fbreaks |> curry Pretty.blk 0;
 
-fun pretty_theorems_cmd state opt_lim rem_dups spec =
-  let
-    val ctxt = Toplevel.context_of state;
-    val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-  in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
+end;
 
 
 
 (** Isar command syntax **)
+
+fun proof_state st =
+  (case try Toplevel.proof_of st of
+    SOME state => state
+  | NONE => Proof.init (Toplevel.context_of st));
 
 local
 
 val criterion =
   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||

 
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_theorems"}
     "find theorems meeting specified criteria"
     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
-      Toplevel.keep (fn state =>
-        Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
+      Toplevel.keep (fn st =>
+        Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
 
 end;
 
 
 
 (** PIDE query operation **)
 
 val _ =
   Query_Operation.register "find_theorems" (fn st => fn args =>
-    if can Toplevel.theory_of st then
-      Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
-    else error "Unknown theory context");
-
-end;
+    if can Toplevel.context_of st then
+      Pretty.string_of
+        (pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args))
+    else error "Unknown context");
+
+end;