1.1 --- a/src/Pure/Isar/find_theorems.ML Thu May 26 10:05:11 2005 +0200
1.2 +++ b/src/Pure/Isar/find_theorems.ML Thu May 26 10:05:28 2005 +0200
1.3 @@ -28,46 +28,6 @@
1.4 |> map PureThy.selections |> List.concat;
1.5
1.6
1.7 -(* matching theorems *)
1.8 -
1.9 -local
1.10 -
1.11 -(*returns all those facts whose subterm extracted by extract can be
1.12 - instantiated to obj; the list is sorted according to the number of premises
1.13 - and the size of the required substitution*)
1.14 -fun select_match (extract_thms, extract_term) ctxt obj facts =
1.15 - let
1.16 - val match = #2 o Pattern.match (Sign.tsig_of (ProofContext.sign_of ctxt));
1.17 -
1.18 - fun match_size pat =
1.19 - let val subst = match (pat, obj) (*exception Pattern.MATCH*)
1.20 - in SOME (Vartab.foldl (op + o apsnd (Term.size_of_term o #2 o #2)) (0, subst)) end
1.21 - handle Pattern.MATCH => NONE;
1.22 -
1.23 - fun select (fact as (_, thm)) =
1.24 - let
1.25 - fun first_match (th :: ths) res =
1.26 - (case match_size (extract_term (Thm.prop_of th)) of
1.27 - SOME s => ((Thm.nprems_of th, s), fact) :: res
1.28 - | NONE => first_match ths res)
1.29 - | first_match [] res = res;
1.30 - in first_match (extract_thms thm) end;
1.31 -
1.32 - fun thm_ord (((p0, s0), _), ((p1, s1), _)) =
1.33 - prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0, s0), (p1, s1));
1.34 - in
1.35 - fold select facts []
1.36 - |> Library.sort thm_ord |> map #2
1.37 - end;
1.38 -
1.39 -in
1.40 -
1.41 -fun is_matching_thm extract ctxt prop fact =
1.42 - not (null (select_match extract ctxt prop [fact]));
1.43 -
1.44 -end;
1.45 -
1.46 -
1.47
1.48 (** search criteria **)
1.49
1.50 @@ -78,7 +38,8 @@
1.51 | read_criterion _ Intro = Intro
1.52 | read_criterion _ Elim = Elim
1.53 | read_criterion _ Dest = Dest
1.54 - | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term ctxt str)
1.55 + | read_criterion ctxt (Simp str) =
1.56 + Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
1.57 | read_criterion ctxt (Pattern str) =
1.58 Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
1.59
1.60 @@ -91,8 +52,8 @@
1.61 | Intro => Pretty.str (prfx "intro")
1.62 | Elim => Pretty.str (prfx "elim")
1.63 | Dest => Pretty.str (prfx "dest")
1.64 - | Simp t => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
1.65 - Pretty.quote (ProofContext.pretty_term ctxt t)]
1.66 + | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
1.67 + Pretty.quote (ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat))]
1.68 | Pattern pat => Pretty.enclose (prfx " \"") "\""
1.69 [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
1.70 end;
1.71 @@ -101,6 +62,27 @@
1.72
1.73 (** search criterion filters **)
1.74
1.75 +
1.76 +(* matching theorems *)
1.77 +
1.78 +fun is_matching_thm (extract_thms, extract_term) ctxt po obj thm =
1.79 + let
1.80 + val sg = ProofContext.sign_of ctxt;
1.81 + val tsig = Sign.tsig_of sg;
1.82 +
1.83 + val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
1.84 +
1.85 + fun matches pat =
1.86 + is_nontrivial pat andalso
1.87 + Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
1.88 + handle Pattern.MATCH => false;
1.89 +
1.90 + val match_thm = matches o extract_term o Thm.prop_of
1.91 + in
1.92 + List.exists match_thm (extract_thms thm)
1.93 + end;
1.94 +
1.95 +
1.96 (* filter_name *)
1.97
1.98 fun is_substring pat str =
1.99 @@ -132,27 +114,27 @@
1.100 not (Term.dest_Var concl mem prem_vars)
1.101 end;
1.102
1.103 -fun filter_elim_dest check_thm ctxt goal =
1.104 +fun filter_elim_dest check_thm ctxt goal (_,thm) =
1.105 let
1.106 val extract_elim =
1.107 (fn thm => if Thm.no_prems thm then [] else [thm],
1.108 hd o Logic.strip_imp_prems);
1.109 val prems = Logic.prems_of_goal goal 1;
1.110 in
1.111 - fn fact => prems |> List.exists (fn prem =>
1.112 - is_matching_thm extract_elim ctxt prem fact
1.113 - andalso (check_thm ctxt) (#2 fact))
1.114 + prems |>
1.115 + List.exists (fn prem =>
1.116 + is_matching_thm extract_elim ctxt true prem thm
1.117 + andalso (check_thm ctxt) thm)
1.118 end;
1.119
1.120 in
1.121
1.122 -fun filter_intro ctxt goal =
1.123 +fun filter_intro ctxt goal (_,thm) =
1.124 let
1.125 val extract_intro = (single, Logic.strip_imp_concl);
1.126 val concl = Logic.concl_of_goal goal 1;
1.127 in
1.128 - fn fact => is_matching_thm extract_intro ctxt concl fact
1.129 - andalso not (is_elim ctxt (#2 fact))
1.130 + is_matching_thm extract_intro ctxt true concl thm
1.131 end;
1.132
1.133 fun filter_elim ctxt = filter_elim_dest is_elim ctxt;
1.134 @@ -163,19 +145,19 @@
1.135
1.136 (* filter_simp *)
1.137
1.138 -fun filter_simp ctxt t =
1.139 +fun filter_simp ctxt t (_,thm) =
1.140 let
1.141 val (_, {mk_rews = {mk, ...}, ...}) =
1.142 MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
1.143 val extract_simp = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
1.144 - in is_matching_thm extract_simp ctxt t end;
1.145 + in is_matching_thm extract_simp ctxt false t thm end;
1.146
1.147
1.148 (* filter_pattern *)
1.149
1.150 -fun filter_pattern ctxt pat =
1.151 +fun filter_pattern ctxt pat (_, thm) =
1.152 let val tsig = Sign.tsig_of (ProofContext.sign_of ctxt)
1.153 - in fn (_, thm) => Pattern.matches_subterm tsig (pat, Thm.prop_of thm) end;
1.154 + in Pattern.matches_subterm tsig (pat, Thm.prop_of thm) end;
1.155
1.156
1.157 (* interpret criteria as filters *)
1.158 @@ -192,8 +174,8 @@
1.159 | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal
1.160 | filter_crit ctxt (SOME goal) Elim = filter_elim ctxt goal
1.161 | filter_crit ctxt (SOME goal) Dest = filter_dest ctxt goal
1.162 - | filter_crit ctxt _ (Simp str) = filter_simp ctxt str
1.163 - | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str;
1.164 + | filter_crit ctxt _ (Simp pat) = filter_simp ctxt pat
1.165 + | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
1.166
1.167 in
1.168