added read_criterion/pretty_criterion;
improved rule filters -- intro excludes elim rules;
tuned output;
tuned;

--- a/src/Pure/Isar/find_theorems.ML	Sun May 22 19:26:15 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Sun May 22 19:26:16 2005 +0200
@@ -13,10 +13,10 @@
   val find_intros: Proof.context -> term -> (thmref * thm) list
   val find_intros_goal: Proof.context -> thm -> int -> (thmref * thm) list
   val find_elims: Proof.context -> term -> (thmref * thm) list
-  datatype search_criterion =
-    Name of string | Intro | Elim | Dest | Rewrite of string | Pattern of string
+  datatype 'term criterion =
+    Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term
   val print_theorems: Proof.context -> term option -> int option ->
-    (bool * search_criterion) list -> unit
+    (bool * string criterion) list -> unit
 end;
 
 structure FindTheorems: FIND_THEOREMS =
@@ -101,17 +101,31 @@
 
 (** search criteria **)
 
-datatype search_criterion =
-  Name of string | Intro | Elim | Dest | Rewrite of string | Pattern of string;
+datatype 'term criterion =
+  Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term;
+
+fun read_criterion _ (Name name) = Name name
+  | read_criterion _ Intro = Intro
+  | read_criterion _ Elim = Elim
+  | read_criterion _ Dest = Dest
+  | read_criterion ctxt (Rewrite str) = Rewrite (ProofContext.read_term ctxt str)
+  | read_criterion ctxt (Pattern str) =
+      Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
 
