1.1 --- a/src/Pure/Isar/find_theorems.ML Mon Feb 19 16:44:08 2007 +0100
1.2 +++ b/src/Pure/Isar/find_theorems.ML Tue Feb 20 00:14:33 2007 +0100
1.3 @@ -11,7 +11,7 @@
1.4 sig
1.5 datatype 'term criterion =
1.6 Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
1.7 - val print_theorems: Proof.context -> term option -> int option ->
1.8 + val print_theorems: Proof.context -> term option -> int option -> bool ->
1.9 (bool * string criterion) list -> unit
1.10 end;
1.11
1.12 @@ -227,12 +227,43 @@
1.13 in
1.14 map (`(eval_filters filters)) thms
1.15 |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
1.16 - |> sort thm_ord |> map #2
1.17 + |> sort thm_ord |> map #2
1.18 end;
1.19
1.20 end;
1.21
1.22
1.23 +(* removing duplicates, preferring nicer names *)
1.24 +
1.25 +fun rem_thm_dups xs =
1.26 + let
1.27 + fun nicer (Fact x) (Fact y) = size x <= size y
1.28 + | nicer (Fact _) _ = true
1.29 + | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
1.30 + | nicer (PureThy.Name _) (Fact _) = false
1.31 + | nicer (PureThy.Name _) _ = true
1.32 + | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
1.33 + | nicer (NameSelection _) _ = false;
1.34 +
1.35 + fun is_in [] _ = NONE
1.36 + | is_in ((n,t) :: xs) t' = if eq_thm (t, t')
1.37 + then SOME (n,t)
1.38 + else is_in xs t';
1.39 +
1.40 + fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
1.41 +
1.42 + fun rem_d (rev_seen, []) = rev rev_seen
1.43 + | rem_d (rev_seen, (x as (n',t')) :: xs) =
1.44 + case is_in rev_seen t' of
1.45 + NONE => rem_d (x::rev_seen, xs)
1.46 + | SOME (n,t) => if nicer n n'
1.47 + then rem_d (rev_seen, xs)
1.48 + else rem_d (x::remove eq (n,t) rev_seen,xs)
1.49 +
1.50 + in rem_d ([], xs) end;
1.51 +
1.52 +
1.53 +
1.54 (* print_theorems *)
1.55
1.56 fun find_thms ctxt spec =
1.57 @@ -243,25 +274,28 @@
1.58 |> distinct (fn ((r1, th1), (r2, th2)) =>
1.59 r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
1.60
1.61 -fun print_theorems ctxt opt_goal opt_limit raw_criteria =
1.62 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.63 let
1.64 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.65 val filters = map (filter_criterion ctxt opt_goal) criteria;
1.66
1.67 - val matches = all_filters filters (find_thms ctxt ([], []));
1.68 + val raw_matches = all_filters filters (find_thms ctxt ([], []));
1.69 + val matches = if rem_dups then rem_thm_dups raw_matches else raw_matches;
1.70 +
1.71 val len = length matches;
1.72 val limit = the_default (! thms_containing_limit) opt_limit;
1.73 + val thms = Library.drop (len - limit, matches);
1.74
1.75 fun prt_fact (thmref, thm) =
1.76 ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
1.77 in
1.78 Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
1.79 - (if null matches then [Pretty.str "nothing found"]
1.80 + (if null thms then [Pretty.str "nothing found"]
1.81 else
1.82 [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
1.83 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"),
1.84 Pretty.str ""] @
1.85 - map prt_fact (Library.drop (len - limit, matches)))
1.86 + map prt_fact thms)
1.87 |> Pretty.chunks |> Pretty.writeln
1.88 end;
1.89
2.1 --- a/src/Pure/Isar/isar_cmd.ML Mon Feb 19 16:44:08 2007 +0100
2.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Feb 20 00:14:33 2007 +0100
2.3 @@ -94,7 +94,7 @@
2.4 val print_antiquotations: Toplevel.transition -> Toplevel.transition
2.5 val class_deps: Toplevel.transition -> Toplevel.transition
2.6 val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
2.7 - val find_theorems: int option * (bool * string FindTheorems.criterion) list
2.8 + val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
2.9 -> Toplevel.transition -> Toplevel.transition
2.10 val print_binds: Toplevel.transition -> Toplevel.transition
2.11 val print_cases: Toplevel.transition -> Toplevel.transition
2.12 @@ -509,12 +509,13 @@
2.13 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
2.14 ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
2.15
2.16 -fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
2.17 +fun find_theorems ((opt_lim, rem_dups), spec) =
2.18 + Toplevel.unknown_theory o Toplevel.keep (fn state =>
2.19 let
2.20 val proof_state = Toplevel.enter_proof_body state;
2.21 val ctxt = Proof.context_of proof_state;
2.22 val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
2.23 - in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
2.24 + in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
2.25
2.26
2.27 (* print proof context contents *)
3.1 --- a/src/Pure/Isar/isar_syn.ML Mon Feb 19 16:44:08 2007 +0100
3.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Feb 20 00:14:33 2007 +0100
3.3 @@ -810,6 +810,7 @@
3.4 OuterSyntax.improper_command "find_theorems"
3.5 "print theorems meeting specified criteria" K.diag
3.6 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
3.7 + Scan.optional (P.reserved "with_dups" >> K false) true --
3.8 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
3.9 >> (Toplevel.no_timing oo IsarCmd.find_theorems));
3.10