24 | X loc |
24 | X loc |
25 | Op1 "nat => nat" aexp |
25 | Op1 "nat => nat" aexp |
26 | Op2 "nat => nat => nat" aexp aexp |
26 | Op2 "nat => nat => nat" aexp aexp |
27 |
27 |
28 subsection "Evaluation of arithmetic expressions" |
28 subsection "Evaluation of arithmetic expressions" |
29 consts evala :: "((aexp*state) * nat) set" |
29 |
30 syntax "_evala" :: "[aexp*state,nat] => bool" (infixl "-a->" 50) |
30 inductive |
31 translations |
31 evala :: "[aexp*state,nat] => bool" (infixl "-a->" 50) |
32 "aesig -a-> n" == "(aesig,n) : evala" |
32 where |
33 inductive evala |
|
34 intros |
|
35 N: "(N(n),s) -a-> n" |
33 N: "(N(n),s) -a-> n" |
36 X: "(X(x),s) -a-> s(x)" |
34 | X: "(X(x),s) -a-> s(x)" |
37 Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" |
35 | Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" |
38 Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] |
36 | Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] |
39 ==> (Op2 f e0 e1,s) -a-> f n0 n1" |
37 ==> (Op2 f e0 e1,s) -a-> f n0 n1" |
40 |
38 |
41 lemmas [intro] = N X Op1 Op2 |
39 lemmas [intro] = N X Op1 Op2 |
42 |
40 |
43 |
41 |
50 | noti bexp |
48 | noti bexp |
51 | andi bexp bexp (infixl "andi" 60) |
49 | andi bexp bexp (infixl "andi" 60) |
52 | ori bexp bexp (infixl "ori" 60) |
50 | ori bexp bexp (infixl "ori" 60) |
53 |
51 |
54 subsection "Evaluation of boolean expressions" |
52 subsection "Evaluation of boolean expressions" |
55 consts evalb :: "((bexp*state) * bool)set" |
|
56 syntax "_evalb" :: "[bexp*state,bool] => bool" (infixl "-b->" 50) |
|
57 |
53 |
58 translations |
54 inductive |
59 "besig -b-> b" == "(besig,b) : evalb" |
55 evalb :: "[bexp*state,bool] => bool" (infixl "-b->" 50) |
60 |
|
61 inductive evalb |
|
62 -- "avoid clash with ML constructors true, false" |
56 -- "avoid clash with ML constructors true, false" |
63 intros |
57 where |
64 tru: "(true,s) -b-> True" |
58 tru: "(true,s) -b-> True" |
65 fls: "(false,s) -b-> False" |
59 | fls: "(false,s) -b-> False" |
66 ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] |
60 | ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] |
67 ==> (ROp f a0 a1,s) -b-> f n0 n1" |
61 ==> (ROp f a0 a1,s) -b-> f n0 n1" |
68 noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" |
62 | noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" |
69 andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
63 | andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
70 ==> (b0 andi b1,s) -b-> (w0 & w1)" |
64 ==> (b0 andi b1,s) -b-> (w0 & w1)" |
71 ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
65 | ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] |
72 ==> (b0 ori b1,s) -b-> (w0 | w1)" |
66 ==> (b0 ori b1,s) -b-> (w0 | w1)" |
73 |
67 |
74 lemmas [intro] = tru fls ROp noti andi ori |
68 lemmas [intro] = tru fls ROp noti andi ori |
75 |
69 |
76 subsection "Denotational semantics of arithmetic and boolean expressions" |
70 subsection "Denotational semantics of arithmetic and boolean expressions" |
115 by (rule,cases set: evalb) auto |
109 by (rule,cases set: evalb) auto |
116 |
110 |
117 lemma [simp]: |
111 lemma [simp]: |
118 "((ROp f a0 a1,sigma) -b-> w) = |
112 "((ROp f a0 a1,sigma) -b-> w) = |
119 (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" |
113 (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" |
120 by (rule,cases set: evalb) auto |
114 by (rule,cases set: evalb) blast+ |
121 |
115 |
122 lemma [simp]: |
116 lemma [simp]: |
123 "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" |
117 "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" |
124 by (rule,cases set: evalb) auto |
118 by (rule,cases set: evalb) blast+ |
125 |
119 |
126 lemma [simp]: |
120 lemma [simp]: |
127 "((b0 andi b1,sigma) -b-> w) = |
121 "((b0 andi b1,sigma) -b-> w) = |
128 (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" |
122 (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" |
129 by (rule,cases set: evalb) auto |
123 by (rule,cases set: evalb) blast+ |
130 |
124 |
131 lemma [simp]: |
125 lemma [simp]: |
132 "((b0 ori b1,sigma) -b-> w) = |
126 "((b0 ori b1,sigma) -b-> w) = |
133 (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" |
127 (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" |
134 by (rule,cases set: evalb) auto |
128 by (rule,cases set: evalb) blast+ |
135 |
129 |
136 |
130 |
137 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" |
131 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" |
138 by (induct a arbitrary: n) auto |
132 by (induct a arbitrary: n) auto |
139 |
133 |