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;