1 theory BExp imports AExp begin |
1 theory BExp imports AExp begin |
2 |
2 |
3 subsection "Boolean Expressions" |
3 subsection "Boolean Expressions" |
4 |
4 |
|
5 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbexpdef}{% *} |
5 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
6 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
|
7 text_raw{*}\end{isaverbatimwrite}*} |
6 |
8 |
|
9 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbvaldef}{% *} |
7 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
10 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
8 "bval (Bc v) s = v" | |
11 "bval (Bc v) s = v" | |
9 "bval (Not b) s = (\<not> bval b s)" | |
12 "bval (Not b) s = (\<not> bval b s)" | |
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
13 "bval (And b\<^isub>1 b\<^isub>2) s = (bval b\<^isub>1 s \<and> bval b\<^isub>2 s)" | |
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
14 "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)" |
|
15 text_raw{*}\end{isaverbatimwrite}*} |
12 |
16 |
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
17 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
14 <''x'' := 3, ''y'' := 1>" |
18 <''x'' := 3, ''y'' := 1>" |
15 |
19 |
16 |
20 |
17 subsection "Optimization" |
21 text{* To improve automation: *} |
18 |
22 |
19 text{* Optimized constructors: *} |
23 lemma bval_And_if[simp]: |
|
24 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
|
25 by(simp) |
20 |
26 |
|
27 declare bval.simps(3)[simp del] --"remove the original eqn" |
|
28 |
|
29 |
|
30 subsection "Constant Folding" |
|
31 |
|
32 text{* Optimizing constructors: *} |
|
33 |
|
34 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExplessdef}{% *} |
21 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where |
35 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where |
22 "less (N n1) (N n2) = Bc(n1 < n2)" | |
36 "less (N n\<^isub>1) (N n\<^isub>2) = Bc(n\<^isub>1 < n\<^isub>2)" | |
23 "less a1 a2 = Less a1 a2" |
37 "less a\<^isub>1 a\<^isub>2 = Less a\<^isub>1 a\<^isub>2" |
|
38 text_raw{*}\end{isaverbatimwrite}*} |
24 |
39 |
25 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)" |
40 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)" |
26 apply(induction a1 a2 rule: less.induct) |
41 apply(induction a1 a2 rule: less.induct) |
27 apply simp_all |
42 apply simp_all |
28 done |
43 done |
29 |
44 |
|
45 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpanddef}{% *} |
30 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where |
46 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where |
31 "and (Bc True) b = b" | |
47 "and (Bc True) b = b" | |
32 "and b (Bc True) = b" | |
48 "and b (Bc True) = b" | |
33 "and (Bc False) b = Bc False" | |
49 "and (Bc False) b = Bc False" | |
34 "and b (Bc False) = Bc False" | |
50 "and b (Bc False) = Bc False" | |
35 "and b1 b2 = And b1 b2" |
51 "and b\<^isub>1 b\<^isub>2 = And b\<^isub>1 b\<^isub>2" |
|
52 text_raw{*}\end{isaverbatimwrite}*} |
36 |
53 |
37 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)" |
54 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)" |
38 apply(induction b1 b2 rule: and.induct) |
55 apply(induction b1 b2 rule: and.induct) |
39 apply simp_all |
56 apply simp_all |
40 done |
57 done |
41 |
58 |
|
59 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpnotdef}{% *} |
42 fun not :: "bexp \<Rightarrow> bexp" where |
60 fun not :: "bexp \<Rightarrow> bexp" where |
43 "not (Bc True) = Bc False" | |
61 "not (Bc True) = Bc False" | |
44 "not (Bc False) = Bc True" | |
62 "not (Bc False) = Bc True" | |
45 "not b = Not b" |
63 "not b = Not b" |
|
64 text_raw{*}\end{isaverbatimwrite}*} |
46 |
65 |
47 lemma bval_not[simp]: "bval (not b) s = (~bval b s)" |
66 lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)" |
48 apply(induction b rule: not.induct) |
67 apply(induction b rule: not.induct) |
49 apply simp_all |
68 apply simp_all |
50 done |
69 done |
51 |
70 |
52 text{* Now the overall optimizer: *} |
71 text{* Now the overall optimizer: *} |
53 |
72 |
|
73 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *} |
54 fun bsimp :: "bexp \<Rightarrow> bexp" where |
74 fun bsimp :: "bexp \<Rightarrow> bexp" where |
55 "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" | |
75 "bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)" | |
56 "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" | |
76 "bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" | |
57 "bsimp (Not b) = not(bsimp b)" | |
77 "bsimp (Not b) = not(bsimp b)" | |
58 "bsimp (Bc v) = Bc v" |
78 "bsimp (Bc v) = Bc v" |
|
79 text_raw{*}\end{isaverbatimwrite}*} |
59 |
80 |
60 value "bsimp (And (Less (N 0) (N 1)) b)" |
81 value "bsimp (And (Less (N 0) (N 1)) b)" |
61 |
82 |
62 value "bsimp (And (Less (N 1) (N 0)) (B True))" |
83 value "bsimp (And (Less (N 1) (N 0)) (B True))" |
63 |
84 |