1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Provers
8imports Sep_Rotate
9begin
10
11(* Constrained lens for sep_erule tactic *)
12lemma sep_asm_eq_erule:
13  "(P \<and>* R) s \<Longrightarrow> (\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> (T s \<Longrightarrow> (P' \<and>* R') s) \<Longrightarrow> (P' \<and>* R') s"
14  by (clarsimp)
15
16lemma sep_rule:
17  "(\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (T \<and>* R) s \<Longrightarrow> (P \<and>* R) s"
18  by (rule sep_conj_impl1)
19
20lemma sep_erule:
21  "(T \<and>* R') s  \<Longrightarrow> (\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (\<And>s. R' s \<Longrightarrow> R s) \<Longrightarrow>  (P \<and>* R) s"
22  by (rule sep_conj_impl)
23
24(* Construct analogues to rule/drule etc,  for separation logic *)
25
26ML \<open>
27fun sep_select ctxt = resolve_tac ctxt [@{thm sep_eq}]
28fun sep_asm_select ctxt = dresolve_tac ctxt [@{thm sep_asm_eq}]
29fun sep_asm_erule_select ctxt = eresolve_tac ctxt [@{thm sep_asm_eq_erule}]
30
31fun sep_rule_tactic ctxt thms =
32  let val sep_rule = resolve_tac ctxt [@{thm sep_rule}]
33  in sep_apply_tactic ctxt sep_rule thms end
34
35fun sep_drule_tactic ctxt thms =
36  let val sep_drule = dresolve_tac ctxt [rotate_prems ~1 @{thm sep_rule}]
37  in sep_apply_tactic ctxt sep_drule thms end
38
39fun sep_frule_tactic ctxt thms  =
40  let val sep_frule = forward_tac ctxt [rotate_prems ~1 @{thm sep_rule}]
41  in sep_apply_tactic ctxt sep_frule thms end
42
43fun sep_erule_tactic ctxt thms =
44  let val sep_erule = (eresolve_tac ctxt [@{thm sep_erule}])
45  in sep_apply_tactic ctxt sep_erule thms end
46
47fun sep_rule_tac tac ctxt = rotator (sep_select ctxt) tac ctxt
48fun sep_drule_tac tac ctxt = rotator (sep_asm_select ctxt) tac ctxt
49fun sep_erule_tac tac ctxt =  rotator (sep_asm_select ctxt) tac ctxt
50fun sep_erule_concl_tac tac ctxt = rotator (sep_select ctxt) tac ctxt
51
52fun sep_erule_full_tac tac ctxt =
53  let val r = rotator' ctxt
54  in
55    tac |> r (sep_asm_erule_select ctxt) |> r (sep_select ctxt)
56  end
57
58fun sep_erule_full_tac' tac ctxt =
59  let val r = rotator' ctxt
60  in
61    tac |> r (sep_select ctxt) |> r (sep_asm_erule_select ctxt)
62  end
63
64fun sep_rule_comb_tac true  thms ctxt  = sep_rule_tac (resolve_tac ctxt thms) ctxt
65  | sep_rule_comb_tac false thms ctxt  = sep_rule_tac (sep_rule_tactic ctxt thms) ctxt
66
67fun sep_rule_method bool thms ctxt = SIMPLE_METHOD' (sep_rule_comb_tac bool thms ctxt)
68
69fun sep_drule_comb_tac true  thms ctxt = sep_drule_tac (dresolve_tac ctxt thms) ctxt
70  | sep_drule_comb_tac false thms ctxt = sep_drule_tac (sep_drule_tactic ctxt thms) ctxt
71
72fun sep_drule_method bool thms ctxt = SIMPLE_METHOD' (sep_drule_comb_tac bool thms ctxt)
73
74fun sep_frule_method true  thms ctxt = SIMPLE_METHOD' (sep_drule_tac (forward_tac ctxt thms) ctxt)
75  | sep_frule_method false thms ctxt = SIMPLE_METHOD' (sep_drule_tac (sep_frule_tactic ctxt thms) ctxt)
76
77fun sep_erule_method true  thms ctxt = SIMPLE_METHOD' (sep_erule_tac (eresolve_tac ctxt thms) ctxt)
78  | sep_erule_method false thms ctxt = SIMPLE_METHOD' (sep_erule_tac (sep_erule_tactic ctxt thms) ctxt)
79
80fun sep_erule_concl_method true  thms ctxt =
81      SIMPLE_METHOD' (sep_erule_concl_tac (eresolve_tac ctxt thms) ctxt)
82  | sep_erule_concl_method false thms ctxt =
83      SIMPLE_METHOD' (sep_erule_concl_tac (sep_erule_tactic ctxt thms) ctxt)
84
85fun sep_erule_full_method true thms ctxt =
86      SIMPLE_METHOD' (sep_erule_full_tac (eresolve_tac ctxt thms) ctxt)
87  | sep_erule_full_method false thms ctxt =
88      SIMPLE_METHOD' (sep_erule_full_tac (sep_erule_tactic ctxt thms) ctxt)
89\<close>
90
91method_setup sep_rule = \<open>
92  Scan.lift (Args.mode "direct") -- Attrib.thms  >> uncurry sep_rule_method
93\<close>
94
95method_setup sep_drule = \<open>
96  Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_drule_method
97\<close>
98
99method_setup sep_frule = \<open>
100  Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_frule_method
101\<close>
102
103method_setup sep_erule = \<open>
104  Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_erule_method
105\<close>
106
107method_setup sep_erule_concl = \<open>
108  Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_erule_concl_method
109\<close>
110
111method_setup sep_erule_full = \<open>
112  Scan.lift (Args.mode "direct") -- Attrib.thms>> uncurry sep_erule_full_method
113\<close>
114
115end
116