-fun string_of_crit (Name name) = "name: " ^ quote name
-  | string_of_crit Intro = "intro"
-  | string_of_crit Elim = "elim"
-  | string_of_crit Dest = "dest"
-  | string_of_crit (Rewrite s) = "rewrite: " ^ quote s
-  | string_of_crit (Pattern s) = quote s;
-
-fun string_of_criterion (b, c) = (if b then "" else "-") ^ string_of_crit c;
+fun pretty_criterion ctxt (b, c) =
+  let
+    fun prfx s = if b then s else "-" ^ s;
+  in
+    (case c of
+      Name name => Pretty.str (prfx "name: " ^ quote name)
+    | Intro => Pretty.str (prfx "intro")
+    | Elim => Pretty.str (prfx "elim")
+    | Dest => Pretty.str (prfx "dest")
+    | Rewrite t => Pretty.block [Pretty.str (prfx "rewrite:"), Pretty.brk 1,
+        Pretty.quote (ProofContext.pretty_term ctxt t)]
+    | Pattern pat => Pretty.enclose (prfx " \"") "\""
+        [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
+  end;
 
 
 
@@ -130,113 +144,118 @@
 fun filter_name str_pat ((name, _), _) = is_substring str_pat name;
 
 
-(* filter_intro *)
+(* filter intro/elim/dest rules *)
 
-(*checking conclusion of theorem against conclusion of goal*)
-fun filter_intro ctxt goal =
+local
+
+(*elimination rule: conclusion is a Var which does not appear in the major premise*)
+fun is_elim ctxt thm =
   let
-    val extract_intro = (single, Logic.strip_imp_concl);
-    val concl = Logic.concl_of_goal goal 1;
-  in is_matching_thm extract_intro ctxt concl end;
-
+    val sg = ProofContext.sign_of ctxt;
+    val prop = Thm.prop_of thm;
+    val concl = ObjectLogic.drop_judgment sg (Logic.strip_imp_concl prop);
+    val major_prem = Library.take (1, Logic.strip_imp_prems prop);
+    val prem_vars = Drule.vars_of_terms major_prem;
+  in
+    not (null major_prem) andalso
+    Term.is_Var concl andalso
+    not (Term.dest_Var concl mem prem_vars)
+  end;
 
-(* filter_elim_dest *)
-
-(*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
-  check_thm (cf. is_elim_rule below)*)
 fun filter_elim_dest check_thm ctxt goal =
   let
     val extract_elim =
      (fn thm => if Thm.no_prems thm then [] else [thm],
       hd o Logic.strip_imp_prems);
-
     val prems = Logic.prems_of_goal goal 1;
   in
-    fn fact => List.exists (fn prem =>
-      is_matching_thm extract_elim ctxt prem fact andalso check_thm (#2 fact)) prems
+    fn fact => prems |> List.exists (fn prem =>
+      is_matching_thm extract_elim ctxt prem fact
+      andalso (check_thm ctxt) (#2 fact))
   end;
 
-(*elimination rule: conclusion is a Var which does not appears in the
-  major premise*)
-fun is_elim_rule thm =
+in
+
+fun filter_intro ctxt goal =
   let
-    val prop = Thm.prop_of thm;
-    val concl = ObjectLogic.drop_judgment (Thm.sign_of_thm thm) (Logic.strip_imp_concl prop);
-    val major_prem = hd (Logic.strip_imp_prems prop);
-    val prem_vars = Drule.vars_of_terms [major_prem];
+    val extract_intro = (single, Logic.strip_imp_concl);
+    val concl = Logic.concl_of_goal goal 1;
   in
-    Term.is_Var concl andalso not (Term.dest_Var concl mem prem_vars)
+    fn fact => is_matching_thm extract_intro ctxt concl fact
+      andalso not (is_elim ctxt (#2 fact))
   end;
 
+fun filter_elim ctxt = filter_elim_dest is_elim ctxt;
+fun filter_dest ctxt = filter_elim_dest (not oo is_elim) ctxt;
+
+end;
+
 
 (* filter_rewrite *)
 
-fun filter_rewrite ctxt str =
+fun filter_rewrite ctxt t =
   let
     val (_, {mk_rews = {mk, ...}, ...}) =
       MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
     val extract_rewrite = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
-  in is_matching_thm extract_rewrite ctxt (ProofContext.read_term ctxt str) end;
+  in is_matching_thm extract_rewrite ctxt t end;
 
 
 (* filter_pattern *)
 
-(*subterm pattern supplied as raw string*)
-fun filter_pattern ctxt str =
-  let
-    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
-    val [pat] = ProofContext.read_term_pats TypeInfer.logicT ctxt [str];
+fun filter_pattern ctxt pat =
+  let val tsig = Sign.tsig_of (ProofContext.sign_of ctxt)
   in fn (_, thm) => Pattern.matches_subterm tsig (pat, Thm.prop_of thm) end;
 
 
 (* interpret criteria as filters *)
 
+local
+
+fun err_no_goal c =
+  error ("Current goal required for " ^ c ^ " search criterion");
+
 fun filter_crit _ _ (Name name) = filter_name name
+  | filter_crit _ NONE Intro = err_no_goal "intro"
+  | filter_crit _ NONE Elim = err_no_goal "elim"
+  | filter_crit _ NONE Dest = err_no_goal "dest"
+  | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal
+  | filter_crit ctxt (SOME goal) Elim = filter_elim ctxt goal
+  | filter_crit ctxt (SOME goal) Dest = filter_dest ctxt goal
   | filter_crit ctxt _ (Rewrite str) = filter_rewrite ctxt str
-  | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str
-  (*beyond this point, only criteria requiring a goal!*)
-  | filter_crit _ NONE c =
-      error ("Need to have a current goal to use " ^ string_of_crit c)
-  | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal
-  | filter_crit ctxt (SOME goal) Elim = filter_elim_dest is_elim_rule ctxt goal
-  | filter_crit ctxt (SOME goal) Dest =
-      filter_elim_dest (not o is_elim_rule) ctxt goal;
-      (*in this case all that is not elim is dest*)
+  | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str;
+
+in
 
 fun filter_criterion ctxt opt_goal (b, c) =
   (if b then I else not) o filter_crit ctxt opt_goal c;
 
 fun all_filters filters = List.filter (fn x => List.all (fn f => f x) filters);
 
+end;
+
 
 (* print_theorems *)
 
-fun print_theorems ctxt opt_goal opt_limit criteria =
+fun print_theorems ctxt opt_goal opt_limit raw_criteria =
   let
-    fun prt_fact (thmref, thm) =
-      ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
-    val prt_crit = Pretty.str o string_of_criterion;
+    val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
+    val filters = map (filter_criterion ctxt opt_goal) criteria;
 
-    val all_facts = find_thms ctxt ([], []);
-    val filters = map (filter_criterion ctxt opt_goal) criteria;
-    val matches = all_filters filters all_facts;
-
+    val matches = all_filters filters (find_thms ctxt ([], []));
     val len = length matches;
     val limit = if_none opt_limit (! thms_containing_limit);
-    val count = Int.min (limit, len);
 
-    val pruned = len <= limit;
-    val found = "found " ^ string_of_int len ^ " theorems" ^
-      (if pruned then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":";
+    fun prt_fact (thmref, thm) =
+      ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
   in
-    Pretty.big_list "searched for:" (map prt_crit criteria) ::
+    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
      (if null matches then [Pretty.str "nothing found"]
       else
-       [Pretty.str "", Pretty.str found] @
-       (if pruned then [] else [Pretty.str "..."]) @
-       map prt_fact (Library.drop (len - limit, matches)))
+        [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
+          (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"),
+         Pretty.str ""] @
+        map prt_fact (Library.drop (len - limit, matches)))
     |> Pretty.chunks |> Pretty.writeln
   end;