theory Cring_Poly imports"HOL-Algebra.UnivPoly""HOL-Algebra.Subrings" Function_Ring begin
textβΉ
This theory extends the material in π«βΉHOL-Algebra.UnivPolyβΊ. The main additions are
material on Taylor expansions of polynomials and polynomial derivatives, and various applications
of the universal property of polynomial evaluation. These include construing polynomials as
functions from the base ring to itself, composing one polynomial with another, and extending
homomorphisms between rings to homomoprhisms of their polynomial rings. These formalizations
are necessary components of the proof of Hensel's lemma for $p$-adic integers, and for the
proof of $p$-adic quantifier elimination. βΊ
lemma(in ring) ring_hom_finsum: assumes"h β ring_hom R S" assumes"ring S" assumes"finite I" assumes"F β I → carrier R" shows"h (finsum R F I) = finsum S (h β F) I" proof- have I: "(h β ring_hom R S β§ F β I → carrier R) βΆ h (finsum R F I) = finsum S (h βF) I" apply(rule finite_induct, rule assms) using assms ring_hom_zero[of h R S] apply (metis abelian_group_def abelian_monoid.finsum_empty ring_axioms ring_def) proof(rule) fix A a assume A: "finite A""a β A""h β ring_hom R S β§ F β A → carrier R βΆ h (finsum R F A) = finsum S (h β F) A""h β ring_hom R S β§ F β insert a A → carrier R" have0: "h β ring_hom R S β§ F β A → carrier R " using A by auto have1: "h (finsum R F A) = finsum S (h β F) A" using A 0by auto have2: "abelian_monoid S" using assms ring_def abelian_group_def by auto have3: "h (F a β finsum R F A) = h (F a) β (finsum S (h β F) A) " using ring_hom_add assms finsum_closed 1 A(4) by fastforce have4: "finsum R F (insert a A) = F a β finsum R F A" using finsum_insert[of A a F] A assms by auto have5: "finsum S (h β F) (insert a A) = (h β F) a β finsum S (h β F) A" apply(rule abelian_monoid.finsum_insert[of S A a "h β F"]) apply (simp add: "2") apply(rule A) apply(rule A) using ring_hom_closed A "0"apply fastforce using A ring_hom_closed by auto show"h (finsum R F (insert a A)) = finsum S (h β F) (insert a A)" unfolding453by auto qed thus ?thesis using assms by blast qed
lemma(in ring) ring_hom_a_inv: assumes"ring S" assumes"h β ring_hom R S" assumes"b β carrier R" shows"h (β b) = β h b" proof- have"h b β h (β b) = 0" by (metis (no_types, opaque_lifting) abelian_group.a_inv_closed assms(1) assms(2) assms(3)
is_abelian_group local.ring_axioms r_neg ring_hom_add ring_hom_zero) thenshow ?thesis by (metis (no_types, lifting) abelian_group.minus_equality add.inv_closed assms(1)
assms(2) assms(3) ring.is_abelian_group ring.ring_simprules(10) ring_hom_closed) qed
lemma(in ring) ring_hom_minus: assumes"ring S" assumes"h β ring_hom R S" assumes"a β carrier R" assumes"b β carrier R" shows"h (a β b) = h a β h b" using assms ring_hom_add[of h R S a "β b"] unfolding a_minus_def using ring_hom_a_inv[of S h b] by auto
lemma ring_hom_nat_pow: assumes"ring R" assumes"ring S" assumes"h β ring_hom R S" assumes"a β carrier R" shows"h (a[^](n::nat)) = (h a)[^](n::nat)" using assms by (simp add: ring_hom_ring.hom_nat_pow ring_hom_ringI2)
lemma (in ring) Units_not_right_zero_divisor: assumes"a β Units R" assumes"b β carrier R" assumes"a β b = 0" shows"b = 0" proof- have"inv a β a β b = 0 " using assms Units_closed Units_inv_closed r_null m_assoc[of "inv a" a b] by presburger thus ?thesis using assms by (metis Units_l_inv l_one) qed
lemma (in ring) Units_not_left_zero_divisor: assumes"a β Units R" assumes"b β carrier R" assumes"b β a = 0" shows"b = 0" proof- have"b β (a β inv a) = 0 " using assms Units_closed Units_inv_closed l_null m_assoc[of b a"inv a"] by presburger thus ?thesis using assms by (metis Units_r_inv r_one) qed
lemma (in cring) finsum_remove: assumes"β§i. i β Y ==> f i β carrier R" assumes"finite Y" assumes"i β Y" shows"finsum R f Y = f i β finsum R f (Y - {i})" proof- have"finsum R f (insert i (Y - {i})) = f i β finsum R f (Y - {i})" apply(rule finsum_insert) using assms apply blast apply blast using assms apply blast using assms by blast thus ?thesis using assms by (metis insert_Diff) qed
type_synonym degree = nat textβΉThe composition of two ring homomorphisms is a ring homomorphismβΊ lemma ring_hom_compose: assumes"ring R" assumes"ring S" assumes"ring T" assumes"h β ring_hom R S" assumes"g β ring_hom S T" assumes"β§c. c β carrier R ==> f c = g (h c)" shows"f β ring_hom R T" proof(rule ring_hom_memI) show"β§x. x β carrier R ==> f x β carrier T" using assms by (metis ring_hom_closed) show" β§x y. x β carrier R ==> y β carrier R ==> f (x β y) = f x β f y" proof- fix x y assume A: "x β carrier R""y β carrier R" show"f (x β y) = f x β f y" proof- have"f (x β y) = g (h (x β y))" by (simp add: A(1) A(2) assms(1) assms(6) ring.ring_simprules(5)) thenhave"f (x β y) = g ((h x) β (h y))" using A(1) A(2) assms(4) ring_hom_mult by fastforce thenhave"f (x β y) = g (h x) β g (h y)" using A(1) A(2) assms(4) assms(5) ring_hom_closed ring_hom_mult by fastforce thenshow ?thesis by (simp add: A(1) A(2) assms(6)) qed qed show"β§x y. x β carrier R ==> y β carrier R ==> f (x β y) = f x β f y" proof- fix x y assume A: "x β carrier R""y β carrier R" show"f (x β y) = f x β f y" proof- have"f (x β y) = g (h (x β y))" by (simp add: A(1) A(2) assms(1) assms(6) ring.ring_simprules(1)) thenhave"f (x β y) = g ((h x) β (h y))" using A(1) A(2) assms(4) ring_hom_add by fastforce thenhave"f (x β y) = g (h x) β g (h y)" by (metis (no_types, opaque_lifting) A(1) A(2) assms(4) assms(5) ring_hom_add ring_hom_closed) thenshow ?thesis by (simp add: A(1) A(2) assms(6)) qed qed show"f 1 = 1" by (metis assms(1) assms(4) assms(5) assms(6) ring.ring_simprules(6) ring_hom_one) qed
(**************************************************************************************************) (**************************************************************************************************) sectionβΉBasic Notions about PolynomialsβΊ (**************************************************************************************************) (**************************************************************************************************) context UP_ring begin
textβΉrings are closed under monomial termsβΊ lemma monom_term_car: assumes"c β carrier R" assumes"x β carrier R" shows"c β x[^](n::nat) β carrier R" using assms monoid.nat_pow_closed by blast
textβΉUnivariate polynomial ring over RβΊ
lemma P_is_UP_ring: "UP_ring R" by (simp add: UP_ring_axioms)
textβΉDegree functionβΊ abbreviation(input) degree where "degree f β‘ deg R f"
lemma UP_car_memI: assumes"β§n. n > k ==> p n = 0" assumes"β§n. p n β carrier R" shows"p β carrier P" proof- have"bound 0 k p" by (simp add: assms(1) bound.intro) thenshow ?thesis by (metis (no_types, lifting) P_def UP_def assms(2) mem_upI partial_object.select_convs(1)) qed
lemma(in UP_cring) UP_car_memI': assumes"β§x. g x β carrier R" assumes"β§x. x > k ==> g x = 0" shows"g β carrier (UP R)" proof- have"bound 0 k g" using assms unfolding bound_def by blast thenshow ?thesis using P_def UP_car_memI assms(1) by blast qed
lemma(in UP_cring) UP_car_memE: assumes"g β carrier (UP R)" shows"β§x. g x β carrier R" "β§x. x > (deg R g) ==> g x = 0" using P_def assms UP_def[of R] apply (simp add: mem_upD) using assms UP_def[of R] up_def[of R] by (smt (verit, del_insts) UP_ring.deg_aboveD is_UP_ring partial_object.select_convs(1) restrict_apply up_ring.select_convs(2))
end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉLemmas About CoefficientsβΊ (**************************************************************************************************) (**************************************************************************************************)
context UP_ring begin textβΉThe goal here is to reduce dependence on the function coeff from Univ\_Poly, in favour of using
polynomial itself as its coefficient function.βΊ
lemma coeff_simp: assumes"f β carrier P" shows"coeff (UP R) f = f " prooffix x show"coeff (UP R) f x = f x" using assms P_def UP_def[of R] by auto qed
textβΉCoefficients are in RβΊ
lemma cfs_closed: assumes"f β carrier P" shows"f n β carrier R" using assms coeff_simp[of f] P_def coeff_closed by fastforce
lemma cfs_monom: "a β carrier R ==> (monom P a m) n = (if m=n then a else 0)" using coeff_simp P_def coeff_monom monom_closed by auto
lemma cfs_zero [simp]: "0 n = 0" using P_def UP_zero_closed coeff_simp coeff_zero by auto
lemma cfs_one [simp]: "1 n = (if n=0 then 1 else 0)" by (metis P_def R.one_closed UP_ring.cfs_monom UP_ring_axioms monom_one)
lemma cfs_smult [simp]: "[| a β carrier R; p β carrier P |] ==> (a β p) n = a β p n" using P_def UP_ring.coeff_simp UP_ring_axioms UP_smult_closed coeff_smult by fastforce
lemma cfs_add [simp]: "[| p β carrier P; q β carrier P |] ==> (p β q) n = p n β q n" by (metis P.add.m_closed P_def UP_ring.coeff_add UP_ring.coeff_simp UP_ring_axioms)
lemma cfs_a_inv [simp]: assumes R: "p β carrier P" shows"(β p) n = β (p n)" using P.add.inv_closed P_def UP_ring.coeff_a_inv UP_ring.coeff_simp UP_ring_axioms assms by fastforce
lemma cfs_minus [simp]: "[| p β carrier P; q β carrier P |] ==> (p β q) n = p n β q n" using P.minus_closed P_def coeff_minus coeff_simp by auto
lemma cfs_monom_mult_r: assumes"p β carrier P" assumes"a β carrier R" shows"(monom P a n β p) (k + n) = a β p k" using coeff_monom_mult assms P.m_closed P_def coeff_simp monom_closed by auto
lemma(in UP_cring) cfs_monom_mult_l: assumes"p β carrier P" assumes"a β carrier R" shows"(p β monom P a n) (k + n) = a β p k" using UP_m_comm assms(1) assms(2) cfs_monom_mult_r by auto
lemma(in UP_cring) cfs_monom_mult_l': assumes"f β carrier P" assumes"a β carrier R" assumes"m β₯ n" shows"(f β (monom P a n)) m = a β (f (m - n))" using cfs_monom_mult_l[of f a n "m-n"] assms by simp
lemma(in UP_cring) cfs_monom_mult_r': assumes"f β carrier P" assumes"a β carrier R" assumes"m β₯ n" shows"((monom P a n) β f) m = a β (f (m - n))" using cfs_monom_mult_r[of f a n "m-n"] assms by simp end (**************************************************************************************************) (**************************************************************************************************) subsectionβΉDegree Bound LemmasβΊ (**************************************************************************************************) (**************************************************************************************************)
context UP_ring begin
lemma bound_deg_sum: assumes" f β carrier P" assumes"g β carrier P" assumes"degree f β€ n" assumes"degree g β€ n" shows"degree (f β g) β€ n" using P_def UP_ring_axioms assms(1) assms(2) assms(3) assms(4) by (meson deg_add max.boundedI order_trans)
lemma bound_deg_sum': assumes" f β carrier P" assumes"g β carrier P" assumes"degree f < n" assumes"degree g < n" shows"degree (f β g) < n" using P_def UP_ring_axioms assms(1) assms(2)
assms(3) assms(4) by (metis bound_deg_sum le_neq_implies_less less_imp_le_nat not_less)
lemma equal_deg_sum: assumes" f β carrier P" assumes"g β carrier P" assumes"degree f < n" assumes"degree g = n" shows"degree (f β g) = n" proof- have0: "degree (f β g) β€n" using assms bound_deg_sum
P_def UP_ring_axioms by auto show"degree (f β g) = n" proof(rule ccontr) assume"degree (f β g) β n " thenhave1: "degree (f β g) < n" using0by auto have2: "degree (β f) < n" using assms by simp have3: "g = (f β g) β (β f)" using assms by (simp add: P.add.m_comm P.r_neg1) thenshow False using123 assms by (metis UP_a_closed UP_a_inv_closed deg_add leD le_max_iff_disj) qed qed
lemma equal_deg_sum': assumes"f β carrier P" assumes"g β carrier P" assumes"degree g < n" assumes"degree f = n" shows"degree (f β g) = n" using P_def UP_a_comm UP_ring.equal_deg_sum UP_ring_axioms assms(1) assms(2) assms(3) assms(4) by fastforce
lemma degree_of_difference_diff_degree: assumes"p β carrier P" assumes"q β carrier P" assumes"degree q < degree p" shows"degree (p β q) = degree p" proof- have A: "(p β q) = p β (β q)" by (simp add: P.minus_eq) have"degree (β q) = degree q " by (simp add: assms(2)) thenshow ?thesis using assms A by (simp add: degree_of_sum_diff_degree) qed
lemma (in UP_ring) deg_diff_by_const: assumes"g β carrier (UP R)" assumes"a β carrier R" assumes"h = g β R up_ring.monom (UP R) a 0" shows"deg R g = deg R h" unfolding assms using assms by (metis P_def UP_ring.bound_deg_sum UP_ring.deg_monom_le UP_ring.monom_closed UP_ring_axioms degree_of_sum_diff_degree gr_zeroI not_less)
lemma (in UP_ring) deg_diff_by_const': assumes"g β carrier (UP R)" assumes"a β carrier R" assumes"h = g β R up_ring.monom (UP R) a 0" shows"deg R g = deg R h" apply(rule deg_diff_by_const[of _ "β a"]) using assms apply blast using assms apply blast by (metis P.minus_eq P_def assms(2) assms(3) monom_a_inv)
lemma(in UP_ring) deg_gtE: assumes"p β carrier P" assumes"i > deg R p" shows"p i = 0" using assms P_def coeff_simp deg_aboveD by metis end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉLeading Term FunctionβΊ (**************************************************************************************************) (**************************************************************************************************)
definition leading_term where "leading_term R f = monom (UP R) (f (deg R f)) (deg R f)"
context UP_ring begin
abbreviation(input) ltrm where "ltrm f β‘ monom P (f (deg R f)) (deg R f)"
textβΉleading term is a polynomialβΊ lemma ltrm_closed: assumes"f β carrier P" shows"ltrm f β carrier P" using assms by (simp add: cfs_closed)
textβΉSimplified coefficient function description for leading termβΊ lemma ltrm_coeff: assumes"f β carrier P" shows"coeff P (ltrm f) n = (if (n = degree f) then (f (degree f)) else 0)" using assms by (simp add: cfs_closed)
lemma ltrm_cfs: assumes"f β carrier P" shows"(ltrm f) n = (if (n = degree f) then (f (degree f)) else 0)" using assms by (simp add: cfs_closed cfs_monom)
lemma ltrm_cfs_above_deg: assumes"f β carrier P" assumes"n > degree f" shows"ltrm f n = 0" using assms by (simp add: ltrm_cfs)
textβΉThe leading term of f has the same degree as fβΊ
textβΉSubtracting the leading term yields a drop in degreeβΊ
lemma minus_ltrm_degree_drop: assumes"f β carrier P" assumes"degree f = Suc n" shows"degree (f β (ltrm f)) β€ n" proof(rule UP_ring.deg_aboveI) show C0: "UP_ring R" by (simp add: UP_ring_axioms) show C1: "f β ltrm f β carrier (UP R)" using assms ltrm_closed P.minus_closed P_def by blast show C2: "β§m. n < m ==> coeff (UP R) (f β ltrm f) m = 0" proof- fix m assume A: "n<m" show"coeff (UP R) (f β ltrm f) m = 0" proof(cases " m = Suc n") case True have B: "f m β carrier R" using UP.coeff_closed P_def assms(1) cfs_closed by blast have"m = degree f" using True by (simp add: assms(2)) thenhave"f m = (ltrm f) m" using ltrm_cfs assms(1) by auto thenhave"(f m) β( ltrm f) m = 0" using B UP_ring_def P_is_UP_ring
B R.add.r_inv R.is_abelian_group abelian_group.minus_eq by fastforce thenhave"(f β R ltrm f) m = 0" by (metis C1 ltrm_closed P_def assms(1) coeff_minus coeff_simp) thenshow ?thesis using C1 P_def UP_ring.coeff_simp UP_ring_axioms by fastforce next case False have D0: "m > degree f"using False using A assms(2) by linarith have B: "f m β carrier R" using UP.coeff_closed P_def assms(1) cfs_closed by blast have"f m = (ltrm f) m" using D0 ltrm_cfs_above_deg P_def assms(1) coeff_simp deg_aboveD by auto thenshow ?thesis by (metis B ltrm_closed P_def R.r_neg UP_ring.coeff_simp UP_ring_axioms a_minus_def assms(1) coeff_minus) qed qed qed
lemma ltrm_decomp: assumes"f β carrier P" assumes"degree f >(0::nat)" obtains g where"g β carrier P β§ f = g β (ltrm f) β§ degree g < degree f" proof- have0: "f β (ltrm f) β carrier P" using ltrm_closed assms(1) by blast have1: "f = (f β (ltrm f)) β (ltrm f)" using assms by (metis "0" ltrm_closed P.add.inv_solve_right P.minus_eq) show ?thesis using assms 01 minus_ltrm_degree_drop[of f] by (metis ltrm_closed Suc_diff_1 Suc_n_not_le_n deg_ltrm equal_deg_sum' linorder_neqE_nat that) qed
textβΉleading term of a sumβΊ lemma coeff_of_sum_diff_degree0: assumes"p β carrier P" assumes"q β carrier P" assumes"degree q < n" shows"(p β q) n = p n" using assms P_def UP_ring.deg_aboveD UP_ring_axioms cfs_add coeff_simp cfs_closed deg_aboveD by auto
lemma trunc_zero: assumes"f β carrier P" assumes"degree f = 0" shows"trunc f = 0" unfolding truncate_def using assms ltrm_deg_0[of f] by (metis P.r_neg P_def a_minus_def leading_term_def)
lemma trunc_degree: assumes"f β carrier P" assumes"degree f > 0" shows"degree (trunc f) < degree f" unfolding truncate_def using assms by (metis ltrm_closed ltrm_decomp P.add.right_cancel Cring_Poly.truncate_def trunc_closed trunc_simps(1))
textβΉThe coefficients of trunc agree with f for small degreeβΊ
lemma trunc_cfs: assumes"p β carrier P" assumes"n < degree p" shows" (trunc p) n = p n" using P_def assms(1) assms(2) unfolding truncate_def by (smt (verit) ltrm_closed ltrm_cfs R.minus_zero R.ring_axioms UP_ring.cfs_minus
UP_ring_axioms a_minus_def cfs_closed leading_term_def nat_neq_iff ring.ring_simprules(15))
textβΉmonomial predicateβΊ
definition is_UP_monom where "is_UP_monom = (λf. f β carrier (UP R) β§ f = ltrm f)"
lemma is_UP_monomI: assumes"a β carrier R" assumes"p = monom P a n" shows"is_UP_monom p" using assms(1) assms(2) is_UP_monom_def ltrm_monom P_def monom_closed by auto
lemma is_UP_monomI': assumes"f β carrier (UP R)" assumes"f = ltrm f" shows"is_UP_monom f" using assms P_def unfolding is_UP_monom_def by blast
lemma monom_is_UP_monom: assumes"a β carrier R" shows"is_UP_monom (monom P a n)""is_UP_monom (monom (UP R) a n)" using assms P_def ltrm_monom_simp monom_closed unfolding is_UP_monom_def by auto
lemma ltrm_is_UP_monom: assumes"p β carrier P" shows"is_UP_monom (ltrm p)" using assms by (simp add: cfs_closed monom_is_UP_monom(1))
lemma is_UP_monom_mult: assumes"is_UP_monom p" assumes"is_UP_monom q" shows"is_UP_monom (p β q)" apply(rule is_UP_monomI') using assms is_UP_monomE P_def UP_mult_closed apply simp using assms is_UP_monomE[of p] is_UP_monomE[of q]
P_def monom_mult by (metis lcf_closed ltrm_monom R.m_closed) end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉProperties of Leading Terms and Leading Coefficients in Commutative Rings and DomainsβΊ (**************************************************************************************************) (**************************************************************************************************)
context UP_cring begin
lemma cring_deg_mult: assumes"q β carrier P" assumes"p β carrier P" assumes"lcf q β lcf p β 0" shows"degree (q β p) = degree p + degree q" proof- have"q β p = (trunc q β ltrm q) β (trunc p β ltrm p)" using assms(1) assms(2) trunc_simps(1) by auto thenhave"q β p = (trunc q β ltrm q) β (trunc p β ltrm p)" by linarith thenhave0: "q β p = (trunc q β (trunc p β ltrm p)) β ( ltrm q β (trunc p β ltrm p))" by (simp add: P.l_distr assms(1) assms(2) ltrm_closed trunc_closed) have1: "(trunc q β (trunc p β ltrm p)) (degree p + degree q) = 0" proof(cases "degree q = 0") case True thenshow ?thesis using assms(1) assms(2) trunc_simps(1) trunc_zero by auto next case False have"degree ((trunc q) β p) β€ degree (trunc q) + degree p" using assms trunc_simps[of q] deg_mult_ring[of "trunc q" p] trunc_closed by blast thenhave"degree (trunc q β (trunc p β ltrm p)) < degree q + degree p" using False assms(1) assms(2) trunc_degree trunc_simps(1) by fastforce thenshow ?thesis by (metis P_def UP_mult_closed UP_ring.coeff_simp UP_ring_axioms
add.commute assms(1) assms(2) deg_belowI not_less trunc_closed trunc_simps(1)) qed have2: "(q β p) (degree p + degree q) = ( ltrm q β (trunc p β ltrm p)) (degree p + degree q)" using01 assms cfs_closed trunc_closed by auto have3: "(q β p) (degree p + degree q) = ( ltrm q β trunc p) (degree p + degree q) β ( ltrm q β ltrm p) (degree p + degree q)" by (simp add: "2" ltrm_closed UP_r_distr assms(1) assms(2) trunc_closed) have4: "( ltrm q β trunc p) (degree p + degree q) = 0" proof(cases "degree p = 0") case True thenshow ?thesis using"2""3" assms(1) assms(2) cfs_closed ltrm_closed trunc_zero by auto next case False have"degree ( ltrm q β trunc p) β€ degree (ltrm q) + degree (trunc p)" using assms trunc_simps deg_mult_ring ltrm_closed trunc_closed by presburger thenhave"degree ( ltrm q β trunc p) < degree q + degree p" using False assms(1) assms(2) trunc_degree trunc_simps(1) deg_ltrm by fastforce thenshow ?thesis by (metis ltrm_closed P_def UP_mult_closed UP_ring.coeff_simp UP_ring_axioms add.commute assms(1) assms(2) deg_belowI not_less trunc_closed) qed have5: "(q β p) (degree p + degree q) = ( ltrm q β ltrm p) (degree p + degree q)" by (simp add: "3""4" assms(1) assms(2) cfs_closed) have6: "ltrm q β ltrm p = monom P (lcf q β lcf p) (degree p + degree q)" unfolding leading_term_def by (metis P_def UP_ring.monom_mult UP_ring_axioms add.commute assms(1) assms(2) cfs_closed) have7: "( ltrm q β ltrm p) (degree p + degree q) β 0" using56 assms by (metis R.m_closed cfs_closed cfs_monom) have8: "degree (q β p) β₯degree p + degree q" using567 P_def UP_mult_closed assms(1) assms(2) by (simp add: UP_ring.coeff_simp UP_ring_axioms deg_belowI) thenshow ?thesis using assms(1) assms(2) deg_mult_ring by fastforce qed
textβΉleading term is multiplicativeβΊ
lemma ltrm_of_sum_diff_deg: assumes"q β carrier P" assumes"a β carrier R" assumes"a β 0" assumes"degree q < n" assumes"p = q β (monom P a n)" shows"ltrm p = (monom P a n)" proof- have0: "degree (monom P a n) = n" by (simp add: assms(2) assms(3)) have1: "(monom P a n) β carrier P" using assms(2) by auto have2: "ltrm ((monom P a n) β q) = ltrm (monom P a n)" using assms ltrm_of_sum_diff_degree[of "(monom P a n)" q] 1"0"by linarith thenshow ?thesis using UP_a_comm assms(1) assms(2) assms(5) ltrm_monom by auto qed
lemma(in UP_cring) ltrm_smult_cring: assumes"p β carrier P" assumes"a β carrier R" assumes"lcf p β a β 0" shows"ltrm (a βp) = aβ(ltrm p)" using assms by (smt (verit) lcf_monom(1) P_def R.m_closed R.m_comm cfs_closed cfs_smult coeff_simp
cring_deg_mult deg_monom deg_ltrm monom_closed monom_mult_is_smult monom_mult_smult)
lemma lcf_deg_0: assumes"degree p = 0" assumes"p β carrier P" assumes"q β carrier P" shows"(p β q) = (lcf p)βq" using P_def assms(1) assms(2) assms(3) by (metis ltrm_deg_0 cfs_closed monom_mult_is_smult)
textβΉleading term powersβΊ
lemma (indomain) nonzero_pow_nonzero: assumes"a β carrier R" assumes"a β 0" shows"a[^](n::nat) β 0" proof(induction n) case0 thenshow ?case by auto next case (Suc n) fix n::nat assume IH: "a[^] n β 0" show"a[^] (Suc n) β 0" proof- have"a[^] (Suc n) = a[^] n β a" by simp thenshow ?thesis using assms IH using IH assms(1) assms(2) local.integral by auto qed qed
lemma (in UP_cring) cring_monom_degree: assumes"a β (carrier R)" assumes"p = monom P a m" assumes"a[^]n β 0" shows"degree (p[^] n) = n*m" by (simp add: assms(1) assms(2) assms(3) monom_pow)
lemma (in UP_domain) monom_degree: assumes"a β 0" assumes"a β (carrier R)" assumes"p = monom P a m" shows"degree (p[^] n) = n*m" by (simp add: R.domain_axioms assms(1) assms(2) assms(3) domain.nonzero_pow_nonzero monom_pow)
lemma(in UP_cring) cring_pow_ltrm: assumes"p β carrier P" assumes"lcf p [^]n β 0" shows"ltrm (p[^](n::nat)) = (ltrm p)[^]n" proof- have"lcf p [^]n β 0==> ltrm (p[^](n::nat)) = (ltrm p)[^]n" proof(induction n) case0 thenshow ?case using P.ring_simprules(6) P.nat_pow_0 cfs_one deg_one monom_one by presburger next case (Suc n) fix n::nat assume IH : "(lcf p [^] n β 0==> ltrm (p [^] n) = ltrm p [^] n)" assume A: "lcf p [^] Suc n β 0" have a: "ltrm (p [^] n) = ltrm p [^] n" apply(cases "lcf p [^] n = 0") using A lcf_closed assms(1) apply auto[1] by(rule IH) have0: "lcf (ltrm (p [^] n)) = lcf p [^] n" unfolding a by (simp add: lcf_monom(1) assms(1) cfs_closed monom_pow) thenhave1: "lcf (ltrm (p [^] n)) β lcf p β 0" using assms A R.nat_pow_Suc IH by metis thenshow"ltrm (p [^] Suc n) = ltrm p [^] Suc n" using IH 0 assms(1) cring_ltrm_mult cfs_closed by (smt (verit) A lcf_monom(1) ltrm_closed P.nat_pow_Suc2 P.nat_pow_closed R.nat_pow_Suc2 a) qed thenshow ?thesis using assms(2) by blast qed
lemma(in UP_cring) cring_pow_deg: assumes"p β carrier P" assumes"lcf p [^]n β 0" shows"degree (p[^](n::nat)) = n*degree p" proof- have"degree ( (ltrm p)[^]n) = n*degree p" using assms(1) assms(2) cring_monom_degree lcf_closed lcf_ltrm by auto thenshow ?thesis using assms cring_pow_ltrm by (metis P.nat_pow_closed P_def UP_ring.deg_ltrm UP_ring_axioms) qed
lemma(in UP_cring) deg_smult: assumes"a β carrier R" assumes"f β carrier (UP R)" assumes"a β lcf f β 0" shows"deg R (a β R f) = deg R f" using assms P_def cfs_smult deg_eqI deg_smult_decr smult_closed by (metis deg_gtE le_neq_implies_less)
lemma(in UP_cring) deg_smult': assumes"a β Units R" assumes"f β carrier (UP R)" shows"deg R (a β R f) = deg R f" apply(cases "deg R f = 0") apply (metis P_def R.Units_closed assms(1) assms(2) deg_smult_decr le_zero_eq) apply(rule deg_smult) using assms apply blast using assms apply blast proof assume A: "deg R f β 0""a β f (deg R f) = 0" have0: "f (deg R f) = 0" using A assms R.Units_not_right_zero_divisor[of a "f (deg R f)"] UP_car_memE(1) by blast thenshow False using assms A by (metis P_def deg_zero deg_ltrm monom_zero) qed
lemma(in UP_domain) pow_sum0: "β§ p q. p β carrier P ==> q β carrier P ==> degree q < degree p ==> degree ((p βq )[^]n) = (degree p)*n" proof(induction n) case0 thenshow ?case by (metis Group.nat_pow_0 deg_one mult_is_0) next case (Suc n) fix n assume IH: "β§ p q. p β carrier P ==> q β carrier P ==> degree q < degree p ==> degree ((p β q )[^]n) = (degree p)*n" thenshow"β§ p q. p β carrier P ==> q β carrier P ==> degree q < degree p ==> degree ((p β q )[^](Suc n)) = (degree p)*(Suc n)" proof- fix p q assume A0: "p β carrier P"and
A1: "q β carrier P"and
A2: "degree q < degree p" show"degree ((p β q )[^](Suc n)) = (degree p)*(Suc n)" proof(cases "q = 0") case True thenshow ?thesis by (metis A0 A1 A2 IH P.nat_pow_Suc2 P.nat_pow_closed P.r_zero deg_mult domain.nonzero_pow_nonzero local.domain_axioms mult_Suc_right nat_neq_iff) next case False thenshow ?thesis proof- have P0: "degree ((p β q )[^]n) = (degree p)*n" using A0 A1 A2 IH by auto have P1: "(p β q )[^](Suc n) = ((p β q )[^]n) β (p β q )" by simp thenhave P2: "(p β q )[^](Suc n) = (((p β q )[^]n) β p) β (((p β q )[^]n) β q)" by (simp add: A0 A1 UP_r_distr) have P3: "degree (((p β q )[^]n) β p) = (degree p)*n + (degree p)" using P0 A0 A1 A2 deg_nzero_nzero degree_of_sum_diff_degree local.nonzero_pow_nonzero byauto have P4: "degree (((p β q )[^]n) β q) = (degree p)*n + (degree q)" using P0 A0 A1 A2 deg_nzero_nzero degree_of_sum_diff_degree local.nonzero_pow_nonzero False deg_mult by simp have P5: "degree (((p β q )[^]n) β p) > degree (((p β q )[^]n) β q)" using P3 P4 A2 by auto thenshow ?thesis using P5 P3 P2 by (simp add: A0 A1 degree_of_sum_diff_degree) qed qed qed qed
lemma(in UP_domain) deg_pow0: "β§ p. p β carrier P ==> n β₯ degree p ==> degree (p [^] m) = m*(degree p)" proof(induction n) case0 show"p β carrier P ==> 0 β₯ degree p ==> degree (p [^] m) = m*(degree p)" proof- assume B0:"p β carrier P" assume B1: "0 β₯ degree p" thenobtain a where a_def: "a β carrier R β§ p = monom P a 0" using B0 deg_zero_impl_monom by fastforce show"degree (p [^] m) = m*(degree p)"using UP_cring.monom_pow by (metis P_def R.nat_pow_closed UP_cring_axioms a_def deg_const
mult_0_right mult_zero_left) qed next case (Suc n) fix n assume IH: "β§p. (p β carrier P ==> n β₯degree p ==> degree (p [^] m) = m * (degree p))" show"p β carrier P ==> Suc n β₯ degree p ==> degree (p [^] m) = m * (degree p)" proof- assume A0: "p β carrier P" assume A1: "Suc n β₯ degree p" show"degree (p [^] m) = m * (degree p)" proof(cases "Suc n > degree p") case True thenshow ?thesis using IH A0 by simp next case False thenshow ?thesis proof- obtain q where q_def: "q = trunc p" by simp obtain k where k_def: "k = degree q" by simp have q_is_poly: "q β carrier P" by (simp add: A0 q_def trunc_closed) have k_bound0: "k <degree p" using k_def q_def trunc_degree[of p] A0 False by auto have k_bound1: "k β€ n" using k_bound0 A0 A1 by auto have P_q:"degree (q [^] m) = m * k" using IH[of "q"] k_bound1 k_def q_is_poly by auto have P_ltrm: "degree ((ltrm p) [^] m) = m*(degree p)" proof- have"degree p = degree (ltrm p)" by (simp add: A0 deg_ltrm) thenshow ?thesis using monom_degree by (metis A0 P.r_zero P_def cfs_closed coeff_simp equal_deg_sum k_bound0 k_def lcoeff_nonzero2 nat_neq_iff q_is_poly) qed have"p = q β (ltrm p)" by (simp add: A0 q_def trunc_simps(1)) thenshow ?thesis using P_q pow_sum[of "(ltrm p)" q m] A0 UP_a_comm
deg_ltrm k_bound0 k_def ltrm_closed q_is_poly by auto qed qed qed qed
lemma(in UP_domain) deg_pow: assumes"p β carrier P" shows"degree (p [^] m) = m*(degree p)" using deg_pow0 assms by blast
lemma(in UP_domain) ltrm_pow0: "β§f. f β carrier P ==> ltrm (f [^] (n::nat)) = (ltrm f) [^] n" proof(induction n) case0 thenshow ?case using ltrm_deg_0 P.nat_pow_0 P.ring_simprules(6) deg_one by presburger next case (Suc n) fix n::nat assume IH: "β§f. f β carrier P ==> ltrm (f [^] n) = (ltrm f) [^] n" thenshow"β§f. f β carrier P ==> ltrm (f [^] (Suc n)) = (ltrm f) [^] (Suc n)" proof- fix f assume A: "f β carrier P" show" ltrm (f [^] (Suc n)) = (ltrm f) [^] (Suc n)" proof- have0: "ltrm (f [^] n) = (ltrm f) [^] n" using A IH by blast have1: "ltrm (f [^] (Suc n)) = ltrm ((f [^] n)β f)" by auto then show ?thesis using ltrm_mult 01 by (simp add: A) qed qed qed
lemma zcf_zero[simp]: "zcf 0 = 0" using zcf_degree_zero by auto
lemma zcf_one[simp]: "zcf 1 = 1" by (simp add: zcf_def)
lemma ctrm_smult: assumes"f β carrier P" assumes"a β carrier R" shows"ctrm (a β f) = a β(ctrm f)" using P_def UP_ring.monom_mult_smult UP_ring_axioms assms(1) assms(2) cfs_smult coeff_simp by (simp add: UP_ring.monom_mult_smult cfs_closed)
lemma ctrm_monom[simp]: assumes"a β carrier R" shows"ctrm (monom P a (Suc k)) = 0" by (simp add: assms cfs_monom) end (**************************************************************************************************) (**************************************************************************************************) subsectionβΉPolynomial Induction RulesβΊ (**************************************************************************************************) (**************************************************************************************************)
context UP_ring begin
textβΉRule for strong induction on polynomial degreeβΊ
lemma poly_induct: assumes"p β carrier P" assumes Deg_0: "β§p. p β carrier P ==> degree p = 0 ==> Q p" assumes IH: "β§p. (β§q. q β carrier P ==> degree q < degree p ==> Q q) ==> p β carrier P ==> degree p > 0 ==> Q p" shows"Q p" proof- have"β§n. β§p. p β carrier P ==> degree p β€ n ==> Q p" proof- fix n show"β§p. p β carrier P ==> degree p β€ n ==> Q p" proof(induction n) case0 thenshow ?case using Deg_0 by simp next case (Suc n) fix n assume I: "β§p. p β carrier P ==> degree p β€ n ==> Q p" show"β§p. p β carrier P ==> degree p β€ (Suc n) ==> Q p" proof- fix p assume A0: " p β carrier P " assume A1: "degree p β€Suc n" show"Q p" proof(cases "degree p < Suc n") case True thenshow ?thesis using I A0 by auto next case False thenhave D: "degree p = Suc n" by (simp add: A1 nat_less_le) thenhave"(β§q. q β carrier P ==> degree q < degree p ==> Q q)" using I by simp thenshow"Q p" using IH D A0 A1 Deg_0 by blast qed qed qed qed thenshow ?thesis using assms by blast qed
textβΉVariant on induction on degreeβΊ
lemma poly_induct2: assumes"p β carrier P" assumes Deg_0: "β§p. p β carrier P ==> degree p = 0 ==> Q p" assumes IH: "β§p. degree p > 0 ==> p β carrier P ==> Q (trunc p) ==> Q p" shows"Q p" proof(rule poly_induct) show"p β carrier P" by (simp add: assms(1)) show"β§p. p β carrier P ==> degree p = 0 ==> Q p" by (simp add: Deg_0) show"β§p. (β§q. q β carrier P ==> degree q < degree p ==> Q q) ==> p β carrier P ==> 0 < degree p ==> Q p" proof- fix p assume A0: "(β§q. q β carrier P ==> degree q < degree p ==> Q q)" assume A1: " p β carrier P" assume A2: "0 < degree p" show"Q p" proof- have"degree (trunc p) < degree p" by (simp add: A1 A2 trunc_degree) have"Q (trunc p)" by (simp add: A0 A1 βΉdegree (trunc p) < degree pβΊ trunc_closed) thenshow ?thesis by (simp add: A1 A2 IH) qed qed qed
textβΉAdditive properties which are true for all monomials are true for all polynomials βΊ
lemma poly_induct3: assumes"p β carrier P" assumes add: "β§p q. q β carrier P ==> p β carrier P ==> Q p ==> Q q ==> Q (p β q)" assumes monom: "β§a n. a β carrier R ==> Q (monom P a n)" shows"Q p" apply(rule poly_induct2) apply (simp add: assms(1)) apply (metis lcf_closed P_def coeff_simp deg_zero_impl_monom monom) by (metis lcf_closed ltrm_closed add monom trunc_closed trunc_simps(1))
lemma poly_induct4: assumes"p β carrier P" assumes add: "β§p q. q β carrier P ==> p β carrier P ==> Q p ==> Q q ==> Q (p β q)" assumes monom_zero: "β§a. a β carrier R ==> Q (monom P a 0)" assumes monom_Suc: "β§a n. a β carrier R ==> Q (monom P a (Suc n))" shows"Q p" apply(rule poly_induct3) using assms(1) apply auto[1] using add apply blast using monom_zero monom_Suc by (metis P_def UP_ring.monom_zero UP_ring_axioms deg_monom deg_monom_le le_0_eq le_SucE zero_induct)
lemma monic_monom_smult: assumes"a β carrier R" shows"a β monom P 1 n = monom P a n" using assms by (metis R.one_closed R.r_one monom_mult_smult)
lemma poly_induct5: assumes"p β carrier P" assumes add: "β§p q. q β carrier P ==> p β carrier P ==> Q p ==> Q q ==> Q (p β q)" assumes monic_monom: "β§n. Q (monom P 1 n)" assumes smult: "β§p a . a β carrier R ==> p β carrier P ==> Q p ==> Q (a β p)" shows"Q p" apply(rule poly_induct3) apply (simp add: assms(1)) using add apply blast proof- fix a n assume A: "a β carrier R"show"Q (monom P a n)" using monic_monom[of n] smult[of a "monom P 1 n"] monom_mult_smult[of a 1 n] by (simp add: A) qed
lemma poly_induct6: assumes"p β carrier P" assumes monom: "β§a n. a β carrier R ==> Q (monom P a 0)" assumes plus_monom: "β§a n p. a β carrier R ==> a β 0==> p β carrier P ==> degree p < n ==> Q p ==> Q(p β monom P a n)" shows"Q p" apply(rule poly_induct2) using assms(1) apply auto[1] apply (metis lcf_closed P_def coeff_simp deg_zero_impl_monom monom) using plus_monom by (metis lcf_closed P_def coeff_simp lcoeff_nonzero_deg nat_less_le trunc_closed trunc_degree trunc_simps(1))
end
(**************************************************************************************************) (**************************************************************************************************) sectionβΉMapping a Polynomial to its Associated Ring FunctionβΊ (**************************************************************************************************) (**************************************************************************************************)
textβΉTurning a polynomial into a function on R:βΊ definition to_function where "to_function S f = (λs β carrier S. eval S S (λx. x) s f)"
context UP_cring begin
definition to_fun where "to_fun f β‘ to_function R f"
textβΉExplicit formula for evaluating a polynomial function:βΊ
lemma to_fun_eval: assumes"f β carrier P" assumes"x β carrier R" shows"to_fun f x = eval R R (λx. x) x f" using assms unfolding to_function_def to_fun_def by auto
lemma to_fun_formula: assumes"f β carrier P" assumes"x β carrier R" shows"to_fun f x = (β¨i β {..degree f}. (f i) β x [^] i)" proof- have"f β carrier (UP R)" using assms P_def by auto thenhave"eval R R (λx. x) x f = (β¨iβ{..deg R f}. (λx. x) (coeff (UP R) f i) β x [^] i)" apply(simp add:UnivPoly.eval_def) done thenhave"to_fun f x = (β¨iβ{..deg R f}. (λx. x) (coeff (UP R) f i) β x [^] i)" using to_function_def assms unfolding to_fun_def by (simp add: to_function_def) thenshow ?thesis by(simp add: assms coeff_simp) qed
lemma eval_ring_hom: assumes"a β carrier R" shows"eval R R (λx. x) a β ring_hom P R" proof- have"(λx. x) β ring_hom R R" apply(rule ring_hom_memI) apply auto done thenhave"UP_pre_univ_prop R R (λx. x)" using R_cring UP_pre_univ_propI by blast thenshow ?thesis by (simp add: P_def UP_pre_univ_prop.eval_ring_hom assms) qed
lemma to_fun_closed: assumes"f β carrier P" assumes"x β carrier R" shows"to_fun f x β carrier R" using assms to_fun_eval[of f x] eval_ring_hom[of x]
ring_hom_closed by fastforce
lemma to_fun_plus: assumes"g β carrier P" assumes"f β carrier P" assumes"x β carrier R" shows"to_fun (f β g) x = (to_fun f x) β (to_fun g x)" using assms to_fun_eval[of ] eval_ring_hom[of x] by (simp add: ring_hom_add)
lemma to_fun_mult: assumes"g β carrier P" assumes"f β carrier P" assumes"x β carrier R" shows"to_fun (f β g) x = (to_fun f x) β (to_fun g x)" using assms to_fun_eval[of ] eval_ring_hom[of x] by (simp add: ring_hom_mult)
lemma to_fun_ring_hom: assumes"a β carrier R" shows"(λp. to_fun p a) β ring_hom P R" apply(rule ring_hom_memI) apply (simp add: assms to_fun_closed) apply (simp add: assms to_fun_mult) apply (simp add: assms to_fun_plus) using to_fun_eval[of "1" a] eval_ring_hom[of a]
ring_hom_closed by (simp add: assms ring_hom_one)
lemma ring_hom_uminus: assumes"ring S" assumes"f β (ring_hom S R)" assumes"a β carrier S" shows"f (β a) = β (f a)" proof- have"f (a β a) = (f a) β f (β a)" unfolding a_minus_def by (simp add: assms(1) assms(2) assms(3) ring.ring_simprules(3) ring_hom_add) thenhave"(f a) β f (β a) = 0 " by (metis R.ring_axioms a_minus_def assms(1) assms(2) assms(3)
ring.ring_simprules(16) ring_hom_zero) thenshow ?thesis by (metis (no_types, lifting) R.add.m_comm R.minus_equality assms(1)
assms(2) assms(3) ring.ring_simprules(3) ring_hom_closed) qed
lemma to_fun_minus: assumes"f β carrier P" assumes"x β carrier R" shows"to_fun (βf) x = β (to_fun f x)" unfolding to_function_def to_fun_def using eval_ring_hom[of x] assms by (simp add: UP_ring ring_hom_uminus)
lemma id_is_hom: "ring_hom_cring R R (λx. x)" proof(rule ring_hom_cringI) show"cring R" by (simp add: R_cring ) show"cring R" by (simp add: R_cring ) show"(λx. x) β ring_hom R R" unfolding ring_hom_def apply(auto) done qed
lemma UP_pre_univ_prop_fact: "UP_pre_univ_prop R R (λx. x)" unfolding UP_pre_univ_prop_def by (simp add: UP_cring_def R_cring id_is_hom)
end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉto-fun is a Ring Homomorphism from Polynomials to FunctionsβΊ (**************************************************************************************************) (**************************************************************************************************)
context UP_cring begin
lemma to_fun_is_Fun: assumes"x β carrier P" shows"to_fun x β carrier (Fun R)" apply(rule ring_functions.function_ring_car_memI) unfolding ring_functions_def apply(simp add: R.ring_axioms) using to_fun_closed assms apply auto[1] unfolding to_function_def to_fun_def by auto
lemma to_fun_function_ring_hom: "to_fun β ring_hom P (Fun R)" apply(rule ring_hom_memI) using to_fun_is_Fun apply auto[1] apply (simp add: to_fun_Fun_mult) apply (simp add: to_fun_Fun_add) by (simp add: to_fun_Fun_one)
lemma(in UP_cring) to_fun_one: assumes"a β carrier R" shows"to_fun 1 a = 1" using assms to_fun_Fun_one by (metis P_def UP_cring.to_fun_eval UP_cring_axioms UP_one_closed eval_ring_hom ring_hom_one)
lemma(in UP_cring) to_fun_zero: assumes"a β carrier R" shows"to_fun 0 a = 0" by (simp add: assms R.ring_axioms ring_functions.function_zero_eval ring_functions.intro to_fun_Fun_zero)
lemma(in UP_cring) to_fun_nat_pow: assumes"h β carrier (UP R)" assumes"a β carrier R" shows"to_fun (h[^] R(n::nat)) a = (to_fun h a)[^]n" apply(induction n) using assms to_fun_one apply (metis P.nat_pow_0 P_def R.nat_pow_0) using assms to_fun_mult P.nat_pow_closed P_def by auto
lemma(in UP_cring) to_fun_finsum: assumes"finite (Y::'d set)" assumes"f β UNIV → carrier (UP R)" assumes"t β carrier R" shows"to_fun (finsum (UP R) f Y) t = finsum R (λi. (to_fun (f i) t)) Y" proof(rule finite.induct[of Y]) show"finite Y" using assms by blast show"to_fun (finsum (UP R) f {}) t = (β¨iβ{}. to_fun (f i) t)" using P.finsum_empty[of f] assms unfolding P_def R.finsum_empty using P_def to_fun_zero by presburger show"β§A a. finite A ==> to_fun (finsum (UP R) f A) t = (β¨iβA. to_fun (f i) t) ==> to_fun (finsum (UP R) f (insert a A)) t = (β¨iβinsert a A. to_fun (f i) t)" proof- fix A :: "'d set"fix a assume A: "finite A""to_fun (finsum (UP R) f A) t = (β¨iβA. to_fun (f i) t)" show"to_fun (finsum (UP R) f (insert a A)) t = (β¨iβinsert a A. to_fun (f i) t)" proof(cases "a β A") case True thenshow ?thesis using A by (metis insert_absorb) next case False have0: "finsum (UP R) f (insert a A) = f a β R finsum (UP R) f A" using A False finsum_insert[of A a f] assms unfolding P_def by blast have1: "to_fun (f a βfinsum (UP R) f A ) t = to_fun (f a) t β to_fun (finsum (UP R) f A) t" apply(rule to_fun_plus[of "finsum (UP R) f A""f a" t]) using assms(2) finsum_closed[of f A] A unfolding P_def apply blast using P_def assms apply blast using assms by blast have2: "to_fun (f a βfinsum (UP R) f A ) t = to_fun (f a) t β (β¨iβA. to_fun (f i) t)" unfolding1 A by blast have3: "(β¨iβinsert a A. to_fun (f i) t) = to_fun (f a) t β (β¨iβA. to_fun (f i) t)" apply(rule R.finsum_insert, rule A, rule False) using to_fun_closed assms unfolding P_def apply blast apply(rule to_fun_closed) using assms unfolding P_def apply blast using assms by blast show ?thesis unfolding0unfolding3using2unfolding P_def by blast qed qed qed
end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉInclusion of a Ring into its Polynomials Ring via ConstantsβΊ (**************************************************************************************************) (**************************************************************************************************)
definition to_polynomial where "to_polynomial R = (λa. monom (UP R) a 0)"
context UP_cring begin
abbreviation(input) to_poly where "to_poly β‘ to_polynomial R"
lemma to_poly_mult_simp: assumes"b β carrier R" assumes"f β carrier (UP R)" shows"(to_polynomial R b) β R f = b β R f" "f β R (to_polynomial R b) = b β R f" unfolding to_polynomial_def using assms P_def monom_mult_is_smult apply auto[1] using UP_cring.UP_m_comm UP_cring_axioms UP_ring.monom_closed
UP_ring.monom_mult_is_smult UP_ring_axioms assms(1) assms(2) by fastforce
lemma to_fun_to_poly: assumes"a β carrier R" assumes"b β carrier R" shows"to_fun (to_poly a) b = a" unfolding to_function_def to_fun_def to_polynomial_def by (simp add: UP_pre_univ_prop.eval_const UP_pre_univ_prop_fact assms(1) assms(2))
lemma to_poly_inverse: assumes"f β carrier P" assumes"degree f = 0" shows"f = to_poly (f 0)" using P_def assms(1) assms(2) by (metis ltrm_deg_0 to_polynomial_def)
lemma to_poly_closed: assumes"a β carrier R" shows"to_poly a β carrier P" by (metis P_def assms monom_closed to_polynomial_def)
lemma degree_to_poly[simp]: assumes"a β carrier R" shows"degree (to_poly a) = 0" by (metis P_def assms deg_const to_polynomial_def)
lemma to_poly_is_ring_hom: "to_poly β ring_hom R P" unfolding to_polynomial_def unfolding P_def using UP_ring.const_ring_hom[of R]
UP_ring_axioms by simp
lemma to_poly_add: assumes"a β carrier R" assumes"b β carrier R" shows"to_poly (a β b) = to_poly a β to_poly b" by (simp add: assms(1) assms(2) ring_hom_add to_poly_is_ring_hom)
lemma to_poly_mult: assumes"a β carrier R" assumes"b β carrier R" shows"to_poly (a β b) = to_poly a β to_poly b" by (simp add: assms(1) assms(2) ring_hom_mult to_poly_is_ring_hom)
lemma to_poly_minus: assumes"a β carrier R" assumes"b β carrier R" shows"to_poly (a β b) = to_poly a β to_poly b" by (metis P.minus_eq P_def R.add.inv_closed R.ring_axioms UP_ring.monom_add
UP_ring_axioms assms(1) assms(2) monom_a_inv ring.ring_simprules(14) to_polynomial_def)
lemma to_poly_a_inv: assumes"a β carrier R" shows"to_poly (β a) = β to_poly a" by (metis P_def assms monom_a_inv to_polynomial_def)
lemma to_poly_nat_pow: assumes"a β carrier R" shows"(to_poly a) [^] (n::nat)= to_poly (a[^]n)" using assms UP_cring UP_cring_axioms UP_cring_def UnivPoly.ring_hom_cringI ring_hom_cring.hom_pow to_poly_is_ring_hom by fastforce
definitioncomposewhere "compose R f g = eval R (UP R) (to_polynomial R) g f"
abbreviation(in UP_cring)(input) sub (infixlβΉofβΊ70) where "sub f g β‘ compose R f g"
definition rev_compose where "rev_compose R = eval R (UP R) (to_polynomial R)"
abbreviation(in UP_cring)(input) rev_sub where "rev_sub β‘ rev_compose R"
context UP_cring begin
lemma sub_rev_sub: "sub f g = rev_sub g f" unfolding compose_def rev_compose_def by simp
lemma(in UP_cring) to_poly_UP_pre_univ_prop: "UP_pre_univ_prop R P to_poly" proof show"to_poly β ring_hom R P" by (simp add: to_poly_is_ring_hom) qed
lemma rev_sub_is_hom: assumes"g β carrier P" shows"rev_sub g β ring_hom P P" unfolding rev_compose_def using to_poly_UP_pre_univ_prop assms(1) UP_pre_univ_prop.eval_ring_hom[of R P to_poly g] unfolding P_def apply auto done
lemma rev_sub_closed: assumes"p β carrier P" assumes"q β carrier P" shows"rev_sub q p β carrier P" using rev_sub_is_hom[of q] assms ring_hom_closed[of "rev_sub q" P P p] by auto
lemma rev_sub_add: assumes"g β carrier P" assumes"f β carrier P" assumes"h βcarrier P" shows"rev_sub g (f β h) = (rev_sub g f) β (rev_sub g h)" using rev_sub_is_hom assms ring_hom_add by fastforce
lemma sub_add: assumes"g β carrier P" assumes"f β carrier P" assumes"h βcarrier P" shows"((f β h) of g) = ((f of g) β (h of g))" by (simp add: assms(1) assms(2) assms(3) rev_sub_add sub_rev_sub)
lemma rev_sub_mult: assumes"g β carrier P" assumes"f β carrier P" assumes"h βcarrier P" shows"rev_sub g (f β h) = (rev_sub g f) β (rev_sub g h)" using rev_sub_is_hom assms ring_hom_mult by fastforce
lemma sub_mult: assumes"g β carrier P" assumes"f β carrier P" assumes"h βcarrier P" shows"((f β h) of g) = ((f of g) β (h of g))" by (simp add: assms(1) assms(2) assms(3) rev_sub_mult sub_rev_sub)
lemma sub_monom: assumes"g β carrier (UP R)" assumes"a β carrier R" shows"sub (monom (UP R) a n) g = to_poly a β R (g[^] R (n::nat))" "sub (monom (UP R) a n) g = a β R (g[^] R (n::nat))" apply (simp add: UP_cring.to_poly_UP_pre_univ_prop UP_cring_axioms
UP_pre_univ_prop.eval_monom assms(1) assms(2) Cring_Poly.compose_def) by (metis P_def UP_cring.to_poly_mult_simp(1) UP_cring_axioms UP_pre_univ_prop.eval_monom
UP_ring assms(1) assms(2) Cring_Poly.compose_def monoid.nat_pow_closed ring_def to_poly_UP_pre_univ_prop)
textβΉSubbing into a constant does nothingβΊ
lemma rev_sub_to_poly: assumes"g β carrier P" assumes"a β carrier R" shows"rev_sub g (to_poly a) = to_poly a" unfolding to_polynomial_def rev_compose_def using to_poly_UP_pre_univ_prop unfolding to_polynomial_def using P_def UP_pre_univ_prop.eval_const assms(1) assms(2) by fastforce
lemma sub_to_poly: assumes"g β carrier P" assumes"a β carrier R" shows"(to_poly a) of g = to_poly a" by (simp add: assms(1) assms(2) rev_sub_to_poly sub_rev_sub)
lemma sub_const: assumes"g β carrier P" assumes"f β carrier P" assumes"degree f = 0" shows"f of g = f" by (metis lcf_closed assms(1) assms(2) assms(3) sub_to_poly to_poly_inverse)
textβΉSubstitution into a monomialβΊ
lemma monom_sub: assumes"a β carrier R" assumes"g β carrier P" shows"(monom P a n) of g = a β g[^] n" unfolding compose_def using assms UP_pre_univ_prop.eval_monom[of R P to_poly a g n] to_poly_UP_pre_univ_prop unfolding P_def using P.nat_pow_closed P_def to_poly_mult_simp(1) by (simp add: to_poly_mult_simp(1) UP_cring_axioms)
lemma(in UP_cring) cring_sub_monom_bound: assumes"a β carrier R" assumes"a β 0" assumes"f = monom P a n" assumes"g β carrier P" shows"degree (f of g) β€ n*(degree g)" proof- have"f of g = (to_poly a) β (g[^]n)" unfolding compose_def using assms UP_pre_univ_prop.eval_monom[of R P to_poly a g] to_poly_UP_pre_univ_prop unfolding P_def by blast thenshow ?thesis by (smt (verit) P.nat_pow_closed assms(1) assms(4) cring_pow_deg_bound deg_mult_ring
degree_to_poly le_trans plus_nat.add_0 to_poly_closed) qed
lemma(in UP_cring) cring_sub_monom: assumes"a β carrier R" assumes"a β 0" assumes"f = monom P a n" assumes"g β carrier P" assumes"a β (lcf g [^] n) β 0" shows"degree (f of g) = n*(degree g)" proof- have0: "f of g = (to_poly a) β (g[^]n)" unfolding compose_def using assms UP_pre_univ_prop.eval_monom[of R P to_poly a g] to_poly_UP_pre_univ_prop unfolding P_def by blast have1: "lcf (to_poly a) β lcf (g [^] n) β 0" using assms by (smt (verit) P.nat_pow_closed P_def R.nat_pow_closed R.r_null cring_pow_ltrm lcf_closed lcf_ltrm lcf_monom monom_pow to_polynomial_def) thenshow ?thesis using01 assms cring_pow_deg[of g n] cring_deg_mult[of "to_poly a""g[^]n"] by (metis P.nat_pow_closed R.r_null add.right_neutral degree_to_poly to_poly_closed) qed
lemma(in UP_domain) sub_monom: assumes"a β carrier R" assumes"a β 0" assumes"f = monom P a n" assumes"g β carrier P" shows"degree (f of g) = n*(degree g)" proof- have"f of g = (to_poly a) β (g[^]n)" unfolding compose_def using assms UP_pre_univ_prop.eval_monom[of R P to_poly a g] to_poly_UP_pre_univ_prop unfolding P_def by blast thenshow ?thesis using deg_pow deg_mult by (metis P.nat_pow_closed P_def assms(1) assms(2)
assms(4) deg_smult monom_mult_is_smult to_polynomial_def) qed
textβΉSubbing a constant into a polynomial yields a constantβΊ lemma sub_in_const: assumes"g β carrier P" assumes"f β carrier P" assumes"degree g = 0" shows"degree (f of g) = 0" proof- have"β§n. (β§p. p β carrier P ==> degree p β€ n ==> degree (p of g) = 0)" proof- fix n show"β§p. p β carrier P ==> degree p β€ n ==> degree (p of g) = 0" proof(induction n) case0 thenshow ?case by (simp add: assms(1) sub_const) next case (Suc n) fix n assume IH: "β§p. p β carrier P ==> degree p β€ n ==> degree (p of g) = 0" show"β§p. p β carrier P ==> degree p β€ (Suc n) ==> degree (p of g) = 0" proof- fix p assume A0: "p β carrier P" assume A1: "degree p β€ (Suc n)" show"degree (p of g) = 0" proof(cases "degree p < Suc n") case True thenshow ?thesis using IH using A0 by auto next case False thenhave D: "degree p = Suc n" by (simp add: A1 nat_less_le) show ?thesis proof- have P0: "degree ((trunc p) of g) = 0"using IH by (metis A0 D less_Suc_eq_le trunc_degree trunc_closed zero_less_Suc) have P1: "degree ((ltrm p) of g) = 0" proof- obtain a n where an_def: "ltrm p = monom P a n β§ a β carrier R" unfolding leading_term_def using A0 P_def cfs_closed by blast obtain b where b_def: "g = monom P b 0 β§ b β carrier R" using assms deg_zero_impl_monom coeff_closed by blast have0: " monom P b 0 [^] n = monom P (b[^]n) 0" apply(induction n) apply fastforce[1] proof- fix n::nat assume IH: "monom P b 0 [^] n = monom P (b [^] n) 0" have"monom P b 0 [^] Suc n = (monom P (b[^]n) 0) β monom P b 0" using IH by simp thenhave"monom P b 0 [^] Suc n = (monom P ((b[^]n)βb) 0)" using b_def by (simp add: monom_mult_is_smult monom_mult_smult) thenshow"monom P b 0 [^] Suc n = monom P (b [^] Suc n) 0 " by simp qed
thenhave0: "a β monom P b 0 [^] n = monom P (a β b[^]n) 0" by (simp add: an_def b_def monom_mult_smult)
thenshow ?thesis using monom_sub[of a "monom P b 0" n] assms an_def by (simp add: βΉ[a β carrier R; monom P b 0 β carrier P]==> monom P a n of monom P b 0 = a β monom P b 0 [^] nβΊ b_def) qed have P2: "p of g = (trunc p of g) β ((ltrm p) of g)" by (metis A0 assms(1) ltrm_closed sub_add trunc_simps(1) trunc_closed) thenshow ?thesis using P0 P1 P2 deg_add[of "trunc p of g""ltrm p of g"] by (metis A0 assms(1) le_0_eq ltrm_closed max_0R sub_closed trunc_closed) qed qed qed qed qed thenshow ?thesis using assms(2) by blast qed
lemma (in UP_cring) cring_sub_deg_bound: assumes"g β carrier P" assumes"f β carrier P" shows"degree (f of g) β€ degree f * degree g" proof- have"β§n. β§ p. p β carrier P ==> (degree p) β€ n ==> degree (p of g) β€ degree p * degree g" proof- fix n::nat show"β§ p. p β carrier P ==> (degree p) β€ n ==> degree (p of g) β€ degree p * degree g" proof(induction n) case0 thenhave B0: "degree p = 0"by auto thenshow ?caseusing sub_const[of g p] by (simp add: "0.prems"(1) assms(1)) next case (Suc n) fix n assume IH: "(β§p. p β carrier P ==> degree p β€ n ==> degree (p of g) β€ degree p * degree g)" show" p β carrier P ==> degree p β€ Suc n ==> degree (p of g) β€ degree p * degree g" proof- assume A0: "p β carrier P" assume A1: "degree p β€ Suc n" show ?thesis proof(cases "degree p < Suc n") case True thenshow ?thesis using IH by (simp add: A0) next case False thenhave D: "degree p = Suc n" using A1 by auto have P0: "(p of g) = ((trunc p) of g) β ((ltrm p) of g)" by (metis A0 assms(1) ltrm_closed sub_add trunc_simps(1) trunc_closed) have P1: "degree ((trunc p) of g) β€ (degree (trunc p))*(degree g)" using IH by (metis A0 D less_Suc_eq_le trunc_degree trunc_closed zero_less_Suc) have P2: "degree ((ltrm p) of g) β€ (degree p) * degree g" using A0 D P_def UP_cring_axioms assms(1) by (metis False cfs_closed coeff_simp cring_sub_monom_bound deg_zero lcoeff_nonzero2 less_Suc_eq_0_disj) thenshow ?thesis proof(cases "degree g = 0") case True thenshow ?thesis by (simp add: Suc(2) assms(1) sub_in_const) next case F: False thenshow ?thesis proof- have P3: "degree ((trunc p) of g) β€ n*degree g" using A0 False D P1 P2 IH[of "trunc p"] trunc_degree[of p] proof -
{ assume"degree (trunc p) < degree p" thenhave"degree (trunc p) β€ n" using D by auto thenhave ?thesis by (meson P1 le_trans mult_le_cancel2) } thenshow ?thesis by (metis (full_types) A0 D Suc_mult_le_cancel1 nat_mult_le_cancel_disj trunc_degree) qed thenhave P3': "degree ((trunc p) of g) < (degree p)*degree g" using F D by auto have P4: "degree (ltrm p of g) β€ (degree p)*degree g" using cring_sub_monom_bound D P2 by auto thenshow ?thesis using D P0 P1 P3 P4 A0 P3' assms(1) bound_deg_sum less_imp_le_nat
ltrm_closed sub_closed trunc_closed by metis qed qed qed qed qed qed thenshow ?thesis using assms(2) by blast qed
lemma (in UP_cring) cring_sub_deg: assumes"g β carrier P" assumes"f β carrier P" assumes"lcf f β (lcf g [^] (degree f)) β 0" shows"degree (f of g) = degree f * degree g" proof- have0: "f of g = (trunc f of g) β ((ltrm f) of g)" by (metis assms(1) assms(2) ltrm_closed rev_sub_add sub_rev_sub trunc_simps(1) trunc_closed) have1: "lcf f β 0" using assms cring.cring_simprules(26) lcf_closed by auto have2: "degree ((ltrm f) of g) = degree f * degree g" using01 assms cring_sub_monom[of "lcf f""ltrm f""degree f" g] lcf_closed lcf_ltrm by blast show ?thesis apply(cases "degree f = 0") apply (simp add: assms(1) assms(2)) apply(cases "degree g = 0") apply (simp add: assms(1) assms(2) sub_in_const) using01 assms cring_sub_deg_bound[of g "trunc f"] trunc_degree[of f] using sub_const apply auto[1] apply(cases "degree g = 0") using01 assms cring_sub_deg_bound[of g "trunc f"] trunc_degree[of f] using sub_in_const apply fastforce unfolding0using12 by (smt (verit) "0" ltrm_closed βΉ[f β carrier P; 0 < deg R f]==> deg R (Cring_Poly.truncate R f) < deg R fβΊ
assms(1) assms(2) cring_sub_deg_bound degree_of_sum_diff_degree equal_deg_sum
le_eq_less_or_eq mult_less_cancel2 nat_neq_iff neq0_conv sub_closed trunc_closed) qed
lemma (in UP_domain) sub_deg0: assumes"g β carrier P" assumes"f β carrier P" assumes"g β 0" assumes"f β 0" shows"degree (f of g) = degree f * degree g" proof- have"β§n. β§ p. p β carrier P ==> (degree p) β€ n ==> degree (p of g) = degree p * degree g" proof- fix n::nat show"β§ p. p β carrier P ==> (degree p) β€ n ==> degree (p of g) = degree p * degree g" proof(induction n) case0 thenhave B0: "degree p = 0"by auto thenshow ?caseusing sub_const[of g p] by (simp add: "0.prems"(1) assms(1)) next case (Suc n) fix n assume IH: "(β§p. p β carrier P ==> degree p β€ n ==> degree (p of g) = degree p * degree g)" show" p β carrier P ==> degree p β€ Suc n ==> degree (p of g) = degree p * degree g" proof- assume A0: "p β carrier P" assume A1: "degree p β€ Suc n" show ?thesis proof(cases "degree p < Suc n") case True thenshow ?thesis using IH by (simp add: A0) next case False thenhave D: "degree p = Suc n" using A1 by auto have P0: "(p of g) = ((trunc p) of g) β ((ltrm p) of g)" by (metis A0 assms(1) ltrm_closed sub_add trunc_simps(1) trunc_closed) have P1: "degree ((trunc p) of g) = (degree (trunc p))*(degree g)" using IH by (metis A0 D less_Suc_eq_le trunc_degree trunc_closed zero_less_Suc) have P2: "degree ((ltrm p) of g) = (degree p) * degree g" using A0 D P_def UP_domain.sub_monom UP_cring_axioms assms(1) by (metis False UP_domain_axioms UP_ring.coeff_simp UP_ring.lcoeff_nonzero2 UP_ring_axioms cfs_closed deg_nzero_nzero less_Suc_eq_0_disj)
thenshow ?thesis proof(cases "degree g = 0") case True thenshow ?thesis by (simp add: Suc(2) assms(1) sub_in_const) next case False thenshow ?thesis proof- have P3: "degree ((trunc p) of g) < degree ((ltrm p) of g)" using False D P1 P2 by (metis (no_types, lifting) A0 mult.commute mult_right_cancel
nat_less_le nat_mult_le_cancel_disj trunc_degree zero_less_Suc) thenshow ?thesis by (simp add: A0 ltrm_closed P0 P2 assms(1) equal_deg_sum sub_closed trunc_closed) qed qed qed qed qed qed thenshow ?thesis using assms(2) by blast qed
lemma(in UP_domain) sub_deg: assumes"g β carrier P" assumes"f β carrier P" assumes"g β 0" shows"degree (f of g) = degree f * degree g" proof(cases "f = 0") case True thenshow ?thesis using assms(1) sub_const by auto next case False thenshow ?thesis by (simp add: assms(1) assms(2) assms(3) sub_deg0) qed
lemma(in UP_cring) cring_ltrm_sub: assumes"g β carrier P" assumes"f β carrier P" assumes"degree g > 0" assumes"lcf f β (lcf g [^] (degree f)) β 0" shows"ltrm (f of g) = ltrm ((ltrm f) of g)" proof- have P0: "degree (f of g) = degree ((ltrm f) of g)" using assms(1) assms(2) assms(4) cring_sub_deg lcf_eq ltrm_closed deg_ltrm by auto have P1: "f of g = ((trunc f) of g) β((ltrm f) of g)" by (metis assms(1) assms(2) ltrm_closed rev_sub_add sub_rev_sub trunc_simps(1) trunc_closed) thenshow ?thesis proof(cases "degree f = 0") case True thenshow ?thesis using ltrm_deg_0 assms(2) by auto next case False have P2: "degree (f of g) = degree f * degree g" by (simp add: assms(1) assms(2) assms(4) cring_sub_deg) thenhave P3: "degree ((trunc f) of g) < degree ((ltrm f) of g)" using False P0 P1 P_def UP_cring.sub_closed trunc_closed UP_cring_axioms
UP_ring.degree_of_sum_diff_degree UP_ring.ltrm_closed UP_ring_axioms assms(1)
assms(2) assms(4) cring_sub_deg_bound le_antisym less_imp_le_nat less_nat_zero_code
mult_right_le_imp_le nat_neq_iff trunc_degree by (smt (verit) assms(3)) thenshow ?thesis using P0 P1 P2 by (metis (no_types, lifting) ltrm_closed ltrm_of_sum_diff_degree P.add.m_comm assms(1) assms(2) sub_closed trunc_closed) qed qed
lemma(in UP_domain) ltrm_sub: assumes"g β carrier P" assumes"f β carrier P" assumes"degree g > 0" shows"ltrm (f of g) = ltrm ((ltrm f) of g)" proof- have P0: "degree (f of g) = degree ((ltrm f) of g)" using sub_deg by (metis ltrm_closed assms(1) assms(2) assms(3) deg_zero deg_ltrm nat_neq_iff) have P1: "f of g = ((trunc f) of g) β((ltrm f) of g)" by (metis assms(1) assms(2) ltrm_closed rev_sub_add sub_rev_sub trunc_simps(1) trunc_closed) thenshow ?thesis proof(cases "degree f = 0") case True thenshow ?thesis using ltrm_deg_0 assms(2) by auto next case False thenhave P2: "degree ((trunc f) of g) < degree ((ltrm f) of g)" using sub_deg by (metis (no_types, lifting) ltrm_closed assms(1) assms(2) assms(3) deg_zero
deg_ltrm mult_less_cancel2 neq0_conv trunc_closed trunc_degree) thenshow ?thesis using P0 P1 P2 by (metis (no_types, lifting) ltrm_closed ltrm_of_sum_diff_degree P.add.m_comm assms(1) assms(2) sub_closed trunc_closed) qed qed
lemma(in UP_domain) ltrm_of_sub_in_ltrm: assumes"g β carrier P" assumes"f β carrier P" assumes"degree f = n" assumes"degree g > 0" shows"ltrm ((ltrm f) of g) = (lcf f) β ((ltrm g)[^]n)" using assms(1) assms(2) assms(3) lcf_closed ltrm_pow0 ltrm_smult monom_sub by force
textβΉformula for the leading term of a composition βΊ
lemma(in UP_domain) cring_ltrm_of_sub: assumes"g β carrier P" assumes"f β carrier P" assumes"degree f = n" assumes"degree g > 0" assumes"(lcf f) β ((lcf g)[^]n) β 0" shows"ltrm (f of g) = (lcf f) β ((ltrm g)[^]n)" using ltrm_of_sub_in_ltrm ltrm_sub assms(1) assms(2) assms(3) assms(4) by presburger
lemma(in UP_domain) ltrm_of_sub: assumes"g β carrier P" assumes"f β carrier P" assumes"degree f = n" assumes"degree g > 0" shows"ltrm (f of g) = (lcf f) β ((ltrm g)[^]n)" using ltrm_of_sub_in_ltrm ltrm_sub assms(1) assms(2) assms(3) assms(4) by presburger
textβΉsubtitution is associativeβΊ
lemma sub_assoc_monom: assumes"f β carrier P" assumes"q β carrier P" assumes"r β carrier P" shows"(ltrm f) of (q of r) = ((ltrm f) of q) of r" proof- obtain n where n_def: "n = degree f" by simp obtain a where a_def: "a β carrier R β§ (ltrm f) = monom P a n" using assms(1) cfs_closed n_def by blast have LHS: "(ltrm f) of (q of r) = a β (q of r)[^] n" by (metis P.nat_pow_closed P_def UP_pre_univ_prop.eval_monom a_def assms(2)
assms(3) compose_def monom_mult_is_smult sub_closed to_poly_UP_pre_univ_prop to_polynomial_def) have RHS0: "((ltrm f) of q) of r = (a β q[^] n)of r" by (metis P.nat_pow_closed P_def UP_pre_univ_prop.eval_monom a_def
assms(2) compose_def monom_mult_is_smult to_poly_UP_pre_univ_prop to_polynomial_def) have RHS1: "((ltrm f) of q) of r = ((to_poly a) β q[^] n)of r" using RHS0 by (metis P.nat_pow_closed P_def a_def
assms(2) monom_mult_is_smult to_polynomial_def) have RHS2: "((ltrm f) of q) of r = ((to_poly a) of r) β (q[^] n of r)" using RHS1 a_def assms(2) assms(3) sub_mult to_poly_closed by auto have RHS3: "((ltrm f) of q) of r = (to_poly a) β (q[^] n of r)" using RHS2 a_def assms(3) sub_to_poly by auto have RHS4: "((ltrm f) of q) of r = a β ((q[^] n)of r)" using RHS3 by (metis P.nat_pow_closed P_def a_def assms(2) assms(3)
monom_mult_is_smult sub_closed to_polynomial_def) have"(q of r)[^] n = ((q[^] n)of r)" apply(induction n) apply (metis Group.nat_pow_0 P.ring_simprules(6) assms(3) deg_one sub_const) by (simp add: assms(2) assms(3) sub_mult) thenshow ?thesis using RHS4 LHS by simp qed
lemma sub_assoc: assumes"f β carrier P" assumes"q β carrier P" assumes"r β carrier P" shows"f of (q of r) = (f of q) of r" proof- have"β§ n. β§ p. p β carrier P ==> degree p β€ n ==> p of (q of r) = (p of q) of r" proof- fix n show"β§ p. p β carrier P ==> degree p β€ n ==> p of (q of r) = (p of q) of r" proof(induction n) case0 thenhave deg_p: "degree p = 0" by blast thenhave B0: "p of (q of r) = p" using sub_const[of "q of r" p] assms "0.prems"(1) sub_closed by blast have B1: "(p of q) of r = p" proof- have p0: "p of q = p" using deg_p 0 assms(2) by (simp add: P_def UP_cring.sub_const UP_cring_axioms) show ?thesis unfolding p0 using deg_p 0 assms(3) by (simp add: P_def UP_cring.sub_const UP_cring_axioms) qed thenshow"p of (q of r) = (p of q) of r"using B0 B1 by auto next case (Suc n) fix n assume IH: "β§ p. p β carrier P ==> degree p β€ n ==> p of (q of r) = (p of q) of r" thenshow"β§ p. p β carrier P ==> degree p β€ Suc n ==> p of (q of r) = (p of q) of r" proof- fix p assume A0: " p β carrier P " assume A1: "degree p β€ Suc n" show"p of (q of r) = (p of q) of r" proof(cases "degree p < Suc n") case True thenshow ?thesis using A0 A1 IH by auto next case False thenhave"degree p = Suc n" using A1 by auto have I0: "p of (q of r) = ((trunc p) β (ltrm p)) of (q of r)" using A0 trunc_simps(1) by auto have I1: "p of (q of r) = ((trunc p) of (q of r)) β ((ltrm p) of (q of r))" using I0 sub_add by (simp add: A0 assms(2) assms(3) ltrm_closed rev_sub_closed sub_rev_sub trunc_closed) have I2: "p of (q of r) = (((trunc p) of q) of r) β (((ltrm p) of q) of r)" using IH[of "trunc p"] sub_assoc_monom[of p q r] by (metis A0 I1 βΉdegree p = Suc nβΊ assms(2) assms(3)
less_Suc_eq_le trunc_degree trunc_closed zero_less_Suc) have I3: "p of (q of r) = (((trunc p) of q) β ((ltrm p) of q)) of r" using sub_add trunc_simps(1) assms by (simp add: A0 I2 ltrm_closed sub_closed trunc_closed) have I4: "p of (q of r) = (((trunc p)β(ltrm p)) of q) of r" using sub_add trunc_simps(1) assms by (simp add: trunc_simps(1) A0 I3 ltrm_closed trunc_closed) thenshow ?thesis using A0 trunc_simps(1) by auto qed qed qed qed thenshow ?thesis using assms(1) by blast qed
lemma sub_smult: assumes"f β carrier P" assumes"q β carrier P" assumes"a β carrier R" shows"(aβf ) of q = aβ(f of q)" proof- have"(aβf ) of q = ((to_poly a) βf) of q" using assms by (metis P_def monom_mult_is_smult to_polynomial_def) thenhave"(aβf ) of q = ((to_poly a) of q) β(f of q)" by (simp add: assms(1) assms(2) assms(3) sub_mult to_poly_closed) thenhave"(aβf ) of q = (to_poly a) β(f of q)" by (simp add: assms(2) assms(3) sub_to_poly) thenshow ?thesis by (metis P_def assms(1) assms(2) assms(3)
monom_mult_is_smult sub_closed to_polynomial_def) qed
lemma to_fun_sub_monom: assumes"is_UP_monom f" assumes"g β carrier P" assumes"a β carrier R" shows"to_fun (f of g) a = to_fun f (to_fun g a)" proof- obtain b n where b_def: "b β carrier R β§ f = monom P b n" using assms unfolding is_UP_monom_def using P_def cfs_closed by blast thenhave P0: "f of g = b β (g[^]n)" using b_def assms(2) monom_sub by blast have P1: "UP_pre_univ_prop R R (λx. x)" by (simp add: UP_pre_univ_prop_fact) thenhave P2: "to_fun f (to_fun g a) = b β((to_fun g a)[^]n)" using P1 to_fun_eval[of f "to_fun g a"] P_def UP_pre_univ_prop.eval_monom assms(1)
assms(2) assms(3) b_def is_UP_monomE(1) to_fun_closed by force have P3: "to_fun (monom P b n of g) a = b β((to_fun g a)[^]n)" proof- have0: "to_fun (monom P b n of g) a = eval R R (λx. x) a (b β (g[^]n) )"
using UP_pre_univ_prop.eval_monom[of R "(UP R)" to_poly b g n]
P_def assms(2) b_def to_poly_UP_pre_univ_prop to_fun_eval P0 by (metis assms(3) monom_closed sub_closed) have1: "to_fun (monom P b n of g) a = (eval R R (λx. x) a (to_poly b)) β ( eval R R (λx. x) a ( g [^] R n ))" using0 eval_ring_hom by (metis P.nat_pow_closed P0 P_def assms(2) assms(3) b_def monom_mult_is_smult to_fun_eval to_fun_mult to_poly_closed to_polynomial_def) have2: "to_fun (monom P b n of g) a = b β ( eval R R (λx. x) a ( g [^] R n ))" using1 assms(3) b_def to_fun_eval to_fun_to_poly to_poly_closed by auto thenshow ?thesis unfolding to_function_def to_fun_def using eval_ring_hom P_def UP_pre_univ_prop.ring_homD UP_pre_univ_prop_fact
assms(2) assms(3) ring_hom_cring.hom_pow by fastforce qed thenshow ?thesis using b_def P2 by auto qed
lemma to_fun_sub: assumes"g β carrier P" assumes"f β carrier P" assumes"a β carrier R" shows"to_fun (f of g) a = (to_fun f) (to_fun g a)" proof(rule poly_induct2[of f]) show"f β carrier P" using assms by auto show"β§p. p β carrier P ==> degree p = 0 ==> to_fun (p of g) a = to_fun p (to_fun g a)" proof- fix p assume A0: "p β carrier P" assume A1: "degree p = 0" thenhave P0: "degree (p of g) = 0" by (simp add: A0 assms(1) sub_const) thenobtain b where b_def: "p of g = to_poly b β§ b β carrier R" using A0 A1 cfs_closed assms(1) to_poly_inverse by (meson sub_closed) thenhave"to_fun (p of g) a = b" by (simp add: assms(3) to_fun_to_poly) have"p of g = p" using A0 A1 P_def sub_const UP_cring_axioms assms(1) by blast thenhave P1: "p = to_poly b" using b_def by auto have"to_fun g a β carrier R" using assms by (simp add: to_fun_closed) thenshow"to_fun (p of g) a = to_fun p (to_fun g a)" using P1 βΉto_fun (p of g) a = bβΊ b_def by (simp add: to_fun_to_poly) qed show"β§p. 0 < degree p ==> p β carrier P ==> to_fun (trunc p of g) a = to_fun (trunc p) (to_fun g a) ==> to_fun (p of g) a = to_fun p (to_fun g a)" proof- fix p assume A0: "0 < degree p" assume A1: " p β carrier P" assume A2: "to_fun (trunc p of g) a = to_fun (trunc p) (to_fun g a)" show"to_fun (p of g) a = to_fun p (to_fun g a)" proof- have"p of g = (trunc p) of g β (ltrm p) of g" by (metis A1 assms(1) ltrm_closed sub_add trunc_simps(1) trunc_closed) thenhave"to_fun (p of g) a = to_fun ((trunc p) of g) a β (to_fun ((ltrm p) of g) a)" by (simp add: A1 assms(1) assms(3) to_fun_plus ltrm_closed sub_closed trunc_closed) thenhave0: "to_fun (p of g) a = to_fun (trunc p) (to_fun g a) β (to_fun ((ltrm p) of g) a)" by (simp add: A2) have"(to_fun ((ltrm p) of g) a) = to_fun (ltrm p) (to_fun g a)" using to_fun_sub_monom by (simp add: A1 assms(1) assms(3) ltrm_is_UP_monom) thenhave"to_fun (p of g) a = to_fun (trunc p) (to_fun g a) β to_fun (ltrm p) (to_fun g a)" using0by auto thenshow ?thesis by (metis A1 assms(1) assms(3) to_fun_closed to_fun_plus ltrm_closed trunc_simps(1) trunc_closed) qed qed qed end
textβΉMore material on constant terms and constant coefficientsβΊ
context UP_cring begin
lemma to_fun_ctrm: assumes"f β carrier P" assumes"b β carrier R" shows"to_fun (ctrm f) b = (f 0)" using assms by (metis ctrm_degree ctrm_is_poly lcf_monom(2) P_def cfs_closed to_fun_to_poly to_poly_inverse)
lemma to_fun_smult: assumes"f β carrier P" assumes"b β carrier R" assumes"c β carrier R" shows"to_fun (c β f) b = c β(to_fun f b)" proof- have"(c β f) = (to_poly c) β f" by (metis P_def assms(1) assms(3) monom_mult_is_smult to_polynomial_def) thenhave"to_fun (c β f) b = to_fun (to_poly c) b β to_fun f b" by (simp add: assms(1) assms(2) assms(3) to_fun_mult to_poly_closed) thenshow ?thesis by (simp add: assms(2) assms(3) to_fun_to_poly) qed
lemma to_fun_monom: assumes"c β carrier R" assumes"x β carrier R" shows"to_fun (monom P c n) x = c β x [^] n" by (smt (verit) P_def R.m_comm R.nat_pow_closed UP_cring.to_poly_nat_pow UP_cring_axioms assms(1)
assms(2) monom_is_UP_monom(1) sub_monom(1) to_fun_smult to_fun_sub_monom to_fun_to_poly
to_poly_closed to_poly_mult_simp(2))
lemma zcf_monom: assumes"a β carrier R" shows"zcf (monom P a n) = to_fun (monom P a n) 0" using to_fun_monom unfolding zcf_def by (simp add: R.nat_pow_zero assms cfs_monom)
lemma zcf_to_fun: assumes"p β carrier P" shows"zcf p = to_fun p 0" apply(rule poly_induct3[of p]) apply (simp add: assms) using R.zero_closed zcf_add to_fun_plus apply presburger using zcf_monom by blast
lemma zcf_to_poly[simp]: assumes"a β carrier R" shows"zcf (to_poly a) = a" by (metis assms cfs_closed degree_to_poly to_fun_to_poly to_poly_inverse to_poly_closed zcf_def)
lemma zcf_is_ring_hom: "zcfβ ring_hom P R" apply(rule ring_hom_memI) using zcf_mult zcf_add apply (simp add: P_def UP_ring.cfs_closed UP_ring_axioms zcf_def) apply (simp add: zcf_mult) using zcf_add apply auto[1] by simp
lemma ctrm_is_ring_hom: "ctrm β ring_hom P P" apply(rule ring_hom_memI) apply (simp add: ctrm_is_poly) apply (metis zcf_def zcf_mult cfs_closed monom_mult zero_eq_add_iff_both_eq_0) using cfs_add[of _ _ 0] apply (simp add: cfs_closed) by auto
(**************************************************************************************************) (**************************************************************************************************) sectionβΉDescribing the Image of (UP R) in the Ring of Functions from R to RβΊ (**************************************************************************************************) (**************************************************************************************************)
lemma to_fun_diff: assumes"p β carrier P" assumes"q β carrier P" assumes"a β carrier R" shows"to_fun (p β q) a = to_fun p a β to_fun q a" using to_fun_plus[of "β q" p a] by (simp add: P.minus_eq R.minus_eq assms(1) assms(2) assms(3) to_fun_minus)
lemma to_fun_const: assumes"a β carrier R" assumes"b β carrier R" shows"to_fun (monom P a 0) b = a" by (metis lcf_monom(2) P_def UP_cring.to_fun_ctrm UP_cring_axioms assms(1) assms(2) deg_const monom_closed)
lemma to_fun_monic_monom: assumes"b β carrier R" shows"to_fun (monom P 1 n) b = b[^]n" by (simp add: assms to_fun_monom)
textβΉConstant polynomials map to constant polynomialsβΊ
lemma const_to_constant: assumes"a β carrier R" shows"to_fun (monom P a 0) = constant_function (carrier R) a" apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"]) unfolding ring_functions_def apply(simp add: R.ring_axioms) apply (simp add: assms to_fun_is_Fun) using assms ring_functions.constant_function_closed[of R a "carrier R"] unfolding ring_functions_def apply (simp add: R.ring_axioms) using assms to_fun_const[of a ] unfolding constant_function_def by auto
textβΉMonomial polynomials map to monomial functionsβΊ
lemma monom_to_monomial: assumes"a β carrier R" shows"to_fun (monom P a n) = monomial_function R a n" apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"]) unfolding ring_functions_def apply(simp add: R.ring_axioms) apply (simp add: assms to_fun_is_Fun) using assms U_function_ring.monomial_functions[of R a n] R.ring_axioms unfolding U_function_ring_def apply auto[1] unfolding monomial_function_def using assms to_fun_monom[of a _ n] by auto end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉMonic Linear PolynomialsβΊ (**************************************************************************************************) (**************************************************************************************************)
textβΉThe polynomial representing the variable XβΊ
definition X_poly where "X_poly R = monom (UP R) 1 1"
context UP_cring begin
abbreviation(input) X where "X β‘ X_poly R"
lemma X_closed: "X β carrier P" unfolding X_poly_def using P_def monom_closed by blast
lemma degree_X[simp]: assumes"1β 0" shows"degree X = 1" unfolding X_poly_def using assms P_def deg_monom[of 11] by blast
lemma X_not_zero: assumes"1β 0" shows"X β 0" using degree_X assms by force
lemma sub_X[simp]: assumes"p β carrier P" shows"X of p = p" unfolding X_poly_def using P_def UP_pre_univ_prop.eval_monom1 assms compose_def to_poly_UP_pre_univ_prop by metis
lemma sub_monom_deg_one: assumes"p β carrier P" assumes"a β carrier R" shows"monom P a 1 of p = a β p" using assms sub_smult[of X p a] unfolding X_poly_def by (metis P_def R.one_closed R.r_one X_closed X_poly_def monom_mult_smult sub_X)
lemma monom_rep_X_pow: assumes"a β carrier R" shows"monom P a n = aβ(X[^]n)" proof- have"monom P a n = aβmonom P 1 n" by (metis R.one_closed R.r_one assms monom_mult_smult) thenshow ?thesis unfolding X_poly_def using monom_pow by (simp add: P_def) qed
lemma X_sub[simp]: assumes"p β carrier P" shows"p of X = p" apply(rule poly_induct3) apply (simp add: assms) using X_closed sub_add apply presburger using sub_monom[of X] P_def monom_rep_X_pow X_closed by auto
textβΉrepresentation of monomials as scalar multiples of powers of XβΊ
lemma ltrm_rep_X_pow: assumes"p β carrier P" shows"ltrm p = (lcf p)β(X[^](degree p))" proof- have"ltrm p = monom P (lcf p) (degree p)" using assms unfolding leading_term_def by (simp add: P_def) thenshow ?thesis using monom_rep_X_pow P_def assms by (simp add: cfs_closed) qed
lemma to_fun_monom': assumes"c β carrier R" assumes"c β 0" assumes"x β carrier R" shows"to_fun (c β X[^](n::nat)) x = c β x [^] n" using P_def to_fun_monom monom_rep_X_pow UP_cring_axioms assms(1) assms(2) assms(3) by fastforce
lemma to_fun_X_pow: assumes"x β carrier R" shows"to_fun (X[^](n::nat)) x = x [^] n" using to_fun_monom'[of 1 x n] assms by (metis P.nat_pow_closed R.l_one R.nat_pow_closed R.one_closed R.r_null R.r_one
UP_one_closed X_closed to_fun_to_poly ring_hom_one smult_l_null smult_one to_poly_is_ring_hom) end
textβΉMonic linear polynomialsβΊ
definition X_poly_plus where "X_poly_plus R a = (X_poly R) βUP R) to_polynomial R a"
definition X_poly_minus where "X_poly_minus R a = (X_poly R) βUP R) to_polynomial R a"
context UP_cring begin
abbreviation(input) X_plus where "X_plus β‘ X_poly_plus R"
abbreviation(input) X_minus where "X_minus β‘ X_poly_minus R"
lemma X_plus_closed: assumes"a β carrier R" shows"(X_plus a) β carrier P" unfolding X_poly_plus_def using X_closed to_poly_closed using P_def UP_a_closed assms by auto
lemma X_minus_closed: assumes"a β carrier R" shows"(X_minus a) β carrier P" unfolding X_poly_minus_def using X_closed to_poly_closed by (simp add: P_def UP_cring.UP_cring UP_cring_axioms assms cring.cring_simprules(4))
lemma X_minus_plus: assumes"a β carrier R" shows"(X_minus a) = X_plus (βa)" using P_def UP_ring.UP_ring UP_ring_axioms by (simp add: X_poly_minus_def X_poly_plus_def a_minus_def assms to_poly_a_inv)
lemma degree_of_X_plus: assumes"a β carrier R" assumes"1β 0" shows"degree (X_plus a) = 1" proof- have0:"degree (X_plus a) β€ 1" using deg_add degree_X P_def unfolding X_poly_plus_def using UP_cring.to_poly_closed UP_cring_axioms X_closed assms(1) assms(2) by fastforce have1:"degree (X_plus a) > 0" by (metis One_nat_def P_def R.one_closed R.r_zero X_poly_def
X_closed X_poly_plus_def X_plus_closed assms coeff_add coeff_monom deg_aboveD
gr0I lessI n_not_Suc_n to_polynomial_def to_poly_closed) thenshow ?thesis using"0"by linarith qed
lemma degree_of_X_minus: assumes"a β carrier R" assumes"1β 0" shows"degree (X_minus a) = 1" using degree_of_X_plus[of "βa"] X_minus_plus[simp] assms by auto
lemma ltrm_of_X: shows"ltrm X = X" unfolding leading_term_def by (metis P_def R.one_closed X_poly_def is_UP_monom_def is_UP_monomI leading_term_def)
lemma ltrm_of_X_plus: assumes"a β carrier R" assumes"1β 0" shows"ltrm (X_plus a) = X" unfolding X_poly_plus_def using X_closed assms ltrm_of_sum_diff_degree[of X "to_poly a"]
degree_to_poly[of a] to_poly_closed[of a] degree_X ltrm_of_X by (simp add: P_def)
lemma ltrm_of_X_minus: assumes"a β carrier R" assumes"1β 0" shows"ltrm (X_minus a) = X" using X_minus_plus[of a] assms by (simp add: ltrm_of_X_plus)
lemma lcf_of_X_minus: assumes"a β carrier R" assumes"1β 0" shows"lcf (X_minus a) = 1" using ltrm_of_X_minus unfolding X_poly_def using P_def UP_cring.X_minus_closed UP_cring.lcf_eq UP_cring_axioms assms(1) assms(2) lcf_monom by (metis R.one_closed)
lemma lcf_of_X_plus: assumes"a β carrier R" assumes"1β 0" shows"lcf (X_plus a) = 1" using ltrm_of_X_plus unfolding X_poly_def by (metis lcf_of_X_minus P_def UP_cring.lcf_eq UP_cring.X_plus_closed UP_cring_axioms X_minus_closed assms(1) assms(2) degree_of_X_minus)
lemma to_fun_X[simp]: assumes"a β carrier R" shows"to_fun X a = a" using X_closed assms to_fun_sub_monom ltrm_is_UP_monom ltrm_of_X to_poly_closed by (metis sub_X to_fun_to_poly)
lemma to_fun_X_plus[simp]: assumes"a β carrier R" assumes"b β carrier R" shows"to_fun (X_plus a) b = b β a" unfolding X_poly_plus_def using assms to_fun_X[of b] to_fun_plus[of "to_poly a" X b] to_fun_to_poly[of a b] using P_def X_closed to_poly_closed by auto
lemma to_fun_X_minus[simp]: assumes"a β carrier R" assumes"b β carrier R" shows"to_fun (X_minus a) b = b β a" using to_fun_X_plus[of "β a" b] X_minus_plus[of a] assms by (simp add: R.minus_eq)
lemma cfs_X_plus: assumes"a β carrier R" shows"X_plus a n = (if n = 0 then a else (if n = 1 then 1 else 0))" using assms cfs_add monom_closed UP_ring_axioms cfs_monom unfolding X_poly_plus_def to_polynomial_def X_poly_def P_def by auto
lemma cfs_X_minus: assumes"a β carrier R" shows"X_minus a n = (if n = 0 then β a else (if n = 1 then 1 else 0))" using cfs_X_plus[of "β a"] assms unfolding X_poly_plus_def X_poly_minus_def by (simp add: P_def a_minus_def to_poly_a_inv)
lemma X_minus_sub_deg: assumes"a β carrier R" assumes"f β carrier P" shows"degree (f of (X_minus a)) = degree f" using X_plus_sub_deg[of "βa"] assms X_minus_plus[of a] by simp
lemma plus_minus_sub: assumes" a β carrier R" shows"X_plus a of X_minus a = X" unfolding X_poly_plus_def proof- have"(X β to_poly a) of X_minus a = (X of X_minus a) β (to_poly a) of X_minus a" using sub_add by (simp add: X_closed X_minus_closed assms to_poly_closed) thenhave"(X β to_poly a) of X_minus a = (X_minus a) β (to_poly a)" by (simp add: X_minus_closed assms sub_to_poly) thenshow"(X β R to_poly a) of X_minus a = X" unfolding to_polynomial_def X_poly_minus_def by (metis P.add.inv_solve_right P.minus_eq P_def
X_closed X_poly_minus_def X_minus_closed assms monom_closed to_polynomial_def) qed
lemma minus_plus_sub: assumes" a β carrier R" shows"X_minus a of X_plus a = X" using plus_minus_sub[of "βa"] unfolding X_poly_minus_def unfolding X_poly_plus_def using assms apply simp by (metis P_def R.add.inv_closed R.minus_minus a_minus_def to_poly_a_inv)
lemma ltrm_times_X: assumes"p β carrier P" shows"ltrm (X β p) = X β (ltrm p)" using assms ltrm_of_X cring_ltrm_mult[of X p] by (metis ltrm_deg_0 P.r_null R.l_one R.one_closed UP_cring.lcf_monom(1)
UP_cring_axioms X_closed X_poly_def cfs_closed deg_zero deg_ltrm monom_zero)
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉBasic Facts About Taylor ExpansionsβΊ (**************************************************************************************************) (**************************************************************************************************) definition taylor_expansion where "taylor_expansion R a p = compose R p (X_poly_plus R a)"
definition(in UP_cring) taylor where "taylor β‘ taylor_expansion R"
context UP_cring begin
lemma taylor_expansion_ring_hom: assumes"c β carrier R" shows"taylor_expansion R c β ring_hom P P" unfolding taylor_expansion_def using rev_sub_is_hom[of "X_plus c"] unfolding rev_compose_def compose_def using X_plus_closed assms by auto
lemma taylor_deg: assumes"a β carrier R" assumes"p β carrier P" shows"degree (T p) = degree p" unfolding taylor_def taylor_expansion_def using X_plus_sub_deg[of a p] assms by (simp add: taylor_expansion_def)
lemma taylor_id: assumes"a β carrier R" assumes"p β carrier P" shows"p = (T p) of (X_minus a)" unfolding taylor_expansion_def taylor_def using assms sub_assoc[of p "X_plus a""X_minus a"] X_plus_closed[of a] X_minus_closed[of a] by (metis X_sub plus_minus_sub taylor_expansion_def)
lemma taylor_eval: assumes"a β carrier R" assumes"f β carrier P" assumes"b β carrier R" shows"to_fun (T f) b = to_fun f (b β a)" unfolding taylor_expansion_def taylor_def using to_fun_sub[of "(X_plus a)" f b] to_fun_X_plus[of a b]
assms X_plus_closed[of a] by auto
lemma taylor_eval': assumes"a β carrier R" assumes"f β carrier P" assumes"b β carrier R" shows"to_fun f (b) = to_fun (T f) (b β a) " unfolding taylor_expansion_def taylor_def using to_fun_sub[of "(X_minus a)""T f" b] to_fun_X_minus[of b a]
assms X_minus_closed[of a] by (metis taylor_closed taylor_def taylor_id taylor_expansion_def to_fun_X_minus)
lemma(in UP_cring) degree_monom: assumes"a β carrier R" shows"degree (a β R (X_poly R)[^] Rn) = (if a = 0 then 0 else n)" apply(cases "a = 0") apply (metis (full_types) P.nat_pow_closed P_def R.one_closed UP_smult_zero X_poly_def deg_zero monom_closed) using P_def UP_cring.monom_rep_X_pow UP_cring_axioms assms deg_monom by fastforce
lemma(in UP_cring) poly_comp_finsum: assumes"β§i::nat. i β€ n ==> g i β carrier P" assumes"q β carrier P" assumes"p = (β¨ i β {..n}. g i)" shows"p of q = (β¨ i β {..n}. (g i) of q)" proof- have0: "p of q = rev_sub q p" unfolding compose_def rev_compose_def by blast have1: "p of q = finsum P (rev_compose R q β g) {..n}" unfolding0unfolding assms apply(rule ring_hom_finsum[of "rev_compose R q" P "{..n}" g ]) using assms(2) rev_sub_is_hom apply blast apply (simp add: UP_ring) apply simp by (simp add: assms(1)) show ?thesis unfolding1 unfolding comp_apply rev_compose_def compose_def by auto qed
lemma(in UP_cring) poly_comp_expansion: assumes"p β carrier P" assumes"q β carrier P" assumes"degree p β€ n" shows"p of q = (β¨ i β {..n}. (p i) β q[^]i)" proof- obtain g where g_def: "g = (λi. monom P (p i) i)" by blast have0: "β§i. (g i) of q = (p i) β q[^]i" proof- fix i show"g i of q = p i β q [^] i" using assms g_def P_def coeff_simp monom_sub by (simp add: cfs_closed) qed have1: "(β§i. i β€ n ==> g i β carrier P)" using g_def assms by (simp add: cfs_closed) have"(β¨iβ{..n}. monom P (p i) i) = p" using assms up_repr_le[of p n] coeff_simp[of p] unfolding P_def by auto thenhave"p = (β¨ i β {..n}. g i)" using g_def by auto thenhave"p of q = (β¨iβ{..n}. g i of q)" using01 poly_comp_finsum[of n g q p] using assms(2) by blast thenshow ?thesis by(simp add: 0) qed
lemma(in UP_cring) taylor_sum: assumes"p β carrier P" assumes"degree p β€ n" assumes"a β carrier R" shows"p = (β¨ i β {..n}. T p i β (X_minus a)[^]i)" proof- have0: "(T p) of X_minus a = p" using P_def taylor_id assms(1) assms(3) by fastforce have1: "degree (T p) β€ n" using assms by (simp add: taylor_deg) have2: "T p of X_minus a = (β¨iβ{..n}. T p i β X_minus a [^] i)" using1 X_minus_closed[of a] poly_comp_expansion[of "T p""X_minus a" n]
assms taylor_closed by blast thenshow ?thesis using0 by simp qed
textβΉThe $i^{th}$ term in the taylor expansionβΊ definition taylor_term where "taylor_term c p i = (taylor_expansion R c p i) β R (UP_cring.X_minus R c) [^] Ri"
lemma (in UP_cring) taylor_term_closed: assumes"p β carrier P" assumes"a β carrier R" shows"taylor_term a p i β carrier (UP R)" unfolding taylor_term_def using P.nat_pow_closed P_def taylor_closed taylor_def X_minus_closed assms(1) assms(2) smult_closed by (simp add: cfs_closed)
lemma(in UP_cring) taylor_term_sum: assumes"p β carrier P" assumes"degree p β€ n" assumes"a β carrier R" shows"p = (β¨ i β {..n}. taylor_term a p i)" unfolding taylor_term_def taylor_def using assms taylor_sum[of p n a] P_def using taylor_def by auto
lemma (in UP_cring) taylor_expansion_add: assumes"p β carrier P" assumes"q β carrier P" assumes"c β carrier R" shows"taylor_expansion R c (p β R q) = (taylor_expansion R c p) β R (taylor_expansion R c q)" unfolding taylor_expansion_def using assms X_plus_closed[of c] P_def sub_add by blast
lemma (in UP_cring) taylor_term_add: assumes"p β carrier P" assumes"q β carrier P" assumes"a β carrier R" shows"taylor_term a (p β Rq) i = taylor_term a p i β R taylor_term a q i" using assms taylor_expansion_add[of p q a] unfolding taylor_term_def using P.nat_pow_closed P_def taylor_closed X_minus_closed cfs_add smult_l_distr by (simp add: taylor_def cfs_closed)
lemma (in UP_cring) to_fun_taylor_term: assumes"p β carrier P" assumes"a β carrier R" assumes"c β carrier R" shows"to_fun (taylor_term c p i) a = (T p i) β (a β c)[^]i" using assms to_fun_smult[of "X_minus c [^] R i" a "taylor_expansion R c p i"]
to_fun_X_minus[of c a] to_fun_nat_pow[of "X_minus c" a i] unfolding taylor_term_def using P.nat_pow_closed P_def taylor_closed taylor_def X_minus_closed by (simp add: cfs_closed)
end
(**************************************************************************************************) (**************************************************************************************************) subsectionβΉDefining the (Scalar-Valued) Derivative of a Polynomial Using the Taylor ExpansionβΊ (**************************************************************************************************) (**************************************************************************************************) definition derivative where "derivative R f a = (taylor_expansion R a f) 1"
context UP_cring begin
abbreviation(in UP_cring) deriv where "deriv β‘ derivative R"
lemma(in UP_cring) deriv_closed: assumes"f β carrier P" assumes"a β carrier R" shows"(derivative R f a) β carrier R" unfolding derivative_def using taylor_closed taylor_def assms(1) assms(2) cfs_closed by auto
lemma(in UP_cring) deriv_add: assumes"f β carrier P" assumes"g β carrier P" assumes"a β carrier R" shows"deriv (f β g) a = deriv f a β deriv g a" unfolding derivative_def taylor_expansion_def using assms by (simp add: X_plus_closed sub_add sub_closed)
end (**************************************************************************************************) (**************************************************************************************************) sectionβΉThe Polynomial-Valued Derivative OperatorβΊ (**************************************************************************************************) (**************************************************************************************************)
lemma times_X_pow_coeff: assumes"g β carrier P" shows"(monom P 1 k β g) (n + k) = g n" using coeff_monom_mult P.m_closed P_def assms coeff_simp monom_closed by (simp add: cfs_closed)
lemma zcf_eq_zero_unique: assumes"f β carrier P" assumes"g β carrier P β§ (f = X β g)" shows"β§ h. h β carrier P β§ (f = X β h) ==> h = g" proof- fix h assume A: "h β carrier P β§ (f = X β h)" thenhave0: " X β g = X β h" using assms(2) by auto show"h = g" using0 A assms by (metis P_def coeff_simp cfs_times_X up_eqI) qed
lemma poly_shift_id: assumes"f β carrier P" shows"f β ctrm f = X β poly_shift f" using assms poly_shift_eq[of f] poly_shift_closed unfolding a_minus_def by (metis ctrm_is_poly P.add.inv_solve_left P.m_closed UP_a_comm UP_a_inv_closed X_closed)
lemma poly_shift_degree_zero: assumes"p β carrier P" assumes"degree p = 0" shows"poly_shift p = 0" by (metis ltrm_deg_0 P.r_neg P.r_null UP_ring UP_zero_closed X_closed zcf_eq_zero_unique
abelian_group.minus_eq assms(1) assms(2) poly_shift_closed poly_shift_id ring_def)
lemma poly_shift_degree: assumes"p β carrier P" assumes"degree p > 0" shows"degree (poly_shift p) = degree p - 1 " using poly_shift_id[of p] by (metis ctrm_degree ctrm_is_poly P.r_null X_closed add_diff_cancel_right' assms(1) assms(2)
deg_zero degree_of_difference_diff_degree degree_times_X nat_less_le poly_shift_closed)
lemma poly_shift_monom: assumes"a β carrier R" shows"poly_shift (monom P a (Suc k)) = (monom P a k)" proof- have"(monom P a (Suc k)) = ctrm (monom P a (Suc k)) β X βpoly_shift (monom P a (Suc k))" using poly_shift_eq[of "monom P a (Suc k)"] assms monom_closed by blast thenhave"(monom P a (Suc k)) = 0β X βpoly_shift (monom P a (Suc k))" using assms by simp thenhave"(monom P a (Suc k)) = X βpoly_shift (monom P a (Suc k))" using X_closed assms poly_shift_closed by auto thenhave"X β(monom P a k) = X βpoly_shift (monom P a (Suc k))" by (metis P_def R.l_one R.one_closed X_poly_def assms monom_mult plus_1_eq_Suc) thenshow ?thesis using X_closed X_not_zero assms by (meson UP_mult_closed zcf_eq_zero_unique monom_closed poly_shift_closed) qed
lemma(in UP_cring) poly_shift_s_mult: assumes"f β carrier P" assumes"s β carrier R" shows"poly_shift (s βf) = s β (poly_shift f)" proof- have"(s βf) = (ctrm (s βf)) β(X β poly_shift (s βf))" using poly_shift_eq[of "(s βf)"] assms(1) assms(2) by blast thenhave0: "(s βf) = (s β(ctrm f)) β(X β poly_shift (s βf))" using ctrm_smult assms(1) assms(2) by auto have1: "(s βf) = s β ((ctrm f) β (X β (poly_shift f)))" using assms(1) poly_shift_eq by auto have2: "(s βf) = (s β(ctrm f)) β (s β(X β (poly_shift f)))" by (simp add: "1" X_closed assms(1) assms(2) ctrm_is_poly poly_shift_closed smult_r_distr) have3: "(s βf) = (s β(ctrm f)) β (X β (s β(poly_shift f)))" using"2" UP_m_comm X_closed assms(1) assms(2) smult_assoc2 by (simp add: poly_shift_closed) have4: "(X β poly_shift (s βf)) = (X β (s β(poly_shift f)))" using30 X_closed assms(1) assms(2) ctrm_is_poly poly_shift_closed by auto thenshow ?thesis using X_closed X_not_zero assms(1) assms(2) by (metis UP_mult_closed UP_smult_closed zcf_eq_zero_unique poly_shift_closed) qed
lemma zcf_poly_shift: assumes"f β carrier P" shows"zcf (poly_shift f) = f 1" apply(rule poly_induct3) apply (simp add: assms) using poly_shift_add zcf_add cfs_add poly_shift_closed apply metis unfolding zcf_def using poly_shift_monom poly_shift_degree_zero by (simp add: poly_shift_def)
fun poly_shift_iter (βΉshiftβΊ) where
Base:"poly_shift_iter 0 f = f"|
Step:"poly_shift_iter (Suc n) f = poly_shift (poly_shift_iter n f)"
lemma shift_closed: assumes"f β carrier P" shows"shift n f β carrier P" apply(induction n) using assms poly_shift_closed by auto
(**********************************************************************) (**********************************************************************) subsectionβΉOperator Which Multiplies Coefficients by Their DegreeβΊ (**********************************************************************) (**********************************************************************)
definition n_mult where "n_mult f = (λn. [n]β (f n))"
lemma(in UP_cring) n_mult_closed: assumes"f β carrier P" shows"n_mult f β carrier P" apply(rule UP_car_memI[of "deg R f"]) unfolding n_mult_def apply (metis P.l_zero R.add.nat_pow_one UP_zero_closed assms cfs_zero coeff_of_sum_diff_degree0) using assms cfs_closed by auto
textβΉFacts about the shift functionβΊ
lemma shift_one: "shift (Suc 0) = poly_shift" by auto
lemma shift_factor0: assumes"f β carrier P" shows"degree f β₯ (Suc k) ==> degree (f β ((shift (Suc k) f) β(X[^](Suc k)))) < (Suc k)" proof(induction k) case0 have0: " f β (ctrm f) = (shift (Suc 0) f)βX" by (metis UP_m_comm X_closed assms poly_shift_id shift_closed shift_one) thenhave" f β(shift (Suc 0) f)βX = (ctrm f) " proof- have" f β (ctrm f) β (shift (Suc 0) f)βX= (shift (Suc 0) f)βX β (shift (Suc 0) f)βX" using0by simp thenhave" f β (ctrm f) β (shift (Suc 0) f)βX = 0" using UP_cring.UP_cring[of R] assms by (metis "0" P.ring_simprules(4) P_def UP_ring.UP_ring UP_ring_axioms
a_minus_def abelian_group.r_neg ctrm_is_poly ring_def) thenhave" f β ((ctrm f) β (shift (Suc 0) f)βX) = 0" using assms P.ring_simprules by (metis "0" poly_shift_id poly_shift_eq) thenhave" f β ((shift (Suc 0) f)βX β (ctrm f) ) = 0" using P.m_closed UP_a_comm X_closed assms ctrm_is_poly shift_closed by presburger thenhave"f β ((shift (Suc 0) f)βX) β (ctrm f)= 0" using P.add.m_assoc P.ring_simprules(14) P.ring_simprules(19) assms "0"
P.add.inv_closed P.r_neg P.r_zero ctrm_is_poly by (smt (verit, ccfv_threshold)) thenshow ?thesis by (metis "0" P.add.m_comm P.m_closed P.ring_simprules(14) P.ring_simprules(18)
P.ring_simprules(3) X_closed assms ctrm_is_poly poly_shift_id poly_shift_eq
shift_closed) qed thenhave" f β(shift (Suc 0) f)β(X[^](Suc 0)) = (ctrm f) " proof- have"X = X[^](Suc 0)" by (simp add: X_closed) thenshow ?thesis using0βΉf β shift (Suc 0) f β X = ctrm fβΊ by auto qed thenhave" degree (f β(shift (Suc 0) f)β(X[^](Suc 0))) < 1" using ctrm_degree[of f] assms by simp thenshow ?case by blast next case (Suc n) fix k assume IH: "degree f β₯ (Suc k) ==> degree (f β ((shift (Suc k) f) β(X[^](Suc k)))) < (Suc k)" show"degree f β₯ (Suc (Suc k)) ==> degree (f β ((shift (Suc (Suc k)) f) β(X[^](Suc (Suc k))))) < (Suc (Suc k))" proof- obtain n where n_def: "n = Suc k" by simp have IH': "degree f β₯ n ==> degree (f β ((shift n f) β(X[^]n))) < n" using n_def IH by auto have P: "degree f β₯ (Suc n) ==> degree (f β ((shift (Suc n) f) β(X[^](Suc n)))) < (Suc n)" proof- obtain g where g_def: "g = (f β ((shift n f) β(X[^]n)))" by simp obtain s where s_def: "s = shift n f" by simp obtain s' where s'_def: "s' = shift (Suc n) f" by simp have P: "g β carrier P""s β carrier P""s' β carrier P""(X[^]n) β carrier P" using s_def s'_def g_def assms shift_closed[of f n] apply (simp add: X_closed) apply (simp add: βΉf β carrier P ==> shift n f β carrier PβΊ assms s_def) using P_def UP_cring.shift_closed UP_cring_axioms assms s'_defapply blast using X_closed by blast have g_def': "g = (f β (s β(X[^]n)))" using g_def s_def by auto assume"degree f β₯ (Suc n)" thenhave" degree (f β (s β(X[^]n))) < n" using IH' Suc_leD s_def by blast thenhave d_g: "degree g < n"using g_def' by auto have P0: "f β (s' β(X[^](Suc n))) = ((ctrm s)β(X[^]n)) β g" proof- have"s = (ctrm s) β (X β s')" using s_def s'_def P_def poly_shift_eq UP_cring_axioms assms shift_closed by (simp add: UP_cring.poly_shift_eq) thenhave0: "g = f β ((ctrm s) β (X β s')) β(X[^]n)" using g_def' by auto thenhave"g = f β ((ctrm s)β(X[^]n)) β ((X β s') β(X[^]n))" using P cring_axioms X_closed P.l_distr P.ring_simprules(19) UP_a_assoc a_minus_def assms by (simp add: a_minus_def ctrm_is_poly) thenhave"g β ((X β s') β(X[^]n)) = f β ((ctrm s)β(X[^]n))" using P cring_axioms X_closed P.l_distr P.ring_simprules UP_a_assoc a_minus_def assms by (simp add: P.r_neg2 ctrm_is_poly) thenhave" ((ctrm s)β(X[^]n)) = f β (g β ((X β s') β(X[^]n)))" using P cring_axioms X_closed P.ring_simprules UP_a_assoc a_minus_def assms by (simp add: P.ring_simprules(17) ctrm_is_poly) thenhave" ((ctrm s)β(X[^]n)) = f β (((X β s') β(X[^]n)) β g)" by (simp add: P(1) P(3) UP_a_comm X_closed) thenhave"((ctrm s)β(X[^]n)) = f β ((X β s') β(X[^]n)) β g" using P(1) P(3) P.ring_simprules(19) UP_a_assoc a_minus_def assms by (simp add: a_minus_def X_closed) thenhave"((ctrm s)β(X[^]n)) β g= f β ((X β s') β(X[^]n))" by (metis P(1) P(3) P(4) P.add.inv_solve_right P.m_closed P.ring_simprules(14)
P.ring_simprules(4) P_def UP_cring.X_closed UP_cring_axioms assms) thenhave"((ctrm s)β(X[^]n)) β g= f β ((s' β X) β(X[^]n))" by (simp add: P(3) UP_m_comm X_closed) thenhave"((ctrm s)β(X[^]n)) β g= f β (s' β(X[^](Suc n)))" using P(3) P.nat_pow_Suc2 UP_m_assoc X_closed by auto thenshow ?thesis by auto qed have P1: "degree (((ctrm s)β(X[^]n)) β g) β€ n" proof- have Q0: "degree ((ctrm s)β(X[^]n)) β€ n" proof(cases "ctrm s = 0") case True thenshow ?thesis by (simp add: P(4)) next case False thenhave F0: "degree ((ctrm s)β(X[^]n)) β€ degree (ctrm s) + degree (X[^]n) " by (meson ctrm_is_poly P(2) P(4) deg_mult_ring) have F1: "1β 0==> degree (X[^]n) = n" unfolding X_poly_def using P_def cring_monom_degree by auto show ?thesis by (metis (no_types, opaque_lifting) F0 F1 ltrm_deg_0 P(2) P.r_null P_def R.l_null R.l_one
R.nat_pow_closed R.zero_closed X_poly_def assms cfs_closed
add_0 deg_const deg_zero deg_ltrm
monom_pow monom_zero zero_le) qed thenshow ?thesis using d_g by (simp add: P(1) P(2) P(4) bound_deg_sum ctrm_is_poly) qed thenshow ?thesis using s'_def P0 by auto qed assume"degree f β₯ (Suc (Suc k)) " thenshow"degree (f β ((shift (Suc (Suc k)) f) β(X[^](Suc (Suc k))))) < (Suc (Suc k))" using P by(simp add: n_def) qed qed
lemma(in UP_cring) shift_degree0: assumes"f β carrier P" shows"degree f >n ==> Suc (degree (shift (Suc n) f)) = degree (shift n f)" proof(induction n) case0 assume B: "0< degree f" have0: "degree (shift 0 f) = degree f" by simp have1: "degree f = degree (f β (ctrm f))" using assms(1) B ctrm_degree degree_of_difference_diff_degree by (simp add: ctrm_is_poly) have"(f β (ctrm f)) = X β(shift 1 f)" using P_def poly_shift_id UP_cring_axioms assms(1) by auto thenhave"degree (f β (ctrm f)) = 1 + (degree (shift 1 f))" by (metis "1" B P.r_null X_closed add.commute assms deg_nzero_nzero degree_times_X not_gr_zero shift_closed) thenhave"degree (shift 0 f) = 1 + (degree (shift 1 f))" using01by auto thenshow ?case by simp next case (Suc n) fix n assume IH: "(n < degree f ==> Suc (degree (shift (Suc n) f)) = degree (shift n f))" show"Suc n < degree f ==> Suc (degree (shift (Suc (Suc n)) f)) = degree (shift (Suc n) f)" proof- assume A: " Suc n < degree f" thenhave0: "(shift (Suc n) f) = ctrm ((shift (Suc n) f)) β (shift (Suc (Suc n)) f)βX" by (metis UP_m_comm X_closed assms local.Step poly_shift_eq shift_closed) have N: "(shift (Suc (Suc n)) f) β 0" proof assume C: "shift (Suc (Suc n)) f = 0" obtain g where g_def: "g = f β (shift (Suc (Suc n)) f)β(X[^](Suc (Suc n)))" by simp have C0: "degree g < degree f" using g_def assms A by (meson Suc_leI Suc_less_SucD Suc_mono less_trans_Suc shift_factor0) have C1: "g = f" using C by (simp add: P.minus_eq X_closed assms g_def) thenshow False using C0 by auto qed have1: "degree (shift (Suc n) f) = degree ((shift (Suc n) f) β ctrm ((shift (Suc n) f)))" proof(cases "degree (shift (Suc n) f) = 0") case True thenshow ?thesis using N assms poly_shift_degree_zero poly_shift_closed shift_closed by auto next case False thenhave"degree (shift (Suc n) f) > degree (ctrm ((shift (Suc n) f)))" proof - have"shift (Suc n) f β carrier P" using assms shift_closed by blast thenshow ?thesis using False ctrm_degree by auto qed thenshow ?thesis proof - show ?thesis usingβΉdegree (ctrm (shift (Suc n) f)) < degree (shift (Suc n) f)βΊ
assms ctrm_is_poly degree_of_difference_diff_degree shift_closed by presburger qed qed have2: "(shift (Suc n) f) β ctrm ((shift (Suc n) f)) = (shift (Suc (Suc n)) f)βX" using0 by (metis Cring_Poly.INTEG.Step P.m_comm X_closed assms poly_shift_id shift_closed) have3: "degree ((shift (Suc n) f) β ctrm ((shift (Suc n) f))) = degree (shift (Suc (Suc n)) f) + 1" using2 N X_closed X_not_zero assms degree_X shift_closed by (metis UP_m_comm degree_times_X) thenshow ?thesis using1 by linarith qed qed
lemma(in UP_cring) shift_degree: assumes"f β carrier P" shows"degree f β₯ n ==> degree (shift n f) + n = degree f" proof(induction n) case0 thenshow ?case by auto next case (Suc n) fix n assume IH: "(n β€ degree f ==> degree (shift n f) + n = degree f)" show"Suc n β€ degree f ==> degree (shift (Suc n) f) + Suc n = degree f" proof- assume A: "Suc n β€ degree f " have0: "degree (shift n f) + n = degree f" using IH A by auto have1: "degree (shift n f) = Suc (degree (shift (Suc n) f))" using A assms shift_degree0 by auto show"degree (shift (Suc n) f) + Suc n = degree f" using01by simp qed qed
lemma(in UP_cring) shift_degree': assumes"f β carrier P" shows"degree (shift (degree f) f) = 0" using shift_degree assms by fastforce
lemma(in UP_cring) shift_above_degree: assumes"f β carrier P" assumes"k > degree f" shows"(shift k f) = 0" proof- have"β§n. shift ((degree f)+ (Suc n)) f = 0" proof- fix n show"shift ((degree f)+ (Suc n)) f = 0" proof(induction n) case0 have B0:"shift (degree f) f = ctrm(shift (degree f) f) β (shift (degree f + Suc 0) f)βX" proof - have f1: "βf n. f β carrier P β¨ shift n f β carrier P" by (meson shift_closed) thenhave"shift (degree f + Suc 0) f β carrier P" using assms(1) by blast thenshow ?thesis using f1 by (simp add: P.m_comm X_closed assms(1) poly_shift_eq) qed have B1:"shift (degree f) f = ctrm(shift (degree f) f)" proof - have"shift (degree f) f β carrier P" using assms(1) shift_closed by blast thenshow ?thesis using ltrm_deg_0 assms(1) shift_degree' by auto qed have B2: "(shift (degree f + Suc 0) f)βX = 0" using B0 B1 X_closed assms(1) proof - have"βf n. f β carrier P β¨ shift n f β carrier P" using shift_closed by blast thenshow ?thesis by (metis (no_types) B0 B1 P.add.l_cancel_one UP_mult_closed X_closed assms(1)) qed thenshow ?case by (metis P.r_null UP_m_comm UP_zero_closed X_closed assms(1) zcf_eq_zero_unique shift_closed) next case (Suc n) fix n assume"shift (degree f + Suc n) f = 0" thenshow"shift (degree f + Suc (Suc n)) f = 0" by (simp add: poly_shift_degree_zero) qed qed thenshow ?thesis using assms(2) less_iff_Suc_add by auto qed
lemma(in UP_domain) shift_cfs0: assumes"f β carrier P" shows"zcf(shift 1 f) = f 1" using assms by (simp add: zcf_poly_shift)
lemma(in UP_cring) X_mult_cf: assumes"p β carrier P" shows"(p β X) (k+1) = p k" unfolding X_poly_def using assms by (metis UP_m_comm X_closed X_poly_def add.commute plus_1_eq_Suc cfs_times_X)
lemma(in UP_cring) X_pow_cf: assumes"p β carrier P" shows"(p β X[^](n::nat)) (n + k) = p k" proof- have P: "β§f. f β carrier P ==> (f β X[^](n::nat)) (n + k) = f k" proof(induction n) show"β§f. f β carrier P ==> (f β X [^] (0::nat)) (0 + k) = f k" proof- fix f assume B0: "f β carrier P" show"(f β X [^] (0::nat)) (0 + k) = f k" by (simp add: B0) qed fix n fix f assume IH: "(β§f. f β carrier P ==> (f β X [^] n) (n + k) = f k)" assume A0: " f β carrier P" show"(f β X [^] Suc n) (Suc n + k) = f k" proof- have0: "(f β X [^] n)(n + k) = f k" using A0 IH by simp have1: "((f β X [^] n)βX) (Suc n + k) = (f β X [^] n)(n + k)" using X_mult_cf A0 P.m_closed P.nat_pow_closed
Suc_eq_plus1 X_closed add_Suc by presburger have2: "(f β (X [^] n βX)) (Suc n + k) = (f β X [^] n)(n + k)" using1 by (simp add: A0 UP_m_assoc X_closed) thenshow ?thesis by (simp add: "0") qed qed show ?thesis using assms P[of p] by auto qed
lemma poly_shift_cfs: assumes"f β carrier P" shows"poly_shift f n = f (Suc n)" proof- have"(f β ctrm f) (Suc n) = (X β (poly_shift f)) (Suc n)" using assms poly_shift_id by auto thenshow ?thesis unfolding X_poly_def using poly_shift_closed assms by (metis (no_types, lifting) ctrm_degree ctrm_is_poly
P.add.m_comm P.minus_closed coeff_of_sum_diff_degree0 poly_shift_id poly_shift_eq cfs_times_X zero_less_Suc) qed
lemma(in UP_cring) shift_cfs: assumes"p β carrier P" shows"(shift k p) n = p (k + n)" apply(induction k arbitrary: n) by (auto simp: assms poly_shift_cfs shift_closed)
(**********************************************************************) (**********************************************************************) subsectionβΉThe Derivative OperatorβΊ (**********************************************************************) (**********************************************************************) definition pderiv where "pderiv p = poly_shift (n_mult p)"
lemma pderiv_closed: assumes"p β carrier P" shows"pderiv p β carrier P" unfolding pderiv_def using assms n_mult_closed[of p] poly_shift_closed[of "n_mult p"] by blast
textβΉFunction which obtains the first n+1 terms of f, in ascending order of degree:βΊ
definition trms_of_deg_leq where "trms_of_deg_leq n f β‘ f βUP R) ((shift (Suc n) f) β R monom P 1 (Suc n))"
lemma trms_of_deg_leq_closed: assumes"f β carrier P" shows"trms_of_deg_leq n f β carrier P" unfolding trms_of_deg_leq_def using assms by (metis P.m_closed P.minus_closed P_def R.one_closed monom_closed shift_closed)
lemma trms_of_deg_leq_id: assumes"f β carrier P" shows"f β (trms_of_deg_leq k f) = shift (Suc k) f β monom P 1 (Suc k)" unfolding trms_of_deg_leq_def using assms by (smt (verit) P.add.inv_closed P.l_zero P.m_closed P.minus_add P.minus_minus P.r_neg
P_def R.one_closed UP_a_assoc a_minus_def monom_closed shift_closed)
lemma trms_of_deg_leq_id': assumes"f β carrier P" shows"f = (trms_of_deg_leq k f) β shift (Suc k) f β monom P 1 (Suc k)" using trms_of_deg_leq_id assms trms_of_deg_leq_closed[of f] by (smt (verit, ccfv_threshold) P.add.inv_closed P.l_zero P.m_closed P.minus_add P.minus_minus P.r_neg R.one_closed UP_a_assoc a_minus_def monom_closed shift_closed)
lemma deg_leqI: assumes"p β carrier P" assumes"β§n. n > k ==> p n = 0" shows"degree p β€ k" by (metis assms(1) assms(2) deg_zero deg_ltrm le0 le_less_linear monom_zero)
lemma deg_leE: assumes"p β carrier P" assumes"degree p < k" shows"p k = 0" using assms coeff_of_sum_diff_degree0 P_def coeff_simp deg_aboveD by auto
lemma trms_of_deg_leq_deg: assumes"f β carrier P" shows"degree (trms_of_deg_leq k f) β€ k" proof- have"β§n. (trms_of_deg_leq k f) (Suc k + n) = 0" proof- fix n have0: "(shift (Suc k) f β R monom P 1 (Suc k)) (Suc k + n) = shift (Suc k) f n" using assms shift_closed cfs_monom_mult_l by (metis P.m_comm P_def R.one_closed add.commute monom_closed times_X_pow_coeff) thenshow"trms_of_deg_leq k f (Suc k + n) = 0" unfolding trms_of_deg_leq_def using shift_cfs[of f "Suc k" n]
cfs_minus[of f "shift (Suc k) f β R monom P 1 (Suc k)""Suc k + n"] by (metis P.m_closed P.r_neg P_def R.one_closed a_minus_def assms
cfs_minus cfs_zero monom_closed shift_closed) qed thenshow ?thesis using deg_leqI by (metis (no_types, lifting) assms le_iff_add less_Suc_eq_0_disj less_Suc_eq_le trms_of_deg_leq_closed) qed
lemma trms_of_deg_leq_zero_is_ctrm: assumes"f β carrier P" assumes"degree f > 0" shows"trms_of_deg_leq 0 f = ctrm f" proof- have"f = ctrm f β (X β (shift (Suc 0) f))" using assms poly_shift_eq by simp thenhave"f = ctrm f β (X [^] R Suc 0 β (shift (Suc 0) f))" using P.nat_pow_eone P_def X_closed by auto thenshow ?thesis unfolding trms_of_deg_leq_def by (metis (no_types, lifting) ctrm_is_poly One_nat_def P.add.right_cancel P.m_closed
P.minus_closed P.nat_pow_eone P_def UP_m_comm X_closed X_poly_def assms(1) shift_closed
trms_of_deg_leq_def trms_of_deg_leq_id') qed
lemma cfs_monom_mult: assumes"p β carrier P" assumes"a β carrier R" assumes"k < n" shows"(p β (monom P a n)) k = 0" apply(rule poly_induct3[of p]) apply (simp add: assms(1)) apply (metis (no_types, lifting) P.l_distr P.m_closed R.r_zero R.zero_closed assms(2) cfs_add monom_closed) using assms monom_mult[of _ a _ n] by (metis R.m_closed R.m_comm add.commute cfs_monom not_add_less1)
lemma(in UP_cring) cfs_monom_mult_2: assumes"f β carrier P" assumes"a β carrier R" assumes"m < n" shows"((monom P a n) β f) m = 0" using cfs_monom_mult by (simp add: P.m_comm assms(1) assms(2) assms(3))
lemma trms_of_deg_leq_cfs: assumes"f β carrier P" shows"trms_of_deg_leq n f k = (if k β€ n then (f k) else 0)" unfolding trms_of_deg_leq_def apply(cases "k β€ n") using cfs_minus[of f "shift (Suc n) f β R monom P 1 (Suc n)"]
cfs_monom_mult[of _ 1 k "Suc n"] apply (metis (no_types, lifting) P.m_closed P.minus_closed P_def R.one_closed R.r_zero assms
cfs_add cfs_closed le_refl monom_closed nat_less_le nat_neq_iff not_less_eq_eq shift_closed
trms_of_deg_leq_def trms_of_deg_leq_id') using trms_of_deg_leq_deg[of f n] deg_leE unfolding trms_of_deg_leq_def using assms trms_of_deg_leq_closed trms_of_deg_leq_def by auto
lemma trms_of_deg_leq_iter: assumes"f β carrier P" shows"trms_of_deg_leq (Suc k) f = (trms_of_deg_leq k f) β monom P (f (Suc k)) (Suc k)" prooffix x show"trms_of_deg_leq (Suc k) f x = (trms_of_deg_leq k f β monom P (f (Suc k)) (Suc k)) x" apply(cases "x β€ k") using trms_of_deg_leq_cfs trms_of_deg_leq_closed cfs_closed[of f "Suc k"]
cfs_add[of "trms_of_deg_leq k f""monom P (f (Suc k)) (Suc k)" x] apply (simp add: assms) using deg_leE assms cfs_closed cfs_monom apply auto[1] by (simp add: assms cfs_closed cfs_monom trms_of_deg_leq_cfs trms_of_deg_leq_closed) qed
lemma trms_of_deg_leq_degree_f: assumes"f β carrier P" shows"trms_of_deg_leq (degree f) f = f" prooffix x show"trms_of_deg_leq (deg R f) f x = f x" using assms trms_of_deg_leq_cfs deg_leE[of f x] by simp qed
definition(in UP_cring) lin_part where "lin_part f = trms_of_deg_leq 1 f"
lemma(in UP_cring) lin_part_id: assumes"f β carrier P" shows"lin_part f = (ctrm f) β monom P (f 1) 1" unfolding lin_part_def by (simp add: assms trms_of_deg_leq_0 trms_of_deg_leq_iter)
lemma(in UP_cring) lin_part_eq: assumes"f β carrier P" shows"f = lin_part f β (shift 2 f) β monom P 1 2" unfolding lin_part_def by (metis Suc_1 assms trms_of_deg_leq_id')
textβΉConstant term of a substitution:βΊ
lemma zcf_eval: assumes"f β carrier P" shows"zcf f = to_fun f 0" using assms zcf_to_fun by blast
lemma ctrm_of_sub: assumes"f β carrier P" assumes"g β carrier P" shows"zcf(f of g) = to_fun f (zcf g)" apply(rule poly_induct3[of f]) apply (simp add: assms(1)) using P_def UP_cring.to_fun_closed UP_cring_axioms zcf_add zcf_to_fun assms(2) to_fun_plus sub_add sub_closed apply fastforce using R.zero_closed zcf_to_fun assms(2) to_fun_sub monom_closed sub_closed by presburger
lemma(in UP_cring) taylor_deg_1: assumes"f β carrier P" assumes"a β carrier R" shows"f of (X_plus a) = (lin_part (T f)) β (shift (2::nat) (T f))β (X[^](2::nat))" using taylor_eq_1[of f a] unfolding taylor_expansion_def lin_part_def using One_nat_def X_plus_closed assms(1)
assms(2) trms_of_deg_leq_id' numeral_2_eq_2 sub_closed by (metis P.nat_pow_Suc2 P.nat_pow_eone P_def taylor_def X_closed X_poly_def monom_one_Suc taylor_expansion_def)
lemma(in UP_cring) taylor_deg_1_eval: assumes"f β carrier P" assumes"a β carrier R" assumes"b β carrier R" assumes"c = to_fun (shift (2::nat) (T f)) b" assumes"fa = to_fun f a" assumes"f'a = deriv f a" shows"to_fun f (b β a) = fa β (f'a β b) β (c β b[^](2::nat))" using assms taylor_deg_1 unfolding derivative_def proof- have0: "to_fun f (b β a) = to_fun (f of (X_plus a)) b" using to_fun_sub assms X_plus_closed by auto have1: "to_fun (lin_part (T f)) b = fa β (f'a β b) " using assms to_fun_lin_part[of "(T f)" b] by (metis P_def taylor_def UP_cring.taylor_zcf UP_cring.taylor_closed UP_cring_axioms zcf_def derivative_def) have2: "(T f) = (lin_part (T f)) β ((shift 2 (T f))βX[^](2::nat))" using lin_part_eq[of "(Tf)"] assms(1) assms(2) taylor_closed by (metis taylor_def taylor_deg_1 taylor_expansion_def) thenhave"to_fun (Tf) b = fa β (f'a β b) β to_fun ((shift 2 (T f))βX[^](2::nat)) b" using12 by (metis P.nat_pow_closed taylor_closed UP_mult_closed X_closed assms(1) assms(2) assms(3)
to_fun_plus lin_part_def shift_closed trms_of_deg_leq_closed) thenhave"to_fun (Tf) b = fa β (f'a β b) β c β to_fun (X[^](2::nat)) b" by (simp add: taylor_closed X_closed assms(1) assms(2) assms(3) assms(4) to_fun_mult shift_closed) thenhave3: "to_fun f (b β a)= fa β (f'a β b) β c β to_fun (X[^](2::nat)) b" using taylor_eval assms(1) assms(2) assms(3) by auto have"to_fun (X[^](2::nat)) b = b[^](2::nat)" by (metis P.nat_pow_Suc2 P.nat_pow_eone R.nat_pow_Suc2
R.nat_pow_eone Suc_1 to_fun_X
X_closed assms(3) to_fun_mult) thenshow ?thesis using3by auto qed
lemma(in UP_cring) taylor_deg_1_eval': assumes"f β carrier P" assumes"a β carrier R" assumes"b β carrier R" assumes"c = to_fun (shift (2::nat) (T f)) b" assumes"fa = to_fun f a" assumes"f'a = deriv f a" shows"to_fun f (a β b) = fa β (f'a β b) β (c β b[^](2::nat))" using R.add.m_comm taylor_deg_1_eval assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) by auto
lemma(in UP_cring) taylor_deg_1_eval'': assumes"f β carrier P" assumes"a β carrier R" assumes"b β carrier R" assumes"c = to_fun (shift (2::nat) (T f)) (βb)" shows"to_fun f (a β b) = (to_fun f a) β (deriv f a β b) β (c β b[^](2::nat))" proof- have"βb β carrier R" using assms by blast thenhave0: "to_fun f (a β b) = (to_fun f a)β (deriv f a β (βb)) β (c β (βb)[^](2::nat))" unfolding a_minus_def using taylor_deg_1_eval'[of f a "βb" c "(to_fun f a)""deriv f a"] assms by auto have1: "β (deriv f a β b) = (deriv f a β (βb))" using assms by (simp add: R.r_minus deriv_closed) have2: "(c β b[^](2::nat)) = (c β (βb)[^](2::nat))" using assms by (metis R.add.inv_closed R.add.inv_solve_right R.l_zero R.nat_pow_Suc2
R.nat_pow_eone R.zero_closed Suc_1 UP_ring_axioms UP_ring_def
ring.ring_simprules(26) ring.ring_simprules(27)) show ?thesis using012 unfolding a_minus_def by simp qed
lemma(in UP_cring) taylor_deg_1_expansion: assumes"f β carrier P" assumes"a β carrier R" assumes"b β carrier R" assumes"c = to_fun (shift (2::nat) (T f)) (b β a)" assumes"fa = to_fun f a" assumes"f'a = deriv f a" shows"to_fun f (b) = fa β f'a β (b β a) β (c β (b β a)[^](2::nat))" proof- obtain b' where b'_def: "b'= b β a " by simp thenhave b'_def': "b = b' β a" using assms by (metis R.add.inv_solve_right R.minus_closed R.minus_eq) have"to_fun f (b' β a) = fa β (f'a β b') β (c β b'[^](2::nat))" using assms taylor_deg_1_eval[of f a b' c fa f'a] b'_def by blast thenhave"to_fun f (b) = fa β (f'a β b') β (c β b'[^](2::nat))" using b'_def' by auto thenshow"to_fun f (b) = fa β f'a β (b β a) β c β (b β a) [^] (2::nat)" using b'_def by auto qed
lemma(in UP_cring) Taylor_deg_1_expansion': assumes"f β carrier (UP R)" assumes"a β carrier R" assumes"b β carrier R" shows"βc β carrier R. to_fun f (b) = (to_fun f a) β (deriv f a) β (b β a) β (c β (b β a)[^](2::nat))" using taylor_deg_1_expansion[of f a b] assms unfolding P_def by (metis P_def R.minus_closed taylor_closed shift_closed to_fun_closed)
lemma pderiv_deg_0[simp]: assumes"f β carrier P" assumes"degree f = 0" shows"pderiv f = 0" proof- have"degree (n_mult f) = 0" using P_def n_mult_degree_bound assms(1) assms(2) by fastforce thenshow ?thesis unfolding pderiv_def by (simp add: assms(1) n_mult_closed poly_shift_degree_zero) qed
lemma deriv_deg_0: assumes"f β carrier P" assumes"degree f = 0" assumes"a β carrier R" shows"deriv f a = 0" unfolding derivative_def taylor_expansion_def using X_plus_closed assms(1) assms(2) assms(3) deg_leE sub_const by force
lemma poly_shift_monom': assumes"a β carrier R" shows"poly_shift (a β (X[^](Suc n))) = aβ(X[^]n)" using assms monom_rep_X_pow poly_shift_monom by auto
lemma monom_coeff: assumes"a β carrier R" shows"(a β X [^] (n::nat)) k = (if (k = n) then a else 0)" using assms cfs_monom monom_rep_X_pow by auto
lemma cfs_n_mult: assumes"p β carrier P" shows"n_mult p n = [n]β (p n)" by (simp add: n_mult_def)
lemma cfs_add_nat_pow: assumes"p β carrier P" shows"([(n::nat)]β p) k = [n]β (p k)" apply(induction n) by (auto simp: assms)
lemma add_nat_pow_monom: assumes"a β carrier R" shows"[(n::nat)]β monom P a k = monom P ([n]β a) k" apply(rule ext) by (simp add: assms cfs_add_nat_pow cfs_monom)
lemma add_int_pow_monom: assumes"a β carrier R" shows"[(n::int)]β monom P a k = monom P ([n]β a) k" apply(rule ext) by (simp add: assms cfs_add_int_pow cfs_monom)
lemma n_mult_monom: assumes"a β carrier R" shows"n_mult (monom P a (Suc n)) = monom P ([Suc n]β a) (Suc n)" apply(rule ext) unfolding n_mult_def using assms cfs_monom by auto
lemma pderiv_monom: assumes"a β carrier R" shows"pderiv (monom P a n) = monom P ([n]β a) (n-1)" apply(cases "n = 0") apply (simp add: assms) unfolding pderiv_def using assms Suc_diff_1[of n] n_mult_monom[of a "n-1"] poly_shift_monom[of "[Suc (n-1)]β a""Suc (n-1)"] by (metis R.add.nat_pow_closed neq0_conv poly_shift_monom)
lemma pderiv_monom': assumes"a β carrier R" shows"pderiv (a β X[^](n::nat)) = ([n]β a)β X[^](n-1)" using assms pderiv_monom[of a n ] by (simp add: P_def UP_cring.monom_rep_X_pow UP_cring_axioms)
lemma n_mult_add: assumes"p β carrier P" assumes"q β carrier P" shows"n_mult (p β q) = n_mult p β n_mult q" proof(rule ext) fix x show"n_mult (p β q) x = (n_mult p β n_mult q) x" using assms R.add.nat_pow_distrib[of "p x""q x" x] cfs_add[of p q x]
cfs_add[of "n_mult p""n_mult q" x] n_mult_closed unfolding n_mult_def by (simp add: cfs_closed) qed
lemma pderiv_add: assumes"p β carrier P" assumes"q β carrier P" shows"pderiv (p β q) = pderiv p β pderiv q" unfolding pderiv_def using assms poly_shift_add n_mult_add by (simp add: n_mult_closed)
lemma zcf_monom_sub: assumes"p β carrier P" shows"zcf ((monom P 1 (Suc n)) of p) = zcf p [^] (Suc n)" apply(induction n) using One_nat_def P.nat_pow_eone R.nat_pow_eone R.one_closed R.zero_closed zcf_to_fun assms to_fun_closed monom_sub smult_one apply presburger using P_def UP_cring.ctrm_of_sub UP_cring_axioms zcf_to_fun assms to_fun_closed to_fun_monom monom_closed by fastforce
lemma zcf_monom_sub': assumes"p β carrier P" assumes"a β carrier R" shows"zcf ((monom P a (Suc n)) of p) = a β zcf p [^] (Suc n)" using zcf_monom_sub assms P_def R.zero_closed UP_cring.ctrm_of_sub UP_cring.to_fun_monom UP_cring_axioms
zcf_to_fun to_fun_closed monom_closed by fastforce
lemma deriv_monom: assumes"a β carrier R" assumes"b β carrier R" shows"deriv (monom P a n) b = ([n]β a)β(b[^](n-1))" proof(induction n) case0 have0: "b [^] ((0::nat) - 1) β carrier R" using assms by simp thenshow ?caseunfolding derivative_def using assms by (metis R.add.nat_pow_0 R.l_null deg_const deriv_deg_0 derivative_def monom_closed) next case (Suc n) show ?case proof(cases "n = 0") case True have T0: "[Suc n] β a β b [^] (Suc n - 1) = a" by (simp add: True assms(1)) have T1: "(X_poly R β R to_polynomial R b) [^] R Suc n = X_poly R β R to_polynomial R b " using P.nat_pow_eone P_def True UP_a_closed X_closed assms(2) to_poly_closed by auto thenshow ?thesis unfolding derivative_def taylor_expansion_def using T0 T1 True sub_monom(2)[of "X_plus b" a "Suc n"] cfs_add assms unfolding P_def X_poly_plus_def to_polynomial_def X_poly_def by (metis One_nat_def P_def R.add.nat_pow_eone R.nat_pow_0 UP_cring.cfs_X_plus X_plus_closed X_poly_def X_poly_plus_def cfs_smult diff_Suc_1' is_UP_cring n_not_Suc_n to_polynomial_def) next case False have"deriv (monom P a (Suc n)) b = ((monom P a (Suc n)) of (X_plus b)) 1" unfolding derivative_def taylor_expansion_def by auto thenhave"deriv (monom P a (Suc n)) b = (((monom P a n) of (X_plus b)) β (X_plus b)) 1" using monom_mult[of a 1 n 1] sub_mult[of "X_plus b""monom P a n""monom P 1 1" ] X_plus_closed[of b] assms by (metis lcf_monom(1) P.l_one P.nat_pow_eone P_def R.one_closed R.r_one Suc_eq_plus1
deg_one monom_closed monom_one sub_monom(1) to_poly_inverse) thenhave"deriv (monom P a (Suc n)) b = (((monom P a n) of (X_plus b)) β (monom P1 1) β (((monom P a n) of (X_plus b)) β to_poly b)) 1" unfolding X_poly_plus_def by (metis P.r_distr P_def X_closed X_plus_closed X_poly_def X_poly_plus_def assms(1) assms(2) monom_closed sub_closed to_poly_closed) thenhave"deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) 0 β b β ((monom P a n) of (X_plus b)) 1" unfolding X_poly_plus_def by (smt (verit) One_nat_def P.m_closed P_def UP_m_comm X_closed X_plus_closed X_poly_def X_poly_plus_def
assms(1) assms(2) cfs_add cfs_monom_mult_l monom_closed plus_1_eq_Suc sub_closed cfs_times_X to_polynomial_def) thenhave"deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) 0 β b β (deriv (monom P a n) b)" by (simp add: derivative_def taylor_expansion_def) thenhave"deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) 0 β b β ( ([n]β a)β(b[^](n-1)))" by (simp add: Suc) thenhave0: "deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) 0 β ([n]β a)β(b[^]n)" using assms R.m_comm[of b] R.nat_pow_mult[of b "n-1"1] False by (metis (no_types, lifting) R.add.nat_pow_closed R.m_lcomm R.nat_pow_closed R.nat_pow_eone add.commute add_eq_if plus_1_eq_Suc) have1: "((monom P a n) of (X_plus b)) 0 = a β b[^]n" unfolding X_poly_plus_def using zcf_monom_sub' by (smt (verit) ctrm_of_sub One_nat_def P_def R.l_zero R.one_closed UP_cring.zcf_to_poly
UP_cring.f_minus_ctrm UP_cring_axioms X_plus_closed X_poly_def X_poly_plus_def zcf_add
zcf_def assms(1) assms(2) to_fun_monom monom_closed monom_one_Suc2 poly_shift_id poly_shift_monom to_poly_closed) show ?thesis using01 R.add.nat_pow_Suc2 R.add.nat_pow_closed R.l_distr R.nat_pow_closed assms(1) assms(2) diff_Suc_1 by presburger qed qed
lemma deriv_smult: assumes"a β carrier R" assumes"b β carrier R" assumes"g β carrier P" shows"deriv (a β g) b = a β (deriv g b)" unfolding derivative_def taylor_expansion_def using assms sub_smult X_plus_closed cfs_smult by (simp add: sub_closed)
lemma deriv_const: assumes"a β carrier R" assumes"b β carrier R" shows"deriv (monom P a 0) b = 0" unfolding derivative_def using assms taylor_closed taylor_def taylor_deg deg_leE by auto
lemma deriv_monom_deg_one: assumes"a β carrier R" assumes"b β carrier R" shows"deriv (monom P a 1) b = a" unfolding derivative_def taylor_expansion_def using assms cfs_X_plus[of b 1] sub_monom_deg_one X_plus_closed[of b] by simp
lemma monom_Suc: assumes"a β carrier R" shows"monom P a (Suc n) = monom P 1 1 β monom P a n" "monom P a (Suc n) = monom P a n β monom P 1 1" apply (metis R.l_one R.one_closed Suc_eq_plus1_left assms monom_mult) by (metis R.one_closed R.r_one Suc_eq_plus1 assms monom_mult)
lemma(in UP_cring) times_x_product_rule: assumes"f β carrier P" shows"pderiv (f β up_ring.monom P 1 1) = f β pderiv f β up_ring.monom P 1 1" proof(rule poly_induct3[of f]) show"f β carrier P" using assms by blast show"β§p q. q β carrier P ==> p β carrier P ==> pderiv (p β up_ring.monom P 1 1) = p β pderiv p β up_ring.monom P 1 1 ==> pderiv (q β up_ring.monom P 1 1) = q β pderiv q β up_ring.monom P 1 1 ==> pderiv ((p β q) β up_ring.monom P 1 1) = p β q β pderiv (p β q) β up_ring.monom P 1 1" proof- fix p q assume A: "q β carrier P" "p β carrier P" "pderiv (p β up_ring.monom P 1 1) = p β pderiv p β up_ring.monom P 1 1" "pderiv (q β up_ring.monom P 1 1) = q β pderiv q β up_ring.monom P 1 1" have0: "(p β q) β up_ring.monom P 1 1 = (p β up_ring.monom P 1 1) β (q β up_ring.monom P 1 1)" using A assms by (meson R.one_closed UP_l_distr is_UP_monomE(1) is_UP_monomI) have1: "pderiv ((p β q) β up_ring.monom P 1 1) = pderiv (p β up_ring.monom P 1 1)β pderiv (q β up_ring.monom P 1 1)" unfolding0apply(rule pderiv_add) using A is_UP_monomE(1) monom_is_UP_monom(1) apply blast using A is_UP_monomE(1) monom_is_UP_monom(1) by blast have2: "pderiv ((p β q) β up_ring.monom P 1 1) = p β pderiv p β up_ring.monom P 1 1 β (q β pderiv q β up_ring.monom P 1 1)" unfolding1 A by blast have3: "pderiv ((p β q) β up_ring.monom P 1 1) = p β q β (pderiv p β up_ring.monom P 1 1 β pderiv q β up_ring.monom P 1 1)" unfolding2 using A P.add.m_lcomm R.one_closed UP_a_assoc UP_a_closed UP_mult_closed is_UP_monomE(1) monom_is_UP_monom(1) pderiv_closed by presburger have4: "pderiv ((p β q) β up_ring.monom P 1 1) = p β q β ((pderiv p β pderiv q) β up_ring.monom P 1 1)" unfolding3using A P.l_distr R.one_closed is_UP_monomE(1) monom_is_UP_monom(1) pderiv_closed by presburger show5: "pderiv ((p β q) β up_ring.monom P 1 1) = p β q β pderiv (p β q) β up_ring.monom P 1 1" unfolding4using pderiv_add A by presburger qed show"β§a n. a β carrier R ==> pderiv (up_ring.monom P a n β up_ring.monom P 1 1) = up_ring.monom P a n β pderiv (up_ring.monom P a n) β up_ring.monom P 1 1" proof- fix a n assume A: "a β carrier R" have0: "up_ring.monom P a n β up_ring.monom P 1 1 = up_ring.monom P a (Suc n)" using A monom_Suc(2) by presburger have1: "pderiv (up_ring.monom P a n β up_ring.monom P 1 1) = [(Suc n)] β (up_ring.monom P a n)" unfolding0using A add_nat_pow_monom n_mult_monom pderiv_def poly_shift_monom by (simp add: P_def) have2: "pderiv (up_ring.monom P a n β up_ring.monom P 1 1) = (up_ring.monom P a n) β [n] β (up_ring.monom P a n)" unfolding1using A P.add.nat_pow_Suc2 is_UP_monomE(1) monom_is_UP_monom(1) by blast have3: "pderiv (up_ring.monom P a n) β up_ring.monom P 1 1 = [n] β (up_ring.monom P a n)" apply(cases "n = 0") using A add_nat_pow_monom n_mult_monom pderiv_def poly_shift_monom pderiv_deg_0 apply auto[1] using monom_Suc(2)[of a "n-1"] A add_nat_pow_monom n_mult_monom pderiv_def poly_shift_monom by (metis R.add.nat_pow_closed Suc_eq_plus1 add_eq_if monom_Suc(2) pderiv_monom) show"pderiv (up_ring.monom P a n β up_ring.monom P 1 1) = up_ring.monom P a n βpderiv (up_ring.monom P a n) β up_ring.monom P 1 1" unfolding23by blast qed qed
lemma(in UP_cring) deg_one_eval: assumes"g β carrier (UP R)" assumes"deg R g = 1" shows"β§t. t β carrier R ==> to_fun g t = g 0 β (g 1)βt" proof- obtain h where h_def: "h = ltrm g" by blast have0: "deg R (g β R h) = 0" using assms unfolding h_def by (metis ltrm_closed ltrm_eq_imp_deg_drop ltrm_monom P_def UP_car_memE(1) less_one) have1: "g β R h = to_poly (g 0)" proof(rule ext) fix x show"(g β R h) x = to_polynomial R (g 0) x" proof(cases "x = 0") case True have T0: "h 0 = 0" unfolding h_def using assms UP_car_memE(1) cfs_monom by presburger have T1: "(g β R h) 0 = g 0 β h 0" using ltrm_closed P_def assms(1) cfs_minus h_def by blast thenshow ?thesis using T0 assms by (smt (verit) "0" ltrm_closed ltrm_deg_0 P.minus_closed P_def UP_car_memE(1) UP_zero_closed zcf_def zcf_zero deg_zero degree_to_poly h_def to_poly_closed to_poly_inverse to_poly_minus trunc_simps(2) trunc_zero) next case False thenhave"x > 0" by presburger thenshow ?thesis by (metis "0" ltrm_closed P.minus_closed P_def UP_car_memE(1) UP_cring.degree_to_poly UP_cring_axioms assms(1) deg_leE h_def to_poly_closed) qed qed have2: "g = (g β R h) β R h" unfolding h_def using assms by (metis "1" P_def h_def lin_part_def lin_part_id to_polynomial_def trms_of_deg_leq_degree_f) fix t assume A: "t β carrier R" have3: " to_fun g t = to_fun (g β R h) t β to_fun h t" using2 by (metis "1" A P_def UP_car_memE(1) assms(1) h_def monom_closed to_fun_plus to_polynomial_def) thenshow"to_fun g t = g 0 β g 1 β t " unfolding1 h_def using A P_def UP_cring.lin_part_def UP_cring_axioms assms(1) assms(2) to_fun_lin_part trms_of_deg_leq_degree_f by fastforce qed
lemma pderiv_smult: assumes"a β carrier R" assumes"f β carrier P" shows"pderiv (a β f) = a β (pderiv f)" unfolding pderiv_def using assms by (simp add: n_mult_closed nmult_smult poly_shift_s_mult)
lemma(in UP_cring) pderiv_minus: assumes"a β carrier P" assumes"b β carrier P" shows"pderiv (a β b) = pderiv a β pderiv b" proof- have"β b = (β1)βb" using R.one_closed UP_smult_one assms(2) smult_l_minus by presburger thus ?thesis unfolding a_minus_def using pderiv_add assms pderiv_smult by (metis P.add.inv_closed R.add.inv_closed R.one_closed UP_smult_one pderiv_closed smult_l_minus) qed
lemma(in UP_cring) pderiv_const: assumes"b β carrier R" shows"pderiv (up_ring.monom P b 0) = 0" using assms pderiv_monom[of b 0] deg_const is_UP_monomE(1) monom_is_UP_monom(1) pderiv_deg_0 by blast
lemma(in UP_cring) pderiv_minus_const: assumes"a β carrier P" assumes"b β carrier R" shows"pderiv (a β up_ring.monom P b 0) = pderiv a" using pderiv_minus[of a "up_ring.monom P b 0" ] assms pderiv_const[of b] by (smt (verit) P.l_zero P.minus_closed P_def UP_cring.pderiv_const UP_cring.pderiv_minus UP_cring.poly_shift_eq UP_cring_axioms cfs_closed monom_closed pderiv_add pderiv_closed poly_shift_id)
lemma(in UP_cring) monom_product_rule: assumes"f β carrier P" assumes"a β carrier R" shows"pderiv (f β up_ring.monom P a n) = f β pderiv (up_ring.monom P a n) β pderiv f β up_ring.monom P a n" proof- have"βf. f β carrier P βΆ pderiv (f β up_ring.monom P a n) = f β pderiv (up_ring.monom P a n) β pderiv f β up_ring.monom P a n" proof(induction n) case0 show ?case prooffix f show"f β carrier P βΆ pderiv (f β up_ring.monom P a 0) = f β pderiv (up_ring.monom P a 0) β pderiv f β up_ring.monom P a 0 " proofassume A: "f β carrier P" have0: "f β up_ring.monom P a 0 = a βf" using assms A UP_m_comm is_UP_monomE(1) monom_is_UP_monom(1) monom_mult_is_smult by presburger have1: "f β pderiv (up_ring.monom P a 0) = 0" using A assms P.r_null pderiv_const by presburger have2: "pderiv f β up_ring.monom P a 0 = a β pderiv f" using assms A UP_m_comm is_UP_monomE(1) monom_is_UP_monom(1) monom_mult_is_smult pderiv_closed by presburger show"pderiv (f β up_ring.monom P a 0) = f β pderiv (up_ring.monom P a 0) β pderiv f β up_ring.monom P a 0" unfolding012using A UP_l_zero UP_smult_closed assms(2) pderiv_closed pderiv_smult by presburger qed qed next case (Suc n) show"βf. f β carrier P βΆ pderiv (f β up_ring.monom P a (Suc n)) = f β pderiv (up_ring.monom P a (Suc n)) β pderiv f β up_ring.monom P a (Suc n)" prooffix f show"f β carrier P βΆ pderiv (f β up_ring.monom P a (Suc n)) = f β pderiv (up_ring.monom P a (Suc n)) β pderiv f β up_ring.monom P a (Suc n)" proof assume A: "f β carrier P" show" pderiv (f β up_ring.monom P a (Suc n)) = f β pderiv (up_ring.monom P a (Suc n)) β pderiv f β up_ring.monom P a (Suc n)" proof(cases "n = 0") case True have0: "(f β up_ring.monom P a (Suc n)) = a β f β up_ring.monom P 1 1" proof - have"βn. up_ring.monom P a n β carrier P" using assms(2) is_UP_monomE(1) monom_is_UP_monom(1) by presburger thenshow ?thesis by (metis A P.m_assoc P.m_comm R.one_closed True assms(2) is_UP_monomE(1) monom_Suc(2) monom_is_UP_monom(1) monom_mult_is_smult) qed have1: "f β pderiv (up_ring.monom P a (Suc n)) = a β f" using assms True by (metis A One_nat_def P.m_comm R.add.nat_pow_eone diff_Suc_1 is_UP_monomE(1) is_UP_monomI monom_mult_is_smult pderiv_monom) have2: "pderiv f β up_ring.monom P a (Suc n) = a β (pderiv f β up_ring.monom P 11)" using A assms unfolding True by (metis P.m_lcomm R.one_closed UP_mult_closed is_UP_monomE(1) monom_Suc(2) monom_is_UP_monom(1) monom_mult_is_smult pderiv_closed) have3: "a β f β a β (pderiv f β up_ring.monom P 1 1) = a β (f β(pderiv f β up_ring.monom P 1 1))" using assms A P.m_closed R.one_closed is_UP_monomE(1) monom_is_UP_monom(1) pderiv_closed smult_r_distr by presburger show ?thesis unfolding0123 using A times_x_product_rule P.m_closed R.one_closed UP_smult_assoc2 assms(2) is_UP_monomE(1) monom_is_UP_monom(1) pderiv_smult by presburger next case False have IH: "pderiv ((f βup_ring.monom P 1 1) β up_ring.monom P a n) = (f βup_ring.monom P 1 1) β pderiv (up_ring.monom P a n) β pderiv (f βup_ring.monom P 1 1) β up_ring.monom P a n" using Suc A P.m_closed R.one_closed is_UP_monomE(1) is_UP_monomI by presburger have0: "f β up_ring.monom P a (Suc n) = (f βup_ring.monom P 1 1) β up_ring.monom P a n" using A R.one_closed UP_m_assoc assms(2) is_UP_monomE(1) monom_Suc(1) monom_is_UP_monom(1) by presburger have1: "(f βup_ring.monom P 1 1) β pderiv (up_ring.monom P a n) β pderiv (f βup_ring.monom P 1 1) β up_ring.monom P a n = (f βup_ring.monom P 1 1) β pderiv (up_ring.monom P a n) β (f β pderiv f β up_ring.monom P 1 1) β up_ring.monom P a n " using A times_x_product_rule by presburger have2: "(f βup_ring.monom P 1 1) β pderiv (up_ring.monom P a n) =(f βup_ring.monom P ([n]β a) n)" proof- have20: "up_ring.monom P ([n] β a) (n) = up_ring.monom P 1 1 β up_ring.monom P ([n] β a) (n - 1)" using A assms False monom_mult[of 1"[n]β a"1"n-1"] by (metis R.add.nat_pow_closed R.l_one R.one_closed Suc_eq_plus1 add.commute add_eq_if ) show ?thesis unfolding20using assms A False pderiv_monom[of a n] using P.m_assoc R.one_closed is_UP_monomE(1) monom_is_UP_monom(1) by simp qed have3: "(f βup_ring.monom P ([n]β a) n) = [n]β (f βup_ring.monom P a n)" using A assms by (metis P.add_pow_rdistr add_nat_pow_monom is_UP_monomE(1) monom_is_UP_monom(1)) have4: "pderiv (f β up_ring.monom P 1 1) = (f β pderiv f β up_ring.monom P 1 1)" using times_x_product_rule A by blast have5: " (f β pderiv f β up_ring.monom P 1 1) β up_ring.monom P a n = (f β up_ring.monom P a n ) β (pderiv f β up_ring.monom P 1 1 β up_ring.monom P a n )" using A assms by (meson P.l_distr P.m_closed R.one_closed is_UP_monomE(1) is_UP_monomI pderiv_closed) have6: " (f β pderiv f β up_ring.monom P 1 1) β up_ring.monom P a n = (f β up_ring.monom P a n ) β (pderiv f β up_ring.monom P 1 1 β up_ring.monom P a n )" using A assms False 5by blast have7: "(f βup_ring.monom P 1 1) β pderiv (up_ring.monom P a n) β pderiv (f βup_ring.monom P 1 1) β up_ring.monom P a n = [(Suc n)] β (f β up_ring.monom P a n) β pderiv f β up_ring.monom P 1 1 β up_ring.monom P a n" unfolding2356using assms A P.a_assoc by (smt (verit) "1""2""3""6" P.add.nat_pow_Suc P.m_closed R.one_closed is_UP_monomE(1) monom_is_UP_monom(1) pderiv_closed) have8: "pderiv (f β up_ring.monom P a (Suc n)) = pderiv ((f βup_ring.monom P 1 1)β up_ring.monom P a n)" using A assms 0by presburger show" pderiv (f β up_ring.monom P a (Suc n)) = f β pderiv (up_ring.monom P a (Suc n)) β pderiv f β up_ring.monom P a (Suc n)" unfolding8 IH 0123456 by (smt (verit) "2""4""6""7" A P.add_pow_rdistr R.one_closed UP_m_assoc add_nat_pow_monom assms(2) diff_Suc_1 is_UP_monomE(1) is_UP_monomI monom_Suc(1) pderiv_closed pderiv_monom) qed qed qed qed thus ?thesis using assms by blast qed
lemma(in UP_cring) product_rule: assumes"f β carrier (UP R)" assumes"g β carrier (UP R)" shows"pderiv (f β Rg) = (pderiv f β R g) β R (f β R pderiv g)" proof(rule poly_induct3[of f]) show"f β carrier P" using assms unfolding P_def by blast show"β§p q. q β carrier P ==> p β carrier P ==> pderiv (p β R g) = pderiv p β R g β R p β R pderiv g ==> pderiv (q β R g) = pderiv q β R g β R q β R pderiv g ==> pderiv ((p β q) β R g) = pderiv (p β q) β R g β R (p β q) β R pderiv g" proof- fix p q assume A: "q β carrier P""p β carrier P" "pderiv (p β R g) = pderiv p β R g β R p β R pderiv g" "pderiv (q β R g) = pderiv q β R g β R q β R pderiv g" have0: "(p β q) β R g = p β R g β R q β R g" using A assms unfolding P_def using P_def UP_l_distr by blast have1: "pderiv ((p β q) β R g) = pderiv (p β R g) β R pderiv (q β R g)" unfolding0using pderiv_add[of "p β g""q β g"] unfolding P_def using A(1) A(2) P_def UP_mult_closed assms(2) by blast have2: "pderiv ((p β q) β R g) = pderiv p β R g β R p β R pderiv g β R (pderiv q β R g β R q β R pderiv g)" unfolding1 A by blast have3: "pderiv ((p β q) β R g) = pderiv p β R g β R pderiv q β R g β R p β R pderiv g β R q β R pderiv g" using A assms by (metis "1" P.add.m_assoc P.add.m_lcomm P.m_closed P_def pderiv_closed) have4: "pderiv ((p β q) β R g) = (pderiv p β R g β R pderiv q β R g) β R (p β Rpderiv g β R q β R pderiv g)" unfolding3using A assms P_def UP_a_assoc UP_a_closed UP_mult_closed pderiv_closed by auto have5: "pderiv ((p β q) β R g) = ((pderiv p β R pderiv q) β R g) β R ((p β R q)β R pderiv g)" unfolding4using A assms by (metis P.l_distr P_def pderiv_closed) have6: "pderiv ((p β q) β R g) = ((pderiv (p β q)) β R g) β R ((p β R q) β R pderiv g)" unfolding5using A assms by (metis P_def pderiv_add) show"pderiv ((p β q) β R g) = pderiv (p β q) β R g β R (p β q) β R pderiv g" unfolding6using A assms P_def by blast qed show"β§a n. a β carrier R ==> pderiv (up_ring.monom P a n β R g) = pderiv (up_ring.monom P a n) β R g β R up_ring.monom P a n β R pderiv g" using P_def UP_m_comm assms(2) is_UP_monomE(1) monom_is_UP_monom(1) monom_product_rule pderiv_closed by presburger qed
lemma(in UP_cring) chain_rule: assumes"f β carrier P" assumes"g β carrier P" shows"pderiv (compose R f g) = compose R (pderiv f) g β R pderiv g" proof(rule poly_induct3[of f]) show"f β carrier P" using assms by blast show"β§p q. q β carrier P ==> p β carrier P ==> pderiv (Cring_Poly.compose R p g) = Cring_Poly.compose R (pderiv p) g β R pderiv g ==> pderiv (Cring_Poly.compose R q g) = Cring_Poly.compose R (pderiv q) g β R pderiv g ==> pderiv (Cring_Poly.compose R (p β q) g) = Cring_Poly.compose R (pderiv (p β q)) g β R pderiv g" using pderiv_add sub_add by (smt (verit) P_def UP_a_closed UP_m_comm UP_r_distr assms(2) pderiv_closed sub_closed) show"β§a n. a β carrier R ==> pderiv (compose R (up_ring.monom P a n) g) = compose R (pderiv (up_ring.monom P a n)) g β R pderiv g" proof- fix a n assume A: "a β carrier R" show"pderiv (compose R (up_ring.monom P a n) g) = compose R (pderiv (up_ring.monom P a n)) g β R pderiv g" proof(induction n) case0 have00: "(compose R (up_ring.monom P a 0) g) = (up_ring.monom P a 0)" using A P_def assms(2) deg_const is_UP_monom_def monom_is_UP_monom(1) sub_const by presburger have01: "pderiv (up_ring.monom P a 0) = 0" using A pderiv_const by blast show ?caseunfolding0001 by (metis P.l_null P_def UP_zero_closed assms(2) deg_zero pderiv_closed sub_const) next case (Suc n) show"pderiv (Cring_Poly.compose R (up_ring.monom P a (Suc n)) g) = Cring_Poly.compose R (pderiv (up_ring.monom P a (Suc n))) g β R pderiv g" proof(cases "n = 0") case True have0: "compose R (up_ring.monom P a (Suc n)) g = a β g" using A assms sub_monom_deg_one[of g a] unfolding True using One_nat_def by presburger have1: "(pderiv (up_ring.monom P a (Suc n))) = up_ring.monom P a 0" unfolding True proof - have"pderiv (up_ring.monom P a 0) = 0" using A pderiv_const by blast thenshow"pderiv (up_ring.monom P a (Suc 0)) = up_ring.monom P a 0" using A lcf_monom(1) P_def X_closed deg_const deg_nzero_nzero is_UP_monomE(1) monom_Suc(2) monom_is_UP_monom(1) monom_rep_X_pow pderiv_monom poly_shift_degree_zero poly_shift_eq sub_monom(2) sub_monom_deg_one to_poly_inverse to_poly_mult_simp(2) by (metis (no_types, lifting) P.l_null P.r_zero X_poly_def times_x_product_rule) qed thenshow ?thesis unfolding01 using A P_def assms(2) deg_const is_UP_monomE(1) monom_is_UP_monom(1) monom_mult_is_smult pderiv_closed pderiv_smult sub_const by presburger next case False have0: "compose R (up_ring.monom P a (Suc n)) g = (compose R (up_ring.monom P a n) g) β (compose R (up_ring.monom P 1 1) g)" using assms A by (metis R.one_closed monom_Suc(2) monom_closed sub_mult) have1: "compose R (up_ring.monom P a (Suc n)) g = (compose R (up_ring.monom P a n) g) β g" unfolding0using A assms by (metis P_def R.one_closed UP_cring.lcf_monom(1) UP_cring.to_poly_inverse UP_cring_axioms UP_l_one UP_one_closed deg_one monom_one sub_monom_deg_one to_poly_mult_simp(1)) have2: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) = ((pderiv (compose R (up_ring.monom P a n) g)) β g) β ((compose R (up_ring.monom P a n) g) β pderiv g)" unfolding1unfolding P_def apply(rule product_rule) using A assms unfolding P_def using P_def is_UP_monomE(1) is_UP_monomI rev_sub_closed sub_rev_sub apply presburger using assms unfolding P_def by blast have3: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) = (compose R (pderiv (up_ring.monom P a n)) g β R pderiv g β g) β ((compose R (up_ring.monom P a n) g) β pderiv g)" unfolding2 Suc by blast have4: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) = ((compose R (pderiv (up_ring.monom P a n)) g β g) β R pderiv g) β ((compose R (up_ring.monom P a n) g) β pderiv g)" unfolding3using A assms m_assoc m_comm by (smt (verit) P_def monom_closed monom_rep_X_pow pderiv_closed sub_closed) have5: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) = ((compose R (pderiv (up_ring.monom P a n)) g β g) β (compose R (up_ring.monom P a n) g)) β pderiv g" unfolding4using A assms by (metis P.l_distr P.m_closed P_def UP_cring.pderiv_closed UP_cring_axioms monom_closed sub_closed) have6: "compose R (pderiv (up_ring.monom P a n)) g β g = [n]β compose R ((up_ring.monom P a n)) g" proof- have60: "(pderiv (up_ring.monom P a n)) = (up_ring.monom P ([n]β a) (n-1))" using A assms pderiv_monom by blast have61: "compose R (pderiv (up_ring.monom P a n)) g β g = compose R ((up_ring.monom P ([n]β a) (n-1))) g β (compose R (up_ring.monom P 1 1) g)" unfolding60using A assms sub_monom_deg_one[of g 1 ] R.one_closed smult_one by presburger have62: "compose R (pderiv (up_ring.monom P a n)) g β g = compose R (up_ring.monom P ([n]β a) n) g" unfolding61using False A assms sub_mult[of g "up_ring.monom P ([n] β a) (n - 1)""up_ring.monom P 1 1" ] monom_mult[of "[n]β a"1"n-1"1] by (metis Nat.add_0_right R.add.nat_pow_closed R.one_closed R.r_one Suc_eq_plus1 add_eq_if monom_closed) have63: "β§k::nat. Cring_Poly.compose R (up_ring.monom P ([k] β a) n) g = [k] β Cring_Poly.compose R (up_ring.monom P a n) g" proof- fix k::nat show"Cring_Poly.compose R (up_ring.monom P ([k] β a) n) g = [k] β Cring_Poly.compose R (up_ring.monom P a n) g" apply(induction k) using UP_zero_closed assms(2) deg_zero monom_zero sub_const apply (metis A P.add.nat_pow_0 add_nat_pow_monom) proof- fix k::nat assume a: "Cring_Poly.compose R (monom P ([k] β a) n) g = [k] β Cring_Poly.compose R (monom P a n) g" have0: "(monom P ([Suc k] β a) n) = [Suc k] β a β(monom P 1 n)" by (simp add: A monic_monom_smult) have1: "(monom P ([Suc k] β a) n) = [k] β a β(monom P 1 n) βa β(monom P 1 n) " unfolding0 by (simp add: A UP_smult_l_distr) show"Cring_Poly.compose R (monom P ([Suc k] β a) n) g = [Suc k] β (Cring_Poly.compose R (monom P a n) g) " unfolding1 by (simp add: A a assms(2) monic_monom_smult sub_add) qed qed have64: "Cring_Poly.compose R (up_ring.monom P ([n] β a) n) g = [n] β Cring_Poly.compose R (up_ring.monom P a n) g" using63by blast show ?thesis unfolding6264by blast qed have63: "β§k::nat. Cring_Poly.compose R (up_ring.monom P ([k] β a) n) g = [k] β Cring_Poly.compose R (up_ring.monom P a n) g" proof- fix k::nat show"Cring_Poly.compose R (up_ring.monom P ([k] β a) n) g = [k] β Cring_Poly.compose R (up_ring.monom P a n) g" apply(induction k) using UP_zero_closed assms(2) deg_zero monom_zero sub_const apply (metis A P.add.nat_pow_0 add_nat_pow_monom) using A P.add.nat_pow_Suc add_nat_pow_monom assms(2) is_UP_monomE(1) monom_is_UP_monom(1) rev_sub_add sub_rev_sub by (metis P.add.nat_pow_closed) qed have7: "([n] β Cring_Poly.compose R (up_ring.monom P a n) g β Cring_Poly.compose R (up_ring.monom P a n) g) = [Suc n] β (Cring_Poly.compose R (up_ring.monom P a n) g)" using A assms P.add.nat_pow_Suc by presburger have8: "[Suc n] β Cring_Poly.compose R (up_ring.monom P a n) g β pderiv g = Cring_Poly.compose R (up_ring.monom P ([Suc n] β a) n) g β pderiv g" unfolding63[of "Suc n"] by blast show ?thesis unfolding5678using A assms pderiv_monom[of "a""Suc n"] using P_def diff_Suc_1 by metis qed qed qed qed
lemma deriv_prod_rule_times_monom: assumes"a β carrier R" assumes"b β carrier R" assumes"q β carrier P" shows"deriv ((monom P a n) β q) b = (deriv (monom P a n) b) β (to_fun q b) β (to_fun (monom P a n) b) β deriv q b" proof(rule poly_induct3[of q]) show"q β carrier P" using assms by simp show" β§p q. q β carrier P ==> p β carrier P ==> deriv (monom P a n β p) b = deriv (monom P a n) b β to_fun p b β to_fun (monom P a n) b β deriv p b ==> deriv (monom P a n β q) b = deriv (monom P a n) b β to_fun q b β to_fun (monom P a n) b β deriv q b ==> deriv (monom P a n β (p β q)) b = deriv (monom P a n) b β to_fun (p β q) b β to_fun (monom P a n) b β deriv (p β q) b" proof- fix p q assume A: "q β carrier P"" p β carrier P" "deriv (monom P a n β p) b = deriv (monom P a n) b β to_fun p b β to_fun (monom P a n) b β deriv p b" "deriv (monom P a n β q) b = deriv (monom P a n) b β to_fun q b β to_fun (monom P a n) b β deriv q b" have"deriv (monom P a n β (p β q)) b = deriv (monom P a n) b β to_fun p b β to_fun (monom P a n) b β deriv p b βderiv (monom P a n) b β to_fun q b β to_fun (monom P a n) b β deriv q b" using A assms by (simp add: P.r_distr R.add.m_assoc deriv_add deriv_closed to_fun_closed) hence"deriv (monom P a n β (p β q)) b = deriv (monom P a n) b β to_fun p b βderiv (monom P a n) b β to_fun q b β to_fun (monom P a n) b β deriv p b β to_fun (monom P a n) b β deriv q b" using A(1) A(2) R.add.m_assoc R.add.m_comm assms(1) assms(2) deriv_closed to_fun_closed by auto hence"deriv (monom P a n β (p β q)) b = deriv (monom P a n) b β (to_fun p b βto_fun q b) β to_fun (monom P a n) b β (deriv p b β deriv q b)" by (simp add: A(1) A(2) R.add.m_assoc R.r_distr assms(1) assms(2) deriv_closed to_fun_closed) thus"deriv (monom P a n β (p β q)) b = deriv (monom P a n) b β to_fun (p β q) b β to_fun (monom P a n) b β deriv (p β q) b" by (simp add: A(1) A(2) assms(2) deriv_add to_fun_plus) qed show"β§c m. c β carrier R ==> deriv (monom P a n β monom P c m) b = deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) b β deriv (monom P c m) b" proof- fix c m assume A: "c β carrier R" show"deriv (monom P a n β monom P c m) b = deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) b β deriv (monom P c m) b" proof(cases "n = 0") case True have LHS: "deriv (monom P a n β monom P c m) b = deriv (monom P (a β c) m) b" by (metis A True add.left_neutral assms(1) monom_mult) have RHS: "deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) bβ deriv (monom P c m) b = a β deriv (monom P c m) b " using deriv_const to_fun_monom A True assms(1) assms(2) deriv_closed by auto show ?thesis using A assms LHS RHS deriv_monom by (smt (verit) R.add.nat_pow_closed R.add_pow_rdistr R.m_assoc R.m_closed R.nat_pow_closed) next case False show ?thesis proof(cases "m = 0") case True have LHS: "deriv (monom P a n β monom P c m) b = deriv (monom P (a β c) n) b" by (metis A True add.comm_neutral assms(1) monom_mult) have RHS: "deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) bβ deriv (monom P c m) b = c β deriv (monom P a n) b " by (metis (no_types, lifting) A lcf_monom(1) P_def R.m_closed R.m_comm R.r_null
R.r_zero True UP_cring.to_fun_ctrm UP_cring_axioms assms(1) assms(2) deg_const
deriv_closed deriv_const to_fun_closed monom_closed) show ?thesis using LHS RHS deriv_monom A assms by (smt (verit) R.add.nat_pow_closed R.add_pow_ldistr R.m_assoc R.m_closed R.m_comm R.nat_pow_closed) next case F: False have pos: "n > 0""m >0" using F False by auto have RHS: "deriv (monom P a n β monom P c m) b = [(n + m)] β (a β c) β b [^] (n + m - 1)" using deriv_monom[of "a β c" b "n + m"] monom_mult[of a c n m] by (simp add: A assms(1) assms(2)) have LHS: "deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) b β deriv (monom P c m) b = [n]β a β(b[^](n-1)) β c β b[^]m β a β b[^]n β [m]β c β(b[^](m-1))" using deriv_monom[of a b n] to_fun_monom[of a b n]
deriv_monom[of c b m] to_fun_monom[of c b m] A assms by (simp add: R.m_assoc) have0: "[n]β a β (b[^](n-1)) β c β b[^]m = [n]β a β c β b[^](n + m -1) " proof- have"[n]β a β (b[^](n-1)) β c β b[^]m = [n]β a β c β (b[^](n-1)) β b[^]m" by (simp add: A R.m_lcomm R.semiring_axioms assms(1) assms(2) semiring.semiring_simprules(8)) hence"[n]β a β (b[^](n-1)) β c β b[^]m = [n]β a β c β ((b[^](n-1)) β b[^]m)" by (simp add: A R.m_assoc assms(1) assms(2)) thus ?thesis by (simp add: False R.nat_pow_mult add_eq_if assms(2)) qed have1: "a β b[^]n β [m]β c β(b[^](m-1)) = a β [m]β c β b[^](n + m -1)" proof- have"a β b[^]n β [m]β c β(b[^](m-1)) = a β [m]β c β b[^]n β(b[^](m-1))" using A R.m_comm R.m_lcomm assms(1) assms(2) by auto hence"a β b[^]n β [m]β c β(b[^](m-1)) = a β [m]β c β (b[^]n β(b[^](m-1)))" by (simp add: A R.m_assoc assms(1) assms(2)) thus ?thesis by (simp add: F R.nat_pow_mult add.commute add_eq_if assms(2)) qed have LHS: "deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) b β deriv (monom P c m) b = [n]β a β c β b[^](n + m -1) β a β [m]β c β b[^](n + m -1)" using LHS 01 by simp hence LHS: "deriv (monom P a n) b β to_fun (monom P c m) b β to_fun (monom P a n) b β deriv (monom P c m) b = [n]β (a β c β b[^](n + m -1)) β [m]β (a β c β b[^](n + m -1))" by (simp add: A R.add_pow_ldistr R.add_pow_rdistr assms(1) assms(2)) show ?thesis using LHS RHS by (simp add: A R.add.nat_pow_mult R.add_pow_ldistr assms(1) assms(2)) qed qed qed qed
lemma deriv_prod_rule: assumes"p β carrier P" assumes"q β carrier P" assumes"a β carrier R" shows"deriv (p β q) a = deriv p a β (to_fun q a) β (to_fun p a) β deriv q a" proof(rule poly_induct3[of p]) show"p β carrier P" using assms(1) by simp show" β§p qa. qa β carrier P ==> p β carrier P ==> deriv (p β q) a = deriv p a β to_fun q a β to_fun p a β deriv q a ==> deriv (qa β q) a = deriv qa a β to_fun q a β to_fun qa a β deriv q a ==> deriv ((p β qa) β q) a = deriv (p β qa) a β to_fun q a β to_fun (p β qa) a β deriv q a" proof- fix f g assume A: "f β carrier P""g β carrier P" "deriv (f β q) a = deriv f a β to_fun q a β to_fun f a β deriv q a" "deriv (g β q) a = deriv g a β to_fun q a β to_fun g a β deriv q a" have"deriv ((f β g) β q) a = deriv f a β to_fun q a β to_fun f a β deriv q a β deriv g a β to_fun q a β to_fun g a β deriv q a" using A deriv_add by (simp add: P.l_distr R.add.m_assoc assms(2) assms(3) deriv_closed to_fun_closed) hence"deriv ((f β g) β q) a = deriv f a β to_fun q a β deriv g a β to_fun q a β to_fun f a β deriv q a β to_fun g a β deriv q a" using R.a_comm R.a_assoc deriv_closed to_fun_closed assms by (simp add: A(1) A(2)) hence"deriv ((f β g) β q) a = (deriv f a β to_fun q a β deriv g a β to_fun q a) β (to_fun f a β deriv q a β to_fun g a β deriv q a)" by (simp add: A(1) A(2) R.add.m_assoc assms(2) assms(3) deriv_closed to_fun_closed) thus"deriv ((f β g) β q) a = deriv (f β g) a β to_fun q a β to_fun (f β g) a β deriv q a" by (simp add: A(1) A(2) R.l_distr assms(2) assms(3) deriv_add deriv_closed to_fun_closed to_fun_plus) qed show"β§aa n. aa β carrier R ==> deriv (monom P aa n β q) a = deriv (monom P aa n) a β to_fun q a β to_fun (monom P aa n) a β deriv q a" using deriv_prod_rule_times_monom by (simp add: assms(2) assms(3)) qed
lemma pderiv_eval_deriv_monom: assumes"a β carrier R" assumes"b β carrier R" shows"to_fun (pderiv (monom P a n)) b = deriv (monom P a n) b" using deriv_monom assms pderiv_monom by (simp add: P_def UP_cring.to_fun_monom UP_cring_axioms)
lemma pderiv_eval_deriv: assumes"f β carrier P" assumes"a β carrier R" shows"deriv f a = to_fun (pderiv f) a" apply(rule poly_induct3[of f]) apply (simp add: assms(1)) using assms(2) deriv_add to_fun_plus pderiv_add pderiv_closed apply presburger using assms(2) pderiv_eval_deriv_monom by presburger
textβΉTaking taylor expansions commutes with taking derivatives:βΊ
lemma(in UP_cring) taylor_expansion_pderiv_comm: assumes"f β carrier (UP R)" assumes"c β carrier R" shows"pderiv (taylor_expansion R c f) = taylor_expansion R c (pderiv f)" apply(rule poly_induct3[of f]) using assms unfolding P_def apply blast proof- fix p q assume A: " q β carrier (UP R)""p β carrier (UP R)" "pderiv (taylor_expansion R c p) = taylor_expansion R c (pderiv p)" "pderiv (taylor_expansion R c q) = taylor_expansion R c (pderiv q)" have0: " pderiv (taylor_expansion R c (p β R q)) = pderiv (taylor_expansion R c p β R taylor_expansion R c q)" using A P_def taylor_expansion_add assms(2) by presburger show"pderiv (taylor_expansion R c (p β R q)) = taylor_expansion R c (pderiv (p β R q))" unfolding0 using A(1) A(2) A(3) A(4) taylor_def UP_cring.taylor_closed UP_cring.taylor_expansion_add UP_cring.pderiv_add UP_cring.pderiv_closed UP_cring_axioms assms(2) by fastforce next fix a n assume A: "a β carrier R" show"pderiv (taylor_expansion R c (up_ring.monom (UP R) a n)) = taylor_expansion R c (pderiv (up_ring.monom (UP R) a n))" proof(cases "n = 0") case True have0: "deg R (taylor_expansion R c (up_ring.monom (UP R) a n)) = 0" unfolding True using P_def A assms taylor_def taylor_deg deg_const is_UP_monomE(1) monom_is_UP_monom(2) by presburger have1: "(pderiv (up_ring.monom (UP R) a n)) = 0" unfolding True using P_def A assms pderiv_const by blast show ?thesis unfolding1using0 A assms P_def by (metis P.add.right_cancel taylor_closed taylor_def taylor_expansion_add UP_l_zero UP_zero_closed monom_closed pderiv_deg_0) next case False have0: "pderiv (up_ring.monom (UP R) a n) = (up_ring.monom (UP R) ([n]β a) (n-1))" using A by (simp add: UP_cring.pderiv_monom UP_cring_axioms) have1: "pderiv (taylor_expansion R c (up_ring.monom (UP R) a n)) = (Cring_Poly.compose R (up_ring.monom (UP R) ([n]β a) (n-1)) (X_plus c)) β pderiv (X_plus c)" using chain_rule[of "up_ring.monom (UP R) a n""X_plus c"] unfolding0 taylor_expansion_def using A P_def X_plus_closed assms(2) is_UP_monom_def monom_is_UP_monom(1) by presburger have2: "pderiv (X_plus c) = 1" using pderiv_add[of "X_poly R""to_poly c"] P.l_null P.l_one P.r_zero P_def R.one_closed X_closed
X_poly_def X_poly_plus_def assms(2) monom_one pderiv_const to_poly_closed to_polynomial_def by (metis times_x_product_rule) show ?thesis unfolding102 taylor_expansion_def by (metis "1""2" A P.l_one P_def R.add.nat_pow_closed UP_m_comm UP_one_closed X_plus_closed assms(2) monom_closed sub_closed taylor_expansion_def) qed qed
(**********************************************************************) (**********************************************************************) subsectionβΉLinear SubstitutionsβΊ (**********************************************************************) (**********************************************************************) lemma(in UP_ring) lcoeff_Lcf: assumes"f β carrier P" shows"lcoeff f = lcf f" unfolding P_def using assms coeff_simp[of f] by metis
lemma(in UP_cring) linear_sub_cfs: assumes"f β carrier (UP R)" assumes"d β carrier R" assumes"g = compose R f (up_ring.monom (UP R) d 1)" shows"g i = d[^]i β f i" proof- have0: "(up_ring.monom (UP R) d 1) β carrier (UP R)" using assms by (meson R.ring_axioms UP_ring.intro UP_ring.monom_closed) have1: "(βi. compose R f (up_ring.monom (UP R) d 1) i = d[^]i β f i)" apply(rule poly_induct3[of f]) using assms unfolding P_def apply blast proof- show"β§p q. q β carrier (UP R) ==> p β carrier (UP R) ==> βi. Cring_Poly.compose R p (up_ring.monom (UP R) d 1) i = d [^] i β p i ==> βi. Cring_Poly.compose R q (up_ring.monom (UP R) d 1) i = d [^] i β q i ==> βi. Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = d [^] i β (p β R q) i" proof fix p q i assume A: "q β carrier (UP R)" "p β carrier (UP R)" "βi. Cring_Poly.compose R p (up_ring.monom (UP R) d 1) i = d [^] i β p i" "βi. Cring_Poly.compose R q (up_ring.monom (UP R) d 1) i = d [^] i β q i" show"Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = d [^] i β (p β R q) i" proof- have1: "Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) = Cring_Poly.compose R p (up_ring.monom (UP R) d 1) β R Cring_Poly.compose R q (up_ring.monom (UP R) d 1)" using A(1) A(2) sub_add[of "up_ring.monom (UP R) d 1" q p] unfolding P_def using"0" P_def sub_add by blast have2: "Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = Cring_Poly.compose R p (up_ring.monom (UP R) d 1) i β Cring_Poly.compose R q (up_ring.monom (UP R) d 1) i" using1by (metis (no_types, lifting) "0" A(1) A(2) P_def cfs_add sub_closed) have3: "Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = d [^] i β p i β d [^] i β q i" unfolding2using A by presburger have4: "Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = d [^] i β (p i β q i)" using"3" A(1) A(2) R.nat_pow_closed R.r_distr UP_car_memE(1) assms(2) by presburger thus"Cring_Poly.compose R (p β R q) (up_ring.monom (UP R) d 1) i = d [^] i β (p β R q) i" unfolding4using A(1) A(2) P_def cfs_add by presburger qed qed show"β§a n. a β carrier R ==> βi. Cring_Poly.compose R (up_ring.monom (UP R) a n) (up_ring.monom (UP R) d 1) i = d [^] i β up_ring.monom (UP R) a n i" prooffix a n i assume A: "a β carrier R" have0: "Cring_Poly.compose R (up_ring.monom (UP R) a n) (up_ring.monom (UP R) d 1) = a β R(up_ring.monom (UP R) d 1)[^] Rn" using assms A 0 P_def monom_sub by blast have1: "Cring_Poly.compose R (up_ring.monom (UP R) a n) (up_ring.monom (UP R) d 1) = a β R (d[^]n β R(up_ring.monom (UP R) 1 n))" unfolding0using A assms by (metis P_def R.nat_pow_closed monic_monom_smult monom_pow mult.left_neutral) have2: "Cring_Poly.compose R (up_ring.monom (UP R) a n) (up_ring.monom (UP R) d 1) = (a βd[^]n)β R(up_ring.monom (UP R) 1 n)" unfolding1using A assms by (metis R.nat_pow_closed R.one_closed R.ring_axioms UP_ring.UP_smult_assoc1 UP_ring.intro UP_ring.monom_closed) show"Cring_Poly.compose R (up_ring.monom (UP R) a n) (up_ring.monom (UP R) d 1) i = d [^] i β up_ring.monom (UP R) a n i" apply(cases "i = n") unfolding2using A P_def R.m_closed R.m_comm R.nat_pow_closed assms(2) cfs_monom monic_monom_smult apply presburger using A P_def R.m_closed R.nat_pow_closed R.r_null assms(2) cfs_monom monic_monom_smult by presburger qed qed show ?thesis using1unfolding assms by blast qed
lemma(in UP_cring) linear_sub_deriv: assumes"f β carrier (UP R)" assumes"d β carrier R" assumes"g = compose R f (up_ring.monom (UP R) d 1)" assumes"c β carrier R" shows"pderiv g = d β R compose R (pderiv f) (up_ring.monom (UP R) d 1)" unfolding assms proof(rule poly_induct3[of f]) show"f β carrier P" using assms unfolding P_def by blast show"β§ p q. q β carrier P ==> p β carrier P ==> pderiv (Cring_Poly.compose R p (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv p) (up_ring.monom (UP R) d 1) ==> pderiv (Cring_Poly.compose R q (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv q) (up_ring.monom (UP R) d 1) ==> pderiv (Cring_Poly.compose R (p β q) (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv (p β q)) (up_ring.monom (UP R) d 1)" proof- fix p q assume A: "q β carrier P""p β carrier P" "pderiv (Cring_Poly.compose R p (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv p) (up_ring.monom (UP R) d 1)" "pderiv (Cring_Poly.compose R q (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv q) (up_ring.monom (UP R) d 1)" show" pderiv (Cring_Poly.compose R (p β q) (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv (p β q)) (up_ring.monom (UP R) d 1)" using A assms P_def monom_closed pderiv_add pderiv_closed smult_r_distr sub_add sub_closed by force qed show"β§a n. a β carrier R ==> pderiv (Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv (up_ring.monom P a n)) (up_ring.monom (UP R) d 1)" proof- fix a n assume A: "a β carrier R" have"(Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = aβ R (up_ring.monom P d 1)[^] R n" using A assms sub_monom(2) P_def is_UP_monomE(1) monom_is_UP_monom(1) by blast hence0: "(Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = a β R (up_ring.monom P (d[^]n) n)" using A assms P_def monom_pow nat_mult_1 by metis show"pderiv (Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = d β R Cring_Poly.compose R (pderiv (up_ring.monom P a n)) (up_ring.monom (UP R) d 1)" proof(cases "n = 0") case True have T0: "pderiv (up_ring.monom P a n) = 0UP R"unfolding True using A P_def pderiv_const by blast have T1: "(Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = up_ring.monom P a n" unfolding True using A assms P_def deg_const is_UP_monomE(1) monom_is_UP_monom(1) sub_const by presburger thus ?thesis unfolding T0 T1 by (metis P.nat_pow_eone P_def UP_smult_closed UP_zero_closed X_closed assms(2) deg_zero monom_rep_X_pow smult_r_null sub_const) next case False have F0: "pderiv (Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = (a β R (up_ring.monom P ([n]β (d[^]n))(n-1)))" using A assms pderiv_monom unfolding0 using P_def R.nat_pow_closed is_UP_monomE(1) monom_is_UP_monom(1) pderiv_smult by metis have F1: "(pderiv (up_ring.monom P a n)) = up_ring.monom P ([n] β a) (n - 1)" using A assms pderiv_monom[of a n] by blast hence F2: "(pderiv (up_ring.monom P a n)) = ([n] β a) β Rup_ring.monom P 1 (n - 1)" using A P_def monic_monom_smult by auto have F3: "Cring_Poly.compose R ((([n] β a) β R (up_ring.monom P 1 (n - 1)))) (up_ring.monom (UP R) d 1) = ([n] β a) β R ((up_ring.monom (UP R) d 1)[^] R(n-1))" using A F1 F2 P_def assms(2) monom_closed sub_monom(2) by fastforce have F4: "Cring_Poly.compose R ((([n] β a) β R (up_ring.monom P 1 (n - 1)))) (up_ring.monom (UP R) d 1) = ([n] β a) β R ((up_ring.monom (UP R) (d[^](n-1)) (n-1)))" by (metis F3 P_def assms(2) monom_pow nat_mult_1) have F5: "d β R (Cring_Poly.compose R (pderiv (up_ring.monom P a n)) (up_ring.monom (UP R) d 1)) = (d β([n] β a)) β R up_ring.monom (UP R) (d [^] (n - 1)) (n - 1)" unfolding F4 F2 using A P_def assms(2) monom_closed smult_assoc1 by auto have F6: "d β R (Cring_Poly.compose R (pderiv (up_ring.monom P a n)) (up_ring.monom (UP R) d 1)) = (d β d[^](n-1) β[n] β a) β R ((up_ring.monom (UP R) 1 (n-1)))" unfolding F5 using False A assms P_def R.m_assoc R.m_closed R.m_comm R.nat_pow_closed monic_monom_smult monom_mult_smult by (smt (verit) R.add.nat_pow_closed) have F7: "pderiv (Cring_Poly.compose R (up_ring.monom P a n) (up_ring.monom (UP R) d 1)) = (a β ([n]β (d[^]n)) β R (up_ring.monom P 1 (n-1)))" unfolding F0 using A assms P_def R.m_closed R.nat_pow_closed monic_monom_smult monom_mult_smult by simp have F8: "a β [n] β (d [^] n) = d β d [^] (n - 1) β [n] β a" proof- have F80: "d β d [^] (n - 1) β [n] β a = d [^] n β [n] β a" using A assms False by (metis R.nat_pow_Suc2 add.right_neutral add_eq_if) show ?thesis unfolding F80 using A R.add_pow_rdistr R.m_comm R.nat_pow_closed assms(2) by presburger qed show ?thesis unfolding F6 F7 unfolding F8 P_def by blast qed qed qed
lemma(in UP_cring) linear_sub_deriv': assumes"f β carrier (UP R)" assumes"d β carrier R" assumes"g = compose R f (up_ring.monom (UP R) d 1)" assumes"c β carrier R" shows"pderiv g = compose R (d β R pderiv f) (up_ring.monom (UP R) d 1)" using assms linear_sub_deriv[of f d g c] P_def is_UP_monomE(1) is_UP_monomI pderiv_closed sub_smult by metis
lemma(in UP_cring) linear_sub_inv: assumes"f β carrier (UP R)" assumes"d β Units R" assumes"g = compose R f (up_ring.monom (UP R) d 1)" shows"compose R g (up_ring.monom (UP R) (inv d) 1) = f" unfolding assms prooffix x have0: "Cring_Poly.compose R (Cring_Poly.compose R f (up_ring.monom (UP R) d 1)) (up_ring.monom (UP R) (inv d) 1) x = (inv d)[^]x β ((Cring_Poly.compose R f (up_ring.monom (UP R) d 1)) x)" apply(rule linear_sub_cfs) using P_def R.Units_closed assms(1) assms(2) monom_closed sub_closed apply auto[1] apply (simp add: assms(2)) by blast show"Cring_Poly.compose R (Cring_Poly.compose R f (up_ring.monom (UP R) d 1)) (up_ring.monom (UP R) (inv d) 1) x = f x " unfolding0using linear_sub_cfs[of f d "Cring_Poly.compose R f (up_ring.monom (UP R) d 1)" x]
assms by (smt (verit) R.Units_closed R.Units_inv_closed R.Units_l_inv R.m_assoc R.m_comm R.nat_pow_closed R.nat_pow_distrib R.nat_pow_one R.r_one UP_car_memE(1)) qed
lemma(in UP_cring) linear_sub_deg: assumes"f β carrier (UP R)" assumes"d β Units R" assumes"g = compose R f (up_ring.monom (UP R) d 1)" shows"deg R g = deg R f" proof(cases "deg R f = 0") case True show ?thesis using assms unfolding True assms using P_def True monom_closed by (simp add: R.Units_closed sub_const) next case False have0: "monom (UP R) d 1 (deg R (monom (UP R) d 1)) = d" using assms lcf_monom(2) by blast have1: "d[^](deg R f) β Units R" using assms(2) by (metis Group.comm_monoid.axioms(1) R.units_comm_group R.units_of_pow comm_group_def monoid.nat_pow_closed units_of_carrier) have2: "f (deg R f) β 0" using assms False P_def UP_cring.ltrm_rep_X_pow UP_cring_axioms deg_ltrm degree_monom byfastforce have"deg R g = deg R f * deg R (up_ring.monom (UP R) d 1)" unfolding assms apply(rule cring_sub_deg[of "up_ring.monom (UP R) d 1" f] ) using assms P_def monom_closed apply blast unfolding P_def apply(rule assms) unfolding0using21 by (metis R.Units_closed R.Units_l_cancel R.m_comm R.r_null R.zero_closed UP_car_memE(1) assms(1)) thus ?thesis using assms unfolding assms by (metis (no_types, lifting) P_def R.Units_closed deg_monom deg_zero is_UP_monomE(1) linear_sub_inv monom_is_UP_monom(2) monom_zero mult.right_neutral mult_0_right sub_closed sub_const) qed
end
(**************************************************************************************************) (**************************************************************************************************) sectionβΉLemmas About Polynomial DivisionβΊ (**************************************************************************************************) (**************************************************************************************************) context UP_cring begin
(**********************************************************************) (**********************************************************************) subsectionβΉDivision by Linear TermsβΊ (**********************************************************************) (**********************************************************************) definition UP_root_div where "UP_root_div f a = (poly_shift (T f)) of (X_minus a)"
definition UP_root_rem where "UP_root_rem f a = ctrm (T f)"
lemma UP_root_div_closed: assumes"f β carrier P" assumes"a β carrier R" shows"UP_root_div f a β carrier P" using assms unfolding UP_root_div_def by (simp add: taylor_closed X_minus_closed poly_shift_closed sub_closed)
lemma rem_closed: assumes"f β carrier P" assumes"a β carrier R" shows"UP_root_rem f a β carrier P" using assms unfolding UP_root_rem_def by (simp add: taylor_closed ctrm_is_poly)
lemma rem_deg: assumes"f β carrier P" assumes"a β carrier R" shows"degree (UP_root_rem f a) = 0" by (simp add: taylor_closed assms(1) assms(2) ctrm_degree UP_root_rem_def)
lemma remainder_theorem: assumes"f β carrier P" assumes"a β carrier R" assumes"g = UP_root_div f a" assumes"r = UP_root_rem f a" shows"f = r β (X_minus a) β g" proof- have"Tf = (ctrm (Tf)) β X β poly_shift (Tf)" using poly_shift_eq[of "Tf"] assms taylor_closed by blast hence1: "Tf of (X_minus a) = (ctrm (Tf)) β (X_minus a) β (poly_shift (Tf) of (X_minus a))" using assms taylor_closed[of f a] X_minus_closed[of a] X_closed
sub_add[of "X_minus a""ctrm (Tf)""X β poly_shift (Tf)"]
sub_const[of "X_minus a"] sub_mult[of "X_minus a" X "poly_shift (Tf)"]
ctrm_degree ctrm_is_poly P.m_closed poly_shift_closed sub_X by presburger have2: "f = (ctrm (Tf)) β (X_minus a) β (poly_shift (Tf) of (X_minus a))" using1 taylor_id[of a f] assms by simp thenshow ?thesis using assms unfolding UP_root_div_def UP_root_rem_def by auto qed
lemma remainder_theorem': assumes"f β carrier P" assumes"a β carrier R" shows"f = UP_root_rem f a β (X_minus a) β UP_root_div f a" using assms remainder_theorem by auto
lemma factor_theorem: assumes"f β carrier P" assumes"a β carrier R" assumes"g = UP_root_div f a" assumes"to_fun f a = 0" shows"f = (X_minus a) β g" using remainder_theorem[of f a g _] assms unfolding UP_root_rem_def by (simp add: ctrm_zcf taylor_zcf taylor_closed UP_root_div_closed X_minus_closed)
lemma factor_theorem': assumes"f β carrier P" assumes"a β carrier R" assumes"to_fun f a = 0" shows"f = (X_minus a) β UP_root_div f a" by (simp add: assms(1) assms(2) assms(3) factor_theorem)
(**********************************************************************) (**********************************************************************) subsectionβΉGeometric SumsβΊ (**********************************************************************) (**********************************************************************) lemma geom_quot: assumes"a β carrier R" assumes"b β carrier R" assumes"p = monom P 1 (Suc n) β monom P (b[^](Suc n)) 0 " assumes"g = UP_root_div p b" shows"a[^](Suc n) β b[^] (Suc n) = (a β b) β (to_fun g a)" proof- have root: "to_fun p b = 0" using assms to_fun_const[of "b[^](Suc n)" b] to_fun_monic_monom[of b "Suc n"] R.nat_pow_closed[of b "Suc n"]
to_fun_diff[of "monom P 1 (Suc n)""monom P (b[^](Suc n)) 0" b] monom_closed by (metis P.minus_closed P_def R.one_closed R.zero_closed UP_cring.f_minus_ctrm
UP_cring.to_fun_diff UP_cring_axioms zcf_to_fun cfs_monom to_fun_const) have LHS: "to_fun p a = a[^](Suc n) β b[^] (Suc n)" using assms to_fun_const to_fun_monic_monom to_fun_diff by auto have RHS: "to_fun ((X_minus b) β g) a = (a β b) β (to_fun g a)" using to_fun_mult[of g "X_minus b"] assms X_minus_closed by (metis P.minus_closed P_def R.nat_pow_closed R.one_closed UP_cring.UP_root_div_closed UP_cring_axioms to_fun_X_minus monom_closed) show ?thesis using RHS LHS root factor_theorem' assms(2) assms(3) assms(4) by auto qed
end
context UP_cring begin
definition geometric_series where "geometric_series n a b = to_fun (UP_root_div (monom P 1 (Suc n) β R (monom P (b[^](Suc n)) 0)) b) a"
lemma geometric_series_id: assumes"a β carrier R" assumes"b β carrier R" shows"a[^](Suc n) βb[^] (Suc n) = (a β b) β (geometric_series n a b)" using assms geom_quot by (simp add: P_def geometric_series_def)
lemma geometric_series_closed: assumes"a β carrier R" assumes"b β carrier R" shows"(geometric_series n a b) β carrier R" unfolding geometric_series_def using assms P.minus_closed P_def UP_root_div_closed to_fun_closed monom_closed by auto
textβΉShows that $a^n - b^n$ has $a - b$ as a factor:βΊ lemma to_fun_monic_monom_diff: assumes"a β carrier R" assumes"b β carrier R" shows"βc. c β carrier R β§ to_fun (monom P 1 n) a β to_fun (monom P 1 n) b = (a β b) β c" proof(cases "n = 0") case True have"to_fun (monom P 1 0) a β to_fun (monom P 1 0) b = (a β b) β0" unfolding a_minus_def using to_fun_const[of 1] assms by (simp add: R.r_neg) thenshow ?thesis using True by blast next case False thenshow ?thesis using Suc_diff_1[of n] geometric_series_id[of a b "n-1"] geometric_series_closed[of a b "n-1"]
assms(1) assms(2) to_fun_monic_monom by auto qed
lemma to_fun_diff_factor: assumes"a β carrier R" assumes"b β carrier R" assumes"f β carrier P" shows"βc. c β carrier R β§(to_fun f a) β (to_fun f b) = (a β b)βc" proof(rule poly_induct5[of f]) show"f β carrier P"using assms by simp show"β§p q. q β carrier P ==> p β carrier P ==> βc. c β carrier R β§ to_fun p a β to_fun p b = (a β b) β c ==> βc. c β carrier R β§ to_fun q a β to_fun q b = (a β b) β c ==> βc. c β carrier R β§ to_fun (p β q) a β to_fun (p β q) b = (a β b) β c" proof- fix p q assume A: "q β carrier P""p β carrier P" "βc. c β carrier R β§ to_fun p a β to_fun p b = (a β b) β c" "βc. c β carrier R β§ to_fun q a β to_fun q b = (a β b) β c" obtain c where c_def: "c β carrier R β§ to_fun p a β to_fun p b = (a β b) β c" using A by blast obtain c' where c'_def: "c' β carrier R β§ to_fun q a β to_fun q b = (a β b) β c'" using A by blast have0: "(a β b) β c β (a β b) β c' = (a β b)β(c β c')" using assms c_def c'_defunfolding a_minus_def by (simp add: R.r_distr R.r_minus) have1: "to_fun (p βq) a β to_fun (p β q) b = to_fun p a β to_fun q a β to_fun p bβ to_fun q b" using A to_fun_plus[of p q a] to_fun_plus[of p q b] assms to_fun_closed
R.ring_simprules(19)[of "to_fun p b""to_fun q b"] by (simp add: R.add.m_assoc R.minus_eq to_fun_plus) hence"to_fun (p βq) a β to_fun (p β q) b = to_fun p a β to_fun p b β to_fun q a β to_fun q b" using0 A assms R.ring_simprules to_fun_closed a_assoc a_comm unfolding a_minus_def by (smt (verit, del_insts)) hence"to_fun (p βq) a β to_fun (p β q) b = to_fun p a β to_fun p b β (to_fun q aβ to_fun q b)" using0 A assms R.ring_simprules to_fun_closed unfolding a_minus_def by metis hence"to_fun (p βq) a β to_fun (p β q) b = (a β b)β(c β c')" using0 A c_def c'_def by simp thus"βc. c β carrier R β§ to_fun (p β q) a β to_fun (p β q) b = (a β b) β c" using R.add.m_closed c'_def c_def by blast qed show"β§n. βc. c β carrier R β§ to_fun (monom P 1 n) a β to_fun (monom P 1 n) b = (a β b) β c" by (simp add: assms(1) assms(2) to_fun_monic_monom_diff) show"β§p aa. aa β carrier R ==> p β carrier P ==>βc. c β carrier R β§ to_fun p a β to_fun p b = (a β b) β c ==>βc. c β carrier R β§ to_fun (aa β p) a β to_fun (aa β p) b = (a β b) β c" proof- fix p c assume A: "c β carrier R"" p β carrier P" "βe. e β carrier R β§ to_fun p a β to_fun p b = (a β b) β e" thenobtain d where d_def: "d β carrier R β§ to_fun p a β to_fun p b = (a β b) β d" by blast have"to_fun (c β p) a β to_fun (c β p) b = c β (to_fun p a β to_fun p b)" using A d_def assms to_fun_smult[of p a c] to_fun_smult[of p b c]
to_fun_closed[of p a] to_fun_closed[of p b] R.ring_simprules by presburger hence"cβd β carrier R β§ to_fun (c β p) a β to_fun (c β p) b = (a β b) β (c βd)" by (simp add: A(1) R.m_lcomm assms(1) assms(2) d_def) thus"βe. e β carrier R β§ to_fun (c β p) a β to_fun (c β p) b = (a β b) β e" by blast qed qed
textβΉAny finite set over a domain is the zero set of a polynomial:βΊ lemma(in UP_domain) fin_set_poly_roots: assumes"F β carrier R" assumes"finite F" shows"β P β carrier (UP R). β x β carrier R. to_fun P x = 0β· x β F" apply(rule finite.induct) apply (simp add: assms(2)) proof- show"βPβcarrier (UP R). βxβcarrier R. (to_fun P x = 0) = (x β {})" proof- have"βxβcarrier R. (to_fun (1 R) x = 0) = (x β {})" proof fix x assume A: "x β carrier R" thenhave"(to_fun (1 R)) x = 1" by (metis P_def R.one_closed UP_cring.to_fun_to_poly UP_cring_axioms ring_hom_one to_poly_is_ring_hom) thenshow"(to_fun 1 R x = 0) = (x β {})" by simp qed thenshow ?thesis using P_def UP_one_closed by blast qed show"β§A a. finite A ==> βPβcarrier (UP R). βxβcarrier R. (to_fun P x = 0) = (x β A) ==>βPβcarrier (UP R). βxβcarrier R. (to_fun P x = 0) = (x β insert a A)" proof- fix A :: "'a set"fix a assume fin_A: "finite A" assume IH: "βPβcarrier (UP R). βxβcarrier R. (to_fun P x = 0) = (x β A)" thenobtain p where p_def: "p βcarrier (UP R) β§ (βxβcarrier R. (to_fun p x = 0) = (x β A))" by blast show"βPβcarrier (UP R). βxβcarrier R. (to_fun P x = 0) = (x β insert a A)" proof(cases "a β carrier R") case True obtain Q where Q_def: "Q = p β R (X β R to_poly a)" by blast have"βxβcarrier R. (to_fun Q x = 0) = (x β insert a A)" prooffix x assume P: "x β carrier R" have P0: "to_fun (X β R to_poly a) x = x β a" using to_fun_plus[of X "β R to_poly a" x] True P unfolding a_minus_def by (metis X_poly_minus_def a_minus_def to_fun_X_minus) thenhave"to_fun Q x = (to_fun p x) β (x β a)" proof- have0: " p β carrier P" by (simp add: P_def p_def) have1: " X β R to_poly a β carrier P" using P.minus_closed P_def True X_closed to_poly_closed by auto have2: "x β carrier R" by (simp add: P) thenshow ?thesis using to_fun_mult[of p "(X β R to_poly a)" x] P0 012 Q_def True P_def to_fun_mult by auto qed thenshow"(to_fun Q x = 0) = (x β insert a A)" using p_def by (metis P R.add.inv_closed R.integral_iff R.l_neg R.minus_closed R.minus_unique True UP_cring.to_fun_closed UP_cring_axioms a_minus_def insert_iff) qed thenhave"Q β carrier (UP R) β§ (βxβcarrier R. (to_fun Q x = 0) = (x β insert a A))" using P.minus_closed P_def Q_def True UP_mult_closed X_closed p_def to_poly_closed by auto thenshow ?thesis by blast next case False thenshow ?thesis using IH subsetD by auto qed qed qed
(**********************************************************************) (**********************************************************************) subsectionβΉPolynomial Evaluation at Multiplicative InversesβΊ (**********************************************************************) (**********************************************************************) textβΉFor every polynomial $p(x)$ of degree $n$, there is a unique polynomial $q(x)$ which satisfies the equation $q(x) = x^n p(1/x)$. This section defines this polynomial and proves this identity.βΊ definition(in UP_cring) one_over_poly where "one_over_poly p = (λ n. if n β€ degree p then p ((degree p) - n) else 0)"
lemma(in UP_cring) one_over_poly_closed: assumes"p β carrier P" shows"one_over_poly p β carrier P" apply(rule UP_car_memI[of "degree p" ]) unfolding one_over_poly_def using assms apply simp by (simp add: assms cfs_closed)
lemma(in UP_cring) one_over_poly_monom: assumes"a β carrier R" shows"one_over_poly (monom P a n) = monom P a 0" apply(rule ext) unfolding one_over_poly_def using assms by (metis cfs_monom deg_monom diff_diff_cancel diff_is_0_eq diff_self_eq_0 zero_diff)
lemma(in UP_cring) one_over_poly_monom_add: assumes"a β carrier R" assumes"a β 0" assumes"p β carrier P" assumes"degree p < n" shows"one_over_poly (p β monom P a n) = monom P a 0 β monom P 1 (n - degree p) β one_over_poly p" proof- have0: "degree (p β monom P a n) = n" by (simp add: assms(1) assms(2) assms(3) assms(4) equal_deg_sum) show ?thesis proof(rule ext) fix x show"one_over_poly (p β monom P a n) x = (monom P a 0 β monom P 1 (n - deg R p) β one_over_poly p) x" proof(cases "x = 0") case T: True have T0: "one_over_poly (p β monom P a n) 0 = a" unfolding one_over_poly_def by (metis lcf_eq lcf_monom(1) ltrm_of_sum_diff_deg P.add.m_closed assms(1) assms(2) assms(3) assms(4) diff_zero le0 monom_closed) have T1: "(monom P a 0 β monom P 1 (n - degree p) β one_over_poly p) 0 = a" using one_over_poly_closed by (metis (no_types, lifting) lcf_monom(1) R.one_closed R.r_zero UP_m_comm UP_mult_closed assms(1) assms(3) assms(4) cfs_add cfs_monom_mult deg_const monom_closed zero_less_diff) show ?thesis using T0 T1 T by auto next case F: False show ?thesis proof(cases "x < n - degree p") case True thenhave T0: "degree p < n - x β§ n - x < n" using F by auto thenhave T1: "one_over_poly (p β monom P a n) x = 0" using True F 0unfolding one_over_poly_def using assms(1) assms(3) coeff_of_sum_diff_degree0 by (metis ltrm_cfs ltrm_of_sum_diff_deg P.add.m_closed P.add.m_comm assms(2) assms(4) monom_closed nat_neq_iff) have"(monom P a 0 β monom P 1 (n - degree p) β one_over_poly p) x = 0" using True F 0 one_over_poly_def one_over_poly_closed by (metis (no_types, lifting) P.add.m_comm P.m_closed R.one_closed UP_m_comm assms(1)
assms(3) cfs_monom_mult coeff_of_sum_diff_degree0 deg_const monom_closed neq0_conv) thenshow ?thesis using T1 by auto next case False thenhave"n - degree p β€ x" by auto thenobtain k where k_def: "k + (n - degree p) = x" using le_Suc_ex diff_add by blast have F0: "(monom P a 0 β monom P 1 (n - deg R p) β one_over_poly p) x = one_over_poly p k" using k_def one_over_poly_closed assms
times_X_pow_coeff[of "one_over_poly p""n - deg R p" k]
P.m_closed by (metis (no_types, lifting) P.add.m_comm R.one_closed add_gr_0 coeff_of_sum_diff_degree0 deg_const monom_closed zero_less_diff) show ?thesis proof(cases "x β€ n") case True have T0: "n - x = degree p - k" using assms(4) k_def by linarith have T1: "n - x < n" using True F by linarith thenhave F1: "(p β monom P a n) (n - x) = p (degree p - k)" using True False F0 0 k_def cfs_add by (simp add: F0 T0 assms(1) assms(3) cfs_closed cfs_monom) thenshow ?thesis using"0" F0 assms(1) assms(2) assms(3) degree_of_sum_diff_degree k_def one_over_poly_def by auto next case False thenshow ?thesis using"0" F0 assms(1) assms(2) assms(3) degree_of_sum_diff_degree k_def one_over_poly_def by auto qed qed qed qed qed
lemma( in UP_cring) one_over_poly_eval: assumes"p β carrier P" assumes"x β carrier R" assumes"x β Units R" shows"to_fun (one_over_poly p) x = (x[^](degree p)) β (to_fun p (inv x))" proof(rule poly_induct6[of p]) show" p β carrier P" using assms by simp show"β§a n. a β carrier R ==> to_fun (one_over_poly (monom P a 0)) x = x [^] deg R (monom P a 0) β to_fun (monom P a 0) (inv x)" using assms to_fun_const one_over_poly_monom by auto show"β§a n p. a β carrier R ==> a β 0==> p β carrier P ==> deg R p < n ==> to_fun (one_over_poly p) x = x [^] deg R p β to_fun p (inv x) ==> to_fun (one_over_poly (p β monom P a n)) x = x [^] deg R (p β monom P a n) β to_fun (p β monom P a n) (inv x)" proof- fix a n p assume A: "a β carrier R""a β 0""p β carrier P""deg R p < n" "to_fun (one_over_poly p) x = x [^] deg R p β to_fun p (inv x)" have"one_over_poly (p β monom P a n) = monom P a 0 β monom P 1 (n - degree p) βone_over_poly p" using A by (simp add: one_over_poly_monom_add) hence"to_fun ( one_over_poly (p β monom P a n)) x = a β to_fun ( monom P 1 (n - degree p) β one_over_poly p) x" using A to_fun_plus one_over_poly_closed cfs_add by (simp add: assms(2) to_fun_const) hence"to_fun (one_over_poly (p β monom P a n)) x = a β x[^](n - degree p) β x [^] degree p β to_fun p (inv x)" by (simp add: A(3) A(5) R.m_assoc assms(2) assms(3) to_fun_closed to_fun_monic_monom to_fun_mult one_over_poly_closed) hence0:"to_fun (one_over_poly (p β monom P a n)) x = a β x[^]n β to_fun p (inv x)" using A R.nat_pow_mult assms(2) by auto have1: "to_fun (one_over_poly (p β monom P a n)) x = x[^]n β (a β inv x [^]n β to_fun p (inv x))" proof- have"x[^]n β a β inv x [^]n = a" by (metis (no_types, opaque_lifting) A(1) R.Units_inv_closed R.Units_r_inv R.m_assoc
R.m_comm R.nat_pow_closed R.nat_pow_distrib R.nat_pow_one R.r_one assms(2) assms(3)) thus ?thesis using A R.ring_simprules(23)[of _ _ "x[^]n"] 0 R.m_assoc assms(2) assms(3) to_fun_closed by auto qed have2: "degree (p β monom P a n) = n" by (simp add: A(1) A(2) A(3) A(4) equal_deg_sum) show" to_fun (one_over_poly (p β monom P a n)) x = x [^] deg R (p β monom P a n)β to_fun (p β monom P a n) (inv x)" using12 by (metis (no_types, lifting) A(1) A(3) P_def R.Units_inv_closed R.add.m_comm
UP_cring.to_fun_monom UP_cring_axioms assms(3) to_fun_closed to_fun_plus monom_closed) qed qed
end
(**************************************************************************************************) (**************************************************************************************************) sectionβΉLifting Homomorphisms of Rings to Polynomial Rings by Application to CoefficientsβΊ (**************************************************************************************************) (**************************************************************************************************)
definition poly_lift_hom where "poly_lift_hom R S φ = eval R (UP S) (to_polynomial S β φ) (X_poly S)"
context UP_ring begin
lemma(in UP_cring) pre_poly_lift_hom_is_hom: assumes"cring S" assumes"φ β ring_hom R S" shows"ring_hom_ring R (UP S) (to_polynomial S β φ)" apply(rule ring_hom_ringI) apply (simp add: R.ring_axioms) apply (simp add: UP_ring.UP_ring UP_ring.intro assms(1) cring.axioms(1)) using UP_cring.intro UP_cring.to_poly_closed assms(1) assms(2) ring_hom_closed apply fastforce using assms UP_cring.to_poly_closed[of S] ring_hom_closed[of φ R S] comp_apply[of "to_polynomial S" φ] unfolding UP_cring_def apply (metis UP_cring.to_poly_mult UP_cring_def ring_hom_mult) using assms UP_cring.to_poly_closed[of S] ring_hom_closed[of φ R S] comp_apply[of "to_polynomial S" φ] unfolding UP_cring_def apply (metis UP_cring.to_poly_add UP_cring_def ring_hom_add) using assms UP_cring.to_poly_closed[of S] ring_hom_one[of φ R S] comp_apply[of "to_polynomial S" φ] unfolding UP_cring_def by (simp add: βΉφ β ring_hom R S ==> φ 1 = 1βΊ UP_cring.intro UP_cring.to_poly_is_ring_hom ring_hom_one)
lemma(in UP_cring) poly_lift_hom_is_hom: assumes"cring S" assumes"φ β ring_hom R S" shows"poly_lift_hom R S φ β ring_hom (UP R) (UP S)" unfolding poly_lift_hom_def apply( rule UP_pre_univ_prop.eval_ring_hom[of R "UP S" ]) unfolding UP_pre_univ_prop_def apply (simp add: R_cring RingHom.ring_hom_cringI UP_cring.UP_cring UP_cring_def assms(1) assms(2) pre_poly_lift_hom_is_hom) by (simp add: UP_cring.X_closed UP_cring.intro assms(1))
lemma(in UP_cring) poly_lift_hom_closed: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" shows"poly_lift_hom R S φ p β carrier (UP S)" by (metis assms(1) assms(2) assms(3) poly_lift_hom_is_hom ring_hom_closed)
lemma(in UP_cring) poly_lift_hom_add: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" assumes"q β carrier (UP R)" shows"poly_lift_hom R S φ (p β R q) = poly_lift_hom R S φ p β S poly_lift_hom R S φ q" using assms poly_lift_hom_is_hom[of S φ] ring_hom_add[of "poly_lift_hom R S φ""UP R""UP S" p q] by blast
lemma(in UP_cring) poly_lift_hom_mult: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" assumes"q β carrier (UP R)" shows"poly_lift_hom R S φ (p β R q) = poly_lift_hom R S φ p β S poly_lift_hom R S φ q" using assms poly_lift_hom_is_hom[of S φ] ring_hom_mult[of "poly_lift_hom R S φ""UP R""UP S" p q] by blast
lemma(in UP_cring) poly_lift_hom_extends_hom: assumes"cring S" assumes"φ β ring_hom R S" assumes"r β carrier R" shows"poly_lift_hom R S φ (to_polynomial R r) = to_polynomial S (φ r)" using UP_pre_univ_prop.eval_const[of R "UP S""to_polynomial S β φ""X_poly S" r ] assms
comp_apply[of "λa. monom (UP S) a 0" φ r] pre_poly_lift_hom_is_hom[of S φ] unfolding poly_lift_hom_def to_polynomial_def UP_pre_univ_prop_def by (simp add: R_cring RingHom.ring_hom_cringI UP_cring.UP_cring UP_cring.X_closed UP_cring.intro)
lemma(in UP_cring) poly_lift_hom_extends_hom': assumes"cring S" assumes"φ β ring_hom R S" assumes"r β carrier R" shows"poly_lift_hom R S φ (monom P r 0) = monom (UP S) (φ r) 0" using poly_lift_hom_extends_hom[of S φ r] assms unfolding to_polynomial_def P_def by blast
lemma(in UP_cring) poly_lift_hom_smult: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" assumes"a β carrier R" shows"poly_lift_hom R S φ (a β R p) = φ a β S (poly_lift_hom R S φ p)" using assms poly_lift_hom_is_hom[of S φ] poly_lift_hom_extends_hom'[of S φ a]
poly_lift_hom_mult[of S φ "monom P a 0" p] ring_hom_closed[of φ R S a]
UP_ring.monom_mult_is_smult[of S "φ a""poly_lift_hom R S φ p"]
monom_mult_is_smult[of a p] monom_closed[of a 0] poly_lift_hom_closed[of S φ p] unfolding to_polynomial_def UP_ring_def P_def cring_def by simp
lemma(in UP_cring) poly_lift_hom_monom: assumes"cring S" assumes"φ β ring_hom R S" assumes"r β carrier R" shows"poly_lift_hom R S φ (monom (UP R) r n) = (monom (UP S) (φ r) n)" proof- have"eval R (UP S) (to_polynomial S β φ) (X_poly S) (monom (UP R) r n) = (to_polynomial S β φ) r β S X_poly S [^] S n" using assms UP_pre_univ_prop.eval_monom[of R "UP S""to_polynomial S β φ" r "X_poly S" n] unfolding UP_pre_univ_prop_def UP_cring_def ring_hom_cring_def by (meson UP_cring.UP_cring UP_cring.X_closed UP_cring.pre_poly_lift_hom_is_hom UP_cring_axioms
UP_cring_def ring_hom_cring_axioms.intro ring_hom_ring.homh) thenhave"eval R (UP S) (to_polynomial S β φ) (X_poly S) (monom (UP R) r n) = (to_polynomial S (φ r)) β S X_poly S [^] S n" by simp thenshow ?thesis unfolding poly_lift_hom_def using assms UP_cring.monom_rep_X_pow[of S "φ r" n] ring_hom_closed[of φ R S r] by (metis UP_cring.X_closed UP_cring.intro UP_cring.monom_sub UP_cring.sub_monom(1)) qed
lemma(in UP_cring) poly_lift_hom_X_var: assumes"cring S" assumes"φ β ring_hom R S" shows"poly_lift_hom R S φ (monom (UP R) 1 1) = (monom (UP S) 1 1)" using assms(1) assms(2) poly_lift_hom_monom ring_hom_one by fastforce
lemma(in UP_cring) poly_lift_hom_X_var': assumes"cring S" assumes"φ β ring_hom R S" shows"poly_lift_hom R S φ (X_poly R) = (X_poly S)" unfolding X_poly_def using assms(1) assms(2) poly_lift_hom_X_var by blast
lemma(in UP_cring) poly_lift_hom_X_var'': assumes"cring S" assumes"φ β ring_hom R S" shows"poly_lift_hom R S φ (monom (UP R) 1 n) = (monom (UP S) 1 n)" using assms(1) assms(2) poly_lift_hom_monom ring_hom_one by fastforce
lemma(in UP_cring) poly_lift_hom_X_var''': assumes"cring S" assumes"φ β ring_hom R S" shows"poly_lift_hom R S φ (X_poly R [^] R (n::nat)) = (X_poly S) [^] S (n::nat)" using assms by (smt (verit) ltrm_of_X P.nat_pow_closed P_def R.ring_axioms UP_cring.to_fun_closed UP_cring.intro
UP_cring.monom_pow UP_cring.poly_lift_hom_monom UP_cring_axioms X_closed cfs_closed
cring.axioms(1) to_fun_X_pow poly_lift_hom_X_var' ring_hom_closed ring_hom_nat_pow)
lemma(in UP_cring) poly_lift_hom_X_plus: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" shows"poly_lift_hom R S φ (X_poly_plus R a) = X_poly_plus S (φ a)" using ring_hom_add unfolding X_poly_plus_def using P_def X_closed assms(1) assms(2) assms(3) poly_lift_hom_X_var' poly_lift_hom_add poly_lift_hom_extends_hom to_poly_closed by fastforce
lemma(in UP_cring) poly_lift_hom_X_plus_nat_pow: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" shows"poly_lift_hom R S φ (X_poly_plus R a [^] R (n::nat)) = X_poly_plus S (φ a) [^] S (n::nat)" using assms poly_lift_hom_X_plus[of S φ a]
ring_hom_nat_pow[of "UP R""UP S""poly_lift_hom R S φ""X_poly_plus R a" n]
poly_lift_hom_is_hom[of S φ] X_plus_closed[of a] UP_ring.UP_ring[of S] unfolding P_def cring_def UP_cring_def using P_def UP_ring UP_ring.intro by (simp add: UP_ring.intro)
lemma(in UP_cring) X_poly_plus_nat_pow_closed: assumes"a β carrier R" shows" X_poly_plus R a [^] R (n::nat) β carrier (UP R)" using assms P.nat_pow_closed P_def X_plus_closed by auto
lemma(in UP_cring) poly_lift_hom_X_plus_nat_pow_smult: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" assumes"b β carrier R" shows"poly_lift_hom R S φ (b β R X_poly_plus R a [^] R (n::nat)) = φ b β S X_poly_plus S (φ a) [^] S (n::nat)" by (simp add: X_poly_plus_nat_pow_closed assms(1) assms(2) assms(3) assms(4) poly_lift_hom_X_plus_nat_pow poly_lift_hom_smult)
lemma(in UP_cring) poly_lift_hom_X_minus: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" shows"poly_lift_hom R S φ (X_poly_minus R a) = X_poly_minus S (φ a)" using poly_lift_hom_X_plus[of S φ "β a"] X_minus_plus[of a] UP_cring.X_minus_plus[of S "φ a"]
R.ring_hom_a_inv[of S φ a] unfolding UP_cring_def P_def by (metis R.add.inv_closed assms(1) assms(2) assms(3) cring.axioms(1) ring_hom_closed)
lemma(in UP_cring) poly_lift_hom_X_minus_nat_pow: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" shows"poly_lift_hom R S φ (X_poly_minus R a [^] R (n::nat)) = X_poly_minus S (φ a) [^] S (n::nat)" using assms poly_lift_hom_X_minus ring_hom_nat_pow X_minus_plus UP_cring.X_minus_plus
poly_lift_hom_X_plus poly_lift_hom_X_plus_nat_pow by fastforce
lemma(in UP_cring) X_poly_minus_nat_pow_closed: assumes"a β carrier R" shows"X_poly_minus R a [^] R (n::nat) β carrier (UP R)" using assms monoid.nat_pow_closed[of "UP R""X_poly_minus R a" n]
P.nat_pow_closed P_def X_minus_closed by auto
lemma(in UP_cring) poly_lift_hom_X_minus_nat_pow_smult: assumes"cring S" assumes"φ β ring_hom R S" assumes"a β carrier R" assumes"b β carrier R" shows"poly_lift_hom R S φ (b β R X_poly_minus R a [^] R (n::nat)) = φ b β S X_poly_minus S (φ a) [^] S (n::nat)" by (simp add: X_poly_minus_nat_pow_closed assms(1) assms(2) assms(3) assms(4) poly_lift_hom_X_minus_nat_pow poly_lift_hom_smult)
lemma(in UP_cring) poly_lift_hom_cf: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier P" shows"poly_lift_hom R S φ p k = φ (p k)" apply(rule poly_induct3[of p]) apply (simp add: assms(3)) proof- show"β§p q. q β carrier P ==> p β carrier P ==> poly_lift_hom R S φ p k = φ (p k) ==> poly_lift_hom R S φ q k = φ (q k) ==> poly_lift_hom R S φ (p β q) k = φ ((p β q) k)" proof- fix p q assume A: "p β carrier P""q β carrier P" "poly_lift_hom R S φ p k = φ (p k)""poly_lift_hom R S φ q k = φ (q k)" show"poly_lift_hom R S φ q k = φ (q k) ==> poly_lift_hom R S φ (p β q) k = φ ((p β q) k)" using A assms poly_lift_hom_add[of S φ p q]
poly_lift_hom_closed[of S φ p] poly_lift_hom_closed[of S φ q]
UP_ring.cfs_closed[of S "poly_lift_hom R S φ q " k] UP_ring.cfs_closed[of S "poly_lift_hom R S φ p" k]
UP_ring.cfs_add[of S "poly_lift_hom R S φ p""poly_lift_hom R S φ q" k] unfolding P_def UP_ring_def by (metis (full_types) P_def cfs_add cfs_closed cring.axioms(1) ring_hom_add) qed show"β§a n. a β carrier R ==> poly_lift_hom R S φ (monom P a n) k = φ (monom P a n k)" proof- fix a m assume A: "a β carrier R" show"poly_lift_hom R S φ (monom P a m) k = φ (monom P a m k)" apply(cases "m = k") using cfs_monom[of a m k] assms poly_lift_hom_monom[of S φ a m] UP_ring.cfs_monom[of S "φ a" m k] unfolding P_def UP_ring_def apply (simp add: A cring.axioms(1) ring_hom_closed) using cfs_monom[of a m k] assms poly_lift_hom_monom[of S φ a m] UP_ring.cfs_monom[of S "φ a" m k] unfolding P_def UP_ring_def by (metis A P_def R.ring_axioms cring.axioms(1) ring_hom_closed ring_hom_zero) qed qed
lemma(in ring) ring_hom_monom_term: assumes"a β carrier R" assumes"c β carrier R" assumes"ring S" assumes"h β ring_hom R S" shows"h (a β c[^](n::nat)) = h a β (h c)[^]n" apply(induction n) using assms ringE(2) ring_hom_closed apply fastforce by (metis assms(1) assms(2) assms(3) assms(4) local.ring_axioms nat_pow_closed ring_hom_mult ring_hom_nat_pow)
lemma(in UP_cring) poly_lift_hom_eval: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier P" assumes"a β carrier R" shows"UP_cring.to_fun S (poly_lift_hom R S φ p) (φ a) = φ (to_fun p a) " apply(rule poly_induct3[of p]) apply (simp add: assms(3)) proof- show"β§p q. q β carrier P ==> p β carrier P ==> UP_cring.to_fun S (poly_lift_hom R S φ p) (φ a) = φ (to_fun p a) ==> UP_cring.to_fun S (poly_lift_hom R S φ q) (φ a) = φ (to_fun q a) ==> UP_cring.to_fun S (poly_lift_hom R S φ (p β q)) (φ a) = φ (to_fun (p β q) a)" proof- fix p q assume A: "q β carrier P""p β carrier P" "UP_cring.to_fun S (poly_lift_hom R S φ p) (φ a) = φ (to_fun p a)" "UP_cring.to_fun S (poly_lift_hom R S φ q) (φ a) = φ (to_fun q a)" have"(poly_lift_hom R S φ (p β q)) = poly_lift_hom R S φ p β S poly_lift_hom R S φ q" using A(1) A(2) P_def assms(1) assms(2) poly_lift_hom_add by auto hence"UP_cring.to_fun S (poly_lift_hom R S φ (p β q)) (φ a) = UP_cring.to_fun S (poly_lift_hom R S φ p) (φ a) β UP_cring.to_fun S (poly_lift_hom R S φ q) (φ a)" using UP_cring.to_fun_plus[of S] assms unfolding UP_cring_def by (metis (no_types, lifting) A(1) A(2) P_def poly_lift_hom_closed ring_hom_closed) thus"UP_cring.to_fun S (poly_lift_hom R S φ (p β q)) (φ a) = φ (to_fun (p β q) a)" using A to_fun_plus assms ring_hom_add[of φ R S]
poly_lift_hom_closed[of S φ] UP_cring.to_fun_def[of S] to_fun_def unfolding P_def UP_cring_def using UP_cring.to_fun_closed UP_cring_axioms by metis qed show"β§c n. c β carrier R ==> UP_cring.to_fun S (poly_lift_hom R S φ (monom P c n)) (φ a) = φ (to_fun (monom P c n) a)" unfolding P_def proof - fix c n assume A: "c β carrier R" have0: "φ (a [^] (n::nat)) = φ a [^] n" using assms ring_hom_nat_pow[of R S φ a n] unfolding cring_def using R.ring_axioms by blast have1: "φ (c β a [^] n) = φ c β φ a [^] n" using ring_hom_mult[of φ R S c "a [^] n" ] 0 assms A monoid.nat_pow_closed [of R a n] by (simp add: cring.axioms(1) ringE(2)) show"UP_cring.to_fun S (poly_lift_hom R S φ (monom (UP R) c n)) (φ a) = φ (to_fun(monom (UP R) c n) a)" using assms A poly_lift_hom_monom[of S φ c n] UP_cring.to_fun_monom[of S "φ c""φ a" n]
to_fun_monom[of c a n] 01 ring_hom_closed[of φ R S] unfolding UP_cring_def by (simp add: P_def to_fun_def) qed qed
lemma(in UP_cring) poly_lift_hom_sub: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier P" assumes"q β carrier P" shows"poly_lift_hom R S φ (compose R p q) = compose S (poly_lift_hom R S φ p) (poly_lift_hom R S φ q)" apply(rule poly_induct3[of p]) apply (simp add: assms(3)) proof- show" β§p qa. qa β carrier P ==> p β carrier P ==> poly_lift_hom R S φ (Cring_Poly.compose R p q) = Cring_Poly.compose S (poly_lift_hom R S φ p) (poly_lift_hom R S φ q) ==> poly_lift_hom R S φ (Cring_Poly.compose R qa q) = Cring_Poly.compose S (poly_lift_hom R S φ qa) (poly_lift_hom R S φ q) ==> poly_lift_hom R S φ (Cring_Poly.compose R (p β qa) q) = Cring_Poly.compose S (poly_lift_hom R S φ (p β qa)) (poly_lift_hom R S φ q)" proof- fix a b assume A: "a β carrier P" "b β carrier P" "poly_lift_hom R S φ (Cring_Poly.compose R a q) = Cring_Poly.compose S (poly_lift_hom R S φ a) (poly_lift_hom R S φ q)" "poly_lift_hom R S φ (Cring_Poly.compose R b q) = Cring_Poly.compose S (poly_lift_hom R S φ b) (poly_lift_hom R S φ q)" show"poly_lift_hom R S φ (Cring_Poly.compose R (a β b) q) = Cring_Poly.compose S (poly_lift_hom R S φ (a β b)) (poly_lift_hom R S φ q)" using assms UP_cring.sub_add[of R q a b ] UP_cring.sub_add[of S ] unfolding UP_cring_def by (metis A(1) A(2) A(3) A(4) P_def R_cring UP_cring.sub_closed UP_cring_axioms poly_lift_hom_add poly_lift_hom_closed) qed show"β§a n. a β carrier R ==> poly_lift_hom R S φ (Cring_Poly.compose R (monom P a n) q) = Cring_Poly.compose S (poly_lift_hom R S φ (monom P a n)) (poly_lift_hom R S φ q)" proof- fix a n assume A: "a β carrier R" have0: "(poly_lift_hom R S φ (monom (UP R) a n)) = monom (UP S) (φ a) n" by (simp add: A assms(1) assms(2) assms(3) assms(4) poly_lift_hom_monom) have1: " q [^] R n β carrier (UP R)" using monoid.nat_pow_closed[of "UP R" q n] UP_ring.UP_ring UP_ring.intro assms(1) assms
P.monoid_axioms P_def by blast have2: "poly_lift_hom R S φ (to_polynomial R a β R q [^] R n) = to_polynomial S (φ a) β S (poly_lift_hom R S φ q) [^] S n" using poly_lift_hom_mult[of S φ "to_polynomial R a""q [^] R n"] poly_lift_hom_is_hom[of S φ]
ring_hom_nat_pow[of P "UP S""poly_lift_hom R S φ" q n] UP_cring.UP_cring[of S]
UP_cring poly_lift_hom_monom[of S φ a 0] ring_hom_closed[of φ R S a]
monom_closed[of a 0] nat_pow_closed[of q n] assms A unfolding to_polynomial_def P_def UP_cring_def cring_def by auto have3: "poly_lift_hom R S φ (Cring_Poly.compose R (monom (UP R) a n) q) = to_polynomial S (φ a) β S (poly_lift_hom R S φ q) [^] S n" using"2" A P_def assms(4) sub_monom(1) by auto have4: "Cring_Poly.compose S (poly_lift_hom R S φ (monom (UP R) a n)) (poly_lift_hom R S φ q) = Cring_Poly.compose S (monom (UP S) (φ a) n) (poly_lift_hom R S φ q)" by (simp add: "0") have"poly_lift_hom R S φ q β carrier (UP S)" using P_def UP_cring.poly_lift_hom_closed UP_cring_axioms assms(1) assms(2) assms(4) byblast thenhave5: "Cring_Poly.compose S (poly_lift_hom R S φ (monom (UP R) a n)) (poly_lift_hom R S φ q) = to_polynomial S (φ a) β S (poly_lift_hom R S φ q) [^] S n" using4 UP_cring.sub_monom[of S "poly_lift_hom R S φ q""φ a" n] assms unfolding UP_cring_def by (simp add: A ring_hom_closed) thus"poly_lift_hom R S φ (Cring_Poly.compose R (monom P a n) q) = Cring_Poly.compose S (poly_lift_hom R S φ (monom P a n)) (poly_lift_hom R S φ q)" using01234 assms A by (simp add: P_def) qed qed
lemma(in UP_cring) poly_lift_hom_comm_taylor_expansion: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier P" assumes"a β carrier R" shows"poly_lift_hom R S φ (taylor_expansion R a p) = taylor_expansion S (φ a) (poly_lift_hom R S φ p)" unfolding taylor_expansion_def using poly_lift_hom_sub[of S φ p "(X_poly_plus R a)"] poly_lift_hom_X_plus[of S φ a] assms by (simp add: P_def UP_cring.X_plus_closed UP_cring_axioms)
lemma(in UP_cring) poly_lift_hom_comm_taylor_expansion_cf: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" assumes"a β carrier R" shows"φ (taylor_expansion R a p i) = taylor_expansion S (φ a) (poly_lift_hom R S φ p) i" using poly_lift_hom_cf assms poly_lift_hom_comm_taylor_expansion P_def
taylor_def UP_cring.taylor_closed UP_cring_axioms by fastforce
lemma(in UP_cring) taylor_expansion_cf_closed: assumes"p β carrier P" assumes"a β carrier R" shows"taylor_expansion R a p i β carrier R" using assms taylor_closed by (simp add: taylor_def cfs_closed)
lemma(in UP_cring) poly_lift_hom_comm_taylor_term: assumes"cring S" assumes"φ β ring_hom R S" assumes"p β carrier (UP R)" assumes"a β carrier R" shows"poly_lift_hom R S φ (taylor_term a p i) = UP_cring.taylor_term S (φ a) (poly_lift_hom R S φ p) i" using poly_lift_hom_X_minus_nat_pow_smult[of S φ a "taylor_expansion R a p i" i]
poly_lift_hom_comm_taylor_expansion[of S φ p a]
poly_lift_hom_comm_taylor_expansion_cf[of S φ p a i]
assms UP_cring.taylor_term_def[of S] unfolding taylor_term_def UP_cring_def P_def by (simp add: UP_cring.taylor_expansion_cf_closed UP_cring_axioms)
lemma(in UP_cring) poly_lift_hom_degree_bound: assumes"cring S" assumes"h β ring_hom R S" assumes"f β carrier (UP R)" shows"deg S (poly_lift_hom R S h f) β€ deg R f" using poly_lift_hom_closed[of S h f] UP_cring.deg_leqI[of S "poly_lift_hom R S h f""deg R f"] assms ring_hom_zero[of h R S] deg_aboveD[of f] coeff_simp[of f] unfolding P_def UP_cring_def by (simp add: P_def R.ring_axioms cring.axioms(1) poly_lift_hom_cf)
lemma(in UP_cring) deg_eqI: assumes"f β carrier (UP R)" assumes"deg R f β€ n" assumes"f n β 0" shows"deg R f = n" using assms coeff_simp[of f] P_def deg_leE le_neq_implies_less by blast
lemma(in UP_cring) poly_lift_hom_degree_eq: assumes"cring S" assumes"h β ring_hom R S" assumes"h (lcf f) β 0" assumes"f β carrier (UP R)" shows"deg S (poly_lift_hom R S h f) = deg R f" apply(rule UP_cring.deg_eqI) using assms unfolding UP_cring_def apply blast using poly_lift_hom_closed[of S h f] assms apply blast using poly_lift_hom_degree_bound[of S h f] assms apply blast using assms poly_lift_hom_cf[of S h f] by (metis P_def)
lemma(in UP_cring) poly_lift_hom_lcoeff: assumes"cring S" assumes"h β ring_hom R S" assumes"h (lcf f) β 0" assumes"f β carrier (UP R)" shows"UP_ring.lcf S (poly_lift_hom R S h f) = h (lcf f)" using poly_lift_hom_degree_eq[of S h f] assms by (simp add: P_def poly_lift_hom_cf)
end
(**************************************************************************************************) (**************************************************************************************************) sectionβΉCoefficient List Constructor for PolynomialsβΊ (**************************************************************************************************) (**************************************************************************************************)
definition list_to_poly where "list_to_poly R as n = (if n < length as then as!n else 0)"
context UP_ring begin
lemma(in UP_ring) list_to_poly_closed: assumes"set as β carrier R" shows"list_to_poly R as β carrier P" apply(rule UP_car_memI[of "length as"]) apply (simp add: list_to_poly_def) by (metis R.zero_closed assms in_mono list_to_poly_def nth_mem)
lemma(in UP_ring) list_to_poly_zero[simp]: "list_to_poly R [] = 0 R" unfolding list_to_poly_def apply auto by(simp add: UP_def)
lemma(in UP_domain) list_to_poly_singleton: assumes"a β carrier R" shows"list_to_poly R [a] = monom P a 0" apply(rule ext) unfolding list_to_poly_def using assms by (simp add: cfs_monom) end
definition cf_list where "cf_list R p = map p [(0::nat)..< Suc (deg R p)]"
lemma cf_list_length: "length (cf_list R p) = Suc (deg R p)" unfolding cf_list_def by simp
lemma cf_list_entries: assumes"i β€ deg R p" shows"(cf_list R p)!i = p i" using assms by (simp add: cf_list_def nth_append)
lemma(in UP_ring) list_to_poly_cf_list_inv: assumes"p β carrier (UP R)" shows"list_to_poly R (cf_list R p) = p" proof fix x show"list_to_poly R (cf_list R p) x = p x" apply(cases "x < degree p") unfolding list_to_poly_def using assms cf_list_length[of R p] cf_list_entries[of _ R p] apply simp by (metis P_def UP_ring.coeff_simp UP_ring_axioms βΉβ§i. i β€ deg R p ==> cf_list R p ! i = p iβΊβΉlength (cf_list R p) = Suc (deg R p)βΊ assms deg_belowI less_Suc_eq_le) qed
sectionβΉPolynomial Rings over a SubringβΊ
subsectionβΉCharacterizing the Carrier of a Polynomial Ring over a SubringβΊ lemma(in ring) carrier_update: "carrier (R(carrier := S)) = S" "0R(carrier := S)) = 0" "1R(carrier := S)) = 1" "(βR(carrier := S))) = (β)" "(βR(carrier := S))) = (β)" by auto
lemma(in UP_cring) poly_cfs_subring: assumes"subring S R" assumes"g β carrier (UP R)" assumes"β§n. g n β S" shows"g β carrier (UP (R ( carrier := S )))" apply(rule UP_cring.UP_car_memI') using R.subcringI' R.subcring_iff UP_cring.intro assms(1) subringE(1) apply blast proof- have"carrier (R(carrier := S)) = S" using ring.carrier_update by simp thenshow0: "β§x. g x β carrier (R(carrier := S))" using assms by blast have0: "0(carrier := S) = 0" using R.carrier_update(2) by blast thenshow"β§x. (deg R g) < x ==> g x = 0(carrier := S)" using UP_car_memE assms(2) by presburger qed
lemma(in UP_cring) UP_ring_subring: assumes"subring S R" shows"UP_cring (R ( carrier := S ))""UP_ring (R ( carrier := S ))" using assms unfolding UP_cring_def using R.subcringI' R.subcring_iff subringE(1) apply blast using assms unfolding UP_ring_def using R.subcringI' R.subcring_iff subringE(1) by (simp add: R.subring_is_ring)
lemma(in UP_cring) UP_ring_subring_is_ring: assumes"subring S R" shows"cring (UP (R ( carrier := S )))" using assms UP_ring_subring[of S] UP_cring.UP_cring[of "R(carrier := S)"] by blast
lemma(in UP_cring) UP_ring_subring_add_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"f β carrier (UP (R ( carrier := S )))" shows"f β (R ( carrier := S ))g β carrier (UP (R ( carrier := S )))" using assms UP_ring_subring_is_ring[of S] by (meson cring.cring_simprules(1))
lemma(in UP_cring) UP_ring_subring_mult_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"f β carrier (UP (R ( carrier := S )))" shows"f β (R ( carrier := S ))g β carrier (UP (R ( carrier := S )))" using assms UP_ring_subring_is_ring[of S] by (meson cring.carrier_is_subcring subcringE(6))
lemma(in UP_cring) UP_ring_subring_car: assumes"subring S R" shows"carrier (UP (R ( carrier := S ))) = {h β carrier (UP R). βn. h n β S}" proof show"carrier (UP (R(carrier := S))) β {h β carrier (UP R). βn. h n β S}" proof fix h assume A: "h β carrier (UP (R(carrier := S)))" have"h β carrier P" apply(rule UP_car_memI[of "deg (R(carrier := S)) h"]) unfolding P_def using UP_cring.UP_car_memE[of "R(carrier := S)" h] R.carrier_update[of S]
assms UP_ring_subring A apply presburger using UP_cring.UP_car_memE[of "R(carrier := S)" h] assms by (metis A R.ring_axioms UP_cring_def βΉcarrier (R(carrier := S)) = SβΊ cring.subcringI' is_UP_cring ring.subcring_iff subringE(1) subsetD) thenshow"h β {h β carrier (UP R). βn. h n β S}" unfolding P_def using assms A UP_cring.UP_car_memE[of "R(carrier := S)" h] R.carrier_update[of S]
UP_ring_subring by blast qed show"{h β carrier (UP R). βn. h n β S} β carrier (UP (R(carrier := S)))" prooffix h assume A: "h β {h β carrier (UP R). βn. h n β S}" have0: "h β carrier (UP R)" using A by blast have1: "β§n. h n β S" using A by blast show"h β carrier (UP (R(carrier := S)))" apply(rule UP_ring.UP_car_memI[of _ "deg R h"]) using assms UP_ring_subring[of S] UP_cring.axioms UP_ring.intro cring.axioms(1) apply blast using UP_car_memE[of h] carrier_update 0 R.carrier_update(2) apply presburger using assms 1 R.carrier_update(1) by blast qed qed
lemma(in UP_cring) UP_ring_subring_car_subset: assumes"subring S R" shows"carrier (UP (R ( carrier := S ))) β carrier (UP R)" prooffix h assume"h β carrier (UP (R ( carrier := S )))" thenshow"h β carrier (UP R)" using assms UP_ring_subring_car[of S] by blast qed
lemma(in UP_cring) UP_ring_subring_car_subset': assumes"subring S R" assumes"h β carrier (UP (R ( carrier := S )))" shows"h β carrier (UP R)" using assms UP_ring_subring_car_subset[of S] by blast
lemma(in UP_cring) UP_ring_subring_add: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"f β carrier (UP (R ( carrier := S )))" shows"g β R f = g β (R ( carrier := S ))f" proof(rule ext) fix x show"(g β R f) x = (g β (R(carrier := S)) f) x" proof- have0: " (g β f) x = g x β f x" using assms cfs_add[of g f x] unfolding P_def using UP_ring_subring_car_subset' by blast have1: "(g β (R(carrier := S)) f) x = g x β(carrier := S) f x" using UP_ring.cfs_add[of "R ( carrier := S )" g f x] UP_ring_subring[of S] assms unfolding UP_ring_def UP_cring_def using R.subring_is_ring by blast show ?thesis using01 R.carrier_update(4)[of S] by (simp add: P_def) qed qed
lemma(in UP_cring) UP_ring_subring_deg: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" shows"deg R g = deg (R ( carrier := S )) g" proof- have0: "g β carrier (UP R)" using assms UP_ring_subring_car[of S] by blast have1: "deg R g β€ deg (R ( carrier := S )) g" using0 assms UP_cring.UP_car_memE[of "R ( carrier := S )" g]
UP_car_memE[of g] P_def R.carrier_update(2) UP_ring_subring deg_leqI by presburger have2: "deg (R ( carrier := S )) g β€ deg R g" using0 assms UP_cring.UP_car_memE[of "R ( carrier := S )" g]
UP_car_memE[of g] P_def R.carrier_update(2) UP_ring_subring UP_cring.deg_leqI by metis
show ?thesis using12by presburger qed
lemma(in UP_cring) UP_subring_monom: assumes"subring S R" assumes"a β S" shows"up_ring.monom (UP R) a n = up_ring.monom (UP (R ( carrier := S ))) a n" prooffix x have0: "a β carrier R" using assms subringE(1) by blast have1: "a β carrier (R(carrier := S))" using assms by (simp add: assms(2)) have2: " up_ring.monom (UP (R(carrier := S))) a n x = (if n = x then a else 0(carrier := S))" using1 assms UP_ring_subring[of S] UP_ring.cfs_monom[of "R(carrier := S)" a n x] UP_cring.axioms UP_ring.intro cring.axioms(1) by blast show"up_ring.monom (UP R) a n x = up_ring.monom (UP (R(carrier := S))) a n x" using012 cfs_monom[of a n x] R.carrier_update(2)[of S] unfolding P_def by presburger qed
lemma(in UP_cring) UP_ring_subring_mult: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"f β carrier (UP (R ( carrier := S )))" shows"g β R f = g β (R ( carrier := S ))f" proof(rule UP_ring.poly_induct3[of "R ( carrier := S )" f]) show"UP_ring (R(carrier := S))" by (simp add: UP_ring_subring(2) assms(1)) show" f β carrier (UP (R(carrier := S)))" by (simp add: assms(3)) show" β§p q. q β carrier (UP (R(carrier := S))) ==> p β carrier (UP (R(carrier := S))) ==> g β R p = g β (R(carrier := S)) p ==> g β R q = g β (R(carrier := S)) q ==> g β R (p β (R(carrier := S)) q) = g β (R(carrier := S)) (p β (R(carrier := S)) q)" proof- fix p q assume A: " q β carrier (UP (R(carrier := S)))" "p β carrier (UP (R(carrier := S)))" "g β R p = g β (R(carrier := S)) p" "g β R q = g β (R(carrier := S)) q" have0: "p β (R(carrier := S)) q = p β R q" using A UP_ring_subring_add[of S p q] by (simp add: assms(1)) have1: "g β R (p β R q) = g β R p β R g β R q" using0 A assms P.r_distr P_def UP_ring_subring_car_subset' by auto hence2:"g β R (p β (R(carrier := S)) q) = g β R p β R g β R q" using0by simp have3: "g β (R(carrier := S)) (p β (R(carrier := S)) q) = g β (R(carrier := S)) p β (R(carrier := S)) g β (R(carrier := S)) q" using0 A assms semiring.r_distr[of "UP (R(carrier := S))"] UP_ring_subring_car_subset' using UP_ring.UP_r_distr βΉUP_ring (R(carrier := S))βΊby blast hence4: "g β (R(carrier := S)) (p β (R(carrier := S)) q) = g β R p β (R(carrier := S)) g β R q" using A by simp hence5: "g β (R(carrier := S)) (p β (R(carrier := S)) q) = g β R p β R g β R q" using UP_ring_subring_add[of S] by (simp add: A(1) A(2) A(3) A(4) UP_ring.UP_mult_closed βΉUP_ring (R(carrier := S))βΊ assms(1) assms(2)) show"g β R (p β (R(carrier := S)) q) = g β (R(carrier := S)) (p β (R(carrier := S)) q)" by (simp add: "2""5") qed show"β§a n. a β carrier (R(carrier := S)) ==> g β R monom (UP (R(carrier := S))) a n = g β (R(carrier := S)) monom (UP (R(carrier := S))) a n" prooffix a n x assume A: "a β carrier (R(carrier := S))" have0: "monom (UP (R(carrier := S))) a n = monom (UP R) a n" using A UP_subring_monom assms(1) by auto have1: "g β carrier (UP R)" using assms UP_ring_subring_car_subset' by blast have2: "a β carrier R" using A assms subringE(1)[of S R] R.carrier_update[of S] by blast show"(g β R monom (UP (R(carrier := S))) a n) x = (g β (R(carrier := S)) monom (UP (R(carrier := S))) a n) x" proof(cases "x < n") case True have T0: "(g β R monom (UP R) a n) x = 0" using12 True cfs_monom_mult[of g a x n] A assms unfolding P_def by blast thenshow ?thesis using UP_cring.cfs_monom_mult[of "R(carrier := S)" g a x n] 0 A True
UP_ring_subring(1) assms(1) assms(2) by auto next case False have F0: "(g β R monom (UP R) a n) x = a β (g (x - n))" using12 False cfs_monom_mult_l[of g a n "x - n"] A assms unfolding P_def by simp have F1: "(g β (R(carrier := S)) monom (UP (R(carrier := S))) a n) (x - n + n) = a β(carrier := S) g (x - n)" using12 False UP_cring.cfs_monom_mult_l[of "R(carrier := S)" g a n "x - n"] A assms
UP_ring_subring(1) by blast hence F2: "(g β (R(carrier := S)) monom (UP R) a n) (x - n + n) = a β g (x - n)" using UP_subring_monom[of S a n] R.carrier_update[of S] assms 0by metis show ?thesis using F0 F1 12 assms by (simp add: "0" False add.commute add_diff_inverse_nat) qed qed qed
lemma(in UP_cring) UP_ring_subring_one: assumes"subring S R" shows"1 R = 1 (R ( carrier := S ))" using UP_subring_monom[of S 10] assms P_def R.subcringI' UP_ring.monom_one UP_ring_subring(2) monom_one subcringE(3) by force
lemma(in UP_cring) UP_ring_subring_zero: assumes"subring S R" shows"0 R = 0 (R ( carrier := S ))" using UP_subring_monom[of S 00] UP_ring.monom_zero[of "R ( carrier := S )"0] assms monom_zero[of 0]
UP_ring_subring[of S] subringE(2)[of S R] unfolding P_def by (simp add: P_def R.carrier_update(2))
lemma(in UP_cring) UP_ring_subring_nat_pow: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" shows"g[^] Rn = g[^] (R ( carrier := S ))(n::nat)" apply(induction n) using assms apply (simp add: UP_ring_subring_one) proof- fix n::nat assume A: "g [^] R n = g [^] (R(carrier := S)) n" have"Group.monoid (UP (R(carrier := S))) " using assms UP_ring_subring[of S] UP_ring.UP_ring[of "R(carrier := S)"] ring.is_monoid byblast hence0 : " g [^] (R(carrier := S)) n β carrier (UP (R(carrier := S)))" using monoid.nat_pow_closed[of "UP (R ( carrier := S ))" g n] assms UP_ring_subring unfolding UP_ring_def ring_def by blast have1: "g [^] R n β carrier (UP R)" using0 assms UP_ring_subring_car_subset'[of S] by (simp add: A) thenhave2: "g [^] R n β R g = g [^] (R(carrier := S)) n β (R(carrier := S)) g" using assms UP_ring_subring_mult[of S "g [^] R n" g] by (simp add: "0" A) thenshow"g [^] R Suc n = g [^] (R(carrier := S)) Suc n" by simp qed
lemma(in UP_cring) UP_subring_compose_monom: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"compose R (up_ring.monom (UP R) a n) g = compose (R ( carrier := S )) (up_ring.monom (UP (R ( carrier := S ))) a n) g" proof- have g_closed: "g β carrier (UP R)" using assms UP_ring_subring_car by blast have0: "a β carrier R" using assms subringE(1) by blast have1: "compose R (up_ring.monom (UP R) a n) g = a β R (g[^] Rn)" using monom_sub[of a g n] unfolding P_def using"0" assms(2) g_closed by blast have2: "compose (R(carrier := S)) (up_ring.monom (UP (R(carrier := S))) a n) g = a β(R(carrier := S)) g [^] (R(carrier := S)) n" using assms UP_cring.monom_sub[of "R ( carrier := S )" a g n] UP_ring_subring[of S] R.carrier_update[of S] by blast have3: " g [^] (R(carrier := S)) n = g[^] Rn" using UP_ring_subring_nat_pow[of S g n] by (simp add: assms(1) assms(2)) have4: "a β R (g[^] Rn) = a β (R(carrier := S)) g [^] (R(carrier := S)) n" prooffix x show"(a β R g [^] R n) x = (a β (R(carrier := S)) g [^] (R(carrier := S)) n) x" proof- have LHS: "(a β R g [^] R n) x = a β ((g [^] R n) x)" using"0" P.nat_pow_closed P_def cfs_smult g_closed by auto have RHS: "(a β (R(carrier := S)) g [^] (R(carrier := S)) n) x = a β(carrier := S) ((g [^] (R(carrier := S)) n) x)" proof- have"Group.monoid (UP (R(carrier := S))) " using assms UP_ring_subring[of S] UP_ring.UP_ring[of "R(carrier := S)"] ring.is_monoid byblast hence0 : " g [^] (R(carrier := S)) n β carrier (UP (R(carrier := S)))" using monoid.nat_pow_closed[of "UP (R ( carrier := S ))" g n] assms UP_ring_subring unfolding UP_ring_def ring_def by blast have1: "g [^] (R(carrier := S)) n β carrier (UP (R(carrier := S)))" using assms UP_ring_subring[of S] R.carrier_update[of S] 0by blast thenshow ?thesis using UP_ring.cfs_smult UP_ring_subring assms by (simp add: UP_ring.cfs_smult) qed show ?thesis using R.carrier_update RHS LHS 3 assms by simp qed qed show ?thesis using01234 by simp qed
lemma(in UP_cring) UP_subring_compose: assumes"subring S R" assumes"g β carrier (UP R)" assumes"f β carrier (UP R)" assumes"β§n. g n β S" assumes"β§n. f n β S" shows"compose R f g = compose (R ( carrier := S )) f g" proof- have g_closed: "g β carrier (UP (R ( carrier := S )))" using assms poly_cfs_subring by blast have0: "β§n. (β h. h β carrier (UP R) β§ deg R h β€ n β§ h β carrier (UP (R ( carrier := S ))) βΆ compose R h g = compose (R ( carrier := S )) h g)" proof- fix n show"(β h. h β carrier (UP R) β§ deg R h β€ n β§ h β carrier (UP (R ( carrier := S ))) βΆ compose R h g = compose (R ( carrier := S )) h g)" proof(induction n) show"βh. h β carrier (UP R) β§ deg R h β€ 0 β§ h β carrier (UP (R(carrier := S))) βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" prooffix h show"h β carrier (UP R) β§ deg R h β€ 0 β§ h β carrier (UP (R(carrier := S))) βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" proof assume A: "h β carrier (UP R) β§ deg R h β€ 0 β§ h β carrier (UP (R(carrier := S)))" thenhave0: "deg R h = 0" by linarith thenhave1: "deg (R ( carrier := S )) h = 0" using A assms UP_ring_subring_deg[of S h] by linarith show"Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" using01 g_closed assms sub_const[of g h] UP_cring.sub_const[of "R(carrier := S)" g h] A P_def UP_ring_subring by presburger qed qed show"β§n. βh. h β carrier (UP R) β§ deg R h β€ n β§ h β carrier (UP (R(carrier := S)))βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g ==> βh. h β carrier (UP R) β§ deg R h β€ Suc n β§ h β carrier (UP (R(carrier := S))) βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" prooffix n h assume IH: "βh. h β carrier (UP R) β§ deg R h β€ n β§ h β carrier (UP (R(carrier := S))) βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" show"h β carrier (UP R) β§ deg R h β€ Suc n β§ h β carrier (UP (R(carrier := S))) βΆ Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" proofassume A: "h β carrier (UP R) β§ deg R h β€ Suc n β§ h β carrier (UP (R(carrier := S)))" show"Cring_Poly.compose R h g = Cring_Poly.compose (R(carrier := S)) h g" proof(cases "deg R h β€ n") case True thenshow ?thesis using A IH by blast next case False thenhave F0: "deg R h = Suc n" using A by (simp add: A le_Suc_eq) thenhave F1: "deg (R(carrier := S)) h = Suc n" using UP_ring_subring_deg[of S h] A by (simp add: βΉh β carrier (UP R) β§ deg R h β€ Suc n β§ h β carrier (UP (R(carrier := S)))βΊ assms(1)) obtain j where j_def: "j β carrier (UP (R(carrier := S))) β§ h = j β (R(carrier := S)) up_ring.monom (UP (R(carrier := S))) (h (deg (R(carrier := S)) h)) (deg (R(carrier := S)) h) β§ deg (R(carrier := S)) j < deg (R(carrier := S)) h" using A UP_ring.ltrm_decomp[of "R(carrier := S)" h] assms UP_ring_subring[of S]
F1 by (metis (mono_tags, lifting) F0 False zero_less_Suc) have j_closed: "j β carrier (UP R)" using j_def assms UP_ring_subring_car_subset by blast have F2: "deg R j < deg R h" using j_def assms by (metis (no_types, lifting) F0 F1 UP_ring_subring_deg) have F3: "(deg (R(carrier := S)) h) = deg R h" by (simp add: F0 F1) have F30: "h (deg (R(carrier := S)) h) β S " using A UP_cring.UP_car_memE[of "R(carrier := S)" h "deg (R(carrier := S)) h"] by (metis R.carrier_update(1) UP_ring_subring(1) assms(1)) hence F4: "up_ring.monom P (h (deg R h)) (deg R h) = up_ring.monom (UP (R(carrier := S))) (h (deg (R(carrier := S)) h)) (deg (R(carrier := S)) h)" using F3 g_closed j_def UP_subring_monom[of S "h (deg (R(carrier := S)) h)"] assms unfolding P_def by metis have F5: "compose R (up_ring.monom (UP R) (h (deg R h)) (deg R h)) g = compose (R ( carrier := S )) (up_ring.monom (UP (R ( carrier := S ))) (h (deg (R(carrier := S)) h)) (deg (R(carrier := S)) h)) g" using F0 F1 F2 F3 F4 UP_subring_compose_monom[of S] assms P_def βΉh (deg (R(carrier := S)) h)β SβΊ by (metis g_closed) have F5: "compose R j g = compose (R ( carrier := S )) j g" using F0 F2 IH UP_ring_subring_car_subset' assms(1) j_def by auto have F6: "h = j β R monom (UP R) (h (deg R h)) (deg R h)" using j_def F4 UP_ring_subring_add[of S j "up_ring.monom (UP (R(carrier := S))) (h (deg (R(carrier := S)) h)) (deg (R(carrier := S)) h)"]
UP_ring.monom_closed[of "R(carrier := S)""h (deg (R(carrier := S)) h)""deg (R(carrier := S)) h"] using P_def UP_ring_subring(2) βΉh (deg (R(carrier := S)) h) β SβΊ assms(1) by auto have F7: "compose R h g =compose R j g β R compose R (up_ring.monom (UP R) (h (deg R h)) (deg R h)) g" proof- show ?thesis using assms(2) j_closed F5 sub_add[of g j "up_ring.monom P (h (deg R h)) (deg R h)" ]
F4 F3 F2 F1 g_closed unfolding P_def by (metis A F6 ltrm_closed P_def) qed have F8: "compose (R ( carrier := S )) h g = compose (R ( carrier := S )) j g β (R ( carrier := S )) compose (R ( carrier := S )) (up_ring.monom (UP (R ( carrier := S ))) (h (deg (R ( carrier := S )) h)) (deg (R ( carrier := S )) h)) g" proof- have0: " UP_cring (R(carrier := S))" by (simp add: UP_ring_subring(1) assms(1)) have1: "monom (UP (R(carrier := S))) (h (deg R h)) (deg R h) β carrier (UP (R(carrier := S)))" using assms 0 F30 UP_ring.monom_closed[of "R(carrier := S)""h (deg R h)""deg R h"] R.carrier_update[of S] unfolding UP_ring_def UP_cring_def by (simp add: F3 cring.axioms(1)) show ?thesis using01 g_closed j_def UP_cring.sub_add[of "R ( carrier := S )" g j "monom (UP (R(carrier := S))) (h (deg R h)) (deg R h)" ] using F3 by auto qed have F9: "compose R j g β carrier (UP R)" by (simp add: UP_cring.sub_closed assms(2) is_UP_cring j_closed) have F10: "compose (R ( carrier := S )) j g β carrier (UP (R ( carrier := S )))" using assms j_def UP_cring.sub_closed[of "R ( carrier := S )"] UP_ring_subring(1) g_closed by blast have F11: " compose R (up_ring.monom (UP R) (h (deg R h)) (deg R h)) g β carrier (UP R)" using assms j_def UP_cring.sub_closed[of "R ( carrier := S )"]
UP_ring.monom_closed[of "R ( carrier := S )"] by (simp add: A UP_car_memE(1) UP_cring.rev_sub_closed UP_ring.monom_closed is_UP_cring is_UP_ring sub_rev_sub) have F12: " compose (R ( carrier := S )) (up_ring.monom (UP (R ( carrier := S ))) (h (deg (R ( carrier := S )) h)) (deg (R ( carrier := S )) h)) g β carrier (UP (R ( carrier := S )))" using assms j_def UP_cring.sub_closed[of "R ( carrier := S )"]
UP_ring.monom_closed[of "R ( carrier := S )"] UP_ring_subring[of S] using A UP_ring.ltrm_closed g_closed by fastforce show ?thesis using F9 F10 F11 F12 F7 F8 F5 UP_ring_subring_add[of S "compose R j g""compose R (up_ring.monom (UP R) (h (deg R h)) (deg R h)) g"]
assms using F3 F30 UP_subring_compose_monom g_closed by auto qed qed qed qed qed show ?thesis using0[of "deg R f"] by (simp add: assms(1) assms(3) assms(5) poly_cfs_subring) qed
subsectionβΉEvaluation over a SubringβΊ
lemma(in UP_cring) UP_subring_eval: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"to_function R g a = to_function (R ( carrier := S )) g a" apply(rule UP_ring.poly_induct3[of "R ( carrier := S )" g] ) apply (simp add: UP_ring_subring(2) assms(1)) apply (simp add: assms(2)) proof- show"β§p q. q β carrier (UP (R(carrier := S))) ==> p β carrier (UP (R(carrier := S))) ==> to_function R p a = to_function (R(carrier := S)) p a ==> to_function R q a = to_function (R(carrier := S)) q a ==> to_function R (p β (R(carrier := S)) q) a = to_function (R(carrier := S)) (p β (R(carrier := S)) q) a" proof- fix p q assume A: "q β carrier (UP (R(carrier := S)))" "p β carrier (UP (R(carrier := S)))" " to_function R p a = to_function (R(carrier := S)) p a" " to_function R q a = to_function (R(carrier := S)) q a" have a_closed: "a β carrier R" using assms R.carrier_update[of S] subringE(1) by blast have0: "UP_cring (R(carrier := S))" using assms by (simp add: UP_ring_subring(1)) have1: "to_function (R(carrier := S)) p a β S" using A 0 UP_cring.to_fun_closed[of "R(carrier := S)"] by (simp add: UP_cring.to_fun_def assms(3)) have2: "to_function (R(carrier := S)) q a β S" using A 0 UP_cring.to_fun_closed[of "R(carrier := S)"] by (simp add: UP_cring.to_fun_def assms(3)) have3: "p β carrier (UP R)" using A assms 0 UP_ring_subring_car_subset' by blast have4: "q β carrier (UP R)" using A assms 0 UP_ring_subring_car_subset' by blast have5: "to_fun p a β to_fun q a = UP_cring.to_fun (R(carrier := S)) p a β(carrier := S) UP_cring.to_fun (R(carrier := S)) q a" using12 A R.carrier_update[of S] assms by (simp add: "0" UP_cring.to_fun_def to_fun_def) have6: "UP_cring.to_fun (R(carrier := S)) (p β (R(carrier := S)) q) a = UP_cring.to_fun (R(carrier := S)) p a β(carrier := S) UP_cring.to_fun (R(carrier := S)) q a" using UP_cring.to_fun_plus[of "R ( carrier := S )" q p a] by (simp add: "0" A(1) A(2) assms(3)) have7: "to_fun (p β q) a = to_fun p a β to_fun q a" using to_fun_plus[of q p a] 34 a_closed by (simp add: P_def) have8: "p β (R(carrier := S)) q = p β q" unfolding P_def using assms A R.carrier_update[of S] UP_ring_subring_add[of S p q] by simp show"to_function R (p β (R(carrier := S)) q) a = to_function (R(carrier := S)) (p β(R(carrier := S)) q) a" using UP_ring_subring_car_subset'[of S ] 012345678 A R.carrier_update[of S] unfolding P_def by (simp add: UP_cring.to_fun_def to_fun_def) qed show"β§b n. b β carrier (R(carrier := S)) ==> to_function R (monom (UP (R(carrier := S))) b n) a = to_function (R(carrier := S)) (monom (UP (R(carrier := S))) b n) a" proof- fix b n assume A: "b β carrier (R(carrier := S))" have0: "UP_cring (R(carrier := S))" by (simp add: UP_ring_subring(1) assms(1)) have a_closed: "a β carrier R" using assms subringE by blast have1: "UP_cring.to_fun (R(carrier := S)) (monom (UP (R(carrier := S))) b n) a = b β(carrier := S) a [^](carrier := S) n" using assms A UP_cring.to_fun_monom[of "R(carrier := S)" b a n] by (simp add: "0") have2: "UP_cring.to_fun (R(carrier := S)) (monom (UP (R(carrier := S))) b n) β‘ to_function (R(carrier := S)) (monom (UP (R(carrier := S))) b n)" using UP_cring.to_fun_def[of "R(carrier := S)""monom (UP (R(carrier := S))) b n"] 0by linarith have3: "(monom (UP (R(carrier := S))) b n) = monom P b n" using A assms unfolding P_def using UP_subring_monom by auto have4: " b β a [^] n = b β(carrier := S) a [^](carrier := S) n" apply(induction n) using R.carrier_update[of S] apply simp using R.carrier_update[of S] R.nat_pow_consistent by auto hence5: "to_function R (monom (UP (R(carrier := S))) b n) a = b β(carrier := S) a[^](carrier := S)n" using0123 assms A UP_cring.to_fun_monom[of "R(carrier := S)" b a n] UP_cring.to_fun_def[of "R(carrier := S)""monom (UP (R(carrier := S))) b n"]
R.carrier_update[of S] subringE[of S R] a_closed UP_ring.monom_closed[of "R(carrier := S)" a n]
to_fun_monom[of b a n] unfolding P_def UP_cring.to_fun_def to_fun_def by (metis subsetD) thus" to_function R (monom (UP (R(carrier := S))) b n) a = to_function (R(carrier := S)) (monom (UP (R(carrier := S))) b n) a" using"1""2"by auto qed qed
lemma(in UP_cring) UP_subring_eval': assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"to_fun g a = to_function (R ( carrier := S )) g a" unfolding to_fun_def using assms by (simp add: UP_subring_eval)
lemma(in UP_cring) UP_subring_eval_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"to_fun g a β S" using assms UP_subring_eval'[of S g a] UP_cring.to_fun_closed UP_cring.to_fun_def R.carrier_update(1) UP_ring_subring(1) by fastforce
subsectionβΉDerivatives and Taylor Expansions over a SubringβΊ
lemma(in UP_cring) UP_subring_taylor: assumes"subring S R" assumes"g β carrier (UP R)" assumes"β§n. g n β S" assumes"a β S" shows"taylor_expansion R a g = taylor_expansion (R ( carrier := S )) a g" proof- have a_closed: "a β carrier R" using assms subringE by blast have0: "X_plus a β carrier (UP R)" using assms X_plus_closed unfolding P_def usinglocal.a_closed by auto have1: "β§n. X_plus a n β S" proof- fix n have"X_plus a n = (if n = 0 then a else (if n = 1 then 1 else 0))" using a_closed by (simp add: cfs_X_plus) thenshow"X_plus a n β S"using subringE assms by (simp add: subringE(2) subringE(3)) qed have2: "(X_poly_plus (R(carrier := S)) a) = X_plus a" proof- have20: "(X_poly_plus (R(carrier := S)) a) = (λk. if k = (0::nat) then a else (if k = 1 then 1 else 0))" using a_closed assms UP_cring.cfs_X_plus[of "R(carrier := S)" a] R.carrier_update
UP_ring_subring(1) by auto have21: "X_plus a = (λk. if k = (0::nat) then a else (if k = 1 then 1 else 0))" using cfs_X_plus[of a] a_closed by blast show ?thesis apply(rule ext) using2021 by auto qed show ?thesis unfolding taylor_expansion_def using012 assms UP_subring_compose[of S g "X_plus a"] by (simp add: UP_subring_compose) qed
lemma(in UP_cring) UP_subring_taylor_closed: assumes"subring S R" assumes"g β carrier (UP R)" assumes"β§n. g n β S" assumes"a β S" shows"taylor_expansion R a g β carrier (UP (R ( carrier := S )))" proof- have"g β carrier (UP (R(carrier := S)))" by (metis P_def R.carrier_update(1) R.carrier_update(2) UP_cring.UP_car_memI' UP_ring_subring(1) assms(1) assms(2) assms(3) deg_leE) thenshow ?thesis using assms UP_cring.taylor_def[of "R(carrier := S)"] UP_subring_taylor[of S g a]
UP_cring.taylor_closed[of "R ( carrier := S )" g a] UP_ring_subring(1)[of S] by simp qed
lemma(in UP_cring) UP_subring_taylor_closed': assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"taylor_expansion R a g β carrier (UP (R ( carrier := S )))" using UP_subring_taylor_closed assms UP_cring.UP_car_memE[of "R ( carrier := S )" g] R.carrier_update[of S]
UP_ring_subring(1) UP_ring_subring_car_subset' by auto
lemma(in UP_cring) UP_subring_taylor': assumes"subring S R" assumes"g β carrier (UP R)" assumes"β§n. g n β S" assumes"a β S" shows"taylor_expansion R a g n β S" using assms UP_subring_taylor R.carrier_update[of S] UP_cring.taylor_closed[of "R ( carrier := S )"] using UP_cring.taylor_expansion_cf_closed UP_ring_subring(1) poly_cfs_subring by metis
lemma(in UP_cring) UP_subring_deriv: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"deriv g a= UP_cring.deriv (R ( carrier := S )) g a" proof- have0: "(β§n. g n β S)" using assms UP_ring_subring_car by blast thus ?thesis unfolding derivative_def using0 UP_ring_subring_car_subset[of S] assms UP_subring_taylor[of S g a] by (simp add: subset_iff) qed
lemma(in UP_cring) UP_subring_deriv_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" shows"deriv g a β S" using assms UP_cring.deriv_closed[of "R ( carrier := S )" g a] UP_subring_deriv[of S g a]
UP_ring_subring_car_subset[of S] UP_ring_subring[of S] by simp
lemma(in UP_cring) poly_shift_subring_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" shows"poly_shift g β carrier (UP (R ( carrier := S )))" using UP_cring.poly_shift_closed[of "R ( carrier := S )" g] assms UP_ring_subring[of S] by simp
lemma(in UP_cring) UP_subring_taylor_appr: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" assumes"b β S" shows"βc β S. to_fun g a= to_fun g b β (deriv g b)β (a β b) β (c β (a β b)[^](2::nat))" proof- have a_closed: "a β carrier R" using assms subringE by blast have b_closed: "b β carrier R" using assms subringE by blast have g_closed: " g β carrier (UP R)" using UP_ring_subring_car_subset[of S] assms by blast have0: "to_fun (shift 2 (T g)) (a β b) = to_fun (shift 2 (T g)) (a β b)" by simp have1: "to_fun g b = to_fun g b" by simp have2: "deriv g b = deriv g b" by simp have3: "to_fun g a = to_fun g b β deriv g b β (a β b) β to_fun (shift 2 (T g)) (aβ b) β (a β b) [^] (2::nat)" using taylor_deg_1_expansion[of g b a "to_fun (shift 2 (T g)) (a β b)""to_fun g b""deriv g b"]
assms a_closed b_closed g_closed 012unfolding P_def by blast have4: "to_fun (shift 2 (T g)) (a β b) β S" proof- have0: "(2::nat) = Suc (Suc 0)" by simp have1: "a β b β S" using assms unfolding a_minus_def by (simp add: subringE(5) subringE(7)) have2: "poly_shift (T g) β carrier (UP (R(carrier := S)))" using poly_shift_subring_closed[of S "taylor_expansion R b g"] UP_ring_subring[of S]
UP_subring_taylor_closed'[of S g b] assms unfolding taylor_def by blast hence3: "poly_shift (poly_shift (T g)) β carrier (UP (R(carrier := S)))" using UP_cring.poly_shift_closed[of "R(carrier := S)""(poly_shift (T g))"] unfolding taylor_def using assms(1) poly_shift_subring_closed by blast have4: "to_fun (poly_shift (poly_shift (T g))) (a β b) β S" using1230 UP_subring_eval_closed[of S "poly_shift (poly_shift (T g))""a β b"]
UP_cring.poly_shift_closed[of "R(carrier := S)"] assms by blast thenshow ?thesis by (simp add: numeral_2_eq_2) qed obtain c where c_def: "c = to_fun (shift 2 (T g)) (a β b)" by blast have5: "c β S β§ to_fun g a = to_fun g b β deriv g b β (a β b) β c β (a β b) [^] (2::nat)" unfolding c_def using34by blast thus ?thesis using c_def 4by blast qed
lemma(in UP_cring) UP_subring_taylor_appr': assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" assumes"a β S" assumes"b β S" shows"βc c' c''. c β S β§ c' β S β§ c'' β S β§ to_fun g a= c β c'β (a β b) β (c'' β (a β b)[^](2::nat))" using UP_subring_taylor_appr[of S g a b] assms UP_subring_deriv_closed[of S g b] UP_subring_eval_closed[of S g b] by blast
lemma (in UP_cring) pderiv_cfs: assumes"g β carrier (UP R)" shows"pderiv g n = [Suc n]β (g (Suc n))" unfolding pderiv_def using n_mult_closed[of g] assms poly_shift_cfs[of "n_mult g" n] unfolding P_def n_mult_def by blast
lemma(in ring) subring_add_pow: assumes"subring S R" assumes"a β S" shows"[(n::nat)] β (carrier := S) a = [(n::nat)] β a" proof- have0: "a β carrier R" using assms(1) assms(2) subringE(1) by blast have1: "a β carrier (R(carrier := S))" by (simp add: assms(2)) show ?thesis apply(induction n) using assms 01 carrier_update[of S] apply (simp add: add_pow_def) using assms 01 carrier_update[of S] by (simp add: add_pow_def) qed
lemma(in UP_cring) UP_subring_pderiv_equal: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" shows"pderiv g = UP_cring.pderiv (R(carrier := S)) g" prooffix n show"pderiv g n = UP_cring.pderiv (R(carrier := S)) g n" using UP_cring.pderiv_cfs[of "R ( carrier := S )" g n] pderiv_cfs[of g n]
assms R.subring_add_pow[of S "g (Suc n)""Suc n"] by (simp add: UP_ring_subring(1) UP_ring_subring_car) qed
lemma(in UP_cring) UP_subring_pderiv_closed: assumes"subring S R" assumes"g β carrier (UP (R ( carrier := S )))" shows"pderiv g β carrier (UP (R ( carrier := S )))" using assms UP_cring.pderiv_closed[of "R ( carrier := S )" g] R.carrier_update(1) UP_ring_subring(1)
UP_subring_pderiv_equal by auto
lemma(in UP_cring) UP_subring_pderiv_closed': assumes"subring S R" assumes"g β carrier (UP R)" assumes"β§n. g n β S" shows"β§n. pderiv g n β S" using assms UP_subring_pderiv_closed[of S g] poly_cfs_subring[of S g] UP_ring_subring_car by blast
lemma(in UP_cring) taylor_deg_one_expansion_subring: assumes"f β carrier (UP R)" assumes"subring S R" assumes"β§i. f i β S" assumes"a β S" assumes"b β S" shows"βc β S. to_fun f b = (to_fun f a) β (deriv f a) β (b β a) β (c β (b β a)[^](2::nat))" apply(rule UP_subring_taylor_appr, rule assms) using assms poly_cfs_subring apply blast by(rule assms, rule assms)
lemma(in UP_cring) taylor_deg_one_expansion_subring': assumes"f β carrier (UP R)" assumes"subring S R" assumes"β§i. f i β S" assumes"a β S" assumes"b β S" shows"βc β S. to_fun f b = (to_fun f a) β (to_fun (pderiv f) a) β (b β a) β (c β (b β a)[^](2::nat))" proof- have"S β carrier R" using assms subringE(1) by blast hence0: "deriv f a = to_fun (pderiv f) a" using assms pderiv_eval_deriv[of f a] unfolding P_def by blast show ?thesis using assms taylor_deg_one_expansion_subring[of f S a b] unfolding0by blast qed
end
Messung V0.5 in Prozent
Β€ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfΓ€ltig zusammengestellt. Es wird jedoch weder VollstΓ€ndigkeit, noch Richtigkeit,
noch QualitΓ€t der bereit gestellten Informationen zugesichert.1.403Bemerkung:
(vorverarbeitet am 2026-07-02)
Β€
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfΓ€ltig zusammengestellt. Es wird jedoch weder VollstΓ€ndigkeit, noch Richtigkeit,
noch QualitΓ€t der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.