--- /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