# HG changeset patch
# User nipkow
# Date 1048417027 -3600
# Node ID 12997e3ddd8de746c35988efb0b0cafe7834d570
# Parent  0da2141606c621456030544ba061c07d81ab8147
*** empty log message ***

diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/ExamplesAbort.thy
--- a/src/HOL/Hoare/ExamplesAbort.thy	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -4,26 +4,27 @@
     Copyright   1998 TUM
 
 Some small examples for programs that may abort.
-Currently only show the absence of abort.
 *)
 
 theory ExamplesAbort = HoareAbort:
 
-syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
-translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
-
 lemma "VARS x y z::nat
  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
 by vcg_simp
 
+lemma
+ "VARS a i j
+ {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
+apply vcg_simp
+apply arith
+done
+
 lemma "VARS (a::int list) i
  {True}
  i := 0;
  WHILE i < length a
  INV {i <= length a}
- DO i < length a \<rightarrow> a := a[i := 7];
-    i := i+1
- OD
+ DO a[i] := 7; i := i+1 OD
  {True}"
 apply vcg_simp
 apply arith
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/Heap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Heap.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -0,0 +1,162 @@
+(*  Title:      HOL/Hoare/Heap.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2002 TUM
+
+Pointers, heaps and heap abstractions.
+See the paper by Mehta and Nipkow.
+*)
+
+theory Heap = Main:
+
+subsection "References"
+
+datatype 'a ref = Null | Ref 'a
+
+lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
+  by (induct x) auto
+
+lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
+  by (induct x) auto
+
+consts addr :: "'a ref \<Rightarrow> 'a"
+primrec "addr(Ref a) = a"
+
+
+section "The heap"
+
+subsection "Paths in the heap"
+
+consts
+ Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+primrec
+"Path h x [] y = (x = y)"
+"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
+
+lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
+apply(case_tac xs)
+apply fastsimp
+apply fastsimp
+done
+
+lemma [simp]: "Path h (Ref a) as z =
+ (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
+apply(case_tac as)
+apply fastsimp
+apply fastsimp
+done
+
+lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
+by(induct as, simp+)
+
+lemma Path_upd[simp]:
+ "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
+by(induct as, simp, simp add:eq_sym_conv)
+
+lemma Path_snoc:
+ "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
+by simp
+
+
+subsection "Lists on the heap"
+
+subsubsection "Relational abstraction"
+
+constdefs
+ List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
+"List h x as == Path h x as Null"
+
+lemma [simp]: "List h x [] = (x = Null)"
+by(simp add:List_def)
+
+lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
+by(simp add:List_def)
+
+lemma [simp]: "List h Null as = (as = [])"
+by(case_tac as, simp_all)
+
+lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
+by(case_tac as, simp_all, fast)
+
+theorem notin_List_update[simp]:
+ "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
+apply(induct as)
+apply simp
+apply(clarsimp simp add:fun_upd_apply)
+done
+
+lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
+by(induct as, simp, clarsimp)
+
+lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
+by(blast intro:List_unique)
+
+lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
+by(induct as, simp, clarsimp)
+
+lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
+apply (clarsimp simp add:in_set_conv_decomp)
+apply(frule List_app[THEN iffD1])
+apply(fastsimp dest: List_unique)
+done
+
+lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
+apply(induct as, simp)
+apply(fastsimp dest:List_hd_not_in_tl)
+done
+
+subsection "Functional abstraction"
+
+constdefs
+ islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
+"islist h p == \<exists>as. List h p as"
+ list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+"list h p == SOME as. List h p as"
+
+lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
+apply(simp add:islist_def list_def)
+apply(rule iffI)
+apply(rule conjI)
+apply blast
+apply(subst some1_equality)
+  apply(erule List_unique1)
+ apply assumption
+apply(rule refl)
+apply simp
+apply(rule someI_ex)
+apply fast
+done
+
+lemma [simp]: "islist h Null"
+by(simp add:islist_def)
+
+lemma [simp]: "islist h (Ref a) = islist h (h a)"
+by(simp add:islist_def)
+
+lemma [simp]: "list h Null = []"
+by(simp add:list_def)
+
+lemma list_Ref_conv[simp]:
+ "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
+apply(insert List_Ref[of h])
+apply(fastsimp simp:List_conv_islist_list)
+done
+
+lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
+apply(insert List_hd_not_in_tl[of h])
+apply(simp add:List_conv_islist_list)
+done
+
+lemma list_upd_conv[simp]:
+ "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
+apply(drule notin_List_update[of _ _ h q p])
+apply(simp add:List_conv_islist_list)
+done
+
+lemma islist_upd[simp]:
+ "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
+apply(frule notin_List_update[of _ _ h q p])
+apply(simp add:List_conv_islist_list)
+done
+
+end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/HeapSyntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/HeapSyntax.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOL/Hoare/HeapSyntax.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2002 TUM
+*)
+
+theory HeapSyntax = Hoare + Heap:
+
+subsection "Field access and update"
+
+syntax
+  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
+  "@fassign"  :: "'a ref => id => 'v => 's com"
+   ("(2_^._ :=/ _)" [70,1000,65] 61)
+  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+   ("_^._" [65,1000] 65)
+translations
+  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
+  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
+  "p^.f"       =>  "f(addr p)"
+
+
+declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
+
+
+text "An example due to Suzuki:"
+
+lemma "VARS v n
+  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
+   distinct[w0,x0,y0,z0]}
+  w^.v := (1::int); w^.n := x;
+  x^.v := 2; x^.n := y;
+  y^.v := 3; y^.n := z;
+  z^.v := 4; x^.n := z
+  {w^.n^.n^.v = 4}"
+by vcg_simp
+
+end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/HeapSyntaxAbort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -0,0 +1,47 @@
+(*  Title:      HOL/Hoare/HeapSyntax.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2002 TUM
+*)
+
+theory HeapSyntaxAbort = HoareAbort + Heap:
+
+subsection "Field access and update"
+
+text{* Heap update @{text"p^.h := e"} is now guarded against @{term p}
+being Null. However, @{term p} may still be illegal,
+e.g. uninitialized or dangling. To guard against that, one needs a
+more detailed model of the heap where allocated and free addresses are
+distinguished, e.g. by making the heap a map, or by carrying the set
+of free addresses around. This is needed anyway as soon as we want to
+reason about storage allocation/deallocation. *}
+
+syntax
+  "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
+  "@fassign"  :: "'a ref => id => 'v => 's com"
+   ("(2_^._ :=/ _)" [70,1000,65] 61)
+  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+   ("_^._" [65,1000] 65)
+translations
+  "refupdate f r v"  ==  "f(addr r := v)"
+  "p^.f := e"  =>  "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
+  "p^.f"       =>  "f(addr p)"
+
+
+declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
+
+
+text "An example due to Suzuki:"
+
+lemma "VARS v n
+  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
+   distinct[w0,x0,y0,z0]}
+  w^.v := (1::int); w^.n := x;
+  x^.v := 2; x^.n := y;
+  y^.v := 3; y^.n := z;
+  z^.v := 4; x^.n := z
+  {w^.n^.n^.v = 4}"
+by vcg_simp
+
+end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -31,20 +31,20 @@
 
 consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
 primrec
