|
1 header {* |
|
2 Generic Separation Logic |
|
3 *} |
|
4 |
|
5 theory Hoare_gen |
|
6 imports Main |
|
7 (*"../progtut/Tactical" *) |
|
8 "../Separation_Algebra/Sep_Tactics" |
|
9 begin |
|
10 |
|
11 ML_file "../Separation_Algebra/sep_tactics.ML" |
|
12 |
|
13 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71) |
|
14 where "pasrt b = (\<lambda> s . s = 0 \<and> b)" |
|
15 |
|
16 lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)" |
|
17 by(simp add: sep_conj_ac) |
|
18 |
|
19 lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)" |
|
20 by(simp add: sep_conj_ac) |
|
21 |
|
22 lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)" |
|
23 by (metis sep.mult_assoc) |
|
24 |
|
25 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3 |
|
26 |
|
27 lemma cond_true_eq[simp]: "<True> = \<box>" |
|
28 by(unfold sep_empty_def pasrt_def, auto) |
|
29 |
|
30 lemma cond_true_eq1: "(<True> \<and>* p) = p" |
|
31 by(simp) |
|
32 |
|
33 lemma false_simp [simp]: "<False> = sep_false" (* move *) |
|
34 by (simp add:pasrt_def) |
|
35 |
|
36 lemma cond_true_eq2: "(p \<and>* <True>) = p" |
|
37 by simp |
|
38 |
|
39 lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s" |
|
40 by (unfold sep_conj_def pasrt_def, auto) |
|
41 |
|
42 locale sep_exec = |
|
43 fixes step :: "'conf \<Rightarrow> 'conf" |
|
44 and recse:: "'conf \<Rightarrow> 'a::sep_algebra" |
|
45 begin |
|
46 |
|
47 definition "run n = step ^^ n" |
|
48 |
|
49 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)" |
|
50 apply (unfold run_def) |
|
51 by (metis funpow_add o_apply) |
|
52 |
|
53 definition |
|
54 Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
55 ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
|
56 where |
|
57 "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> \<equiv> |
|
58 (\<forall> s r. (p**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))" |
|
59 |
|
60 lemma HoareI [case_names Pre]: |
|
61 assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))" |
|
62 shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>" |
|
63 using h |
|
64 by (unfold Hoare_gen_def, auto) |
|
65 |
|
66 lemma frame_rule: |
|
67 assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>" |
|
68 shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>" |
|
69 proof(induct rule: HoareI) |
|
70 case (Pre r' s') |
|
71 hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac) |
|
72 from h[unfolded Hoare_gen_def, rule_format, OF this] |
|
73 show ?case |
|
74 by (metis sep_conj_assoc sep_conj_left_commute) |
|
75 qed |
|
76 |
|
77 lemma sequencing: |
|
78 assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
79 and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>" |
|
80 shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>" |
|
81 proof(induct rule:HoareI) |
|
82 case (Pre r' s') |
|
83 from h1[unfolded Hoare_gen_def, rule_format, OF Pre] |
|
84 obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto |
|
85 from h2[unfolded Hoare_gen_def, rule_format, OF this] |
|
86 obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto |
|
87 thus ?case |
|
88 apply (rule_tac x = "Suc (k1 + k2)" in exI) |
|
89 by (metis add_Suc_right nat_add_commute sep_exec.run_add) |
|
90 qed |
|
91 |
|
92 lemma pre_stren: |
|
93 assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
94 and h2: "\<And>s. r s \<Longrightarrow> p s" |
|
95 shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>" |
|
96 proof(induct rule:HoareI) |
|
97 case (Pre r' s') |
|
98 with h2 |
|
99 have "(p \<and>* c \<and>* r') (recse s')" |
|
100 by (metis sep_conj_impl1) |
|
101 from h1[unfolded Hoare_gen_def, rule_format, OF this] |
|
102 show ?case . |
|
103 qed |
|
104 |
|
105 lemma post_weaken: |
|
106 assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
107 and h2: "\<And> s. q s \<Longrightarrow> r s" |
|
108 shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>" |
|
109 proof(induct rule:HoareI) |
|
110 case (Pre r' s') |
|
111 from h1[unfolded Hoare_gen_def, rule_format, OF this] |
|
112 obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast |
|
113 with h2 |
|
114 show ?case |
|
115 by (metis sep_conj_impl1) |
|
116 qed |
|
117 |
|
118 lemma hoare_adjust: |
|
119 assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>" |
|
120 and h2: "\<And>s. p s \<Longrightarrow> p1 s" |
|
121 and h3: "\<And>s. q1 s \<Longrightarrow> q s" |
|
122 shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
123 using h1 h2 h3 post_weaken pre_stren |
|
124 by (metis) |
|
125 |
|
126 lemma code_exI: |
|
127 assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>" |
|
128 shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>" |
|
129 proof(unfold pred_ex_def, induct rule:HoareI) |
|
130 case (Pre r' s') |
|
131 then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')" |
|
132 by (auto elim!:sep_conjE intro!:sep_conjI) |
|
133 from h[unfolded Hoare_gen_def, rule_format, OF this] |
|
134 show ?case |
|
135 by (auto elim!:sep_conjE intro!:sep_conjI) |
|
136 qed |
|
137 |
|
138 lemma code_extension: |
|
139 assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>" |
|
140 shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>" |
|
141 proof(induct rule:HoareI) |
|
142 case (Pre r' s') |
|
143 hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac) |
|
144 from h[unfolded Hoare_gen_def, rule_format, OF this] |
|
145 show ?case |
|
146 by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac) |
|
147 qed |
|
148 |
|
149 lemma code_extension1: |
|
150 assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>" |
|
151 shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>" |
|
152 by (metis code_extension h sep.mult_commute) |
|
153 |
|
154 lemma composition: |
|
155 assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>" |
|
156 and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>" |
|
157 shows "\<lbrace>p\<rbrace> c1 ** c2 \<lbrace>r\<rbrace>" |
|
158 proof(induct rule:HoareI) |
|
159 case (Pre r' s') |
|
160 hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac) |
|
161 from h1[unfolded Hoare_gen_def, rule_format, OF this] |
|
162 obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))" |
|
163 by (auto simp:sep_conj_ac) |
|
164 from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add] |
|
165 show ?case |
|
166 by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac) |
|
167 qed |
|
168 |
|
169 |
|
170 definition |
|
171 IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> |
|
172 ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" |
|
173 ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
|
174 where |
|
175 "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c |
|
176 \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)" |
|
177 |
|
178 lemma IHoareI [case_names IPre]: |
|
179 assumes h: "\<And>s' s r cnf . (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> |
|
180 (\<exists>k t. (<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))" |
|
181 shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
182 unfolding IHoare_def |
|
183 proof |
|
184 fix s' |
|
185 show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
|
186 \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" |
|
187 proof(unfold pred_ex_def, induct rule:HoareI) |
|
188 case (Pre r s) |
|
189 then obtain sa where "(<P sa> \<and>* <(sa ## s')> \<and>* I (sa + s') \<and>* c \<and>* r) (recse s)" |
|
190 by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac) |
|
191 hence " (\<exists>k t. (<Q t> \<and>* <(t##s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s)))" |
|
192 by (rule h) |
|
193 then obtain k t where h2: "(<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) s))" |
|
194 by auto |
|
195 thus "\<exists>k. ((\<lambda>s. \<exists>sa. (<Q sa> \<and>* <(sa ## s')> \<and>* I (sa + s')) s) \<and>* c \<and>* r) (recse (run (Suc k) s))" |
|
196 apply (rule_tac x = k in exI) |
|
197 by (auto intro!:sep_conjI elim!:sep_conjE simp:sep_conj_ac) |
|
198 qed |
|
199 qed |
|
200 |
|
201 lemma I_frame_rule: |
|
202 assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
203 shows "I. \<lbrace>P \<and>* R\<rbrace> c \<lbrace>Q \<and>* R\<rbrace>" |
|
204 proof(induct rule:IHoareI) |
|
205 case (IPre s' s r cnf) |
|
206 hence "((<(P \<and>* R) s> \<and>* <(s##s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)" |
|
207 by (auto simp:sep_conj_ac) |
|
208 then obtain s1 s2 |
|
209 where h1: "((<P s1> \<and>* <((s1 + s2) ## s')> \<and>*I (s1 + s2 + s')) \<and>* c \<and>* r) (recse cnf)" |
|
210 "s1 ## s2" "s1 + s2 ## s'" "P s1" "R s2" |
|
211 by (unfold pasrt_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
212 hence "((EXS s. <P s> \<and>* <(s ## s2 +s')> \<and>*I (s + (s2 + s'))) \<and>* c \<and>* r) (recse cnf)" |
|
213 apply (sep_cancel, unfold pred_ex_def, auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE) |
|
214 apply (rule_tac x = s1 in exI, unfold pasrt_def, |
|
215 auto intro!:sep_conjI sep_disj_addI3 elim!:sep_conjE simp:sep_conj_ac) |
|
216 by (metis sep_add_assoc sep_add_disjD) |
|
217 from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this] |
|
218 obtain k s where |
|
219 "((<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) \<and>* c \<and>* r) (recse (run (Suc k) cnf))" |
|
220 by (unfold pasrt_def pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
221 thus ?case |
|
222 proof(rule_tac x = k in exI, rule_tac x = "s + s2" in exI, sep_cancel+) |
|
223 fix h ha |
|
224 assume hh: "(<Q s> \<and>* <(s ## s2 + s')> \<and>* I (s + (s2 + s'))) ha" |
|
225 show " (<(Q \<and>* R) (s + s2)> \<and>* <(s + s2 ## s')> \<and>* I (s + s2 + s')) ha" |
|
226 proof - |
|
227 from hh have h0: "s ## s2 + s'" |
|
228 by (metis pasrt_def sep_conjD) |
|
229 with h1(2, 3) |
|
230 have h2: "s + s2 ## s'" |
|
231 by (metis sep_add_disjD sep_disj_addI1) |
|
232 moreover from h1(2, 3) h2 have h3: "(s + (s2 + s')) = (s + s2 + s')" |
|
233 by (metis `s ## s2 + s'` sep_add_assoc sep_add_disjD sep_disj_addD1) |
|
234 moreover from hh have "Q s" by (metis pasrt_def sep_conjD) |
|
235 moreover from h0 h1(2) h1(3) have "s ## s2" |
|
236 by (metis sep_add_disjD sep_disj_addD) |
|
237 moreover note h1(5) |
|
238 ultimately show ?thesis |
|
239 by (smt h0 hh sep_conjI) |
|
240 qed |
|
241 qed |
|
242 qed |
|
243 |
|
244 lemma I_sequencing: |
|
245 assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
246 and h2: "I. \<lbrace>Q\<rbrace> c \<lbrace>R\<rbrace>" |
|
247 shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>" |
|
248 using h1 h2 sequencing |
|
249 by (smt IHoare_def) |
|
250 |
|
251 lemma I_pre_stren: |
|
252 assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
253 and h2: "\<And>s. R s \<Longrightarrow> P s" |
|
254 shows "I. \<lbrace>R\<rbrace> c \<lbrace>Q\<rbrace>" |
|
255 proof(unfold IHoare_def, default) |
|
256 fix s' |
|
257 show "\<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
|
258 \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" |
|
259 proof(rule pre_stren) |
|
260 from h1[unfolded IHoare_def, rule_format, of s'] |
|
261 show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
|
262 \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" . |
|
263 next |
|
264 fix s |
|
265 show "(EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> |
|
266 (EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')) s" |
|
267 apply (unfold pred_ex_def, clarify) |
|
268 apply (rule_tac x = sa in exI, sep_cancel+) |
|
269 by (insert h2, auto simp:pasrt_def) |
|
270 qed |
|
271 qed |
|
272 |
|
273 lemma I_post_weaken: |
|
274 assumes h1: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
275 and h2: "\<And> s. Q s \<Longrightarrow> R s" |
|
276 shows "I. \<lbrace>P\<rbrace> c \<lbrace>R\<rbrace>" |
|
277 proof(unfold IHoare_def, default) |
|
278 fix s' |
|
279 show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
|
280 \<lbrace>EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" |
|
281 proof(rule post_weaken) |
|
282 from h1[unfolded IHoare_def, rule_format, of s'] |
|
283 show "\<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
|
284 \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" . |
|
285 next |
|
286 fix s |
|
287 show "(EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')) s \<Longrightarrow> |
|
288 (EXS s. <R s> \<and>* <(s ## s')> \<and>* I (s + s')) s" |
|
289 apply (unfold pred_ex_def, clarify) |
|
290 apply (rule_tac x = sa in exI, sep_cancel+) |
|
291 by (insert h2, auto simp:pasrt_def) |
|
292 qed |
|
293 qed |
|
294 |
|
295 lemma I_hoare_adjust: |
|
296 assumes h1: "I. \<lbrace>P1\<rbrace> c \<lbrace>Q1\<rbrace>" |
|
297 and h2: "\<And>s. P s \<Longrightarrow> P1 s" |
|
298 and h3: "\<And>s. Q1 s \<Longrightarrow> Q s" |
|
299 shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
300 using h1 h2 h3 I_post_weaken I_pre_stren |
|
301 by (metis) |
|
302 |
|
303 lemma I_code_exI: |
|
304 assumes h: "\<And> k. I. \<lbrace>P\<rbrace> c(k) \<lbrace>Q\<rbrace>" |
|
305 shows "I. \<lbrace>P\<rbrace> EXS k. c(k) \<lbrace>Q\<rbrace>" |
|
306 using h |
|
307 by (smt IHoare_def code_exI) |
|
308 |
|
309 lemma I_code_extension: |
|
310 assumes h: "I. \<lbrace> P \<rbrace> c \<lbrace> Q \<rbrace>" |
|
311 shows "I. \<lbrace> P \<rbrace> c ** e \<lbrace> Q \<rbrace>" |
|
312 using h |
|
313 by (smt IHoare_def sep_exec.code_extension) |
|
314 |
|
315 lemma I_composition: |
|
316 assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>" |
|
317 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
|
318 shows "I. \<lbrace>P\<rbrace> c1 ** c2 \<lbrace>R\<rbrace>" |
|
319 using h1 h2 |
|
320 by (smt IHoare_def sep_exec.composition) |
|
321 |
|
322 lemma pre_condI: |
|
323 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
324 shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>" |
|
325 proof(induct rule:HoareI) |
|
326 case (Pre r s) |
|
327 hence "cond" "(p \<and>* c \<and>* r) (recse s)" |
|
328 apply (metis pasrt_def sep_conjD) |
|
329 by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def) |
|
330 from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)] |
|
331 show ?case . |
|
332 qed |
|
333 |
|
334 lemma I_pre_condI: |
|
335 assumes h: "cond \<Longrightarrow> I.\<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
336 shows "I.\<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
337 using h |
|
338 by (smt IHoareI condD cond_true_eq2 sep.mult_commute) |
|
339 |
|
340 lemma code_condI: |
|
341 assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
342 shows "\<lbrace>p\<rbrace> <b>**c \<lbrace>q\<rbrace>" |
|
343 proof(induct rule: HoareI) |
|
344 case (Pre r s) |
|
345 hence h1: "b" "(p \<and>* c \<and>* r) (recse s)" |
|
346 apply (metis condD sep_conjD sep_conj_assoc) |
|
347 by (smt Pre.hyps condD sep_conj_impl) |
|
348 from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)] |
|
349 and h1(1) |
|
350 show ?case |
|
351 by (metis (full_types) cond_true_eq1) |
|
352 qed |
|
353 |
|
354 lemma I_code_condI: |
|
355 assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
|
356 shows "I.\<lbrace>P\<rbrace> <b>**c \<lbrace>Q\<rbrace>" |
|
357 using h |
|
358 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1) |
|
359 |
|
360 lemma precond_exI: |
|
361 assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
362 shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
363 proof(induct rule:HoareI) |
|
364 case (Pre r s) |
|
365 then obtain x where "(p x \<and>* c \<and>* r) (recse s)" |
|
366 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
367 from h[of x, unfolded Hoare_gen_def, rule_format, OF this] |
|
368 show ?case . |
|
369 qed |
|
370 |
|
371 lemma I_precond_exI: |
|
372 assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>" |
|
373 shows "I.\<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>" |
|
374 proof(induct rule:IHoareI) |
|
375 case (IPre s' s r cnf) |
|
376 then obtain x |
|
377 where "((EXS s. <P x s> \<and>* <(s ## s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)" |
|
378 by ( auto elim!:sep_conjE intro!:sep_conjI simp:pred_ex_def pasrt_def sep_conj_ac) |
|
379 from h[unfolded IHoare_def Hoare_gen_def, rule_format, OF this] |
|
380 obtain k t |
|
381 where "((<Q t> \<and>* <(t ## s')> \<and>* I (t + s')) \<and>* c \<and>* r) (recse (run (Suc k) cnf))" |
|
382 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
383 thus ?case |
|
384 by (auto simp:sep_conj_ac) |
|
385 qed |
|
386 |
|
387 lemma hoare_sep_false: |
|
388 "\<lbrace>sep_false\<rbrace> c |
|
389 \<lbrace>q\<rbrace>" |
|
390 by(unfold Hoare_gen_def, clarify, simp) |
|
391 |
|
392 lemma I_hoare_sep_false: |
|
393 "I. \<lbrace>sep_false\<rbrace> c |
|
394 \<lbrace>Q\<rbrace>" |
|
395 by (smt IHoareI condD) |
|
396 |
|
397 end |
|
398 |
|
399 instantiation set :: (type)sep_algebra |
|
400 begin |
|
401 |
|
402 definition set_zero_def: "0 = {}" |
|
403 |
|
404 definition plus_set_def: "s1 + s2 = s1 \<union> s2" |
|
405 |
|
406 definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})" |
|
407 |
|
408 lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def |
|
409 |
|
410 instance |
|
411 apply(default) |
|
412 apply(simp add:set_ins_def) |
|
413 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
414 apply (metis inf_commute) |
|
415 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
416 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
417 apply (metis sup_commute) |
|
418 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
419 apply (metis (lifting) Un_assoc) |
|
420 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
421 apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff) |
|
422 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
423 by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff) |
|
424 end |
|
425 |
|
426 section {* A big operator of infinite separation conjunction *} |
|
427 |
|
428 definition "fam_conj I cpt s = (\<exists> p. (s = (\<Union> i \<in> I. p(i))) \<and> |
|
429 (\<forall> i \<in> I. cpt i (p i)) \<and> |
|
430 (\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j)))" |
|
431 |
|
432 lemma fam_conj_zero_simp: "fam_conj {} cpt = <True>" |
|
433 proof |
|
434 fix s |
|
435 show "fam_conj {} cpt s = (<True>) s" |
|
436 proof |
|
437 assume "fam_conj {} cpt s" |
|
438 then obtain p where "s = (\<Union> i \<in> {}. p(i))" |
|
439 by (unfold fam_conj_def, auto) |
|
440 hence "s = {}" by auto |
|
441 thus "(<True>) s" by (metis pasrt_def set_zero_def) |
|
442 next |
|
443 assume "(<True>) s" |
|
444 hence eq_s: "s = {}" by (metis pasrt_def set_zero_def) |
|
445 let ?p = "\<lambda> i. {}" |
|
446 have "(s = (\<Union> i \<in> {}. ?p(i)))" by (unfold eq_s, auto) |
|
447 moreover have "(\<forall> i \<in> {}. cpt i (?p i))" by auto |
|
448 moreover have "(\<forall> i \<in> {}. \<forall> j \<in> {}. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" by auto |
|
449 ultimately show "fam_conj {} cpt s" |
|
450 by (unfold eq_s fam_conj_def, auto) |
|
451 qed |
|
452 qed |
|
453 |
|
454 lemma fam_conj_disj_simp_pre: |
|
455 assumes h1: "I = I1 + I2" |
|
456 and h2: "I1 ## I2" |
|
457 shows "fam_conj I cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)" |
|
458 proof |
|
459 fix s |
|
460 let ?fm = "fam_conj I cpt" and ?fm1 = "fam_conj I1 cpt" and ?fm2 = "fam_conj I2 cpt" |
|
461 show "?fm s = (?fm1 \<and>* ?fm2) s" |
|
462 proof |
|
463 assume "?fm s" |
|
464 then obtain p where pre: |
|
465 "s = (\<Union> i \<in> I. p(i))" |
|
466 "(\<forall> i \<in> I. cpt i (p i))" |
|
467 "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j))" |
|
468 unfolding fam_conj_def by metis |
|
469 from pre(1) h1 h2 have "s = (\<Union> i \<in> I1. p(i)) + (\<Union> i \<in> I2. p(i))" |
|
470 by (auto simp:set_ins_def) |
|
471 moreover from pre h1 have "?fm1 (\<Union> i \<in> I1. p(i))" |
|
472 by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def) |
|
473 moreover from pre h1 have "?fm2 (\<Union> i \<in> I2. p(i))" |
|
474 by (unfold fam_conj_def, rule_tac x = p in exI, auto simp:set_ins_def) |
|
475 moreover have "(\<Union> i \<in> I1. p(i)) ## (\<Union> i \<in> I2. p(i))" |
|
476 proof - |
|
477 { fix x xa xb |
|
478 assume h: "I1 \<inter> I2 = {}" |
|
479 "\<forall>i\<in>I1 \<union> I2. \<forall>j\<in>I1 \<union> I2. i \<noteq> j \<longrightarrow> p i \<inter> p j = {}" |
|
480 "xa \<in> I1" "x \<in> p xa" "xb \<in> I2" "x \<in> p xb" |
|
481 have "p xa \<inter> p xb = {}" |
|
482 proof(rule h(2)[rule_format]) |
|
483 from h(1, 3, 5) show "xa \<in> I1 \<union> I2" by auto |
|
484 next |
|
485 from h(1, 3, 5) show "xb \<in> I1 \<union> I2" by auto |
|
486 next |
|
487 from h(1, 3, 5) show "xa \<noteq> xb" by auto |
|
488 qed with h(4, 6) have False by auto |
|
489 } with h1 h2 pre(3) show ?thesis by (auto simp:set_ins_def) |
|
490 qed |
|
491 ultimately show "(?fm1 \<and>* ?fm2) s" by (auto intro!:sep_conjI) |
|
492 next |
|
493 assume "(?fm1 \<and>* ?fm2) s" |
|
494 then obtain s1 s2 where pre: |
|
495 "s = s1 + s2" "s1 ## s2" "?fm1 s1" "?fm2 s2" |
|
496 by (auto dest!:sep_conjD) |
|
497 from pre(3) obtain p1 where pre1: |
|
498 "s1 = (\<Union> i \<in> I1. p1(i))" |
|
499 "(\<forall> i \<in> I1. cpt i (p1 i))" |
|
500 "(\<forall> i \<in> I1. \<forall> j \<in> I1. i \<noteq> j \<longrightarrow> p1(i) ## p1(j))" |
|
501 unfolding fam_conj_def by metis |
|
502 from pre(4) obtain p2 where pre2: |
|
503 "s2 = (\<Union> i \<in> I2. p2(i))" |
|
504 "(\<forall> i \<in> I2. cpt i (p2 i))" |
|
505 "(\<forall> i \<in> I2. \<forall> j \<in> I2. i \<noteq> j \<longrightarrow> p2(i) ## p2(j))" |
|
506 unfolding fam_conj_def by metis |
|
507 let ?p = "\<lambda> i. if i \<in> I1 then p1 i else p2 i" |
|
508 from h2 pre(2) |
|
509 have "s = (\<Union> i \<in> I. ?p(i))" |
|
510 apply (unfold h1 pre(1) pre1(1) pre2(1) set_ins_def, auto split:if_splits) |
|
511 by (metis disjoint_iff_not_equal) |
|
512 moreover from h2 pre1(2) pre2(2) have "(\<forall> i \<in> I. cpt i (?p i))" |
|
513 by (unfold h1 set_ins_def, auto split:if_splits) |
|
514 moreover from pre1(1, 3) pre2(1, 3) pre(2) h2 |
|
515 have "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> ?p(i) ## ?p(j))" |
|
516 apply (unfold h1 set_ins_def, auto split:if_splits) |
|
517 by (metis IntI empty_iff) |
|
518 ultimately show "?fm s" by (unfold fam_conj_def, auto) |
|
519 qed |
|
520 qed |
|
521 |
|
522 lemma fam_conj_disj_simp: |
|
523 assumes h: "I1 ## I2" |
|
524 shows "fam_conj (I1 + I2) cpt = (fam_conj I1 cpt \<and>* fam_conj I2 cpt)" |
|
525 proof - |
|
526 from fam_conj_disj_simp_pre[OF _ h, of "I1 + I2"] |
|
527 show ?thesis by simp |
|
528 qed |
|
529 |
|
530 lemma fam_conj_elm_simp: |
|
531 assumes h: "i \<in> I" |
|
532 shows "fam_conj I cpt = (cpt(i) \<and>* fam_conj (I - {i}) cpt)" |
|
533 proof |
|
534 fix s |
|
535 show "fam_conj I cpt s = (cpt i \<and>* fam_conj (I - {i}) cpt) s" |
|
536 proof |
|
537 assume pre: "fam_conj I cpt s" |
|
538 show "(cpt i \<and>* fam_conj (I - {i}) cpt) s" |
|
539 proof - |
|
540 from pre obtain p where pres: |
|
541 "s = (\<Union> i \<in> I. p(i))" |
|
542 "(\<forall> i \<in> I. cpt i (p i))" |
|
543 "(\<forall> i \<in> I. \<forall> j \<in> I. i \<noteq> j \<longrightarrow> p(i) ## p(j))" |
|
544 unfolding fam_conj_def by metis |
|
545 let ?s = "(\<Union>i\<in>(I - {i}). p i)" |
|
546 from pres(3) h have disj: "(p i) ## ?s" |
|
547 by (auto simp:set_ins_def) |
|
548 moreover from pres(1) h have eq_s: "s = (p i) + ?s" |
|
549 by (auto simp:set_ins_def) |
|
550 moreover from pres(2) h have "cpt i (p i)" by auto |
|
551 moreover from pres have "(fam_conj (I - {i}) cpt) ?s" |
|
552 by (unfold fam_conj_def, rule_tac x = p in exI, auto) |
|
553 ultimately show ?thesis by (auto intro!:sep_conjI) |
|
554 qed |
|
555 next |
|
556 let ?fam = "fam_conj (I - {i}) cpt" |
|
557 assume "(cpt i \<and>* ?fam) s" |
|
558 then obtain s1 s2 where pre: |
|
559 "s = s1 + s2" "s1 ## s2" "cpt i s1" "?fam s2" |
|
560 by (auto dest!:sep_conjD) |
|
561 from pre(4) obtain p where pres: |
|
562 "s2 = (\<Union> ia \<in> I - {i}. p(ia))" |
|
563 "(\<forall> ia \<in> I - {i}. cpt ia (p ia))" |
|
564 "(\<forall> ia \<in> I - {i}. \<forall> j \<in> I - {i}. ia \<noteq> j \<longrightarrow> p(ia) ## p(j))" |
|
565 unfolding fam_conj_def by metis |
|
566 let ?p = "p(i:=s1)" |
|
567 from h pres(3) pre(2)[unfolded pres(1)] |
|
568 have " \<forall>ia\<in>I. \<forall>j\<in>I. ia \<noteq> j \<longrightarrow> ?p ia ## ?p j" by (auto simp:set_ins_def) |
|
569 moreover from pres(1) pre(1) h pre(2) |
|
570 have "(s = (\<Union> i \<in> I. ?p(i)))" by (auto simp:set_ins_def split:if_splits) |
|
571 moreover from pre(3) pres(2) h |
|
572 have "(\<forall> i \<in> I. cpt i (?p i))" by (auto simp:set_ins_def split:if_splits) |
|
573 ultimately show "fam_conj I cpt s" |
|
574 by (unfold fam_conj_def, auto) |
|
575 qed |
|
576 qed |
|
577 |
|
578 lemma fam_conj_insert_simp: |
|
579 assumes h:"i \<notin> I" |
|
580 shows "fam_conj (insert i I) cpt = (cpt(i) \<and>* fam_conj I cpt)" |
|
581 proof - |
|
582 have "i \<in> insert i I" by auto |
|
583 from fam_conj_elm_simp[OF this] and h |
|
584 show ?thesis by auto |
|
585 qed |
|
586 |
|
587 lemmas fam_conj_simps = fam_conj_insert_simp fam_conj_zero_simp |
|
588 |
|
589 lemma "fam_conj {0, 2, 3} cpt = (cpt 2 \<and>* cpt (0::int) \<and>* cpt 3)" |
|
590 by (simp add:fam_conj_simps sep_conj_ac) |
|
591 |
|
592 lemma fam_conj_ext_eq: |
|
593 assumes h: "\<And> i . i \<in> I \<Longrightarrow> f i = g i" |
|
594 shows "fam_conj I f = fam_conj I g" |
|
595 proof |
|
596 fix s |
|
597 show "fam_conj I f s = fam_conj I g s" |
|
598 by (unfold fam_conj_def, auto simp:h) |
|
599 qed |
|
600 |
|
601 end |
|
602 |