1section "Arithmetic and Boolean Expressions"
2
3theory AExp imports Main begin
4
5subsection "Arithmetic Expressions"
6
7type_synonym vname = string
8type_synonym val = int
9type_synonym state = "vname \<Rightarrow> val"
10
11text_raw\<open>\snip{AExpaexpdef}{2}{1}{%\<close>
12datatype aexp = N int | V vname | Plus aexp aexp
13text_raw\<open>}%endsnip\<close>
14
15text_raw\<open>\snip{AExpavaldef}{1}{2}{%\<close>
16fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
17"aval (N n) s = n" |
18"aval (V x) s = s x" |
19"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
20text_raw\<open>}%endsnip\<close>
21
22
23value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
24
25text \<open>The same state more concisely:\<close>
26value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
27
28text \<open>A little syntax magic to write larger states compactly:\<close>
29
30definition null_state ("<>") where
31  "null_state \<equiv> \<lambda>x. 0"
32syntax 
33  "_State" :: "updbinds => 'a" ("<_>")
34translations
35  "_State ms" == "_Update <> ms"
36  "_State (_updbinds b bs)" <= "_Update (_State b) bs"
37
38text \<open>\noindent
39  We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
40\<close>
41lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))"
42  by (rule refl)
43
44value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
45
46
47text \<open>In  the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
48\<close>
49value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
50
51text\<open>Note that this @{text"<\<dots>>"} syntax works for any function space
52@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}.\<close>
53
54
55subsection "Constant Folding"
56
57text\<open>Evaluate constant subsexpressions:\<close>
58
59text_raw\<open>\snip{AExpasimpconstdef}{0}{2}{%\<close>
60fun asimp_const :: "aexp \<Rightarrow> aexp" where
61"asimp_const (N n) = N n" |
62"asimp_const (V x) = V x" |
63"asimp_const (Plus a\<^sub>1 a\<^sub>2) =
64  (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
65    (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N(n\<^sub>1+n\<^sub>2) |
66    (b\<^sub>1,b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)"
67text_raw\<open>}%endsnip\<close>
68
69theorem aval_asimp_const:
70  "aval (asimp_const a) s = aval a s"
71apply(induction a)
72apply (auto split: aexp.split)
73done
74
75text\<open>Now we also eliminate all occurrences 0 in additions. The standard
76method: optimized versions of the constructors:\<close>
77
78text_raw\<open>\snip{AExpplusdef}{0}{2}{%\<close>
79fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
80"plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>2)" |
81"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
82"plus a (N i) = (if i=0 then a else Plus a (N i))" |
83"plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
84text_raw\<open>}%endsnip\<close>
85
86lemma aval_plus[simp]:
87  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
88apply(induction a1 a2 rule: plus.induct)
89apply simp_all (* just for a change from auto *)
90done
91
92text_raw\<open>\snip{AExpasimpdef}{2}{0}{%\<close>
93fun asimp :: "aexp \<Rightarrow> aexp" where
94"asimp (N n) = N n" |
95"asimp (V x) = V x" |
96"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
97text_raw\<open>}%endsnip\<close>
98
99text\<open>Note that in @{const asimp_const} the optimized constructor was
100inlined. Making it a separate function @{const plus} improves modularity of
101the code and the proofs.\<close>
102
103value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
104
105theorem aval_asimp[simp]:
106  "aval (asimp a) s = aval a s"
107apply(induction a)
108apply simp_all
109done
110
111end
112