# HG changeset patch
# User wenzelm
# Date 1214424094 -7200
# Node ID a6dc1769fdda19ae693f4ac5a20401644e74e4c3
# Parent  24ec32bee347f14680d5a9b59958f3a2b5dccab6
modernized specifications;

diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Com.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -28,9 +28,9 @@
       | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
       | While  bexp com         ("WHILE _ DO _"  60)
 
-syntax (latex)
-  SKIP :: com   ("\<SKIP>")
-  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
-  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
+notation (latex)
+  SKIP  ("\<SKIP>") and
+  Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
+  While  ("\<WHILE> _ \<DO> _"  60)
 
 end
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -8,16 +8,16 @@
 
 subsection "The compiler"
 
-consts compile :: "com \<Rightarrow> instr list"
-primrec
-"compile \<SKIP> = []"
-"compile (x:==a) = [SET x a]"
-"compile (c1;c2) = compile c1 @ compile c2"
-"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
- [JMPF b (length(compile c1) + 1)] @ compile c1 @
- [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
-"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
- [JMPB (length(compile c)+1)]"
+primrec compile :: "com \<Rightarrow> instr list"
+where
+  "compile \<SKIP> = []"
+| "compile (x:==a) = [SET x a]"
+| "compile (c1;c2) = compile c1 @ compile c2"
+| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
+    [JMPF b (length(compile c1) + 1)] @ compile c1 @
+    [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
+| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
+    [JMPB (length(compile c)+1)]"
 
 subsection "Compiler correctness"
 
@@ -65,31 +65,33 @@
 lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
 by(simp add: rtrancl_is_UN_rel_pow)
 
-constdefs
- forws :: "instr \<Rightarrow> nat set"
-"forws instr == case instr of
- SET x a \<Rightarrow> {0} |
- JMPF b n \<Rightarrow> {0,n} |
- JMPB n \<Rightarrow> {}"
- backws :: "instr \<Rightarrow> nat set"
-"backws instr == case instr of
- SET x a \<Rightarrow> {} |
- JMPF b n \<Rightarrow> {} |
- JMPB n \<Rightarrow> {n}"
+definition
+  forws :: "instr \<Rightarrow> nat set" where
+  "forws instr = (case instr of
+     SET x a \<Rightarrow> {0} |
+     JMPF b n \<Rightarrow> {0,n} |
+     JMPB n \<Rightarrow> {})"
 
-consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
-primrec
-"closed m n [] = True"
-"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
-                        (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
+definition
+  backws :: "instr \<Rightarrow> nat set" where
+  "backws instr = (case instr of
+     SET x a \<Rightarrow> {} |
+     JMPF b n \<Rightarrow> {} |
+     JMPB n \<Rightarrow> {n})"
+
+primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
+where
+  "closed m n [] = True"
+| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
+                          (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
 
 lemma [simp]:
  "\<And>m n. closed m n (C1@C2) =
          (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
-by(induct C1, simp, simp add:add_ac)
+by(induct C1) (simp, simp add:add_ac)
 
 theorem [simp]: "\<And>m n. closed m n (compile c)"
-by(induct c, simp_all add:backws_def forws_def)
+by(induct c) (simp_all add:backws_def forws_def)
 
 lemma drop_lem: "n \<le> size(p1@p2)
  \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -10,21 +10,19 @@
 
 types com_den = "(state\<times>state)set"
 
-constdefs
-  Gamma :: "[bexp,com_den] => (com_den => com_den)"
-  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+definition
+  Gamma :: "[bexp,com_den] => (com_den => com_den)" where
+  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
                        {(s,t). s=t \<and> \<not>b s})"
 
-consts
-  C :: "com => com_den"
-
-primrec
+primrec C :: "com => com_den"
+where
   C_skip:   "C \<SKIP>   = Id"
-  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
-  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
-  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
+| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
+| C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
+| C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
-  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
+| C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
 
 
 (**** mono (Gamma(b,c)) ****)
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Examples.thy
--- a/src/HOL/IMP/Examples.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Examples.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -8,11 +8,11 @@
 
 theory Examples imports Natural begin
 
-constdefs
-  factorial :: "loc => loc => com"
-  "factorial a b == b :== (%s. 1);
+definition
+  factorial :: "loc => loc => com" where
+  "factorial a b = (b :== (%s. 1);
                     \<WHILE> (%s. s a ~= 0) \<DO>
-                    (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+                    (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
 
 declare update_def [simp]
 
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Expr.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -68,23 +68,22 @@
 lemmas [intro] = tru fls ROp noti andi ori
 
 subsection "Denotational semantics of arithmetic and boolean expressions"
-consts
-  A     :: "aexp => state => nat"
-  B     :: "bexp => state => bool"
 
-primrec
+primrec A :: "aexp => state => nat"
+where
   "A(N(n)) = (%s. n)"
-  "A(X(x)) = (%s. s(x))"
-  "A(Op1 f a) = (%s. f(A a s))"
-  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+| "A(X(x)) = (%s. s(x))"
+| "A(Op1 f a) = (%s. f(A a s))"
+| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
 
-primrec
+primrec B :: "bexp => state => bool"
+where
   "B(true) = (%s. True)"
-  "B(false) = (%s. False)"
-  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-  "B(noti(b)) = (%s. ~(B b s))"
-  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+| "B(false) = (%s. False)"
+| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+| "B(noti(b)) = (%s. ~(B b s))"
+| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
 
 lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
   by (rule,cases set: evala) auto
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Hoare.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -10,8 +10,9 @@
 
 types assn = "state => bool"
 
-constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
-          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
+definition
+  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
 
 inductive
   hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
@@ -26,8 +27,9 @@
 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
           |- {P'}c{Q'}"
 
-constdefs wp :: "com => assn => assn"
-          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
+definition
+  wp :: "com => assn => assn" where
+  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
 
 (*
 Soundness (and part of) relative completeness of Hoare rules
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Natural.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -18,12 +18,12 @@
   @{text "(c,s,s')"} is part of the relation @{text evalc}}:
 *}
 
-constdefs
-  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
-  "update == fun_upd"
+definition
+  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
+  "update = fun_upd"
 
-syntax (xsymbols)
-  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
+notation (xsymbols)
+  update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
 
 text {*
   The big-step execution relation @{text evalc} is defined inductively:
@@ -104,9 +104,9 @@
   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   in the same @{text s'}}. Formally:
 *}
-constdefs
-  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
-  "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
+definition
+  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
+  "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
 
 text {*
   Proof rules telling Isabelle to unfold the definition
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Transition.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -25,21 +25,20 @@
   Some syntactic sugar that we will use to hide the
   @{text option} part in configurations:
 *}
-syntax
-  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
-  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
-
-syntax (xsymbols)
-  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
-  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+abbreviation
+  angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where
+  "<c,s> == (Some c, s)"
+abbreviation
+  angle2 :: "state \<Rightarrow> com option \<times> state"  ("<_>") where
+  "<s> == (None, s)"
 
-syntax (HTML output)
-  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
-  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+notation (xsymbols)
+  angle  ("\<langle>_,_\<rangle>") and
+  angle2  ("\<langle>_\<rangle>")
 
-translations
-  "\<langle>c,s\<rangle>" == "(Some c, s)"
-  "\<langle>s\<rangle>" == "(None, s)"
+notation (HTML output)
+  angle  ("\<langle>_,_\<rangle>") and
+  angle2  ("\<langle>_\<rangle>")
 
 text {*
   Now, finally, we are set to write down the rules for our small step semantics:
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/VC.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -18,46 +18,44 @@
                | Aif    bexp acom acom
                | Awhile bexp assn acom
 
-consts
-  vc :: "acom => assn => assn"
-  awp :: "acom => assn => assn"
-  vcawp :: "acom => assn => assn \<times> assn"
-  astrip :: "acom => com"
-
-primrec
+primrec awp :: "acom => assn => assn"
+where
   "awp Askip Q = Q"
-  "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
-  "awp (Asemi c d) Q = awp c (awp d Q)"
-  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
-  "awp (Awhile b I c) Q = I"
+| "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
+| "awp (Asemi c d) Q = awp c (awp d Q)"
+| "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
+| "awp (Awhile b I c) Q = I"
 
-primrec
+primrec vc :: "acom => assn => assn"
+where
   "vc Askip Q = (\<lambda>s. True)"
-  "vc (Aass x a) Q = (\<lambda>s. True)"
-  "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
-  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
-  "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
+| "vc (Aass x a) Q = (\<lambda>s. True)"
+| "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
+| "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
+| "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
                               (I s & b s --> awp c I s) & vc c I s)"
 
-primrec
+primrec astrip :: "acom => com"
+where
   "astrip Askip = SKIP"
-  "astrip (Aass x a) = (x:==a)"
-  "astrip (Asemi c d) = (astrip c;astrip d)"
-  "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
-  "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
+| "astrip (Aass x a) = (x:==a)"
+| "astrip (Asemi c d) = (astrip c;astrip d)"
+| "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
+| "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
 
 (* simultaneous computation of vc and awp: *)
-primrec
+primrec vcawp :: "acom => assn => assn \<times> assn"
+where
   "vcawp Askip Q = (\<lambda>s. True, Q)"
-  "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
-  "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
+| "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
+| "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c wpd
                           in (\<lambda>s. vcc s & vcd s, wpc))"
-  "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
+| "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c Q
                           in (\<lambda>s. vcc s & vcd s,
                               \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
-  "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
+| "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
                              in (\<lambda>s. (I s & ~b s --> Q s) &
                                      (I s & b s --> wpc s) & vcc s, I))"
 
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMPP/Com.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -15,8 +15,8 @@
 typedecl glb
 typedecl loc
 
-consts
-  Arg :: loc
+axiomatization
+  Arg :: loc and
   Res :: loc
 
 datatype vname  = Glb glb | Loc loc
@@ -43,8 +43,9 @@
       | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)
 
 consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
-       body   :: " pname ~=> com"
-defs   body_def: "body == map_of bodies"
+definition
+  body :: " pname ~=> com" where
+  "body = map_of bodies"
 
 
 (* Well-typedness: all procedures called must exist *)
@@ -78,9 +79,9 @@
   "WT (c1;;c2)"  "WT (IF b THEN c1 ELSE c2)"  "WT (WHILE b DO c)"
   "WT (BODY P)"  "WT (X:=CALL P(a))"
 
-constdefs
-  WT_bodies :: bool
-  "WT_bodies == !(pn,b):set bodies. WT b"
+definition
+  WT_bodies :: bool where
+  "WT_bodies = (!(pn,b):set bodies. WT b)"
 
 
 ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -10,38 +10,41 @@
 imports Misc
 begin
 
-constdefs
-  even :: "nat => bool"
-  "even n == 2 dvd n"
+definition
+  even :: "nat => bool" where
+  "even n = (2 dvd n)"
 
-consts
-  Even :: pname
+axiomatization
+  Even :: pname and
   Odd :: pname
-axioms
-  Even_neq_Odd: "Even ~= Odd"
+where
+  Even_neq_Odd: "Even ~= Odd" and
   Arg_neq_Res:  "Arg  ~= Res"
 
-constdefs
-  evn :: com
- "evn == IF (%s. s<Arg> = 0)
+definition
+  evn :: com where
+ "evn = (IF (%s. s<Arg> = 0)
          THEN Loc Res:==(%s. 0)
          ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
               Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
-              Loc Res:==(%s. s<Res> * s<Arg>))"
-  odd :: com
- "odd == IF (%s. s<Arg> = 0)
+              Loc Res:==(%s. s<Res> * s<Arg>)))"
+
+definition
+  odd :: com where
+ "odd = (IF (%s. s<Arg> = 0)
          THEN Loc Res:==(%s. 1)
