# HG changeset patch
# User wenzelm
# Date 1281544866 -7200
# Node ID d98baa2cf58929f9a94badc5277351d0b56c6559
# Parent  4c8bcb826e8353086dae378540c03692c0b3499d
modernized specifications;
tuned headers;

diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -9,17 +9,16 @@
 imports Main
 begin
 
-definition "cd" :: "[nat, nat, nat] => bool" where
-  "cd x m n  == x dvd m & x dvd n"
-
-definition gcd     :: "[nat, nat] => nat" where
-  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+definition "cd" :: "[nat, nat, nat] => bool"
+  where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
 
-consts fac     :: "nat => nat"
+definition gcd :: "[nat, nat] => nat"
+  where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))"
 
-primrec
+primrec fac :: "nat => nat"
+where
   "fac 0 = Suc 0"
-  "fac(Suc n) = (Suc n)*fac(n)"
+| "fac (Suc n) = Suc n * fac n"
 
 
 subsubsection {* cd *}
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Heap.thy
--- a/src/HOL/Hoare/Heap.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Heap.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -57,8 +57,8 @@
 
 subsection "Non-repeating paths"
 
-definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
-  "distPath h x as y   \<equiv>   Path h x as y  \<and>  distinct as"
+definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+  where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
 
 text{* The term @{term"distPath h x as y"} expresses the fact that a
 non-repeating path @{term as} connects location @{term x} to location
@@ -82,8 +82,8 @@
 
 subsubsection "Relational abstraction"
 
-definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
@@ -133,11 +133,11 @@
 
 subsection "Functional abstraction"
 
-definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
+  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
-definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+  where "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)
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -41,8 +41,8 @@
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
-  "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
 
 
 
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -216,18 +216,19 @@
 
 text"This is still a bit rough, especially the proof."
 
-definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cor P Q == if P then True else Q"
+definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cor P Q \<longleftrightarrow> (if P then True else Q)"
 
-definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cand P Q == if P then Q else False"
+definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cand P Q \<longleftrightarrow> (if P then Q else False)"
 
-fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
-"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
-                                else y # merge(x#xs,ys,f))" |
-"merge(x#xs,[],f) = x # merge(xs,[],f)" |
-"merge([],y#ys,f) = y # merge([],ys,f)" |
-"merge([],[],f) = []"
+fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
+where
+  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
+                                  else y # merge(x#xs,ys,f))"
+| "merge(x#xs,[],f) = x # merge(xs,[],f)"
+| "merge([],y#ys,f) = y # merge([],ys,f)"
+| "merge([],[],f) = []"
 
 text{* Simplifies the proof a little: *}
 
@@ -336,8 +337,9 @@
 Path}. Since the result is not that convincing, we do not prove any of
 the lemmas.*}
 
-consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
-       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+axiomatization
+  ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
+  path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
 
 text"First some basic lemmas:"
 
@@ -479,8 +481,8 @@
 
 subsection "Storage allocation"
 
-definition new :: "'a set \<Rightarrow> 'a" where
-"new A == SOME a. a \<notin> A"
+definition new :: "'a set \<Rightarrow> 'a"
+  where "new A = (SOME a. a \<notin> A)"
 
 
 lemma new_notin:
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -44,11 +44,10 @@
 
 subsection "Paths in the heap"
 
-consts
- Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
+primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  "Path h x [] y = (x = y)"
+| "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
 
 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
 apply(case_tac xs)
@@ -73,8 +72,8 @@
 
 subsubsection "Relational abstraction"
 
-definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
@@ -121,11 +120,11 @@
 
 subsection "Functional abstraction"
 
-definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
+  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
-definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
+  where "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)
@@ -404,8 +403,8 @@
 
 subsection "Storage allocation"
 
-definition new :: "'a set \<Rightarrow> 'a::ref" where
-"new A == SOME a. a \<notin> A & a \<noteq> Null"
+definition new :: "'a set \<Rightarrow> 'a::ref"
+  where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
 
 
 lemma new_notin:
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/README.html
--- a/src/HOL/Hoare/README.html	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/README.html	Wed Aug 11 18:41:06 2010 +0200
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/SchorrWaite.thy
-    ID:         $Id$
     Author:     Farhad Mehta
     Copyright   2003 TUM
 
@@ -146,14 +145,15 @@
  apply(simp add:fun_upd_apply S_def)+
 done
 
-consts
+primrec
   --"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
   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"
-primrec
-stkOk_nil:  "stkOk c l r iL iR t [] = True"
-stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
-                                  iL p = (if c p then l p else t) \<and>
-                                  iR p = (if c p then t else r p))"
+where
+  stkOk_nil:  "stkOk c l r iL iR t [] = True"
+| stkOk_cons:
+    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
+      iL p = (if c p then l p else t) \<and>
+      iR p = (if c p then t else r p))"
 
 text {* Rewrite rules for stkOk *}
 
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Heap.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
@@ -18,11 +17,10 @@
 
 subsection "Paths in the heap"
 
-consts
- Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"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))"
+primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "Path h x [] y = (x = y)"
+| "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))"
 
 lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
 by (cases xs) simp_all
@@ -41,8 +39,8 @@
 
 subsection "Lists on the heap"
 
-definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
-"List h x as == Path h x as 0"
+definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
+  where "List h x as = Path h x as 0"
 
 lemma [simp]: "List h x [] = (x = 0)"
 by (simp add: List_def)
diff -r 4c8bcb826e83 -r d98baa2cf589 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Separation.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -16,20 +16,20 @@
 
 text{* The semantic definition of a few connectives: *}
 
-definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) where
-"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
+definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
+  where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
 
-definition is_empty :: "heap \<Rightarrow> bool" where
-"is_empty h == h = empty"
+definition is_empty :: "heap \<Rightarrow> bool"
+  where "is_empty h \<longleftrightarrow> h = empty"
 
-definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
-"singl h x y == dom h = {x} & h x = Some y"
+definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
 
-definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
+definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+  where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
 
-definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
+definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+  where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
 
 text{*This is what assertions look like without any syntactic sugar: *}