--- a/src/HOL/Hoare/Hoare.thy Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Hoare.thy Fri Mar 08 13:11:09 1996 +0100
@@ -27,31 +27,30 @@
"@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")
-consts
- (* semantics *)
+constdefs
+ (* denotational semantics *)
Skip :: 'a com
+ "Skip s s' == (s=s')"
+
Assign :: [pvar, 'a exp] => 'a com
+ "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+
Seq :: ['a com, 'a com] => 'a com
+ "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
+
Cond :: ['a bexp, 'a com, 'a com] => 'a com
+ "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
+
While :: ['a bexp, 'a bexp, 'a com] => 'a com
+ "While b inv c s s' == ? n. Iter n b c s s'"
+
Iter :: [nat, 'a bexp, 'a com] => 'a com
+ "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
+ (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
Spec :: ['a bexp, 'a com, 'a bexp] => bool
-
-defs
- (* denotational semantics *)
-
- SkipDef "Skip s s' == (s=s')"
- AssignDef "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
- SeqDef "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
- CondDef "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
- WhileDef "While b inv c s s' == ? n. Iter n b c s s'"
-
- IterDef "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
- (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
-
- SpecDef "Spec p c q == !s s'. c s s' --> p s --> q s'"
+ "Spec p c q == !s s'. c s s' --> p s --> q s'"
end