diff --git a/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy b/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy --- a/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy +++ b/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy @@ -1,227 +1,225 @@ (* File: Linear_Recurrences_Misc.thy Author: Manuel Eberl, TU München *) section \Miscellaneous material required for linear recurrences\ theory Linear_Recurrences_Misc imports Complex_Main "HOL-Computational_Algebra.Computational_Algebra" "HOL-Computational_Algebra.Polynomial_Factorial" begin fun zip_with where "zip_with f (x#xs) (y#ys) = f x y # zip_with f xs ys" | "zip_with f _ _ = []" lemma length_zip_with [simp]: "length (zip_with f xs ys) = min (length xs) (length ys)" by (induction f xs ys rule: zip_with.induct) simp_all lemma zip_with_altdef: "zip_with f xs ys = map (\(x,y). f x y) (zip xs ys)" by (induction f xs ys rule: zip_with.induct) simp_all lemma zip_with_nth [simp]: "n < length xs \ n < length ys \ zip_with f xs ys ! n = f (xs!n) (ys!n)" by (simp add: zip_with_altdef) lemma take_zip_with: "take n (zip_with f xs ys) = zip_with f (take n xs) (take n ys)" proof (induction f xs ys arbitrary: n rule: zip_with.induct) case (1 f x xs y ys n) thus ?case by (cases n) simp_all qed simp_all lemma drop_zip_with: "drop n (zip_with f xs ys) = zip_with f (drop n xs) (drop n ys)" proof (induction f xs ys arbitrary: n rule: zip_with.induct) case (1 f x xs y ys n) thus ?case by (cases n) simp_all qed simp_all lemma map_zip_with: "map f (zip_with g xs ys) = zip_with (\x y. f (g x y)) xs ys" by (induction g xs ys rule: zip_with.induct) simp_all lemma zip_with_map: "zip_with f (map g xs) (map h ys) = zip_with (\x y. f (g x) (h y)) xs ys" by (induction "\x y. f (g x) (h y)" xs ys rule: zip_with.induct) simp_all lemma zip_with_map_left: "zip_with f (map g xs) ys = zip_with (\x y. f (g x) y) xs ys" using zip_with_map[of f g xs "\x. x" ys] by simp lemma zip_with_map_right: "zip_with f xs (map g ys) = zip_with (\x y. f x (g y)) xs ys" using zip_with_map[of f "\x. x" xs g ys] by simp lemma zip_with_swap: "zip_with (\x y. f y x) xs ys = zip_with f ys xs" by (induction f ys xs rule: zip_with.induct) simp_all lemma set_zip_with: "set (zip_with f xs ys) = (\(x,y). f x y) ` set (zip xs ys)" by (induction f xs ys rule: zip_with.induct) simp_all lemma zip_with_Pair: "zip_with Pair (xs :: 'a list) (ys :: 'b list) = zip xs ys" by (induction "Pair :: 'a \ 'b \ _" xs ys rule: zip_with.induct) simp_all lemma zip_with_altdef': "zip_with f xs ys = [f (xs!i) (ys!i). i \ [0.. [0.. 0" shows "card {x. poly p x = 0} \ degree p" using assms proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "\x. poly p x = 0") case False hence "{x. poly p x = 0} = {}" by blast thus ?thesis by simp next case True then obtain x where x: "poly p x = 0" by blast hence "[:-x, 1:] dvd p" by (subst (asm) poly_eq_0_iff_dvd) then obtain q where q: "p = [:-x, 1:] * q" by (auto simp: dvd_def) with \p \ 0\ have [simp]: "q \ 0" by auto have deg: "degree p = Suc (degree q)" by (subst q, subst degree_mult_eq) auto have "card {x. poly p x = 0} \ card (insert x {x. poly q x = 0})" by (intro card_mono) (auto intro: poly_roots_finite simp: q) also have "\ \ Suc (card {x. poly q x = 0})" by (rule card_insert_le_m1) auto also from deg have "card {x. poly q x = 0} \ degree q" using \p \ 0\ and q by (intro less) auto also have "Suc \ = degree p" by (simp add: deg) finally show ?thesis by - simp_all qed qed lemma poly_eqI_degree: fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" assumes "\x. x \ A \ poly p x = poly q x" assumes "card A > degree p" "card A > degree q" shows "p = q" proof (rule ccontr) assume neq: "p \ q" have "degree (p - q) \ max (degree p) (degree q)" by (rule degree_diff_le_max) also from assms have "\ < card A" by linarith also have "\ \ card {x. poly (p - q) x = 0}" using neq and assms by (intro card_mono poly_roots_finite) auto finally have "degree (p - q) < card {x. poly (p - q) x = 0}" . moreover have "degree (p - q) \ card {x. poly (p - q) x = 0}" using neq by (intro card_poly_roots_bound) auto ultimately show False by linarith qed lemma poly_root_order_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes "P 0" "\p. (\x. poly p x \ 0) \ P p" "\p x n. n > 0 \ poly p x \ 0 \ P p \ P ([:-x, 1:] ^ n * p)" shows "P p" proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) consider "p = 0" | "p \ 0" "\x. poly p x = 0" | "\x. poly p x \ 0" by blast thus ?case proof cases case 3 with assms(2)[of p] show ?thesis by simp next case 2 then obtain x where x: "poly p x = 0" by auto have "[:-x, 1:] ^ order x p dvd p" by (intro order_1) then obtain q where q: "p = [:-x, 1:] ^ order x p * q" by (auto simp: dvd_def) with 2 have [simp]: "q \ 0" by auto have order_pos: "order x p > 0" using \p \ 0\ and x by (auto simp: order_root) have "order x p = order x p + order x q" by (subst q, subst order_mult) (auto simp: order_power_n_n) hence [simp]: "order x q = 0" by simp have deg: "degree p = order x p + degree q" by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq) with order_pos have "degree q < degree p" by simp hence "P q" by (rule less) with order_pos have "P ([:-x, 1:] ^ order x p * q)" by (intro assms(3)) (auto simp: order_root) with q show ?thesis by simp qed (simp_all add: assms(1)) qed lemma complex_poly_decompose: "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:] ^ order z p) = (p :: complex poly)" proof (induction p rule: poly_root_order_induct) case (no_roots p) show ?case proof (cases "degree p = 0") case False hence "\constant (poly p)" by (subst constant_degree) with fundamental_theorem_of_algebra and no_roots show ?thesis by blast qed (auto elim!: degree_eq_zeroE) next case (root p x n) from root have *: "{z. poly ([:- x, 1:] ^ n * p) z = 0} = insert x {z. poly p z = 0}" by auto have "smult (lead_coeff ([:-x, 1:] ^ n * p)) (\z|poly ([:-x,1:] ^ n * p) z = 0. [:-z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = [:- x, 1:] ^ order x ([:- x, 1:] ^ n * p) * smult (lead_coeff p) (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p))" by (subst *, subst prod.insert) (insert root, auto intro: poly_roots_finite simp: mult_ac lead_coeff_mult lead_coeff_power) also have "order x ([:- x, 1:] ^ n * p) = n" using root by (subst order_mult) (auto simp: order_power_n_n order_0I) also have "(\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z p)" proof (intro prod.cong refl, goal_cases) case (1 y) with root have "order y ([:-x,1:] ^ n) = 0" by (intro order_0I) auto thus ?case using root by (subst order_mult) auto qed also note root.IH finally show ?case . qed simp_all lemma normalize_field: "normalize (x :: 'a :: {normalization_semidom,field}) = (if x = 0 then 0 else 1)" by (auto simp: normalize_1_iff dvd_field_iff) lemma unit_factor_field [simp]: "unit_factor (x :: 'a :: {normalization_semidom,field}) = x" using unit_factor_mult_normalize[of x] normalize_field[of x] by (simp split: if_splits) lemma coprime_linear_poly: fixes c :: "'a :: field_gcd" assumes "c \ c'" shows "coprime [:c,1:] [:c',1:]" proof - have "gcd [:c,1:] [:c',1:] = gcd ([:c,1:] - [:c',1:]) [:c',1:]" by (rule gcd_diff1 [symmetric]) also have "[:c,1:] - [:c',1:] = [:c-c':]" by simp also from assms have "gcd \ [:c',1:] = normalize [:c-c':]" by (intro gcd_proj1_if_dvd) (auto simp: const_poly_dvd_iff dvd_field_iff) also from assms have "\ = 1" by (simp add: normalize_poly_def) finally show "coprime [:c,1:] [:c',1:]" by (simp add: gcd_eq_1_imp_coprime) qed lemma coprime_linear_poly': fixes c :: "'a :: field_gcd" assumes "c \ c'" "c \ 0" "c' \ 0" shows "coprime [:1,c:] [:1,c':]" proof - have "gcd [:1,c:] [:1,c':] = gcd ([:1,c:] mod [:1,c':]) [:1,c':]" by simp - also have "eucl_rel_poly [:1, c:] [:1, c':] ([:c/c':], [:1-c/c':])" - using assms by (auto simp add: eucl_rel_poly_iff one_pCons) - hence "[:1,c:] mod [:1,c':] = [:1 - c / c':]" - by (rule mod_poly_eq) + also have \[:1,c:] mod [:1,c':] = [:1 - c / c':]\ + using \c' \ 0\ by (simp add: mod_pCons) also from assms have "gcd \ [:1,c':] = normalize ([:1 - c / c':])" by (intro gcd_proj1_if_dvd) (auto simp: const_poly_dvd_iff dvd_field_iff) also from assms have "\ = 1" by (auto simp: normalize_poly_def) finally show ?thesis by (rule gcd_eq_1_imp_coprime) qed end diff --git a/thys/Polynomial_Interpolation/Ring_Hom_Poly.thy b/thys/Polynomial_Interpolation/Ring_Hom_Poly.thy --- a/thys/Polynomial_Interpolation/Ring_Hom_Poly.thy +++ b/thys/Polynomial_Interpolation/Ring_Hom_Poly.thy @@ -1,450 +1,455 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) section \Connecting Polynomials with Homomorphism Locales\ theory Ring_Hom_Poly imports "HOL-Computational_Algebra.Euclidean_Algorithm" Ring_Hom Missing_Polynomial begin text\@{term poly} as a homomorphism. Note that types differ.\ interpretation poly_hom: comm_semiring_hom "\p. poly p a" by (unfold_locales, auto) interpretation poly_hom: comm_ring_hom "\p. poly p a".. interpretation poly_hom: idom_hom "\p. poly p a".. text \@{term "(\\<^sub>p)"} as a homomorphism.\ interpretation pcompose_hom: comm_semiring_hom "\q. q \\<^sub>p p" using pcompose_add pcompose_mult pcompose_1 by (unfold_locales, auto) interpretation pcompose_hom: comm_ring_hom "\q. q \\<^sub>p p" .. interpretation pcompose_hom: idom_hom "\q. q \\<^sub>p p" .. definition eval_poly :: "('a \ 'b :: comm_semiring_1) \ 'a :: zero poly \ 'b \ 'b" where [code del]: "eval_poly h p = poly (map_poly h p)" lemma eval_poly_code[code]: "eval_poly h p x = fold_coeffs (\ a b. h a + x * b) p 0" by (induct p, auto simp: eval_poly_def) lemma eval_poly_as_sum: fixes h :: "'a :: zero \ 'b :: comm_semiring_1" assumes "h 0 = 0" shows "eval_poly h p x = (\i\degree p. x^i * h (coeff p i))" unfolding eval_poly_def proof (induct p) case 0 show ?case using assms by simp next case (pCons a p) thus ?case proof (cases "p = 0") case True show ?thesis by (simp add: True map_poly_simps assms) next case False show ?thesis unfolding degree_pCons_eq[OF False] unfolding sum.atMost_Suc_shift unfolding map_poly_pCons[OF pCons(1)] by (simp add: pCons(2) sum_distrib_left mult.assoc) qed qed lemma coeff_const: "coeff [: a :] i = (if i = 0 then a else 0)" by (metis coeff_monom monom_0) lemma x_as_monom: "[:0,1:] = monom 1 1" by (simp add: monom_0 monom_Suc) lemma x_pow_n: "monom 1 1 ^ n = monom 1 n" by (induct n) (simp_all add: monom_0 monom_Suc) lemma map_poly_eval_poly: assumes h0: "h 0 = 0" shows "map_poly h p = eval_poly (\ a. [: h a :]) p [:0,1:]" (is "?mp = ?ep") proof (rule poly_eqI) fix i :: nat have 2: "(\x\i. \xa\degree p. (if xa = x then 1 else 0) * coeff [:h (coeff p xa):] (i - x)) = h (coeff p i)" (is "sum ?f ?s = ?r") proof - have "sum ?f ?s = ?f i + sum ?f ({..i} - {i})" by (rule sum.remove[of _ i], auto) also have "sum ?f ({..i} - {i}) = 0" by (rule sum.neutral, intro ballI, rule sum.neutral, auto simp: coeff_const) also have "?f i = (\xa\degree p. (if xa = i then 1 else 0) * h (coeff p xa))" (is "_ = ?m") unfolding coeff_const by simp also have "\ = ?r" proof (cases "i \ degree p") case True show ?thesis by (subst sum.remove[of _ i], insert True, auto) next case False hence [simp]: "coeff p i = 0" using le_degree by blast show ?thesis by (subst sum.neutral, auto simp: h0) qed finally show ?thesis by simp qed have h'0: "[: h 0 :] = 0" using h0 by auto show "coeff ?mp i = coeff ?ep i" unfolding coeff_map_poly[of h, OF h0] unfolding eval_poly_as_sum[of "\a. [: h a :]", OF h'0] unfolding coeff_sum unfolding x_as_monom x_pow_n coeff_mult unfolding sum.swap[of _ _ "{..degree p}"] unfolding coeff_monom using 2 by auto qed lemma smult_as_map_poly: "smult a = map_poly ((*) a)" by (rule ext, rule poly_eqI, subst coeff_map_poly, auto) subsection \@{const map_poly} of Homomorphisms\ context zero_hom begin text \We will consider @{term hom} is always simpler than @{term "map_poly hom"}.\ lemma map_poly_hom_monom[simp]: "map_poly hom (monom a i) = monom (hom a) i" by(rule map_poly_monom, auto) lemma coeff_map_poly_hom[simp]: "coeff (map_poly hom p) i = hom (coeff p i)" by (rule coeff_map_poly, rule hom_zero) end locale map_poly_zero_hom = base: zero_hom begin sublocale zero_hom "map_poly hom" by (unfold_locales, auto) end text \@{const map_poly} preserves homomorphisms over addition.\ context comm_monoid_add_hom begin lemma map_poly_hom_add[hom_distribs]: "map_poly hom (p + q) = map_poly hom p + map_poly hom q" by (rule map_poly_add; simp add: hom_distribs) end locale map_poly_comm_monoid_add_hom = base: comm_monoid_add_hom begin sublocale comm_monoid_add_hom "map_poly hom" by (unfold_locales, auto simp:hom_distribs) end text \To preserve homomorphisms over multiplication, it demands commutative ring homomorphisms.\ context comm_semiring_hom begin lemma map_poly_pCons_hom[hom_distribs]: "map_poly hom (pCons a p) = pCons (hom a) (map_poly hom p)" unfolding map_poly_simps by auto lemma map_poly_hom_smult[hom_distribs]: "map_poly hom (smult c p) = smult (hom c) (map_poly hom p)" by (induct p, auto simp: hom_distribs) lemma poly_map_poly[simp]: "poly (map_poly hom p) (hom x) = hom (poly p x)" by (induct p; simp add: hom_distribs) end locale map_poly_comm_semiring_hom = base: comm_semiring_hom begin sublocale map_poly_comm_monoid_add_hom.. sublocale comm_semiring_hom "map_poly hom" proof show "map_poly hom 1 = 1" by simp fix p q show "map_poly hom (p * q) = map_poly hom p * map_poly hom q" by (induct p, auto simp: hom_distribs) qed end locale map_poly_comm_ring_hom = base: comm_ring_hom begin sublocale map_poly_comm_semiring_hom.. sublocale comm_ring_hom "map_poly hom".. end locale map_poly_idom_hom = base: idom_hom begin sublocale map_poly_comm_ring_hom.. sublocale idom_hom "map_poly hom".. end subsubsection \Injectivity\ locale map_poly_inj_zero_hom = base: inj_zero_hom begin sublocale inj_zero_hom "map_poly hom" proof (unfold_locales) fix p q :: "'a poly" assume "map_poly hom p = map_poly hom q" from cong[of "\p. coeff p _", OF refl this] show "p = q" by (auto intro: poly_eqI) qed simp end locale map_poly_inj_comm_monoid_add_hom = base: inj_comm_monoid_add_hom begin sublocale map_poly_comm_monoid_add_hom.. sublocale map_poly_inj_zero_hom.. sublocale inj_comm_monoid_add_hom "map_poly hom".. end locale map_poly_inj_comm_semiring_hom = base: inj_comm_semiring_hom begin sublocale map_poly_comm_semiring_hom.. sublocale map_poly_inj_zero_hom.. sublocale inj_comm_semiring_hom "map_poly hom".. end locale map_poly_inj_comm_ring_hom = base: inj_comm_ring_hom begin sublocale map_poly_inj_comm_semiring_hom.. sublocale inj_comm_ring_hom "map_poly hom".. end locale map_poly_inj_idom_hom = base: inj_idom_hom begin sublocale map_poly_inj_comm_ring_hom.. sublocale inj_idom_hom "map_poly hom".. end lemma degree_map_poly_le: "degree (map_poly f p) \ degree p" by(induct p;auto) lemma coeffs_map_poly: (* An exact variant *) assumes "f (lead_coeff p) = 0 \ p = 0" shows "coeffs (map_poly f p) = map f (coeffs p)" unfolding coeffs_map_poly using assms by (simp add:coeffs_def) lemma degree_map_poly: (* An exact variant *) assumes "f (lead_coeff p) = 0 \ p = 0" shows "degree (map_poly f p) = degree p" unfolding degree_eq_length_coeffs unfolding coeffs_map_poly[of f, OF assms] by simp context zero_hom_0 begin lemma degree_map_poly_hom[simp]: "degree (map_poly hom p) = degree p" by (rule degree_map_poly, auto) lemma coeffs_map_poly_hom[simp]: "coeffs (map_poly hom p) = map hom (coeffs p)" by (rule coeffs_map_poly, auto) lemma hom_lead_coeff[simp]: "lead_coeff (map_poly hom p) = hom (lead_coeff p)" by simp end context comm_semiring_hom begin interpretation map_poly_hom: map_poly_comm_semiring_hom.. lemma poly_map_poly_0[simp]: "poly (map_poly hom p) 0 = hom (poly p 0)" (is "?l = ?r") proof- have "?l = poly (map_poly hom p) (hom 0)" by auto then show ?thesis unfolding poly_map_poly. qed lemma poly_map_poly_1[simp]: "poly (map_poly hom p) 1 = hom (poly p 1)" (is "?l = ?r") proof- have "?l = poly (map_poly hom p) (hom 1)" by auto then show ?thesis unfolding poly_map_poly. qed lemma map_poly_hom_as_monom_sum: "(\j\degree p. monom (hom (coeff p j)) j) = map_poly hom p" proof - show ?thesis by (subst(6) poly_as_sum_of_monoms'[OF le_refl, symmetric], simp add: hom_distribs) qed lemma map_poly_pcompose[hom_distribs]: "map_poly hom (f \\<^sub>p g) = map_poly hom f \\<^sub>p map_poly hom g" by (induct f arbitrary: g; auto simp: hom_distribs) end context comm_semiring_hom begin lemma eval_poly_0[simp]: "eval_poly hom 0 x = 0" unfolding eval_poly_def by simp lemma eval_poly_monom: "eval_poly hom (monom a n) x = hom a * x ^ n" unfolding eval_poly_def unfolding map_poly_monom[of hom, OF hom_zero] using poly_monom. lemma poly_map_poly_eval_poly: "poly (map_poly hom p) = eval_poly hom p" unfolding eval_poly_def.. lemma map_poly_eval_poly: "map_poly hom p = eval_poly (\ a. [: hom a :]) p [:0,1:]" by (rule map_poly_eval_poly, simp) lemma degree_extension: assumes "degree p \ n" shows "(\i\degree p. x ^ i * hom (coeff p i)) = (\i\n. x ^ i * hom (coeff p i))" (is "?l = ?r") proof - let ?f = "\ i. x ^ i * hom (coeff p i)" define m where "m = n - degree p" have n: "n = degree p + m" unfolding m_def using assms by auto have "?r = (\ i \ degree p + m. ?f i)" unfolding n .. also have "\ = ?l + sum ?f {Suc (degree p) .. degree p + m}" by (subst sum.union_disjoint[symmetric], auto intro: sum.cong) also have "sum ?f {Suc (degree p) .. degree p + m} = 0" by (rule sum.neutral, auto simp: coeff_eq_0) finally show ?thesis by simp qed lemma eval_poly_add[simp]: "eval_poly hom (p + q) x = eval_poly hom p x + eval_poly hom q x" unfolding eval_poly_def hom_distribs.. lemma eval_poly_sum: "eval_poly hom (\k\A. p k) x = (\k\A. eval_poly hom (p k) x)" proof (induct A rule: infinite_finite_induct) case (insert a A) show ?case unfolding sum.insert[OF insert(1-2)] insert(3)[symmetric] by simp qed (auto simp: eval_poly_def) lemma eval_poly_poly: "eval_poly hom p (hom x) = hom (poly p x)" unfolding eval_poly_def by auto end context comm_ring_hom begin interpretation map_poly_hom: map_poly_comm_ring_hom.. lemma pseudo_divmod_main_hom: "pseudo_divmod_main (hom lc) (map_poly hom q) (map_poly hom r) (map_poly hom d) dr i = map_prod (map_poly hom) (map_poly hom) (pseudo_divmod_main lc q r d dr i)" proof- show ?thesis by (induct lc q r d dr i rule:pseudo_divmod_main.induct, auto simp: Let_def hom_distribs) qed end lemma(in inj_comm_ring_hom) pseudo_divmod_hom: "pseudo_divmod (map_poly hom p) (map_poly hom q) = map_prod (map_poly hom) (map_poly hom) (pseudo_divmod p q)" unfolding pseudo_divmod_def using pseudo_divmod_main_hom[of _ 0] by (cases "q = 0",auto) lemma(in inj_idom_hom) pseudo_mod_hom: "pseudo_mod (map_poly hom p) (map_poly hom q) = map_poly hom (pseudo_mod p q)" using pseudo_divmod_hom unfolding pseudo_mod_def by auto lemma(in idom_hom) map_poly_pderiv[hom_distribs]: "map_poly hom (pderiv p) = pderiv (map_poly hom p)" proof (induct p rule: pderiv.induct) case (1 a p) then show ?case unfolding pderiv.simps map_poly_pCons_hom by (cases "p = 0", auto simp: hom_distribs) qed context field_hom begin -lemma map_poly_pdivmod[hom_distribs]: - "map_prod (map_poly hom) (map_poly hom) (p div q, p mod q) = - (map_poly hom p div map_poly hom q, map_poly hom p mod map_poly hom q)" - (is "?l = ?r") +lemma dvd_map_poly_hom_imp_dvd: \map_poly hom x dvd map_poly hom y \ x dvd y\ + by (smt (verit, del_insts) degree_map_poly_hom hom_0 hom_div hom_lead_coeff hom_one hom_power map_poly_hom_smult map_poly_zero mod_eq_0_iff_dvd mod_poly_def pseudo_mod_hom) + +lemma map_poly_pdivmod [hom_distribs]: + \map_prod (map_poly hom) (map_poly hom) (p div q, p mod q) = + (map_poly hom p div map_poly hom q, map_poly hom p mod map_poly hom q)\ proof - - let ?mp = "map_poly hom" - interpret map_poly_hom: map_poly_idom_hom.. - obtain r s where dm: "(p div q, p mod q) = (r, s)" - by force - hence r: "r = p div q" and s: "s = p mod q" - by simp_all - from dm [folded pdivmod_pdivmodrel] have "eucl_rel_poly p q (r, s)" - by auto - from this[unfolded eucl_rel_poly_iff] - have eq: "p = r * q + s" and cond: "(if q = 0 then r = 0 else s = 0 \ degree s < degree q)" by auto - from arg_cong[OF eq, of ?mp, unfolded map_poly_add] - have eq: "?mp p = ?mp q * ?mp r + ?mp s" by (auto simp: hom_distribs) - from cond have cond: "(if ?mp q = 0 then ?mp r = 0 else ?mp s = 0 \ degree (?mp s) < degree (?mp q))" + let ?mp = \map_poly hom\ + interpret map_poly_hom: map_poly_idom_hom .. + have \(?mp p div ?mp q, ?mp p mod ?mp q) = (?mp (p div q), ?mp (p mod q))\ + proof (cases \?mp q\ \?mp (p div q)\ \?mp (p mod q)\ \?mp p\ rule: euclidean_relation_polyI) + case by0 + then show ?case + by simp + next + case divides + then have \q \ 0\ \q dvd p\ + by (auto dest: dvd_map_poly_hom_imp_dvd) + from \q dvd p\ obtain r where \p = q * r\ .. + with \q \ 0\ show ?case + by (simp add: map_poly_hom.hom_mult) + next + case euclidean_relation + with degree_mod_less_degree [of q p] show ?case + by (auto simp flip: map_poly_hom.hom_mult map_poly_hom_add) + qed + then show ?thesis by simp - from eq cond have "eucl_rel_poly (?mp p) (?mp q) (?mp r, ?mp s)" - unfolding eucl_rel_poly_iff by auto - from this[unfolded pdivmod_pdivmodrel] - show ?thesis unfolding dm prod.simps by simp qed lemma map_poly_div[hom_distribs]: "map_poly hom (p div q) = map_poly hom p div map_poly hom q" using map_poly_pdivmod[of p q] by simp lemma map_poly_mod[hom_distribs]: "map_poly hom (p mod q) = map_poly hom p mod map_poly hom q" using map_poly_pdivmod[of p q] by simp end locale field_hom' = field_hom hom for hom :: "'a :: {field_gcd} \ 'b :: {field_gcd}" begin lemma map_poly_normalize[hom_distribs]: "map_poly hom (normalize p) = normalize (map_poly hom p)" by (simp add: normalize_poly_def hom_distribs) lemma map_poly_gcd[hom_distribs]: "map_poly hom (gcd p q) = gcd (map_poly hom p) (map_poly hom q)" by (induct p q rule: eucl_induct) (simp_all add: map_poly_normalize ac_simps hom_distribs) end definition div_poly :: "'a :: euclidean_semiring \ 'a poly \ 'a poly" where "div_poly a p = map_poly (\ c. c div a) p" lemma smult_div_poly: assumes "\ c. c \ set (coeffs p) \ a dvd c" shows "smult a (div_poly a p) = p" unfolding smult_as_map_poly div_poly_def by (subst map_poly_map_poly, force, subst map_poly_idI, insert assms, auto) lemma coeff_div_poly: "coeff (div_poly a f) n = coeff f n div a" unfolding div_poly_def by (rule coeff_map_poly, auto) locale map_poly_inj_idom_divide_hom = base: inj_idom_divide_hom begin sublocale map_poly_idom_hom .. sublocale map_poly_inj_zero_hom .. sublocale inj_idom_hom "map_poly hom" .. lemma divide_poly_main_hom: defines "hh \ map_poly hom" shows "hh (divide_poly_main lc f g h i j) = divide_poly_main (hom lc) (hh f) (hh g) (hh h) i j" unfolding hh_def proof (induct j arbitrary: lc f g h i) case (Suc j lc f g h i) let ?h = "map_poly hom" show ?case unfolding divide_poly_main.simps Let_def unfolding base.coeff_map_poly_hom base.hom_div[symmetric] base.hom_mult[symmetric] base.eq_iff if_distrib[of ?h] hom_zero by (rule if_cong[OF refl _ refl], subst Suc, simp add: hom_minus hom_add hom_mult) qed simp sublocale inj_idom_divide_hom "map_poly hom" proof fix f g :: "'a poly" let ?h = "map_poly hom" show "?h (f div g) = (?h f) div (?h g)" unfolding divide_poly_def if_distrib[of ?h] divide_poly_main_hom by simp qed lemma order_hom: "order (hom x) (map_poly hom f) = order x f" unfolding Polynomial.order_def unfolding hom_dvd_iff[symmetric] unfolding hom_power by (simp add: base.hom_uminus) end subsection \Example Interpretations\ abbreviation "of_int_poly \ map_poly of_int" interpretation of_int_poly_hom: map_poly_comm_semiring_hom of_int.. interpretation of_int_poly_hom: map_poly_comm_ring_hom of_int.. interpretation of_int_poly_hom: map_poly_idom_hom of_int.. interpretation of_int_poly_hom: map_poly_inj_comm_ring_hom "of_int :: int \ 'a :: {comm_ring_1,ring_char_0}" .. interpretation of_int_poly_hom: map_poly_inj_idom_hom "of_int :: int \ 'a :: {idom,ring_char_0}" .. text \The following operations are homomorphic w.r.t. only @{class monoid_add}.\ interpretation pCons_0_hom: injective "pCons 0" by (unfold_locales, auto) interpretation pCons_0_hom: zero_hom_0 "pCons 0" by (unfold_locales, auto) interpretation pCons_0_hom: inj_comm_monoid_add_hom "pCons 0" by (unfold_locales, auto) interpretation pCons_0_hom: inj_ab_group_add_hom "pCons 0" by (unfold_locales, auto) interpretation monom_hom: injective "\x. monom x d" by (unfold_locales, auto) interpretation monom_hom: inj_monoid_add_hom "\x. monom x d" by (unfold_locales, auto simp: add_monom) interpretation monom_hom: inj_comm_monoid_add_hom "\x. monom x d".. end diff --git a/thys/Subresultants/Subresultant.thy b/thys/Subresultants/Subresultant.thy --- a/thys/Subresultants/Subresultant.thy +++ b/thys/Subresultants/Subresultant.thy @@ -1,2778 +1,2778 @@ section \Subresultants and the subresultant PRS\ text \This theory contains most of the soundness proofs of the subresultant PRS algorithm, where we closely follow the papers of Brown \cite{Brown} and Brown and Traub \cite{BrownTraub}. This is in contrast to a similar Coq formalization of Mahboubi \cite{Mahboubi06} which is based on polynomial determinants. Whereas the current file only contains an algorithm to compute the resultant of two polynomials efficiently, there is another theory ``Subresultant-Gcd'' which also contains the algorithm to compute the GCD of two polynomials via the subresultant algorithm. In both algorithms we integrate Lazard's optimization in the dichotomous version, but not the second optmization described by Ducos \cite{Ducos}.\ theory Subresultant imports Resultant_Prelim Dichotomous_Lazard Binary_Exponentiation More_Homomorphisms Coeff_Int begin subsection \Algorithm\ locale div_exp_param = fixes div_exp :: "'a :: idom_divide \ 'a \ nat \ 'a" begin partial_function(tailrec) subresultant_prs_main where "subresultant_prs_main f g c = (let m = degree f; n = degree g; lf = lead_coeff f; lg = lead_coeff g; \ = m - n; d = div_exp lg c \; h = pseudo_mod f g in if h = 0 then (g,d) else subresultant_prs_main g (sdiv_poly h ((-1) ^ (\ + 1) * lf * (c ^ \))) d)" definition subresultant_prs where "subresultant_prs f g = (let h = pseudo_mod f g; \ = (degree f - degree g); d = lead_coeff g ^ \ in if h = 0 then (g,d) else subresultant_prs_main g ((- 1) ^ (\ + 1) * h) d)" definition resultant_impl_main where "resultant_impl_main G1 G2 = (if G2 = 0 then (if degree G1 = 0 then 1 else 0) else case subresultant_prs G1 G2 of (Gk,hk) \ (if degree Gk = 0 then hk else 0))" definition resultant_impl where "resultant_impl f g = (if length (coeffs f) \ length (coeffs g) then resultant_impl_main f g else let res = resultant_impl_main g f in if even (degree f) \ even (degree g) then res else - res)" end locale div_exp_sound = div_exp_param + assumes div_exp: "\ x y n. (to_fract x)^n / (to_fract y)^(n-1) \ range to_fract \ to_fract (div_exp x y n) = (to_fract x)^n / (to_fract y)^(n-1)" definition basic_div_exp :: "'a :: idom_divide \ 'a \ nat \ 'a" where "basic_div_exp x y n = x^n div y^(n-1)" text \We have an instance for arbitrary integral domains.\ lemma basic_div_exp: "div_exp_sound basic_div_exp" by (unfold_locales, unfold basic_div_exp_def, rule sym, rule div_divide_to_fract, auto simp: hom_distribs) text \Lazard's optimization is only proven for factorial rings.\ lemma dichotomous_Lazard: "div_exp_sound (dichotomous_Lazard :: 'a :: factorial_ring_gcd \ _)" by (unfold_locales, rule dichotomous_Lazard) subsection \Soundness Proof for @{term "div_exp_param.resultant_impl div_exp = resultant"}\ abbreviation pdivmod :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly" where "pdivmod p q \ (p div q, p mod q)" lemma even_sum_list: assumes "\ x. x \ set xs \ even (f x) = even (g x)" shows "even (sum_list (map f xs)) = even (sum_list (map g xs))" using assms by (induct xs, auto) lemma for_all_Suc: "P i \ (\ j \ Suc i. P j) = (\ j \ i. P j)" for P by (metis (full_types) Suc_le_eq less_le) (* part on pseudo_divmod *) lemma pseudo_mod_left_0[simp]: "pseudo_mod 0 x = 0" unfolding pseudo_mod_def pseudo_divmod_def by (cases "x = 0"; cases "length (coeffs x)", auto) lemma pseudo_mod_right_0[simp]: "pseudo_mod x 0 = x" unfolding pseudo_mod_def pseudo_divmod_def by simp lemma snd_pseudo_divmod_main_cong: assumes "a1 = b1" "a3 = b3" "a4 = b4" "a5 = b5" "a6 = b6" (* note that a2 = b2 is not required! *) shows "snd (pseudo_divmod_main a1 a2 a3 a4 a5 a6) = snd (pseudo_divmod_main b1 b2 b3 b4 b5 b6)" using assms snd_pseudo_divmod_main by metis lemma snd_pseudo_mod_smult_invar_right: shows "(snd (pseudo_divmod_main (x * lc) q r (smult x d) dr n)) = snd (pseudo_divmod_main lc q' (smult (x^n) r) d dr n)" proof(induct n arbitrary: q q' r dr) case (Suc n) let ?q = "smult (x * lc) q + monom (coeff r dr) n" let ?r = "smult (x * lc) r - (smult x (monom (coeff r dr) n * d))" let ?dr = "dr - 1" let ?rec_lhs = "pseudo_divmod_main (x * lc) ?q ?r (smult x d) ?dr n" let ?rec_rhs = "pseudo_divmod_main lc q' (smult (x^n) ?r) d ?dr n" have [simp]: "\ n. x ^ n * (x * lc) = lc * (x * x ^ n)" "\ n c. x ^ n * (x * c) = x * x ^ n * c" "\ n. x * x ^ n * lc = lc * (x * x ^ n)" by (auto simp: ac_simps) have "snd (pseudo_divmod_main (x * lc) q r (smult x d) dr (Suc n)) = snd ?rec_lhs" by (auto simp:Let_def) also have "\ = snd ?rec_rhs" using Suc by auto also have "\ = snd (pseudo_divmod_main lc q' (smult (x^Suc n) r) d dr (Suc n))" unfolding pseudo_divmod_main.simps Let_def proof(rule snd_pseudo_divmod_main_cong,goal_cases) case 2 show ?case by (auto simp:smult_add_right smult_diff_right smult_monom smult_monom_mult) qed auto finally show ?case by auto qed auto lemma snd_pseudo_mod_smult_invar_left: shows "snd (pseudo_divmod_main lc q (smult x r) d dr n) = smult x (snd (pseudo_divmod_main lc q' r d dr n))" proof(induct n arbitrary:x lc q q' r d dr) case (Suc n) have sm:"smult lc (smult x r) - monom (coeff (smult x r) dr) n * d =smult x (smult lc r - monom (coeff r dr) n * d) " by (auto simp:smult_diff_right smult_monom smult_monom_mult mult.commute[of lc x]) let ?q' = "smult lc q' + monom (coeff r dr) n" show ?case unfolding pseudo_divmod_main.simps Let_def Suc(1)[of lc _ _ _ _ _ ?q'] sm by auto qed auto lemma snd_pseudo_mod_smult_left[simp]: shows "snd (pseudo_divmod (smult (x::'a::idom) p) q) = (smult x (snd (pseudo_divmod p q)))" unfolding pseudo_divmod_def by (auto simp:snd_pseudo_mod_smult_invar_left[of _ _ _ _ _ _ _ 0] Polynomial.coeffs_smult) lemma pseudo_mod_smult_right: assumes "(x::'a::idom)\0" "q\0" shows "(pseudo_mod p (smult (x::'a::idom) q)) = (smult (x^(Suc (length (coeffs p)) - length (coeffs q))) (pseudo_mod p q))" unfolding pseudo_divmod_def pseudo_mod_def by (auto simp:snd_pseudo_mod_smult_invar_right[of _ _ _ _ _ _ _ 0] snd_pseudo_mod_smult_invar_left[of _ _ _ _ _ _ _ 0] Polynomial.coeffs_smult assms) lemma pseudo_mod_zero[simp]: "pseudo_mod 0 f = (0::'a :: {idom} poly)" "pseudo_mod f 0 = f" unfolding pseudo_mod_def snd_pseudo_mod_smult_left[of 0 _ f,simplified] unfolding pseudo_divmod_def by auto (* part on prod_list *) lemma prod_combine: assumes "j \ i" shows "f i * (\l\[j.. i. (-1)^(f i)) xs) = (-1)^(sum_list (map f xs))" by (induct xs, auto simp: power_add) lemma minus_1_power_even: "(- (1 :: 'b :: comm_ring_1))^ k = (if even k then 1 else (-1))" by auto lemma minus_1_even_eqI: assumes "even k = even l" shows "(- (1 :: 'b :: comm_ring_1))^k = (- 1)^l" unfolding minus_1_power_even assms by auto lemma (in comm_monoid_mult) prod_list_multf: "(\x\xs. f x * g x) = prod_list (map f xs) * prod_list (map g xs)" by (induct xs) (simp_all add: algebra_simps) lemma inverse_prod_list: "inverse (prod_list xs) = prod_list (map inverse (xs :: 'a :: field list))" by (induct xs, auto) (* part on pow_int, i.e., exponentiation with integer exponent *) definition pow_int :: "'a :: field \ int \ 'a" where "pow_int x e = (if e < 0 then 1 / (x ^ (nat (-e))) else x ^ (nat e))" lemma pow_int_0[simp]: "pow_int x 0 = 1" unfolding pow_int_def by auto lemma pow_int_1[simp]: "pow_int x 1 = x" unfolding pow_int_def by auto lemma exp_pow_int: "x ^ n = pow_int x n" unfolding pow_int_def by auto lemma pow_int_add: assumes x: "x \ 0" shows "pow_int x (a + b) = pow_int x a * pow_int x b" proof - have *: "\ a + b < 0 \ a < 0 \ nat b = nat (a + b) + nat (-a)" "\ a + b < 0 \ b < 0 \ nat a = nat (a + b) + nat (-b)" "a + b < 0 \ \ a < 0 \ nat (-b) = nat a + nat (-a -b) " "a + b < 0 \ \ b < 0 \ nat (-a) = nat b + nat (-a -b) " by auto have pow_eq: "l = m \ (x ^ l = x ^ m)" for l m by auto from x show ?thesis unfolding pow_int_def by (auto split: if_splits simp: power_add[symmetric] simp: * intro!: pow_eq, auto simp: power_add) qed lemma pow_int_mult: "pow_int (x * y) a = pow_int x a * pow_int y a" unfolding pow_int_def by (cases "a < 0", auto simp: power_mult_distrib) lemma pow_int_base_1[simp]: "pow_int 1 a = 1" unfolding pow_int_def by (cases "a < 0", auto) lemma pow_int_divide: "a / pow_int x b = a * pow_int x (-b)" unfolding pow_int_def by (cases b rule: linorder_cases[of _ 0], auto) lemma divide_prod_assoc: "x / (y * z :: 'a :: field) = x / y / z" by (simp add: field_simps) lemma minus_1_inverse_pow[simp]: "x / (-1)^n = (x :: 'a :: field) * (-1)^n" by (simp add: minus_1_power_even) (* part on subresultants *) definition subresultant_mat :: "nat \ 'a :: comm_ring_1 poly \ 'a poly \ 'a poly mat" where "subresultant_mat J F G = (let dg = degree G; df = degree F; f = coeff_int F; g = coeff_int G; n = (df - J) + (dg - J) in mat n n (\ (i,j). if j < dg - J then if i = n - 1 then monom 1 (dg - J - 1 - j) * F else [: f (df - int i + int j) :] else let jj = j - (dg - J) in if i = n - 1 then monom 1 (df - J - 1 - jj) * G else [: g (dg - int i + int jj) :]))" lemma subresultant_mat_dim[simp]: fixes j p q defines "S \ subresultant_mat j p q" shows "dim_row S = (degree p - j) + (degree q - j)" and "dim_col S = (degree p - j) + (degree q - j)" unfolding S_def subresultant_mat_def Let_def by auto definition subresultant'_mat :: "nat \ nat \ 'a :: comm_ring_1 poly \ 'a poly \ 'a mat" where "subresultant'_mat J l F G = (let \ = degree G; \ = degree F; f = coeff_int F; g = coeff_int G; n = (\ - J) + (\ - J) in mat n n (\ (i,j). if j < \ - J then if i = n - 1 then (f (l - int (\ - J - 1) + int j)) else (f (\ - int i + int j)) else let jj = j - (\ - J) in if i = n - 1 then (g (l - int (\ - J - 1) + int jj)) else (g (\ - int i + int jj))))" lemma subresultant_index_mat: fixes F G assumes i: "i < (degree F - J) + (degree G - J)" and j: "j < (degree F - J) + (degree G - J)" shows "subresultant_mat J F G $$ (i,j) = (if j < degree G - J then if i = (degree F - J) + (degree G - J) - 1 then monom 1 (degree G - J - 1 - j) * F else ([: coeff_int F ( degree F - int i + int j) :]) else let jj = j - (degree G - J) in if i = (degree F - J) + (degree G - J) - 1 then monom 1 ( degree F - J - 1 - jj) * G else ([: coeff_int G (degree G - int i + int jj) :]))" unfolding subresultant_mat_def Let_def unfolding index_mat(1)[OF i j] split by auto definition subresultant :: "nat \ 'a :: comm_ring_1 poly \ 'a poly \ 'a poly" where "subresultant J F G = det (subresultant_mat J F G)" lemma subresultant_smult_left: assumes "(c :: 'a :: {comm_ring_1, semiring_no_zero_divisors}) \ 0" shows "subresultant J (smult c f) g = smult (c ^ (degree g - J)) (subresultant J f g)" proof - let ?df = "degree f" let ?dg = "degree g" let ?n = "(?df - J) + (?dg - J)" let ?m = "?dg - J" let ?M = "mat ?n ?n (\ (i,j). if i = j then if i < ?m then [:c:] else 1 else 0)" from \c \ 0\ have deg: "degree (smult c f) = ?df" by simp let ?S = "subresultant_mat J f g" let ?cS = "subresultant_mat J (smult c f) g" have dim: "dim_row ?S = ?n" "dim_col ?S = ?n" "dim_row ?cS = ?n" "dim_col ?cS = ?n" using deg by auto hence C: "?S \ carrier_mat ?n ?n" "?cS \ carrier_mat ?n ?n" "?M \ carrier_mat ?n ?n" by auto have dim': "dim_row (?S * ?M) = ?n" "dim_col (?S * ?M) = ?n" using dim (1,2) by simp_all define S where "S = ?S" have "?cS = ?S * ?M" proof (rule eq_matI, unfold dim' dim) fix i j assume ij: "i < ?n" "j < ?n" have "(?S * ?M) $$ (i,j) = row ?S i \ col ?M j" by (rule index_mult_mat, insert ij dim, auto) also have "\ = (\k = 0.. = (\k = 0.. = S $$ (i,j) * ?M $$ (j,j) + sum (\ k. S $$ (i,k) * ?M $$ (k,j)) ({0.. = S $$ (i,j) * ?M $$ (j,j)" by (subst sum.neutral, insert ij, auto) also have "\ = ?cS $$ (i,j)" unfolding subresultant_index_mat[OF ij] S_def by (subst subresultant_index_mat, unfold deg, insert ij, auto) finally show "?cS $$ (i,j) = (?S * ?M) $$ (i,j)" by simp qed auto from arg_cong[OF this, of det] det_mult[OF C(1) C(3)] have "subresultant J (smult c f) g = subresultant J f g * det ?M" unfolding subresultant_def by auto also have "det ?M = [:c ^ ?m :]" proof (subst det_upper_triangular[OF _ C(3)]) show "upper_triangular ?M" by (rule upper_triangularI, auto) have "prod_list (diag_mat ?M) = (\k = 0.. = (\k = 0..k = ?m..k = 0..k = 0..k = 0..k = ?m..k = ?m.. ((if j < ?k then j + ?n else j - ?k) < ?n) = (\ (j < ?k))" for j by auto have "subresultant J f g = det ?A" unfolding subresultant_def by simp also have "\ = (-1)^(?k * ?n) * det (mat (?k + ?n) (?k + ?n) (\ (i,j). ?A $$ (i,(if j < ?k then j + ?n else j - ?k))))" (is "_ = _ * det ?B") by (rule det_swap_cols, auto simp: subresultant_mat_def Let_def) also have "?B = subresultant_mat J g f" unfolding subresultant_mat_def Let_def by (rule eq_matI, unfold dim_row_mat dim_col_mat nk index_mat split, subst index_mat, (auto)[2], unfold split, subst change, force, unfold if_conn, rule if_cong[OF refl if_cong if_cong], auto) also have "det \ = subresultant J g f" unfolding subresultant_def .. also have "(-1)^(?k * ?n) * \ = [: (-1)^(?k * ?n) :] * \ " by (unfold hom_distribs, simp) also have "\ = smult ((-1)^(?k * ?n)) (subresultant J g f)" by simp finally show ?thesis . qed lemma subresultant_smult_right:assumes "(c :: 'a :: {comm_ring_1, semiring_no_zero_divisors}) \ 0" shows "subresultant J f (smult c g) = smult (c ^ (degree f - J)) (subresultant J f g)" unfolding subresultant_swap[of _ f] subresultant_smult_left[OF assms] degree_smult_eq using assms by (simp add: ac_simps) lemma coeff_subresultant: "coeff (subresultant J F G) l = (if degree F - J + (degree G - J) = 0 \ l \ 0 then 0 else det (subresultant'_mat J l F G))" proof (cases "degree F - J + (degree G - J) = 0") case True show ?thesis unfolding subresultant_def subresultant_mat_def subresultant'_mat_def Let_def True by simp next case False let ?n = "degree F - J + (degree G - J)" define n where "n = ?n" from False have n: "n \ 0" unfolding n_def by auto hence id: "{0..i = 0..i = 0 ..< (n - 1). coeff_int (M $$ (i, p i)) 0) * coeff_int (M $$ (n - 1, p (n - 1))) l" unfolding id proof (rule coeff_int_prod_const, (auto)[2]) fix i assume "i \ {0 ..< n - 1}" with p have i: "i \ n - 1" and "i < n" "p i < n" by (auto simp: n_def) note id = subresultant_index_mat[OF this(2-3)[unfolded n_def], folded M_def n_def] show "degree (M $$ (i, p i)) = 0" unfolding id Let_def using i by (simp split: if_splits) qed also have "(\i = 0 ..< (n - 1). coeff_int (M $$ (i, p i)) 0) = (\i = 0 ..< (n - 1). L $$ (i, p i))" proof (rule prod.cong[OF refl]) fix i assume "i \ {0 ..< n - 1}" with p have i: "i \ n - 1" and ii: "i < n" "p i < n" by (auto simp: n_def) note id = subresultant_index_mat[OF this(2-3)[unfolded n_def], folded M_def n_def] note id' = L_def[unfolded subresultant'_mat_def Let_def, folded n_def] index_mat[OF ii] show "coeff_int (M $$ (i, p i)) 0 = L $$ (i, p i)" unfolding id id' split using i proof (simp add: if_splits Let_def) qed qed also have "coeff_int (M $$ (n - 1, p (n - 1))) l = (if p (n - 1) < degree G - J then coeff_int (monom 1 (degree G - J - 1 - p (n - 1)) * F) l else coeff_int (monom 1 (degree F - J - 1 - (p (n - 1) - (degree G - J))) * G) l)" using subresultant_index_mat[OF n1[unfolded n_def], folded M_def n_def, unfolded idn if_True Let_def] by simp also have "\ = (if p (n - 1) < degree G - J then coeff_int F (int l - int (degree G - J - 1 - p (n - 1))) else coeff_int G (int l - int (degree F - J - 1 - (p (n - 1) - (degree G - J)))))" unfolding coeff_int_monom_mult by simp also have "\ = (if p (n - 1) < degree G - J then coeff_int F (int l - int (degree G - J - 1) + p (n - 1)) else coeff_int G (int l - int (degree F - J - 1) + (p (n - 1) - (degree G - J))))" proof (cases "p (n - 1) < degree G - J") case True hence "int (degree G - J - 1 - p (n - 1)) = int (degree G - J - 1) - p (n - 1)" by simp hence id: "int l - int (degree G - J - 1 - p (n - 1)) = int l - int (degree G - J - 1) + p (n - 1)" by simp show ?thesis using True unfolding id by simp next case False from n1 False have "degree F - J - 1 \ p (n - 1) - (degree G - J)" unfolding n_def by linarith hence "int (degree F - J - 1 - (p (n - 1) - (degree G - J))) = int (degree F - J - 1) - (p (n - 1) - (degree G - J))" by linarith hence id: "int l - int (degree F - J - 1 - (p (n - 1) - (degree G - J))) = int l - int (degree F - J - 1) + (p (n - 1) - (degree G - J))" by simp show ?thesis unfolding id using False by simp qed also have "\ = L $$ (n - 1, p (n - 1))" unfolding L_def subresultant'_mat_def Let_def n_def[symmetric] using n1 by simp also have "(\i = 0.. = (\i = 0..i = 0..i = 0..p\{p. p permutes {0..i = 0.. = (\p\{p. p permutes {0..i = 0.. = det L" proof - have id: "dim_row (subresultant'_mat J l F G) = n" "dim_col (subresultant'_mat J l F G) = n" unfolding subresultant'_mat_def Let_def n_def by auto show ?thesis unfolding det_def L_def id by simp qed finally show ?thesis unfolding L_def coeff_int_def using False by auto qed lemma subresultant'_zero_ge: assumes "(degree f - J) + (degree g - J) \ 0" and "k \ degree f + (degree g - J)" shows "det (subresultant'_mat J k f g) = 0" (* last row is zero *) proof - obtain dg where dg: "degree g - J = dg" by simp obtain df where df: "degree f - J = df" by simp obtain ddf where ddf: "degree f = ddf" by simp note * = assms(2)[unfolded ddf dg] assms(1) define M where "M = (\ i j. if j < dg then coeff_int f (degree f - int i + int j) else coeff_int g (degree g - int i + int (j - dg)))" let ?M = "subresultant'_mat J k f g" have M: "det ?M = det (mat (df + dg) (df + dg) (\(i, j). if i = df + dg - 1 then if j < dg then coeff_int f (int k - int (dg - 1) + int j) else coeff_int g (int k - int (df - 1) + int (j - dg)) else M i j))" (is "_ = det ?N") unfolding subresultant'_mat_def Let_def M_def by (rule arg_cong[of _ _ det], rule eq_matI, auto simp: df dg) also have "?N = mat (df + dg) (df + dg) (\(i, j). if i = df + dg - 1 then 0 else M i j)" by (rule cong_mat[OF refl refl], unfold split, rule if_cong[OF refl _ refl], auto simp add: coeff_int_def df dg ddf intro!: coeff_eq_0, insert *(1), unfold ddf[symmetric] dg[symmetric] df[symmetric], linarith+) also have "\ = mat\<^sub>r (df + dg) (df + dg) (\i. if i = df + dg - 1 then 0\<^sub>v (df + dg) else vec (df + dg) (\ j. M i j))" by (rule eq_matI, auto) also have "det \ = 0" by (rule det_row_0, insert *, auto simp: df[symmetric] dg[symmetric] ddf[symmetric]) finally show ?thesis . qed lemma subresultant'_zero_lt: assumes J: "J \ degree f" "J \ degree g" "J < k" and k: "k < degree f + (degree g - J)" shows "det (subresultant'_mat J k f g) = 0" (* last row is identical to last row - k *) proof - obtain dg where dg: "dg = degree g - J" by simp obtain df where df: "df = degree f - J" by simp note * = assms[folded df dg] define M where "M = (\ i j. if j < dg then coeff_int f (degree f - int i + int j) else coeff_int g (degree g - int i + int (j - dg)))" define N where "N = (\ j. if j < dg then coeff_int f (int k - int (dg - 1) + int j) else coeff_int g (int k - int (df - 1) + int (j - dg)))" let ?M = "subresultant'_mat J k f g" have M: "?M = mat (df + dg) (df + dg) (\(i, j). if i = df + dg - 1 then N j else M i j)" unfolding subresultant'_mat_def Let_def by (rule eq_matI, auto simp: df dg M_def N_def) also have "\ = mat (df + dg) (df + dg) (\(i, j). if i = df + dg - 1 then N j else if i = degree f + dg - 1 - k then N j else M i j)" (is "_ = ?N") unfolding N_def by (rule cong_mat[OF refl refl], unfold split, rule if_cong[OF refl refl], unfold M_def N_def, insert J k, auto simp: df dg intro!: arg_cong[of _ _ "coeff_int _"]) finally have id: "?M = ?N" . have deg: "degree f + dg - 1 - k < df + dg" "df + dg - 1 < df + dg" using k J unfolding df dg by auto have id: "row ?M (degree f + dg - 1 - k) = row ?M (df + dg - 1)" unfolding arg_cong[OF id, of row] by (rule eq_vecI, insert deg, auto) show ?thesis by (rule det_identical_rows[OF _ _ _ _ id, of "df + dg"], insert deg assms, auto simp: subresultant'_mat_def Let_def df dg) qed lemma subresultant'_mat_sylvester_mat: "transpose_mat (subresultant'_mat 0 0 f g) = sylvester_mat f g" proof - obtain dg where dg: "degree g = dg" by simp obtain df where df: "degree f = df" by simp let ?M = "transpose_mat (subresultant'_mat 0 0 f g)" let ?n = "degree f + degree g" have dim: "dim_row ?M = ?n" "dim_col ?M = ?n" by (auto simp: subresultant'_mat_def Let_def) show ?thesis proof (rule eq_matI, unfold sylvester_mat_dim dim df dg, goal_cases) case ij: (1 i j) have "?M $$ (i,j) = (if i < dg then if j = df + dg - 1 then coeff_int f (- int (dg - 1) + int i) else coeff_int f (int df - int j + int i) else if j = df + dg - 1 then coeff_int g (- int (df - 1) + int (i - dg)) else coeff_int g (int dg - int j + int (i - dg)))" using ij unfolding subresultant'_mat_def Let_def by (simp add: if_splits df dg) also have "\ = (if i < dg then coeff_int f (int df - int j + int i) else coeff_int g (int dg - int j + int (i - dg)))" proof - have cong: "(b \ x = z) \ (\ b \ y = z) \ (if b then coeff_int f x else coeff_int f y) = coeff_int f z" for b x y z and f :: "'a poly" by auto show ?thesis by (rule if_cong[OF refl cong cong], insert ij, auto) qed also have "\ = sylvester_mat f g $$ (i,j)" proof - have *: "i \ j \ j - i \ df \ nat (int df - int j + int i) = df - (j - i)" for j i df by simp show ?thesis unfolding sylvester_index_mat[OF ij[folded df dg]] df dg proof (rule if_cong[OF refl]) assume i: "i < dg" have "int df - int j + int i < 0 \ \ j - i \ df" by auto thus "coeff_int f (int df - int j + int i) = (if i \ j \ j - i \ df then coeff f (df + i - j) else 0)" using i ij by (simp add: coeff_int_def *, intro impI coeff_eq_0[of f, unfolded df], linarith) next assume i: "\ i < dg" hence **: "i - dg \ j \ dg - (j + dg - i) = i - j" using ij by linarith have "int dg - int j + int (i - dg) < 0 \ \ j \ i" by auto thus "coeff_int g (int dg - int j + int (i - dg)) = (if i - dg \ j \ j \ i then coeff g (i - j) else 0)" using ij i by (simp add: coeff_int_def * **, intro impI coeff_eq_0[of g, unfolded dg], linarith) qed qed finally show ?case . qed auto qed lemma coeff_subresultant_0_0_resultant: "coeff (subresultant 0 f g) 0 = resultant f g" proof - let ?M = "transpose_mat (subresultant'_mat 0 0 f g)" have "det (subresultant'_mat 0 0 f g) = det ?M" by (subst det_transpose, auto simp: subresultant'_mat_def Let_def) also have "?M = sylvester_mat f g" by (rule subresultant'_mat_sylvester_mat) finally show ?thesis by (simp add: coeff_subresultant resultant_def) qed lemma subresultant_zero_ge: assumes "k \ degree f + (degree g - J)" and "(degree f - J) + (degree g - J) \ 0" shows "coeff (subresultant J f g) k = 0" unfolding coeff_subresultant by (subst subresultant'_zero_ge[OF assms(2,1)], simp) lemma subresultant_zero_lt: assumes "k < degree f + (degree g - J)" and "J \ degree f" "J \ degree g" "J < k" shows "coeff (subresultant J f g) k = 0" unfolding coeff_subresultant by (subst subresultant'_zero_lt[OF assms(2,3,4,1)], simp) lemma subresultant_resultant: "subresultant 0 f g = [: resultant f g :]" proof (cases "degree f + degree g = 0") case True thus ?thesis unfolding subresultant_def subresultant_mat_def resultant_def Let_def sylvester_mat_def sylvester_mat_sub_def by simp next case 0: False show ?thesis proof (rule poly_eqI) fix k show "coeff (subresultant 0 f g) k = coeff [:resultant f g:] k" proof (cases "k = 0") case True thus ?thesis using coeff_subresultant_0_0_resultant[of f g] by auto next case False hence "0 < k \ k < degree f + degree g \ k \ degree f + degree g" by auto thus ?thesis using subresultant_zero_ge[of f g 0 k] 0 subresultant_zero_lt[of k f g 0] 0 False by (cases k, auto) qed qed qed lemma (in inj_comm_ring_hom) subresultant_hom: "map_poly hom (subresultant J f g) = subresultant J (map_poly hom f) (map_poly hom g)" proof - note d = subresultant_mat_def Let_def interpret p: map_poly_inj_comm_ring_hom hom.. show ?thesis unfolding subresultant_def unfolding p.hom_det[symmetric] proof (rule arg_cong[of _ _ det]) show "p.mat_hom (subresultant_mat J f g) = subresultant_mat J (map_poly hom f) (map_poly hom g)" proof (rule eq_matI, goal_cases) case (1 i j) hence ij: "i < degree f - J + (degree g - J)" "j < degree f - J + (degree g - J)" unfolding d degree_map_poly by auto show ?case by (auto simp add: coeff_int_def d map_mat_def index_mat(1)[OF ij] hom_distribs) qed (auto simp: d) qed qed text \We now derive properties of the resultant via the connection to subresultants.\ lemma resultant_smult_left: assumes "(c :: 'a :: idom) \ 0" shows "resultant (smult c f) g = c ^ degree g * resultant f g" unfolding coeff_subresultant_0_0_resultant[symmetric] subresultant_smult_left[OF assms] coeff_smult by simp lemma resultant_smult_right: assumes "(c :: 'a :: idom) \ 0" shows "resultant f (smult c g) = c ^ degree f * resultant f g" unfolding coeff_subresultant_0_0_resultant[symmetric] subresultant_smult_right[OF assms] coeff_smult by simp lemma resultant_swap: "resultant f g = (-1)^(degree f * degree g) * (resultant g f)" unfolding coeff_subresultant_0_0_resultant[symmetric] unfolding arg_cong[OF subresultant_swap[of 0 f g], of "\ x. coeff x 0"] coeff_smult by simp text \The following equations are taken from Brown-Traub ``On Euclid's Algorithm and the Theory of Subresultant'' (BT)\ lemma fixes F B G H :: "'a :: idom poly" and J :: nat defines df: "df \ degree F" and dg: "dg \ degree G" and dh: "dh \ degree H" and db: "db \ degree B" defines n: "n \ (df - J) + (dg - J)" and f: "f \ coeff_int F" and b: "b \ coeff_int B" and g: "g \ coeff_int G" and h: "h \ coeff_int H" assumes FGH: "F + B * G = H" and dfg: "df \ dg" and choice: "dg > dh \ H = 0 \ F \ 0 \ G \ 0" shows BT_eq_18: "subresultant J F G = smult ((-1)^((df - J) * (dg - J))) (det (mat n n (\ (i,j). if j < df - J then if i = n - 1 then monom 1 ((df - J) - 1 - j) * G else [:g (int dg - int i + int j):] else if i = n - 1 then monom 1 ((dg - J) - 1 - (j - (df - J))) * H else [:h (int df - int i + int (j - (df - J))):])))" (is "_ = smult ?m1 ?right") and BT_eq_19: "dh \ J \ J < dg \ subresultant J F G = smult ( (-1)^((df - J) * (dg - J)) * lead_coeff G ^ (df - J) * coeff H J ^ (dg - J - 1)) H" (is "_ \ _ \ _ = smult (_ * ?G * ?H) H") and BT_lemma_1_12: "J < dh \ subresultant J F G = smult ( (-1)^((df - J) * (dg - J)) * lead_coeff G ^ (df - dh)) (subresultant J G H)" and BT_lemma_1_13': "J = dh \ dg > dh \ H \ 0 \ subresultant dh F G = smult ( (-1)^((df - dh) * (dg - dh)) * lead_coeff G ^ (df - dh) * lead_coeff H ^ (dg - dh - 1)) H" and BT_lemma_1_14: "dh < J \ J < dg - 1 \ subresultant J F G = 0" and BT_lemma_1_15': "J = dg - 1 \ dg > dh \ H \ 0 \ subresultant (dg - 1) F G = smult ( (-1)^(df - dg + 1) * lead_coeff G ^ (df - dg + 1)) H" proof - define dfj where "dfj = df - J" define dgj where "dgj = dg - J" note d = df dg dh db have F0: "F \ 0" using dfg choice df by auto have G0: "G \ 0" using choice dg by auto have dgh: "dg \ dh" using choice unfolding dh by auto have B0: "B \ 0" using FGH dfg dgh choice F0 G0 unfolding d by auto have dfh: "df \ dh" using dfg dgh by auto have "df = degree (B * G)" proof (cases "H = 0") case False with choice dfg have dfh: "df > dh" by auto show ?thesis using dfh[folded arg_cong[OF FGH, of degree, folded dh]] choice unfolding df by (metis \degree (F + B * G) < df\ degree_add_eq_left degree_add_eq_right df nat_neq_iff) next case True have "F = - B * G" using arg_cong[OF FGH[unfolded True], of "\ x. x - B * G"] by auto thus ?thesis using F0 G0 B0 unfolding df by simp qed hence dfbg: "df = db + dg" using degree_mult_eq[OF B0 G0] by (simp add: d) hence dbfg: "db = df - dg" by simp let ?dfj = "df - J" let ?dgj = "dg - J" have norm: "?dgj + ?dfj = ?dfj + ?dgj" by simp let ?bij = "\ i j. b (db - int i + int (j - dfj))" let ?M = "mat n n (\ (i,j). if i = j then 1 else if j < dfj then 0 else if i < j then [: ?bij i j :] else 0)" (* this is the matrix which contains all the column-operations that are required to transform the subresultant-matrix of F and G into the one of G and H ( the matrix depicted in equation (18) in BT *) let ?GF = "\ i j. if j < dfj then if i = n - 1 then monom 1 (dfj - 1 - j) * G else [:g (int dg - int i + int j):] else if i = n - 1 then monom 1 (dgj - 1 - (j - dfj)) * F else [:f (int df - int i + int (j - dfj)):]" let ?G_F = "mat n n (\ (i,j). ?GF i j)" let ?GH = "\ i j. if j < dfj then if i = n - 1 then monom 1 (dfj - 1 - j) * G else [:g (int dg - int i + int j):] else if i = n - 1 then monom 1 (dgj - 1 - (j - dfj)) * H else [:h (int df - int i + int (j - dfj)):]" let ?G_H = "mat n n (\ (i,j). ?GH i j)" have hfg: "h i = f i + coeff_int (B * G) i" for i unfolding FGH[symmetric] f g h unfolding coeff_int_def by simp have dM1: "det ?M = 1" by (subst det_upper_triangular, (auto)[2], subst prod_list_diag_prod, auto) have "subresultant J F G = smult ?m1 (subresultant J G F)" unfolding subresultant_swap[of _ F] d by simp also have "subresultant J G F = det ?G_F" unfolding subresultant_def n norm subresultant_mat_def g f Let_def d[symmetric] dfj_def dgj_def by simp also have "\ = det (?G_F * ?M)" by (subst det_mult[of _ n], unfold dM1, auto) also have "?G_F * ?M = ?G_H" proof (rule eq_matI, unfold dim_col_mat dim_row_mat) fix i j assume i: "i < n" and j: "j < n" have "(?G_F * ?M) $$ (i,j) = row (?G_F) i \ col ?M j" using i j by simp also have "\ = ?GH i j" proof (cases "j < dfj") case True have id: "col ?M j = unit_vec n j" by (rule eq_vecI, insert True i j, auto) show ?thesis unfolding id using True i j by simp next case False define d where "d = j - dfj" from False have jd: "j = d + dfj" unfolding d_def by auto hence idj: "{0 ..< j} = {0 ..< dfj} \ {dfj ..< dfj + d}" by auto let ?H = "(if i = n - 1 then monom 1 (dgj - Suc d) * H else [:h (int df - int i + int d):])" have idr: "?GH i j = ?H" unfolding d_def using jd by auto let ?bi = "\ i. b (db - int i + int d)" let ?m = "\ i. if i = j then 1 else if i < j then [:?bij i j:] else 0" let ?P = "\ k. (?GF i k * ?m k)" let ?Q = "\ k. ?GF i k * [: ?bi k :]" let ?G = "\ k. if i = n - 1 then monom 1 (dfj - 1 - k) * G else [:g (int dg - int i + int k):]" let ?Gb = "\ k. ?G k * [:?bi k:]" let ?off = "- (int db - int dfj + 1 + int d)" have off0: "?off \ 0" using False dfg j unfolding dfj_def d_def dbfg n by simp from nat_0_le[OF this] obtain off where off: "int off = ?off" by blast have "int off \ int dfj" unfolding off by auto hence "off \ dfj" by simp hence split1: "{0 ..< dfj} = {0 ..< off} \ {off ..< dfj}" by auto have "int off + Suc db \ dfj" unfolding off by auto hence split2: "{off ..< dfj} = {off .. off + db} \ {off + Suc db ..< dfj} " by auto let ?g_b = "\k. (if i = n - 1 then monom 1 k * G else [:g (int dg - int i + int (dfj - Suc k)):]) * [:b (k - int off):]" let ?gb = "\k. (if i = n - 1 then monom 1 (k + off) * G else [:g (int dg - int i + int (dfj - Suc k - off)):]) * [:coeff B k:]" let ?F = "\ k. if i = n - 1 then monom 1 (dgj - 1 - (k - dfj)) * F else [:f (int df - int i + int (k - dfj)):]" let ?Fb = "\ k. ?F k * [:?bi k:]" let ?Pj = "if i = n - 1 then monom 1 (dgj - Suc d) * F else [:f (int df - int i + int d):]" from False have id: "col ?M j = vec n ?m" using j i by (intro eq_vecI, auto) have "row ?G_F i \ col ?M j = sum ?P {0 ..< n}" using i j unfolding id by (simp add: scalar_prod_def) also have "{0 ..< n} = {0 ..< j} \ {j} \ {Suc j ..< n}" using j by auto also have "sum ?P \ = sum ?P {0 ..< j} + ?P j + sum ?P {Suc j ..< n}" by (simp add: sum.union_disjoint) also have "sum ?P {Suc j ..< n} = 0" by (rule sum.neutral, auto) also have "?P j = ?Pj" unfolding d_def using jd by simp also have "sum ?P {0 ..< j} = sum ?Q {0 ..< j}" by (rule sum.cong[OF refl], unfold d_def, insert jd, auto) also have "sum ?Q {0 ..< j} = sum ?Q {0 ..< dfj} + sum ?Q {dfj ..< dfj+d}" unfolding idj by (simp add: sum.union_disjoint) also have "sum ?Q {0 ..< dfj} = sum ?Gb {0 ..< dfj}" by (rule sum.cong, auto) also have "sum ?Q {dfj ..< dfj+d} = sum ?Fb {dfj ..< dfj+d}" by (rule sum.cong, auto) also have "\ = 0" proof (rule sum.neutral, intro ballI) fix k assume k: "k \ {dfj ..< dfj+d}" hence k: "db + d < k" using k j False unfolding n db[symmetric] dfbg dfj_def d_def by auto let ?k = "(int db - int k + int d)" have "?k < 0" using k by auto hence "b ?k = 0" unfolding b by (intro coeff_int_eq_0, auto) thus "?Fb k = 0" by simp qed also have "sum ?Gb {0 ..< dfj} = sum ?g_b {0 ..< dfj}" proof (rule sum.reindex_cong[of "\ k. dfj - Suc k"], (auto simp: inj_on_def off)[2], goal_cases) case (1 k) hence "k = dfj - (Suc (dfj - Suc k))" and "(dfj - Suc k) \ {0.. = sum ?g_b {0 ..< off} + sum ?g_b {off ..< dfj}" unfolding split1 by (simp add: sum.union_disjoint) also have "sum ?g_b {0 ..< off} = 0" by (rule sum.neutral, intro ballI, auto simp: b coeff_int_def) also have "sum ?g_b {off ..< dfj} = sum ?g_b {off .. off + db} + sum ?g_b {off + Suc db ..< dfj}" unfolding split2 by (rule sum.union_disjoint, auto) also have "sum ?g_b {off + Suc db ..< dfj} = 0" proof (rule sum.neutral, intro ballI, goal_cases) case (1 k) hence "b (int k - int off) = 0" unfolding b db by (intro coeff_int_eq_0, auto) thus ?case by simp qed also have "sum ?g_b {off .. off + db} = sum ?gb {0 .. db}" using sum.atLeastAtMost_shift_bounds [of ?g_b 0 off db] by (auto intro: sum.cong simp add: b ac_simps) finally have id: "row ?G_F i \ col ?M j - ?H = ?Pj + sum ?gb {0 .. db} - ?H" (is "_ = ?E") by (simp add: ac_simps) define E where "E = ?E" let ?b = "coeff B" have Bsum: "(\k = 0..db. monom (?b k) k) = B" unfolding db using atMost_atLeast0 poly_as_sum_of_monoms by auto have "E = 0" proof (cases "i = n - 1") case i_n: False hence id: "(i = n - 1) = False" by simp with i have i: "i < n - 1" by auto let ?ii = "int df - int i + int d" have "?thesis = ([:f ?ii:] + (\k = 0..db. [:g (int dg - int i + int (dfj - Suc k - off)):] * [:?b k:]) - [:h ?ii:] = 0)" (is "_ = (?e = 0)") unfolding E_def id if_False by simp also have "?e = [: f ?ii + (\k = 0..db. g (int dg - int i + int (dfj - Suc k - off)) * ?b k) - h ?ii:]" (is "_ = [: ?e :]") proof (rule poly_eqI, goal_cases) case (1 n) show ?case unfolding coeff_diff coeff_add coeff_sum coeff_const by (cases n, auto simp: ac_simps) qed also have "[: ?e :] = 0 \ ?e = 0" by simp also have "?e = (\k = 0..db. g (int dg - int i + int (dfj - Suc k - off)) * ?b k) - coeff_int (B * G) ?ii" unfolding hfg by simp also have "(B * G) = (\k = 0..db. monom (?b k) k) * G" unfolding Bsum by simp also have "\ = (\k = 0..db. monom (?b k) k * G)" by (rule sum_distrib_right) also have "coeff_int \ ?ii = (\k = 0..db. g (?ii - k) * ?b k)" unfolding coeff_int_sum coeff_int_monom_mult g by (simp add: ac_simps) also have "\ = (\k = 0..db. g (int dg - int i + int (dfj - Suc k - off)) * ?b k)" proof (rule sum.cong[OF refl], goal_cases) case (1 k) hence "k \ db" by simp hence id: "int dg - int i + int (dfj - Suc k - off) = ?ii - k" using False i j off dfg unfolding dbfg d_def dfj_def n by linarith show ?case unfolding id .. qed finally show ?thesis by simp next case True let ?jj = "dgj - Suc d" have zero: "int off - (dgj - Suc d) = 0" using dfg False j unfolding off dbfg dfj_def d_def dgj_def n by linarith from True have "E = monom 1 ?jj * F + (\k = 0.. db. monom 1 (k + off) * G * [: ?b k :]) - monom 1 ?jj * H" (is "_ = ?A + ?sum - ?mon") unfolding id E_def by simp also have "?mon = monom 1 ?jj * F + monom 1 ?jj * (B * G)" unfolding FGH[symmetric] by (simp add: ring_distribs) also have "?A + ?sum - \ = ?sum - (monom 1 ?jj * G) * B" (is "_ = _ - ?GB * B") by simp also have "?sum = (\k = 0..db. (monom 1 ?jj * G) * (monom 1 (k + off - ?jj) * [: ?b k :]))" proof (rule sum.cong[OF refl], goal_cases) case (1 k) let ?one = "1 :: 'a" have "int off \ int ?jj" using j False i True unfolding off d_def dfj_def dgj_def dfbg n by linarith hence "k + off = ?jj + (k + off - ?jj)" by linarith hence id: "monom ?one (k + off) = monom (1 * 1) (?jj + (k + off - ?jj))" by simp show ?case unfolding id[folded mult_monom] by (simp add: ac_simps) qed also have "\ = (monom 1 ?jj * G) * (\k = 0..db. monom 1 (k + off - ?jj) * [:?b k:])" (is "_ = _ * ?sum") unfolding sum_distrib_left .. also have "\ - (monom 1 ?jj * G) * B = (monom 1 ?jj * G) * (?sum - B)" by (simp add: ring_distribs) also have "?sum = (\k = 0..db. monom 1 k * [:?b k:])" by (rule sum.cong[OF refl], insert zero, auto) also have "\ = (\k = 0..db. monom (?b k) k)" by (rule sum.cong[OF refl], rule poly_eqI, auto) also have "\ = B" unfolding Bsum .. finally show ?thesis by simp qed from id[folded E_def, unfolded this] show ?thesis using False unfolding d_def by simp qed also have "\ = ?G_H $$ (i,j)" using i j by simp finally show "(?G_F * ?M) $$ (i,j) = ?G_H $$ (i,j)" . qed auto finally show eq_18: "subresultant J F G = smult ?m1 (det ?G_H)" unfolding dfj_def dgj_def . { fix i j assume ij: "i < j" and j: "j < n" with dgh have "int dg - int i + int j > int dg" by auto hence "g (int dg - int i + int j) = 0" unfolding g dg by (intro coeff_int_eq_0, auto) } note g0 = this { assume *: "dh \ J" "J < dg" have n_dfj: "n > dfj" using * unfolding n dfj_def by auto note eq_18 also have "det ?G_H = prod_list (diag_mat ?G_H)" proof (rule det_lower_triangular[of n]) fix i j assume ij: "i < j" and j: "j < n" from ij j have if_e: "i = n - 1 \ False" by auto have "?G_H $$ (i,j) = ?GH i j" using ij j by auto also have "\ = 0" proof (cases "j < dfj") case True with True g0[OF ij j] show ?thesis unfolding if_e by simp next case False have "h (int df - int i + int (j - dfj)) = 0" unfolding h by (rule coeff_int_eq_0, insert False * ij j dfg, unfold dfj_def dh[symmetric], auto) with False show ?thesis unfolding if_e by auto qed finally show "?G_H $$ (i,j) = 0" . qed auto also have "\ = (\i = 0.. {dfj ..< n}" unfolding n dfj_def by auto also have "prod (\ i. ?GH i i) \ = prod (\ i. ?GH i i) {0 ..< dfj} * prod (\ i. ?GH i i) {dfj ..< n}" by (simp add: prod.union_disjoint) also have "prod (\ i. ?GH i i) {0 ..< dfj} = prod (\ i. [: lead_coeff G :]) {0 ..< dfj}" proof - show ?thesis by (rule prod.cong[OF refl], insert n_dfj, auto simp: g coeff_int_def dg) qed also have "\ = [: (lead_coeff G)^dfj :]" by (simp add: poly_const_pow) also have "{dfj ..< n} = {dfj ..< n-1} \ {n - 1}" using n_dfj by auto also have "prod (\ i. ?GH i i) \ = prod (\ i. ?GH i i) {dfj ..< n-1} * ?GH (n - 1) (n - 1)" by (simp add: prod.union_disjoint) also have "?GH (n - 1) (n - 1) = H" proof - have "dgj - 1 - (n - 1 - dfj) = 0" using n_dfj unfolding dgj_def dfj_def n by auto with n_dfj show ?thesis by auto qed also have "prod (\ i. ?GH i i) {dfj ..< n-1} = prod (\ i. [:h (int df - dfj):]) {dfj ..< n-1}" by (rule prod.cong[OF refl], auto intro!: arg_cong[of _ _ h]) also have "\ = [: h (int df - dfj) ^ (n - 1 - dfj) :]" unfolding prod_constant by (simp add: poly_const_pow) also have "n - 1 - dfj = dg - J - 1" unfolding n dfj_def by simp also have "int df - dfj = J" using * dfg unfolding dfj_def by auto also have "h J = coeff H J" unfolding h coeff_int_def by simp finally show "subresultant J F G = smult (?m1 * ?G * ?H) H" by (simp add: dfj_def ac_simps) } note eq_19 = this { assume J: "J < dh" define dhj where "dhj = dh - J" have n_add: "n = (df - dh) + (dhj + dgj)" unfolding dhj_def dgj_def n using J dfg dgh by auto let ?split = "split_block ?G_H (df - dh) (df - dh)" have dim: "dim_row ?G_H = (df - dh) + (dhj + dgj)" "dim_col ?G_H = (df - dh) + (dhj + dgj)" unfolding n_add by auto obtain UL UR LL LR where spl: "?split = (UL,UR,LL,LR)" by (cases ?split, auto) note spl' = spl[unfolded split_block_def Let_def, simplified] let ?LR = "subresultant_mat J G H" have "LR = mat (dgj + dhj) (dgj + dhj) (\ (i,j). ?GH (i + (df - dh)) (j + (df - dh)))" using spl' by (auto simp: n_add) also have "\ = ?LR" unfolding subresultant_mat_def Let_def dhj_def dgj_def d[symmetric] proof (rule eq_matI, unfold dim_row_mat dim_col_mat index_mat split dfj_def, goal_cases) case (1 i j) hence id1: "(j + (df - dh) < df - J) = (j < dh - J)" using dgh dfg J by auto have id2: "(i + (df - dh) = n - 1) = (i = dg - J + (dh - J) - 1)" unfolding n_add dhj_def dgj_def using dgh dfg J by auto have id3: "(df - J - 1 - (j + (df - dh))) = (dh - J - 1 - j)" and id4: "(int dg - int (i + (df - dh)) + int (j + (df - dh))) = (int dg - int i + int j)" and id5: "(dg - J - 1 - (j + (df - dh) - (df - J))) = (dg - J - 1 - (j - (dh - J)))" and id6: "(int df - int (i + (df - dh)) + int (j + (df - dh) - (df - J))) = (int dh - int i + int (j - (dh - J)))" using dgh dfg J by auto show ?case unfolding g[symmetric] h[symmetric] id3 id4 id5 id6 by (rule if_cong[OF id1 if_cong[OF id2 refl refl] if_cong[OF id2 refl refl]]) qed auto finally have "LR = ?LR" . note spl = spl[unfolded this] let ?UR = "0\<^sub>m (df - dh) (dgj + dhj)" have "UR = mat (df - dh) (dgj + dhj) (\ (i,j). ?GH i (j + (df - dh)))" using spl' by (auto simp: n_add) also have "\ = ?UR" proof (rule eq_matI, unfold dim_row_mat dim_col_mat index_mat split dfj_def index_zero_mat, goal_cases) case (1 i j) hence in1: "i \ n - 1" using J unfolding dgj_def dhj_def n_add by auto { assume "j + (df - dh) < df - J" hence "dg < int dg - int i + int (j + (df - dh))" using 1 J unfolding dgj_def dhj_def by auto hence "g \ = 0" unfolding dg g by (intro coeff_int_eq_0, auto) } note g = this { assume "\ (j + (df - dh) < df - J)" hence "dh < int df - int i + int (j + (df - dh) - (df - J))" using 1 J unfolding dgj_def dhj_def by auto hence "h \ = 0" unfolding dh h by (intro coeff_int_eq_0, auto) } note h = this show ?case using in1 g h by auto qed auto finally have "UR = ?UR" . note spl = spl[unfolded this] let ?G = "\ (i,j). if i = j then [:lead_coeff G:] else if i < j then 0 else ?GH i j" let ?UL = "mat (df - dh) (df - dh) ?G" have "UL = mat (df - dh) (df - dh) (\ (i,j). ?GH i j)" using spl' by (auto simp: n_add) also have "\ = ?UL" proof (rule eq_matI, unfold dim_row_mat dim_col_mat index_mat split, goal_cases) case (1 i j) { assume "i = j" hence "int dg - int i + int j = dg" using 1 by auto hence "g (int dg - int i + int j) = lead_coeff G" unfolding g dg coeff_int_def by simp } note eq = this { assume "i < j" hence "dg < int dg - int i + int j" using 1 by auto hence "g (int dg - int i + int j) = 0" unfolding g dg by (intro coeff_int_eq_0, auto) } note lt = this from 1 have *: "j < dfj" "i \ n - 1" using J unfolding n_add dhj_def dgj_def dfj_def by auto hence "?GH i j = [:g (int dg - int i + int j):]" by simp also have "\ = (if i = j then [: lead_coeff G :] else if i < j then 0 else ?GH i j)" using eq lt * by auto finally show ?case by simp qed auto finally have "UL = ?UL" . note spl = spl[unfolded this] from split_block[OF spl dim] have GH: "?G_H = four_block_mat ?UL ?UR LL ?LR" and C: "?UL \ carrier_mat (df - dh) (df - dh)" "?UR \ carrier_mat (df - dh) (dhj + dgj)" "LL \ carrier_mat (dhj + dgj) (df - dh)" "?LR \ carrier_mat (dhj + dgj) (dhj + dgj)" by auto from arg_cong[OF GH, of det] have "det ?G_H = det (four_block_mat ?UL ?UR LL ?LR)" unfolding GH[symmetric] .. also have "\ = det ?UL * det ?LR" by (rule det_four_block_mat_upper_right_zero[OF _ refl], insert C, auto simp: ac_simps) also have "det ?LR = subresultant J G H" unfolding subresultant_def by simp also have "det ?UL = prod_list (diag_mat ?UL)" by (rule det_lower_triangular[of "df - dh"], auto) also have "\ = (\i = 0..< (df - dh). [: lead_coeff G :])" unfolding prod_list_diag_prod by simp also have "\ = [: lead_coeff G ^ (df - dh) :]" by (simp add: poly_const_pow) finally have det: "det ?G_H = [:lead_coeff G ^ (df - dh):] * subresultant J G H" by auto show "subresultant J F G = smult (?m1 * lead_coeff G ^ (df - dh)) (subresultant J G H)" unfolding eq_18 det by simp } { assume J: "dh < J" "J < dg - 1" hence "dh \ J" "J < dg" by auto from eq_19[OF this] have "subresultant J F G = smult ((- 1) ^ ((df - J) * (dg - J)) * lead_coeff G ^ (df - J) * coeff H J ^ (dg - J - 1)) H" by simp also have "coeff H J = 0" by (rule coeff_eq_0, insert J, auto simp: dh) also have "\ ^ (dg - J - 1) = 0" using J by auto finally show "subresultant J F G = 0" by simp } { assume J: "J = dh" and "dg > dh \ H \ 0" with choice have dgh: "dg > dh" by auto show "subresultant dh F G = smult ( (-1)^((df - dh) * (dg - dh)) * lead_coeff G ^ (df - dh) * lead_coeff H ^ (dg - dh - 1)) H" unfolding eq_19[unfolded J, OF le_refl dgh] unfolding dh by simp } { assume J: "J = dg - 1" and "dg > dh \ H \ 0" with choice have dgh: "dg > dh" by auto have *: "dh \ dg - 1" "dg - 1 < dg" using dgh by auto have **: "df - (dg - 1) = df - dg + 1" "dg - (dg - 1) - 1 = 0" "dg - (dg - 1) = 1" using dfg dgh by linarith+ show "subresultant (dg - 1) F G = smult ( (-1)^(df - dg + 1) * lead_coeff G ^ (df - dg + 1)) H" unfolding eq_19[unfolded J, OF *] unfolding ** by simp } qed lemmas BT_lemma_1_13 = BT_lemma_1_13'[OF _ _ _ refl] lemmas BT_lemma_1_15 = BT_lemma_1_15'[OF _ _ _ refl] lemma subresultant_product: fixes F :: "'a :: idom poly" assumes "F = B * G" and FG: "degree F \ degree G" shows "subresultant J F G = (if J < degree G then 0 else if J < degree F then smult (lead_coeff G ^ (degree F - J - 1)) G else 1)" proof (cases "J < degree G") case J: True from assms have eq: "F + (-B) * G = 0" by auto from J have lt: "degree 0 < degree G \ b" for b by auto from BT_lemma_1_13[OF eq FG lt lt] have "subresultant 0 F G = 0" using J by auto with BT_lemma_1_14[OF eq FG lt, of J] have 00: "J = 0 \ J < degree G - 1 \ subresultant J F G = 0" by auto from BT_lemma_1_15[OF eq FG lt lt] J have 01: "subresultant (degree G - 1) F G = 0" by simp from J have "(J = 0 \ J < degree G - 1) \ J = degree G - 1" by linarith with 00 01 have "subresultant J F G = 0" by auto thus ?thesis using J by simp next case J: False hence dg: "degree G - J = 0" by simp let ?n = "degree F - J" have *: "(j :: nat) < 0 \ False" "j - 0 = j" for j by auto let ?M = "mat ?n ?n (\(i, j). if i = ?n - 1 then monom 1 (?n - 1 - j) * G else [:coeff_int G (int (degree G) - int i + int j):])" have "subresultant J F G = det ?M" unfolding subresultant_def subresultant_mat_def Let_def dg * by auto also have "det ?M = prod_list (diag_mat ?M)" by (rule det_lower_triangular[of ?n], auto intro: coeff_int_eq_0) also have "\ = (\i = 0..< ?n. ?M $$ (i,i))" unfolding prod_list_diag_prod by simp also have "\ = (\i = 0..< ?n. if i = ?n - 1 then G else [: lead_coeff G :])" by (rule prod.cong[OF refl], auto simp: coeff_int_def) also have "\ = (if J < degree F then smult (lead_coeff G ^ (?n - 1)) G else 1)" proof (cases "J < degree F") case True hence id: "{ 0 ..< ?n} = { 0 ..< ?n - 1} \ {?n - 1}" by auto have "(\i = 0..< ?n. if i = ?n - 1 then G else [: lead_coeff G :]) = (\i = 0 ..< ?n - 1. if i = ?n - 1 then G else [: lead_coeff G :]) * G" (is "_ = ?P * G") unfolding id by (subst prod.union_disjoint, auto) also have "?P = (\i = 0 ..< ?n - 1. [: lead_coeff G :])" by (rule prod.cong, auto) also have "\ = [: lead_coeff G ^ (?n - 1) :]" by (simp add: poly_const_pow) finally show ?thesis by auto qed auto finally have "subresultant J F G = (if J < degree F then smult (lead_coeff G ^ (degree F - J - 1)) G else 1)" . thus ?thesis using J by simp qed lemma resultant_pseudo_mod_0: assumes "pseudo_mod f g = (0 :: 'a :: idom_divide poly)" and dfg: "degree f \ degree g" and f: "f \ 0" and g: "g \ 0" shows "resultant f g = (if degree g = 0 then lead_coeff g^degree f else 0)" proof - let ?df = "degree f" let ?dg = "degree g" obtain d r where pd: "pseudo_divmod f g = (d,r)" by force from pd have r: "r = pseudo_mod f g" unfolding pseudo_mod_def by simp with assms pd have pd: "pseudo_divmod f g = (d,0)" by auto from pseudo_divmod[OF g pd] g obtain a q where prod: "smult a f = g * q" and a: "a \ 0" "a = lead_coeff g ^ (Suc ?df - ?dg)" by auto from a dfg have dfg: "degree g \ degree (smult a f)" by auto have g0: "degree g = 0 \ coeff g 0 = 0 \ g = 0" using leading_coeff_0_iff by fastforce from prod have "smult a f = q * g" by simp from arg_cong[OF subresultant_product[OF this dfg, of 0, unfolded subresultant_resultant resultant_smult_left[OF a(1)]], of "\ x. coeff x 0"] show ?thesis using a g0 by (cases "degree f", auto) qed locale primitive_remainder_sequence = fixes F :: "nat \ 'a :: idom_divide poly" and n :: "nat \ nat" and \ :: "nat \ nat" and f :: "nat \ 'a" and k :: nat and \ :: "nat \ 'a" assumes f: "\ i. f i = lead_coeff (F i)" and n: "\ i. n i = degree (F i)" and \: "\ i. \ i = n i - n (Suc i)" and n12: "n 1 \ n 2" and F12: "F 1 \ 0" "F 2 \ 0" and F0: "\ i. i \ 0 \ F i = 0 \ i > k" and \0: "\ i. \ i \ 0" and pmod: "\ i. i \ 3 \ i \ Suc k \ smult (\ i) (F i) = pseudo_mod (F (i - 2)) (F (i - 1))" begin lemma f10: "f 1 \ 0" and f20: "f 2 \ 0" unfolding f using F12 by auto lemma f0: "i \ 0 \ f i = 0 \ i > k" using F0[of i] unfolding f by auto lemma n_gt: assumes "2 \ i" "i < k" shows "n i > n (Suc i)" proof - from assms have "3 \ Suc i" "Suc i \ Suc k" by auto note pmod = pmod[OF this] from assms F0 have "F (Suc i - 1) \ 0" "F (Suc i) \ 0" by auto from pseudo_mod(2)[OF this(1), of "F (Suc i - 2)", folded pmod] this(2) show ?thesis unfolding n using \0 by auto qed lemma n_ge: assumes "1 \ i" "i < k" shows "n i \ n (Suc i)" using n12 n_gt[OF _ assms(2)] assms(1) by (cases "i = 1", auto simp: numeral_2_eq_2) lemma n_ge_trans: assumes "1 \ i" "i \ j" "j \ k" shows "n i \ n j" proof - from assms(2) have "j = i + (j - i)" by simp then obtain jj where j: "j = i + jj" by blast from assms(3)[unfolded j] show ?thesis unfolding j proof (induct jj) case (Suc j) from Suc(2) have "i + j \ k" by simp from Suc(1)[OF this] have IH: "n (i + j) \ n i" . have "n (Suc (i + j)) \ n (i + j)" by (rule n_ge, insert assms(1) Suc(2), auto) with IH show ?case by auto qed auto qed lemma delta_gt: assumes "2 \ i" "i < k" shows "\ i > 0" using n_gt[OF assms] unfolding \ by auto lemma k2:"2 \ k" by (metis le_cases linorder_not_le F0 F12(2) zero_order(2)) lemma k0: "k \ 0" using k2 by auto lemma ni2:"3 \ i \ i \ k \ n i \ n 2" by (metis Suc_numeral \ delta_gt k2 le_imp_less_Suc le_less n_ge_trans not_le one_le_numeral semiring_norm(5) zero_less_diff) end locale subresultant_prs_locale = primitive_remainder_sequence F n \ f k \ for F :: "nat \ 'a :: idom_divide fract poly" and n :: "nat \ nat" and \ :: "nat \ nat" and f :: "nat \ 'a fract" and k :: nat and \ :: "nat \ 'a fract" + fixes G1 G2 :: "'a poly" assumes F1: "F 1 = map_poly to_fract G1" and F2: "F 2 = map_poly to_fract G2" begin definition "\ i = (f (i - 1))^(Suc (\ (i - 2)))" lemma \0: "i > 1 \ \ i = 0 \ (i - 1) > k" unfolding \_def using f0[of "i - 1"] by auto lemma \_char: assumes "3 \ i" "i < k + 2" shows "\ i = (f (i - 1)) ^ (Suc (length (coeffs (F (i - 2)))) - length (coeffs (F (i - 1))))" proof (cases "i = 3") case True have triv:"Suc (Suc 0) = 2" by auto have l:"length (coeffs (F 2)) \ 0" "length (coeffs (F 1)) \ 0" using F12 by auto hence "length (coeffs (F 2)) \ length (coeffs (F (Suc 0)))" using n12 unfolding n degree_eq_length_coeffs One_nat_def by linarith hence "Suc (length (coeffs (F 1)) - 1 - (length (coeffs (F 2)) - 1)) = (Suc (length (coeffs (F 1))) - length (coeffs (F (3 - 1))))" using l by simp thus ?thesis unfolding True \_def n \ degree_eq_length_coeffs by (simp add:triv) next case False hence assms:"2 \ i - 2" "i - 2 < k" using assms by auto have i:"i - 2 \ 0" "i - 1 \ 0" using assms by auto hence [simp]: "Suc (i - 2) = i - 1" by auto from assms(2) F0[OF i(2)] have "F (i - 1) \ 0" by auto then have "length (coeffs (F (i - 1))) > 0" by (cases "F (i - 1)") auto with delta_gt[unfolded \ n degree_eq_length_coeffs,OF assms] have * : "Suc (\ (i - 2)) = Suc (length (coeffs (F (i - 2)))) - (length (coeffs (F (Suc (i - 2)))))" by (auto simp:\ n degree_eq_length_coeffs) show ?thesis unfolding \_def * by simp qed definition Q :: "nat \ 'a fract poly" where "Q i \ smult (\ i) (fst (pdivmod (F (i - 2)) (F (i - 1))))" lemma beta_F_as_sum: assumes "3 \ i" "i \ Suc k" shows "smult (\ i) (F i) = smult (\ i) (F (i - 2)) + - Q i * F (i - 1)" (is ?t1) proof - have ik:"i < k + 2" using assms by auto have f0:"F (i - 1) = 0 \ False" "F (i - Suc 0) = 0 \ False" using F0[of "i - 1"] assms by auto hence f0_b:"(inverse (coeff (F (i - 1)) (degree (F (i - 1))))) \ 0" "F (i - 1) \ 0" by auto have i:"i - 2 \ 0" "Suc (i - 2) = i - 1" "(k < i - 2) \ False" using assms by auto have "F (i - 2) \ 0" using F0[of "i - 2"] assms by auto let ?c = "(inverse (f (i - 1)) ^ (Suc (length (coeffs (F (i - 2)))) - length (coeffs (F (i - 1)))))" have inv:"inverse (\ i) = ?c" unfolding \_char[OF assms(1) ik] power_inverse by auto have alpha0:"\ i \ 0" unfolding \_def f using f0 by auto have \_inv[simp]:"\ i * inverse (\ i) = 1" using field_class.field_inverse[OF alpha0] mult.commute by metis with field_class.field_inverse[OF alpha0,unfolded inv] have c_times_Q:"smult ?c (Q i) = fst (pdivmod (F (i - 2)) (F (i - 1)))" unfolding Q_def by auto have "pdivmod (F (i - 2)) (F (i - 1)) = (smult ?c (Q i), smult ?c (smult (\ i) (F i)))" unfolding c_times_Q unfolding pdivmod_via_pseudo_divmod pmod[OF assms] f n c_times_Q pseudo_mod_smult_right[OF f0_b, of "F (i - 2)",symmetric] f0 if_False Let_def unfolding pseudo_mod_def by (auto split:prod.split) - from this[folded pdivmod_pdivmodrel] - have pr:"F (i - 2) = smult ?c (Q i) * F (i - 1) + smult ?c ( smult (\ i) (F i))" - by (auto simp: eucl_rel_poly_iff) - hence "F (i - 2) = smult (inverse (\ i)) (Q i) * F (i - 1) + from this [symmetric] + have pr: \F (i - 2) = smult ?c (Q i) * F (i - 1) + smult ?c ( smult (\ i) (F i))\ + by (simp only: prod_eq_iff fst_conv snd_conv div_mult_mod_eq) + then have "F (i - 2) = smult (inverse (\ i)) (Q i) * F (i - 1) + smult (inverse (\ i)) ( smult (\ i) (F i))" (is "?l = ?r" is "_ = ?t + _") unfolding inv. hence eq:"smult (\ i) (?l - ?t) = smult (\ i) (?r - ?t)" by auto have " smult (\ i) (F (i - 2)) - Q i * (F (i - 1)) = smult (\ i) (?l - ?t)" unfolding smult_diff_right by auto also have "\ = smult (\ i) (?r - ?t)" unfolding eq.. also have "\ = smult (\ i) (F i)" by (auto simp:mult.assoc[symmetric]) finally show ?t1 by auto qed lemma assumes "3 \ i" "i \ k" shows BT_lemma_2_21: "j < n i \ smult (\ i ^ (n (i - 1) - j)) (subresultant j (F (i - 2)) (F (i - 1))) = smult ((- 1) ^ ((n (i - 2) - j) * (n (i - 1) - j)) * (f (i - 1)) ^ (\ (i - 2) + \ (i - 1)) * (\ i) ^ (n (i - 1) - j)) (subresultant j (F (i - 1)) (F i))" (is "_ \ ?eq_21") and BT_lemma_2_22: "smult (\ i ^ (\ (i - 1))) (subresultant (n i) (F (i - 2)) (F (i - 1))) = smult ((- 1) ^ ((\ (i - 2) + \ (i - 1)) * \ (i - 1)) * f (i - 1) ^ (\ (i - 2) + \ (i - 1)) * f i ^ (\ (i - 1) - 1) * (\ i) ^ \ (i - 1)) (F i)" (is "?eq_22") and BT_lemma_2_23: "n i < j \ j < n (i - 1) - 1 \ subresultant j (F (i - 2)) (F (i - 1)) = 0" (is "_ \ _ \ ?eq_23") and BT_lemma_2_24: "smult (\ i) (subresultant (n (i - 1) - 1) (F (i - 2)) (F (i - 1))) = smult ((- 1) ^ (\ (i - 2) + 1) * f (i - 1) ^ (\ (i - 2) + 1) * \ i) (F i)" (is "?eq_24") proof - from assms have ik:"i \ Suc k" by auto note beta_F_as_sum = beta_F_as_sum[OF assms(1) ik, symmetric] have s[simp]:"Suc (i - 2) = i - 1" "Suc (i - 1) = i" using assms by auto have \0:"\ i \ 0" using assms f0[of "i - 1"] unfolding \_def f by auto hence \0pow:"\ x. \ i ^ x \ 0" by auto have df:"degree (F (i - 1)) \ degree (smult (\ i) (F (i - 2)))" "degree (smult (\ i) (F i)) < degree (F (i - 1)) \ b" for b using n_ge[of "i-2"] n_gt[of "i-1"] assms \0 \0 unfolding n by auto have degree_smult_eq:"\ c f. (c::_::{idom_divide}) \ 0 \ degree (smult c f) = degree f" by auto have n_lt:"n i < n (i - 1)" using n_gt[of "i-1"] assms unfolding n by auto from semiring_normalization_rules(30) mult.commute have *:"\ x y q. (x * (y::'a fract)) ^ q = y ^ q * x ^ q" by metis have "n (i - 1) - n i > 0" using n_lt by auto hence **:"\ i ^ (n (i - 1) - n i - 1) * \ i = \ i ^ (n (i - 1) - n i)" by (subst power_minus_mult) auto have "max (n (i - 2)) (n (i - 1)) = n (i - 2)" using n_ge[of "i-2"] assms unfolding max_def by auto with diff_add_assoc[OF n_ge[of "i-1"],symmetric] assms have ns : "n (i - 2) - n (i - 1) + (n (i - 1) - n i) = n (i - 2) - n i" by (auto simp:nat_minus_add_max) { assume "j < n i" hence j:"j < degree (smult (\ i) (F i))" using \0 unfolding n by auto from BT_lemma_1_12[OF beta_F_as_sum df j] show ?eq_21 unfolding subresultant_smult_right[OF \0] subresultant_smult_left[OF \0] degree_smult_eq[OF \0] degree_smult_eq[OF \0] n[symmetric] f[symmetric] \ s ns using f n by auto} { from BT_lemma_1_13[OF beta_F_as_sum df df(2)] show ?eq_22 unfolding subresultant_smult_left[OF \0] lead_coeff_smult smult_smult degree_smult_eq[OF \0] degree_smult_eq[OF \0] n[symmetric] f[symmetric] \ s ns by (metis (no_types, lifting) * ** coeff_smult f mult.assoc n)} { assume "n i < j" "j < n (i - 1) - 1" hence j:"degree (smult (\ i) (F i)) < j" "j < degree (F (i - 1)) - 1" using \0 unfolding n by auto from BT_lemma_1_14[OF beta_F_as_sum df j] show ?eq_23 unfolding subresultant_smult_left[OF \0] smult_eq_0_iff using \0pow by auto} { have ***: "n (i - 1) - (n (i - 1) - 1) = 1" using n_lt by auto from BT_lemma_1_15[OF beta_F_as_sum df df(2)] show ?eq_24 unfolding subresultant_smult_left[OF \0] *** degree_smult_eq[OF \0] n[symmetric] f \ by (auto simp:mult.commute)} qed lemma BT_eq_30: "3 \ i \ i \ k + 1 \ j < n (i - 1) \ smult (\l\[3.. l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2)) = smult (\l\[3.. l ^ (n (l - 1) - j) * f (l - 1) ^ (\ (l - 2) + \ (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1)))" proof (induct "i - 3" arbitrary:i) case (Suc x) from Suc.hyps(2) Suc.prems(1-2) have prems:"x = (i - 1) - 3" "3 \ i - 1" "i - 1 \ k + 1" "2 \ i - 1 - 1" "i - 1 - 1 < k" "i - 1 \ k" by auto from prems(2) have inset:"i - 1 \ set [3.. c d e x. smult c d = e \ smult (x * c) d = smult x e" by auto have **:"\ c d e x. smult c d = e \ smult c (smult x d) = smult x e" by (auto simp:mult.commute) show ?case unfolding prod_list_map_remove1[OF inset(1),unfolded r1] *[OF Suc.hyps(1)[OF prems(1-3) j]] **[OF BT_lemma_2_21[OF prems(2,6) Suc.prems(3)]] by (auto simp: numeral_2_eq_2 ac_simps) qed auto lemma nonzero_alphaprod: assumes "i \ k + 1" shows "(\l\[3.. l ^ (p l)) \ 0" unfolding prod_list_zero_iff using assms by (auto simp: \0) lemma BT_eq_30': assumes i: "3 \ i" "i \ k + 1" "j < n (i - 1)" shows "subresultant j (F 1) (F 2) = smult ((- 1) ^ (\l\[3..l\[3.. l / \ l) ^ (n (l - 1) - j)) * (\l\[3.. (l - 2) + \ (l - 1)))) (subresultant j (F (i - 2)) (F (i - 1)))" (is "_ = smult (?mm * ?b * ?f) _") proof - let ?a = "\l\[3.. l ^ (n (l - 1) - j)" let ?d = "\l\[3.. l ^ (n (l - 1) - j) * f (l - 1) ^ (\ (l - 2) + \ (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))" let ?m = "\l\[3.. 0" by (rule nonzero_alphaprod, rule i) with arg_cong[OF BT_eq_30[OF i], of "smult (inverse ?a)", unfolded smult_smult] have "subresultant j (F 1) (F 2) = smult (inverse ?a * ?d) (subresultant j (F (i - 2)) (F (i - 1)))" by simp also have "inverse ?a * ?d = ?b * ?f * ?m" unfolding prod_list_multf inverse_prod_list map_map o_def power_inverse[symmetric] power_mult_distrib divide_inverse_commute by simp also have "?m = ?mm" unfolding prod_list_minus_1_exp by simp finally show ?thesis by (simp add: ac_simps) qed text \For defining the subresultant PRS, we mainly follow Brown's ``The Subresultant PRS Algorithm'' (B).\ definition "R j = (if j = n 2 then sdiv_poly (smult ((lead_coeff G2)^(\ 1)) G2) (lead_coeff G2) else subresultant j G1 G2)" abbreviation "ff i \ to_fract (i :: 'a)" abbreviation "ffp \ map_poly ff" sublocale map_poly_hom: map_poly_inj_idom_hom to_fract.. (* for \ and \ we only take additions, so that no negative number-problems occur *) definition "\ i = (\l\[3.. i = (\l\[3.. i = (-1)^(\ i) * pow_int ( f (i - 1)) (1 - int (\ (i - 1))) * (\l\[3.. l / \ l)^(n (l - 1) - n (i - 1) + 1) * (f (l - 1))^(\ (l - 2) + \ (l - 1)))" definition "\ i = (-1)^(\ i) * pow_int (f i) (int (\ (i - 1)) - 1) * (\l\[3.. l / \ l)^(n (l - 1) - n i) * (f (l - 1))^(\ (l - 2) + \ (l - 1)))" (* is eq 29 in BT *) lemma fundamental_theorem_eq_4: assumes i: "3 \ i" "i \ k" shows "ffp (R (n (i - 1) - 1)) = smult (\ i) (F i)" proof - have "n (i - 1) \ n 2" by (rule n_ge_trans, insert i, auto) with n_gt[of "i - 1"] i have "n (i - 1) - 1 < n 2" and lt: "n (i - 1) - 1 < n (i - 1)" by linarith+ hence "R (n (i - 1) - 1) = subresultant (n (i - 1) - 1) G1 G2" unfolding R_def by auto from arg_cong[OF this, of ffp, unfolded to_fract_hom.subresultant_hom, folded F1 F2] have id1: "ffp (R (n (i - 1) - 1)) = subresultant (n (i - 1) - 1) (F 1) (F 2)" . note eq_24 = BT_lemma_2_24[OF i] let ?o = "(- 1) :: 'a fract" let ?m1 = "(\ (i - 2) + 1)" let ?d1 = "f (i - 1) ^ (\ (i - 2) + 1) * \ i" let ?c1 = "?o ^ ?m1 * ?d1" let ?c0 = "\ i" have "?c0 \ 0" using \0[of i] i by auto with arg_cong[OF eq_24, of "smult (inverse ?c0)"] have id2: "subresultant (n (i - 1) - 1) (F (i - 2)) (F (i - 1)) = smult (inverse ?c0 * ?c1) (F i)" by (auto intro: poly_eqI) from i have "3 \ i" "i \ k + 1" by auto note id3 = BT_eq_30'[OF this lt] let ?f = "\ l. f (l - 1) ^ (\ (l - 2) + \ (l - 1))" let ?b = "\ l. (\ l / \ l) ^ (n (l - 1) - (n (i - 1) - 1))" let ?b' = "\ l. (\ l / \ l) ^ (n (l - 1) - n (i - 1) + 1)" let ?m = "\ l. (n (l - 2) - (n (i - 1) - 1)) * (n (l - 1) - (n (i - 1) - 1))" let ?m' = "\ l. (n (l - 2) + n (i - 1) + 1) * (n (l - 1) + n (i - 1) + 1)" let ?m2 = "(\l\[3.. i = ?o ^ (?m1 + ?m2) * (inverse ?c0 * ?d1 * ?b2 * ?f2)" proof - have id: "\ i = (-1)^(\ i) * (?f1 * (\l\[3..l\[3.._def prod_list_multf by simp have cong: "even m1 = even m2 \ c1 = c2 \ ?o^m1 * c1 = ?o^m2 * c2" for m1 m2 c1 c2 unfolding minus_1_power_even by auto show ?thesis unfolding id proof (rule cong) from n_gt[of "i - 1"] i have n1: "n (i - 1) \ 0" by linarith { fix l assume "2 \ l" "l \ i" hence l: "l \ 2" "l - 1 \ i - 1" "l \ k" using i by auto from n_ge_trans[OF _ l(2)] l i have n2: "n (i - 1) \ n (l - 1)" by auto from n1 n2 have id: "n (l - 1) - (n (i - 1) - 1) = n (l - 1) - n (i - 1) + 1" by auto have "even (n (l - 1) - (n (i - 1) - 1)) = even (n (l - 1) + n (i - 1) + 1)" unfolding id using n2 by auto note id n2 this } note diff = this have f0: "f (i - 1) \ 0" using f0[of "i - 1"] i by auto have "(\l\[3..l\[3.. = ?b2 * ?b i" using i by auto finally have "?f1 * (\l\[3..l\[3.. i * inverse ?c0" using n1 by (simp add: divide_inverse) also have "?f1 * ?f i = f (i - 1) ^ (\ (i - 2) + 1)" unfolding exp_pow_int pow_int_add[OF f0, symmetric] by simp finally show "?f1 * (\l\[3..l\[3.. i) = even ((\l\[3.._def using i by simp also have "\ = (even (\l\[3..l\[3.. 2" "l \ i" and l1: "l - 1 \ 2" "l - 1 \ i" by auto have l2: "l - 2 = l - 1 - 1" by simp show ?case using diff(3) [OF l] diff(3) [OF l1] l2 by auto qed also have "even (?m' i) = even ?m1" proof - from i have id: "Suc (i - 1 - 1) = i - 1" "i - 2 = i - 1 - 1" by auto have "even ?m1 = even (n (i - 2) + n (i - 1) + 1)" unfolding \ id using diff[of "i - 1"] i by auto also have "\ = even (?m' i)" by auto finally show ?thesis by simp qed also have "(even ?m2 = even ?m1) = even (?m2 + ?m1)" unfolding even_add by simp also have "?m2 + ?m1 = ?m1 + ?m2" by simp finally show "even (\ i) = even (?m1 + ?m2)" . qed qed show ?thesis unfolding id1 id3 id2 smult_smult id4 by (simp add: ac_simps power_add) qed (* equation 28 in BT *) lemma fundamental_theorem_eq_5: assumes i: "3 \ i" "i \ k" "n i < j" "j < n (i - 1) - 1" shows "R j = 0" proof - from BT_lemma_2_23[OF i] have id1: "subresultant j (F (i - 2)) (F (i - 1)) = 0" . have "n (i - 1) \ n 2" by (rule n_ge_trans, insert i, auto) with n_gt[of "i - 1"] i have "n (i - 1) - 1 < n 2" and lt: "j < n (i - 1)" by linarith+ with i have "R j = subresultant j G1 G2" unfolding R_def by auto from arg_cong[OF this, of ffp, unfolded to_fract_hom.subresultant_hom, folded F1 F2] have id2: "ffp (R j) = subresultant j (F 1) (F 2)" . from i have "3 \ i" "i \ k + 1" by auto note eq_30 = BT_eq_30[OF this lt] let ?c3 = "\l\[3.. l ^ (n (l - 1) - j)" let ?c2 = "\l\[3.. l ^ (n (l - 1) - j) * f (l - 1) ^ (\ (l - 2) + \ (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))" have "?c3 \ 0" by (rule nonzero_alphaprod, insert i, auto) with arg_cong[OF eq_30, of "smult (inverse ?c3)"] have id3: "subresultant j (F 1) (F 2) = smult (inverse ?c3 * ?c2) (subresultant j (F (i - 2)) (F (i - 1)))" by (auto intro: poly_eqI) have "ffp (R j) = 0" unfolding id1 id2 id3 by simp thus ?thesis by simp qed (* equation 27 in BT *) lemma fundamental_theorem_eq_6: assumes "3 \ i" "i \ k" shows "ffp (R (n i)) = smult (\ i) (F i)" (is "?lhs=?rhs") proof - from assms have i1:"1 \ i" by auto from assms have nlt:"i \ k + 1" "n i < n (i - 1)" using n_gt[of "i - 1"] by auto from assms have \nz:"\ i ^ \ (i - 1) \ 0" using \0 by auto have *:"\ a f b. a \ 0 \ smult a f = b \ f = smult (inverse (a::'a fract)) b" by auto have **:"\ f g xs c. c * prod_list (map f xs) * prod_list (map g xs) = c * (\x\xs. f x * (g:: _ \ (_ :: comm_monoid_mult)) x)" by (auto simp:ac_simps prod_list_multf) have ***:"\ c. \ i ^ \ (i - Suc 0) * (inverse (\ i ^ \ (i - Suc 0)) * c) = (\ i / \ i) ^ \ (i - 1) * c" by (auto simp:inverse_eq_divide power_divide) have ****:"int (n (i - Suc 0) - n i) - 1 = int (n (i - 1) - Suc (n i))" using assms nlt by auto from assms n_ge[of "i-2"] nlt n_ge[of i] have nge:"n (i - Suc 0) \ n (i - 2)" "n i < n (i - Suc 0)" "n i < n (i - 1)" "Suc (i - 2) = i - 1" by (cases i,auto simp:numeral_2_eq_2 numeral_3_eq_3) have *****:"(- 1 :: 'a fract) ^ ((n (i - Suc 0) - n i) * (n (i - Suc 0) - n i + (n (i - 2) - n (Suc (i - 2))))) = (- 1) ^ ((n i + n (i - Suc 0)) * (n i + n (i - 2)))" "(- 1 :: 'a fract) ^ (\l\[3..l\[3.. n (x - Suc 0)" "n (x - 2) \ n i" by auto with 1 show ?case by auto qed have "ffp (R (n i)) = subresultant (n i) (F 1) (F 2)" unfolding R_def F1 F2 by (auto simp: to_fract_hom.subresultant_hom ni2[OF assms]) also have "\ = smult ((- 1) ^ (\l\[3..x\[3.. x / \ x) ^ (n (x - 1) - n i) * f (x - 1) ^ (\ (x - 1) + \ (x - 2))) * (((\ i / \ i) ^ \ (i - 1)) * f (i - 1) ^ (\ (i - 1) + \ (i - 2))) * ((- 1) ^ ((\ (i - 2) + \ (i - 1)) * \ (i - 1)) * f i ^ (\ (i - 1) - 1) )) (F i)" unfolding BT_eq_30'[OF assms(1) nlt] ** *[OF \nz BT_lemma_2_22[OF assms]] smult_smult by (auto simp:ac_simps *** ) also have "\ = ?rhs" unfolding \_def \_def using prod_combine[OF assms(1)] \ assms by (auto simp:ac_simps exp_pow_int[symmetric] power_add ***** ****) finally show ?thesis. qed (* equation 26 in BT *) lemma fundamental_theorem_eq_7: assumes j: "j < n k" shows "R j = 0" proof - let ?P = "pseudo_divmod (F (k - 1)) (F k)" from F0[of k] k2 have Fk: "F k \ 0" by auto from pmod[of "Suc k"] k2 F0[of "Suc k"] have "pseudo_mod (F (k - 1)) (F k) = 0" by auto then obtain Q where "?P = (Q,0)" unfolding pseudo_mod_def by (cases ?P, auto) from pseudo_divmod(1)[OF Fk this] Fk obtain c where id: "smult c (F (k - 1)) = F k * Q" and c: "c \ 0" by auto from id have id: "smult c (F (k - 1)) = Q * F k" by auto from n_ge[unfolded n, of "k - 1"] k2 c have "degree (F k) \ degree (smult c (F (k - 1)))" by auto from subresultant_product[OF id this, unfolded subresultant_smult_left[OF c], of j] j have *:"subresultant j (F (k + 1 - 2)) (F (k + 1 - 1)) = 0" using c unfolding n by simp from assms have **:"j \ n 2" by (meson k2 n_ge_trans not_le one_le_numeral order_refl) from k2 assms have "3 \ k + 1" "k + 1 \ k + 1" "j < n (k + 1 - 1)" by auto from BT_eq_30[OF this,unfolded *] nonzero_alphaprod[OF le_refl] ** F1 F2 show ?thesis by (auto simp:R_def F0 to_fract_hom.subresultant_hom[symmetric]) qed definition "G i = R (n (i - 1) - 1)" definition "H i = R (n i)" lemma gamma_delta_beta_3: "\ 3 = (- 1) ^ (\ 1 + 1) * \ 3" proof - have "\ 3 = (- 1) ^ \ 3 * pow_int (f 2) (1 - int (\ 2)) * (\ 3 / (f 2 ^ Suc (\ 1)) * f 2 ^ (\ 1 + \ 2))" unfolding \_def \ \_def by (simp add: \) also have "f 2 ^ (\ 1 + \ 2) = pow_int (f 2) (int (\ 1 + \ 2))" unfolding pow_int_def nat_int by auto also have "int (\ 1 + \ 2) = int (Suc (\ 1)) + (int (\ 2) - 1)" by simp also have "pow_int (f 2) \ = pow_int (f 2) (Suc (\ 1)) * pow_int (f 2) (int (\ 2) - 1)" by (rule pow_int_add, insert f20, auto) also have "pow_int (f 2) (Suc (\ 1)) = f 2 ^ (Suc (\ 1))" unfolding pow_int_def nat_int by simp also have "\ 3 / (f 2 ^ Suc (\ 1)) * (f 2 ^ Suc (\ 1) * pow_int (f 2) (int (\ 2) - 1)) = (\ 3 / (f 2 ^ Suc (\ 1)) * f 2 ^ Suc (\ 1) * pow_int (f 2) (int (\ 2) - 1))" by simp also have "\ 3 / (f 2 ^ Suc (\ 1)) * f 2 ^ Suc (\ 1) = \ 3" using f20 by auto finally have "\ 3 = ((- 1) ^ \ 3 * \ 3) * (pow_int (f 2) (1 - int (\ 2)) * pow_int (f 2) (int (\ 2) - 1))" by simp also have "pow_int (f 2) (1 - int (\ 2)) * pow_int (f 2) (int (\ 2) - 1) = 1" by (subst pow_int_add[symmetric], insert f20, auto) finally have "\ 3 = (- 1) ^ \ 3 * \ 3" by simp also have "\ 3 = (n 1 + n 2 + 1) * (n 2 + n 2 + 1)" unfolding \_def by simp also have "(- (1 :: 'a fract)) ^ \ = (- 1) ^ (n 1 - n 2 + 1)" by (rule minus_1_even_eqI, insert n12, auto) also have "\ = (- 1)^(\ 1 + 1)" unfolding \ by (simp add: numeral_2_eq_2) finally show "\ 3 = (- 1) ^ (\ 1 + 1) * \ 3" . qed fun h :: "nat \ 'a fract" where "h i = (if (i \ 1) then 1 else if i = 2 then (f 2 ^ \ 1) else (f i ^ \ (i - 1) / (h (i - 1) ^ (\ (i - 1) - 1))))" lemma smult_inverse_sdiv_poly: assumes ffp: "p \ range ffp" and p: "p = smult (inverse x) q" and p': "p' = sdiv_poly q' x'" and xx: "x = ff x'" and qq: "q = ffp q'" shows "p = ffp p'" proof (rule poly_eqI) fix i have "coeff p i = coeff q i / x" unfolding p by (simp add: field_simps) also have "\ = ff (coeff q' i) / ff x'" unfolding qq xx by simp finally have cpi: "coeff p i = ff (coeff q' i) / ff x'" . from ffp obtain r where pr: "p = ffp r" by auto from arg_cong[OF this, of "\ p. coeff p i", unfolded cpi] have "ff (coeff q' i) / ff x' \ range ff" by auto hence id: "ff (coeff q' i) / ff x' = ff (coeff q' i div x')" by (rule div_divide_to_fract, auto) show "coeff p i = coeff (ffp p') i" unfolding cpi id p' by (simp add: sdiv_poly_def coeff_map_poly) qed end locale subresultant_prs_locale2 = subresultant_prs_locale F n \ f k \ G1 G2 for F :: "nat \ 'a :: idom_divide fract poly" and n :: "nat \ nat" and \ :: "nat \ nat" and f :: "nat \ 'a fract" and k :: nat and \ :: "nat \ 'a fract" and G1 G2 :: "'a poly" + assumes \3: "\ 3 = (-1)^(\ 1 + 1)" and \i: "\ i. 4 \ i \ i \ Suc k \ \ i = (-1)^(\ (i - 2) + 1) * f (i - 2) * h (i - 2) ^ (\ (i - 2))" begin lemma B_eq_17_main: "2 \ i \ i \ k \ h i = (-1) ^ (n 1 + n i + i + 1) / f i * (\l\[3..< Suc (Suc i)]. (\ l / \ l)) \ h i \ 0" proof (induct i rule: less_induct) case (less i) from less(2-) have fi0: "f i \ 0" using f0[of i] by simp have 1: "(- 1) \ (0 :: 'a fract)" by simp show ?case (is "h i = ?r i \ _") proof (cases "i = 2") case True have f20: "f 2 \ 0" using f20 by auto have hi: "h i = f 2 ^ \ 1" unfolding True h.simps[of 2] by simp have id: "int (\ 1) = int (n 1) - int (n 2)" using n12 unfolding \ numeral_2_eq_2 by simp have "?r i = (- 1) ^ (1 + n 1 + n 2) * ((f 2 ^ Suc (\ 1)) / (\ 3)) / pow_int (f 2) 1" unfolding True \_def by simp also have "\ 3 = (- 1) ^ (\ 1 + 1)" by (rule \3) also have "f 2 ^ Suc (\ 1) / \ = \ * f 2 ^ Suc (\ 1)" by simp finally have "?r i = ((- 1) ^ (1 + n 1 + n 2) * ((- 1) ^ (\ 1 + 1))) * pow_int (f 2) (int (Suc (\ 1)) + (-1))" (is "_ = ?a * _") unfolding pow_int_divide exp_pow_int power_add pow_int_add[OF f20] by (simp add: ac_simps pow_int_add) also have "?a = (-1)^(1 + n 1 + n 2 + \ 1 + 1)" unfolding power_add by simp also have "\ = (-1)^0" by (rule minus_1_even_eqI, insert n12, auto simp: \ numeral_2_eq_2, presburger) finally have ri: "?r i = pow_int (f 2) (int (\ 1))" by simp show ?thesis unfolding ri hi exp_pow_int[symmetric] using f20 by simp next case False hence i: "i \ 3" and ii: "i - 1 < i" "2 \ i - 1" "i - 1 \ k" using less(2-) by auto from i less(2-) have cc: "4 \ Suc i" "Suc i \ Suc k" by auto define P where "P = (\l\[3..< Suc i]. \ l / \ l)" define Q where "Q = P * pow_int (h (i - 1)) (- int (\ (i - 1)))" define R where "R = f i ^ \ (i - 1)" define S where "S = pow_int (f (i - 1)) (- 1)" note IH = less(1)[OF ii] hence hi0: "h (i - 1) \ 0" by auto have hii: "h i = f i ^ \ (i - 1) / h (i - 1) ^ (\ (i - 1) - 1)" unfolding h.simps[of i] using i by simp also have "\ = f i ^ \ (i - 1) * pow_int (h (i - 1)) (- int (\ (i - 1) - 1))" unfolding exp_pow_int pow_int_divide by simp also have "int (\ (i - 1) - 1) = int (\ (i - 1)) - 1" proof - have "\ (i - 1) > 0" unfolding \[of "i - 1"] using n_gt[OF ii(2)] less(2-) by auto thus ?thesis by simp qed also have "- (int (\ (i - 1)) - 1) = 1 + (- int (\ (i - 1)))" by simp finally have hi: "h i = (- 1) ^ (n 1 + n (i - 1) + i) * (R * Q * S)" unfolding pow_int_add[OF hi0] P_def Q_def pow_int_divide[symmetric] R_def S_def using IH i by (simp add: ac_simps) from i have id: "[3.. (Suc i) / \ (Suc i)" unfolding pow_int_divide[symmetric] P_def id Fract_conv_to_fract by simp also have "\ (Suc i) = (- 1) ^ (\ (i - 1) + 1) * f (i - 1) * h (i - 1) ^ \ (i - 1)" using \i[OF cc] by simp also have "\ (Suc i) = f i ^ Suc (\ (i - 1))" unfolding \_def by simp finally have "?r i = (- 1) ^ (n 1 + n i + i + 1) * pow_int (f i) (- 1) * P * (f i ^ Suc (\ (i - 1))) / (- 1) ^ (\ (i - 1) + 1) * pow_int (f (i - 1)) (- 1) / h (i - 1) ^ \ (i - 1)" (is "_ = ?a1 * ?fi1 * P * ?fi2 / ?a2 * ?b / ?c") unfolding exp_pow_int pow_int_divide[symmetric] by simp also have "\ = (?a1 / ?a2) * (?fi1 * ?fi2) * (P / ?c) * ?b" by (simp add: ac_simps) also have "?a1 / ?a2 = (- 1) ^ (n 1 + n i + i + 1 + \ (i - 1) + 1)" by (simp add: power_add) also have "\ = (-1) ^ (n 1 + n i + i + \ (i - 1))" by (rule minus_1_even_eqI, auto) also have "n 1 + n i + i + \ (i - 1) = n 1 + n (i - 1) + i" unfolding \ using i less(2-) n_ge[of "i - 1"] by simp also have "?fi1 * ?fi2 = pow_int (f i) (-1 + int (Suc (\ (i - 1))))" unfolding exp_pow_int pow_int_add[OF fi0] by simp also have "\ = pow_int (f i) (int (\ (i - 1)))" by simp also have "P / ?c = Q" unfolding Q_def exp_pow_int pow_int_divide by simp also have "?b = S" unfolding S_def by simp finally have ri: "?r i = (-1)^(n 1 + n (i - 1) + i) * (R * Q * S)" by (simp add: exp_pow_int R_def) have id: "h i = ?r i" unfolding hi ri .. show ?thesis by (rule conjI[OF id], unfold hii, insert IH fi0, auto) qed qed lemma B_eq_17: "2 \ i \ i \ k \ h i = (-1) ^ (n 1 + n i + i + 1) / f i * (\l\[3..< Suc (Suc i)]. (\ l / \ l))" using B_eq_17_main by blast lemma B_theorem_2: "3 \ i \ i \ Suc k \ \ i = 1" proof (induct i rule: less_induct) case (less i) show ?case proof (cases "i = 3") case True show ?thesis unfolding True unfolding gamma_delta_beta_3 \3 by simp next case False with less(2-) have i: "i \ 4" and ii: "i - 1 < i" "3 \ i - 1" "i - 1 \ Suc k" and iii: "4 \ i" "i \ Suc k" and iv: "2 \ i - 2" "i - 2 \ k" by auto from less(1)[OF ii] have IH: "\ (i - 1) = 1" . define L where "L = [3..< i]" have id: "[3.. l. \ l / \ l)" define A where "A = (\ l. \ l / \ l)" define Q where "Q = (\ l. f (l - 1) ^ (\ (l - 2) + \ (l - 1)))" define R where "R = (\ i l. B l ^ (n (l - 1) - n (i - 1) + 1))" define P where "P = (\ i l. R i l * Q l)" have fi0: "f (i - 1) \ 0" using f0[of "i - 1"] less(2-) by auto have fi0': "f (i - 2) \ 0" using f0[of "i - 2"] less(2-) by auto { fix j assume "j \ set L" hence "j \ 3" "j < i" unfolding L_def by auto with less(3) have j: "j - 1 \ 0" "j - 1 < k" by auto hence Q: "Q j \ 0" unfolding Q_def using f0[of "j - 1"] by auto from j \0 \0[of j] have 0: "\ j \ 0" "\ j \ 0" by auto hence "B j \ 0" "A j \ 0" unfolding B_def A_def by auto note Q this } note L0 = this let ?exp = "\ (i - 2)" have "\ i = \ i / \ (i - 1)" unfolding IH by simp also have "\ = (- 1) ^ \ i * pow_int (f (i - 1)) (1 - int (\ (i - 1))) * (\l\L. P i l) * P i i / ((- 1) ^ \ (i - 1) * pow_int (f (i - 2)) (1 - int (\ (i - 2))) * (\l\L. P (i - 1) l))" (is "_ = ?a1 * ?f1 * ?L1 * P i i / (?a2 * ?f2 * ?L2)") unfolding \_def id P_def Q_def R_def B_def by (simp add: numeral_2_eq_2) also have "\ = (?a1 * ?a2) * (?f1 * P i i) / ?f2 * (?L1 / ?L2)" unfolding divide_prod_assoc by simp also have "?a1 * ?a2 = (-1)^(\ i + \ (i - 1))" (is "_ = ?a") unfolding power_add by simp also have "?L1 / ?L2 = (\l\L. R i l) / (\l\L. R (i - 1) l) * ((\l\L. Q l) / (\l\L. Q l))" unfolding P_def prod_list_multf divide_prod_assoc by simp also have "\ = (\l\L. R i l) / (\l\L. R (i - 1) l)" (is "_ = ?L1 / ?L2") proof - have "(\l\L. Q l) \ 0" unfolding prod_list_zero_iff using L0 by auto thus ?thesis by simp qed also have "?f1 * P i i = (?f1 * pow_int (f (i - 1)) (int ?exp + int (\ (i - 1)))) * R i i" unfolding P_def Q_def exp_pow_int by simp also have "?f1 * pow_int (f (i - 1)) (int ?exp + \ (i - 1)) = pow_int (f (i - 1)) (1 + int ?exp)" (is "_ = ?f1") unfolding pow_int_add[OF fi0, symmetric] by simp also have "R i i = \ i / \ i" unfolding B_def R_def Fract_conv_to_fract by simp also have "\ i = f (i - 1) ^ Suc ?exp" unfolding \_def by simp also have "\ i / \ = \ i * pow_int (f (i - 1)) (- 1 - ?exp)" (is "_ = ?\ * ?f12") unfolding exp_pow_int pow_int_divide by simp finally have "\ i = (?a * (?f1 * ?f12)) * ?\ / ?f2 * (?L1 / ?L2)" by simp also have "?a * (?f1 * ?f12) = ?a" unfolding pow_int_add[OF fi0, symmetric] by simp also have "?L1 / ?L2 = pow_int (\l\L. A l) (- ?exp)" proof - have id: "i - 1 - 1 = i - 2" by simp have "set L \ {l. 3 \ l \ l \ k \ l < i}" unfolding L_def using less(3) by auto thus ?thesis unfolding R_def id proof (induct L) case (Cons l L) from Cons(2) have l: "3 \ l" "l \ k" "l < i" and L: "set L \ {l. 3 \ l \ l \ k \ l < i}" by auto note IH = Cons(1)[OF L] from l \0 \0[of l] have 0: "\ l \ 0" "\ l \ 0" by auto hence B0: "B l \ 0" unfolding B_def by auto have "(\l\l # L. B l ^ (n (l - 1) - n (i - 1) + 1)) / (\l\l # L. B l ^ (n (l - 1) - n (i - 2) + 1)) = (B l ^ (n (l - 1) - n (i - 1) + 1) * (\l\L. B l ^ (n (l - 1) - n (i - 1) + 1))) / (B l ^ (n (l - 1) - n (i - 2) + 1) * (\l\L. B l ^ (n (l - 1) - n (i - 2) + 1)))" (is "_ = (?l1 * ?L1) / (?l2 * ?L2)") by simp also have "\ = (?l1 / ?l2) * (?L1 / ?L2)" by simp also have "?L1 / ?L2 = pow_int (prod_list (map A L)) (- int (\ (i - 2)))" by (rule IH) also have "?l1 / ?l2 = pow_int (B l) (int (n (l - 1) - n (i - 1)) - int (n (l - 1) - n (i - 2)))" unfolding exp_pow_int pow_int_divide pow_int_add[OF B0, symmetric] by simp also have "int (n (l - 1) - n (i - 1)) - int (n (l - 1) - n (i - 2)) = int ?exp" proof - have "n (l - 1) \ n (i - 2)" "n (l - 1) \ n (i - 1)" "n (i - 2) \ n (i - 1)" using i l less(3) by (intro n_ge_trans, auto)+ hence id: "int (n (l - 1) - n (i - 1)) = int (n (l - 1)) - int (n (i - 1))" "int (n (l - 1) - n (i - 2)) = int (n (l - 1)) - int (n (i - 2))" "int (n (i - 2) - n (i - 1)) = int (n (i - 2)) - int (n (i - 1))" by simp_all have id2: "int ?exp = int (n (i - 2) - n (i - 1))" unfolding \ using i by (cases i; cases "i - 1", auto) show ?thesis unfolding id2 unfolding id by simp qed also have "pow_int (B l) \ = pow_int (inverse (B l)) (- \)" unfolding pow_int_def by (cases "int (\ (i - 2))" rule: linorder_cases, auto simp: field_simps) also have "inverse (B l) = A l" unfolding B_def A_def by simp also have "pow_int (A l) (- int ?exp) * pow_int (prod_list (map A L)) (- int ?exp) = pow_int (prod_list (map A (l # L))) (- int ?exp)" by (simp add: pow_int_mult) finally show ?case . qed simp qed also have "\ i = (- 1) ^ (?exp + 1) * f (i - 2) * h (i - 2) ^ ?exp" unfolding \i[OF iii] .. finally have "\ i = (((- 1) ^ (\ i + \ (i - 1)) * (- 1) ^ (?exp + 1))) * (pow_int (f (i - 2)) 1 * pow_int (f (i - 2)) (int ?exp - 1)) * h (i - 2) ^ ?exp / (\l\L. A l) ^ ?exp" (is "_ = ?a * ?f1 * ?H / ?L") unfolding pow_int_divide exp_pow_int by simp also have "?f1 = pow_int (f (i - 2)) (int ?exp)" (is "_ = ?f1") unfolding pow_int_add[OF fi0', symmetric] by simp also have "h (i - 2) = (- 1) ^ (n 1 + n (i - 2) + (i - 2) + 1) / f (i - 2) * (\l\L. A l)" (is "_ = ?a2 / ?f2 * ?L") unfolding B_eq_17[OF iv] A_def id L_def by simp also have "((- (1 :: 'a fract)) ^ (\ i + \ (i - 1)) * (- 1) ^ (?exp + 1)) = ((- 1) ^ (\ i + \ (i - 1) + ?exp + 1))" (is "_ = ?a1") by (simp add: power_add) finally have "\ i = ?a1 * ?f1 * (?a2 / ?f2 * ?L) ^ ?exp / ?L ^ ?exp" by simp also have "\ = (?a1 * ?a2^?exp) * (?f1 / ?f2 ^ ?exp) * (?L^?exp / ?L ^ ?exp)" unfolding power_mult_distrib power_divide by auto also have " ?L ^ ?exp / ?L ^ ?exp = 1" proof - have "?L \ 0" unfolding prod_list_zero_iff using L0 by auto thus ?thesis by simp qed also have "?f1 / ?f2 ^ ?exp = 1" unfolding exp_pow_int pow_int_divide pow_int_add[OF fi0', symmetric] by simp also have "?a2^?exp = (- 1) ^ ((n 1 + n (i - 2) + (i - 2) + 1) * ?exp)" by (rule semiring_normalization_rules) also have "?a1 * \ = (- 1) ^ (\ i + \ (i - 1) + ?exp + 1 + (n 1 + n (i - 2) + (i - 2) + 1) * ?exp)" (is "_ = _ ^ ?e") by (simp add: power_add) also have "\ = (-1)^0" proof - define e where "e = ?e" have *: "?e = (2 * ?exp + \ i + \ (i - 1) + 1 + (n 1 + n (i - 2) + (i - 2)) * ?exp)" by simp define A where "A = (\ i l. (n (l - 2) + n (i - 1) + 1) * (n (l - 1) + n (i - 1) + 1))" define B where "B = (\ i. (n (i - 1) + 1) * (n (i - 1) + 1))" define C where "C = (\ l. (n (l - 1) + n (l - 2) + n (l - 1) * n (l - 2)))" define D where "D = (\ l. n (l - 1) + n (l - 2))" define m2 where "m2 = n (i - 2)" define m1 where "m1 = n (i - 1)" define m0 where "m0 = n 1" define i3 where "i3 = i - 3" have m12: "m2 \ m1" unfolding m2_def m1_def using n_ge[of "i - 2"] i less(3) by (cases i, auto) have idd: "Suc (i - 2) = i - 1" "i - 1 - 1 = i - 2" using i by auto have id4: "i - 2 = Suc i3" unfolding i3_def using i by auto from i have "3 < i" by auto hence "\ k. sum_list (map D L) = n 1 + n (i - 2) + 2 * k" unfolding L_def proof (induct i rule: less_induct) case (less i) show ?case proof (cases "i = 4") case True thus ?thesis by (simp add: D_def) next case False obtain ii where i: "i = Suc ii" and ii: "ii < i" "3 < ii" using False less(2) by (cases i, auto) from less(1)[OF ii] obtain k where IH: "sum_list (map D [3 ..< ii]) = n 1 + n (ii - 2) + 2 * k" by auto have "map D [3 ..< i] = map D [3 ..< ii] @ [D ii]" unfolding i using ii by auto hence "sum_list (map D [3.. = n 1 + n (ii - 1) + 2 * (n (ii - 2) + k)" unfolding D_def by simp also have "n (ii - 1) = n (i - 2)" unfolding i by simp finally show ?thesis by blast qed qed then obtain kk where DL: "sum_list (map D L) = n 1 + n (i - 2) + 2 * kk" .. let ?l = "i - 3" have len: "length L = i - 3" unfolding L_def using i by auto have A: "A i l = B i + D l * n (i - 1) + C l" for i l unfolding A_def B_def C_def D_def ring_distribs by simp have id2: "[3.. = even ((1 + (n 1 + n (i - 2) + (i - 2)) * ?exp) + (\ i + \ (i - 1)))" (is "_ = even (?g + ?j)") unfolding * by (simp add: ac_simps) also have "?j = (\l\L @ [i]. A i l) + (\l\L. A (i - 1) l)" unfolding \_def id A_def by simp also have "\ = 2 * (\l\L. C l) + (Suc ?l) * B i + (\l\L @ [i]. D l * n (i - 1)) + C i + ?l * B (i - 1) + (\l\L. D l * n (i - 1 - 1))" unfolding A sum_list_addf by (simp add: sum_list_triv len) also have "\ = ((Suc ?l * B i + C i + ?l * B (i - 1) + D i * n (i - 1)) + ((\l\L. D l) * (n (i - 1) + n (i - 2)) + 2 * (\l\L. C l)))" (is "_ = ?i + ?j") unfolding sum_list_mult_const by (simp add: ring_distribs numeral_2_eq_2) also have "?j = (n 1 + n (i - 2)) * (n (i - 1) + n (i - 2)) + 2 * (kk * (n (i - 1) + n (i - 2)) + (\l\L. C l))" (is "_ = ?h + 2 * ?f") unfolding DL by (simp add: ring_distribs) finally have "even e = even (?g + ?i + ?h + 2 * ?f)" by presburger also have "\ = even (?g + ?i + ?h)" by presburger also have "?g + ?i + ?h = i3 * (m2 - m1 + m1 * m1 + m2 * m2) + (m2 - m1 + m1 + m2) * (m0 + m2) + (m1 + m2 + (m2 - m1)) + 2 * (m1 * m2 + m1 * m1 + 1 + i3 + m1 * Suc i3 + m2 * i3)" unfolding idd B_def D_def C_def \ m1_def[symmetric] m2_def[symmetric] m0_def[symmetric] unfolding i3_def[symmetric] id4 by (simp add: ring_distribs) also have "(m1 + m2 + (m2 - m1)) = 2 * m2" using m12 by simp also have "(m2 - m1 + m1 + m2) * (m0 + m2) = 2 * (m2 * (m0 + m2))" using m12 by simp finally obtain l1 l2 l3 where "even e = even (i3 * (m2 - m1 + m1 * m1 + m2 * m2) + 2 * l1 + 2 * l2 + 2 * l3)" by blast also have "\ = even (i3 * (m2 - m1 + m1 * m1 + m2 * m2))" by simp also have "\ = even (i3 * (2 * m1 + (m2 - m1 + m1 * m1 + m2 * m2)))" by simp also have "2 * m1 + (m2 - m1 + m1 * m1 + m2 * m2) = m1 + m2 + m1 * m1 + m2 * m2" using m12 by simp also have "even (i3 * \)" by auto finally have "even e" . thus ?thesis unfolding e_def by (intro minus_1_even_eqI, auto) qed finally show "\ i = 1" by simp qed qed context fixes i :: nat assumes i: "3 \ i" "i \ k" begin lemma B_theorem_3_b: "\ i * f i = ff (lead_coeff (H i))" using arg_cong[OF fundamental_theorem_eq_6[folded H_def, OF i], of lead_coeff] unfolding f[of i] lead_coeff_smult by simp lemma B_theorem_3_main: "\ i * f i / \ (i + 1) = (-1)^(n 1 + n i + i + 1) / f i * (\l\[3..< Suc (Suc i)]. (\ l / \ l))" proof (cases "f i = 0") case True thus ?thesis by simp next case False note ff0 = this from i(1) have "Suc (Suc i) > 3" by auto hence id: "[3 ..< Suc (i + 1)] = [3 ..< Suc i] @ [Suc i]" "[3 ..< Suc (Suc i)] = [3 ..< Suc i] @ [Suc i]" by auto have cong: "\ a b c d. a = c \ b = d \ a * b = c * (d :: 'a fract)" by auto define AB where "AB = (\ l. \ l / \ l)" define ABP where "ABP = (\ l. AB l ^ (n (l - 1) - n i) * f (l - 1) ^ (\ (l - 2) + \ (l - 1)))" define PR where "PR = (\l\[3..l\[3.. i * f i / \ (i + 1) = ( ((- 1) ^ \ i * (- 1) ^ \ (i + 1)) * (pow_int (f i) (int (\ (i - 1)) - 1) * PR * f i / pow_int (f i) (1 - int (\ i)) / ((\l\[3.. (i - 1) + \ i))))" unfolding id prod_list.append map_append \_def \_def divide_prod_assoc by (simp add: field_simps power_add AB_def ABP_def PR_def) also have "(- 1 :: 'a fract) ^ \ i * (- 1) ^ \ (i + 1) = (- 1) ^ (\ i + \ (i + 1))" unfolding power_add by (auto simp: field_simps) also have "\ = (- 1) ^ (n 1 + n i + i + 1)" proof (cases "i = 2") case True show ?thesis unfolding \_def \_def True by (auto, rule minus_1_even_eqI, auto) next case False define a where "a = (\ l. n (l - 2) + n i)" define b where "b = (\ l. n (l - 1) + n i)" define c where "c = (\l\[3..l\[3.. i + \ (i + 1)) = ((\l\[3.._def \_def id a_def b_def sum_list_addf by simp also have "(\l\[3..l\[3.. = (\l\[3.. = 2 * c + (\l\[3..l\[3..l\[3..l\[3..l\[3..l\3 # [4.. = n 1 + (\l\[(Suc 3)..l\[(Suc 3)..l\[3..l\[3..l\[3.. i + \ (i + 1) = 2 * d + n (i - 1) + n 1 + length [3.. i + \ (i + 1) = 2 * (d + n (i - 1) + e) + n 1 + (i - 2) + n i + 1" by simp show ?thesis by (rule minus_1_even_eqI, unfold id, insert i, auto) qed also have "(\l\[3.. (i - 1)) - 1) * PR * f i / pow_int (f i) (1 - int (\ i)) / (PR * PR2 * AB (Suc i) * f i ^ (\ (i - 1) + \ i))) = ((pow_int (f i) (int (\ (i - 1)) - 1) * pow_int (f i) 1 * pow_int (f i) (int (\ i) - 1) / pow_int (f i) (int (\ (i - 1) + \ i)))) * (PR / PR / (PR2 * AB (Suc i)))" (is "\ = ?x * ?y") unfolding exp_pow_int[symmetric] by (simp add: pow_int_divide ac_simps) also have "?x = pow_int (f i) (-1)" unfolding pow_int_divide pow_int_add[OF ff0, symmetric] by simp also have "\ = 1 / (f i)" unfolding pow_int_def by simp also have "PR / PR = 1" proof - have "PR \ 0" unfolding PR_def prod_list_zero_iff set_map proof assume "0 \ ABP ` set [3 ..< Suc i]" then obtain j where j: "3 \ j" "j < Suc i" and 0: "ABP j = 0" by auto with i have jk: "j \ k" and j1: "j - 1 \ 0" "j - 1 < k" by auto hence 1: "\ j \ 0" "f (j - 1) \ 0" using \0 f0 by auto with 0 have "AB j = 0" unfolding ABP_def by simp from this[unfolded AB_def] 1(1) \0[of j] show False by auto qed thus ?thesis by simp qed also have "PR2 * AB (Suc i) = (\l\[3.. = inverse \" by (simp add: inverse_eq_divide) also have "\ = (\l\[3.. l / \ l)" unfolding AB_def inverse_prod_list map_map o_def by (auto cong: map_cong) finally show ?thesis by simp qed lemma B_theorem_3: "h i = \ i * f i" "h i = ff (lead_coeff (H i))" proof - have "\ i * f i = \ i * f i / \ (i + 1)" using B_theorem_2[of "i + 1"] i by auto also have "\ = (- 1) ^ (n 1 + n i + i + 1) / f i * (\l\[3.. l / \ l)" by (rule B_theorem_3_main) also have "\ = h i" using B_eq_17[of i] i by simp finally show "h i = \ i * f i" .. thus "h i = ff (lead_coeff (H i))" using B_theorem_3_b by auto qed end lemma h0: "i \ k \ h i \ 0" proof (induct i) case (Suc i) thus ?case unfolding h.simps[of "Suc i"] using f0 by (auto simp del: h.simps) qed auto lemma deg_G12: "degree G1 \ degree G2" using n12 unfolding n F1 F2 by auto lemma R0: shows "R 0 = [: resultant G1 G2 :]" proof(cases "n 2 = 0") case True hence d:"degree G2 = 0" unfolding n F2 by auto from degree0_coeffs[OF d] F2 F12 obtain a where G2: "G2 = [:a:]" and a: "a \ 0" by auto have "sdiv_poly [:a * a ^ degree G1:] a = [:a ^ degree G1:]" using a unfolding sdiv_poly_def by auto note dp = this show ?thesis using G2 F12 unfolding R_def \ n F1 F2 Suc_1 by (auto split:if_splits simp:mult.commute dp) next case False from False n12 have d:"degree G2 \ 0" "degree G2 \ degree G1" unfolding n F2 F1 by auto from False have "R 0 = subresultant 0 G1 G2" unfolding R_def by simp also have "\ = [: resultant G1 G2 :]" unfolding subresultant_resultant by simp finally show ?thesis . qed context fixes div_exp :: "'a \ 'a \ nat \ 'a" assumes div_exp_sound: "div_exp_sound div_exp" begin interpretation div_exp_sound div_exp by (rule div_exp_sound) lemma subresultant_prs_main: assumes "subresultant_prs_main Gi_1 Gi hi_1 = (Gk, hk)" and "F i = ffp Gi" and "F (i - 1) = ffp Gi_1" and "h (i - 1) = ff hi_1" and "i \ 3" "i \ k" shows "F k = ffp Gk \ h k = ff hk \ (\ j. i \ j \ j \ k \ F j \ range ffp \ \ (Suc j) \ range ff)" proof - obtain m where m: "m = k - i" by auto show ?thesis using m assms proof (induct m arbitrary: Gi_1 Gi hi_1 i rule: less_induct) case (less m Gi_1 Gi hi_1 i) note IH = less(1) note m = less(2) note res = less(3) note id = less(4-6) note i = less(7-8) let ?pmod = "pseudo_mod Gi_1 Gi" let ?ni = "degree Gi" let ?ni_1 = "degree Gi_1" let ?gi = "lead_coeff Gi" let ?gi_1 = "lead_coeff Gi_1" let ?d1 = "?ni_1 - ?ni" obtain hi where hi: "hi = div_exp ?gi hi_1 ?d1" by auto obtain divisor where div: "divisor = (-1) ^ (?d1 + 1) * ?gi_1 * (hi_1 ^ ?d1)" by auto obtain G1_p1 where G1_p1: "G1_p1 = sdiv_poly ?pmod divisor" by auto note res = res[unfolded subresultant_prs_main.simps[of Gi_1] Let_def, folded hi, folded div, folded G1_p1] have h_i: "h i = f i ^ \ (i - 1) / h (i - 1) ^ (\ (i - 1) - 1)" unfolding h.simps[of i] using i by simp have hi_ff: "h i \ range ff" using B_theorem_3[OF _ i(2)] i by auto have d1: "\ (i - 1) = ?d1" unfolding \ n using id(1,2) using i by simp have fi: "f i = ff ?gi" unfolding f id by simp have fi1: "f (i - 1) = ff ?gi_1" unfolding f id by simp have eq': "h i = ff (lead_coeff Gi) ^ \ (i - 1) / ff hi_1 ^ (\ (i - 1) - 1)" unfolding h_i fi id .. have idh: "h i = ff hi" using hi_ff h_i fi id unfolding hi d1[symmetric] by (subst div_exp[of ?gi "\ (i - 1)" hi_1], unfold eq'[symmetric], insert assms, blast+) have "\ (Suc i) = (- 1) ^ (\ (i - 1) + 1) * f (i - 1) * h (i - 1) ^ \ (i - 1)" using \i[of "Suc i"] i by auto also have "\ = ff ((- 1) ^ (\ (i - 1) + 1) * lead_coeff Gi_1 * hi_1 ^ \ (i - 1))" unfolding id f by (simp add: hom_distribs) also have "\ \ range ff" by blast finally have beta: "\ (Suc i) \ range ff" . have pm: "pseudo_mod (F (i - 1)) (F i) = ffp ?pmod" unfolding to_fract_hom.pseudo_mod_hom[symmetric] id by simp have eq: "(?pmod = 0) = (i = k)" using pm i pmod[of "Suc i"] F0[of "Suc i"] i \0[of "Suc i"] by auto show ?case proof (cases "i = k") case True with res eq have res: "Gk = Gi" "hk = hi" by auto with pmod have "F k = ffp Gk \ h k = ff hk" unfolding res idh[symmetric] id[symmetric] True by auto thus ?thesis using beta unfolding True by auto next case False with res eq have res: "subresultant_prs_main Gi G1_p1 hi = (Gk, hk)" by auto from m False i have m: "m - 1 < m" "m - 1 = k - Suc i" by auto have si: "Suc i - 1 = i" and ii: "3 \ Suc i" "Suc i \ k" and iii: "3 \ Suc i" "Suc i \ Suc k" using False i by auto have *: "(\j\Suc i. j \ k \ F j \ range ffp \ \ (Suc j) \ range ff) = (\j\i. j \ k \ F j \ range ffp \ \ (Suc j) \ range ff)" by (rule for_all_Suc, insert id(1) beta, auto) show ?thesis proof (rule IH[OF m res, unfolded si, OF _ id(1) idh ii, unfolded *]) have F_ffp: "F (Suc i) \ range ffp" using fundamental_theorem_eq_4[OF ii, symmetric] B_theorem_2[OF iii] by auto from pmod[OF iii] have "smult (\ (Suc i)) (F (Suc i)) = pseudo_mod (F (i - 1)) (F i)" by simp from arg_cong[OF this, of "\ x. smult (inverse (\ (Suc i))) x"] have Fsi: "F (Suc i) = smult (inverse (\ (Suc i))) (pseudo_mod (F (i - 1)) (F i))" using \0[of "Suc i"] by auto show "F (Suc i) = ffp G1_p1" proof (rule smult_inverse_sdiv_poly[OF F_ffp Fsi G1_p1 _ pm]) from i ii have iv: "4 \ Suc i" "Suc i \ Suc k" by auto have *: "Suc i - 2 = i - 1" by auto show "\ (Suc i) = ff divisor" unfolding \i[OF iv] div d1 * fi1 using id by (simp add: hom_distribs) qed qed qed qed qed lemma subresultant_prs: assumes res: "subresultant_prs G1 G2 = (Gk, hk)" shows "F k = ffp Gk \ h k = ff hk \ (i \ 0 \ F i \ range ffp) \ (3 \ i \ i \ Suc k \ \ i \ range ff)" proof - let ?pmod = "pseudo_mod G1 G2" have pm: "pseudo_mod (F 1) (F 2) = ffp ?pmod" unfolding to_fract_hom.pseudo_mod_hom[symmetric] F1 F2 by simp let ?g2 = "lead_coeff G2" let ?n2 = "degree G2" obtain d1 where d1: "d1 = degree G1 - ?n2" by auto obtain h2 where h2: "h2 = ?g2 ^ d1" by auto have "(?pmod = 0) = (pseudo_mod (F 1) (F 2) = 0)" using pm by auto also have "\ = (k < 3)" using k2 pmod[of 3] F0[of 3] \0[of 3] by auto finally have eq: "?pmod = 0 \ k = 2" using k2 by linarith note res = res[unfolded subresultant_prs_def Let_def eq, folded d1, folded h2] have idh2: "h 2 = ff h2" unfolding h2 d1 h.simps[of 2] \ n F1 using F2 by (simp add: numeral_2_eq_2 f hom_distribs) have main: "F k = ffp Gk \ h k = ff hk \ (i \ 3 \ i \ k \ F i \ range ffp \ \ (Suc i) \ range ff)" for i proof (cases "k = 2") case True with res have "Gk = G2" "hk = h2" by auto thus ?thesis using True idh2 F2 by auto next case False hence "(k = 2) = False" by simp note res = res[unfolded this if_False] have F_2: "F (3 - 1) = ffp G2" using F2 by simp have h2: "h (3 - 1) = ff h2" using idh2 by simp have n2: "degree G2 = n (3 - 1)" unfolding n using F2 by simp from False k2 have k3: "3 \ k" by auto have "F k = ffp Gk \ h k = ff hk \ (\j\3. j \ k \ F j \ range ffp \ \ (Suc j) \ range ff)" proof (rule subresultant_prs_main[OF res _ F_2 h2 le_refl k3]) let ?pow = "(- 1) ^ (\ 1 + 1) :: 'a fract" from pmod[of 3] k3 have "smult (\ 3) (F 3) = pseudo_mod (F 1) (F 2)" by simp also have "\ = pseudo_mod (ffp G1) (ffp G2)" using F1 F2 by auto also have "\ = ffp (pseudo_mod G1 G2)" unfolding to_fract_hom.pseudo_mod_hom by simp also have "\ 3 = (- 1) ^ (\ 1 + 1)" unfolding \3 by simp finally have "smult ((- 1) ^ (\ 1 + 1)) (F 3) = ffp (pseudo_mod G1 G2)" by simp also have "smult ((- 1) ^ (\ 1 + 1)) (F 3) = [: ?pow :] * F 3" by simp also have "[: ?pow :] = (- 1) ^ (\ 1 + 1)" by (unfold hom_distribs, simp) finally have "(- 1) ^ (\ 1 + 1) * F 3 = ffp (pseudo_mod G1 G2)" by simp from arg_cong[OF this, of "\ i. (- 1) ^ (\ 1 + 1) * i"] have "F 3 = (- 1) ^ (\ 1 + 1) * ffp (pseudo_mod G1 G2)" by simp also have "\ 1 = d1" unfolding \ n d1 using F1 F2 by (simp add: numeral_2_eq_2) finally show F3: "F 3 = ffp ((- 1) ^ (d1 + 1) * pseudo_mod G1 G2)" by (simp add: hom_distribs) qed thus ?thesis by auto qed show ?thesis proof (intro conjI impI) assume "i \ 0" then consider (12) "i = 1 \ i = 2" | (i3) "i \ 3 \ i \ k" | (ik) "i > k" by linarith thus "F i \ range ffp" proof cases case 12 thus ?thesis using F1 F2 by auto next case i3 thus ?thesis using main by auto next case ik hence "F i = 0" using F0 by auto thus ?thesis by simp qed next assume "3 \ i" and "i \ Suc k" then consider (3) "i = 3" | (4) "3 \ i - 1" "i - 1 \ k" by linarith thus "\ i \ range ff" proof (cases) case 3 have "\ i = ff ((- 1) ^ (\ 1 + 1))" unfolding 3 \3 by (auto simp: hom_distribs) thus ?thesis by blast next case 4 with main[of "i - 1"] show ?thesis by auto qed qed (insert main, auto) qed lemma resultant_impl_main: "resultant_impl_main G1 G2 = resultant G1 G2" proof - from F0[of 2] F12(2) have k2: "k \ 2" by auto obtain Gk hk where sub: "subresultant_prs G1 G2 = (Gk, hk)" by force from subresultant_prs[OF this] have *: "F k = ffp Gk" "h k = ff hk" by auto have "resultant_impl_main G1 G2 = (if degree (F k) = 0 then hk else 0)" unfolding resultant_impl_main_def sub split * using F2 F12 by auto also have "\ = resultant G1 G2" proof (cases "n k = 0") case False with fundamental_theorem_eq_7[of 0] show ?thesis unfolding n[of k] * R0 by auto next case True from H_def[of k, unfolded True] have R: "R 0 = H k" by simp show ?thesis proof (cases "k = 2") case False with k2 have k3: "k \ 3" by auto from B_theorem_3[OF k3] R0 R have "h k = ff (resultant G1 G2)" by simp from this[folded *] * have "hk = resultant G1 G2" by simp with True show ?thesis unfolding n by auto next case 2: True have id: "(if degree (F k) = 0 then hk else 0) = hk" using True unfolding n by simp from F0[of 3, unfolded 2] have "F 3 = 0" by simp with pmod[of 3, unfolded 2] \0[of 3] have "pseudo_mod (F 1) (F 2) = 0" by auto hence pm: "pseudo_mod G1 G2 = 0" unfolding F1 F2 to_fract_hom.pseudo_mod_hom by simp from subresultant_prs_def[of G1 G2, unfolded sub Let_def this] have id: "Gk = G2" "hk = lead_coeff G2 ^ (degree G1 - degree G2)" by auto from F12 F1 F2 have "G1 \ 0" "G2 \ 0" by auto from resultant_pseudo_mod_0[OF pm deg_G12 this] have res: "resultant G1 G2 = (if degree G2 = 0 then lead_coeff G2 ^ degree G1 else 0)" by simp from True[unfolded 2 n F2] have "degree G2 = 0" by simp thus ?thesis unfolding res 2 F2 id by simp qed qed finally show ?thesis . qed end end text \At this point, we have soundness of the resultant-implementation, provided that we can instantiate the locale by constructing suitable values of F, b, h, etc. Now we show the existence of suitable locale parameters by constructively computing them.\ context fixes G1 G2 :: "'a :: idom_divide poly" begin private function F and b and h where "F i = (if i = (0 :: nat) then 1 else if i = 1 then map_poly to_fract G1 else if i = 2 then map_poly to_fract G2 else (let G = pseudo_mod (F (i - 2)) (F (i - 1)) in if F (i - 1) = 0 \ G = 0 then 0 else smult (inverse (b i)) G))" | "b i = (if i \ 2 then 1 else if i = 3 then (- 1) ^ (degree (F 1) - degree (F 2) + 1) else if F (i - 2) = 0 then 1 else (- 1) ^ (degree (F (i - 2)) - degree (F (i - 1)) + 1) * lead_coeff (F (i - 2)) * h (i - 2) ^ (degree (F (i - 2)) - degree (F (i - 1))))" | "h i = (if (i \ 1) then 1 else if i = 2 then (lead_coeff (F 2) ^ (degree (F 1) - degree (F 2))) else if F i = 0 then 1 else (lead_coeff (F i) ^ (degree (F (i - 1)) - degree (F i)) / (h (i - 1) ^ ((degree (F (i - 1)) - degree (F i)) - 1))))" by pat_completeness auto termination proof show "wf (measure (case_sum (\ fi. 3 * fi +1) (case_sum (\ bi. 3 * bi) (\ hi. 3 * hi + 2))))" by simp qed (auto simp: termination_simp) declare h.simps[simp del] b.simps[simp del] F.simps[simp del] private lemma Fb0: assumes base: "G1 \ 0" "G2 \ 0" shows "(F i = 0 \ F (Suc i) = 0) \ b i \ 0 \ h i \ 0" proof (induct i rule: less_induct) case (less i) note * [simp] = F.simps[of i] b.simps[of i] h.simps[of i] consider (0) "i = 0" | (1) "i = 1" | (2) "i \ 2" by linarith thus ?case proof cases case 0 show ?thesis unfolding * unfolding 0 by simp next case 1 show ?thesis unfolding * unfolding 1 using assms by simp next case 2 have F: "F i = 0 \ F (Suc i) = 0" unfolding F.simps[of "Suc i"] using 2 by simp from assms have F2: "F 2 \ 0" unfolding F.simps[of 2] by simp from 2 have "i - 1 < i" "i - 2 < i" by auto note IH = less[OF this(1)] less[OF this(2)] hence b: "b (i - 1) \ 0" and h: "h (i - 1) \ 0" "h (i - 2) \ 0" by auto from h have hi: "h i \ 0" unfolding h.simps[of i] using 2 F2 by auto have bi: "b i \ 0" unfolding b.simps[of i] using h(2) by auto show ?thesis using hi bi F by blast qed qed private definition "k = (LEAST i. F (Suc i) = 0)" private lemma k_exists: "\ i. F (Suc i) = 0" proof - obtain n i where "i \ 3" "length (coeffs (F (Suc i))) = n" by blast thus ?thesis proof (induct n arbitrary: i rule: less_induct) case (less n i) let ?ii = "Suc (Suc i)" let ?i = "Suc i" from less(2) have i: "?i \ 3" by auto let ?mod = "pseudo_mod (F (?ii - 2)) (F ?i)" have Fi: "F ?ii = (if F ?i = 0 \ ?mod = 0 then 0 else smult (inverse (b ?ii)) ?mod)" unfolding F.simps[of ?ii] using i by auto show ?case proof (cases "F ?ii = 0") case False hence Fi: "F ?ii = smult (inverse (b ?ii)) ?mod" and mod: "?mod \ 0" and Fi1: "F ?i \ 0" unfolding Fi by auto from pseudo_mod[OF Fi1, of "F (?ii - 2)"] mod have "degree ?mod < degree (F ?i)" by simp hence deg: "degree (F ?ii) < degree (F ?i)" unfolding Fi by auto hence "length (coeffs (F ?ii)) < length (coeffs (F ?i))" unfolding degree_eq_length_coeffs by auto from less(1)[OF _ i refl, folded less(3), OF this] show ?thesis by auto qed blast qed qed private lemma k: "F (Suc k) = 0" "i < k \ F (Suc i) \ 0" proof - show "F (Suc k) = 0" unfolding k_def using k_exists by (rule LeastI2_ex) assume "i < k" from not_less_Least[OF this[unfolded k_def]] show "F (Suc i) \ 0" . qed lemma enter_subresultant_prs: assumes len: "length (coeffs G1) \ length (coeffs G2)" and G2: "G2 \ 0" shows "\ F n d f k b. subresultant_prs_locale2 F n d f k b G1 G2" proof (intro exI) from G2 len have G1: "G1 \ 0" by auto from len have deg_le: "degree (F 2) \ degree (F 1)" by (simp add: F.simps degree_eq_length_coeffs) from G2 G1 have F1: "F 1 \ 0" and F2: "F 2 \ 0" by (auto simp: F.simps) note Fb0 = Fb0[OF G1 G2] interpret s: subresultant_prs_locale F "\ i. degree (F i)" "\ i. degree (F i) - degree (F (Suc i))" "\ i. lead_coeff (F i)" k b G1 G2 proof (unfold_locales, rule refl, rule refl, rule refl, rule deg_le, rule F1, rule F2) from k(1) F1 have k0: "k \ 0" by (cases k, auto) show Fk: "(F i = 0) = (k < i)" for i proof assume "F i = 0" with k(2)[of "i - 1"] have "\ (i - 1 < k)" by (cases i, auto simp: F.simps) thus "i > k" using k0 by auto next assume "i > k" then obtain j l where i: "i = j + l" and "j = Suc k" and "l = i - Suc k" and Fj: "F j = 0" using k(1) by auto with F1 F2 k0 have j2: "j \ 2" by auto show "F i = 0" unfolding i proof (induct l) case (Suc l) thus ?case unfolding F.simps[of "j + Suc l"] using j2 by auto qed (auto simp: Fj) qed show b: "b i \ 0" for i using Fb0 by blast show "F 1 = map_poly to_fract G1" unfolding F.simps[of 1] by simp show "F 2 = map_poly to_fract G2" unfolding F.simps[of 2] by simp fix i let ?mod = "pseudo_mod (F (i - 2)) (F (i - 1))" assume i: "3 \ i" "i \ Suc k" from Fk[of "i - 1"] i have "F (i - 1) \ 0" by auto with i have Fi: "F i = (if ?mod = 0 then 0 else smult (inverse (b i)) ?mod)" unfolding F.simps[of i] Let_def by simp show "smult (b i) (F i) = ?mod" proof (cases "?mod = 0") case True thus ?thesis unfolding Fi by simp next case False with Fi have Fi: "F i = smult (inverse (b i)) ?mod" by simp from arg_cong[OF this, of "smult (b i)"] b[of i] show ?thesis by simp qed qed note s.h.simps[simp del] show "subresultant_prs_locale2 F (\ i. degree (F i)) (\ i. degree (F i) - degree (F (Suc i))) (\ i. lead_coeff (F i)) k b G1 G2" proof show "b 3 = (- 1) ^ (degree (F 1) - degree (F (Suc 1)) + 1)" unfolding b.simps numeral_2_eq_2 by simp fix i assume i: "4 \ i" "i \ Suc k" with s.F0[of "i - 2"] have "F (i - 2) \ 0" by auto hence bi: "b i = (- 1) ^ (degree (F (i - 2)) - degree (F (i - 1)) + 1) * lead_coeff (F (i - 2)) * h (i - 2) ^ (degree (F (i - 2)) - degree (F (i - 1)))" unfolding b.simps using i by auto have "i < k \ s.h i = h i" for i proof (induct i) case 0 thus ?case by (simp add: h.simps s.h.simps) next case (Suc i) from Suc(2) s.F0[of "Suc i"] have "F (Suc i) \ 0" by auto with Suc show ?case unfolding h.simps[of "Suc i"] s.h.simps[of "Suc i"] numeral_2_eq_2 by simp qed hence sh: "s.h (i - 2) = h (i - 2)" using i by simp from i have *: "Suc (i - 2) = i - 1" by auto show "b i = (- 1) ^ (degree (F (i - 2)) - degree (F (Suc (i - 2))) + 1) * lead_coeff (F (i - 2)) * s.h (i - 2) ^ (degree (F (i - 2)) - degree (F (Suc (i - 2))))" unfolding sh bi * .. qed qed end text \Now we obtain the soundness lemma outside the locale.\ context div_exp_sound begin lemma resultant_impl_main: assumes len: "length (coeffs G1) \ length (coeffs G2)" shows "resultant_impl_main G1 G2 = resultant G1 G2" proof (cases "G2 = 0") case G2: False from enter_subresultant_prs[OF len G2] obtain F n d f k b where "subresultant_prs_locale2 F n d f k b G1 G2" by auto interpret subresultant_prs_locale2 F n d f k b G1 G2 by fact show ?thesis by (rule resultant_impl_main, standard) next case G2: True show ?thesis unfolding G2 resultant_impl_main_def using resultant_const(2)[of G1 0] by simp qed theorem resultant_impl: "resultant_impl = resultant" proof (intro ext) fix f g :: "'a poly" show "resultant_impl f g = resultant f g" proof (cases "length (coeffs f) \ length (coeffs g)") case True thus ?thesis unfolding resultant_impl_def resultant_impl_main[OF True] by auto next case False hence "length (coeffs g) \ length (coeffs f)" by auto from resultant_impl_main[OF this] show ?thesis unfolding resultant_impl_def resultant_swap[of f g] using False by (auto simp: Let_def) qed qed end subsection \Code Equations\ text \In the following code-equations, we only compute the required values, e.g., $h_k$ is not required if $n_k > 0$, we compute $(-1)^{\ldots} * \ldots$ via a case-analysis, and we perform special cases for $\delta_i = 1$, which is the most frequent case.\ context div_exp_param begin partial_function(tailrec) subresultant_prs_main_impl where "subresultant_prs_main_impl f Gi_1 Gi ni_1 d1_1 hi_2 = (let gi_1 = lead_coeff Gi_1; ni = degree Gi; hi_1 = (if d1_1 = 1 then gi_1 else div_exp gi_1 hi_2 d1_1); d1 = ni_1 - ni; pmod = pseudo_mod Gi_1 Gi in (if pmod = 0 then f (Gi, (if d1 = 1 then lead_coeff Gi else div_exp (lead_coeff Gi) hi_1 d1)) else let gi = lead_coeff Gi; divisor = (-1) ^ (d1 + 1) * gi_1 * (hi_1 ^ d1) ; Gi_p1 = sdiv_poly pmod divisor in subresultant_prs_main_impl f Gi Gi_p1 ni d1 hi_1))" definition subresultant_prs_impl where "subresultant_prs_impl f G1 G2 = (let pmod = pseudo_mod G1 G2; n2 = degree G2; delta_1 = (degree G1 - n2); g2 = lead_coeff G2; h2 = g2 ^ delta_1 in if pmod = 0 then f (G2,h2) else let G3 = (- 1) ^ (delta_1 + 1) * pmod; g3 = lead_coeff G3; n3 = degree G3; d2 = n2 - n3; pmod = pseudo_mod G2 G3 in if pmod = 0 then f (G3, if d2 = 1 then g3 else div_exp g3 h2 d2) else let divisor = (- 1) ^ (d2 + 1) * g2 * h2 ^ d2; G4 = sdiv_poly pmod divisor in subresultant_prs_main_impl f G3 G4 n3 d2 h2 )" end context div_exp_sound begin lemma div_exp_1: "div_exp g h (Suc 0) = g" using div_exp[of g "Suc 0" h] by simp lemma subresultant_prs_impl: "subresultant_prs_impl f G1 G2 = f (subresultant_prs G1 G2)" proof - define h2 where "h2 = lead_coeff G2 ^ (degree G1 - degree G2)" define G3 where "G3 = ((- 1) ^ (degree G1 - degree G2 + 1) * pseudo_mod G1 G2)" define G4 where "G4 = sdiv_poly (pseudo_mod G2 G3) ((- 1) ^ (degree G2 - degree G3 + 1) * lead_coeff G2 * h2 ^ (degree G2 - degree G3))" define d2 where "d2 = degree G2 - degree G3" have dl1: "(if d = 1 then (g :: 'a) else div_exp g h d) = div_exp g h d" for d g h by (cases "d = 1", auto simp: div_exp_1) show ?thesis unfolding subresultant_prs_impl_def subresultant_prs_def Let_def subresultant_prs_main.simps[of G2] if_distrib[of f] dl1 proof (rule if_cong[OF refl refl if_cong[OF refl refl]], unfold h2_def[symmetric], unfold G3_def[symmetric], unfold G4_def[symmetric], unfold d2_def[symmetric]) note simp = subresultant_prs_main_impl.simps[of f] subresultant_prs_main.simps show "subresultant_prs_main_impl f G3 G4 (degree G3) d2 h2 = f (subresultant_prs_main G3 G4 (div_exp (lead_coeff G3) h2 d2))" proof (induct G4 arbitrary: G3 d2 h2 rule: wf_induct[OF wf_measure[of degree]]) case (1 G4 G3 d2 h2) let ?M = "pseudo_mod G3 G4" show ?case proof (cases "?M = 0") case True thus ?thesis unfolding simp[of G3] Let_def dl1 by simp next case False hence id: "(?M = 0) = False" by auto let ?c = "((- 1) ^ (degree G3 - degree G4 + 1) * lead_coeff G3 * (div_exp (lead_coeff G3) h2 d2) ^ (degree G3 - degree G4))" let ?N = "sdiv_poly ?M ?c" show ?thesis proof (cases "G4 = 0") case G4: False have "degree ?N \ degree ?M" unfolding sdiv_poly_def by (rule degree_map_poly_le) also have "\ < degree G4" using pseudo_mod[OF G4, of G3] False by auto finally show ?thesis unfolding simp[of G3] Let_def id if_False dl1 by (intro 1(1)[rule_format], auto) next case 0: True with False have "G3 \ 0" by auto show ?thesis unfolding 0 unfolding simp[of G3] Let_def unfolding dl1 simp[of 0] by simp qed qed qed qed qed definition "resultant_impl_rec = subresultant_prs_main_impl (\ (Gk,hk). if degree Gk = 0 then hk else 0)" definition "resultant_impl_start = subresultant_prs_impl (\ (Gk,hk). if degree Gk = 0 then hk else 0)" lemma resultant_impl_start_code: "resultant_impl_start G1 G2 = (let pmod = pseudo_mod G1 G2; n2 = degree G2; n1 = degree G1; g2 = lead_coeff G2; d1 = n1 - n2 in if pmod = 0 then if n2 = 0 then if d1 = 0 then 1 else if d1 = 1 then g2 else g2 ^ d1 else 0 else let G3 = if even d1 then - pmod else pmod; n3 = degree G3; pmod = pseudo_mod G2 G3 in if pmod = 0 then if n3 = 0 then let d2 = n2 - n3; g3 = lead_coeff G3 in (if d2 = 1 then g3 else div_exp g3 (if d1 = 1 then g2 else g2 ^ d1) d2) else 0 else let h2 = (if d1 = 1 then g2 else g2 ^ d1); d2 = n2 - n3; divisor = (if d2 = 1 then g2 * h2 else if even d2 then - g2 * h2 ^ d2 else g2 * h2 ^ d2); G4 = sdiv_poly pmod divisor in resultant_impl_rec G3 G4 n3 d2 h2)" proof - obtain d1 where d1: "degree G1 - degree G2 = d1" by auto have id1: "(if even d1 then - pmod else pmod) = (-1)^ (d1 + 1) * (pmod :: 'a poly)" for pmod by simp have id3: "(if d2 = 1 then g2 * h2 else if even d2 then - g2 * h2 ^ d2 else g2 * h2 ^ d2) = ((- 1) ^ (d2 + 1) * g2 * h2 ^ d2)" for d2 and g2 h2 :: 'a by auto show ?thesis unfolding resultant_impl_start_def subresultant_prs_impl_def resultant_impl_rec_def[symmetric] Let_def split unfolding d1 unfolding id1 unfolding id3 by (rule if_cong[OF refl if_cong if_cong], auto simp: power2_eq_square) qed lemma resultant_impl_rec_code: "resultant_impl_rec Gi_1 Gi ni_1 d1_1 hi_2 = ( let ni = degree Gi; pmod = pseudo_mod Gi_1 Gi in if pmod = 0 then if ni = 0 then let d1 = ni_1 - ni; gi = lead_coeff Gi in if d1 = 1 then gi else let gi_1 = lead_coeff Gi_1; hi_1 = (if d1_1 = 1 then gi_1 else div_exp gi_1 hi_2 d1_1) in div_exp gi hi_1 d1 else 0 else let d1 = ni_1 - ni; gi_1 = lead_coeff Gi_1; hi_1 = (if d1_1 = 1 then gi_1 else div_exp gi_1 hi_2 d1_1); divisor = if d1 = 1 then gi_1 * hi_1 else if even d1 then - gi_1 * hi_1 ^ d1 else gi_1 * hi_1 ^ d1; Gi_p1 = sdiv_poly pmod divisor in resultant_impl_rec Gi Gi_p1 ni d1 hi_1)" unfolding resultant_impl_rec_def subresultant_prs_main_impl.simps[of _ Gi_1] split Let_def unfolding resultant_impl_rec_def[symmetric] by (rule if_cong[OF _ if_cong _], auto) lemma resultant_impl_main_code: "resultant_impl_main G1 G2 = (if G2 = 0 then if degree G1 = 0 then 1 else 0 else resultant_impl_start G1 G2)" unfolding resultant_impl_main_def resultant_impl_start_def subresultant_prs_impl by simp lemma resultant_impl_code: "resultant_impl f g = (if length (coeffs f) \ length (coeffs g) then resultant_impl_main f g else let res = resultant_impl_main g f in if even (degree f) \ even (degree g) then res else - res)" unfolding resultant_impl_def resultant_impl_def .. lemma resultant_code: "resultant = resultant_impl" using resultant_impl by fastforce lemmas resultant_code_lemmas = resultant_impl_code resultant_impl_main_code resultant_impl_start_code resultant_impl_rec_code end global_interpretation div_exp_Lazard: div_exp_sound "dichotomous_Lazard :: 'a :: factorial_ring_gcd \ _" defines resultant_impl_Lazard = div_exp_Lazard.resultant_impl and resultant_impl_main_Lazard = div_exp_Lazard.resultant_impl_main and resultant_impl_start_Lazard = div_exp_Lazard.resultant_impl_start and resultant_impl_rec_Lazard = div_exp_Lazard.resultant_impl_rec by (rule dichotomous_Lazard) declare div_exp_Lazard.resultant_code_lemmas[code] text \As default use Lazard-implementation, which implements resultants on factorial rings.\ declare div_exp_Lazard.resultant_code[code] text \We also provide a second implementation without Lazard's optimization, which works on integral domains.\ global_interpretation div_exp_basic: div_exp_sound basic_div_exp defines resultant_impl_basic = div_exp_basic.resultant_impl and resultant_impl_main_basic = div_exp_basic.resultant_impl_main and resultant_impl_start_basic = div_exp_basic.resultant_impl_start and resultant_impl_rec_basic = div_exp_basic.resultant_impl_rec by (rule basic_div_exp) declare div_exp_basic.resultant_code_lemmas[code] thm div_exp_basic.resultant_code end \ No newline at end of file diff --git a/thys/Winding_Number_Eval/Missing_Algebraic.thy b/thys/Winding_Number_Eval/Missing_Algebraic.thy --- a/thys/Winding_Number_Eval/Missing_Algebraic.thy +++ b/thys/Winding_Number_Eval/Missing_Algebraic.thy @@ -1,371 +1,335 @@ (* Author: Wenda Li *) section \Some useful lemmas in algebra\ theory Missing_Algebraic imports "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" "HOL-Complex_Analysis.Complex_Analysis" Missing_Topology "Budan_Fourier.BF_Misc" begin subsection \Misc\ lemma poly_holomorphic_on[simp]: "(poly p) holomorphic_on s" apply (rule holomorphic_onI) apply (unfold field_differentiable_def) apply (rule_tac x="poly (pderiv p) x" in exI) by (simp add:has_field_derivative_at_within) lemma order_zorder: fixes p::"complex poly" and z::complex assumes "p\0" shows "order z p = nat (zorder (poly p) z)" proof - define n where "n=nat (zorder (poly p) z)" define h where "h=zor_poly (poly p) z" have "\w. poly p w \ 0" using assms poly_all_0_iff_0 by auto then obtain r where "0 < r" "cball z r \ UNIV" and h_holo: "h holomorphic_on cball z r" and poly_prod:"(\w\cball z r. poly p w = h w * (w - z) ^ n \ h w \ 0)" using zorder_exist_zero[of "poly p" UNIV z,folded h_def] poly_holomorphic_on unfolding n_def by auto then have "h holomorphic_on ball z r" and "(\w\ball z r. poly p w = h w * (w - z) ^ n)" and "h z\0" by auto then have "order z p = n" using \p\0\ proof (induct n arbitrary:p h) case 0 then have "poly p z=h z" using \r>0\ by auto then have "poly p z\0" using \h z\0\ by auto then show ?case using order_root by blast next case (Suc n) define sn where "sn=Suc n" define h' where "h'\ \w. deriv h w * (w-z)+ sn * h w" have "(poly p has_field_derivative poly (pderiv p) w) (at w)" for w using poly_DERIV[of p w] . moreover have "(poly p has_field_derivative (h' w)*(w-z)^n ) (at w)" when "w\ball z r" for w proof (subst DERIV_cong_ev[of w w "poly p" "\w. h w * (w - z) ^ Suc n" ],simp_all) show "\\<^sub>F x in nhds w. poly p x = h x * ((x - z) * (x - z) ^ n)" unfolding eventually_nhds using Suc(3) \w\ball z r\ apply (intro exI[where x="ball z r"]) by auto next have "(h has_field_derivative deriv h w) (at w)" using \h holomorphic_on ball z r\ \w\ball z r\ holomorphic_on_imp_differentiable_at by (simp add: holomorphic_derivI) then have "((\w. h w * ((w - z) ^ sn)) has_field_derivative h' w * (w - z) ^ (sn - 1)) (at w)" unfolding h'_def apply (auto intro!: derivative_eq_intros simp add:field_simps) by (auto simp add:field_simps sn_def) then show "((\w. h w * ((w - z) * (w - z) ^ n)) has_field_derivative h' w * (w - z) ^ n) (at w)" unfolding sn_def by auto qed ultimately have "\w\ball z r. poly (pderiv p) w = h' w * (w - z) ^ n" using DERIV_unique by blast moreover have "h' holomorphic_on ball z r" unfolding h'_def using \h holomorphic_on ball z r\ by (auto intro!: holomorphic_intros) moreover have "h' z\0" unfolding h'_def sn_def using \h z \ 0\ of_nat_neq_0 by auto moreover have "pderiv p \ 0" proof assume "pderiv p = 0" obtain c where "p=[:c:]" using \pderiv p = 0\ using pderiv_iszero by blast then have "c=0" using Suc(3)[rule_format,of z] \r>0\ by auto then show False using \p\0\ using \p=[:c:]\ by auto qed ultimately have "order z (pderiv p) = n" by (auto elim: Suc.hyps) moreover have "order z p \ 0" using Suc(3)[rule_format,of z] \r>0\ order_root \p\0\ by auto ultimately show ?case using order_pderiv[OF \pderiv p \ 0\] by auto qed then show ?thesis unfolding n_def . qed lemma pcompose_pCons_0:"pcompose p [:a:] = [:poly p a:]" apply (induct p) by (auto simp add:pcompose_pCons algebra_simps) lemma pcompose_coeff_0: "coeff (pcompose p q) 0 = poly p (coeff q 0)" apply (induct p) by (auto simp add:pcompose_pCons coeff_mult) lemma poly_field_differentiable_at[simp]: "poly p field_differentiable (at x within s)" apply (unfold field_differentiable_def) apply (rule_tac x="poly (pderiv p) x" in exI) by (simp add:has_field_derivative_at_within) lemma deriv_pderiv: "deriv (poly p) = poly (pderiv p)" apply (rule ext) apply (rule DERIV_imp_deriv) using poly_DERIV . lemma lead_coeff_map_poly_nz: assumes "f (lead_coeff p) \0" "f 0=0" shows "lead_coeff (map_poly f p) = f (lead_coeff p) " proof - have "lead_coeff (Poly (map f (coeffs p))) = f (lead_coeff p)" by (metis (mono_tags, lifting) antisym assms(1) assms(2) coeff_0_degree_minus_1 coeff_map_poly degree_Poly degree_eq_length_coeffs le_degree length_map map_poly_def) then show ?thesis by (simp add: map_poly_def) qed lemma filterlim_poly_at_infinity: fixes p::"'a::real_normed_field poly" assumes "degree p>0" shows "filterlim (poly p) at_infinity at_infinity" using assms proof (induct p) case 0 then show ?case by auto next case (pCons a p) have ?case when "degree p=0" proof - obtain c where c_def:"p=[:c:]" using \degree p = 0\ degree_eq_zeroE by blast then have "c\0" using \0 < degree (pCons a p)\ by auto then show ?thesis unfolding c_def apply (auto intro!:tendsto_add_filterlim_at_infinity) apply (subst mult.commute) by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident) qed moreover have ?case when "degree p\0" proof - have "filterlim (poly p) at_infinity at_infinity" using that by (auto intro:pCons) then show ?thesis by (auto intro!:tendsto_add_filterlim_at_infinity filterlim_at_infinity_times filterlim_ident) qed ultimately show ?case by auto qed lemma poly_divide_tendsto_aux: fixes p::"'a::real_normed_field poly" shows "((\x. poly p x/x^(degree p)) \ lead_coeff p) at_infinity" proof (induct p) case 0 then show ?case by (auto intro:tendsto_eq_intros) next case (pCons a p) have ?case when "p=0" using that by auto moreover have ?case when "p\0" proof - define g where "g=(\x. a/(x*x^degree p))" define f where "f=(\x. poly p x/x^degree p)" have "\\<^sub>Fx in at_infinity. poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume "norm x\1" then have "x\0" by auto then show "poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" using that unfolding g_def f_def by (auto simp add:field_simps) qed moreover have "((\x. g x+f x) \ lead_coeff (pCons a p)) at_infinity" proof - have "(g \ 0) at_infinity" unfolding g_def using filterlim_poly_at_infinity[of "monom 1 (Suc (degree p))"] apply (auto intro!:tendsto_intros tendsto_divide_0 simp add: degree_monom_eq) apply (subst filterlim_cong[where g="poly (monom 1 (Suc (degree p)))"]) by (auto simp add:poly_monom) moreover have "(f \ lead_coeff (pCons a p)) at_infinity" using pCons \p\0\ unfolding f_def by auto ultimately show ?thesis by (auto intro:tendsto_eq_intros) qed ultimately show ?thesis by (auto dest:tendsto_cong) qed ultimately show ?case by auto qed lemma filterlim_power_at_infinity: assumes "n\0" shows "filterlim (\x::'a::real_normed_field. x^n) at_infinity at_infinity" using filterlim_poly_at_infinity[of "monom 1 n"] assms apply (subst filterlim_cong[where g="poly (monom 1 n)"]) by (auto simp add:poly_monom degree_monom_eq) lemma poly_divide_tendsto_0_at_infinity: fixes p::"'a::real_normed_field poly" assumes "degree p > degree q" shows "((\x. poly q x / poly p x) \ 0 ) at_infinity" proof - define pp where "pp=(\x. x^(degree p) / poly p x)" define qq where "qq=(\x. poly q x/x^(degree q))" define dd where "dd=(\x::'a. 1/x^(degree p - degree q))" have "\\<^sub>Fx in at_infinity. poly q x / poly p x = qq x * pp x * dd x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume "norm x\1" then have "x\0" by auto then show "poly q x / poly p x = qq x * pp x * dd x" unfolding qq_def pp_def dd_def using assms by (auto simp add:field_simps divide_simps power_diff) qed moreover have "((\x. qq x * pp x * dd x) \ 0) at_infinity" proof - have "(qq \ lead_coeff q) at_infinity" unfolding qq_def using poly_divide_tendsto_aux[of q] . moreover have "(pp \ 1/lead_coeff p) at_infinity" proof - have "p\0" using assms by auto then show ?thesis unfolding pp_def using poly_divide_tendsto_aux[of p] apply (drule_tac tendsto_inverse) by (auto simp add:inverse_eq_divide) qed moreover have "(dd \ 0) at_infinity" unfolding dd_def apply (rule tendsto_divide_0) by (auto intro!: filterlim_power_at_infinity simp add:assms) ultimately show ?thesis by (auto intro:tendsto_eq_intros) qed ultimately show ?thesis by (auto dest:tendsto_cong) qed lemma lead_coeff_list_def: "lead_coeff p= (if coeffs p=[] then 0 else last (coeffs p))" by (simp add: last_coeffs_eq_coeff_degree) lemma poly_linepath_comp: fixes a::"'a::{real_normed_vector,comm_semiring_0,real_algebra_1}" shows "poly p o (linepath a b) = poly (p \\<^sub>p [:a, b-a:]) o of_real" apply rule by (auto simp add:poly_pcompose linepath_def scaleR_conv_of_real algebra_simps) lemma poly_eventually_not_zero: fixes p::"real poly" assumes "p\0" shows "eventually (\x. poly p x\0) at_infinity" proof (rule eventually_at_infinityI[of "Max (norm ` {x. poly p x=0}) + 1"]) fix x::real assume asm:"Max (norm ` {x. poly p x=0}) + 1 \ norm x" have False when "poly p x=0" proof - define S where "S=norm `{x. poly p x = 0}" have "norm x\S" using that unfolding S_def by auto moreover have "finite S" using \p\0\ poly_roots_finite unfolding S_def by blast ultimately have "norm x\Max S" by simp moreover have "Max S + 1 \ norm x" using asm unfolding S_def by simp ultimately show False by argo qed then show "poly p x \ 0" by auto qed subsection \More about @{term degree}\ -lemma degree_div_less: - fixes x y::"'a::field poly" - assumes "degree x\0" "degree y\0" - shows "degree (x div y) < degree x" -proof - - have "x\0" "y\0" using assms by auto - define q r where "q=x div y" and "r=x mod y" - have *:"eucl_rel_poly x y (q, r)" unfolding q_def r_def - by (simp add: eucl_rel_poly) - then have "r = 0 \ degree r < degree y" using \y\0\ unfolding eucl_rel_poly_iff by auto - moreover have ?thesis when "r=0" - proof - - have "x = q * y" using * that unfolding eucl_rel_poly_iff by auto - then have "q\0" using \x\0\ \y\0\ by auto - from degree_mult_eq[OF this \y\0\] \x = q * y\ - have "degree x = degree q +degree y" by auto - then show ?thesis unfolding q_def using assms by auto - qed - moreover have ?thesis when "degree rdegree x") - case True - then have "q=0" unfolding q_def using div_poly_less by auto - then show ?thesis unfolding q_def using assms(1) by auto - next - case False - then have "degree x>degree r" using that by auto - then have "degree x = degree (x-r)" using degree_add_eq_right[of "-r" x] by auto - have "x-r = q*y" using * unfolding eucl_rel_poly_iff by auto - then have "q\0" using \degree r < degree x\ by auto - have "degree x = degree q +degree y" - using degree_mult_eq[OF \q\0\ \y\0\] \x-r = q*y\ \degree x = degree (x-r)\ by auto - then show ?thesis unfolding q_def using assms by auto - qed - ultimately show ?thesis by auto -qed - lemma map_poly_degree_eq: assumes "f (lead_coeff p) \0" shows "degree (map_poly f p) = degree p" using assms unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly lead_coeff_list_def by (metis (full_types) last_conv_nth_default length_map no_trailing_unfold nth_default_coeffs_eq nth_default_map_eq strip_while_idem) lemma map_poly_degree_less: assumes "f (lead_coeff p) =0" "degree p\0" shows "degree (map_poly f p) < degree p" proof - have "length (coeffs p) >1" using \degree p\0\ by (simp add: degree_eq_length_coeffs) then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0" by (metis One_nat_def add.commute add_diff_cancel_left' append_Nil assms(2) degree_eq_length_coeffs length_greater_0_conv list.size(3) list.size(4) not_less_zero rev_exhaust) have "f x=0" using assms(1) by (simp add: lead_coeff_list_def xs_def(1)) have "degree (map_poly f p) = length (strip_while ((=) 0) (map f (xs@[x]))) - 1" unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly by (subst xs_def,auto) also have "... = length (strip_while ((=) 0) (map f xs)) - 1" using \f x=0\ by simp also have "... \ length xs -1" using length_strip_while_le by (metis diff_le_mono length_map) also have "... < length (xs@[x]) - 1" using xs_def(2) by auto also have "... = degree p" unfolding degree_eq_length_coeffs xs_def by simp finally show ?thesis . qed lemma map_poly_degree_leq[simp]: shows "degree (map_poly f p) \ degree p" unfolding map_poly_def degree_eq_length_coeffs by (metis coeffs_Poly diff_le_mono length_map length_strip_while_le) subsection \roots / zeros of a univariate function\ definition roots_within::"('a \ 'b::zero) \ 'a set \ 'a set" where "roots_within f s = {x\s. f x = 0}" abbreviation roots::"('a \ 'b::zero) \ 'a set" where "roots f \ roots_within f UNIV" subsection \The argument principle specialised to polynomials.\ lemma argument_principle_poly: assumes "p\0" and valid:"valid_path g" and loop: "pathfinish g = pathstart g" and no_proots:"path_image g \ - proots p" shows "contour_integral g (\x. deriv (poly p) x / poly p x) = 2 * of_real pi * \ * (\x\proots p. winding_number g x * of_nat (order x p))" proof - have "contour_integral g (\x. deriv (poly p) x / poly p x) = 2 * of_real pi * \ * (\x | poly p x = 0. winding_number g x * of_int (zorder (poly p) x))" apply (rule argument_principle[of UNIV "poly p" "{}" "\_. 1" g,simplified,OF _ valid loop]) using no_proots[unfolded proots_def] by (auto simp add:poly_roots_finite[OF \p\0\] ) also have "... = 2 * of_real pi * \ * (\x\proots p. winding_number g x * of_nat (order x p))" proof - have "nat (zorder (poly p) x) = order x p" when "x\proots p" for x using order_zorder[OF \p\0\] that unfolding proots_def by auto then show ?thesis unfolding proots_def apply (auto intro!:comm_monoid_add_class.sum.cong) by (metis assms(1) nat_eq_iff2 of_nat_nat order_root) qed finally show ?thesis . qed end