43141
|
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 |
|
44923
|
19 |
value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
|
43141
|
20 |
|
43158
|
21 |
text {* The same state more concisely: *}
|
44923
|
22 |
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
|
43158
|
23 |
|
|
24 |
text {* A little syntax magic to write larger states compactly: *}
|
|
25 |
|
44923
|
26 |
definition null_state ("<>") where
|
|
27 |
"null_state \<equiv> \<lambda>x. 0"
|
44036
|
28 |
syntax
|
|
29 |
"_State" :: "updbinds => 'a" ("<_>")
|
43158
|
30 |
translations
|
44923
|
31 |
"_State ms" => "_Update <> ms"
|
43141
|
32 |
|
43158
|
33 |
text {*
|
|
34 |
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
|
|
35 |
*}
|
44923
|
36 |
lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"
|
43158
|
37 |
by (rule refl)
|
|
38 |
|
44036
|
39 |
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
|
43158
|
40 |
|
44923
|
41 |
|
43158
|
42 |
text {* Variables that are not mentioned in the state are 0 by default in
|
44036
|
43 |
the @{term "<a := b::int>"} syntax:
|
44923
|
44 |
*}
|
44036
|
45 |
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
|
43141
|
46 |
|
44923
|
47 |
text{* Note that this @{text"<\<dots>>"} syntax works for any function space
|
|
48 |
@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
|
|
49 |
|
43141
|
50 |
|
|
51 |
subsection "Optimization"
|
|
52 |
|
|
53 |
text{* Evaluate constant subsexpressions: *}
|
|
54 |
|
|
55 |
fun asimp_const :: "aexp \<Rightarrow> aexp" where
|
|
56 |
"asimp_const (N n) = N n" |
|
|
57 |
"asimp_const (V x) = V x" |
|
|
58 |
"asimp_const (Plus a1 a2) =
|
|
59 |
(case (asimp_const a1, asimp_const a2) of
|
|
60 |
(N n1, N n2) \<Rightarrow> N(n1+n2) |
|
|
61 |
(a1',a2') \<Rightarrow> Plus a1' a2')"
|
|
62 |
|
|
63 |
theorem aval_asimp_const[simp]:
|
|
64 |
"aval (asimp_const a) s = aval a s"
|
45015
|
65 |
apply(induction a)
|
43141
|
66 |
apply (auto split: aexp.split)
|
|
67 |
done
|
|
68 |
|
|
69 |
text{* Now we also eliminate all occurrences 0 in additions. The standard
|
|
70 |
method: optimized versions of the constructors: *}
|
|
71 |
|
|
72 |
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
|
|
73 |
"plus (N i1) (N i2) = N(i1+i2)" |
|
|
74 |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
|
|
75 |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
|
|
76 |
"plus a1 a2 = Plus a1 a2"
|
|
77 |
|
|
78 |
lemma aval_plus[simp]:
|
|
79 |
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
|
45015
|
80 |
apply(induction a1 a2 rule: plus.induct)
|
43141
|
81 |
apply simp_all (* just for a change from auto *)
|
|
82 |
done
|
|
83 |
|
|
84 |
fun asimp :: "aexp \<Rightarrow> aexp" where
|
|
85 |
"asimp (N n) = N n" |
|
|
86 |
"asimp (V x) = V x" |
|
|
87 |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
|
|
88 |
|
|
89 |
text{* Note that in @{const asimp_const} the optimized constructor was
|
|
90 |
inlined. Making it a separate function @{const plus} improves modularity of
|
|
91 |
the code and the proofs. *}
|
|
92 |
|
|
93 |
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
|
|
94 |
|
|
95 |
theorem aval_asimp[simp]:
|
|
96 |
"aval (asimp a) s = aval a s"
|
45015
|
97 |
apply(induction a)
|
43141
|
98 |
apply simp_all
|
|
99 |
done
|
|
100 |
|
|
101 |
end
|