--- a/ROOT	Fri Sep 12 00:47:15 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-session "Hoare_gen" in "thys" = "HOL" +
-  theories 
-     Hoare_gen
-
-session "Hoare_tm" in "thys" = "Hoare_gen" +
-  theories 
-     Hoare_tm
-     Hoare_tm2
-
-session "Hoare_abc" in "thys" = "Hoare_tm" +
-  theories
-     Hoare_abc
-     Hoare_abc2
-
-session "TM" in "thys" = Hoare_abc +
-  theories 
-    My_block
-    LetElim
-    StateMonad
-    TM_Assemble
-
-session "Paper" in "paper" = TM +
-  options [document = pdf, document_output = "..", document_variants = "journal"]
-  theories
-    Paper
-  files "document/root.tex"
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Map_Extra.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,573 @@
+(* Author: Rafal Kolanski, 2008
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header {* More properties of maps plus map disjuction. *}
+
+theory Map_Extra
+  imports Main
+begin
+
+text {*
+  A note on naming:
+  Anything not involving heap disjuction can potentially be incorporated
+  directly into Map.thy, thus uses @{text "m"} for map variable names.
+  Anything involving heap disjunction is not really mergeable with Map, is
+  destined for use in separation logic, and hence uses @{text "h"}
+*}
+
+section {* Things that could go into Option Type *}
+
+text {* Misc option lemmas *}
+
+lemma None_not_eq: "(None \<noteq> x) = (\<exists>y. x = Some y)" by (cases x) auto
+
+lemma None_com: "(None = x) = (x = None)" by fast
+
+lemma Some_com: "(Some y = x) = (x = Some y)" by fast
+
+
+section {* Things that go into Map.thy *}
+
+text {* Map intersection: set of all keys for which the maps agree. *}
+
+definition
+  map_inter :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" (infixl "\<inter>\<^isub>m" 70) where
+  "m\<^isub>1 \<inter>\<^isub>m m\<^isub>2 \<equiv> {x \<in> dom m\<^isub>1. m\<^isub>1 x = m\<^isub>2 x}"
+
+text {* Map restriction via domain subtraction *}
+
+definition
+  sub_restrict_map :: "('a \<rightharpoonup> 'b) => 'a set => ('a \<rightharpoonup> 'b)" (infixl "`-"  110)
+  where
+  "m `- S \<equiv> (\<lambda>x. if x \<in> S then None else m x)"
+
+
+subsection {* Properties of maps not related to restriction *}
+
+lemma empty_forall_equiv: "(m = empty) = (\<forall>x. m x = None)"
+  by (fastforce intro!: ext)
+
+lemma map_le_empty2 [simp]:
+  "(m \<subseteq>\<^sub>m empty) = (m = empty)"
+  by (auto simp: map_le_def intro: ext)
+
+lemma dom_iff:
+  "(\<exists>y. m x = Some y) = (x \<in> dom m)"
+  by auto
+
+lemma non_dom_eval:
+  "x \<notin> dom m \<Longrightarrow> m x = None"
+  by auto
+
+lemma non_dom_eval_eq:
+  "x \<notin> dom m = (m x = None)"
+  by auto
+
+lemma map_add_same_left_eq:
+  "m\<^isub>1 = m\<^isub>1' \<Longrightarrow> (m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0 ++ m\<^isub>1')"
+  by simp
+
+lemma map_add_left_cancelI [intro!]:
+  "m\<^isub>1 = m\<^isub>1' \<Longrightarrow> m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0 ++ m\<^isub>1'"
+  by simp
+
+lemma dom_empty_is_empty:
+  "(dom m = {}) = (m = empty)"
+proof (rule iffI)
+  assume a: "dom m = {}"
+  { assume "m \<noteq> empty"
+    hence "dom m \<noteq> {}"
+      by - (subst (asm) empty_forall_equiv, simp add: dom_def)
+    hence False using a by blast
+  }
+  thus "m = empty" by blast
+next
+  assume a: "m = empty"
+  thus "dom m = {}" by simp
+qed
+
+lemma map_add_dom_eq:
+  "dom m = dom m' \<Longrightarrow> m ++ m' = m'"
+  by (rule ext) (auto simp: map_add_def split: option.splits)
+
+lemma map_add_right_dom_eq:
+  "\<lbrakk> m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0' ++ m\<^isub>1'; dom m\<^isub>1 = dom m\<^isub>1' \<rbrakk> \<Longrightarrow> m\<^isub>1 = m\<^isub>1'"
+  unfolding map_add_def
+  by (rule ext, rule ccontr,
+      drule_tac x=x in fun_cong, clarsimp split: option.splits,
+      drule sym, drule sym, force+)
+
+lemma map_le_same_dom_eq:
+  "\<lbrakk> m\<^isub>0 \<subseteq>\<^sub>m m\<^isub>1 ; dom m\<^isub>0 = dom m\<^isub>1 \<rbrakk> \<Longrightarrow> m\<^isub>0 = m\<^isub>1"
+  by (auto intro!: ext simp: map_le_def elim!: ballE)
+
+
+subsection {* Properties of map restriction *}
+
+lemma restrict_map_cancel:
+  "(m |` S = m |` T) = (dom m \<inter> S = dom m \<inter> T)"
+  by (fastforce intro: ext dest: fun_cong
+               simp: restrict_map_def None_not_eq
+               split: split_if_asm)
+
+lemma map_add_restricted_self [simp]:
+  "m ++ m |` S = m"
+  by (auto intro: ext simp: restrict_map_def map_add_def split: option.splits)
+
+lemma map_add_restrict_dom_right [simp]:
+  "(m ++ m') |` dom m' = m'"
+  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
+
+lemma restrict_map_UNIV [simp]:
+  "m |` UNIV = m"
+  by (simp add: restrict_map_def)
+
+lemma restrict_map_dom:
+  "S = dom m \<Longrightarrow> m |` S = m"
+  by (auto intro!: ext simp: restrict_map_def None_not_eq)
+
+lemma restrict_map_subdom:
+  "dom m \<subseteq> S \<Longrightarrow> m |` S = m"
+  by (fastforce simp: restrict_map_def None_com intro: ext)
+
+lemma map_add_restrict:
+  "(m\<^isub>0 ++ m\<^isub>1) |` S = ((m\<^isub>0 |` S) ++ (m\<^isub>1 |` S))"
+  by (force simp: map_add_def restrict_map_def intro: ext)
+
+lemma map_le_restrict:
+  "m \<subseteq>\<^sub>m m' \<Longrightarrow> m = m' |` dom m"
+  by (force simp: map_le_def restrict_map_def None_com intro: ext)
+
+lemma restrict_map_le:
+  "m |` S \<subseteq>\<^sub>m m"
+  by (auto simp: map_le_def)
+
+lemma restrict_map_remerge:
+  "\<lbrakk> S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m |` (S \<union> T)"
+  by (rule ext, clarsimp simp: restrict_map_def map_add_def
+                         split: option.splits)
+
+lemma restrict_map_empty:
+  "dom m \<inter> S = {} \<Longrightarrow> m |` S = empty"
+  by (fastforce simp: restrict_map_def intro: ext)
+
+lemma map_add_restrict_comp_right [simp]:
+  "(m |` S ++ m |` (UNIV - S)) = m"
+  by (force simp: map_add_def restrict_map_def split: option.splits intro: ext)
+
+lemma map_add_restrict_comp_right_dom [simp]:
+  "(m |` S ++ m |` (dom m - S)) = m"
+  by (auto simp: map_add_def restrict_map_def split: option.splits intro!: ext)
+
+lemma map_add_restrict_comp_left [simp]:
+  "(m |` (UNIV - S) ++ m |` S) = m"
+  by (subst map_add_comm, auto)
+
+lemma restrict_self_UNIV:
+  "m |` (dom m - S) = m |` (UNIV - S)"
+  by (auto intro!: ext simp: restrict_map_def)
+
+lemma map_add_restrict_nonmember_right:
+  "x \<notin> dom m' \<Longrightarrow> (m ++ m') |` {x} = m |` {x}"
+  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
+
+lemma map_add_restrict_nonmember_left:
+  "x \<notin> dom m \<Longrightarrow> (m ++ m') |` {x} = m' |` {x}"
+  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
+
+lemma map_add_restrict_right:
+  "x \<subseteq> dom m' \<Longrightarrow> (m ++ m') |` x = m' |` x"
+  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
+
+lemma restrict_map_compose:
+  "\<lbrakk> S \<union> T = dom m ; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m"
+  by (fastforce intro: ext simp: map_add_def restrict_map_def)
+
+lemma map_le_dom_subset_restrict:
+  "\<lbrakk> m' \<subseteq>\<^sub>m m; dom m' \<subseteq> S \<rbrakk> \<Longrightarrow> m' \<subseteq>\<^sub>m (m |` S)"
+  by (force simp: restrict_map_def map_le_def)
+
+lemma map_le_dom_restrict_sub_add:
+  "m' \<subseteq>\<^sub>m m \<Longrightarrow> m |` (dom m - dom m') ++ m' = m"
+  by (auto simp: None_com map_add_def restrict_map_def map_le_def
+           split: option.splits
+           intro!: ext)
+     (force simp: Some_com)+
+
+lemma subset_map_restrict_sub_add:
+  "T \<subseteq> S \<Longrightarrow> m |` (S - T) ++ m |` T = m |` S"
+  by (auto simp: restrict_map_def map_add_def intro!: ext split: option.splits)
+
+lemma restrict_map_sub_union:
+  "m |` (dom m - (S \<union> T)) = (m |` (dom m - T)) |` (dom m - S)"
+  by (auto intro!: ext simp: restrict_map_def)
+
+lemma prod_restrict_map_add:
+  "\<lbrakk> S \<union> T = U; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` (X \<times> S) ++ m |` (X \<times> T) = m |` (X \<times> U)"
+  by (auto simp: map_add_def restrict_map_def intro!: ext split: option.splits)
+
+
+section {* Things that should not go into Map.thy (separation logic) *}
+
+subsection {* Definitions *}
+
+text {* Map disjuction *}
+
+definition
+  map_disj :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<bottom>" 51) where
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<equiv> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}"
+
+declare None_not_eq [simp]
+
+
+subsection {* Properties of @{term "sub_restrict_map"} *}
+
+lemma restrict_map_sub_disj: "h |` S \<bottom> h `- S"
+  by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def
+               split: option.splits split_if_asm)
+
+lemma restrict_map_sub_add: "h |` S ++ h `- S = h"
+  by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def
+               split: option.splits split_if
+               intro: ext)
+
+
+subsection {* Properties of map disjunction *}
+
+lemma map_disj_empty_right [simp]:
+  "h \<bottom> empty"
+  by (simp add: map_disj_def)
+
+lemma map_disj_empty_left [simp]:
+  "empty \<bottom> h"
+  by (simp add: map_disj_def)
+
+lemma map_disj_com:
+  "h\<^isub>0 \<bottom> h\<^isub>1 = h\<^isub>1 \<bottom> h\<^isub>0"
+  by (simp add: map_disj_def, fast)
+
+lemma map_disjD:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}"
+  by (simp add: map_disj_def)
+
+lemma map_disjI:
+  "dom h\<^isub>0 \<inter> dom h\<^isub>1 = {} \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1"
+  by (simp add: map_disj_def)
+
+
+subsection {* Map associativity-commutativity based on map disjuction *}
+
+lemma map_add_com:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 ++ h\<^isub>1 = h\<^isub>1 ++ h\<^isub>0"
+  by (drule map_disjD, rule map_add_comm, force)
+
+lemma map_add_left_commute:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 ++ (h\<^isub>1 ++ h\<^isub>2) = h\<^isub>1 ++ (h\<^isub>0 ++ h\<^isub>2)"
+  by (simp add: map_add_com map_disj_com map_add_assoc)
+
+lemma map_add_disj:
+  "h\<^isub>0 \<bottom> (h\<^isub>1 ++ h\<^isub>2) = (h\<^isub>0 \<bottom> h\<^isub>1 \<and> h\<^isub>0 \<bottom> h\<^isub>2)"
+  by (simp add: map_disj_def, fast)
+
+lemma map_add_disj':
+  "(h\<^isub>1 ++ h\<^isub>2) \<bottom> h\<^isub>0 = (h\<^isub>1 \<bottom> h\<^isub>0 \<and> h\<^isub>2 \<bottom> h\<^isub>0)"
+  by (simp add: map_disj_def, fast)
+
+text {*
+  We redefine @{term "map_add"} associativity to bind to the right, which
+  seems to be the more common case.
+  Note that when a theory includes Map again, @{text "map_add_assoc"} will
+  return to the simpset and will cause infinite loops if its symmetric
+  counterpart is added (e.g. via @{text "map_add_ac"})
+  *}
+
+declare map_add_assoc [simp del]
+
+text {*
+  Since the associativity-commutativity of @{term "map_add"} relies on
+  map disjunction, we include some basic rules into the ac set.
+  *}
+
+lemmas map_add_ac =
+  map_add_assoc[symmetric] map_add_com map_disj_com
+  map_add_left_commute map_add_disj map_add_disj'
+
+
+subsection {* Basic properties *}
+
+lemma map_disj_None_right:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; x \<in> dom h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>1 x = None"
+  by (auto simp: map_disj_def dom_def)
+
+lemma map_disj_None_left:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; x \<in> dom h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 x = None"
+  by (auto simp: map_disj_def dom_def)
+
+lemma map_disj_None_left':
+  "\<lbrakk> h\<^isub>0 x = Some y ; h\<^isub>1 \<bottom> h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>1 x = None "
+  by (auto simp: map_disj_def)
+
+lemma map_disj_None_right':
+  "\<lbrakk> h\<^isub>1 x = Some y ; h\<^isub>1 \<bottom> h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0 x = None "
+  by (auto simp: map_disj_def)
+
+lemma map_disj_common:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>0 p = Some v ; h\<^isub>1 p = Some v' \<rbrakk> \<Longrightarrow> False"
+  by (frule (1) map_disj_None_left', simp)
+
+lemma map_disj_eq_dom_left:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; dom h\<^isub>0' = dom h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0' \<bottom> h\<^isub>1"
+  by (auto simp: map_disj_def)
+
+
+subsection {* Map disjunction and addition *}
+
+lemma map_add_eval_left:
+  "\<lbrakk> x \<in> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x"
+  by (auto dest!: map_disj_None_right simp: map_add_def cong: option.case_cong)
+
+lemma map_add_eval_right:
+  "\<lbrakk> x \<in> dom h' ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x"
+  by (auto elim!: map_disjD simp: map_add_comm map_add_eval_left map_disj_com)
+
+lemma map_add_eval_left':
+  "\<lbrakk> x \<notin> dom h' ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x"
+  by (clarsimp simp: map_disj_def map_add_def split: option.splits)
+
+lemma map_add_eval_right':
+  "\<lbrakk> x \<notin> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x"
+  by (clarsimp simp: map_disj_def map_add_def split: option.splits)
+
+lemma map_add_left_dom_eq:
+  assumes eq: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'"
+  assumes etc: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0' \<bottom> h\<^isub>1'" "dom h\<^isub>0 = dom h\<^isub>0'"
+  shows "h\<^isub>0 = h\<^isub>0'"
+proof -
+  from eq have "h\<^isub>1 ++ h\<^isub>0 = h\<^isub>1' ++ h\<^isub>0'" using etc by (simp add: map_add_ac)
+  thus ?thesis using etc
+    by (fastforce elim!: map_add_right_dom_eq simp: map_add_ac)
+qed
+
+lemma map_add_left_eq:
+  assumes eq: "h\<^isub>0 ++ h = h\<^isub>1 ++ h"
+  assumes disj: "h\<^isub>0 \<bottom> h" "h\<^isub>1 \<bottom> h"
+  shows "h\<^isub>0 = h\<^isub>1"
+proof (rule ext)
+  fix x
+  from eq have eq': "(h\<^isub>0 ++ h) x = (h\<^isub>1 ++ h) x" by (auto intro!: ext)
+  { assume "x \<in> dom h"
+    hence "h\<^isub>0 x = h\<^isub>1 x" using disj by (simp add: map_disj_None_left)
+  } moreover {
+    assume "x \<notin> dom h"
+    hence "h\<^isub>0 x = h\<^isub>1 x" using disj eq' by (simp add: map_add_eval_left')
+  }
+  ultimately show "h\<^isub>0 x = h\<^isub>1 x" by cases
+qed
+
+lemma map_add_right_eq:
+  "\<lbrakk>h ++ h\<^isub>0 = h ++ h\<^isub>1; h\<^isub>0 \<bottom> h; h\<^isub>1 \<bottom> h\<rbrakk> \<Longrightarrow> h\<^isub>0 = h\<^isub>1"
+  by (rule_tac h=h in map_add_left_eq, auto simp: map_add_ac)
+
+lemma map_disj_add_eq_dom_right_eq:
+  assumes merge: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'" and d: "dom h\<^isub>0 = dom h\<^isub>0'" and
+      ab_disj: "h\<^isub>0 \<bottom> h\<^isub>1" and cd_disj: "h\<^isub>0' \<bottom> h\<^isub>1'"
+  shows "h\<^isub>1 = h\<^isub>1'"
+proof (rule ext)
+  fix x
+  from merge have merge_x: "(h\<^isub>0 ++ h\<^isub>1) x = (h\<^isub>0' ++ h\<^isub>1') x" by simp
+  with d ab_disj cd_disj show  "h\<^isub>1 x = h\<^isub>1' x"
+    by - (case_tac "h\<^isub>1 x", case_tac "h\<^isub>1' x", simp, fastforce simp: map_disj_def,
+          case_tac "h\<^isub>1' x", clarsimp, simp add: Some_com,
+          force simp: map_disj_def, simp)
+qed
+
+lemma map_disj_add_eq_dom_left_eq:
+  assumes add: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'" and
+          dom: "dom h\<^isub>1 = dom h\<^isub>1'" and
+          disj: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0' \<bottom> h\<^isub>1'"
+  shows "h\<^isub>0 = h\<^isub>0'"
+proof -
+  have "h\<^isub>1 ++ h\<^isub>0 = h\<^isub>1' ++ h\<^isub>0'" using add disj by (simp add: map_add_ac)
+  thus ?thesis using dom disj
+    by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com)
+qed
+
+lemma map_add_left_cancel:
+  assumes disj: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0 \<bottom> h\<^isub>1'"
+  shows "(h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0 ++ h\<^isub>1') = (h\<^isub>1 = h\<^isub>1')"
+proof (rule iffI, rule ext)
+  fix x
+  assume "(h\<^isub>0 ++ h\<^isub>1) = (h\<^isub>0 ++ h\<^isub>1')"
+  hence "(h\<^isub>0 ++ h\<^isub>1) x = (h\<^isub>0 ++ h\<^isub>1') x" by (auto intro!: ext)
+  hence "h\<^isub>1 x = h\<^isub>1' x" using disj
+    by - (cases "x \<in> dom h\<^isub>0",
+          simp_all add: map_disj_None_right map_add_eval_right')
+  thus "h\<^isub>1 x = h\<^isub>1' x" by (auto intro!: ext)
+qed auto
+
+lemma map_add_lr_disj:
+  "\<lbrakk> h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'; h\<^isub>1 \<bottom> h\<^isub>1'  \<rbrakk> \<Longrightarrow> dom h\<^isub>1 \<subseteq> dom h\<^isub>0'"
+  by (clarsimp simp: map_disj_def map_add_def, drule_tac x=x in fun_cong)
+     (auto split: option.splits)
+
+
+subsection {* Map disjunction and map updates *}
+
+lemma map_disj_update_left [simp]:
+  "p \<in> dom h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1(p \<mapsto> v) = h\<^isub>0 \<bottom> h\<^isub>1"
+  by (clarsimp simp add: map_disj_def, blast)
+
+lemma map_disj_update_right [simp]:
+  "p \<in> dom h\<^isub>1 \<Longrightarrow> h\<^isub>1(p \<mapsto> v) \<bottom> h\<^isub>0 = h\<^isub>1 \<bottom> h\<^isub>0"
+  by (simp add: map_disj_com)
+
+lemma map_add_update_left:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; p \<in> dom h\<^isub>0 \<rbrakk> \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1)(p \<mapsto> v) = (h\<^isub>0(p \<mapsto> v) ++ h\<^isub>1)"
+  by (drule (1) map_disj_None_right)
+     (auto intro: ext simp: map_add_def cong: option.case_cong)
+
+lemma map_add_update_right:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; p \<in> dom h\<^isub>1  \<rbrakk> \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1)(p \<mapsto> v) = (h\<^isub>0 ++ h\<^isub>1 (p \<mapsto> v))"
+  by (drule (1) map_disj_None_left)
+     (auto intro: ext simp: map_add_def cong: option.case_cong)
+
+lemma map_add3_update:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>1  \<bottom> h\<^isub>2 ; h\<^isub>0 \<bottom> h\<^isub>2 ; p \<in> dom h\<^isub>0 \<rbrakk>
+  \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1 ++ h\<^isub>2)(p \<mapsto> v) = h\<^isub>0(p \<mapsto> v) ++ h\<^isub>1 ++ h\<^isub>2"
+  by (auto simp: map_add_update_left[symmetric] map_add_ac)
+
+
+subsection {* Map disjunction and @{term "map_le"} *}
+
+lemma map_le_override [simp]:
+  "\<lbrakk> h \<bottom> h' \<rbrakk> \<Longrightarrow> h \<subseteq>\<^sub>m h ++ h'"
+  by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)
+
+lemma map_leI_left:
+  "\<lbrakk> h = h\<^isub>0 ++ h\<^isub>1 ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h" by auto
+
+lemma map_leI_right:
+  "\<lbrakk> h = h\<^isub>0 ++ h\<^isub>1 ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>1 \<subseteq>\<^sub>m h" by auto
+
+lemma map_disj_map_le:
+  "\<lbrakk> h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0' \<bottom> h\<^isub>1"
+  by (force simp: map_disj_def map_le_def)
+
+lemma map_le_on_disj_left:
+  "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 ; h' = h\<^isub>0 ++ h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h"
+  unfolding map_le_def
+  by (rule ballI, erule_tac x=a in ballE, auto simp: map_add_eval_left)+
+
+lemma map_le_on_disj_right:
+  "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 ; h' = h\<^isub>1 ++ h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h"
+  by (auto simp: map_le_on_disj_left map_add_ac)
+
+lemma map_le_add_cancel:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0' ++ h\<^isub>1 \<subseteq>\<^sub>m h\<^isub>0 ++ h\<^isub>1"
+  by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)
+
+lemma map_le_override_bothD:
+  assumes subm: "h\<^isub>0' ++ h\<^isub>1 \<subseteq>\<^sub>m h\<^isub>0 ++ h\<^isub>1"
+  assumes disj': "h\<^isub>0' \<bottom> h\<^isub>1"
+  assumes disj: "h\<^isub>0 \<bottom> h\<^isub>1"
+  shows "h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0"
+unfolding map_le_def
+proof (rule ballI)
+  fix a
+  assume a: "a \<in> dom h\<^isub>0'"
+  hence sumeq: "(h\<^isub>0' ++ h\<^isub>1) a = (h\<^isub>0 ++ h\<^isub>1) a"
+    using subm unfolding map_le_def by auto
+  from a have "a \<notin> dom h\<^isub>1" using disj' by (auto dest!: map_disj_None_right)
+  thus "h\<^isub>0' a = h\<^isub>0 a" using a sumeq disj disj'
+    by (simp add: map_add_eval_left map_add_eval_left')
+qed
+
+lemma map_le_conv:
+  "(h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 \<and> h\<^isub>0' \<noteq> h\<^isub>0) = (\<exists>h\<^isub>1. h\<^isub>0 = h\<^isub>0' ++ h\<^isub>1 \<and> h\<^isub>0' \<bottom> h\<^isub>1 \<and> h\<^isub>0' \<noteq> h\<^isub>0)"
+  unfolding map_le_def map_disj_def map_add_def
+  by (rule iffI,
+      clarsimp intro!: exI[where x="\<lambda>x. if x \<notin> dom h\<^isub>0' then h\<^isub>0 x else None"])
+     (fastforce intro: ext intro: split: option.splits split_if_asm)+
+
+lemma map_le_conv2:
+  "h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 = (\<exists>h\<^isub>1. h\<^isub>0 = h\<^isub>0' ++ h\<^isub>1 \<and> h\<^isub>0' \<bottom> h\<^isub>1)"
+  by (case_tac "h\<^isub>0'=h\<^isub>0", insert map_le_conv, auto intro: exI[where x=empty])
+
+
+subsection {* Map disjunction and restriction *}
+
+lemma map_disj_comp [simp]:
+  "h\<^isub>0 \<bottom> h\<^isub>1 |` (UNIV - dom h\<^isub>0)"
+  by (force simp: map_disj_def)
+
+lemma restrict_map_disj:
+  "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h |` T"
+  by (auto simp: map_disj_def restrict_map_def dom_def)
+
+lemma map_disj_restrict_dom [simp]:
+  "h\<^isub>0 \<bottom> h\<^isub>1 |` (dom h\<^isub>1 - dom h\<^isub>0)"
+  by (force simp: map_disj_def)
+
+lemma restrict_map_disj_dom_empty:
+  "h \<bottom> h' \<Longrightarrow> h |` dom h' = empty"
+  by (fastforce simp: map_disj_def restrict_map_def intro: ext)
+
+lemma restrict_map_univ_disj_eq:
+  "h \<bottom> h' \<Longrightarrow> h |` (UNIV - dom h') = h"
+  by (rule ext, auto simp: map_disj_def restrict_map_def)
+
+lemma restrict_map_disj_dom:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h |` dom h\<^isub>0 \<bottom> h |` dom h\<^isub>1"
+  by (auto simp: map_disj_def restrict_map_def dom_def)
+
+lemma map_add_restrict_dom_left:
+  "h \<bottom> h' \<Longrightarrow> (h ++ h') |` dom h = h"
+  by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
+                     split: option.splits)
+
+lemma map_add_restrict_dom_left':
+  "h \<bottom> h' \<Longrightarrow> S = dom h \<Longrightarrow> (h ++ h') |` S = h"
+  by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
+                     split: option.splits)
+
+lemma restrict_map_disj_left:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 |` S \<bottom> h\<^isub>1"
+  by (auto simp: map_disj_def)
+
+lemma restrict_map_disj_right:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1 |` S"
+  by (auto simp: map_disj_def)
+
+lemmas restrict_map_disj_both = restrict_map_disj_right restrict_map_disj_left
+
+lemma map_dom_disj_restrict_right:
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>0') |` dom h\<^isub>1 = h\<^isub>0' |` dom h\<^isub>1"
+  by (simp add: map_add_restrict restrict_map_empty map_disj_def)
+
+lemma restrict_map_on_disj:
+  "h\<^isub>0' \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 |` dom h\<^isub>0' \<bottom> h\<^isub>1"
+  unfolding map_disj_def by auto
+
+lemma restrict_map_on_disj':
+  "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1 |` S"
+  by (auto simp: map_disj_def map_add_def)
+
+lemma map_le_sub_dom:
+  "\<lbrakk> h\<^isub>0 ++ h\<^isub>1 \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h |` (dom h - dom h\<^isub>1)"
+  by (rule map_le_override_bothD, subst map_le_dom_restrict_sub_add)
+     (auto elim: map_add_le_mapE simp: map_add_ac)
+
+lemma map_submap_break:
+  "\<lbrakk> h \<subseteq>\<^sub>m h' \<rbrakk> \<Longrightarrow> h' = (h' |` (UNIV - dom h)) ++ h"
+  by (fastforce intro!: ext split: option.splits
+               simp: map_le_restrict restrict_map_def map_le_def map_add_def
+                     dom_def)
+
+lemma map_add_disj_restrict_both:
+  "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1; S \<inter> S' = {}; T \<inter> T' = {} \<rbrakk>
+   \<Longrightarrow> (h\<^isub>0 |` S) ++ (h\<^isub>1 |` T) \<bottom> (h\<^isub>0 |` S') ++ (h\<^isub>1 |` T')"
+  by (auto simp: map_add_ac intro!: restrict_map_disj_both restrict_map_disj)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/README	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,11 @@
+This directory contains a generic type class implementation of separation
+algebra for Isabelle/HOL as well as lemmas and generic tactics which can be
+used directly for any instantiation of the type class.
+
+The ex directory contains example instantiations that include structures such
+as a heap or virtual memory.
+
+The abstract separation algebra is based upon "Abstract Separation Logic" by
+Calcagno et al. These theories are also the basis of "Mechanised Separation
+Algebra" by Klein et al.
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ROOT	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,11 @@
+session Separation_Algebra (AFP) = "HOL-Word" +
+  options [timeout = 3600]
+  theories
+    "ex/Simple_Separation_Example"
+    "ex/Sep_Tactics_Test"
+    "ex/VM_Example"
+    Sep_Eq
+    "ex/capDL/Separation_D"
+  files
+    "document/root.bib"
+    "document/root.tex"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Sep_Eq.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,108 @@
+(* Author: Gerwin Klein, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Equivalence between Separation Algebra Formulations"
+
+theory Sep_Eq
+imports Separation_Algebra Separation_Algebra_Alt
+begin
+
+text {*
+  In this theory we show that our total formulation of separation algebra is
+  equivalent in strength to Calcagno et al's original partial one.
+
+  This theory is not intended to be included in own developments.
+*}
+
+no_notation map_add (infixl "++" 100)
+
+section "Total implies Partial"
+
+definition add2 :: "'a::sep_algebra => 'a => 'a option" where
+  "add2 x y \<equiv> if x ## y then Some (x + y) else None"
+
+lemma add2_zero: "add2 x 0 = Some x"
+  by (simp add: add2_def)
+
+lemma add2_comm: "add2 x y = add2 y x"
+  by (auto simp: add2_def sep_add_commute sep_disj_commute)
+
+lemma add2_assoc:
+  "lift2 add2 a (lift2 add2 b c) = lift2 add2 (lift2 add2 a b) c"
+  by (auto simp: add2_def lift2_def sep_add_assoc
+              dest: sep_disj_addD sep_disj_addI3
+                    sep_add_disjD sep_disj_addI2 sep_disj_commuteI
+              split: option.splits)
+
+interpretation total_partial: sep_algebra_alt 0 add2
+  by (unfold_locales) (auto intro: add2_zero add2_comm add2_assoc)
+
+
+section "Partial implies Total"
+
+definition
+  sep_add' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a :: sep_algebra_alt" where
+  "sep_add' x y \<equiv> if disjoint x y then the (add x y) else undefined"
+
+lemma sep_disj_zero':
+  "disjoint x 0"
+  by simp
+
+lemma sep_disj_commuteI':
+  "disjoint x y \<Longrightarrow> disjoint y x"
+  by (clarsimp simp: disjoint_def add_comm)
+
+lemma sep_add_zero':
+  "sep_add' x 0 = x"
+  by (simp add: sep_add'_def)
+
+lemma sep_add_commute':
+  "disjoint x y \<Longrightarrow> sep_add' x y = sep_add' y x"
+  by (clarsimp simp: sep_add'_def disjoint_def add_comm)
+
+lemma sep_add_assoc':
+  "\<lbrakk> disjoint x y; disjoint y z; disjoint x z \<rbrakk> \<Longrightarrow>
+  sep_add' (sep_add' x y) z = sep_add' x (sep_add' y z)"
+  using add_assoc [of "Some x" "Some y" "Some z"]
+  by (clarsimp simp: disjoint_def sep_add'_def lift2_def
+               split: option.splits)
+
+lemma sep_disj_addD1':
+  "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint x y"
+proof (clarsimp simp: disjoint_def sep_add'_def)
+  fix a assume a: "y \<oplus> z = Some a"
+  fix b assume b: "x \<oplus> a = Some b"
+  with a have "Some x ++ (Some y ++ Some z) = Some b" by (simp add: lift2_def)
+  hence "(Some x ++ Some y) ++ Some z = Some b" by (simp add: add_assoc)
+  thus "\<exists>b. x \<oplus> y = Some b" by (simp add: lift2_def split: option.splits)
+qed
+
+lemma sep_disj_addI1':
+  "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint (sep_add' x y) z"
+  apply (clarsimp simp: disjoint_def sep_add'_def)
+  apply (rule conjI)
+   apply clarsimp
+   apply (frule lift_to_add2, assumption)
+   apply (simp add: add_assoc)
+   apply (clarsimp simp: lift2_def add_comm)
+  apply clarsimp
+  apply (frule lift_to_add2, assumption)
+  apply (simp add: add_assoc)
+  apply (clarsimp simp: lift2_def)
+  done
+
+interpretation partial_total: sep_algebra sep_add' 0 disjoint
+  apply (unfold_locales)
+        apply (rule sep_disj_zero')
+       apply (erule sep_disj_commuteI')
+      apply (rule sep_add_zero')
+     apply (erule sep_add_commute')
+    apply (erule (2) sep_add_assoc')
+   apply (erule (1) sep_disj_addD1')
+  apply (erule (1) sep_disj_addI1')
+  done
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Sep_Heap_Instance.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,84 @@
+(* Author: Gerwin Klein, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Standard Heaps as an Instance of Separation Algebra"
+
+theory Sep_Heap_Instance
+imports Separation_Algebra
+begin
+
+text {*
+  Example instantiation of a the separation algebra to a map, i.e.\ a
+  function from any type to @{typ "'a option"}.
+*}
+
+class opt =
+  fixes none :: 'a
+begin
+  definition "domain f \<equiv> {x. f x \<noteq> none}"
+end
+
+instantiation option :: (type) opt
+begin
+  definition none_def [simp]: "none \<equiv> None"
+  instance ..
+end
+
+instantiation "fun" :: (type, opt) zero
+begin
+  definition zero_fun_def: "0 \<equiv> \<lambda>s. none"
+  instance ..
+end
+
+instantiation "fun" :: (type, opt) sep_algebra
+begin
+
+definition
+  plus_fun_def: "m1 + m2 \<equiv> \<lambda>x. if m2 x = none then m1 x else m2 x"
+
+definition
+  sep_disj_fun_def: "sep_disj m1 m2 \<equiv> domain m1 \<inter> domain m2 = {}"
+
+instance
+  apply default
+        apply (simp add: sep_disj_fun_def domain_def zero_fun_def)
+       apply (fastforce simp: sep_disj_fun_def)
+      apply (simp add: plus_fun_def zero_fun_def)
+     apply (simp add: plus_fun_def sep_disj_fun_def domain_def)
+     apply (rule ext)
+     apply fastforce
+    apply (rule ext)
+    apply (simp add: plus_fun_def)
+   apply (simp add: sep_disj_fun_def domain_def plus_fun_def)
+   apply fastforce
+  apply (simp add: sep_disj_fun_def domain_def plus_fun_def)
+  apply fastforce
+  done
+
+end
+
+text {*
+  For the actual option type @{const domain} and @{text "+"} are
+  just @{const dom} and @{text "++"}:
+*}
+
+lemma domain_conv: "domain = dom"
+  by (rule ext) (simp add: domain_def dom_def)
+
+lemma plus_fun_conv: "a + b = a ++ b"
+  by (auto simp: plus_fun_def map_add_def split: option.splits)
+
+lemmas map_convs = domain_conv plus_fun_conv
+
+text {*
+  Any map can now act as a separation heap without further work:
+*}
+lemma
+  fixes h :: "(nat => nat) => 'foo option"
+  shows "(P ** Q ** H) h = (Q ** H ** P) h"
+  by (simp add: sep_conj_ac)
+
+end
+

--- a/Separation_Algebra/Sep_Tactics.thy	Fri Sep 12 00:47:15 2014 +0800
+++ b/Separation_Algebra/Sep_Tactics.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -6,50 +6,78 @@
 header "Separation Logic Tactics"
 
 theory Sep_Tactics
-imports Separation_Algebra
+imports Separation_Algebra 
+uses "sep_tactics.ML"
 begin
 
-ML_file "sep_tactics.ML"
 
 text {* A number of proof methods to assist with reasoning about separation logic. *}
 
 
 section {* Selection (move-to-front) tactics *}
 
+ML {*
+  fun sep_select_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_tac ctxt n);
+  fun sep_select_asm_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n);
+*}
+
 method_setup sep_select = {*
-  Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_tac ctxt n))
+  Scan.lift Parse.int >> sep_select_method
 *} "Select nth separation conjunct in conclusion"
 
 method_setup sep_select_asm = {*
-  Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_asm_tac ctxt n))
+  Scan.lift Parse.int >> sep_select_asm_method
 *} "Select nth separation conjunct in assumptions"
 
 
 section {* Substitution *}
 
+ML {*
+  fun sep_subst_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_tac ctxt occs thms);
+  fun sep_subst_asm_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms);
+
+  val sep_subst_parser =
+        Args.mode "asm"
+        -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])
+        -- Attrib.thms;
+*}
+
 method_setup "sep_subst" = {*
-  Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
-    Attrib.thms >> (fn ((asm, occs), thms) => fn ctxt =>
-      SIMPLE_METHOD' ((if asm then sep_subst_asm_tac else sep_subst_tac) ctxt occs thms))
+  sep_subst_parser >>
+    (fn ((asm, occs), thms) => fn ctxt =>
+      (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms)
 *}
 "single-step substitution after solving one separation logic assumption"
 
 
 section {* Forward Reasoning *}
 
+ML {*
+  fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms);
+  fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms);
+*}
+
 method_setup "sep_drule" = {*
-  Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_dtac ctxt thms))
+  Attrib.thms >> sep_drule_method
 *} "drule after separating conjunction reordering"
 
 method_setup "sep_frule" = {*
-  Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_ftac ctxt thms))
+  Attrib.thms >> sep_frule_method
 *} "frule after separating conjunction reordering"
 
 
 section {* Backward Reasoning *}
 
