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