src/HOL/Library/Polynomial.thy
 changeset 62065 1546a042e87b parent 61945 1135b8de26c3 child 62067 0fd850943901
equal inserted replaced
62060:b75764fc4c35 62065:1546a042e87b
`   279   by (induct n) simp_all`
`   279   by (induct n) simp_all`
`   280 `
`   280 `
`   281 lemma Poly_eq_0:`
`   281 lemma Poly_eq_0:`
`   282   "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"`
`   282   "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"`
`   283   by (induct as) (auto simp add: Cons_replicate_eq)`
`   283   by (induct as) (auto simp add: Cons_replicate_eq)`
`   284 `
`   284   `
`       `
`   285 lemma degree_Poly: "degree (Poly xs) \<le> length xs"`
`       `
`   286   by (induction xs) simp_all`
`       `
`   287   `
`   285 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"`
`   288 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"`
`   286 where`
`   289 where`
`   287   "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"`
`   290   "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"`
`   288 `
`   291 `
`   289 lemma coeffs_eq_Nil [simp]:`
`   292 lemma coeffs_eq_Nil [simp]:`
`   309   note * = this`
`   312   note * = this`
`   310   show ?thesis`
`   313   show ?thesis`
`   311     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)`
`   314     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)`
`   312 qed`
`   315 qed`
`   313 `
`   316 `
`       `
`   317 lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"`
`       `
`   318   by (simp add: coeffs_def)`
`       `
`   319   `
`       `
`   320 lemma coeffs_nth:`
`       `
`   321   assumes "p \<noteq> 0" "n \<le> degree p"`
`       `
`   322   shows   "coeffs p ! n = coeff p n"`
`       `
`   323   using assms unfolding coeffs_def by (auto simp del: upt_Suc)`
`       `
`   324 `
`   314 lemma not_0_cCons_eq [simp]:`
`   325 lemma not_0_cCons_eq [simp]:`
`   315   "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"`
`   326   "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"`
`   316   by (simp add: cCons_def)`
`   327   by (simp add: cCons_def)`
`   317 `
`   328 `
`   318 lemma Poly_coeffs [simp, code abstype]:`
`   329 lemma Poly_coeffs [simp, code abstype]:`
`   448 `
`   459 `
`   449 lemma poly_pCons [simp]:`
`   460 lemma poly_pCons [simp]:`
`   450   "poly (pCons a p) x = a + x * poly p x"`
`   461   "poly (pCons a p) x = a + x * poly p x"`
`   451   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)`
`   462   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)`
`   452 `
`   463 `
`       `
`   464 lemma poly_altdef: `
`       `
`   465   "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"`
`       `
`   466 proof (induction p rule: pCons_induct)`
`       `
`   467   case (pCons a p)`
`       `
`   468     show ?case`
`       `
`   469     proof (cases "p = 0")`
`       `
`   470       case False`
`       `
`   471       let ?p' = "pCons a p"`
`       `
`   472       note poly_pCons[of a p x]`
`       `
`   473       also note pCons.IH`
`       `
`   474       also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =`
`       `
`   475                  coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"`
`       `
`   476           by (simp add: field_simps setsum_right_distrib coeff_pCons)`
`       `
`   477       also note setsum_atMost_Suc_shift[symmetric]`
`       `
`   478       also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]`
`       `
`   479       finally show ?thesis .`
`       `
`   480    qed simp`
`       `
`   481 qed simp`
`       `
`   482 `
`   453 `
`   483 `
`   454 subsection \<open>Monomials\<close>`
`   484 subsection \<open>Monomials\<close>`
`   455 `
`   485 `
`   456 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"`
`   486 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"`
`   457   is "\<lambda>a m n. if m = n then a else 0"`
`   487   is "\<lambda>a m n. if m = n then a else 0"`
`   498   fixes a x :: "'a::{comm_semiring_1}"`
`   528   fixes a x :: "'a::{comm_semiring_1}"`
`   499   shows "poly (monom a n) x = a * x ^ n"`
`   529   shows "poly (monom a n) x = a * x ^ n"`
`   500   by (cases "a = 0", simp_all)`
`   530   by (cases "a = 0", simp_all)`
`   501     (induct n, simp_all add: mult.left_commute poly_def)`
`   531     (induct n, simp_all add: mult.left_commute poly_def)`
`   502 `
`   532 `
`   503 `
`   533     `
`   504 subsection \<open>Addition and subtraction\<close>`
`   534 subsection \<open>Addition and subtraction\<close>`
`   505 `
`   535 `
`   506 instantiation poly :: (comm_monoid_add) comm_monoid_add`
`   536 instantiation poly :: (comm_monoid_add) comm_monoid_add`
`   507 begin`
`   537 begin`
`   508 `
`   538 `
`   712   using poly_add [of p "- q" x] by simp`
`   742   using poly_add [of p "- q" x] by simp`
`   713 `
`   743 `
`   714 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"`
`   744 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"`
`   715   by (induct A rule: infinite_finite_induct) simp_all`
`   745   by (induct A rule: infinite_finite_induct) simp_all`
`   716 `
`   746 `
`       `
`   747 lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"`
`       `
`   748   by (induction xs) (simp_all add: monom_0 monom_Suc)`
`       `
`   749 `
`   717 `
`   750 `
`   718 subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>`
`   751 subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>`
`   719 `
`   752 `
`   720 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"`
`   753 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"`
`   721   is "\<lambda>a p n. a * coeff p n"`
`   754   is "\<lambda>a p n. a * coeff p n"`
`   922 lemma poly_power [simp]:`
`   955 lemma poly_power [simp]:`
`   923   fixes p :: "'a::{comm_semiring_1} poly"`
`   956   fixes p :: "'a::{comm_semiring_1} poly"`
`   924   shows "poly (p ^ n) x = poly p x ^ n"`
`   957   shows "poly (p ^ n) x = poly p x ^ n"`
`   925   by (induct n) simp_all`
`   958   by (induct n) simp_all`
`   926 `
`   959 `
`       `
`   960   `
`       `
`   961 subsection \<open>Conversions from natural numbers\<close>`
`       `
`   962 `
`       `
`   963 lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"`
`       `
`   964 proof (induction n)`
`       `
`   965   case (Suc n)`
`       `
`   966   hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" `
`       `
`   967     by simp`
`       `
`   968   also have "(of_nat n :: 'a poly) = [: of_nat n :]" `
`       `
`   969     by (subst Suc) (rule refl)`
`       `
`   970   also have "1 = [:1:]" by (simp add: one_poly_def)`
`       `
`   971   finally show ?case by (subst (asm) add_pCons) simp`
`       `
`   972 qed simp`
`       `
`   973 `
`       `
`   974 lemma degree_of_nat [simp]: "degree (of_nat n) = 0"`
`       `
`   975   by (simp add: of_nat_poly)`
`       `
`   976 `
`       `
`   977 lemma degree_numeral [simp]: "degree (numeral n) = 0"`
`       `
`   978   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp`
`       `
`   979 `
`       `
`   980 lemma numeral_poly: "numeral n = [:numeral n:]"`
`       `
`   981   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp`
`   927 `
`   982 `
`   928 subsection \<open>Lemmas about divisibility\<close>`
`   983 subsection \<open>Lemmas about divisibility\<close>`
`   929 `
`   984 `
`   930 lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"`
`   985 lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"`
`   931 proof -`
`   986 proof -`
`  1785 apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)`
`  1840 apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)`
`  1786 unfolding poly_eq_0_iff_dvd`
`  1841 unfolding poly_eq_0_iff_dvd`
`  1787 apply (metis dvd_power dvd_trans order_1)`
`  1842 apply (metis dvd_power dvd_trans order_1)`
`  1788 done`
`  1843 done`
`  1789 `
`  1844 `
`       `
`  1845 lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"`
`       `
`  1846   by (subst (asm) order_root) auto`
`       `
`  1847 `
`  1790 `
`  1848 `
`  1791 subsection \<open>GCD of polynomials\<close>`
`  1849 subsection \<open>GCD of polynomials\<close>`
`  1792 `
`  1850 `
`  1793 instantiation poly :: (field) gcd`
`  1851 instantiation poly :: (field) gcd`
`  1794 begin`
`  1852 begin`
`  1917 lemma poly_gcd_code [code]:`
`  1975 lemma poly_gcd_code [code]:`
`  1918   "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"`
`  1976   "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"`
`  1919   by (simp add: gcd_poly.simps)`
`  1977   by (simp add: gcd_poly.simps)`
`  1920 `
`  1978 `
`  1921 `
`  1979 `
`       `
`  1980 subsection \<open>Additional induction rules on polynomials\<close>`
`       `
`  1981 `
`       `
`  1982 text \<open>`
`       `
`  1983   An induction rule for induction over the roots of a polynomial with a certain property. `
`       `
`  1984   (e.g. all positive roots)`
`       `
`  1985 \<close>`
`       `
`  1986 lemma poly_root_induct [case_names 0 no_roots root]:`
`       `
`  1987   fixes p :: "'a :: idom poly"`
`       `
`  1988   assumes "Q 0"`
`       `
`  1989   assumes "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"`
`       `
`  1990   assumes "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"`
`       `
`  1991   shows   "Q p"`
`       `
`  1992 proof (induction "degree p" arbitrary: p rule: less_induct)`
`       `
`  1993   case (less p)`
`       `
`  1994   show ?case`
`       `
`  1995   proof (cases "p = 0")`
`       `
`  1996     assume nz: "p \<noteq> 0"`
`       `
`  1997     show ?case`
`       `
`  1998     proof (cases "\<exists>a. P a \<and> poly p a = 0")`
`       `
`  1999       case False`
`       `
`  2000       thus ?thesis by (intro assms(2)) blast`
`       `
`  2001     next`
`       `
`  2002       case True`
`       `
`  2003       then obtain a where a: "P a" "poly p a = 0" `
`       `
`  2004         by blast`
`       `
`  2005       hence "-[:-a, 1:] dvd p" `
`       `
`  2006         by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)`
`       `
`  2007       then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp`
`       `
`  2008       with nz have q_nz: "q \<noteq> 0" by auto`
`       `
`  2009       have "degree p = Suc (degree q)"`
`       `
`  2010         by (subst q, subst degree_mult_eq) (simp_all add: q_nz)`
`       `
`  2011       hence "Q q" by (intro less) simp`
`       `
`  2012       from a(1) and this have "Q ([:a, -1:] * q)" `
`       `
`  2013         by (rule assms(3))`
`       `
`  2014       with q show ?thesis by simp`
`       `
`  2015     qed`
`       `
`  2016   qed (simp add: assms(1))`
`       `
`  2017 qed`
`       `
`  2018 `
`       `
`  2019 lemma dropWhile_replicate_append: `
`       `
`  2020   "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys"`
`       `
`  2021   by (induction n) simp_all`
`       `
`  2022 `
`       `
`  2023 lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"`
`       `
`  2024   by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)`
`       `
`  2025 `
`       `
`  2026 text \<open>`
`       `
`  2027   An induction rule for simultaneous induction over two polynomials, `
`       `
`  2028   prepending one coefficient in each step.`
`       `
`  2029 \<close>`
`       `
`  2030 lemma poly_induct2 [case_names 0 pCons]:`
`       `
`  2031   assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"`
`       `
`  2032   shows   "P p q"`
`       `
`  2033 proof -`
`       `
`  2034   def n \<equiv> "max (length (coeffs p)) (length (coeffs q))"`
`       `
`  2035   def xs \<equiv> "coeffs p @ (replicate (n - length (coeffs p)) 0)"`
`       `
`  2036   def ys \<equiv> "coeffs q @ (replicate (n - length (coeffs q)) 0)"`
`       `
`  2037   have "length xs = length ys" `
`       `
`  2038     by (simp add: xs_def ys_def n_def)`
`       `
`  2039   hence "P (Poly xs) (Poly ys)" `
`       `
`  2040     by (induction rule: list_induct2) (simp_all add: assms)`
`       `
`  2041   also have "Poly xs = p" `
`       `
`  2042     by (simp add: xs_def Poly_append_replicate_0)`
`       `
`  2043   also have "Poly ys = q" `
`       `
`  2044     by (simp add: ys_def Poly_append_replicate_0)`
`       `
`  2045   finally show ?thesis .`
`       `
`  2046 qed`
`       `
`  2047 `
`       `
`  2048 `
`  1922 subsection \<open>Composition of polynomials\<close>`
`  2049 subsection \<open>Composition of polynomials\<close>`
`  1923 `
`  2050 `
`  1924 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"`
`  2051 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"`
`  1925 where`
`  2052 where`
`  1926   "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"`
`  2053   "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"`
`  1943 apply (simp add: pcompose_pCons, clarify)`
`  2070 apply (simp add: pcompose_pCons, clarify)`
`  1944 apply (rule degree_add_le, simp)`
`  2071 apply (rule degree_add_le, simp)`
`  1945 apply (rule order_trans [OF degree_mult_le], simp)`
`  2072 apply (rule order_trans [OF degree_mult_le], simp)`
`  1946 done`
`  2073 done`
`  1947 `
`  2074 `
`       `
`  2075 lemma pcompose_add:`
`       `
`  2076   fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly"`
`       `
`  2077   shows "pcompose (p + q) r = pcompose p r + pcompose q r"`
`       `
`  2078 proof (induction p q rule: poly_induct2)`
`       `
`  2079   case (pCons a p b q)`
`       `
`  2080   have "pcompose (pCons a p + pCons b q) r = `
`       `
`  2081           [:a + b:] + r * pcompose p r + r * pcompose q r"`
`       `
`  2082     by (simp_all add: pcompose_pCons pCons.IH algebra_simps)`
`       `
`  2083   also have "[:a + b:] = [:a:] + [:b:]" by simp`
`       `
`  2084   also have "\<dots> + r * pcompose p r + r * pcompose q r = `
`       `
`  2085                  pcompose (pCons a p) r + pcompose (pCons b q) r"`
`       `
`  2086     by (simp only: pcompose_pCons add_ac)`
`       `
`  2087   finally show ?case .`
`       `
`  2088 qed simp`
`       `
`  2089 `
`       `
`  2090 lemma pcompose_minus:`
`       `
`  2091   fixes p r :: "'a :: comm_ring poly"`
`       `
`  2092   shows "pcompose (-p) r = -pcompose p r"`
`       `
`  2093   by (induction p) (simp_all add: pcompose_pCons)`
`       `
`  2094 `
`       `
`  2095 lemma pcompose_diff:`
`       `
`  2096   fixes p q r :: "'a :: comm_ring poly"`
`       `
`  2097   shows "pcompose (p - q) r = pcompose p r - pcompose q r"`
`       `
`  2098   using pcompose_add[of p "-q"] by (simp add: pcompose_minus)`
`       `
`  2099 `
`       `
`  2100 lemma pcompose_smult:`
`       `
`  2101   fixes p r :: "'a :: comm_semiring_0 poly"`
`       `
`  2102   shows "pcompose (smult a p) r = smult a (pcompose p r)"`
`       `
`  2103   by (induction p) `
`       `
`  2104      (simp_all add: pcompose_pCons pcompose_add smult_add_right)`
`       `
`  2105 `
`       `
`  2106 lemma pcompose_mult:`
`       `
`  2107   fixes p q r :: "'a :: comm_semiring_0 poly"`
`       `
`  2108   shows "pcompose (p * q) r = pcompose p r * pcompose q r"`
`       `
`  2109   by (induction p arbitrary: q)`
`       `
`  2110      (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)`
`       `
`  2111 `
`       `
`  2112 lemma pcompose_assoc: `
`       `
`  2113   "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) =`
`       `
`  2114      pcompose (pcompose p q) r"`
`       `
`  2115   by (induction p arbitrary: q) `
`       `
`  2116      (simp_all add: pcompose_pCons pcompose_add pcompose_mult)`
`       `
`  2117 `
`       `
`  2118 `
`       `
`  2119 (* The remainder of this section and the next were contributed by Wenda Li *)`
`       `
`  2120 `
`       `
`  2121 lemma degree_mult_eq_0:`
`       `
`  2122   fixes p q:: "'a :: idom poly"`
`       `
`  2123   shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"`
`       `
`  2124 by (auto simp add:degree_mult_eq)`
`       `
`  2125 `
`       `
`  2126 lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) `
`       `
`  2127 `
`       `
`  2128 lemma pcompose_0':"pcompose p 0=[:coeff p 0:]"`
`       `
`  2129   apply (induct p)`
`       `
`  2130   apply (auto simp add:pcompose_pCons)`
`       `
`  2131 done`
`       `
`  2132 `
`       `
`  2133 lemma degree_pcompose:`
`       `
`  2134   fixes p q:: "'a::idom poly"`
`       `
`  2135   shows "degree(pcompose p q) = degree p * degree q"`
`       `
`  2136 proof (induct p)`
`       `
`  2137   case 0`
`       `
`  2138   thus ?case by auto`
`       `
`  2139 next`
`       `
`  2140   case (pCons a p)`
`       `
`  2141   have "degree (q * pcompose p q) = 0 \<Longrightarrow> ?case" `
`       `
`  2142     proof (cases "p=0")`
`       `
`  2143       case True`
`       `
`  2144       thus ?thesis by auto`
`       `
`  2145     next`
`       `
`  2146       case False assume "degree (q * pcompose p q) = 0"`
`       `
`  2147       hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)`
`       `
`  2148       moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0` `
`       `
`  2149         proof -`
`       `
`  2150           assume "pcompose p q=0" "degree q\<noteq>0"`
`       `
`  2151           hence "degree p=0" using pCons.hyps(2) by auto`
`       `
`  2152           then obtain a1 where "p=[:a1:]"`
`       `
`  2153             by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)`
`       `
`  2154           thus False using `pcompose p q=0` `p\<noteq>0` by auto`
`       `
`  2155         qed`
`       `
`  2156       ultimately have "degree (pCons a p) * degree q=0" by auto`
`       `
`  2157       moreover have "degree (pcompose (pCons a p) q) = 0" `
`       `
`  2158         proof -`
`       `
`  2159           have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"`
`       `
`  2160             using `degree (q * pcompose p q) = 0` by simp`
`       `
`  2161           also have "... \<ge> degree ([:a:] + q * pcompose p q)"`
`       `
`  2162             by (rule degree_add_le_max)`
`       `
`  2163           finally show ?thesis by (auto simp add:pcompose_pCons)`
`       `
`  2164         qed`
`       `
`  2165       ultimately show ?thesis by simp`
`       `
`  2166     qed`
`       `
`  2167   moreover have "degree (q * pcompose p q)>0 \<Longrightarrow> ?case" `
`       `
`  2168     proof -`
`       `
`  2169       assume asm:"0 < degree (q * pcompose p q)"`
`       `
`  2170       hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto`
`       `
`  2171       have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"`
`       `
`  2172         unfolding pcompose_pCons`
`       `
`  2173         using degree_add_eq_right[of "[:a:]" ] asm by auto       `
`       `
`  2174       thus ?thesis `
`       `
`  2175         using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto`
`       `
`  2176     qed`
`       `
`  2177   ultimately show ?case by blast`
`       `
`  2178 qed`
`       `
`  2179 `
`       `
`  2180 lemma pcompose_eq_0:`
`       `
`  2181   fixes p q:: "'a::idom poly"`
`       `
`  2182   assumes "pcompose p q=0" "degree q>0" `
`       `
`  2183   shows "p=0"`
`       `
`  2184 proof -`
`       `
`  2185   have "degree p=0" using assms degree_pcompose[of p q] by auto`
`       `
`  2186   then obtain a where "p=[:a:]" `
`       `
`  2187     by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)`
`       `
`  2188   hence "a=0" using assms(1) by auto`
`       `
`  2189   thus ?thesis using `p=[:a:]` by simp`
`       `
`  2190 qed`
`       `
`  2191 `
`       `
`  2192 `
`       `
`  2193 section{*lead coefficient*}`
`       `
`  2194 `
`       `
`  2195 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where`
`       `
`  2196   "lead_coeff p= coeff p (degree p)"`
`       `
`  2197 `
`       `
`  2198 lemma lead_coeff_pCons[simp]:`
`       `
`  2199     "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"`
`       `
`  2200     "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"`
`       `
`  2201 unfolding lead_coeff_def by auto`
`       `
`  2202 `
`       `
`  2203 lemma lead_coeff_0[simp]:"lead_coeff 0 =0" `
`       `
`  2204   unfolding lead_coeff_def by auto`
`       `
`  2205 `
`       `
`  2206 lemma lead_coeff_mult:`
`       `
`  2207    fixes p q::"'a ::idom poly"`
`       `
`  2208    shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"`
`       `
`  2209 by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)`
`       `
`  2210 `
`       `
`  2211 lemma lead_coeff_add_le:`
`       `
`  2212   assumes "degree p < degree q"`
`       `
`  2213   shows "lead_coeff (p+q) = lead_coeff q" `
`       `
`  2214 using assms unfolding lead_coeff_def`
`       `
`  2215 by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)`
`       `
`  2216 `
`       `
`  2217 lemma lead_coeff_minus:`
`       `
`  2218   "lead_coeff (-p) = - lead_coeff p"`
`       `
`  2219 by (metis coeff_minus degree_minus lead_coeff_def)`
`       `
`  2220 `
`       `
`  2221 `
`       `
`  2222 lemma lead_coeff_comp:`
`       `
`  2223   fixes p q:: "'a::idom poly"`
`       `
`  2224   assumes "degree q > 0" `
`       `
`  2225   shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"`
`       `
`  2226 proof (induct p)`
`       `
`  2227   case 0`
`       `
`  2228   thus ?case unfolding lead_coeff_def by auto`
`       `
`  2229 next`
`       `
`  2230   case (pCons a p)`
`       `
`  2231   have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"`
`       `
`  2232     proof -`
`       `
`  2233       assume "degree ( q * pcompose p q) = 0"`
`       `
`  2234       hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)`
`       `
`  2235       hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp`
`       `
`  2236       thus ?thesis by auto`
`       `
`  2237     qed`
`       `
`  2238   moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" `
`       `
`  2239     proof -`
`       `
`  2240       assume "degree ( q * pcompose p q) > 0"`
`       `
`  2241       hence "lead_coeff (pcompose (pCons a p) q) =lead_coeff ( q * pcompose p q)"`
`       `
`  2242         by (auto simp add:pcompose_pCons lead_coeff_add_le)`
`       `
`  2243       also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"`
`       `
`  2244         using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp`
`       `
`  2245       also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"`
`       `
`  2246         by auto`
`       `
`  2247       finally show ?thesis by auto`
`       `
`  2248     qed`
`       `
`  2249   ultimately show ?case by blast`
`       `
`  2250 qed`
`       `
`  2251 `
`       `
`  2252 lemma lead_coeff_smult: `
`       `
`  2253   "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"`
`       `
`  2254 proof -`
`       `
`  2255   have "smult c p = [:c:] * p" by simp`
`       `
`  2256   also have "lead_coeff \<dots> = c * lead_coeff p" `
`       `
`  2257     by (subst lead_coeff_mult) simp_all`
`       `
`  2258   finally show ?thesis .`
`       `
`  2259 qed`
`       `
`  2260 `
`       `
`  2261 lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"`
`       `
`  2262   by (simp add: lead_coeff_def)`
`       `
`  2263 `
`       `
`  2264 lemma lead_coeff_of_nat [simp]:`
`       `
`  2265   "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"`
`       `
`  2266   by (induction n) (simp_all add: lead_coeff_def of_nat_poly)`
`       `
`  2267 `
`       `
`  2268 lemma lead_coeff_numeral [simp]: `
`       `
`  2269   "lead_coeff (numeral n) = numeral n"`
`       `
`  2270   unfolding lead_coeff_def`
`       `
`  2271   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp`
`       `
`  2272 `
`       `
`  2273 lemma lead_coeff_power: `
`       `
`  2274   "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"`
`       `
`  2275   by (induction n) (simp_all add: lead_coeff_mult)`
`       `
`  2276 `
`       `
`  2277 lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"`
`       `
`  2278   by (simp add: lead_coeff_def)`
`       `
`  2279   `
`       `
`  2280   `
`  1948 `
`  2281 `
`  1949 no_notation cCons (infixr "##" 65)`
`  2282 no_notation cCons (infixr "##" 65)`
`  1950 `
`  2283 `
`  1951 end`
`  2284 end`