+ML {*
+  fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms)
+*}
+
 method_setup "sep_rule" = {*
-  Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_rtac ctxt thms))
+  Attrib.thms >> sep_rule_method
 *} "applies rule after separating conjunction reordering"
 
 
@@ -97,31 +125,37 @@
   fun sep_cancel_smart_tac_rules ctxt etacs =
       sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));
 
-  val sep_cancel_syntax = Method.sections [
-    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)] >> K ();
-*}
-
-method_setup sep_cancel = {*
-  sep_cancel_syntax >> (fn _ => fn ctxt =>
+  fun sep_cancel_method ctxt =
     let
       val etacs = map etac (SepCancel_Rules.get ctxt);
     in
       SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)
-    end)
+    end;
+
+  val sep_cancel_syntax = Method.sections [
+    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)];
+*}
+
+method_setup sep_cancel = {*
+  sep_cancel_syntax >> K sep_cancel_method
 *} "Separating conjunction conjunct cancellation"
 
 text {*
   As above, but use blast with a depth limit to figure out where cancellation
   can be done. *}
 
-method_setup sep_cancel_blast = {*
-  sep_cancel_syntax >> (fn _ => fn ctxt =>
+ML {*
+  fun sep_cancel_blast_method ctxt =
     let
       val rules = SepCancel_Rules.get ctxt;
       val tac = Blast.depth_tac (ctxt addIs rules) 10;
     in
       SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)
-    end)
+    end;
+*}
+
+method_setup sep_cancel_blast = {*
+  sep_cancel_syntax >> K sep_cancel_blast_method
 *} "Separating conjunction conjunct cancellation using blast"
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Sep_Tactics.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,161 @@
+(* Authors: Gerwin Klein and Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Separation Logic Tactics"
+
+theory Sep_Tactics
+imports Separation_Algebra
+begin
+
+ML_file "sep_tactics.ML"
+
+text {* A number of proof methods to assist with reasoning about separation logic. *}
+
+
+section {* Selection (move-to-front) tactics *}
+
+ML {*
+  fun sep_select_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_tac ctxt n);
+  fun sep_select_asm_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n);
+*}
+
+method_setup sep_select = {*
+  Scan.lift Parse.int >> sep_select_method
+*} "Select nth separation conjunct in conclusion"
+
+method_setup sep_select_asm = {*
+  Scan.lift Parse.int >> sep_select_asm_method
+*} "Select nth separation conjunct in assumptions"
+
+
+section {* Substitution *}
+
+ML {*
+  fun sep_subst_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_tac ctxt occs thms);
+  fun sep_subst_asm_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms);
+
+  val sep_subst_parser =
+        Args.mode "asm"
+        -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])
+        -- Attrib.thms;
+*}
+
+method_setup "sep_subst" = {*
+  sep_subst_parser >>
+    (fn ((asm, occs), thms) => fn ctxt =>
+      (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms)
+*}
+"single-step substitution after solving one separation logic assumption"
+
+
+section {* Forward Reasoning *}
+
+ML {*
+  fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms);
+  fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms);
+*}
+
+method_setup "sep_drule" = {*
+  Attrib.thms >> sep_drule_method
+*} "drule after separating conjunction reordering"
+
+method_setup "sep_frule" = {*
+  Attrib.thms >> sep_frule_method
+*} "frule after separating conjunction reordering"
+
+
+section {* Backward Reasoning *}
+
+ML {*
+  fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms)
+*}
+
+method_setup "sep_rule" = {*
+  Attrib.thms >> sep_rule_method
+*} "applies rule after separating conjunction reordering"
+
+
+section {* Cancellation of Common Conjuncts via Elimination Rules *}
+
+ML {*
+  structure SepCancel_Rules = Named_Thms (
+    val name = @{binding "sep_cancel"};
+    val description = "sep_cancel rules";
+  );
+*}
+setup SepCancel_Rules.setup
+
+text {*
+  The basic @{text sep_cancel_tac} is minimal. It only eliminates
+  erule-derivable conjuncts between an assumption and the conclusion.
+
+  To have a more useful tactic, we augment it with more logic, to proceed as
+  follows:
+  \begin{itemize}
+  \item try discharge the goal first using @{text tac}
+  \item if that fails, invoke @{text sep_cancel_tac}
+  \item if @{text sep_cancel_tac} succeeds
+    \begin{itemize}
+    \item try to finish off with tac (but ok if that fails)
+    \item try to finish off with @{term sep_true} (but ok if that fails)
+    \end{itemize}
+  \end{itemize}
+  *}
+
+ML {*
+  fun sep_cancel_smart_tac ctxt tac =
+    let fun TRY' tac = tac ORELSE' (K all_tac)
+    in
+      tac
+      ORELSE' (sep_cancel_tac ctxt tac
+               THEN' TRY' tac
+               THEN' TRY' (rtac @{thm TrueI}))
+      ORELSE' (etac @{thm sep_conj_sep_emptyE}
+               THEN' sep_cancel_tac ctxt tac
+               THEN' TRY' tac
+               THEN' TRY' (rtac @{thm TrueI}))
+    end;
+
+  fun sep_cancel_smart_tac_rules ctxt etacs =
+      sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));
+
+  fun sep_cancel_method ctxt =
+    let
+      val etacs = map etac (SepCancel_Rules.get ctxt);
+    in
+      SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)
+    end;
+
+  val sep_cancel_syntax = Method.sections [
+    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)];
+*}
+
+method_setup sep_cancel = {*
+  sep_cancel_syntax >> K sep_cancel_method
+*} "Separating conjunction conjunct cancellation"
+
+text {*
+  As above, but use blast with a depth limit to figure out where cancellation
+  can be done. *}
+
+ML {*
+  fun sep_cancel_blast_method ctxt =
+    let
+      val rules = SepCancel_Rules.get ctxt;
+      val tac = Blast.depth_tac (ctxt addIs rules) 10;
+    in
+      SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)
+    end;
+*}
+
+method_setup sep_cancel_blast = {*
+  sep_cancel_syntax >> K sep_cancel_blast_method
+*} "Separating conjunction conjunct cancellation using blast"
+
+end

