Theory Function_Ring
theory Function_Ring
imports "HOL-Algebra.Ring" "HOL-Library.FuncSet" "HOL-Algebra.Module"
begin
text‹
This theory formalizes basic facts about the ring of extensional functions from a fixed set to
a fixed ring. This will be useful for providing a generic framework for various constructions
related to the $p$-adics such as polynomial evaluation and sequences. The rings of semialgebraic
functions will be defined as subrings of these function rings, which will be necessary for the
proof of $p$-adic quantifier elimination.
›
section‹The Ring of Extensional Functions from a Fixed Base Set to a Fixed Base Ring›
subsection‹Basic Operations on Extensional Functions›
definition function_mult:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_mult S R f g = (λx ∈ S. (f x) ⊗⇘R⇙ (g x))"
abbreviation(input) ring_function_mult:: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_mult R f g ≡ function_mult (carrier R) R f g"
definition function_add:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_add S R f g = (λx ∈ S. (f x) ⊕⇘R⇙ (g x))"
abbreviation(input) ring_function_add:: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_add R f g ≡ function_add (carrier R) R f g"
definition function_one:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a)" where
"function_one S R = (λx ∈ S. 𝟭⇘R⇙)"
abbreviation(input) ring_function_one :: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a)" where
"ring_function_one R ≡ function_one (carrier R) R"
definition function_zero:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a)" where
"function_zero S R = (λx ∈ S. 𝟬⇘R⇙)"
abbreviation(input) ring_function_zero :: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a)" where
"ring_function_zero R ≡ function_zero (carrier R) R"
definition function_uminus:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_uminus S R a = (λ x ∈ S. ⊖⇘R⇙ (a x))"
definition ring_function_uminus:: " ('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_uminus R a = function_uminus (carrier R) R a"
definition function_scalar_mult:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ 'a ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_scalar_mult S R a f = (λ x ∈ S. a ⊗⇘R⇙ (f x))"
subsection‹Defining the Ring of Extensional Functions›
definition function_ring:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ( 'a, 'c ⇒ 'a) module" where
"function_ring S R = ⦇
carrier = extensional_funcset S (carrier R),
Group.monoid.mult = (function_mult S R),
one = (function_one S R),
zero = (function_zero S R),
add = (function_add S R),
smult = function_scalar_mult S R ⦈ "
text‹The following locale consists of a struct R, and a distinguished set S which is meant to serve as the domain for a ring of functions $S \to carrier R$. ›
locale struct_functions =
fixes R ::"('a, 'b) partial_object_scheme" (structure)
and S :: "'c set"
text‹The following are locales which fix a ring R (which may be commutative, a domain, or a field) and a function ring F of extensional functions from a fixed set S to $carrier R$›
locale ring_functions = struct_functions + R?: ring R +
fixes F (structure)
defines F_def: "F ≡ function_ring S R"
locale cring_functions = ring_functions + R?: cring R
locale domain_functions = ring_functions + R?: domain R
locale field_functions = ring_functions + R?: field R
sublocale cring_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale domain_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale domain_functions < cring_functions
apply (simp add: cring_functions_def is_cring ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < domain_functions
apply (simp add: domain_axioms domain_functions_def ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < cring_functions
apply (simp add: cring_functions_axioms)
by (simp add: F_def)
abbreviation(input) ring_function_ring:: "('a, 'b) ring_scheme ⇒ ('a, 'a ⇒ 'a) module" ("Fun") where
"ring_function_ring R ≡ function_ring (carrier R) R"
subsection‹Algebraic Properties of the Basic Operations›
subsubsection‹Basic Carrier Facts›
lemma(in ring_functions) function_ring_defs:
"carrier F = extensional_funcset S (carrier R)"
"(⊗⇘F⇙) = (function_mult S R)"
"(⊕⇘F⇙) = (function_add S R)"
"𝟭⇘F⇙ = function_one S R"
"𝟬⇘F⇙ = function_zero S R"
"(⊙⇘F⇙) = function_scalar_mult S R"
unfolding F_def
by ( auto simp add: function_ring_def)
lemma(in ring_functions) function_ring_car_memE:
assumes "a ∈ carrier F"
shows "a ∈ extensional S"
"a ∈ S → carrier R"
using assms function_ring_defs apply auto[1]
using assms function_ring_defs PiE_iff apply blast
using assms function_ring_defs(1) by fastforce
lemma(in ring_functions) function_ring_car_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "f a ∈ carrier R"
using assms unfolding function_ring_def F_def by auto
lemma(in ring_functions) function_ring_not_car:
assumes "a ∉ S"
assumes "f ∈ carrier F"
shows "f a = undefined"
using assms unfolding function_ring_def F_def by auto
lemma(in ring_functions) function_ring_car_eqI:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
assumes "⋀a. a ∈ S ⟹ f a = g a"
shows "f = g"
using assms(1) assms(2) assms(3) extensionalityI function_ring_car_memE(1) by blast
lemma(in ring_functions) function_ring_car_memI:
assumes "⋀a. a ∈ S ⟹ f a ∈ carrier R"
assumes "⋀ a. a ∉ S⟹ f a = undefined"
shows "f ∈ carrier F"
using function_ring_defs assms
unfolding extensional_funcset_def
by (simp add: ‹⋀a. a ∈ S ⟹ f a ∈ carrier R› extensional_def)
lemma(in ring) function_ring_car_memI:
assumes "⋀a. a ∈ S ⟹ f a ∈ carrier R"
assumes "⋀ a. a ∉ S⟹ f a = undefined"
shows "f ∈ carrier (function_ring S R)"
by (simp add: assms(1) assms(2) local.ring_axioms ring_functions.function_ring_car_memI ring_functions.intro)
subsubsection‹Basic Multiplication Facts›
lemma(in ring_functions) function_mult_eval_car:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊗⇘F⇙ g) a = (f a) ⊗ (g a)"
using assms function_ring_defs
unfolding function_mult_def
by simp
lemma(in ring_functions) function_mult_eval_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊗⇘F⇙ g) a ∈ carrier R"
using assms function_mult_eval_car
using F_def ring_functions.function_ring_car_closed ring_functions_axioms by fastforce
lemma(in ring_functions) fun_mult_closed:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "f ⊗⇘F⇙ g ∈ carrier F"
apply(rule function_ring_car_memI)
apply (simp add: assms(1) assms(2) function_mult_eval_closed)
by (simp add: function_mult_def function_ring_defs(2))
lemma(in ring_functions) fun_mult_eval_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
assumes "a ∈ S"
shows "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a"
proof-
have 0: "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) a = (x a) ⊗ (y a) ⊗ (z a) "
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_mult_closed function_mult_eval_car)
have 1: "(x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a = (x a) ⊗ ((y a) ⊗ (z a))"
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_mult_closed function_mult_eval_car)
have 2:"(x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a = (x a) ⊗ (y a) ⊗ (z a)"
using 1 assms
by (simp add: function_ring_car_closed m_assoc)
show ?thesis
using 0 2 by auto
qed
lemma(in ring_functions) fun_mult_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes "z ∈ carrier F"
shows "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) = (x ⊗⇘F⇙ (y ⊗⇘F⇙ z))"
using fun_mult_eval_assoc[of x]
by (simp add: assms(1) assms(2) assms(3) fun_mult_closed function_ring_car_eqI)
subsubsection‹Basic Addition Facts›
lemma(in ring_functions) fun_add_eval_car:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊕⇘F⇙ g) a = (f a) ⊕ (g a)"
by (simp add: assms(1) function_add_def function_ring_defs(3))
lemma(in ring_functions) fun_add_eval_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊕⇘F⇙ g) a ∈ carrier R"
using assms unfolding F_def
using F_def fun_add_eval_car function_ring_car_closed
by auto
lemma(in ring_functions) fun_add_closed:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "f ⊕⇘F⇙ g ∈ carrier F"
apply(rule function_ring_car_memI)
using assms unfolding F_def
using F_def fun_add_eval_closed apply blast
by (simp add: function_add_def function_ring_def)
lemma(in ring_functions) fun_add_eval_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
assumes "a ∈ S"
shows "(x ⊕⇘F⇙ y ⊕⇘F⇙ z) a = (x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a"
proof-
have 0: "(x ⊕⇘F⇙ y ⊕⇘F⇙ z) a = (x a) ⊕ (y a) ⊕ (z a) "
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_add_closed fun_add_eval_car)
have 1: "(x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a = (x a) ⊕ ((y a) ⊕ (z a))"
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_add_closed fun_add_eval_car)
have 2:"(x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a = (x a) ⊕ (y a) ⊕ (z a)"
using 1 assms
by (simp add: add.m_assoc function_ring_car_closed)
show ?thesis
using 0 2 by auto
qed
lemma(in ring_functions) fun_add_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
shows "x ⊕⇘F⇙ y ⊕⇘F⇙ z = x ⊕⇘F⇙ (y ⊕⇘F⇙ z)"
apply(rule function_ring_car_eqI)
using assms apply (simp add: fun_add_closed)
apply (simp add: assms(1) assms(2) assms(3) fun_add_closed)
by (simp add: assms(1) assms(2) assms(3) fun_add_eval_assoc)
lemma(in ring_functions) fun_add_eval_comm:
assumes "a ∈ S"
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
shows "(x ⊕⇘F⇙ y) a = (y ⊕⇘F⇙ x) a"
by (metis F_def assms(1) assms(2) assms(3) fun_add_eval_car ring.ring_simprules(10) ring_functions.function_ring_car_closed ring_functions_axioms ring_functions_def)
lemma(in ring_functions) fun_add_comm:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
shows "x ⊕⇘F⇙ y = y ⊕⇘F⇙ x"
using fun_add_eval_comm assms
by (metis (no_types, hide_lams) fun_add_closed function_ring_car_eqI)
subsubsection‹Basic Facts About the Multiplicative Unit›
lemma(in ring_functions) function_one_eval:
assumes "a ∈ S"
shows "𝟭⇘F⇙ a = 𝟭"
using assms function_ring_defs unfolding function_one_def
by simp
lemma(in ring_functions) function_one_closed:
"𝟭⇘F⇙ ∈carrier F"
apply(rule function_ring_car_memI)
using function_ring_defs
using function_one_eval apply auto[1]
by (simp add: function_one_def function_ring_defs(4))
lemma(in ring_functions) function_times_one_l:
assumes "a ∈ carrier F"
shows "𝟭⇘F⇙ ⊗⇘F⇙ a = a"
proof(rule function_ring_car_eqI)
show "𝟭⇘F⇙ ⊗⇘F⇙ a ∈ carrier F"
using assms fun_mult_closed function_one_closed
by blast
show " a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (𝟭⇘F⇙ ⊗⇘F⇙ a) c = a c "
by (simp add: assms function_mult_eval_car function_one_eval function_one_closed function_ring_car_closed)
qed
lemma(in ring_functions) function_times_one_r:
assumes "a ∈ carrier F"
shows "a⊗⇘F⇙ 𝟭⇘F⇙ = a"
proof(rule function_ring_car_eqI)
show "a⊗⇘F⇙ 𝟭⇘F⇙ ∈ carrier F"
using assms fun_mult_closed function_one_closed
by blast
show " a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (a⊗⇘F⇙ 𝟭⇘F⇙) c = a c "
using assms
by (simp add: function_mult_eval_car function_one_eval function_one_closed function_ring_car_closed)
qed
subsubsection‹Basic Facts About the Additive Unit›
lemma(in ring_functions) function_zero_eval:
assumes "a ∈ S"
shows "𝟬⇘F⇙ a = 𝟬"
using assms function_ring_defs
unfolding function_zero_def
by simp
lemma(in ring_functions) function_zero_closed:
"𝟬⇘F⇙ ∈carrier F"
apply(rule function_ring_car_memI)
apply (simp add: function_zero_eval)
by (simp add: function_ring_defs(5) function_zero_def)
lemma(in ring_functions) fun_add_zeroL:
assumes "a ∈ carrier F"
shows "𝟬⇘F⇙ ⊕⇘F⇙ a = a"
proof(rule function_ring_car_eqI)
show "𝟬⇘F⇙ ⊕⇘F⇙ a ∈ carrier F"
using assms fun_add_closed function_zero_closed
by blast
show "a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (𝟬⇘F⇙ ⊕⇘F⇙ a) c = a c "
using assms F_def fun_add_eval_car function_zero_closed
ring_functions.function_zero_eval ring_functions_axioms
by (simp add: ring_functions.function_zero_eval function_ring_car_closed)
qed
lemma(in ring_functions) fun_add_zeroR:
assumes "a ∈ carrier F"
shows "a ⊕⇘F⇙ 𝟬⇘F⇙ = a"
using assms fun_add_comm fun_add_zeroL
by (simp add: function_zero_closed)
subsubsection‹Distributive Laws›
lemma(in ring_functions) function_mult_r_distr:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
assumes " z ∈ carrier F"
shows " (x ⊕⇘F⇙ y) ⊗⇘F⇙ z = x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z"
proof(rule function_ring_car_eqI)
show "(x ⊕⇘F⇙ y) ⊗⇘F⇙ z ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "⋀a. a ∈ S ⟹ ((x ⊕⇘F⇙ y) ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z) a"
proof-
fix a
assume A: "a ∈ S"
show "((x ⊕⇘F⇙ y) ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z) a"
using A assms fun_add_eval_car[of a x y] fun_add_eval_car[of a "x ⊗⇘F⇙z" "y ⊗⇘F⇙ z"]
function_mult_eval_car[of a "x ⊕⇘F⇙ y" z] semiring_simprules(10)
F_def
by (smt fun_add_closed function_mult_eval_car function_ring_car_closed
ring_functions.fun_mult_closed ring_functions_axioms)
qed
qed
lemma(in ring_functions) function_mult_l_distr:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
assumes " z ∈ carrier F"
shows "z ⊗⇘F⇙ (x ⊕⇘F⇙ y) = z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y"
proof(rule function_ring_car_eqI)
show "z ⊗⇘F⇙ (x ⊕⇘F⇙ y) ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "⋀a. a ∈ S ⟹ (z ⊗⇘F⇙ (x ⊕⇘F⇙ y)) a = (z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y) a"
proof-
fix a
assume A: "a ∈ S"
show "(z ⊗⇘F⇙ (x ⊕⇘F⇙ y)) a = (z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y) a"
using A assms function_ring_defs fun_add_closed fun_mult_closed
function_mult_eval_car[of a z "x ⊕⇘F⇙ y"]
function_mult_eval_car[of a z x]
function_mult_eval_car[of a z y]
fun_add_eval_car[of a x y]
semiring_simprules(13)
fun_add_eval_car function_ring_car_closed by auto
qed
qed
subsubsection‹Additive Inverses›
lemma(in ring_functions) function_uminus_closed:
assumes "f ∈ carrier F"
shows "function_uminus S R f ∈ carrier F"
proof(rule function_ring_car_memI)
show "⋀a. a ∈ S ⟹ function_uminus S R f a ∈ carrier R"
using assms function_ring_car_closed[of _ f] unfolding function_uminus_def
by simp
show "⋀a. a ∉ S ⟹ function_uminus S R f a = undefined"
by (simp add: function_uminus_def)
qed
lemma(in ring_functions) function_uminus_eval:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "(function_uminus S R f) a = ⊖ (f a)"
using assms unfolding function_uminus_def
by simp
lemma(in ring_functions) function_uminus_add_r:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "f ⊕⇘F⇙ function_uminus S R f = 𝟬⇘F⇙"
apply(rule function_ring_car_eqI)
using assms fun_add_closed function_uminus_closed apply blast
unfolding F_def using F_def function_zero_closed apply blast
using F_def assms(2) fun_add_eval_car function_ring_car_closed function_uminus_closed
function_uminus_eval function_zero_eval r_neg by auto
lemma(in ring_functions) function_uminus_add_l:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "function_uminus S R f ⊕⇘F⇙ f = 𝟬⇘F⇙"
using assms(1) assms(2) fun_add_comm function_uminus_add_r function_uminus_closed by auto
subsubsection‹Scalar Multiplication›
lemma(in ring_functions) function_smult_eval:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
assumes "b ∈ S"
shows "(a ⊙⇘F⇙ f) b = a ⊗ (f b)"
using function_ring_defs(6) unfolding function_scalar_mult_def
by(simp add: assms)
lemma(in ring_functions) function_smult_closed:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
shows "a ⊙⇘F⇙ f ∈ carrier F"
apply(rule function_ring_car_memI)
using function_smult_eval assms
apply (simp add: function_ring_car_closed)
using function_scalar_mult_def F_def
by (metis function_ring_defs(6) restrict_apply)
lemma(in ring_functions) function_smult_assoc1:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
assumes "f ∈ carrier F"
shows "b ⊙⇘F⇙ (a ⊙⇘F⇙ f) = (b ⊗ a)⊙⇘F⇙f"
apply(rule function_ring_car_eqI)
using assms function_smult_closed apply simp
using assms function_smult_closed apply simp
by (metis F_def assms(1) assms(2) assms(3) function_mult_eval_closed function_one_closed
function_smult_eval function_times_one_r m_assoc m_closed ring_functions.function_smult_closed ring_functions_axioms)
lemma(in ring_functions) function_smult_assoc2:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(a ⊙⇘F⇙ f)⊗⇘F⇙g = a ⊙⇘F⇙ (f ⊗⇘F⇙ g)"
apply(rule function_ring_car_eqI)
using assms function_smult_closed apply (simp add: fun_mult_closed)
apply (simp add: assms(1) assms(2) assms(3) fun_mult_closed function_smult_closed)
by (metis (full_types) F_def assms(1) assms(2) assms(3) fun_mult_closed
function_mult_eval_car function_smult_closed function_smult_eval m_assoc ring_functions.function_ring_car_closed ring_functions_axioms)
lemma(in ring_functions) function_smult_one:
assumes "f ∈ carrier F"
shows "𝟭⊙⇘F⇙f = f"
apply(rule function_ring_car_eqI)
apply (simp add: assms function_smult_closed)
apply (simp add: assms)
by (simp add: assms function_ring_car_closed function_smult_eval)
lemma(in ring_functions) function_smult_l_distr:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier F |] ==>
(a ⊕ b) ⊙⇘F⇙ x = a ⊙⇘F⇙ x ⊕⇘F⇙ b ⊙⇘F⇙ x"
apply(rule function_ring_car_eqI)
apply (simp add: function_smult_closed)
apply (simp add: fun_add_closed function_smult_closed)
using function_smult_eval
by (simp add: fun_add_eval_car function_ring_car_closed function_smult_closed l_distr)
lemma(in ring_functions) function_smult_r_distr:
"[| a ∈ carrier R; x ∈ carrier F; y ∈ carrier F |] ==>
a ⊙⇘F⇙ (x ⊕⇘F⇙ y) = a ⊙⇘F⇙ x ⊕⇘F⇙ a ⊙⇘F⇙ y"
apply(rule function_ring_car_eqI)
apply (simp add: fun_add_closed function_smult_closed)
apply (simp add: fun_add_closed function_smult_closed)
by (simp add: fun_add_closed fun_add_eval_car function_ring_car_closed function_smult_closed function_smult_eval r_distr)
subsubsection‹The Ring of Functions Forms an Algebra›
lemma(in ring_functions) function_ring_is_abelian_group:
"abelian_group F"
apply(rule abelian_groupI)
apply (simp add: fun_add_closed)
apply (simp add: function_zero_closed)
using fun_add_assoc apply simp
apply (simp add: fun_add_comm)
apply (simp add: fun_add_comm fun_add_zeroR function_zero_closed)
using fun_add_zeroL function_ring_car_eqI function_uminus_add_l
function_uminus_closed function_zero_closed by blast
lemma(in ring_functions) function_ring_is_monoid:
"monoid F"
apply(rule monoidI)
apply (simp add: fun_mult_closed)
apply (simp add: function_one_closed)
apply (simp add: fun_mult_assoc)
apply (simp add: function_times_one_l)
by (simp add: function_times_one_r)
lemma(in ring_functions) function_ring_is_ring:
"ring F"
apply(rule ringI)
apply (simp add: function_ring_is_abelian_group)
apply (simp add: function_ring_is_monoid)
apply (simp add: function_mult_r_distr)
by (simp add: function_mult_l_distr)
sublocale ring_functions < F?: ring F
by (rule function_ring_is_ring)
lemma(in cring_functions) function_mult_comm:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
shows "x ⊗⇘F⇙ y = y ⊗⇘F⇙ x"
apply(rule function_ring_car_eqI)
apply (simp add: assms(1) assms(2) fun_mult_closed)
apply (simp add: assms(1) assms(2) fun_mult_closed)
by (simp add: assms(1) assms(2) function_mult_eval_car function_ring_car_closed m_comm)
lemma(in cring_functions) function_ring_is_comm_monoid:
"comm_monoid F"
apply(rule comm_monoidI)
using fun_mult_assoc function_one_closed
apply (simp add: fun_mult_closed)
apply (simp add: function_one_closed)
apply (simp add: fun_mult_assoc)
apply (simp add: function_times_one_l)
by (simp add: function_mult_comm)
lemma(in cring_functions) function_ring_is_cring:
"cring F"
apply(rule cringI)
apply (simp add: function_ring_is_abelian_group)
apply (simp add: function_ring_is_comm_monoid)
by (simp add: function_mult_r_distr)
lemma(in cring_functions) function_ring_is_algebra:
"algebra R F"
apply(rule algebraI)
apply (simp add: is_cring)
apply (simp add: function_ring_is_cring)
using function_smult_closed apply blast
apply (simp add: function_smult_l_distr)
apply (simp add: function_smult_r_distr)
apply (simp add: function_smult_assoc1)
apply (simp add: function_smult_one)
by (simp add: function_smult_assoc2)
lemma(in ring_functions) function_uminus:
assumes "f ∈ carrier F"
shows "⊖⇘F⇙ f = (function_uminus S R) f"
using assms a_inv_def[of F]
by (metis F_def abelian_group.a_group abelian_group.r_neg function_uminus_add_r function_uminus_closed group.inv_closed partial_object.select_convs(1) ring.ring_simprules(18) ring_functions.function_ring_car_eqI ring_functions.function_ring_is_abelian_group ring_functions.function_ring_is_ring ring_functions_axioms)
lemma(in ring_functions) function_uminus_eval':
assumes "f ∈ carrier F"
assumes "a ∈ S"
shows "(⊖⇘F⇙ f) a = (function_uminus S R) f a"
using assms
by (simp add: function_uminus)
lemma(in ring_functions) function_uminus_eval'':
assumes "f ∈ carrier F"
assumes "a ∈ S"
shows "(⊖⇘F⇙ f) a = ⊖ (f a)"
using assms(1) assms(2) function_uminus
by (simp add: function_uminus_eval)
sublocale cring_functions < F?: algebra R F
using function_ring_is_algebra by auto
subsection‹Constant Functions›
definition constant_function where
"constant_function S a =(λx ∈ S. a)"
abbreviation(in ring_functions)(input) const where
"const ≡ constant_function S"
lemma(in ring_functions) constant_function_closed:
assumes "a ∈ carrier R"
shows "const a ∈ carrier F"
apply(rule function_ring_car_memI)
unfolding constant_function_def
apply (simp add: assms)
by simp
lemma(in ring_functions) constant_functionE:
assumes "a ∈ carrier R"
assumes "b ∈ S"
shows "const a b = a"
by (simp add: assms(2) constant_function_def)
lemma(in ring_functions) constant_function_add:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "const (a ⊕⇘R⇙ b) = (const a) ⊕⇘F⇙ (const b) "
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms(1) assms(2))
using assms(1) constant_function_closed assms(2) fun_add_closed apply auto[1]
by (simp add: assms(1) assms(2) constant_function_closed constant_functionE fun_add_eval_car)
lemma(in ring_functions) constant_function_mult:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "const (a ⊗⇘R⇙ b) = (const a) ⊗⇘F⇙ (const b)"
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms(1) assms(2))
using assms(1) constant_function_closed assms(2) fun_mult_closed apply auto[1]
by (simp add: constant_function_closed assms(1) assms(2) constant_functionE function_mult_eval_car)
lemma(in ring_functions) constant_function_minus:
assumes "a ∈ carrier R"
shows "⊖⇘F⇙(const a) = (const (⊖⇘R⇙ a)) "
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms local.function_uminus)
apply (simp add: constant_function_closed assms function_uminus_closed)
apply (simp add: constant_function_closed assms)
by (simp add: constant_function_closed assms constant_functionE function_uminus_eval'')
lemma(in ring_functions) function_one_is_constant:
"const 𝟭 = 𝟭⇘F⇙"
unfolding F_def
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed)
using F_def function_one_closed apply auto[1]
using F_def constant_functionE function_one_eval by auto
lemma(in ring_functions) function_zero_is_constant:
"const 𝟬 = 𝟬⇘F⇙"
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed)
using F_def function_zero_closed apply auto[1]
using F_def constant_functionE function_zero_eval by auto
subsection‹Special Examples of Functions Rings›
subsubsection‹Functions from the Carrier of a Ring to Itself›
locale U_function_ring = ring
locale U_function_cring = U_function_ring + cring
sublocale U_function_ring < S?: struct_functions R "carrier R"
done
sublocale U_function_ring < FunR?: ring_functions R "carrier R" "Fun R"
apply (simp add: local.ring_axioms ring_functions.intro)
by simp
sublocale U_function_cring < FunR?: cring_functions R "carrier R" "Fun R"
apply (simp add: cring_functions_def is_cring ring_functions_axioms)
by simp
abbreviation(in U_function_ring)(input) ring_compose :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_compose ≡ compose (carrier R)"
lemma(in U_function_ring) ring_function_ring_comp:
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "ring_compose f g ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
apply (simp add: assms(1) assms(2) compose_eq)
apply (simp add: assms(1) assms(2) function_ring_car_closed)
by (meson compose_extensional extensional_arb)
abbreviation(in U_function_ring)(input) ring_const ("𝔠ı") where
"ring_const ≡ constant_function (carrier R)"
lemma(in ring_functions) function_nat_pow_eval:
assumes "f ∈ carrier F"
assumes "s ∈ S"
shows "(f[^]⇘F⇙(n::nat)) s = (f s)[^]n"
apply(induction n)
using assms(2) function_one_eval apply auto[1]
by (simp add: assms(1) assms(2) function_mult_eval_car function_ring_is_monoid monoid.nat_pow_closed)
context U_function_ring
begin
definition a_translate :: "'a ⇒ 'a ⇒ 'a" where
"a_translate = (λ r ∈ carrier R. restrict ((add R) r) (carrier R))"
definition m_translate :: "'a ⇒ 'a ⇒ 'a" where
"m_translate = (λ r ∈ carrier R. restrict ((mult R) r) (carrier R))"
definition nat_power :: "nat ⇒ 'a ⇒ 'a" where
"nat_power = (λ(n::nat). restrict (λa. a[^]⇘R⇙n) (carrier R)) "
text‹Restricted operations are in Fs›
lemma a_translate_functions:
assumes "c ∈ carrier R"
shows "a_translate c ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using assms a_translate_def
apply simp
using assms a_translate_def
by simp
lemma m_translate_functions:
assumes "c ∈ carrier R"
shows "m_translate c ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using assms m_translate_def
apply simp
using assms m_translate_def
by simp
lemma nat_power_functions:
shows "nat_power n ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using nat_power_def
apply simp
by (simp add: nat_power_def)
text‹Restricted operations simps›
lemma a_translate_eq:
assumes "c ∈ carrier R"
assumes "a ∈ carrier R"
shows "a_translate c a = c ⊕ a"
by (simp add: a_translate_def assms(1) assms(2))
lemma a_translate_eq':
assumes "c ∈ carrier R"
assumes "a ∉ carrier R"
shows "a_translate c a = undefined"
by (meson a_translate_functions assms(1) assms(2) function_ring_not_car)
lemma a_translate_eq'':
assumes "c ∉ carrier R"
shows "a_translate c = undefined"
by (simp add: a_translate_def assms)
lemma m_translate_eq:
assumes "c ∈ carrier R"
assumes "a ∈ carrier R"
shows "m_translate c a = c ⊗ a"
by (simp add: m_translate_def assms(1) assms(2))
lemma m_translate_eq':
assumes "c ∈ carrier R"
assumes "a ∉ carrier R"
shows "m_translate c a = undefined "
by (meson m_translate_functions assms(1) assms(2) function_ring_not_car)
lemma m_translate_eq'':
assumes "c ∉ carrier R"
shows "m_translate c = undefined"
by (simp add: m_translate_def assms)
lemma nat_power_eq:
assumes "a ∈ carrier R"
shows "nat_power n a = a[^]⇘R⇙ n"
by (simp add: assms nat_power_def)
lemma nat_power_eq':
assumes "a ∉ carrier R"
shows "nat_power n a = undefined"
by (simp add: assms nat_power_def)
text‹Constant ring\_function properties›
lemma constant_function_eq:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "𝔠⇘a⇙ b = a"
using assms
by (simp add: constant_functionE)
lemma constant_function_eq':
assumes "a ∈ carrier R"
assumes "b ∉ carrier R"
shows "𝔠⇘a⇙ b = undefined"
by (simp add: constant_function_closed assms(1) assms(2) function_ring_not_car)
text‹Compound expressions from algebraic operations›
end
definition monomial_function where
"monomial_function R c (n::nat) = (λ x ∈ carrier R. c ⊗⇘R⇙ (x[^]⇘R⇙n))"
context U_function_ring
begin
abbreviation monomial where
"monomial ≡ monomial_function R"
lemma monomial_functions:
assumes "c ∈ carrier R"
shows "monomial c n ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
unfolding monomial_function_def
apply (simp add: assms)
by simp
definition ring_id where
"ring_id ≡ restrict (λx. x) (carrier R) "
lemma ring_id_closed[simp]:
"ring_id ∈ carrier (Fun R)"
by (simp add: function_ring_car_memI ring_id_def)
lemma ring_id_eval:
assumes "a ∈ carrier R"
shows "ring_id a = a"
using assms unfolding ring_id_def
by simp
lemma constant_a_trans:
assumes "a ∈carrier R"
shows "m_translate a = 𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id"
proof(rule function_ring_car_eqI)
show "m_translate a ∈ carrier (Fun R)"
using assms
using m_translate_functions by blast
show "𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id ∈ carrier (Fun R)"
unfolding ring_id_def
using assms ring_id_closed ring_id_def
by (simp add: constant_function_closed fun_mult_closed)
show "⋀x. x ∈ carrier R ⟹ m_translate a x = (𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id) x"
by (simp add: constant_function_closed assms constant_function_eq function_mult_eval_car m_translate_eq ring_id_eval)
qed
text‹polynomials in one variable›
fun polynomial :: "'a list ⇒ ('a ⇒ 'a)" where
"polynomial [] = 𝟬⇘Fun R⇙ "|
"polynomial (a#as) = (λx ∈ carrier R. a ⊕ x ⊗ (polynomial as x))"
lemma polynomial_induct_lemma:
assumes "f ∈ carrier (Fun R)"
assumes "a ∈ carrier R"
shows "(λx ∈ carrier R. a ⊕ x ⊗ (f x)) ∈ carrier (Fun R)"
proof(rule function_ring_car_memI)
show "⋀aa. aa ∈ carrier R ⟹ (λx∈carrier R. a ⊕ x ⊗ f x) aa ∈ carrier R"
proof- fix y assume A: "y ∈ carrier R"
have "a ⊕ y ⊗ f y ∈ carrier R"
using A assms(1) assms(2) function_ring_car_closed by blast
thus "(λx∈carrier R. a ⊕ x ⊗ f x) y ∈ carrier R"
using A by auto
qed
show "⋀aa. aa ∉ carrier R ⟹ (λx∈carrier R. a ⊕ x ⊗ f x) aa = undefined"
by auto
qed
lemma polynomial_function:
shows "set as ⊆ carrier R ⟹ polynomial as ∈ carrier (Fun R)"
proof(induction as)
case Nil
then show ?case
by (simp add: function_zero_closed)
next
case (Cons a as)
then show "polynomial (a # as) ∈ carrier (function_ring (carrier R) R)"
using polynomial.simps(2)[of a as] polynomial_induct_lemma[of "polynomial as" a]
by simp
qed
lemma polynomial_constant:
assumes "a ∈ carrier R"
shows "polynomial [a] = 𝔠⇘a⇙"
apply(rule function_ring_car_eqI)
using assms polynomial_function
apply (metis (full_types) list.distinct(1) list.set_cases set_ConsD subset_code(1))
apply (simp add: constant_function_closed assms)
using polynomial.simps(2)[of a "[]"] polynomial.simps(1) assms
by (simp add: constant_function_eq function_zero_eval)
end
subsubsection‹Sequences Indexed by the Natural Numbers›
definition nat_seqs ("_⇗ω⇖")where
"nat_seqs R ≡ function_ring (UNIV::nat set) R"
abbreviation(input) closed_seqs where
"closed_seqs R ≡ carrier (R⇗ω⇖)"
lemma closed_seqs_memI:
assumes "⋀k. s k ∈ carrier R"
shows "s ∈ closed_seqs R"
unfolding nat_seqs_def function_ring_def
by (simp add: PiE_UNIV_domain assms)
lemma closed_seqs_memE:
assumes "s ∈ closed_seqs R"
shows "s k ∈ carrier R"
using assms unfolding nat_seqs_def function_ring_def
by (simp add: PiE_iff)
definition is_constant_fun where
"is_constant_fun R f = (∃x ∈ carrier R. f = constant_function (carrier R) R x)"
definition is_constant_seq where
"is_constant_seq R s = (∃x ∈ carrier R. s = constant_function (UNIV::nat set) x)"
lemma is_constant_seqI:
fixes a
assumes "s ∈ closed_seqs R"
assumes "⋀k. s k = a"
shows "is_constant_seq R s"
unfolding is_constant_seq_def constant_function_def
by (metis assms(1) assms(2) closed_seqs_memE restrict_UNIV restrict_ext)
lemma is_constant_seqE:
assumes "is_constant_seq R s"
assumes "s k = a"
shows "s n = a"
using assms unfolding is_constant_seq_def
by (metis constant_function_def restrict_UNIV)
lemma is_constant_seq_imp_closed:
assumes "is_constant_seq R s"
shows "s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
using assms unfolding is_constant_seq_def constant_function_def
by auto
context U_function_ring
begin
text‹Sequence sums and products are closed›
lemma seq_plus_closed:
assumes "s ∈ closed_seqs R"
assumes "s' ∈ closed_seqs R"
shows "s ⊕⇘R⇗ω⇖⇙ s' ∈ closed_seqs R"
by (metis assms(1) assms(2) nat_seqs_def ring_functions.fun_add_closed ring_functions_axioms)
lemma seq_mult_closed:
assumes "s ∈ closed_seqs R"
assumes "s' ∈ closed_seqs R"
shows "s ⊗⇘R⇗ω⇖⇙ s' ∈ closed_seqs R"
apply(rule closed_seqs_memI)
by (metis assms(1) assms(2) closed_seqs_memE nat_seqs_def ring_functions.fun_mult_closed ring_functions_axioms)
lemma constant_function_comp_is_closed_seq:
assumes "a ∈ carrier R"
assumes "s ∈ closed_seqs R"
shows "(const a ∘ s) ∈ closed_seqs R"
by (simp add: constant_functionE assms(1) assms(2) closed_seqs_memE closed_seqs_memI)
lemma constant_function_comp_is_constant_seq:
assumes "a ∈ carrier R"
assumes "s ∈ closed_seqs R"
shows "is_constant_seq R ((const a) ∘ s)"
apply(rule is_constant_seqI[of _ _ a] )
apply (simp add: assms(1) assms(2) constant_function_comp_is_closed_seq)
using assms(1) assms(2) closed_seqs_memE
by (simp add: closed_seqs_memE constant_functionE)
lemma function_comp_is_closed_seq:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
shows "f ∘ s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
using assms(1) assms(2) closed_seqs_memE
by (metis comp_apply fun_add_eval_closed fun_add_zeroR function_zero_closed)
lemma function_sum_comp_is_seq_sum:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "(f ⊕⇘Fun R⇙ g) ∘ s = (f ∘ s) ⊕⇘R⇗ω⇖⇙ (g ∘ s)"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
apply (simp add: ring_functions_axioms)
using function_comp_is_closed_seq
apply (metis assms(1) assms(2) assms(3) fun_add_closed nat_seqs_def)
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_plus_closed)
by (smt UNIV_eq_I assms(1) assms(2) assms(3) closed_seqs_memE comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.fun_add_eval_car ring_functions_axioms)
lemma function_mult_comp_is_seq_mult:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "(f ⊗⇘Fun R⇙ g) ∘ s = (f ∘ s) ⊗⇘R⇗ω⇖⇙ (g ∘ s)"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
apply (simp add: ring_functions_axioms)
using function_comp_is_closed_seq
apply (metis assms(1) assms(2) assms(3) fun_mult_closed nat_seqs_def)
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_mult_closed)
by (metis (no_types, lifting) assms(1) assms(2) assms(3) comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.function_mult_eval_car ring_functions.function_ring_car_closed ring_functions_axioms)
lemma seq_plus_simp:
assumes "s ∈ closed_seqs R"
assumes "t ∈ closed_seqs R"
shows "(s ⊕⇘R⇗ω⇖⇙ t) k = s k ⊕ t k"
using assms unfolding nat_seqs_def
by (simp add: ring_functions.fun_add_eval_car ring_functions_axioms)
lemma seq_mult_simp:
assumes "s ∈ closed_seqs R"
assumes "t ∈ closed_seqs R"
shows "(s ⊗⇘R⇗ω⇖⇙ t) k = s k ⊗ t k"
using assms unfolding nat_seqs_def
by (simp add: ring_functions.function_mult_eval_car ring_functions_axioms)
lemma seq_one_simp:
"𝟭⇘R⇗ω⇖⇙ k = 𝟭"
by (simp add: nat_seqs_def ring_functions.function_one_eval ring_functions_axioms)
lemma seq_zero_simp:
"𝟬⇘R⇗ω⇖⇙ k = 𝟬"
by (simp add: nat_seqs_def ring_functions.function_zero_eval ring_functions_axioms)
lemma(in U_function_ring) ring_id_seq_comp:
assumes "s ∈ closed_seqs R"
shows "ring_id ∘ s = s"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV::nat set"])
using ring_functions_axioms apply auto[1]
apply (metis assms function_comp_is_closed_seq nat_seqs_def ring_id_closed)
apply (metis assms nat_seqs_def)
by (simp add: assms closed_seqs_memE ring_id_eval)
lemma(in U_function_ring) ring_seq_smult_closed:
assumes "s ∈ closed_seqs R"
assumes "a ∈ carrier R"
shows "a ⊙⇘R⇗ω⇖⇙ s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
by (metis assms(1) assms(2) closed_seqs_memE nat_seqs_def ring_functions.function_smult_closed ring_functions_axioms)
lemma(in U_function_ring) ring_seq_smult_eval:
assumes "s ∈ closed_seqs R"
assumes "a ∈ carrier R"
shows "(a ⊙⇘R⇗ω⇖⇙ s) k = a ⊗ (s k)"
by (metis UNIV_I assms(1) assms(2) nat_seqs_def ring_functions.function_smult_eval ring_functions_axioms)
lemma(in U_function_ring) ring_seq_smult_comp_assoc:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "a ∈ carrier R"
shows "((a ⊙⇘Fun R⇙ f) ∘ s) = a ⊙⇘R⇗ω⇖⇙ (f ∘ s)"
apply(rule ext)
using function_smult_eval[of a f] ring_seq_smult_eval[of "f ∘ s" a]
by (simp add: assms(1) assms(2) assms(3) closed_seqs_memE function_comp_is_closed_seq)
end
section‹Extensional Maps Between the Carriers of two Structures›
definition struct_maps :: "('a, 'c) partial_object_scheme ⇒ ('b, 'd) partial_object_scheme
⇒ ('a ⇒ 'b) set" where
"struct_maps T S = {f. (f ∈ (carrier T) → (carrier S)) ∧ f = restrict f (carrier T) }"
definition to_struct_map where
"to_struct_map T f = restrict f (carrier T)"
lemma to_struct_map_closed:
assumes "f ∈ (carrier T) → (carrier S)"
shows "to_struct_map T f ∈ (struct_maps T S)"
by (smt PiE_restrict Pi_iff assms mem_Collect_eq restrict_PiE struct_maps_def to_struct_map_def)
lemma struct_maps_memI:
assumes "⋀ x. x ∈ carrier T ⟹ f x ∈ carrier S"
assumes "⋀x. x ∉ carrier T ⟹ f x = undefined"
shows "f ∈ struct_maps T S"
proof-
have 0: " (f ∈ (carrier T) → (carrier S))"
using assms
by blast
have 1: "f = restrict f (carrier T)"
using assms
by (simp add: extensional_def extensional_restrict)
show ?thesis
using 0 1
unfolding struct_maps_def
by blast
qed
lemma struct_maps_memE:
assumes "f ∈ struct_maps T S"
shows "⋀ x. x ∈ carrier T ⟹ f x ∈ carrier S"
"⋀x. x ∉ carrier T ⟹ f x = undefined"
using assms unfolding struct_maps_def
apply blast
using assms unfolding struct_maps_def
by (metis (mono_tags, lifting) mem_Collect_eq restrict_apply)
text‹An abbreviation for restricted composition of function of functions. This is necessary for the composition of two struct maps to again be a struct map.›
abbreviation(input) rcomp
where "rcomp ≡ FuncSet.compose"
lemma struct_map_comp:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
shows "rcomp (carrier T) f g ∈ (struct_maps T U)"
proof(rule struct_maps_memI)
show "⋀x. x ∈ carrier T ⟹ rcomp (carrier T) f g x ∈ carrier U"
using assms struct_maps_memE(1)
by (metis compose_eq)
show " ⋀x. x ∉ carrier T ⟹ rcomp (carrier T) f g x = undefined"
by (meson compose_extensional extensional_arb)
qed
lemma r_comp_is_compose:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
assumes "a ∈ (carrier T)"
shows "(rcomp (carrier T) f g) a = (f ∘ g) a"
by (simp add: FuncSet.compose_def assms(3))
lemma r_comp_not_in_car:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
assumes "a ∉ (carrier T)"
shows "(rcomp (carrier T) f g) a = undefined"
by (simp add: FuncSet.compose_def assms(3))
text‹The reverse composition of two struct maps:›
definition pullback ::
"('a, 'd) partial_object_scheme ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'c)" where
"pullback T f g = rcomp (carrier T) g f"
lemma pullback_closed:
assumes "f ∈ (struct_maps T S)"
assumes "g ∈ (struct_maps S U)"
shows "pullback T f g ∈ (struct_maps T U)"
by (metis assms(1) assms(2) pullback_def struct_map_comp)
text‹Composition of struct maps which takes the structure itself rather than the carrier as a parameter:›
definition pushforward ::
"('a, 'd) partial_object_scheme ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c)" where
"pushforward T f g ≡ rcomp (carrier T) f g"
lemma pushforward_closed:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
shows "pushforward T f g ∈ (struct_maps T U)"
using assms(1) assms(2) struct_map_comp
by (metis pushforward_def)
end
Theory Cring_Poly
theory Cring_Poly
imports "HOL-Algebra.UnivPoly" "HOL-Algebra.Subrings" Function_Ring
begin
text‹
This theory extends the material in \<^theory>‹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 is_ring 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) ⊕⇘S⇙ (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 ⊕⇘S⇙ 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) = ⊖⇘S⇙ h b"
proof-
have "h b ⊕⇘S⇙ h (⊖ b) = 𝟬⇘S⇙"
by (metis (no_types, hide_lams) 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 ⊖⇘S⇙ h b"
using assms ring_hom_add[of h R S a "⊖⇘R⇙ 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[^]⇘R⇙(n::nat)) = (h a)[^]⇘S⇙(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 = 𝟬"
shows "b = 𝟬"
proof-
have "inv a ⊗ a ⊗ b = 𝟬 "
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 = 𝟬"
shows "b = 𝟬"
proof-
have "b ⊗ (a ⊗ inv a) = 𝟬 "
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 ⊗⇘R⇙ y) = f x ⊗⇘T⇙ f y"
proof-
fix x y
assume A: "x ∈ carrier R" "y ∈ carrier R"
show "f (x ⊗⇘R⇙ y) = f x ⊗⇘T⇙ f y"
proof-
have "f (x ⊗⇘R⇙ y) = g (h (x ⊗⇘R⇙ y))"
by (simp add: A(1) A(2) assms(1) assms(6) ring.ring_simprules(5))
then have "f (x ⊗⇘R⇙ y) = g ((h x) ⊗⇘S⇙ (h y))"
using A(1) A(2) assms(4) ring_hom_mult by fastforce
then have "f (x ⊗⇘R⇙ y) = g (h x) ⊗⇘T⇙ 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 ⊕⇘R⇙ y) = f x ⊕⇘T⇙ f y"
proof-
fix x y
assume A: "x ∈ carrier R" "y ∈ carrier R"
show "f (x ⊕⇘R⇙ y) = f x ⊕⇘T⇙ f y"
proof-
have "f (x ⊕⇘R⇙ y) = g (h (x ⊕⇘R⇙ y))"
by (simp add: A(1) A(2) assms(1) assms(6) ring.ring_simprules(1))
then have "f (x ⊕⇘R⇙ y) = g ((h x) ⊕⇘S⇙ (h y))"
using A(1) A(2) assms(4) ring_hom_add by fastforce
then have "f (x ⊕⇘R⇙ y) = g (h x) ⊕⇘T⇙ g (h y)"
by (metis (no_types, hide_lams) 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 𝟭⇘R⇙ = 𝟭⇘T⇙"
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 = 𝟬"
assumes "⋀n. p n ∈ carrier R"
shows "p ∈ carrier P"
proof-
have "bound 𝟬 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 = 𝟬"
shows "g ∈ carrier (UP R)"
proof-
have "bound 𝟬 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 = 𝟬"
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 R.ring_axioms UP_ring.deg_aboveD UP_ring.intro partial_object.select_convs(1) restrict_apply up_ring.simps(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
a 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 𝟬)"
using coeff_simp P_def coeff_monom monom_closed by auto
lemma cfs_zero [simp]: "𝟬⇘P⇙ n = 𝟬"
using P_def UP_zero_closed coeff_simp coeff_zero by auto
lemma cfs_one [simp]: "𝟭⇘P⇙ n = (if n=0 then 𝟭 else 𝟬)"
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⇙ 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 ⊕⇘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⇙ 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 ⊖⇘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⇙ 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 ⊗⇘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 ⊗⇘P⇙ (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) ⊗⇘P⇙ 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 ⊕⇘P⇙ 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 ⊕⇘P⇙ 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 ⊕⇘P⇙ g) = n"
proof-
have 0: "degree (f ⊕⇘P⇙ g) ≤n"
using assms bound_deg_sum
P_def UP_ring_axioms by auto
show "degree (f ⊕⇘P⇙ g) = n"
proof(rule ccontr)
assume "degree (f ⊕⇘P⇙ g) ≠ n "
then have 1: "degree (f ⊕⇘P⇙ g) < n"
using 0 by auto
have 2: "degree (⊖⇘P⇙ f) < n"
using assms by simp
have 3: "g = (f ⊕⇘P⇙ g) ⊕⇘P⇙ (⊖⇘P⇙ 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 ⊕⇘P⇙ 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 ⊕⇘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 ⊖⇘P⇙ q) = degree p"
proof-
have A: "(p ⊖⇘P⇙ q) = p ⊕⇘P⇙ (⊖⇘P⇙ q)"
by (simp add: P.minus_eq)
have "degree (⊖⇘P⇙ 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 ⊕⇘UP 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 ⊖⇘UP 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 = 𝟬"
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 𝟬)"
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 𝟬)"
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 = 𝟬"
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 ⊖⇘P⇙ (ltrm f)) ≤ n"
proof(rule UP_ring.deg_aboveI)
show C0: "UP_ring R"
by (simp add: UP_ring_axioms)
show C1: "f ⊖⇘P⇙ 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 ⊖⇘P⇙ ltrm f) m = 𝟬"
proof-
fix m
assume A: "n<m"
show "coeff (UP R) (f ⊖⇘P⇙ ltrm f) m = 𝟬"
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) ⊖⇘R⇙( ltrm f) m = 𝟬"
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 ⊖⇘UP R⇙ ltrm f) m = 𝟬"
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 ⊕⇘P⇙ (ltrm f) ∧ degree g < degree f"
proof-
have 0: "f ⊖⇘P⇙ (ltrm f) ∈ carrier P"
using ltrm_closed assms(1) by blast
have 1: "f = (f ⊖⇘P⇙ (ltrm f)) ⊕⇘P⇙ (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 ⊕⇘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 ⊕⇘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 ⊕⇘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) ⊗⇘P⇙ (ltrm q)) = (ltrm p) ⊗⇘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) ⊕⇘P⇙ (ltrm f)"
"f ⊖⇘P⇙ (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 = 𝟬⇘P⇙"
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 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 ⊗⇘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 ≠𝟬"
shows "degree (q ⊗⇘P⇙ p) = degree p + degree q"
proof-
have "q ⊗⇘P⇙ p = (trunc q ⊕⇘P⇙ ltrm q) ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p)"
using assms(1) assms(2) trunc_simps(1) by auto
then have "q ⊗⇘P⇙ p = (trunc q ⊕⇘P⇙ ltrm q) ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p)"
by linarith
then have 0: "q ⊗⇘P⇙ p = (trunc q ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p)) ⊕⇘P⇙ ( ltrm q ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p))"
by (simp add: P.l_distr assms(1) assms(2) ltrm_closed trunc_closed)
have 1: "(trunc q ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p)) (degree p + degree q) = 𝟬"
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⇙ 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 ⊗⇘P⇙ (trunc p ⊕⇘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⇙ p) (degree p + degree q) =
( ltrm q ⊗⇘P⇙ (trunc p ⊕⇘P⇙ ltrm p)) (degree p + degree q)"
using 0 1 assms cfs_closed trunc_closed by auto
have 3: "(q ⊗⇘P⇙ p) (degree p + degree q) =
( ltrm q ⊗⇘P⇙ trunc p) (degree p + degree q) ⊕ ( ltrm q ⊗⇘P⇙ 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 ⊗⇘P⇙ trunc p) (degree p + degree q) = 𝟬"
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 ⊗⇘P⇙ 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 ⊗⇘P⇙ 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⇙ p) (degree p + degree q) = ( ltrm q ⊗⇘P⇙ ltrm p) (degree p + degree q)"
by (simp add: "3" "4" assms(1) assms(2) cfs_closed)
have 6: "ltrm q ⊗⇘P⇙ 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 ⊗⇘P⇙ ltrm p) (degree p + degree q) ≠𝟬"
using 5 6 assms
by (metis R.m_closed cfs_closed cfs_monom)
have 8: "degree (q ⊗⇘P⇙ 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 ≠𝟬"
assumes "degree q < n"
assumes "p = q ⊕⇘P⇙ (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) ⊕⇘P⇙ 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 ≠ 𝟬"
shows "ltrm (a ⊙⇘P⇙p) = a⊙⇘P⇙(ltrm p)"
using assms
by (smt 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⇙p) = a⊙⇘P⇙(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⇙p) = a⊙⇘P⇙(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 ≠ 𝟬"
shows "ltrm (p ⊗⇘P⇙ q) = (ltrm p) ⊗⇘P⇙ (ltrm q)"
proof(cases "degree p = 0 ∨ degree q = 0")
case True
then show ?thesis
by (smt 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 ⊗⇘P⇙ q = (p0 ⊕⇘P⇙ ltrm(p)) ⊗⇘P ⇙(q0 ⊕⇘P⇙ ltrm(q))"
using assms(1) assms(2) p0_def q0_def trunc_simps(1) by auto
then have P0: "p ⊗⇘P⇙ q = ((p0 ⊕⇘P⇙ ltrm(p)) ⊗⇘P ⇙q0) ⊕⇘P⇙ ((p0 ⊕⇘P⇙ ltrm(p))⊗⇘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 ⊕⇘P⇙ ltrm(p)) ⊗⇘P ⇙q0) < degree ((p0 ⊕⇘P⇙ ltrm(p))⊗⇘P ⇙ltrm(q))"
proof-
have LHS: "degree ((p0 ⊕⇘P⇙ ltrm(p)) ⊗⇘P ⇙q0) ≤ degree p + degree q0 "
proof(cases "q0 = 𝟬⇘P⇙")
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 ⊕⇘P⇙ ltrm(p))⊗⇘P ⇙ltrm(q)) = degree p + degree q"
using assms(1) assms(2) deg_mult_ring ltrm_closed p0_def trunc_simps(1)
by (smt 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 ⊗⇘P⇙ q) = ltrm ((p0 ⊕⇘P⇙ ltrm(p))⊗⇘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 ⊕⇘P⇙ ltrm(p))⊗⇘P ⇙ltrm(q)) = ltrm p ⊗⇘P⇙ ltrm q"
proof-
have Q0: "((p0 ⊕⇘P⇙ ltrm(p))⊗⇘P ⇙ltrm(q)) = (p0 ⊗⇘P ⇙ltrm(q)) ⊕⇘P⇙ (ltrm(p))⊗⇘P ⇙ltrm(q)"
by (simp add: P.l_distr assms(1) assms(2) ltrm_closed p0_def trunc_closed)
have Q1: "degree ((p0 ⊗⇘P ⇙ltrm(q)) ) < degree ((ltrm(p))⊗⇘P ⇙ltrm(q))"
proof(cases "p0 = 𝟬⇘P⇙")
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 ⊗⇘P ⇙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 add_le_cancel_right deg_mult_ring le_trans not_less)
have RHS: "degree ((ltrm(p))⊗⇘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 ⊕⇘P⇙ ltrm(p))⊗⇘P ⇙ltrm(q)) = ltrm ((ltrm(p))⊗⇘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 ⊗⇘P⇙ q) = (ltrm p) ⊗⇘P⇙ (ltrm q)"
using cring_ltrm_mult assms
by (smt 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 ⊗⇘P⇙ q) = (lcf p)⊙⇘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 ≠𝟬"
shows "a[^](n::nat) ≠ 𝟬"
proof(induction n)
case 0
then show ?case
by auto
next
case (Suc n)
fix n::nat
assume IH: "a[^] n ≠ 𝟬"
show "a[^] (Suc n) ≠ 𝟬"
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 ≠ 𝟬"
shows "degree (p[^]⇘P⇙ n) = n*m"
by (simp add: assms(1) assms(2) assms(3) monom_pow)
lemma (in UP_domain) monom_degree:
assumes "a ≠𝟬"
assumes "a ∈ (carrier R)"
assumes "p = monom P a m"
shows "degree (p[^]⇘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 ≠ 𝟬"
shows "ltrm (p[^]⇘P⇙(n::nat)) = (ltrm p)[^]⇘P⇙n"
proof-
have "lcf p [^]n ≠ 𝟬 ⟹ ltrm (p[^]⇘P⇙(n::nat)) = (ltrm p)[^]⇘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 ≠ 𝟬 ⟹ ltrm (p [^]⇘P⇙ n) = ltrm p [^]⇘P⇙ n)"
assume A: "lcf p [^] Suc n ≠ 𝟬"
have a: "ltrm (p [^]⇘P⇙ n) = ltrm p [^]⇘P⇙ n"
apply(cases "lcf p [^] n = 𝟬")
using A lcf_closed assms(1) apply auto[1]
by(rule IH)
have 0: "lcf (ltrm (p [^]⇘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 [^]⇘P⇙ n)) ⊗ lcf p ≠ 𝟬"
using assms A R.nat_pow_Suc IH by metis
then show "ltrm (p [^]⇘P⇙ Suc n) = ltrm p [^]⇘P⇙ Suc n"
using IH 0 assms(1) cring_ltrm_mult cfs_closed
by (smt 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 ≠ 𝟬"
shows "degree (p[^]⇘P⇙(n::nat)) = n*degree p"
proof-
have "degree ( (ltrm p)[^]⇘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[^]⇘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 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 ≠ 𝟬"
shows "deg R (a ⊙⇘UP 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 ⊙⇘UP 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) = 𝟬"
have 0: "f (deg R f) = 𝟬"
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 ⊕⇘P⇙ q )[^]⇘P⇙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 ⊕⇘P⇙ q )[^]⇘P⇙n) = (degree p)*n"
then show "⋀ p q. p ∈ carrier P ⟹ q ∈ carrier P ⟹
degree q < degree p ⟹ degree ((p ⊕⇘P⇙ q )[^]⇘P⇙(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 ⊕⇘P⇙ q )[^]⇘P⇙(Suc n)) = (degree p)*(Suc n)"
proof(cases "q = 𝟬⇘P⇙")
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 ⊕⇘P⇙ q )[^]⇘P⇙n) = (degree p)*n"
using A0 A1 A2 IH by auto
have P1: "(p ⊕⇘P⇙ q )[^]⇘P⇙(Suc n) = ((p ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ (p ⊕⇘P⇙ q )"
by simp
then have P2: "(p ⊕⇘P⇙ q )[^]⇘P⇙(Suc n) = (((p ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ p) ⊕⇘P⇙ (((p ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ q)"
by (simp add: A0 A1 UP_r_distr)
have P3: "degree (((p ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ 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 ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ 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 ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ p) > degree (((p ⊕⇘P⇙ q )[^]⇘P⇙n) ⊗⇘P⇙ 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 ⊕⇘P⇙ q )[^]⇘P⇙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 [^]⇘P⇙ m) = m*(degree p)"
proof(induction n)
case 0
show "p ∈ carrier P ⟹ 0 ≥ degree p ⟹ degree (p [^]⇘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 [^]⇘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 [^]⇘P⇙ m) = m * (degree p))"
show "p ∈ carrier P ⟹ Suc n ≥ degree p ⟹ degree (p [^]⇘P⇙ m) = m * (degree p)"
proof-
assume A0: "p ∈ carrier P"
assume A1: "Suc n ≥ degree p"
show "degree (p [^]⇘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 [^]⇘P⇙ m) = m * k"
using IH[of "q"] k_bound1 k_def q_is_poly by auto
have P_ltrm: "degree ((ltrm p) [^]⇘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 ⊕⇘P⇙ (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 [^]⇘P⇙ m) = m*(degree p)"
using deg_pow0 assms by blast
lemma(in UP_domain) ltrm_pow0:
"⋀f. f ∈ carrier P ⟹ ltrm (f [^]⇘P⇙ (n::nat)) = (ltrm f) [^]⇘P⇙ 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 [^]⇘P⇙ n) = (ltrm f) [^]⇘P⇙ n"
then show "⋀f. f ∈ carrier P ⟹ ltrm (f [^]⇘P⇙ (Suc n)) = (ltrm f) [^]⇘P⇙ (Suc n)"
proof-
fix f
assume A: "f ∈ carrier P"
show " ltrm (f [^]⇘P⇙ (Suc n)) = (ltrm f) [^]⇘P⇙ (Suc n)"
proof-
have 0: "ltrm (f [^]⇘P⇙ n) = (ltrm f) [^]⇘P⇙ n"
using A IH by blast
have 1: "ltrm (f [^]⇘P⇙ (Suc n)) = ltrm ((f [^]⇘P⇙ n)⊗⇘P⇙ 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 [^]⇘P⇙ (n::nat)) = (ltrm f) [^]⇘P⇙ 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 ⊖⇘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 ⊖⇘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 ⊖⇘P⇙ q) ≠ degree p"
proof
assume A: "degree (p ⊖⇘P⇙ q) = degree p"
have Q0: "p ⊖⇘P⇙ q = ((trunc p) ⊕⇘P⇙ (ltrm p)) ⊖⇘P⇙ ((trunc q) ⊕⇘P⇙ (ltrm p))"
using assms(1) assms(2) assms(3) trunc_simps(1) by force
have Q1: "p ⊖⇘P⇙ q = (trunc p) ⊖⇘P⇙ (trunc q)"
proof-
have "p ⊖⇘P⇙ q = ((trunc p) ⊕⇘P⇙ (ltrm p)) ⊖⇘P⇙ (trunc q) ⊖ ⇘P⇙ (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) ≠𝟬"
shows "lcf (a ⊙⇘P⇙ p) = a ⊗ (lcf p)"
proof-
have 0: "lcf (a ⊙⇘P⇙ p) = lcf (ltrm (a ⊙⇘P⇙ p))"
using assms lcf_eq smult_closed by blast
have 1: "degree (a ⊙⇘P⇙ p) = degree p"
by (smt 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⇙ p) = lcf (a ⊙⇘P⇙ (ltrm p))"
using lcf_eq[of "a ⊙⇘P⇙ 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⇙ p) = a ⊗ (lcf p)"
proof-
have "lcf (a ⊙⇘P⇙ p) = lcf (ltrm (a ⊙⇘P⇙ p))"
using lcf_eq UP_smult_closed assms(1) assms(2) by blast
then have "lcf (a ⊙⇘P⇙ p) = lcf (a ⊙⇘P⇙ (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) ≠𝟬"
shows "lcf (p ⊗⇘P⇙ q) = (lcf p) ⊗ (lcf q)"
using assms cring_ltrm_mult
by (smt 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 ⊗⇘P⇙ q) = (lcf p) ⊗ (lcf q)"
by (smt ltrm_deg_0 R.integral_iff assms(1) assms(2) cfs_closed cring_lcf_mult deg_zero deg_ltrm local.integral_iff monom_zero)
lemma(in UP_cring) cring_lcf_pow:
assumes "p ∈ carrier P"
assumes "(lcf p)[^]n ≠𝟬"
shows "lcf (p[^]⇘P⇙(n::nat)) = (lcf p)[^]n"
by (smt 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[^]⇘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[^]⇘P⇙(n::nat)) = (lcf p)[^]n"
show "lcf (p[^]⇘P⇙(Suc n)) = (lcf p)[^](Suc n)"
proof-
have "lcf (p[^]⇘P⇙(Suc n)) = lcf ((p[^]⇘P⇙n) ⊗⇘P⇙p)"
by simp
then have "lcf (p[^]⇘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 = 𝟬"
shows "ctrm f = 𝟬⇘P⇙"
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 = 𝟬"
shows "f = 𝟬⇘P⇙"
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 ⊕⇘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) = 𝟬"
by (metis ltrm_cfs_above_deg ltrm_cfs zcf_def assms(1) assms(2))
lemma zcf_zero[simp]:
"zcf 𝟬⇘P⇙ = 𝟬"
using zcf_degree_zero by auto
lemma zcf_one[simp]:
"zcf 𝟭⇘P⇙ = 𝟭"
by (simp add: zcf_def)
lemma ctrm_smult:
assumes "f ∈ carrier P"
assumes "a ∈ carrier R"
shows "ctrm (a ⊙⇘P⇙ f) = a ⊙⇘P⇙(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)) = 𝟬⇘P⇙"
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 ⊕⇘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 ⊕⇘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 ⊙⇘P⇙ monom P 𝟭 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 ⊕⇘P⇙ q)"
assumes monic_monom: "⋀n. Q (monom P 𝟭 n)"
assumes smult: "⋀p a . a ∈ carrier R ⟹ p ∈ carrier P ⟹ Q p ⟹ Q (a ⊙⇘P⇙ 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 𝟭 n"] monom_mult_smult[of a 𝟭 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 ≠ 𝟬 ⟹ p ∈ carrier P ⟹ degree p < n ⟹ Q p ⟹
Q(p ⊕⇘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 = (⨁⇘R⇙i∈{..deg R f}. (λx. x) (coeff (UP R) f i) ⊗⇘R⇙ x [^]⇘R⇙ i)"
apply(simp add:UnivPoly.eval_def) done
then have "to_fun f x = (⨁⇘R⇙i∈{..deg R f}. (λx. x) (coeff (UP R) f i) ⊗⇘R⇙ x [^]⇘R⇙ 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 ⊕⇘P⇙ 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 ⊗⇘P⇙ 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 "𝟭⇘P⇙" 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 (⊖⇘S⇙ a) = ⊖ (f a)"
proof-
have "f (a ⊖⇘S⇙ a) = (f a) ⊕ f (⊖⇘S⇙ 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 (⊖⇘S⇙ a) = 𝟬 "
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 (⊖⇘P⇙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 ⊗⇘P⇙ y) = to_fun x ⊗⇘function_ring (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 ⊕⇘P⇙ y) = to_fun x ⊕⇘function_ring (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 𝟭⇘P⇙ = 𝟭⇘Fun 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 𝟬⇘P⇙ = 𝟬⇘Fun 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 𝟭⇘P⇙ a = 𝟭"
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 𝟬⇘P⇙ a = 𝟬"
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[^]⇘UP 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 ⊕⇘UP 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 ⊕⇘P⇙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 ⊕⇘P⇙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) ⊗⇘UP R⇙ f = b ⊙⇘UP R⇙ f"
"f ⊗⇘UP R⇙ (to_polynomial R b) = b ⊙⇘UP 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 ⊕⇘P⇙ 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 ⊗⇘P⇙ 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 ⊖⇘P⇙ 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) = ⊖⇘P⇙ 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) [^]⇘P⇙ (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 ⊕⇘P⇙ h) = (rev_sub g f) ⊕⇘P⇙ (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 ⊕⇘P⇙ h) of g) = ((f of g) ⊕⇘P⇙ (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 ⊗⇘P⇙ h) = (rev_sub g f) ⊗⇘P⇙ (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 ⊗⇘P⇙ h) of g) = ((f of g) ⊗⇘P⇙ (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 ⊗⇘UP R⇙ (g[^]⇘UP R⇙ (n::nat))"
"sub (monom (UP R) a n) g = a ⊙⇘UP R⇙ (g[^]⇘UP 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 ⊙⇘P⇙ g[^]⇘P⇙ 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 ≠𝟬"
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) ⊗⇘P⇙ (g[^]⇘P⇙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 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 ≠𝟬"
assumes "f = monom P a n"
assumes "g ∈ carrier P"
assumes "a ⊗ (lcf g [^] n) ≠ 𝟬"
shows "degree (f of g) = n*(degree g)"
proof-
have 0: "f of g = (to_poly a) ⊗⇘P⇙ (g[^]⇘P⇙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 [^]⇘P⇙ n) ≠ 𝟬"
using assms
by (smt 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[^]⇘P⇙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 ≠𝟬"
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) ⊗⇘P⇙ (g[^]⇘P⇙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 [^]⇘P⇙ n = monom P (b[^]n) 0"
apply(induction n)
apply fastforce[1]
proof- fix n::nat assume IH: "monom P b 0 [^]⇘P⇙ n = monom P (b [^] n) 0"
have "monom P b 0 [^]⇘P⇙ Suc n = (monom P (b[^]n) 0) ⊗⇘P⇙ monom P b 0"
using IH by simp
then have "monom P b 0 [^]⇘P⇙ 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 [^]⇘P⇙ Suc n = monom P (b [^] Suc n) 0 "
by simp
qed
then have 0: "a ⊙⇘P⇙ monom P b 0 [^]⇘P⇙ 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 ⊙⇘P⇙ monom P b 0 [^]⇘P⇙ n› b_def)
qed
have P2: "p of g = (trunc p of g) ⊕⇘P⇙ ((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) ⊕⇘P⇙ ((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)) ≠ 𝟬"
shows "degree (f of g) = degree f * degree g"
proof-
have 0: "f of g = (trunc f of g) ⊕⇘P⇙ ((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 ≠ 𝟬"
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 "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 ≠ 𝟬⇘P⇙"
assumes "f ≠ 𝟬⇘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) ⊕⇘P⇙ ((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
proof(cases "degree g = 0")
case True
then show ?thesis
by (simp add: Suc(2) assms(1) sub_in_const)
next
case False
then show ?thesis
proof-
have P3: "degree ((trunc p) of g) < degree ((ltrm p) of g)"
using False D P1 P2
by (metis (no_types, lifting) A0 mult.commute mult_right_cancel
nat_less_le nat_mult_le_cancel_disj trunc_degree zero_less_Suc)
then show ?thesis
by (simp add: A0 ltrm_closed P0 P2 assms(1) equal_deg_sum sub_closed trunc_closed)
qed
qed
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 ≠ 𝟬⇘P⇙"
shows "degree (f of g) = degree f * degree g"
proof(cases "f = 𝟬⇘P⇙")
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)) ≠ 𝟬"
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) ⊕⇘P⇙((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 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) ⊕⇘P⇙((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) ≠𝟬"
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)) ⊗⇘P⇙ (g[^]⇘P⇙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) ⊙⇘P⇙(g[^]⇘P⇙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))) ⊗⇘P⇙ (ltrm (g[^]⇘P⇙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)) ⊗⇘P⇙ (ltrm (g[^]⇘P⇙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) ⊙⇘P⇙ ((ltrm g)[^]⇘P⇙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)[^]⇘P⇙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) ≠𝟬"
shows "ltrm ((ltrm f) of g) = (lcf f) ⊙⇘P⇙ ((ltrm g)[^]⇘P⇙n)"
by (smt 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) ⊙⇘P⇙ ((ltrm g)[^]⇘P⇙n)"
by (smt Group.nat_pow_0 lcf_of_sub_in_ltrm lcf_pow lcf_scalar_mult ltrm_closed
ltrm_pow0 ltrm_smult P.nat_pow_closed P_def UP_ring.monom_one UP_ring_axioms assms(1)
assms(2) assms(3) assms(4) cfs_closed coeff_simp deg_const deg_nzero_nzero deg_pow
deg_smult deg_ltrm lcoeff_nonzero2 nat_less_le sub_deg)
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) ≠𝟬"
shows "ltrm (f of g) = (lcf f) ⊙⇘P⇙ ((ltrm g)[^]⇘P⇙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) ⊙⇘P⇙ ((ltrm g)[^]⇘P⇙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 ⊙⇘P⇙ (q of r)[^]⇘P⇙ 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 ⊙⇘P⇙ q[^]⇘P⇙ 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) ⊗⇘P⇙ q[^]⇘P⇙ 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) ⊗⇘P⇙ (q[^]⇘P⇙ 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) ⊗⇘P⇙ (q[^]⇘P⇙ n of r)"
using RHS2 a_def assms(3) sub_to_poly by auto
have RHS4: "((ltrm f) of q) of r = a ⊙⇘P⇙ ((q[^]⇘P⇙ 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)[^]⇘P⇙ n = ((q[^]⇘P⇙ 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) ⊕⇘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)) ⊕⇘P⇙ ((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) ⊕⇘P⇙ (((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) ⊕⇘P⇙ ((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)⊕⇘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⊙⇘P⇙f ) of q = a⊙⇘P⇙(f of q)"
proof-
have "(a⊙⇘P⇙f ) of q = ((to_poly a) ⊗⇘P⇙f) of q"
using assms by (metis P_def monom_mult_is_smult to_polynomial_def)
then have "(a⊙⇘P⇙f ) of q = ((to_poly a) of q) ⊗⇘P⇙(f of q)"
by (simp add: assms(1) assms(2) assms(3) sub_mult to_poly_closed)
then have "(a⊙⇘P⇙f ) of q = (to_poly a) ⊗⇘P⇙(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 ⊙⇘P⇙ (g[^]⇘P⇙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 ⊙⇘P⇙ (g[^]⇘P⇙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 [^]⇘UP 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 [^]⇘UP 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 ⊕⇘P⇙ (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 ⊙⇘P⇙ f) b = c ⊗(to_fun f b)"
proof-
have "(c ⊙⇘P⇙ f) = (to_poly c) ⊗⇘P⇙ f"
by (metis P_def assms(1) assms(3) monom_mult_is_smult to_polynomial_def)
then have "to_fun (c ⊙⇘P⇙ 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 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) 𝟬"
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 𝟬"
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) ⊗⇘P⇙ q) = 𝟬"
using zcf_to_fun[of "ltrm p ⊗⇘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 ⊗⇘P⇙ q) = (zcf p) ⊗ (zcf q)"
using zcf_to_fun[of " p ⊗⇘P⇙<