src/HOL/Library/Polynomial.thy
changeset 62065 1546a042e87b
parent 61945 1135b8de26c3
child 62067 0fd850943901
equal deleted 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