1 (* Title: Pure/Isar/find_theorems.ML |
|
2 Author: Rafal Kolanski and Gerwin Klein, NICTA |
|
3 |
|
4 Retrieve theorems from proof context. |
|
5 *) |
|
6 |
|
7 signature FIND_THEOREMS = |
|
8 sig |
|
9 val limit: int ref |
|
10 val tac_limit: int ref |
|
11 |
|
12 datatype 'term criterion = |
|
13 Name of string | Intro | Elim | Dest | Solves | Simp of 'term | |
|
14 Pattern of 'term |
|
15 |
|
16 val find_theorems: Proof.context -> thm option -> bool -> |
|
17 (bool * string criterion) list -> (Facts.ref * thm) list |
|
18 |
|
19 val print_theorems: Proof.context -> thm option -> int option -> bool -> |
|
20 (bool * string criterion) list -> unit |
|
21 end; |
|
22 |
|
23 structure FindTheorems: FIND_THEOREMS = |
|
24 struct |
|
25 |
|
26 (** search criteria **) |
|
27 |
|
28 datatype 'term criterion = |
|
29 Name of string | Intro | Elim | Dest | Solves | Simp of 'term | |
|
30 Pattern of 'term; |
|
31 |
|
32 fun read_criterion _ (Name name) = Name name |
|
33 | read_criterion _ Intro = Intro |
|
34 | read_criterion _ Elim = Elim |
|
35 | read_criterion _ Dest = Dest |
|
36 | read_criterion _ Solves = Solves |
|
37 | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) |
|
38 | read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str); |
|
39 |
|
40 fun pretty_criterion ctxt (b, c) = |
|
41 let |
|
42 fun prfx s = if b then s else "-" ^ s; |
|
43 in |
|
44 (case c of |
|
45 Name name => Pretty.str (prfx "name: " ^ quote name) |
|
46 | Intro => Pretty.str (prfx "intro") |
|
47 | Elim => Pretty.str (prfx "elim") |
|
48 | Dest => Pretty.str (prfx "dest") |
|
49 | Solves => Pretty.str (prfx "solves") |
|
50 | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, |
|
51 Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] |
|
52 | Pattern pat => Pretty.enclose (prfx " \"") "\"" |
|
53 [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) |
|
54 end; |
|
55 |
|
56 (** search criterion filters **) |
|
57 |
|
58 (*generated filters are to be of the form |
|
59 input: (Facts.ref * thm) |
|
60 output: (p:int, s:int) option, where |
|
61 NONE indicates no match |
|
62 p is the primary sorting criterion |
|
63 (eg. number of assumptions in the theorem) |
|
64 s is the secondary sorting criterion |
|
65 (eg. size of the substitution for intro, elim and dest) |
|
66 when applying a set of filters to a thm, fold results in: |
|
67 (biggest p, sum of all s) |
|
68 currently p and s only matter for intro, elim, dest and simp filters, |
|
69 otherwise the default ordering is used. |
|
70 *) |
|
71 |
|
72 |
|
73 (* matching theorems *) |
|
74 |
|
75 fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; |
|
76 |
|
77 (*extract terms from term_src, refine them to the parts that concern us, |
|
78 if po try match them against obj else vice versa. |
|
79 trivial matches are ignored. |
|
80 returns: smallest substitution size*) |
|
81 fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = |
|
82 let |
|
83 val thy = ProofContext.theory_of ctxt; |
|
84 |
|
85 fun matches pat = |
|
86 is_nontrivial thy pat andalso |
|
87 Pattern.matches thy (if po then (pat, obj) else (obj, pat)); |
|
88 |
|
89 fun substsize pat = |
|
90 let val (_, subst) = |
|
91 Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) |
|
92 in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; |
|
93 |
|
94 fun bestmatch [] = NONE |
|
95 | bestmatch xs = SOME (foldr1 Int.min xs); |
|
96 |
|
97 val match_thm = matches o refine_term; |
|
98 in |
|
99 map (substsize o refine_term) (filter match_thm (extract_terms term_src)) |
|
100 |> bestmatch |
|
101 end; |
|
102 |
|
103 |
|
104 (* filter_name *) |
|
105 |
|
106 fun filter_name str_pat (thmref, _) = |
|
107 if match_string str_pat (Facts.name_of_ref thmref) |
|
108 then SOME (0, 0) else NONE; |
|
109 |
|
110 (* filter intro/elim/dest/solves rules *) |
|
111 |
|
112 fun filter_dest ctxt goal (_, thm) = |
|
113 let |
|
114 val extract_dest = |
|
115 (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], |
|
116 hd o Logic.strip_imp_prems); |
|
117 val prems = Logic.prems_of_goal goal 1; |
|
118 |
|
119 fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; |
|
120 val successful = prems |> map_filter try_subst; |
|
121 in |
|
122 (*if possible, keep best substitution (one with smallest size)*) |
|
123 (*dest rules always have assumptions, so a dest with one |
|
124 assumption is as good as an intro rule with none*) |
|
125 if not (null successful) |
|
126 then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE |
|
127 end; |
|
128 |
|
129 fun filter_intro ctxt goal (_, thm) = |
|
130 let |
|
131 val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); |
|
132 val concl = Logic.concl_of_goal goal 1; |
|
133 val ss = is_matching_thm extract_intro ctxt true concl thm; |
|
134 in |
|
135 if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE |
|
136 end; |
|
137 |
|
138 fun filter_elim ctxt goal (_, thm) = |
|
139 if not (Thm.no_prems thm) then |
|
140 let |
|
141 val rule = Thm.full_prop_of thm; |
|
142 val prems = Logic.prems_of_goal goal 1; |
|
143 val goal_concl = Logic.concl_of_goal goal 1; |
|
144 val rule_mp = hd (Logic.strip_imp_prems rule); |
|
145 val rule_concl = Logic.strip_imp_concl rule; |
|
146 fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); |
|
147 val rule_tree = combine rule_mp rule_concl; |
|
148 fun goal_tree prem = combine prem goal_concl; |
|
149 fun try_subst prem = |
|
150 is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; |
|
151 val successful = prems |> map_filter try_subst; |
|
152 in |
|
153 (*elim rules always have assumptions, so an elim with one |
|
154 assumption is as good as an intro rule with none*) |
|
155 if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) |
|
156 andalso not (null successful) |
|
157 then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE |
|
158 end |
|
159 else NONE |
|
160 |
|
161 val tac_limit = ref 5; |
|
162 |
|
163 fun filter_solves ctxt goal = let |
|
164 val baregoal = Logic.get_goal (prop_of goal) 1; |
|
165 |
|
166 fun etacn thm i = Seq.take (!tac_limit) o etac thm i; |
|
167 fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal |
|
168 else (etacn thm THEN_ALL_NEW |
|
169 (Goal.norm_hhf_tac THEN' |
|
170 Method.assumption_tac ctxt)) 1 goal; |
|
171 in |
|
172 fn (_, thm) => if (is_some o Seq.pull o try_thm) thm |
|
173 then SOME (Thm.nprems_of thm, 0) else NONE |
|
174 end; |
|
175 |
|
176 (* filter_simp *) |
|
177 |
|
178 fun filter_simp ctxt t (_, thm) = |
|
179 let |
|
180 val (_, {mk_rews = {mk, ...}, ...}) = |
|
181 Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); |
|
182 val extract_simp = |
|
183 (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); |
|
184 val ss = is_matching_thm extract_simp ctxt false t thm |
|
185 in |
|
186 if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE |
|
187 end; |
|
188 |
|
189 |
|
190 (* filter_pattern *) |
|
191 |
|
192 fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []); |
|
193 fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); |
|
194 (* Including all constants and frees is only sound because |
|
195 matching uses higher-order patterns. If full matching |
|
196 were used, then constants that may be subject to |
|
197 beta-reduction after substitution of frees should |
|
198 not be included for LHS set because they could be |
|
199 thrown away by the substituted function. |
|
200 e.g. for (?F 1 2) do not include 1 or 2, if it were |
|
201 possible for ?F to be (% x y. 3) |
|
202 The largest possible set should always be included on |
|
203 the RHS. *) |
|
204 |
|
205 fun filter_pattern ctxt pat = let |
|
206 val pat_consts = get_names pat; |
|
207 |
|
208 fun check (t, NONE) = check (t, SOME (get_thm_names t)) |
|
209 | check ((_, thm), c as SOME thm_consts) = |
|
210 (if pat_consts subset_string thm_consts |
|
211 andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt) |
|
212 (pat, Thm.full_prop_of thm)) |
|
213 then SOME (0, 0) else NONE, c); |
|
214 in check end; |
|
215 |
|
216 (* interpret criteria as filters *) |
|
217 |
|
218 local |
|
219 |
|
220 fun err_no_goal c = |
|
221 error ("Current goal required for " ^ c ^ " search criterion"); |
|
222 |
|
223 val fix_goal = Thm.prop_of; |
|
224 val fix_goalo = Option.map fix_goal; |
|
225 |
|
226 fun filter_crit _ _ (Name name) = apfst (filter_name name) |
|
227 | filter_crit _ NONE Intro = err_no_goal "intro" |
|
228 | filter_crit _ NONE Elim = err_no_goal "elim" |
|
229 | filter_crit _ NONE Dest = err_no_goal "dest" |
|
230 | filter_crit _ NONE Solves = err_no_goal "solves" |
|
231 | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt |
|
232 (fix_goal goal)) |
|
233 | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt |
|
234 (fix_goal goal)) |
|
235 | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt |
|
236 (fix_goal goal)) |
|
237 | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) |
|
238 | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) |
|
239 | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; |
|
240 |
|
241 fun opt_not x = if is_some x then NONE else SOME (0, 0); |
|
242 |
|
243 fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) |
|
244 | opt_add _ _ = NONE; |
|
245 |
|
246 fun app_filters thm = let |
|
247 fun app (NONE, _, _) = NONE |
|
248 | app (SOME v, consts, []) = SOME (v, thm) |
|
249 | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts) |
|
250 in app (opt_add r r', consts', fs) end; |
|
251 in app end; |
|
252 |
|
253 in |
|
254 |
|
255 fun filter_criterion ctxt opt_goal (b, c) = |
|
256 (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; |
|
257 |
|
258 fun all_filters filters thms = |
|
259 let |
|
260 fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters); |
|
261 |
|
262 (*filters return: (number of assumptions, substitution size) option, so |
|
263 sort (desc. in both cases) according to number of assumptions first, |
|
264 then by the substitution size*) |
|
265 fun thm_ord (((p0, s0), _), ((p1, s1), _)) = |
|
266 prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
|
267 in map_filter eval_filters thms |> sort thm_ord |> map #2 end; |
|
268 |
|
269 end; |
|
270 |
|
271 |
|
272 (* removing duplicates, preferring nicer names, roughly n log n *) |
|
273 |
|
274 local |
|
275 |
|
276 val index_ord = option_ord (K EQUAL); |
|
277 val hidden_ord = bool_ord o pairself NameSpace.is_hidden; |
|
278 val qual_ord = int_ord o pairself (length o NameSpace.explode); |
|
279 val txt_ord = int_ord o pairself size; |
|
280 |
|
281 fun nicer_name (x, i) (y, j) = |
|
282 (case hidden_ord (x, y) of EQUAL => |
|
283 (case index_ord (i, j) of EQUAL => |
|
284 (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) |
|
285 | ord => ord) |
|
286 | ord => ord) <> GREATER; |
|
287 |
|
288 fun rem_cdups nicer xs = |
|
289 let |
|
290 fun rem_c rev_seen [] = rev rev_seen |
|
291 | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] |
|
292 | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = |
|
293 if Thm.eq_thm_prop (t, t') |
|
294 then rem_c rev_seen ((if nicer n n' then x else y) :: xs) |
|
295 else rem_c (x :: rev_seen) (y :: xs) |
|
296 in rem_c [] xs end; |
|
297 |
|
298 in |
|
299 |
|
300 fun nicer_shortest ctxt = let |
|
301 val ns = ProofContext.theory_of ctxt |
|
302 |> PureThy.facts_of |
|
303 |> Facts.space_of; |
|
304 |
|
305 val len_sort = sort (int_ord o (pairself size)); |
|
306 fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of |
|
307 [] => s |
|
308 | s'::_ => s'); |
|
309 |
|
310 fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
|
311 nicer_name (shorten x, i) (shorten y, j) |
|
312 | nicer (Facts.Fact _) (Facts.Named _) = true |
|
313 | nicer (Facts.Named _) (Facts.Fact _) = false; |
|
314 in nicer end; |
|
315 |
|
316 fun rem_thm_dups nicer xs = |
|
317 xs ~~ (1 upto length xs) |
|
318 |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) |
|
319 |> rem_cdups nicer |
|
320 |> sort (int_ord o pairself #2) |
|
321 |> map #1; |
|
322 |
|
323 end; |
|
324 |
|
325 |
|
326 (* print_theorems *) |
|
327 |
|
328 fun all_facts_of ctxt = |
|
329 maps Facts.selections |
|
330 (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ |
|
331 Facts.dest_static [] (ProofContext.facts_of ctxt)); |
|
332 |
|
333 val limit = ref 40; |
|
334 |
|
335 fun find_theorems ctxt opt_goal rem_dups raw_criteria = |
|
336 let |
|
337 val add_prems = Seq.hd o (TRY (Method.insert_tac |
|
338 (Assumption.prems_of ctxt) 1)); |
|
339 val opt_goal' = Option.map add_prems opt_goal; |
|
340 |
|
341 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
|
342 val filters = map (filter_criterion ctxt opt_goal') criteria; |
|
343 |
|
344 val raw_matches = all_filters filters (all_facts_of ctxt); |
|
345 |
|
346 val matches = |
|
347 if rem_dups |
|
348 then rem_thm_dups (nicer_shortest ctxt) raw_matches |
|
349 else raw_matches; |
|
350 in matches end; |
|
351 |
|
352 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let |
|
353 val start = start_timing (); |
|
354 |
|
355 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
|
356 val matches = find_theorems ctxt opt_goal rem_dups raw_criteria; |
|
357 |
|
358 val len = length matches; |
|
359 val lim = the_default (! limit) opt_limit; |
|
360 val thms = Library.drop (len - lim, matches); |
|
361 |
|
362 val end_msg = " in " ^ |
|
363 (List.nth (String.tokens Char.isSpace (end_timing start), 3)) |
|
364 ^ " secs" |
|
365 in |
|
366 Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) |
|
367 :: Pretty.str "" :: |
|
368 (if null thms then [Pretty.str ("nothing found" ^ end_msg)] |
|
369 else |
|
370 [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^ |
|
371 (if len <= lim then "" |
|
372 else " (" ^ string_of_int lim ^ " displayed)") |
|
373 ^ end_msg ^ ":"), Pretty.str ""] @ |
|
374 map Display.pretty_fact thms) |
|
375 |> Pretty.chunks |> Pretty.writeln |
|
376 end |
|
377 |
|
378 end; |
|