theory chap3
imports Main
begin

type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp
type_synonym assignment = "vname => int"

fun aval :: "aexp => assignment => int" where
"aval (N n) _ = n" |
"aval (V v) m = m v" |
"aval (Plus a1 a2) m = aval a1 m + aval a2 m"

fun asimp_const :: "aexp => aexp" where
"asimp_const (N n) = N n" |
"asimp_const (V v) = V v" |
"asimp_const (Plus a1 a2) =
  (case (asimp_const a1, asimp_const a2) of
     (N n1, N n2) => N (n1 + n2) |
     (a1', a2') => Plus a1' a2'
    )"

―‹optimized plus that does constant folding and 0 elim›
fun plus :: "aexp => aexp => aexp" where
"plus (N i) (N j) = N (i + j)" |
"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 a1 a2 = Plus a1 a2"

theorem plus_preserve_value_under_aval : "aval (plus a1 a2) as = aval a1 as + aval a2 as"
apply(induction rule:plus.induct)
apply(auto)
done

fun asimp :: "aexp => aexp" where
"asimp (N n) = N n" |
"asimp (V v) = V v" |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"

theorem asimp_preserve_value_under_aval : "aval (asimp a) as = aval a as"
apply(induction rule:asimp.induct)
apply(auto simp add:plus_preserve_value_under_aval)
done

―‹exercise 3.1›
fun optimal :: "aexp => bool" where
"optimal (N n) = True" |
"optimal (V v) = True" |
"optimal (Plus a1 a2) =
  (case (a1, a2) of
     (N _, N _) => False |
     _ => optimal a1 ∧ optimal a2)"

theorem asimp_const_optimality : "optimal (asimp_const a)"
apply(induction a)
apply(auto split: aexp.split)
done

―‹exercise 3.2›
fun full_asimp :: "aexp => aexp" where
"full_asimp (N n) = N n" |
"full_asimp (V v) = V v" |
"full_asimp (Plus a1 a2) = _"

end

fun optimal :: "aexp => bool" where
"optimal (N n) = True" |
"optimal (V v) = True" |
"optimal (Plus (N _) (N _)) = False" |
"optimal (Plus a1 a2) = (optimal a1 ∧ optimal a2)"

theorem asimp_const_optimality : "optimal (asimp_const a)"
  apply(induction a)
  supply[[simp_trace_new]]
apply(auto split: aexp.split)