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