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
     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 (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;
   247 
   248 
   249 (* filter_simp *)
   250 
   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;
   263 
   264 
   265 (* filter_pattern *)
   266 
   267 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
   268 
   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.*)
   276 
   277 fun filter_pattern ctxt pat =
   278   let
   279     val pat_consts = get_names pat;
   280 
   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;
   287 
   288 
   289 (* interpret criteria as filters *)
   290 
   291 local
   292 
   293 fun err_no_goal c =
   294   error ("Current goal required for " ^ c ^ " search criterion");
   295 
   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;
   307 
   308 fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
   309 
   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;
   312 
   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;
   321 
   322 in
   323 
   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;
   326 
   327 fun sorted_filter filters theorems =
   328   let
   329     fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
   330 
   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;
   341 
   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;
   351 
   352 end;
   353 
   354 
   355 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
   356 
   357 local
   358 
   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;
   363 
   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;
   370 
   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;
   380 
   381 in
   382 
   383 fun nicer_shortest ctxt =
   384   let
   385     val space = Facts.space_of (Proof_Context.facts_of ctxt);
   386 
   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;
   393 
   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;
   399 
   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;
   406 
   407 end;
   408 
   409 
   410 
   411 (** main operations **)
   412 
   413 (* filter_theorems *)
   414 
   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;
   425 
   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;
   430 
   431     fun find_all theorems =
   432       let
   433         val raw_matches = sorted_filter filters theorems;
   434 
   435         val matches =
   436           if rem_dups
   437           then rem_thm_dups (nicer_shortest ctxt) raw_matches
   438           else raw_matches;
   439 
   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;
   443 
   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;
   448 
   449   in find theorems end;
   450 
   451 fun filter_theorems_cmd ctxt theorems raw_query =
   452   filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
   453 
   454 
   455 (* find_theorems *)
   456 
   457 local
   458 
   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;
   471 
   472 in
   473 
   474 val find_theorems = gen_find_theorems filter_theorems;
   475 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
   476 
   477 end;
   478 
   479 
   480 (* pretty_theorems *)
   481 
   482 local
   483 
   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;
   494 
   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]);
   499 
   500 in
   501 
   502 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
   503 
   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;
   509 
   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;
   514 
   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;
   531 
   532 end;
   533 
   534 
   535 
   536 (** Isar command syntax **)
   537 
   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));
   542 
   543 local
   544 
   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;
   553 
   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);
   559 
   560 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   561 
   562 in
   563 
   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;
   569 
   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))));
   576 
   577 end;
   578 
   579 
   580 
   581 (** PIDE query operation **)
   582 
   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");
   596 
   597 end;