-"iter 0 b S = (%s s'. s ~: Some ` b & (s=s'))"
-"iter (Suc n) b S = (%s s'. s : Some ` b & (? s''. S s s'' & iter n b S s'' s'))"
+"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
+"iter (Suc n) b S =
+  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
 
 consts Sem :: "'a com => 'a sem"
 primrec
 "Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
 "Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
+"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
 "Sem(IF b THEN c1 ELSE c2 FI) s s' =
  (case s of None \<Rightarrow> s' = None
-  | Some t \<Rightarrow> ((t : b --> Sem c1 s s') & (t ~: b --> Sem c2 s s')))"
+  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
 "Sem(While b x c) s s' =
- (if s = None then s' = None
-  else EX n. iter n b (Sem c) s s')"
+ (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
 
 constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
@@ -211,8 +211,9 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastsimp simp:Valid_def image_def)
 
-lemma iter_aux: "! s s'. Sem c s s' --> s : Some ` (I \<inter> b) --> s' : Some ` I ==>
-       (\<And>s s'. s : Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : Some ` (I \<inter> -b))";
+lemma iter_aux:
+ "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
 apply(unfold image_def)
 apply(induct n)
  apply clarsimp
@@ -247,4 +248,17 @@
       hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
   "verification condition generator plus simplification"
 
+(* Special syntax for guarded statements and guarded array updates: *)
+
+syntax
+  guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
+  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
+translations
+  "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
+  "a[i] := v" => "(i < length a) \<rightarrow> (a := list_update a i v)"
+  (* reverse translation not possible because of duplicate "a" *)
+
+text{* Note: there is no special syntax for guarded array access. Thus
+you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *}
+
 end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -6,7 +6,7 @@
 Examples of verifications of pointer programs
 *)
 
-theory Pointer_Examples = Pointers:
+theory Pointer_Examples = HeapSyntax:
 
 section "Verifications"
 
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -0,0 +1,30 @@
+(*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2002 TUM
+
+Examples of verifications of pointer programs
+*)
+
+theory Pointer_ExamplesAbort = HeapSyntaxAbort:
+
+section "Verifications"
+
+subsection "List reversal"
+
+text "Interestingly, this proof is the same as for the unguarded program:"
+
+lemma "VARS tl p q r
+  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
+  WHILE p \<noteq> Null
+  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
+                 rev ps @ qs = rev Ps @ Qs}
+  DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
+  {List tl q (rev Ps @ Qs)}"
+apply vcg_simp
+  apply fastsimp
+ apply(fastsimp intro:notin_List_update[THEN iffD2])
+apply fastsimp
+done
+
+end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Fri Mar 21 18:16:18 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,193 +0,0 @@
-(*  Title:      HOL/Hoare/Pointers.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   2002 TUM
-
-How to use Hoare logic to verify pointer manipulating programs.
-The old idea: the store is a global mapping from pointers to values.
-See the paper by Mehta and Nipkow.
-*)
-
-theory Pointers = Hoare:
-
-subsection "References"
-
-datatype 'a ref = Null | Ref 'a
-
-lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
-  by (induct x) auto
-
-lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
-  by (induct x) auto
-
-consts addr :: "'a ref \<Rightarrow> 'a"
-primrec "addr(Ref a) = a"
-
-subsection "Field access and update"
-
-syntax
-  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
-   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
-  "@fassign"  :: "'a ref => id => 'v => 's com"
-   ("(2_^._ :=/ _)" [70,1000,65] 61)
-  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
-   ("_^._" [65,1000] 65)
-translations
-  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
-  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
-  "p^.f"       =>  "f(addr p)"
-
-
-text "An example due to Suzuki:"
-
-lemma "VARS v n
-  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
-   distinct[w0,x0,y0,z0]}
-  w^.v := (1::int); w^.n := x;
-  x^.v := 2; x^.n := y;
-  y^.v := 3; y^.n := z;
-  z^.v := 4; x^.n := z
-  {w^.n^.n^.v = 4}"
-by vcg_simp
-
-
-section "The heap"
-
-subsection "Paths in the heap"
-
-consts
- Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
-
-lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
-apply(case_tac xs)
-apply fastsimp
-apply fastsimp
-done
-
-lemma [simp]: "Path h (Ref a) as z =
- (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
-apply(case_tac as)
-apply fastsimp
-apply fastsimp
-done
-
-lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
-by(induct as, simp+)
-
-lemma Path_upd[simp]:
- "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
-by(induct as, simp, simp add:eq_sym_conv)
-
-lemma Path_snoc:
- "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
-by simp
-
-
-subsection "Lists on the heap"
-
-subsubsection "Relational abstraction"
-
-constdefs
- List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
-"List h x as == Path h x as Null"
-
-lemma [simp]: "List h x [] = (x = Null)"
-by(simp add:List_def)
-
-lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
-by(simp add:List_def)
-
-lemma [simp]: "List h Null as = (as = [])"
-by(case_tac as, simp_all)
-
-lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
-by(case_tac as, simp_all, fast)
-
-theorem notin_List_update[simp]:
- "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
-apply(induct as)
-apply simp
-apply(clarsimp simp add:fun_upd_apply)
-done
-
-
-declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]
-
-lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
-by(induct as, simp, clarsimp)
-
-lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
-by(blast intro:List_unique)
-
-lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
-by(induct as, simp, clarsimp)
-
-lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
-apply (clarsimp simp add:in_set_conv_decomp)
-apply(frule List_app[THEN iffD1])
-apply(fastsimp dest: List_unique)
-done
-
-lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
-apply(induct as, simp)
-apply(fastsimp dest:List_hd_not_in_tl)
-done
-
-subsection "Functional abstraction"
-
-constdefs
- islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
-"islist h p == \<exists>as. List h p as"
- list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
-"list h p == SOME as. List h p as"
-
-lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
-apply(simp add:islist_def list_def)
-apply(rule iffI)
-apply(rule conjI)
-apply blast
-apply(subst some1_equality)
-  apply(erule List_unique1)
- apply assumption
-apply(rule refl)
-apply simp
-apply(rule someI_ex)
-apply fast
-done
-
-lemma [simp]: "islist h Null"
-by(simp add:islist_def)
-
-lemma [simp]: "islist h (Ref a) = islist h (h a)"
-by(simp add:islist_def)
-
-lemma [simp]: "list h Null = []"
-by(simp add:list_def)
-
-lemma list_Ref_conv[simp]:
- "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
-apply(insert List_Ref[of h])
-apply(fastsimp simp:List_conv_islist_list)
-done
-
-lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
-apply(insert List_hd_not_in_tl[of h])
-apply(simp add:List_conv_islist_list)
-done
-
-lemma list_upd_conv[simp]:
- "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
-apply(drule notin_List_update[of _ _ h q p])
-apply(simp add:List_conv_islist_list)
-done
-
-lemma islist_upd[simp]:
- "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
-apply(frule notin_List_update[of _ _ h q p])
-apply(simp add:List_conv_islist_list)
-done
-
-end
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/README.html
--- a/src/HOL/Hoare/README.html	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/README.html	Sun Mar 23 11:57:07 2003 +0100
@@ -18,7 +18,7 @@
 
 After loading theory Hoare, you can state goals of the form
 <PRE>
