*** empty log message ***
authornipkow
Sun Mar 23 11:57:07 2003 +0100 (2003-03-23)
changeset 1387512997e3ddd8d
parent 13874 0da2141606c6
child 13876 68f4ed8311ac
*** empty log message ***
src/HOL/Hoare/ExamplesAbort.thy
src/HOL/Hoare/Heap.thy
src/HOL/Hoare/HeapSyntax.thy
src/HOL/Hoare/HeapSyntaxAbort.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/Pointer_Examples.thy
src/HOL/Hoare/Pointer_ExamplesAbort.thy
src/HOL/Hoare/Pointers.thy
src/HOL/Hoare/README.html
src/HOL/Hoare/ROOT.ML
src/HOL/Hoare/SchorrWaite.thy
src/HOL/Hoare/Separation.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hoare/ExamplesAbort.thy	Fri Mar 21 18:16:18 2003 +0100
     1.2 +++ b/src/HOL/Hoare/ExamplesAbort.thy	Sun Mar 23 11:57:07 2003 +0100
     1.3 @@ -4,26 +4,27 @@
     1.4      Copyright   1998 TUM
     1.5  
     1.6  Some small examples for programs that may abort.
     1.7 -Currently only show the absence of abort.
     1.8  *)
     1.9  
    1.10  theory ExamplesAbort = HoareAbort:
    1.11  
    1.12 -syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
    1.13 -translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
    1.14 -
    1.15  lemma "VARS x y z::nat
    1.16   {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
    1.17  by vcg_simp
    1.18  
    1.19 +lemma
    1.20 + "VARS a i j
    1.21 + {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
    1.22 +apply vcg_simp
    1.23 +apply arith
    1.24 +done
    1.25 +
    1.26  lemma "VARS (a::int list) i
    1.27   {True}
    1.28   i := 0;
    1.29   WHILE i < length a
    1.30   INV {i <= length a}
    1.31 - DO i < length a \<rightarrow> a := a[i := 7];
    1.32 -    i := i+1
    1.33 - OD
    1.34 + DO a[i] := 7; i := i+1 OD
    1.35   {True}"
    1.36  apply vcg_simp
    1.37  apply arith
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Hoare/Heap.thy	Sun Mar 23 11:57:07 2003 +0100
     2.3 @@ -0,0 +1,162 @@
     2.4 +(*  Title:      HOL/Hoare/Heap.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   2002 TUM
     2.8 +
     2.9 +Pointers, heaps and heap abstractions.
    2.10 +See the paper by Mehta and Nipkow.
    2.11 +*)
    2.12 +
    2.13 +theory Heap = Main:
    2.14 +
    2.15 +subsection "References"
    2.16 +
    2.17 +datatype 'a ref = Null | Ref 'a
    2.18 +
    2.19 +lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
    2.20 +  by (induct x) auto
    2.21 +
    2.22 +lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
    2.23 +  by (induct x) auto
    2.24 +
    2.25 +consts addr :: "'a ref \<Rightarrow> 'a"
    2.26 +primrec "addr(Ref a) = a"
    2.27 +
    2.28 +
    2.29 +section "The heap"
    2.30 +
    2.31 +subsection "Paths in the heap"
    2.32 +
    2.33 +consts
    2.34 + Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    2.35 +primrec
    2.36 +"Path h x [] y = (x = y)"
    2.37 +"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
    2.38 +
    2.39 +lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
    2.40 +apply(case_tac xs)
    2.41 +apply fastsimp
    2.42 +apply fastsimp
    2.43 +done
    2.44 +
    2.45 +lemma [simp]: "Path h (Ref a) as z =
    2.46 + (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
    2.47 +apply(case_tac as)
    2.48 +apply fastsimp
    2.49 +apply fastsimp
    2.50 +done
    2.51 +
    2.52 +lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    2.53 +by(induct as, simp+)
    2.54 +
    2.55 +lemma Path_upd[simp]:
    2.56 + "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    2.57 +by(induct as, simp, simp add:eq_sym_conv)
    2.58 +
    2.59 +lemma Path_snoc:
    2.60 + "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
    2.61 +by simp
    2.62 +
    2.63 +
    2.64 +subsection "Lists on the heap"
    2.65 +
    2.66 +subsubsection "Relational abstraction"
    2.67 +
    2.68 +constdefs
    2.69 + List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
    2.70 +"List h x as == Path h x as Null"
    2.71 +
    2.72 +lemma [simp]: "List h x [] = (x = Null)"
    2.73 +by(simp add:List_def)
    2.74 +
    2.75 +lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
    2.76 +by(simp add:List_def)
    2.77 +
    2.78 +lemma [simp]: "List h Null as = (as = [])"
    2.79 +by(case_tac as, simp_all)
    2.80 +
    2.81 +lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
    2.82 +by(case_tac as, simp_all, fast)
    2.83 +
    2.84 +theorem notin_List_update[simp]:
    2.85 + "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
    2.86 +apply(induct as)
    2.87 +apply simp
    2.88 +apply(clarsimp simp add:fun_upd_apply)
    2.89 +done
    2.90 +
    2.91 +lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
    2.92 +by(induct as, simp, clarsimp)
    2.93 +
    2.94 +lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
    2.95 +by(blast intro:List_unique)
    2.96 +
    2.97 +lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
    2.98 +by(induct as, simp, clarsimp)
    2.99 +
   2.100 +lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
   2.101 +apply (clarsimp simp add:in_set_conv_decomp)
   2.102 +apply(frule List_app[THEN iffD1])
   2.103 +apply(fastsimp dest: List_unique)
   2.104 +done
   2.105 +
   2.106 +lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
   2.107 +apply(induct as, simp)
   2.108 +apply(fastsimp dest:List_hd_not_in_tl)
   2.109 +done
   2.110 +
   2.111 +subsection "Functional abstraction"
   2.112 +
   2.113 +constdefs
   2.114 + islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
   2.115 +"islist h p == \<exists>as. List h p as"
   2.116 + list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   2.117 +"list h p == SOME as. List h p as"
   2.118 +
   2.119 +lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
   2.120 +apply(simp add:islist_def list_def)
   2.121 +apply(rule iffI)
   2.122 +apply(rule conjI)
   2.123 +apply blast
   2.124 +apply(subst some1_equality)
   2.125 +  apply(erule List_unique1)
   2.126 + apply assumption
   2.127 +apply(rule refl)
   2.128 +apply simp
   2.129 +apply(rule someI_ex)
   2.130 +apply fast
   2.131 +done
   2.132 +
   2.133 +lemma [simp]: "islist h Null"
   2.134 +by(simp add:islist_def)
   2.135 +
   2.136 +lemma [simp]: "islist h (Ref a) = islist h (h a)"
   2.137 +by(simp add:islist_def)
   2.138 +
   2.139 +lemma [simp]: "list h Null = []"
   2.140 +by(simp add:list_def)
   2.141 +
   2.142 +lemma list_Ref_conv[simp]:
   2.143 + "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
   2.144 +apply(insert List_Ref[of h])
   2.145 +apply(fastsimp simp:List_conv_islist_list)
   2.146 +done
   2.147 +
   2.148 +lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
   2.149 +apply(insert List_hd_not_in_tl[of h])
   2.150 +apply(simp add:List_conv_islist_list)
   2.151 +done
   2.152 +
   2.153 +lemma list_upd_conv[simp]:
   2.154 + "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
   2.155 +apply(drule notin_List_update[of _ _ h q p])
   2.156 +apply(simp add:List_conv_islist_list)
   2.157 +done
   2.158 +
   2.159 +lemma islist_upd[simp]:
   2.160 + "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
   2.161 +apply(frule notin_List_update[of _ _ h q p])
   2.162 +apply(simp add:List_conv_islist_list)
   2.163 +done
   2.164 +
   2.165 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Hoare/HeapSyntax.thy	Sun Mar 23 11:57:07 2003 +0100
     3.3 @@ -0,0 +1,39 @@
     3.4 +(*  Title:      HOL/Hoare/HeapSyntax.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   2002 TUM
     3.8 +*)
     3.9 +
    3.10 +theory HeapSyntax = Hoare + Heap:
    3.11 +
    3.12 +subsection "Field access and update"
    3.13 +
    3.14 +syntax
    3.15 +  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    3.16 +   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    3.17 +  "@fassign"  :: "'a ref => id => 'v => 's com"
    3.18 +   ("(2_^._ :=/ _)" [70,1000,65] 61)
    3.19 +  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    3.20 +   ("_^._" [65,1000] 65)
    3.21 +translations
    3.22 +  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    3.23 +  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    3.24 +  "p^.f"       =>  "f(addr p)"
    3.25 +
    3.26 +
    3.27 +declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
    3.28 +
    3.29 +
    3.30 +text "An example due to Suzuki:"
    3.31 +
    3.32 +lemma "VARS v n
    3.33 +  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    3.34 +   distinct[w0,x0,y0,z0]}
    3.35 +  w^.v := (1::int); w^.n := x;
    3.36 +  x^.v := 2; x^.n := y;
    3.37 +  y^.v := 3; y^.n := z;
    3.38 +  z^.v := 4; x^.n := z
    3.39 +  {w^.n^.n^.v = 4}"
    3.40 +by vcg_simp
    3.41 +
    3.42 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 23 11:57:07 2003 +0100
     4.3 @@ -0,0 +1,47 @@
     4.4 +(*  Title:      HOL/Hoare/HeapSyntax.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow
     4.7 +    Copyright   2002 TUM
     4.8 +*)
     4.9 +
    4.10 +theory HeapSyntaxAbort = HoareAbort + Heap:
    4.11 +
    4.12 +subsection "Field access and update"
    4.13 +
    4.14 +text{* Heap update @{text"p^.h := e"} is now guarded against @{term p}
    4.15 +being Null. However, @{term p} may still be illegal,
    4.16 +e.g. uninitialized or dangling. To guard against that, one needs a
    4.17 +more detailed model of the heap where allocated and free addresses are
    4.18 +distinguished, e.g. by making the heap a map, or by carrying the set
    4.19 +of free addresses around. This is needed anyway as soon as we want to
    4.20 +reason about storage allocation/deallocation. *}
    4.21 +
    4.22 +syntax
    4.23 +  "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    4.24 +   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    4.25 +  "@fassign"  :: "'a ref => id => 'v => 's com"
    4.26 +   ("(2_^._ :=/ _)" [70,1000,65] 61)
    4.27 +  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    4.28 +   ("_^._" [65,1000] 65)
    4.29 +translations
    4.30 +  "refupdate f r v"  ==  "f(addr r := v)"
    4.31 +  "p^.f := e"  =>  "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
    4.32 +  "p^.f"       =>  "f(addr p)"
    4.33 +
    4.34 +
    4.35 +declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
    4.36 +
    4.37 +
    4.38 +text "An example due to Suzuki:"
    4.39 +
    4.40 +lemma "VARS v n
    4.41 +  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    4.42 +   distinct[w0,x0,y0,z0]}
    4.43 +  w^.v := (1::int); w^.n := x;
    4.44 +  x^.v := 2; x^.n := y;
    4.45 +  y^.v := 3; y^.n := z;
    4.46 +  z^.v := 4; x^.n := z
    4.47 +  {w^.n^.n^.v = 4}"
    4.48 +by vcg_simp
    4.49 +
    4.50 +end
     5.1 --- a/src/HOL/Hoare/HoareAbort.thy	Fri Mar 21 18:16:18 2003 +0100
     5.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Sun Mar 23 11:57:07 2003 +0100
     5.3 @@ -31,20 +31,20 @@
     5.4  
     5.5  consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
     5.6  primrec
     5.7 -"iter 0 b S = (%s s'. s ~: Some ` b & (s=s'))"
     5.8 -"iter (Suc n) b S = (%s s'. s : Some ` b & (? s''. S s s'' & iter n b S s'' s'))"
     5.9 +"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
    5.10 +"iter (Suc n) b S =
    5.11 +  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
    5.12  
    5.13  consts Sem :: "'a com => 'a sem"
    5.14  primrec
    5.15  "Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
    5.16  "Sem Abort s s' = (s' = None)"
    5.17 -"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
    5.18 +"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
    5.19  "Sem(IF b THEN c1 ELSE c2 FI) s s' =
    5.20   (case s of None \<Rightarrow> s' = None
    5.21 -  | Some t \<Rightarrow> ((t : b --> Sem c1 s s') & (t ~: b --> Sem c2 s s')))"
    5.22 +  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
    5.23  "Sem(While b x c) s s' =
    5.24 - (if s = None then s' = None
    5.25 -  else EX n. iter n b (Sem c) s s')"
    5.26 + (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
    5.27  
    5.28  constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    5.29    "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
    5.30 @@ -211,8 +211,9 @@
    5.31    \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
    5.32  by (fastsimp simp:Valid_def image_def)
    5.33  
    5.34 -lemma iter_aux: "! s s'. Sem c s s' --> s : Some ` (I \<inter> b) --> s' : Some ` I ==>
    5.35 -       (\<And>s s'. s : Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : Some ` (I \<inter> -b))";
    5.36 +lemma iter_aux:
    5.37 + "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
    5.38 +  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
    5.39  apply(unfold image_def)
    5.40  apply(induct n)
    5.41   apply clarsimp
    5.42 @@ -247,4 +248,17 @@
    5.43        hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
    5.44    "verification condition generator plus simplification"
    5.45  
    5.46 +(* Special syntax for guarded statements and guarded array updates: *)
    5.47 +
    5.48 +syntax
    5.49 +  guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
    5.50 +  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
    5.51 +translations
    5.52 +  "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
    5.53 +  "a[i] := v" => "(i < length a) \<rightarrow> (a := list_update a i v)"
    5.54 +  (* reverse translation not possible because of duplicate "a" *)
    5.55 +
    5.56 +text{* Note: there is no special syntax for guarded array access. Thus
    5.57 +you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *}
    5.58 +
    5.59  end
     6.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Mar 21 18:16:18 2003 +0100
     6.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 23 11:57:07 2003 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  Examples of verifications of pointer programs
     6.5  *)
     6.6  
     6.7 -theory Pointer_Examples = Pointers:
     6.8 +theory Pointer_Examples = HeapSyntax:
     6.9  
    6.10  section "Verifications"
    6.11  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Sun Mar 23 11:57:07 2003 +0100
     7.3 @@ -0,0 +1,30 @@
     7.4 +(*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Tobias Nipkow
     7.7 +    Copyright   2002 TUM
     7.8 +
     7.9 +Examples of verifications of pointer programs
    7.10 +*)
    7.11 +
    7.12 +theory Pointer_ExamplesAbort = HeapSyntaxAbort:
    7.13 +
    7.14 +section "Verifications"
    7.15 +
    7.16 +subsection "List reversal"
    7.17 +
    7.18 +text "Interestingly, this proof is the same as for the unguarded program:"
    7.19 +
    7.20 +lemma "VARS tl p q r
    7.21 +  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    7.22 +  WHILE p \<noteq> Null
    7.23 +  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    7.24 +                 rev ps @ qs = rev Ps @ Qs}
    7.25 +  DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
    7.26 +  {List tl q (rev Ps @ Qs)}"
    7.27 +apply vcg_simp
    7.28 +  apply fastsimp
    7.29 + apply(fastsimp intro:notin_List_update[THEN iffD2])
    7.30 +apply fastsimp
    7.31 +done
    7.32 +
    7.33 +end
     8.1 --- a/src/HOL/Hoare/Pointers.thy	Fri Mar 21 18:16:18 2003 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,193 +0,0 @@
     8.4 -(*  Title:      HOL/Hoare/Pointers.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Tobias Nipkow
     8.7 -    Copyright   2002 TUM
     8.8 -
     8.9 -How to use Hoare logic to verify pointer manipulating programs.
    8.10 -The old idea: the store is a global mapping from pointers to values.
    8.11 -See the paper by Mehta and Nipkow.
    8.12 -*)
    8.13 -
    8.14 -theory Pointers = Hoare:
    8.15 -
    8.16 -subsection "References"
    8.17 -
    8.18 -datatype 'a ref = Null | Ref 'a
    8.19 -
    8.20 -lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
    8.21 -  by (induct x) auto
    8.22 -
    8.23 -lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
    8.24 -  by (induct x) auto
    8.25 -
    8.26 -consts addr :: "'a ref \<Rightarrow> 'a"
    8.27 -primrec "addr(Ref a) = a"
    8.28 -
    8.29 -subsection "Field access and update"
    8.30 -
    8.31 -syntax
    8.32 -  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    8.33 -   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    8.34 -  "@fassign"  :: "'a ref => id => 'v => 's com"
    8.35 -   ("(2_^._ :=/ _)" [70,1000,65] 61)
    8.36 -  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    8.37 -   ("_^._" [65,1000] 65)
    8.38 -translations
    8.39 -  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    8.40 -  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    8.41 -  "p^.f"       =>  "f(addr p)"
    8.42 -
    8.43 -
    8.44 -text "An example due to Suzuki:"
    8.45 -
    8.46 -lemma "VARS v n
    8.47 -  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    8.48 -   distinct[w0,x0,y0,z0]}
    8.49 -  w^.v := (1::int); w^.n := x;
    8.50 -  x^.v := 2; x^.n := y;
    8.51 -  y^.v := 3; y^.n := z;
    8.52 -  z^.v := 4; x^.n := z
    8.53 -  {w^.n^.n^.v = 4}"
    8.54 -by vcg_simp
    8.55 -
    8.56 -
    8.57 -section "The heap"
    8.58 -
    8.59 -subsection "Paths in the heap"
    8.60 -
    8.61 -consts
    8.62 - Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    8.63 -primrec
    8.64 -"Path h x [] y = (x = y)"
    8.65 -"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
    8.66 -
    8.67 -lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
    8.68 -apply(case_tac xs)
    8.69 -apply fastsimp
    8.70 -apply fastsimp
    8.71 -done
    8.72 -
    8.73 -lemma [simp]: "Path h (Ref a) as z =
    8.74 - (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
    8.75 -apply(case_tac as)
    8.76 -apply fastsimp
    8.77 -apply fastsimp
    8.78 -done
    8.79 -
    8.80 -lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    8.81 -by(induct as, simp+)
    8.82 -
    8.83 -lemma Path_upd[simp]:
    8.84 - "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    8.85 -by(induct as, simp, simp add:eq_sym_conv)
    8.86 -
    8.87 -lemma Path_snoc:
    8.88 - "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
    8.89 -by simp
    8.90 -
    8.91 -
    8.92 -subsection "Lists on the heap"
    8.93 -
    8.94 -subsubsection "Relational abstraction"
    8.95 -
    8.96 -constdefs
    8.97 - List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
    8.98 -"List h x as == Path h x as Null"
    8.99 -
   8.100 -lemma [simp]: "List h x [] = (x = Null)"
   8.101 -by(simp add:List_def)
   8.102 -
   8.103 -lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
   8.104 -by(simp add:List_def)
   8.105 -
   8.106 -lemma [simp]: "List h Null as = (as = [])"
   8.107 -by(case_tac as, simp_all)
   8.108 -
   8.109 -lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
   8.110 -by(case_tac as, simp_all, fast)
   8.111 -
   8.112 -theorem notin_List_update[simp]:
   8.113 - "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
   8.114 -apply(induct as)
   8.115 -apply simp
   8.116 -apply(clarsimp simp add:fun_upd_apply)
   8.117 -done
   8.118 -
   8.119 -
   8.120 -declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]
   8.121 -
   8.122 -lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
   8.123 -by(induct as, simp, clarsimp)
   8.124 -
   8.125 -lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
   8.126 -by(blast intro:List_unique)
   8.127 -
   8.128 -lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
   8.129 -by(induct as, simp, clarsimp)
   8.130 -
   8.131 -lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
   8.132 -apply (clarsimp simp add:in_set_conv_decomp)
   8.133 -apply(frule List_app[THEN iffD1])
   8.134 -apply(fastsimp dest: List_unique)
   8.135 -done
   8.136 -
   8.137 -lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
   8.138 -apply(induct as, simp)
   8.139 -apply(fastsimp dest:List_hd_not_in_tl)
   8.140 -done
   8.141 -
   8.142 -subsection "Functional abstraction"
   8.143 -
   8.144 -constdefs
   8.145 - islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
   8.146 -"islist h p == \<exists>as. List h p as"
   8.147 - list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   8.148 -"list h p == SOME as. List h p as"
   8.149 -
   8.150 -lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
   8.151 -apply(simp add:islist_def list_def)
   8.152 -apply(rule iffI)
   8.153 -apply(rule conjI)
   8.154 -apply blast
   8.155 -apply(subst some1_equality)
   8.156 -  apply(erule List_unique1)
   8.157 - apply assumption
   8.158 -apply(rule refl)
   8.159 -apply simp
   8.160 -apply(rule someI_ex)
   8.161 -apply fast
   8.162 -done
   8.163 -
   8.164 -lemma [simp]: "islist h Null"
   8.165 -by(simp add:islist_def)
   8.166 -
   8.167 -lemma [simp]: "islist h (Ref a) = islist h (h a)"
   8.168 -by(simp add:islist_def)
   8.169 -
   8.170 -lemma [simp]: "list h Null = []"
   8.171 -by(simp add:list_def)
   8.172 -
   8.173 -lemma list_Ref_conv[simp]:
   8.174 - "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
   8.175 -apply(insert List_Ref[of h])
   8.176 -apply(fastsimp simp:List_conv_islist_list)
   8.177 -done
   8.178 -
   8.179 -lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
   8.180 -apply(insert List_hd_not_in_tl[of h])
   8.181 -apply(simp add:List_conv_islist_list)
   8.182 -done
   8.183 -
   8.184 -lemma list_upd_conv[simp]:
   8.185 - "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
   8.186 -apply(drule notin_List_update[of _ _ h q p])
   8.187 -apply(simp add:List_conv_islist_list)
   8.188 -done
   8.189 -
   8.190 -lemma islist_upd[simp]:
   8.191 - "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
   8.192 -apply(frule notin_List_update[of _ _ h q p])
   8.193 -apply(simp add:List_conv_islist_list)
   8.194 -done
   8.195 -
   8.196 -end
     9.1 --- a/src/HOL/Hoare/README.html	Fri Mar 21 18:16:18 2003 +0100
     9.2 +++ b/src/HOL/Hoare/README.html	Sun Mar 23 11:57:07 2003 +0100
     9.3 @@ -18,7 +18,7 @@
     9.4  
     9.5  After loading theory Hoare, you can state goals of the form
     9.6  <PRE>
     9.7 -|- VARS x y ... . {P} prog {Q}
     9.8 +|- VARS x y ... {P} prog {Q}
     9.9  </PRE>
    9.10  where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
    9.11  precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
    10.1 --- a/src/HOL/Hoare/ROOT.ML	Fri Mar 21 18:16:18 2003 +0100
    10.2 +++ b/src/HOL/Hoare/ROOT.ML	Sun Mar 23 11:57:07 2003 +0100
    10.3 @@ -8,3 +8,5 @@
    10.4  time_use_thy "ExamplesAbort";
    10.5  time_use_thy "Pointers0";
    10.6  time_use_thy "Pointer_Examples";
    10.7 +time_use_thy "Pointer_ExamplesAbort";
    10.8 +time_use_thy "SchorrWaite";
    11.1 --- a/src/HOL/Hoare/SchorrWaite.thy	Fri Mar 21 18:16:18 2003 +0100
    11.2 +++ b/src/HOL/Hoare/SchorrWaite.thy	Sun Mar 23 11:57:07 2003 +0100
    11.3 @@ -7,13 +7,7 @@
    11.4  *)
    11.5  
    11.6  
    11.7 -theory SchorrWaite = Pointers:
    11.8 -
    11.9 -syntax comment1 :: "'a \<Rightarrow> nat \<Rightarrow> 'a" ("_ --- _" [1000,0] 999)
   11.10 -       comment2 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" ("-- _ _" [0,1000] 1000)
   11.11 -translations
   11.12 - "-- i x" => "x"
   11.13 - "x --- i" => "x"
   11.14 +theory SchorrWaite = HeapSyntax:
   11.15  
   11.16  section {* Machinery for the Schorr-Waite proof*}
   11.17  
   11.18 @@ -203,23 +197,23 @@
   11.19   t := root; p := Null;
   11.20   WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
   11.21   INV {\<exists>stack.
   11.22 -          List (S c l r) p stack \<and>                                         -- (i1)
   11.23 -          (\<forall>x \<in> set stack. m x) \<and>                                        -- (i2)
   11.24 -          R = reachable (relS{l, r}) {t,p} \<and>                           -- (i3)
   11.25 -          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        -- (i4)
   11.26 +          List (S c l r) p stack \<and>                                         (*i1*)
   11.27 +          (\<forall>x \<in> set stack. m x) \<and>                                        (*i2*)
   11.28 +          R = reachable (relS{l, r}) {t,p} \<and>                           (*i3*)
   11.29 +          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        (*i4*)
   11.30                   x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
   11.31 -          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         -- (i5)
   11.32 -          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       -- (i6)
   11.33 -          (stkOk c l r iL iR t stack)                                    --- (i7) }
   11.34 +          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         (*i5*)
   11.35 +          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       (*i6*)
   11.36 +          (stkOk c l r iL iR t stack)                                    (*i7*) }
   11.37   DO IF t = Null \<or> t^.m
   11.38        THEN IF p^.c
   11.39 -               THEN q := t; t := p; p := p^.r; t^.r := q               --- pop
   11.40 -               ELSE q := t; t := p^.r; p^.r := p^.l;                      -- swing
   11.41 +               THEN q := t; t := p; p := p^.r; t^.r := q               (*pop*)
   11.42 +               ELSE q := t; t := p^.r; p^.r := p^.l;                      (*swing*)
   11.43                          p^.l := q; p^.c := True          FI    
   11.44 -      ELSE q := p; p := t; t := t^.l; p^.l := q;                         -- push
   11.45 +      ELSE q := p; p := t; t := t^.l; p^.l := q;                         (*push*)
   11.46                 p^.m := True; p^.c := False            FI       OD
   11.47   {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
   11.48 -  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}") 
   11.49 +  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
   11.50  proof (vcg)
   11.51    let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
   11.52      {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
    12.1 --- a/src/HOL/Hoare/Separation.thy	Fri Mar 21 18:16:18 2003 +0100
    12.2 +++ b/src/HOL/Hoare/Separation.thy	Sun Mar 23 11:57:07 2003 +0100
    12.3 @@ -6,21 +6,27 @@
    12.4  text{* The semantic definition of a few connectives: *}
    12.5  
    12.6  constdefs
    12.7 - R:: "heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> bool"
    12.8 -"R h h1 h2 == dom h1 \<inter> dom h2 = {} \<and> h = h1 ++ h2"
    12.9 + ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
   12.10 +"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
   12.11  
   12.12 - star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   12.13 -"star P Q == \<lambda>h. \<exists>h1 h2. R h h1 h2 \<and> P h1 \<and> Q h2"
   12.14 + is_empty :: "heap \<Rightarrow> bool"
   12.15 +"is_empty h == h = empty"
   12.16  
   12.17   singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   12.18  "singl h x y == dom h = {x} & h x = Some y"
   12.19  
   12.20 + star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   12.21 +"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
   12.22 +
   12.23 + wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   12.24 +"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
   12.25 +
   12.26  lemma "VARS x y z w h
   12.27   {star (%h. singl h x y) (%h. singl h z w) h}
   12.28   SKIP
   12.29   {x \<noteq> z}"
   12.30  apply vcg
   12.31 -apply(auto simp:star_def R_def singl_def)
   12.32 +apply(auto simp:star_def ortho_def singl_def)
   12.33  done
   12.34  
   12.35  text{* To suppress the heap parameter of the connectives, we assume it
   12.36 @@ -32,45 +38,110 @@
   12.37  text{* Nice input syntax: *}
   12.38  
   12.39  syntax
   12.40 + "@emp" :: "bool" ("emp")
   12.41   "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
   12.42   "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
   12.43 + "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-o" 60)
   12.44  
   12.45  ML{*
   12.46 +(* free_tr takes care of free vars in the scope of sep. logic connectives:
   12.47 +   they are implicitly applied to the heap *)
   12.48 +fun free_tr(t as Free _) = t $ Syntax.free "H"
   12.49 +  | free_tr t = t
   12.50 +
   12.51 +fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
   12.52 +  | emp_tr ts = raise TERM ("emp_tr", ts);
   12.53  fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
   12.54    | singl_tr ts = raise TERM ("singl_tr", ts);
   12.55  fun star_tr [P,Q] = Syntax.const "star" $
   12.56 +      absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
   12.57 +      Syntax.free "H"
   12.58 +  | star_tr ts = raise TERM ("star_tr", ts);
   12.59 +fun wand_tr [P,Q] = Syntax.const "wand" $
   12.60        absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
   12.61 -  | star_tr ts = raise TERM ("star_tr", ts);
   12.62 +  | wand_tr ts = raise TERM ("wand_tr", ts);
   12.63  *}
   12.64  
   12.65 -parse_translation {* [("@singl", singl_tr),("@star", star_tr)] *}
   12.66 +parse_translation
   12.67 + {* [("@emp", emp_tr), ("@singl", singl_tr),
   12.68 +     ("@star", star_tr), ("@wand", wand_tr)] *}
   12.69  
   12.70  lemma "VARS H x y z w
   12.71   {[x\<mapsto>y] ** [z\<mapsto>w]}
   12.72   SKIP
   12.73   {x \<noteq> z}"
   12.74  apply vcg
   12.75 -apply(auto simp:star_def R_def singl_def)
   12.76 +apply(auto simp:star_def ortho_def singl_def)
   12.77 +done
   12.78 +
   12.79 +lemma "VARS H x y z w
   12.80 + {emp ** emp}
   12.81 + SKIP
   12.82 + {emp}"
   12.83 +apply vcg
   12.84 +apply(auto simp:star_def ortho_def is_empty_def)
   12.85  done
   12.86  
   12.87  text{* Nice output syntax: *}
   12.88  
   12.89  ML{*
   12.90 +local
   12.91 +fun strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
   12.92 +  | strip (Abs(_,_,(t as Var _) $ Bound 0)) = t
   12.93 +  | strip (Abs(_,_,P)) = P
   12.94 +  | strip (Const("is_empty",_)) = Syntax.const "@emp"
   12.95 +  | strip t = t;
   12.96 +in
   12.97 +fun is_empty_tr' [_] = Syntax.const "@emp"
   12.98  fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
   12.99 -fun star_tr' [Abs(_,_,P),Abs(_,_,Q),_] = Syntax.const "@star" $ P $ Q
  12.100 +fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
  12.101 +fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
  12.102 +end
  12.103  *}
  12.104  
  12.105 -print_translation {* [("singl", singl_tr'),("star", star_tr')] *}
  12.106 +print_translation
  12.107 + {* [("is_empty", is_empty_tr'),("singl", singl_tr'),("star", star_tr')] *}
  12.108  
  12.109  lemma "VARS H x y z w
  12.110   {[x\<mapsto>y] ** [z\<mapsto>w]}
  12.111   y := w
  12.112   {x \<noteq> z}"
  12.113  apply vcg
  12.114 -apply(auto simp:star_def R_def singl_def)
  12.115 +apply(auto simp:star_def ortho_def singl_def)
  12.116 +done
  12.117 +
  12.118 +lemma "VARS H x y z w
  12.119 + {emp ** emp}
  12.120 + SKIP
  12.121 + {emp}"
  12.122 +apply vcg
  12.123 +apply(auto simp:star_def ortho_def is_empty_def)
  12.124 +done
  12.125 +
  12.126 +(* move to Map.thy *)
  12.127 +lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
  12.128 +apply(rule ext)
  12.129 +apply(fastsimp simp:override_def split:option.split)
  12.130  done
  12.131  
  12.132 +(* a law of separation logic *)
  12.133 +(* something is wrong with the pretty printer, but I cannot figure out what. *)
  12.134  
  12.135 +lemma star_comm: "P ** Q = Q ** P"
  12.136 +apply(simp add:star_def ortho_def)
  12.137 +apply(blast intro:override_comm)
  12.138 +done
  12.139 +
  12.140 +lemma "VARS H x y z w
  12.141 + {P ** Q}
  12.142 + SKIP
  12.143 + {Q ** P}"
  12.144 +apply vcg
  12.145 +apply(simp add: star_comm)
  12.146 +done
  12.147 +
  12.148 +end
  12.149 +(*
  12.150  consts llist :: "(heap * nat)set"
  12.151  inductive llist
  12.152  intros
  12.153 @@ -86,5 +157,4 @@
  12.154  prefer 3 apply assumption
  12.155  prefer 2 apply(simp add:singl_def dom_def)
  12.156  apply(simp add:R_def dom_def)
  12.157 -
  12.158 -
  12.159 +*)
  12.160 \ No newline at end of file
    13.1 --- a/src/HOL/IsaMakefile	Fri Mar 21 18:16:18 2003 +0100
    13.2 +++ b/src/HOL/IsaMakefile	Sun Mar 23 11:57:07 2003 +0100
    13.3 @@ -296,8 +296,9 @@
    13.4  
    13.5  $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
    13.6    Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
    13.7 -  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
    13.8 -  Hoare/ExamplesAbort.thy Hoare/hoareAbort.ML Hoare/HoareAbort.thy
    13.9 +  Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
   13.10 +  Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
   13.11 +  Hoare/hoareAbort.ML Hoare/HoareAbort.thy
   13.12  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
   13.13  
   13.14