Theory HOL-IMP.AExp

section "Arithmetic and Boolean Expressions"

subsection "Arithmetic Expressions"

theory AExp imports Main begin

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
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⇩1 a⇩2) s = aval a⇩1 s + aval a⇩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> = (<> (a := 1)) (b := (2::int))"
  by (rule refl)

value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"


text ‹In  the @{term[source] "<a := b>"} 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
‹τ⇩1 ⇒ τ⇩2› where ‹τ⇩2› has a ‹0›.›


subsection "Constant Folding"

text‹Evaluate constant subsexpressions:›

text_raw‹\snip{AExpasimpconstdef}{0}{2}{%›
fun asimp_const :: "aexp ⇒ aexp" where
"asimp_const (N n) = N n" |
"asimp_const (V x) = V x" |
"asimp_const (Plus a⇩1 a⇩2) =
  (case (asimp_const a⇩1, asimp_const a⇩2) of
    (N n⇩1, N n⇩2) ⇒ N(n⇩1+n⇩2) |
    (b⇩1,b⇩2) ⇒ Plus b⇩1 b⇩2)"
text_raw‹}%endsnip›

theorem aval_asimp_const:
  "aval (asimp_const a) s = aval a s"
apply(induction a)
apply (auto split: aexp.split)
done

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⇩1) (N i⇩2) = N(i⇩1+i⇩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⇩1 a⇩2 = Plus a⇩1 a⇩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

text_raw‹\snip{AExpasimpdef}{2}{0}{%›
fun asimp :: "aexp ⇒ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a⇩1 a⇩2) = plus (asimp a⇩1) (asimp a⇩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