src/HOL/Polynomial.thy
changeset 29475 c06d1b0a970f
parent 29474 674a21226c5a
child 29478 4a2482e16934
equal deleted 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"