# HG changeset patch
# User kleing
# Date 1171926873 -3600
# Node ID 275802767bf3e20b3674c6701d5a8d0b12aae1c0
# Parent  0dc6b45e5662d584770bb467b8849cffa49a5d23
Remove duplicates from printed theorems in find_theorems
(still pretty slow, needs optimising).
Added syntax "find_theorems (..) with_dups .." to switch off removal.

diff -r 0dc6b45e5662 -r 275802767bf3 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Mon Feb 19 16:44:08 2007 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Tue Feb 20 00:14:33 2007 +0100
@@ -11,7 +11,7 @@
 sig
   datatype 'term criterion =
     Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
-  val print_theorems: Proof.context -> term option -> int option ->
+  val print_theorems: Proof.context -> term option -> int option -> bool ->
     (bool * string criterion) list -> unit
 end;
 
@@ -227,12 +227,43 @@
   in
     map (`(eval_filters filters)) thms
     |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
-    |> sort thm_ord |> map #2
+    |> sort thm_ord |> map #2 
   end;
 
 end;
 
 
+(* removing duplicates, preferring nicer names *)
+
+fun rem_thm_dups xs =
+    let 
+      fun nicer (Fact x) (Fact y) = size x <= size y
+        | nicer (Fact _) _        = true
+        | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
+        | nicer (PureThy.Name _) (Fact _) = false
+        | nicer (PureThy.Name _) _ = true
+        | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
+        | nicer (NameSelection _) _ = false;
+
+      fun is_in [] _ = NONE
+        | is_in ((n,t) :: xs) t' = if eq_thm (t, t') 
+                                   then SOME (n,t) 
+                                   else is_in xs t';
+
+      fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
+
+      fun rem_d (rev_seen, []) = rev rev_seen
+        | rem_d (rev_seen, (x as (n',t')) :: xs) = 
+          case is_in rev_seen t' of 
+            NONE => rem_d (x::rev_seen, xs)
+          | SOME (n,t) => if nicer n n' 
+                          then rem_d (rev_seen, xs) 
+                          else rem_d (x::remove eq (n,t) rev_seen,xs)
+
+    in rem_d ([], xs) end;
+
+
+
 (* print_theorems *)
 
 fun find_thms ctxt spec =
@@ -243,25 +274,28 @@
     |> distinct (fn ((r1, th1), (r2, th2)) =>
         r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
 
-fun print_theorems ctxt opt_goal opt_limit raw_criteria =
+fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val filters = map (filter_criterion ctxt opt_goal) criteria;
 
-    val matches = all_filters filters (find_thms ctxt ([], []));
+    val raw_matches = all_filters filters (find_thms ctxt ([], []));
+    val matches = if rem_dups then rem_thm_dups raw_matches else raw_matches;
+
     val len = length matches;
     val limit = the_default (! thms_containing_limit) opt_limit;
+    val thms = Library.drop (len - limit, matches);
 
     fun prt_fact (thmref, thm) =
       ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
-     (if null matches then [Pretty.str "nothing found"]
+     (if null thms then [Pretty.str "nothing found"]
       else
         [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)))
+        map prt_fact thms)
     |> Pretty.chunks |> Pretty.writeln
   end;
 
diff -r 0dc6b45e5662 -r 275802767bf3 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Feb 19 16:44:08 2007 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Feb 20 00:14:33 2007 +0100
@@ -94,7 +94,7 @@
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
-  val find_theorems: int option * (bool * string FindTheorems.criterion) list
+  val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
@@ -509,12 +509,13 @@
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
 
-fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+fun find_theorems ((opt_lim, rem_dups), spec) = 
+  Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val proof_state = Toplevel.enter_proof_body state;
     val ctxt = Proof.context_of proof_state;
     val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
-  in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
+  in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 
 (* print proof context contents *)
diff -r 0dc6b45e5662 -r 275802767bf3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 19 16:44:08 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 20 00:14:33 2007 +0100
@@ -810,6 +810,7 @@
   OuterSyntax.improper_command "find_theorems"
     "print theorems meeting specified criteria" K.diag
     (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
+     Scan.optional (P.reserved "with_dups" >> K false) true -- 
      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo IsarCmd.find_theorems));