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