58 (* separation Hoare tripple *) |
59 (* separation Hoare tripple *) |
59 definition |
60 definition |
60 Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
61 Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
61 where |
62 where |
62 "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv> |
63 "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv> |
63 (\<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s)))))" |
64 \<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. (q \<and>* c \<and>* r) (recse (run (Suc k) s)))" |
64 |
65 |
65 lemma HoareI [case_names Pre]: |
66 lemma HoareI [case_names Pre]: |
66 assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s))))" |
67 assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> \<exists>k. (q \<and>* c \<and>* r) (recse (run (Suc k) s))" |
67 shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
68 shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
68 using h |
69 using h |
69 unfolding Hoare_gen_def |
70 unfolding Hoare_gen_def |
70 by simp |
71 by simp |
71 |
72 |
121 unfolding pred_ex_def |
122 unfolding pred_ex_def |
122 proof(induct rule:HoareI) |
123 proof(induct rule:HoareI) |
123 case (Pre r' s') |
124 case (Pre r' s') |
124 then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')" |
125 then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')" |
125 by (auto elim!: sep_conjE intro!: sep_conjI) |
126 by (auto elim!: sep_conjE intro!: sep_conjI) |
126 from h[unfolded Hoare_gen_def, rule_format, OF this] |
127 with h[unfolded Hoare_gen_def] |
127 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'))" |
128 by (auto elim!: sep_conjE intro!: sep_conjI) |
129 by (blast elim!: sep_conjE intro!: sep_conjI) |
129 qed |
130 qed |
130 |
131 |
|
132 (* FIXME: generic section ? *) |
131 lemma code_extension: |
133 lemma code_extension: |
132 assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
134 assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
133 shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>" |
135 shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>" |
134 using assms |
136 using assms |
135 unfolding Hoare_gen_def |
137 unfolding Hoare_gen_def |
152 |
154 |
153 definition |
155 definition |
154 IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" |
156 IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" |
155 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
157 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
156 where |
158 where |
157 "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c |
159 "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c |
158 \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)" |
160 \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)" |
159 |
161 |
160 lemma IHoareI [case_names IPre]: |
162 lemma IHoareI [case_names IPre]: |
161 assumes h: "\<And>s' s r cnf . (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> |
163 assumes h: "\<And>s' s r cnf . (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> |
162 (\<exists>k t. (<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))" |
164 \<exists>k t. (<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf))" |
163 shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
165 shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
164 unfolding IHoare_def |
166 unfolding IHoare_def |
165 proof |
167 proof |
166 fix s' |
168 fix s' |
167 show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
169 show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c |
299 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
301 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
300 shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>" |
302 shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>" |
301 using h1 h2 |
303 using h1 h2 |
302 by (smt IHoare_def sep_exec.composition) |
304 by (smt IHoare_def sep_exec.composition) |
303 |
305 |
|
306 (* FIXME: generic section *) |
304 lemma pre_condI: |
307 lemma pre_condI: |
305 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
308 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
306 shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>" |
309 shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>" |
307 proof(induct rule:HoareI) |
310 proof(induct rule:HoareI) |
308 case (Pre r s) |
311 case (Pre r s) |
312 from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)] |
315 from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)] |
313 show ?case . |
316 show ?case . |
314 qed |
317 qed |
315 |
318 |
316 lemma I_pre_condI: |
319 lemma I_pre_condI: |
317 assumes h: "cond \<Longrightarrow> I.\<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
320 assumes h: "cond \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
318 shows "I.\<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>" |
321 shows "I. \<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>" |
319 using h |
322 using h |
320 by (smt IHoareI condD cond_true_eq2 sep.mult_commute) |
323 by (smt IHoareI condD cond_true_eq2 sep.mult_commute) |
321 |
324 |
|
325 (* FIXME: generic section *) |
322 lemma code_condI: |
326 lemma code_condI: |
323 assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
327 assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
324 shows "\<lbrace>p\<rbrace> <b>**c \<lbrace>q\<rbrace>" |
328 shows "\<lbrace>p\<rbrace> <b> \<and>* c \<lbrace>q\<rbrace>" |
325 proof(induct rule: HoareI) |
329 proof(induct rule: HoareI) |
326 case (Pre r s) |
330 case (Pre r s) |
327 hence h1: "b" "(p \<and>* c \<and>* r) (recse s)" |
331 hence h1: "b" "(p \<and>* c \<and>* r) (recse s)" |
328 apply (metis condD sep_conjD sep_conj_assoc) |
332 apply (metis condD sep_conjD sep_conj_assoc) |
329 by (smt Pre.hyps condD sep_conj_impl) |
333 by (smt Pre.hyps condD sep_conj_impl) |
333 by (metis (full_types) cond_true_eq1) |
337 by (metis (full_types) cond_true_eq1) |
334 qed |
338 qed |
335 |
339 |
336 lemma I_code_condI: |
340 lemma I_code_condI: |
337 assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
341 assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
338 shows "I.\<lbrace>P\<rbrace> <b>**c \<lbrace>Q\<rbrace>" |
342 shows "I. \<lbrace>P\<rbrace> <b> \<and>* c \<lbrace>Q\<rbrace>" |
339 using h |
343 using h |
340 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1) |
344 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1) |
341 |
345 |
|
346 (* FIXME: generic section *) |
342 lemma precond_exI: |
347 lemma precond_exI: |
343 assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>" |
348 assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>" |
344 shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>" |
349 shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>" |
345 proof(induct rule:HoareI) |
350 proof(induct rule: HoareI) |
346 case (Pre r s) |
351 case (Pre r s) |
347 then obtain x where "(p x \<and>* c \<and>* r) (recse s)" |
352 then obtain x where "(p x \<and>* c \<and>* r) (recse s)" |
348 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
353 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
349 from h[of x, unfolded Hoare_gen_def, rule_format, OF this] |
354 from h[of x, unfolded Hoare_gen_def, rule_format, OF this] |
350 show ?case . |
355 show ?case . |
351 qed |
356 qed |
352 |
357 |
353 lemma I_precond_exI: |
358 lemma I_precond_exI: |
354 assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>" |
359 assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>" |
355 shows "I.\<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>" |
360 shows "I. \<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>" |
356 proof(induct rule:IHoareI) |
361 proof(induct rule:IHoareI) |
357 case (IPre s' s r cnf) |
362 case (IPre s' s r cnf) |
358 then obtain x |
363 then obtain x |
359 where "((EXS s. <P x s> \<and>* <(s ## s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)" |
364 where "((EXS s. <P x s> \<and>* <(s ## s')> \<and>* I (s + s')) \<and>* c \<and>* r) (recse cnf)" |
360 by ( auto elim!:sep_conjE intro!:sep_conjI simp:pred_ex_def pasrt_def sep_conj_ac) |
365 by ( auto elim!:sep_conjE intro!:sep_conjI simp:pred_ex_def pasrt_def sep_conj_ac) |
364 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
369 by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI) |
365 thus ?case |
370 thus ?case |
366 by (auto simp:sep_conj_ac) |
371 by (auto simp:sep_conj_ac) |
367 qed |
372 qed |
368 |
373 |
|
374 (* FIXME: generic section *) |
369 lemma hoare_sep_false: |
375 lemma hoare_sep_false: |
370 "\<lbrace>sep_false\<rbrace> c |
376 "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" |
371 \<lbrace>q\<rbrace>" |
|
372 by(unfold Hoare_gen_def, clarify, simp) |
377 by(unfold Hoare_gen_def, clarify, simp) |
373 |
378 |
374 lemma I_hoare_sep_false: |
379 lemma I_hoare_sep_false: |
375 "I. \<lbrace>sep_false\<rbrace> c |
380 "I. \<lbrace>sep_false\<rbrace> c \<lbrace>Q\<rbrace>" |
376 \<lbrace>Q\<rbrace>" |
|
377 by (smt IHoareI condD) |
381 by (smt IHoareI condD) |
378 |
382 |
379 end |
383 end |
380 |
384 |
381 instantiation set :: (type)sep_algebra |
385 instantiation set :: (type)sep_algebra |
389 |
393 |
390 lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def |
394 lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def |
391 |
395 |
392 instance |
396 instance |
393 apply(default) |
397 apply(default) |
394 apply(simp add:set_ins_def) |
398 apply(auto simp: set_ins_def) |
395 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
399 done |
396 apply (metis inf_commute) |
400 |
397 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
398 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
399 apply (metis sup_commute) |
|
400 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
401 apply (metis (lifting) Un_assoc) |
|
402 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
403 apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff) |
|
404 apply(simp add:sep_disj_set_def plus_set_def set_zero_def) |
|
405 by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff) |
|
406 end |
401 end |
407 |
402 |
408 section {* A big operator of infinite separation conjunction *} |
403 section {* A big operator of infinite separation conjunction *} |
409 |
404 |
410 definition "fam_conj I cpt s = (\<exists> p. (s = (\<Union> i \<in> I. p(i))) \<and> |
405 definition "fam_conj I cpt s = (\<exists> p. (s = (\<Union> i \<in> I. p(i))) \<and> |