2.11.thy

datatype exp = Var | Const int | Add exp exp | Mult exp exp

fun eval where
"eval Var v = v" |
"eval (Const x) v = x" |
"eval (Add a b) v = eval a v + eval b v" |
"eval (Mult a b) v = eval a v * eval b v"

fun evalp :: "int list ⇒ int ⇒ int"  where
"evalp [] v = 0" |
"evalp (c # cs) v = c + v * evalp cs v"

type_synonym polynomial = "int list"

fun padd :: "polynomial ⇒ polynomial ⇒ polynomial" where
"padd [] ys = ys" |
"padd xs [] = xs" |
"padd (x#xs) (y#ys) = (x + y) # padd xs ys"

fun pmult :: "polynomial ⇒ polynomial ⇒ polynomial" where
"pmult xs [] = []" |
"pmult xs (y#ys) = padd (map ((*) y) xs) (0 # pmult xs ys)"

lemma [simp]: "evalp (padd a b) v = (evalp a v) + (evalp b v)"
  apply (induction a b rule: padd.induct)
    apply (auto simp add: algebra_simps)
  done

lemma [simp]: "evalp (map ((*) y) cs) v = y * evalp cs v"
  apply (induction cs)
   apply (auto simp add: algebra_simps)
  done

lemma [simp]: "evalp (pmult a b) v = (evalp a v) * (evalp b v)"
  apply (induction a b rule: pmult.induct)
   apply (auto simp add: algebra_simps)
  done

fun coeffs :: "exp ⇒ polynomial" where
"coeffs Var = [0, 1]" |
"coeffs (Const x) = [x]" |
"coeffs (Add a b) = padd (coeffs a) (coeffs b)" |
"coeffs (Mult a b) = pmult (coeffs a) (coeffs b)"

lemma "evalp (coeffs e) x = eval e x"
  apply (induction e)
   apply (auto)
  done