--- 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
--- /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
--- /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
--- /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
--- 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
--- 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"
--- /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
--- 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
--- 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
--- 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";
--- 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
--- 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
--- 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