src/HOL/Library/Polynomial.thy
changeset 62072 bf3d9f113474
parent 62067 0fd850943901
child 62128 3201ddb00097
equal deleted inserted replaced
62071:4e6e850e97c2 62072:bf3d9f113474
   473       also note pCons.IH
   473       also note pCons.IH
   474       also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
   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)"
   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)
   476           by (simp add: field_simps setsum_right_distrib coeff_pCons)
   477       also note setsum_atMost_Suc_shift[symmetric]
   477       also note setsum_atMost_Suc_shift[symmetric]
   478       also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
   478       also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
   479       finally show ?thesis .
   479       finally show ?thesis .
   480    qed simp
   480    qed simp
   481 qed simp
   481 qed simp
   482 
   482 
   483 
   483 
  2143       case True
  2143       case True
  2144       thus ?thesis by auto
  2144       thus ?thesis by auto
  2145     next
  2145     next
  2146       case False assume "degree (q * pcompose p q) = 0"
  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)
  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` 
  2148       moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close> 
  2149         proof -
  2149         proof -
  2150           assume "pcompose p q=0" "degree q\<noteq>0"
  2150           assume "pcompose p q=0" "degree q\<noteq>0"
  2151           hence "degree p=0" using pCons.hyps(2) by auto
  2151           hence "degree p=0" using pCons.hyps(2) by auto
  2152           then obtain a1 where "p=[:a1:]"
  2152           then obtain a1 where "p=[:a1:]"
  2153             by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
  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
  2154           thus False using \<open>pcompose p q=0\<close> \<open>p\<noteq>0\<close> by auto
  2155         qed
  2155         qed
  2156       ultimately have "degree (pCons a p) * degree q=0" by auto
  2156       ultimately have "degree (pCons a p) * degree q=0" by auto
  2157       moreover have "degree (pcompose (pCons a p) q) = 0" 
  2157       moreover have "degree (pcompose (pCons a p) q) = 0" 
  2158         proof -
  2158         proof -
  2159           have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
  2159           have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
  2160             using `degree (q * pcompose p q) = 0` by simp
  2160             using \<open>degree (q * pcompose p q) = 0\<close> by simp
  2161           also have "... \<ge> degree ([:a:] + q * pcompose p q)"
  2161           also have "... \<ge> degree ([:a:] + q * pcompose p q)"
  2162             by (rule degree_add_le_max)
  2162             by (rule degree_add_le_max)
  2163           finally show ?thesis by (auto simp add:pcompose_pCons)
  2163           finally show ?thesis by (auto simp add:pcompose_pCons)
  2164         qed
  2164         qed
  2165       ultimately show ?thesis by simp
  2165       ultimately show ?thesis by simp
  2170       hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto
  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)"
  2171       have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"
  2172         unfolding pcompose_pCons
  2172         unfolding pcompose_pCons
  2173         using degree_add_eq_right[of "[:a:]" ] asm by auto       
  2173         using degree_add_eq_right[of "[:a:]" ] asm by auto       
  2174       thus ?thesis 
  2174       thus ?thesis 
  2175         using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
  2175         using pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] by auto
  2176     qed
  2176     qed
  2177   ultimately show ?case by blast
  2177   ultimately show ?case by blast
  2178 qed
  2178 qed
  2179 
  2179 
  2180 lemma pcompose_eq_0:
  2180 lemma pcompose_eq_0:
  2184 proof -
  2184 proof -
  2185   have "degree p=0" using assms degree_pcompose[of p q] by auto
  2185   have "degree p=0" using assms degree_pcompose[of p q] by auto
  2186   then obtain a where "p=[:a:]" 
  2186   then obtain a where "p=[:a:]" 
  2187     by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
  2187     by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
  2188   hence "a=0" using assms(1) by auto
  2188   hence "a=0" using assms(1) by auto
  2189   thus ?thesis using `p=[:a:]` by simp
  2189   thus ?thesis using \<open>p=[:a:]\<close> by simp
  2190 qed
  2190 qed
  2191 
  2191 
  2192 
  2192 
  2193 subsection {* Leading coefficient *}
  2193 subsection \<open>Leading coefficient\<close>
  2194 
  2194 
  2195 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
  2195 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
  2196   "lead_coeff p= coeff p (degree p)"
  2196   "lead_coeff p= coeff p (degree p)"
  2197 
  2197 
  2198 lemma lead_coeff_pCons[simp]:
  2198 lemma lead_coeff_pCons[simp]:
  2230   case (pCons a p)
  2230   case (pCons a p)
  2231   have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
  2231   have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
  2232     proof -
  2232     proof -
  2233       assume "degree ( q * pcompose p q) = 0"
  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)
  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
  2235       hence "p=0" using pcompose_eq_0[OF _ \<open>degree q > 0\<close>] by simp
  2236       thus ?thesis by auto
  2236       thus ?thesis by auto
  2237     qed
  2237     qed
  2238   moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
  2238   moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
  2239     proof -
  2239     proof -
  2240       assume "degree ( q * pcompose p q) > 0"
  2240       assume "degree ( q * pcompose p q) > 0"