|
1 header "Arithmetic and Boolean Expressions" |
|
2 |
|
3 theory AExp imports Main begin |
|
4 |
|
5 subsection "Arithmetic Expressions" |
|
6 |
|
7 type_synonym name = string |
|
8 type_synonym val = int |
|
9 type_synonym state = "name \<Rightarrow> val" |
|
10 |
|
11 datatype aexp = N int | V name | Plus aexp aexp |
|
12 |
|
13 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where |
|
14 "aval (N n) _ = n" | |
|
15 "aval (V x) s = s x" | |
|
16 "aval (Plus a1 a2) s = aval a1 s + aval a2 s" |
|
17 |
|
18 |
|
19 value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)" |
|
20 |
|
21 fun lookup :: "(string * val)list \<Rightarrow> string \<Rightarrow> val" where |
|
22 "lookup ((x,i)#xis) y = (if x=y then i else lookup xis y)" |
|
23 |
|
24 value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])" |
|
25 |
|
26 value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])" |
|
27 |
|
28 |
|
29 subsection "Optimization" |
|
30 |
|
31 text{* Evaluate constant subsexpressions: *} |
|
32 |
|
33 fun asimp_const :: "aexp \<Rightarrow> aexp" where |
|
34 "asimp_const (N n) = N n" | |
|
35 "asimp_const (V x) = V x" | |
|
36 "asimp_const (Plus a1 a2) = |
|
37 (case (asimp_const a1, asimp_const a2) of |
|
38 (N n1, N n2) \<Rightarrow> N(n1+n2) | |
|
39 (a1',a2') \<Rightarrow> Plus a1' a2')" |
|
40 |
|
41 theorem aval_asimp_const[simp]: |
|
42 "aval (asimp_const a) s = aval a s" |
|
43 apply(induct a) |
|
44 apply (auto split: aexp.split) |
|
45 done |
|
46 |
|
47 text{* Now we also eliminate all occurrences 0 in additions. The standard |
|
48 method: optimized versions of the constructors: *} |
|
49 |
|
50 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where |
|
51 "plus (N i1) (N i2) = N(i1+i2)" | |
|
52 "plus (N i) a = (if i=0 then a else Plus (N i) a)" | |
|
53 "plus a (N i) = (if i=0 then a else Plus a (N i))" | |
|
54 "plus a1 a2 = Plus a1 a2" |
|
55 |
|
56 text "" |
|
57 code_thms plus |
|
58 code_thms plus |
|
59 |
|
60 (* FIXME: dropping subsumed code eqns?? *) |
|
61 lemma aval_plus[simp]: |
|
62 "aval (plus a1 a2) s = aval a1 s + aval a2 s" |
|
63 apply(induct a1 a2 rule: plus.induct) |
|
64 apply simp_all (* just for a change from auto *) |
|
65 done |
|
66 code_thms plus |
|
67 |
|
68 fun asimp :: "aexp \<Rightarrow> aexp" where |
|
69 "asimp (N n) = N n" | |
|
70 "asimp (V x) = V x" | |
|
71 "asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)" |
|
72 |
|
73 text{* Note that in @{const asimp_const} the optimized constructor was |
|
74 inlined. Making it a separate function @{const plus} improves modularity of |
|
75 the code and the proofs. *} |
|
76 |
|
77 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" |
|
78 |
|
79 theorem aval_asimp[simp]: |
|
80 "aval (asimp a) s = aval a s" |
|
81 apply(induct a) |
|
82 apply simp_all |
|
83 done |
|
84 |
|
85 end |