--- a/Separation_Algebra/Separation_Algebra.thy	Fri Sep 12 00:47:15 2014 +0800
+++ b/Separation_Algebra/Separation_Algebra.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -35,7 +35,7 @@
   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
 
-(* was an abbreviation *)
+(* abbreviation *)
   definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
   "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
 
@@ -216,6 +216,7 @@
   then obtain x y z where "P x" and "Q y" and "R z"
                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
                       and "h = x + y + z"
+    thm sep_disj_addD
     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
   thus "?lhs h"
     by (metis sep_conj_def sep_disj_addI1)

--- a/Separation_Algebra/Separation_Algebra.thy-orig	Fri Sep 12 00:47:15 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,815 +0,0 @@
-(* Authors: Gerwin Klein and Rafal Kolanski, 2012
-   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
-                Rafal Kolanski <rafal.kolanski at nicta.com.au>
-*)
-
-header "Abstract Separation Algebra"
-
-theory Separation_Algebra
-imports Main
-begin
-
-
-text {* This theory is the main abstract separation algebra development *}
-
-
-section {* Input syntax for lifting boolean predicates to separation predicates *}
-
-abbreviation (input)
-  pred_and :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where
-  "a and b \<equiv> \<lambda>s. a s \<and> b s"
-
-abbreviation (input)
-  pred_or :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "or" 30) where
-  "a or b \<equiv> \<lambda>s. a s \<or> b s"
-
-abbreviation (input)
-  pred_not :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" ("not _" [40] 40) where
-  "not a \<equiv> \<lambda>s. \<not>a s"
-
-abbreviation (input)
-  pred_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "imp" 25) where
-  "a imp b \<equiv> \<lambda>s. a s \<longrightarrow> b s"
-
-abbreviation (input)
-  pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
-  "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
-
-abbreviation (input)
-  pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
-  "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
-
-abbreviation (input)
-  pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where
-  "ALLS x. P x \<equiv> \<lambda>s. \<forall>x. P x s"
-
-
-section {* Associative/Commutative Monoid Basis of Separation Algebras *}
-
-class pre_sep_algebra = zero + plus +
-  fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)
-
-  assumes sep_disj_zero [simp]: "x ## 0"
-  assumes sep_disj_commuteI: "x ## y \<Longrightarrow> y ## x"
-
-  assumes sep_add_zero [simp]: "x + 0 = x"
-  assumes sep_add_commute: "x ## y \<Longrightarrow> x + y = y + x"
-
-  assumes sep_add_assoc:
-    "\<lbrakk> x ## y; y ## z; x ## z \<rbrakk> \<Longrightarrow> (x + y) + z = x + (y + z)"
-begin
-
-lemma sep_disj_commute: "x ## y = y ## x"
-  by (blast intro: sep_disj_commuteI)
-
-lemma sep_add_left_commute:
-  assumes a: "a ## b" "b ## c" "a ## c"
-  shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs")
-proof -
-  have "?lhs = b + a + c" using a
-    by (simp add: sep_add_assoc[symmetric] sep_disj_commute)
-  also have "... = a + b + c" using a
-    by (simp add: sep_add_commute sep_disj_commute)
-  also have "... = ?rhs" using a
-    by (simp add: sep_add_assoc sep_disj_commute)
-  finally show ?thesis .
-qed
-
-lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute
-                    sep_disj_commute (* nearly always necessary *)
-
-end
-
-
-section {* Separation Algebra as Defined by Calcagno et al. *}
-
-class sep_algebra = pre_sep_algebra +
-  assumes sep_disj_addD1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y"
-  assumes sep_disj_addI1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + y ##  z"
-begin
-
-subsection {* Basic Construct Definitions and Abbreviations *}
-
-definition
-  sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "**" 35)
-  where
-  "P ** Q \<equiv> \<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
-
-notation
-  sep_conj (infixr "\<and>*" 35)
-
-definition
-  sep_empty :: "'a \<Rightarrow> bool" ("\<box>") where
-  "\<box> \<equiv> \<lambda>h. h = 0"
-
-definition
-  sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>*" 25)
-  where
-  "P \<longrightarrow>* Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')"
-
-definition
-  sep_substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where
-  "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> x + z = y"
-
-(* We want these to be abbreviations not definitions, because basic True and
-   False will occur by simplification in sep_conj terms *)
-abbreviation
-  "sep_true \<equiv> \<langle>True\<rangle>"
-
-abbreviation
-  "sep_false \<equiv> \<langle>False\<rangle>"
-
-definition
-  sep_list_conj :: "('a \<Rightarrow> bool) list \<Rightarrow> ('a \<Rightarrow> bool)"  ("\<And>* _" [60] 90) where
-  "sep_list_conj Ps \<equiv> foldl (op **) \<box> Ps"
-
-
-subsection {* Disjunction/Addition Properties *}
-
-lemma disjoint_zero_sym [simp]: "0 ## x"
-  by (simp add: sep_disj_commute)
-
-lemma sep_add_zero_sym [simp]: "0 + x = x"
-  by (simp add: sep_add_commute)
-
-lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z"
-  by (metis sep_disj_addD1 sep_add_ac)
-
-lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z"
-  by (metis sep_disj_addD1 sep_disj_addD2)
-
-lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z"
-  by (metis sep_disj_addD sep_disj_commuteI)
-
-lemma sep_disj_addI2:
-  "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y"
-  by (metis sep_add_ac sep_disj_addI1)
-
-lemma sep_add_disjI1:
-  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y"
-  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
-
-lemma sep_add_disjI2:
-  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x"
-  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
-
-lemma sep_disj_addI3:
-   "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z"
-   by (metis sep_add_ac sep_add_disjD sep_add_disjI2)
-
-lemma sep_disj_add:
-  "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z"
-  by (metis sep_disj_addI1 sep_disj_addI3)
-
-
-subsection {* Substate Properties *}
-
-lemma sep_substate_disj_add:
-  "x ## y \<Longrightarrow> x \<preceq> x + y"
-  unfolding sep_substate_def by blast
-
-lemma sep_substate_disj_add':
-  "x ## y \<Longrightarrow> x \<preceq> y + x"
-  by (simp add: sep_add_ac sep_substate_disj_add)
-
-
-subsection {* Separating Conjunction Properties *}
-
-lemma sep_conjD:
-  "(P \<and>* Q) h \<Longrightarrow> \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
-  by (simp add: sep_conj_def)
-
-lemma sep_conjE:
-  "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"
-  by (auto simp: sep_conj_def)
-
-lemma sep_conjI:
-  "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h"
-  by (auto simp: sep_conj_def)
-
-lemma sep_conj_commuteI:
-  "(P ** Q) h \<Longrightarrow> (Q ** P) h"
-  by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac)
-
-lemma sep_conj_commute:
-  "(P ** Q) = (Q ** P)"
-  by (rule ext) (auto intro: sep_conj_commuteI)
-
-lemma sep_conj_assoc:
-  "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs")
-proof (rule ext, rule iffI)
-  fix h
-  assume a: "?lhs h"
-  then obtain x y z where "P x" and "Q y" and "R z"
-                      and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"
-                      and "h = x + y + z"
-    by (auto dest!: sep_conjD dest: sep_add_disjD)
-  moreover
-  then have "x ## y + z"
-    by (simp add: sep_disj_add)
-  ultimately
-  show "?rhs h"
-    by (auto simp: sep_add_ac intro!: sep_conjI)
-next
-  fix h
-  assume a: "?rhs h"
-  then obtain x y z where "P x" and "Q y" and "R z"
-                      and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
-                      and "h = x + y + z"
-    by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
-  thus "?lhs h"
-    by (metis sep_conj_def sep_disj_addI1)
-qed
-
-lemma sep_conj_impl:
-  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h \<rbrakk> \<Longrightarrow> (P' ** Q') h"
-  by (erule sep_conjE, auto intro!: sep_conjI)
-
-lemma sep_conj_impl1:
-  assumes P: "\<And>h. P h \<Longrightarrow> I h"
-  shows "(P ** R) h \<Longrightarrow> (I ** R) h"
-  by (auto intro: sep_conj_impl P)
-
-lemma sep_globalise:
-  "\<lbrakk> (P ** R) h; (\<And>h. P h \<Longrightarrow> Q h) \<rbrakk> \<Longrightarrow> (Q ** R) h"
-  by (fast elim: sep_conj_impl)
-
-lemma sep_conj_trivial_strip2:
-  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp
-
-lemma disjoint_subheaps_exist:
-  "\<exists>x y. x ## y \<and> h = x + y"
-  by (rule_tac x=0 in exI, auto)
-
-lemma sep_conj_left_commute: (* for permutative rewriting *)
-  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")
-proof -
-  have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute)
-  also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
-  finally show ?thesis by (simp add: sep_conj_commute)
-qed
-
-lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute
-
-lemma ab_semigroup_mult_sep_conj: "class.ab_semigroup_mult op **"
-  by (unfold_locales)
-     (auto simp: sep_conj_ac)
-
-lemma sep_empty_zero [simp,intro!]: "\<box> 0"
-  by (simp add: sep_empty_def)
-
-
-subsection {* Properties of @{text sep_true} and @{text sep_false} *}
-
-lemma sep_conj_sep_true:
-  "P h \<Longrightarrow> (P ** sep_true) h"
-  by (simp add: sep_conjI[where y=0])
-
-lemma sep_conj_sep_true':
-  "P h \<Longrightarrow> (sep_true ** P) h"
-  by (simp add: sep_conjI[where x=0])
-
-lemma sep_conj_true [simp]:
-  "(sep_true ** sep_true) = sep_true"
-  unfolding sep_conj_def
-  by (auto intro!: ext intro: disjoint_subheaps_exist)
-
-lemma sep_conj_false_right [simp]:
-  "(P ** sep_false) = sep_false"
-  by (force elim: sep_conjE intro!: ext)
-
-lemma sep_conj_false_left [simp]:
-  "(sep_false ** P) = sep_false"
-  by (subst sep_conj_commute) (rule sep_conj_false_right)
-
-
-
-subsection {* Properties of zero (@{const sep_empty}) *}
-
-lemma sep_conj_empty [simp]:
-  "(P ** \<box>) = P"
-  by (simp add: sep_conj_def sep_empty_def)
-
-lemma sep_conj_empty'[simp]:
-  "(\<box> ** P) = P"
-  by (subst sep_conj_commute, rule sep_conj_empty)
-
-lemma sep_conj_sep_emptyI:
-  "P h \<Longrightarrow> (P ** \<box>) h"
-  by simp
-
-lemma sep_conj_sep_emptyE:
-  "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s"
-  by simp
-
-lemma monoid_add: "class.monoid_add (op **) \<box>"
-  by (unfold_locales) (auto simp: sep_conj_ac)
-
-lemma comm_monoid_add: "class.comm_monoid_add op ** \<box>"
-  by (unfold_locales) (auto simp: sep_conj_ac)
-
-
-subsection {* Properties of top (@{text sep_true}) *}
-
-lemma sep_conj_true_P [simp]:
-  "(sep_true ** (sep_true ** P)) = (sep_true ** P)"
-  by (simp add: sep_conj_assoc[symmetric])
-
-lemma sep_conj_disj:
-  "((P or Q) ** R) = ((P ** R) or (Q ** R))"
-  by (auto simp: sep_conj_def intro!: ext)
-
-lemma sep_conj_sep_true_left:
-  "(P ** Q) h \<Longrightarrow> (sep_true ** Q) h"
-  by (erule sep_conj_impl, simp+)
-
-lemma sep_conj_sep_true_right:
-  "(P ** Q) h \<Longrightarrow> (P ** sep_true) h"
-  by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,
-      simp add: sep_conj_ac)
-
-
-subsection {* Separating Conjunction with Quantifiers *}
-
-lemma sep_conj_conj:
-  "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h"
-  by (force intro: sep_conjI elim!: sep_conjE)
-
-lemma sep_conj_exists1:
-  "((EXS x. P x) ** Q) = (EXS x. (P x ** Q))"
-  by (force intro!: ext intro: sep_conjI elim: sep_conjE)
-
-lemma sep_conj_exists2:
-  "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)"
-  by (force intro!: sep_conjI ext elim!: sep_conjE)
-
-lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
-
-lemma sep_conj_spec:
-  "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h"
-  by (force intro: sep_conjI elim: sep_conjE)
-
-
-subsection {* Properties of Separating Implication *}
-
-lemma sep_implI:
-  assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')"
-  shows "(P \<longrightarrow>* Q) h"
-  unfolding sep_impl_def by (auto elim: a)
-
-lemma sep_implD:
-  "(x \<longrightarrow>* y) h \<Longrightarrow> \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h')"
-  by (force simp: sep_impl_def)
-
-lemma sep_implE:
-  "(x \<longrightarrow>* y) h \<Longrightarrow> (\<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q) \<Longrightarrow> Q"
-  by (auto dest: sep_implD)
-
-lemma sep_impl_sep_true [simp]:
-  "(P \<longrightarrow>* sep_true) = sep_true"
-  by (force intro!: sep_implI ext)
-
-lemma sep_impl_sep_false [simp]:
-  "(sep_false \<longrightarrow>* P) = sep_true"
-  by (force intro!: sep_implI ext)
-
-lemma sep_impl_sep_true_P:
-  "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h"
-  by (clarsimp dest!: sep_implD elim!: allE[where x=0])
-
-lemma sep_impl_sep_true_false [simp]:
-  "(sep_true \<longrightarrow>* sep_false) = sep_false"
-  by (force intro!: ext dest: sep_impl_sep_true_P)
-
-lemma sep_conj_sep_impl:
-  "\<lbrakk> P h; \<And>h. (P ** Q) h \<Longrightarrow> R h \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) h"
-proof (rule sep_implI)
-  fix h' h
-  assume "P h" and "h ## h'" and "Q h'"
-  hence "(P ** Q) (h + h')" by (force intro: sep_conjI)
-  moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h"
-  ultimately show "R (h + h')" by simp
-qed
-
-lemma sep_conj_sep_impl2:
-  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> (Q \<longrightarrow>* R) h \<rbrakk> \<Longrightarrow> R h"
-  by (force dest: sep_implD elim: sep_conjE)
-
-lemma sep_conj_sep_impl_sep_conj2:
-  "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h"
-  by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)
-
-
-subsection {* Pure assertions *}
-
-definition
-  pure :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "pure P \<equiv> \<forall>h h'. P h = P h'"
-
-lemma pure_sep_true:
-  "pure sep_true"
-  by (simp add: pure_def)
-
-lemma pure_sep_false:
-  "pure sep_true"
-  by (simp add: pure_def)
-
-lemma pure_split:
-  "pure P = (P = sep_true \<or> P = sep_false)"
-  by (force simp: pure_def intro!: ext)
-
-lemma pure_sep_conj:
-  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)"
-  by (force simp: pure_split)
-
-lemma pure_sep_impl:
-  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)"
-  by (force simp: pure_split)
-
-lemma pure_conj_sep_conj:
-  "\<lbrakk> (P and Q) h; pure P \<or> pure Q \<rbrakk> \<Longrightarrow> (P \<and>* Q) h"
-  by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)
-
-lemma pure_sep_conj_conj:
-  "\<lbrakk> (P \<and>* Q) h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P and Q) h"
-  by (force simp: pure_split)
-
-lemma pure_conj_sep_conj_assoc:
-  "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))"
-  by (auto simp: pure_split)
-
-lemma pure_sep_impl_impl:
-  "\<lbrakk> (P \<longrightarrow>* Q) h; pure P \<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h"
-  by (force simp: pure_split dest: sep_impl_sep_true_P)
-
-lemma pure_impl_sep_impl:
-  "\<lbrakk> P h \<longrightarrow> Q h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h"
-  by (force simp: pure_split)
-
-lemma pure_conj_right: "(Q \<and>* (\<langle>P'\<rangle> and Q')) = (\<langle>P'\<rangle> and (Q \<and>* Q'))"
-  by (rule ext, rule, rule, clarsimp elim!: sep_conjE)
-     (erule sep_conj_impl, auto)
-
-lemma pure_conj_right': "(Q \<and>* (P' and \<langle>Q'\<rangle>)) = (\<langle>Q'\<rangle> and (Q \<and>* P'))"
-  by (simp add: conj_comms pure_conj_right)
-
-lemma pure_conj_left: "((\<langle>P'\<rangle> and Q') \<and>* Q) = (\<langle>P'\<rangle> and (Q' \<and>* Q))"
-  by (simp add: pure_conj_right sep_conj_ac)
-
-lemma pure_conj_left': "((P' and \<langle>Q'\<rangle>) \<and>* Q) = (\<langle>Q'\<rangle> and (P' \<and>* Q))"
-  by (subst conj_comms, subst pure_conj_left, simp)
-
-lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left
-    pure_conj_left'
-
-declare pure_conj[simp add]
-
-
-subsection {* Intuitionistic assertions *}
-
-definition intuitionistic :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "intuitionistic P \<equiv> \<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'"
-
-lemma intuitionisticI:
-  "(\<And>h h'. \<lbrakk> P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h') \<Longrightarrow> intuitionistic P"
-  by (unfold intuitionistic_def, fast)
-
-lemma intuitionisticD:
-  "\<lbrakk> intuitionistic P; P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h'"
-  by (unfold intuitionistic_def, fast)
-
-lemma pure_intuitionistic:
-  "pure P \<Longrightarrow> intuitionistic P"
-  by (clarsimp simp: intuitionistic_def pure_def, fast)
-
-lemma intuitionistic_conj:
-  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_disj:
-  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_forall:
-  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_exists:
-  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_sep_conj_sep_true:
-  "intuitionistic (sep_true \<and>* P)"
-proof (rule intuitionisticI)
-  fix h h' r
-  assume a: "(sep_true \<and>* P) h"
-  then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y"
-    by - (drule sep_conjD, clarsimp)
-  moreover assume a2: "h \<preceq> h'"
-  then obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  moreover have "(P \<and>* sep_true) (y + (x + z))"
-    using P h hzd xyd
-    by (metis sep_add_disjI1 sep_disj_commute sep_conjI)
-  ultimately show "(sep_true \<and>* P) h'" using hzd
-    by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD)
-qed
-
-lemma intuitionistic_sep_impl_sep_true:
-  "intuitionistic (sep_true \<longrightarrow>* P)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-  show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd
-    apply (clarsimp dest!: sep_implD)
-    apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI)
-    done
-qed
-
-lemma intuitionistic_sep_conj:
-  assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))"
-  shows "intuitionistic (P \<and>* Q)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  from sc obtain x y where px: "P x" and qy: "Q y"
-                       and h: "h = x + y" and xyd: "x ## y"
-    by (clarsimp simp: sep_conj_def)
-
-  have "x ## z" using hzd h xyd
-    by (metis sep_add_disjD)
-
-  with ip px have "P (x + z)"
-    by (fastforce elim: intuitionisticD sep_substate_disj_add)
-
-  thus "(P \<and>* Q) h'" using h' h hzd qy xyd
-    by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2
-              sep_add_left_commute sep_conjI)
-qed
-
-lemma intuitionistic_sep_impl:
-  assumes iq: "intuitionistic Q"
-  shows "intuitionistic (P \<longrightarrow>* Q)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume imp: "(P \<longrightarrow>* Q) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  {
-    fix x
-    assume px: "P x" and hzx: "h + z ## x"
-
-    have "h + x \<preceq> h + x + z" using hzx hzd
-    by (metis sep_add_disjI1 sep_substate_def)
-
-    with imp hzd iq px hzx
-    have "Q (h + z + x)"
-    by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE)
-  }
-
-  with imp h' hzd iq show "(P \<longrightarrow>* Q) h'"
-    by (fastforce intro: sep_implI)
-qed
-
-lemma strongest_intuitionistic:
-  "\<not> (\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and>
-      Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))"
-  by (fastforce intro!: ext sep_substate_disj_add
-                dest!: sep_conjD intuitionisticD)
-
-lemma weakest_intuitionistic:
-  "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and>
-      Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))"
-  apply (clarsimp intro!: ext)
-  apply (rule iffI)
-   apply (rule sep_implI)
-   apply (drule_tac h="x" and h'="x + h'" in intuitionisticD)
-     apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+
-  done
-
-lemma intuitionistic_sep_conj_sep_true_P:
-  "\<lbrakk> (P \<and>* sep_true) s; intuitionistic P \<rbrakk> \<Longrightarrow> P s"
-  by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add)
-
-lemma intuitionistic_sep_conj_sep_true_simp:
-  "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P"
-  by (fast intro!: sep_conj_sep_true ext
-           elim: intuitionistic_sep_conj_sep_true_P)
-
-lemma intuitionistic_sep_impl_sep_true_P:
-  "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h"
-  by (force intro!: sep_implI dest: intuitionisticD
-            intro: sep_substate_disj_add)
-
-lemma intuitionistic_sep_impl_sep_true_simp:
-  "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P"
-  by (fast intro!: ext
-           elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)
-
-
-subsection {* Strictly exact assertions *}
-
-definition strictly_exact :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "strictly_exact P \<equiv> \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'"
-
-lemma strictly_exactD:
-  "\<lbrakk> strictly_exact P; P h; P h' \<rbrakk> \<Longrightarrow> h = h'"
-  by (unfold strictly_exact_def, fast)
-
-lemma strictly_exactI:
-  "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P"
-  by (unfold strictly_exact_def, fast)
-
-lemma strictly_exact_sep_conj:
-  "\<lbrakk> strictly_exact P; strictly_exact Q \<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q)"
-  apply (rule strictly_exactI)
-  apply (erule sep_conjE)+
-  apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+)
-  apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+)
-  apply clarsimp
-  done
-
-lemma strictly_exact_conj_impl:
-  "\<lbrakk> (Q \<and>* sep_true) h; P h; strictly_exact Q \<rbrakk> \<Longrightarrow> (Q \<and>* (Q \<longrightarrow>* P)) h"
-  by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE
-            simp: sep_add_commute sep_add_assoc)
-
-end
-
-interpretation sep: ab_semigroup_mult "op **"
-  by (rule ab_semigroup_mult_sep_conj)
-
-interpretation sep: comm_monoid_add "op **" \<box>
-  by (rule comm_monoid_add)
-
-
-section {* Separation Algebra with Stronger, but More Intuitive Disjunction Axiom *}
-
-class stronger_sep_algebra = pre_sep_algebra +
-  assumes sep_add_disj_eq [simp]: "y ## z \<Longrightarrow> x ## y + z = (x ## y \<and> x ## z)"
-begin
-
-lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)"
-  by (metis sep_add_disj_eq sep_disj_commute)
-
-subclass sep_algebra by default auto
-
-end
-
-
-section {* Folding separating conjunction over lists of predicates *}
-
-lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>"
-  by (simp add: sep_list_conj_def)
-
-(* apparently these two are rarely used and had to be removed from List.thy *)
-lemma (in semigroup_add) foldl_assoc:
-shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
-by (induct zs arbitrary: y) (simp_all add:add_assoc)
-
-lemma (in monoid_add) foldl_absorb0:
-shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
-by (induct zs) (simp_all add:foldl_assoc)
-
-lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)"
-  by (simp add: sep_list_conj_def sep.foldl_absorb0)
-
-lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)"
-  by (simp add: sep_list_conj_def sep.foldl_absorb0)
-
-lemma (in comm_monoid_add) foldl_map_filter:
-  "foldl op + 0 (map f (filter P xs)) +
-     foldl op + 0 (map f (filter (not P) xs))
-   = foldl op + 0 (map f xs)"
-proof (induct xs)
-  case Nil thus ?case by clarsimp
-next
-  case (Cons x xs)
-  hence IH: "foldl op + 0 (map f xs) =
-               foldl op + 0 (map f (filter P xs)) +
-               foldl op + 0 (map f [x\<leftarrow>xs . \<not> P x])"
-               by (simp only: eq_commute)
-
-  have foldl_Cons':
-    "\<And>x xs. foldl op + 0 (x # xs) = x + (foldl op + 0 xs)"
-    by (simp, subst foldl_absorb0[symmetric], rule refl)
-
-  { assume "P x"
-    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
-  } moreover {
-    assume "\<not> P x"
-    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
-  }
-  ultimately show ?case by blast
-qed
-
-
-section {* Separation Algebra with a Cancellative Monoid (for completeness) *}
-
-text {*
-  Separation algebra with a cancellative monoid. The results of being a precise
-  assertion (distributivity over separating conjunction) require this.
-  although we never actually use this property in our developments, we keep
-  it here for completeness.
-  *}
-class cancellative_sep_algebra = sep_algebra +
-  assumes sep_add_cancelD: "\<lbrakk> x + z = y + z ; x ## z ; y ## z \<rbrakk> \<Longrightarrow> x = y"
-begin
-
-definition
-  (* In any heap, there exists at most one subheap for which P holds *)
-  precise :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "precise P = (\<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp')"
-
-lemma "precise (op = s)"
-  by (metis (full_types) precise_def)
-
-lemma sep_add_cancel:
-  "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)"
-  by (metis sep_add_cancelD)
-
-lemma precise_distribute:
-  "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))"
-proof (rule iffI)
-  assume pp: "precise P"
-  {
-    fix Q R
-    fix h hp hp' s
-
-    { assume a: "((Q and R) \<and>* P) s"
-      hence "((Q \<and>* P) and (R \<and>* P)) s"
-        by (fastforce dest!: sep_conjD elim: sep_conjI)
-    }
-    moreover
-    { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s"
-
-      from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"
-                           and x: "Q x" and y: "P y"
-        by (fastforce dest!: sep_conjD)
-      from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"
-                           and x': "R x'" and y': "P y'"
-        by (fastforce dest!: sep_conjD)
-
-      from sxy have ys: "y \<preceq> x + y" using xy
-        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
-      from sxy' have ys': "y' \<preceq> x' + y'" using xy'
-        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
-
-      from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys'
-        by (fastforce simp: precise_def)
-
-      hence "x = x'" using sxy sxy' xy xy'
-        by (fastforce dest!: sep_add_cancelD)
-
-      hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy'
-        by (fastforce intro: sep_conjI)
-    }
-    ultimately
-    have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast
-  }
-  thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by (blast intro!: ext)
-
-next
-  assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))"
-  thus "precise P"
-  proof (clarsimp simp: precise_def)
-    fix h hp hp' Q R
-    assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'"
-
-    obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp
-      by (clarsimp simp: sep_substate_def)
-    obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp'
-      by (clarsimp simp: sep_substate_def)
-
-    have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz'
-      by (fastforce simp: sep_add_ac)
-
-    from hhp hhp' a hpz hpz' h_eq
-    have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')"
-      by (fastforce simp: h_eq sep_add_ac sep_conj_commute)
-
-    hence "((op = z and op = z') \<and>* P) (z + hp) =
-           ((op = z \<and>* P) and (op = z' \<and>* P)) (z' + hp')" by blast
-
-    thus  "hp = hp'" using php php' hpz hpz' h_eq
-      by (fastforce dest!: iffD2 cong: conj_cong
-                    simp: sep_add_ac sep_add_cancel sep_conj_def)
-  qed
-qed
-
-lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P"
-  by (metis precise_def strictly_exactD)
-
-end
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Separation_Algebra.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,815 @@
+(* Authors: Gerwin Klein and Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Abstract Separation Algebra"
+
+theory Separation_Algebra
+imports Main
+begin
+
+
+text {* This theory is the main abstract separation algebra development *}
+
+
+section {* Input syntax for lifting boolean predicates to separation predicates *}
+
+abbreviation (input)
+  pred_and :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where
+  "a and b \<equiv> \<lambda>s. a s \<and> b s"
+
+abbreviation (input)
+  pred_or :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "or" 30) where
+  "a or b \<equiv> \<lambda>s. a s \<or> b s"
+
+abbreviation (input)
+  pred_not :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" ("not _" [40] 40) where
+  "not a \<equiv> \<lambda>s. \<not>a s"
+
+abbreviation (input)
+  pred_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "imp" 25) where
+  "a imp b \<equiv> \<lambda>s. a s \<longrightarrow> b s"
+
+abbreviation (input)
+  pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
+  "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
+
+(* abbreviation *)
+  definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
+  "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
+
+abbreviation (input)
+  pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where
+  "ALLS x. P x \<equiv> \<lambda>s. \<forall>x. P x s"
+
+
+section {* Associative/Commutative Monoid Basis of Separation Algebras *}
+
+class pre_sep_algebra = zero + plus +
+  fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)
+
+  assumes sep_disj_zero [simp]: "x ## 0"
+  assumes sep_disj_commuteI: "x ## y \<Longrightarrow> y ## x"
+
+  assumes sep_add_zero [simp]: "x + 0 = x"
+  assumes sep_add_commute: "x ## y \<Longrightarrow> x + y = y + x"
+
+  assumes sep_add_assoc:
+    "\<lbrakk> x ## y; y ## z; x ## z \<rbrakk> \<Longrightarrow> (x + y) + z = x + (y + z)"
+begin
+
+lemma sep_disj_commute: "x ## y = y ## x"
+  by (blast intro: sep_disj_commuteI)
+
+lemma sep_add_left_commute:
+  assumes a: "a ## b" "b ## c" "a ## c"
+  shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = b + a + c" using a
+    by (simp add: sep_add_assoc[symmetric] sep_disj_commute)
+  also have "... = a + b + c" using a
+    by (simp add: sep_add_commute sep_disj_commute)
+  also have "... = ?rhs" using a
+    by (simp add: sep_add_assoc sep_disj_commute)
+  finally show ?thesis .
+qed
+
+lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute
+                    sep_disj_commute (* nearly always necessary *)
+
+end
+
+
+section {* Separation Algebra as Defined by Calcagno et al. *}
+
+class sep_algebra = pre_sep_algebra +
+  assumes sep_disj_addD1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y"
+  assumes sep_disj_addI1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + y ##  z"
+begin
+
+subsection {* Basic Construct Definitions and Abbreviations *}
+
+definition
+  sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "**" 35)
+  where
+  "P ** Q \<equiv> \<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
+
+notation
+  sep_conj (infixr "\<and>*" 35)
+
+definition
+  sep_empty :: "'a \<Rightarrow> bool" ("\<box>") where
+  "\<box> \<equiv> \<lambda>h. h = 0"
+
+definition
+  sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>*" 25)
+  where
+  "P \<longrightarrow>* Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')"
+
+definition
+  sep_substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where
+  "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> x + z = y"
+
+(* We want these to be abbreviations not definitions, because basic True and
+   False will occur by simplification in sep_conj terms *)
+abbreviation
+  "sep_true \<equiv> \<langle>True\<rangle>"
+
+abbreviation
+  "sep_false \<equiv> \<langle>False\<rangle>"
+
+definition
+  sep_list_conj :: "('a \<Rightarrow> bool) list \<Rightarrow> ('a \<Rightarrow> bool)"  ("\<And>* _" [60] 90) where
+  "sep_list_conj Ps \<equiv> foldl (op **) \<box> Ps"
+
+
+subsection {* Disjunction/Addition Properties *}
+
+lemma disjoint_zero_sym [simp]: "0 ## x"
+  by (simp add: sep_disj_commute)
+
+lemma sep_add_zero_sym [simp]: "0 + x = x"
+  by (simp add: sep_add_commute)
+
+lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z"
+  by (metis sep_disj_addD1 sep_add_ac)
+
+lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z"
+  by (metis sep_disj_addD1 sep_disj_addD2)
+
+lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z"
+  by (metis sep_disj_addD sep_disj_commuteI)
+
+lemma sep_disj_addI2:
+  "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y"
+  by (metis sep_add_ac sep_disj_addI1)
+
+lemma sep_add_disjI1:
+  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y"
+  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
+
+lemma sep_add_disjI2:
+  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x"
+  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
+
+lemma sep_disj_addI3:
+   "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z"
+   by (metis sep_add_ac sep_add_disjD sep_add_disjI2)
+
+lemma sep_disj_add:
+  "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z"
+  by (metis sep_disj_addI1 sep_disj_addI3)
+
+
+subsection {* Substate Properties *}
+
+lemma sep_substate_disj_add:
+  "x ## y \<Longrightarrow> x \<preceq> x + y"
+  unfolding sep_substate_def by blast
+
+lemma sep_substate_disj_add':
+  "x ## y \<Longrightarrow> x \<preceq> y + x"
+  by (simp add: sep_add_ac sep_substate_disj_add)
+
+
+subsection {* Separating Conjunction Properties *}
+
+lemma sep_conjD:
+  "(P \<and>* Q) h \<Longrightarrow> \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
+  by (simp add: sep_conj_def)
+
+lemma sep_conjE:
+  "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"
+  by (auto simp: sep_conj_def)
+
+lemma sep_conjI:
+  "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h"
+  by (auto simp: sep_conj_def)
+
+lemma sep_conj_commuteI:
+  "(P ** Q) h \<Longrightarrow> (Q ** P) h"
+  by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac)
+
+lemma sep_conj_commute:
+  "(P ** Q) = (Q ** P)"
+  by (rule ext) (auto intro: sep_conj_commuteI)
+
+lemma sep_conj_assoc:
+  "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs")
+proof (rule ext, rule iffI)
+  fix h
+  assume a: "?lhs h"
+  then obtain x y z where "P x" and "Q y" and "R z"
+                      and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"
+                      and "h = x + y + z"
+    by (auto dest!: sep_conjD dest: sep_add_disjD)
+  moreover
+  then have "x ## y + z"
+    by (simp add: sep_disj_add)
+  ultimately
+  show "?rhs h"
+    by (auto simp: sep_add_ac intro!: sep_conjI)
+next
+  fix h
+  assume a: "?rhs h"
+  then obtain x y z where "P x" and "Q y" and "R z"
+                      and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
+                      and "h = x + y + z"
+    by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
+  thus "?lhs h"
+    by (metis sep_conj_def sep_disj_addI1)
+qed
+
+lemma sep_conj_impl:
+  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h \<rbrakk> \<Longrightarrow> (P' ** Q') h"
+  by (erule sep_conjE, auto intro!: sep_conjI)
+
+lemma sep_conj_impl1:
+  assumes P: "\<And>h. P h \<Longrightarrow> I h"
+  shows "(P ** R) h \<Longrightarrow> (I ** R) h"
+  by (auto intro: sep_conj_impl P)
+
+lemma sep_globalise:
+  "\<lbrakk> (P ** R) h; (\<And>h. P h \<Longrightarrow> Q h) \<rbrakk> \<Longrightarrow> (Q ** R) h"
+  by (fast elim: sep_conj_impl)
+
+lemma sep_conj_trivial_strip2:
+  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp
+
+lemma disjoint_subheaps_exist:
+  "\<exists>x y. x ## y \<and> h = x + y"
+  by (rule_tac x=0 in exI, auto)
+
+lemma sep_conj_left_commute: (* for permutative rewriting *)
+  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")
+proof -
+  have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute)
+  also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
+  finally show ?thesis by (simp add: sep_conj_commute)
+qed
+
+lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute
+
+lemma ab_semigroup_mult_sep_conj: "class.ab_semigroup_mult op **"
+  by (unfold_locales)
+     (auto simp: sep_conj_ac)
+
+lemma sep_empty_zero [simp,intro!]: "\<box> 0"
+  by (simp add: sep_empty_def)
+
+
+subsection {* Properties of @{text sep_true} and @{text sep_false} *}
+
+lemma sep_conj_sep_true:
+  "P h \<Longrightarrow> (P ** sep_true) h"
+  by (simp add: sep_conjI[where y=0])
+
+lemma sep_conj_sep_true':
+  "P h \<Longrightarrow> (sep_true ** P) h"
+  by (simp add: sep_conjI[where x=0])
+
+lemma sep_conj_true [simp]:
+  "(sep_true ** sep_true) = sep_true"
+  unfolding sep_conj_def
+  by (auto intro!: ext intro: disjoint_subheaps_exist)
+
+lemma sep_conj_false_right [simp]:
+  "(P ** sep_false) = sep_false"
+  by (force elim: sep_conjE intro!: ext)
+
+lemma sep_conj_false_left [simp]:
+  "(sep_false ** P) = sep_false"
+  by (subst sep_conj_commute) (rule sep_conj_false_right)
+
+
+
+subsection {* Properties of zero (@{const sep_empty}) *}
+
+lemma sep_conj_empty [simp]:
+  "(P ** \<box>) = P"
+  by (simp add: sep_conj_def sep_empty_def)
+
+lemma sep_conj_empty'[simp]:
+  "(\<box> ** P) = P"
+  by (subst sep_conj_commute, rule sep_conj_empty)
+
+lemma sep_conj_sep_emptyI:
+  "P h \<Longrightarrow> (P ** \<box>) h"
+  by simp
+
+lemma sep_conj_sep_emptyE:
+  "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s"
+  by simp
+
+lemma monoid_add: "class.monoid_add (op **) \<box>"
+  by (unfold_locales) (auto simp: sep_conj_ac)
+
+lemma comm_monoid_add: "class.comm_monoid_add op ** \<box>"
+  by (unfold_locales) (auto simp: sep_conj_ac)
+
+
+subsection {* Properties of top (@{text sep_true}) *}
+
+lemma sep_conj_true_P [simp]:
+  "(sep_true ** (sep_true ** P)) = (sep_true ** P)"
+  by (simp add: sep_conj_assoc[symmetric])
+
+lemma sep_conj_disj:
+  "((P or Q) ** R) = ((P ** R) or (Q ** R))"
+  by (auto simp: sep_conj_def intro!: ext)
+
+lemma sep_conj_sep_true_left:
+  "(P ** Q) h \<Longrightarrow> (sep_true ** Q) h"
+  by (erule sep_conj_impl, simp+)
+
+lemma sep_conj_sep_true_right:
+  "(P ** Q) h \<Longrightarrow> (P ** sep_true) h"
+  by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,
+      simp add: sep_conj_ac)
+
+
+subsection {* Separating Conjunction with Quantifiers *}
+
+lemma sep_conj_conj:
+  "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h"
+  by (force intro: sep_conjI elim!: sep_conjE)
+
+lemma sep_conj_exists1:
+  "((EXS x. P x) ** Q) = (EXS x. (P x ** Q))"
+  by (unfold pred_ex_def, force intro!: ext intro: sep_conjI elim: sep_conjE)
+
+lemma sep_conj_exists2:
+  "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)"
+  by (unfold pred_ex_def, force intro!: sep_conjI ext elim!: sep_conjE)
+
+lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
+
+lemma sep_conj_spec:
+  "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h"
+  by (force intro: sep_conjI elim: sep_conjE)
+
+
+subsection {* Properties of Separating Implication *}
+
+lemma sep_implI:
+  assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')"
+  shows "(P \<longrightarrow>* Q) h"
+  unfolding sep_impl_def by (auto elim: a)
+
+lemma sep_implD:
+  "(x \<longrightarrow>* y) h \<Longrightarrow> \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h')"
+  by (force simp: sep_impl_def)
+
+lemma sep_implE:
+  "(x \<longrightarrow>* y) h \<Longrightarrow> (\<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q) \<Longrightarrow> Q"
+  by (auto dest: sep_implD)
+
+lemma sep_impl_sep_true [simp]:
+  "(P \<longrightarrow>* sep_true) = sep_true"
+  by (force intro!: sep_implI ext)
+
+lemma sep_impl_sep_false [simp]:
+  "(sep_false \<longrightarrow>* P) = sep_true"
+  by (force intro!: sep_implI ext)
+
+lemma sep_impl_sep_true_P:
+  "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h"
+  by (clarsimp dest!: sep_implD elim!: allE[where x=0])
+
+lemma sep_impl_sep_true_false [simp]:
+  "(sep_true \<longrightarrow>* sep_false) = sep_false"
+  by (force intro!: ext dest: sep_impl_sep_true_P)
+
+lemma sep_conj_sep_impl:
+  "\<lbrakk> P h; \<And>h. (P ** Q) h \<Longrightarrow> R h \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) h"
+proof (rule sep_implI)
+  fix h' h
+  assume "P h" and "h ## h'" and "Q h'"
+  hence "(P ** Q) (h + h')" by (force intro: sep_conjI)
+  moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h"
+  ultimately show "R (h + h')" by simp
+qed
+
+lemma sep_conj_sep_impl2:
+  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> (Q \<longrightarrow>* R) h \<rbrakk> \<Longrightarrow> R h"
+  by (force dest: sep_implD elim: sep_conjE)
+
+lemma sep_conj_sep_impl_sep_conj2:
+  "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h"
+  by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)
+
+
+subsection {* Pure assertions *}
+
+definition
+  pure :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "pure P \<equiv> \<forall>h h'. P h = P h'"
+
+lemma pure_sep_true:
+  "pure sep_true"
+  by (simp add: pure_def)
+
+lemma pure_sep_false:
+  "pure sep_true"
+  by (simp add: pure_def)
+
+lemma pure_split:
+  "pure P = (P = sep_true \<or> P = sep_false)"
+  by (force simp: pure_def intro!: ext)
+
+lemma pure_sep_conj:
+  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)"
+  by (force simp: pure_split)
+
+lemma pure_sep_impl:
+  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)"
+  by (force simp: pure_split)
+
+lemma pure_conj_sep_conj:
+  "\<lbrakk> (P and Q) h; pure P \<or> pure Q \<rbrakk> \<Longrightarrow> (P \<and>* Q) h"
+  by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)
+
+lemma pure_sep_conj_conj:
+  "\<lbrakk> (P \<and>* Q) h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P and Q) h"
+  by (force simp: pure_split)
+
+lemma pure_conj_sep_conj_assoc:
+  "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))"
+  by (auto simp: pure_split)
+
+lemma pure_sep_impl_impl:
+  "\<lbrakk> (P \<longrightarrow>* Q) h; pure P \<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h"
+  by (force simp: pure_split dest: sep_impl_sep_true_P)
+
+lemma pure_impl_sep_impl:
+  "\<lbrakk> P h \<longrightarrow> Q h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h"
+  by (force simp: pure_split)
+
+lemma pure_conj_right: "(Q \<and>* (\<langle>P'\<rangle> and Q')) = (\<langle>P'\<rangle> and (Q \<and>* Q'))"
+  by (rule ext, rule, rule, clarsimp elim!: sep_conjE)
+     (erule sep_conj_impl, auto)
+
+lemma pure_conj_right': "(Q \<and>* (P' and \<langle>Q'\<rangle>)) = (\<langle>Q'\<rangle> and (Q \<and>* P'))"
+  by (simp add: conj_comms pure_conj_right)
+
+lemma pure_conj_left: "((\<langle>P'\<rangle> and Q') \<and>* Q) = (\<langle>P'\<rangle> and (Q' \<and>* Q))"
+  by (simp add: pure_conj_right sep_conj_ac)
+
+lemma pure_conj_left': "((P' and \<langle>Q'\<rangle>) \<and>* Q) = (\<langle>Q'\<rangle> and (P' \<and>* Q))"
+  by (subst conj_comms, subst pure_conj_left, simp)
+
+lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left
+    pure_conj_left'
+
+declare pure_conj[simp add]
+
+
+subsection {* Intuitionistic assertions *}
+
+definition intuitionistic :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "intuitionistic P \<equiv> \<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'"
+
+lemma intuitionisticI:
+  "(\<And>h h'. \<lbrakk> P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h') \<Longrightarrow> intuitionistic P"
+  by (unfold intuitionistic_def, fast)
+
+lemma intuitionisticD:
+  "\<lbrakk> intuitionistic P; P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h'"
+  by (unfold intuitionistic_def, fast)
+
+lemma pure_intuitionistic:
+  "pure P \<Longrightarrow> intuitionistic P"
+  by (clarsimp simp: intuitionistic_def pure_def, fast)
+
+lemma intuitionistic_conj:
+  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)"
+  by (force intro: intuitionisticI dest: intuitionisticD)
+
+lemma intuitionistic_disj:
+  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)"
+  by (force intro: intuitionisticI dest: intuitionisticD)
+
+lemma intuitionistic_forall:
+  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)"
+  by (force intro: intuitionisticI dest: intuitionisticD)
+
+lemma intuitionistic_exists:
+  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)"
+  by (unfold pred_ex_def, force intro: intuitionisticI dest: intuitionisticD)
+
+lemma intuitionistic_sep_conj_sep_true:
+  "intuitionistic (sep_true \<and>* P)"
+proof (rule intuitionisticI)
+  fix h h' r
+  assume a: "(sep_true \<and>* P) h"
+  then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y"
+    by - (drule sep_conjD, clarsimp)
+  moreover assume a2: "h \<preceq> h'"
+  then obtain z where h': "h' = h + z" and hzd: "h ## z"
+    by (clarsimp simp: sep_substate_def)
+
+  moreover have "(P \<and>* sep_true) (y + (x + z))"
+    using P h hzd xyd
+    by (metis sep_add_disjI1 sep_disj_commute sep_conjI)
+  ultimately show "(sep_true \<and>* P) h'" using hzd
+    by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD)
+qed
+
+lemma intuitionistic_sep_impl_sep_true:
+  "intuitionistic (sep_true \<longrightarrow>* P)"
+proof (rule intuitionisticI)
+  fix h h'
+  assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'"
+
+  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
+    by (clarsimp simp: sep_substate_def)
+  show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd
+    apply (clarsimp dest!: sep_implD)
+    apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI)
+    done
+qed
+
+lemma intuitionistic_sep_conj:
+  assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))"
+  shows "intuitionistic (P \<and>* Q)"
+proof (rule intuitionisticI)
+  fix h h'
+  assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'"
+
+  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
+    by (clarsimp simp: sep_substate_def)
+
+  from sc obtain x y where px: "P x" and qy: "Q y"
+                       and h: "h = x + y" and xyd: "x ## y"
+    by (clarsimp simp: sep_conj_def)
+
+  have "x ## z" using hzd h xyd
+    by (metis sep_add_disjD)
+
+  with ip px have "P (x + z)"
+    by (fastforce elim: intuitionisticD sep_substate_disj_add)
+
+  thus "(P \<and>* Q) h'" using h' h hzd qy xyd
+    by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2
+              sep_add_left_commute sep_conjI)
+qed
+
+lemma intuitionistic_sep_impl:
+  assumes iq: "intuitionistic Q"
+  shows "intuitionistic (P \<longrightarrow>* Q)"
+proof (rule intuitionisticI)
+  fix h h'
+  assume imp: "(P \<longrightarrow>* Q) h" and hh': "h \<preceq> h'"
+
+  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
+    by (clarsimp simp: sep_substate_def)
+
+  {
+    fix x
+    assume px: "P x" and hzx: "h + z ## x"
+
+    have "h + x \<preceq> h + x + z" using hzx hzd
+    by (metis sep_add_disjI1 sep_substate_def)
+
+    with imp hzd iq px hzx
+    have "Q (h + z + x)"
+    by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE)
+  }
+
+  with imp h' hzd iq show "(P \<longrightarrow>* Q) h'"
+    by (fastforce intro: sep_implI)
+qed
+
+lemma strongest_intuitionistic:
+  "\<not> (\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and>
+      Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))"
+  by (fastforce intro!: ext sep_substate_disj_add
+                dest!: sep_conjD intuitionisticD)
+
+lemma weakest_intuitionistic:
+  "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and>
+      Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))"
+  apply (clarsimp intro!: ext)
+  apply (rule iffI)
+   apply (rule sep_implI)
+   apply (drule_tac h="x" and h'="x + h'" in intuitionisticD)
+     apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+
+  done
+
+lemma intuitionistic_sep_conj_sep_true_P:
+  "\<lbrakk> (P \<and>* sep_true) s; intuitionistic P \<rbrakk> \<Longrightarrow> P s"
+  by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add)
+
+lemma intuitionistic_sep_conj_sep_true_simp:
+  "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P"
+  by (fast intro!: sep_conj_sep_true ext
+           elim: intuitionistic_sep_conj_sep_true_P)
+
+lemma intuitionistic_sep_impl_sep_true_P:
+  "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h"
+  by (force intro!: sep_implI dest: intuitionisticD
+            intro: sep_substate_disj_add)
+
+lemma intuitionistic_sep_impl_sep_true_simp:
+  "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P"
+  by (fast intro!: ext
+           elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)
+
+
+subsection {* Strictly exact assertions *}
+
+definition strictly_exact :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "strictly_exact P \<equiv> \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'"
+
+lemma strictly_exactD:
+  "\<lbrakk> strictly_exact P; P h; P h' \<rbrakk> \<Longrightarrow> h = h'"
+  by (unfold strictly_exact_def, fast)
+
+lemma strictly_exactI:
+  "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P"
+  by (unfold strictly_exact_def, fast)
+
+lemma strictly_exact_sep_conj:
+  "\<lbrakk> strictly_exact P; strictly_exact Q \<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q)"
+  apply (rule strictly_exactI)
+  apply (erule sep_conjE)+
+  apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+)
+  apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+)
+  apply clarsimp
+  done
+
+lemma strictly_exact_conj_impl:
+  "\<lbrakk> (Q \<and>* sep_true) h; P h; strictly_exact Q \<rbrakk> \<Longrightarrow> (Q \<and>* (Q \<longrightarrow>* P)) h"
+  by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE
+            simp: sep_add_commute sep_add_assoc)
+
+end
+
+interpretation sep: ab_semigroup_mult "op **"
+  by (rule ab_semigroup_mult_sep_conj)
+
+interpretation sep: comm_monoid_add "op **" \<box>
+  by (rule comm_monoid_add)
+
+
+section {* Separation Algebra with Stronger, but More Intuitive Disjunction Axiom *}
+
+class stronger_sep_algebra = pre_sep_algebra +
+  assumes sep_add_disj_eq [simp]: "y ## z \<Longrightarrow> x ## y + z = (x ## y \<and> x ## z)"
+begin
+
+lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)"
+  by (metis sep_add_disj_eq sep_disj_commute)
+
+subclass sep_algebra by default auto
+
+end
+
+
+section {* Folding separating conjunction over lists of predicates *}
+
+lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>"
+  by (simp add: sep_list_conj_def)
+
+(* apparently these two are rarely used and had to be removed from List.thy *)
+lemma (in semigroup_add) foldl_assoc:
+shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
+by (induct zs arbitrary: y) (simp_all add:add_assoc)
+
+lemma (in monoid_add) foldl_absorb0:
+shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
+by (induct zs) (simp_all add:foldl_assoc)
+
+lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)"
+  by (simp add: sep_list_conj_def sep.foldl_absorb0)
+
+lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)"
+  by (simp add: sep_list_conj_def sep.foldl_absorb0)
+
+lemma (in comm_monoid_add) foldl_map_filter:
+  "foldl op + 0 (map f (filter P xs)) +
+     foldl op + 0 (map f (filter (not P) xs))
+   = foldl op + 0 (map f xs)"
+proof (induct xs)
+  case Nil thus ?case by clarsimp
+next
+  case (Cons x xs)
+  hence IH: "foldl op + 0 (map f xs) =
+               foldl op + 0 (map f (filter P xs)) +
+               foldl op + 0 (map f [x\<leftarrow>xs . \<not> P x])"
+               by (simp only: eq_commute)
+
+  have foldl_Cons':
+    "\<And>x xs. foldl op + 0 (x # xs) = x + (foldl op + 0 xs)"
+    by (simp, subst foldl_absorb0[symmetric], rule refl)
+
+  { assume "P x"
+    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
+  } moreover {
+    assume "\<not> P x"
+    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
+  }
+  ultimately show ?case by blast
+qed
+
+
+section {* Separation Algebra with a Cancellative Monoid (for completeness) *}
+
+text {*
+  Separation algebra with a cancellative monoid. The results of being a precise
+  assertion (distributivity over separating conjunction) require this.
+  although we never actually use this property in our developments, we keep
+  it here for completeness.
+  *}
+class cancellative_sep_algebra = sep_algebra +
+  assumes sep_add_cancelD: "\<lbrakk> x + z = y + z ; x ## z ; y ## z \<rbrakk> \<Longrightarrow> x = y"
+begin
+
+definition
+  (* In any heap, there exists at most one subheap for which P holds *)
+  precise :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "precise P = (\<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp')"
+
+lemma "precise (op = s)"
+  by (metis (full_types) precise_def)
+
+lemma sep_add_cancel:
+  "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)"
+  by (metis sep_add_cancelD)
+
+lemma precise_distribute:
+  "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))"
+proof (rule iffI)
+  assume pp: "precise P"
+  {
+    fix Q R
+    fix h hp hp' s
+
+    { assume a: "((Q and R) \<and>* P) s"
+      hence "((Q \<and>* P) and (R \<and>* P)) s"
+        by (fastforce dest!: sep_conjD elim: sep_conjI)
+    }
+    moreover
+    { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s"
+
+      from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"
+                           and x: "Q x" and y: "P y"
+        by (fastforce dest!: sep_conjD)
+      from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"
+                           and x': "R x'" and y': "P y'"
+        by (fastforce dest!: sep_conjD)
+
+      from sxy have ys: "y \<preceq> x + y" using xy
+        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
+      from sxy' have ys': "y' \<preceq> x' + y'" using xy'
+        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
+
+      from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys'
+        by (fastforce simp: precise_def)
+
+      hence "x = x'" using sxy sxy' xy xy'
+        by (fastforce dest!: sep_add_cancelD)
+
+      hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy'
+        by (fastforce intro: sep_conjI)
+    }
+    ultimately
+    have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast
+  }
+  thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by (blast intro!: ext)
+
+next
+  assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))"
+  thus "precise P"
+  proof (clarsimp simp: precise_def)
+    fix h hp hp' Q R
+    assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'"
+
+    obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp
+      by (clarsimp simp: sep_substate_def)
+    obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp'
+      by (clarsimp simp: sep_substate_def)
+
+    have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz'
+      by (fastforce simp: sep_add_ac)
+
+    from hhp hhp' a hpz hpz' h_eq
+    have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')"
+      by (fastforce simp: h_eq sep_add_ac sep_conj_commute)
+
+    hence "((op = z and op = z') \<and>* P) (z + hp) =
+           ((op = z \<and>* P) and (op = z' \<and>* P)) (z' + hp')" by blast
+
+    thus  "hp = hp'" using php php' hpz hpz' h_eq
+      by (fastforce dest!: iffD2 cong: conj_cong
+                    simp: sep_add_ac sep_add_cancel sep_conj_def)
+  qed
+qed
+
+lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P"
+  by (metis precise_def strictly_exactD)
+
+end
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Separation_Algebra_Alt.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,313 @@
+(* Author: Gerwin Klein, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Abstract Separation Logic, Alternative Definition"
+
+theory Separation_Algebra_Alt
+imports Main
+begin
+
+text {*
+  This theory contains an alternative definition of speration algebra,
+  following Calcagno et al very closely. While some of the abstract
+  development is more algebraic, it is cumbersome to instantiate.
+  We only use it to prove equivalence and to give an impression of how
+  it would look like.
+*}
+
+(* The @{text "++"} notation is a horrible choice, but this theory is 
+   only intended to show how the development would look like, not to 
+   actually use it. We remove the notation for map-add so it doesn't
+   conflict.
+*)
+no_notation map_add (infixl "++" 100)
+
+definition
+  lift2 :: "('a => 'b => 'c option) \<Rightarrow> 'a option => 'b option => 'c option"
+where
+  "lift2 f a b \<equiv> case (a,b) of (Some a, Some b) \<Rightarrow> f a b | _ \<Rightarrow> None"
+
+
+class sep_algebra_alt = zero +
+  fixes add :: "'a => 'a => 'a option" (infixr "\<oplus>" 65)
+
+  assumes add_zero [simp]: "x \<oplus> 0 = Some x"
+  assumes add_comm: "x \<oplus> y = y \<oplus> x"
+  assumes add_assoc: "lift2 add a (lift2 add b c) = lift2 add (lift2 add a b) c"
+
+begin
+
+definition
+  disjoint :: "'a => 'a => bool" (infix "##" 60)
+where
+  "a ## b \<equiv> a \<oplus> b \<noteq> None"
+
+lemma disj_com: "x ## y = y ## x"
+  by (auto simp: disjoint_def add_comm)
+
+lemma disj_zero [simp]: "x ## 0"
+  by (auto simp: disjoint_def)
+
+lemma disj_zero2 [simp]: "0 ## x"
+  by (subst disj_com) simp
+
+lemma add_zero2 [simp]: "0 \<oplus> x = Some x"
+  by (subst add_comm) auto
+
+definition
+  substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where
+  "a \<preceq> b \<equiv> \<exists>c. a \<oplus> c = Some b"
+
+definition
+  sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "**" 61)
+  where
+  "P ** Q \<equiv> \<lambda>s. \<exists>p q. p \<oplus> q = Some s \<and> P p \<and> Q q"
+
+definition emp :: "'a \<Rightarrow> bool" ("\<box>") where
+  "\<box> \<equiv> \<lambda>s. s = 0"
+
+definition
+  sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>\<^sup>*" 25)
+  where
+  "P \<longrightarrow>\<^sup>* Q \<equiv> \<lambda>h. \<forall>h' h''. h \<oplus> h' = Some h'' \<and> P h' \<longrightarrow> Q h''"
+
+definition
+  "sep_true \<equiv> \<lambda>s. True"
+
+definition
+  "sep_false \<equiv> \<lambda>s. False"
+
+
+abbreviation
+  add2 :: "'a option => 'a option => 'a option" (infixr "++" 65)
+where
+  "add2 == lift2 add"
+
+
+lemma add2_comm:
+  "a ++ b = b ++ a"
+  by (simp add: lift2_def add_comm split: option.splits)
+
+lemma add2_None [simp]:
+  "x ++ None = None"
+  by (simp add: lift2_def split: option.splits)
+
+lemma None_add2 [simp]:
+  "None ++ x = None"
+  by (simp add: lift2_def split: option.splits)
+
+lemma add2_Some_Some:
+  "Some x ++ Some y = x \<oplus> y"
+  by (simp add: lift2_def)
+
+lemma add2_zero [simp]:
+  "Some x ++ Some 0 = Some x"
+  by (simp add: add2_Some_Some)
+
+lemma zero_add2 [simp]:
+  "Some 0 ++ Some x = Some x"
+  by (simp add: add2_Some_Some)
+
+
+lemma sep_conjE:
+  "\<lbrakk> (P ** Q) s; \<And>p q. \<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"
+  by (auto simp: sep_conj_def)
+
+lemma sep_conjI:
+  "\<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> (P ** Q) s"
+  by (auto simp: sep_conj_def)
+
+lemma sep_conj_comI:
+  "(P ** Q) s \<Longrightarrow> (Q ** P) s"
+  by (auto intro!: sep_conjI elim!: sep_conjE simp: add_comm)
+
+lemma sep_conj_com:
+  "P ** Q = Q ** P"
+  by (auto intro: sep_conj_comI intro!: ext)
+
+lemma lift_to_add2:
+  "\<lbrakk>z \<oplus> q = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> Some z ++ Some x ++ Some y = Some s"
+  by (simp add: add2_Some_Some)
+
+lemma lift_to_add2':
+  "\<lbrakk>q \<oplus> z = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> (Some x ++ Some y) ++ Some z = Some s"
+  by (simp add: add2_Some_Some)
+
+lemma add2_Some:
+  "(x ++ Some y = Some z) = (\<exists>x'. x = Some x' \<and> x' \<oplus> y = Some z)"
+  by (simp add: lift2_def split: option.splits)
+
+lemma Some_add2:
+  "(Some x ++ y = Some z) = (\<exists>y'. y = Some y' \<and> x \<oplus> y' = Some z)"
+  by (simp add: lift2_def split: option.splits)
+
+lemma sep_conj_assoc:
+  "P ** (Q ** R) = (P ** Q) ** R"
+  unfolding sep_conj_def
+  apply (rule ext)
+  apply (rule iffI)
+   apply clarsimp
+   apply (drule (1) lift_to_add2)
+   apply (subst (asm) add_assoc)
+   apply (fastforce simp: add2_Some_Some add2_Some)
+  apply clarsimp
+  apply (drule (1) lift_to_add2')
+  apply (subst (asm) add_assoc [symmetric])
+  apply (fastforce simp: add2_Some_Some Some_add2)
+  done
+
+lemma sep_true[simp]: "sep_true s" by (simp add: sep_true_def)
+lemma sep_false[simp]: "\<not>sep_false x" by (simp add: sep_false_def)
+
+lemma sep_conj_sep_true:
+  "P s \<Longrightarrow> (P ** sep_true) s"
+  by (auto simp: sep_conjI [where q=0])
+
+lemma sep_conj_sep_true':
+  "P s \<Longrightarrow> (sep_true ** P) s"
+  by (auto simp: sep_conjI [where p=0])
+
+lemma disjoint_submaps_exist:
+  "\<exists>h\<^isub>0 h\<^isub>1. h\<^isub>0 \<oplus> h\<^isub>1 = Some h"
+  by (rule_tac x=0 in exI, auto)
+
+lemma sep_conj_true[simp]:
+  "(sep_true ** sep_true) = sep_true"
+  unfolding sep_conj_def
+  by (auto intro!: ext intro: disjoint_submaps_exist)
+
+lemma sep_conj_false_right[simp]:
+  "(P ** sep_false) = sep_false"
+  by (force elim: sep_conjE intro!: ext)
+
+lemma sep_conj_false_left[simp]:
+  "(sep_false ** P) = sep_false"
+  by (subst sep_conj_com) (rule sep_conj_false_right)
+
+lemma sep_conj_left_com:
+  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")
+proof -
+  have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_com)
+  also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
+  finally show ?thesis by (simp add: sep_conj_com)
+qed
+
+lemmas sep_conj_ac = sep_conj_com sep_conj_assoc sep_conj_left_com
+
+lemma empty_empty[simp]: "\<box> 0"
+  by (simp add: emp_def)
+
+lemma sep_conj_empty[simp]:
+  "(P ** \<box>) = P"
+  by (simp add: sep_conj_def emp_def)
+
+  lemma sep_conj_empty'[simp]:
+  "(\<box> ** P) = P"
+  by (subst sep_conj_com, rule sep_conj_empty)
+
+lemma sep_conj_sep_emptyI:
+  "P s \<Longrightarrow> (P ** \<box>) s"
+  by simp
+
+lemma sep_conj_true_P[simp]:
+  "(sep_true ** (sep_true ** P)) = (sep_true ** P)"
+  by (simp add: sep_conj_assoc)
+
+lemma sep_conj_disj:
+  "((\<lambda>s. P s \<or> Q s) ** R) s = ((P ** R) s \<or> (Q ** R) s)" (is "?x = (?y \<or> ?z)")
+  by (auto simp: sep_conj_def)
+
+lemma sep_conj_conj:
+  "((\<lambda>s. P s \<and> Q s) ** R) s \<Longrightarrow> (P ** R) s \<and> (Q ** R) s"
+  by (force intro: sep_conjI elim!: sep_conjE)
+
+lemma sep_conj_exists1:
+  "((\<lambda>s. \<exists>x. P x s) ** Q) s = (\<exists>x. (P x ** Q) s)"
+  by (force intro: sep_conjI elim: sep_conjE)
+
+lemma sep_conj_exists2:
+  "(P ** (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P ** Q x) s))"
+  by (force intro!: sep_conjI ext elim!: sep_conjE)
+
+lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
+
+lemma sep_conj_forall:
+  "((\<lambda>s. \<forall>x. P x s) ** Q) s \<Longrightarrow> (P x ** Q) s"
+  by (force intro: sep_conjI elim: sep_conjE)
+
+lemma sep_conj_impl:
+  "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> P' s; \<And>s. Q s \<Longrightarrow> Q' s \<rbrakk> \<Longrightarrow> (P' ** Q') s"
+  by (erule sep_conjE, auto intro!: sep_conjI)
+
+lemma sep_conj_impl1:
+  assumes P: "\<And>s. P s \<Longrightarrow> I s"
+  shows "(P ** R) s \<Longrightarrow> (I ** R) s"
+  by (auto intro: sep_conj_impl P)
+
+lemma sep_conj_sep_true_left:
+  "(P ** Q) s \<Longrightarrow> (sep_true ** Q) s"
+  by (erule sep_conj_impl, simp+)
+
+lemma sep_conj_sep_true_right:
+  "(P ** Q) s \<Longrightarrow> (P ** sep_true) s"
+  by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left,
+      simp add: sep_conj_ac)
+
+lemma sep_globalise:
+  "\<lbrakk> (P ** R) s; (\<And>s. P s \<Longrightarrow> Q s) \<rbrakk> \<Longrightarrow> (Q ** R) s"
+  by (fast elim: sep_conj_impl)
+
+lemma sep_implI:
+  assumes a: "\<And>h' h''. \<lbrakk> h \<oplus> h' = Some h''; P h' \<rbrakk> \<Longrightarrow> Q h''"
+  shows "(P \<longrightarrow>\<^sup>* Q) h"
+  unfolding sep_impl_def by (auto elim: a)
+
+lemma sep_implD:
+  "(x \<longrightarrow>\<^sup>* y) h \<Longrightarrow> \<forall>h' h''. h \<oplus> h' = Some h'' \<and> x h' \<longrightarrow> y h''"
+  by (force simp: sep_impl_def)
+
+lemma sep_impl_sep_true[simp]:
+  "(P \<longrightarrow>\<^sup>* sep_true) = sep_true"
+  by (force intro!: sep_implI ext)
+
+lemma sep_impl_sep_false[simp]:
+  "(sep_false \<longrightarrow>\<^sup>* P) = sep_true"
+  by (force intro!: sep_implI ext)
+
+lemma sep_impl_sep_true_P:
+  "(sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s"
+  apply (drule sep_implD)
+  apply (erule_tac x=0 in allE)
+  apply simp
+  done
+
+lemma sep_impl_sep_true_false[simp]:
+  "(sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false"
+  by (force intro!: ext dest: sep_impl_sep_true_P)
+
+lemma sep_conj_sep_impl:
+  "\<lbrakk> P s; \<And>s. (P ** Q) s \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s"
+proof (rule sep_implI)
+  fix h' h h''
+  assume "P h" and "h \<oplus> h' = Some h''" and "Q h'"
+  hence "(P ** Q) h''" by (force intro: sep_conjI)
+  moreover assume "\<And>s. (P ** Q) s \<Longrightarrow> R s"
+  ultimately show "R h''" by simp
+qed
+
+lemma sep_conj_sep_impl2:
+  "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s \<rbrakk> \<Longrightarrow> R s"
+  by (force dest: sep_implD elim: sep_conjE)
+
+lemma sep_conj_sep_impl_sep_conj2:
+  "(P ** R) s \<Longrightarrow> (P ** (Q \<longrightarrow>\<^sup>* (Q ** R))) s"
+  by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)
+
+lemma sep_conj_triv_strip2:
+  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp
+
+end
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/config	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,9 @@
+# -*- shell-script -*-
+
+# Get email when automated build fails. May be empty.
+# values: "email1 email2 .. emailn"
+NOTIFY="kleing@cse.unsw.edu.au rafal.kolanski@nicta.com.au"
+
+# Participate in frequent (nightly) build (only for small submissions)
+# values: "yes" "no"
+FREQUENT="yes"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/document/root.bib	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,6 @@
+@inproceedings{KleinKB-ITP12,
+author={Gerwin Klein and Rafal Kolanski and Andrew Boyton},
+title={Mechanised Separation Algebra (Rough Diamond)},
+booktitle={Interactive Theorem Proving (ITP 2012)},
+editor={Beringer and Felty},
+publisher={Springer},series={LNCS},volume={},pages={},year=2012}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/document/root.tex	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,67 @@
+% $Id: root.tex,v 1.2 2007-11-12 21:00:45 nipkow Exp $
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also isabellesym.sty)
+% use only when needed
+\usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,
+                                       % \<sqsupset>, \<mho>, \<Join>, 
+                                       % \<lhd>, \<lesssim>, \<greatersim>,
+                                       % \<lessapprox>, \<greaterapprox>,
+                                       % \<triangleq>, \<yen>, \<lozenge>
+%\usepackage[greek,english]{babel}     % greek for \<euro>,
+                                       % english for \<guillemotleft>, 
+                                       %             \<guillemotright>
+                                       % default language = last
+%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
+                                       % \<twosuperior>, \<onehalf>,
+                                       % \<threesuperior>, \<threequarters>,
+                                       % \<degree>
+%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
+%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
+                                       % (only needed if amssymb not used)
+%\usepackage{textcomp}                 % for \<cent>, \<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Separation Algebra}
+\author{Gerwin Klein and Rafal Kolanski and Andrew Boyton}
+\maketitle
+
+\begin{abstract}
+We present a generic type class implementation of separation
+algebra for Isabelle/HOL as well as lemmas and generic tactics which can
+be used directly for any instantiation of the type class.
+
+The ex directory contains example instantiations that include structures
+such as a heap or virtual memory.
+
+The abstract separation algebra is based upon ``Abstract Separation
+Logic'' by Calcagno et al. These theories are also the basis of
+``Mechanised Separation Algebra'' by the authors \cite{KleinKB-ITP12}.
+
+The aim of this work is to support and significantly reduce the effort
+for future separation logic developments in Isabelle/HOL by factoring
+out the part of separation logic that can be treated abstractly once
+and for all. This includes developing typical default rule sets for
+reasoning as well as automated tactic support for separation logic.
+\end{abstract}
+
+\tableofcontents
+
+% include generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/Sep_Tactics_Test.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,123 @@
+(* Authors: Gerwin Klein and Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+theory Sep_Tactics_Test
+imports "../Sep_Tactics"
+begin
+
+text {* Substitution and forward/backward reasoning *}
+
+typedecl p
+typedecl val
+typedecl heap
+
+arities heap :: sep_algebra
+
+axiomatization
+  points_to :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> bool" and
+  val :: "heap \<Rightarrow> p \<Rightarrow> val"
+where
+  points_to: "(points_to p v ** P) h \<Longrightarrow> val h p = v"
+
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_subst (2) points_to)
+  apply (sep_subst (asm) points_to)
+  apply (sep_subst points_to)
+  oops
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_drule points_to)
+  apply simp
+  oops
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_frule points_to)
+  apply simp
+  oops
+
+consts
+  update :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> heap"
+
+schematic_lemma
+  assumes a: "\<And>P. (stuff p ** P) H \<Longrightarrow> (other_stuff p v ** P) (update p v H)"
+  shows "(X ** Y ** other_stuff p ?v) (update p v H)"
+  apply (sep_rule a)
+  oops
+
+
+text {* Example of low-level rewrites *}
+
+lemma "\<lbrakk> unrelated s ; (P ** Q ** R) s \<rbrakk> \<Longrightarrow> (A ** B ** Q ** P) s"
+  apply (tactic {* dtac (mk_sep_select_rule @{context} true (3,1)) 1 *})
+  apply (tactic {* rtac (mk_sep_select_rule @{context} false (4,2)) 1 *})
+  (* now sep_conj_impl1 can be used *)
+  apply (erule (1) sep_conj_impl)
+  oops
+
+
+text {* Conjunct selection *}
+
+lemma "(A ** B ** Q ** P) s"
+  apply (sep_select 1)
+  apply (sep_select 3)
+  apply (sep_select 4)
+  oops
+
+lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated"
+  apply (sep_select_asm 2)
+  oops
+
+
+section {* Test cases for @{text sep_cancel}. *}
+
+lemma
+  assumes forward: "\<And>s g p v. A g p v s \<Longrightarrow> AA g p s "
+  shows "\<And>xv yv P s y x s. (A g x yv ** A g y yv ** P) s \<Longrightarrow> (AA g y ** sep_true) s"
+  by (sep_cancel add: forward)
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "(A ** generic ** B) s \<Longrightarrow> ((instance ** B)**A) s"
+  by (sep_cancel add: forward)+
+
+lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s"
+  apply (sep_cancel)
+  oops
+
+lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s"
+  apply (sep_cancel)
+  oops
+
+schematic_lemma tt: "\<lbrakk> (B ** A ** C) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** ?X) s) s"
+  by (sep_cancel)
+
+(* test backtracking on premises with same state *)
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "\<lbrakk> (A ** B) s ; (generic ** Y) s \<rbrakk> \<Longrightarrow> (X ** instance) s"
+  apply (sep_cancel add: forward)
+  oops
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "generic s \<Longrightarrow> instance s"
+  by (sep_cancel add: forward)
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"
+  shows "generic s \<Longrightarrow> (instance2 ** sep_true) s"
+  by (sep_cancel_blast add: forward forward2)
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/Sep_Tactics_Test.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,122 @@
+(* Authors: Gerwin Klein and Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+theory Sep_Tactics_Test
+imports "../Sep_Tactics"
+begin
+
+text {* Substitution and forward/backward reasoning *}
+
+typedecl p
+typedecl val
+typedecl heap
+
+arities heap :: sep_algebra
+
+axiomatization
+  points_to :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> bool" and
+  val :: "heap \<Rightarrow> p \<Rightarrow> val"
+where
+  points_to: "(points_to p v ** P) h \<Longrightarrow> val h p = v"
+
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_subst (2) points_to)
+  apply (sep_subst (asm) points_to)
+  apply (sep_subst points_to)
+  oops
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_drule points_to)
+  apply simp
+  oops
+
+lemma
+  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
+   \<Longrightarrow> Q (val h p) (val h p)"
+  apply (sep_frule points_to)
+  apply simp
+  oops
+
+consts
+  update :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> heap"
+
+schematic_lemma
+  assumes a: "\<And>P. (stuff p ** P) H \<Longrightarrow> (other_stuff p v ** P) (update p v H)"
+  shows "(X ** Y ** other_stuff p ?v) (update p v H)"
+  apply (sep_rule a)
+  oops
+
+
+text {* Example of low-level rewrites *}
+
+lemma "\<lbrakk> unrelated s ; (P ** Q ** R) s \<rbrakk> \<Longrightarrow> (A ** B ** Q ** P) s"
+  apply (tactic {* dtac (mk_sep_select_rule @{context} true (3,1)) 1 *})
+  apply (tactic {* rtac (mk_sep_select_rule @{context} false (4,2)) 1 *})
+  (* now sep_conj_impl1 can be used *)
+  apply (erule (1) sep_conj_impl)
+  oops
+
+
+text {* Conjunct selection *}
+
+lemma "(A ** B ** Q ** P) s"
+  apply (sep_select 1)
+  apply (sep_select 3)
+  apply (sep_select 4)
+  oops
+
+lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated"
+  apply (sep_select_asm 2)
+  oops
+
+
+section {* Test cases for @{text sep_cancel}. *}
+
+lemma
+  assumes forward: "\<And>s g p v. A g p v s \<Longrightarrow> AA g p s "
+  shows "\<And>xv yv P s y x s. (A g x yv ** A g y yv ** P) s \<Longrightarrow> (AA g y ** sep_true) s"
+  by (sep_cancel add: forward)
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "(A ** generic ** B) s \<Longrightarrow> (instance ** sep_true) s"
+  by (sep_cancel add: forward)
+
+lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s"
+  apply (sep_cancel)
+  oops
+
+lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s"
+  apply (sep_cancel)
+  oops
+
+schematic_lemma "\<lbrakk> (B ** A ** C) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** ?X) s) s"
+  by (sep_cancel)
+
+(* test backtracking on premises with same state *)
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "\<lbrakk> (A ** B) s ; (generic ** Y) s \<rbrakk> \<Longrightarrow> (X ** instance) s"
+  apply (sep_cancel add: forward)
+  oops
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  shows "generic s \<Longrightarrow> instance s"
+  by (sep_cancel add: forward)
+
+lemma
+  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
+  assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"
+  shows "generic s \<Longrightarrow> (instance2 ** sep_true) s"
+  by (sep_cancel_blast add: forward forward2)
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/Simple_Separation_Example.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,109 @@
+(* Title: Adaptation of example from HOL/Hoare/Separation
+   Author: Gerwin Klein, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Example from HOL/Hoare/Separation"
+
+theory Simple_Separation_Example
+  imports "~~/src/HOL/Hoare/Hoare_Logic_Abort" "../Sep_Heap_Instance"
+          "../Sep_Tactics"
+begin
+
+declare [[syntax_ambiguity_warning = false]]
+
+type_synonym heap = "(nat \<Rightarrow> nat option)"
+
+(* This syntax isn't ideal, but this is what is used in the original *)
+definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56)
+  where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]"
+
+(* If you don't mind syntax ambiguity: *)
+notation pred_ex  (binder "\<exists>" 10)
+
+(* could be generated automatically *)
+definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56)
+  where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y"
+
+
+(* could be generated automatically *)
+lemma maps_to_maps_to_ex [elim!]:
+  "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s"
+  by (auto simp: maps_to_ex_def)
+
+(* The basic properties of maps_to: *)
+lemma maps_to_write:
+  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))"
+  apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits)
+  apply (rule_tac x=y in exI)
+  apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits)
+  done
+
+lemma points_to:
+  "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v"
+  by (auto elim!: sep_conjE
+           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
+           split: option.splits)
+
+
+(* This differs from the original and uses separation logic for the definition. *)
+primrec
+  list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool"
+where
+  "list i [] = (\<langle>i=0\<rangle> and \<box>)"
+| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))"
+
+lemma list_empty [simp]:
+  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)"
+  by (cases xs) auto
+
+(* The examples from Hoare/Separation.thy *)
+lemma "VARS x y z w h
+ {(x \<mapsto> y ** z \<mapsto> w) h}
+ SKIP
+ {x \<noteq> z}"
+  apply vcg
+  apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv)
+done
+
+lemma "VARS H x y z w
+ {(P ** Q) H}
+ SKIP
+ {(Q ** P) H}"
+  apply vcg
+  apply(simp add: sep_conj_commute)
+done
+
+lemma "VARS H
+ {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}
+ H := H(p \<mapsto> q)
+ {list p (p#qs) H}"
+  apply vcg
+  apply (auto intro: maps_to_write)
+done
+
+lemma "VARS H p q r
+  {(list p Ps ** list q Qs) H}
+  WHILE p \<noteq> 0
+  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
+  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
+  {list q (rev Ps @ Qs) H}"
+  apply vcg
+    apply fastforce
+   apply clarsimp
+   apply (case_tac ps, simp)
+   apply (rename_tac p ps')
+   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
+   apply (sep_subst points_to)
+   apply (rule_tac x = "ps'" in exI)
+   apply (rule_tac x = "p # qs" in exI)
+   apply (simp add: sep_conj_exists sep_conj_ac)
+   apply (rule exI)
+   apply (sep_rule maps_to_write)
+   apply (sep_cancel)+
+   apply ((sep_cancel add: maps_to_maps_to_ex)+)[1]
+  apply clarsimp
+  done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/Simple_Separation_Example.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,109 @@
+(* Title: Adaptation of example from HOL/Hoare/Separation
+   Author: Gerwin Klein, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Example from HOL/Hoare/Separation"
+
+theory Simple_Separation_Example
+  imports "~~/src/HOL/Hoare/Hoare_Logic_Abort" "../Sep_Heap_Instance"
+          "../Sep_Tactics"
+begin
+
+declare [[syntax_ambiguity_warning = false]]
+
+type_synonym heap = "(nat \<Rightarrow> nat option)"
+
+(* This syntax isn't ideal, but this is what is used in the original *)
+definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56)
+  where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]"
+
+(* If you don't mind syntax ambiguity: *)
+notation pred_ex  (binder "\<exists>" 10)
+
+(* could be generated automatically *)
+definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56)
+  where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y"
+
+
+(* could be generated automatically *)
+lemma maps_to_maps_to_ex [elim!]:
+  "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s"
+  by (auto simp: maps_to_ex_def)
+
+(* The basic properties of maps_to: *)
+lemma maps_to_write:
+  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))"
+  apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits)
+  apply (rule_tac x=y in exI)
+  apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits)
+  done
+
+lemma points_to:
+  "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v"
+  by (auto elim!: sep_conjE
+           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
+           split: option.splits)
+
+
+(* This differs from the original and uses separation logic for the definition. *)
+primrec
+  list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool"
+where
+  "list i [] = (\<langle>i=0\<rangle> and \<box>)"
+| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))"
+
+lemma list_empty [simp]:
+  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)"
+  by (cases xs) auto
+
+(* The examples from Hoare/Separation.thy *)
+lemma "VARS x y z w h
+ {(x \<mapsto> y ** z \<mapsto> w) h}
+ SKIP
+ {x \<noteq> z}"
+  apply vcg
+  apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv)
+done
+
+lemma "VARS H x y z w
+ {(P ** Q) H}
+ SKIP
+ {(Q ** P) H}"
+  apply vcg
+  apply(simp add: sep_conj_commute)
+done
+
+lemma "VARS H
+ {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}
+ H := H(p \<mapsto> q)
+ {list p (p#qs) H}"
+  apply vcg
+  apply (auto intro: maps_to_write)
+done
+
+lemma "VARS H p q r
+  {(list p Ps ** list q Qs) H}
+  WHILE p \<noteq> 0
+  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
+  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
+  {list q (rev Ps @ Qs) H}"
+  apply vcg
+    apply fastforce
+   apply clarsimp
+   apply (case_tac ps, simp)
+   apply (rename_tac p ps')
+   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
+   apply (sep_subst points_to)
+   apply (rule_tac x = "ps'" in exI)
+   apply (rule_tac x = "p # qs" in exI)
+   apply (simp add: sep_conj_exists sep_conj_ac)
+   apply (rule exI)
+   apply (sep_rule maps_to_write)
+   apply (sep_cancel)+
+   apply ((sep_cancel add: maps_to_maps_to_ex)+)[1]
+  apply clarsimp
+  done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/VM_Example.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,78 @@
+(* Title: Adaptation of example from HOL/Hoare/Separation
+   Author: Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Separation Algebra for Virtual Memory"
+
+theory VM_Example
+imports "../Sep_Tactics" "../Map_Extra"
+begin
+
+text {*
+  Example instantiation of the abstract separation algebra to the sliced-memory
+  model used for building a separation logic in ``Verification of Programs in
+  Virtual Memory Using Separation Logic'' (PhD Thesis) by Rafal Kolanski.
+
+  We wrap up the concept of physical and virtual pointers as well as value
+  (usually a byte), and the page table root, into a datatype for instantiation.
+  This avoids having to produce a hierarchy of type classes.
+
+  The result is more general than the original. It does not mention the types
+  of pointers or virtual memory addresses. Instead of supporting only
+  singleton page table roots, we now support sets so we can identify a single
+  0 for the monoid.
+  This models multiple page tables in memory, whereas the original logic was
+  only capable of one at a time.
+*}
+
+datatype ('p,'v,'value,'r) vm_sep_state
+  = VMSepState "((('p \<times> 'v) \<rightharpoonup> 'value) \<times> 'r set)"
+
+instantiation vm_sep_state :: (type, type, type, type) sep_algebra
+begin
+
+fun
+  vm_heap :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> (('a \<times> 'b) \<rightharpoonup> 'c)" where
+  "vm_heap (VMSepState (h,r)) = h"
+
+fun
+  vm_root :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> 'd set" where
+  "vm_root (VMSepState (h,r)) = r"
+
+definition
+  sep_disj_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state
+                            \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state \<Rightarrow> bool" where
+  "sep_disj_vm_sep_state x y = vm_heap x \<bottom> vm_heap y"
+
+definition
+  zero_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state" where
+  "zero_vm_sep_state \<equiv> VMSepState (empty, {})"
+
+fun
+  plus_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state
+                        \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state
+                        \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state" where
+  "plus_vm_sep_state (VMSepState (x,r)) (VMSepState (y,r'))
+     = VMSepState (x ++ y, r \<union> r')"
+
+instance
+  apply default
+        apply (simp add: zero_vm_sep_state_def sep_disj_vm_sep_state_def)
+       apply (fastforce simp: sep_disj_vm_sep_state_def map_disj_def)
+      apply (case_tac x, clarsimp simp: zero_vm_sep_state_def)
+     apply (case_tac x, case_tac y)
+     apply (fastforce simp: sep_disj_vm_sep_state_def map_add_ac)
+    apply (case_tac x, case_tac y, case_tac z)
+    apply (fastforce simp: sep_disj_vm_sep_state_def)
+   apply (case_tac x, case_tac y, case_tac z)
+   apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj)
+  apply (case_tac x, case_tac y, case_tac z)
+  apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj map_disj_com)
+  done
+
+end
+
+end
+