1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Forward
8imports
9  Extended_Separation_Algebra
10  Sep_Util
11begin
12
13lemma sep_conj_sep_impl_spec:
14  "\<lbrakk>((Q -* R) \<and>* P) h; \<And>h. (Q -* R) h \<Longrightarrow> (P \<longrightarrow>* R') h\<rbrakk> \<Longrightarrow> R' h"
15  by (metis (full_types) sep_conj_sep_impl2)
16
17
18method sep_invert = ((erule sep_septraction_snake | sep_erule (direct) sep_conj_sep_impl_spec),
19                      sep_flatten?; sep_invert?)
20
21lemma sep_conj_coimpl_cancel: "(P \<and>* R) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> P s) \<Longrightarrow> precise P \<Longrightarrow>
22                               (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s"
23  apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def)
24  apply (clarsimp simp: precise_def)
25  apply (erule_tac x=s in allE)
26  apply (erule_tac x=x in allE)
27  apply (erule_tac x=xa in allE)
28  apply (clarsimp, drule mp)
29   apply (intro conjI)
30    apply (fastforce simp: sep_substate_def)
31   apply (fastforce simp: sep_substate_def)
32  apply (clarsimp)
33  by (metis sep_add_cancelD sep_add_commute sep_disj_commuteI)
34
35lemma sep_conj_coimpl_cancel': "(P \<and>* R) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> precise Q \<Longrightarrow>
36                               (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s"
37  apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def)
38  apply (clarsimp simp: precise_def)
39  apply (erule_tac x=s in allE)
40  apply (erule_tac x=x in allE)
41  apply (erule_tac x=xa in allE)
42  apply (clarsimp, drule mp)
43   apply (intro conjI)
44    apply (fastforce simp: sep_substate_def)
45   apply (fastforce simp: sep_substate_def)
46  apply (clarsimp)
47  by (metis sep_add_cancelD sep_add_commute sep_disj_commuteI)
48
49lemma sep_conj_coimpl_cancel'':
50  "(\<And>s. pred_imp P Q s) \<Longrightarrow> (P \<and>* R) s \<Longrightarrow>  precise Q \<Longrightarrow>
51   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s"
52  by (simp add: sep_conj_coimpl_cancel')
53
54lemma sep_conj_coimpl_cancel''':
55  "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<and>* R) s  \<Longrightarrow> precise P \<Longrightarrow>
56   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s"
57  by (simp add: sep_conj_coimpl_cancel)
58
59lemma sep_coimpl_cancel':
60  "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<leadsto>* R) s   \<Longrightarrow>
61   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s"
62  by (metis pred_neg_def sep_coimpl_def sep_conj_def)
63
64definition "pointer P \<equiv> (\<forall>x y. \<forall>s R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s)"
65
66lemma sep_conj_pointer_coimpl_cancel:
67  "(P x \<and>* R) s  \<Longrightarrow> pointer P \<Longrightarrow>
68   (\<And>s. R s \<Longrightarrow> y = x \<Longrightarrow>  R'  s) \<Longrightarrow> (P y \<leadsto>* R') s"
69  apply (clarsimp simp: pointer_def)
70  apply (erule_tac x=x in allE)
71  apply (erule_tac x=y in allE)
72  apply (erule_tac x=s in allE)
73  apply (erule_tac x=R in allE)
74  apply (clarsimp simp: pred_conj_def)
75  apply (erule sep_coimpl_cancel'[rotated]; simp)
76  done
77
78named_theorems precise
79
80method septract_cancel declares precise =
81   ((sep_erule (direct) sep_cancel[simplified atomize_imp, THEN sep_conj_coimpl_cancel''], rule precise) |
82   (sep_erule (direct) sep_cancel[simplified atomize_imp, THEN sep_conj_coimpl_cancel'''], rule precise) |
83    erule sep_cancel[simplified atomize_imp, THEN sep_coimpl_cancel'] |
84    (sep_erule (direct) sep_conj_pointer_coimpl_cancel , rule precise))
85
86method abs_used for P = (match (P) in "\<lambda>s. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
87
88method sep_lift = match conclusion in "(_ \<longrightarrow>* _) s" for s :: "_ :: sep_algebra" \<Rightarrow>
89                  \<open>((match premises in I[thin]: "P s" for P \<Rightarrow>
90                      \<open>abs_used P,  rule sep_curry[where h=s and P=P, rotated, OF I]\<close>))\<close>
91
92method sep_snake_uncurry = match conclusion in "(_ \<leadsto>* _) s" for s :: "_ :: sep_algebra" \<Rightarrow>
93                  \<open>((match premises in I[thin]: "P s" for P \<Rightarrow>
94                      \<open>abs_used P, rule sep_snake_septraction[where s=s and Q=P, OF I]\<close>))\<close>
95
96lemma septract_impl_cancel: "(P -* Q) s  \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> strictly_exact P \<Longrightarrow> (P \<longrightarrow>* Q') s"
97  apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def strictly_exact_def)
98  by (fastforce)
99
100method sep_forward = (sep_cancel | septract_cancel |  sep_lift |
101                              sep_snake_uncurry )
102
103method sep_forward_solve = (solves \<open>sep_invert; (sep_forward) +\<close>)
104
105method sep_cancel uses add = (Sep_Cancel.sep_cancel add: add | sep_lift)
106
107lemma septract_mp: "\<lbrakk>(R' \<and>* (R' -* R)) s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'\<rbrakk> \<Longrightarrow> R s"
108  apply (sep_invert)
109  apply (atomize, erule allE, drule (1) mp)
110  using precise_conj_coimpl by blast
111
112end