author | nipkow |
Sat, 22 Oct 2011 20:17:50 +0200 | |
changeset 45246 | 4fbeabee6487 |
parent 45238 | ed2bb3b58cc4 |
child 45255 | ffc06165d272 |
permissions | -rw-r--r-- |
43141 | 1 |
header "Arithmetic and Boolean Expressions" |
2 |
||
3 |
theory AExp imports Main begin |
|
4 |
||
5 |
subsection "Arithmetic Expressions" |
|
6 |
||
45212 | 7 |
type_synonym vname = string |
43141 | 8 |
type_synonym val = int |
45212 | 9 |
type_synonym state = "vname \<Rightarrow> val" |
43141 | 10 |
|
45212 | 11 |
datatype aexp = N int | V vname | Plus aexp aexp |
43141 | 12 |
|
13 |
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where |
|
45216 | 14 |
"aval (N n) s = n" | |
43141 | 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 |
||
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
55 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *} |
43141 | 56 |
fun asimp_const :: "aexp \<Rightarrow> aexp" where |
57 |
"asimp_const (N n) = N n" | |
|
58 |
"asimp_const (V x) = V x" | |
|
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
59 |
"asimp_const (Plus a\<^isub>1 a\<^isub>2) = |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
60 |
(case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
61 |
(N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2) | |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
62 |
(b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)" |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
63 |
text_raw{*}\end{isaverbatimwrite}*} |
43141 | 64 |
|
45238 | 65 |
theorem aval_asimp_const: |
43141 | 66 |
"aval (asimp_const a) s = aval a s" |
45015 | 67 |
apply(induction a) |
43141 | 68 |
apply (auto split: aexp.split) |
69 |
done |
|
70 |
||
71 |
text{* Now we also eliminate all occurrences 0 in additions. The standard |
|
72 |
method: optimized versions of the constructors: *} |
|
73 |
||
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
74 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *} |
43141 | 75 |
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where |
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
76 |
"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" | |
43141 | 77 |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" | |
78 |
"plus a (N i) = (if i=0 then a else Plus a (N i))" | |
|
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
79 |
"plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2" |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
80 |
text_raw{*}\end{isaverbatimwrite}*} |
43141 | 81 |
|
82 |
lemma aval_plus[simp]: |
|
83 |
"aval (plus a1 a2) s = aval a1 s + aval a2 s" |
|
45015 | 84 |
apply(induction a1 a2 rule: plus.induct) |
43141 | 85 |
apply simp_all (* just for a change from auto *) |
86 |
done |
|
87 |
||
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
88 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *} |
43141 | 89 |
fun asimp :: "aexp \<Rightarrow> aexp" where |
90 |
"asimp (N n) = N n" | |
|
91 |
"asimp (V x) = V x" | |
|
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
92 |
"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)" |
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset
|
93 |
text_raw{*}\end{isaverbatimwrite}*} |
43141 | 94 |
|
95 |
text{* Note that in @{const asimp_const} the optimized constructor was |
|
96 |
inlined. Making it a separate function @{const plus} improves modularity of |
|
97 |
the code and the proofs. *} |
|
98 |
||
99 |
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" |
|
100 |
||
101 |
theorem aval_asimp[simp]: |
|
102 |
"aval (asimp a) s = aval a s" |
|
45015 | 103 |
apply(induction a) |
43141 | 104 |
apply simp_all |
105 |
done |
|
106 |
||
107 |
end |