src/Pure/Tools/find_theorems.ML
changeset 41844 b933142e02d0
parent 41841 c27b0b37041a
child 41845 6611b9cef38b
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 14:25:52 2011 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:43 2011 +0100
     1.3 @@ -9,13 +9,18 @@
     1.4    datatype 'term criterion =
     1.5      Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
     1.6      Pattern of 'term
     1.7 +
     1.8 +  datatype theorem =
     1.9 +    Internal of Facts.ref * thm |
    1.10 +    External of Facts.ref * term
    1.11 +
    1.12    val tac_limit: int Unsynchronized.ref
    1.13    val limit: int Unsynchronized.ref
    1.14    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.15      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    1.16 -  val filter_facts: Proof.context -> (Facts.ref * thm) list -> thm option ->
    1.17 +  val filter_theorems: Proof.context -> theorem list -> thm option ->
    1.18      int option -> bool -> (bool * string criterion) list ->
    1.19 -    int option * (Facts.ref * thm) list
    1.20 +    int option * theorem list
    1.21  
    1.22    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.23  end;
    1.24 @@ -75,11 +80,29 @@
    1.25    end;
    1.26  
    1.27  
    1.28 +(** theorems, either internal or external (without proof) *)
    1.29 +
    1.30 +datatype theorem =
    1.31 +  Internal of Facts.ref * thm |
    1.32 +  External of Facts.ref * term;
    1.33 +
    1.34 +fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    1.35 +  | prop_of (External (_, prop)) = prop;
    1.36 +
    1.37 +fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
    1.38 +  | nprems_of (External (_, prop)) = Logic.count_prems prop;
    1.39 +
    1.40 +fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm
    1.41 +  | major_prem_of (External (_, prop)) =
    1.42 +      Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop));
    1.43 +
    1.44 +fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
    1.45 +  | fact_ref_of (External (fact_ref, _)) = fact_ref;
    1.46  
    1.47  (** search criterion filters **)
    1.48  
    1.49  (*generated filters are to be of the form
    1.50 -  input: (Facts.ref * thm)
    1.51 +  input: theorem
    1.52    output: (p:int, s:int) option, where
    1.53      NONE indicates no match
    1.54      p is the primary sorting criterion
    1.55 @@ -142,43 +165,43 @@
    1.56  
    1.57  (* filter_name *)
    1.58  
    1.59 -fun filter_name str_pat (thmref, _) =
    1.60 -  if match_string str_pat (Facts.name_of_ref thmref)
    1.61 +fun filter_name str_pat theorem =
    1.62 +  if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
    1.63    then SOME (0, 0) else NONE;
    1.64  
    1.65  
    1.66  (* filter intro/elim/dest/solves rules *)
    1.67  
    1.68 -fun filter_dest ctxt goal (_, thm) =
    1.69 +fun filter_dest ctxt goal theorem =
    1.70    let
    1.71      val extract_dest =
    1.72 -     (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
    1.73 +     (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem],
    1.74        hd o Logic.strip_imp_prems);
    1.75      val prems = Logic.prems_of_goal goal 1;
    1.76  
    1.77 -    fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm;
    1.78 +    fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem;
    1.79      val successful = prems |> map_filter try_subst;
    1.80    in
    1.81      (*if possible, keep best substitution (one with smallest size)*)
    1.82      (*dest rules always have assumptions, so a dest with one
    1.83        assumption is as good as an intro rule with none*)
    1.84      if not (null successful)
    1.85 -    then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
    1.86 +    then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
    1.87    end;
    1.88  
    1.89 -fun filter_intro doiff ctxt goal (_, thm) =
    1.90 +fun filter_intro doiff ctxt goal theorem =
    1.91    let
    1.92 -    val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
    1.93 +    val extract_intro = (single o prop_of, Logic.strip_imp_concl);
    1.94      val concl = Logic.concl_of_goal goal 1;
    1.95 -    val ss = is_matching_thm doiff extract_intro ctxt true concl thm;
    1.96 +    val ss = is_matching_thm doiff extract_intro ctxt true concl theorem;
    1.97    in
    1.98 -    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
    1.99 +    if is_some ss then SOME (nprems_of theorem, the ss) else NONE
   1.100    end;
   1.101  
   1.102 -fun filter_elim ctxt goal (_, thm) =
   1.103 -  if not (Thm.no_prems thm) then
   1.104 +fun filter_elim ctxt goal theorem =
   1.105 +  if nprems_of theorem > 0 then
   1.106      let
   1.107 -      val rule = Thm.full_prop_of thm;
   1.108 +      val rule = prop_of theorem;
   1.109        val prems = Logic.prems_of_goal goal 1;
   1.110        val goal_concl = Logic.concl_of_goal goal 1;
   1.111        val rule_mp = hd (Logic.strip_imp_prems rule);
   1.112 @@ -192,9 +215,9 @@
   1.113      in
   1.114        (*elim rules always have assumptions, so an elim with one
   1.115          assumption is as good as an intro rule with none*)
   1.116 -      if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
   1.117 +      if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem)
   1.118          andalso not (null successful)
   1.119 -      then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
   1.120 +      then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
   1.121      end
   1.122    else NONE
   1.123  
   1.124 @@ -207,29 +230,30 @@
   1.125        if Thm.no_prems thm then rtac thm 1 goal
   1.126        else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
   1.127    in
   1.128 -    fn (_, thm) =>
   1.129 +    fn Internal (_, thm) =>
   1.130        if is_some (Seq.pull (try_thm thm))
   1.131        then SOME (Thm.nprems_of thm, 0) else NONE
   1.132 +     | External _ => NONE
   1.133    end;
   1.134  
   1.135  
   1.136  (* filter_simp *)
   1.137  
   1.138 -fun filter_simp ctxt t (_, thm) =
   1.139 -  let
   1.140 -    val mksimps = Simplifier.mksimps (simpset_of ctxt);
   1.141 -    val extract_simp =
   1.142 -      (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   1.143 -    val ss = is_matching_thm false extract_simp ctxt false t thm;
   1.144 -  in
   1.145 -    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   1.146 -  end;
   1.147 +fun filter_simp ctxt t (Internal (_, thm)) =
   1.148 +      let
   1.149 +        val mksimps = Simplifier.mksimps (simpset_of ctxt);
   1.150 +        val extract_simp =
   1.151 +          (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   1.152 +        val ss = is_matching_thm false extract_simp ctxt false t thm;
   1.153 +      in
   1.154 +        if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   1.155 +      end
   1.156 +  | filter_simp _ _ (External _) = NONE;
   1.157  
   1.158  
   1.159  (* filter_pattern *)
   1.160  
   1.161  fun get_names t = Term.add_const_names t (Term.add_free_names t []);
   1.162 -fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
   1.163  
   1.164  (*Including all constants and frees is only sound because
   1.165    matching uses higher-order patterns. If full matching
   1.166 @@ -246,10 +270,10 @@
   1.167    let
   1.168      val pat_consts = get_names pat;
   1.169  
   1.170 -    fun check (t, NONE) = check (t, SOME (get_thm_names t))
   1.171 -      | check ((_, thm), c as SOME thm_consts) =
   1.172 +    fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
   1.173 +      | check (theorem, c as SOME thm_consts) =
   1.174           (if subset (op =) (pat_consts, thm_consts) andalso
   1.175 -            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
   1.176 +            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem)
   1.177            then SOME (0, 0) else NONE, c);
   1.178    in check end;
   1.179  
   1.180 @@ -297,16 +321,16 @@
   1.181  fun filter_criterion ctxt opt_goal (b, c) =
   1.182    (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
   1.183  
   1.184 -fun sorted_filter filters thms =
   1.185 +fun sorted_filter filters theorems =
   1.186    let
   1.187 -    fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters);
   1.188 +    fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters);
   1.189  
   1.190      (*filters return: (number of assumptions, substitution size) option, so
   1.191        sort (desc. in both cases) according to number of assumptions first,
   1.192        then by the substitution size*)
   1.193 -    fun thm_ord (((p0, s0), _), ((p1, s1), _)) =
   1.194 +    fun result_ord (((p0, s0), _), ((p1, s1), _)) =
   1.195        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
   1.196 -  in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
   1.197 +  in map_filter eval_filters theorems |> sort result_ord |> map #2 end;
   1.198  
   1.199  fun lazy_filter filters =
   1.200    let
   1.201 @@ -342,9 +366,9 @@
   1.202    let
   1.203      fun rem_c rev_seen [] = rev rev_seen
   1.204        | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
   1.205 -      | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
   1.206 -          if Thm.eq_thm_prop (t, t')
   1.207 -          then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
   1.208 +      | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
   1.209 +          if (prop_of t) aconv (prop_of t')
   1.210 +          then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
   1.211            else rem_c (x :: rev_seen) (y :: xs)
   1.212    in rem_c [] xs end;
   1.213  
   1.214 @@ -367,7 +391,7 @@
   1.215  
   1.216  fun rem_thm_dups nicer xs =
   1.217    xs ~~ (1 upto length xs)
   1.218 -  |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   1.219 +  |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
   1.220    |> rem_cdups nicer
   1.221    |> sort (int_ord o pairself #2)
   1.222    |> map #1;
   1.223 @@ -385,12 +409,14 @@
   1.224    in
   1.225      maps Facts.selections
   1.226       (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
   1.227 +
   1.228 +
   1.229        visible_facts (ProofContext.facts_of ctxt))
   1.230    end;
   1.231  
   1.232  val limit = Unsynchronized.ref 40;
   1.233  
   1.234 -fun filter_facts ctxt facts opt_goal opt_limit rem_dups raw_criteria =
   1.235 +fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
   1.236    let
   1.237      val assms =
   1.238        ProofContext.get_fact ctxt (Facts.named "local.assms")
   1.239 @@ -401,9 +427,9 @@
   1.240      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   1.241      val filters = map (filter_criterion ctxt opt_goal') criteria;
   1.242  
   1.243 -    fun find_all facts =
   1.244 +    fun find_all theorems =
   1.245        let
   1.246 -        val raw_matches = sorted_filter filters facts;
   1.247 +        val raw_matches = sorted_filter filters theorems;
   1.248  
   1.249          val matches =
   1.250            if rem_dups
   1.251 @@ -419,9 +445,12 @@
   1.252        then find_all
   1.253        else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
   1.254  
   1.255 -  in find facts end;
   1.256 +  in find theorems end;
   1.257  
   1.258 -fun find_theorems ctxt = filter_facts ctxt (all_facts_of ctxt)
   1.259 +fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   1.260 +  filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
   1.261 +     rem_dups raw_criteria
   1.262 +  |> apsnd (map (fn Internal f => f));
   1.263  
   1.264  fun pretty_thm ctxt (thmref, thm) = Pretty.block
   1.265    [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,