1.1 --- a/src/Pure/Tools/find_theorems.ML Fri Sep 13 23:52:01 2013 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML Sat Sep 14 20:56:12 2013 +1000
1.3 @@ -108,6 +108,9 @@
1.4 fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
1.5 | nprems_of (External (_, prop)) = Logic.count_prems prop;
1.6
1.7 +fun size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm)
1.8 + | size_of (External (_, prop)) = size_of_term prop;
1.9 +
1.10 fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm
1.11 | major_prem_of (External (_, prop)) =
1.12 Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop));
1.13 @@ -121,16 +124,16 @@
1.14
1.15 (*generated filters are to be of the form
1.16 input: theorem
1.17 - output: (p:int, s:int) option, where
1.18 + output: (p:int, s:int, t:int) option, where
1.19 NONE indicates no match
1.20 p is the primary sorting criterion
1.21 + (eg. size of term)
1.22 + s is the secondary sorting criterion
1.23 (eg. number of assumptions in the theorem)
1.24 - s is the secondary sorting criterion
1.25 + t is the tertiary sorting criterion
1.26 (eg. size of the substitution for intro, elim and dest)
1.27 when applying a set of filters to a thm, fold results in:
1.28 - (biggest p, sum of all s)
1.29 - currently p and s only matter for intro, elim, dest and simp filters,
1.30 - otherwise the default ordering is used.
1.31 + (max p, max s, sum of all t)
1.32 *)
1.33
1.34
1.35 @@ -169,7 +172,7 @@
1.36
1.37 fun filter_name str_pat theorem =
1.38 if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
1.39 - then SOME (0, 0) else NONE;
1.40 + then SOME (0, 0, 0) else NONE;
1.41
1.42
1.43 (* filter intro/elim/dest/solves rules *)
1.44 @@ -188,7 +191,7 @@
1.45 (*dest rules always have assumptions, so a dest with one
1.46 assumption is as good as an intro rule with none*)
1.47 if not (null successful)
1.48 - then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.49 + then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.50 end;
1.51
1.52 fun filter_intro ctxt goal theorem =
1.53 @@ -197,7 +200,7 @@
1.54 val concl = Logic.concl_of_goal goal 1;
1.55 val ss = is_matching_thm extract_intro ctxt true concl theorem;
1.56 in
1.57 - if is_some ss then SOME (nprems_of theorem, the ss) else NONE
1.58 + if is_some ss then SOME (size_of theorem, nprems_of theorem, the ss) else NONE
1.59 end;
1.60
1.61 fun filter_elim ctxt goal theorem =
1.62 @@ -218,7 +221,7 @@
1.63 assumption is as good as an intro rule with none*)
1.64 if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
1.65 andalso not (null successful)
1.66 - then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.67 + then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.68 end
1.69 else NONE;
1.70
1.71 @@ -238,7 +241,7 @@
1.72 in
1.73 fn Internal (_, thm) =>
1.74 if is_some (Seq.pull (try_thm thm))
1.75 - then SOME (Thm.nprems_of thm, 0) else NONE
1.76 + then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE
1.77 | External _ => NONE
1.78 end;
1.79
1.80 @@ -252,7 +255,9 @@
1.81 (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
1.82 val ss = is_matching_thm extract_simp ctxt false t thm;
1.83 in
1.84 - if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
1.85 + if is_some ss
1.86 + then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss)
1.87 + else NONE
1.88 end
1.89 | filter_simp _ _ (External _) = NONE;
1.90
1.91 @@ -277,7 +282,7 @@
1.92 | check (theorem, c as SOME thm_consts) =
1.93 (if subset (op =) (pat_consts, thm_consts) andalso
1.94 Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
1.95 - then SOME (0, 0) else NONE, c);
1.96 + then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c);
1.97 in check end;
1.98
1.99
1.100 @@ -300,9 +305,9 @@
1.101 | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
1.102 | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
1.103
1.104 -fun opt_not x = if is_some x then NONE else SOME (0, 0);
1.105 +fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
1.106
1.107 -fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
1.108 +fun opt_add (SOME (a, c, x)) (SOME (b, d, y)) = SOME (Int.max (a,b), Int.max (c, d), x + y : int)
1.109 | opt_add _ _ = NONE;
1.110
1.111 fun app_filters thm =
1.112 @@ -321,13 +326,14 @@
1.113
1.114 fun sorted_filter filters theorems =
1.115 let
1.116 - fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters);
1.117 + fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
1.118
1.119 - (*filters return: (number of assumptions, substitution size) option, so
1.120 - sort (desc. in both cases) according to number of assumptions first,
1.121 - then by the substitution size*)
1.122 - fun result_ord (((p0, s0), _), ((p1, s1), _)) =
1.123 - prod_ord int_ord int_ord ((p1, s1), (p0, s0));
1.124 + (*filters return: (thm size, number of assumptions, substitution size) option, so
1.125 + sort according to size of thm first, then number of assumptions,
1.126 + then by the substitution size, then by term order *)
1.127 + fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) =
1.128 + prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
1.129 + ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0))));
1.130 in
1.131 grouped 100 Par_List.map eval_filters theorems
1.132 |> map_filter I |> sort result_ord |> map #2
1.133 @@ -338,7 +344,7 @@
1.134 fun lazy_match thms = Seq.make (fn () => first_match thms)
1.135 and first_match [] = NONE
1.136 | first_match (thm :: thms) =
1.137 - (case app_filters thm (SOME (0, 0), NONE, filters) of
1.138 + (case app_filters thm (SOME (0, 0, 0), NONE, filters) of
1.139 NONE => first_match thms
1.140 | SOME (_, t) => SOME (t, lazy_match thms));
1.141 in lazy_match end;