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