1.1 --- a/src/HOL/IMP/Com.thy Wed Jun 25 21:25:51 2008 +0200
1.2 +++ b/src/HOL/IMP/Com.thy Wed Jun 25 22:01:34 2008 +0200
1.3 @@ -28,9 +28,9 @@
1.4 | Cond bexp com com ("IF _ THEN _ ELSE _" 60)
1.5 | While bexp com ("WHILE _ DO _" 60)
1.6
1.7 -syntax (latex)
1.8 - SKIP :: com ("\<SKIP>")
1.9 - Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com" ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
1.10 - While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _" 60)
1.11 +notation (latex)
1.12 + SKIP ("\<SKIP>") and
1.13 + Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and
1.14 + While ("\<WHILE> _ \<DO> _" 60)
1.15
1.16 end
2.1 --- a/src/HOL/IMP/Compiler.thy Wed Jun 25 21:25:51 2008 +0200
2.2 +++ b/src/HOL/IMP/Compiler.thy Wed Jun 25 22:01:34 2008 +0200
2.3 @@ -8,16 +8,16 @@
2.4
2.5 subsection "The compiler"
2.6
2.7 -consts compile :: "com \<Rightarrow> instr list"
2.8 -primrec
2.9 -"compile \<SKIP> = []"
2.10 -"compile (x:==a) = [SET x a]"
2.11 -"compile (c1;c2) = compile c1 @ compile c2"
2.12 -"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
2.13 - [JMPF b (length(compile c1) + 1)] @ compile c1 @
2.14 - [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
2.15 -"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
2.16 - [JMPB (length(compile c)+1)]"
2.17 +primrec compile :: "com \<Rightarrow> instr list"
2.18 +where
2.19 + "compile \<SKIP> = []"
2.20 +| "compile (x:==a) = [SET x a]"
2.21 +| "compile (c1;c2) = compile c1 @ compile c2"
2.22 +| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
2.23 + [JMPF b (length(compile c1) + 1)] @ compile c1 @
2.24 + [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
2.25 +| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
2.26 + [JMPB (length(compile c)+1)]"
2.27
2.28 subsection "Compiler correctness"
2.29
2.30 @@ -65,31 +65,33 @@
2.31 lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
2.32 by(simp add: rtrancl_is_UN_rel_pow)
2.33
2.34 -constdefs
2.35 - forws :: "instr \<Rightarrow> nat set"
2.36 -"forws instr == case instr of
2.37 - SET x a \<Rightarrow> {0} |
2.38 - JMPF b n \<Rightarrow> {0,n} |
2.39 - JMPB n \<Rightarrow> {}"
2.40 - backws :: "instr \<Rightarrow> nat set"
2.41 -"backws instr == case instr of
2.42 - SET x a \<Rightarrow> {} |
2.43 - JMPF b n \<Rightarrow> {} |
2.44 - JMPB n \<Rightarrow> {n}"
2.45 +definition
2.46 + forws :: "instr \<Rightarrow> nat set" where
2.47 + "forws instr = (case instr of
2.48 + SET x a \<Rightarrow> {0} |
2.49 + JMPF b n \<Rightarrow> {0,n} |
2.50 + JMPB n \<Rightarrow> {})"
2.51
2.52 -consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
2.53 -primrec
2.54 -"closed m n [] = True"
2.55 -"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
2.56 - (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
2.57 +definition
2.58 + backws :: "instr \<Rightarrow> nat set" where
2.59 + "backws instr = (case instr of
2.60 + SET x a \<Rightarrow> {} |
2.61 + JMPF b n \<Rightarrow> {} |
2.62 + JMPB n \<Rightarrow> {n})"
2.63 +
2.64 +primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
2.65 +where
2.66 + "closed m n [] = True"
2.67 +| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
2.68 + (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
2.69
2.70 lemma [simp]:
2.71 "\<And>m n. closed m n (C1@C2) =
2.72 (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
2.73 -by(induct C1, simp, simp add:add_ac)
2.74 +by(induct C1) (simp, simp add:add_ac)
2.75
2.76 theorem [simp]: "\<And>m n. closed m n (compile c)"
2.77 -by(induct c, simp_all add:backws_def forws_def)
2.78 +by(induct c) (simp_all add:backws_def forws_def)
2.79
2.80 lemma drop_lem: "n \<le> size(p1@p2)
2.81 \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
3.1 --- a/src/HOL/IMP/Denotation.thy Wed Jun 25 21:25:51 2008 +0200
3.2 +++ b/src/HOL/IMP/Denotation.thy Wed Jun 25 22:01:34 2008 +0200
3.3 @@ -10,21 +10,19 @@
3.4
3.5 types com_den = "(state\<times>state)set"
3.6
3.7 -constdefs
3.8 - Gamma :: "[bexp,com_den] => (com_den => com_den)"
3.9 - "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
3.10 +definition
3.11 + Gamma :: "[bexp,com_den] => (com_den => com_den)" where
3.12 + "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
3.13 {(s,t). s=t \<and> \<not>b s})"
3.14
3.15 -consts
3.16 - C :: "com => com_den"
3.17 -
3.18 -primrec
3.19 +primrec C :: "com => com_den"
3.20 +where
3.21 C_skip: "C \<SKIP> = Id"
3.22 - C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
3.23 - C_comp: "C (c0;c1) = C(c1) O C(c0)"
3.24 - C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
3.25 +| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
3.26 +| C_comp: "C (c0;c1) = C(c1) O C(c0)"
3.27 +| C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
3.28 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
3.29 - C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
3.30 +| C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
3.31
3.32
3.33 (**** mono (Gamma(b,c)) ****)
4.1 --- a/src/HOL/IMP/Examples.thy Wed Jun 25 21:25:51 2008 +0200
4.2 +++ b/src/HOL/IMP/Examples.thy Wed Jun 25 22:01:34 2008 +0200
4.3 @@ -8,11 +8,11 @@
4.4
4.5 theory Examples imports Natural begin
4.6
4.7 -constdefs
4.8 - factorial :: "loc => loc => com"
4.9 - "factorial a b == b :== (%s. 1);
4.10 +definition
4.11 + factorial :: "loc => loc => com" where
4.12 + "factorial a b = (b :== (%s. 1);
4.13 \<WHILE> (%s. s a ~= 0) \<DO>
4.14 - (b :== (%s. s b * s a); a :== (%s. s a - 1))"
4.15 + (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
4.16
4.17 declare update_def [simp]
4.18
5.1 --- a/src/HOL/IMP/Expr.thy Wed Jun 25 21:25:51 2008 +0200
5.2 +++ b/src/HOL/IMP/Expr.thy Wed Jun 25 22:01:34 2008 +0200
5.3 @@ -68,23 +68,22 @@
5.4 lemmas [intro] = tru fls ROp noti andi ori
5.5
5.6 subsection "Denotational semantics of arithmetic and boolean expressions"
5.7 -consts
5.8 - A :: "aexp => state => nat"
5.9 - B :: "bexp => state => bool"
5.10
5.11 -primrec
5.12 +primrec A :: "aexp => state => nat"
5.13 +where
5.14 "A(N(n)) = (%s. n)"
5.15 - "A(X(x)) = (%s. s(x))"
5.16 - "A(Op1 f a) = (%s. f(A a s))"
5.17 - "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
5.18 +| "A(X(x)) = (%s. s(x))"
5.19 +| "A(Op1 f a) = (%s. f(A a s))"
5.20 +| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
5.21
5.22 -primrec
5.23 +primrec B :: "bexp => state => bool"
5.24 +where
5.25 "B(true) = (%s. True)"
5.26 - "B(false) = (%s. False)"
5.27 - "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
5.28 - "B(noti(b)) = (%s. ~(B b s))"
5.29 - "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
5.30 - "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
5.31 +| "B(false) = (%s. False)"
5.32 +| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
5.33 +| "B(noti(b)) = (%s. ~(B b s))"
5.34 +| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
5.35 +| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
5.36
5.37 lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
5.38 by (rule,cases set: evala) auto
6.1 --- a/src/HOL/IMP/Hoare.thy Wed Jun 25 21:25:51 2008 +0200
6.2 +++ b/src/HOL/IMP/Hoare.thy Wed Jun 25 22:01:34 2008 +0200
6.3 @@ -10,8 +10,9 @@
6.4
6.5 types assn = "state => bool"
6.6
6.7 -constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
6.8 - "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
6.9 +definition
6.10 + hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
6.11 + "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
6.12
6.13 inductive
6.14 hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
6.15 @@ -26,8 +27,9 @@
6.16 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
6.17 |- {P'}c{Q'}"
6.18
6.19 -constdefs wp :: "com => assn => assn"
6.20 - "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
6.21 +definition
6.22 + wp :: "com => assn => assn" where
6.23 + "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
6.24
6.25 (*
6.26 Soundness (and part of) relative completeness of Hoare rules
7.1 --- a/src/HOL/IMP/Natural.thy Wed Jun 25 21:25:51 2008 +0200
7.2 +++ b/src/HOL/IMP/Natural.thy Wed Jun 25 22:01:34 2008 +0200
7.3 @@ -18,12 +18,12 @@
7.4 @{text "(c,s,s')"} is part of the relation @{text evalc}}:
7.5 *}
7.6
7.7 -constdefs
7.8 - update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
7.9 - "update == fun_upd"
7.10 +definition
7.11 + update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
7.12 + "update = fun_upd"
7.13
7.14 -syntax (xsymbols)
7.15 - update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
7.16 +notation (xsymbols)
7.17 + update ("_/[_ \<mapsto> /_]" [900,0,0] 900)
7.18
7.19 text {*
7.20 The big-step execution relation @{text evalc} is defined inductively:
7.21 @@ -104,9 +104,9 @@
7.22 in @{text s'} iff @{text c'} started in the same @{text s} also terminates
7.23 in the same @{text s'}}. Formally:
7.24 *}
7.25 -constdefs
7.26 - equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
7.27 - "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
7.28 +definition
7.29 + equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
7.30 + "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
7.31
7.32 text {*
7.33 Proof rules telling Isabelle to unfold the definition
8.1 --- a/src/HOL/IMP/Transition.thy Wed Jun 25 21:25:51 2008 +0200
8.2 +++ b/src/HOL/IMP/Transition.thy Wed Jun 25 22:01:34 2008 +0200
8.3 @@ -25,21 +25,20 @@
8.4 Some syntactic sugar that we will use to hide the
8.5 @{text option} part in configurations:
8.6 *}
8.7 -syntax
8.8 - "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
8.9 - "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
8.10 +abbreviation
8.11 + angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where
8.12 + "<c,s> == (Some c, s)"
8.13 +abbreviation
8.14 + angle2 :: "state \<Rightarrow> com option \<times> state" ("<_>") where
8.15 + "<s> == (None, s)"
8.16
8.17 -syntax (xsymbols)
8.18 - "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
8.19 - "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
8.20 +notation (xsymbols)
8.21 + angle ("\<langle>_,_\<rangle>") and
8.22 + angle2 ("\<langle>_\<rangle>")
8.23
8.24 -syntax (HTML output)
8.25 - "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
8.26 - "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
8.27 -
8.28 -translations
8.29 - "\<langle>c,s\<rangle>" == "(Some c, s)"
8.30 - "\<langle>s\<rangle>" == "(None, s)"
8.31 +notation (HTML output)
8.32 + angle ("\<langle>_,_\<rangle>") and
8.33 + angle2 ("\<langle>_\<rangle>")
8.34
8.35 text {*
8.36 Now, finally, we are set to write down the rules for our small step semantics:
9.1 --- a/src/HOL/IMP/VC.thy Wed Jun 25 21:25:51 2008 +0200
9.2 +++ b/src/HOL/IMP/VC.thy Wed Jun 25 22:01:34 2008 +0200
9.3 @@ -18,46 +18,44 @@
9.4 | Aif bexp acom acom
9.5 | Awhile bexp assn acom
9.6
9.7 -consts
9.8 - vc :: "acom => assn => assn"
9.9 - awp :: "acom => assn => assn"
9.10 - vcawp :: "acom => assn => assn \<times> assn"
9.11 - astrip :: "acom => com"
9.12 +primrec awp :: "acom => assn => assn"
9.13 +where
9.14 + "awp Askip Q = Q"
9.15 +| "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
9.16 +| "awp (Asemi c d) Q = awp c (awp d Q)"
9.17 +| "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
9.18 +| "awp (Awhile b I c) Q = I"
9.19
9.20 -primrec
9.21 - "awp Askip Q = Q"
9.22 - "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
9.23 - "awp (Asemi c d) Q = awp c (awp d Q)"
9.24 - "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
9.25 - "awp (Awhile b I c) Q = I"
9.26 -
9.27 -primrec
9.28 +primrec vc :: "acom => assn => assn"
9.29 +where
9.30 "vc Askip Q = (\<lambda>s. True)"
9.31 - "vc (Aass x a) Q = (\<lambda>s. True)"
9.32 - "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
9.33 - "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
9.34 - "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
9.35 +| "vc (Aass x a) Q = (\<lambda>s. True)"
9.36 +| "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
9.37 +| "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
9.38 +| "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
9.39 (I s & b s --> awp c I s) & vc c I s)"
9.40
9.41 -primrec
9.42 +primrec astrip :: "acom => com"
9.43 +where
9.44 "astrip Askip = SKIP"
9.45 - "astrip (Aass x a) = (x:==a)"
9.46 - "astrip (Asemi c d) = (astrip c;astrip d)"
9.47 - "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
9.48 - "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
9.49 +| "astrip (Aass x a) = (x:==a)"
9.50 +| "astrip (Asemi c d) = (astrip c;astrip d)"
9.51 +| "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
9.52 +| "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
9.53
9.54 (* simultaneous computation of vc and awp: *)
9.55 -primrec
9.56 +primrec vcawp :: "acom => assn => assn \<times> assn"
9.57 +where
9.58 "vcawp Askip Q = (\<lambda>s. True, Q)"
9.59 - "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
9.60 - "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
9.61 +| "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
9.62 +| "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
9.63 (vcc,wpc) = vcawp c wpd
9.64 in (\<lambda>s. vcc s & vcd s, wpc))"
9.65 - "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
9.66 +| "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
9.67 (vcc,wpc) = vcawp c Q
9.68 in (\<lambda>s. vcc s & vcd s,
9.69 \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
9.70 - "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
9.71 +| "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
9.72 in (\<lambda>s. (I s & ~b s --> Q s) &
9.73 (I s & b s --> wpc s) & vcc s, I))"
9.74
10.1 --- a/src/HOL/IMPP/Com.thy Wed Jun 25 21:25:51 2008 +0200
10.2 +++ b/src/HOL/IMPP/Com.thy Wed Jun 25 22:01:34 2008 +0200
10.3 @@ -15,8 +15,8 @@
10.4 typedecl glb
10.5 typedecl loc
10.6
10.7 -consts
10.8 - Arg :: loc
10.9 +axiomatization
10.10 + Arg :: loc and
10.11 Res :: loc
10.12
10.13 datatype vname = Glb glb | Loc loc
10.14 @@ -43,8 +43,9 @@
10.15 | Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60)
10.16
10.17 consts bodies :: "(pname * com) list"(* finitely many procedure definitions *)
10.18 - body :: " pname ~=> com"
10.19 -defs body_def: "body == map_of bodies"
10.20 +definition
10.21 + body :: " pname ~=> com" where
10.22 + "body = map_of bodies"
10.23
10.24
10.25 (* Well-typedness: all procedures called must exist *)
10.26 @@ -78,9 +79,9 @@
10.27 "WT (c1;;c2)" "WT (IF b THEN c1 ELSE c2)" "WT (WHILE b DO c)"
10.28 "WT (BODY P)" "WT (X:=CALL P(a))"
10.29
10.30 -constdefs
10.31 - WT_bodies :: bool
10.32 - "WT_bodies == !(pn,b):set bodies. WT b"
10.33 +definition
10.34 + WT_bodies :: bool where
10.35 + "WT_bodies = (!(pn,b):set bodies. WT b)"
10.36
10.37
10.38 ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
11.1 --- a/src/HOL/IMPP/EvenOdd.thy Wed Jun 25 21:25:51 2008 +0200
11.2 +++ b/src/HOL/IMPP/EvenOdd.thy Wed Jun 25 22:01:34 2008 +0200
11.3 @@ -10,38 +10,41 @@
11.4 imports Misc
11.5 begin
11.6
11.7 -constdefs
11.8 - even :: "nat => bool"
11.9 - "even n == 2 dvd n"
11.10 +definition
11.11 + even :: "nat => bool" where
11.12 + "even n = (2 dvd n)"
11.13
11.14 -consts
11.15 - Even :: pname
11.16 +axiomatization
11.17 + Even :: pname and
11.18 Odd :: pname
11.19 -axioms
11.20 - Even_neq_Odd: "Even ~= Odd"
11.21 +where
11.22 + Even_neq_Odd: "Even ~= Odd" and
11.23 Arg_neq_Res: "Arg ~= Res"
11.24
11.25 -constdefs
11.26 - evn :: com
11.27 - "evn == IF (%s. s<Arg> = 0)
11.28 +definition
11.29 + evn :: com where
11.30 + "evn = (IF (%s. s<Arg> = 0)
11.31 THEN Loc Res:==(%s. 0)
11.32 ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
11.33 Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
11.34 - Loc Res:==(%s. s<Res> * s<Arg>))"
11.35 - odd :: com
11.36 - "odd == IF (%s. s<Arg> = 0)
11.37 + Loc Res:==(%s. s<Res> * s<Arg>)))"
11.38 +
11.39 +definition
11.40 + odd :: com where
11.41 + "odd = (IF (%s. s<Arg> = 0)
11.42 THEN Loc Res:==(%s. 1)
11.43 - ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
11.44 + ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
11.45
11.46 defs
11.47 bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
11.48
11.49 -consts
11.50 - Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50)
11.51 - "even_Z=(Res=0)" :: "nat assn" ("Res'_ok")
11.52 -defs
11.53 - Z_eq_Arg_plus_def: "Z=Arg+n == %Z s. Z = s<Arg>+n"
11.54 - Res_ok_def: "Res_ok == %Z s. even Z = (s<Res> = 0)"
11.55 +definition
11.56 + Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
11.57 + "Z=Arg+n = (%Z s. Z = s<Arg>+n)"
11.58 +
11.59 +definition
11.60 + Res_ok :: "nat assn" where
11.61 + "Res_ok = (%Z s. even Z = (s<Res> = 0))"
11.62
11.63
11.64 subsection "even"
12.1 --- a/src/HOL/IMPP/Natural.thy Wed Jun 25 21:25:51 2008 +0200
12.2 +++ b/src/HOL/IMPP/Natural.thy Wed Jun 25 22:01:34 2008 +0200
12.3 @@ -17,10 +17,10 @@
12.4 setlocs :: "state => locals => state"
12.5 getlocs :: "state => locals"
12.6 update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)
12.7 -syntax (* IN Natural.thy *)
12.8 - loc :: "state => locals" ("_<_>" [75,0] 75)
12.9 -translations
12.10 - "s<X>" == "getlocs s X"
12.11 +
12.12 +abbreviation
12.13 + loc :: "state => locals" ("_<_>" [75,0] 75) where
12.14 + "s<X> == getlocs s X"
12.15
12.16 inductive
12.17 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51)
13.1 --- a/src/HOLCF/IMP/Denotational.thy Wed Jun 25 21:25:51 2008 +0200
13.2 +++ b/src/HOLCF/IMP/Denotational.thy Wed Jun 25 22:01:34 2008 +0200
13.3 @@ -14,15 +14,14 @@
13.4 dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
13.5 "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
13.6
13.7 -consts D :: "com => state discr -> state lift"
13.8 -
13.9 -primrec
13.10 +primrec D :: "com => state discr -> state lift"
13.11 +where
13.12 "D(\<SKIP>) = (LAM s. Def(undiscr s))"
13.13 - "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
13.14 - "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
13.15 - "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
13.16 +| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
13.17 +| "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
13.18 +| "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
13.19 (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
13.20 - "D(\<WHILE> b \<DO> c) =
13.21 +| "D(\<WHILE> b \<DO> c) =
13.22 fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
13.23 else Def(undiscr s))"
13.24