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