(* Title: HOL/Algebra/Polynomials.thy Author: Paulo Emílio de Vilhena *) theory Polynomials imports Ring Ring_Divisibility Subrings begin section ‹Polynomials› subsection ‹Definitions› abbreviation lead_coeff :: "'a list ⇒ 'a" where "lead_coeff ≡ hd" abbreviation degree :: "'a list ⇒ nat" where "degree p ≡ length p - 1" definition polynomial :: "_ ⇒ 'a set ⇒ 'a list ⇒ bool" ("polynomialı") where "polynomial⇘R⇙ K p ⟷ p = [] ∨ (set p ⊆ K ∧ lead_coeff p ≠ 𝟬⇘R⇙)" definition (in ring) monom :: "'a ⇒ nat ⇒ 'a list" where "monom a n = a # (replicate n 𝟬⇘R⇙)" fun (in ring) eval :: "'a list ⇒ 'a ⇒ 'a" where "eval [] = (λ_. 𝟬)" | "eval p = (λx. ((lead_coeff p) ⊗ (x [^] (degree p))) ⊕ (eval (tl p) x))" fun (in ring) coeff :: "'a list ⇒ nat ⇒ 'a" where "coeff [] = (λ_. 𝟬)" | "coeff p = (λi. if i = degree p then lead_coeff p else (coeff (tl p)) i)" fun (in ring) normalize :: "'a list ⇒ 'a list" where "normalize [] = []" | "normalize p = (if lead_coeff p ≠ 𝟬 then p else normalize (tl p))" fun (in ring) poly_add :: "'a list ⇒ 'a list ⇒ 'a list" where "poly_add p1 p2 = (if length p1 ≥ length p2 then normalize (map2 (⊕) p1 ((replicate (length p1 - length p2) 𝟬) @ p2)) else poly_add p2 p1)" fun (in ring) poly_mult :: "'a list ⇒ 'a list ⇒ 'a list" where "poly_mult [] p2 = []" | "poly_mult p1 p2 = poly_add ((map (λa. lead_coeff p1 ⊗ a) p2) @ (replicate (degree p1) 𝟬)) (poly_mult (tl p1) p2)" fun (in ring) dense_repr :: "'a list ⇒ ('a × nat) list" where "dense_repr [] = []" | "dense_repr p = (if lead_coeff p ≠ 𝟬 then (lead_coeff p, degree p) # (dense_repr (tl p)) else (dense_repr (tl p)))" fun (in ring) poly_of_dense :: "('a × nat) list ⇒ 'a list" where "poly_of_dense dl = foldr (λ(a, n) l. poly_add (monom a n) l) dl []" definition (in ring) poly_of_const :: "'a ⇒ 'a list" where "poly_of_const = (λk. normalize [ k ])" subsection ‹Basic Properties› context ring begin lemma polynomialI [intro]: "⟦ set p ⊆ K; lead_coeff p ≠ 𝟬 ⟧ ⟹ polynomial K p" unfolding polynomial_def by auto lemma polynomial_incl: "polynomial K p ⟹ set p ⊆ K" unfolding polynomial_def by auto lemma monom_in_carrier [intro]: "a ∈ carrier R ⟹ set (monom a n) ⊆ carrier R" unfolding monom_def by auto lemma lead_coeff_not_zero: "polynomial K (a # p) ⟹ a ∈ K - { 𝟬 }" unfolding polynomial_def by simp lemma zero_is_polynomial [intro]: "polynomial K []" unfolding polynomial_def by simp lemma const_is_polynomial [intro]: "a ∈ K - { 𝟬 } ⟹ polynomial K [ a ]" unfolding polynomial_def by auto lemma normalize_gives_polynomial: "set p ⊆ K ⟹ polynomial K (normalize p)" by (induction p) (auto simp add: polynomial_def) lemma normalize_in_carrier: "set p ⊆ carrier R ⟹ set (normalize p) ⊆ carrier R" by (induction p) (auto) lemma normalize_polynomial: "polynomial K p ⟹ normalize p = p" unfolding polynomial_def by (cases p) (auto) lemma normalize_idem: "normalize ((normalize p) @ q) = normalize (p @ q)" by (induct p) (auto) lemma normalize_length_le: "length (normalize p) ≤ length p" by (induction p) (auto) lemma eval_in_carrier: "⟦ set p ⊆ carrier R; x ∈ carrier R ⟧ ⟹ (eval p) x ∈ carrier R" by (induction p) (auto) lemma coeff_in_carrier [simp]: "set p ⊆ carrier R ⟹ (coeff p) i ∈ carrier R" by (induction p) (auto) lemma lead_coeff_simp [simp]: "p ≠ [] ⟹ (coeff p) (degree p) = lead_coeff p" by (metis coeff.simps(2) list.exhaust_sel) lemma coeff_list: "map (coeff p) (rev [0..< length p]) = p" proof (induction p) case Nil thus ?case by simp next case (Cons a p) have "map (coeff (a # p)) (rev [0..<length (a # p)]) = a # (map (coeff p) (rev [0..<length p]))" by auto also have " ... = a # p" using Cons by simp finally show ?case . qed lemma coeff_nth: "i < length p ⟹ (coeff p) i = p ! (length p - 1 - i)" proof - assume i_lt: "i < length p" hence "(coeff p) i = (map (coeff p) [0..< length p]) ! i" by simp also have " ... = (rev (map (coeff p) (rev [0..< length p]))) ! i" by (simp add: rev_map) also have " ... = (map (coeff p) (rev [0..< length p])) ! (length p - 1 - i)" using coeff_list i_lt rev_nth by auto also have " ... = p ! (length p - 1 - i)" using coeff_list[of p] by simp finally show "(coeff p) i = p ! (length p - 1 - i)" . qed lemma coeff_iff_length_cond: assumes "length p1 = length p2" shows "p1 = p2 ⟷ coeff p1 = coeff p2" proof show "p1 = p2 ⟹ coeff p1 = coeff p2" by simp next assume A: "coeff p1 = coeff p2" have "p1 = map (coeff p1) (rev [0..< length p1])" using coeff_list[of p1] by simp also have " ... = map (coeff p2) (rev [0..< length p2])" using A assms by simp also have " ... = p2" using coeff_list[of p2] by simp finally show "p1 = p2" . qed lemma coeff_img_restrict: "(coeff p) ` {..< length p} = set p" using coeff_list[of p] by (metis atLeast_upt image_set set_rev) lemma coeff_length: "⋀i. i ≥ length p ⟹ (coeff p) i = 𝟬" by (induction p) (auto) lemma coeff_degree: "⋀i. i > degree p ⟹ (coeff p) i = 𝟬" using coeff_length by (simp) lemma replicate_zero_coeff [simp]: "coeff (replicate n 𝟬) = (λ_. 𝟬)" by (induction n) (auto) lemma scalar_coeff: "a ∈ carrier R ⟹ coeff (map (λb. a ⊗ b) p) = (λi. a ⊗ (coeff p) i)" by (induction p) (auto) lemma monom_coeff: "coeff (monom a n) = (λi. if i = n then a else 𝟬)" unfolding monom_def by (induction n) (auto) lemma coeff_img: "(coeff p) ` {..< length p} = set p" "(coeff p) ` { length p ..} = { 𝟬 }" "(coeff p) ` UNIV = (set p) ∪ { 𝟬 }" using coeff_img_restrict proof (simp) show coeff_img_up: "(coeff p) ` { length p ..} = { 𝟬 }" using coeff_length[of p] by force from coeff_img_up and coeff_img_restrict[of p] show "(coeff p) ` UNIV = (set p) ∪ { 𝟬 }" by force qed lemma degree_def': assumes "polynomial K p" shows "degree p = (LEAST n. ∀i. i > n ⟶ (coeff p) i = 𝟬)" proof (cases p) case Nil thus ?thesis by auto next define P where "P = (λn. ∀i. i > n ⟶ (coeff p) i = 𝟬)" case (Cons a ps) hence "(coeff p) (degree p) ≠ 𝟬" using assms unfolding polynomial_def by auto hence "⋀n. n < degree p ⟹ ¬ P n" unfolding P_def by auto moreover have "P (degree p)" unfolding P_def using coeff_degree[of p] by simp ultimately have "degree p = (LEAST n. P n)" by (meson LeastI nat_neq_iff not_less_Least) thus ?thesis unfolding P_def . qed lemma coeff_iff_polynomial_cond: assumes "polynomial K p1" and "polynomial K p2" shows "p1 = p2 ⟷ coeff p1 = coeff p2" proof show "p1 = p2 ⟹ coeff p1 = coeff p2" by simp next assume coeff_eq: "coeff p1 = coeff p2" hence deg_eq: "degree p1 = degree p2" using degree_def'[OF assms(1)] degree_def'[OF assms(2)] by auto thus "p1 = p2" proof (cases) assume "p1 ≠ [] ∧ p2 ≠ []" hence "length p1 = length p2" using deg_eq by (simp add: Nitpick.size_list_simp(2)) thus ?thesis using coeff_iff_length_cond[of p1 p2] coeff_eq by simp next { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2" have "p2 = []" proof (rule ccontr) assume "p2 ≠ []" hence "(coeff p2) (degree p2) ≠ 𝟬" using A(3) unfolding polynomial_def by (metis coeff.simps(2) list.collapse) moreover have "(coeff p1) ` UNIV = { 𝟬 }" using A(1) by auto hence "(coeff p2) ` UNIV = { 𝟬 }" using A(2) by simp ultimately show False by blast qed } note aux_lemma = this assume "¬ (p1 ≠ [] ∧ p2 ≠ [])" hence "p1 = [] ∨ p2 = []" by simp thus ?thesis using assms coeff_eq aux_lemma[of p1 p2] aux_lemma[of p2 p1] by auto qed qed lemma normalize_lead_coeff: assumes "length (normalize p) < length p" shows "lead_coeff p = 𝟬" proof (cases p) case Nil thus ?thesis using assms by simp next case (Cons a ps) thus ?thesis using assms by (cases "a = 𝟬") (auto) qed lemma normalize_length_lt: assumes "lead_coeff p = 𝟬" and "length p > 0" shows "length (normalize p) < length p" proof (cases p) case Nil thus ?thesis using assms by simp next case (Cons a ps) thus ?thesis using normalize_length_le[of ps] assms by simp qed lemma normalize_length_eq: assumes "lead_coeff p ≠ 𝟬" shows "length (normalize p) = length p" using normalize_length_le[of p] assms nat_less_le normalize_lead_coeff by auto lemma normalize_replicate_zero: "normalize ((replicate n 𝟬) @ p) = normalize p" by (induction n) (auto) lemma normalize_def': shows "p = (replicate (length p - length (normalize p)) 𝟬) @ (drop (length p - length (normalize p)) p)" (is ?statement1) and "normalize p = drop (length p - length (normalize p)) p" (is ?statement2) proof - show ?statement1 proof (induction p) case Nil thus ?case by simp next case (Cons a p) thus ?case proof (cases "a = 𝟬") assume "a ≠ 𝟬" thus ?case using Cons by simp next assume eq_zero: "a = 𝟬" hence len_eq: "Suc (length p - length (normalize p)) = length (a # p) - length (normalize (a # p))" by (simp add: Suc_diff_le normalize_length_le) have "a # p = 𝟬 # (replicate (length p - length (normalize p)) 𝟬 @ drop (length p - length (normalize p)) p)" using eq_zero Cons by simp also have " ... = (replicate (Suc (length p - length (normalize p))) 𝟬 @ drop (Suc (length p - length (normalize p))) (a # p))" by simp also have " ... = (replicate (length (a # p) - length (normalize (a # p))) 𝟬 @ drop (length (a # p) - length (normalize (a # p))) (a # p))" using len_eq by simp finally show ?case . qed qed next show ?statement2 proof - have "∃m. normalize p = drop m p" proof (induction p) case Nil thus ?case by simp next case (Cons a p) thus ?case apply (cases "a = 𝟬") apply (auto) apply (metis drop_Suc_Cons) apply (metis drop0) done qed then obtain m where m: "normalize p = drop m p" by auto hence "length (normalize p) = length p - m" by simp thus ?thesis using m by (metis rev_drop rev_rev_ident take_rev) qed qed corollary normalize_trick: shows "p = (replicate (length p - length (normalize p)) 𝟬) @ (normalize p)" using normalize_def'(1)[of p] unfolding sym[OF normalize_def'(2)] . lemma normalize_coeff: "coeff p = coeff (normalize p)" proof (induction p) case Nil thus ?case by simp next case (Cons a p) have "coeff (normalize p) (length p) = 𝟬" using normalize_length_le[of p] coeff_degree[of "normalize p"] coeff_length by blast then show ?case using Cons by (cases "a = 𝟬") (auto) qed lemma append_coeff: "coeff (p @ q) = (λi. if i < length q then (coeff q) i else (coeff p) (i - length q))" proof (induction p) case Nil thus ?case using coeff_length[of q] by auto next case (Cons a p) have "coeff ((a # p) @ q) = (λi. if i = length p + length q then a else (coeff (p @ q)) i)" by auto also have " ... = (λi. if i = length p + length q then a else if i < length q then (coeff q) i else (coeff p) (i - length q))" using Cons by auto also have " ... = (λi. if i < length q then (coeff q) i else if i = length p + length q then a else (coeff p) (i - length q))" by auto also have " ... = (λi. if i < length q then (coeff q) i else if i - length q = length p then a else (coeff p) (i - length q))" by fastforce also have " ... = (λi. if i < length q then (coeff q) i else (coeff (a # p)) (i - length q))" by auto finally show ?case . qed lemma prefix_replicate_zero_coeff: "coeff p = coeff ((replicate n 𝟬) @ p)" using append_coeff[of "replicate n 𝟬" p] replicate_zero_coeff[of n] coeff_length[of p] by auto (* ========================================================================== *) context fixes K :: "'a set" assumes K: "subring K R" begin lemma polynomial_in_carrier [intro]: "polynomial K p ⟹ set p ⊆ carrier R" unfolding polynomial_def using subringE(1)[OF K] by auto lemma carrier_polynomial [intro]: "polynomial K p ⟹ polynomial (carrier R) p" unfolding polynomial_def using subringE(1)[OF K] by auto lemma append_is_polynomial: "⟦ polynomial K p; p ≠ [] ⟧ ⟹ polynomial K (p @ (replicate n 𝟬))" unfolding polynomial_def using subringE(2)[OF K] by auto lemma lead_coeff_in_carrier: "polynomial K (a # p) ⟹ a ∈ carrier R - { 𝟬 }" unfolding polynomial_def using subringE(1)[OF K] by auto lemma monom_is_polynomial [intro]: "a ∈ K - { 𝟬 } ⟹ polynomial K (monom a n)" unfolding polynomial_def monom_def using subringE(2)[OF K] by auto lemma eval_poly_in_carrier: "⟦ polynomial K p; x ∈ carrier R ⟧ ⟹ (eval p) x ∈ carrier R" using eval_in_carrier[OF polynomial_in_carrier] . lemma poly_coeff_in_carrier [simp]: "polynomial K p ⟹ coeff p i ∈ carrier R" using coeff_in_carrier[OF polynomial_in_carrier] . end (* of fixed K context. *) (* ========================================================================== *) subsection ‹Polynomial Addition› (* ========================================================================== *) context fixes K :: "'a set" assumes K: "subring K R" begin lemma poly_add_is_polynomial: assumes "set p1 ⊆ K" and "set p2 ⊆ K" shows "polynomial K (poly_add p1 p2)" proof - { fix p1 p2 assume A: "set p1 ⊆ K" "set p2 ⊆ K" "length p1 ≥ length p2" hence "polynomial K (poly_add p1 p2)" proof - define p2' where "p2' = (replicate (length p1 - length p2) 𝟬) @ p2" hence "set p2' ⊆ K" and "length p1 = length p2'" using A(2-3) subringE(2)[OF K] by auto hence "set (map2 (⊕) p1 p2') ⊆ K" using A(1) subringE(7)[OF K] by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD) thus ?thesis unfolding p2'_def using normalize_gives_polynomial A(3) by simp qed } thus ?thesis using assms by auto qed lemma poly_add_closed: "⟦ polynomial K p1; polynomial K p2 ⟧ ⟹ polynomial K (poly_add p1 p2)" using poly_add_is_polynomial polynomial_incl by simp lemma poly_add_length_eq: assumes "polynomial K p1" "polynomial K p2" and "length p1 ≠ length p2" shows "length (poly_add p1 p2) = max (length p1) (length p2)" proof - { fix p1 p2 assume A: "polynomial K p1" "polynomial K p2" "length p1 > length p2" hence "length (poly_add p1 p2) = max (length p1) (length p2)" proof - let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2" have p1: "p1 ≠ []" and p2: "?p2 ≠ []" using A(3) by auto then have "zip p1 (replicate (length p1 - length p2) 𝟬 @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) 𝟬 @ p2) # tl (replicate (length p1 - length p2) 𝟬 @ p2))" by auto hence "lead_coeff (map2 (⊕) p1 ?p2) = lead_coeff p1 ⊕ lead_coeff ?p2" by simp moreover have "lead_coeff p1 ∈ carrier R" using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto ultimately have "lead_coeff (map2 (⊕) p1 ?p2) = lead_coeff p1" using A(3) by auto moreover have "lead_coeff p1 ≠ 𝟬" using p1 A(1) unfolding polynomial_def by simp ultimately have "length (normalize (map2 (⊕) p1 ?p2)) = length p1" using normalize_length_eq by auto thus ?thesis using A(3) by auto qed } thus ?thesis using assms by auto qed lemma poly_add_degree_eq: assumes "polynomial K p1" "polynomial K p2" and "degree p1 ≠ degree p2" shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)" using poly_add_length_eq[OF assms(1-2)] assms(3) by simp end (* of fixed K context. *) (* ========================================================================== *) lemma poly_add_in_carrier: "⟦ set p1 ⊆ carrier R; set p2 ⊆ carrier R ⟧ ⟹ set (poly_add p1 p2) ⊆ carrier R" using polynomial_incl[OF poly_add_is_polynomial[OF carrier_is_subring]] by simp lemma poly_add_length_le: "length (poly_add p1 p2) ≤ max (length p1) (length p2)" proof - { fix p1 p2 :: "'a list" assume A: "length p1 ≥ length p2" let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2" have "length (poly_add p1 p2) ≤ max (length p1) (length p2)" using normalize_length_le[of "map2 (⊕) p1 ?p2"] A by auto } thus ?thesis by (metis le_cases max.commute poly_add.simps) qed lemma poly_add_degree: "degree (poly_add p1 p2) ≤ max (degree p1) (degree p2)" using poly_add_length_le by (meson diff_le_mono le_max_iff_disj) lemma poly_add_coeff_aux: assumes "length p1 ≥ length p2" shows "coeff (poly_add p1 p2) = (λi. ((coeff p1) i) ⊕ ((coeff p2) i))" proof fix i have "i < length p1 ⟹ (coeff (poly_add p1 p2)) i = ((coeff p1) i) ⊕ ((coeff p2) i)" proof - let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2" have len_eqs: "length p1 = length ?p2" "length (map2 (⊕) p1 ?p2) = length p1" using assms by auto assume i_lt: "i < length p1" have "(coeff (poly_add p1 p2)) i = (coeff (map2 (⊕) p1 ?p2)) i" using normalize_coeff[of "map2 (⊕) p1 ?p2"] assms by auto also have " ... = (map2 (⊕) p1 ?p2) ! (length p1 - 1 - i)" using coeff_nth[of i "map2 (⊕) p1 ?p2"] len_eqs(2) i_lt by auto also have " ... = (p1 ! (length p1 - 1 - i)) ⊕ (?p2 ! (length ?p2 - 1 - i))" using len_eqs i_lt by auto also have " ... = ((coeff p1) i) ⊕ ((coeff ?p2) i)" using coeff_nth[of i p1] coeff_nth[of i ?p2] i_lt len_eqs(1) by auto also have " ... = ((coeff p1) i) ⊕ ((coeff p2) i)" using prefix_replicate_zero_coeff by simp finally show "(coeff (poly_add p1 p2)) i = ((coeff p1) i) ⊕ ((coeff p2) i)" . qed moreover have "i ≥ length p1 ⟹ (coeff (poly_add p1 p2)) i = ((coeff p1) i) ⊕ ((coeff p2) i)" using coeff_length[of "poly_add p1 p2"] coeff_length[of p1] coeff_length[of p2] poly_add_length_le[of p1 p2] assms by auto ultimately show "(coeff (poly_add p1 p2)) i = ((coeff p1) i) ⊕ ((coeff p2) i)" using not_le by blast qed lemma poly_add_coeff: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "coeff (poly_add p1 p2) = (λi. ((coeff p1) i) ⊕ ((coeff p2) i))" proof - have "length p1 ≥ length p2 ∨ length p2 > length p1" by auto thus ?thesis proof assume "length p1 ≥ length p2" thus ?thesis using poly_add_coeff_aux by simp next assume "length p2 > length p1" hence "coeff (poly_add p1 p2) = (λi. ((coeff p2) i) ⊕ ((coeff p1) i))" using poly_add_coeff_aux by simp thus ?thesis using assms by (simp add: add.m_comm) qed qed lemma poly_add_comm: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_add p1 p2 = poly_add p2 p1" proof - have "coeff (poly_add p1 p2) = coeff (poly_add p2 p1)" using poly_add_coeff[OF assms] poly_add_coeff[OF assms(2) assms(1)] coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] add.m_comm by auto thus ?thesis using coeff_iff_polynomial_cond[OF poly_add_is_polynomial[OF carrier_is_subring assms] poly_add_is_polynomial[OF carrier_is_subring assms(2,1)]] by simp qed lemma poly_add_monom: assumes "set p ⊆ carrier R" and "a ∈ carrier R - { 𝟬 }" shows "poly_add (monom a (length p)) p = a # p" unfolding monom_def using assms by (induction p) (auto) lemma poly_add_append_replicate: assumes "set p ⊆ carrier R" "set q ⊆ carrier R" shows "poly_add (p @ (replicate (length q) 𝟬)) q = normalize (p @ q)" proof - have "map2 (⊕) (p @ (replicate (length q) 𝟬)) ((replicate (length p) 𝟬) @ q) = p @ q" using assms by (induct p) (induct q, auto) thus ?thesis by simp qed lemma poly_add_append_zero: assumes "set p ⊆ carrier R" "set q ⊆ carrier R" shows "poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ]) = normalize ((poly_add p q) @ [ 𝟬 ])" proof - have in_carrier: "set (p @ [ 𝟬 ]) ⊆ carrier R" "set (q @ [ 𝟬 ]) ⊆ carrier R" using assms by auto have "coeff (poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ])) = coeff ((poly_add p q) @ [ 𝟬 ])" using append_coeff[of p "[ 𝟬 ]"] poly_add_coeff[OF in_carrier] append_coeff[of q "[ 𝟬 ]"] append_coeff[of "poly_add p q" "[ 𝟬 ]"] poly_add_coeff[OF assms] assms[THEN coeff_in_carrier] by auto hence "coeff (poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ])) = coeff (normalize ((poly_add p q) @ [ 𝟬 ]))" using normalize_coeff by simp moreover have "set ((poly_add p q) @ [ 𝟬 ]) ⊆ carrier R" using poly_add_in_carrier[OF assms] by simp ultimately show ?thesis using coeff_iff_polynomial_cond[OF poly_add_is_polynomial[OF carrier_is_subring in_carrier] normalize_gives_polynomial] by simp qed lemma poly_add_normalize_aux: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_add p1 p2 = poly_add (normalize p1) p2" proof - { fix n p1 p2 assume "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" hence "poly_add p1 p2 = poly_add ((replicate n 𝟬) @ p1) p2" proof (induction n) case 0 thus ?case by simp next { fix p1 p2 :: "'a list" assume in_carrier: "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" have "poly_add p1 p2 = poly_add (𝟬 # p1) p2" proof - have "length p1 ≥ length p2 ⟹ ?thesis" proof - assume A: "length p1 ≥ length p2" let ?p2 = "λn. (replicate n 𝟬) @ p2" have "poly_add p1 p2 = normalize (map2 (⊕) (𝟬 # p1) (𝟬 # ?p2 (length p1 - length p2)))" using A by simp also have " ... = normalize (map2 (⊕) (𝟬 # p1) (?p2 (length (𝟬 # p1) - length p2)))" by (simp add: A Suc_diff_le) also have " ... = poly_add (𝟬 # p1) p2" using A by simp finally show ?thesis . qed moreover have "length p2 > length p1 ⟹ ?thesis" proof - assume A: "length p2 > length p1" let ?f = "λn p. (replicate n 𝟬) @ p" have "poly_add p1 p2 = poly_add p2 p1" using A by simp also have " ... = normalize (map2 (⊕) p2 (?f (length p2 - length p1) p1))" using A by simp also have " ... = normalize (map2 (⊕) p2 (?f (length p2 - Suc (length p1)) (𝟬 # p1)))" by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same) also have " ... = poly_add p2 (𝟬 # p1)" using A by simp also have " ... = poly_add (𝟬 # p1) p2" using poly_add_comm[of p2 "𝟬 # p1"] in_carrier by auto finally show ?thesis . qed ultimately show ?thesis by auto qed } note aux_lemma = this case (Suc n) hence in_carrier: "set (replicate n 𝟬 @ p1) ⊆ carrier R" by auto have "poly_add p1 p2 = poly_add (replicate n 𝟬 @ p1) p2" using Suc by simp also have " ... = poly_add (replicate (Suc n) 𝟬 @ p1) p2" using aux_lemma[OF in_carrier Suc(3)] by simp finally show ?case . qed } note aux_lemma = this have "poly_add p1 p2 = poly_add ((replicate (length p1 - length (normalize p1)) 𝟬) @ normalize p1) p2" using normalize_def'[of p1] by simp also have " ... = poly_add (normalize p1) p2" using aux_lemma[OF normalize_in_carrier[OF assms(1)] assms(2)] by simp finally show ?thesis . qed lemma poly_add_normalize: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_add p1 p2 = poly_add (normalize p1) p2" and "poly_add p1 p2 = poly_add p1 (normalize p2)" and "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)" proof - show "poly_add p1 p2 = poly_add p1 (normalize p2)" unfolding poly_add_comm[OF assms] poly_add_normalize_aux[OF assms(2) assms(1)] poly_add_comm[OF normalize_in_carrier[OF assms(2)] assms(1)] by simp next show "poly_add p1 p2 = poly_add (normalize p1) p2" using poly_add_normalize_aux[OF assms] . also have " ... = poly_add (normalize p2) (normalize p1)" unfolding poly_add_comm[OF normalize_in_carrier[OF assms(1)] assms(2)] poly_add_normalize_aux[OF assms(2) normalize_in_carrier[OF assms(1)]] by simp finally show "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)" unfolding poly_add_comm[OF assms[THEN normalize_in_carrier]] . qed lemma poly_add_zero': assumes "set p ⊆ carrier R" shows "poly_add p [] = normalize p" and "poly_add [] p = normalize p" proof - have "map2 (⊕) p (replicate (length p) 𝟬) = p" using assms by (induct p) (auto) thus "poly_add p [] = normalize p" and "poly_add [] p = normalize p" using poly_add_comm[OF assms, of "[]"] by simp+ qed lemma poly_add_zero: assumes "subring K R" "polynomial K p" shows "poly_add p [] = p" and "poly_add [] p = p" using poly_add_zero' normalize_polynomial polynomial_in_carrier assms by auto lemma poly_add_replicate_zero': assumes "set p ⊆ carrier R" shows "poly_add p (replicate n 𝟬) = normalize p" and "poly_add (replicate n 𝟬) p = normalize p" proof - have "poly_add p (replicate n 𝟬) = poly_add p []" using poly_add_normalize(2)[OF assms, of "replicate n 𝟬"] normalize_replicate_zero[of n "[]"] by force also have " ... = normalize p" using poly_add_zero'[OF assms] by simp finally show "poly_add p (replicate n 𝟬) = normalize p" . thus "poly_add (replicate n 𝟬) p = normalize p" using poly_add_comm[OF assms, of "replicate n 𝟬"] by force qed lemma poly_add_replicate_zero: assumes "subring K R" "polynomial K p" shows "poly_add p (replicate n 𝟬) = p" and "poly_add (replicate n 𝟬) p = p" using poly_add_replicate_zero' normalize_polynomial polynomial_in_carrier assms by auto subsection ‹Dense Representation› lemma dense_repr_replicate_zero: "dense_repr ((replicate n 𝟬) @ p) = dense_repr p" by (induction n) (auto) lemma dense_repr_normalize: "dense_repr (normalize p) = dense_repr p" by (induct p) (auto) lemma polynomial_dense_repr: assumes "polynomial K p" and "p ≠ []" shows "dense_repr p = (lead_coeff p, degree p) # dense_repr (normalize (tl p))" proof - let ?len = length and ?norm = normalize obtain a p' where p: "p = a # p'" using assms(2) list.exhaust_sel by blast hence a: "a ∈ K - { 𝟬 }" and p': "set p' ⊆ K" using assms(1) unfolding p by (auto simp add: polynomial_def) hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'" unfolding p by simp also have " ... = (lead_coeff p, degree p) # dense_repr ((replicate (?len p' - ?len (?norm p')) 𝟬) @ ?norm p')" using normalize_def' dense_repr_replicate_zero by simp also have " ... = (lead_coeff p, degree p) # dense_repr (?norm p')" using dense_repr_replicate_zero by simp finally show ?thesis unfolding p by simp qed lemma monom_decomp: assumes "subring K R" "polynomial K p" shows "p = poly_of_dense (dense_repr p)" using assms(2) proof (induct "length p" arbitrary: p rule: less_induct) case less thus ?case proof (cases p) case Nil thus ?thesis by simp next case (Cons a l) hence a: "a ∈ carrier R - { 𝟬 }" and l: "set l ⊆ carrier R" "set l ⊆ K" using less(2) subringE(1)[OF assms(1)] by (auto simp add: polynomial_def) hence "a # l = poly_add (monom a (degree (a # l))) l" using poly_add_monom[of l a] by simp also have " ... = poly_add (monom a (degree (a # l))) (normalize l)" using poly_add_normalize(2)[of "monom a (degree (a # l))", OF _ l(1)] a unfolding monom_def by force also have " ... = poly_add (monom a (degree (a # l))) (poly_of_dense (dense_repr (normalize l)))" using less(1)[OF _ normalize_gives_polynomial[OF l(2)]] normalize_length_le[of l] unfolding Cons by simp also have " ... = poly_of_dense ((a, degree (a # l)) # dense_repr (normalize l))" by simp also have " ... = poly_of_dense (dense_repr (a # l))" using polynomial_dense_repr[OF less(2)] unfolding Cons by simp finally show ?thesis unfolding Cons by simp qed qed subsection ‹Polynomial Multiplication› lemma poly_mult_is_polynomial: assumes "subring K R" "set p1 ⊆ K" and "set p2 ⊆ K" shows "polynomial K (poly_mult p1 p2)" using assms(2-3) proof (induction p1) case Nil thus ?case by (simp add: polynomial_def) next case (Cons a p1) let ?a_p2 = "(map (λb. a ⊗ b) p2) @ (replicate (degree (a # p1)) 𝟬)" have "set (poly_mult p1 p2) ⊆ K" using Cons unfolding polynomial_def by auto moreover have "set ?a_p2 ⊆ K" using assms(3) Cons(2) subringE(1-2,6)[OF assms(1)] by(induct p2) (auto) ultimately have "polynomial K (poly_add ?a_p2 (poly_mult p1 p2))" using poly_add_is_polynomial[OF assms(1)] by blast thus ?case by simp qed lemma poly_mult_closed: assumes "subring K R" shows "⟦ polynomial K p1; polynomial K p2 ⟧ ⟹ polynomial K (poly_mult p1 p2)" using poly_mult_is_polynomial polynomial_incl assms by simp lemma poly_mult_in_carrier: "⟦ set p1 ⊆ carrier R; set p2 ⊆ carrier R ⟧ ⟹ set (poly_mult p1 p2) ⊆ carrier R" using poly_mult_is_polynomial polynomial_in_carrier carrier_is_subring by simp lemma poly_mult_coeff: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "coeff (poly_mult p1 p2) = (λi. ⨁ k ∈ {..i}. (coeff p1) k ⊗ (coeff p2) (i - k))" using assms(1) proof (induction p1) case Nil thus ?case using assms(2) by auto next case (Cons a p1) hence in_carrier: "a ∈ carrier R" "⋀i. (coeff p1) i ∈ carrier R" "⋀i. (coeff p2) i ∈ carrier R" using coeff_in_carrier assms(2) by auto let ?a_p2 = "(map (λb. a ⊗ b) p2) @ (replicate (degree (a # p1)) 𝟬)" have "coeff (replicate (degree (a # p1)) 𝟬) = (λ_. 𝟬)" and "length (replicate (degree (a # p1)) 𝟬) = length p1" using prefix_replicate_zero_coeff[of "[]" "length p1"] by auto hence "coeff ?a_p2 = (λi. if i < length p1 then 𝟬 else (coeff (map (λb. a ⊗ b) p2)) (i - length p1))" using append_coeff[of "map (λb. a ⊗ b) p2" "replicate (length p1) 𝟬"] by auto also have " ... = (λi. if i < length p1 then 𝟬 else a ⊗ ((coeff p2) (i - length p1)))" proof - have "⋀i. i < length p2 ⟹ (coeff (map (λb. a ⊗ b) p2)) i = a ⊗ ((coeff p2) i)" proof - fix i assume i_lt: "i < length p2" hence "(coeff (map (λb. a ⊗ b) p2)) i = (map (λb. a ⊗ b) p2) ! (length p2 - 1 - i)" using coeff_nth[of i "map (λb. a ⊗ b) p2"] by auto also have " ... = a ⊗ (p2 ! (length p2 - 1 - i))" using i_lt by auto also have " ... = a ⊗ ((coeff p2) i)" using coeff_nth[OF i_lt] by simp finally show "(coeff (map (λb. a ⊗ b) p2)) i = a ⊗ ((coeff p2) i)" . qed moreover have "⋀i. i ≥ length p2 ⟹ (coeff (map (λb. a ⊗ b) p2)) i = a ⊗ ((coeff p2) i)" using coeff_length[of p2] coeff_length[of "map (λb. a ⊗ b) p2"] in_carrier by auto ultimately show ?thesis by (meson not_le) qed also have " ... = (λi. ⨁ k ∈ {..i}. (if k = length p1 then a else 𝟬) ⊗ (coeff p2) (i - k))" (is "?f1 = (λi. (⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k)))") proof fix i have "⋀k. k ∈ {..i} ⟹ ?f2 k ⊗ ?f3 (i - k) = 𝟬" if "i < length p1" using in_carrier that by auto hence "(⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k)) = 𝟬" if "i < length p1" using that in_carrier add.finprod_cong'[of "{..i}" "{..i}" "λk. ?f2 k ⊗ ?f3 (i - k)" "λi. 𝟬"] by auto hence eq_lt: "?f1 i = (λi. (⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k))) i" if "i < length p1" using that by auto have "⋀k. k ∈ {..i} ⟹ ?f2 k ⊗⇘R⇙ ?f3 (i - k) = (if length p1 = k then a ⊗ coeff p2 (i - k) else 𝟬)" using in_carrier by auto hence "(⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k)) = (⨁ k ∈ {..i}. (if length p1 = k then a ⊗ coeff p2 (i - k) else 𝟬))" using in_carrier add.finprod_cong'[of "{..i}" "{..i}" "λk. ?f2 k ⊗ ?f3 (i - k)" "λk. (if length p1 = k then a ⊗ coeff p2 (i - k) else 𝟬)"] by fastforce also have " ... = a ⊗ (coeff p2) (i - length p1)" if "i ≥ length p1" using add.finprod_singleton[of "length p1" "{..i}" "λj. a ⊗ (coeff p2) (i - j)"] in_carrier that by auto finally have "(⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k)) = a ⊗ (coeff p2) (i - length p1)" if "i ≥ length p1" using that by simp hence eq_ge: "?f1 i = (λi. (⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k))) i" if "i ≥ length p1" using that by auto from eq_lt eq_ge show "?f1 i = (λi. (⨁ k ∈ {..i}. ?f2 k ⊗ ?f3 (i - k))) i" by auto qed finally have coeff_a_p2: "coeff ?a_p2 = (λi. ⨁ k ∈ {..i}. (if k = length p1 then a else 𝟬) ⊗ (coeff p2) (i - k))" . have "set ?a_p2 ⊆ carrier R" using in_carrier(1) assms(2) by auto moreover have "set (poly_mult p1 p2) ⊆ carrier R" using poly_mult_in_carrier[OF _ assms(2)] Cons(2) by simp ultimately have "coeff (poly_mult (a # p1) p2) = (λi. ((coeff ?a_p2) i) ⊕ ((coeff (poly_mult p1 p2)) i))" using poly_add_coeff[of ?a_p2 "poly_mult p1 p2"] by simp also have " ... = (λi. (⨁ k ∈ {..i}. (if k = length p1 then a else 𝟬) ⊗ (coeff p2) (i - k)) ⊕ (⨁ k ∈ {..i}. (coeff p1) k ⊗ (coeff p2) (i - k)))" using Cons coeff_a_p2 by simp also have " ... = (λi. (⨁ k ∈ {..i}. ((if k = length p1 then a else 𝟬) ⊗ (coeff p2) (i - k)) ⊕ ((coeff p1) k ⊗ (coeff p2) (i - k))))" using add.finprod_multf in_carrier by auto also have " ... = (λi. (⨁ k ∈ {..i}. (coeff (a # p1) k) ⊗ (coeff p2) (i - k)))" (is "(λi. (⨁ k ∈ {..i}. ?f i k)) = (λi. (⨁ k ∈ {..i}. ?g i k))") proof fix i have "⋀k. ?f i k = ?g i k" using in_carrier coeff_length[of p1] by auto thus "(⨁ k ∈ {..i}. ?f i k) = (⨁ k ∈ {..i}. ?g i k)" by simp qed finally show ?case . qed lemma poly_mult_zero: assumes "set p ⊆ carrier R" shows "poly_mult [] p = []" and "poly_mult p [] = []" proof (simp) have "coeff (poly_mult p []) = (λ_. 𝟬)" using poly_mult_coeff[OF assms, of "[]"] coeff_in_carrier[OF assms] by auto thus "poly_mult p [] = []" using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF carrier_is_subring assms] zero_is_polynomial] by simp qed lemma poly_mult_l_distr': assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" "set p3 ⊆ carrier R" shows "poly_mult (poly_add p1 p2) p3 = poly_add (poly_mult p1 p3) (poly_mult p2 p3)" proof - let ?c1 = "coeff p1" and ?c2 = "coeff p2" and ?c3 = "coeff p3" have in_carrier: "⋀i. ?c1 i ∈ carrier R" "⋀i. ?c2 i ∈ carrier R" "⋀i. ?c3 i ∈ carrier R" using assms coeff_in_carrier by auto have "coeff (poly_mult (poly_add p1 p2) p3) = (λn. ⨁i ∈ {..n}. (?c1 i ⊕ ?c2 i) ⊗ ?c3 (n - i))" using poly_mult_coeff[of "poly_add p1 p2" p3] poly_add_coeff[OF assms(1-2)] poly_add_in_carrier[OF assms(1-2)] assms by auto also have " ... = (λn. ⨁i ∈ {..n}. (?c1 i ⊗ ?c3 (n - i)) ⊕ (?c2 i ⊗ ?c3 (n - i)))" using in_carrier l_distr by auto also have " ... = (λn. (⨁i ∈ {..n}. (?c1 i ⊗ ?c3 (n - i))) ⊕ (⨁i ∈ {..n}. (?c2 i ⊗ ?c3 (n - i))))" using add.finprod_multf in_carrier by auto also have " ... = coeff (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" using poly_mult_coeff[OF assms(1) assms(3)] poly_mult_coeff[OF assms(2-3)] poly_add_coeff[OF poly_mult_in_carrier[OF assms(1) assms(3)]] poly_mult_in_carrier[OF assms(2-3)] by simp finally have "coeff (poly_mult (poly_add p1 p2) p3) = coeff (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" . moreover have "polynomial (carrier R) (poly_mult (poly_add p1 p2) p3)" and "polynomial (carrier R) (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier carrier_is_subring by auto ultimately show ?thesis using coeff_iff_polynomial_cond by auto qed lemma poly_mult_l_distr: assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K p3" shows "poly_mult (poly_add p1 p2) p3 = poly_add (poly_mult p1 p3) (poly_mult p2 p3)" using poly_mult_l_distr' polynomial_in_carrier assms by auto lemma poly_mult_prepend_replicate_zero: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_mult p1 p2 = poly_mult ((replicate n 𝟬) @ p1) p2" proof - { fix p1 p2 assume A: "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" hence "poly_mult p1 p2 = poly_mult (𝟬 # p1) p2" proof - let ?a_p2 = "(map ((⊗) 𝟬) p2) @ (replicate (length p1) 𝟬)" have "?a_p2 = replicate (length p2 + length p1) 𝟬" using A(2) by (induction p2) (auto) hence "poly_mult (𝟬 # p1) p2 = poly_add (replicate (length p2 + length p1) 𝟬) (poly_mult p1 p2)" by simp also have " ... = poly_add (normalize (replicate (length p2 + length p1) 𝟬)) (poly_mult p1 p2)" using poly_add_normalize(1)[of "replicate (length p2 + length p1) 𝟬" "poly_mult p1 p2"] poly_mult_in_carrier[OF A] by force also have " ... = poly_mult p1 p2" using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp finally show ?thesis by auto qed } note aux_lemma = this from assms show ?thesis proof (induction n) case 0 thus ?case by simp next case (Suc n) thus ?case using aux_lemma[of "replicate n 𝟬 @ p1" p2] by force qed qed lemma poly_mult_normalize: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_mult p1 p2 = poly_mult (normalize p1) p2" proof - let ?replicate = "replicate (length p1 - length (normalize p1)) 𝟬" have "poly_mult p1 p2 = poly_mult (?replicate @ (normalize p1)) p2" using normalize_def'[of p1] by simp thus ?thesis using poly_mult_prepend_replicate_zero normalize_in_carrier assms by auto qed lemma poly_mult_append_zero: assumes "set p ⊆ carrier R" "set q ⊆ carrier R" shows "poly_mult (p @ [ 𝟬 ]) q = normalize ((poly_mult p q) @ [ 𝟬 ])" using assms(1) proof (induct p) case Nil thus ?case using poly_mult_normalize[OF _ assms(2), of "[] @ [ 𝟬 ]"] poly_mult_zero(1) poly_mult_zero(1)[of "q @ [ 𝟬 ]"] assms(2) by auto next case (Cons a p) let ?q_a = "λn. (map ((⊗) a) q) @ (replicate n 𝟬)" have set_q_a: "⋀n. set (?q_a n) ⊆ carrier R" using Cons(2) assms(2) by (induct q) (auto) have set_poly_mult: "set ((poly_mult p q) @ [ 𝟬 ]) ⊆ carrier R" using poly_mult_in_carrier[OF _ assms(2)] Cons(2) by auto have "poly_mult ((a # p) @ [𝟬]) q = poly_add (?q_a (Suc (length p))) (poly_mult (p @ [𝟬]) q)" by auto also have " ... = poly_add (?q_a (Suc (length p))) (normalize ((poly_mult p q) @ [ 𝟬 ]))" using Cons by simp also have " ... = poly_add ((?q_a (length p)) @ [ 𝟬 ]) ((poly_mult p q) @ [ 𝟬 ])" using poly_add_normalize(2)[OF set_q_a[of "Suc (length p)"] set_poly_mult] by (simp add: replicate_append_same) also have " ... = normalize ((poly_add (?q_a (length p)) (poly_mult p q)) @ [ 𝟬 ])" using poly_add_append_zero[OF set_q_a[of "length p"] poly_mult_in_carrier[OF _ assms(2)]] Cons(2) by auto also have " ... = normalize ((poly_mult (a # p) q) @ [ 𝟬 ])" by auto finally show ?case . qed end (* of ring context. *) subsection ‹Properties Within a Domain› context domain begin lemma one_is_polynomial [intro]: "subring K R ⟹ polynomial K [ 𝟭 ]" unfolding polynomial_def using subringE(3) by auto lemma poly_mult_comm: assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" shows "poly_mult p1 p2 = poly_mult p2 p1" proof - let ?c1 = "coeff p1" and ?c2 = "coeff p2" have "⋀i. (⨁k ∈ {..i}. ?c1 k ⊗ ?c2 (i - k)) = (⨁k ∈ {..i}. ?c2 k ⊗ ?c1 (i - k))" proof - fix i :: nat let ?f = "λk. ?c1 k ⊗ ?c2 (i - k)" have in_carrier: "⋀i. ?c1 i ∈ carrier R" "⋀i. ?c2 i ∈ carrier R" using coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] by auto have reindex_inj: "inj_on (λk. i - k) {..i}" using inj_on_def by force moreover have "(λk. i - k) ` {..i} ⊆ {..i}" by auto hence "(λk. i - k) ` {..i} = {..i}" using reindex_inj endo_inj_surj[of "{..i}" "λk. i - k"] by simp ultimately have "(⨁k ∈ {..i}. ?f k) = (⨁k ∈ {..i}. ?f (i - k))" using add.finprod_reindex[of ?f "λk. i - k" "{..i}"] in_carrier by auto moreover have "⋀k. k ∈ {..i} ⟹ ?f (i - k) = ?c2 k ⊗ ?c1 (i - k)" using in_carrier m_comm by auto hence "(⨁k ∈ {..i}. ?f (i - k)) = (⨁k ∈ {..i}. ?c2 k ⊗ ?c1 (i - k))" using add.finprod_cong'[of "{..i}" "{..i}"] in_carrier by auto ultimately show "(⨁k ∈ {..i}. ?f k) = (⨁k ∈ {..i}. ?c2 k ⊗ ?c1 (i - k))" by simp qed hence "coeff (poly_mult p1 p2) = coeff (poly_mult p2 p1)" using poly_mult_coeff[OF assms] poly_mult_coeff[OF assms(2,1)] by simp thus ?thesis using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF _ assms] poly_mult_is_polynomial[OF _ assms(2,1)]] carrier_is_subring by simp qed lemma poly_mult_r_distr': assumes "set p1 ⊆ carrier R" "set p2 ⊆ carrier R" "set p3 ⊆ carrier R" shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)" unfolding poly_mult_comm[OF assms(1) poly_add_in_carrier[OF assms(2-3)]] poly_mult_l_distr'[OF assms(2-3,1)] assms(2-3)[THEN poly_mult_comm[OF _ assms(1)]] .. lemma poly_mult_r_distr: assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K p3" shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)" using poly_mult_r_distr' polynomial_in_carrier assms by auto lemma poly_mult_replicate_zero: assumes "set p ⊆ carrier R" shows "poly_mult (replicate n 𝟬) p = []" and "poly_mult p (replicate n 𝟬) = []" proof - have in_carrier: "⋀n. set (replicate n 𝟬) ⊆ carrier R" by auto show "poly_mult (replicate n 𝟬) p = []" using assms proof (induction n) case 0 thus ?case by simp next case (Suc n) hence "poly_mult (replicate (Suc n) 𝟬) p = poly_mult (𝟬 # (replicate n 𝟬)) p" by simp also have " ... = poly_add ((map (λa. 𝟬 ⊗ a) p) @ (replicate n 𝟬)) []" using Suc by simp also have " ... = poly_add ((map (λa. 𝟬) p) @ (replicate n 𝟬)) []" proof - have "map ((⊗) 𝟬) p = map (λa. 𝟬) p" using Suc.prems by auto then show ?thesis by presburger qed also have " ... = poly_add (replicate (length p + n) 𝟬) []" by (simp add: map_replicate_const replicate_add) also have " ... = poly_add [] []" using poly_add_normalize(1)[of "replicate (length p + n) 𝟬" "[]"] normalize_replicate_zero[of "length p + n" "[]"] by auto also have " ... = []" by simp finally show ?case . qed thus "poly_mult p (replicate n 𝟬) = []" using poly_mult_comm[OF assms in_carrier] by simp qed lemma poly_mult_const': assumes "set p ⊆ carrier R" "a ∈ carrier R" shows "poly_mult [ a ] p = normalize (map (λb. a ⊗ b) p)" and "poly_mult p [ a ] = normalize (map (λb. a ⊗ b) p)" proof - have "map2 (⊕) (map ((⊗) a) p) (replicate (length p) 𝟬) = map ((⊗) a) p" using assms by (induction p) (auto) thus "poly_mult [ a ] p = normalize (map (λb. a ⊗ b) p)" by simp thus "poly_mult p [ a ] = normalize (map (λb. a ⊗ b) p)" using poly_mult_comm[OF assms(1), of "[ a ]"] assms(2) by auto qed lemma poly_mult_const: assumes "subring K R" "polynomial K p" "a ∈ K - { 𝟬 }" shows "poly_mult [ a ] p = map (λb. a ⊗ b) p" and "poly_mult p [ a ] = map (λb. a ⊗ b) p" proof - have in_carrier: "set p ⊆ carrier R" "a ∈ carrier R" using polynomial_in_carrier[OF assms(1-2)] assms(3) subringE(1)[OF assms(1)] by auto show "poly_mult [ a ] p = map (λb. a ⊗ b) p" proof (cases p) case Nil thus ?thesis using poly_mult_const'(1) in_carrier by auto next case (Cons b q) have "lead_coeff (map (λb. a ⊗ b) p) ≠ 𝟬" using assms subringE(1)[OF assms(1)] integral[of a b] Cons lead_coeff_in_carrier by auto hence "normalize (map (λb. a ⊗ b) p) = (map (λb. a ⊗ b) p)" unfolding Cons by simp thus ?thesis using poly_mult_const'(1) in_carrier by auto qed thus "poly_mult p [ a ] = map (λb. a ⊗ b) p" using poly_mult_comm[OF in_carrier(1)] in_carrier(2) by auto qed lemma poly_mult_semiassoc: assumes "set p ⊆ carrier R" "set q ⊆ carrier R" and "a ∈ carrier R" shows "poly_mult (poly_mult [ a ] p) q = poly_mult [ a ] (poly_mult p q)" proof - let ?cp = "coeff p" and ?cq = "coeff q" have "coeff (poly_mult [ a ] p) = (λi. (a ⊗ ?cp i))" using poly_mult_const'(1)[OF assms(1,3)] normalize_coeff scalar_coeff[OF assms(3)] by simp hence "coeff (poly_mult (poly_mult [ a ] p) q) = (λi. (⨁j ∈ {..i}. (a ⊗ ?cp j) ⊗ ?cq (i - j)))" using poly_mult_coeff[OF poly_mult_in_carrier[OF _ assms(1)] assms(2), of "[ a ]"] assms(3) by auto also have " ... = (λi. a ⊗ (⨁j ∈ {..i}. ?cp j ⊗ ?cq (i - j)))" proof fix i show "(⨁j ∈ {..i}. (a ⊗ ?cp j) ⊗ ?cq (i - j)) = a ⊗ (⨁j ∈ {..i}. ?cp j ⊗ ?cq (i - j))" using finsum_rdistr[OF _ assms(3), of _ "λj. ?cp j ⊗ ?cq (i - j)"] assms(1-2)[THEN coeff_in_carrier] by (simp add: assms(3) m_assoc) qed also have " ... = coeff (poly_mult [ a ] (poly_mult p q))" unfolding poly_mult_const'(1)[OF poly_mult_in_carrier[OF assms(1-2)] assms(3)] using scalar_coeff[OF assms(3), of "poly_mult p q"] poly_mult_coeff[OF assms(1-2)] normalize_coeff by simp finally have "coeff (poly_mult (poly_mult [ a ] p) q) = coeff (poly_mult [ a ] (poly_mult p q))" . moreover have "polynomial (carrier R) (poly_mult (poly_mult [ a ] p) q)" and "polynomial (carrier R) (poly_mult [ a ] (poly_mult p q))" using poly_mult_is_polynomial[OF _ poly_mult_in_carrier[OF _ assms(1)] assms(2)] poly_mult_is_polynomial[OF _ _ poly_mult_in_carrier[OF assms(1-2)]] carrier_is_subring assms(3) by (auto simp del: poly_mult.simps) ultimately show ?thesis using coeff_iff_polynomial_cond by simp qed text ‹Note that "polynomial (carrier R) p" and "subring K p; polynomial K p" are "equivalent" assumptions for any lemma in ring which the result doesn't depend on K, because carrier is a subring and a polynomial for a subset of the carrier is a carrier polynomial. The decision between one of them should be based on how the lemma is going to be used and proved. These are some tips: (a) Lemmas about the algebraic structure of polynomials should use the latter option. (b) Also, if the lemma deals with lots of polynomials, then the latter option is preferred. (c) If the proof is going to be much easier with the first option, do not hesitate. › lemma poly_mult_monom': assumes "set p ⊆ carrier R" "a ∈ carrier R" shows "poly_mult (monom a n) p = normalize ((map ((⊗) a) p) @ (replicate n 𝟬))" proof - have set_map: "set ((map ((⊗) a) p) @ (replicate n 𝟬)) ⊆ carrier R" using assms by (induct p) (auto) show ?thesis using poly_mult_replicate_zero(1)[OF assms(1), of n] poly_add_zero'(1)[OF set_map] unfolding monom_def by simp qed lemma poly_mult_monom: assumes "polynomial (carrier R) p" "a ∈ carrier R - { 𝟬 }" shows "poly_mult (monom a n) p = (if p = [] then [] else (poly_mult [ a ] p) @ (replicate n 𝟬))" proof (cases p) case Nil thus ?thesis using poly_mult_zero(2)[of "monom a n"] assms(2) monom_def by fastforce next case (Cons b ps) hence "lead_coeff ((map (λb. a ⊗ b) p) @ (replicate n 𝟬)) ≠ 𝟬" using Cons assms integral[of a b] unfolding polynomial_def by auto thus ?thesis using poly_mult_monom'[OF polynomial_incl[OF assms(1)], of a n] assms(2) Cons unfolding poly_mult_const(1)[OF carrier_is_subring assms] by simp qed lemma poly_mult_one': assumes "set p ⊆ carrier R" shows "poly_mult [ 𝟭 ] p = normalize p" and "poly_mult p [ 𝟭 ] = normalize p" proof - have "map2 (⊕) (map ((⊗) 𝟭) p) (replicate (length p) 𝟬) = p" using assms by (induct p) (auto) thus "poly_mult [ 𝟭 ] p = normalize p" and "poly_mult p [ 𝟭 ] = normalize p" using poly_mult_comm[OF assms, of "[ 𝟭 ]"] by auto qed lemma poly_mult_one: assumes "subring K R" "polynomial K p" shows "poly_mult [ 𝟭 ] p = p" and "poly_mult p [ 𝟭 ] = p" using poly_mult_one'[OF polynomial_in_carrier[OF assms]] normalize_polynomial[OF assms(2)] by auto lemma poly_mult_lead_coeff_aux: assumes "subring K R" "polynomial K p1" "polynomial K p2" and "p1 ≠ []" and "p2 ≠ []" shows "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = (lead_coeff p1) ⊗ (lead_coeff p2)" proof - have p1: "lead_coeff p1 ∈ carrier R - { 𝟬 }" and p2: "lead_coeff p2 ∈ carrier R - { 𝟬 }" using assms(2-5) lead_coeff_in_carrier[OF assms(1)] by (metis list.collapse)+ have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = (⨁ k ∈ {..((degree p1) + (degree p2))}. (coeff p1) k ⊗ (coeff p2) ((degree p1) + (degree p2) - k))" using poly_mult_coeff[OF assms(2-3)[THEN polynomial_in_carrier[OF assms(1)]]] by simp also have " ... = (lead_coeff p1) ⊗ (lead_coeff p2)" proof - let ?f = "λi. (coeff p1) i ⊗ (coeff p2) ((degree p1) + (degree p2) - i)