127 with h[unfolded Hoare_gen_def] |
127 with h[unfolded Hoare_gen_def] |
128 show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))" |
128 show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))" |
129 by (blast elim!: sep_conjE intro!: sep_conjI) |
129 by (blast elim!: sep_conjE intro!: sep_conjI) |
130 qed |
130 qed |
131 |
131 |
132 (* FIXME: generic section ? *) |
|
133 lemma code_extension: |
132 lemma code_extension: |
134 assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
133 assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
135 shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>" |
134 shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>" |
136 using assms |
135 using assms |
137 unfolding Hoare_gen_def |
136 unfolding Hoare_gen_def |
149 and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>" |
148 and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>" |
150 shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>" |
149 shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>" |
151 using assms |
150 using assms |
152 by (auto intro: sequencing code_extension code_extension1) |
151 by (auto intro: sequencing code_extension code_extension1) |
153 |
152 |
|
153 lemma pre_condI: |
|
154 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
155 shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>" |
|
156 proof(induct rule:HoareI) |
|
157 case (Pre r s) |
|
158 hence "cond" "(p \<and>* c \<and>* r) (recse s)" |
|
159 apply (metis pasrt_def sep_conjD) |
|
160 by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def) |
|
161 from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)] |
|
162 show ?case . |
|
163 qed |
|
164 |
|
165 lemma code_condI: |
|
166 assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
167 shows "\<lbrace>p\<rbrace> <b> \<and>* c \<lbrace>q\<rbrace>" |
|
168 proof(induct rule: HoareI) |
|
169 case (Pre r s) |
|
170 hence h1: "b" "(p \<and>* c \<and>* r) (recse s)" |
|
171 apply (metis condD sep_conjD sep_conj_assoc) |
|
172 by (smt Pre.hyps condD sep_conj_impl) |
|
173 from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)] |
|
174 and h1(1) |
|
175 show ?case |
|
176 by (metis (full_types) cond_true_eq1) |
|
177 qed |
|
178 |
|
179 lemma precond_exI: |
|
180 assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
181 shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
182 proof(induct rule: HoareI) |
|
183 case (Pre r s) |
|
184 then obtain x where "(p x \<and>* c \<and>* r) (recse s)" |
|
185 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
186 from h[of x, unfolded Hoare_gen_def, rule_format, OF this] |
|
187 show ?case . |
|
188 qed |
|
189 |
|
190 lemma hoare_sep_false: |
|
191 "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" |
|
192 by(unfold Hoare_gen_def, clarify, simp) |
|
193 |
|
194 |
|
195 lemma pred_exI: |
|
196 assumes "(P(x) \<and>* r) s" |
|
197 shows "((EXS x. P(x)) \<and>* r) s" |
|
198 by (metis assms pred_ex_def sep_globalise) |
154 |
199 |
155 definition |
200 definition |
156 IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" |
201 IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" |
157 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
202 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
158 where |
203 where |
301 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
346 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
302 shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>" |
347 shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>" |
303 using h1 h2 |
348 using h1 h2 |
304 by (smt IHoare_def sep_exec.composition) |
349 by (smt IHoare_def sep_exec.composition) |
305 |
350 |
306 (* FIXME: generic section *) |
|
307 lemma pre_condI: |
|
308 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
309 shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>" |
|
310 proof(induct rule:HoareI) |
|
311 case (Pre r s) |
|
312 hence "cond" "(p \<and>* c \<and>* r) (recse s)" |
|
313 apply (metis pasrt_def sep_conjD) |
|
314 by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def) |
|
315 from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)] |
|
316 show ?case . |
|
317 qed |
|
318 |
|
319 lemma I_pre_condI: |
351 lemma I_pre_condI: |
320 assumes h: "cond \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
352 assumes h: "cond \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
321 shows "I. \<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>" |
353 shows "I. \<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>" |
322 using h |
354 using h |
323 by (smt IHoareI condD cond_true_eq2 sep.mult_commute) |
355 by (smt IHoareI condD cond_true_eq2 sep.mult_commute) |
324 |
356 |
325 (* FIXME: generic section *) |
|
326 lemma code_condI: |
|
327 assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
|
328 shows "\<lbrace>p\<rbrace> <b> \<and>* c \<lbrace>q\<rbrace>" |
|
329 proof(induct rule: HoareI) |
|
330 case (Pre r s) |
|
331 hence h1: "b" "(p \<and>* c \<and>* r) (recse s)" |
|
332 apply (metis condD sep_conjD sep_conj_assoc) |
|
333 by (smt Pre.hyps condD sep_conj_impl) |
|
334 from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)] |
|
335 and h1(1) |
|
336 show ?case |
|
337 by (metis (full_types) cond_true_eq1) |
|
338 qed |
|
339 |
|
340 lemma I_code_condI: |
357 lemma I_code_condI: |
341 assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
358 assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
342 shows "I. \<lbrace>P\<rbrace> <b> \<and>* c \<lbrace>Q\<rbrace>" |
359 shows "I. \<lbrace>P\<rbrace> <b> \<and>* c \<lbrace>Q\<rbrace>" |
343 using h |
360 using h |
344 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1) |
361 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1) |
345 |
362 |
346 (* FIXME: generic section *) |
|
347 lemma precond_exI: |
|
348 assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
349 shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>" |
|
350 proof(induct rule: HoareI) |
|
351 case (Pre r s) |
|
352 then obtain x where "(p x \<and>* c \<and>* r) (recse s)" |
|
353 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
|
354 from h[of x, unfolded Hoare_gen_def, rule_format, OF this] |
|
355 show ?case . |
|
356 qed |
|
357 |
363 |
358 lemma I_precond_exI: |
364 lemma I_precond_exI: |
359 assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>" |
365 assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>" |
360 shows "I. \<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>" |
366 shows "I. \<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>" |
361 proof(induct rule:IHoareI) |
367 proof(induct rule:IHoareI) |
368 where "((<Q t> \<and>* <(t ## s')> \<and>* I (t + s')) \<and>* c \<and>* r) (recse (run (Suc k) cnf))" |
374 where "((<Q t> \<and>* <(t ## s')> \<and>* I (t + s')) \<and>* c \<and>* r) (recse (run (Suc k) cnf))" |
369 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
375 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
370 thus ?case |
376 thus ?case |
371 by (auto simp:sep_conj_ac) |
377 by (auto simp:sep_conj_ac) |
372 qed |
378 qed |
373 |
|
374 (* FIXME: generic section *) |
|
375 lemma hoare_sep_false: |
|
376 "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" |
|
377 by(unfold Hoare_gen_def, clarify, simp) |
|
378 |
379 |
379 lemma I_hoare_sep_false: |
380 lemma I_hoare_sep_false: |
380 "I. \<lbrace>sep_false\<rbrace> c \<lbrace>Q\<rbrace>" |
381 "I. \<lbrace>sep_false\<rbrace> c \<lbrace>Q\<rbrace>" |
381 by (smt IHoareI condD) |
382 by (smt IHoareI condD) |
382 |
383 |