--- a/src/Pure/Tools/find_theorems.ML Sat Feb 22 17:13:30 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sat Feb 22 18:07:31 2014 +0100
@@ -89,35 +89,10 @@
{goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
-
-(** theorems, either internal or external (without proof) **)
-
-datatype theorem =
- Internal of Facts.ref * thm |
- External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
-
-fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
- | prop_of (External (_, prop)) = prop;
-
-fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
- | nprems_of (External (_, prop)) = Logic.count_prems prop;
-
-fun size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm)
- | size_of (External (_, prop)) = size_of_term prop;
-
-fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm
- | major_prem_of (External (_, prop)) =
- Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop));
-
-fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
- | fact_ref_of (External (fact_ref, _)) = fact_ref;
-
-
-
(** search criterion filters **)
(*generated filters are to be of the form
- input: theorem
+ input: (Facts.ref * thm)
output: (p:int, s:int, t:int) option, where
NONE indicates no match
p is the primary sorting criterion
@@ -164,43 +139,45 @@
(* filter_name *)
-fun filter_name str_pat theorem =
- if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
+fun filter_name str_pat (thmref, _) =
+ if match_string str_pat (Facts.name_of_ref thmref)
then SOME (0, 0, 0) else NONE;
(* filter intro/elim/dest/solves rules *)
-fun filter_dest ctxt goal theorem =
+fun filter_dest ctxt goal (_, thm) =
let
val extract_dest =
- (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem],
+ (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
hd o Logic.strip_imp_prems);
val prems = Logic.prems_of_goal goal 1;
- fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
+ fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
val successful = prems |> map_filter try_subst;
in
(*if possible, keep best substitution (one with smallest size)*)
(*dest rules always have assumptions, so a dest with one
assumption is as good as an intro rule with none*)
- if not (null successful)
- then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
+ if not (null successful) then
+ SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
+ else NONE
end;
-fun filter_intro ctxt goal theorem =
+fun filter_intro ctxt goal (_, thm) =
let
- val extract_intro = (single o prop_of, Logic.strip_imp_concl);
+ val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
val concl = Logic.concl_of_goal goal 1;
- val ss = is_matching_thm extract_intro ctxt true concl theorem;
in
- if is_some ss then SOME (size_of theorem, nprems_of theorem, the ss) else NONE
+ (case is_matching_thm extract_intro ctxt true concl thm of
+ SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
+ | NONE => NONE)
end;
-fun filter_elim ctxt goal theorem =
- if nprems_of theorem > 0 then
+fun filter_elim ctxt goal (_, thm) =
+ if Thm.nprems_of thm > 0 then
let
- val rule = prop_of theorem;
+ val rule = Thm.full_prop_of thm;
val prems = Logic.prems_of_goal goal 1;
val goal_concl = Logic.concl_of_goal goal 1;
val rule_mp = hd (Logic.strip_imp_prems rule);
@@ -213,9 +190,10 @@
in
(*elim rules always have assumptions, so an elim with one
assumption is as good as an intro rule with none*)
- if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
- andalso not (null successful)
- then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
+ if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
+ andalso not (null successful) then
+ SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
+ else NONE
end
else NONE;
@@ -235,27 +213,25 @@
(limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
1 goal';
in
- fn Internal (_, thm) =>
- if is_some (Seq.pull (try_thm thm))
- then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE
- | External _ => NONE
+ fn (_, thm) =>
+ if is_some (Seq.pull (try_thm thm))
+ then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0)
+ else NONE
end;
(* filter_simp *)
-fun filter_simp ctxt t (Internal (_, thm)) =
- let
- val mksimps = Simplifier.mksimps ctxt;
- val extract_simp =
- (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
- val ss = is_matching_thm extract_simp ctxt false t thm;
- in
- if is_some ss
- then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss)
- else NONE
- end
- | filter_simp _ _ (External _) = NONE;
+fun filter_simp ctxt t (_, thm) =
+ let
+ val mksimps = Simplifier.mksimps ctxt;
+ val extract_simp =
+ (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
+ in
+ (case is_matching_thm extract_simp ctxt false t thm of
+ SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
+ | NONE => NONE)
+ end;
(* filter_pattern *)
@@ -274,11 +250,11 @@
let
val pat_consts = get_names pat;
- fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
- | check (theorem, c as SOME thm_consts) =
+ fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
+ | check ((_, thm), c as SOME thm_consts) =
(if subset (op =) (pat_consts, thm_consts) andalso
- Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
- then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c);
+ Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
+ then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
in check end;
@@ -320,18 +296,18 @@
fun filter_criterion ctxt opt_goal (b, c) =
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
-fun sorted_filter filters theorems =
+fun sorted_filter filters thms =
let
- fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
+ fun eval_filters thm = app_filters thm (SOME (0, 0, 0), NONE, filters);
(*filters return: (thm size, number of assumptions, substitution size) option, so
sort according to size of thm first, then number of assumptions,
then by the substitution size, then by term order *)
- fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) =
- prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
- ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0))));
+ fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) =
+ prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
+ ((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0))));
in
- grouped 100 Par_List.map eval_filters theorems
+ grouped 100 Par_List.map eval_filters thms
|> map_filter I |> sort result_ord |> map #2
end;
@@ -368,10 +344,10 @@
let
fun rem_c rev_seen [] = rev rev_seen
| rem_c rev_seen [x] = rem_c (x :: rev_seen) []
- | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
- if prop_of t aconv prop_of t'
- then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
- else rem_c (x :: rev_seen) (y :: xs);
+ | rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) =
+ if Thm.eq_thm_prop (thm, thm')
+ then rem_c rev_seen ((if nicer n n' then x else y) :: rest)
+ else rem_c (x :: rev_seen) (y :: rest);
in rem_c [] xs end;
in
@@ -396,7 +372,7 @@
fun rem_thm_dups nicer xs =
(xs ~~ (1 upto length xs))
- |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
+ |> sort (Term_Ord.fast_term_ord o pairself (Thm.full_prop_of o #2 o #1))
|> rem_cdups nicer
|> sort (int_ord o pairself #2)
|> map #1;
@@ -461,9 +437,8 @@
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
val opt_goal' = Option.map add_prems opt_goal;
in
- filter ctxt (map Internal (all_facts_of ctxt))
+ filter ctxt (all_facts_of ctxt)
{goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
- |> apsnd (map (fn Internal f => f))
end;
in
@@ -489,14 +464,10 @@
Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
end;
-fun pretty_theorem ctxt (Internal (thmref, thm)) =
- Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
- | pretty_theorem ctxt (External (thmref, prop)) =
- Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
-
in
-fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
+fun pretty_thm ctxt (thmref, thm) =
+ Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
fun pretty_theorems state opt_limit rem_dups raw_criteria =
let
@@ -505,7 +476,7 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (opt_found, theorems) =
- filter_theorems ctxt (map Internal (all_facts_of ctxt))
+ filter_theorems ctxt (all_facts_of ctxt)
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;
@@ -523,7 +494,7 @@
(if null theorems then [Pretty.str "nothing found"]
else
[Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
- grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) (rev theorems))
+ grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
end |> Pretty.fbreaks |> curry Pretty.blk 0;
end;