poly.thy

theory poly
  imports Main HOL Nat
begin
(*
 * Power function
 *)

primrec pow :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"pow x 0 = Suc 0"
| "pow x (Suc y) = x * pow x y"

lemma addiction_rule[simp]: "pow x (y + z) = pow x y * pow x z"
  apply(induct z)
   apply auto
  done

lemma power_of_power: "pow (pow x y) z = pow x (y * z)"
  apply(induct z)
   apply auto
  done

(*
 * Definition of polynomial
 * either is
 * a constant of natural number
 * a variable of natural number
 * the product of two polynomial
 * the sum of two polynomial
 *)

datatype poly = Nat nat | Var nat | Times poly poly | Sums poly poly | Exp poly poly
fun poly_exe :: "poly \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where
"poly_exe (Nat x) _ = x"
| "poly_exe (Var x) f = f x"
| "poly_exe (Times x y) f = (poly_exe x f) * (poly_exe y f)"
| "poly_exe (Sums x y) f = (poly_exe x f) + (poly_exe y f)"
| "poly_exe (Exp x y) f = pow (poly_exe x f) (poly_exe y f)"

lemma distrubutive_nat: "(x::nat) * (y + z) = x * y + x * z"
  apply(induct x)
   apply auto
  done

lemma distributive_poly: "poly_exe (Times x (Sums y z)) f = poly_exe (Sums (Times x y) (Times x z)) f"
  apply(simp add: distrubutive_nat)
  done

lemma time_comutativity_poly: "poly_exe (Times x y) f = poly_exe (Times y x) f"
  apply auto
  done

lemma sum_commutativity_poly: "poly_exe (Sums x y) f = poly_exe (Sums y x) f"
  apply auto
  done

lemma sum_associativity_poly: "poly_exe (Sums x (Sums y z)) f = poly_exe (Sums (Sums x y) z) f"
  apply auto
  done

lemma time_associativity_poly: "poly_exe (Times x (Times y z)) f = poly_exe (Times (Times x y) z) f"
  apply auto
  done