Created
November 8, 2017 19:38
-
-
Save DengYiping/62474343197f52bd222ca4ace25aca79 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment