searching for thms by combination of criteria (intro, elim, dest, name, term pattern)

--- a/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:34:20 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:35:05 2005 +0200
@@ -56,7 +56,7 @@
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
-  val print_thms_containing: int option * string list
+  val print_thms_containing: int option * (bool * ProofContext.search_criterion) list
     -> Toplevel.transition -> Toplevel.transition
   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
@@ -244,9 +244,22 @@
 
 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
 
-fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  ProofContext.print_thms_containing
-    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
+fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o 
+Toplevel.keep (fn state =>
+  let
+    fun get_goal () = 
+      let val (_, (_, st)) = Proof.get_goal (Toplevel.proof_of state);
+      in prop_of st end;
+    
+    (* searching is permitted without a goal.
+       I am not sure whether the only exception that I should catch is UNDEF *)
+    val goal = SOME (get_goal ()) handle Toplevel.UNDEF => NONE;
+    
+    val ctxt = (Toplevel.node_case ProofContext.init Proof.context_of state);
+  in
+    ProofContext.print_thms_containing ctxt goal lim spec
+  end);
+
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));

--- a/src/Pure/Isar/isar_syn.ML	Mon May 16 09:34:20 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 16 09:35:05 2005 +0200
@@ -631,10 +631,30 @@
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
 
 val thms_containingP =
