--- a/src/HOL/Library/Polynomial.thy Sat Apr 01 22:15:59 2017 +0200
+++ b/src/HOL/Library/Polynomial.thy Sat Apr 01 23:48:28 2017 +0200
@@ -2573,7 +2573,7 @@
lemma poly_pinfty_gt_lc:
fixes p :: "real poly"
assumes "lead_coeff p > 0"
- shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
+ shows "\<exists>n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
using assms
proof (induct p)
case 0
@@ -2691,47 +2691,48 @@
qed
lemma poly_squarefree_decomp_order2:
- "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
- p = q * d;
- pderiv p = e * d;
- d = r * p + s * pderiv p
- \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
-by (blast intro: poly_squarefree_decomp_order)
+ "pderiv p \<noteq> 0 \<Longrightarrow> p = q * d \<Longrightarrow> pderiv p = e * d \<Longrightarrow>
+ d = r * p + s * pderiv p \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
+ for p :: "'a::field_char_0 poly"
+ by (blast intro: poly_squarefree_decomp_order)
lemma order_pderiv2:
- "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
- \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
-by (auto dest: order_pderiv)
+ "pderiv p \<noteq> 0 \<Longrightarrow> order a p \<noteq> 0 \<Longrightarrow> order a (pderiv p) = n \<longleftrightarrow> order a p = Suc n"
+ for p :: "'a::field_char_0 poly"
+ by (auto dest: order_pderiv)
definition rsquarefree :: "'a::idom poly \<Rightarrow> bool"
where "rsquarefree p \<longleftrightarrow> p \<noteq> 0 \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
-lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
+lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]"
+ for p :: "'a::{semidom,semiring_char_0} poly"
by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
-lemma rsquarefree_roots:
- fixes p :: "'a :: field_char_0 poly"
- shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
-apply (simp add: rsquarefree_def)
-apply (case_tac "p = 0", simp, simp)
-apply (case_tac "pderiv p = 0")
-apply simp
-apply (drule pderiv_iszero, clarsimp)
-apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
-apply (force simp add: order_root order_pderiv2)
+lemma rsquarefree_roots: "rsquarefree p \<longleftrightarrow> (\<forall>a. \<not> (poly p a = 0 \<and> poly (pderiv p) a = 0))"
+ for p :: "'a::field_char_0 poly"
+ apply (simp add: rsquarefree_def)
+ apply (case_tac "p = 0")
+ apply simp
+ apply simp
+ apply (case_tac "pderiv p = 0")
+ apply simp
+ apply (drule pderiv_iszero, clarsimp)
+ apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
+ apply (force simp add: order_root order_pderiv2)
done
lemma poly_squarefree_decomp:
- assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
+ fixes p :: "'a::field_char_0 poly"
+ assumes "pderiv p \<noteq> 0"
and "p = q * d"
and "pderiv p = e * d"
and "d = r * p + s * pderiv p"
- shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
+ shows "rsquarefree q \<and> (\<forall>a. poly q a = 0 \<longleftrightarrow> poly p a = 0)"
proof -
from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
- have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
- using assms by (rule poly_squarefree_decomp_order2)
+ from assms have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
+ by (rule poly_squarefree_decomp_order2)
with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
by (simp add: rsquarefree_def order_root)
qed
@@ -2748,80 +2749,84 @@
LCM of its coefficients, yielding an integer polynomial with the same roots.
\<close>
-definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
- "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
-
-lemma algebraicI:
- assumes "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
- shows "algebraic x"
- using assms unfolding algebraic_def by blast
+definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool"
+ where "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
+
+lemma algebraicI: "(\<And>i. coeff p i \<in> \<int>) \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> poly p x = 0 \<Longrightarrow> algebraic x"
+ unfolding algebraic_def by blast
lemma algebraicE:
assumes "algebraic x"
obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
using assms unfolding algebraic_def by blast
-lemma algebraic_altdef:
- fixes p :: "'a :: field_char_0 poly"
- shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
+lemma algebraic_altdef: "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
+ for p :: "'a::field_char_0 poly"
proof safe
- fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
+ fix p
+ assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
define cs where "cs = coeffs p"
- from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
+ from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'"
+ unfolding Rats_def by blast
then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
by (subst (asm) bchoice_iff) blast
define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
define d where "d = Lcm (set (map snd cs'))"
define p' where "p' = smult (of_int d) p"
- have "\<forall>n. coeff p' n \<in> \<int>"
- proof
- fix n :: nat
- show "coeff p' n \<in> \<int>"
- proof (cases "n \<le> degree p")
- case True
- define c where "c = coeff p n"
- define a where "a = fst (quotient_of (f (coeff p n)))"
- define b where "b = snd (quotient_of (f (coeff p n)))"
- have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp
- have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def)
- also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def
- by (subst quotient_of_div [of "f (coeff p n)", symmetric])
- (simp_all add: f [symmetric])
- also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
- by (simp add: of_rat_mult of_rat_divide)
- also from nz True have "b \<in> snd ` set cs'" unfolding cs'_def
- by (force simp: o_def b_def coeffs_def simp del: upt_Suc)
- then have "b dvd (a * d)" unfolding d_def by simp
- then have "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
- by (rule of_int_divide_in_Ints)
- then have "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
- finally show ?thesis .
- qed (auto simp: p'_def not_le coeff_eq_0)
+ have "coeff p' n \<in> \<int>" for n
+ proof (cases "n \<le> degree p")
+ case True
+ define c where "c = coeff p n"
+ define a where "a = fst (quotient_of (f (coeff p n)))"
+ define b where "b = snd (quotient_of (f (coeff p n)))"
+ have b_pos: "b > 0"
+ unfolding b_def using quotient_of_denom_pos' by simp
+ have "coeff p' n = of_int d * coeff p n"
+ by (simp add: p'_def)
+ also have "coeff p n = of_rat (of_int a / of_int b)"
+ unfolding a_def b_def
+ by (subst quotient_of_div [of "f (coeff p n)", symmetric]) (simp_all add: f [symmetric])
+ also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
+ by (simp add: of_rat_mult of_rat_divide)
+ also from nz True have "b \<in> snd ` set cs'"
+ by (force simp: cs'_def o_def b_def coeffs_def simp del: upt_Suc)
+ then have "b dvd (a * d)"
+ by (simp add: d_def)
+ then have "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
+ by (rule of_int_divide_in_Ints)
+ then have "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
+ finally show ?thesis .
+ next
+ case False
+ then show ?thesis
+ by (auto simp: p'_def not_le coeff_eq_0)
qed
-
moreover have "set (map snd cs') \<subseteq> {0<..}"
unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc)
- then have "d \<noteq> 0" unfolding d_def by (induction cs') simp_all
+ then have "d \<noteq> 0"
+ unfolding d_def by (induct cs') simp_all
with nz have "p' \<noteq> 0" by (simp add: p'_def)
- moreover from root have "poly p' x = 0" by (simp add: p'_def)
- ultimately show "algebraic x" unfolding algebraic_def by blast
+ moreover from root have "poly p' x = 0"
+ by (simp add: p'_def)
+ ultimately show "algebraic x"
+ unfolding algebraic_def by blast
next
assume "algebraic x"
then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
by (force simp: algebraic_def)
- moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
- ultimately show "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
+ moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i
+ by (elim Ints_cases) simp
+ ultimately show "\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0" by auto
qed
subsection \<open>Content and primitive part of a polynomial\<close>
-definition content :: "('a :: semiring_gcd poly) \<Rightarrow> 'a" where
- "content p = gcd_list (coeffs p)"
-
-lemma content_eq_fold_coeffs [code]:
- "content p = fold_coeffs gcd p 0"
+definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
+ where "content p = gcd_list (coeffs p)"
+
+lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
lemma content_0 [simp]: "content 0 = 0"
@@ -2833,22 +2838,26 @@
lemma content_const [simp]: "content [:c:] = normalize c"
by (simp add: content_def cCons_def)
-lemma const_poly_dvd_iff_dvd_content:
- fixes c :: "'a :: semiring_gcd"
- shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
+lemma const_poly_dvd_iff_dvd_content: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
+ for c :: "'a::semiring_gcd"
proof (cases "p = 0")
- case [simp]: False
- have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
+ case True
+ then show ?thesis by simp
+next
+ case False
+ have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
+ by (rule const_poly_dvd_iff)
also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
proof safe
- fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
+ fix n :: nat
+ assume "\<forall>a\<in>set (coeffs p). c dvd a"
then show "c dvd coeff p n"
by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
also have "\<dots> \<longleftrightarrow> c dvd content p"
by (simp add: content_def dvd_Gcd_fin_iff dvd_mult_unit_iff)
finally show ?thesis .
-qed simp_all
+qed
lemma content_dvd [simp]: "[:content p:] dvd p"
by (subst const_poly_dvd_iff_dvd_content) simp_all
@@ -2884,38 +2893,45 @@
lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
by (auto simp: content_def simp: poly_eq_iff coeffs_def)
-definition primitive_part :: "'a :: semiring_gcd poly \<Rightarrow> 'a poly" where
- "primitive_part p = map_poly (\<lambda>x. x div content p) p"
+definition primitive_part :: "'a :: semiring_gcd poly \<Rightarrow> 'a poly"
+ where "primitive_part p = map_poly (\<lambda>x. x div content p) p"
lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
by (simp add: primitive_part_def)
-lemma content_times_primitive_part [simp]:
- fixes p :: "'a :: semiring_gcd poly"
- shows "smult (content p) (primitive_part p) = p"
+lemma content_times_primitive_part [simp]: "smult (content p) (primitive_part p) = p"
+ for p :: "'a :: semiring_gcd poly"
proof (cases "p = 0")
+ case True
+ then show ?thesis by simp
+next
case False
then show ?thesis
unfolding primitive_part_def
by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
- intro: map_poly_idI)
-qed simp_all
+ intro: map_poly_idI)
+qed
lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
proof (cases "p = 0")
+ case True
+ then show ?thesis by simp
+next
case False
then have "primitive_part p = map_poly (\<lambda>x. x div content p) p"
by (simp add: primitive_part_def)
also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
- finally show ?thesis using False by simp
-qed simp
+ finally show ?thesis
+ using False by simp
+qed
lemma content_primitive_part [simp]:
assumes "p \<noteq> 0"
- shows "content (primitive_part p) = 1"
+ shows "content (primitive_part p) = 1"
proof -
- have "p = smult (content p) (primitive_part p)" by simp
+ have "p = smult (content p) (primitive_part p)"
+ by simp
also have "content \<dots> = content (primitive_part p) * content p"
by (simp del: content_times_primitive_part add: ac_simps)
finally have "1 * content p = content (primitive_part p) * content p"
@@ -2927,21 +2943,23 @@
qed
lemma content_decompose:
- fixes p :: "'a :: semiring_gcd poly"
- obtains p' where "p = smult (content p) p'" "content p' = 1"
+ obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
proof (cases "p = 0")
case True
then show ?thesis by (intro that[of 1]) simp_all
next
case False
- from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
- have "content p * 1 = content p * content r" by (subst r) simp
- with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
- with r show ?thesis by (intro that[of r]) simp_all
+ from content_dvd[of p] obtain r where r: "p = [:content p:] * r"
+ by (rule dvdE)
+ have "content p * 1 = content p * content r"
+ by (subst r) simp
+ with False have "content r = 1"
+ by (subst (asm) mult_left_cancel) simp_all
+ with r show ?thesis
+ by (intro that[of r]) simp_all
qed
-lemma content_dvd_contentI [intro]:
- "p dvd q \<Longrightarrow> content p dvd content q"
+lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q"
using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
@@ -2952,12 +2970,16 @@
lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
proof (cases "p = 0")
+ case True
+ then show ?thesis by simp
+next
case False
- have "p = smult (content p) (primitive_part p)" by simp
+ have "p = smult (content p) (primitive_part p)"
+ by simp
also from False have "degree \<dots> = degree (primitive_part p)"
by (subst degree_smult_eq) simp_all
finally show ?thesis ..
-qed simp_all
+qed
subsection \<open>Division of polynomials\<close>
@@ -2967,29 +2989,33 @@
instantiation poly :: (idom_divide) idom_divide
begin
-fun divide_poly_main :: "'a \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
- \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly" where
- "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in
- if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
- divide_poly_main
- lc
- (q + mon)
- (r - mon * d)
- d (dr - 1) n else 0)"
-| "divide_poly_main lc q r d dr 0 = q"
-
-definition divide_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
- "divide_poly f g = (if g = 0 then 0 else
- divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))"
+fun divide_poly_main :: "'a \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly"
+ where
+ "divide_poly_main lc q r d dr (Suc n) =
+ (let cr = coeff r dr; a = cr div lc; mon = monom a n in
+ if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
+ divide_poly_main
+ lc
+ (q + mon)
+ (r - mon * d)
+ d (dr - 1) n else 0)"
+ | "divide_poly_main lc q r d dr 0 = q"
+
+definition divide_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+ where "divide_poly f g =
+ (if g = 0 then 0
+ else
+ divide_poly_main (coeff g (degree g)) 0 f g (degree f)
+ (1 + length (coeffs f) - length (coeffs g)))"
lemma divide_poly_main:
assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
- and *: "degree (d * r) \<le> dr" "divide_poly_main lc q (d * r) d dr n = q'"
- "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> d * r = 0"
+ and "degree (d * r) \<le> dr" "divide_poly_main lc q (d * r) d dr n = q'"
+ and "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> d * r = 0"
shows "q' = q + r"
- using *
+ using assms(3-)
proof (induct n arbitrary: q r dr)
- case (Suc n q r dr)
+ case (Suc n)
let ?rr = "d * r"
let ?a = "coeff ?rr dr"
let ?qq = "?a div lc"
@@ -2997,107 +3023,135 @@
let ?rrr = "d * (r - b)"
let ?qqq = "q + b"
note res = Suc(3)
- have dr: "dr = n + degree d" using Suc(4) by auto
- have lc: "lc \<noteq> 0" using d by auto
+ from Suc(4) have dr: "dr = n + degree d" by auto
+ from d have lc: "lc \<noteq> 0" by auto
have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
proof (cases "?qq = 0")
+ case True
+ then show ?thesis by simp
+ next
case False
- then have n: "n = degree b" by (simp add: degree_monom_eq)
- show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
- qed simp
- also have "\<dots> = lc * coeff b n" unfolding d by simp
+ then have n: "n = degree b"
+ by (simp add: degree_monom_eq)
+ show ?thesis
+ unfolding n dr by (simp add: coeff_mult_degree_sum)
+ qed
+ also have "\<dots> = lc * coeff b n"
+ by (simp add: d)
finally have c2: "coeff (b * d) dr = lc * coeff b n" .
- have rrr: "?rrr = ?rr - b * d" by (simp add: field_simps)
+ have rrr: "?rrr = ?rr - b * d"
+ by (simp add: field_simps)
have c1: "coeff (d * r) dr = lc * coeff r n"
proof (cases "degree r = n")
case True
- then show ?thesis using Suc(2) unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps)
+ with Suc(2) show ?thesis
+ unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps)
next
case False
- have "degree r \<le> n" using dr Suc(2) by auto
- (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq diff_is_0_eq diff_zero le_cases)
- with False have r_n: "degree r < n" by auto
- then have right: "lc * coeff r n = 0" by (simp add: coeff_eq_0)
- have "coeff (d * r) dr = coeff (d * r) (degree d + n)" unfolding dr by (simp add: ac_simps)
- also have "\<dots> = 0" using r_n
+ from dr Suc(2) have "degree r \<le> n"
+ by auto
+ (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq
+ diff_is_0_eq diff_zero le_cases)
+ with False have r_n: "degree r < n"
+ by auto
+ then have right: "lc * coeff r n = 0"
+ by (simp add: coeff_eq_0)
+ have "coeff (d * r) dr = coeff (d * r) (degree d + n)"
+ by (simp add: dr ac_simps)
+ also from r_n have "\<dots> = 0"
by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0
coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq)
- finally show ?thesis unfolding right .
+ finally show ?thesis
+ by (simp only: right)
qed
have c0: "coeff ?rrr dr = 0"
- and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr" unfolding rrr coeff_diff c2
+ and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr"
+ unfolding rrr coeff_diff c2
unfolding b_def coeff_monom coeff_smult c1 using lc by auto
from res[unfolded divide_poly_main.simps[of lc q] Let_def] id
have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'"
by (simp del: divide_poly_main.simps add: field_simps)
note IH = Suc(1)[OF _ res]
- have dr: "dr = n + degree d" using Suc(4) by auto
- have deg_rr: "degree ?rr \<le> dr" using Suc(2) by auto
+ from Suc(4) have dr: "dr = n + degree d" by auto
+ from Suc(2) have deg_rr: "degree ?rr \<le> dr" by auto
have deg_bd: "degree (b * d) \<le> dr"
- unfolding dr b_def by (rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
- have "degree ?rrr \<le> dr" unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd])
+ unfolding dr b_def by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le)
+ have "degree ?rrr \<le> dr"
+ unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd])
with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)"
by (rule coeff_0_degree_minus_1)
have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
proof (cases dr)
case 0
- with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
- with deg_rrr have "degree ?rrr = 0" by simp
- from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]" by metis
- show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
- qed (insert Suc(4), auto)
- note IH = IH[OF deg_rrr this]
- show ?case using IH by simp
+ with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0"
+ by auto
+ with deg_rrr have "degree ?rrr = 0"
+ by simp
+ from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]"
+ by metis
+ show ?thesis
+ unfolding 0 using c0 unfolding rrr 0 by simp
+ next
+ case _: Suc
+ with Suc(4) show ?thesis by auto
+ qed
+ from IH[OF deg_rrr this] show ?case
+ by simp
next
- case (0 q r dr)
+ case 0
show ?case
proof (cases "r = 0")
case True
- then show ?thesis using 0 by auto
+ with 0 show ?thesis by auto
next
case False
- have "degree (d * r) = degree d + degree r" using d False
- by (subst degree_mult_eq, auto)
- then show ?thesis using 0 d by auto
+ from d False have "degree (d * r) = degree d + degree r"
+ by (subst degree_mult_eq) auto
+ with 0 d show ?thesis by auto
qed
qed
lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0"
proof (induct n arbitrary: r d dr)
- case (Suc n r d dr)
- show ?case unfolding divide_poly_main.simps[of _ _ r] Let_def
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ show ?case
+ unfolding divide_poly_main.simps[of _ _ r] Let_def
by (simp add: Suc del: divide_poly_main.simps)
-qed simp
+qed
lemma divide_poly:
assumes g: "g \<noteq> 0"
shows "(f * g) div g = (f :: 'a poly)"
proof -
- have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs g))
- = (f * g) div g" unfolding divide_poly_def Let_def by (simp add: ac_simps)
+ have len: "length (coeffs f) = Suc (degree f)" if "f \<noteq> 0" for f :: "'a poly"
+ using that unfolding degree_eq_length_coeffs by auto
+ have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f))
+ (1 + length (coeffs (g * f)) - length (coeffs g)) = (f * g) div g"
+ by (simp add: divide_poly_def Let_def ac_simps)
note main = divide_poly_main[OF g refl le_refl this]
- {
- fix f :: "'a poly"
- assume "f \<noteq> 0"
- then have "length (coeffs f) = Suc (degree f)" unfolding degree_eq_length_coeffs by auto
- } note len = this
have "(f * g) div g = 0 + f"
proof (rule main, goal_cases)
case 1
show ?case
proof (cases "f = 0")
case True
- with g show ?thesis by (auto simp: degree_eq_length_coeffs)
+ with g show ?thesis
+ by (auto simp: degree_eq_length_coeffs)
next
case False
with g have fg: "g * f \<noteq> 0" by auto
- show ?thesis unfolding len[OF fg] len[OF g] by auto
+ show ?thesis
+ unfolding len[OF fg] len[OF g] by auto
qed
qed
then show ?thesis by simp
qed
-lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
+lemma divide_poly_0: "f div 0 = 0"
+ for f :: "'a poly"
by (simp add: divide_poly_def Let_def divide_poly_main_0)
instance
@@ -3109,17 +3163,23 @@
lemma div_const_poly_conv_map_poly:
assumes "[:c:] dvd p"
- shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
+ shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
proof (cases "c = 0")
+ case True
+ then show ?thesis
+ by (auto intro!: poly_eqI simp: coeff_map_poly)
+next
case False
- from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
+ from assms obtain q where p: "p = [:c:] * q" by (rule dvdE)
moreover {
- have "smult c q = [:c:] * q" by simp
- also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
+ have "smult c q = [:c:] * q"
+ by simp
+ also have "\<dots> div [:c:] = q"
+ by (rule nonzero_mult_div_cancel_left) (use False in auto)
finally have "smult c q div [:c:] = q" .
}
ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
-qed (auto intro!: poly_eqI simp: coeff_map_poly)
+qed
lemma is_unit_monom_0:
fixes a :: "'a::field"
@@ -3130,46 +3190,47 @@
by (simp add: mult_monom)
qed
-lemma is_unit_triv:
- fixes a :: "'a::field"
- assumes "a \<noteq> 0"
- shows "is_unit [:a:]"
- using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
+lemma is_unit_triv: "a \<noteq> 0 \<Longrightarrow> is_unit [:a:]"
+ for a :: "'a::field"
+ by (simp add: is_unit_monom_0 monom_0 [symmetric])
lemma is_unit_iff_degree:
- assumes "p \<noteq> (0 :: _ :: field poly)"
- shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
+ fixes p :: "'a::field poly"
+ assumes "p \<noteq> 0"
+ shows "is_unit p \<longleftrightarrow> degree p = 0"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume ?Q
- then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
- with assms show ?P by (simp add: is_unit_triv)
+ assume ?rhs
+ then obtain a where "p = [:a:]"
+ by (rule degree_eq_zeroE)
+ with assms show ?lhs
+ by (simp add: is_unit_triv)
next
- assume ?P
+ assume ?lhs
then obtain q where "q \<noteq> 0" "p * q = 1" ..
then have "degree (p * q) = degree 1"
by simp
with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
by (simp add: degree_mult_eq)
- then show ?Q by simp
+ then show ?rhs by simp
qed
-lemma is_unit_pCons_iff:
- "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
- by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
-
-lemma is_unit_monom_trival:
- fixes p :: "'a::field poly"
- assumes "is_unit p"
- shows "monom (coeff p (degree p)) 0 = p"
- using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
-
-lemma is_unit_const_poly_iff:
- "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
+lemma is_unit_pCons_iff: "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
+ for p :: "'a::field poly"
+ by (cases "p = 0") (auto simp: is_unit_triv is_unit_iff_degree)
+
+lemma is_unit_monom_trival: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
+ for p :: "'a::field poly"
+ by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
+
+lemma is_unit_const_poly_iff: "[:c:] dvd 1 \<longleftrightarrow> c dvd 1"
+ for c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
by (auto simp: one_poly_def)
lemma is_unit_polyE:
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
- assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
+ assumes "p dvd 1"
+ obtains c where "p = [:c:]" "c dvd 1"
proof -
from assms obtain q where "1 = p * q"
by (rule dvdE)
@@ -3181,53 +3242,62 @@
by (simp add: degree_mult_eq)
finally have "degree p = 0" by simp
with degree_eq_zeroE obtain c where c: "p = [:c:]" .
- moreover with \<open>p dvd 1\<close> have "c dvd 1"
+ with \<open>p dvd 1\<close> have "c dvd 1"
by (simp add: is_unit_const_poly_iff)
- ultimately show thesis
- by (rule that)
+ with c show thesis ..
qed
lemma is_unit_polyE':
- assumes "is_unit (p::_::field poly)"
+ fixes p :: "'a::field poly"
+ assumes "is_unit p"
obtains a where "p = monom a 0" and "a \<noteq> 0"
proof -
- obtain a q where "p = pCons a q" by (cases p)
+ obtain a q where "p = pCons a q"
+ by (cases p)
with assms have "p = [:a:]" and "a \<noteq> 0"
by (simp_all add: is_unit_pCons_iff)
with that show thesis by (simp add: monom_0)
qed
-lemma is_unit_poly_iff:
- fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
- shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
+lemma is_unit_poly_iff: "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
+ for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
subsubsection \<open>Pseudo-Division\<close>
-text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
-
-fun pseudo_divmod_main :: "'a :: comm_ring_1 \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
- \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly \<times> 'a poly" where
- "pseudo_divmod_main lc q r d dr (Suc n) = (let
- rr = smult lc r;
- qq = coeff r dr;
- rrr = rr - monom qq n * d;
- qqq = smult lc q + monom qq n
- in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
-| "pseudo_divmod_main lc q r d dr 0 = (q,r)"
-
-definition pseudo_divmod :: "'a :: comm_ring_1 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" where
- "pseudo_divmod p q \<equiv> if q = 0 then (0,p) else
- pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p) (1 + length (coeffs p) - length (coeffs q))"
-
-lemma pseudo_divmod_main: assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
- and *: "degree r \<le> dr" "pseudo_divmod_main lc q r d dr n = (q',r')"
- "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> r = 0"
+text \<open>This part is by René Thiemann and Akihisa Yamada.\<close>
+
+fun pseudo_divmod_main ::
+ "'a :: comm_ring_1 \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly \<times> 'a poly"
+ where
+ "pseudo_divmod_main lc q r d dr (Suc n) =
+ (let
+ rr = smult lc r;
+ qq = coeff r dr;
+ rrr = rr - monom qq n * d;
+ qqq = smult lc q + monom qq n
+ in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
+ | "pseudo_divmod_main lc q r d dr 0 = (q,r)"
+
+definition pseudo_divmod :: "'a :: comm_ring_1 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
+ where "pseudo_divmod p q \<equiv>
+ if q = 0 then (0, p)
+ else
+ pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p)
+ (1 + length (coeffs p) - length (coeffs q))"
+
+lemma pseudo_divmod_main:
+ assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
+ and "degree r \<le> dr" "pseudo_divmod_main lc q r d dr n = (q',r')"
+ and "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> r = 0"
shows "(r' = 0 \<or> degree r' < degree d) \<and> smult (lc^n) (d * q + r) = d * q' + r'"
- using *
+ using assms(3-)
proof (induct n arbitrary: q r dr)
- case (Suc n q r dr)
+ case 0
+ then show ?case by auto
+next
+ case (Suc n)
let ?rr = "smult lc r"
let ?qq = "coeff r dr"
define b where [simp]: "b = monom ?qq n"
@@ -3237,158 +3307,186 @@
from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def]
have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')"
by (simp del: pseudo_divmod_main.simps)
- have dr: "dr = n + degree d" using Suc(4) by auto
+ from Suc(4) have dr: "dr = n + degree d" by auto
have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
proof (cases "?qq = 0")
+ case True
+ then show ?thesis by auto
+ next
case False
- then have n: "n = degree b" by (simp add: degree_monom_eq)
- show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum)
- qed auto
- also have "\<dots> = lc * coeff b n" unfolding d by simp
+ then have n: "n = degree b"
+ by (simp add: degree_monom_eq)
+ show ?thesis
+ unfolding n dr by (simp add: coeff_mult_degree_sum)
+ qed
+ also have "\<dots> = lc * coeff b n" by (simp add: d)
finally have "coeff (b * d) dr = lc * coeff b n" .
- moreover have "coeff ?rr dr = lc * coeff r dr" by simp
- ultimately have c0: "coeff ?rrr dr = 0" by auto
- have dr: "dr = n + degree d" using Suc(4) by auto
- have deg_rr: "degree ?rr \<le> dr" using Suc(2)
- using degree_smult_le dual_order.trans by blast
+ moreover have "coeff ?rr dr = lc * coeff r dr"
+ by simp
+ ultimately have c0: "coeff ?rrr dr = 0"
+ by auto
+ from Suc(4) have dr: "dr = n + degree d" by auto
+ have deg_rr: "degree ?rr \<le> dr"
+ using Suc(2) degree_smult_le dual_order.trans by blast
have deg_bd: "degree (b * d) \<le> dr"
- unfolding dr
- by(rule order.trans[OF degree_mult_le], auto simp: degree_monom_le)
+ unfolding dr by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le)
have "degree ?rrr \<le> dr"
using degree_diff_le[OF deg_rr deg_bd] by auto
- with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)" by (rule coeff_0_degree_minus_1)
+ with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)"
+ by (rule coeff_0_degree_minus_1)
have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
proof (cases dr)
case 0
with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
with deg_rrr have "degree ?rrr = 0" by simp
- then have "\<exists> a. ?rrr = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
- from this obtain a where rrr: "?rrr = [:a:]" by auto
- show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp
- qed (insert Suc(4), auto)
+ then have "\<exists>a. ?rrr = [:a:]"
+ by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
+ from this obtain a where rrr: "?rrr = [:a:]"
+ by auto
+ show ?thesis
+ unfolding 0 using c0 unfolding rrr 0 by simp
+ next
+ case _: Suc
+ with Suc(4) show ?thesis by auto
+ qed
note IH = Suc(1)[OF deg_rrr res this]
show ?case
proof (intro conjI)
- show "r' = 0 \<or> degree r' < degree d" using IH by blast
+ from IH show "r' = 0 \<or> degree r' < degree d"
+ by blast
show "smult (lc ^ Suc n) (d * q + r) = d * q' + r'"
unfolding IH[THEN conjunct2,symmetric]
by (simp add: field_simps smult_add_right)
qed
-qed auto
+qed
lemma pseudo_divmod:
- assumes g: "g \<noteq> 0" and *: "pseudo_divmod f g = (q,r)"
- shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is ?A)
- and "r = 0 \<or> degree r < degree g" (is ?B)
+ assumes g: "g \<noteq> 0"
+ and *: "pseudo_divmod f g = (q,r)"
+ shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is ?A)
+ and "r = 0 \<or> degree r < degree g" (is ?B)
proof -
from *[unfolded pseudo_divmod_def Let_def]
- have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (auto simp: g)
+ have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f)
+ (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
+ by (auto simp: g)
note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl]
- have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \<or>
- degree f = 0 \<and> 1 + length (coeffs f) - length (coeffs g) = 0 \<and> f = 0" using g
- by (cases "f = 0"; cases "coeffs g", auto simp: degree_eq_length_coeffs)
- note main = main[OF this]
- from main show "r = 0 \<or> degree r < degree g" by auto
+ from g have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \<or>
+ degree f = 0 \<and> 1 + length (coeffs f) - length (coeffs g) = 0 \<and> f = 0"
+ by (cases "f = 0"; cases "coeffs g") (auto simp: degree_eq_length_coeffs)
+ note main' = main[OF this]
+ then show "r = 0 \<or> degree r < degree g" by auto
show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r"
- by (subst main[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
- insert g, cases "f = 0"; cases "coeffs g", auto)
+ by (subst main'[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
+ cases "f = 0"; cases "coeffs g", use g in auto)
qed
definition "pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)"
lemma snd_pseudo_divmod_main:
"snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)"
-by (induct n arbitrary: q q' lc r d dr; simp add: Let_def)
-
-definition pseudo_mod
- :: "'a :: {comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
- "pseudo_mod f g = snd (pseudo_divmod f g)"
+ by (induct n arbitrary: q q' lc r d dr) (simp_all add: Let_def)
+
+definition pseudo_mod :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+ where "pseudo_mod f g = snd (pseudo_divmod f g)"
lemma pseudo_mod:
- fixes f g
+ fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
defines "r \<equiv> pseudo_mod f g"
assumes g: "g \<noteq> 0"
- shows "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" "r = 0 \<or> degree r < degree g"
+ shows "\<exists>a q. a \<noteq> 0 \<and> smult a f = g * q + r" "r = 0 \<or> degree r < degree g"
proof -
let ?cg = "coeff g (degree g)"
let ?cge = "?cg ^ (Suc (degree f) - degree g)"
define a where "a = ?cge"
- obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def]
- by (cases "pseudo_divmod f g", auto)
+ from r_def[unfolded pseudo_mod_def] obtain q where pdm: "pseudo_divmod f g = (q, r)"
+ by (cases "pseudo_divmod f g") auto
from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g"
- unfolding a_def by auto
+ by (auto simp: a_def)
show "r = 0 \<or> degree r < degree g" by fact
- from g have "a \<noteq> 0" unfolding a_def by auto
- then show "\<exists> a q. a \<noteq> 0 \<and> smult a f = g * q + r" using id by auto
+ from g have "a \<noteq> 0"
+ by (auto simp: a_def)
+ with id show "\<exists>a q. a \<noteq> 0 \<and> smult a f = g * q + r"
+ by auto
qed
lemma fst_pseudo_divmod_main_as_divide_poly_main:
assumes d: "d \<noteq> 0"
defines lc: "lc \<equiv> coeff d (degree d)"
- shows "fst (pseudo_divmod_main lc q r d dr n) = divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n"
-proof(induct n arbitrary: q r dr)
- case 0 then show ?case by simp
+ shows "fst (pseudo_divmod_main lc q r d dr n) =
+ divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n"
+proof (induct n arbitrary: q r dr)
+ case 0
+ then show ?case by simp
next
case (Suc n)
- note lc0 = leading_coeff_neq_0[OF d, folded lc]
- then have "pseudo_divmod_main lc q r d dr (Suc n) =
+ note lc0 = leading_coeff_neq_0[OF d, folded lc]
+ then have "pseudo_divmod_main lc q r d dr (Suc n) =
pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n)
(smult lc r - monom (coeff r dr) n * d) d (dr - 1) n"
by (simp add: Let_def ac_simps)
- also have "fst \<dots> = divide_poly_main lc
+ also have "fst \<dots> = divide_poly_main lc
(smult (lc^n) (smult lc q + monom (coeff r dr) n))
(smult (lc^n) (smult lc r - monom (coeff r dr) n * d))
d (dr - 1) n"
- unfolding Suc[unfolded divide_poly_main.simps Let_def]..
- also have "\<dots> = divide_poly_main lc (smult (lc ^ Suc n) q)
- (smult (lc ^ Suc n) r) d dr (Suc n)"
- unfolding smult_monom smult_distribs mult_smult_left[symmetric]
- using lc0 by (simp add: Let_def ac_simps)
- finally show ?case.
+ by (simp only: Suc[unfolded divide_poly_main.simps Let_def])
+ also have "\<dots> = divide_poly_main lc (smult (lc ^ Suc n) q) (smult (lc ^ Suc n) r) d dr (Suc n)"
+ unfolding smult_monom smult_distribs mult_smult_left[symmetric]
+ using lc0 by (simp add: Let_def ac_simps)
+ finally show ?case .
qed
subsubsection \<open>Division in polynomials over fields\<close>
lemma pseudo_divmod_field:
- assumes g: "(g::'a::field poly) \<noteq> 0" and *: "pseudo_divmod f g = (q,r)"
+ fixes g :: "'a::field poly"
+ assumes g: "g \<noteq> 0"
+ and *: "pseudo_divmod f g = (q,r)"
defines "c \<equiv> coeff g (degree g) ^ (Suc (degree f) - degree g)"
shows "f = g * smult (1/c) q + smult (1/c) r"
proof -
- from leading_coeff_neq_0[OF g] have c0: "c \<noteq> 0" unfolding c_def by auto
- from pseudo_divmod(1)[OF g *, folded c_def]
- have "smult c f = g * q + r" by auto
- also have "smult (1/c) \<dots> = g * smult (1/c) q + smult (1/c) r" by (simp add: smult_add_right)
- finally show ?thesis using c0 by auto
+ from leading_coeff_neq_0[OF g] have c0: "c \<noteq> 0"
+ by (auto simp: c_def)
+ from pseudo_divmod(1)[OF g *, folded c_def] have "smult c f = g * q + r"
+ by auto
+ also have "smult (1 / c) \<dots> = g * smult (1 / c) q + smult (1 / c) r"
+ by (simp add: smult_add_right)
+ finally show ?thesis
+ using c0 by auto
qed
lemma divide_poly_main_field:
- assumes d: "(d::'a::field poly) \<noteq> 0"
+ fixes d :: "'a::field poly"
+ assumes d: "d \<noteq> 0"
defines lc: "lc \<equiv> coeff d (degree d)"
- shows "divide_poly_main lc q r d dr n = fst (pseudo_divmod_main lc (smult ((1/lc)^n) q) (smult ((1/lc)^n) r) d dr n)"
- unfolding lc
- by(subst fst_pseudo_divmod_main_as_divide_poly_main, auto simp: d power_one_over)
+ shows "divide_poly_main lc q r d dr n =
+ fst (pseudo_divmod_main lc (smult ((1 / lc)^n) q) (smult ((1 / lc)^n) r) d dr n)"
+ unfolding lc by (subst fst_pseudo_divmod_main_as_divide_poly_main) (auto simp: d power_one_over)
lemma divide_poly_field:
- fixes f g :: "'a :: field poly"
+ fixes f g :: "'a::field poly"
defines "f' \<equiv> smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f"
- shows "(f::'a::field poly) div g = fst (pseudo_divmod f' g)"
+ shows "f div g = fst (pseudo_divmod f' g)"
proof (cases "g = 0")
- case True show ?thesis
- unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True by (simp add: divide_poly_main_0)
+ case True
+ show ?thesis
+ unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True
+ by (simp add: divide_poly_main_0)
next
case False
- from leading_coeff_neq_0[OF False] have "degree f' = degree f" unfolding f'_def by auto
- then show ?thesis
- using length_coeffs_degree[of f'] length_coeffs_degree[of f]
- unfolding divide_poly_def pseudo_divmod_def Let_def
- divide_poly_main_field[OF False]
- length_coeffs_degree[OF False]
- f'_def
- by force
+ from leading_coeff_neq_0[OF False] have "degree f' = degree f"
+ by (auto simp: f'_def)
+ then show ?thesis
+ using length_coeffs_degree[of f'] length_coeffs_degree[of f]
+ unfolding divide_poly_def pseudo_divmod_def Let_def
+ divide_poly_main_field[OF False]
+ length_coeffs_degree[OF False]
+ f'_def
+ by force
qed
-instantiation poly :: ("{semidom_divide_unit_factor, idom_divide}") normalization_semidom
+instantiation poly :: ("{semidom_divide_unit_factor,idom_divide}") normalization_semidom
begin
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
@@ -3397,7 +3495,8 @@
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
where "normalize p = p div [:unit_factor (lead_coeff p):]"
-instance proof
+instance
+proof
fix p :: "'a poly"
show "unit_factor p * normalize p = p"
proof (cases "p = 0")
@@ -3417,8 +3516,7 @@
have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
proof -
from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
- then show ?thesis
- using False * by simp
+ with False * show ?thesis by simp
qed
have "p div [:unit_factor (lead_coeff p):] =
map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
@@ -3435,15 +3533,15 @@
then show "unit_factor p = p"
by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
next
- fix p :: "'a poly" assume "p \<noteq> 0"
+ fix p :: "'a poly"
+ assume "p \<noteq> 0"
then show "is_unit (unit_factor p)"
by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
end
-lemma normalize_poly_eq_map_poly:
- "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+lemma normalize_poly_eq_map_poly: "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
proof -
have "[:unit_factor (lead_coeff p):] dvd p"
by (metis unit_factor_poly_def unit_factor_self)
@@ -3463,11 +3561,9 @@
proof
fix a
assume "a \<noteq> 0"
- then have "1 = a * inverse a"
- by simp
+ then have "1 = a * inverse a" by simp
then have "a dvd 1" ..
- then show "unit_factor a dvd 1"
- by simp
+ then show "unit_factor a dvd 1" by simp
qed simp_all
end
@@ -3476,12 +3572,10 @@
"unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
by (simp add: unit_factor_poly_def)
-lemma normalize_monom [simp]:
- "normalize (monom a n) = monom (normalize a) n"
+lemma normalize_monom [simp]: "normalize (monom a n) = monom (normalize a) n"
by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
-lemma unit_factor_monom [simp]:
- "unit_factor (monom a n) = [:unit_factor a:]"
+lemma unit_factor_monom [simp]: "unit_factor (monom a n) = [:unit_factor a:]"
by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
@@ -3499,32 +3593,30 @@
"smult (content p) (normalize (primitive_part p)) = normalize p"
proof -
have "smult (content p) (normalize (primitive_part p)) =
- normalize ([:content p:] * primitive_part p)"
+ normalize ([:content p:] * primitive_part p)"
by (subst normalize_mult) (simp_all add: normalize_const_poly)
also have "[:content p:] * primitive_part p = p" by simp
finally show ?thesis .
qed
inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
- where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
+ where
+ eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
| eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
- | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
- \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
+ | eucl_rel_poly_remainderI:
+ "y \<noteq> 0 \<Longrightarrow> degree r < degree y \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
lemma eucl_rel_poly_iff:
"eucl_rel_poly x y (q, r) \<longleftrightarrow>
- x = q * y + r \<and>
- (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
+ x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
by (auto elim: eucl_rel_poly.cases
- intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
-
-lemma eucl_rel_poly_0:
- "eucl_rel_poly 0 y (0, 0)"
- unfolding eucl_rel_poly_iff by simp
-
-lemma eucl_rel_poly_by_0:
- "eucl_rel_poly x 0 (0, x)"
- unfolding eucl_rel_poly_iff by simp
+ intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
+
+lemma eucl_rel_poly_0: "eucl_rel_poly 0 y (0, 0)"
+ by (simp add: eucl_rel_poly_iff)
+
+lemma eucl_rel_poly_by_0: "eucl_rel_poly x 0 (0, x)"
+ by (simp add: eucl_rel_poly_iff)
lemma eucl_rel_poly_pCons:
assumes rel: "eucl_rel_poly x y (q, r)"
@@ -3533,45 +3625,41 @@
shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
(is "eucl_rel_poly ?x y (?q, ?r)")
proof -
- have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
- using assms unfolding eucl_rel_poly_iff by simp_all
-
- have 1: "?x = ?q * y + ?r"
- using b x by simp
-
- have 2: "?r = 0 \<or> degree ?r < degree y"
+ from assms have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
+ by (simp_all add: eucl_rel_poly_iff)
+ from b x have "?x = ?q * y + ?r" by simp
+ moreover
+ have "?r = 0 \<or> degree ?r < degree y"
proof (rule eq_zero_or_degree_less)
show "degree ?r \<le> degree y"
proof (rule degree_diff_le)
- show "degree (pCons a r) \<le> degree y"
- using r by auto
+ from r show "degree (pCons a r) \<le> degree y"
+ by auto
show "degree (smult b y) \<le> degree y"
by (rule degree_smult_le)
qed
- next
- show "coeff ?r (degree y) = 0"
- using \<open>y \<noteq> 0\<close> unfolding b by simp
+ from \<open>y \<noteq> 0\<close> show "coeff ?r (degree y) = 0"
+ by (simp add: b)
qed
-
- from 1 2 show ?thesis
- unfolding eucl_rel_poly_iff
- using \<open>y \<noteq> 0\<close> by simp
+ ultimately show ?thesis
+ unfolding eucl_rel_poly_iff using \<open>y \<noteq> 0\<close> by simp
qed
lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
-apply (cases "y = 0")
-apply (fast intro!: eucl_rel_poly_by_0)
-apply (induct x)
-apply (fast intro!: eucl_rel_poly_0)
-apply (fast intro!: eucl_rel_poly_pCons)
-done
+ apply (cases "y = 0")
+ apply (fast intro!: eucl_rel_poly_by_0)
+ apply (induct x)
+ apply (fast intro!: eucl_rel_poly_0)
+ apply (fast intro!: eucl_rel_poly_pCons)
+ done
lemma eucl_rel_poly_unique:
assumes 1: "eucl_rel_poly x y (q1, r1)"
assumes 2: "eucl_rel_poly x y (q2, r2)"
shows "q1 = q2 \<and> r1 = r2"
proof (cases "y = 0")
- assume "y = 0" with assms show ?thesis
+ assume "y = 0"
+ with assms show ?thesis
by (simp add: eucl_rel_poly_iff)
next
assume [simp]: "y \<noteq> 0"
@@ -3583,27 +3671,26 @@
by (simp add: algebra_simps)
from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
by (auto intro: degree_diff_less)
-
show "q1 = q2 \<and> r1 = r2"
- proof (rule ccontr)
- assume "\<not> (q1 = q2 \<and> r1 = r2)"
+ proof (rule classical)
+ assume "\<not> ?thesis"
with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
with r3 have "degree (r2 - r1) < degree y" by simp
also have "degree y \<le> degree (q1 - q2) + degree y" by simp
- also have "\<dots> = degree ((q1 - q2) * y)"
- using \<open>q1 \<noteq> q2\<close> by (simp add: degree_mult_eq)
- also have "\<dots> = degree (r2 - r1)"
- using q3 by simp
+ also from \<open>q1 \<noteq> q2\<close> have "\<dots> = degree ((q1 - q2) * y)"
+ by (simp add: degree_mult_eq)
+ also from q3 have "\<dots> = degree (r2 - r1)"
+ by simp
finally have "degree (r2 - r1) < degree (r2 - r1)" .
- then show "False" by simp
+ then show ?thesis by simp
qed
qed
lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
-by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
+ by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
-by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
+ by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
@@ -3613,22 +3700,23 @@
begin
definition modulo_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
- where mod_poly_def: "f mod g = (if g = 0 then f
- else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)"
-
-instance proof
+ where mod_poly_def: "f mod g =
+ (if g = 0 then f else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)"
+
+instance
+proof
fix x y :: "'a poly"
show "x div y * y + x mod y = x"
proof (cases "y = 0")
- case True then show ?thesis
+ case True
+ then show ?thesis
by (simp add: divide_poly_0 mod_poly_def)
next
case False
then have "pseudo_divmod (smult ((1 / lead_coeff y) ^ (Suc (degree x) - degree y)) x) y =
- (x div y, x mod y)"
+ (x div y, x mod y)"
by (simp add: divide_poly_field mod_poly_def pseudo_mod_def)
- from pseudo_divmod [OF False this]
- show ?thesis using False
+ with False pseudo_divmod [OF False this] show ?thesis
by (simp add: power_mult_distrib [symmetric] ac_simps)
qed
qed
@@ -3636,32 +3724,34 @@
end
lemma eucl_rel_poly: "eucl_rel_poly x y (x div y, x mod y)"
-unfolding eucl_rel_poly_iff proof
+ unfolding eucl_rel_poly_iff
+proof
show "x = x div y * y + x mod y"
by (simp add: div_mult_mod_eq)
show "if y = 0 then x div y = 0 else x mod y = 0 \<or> degree (x mod y) < degree y"
proof (cases "y = 0")
- case True then show ?thesis by auto
+ case True
+ then show ?thesis by auto
next
case False
- with pseudo_mod[OF this] show ?thesis unfolding mod_poly_def by simp
+ with pseudo_mod[OF this] show ?thesis
+ by (simp add: mod_poly_def)
qed
qed
-lemma div_poly_eq:
- "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
- by(rule eucl_rel_poly_unique_div [OF eucl_rel_poly])
-
-lemma mod_poly_eq:
- "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
+lemma div_poly_eq: "eucl_rel_poly x y (q, r) \<Longrightarrow> x div y = q"
+ for x :: "'a::field poly"
+ by (rule eucl_rel_poly_unique_div [OF eucl_rel_poly])
+
+lemma mod_poly_eq: "eucl_rel_poly x y (q, r) \<Longrightarrow> x mod y = r"
+ for x :: "'a::field poly"
by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
instance poly :: (field) ring_div
proof
fix x y z :: "'a poly"
assume "y \<noteq> 0"
- then have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
- using eucl_rel_poly [of x y]
+ with eucl_rel_poly [of x y] have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
by (simp add: eucl_rel_poly_iff distrib_right)
then show "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
@@ -3678,84 +3768,88 @@
by (rule eucl_rel_poly_0)
then have [simp]: "\<And>x::'a poly. 0 div x = 0"
by (rule div_poly_eq)
- case False then show ?thesis by auto
+ case False
+ then show ?thesis by auto
next
- case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
- with \<open>x \<noteq> 0\<close>
- have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
- by (auto simp add: eucl_rel_poly_iff algebra_simps)
- (rule classical, simp add: degree_mult_eq)
+ case True
+ then have "y \<noteq> 0" and "z \<noteq> 0" by auto
+ with \<open>x \<noteq> 0\<close> have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
+ by (auto simp: eucl_rel_poly_iff algebra_simps) (rule classical, simp add: degree_mult_eq)
moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
- then show ?thesis by (simp add: div_poly_eq)
+ then show ?thesis
+ by (simp add: div_poly_eq)
qed
qed
lemma div_pCons_eq:
- "pCons a p div q = (if q = 0 then 0
- else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q)
- (p div q))"
+ "pCons a p div q =
+ (if q = 0 then 0
+ else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) (p div q))"
using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p]
by (auto intro: div_poly_eq)
lemma mod_pCons_eq:
- "pCons a p mod q = (if q = 0 then pCons a p
- else pCons a (p mod q) - smult (coeff (pCons a (p mod q)) (degree q) / lead_coeff q)
- q)"
+ "pCons a p mod q =
+ (if q = 0 then pCons a p
+ else pCons a (p mod q) - smult (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) q)"
using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p]
by (auto intro: mod_poly_eq)
lemma div_mod_fold_coeffs:
- "(p div q, p mod q) = (if q = 0 then (0, p)
- else fold_coeffs (\<lambda>a (s, r).
- let b = coeff (pCons a r) (degree q) / coeff q (degree q)
- in (pCons b s, pCons a r - smult b q)
- ) p (0, 0))"
- by (rule sym, induct p) (auto simp add: div_pCons_eq mod_pCons_eq Let_def)
-
-lemma degree_mod_less:
- "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
- using eucl_rel_poly [of x y]
- unfolding eucl_rel_poly_iff by simp
+ "(p div q, p mod q) =
+ (if q = 0 then (0, p)
+ else
+ fold_coeffs
+ (\<lambda>a (s, r).
+ let b = coeff (pCons a r) (degree q) / coeff q (degree q)
+ in (pCons b s, pCons a r - smult b q)) p (0, 0))"
+ by (rule sym, induct p) (auto simp: div_pCons_eq mod_pCons_eq Let_def)
+
+lemma degree_mod_less: "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
+ using eucl_rel_poly [of x y] unfolding eucl_rel_poly_iff by simp
lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
using degree_mod_less[of b a] by auto
-lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
+lemma div_poly_less:
+ fixes x :: "'a::field poly"
+ assumes "degree x < degree y"
+ shows "x div y = 0"
proof -
- assume "degree x < degree y"
- then have "eucl_rel_poly x y (0, x)"
+ from assms have "eucl_rel_poly x y (0, x)"
by (simp add: eucl_rel_poly_iff)
- then show "x div y = 0" by (rule div_poly_eq)
+ then show "x div y = 0"
+ by (rule div_poly_eq)
qed
-lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
+lemma mod_poly_less:
+ assumes "degree x < degree y"
+ shows "x mod y = x"
proof -
- assume "degree x < degree y"
- then have "eucl_rel_poly x y (0, x)"
+ from assms have "eucl_rel_poly x y (0, x)"
by (simp add: eucl_rel_poly_iff)
- then show "x mod y = x" by (rule mod_poly_eq)
+ then show "x mod y = x"
+ by (rule mod_poly_eq)
qed
lemma eucl_rel_poly_smult_left:
- "eucl_rel_poly x y (q, r)
- \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
- unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
-
-lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
+ "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
+ by (simp add: eucl_rel_poly_iff smult_add_right)
+
+lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
+ for x y :: "'a::field poly"
by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
-lemma poly_div_minus_left [simp]:
- fixes x y :: "'a::field poly"
- shows "(- x) div y = - (x div y)"
+lemma poly_div_minus_left [simp]: "(- x) div y = - (x div y)"
+ for x y :: "'a::field poly"
using div_smult_left [of "- 1::'a"] by simp
-lemma poly_mod_minus_left [simp]:
- fixes x y :: "'a::field poly"
- shows "(- x) mod y = - (x mod y)"
+lemma poly_mod_minus_left [simp]: "(- x) mod y = - (x mod y)"
+ for x y :: "'a::field poly"
using mod_smult_left [of "- 1::'a"] by simp
lemma eucl_rel_poly_add_left:
@@ -3763,86 +3857,76 @@
assumes "eucl_rel_poly x' y (q', r')"
shows "eucl_rel_poly (x + x') y (q + q', r + r')"
using assms unfolding eucl_rel_poly_iff
- by (auto simp add: algebra_simps degree_add_less)
-
-lemma poly_div_add_left:
- fixes x y z :: "'a::field poly"
- shows "(x + y) div z = x div z + y div z"
+ by (auto simp: algebra_simps degree_add_less)
+
+lemma poly_div_add_left: "(x + y) div z = x div z + y div z"
+ for x y z :: "'a::field poly"
using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
by (rule div_poly_eq)
-lemma poly_mod_add_left:
- fixes x y z :: "'a::field poly"
- shows "(x + y) mod z = x mod z + y mod z"
+lemma poly_mod_add_left: "(x + y) mod z = x mod z + y mod z"
+ for x y z :: "'a::field poly"
using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
by (rule mod_poly_eq)
-lemma poly_div_diff_left:
- fixes x y z :: "'a::field poly"
- shows "(x - y) div z = x div z - y div z"
+lemma poly_div_diff_left: "(x - y) div z = x div z - y div z"
+ for x y z :: "'a::field poly"
by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
-lemma poly_mod_diff_left:
- fixes x y z :: "'a::field poly"
- shows "(x - y) mod z = x mod z - y mod z"
+lemma poly_mod_diff_left: "(x - y) mod z = x mod z - y mod z"
+ for x y z :: "'a::field poly"
by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
lemma eucl_rel_poly_smult_right:
- "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
- \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
- unfolding eucl_rel_poly_iff by simp
-
-lemma div_smult_right:
- "(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
+ "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
+ by (simp add: eucl_rel_poly_iff)
+
+lemma div_smult_right: "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
+ for x y :: "'a::field poly"
by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
-lemma poly_div_minus_right [simp]:
- fixes x y :: "'a::field poly"
- shows "x div (- y) = - (x div y)"
+lemma poly_div_minus_right [simp]: "x div (- y) = - (x div y)"
+ for x y :: "'a::field poly"
using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
-lemma poly_mod_minus_right [simp]:
- fixes x y :: "'a::field poly"
- shows "x mod (- y) = x mod y"
+lemma poly_mod_minus_right [simp]: "x mod (- y) = x mod y"
+ for x y :: "'a::field poly"
using mod_smult_right [of "- 1::'a"] by simp
lemma eucl_rel_poly_mult:
- "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
- \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
-apply (cases "z = 0", simp add: eucl_rel_poly_iff)
-apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
-apply (cases "r = 0")
-apply (cases "r' = 0")
-apply (simp add: eucl_rel_poly_iff)
-apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
-apply (cases "r' = 0")
-apply (simp add: eucl_rel_poly_iff degree_mult_eq)
-apply (simp add: eucl_rel_poly_iff field_simps)
-apply (simp add: degree_mult_eq degree_add_less)
-done
-
-lemma poly_div_mult_right:
- fixes x y z :: "'a::field poly"
- shows "x div (y * z) = (x div y) div z"
+ "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r') \<Longrightarrow>
+ eucl_rel_poly x (y * z) (q', y * r' + r)"
+ apply (cases "z = 0", simp add: eucl_rel_poly_iff)
+ apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
+ apply (cases "r = 0")
+ apply (cases "r' = 0")
+ apply (simp add: eucl_rel_poly_iff)
+ apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
+ apply (cases "r' = 0")
+ apply (simp add: eucl_rel_poly_iff degree_mult_eq)
+ apply (simp add: eucl_rel_poly_iff field_simps)
+ apply (simp add: degree_mult_eq degree_add_less)
+ done
+
+lemma poly_div_mult_right: "x div (y * z) = (x div y) div z"
+ for x y z :: "'a::field poly"
by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
-lemma poly_mod_mult_right:
- fixes x y z :: "'a::field poly"
- shows "x mod (y * z) = y * (x div y mod z) + x mod y"
+lemma poly_mod_mult_right: "x mod (y * z) = y * (x div y mod z) + x mod y"
+ for x y z :: "'a::field poly"
by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
lemma mod_pCons:
- fixes a and x
+ fixes a :: "'a::field"
+ and x y :: "'a::field poly"
assumes y: "y \<noteq> 0"
- defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
- shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
-unfolding b
-apply (rule mod_poly_eq)
-apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
-done
+ defines "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
+ shows "(pCons a x) mod y = pCons a (x mod y) - smult b y"
+ unfolding b_def
+ by (rule mod_poly_eq, rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
subsubsection \<open>List-based versions for fast implementation\<close>
@@ -3851,352 +3935,421 @@
René Thiemann
Akihisa Yamada
*)
-fun minus_poly_rev_list :: "'a :: group_add list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
-| "minus_poly_rev_list xs [] = xs"
-| "minus_poly_rev_list [] (y # ys) = []"
-
-fun pseudo_divmod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list
- \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
- "pseudo_divmod_main_list lc q r d (Suc n) = (let
- rr = map (op * lc) r;
- a = hd r;
- qqq = cCons a (map (op * lc) q);
- rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
- in pseudo_divmod_main_list lc qqq rrr d n)"
-| "pseudo_divmod_main_list lc q r d 0 = (q,r)"
-
-fun pseudo_mod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list
- \<Rightarrow> nat \<Rightarrow> 'a list" where
- "pseudo_mod_main_list lc r d (Suc n) = (let
- rr = map (op * lc) r;
- a = hd r;
- rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
- in pseudo_mod_main_list lc rrr d n)"
-| "pseudo_mod_main_list lc r d 0 = r"
-
-
-fun divmod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list
- \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list" where
- "divmod_poly_one_main_list q r d (Suc n) = (let
- a = hd r;
- qqq = cCons a q;
- rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
- in divmod_poly_one_main_list qqq rr d n)"
-| "divmod_poly_one_main_list q r d 0 = (q,r)"
-
-fun mod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list
- \<Rightarrow> nat \<Rightarrow> 'a list" where
- "mod_poly_one_main_list r d (Suc n) = (let
- a = hd r;
- rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
- in mod_poly_one_main_list rr d n)"
-| "mod_poly_one_main_list r d 0 = r"
-
-definition pseudo_divmod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list" where
- "pseudo_divmod_list p q =
- (if q = [] then ([],p) else
- (let rq = rev q;
- (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in
- (qu,rev re)))"
-
-definition pseudo_mod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "pseudo_mod_list p q =
- (if q = [] then p else
- (let rq = rev q;
- re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in
- (rev re)))"
-
-lemma minus_zero_does_nothing:
-"(minus_poly_rev_list x (map (op * 0) y)) = (x :: 'a :: ring list)"
- by(induct x y rule: minus_poly_rev_list.induct, auto)
-
-lemma length_minus_poly_rev_list[simp]:
- "length (minus_poly_rev_list xs ys) = length xs"
- by(induct xs ys rule: minus_poly_rev_list.induct, auto)
+fun minus_poly_rev_list :: "'a :: group_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ where
+ "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
+ | "minus_poly_rev_list xs [] = xs"
+ | "minus_poly_rev_list [] (y # ys) = []"
+
+fun pseudo_divmod_main_list ::
+ "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list"
+ where
+ "pseudo_divmod_main_list lc q r d (Suc n) =
+ (let
+ rr = map (op * lc) r;
+ a = hd r;
+ qqq = cCons a (map (op * lc) q);
+ rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
+ in pseudo_divmod_main_list lc qqq rrr d n)"
+ | "pseudo_divmod_main_list lc q r d 0 = (q, r)"
+
+fun pseudo_mod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
+ where
+ "pseudo_mod_main_list lc r d (Suc n) =
+ (let
+ rr = map (op * lc) r;
+ a = hd r;
+ rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
+ in pseudo_mod_main_list lc rrr d n)"
+ | "pseudo_mod_main_list lc r d 0 = r"
+
+
+fun divmod_poly_one_main_list ::
+ "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list"
+ where
+ "divmod_poly_one_main_list q r d (Suc n) =
+ (let
+ a = hd r;
+ qqq = cCons a q;
+ rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
+ in divmod_poly_one_main_list qqq rr d n)"
+ | "divmod_poly_one_main_list q r d 0 = (q, r)"
+
+fun mod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
+ where
+ "mod_poly_one_main_list r d (Suc n) =
+ (let
+ a = hd r;
+ rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
+ in mod_poly_one_main_list rr d n)"
+ | "mod_poly_one_main_list r d 0 = r"
+
+definition pseudo_divmod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list"
+ where "pseudo_divmod_list p q =
+ (if q = [] then ([], p)
+ else
+ (let rq = rev q;
+ (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q)
+ in (qu, rev re)))"
+
+definition pseudo_mod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ where "pseudo_mod_list p q =
+ (if q = [] then p
+ else
+ (let
+ rq = rev q;
+ re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q)
+ in rev re))"
+
+lemma minus_zero_does_nothing: "minus_poly_rev_list x (map (op * 0) y) = x"
+ for x :: "'a::ring list"
+ by (induct x y rule: minus_poly_rev_list.induct) auto
+
+lemma length_minus_poly_rev_list [simp]: "length (minus_poly_rev_list xs ys) = length xs"
+ by (induct xs ys rule: minus_poly_rev_list.induct) auto
lemma if_0_minus_poly_rev_list:
- "(if a = 0 then x else minus_poly_rev_list x (map (op * a) y))
- = minus_poly_rev_list x (map (op * (a :: 'a :: ring)) y)"
- by(cases "a=0",simp_all add:minus_zero_does_nothing)
-
-lemma Poly_append:
- "Poly ((a::'a::comm_semiring_1 list) @ b) = Poly a + monom 1 (length a) * Poly b"
- by (induct a,auto simp: monom_0 monom_Suc)
-
-lemma minus_poly_rev_list: "length p \<ge> length (q :: 'a :: comm_ring_1 list) \<Longrightarrow>
- Poly (rev (minus_poly_rev_list (rev p) (rev q)))
- = Poly p - monom 1 (length p - length q) * Poly q"
+ "(if a = 0 then x else minus_poly_rev_list x (map (op * a) y)) =
+ minus_poly_rev_list x (map (op * a) y)"
+ for a :: "'a::ring"
+ by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
+
+lemma Poly_append: "Poly (a @ b) = Poly a + monom 1 (length a) * Poly b"
+ for a :: "'a::comm_semiring_1 list"
+ by (induct a) (auto simp: monom_0 monom_Suc)
+
+lemma minus_poly_rev_list: "length p \<ge> length q \<Longrightarrow>
+ Poly (rev (minus_poly_rev_list (rev p) (rev q))) =
+ Poly p - monom 1 (length p - length q) * Poly q"
+ for p q :: "'a :: comm_ring_1 list"
proof (induct "rev p" "rev q" arbitrary: p q rule: minus_poly_rev_list.induct)
case (1 x xs y ys)
- have "length (rev q) \<le> length (rev p)" using 1 by simp
- from this[folded 1(2,3)] have ys_xs:"length ys \<le> length xs" by simp
- then have a:"Poly (rev (minus_poly_rev_list xs ys)) =
- Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)"
- by(subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev],auto)
- have "Poly p - monom 1 (length p - length q) * Poly q
- = Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))"
+ then have "length (rev q) \<le> length (rev p)"
+ by simp
+ from this[folded 1(2,3)] have ys_xs: "length ys \<le> length xs"
+ by simp
+ then have *: "Poly (rev (minus_poly_rev_list xs ys)) =
+ Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)"
+ by (subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev]) auto
+ have "Poly p - monom 1 (length p - length q) * Poly q =
+ Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))"
by simp
- also have "\<dots> = Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))"
+ also have "\<dots> =
+ Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))"
unfolding 1(2,3) by simp
- also have "\<dots> = Poly (rev xs) + monom x (length xs) -
- (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))" using ys_xs
- by (simp add:Poly_append distrib_left mult_monom smult_monom)
+ also from ys_xs have "\<dots> =
+ Poly (rev xs) + monom x (length xs) -
+ (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))"
+ by (simp add: Poly_append distrib_left mult_monom smult_monom)
also have "\<dots> = Poly (rev (minus_poly_rev_list xs ys)) + monom (x - y) (length xs)"
- unfolding a diff_monom[symmetric] by(simp)
+ unfolding * diff_monom[symmetric] by simp
finally show ?case
- unfolding 1(2,3)[symmetric] by (simp add: smult_monom Poly_append)
+ by (simp add: 1(2,3)[symmetric] smult_monom Poly_append)
qed auto
lemma smult_monom_mult: "smult a (monom b n * f) = monom (a * b) n * f"
using smult_monom [of a _ n] by (metis mult_smult_left)
lemma head_minus_poly_rev_list:
- "length d \<le> length r \<Longrightarrow> d\<noteq>[] \<Longrightarrow>
- hd (minus_poly_rev_list (map (op * (last d :: 'a :: comm_ring)) r) (map (op * (hd r)) (rev d))) = 0"
-proof(induct r)
+ "length d \<le> length r \<Longrightarrow> d \<noteq> [] \<Longrightarrow>
+ hd (minus_poly_rev_list (map (op * (last d)) r) (map (op * (hd r)) (rev d))) = 0"
+ for d r :: "'a::comm_ring list"
+proof (induct r)
+ case Nil
+ then show ?case by simp
+next
case (Cons a rs)
- then show ?case by(cases "rev d", simp_all add:ac_simps)
-qed simp
+ then show ?case by (cases "rev d") (simp_all add: ac_simps)
+qed
lemma Poly_map: "Poly (map (op * a) p) = smult a (Poly p)"
proof (induct p)
- case(Cons x xs) then show ?case by (cases "Poly xs = 0",auto)
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case (Cons x xs)
+ then show ?case by (cases "Poly xs = 0") auto
+qed
lemma last_coeff_is_hd: "xs \<noteq> [] \<Longrightarrow> coeff (Poly xs) (length xs - 1) = hd (rev xs)"
by (simp_all add: hd_conv_nth rev_nth nth_default_nth nth_append)
-lemma pseudo_divmod_main_list_invar :
- assumes leading_nonzero:"last d \<noteq> 0"
- and lc:"last d = lc"
- and dNonempty:"d \<noteq> []"
- and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q',rev r')"
- and "n = (1 + length r - length d)"
- shows
- "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n =
- (Poly q', Poly r')"
-using assms(4-)
-proof(induct "n" arbitrary: r q)
-case (Suc n r q)
- have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
- have rNonempty:"r \<noteq> []"
- using ifCond dNonempty using Suc_leI length_greater_0_conv list.size(3) by fastforce
+lemma pseudo_divmod_main_list_invar:
+ assumes leading_nonzero: "last d \<noteq> 0"
+ and lc: "last d = lc"
+ and "d \<noteq> []"
+ and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q', rev r')"
+ and "n = 1 + length r - length d"
+ shows "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n =
+ (Poly q', Poly r')"
+ using assms(4-)
+proof (induct n arbitrary: r q)
+ case (Suc n)
+ from Suc.prems have *: "\<not> Suc (length r) \<le> length d"
+ by simp
+ with \<open>d \<noteq> []\<close> have "r \<noteq> []"
+ using Suc_leI length_greater_0_conv list.size(3) by fastforce
let ?a = "(hd (rev r))"
let ?rr = "map (op * lc) (rev r)"
let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (op * ?a) (rev d))))"
let ?qq = "cCons ?a (map (op * lc) q)"
- have n: "n = (1 + length r - length d - 1)"
- using ifCond Suc(3) by simp
- have rr_val:"(length ?rrr) = (length r - 1)" using ifCond by auto
- then have rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)"
- using rNonempty ifCond unfolding One_nat_def by auto
- from ifCond have id: "Suc (length r) - length d = Suc (length r - length d)" by auto
+ from * Suc(3) have n: "n = (1 + length r - length d - 1)"
+ by simp
+ from * have rr_val:"(length ?rrr) = (length r - 1)"
+ by auto
+ with \<open>r \<noteq> []\<close> * have rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)"
+ by auto
+ from * have id: "Suc (length r) - length d = Suc (length r - length d)"
+ by auto
+ from Suc.prems *
have "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')"
- using Suc.prems ifCond by (simp add:Let_def if_0_minus_poly_rev_list id)
- then have v:"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')"
- using n by auto
- have sucrr:"Suc (length r) - length d = Suc (length r - length d)"
- using Suc_diff_le ifCond not_less_eq_eq by blast
- have n_ok : "n = 1 + (length ?rrr) - length d" using Suc(3) rNonempty by simp
+ by (simp add: Let_def if_0_minus_poly_rev_list id)
+ with n have v: "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')"
+ by auto
+ from * have sucrr:"Suc (length r) - length d = Suc (length r - length d)"
+ using Suc_diff_le not_less_eq_eq by blast
+ from Suc(3) \<open>r \<noteq> []\<close> have n_ok : "n = 1 + (length ?rrr) - length d"
+ by simp
have cong: "\<And>x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
- pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n" by simp
- have hd_rev:"coeff (Poly r) (length r - Suc 0) = hd (rev r)"
- using last_coeff_is_hd[OF rNonempty] by simp
- show ?case unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def
+ pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n"
+ by simp
+ have hd_rev: "coeff (Poly r) (length r - Suc 0) = hd (rev r)"
+ using last_coeff_is_hd[OF \<open>r \<noteq> []\<close>] by simp
+ show ?case
+ unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def
proof (rule cong[OF _ _ refl], goal_cases)
case 1
- show ?case unfolding monom_Suc hd_rev[symmetric]
- by (simp add: smult_monom Poly_map)
+ show ?case
+ by (simp add: monom_Suc hd_rev[symmetric] smult_monom Poly_map)
next
case 2
show ?case
proof (subst Poly_on_rev_starting_with_0, goal_cases)
show "hd (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))) = 0"
- by (fold lc, subst head_minus_poly_rev_list, insert ifCond dNonempty,auto)
- from ifCond have "length d \<le> length r" by simp
+ by (fold lc, subst head_minus_poly_rev_list, insert * \<open>d \<noteq> []\<close>, auto)
+ from * have "length d \<le> length r"
+ by simp
then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
- Poly (rev (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))))"
+ Poly (rev (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))))"
by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
- minus_poly_rev_list)
+ minus_poly_rev_list)
qed
qed simp
qed simp
lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g =
map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
-proof (cases "g=0")
-case False
- then have coeffs_g_nonempty:"(coeffs g) \<noteq> []" by simp
- then have lastcoeffs:"last (coeffs g) = coeff g (degree g)"
+proof (cases "g = 0")
+ case False
+ then have coeffs_g_nonempty:"(coeffs g) \<noteq> []"
+ by simp
+ then have lastcoeffs: "last (coeffs g) = coeff g (degree g)"
by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil)
- obtain q r where qr: "pseudo_divmod_main_list
- (last (coeffs g)) (rev [])
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) -
- length (coeffs g)) = (q,rev (rev r))" by force
- then have qr': "pseudo_divmod_main_list
- (hd (rev (coeffs g))) []
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) -
- length (coeffs g)) = (q,r)" using hd_rev[OF coeffs_g_nonempty] by(auto)
- from False have cg: "(coeffs g = []) = False" by auto
- have last_non0:"last (coeffs g) \<noteq> 0" using False by (simp add:last_coeffs_not_0)
- show ?thesis
+ obtain q r where qr:
+ "pseudo_divmod_main_list
+ (last (coeffs g)) (rev [])
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) - length (coeffs g)) = (q, rev (rev r))"
+ by force
+ then have qr':
+ "pseudo_divmod_main_list
+ (hd (rev (coeffs g))) []
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
+ using hd_rev[OF coeffs_g_nonempty] by auto
+ from False have cg: "coeffs g = [] \<longleftrightarrow> False"
+ by auto
+ from False have last_non0: "last (coeffs g) \<noteq> 0"
+ by (simp add: last_coeffs_not_0)
+ from False show ?thesis
unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False
pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False]
poly_of_list_def
- using False by (auto simp: degree_eq_length_coeffs)
+ by (auto simp: degree_eq_length_coeffs)
next
case True
- show ?thesis unfolding True unfolding pseudo_divmod_def pseudo_divmod_list_def
- by auto
+ then show ?thesis
+ by (auto simp: pseudo_divmod_def pseudo_divmod_list_def)
qed
-lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q
- xs ys n) = pseudo_mod_main_list l xs ys n"
- by (induct n arbitrary: l q xs ys, auto simp: Let_def)
-
-lemma pseudo_mod_impl[code]: "pseudo_mod f g =
- poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))"
+lemma pseudo_mod_main_list:
+ "snd (pseudo_divmod_main_list l q xs ys n) = pseudo_mod_main_list l xs ys n"
+ by (induct n arbitrary: l q xs ys) (auto simp: Let_def)
+
+lemma pseudo_mod_impl[code]: "pseudo_mod f g = poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))"
proof -
have snd_case: "\<And>f g p. snd ((\<lambda>(x,y). (f x, g y)) p) = g (snd p)"
by auto
show ?thesis
- unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
- pseudo_mod_list_def Let_def
- by (simp add: snd_case pseudo_mod_main_list)
+ unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
+ pseudo_mod_list_def Let_def
+ by (simp add: snd_case pseudo_mod_main_list)
qed
-(* *************** *)
subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> (p div q, p mod q) = (r, s)"
by (metis eucl_rel_poly eucl_rel_poly_unique)
-lemma pdivmod_via_pseudo_divmod: "(f div g, f mod g) = (if g = 0 then (0,f)
- else let
- ilc = inverse (coeff g (degree g));
- h = smult ilc g;
- (q,r) = pseudo_divmod f h
- in (smult ilc q, r))" (is "?l = ?r")
+lemma pdivmod_via_pseudo_divmod:
+ "(f div g, f mod g) =
+ (if g = 0 then (0, f)
+ else
+ let
+ ilc = inverse (coeff g (degree g));
+ h = smult ilc g;
+ (q,r) = pseudo_divmod f h
+ in (smult ilc q, r))"
+ (is "?l = ?r")
proof (cases "g = 0")
+ case True
+ then show ?thesis by simp
+next
case False
define lc where "lc = inverse (coeff g (degree g))"
define h where "h = smult lc g"
- from False have h1: "coeff h (degree h) = 1" and lc: "lc \<noteq> 0" unfolding h_def lc_def by auto
- then have h0: "h \<noteq> 0" by auto
- obtain q r where p: "pseudo_divmod f h = (q,r)" by force
+ from False have h1: "coeff h (degree h) = 1" and lc: "lc \<noteq> 0"
+ by (auto simp: h_def lc_def)
+ then have h0: "h \<noteq> 0"
+ by auto
+ obtain q r where p: "pseudo_divmod f h = (q, r)"
+ by force
from False have id: "?r = (smult lc q, r)"
- unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
+ by (auto simp: Let_def h_def[symmetric] lc_def[symmetric] p)
from pseudo_divmod[OF h0 p, unfolded h1]
- have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
- have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
- then have "(f div h, f mod h) = (q,r)" by (simp add: pdivmod_pdivmodrel)
- then have "(f div g, f mod g) = (smult lc q, r)"
- unfolding h_def div_smult_right[OF lc] mod_smult_right[OF lc]
- using lc by auto
- with id show ?thesis by auto
-qed simp
-
-lemma pdivmod_via_pseudo_divmod_list: "(f div g, f mod g) = (let
- cg = coeffs g
- in if cg = [] then (0,f)
- else let
- cf = coeffs f;
- ilc = inverse (last cg);
- ch = map (op * ilc) cg;
- (q,r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
- in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))"
+ have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h"
+ by auto
+ from f r h0 have "eucl_rel_poly f h (q, r)"
+ by (auto simp: eucl_rel_poly_iff)
+ then have "(f div h, f mod h) = (q, r)"
+ by (simp add: pdivmod_pdivmodrel)
+ with lc have "(f div g, f mod g) = (smult lc q, r)"
+ by (auto simp: h_def div_smult_right[OF lc] mod_smult_right[OF lc])
+ with id show ?thesis
+ by auto
+qed
+
+lemma pdivmod_via_pseudo_divmod_list:
+ "(f div g, f mod g) =
+ (let cg = coeffs g in
+ if cg = [] then (0, f)
+ else
+ let
+ cf = coeffs f;
+ ilc = inverse (last cg);
+ ch = map (op * ilc) cg;
+ (q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
+ in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))"
proof -
- note d = pdivmod_via_pseudo_divmod
- pseudo_divmod_impl pseudo_divmod_list_def
+ note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def
show ?thesis
proof (cases "g = 0")
- case True then show ?thesis unfolding d by auto
+ case True
+ with d show ?thesis by auto
next
case False
define ilc where "ilc = inverse (coeff g (degree g))"
- from False have ilc: "ilc \<noteq> 0" unfolding ilc_def by auto
- with False have id: "(g = 0) = False" "(coeffs g = []) = False"
+ from False have ilc: "ilc \<noteq> 0"
+ by (auto simp: ilc_def)
+ with False have id: "g = 0 \<longleftrightarrow> False" "coeffs g = [] \<longleftrightarrow> False"
"last (coeffs g) = coeff g (degree g)"
- "(coeffs (smult ilc g) = []) = False"
+ "coeffs (smult ilc g) = [] \<longleftrightarrow> False"
by (auto simp: last_coeffs_eq_coeff_degree)
have id2: "hd (rev (coeffs (smult ilc g))) = 1"
by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
have id3: "length (coeffs (smult ilc g)) = length (coeffs g)"
- "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))" unfolding coeffs_smult using ilc by auto
- obtain q r where pair: "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g)))
- (1 + length (coeffs f) - length (coeffs g)) = (q,r)" by force
- show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2
- unfolding id3 pair map_prod_def split by (auto simp: Poly_map)
+ "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))"
+ unfolding coeffs_smult using ilc by auto
+ obtain q r where pair:
+ "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g)))
+ (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
+ by force
+ show ?thesis
+ unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2
+ unfolding id3 pair map_prod_def split
+ by (auto simp: Poly_map)
qed
qed
lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
proof (intro ext, goal_cases)
case (1 q r d n)
- {
- fix xs :: "'a list"
- have "map (op * 1) xs = xs" by (induct xs, auto)
- } note [simp] = this
- show ?case by (induct n arbitrary: q r d, auto simp: Let_def)
+ have *: "map (op * 1) xs = xs" for xs :: "'a list"
+ by (induct xs) auto
+ show ?case
+ by (induct n arbitrary: q r d) (auto simp: * Let_def)
qed
-fun divide_poly_main_list :: "'a::idom_divide \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list
- \<Rightarrow> nat \<Rightarrow> 'a list" where
- "divide_poly_main_list lc q r d (Suc n) = (let
- cr = hd r
- in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
- a = cr div lc;
- qq = cCons a q;
- rr = minus_poly_rev_list r (map (op * a) d)
- in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
-| "divide_poly_main_list lc q r d 0 = q"
-
-lemma divide_poly_main_list_simp[simp]: "divide_poly_main_list lc q r d (Suc n) = (let
- cr = hd r;
- a = cr div lc;
- qq = cCons a q;
- rr = minus_poly_rev_list r (map (op * a) d)
+fun divide_poly_main_list :: "'a::idom_divide \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
+ where
+ "divide_poly_main_list lc q r d (Suc n) =
+ (let
+ cr = hd r
+ in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
+ a = cr div lc;
+ qq = cCons a q;
+ rr = minus_poly_rev_list r (map (op * a) d)
+ in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
+ | "divide_poly_main_list lc q r d 0 = q"
+
+lemma divide_poly_main_list_simp [simp]:
+ "divide_poly_main_list lc q r d (Suc n) =
+ (let
+ cr = hd r;
+ a = cr div lc;
+ qq = cCons a q;
+ rr = minus_poly_rev_list r (map (op * a) d)
in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
by (simp add: Let_def minus_zero_does_nothing)
declare divide_poly_main_list.simps(1)[simp del]
-definition divide_poly_list :: "'a::idom_divide poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
- "divide_poly_list f g =
- (let cg = coeffs g
- in if cg = [] then g
- else let cf = coeffs f; cgr = rev cg
- in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
+definition divide_poly_list :: "'a::idom_divide poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+ where "divide_poly_list f g =
+ (let cg = coeffs g in
+ if cg = [] then g
+ else
+ let
+ cf = coeffs f;
+ cgr = rev cg
+ in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
lemmas pdivmod_via_divmod_list = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1]
lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n"
- by (induct n arbitrary: q r d, auto simp: Let_def)
-
-lemma mod_poly_code[code]: "f mod g =
- (let cg = coeffs g
- in if cg = [] then f
- else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
- r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
- in poly_of_list (rev r))" (is "?l = ?r")
+ by (induct n arbitrary: q r d) (auto simp: Let_def)
+
+lemma mod_poly_code [code]:
+ "f mod g =
+ (let cg = coeffs g in
+ if cg = [] then f
+ else
+ let
+ cf = coeffs f;
+ ilc = inverse (last cg);
+ ch = map (op * ilc) cg;
+ r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
+ in poly_of_list (rev r))"
+ (is "_ = ?rhs")
proof -
- have "snd (f div g, f mod g) = ?r" unfolding pdivmod_via_divmod_list Let_def
- mod_poly_one_main_list [symmetric, of _ _ _ Nil] by (auto split: prod.splits)
- then show ?thesis
- by simp
+ have "snd (f div g, f mod g) = ?rhs"
+ unfolding pdivmod_via_divmod_list Let_def mod_poly_one_main_list [symmetric, of _ _ _ Nil]
+ by (auto split: prod.splits)
+ then show ?thesis by simp
qed
-definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
- "div_field_poly_impl f g = (
- let cg = coeffs g
- in if cg = [] then 0
- else let cf = coeffs f; ilc = inverse (last cg); ch = map (op * ilc) cg;
- q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
- in poly_of_list ((map (op * ilc) q)))"
+definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+ where "div_field_poly_impl f g =
+ (let cg = coeffs g in
+ if cg = [] then 0
+ else
+ let
+ cf = coeffs f;
+ ilc = inverse (last cg);
+ ch = map (op * ilc) cg;
+ q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
+ in poly_of_list ((map (op * ilc) q)))"
text \<open>We do not declare the following lemma as code equation, since then polynomial division
on non-fields will no longer be executable. However, a code-unfold is possible, since
@@ -4204,53 +4357,60 @@
lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl"
proof (intro ext)
fix f g :: "'a poly"
- have "fst (f div g, f mod g) = div_field_poly_impl f g" unfolding
- div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits)
+ have "fst (f div g, f mod g) = div_field_poly_impl f g"
+ unfolding div_field_poly_impl_def pdivmod_via_divmod_list Let_def
+ by (auto split: prod.splits)
then show "f div g = div_field_poly_impl f g"
by simp
qed
lemma divide_poly_main_list:
assumes lc0: "lc \<noteq> 0"
- and lc:"last d = lc"
- and d:"d \<noteq> []"
- and "n = (1 + length r - length d)"
- shows
- "Poly (divide_poly_main_list lc q (rev r) (rev d) n) =
- divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n"
-using assms(4-)
-proof(induct "n" arbitrary: r q)
-case (Suc n r q)
- have ifCond: "\<not> Suc (length r) \<le> length d" using Suc.prems by simp
- have r: "r \<noteq> []"
- using ifCond d using Suc_leI length_greater_0_conv list.size(3) by fastforce
- then obtain rr lcr where r: "r = rr @ [lcr]" by (cases r rule: rev_cases, auto)
+ and lc: "last d = lc"
+ and d: "d \<noteq> []"
+ and "n = (1 + length r - length d)"
+ shows "Poly (divide_poly_main_list lc q (rev r) (rev d) n) =
+ divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n"
+ using assms(4-)
+proof (induct "n" arbitrary: r q)
+ case (Suc n)
+ from Suc.prems have ifCond: "\<not> Suc (length r) \<le> length d"
+ by simp
+ with d have r: "r \<noteq> []"
+ using Suc_leI length_greater_0_conv list.size(3) by fastforce
+ then obtain rr lcr where r: "r = rr @ [lcr]"
+ by (cases r rule: rev_cases) auto
from d lc obtain dd where d: "d = dd @ [lc]"
- by (cases d rule: rev_cases, auto)
- from Suc(2) ifCond have n: "n = 1 + length rr - length d" by (auto simp: r)
- from ifCond have len: "length dd \<le> length rr" by (simp add: r d)
+ by (cases d rule: rev_cases) auto
+ from Suc(2) ifCond have n: "n = 1 + length rr - length d"
+ by (auto simp: r)
+ from ifCond have len: "length dd \<le> length rr"
+ by (simp add: r d)
show ?case
proof (cases "lcr div lc * lc = lcr")
case False
- then show ?thesis unfolding Suc(2)[symmetric] using r d
+ with r d show ?thesis
+ unfolding Suc(2)[symmetric]
by (auto simp add: Let_def nth_default_append)
next
case True
- then have id:
- "?thesis = (Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
- (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) =
- divide_poly_main lc
- (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
- (Poly r - monom (lcr div lc) n * Poly d)
- (Poly d) (length rr - 1) n)"
- using r d
- by (cases r rule: rev_cases; cases "d" rule: rev_cases;
- auto simp add: Let_def rev_map nth_default_append)
+ with r d have id:
+ "?thesis \<longleftrightarrow>
+ Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
+ (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) =
+ divide_poly_main lc
+ (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
+ (Poly r - monom (lcr div lc) n * Poly d)
+ (Poly d) (length rr - 1) n"
+ by (cases r rule: rev_cases; cases "d" rule: rev_cases)
+ (auto simp add: Let_def rev_map nth_default_append)
have cong: "\<And>x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
- divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n" by simp
- show ?thesis unfolding id
+ divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n"
+ by simp
+ show ?thesis
+ unfolding id
proof (subst Suc(1), simp add: n,
- subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases)
+ subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases)
case 2
have "monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)"
by (simp add: mult_monom len True)
@@ -4260,26 +4420,28 @@
qed
qed simp
-
lemma divide_poly_list[code]: "f div g = divide_poly_list f g"
proof -
note d = divide_poly_def divide_poly_list_def
show ?thesis
proof (cases "g = 0")
case True
- show ?thesis unfolding d True by auto
+ show ?thesis by (auto simp: d True)
next
case False
- then obtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases, auto)
- with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False" by auto
+ then obtain cg lcg where cg: "coeffs g = cg @ [lcg]"
+ by (cases "coeffs g" rule: rev_cases) auto
+ with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False"
+ by auto
from cg False have lcg: "coeff g (degree g) = lcg"
using last_coeffs_eq_coeff_degree last_snoc by force
- with False have lcg0: "lcg \<noteq> 0" by auto
- from cg have ltp: "Poly (cg @ [lcg]) = g"
- using Poly_coeffs [of g] by auto
- show ?thesis unfolding d cg Let_def id if_False poly_of_list_def
- by (subst divide_poly_main_list, insert False cg lcg0, auto simp: lcg ltp,
- simp add: degree_eq_length_coeffs)
+ with False have "lcg \<noteq> 0" by auto
+ from cg Poly_coeffs [of g] have ltp: "Poly (cg @ [lcg]) = g"
+ by auto
+ show ?thesis
+ unfolding d cg Let_def id if_False poly_of_list_def
+ by (subst divide_poly_main_list, insert False cg \<open>lcg \<noteq> 0\<close>)
+ (auto simp: lcg ltp, simp add: degree_eq_length_coeffs)
qed
qed