|
1 theory BExp imports AExp begin |
|
2 |
|
3 subsection "Boolean Expressions" |
|
4 |
|
5 datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp |
|
6 |
|
7 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
|
8 "bval (B bv) _ = bv" | |
|
9 "bval (Not b) s = (\<not> bval b s)" | |
|
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
|
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
|
12 |
|
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
|
14 (lookup [(''x'',3),(''y'',1)])" |
|
15 |
|
16 |
|
17 subsection "Optimization" |
|
18 |
|
19 text{* Optimized constructors: *} |
|
20 |
|
21 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where |
|
22 "less (N n1) (N n2) = B(n1 < n2)" | |
|
23 "less a1 a2 = Less a1 a2" |
|
24 |
|
25 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)" |
|
26 apply(induct a1 a2 rule: less.induct) |
|
27 apply simp_all |
|
28 done |
|
29 |
|
30 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where |
|
31 "and (B True) b = b" | |
|
32 "and b (B True) = b" | |
|
33 "and (B False) b = B False" | |
|
34 "and b (B False) = B False" | |
|
35 "and b1 b2 = And b1 b2" |
|
36 |
|
37 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)" |
|
38 apply(induct b1 b2 rule: and.induct) |
|
39 apply simp_all |
|
40 done |
|
41 |
|
42 fun not :: "bexp \<Rightarrow> bexp" where |
|
43 "not (B True) = B False" | |
|
44 "not (B False) = B True" | |
|
45 "not b = Not b" |
|
46 |
|
47 lemma bval_not[simp]: "bval (not b) s = (~bval b s)" |
|
48 apply(induct b rule: not.induct) |
|
49 apply simp_all |
|
50 done |
|
51 |
|
52 text{* Now the overall optimizer: *} |
|
53 |
|
54 fun bsimp :: "bexp \<Rightarrow> bexp" where |
|
55 "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" | |
|
56 "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" | |
|
57 "bsimp (Not b) = not(bsimp b)" | |
|
58 "bsimp (B bv) = B bv" |
|
59 |
|
60 value "bsimp (And (Less (N 0) (N 1)) b)" |
|
61 |
|
62 value "bsimp (And (Less (N 1) (N 0)) (B True))" |
|
63 |
|
64 theorem "bval (bsimp b) s = bval b s" |
|
65 apply(induct b) |
|
66 apply simp_all |
|
67 done |
|
68 |
|
69 end |