diff -r 77daf1b85cf0 -r a5f5b9336007 Separation_Algebra/ex/Simple_Separation_Example.thy
--- /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