28 "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)" |
28 "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)" |
29 by (rule sep.mult_assoc) |
29 by (rule sep.mult_assoc) |
30 |
30 |
31 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3 |
31 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3 |
32 |
32 |
33 lemma cond_true_eq[simp]: "<True> = \<box>" |
33 lemma cond_true_eq [simp]: |
|
34 "<True> = \<box>" |
34 by(unfold sep_empty_def pasrt_def, auto) |
35 by(unfold sep_empty_def pasrt_def, auto) |
35 |
36 |
36 lemma cond_true_eq1: "(<True> \<and>* p) = p" |
37 lemma cond_true_eq1: |
37 by(simp) |
38 "(<True> \<and>* p) = p" |
38 |
39 by (simp) |
39 lemma false_simp [simp]: "<False> = sep_false" (* move *) |
40 |
|
41 lemma cond_true_eq2: |
|
42 "(p \<and>* <True>) = p" |
|
43 by simp |
|
44 |
|
45 lemma false_simp [simp]: |
|
46 "<False> = sep_false" (* move *) |
40 by (simp add:pasrt_def) |
47 by (simp add:pasrt_def) |
41 |
48 |
42 lemma cond_true_eq2: "(p \<and>* <True>) = p" |
49 lemma condD: |
43 by simp |
50 "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" |
44 |
51 unfolding sep_conj_def pasrt_def |
45 lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" |
52 by auto |
46 by (unfold sep_conj_def pasrt_def, auto) |
|
47 |
53 |
48 locale sep_exec = |
54 locale sep_exec = |
49 fixes step :: "'conf \<Rightarrow> 'conf" |
55 fixes step :: "'conf \<Rightarrow> 'conf" |
50 and recse:: "'conf \<Rightarrow> 'a::sep_algebra" |
56 and recse:: "'conf \<Rightarrow> 'a::sep_algebra" |
51 begin |
57 begin |
187 show ?case . |
193 show ?case . |
188 qed |
194 qed |
189 |
195 |
190 lemma hoare_sep_false: |
196 lemma hoare_sep_false: |
191 "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" |
197 "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" |
192 by(unfold Hoare_gen_def, clarify, simp) |
198 unfolding Hoare_gen_def |
193 |
199 by auto |
194 |
200 |
195 lemma pred_exI: |
201 lemma pred_exI: |
196 assumes "(P(x) \<and>* r) s" |
202 assumes "(P(x) \<and>* r) s" |
197 shows "((EXS x. P(x)) \<and>* r) s" |
203 shows "((EXS x. P(x)) \<and>* r) s" |
198 by (metis assms pred_ex_def sep_globalise) |
204 by (metis assms pred_ex_def sep_globalise) |