--- 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 *}
--- 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)
--- 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)"
--- 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:
--- 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
--- 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:
--- 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>
--- 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 *}
--- 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)
--- 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: *}