|
|
|
|
Impressum Cring_Poly.thy
Sprache: Isabelle
|
|
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"
have 0: "h ∈ ring_hom R S ∧ F ∈ A → carrier R "
using A by auto
have 1: "h (finsum R F A) = finsum S (h ∘ F) A"
using A 0 by auto
have 2: "abelian_monoid S"
using assms ring_def abelian_group_def by auto
have 3: "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
have 4: "finsum R F (insert a A) = F a ⊕ finsum R F A"
using finsum_insert[of A a F] A assms by auto
have 5: "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)"
unfolding 4 5 3 by 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)
then show ?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))
then have "f (x ⊗ y) = g ((h x) ⊗ (h y))"
using A(1) A(2) assms(4) ring_hom_mult by fastforce
then have "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
then show ?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))
then have "f (x ⊕ y) = g ((h x) ⊕ (h y))"
using A(1) A(2) assms(4) ring_hom_add by fastforce
then have "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)
then show ?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)
then show ?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
then show ?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 "
proof fix 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-
have 0: "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 "
then have 1: "degree (f ⊕ g) < n"
using 0 by auto
have 2: "degree (⊖ f) < n"
using assms by simp
have 3: "g = (f ⊕ g) ⊕ (⊖ f)"
using assms
by (simp add: P.add.m_comm P.r_neg1)
then show False using 1 2 3 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_sum_diff_degree:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree q < degree p"
shows "degree (p ⊕ q) = degree p"
by(rule equal_deg_sum', auto simp: assms)
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))
then show ?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›
lemma deg_ltrm:
assumes "f ∈ carrier P"
shows "degree (ltrm f) = degree f"
using assms
by (metis P_def UP_ring.lcoeff_nonzero_deg UP_ring_axioms cfs_closed coeff_simp deg_const deg_monom)
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))
then have "f m = (ltrm f) m"
using ltrm_cfs assms(1) by auto
then have "(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
then have "(f ⊖ R ltrm f) m = 0"
by (metis C1 ltrm_closed P_def assms(1) coeff_minus coeff_simp)
then show ?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
then show ?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-
have 0: "f ⊖ (ltrm f) ∈ carrier P"
using ltrm_closed assms(1) by blast
have 1: "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 0 1 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 coeff_of_sum_diff_degree1:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree q < degree p"
shows "(p ⊕ q) (degree p) = p (degree p)"
using assms(1) assms(2) assms(3) coeff_of_sum_diff_degree0 by blast
lemma ltrm_of_sum_diff_degree:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree p > degree q"
shows "ltrm (p ⊕ q) = ltrm p"
unfolding leading_term_def
using assms(1) assms(2) assms(3) coeff_of_sum_diff_degree1 degree_of_sum_diff_degree
by presburger
text‹leading term of a monomial›
lemma ltrm_monom:
assumes "a ∈ carrier R"
assumes "f = monom P a n"
shows "ltrm f = f"
unfolding leading_term_def
by (metis P_def UP_ring.cfs_monom UP_ring.monom_zero UP_ring_axioms assms(1) assms(2) deg_monom)
lemma ltrm_monom_simp:
assumes "a ∈ carrier R"
shows "ltrm (monom P a n) = monom P a n"
using assms ltrm_monom by auto
lemma ltrm_inv_simp[simp]:
assumes "f ∈ carrier P"
shows "ltrm (ltrm f) = ltrm f"
by (metis assms deg_ltrm ltrm_cfs)
lemma ltrm_deg_0:
assumes "p ∈ carrier P"
assumes "degree p = 0"
shows "ltrm p = p"
using ltrm_monom assms P_def UP_ring.deg_zero_impl_monom UP_ring_axioms coeff_simp
by fastforce
lemma ltrm_prod_ltrm:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "ltrm ((ltrm p) ⊗ (ltrm q)) = (ltrm p) ⊗ (ltrm q)"
using ltrm_monom R.m_closed assms(1) assms(2) cfs_closed monom_mult
by metis
text‹lead coefficient function›
abbreviation(input) lcf where
"lcf p ≡ p (deg R p)"
lemma(in UP_ring) lcf_ltrm:
"ltrm p = monom P (lcf p) (degree p)"
by auto
lemma lcf_closed:
assumes "f ∈ carrier P"
shows "lcf f ∈ carrier R"
by (simp add: assms cfs_closed)
lemma(in UP_cring) lcf_monom:
assumes "a ∈ carrier R"
shows "lcf (monom P a n) = a" "lcf (monom (UP R) a n) = a"
using assms deg_monom cfs_monom apply fastforce
by (metis UP_ring.cfs_monom UP_ring.deg_monom UP_ring_axioms assms)
end
text‹Function which truncates a polynomial by removing the leading term›
definition truncate where
"truncate R f = f ⊖UP R) (leading_term R f)"
context UP_ring
begin
abbreviation(input) trunc where
"trunc ≡ truncate R"
lemma trunc_closed:
assumes "f ∈ carrier P"
shows "trunc f ∈ carrier P"
using assms unfolding truncate_def
by (metis ltrm_closed P_def UP_ring.UP_ring UP_ring_axioms leading_term_def ring.ring_simprules(4))
lemma trunc_simps:
assumes "f ∈ carrier P"
shows "f = (trunc f) ⊕ (ltrm f)"
"f ⊖ (trunc f) = ltrm f"
apply (metis ltrm_closed P.add.inv_solve_right P.minus_closed P_def a_minus_def assms Cring_Poly.truncate_def leading_term_def)
using trunc_closed[of f] ltrm_closed[of f] P_def P.add.inv_solve_right[of "ltrm f" f "trunc f"]
assms unfolding UP_cring_def
by (metis P.add.inv_closed P.add.m_lcomm P.add.r_inv_ex P.minus_eq P.minus_minus
P.r_neg2 P.r_zero Cring_Poly.truncate_def leading_term_def)
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 is_UP_monomE:
assumes "is_UP_monom f"
shows "f ∈ carrier P" "f = monom P (lcf f) (degree f)" "f = monom (UP R) (lcf f) (degree f)"
using assms unfolding is_UP_monom_def
by(auto simp: P_def )
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
then have "q ⊗ p = (trunc q ⊕ ltrm q) ⊗ (trunc p ⊕ ltrm p)"
by linarith
then have 0: "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)
have 1: "(trunc q ⊗ (trunc p ⊕ ltrm p)) (degree p + degree q) = 0"
proof(cases "degree q = 0")
case True
then show ?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
then have "degree (trunc q ⊗ (trunc p ⊕ ltrm p)) < degree q + degree p"
using False assms(1) assms(2) trunc_degree trunc_simps(1) by fastforce
then show ?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
have 2: "(q ⊗ p) (degree p + degree q) =
( ltrm q ⊗ (trunc p ⊕ ltrm p)) (degree p + degree q)"
using 0 1 assms cfs_closed trunc_closed by auto
have 3: "(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)
have 4: "( ltrm q ⊗ trunc p) (degree p + degree q) = 0"
proof(cases "degree p = 0")
case True
then show ?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
then have "degree ( ltrm q ⊗ trunc p) < degree q + degree p"
using False assms(1) assms(2) trunc_degree trunc_simps(1) deg_ltrm by fastforce
then show ?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
have 5: "(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)
have 6: "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)
have 7: "( ltrm q ⊗ ltrm p) (degree p + degree q) ≠0"
using 5 6 assms
by (metis R.m_closed cfs_closed cfs_monom)
have 8: "degree (q ⊗ p) ≥degree p + degree q"
using 5 6 7 P_def UP_mult_closed assms(1) assms(2)
by (simp add: UP_ring.coeff_simp UP_ring_axioms deg_belowI)
then show ?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-
have 0: "degree (monom P a n) = n"
by (simp add: assms(2) assms(3))
have 1: "(monom P a n) ∈ carrier P"
using assms(2) by auto
have 2: "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
then show ?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(in UP_cring) deg_zero_ltrm_smult_cring:
assumes "p ∈ carrier P"
assumes "a ∈ carrier R"
assumes "degree p = 0"
shows "ltrm (a ⊙p) = a⊙(ltrm p)"
by (metis ltrm_deg_0 assms(1) assms(2) assms(3) deg_smult_decr le_0_eq module.smult_closed module_axioms)
lemma(in UP_domain) ltrm_smult:
assumes "p ∈ carrier P"
assumes "a ∈ carrier R"
shows "ltrm (a ⊙p) = a⊙(ltrm p)"
by (metis lcf_closed ltrm_closed ltrm_smult_cring P_def R.integral_iff UP_ring.deg_ltrm
UP_ring_axioms UP_smult_zero assms(1) assms(2) cfs_zero deg_nzero_nzero deg_zero_ltrm_smult_cring monom_zero)
lemma(in UP_cring) cring_ltrm_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "lcf p ⊗ lcf q ≠ 0"
shows "ltrm (p ⊗ q) = (ltrm p) ⊗ (ltrm q)"
proof(cases "degree p = 0 ∨ degree q = 0")
case True
then show ?thesis
by (smt (verit) ltrm_closed ltrm_deg_0 ltrm_smult_cring R.m_comm UP_m_comm assms(1) assms(2) assms(3) cfs_closed monom_mult_is_smult)
next
case False
obtain q0 where q0_def: "q0 = trunc q"
by simp
obtain p0 where p0_def: "p0 = trunc p"
by simp
have Pq: "degree q0 < degree q"
using False P_def assms(2) q0_def trunc_degree by blast
have Pp: "degree p0 < degree p"
using False P_def assms(1) p0_def trunc_degree by blast
have "p ⊗ q = (p0 ⊕ ltrm(p)) ⊗ (q0 ⊕ ltrm(q))"
using assms(1) assms(2) p0_def q0_def trunc_simps(1) by auto
then have P0: "p ⊗ q = ((p0 ⊕ ltrm(p)) ⊗ q0) ⊕ ((p0 ⊕ ltrm(p))⊗ ltrm(q))"
by (simp add: P.r_distr assms(1) assms(2) ltrm_closed p0_def q0_def trunc_closed)
have P1: "degree ((p0 ⊕ ltrm(p)) ⊗ q0) < degree ((p0 ⊕ ltrm(p))⊗ ltrm(q))"
proof-
have LHS: "degree ((p0 ⊕ ltrm(p)) ⊗ q0) ≤ degree p + degree q0 "
proof(cases "q0 = 0")
case True
then show ?thesis
using assms(1) p0_def trunc_simps(1) by auto
next
case False
then show ?thesis
using assms(1) assms(2) deg_mult_ring p0_def
q0_def trunc_simps(1) trunc_closed by auto
qed
have RHS: "degree ((p0 ⊕ ltrm(p))⊗ ltrm(q)) = degree p + degree q"
using assms(1) assms(2) deg_mult_ring ltrm_closed p0_def trunc_simps(1)
by (smt (verit) P_def UP_cring.lcf_monom(1) UP_cring.cring_deg_mult UP_cring_axioms add.commute assms(3) cfs_closed deg_ltrm)
then show ?thesis
using RHS LHS Pq
by linarith
qed
then have P2: "ltrm (p ⊗ q) = ltrm ((p0 ⊕ ltrm(p))⊗ ltrm(q))"
using P0 P1
by (metis (no_types, lifting) ltrm_closed ltrm_of_sum_diff_degree P.add.m_comm
UP_mult_closed assms(1) assms(2) p0_def q0_def trunc_closed trunc_simps(1))
have P3: " ltrm ((p0 ⊕ ltrm(p))⊗ ltrm(q)) = ltrm p ⊗ ltrm q"
proof-
have Q0: "((p0 ⊕ ltrm(p))⊗ ltrm(q)) = (p0 ⊗ ltrm(q)) ⊕ (ltrm(p))⊗ ltrm(q)"
by (simp add: P.l_distr assms(1) assms(2) ltrm_closed p0_def trunc_closed)
have Q1: "degree ((p0 ⊗ ltrm(q)) ) < degree ((ltrm(p))⊗ ltrm(q))"
proof(cases "p0 = 0")
case True
then show ?thesis
using P1 assms(1) assms(2) ltrm_closed by auto
next
case F: False
then show ?thesis
proof-
have LHS: "degree ((p0 ⊗ ltrm(q))) < degree p + degree q"
using False F Pp assms(1) assms(2) deg_nzero_nzero
deg_ltrm ltrm_closed p0_def trunc_closed
by (smt (verit) add_le_cancel_right deg_mult_ring le_trans not_less)
have RHS: "degree ((ltrm(p))⊗ ltrm(q)) = degree p + degree q"
using cring_deg_mult[of "ltrm p" "ltrm q"] assms
by (simp add: ltrm_closed ltrm_cfs deg_ltrm)
then show ?thesis using LHS RHS by auto
qed
qed
have Q2: "ltrm ((p0 ⊕ ltrm(p))⊗ ltrm(q)) = ltrm ((ltrm(p))⊗ ltrm(q))"
using Q0 Q1
by (metis (no_types, lifting) ltrm_closed ltrm_of_sum_diff_degree P.add.m_comm
UP_mult_closed assms(1) assms(2) p0_def trunc_closed)
show ?thesis using ltrm_prod_ltrm Q0 Q1 Q2
by (simp add: assms(1) assms(2))
qed
then show ?thesis
by (simp add: P2)
qed
lemma(in UP_domain) ltrm_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "ltrm (p ⊗ q) = (ltrm p) ⊗ (ltrm q)"
using cring_ltrm_mult assms
by (smt (verit) ltrm_closed ltrm_deg_0 cfs_closed deg_nzero_nzero deg_ltrm local.integral_iff monom_mult monom_zero)
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 (in domain) nonzero_pow_nonzero:
assumes "a ∈ carrier R"
assumes "a ≠0"
shows "a[^](n::nat) ≠ 0"
proof(induction n)
case 0
then show ?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
then show ?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)
case 0
then show ?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)
have 0: "lcf (ltrm (p [^] n)) = lcf p [^] n"
unfolding a
by (simp add: lcf_monom(1) assms(1) cfs_closed monom_pow)
then have 1: "lcf (ltrm (p [^] n)) ⊗ lcf p ≠ 0"
using assms A R.nat_pow_Suc IH by metis
then show "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
then show ?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
then show ?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) cring_pow_deg_bound:
assumes "p ∈ carrier P"
shows "degree (p[^](n::nat)) ≤ n*degree p"
apply(induction n)
apply (metis Group.nat_pow_0 deg_one le_zero_eq mult_is_0)
using deg_mult_ring[of _ p]
by (smt (verit) P.nat_pow_Suc2 P.nat_pow_closed ab_semigroup_add_class.add_ac(1) assms deg_mult_ring le_iff_add mult_Suc)
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"
have 0: "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
then show 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)
case 0
then show ?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"
then show "∧ 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
then show ?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
then show ?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
then have 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 by auto
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
then show ?thesis using P5 P3 P2
by (simp add: A0 A1 degree_of_sum_diff_degree)
qed
qed
qed
qed
lemma(in UP_domain) pow_sum:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree q < degree p"
shows "degree ((p ⊕ q )[^]n) = (degree p)*n"
using assms(1) assms(2) assms(3) pow_sum0 by blast
lemma(in UP_domain) deg_pow0:
"∧ p. p ∈ carrier P ==> n ≥ degree p ==> degree (p [^] m) = m*(degree p)"
proof(induction n)
case 0
show "p ∈ carrier P ==> 0 ≥ degree p ==> degree (p [^] m) = m*(degree p)"
proof-
assume B0:"p ∈ carrier P"
assume B1: "0 ≥ degree p"
then obtain 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
then show ?thesis using IH A0 by simp
next
case False
then show ?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)
then show ?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))
then show ?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)
case 0
then show ?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"
then show "∧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-
have 0: "ltrm (f [^] n) = (ltrm f) [^] n"
using A IH by blast
have 1: "ltrm (f [^] (Suc n)) = ltrm ((f [^] n)⊗ f)"
by auto then
show ?thesis using ltrm_mult 0 1
by (simp add: A)
qed
qed
qed
lemma(in UP_domain) ltrm_pow:
assumes "f ∈ carrier P"
shows " ltrm (f [^] (n::nat)) = (ltrm f) [^] n"
using assms ltrm_pow0 by blast
text‹lemma on the leading coefficient›
lemma lcf_eq:
assumes "f ∈ carrier P"
shows "lcf f = lcf (ltrm f)"
using ltrm_deg_0
by (simp add: ltrm_cfs assms deg_ltrm)
lemma lcf_eq_deg_eq_imp_ltrm_eq:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree p > 0"
assumes "degree p = degree q"
assumes "lcf p = lcf q"
shows "ltrm p = ltrm q"
using assms(4) assms(5)
by (simp add: leading_term_def)
lemma ltrm_eq_imp_lcf_eq:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "ltrm p = ltrm q"
shows "lcf p = lcf q"
using assms
by (metis lcf_eq)
lemma ltrm_eq_imp_deg_drop:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "ltrm p = ltrm q"
assumes "degree p >0"
shows "degree (p ⊖ q) < degree p"
proof-
have P0: "degree p = degree q"
by (metis assms(1) assms(2) assms(3) deg_ltrm)
then have P1: "degree (p ⊖ q) ≤ degree p"
by (metis P.add.inv_solve_right P.minus_closed P.minus_eq assms(1)
assms(2) degree_of_sum_diff_degree neqE order.strict_implies_order order_refl)
have "degree (p ⊖ q) ≠ degree p"
proof
assume A: "degree (p ⊖ q) = degree p"
have Q0: "p ⊖ q = ((trunc p) ⊕ (ltrm p)) ⊖ ((trunc q) ⊕ (ltrm p))"
using assms(1) assms(2) assms(3) trunc_simps(1) by force
have Q1: "p ⊖ q = (trunc p) ⊖ (trunc q)"
proof-
have "p ⊖ q = ((trunc p) ⊕ (ltrm p)) ⊖ (trunc q) ⊖ (ltrm p)"
using Q0
by (simp add: P.minus_add P.minus_eq UP_a_assoc assms(1) assms(2) ltrm_closed trunc_closed)
then show ?thesis
by (metis (no_types, lifting) ltrm_closed P.add.inv_mult_group P.minus_eq
P.r_neg2 UP_a_assoc assms(1) assms(2) assms(3) carrier_is_submodule submoduleE(6) trunc_closed trunc_simps(1))
qed
have Q2: "degree (trunc p) < degree p"
by (simp add: assms(1) assms(4) trunc_degree)
have Q3: "degree (trunc q) < degree q"
using P0 assms(2) assms(4) trunc_degree by auto
then show False using A Q1 Q2 Q3 by (simp add: P.add.inv_solve_right
P.minus_eq P0 assms(1) assms(2) degree_of_sum_diff_degree trunc_closed)
qed
then show ?thesis
using P1 by auto
qed
lemma(in UP_cring) cring_lcf_scalar_mult:
assumes "p ∈ carrier P"
assumes "a ∈ carrier R"
assumes "a ⊗ (lcf p) ≠0"
shows "lcf (a ⊙ p) = a ⊗ (lcf p)"
proof-
have 0: "lcf (a ⊙ p) = lcf (ltrm (a ⊙ p))"
using assms lcf_eq smult_closed by blast
have 1: "degree (a ⊙ p) = degree p"
by (smt (verit) lcf_monom(1) P_def R.one_closed R.r_null UP_ring.coeff_smult UP_ring_axioms
assms(1) assms(2) assms(3) coeff_simp cring_deg_mult deg_const monom_closed monom_mult_is_smult smult_one)
then have "lcf (a ⊙ p) = lcf (a ⊙ (ltrm p))"
using lcf_eq[of "a ⊙ p"] smult_closed assms 0
by (metis cfs_closed cfs_smult monom_mult_smult)
then show ?thesis
unfolding leading_term_def
by (metis P_def R.m_closed UP_cring.lcf_monom UP_cring_axioms assms(1) assms(2) cfs_closed monom_mult_smult)
qed
lemma(in UP_domain) lcf_scalar_mult:
assumes "p ∈ carrier P"
assumes "a ∈ carrier R"
shows "lcf (a ⊙ p) = a ⊗ (lcf p)"
proof-
have "lcf (a ⊙ p) = lcf (ltrm (a ⊙ p))"
using lcf_eq UP_smult_closed assms(1) assms(2) by blast
then have "lcf (a ⊙ p) = lcf (a ⊙ (ltrm p))"
using ltrm_smult assms(1) assms(2) by metis
then show ?thesis
by (metis (full_types) UP_smult_zero assms(1) assms(2) cfs_smult cfs_zero deg_smult)
qed
lemma(in UP_cring) cring_lcf_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "(lcf p) ⊗ (lcf q) ≠0"
shows "lcf (p ⊗ q) = (lcf p) ⊗ (lcf q)"
using assms cring_ltrm_mult
by (smt (verit) lcf_monom(1) P.m_closed R.m_closed cfs_closed monom_mult)
lemma(in UP_domain) lcf_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "lcf (p ⊗ q) = (lcf p) ⊗ (lcf q)"
by (metis P_def R.integral_iff assms(1) assms(2) cfs_closed coeff_simp cring_lcf_mult lcoeff_nonzero local.integral_iff)
lemma(in UP_cring) cring_lcf_pow:
assumes "p ∈ carrier P"
assumes "(lcf p)[^]n ≠0"
shows "lcf (p[^](n::nat)) = (lcf p)[^]n"
by (smt (verit) P.nat_pow_closed R.nat_pow_closed assms(1) assms(2) cring_pow_ltrm lcf_closed lcf_ltrm lcf_monom monom_pow)
lemma(in UP_domain) lcf_pow:
assumes "p ∈ carrier P"
shows "lcf (p[^](n::nat)) = (lcf p)[^]n"
proof-
show ?thesis
proof(induction n)
case 0
then show ?case
by (metis Group.nat_pow_0 P_def R.one_closed UP_cring.lcf_monom UP_cring_axioms monom_one)
next
case (Suc n)
fix n
assume IH: "lcf (p[^](n::nat)) = (lcf p)[^]n"
show "lcf (p[^](Suc n)) = (lcf p)[^](Suc n)"
proof-
have "lcf (p[^](Suc n)) = lcf ((p[^]n) ⊗p)"
by simp
then have "lcf (p[^](Suc n)) = (lcf p)[^]n ⊗ (lcf p)"
by (simp add: IH assms lcf_mult)
then show ?thesis by auto
qed
qed
qed
end
(**************************************************************************************************)
(**************************************************************************************************)
subsection‹Constant Terms and Constant Coefficients›
(**************************************************************************************************)
(**************************************************************************************************)
text‹Constant term and coefficient function›
definition zcf where
"zcf f = (f 0)"
abbreviation(in UP_cring)(input) ctrm where
"ctrm f ≡ monom P (f 0) 0"
context UP_cring
begin
lemma ctrm_is_poly:
assumes "p ∈ carrier P"
shows "ctrm p ∈ carrier P"
by (simp add: assms cfs_closed)
lemma ctrm_degree:
assumes "p ∈ carrier P"
shows "degree (ctrm p) = 0"
by (simp add: assms cfs_closed)
lemma ctrm_zcf:
assumes "f ∈ carrier P"
assumes "zcf f = 0"
shows "ctrm f = 0"
by (metis P_def UP_ring.monom_zero UP_ring_axioms zcf_def assms(2))
lemma zcf_degree_zero:
assumes "f ∈ carrier P"
assumes "degree f = 0"
shows "lcf f = zcf f"
by (simp add: zcf_def assms(2))
lemma zcf_zero_degree_zero:
assumes "f ∈ carrier P"
assumes "degree f = 0"
assumes "zcf f = 0"
shows "f = 0"
using zcf_degree_zero[of f] assms ltrm_deg_0[of f]
by simp
lemma zcf_ctrm:
assumes "p ∈ carrier P"
shows "zcf (ctrm p) = zcf p"
unfolding zcf_def
using P_def UP_ring.cfs_monom UP_ring_axioms assms cfs_closed by fastforce
lemma ctrm_trunc:
assumes "p ∈ carrier P"
assumes "degree p >0"
shows "zcf(trunc p) = zcf p"
by (simp add: zcf_def assms(1) assms(2) trunc_cfs)
text‹Constant coefficient function is a ring homomorphism›
lemma zcf_add:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "zcf(p ⊕ q) = (zcf p) ⊕ (zcf q)"
by (simp add: zcf_def assms(1) assms(2))
lemma coeff_ltrm[simp]:
assumes "p ∈ carrier P"
assumes "degree p > 0"
shows "zcf(ltrm p) = 0"
by (metis ltrm_cfs_above_deg ltrm_cfs zcf_def assms(1) assms(2))
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)
case 0
then show ?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
then show ?thesis
using I A0 by auto
next
case False
then have D: "degree p = Suc n"
by (simp add: A1 nat_less_le)
then have "(∧q. q ∈ carrier P ==> degree q < degree p ==> Q q)"
using I by simp
then show "Q p"
using IH D A0 A1 Deg_0 by blast
qed
qed
qed
qed
then show ?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)
then show ?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
then have "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
then have "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)
then show ?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
then have "UP_pre_univ_prop R R (λx. x)"
using R_cring UP_pre_univ_propI by blast
then show ?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)
then have "(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)
then show ?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_Fun_mult:
assumes "x ∈ carrier P"
assumes "y ∈ carrier P"
shows "to_fun (x ⊗ y) = to_fun x ⊗ (carrier R) R to_fun y"
apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"])
apply (simp add: R.ring_axioms ring_functions_def)
apply (simp add: assms(1) assms(2) to_fun_is_Fun)
apply (simp add: R.ring_axioms assms(1) assms(2) ring_functions.fun_mult_closed ring_functions.intro to_fun_is_Fun)
by (simp add: R.ring_axioms assms(1) assms(2) ring_functions.function_mult_eval_car ring_functions.intro to_fun_is_Fun to_fun_mult)
lemma to_fun_Fun_add:
assumes "x ∈ carrier P"
assumes "y ∈ carrier P"
shows "to_fun (x ⊕ y) = to_fun x ⊕ (carrier R) R to_fun y"
apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"])
apply (simp add: R.ring_axioms ring_functions_def)
apply (simp add: assms(1) assms(2) to_fun_is_Fun)
apply (simp add: R.ring_axioms assms(1) assms(2) ring_functions.fun_add_closed ring_functions.intro to_fun_is_Fun)
by (simp add: R.ring_axioms assms(1) assms(2) ring_functions.fun_add_eval_car ring_functions.intro to_fun_is_Fun to_fun_plus)
lemma to_fun_Fun_one:
"to_fun 1 = 1 R"
apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"])
apply (simp add: R.ring_axioms ring_functions_def)
apply (simp add: to_fun_is_Fun)
apply (simp add: R.ring_axioms ring_functions.function_one_closed ring_functions_def)
using P_def R.ring_axioms UP_cring.eval_ring_hom UP_cring.to_fun_eval UP_cring_axioms UP_one_closed ring_functions.function_one_eval ring_functions.intro ring_hom_one
by fastforce
lemma to_fun_Fun_zero:
"to_fun 0 = 0 R"
apply(rule ring_functions.function_ring_car_eqI[of R _ "carrier R"])
apply (simp add: R.ring_axioms ring_functions_def)
apply (simp add: to_fun_is_Fun)
apply (simp add: R.ring_axioms ring_functions.function_zero_closed ring_functions_def)
using P_def R.ring_axioms UP_cring.eval_ring_hom UP_cring.to_fun_eval UP_cring_axioms UP_zero_closed ring_functions.function_zero_eval ring_functions.intro ring_hom_zero
by (metis UP_ring eval_ring_hom)
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
then show ?thesis using A
by (metis insert_absorb)
next
case False
have 0: "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
have 1: "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
have 2: "to_fun (f a ⊕finsum (UP R) f A ) t = to_fun (f a) t ⊕ (⨁i∈A. to_fun (f i) t)"
unfolding 1 A by blast
have 3: "(⨁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
unfolding 0 unfolding 3 using 2 unfolding 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
end
(**************************************************************************************************)
(**************************************************************************************************)
section‹Polynomial Substitution›
(**************************************************************************************************)
(**************************************************************************************************)
definition compose where
"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 sub_closed:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "sub q p ∈ carrier P"
by (simp add: assms(1) assms(2) rev_sub_closed sub_rev_sub)
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
then show ?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-
have 0: "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
have 1: "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)
then show ?thesis
using 0 1 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
then show ?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)
case 0
then show ?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
then show ?thesis using IH
using A0 by auto
next
case False
then have 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
have 0: " 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
then have "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)
then show "monom P b 0 [^] Suc n = monom P (b [^] Suc n) 0 "
by simp
qed
then have 0: "a ⊙ monom P b 0 [^] n = monom P (a ⊗ b[^]n) 0"
by (simp add: an_def b_def monom_mult_smult)
then show ?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)
then show ?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
then show ?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)
case 0
then have B0: "degree p = 0" by auto
then show ?case using 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
then show ?thesis using IH
by (simp add: A0)
next
case False
then have 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)
then show ?thesis
proof(cases "degree g = 0")
case True
then show ?thesis
by (simp add: Suc(2) assms(1) sub_in_const)
next
case F: False
then show ?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"
then have "degree (trunc p) ≤ n"
using D by auto
then have ?thesis
by (meson P1 le_trans mult_le_cancel2) }
then show ?thesis
by (metis (full_types) A0 D Suc_mult_le_cancel1 nat_mult_le_cancel_disj trunc_degree)
qed
then have 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
then show ?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
then show ?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-
have 0: "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)
have 1: "lcf f ≠ 0"
using assms cring.cring_simprules(26) lcf_closed
by auto
have 2: "degree ((ltrm f) of g) = degree f * degree g"
using 0 1 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)
using 0 1 assms cring_sub_deg_bound[of g "trunc f"] trunc_degree[of f]
using sub_const apply auto[1]
apply(cases "degree g = 0")
using 0 1 assms cring_sub_deg_bound[of g "trunc f"] trunc_degree[of f]
using sub_in_const apply fastforce
unfolding 0 using 1 2
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)
case 0
then have B0: "degree p = 0" by auto
then show ?case using 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
then show ?thesis using IH
by (simp add: A0)
next
case False
then have 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)
then show ?thesis
asesdegreeg "
case True
then show ?thesis
by (simp add: Suc(2) assms(1 u_incnt
n"java.lang.StringIndexOutOfBoundsException: Range [10, 9) out of bounds for length 128
case False
java.lang.StringIndexOutOfBoundsException: Range [32, 31) out of bounds for length 32
proof-
"ere(tucp fg) degree ((ltrm p) of g)"
using False D P1 P2
by (metis (no_types, lifting) A0 mult.commute mult_right_cancel
java.lang.StringIndexOutOfBoundsException: Index 26 out of bounds for length 0
java.lang.StringIndexOutOfBoundsException: Range [27, 26) out of bounds for length 34
by java.lang.StringIndexOutOfBoundsException: Range [46, 45) out of bounds for length 116
qed
java.lang.StringIndexOutOfBoundsException: Range [23, 21) out of bounds for length 116
qed
qed
qed
qed
then show ?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
then show ?thesis
using assms(1) sub_const by auto
next
case False
then show ?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)
then show ?thesis
proof(cases "degree f = 0")
case True
then show ?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)
then have 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))
then show ?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)
then show ?thesis
proof(cases "degree f = 0")
case True
then show ?thesis
using ltrm_deg_0 assms(2) by auto
next
case False
then have 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)
then show ?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_cring) cring_lcf_of_sub_in_ltrm:
assumes "g ∈ carrier P"
assumes "f ∈ carrier P"
assumes "degree f = n"
assumes "degree g > 0"
assumes "(lcf f) ⊗ ((lcf g)[^]n) ≠0"
shows "lcf ((ltrm f) of g) = (lcf f) ⊗ ((lcf g)[^]n)"
by (metis (no_types, lifting) P.nat_pow_closed P_def R.r_null UP_cring.monom_sub UP_cring_axioms
assms(1) assms(2) assms(3) assms(5) cfs_closed cring_lcf_pow cring_lcf_scalar_mult)
lemma(in UP_domain) lcf_of_sub_in_ltrm:
assumes "g ∈ carrier P"
assumes "f ∈ carrier P"
assumes "degree f = n"
assumes "degree g > 0"
shows "lcf ((ltrm f) of g) = (lcf f) ⊗ ((lcf g)[^]n)"
proof(cases "degree f = 0")
case True
then show ?thesis
using ltrm_deg_0 assms(1) assms(2) assms(3) cfs_closed
by (simp add: sub_const)
next
case False
then show ?thesis
proof-
have P0: "(ltrm f) of g = (to_poly (lcf f)) ⊗ (g[^]n)"
unfolding compose_def
using assms UP_pre_univ_prop.eval_monom[of R P to_poly "(lcf f)" g n] to_poly_UP_pre_univ_prop
unfolding P_def
using P_def cfs_closed by blast
have P1: "(ltrm f) of g = (lcf f) ⊙(g[^]n)"
using P0 P.nat_pow_closed
by (simp add: assms(1) assms(2) assms(3) cfs_closed monom_sub)
have P2: "ltrm ((ltrm f) of g) = (ltrm (to_poly (lcf f))) ⊗ (ltrm (g[^]n))"
using P0 ltrm_mult P.nat_pow_closed P_def assms(1) assms(2)
to_poly_closed
by (simp add: cfs_closed)
have P3: "ltrm ((ltrm f) of g) = (to_poly (lcf f)) ⊗ (ltrm (g[^]n))"
using P2 ltrm_deg_0 assms(2) to_poly_closed
by (simp add: cfs_closed)
have P4: "ltrm ((ltrm f) of g) = (lcf f) ⊙ ((ltrm g)[^]n)"
using P.nat_pow_closed P1 P_def assms(1) assms(2) ltrm_pow0 ltrm_smult
by (simp add: cfs_closed)
have P5: "lcf ((ltrm f) of g) = (lcf f) ⊗ (lcf ((ltrm g)[^]n))"
using lcf_scalar_mult P4 by (metis P.nat_pow_closed P1 cfs_closed
UP_smult_closed assms(1) assms(2) assms(3) lcf_eq ltrm_closed sub_rev_sub)
show ?thesis
using P5 ltrm_pow lcf_pow assms(1) lcf_eq ltrm_closed by presburger
qed
qed
lemma(in UP_cring) cring_ltrm_of_sub_in_ltrm:
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 ((ltrm f) of g) = (lcf f) ⊙ ((ltrm g)[^]n)"
by (smt (verit) lcf_eq ltrm_closed R.nat_pow_closed R.r_null assms(1) assms(2) assms(3)
assms(4) assms(5) cfs_closed cring_lcf_of_sub_in_ltrm cring_lcf_pow cring_pow_ltrm
cring_pow_deg cring_sub_deg deg_zero deg_ltrm monom_mult_smult neq0_conv)
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)
then show ?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)
case 0
then have deg_p: "degree p = 0"
by blast
then have 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
then show "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"
then show "∧ 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
then show ?thesis using A0 A1 IH by auto
next
case False
then have "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)
then show ?thesis
using A0 trunc_simps(1) by auto
qed
qed
qed
qed
then show ?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)
then have "(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)
then have "(a⊙f ) of q = (to_poly a) ⊗(f of q)"
by (simp add: assms(2) assms(3) sub_to_poly)
then show ?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
then have 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)
then have 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-
have 0: "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)
have 1: "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 ))"
using 0 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)
have 2: "to_fun (monom P b n of g) a = b ⊗ ( eval R R (λx. x) a ( g [^] R n ))"
using 1 assms(3) b_def to_fun_eval to_fun_to_poly to_poly_closed by auto
then show ?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
then show ?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"
then have P0: "degree (p of g) = 0"
by (simp add: A0 assms(1) sub_const)
then obtain 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)
then have "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
then have 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)
then show "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)
then have "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)
then have 0: "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)
then have "to_fun (p of g) a = to_fun (trunc p) (to_fun g a) ⊕ to_fun (ltrm p) (to_fun g a)"
using 0 by auto
then show ?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)
then have "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)
then show ?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_ltrm_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
assumes "degree p > 0"
shows "zcf((ltrm p) ⊗ q) = 0"
using zcf_to_fun[of "ltrm p ⊗ q" ]
by (metis ltrm_closed P.l_null P.m_closed R.zero_closed UP_zero_closed zcf_to_fun
zcf_zero assms(1) assms(2) assms(3) coeff_ltrm to_fun_mult)
lemma zcf_mult:
assumes "p ∈ carrier P"
assumes "q ∈ carrier P"
shows "zcf(p ⊗ q) = (zcf p) ⊗ (zcf q)"
using zcf_to_fun[of " p ⊗ q" ] zcf_to_fun[of "p" ] zcf_to_fun[of "q" ] to_fun_mult[of q p 0]
by (simp add: assms(1) assms(2))
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
(**************************************************************************************************)
(**************************************************************************************************)
section‹Taylor Expansions›
(**************************************************************************************************)
(**************************************************************************************************)
(**************************************************************************************************)
(**************************************************************************************************)
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 1 1]
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)
then show ?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)
then show ?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-
have 0:"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
have 1:"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)
then show ?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)
text‹Linear substituions›
lemma X_plus_sub_deg:
assumes "a ∈ carrier R"
assumes "f ∈ carrier P"
shows "degree (f of (X_plus a)) = degree f"
apply(cases "1 = 0")
apply (metis P_def UP_one_closed X_plus_closed X_poly_def sub_X assms(1) assms(2) deg_one monom_one monom_zero sub_const)
using cring_sub_deg[of "X_plus a" f] assms X_plus_closed[of a] lcf_of_X_plus[of a]
ltrm_of_X_plus degree_of_X_plus[of a] P_def
by (metis lcf_eq R.nat_pow_one R.r_one UP_cring.cring_sub_deg UP_cring_axioms X_closed X_sub
cfs_closed coeff_simp deg_nzero_nzero degree_X lcoeff_nonzero2 sub_const)
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)
then have "(X ⊕ to_poly a) of X_minus a = (X_minus a) ⊕ (to_poly a)"
by (simp add: X_minus_closed assms sub_to_poly)
then show "(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)
lemma times_X_not_zero:
assumes "p ∈ carrier P"
assumes "p ≠ 0"
shows "(X ⊗ p) ≠ 0"
by (metis (no_types, opaque_lifting) lcf_monom(1) lcf_of_X_minus ltrm_of_X_minus P.inv_unique
P.r_null R.l_one R.one_closed UP_zero_closed X_closed zcf_def
zcf_zero_degree_zero assms(1) assms(2) cfs_closed cfs_zero cring_lcf_mult
deg_monom deg_nzero_nzero deg_ltrm degree_X degree_of_X_minus
monom_one monom_zero)
lemma degree_times_X:
assumes "p ∈ carrier P"
assumes "p ≠ 0"
shows "degree (X ⊗ p) = degree p + 1"
using cring_deg_mult[of X p] assms times_X_not_zero[of p]
by (metis (no_types, lifting) P.r_null P.r_one P_def R.l_one R.one_closed
UP_cring.lcf_monom(1) UP_cring_axioms UP_zero_closed X_closed X_poly_def cfs_closed
deg_zero deg_ltrm degree_X monom_one monom_zero to_poly_inverse)
end
(**************************************************************************************************)
(**************************************************************************************************)
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
notation taylor (‹T›)
lemma(in UP_cring) taylor_closed:
assumes "f ∈ carrier P"
assumes "a ∈ carrier R"
shows "T f ∈ carrier P"
unfolding taylor_def
by (simp add: X_plus_closed assms(1) assms(2) sub_closed taylor_expansion_def)
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-
have 0: "p of q = rev_sub q p"
unfolding compose_def rev_compose_def by blast
have 1: "p of q = finsum P (rev_compose R q ∘ g) {..n}"
unfolding 0 unfolding 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 unfolding 1
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
have 0: "∧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
have 1: "(∧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
then have "p = (⨁ i ∈ {..n}. g i)"
using g_def by auto
then have "p of q = (⨁i∈{..n}. g i of q)"
using 0 1 poly_comp_finsum[of n g q p]
using assms(2)
by blast
then show ?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-
have 0: "(T p) of X_minus a = p"
using P_def taylor_id assms(1) assms(3)
by fastforce
have 1: "degree (T p) ≤ n"
using assms
by (simp add: taylor_deg)
have 2: "T p of X_minus a = (⨁i∈{..n}. T p i ⊙ X_minus a [^] i)"
using 1 X_minus_closed[of a] poly_comp_expansion[of "T p" "X_minus a" n]
assms taylor_closed
by blast
then show ?thesis
using 0
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 \<in> carrier P"
assumes "degree p \<le> n"
assumes "a \<in> carrier R"
shows "p = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..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 \<in> carrier P"
assumes "q \<in> carrier P"
assumes "c \<in> carrier R"
shows "taylor_expansion R c (p \<oplus>\<^bsub>UP R\<^esub> q) = (taylor_expansion R c p) \<oplus>\<^bsub>UP R\<^esub> (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 \<in> carrier P"
assumes "q \<in> carrier P"
assumes "a \<in> carrier R"
shows "taylor_term a (p \<oplus>\<^bsub>UP R\<^esub>q) i = taylor_term a p i \<oplus>\<^bsub>UP R\<^esub> 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 \<in> carrier P"
assumes "a \<in> carrier R"
assumes "c \<in> carrier R"
shows "to_fun (taylor_term c p i) a = (T\<^bsub>c\<^esub> p i) \<otimes> (a \<ominus> c)[^]i"
using assms to_fun_smult[of "X_minus c [^]\<^bsub>UP R\<^esub> 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\<open>Defining the (Scalar-Valued) Derivative of a Polynomial Using the Taylor Expansion\<close>
(**************************************************************************************************)
(**************************************************************************************************)
definition derivative where
"derivative R f a = (taylor_expansion R a f) 1"
context UP_cring
begin
abbreviation(in UP_cring) deriv where
"deriv \<equiv> derivative R"
lemma(in UP_cring) deriv_closed:
assumes "f \<in> carrier P"
assumes "a \<in> carrier R"
shows "(derivative R f a) \<in> 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 \<in> carrier P"
assumes "g \<in> carrier P"
assumes "a \<in> carrier R"
shows "deriv (f \<oplus>\<^bsub>P\<^esub> g) a = deriv f a \<oplus> deriv g a"
unfolding derivative_def taylor_expansion_def using assms
by (simp add: X_plus_closed sub_add sub_closed)
end
(**************************************************************************************************)
(**************************************************************************************************)
section\<open>The Polynomial-Valued Derivative Operator\<close>
(**************************************************************************************************)
(**************************************************************************************************)
context UP_cring
begin
(**********************************************************************)
(**********************************************************************)
subsection\<open>Operator Which Shifts Coefficients\<close>
(**********************************************************************)
(**********************************************************************)
lemma cfs_times_X:
assumes "g \<in> carrier P"
shows "(X \<otimes>\<^bsub>P\<^esub> g) (Suc n) = g n"
apply(rule poly_induct3[of g])
apply (simp add: assms)
apply (metis (no_types, lifting) P.m_closed P.r_distr X_closed cfs_add)
by (metis (no_types, lifting) P_def R.l_one R.one_closed R.r_null Suc_eq_plus1 X_poly_def
cfs_monom coeff_monom_mult coeff_simp monom_closed monom_mult)
lemma times_X_pow_coeff:
assumes "g \<in> carrier P"
shows "(monom P \<one> k \<otimes>\<^bsub>P\<^esub> 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 \<in> carrier P"
assumes "g \<in> carrier P \<and> (f = X \<otimes>\<^bsub>P\<^esub> g)"
shows "\<And> h. h \<in> carrier P \<and> (f = X \<otimes>\<^bsub>P\<^esub> h) \<Longrightarrow> h = g"
proof-
fix h
assume A: "h \<in> carrier P \<and> (f = X \<otimes>\<^bsub>P\<^esub> h)"
then have 0: " X \<otimes>\<^bsub>P\<^esub> g = X \<otimes>\<^bsub>P\<^esub> h"
using assms(2) by auto
show "h = g"
using 0 A assms
by (metis P_def coeff_simp cfs_times_X up_eqI)
qed
lemma f_minus_ctrm:
assumes "f \<in> carrier P"
shows "zcf(f \<ominus>\<^bsub>P\<^esub> ctrm f) = \<zero>"
using assms
by (smt (verit) ctrm_is_poly P.add.inv_closed P.minus_closed P_def R.r_neg R.zero_closed zcf_to_fun
to_fun_minus to_fun_plus UP_cring_axioms zcf_ctrm zcf_def a_minus_def cfs_closed)
definition poly_shift where
"poly_shift f n = f (Suc n)"
lemma poly_shift_closed:
assumes "f \<in> carrier P"
shows "poly_shift f \<in> carrier P"
apply(rule UP_car_memI[of "deg R f"])
unfolding poly_shift_def
proof -
fix n :: nat
assume "deg R f < n"
then have "deg R f < Suc n"
using Suc_lessD by blast
then have "f (Suc n) = \<zero>\<^bsub>P\<^esub> (Suc n)"
by (metis P.l_zero UP_zero_closed assms coeff_of_sum_diff_degree0)
then show "f (Suc n) = \<zero>"
by simp
next
show " \<And>n. f (Suc n) \<in> carrier R"
by(rule cfs_closed, rule assms)
qed
lemma poly_shift_eq_0:
assumes "f \<in> carrier P"
shows "f n = (ctrm f \<oplus>\<^bsub>P\<^esub> X \<otimes>\<^bsub>P\<^esub> poly_shift f) n"
apply(cases "n = 0")
apply (smt (verit) ctrm_degree ctrm_is_poly ltrm_of_X One_nat_def P.r_null P.r_zero P_def UP_cring.lcf_monom(1) UP_cring_axioms UP_mult_closed UP_r_one UP_zero_closed X_closed zcf_ltrm_mult zcf_def zcf_zero assms cfs_add cfs_closed deg_zero degree_X lessI monom_one poly_shift_closed to_poly_inverse)
proof- assume A: "n \<noteq> 0"
then obtain k where k_def: " n = Suc k"
by (meson lessI less_Suc_eq_0_disj)
show ?thesis
using cfs_times_X[of "poly_shift f" k] poly_shift_def[of f k] poly_shift_closed assms
cfs_add[of "ctrm f" "X \<otimes>\<^bsub>P\<^esub> poly_shift f" n] unfolding k_def
by (simp add: X_closed cfs_closed cfs_monom)
qed
lemma poly_shift_eq:
assumes "f \<in> carrier P"
shows "f = (ctrm f \<oplus>\<^bsub>P\<^esub> X \<otimes>\<^bsub>P\<^esub> poly_shift f)"
by(rule ext, rule poly_shift_eq_0, rule assms)
lemma poly_shift_id:
assumes "f \<in> carrier P"
shows "f \<ominus>\<^bsub>P\<^esub> ctrm f = X \<otimes>\<^bsub>P\<^esub> 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 \<in> carrier P"
assumes "degree p = 0"
shows "poly_shift p = \<zero>\<^bsub>P\<^esub>"
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 \<in> 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 \<in> 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)) \<oplus>\<^bsub>P\<^esub> X \<otimes>\<^bsub>P\<^esub>poly_shift (monom P a (Suc k))"
using poly_shift_eq[of "monom P a (Suc k)"] assms monom_closed
by blast
then have "(monom P a (Suc k)) = \<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> X \<otimes>\<^bsub>P\<^esub>poly_shift (monom P a (Suc k))"
using assms by simp
then have "(monom P a (Suc k)) = X \<otimes>\<^bsub>P\<^esub>poly_shift (monom P a (Suc k))"
using X_closed assms poly_shift_closed by auto
then have "X \<otimes>\<^bsub>P\<^esub>(monom P a k) = X \<otimes>\<^bsub>P\<^esub>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)
then show ?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_add:
assumes "f \<in> carrier P"
assumes "g \<in> carrier P"
shows "poly_shift (f \<oplus>\<^bsub>P\<^esub> g) = (poly_shift f) \<oplus>\<^bsub>P\<^esub> (poly_shift g)"
apply(rule ext)
using cfs_add[of "poly_shift f" "poly_shift g"] poly_shift_closed poly_shift_def
by (simp add: poly_shift_def assms(1) assms(2))
lemma(in UP_cring) poly_shift_s_mult:
assumes "f \<in> carrier P"
assumes "s \<in> carrier R"
shows "poly_shift (s \<odot>\<^bsub>P\<^esub>f) = s \<odot>\<^bsub>P\<^esub> (poly_shift f)"
proof-
have "(s \<odot>\<^bsub>P\<^esub>f) = (ctrm (s \<odot>\<^bsub>P\<^esub>f)) \<oplus>\<^bsub>P\<^esub>(X \<otimes>\<^bsub>P\<^esub> poly_shift (s \<odot>\<^bsub>P\<^esub>f))"
using poly_shift_eq[of "(s \<odot>\<^bsub>P\<^esub>f)"] assms(1) assms(2)
by blast
then have 0: "(s \<odot>\<^bsub>P\<^esub>f) = (s \<odot>\<^bsub>P\<^esub>(ctrm f)) \<oplus>\<^bsub>P\<^esub>(X \<otimes>\<^bsub>P\<^esub> poly_shift (s \<odot>\<^bsub>P\<^esub>f))"
using ctrm_smult assms(1) assms(2) by auto
have 1: "(s \<odot>\<^bsub>P\<^esub>f) = s \<odot>\<^bsub>P\<^esub> ((ctrm f) \<oplus>\<^bsub>P\<^esub> (X \<otimes>\<^bsub>P\<^esub> (poly_shift f)))"
using assms(1) poly_shift_eq by auto
have 2: "(s \<odot>\<^bsub>P\<^esub>f) = (s \<odot>\<^bsub>P\<^esub>(ctrm f)) \<oplus>\<^bsub>P\<^esub> (s \<odot>\<^bsub>P\<^esub>(X \<otimes>\<^bsub>P\<^esub> (poly_shift f)))"
by (simp add: "1" X_closed assms(1) assms(2) ctrm_is_poly poly_shift_closed smult_r_distr)
have 3: "(s \<odot>\<^bsub>P\<^esub>f) = (s \<odot>\<^bsub>P\<^esub>(ctrm f)) \<oplus>\<^bsub>P\<^esub> (X \<otimes>\<^bsub>P\<^esub> (s \<odot>\<^bsub>P\<^esub>(poly_shift f)))"
using "2" UP_m_comm X_closed assms(1) assms(2) smult_assoc2
by (simp add: poly_shift_closed)
have 4: "(X \<otimes>\<^bsub>P\<^esub> poly_shift (s \<odot>\<^bsub>P\<^esub>f)) = (X \<otimes>\<^bsub>P\<^esub> (s \<odot>\<^bsub>P\<^esub>(poly_shift f)))"
using 3 0 X_closed assms(1) assms(2) ctrm_is_poly poly_shift_closed
by auto
then show ?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
lemmaf_poly_shift::
assumes "f \in> 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 (\<open>shift\<close>) where
Base:"poly_shift_iter 0 f = f"|
Step:"poly_shift_iter (Sucstatic const struct inode_operations ceph_encrypted_symlink_iops;
lemma shift_closed:
assumes "f \<in> carrier P"
shows "}
apply(induction n)
using assms poly_shift_closed by auto
(**********************************************************************)
(****************************************************)
subsection\<open>Operator Which Multiplies Coefficients by Their Degree\<close>
(************************************* * they donotmatch–which can theoretically happen if parentdentry was
(************************************************************java.lang.StringIndexOutOfBoundsException: Index 74 out of bounds for length 74
definition n_mult where
"n_mult f = (\<lambda>n. [n]\<cdot>\<^bsub>R\<^esub>(f n))"
lemma(in UP_cring) n_mult_closed:
assumes "f \<in> carrier P"
shows "n_mult f \<in> carrier P"
apply(rule UP_car_memI[of "deg R f"])
unfoldingjava.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
apply returnparent /* matches – use the original reference */
using assms cfs_closed by auto
text\<open>Facts about the shift function\<close>
java.lang.StringIndexOutOfBoundsException: Range [16, 15) out of bounds for length 16
"shift (Suc 0) = poly_shift"
by auto
lemma shift_factor0:
assumes "f \<in> carrier P"
* info for new inode.
proof(induction k)
java.lang.StringIndexOutOfBoundsException: Range [8, 6) out of bounds for length 8
0 <><^sub\^esub> ctrm)= (shift(Suc 0 )\otimes>\<^bsub>P\<^esub>X"
by (metis UP_m_comm X_closed assms java.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 0
ub(shift (uc0)f\<otimes>\<bsub>P\<^> = ctrm f
proof-
have " f \<ominus>\<^bsub>P\<^esub> (ctrm f) \<ominus>\<^bsub>P\<^esub> (shift (Suc 0) f)\<otimes>\<^bsub>P\<^esub>X= (shift (Suc 0) f)\<otimes>\<^bsub>P\<^esub>X \<ominus>\<^bsub>P\<^esub> (shift (Suc *the ()
using
then have " f \< struct *as_ctx
using
by (metis "0" P. *@sb superblock tosearch and allocate in
a_minus_def abelian_group.r_neg ctrm_is_poly ring_def)
then have " f \<ominus>\<^bsub>P\<^esub> ((ctrm f) \<oplus>\<^bsub>P\<^esub> (shift (Suc 0) f)\<otimes>\<^bsub>P\<^esub>X) = \<zero>\<^bsub>P\<^esub>"
using assms P.ring_simprules
by (metis "0" poly_shift_id poly_shift_eq)
then have " f \<ominus>\<^bsub>P\<^esub> ((shift (Suc 0) f)\<otimes>\<^bsub>P\<^esub>X \<oplus>\<^bsub>P\<^esub> (ctrm f) ) = \<zero>\<^bsub>P\<^esub>"
osed
presburger
then have "f \<java.lang.StringIndexOutOfBoundsException: Index 25 out of bounds for length 21
Paddm_assoc P.ring_simprules(14)P.ring_simprules(19) assms "0"
P.add.inv_closed P.r_neg P.r_zero ctrm_is_poly
((erit, ccfv_threshold))
then show ?thesis
by m ""P..m_comm P.m_closed P.ring_simprules() .ring_simprules(18)
P.ring_simprules(3) X_closed assms ctrm_is_poly poly_shift_id poly_shift_eq
shift_closed)
qed
then have " f .ino =ceph_ino(arent)
X^]\^bsub>\^>Suc)"
by (simp add inode_set_mtime_to_ts(,inode_get_mtime(parent));
show ?thesis
usingceph_inode_info*pci =ceph_inode(parent);
inode-i_flags =S_ENCRYPTED;
qed
then have "
usingctrm_degree[f ] assms by simp
then show iput(inode);
by blast
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
case (Suc n)
fix k
assume IH: " * foragiven inode (usually there is just a single fragment). We
show "degree f \<ge> (Suc (Suc k)) \<Longrightarrow> degree (f \<ominus>\<^bsub>P\<^esub> ((shift (Suc (Suc k)) f) \<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>(Suc (Suc k))))) < (Suc (Suc k))"
proof-
obtain n where n_def: "n = Suc k"
by simp
have IH': "degree f \<ge> n \<Longrightarrow> degree (f \<ominus>\<^bsub>P\<^esub> ((shift n f) \<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>n))) < n"
using n_def IH by struct inode*node=&ci-netfs.inode;
have :"degree \ge> (uc n \<Longrightarrow> degree (f \<ominus>\<^bsub>P\<^esub> ((shift (Suc n) f) \<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>(Suc n)))) < (Suc n)"
proof-
obtain where g_def:" =(f \<ominus><^bsub\<esub> ((shift n f) \<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>n)))"
simp
f: "s =shift n f"
by simp
obtain s' where s'_def: "s' = shift (Suc n){
bysimp
have P: "g
using s_def s'_def g_def assms shift_closed[of f n]
apply (simp add: X_closed)
apply (simp add: \<open>f \<in> carrier P \<Longrightarrow> shift n f \<in> carrier P\<close> assms s_def)
using P_defUP_cring.shift_closed UP_cring_axioms assms s'defapplyblast
using X_closed by blast
have g_def
using g_def s_def by auto
assume "degree while (){
then have " degree (f \<ominus> if (rag->plit_by == 0) {
using IH' Suc_leD s_def by blast
then have d_g: "degree g < n" using g_def' by auto
sub>\<esub (s \otimes\^bsub\<^sub>(X^\<^bsubP<^sub(Sucn))=((ctrms)\<otimes>\^bsub>\<^sub(^\<bsubP\<esub>n)\oplus>\<^bsub>P<esub> g"
proof-
have "s = (ctrm s) \<oplus>\<^bsub>P\<^esub>}
using s_def s'_ u32 ret;
by (simp/
then have 0: "g = f \<ominus>\<^bsub>P\<^esub> ((ctrm s) \<oplus>\<^bsub>P\<^esub> (X \<otimes>\<^bsub>P\<^esub> s')) \<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>n)"
using g_def' by auto
then have "g = f \<ominus>\<^bsub>P\< * branches/splits are included in i_fragtree)
using cring_axioms X_closed P._distr P.ring_simprules(19) UP_a_assoc a_minus_def assms
by (simp add: a_minus_def ctrm_is_poly)
then have "g \<oplus>\<^bsub> int i;
using cring_axiomscring_axioms X_closed .l_distr Pring_simprules UP_a_assoc a_minus_def assms
by (simp add: P.r_neg2 ctrm_is_poly)
then have " frag>split_by ==0 {
usingP X_closed P.ring_simprules UP_a_assoc a_minus_def assms
by (simp add: P.ring_simprules(17) ctrm_is_poly)
then have " ( java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2
by sadd P(1) P()UP_a_comm X_closed)
then have"(ctrm s\<times><^sub>P\<esub(X[^\<^bsubP\^esub>n)= f \<ominus>\^bsub>P<^esub>((X \otimes\<^sub>P\<esub> s') \otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>n)) \<ominus>\<^bsub>P\<^esub> g"
using P(1) P(3) }
by (simp add: a_minus_def X_closed)
then have "((ctrm java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
by (metis {
P.ring_simprules(4) P_def return ceph_frag_compare(le32_to_cpu(ls->fragceph_frag_compare(le32_to_cpu(ls->frag),
then have "((ctrm s)\<otimes{
by (simp add: P returnfalse;
then have "((ctrm s)\<otimes> struct ceph_frag_tree_head *fragtree,
using P struct ceph_inode_info *i =ceph_inode(node;
then show ?thesis
by auto
qed
:"degree ((ctrm s)<otimes>\^bsubP\^esuble> n"
proof-
java.lang.StringIndexOutOfBoundsException: Index 17 out of bounds for length 17
proof(-s, nsplits sizeoffragtree-splits[],
case
then show ?thesis
by (simp add: P())
next
rb_node = rb_next()java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds for length 30
have:"degree ((ctrm s)\otimes\<bsub>\<^esub>([^]\<^bsub>P\<^sub>n)) \<e>degree (ctrm s) + degree (X[^]\<^bsub>P\<^esub>n) "
by ( ctrm_is_poly P2 (4) deg_mult_ring)
haveF1 "\<one>\<><zero\<Longrightarrow> degree (X[^]\<^bsub>P\<^esub>n) = n"
unfolding X_poly_def
usingP_def java.lang.StringIndexOutOfBoundsException: Range [36, 28) out of bounds for length 36
show ?thesis
by(metis(no_types,opaque_lifting) F0F1ltrm_deg_0 P(2) P.r_null P_def R.l_null R.l_one
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
add_0 deg_const deg_zero java.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 0
)
then show ?thesis
using atomic64_set(&ci->atomic64_set(&ci-i_complete_seq[0], 0);
(simp add: P(1)P(2) P(4)bound_deg_sumctrm_is_poly)
qed
then ?hesis
using s'_def P0 by auto
qed
assume "degree f \<ge> (Suc (Suc k)) "
then show "degree (f \ ci->i_dirty_caps =0;
P by( add n_def)
qed
qed
lemma(in UP_cring) shift_degree0:
assumes "f \<in> carrier P"
shows "degree f >n \<java.lang.StringIndexOutOfBoundsException: Index 31 out of bounds for length 18
proof(induction n)
case 0
B:"0< degree f"
have :"egree(shift0f = degree f"
by simp
have 1: "degree f = degree {
usingassms() B ctrm_degree degree_of_difference_diff_degree
by (simp add: ctrm_is_poly) *inode)
>\<^bsubP<^esub> (ctrm f)) = X \otimes>\<^bsub\<^esub>(shift 1 f)"
using P_def poly_shift_id UP_cring_axioms assms(1) by auto
then have "degree (f \<ominus>\<^bsub>P\<^esub> (ctrm f)) = 1 + (degree (shift 1 f))"
by (metis "1" B
then have "degree (shift 0 if (__ceph_has_quota(ci, QUOTAGET_ANY))
using 0 1 byauto
then show ?case
by simp
next
case (Suc n)
n
assume IH: "(n < frag = rb_entry(n, struct ceph_inode_frag, node);
show "Suc n < degree f
proof-
assume A: " Suc n < degree f"
thenhave 0 "shift(Suc n f) = ctrm (shift (Suc n f)) \oplus\<^bsub>P\<esub (hift(Suc (uc n)f)\<times\^bsub>P\<esub>X"
local.Step poly_shift_eq shift_closed)
have N: "(shift (Suc (Suc n)) f) \<noteq> \<zero>\<^bsub>P\<^esub>"
proof
assume C: "shift (Suc (Suc n)) f = \<zero>\<^bsub>P\<^esub>"
obtain g where g_def: "g = f \<ominus>\<^bsub>P\<^esub> (shift (Suc (Suc n)) f)\<otimes>\<^bsub>P\<^esub>(X[^]\<^bsub>P\<^esub>(Suc (Suc n)))"
by simp
* and sizeare monotonicallyincreasing, except when utimes() or
using g_def assms A
Suc_leI Suc_less_SucD Suc_mono less_trans_Suc shift_factor0)
have C1:"g =f"
using C
by ( add Pminus_eq X_closed assms g_def)
thenshowFalse
using C0 by auto
qed
have 1: "degree (shift (Suc n) f) = degree ((shift (Suc n) f) \<ominus>\<^bsub>P\<^esub> ctrm ((shift (Suc n) f)))"
proofcases "degree (shift (Suc n) f) = 0")
case True
then show ?thesis
using N * the MDS should have revoked these caps */
case False
then have "degree (shift (Suc n) f) > degree (ctrm ((shift (Suc n) f)))"
proof -
have "shift (Suc n) *the is either opened or mmapedmmaped
using CEPH_CAP_FILE_BUFFER)) ||
then show ? mapping_mapped(inode->i_mapping) ||
using False ctrm_degree by auto
qed
then show ?thesis
proof -
show ?thesis
using \<open>degree (ctrm (shift (Suc n) f)) < degree (shift (Suc n) f)\<close>
assms ctrm_is_poly degree_of_difference_diff_degree shift_closed by presburger
qed
have >i_truncate_pagecache_size, size);
using 0
by (metis Cring_Poly.INTEG.Stepvoid ceph_fill_file_time(struct inode *inode,int ,
have 3: "struct ceph_client*cl = ceph_inode_to_client(inode);
using 2 N X_closed X_not_zero assms degree_X shift_closed
by (metis UP_m_comm degree_times_X)
then show ?thesis using 1
by linarith
qed
qed
lemma(n )shift_degree:
assumes " }else if (ime_warp_seq == ci->i_time_warp_seq) {
shows "degree f \<ge> n \<Longrightarrow> degree (shift n f) + n = degree f"
uction n
0
then show ?
by auto
next
case (Suc n)
fix n
assume IH: " /*wehave no write|excl caps; whatever the MDS says is true */
show "Suc n inode_set_mtime_to_ts(inode, *mtime);
proof-
assume A: doutc(, "% mds %llu < %u\n", inode,
have#if IS_ENABLED(CONFIG_FS_ENCRYPTION)
using IH byauto
ave:" (shift n f) = Suc (egree (shift (Suc n) f))"
using A assms shift_degree0 by auto
show "degree{
using 0 1 by simp
qed
qed
lemma(in }
java.lang.StringIndexOutOfBoundsException: Index 43 out of bounds for length 29
shows "degree (shift (degree f) f) = 0"
using shift_degree assms
by fastforce
lemma) shift_above_degree:
assumes "f \<in> carrier P"
assumes "k > degree f"
shows "(shift k f) = \<zero>\<^bsub>P\<^esub>"
-
have "\<java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
/* Once I_NEW is cleared, we can't change type or dev numbers */
fix n
show "shift ((degree f)+ (Suc n)) f = \<zero>\<^bsub>P\<^esub>"
induction n
case 0
have B0:"shift (degree f) f = ctrm(shift (degree f) f) \<oplus>\<^bsub>P\<^esub> (shift (degree f + Suc 0) f)\<otimes>\<^bsub>P\<^esub>X"
proof -
have f1: "\<forall>f n. f \<notin> carrier P \<or> shift n f \<in> carrier P"
by (meson shift_closed)
then have "shift (degree f + Suc 0) f \<in> carrier P"
using assms(1) by blast
then show ?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 \<in> carrier P"
using assms(1) shift_closed by blast
then show ?thesis
sing ltrm_deg_0 assms(1)shift_degree by auto
qed
B2:"s (degree f + Suc) )\<otimes>\<^bsub\<^esub>X = \zero><^bsub>P\<^esub>"
using}
java.lang.StringIndexOutOfBoundsException: Range [24, 13) out of bounds for length 13
have "\<forall>f n. f \<notin> carrier P \<or> shift n f \<in> carrier P"
using shift_closed by blast
then show ?thesis
by (metis (no_types) B0 B1 P.add.l_cancel_one UP_mult_closed iinfo>xattr_len)java.lang.StringIndexOutOfBoundsException: Index 28 out of bounds for length 28
qed iinfo->pool_ns_len);
then ci->_snapid_map = ceph_get_snapid_map(mdsc, ceph_snap(inode));
by (etisP._ UP_m_comm UP_zero_closed X_closed assms1 zcf_eq_zero_unique shift_closed)
next
case (Suc n)
fix n
assume "shift (degree f + Suc n) f = \<zero>\<^bsub>P\<^esub>"
then show "shift (degree f + Suc (Suc n)) f = \<zero>\<^bsub>P\<^esub>"
by (simp add: poly_shift_degree_zero)
qed
qed
then show ?thesis
using assms(2) less_iff_Suc_add by auto
qed
lemma(in UP_domain) shift_cfs0:
__ceph_caps_issuedci, &ssued)java.lang.StringIndexOutOfBoundsException: Index 33 out of bounds for length 33
shows "zcf(shift
java.lang.StringIndexOutOfBoundsException: Index 37 out of bounds for length 14
by (simp add:zcf_poly_shift)
lemma(in UP_cring) X_mult_cf:
assumes "p \<in> carrier P"
shows "( \<otimes>\^bsub>P\<^esub> X) k1 = p kjava.lang.StringIndexOutOfBoundsException: Index 54 out of bounds for length 54
unfolding X_poly_def
using assms
by (metis UP_m_comm X_closed/* directories have fl_stripe_unit set to zero */
lemma(in UP_cring) X_pow_cf:
assumes "p \<in> carrier P"
shows"p\<otimes>\<bsubP\^esub> X^]\<^bsubP<esub(n:nat) (n k) = p k"
proof-
have P: "\<And>f. f \ ceph_fill_file_time(node ,
proof(induction n)
show "\<And>f. f (new_issued & (|java.lang.StringIndexOutOfBoundsException: Range [64, 63) out of bounds for length 68
proof-
if(-ilayout.ool_id ! | pool_ns! old_ns)
assume B0: =old_ns;
show "(f \<otimes>\<^bsub>P\<^esub u64 fsize = _le64_to_cpu(*__le64 *)iinfo->fscrypt_file)java.lang.StringIndexOutOfBoundsException: Index 61 out of bounds for length 61
(imp:java.lang.StringIndexOutOfBoundsException: Index 25 out of bounds for length 25
qed
fix n
fix f
IH: "\Andf. f \in> carrier P\Longrightarrow> ( \<otimes>\^bsub>\^ X ^\^><esub> n)n +k = f k"
A0: <n carrier P"
"f\otimes\^bsub>\^>X ^\<^sub>P\^> Suc n) (ucn+ k) =f k"
proof-
have ifci>i_xattrs.blob)
using A0 iinfo-x -x;
java.lang.StringIndexOutOfBoundsException: Range [13, 12) out of bounds for length 20
using
caseS_IFSOCK
have 2: "(f \<otimes> -i_op =&;
using 1
by (simp add: A0 X_closed)
then show ?thesis
by(simp add:""
qed
qed
show ?thesis using assms pr_err_clientcl,
qed
lemma java.lang.StringIndexOutOfBoundsException: Index 20 out of bounds for length 13
assumes "f \<in> carrier P"
shows "poly_shift f n = f
proof-
have "(f \<ominus>\<^bsub>P\<^esub> ctrm f) (Suc n) = (X \<otimes>\<^bsub>P\<^esub> (poly_shift f)) (Suc n)"
using assms poly_shift_id by auto
then show ?thesis unfolding X_poly_def inode>_p = ceph_dir_iops;
y
P.ddm_comm .minus_closedcoeff_of_sum_diff_degree0poly_shift_id poly_shift_eq cfs_times_X zero_less_Suc)
qed
in )shift_cfs:
assumes" \in>carrier "
shows"shiftkp) n p( +n)java.lang.StringIndexOutOfBoundsException: Index 35 out of bounds for length 35
apply(induction k arbitrary: n)
by a assmspoly_shift_cfs )
****************************************
(********************************* java.lang.StringIndexOutOfBoundsException: Range [22, 21) out of bounds for length 30
subsection\<open>The Derivative if(ill_inline
(************************* wake_up_all(ci>i_cap_wq)
(***********************************************java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
definition pderiv where
"pderiv p out:
p \<in>carrier P"
"deriv \<n carrier P"
unfolding pderiv_def
usingn_mult_closed[ ] [of"n_mult p]
blast
text\<open>Function which obtains the first n+1 terms
definition trms_of_deg_leq where
"trms_of_deg_leq n f \<equiv> f \<ominus>\<^bsub>(return; * we already have a newer lease. */
lemma trms_of_deg_leq_closed:
assumes "f \<in> carrier P"
shows_java.lang.StringIndexOutOfBoundsException: Range [27, 26) out of bounds for length 31
unfolding trms_of_deg_leq_def using assms
by (spin_lock&>)
lemma trms_of_deg_leq_id:
assumes "f \<in> carrier P"
shows "f \<ominus>\ struct ceph_vino *,
unfolding mds_session *=NULL;
using
by (smt (verit) P.add.inv_closed P.l_zero java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
gotoout_unlock;
lemma spin_unlock(&dentry->d_(&>_);
spliceadentry aninode.
shows "f = (trms_of_deg_leq k f) \<oplus>\<^bsub>P\<^esub> shift (Suc k) f \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
using trms_of_deg_leq_id assms trms_of_deg_leq_closed[of f]
by (smt (verit, ccfv_threshold) java.lang.StringIndexOutOfBoundsException: Range [0, 35) out of bounds for length 27
lemma deg_leqI:
assumes "p \ realdn =d_find_any_alias();){
assumes "\< realdn->d_op>d_prune(realdn);
"egree p \l k"
by (metis assms(1) }
emma deg_leE:
assumes "p \<in> PTR_ERR(realdn PTR_ERR(realdn) dn, in,ceph_vinop(n);
assumes d p <k"
shows "p k = \<zero>"
f_sum_diff_degree0 P_def coeff_simp deg_aboveD
by autoreturn0
lemma trms_of_deg_leq_deg:
assumes "f \<in> carrier P"
shows "degree (trms_of_deg_leq k f) \<le> k"
proof-
anda target inode
proof-
fix
have 0: "(shift (Suc k) f \< struct ceph_vino tvino, dvino;
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)
then show "trms_of_deg_leq k f (Suc rinfo->head-is_dentry, rinfo->ead-is_target);
unfolding trms_of_deg_leq_def
ceph_invalidate_dir_requestreq;
[of f s(uck f\otimes>\<bsub>PR\^esub monom P <one> ( ) "uc k + n"
by (metis P.m_closed P.r_neg P_def R.one_closed a_minus_def assms
cfs_minus cfs_zero *so weneedto thecorrect
qed
if
by (metis (no_types, lifting) assms le_iff_add less_Suc_eq_0_disj less_Suc_eq_le if(rr<0
qed
lemma trms_of_deg_leq_zero_is_ctrm:
assumes .ame -dname,
assumes "degree f > 0"
shows =(;
proof-
have "f = ctrm
dput(arent)
then "f ctrm f\<oplus><bsubP<esub ( []^bsub> R\<esub Suc 0\<otimes><bsub>P\<>( S 0) f))"
using P.nat_pow_eone P_def X_closed by auto
then
unfolding trms_of_deg_leq_def
by (metis (no_types, lifting) ctrm_is_poly One_nat_def P.add.right_cancel P.m_closed
Pminus_closed .nat_pow_eone P_def X_poly_def assms1 shift_closed
(d_inode(dn) ! . |
qed
lemma cfs_monom_mult:
assumes "p \<in> carrier P"
assumes "a \<in> carrier R"
assumes "k < n"
shows "p\otimes><^>P\<^esub>(P n)) <zero>java.lang.StringIndexOutOfBoundsException: Index 66 out of bounds for length 66
( [ofp)
apply (simp add if->_state &I_NEW)
apply (etis(o_types lifting)Pl_distr P.R.r_zeroR. assms() 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 \<in> carrier P"
assumes "a \<in> carrier R"
assumes "m < n"
shows "((monom P a n) \<otimes>\<^bsub>P\<^esub> f) m = \<zero>"
using cfs_monom_mult
by (simp add: P.m_comm assms(1) assms(2) assms(3))
lemma trms_of_deg_leq_cfs:
assumes " \in>carrier P"
shows" n f k ( <le>n (k) \<ero)
unfolding trms_of_deg_leq_def
apply(cases "k \<le> n")
using cfs_minus[of f struct inode *olddir =>;
cfs_monom_mult[of _ \<one> k "Suc n"]
apply (metis (no_types, lifting) P.m_closed /java.lang.StringIndexOutOfBoundsException: Index 51 out of bounds for length 51
cfs_add req->r_old_dentry-r_old_dentry, req->r_old_dentry, dn, dn);
trms_of_deg_leq_def trms_of_deg_leq_id')
doutcc,"dn% new offset %ld\"
unfolding trms_of_deg_leq_def
using assms trms_of_deg_leq_closed trms_of_deg_leq_def by auto
/*null dentry?*/
assumes "f \<in> carrier P"
trms_of_deg_leq( k)f=(trms_of_deg_leq k f) \<oplus\^bsub>P\^esub>monomP (f ( k))(Suc k)
proof fix x
show "trms_of_deg_leq (Suc k) f x = (trms_of_deg_leq k f \ ->lease,session,
apply( /* attach proper inode */
using trms_of_deg_leq_cfs =splice_dentry(req>_,in)java.lang.StringIndexOutOfBoundsException: Index 43 out of bounds for length 43
cfs_add[of doutc(l p linksto %p %llx.%llx, not %llx.%llx\n",
apply ( ceph_vinop();
using deg_leE assms cfs_monomapply auto[]
by (simp add: assms cfs_closed cfs_monom java.lang.StringIndexOutOfBoundsException: Index 49 out of bounds for length 34
lemma trms_of_deg_leq_0 BUG_ON(req>_dentry)java.lang.StringIndexOutOfBoundsException: Index 25 out of bounds for length 25
assumes "f \<in> carrier P"
f"
(etis One_nat_def Pr_null UP_zero_closed X_poly_defassms java.lang.StringIndexOutOfBoundsException: Range [101, 102) out of bounds for length 101
shift_onetrms_of_deg_leq_def trms_of_deg_leq_zero_is_ctrmtrunc_simps2 trunc_zero)
lemma trms_of_deg_leq_degree_f:
assumes "f \<in> carrier P"
shows iput();
proof fix 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
definitionintrc;
"lin_part f = trms_of_deg_leq 1 f"
lemma }
assumes "f \<in> carrier P"if( ){
shows "lin_part f = ( if (n-i_state I_NEW {
unfolding lin_part_def
by (simp add: assms trms_of_deg_leq_0 java.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 11
lemma(in UP_cring) lin_part_eq:
assumes "f \<in> carrier P"
>P\<^ (shift2 f) \<times\^sub>\<^esub>monomP\<ne 2"
unfolding lin_part_def
by (metis Suc_1 assms trms_of_deg_leq_id')
text\<open>Constant term of a substitution:\<close>
lemma zcf_eval:
assumes f \<in> carrierP"
shows "zcf f = to_fun f \<zero>"
-dentries (-f,0);
lemma ctrm_of_sub:
assumes "f \<in> carrier P"
assumes "g \<in> carrier P"
shows "zcf(f of g) = to_fun f (zcf g)"
apply(rule poly_induct3[of f])
apply (simp add: assms(1))
usingint =0 skipped =0,,i;
Rzero_closed zcf_to_fun 2 to_fun_sub monom_closed sub_closed presburger
text\<open>Evaluation of linear part:\<close>
lemma to_fun_lin_part:
assumes "f \<in> carrier P" /* mds understands offset_hash */
assumes "b \<in> carrier R"
shows "to_fun (lin_part f) b = (f 0) \<oplus> (f 1) \<otimes> b" (->dir_dir>)=frag)
using assms frag =le32_to_cpurinfo-dir_dir-frag;
by (simp >_eaddir_offset=2;
>Constantterm taylorexpansion\close
lemma taylor_zcf:
assumes "f \<in> carrier P"
assumes "a \<in> carrier R"
shows "zcf(T\<^bsub> cache_ctl.index = req-.index = req-r_readdir_cache_idx;
unfolding taylor_expansion_def
using ctrm_of_sub assms P_def zcf_eval java.lang.StringIndexOutOfBoundsException: Index 44 out of bounds for length 25
lemmainUP_cring)taylor_eq_1:
assumes "f \<in> carrier P"
assumes " <>carrier Rjava.lang.StringIndexOutOfBoundsException: Index 29 out of bounds for length 29
shows "(retry_lookup:
by (metis ,dname. dname.ame,dn)
assms() monom_one_Suc2 one_add_one trms_of_deg_leq_id)
lemma(in UP_cring) taylor_deg_1:
assumes "f \<in> carrier P"
assumes "a \<in> carrier R"
shows "fof (X_plus a) = (lin_part (T\\<bsub>a\<^esub>f) \oplus><^sub>\<esub>(shift(2:: (\^>a<^>f))\<otimes>\<>P\<^esub (^\<^P\^sub>(2:))"
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' d_delete(dn;
by java.lang.StringIndexOutOfBoundsException: Index 5 out of bounds for length 0
emmain UP_cring taylor_deg_1_eval:
assumes "f \<in> carrier P"
assumes "a \<in> carrier R"
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
assumes "c = to_fun (shift (2::nat) (T\<^bsub>a\<^esub> f)) b"
assumes "fa=to_funf a"
assumes "f'a = deriv f a"
shows "to_fun f (b \<oplus> a) = fa \<oplus> (f'a \<otimes> b) \<oplus> ( }
if (d_really_is_negative(dn)) {
proof-
have 0: "to_fun f (b \<oplus> a) = to_fun (f of (X_plus a)) b"
using
have 1: "to_fun (lin_part (T\<^bsub>a\<^esub> f)) b = fa \<oplus> ( }
using to_fun_lin_part[ "T\<^sub>a\<^>f"b
_ taylor_def UP_cring UP_cring.taylor_closed UP_cring_axioms zcf_defderivative_def
have 2: "(T\<^bsub>a\<^esub> f) = (lin_part (T\< err =retjava.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for length 14
using lin_part_eq[of "(T\ set_bit(CEPH_MDS_R_DID_PREPOPULATE, &req->r_req_flags);
by (metis taylor_def taylor_deg_1 req>r_readdir_cache_idx = cache_ctl.index;
then have doutccl "done\n";
using 1 2
_closed taylor_closed UP_mult_closed X_closedassms()assms2 assms(3
to_fun_plus lin_part_def shift_closed trms_of_deg_leq_closed)
then have "to_fun (T\<^bsub>a\<^esub inode)java.lang.StringIndexOutOfBoundsException: Index 28 out of bounds for length 28
by (simp add: taylor_closed X_closed assms(1) assms(2) assms(3) assms(4) to_fun_mult shift_closed
> (f'a \<otimes> b) <oplus> c \<times (X^\<^sub>P\^esub>(2:)b"
sing taylor_eval assms(1) assms()assms(3)) by auto
have"to_fun (X[]<bsub>P\<esub>(:nat) b=b^](2:"
by (metis P.nat_pow_Suc2 P.ifqfsc-i, ci-i_work) java.lang.StringIndexOutOfBoundsException: Index 46 out of bounds for length 46
nat_pow_eoneSuc_1
X_closed assms(3) to_fun_mult)
then show ?thesis
using 3 by auto
qed
lemma(in UP_cring) taylor_deg_1_eval':
assumes "f \<in> carrier P"
assumes "a \<in> carrier R"
spin_lock(ci-i_ceph_lock)
assumes " ((::nat) (<^sub>a\<> ) b"
assumes " = 1;
assumes "f'a = deriv f a"
shows "to_fun f (a \<oplus> b (invalidate_inode_pages2(inode>_mapping) 0) {
using R.add.m_comm taylor_deg_1_eval assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
by
lemma(in UP_cring) taylor_deg_1_eval'':
assumes "f \<in> carrier P"
assumes "a \<in> carrier inode,ceph_vinop(inode), orig_gen, ci->i_rdcache_gen,
assumes "b \<in> carrier R"
assumes "c = to_fun (shift (2::nat) (T\<^bsub> mutex_unlock(&->truncate_mutex;
shows "to_fun f (a \<ominus> b) = (to_fun f a) \<ominus>
proof-
have "\<ominus>b \ *that may depend on .
using assms
by blast
then have 0: "to_fun f (a \<ominus> b) = (to_fun f a)\<oplus> (java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
unfolding a_minus_def
using taylor_deg_1_eval return;
by auto
have 1: "<ominus> (deriv f a \<otimes> b) = (deriv f a \<otimes> (\<ominus>b))"
using assms
by (simp add: R.r_minus deriv_closed)
have 2: "(c \<otimes> b[^](2::nat)) = (c \<otimes> (\<ominus>b)[^](2::nat))"
using assms
by (metis R.add.inv_closed R.add.inv_solve_right R.l_zero R.java.lang.StringIndexOutOfBoundsException: Index 66 out of bounds for length 13
R.nat_pow_eone R.zero_closed Suc_1 UP_ring_axioms UP_ring_def
ringring_simprules(26)ring.27)
show ?thesis
using 0 1 2
a_minus_def
by simp
qed
lemma(in UP_cring
assumes "f \<in> java.lang.StringIndexOutOfBoundsException: Range [72, 23) out of bounds for length 72
" \in> carrierR
assumes "b \<in }
assumes
assumes "fa = java.lang.StringIndexOutOfBoundsException: Index 17 out of bounds for length 0
assumes "f'a = deriv f a"
shows "to_fun f (b) = fa \<oplus> f'a \<otimes> (b \<ominus> a) \<oplus> (c \<otimes> (b \<ominus> a)[^] iput();
proof-
obtain b' where b'_def: "b'= b \<ominus> a "
by simp
then have b'':" = b' <oplus> a"
using assms
by (metis R.add.inv_solve_right R.minus_closed R.minus_eq)
have
usingassms taylor_deg_1_evalof f a b' fa f'a] b_
by blast
have "f() =fa\oplus> (' \<otimes> b') \<oplus> (c \<otimes> b'[^](2::nat))"
using b'_def'
by auto
then show "to_fun f (b) = fa \<oplus>static const struct inode_operations ceph_symlink_iops = {
using b'_def
by . = ceph_listxattr,
qed
lemma(in UP_cring) Taylor_deg_1_expansion':
assumes "f \<in> carrier (UP R)"
assumes "a \<in> carrier R"
assumes "b \<in> carrier R"
"<c\in> carrier . to_fun f()=(f)\oplus deriv f a)\o (\<ominus> a) \<oplus> (c \<otimes> (b \<ominus> a)[^](2::nat))"
using[ b assms
by m P_defR. to_fun_closed)
text\ objverjava.lang.StringIndexOutOfBoundsException: Index 12 out of bounds for length 12
lemma n_mult_degree_bound:
assumes "f \<in> carrier P"
shows "degree (n_mult f) \<le> degree f"
apply(rule deg_leqI)
}
by ( add assms deg_leE n_mult_def)
pderiv_deg_0[]:
assumes "f \<in> carrier P"
assumes "degree f = 0"
shows "pderiv f = \<zero>\<^bsub>P\<^esub>"
if( < 0
have "degree (n_mult f) = 0"
using P_def n_mult_degree_bound
then show ?thesis
unfolding pderiv_def
by (simp add: assms(1) n_mult_closed poly_shift_degree_zero)
qed
lemmaderiv_deg_0
" <n>carrier "
assumes "degree f = 0"
assumes "a \<in> carrier R"
shows "deriv f a = \<zero>"
unfolding derivative_def taylor_expansion_def
using X_plus_closed assms(}else{
lemma poly_shift_monom':
assumes "a \<n carrier
"oly_shift (a <\^>\^>([]<bsub>\^esub( ))=a<><^bsub>\<esub>(X[]<b>\<e>"
using assms monom_rep_X_pow poly_shift_monom by auto
lemma monom_coeff:
assumes a \in R
;
using assms cfs_monom monom_rep_X_pow by auto
lemma cfs_n_mult:
assumes "p \<in> carrier P"
shows "n_mult p n = [n]\
by (impadd: n_mult_def)
lemma cfs_add_nat_pow:
assumes "p \<in> carrier P"
shows "([(n::nat)]\<cdot>\<^bsub>P\<^esub>p) k = [ int 20/
lyinductionn a :assms)
lemma:
p \in carrierP
shows " }
apply(induction n)
by(auto simp: add_pow_int_ge assms cfs_add_nat_pow add_pow_int_lt)
lemma add_nat_pow_monom =;
assumes "a \<in> carrier R"
shows java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
apply(rule ext)
by (simp add: assms cfs_add_nat_pow cfs_monom)
lemma add_int_pow_monom:
assumes "a \ spin_lock(ci-_eph_lock)
shows "[(n::int)]\<cdot>\<^bsub>P\<^esub>monom P a k = monom P
apply(rule ext)
by (simp add: assms cfs_add_int_pow cfs_monom)
lemma n_mult_monom:
assumes "a \<in> carrier R"
shows "n_mult (monom P a (Suc java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
apply(rule ext)
unfoldingn_mult_def
using >scrypt_auth_len len
lemma pderiv_monom:
assumes "a \<in> carrier R"
shows "pderiv err =-EINVAL;
apply(cases "n = 0")
apply (simp add: assms)
unfolding pderiv_def
)
poly_shift_monom
lemma pderiv_monom':
assumes "a \<in> carrier R"
shows "pderiv (a \<odot>\<^bsub>P\<^esub> X[^]\<^bsub>P\<^esub>(n::nat)) = ([n] fsgid =idmap,inode) attr->ia_vfsgid);
using assms pderiv_monom[of a n ]
by (simp add: P_def UP_cring. inode>_gid=fsgid;
lemma n_mult_add:
assumes "p \<in> carrier P"
assumes "q \<in> carrier P"
shows "n_mult( \oplus>\<bsub>P\^esub>q) = n_mult p <oplus><bsub>P\^sub n_mult q"
proof(rule ext) fix x show "n_mult (p {
using assms R.add.nat_pow_distrib[of "p x" "q x" x] cfs_add[of p q x req->r_args.etattr.mode=cpu_to_le32(attr>;
cfs_add[of "n_mult p" "n_mult q" x] n_mult_closed
struct timespec64java.lang.StringIndexOutOfBoundsException: Range [49, 43) out of bounds for length 51
by s add cfs_closed
qed
lemma pderiv_add:
assumes "p \<in> carrier P"
assumes "q \<in> carrier P"
shows "pderiv (p \<oplus>\<^bsub>P\<^esub> q) = pderiv p java.lang.StringIndexOutOfBoundsException: Range [59, 43) out of bounds for length 43
unfolding pderiv_def
using n_mult_add
by (simp add: n_mult_closed)
lemma zcf_monom_sub:
assumes "p \ req-r_argssetattr.size java.lang.StringIndexOutOfBoundsException: Index 29 out of bounds for length 29
shows "zcf ((monom P \<one> (Suc n)) of p) = zcf p [^] (Suc n)"
apply( 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 } else (do_sync& (issued &CEPH_CAP_FILE_EXCL)& attr>a_size > java.lang.StringIndexOutOfBoundsException: Index 83 out of bounds for length 83
using P_def UP_cring.ctrm_of_sub UP_cring_axioms -i_reported_size >ia_size
by fastforce
lemma zcf_monom_sub':
assumes "p \<in> carrier P"
assumes "a \<in> carrier R"
shows "zcf ((monom P a (Suc n)) of p) = a \<otimes> zcf p [^] req- =attr-ia_size;
Rzero_closed ctrm_of_sub to_fun_monom
zcf_to_fun to_fun_closed monom_closed by fastforce
assumes "a \<in> carrier R"
assumes "b \<in> carrier R"
shows "deriv (monom P a n) b = ([n]\<cdot>a)\<otimes>(b[^](n-1))"
proof( ( java.lang.StringIndexOutOfBoundsException: Range [45, 43) out of bounds for length 52
case 0
have 0: "b [^] ((0::nat) - 1) \<in> carrier R"
using assms
by simp
then show ?case unfolding derivative_def using assms doutc(cl, "%p %llx.%llx ctime %lld.%09ld -> %lld.%09ld (%s)\n",
by(metis .add.nat_pow_0.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] \<cdot> a \<otimes> b [^] (Suc n - 1) = a"
by ( by (simp&CEPH_CAP_XATTR_EXCLjava.lang.StringIndexOutOfBoundsException: Index 41 out of bounds for length 41
have T1}
using P.nat_pow_eone P_def True UP_a_closed X_closed assms(2) to_poly_closed by auto
then) {
unfolding derivative_def taylor_expansion_def
using T0 T1 True sub_monom(2)[of "X_plus b" a "Suc n"] ()java.lang.StringIndexOutOfBoundsException: Index 32 out of bounds for length 32
unfolding P_def X_poly_plus_def to_polynomial_def X_poly_def
by
nextjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
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
then have "deriv (monom P a (Suc n)) b = (((monom P a n) of (X_plus b)) \<otimes>\<^bsub>P\<^esub> }
using *The truncaterequestwill return -when the
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 * avoid corrupting filecontentswe toretry
then have "deriv (monom P a (Suc n)) b = (((monom P a n) of (X_plus b)) \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) \<oplus>\<^bsub>P\<^esub>
(((monom doutc(,"p%lx%result=d % locally,% ,retry !n,
unfolding X_poly_plus_def
by (metis Pout
then have "deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
unfolding 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 java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
then have /
by (simp add: derivative_def taylor_expansion_defint ceph_setattr(struct mnt_idmap *idmap,struct dentry *,
then have "deriv (monom P a (Suc n)) b = ((monom P a n) of (X_plus b)) 0 ceph_fs_client * ceph_inode_to_fs_client(node;
by (simp add: Suc)
then have 0:" (monom P ( n)) b (monom P a n of (_plus b)) 0\<oplus> ([]<cdot>a)\<times(b[^n)java.lang.StringIndexOutOfBoundsException: Index 117 out of bounds for length 117
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. = (, , ;
have 1: "((monom P a n) of (X_plus b)) 0 = a \<otimes> 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
assms()assms(2) to_fun_monom java.lang.StringIndexOutOfBoundsException: Range [122, 121) out of bounds for length 122
show ?thesis
using01R.ddnat_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 \<in> carrier R"
assumes "b \<in> carrier R"
assumes "g \<in> carrier P"
shows "deriv (a \<odot>\<^bsub>P\<^esub> g) b = a \<otimes> (deriv g b)"
unfolding*Thiscost muchwhen the Lockerstatetransitionand
using assms sub_smult X_plus_closed cfs_smult
by (imp )
lemma deriv_const:
assumes "a \<in> carrier R"
assumes "b \<in> carrier R"
shows "( P a 0) b =\<>"
unfolding derivative_def
java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
lemma deriv_monom_deg_one:
assumes "a \<in> carrier R"
assumes "b \<in> carrier R"
shows "deriv (monom P a 1) b = a"
unfolding derivative_def taylor_expansion_def
using assms cfs_X_plus[of (node))
by simp
lemma monom_Suc:
assumes "a \ ceph_mdsc_create_request(mdsc,CEPH_MDS_OP_GETATTR,mode)
req>r_inode= inode;
"monom P a (Suc n) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P \<one> 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)
(*************************************************************}else
(*******************************************************************************}
subsection\<open>The Product Rule\<close>
(*********intceph_do_getvxattr(tructinode *node const *name *,
(**************************************structceph_fs_client fsc=ceph_sb_to_fs_clientinode-is)
lemma(in UP_cring) times_x_product_rule:
assumes "f \<in> carrier
shows "pderiv (f \<otimes>\<^ err=-ENOMEM;
proof(rule poly_induct3[of f])
show "f \<in> carrier P"
using assms by blast
show "\<And>p q. q \<in> carrier P \<Longrightarrow>
p \<in> carrier P \<Longrightarrow>
pderiv (p \<otimes>\<^bsub>P\<^esub> up_ring =req->xattr_infoxattr_value_len
pderiv (q \<otimes>\<^bsub>P\<^esub> up_ring.monom Pjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) err=-RANGE;
proof-fixp A q\in carrierP"
"p \<in> carrier memcpy(value, xattr_value, xattr_value_len;
"pderiv (p \<otimes>\<^ doutc(, "%\" err)
"pderiv (q \<otimes>\<^bsub>P\<^esub>
have *Checkinodepermissions. We verify we have a valid value for
* the AUTHcap,then call the generichandler.
have 1: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P int mask)
unfolding 0 apply(rule pderiv_add)
using A is_UP_monomE(1) monom_is_UP_monom(1) apply return -ECHILDjava.lang.StringIndexOutOfBoundsException: Index 17 out of bounds for length 17
using A is_UP_monomE(1) monom_is_UP_monom(1) by blast
have 2: "pderiv ((p \<oplus>\<^java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
have 3: "pderiv ((p \< if (want & (STATX_MODE|STATX_U|STATX_GID||STATX_BTIME||STATX_CHANGE_COOKIE))
unfolding 2
* linklinkcount fordependsinode-i_subdirs
have 4: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) = p \<oplus>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> ((pderiv p \<oplus>\<^bsub>P\<^esub> pderiv q) \<otimes>\< *
unfolding 3 using A P}
show 5: "pderiv ( | CEPH_CAP_FILE_SHARED;
4 Abypresburger
qed
show "\<And>a n. a \<in> carrier R \<Longrightarrow>
*
proof- fix struct stat,u32 request_mask,unsigned int flags)
java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
struct ceph_inode_info *ci = ceph_inode();
have 1: "pderiv (up_ring.monom P a n \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) = [(Suc n)] \
unfolding 0 using A java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
(
have 2: "pderiv (up_ring.monom P a n \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) = if (err)
unfolding 1 using A P.add.nat_pow_Suc2 is_UP_monomE(1) monom_is_UP_monom(1) by blast
have 3: "pderiv (up_ring.monom P a n) \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1
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
by (metis if(equest_mask &STATX_CHANGE_COOKIE
show "pderiv (up_ring.monom P a n \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) =java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
unfolding 2 3 by blast
qed
qed
i UP_cring)deg_one_eval:
assumes g\in> java.lang.StringIndexOutOfBoundsException: Range [27, 26) out of bounds for length 34
assumes "deg R g = 1" spin_lock(pci-i_ceph_lock);
shows "\<And>t. if ()
proof-
obtain h where
by
stat>blksize =65536;
using assms unfolding h_def
by (metis ltrm_closed ltrm_eq_imp_deg_drop ltrm_monom P_def UP_car_memE(1) less_one)
have 1: "g \<ominus>\<^bsub>UP R\<^esub> h = to_poly (g 0)"
proof(rule ext) fix x show stat-> + +-i_subdirs;
proof stat>attributes | STATX_ATTR_CHANGE_MONOTONIC;
case
have T0: " 0 = \<zero>"
h_def usingassms ()
have T1: "(g \<ominus>\<^bsub>UP R\<^esub> h) 0 = g 0 \<void ceph_inode_shutdown(inode inode)
using ltrm_closed P_def assms(1) cfs_minus h_def by blast
then show
;
next
case False
0"
by presburger
then show ?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
have 2: "g = (g \<ominus>\<^bsub>UP R\<^esub> h) \<oplus>\<^bsub>UP R\<^esub> 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 \<in> carrier R"
have 3: " to_fun g t = to_fun (g \<ominus>\<^bsub>UP R\<^esub> h) t \<oplus> to_fun h t"
using 2
by (metis "1" A P_def UP_car_memE(1) assms(1) h_def monom_closed to_fun_plus to_polynomial_def)
then show "to_fun g t = g 0 \<oplus> g 1 \<otimes> t "
unfolding 1 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 nmult_smult:
assumes "a \<in> carrier R"
assumes "f \<in> carrier P"
shows "n_mult (a \<odot>\<^bsub>P\<^esub> f) = a \<odot>\<^bsub>P\<^esub> (n_mult f)"
apply(rule poly_induct4[of f])
apply (simp add: assms(2))
using assms(1) n_mult_add n_mult_closed smult_closed smult_r_distr apply presburger
using assms apply(intro ext, metis (no_types, lifting) ctrm_smult ltrm_deg_0 P_def R.add.nat_pow_0 UP_cring.ctrm_degree UP_cring.n_mult_closed UP_cring.n_mult_def UP_cring_axioms UP_smult_closed UP_zero_closed zcf_degree_zero zcf_zero deg_const deg_zero le_0_eq monom_closed n_mult_degree_bound smult_r_null)
using monom_mult_smult n_mult_monom assms
by (smt (verit) lcf_monom(1) P_def R.add.nat_pow_closed R.add_pow_rdistr R.zero_closed UP_cring.to_poly_mult_simp(1) UP_cring_axioms UP_smult_closed cfs_closed cring_lcf_mult monom_closed to_polynomial_def)
lemma pderiv_smult:
assumes "a \<in> carrier R"
assumes "f \<in> carrier P"
shows "pderiv (a \<odot>\<^bsub>P\<^esub> f) = a \<odot>\<^bsub>P\<^esub> (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 \<in> carrier P"
assumes "b \<in> carrier P"
shows "pderiv (a \<ominus>\<^bsub>P\<^esub> b) = pderiv a \<ominus>\<^bsub>P\<^esub> pderiv b"
proof-
have "\<ominus>\<^bsub>P\<^esub> b = (\<ominus>\<one>)\<odot>\<^bsub>P\<^esub>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 \<in> carrier R"
shows "pderiv (up_ring.monom P b 0) = \<zero>\<^bsub>P\<^esub>"
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 \<in> carrier P"
assumes "b \<in> carrier R"
shows "pderiv (a \<ominus>\<^bsub>P\<^esub> 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 \<in> carrier P"
assumes "a \<in> carrier R"
shows "pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n"
proof-
have "\<forall>f. f \<in> carrier P \<longrightarrow> pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n"
proof(induction n)
case 0
show ?case
proof fix f show "f \<in> carrier P \<longrightarrow> pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a 0) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0 "
proof assume A: "f \<in> carrier P"
have 0: "f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0 = a \<odot>\<^bsub>P\<^esub>f"
using assms A UP_m_comm is_UP_monomE(1) monom_is_UP_monom(1) monom_mult_is_smult by presburger
have 1: "f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a 0) = \<zero>\<^bsub>P\<^esub>"
using A assms P.r_null pderiv_const by presburger
have 2: "pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0 = a \<odot>\<^bsub>P\<^esub> 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 \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a 0) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a 0"
unfolding 0 1 2 using A UP_l_zero UP_smult_closed assms(2) pderiv_closed pderiv_smult by presburger
qed
qed
next
case (Suc n)
show "\<forall>f. f \<in> carrier P \<longrightarrow>
pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a (Suc n)) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)"
proof fix f
show "f \<in> carrier P \<longrightarrow>
pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a (Suc n)) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)"
proof
assume A: "f \<in> carrier P"
show " pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a (Suc n)) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)"
proof(cases "n = 0")
case True
have 0: "(f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = a \<odot>\<^bsub>P\<^esub> f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1"
proof -
have "\<forall>n. up_ring.monom P a n \<in> carrier P"
using assms(2) is_UP_monomE(1) monom_is_UP_monom(1) by presburger
then show ?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
have 1: "f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a (Suc n)) = a \<odot>\<^bsub>P\<^esub> 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)
have 2: "pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n) = a \<odot>\<^bsub>P\<^esub> (pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1)"
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)
have 3: "a \<odot>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> (pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) = a \<odot>\<^bsub>P\<^esub> (f \<oplus>\<^bsub>P\<^esub>(pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 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
unfolding 0 1 2 3
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 \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n) = (f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv (f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n"
using Suc A P.m_closed R.one_closed is_UP_monomE(1) is_UP_monomI by presburger
have 0: "f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n) = (f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> 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
have 1: "(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv (f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n =
(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> (f \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n "
using A times_x_product_rule by presburger
have 2: "(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) =(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P ([n]\<cdot>a) n)"
proof-
have 20: "up_ring.monom P ([n] \<cdot> a) (n) = up_ring.monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> up_ring.monom P ([n] \<cdot> a) (n - 1)"
using A assms False monom_mult[of \<one> "[n]\<cdot>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 unfolding 20 using 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
have 3: "(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P ([n]\<cdot>a) n) = [n]\<cdot>\<^bsub>P\<^esub>(f \<otimes>\<^bsub>P\<^esub>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))
have 4: "pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) = (f \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1)"
using times_x_product_rule A by blast
have 5: " (f \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n =
(f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n ) \<oplus>\<^bsub>P\<^esub> (pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> 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)
have 6: " (f \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n =
(f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n ) \<oplus>\<^bsub>P\<^esub> (pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n )"
using A assms False 5 by blast
have 7: "(f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv (f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n =
[(Suc n)] \<cdot>\<^bsub>P\<^esub> (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n"
unfolding 2 3 5 6 using 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)
have 8: "pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = pderiv ((f \<otimes>\<^bsub>P\<^esub>up_ring.monom P \<one> 1) \<otimes>\<^bsub>P\<^esub> up_ring.monom P a n)"
using A assms 0 by presburger
show " pderiv (f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)) = f \<otimes>\<^bsub>P\<^esub> pderiv (up_ring.monom P a (Suc n)) \<oplus>\<^bsub>P\<^esub> pderiv f \<otimes>\<^bsub>P\<^esub> up_ring.monom P a (Suc n)"
unfolding 8 IH 0 1 2 3 4 5 6
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 \<in> carrier (UP R)"
assumes "g \<in> carrier (UP R)"
shows "pderiv (f \<otimes>\<^bsub>UP R\<^esub>g) = (pderiv f \<otimes>\<^bsub>UP R\<^esub> g) \<oplus>\<^bsub>UP R\<^esub> (f \<otimes>\<^bsub>UP R\<^esub> pderiv g)"
proof(rule poly_induct3[of f])
show "f \<in> carrier P"
using assms unfolding P_def by blast
show "\<And>p q. q \<in> carrier P \<Longrightarrow>
p \<in> carrier P \<Longrightarrow>
pderiv (p \<otimes>\<^bsub>UP R\<^esub> g) = pderiv p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> p \<otimes>\<^bsub>UP R\<^esub> pderiv g \<Longrightarrow>
pderiv (q \<otimes>\<^bsub>UP R\<^esub> g) = pderiv q \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> pderiv g \<Longrightarrow>
pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = pderiv (p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> pderiv g"
proof- fix p q
assume A: "q \<in> carrier P" "p \<in> carrier P"
"pderiv (p \<otimes>\<^bsub>UP R\<^esub> g) = pderiv p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> p \<otimes>\<^bsub>UP R\<^esub> pderiv g"
"pderiv (q \<otimes>\<^bsub>UP R\<^esub> g) = pderiv q \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> pderiv g"
have 0: "(p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g = p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> g"
using A assms unfolding P_def using P_def UP_l_distr by blast
have 1: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = pderiv (p \<otimes>\<^bsub>UP R\<^esub> g) \<oplus>\<^bsub>UP R\<^esub> pderiv (q \<otimes>\<^bsub>UP R\<^esub> g)"
unfolding 0 using pderiv_add[of "p \<otimes>\<^bsub>P\<^esub> g" "q \<otimes>\<^bsub>P\<^esub> g"] unfolding P_def
using A(1) A(2) P_def UP_mult_closed assms(2) by blast
have 2: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = pderiv p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> p \<otimes>\<^bsub>UP R\<^esub> pderiv g \<oplus>\<^bsub>UP R\<^esub> (pderiv q \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> pderiv g)"
unfolding 1 A by blast
have 3: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = pderiv p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> pderiv q \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> p \<otimes>\<^bsub>UP R\<^esub> pderiv g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> pderiv g"
using A assms by (metis "1" P.add.m_assoc P.add.m_lcomm P.m_closed P_def pderiv_closed)
have 4: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = (pderiv p \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> pderiv q \<otimes>\<^bsub>UP R\<^esub> g) \<oplus>\<^bsub>UP R\<^esub> (p \<otimes>\<^bsub>UP R\<^esub> pderiv g \<oplus>\<^bsub>UP R\<^esub> q \<otimes>\<^bsub>UP R\<^esub> pderiv g)"
unfolding 3 using A assms P_def UP_a_assoc UP_a_closed UP_mult_closed pderiv_closed by auto
have 5: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = ((pderiv p \<oplus>\<^bsub>UP R\<^esub> pderiv q) \<otimes>\<^bsub>UP R\<^esub> g) \<oplus>\<^bsub>UP R\<^esub> ((p \<oplus>\<^bsub>UP R\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> pderiv g)"
unfolding 4 using A assms by (metis P.l_distr P_def pderiv_closed)
have 6: "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = ((pderiv (p \<oplus>\<^bsub>P\<^esub> q)) \<otimes>\<^bsub>UP R\<^esub> g) \<oplus>\<^bsub>UP R\<^esub> ((p \<oplus>\<^bsub>UP R\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> pderiv g)"
unfolding 5 using A assms
by (metis P_def pderiv_add)
show "pderiv ((p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g) = pderiv (p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>UP R\<^esub> pderiv g"
unfolding 6 using A assms P_def by blast
qed
show "\<And>a n. a \<in> carrier R \<Longrightarrow>
pderiv (up_ring.monom P a n \<otimes>\<^bsub>UP R\<^esub> g) = pderiv (up_ring.monom P a n) \<otimes>\<^bsub>UP R\<^esub> g \<oplus>\<^bsub>UP R\<^esub> up_ring.monom P a n \<otimes>\<^bsub>UP R\<^esub> 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
(**************************************************************************************************)
(**************************************************************************************************)
subsection\<open>The Chain Rule\<close>
(**************************************************************************************************)
(**************************************************************************************************)
lemma(in UP_cring) chain_rule:
assumes "f \<in> carrier P"
assumes "g \<in> carrier P"
shows "pderiv (compose R f g) = compose R (pderiv f) g \<otimes>\<^bsub>UP R\<^esub> pderiv g"
proof(rule poly_induct3[of f])
show "f \<in> carrier P"
using assms by blast
show "\<And>p q. q \<in> carrier P \<Longrightarrow>
p \<in> carrier P \<Longrightarrow>
pderiv (Cring_Poly.compose R p g) = Cring_Poly.compose R (pderiv p) g \<otimes>\<^bsub>UP R\<^esub> pderiv g \<Longrightarrow>
pderiv (Cring_Poly.compose R q g) = Cring_Poly.compose R (pderiv q) g \<otimes>\<^bsub>UP R\<^esub> pderiv g \<Longrightarrow>
pderiv (Cring_Poly.compose R (p \<oplus>\<^bsub>P\<^esub> q) g) = Cring_Poly.compose R (pderiv (p \<oplus>\<^bsub>P\<^esub> q)) g \<otimes>\<^bsub>UP R\<^esub> 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 "\<And>a n. a \<in> carrier R \<Longrightarrow>
pderiv (compose R (up_ring.monom P a n) g) = compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>UP R\<^esub> pderiv g"
proof-
fix a n assume A: "a \<in> carrier R"
show "pderiv (compose R (up_ring.monom P a n) g) = compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>UP R\<^esub> pderiv g"
proof(induction n)
case 0
have 00: "(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
have 01: "pderiv (up_ring.monom P a 0) = \<zero>\<^bsub>P\<^esub>"
using A pderiv_const by blast
show ?case unfolding 00 01
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 \<otimes>\<^bsub>UP R\<^esub> pderiv g"
proof(cases "n = 0")
case True
have 0: "compose R (up_ring.monom P a (Suc n)) g = a \<odot>\<^bsub>P\<^esub> g"
using A assms sub_monom_deg_one[of g a] unfolding True using One_nat_def
by presburger
have 1: "(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) = \<zero>\<^bsub>P\<^esub>"
using A pderiv_const by blast
then show "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
then show ?thesis unfolding 0 1
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
have 0: "compose R (up_ring.monom P a (Suc n)) g = (compose R (up_ring.monom P a n) g) \<otimes>\<^bsub>P\<^esub> (compose R (up_ring.monom P \<one> 1) g)"
using assms A by (metis R.one_closed monom_Suc(2) monom_closed sub_mult)
have 1: "compose R (up_ring.monom P a (Suc n)) g = (compose R (up_ring.monom P a n) g) \<otimes>\<^bsub>P\<^esub> g"
unfolding 0 using 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))
have 2: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) =
((pderiv (compose R (up_ring.monom P a n) g)) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> ((compose R (up_ring.monom P a n) g) \<otimes>\<^bsub>P\<^esub> pderiv g)"
unfolding 1 unfolding 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
have 3: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) =
(compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>UP R\<^esub> pderiv g \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> ((compose R (up_ring.monom P a n) g) \<otimes>\<^bsub>P\<^esub> pderiv g)"
unfolding 2 Suc by blast
have 4: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) =
((compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>P\<^esub> g) \<otimes>\<^bsub>UP R\<^esub> pderiv g) \<oplus>\<^bsub>P\<^esub> ((compose R (up_ring.monom P a n) g) \<otimes>\<^bsub>P\<^esub> pderiv g)"
unfolding 3 using A assms m_assoc m_comm
by (smt (verit) P_def monom_closed monom_rep_X_pow pderiv_closed sub_closed)
have 5: "pderiv (compose R (up_ring.monom P a (Suc n)) g ) =
((compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> (compose R (up_ring.monom P a n) g)) \<otimes>\<^bsub>P\<^esub> pderiv g"
unfolding 4 using A assms
by (metis P.l_distr P.m_closed P_def UP_cring.pderiv_closed UP_cring_axioms monom_closed sub_closed)
have 6: "compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>P\<^esub> g = [n]\<cdot>\<^bsub>P\<^esub>compose R ((up_ring.monom P a n)) g"
proof-
have 60: "(pderiv (up_ring.monom P a n)) = (up_ring.monom P ([n]\<cdot>a) (n-1))"
using A assms pderiv_monom by blast
have 61: "compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>P\<^esub> g = compose R ((up_ring.monom P ([n]\<cdot>a) (n-1))) g \<otimes>\<^bsub>P\<^esub> (compose R (up_ring.monom P \<one> 1) g)"
unfolding 60 using A assms sub_monom_deg_one[of g \<one> ] R.one_closed smult_one by presburger
have 62: "compose R (pderiv (up_ring.monom P a n)) g \<otimes>\<^bsub>P\<^esub> g = compose R (up_ring.monom P ([n]\<cdot>a) n) g"
unfolding 61 using False A assms sub_mult[of g "up_ring.monom P ([n] \<cdot> a) (n - 1)" "up_ring.monom P \<one> 1" ] monom_mult[of "[n]\<cdot>a" \<one> "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)
have 63: "\<And>k::nat. Cring_Poly.compose R (up_ring.monom P ([k] \<cdot> a) n) g = [k] \<cdot>\<^bsub>P\<^esub>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] \<cdot> a) n) g = [k] \<cdot>\<^bsub>P\<^esub>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] \<cdot> a) n) g =
[k] \<cdot>\<^bsub>P\<^esub> Cring_Poly.compose R (monom P a n) g"
have 0: "(monom P ([Suc k] \<cdot> a) n) = [Suc k] \<cdot> a \<odot>\<^bsub>P\<^esub>(monom P \<one> n)"
by (simp add: A monic_monom_smult)
have 1: "(monom P ([Suc k] \<cdot> a) n) = [k] \<cdot> a \<odot>\<^bsub>P\<^esub>(monom P \<one> n) \<oplus>\<^bsub>P\<^esub>a \<odot>\<^bsub>P\<^esub>(monom P \<one> n) "
unfolding 0
by (simp add: A UP_smult_l_distr)
show "Cring_Poly.compose R (monom P ([Suc k] \<cdot> a) n) g =
[Suc k] \<cdot>\<^bsub>P\<^esub> (Cring_Poly.compose R (monom P a n) g) "
unfolding 1
by (simp add: A a assms(2) monic_monom_smult sub_add)
qed
qed
have 64: "Cring_Poly.compose R (up_ring.monom P ([n] \<cdot> a) n) g = [n] \<cdot>\<^bsub>P\<^esub>Cring_Poly.compose R (up_ring.monom P a n) g"
using 63 by blast
show ?thesis unfolding 62 64 by blast
qed
have 63: "\<And>k::nat. Cring_Poly.compose R (up_ring.monom P ([k] \<cdot> a) n) g = [k] \<cdot>\<^bsub>P\<^esub>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] \<cdot> a) n) g = [k] \<cdot>\<^bsub>P\<^esub>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
have 7: "([n] \<cdot>\<^bsub>P\<^esub> Cring_Poly.compose R (up_ring.monom P a n) g \<oplus>\<^bsub>P\<^esub> Cring_Poly.compose R (up_ring.monom P a n) g) =
[Suc n] \<cdot>\<^bsub>P\<^esub> (Cring_Poly.compose R (up_ring.monom P a n) g)"
using A assms P.add.nat_pow_Suc by presburger
have 8: "[Suc n] \<cdot>\<^bsub>P\<^esub> Cring_Poly.compose R (up_ring.monom P a n) g \<otimes>\<^bsub>P\<^esub> pderiv g = Cring_Poly.compose R (up_ring.monom P ([Suc n] \<cdot> a) n) g \<otimes>\<^bsub>P\<^esub> pderiv g"
unfolding 63[of "Suc n"] by blast
show ?thesis unfolding 5 6 7 8 using 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 \<in> carrier R"
assumes "b \<in> carrier R"
assumes "q \<in> carrier P"
shows "deriv ((monom P a n) \<otimes>\<^bsub>P\<^esub> q) b = (deriv (monom P a n) b) \<otimes> (to_fun q b) \<oplus> (to_fun (monom P a n) b) \<otimes> deriv q b"
proof(rule poly_induct3[of q])
show "q \<in> carrier P"
using assms by simp
show " \<And>p q. q \<in> carrier P \<Longrightarrow>
p \<in> carrier P \<Longrightarrow>
deriv (monom P a n \<otimes>\<^bsub>P\<^esub> p) b = deriv (monom P a n) b \<otimes> to_fun p b \<oplus> to_fun (monom P a n) b \<otimes> deriv p b \<Longrightarrow>
deriv (monom P a n \<otimes>\<^bsub>P\<^esub> q) b = deriv (monom P a n) b \<otimes> to_fun q b \<oplus> to_fun (monom P a n) b \<otimes> deriv q b \<Longrightarrow>
deriv (monom P a n \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q)) b = deriv (monom P a n) b \<otimes> to_fun (p \<oplus>\<^bsub>P\<^esub> q) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (p \<oplus>\<^bsub>P\<^esub> q) b"
proof- fix p q assume A: "q \<in> carrier P" " p \<in> carrier P"
"deriv (monom P a n \<otimes>\<^bsub>P\<^esub> p) b = deriv (monom P a n) b \<otimes> to_fun p b \<oplus> to_fun (monom P a n) b \<otimes> deriv p b"
"deriv (monom P a n \<otimes>\<^bsub>P\<^esub> q) b = deriv (monom P a n) b \<otimes> to_fun q b \<oplus> to_fun (monom P a n) b \<otimes> deriv q b"
have "deriv (monom P a n \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q)) b = deriv (monom P a n) b \<otimes> to_fun p b \<oplus> to_fun (monom P a n) b \<otimes> deriv p b
\<oplus>deriv (monom P a n) b \<otimes> to_fun q b \<oplus> to_fun (monom P a n) b \<otimes> 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 \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q)) b = deriv (monom P a n) b \<otimes> to_fun p b \<oplus>deriv (monom P a n) b \<otimes> to_fun q b
\<oplus> to_fun (monom P a n) b \<otimes> deriv p b \<oplus> to_fun (monom P a n) b \<otimes> 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 \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q)) b = deriv (monom P a n) b \<otimes> (to_fun p b \<oplus> to_fun q b)
\<oplus> to_fun (monom P a n) b \<otimes> (deriv p b \<oplus> 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 \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q)) b = deriv (monom P a n) b \<otimes> to_fun (p \<oplus>\<^bsub>P\<^esub> q) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (p \<oplus>\<^bsub>P\<^esub> q) b"
by (simp add: A(1) A(2) assms(2) deriv_add to_fun_plus)
qed
show "\<And>c m. c \<in> carrier R \<Longrightarrow> deriv (monom P a n \<otimes>\<^bsub>P\<^esub> monom P c m) b =
deriv (monom P a n) b \<otimes> to_fun (monom P c m) b
\<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b"
proof- fix c m assume A: "c \<in> carrier R"
show "deriv (monom P a n \<otimes>\<^bsub>P\<^esub> monom P c m) b = deriv (monom P a n) b \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b"
proof(cases "n = 0")
case True
have LHS: "deriv (monom P a n \<otimes>\<^bsub>P\<^esub> monom P c m) b = deriv (monom P (a \<otimes> c) m) b"
by (metis A True add.left_neutral assms(1) monom_mult)
have RHS: "deriv (monom P a n) b \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b
= a \<otimes> 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 \<otimes>\<^bsub>P\<^esub> monom P c m) b = deriv (monom P (a \<otimes> c) n) b"
by (metis A True add.comm_neutral assms(1) monom_mult)
have RHS: "deriv (monom P a n) b \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b
= c \<otimes> 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 \<otimes>\<^bsub>P\<^esub> monom P c m) b = [(n + m)] \<cdot> (a \<otimes> c) \<otimes> b [^] (n + m - 1)"
using deriv_monom[of "a \<otimes> 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 \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b
= [n]\<cdot>a \<otimes>(b[^](n-1)) \<otimes> c \<otimes> b[^]m \<oplus> a \<otimes> b[^]n \<otimes> [m]\<cdot>c \<otimes>(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)
have 0: "[n]\<cdot>a \<otimes> (b[^](n-1)) \<otimes> c \<otimes> b[^]m = [n]\<cdot>a \<otimes> c \<otimes> b[^](n + m -1) "
proof-
have "[n]\<cdot>a \<otimes> (b[^](n-1)) \<otimes> c \<otimes> b[^]m = [n]\<cdot>a \<otimes> c \<otimes> (b[^](n-1)) \<otimes> b[^]m"
by (simp add: A R.m_lcomm R.semiring_axioms assms(1) assms(2) semiring.semiring_simprules(8))
hence "[n]\<cdot>a \<otimes> (b[^](n-1)) \<otimes> c \<otimes> b[^]m = [n]\<cdot>a \<otimes> c \<otimes> ((b[^](n-1)) \<otimes> 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
have 1: "a \<otimes> b[^]n \<otimes> [m]\<cdot>c \<otimes>(b[^](m-1)) = a \<otimes> [m]\<cdot>c \<otimes> b[^](n + m -1)"
proof-
have "a \<otimes> b[^]n \<otimes> [m]\<cdot>c \<otimes>(b[^](m-1)) = a \<otimes> [m]\<cdot>c \<otimes> b[^]n \<otimes>(b[^](m-1))"
using A R.m_comm R.m_lcomm assms(1) assms(2) by auto
hence "a \<otimes> b[^]n \<otimes> [m]\<cdot>c \<otimes>(b[^](m-1)) = a \<otimes> [m]\<cdot>c \<otimes> (b[^]n \<otimes>(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 \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b
= [n]\<cdot>a \<otimes> c \<otimes> b[^](n + m -1) \<oplus> a \<otimes> [m]\<cdot>c \<otimes> b[^](n + m -1)"
using LHS 0 1
by simp
hence LHS: "deriv (monom P a n) b \<otimes> to_fun (monom P c m) b \<oplus> to_fun (monom P a n) b \<otimes> deriv (monom P c m) b
= [n]\<cdot> (a \<otimes> c \<otimes> b[^](n + m -1)) \<oplus> [m]\<cdot> (a \<otimes> c \<otimes> 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 \<in> carrier P"
assumes "q \<in> carrier P"
assumes "a \<in> carrier R"
shows "deriv (p \<otimes>\<^bsub>P\<^esub> q) a = deriv p a \<otimes> (to_fun q a) \<oplus> (to_fun p a) \<otimes> deriv q a"
proof(rule poly_induct3[of p])
show "p \<in> carrier P"
using assms(1) by simp
show " \<And>p qa.
qa \<in> carrier P \<Longrightarrow>
p \<in> carrier P \<Longrightarrow>
deriv (p \<otimes>\<^bsub>P\<^esub> q) a = deriv p a \<otimes> to_fun q a \<oplus> to_fun p a \<otimes> deriv q a \<Longrightarrow>
deriv (qa \<otimes>\<^bsub>P\<^esub> q) a = deriv qa a \<otimes> to_fun q a \<oplus> to_fun qa a \<otimes> deriv q a \<Longrightarrow>
deriv ((p \<oplus>\<^bsub>P\<^esub> qa) \<otimes>\<^bsub>P\<^esub> q) a = deriv (p \<oplus>\<^bsub>P\<^esub> qa) a \<otimes> to_fun q a \<oplus> to_fun (p \<oplus>\<^bsub>P\<^esub> qa) a \<otimes> deriv q a"
proof- fix f g assume A: "f \<in> carrier P" "g \<in> carrier P"
"deriv (f \<otimes>\<^bsub>P\<^esub> q) a = deriv f a \<otimes> to_fun q a \<oplus> to_fun f a \<otimes> deriv q a"
"deriv (g \<otimes>\<^bsub>P\<^esub> q) a = deriv g a \<otimes> to_fun q a \<oplus> to_fun g a \<otimes> deriv q a"
have "deriv ((f \<oplus>\<^bsub>P\<^esub> g) \<otimes>\<^bsub>P\<^esub> q) a = deriv f a \<otimes> to_fun q a \<oplus> to_fun f a \<otimes> deriv q a \<oplus>
deriv g a \<otimes> to_fun q a \<oplus> to_fun g a \<otimes> 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 \<oplus>\<^bsub>P\<^esub> g) \<otimes>\<^bsub>P\<^esub> q) a = deriv f a \<otimes> to_fun q a \<oplus> deriv g a \<otimes> to_fun q a \<oplus>
to_fun f a \<otimes> deriv q a \<oplus> to_fun g a \<otimes> 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 \<oplus>\<^bsub>P\<^esub> g) \<otimes>\<^bsub>P\<^esub> q) a = (deriv f a \<otimes> to_fun q a \<oplus> deriv g a \<otimes> to_fun q a) \<oplus>
(to_fun f a \<otimes> deriv q a \<oplus> to_fun g a \<otimes> 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 \<oplus>\<^bsub>P\<^esub> g) \<otimes>\<^bsub>P\<^esub> q) a = deriv (f \<oplus>\<^bsub>P\<^esub> g) a \<otimes> to_fun q a \<oplus> to_fun (f \<oplus>\<^bsub>P\<^esub> g) a \<otimes> 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 "\<And>aa n. aa \<in> carrier R \<Longrightarrow> deriv (monom P aa n \<otimes>\<^bsub>P\<^esub> q) a = | | |