-         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
+         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
 
 defs
   bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
 
-consts
-  Z_eq_Arg_plus   :: "nat => nat assn" ("Z=Arg+_" [50]50)
- "even_Z=(Res=0)" ::        "nat assn" ("Res'_ok")
-defs
-  Z_eq_Arg_plus_def: "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
-  Res_ok_def:       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
+definition
+  Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
+  "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
+
+definition
+  Res_ok :: "nat assn" where
+  "Res_ok = (%Z s. even Z = (s<Res> = 0))"
 
 
 subsection "even"
diff -r 24ec32bee347 -r a6dc1769fdda src/HOL/IMPP/Natural.thy
--- a/src/HOL/IMPP/Natural.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMPP/Natural.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -17,10 +17,10 @@
   setlocs :: "state => locals => state"
   getlocs :: "state => locals"
   update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
-syntax (* IN Natural.thy *)
-  loc :: "state => locals"    ("_<_>" [75,0] 75)
-translations
-  "s<X>" == "getlocs s X"
+
+abbreviation
+  loc :: "state => locals"  ("_<_>" [75,0] 75) where
+  "s<X> == getlocs s X"
 
 inductive
   evalc :: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
diff -r 24ec32bee347 -r a6dc1769fdda src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOLCF/IMP/Denotational.thy	Wed Jun 25 22:01:34 2008 +0200
@@ -14,15 +14,14 @@
   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
   "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
 
-consts D :: "com => state discr -> state lift"
-
-primrec
+primrec D :: "com => state discr -> state lift"
+where
   "D(\<SKIP>) = (LAM s. Def(undiscr s))"
-  "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
-  "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
-  "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
+| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
+| "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
+| "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
         (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
-  "D(\<WHILE> b \<DO> c) =
+| "D(\<WHILE> b \<DO> c) =
         fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
                       else Def(undiscr s))"