1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Solve
8imports Sep_Cancel Sep_MP
9begin
10
11ML \<open>
12  fun sep_schem ctxt =
13    rotator' ctxt (sep_asm_erule_select ctxt)
14            (SOLVED' ((eresolve0_tac [@{thm sep_conj_sep_impl2}] THEN'
15                      (FIRST' [assume_tac ctxt, resolve0_tac [@{thm TrueI}], sep_cancel_tactic' ctxt true]
16                       |> REPEAT_ALL_NEW))))
17
18  fun sep_solve_tactic ctxt  =
19  let
20    val truei = resolve0_tac [@{thm TrueI}]
21    fun sep_cancel_rotating i =
22      sep_select_tactic (sep_asm_select ctxt) [1] ctxt i THEN_ELSE
23      (rotator' ctxt (sep_asm_select ctxt)
24         (FIRST' [assume_tac ctxt, truei, sep_cancel_tactic' ctxt false, eresolve0_tac [@{thm sep_conj_sep_impl}]]
25          |> REPEAT_ALL_NEW |> SOLVED') i,
26       SOLVED' (FIRST' [assume_tac ctxt, truei, sep_cancel_tactic' ctxt false, eresolve0_tac [@{thm sep_conj_sep_impl}]]
27          |> REPEAT_ALL_NEW) i)
28    val sep_cancel_tac =
29      FIRST' [assume_tac ctxt, truei, sep_cancel_tactic' ctxt false, eresolve0_tac [@{thm sep_conj_sep_impl}]]
30      |> REPEAT_ALL_NEW
31  in
32    (DETERM o SOLVED' (FIRST' [assume_tac ctxt,truei, sep_cancel_tac])) ORELSE'
33    (SOLVED' ((TRY o CHANGED_PROP o sep_mp_solver ctxt) THEN_ALL_NEW sep_cancel_rotating))
34    |> SOLVED'
35  end
36
37  fun sep_solve_method _ ctxt = SIMPLE_METHOD' (sep_solve_tactic ctxt)
38  fun sep_schem_method _ ctxt = SIMPLE_METHOD' (sep_schem ctxt)
39\<close>
40
41method_setup sep_solve = \<open>sep_cancel_syntax >> sep_solve_method\<close>
42method_setup sep_schem = \<open>sep_cancel_syntax >> sep_schem_method\<close>
43
44end
45