-  OuterSyntax.improper_command "thms_containing"
-    "print facts containing certain constants or variables"
-    K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
-      Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+  let
+    (* intro, elim, dest and rewrite are reserved, otherwise it's a pattern *)
+    fun decode "intro" = ProofContext.Intro
+      | decode "elim" = ProofContext.Elim
+      | decode "dest" = ProofContext.Dest
+      | decode "rewrite" = ProofContext.Rewrite
+      | decode x = ProofContext.Pattern x;
+  
+    (* either name:term or term *)
+    val criterion = ((P.term :-- (fn "name" => P.$$$ ":" |-- P.term | 
+                                     _ => Scan.fail)
+                                 ) >> (ProofContext.Name o #2)) ||
+                    (P.term >> decode);
+  in
+    OuterSyntax.improper_command "thms_containing"
+      "print facts meeting specified criteria"
+      K.diag 
+      (* obtain (int option * (bool * string) list) representing
+         a limit and a set of constraints (the bool indicates whether
+         the constraint is inclusive or exclusive) *)
+      (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
+       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+        >> (Toplevel.no_timing oo IsarCmd.print_thms_containing))
+  end;
 
 val thm_depsP =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"

--- a/src/Pure/Isar/proof_context.ML	Mon May 16 09:34:20 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 16 09:35:05 2005 +0200
@@ -155,7 +155,9 @@
   val prems_limit: int ref
   val pretty_asms: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
-  val print_thms_containing: context -> int option -> string list -> unit
+  datatype search_criterion = Intro | Elim  | Dest | Rewrite |
+                              Pattern of string | Name of string;
+  val print_thms_containing: context -> term option -> int option -> (bool * search_criterion) list -> unit
 end;
 
 signature PRIVATE_PROOF_CONTEXT =
@@ -171,6 +173,8 @@
 structure ProofContext: PRIVATE_PROOF_CONTEXT =
 struct
 
+datatype search_criterion = Intro | Elim | Dest | Rewrite |
+                          Pattern of string | Name of string;
 
 (** datatype context **)
 
@@ -1470,28 +1474,159 @@
     (* things like "prems" can occur twice under some circumstances *)
     gen_distinct eq_fst (FactIndex.find ([],[]) index);
 
-fun print_thms_containing ctxt opt_limit ss =
+fun isSubstring pat str = 
+  if String.size pat = 0 then true
+  else if String.size pat > String.size str then false
+  else if String.substring (str, 0, String.size pat) = pat then true
+  else isSubstring pat (String.extract (str, 1, NONE));
+
+(* 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;
+
+(* alternate rem_top which checks for a Trueprop, unlike that in PureThy *)
+fun rem_top_c (Term.Const ("Trueprop", _)  $ t) = t
+  | rem_top_c _ = Bound 0;
+
+(* ---------- search filter contructions go here *)
+
+(* terms supplied in string form as patterns *)
+fun str_term_pat_to_filter sg str_pat = 
+  let
+    val tsig = Sign.tsig_of sg;
+    val pat = str_pattern_to_term sg str_pat;
+    
+    (* must qualify type so ML doesn't go and replace it with a concrete one *)
+    fun name_thm_matches_pattern tsig pat (_:string, thm) =
+      Pattern.matches_subterm tsig (pat, Thm.prop_of thm);
+  in
+    name_thm_matches_pattern (Sign.tsig_of sg) pat
+  end;
+ 
+(* create filter that just looks for a string in the name,
+   substring match only (no regexps are performed) *)
+fun str_name_pat_to_filter str_pat (name, _:Thm.thm) = isSubstring str_pat name;
+
+(* for elimination and destruction rules, we must check if the major premise
+   matches with one of the assumptions in the top subgoal, but we must 
+   additionally make sure that we tell elim/dest apart, using thm_check_fun *)
+fun elim_dest_filter thm_check_fun sg goal =
+  let
+    val elims_extract = (fn thm => if Thm.no_prems thm then [] else [thm],
+                       rem_top_c o hd o Logic.strip_imp_prems);
+
+    (* assumptions of the top subgoal *)
+    val prems = map rem_top_c (Logic.prems_of_goal goal 1);  
+    
+    fun prem_matches_name_thm prems (name_thm as (name,thm)) =
+        List.exists
+        (fn p => PureThy.is_matching_thm elims_extract sg p name_thm
+                andalso (thm_check_fun thm)) prems;
+  in
+    prem_matches_name_thm prems      
+  end;
+
+(* ------------</filter constructions> *)
+
+(* collect all the Var statements in a term *)
+fun vars_of_term (Const _) = []
+  | vars_of_term (Free _) = []
+  | vars_of_term (Bound _) = []
+  | vars_of_term (Abs (_,_,t)) = vars_of_term t
+  | vars_of_term (v as (Var _)) = [v]
+  | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y);
+
+(* elimination rule: conclusion is a Var and 
+   no Var in the conclusion appears in the major premise
+   Note: only makes sense if the major premise already matched the assumption 
+         of some goal! *)
+fun is_elim_rule thm =
+  let
+    val {prop, ...} = rep_thm thm;
+    val concl = rem_top_c (Logic.strip_imp_concl prop);
+    val major_prem = hd (Logic.strip_imp_prems prop);
+    val prem_vars = distinct (vars_of_term major_prem);
+    val concl_vars = distinct (vars_of_term concl);
+  in
+    Term.is_Var concl andalso ((prem_vars inter concl_vars) = [])
+  end;
+
+fun crit2str (Name name) = "name:" ^ name
+  | crit2str Elim = "elim"
+  | crit2str Intro = "intro"
+  | crit2str Rewrite = "rewrite"
+  | crit2str Dest = "dest"
+  | crit2str (Pattern x) = x;
+
+val criteria_to_str =
+  let
+    fun criterion_to_str ( true, ct) = "+ :   " ^ crit2str ct
+      | criterion_to_str (false, ct) = "- :   " ^ crit2str ct
+  in 
+    map criterion_to_str 
+  end;
+
+fun make_filter _ _ (Name name) = str_name_pat_to_filter name
+  | make_filter sg _ (Pattern p) = str_term_pat_to_filter sg p
+  (* beyond this point, only criteria requiring a goal! *)
+  | make_filter _ NONE c =
+      error ("Need to have a current goal to use " ^ (crit2str c))
+  | make_filter sg (SOME goal) Elim =
+      elim_dest_filter is_elim_rule sg goal
+  | make_filter sg (SOME goal) Dest =
+      (* in this case all that is not elim rule is dest *)
+      elim_dest_filter (not o is_elim_rule) sg goal
+  | make_filter sg (SOME goal) Intro =
+    let
+      (* filter by checking conclusion of theorem against conclusion of goal *)
+      fun intros_extract () = (single, rem_top_c o Logic.strip_imp_concl);
+      val concl = rem_top_c (Logic.concl_of_goal goal 1);
+    in
+      (fn name_thm => 
+            PureThy.is_matching_thm (intros_extract ()) sg concl name_thm)
+    end
+  | make_filter _ _ c =
+      error (crit2str c ^ " unimplemented");
+  (* XXX: searching for rewrites currently impossible since we'd need
+          a simplifier, which is included *after* Pure *)
+
+(* create filters ... convert negative ones to positive ones *)
+fun make_filters sg opt_goal =
+    map (fn (b,sc) => (if b then I else not) o (make_filter sg opt_goal sc));
+
+fun print_thms_containing ctxt opt_goal opt_limit criteria =
   let
     val prt_term = pretty_term ctxt;
     val prt_fact = pretty_fact ctxt;
+    val ss = criteria_to_str criteria;
 
-    (* theorems from the theory and its ancestors *)
+    (* facts 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 facts1 = List.concat (map PureThy.thms_with_names_of all_thys);
+    val filters1 = make_filters sg1 opt_goal criteria;
+    val matches1 = PureThy.find_theorems facts1 filters1;
 
-    (* theorems from the local context *)
+    (* facts from the local context *)
     val sg2 = sign_of ctxt;
-    val thms2 = local_facts ctxt;
-    val facts2 = 
-      PureThy.find_theorems sg2 thms2 ss;
+    val facts2 = local_facts ctxt;
+    val filters2 = make_filters sg2 opt_goal criteria;
+    val matches2 = PureThy.find_theorems facts2 filters2;
     
     (* combine them, use a limit, then print *)
-    val facts = facts1 @ facts2; 
-    val len = length facts;
+    val matches = matches1 @ matches2;
+    val len = length matches;
     val limit = getOpt (opt_limit, ! thms_containing_limit);
     val count = Int.min (limit, len);
     
@@ -1503,13 +1638,14 @@
                 " theorems (" ^ (Int.toString count) ^ " displayed):"), 
             Pretty.fbrk]);
   in
-    if null facts then
+    if null matches 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
+      Pretty.writeln header;
+      ((if len <= limit then [] else [Pretty.str "..."]) @
+      map (prt_fact) (Library.drop (len - limit, matches))) |> 
+        Pretty.chunks |> Pretty.writeln
   end;
 
 end;
+

--- a/src/Pure/proof_general.ML	Mon May 16 09:34:20 2005 +0200
+++ b/src/Pure/proof_general.ML	Mon May 16 09:35:05 2005 +0200
@@ -372,8 +372,11 @@
 
 (* misc commands for ProofGeneral/isa *)
 
+(* PG/isa mode does not go through the Isar parser, hence we 
+   interpret everything as term pattern only *)
 fun thms_containing ss =
-  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE ss;
+  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE 
+    (map (fn s => (true, ProofContext.Pattern s)) ss);
 
 val welcome = priority o Session.welcome;
 val help = welcome;

--- a/src/Pure/pure_thy.ML	Mon May 16 09:34:20 2005 +0200
+++ b/src/Pure/pure_thy.ML	Mon May 16 09:35:05 2005 +0200
@@ -33,10 +33,12 @@
   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 find_theorems: ('a * 'b list) list -> ('a * 'b -> bool) list -> ('a * 'b 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
+  val is_matching_thm: (thm -> thm list) * (term -> term)
+        -> Sign.sg -> term -> (string * thm) -> bool
   val find_intros: theory -> term -> (string * thm) list
   val find_intros_goal : theory -> thm -> int -> (string * thm) list
   val find_elims : theory -> term -> (string * thm) list
@@ -252,46 +254,29 @@
   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;
+(* Searching based on filters *)
+(* a filter must only take a (name:string, theorem:Thm.thm) and return true
+   if it finds a match, false if it doesn't *)
 
-(* 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; 
+(* given facts and filters, find all facts in which at least one theorem 
+   matches on ALL filters *)
+fun find_theorems facts filters =
+  let
+    (* break fact up into theorems, but associate them with the name of this 
+       fact, so that filters looking by name will only consider the fact's
+       name *)
+    fun fact_to_names_thms (name, thms) =
+      map (fn thm => (name, thm)) 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;
+    (* all filters return true when applied to a named theorem *)
+    fun match_all_filters filters name_thm =
+      List.all (fn filter => filter name_thm) filters;
 
-    (* 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
+    (* at least one theorem in this fact which matches all filters *)
+    fun fact_matches_filters filters fact =
+      List.exists (match_all_filters filters) (fact_to_names_thms fact);
+
+    fun matches x = (fact_matches_filters filters x)
   in
     List.filter matches facts
   end;
@@ -347,6 +332,13 @@
 
   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
 
+(* like find_matching_thms, but for one named theorem only *)
+fun is_matching_thm extract sg prop name_thm =
+  (case top_const prop of NONE => false
+   | SOME c => 
+      not ([] = select_match(c,prop, sg,[name_thm],extract)));
+
+
 fun find_matching_thms extract thy prop =
   (case top_const prop of NONE => []
    | SOME c => let val thms = thms_containing_consts thy [c]