1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Select 8imports Separation_Algebra 9begin 10 11ML_file "sep_tactics.ML" 12 13ML\<open> 14 structure SepSelect_Rules = Named_Thms ( 15 val name = @{binding "sep_select"} 16 val description = "sep_select rules" 17 ) 18\<close> 19setup SepSelect_Rules.setup 20 21ML \<open> 22 structure SepSelectAsm_Rules = Named_Thms ( 23 val name = @{binding "sep_select_asm"} 24 val description = "sep_select_asm rules" 25 ) 26\<close> 27setup SepSelectAsm_Rules.setup 28 29ML \<open> 30 fun sep_selects_tactic ns ctxt = 31 sep_select_tactic (resolve_tac ctxt (SepSelect_Rules.get ctxt)) ns ctxt 32 33 fun sep_select_asms_tactic ns ctxt = 34 sep_select_tactic (dresolve_tac ctxt (SepSelectAsm_Rules.get ctxt)) ns ctxt 35\<close> 36 37method_setup sep_select_asm = \<open> 38 Scan.lift (Scan.repeat Parse.int) >> 39 (fn ns => fn ctxt => SIMPLE_METHOD' (sep_select_asms_tactic ns ctxt)) 40\<close> "Reorder assumptions" 41 42method_setup sep_select = \<open> 43 Scan.lift (Scan.repeat Parse.int) >> 44 (fn ns => fn ctxt => SIMPLE_METHOD' (sep_selects_tactic ns ctxt)) 45\<close> "Reorder conclusions" 46 47lemma sep_eq [sep_select]: "(\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> T s \<Longrightarrow> (P \<and>* R) s" by clarsimp 48lemma sep_asm_eq [sep_select_asm]: "(P \<and>* R) s \<Longrightarrow> (\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> T s" by clarsimp 49 50ML \<open> 51 (* export method form of these two for use outisde this entry *) 52 53 fun sep_select_method lens ns ctxt = 54 SIMPLE_METHOD' (sep_select_tactic lens ns ctxt) 55 56 fun sep_select_generic_method asm thms ns ctxt = 57 sep_select_method (if asm then dresolve_tac ctxt thms else resolve_tac ctxt thms) ns ctxt 58\<close> 59 60method_setup sep_select_gen = \<open> 61 Attrib.thms --| Scan.lift Args.colon -- Scan.lift (Scan.repeat Parse.int) -- Scan.lift (Args.mode "asm") >> 62 (fn ((lens, ns), asm) => sep_select_generic_method asm lens ns) 63\<close> 64 65end 66