theory Ex31
imports Main
begin
type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp

fun optimal :: "aexp ⇒ bool" where
"optimal (N n) = true" |
"optimal (V x) = true" |
"optimal (Plus a1 a2) =
  (case (a1,a2) of
    (N n1, N n2) ⇒ false |
    (b1,b2) ⇒ optimal b1 ∧ optimal b2)"


fun asimp_const :: "aexp ⇒ aexp" where
"asimp_const (N n) = N n" |
"asimp_const (V x) = V x" |
"asimp_const (Plus a1 a2) =
  (case (asimp_const a1, asimp_const a2) of
    (N n1, N n2) ⇒ N(n1+n2) |
    (b1,b2) ⇒ Plus b1 b2)"
end