src/Pure/Tools/find_theorems.ML
 author kleing Sat Sep 14 20:57:22 2013 +1000 (2013-09-14) changeset 53633 69f1221fc892 parent 53632 96808429b9ec child 54742 7a86358a3c0b permissions -rw-r--r--
print find_thms result in reverse order so best result is on top
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};
93 (** theorems, either internal or external (without proof) **)
95 datatype theorem =
96   Internal of Facts.ref * thm |
97   External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
99 fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) =
100       Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
101   | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
102       Position.markup pos o Markup.properties [("name", name)]
103   | fact_ref_markup fact_ref = raise Fail "bad fact ref";
105 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
106   | prop_of (External (_, prop)) = prop;
108 fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
109   | nprems_of (External (_, prop)) = Logic.count_prems prop;
111 fun size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm)
112   | size_of (External (_, prop)) = size_of_term prop;
114 fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm
115   | major_prem_of (External (_, prop)) =
116       Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop));
118 fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
119   | fact_ref_of (External (fact_ref, _)) = fact_ref;
123 (** search criterion filters **)
125 (*generated filters are to be of the form
126   input: theorem
127   output: (p:int, s:int, t:int) option, where
128     NONE indicates no match
129     p is the primary sorting criterion
130       (eg. size of term)
131     s is the secondary sorting criterion
132       (eg. number of assumptions in the theorem)
133     t is the tertiary sorting criterion
134       (eg. size of the substitution for intro, elim and dest)
135   when applying a set of filters to a thm, fold results in:
136     (max p, max s, sum of all t)
137 *)
140 (* matching theorems *)
142 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
144 (*extract terms from term_src, refine them to the parts that concern us,
145   if po try match them against obj else vice versa.
146   trivial matches are ignored.
147   returns: smallest substitution size*)
148 fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
149   let
150     val thy = Proof_Context.theory_of ctxt;
152     fun matches pat =
153       is_nontrivial thy pat andalso
154       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
156     fun subst_size pat =
157       let val (_, subst) =
158         Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
159       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
161     fun best_match [] = NONE
162       | best_match xs = SOME (foldl1 Int.min xs);
164     val match_thm = matches o refine_term;
165   in
166     map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
167     |> best_match
168   end;
171 (* filter_name *)
173 fun filter_name str_pat theorem =
174   if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
175   then SOME (0, 0, 0) else NONE;
178 (* filter intro/elim/dest/solves rules *)
180 fun filter_dest ctxt goal theorem =
181   let
182     val extract_dest =
183      (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem],
184       hd o Logic.strip_imp_prems);
185     val prems = Logic.prems_of_goal goal 1;
187     fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
188     val successful = prems |> map_filter try_subst;
189   in
190     (*if possible, keep best substitution (one with smallest size)*)
191     (*dest rules always have assumptions, so a dest with one
192       assumption is as good as an intro rule with none*)
193     if not (null successful)
194     then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
195   end;
197 fun filter_intro ctxt goal theorem =
198   let
199     val extract_intro = (single o prop_of, Logic.strip_imp_concl);
200     val concl = Logic.concl_of_goal goal 1;
201     val ss = is_matching_thm extract_intro ctxt true concl theorem;
202   in
203     if is_some ss then SOME (size_of theorem, nprems_of theorem, the ss) else NONE
204   end;
206 fun filter_elim ctxt goal theorem =
207   if nprems_of theorem > 0 then
208     let
209       val rule = prop_of theorem;
210       val prems = Logic.prems_of_goal goal 1;
211       val goal_concl = Logic.concl_of_goal goal 1;
212       val rule_mp = hd (Logic.strip_imp_prems rule);
213       val rule_concl = Logic.strip_imp_concl rule;
214       fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) \$ (t1 \$ t2);  (* FIXME ?? *)
215       val rule_tree = combine rule_mp rule_concl;
216       fun goal_tree prem = combine prem goal_concl;
217       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
218       val successful = prems |> map_filter try_subst;
219     in
220       (*elim rules always have assumptions, so an elim with one
221         assumption is as good as an intro rule with none*)
222       if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
223         andalso not (null successful)
224       then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
225     end
226   else NONE;
228 fun filter_solves ctxt goal =
229   let
230     val thy' =
231       Proof_Context.theory_of ctxt
232       |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
233     val ctxt' = Proof_Context.transfer thy' ctxt;
234     val goal' = Thm.transfer thy' goal;
236     fun limited_etac thm i =
237       Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
238     fun try_thm thm =
239       if Thm.no_prems thm then rtac thm 1 goal'
240       else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
241   in
242     fn Internal (_, thm) =>
243         if is_some (Seq.pull (try_thm thm))
244         then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE
245      | External _ => NONE
246   end;
249 (* filter_simp *)
251 fun filter_simp ctxt t (Internal (_, thm)) =
252       let
253         val mksimps = Simplifier.mksimps ctxt;
254         val extract_simp =
255           (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
256         val ss = is_matching_thm extract_simp ctxt false t thm;
257       in
258         if is_some ss
259         then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss)
260         else NONE
261       end
262   | filter_simp _ _ (External _) = NONE;
265 (* filter_pattern *)
267 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
269 (*Including all constants and frees is only sound because matching
270   uses higher-order patterns. If full matching were used, then
271   constants that may be subject to beta-reduction after substitution
272   of frees should not be included for LHS set because they could be
273   thrown away by the substituted function.  E.g. for (?F 1 2) do not
274   include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
275   largest possible set should always be included on the RHS.*)
277 fun filter_pattern ctxt pat =
278   let
279     val pat_consts = get_names pat;
281     fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
282       | check (theorem, c as SOME thm_consts) =
283          (if subset (op =) (pat_consts, thm_consts) andalso
284             Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
285           then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c);
286   in check end;
289 (* interpret criteria as filters *)
291 local
293 fun err_no_goal c =
294   error ("Current goal required for " ^ c ^ " search criterion");
296 fun filter_crit _ _ (Name name) = apfst (filter_name name)
297   | filter_crit _ NONE Intro = err_no_goal "intro"
298   | filter_crit _ NONE Elim = err_no_goal "elim"
299   | filter_crit _ NONE Dest = err_no_goal "dest"
300   | filter_crit _ NONE Solves = err_no_goal "solves"
301   | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
302   | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
303   | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
304   | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
305   | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
306   | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
308 fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
310 fun opt_add (SOME (a, c, x)) (SOME (b, d, y)) = SOME (Int.max (a,b), Int.max (c, d), x + y : int)
311   | opt_add _ _ = NONE;
313 fun app_filters thm =
314   let
315     fun app (NONE, _, _) = NONE
316       | app (SOME v, _, []) = SOME (v, thm)
317       | app (r, consts, f :: fs) =
318           let val (r', consts') = f (thm, consts)
319           in app (opt_add r r', consts', fs) end;
320   in app end;
322 in
324 fun filter_criterion ctxt opt_goal (b, c) =
325   (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
327 fun sorted_filter filters theorems =
328   let
329     fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
331     (*filters return: (thm size, number of assumptions, substitution size) option, so
332       sort according to size of thm first, then number of assumptions,
333       then by the substitution size, then by term order *)
334     fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) =
335       prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
336          ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0))));
337   in
338     grouped 100 Par_List.map eval_filters theorems
339     |> map_filter I |> sort result_ord |> map #2
340   end;
342 fun lazy_filter filters =
343   let
344     fun lazy_match thms = Seq.make (fn () => first_match thms)
345     and first_match [] = NONE
346       | first_match (thm :: thms) =
347           (case app_filters thm (SOME (0, 0, 0), NONE, filters) of
348             NONE => first_match thms
349           | SOME (_, t) => SOME (t, lazy_match thms));
350   in lazy_match end;
352 end;
355 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
357 local
359 val index_ord = option_ord (K EQUAL);
360 val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
361 val qual_ord = int_ord o pairself (length o Long_Name.explode);
362 val txt_ord = int_ord o pairself size;
364 fun nicer_name (x, i) (y, j) =
365   (case hidden_ord (x, y) of EQUAL =>
366     (case index_ord (i, j) of EQUAL =>
367       (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
368     | ord => ord)
369   | ord => ord) <> GREATER;
371 fun rem_cdups nicer xs =
372   let
373     fun rem_c rev_seen [] = rev rev_seen
374       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
375       | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
376           if (prop_of t) aconv (prop_of t')
377           then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
378           else rem_c (x :: rev_seen) (y :: xs)
379   in rem_c [] xs end;
381 in
383 fun nicer_shortest ctxt =
384   let
385     val space = Facts.space_of (Proof_Context.facts_of ctxt);
387     val shorten =
388       Name_Space.extern
389         (ctxt
390           |> Config.put Name_Space.names_long false
391           |> Config.put Name_Space.names_short false
392           |> Config.put Name_Space.names_unique false) space;
394     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
395           nicer_name (shorten x, i) (shorten y, j)
396       | nicer (Facts.Fact _) (Facts.Named _) = true
397       | nicer (Facts.Named _) (Facts.Fact _) = false;
398   in nicer end;
400 fun rem_thm_dups nicer xs =
401   (xs ~~ (1 upto length xs))
402   |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
403   |> rem_cdups nicer
404   |> sort (int_ord o pairself #2)
405   |> map #1;
407 end;
411 (** main operations **)
413 (* filter_theorems *)
415 fun all_facts_of ctxt =
416   let
417     fun visible_facts facts =
418       Facts.dest_static [] facts
419       |> filter_out (Facts.is_concealed facts o #1);
420   in
421     maps Facts.selections
422      (visible_facts (Proof_Context.facts_of ctxt) @
423       visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
424   end;
426 fun filter_theorems ctxt theorems query =
427   let
428     val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
429     val filters = map (filter_criterion ctxt opt_goal) criteria;
431     fun find_all theorems =
432       let
433         val raw_matches = sorted_filter filters theorems;
435         val matches =
436           if rem_dups
437           then rem_thm_dups (nicer_shortest ctxt) raw_matches
438           else raw_matches;
440         val len = length matches;
441         val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
442       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
444     val find =
445       if rem_dups orelse is_none opt_limit
446       then find_all
447       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
449   in find theorems end;
451 fun filter_theorems_cmd ctxt theorems raw_query =
452   filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
455 (* find_theorems *)
457 local
459 fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
460   let
461     val assms =
462       Proof_Context.get_fact ctxt (Facts.named "local.assms")
463         handle ERROR _ => [];
464     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
465     val opt_goal' = Option.map add_prems opt_goal;
466   in
467     filter ctxt (map Internal (all_facts_of ctxt))
468       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
469     |> apsnd (map (fn Internal f => f))
470   end;
472 in
474 val find_theorems = gen_find_theorems filter_theorems;
475 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
477 end;
480 (* pretty_theorems *)
482 local
484 fun pretty_ref ctxt thmref =
485   let
486     val (name, sel) =
487       (case thmref of
488         Facts.Named ((name, _), sel) => (name, sel)
489       | Facts.Fact _ => raise Fail "Illegal literal fact");
490   in
491     [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
492       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
493   end;
495 fun pretty_theorem ctxt (Internal (thmref, thm)) =
496       Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
497   | pretty_theorem ctxt (External (thmref, prop)) =
498       Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
500 in
502 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
504 fun pretty_theorems state opt_limit rem_dups raw_criteria =
505   let
506     val ctxt = Proof.context_of state;
507     val opt_goal = try Proof.simple_goal state |> Option.map #goal;
508     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
510     val (opt_found, theorems) =
511       filter_theorems ctxt (map Internal (all_facts_of ctxt))
512         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
513     val returned = length theorems;
515     val tally_msg =
516       (case opt_found of
517         NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
518       | SOME found =>
519           "found " ^ string_of_int found ^ " theorem(s)" ^
520             (if returned < found
521              then " (" ^ string_of_int returned ^ " displayed)"
522              else ""));
523   in
524     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
525     Pretty.str "" ::
526     (if null theorems then [Pretty.str "nothing found"]
527      else
528       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
529         grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) (rev theorems))
530   end |> Pretty.fbreaks |> curry Pretty.blk 0;
532 end;
536 (** Isar command syntax **)
538 fun proof_state st =
539   (case try Toplevel.proof_of st of
540     SOME state => state
541   | NONE => Proof.init (Toplevel.context_of st));
543 local
545 val criterion =
546   Parse.reserved "name" |-- Parse.!!! (Parse.\$\$\$ ":" |-- Parse.xname) >> Name ||
547   Parse.reserved "intro" >> K Intro ||
548   Parse.reserved "elim" >> K Elim ||
549   Parse.reserved "dest" >> K Dest ||
550   Parse.reserved "solves" >> K Solves ||
551   Parse.reserved "simp" |-- Parse.!!! (Parse.\$\$\$ ":" |-- Parse.term) >> Simp ||
552   Parse.term >> Pattern;
554 val options =
555   Scan.optional
556     (Parse.\$\$\$ "(" |--
557       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
558         --| Parse.\$\$\$ ")")) (NONE, true);
560 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
562 in
564 fun read_query pos str =
565   Outer_Syntax.scan pos str
566   |> filter Token.is_proper
567   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
568   |> #1;
570 val _ =
571   Outer_Syntax.improper_command @{command_spec "find_theorems"}
572     "find theorems meeting specified criteria"
573     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
574       Toplevel.keep (fn st =>
575         Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
577 end;
581 (** PIDE query operation **)
583 val _ =
584   Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
585     if can Toplevel.context_of st then
586       let
587         val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
588         val state =
589           if context_arg = "" then proof_state st
590           else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
591         val opt_limit = Int.fromString limit_arg;
592         val rem_dups = allow_dups_arg = "false";
593         val criteria = read_query Position.none query_arg;
594       in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
595     else error "Unknown context");
597 end;