1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Solves_Tac 8imports 9 "Main" 10begin 11 12ML \<open> 13 14val ETAC_LIMIT = 5; 15 16(* Solve the tactic by applying the given rule, then unifying assumptions. *) 17fun solve_tac ctxt thm i goal = 18let 19 (* Use "etac", but give up if there are countless unifications that 20 * don't end up working. *) 21 fun limited_etac thm i = 22 Seq.take ETAC_LIMIT o eresolve_tac ctxt [thm] i 23in 24 if Thm.no_prems thm then 25 SOLVED' (resolve_tac ctxt [thm]) i goal 26 else 27 SOLVED' ( 28 limited_etac thm 29 THEN_ALL_NEW ( 30 Goal.norm_hhf_tac ctxt THEN' Method.assm_tac ctxt)) i goal 31end 32 33(* 34 * Return all thms available in the context. 35 * 36 * Clagged from "find_theorems" 37 *) 38fun all_facts_of ctxt = 39let 40 val local_facts = Proof_Context.facts_of ctxt; 41 val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); 42in 43 maps Facts.selections 44 (Facts.dest_static false [global_facts] local_facts @ 45 Facts.dest_static false [] global_facts) 46 |> map snd 47end 48 49(* Try blindly applying every previously proven rule. *) 50fun solves_tac ctxt = 51let 52 val assms = 53 Proof_Context.get_fact ctxt (Facts.named "local.assms") 54 handle ERROR _ => []; 55 fun add_prems i = TRY (Method.insert_tac ctxt assms i); 56 val all_facts = all_facts_of ctxt 57 val solve_tacs = map (fn thm => solve_tac ctxt thm 1) all_facts 58in 59 (add_prems THEN' assume_tac ctxt) 60 ORELSE' 61 SOLVED' (Subgoal.FOCUS_PARAMS (K (add_prems 1 THEN FIRST solve_tacs)) ctxt) 62end 63 64\<close> 65 66method_setup solves = " 67 Scan.succeed (SIMPLE_METHOD' o solves_tac) 68" "find a previously proven fact that solves the goal" 69 70 71lemma "(A = B) = (B = A)" 72 apply solves 73 oops 74 75lemma "\<lbrakk> A \<Longrightarrow> B ; B \<Longrightarrow> A \<rbrakk> \<Longrightarrow> A = B" 76 apply solves 77 oops 78 79end 80