1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Util
8imports
9  Sep_Algebra_L4v
10  "HOL-Eisbach.Eisbach"
11begin
12
13(* The sep_simp, sep_flatten, and sep_map tactics. *)
14
15ML \<open>
16fun all_rotator lens tactic ctxt i st =
17  let
18    val len = case Seq.pull ((lens THEN' resolve0_tac [@{thm iffI}]) i st) of
19                NONE => 0
20              | SOME (thm, _) => conj_length ctxt (Thm.cprem_of thm i)
21    val nums = range 1 len
22    val selector = sep_select_tactic lens
23    val tac' = map (fn x => selector [x] ctxt THEN' tactic) nums
24    val every = fold (fn x => fn y => x THEN_ALL_NEW TRY o y) tac' (K all_tac)
25  in
26    (selector [1] ctxt THEN' every THEN' (TRY o selector (rev nums) ctxt)) i st
27  end
28
29fun sep_all tac ctxt =
30  let fun r lens tactic = rotator lens tactic ctxt
31  in
32    (TRY o sep_flatten ctxt) THEN' (tac |> r (sep_asm_select ctxt))
33  end
34
35fun sep_simp thms ctxt =
36   let val ctxt' = ctxt addsimps thms
37       val clarsimp' = CHANGED_PROP o clarsimp_tac ctxt'
38 in REPEAT_ALL_NEW (sep_all clarsimp' ctxt)
39end
40
41fun sep_simp_method (thms : thm list) ctxt = SIMPLE_METHOD' (sep_simp thms ctxt)
42\<close>
43
44method_setup sep_flatten = \<open>
45  Scan.succeed (SIMPLE_METHOD' o sep_flatten)
46\<close>
47
48(* sep_flatten is a tactic to apply the associativity rule for separating conjunction,
49   and nothing else. *)
50
51method_setup sep_simp = \<open>
52 Attrib.thms >> sep_simp_method
53\<close>
54
55(* sep_simp repeatedly applies clarsimp, rotating the premises in-between invocations,
56   until it cannot apply. *)
57
58method sep_map uses thms = ((sep_drule thms, sep_flatten?)+)[1]
59
60(* sep_map attempts to apply a rule destructively to each conjunct that matches. *)
61
62end