theory Ex_3_4
imports Main
begin
text \Take a copy of theory AExp and modify it as follows. Extend
type aexp with a binary constructor Times that represents multiplication.
Modify the definition of the functions aval and asimp accordingly. You can
remove asimp_const. Function asimp should eliminate 0 and 1 from multiplications
as well as evaluate constant subterms. Update all proofs concerned.\
section "Arithmetic and Boolean Expressions"
subsection "Arithmetic Expressions"
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \ val"
text_raw\\snip{AExpaexpdef}{2}{1}{%\
datatype aexp = N int | V vname | Plus aexp aexp | Times aexp aexp
text_raw\}%endsnip\
text_raw\\snip{AExpavaldef}{1}{2}{%\
fun aval :: "aexp \ state \ val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
"aval (Times a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s) * (aval a\<^sub>2 s)"
text_raw\}%endsnip\
value "aval (Plus (V ''x'') (N 5)) (\x. if x = ''x'' then 7 else 0)"
text \The same state more concisely:\
value "aval (Plus (V ''x'') (N 5)) ((\x. 0) (''x'':= 7))"
text \A little syntax magic to write larger states compactly:\
definition null_state ("<>") where
"null_state \ \x. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
text \\noindent
We can now write a series of updates to the function \\x. 0\ compactly:
\
lemma " = (<> (a := 1)) (b := (2::int))"
by (rule refl)
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
text \In the @{term[source] ""} syntax, variables that are not mentioned are 0 by default:
\
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
text\Note that this \<\>\ syntax works for any function space
\\\<^sub>1 \ \\<^sub>2\ where \\\<^sub>2\ has a \0\.\
text\Now we also eliminate all occurrences 0 in additions. The standard
method: optimized versions of the constructors:\
text_raw\\snip{AExpplusdef}{0}{2}{%\
fun plus :: "aexp \ aexp \ aexp" where
"plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
text_raw\}%endsnip\
lemma aval_plus[simp]:
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
apply(induction a1 a2 rule: plus.induct)
apply simp_all (* just for a change from auto *)
done
fun times :: "aexp \ aexp \ aexp" where
"times (N i) (N j) = N(i*j)"
| "times (N 0) a = (N 0)"
| "times (N 1) a = a"
| "times (N i) a = Times (N i) a"
| "times a (N 0) = (N 0)"
| "times a (N 1) = a"
| "times a (N i) = Times (N i) a"
| "times a1 a2 = Times a1 a2"
text_raw\\snip{AExpasimpdef}{2}{0}{%\
fun asimp :: "aexp \ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)" |
"asimp (Times a\<^sub>1 a\<^sub>2) = times (asimp a\<^sub>1) (asimp a\<^sub>2)"
text_raw\}%endsnip\
text\Note that in \<^const>\asimp_const\ the optimized constructor was
inlined. Making it a separate function \<^const>\plus\ improves modularity of
the code and the proofs.\
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
theorem aval_asimp[simp]:
"aval (asimp a) s = aval a s"
apply(induction a)
apply simp_all
done
end
end