src/Pure/Tools/find_theorems.ML
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 53633 69f1221fc892
child 55669 4612c450b59c
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     1 (*  Title:      Pure/Tools/find_theorems.ML
     2     Author:     Rafal Kolanski and Gerwin Klein, NICTA
     3     Author:     Lars Noschinski and Alexander Krauss, TU Muenchen
     4 
     5 Retrieve theorems from proof context.
     6 *)
     7 
     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;
    25 
    26 structure Find_Theorems: FIND_THEOREMS =
    27 struct
    28 
    29 (** search criteria **)
    30 
    31 datatype 'term criterion =
    32   Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
    33 
    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;
    39 
    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;
    52 
    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);
    60 
    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;
    76 
    77 
    78 
    79 (** queries **)
    80 
    81 type 'term query = {
    82   goal: thm option,
    83   limit: int option,
    84   rem_dups: bool,
    85   criteria: (bool * 'term criterion) list
    86 };
    87 
    88 fun map_criteria f {goal, limit, rem_dups, criteria} =
    89   {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
    90 
    91 
    92 
    93 (** theorems, either internal or external (without proof) **)
    94 
    95 datatype theorem =
    96   Internal of Facts.ref * thm |
    97   External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
    98 
    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";
   104 
   105 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   106   | prop_of (External (_, prop)) = prop;
   107 
   108 fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
   109   | nprems_of (External (_, prop)) = Logic.count_prems prop;
   110 
   111 fun size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm)
   112   | size_of (External (_, prop)) = size_of_term prop;
   113 
   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));
   117 
   118 fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
   119   | fact_ref_of (External (fact_ref, _)) = fact_ref;
   120 
   121 
   122 
   123 (** search criterion filters **)
   124 
   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 *)
   138 
   139 
   140 (* matching theorems *)
   141 
   142 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
   143 
   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;
   151 
   152     fun matches pat =
   153       is_nontrivial thy pat andalso
   154       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   155 
   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;
   160 
   161     fun best_match [] = NONE
   162       | best_match xs = SOME (foldl1 Int.min xs);
   163 
   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;
   169 
   170 
   171 (* filter_name *)
   172 
   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;
   176 
   177 
   178 (* filter intro/elim/dest/solves rules *)
   179 
   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;
   186 
   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;
   196 
   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;
   205 
   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;
   227 
   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;
   235 
   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
   241         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
   242           1 goal';
   243   in
   244     fn Internal (_, thm) =>
   245         if is_some (Seq.pull (try_thm thm))
   246         then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE
   247      | External _ => NONE
   248   end;
   249 
   250 
   251 (* filter_simp *)
   252 
   253 fun filter_simp ctxt t (Internal (_, thm)) =
   254       let
   255         val mksimps = Simplifier.mksimps ctxt;
   256         val extract_simp =
   257           (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   258         val ss = is_matching_thm extract_simp ctxt false t thm;
   259       in
   260         if is_some ss
   261         then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss)
   262         else NONE
   263       end
   264   | filter_simp _ _ (External _) = NONE;
   265 
   266 
   267 (* filter_pattern *)
   268 
   269 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
   270 
   271 (*Including all constants and frees is only sound because matching
   272   uses higher-order patterns. If full matching were used, then
   273   constants that may be subject to beta-reduction after substitution
   274   of frees should not be included for LHS set because they could be
   275   thrown away by the substituted function.  E.g. for (?F 1 2) do not
   276   include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
   277   largest possible set should always be included on the RHS.*)
   278 
   279 fun filter_pattern ctxt pat =
   280   let
   281     val pat_consts = get_names pat;
   282 
   283     fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
   284       | check (theorem, c as SOME thm_consts) =
   285          (if subset (op =) (pat_consts, thm_consts) andalso
   286             Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
   287           then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c);
   288   in check end;
   289 
   290 
   291 (* interpret criteria as filters *)
   292 
   293 local
   294 
   295 fun err_no_goal c =
   296   error ("Current goal required for " ^ c ^ " search criterion");
   297 
   298 fun filter_crit _ _ (Name name) = apfst (filter_name name)
   299   | filter_crit _ NONE Intro = err_no_goal "intro"
   300   | filter_crit _ NONE Elim = err_no_goal "elim"
   301   | filter_crit _ NONE Dest = err_no_goal "dest"
   302   | filter_crit _ NONE Solves = err_no_goal "solves"
   303   | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
   304   | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
   305   | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
   306   | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
   307   | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
   308   | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
   309 
   310 fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
   311 
   312 fun opt_add (SOME (a, c, x)) (SOME (b, d, y)) = SOME (Int.max (a,b), Int.max (c, d), x + y : int)
   313   | opt_add _ _ = NONE;
   314 
   315 fun app_filters thm =
   316   let
   317     fun app (NONE, _, _) = NONE
   318       | app (SOME v, _, []) = SOME (v, thm)
   319       | app (r, consts, f :: fs) =
   320           let val (r', consts') = f (thm, consts)
   321           in app (opt_add r r', consts', fs) end;
   322   in app end;
   323 
   324 in
   325 
   326 fun filter_criterion ctxt opt_goal (b, c) =
   327   (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
   328 
   329 fun sorted_filter filters theorems =
   330   let
   331     fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
   332 
   333     (*filters return: (thm size, number of assumptions, substitution size) option, so
   334       sort according to size of thm first, then number of assumptions,
   335       then by the substitution size, then by term order *)
   336     fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) =
   337       prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord)) 
   338          ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0))));
   339   in
   340     grouped 100 Par_List.map eval_filters theorems
   341     |> map_filter I |> sort result_ord |> map #2
   342   end;
   343 
   344 fun lazy_filter filters =
   345   let
   346     fun lazy_match thms = Seq.make (fn () => first_match thms)
   347     and first_match [] = NONE
   348       | first_match (thm :: thms) =
   349           (case app_filters thm (SOME (0, 0, 0), NONE, filters) of
   350             NONE => first_match thms
   351           | SOME (_, t) => SOME (t, lazy_match thms));
   352   in lazy_match end;
   353 
   354 end;
   355 
   356 
   357 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
   358 
   359 local
   360 
   361 val index_ord = option_ord (K EQUAL);
   362 val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
   363 val qual_ord = int_ord o pairself (length o Long_Name.explode);
   364 val txt_ord = int_ord o pairself size;
   365 
   366 fun nicer_name (x, i) (y, j) =
   367   (case hidden_ord (x, y) of EQUAL =>
   368     (case index_ord (i, j) of EQUAL =>
   369       (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
   370     | ord => ord)
   371   | ord => ord) <> GREATER;
   372 
   373 fun rem_cdups nicer xs =
   374   let
   375     fun rem_c rev_seen [] = rev rev_seen
   376       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
   377       | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
   378           if (prop_of t) aconv (prop_of t')
   379           then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
   380           else rem_c (x :: rev_seen) (y :: xs)
   381   in rem_c [] xs end;
   382 
   383 in
   384 
   385 fun nicer_shortest ctxt =
   386   let
   387     val space = Facts.space_of (Proof_Context.facts_of ctxt);
   388 
   389     val shorten =
   390       Name_Space.extern
   391         (ctxt
   392           |> Config.put Name_Space.names_long false
   393           |> Config.put Name_Space.names_short false
   394           |> Config.put Name_Space.names_unique false) space;
   395 
   396     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   397           nicer_name (shorten x, i) (shorten y, j)
   398       | nicer (Facts.Fact _) (Facts.Named _) = true
   399       | nicer (Facts.Named _) (Facts.Fact _) = false;
   400   in nicer end;
   401 
   402 fun rem_thm_dups nicer xs =
   403   (xs ~~ (1 upto length xs))
   404   |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
   405   |> rem_cdups nicer
   406   |> sort (int_ord o pairself #2)
   407   |> map #1;
   408 
   409 end;
   410 
   411 
   412 
   413 (** main operations **)
   414 
   415 (* filter_theorems *)
   416 
   417 fun all_facts_of ctxt =
   418   let
   419     fun visible_facts facts =
   420       Facts.dest_static [] facts
   421       |> filter_out (Facts.is_concealed facts o #1);
   422   in
   423     maps Facts.selections
   424      (visible_facts (Proof_Context.facts_of ctxt) @
   425       visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
   426   end;
   427 
   428 fun filter_theorems ctxt theorems query =
   429   let
   430     val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
   431     val filters = map (filter_criterion ctxt opt_goal) criteria;
   432 
   433     fun find_all theorems =
   434       let
   435         val raw_matches = sorted_filter filters theorems;
   436 
   437         val matches =
   438           if rem_dups
   439           then rem_thm_dups (nicer_shortest ctxt) raw_matches
   440           else raw_matches;
   441 
   442         val len = length matches;
   443         val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
   444       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
   445 
   446     val find =
   447       if rem_dups orelse is_none opt_limit
   448       then find_all
   449       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
   450 
   451   in find theorems end;
   452 
   453 fun filter_theorems_cmd ctxt theorems raw_query =
   454   filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
   455 
   456 
   457 (* find_theorems *)
   458 
   459 local
   460 
   461 fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
   462   let
   463     val assms =
   464       Proof_Context.get_fact ctxt (Facts.named "local.assms")
   465         handle ERROR _ => [];
   466     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
   467     val opt_goal' = Option.map add_prems opt_goal;
   468   in
   469     filter ctxt (map Internal (all_facts_of ctxt))
   470       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
   471     |> apsnd (map (fn Internal f => f))
   472   end;
   473 
   474 in
   475 
   476 val find_theorems = gen_find_theorems filter_theorems;
   477 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
   478 
   479 end;
   480 
   481 
   482 (* pretty_theorems *)
   483 
   484 local
   485 
   486 fun pretty_ref ctxt thmref =
   487   let
   488     val (name, sel) =
   489       (case thmref of
   490         Facts.Named ((name, _), sel) => (name, sel)
   491       | Facts.Fact _ => raise Fail "Illegal literal fact");
   492   in
   493     [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
   494       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   495   end;
   496 
   497 fun pretty_theorem ctxt (Internal (thmref, thm)) =
   498       Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
   499   | pretty_theorem ctxt (External (thmref, prop)) =
   500       Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
   501 
   502 in
   503 
   504 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
   505 
   506 fun pretty_theorems state opt_limit rem_dups raw_criteria =
   507   let
   508     val ctxt = Proof.context_of state;
   509     val opt_goal = try Proof.simple_goal state |> Option.map #goal;
   510     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   511 
   512     val (opt_found, theorems) =
   513       filter_theorems ctxt (map Internal (all_facts_of ctxt))
   514         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
   515     val returned = length theorems;
   516 
   517     val tally_msg =
   518       (case opt_found of
   519         NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
   520       | SOME found =>
   521           "found " ^ string_of_int found ^ " theorem(s)" ^
   522             (if returned < found
   523              then " (" ^ string_of_int returned ^ " displayed)"
   524              else ""));
   525   in
   526     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
   527     Pretty.str "" ::
   528     (if null theorems then [Pretty.str "nothing found"]
   529      else
   530       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
   531         grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) (rev theorems))
   532   end |> Pretty.fbreaks |> curry Pretty.blk 0;
   533 
   534 end;
   535 
   536 
   537 
   538 (** Isar command syntax **)
   539 
   540 fun proof_state st =
   541   (case try Toplevel.proof_of st of
   542     SOME state => state
   543   | NONE => Proof.init (Toplevel.context_of st));
   544 
   545 local
   546 
   547 val criterion =
   548   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   549   Parse.reserved "intro" >> K Intro ||
   550   Parse.reserved "elim" >> K Elim ||
   551   Parse.reserved "dest" >> K Dest ||
   552   Parse.reserved "solves" >> K Solves ||
   553   Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
   554   Parse.term >> Pattern;
   555 
   556 val options =
   557   Scan.optional
   558     (Parse.$$$ "(" |--
   559       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
   560         --| Parse.$$$ ")")) (NONE, true);
   561 
   562 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   563 
   564 in
   565 
   566 fun read_query pos str =
   567   Outer_Syntax.scan pos str
   568   |> filter Token.is_proper
   569   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   570   |> #1;
   571 
   572 val _ =
   573   Outer_Syntax.improper_command @{command_spec "find_theorems"}
   574     "find theorems meeting specified criteria"
   575     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   576       Toplevel.keep (fn st =>
   577         Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
   578 
   579 end;
   580 
   581 
   582 
   583 (** PIDE query operation **)
   584 
   585 val _ =
   586   Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
   587     if can Toplevel.context_of st then
   588       let
   589         val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
   590         val state =
   591           if context_arg = "" then proof_state st
   592           else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
   593         val opt_limit = Int.fromString limit_arg;
   594         val rem_dups = allow_dups_arg = "false";
   595         val criteria = read_query Position.none query_arg;
   596       in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
   597     else error "Unknown context");
   598 
   599 end;