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