new thms_containing that searches for patterns instead of constants
(by Rafal Kolanski, NICTA)

--- a/src/Pure/Isar/proof_context.ML	Fri Apr 29 08:05:06 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 29 11:22:41 2005 +0200
@@ -1463,38 +1463,52 @@
       | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
   in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end;
 
+(* facts which are local to the current context, with their names 
+   examples are "prems" and "x" in "assumes x:" during a proof *)
+fun local_facts (ctxt as Context {thms = (_, _, _, index), ...}) = 
+    (* things like "prems" can occur twice under some circumstances *)
+    gen_distinct eq_fst (FactIndex.find ([],[]) index);
 
 fun print_thms_containing ctxt opt_limit ss =
   let
     val prt_term = pretty_term ctxt;
     val prt_fact = pretty_fact ctxt;
-    fun prt_consts [] = []
-      | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" ::
-          map (Pretty.quote o prt_term o Syntax.const) cs))];
-    fun prt_frees [] = []
-      | prt_frees xs = [Pretty.block (Pretty.breaks (Pretty.str "variables" ::
-          map (Pretty.quote o prt_term o Syntax.free) xs))];
+
+    (* theorems from the theory and its ancestors *)
+    val thy = theory_of ctxt;
+    val sg1 = Theory.sign_of thy;
+    val all_thys = thy :: (Theory.ancestors_of thy)
+    val thms1 = List.concat (map PureThy.thms_with_names_of all_thys);
+    val facts1 =
+      PureThy.find_theorems sg1 thms1 ss;
 
-    val (cs, xs) = Library.foldl (FactIndex.index_term (is_known ctxt))
-      (([], []), map (read_term_dummies ctxt) ss);
-    val empty_idx = null cs andalso null xs;
-
-    val header =
-      if empty_idx then [Pretty.block [Pretty.str "Known facts:", Pretty.fbrk]]
-      else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
-        separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
-          [Pretty.str ":", Pretty.fbrk])]
-    val facts =
-      PureThy.thms_containing (theory_of ctxt) (cs, xs) @ lthms_containing ctxt (cs, xs)
-      |> sort_wrt #1;
+    (* theorems from the local context *)
+    val sg2 = sign_of ctxt;
+    val thms2 = local_facts ctxt;
+    val facts2 = 
+      PureThy.find_theorems sg2 thms2 ss;
+    
+    (* combine them, use a limit, then print *)
+    val facts = facts1 @ facts2; 
     val len = length facts;
     val limit = getOpt (opt_limit, ! thms_containing_limit);
+    val count = Int.min (limit, len);
+    
+    val header = Pretty.blk (0, [Pretty.str "Searched for:", Pretty.fbrk,
+            Pretty.indent 4 (
+                Pretty.blk (0, separate Pretty.fbrk (map Pretty.str ss))),
+            Pretty.fbrk, Pretty.fbrk,
+            Pretty.str ("Found " ^ (Int.toString len) ^ 
+                " theorems (" ^ (Int.toString count) ^ " displayed):"), 
+            Pretty.fbrk]);
   in
-    if empty_idx andalso not (null ss) then
-      warning "thms_containing: no consts/frees in specification"
-    else (header @ (if len <= limit then [] else [Pretty.str "..."]) @
-        map prt_fact (Library.drop (len - limit, facts))) |> Pretty.chunks |> Pretty.writeln
+    if null facts then
+      warning "find_theorems: nothing found"
+    else 
+        Pretty.writeln header;
+        ((if len <= limit then [] else [Pretty.str "..."]) @
+        map (prt_fact) (Library.drop (len - limit, facts))) |> 
+            Pretty.chunks |> Pretty.writeln
   end;
 
-
 end;

--- a/src/Pure/pure_thy.ML	Fri Apr 29 08:05:06 2005 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 29 11:22:41 2005 +0200
@@ -14,6 +14,7 @@
   val get_thms: theory -> thmref -> thm list
   val get_thmss: theory -> thmref list -> thm list
   val thms_of: theory -> (string * thm) list
+  val thms_with_names_of: theory -> (string * thm list) list
   structure ProtoPure:
     sig
       val thy: theory
@@ -31,6 +32,7 @@
   val select_thm: thmref -> thm list -> thm list
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
   val thms_containing: theory -> string list * string list -> (string * thm list) list
+  val find_theorems: Sign.sg -> (string * thm list) list -> string list -> (string * thm list) list 
   val thms_containing_consts: theory -> string list -> (string * thm) list
   val find_matching_thms: (thm -> thm list) * (term -> term)
         -> theory -> term -> (string * thm) list
@@ -226,6 +228,10 @@
     map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms_tab)))
   end;
 
+(* thms_with_names_of - theorems in this theory and their names *)
+fun thms_with_names_of thy = 
+  TheoremsData.get thy |> ! |> #index |> FactIndex.find ([],[]);
+  (* looking for nothing in a FactIndex finds everything, i.e. all theorems *)
 
 (* thms_containing *)
 
@@ -245,6 +251,49 @@
   thms_containing thy (consts, []) |> map #2 |> List.concat
   |> map (fn th => (Thm.name_of_thm th, th))
 
+(* find_theorems - finding theorems by matching on a series of subterms  *)
+
+(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into
+    a term with all free variables made schematic *)
+fun str_pattern_to_term sg str_pattern =
+  let
+    (* pattern as term with dummies as Consts *)
+    val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
+                       |> Thm.term_of; 
+    (* with dummies as Vars *)
+    val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern));
+  in
+    (* with schematic vars *)
+    #1 (Type.varify (v_pattern, []))
+  end;
+
+(* find all thms such that for each returned thm, all given 
+    propositions are subterms of it *)
+fun thms_matching_patterns tsign (pat::pats) thms = 
+    let 
+        fun match_single pattern thm = 
+            Pattern.matches_subterm tsign (pat, Thm.prop_of thm);
+    in
+        thms_matching_patterns tsign pats
+            (List.filter (match_single pat) thms)
+    end
+  | thms_matching_patterns _ _ thms = thms; 
+
+(* facts are pairs of theorem name and a list of its thms *)
+fun find_theorems sg facts str_patterns =
+  let
+    val typesg = Sign.tsig_of sg;
+    
+    (* the patterns we will be looking for *)
+    val patterns = map (str_pattern_to_term sg) str_patterns;
+
+    (* we are interested in theorems which have one or more thms for which
+       all patterns are subterms *)
+    fun matches (_, thms) = 
+        (not o null o (thms_matching_patterns typesg patterns)) thms
+  in
+    List.filter matches facts
+  end;
 
 (* intro/elim theorems *)