src/HOL/Polynomial.thy
 changeset 29475 c06d1b0a970f parent 29474 674a21226c5a child 29478 4a2482e16934
equal inserted replaced
29474:674a21226c5a 29475:c06d1b0a970f
`   206 subsection {* Recursion combinator for polynomials *}`
`   206 subsection {* Recursion combinator for polynomials *}`
`   207 `
`   207 `
`   208 function`
`   208 function`
`   209   poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"`
`   209   poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"`
`   210 where`
`   210 where`
`   211   poly_rec_pCons_eq_if [simp del]:`
`   211   poly_rec_pCons_eq_if [simp del, code del]:`
`   212     "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"`
`   212     "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"`
`   213 by (case_tac x, rename_tac q, case_tac q, auto)`
`   213 by (case_tac x, rename_tac q, case_tac q, auto)`
`   214 `
`   214 `
`   215 termination poly_rec`
`   215 termination poly_rec`
`   216 by (relation "measure (degree \<circ> snd \<circ> snd)", simp)`
`   216 by (relation "measure (degree \<circ> snd \<circ> snd)", simp)`
`   485 `
`   485 `
`   486 instantiation poly :: (comm_semiring_0) comm_semiring_0`
`   486 instantiation poly :: (comm_semiring_0) comm_semiring_0`
`   487 begin`
`   487 begin`
`   488 `
`   488 `
`   489 definition`
`   489 definition`
`   490   times_poly_def:`
`   490   times_poly_def [code del]:`
`   491     "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"`
`   491     "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"`
`   492 `
`   492 `
`   493 lemma mult_poly_0_left: "(0::'a poly) * q = 0"`
`   493 lemma mult_poly_0_left: "(0::'a poly) * q = 0"`
`   494   unfolding times_poly_def by (simp add: poly_rec_0)`
`   494   unfolding times_poly_def by (simp add: poly_rec_0)`
`   495 `
`   495 `
`   647 subsection {* Long division of polynomials *}`
`   647 subsection {* Long division of polynomials *}`
`   648 `
`   648 `
`   649 definition`
`   649 definition`
`   650   divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"`
`   650   divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"`
`   651 where`
`   651 where`
`       `
`   652   [code del]:`
`   652   "divmod_poly_rel x y q r \<longleftrightarrow>`
`   653   "divmod_poly_rel x y q r \<longleftrightarrow>`
`   653     x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"`
`   654     x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"`
`   654 `
`   655 `
`   655 lemma divmod_poly_rel_0:`
`   656 lemma divmod_poly_rel_0:`
`   656   "divmod_poly_rel 0 y 0 0"`
`   657   "divmod_poly_rel 0 y 0 0"`