-
Notifications
You must be signed in to change notification settings - Fork 108
/
MonadSep.thy
203 lines (180 loc) · 9.47 KB
/
MonadSep.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory MonadSep
imports
Sep_Algebra_L4v
"Lib.LemmaBucket"
begin
locale sep_lifted =
fixes lft :: "'a \<Rightarrow> 's :: sep_algebra"
begin
abbreviation
lift :: "('s \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ("<_>")
where
"<P> s \<equiv> P (lft s)"
lemma hoare_gen_lifted_asm:
"(P \<Longrightarrow> \<lbrace>\<lambda>s. P' (lft s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P' and K P) (lft s)\<rbrace> f \<lbrace>Q\<rbrace>"
by (auto intro: hoare_assume_pre)
lemma mapM_x_sep_inv':
includes no_pre
assumes f:
"\<And>R x. x \<in> S \<Longrightarrow>
\<lbrace>\<lambda>s.<P x \<and>* I \<and>* R> s \<and> I' s\<rbrace>
f x
\<lbrace>\<lambda>_ s.<Q x \<and>* I \<and>* R> s \<and> I' s\<rbrace>"
shows
"set xs \<subseteq> S \<Longrightarrow>
\<lbrace>\<lambda>s.<\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>
mapM_x f xs
\<lbrace>\<lambda>_ s.<\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>"
proof (induct xs arbitrary: R)
case Nil
thus ?case by (simp add: mapM_x_Nil)
next
case (Cons x xs)
thus ?case
apply (simp add: sep_conj_assoc mapM_x_Cons)
apply (wp)
apply (insert Cons.hyps [where R1="Q x ** R"])[1]
apply (simp add: sep_conj_ac)
apply (insert f [where R1="R ** \<And>* map P xs" and x1=x ])[1]
apply (simp add: sep_conj_ac)
done
qed
lemmas mapM_x_sep_inv = mapM_x_sep_inv' [OF _ subset_refl]
lemmas mapM_x_sep = mapM_x_sep_inv [where I' = \<top>, simplified]
lemmas mapM_x_sep' = mapM_x_sep [where I=\<box>, simplified]
lemma mapM_x_set_sep_inv:
"\<lbrakk>distinct xs; set xs = X; (\<And>R x. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>)\<rbrakk> \<Longrightarrow>
\<lbrace><(\<And>* x \<in> X. P x) \<and>* I \<and>* R> and I'\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <(\<And>* x \<in> X. Q x) \<and>* I \<and>* R> and I'\<rbrace>"
apply (clarsimp simp: pred_conj_def)
apply (drule mapM_x_sep_inv [where R=R])
apply (subst (asm) sep_list_conj_sep_map_set_conj, assumption)+
apply assumption
done
lemmas mapM_x_set_sep' = mapM_x_set_sep_inv [where I' = \<top>, simplified]
lemma mapM_x_set_sep:
"\<lbrakk>distinct xs; \<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><(\<And>* x \<in> set xs. P x) \<and>* I \<and>* R>\<rbrace> mapM_x f xs \<lbrace>\<lambda>_. <(\<And>* x \<in> set xs. Q x) \<and>* I \<and>* R>\<rbrace>"
by (erule mapM_x_set_sep', simp+)
(* NOTE: unused *)
lemma foldM_Cons:
"foldM f (x # xs) acc =
do acc' \<leftarrow> foldM f xs acc;
f x acc'
od"
by (clarsimp simp: foldM_def)
lemma foldM_sep_inv':
includes no_pre
assumes f:
"\<And>R x acc. x \<in> S \<Longrightarrow>
\<lbrace>\<lambda>s. <P x \<and>* I \<and>* R> s \<and> I' s\<rbrace>
f x acc
\<lbrace>\<lambda>acc' s. <Q x \<and>* I \<and>* R> s \<and> I' s\<rbrace>"
shows
"set xs \<subseteq> S \<Longrightarrow>
\<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>
foldM f xs acc
\<lbrace>\<lambda>acc' s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>"
proof (induct xs arbitrary: R acc)
case Nil
thus ?case
by (simp add: foldM_def)
next
case (Cons x xs)
thus ?case
apply (simp add: sep_conj_assoc foldM_Cons)
apply wp
apply (insert f[where R1="R ** \<And>* map Q xs" and x1=x])[1]
apply (fastforce simp: sep_conj_ac)
apply (insert Cons.hyps [where R1="P x ** R"])[1]
apply (clarsimp simp: sep_conj_ac)
done
qed
lemmas foldM_sep_inv = foldM_sep_inv' [OF _ subset_refl]
lemmas foldM_sep = foldM_sep_inv [where I' = \<top>, simplified]
lemmas foldM_sep' = foldM_sep [where I=\<box>, simplified]
lemma foldM_set_sep_inv:
"\<lbrakk>distinct xs;
set xs = X;
\<And>R x acc. x \<in> X \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R> and I'\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R> and I'\<rbrace>\<rbrakk> \<Longrightarrow>
\<lbrace><(\<And>* x \<in> X. P x) \<and>* I \<and>* R> and I'\<rbrace>
foldM f xs acc
\<lbrace>\<lambda>_. <(\<And>* x \<in> X. Q x) \<and>* I \<and>* R> and I'\<rbrace>"
apply (clarsimp simp: pred_conj_def)
apply (drule foldM_sep_inv [where R=R])
apply (subst (asm) sep_list_conj_sep_map_set_conj, assumption)+
apply assumption
done
lemmas foldM_set_sep' = foldM_set_sep_inv [where I' = \<top>, simplified]
lemma foldM_set_sep:
"\<lbrakk>distinct xs;
\<And>R x acc. x \<in> set xs \<Longrightarrow> \<lbrace><P x \<and>* I \<and>* R>\<rbrace> f x acc \<lbrace>\<lambda>_. <Q x \<and>* I \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><(\<And>* x \<in> set xs. P x) \<and>* I \<and>* R>\<rbrace> foldM f xs acc \<lbrace>\<lambda>_. <(\<And>* x \<in> set xs. Q x) \<and>* I \<and>* R>\<rbrace>"
by (erule foldM_set_sep', simp+)
lemma sep_list_conj_map_singleton_wp:
"\<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>"
apply (rule hoare_chain[where P'="<P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>" and
Q'="\<lambda>_. <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>"])
apply fastforce
apply (subst (asm) sep_list_conj_map_remove1, assumption)
apply (sep_select_asm 3)
apply (sep_solve)
apply (subst sep_list_conj_map_remove1, sep_solve+)
done
lemma sep_set_conj_map_singleton_wp:
"\<lbrakk>finite xs; x \<in> xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* (\<And>* x\<in>xs. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x\<in>xs. I x) \<and>* R>\<rbrace>"
apply (rule hoare_chain[where P'="<P \<and>* I x \<and>* (\<And>* x\<in>xs - {x}. I x) \<and>* R>" and
Q'="\<lambda>_. <Q \<and>* I x \<and>* (\<And>* x\<in>xs - {x}. I x) \<and>* R>"], assumption)
apply (subst (asm) sep.prod.remove, assumption+)
apply sep_solve
apply (subst sep.prod.remove, assumption+)
apply sep_solve
done
lemma sep_list_conj_submap_wp:
"\<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys;
\<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* R>\<rbrace>"
apply (subst sep_list_con_map_filter [where t="\<lambda>x. x \<in> set xs" and xs=ys, THEN sym])
apply (subst sep_list_con_map_filter [where t="\<lambda>x. x \<in> set xs" and xs=ys, THEN sym])
apply (subgoal_tac "set [x\<leftarrow>ys . x \<in> set xs] = set xs")
apply (subst sep_list_conj_eq [where xs="[x\<leftarrow>ys . x \<in> set xs]" and ys=xs], clarsimp+)
apply (subst sep_list_conj_eq [where xs="[x\<leftarrow>ys . x \<in> set xs]" and ys=xs], clarsimp+)
apply (clarsimp simp: sep_conj_assoc)
apply auto
done
(* This just saves some rearranging later. *)
lemma sep_list_conj_submap_wp':
"\<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys;
\<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* S \<and>* R>\<rbrace>"
apply (cut_tac sep_list_conj_submap_wp [where P="P \<and>* S" and Q="Q \<and>* S" and
I=I and R=R and ys=ys and xs=xs and f=f])
apply (fastforce simp: sep_conj_ac)+
done
lemma sep_set_conj_subset_wp:
"\<lbrakk>xs \<subseteq> ys; finite xs; finite ys;
\<And>R. \<lbrace><P \<and>* (\<And>* x \<in> xs. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> xs. I x) \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* (\<And>* x \<in> ys. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> ys. I x) \<and>* R>\<rbrace>"
apply (subst sep_map_set_conj_restrict [where t="\<lambda>x. x \<in> xs" and xs=ys], assumption)
apply (subst sep_map_set_conj_restrict [where t="\<lambda>x. x \<in> xs" and xs=ys], assumption)
apply (subgoal_tac "{x \<in> ys. x \<in> xs} = xs")
apply (clarsimp simp: sep_conj_assoc)
apply auto
done
(* This just saves some rearranging later. *)
lemma sep_set_conj_subset_wp':
"\<lbrakk>xs \<subseteq> ys; finite xs; finite ys;
\<And>R. \<lbrace><P \<and>* (\<And>* x \<in> xs. I x) \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> xs. I x) \<and>* S \<and>* R>\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace><P \<and>* (\<And>* x \<in> ys. I x) \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> ys. I x) \<and>* S \<and>* R>\<rbrace>"
apply (cut_tac sep_set_conj_subset_wp [where P="P \<and>* S" and Q="Q \<and>* S" and
I=I and R=R and ys=ys and xs=xs and f=f])
apply (fastforce simp: sep_conj_ac)+
done
end
end