equal
deleted
inserted
replaced
10 definition |
10 definition |
11 pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71) |
11 pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71) |
12 where "pasrt b = (\<lambda> s . s = 0 \<and> b)" |
12 where "pasrt b = (\<lambda> s . s = 0 \<and> b)" |
13 |
13 |
14 |
14 |
15 (* smae as sep.mult.left_commute *) |
15 (* same as sep.mult.left_commute *) |
16 lemma sep_conj_cond1: |
16 lemma sep_conj_cond1: |
17 "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)" |
17 "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)" |
18 by (rule sep.mult.left_commute) |
18 by (rule sep.mult.left_commute) |
19 |
19 |
20 (* same as sep.mult.commute *) |
20 (* same as sep.mult.commute *) |
287 shows "I. \<lbrace>P\<rbrace> EXS k. c(k) \<lbrace>Q\<rbrace>" |
287 shows "I. \<lbrace>P\<rbrace> EXS k. c(k) \<lbrace>Q\<rbrace>" |
288 using h |
288 using h |
289 by (smt IHoare_def code_exI) |
289 by (smt IHoare_def code_exI) |
290 |
290 |
291 lemma I_code_extension: |
291 lemma I_code_extension: |
292 assumes h: "I. \<lbrace> P \<rbrace> c \<lbrace> Q \<rbrace>" |
292 assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" |
293 shows "I. \<lbrace> P \<rbrace> c ** e \<lbrace> Q \<rbrace>" |
293 shows "I. \<lbrace>P\<rbrace> c \<and>* e \<lbrace>Q\<rbrace>" |
294 using h |
294 using h |
295 by (smt IHoare_def sep_exec.code_extension) |
295 by (smt IHoare_def sep_exec.code_extension) |
296 |
296 |
297 lemma I_composition: |
297 lemma I_composition: |
298 assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>" |
298 assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>" |
299 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
299 and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>" |
300 shows "I. \<lbrace>P\<rbrace> c1 ** c2 \<lbrace>R\<rbrace>" |
300 shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>" |
301 using h1 h2 |
301 using h1 h2 |
302 by (smt IHoare_def sep_exec.composition) |
302 by (smt IHoare_def sep_exec.composition) |
303 |
303 |
304 lemma pre_condI: |
304 lemma pre_condI: |
305 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |
305 assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" |