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