1 (* test *) |
|
2 theory Chap03 |
1 theory Chap03 |
3 imports Main |
2 imports Main |
4 begin |
3 begin |
5 |
4 |
|
5 (* 2.5.6 Case Study: Boolean Expressions *) |
|
6 |
|
7 datatype boolex = Const bool | Var nat | Neg boolex |
|
8 | And boolex boolex |
|
9 |
|
10 primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where |
|
11 "value2 (Const b) env = b" | |
|
12 "value2 (Var x) env = env x" | |
|
13 "value2 (Neg b) env = (\<not> value2 b env)" | |
|
14 "value2 (And b c) env = (value2 b env \<and> value2 c env)" |
|
15 |
|
16 value "Const true" |
|
17 value "Var (Suc(0))" |
|
18 value "value2 (Const False) (\<lambda>x. False)" |
|
19 value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)" |
|
20 value "value2 (Var 11) (\<lambda>x. True )" |
|
21 |
|
22 definition |
|
23 "en1 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)" |
|
24 |
|
25 abbreviation |
|
26 "en2 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)" |
|
27 |
|
28 value "value2 (And (Var 10) (Var 11)) en2" |
|
29 |
|
30 lemma "value2 (And (Var 10) (Var 11)) en2 = True" |
|
31 apply(simp) |
|
32 done |
|
33 |
|
34 datatype ifex = |
|
35 CIF bool |
|
36 | VIF nat |
|
37 | IF ifex ifex ifex |
|
38 |
|
39 primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where |
|
40 "valif (CIF b) env = b" | |
|
41 "valif (VIF x) env = env x" | |
|
42 "valif (IF b t e) env = (if valif b env then valif t env else valif e env)" |
|
43 |
|
44 abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)" |
|
45 abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)" |
|
46 abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)" |
|
47 |
|
48 value "valif (CIF False) (\<lambda>x. False)" |
|
49 value "valif (VIF 11) (\<lambda>x. True)" |
|
50 value "valif (IF (CIF False) (CIF True) (CIF True))" |
|
51 |
|
52 primrec bool2if :: "boolex \<Rightarrow> ifex" where |
|
53 "bool2if (Const b) = CIF b" | |
|
54 "bool2if (Var x) = VIF x" | |
|
55 "bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" | |
|
56 "bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)" |
|
57 |
|
58 lemma "valif (bool2if b) env = value2 b env" |
|
59 apply(induct_tac b) |
|
60 apply(auto) |
|
61 done |
|
62 |
|
63 primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where |
|
64 "normif (CIF b) t e = IF (CIF b) t e" | |
|
65 "normif (VIF x) t e = IF (VIF x) t e" | |
|
66 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)" |
|
67 |
|
68 primrec norm :: "ifex \<Rightarrow> ifex" where |
|
69 "norm (CIF b) = CIF b" | |
|
70 "norm (VIF x) = VIF x" | |
|
71 "norm (IF b t e) = normif b (norm t) (norm e)" |
|
72 |
|
73 (*************** CHAPTER-3 ********************************) |
|
74 |
6 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" |
75 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" |
7 apply simp |
76 apply simp |
8 done |
77 done |
9 |
78 |
10 lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" |
79 lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" |
144 |
215 |
145 primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where |
216 primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where |
146 "value (Cex v) env = v" | |
217 "value (Cex v) env = v" | |
147 "value (Vex a) env = env a" | |
218 "value (Vex a) env = env a" | |
148 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)" |
219 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)" |
|
220 |
|
221 value "value (Cex a) (\<lambda>x. True)" |
149 |
222 |
150 datatype ('a,'v)instr = |
223 datatype ('a,'v)instr = |
151 Const 'v |
224 Const 'v |
152 | Load 'a |
225 | Load 'a |
153 | Apply "'v binop" |
226 | Apply "'v binop" |
180 apply(simp) |
253 apply(simp) |
181 apply(simp) |
254 apply(simp) |
182 apply(simp split: instr.split) |
255 apply(simp split: instr.split) |
183 done |
256 done |
184 |
257 |
185 (* 2.5.6 Case Study: Boolean Expressions *) |
258 (* 3.4 Advanced Datatypes *) |
186 |
259 |
187 datatype boolex = Const bool | Var nat | Neg boolex |
260 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" |
188 | And boolex boolex |
261 | Sum "'a aexp" "'a aexp" |
189 |
262 | Diff "'a aexp" "'a aexp" |
190 primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where |
263 | Var 'a |
191 "value2 (Const b) env = b" | |
264 | Num nat |
192 "value2 (Var x) env = env x" | |
265 and 'a bexp = Less "'a aexp" "'a aexp" |
193 "value2 (Neg b) env = (\<not> value2 b env)" | |
266 | And "'a bexp" "'a bexp" |
194 "value2 (And b c) env = (value2 b env \<and> value2 c env)" |
267 | Neg "'a bexp" |
195 |
268 |
196 value "Const true" |
269 (* Total Recursive Functions: Fun *) |
197 value "Var (Suc(0))" |
270 (* 3.5.1 Definition *) |
198 |
271 |
199 |
272 fun fib :: "nat \<Rightarrow> nat" where |
200 |
273 "fib 0 = 0" | |
201 value "value2 (Const False) (\<lambda>x. False)" |
274 "fib (Suc 0) = 1" | |
202 value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)" |
275 "fib (Suc(Suc x)) = fib x + fib (Suc x)" |
203 |
276 |
204 definition |
277 value "fib (Suc(Suc(Suc(Suc(Suc 0)))))" |
205 "en1 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)" |
278 |
206 |
279 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
207 abbreviation |
280 "sep a [] = []" | |
208 "en2 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)" |
281 "sep a [x] = [x]" | |
209 |
282 "sep a (x#y#zs) = x # a # sep a (y#zs)" |
210 value "value2 (And (Var 10) (Var 11)) en2" |
283 |
211 |
284 fun last :: "'a list \<Rightarrow> 'a" where |
212 lemma "value2 (And (Var 10) (Var 11)) en2 = True" |
285 "last [x] = x" | |
213 apply(simp) |
286 "last (_#y#zs) = last (y#zs)" |
214 done |
287 |
215 |
288 fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
289 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" | |
|
290 "sep1 _ xs = xs" |
|
291 |
|
292 fun swap12:: "'a list \<Rightarrow> 'a list" where |
|
293 "swap12 (x#y#zs) = y#x#zs" | |
|
294 "swap12 zs = zs" |
|
295 |