author krauss Fri Feb 25 16:57:43 2011 +0100 (2011-02-25) changeset 41844 b933142e02d0 parent 41843 15d76ed6ea67 child 41845 6611b9cef38b
generalize find_theorems filters to work on raw propositions, too
```     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.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,
```