modernized specifications;
authorwenzelm
Wed Aug 11 18:41:06 2010 +0200 (2010-08-11)
changeset 38353d98baa2cf589
parent 38352 4c8bcb826e83
child 38354 fed4e71a8c0f
modernized specifications;
tuned headers;
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Heap.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Pointer_Examples.thy
src/HOL/Hoare/Pointer_ExamplesAbort.thy
src/HOL/Hoare/Pointers0.thy
src/HOL/Hoare/README.html
src/HOL/Hoare/SchorrWaite.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/Hoare/Separation.thy
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Wed Aug 11 18:22:14 2010 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Wed Aug 11 18:41:06 2010 +0200
     1.3 @@ -9,17 +9,16 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -definition "cd" :: "[nat, nat, nat] => bool" where
     1.8 -  "cd x m n  == x dvd m & x dvd n"
     1.9 -
    1.10 -definition gcd     :: "[nat, nat] => nat" where
    1.11 -  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    1.12 +definition "cd" :: "[nat, nat, nat] => bool"
    1.13 +  where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
    1.14  
    1.15 -consts fac     :: "nat => nat"
    1.16 +definition gcd :: "[nat, nat] => nat"
    1.17 +  where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))"
    1.18  
    1.19 -primrec
    1.20 +primrec fac :: "nat => nat"
    1.21 +where
    1.22    "fac 0 = Suc 0"
    1.23 -  "fac(Suc n) = (Suc n)*fac(n)"
    1.24 +| "fac (Suc n) = Suc n * fac n"
    1.25  
    1.26  
    1.27  subsubsection {* cd *}
     2.1 --- a/src/HOL/Hoare/Heap.thy	Wed Aug 11 18:22:14 2010 +0200
     2.2 +++ b/src/HOL/Hoare/Heap.thy	Wed Aug 11 18:41:06 2010 +0200
     2.3 @@ -57,8 +57,8 @@
     2.4  
     2.5  subsection "Non-repeating paths"
     2.6  
     2.7 -definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
     2.8 -  "distPath h x as y   \<equiv>   Path h x as y  \<and>  distinct as"
     2.9 +definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    2.10 +  where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
    2.11  
    2.12  text{* The term @{term"distPath h x as y"} expresses the fact that a
    2.13  non-repeating path @{term as} connects location @{term x} to location
    2.14 @@ -82,8 +82,8 @@
    2.15  
    2.16  subsubsection "Relational abstraction"
    2.17  
    2.18 -definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.19 -"List h x as == Path h x as Null"
    2.20 +definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
    2.21 +  where "List h x as = Path h x as Null"
    2.22  
    2.23  lemma [simp]: "List h x [] = (x = Null)"
    2.24  by(simp add:List_def)
    2.25 @@ -133,11 +133,11 @@
    2.26  
    2.27  subsection "Functional abstraction"
    2.28  
    2.29 -definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool" where
    2.30 -"islist h p == \<exists>as. List h p as"
    2.31 +definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
    2.32 +  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
    2.33  
    2.34 -definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list" where
    2.35 -"list h p == SOME as. List h p as"
    2.36 +definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    2.37 +  where "list h p = (SOME as. List h p as)"
    2.38  
    2.39  lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
    2.40  apply(simp add:islist_def list_def)
     3.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 18:22:14 2010 +0200
     3.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 18:41:06 2010 +0200
     3.3 @@ -41,8 +41,8 @@
     3.4    "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
     3.5    "Sem (IF b THEN c1 ELSE c2 FI) s s'"
     3.6  
     3.7 -definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
     3.8 -  "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
     3.9 +definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    3.10 +  where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
    3.11  
    3.12  
    3.13  
     4.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:22:14 2010 +0200
     4.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:41:06 2010 +0200
     4.3 @@ -216,18 +216,19 @@
     4.4  
     4.5  text"This is still a bit rough, especially the proof."
     4.6  
     4.7 -definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
     4.8 -"cor P Q == if P then True else Q"
     4.9 +definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    4.10 +  where "cor P Q \<longleftrightarrow> (if P then True else Q)"
    4.11  
    4.12 -definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    4.13 -"cand P Q == if P then Q else False"
    4.14 +definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    4.15 +  where "cand P Q \<longleftrightarrow> (if P then Q else False)"
    4.16  
    4.17 -fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
    4.18 -"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
    4.19 -                                else y # merge(x#xs,ys,f))" |
    4.20 -"merge(x#xs,[],f) = x # merge(xs,[],f)" |
    4.21 -"merge([],y#ys,f) = y # merge([],ys,f)" |
    4.22 -"merge([],[],f) = []"
    4.23 +fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
    4.24 +where
    4.25 +  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
    4.26 +                                  else y # merge(x#xs,ys,f))"
    4.27 +| "merge(x#xs,[],f) = x # merge(xs,[],f)"
    4.28 +| "merge([],y#ys,f) = y # merge([],ys,f)"
    4.29 +| "merge([],[],f) = []"
    4.30  
    4.31  text{* Simplifies the proof a little: *}
    4.32  
    4.33 @@ -336,8 +337,9 @@
    4.34  Path}. Since the result is not that convincing, we do not prove any of
    4.35  the lemmas.*}
    4.36  
    4.37 -consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
    4.38 -       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    4.39 +axiomatization
    4.40 +  ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
    4.41 +  path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    4.42  
    4.43  text"First some basic lemmas:"
    4.44  
    4.45 @@ -479,8 +481,8 @@
    4.46  
    4.47  subsection "Storage allocation"
    4.48  
    4.49 -definition new :: "'a set \<Rightarrow> 'a" where
    4.50 -"new A == SOME a. a \<notin> A"
    4.51 +definition new :: "'a set \<Rightarrow> 'a"
    4.52 +  where "new A = (SOME a. a \<notin> A)"
    4.53  
    4.54  
    4.55  lemma new_notin:
     5.1 --- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 18:22:14 2010 +0200
     5.2 +++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 18:41:06 2010 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7      Copyright   2002 TUM
     5.8  
     6.1 --- a/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 18:22:14 2010 +0200
     6.2 +++ b/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 18:41:06 2010 +0200
     6.3 @@ -44,11 +44,10 @@
     6.4  
     6.5  subsection "Paths in the heap"
     6.6  
     6.7 -consts
     6.8 - Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
     6.9 -primrec
    6.10 -"Path h x [] y = (x = y)"
    6.11 -"Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
    6.12 +primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
    6.13 +where
    6.14 +  "Path h x [] y = (x = y)"
    6.15 +| "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
    6.16  
    6.17  lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
    6.18  apply(case_tac xs)
    6.19 @@ -73,8 +72,8 @@
    6.20  
    6.21  subsubsection "Relational abstraction"
    6.22  
    6.23 -definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
    6.24 -"List h x as == Path h x as Null"
    6.25 +definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
    6.26 +  where "List h x as = Path h x as Null"
    6.27  
    6.28  lemma [simp]: "List h x [] = (x = Null)"
    6.29  by(simp add:List_def)
    6.30 @@ -121,11 +120,11 @@
    6.31  
    6.32  subsection "Functional abstraction"
    6.33  
    6.34 -definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
    6.35 -"islist h p == \<exists>as. List h p as"
    6.36 +definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
    6.37 +  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
    6.38  
    6.39 -definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
    6.40 -"list h p == SOME as. List h p as"
    6.41 +definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
    6.42 +  where "list h p = (SOME as. List h p as)"
    6.43  
    6.44  lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
    6.45  apply(simp add:islist_def list_def)
    6.46 @@ -404,8 +403,8 @@
    6.47  
    6.48  subsection "Storage allocation"
    6.49  
    6.50 -definition new :: "'a set \<Rightarrow> 'a::ref" where
    6.51 -"new A == SOME a. a \<notin> A & a \<noteq> Null"
    6.52 +definition new :: "'a set \<Rightarrow> 'a::ref"
    6.53 +  where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
    6.54  
    6.55  
    6.56  lemma new_notin:
     7.1 --- a/src/HOL/Hoare/README.html	Wed Aug 11 18:22:14 2010 +0200
     7.2 +++ b/src/HOL/Hoare/README.html	Wed Aug 11 18:41:06 2010 +0200
     7.3 @@ -1,7 +1,5 @@
     7.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     7.5  
     7.6 -<!-- $Id$ -->
     7.7 -
     7.8  <HTML>
     7.9  
    7.10  <HEAD>
     8.1 --- a/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 18:22:14 2010 +0200
     8.2 +++ b/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 18:41:06 2010 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Hoare/SchorrWaite.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Farhad Mehta
     8.7      Copyright   2003 TUM
     8.8  
     8.9 @@ -146,14 +145,15 @@
    8.10   apply(simp add:fun_upd_apply S_def)+
    8.11  done
    8.12  
    8.13 -consts
    8.14 +primrec
    8.15    --"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
    8.16    stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
    8.17 -primrec
    8.18 -stkOk_nil:  "stkOk c l r iL iR t [] = True"
    8.19 -stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
    8.20 -                                  iL p = (if c p then l p else t) \<and>
    8.21 -                                  iR p = (if c p then t else r p))"
    8.22 +where
    8.23 +  stkOk_nil:  "stkOk c l r iL iR t [] = True"
    8.24 +| stkOk_cons:
    8.25 +    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
    8.26 +      iL p = (if c p then l p else t) \<and>
    8.27 +      iR p = (if c p then t else r p))"
    8.28  
    8.29  text {* Rewrite rules for stkOk *}
    8.30  
     9.1 --- a/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 18:22:14 2010 +0200
     9.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 18:41:06 2010 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Hoare/Heap.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Tobias Nipkow
     9.7      Copyright   2002 TUM
     9.8  
     9.9 @@ -18,11 +17,10 @@
    9.10  
    9.11  subsection "Paths in the heap"
    9.12  
    9.13 -consts
    9.14 - Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
    9.15 -primrec
    9.16 -"Path h x [] y = (x = y)"
    9.17 -"Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
    9.18 +primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
    9.19 +where
    9.20 +  "Path h x [] y = (x = y)"
    9.21 +| "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
    9.22  
    9.23  lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
    9.24  by (cases xs) simp_all
    9.25 @@ -41,8 +39,8 @@
    9.26  
    9.27  subsection "Lists on the heap"
    9.28  
    9.29 -definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
    9.30 -"List h x as == Path h x as 0"
    9.31 +definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
    9.32 +  where "List h x as = Path h x as 0"
    9.33  
    9.34  lemma [simp]: "List h x [] = (x = 0)"
    9.35  by (simp add: List_def)
    10.1 --- a/src/HOL/Hoare/Separation.thy	Wed Aug 11 18:22:14 2010 +0200
    10.2 +++ b/src/HOL/Hoare/Separation.thy	Wed Aug 11 18:41:06 2010 +0200
    10.3 @@ -16,20 +16,20 @@
    10.4  
    10.5  text{* The semantic definition of a few connectives: *}
    10.6  
    10.7 -definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) where
    10.8 -"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
    10.9 +definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
   10.10 +  where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
   10.11  
   10.12 -definition is_empty :: "heap \<Rightarrow> bool" where
   10.13 -"is_empty h == h = empty"
   10.14 +definition is_empty :: "heap \<Rightarrow> bool"
   10.15 +  where "is_empty h \<longleftrightarrow> h = empty"
   10.16  
   10.17 -definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   10.18 -"singl h x y == dom h = {x} & h x = Some y"
   10.19 +definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   10.20 +  where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
   10.21  
   10.22 -definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
   10.23 -"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
   10.24 +definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   10.25 +  where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
   10.26  
   10.27 -definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
   10.28 -"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
   10.29 +definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   10.30 +  where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
   10.31  
   10.32  text{*This is what assertions look like without any syntactic sugar: *}
   10.33