2256 lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1" |
2256 lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1" |
2257 by (simp add: reflect_poly_def one_poly_def) |
2257 by (simp add: reflect_poly_def one_poly_def) |
2258 |
2258 |
2259 lemma coeff_reflect_poly: |
2259 lemma coeff_reflect_poly: |
2260 "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))" |
2260 "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))" |
2261 by (cases "p = 0") (auto simp add: reflect_poly_def coeff_Poly_eq nth_default_def |
2261 by (cases "p = 0") (auto simp add: reflect_poly_def nth_default_def |
2262 rev_nth degree_eq_length_coeffs coeffs_nth not_less |
2262 rev_nth degree_eq_length_coeffs coeffs_nth not_less |
2263 dest: le_imp_less_Suc) |
2263 dest: le_imp_less_Suc) |
2264 |
2264 |
2265 lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0" |
2265 lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0" |
2266 by (simp add: coeff_reflect_poly) |
2266 by (simp add: coeff_reflect_poly) |
2310 proof (rule poly_eqI) |
2310 proof (rule poly_eqI) |
2311 fix i :: nat |
2311 fix i :: nat |
2312 show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" |
2312 show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" |
2313 proof (cases "i \<le> degree (p * q)") |
2313 proof (cases "i \<le> degree (p * q)") |
2314 case True |
2314 case True |
2315 def A \<equiv> "{..i} \<inter> {i - degree q..degree p}" |
2315 define A where "A = {..i} \<inter> {i - degree q..degree p}" |
2316 def B \<equiv> "{..degree p} \<inter> {degree p - i..degree (p*q) - i}" |
2316 define B where "B = {..degree p} \<inter> {degree p - i..degree (p*q) - i}" |
2317 let ?f = "\<lambda>j. degree p - j" |
2317 let ?f = "\<lambda>j. degree p - j" |
2318 |
2318 |
2319 from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)" |
2319 from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)" |
2320 by (simp add: coeff_reflect_poly) |
2320 by (simp add: coeff_reflect_poly) |
2321 also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))" |
2321 also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))" |
3678 qed |
3678 qed |
3679 qed |
3679 qed |
3680 |
3680 |
3681 end |
3681 end |
3682 |
3682 |
|
3683 lemma div_pCons_eq: |
|
3684 "pCons a p div q = (if q = 0 then 0 |
|
3685 else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) |
|
3686 (p div q))" |
|
3687 using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p] |
|
3688 by (auto intro: div_poly_eq) |
|
3689 |
|
3690 lemma mod_pCons_eq: |
|
3691 "pCons a p mod q = (if q = 0 then pCons a p |
|
3692 else pCons a (p mod q) - smult (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) |
|
3693 q)" |
|
3694 using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p] |
|
3695 by (auto intro: mod_poly_eq) |
|
3696 |
|
3697 lemma div_mod_fold_coeffs: |
|
3698 "(p div q, p mod q) = (if q = 0 then (0, p) |
|
3699 else fold_coeffs (\<lambda>a (s, r). |
|
3700 let b = coeff (pCons a r) (degree q) / coeff q (degree q) |
|
3701 in (pCons b s, pCons a r - smult b q) |
|
3702 ) p (0, 0))" |
|
3703 by (rule sym, induct p) (auto simp add: div_pCons_eq mod_pCons_eq Let_def) |
|
3704 |
3683 lemma degree_mod_less: |
3705 lemma degree_mod_less: |
3684 "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y" |
3706 "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y" |
3685 using eucl_rel_poly [of x y] |
3707 using eucl_rel_poly [of x y] |
3686 unfolding eucl_rel_poly_iff by simp |
3708 unfolding eucl_rel_poly_iff by simp |
3687 |
3709 |
3808 shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)" |
3830 shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)" |
3809 unfolding b |
3831 unfolding b |
3810 apply (rule mod_poly_eq) |
3832 apply (rule mod_poly_eq) |
3811 apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl]) |
3833 apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl]) |
3812 done |
3834 done |
3813 |
|
3814 definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" |
|
3815 where |
|
3816 "pdivmod p q = (p div q, p mod q)" |
|
3817 |
|
3818 lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)" |
|
3819 by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique) |
|
3820 |
|
3821 lemma pdivmod_0: |
|
3822 "pdivmod 0 q = (0, 0)" |
|
3823 by (simp add: pdivmod_def) |
|
3824 |
|
3825 lemma pdivmod_pCons: |
|
3826 "pdivmod (pCons a p) q = |
|
3827 (if q = 0 then (0, pCons a p) else |
|
3828 (let (s, r) = pdivmod p q; |
|
3829 b = coeff (pCons a r) (degree q) / coeff q (degree q) |
|
3830 in (pCons b s, pCons a r - smult b q)))" |
|
3831 apply (simp add: pdivmod_def Let_def, safe) |
|
3832 apply (rule div_poly_eq) |
|
3833 apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl]) |
|
3834 apply (rule mod_poly_eq) |
|
3835 apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl]) |
|
3836 done |
|
3837 |
|
3838 lemma pdivmod_fold_coeffs: |
|
3839 "pdivmod p q = (if q = 0 then (0, p) |
|
3840 else fold_coeffs (\<lambda>a (s, r). |
|
3841 let b = coeff (pCons a r) (degree q) / coeff q (degree q) |
|
3842 in (pCons b s, pCons a r - smult b q) |
|
3843 ) p (0, 0))" |
|
3844 apply (cases "q = 0") |
|
3845 apply (simp add: pdivmod_def) |
|
3846 apply (rule sym) |
|
3847 apply (induct p) |
|
3848 apply (simp_all add: pdivmod_0 pdivmod_pCons) |
|
3849 apply (case_tac "a = 0 \<and> p = 0") |
|
3850 apply (auto simp add: pdivmod_def) |
|
3851 done |
|
3852 |
3835 |
3853 |
3836 |
3854 subsubsection \<open>List-based versions for fast implementation\<close> |
3837 subsubsection \<open>List-based versions for fast implementation\<close> |
3855 (* Subsection by: |
3838 (* Subsection by: |
3856 Sebastiaan Joosten |
3839 Sebastiaan Joosten |
4076 |
4059 |
4077 |
4060 |
4078 (* *************** *) |
4061 (* *************** *) |
4079 subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close> |
4062 subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close> |
4080 |
4063 |
4081 lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f) |
4064 lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> (p div q, p mod q) = (r, s)" |
|
4065 by (metis eucl_rel_poly eucl_rel_poly_unique) |
|
4066 |
|
4067 lemma pdivmod_via_pseudo_divmod: "(f div g, f mod g) = (if g = 0 then (0,f) |
4082 else let |
4068 else let |
4083 ilc = inverse (coeff g (degree g)); |
4069 ilc = inverse (coeff g (degree g)); |
4084 h = smult ilc g; |
4070 h = smult ilc g; |
4085 (q,r) = pseudo_divmod f h |
4071 (q,r) = pseudo_divmod f h |
4086 in (smult ilc q, r))" (is "?l = ?r") |
4072 in (smult ilc q, r))" (is "?l = ?r") |
4094 from False have id: "?r = (smult lc q, r)" |
4080 from False have id: "?r = (smult lc q, r)" |
4095 unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto |
4081 unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto |
4096 from pseudo_divmod[OF h0 p, unfolded h1] |
4082 from pseudo_divmod[OF h0 p, unfolded h1] |
4097 have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto |
4083 have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto |
4098 have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto |
4084 have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto |
4099 hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel) |
4085 hence "(f div h, f mod h) = (q,r)" by (simp add: pdivmod_pdivmodrel) |
4100 hence "pdivmod f g = (smult lc q, r)" |
4086 hence "(f div g, f mod g) = (smult lc q, r)" |
4101 unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc] |
4087 unfolding h_def div_smult_right[OF lc] mod_smult_right[OF lc] |
4102 using lc by auto |
4088 using lc by auto |
4103 with id show ?thesis by auto |
4089 with id show ?thesis by auto |
4104 qed (auto simp: pdivmod_def) |
4090 qed simp |
4105 |
4091 |
4106 lemma pdivmod_via_pseudo_divmod_list: "pdivmod f g = (let |
4092 lemma pdivmod_via_pseudo_divmod_list: "(f div g, f mod g) = (let |
4107 cg = coeffs g |
4093 cg = coeffs g |
4108 in if cg = [] then (0,f) |
4094 in if cg = [] then (0,f) |
4109 else let |
4095 else let |
4110 cf = coeffs f; |
4096 cf = coeffs f; |
4111 ilc = inverse (last cg); |
4097 ilc = inverse (last cg); |
4156 qq = cCons a q; |
4142 qq = cCons a q; |
4157 rr = minus_poly_rev_list r (map (op * a) d) |
4143 rr = minus_poly_rev_list r (map (op * a) d) |
4158 in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])" |
4144 in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])" |
4159 | "divide_poly_main_list lc q r d 0 = q" |
4145 | "divide_poly_main_list lc q r d 0 = q" |
4160 |
4146 |
4161 |
|
4162 lemma divide_poly_main_list_simp[simp]: "divide_poly_main_list lc q r d (Suc n) = (let |
4147 lemma divide_poly_main_list_simp[simp]: "divide_poly_main_list lc q r d (Suc n) = (let |
4163 cr = hd r; |
4148 cr = hd r; |
4164 a = cr div lc; |
4149 a = cr div lc; |
4165 qq = cCons a q; |
4150 qq = cCons a q; |
4166 rr = minus_poly_rev_list r (map (op * a) d) |
4151 rr = minus_poly_rev_list r (map (op * a) d) |
4174 (let cg = coeffs g |
4159 (let cg = coeffs g |
4175 in if cg = [] then g |
4160 in if cg = [] then g |
4176 else let cf = coeffs f; cgr = rev cg |
4161 else let cf = coeffs f; cgr = rev cg |
4177 in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))" |
4162 in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))" |
4178 |
4163 |
4179 lemmas pdivmod_via_divmod_list[code] = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1] |
4164 lemmas pdivmod_via_divmod_list = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1] |
4180 |
4165 |
4181 lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n" |
4166 lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n" |
4182 by (induct n arbitrary: q r d, auto simp: Let_def) |
4167 by (induct n arbitrary: q r d, auto simp: Let_def) |
4183 |
4168 |
4184 lemma mod_poly_code[code]: "f mod g = |
4169 lemma mod_poly_code[code]: "f mod g = |
4186 in if cg = [] then f |
4171 in if cg = [] then f |
4187 else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg; |
4172 else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg; |
4188 r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg) |
4173 r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg) |
4189 in poly_of_list (rev r))" (is "?l = ?r") |
4174 in poly_of_list (rev r))" (is "?l = ?r") |
4190 proof - |
4175 proof - |
4191 have "?l = snd (pdivmod f g)" unfolding pdivmod_def by simp |
4176 have "snd (f div g, f mod g) = ?r" unfolding pdivmod_via_divmod_list Let_def |
4192 also have "\<dots> = ?r" unfolding pdivmod_via_divmod_list Let_def |
4177 mod_poly_one_main_list [symmetric, of _ _ _ Nil] by (auto split: prod.splits) |
4193 mod_poly_one_main_list[symmetric, of _ _ _ Nil] by (auto split: prod.splits) |
4178 then show ?thesis |
4194 finally show ?thesis . |
4179 by simp |
4195 qed |
4180 qed |
4196 |
4181 |
4197 definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
4182 definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
4198 "div_field_poly_impl f g = ( |
4183 "div_field_poly_impl f g = ( |
4199 let cg = coeffs g |
4184 let cg = coeffs g |
4206 on non-fields will no longer be executable. However, a code-unfold is possible, since |
4191 on non-fields will no longer be executable. However, a code-unfold is possible, since |
4207 \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close> |
4192 \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close> |
4208 lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl" |
4193 lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl" |
4209 proof (intro ext) |
4194 proof (intro ext) |
4210 fix f g :: "'a poly" |
4195 fix f g :: "'a poly" |
4211 have "f div g = fst (pdivmod f g)" unfolding pdivmod_def by simp |
4196 have "fst (f div g, f mod g) = div_field_poly_impl f g" unfolding |
4212 also have "\<dots> = div_field_poly_impl f g" unfolding |
|
4213 div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits) |
4197 div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits) |
4214 finally show "f div g = div_field_poly_impl f g" . |
4198 then show "f div g = div_field_poly_impl f g" |
4215 qed |
4199 by simp |
4216 |
4200 qed |
4217 |
4201 |
4218 lemma divide_poly_main_list: |
4202 lemma divide_poly_main_list: |
4219 assumes lc0: "lc \<noteq> 0" |
4203 assumes lc0: "lc \<noteq> 0" |
4220 and lc:"last d = lc" |
4204 and lc:"last d = lc" |
4221 and d:"d \<noteq> []" |
4205 and d:"d \<noteq> []" |