14 |
14 |
15 theory Separation imports Hoare_Logic_Abort SepLogHeap begin |
15 theory Separation imports Hoare_Logic_Abort SepLogHeap begin |
16 |
16 |
17 text{* The semantic definition of a few connectives: *} |
17 text{* The semantic definition of a few connectives: *} |
18 |
18 |
19 constdefs |
19 definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) where |
20 ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) |
|
21 "h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}" |
20 "h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}" |
22 |
21 |
23 is_empty :: "heap \<Rightarrow> bool" |
22 definition is_empty :: "heap \<Rightarrow> bool" where |
24 "is_empty h == h = empty" |
23 "is_empty h == h = empty" |
25 |
24 |
26 singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
25 definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
27 "singl h x y == dom h = {x} & h x = Some y" |
26 "singl h x y == dom h = {x} & h x = Some y" |
28 |
27 |
29 star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
28 definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where |
30 "star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2" |
29 "star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2" |
31 |
30 |
32 wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
31 definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where |
33 "wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')" |
32 "wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')" |
34 |
33 |
35 text{*This is what assertions look like without any syntactic sugar: *} |
34 text{*This is what assertions look like without any syntactic sugar: *} |
36 |
35 |
37 lemma "VARS x y z w h |
36 lemma "VARS x y z w h |