src/Pure/Tools/find_theorems.ML
 changeset 53632 96808429b9ec parent 52982 8e78bd316a53 child 53633 69f1221fc892
```     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;
```