src/Pure/Tools/find_theorems.ML
 author wenzelm Wed Nov 26 20:05:34 2014 +0100 (2014-11-26) changeset 59058 a78612c67ec0 parent 58928 23d0ffd48006 child 59083 88b0b1f28adc permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
1 (*  Title:      Pure/Tools/find_theorems.ML
2     Author:     Rafal Kolanski and Gerwin Klein, NICTA
3     Author:     Lars Noschinski and Alexander Krauss, TU Muenchen
5 Retrieve theorems from proof context.
6 *)
8 signature FIND_THEOREMS =
9 sig
10   datatype 'term criterion =
11     Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
12   type 'term query = {
13     goal: thm option,
14     limit: int option,
15     rem_dups: bool,
16     criteria: (bool * 'term criterion) list
17   }
18   val read_query: Position.T -> string -> (bool * string criterion) list
19   val find_theorems: Proof.context -> thm option -> int option -> bool ->
20     (bool * term criterion) list -> int option * (Facts.ref * thm) list
21   val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
22     (bool * string criterion) list -> int option * (Facts.ref * thm) list
23   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
24 end;
26 structure Find_Theorems: FIND_THEOREMS =
27 struct
29 (** search criteria **)
31 datatype 'term criterion =
32   Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
34 fun apply_dummies tm =
35   let
36     val (xs, _) = Term.strip_abs tm;
37     val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
38   in #1 (Term.replace_dummy_patterns tm' 1) end;
40 fun parse_pattern ctxt nm =
41   let
42     val consts = Proof_Context.consts_of ctxt;
43     val nm' =
44       (case Syntax.parse_term ctxt nm of
45         Const (c, _) => c
46       | _ => Consts.intern consts nm);
47   in
48     (case try (Consts.the_abbreviation consts) nm' of
49       SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
50     | NONE => Proof_Context.read_term_pattern ctxt nm)
51   end;
53 fun read_criterion _ (Name name) = Name name
54   | read_criterion _ Intro = Intro
55   | read_criterion _ Elim = Elim
56   | read_criterion _ Dest = Dest
57   | read_criterion _ Solves = Solves
58   | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
59   | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
61 fun pretty_criterion ctxt (b, c) =
62   let
63     fun prfx s = if b then s else "-" ^ s;
64   in
65     (case c of
66       Name name => Pretty.str (prfx "name: " ^ quote name)
67     | Intro => Pretty.str (prfx "intro")
68     | Elim => Pretty.str (prfx "elim")
69     | Dest => Pretty.str (prfx "dest")
70     | Solves => Pretty.str (prfx "solves")
71     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
72         Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
73     | Pattern pat => Pretty.enclose (prfx "\"") "\""
74         [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
75   end;
79 (** queries **)
81 type 'term query = {
82   goal: thm option,
83   limit: int option,
84   rem_dups: bool,
85   criteria: (bool * 'term criterion) list
86 };
88 fun map_criteria f {goal, limit, rem_dups, criteria} =
89   {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
92 (** search criterion filters **)
94 (*generated filters are to be of the form
95   input: (Facts.ref * thm)
96   output: (p:int, s:int, t:int) option, where
97     NONE indicates no match
98     p is the primary sorting criterion
99       (eg. size of term)
100     s is the secondary sorting criterion
101       (eg. number of assumptions in the theorem)
102     t is the tertiary sorting criterion
103       (eg. size of the substitution for intro, elim and dest)
104   when applying a set of filters to a thm, fold results in:
105     (max p, max s, sum of all t)
106 *)
109 (* matching theorems *)
111 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
113 (*extract terms from term_src, refine them to the parts that concern us,
114   if po try match them against obj else vice versa.
115   trivial matches are ignored.
116   returns: smallest substitution size*)
117 fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
118   let
119     val thy = Proof_Context.theory_of ctxt;
121     fun matches pat =
122       is_nontrivial thy pat andalso
123       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
125     fun subst_size pat =
126       let val (_, subst) =
127         Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
128       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
130     fun best_match [] = NONE
131       | best_match xs = SOME (foldl1 Int.min xs);
133     val match_thm = matches o refine_term;
134   in
135     map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
136     |> best_match
137   end;
140 (* filter_name *)
142 fun filter_name str_pat (thmref, _) =
143   if match_string str_pat (Facts.name_of_ref thmref)
144   then SOME (0, 0, 0) else NONE;
147 (* filter intro/elim/dest/solves rules *)
149 fun filter_dest ctxt goal (_, thm) =
150   let
151     val extract_dest =
152      (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
153       hd o Logic.strip_imp_prems);
154     val prems = Logic.prems_of_goal goal 1;
156     fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
157     val successful = prems |> map_filter try_subst;
158   in
159     (*if possible, keep best substitution (one with smallest size)*)
160     (*dest rules always have assumptions, so a dest with one
161       assumption is as good as an intro rule with none*)
162     if not (null successful) then
163       SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
164     else NONE
165   end;
167 fun filter_intro ctxt goal (_, thm) =
168   let
169     val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
170     val concl = Logic.concl_of_goal goal 1;
171   in
172     (case is_matching_thm extract_intro ctxt true concl thm of
173       SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
174     | NONE => NONE)
175   end;
177 fun filter_elim ctxt goal (_, thm) =
178   if Thm.nprems_of thm > 0 then
179     let
180       val rule = Thm.full_prop_of thm;
181       val prems = Logic.prems_of_goal goal 1;
182       val goal_concl = Logic.concl_of_goal goal 1;
183       val rule_mp = hd (Logic.strip_imp_prems rule);
184       val rule_concl = Logic.strip_imp_concl rule;
185       fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) \$ (t1 \$ t2);  (* FIXME ?!? *)
186       val rule_tree = combine rule_mp rule_concl;
187       fun goal_tree prem = combine prem goal_concl;
188       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
189       val successful = prems |> map_filter try_subst;
190     in
191       (*elim rules always have assumptions, so an elim with one
192         assumption is as good as an intro rule with none*)
193       if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
194           andalso not (null successful) then
195         SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
196       else NONE
197     end
198   else NONE;
200 fun filter_solves ctxt goal =
201   let
202     val thy' =
203       Proof_Context.theory_of ctxt
204       |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
205     val ctxt' = Proof_Context.transfer thy' ctxt;
206     val goal' = Thm.transfer thy' goal;
208     fun limited_etac thm i =
209       Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
210         eresolve_tac [thm] i;
211     fun try_thm thm =
212       if Thm.no_prems thm then resolve_tac [thm] 1 goal'
213       else
214         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
215           1 goal';
216   in
217     fn (_, thm) =>
218       if is_some (Seq.pull (try_thm thm))
219       then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0)
220       else NONE
221   end;
224 (* filter_simp *)
226 fun filter_simp ctxt t (_, thm) =
227   let
228     val mksimps = Simplifier.mksimps ctxt;
229     val extract_simp =
230       (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
231   in
232     (case is_matching_thm extract_simp ctxt false t thm of
233       SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
234     | NONE => NONE)
235   end;
238 (* filter_pattern *)
240 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
242 (*Including all constants and frees is only sound because matching
243   uses higher-order patterns. If full matching were used, then
244   constants that may be subject to beta-reduction after substitution
245   of frees should not be included for LHS set because they could be
246   thrown away by the substituted function.  E.g. for (?F 1 2) do not
247   include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
248   largest possible set should always be included on the RHS.*)
250 fun filter_pattern ctxt pat =
251   let
252     val pat_consts = get_names pat;
254     fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
255       | check ((_, thm), c as SOME thm_consts) =
256          (if subset (op =) (pat_consts, thm_consts) andalso
257             Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
258           then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
259   in check end;
262 (* interpret criteria as filters *)
264 local
266 fun err_no_goal c =
267   error ("Current goal required for " ^ c ^ " search criterion");
269 fun filter_crit _ _ (Name name) = apfst (filter_name name)
270   | filter_crit _ NONE Intro = err_no_goal "intro"
271   | filter_crit _ NONE Elim = err_no_goal "elim"
272   | filter_crit _ NONE Dest = err_no_goal "dest"
273   | filter_crit _ NONE Solves = err_no_goal "solves"
274   | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
275   | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
276   | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
277   | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
278   | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
279   | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
281 fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
283 fun opt_add (SOME (a, c, x)) (SOME (b, d, y)) = SOME (Int.max (a,b), Int.max (c, d), x + y : int)
284   | opt_add _ _ = NONE;
286 fun app_filters thm =
287   let
288     fun app (NONE, _, _) = NONE
289       | app (SOME v, _, []) = SOME (v, thm)
290       | app (r, consts, f :: fs) =
291           let val (r', consts') = f (thm, consts)
292           in app (opt_add r r', consts', fs) end;
293   in app end;
295 in
297 fun filter_criterion ctxt opt_goal (b, c) =
298   (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
300 fun sorted_filter filters thms =
301   let
302     fun eval_filters thm = app_filters thm (SOME (0, 0, 0), NONE, filters);
304     (*filters return: (thm size, number of assumptions, substitution size) option, so
305       sort according to size of thm first, then number of assumptions,
306       then by the substitution size, then by term order *)
307     fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) =
308       prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
309          ((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0))));
310   in
311     grouped 100 Par_List.map eval_filters thms
312     |> map_filter I |> sort result_ord |> map #2
313   end;
315 fun lazy_filter filters =
316   let
317     fun lazy_match thms = Seq.make (fn () => first_match thms)
318     and first_match [] = NONE
319       | first_match (thm :: thms) =
320           (case app_filters thm (SOME (0, 0, 0), NONE, filters) of
321             NONE => first_match thms
322           | SOME (_, t) => SOME (t, lazy_match thms));
323   in lazy_match end;
325 end;
328 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
330 local
332 val index_ord = option_ord (K EQUAL);
333 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
334 val qual_ord = int_ord o apply2 Long_Name.qualification;
335 val txt_ord = int_ord o apply2 size;
337 fun nicer_name (x, i) (y, j) =
338   (case hidden_ord (x, y) of EQUAL =>
339     (case index_ord (i, j) of EQUAL =>
340       (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
341     | ord => ord)
342   | ord => ord) <> GREATER;
344 fun rem_cdups nicer xs =
345   let
346     fun rem_c rev_seen [] = rev rev_seen
347       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
348       | rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) =
349           if Thm.eq_thm_prop (thm, thm')
350           then rem_c rev_seen ((if nicer n n' then x else y) :: rest)
351           else rem_c (x :: rev_seen) (y :: rest);
352   in rem_c [] xs end;
354 in
356 fun nicer_shortest ctxt =
357   let
358     fun extern_shortest name =
359       Name_Space.extern_shortest ctxt
360         (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
362     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
363           nicer_name (extern_shortest x, i) (extern_shortest y, j)
364       | nicer (Facts.Fact _) (Facts.Named _) = true
365       | nicer (Facts.Named _) (Facts.Fact _) = false
366       | nicer (Facts.Fact _) (Facts.Fact _) = true;
367   in nicer end;
369 fun rem_thm_dups nicer xs =
370   (xs ~~ (1 upto length xs))
371   |> sort (Term_Ord.fast_term_ord o apply2 (Thm.full_prop_of o #2 o #1))
372   |> rem_cdups nicer
373   |> sort (int_ord o apply2 #2)
374   |> map #1;
376 end;
380 (** main operations **)
382 (* filter_theorems *)
384 fun all_facts_of ctxt =
385   let
386     val local_facts = Proof_Context.facts_of ctxt;
387     val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
388   in
389     maps Facts.selections
390      (Facts.dest_static false [global_facts] local_facts @
391       Facts.dest_static false [] global_facts)
392   end;
394 fun filter_theorems ctxt theorems query =
395   let
396     val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
397     val filters = map (filter_criterion ctxt opt_goal) criteria;
399     fun find_all theorems =
400       let
401         val raw_matches = sorted_filter filters theorems;
403         val matches =
404           if rem_dups
405           then rem_thm_dups (nicer_shortest ctxt) raw_matches
406           else raw_matches;
408         val len = length matches;
409         val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
410       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
412     val find =
413       if rem_dups orelse is_none opt_limit
414       then find_all
415       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
417   in find theorems end;
419 fun filter_theorems_cmd ctxt theorems raw_query =
420   filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
423 (* find_theorems *)
425 local
427 fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
428   let
429     val assms =
430       Proof_Context.get_fact ctxt (Facts.named "local.assms")
431         handle ERROR _ => [];
432     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
433     val opt_goal' = Option.map add_prems opt_goal;
434   in
435     filter ctxt (all_facts_of ctxt)
436       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
437   end;
439 in
441 val find_theorems = gen_find_theorems filter_theorems;
442 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
444 end;
447 (* pretty_theorems *)
449 local
451 fun pretty_ref ctxt thmref =
452   let
453     val (name, sel) =
454       (case thmref of
455         Facts.Named ((name, _), sel) => (name, sel)
456       | Facts.Fact _ => raise Fail "Illegal literal fact");
457   in
458     [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
459       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
460   end;
462 in
464 fun pretty_thm ctxt (thmref, thm) =
465   Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
467 fun pretty_theorems state opt_limit rem_dups raw_criteria =
468   let
469     val ctxt = Proof.context_of state;
470     val opt_goal = try Proof.simple_goal state |> Option.map #goal;
471     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
473     val (opt_found, theorems) =
474       filter_theorems ctxt (all_facts_of ctxt)
475         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
476     val returned = length theorems;
478     val tally_msg =
479       (case opt_found of
480         NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
481       | SOME found =>
482           "found " ^ string_of_int found ^ " theorem(s)" ^
483             (if returned < found
484              then " (" ^ string_of_int returned ^ " displayed)"
485              else ""));
486     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
487   in
488     Pretty.block
489       (Pretty.fbreaks
490         (Pretty.mark position_markup (Pretty.keyword1 "find_theorems") ::
491           map (pretty_criterion ctxt) criteria)) ::
492     Pretty.str "" ::
493     (if null theorems then [Pretty.str "found nothing"]
494      else
495        Pretty.str (tally_msg ^ ":") ::
496        grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
497   end |> Pretty.fbreaks |> curry Pretty.blk 0;
499 end;
503 (** Isar command syntax **)
505 fun proof_state st =
506   (case try Toplevel.proof_of st of
507     SOME state => state
508   | NONE => Proof.init (Toplevel.context_of st));
510 local
512 val criterion =
513   Parse.reserved "name" |-- Parse.!!! (Parse.\$\$\$ ":" |-- Parse.xname) >> Name ||
514   Parse.reserved "intro" >> K Intro ||
515   Parse.reserved "elim" >> K Elim ||
516   Parse.reserved "dest" >> K Dest ||
517   Parse.reserved "solves" >> K Solves ||
518   Parse.reserved "simp" |-- Parse.!!! (Parse.\$\$\$ ":" |-- Parse.term) >> Simp ||
519   Parse.term >> Pattern;
521 val options =
522   Scan.optional
523     (Parse.\$\$\$ "(" |--
524       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
525         --| Parse.\$\$\$ ")")) (NONE, true);
527 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
529 val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
531 in
533 fun read_query pos str =
534   Outer_Syntax.scan query_keywords pos str
535   |> filter Token.is_proper
536   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
537   |> #1;
539 val _ =
540   Outer_Syntax.command @{command_spec "find_theorems"}
541     "find theorems meeting specified criteria"
542     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
543       Toplevel.keep (fn st =>
544         Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
546 end;
550 (** PIDE query operation **)
552 val _ =
553   Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
554     if can Toplevel.context_of st then
555       let
556         val [limit_arg, allow_dups_arg, query_arg] = args;
557         val state = proof_state st;
558         val opt_limit = Int.fromString limit_arg;
559         val rem_dups = allow_dups_arg = "false";
560         val criteria = read_query Position.none query_arg;
561       in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
562     else error "Unknown context");
564 end;