diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/ex/Simple_Separation_Example.thy~
--- a/Separation_Algebra/ex/Simple_Separation_Example.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* 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