-|- VARS x y ... . {P} prog {Q}
+|- VARS x y ... {P} prog {Q}
 </PRE>
 where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
 precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/ROOT.ML	Sun Mar 23 11:57:07 2003 +0100
@@ -8,3 +8,5 @@
 time_use_thy "ExamplesAbort";
 time_use_thy "Pointers0";
 time_use_thy "Pointer_Examples";
+time_use_thy "Pointer_ExamplesAbort";
+time_use_thy "SchorrWaite";
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/SchorrWaite.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -7,13 +7,7 @@
 *)
 
 
-theory SchorrWaite = Pointers:
-
-syntax comment1 :: "'a \<Rightarrow> nat \<Rightarrow> 'a" ("_ --- _" [1000,0] 999)
-       comment2 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" ("-- _ _" [0,1000] 1000)
-translations
- "-- i x" => "x"
- "x --- i" => "x"
+theory SchorrWaite = HeapSyntax:
 
 section {* Machinery for the Schorr-Waite proof*}
 
@@ -203,23 +197,23 @@
  t := root; p := Null;
  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
  INV {\<exists>stack.
-          List (S c l r) p stack \<and>                                         -- (i1)
-          (\<forall>x \<in> set stack. m x) \<and>                                        -- (i2)
-          R = reachable (relS{l, r}) {t,p} \<and>                           -- (i3)
-          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        -- (i4)
+          List (S c l r) p stack \<and>                                         (*i1*)
+          (\<forall>x \<in> set stack. m x) \<and>                                        (*i2*)
+          R = reachable (relS{l, r}) {t,p} \<and>                           (*i3*)
+          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        (*i4*)
                  x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
-          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         -- (i5)
-          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       -- (i6)
-          (stkOk c l r iL iR t stack)                                    --- (i7) }
+          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         (*i5*)
+          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       (*i6*)
+          (stkOk c l r iL iR t stack)                                    (*i7*) }
  DO IF t = Null \<or> t^.m
       THEN IF p^.c
