src/HOL/Library/Polynomial.thy
 changeset 62072 bf3d9f113474 parent 62067 0fd850943901 child 62128 3201ddb00097
equal 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"`