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