-               THEN q := t; t := p; p := p^.r; t^.r := q               --- pop
-               ELSE q := t; t := p^.r; p^.r := p^.l;                      -- swing
+               THEN q := t; t := p; p := p^.r; t^.r := q               (*pop*)
+               ELSE q := t; t := p^.r; p^.r := p^.l;                      (*swing*)
                         p^.l := q; p^.c := True          FI    
-      ELSE q := p; p := t; t := t^.l; p^.l := q;                         -- push
+      ELSE q := p; p := t; t := t^.l; p^.l := q;                         (*push*)
                p^.m := True; p^.c := False            FI       OD
  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
-  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}") 
+  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
 proof (vcg)
   let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
     {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/Hoare/Separation.thy	Sun Mar 23 11:57:07 2003 +0100
@@ -6,21 +6,27 @@
 text{* The semantic definition of a few connectives: *}
 
 constdefs
- R:: "heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> bool"
-"R h h1 h2 == dom h1 \<inter> dom h2 = {} \<and> h = h1 ++ h2"
+ ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
+"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
 
- star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
-"star P Q == \<lambda>h. \<exists>h1 h2. R h h1 h2 \<and> P h1 \<and> Q h2"
+ is_empty :: "heap \<Rightarrow> bool"
+"is_empty h == h = empty"
 
  singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 "singl h x y == dom h = {x} & h x = Some y"
 
+ star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
+
+ wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
+
 lemma "VARS x y z w h
  {star (%h. singl h x y) (%h. singl h z w) h}
  SKIP
  {x \<noteq> z}"
 apply vcg
-apply(auto simp:star_def R_def singl_def)
+apply(auto simp:star_def ortho_def singl_def)
 done
 
 text{* To suppress the heap parameter of the connectives, we assume it
@@ -32,45 +38,110 @@
 text{* Nice input syntax: *}
 
 syntax
+ "@emp" :: "bool" ("emp")
  "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
  "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
+ "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-o" 60)
 
 ML{*
+(* free_tr takes care of free vars in the scope of sep. logic connectives:
+   they are implicitly applied to the heap *)
+fun free_tr(t as Free _) = t $ Syntax.free "H"
+  | free_tr t = t
+
+fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
+  | emp_tr ts = raise TERM ("emp_tr", ts);
 fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
   | singl_tr ts = raise TERM ("singl_tr", ts);
 fun star_tr [P,Q] = Syntax.const "star" $
+      absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
+      Syntax.free "H"
+  | star_tr ts = raise TERM ("star_tr", ts);
+fun wand_tr [P,Q] = Syntax.const "wand" $
       absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
-  | star_tr ts = raise TERM ("star_tr", ts);
+  | wand_tr ts = raise TERM ("wand_tr", ts);
 *}
 
-parse_translation {* [("@singl", singl_tr),("@star", star_tr)] *}
+parse_translation
+ {* [("@emp", emp_tr), ("@singl", singl_tr),
+     ("@star", star_tr), ("@wand", wand_tr)] *}
 
 lemma "VARS H x y z w
  {[x\<mapsto>y] ** [z\<mapsto>w]}
  SKIP
  {x \<noteq> z}"
 apply vcg
-apply(auto simp:star_def R_def singl_def)
+apply(auto simp:star_def ortho_def singl_def)
+done
+
+lemma "VARS H x y z w
+ {emp ** emp}
+ SKIP
+ {emp}"
+apply vcg
+apply(auto simp:star_def ortho_def is_empty_def)
 done
 
 text{* Nice output syntax: *}
 
 ML{*
+local
+fun strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
+  | strip (Abs(_,_,(t as Var _) $ Bound 0)) = t
+  | strip (Abs(_,_,P)) = P
+  | strip (Const("is_empty",_)) = Syntax.const "@emp"
+  | strip t = t;
+in
+fun is_empty_tr' [_] = Syntax.const "@emp"
 fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
-fun star_tr' [Abs(_,_,P),Abs(_,_,Q),_] = Syntax.const "@star" $ P $ Q
+fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
+end
 *}
 
-print_translation {* [("singl", singl_tr'),("star", star_tr')] *}
+print_translation
+ {* [("is_empty", is_empty_tr'),("singl", singl_tr'),("star", star_tr')] *}
 
 lemma "VARS H x y z w
  {[x\<mapsto>y] ** [z\<mapsto>w]}
  y := w
  {x \<noteq> z}"
 apply vcg
-apply(auto simp:star_def R_def singl_def)
+apply(auto simp:star_def ortho_def singl_def)
+done
+
+lemma "VARS H x y z w
+ {emp ** emp}
+ SKIP
+ {emp}"
+apply vcg
+apply(auto simp:star_def ortho_def is_empty_def)
+done
+
+(* move to Map.thy *)
+lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
+apply(rule ext)
+apply(fastsimp simp:override_def split:option.split)
 done
 
+(* a law of separation logic *)
+(* something is wrong with the pretty printer, but I cannot figure out what. *)
 
+lemma star_comm: "P ** Q = Q ** P"
+apply(simp add:star_def ortho_def)
+apply(blast intro:override_comm)
+done
+
+lemma "VARS H x y z w
+ {P ** Q}
+ SKIP
+ {Q ** P}"
+apply vcg
+apply(simp add: star_comm)
+done
+
+end
+(*
 consts llist :: "(heap * nat)set"
 inductive llist
 intros
@@ -86,5 +157,4 @@
 prefer 3 apply assumption
 prefer 2 apply(simp add:singl_def dom_def)
 apply(simp add:R_def dom_def)
-
-
+*)
\ No newline at end of file
diff -r 0da2141606c6 -r 12997e3ddd8d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 21 18:16:18 2003 +0100
+++ b/src/HOL/IsaMakefile	Sun Mar 23 11:57:07 2003 +0100
@@ -296,8 +296,9 @@
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
   Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
-  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
-  Hoare/ExamplesAbort.thy Hoare/hoareAbort.ML Hoare/HoareAbort.thy
+  Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
+  Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
+  Hoare/hoareAbort.ML Hoare/HoareAbort.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Hoare