author | bulwahn |
Thu, 07 Jul 2011 23:33:14 +0200 | |
changeset 43704 | 47b0be18ccbe |
parent 43250 | c729110a9f08 |
child 44036 | d03f9f28d01d |
permissions | -rw-r--r-- |
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 |
||
19 |
value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)" |
|
20 |
||
43158 | 21 |
text {* The same state more concisely: *} |
22 |
value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))" |
|
23 |
||
24 |
text {* A little syntax magic to write larger states compactly: *} |
|
25 |
||
26 |
nonterminal funlets and funlet |
|
27 |
||
28 |
syntax |
|
29 |
"_funlet" :: "['a, 'a] => funlet" ("_ /->/ _") |
|
30 |
"" :: "funlet => funlets" ("_") |
|
31 |
"_Funlets" :: "[funlet, funlets] => funlets" ("_,/ _") |
|
32 |
"_Fun" :: "funlets => 'a => 'b" ("(1[_])") |
|
33 |
"_FunUpd" :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900) |
|
34 |
||
35 |
syntax (xsymbols) |
|
36 |
"_funlet" :: "['a, 'a] => funlet" ("_ /\<rightarrow>/ _") |
|
43141 | 37 |
|
43250
c729110a9f08
use null_heap instead of %_. 0 to avoid printing problems
kleing
parents:
43158
diff
changeset
|
38 |
definition |
c729110a9f08
use null_heap instead of %_. 0 to avoid printing problems
kleing
parents:
43158
diff
changeset
|
39 |
"null_heap \<equiv> \<lambda>x. 0" |
c729110a9f08
use null_heap instead of %_. 0 to avoid printing problems
kleing
parents:
43158
diff
changeset
|
40 |
|
43158 | 41 |
translations |
42 |
"_FunUpd m (_Funlets xy ms)" == "_FunUpd (_FunUpd m xy) ms" |
|
43 |
"_FunUpd m (_funlet x y)" == "m(x := y)" |
|
43250
c729110a9f08
use null_heap instead of %_. 0 to avoid printing problems
kleing
parents:
43158
diff
changeset
|
44 |
"_Fun ms" == "_FunUpd (CONST null_heap) ms" |
43158 | 45 |
"_Fun (_Funlets ms1 ms2)" <= "_FunUpd (_Fun ms1) ms2" |
46 |
"_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3" |
|
43141 | 47 |
|
43158 | 48 |
text {* |
49 |
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: |
|
50 |
*} |
|
43250
c729110a9f08
use null_heap instead of %_. 0 to avoid printing problems
kleing
parents:
43158
diff
changeset
|
51 |
lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = (null_heap (a := Suc 0)) (b := 2)" |
43158 | 52 |
by (rule refl) |
53 |
||
54 |
value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]" |
|
55 |
||
56 |
text {* Variables that are not mentioned in the state are 0 by default in |
|
57 |
the @{term "[a \<rightarrow> b::int]"} syntax: |
|
58 |
*} |
|
59 |
value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]" |
|
43141 | 60 |
|
61 |
||
62 |
subsection "Optimization" |
|
63 |
||
64 |
text{* Evaluate constant subsexpressions: *} |
|
65 |
||
66 |
fun asimp_const :: "aexp \<Rightarrow> aexp" where |
|
67 |
"asimp_const (N n) = N n" | |
|
68 |
"asimp_const (V x) = V x" | |
|
69 |
"asimp_const (Plus a1 a2) = |
|
70 |
(case (asimp_const a1, asimp_const a2) of |
|
71 |
(N n1, N n2) \<Rightarrow> N(n1+n2) | |
|
72 |
(a1',a2') \<Rightarrow> Plus a1' a2')" |
|
73 |
||
74 |
theorem aval_asimp_const[simp]: |
|
75 |
"aval (asimp_const a) s = aval a s" |
|
76 |
apply(induct a) |
|
77 |
apply (auto split: aexp.split) |
|
78 |
done |
|
79 |
||
80 |
text{* Now we also eliminate all occurrences 0 in additions. The standard |
|
81 |
method: optimized versions of the constructors: *} |
|
82 |
||
83 |
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where |
|
84 |
"plus (N i1) (N i2) = N(i1+i2)" | |
|
85 |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" | |
|
86 |
"plus a (N i) = (if i=0 then a else Plus a (N i))" | |
|
87 |
"plus a1 a2 = Plus a1 a2" |
|
88 |
||
89 |
code_thms plus |
|
90 |
code_thms plus |
|
91 |
||
92 |
(* FIXME: dropping subsumed code eqns?? *) |
|
93 |
lemma aval_plus[simp]: |
|
94 |
"aval (plus a1 a2) s = aval a1 s + aval a2 s" |
|
95 |
apply(induct a1 a2 rule: plus.induct) |
|
96 |
apply simp_all (* just for a change from auto *) |
|
97 |
done |
|
98 |
code_thms plus |
|
99 |
||
100 |
fun asimp :: "aexp \<Rightarrow> aexp" where |
|
101 |
"asimp (N n) = N n" | |
|
102 |
"asimp (V x) = V x" | |
|
103 |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)" |
|
104 |
||
105 |
text{* Note that in @{const asimp_const} the optimized constructor was |
|
106 |
inlined. Making it a separate function @{const plus} improves modularity of |
|
107 |
the code and the proofs. *} |
|
108 |
||
109 |
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" |
|
110 |
||
111 |
theorem aval_asimp[simp]: |
|
112 |
"aval (asimp a) s = aval a s" |
|
113 |
apply(induct a) |
|
114 |
apply simp_all |
|
115 |
done |
|
116 |
||
117 |
end |