diff --git a/thys/Algebraic_Numbers/Algebraic_Numbers_Pre_Impl.thy b/thys/Algebraic_Numbers/Algebraic_Numbers_Pre_Impl.thy new file mode 100644 --- /dev/null +++ b/thys/Algebraic_Numbers/Algebraic_Numbers_Pre_Impl.thy @@ -0,0 +1,336 @@ +(* + Author: Sebastiaan Joosten + René Thiemann + Akihisa Yamada + License: BSD +*) +section \Algebraic Numbers -- Preliminary Implementation\ + +text \This theory gathers some preliminary results to implement algebraic numbers, + e.g., it defines an invariant to have unique representing polynomials and shows + that polynomials for unary minus and inversion preserve this invariant.\ + + +theory Algebraic_Numbers_Pre_Impl +imports + "Abstract-Rewriting.SN_Order_Carrier" + Deriving.Compare_Rat + Deriving.Compare_Real + Jordan_Normal_Form.Gauss_Jordan_IArray_Impl + Algebraic_Numbers + Sturm_Rat + Factors_of_Int_Poly + Min_Int_Poly +begin + +text \For algebraic numbers, it turned out that @{const gcd_int_poly} is not + preferable to the default implementation of @{const gcd}, which just implements + Collin's primitive remainder sequence.\ +declare gcd_int_poly_code[code_unfold del] + +(*TODO: move *) +lemma ex1_imp_Collect_singleton: "(\!x. P x) \ P x \ Collect P = {x}" +proof(intro iffI conjI, unfold conj_imp_eq_imp_imp) + assume "Ex1 P" "P x" then show "Collect P = {x}" by blast +next + assume Px: "Collect P = {x}" + then have "P y \ x = y" for y by auto + then show "Ex1 P" by auto + from Px show "P x" by auto +qed + +lemma ex1_Collect_singleton[consumes 2]: + assumes "\!x. P x" and "P x" and "Collect P = {x} \ thesis" shows thesis + by (rule assms(3), subst ex1_imp_Collect_singleton[symmetric], insert assms(1,2), auto) + +lemma ex1_iff_Collect_singleton: "P x \ (\!x. P x) \ Collect P = {x}" + by (subst ex1_imp_Collect_singleton[symmetric], auto) + +context + fixes f + assumes bij: "bij f" +begin +lemma bij_imp_ex1_iff: "(\!x. P (f x)) \ (\!y. P y)" (is "?l = ?r") +proof (intro iffI) + assume l: ?l + then obtain x where "P (f x)" by auto + with l have *: "{x} = Collect (P o f)" by auto + also have "f ` \ = {y. P (f (Hilbert_Choice.inv f y))}" using bij_image_Collect_eq[OF bij] by auto + also have "\ = {y. P y}" + proof- + have "f (Hilbert_Choice.inv f y) = y" for y by (meson bij bij_inv_eq_iff) + then show ?thesis by simp + qed + finally have "Collect P = {f x}" by auto + then show ?r by (fold ex1_imp_Collect_singleton, auto) +next + assume r: ?r + then obtain y where "P y" by auto + with r have "{y} = Collect P" by auto + also have "Hilbert_Choice.inv f ` \ = Collect (P \ f)" + using bij_image_Collect_eq[OF bij_imp_bij_inv[OF bij]] bij by (auto simp: inv_inv_eq) + finally have "Collect (P o f) = {Hilbert_Choice.inv f y}" by (simp add: o_def) + then show ?l by (fold ex1_imp_Collect_singleton, auto) +qed + +lemma bij_ex1_imp_the_shift: + assumes ex1: "\!y. P y" shows "(THE x. P (f x)) = Hilbert_Choice.inv f (THE y. P y)" (is "?l = ?r") +proof- + from ex1 have "P (THE y. P y)" by (rule the1I2) + moreover from ex1[folded bij_imp_ex1_iff] have "P (f (THE x. P (f x)))" by (rule the1I2) + ultimately have "(THE y. P y) = f (THE x. P (f x))" using ex1 by auto + also have "Hilbert_Choice.inv f \ = (THE x. P (f x))" using bij by (simp add: bij_is_inj) + finally show "?l = ?r" by auto +qed + +lemma bij_imp_Collect_image: "{x. P (f x)} = Hilbert_Choice.inv f ` {y. P y}" (is "?l = ?g ` _") +proof- + have "?l = ?g ` f ` ?l" by (simp add: image_comp inv_o_cancel[OF bij_is_inj[OF bij]]) + also have "f ` ?l = {f x | x. P (f x)}" by auto + also have "\ = {y. P y}" by (metis bij bij_iff) + finally show ?thesis. +qed + +lemma bij_imp_card_image: "card (f ` X) = card X" + by (metis bij bij_iff card.infinite finite_imageD inj_onI inj_on_iff_eq_card) + +end + +definition poly_cond :: "int poly \ bool" where + "poly_cond p = (lead_coeff p > 0 \ irreducible p)" + +lemma poly_condI[intro]: + assumes "lead_coeff p > 0" and "irreducible p" shows "poly_cond p" using assms by (auto simp: poly_cond_def) + +lemma poly_condD: + assumes "poly_cond p" + shows "irreducible p" and "lead_coeff p > 0" and "root_free p" and "square_free p" and "p \ 0" + using assms unfolding poly_cond_def using irreducible_root_free irreducible_imp_square_free cf_pos_def by auto + +lemma poly_condE[elim]: + assumes "poly_cond p" + and "irreducible p \ lead_coeff p > 0 \ root_free p \ square_free p \ p \ 0 \ thesis" + shows thesis + using assms by (auto dest:poly_condD) + +lemma poly_cond_abs_int_poly[simp]: "irreducible p \ poly_cond (abs_int_poly p)" + unfolding poly_cond_def by (cases "p = 0", auto) + + +definition poly_uminus_abs :: "int poly \ int poly" where + "poly_uminus_abs p = abs_int_poly (poly_uminus p)" + +lemma irreducible_poly_uminus[simp]: "irreducible p \ irreducible (poly_uminus (p :: int poly))" +proof (cases "degree p = 0") + case True + from degree0_coeffs[OF this] + obtain a where p: "p = [:a:]" by auto + have "poly_uminus p = p" unfolding p by (cases "a = 0", auto) + thus "irreducible p \ irreducible (poly_uminus p)" by auto +next + case False + from poly_uminus_irreducible[OF _ this] + show "irreducible p \ irreducible (poly_uminus p)" . +qed + +lemma irreducible_poly_uminus_abs[simp]: "irreducible p \ irreducible (poly_uminus_abs p)" + unfolding poly_uminus_abs_def using irreducible_poly_uminus[of p] by auto + +lemma poly_cond_poly_uminus_abs[simp]: "poly_cond p \ poly_cond (poly_uminus_abs p)" + by (auto simp: poly_cond_def, unfold poly_uminus_abs_def, subst pos_poly_abs_poly, auto) + +lemma ipoly_poly_uminus_abs_zero[simp]: "ipoly (poly_uminus_abs p) (x :: 'a :: idom) = 0 \ ipoly p (-x) = 0" + unfolding poly_uminus_abs_def by simp + +lemma degree_poly_uminus_abs[simp]: "degree (poly_uminus_abs p) = degree p" + unfolding poly_uminus_abs_def by auto + +definition poly_inverse :: "int poly \ int poly" where + "poly_inverse p = abs_int_poly (reflect_poly p)" + +lemma irreducible_poly_inverse[simp]: "coeff p 0 \ 0 \ irreducible p \ irreducible (poly_inverse p)" + unfolding poly_inverse_def by (auto simp: irreducible_reflect_poly) + +lemma degree_poly_inverse[simp]: "coeff p 0 \ 0 \ degree (poly_inverse p) = degree p" + unfolding poly_inverse_def by auto + +lemma ipoly_poly_inverse[simp]: assumes "coeff p 0 \ 0" + shows "ipoly (poly_inverse p) (x :: 'a :: field_char_0) = 0 \ ipoly p (inverse x) = 0" + unfolding poly_inverse_def ipoly_abs_int_poly_eq_zero_iff +proof (cases "x = 0") + case False + thus "(ipoly (reflect_poly p) x = 0) = (ipoly p (inverse x) = 0)" + by (subst ipoly_reflect_poly, auto) +next + case True + show "(ipoly (reflect_poly p) x = 0) = (ipoly p (inverse x) = 0)" unfolding True using assms by (auto simp: poly_0_coeff_0) +qed + +lemma ipoly_roots_finite: "p \ 0 \ finite {x :: 'a :: {idom, ring_char_0}. ipoly p x = 0}" + by (rule poly_roots_finite, simp) + +lemma root_sign_change: assumes + p0: "poly (p::real poly) x = 0" and + pd_ne0: "poly (pderiv p) x \ 0" + obtains d where + "0 < d" + "sgn (poly p (x - d)) \ sgn (poly p (x + d))" + "sgn (poly p (x - d)) \ 0" + "0 \ sgn (poly p (x + d))" + "\ d' > 0. d' \ d \ sgn (poly p (x + d')) = sgn (poly p (x + d)) \ sgn (poly p (x - d')) = sgn (poly p (x - d))" +proof - + assume a:"(\d. 0 < d \ + sgn (poly p (x - d)) \ sgn (poly p (x + d)) \ + sgn (poly p (x - d)) \ 0 \ + 0 \ sgn (poly p (x + d)) \ + \d'>0. d' \ d \ + sgn (poly p (x + d')) = sgn (poly p (x + d)) \ sgn (poly p (x - d')) = sgn (poly p (x - d)) \ + thesis)" + from pd_ne0 consider "poly (pderiv p) x > 0" | "poly (pderiv p) x < 0" by linarith + thus ?thesis proof(cases) + case 1 + obtain d1 where d1:"\h. 0 h < d1 \ poly p (x - h) < 0" "d1 > 0" + using DERIV_pos_inc_left[OF poly_DERIV 1] p0 by auto + obtain d2 where d2:"\h. 0 h < d2 \ poly p (x + h) > 0" "d2 > 0" + using DERIV_pos_inc_right[OF poly_DERIV 1] p0 by auto + have g0:"0 < (min d1 d2) / 2" using d1 d2 by auto + hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2" by auto + { fix d + assume a1:"0 < d" and a2:"d < min d1 d2" + have "sgn (poly p (x - d)) = -1" "sgn (poly p (x + d)) = 1" + using d1(1)[OF a1] d2(1)[OF a1] a2 by auto + } note d=this + show ?thesis by(rule a[OF g0];insert d g0 m1 m2, simp) + next + case 2 + obtain d1 where d1:"\h. 0 h < d1 \ poly p (x - h) > 0" "d1 > 0" + using DERIV_neg_dec_left[OF poly_DERIV 2] p0 by auto + obtain d2 where d2:"\h. 0 h < d2 \ poly p (x + h) < 0" "d2 > 0" + using DERIV_neg_dec_right[OF poly_DERIV 2] p0 by auto + have g0:"0 < (min d1 d2) / 2" using d1 d2 by auto + hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2" by auto + { fix d + assume a1:"0 < d" and a2:"d < min d1 d2" + have "sgn (poly p (x - d)) = 1" "sgn (poly p (x + d)) = -1" + using d1(1)[OF a1] d2(1)[OF a1] a2 by auto + } note d=this + show ?thesis by(rule a[OF g0];insert d g0 m1 m2, simp) + qed +qed + + +lemma gt_rat_sign_change_square_free: + assumes ur: "\! x. root_cond plr x" + and plr[simp]: "plr = (p,l,r)" + and sf: "square_free p" and in_interval: "l \ y" "y \ r" + and py0: "ipoly p y \ 0" and pr0: "ipoly p r \ 0" + shows "(sgn (ipoly p y) = sgn (ipoly p r)) = (of_rat y > (THE x. root_cond plr x))" (is "?gt = _") +proof (rule ccontr) + define ur where "ur = (THE x. root_cond plr x)" + assume "\ ?thesis" + hence "?gt \ (real_of_rat y > ur)" unfolding ur_def by auto + note a = this[unfolded plr] + from py0 have "p \ 0" unfolding irreducible_def by auto + hence p0_real: "real_of_int_poly p \ (0::real poly)" by auto + let ?p = "real_of_int_poly p" + let ?r = real_of_rat + from in_interval have in':"?r l \ ?r y" "?r y \ ?r r" unfolding of_rat_less_eq by auto + from sf square_free_of_int_poly[of p] square_free_rsquarefree + have rsf:"rsquarefree ?p" by auto + from ur have "root_cond plr ur" by (metis ur_def theI') + note urD = this[unfolded root_cond_def plr split] this[unfolded plr] + have ur3:"poly ?p ur = 0" using urD by auto + from urD have "ur \ of_rat r" by auto + moreover + from pr0 have "ipoly p (real_of_rat r) \ 0" by auto + with ur3 have "real_of_rat r \ ur" by force + ultimately have "ur < ?r r" by auto + hence ur2: "0 < ?r r - ur" by linarith + from rsquarefree_roots rsf ur3 + have pd_nonz:"poly (pderiv ?p) ur \ 0" by auto + obtain d where d':"\d'. d'>0 \ d' \ d \ + sgn (poly ?p (ur + d')) = sgn (poly ?p (ur + d)) \ + sgn (poly ?p (ur - d')) = sgn (poly ?p (ur - d))" + "sgn (poly ?p (ur - d)) \ sgn (poly ?p (ur + d))" + "sgn (poly ?p (ur + d)) \ 0" + and d_ge_0:"d > 0" + by (metis root_sign_change[OF ur3 pd_nonz]) + have sr:"sgn (poly ?p (ur + d)) = sgn (poly ?p (?r r))" + proof (cases "?r r - ur \ d") + case True show ?thesis using d'(1)[OF ur2 True] by auto + next + case False hence less:"ur + d < ?r r" by auto + show ?thesis + proof(rule no_roots_inbetween_imp_same_sign[OF less,rule_format],goal_cases) + case (1 x) + from ur 1 d_ge_0 have ran: "real_of_rat l \ x" "x \ real_of_rat r" using urD by auto + from 1 d_ge_0 have "ur \ x" by auto + with ur urD have "\ root_cond (p,l,r) x" by (auto simp: root_cond_def) + with ran show ?case by (auto simp: root_cond_def) + qed + qed + consider "?r l < ur - d" "?r l < ur" | "0 < ur - ?r l" "ur - ?r l \ d" | "ur = ?r l" + using urD by argo + hence sl:"sgn (poly ?p (ur - d)) = sgn (poly ?p (?r l)) \ 0 = sgn (poly ?p (?r l))" + proof (cases) + case 1 + have "sgn (poly ?p (?r l)) = sgn (poly ?p (ur - d))" + proof(rule no_roots_inbetween_imp_same_sign[OF 1(1),rule_format],goal_cases) + case (1 x) + from ur 1 d_ge_0 urD have ran: "real_of_rat l \ x" "x \ real_of_rat r" by auto + from 1 d_ge_0 have "ur \ x" by auto + with ur urD have "\ root_cond (p,l,r) x" by (auto simp: root_cond_def) + with ran show ?case by (auto simp: root_cond_def) + qed + thus ?thesis by auto + next + case 2 show ?thesis using d'(1)[OF 2] by simp + qed (insert ur3,simp) + have diff_sign: "sgn (ipoly p l) \ sgn (ipoly p r)" + using d'(2-) sr sl real_of_rat_sgn by auto + have ur':"\x. real_of_rat l \ x \ x \ real_of_rat y \ ipoly p x = 0 \ \ (?r y \ ur)" + proof(standard+,goal_cases) + case (1 x) + { + assume id: "ur = ?r y" + with urD ur py0 have False by auto + } note neq = this + have x: "root_cond (p, l, r) x" unfolding root_cond_def + using 1 a ur urD by auto + from ur urD x have ur_eqI: "ur = x" + by auto + with 1 have "ur = of_rat y" by auto + with urD(1) py0 show False by auto + qed + hence ur'':"\x. real_of_rat y \ x \ x \ real_of_rat r \ poly (real_of_int_poly p) x \ 0 \ \ (?r y \ ur)" + using urD by auto + have "(sgn (ipoly p y) = sgn (ipoly p r)) = (?r y > ur)" + proof(cases "sgn (ipoly p r) = sgn (ipoly p y)") + case True + have sgn:"sgn (poly ?p (real_of_rat l)) \ sgn (poly ?p (real_of_rat y))" using True diff_sign + by (simp add: real_of_rat_sgn) + have ly:"of_rat l < (of_rat y::real)" using in_interval True diff_sign less_eq_rat_def of_rat_less by auto + with no_roots_inbetween_imp_same_sign[OF ly,of ?p] sgn ur' True + show ?thesis by force + next + case False + hence ne:"sgn (ipoly p (real_of_rat y)) \ sgn (ipoly p (real_of_rat r))" by (simp add: real_of_rat_sgn) + have ry:"of_rat y < (of_rat r::real)" using in_interval False diff_sign less_eq_rat_def of_rat_less by auto + obtain x where x:"real_of_rat y \ x" "x \ real_of_rat r" "ipoly p x = 0" + using no_roots_inbetween_imp_same_sign[OF ry,of ?p] ne by auto + hence lx:"real_of_rat l \ x" using in_interval + using False a urD by auto + with x have "root_cond (p,l,r) x" by (auto simp: root_cond_def) + with urD ur + have "ur = x" by auto + then show ?thesis using False x by auto + qed + thus False using diff_sign(1) a py0 by(cases "ipoly p r = 0";auto simp:sgn_0_0) +qed + +definition algebraic_real :: "real \ bool" where + [simp]: "algebraic_real = algebraic" + +lemma algebraic_real_iff[code_unfold]: "algebraic = algebraic_real" by simp + +end diff --git a/thys/Algebraic_Numbers/Cauchy_Root_Bound.thy b/thys/Algebraic_Numbers/Cauchy_Root_Bound.thy new file mode 100644 --- /dev/null +++ b/thys/Algebraic_Numbers/Cauchy_Root_Bound.thy @@ -0,0 +1,185 @@ +(* + Author: René Thiemann + Akihisa Yamada + License: BSD +*) +section \Cauchy's Root Bound\ + +text \This theory contains a formalization of Cauchy's root bound, i.e., + given an integer polynomial it determines a bound \b\ such that all real or complex + roots of the polynomials have a norm below \b\.\ + +theory Cauchy_Root_Bound +imports + Algebraic_Numbers_Pre_Impl +begin + +hide_const (open) UnivPoly.coeff +hide_const (open) Module.smult + +text \Division of integers, rounding to the upper value.\ +definition div_ceiling :: "int \ int \ int" where + "div_ceiling x y = (let q = x div y in if q * y = x then q else q + 1)" + +definition root_bound :: "int poly \ rat" where + "root_bound p \ let + n = degree p; + m = 1 + div_ceiling (max_list_non_empty (map (\i. abs (coeff p i)) [0.. \round to the next higher number \2^n\, so that bisection will\ + \ \stay on integers for as long as possible\ + in of_int (2 ^ (log_ceiling 2 m))" + + +lemma root_imp_deg_nonzero: assumes "p \ 0" "poly p x = 0" + shows "degree p \ 0" +proof + assume "degree p = 0" + from degree0_coeffs[OF this] assms show False by auto +qed + +lemma cauchy_root_bound: fixes x :: "'a :: real_normed_field" + assumes x: "poly p x = 0" and p: "p \ 0" + shows "norm x \ 1 + max_list_non_empty (map (\ i. norm (coeff p i)) [0 ..< degree p]) + / norm (lead_coeff p)" (is "_ \ _ + ?max / ?nlc") +proof - + let ?n = "degree p" + let ?p = "coeff p" + let ?lc = "lead_coeff p" + define ml where "ml = ?max / ?nlc" + from p have lc: "?lc \ 0" by auto + hence nlc: "norm ?lc > 0" by auto + from root_imp_deg_nonzero[OF p x] have *: "0 \ set [0 ..< degree p]" by auto + have "0 \ norm (?p 0)" by simp + also have "\ \ ?max" + by (rule max_list_non_empty, insert *, auto) + finally have max0: "?max \ 0" . + with nlc have ml0: "ml \ 0" unfolding ml_def by auto + hence easy: "norm x \ 1 \ ?thesis" unfolding ml_def[symmetric] by auto + show ?thesis + proof (cases "norm x \ 1") + case True + thus ?thesis using easy by auto + next + case False + hence nx: "norm x > 1" by simp + hence x0: "x \ 0" by auto + hence xn0: "0 < norm x ^ ?n" by auto + from x[unfolded poly_altdef] have "x ^ ?n * ?lc = x ^ ?n * ?lc - (\i\?n. x ^ i * ?p i)" + unfolding poly_altdef by (simp add: ac_simps) + also have "(\i\?n. x ^ i * ?p i) = x ^ ?n * ?lc + (\i < ?n. x ^ i * ?p i)" + by (subst sum.remove[of _ ?n], auto intro: sum.cong) + finally have "x ^ ?n * ?lc = - (\i < ?n. x ^ i * ?p i)" by simp + with lc have "x ^ ?n = - (\i < ?n. x ^ i * ?p i) / ?lc" by (simp add: field_simps) + from arg_cong[OF this, of norm] + have "norm x ^ ?n = norm ((\i < ?n. x ^ i * ?p i) / ?lc)" unfolding norm_power by simp + also have "(\i < ?n. x ^ i * ?p i) / ?lc = (\i < ?n. x ^ i * ?p i / ?lc)" + by (rule sum_divide_distrib) + also have "norm \ \ (\i < ?n. norm (x ^ i * (?p i / ?lc)))" + by (simp add: field_simps, rule norm_sum) + also have "\ = (\i < ?n. norm x ^ i * norm (?p i / ?lc))" + unfolding norm_mult norm_power .. + also have "\ \ (\i < ?n. norm x ^ i * ml)" + proof (rule sum_mono) + fix i + assume "i \ {.. norm x ^ i * ml" + proof (rule mult_left_mono) + show "0 \ norm x ^ i" using nx by auto + show "norm (?p i / ?lc) \ ml" unfolding norm_divide ml_def + by (rule divide_right_mono[OF max_list_non_empty], insert nlc i, auto) + qed + qed + also have "\ = ml * (\i < ?n. norm x ^ i)" + unfolding sum_distrib_right[symmetric] by simp + also have "(\i < ?n. norm x ^ i) = (norm x ^ ?n - 1) / (norm x - 1)" + by (rule geometric_sum, insert nx, auto) + finally have "norm x ^ ?n \ ml * (norm x ^ ?n - 1) / (norm x - 1)" by simp + from mult_left_mono[OF this, of "norm x - 1"] + have "(norm x - 1) * (norm x ^ ?n) \ ml * (norm x ^ ?n - 1)" using nx by auto + also have "\ = (ml * (1 - 1 / (norm x ^ ?n))) * norm x ^ ?n" + using nx False x0 by (simp add: field_simps) + finally have "(norm x - 1) * (norm x ^ ?n) \ (ml * (1 - 1 / (norm x ^ ?n))) * norm x ^ ?n" . + from mult_right_le_imp_le[OF this xn0] + have "norm x - 1 \ ml * (1 - 1 / (norm x ^ ?n))" by simp + hence "norm x \ 1 + ml - ml / (norm x ^ ?n)" by (simp add: field_simps) + also have "\ \ 1 + ml" using ml0 xn0 by auto + finally show ?thesis unfolding ml_def . + qed +qed + +lemma div_le_div_ceiling: "x div y \ div_ceiling x y" + unfolding div_ceiling_def Let_def by auto + +lemma div_ceiling: assumes q: "q \ 0" + shows "(of_int x :: 'a :: floor_ceiling) / of_int q \ of_int (div_ceiling x q)" +proof (cases "q dvd x") + case True + then obtain k where xqk: "x = q * k" unfolding dvd_def by auto + hence id: "div_ceiling x q = k" unfolding div_ceiling_def Let_def using q by auto + show ?thesis unfolding id unfolding xqk using q by simp +next + case False + { + assume "x div q * q = x" + hence "x = q * (x div q)" by (simp add: ac_simps) + hence "q dvd x" unfolding dvd_def by auto + with False have False by simp + } + hence id: "div_ceiling x q = x div q + 1" + unfolding div_ceiling_def Let_def using q by auto + show ?thesis unfolding id + by (metis floor_divide_of_int_eq le_less add1_zle_eq floor_less_iff) +qed + +lemma max_list_non_empty_map: assumes hom: "\ x y. max (f x) (f y) = f (max x y)" + shows "xs \ [] \ max_list_non_empty (map f xs) = f (max_list_non_empty xs)" + by (induct xs rule: max_list_non_empty.induct, auto simp: hom) + +lemma root_bound: assumes "root_bound p = B" and deg: "degree p > 0" + shows "ipoly p (x :: 'a :: real_normed_field) = 0 \ norm x \ of_rat B" "B \ 0" +proof - + let ?r = "of_rat :: _ \ 'a" + let ?i = "of_int :: _ \ 'a" + let ?p = "map_poly ?i p" + define n where "n = degree p" + let ?lc = "coeff p n" + let ?list = "map (\i. abs (coeff p i)) [0.. 0" by auto + from p0 have alc0: "abs ?lc \ 0" unfolding n_def by auto + from deg have mem: "abs (coeff p 0) \ set ?list" unfolding n_def by auto + from max_list_non_empty[OF this, folded m_def] + have m0: "m \ 0" by auto + have "div_ceiling m (abs ?lc) \ 0" + by (rule order_trans[OF _ div_le_div_ceiling[of m "abs ?lc"]], subst + pos_imp_zdiv_nonneg_iff, insert p0 m0, auto simp: n_def) + hence mup: "m_up \ 1" unfolding m_up_def by auto + have "m_up \ 2 ^ (log_ceiling 2 m_up)" using mup log_ceiling_sound(1) by auto + hence Cmup: "C \ of_int m_up" unfolding C_def by linarith + with mup have C: "C \ 1" by auto + from assms(1)[unfolded root_bound_def Let_def] + have B: "C = B" unfolding C_def m_up_def n_def m_def by auto + note dc = div_le_div_ceiling[of m "abs ?lc"] + with C show "B \ 0" unfolding B by auto + assume "ipoly p x = 0" + hence rt: "poly ?p x = 0" by simp + from root_imp_deg_nonzero[OF _ this] p0 have n0: "n \ 0" unfolding n_def by auto + from cauchy_root_bound[OF rt] p0 + have "norm x \ 1 + max_list_non_empty ?list' / real_of_int (abs ?lc)" + by (simp add: n_def) + also have "?list' = map real_of_int ?list" by simp + also have "max_list_non_empty \ = real_of_int m" unfolding m_def + by (rule max_list_non_empty_map, insert mem, auto) + also have "1 + m / real_of_int (abs ?lc) \ real_of_int m_up" + unfolding m_up_def using div_ceiling[OF alc0, of m] by auto + also have "\ \ real_of_rat C" using Cmup using of_rat_less_eq by force + finally have "norm x \ real_of_rat C" . + thus "norm x \ real_of_rat B" unfolding B by simp +qed + +end diff --git a/thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy b/thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy --- a/thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy +++ b/thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy @@ -1,3647 +1,3411 @@ (* Author: Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section \Real Algebraic Numbers\ text \Whereas we previously only proved the closure properties of algebraic numbers, this theory adds the numeric computations that are required to separate the roots, and to pick unique representatives of algebraic numbers. The development is split into three major parts. First, an ambiguous representation of algebraic numbers is used, afterwards another layer is used with special treatment of rational numbers which still does not admit unique representatives, and finally, a quotient type is created modulo the equivalence. The theory also contains a code-setup to implement real numbers via real algebraic numbers.\ text \The results are taken from the textbook \cite[pages 329ff]{AlgNumbers}.\ theory Real_Algebraic_Numbers imports - "Abstract-Rewriting.SN_Order_Carrier" - Deriving.Compare_Rat - Deriving.Compare_Real - Jordan_Normal_Form.Gauss_Jordan_IArray_Impl - Algebraic_Numbers - Sturm_Rat - Factors_of_Int_Poly - Min_Int_Poly + Algebraic_Numbers_Pre_Impl begin -text \For algebraic numbers, it turned out that @{const gcd_int_poly} is not - preferable to the default implementation of @{const gcd}, which just implements - Collin's primitive remainder sequence.\ -declare gcd_int_poly_code[code_unfold del] - (*TODO: move *) lemma ex1_imp_Collect_singleton: "(\!x. P x) \ P x \ Collect P = {x}" proof(intro iffI conjI, unfold conj_imp_eq_imp_imp) assume "Ex1 P" "P x" then show "Collect P = {x}" by blast next assume Px: "Collect P = {x}" then have "P y \ x = y" for y by auto then show "Ex1 P" by auto from Px show "P x" by auto qed lemma ex1_Collect_singleton[consumes 2]: assumes "\!x. P x" and "P x" and "Collect P = {x} \ thesis" shows thesis by (rule assms(3), subst ex1_imp_Collect_singleton[symmetric], insert assms(1,2), auto) lemma ex1_iff_Collect_singleton: "P x \ (\!x. P x) \ Collect P = {x}" by (subst ex1_imp_Collect_singleton[symmetric], auto) -context - fixes f - assumes bij: "bij f" -begin -lemma bij_imp_ex1_iff: "(\!x. P (f x)) \ (\!y. P y)" (is "?l = ?r") -proof (intro iffI) - assume l: ?l - then obtain x where "P (f x)" by auto - with l have *: "{x} = Collect (P o f)" by auto - also have "f ` \ = {y. P (f (Hilbert_Choice.inv f y))}" using bij_image_Collect_eq[OF bij] by auto - also have "\ = {y. P y}" - proof- - have "f (Hilbert_Choice.inv f y) = y" for y by (meson bij bij_inv_eq_iff) - then show ?thesis by simp - qed - finally have "Collect P = {f x}" by auto - then show ?r by (fold ex1_imp_Collect_singleton, auto) -next - assume r: ?r - then obtain y where "P y" by auto - with r have "{y} = Collect P" by auto - also have "Hilbert_Choice.inv f ` \ = Collect (P \ f)" - using bij_image_Collect_eq[OF bij_imp_bij_inv[OF bij]] bij by (auto simp: inv_inv_eq) - finally have "Collect (P o f) = {Hilbert_Choice.inv f y}" by (simp add: o_def) - then show ?l by (fold ex1_imp_Collect_singleton, auto) -qed - -lemma bij_ex1_imp_the_shift: - assumes ex1: "\!y. P y" shows "(THE x. P (f x)) = Hilbert_Choice.inv f (THE y. P y)" (is "?l = ?r") -proof- - from ex1 have "P (THE y. P y)" by (rule the1I2) - moreover from ex1[folded bij_imp_ex1_iff] have "P (f (THE x. P (f x)))" by (rule the1I2) - ultimately have "(THE y. P y) = f (THE x. P (f x))" using ex1 by auto - also have "Hilbert_Choice.inv f \ = (THE x. P (f x))" using bij by (simp add: bij_is_inj) - finally show "?l = ?r" by auto -qed - -lemma bij_imp_Collect_image: "{x. P (f x)} = Hilbert_Choice.inv f ` {y. P y}" (is "?l = ?g ` _") -proof- - have "?l = ?g ` f ` ?l" by (simp add: image_comp inv_o_cancel[OF bij_is_inj[OF bij]]) - also have "f ` ?l = {f x | x. P (f x)}" by auto - also have "\ = {y. P y}" by (metis bij bij_iff) - finally show ?thesis. -qed - -lemma bij_imp_card_image: "card (f ` X) = card X" - by (metis bij bij_iff card.infinite finite_imageD inj_onI inj_on_iff_eq_card) - -end - lemma bij_imp_card: assumes bij: "bij f" shows "card {x. P (f x)} = card {x. P x}" unfolding bij_imp_Collect_image[OF bij] bij_imp_card_image[OF bij_imp_bij_inv[OF bij]].. lemma bij_add: "bij (\x. x + y :: 'a :: group_add)" (is ?g1) and bij_minus: "bij (\x. x - y :: 'a)" (is ?g2) and inv_add[simp]: "Hilbert_Choice.inv (\x. x + y) = (\x. x - y)" (is ?g3) and inv_minus[simp]: "Hilbert_Choice.inv (\x. x - y) = (\x. x + y)" (is ?g4) proof- have 1: "(\x. x - y) \ (\x. x + y) = id" and 2: "(\x. x + y) \ (\x. x - y) = id" by auto from o_bij[OF 1 2] show ?g1. from o_bij[OF 2 1] show ?g2. from inv_unique_comp[OF 2 1] show ?g3. from inv_unique_comp[OF 1 2] show ?g4. qed lemmas ex1_shift[simp] = bij_imp_ex1_iff[OF bij_add] bij_imp_ex1_iff[OF bij_minus] lemma ex1_the_shift: assumes ex1: "\!y :: 'a :: group_add. P y" shows "(THE x. P (x + d)) = (THE y. P y) - d" and "(THE x. P (x - d)) = (THE y. P y) + d" unfolding bij_ex1_imp_the_shift[OF bij_add ex1] bij_ex1_imp_the_shift[OF bij_minus ex1] by auto lemma card_shift_image[simp]: shows "card ((\x :: 'a :: group_add. x + d) ` X) = card X" and "card ((\x. x - d) ` X) = card X" by (auto simp: bij_imp_card_image[OF bij_add] bij_imp_card_image[OF bij_minus]) lemma irreducible_root_free: fixes p :: "'a :: {idom,comm_ring_1} poly" assumes irr: "irreducible p" shows "root_free p" proof (cases "degree p" "1::nat" rule: linorder_cases) case greater { fix x assume "poly p x = 0" hence "[:-x,1:] dvd p" using poly_eq_0_iff_dvd by blast then obtain r where p: "p = r * [:-x,1:]" by (elim dvdE, auto) have deg: "degree [:-x,1:] = 1" by simp have dvd: "\ [:-x,1:] dvd 1" by (auto simp: poly_dvd_1) from greater have "degree r \ 0" using degree_mult_le[of r "[:-x,1:]", unfolded deg, folded p] by auto then have "\ r dvd 1" by (auto simp: poly_dvd_1) with p irr irreducibleD[OF irr p] dvd have False by auto } thus ?thesis unfolding root_free_def by auto next case less then have deg: "degree p = 0" by auto from deg obtain p0 where p: "p = [:p0:]" using degree0_coeffs by auto with irr have "p \ 0" by auto with p have "poly p x \ 0" for x by auto thus ?thesis by (auto simp: root_free_def) qed (auto simp: root_free_def) (* **************************************************************** *) subsection \Real Algebraic Numbers -- Innermost Layer\ text \We represent a real algebraic number \\\ by a tuple (p,l,r): \\\ is the unique root in the interval [l,r] and l and r have the same sign. We always assume that p is normalized, i.e., p is the unique irreducible and positive content-free polynomial which represents the algebraic number. This representation clearly admits duplicate representations for the same number, e.g. (...,x-3, 3,3) is equivalent to (...,x-3,2,10).\ subsubsection \Basic Definitions\ type_synonym real_alg_1 = "int poly \ rat \ rat" fun poly_real_alg_1 :: "real_alg_1 \ int poly" where "poly_real_alg_1 (p,_,_) = p" fun rai_ub :: "real_alg_1 \ rat" where "rai_ub (_,_,r) = r" fun rai_lb :: "real_alg_1 \ rat" where "rai_lb (_,l,_) = l" abbreviation "roots_below p x \ {y :: real. y \ x \ ipoly p y = 0}" abbreviation(input) unique_root :: "real_alg_1 \ bool" where "unique_root plr \ (\! x. root_cond plr x)" abbreviation the_unique_root :: "real_alg_1 \ real" where "the_unique_root plr \ (THE x. root_cond plr x)" abbreviation real_of_1 where "real_of_1 \ the_unique_root" lemma root_condI[intro]: assumes "of_rat (rai_lb plr) \ x" and "x \ of_rat (rai_ub plr)" and "ipoly (poly_real_alg_1 plr) x = 0" shows "root_cond plr x" using assms by (auto simp: root_cond_def) lemma root_condE[elim]: assumes "root_cond plr x" and "of_rat (rai_lb plr) \ x \ x \ of_rat (rai_ub plr) \ ipoly (poly_real_alg_1 plr) x = 0 \ thesis" shows thesis using assms by (auto simp: root_cond_def) lemma assumes ur: "unique_root plr" defines "x \ the_unique_root plr" and "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" shows unique_rootD: "of_rat l \ x" "x \ of_rat r" "ipoly p x = 0" "root_cond plr x" "x = y \ root_cond plr y" "y = x \ root_cond plr y" and the_unique_root_eqI: "root_cond plr y \ y = x" "root_cond plr y \ x = y" proof - from ur show x: "root_cond plr x" unfolding x_def by (rule theI') have "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def) from x[unfolded this] show "of_rat l \ x" "x \ of_rat r" "ipoly p x = 0" by auto from x ur show "root_cond plr y \ y = x" and "root_cond plr y \ x = y" and "x = y \ root_cond plr y" and "y = x \ root_cond plr y" by auto qed lemma unique_rootE: assumes ur: "unique_root plr" defines "x \ the_unique_root plr" and "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes main: "of_rat l \ x \ x \ of_rat r \ ipoly p x = 0 \ root_cond plr x \ (\y. x = y \ root_cond plr y) \ (\y. y = x \ root_cond plr y) \ thesis" shows thesis by (rule main, unfold x_def p_def l_def r_def; rule unique_rootD[OF ur]) lemma unique_rootI: assumes "\ y. root_cond plr y \ x = y" "root_cond plr x" shows "unique_root plr" using assms by blast -definition poly_cond :: "int poly \ bool" where - "poly_cond p = (lead_coeff p > 0 \ irreducible p)" - -lemma poly_condI[intro]: - assumes "lead_coeff p > 0" and "irreducible p" shows "poly_cond p" using assms by (auto simp: poly_cond_def) - -lemma poly_condD: - assumes "poly_cond p" - shows "irreducible p" and "lead_coeff p > 0" and "root_free p" and "square_free p" and "p \ 0" - using assms unfolding poly_cond_def using irreducible_root_free irreducible_imp_square_free cf_pos_def by auto - -lemma poly_condE[elim]: - assumes "poly_cond p" - and "irreducible p \ lead_coeff p > 0 \ root_free p \ square_free p \ p \ 0 \ thesis" - shows thesis - using assms by (auto dest:poly_condD) - definition invariant_1 :: "real_alg_1 \ bool" where "invariant_1 tup \ case tup of (p,l,r) \ unique_root (p,l,r) \ sgn l = sgn r \ poly_cond p" lemma invariant_1I: assumes "unique_root plr" and "sgn (rai_lb plr) = sgn (rai_ub plr)" and "poly_cond (poly_real_alg_1 plr)" shows "invariant_1 plr" using assms by (auto simp: invariant_1_def) lemma assumes "invariant_1 plr" defines "x \ the_unique_root plr" and "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" shows invariant_1D: "root_cond plr x" "sgn l = sgn r" "sgn x = of_rat (sgn r)" "unique_root plr" "poly_cond p" "degree p > 0" "primitive p" and invariant_1_root_cond: "\ y. root_cond plr y \ y = x" proof - let ?l = "of_rat l :: real" let ?r = "of_rat r :: real" have plr: "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def) from assms show ur: "unique_root plr" and sgn: "sgn l = sgn r" and pc: "poly_cond p" by (auto simp: invariant_1_def) from ur show rc: "root_cond plr x" by (auto simp add: x_def plr intro: theI') from this[unfolded plr] have x: "ipoly p x = 0" and bnd: "?l \ x" "x \ ?r" by auto show "sgn x = of_rat (sgn r)" proof (cases "0::real" "x" rule:linorder_cases) case less with bnd(2) have "0 < ?r" by arith thus ?thesis using less by simp next case equal with bnd have "?l \ 0" "?r \ 0" by auto hence "l \ 0" "r \ 0" by auto with \sgn l = sgn r\ have "l = 0" "r = 0" unfolding sgn_rat_def by (auto split: if_splits) with rc[unfolded plr] show ?thesis by auto next case greater with bnd(1) have "?l < 0" by arith thus ?thesis unfolding \sgn l = sgn r\[symmetric] using greater by simp qed from the_unique_root_eqI[OF ur] rc show "\ y. root_cond plr y \ y = x" by metis { assume "degree p = 0" with poly_zero[OF x, simplified] sgn bnd have "p = 0" by auto with pc have "False" by auto } then show "degree p > 0" by auto with pc show "primitive p" by (intro irreducible_imp_primitive, auto) qed lemma invariant_1E[elim]: assumes "invariant_1 plr" defines "x \ the_unique_root plr" and "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes main: "root_cond plr x \ sgn l = sgn r \ sgn x = of_rat (sgn r) \ unique_root plr \ poly_cond p \ degree p > 0 \ primitive p \ thesis" shows thesis apply (rule main) using assms(1) unfolding x_def p_def l_def r_def by (auto dest: invariant_1D) lemma invariant_1_realI: fixes plr :: real_alg_1 defines "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes x: "root_cond plr x" and "sgn l = sgn r" and ur: "unique_root plr" and "poly_cond p" shows "invariant_1 plr \ real_of_1 plr = x" using the_unique_root_eqI[OF ur x] assms by (cases plr, auto intro: invariant_1I) lemma real_of_1_0: assumes "invariant_1 (p,l,r)" shows [simp]: "the_unique_root (p,l,r) = 0 \ r = 0" and [dest]: "l = 0 \ r = 0" and [intro]: "r = 0 \ l = 0" using assms by (auto simp: sgn_0_0) lemma invariant_1_pos: assumes rc: "invariant_1 (p,l,r)" shows [simp]:"the_unique_root (p,l,r) > 0 \ r > 0" (is "?x > 0 \ _") and [simp]:"the_unique_root (p,l,r) < 0 \ r < 0" and [simp]:"the_unique_root (p,l,r) \ 0 \ r \ 0" and [simp]:"the_unique_root (p,l,r) \ 0 \ r \ 0" and [intro]: "r > 0 \ l > 0" and [dest]: "l > 0 \ r > 0" and [intro]: "r < 0 \ l < 0" and [dest]: "l < 0 \ r < 0" proof(atomize(full),goal_cases) case 1 let ?r = "real_of_rat" from assms[unfolded invariant_1_def] have ur: "unique_root (p,l,r)" and sgn: "sgn l = sgn r" by auto from unique_rootD(1-2)[OF ur] have le: "?r l \ ?x" "?x \ ?r r" by auto from rc show ?case proof (cases r "0::rat" rule:linorder_cases) case greater with sgn have "sgn l = 1" by simp hence l0: "l > 0" by (auto simp: sgn_1_pos) hence "?r l > 0" by auto hence "?x > 0" using le(1) by arith with greater l0 show ?thesis by auto next case equal with real_of_1_0[OF rc] show ?thesis by auto next case less hence "?r r < 0" by auto with le(2) have "?x < 0" by arith with less sgn show ?thesis by (auto simp: sgn_1_neg) qed qed definition invariant_1_2 where "invariant_1_2 rai \ invariant_1 rai \ degree (poly_real_alg_1 rai) > 1" definition poly_cond2 where "poly_cond2 p \ poly_cond p \ degree p > 1" lemma poly_cond2I[intro!]: "poly_cond p \ degree p > 1 \ poly_cond2 p" by (simp add: poly_cond2_def) lemma poly_cond2D: assumes "poly_cond2 p" shows "poly_cond p" and "degree p > 1" using assms by (auto simp: poly_cond2_def) lemma poly_cond2E[elim!]: assumes "poly_cond2 p" and "poly_cond p \ degree p > 1 \ thesis" shows thesis using assms by (auto simp: poly_cond2_def) lemma invariant_1_2_poly_cond2: "invariant_1_2 rai \ poly_cond2 (poly_real_alg_1 rai)" unfolding invariant_1_def invariant_1_2_def poly_cond2_def by auto lemma invariant_1_2I[intro!]: assumes "invariant_1 rai" and "degree (poly_real_alg_1 rai) > 1" shows "invariant_1_2 rai" using assms by (auto simp: invariant_1_2_def) lemma invariant_1_2E[elim!]: assumes "invariant_1_2 rai" and "invariant_1 rai \ degree (poly_real_alg_1 rai) > 1 \ thesis" shows thesis using assms[unfolded invariant_1_2_def] by auto lemma invariant_1_2_realI: fixes plr :: real_alg_1 defines "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes x: "root_cond plr x" and sgn: "sgn l = sgn r" and ur: "unique_root plr" and p: "poly_cond2 p" shows "invariant_1_2 plr \ real_of_1 plr = x" using invariant_1_realI[OF x] p sgn ur unfolding p_def l_def r_def by auto subsection \Real Algebraic Numbers = Rational + Irrational Real Algebraic Numbers\ text \In the next representation of real algebraic numbers, we distinguish between rational and irrational numbers. The advantage is that whenever we only work on rational numbers, there is not much overhead involved in comparison to the existing implementation of real numbers which just supports the rational numbers. For irrational numbers we additionally store the number of the root, counting from left to right. For instance $-\sqrt{2}$ and $\sqrt{2}$ would be root number 1 and 2 of $x^2 - 2$.\ subsubsection \Definitions and Algorithms on Raw Type\ datatype real_alg_2 = Rational rat | Irrational nat real_alg_1 fun invariant_2 :: "real_alg_2 \ bool" where "invariant_2 (Irrational n rai) = (invariant_1_2 rai \ n = card(roots_below (poly_real_alg_1 rai) (real_of_1 rai)))" | "invariant_2 (Rational r) = True" fun real_of_2 :: "real_alg_2 \ real" where "real_of_2 (Rational r) = of_rat r" | "real_of_2 (Irrational n rai) = real_of_1 rai" definition of_rat_2 :: "rat \ real_alg_2" where [code_unfold]: "of_rat_2 = Rational" lemma of_rat_2: "real_of_2 (of_rat_2 x) = of_rat x" "invariant_2 (of_rat_2 x)" by (auto simp: of_rat_2_def) (* Invariant type *) typedef real_alg_3 = "Collect invariant_2" morphisms rep_real_alg_3 Real_Alg_Invariant by (rule exI[of _ "Rational 0"], auto) setup_lifting type_definition_real_alg_3 lift_definition real_of_3 :: "real_alg_3 \ real" is real_of_2 . (* *************** *) subsubsection \Definitions and Algorithms on Quotient Type\ quotient_type real_alg = real_alg_3 / "\ x y. real_of_3 x = real_of_3 y" morphisms rep_real_alg Real_Alg_Quotient by (auto simp: equivp_def) metis (* real_of *) lift_definition real_of :: "real_alg \ real" is real_of_3 . lemma real_of_inj: "(real_of x = real_of y) = (x = y)" by (transfer, simp) (* ********************** *) subsubsection \Sign\ definition sgn_1 :: "real_alg_1 \ rat" where "sgn_1 x = sgn (rai_ub x)" lemma sgn_1: "invariant_1 x \ real_of_rat (sgn_1 x) = sgn (real_of_1 x)" unfolding sgn_1_def by auto lemma sgn_1_inj: "invariant_1 x \ invariant_1 y \ real_of_1 x = real_of_1 y \ sgn_1 x = sgn_1 y" by (auto simp: sgn_1_def elim!: invariant_1E) (* ********************** *) subsubsection \Normalization: Bounds Close Together\ lemma unique_root_lr: assumes ur: "unique_root plr" shows "rai_lb plr \ rai_ub plr" (is "?l \ ?r") proof - let ?p = "poly_real_alg_1 plr" from ur[unfolded root_cond_def] have ex1: "\! x :: real. of_rat ?l \ x \ x \ of_rat ?r \ ipoly ?p x = 0" by (cases plr, simp) then obtain x :: real where bnd: "of_rat ?l \ x" "x \ of_rat ?r" and rt: "ipoly ?p x = 0" by auto from bnd have "real_of_rat ?l \ of_rat ?r" by linarith thus "?l \ ?r" by (simp add: of_rat_less_eq) qed locale map_poly_zero_hom_0 = base: zero_hom_0 begin sublocale zero_hom_0 "map_poly hom" by (unfold_locales,auto) end interpretation of_int_poly_hom: map_poly_zero_hom_0 "of_int :: int \ 'a :: {ring_1, ring_char_0}" .. -lemma ipoly_roots_finite: "p \ 0 \ finite {x :: 'a :: {idom, ring_char_0}. ipoly p x = 0}" - by (rule poly_roots_finite, simp) - lemma roots_below_the_unique_root: assumes ur: "unique_root (p,l,r)" shows "roots_below p (the_unique_root (p,l,r)) = roots_below p (of_rat r)" (is "roots_below p ?x = _") proof- from ur have rc: "root_cond (p,l,r) ?x" by (auto dest!: unique_rootD) with ur have x: "{x. root_cond (p,l,r) x} = {?x}" by (auto intro: the_unique_root_eqI) from rc have "?x \ {y. ?x \ y \ y \ of_rat r \ ipoly p y = 0}" by auto with rc have l1x: "... = {?x}" by (intro equalityI, fold x(1), force, simp add: x) have rb:"roots_below p (of_rat r) = roots_below p ?x \ {y. ?x < y \ y \ of_rat r \ ipoly p y = 0}" using rc by auto have emp: "\x. the_unique_root (p, l, r) < x \ x \ {ra. ?x \ ra \ ra \ real_of_rat r \ ipoly p ra = 0}" using l1x by auto with rb show ?thesis by auto qed lemma unique_root_sub_interval: assumes ur: "unique_root (p,l,r)" and rc: "root_cond (p,l',r') (the_unique_root (p,l,r))" and between: "l \ l'" "r' \ r" shows "unique_root (p,l',r')" and "the_unique_root (p,l',r') = the_unique_root (p,l,r)" proof - from between have ord: "real_of_rat l \ of_rat l'" "real_of_rat r' \ of_rat r" by (auto simp: of_rat_less_eq) from rc have lr': "real_of_rat l' \ of_rat r'" by auto with ord have lr: "real_of_rat l \ real_of_rat r" by auto show "\!x. root_cond (p, l', r') x" proof (rule, rule rc) fix y assume "root_cond (p,l',r') y" with ord have "root_cond (p,l,r) y" by (auto intro!:root_condI) from the_unique_root_eqI[OF ur this] show "y = the_unique_root (p,l,r)" by simp qed from the_unique_root_eqI[OF this rc] show "the_unique_root (p,l',r') = the_unique_root (p,l,r)" by simp qed lemma invariant_1_sub_interval: assumes rc: "invariant_1 (p,l,r)" and sub: "root_cond (p,l',r') (the_unique_root (p,l,r))" and between: "l \ l'" "r' \ r" shows "invariant_1 (p,l',r')" and "real_of_1 (p,l',r') = real_of_1 (p,l,r)" proof - let ?r = real_of_rat note rcD = invariant_1D[OF rc] from rc have ur: "unique_root (p, l', r')" and id: "the_unique_root (p, l', r') = the_unique_root (p, l, r)" by (atomize(full), intro conjI unique_root_sub_interval[OF _ sub between], auto) show "real_of_1 (p,l',r') = real_of_1 (p,l,r)" using id by simp from rcD(1)[unfolded split] have "?r l \ ?r r" by auto hence lr: "l \ r" by (auto simp: of_rat_less_eq) from unique_rootD[OF ur] have "?r l' \ ?r r'" by auto hence lr': "l' \ r'" by (auto simp: of_rat_less_eq) have "sgn l' = sgn r'" proof (cases "r" "0::rat" rule: linorder_cases) case less with lr lr' between have "l < 0" "l' < 0" "r' < 0" "r < 0" by auto thus ?thesis unfolding sgn_rat_def by auto next case equal with rcD(2) have "l = 0" using sgn_0_0 by auto with equal between lr' have "l' = 0" "r' = 0" by auto then show ?thesis by auto next case greater with rcD(4) have "sgn r = 1" unfolding sgn_rat_def by (cases "r = 0", auto) with rcD(2) have "sgn l = 1" by simp hence l: "l > 0" unfolding sgn_rat_def by (cases "l = 0"; cases "l < 0"; auto) with lr lr' between have "l > 0" "l' > 0" "r' > 0" "r > 0" by auto thus ?thesis unfolding sgn_rat_def by auto qed with between ur rc show "invariant_1 (p,l',r')" by (auto simp add: invariant_1_def id) qed -lemma root_sign_change: assumes - p0: "poly (p::real poly) x = 0" and - pd_ne0: "poly (pderiv p) x \ 0" - obtains d where - "0 < d" - "sgn (poly p (x - d)) \ sgn (poly p (x + d))" - "sgn (poly p (x - d)) \ 0" - "0 \ sgn (poly p (x + d))" - "\ d' > 0. d' \ d \ sgn (poly p (x + d')) = sgn (poly p (x + d)) \ sgn (poly p (x - d')) = sgn (poly p (x - d))" -proof - - assume a:"(\d. 0 < d \ - sgn (poly p (x - d)) \ sgn (poly p (x + d)) \ - sgn (poly p (x - d)) \ 0 \ - 0 \ sgn (poly p (x + d)) \ - \d'>0. d' \ d \ - sgn (poly p (x + d')) = sgn (poly p (x + d)) \ sgn (poly p (x - d')) = sgn (poly p (x - d)) \ - thesis)" - from pd_ne0 consider "poly (pderiv p) x > 0" | "poly (pderiv p) x < 0" by linarith - thus ?thesis proof(cases) - case 1 - obtain d1 where d1:"\h. 0 h < d1 \ poly p (x - h) < 0" "d1 > 0" - using DERIV_pos_inc_left[OF poly_DERIV 1] p0 by auto - obtain d2 where d2:"\h. 0 h < d2 \ poly p (x + h) > 0" "d2 > 0" - using DERIV_pos_inc_right[OF poly_DERIV 1] p0 by auto - have g0:"0 < (min d1 d2) / 2" using d1 d2 by auto - hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2" by auto - { fix d - assume a1:"0 < d" and a2:"d < min d1 d2" - have "sgn (poly p (x - d)) = -1" "sgn (poly p (x + d)) = 1" - using d1(1)[OF a1] d2(1)[OF a1] a2 by auto - } note d=this - show ?thesis by(rule a[OF g0];insert d g0 m1 m2, simp) - next - case 2 - obtain d1 where d1:"\h. 0 h < d1 \ poly p (x - h) > 0" "d1 > 0" - using DERIV_neg_dec_left[OF poly_DERIV 2] p0 by auto - obtain d2 where d2:"\h. 0 h < d2 \ poly p (x + h) < 0" "d2 > 0" - using DERIV_neg_dec_right[OF poly_DERIV 2] p0 by auto - have g0:"0 < (min d1 d2) / 2" using d1 d2 by auto - hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2" by auto - { fix d - assume a1:"0 < d" and a2:"d < min d1 d2" - have "sgn (poly p (x - d)) = 1" "sgn (poly p (x + d)) = -1" - using d1(1)[OF a1] d2(1)[OF a1] a2 by auto - } note d=this - show ?thesis by(rule a[OF g0];insert d g0 m1 m2, simp) - qed -qed - lemma rational_root_free_degree_iff: assumes rf: "root_free (map_poly rat_of_int p)" and rt: "ipoly p x = 0" shows "(x \ \) = (degree p = 1)" proof assume "x \ \" then obtain y where x: "x = of_rat y" (is "_ = ?x") unfolding Rats_def by blast from rt[unfolded x] have "poly (map_poly rat_of_int p) y = 0" by simp with rf show "degree p = 1" unfolding root_free_def by auto next assume "degree p = 1" from degree1_coeffs[OF this] obtain a b where p: "p = [:a,b:]" and b: "b \ 0" by auto from rt[unfolded p hom_distribs] have "of_int a + x * of_int b = 0" by auto from arg_cong[OF this, of "\ x. (x - of_int a) / of_int b"] have "x = - of_rat (of_int a) / of_rat (of_int b)" using b by auto also have "\ = of_rat (- of_int a / of_int b)" unfolding of_rat_minus of_rat_divide .. finally show "x \ \" by auto qed lemma rational_poly_cond_iff: assumes "poly_cond p" and "ipoly p x = 0" and "degree p > 1" shows "(x \ \) = (degree p = 1)" proof (rule rational_root_free_degree_iff[OF _ assms(2)]) from poly_condD[OF assms(1)] irreducible_connect_rev[of p] assms(3) have p: "irreducible\<^sub>d p" by auto from irreducible\<^sub>d_int_rat[OF this] have "irreducible (map_poly rat_of_int p)" by simp thus "root_free (map_poly rat_of_int p)" by (rule irreducible_root_free) qed lemma poly_cond_degree_gt_1: assumes "poly_cond p" "degree p > 1" "ipoly p x = 0" shows "x \ \" using rational_poly_cond_iff[OF assms(1,3)] assms(2) by simp lemma poly_cond2_no_rat_root: assumes "poly_cond2 p" shows "ipoly p (real_of_rat x) \ 0" using poly_cond_degree_gt_1[of p "real_of_rat x"] assms by auto context fixes p :: "int poly" and x :: "rat" begin -lemma gt_rat_sign_change_square_free: - assumes ur: "unique_root plr" - defines "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" - assumes sf: "square_free p" and in_interval: "l \ y" "y \ r" - and py0: "ipoly p y \ 0" and pr0: "ipoly p r \ 0" -shows "(sgn (ipoly p y) = sgn (ipoly p r)) = (of_rat y > the_unique_root plr)" (is "?gt = _") -proof (rule ccontr) - have plr[simp]: "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def) - assume "?gt \ (real_of_rat y > the_unique_root plr)" - note a = this[unfolded plr] - from py0 have "p \ 0" unfolding irreducible_def by auto - hence p0_real: "real_of_int_poly p \ (0::real poly)" by auto - let ?p = "real_of_int_poly p" - note urD = unique_rootD[OF ur, simplified] - let ?ur = "the_unique_root (p, l, r)" - let ?r = real_of_rat - from in_interval have in':"?r l \ ?r y" "?r y \ ?r r" unfolding of_rat_less_eq by auto - from sf square_free_of_int_poly[of p] square_free_rsquarefree - have rsf:"rsquarefree ?p" by auto - have ur3:"poly ?p ?ur = 0" using urD(3) by simp - from ur have "?ur \ of_rat r" by (auto elim!: unique_rootE) - moreover - from pr0 have "ipoly p (real_of_rat r) \ 0" by auto - with ur3 have "real_of_rat r \ real_of_1 (p,l,r)" by force - ultimately have "?ur < ?r r" by auto - hence ur2: "0 < ?r r - ?ur" by linarith - from rsquarefree_roots rsf ur3 - have pd_nonz:"poly (pderiv ?p) ?ur \ 0" by auto - obtain d where d':"\d'. d'>0 \ d' \ d \ - sgn (poly ?p (?ur + d')) = sgn (poly ?p (?ur + d)) \ - sgn (poly ?p (?ur - d')) = sgn (poly ?p (?ur - d))" - "sgn (poly ?p (?ur - d)) \ sgn (poly ?p (?ur + d))" - "sgn (poly ?p (?ur + d)) \ 0" - and d_ge_0:"d > 0" - by (metis root_sign_change[OF ur3 pd_nonz]) - have sr:"sgn (poly ?p (?ur + d)) = sgn (poly ?p (?r r))" - proof (cases "?r r - ?ur \ d") - case True show ?thesis using d'(1)[OF ur2 True] by auto - next - case False hence less:"?ur + d < ?r r" by auto - show ?thesis - proof(rule no_roots_inbetween_imp_same_sign[OF less,rule_format],goal_cases) - case (1 x) - from ur 1 d_ge_0 have ran: "real_of_rat l \ x" "x \ real_of_rat r" by (auto elim!: unique_rootE) - from 1 d_ge_0 have "the_unique_root (p, l, r) \ x" by auto - with ur have "\ root_cond (p,l,r) x" by auto - with ran show ?case by auto - qed - qed - consider "?r l < ?ur - d" "?r l < ?ur" | "0 < ?ur - ?r l" "?ur - ?r l \ d" | "?ur = ?r l" - using urD by argo - hence sl:"sgn (poly ?p (?ur - d)) = sgn (poly ?p (?r l)) \ 0 = sgn (poly ?p (?r l))" - proof (cases) - case 1 - have "sgn (poly ?p (?r l)) = sgn (poly ?p (?ur - d))" - proof(rule no_roots_inbetween_imp_same_sign[OF 1(1),rule_format],goal_cases) - case (1 x) - from ur 1 d_ge_0 have ran: "real_of_rat l \ x" "x \ real_of_rat r" by (auto elim!: unique_rootE) - from 1 d_ge_0 have "the_unique_root (p, l, r) \ x" by auto - with ur have "\ root_cond (p,l,r) x" by auto - with ran show ?case by auto - qed - thus ?thesis by auto - next case 2 show ?thesis using d'(1)[OF 2] by simp - qed (insert ur3,simp) - have diff_sign: "sgn (ipoly p l) \ sgn (ipoly p r)" - using d'(2-) sr sl real_of_rat_sgn by auto - have ur':"\x. real_of_rat l \ x \ x \ real_of_rat y \ ipoly p x = 0 \ \ (?r y \ the_unique_root (p,l,r))" - proof(standard+,goal_cases) - case (1 x) - { - assume id: "the_unique_root (p,l,r) = ?r y" - with unique_rootE[OF ur] ur py0 have False by auto - } note neq = this - have "root_cond (p, l, r) x" unfolding root_cond_def - using 1 a ur by (auto elim!: unique_rootE) - with conjunct2[OF 1(1)] 1(2-) the_unique_root_eqI[OF ur] - show ?case by (auto intro!: neq) - qed - hence ur'':"\x. real_of_rat y \ x \ x \ real_of_rat r \ poly (real_of_int_poly p) x \ 0 \ \ (?r y \ the_unique_root (p,l,r))" - using urD(2,3) by auto - have "(sgn (ipoly p y) = sgn (ipoly p r)) = (?r y > the_unique_root (p,l,r))" - proof(cases "sgn (ipoly p r) = sgn (ipoly p y)") - case True - have sgn:"sgn (poly ?p (real_of_rat l)) \ sgn (poly ?p (real_of_rat y))" using True diff_sign - by (simp add: real_of_rat_sgn) - have ly:"of_rat l < (of_rat y::real)" using in_interval True diff_sign less_eq_rat_def of_rat_less by auto - with no_roots_inbetween_imp_same_sign[OF ly,of ?p] sgn ur' True - show ?thesis by force - next - case False - hence ne:"sgn (ipoly p (real_of_rat y)) \ sgn (ipoly p (real_of_rat r))" by (simp add: real_of_rat_sgn) - have ry:"of_rat y < (of_rat r::real)" using in_interval False diff_sign less_eq_rat_def of_rat_less by auto - obtain x where x:"real_of_rat y \ x" "x \ real_of_rat r" "ipoly p x = 0" - using no_roots_inbetween_imp_same_sign[OF ry,of ?p] ne by auto - hence lx:"real_of_rat l \ x" using in_interval - using False a urD by auto - have "?ur = x" using x lx ur by (intro the_unique_root_eqI, auto) - then show ?thesis using False x by auto - qed - thus False using diff_sign(1) a py0 by(cases "ipoly p r = 0";auto simp:sgn_0_0) -qed - lemma gt_rat_sign_change: assumes ur: "unique_root plr" defines "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes p: "poly_cond2 p" and in_interval: "l \ y" "y \ r" - shows "(sgn (ipoly p y) = sgn (ipoly p r)) = (of_rat y > the_unique_root plr)" (is "?gt = _") -proof (rule gt_rat_sign_change_square_free[of plr, folded p_def l_def r_def, OF ur _ in_interval]) - note nz = poly_cond2_no_rat_root[OF p] - from nz[of y] show "ipoly p y \ 0" by auto - from nz[of r] show "ipoly p r \ 0" by auto - from p have "irreducible p" by auto - thus "square_free p" by (rule irreducible_imp_square_free) + shows "(sgn (ipoly p y) = sgn (ipoly p r)) = (of_rat y > the_unique_root plr)" +proof - + have plr: "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def) + show ?thesis + proof (rule gt_rat_sign_change_square_free[OF ur plr _ in_interval]) + note nz = poly_cond2_no_rat_root[OF p] + from nz[of y] show "ipoly p y \ 0" by auto + from nz[of r] show "ipoly p r \ 0" by auto + from p have "irreducible p" by auto + thus "square_free p" by (rule irreducible_imp_square_free) + qed qed definition tighten_poly_bounds :: "rat \ rat \ rat \ rat \ rat \ rat" where "tighten_poly_bounds l r sr = (let m = (l + r) / 2; sm = sgn (ipoly p m) in if sm = sr then (l,m,sm) else (m,r,sr))" lemma tighten_poly_bounds: assumes res: "tighten_poly_bounds l r sr = (l',r',sr')" and ur: "unique_root (p,l,r)" and p: "poly_cond2 p" and sr: "sr = sgn (ipoly p r)" shows "root_cond (p,l',r') (the_unique_root (p,l,r))" "l \ l'" "l' \ r'" "r' \ r" "(r' - l') = (r - l) / 2" "sr' = sgn (ipoly p r')" proof - let ?x = "the_unique_root (p,l,r)" let ?x' = "the_unique_root (p,l',r')" let ?m = "(l + r) / 2" note d = tighten_poly_bounds_def Let_def from unique_root_lr[OF ur] have lr: "l \ r" by auto thus "l \ l'" "l' \ r'" "r' \ r" "(r' - l') = (r - l) / 2" "sr' = sgn (ipoly p r')" using res sr unfolding d by (auto split: if_splits) hence "l \ ?m" "?m \ r" by auto note le = gt_rat_sign_change[OF ur,simplified,OF p this] note urD = unique_rootD[OF ur] show "root_cond (p,l',r') ?x" proof (cases "sgn (ipoly p ?m) = sgn (ipoly p r)") case *: False with res sr have id: "l' = ?m" "r' = r" unfolding d by auto from *[unfolded le] urD show ?thesis unfolding id by auto next case *: True with res sr have id: "l' = l" "r' = ?m" unfolding d by auto from *[unfolded le] urD show ?thesis unfolding id by auto qed qed partial_function (tailrec) tighten_poly_bounds_epsilon :: "rat \ rat \ rat \ rat \ rat \ rat" where [code]: "tighten_poly_bounds_epsilon l r sr = (if r - l \ x then (l,r,sr) else (case tighten_poly_bounds l r sr of (l',r',sr') \ tighten_poly_bounds_epsilon l' r' sr'))" partial_function (tailrec) tighten_poly_bounds_for_x :: "rat \ rat \ rat \ rat \ rat \ rat" where [code]: "tighten_poly_bounds_for_x l r sr = (if x < l \ r < x then (l, r, sr) else (case tighten_poly_bounds l r sr of (l',r',sr') \ tighten_poly_bounds_for_x l' r' sr'))" lemma tighten_poly_bounds_epsilon: assumes ur: "unique_root (p,l,r)" defines u: "u \ the_unique_root (p,l,r)" assumes p: "poly_cond2 p" and res: "tighten_poly_bounds_epsilon l r sr = (l',r',sr')" and sr: "sr = sgn (ipoly p r)" and x: "x > 0" shows "l \ l'" "r' \ r" "root_cond (p,l',r') u" "r' - l' \ x" "sr' = sgn (ipoly p r')" proof - let ?u = "the_unique_root (p,l,r)" define delta where "delta = x / 2" have delta: "delta > 0" unfolding delta_def using x by auto let ?dist = "\ (l,r,sr). r - l" let ?rel = "inv_image {(x, y). 0 \ y \ delta_gt delta x y} ?dist" note SN = SN_inv_image[OF delta_gt_SN[OF delta], of ?dist] note simps = res[unfolded tighten_poly_bounds_for_x.simps[of l r]] let ?P = "\ (l,r,sr). unique_root (p,l,r) \ u = the_unique_root (p,l,r) \ tighten_poly_bounds_epsilon l r sr = (l',r',sr') \ sr = sgn (ipoly p r) \ l \ l' \ r' \ r \ r' - l' \ x \ root_cond (p,l',r') u \ sr' = sgn (ipoly p r')" have "?P (l,r,sr)" proof (induct rule: SN_induct[OF SN]) case (1 lr) obtain l r sr where lr: "lr = (l,r,sr)" by (cases lr, auto) show ?case unfolding lr split proof (intro impI) assume ur: "unique_root (p, l, r)" and u: "u = the_unique_root (p, l, r)" and res: "tighten_poly_bounds_epsilon l r sr = (l', r', sr')" and sr: "sr = sgn (ipoly p r)" note tur = unique_rootD[OF ur] note simps = tighten_poly_bounds_epsilon.simps[of l r sr] show "l \ l' \ r' \ r \ r' - l' \ x \ root_cond (p, l', r') u \ sr' = sgn (ipoly p r')" proof (cases "r - l \ x") case True with res[unfolded simps] ur tur(4) u sr show ?thesis by auto next case False hence x: "r - l > x" by auto let ?tight = "tighten_poly_bounds l r sr" obtain L R SR where tight: "?tight = (L,R,SR)" by (cases ?tight, auto) note tighten = tighten_poly_bounds[OF tight[unfolded sr] ur p] from unique_root_sub_interval[OF ur tighten(1-2,4)] p have ur': "unique_root (p,L,R)" "u = the_unique_root (p,L,R)" unfolding u by auto from res[unfolded simps tight] False sr have "tighten_poly_bounds_epsilon L R SR = (l',r',sr')" by auto note IH = 1[of "(L,R,SR)", unfolded tight split lr, rule_format, OF _ ur' this] have "L \ l' \ r' \ R \ r' - l' \ x \ root_cond (p, l', r') u \ sr' = sgn (ipoly p r')" by (rule IH, insert tighten False, auto simp: delta_gt_def delta_def) thus ?thesis using tighten by auto qed qed qed from this[unfolded split u, rule_format, OF ur refl res sr] show "l \ l'" "r' \ r" "root_cond (p,l',r') u" "r' - l' \ x" "sr' = sgn (ipoly p r')" using u by auto qed lemma tighten_poly_bounds_for_x: assumes ur: "unique_root (p,l,r)" defines u: "u \ the_unique_root (p,l,r)" assumes p: "poly_cond2 p" and res: "tighten_poly_bounds_for_x l r sr = (l',r',sr')" and sr: "sr = sgn (ipoly p r)" shows "l \ l'" "l' \ r'" "r' \ r" "root_cond (p,l',r') u" "\ (l' \ x \ x \ r')" "sr' = sgn (ipoly p r')" "unique_root (p,l',r')" proof - let ?u = "the_unique_root (p,l,r)" let ?x = "real_of_rat x" define delta where "delta = abs ((u - ?x) / 2)" let ?p = "real_of_int_poly p" note ru = unique_rootD[OF ur] { assume "u = ?x" note u = this[unfolded u] from poly_cond2_no_rat_root[OF p] ur have False by (elim unique_rootE, auto simp: u) } hence delta: "delta > 0" unfolding delta_def by auto let ?dist = "\ (l,r,sr). real_of_rat (r - l)" let ?rel = "inv_image {(x, y). 0 \ y \ delta_gt delta x y} ?dist" note SN = SN_inv_image[OF delta_gt_SN[OF delta], of ?dist] note simps = res[unfolded tighten_poly_bounds_for_x.simps[of l r]] let ?P = "\ (l,r,sr). unique_root (p,l,r) \ u = the_unique_root (p,l,r) \ tighten_poly_bounds_for_x l r sr = (l',r',sr') \ sr = sgn (ipoly p r) \ l \ l' \ r' \ r \ \ (l' \ x \ x \ r') \ root_cond (p,l',r') u \ sr' = sgn (ipoly p r')" have "?P (l,r,sr)" proof (induct rule: SN_induct[OF SN]) case (1 lr) obtain l r sr where lr: "lr = (l,r,sr)" by (cases lr, auto) let ?l = "real_of_rat l" let ?r = "real_of_rat r" show ?case unfolding lr split proof (intro impI) assume ur: "unique_root (p, l, r)" and u: "u = the_unique_root (p, l, r)" and res: "tighten_poly_bounds_for_x l r sr = (l', r', sr')" and sr: "sr = sgn (ipoly p r)" note tur = unique_rootD[OF ur] note simps = tighten_poly_bounds_for_x.simps[of l r] show "l \ l' \ r' \ r \ \ (l' \ x \ x \ r') \ root_cond (p, l', r') u \ sr' = sgn (ipoly p r')" proof (cases "x < l \ r < x") case True with res[unfolded simps] ur tur(4) u sr show ?thesis by auto next case False hence x: "?l \ ?x" "?x \ ?r" by (auto simp: of_rat_less_eq) let ?tight = "tighten_poly_bounds l r sr" obtain L R SR where tight: "?tight = (L,R,SR)" by (cases ?tight, auto) note tighten = tighten_poly_bounds[OF tight ur p sr] from unique_root_sub_interval[OF ur tighten(1-2,4)] p have ur': "unique_root (p,L,R)" "u = the_unique_root (p,L,R)" unfolding u by auto from res[unfolded simps tight] False have "tighten_poly_bounds_for_x L R SR = (l',r',sr')" by auto note IH = 1[of ?tight, unfolded tight split lr, rule_format, OF _ ur' this] let ?DIFF = "real_of_rat (R - L)" let ?diff = "real_of_rat (r - l)" have diff0: "0 \ ?DIFF" using tighten(3) by (metis cancel_comm_monoid_add_class.diff_cancel diff_right_mono of_rat_less_eq of_rat_hom.hom_zero) have *: "r - l - (r - l) / 2 = (r - l) / 2" by (auto simp: field_simps) have "delta_gt delta ?diff ?DIFF = (abs (u - of_rat x) \ real_of_rat (r - l) * 1)" unfolding delta_gt_def tighten(5) delta_def of_rat_diff[symmetric] * by (simp add: hom_distribs) also have "real_of_rat (r - l) * 1 = ?r - ?l" unfolding of_rat_divide of_rat_mult of_rat_diff by auto also have "abs (u - of_rat x) \ ?r - ?l" using x ur by (elim unique_rootE, auto simp: u) finally have delta: "delta_gt delta ?diff ?DIFF" . have "L \ l' \ r' \ R \ \ (l' \ x \ x \ r') \ root_cond (p, l', r') u \ sr' = sgn (ipoly p r')" by (rule IH, insert delta diff0 tighten(6), auto) with \l \ L\ \R \ r\ show ?thesis by auto qed qed qed from this[unfolded split u, rule_format, OF ur refl res sr] show *: "l \ l'" "r' \ r" "root_cond (p,l',r') u" "\ (l' \ x \ x \ r')" "sr' = sgn (ipoly p r')" unfolding u by auto from *(3)[unfolded split] have "real_of_rat l' \ of_rat r'" by auto thus "l' \ r'" unfolding of_rat_less_eq . show "unique_root (p,l',r')" using ur *(1-3) p poly_condD(5) u unique_root_sub_interval(1) by blast qed end definition real_alg_precision :: rat where "real_alg_precision \ Rat.Fract 1 2" lemma real_alg_precision: "real_alg_precision > 0" by eval definition normalize_bounds_1_main :: "rat \ real_alg_1 \ real_alg_1" where "normalize_bounds_1_main eps rai = (case rai of (p,l,r) \ let (l',r',sr') = tighten_poly_bounds_epsilon p eps l r (sgn (ipoly p r)); fr = rat_of_int (floor r'); (l'',r'',_) = tighten_poly_bounds_for_x p fr l' r' sr' in (p,l'',r''))" definition normalize_bounds_1 :: "real_alg_1 \ real_alg_1" where "normalize_bounds_1 = (normalize_bounds_1_main real_alg_precision)" context fixes p q and l r :: rat assumes cong: "\ x. real_of_rat l \ x \ x \ of_rat r \ (ipoly p x = (0 :: real)) = (ipoly q x = 0)" begin lemma root_cond_cong: "root_cond (p,l,r) = root_cond (q,l,r)" by (intro ext, insert cong, auto simp: root_cond_def) lemma the_unique_root_cong: "the_unique_root (p,l,r) = the_unique_root (q,l,r)" unfolding root_cond_cong .. lemma unique_root_cong: "unique_root (p,l,r) = unique_root (q,l,r)" unfolding root_cond_cong .. end lemma normalize_bounds_1_main: assumes eps: "eps > 0" and rc: "invariant_1_2 x" defines y: "y \ normalize_bounds_1_main eps x" shows "invariant_1_2 y \ (real_of_1 y = real_of_1 x)" proof - obtain p l r where x: "x = (p,l,r)" by (cases x) auto note rc = rc[unfolded x] obtain l' r' sr' where tb: "tighten_poly_bounds_epsilon p eps l r (sgn (ipoly p r)) = (l',r',sr')" by (cases rule: prod_cases3, auto) let ?fr = "rat_of_int (floor r')" obtain l'' r'' sr'' where tbx: "tighten_poly_bounds_for_x p ?fr l' r' sr' = (l'',r'',sr'')" by (cases rule: prod_cases3, auto) from y[unfolded normalize_bounds_1_main_def x] tb tbx have y: "y = (p, l'', r'')" by (auto simp: Let_def) from rc have "unique_root (p, l, r)" and p2: "poly_cond2 p" by auto from tighten_poly_bounds_epsilon[OF this tb refl eps] have bnd: "l \ l'" "r' \ r" and rc': "root_cond (p, l', r') (the_unique_root (p, l, r))" and eps: "r' - l' \ eps" (* currently not relevant for lemma *) and sr': "sr' = sgn (ipoly p r')" by auto from invariant_1_sub_interval[OF _ rc' bnd] rc have inv': "invariant_1 (p, l', r')" and eq: "real_of_1 (p, l', r') = real_of_1 (p, l, r)" by auto have bnd: "l' \ l''" "r'' \ r'" and rc': "root_cond (p, l'', r'') (the_unique_root (p, l', r'))" by (rule tighten_poly_bounds_for_x[OF _ p2 tbx sr'], fact invariant_1D[OF inv'])+ from invariant_1_sub_interval[OF inv' rc' bnd] p2 eq show ?thesis unfolding y x by auto qed lemma normalize_bounds_1: assumes x: "invariant_1_2 x" shows "invariant_1_2 (normalize_bounds_1 x) \ (real_of_1 (normalize_bounds_1 x) = real_of_1 x)" proof(cases x) case xx:(fields p l r) let ?res = "(p,l,r)" have norm: "normalize_bounds_1 x = (normalize_bounds_1_main real_alg_precision ?res)" unfolding normalize_bounds_1_def by (simp add: xx) from x have x: "invariant_1_2 ?res" "real_of_1 ?res = real_of_1 x" unfolding xx by auto from normalize_bounds_1_main[OF real_alg_precision x(1)] x(2-) show ?thesis unfolding normalize_bounds_1_def xx by auto qed lemma normalize_bound_1_poly: "poly_real_alg_1 (normalize_bounds_1 rai) = poly_real_alg_1 rai" unfolding normalize_bounds_1_def normalize_bounds_1_main_def Let_def by (auto split: prod.splits) definition real_alg_2_main :: "root_info \ real_alg_1 \ real_alg_2" where "real_alg_2_main ri rai \ let p = poly_real_alg_1 rai in (if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1)) else (case normalize_bounds_1 rai of (p',l,r) \ Irrational (root_info.number_root ri r) (p',l,r)))" definition real_alg_2 :: "real_alg_1 \ real_alg_2" where "real_alg_2 rai \ let p = poly_real_alg_1 rai in (if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1)) else (case normalize_bounds_1 rai of (p',l,r) \ Irrational (root_info.number_root (root_info p) r) (p',l,r)))" lemma degree_1_ipoly: assumes "degree p = Suc 0" shows "ipoly p x = 0 \ (x = real_of_rat (Rat.Fract (- coeff p 0) (coeff p 1)))" proof - from roots1[of "map_poly real_of_int p"] assms have "ipoly p x = 0 \ x \ {roots1 (real_of_int_poly p)}" by auto also have "\ = (x = real_of_rat (Rat.Fract (- coeff p 0) (coeff p 1)))" unfolding Fract_of_int_quotient roots1_def hom_distribs by auto finally show ?thesis . qed lemma invariant_1_degree_0: assumes inv: "invariant_1 rai" shows "degree (poly_real_alg_1 rai) \ 0" (is "degree ?p \ 0") proof (rule notI) assume deg: "degree ?p = 0" from inv have "ipoly ?p (real_of_1 rai) = 0" by auto with deg have "?p = 0" by (meson less_Suc0 representsI represents_degree) with inv show False by auto qed lemma real_alg_2_main: assumes inv: "invariant_1 rai" defines [simp]: "p \ poly_real_alg_1 rai" assumes ric: "irreducible (poly_real_alg_1 rai) \ root_info_cond ri (poly_real_alg_1 rai)" shows "invariant_2 (real_alg_2_main ri rai)" "real_of_2 (real_alg_2_main ri rai) = real_of_1 rai" proof (atomize(full)) define l r where [simp]: "l \ rai_lb rai" and [simp]: "r \ rai_ub rai" show "invariant_2 (real_alg_2_main ri rai) \ real_of_2 (real_alg_2_main ri rai) = real_of_1 rai" unfolding id using invariant_1D proof (cases "degree p" "Suc 0" rule: linorder_cases) case deg: equal hence id: "real_alg_2_main ri rai = Rational (Rat.Fract (- coeff p 0) (coeff p 1))" unfolding real_alg_2_main_def Let_def by auto note rc = invariant_1D[OF inv] from degree_1_ipoly[OF deg, of "the_unique_root rai"] rc(1) show ?thesis unfolding id by auto next case deg: greater with inv have inv: "invariant_1_2 rai" unfolding p_def by auto define rai' where "rai' = normalize_bounds_1 rai" have rai': "real_of_1 rai = real_of_1 rai'" and inv': "invariant_1_2 rai'" unfolding rai'_def using normalize_bounds_1[OF inv] by auto obtain p' l' r' where "rai' = (p',l',r')" by (cases rai') with arg_cong[OF rai'_def, of poly_real_alg_1, unfolded normalize_bound_1_poly] split have split: "rai' = (p,l',r')" by auto from inv'[unfolded split] have "poly_cond p" by auto from poly_condD[OF this] have irr: "irreducible p" by simp from ric irr have ric: "root_info_cond ri p" by auto have id: "real_alg_2_main ri rai = (Irrational (root_info.number_root ri r') rai')" unfolding real_alg_2_main_def Let_def using deg split rai'_def by (auto simp: rai'_def rai') show ?thesis unfolding id using rai' root_info_condD(2)[OF ric] inv'[unfolded split] apply (elim invariant_1_2E invariant_1E) using inv' by(auto simp: split roots_below_the_unique_root) next case deg: less then have "degree p = 0" by auto from this invariant_1_degree_0[OF inv] have "p = 0" by simp with inv show ?thesis by auto qed qed lemma real_alg_2: assumes "invariant_1 rai" shows "invariant_2 (real_alg_2 rai)" "real_of_2 (real_alg_2 rai) = real_of_1 rai" proof - have deg: "0 < degree (poly_real_alg_1 rai)" using assms by auto have "real_alg_2 rai = real_alg_2_main (root_info (poly_real_alg_1 rai)) rai" unfolding real_alg_2_def real_alg_2_main_def Let_def by auto from real_alg_2_main[OF assms root_info, folded this, simplified] deg show "invariant_2 (real_alg_2 rai)" "real_of_2 (real_alg_2 rai) = real_of_1 rai" by auto qed lemma invariant_2_realI: fixes plr :: real_alg_1 defines "p \ poly_real_alg_1 plr" and "l \ rai_lb plr" and "r \ rai_ub plr" assumes x: "root_cond plr x" and sgn: "sgn l = sgn r" and ur: "unique_root plr" and p: "poly_cond p" shows "invariant_2 (real_alg_2 plr) \ real_of_2 (real_alg_2 plr) = x" using invariant_1_realI[OF x,folded p_def l_def r_def] sgn ur p real_alg_2[of plr] by auto (* ********************* *) subsubsection \Comparisons\ fun compare_rat_1 :: "rat \ real_alg_1 \ order" where "compare_rat_1 x (p,l,r) = (if x < l then Lt else if x > r then Gt else if sgn (ipoly p x) = sgn(ipoly p r) then Gt else Lt)" lemma compare_rat_1: assumes rai: "invariant_1_2 y" shows "compare_rat_1 x y = compare (of_rat x) (real_of_1 y)" proof- define p l r where "p \ poly_real_alg_1 y" "l \ rai_lb y" "r \ rai_ub y" then have y [simp]: "y = (p,l,r)" by (cases y, auto) from rai have ur: "unique_root y" by auto show ?thesis proof (cases "x < l \ x > r") case True { assume xl: "x < l" hence "real_of_rat x < of_rat l" unfolding of_rat_less by auto with rai have "of_rat x < the_unique_root y" by (auto elim!: invariant_1E) with xl rai have ?thesis by (cases y, auto simp: compare_real_def comparator_of_def) } moreover { assume xr: "\ x < l" "x > r" hence "real_of_rat x > of_rat r" unfolding of_rat_less by auto with rai have "of_rat x > the_unique_root y" by (auto elim!: invariant_1E) with xr rai have ?thesis by (cases y, auto simp: compare_real_def comparator_of_def) } ultimately show ?thesis using True by auto next case False have 0: "ipoly p (real_of_rat x) \ 0" by (rule poly_cond2_no_rat_root, insert rai, auto) with rai have diff: "real_of_1 y \ of_rat x" by (auto elim!: invariant_1E) have "\ P. (1 < degree (poly_real_alg_1 y) \ \!x. root_cond y x \ poly_cond p \ P) \ P" using poly_real_alg_1.simps y rai invariant_1_2E invariant_1E by metis from this[OF gt_rat_sign_change] False have left: "compare_rat_1 x y = (if real_of_rat x \ the_unique_root y then Lt else Gt)" by (auto simp:poly_cond2_def) also have "\ = compare (real_of_rat x) (real_of_1 y)" using diff by (auto simp: compare_real_def comparator_of_def) finally show ?thesis . qed qed lemma cf_pos_0[simp]: "\ cf_pos 0" unfolding cf_pos_def by auto (* ********************* *) subsubsection\Negation\ fun uminus_1 :: "real_alg_1 \ real_alg_1" where "uminus_1 (p,l,r) = (abs_int_poly (poly_uminus p), -r, -l)" lemma uminus_1: assumes x: "invariant_1 x" defines y: "y \ uminus_1 x" shows "invariant_1 y \ (real_of_1 y = - real_of_1 x)" proof (cases x) case plr: (fields p l r) from x plr have inv: "invariant_1 (p,l,r)" by auto note * = invariant_1D[OF this] from plr have x: "x = (p,l,r)" by simp let ?p = "poly_uminus p" let ?mp = "abs_int_poly ?p" have y: "y = (?mp, -r , -l)" unfolding y plr by (simp add: Let_def) { fix y assume "root_cond (?mp, - r, - l) y" hence mpy: "ipoly ?mp y = 0" and bnd: "- of_rat r \ y" "y \ - of_rat l" unfolding root_cond_def by (auto simp: of_rat_minus) from mpy have id: "ipoly p (- y) = 0" by auto from bnd have bnd: "of_rat l \ - y" "-y \ of_rat r" by auto from id bnd have "root_cond (p, l, r) (-y)" unfolding root_cond_def by auto with inv x have "real_of_1 x = -y" by (auto intro!: the_unique_root_eqI) then have "-real_of_1 x = y" by auto } note inj = this have rc: "root_cond (?mp, - r, - l) (- real_of_1 x)" using * unfolding root_cond_def y x by (auto simp: of_rat_minus sgn_minus_rat) from inj rc have ur': "unique_root (?mp, -r, -l)" by (auto intro: unique_rootI) with rc have the: "- real_of_1 x = the_unique_root (?mp, -r, -l)" by (auto intro: the_unique_root_eqI) have xp: "p represents (real_of_1 x)" using * unfolding root_cond_def split represents_def x by auto from * have mon: "lead_coeff ?mp > 0" by (unfold pos_poly_abs_poly, auto) from poly_uminus_irreducible * have mi: "irreducible ?mp" by auto from mi mon have pc': "poly_cond ?mp" by (auto simp: cf_pos_def) from poly_condD[OF pc'] have irr: "irreducible ?mp" by auto show ?thesis unfolding y apply (intro invariant_1_realI ur' rc) using pc' inv by auto qed lemma uminus_1_2: assumes x: "invariant_1_2 x" defines y: "y \ uminus_1 x" shows "invariant_1_2 y \ (real_of_1 y = - real_of_1 x)" proof - from x have "invariant_1 x" by auto from uminus_1[OF this] have *: "real_of_1 y = - real_of_1 x" "invariant_1 y" unfolding y by auto obtain p l r where id: "x = (p,l,r)" by (cases x) from x[unfolded id] have "degree p > 1" by auto moreover have "poly_real_alg_1 y = abs_int_poly (poly_uminus p)" unfolding y id uminus_1.simps split Let_def by auto ultimately have "degree (poly_real_alg_1 y) > 1" by simp with * show ?thesis by auto qed fun uminus_2 :: "real_alg_2 \ real_alg_2" where "uminus_2 (Rational r) = Rational (-r)" | "uminus_2 (Irrational n x) = real_alg_2 (uminus_1 x)" lemma uminus_2: assumes "invariant_2 x" shows "real_of_2 (uminus_2 x) = uminus (real_of_2 x)" "invariant_2 (uminus_2 x)" using assms real_alg_2 uminus_1 by (atomize(full), cases x, auto simp: hom_distribs) declare uminus_1.simps[simp del] lift_definition uminus_3 :: "real_alg_3 \ real_alg_3" is uminus_2 by (auto simp: uminus_2) lemma uminus_3: "real_of_3 (uminus_3 x) = - real_of_3 x" by (transfer, auto simp: uminus_2) instantiation real_alg :: uminus begin lift_definition uminus_real_alg :: "real_alg \ real_alg" is uminus_3 by (simp add: uminus_3) instance .. end lemma uminus_real_alg: "- (real_of x) = real_of (- x)" by (transfer, rule uminus_3[symmetric]) (* ********************* *) subsubsection\Inverse\ fun inverse_1 :: "real_alg_1 \ real_alg_2" where "inverse_1 (p,l,r) = real_alg_2 (abs_int_poly (reflect_poly p), inverse r, inverse l)" lemma invariant_1_2_of_rat: assumes rc: "invariant_1_2 rai" shows "real_of_1 rai \ of_rat x" proof - obtain p l r where rai: "rai = (p, l, r)" by (cases rai, auto) from rc[unfolded rai] have "poly_cond2 p" "ipoly p (the_unique_root (p, l, r)) = 0" by (auto elim!: invariant_1E) from poly_cond2_no_rat_root[OF this(1), of x] this(2) show ?thesis unfolding rai by auto qed lemma inverse_1: assumes rcx: "invariant_1_2 x" defines y: "y \ inverse_1 x" shows "invariant_2 y \ (real_of_2 y = inverse (real_of_1 x))" proof (cases x) case x: (fields p l r) from x rcx have rcx: "invariant_1_2 (p,l,r)" by auto from invariant_1_2_poly_cond2[OF rcx] have pc2: "poly_cond2 p" by simp have x0: "real_of_1 (p,l,r) \ 0" using invariant_1_2_of_rat[OF rcx, of 0] x by auto let ?x = "real_of_1 (p,l,r)" let ?mp = "abs_int_poly (reflect_poly p)" from x0 rcx have lr0: "l \ 0" and "r \ 0" by auto from x0 rcx have y: "y = real_alg_2 (?mp, inverse r, inverse l)" unfolding y x Let_def inverse_1.simps by auto from rcx have mon: "lead_coeff ?mp > 0" by (unfold lead_coeff_abs_int_poly, auto) { fix y assume "root_cond (?mp, inverse r, inverse l) y" hence mpy: "ipoly ?mp y = 0" and bnd: "inverse (of_rat r) \ y" "y \ inverse (of_rat l)" unfolding root_cond_def by (auto simp: of_rat_inverse) from sgn_real_mono[OF bnd(1)] sgn_real_mono[OF bnd(2)] have "sgn (of_rat r) \ sgn y" "sgn y \ sgn (of_rat l)" by (simp_all add: algebra_simps) with rcx have sgn: "sgn (inverse (of_rat r)) = sgn y" "sgn y = sgn (inverse (of_rat l))" unfolding sgn_inverse inverse_sgn by (auto simp add: real_of_rat_sgn intro: order_antisym) from sgn[simplified, unfolded real_of_rat_sgn] lr0 have "y \ 0" by (auto simp:sgn_0_0) with mpy have id: "ipoly p (inverse y) = 0" by (auto simp: ipoly_reflect_poly) from inverse_le_sgn[OF sgn(1) bnd(1)] inverse_le_sgn[OF sgn(2) bnd(2)] have bnd: "of_rat l \ inverse y" "inverse y \ of_rat r" by auto from id bnd have "root_cond (p,l,r) (inverse y)" unfolding root_cond_def by auto from rcx this x0 have "?x = inverse y" by auto then have "inverse ?x = y" by auto } note inj = this have rc: "root_cond (?mp, inverse r, inverse l) (inverse ?x)" using rcx x0 apply (elim invariant_1_2E invariant_1E) by (simp add: root_cond_def of_rat_inverse real_of_rat_sgn inverse_le_iff_sgn ipoly_reflect_poly) from inj rc have ur: "unique_root (?mp, inverse r, inverse l)" by (auto intro: unique_rootI) with rc have the: "the_unique_root (?mp, inverse r, inverse l) = inverse ?x" by (auto intro: the_unique_root_eqI) have xp: "p represents ?x" unfolding split represents_def using rcx by (auto elim!: invariant_1E) from reflect_poly_irreducible[OF _ xp x0] poly_condD rcx have mi: "irreducible ?mp" by auto from mi mon have un: "poly_cond ?mp" by (auto simp: poly_cond_def) show ?thesis using rcx rc ur unfolding y by (intro invariant_2_realI, auto simp: x y un) qed fun inverse_2 :: "real_alg_2 \ real_alg_2" where "inverse_2 (Rational r) = Rational (inverse r)" | "inverse_2 (Irrational n x) = inverse_1 x" lemma inverse_2: assumes "invariant_2 x" shows "real_of_2 (inverse_2 x) = inverse (real_of_2 x)" "invariant_2 (inverse_2 x)" using assms by (atomize(full), cases x, auto simp: real_alg_2 inverse_1 hom_distribs) lift_definition inverse_3 :: "real_alg_3 \ real_alg_3" is inverse_2 by (auto simp: inverse_2) lemma inverse_3: "real_of_3 (inverse_3 x) = inverse (real_of_3 x)" by (transfer, auto simp: inverse_2) (* ********************* *) subsubsection\Floor\ fun floor_1 :: "real_alg_1 \ int" where "floor_1 (p,l,r) = (let (l',r',sr') = tighten_poly_bounds_epsilon p (1/2) l r (sgn (ipoly p r)); fr = floor r'; fl = floor l'; fr' = rat_of_int fr in (if fr = fl then fr else let (l'',r'',sr'') = tighten_poly_bounds_for_x p fr' l' r' sr' in if fr' < l'' then fr else fl))" lemma floor_1: assumes "invariant_1_2 x" shows "floor (real_of_1 x) = floor_1 x" proof (cases x) case (fields p l r) obtain l' r' sr' where tbe: "tighten_poly_bounds_epsilon p (1 / 2) l r (sgn (ipoly p r)) = (l',r',sr')" by (cases rule: prod_cases3, auto) let ?fr = "floor r'" let ?fl = "floor l'" let ?fr' = "rat_of_int ?fr" obtain l'' r'' sr'' where tbx: "tighten_poly_bounds_for_x p ?fr' l' r' sr' = (l'',r'',sr'')" by (cases rule: prod_cases3, auto) note rc = assms[unfolded fields] hence rc1: "invariant_1 (p,l,r)" by auto have id: "floor_1 x = ((if ?fr = ?fl then ?fr else if ?fr' < l'' then ?fr else ?fl))" unfolding fields floor_1.simps tbe Let_def split tbx by simp let ?x = "real_of_1 x" have x: "?x = the_unique_root (p,l,r)" unfolding fields by simp have bnd: "l \ l'" "r' \ r" "r' - l' \ 1 / 2" and rc': "root_cond (p, l', r') (the_unique_root (p, l, r))" and sr': "sr' = sgn (ipoly p r')" by (atomize(full), intro conjI tighten_poly_bounds_epsilon[OF _ _ tbe refl],insert rc,auto elim!: invariant_1E) let ?r = real_of_rat from rc'[folded x, unfolded split] have ineq: "?r l' \ ?x" "?x \ ?r r'" "?r l' \ ?r r'" by auto hence lr': "l' \ r'" unfolding of_rat_less_eq by simp have flr: "?fl \ ?fr" by (rule floor_mono[OF lr']) from invariant_1_sub_interval[OF rc1 rc' bnd(1,2)] have rc': "invariant_1 (p, l', r')" and id': "the_unique_root (p, l', r') = the_unique_root (p, l, r)" by auto with rc have rc2': "invariant_1_2 (p, l', r')" by auto have x: "?x = the_unique_root (p,l',r')" unfolding fields using id' by simp { assume "?fr \ ?fl" with flr have flr: "?fl \ ?fr - 1" by simp have "?fr' \ r'" "l' \ ?fr'" using flr bnd by linarith+ } note fl_diff = this show ?thesis proof (cases "?fr = ?fl") case True hence id1: "floor_1 x = ?fr" unfolding id by auto from True have id: "floor (?r l') = floor (?r r')" by simp have "floor ?x \ floor (?r r')" by (rule floor_mono[OF ineq(2)]) moreover have "floor (?r l') \ floor ?x" by (rule floor_mono[OF ineq(1)]) ultimately have "floor ?x = floor (?r r')" unfolding id by (simp add: id) then show ?thesis by (simp add: id1) next case False with id have id: "floor_1 x = (if ?fr' < l'' then ?fr else ?fl)" by simp from rc2' have "unique_root (p,l',r')" "poly_cond2 p" by auto from tighten_poly_bounds_for_x[OF this tbx sr'] have ineq': "l' \ l''" "r'' \ r'" and lr'': "l'' \ r''" and rc'': "root_cond (p,l'',r'') ?x" and fr': "\ (l'' \ ?fr' \ ?fr' \ r'')" unfolding x by auto from rc''[unfolded split] have ineq'': "?r l'' \ ?x" "?x \ ?r r''" by auto from False have "?fr \ ?fl" by auto note fr = fl_diff[OF this] show ?thesis proof (cases "?fr' < l''") case True with id have id: "floor_1 x = ?fr" by simp have "floor ?x \ ?fr" using floor_mono[OF ineq(2)] by simp moreover from True have "?r ?fr' < ?r l''" unfolding of_rat_less . with ineq''(1) have "?r ?fr' \ ?x" by simp from floor_mono[OF this] have "?fr \ floor ?x" by simp ultimately show ?thesis unfolding id by auto next case False with id have id: "floor_1 x = ?fl" by simp from False have "l'' \ ?fr'" by auto from floor_mono[OF ineq(1)] have "?fl \ floor ?x" by simp moreover have "floor ?x \ ?fl" proof - from False fr' have fr': "r'' < ?fr'" by auto hence "floor r'' < ?fr" by linarith with floor_mono[OF ineq''(2)] have "floor ?x \ ?fr - 1" by auto also have "?fr - 1 = floor (r' - 1)" by simp also have "\ \ ?fl" by (rule floor_mono, insert bnd, auto) finally show ?thesis . qed ultimately show ?thesis unfolding id by auto qed qed qed (* ********************* *) subsubsection\Generic Factorization and Bisection Framework\ lemma card_1_Collect_ex1: assumes "card (Collect P) = 1" shows "\! x. P x" proof - from assms[unfolded card_eq_1_iff] obtain x where "Collect P = {x}" by auto thus ?thesis by (intro ex1I[of _ x], auto) qed fun sub_interval :: "rat \ rat \ rat \ rat \ bool" where "sub_interval (l,r) (l',r') = (l' \ l \ r \ r')" fun in_interval :: "rat \ rat \ real \ bool" where "in_interval (l,r) x = (of_rat l \ x \ x \ of_rat r)" definition converges_to :: "(nat \ rat \ rat) \ real \ bool" where "converges_to f x \ (\ n. in_interval (f n) x \ sub_interval (f (Suc n)) (f n)) \ (\ (eps :: real) > 0. \ n l r. f n = (l,r) \ of_rat r - of_rat l \ eps)" context fixes bnd_update :: "'a \ 'a" and bnd_get :: "'a \ rat \ rat" begin definition at_step :: "(nat \ rat \ rat) \ nat \ 'a \ bool" where "at_step f n a \ \ i. bnd_get ((bnd_update ^^ i) a) = f (n + i)" partial_function (tailrec) select_correct_factor_main :: "'a \ (int poly \ root_info)list \ (int poly \ root_info)list \ rat \ rat \ nat \ (int poly \ root_info) \ rat \ rat" where [code]: "select_correct_factor_main bnd todo old l r n = (case todo of Nil \ if n = 1 then (hd old, l, r) else let bnd' = bnd_update bnd in (case bnd_get bnd' of (l,r) \ select_correct_factor_main bnd' old [] l r 0) | Cons (p,ri) todo \ let m = root_info.l_r ri l r in if m = 0 then select_correct_factor_main bnd todo old l r n else select_correct_factor_main bnd todo ((p,ri) # old) l r (n + m))" definition select_correct_factor :: "'a \ (int poly \ root_info)list \ (int poly \ root_info) \ rat \ rat" where "select_correct_factor init polys = (case bnd_get init of (l,r) \ select_correct_factor_main init polys [] l r 0)" lemma select_correct_factor_main: assumes conv: "converges_to f x" and at: "at_step f i a" and res: "select_correct_factor_main a todo old l r n = ((q,ri_fin),(l_fin,r_fin))" and bnd: "bnd_get a = (l,r)" and ri: "\ q ri. (q,ri) \ set todo \ set old \ root_info_cond ri q" and q0: "\ q ri. (q,ri) \ set todo \ set old \ q \ 0" and ex: "\q. q \ fst ` set todo \ fst ` set old \ ipoly q x = 0" and dist: "distinct (map fst (todo @ old))" and old: "\ q ri. (q,ri) \ set old \ root_info.l_r ri l r \ 0" and un: "\ x :: real. (\q. q \ fst ` set todo \ fst ` set old \ ipoly q x = 0) \ \!q. q \ fst ` set todo \ fst ` set old \ ipoly q x = 0" and n: "n = sum_list (map (\ (q,ri). root_info.l_r ri l r) old)" shows "unique_root (q,l_fin,r_fin) \ (q,ri_fin) \ set todo \ set old \ x = the_unique_root (q,l_fin,r_fin)" proof - define orig where "orig = set todo \ set old" have orig: "set todo \ set old \ orig" unfolding orig_def by auto let ?rts = "{x :: real. \ q ri. (q,ri) \ orig \ ipoly q x = 0}" define rts where "rts = ?rts" let ?h = "\ (x,y). abs (x - y)" let ?r = real_of_rat have rts: "?rts = (\ ((\ (q,ri). {x. ipoly q x = 0}) ` set (todo @ old)))" unfolding orig_def by auto have "finite rts" unfolding rts rts_def using finite_ipoly_roots[OF q0] finite_set[of "todo @ old"] by auto hence fin: "finite (rts \ rts - Id)" by auto define diffs where "diffs = insert 1 {abs (x - y) | x y. x \ rts \ y \ rts \ x \ y}" have "finite {abs (x - y) | x y. x \ rts \ y \ rts \ x \ y}" by (rule subst[of _ _ finite, OF _ finite_imageI[OF fin, of ?h]], auto) hence diffs: "finite diffs" "diffs \ {}" unfolding diffs_def by auto define eps where "eps = Min diffs / 2" have "\ x. x \ diffs \ x > 0" unfolding diffs_def by auto with Min_gr_iff[OF diffs] have eps: "eps > 0" unfolding eps_def by auto note conv = conv[unfolded converges_to_def] from conv eps obtain N L R where N: "f N = (L,R)" "?r R - ?r L \ eps" by auto obtain pair where pair: "pair = (todo,i)" by auto define rel where "rel = measures [ \ (t,i). N - i, \ (t :: (int poly \ root_info) list,i). length t]" have wf: "wf rel" unfolding rel_def by simp show ?thesis using at res bnd ri q0 ex dist old un n pair orig proof (induct pair arbitrary: todo i old a l r n rule: wf_induct[OF wf]) case (1 pair todo i old a l r n) note IH = 1(1)[rule_format] note at = 1(2) note res = 1(3)[unfolded select_correct_factor_main.simps[of _ todo]] note bnd = 1(4) note ri = 1(5) note q0 = 1(6) note ex = 1(7) note dist = 1(8) note old = 1(9) note un = 1(10) note n = 1(11) note pair = 1(12) note orig = 1(13) from at[unfolded at_step_def, rule_format, of 0] bnd have fi: "f i = (l,r)" by auto with conv have inx: "in_interval (f i) x" by blast hence lxr: "?r l \ x" "x \ ?r r" unfolding fi by auto from order.trans[OF this] have lr: "l \ r" unfolding of_rat_less_eq . show ?case proof (cases todo) case (Cons rri tod) obtain s ri where rri: "rri = (s,ri)" by force with Cons have todo: "todo = (s,ri) # tod" by simp note res = res[unfolded todo list.simps split Let_def] from root_info_condD(1)[OF ri[of s ri, unfolded todo] lr] have ri': "root_info.l_r ri l r = card {x. root_cond (s, l, r) x}" by auto from q0 have s0: "s \ 0" unfolding todo by auto from finite_ipoly_roots[OF s0] have fins: "finite {x. root_cond (s, l, r) x}" unfolding root_cond_def by auto have rel: "((tod,i), pair) \ rel" unfolding rel_def pair todo by simp show ?thesis proof (cases "root_info.l_r ri l r = 0") case True with res have res: "select_correct_factor_main a tod old l r n = ((q, ri_fin), l_fin, r_fin)" by auto from ri'[symmetric, unfolded True] fins have empty: "{x. root_cond (s, l, r) x} = {}" by simp from ex lxr empty have ex': "(\q. q \ fst ` set tod \ fst ` set old \ ipoly q x = 0)" unfolding todo root_cond_def split by auto have "unique_root (q, l_fin, r_fin) \ (q, ri_fin) \ set tod \ set old \ x = the_unique_root (q, l_fin, r_fin)" proof (rule IH[OF rel at res bnd ri _ ex' _ _ _ n refl], goal_cases) case (5 y) thus ?case using un[of y] unfolding todo by auto next case 2 thus ?case using q0 unfolding todo by auto qed (insert dist old orig, auto simp: todo) thus ?thesis unfolding todo by auto next case False with res have res: "select_correct_factor_main a tod ((s, ri) # old) l r (n + root_info.l_r ri l r) = ((q, ri_fin), l_fin, r_fin)" by auto from ex have ex': "\q. q \ fst ` set tod \ fst ` set ((s, ri) # old) \ ipoly q x = 0" unfolding todo by auto from dist have dist: "distinct (map fst (tod @ (s, ri) # old))" unfolding todo by auto have id: "set todo \ set old = set tod \ set ((s, ri) # old)" unfolding todo by simp show ?thesis unfolding id proof (rule IH[OF rel at res bnd ri _ ex' dist], goal_cases) case 4 thus ?case using un unfolding todo by auto qed (insert old False orig, auto simp: q0 todo n) qed next case Nil note res = res[unfolded Nil list.simps Let_def] from ex[unfolded Nil] lxr obtain s where "s \ fst ` set old \ root_cond (s,l,r) x" unfolding root_cond_def by auto then obtain q1 ri1 old' where old': "old = (q1,ri1) # old'" using id by (cases old, auto) let ?ri = "root_info.l_r ri1 l r" from old[unfolded old'] have 0: "?ri \ 0" by auto from n[unfolded old'] 0 have n0: "n \ 0" by auto from ri[unfolded old'] have ri': "root_info_cond ri1 q1" by auto show ?thesis proof (cases "n = 1") case False with n0 have n1: "n > 1" by auto obtain l' r' where bnd': "bnd_get (bnd_update a) = (l',r')" by force with res False have res: "select_correct_factor_main (bnd_update a) old [] l' r' 0 = ((q, ri_fin), l_fin, r_fin)" by auto have at': "at_step f (Suc i) (bnd_update a)" unfolding at_step_def proof (intro allI, goal_cases) case (1 n) have id: "(bnd_update ^^ Suc n) a = (bnd_update ^^ n) (bnd_update a)" by (induct n, auto) from at[unfolded at_step_def, rule_format, of "Suc n"] show ?case unfolding id by simp qed from 0[unfolded root_info_condD(1)[OF ri' lr]] obtain y1 where y1: "root_cond (q1,l,r) y1" by (cases "Collect (root_cond (q1, l, r)) = {}", auto) from n1[unfolded n old'] have "?ri > 1 \ sum_list (map (\ (q,ri). root_info.l_r ri l r) old') \ 0" by (cases "sum_list (map (\ (q,ri). root_info.l_r ri l r) old')", auto) hence "\ q2 ri2 y2. (q2,ri2) \ set old \ root_cond (q2,l,r) y2 \ y1 \ y2" proof assume "?ri > 1" with root_info_condD(1)[OF ri' lr] have "card {x. root_cond (q1, l, r) x} > 1" by simp from card_gt_1D[OF this] y1 obtain y2 where "root_cond (q1,l,r) y2" and "y1 \ y2" by auto thus ?thesis unfolding old' by auto next assume "sum_list (map (\ (q,ri). root_info.l_r ri l r) old') \ 0" then obtain q2 ri2 where mem: "(q2,ri2) \ set old'" and ri2: "root_info.l_r ri2 l r \ 0" by auto with q0 ri have "root_info_cond ri2 q2" unfolding old' by auto from ri2[unfolded root_info_condD(1)[OF this lr]] obtain y2 where y2: "root_cond (q2,l,r) y2" by (cases "Collect (root_cond (q2, l, r)) = {}", auto) from dist[unfolded old'] split_list[OF mem] have diff: "q1 \ q2" by auto from y1 have q1: "q1 \ fst ` set todo \ fst ` set old \ ipoly q1 y1 = 0" unfolding old' root_cond_def by auto from y2 have q2: "q2 \ fst ` set todo \ fst ` set old \ ipoly q2 y2 = 0" unfolding old' root_cond_def using mem by force have "y1 \ y2" proof assume id: "y1 = y2" from q1 have "\ q1. q1 \ fst ` set todo \ fst ` set old \ ipoly q1 y1 = 0" by blast from un[OF this] q1 q2[folded id] have "q1 = q2" by auto with diff show False by simp qed with mem y2 show ?thesis unfolding old' by auto qed then obtain q2 ri2 y2 where mem2: "(q2,ri2) \ set old" and y2: "root_cond (q2,l,r) y2" and diff: "y1 \ y2" by auto from mem2 orig have "(q1,ri1) \ orig" "(q2,ri2) \ orig" unfolding old' by auto with y1 y2 diff have "abs (y1 - y2) \ diffs" unfolding diffs_def rts_def root_cond_def by auto from Min_le[OF diffs(1) this] have "abs (y1 - y2) \ 2 * eps" unfolding eps_def by auto with eps have eps: "abs (y1 - y2) > eps" by auto from y1 y2 have l: "of_rat l \ min y1 y2" unfolding root_cond_def by auto from y1 y2 have r: "of_rat r \ max y1 y2" unfolding root_cond_def by auto from l r eps have eps: "of_rat r - of_rat l > eps" by auto have "i < N" proof (rule ccontr) assume "\ i < N" hence "\ k. i = N + k" by presburger then obtain k where i: "i = N + k" by auto { fix k l r assume "f (N + k) = (l,r)" hence "of_rat r - of_rat l \ eps" proof (induct k arbitrary: l r) case 0 with N show ?case by auto next case (Suc k l r) obtain l' r' where f: "f (N + k) = (l',r')" by force from Suc(1)[OF this] have IH: "?r r' - ?r l' \ eps" by auto from f Suc(2) conv[THEN conjunct1, rule_format, of "N + k"] have "?r l \ ?r l'" "?r r \ ?r r'" by (auto simp: of_rat_less_eq) thus ?case using IH by auto qed } note * = this from at[unfolded at_step_def i, rule_format, of 0] bnd have "f (N + k) = (l,r)" by auto from *[OF this] eps show False by auto qed hence rel: "((old, Suc i), pair) \ rel" unfolding pair rel_def by auto from dist have dist: "distinct (map fst (old @ []))" unfolding Nil by auto have id: "set todo \ set old = set old \ set []" unfolding Nil by auto show ?thesis unfolding id proof (rule IH[OF rel at' res bnd' ri _ _ dist _ _ _ refl], goal_cases) case 2 thus ?case using q0 by auto qed (insert ex un orig Nil, auto) next case True with res old' have id: "q = q1" "ri_fin = ri1" "l_fin = l" "r_fin = r" by auto from n[unfolded True old'] 0 have 1: "?ri = 1" by (cases ?ri; cases "?ri - 1", auto) from root_info_condD(1)[OF ri' lr] 1 have "card {x. root_cond (q1,l,r) x} = 1" by auto from card_1_Collect_ex1[OF this] have unique: "unique_root (q1,l,r)" . from ex[unfolded Nil old'] consider (A) "ipoly q1 x = 0" | (B) q where "q \ fst ` set old'" "ipoly q x = 0" by auto hence "x = the_unique_root (q1,l,r)" proof (cases) case A with lxr have "root_cond (q1,l,r) x" unfolding root_cond_def by auto from the_unique_root_eqI[OF unique this] show ?thesis by simp next case (B q) with lxr have "root_cond (q,l,r) x" unfolding root_cond_def by auto hence empty: "{x. root_cond (q,l,r) x} \ {}" by auto from B(1) obtain ri' where mem: "(q,ri') \ set old'" by force from q0[unfolded old'] mem have q0: "q \ 0" by auto from finite_ipoly_roots[OF this] have "finite {x. root_cond (q,l,r) x}" unfolding root_cond_def by auto with empty have card: "card {x. root_cond (q,l,r) x} \ 0" by simp from ri[unfolded old'] mem have "root_info_cond ri' q" by auto from root_info_condD(1)[OF this lr] card have "root_info.l_r ri' l r \ 0" by auto with n[unfolded True old'] 1 split_list[OF mem] have False by auto thus ?thesis by simp qed thus ?thesis unfolding id using unique ri' unfolding old' by auto qed qed qed qed lemma select_correct_factor: assumes conv: "converges_to (\ i. bnd_get ((bnd_update ^^ i) init)) x" and res: "select_correct_factor init polys = ((q,ri),(l,r))" and ri: "\ q ri. (q,ri) \ set polys \ root_info_cond ri q" and q0: "\ q ri. (q,ri) \ set polys \ q \ 0" and ex: "\q. q \ fst ` set polys \ ipoly q x = 0" and dist: "distinct (map fst polys)" and un: "\ x :: real. (\q. q \ fst ` set polys \ ipoly q x = 0) \ \!q. q \ fst ` set polys \ ipoly q x = 0" shows "unique_root (q,l,r) \ (q,ri) \ set polys \ x = the_unique_root (q,l,r)" proof - obtain l' r' where init: "bnd_get init = (l',r')" by force from res[unfolded select_correct_factor_def init split] have res: "select_correct_factor_main init polys [] l' r' 0 = ((q, ri), l, r)" by auto have at: "at_step (\ i. bnd_get ((bnd_update ^^ i) init)) 0 init" unfolding at_step_def by auto have "unique_root (q,l,r) \ (q,ri) \ set polys \ set [] \ x = the_unique_root (q,l,r)" by (rule select_correct_factor_main[OF conv at res init ri], insert dist un ex q0, auto) thus ?thesis by auto qed definition real_alg_2' :: "root_info \ int poly \ rat \ rat \ real_alg_2" where [code del]: "real_alg_2' ri p l r = ( if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1)) else real_alg_2_main ri (case tighten_poly_bounds_for_x p 0 l r (sgn (ipoly p r)) of (l',r',sr') \ (p, l', r')))" lemma real_alg_2'_code[code]: "real_alg_2' ri p l r = (if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1)) else case normalize_bounds_1 (case tighten_poly_bounds_for_x p 0 l r (sgn (ipoly p r)) of (l', r', sr') \ (p, l', r')) of (p', l, r) \ Irrational (root_info.number_root ri r) (p', l, r))" unfolding real_alg_2'_def real_alg_2_main_def by (cases "tighten_poly_bounds_for_x p 0 l r (sgn (ipoly p r))", simp add: Let_def) definition real_alg_2'' :: "root_info \ int poly \ rat \ rat \ real_alg_2" where "real_alg_2'' ri p l r = (case normalize_bounds_1 (case tighten_poly_bounds_for_x p 0 l r (sgn (ipoly p r)) of (l', r', sr') \ (p, l', r')) of (p', l, r) \ Irrational (root_info.number_root ri r) (p', l, r))" lemma real_alg_2'': "degree p \ 1 \ real_alg_2'' ri p l r = real_alg_2' ri p l r" unfolding real_alg_2'_code real_alg_2''_def by auto lemma poly_cond_degree_0_imp_no_root: fixes x :: "'b :: {comm_ring_1,ring_char_0}" assumes pc: "poly_cond p" and deg: "degree p = 0" shows "ipoly p x \ 0" proof from pc have "p \ 0" by auto moreover assume "ipoly p x = 0" note poly_zero[OF this] ultimately show False using deg by auto qed lemma real_alg_2': assumes ur: "unique_root (q,l,r)" and pc: "poly_cond q" and ri: "root_info_cond ri q" shows "invariant_2 (real_alg_2' ri q l r) \ real_of_2 (real_alg_2' ri q l r) = the_unique_root (q,l,r)" (is "_ \ _ = ?x") proof (cases "degree q" "Suc 0" rule: linorder_cases) case deg: less then have "degree q = 0" by auto from poly_cond_degree_0_imp_no_root[OF pc this] ur have False by force then show ?thesis by auto next case deg: equal hence id: "real_alg_2' ri q l r = Rational (Rat.Fract (- coeff q 0) (coeff q 1))" unfolding real_alg_2'_def by auto show ?thesis unfolding id using degree_1_ipoly[OF deg] using unique_rootD(4)[OF ur] by auto next case deg: greater with pc have pc2: "poly_cond2 q" by auto let ?rai = "real_alg_2' ri q l r" let ?r = real_of_rat obtain l' r' sr' where tight: "tighten_poly_bounds_for_x q 0 l r (sgn (ipoly q r)) = (l',r',sr')" by (cases rule: prod_cases3, auto) let ?rai' = "(q, l', r')" have rai': "?rai = real_alg_2_main ri ?rai'" unfolding real_alg_2'_def using deg tight by auto hence rai: "real_of_1 ?rai' = the_unique_root (q,l',r')" by auto note tight = tighten_poly_bounds_for_x[OF ur pc2 tight refl] let ?x = "the_unique_root (q, l, r)" from tight have tight: "root_cond (q,l',r') ?x" "l \ l'" "l' \ r'" "r' \ r" "l' > 0 \ r' < 0" by auto from unique_root_sub_interval[OF ur tight(1) tight(2,4)] poly_condD[OF pc] have ur': "unique_root (q, l', r')" and x: "?x = the_unique_root (q,l',r')" by auto from tight(2-) have sgn: "sgn l' = sgn r'" by auto show ?thesis unfolding rai' using real_alg_2_main[of ?rai' ri] invariant_1_realI[of ?rai' ?x] by (auto simp: tight(1) sgn pc ri ur') qed definition select_correct_factor_int_poly :: "'a \ int poly \ real_alg_2" where "select_correct_factor_int_poly init p \ let qs = factors_of_int_poly p; polys = map (\ q. (q, root_info q)) qs; ((q,ri),(l,r)) = select_correct_factor init polys in real_alg_2' ri q l r" lemma select_correct_factor_int_poly: assumes conv: "converges_to (\ i. bnd_get ((bnd_update ^^ i) init)) x" and rai: "select_correct_factor_int_poly init p = rai" and x: "ipoly p x = 0" and p: "p \ 0" shows "invariant_2 rai \ real_of_2 rai = x" proof - obtain qs where fact: "factors_of_int_poly p = qs" by auto define polys where "polys = map (\ q. (q, root_info q)) qs" obtain q ri l r where res: "select_correct_factor init polys = ((q,ri),(l,r))" by (cases "select_correct_factor init polys", auto) have fst: "map fst polys = qs" "fst ` set polys = set qs" unfolding polys_def map_map o_def by force+ note fact' = factors_of_int_poly[OF fact] note rai = rai[unfolded select_correct_factor_int_poly_def Let_def fact, folded polys_def, unfolded res split] from fact' fst have dist: "distinct (map fst polys)" by auto from fact'(2)[OF p, of x] x fst have ex: "\q. q \ fst ` set polys \ ipoly q x = 0" by auto { fix q ri assume "(q,ri) \ set polys" hence ri: "ri = root_info q" and q: "q \ set qs" unfolding polys_def by auto from fact'(1)[OF q] have *: "lead_coeff q > 0" "irreducible q" "degree q > 0" by auto from * have q0: "q \ 0" by auto from root_info[OF *(2-3)] ri have ri: "root_info_cond ri q" by auto note ri q0 * } note polys = this have "unique_root (q, l, r) \ (q, ri) \ set polys \ x = the_unique_root (q, l, r)" by (rule select_correct_factor[OF conv res polys(1) _ ex dist, unfolded fst, OF _ _ fact'(3)[OF p]], insert fact'(2)[OF p] polys(2), auto) hence ur: "unique_root (q,l,r)" and mem: "(q,ri) \ set polys" and x: "x = the_unique_root (q,l,r)" by auto note polys = polys[OF mem] from polys(3-4) have ty: "poly_cond q" by (simp add: poly_cond_def) show ?thesis unfolding x rai[symmetric] by (intro real_alg_2' ur ty polys(1)) qed end (* ********************* *) subsubsection\Addition\ lemma ipoly_0_0[simp]: "ipoly f (0::'a::{comm_ring_1,ring_char_0}) = 0 \ poly f 0 = 0" unfolding poly_0_coeff_0 by simp lemma add_rat_roots_below[simp]: "roots_below (poly_add_rat r p) x = (\y. y + of_rat r) ` roots_below p (x - of_rat r)" proof (unfold add_rat_roots image_def, intro Collect_eqI, goal_cases) case (1 y) then show ?case by (auto intro: exI[of _ "y - real_of_rat r"]) qed lemma add_rat_root_cond: shows "root_cond (cf_pos_poly (poly_add_rat m p),l,r) x = root_cond (p, l - m, r - m) (x - of_rat m)" by (unfold root_cond_def, auto simp add: add_rat_roots hom_distribs) lemma add_rat_unique_root: "unique_root (cf_pos_poly (poly_add_rat m p), l, r) = unique_root (p, l-m, r-m)" by (auto simp: add_rat_root_cond) fun add_rat_1 :: "rat \ real_alg_1 \ real_alg_1" where "add_rat_1 r1 (p2,l2,r2) = ( let p = cf_pos_poly (poly_add_rat r1 p2); (l,r,sr) = tighten_poly_bounds_for_x p 0 (l2+r1) (r2+r1) (sgn (ipoly p (r2+r1))) in (p,l,r))" lemma poly_real_alg_1_add_rat[simp]: "poly_real_alg_1 (add_rat_1 r y) = cf_pos_poly (poly_add_rat r (poly_real_alg_1 y))" by (cases y, auto simp: Let_def split: prod.split) lemma sgn_cf_pos: assumes "lead_coeff p > 0" shows "sgn (ipoly (cf_pos_poly p) (x::'a::linordered_field)) = sgn (ipoly p x)" proof (cases "p = 0") case True with assms show ?thesis by auto next case False from cf_pos_poly_main False obtain d where p': "Polynomial.smult d (cf_pos_poly p) = p" by auto have "d > 0" proof (rule zero_less_mult_pos2) from False assms have "0 < lead_coeff p" by (auto simp: cf_pos_def) also from p' have "\ = d * lead_coeff (cf_pos_poly p)" by (metis lead_coeff_smult) finally show "0 < \". show "lead_coeff (cf_pos_poly p) > 0" using False by (unfold lead_coeff_cf_pos_poly) qed moreover from p' have "ipoly p x = of_int d * ipoly (cf_pos_poly p) x" by (fold poly_smult of_int_hom.map_poly_hom_smult, auto) ultimately show ?thesis by (auto simp: sgn_mult[where 'a='a]) qed lemma add_rat_1: fixes r1 :: rat assumes inv_y: "invariant_1_2 y" defines "z \ add_rat_1 r1 y" shows "invariant_1_2 z \ (real_of_1 z = of_rat r1 + real_of_1 y)" proof (cases y) case y_def: (fields p2 l2 r2) define p where "p \ cf_pos_poly (poly_add_rat r1 p2)" obtain l r sr where lr: "tighten_poly_bounds_for_x p 0 (l2+r1) (r2+r1) (sgn (ipoly p (r2+r1))) = (l,r,sr)" by (metis surj_pair) from lr have z: "z = (p,l,r)" by (auto simp: y_def z_def p_def Let_def) from inv_y have ur: "unique_root (p, l2 + r1, r2 + r1)" by (auto simp: p_def add_rat_root_cond y_def add_rat_unique_root) from inv_y[unfolded y_def invariant_1_2_def,simplified] have pc2: "poly_cond2 p" unfolding p_def apply (intro poly_cond2I poly_add_rat_irreducible poly_condI, unfold lead_coeff_cf_pos_poly) apply (auto elim!: invariant_1E) done note main = tighten_poly_bounds_for_x[OF ur pc2 lr refl, simplified] then have "sgn l = sgn r" unfolding sgn_if apply simp apply linarith done from invariant_1_2_realI[OF main(4) _ main(7), simplified, OF this pc2] main(1-3) ur show ?thesis by (auto simp: z p_def y_def add_rat_root_cond ex1_the_shift) qed fun tighten_poly_bounds_binary :: "int poly \ int poly \ (rat \ rat \ rat) \ rat \ rat \ rat \ (rat \ rat \ rat) \ rat \ rat \ rat" where "tighten_poly_bounds_binary cr1 cr2 ((l1,r1,sr1),(l2,r2,sr2)) = (tighten_poly_bounds cr1 l1 r1 sr1, tighten_poly_bounds cr2 l2 r2 sr2)" lemma tighten_poly_bounds_binary: assumes ur: "unique_root (p1,l1,r1)" "unique_root (p2,l2,r2)" and pt: "poly_cond2 p1" "poly_cond2 p2" defines "x \ the_unique_root (p1,l1,r1)" and "y \ the_unique_root (p2,l2,r2)" assumes bnd: "\ l1 r1 l2 r2 l r sr1 sr2. I l1 \ I l2 \ root_cond (p1,l1,r1) x \ root_cond (p2,l2,r2) y \ bnd ((l1,r1,sr1),(l2,r2,sr2)) = (l,r) \ of_rat l \ f x y \ f x y \ of_rat r" and approx: "\ l1 r1 l2 r2 l1' r1' l2' r2' l l' r r' sr1 sr2 sr1' sr2'. I l1 \ I l2 \ l1 \ r1 \ l2 \ r2 \ (l,r) = bnd ((l1,r1,sr1), (l2,r2,sr2)) \ (l',r') = bnd ((l1',r1',sr1'), (l2',r2',sr2')) \ (l1',r1') \ {(l1,(l1+r1)/2),((l1+r1)/2,r1)} \ (l2',r2') \ {(l2,(l2+r2)/2),((l2+r2)/2,r2)} \ (r' - l') \ 3/4 * (r - l) \ l \ l' \ r' \ r" and I_mono: "\ l l'. I l \ l \ l' \ I l'" and I: "I l1" "I l2" and sr: "sr1 = sgn (ipoly p1 r1)" "sr2 = sgn (ipoly p2 r2)" shows "converges_to (\ i. bnd ((tighten_poly_bounds_binary p1 p2 ^^ i) ((l1,r1,sr1),(l2,r2,sr2)))) (f x y)" proof - let ?upd = "tighten_poly_bounds_binary p1 p2" define upd where "upd = ?upd" define init where "init = ((l1, r1, sr1), l2, r2, sr2)" let ?g = "(\i. bnd ((upd ^^ i) init))" obtain l r where bnd_init: "bnd init = (l,r)" by force note ur1 = unique_rootD[OF ur(1)] note ur2 = unique_rootD[OF ur(2)] from ur1(4) ur2(4) x_def y_def have rc1: "root_cond (p1,l1,r1) x" and rc2: "root_cond (p2,l2,r2) y" by auto define g where "g = ?g" { fix i L1 R1 L2 R2 L R j SR1 SR2 assume "((upd ^^ i)) init = ((L1,R1,SR1),(L2,R2,SR2))" "g i = (L,R)" hence "I L1 \ I L2 \ root_cond (p1,L1,R1) x \ root_cond (p2,L2,R2) y \ unique_root (p1, L1, R1) \ unique_root (p2, L2, R2) \ in_interval (L,R) (f x y) \ (i = Suc j \ sub_interval (g i) (g j) \ (R - L \ 3/4 * (snd (g j) - fst (g j)))) \ SR1 = sgn (ipoly p1 R1) \ SR2 = sgn (ipoly p2 R2)" proof (induct i arbitrary: L1 R1 L2 R2 L R j SR1 SR2) case 0 thus ?case using I rc1 rc2 ur bnd[of l1 l2 r1 r2 sr1 sr2 L R] g_def sr unfolding init_def by auto next case (Suc i) obtain l1 r1 l2 r2 sr1 sr2 where updi: "(upd ^^ i) init = ((l1, r1, sr1), l2, r2, sr2)" by (cases "(upd ^^ i) init", auto) obtain l r where bndi: "bnd ((l1, r1, sr1), l2, r2, sr2) = (l,r)" by force hence gi: "g i = (l,r)" using updi unfolding g_def by auto have "(upd ^^ Suc i) init = upd ((l1, r1, sr1), l2, r2, sr2)" using updi by simp from Suc(2)[unfolded this] have upd: "upd ((l1, r1, sr1), l2, r2, sr2) = ((L1, R1, SR1), L2, R2, SR2)" . from upd updi Suc(3) have bndsi: "bnd ((L1, R1, SR1), L2, R2, SR2) = (L,R)" by (auto simp: g_def) from Suc(1)[OF updi gi] have I: "I l1" "I l2" and rc: "root_cond (p1,l1,r1) x" "root_cond (p2,l2,r2) y" and ur: "unique_root (p1, l1, r1)" "unique_root (p2, l2, r2)" and sr: "sr1 = sgn (ipoly p1 r1)" "sr2 = sgn (ipoly p2 r2)" by auto from upd[unfolded upd_def] have tight: "tighten_poly_bounds p1 l1 r1 sr1 = (L1, R1, SR1)" "tighten_poly_bounds p2 l2 r2 sr2 = (L2, R2, SR2)" by auto note tight1 = tighten_poly_bounds[OF tight(1) ur(1) pt(1) sr(1)] note tight2 = tighten_poly_bounds[OF tight(2) ur(2) pt(2) sr(2)] from tight1 have lr1: "l1 \ r1" by auto from tight2 have lr2: "l2 \ r2" by auto note ur1 = unique_rootD[OF ur(1)] note ur2 = unique_rootD[OF ur(2)] from tight1 I_mono[OF I(1)] have I1: "I L1" by auto from tight2 I_mono[OF I(2)] have I2: "I L2" by auto note ur1 = unique_root_sub_interval[OF ur(1) tight1(1,2,4)] note ur2 = unique_root_sub_interval[OF ur(2) tight2(1,2,4)] from rc(1) ur ur1 have x: "x = the_unique_root (p1,L1,R1)" by (auto intro!:the_unique_root_eqI) from rc(2) ur ur2 have y: "y = the_unique_root (p2,L2,R2)" by (auto intro!:the_unique_root_eqI) from unique_rootD[OF ur1(1)] x have x: "root_cond (p1,L1,R1) x" by auto from unique_rootD[OF ur2(1)] y have y: "root_cond (p2,L2,R2) y" by auto from tight(1) have half1: "(L1, R1) \ {(l1, (l1 + r1) / 2), ((l1 + r1) / 2, r1)}" unfolding tighten_poly_bounds_def Let_def by (auto split: if_splits) from tight(2) have half2: "(L2, R2) \ {(l2, (l2 + r2) / 2), ((l2 + r2) / 2, r2)}" unfolding tighten_poly_bounds_def Let_def by (auto split: if_splits) from approx[OF I lr1 lr2 bndi[symmetric] bndsi[symmetric] half1 half2] have "R - L \ 3 / 4 * (r - l) \ l \ L \ R \ r" . hence "sub_interval (g (Suc i)) (g i)" "R - L \ 3/4 * (snd (g i) - fst (g i))" unfolding gi Suc(3) by auto with bnd[OF I1 I2 x y bndsi] show ?case using I1 I2 x y ur1 ur2 tight1(6) tight2(6) by auto qed } note invariants = this define L where "L = (\ i. fst (g i))" define R where "R = (\ i. snd (g i))" { fix i obtain l1 r1 l2 r2 sr1 sr2 where updi: "(upd ^^ i) init = ((l1, r1, sr1), l2, r2, sr2)" by (cases "(upd ^^ i) init", auto) obtain l r where bnd': "bnd ((l1, r1, sr1), l2, r2, sr2) = (l,r)" by force have gi: "g i = (l,r)" unfolding g_def updi bnd' by auto hence id: "l = L i" "r = R i" unfolding L_def R_def by auto from invariants[OF updi gi[unfolded id]] have "in_interval (L i, R i) (f x y)" "\ j. i = Suc j \ sub_interval (g i) (g j) \ R i - L i \ 3 / 4 * (R j - L j)" unfolding L_def R_def by auto } note * = this { fix i from *(1)[of i] *(2)[of "Suc i", OF refl] have "in_interval (g i) (f x y)" "sub_interval (g (Suc i)) (g i)" "R (Suc i) - L (Suc i) \ 3 / 4 * (R i - L i)" unfolding L_def R_def by auto } note * = this show ?thesis unfolding upd_def[symmetric] init_def[symmetric] g_def[symmetric] unfolding converges_to_def proof (intro conjI allI impI, rule *(1), rule *(2)) fix eps :: real assume eps: "0 < eps" let ?r = real_of_rat define r where "r = (\ n. ?r (R n))" define l where "l = (\ n. ?r (L n))" define diff where "diff = (\ n. r n - l n)" { fix n from *(3)[of n] have "?r (R (Suc n) - L (Suc n)) \ ?r (3 / 4 * (R n - L n))" unfolding of_rat_less_eq by simp also have "?r (R (Suc n) - L (Suc n)) = (r (Suc n) - l (Suc n))" unfolding of_rat_diff r_def l_def by simp also have "?r (3 / 4 * (R n - L n)) = 3 / 4 * (r n - l n)" unfolding r_def l_def by (simp add: hom_distribs) finally have "diff (Suc n) \ 3 / 4 * diff n" unfolding diff_def . } note * = this { fix i have "diff i \ (3/4)^i * diff 0" proof (induct i) case (Suc i) from Suc *[of i] show ?case by auto qed auto } then obtain c where *: "\ i. diff i \ (3/4)^i * c" by auto have "\ n. diff n \ eps" proof (cases "c \ 0") case True with *[of 0] eps show ?thesis by (intro exI[of _ 0], auto) next case False hence c: "c > 0" by auto with eps have "inverse c * eps > 0" by auto from exp_tends_to_zero[of "3/4 :: real", OF _ _ this] obtain n where "(3/4) ^ n \ inverse c * eps" by auto from mult_right_mono[OF this, of c] c have "(3/4) ^ n * c \ eps" by (auto simp: field_simps) with *[of n] show ?thesis by (intro exI[of _ n], auto) qed then obtain n where "?r (R n) - ?r (L n) \ eps" unfolding l_def r_def diff_def by blast thus "\n l r. g n = (l, r) \ ?r r - ?r l \ eps" unfolding L_def R_def by (intro exI[of _ n], force) qed qed fun add_1 :: "real_alg_1 \ real_alg_1 \ real_alg_2" where "add_1 (p1,l1,r1) (p2,l2,r2) = ( select_correct_factor_int_poly (tighten_poly_bounds_binary p1 p2) (\ ((l1,r1,sr1),(l2,r2,sr2)). (l1 + l2, r1 + r2)) ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))) (poly_add p1 p2))" lemma add_1: assumes x: "invariant_1_2 x" and y: "invariant_1_2 y" defines z: "z \ add_1 x y" shows "invariant_2 z \ (real_of_2 z = real_of_1 x + real_of_1 y)" proof (cases x) case xt: (fields p1 l1 r1) show ?thesis proof (cases y) case yt: (fields p2 l2 r2) let ?x = "real_of_1 (p1, l1, r1)" let ?y = "real_of_1 (p2, l2, r2)" let ?p = "poly_add p1 p2" note x = x[unfolded xt] note y = y[unfolded yt] from x have ax: "p1 represents ?x" unfolding represents_def by (auto elim!: invariant_1E) from y have ay: "p2 represents ?y" unfolding represents_def by (auto elim!: invariant_1E) let ?bnd = "(\((l1, r1, sr1 :: rat), l2 :: rat, r2 :: rat, sr2 :: rat). (l1 + l2, r1 + r2))" define bnd where "bnd = ?bnd" have "invariant_2 z \ real_of_2 z = ?x + ?y" proof (intro select_correct_factor_int_poly) from represents_add[OF ax ay] show "?p \ 0" "ipoly ?p (?x + ?y) = 0" by auto from z[unfolded xt yt] show sel: "select_correct_factor_int_poly (tighten_poly_bounds_binary p1 p2) bnd ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))) (poly_add p1 p2) = z" by (auto simp: bnd_def) have ur1: "unique_root (p1,l1,r1)" "poly_cond2 p1" using x by auto have ur2: "unique_root (p2,l2,r2)" "poly_cond2 p2" using y by auto show "converges_to (\i. bnd ((tighten_poly_bounds_binary p1 p2 ^^ i) ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))))) (?x + ?y)" by (intro tighten_poly_bounds_binary ur1 ur2; force simp: bnd_def hom_distribs) qed thus ?thesis unfolding xt yt . qed qed declare add_rat_1.simps[simp del] declare add_1.simps[simp del] (* ********************* *) subsubsection\Multiplication\ context begin private fun mult_rat_1_pos :: "rat \ real_alg_1 \ real_alg_2" where "mult_rat_1_pos r1 (p2,l2,r2) = real_alg_2 (cf_pos_poly (poly_mult_rat r1 p2), l2*r1, r2*r1)" private fun mult_1_pos :: "real_alg_1 \ real_alg_1 \ real_alg_2" where "mult_1_pos (p1,l1,r1) (p2,l2,r2) = select_correct_factor_int_poly (tighten_poly_bounds_binary p1 p2) (\ ((l1,r1,sr1),(l2,r2,sr2)). (l1 * l2, r1 * r2)) ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))) (poly_mult p1 p2)" fun mult_rat_1 :: "rat \ real_alg_1 \ real_alg_2" where "mult_rat_1 x y = (if x < 0 then uminus_2 (mult_rat_1_pos (-x) y) else if x = 0 then Rational 0 else (mult_rat_1_pos x y))" fun mult_1 :: "real_alg_1 \ real_alg_1 \ real_alg_2" where "mult_1 x y = (case (x,y) of ((p1,l1,r1),(p2,l2,r2)) \ if r1 > 0 then if r2 > 0 then mult_1_pos x y else uminus_2 (mult_1_pos x (uminus_1 y)) else if r2 > 0 then uminus_2 (mult_1_pos (uminus_1 x) y) else mult_1_pos (uminus_1 x) (uminus_1 y))" lemma mult_rat_1_pos: fixes r1 :: rat assumes r1: "r1 > 0" and y: "invariant_1 y" defines z: "z \ mult_rat_1_pos r1 y" shows "invariant_2 z \ (real_of_2 z = of_rat r1 * real_of_1 y)" proof - obtain p2 l2 r2 where yt: "y = (p2,l2,r2)" by (cases y, auto) let ?x = "real_of_rat r1" let ?y = "real_of_1 (p2, l2, r2)" let ?p = "poly_mult_rat r1 p2" let ?mp = "cf_pos_poly ?p" note y = y[unfolded yt] note yD = invariant_1D[OF y] from yD r1 have p: "?p \ 0" and r10: "r1 \ 0" by auto hence mp: "?mp \ 0" by simp from yD(1) have rt: "ipoly p2 ?y = 0" and bnd: "of_rat l2 \ ?y" "?y \ of_rat r2" by auto from rt r1 have rt: "ipoly ?mp (?x * ?y) = 0" by (auto simp add: field_simps ipoly_mult_rat[OF r10]) from yD(5) have irr: "irreducible p2" unfolding represents_def using y unfolding root_cond_def split by auto from poly_mult_rat_irreducible[OF this _ r10] yD have irr: "irreducible ?mp" by simp from p have mon: "cf_pos ?mp" by auto obtain l r where lr: "l = l2 * r1" "r = r2 * r1" by force from bnd r1 have bnd: "of_rat l \ ?x * ?y" "?x * ?y \ of_rat r" unfolding lr of_rat_mult by auto with rt have rc: "root_cond (?mp,l,r) (?x * ?y)" unfolding root_cond_def by auto have ur: "unique_root (?mp,l,r)" proof (rule ex1I, rule rc) fix z assume "root_cond (?mp,l,r) z" from this[unfolded root_cond_def split] have bndz: "of_rat l \ z" "z \ of_rat r" and rt: "ipoly ?mp z = 0" by auto have "fst (quotient_of r1) \ 0" using quotient_of_div[of r1] r10 by (cases "quotient_of r1", auto) with rt have rt: "ipoly p2 (z * inverse ?x) = 0" by (auto simp: ipoly_mult_rat[OF r10]) from bndz r1 have "of_rat l2 \ z * inverse ?x" "z * inverse ?x \ of_rat r2" unfolding lr of_rat_mult by (auto simp: field_simps) with rt have "root_cond (p2,l2,r2) (z * inverse ?x)" unfolding root_cond_def by auto also note invariant_1_root_cond[OF y] finally have "?y = z * inverse ?x" by auto thus "z = ?x * ?y" using r1 by auto qed from r1 have sgnr: "sgn r = sgn r2" unfolding lr by (cases "r2 = 0"; cases "r2 < 0"; auto simp: mult_neg_pos mult_less_0_iff) from r1 have sgnl: "sgn l = sgn l2" unfolding lr by (cases "l2 = 0"; cases "l2 < 0"; auto simp: mult_neg_pos mult_less_0_iff) from the_unique_root_eqI[OF ur rc] have xy: "?x * ?y = the_unique_root (?mp,l,r)" by auto from z[unfolded yt, simplified, unfolded Let_def lr[symmetric] split] have z: "z = real_alg_2 (?mp, l, r)" by simp have yp2: "p2 represents ?y" using yD unfolding root_cond_def split represents_def by auto with irr mon have pc: "poly_cond ?mp" by (auto simp: poly_cond_def cf_pos_def) have rc: "invariant_1 (?mp, l, r)" unfolding z using yD(2) pc ur by (auto simp add: invariant_1_def ur mp sgnr sgnl) show ?thesis unfolding z using real_alg_2[OF rc] unfolding yt xy unfolding z by simp qed lemma mult_1_pos: assumes x: "invariant_1_2 x" and y: "invariant_1_2 y" defines z: "z \ mult_1_pos x y" assumes pos: "real_of_1 x > 0" "real_of_1 y > 0" shows "invariant_2 z \ (real_of_2 z = real_of_1 x * real_of_1 y)" proof - obtain p1 l1 r1 where xt: "x = (p1,l1,r1)" by (cases x, auto) obtain p2 l2 r2 where yt: "y = (p2,l2,r2)" by (cases y, auto) let ?x = "real_of_1 (p1, l1, r1)" let ?y = "real_of_1 (p2, l2, r2)" let ?r = "real_of_rat" let ?p = "poly_mult p1 p2" note x = x[unfolded xt] note y = y[unfolded yt] from x y have basic: "unique_root (p1, l1, r1)" "poly_cond2 p1" "unique_root (p2, l2, r2)" "poly_cond2 p2" by auto from basic have irr1: "irreducible p1" and irr2: "irreducible p2" by auto from x have ax: "p1 represents ?x" unfolding represents_def by (auto elim!:invariant_1E) from y have ay: "p2 represents ?y" unfolding represents_def by (auto elim!:invariant_1E) from ax ay pos[unfolded xt yt] have axy: "?p represents (?x * ?y)" by (intro represents_mult represents_irr_non_0[OF irr2], auto) from representsD[OF this] have p: "?p \ 0" and rt: "ipoly ?p (?x * ?y) = 0" . from x pos(1)[unfolded xt] have "?r r1 > 0" unfolding split by auto hence "sgn r1 = 1" unfolding sgn_rat_def by (auto split: if_splits) with x have "sgn l1 = 1" by auto hence l1_pos: "l1 > 0" unfolding sgn_rat_def by (cases "l1 = 0"; cases "l1 < 0"; auto) from y pos(2)[unfolded yt] have "?r r2 > 0" unfolding split by auto hence "sgn r2 = 1" unfolding sgn_rat_def by (auto split: if_splits) with y have "sgn l2 = 1" by auto hence l2_pos: "l2 > 0" unfolding sgn_rat_def by (cases "l2 = 0"; cases "l2 < 0"; auto) let ?bnd = "(\((l1, r1, sr1 :: rat), l2 :: rat, r2 :: rat, sr2 :: rat). (l1 * l2, r1 * r2))" define bnd where "bnd = ?bnd" obtain z' where sel: "select_correct_factor_int_poly (tighten_poly_bounds_binary p1 p2) bnd ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))) ?p = z'" by auto have main: "invariant_2 z' \ real_of_2 z' = ?x * ?y" proof (rule select_correct_factor_int_poly[OF _ sel rt p]) { fix l1 r1 l2 r2 l1' r1' l2' r2' l l' r r' :: rat let ?m1 = "(l1+r1)/2" let ?m2 = "(l2+r2)/2" define d1 where "d1 = r1 - l1" define d2 where "d2 = r2 - l2" let ?M1 = "l1 + d1/2" let ?M2 = "l2 + d2/2" assume le: "l1 > 0" "l2 > 0" "l1 \ r1" "l2 \ r2" and id: "(l, r) = (l1 * l2, r1 * r2)" "(l', r') = (l1' * l2', r1' * r2')" and mem: "(l1', r1') \ {(l1, ?m1), (?m1, r1)}" "(l2', r2') \ {(l2, ?m2), (?m2, r2)}" hence id: "l = l1 * l2" "r = (l1 + d1) * (l2 + d2)" "l' = l1' * l2'" "r' = r1' * r2'" "r1 = l1 + d1" "r2 = l2 + d2" and id': "?m1 = ?M1" "?m2 = ?M2" unfolding d1_def d2_def by (auto simp: field_simps) define l1d1 where "l1d1 = l1 + d1" from le have ge0: "d1 \ 0" "d2 \ 0" "l1 \ 0" "l2 \ 0" unfolding d1_def d2_def by auto have "4 * (r' - l') \ 3 * (r - l)" proof (cases "l1' = l1 \ r1' = ?M1 \ l2' = l2 \ r2' = ?M2") case True hence id2: "l1' = l1" "r1' = ?M1" "l2' = l2" "r2' = ?M2" by auto show ?thesis unfolding id id2 unfolding ring_distribs using ge0 by simp next case False note 1 = this show ?thesis proof (cases "l1' = l1 \ r1' = ?M1 \ l2' = ?M2 \ r2' = r2") case True hence id2: "l1' = l1" "r1' = ?M1" "l2' = ?M2" "r2' = r2" by auto show ?thesis unfolding id id2 unfolding ring_distribs using ge0 by simp next case False note 2 = this show ?thesis proof (cases "l1' = ?M1 \ r1' = r1 \ l2' = l2 \ r2' = ?M2") case True hence id2: "l1' = ?M1" "r1' = r1" "l2' = l2" "r2' = ?M2" by auto show ?thesis unfolding id id2 unfolding ring_distribs using ge0 by simp next case False note 3 = this from 1 2 3 mem have id2: "l1' = ?M1" "r1' = r1" "l2' = ?M2" "r2' = r2" unfolding id' by auto show ?thesis unfolding id id2 unfolding ring_distribs using ge0 by simp qed qed qed hence "r' - l' \ 3 / 4 * (r - l)" by simp } note decr = this show "converges_to (\i. bnd ((tighten_poly_bounds_binary p1 p2 ^^ i) ((l1,r1,sgn (ipoly p1 r1)),(l2,r2, sgn (ipoly p2 r2))))) (?x * ?y)" proof (intro tighten_poly_bounds_binary[where f = "(*)" and I = "\ l. l > 0"] basic l1_pos l2_pos, goal_cases) case (1 L1 R1 L2 R2 L R) hence "L = L1 * L2" "R = R1 * R2" unfolding bnd_def by auto hence id: "?r L = ?r L1 * ?r L2" "?r R = ?r R1 * ?r R2" by (auto simp: hom_distribs) from 1(3-4) have le: "?r L1 \ ?x" "?x \ ?r R1" "?r L2 \ ?y" "?y \ ?r R2" unfolding root_cond_def by auto from 1(1-2) have lt: "0 < ?r L1" "0 < ?r L2" by auto from mult_mono[OF le(1,3), folded id] lt le have L: "?r L \ ?x * ?y" by linarith have R: "?x * ?y \ ?r R" by (rule mult_mono[OF le(2,4), folded id], insert lt le, linarith+) show ?case using L R by blast next case (2 l1 r1 l2 r2 l1' r1' l2' r2' l l' r r') from 2(5-6) have lr: "l = l1 * l2" "r = r1 * r2" "l' = l1' * l2'" "r' = r1' * r2'" unfolding bnd_def by auto from 2(1-4) have le: "0 < l1" "0 < l2" "l1 \ r1" "l2 \ r2" by auto from 2(7-8) le have le': "l1 \ l1'" "r1' \ r1" "l2 \ l2'" "r2' \ r2" "0 < r2'" "0 < r2" by auto from mult_mono[OF le'(1,3), folded lr] le le' have l: "l \ l'" by auto have r: "r' \ r" by (rule mult_mono[OF le'(2,4), folded lr], insert le le', linarith+) have "r' - l' \ 3 / 4 * (r - l)" by (rule decr[OF _ _ _ _ _ _ 2(7-8)], insert le le' lr, auto) thus ?case using l r by blast qed auto qed have z': "z' = z" unfolding z[unfolded xt yt, simplified, unfolded bnd_def[symmetric] sel] by auto from main[unfolded this] show ?thesis unfolding xt yt by simp qed lemma mult_1: assumes x: "invariant_1_2 x" and y: "invariant_1_2 y" defines z[simp]: "z \ mult_1 x y" shows "invariant_2 z \ (real_of_2 z = real_of_1 x * real_of_1 y)" proof - obtain p1 l1 r1 where xt[simp]: "x = (p1,l1,r1)" by (cases x) obtain p2 l2 r2 where yt[simp]: "y = (p2,l2,r2)" by (cases y) let ?xt = "(p1, l1, r1)" let ?yt = "(p2, l2, r2)" let ?x = "real_of_1 ?xt" let ?y = "real_of_1 ?yt" let ?mxt = "uminus_1 ?xt" let ?myt = "uminus_1 ?yt" let ?mx = "real_of_1 ?mxt" let ?my = "real_of_1 ?myt" let ?r = "real_of_rat" from invariant_1_2_of_rat[OF x, of 0] have x0: "?x < 0 \ ?x > 0" by auto from invariant_1_2_of_rat[OF y, of 0] have y0: "?y < 0 \ ?y > 0" by auto from uminus_1_2[OF x] have mx: "invariant_1_2 ?mxt" and [simp]: "?mx = - ?x" by auto from uminus_1_2[OF y] have my: "invariant_1_2 ?myt" and [simp]: "?my = - ?y" by auto have id: "r1 > 0 \ ?x > 0" "r1 < 0 \ ?x < 0" "r2 > 0 \ ?y > 0" "r2 < 0 \ ?y < 0" using x y by auto show ?thesis proof (cases "?x > 0") case x0: True show ?thesis proof (cases "?y > 0") case y0: True with x y x0 mult_1_pos[OF x y] show ?thesis by auto next case False with y0 have y0: "?y < 0" by auto with x0 have z: "z = uminus_2 (mult_1_pos ?xt ?myt)" unfolding z xt yt mult_1.simps split id by simp from x0 y0 mult_1_pos[OF x my] uminus_2[of "mult_1_pos ?xt ?myt"] show ?thesis unfolding z by simp qed next case False with x0 have x0: "?x0 < 0" by simp show ?thesis proof (cases "?y > 0") case y0: True with x0 x y id have z: "z = uminus_2 (mult_1_pos ?mxt ?yt)" by simp from x0 y0 mult_1_pos[OF mx y] uminus_2[of "mult_1_pos ?mxt ?yt"] show ?thesis unfolding z by auto next case False with y0 have y0: "?y < 0" by simp with x0 x y have z: "z = mult_1_pos ?mxt ?myt" by auto with x0 y0 x y mult_1_pos[OF mx my] show ?thesis unfolding z by auto qed qed qed lemma mult_rat_1: fixes x assumes y: "invariant_1 y" defines z: "z \ mult_rat_1 x y" shows "invariant_2 z \ (real_of_2 z = of_rat x * real_of_1 y)" proof (cases y) case yt: (fields p2 l2 r2) let ?yt = "(p2, l2, r2)" let ?x = "real_of_rat x" let ?y = "real_of_1 ?yt" let ?myt = "mult_rat_1_pos (- x) ?yt" note y = y[unfolded yt] note z = z[unfolded yt] show ?thesis proof(cases x "0::rat" rule:linorder_cases) case x: greater with z have z: "z = mult_rat_1_pos x ?yt" by simp from mult_rat_1_pos[OF x y] show ?thesis unfolding yt z by auto next case less then have x: "- x > 0" by auto hence z: "z = uminus_2 ?myt" unfolding z by simp from mult_rat_1_pos[OF x y] have rc: "invariant_2 ?myt" and rr: "real_of_2 ?myt = - ?x * ?y" by (auto simp: hom_distribs) from uminus_2[OF rc] rr show ?thesis unfolding z[symmetric] unfolding yt[symmetric] by simp qed (auto simp: z) qed end declare mult_1.simps[simp del] declare mult_rat_1.simps[simp del] (* ********************* *) subsubsection\Root\ definition ipoly_root_delta :: "int poly \ real" where "ipoly_root_delta p = Min (insert 1 { abs (x - y) | x y. ipoly p x = 0 \ ipoly p y = 0 \ x \ y}) / 4" lemma ipoly_root_delta: assumes "p \ 0" shows "ipoly_root_delta p > 0" "2 \ card (Collect (root_cond (p, l, r))) \ ipoly_root_delta p \ real_of_rat (r - l) / 4" proof - let ?z = "0 :: real" let ?R = "{x. ipoly p x = ?z}" let ?set = "{ abs (x - y) | x y. ipoly p x = ?z \ ipoly p y = 0 \ x \ y}" define S where "S = insert 1 ?set" from finite_ipoly_roots[OF assms] have finR: "finite ?R" and fin: "finite (?R \ ?R)" by auto have "finite ?set" by (rule finite_subset[OF _ finite_imageI[OF fin, of "\ (x,y). abs (x - y)"]], force) hence fin: "finite S" and ne: "S \ {}" and pos: "\ x. x \ S \ x > 0" unfolding S_def by auto have delta: "ipoly_root_delta p = Min S / 4" unfolding ipoly_root_delta_def S_def .. have pos: "Min S > 0" using fin ne pos by auto show "ipoly_root_delta p > 0" unfolding delta using pos by auto let ?S = "Collect (root_cond (p, l, r))" assume "2 \ card ?S" hence 2: "Suc (Suc 0) \ card ?S" by simp from 2[unfolded card_le_Suc_iff[of _ ?S]] obtain x T where ST: "?S = insert x T" and xT: "x \ T" and 1: "Suc 0 \ card T" by auto from 1[unfolded card_le_Suc_iff[of _ T]] obtain y where yT: "y \ T" by auto from ST xT yT have x: "x \ ?S" and y: "y \ ?S" and xy: "x \ y" by auto hence "abs (x - y) \ S" unfolding S_def root_cond_def[abs_def] by auto with fin have "Min S \ abs (x - y)" by auto with pos have le: "Min S / 2 \ abs (x - y) / 2" by auto from x y have "abs (x - y) \ of_rat r - of_rat l" unfolding root_cond_def[abs_def] by auto also have "\ = of_rat (r - l)" by (auto simp: of_rat_diff) finally have "abs (x - y) / 2 \ of_rat (r - l) / 2" by auto with le show "ipoly_root_delta p \ real_of_rat (r - l) / 4" unfolding delta by auto qed lemma sgn_less_eq_1_rat: fixes a b :: rat shows "sgn a = 1 \ a \ b \ sgn b = 1" by (metis (no_types, opaque_lifting) not_less one_neq_neg_one one_neq_zero order_trans sgn_rat_def) lemma sgn_less_eq_1_real: fixes a b :: real shows "sgn a = 1 \ a \ b \ sgn b = 1" by (metis (no_types, opaque_lifting) not_less one_neq_neg_one one_neq_zero order_trans sgn_real_def) definition compare_1_rat :: "real_alg_1 \ rat \ order" where "compare_1_rat rai = (let p = poly_real_alg_1 rai in if degree p = 1 then let x = Rat.Fract (- coeff p 0) (coeff p 1) in (\ y. compare y x) else (\ y. compare_rat_1 y rai))" lemma compare_real_of_rat: "compare (real_of_rat x) (of_rat y) = compare x y" unfolding compare_rat_def compare_real_def comparator_of_def of_rat_less by auto lemma compare_1_rat: assumes rc: "invariant_1 y" shows "compare_1_rat y x = compare (of_rat x) (real_of_1 y)" proof (cases "degree (poly_real_alg_1 y)" "Suc 0" rule: linorder_cases) case less with invariant_1_degree_0[OF rc] show ?thesis by auto next case deg: greater with rc have rc: "invariant_1_2 y" by auto from deg compare_rat_1[OF rc, of x] show ?thesis unfolding compare_1_rat_def by auto next case deg: equal obtain p l r where y: "y = (p,l,r)" by (cases y) note rc = invariant_1D[OF rc[unfolded y]] from deg have p: "degree p = Suc 0" and id: "compare_1_rat y x = compare x (Rat.Fract (- coeff p 0) (coeff p 1))" unfolding compare_1_rat_def by (auto simp: Let_def y) from rc(1)[unfolded split] have "ipoly p (real_of_1 y) = 0" unfolding y by auto with degree_1_ipoly[OF p, of "real_of_1 y"] have id': "real_of_1 y = real_of_rat (Rat.Fract (- coeff p 0) (coeff p 1))" by simp show ?thesis unfolding id id' compare_real_of_rat .. qed context fixes n :: nat begin private definition initial_lower_bound :: "rat \ rat" where "initial_lower_bound l = (if l \ 1 then l else of_int (root_rat_floor n l))" private definition initial_upper_bound :: "rat \ rat" where "initial_upper_bound r = (of_int (root_rat_ceiling n r))" context fixes cmpx :: "rat \ order" begin fun tighten_bound_root :: "rat \ rat \ rat \ rat" where "tighten_bound_root (l',r') = (let m' = (l' + r') / 2; m = m' ^ n in case cmpx m of Eq \ (m',m') | Lt \ (m',r') | Gt \ (l',m'))" lemma tighten_bound_root: assumes sgn: "sgn il = 1" "real_of_1 x \ 0" and il: "real_of_rat il \ root n (real_of_1 x)" and ir: "root n (real_of_1 x) \ real_of_rat ir" and rai: "invariant_1 x" and cmpx: "cmpx = compare_1_rat x" and n: "n \ 0" shows "converges_to (\ i. (tighten_bound_root ^^ i) (il, ir)) (root n (real_of_1 x))" (is "converges_to ?f ?x") unfolding converges_to_def proof (intro conjI impI allI) { fix x :: real have "x \ 0 \ (root n x) ^ n = x" using n by simp } note root_exp_cancel = this { fix x :: real have "x \ 0 \ root n (x ^ n) = x" using n using real_root_pos_unique by blast } note root_exp_cancel' = this from il ir have "real_of_rat il \ of_rat ir" by auto hence ir_il: "il \ ir" by (auto simp: of_rat_less_eq) from n have n': "n > 0" by auto { fix i have "in_interval (?f i) ?x \ sub_interval (?f i) (il,ir) \ (i \ 0 \ sub_interval (?f i) (?f (i - 1))) \ snd (?f i) - fst (?f i) \ (ir - il) / 2^i" proof (induct i) case 0 show ?case using il ir by auto next case (Suc i) obtain l' r' where id: "(tighten_bound_root ^^ i) (il, ir) = (l',r')" by (cases "(tighten_bound_root ^^ i) (il, ir)", auto) let ?m' = "(l' + r') / 2" let ?m = "?m' ^ n" define m where "m = ?m" note IH = Suc[unfolded id split snd_conv fst_conv] from IH have "sub_interval (l', r') (il, ir)" by auto hence ill': "il \ l'" "r' \ ir" by auto with sgn have l'0: "l' > 0" using sgn_1_pos sgn_less_eq_1_rat by blast from IH have lr'x: "in_interval (l', r') ?x" by auto hence lr'': "real_of_rat l' \ of_rat r'" by auto hence lr': "l' \ r'" unfolding of_rat_less_eq . with l'0 have r'0: "r' > 0" by auto note compare = compare_1_rat[OF rai, of ?m, folded cmpx] from IH have *: "r' - l' \ (ir - il) / 2 ^ i" by auto have "r' - (l' + r') / 2 = (r' - l') / 2" by (simp add: field_simps) also have "\ \ (ir - il) / 2 ^ i / 2" using * by (rule divide_right_mono, auto) finally have size: "r' - (l' + r') / 2 \ (ir - il) / (2 * 2 ^ i)" by simp also have "r' - (l' + r') / 2 = (l' + r') / 2 - l'" by auto finally have size': "(l' + r') / 2 - l' \ (ir - il) / (2 * 2 ^ i)" by simp have "root n (real_of_rat ?m) = root n ((real_of_rat ?m') ^ n)" by (simp add: hom_distribs) also have "\ = real_of_rat ?m'" by (rule root_exp_cancel', insert l'0 lr', auto) finally have root: "root n (of_rat ?m) = of_rat ?m'" . show ?case proof (cases "cmpx ?m") case Eq from compare[unfolded Eq] have "real_of_1 x = of_rat ?m" unfolding compare_real_def comparator_of_def by (auto split: if_splits) from arg_cong[OF this, of "root n"] have "?x = root n (of_rat ?m)" . also have "\ = root n (real_of_rat ?m') ^ n" using n real_root_power by (auto simp: hom_distribs) also have "\ = of_rat ?m'" by (rule root_exp_cancel, insert IH sgn(2) l'0 r'0, auto) finally have x: "?x = of_rat ?m'" . show ?thesis using x id Eq lr' ill' ir_il by (auto simp: Let_def) next case Lt from compare[unfolded Lt] have lt: "of_rat ?m \ real_of_1 x" unfolding compare_real_def comparator_of_def by (auto split: if_splits) have id'': "?f (Suc i) = (?m',r')" "?f (Suc i - 1) = (l',r')" using Lt id by (auto simp add: Let_def) from real_root_le_mono[OF n' lt] have "of_rat ?m' \ ?x" unfolding root by simp with lr'x lr'' have ineq': "real_of_rat l' + real_of_rat r' \ ?x * 2" by (auto simp: hom_distribs) show ?thesis unfolding id'' by (auto simp: Let_def hom_distribs, insert size ineq' lr' ill' lr'x ir_il, auto) next case Gt from compare[unfolded Gt] have lt: "of_rat ?m \ real_of_1 x" unfolding compare_real_def comparator_of_def by (auto split: if_splits) have id'': "?f (Suc i) = (l',?m')" "?f (Suc i - 1) = (l',r')" using Gt id by (auto simp add: Let_def) from real_root_le_mono[OF n' lt] have "?x \ of_rat ?m'" unfolding root by simp with lr'x lr'' have ineq': "?x * 2 \ real_of_rat l' + real_of_rat r'" by (auto simp: hom_distribs) show ?thesis unfolding id'' by (auto simp: Let_def hom_distribs, insert size' ineq' lr' ill' lr'x ir_il, auto) qed qed } note main = this fix i from main[of i] show "in_interval (?f i) ?x" by auto from main[of "Suc i"] show "sub_interval (?f (Suc i)) (?f i)" by auto fix eps :: real assume eps: "0 < eps" define c where "c = eps / (max (real_of_rat (ir - il)) 1)" have c0: "c > 0" using eps unfolding c_def by auto from exp_tends_to_zero[OF _ _ this, of "1/2"] obtain i where c: "(1/2)^i \ c" by auto obtain l' r' where fi: "?f i = (l',r')" by force from main[of i, unfolded fi] have le: "r' - l' \ (ir - il) / 2 ^ i" by auto have iril: "real_of_rat (ir - il) \ 0" using ir_il by (auto simp: of_rat_less_eq) show "\n la ra. ?f n = (la, ra) \ real_of_rat ra - real_of_rat la \ eps" proof (intro conjI exI, rule fi) have "real_of_rat r' - of_rat l' = real_of_rat (r' - l')" by (auto simp: hom_distribs) also have "\ \ real_of_rat ((ir - il) / 2 ^ i)" using le unfolding of_rat_less_eq . also have "\ = (real_of_rat (ir - il)) * ((1/2) ^ i)" by (simp add: field_simps hom_distribs) also have "\ \ (real_of_rat (ir - il)) * c" by (rule mult_left_mono[OF c iril]) also have "\ \ eps" proof (cases "real_of_rat (ir - il) \ 1") case True hence "c = eps" unfolding c_def by (auto simp: hom_distribs) thus ?thesis using eps True by auto next case False hence "max (real_of_rat (ir - il)) 1 = real_of_rat (ir - il)" "real_of_rat (ir - il) \ 0" by (auto simp: hom_distribs) hence "(real_of_rat (ir - il)) * c = eps" unfolding c_def by auto thus ?thesis by simp qed finally show "real_of_rat r' - of_rat l' \ eps" . qed qed end private fun root_pos_1 :: "real_alg_1 \ real_alg_2" where "root_pos_1 (p,l,r) = ( (select_correct_factor_int_poly (tighten_bound_root (compare_1_rat (p,l,r))) (\ x. x) (initial_lower_bound l, initial_upper_bound r) (poly_nth_root n p)))" fun root_1 :: "real_alg_1 \ real_alg_2" where "root_1 (p,l,r) = ( if n = 0 \ r = 0 then Rational 0 else if r > 0 then root_pos_1 (p,l,r) else uminus_2 (root_pos_1 (uminus_1 (p,l,r))))" context assumes n: "n \ 0" begin lemma initial_upper_bound: assumes x: "x > 0" and xr: "x \ of_rat r" shows "sgn (initial_upper_bound r) = 1" "root n x \ of_rat (initial_upper_bound r)" proof - have n: "n > 0" using n by auto note d = initial_upper_bound_def let ?r = "initial_upper_bound r" from x xr have r0: "r > 0" by (meson not_less of_rat_le_0_iff order_trans) hence "of_rat r > (0 :: real)" by auto hence "root n (of_rat r) > 0" using n by simp hence "1 \ ceiling (root n (of_rat r))" by auto hence "(1 :: rat) \ of_int (ceiling (root n (of_rat r)))" by linarith also have "\ = ?r" unfolding d by simp finally show "sgn ?r = 1" unfolding sgn_rat_def by auto have "root n x \ root n (of_rat r)" unfolding real_root_le_iff[OF n] by (rule xr) also have "\ \ of_rat ?r" unfolding d by simp finally show "root n x \ of_rat ?r" . qed lemma initial_lower_bound: assumes l: "l > 0" and lx: "of_rat l \ x" shows "sgn (initial_lower_bound l) = 1" "of_rat (initial_lower_bound l) \ root n x" proof - have n: "n > 0" using n by auto note d = initial_lower_bound_def let ?l = "initial_lower_bound l" from l lx have x0: "x > 0" by (meson not_less of_rat_le_0_iff order_trans) have "sgn ?l = 1 \ of_rat ?l \ root n x" proof (cases "l \ 1") case True hence ll: "?l = l" and l0: "of_rat l \ (0 :: real)" and l1: "of_rat l \ (1 :: real)" using l unfolding True d by auto have sgn: "sgn ?l = 1" using l unfolding ll by auto have "of_rat ?l = of_rat l" unfolding ll by simp also have "of_rat l \ root n (of_rat l)" using real_root_increasing[OF _ _ l0 l1, of 1 n] n by (cases "n = 1", auto) also have "\ \ root n x" using lx unfolding real_root_le_iff[OF n] . finally show ?thesis using sgn by auto next case False hence l: "(1 :: real) \ of_rat l" and ll: "?l = of_int (floor (root n (of_rat l)))" unfolding d by auto hence "root n 1 \ root n (of_rat l)" unfolding real_root_le_iff[OF n] by auto hence "1 \ root n (of_rat l)" using n by auto from floor_mono[OF this] have "1 \ ?l" using one_le_floor unfolding ll by fastforce hence sgn: "sgn ?l = 1" by simp have "of_rat ?l \ root n (of_rat l)" unfolding ll by simp also have "\ \ root n x" using lx unfolding real_root_le_iff[OF n] . finally have "of_rat ?l \ root n x" . with sgn show ?thesis by auto qed thus "sgn ?l = 1" "of_rat ?l \ root n x" by auto qed lemma root_pos_1: assumes x: "invariant_1 x" and pos: "rai_ub x > 0" defines y: "y \ root_pos_1 x" shows "invariant_2 y \ real_of_2 y = root n (real_of_1 x)" proof (cases x) case (fields p l r) let ?l = "initial_lower_bound l" let ?r = "initial_upper_bound r" from x fields have rai: "invariant_1 (p,l,r)" by auto note * = invariant_1D[OF this] let ?x = "the_unique_root (p,l,r)" from pos[unfolded fields] * have sgnl: "sgn l = 1" by auto from sgnl have l0: "l > 0" by (unfold sgn_1_pos) hence ll0: "real_of_rat l > 0" by auto from * have lx: "of_rat l \ ?x" by auto with ll0 have x0: "?x > 0" by linarith note il = initial_lower_bound[OF l0 lx] from * have "?x \ of_rat r" by auto note iu = initial_upper_bound[OF x0 this] let ?p = "poly_nth_root n p" from x0 have id: "root n ?x ^ n = ?x" using n real_root_pow_pos by blast have rc: "root_cond (?p, ?l, ?r) (root n ?x)" using il iu * by (intro root_condI, auto simp: ipoly_nth_root id) hence root: "ipoly ?p (root n (real_of_1 x)) = 0" unfolding root_cond_def fields by auto from * have "p \ 0" by auto hence p': "?p \ 0" using poly_nth_root_0[of n p] n by auto have tbr: "0 \ real_of_1 x" "real_of_rat (initial_lower_bound l) \ root n (real_of_1 x)" "root n (real_of_1 x) \ real_of_rat (initial_upper_bound r)" using x0 il(2) iu(2) fields by auto from select_correct_factor_int_poly[OF tighten_bound_root[OF il(1)[folded fields] tbr x refl n] refl root p'] show ?thesis by (simp add: y fields) qed end lemma root_1: assumes x: "invariant_1 x" defines y: "y \ root_1 x" shows "invariant_2 y \ (real_of_2 y = root n (real_of_1 x))" proof (cases "n = 0 \ rai_ub x = 0") case True with x have "n = 0 \ real_of_1 x = 0" by (cases x, auto) then have "root n (real_of_1 x) = 0" by auto then show ?thesis unfolding y root_1.simps using x by (cases x, auto) next case False with x have n: "n \ 0" and x0: "real_of_1 x \ 0" by (simp, cases x, auto) note rt = root_pos_1 show ?thesis proof (cases "rai_ub x" "0::rat" rule:linorder_cases) case greater with rt[OF n x this] n show ?thesis by (unfold y, cases x, simp) next case less let ?um = "uminus_1" let ?rt = "root_pos_1" from n less y x0 have y: "y = uminus_2 (?rt (?um x))" by (cases x, auto) from uminus_1[OF x] have umx: "invariant_1 (?um x)" and umx2: "real_of_1 (?um x) = - real_of_1 x" by auto with x less have "0 < rai_ub (uminus_1 x)" by (cases x, auto simp: uminus_1.simps Let_def) from rt[OF n umx this] umx2 have rumx: "invariant_2 (?rt (?um x))" and rumx2: "real_of_2 (?rt (?um x)) = root n (- real_of_1 x)" by auto from uminus_2[OF rumx] rumx2 y real_root_minus show ?thesis by auto next case equal with x0 x show ?thesis by (cases x, auto) qed qed end declare root_1.simps[simp del] (* ********************** *) subsubsection \Embedding of Rational Numbers\ definition of_rat_1 :: "rat \ real_alg_1" where "of_rat_1 x \ (poly_rat x,x,x)" lemma of_rat_1: shows "invariant_1 (of_rat_1 x)" and "real_of_1 (of_rat_1 x) = of_rat x" unfolding of_rat_1_def by (atomize(full), intro invariant_1_realI unique_rootI poly_condI, auto ) fun info_2 :: "real_alg_2 \ rat + int poly \ nat" where "info_2 (Rational x) = Inl x" | "info_2 (Irrational n (p,l,r)) = Inr (p,n)" lemma info_2_card: assumes rc: "invariant_2 x" shows "info_2 x = Inr (p,n) \ poly_cond p \ ipoly p (real_of_2 x) = 0 \ degree p \ 2 \ card (roots_below p (real_of_2 x)) = n" "info_2 x = Inl y \ real_of_2 x = of_rat y" proof (atomize(full), goal_cases) case 1 show ?case proof (cases x) case (Irrational m rai) then obtain q l r where x: "x = Irrational m (q,l,r)" by (cases rai, auto) show ?thesis proof (cases "q = p \ m = n") case False thus ?thesis using x by auto next case True with x have x: "x = Irrational n (p,l,r)" by auto from rc[unfolded x, simplified] have inv: "invariant_1_2 (p,l,r)" and n: "card (roots_below p (real_of_2 x)) = n" and 1: "degree p \ 1" by (auto simp: x) from inv have "degree p \ 0" unfolding irreducible_def by auto with 1 have "degree p \ 2" by linarith thus ?thesis unfolding n using inv x by (auto elim!: invariant_1E) qed qed auto qed lemma real_of_2_Irrational: "invariant_2 (Irrational n rai) \ real_of_2 (Irrational n rai) \ of_rat x" proof assume "invariant_2 (Irrational n rai)" and rat: "real_of_2 (Irrational n rai) = real_of_rat x" hence "real_of_1 rai \ \" "invariant_1_2 rai" by auto from invariant_1_2_of_rat[OF this(2)] rat show False by auto qed lemma info_2: assumes ix: "invariant_2 x" and iy: "invariant_2 y" shows "info_2 x = info_2 y \ real_of_2 x = real_of_2 y" proof (cases x) case x: (Irrational n1 rai1) note ix = ix[unfolded x] show ?thesis proof (cases y) case (Rational y) with real_of_2_Irrational[OF ix, of y] show ?thesis unfolding x by (cases rai1, auto) next case y: (Irrational n2 rai2) obtain p1 l1 r1 where rai1: "rai1 = (p1,l1,r1)" by (cases rai1) obtain p2 l2 r2 where rai2: "rai2 = (p2,l2,r2)" by (cases rai2) let ?rx = "the_unique_root (p1,l1,r1)" let ?ry = "the_unique_root (p2,l2,r2)" have id: "(info_2 x = info_2 y) = (p1 = p2 \ n1 = n2)" "(real_of_2 x = real_of_2 y) = (?rx = ?ry)" unfolding x y rai1 rai2 by auto from ix[unfolded x rai1] have ix: "invariant_1 (p1, l1, r1)" and deg1: "degree p1 > 1" and n1: "n1 = card (roots_below p1 ?rx)" by auto note Ix = invariant_1D[OF ix] from deg1 have p1_0: "p1 \ 0" by auto from iy[unfolded y rai2] have iy: "invariant_1 (p2, l2, r2)" and "degree p2 > 1" and n2: "n2 = card (roots_below p2 ?ry)" by auto note Iy = invariant_1D[OF iy] show ?thesis unfolding id proof assume eq: "?rx = ?ry" from Ix have algx: "p1 represents ?rx \ irreducible p1 \ lead_coeff p1 > 0" unfolding represents_def by auto from iy have algy: "p2 represents ?rx \ irreducible p2 \ lead_coeff p2 > 0" unfolding represents_def eq by (auto elim!: invariant_1E) from algx have "algebraic ?rx" unfolding algebraic_altdef_ipoly by auto note unique = algebraic_imp_represents_unique[OF this] with algx algy have id: "p2 = p1" by auto from eq id n1 n2 show "p1 = p2 \ n1 = n2" by auto next assume "p1 = p2 \ n1 = n2" hence id: "p1 = p2" "n1 = n2" by auto hence card: "card (roots_below p1 ?rx) = card (roots_below p1 ?ry)" unfolding n1 n2 by auto show "?rx = ?ry" proof (cases ?rx ?ry rule: linorder_cases) case less have "roots_below p1 ?rx = roots_below p1 ?ry" proof (intro card_subset_eq finite_subset[OF _ ipoly_roots_finite] card) from less show "roots_below p1 ?rx \ roots_below p1 ?ry" by auto qed (insert p1_0, auto) then show ?thesis using id less unique_rootD(3)[OF Iy(4)] by (auto simp: less_eq_real_def) next case equal then show ?thesis by (simp add: id) next case greater have "roots_below p1 ?ry = roots_below p1 ?rx" proof (intro card_subset_eq card[symmetric] finite_subset[OF _ ipoly_roots_finite[OF p1_0]]) from greater show "roots_below p1 ?ry \ roots_below p1 ?rx" by auto qed auto hence "roots_below p2 ?ry = roots_below p2 ?rx" unfolding id by auto thus ?thesis using id greater unique_rootD(3)[OF Ix(4)] by (auto simp: less_eq_real_def) qed qed qed next case x: (Rational x) show ?thesis proof (cases y) case (Rational y) thus ?thesis using x by auto next case y: (Irrational n rai) with real_of_2_Irrational[OF iy[unfolded y], of x] show ?thesis unfolding x by (cases rai, auto) qed qed lemma info_2_unique: "invariant_2 x \ invariant_2 y \ real_of_2 x = real_of_2 y \ info_2 x = info_2 y" using info_2 by blast lemma info_2_inj: "invariant_2 x \ invariant_2 y \ info_2 x = info_2 y \ real_of_2 x = real_of_2 y" using info_2 by blast context fixes cr1 cr2 :: "rat \ rat \ nat" begin partial_function (tailrec) compare_1 :: "int poly \ int poly \ rat \ rat \ rat \ rat \ rat \ rat \ order" where [code]: "compare_1 p1 p2 l1 r1 sr1 l2 r2 sr2 = (if r1 < l2 then Lt else if r2 < l1 then Gt else let (l1',r1',sr1') = tighten_poly_bounds p1 l1 r1 sr1; (l2',r2',sr2') = tighten_poly_bounds p2 l2 r2 sr2 in compare_1 p1 p2 l1' r1' sr1' l2' r2' sr2') " lemma compare_1: assumes ur1: "unique_root (p1,l1,r1)" and ur2: "unique_root (p2,l2,r2)" and pc: "poly_cond2 p1" "poly_cond2 p2" and diff: "the_unique_root (p1,l1,r1) \ the_unique_root (p2,l2,r2)" and sr: "sr1 = sgn (ipoly p1 r1)" "sr2 = sgn (ipoly p2 r2)" shows "compare_1 p1 p2 l1 r1 sr1 l2 r2 sr2 = compare (the_unique_root (p1,l1,r1)) (the_unique_root (p2,l2,r2))" proof - let ?r = real_of_rat { fix d x y assume d: "d = (r1 - l1) + (r2 - l2)" and xy: "x = the_unique_root (p1,l1,r1)" "y = the_unique_root (p2,l2,r2)" define delta where "delta = abs (x - y) / 4" have delta: "delta > 0" and diff: "x \ y" unfolding delta_def using diff xy by auto let ?rel' = "{(x, y). 0 \ y \ delta_gt delta x y}" let ?rel = "inv_image ?rel' ?r" have SN: "SN ?rel" by (rule SN_inv_image[OF delta_gt_SN[OF delta]]) from d ur1 ur2 have ?thesis unfolding xy[symmetric] using xy sr proof (induct d arbitrary: l1 r1 l2 r2 sr1 sr2 rule: SN_induct[OF SN]) case (1 d l1 r1 l2 r2) note IH = 1(1) note d = 1(2) note ur = 1(3-4) note xy = 1(5-6) note sr = 1(7-8) note simps = compare_1.simps[of p1 p2 l1 r1 sr1 l2 r2 sr2] note urx = unique_rootD[OF ur(1), folded xy] note ury = unique_rootD[OF ur(2), folded xy] show ?case (is "?l = _") proof (cases "r1 < l2") case True hence l: "?l = Lt" and lt: "?r r1 < ?r l2" unfolding simps of_rat_less by auto show ?thesis unfolding l using lt True urx(2) ury(1) by (auto simp: compare_real_def comparator_of_def) next case False note le = this show ?thesis proof (cases "r2 < l1") case True with le have l: "?l = Gt" and lt: "?r r2 < ?r l1" unfolding simps of_rat_less by auto show ?thesis unfolding l using lt True ury(2) urx(1) by (auto simp: compare_real_def comparator_of_def) next case False obtain l1' r1' sr1' where tb1: "tighten_poly_bounds p1 l1 r1 sr1 = (l1',r1',sr1')" by (cases rule: prod_cases3, auto) obtain l2' r2' sr2' where tb2: "tighten_poly_bounds p2 l2 r2 sr2 = (l2',r2',sr2')" by (cases rule: prod_cases3, auto) from False le tb1 tb2 have l: "?l = compare_1 p1 p2 l1' r1' sr1' l2' r2' sr2'" unfolding simps by auto from tighten_poly_bounds[OF tb1 ur(1) pc(1) sr(1)] have rc1: "root_cond (p1, l1', r1') (the_unique_root (p1, l1, r1))" and bnd1: "l1 \ l1'" "l1' \ r1'" "r1' \ r1" and d1: "r1' - l1' = (r1 - l1) / 2" and sr1: "sr1' = sgn (ipoly p1 r1')" by auto from pc have "p1 \ 0" "p2 \ 0" by auto from unique_root_sub_interval[OF ur(1) rc1 bnd1(1,3)] xy ur this have ur1: "unique_root (p1, l1', r1')" and x: "x = the_unique_root (p1, l1', r1')" by (auto intro!: the_unique_root_eqI) from tighten_poly_bounds[OF tb2 ur(2) pc(2) sr(2)] have rc2: "root_cond (p2, l2', r2') (the_unique_root (p2, l2, r2))" and bnd2: "l2 \ l2'" "l2' \ r2'" "r2' \ r2" and d2: "r2' - l2' = (r2 - l2) / 2" and sr2: "sr2' = sgn (ipoly p2 r2')" by auto from unique_root_sub_interval[OF ur(2) rc2 bnd2(1,3)] xy ur pc have ur2: "unique_root (p2, l2', r2')" and y: "y = the_unique_root (p2, l2', r2')" by auto define d' where "d' = d/2" have d': "d' = r1' - l1' + (r2' - l2')" unfolding d'_def d d1 d2 by (simp add: field_simps) have d'0: "d' \ 0" using bnd1 bnd2 unfolding d' by auto have dd: "d - d' = d/2" unfolding d'_def by simp have "abs (x - y) \ 2 * ?r d" proof (rule ccontr) assume "\ ?thesis" hence lt: "2 * ?r d < abs (x - y)" by auto have "r1 - l1 \ d" "r2 - l2 \ d" unfolding d using bnd1 bnd2 by auto from this[folded of_rat_less_eq[where 'a = real]] lt have "?r (r1 - l1) < abs (x - y) / 2" "?r (r2 - l2) < abs (x - y) / 2" and dd: "?r r1 - ?r l1 \ ?r d" "?r r2 - ?r l2 \ ?r d" by (auto simp: of_rat_diff) from le have "r1 \ l2" by auto hence r1l2: "?r r1 \ ?r l2" unfolding of_rat_less_eq by auto from False have "r2 \ l1" by auto hence r2l1: "?r r2 \ ?r l1" unfolding of_rat_less_eq by auto show False proof (cases "x \ y") case True from urx(1-2) dd(1) have "?r r1 \ x + ?r d" by auto with r1l2 have "?r l2 \ x + ?r d" by auto with True lt ury(2) dd(2) show False by auto next case False from ury(1-2) dd(2) have "?r r2 \ y + ?r d" by auto with r2l1 have "?r l1 \ y + ?r d" by auto with False lt urx(2) dd(1) show False by auto qed qed hence dd': "delta_gt delta (?r d) (?r d')" unfolding delta_gt_def delta_def using dd by (auto simp: hom_distribs) show ?thesis unfolding l by (rule IH[OF _ d' ur1 ur2 x y sr1 sr2], insert d'0 dd', auto) qed qed qed } thus ?thesis by auto qed end (* **************************************************************** *) fun real_alg_1 :: "real_alg_2 \ real_alg_1" where "real_alg_1 (Rational r) = of_rat_1 r" | "real_alg_1 (Irrational n rai) = rai" lemma real_alg_1: "real_of_1 (real_alg_1 x) = real_of_2 x" by (cases x, auto simp: of_rat_1) definition root_2 :: "nat \ real_alg_2 \ real_alg_2" where "root_2 n x = root_1 n (real_alg_1 x)" lemma root_2: assumes "invariant_2 x" shows "real_of_2 (root_2 n x) = root n (real_of_2 x)" "invariant_2 (root_2 n x)" proof (atomize(full), cases x, goal_cases) case (1 y) from of_rat_1[of y] root_1[of "of_rat_1 y" n] assms 1 real_alg_2 show ?case by (simp add: root_2_def) next case (2 i rai) from root_1[of rai n] assms 2 real_alg_2 show ?case by (auto simp: root_2_def) qed fun add_2 :: "real_alg_2 \ real_alg_2 \ real_alg_2" where "add_2 (Rational r) (Rational q) = Rational (r + q)" | "add_2 (Rational r) (Irrational n x) = Irrational n (add_rat_1 r x)" | "add_2 (Irrational n x) (Rational q) = Irrational n (add_rat_1 q x)" | "add_2 (Irrational n x) (Irrational m y) = add_1 x y" lemma add_2: assumes x: "invariant_2 x" and y: "invariant_2 y" shows "invariant_2 (add_2 x y)" (is ?g1) and "real_of_2 (add_2 x y) = real_of_2 x + real_of_2 y" (is ?g2) using assms add_rat_1 add_1 by (atomize (full), (cases x; cases y), auto simp: hom_distribs) fun mult_2 :: "real_alg_2 \ real_alg_2 \ real_alg_2" where "mult_2 (Rational r) (Rational q) = Rational (r * q)" | "mult_2 (Rational r) (Irrational n y) = mult_rat_1 r y" | "mult_2 (Irrational n x) (Rational q) = mult_rat_1 q x" | "mult_2 (Irrational n x) (Irrational m y) = mult_1 x y" lemma mult_2: assumes "invariant_2 x" "invariant_2 y" shows "real_of_2 (mult_2 x y) = real_of_2 x * real_of_2 y" "invariant_2 (mult_2 x y)" using assms by (atomize(full), (cases x; cases y; auto simp: mult_rat_1 mult_1 hom_distribs)) fun to_rat_2 :: "real_alg_2 \ rat option" where "to_rat_2 (Rational r) = Some r" | "to_rat_2 (Irrational n rai) = None" lemma to_rat_2: assumes rc: "invariant_2 x" shows "to_rat_2 x = (if real_of_2 x \ \ then Some (THE q. real_of_2 x = of_rat q) else None)" proof (cases x) case (Irrational n rai) from real_of_2_Irrational[OF rc[unfolded this]] show ?thesis unfolding Irrational Rats_def by auto qed simp fun equal_2 :: "real_alg_2 \ real_alg_2 \ bool" where "equal_2 (Rational r) (Rational q) = (r = q)" | "equal_2 (Irrational n (p,_)) (Irrational m (q,_)) = (p = q \ n = m)" | "equal_2 (Rational r) (Irrational _ yy) = False" | "equal_2 (Irrational _ xx) (Rational q) = False" lemma equal_2[simp]: assumes rc: "invariant_2 x" "invariant_2 y" shows "equal_2 x y = (real_of_2 x = real_of_2 y)" using info_2[OF rc] by (cases x; cases y, auto) fun compare_2 :: "real_alg_2 \ real_alg_2 \ order" where "compare_2 (Rational r) (Rational q) = (compare r q)" | "compare_2 (Irrational n (p,l,r)) (Irrational m (q,l',r')) = (if p = q \ n = m then Eq else compare_1 p q l r (sgn (ipoly p r)) l' r' (sgn (ipoly q r')))" | "compare_2 (Rational r) (Irrational _ xx) = (compare_rat_1 r xx)" | "compare_2 (Irrational _ xx) (Rational r) = (invert_order (compare_rat_1 r xx))" lemma compare_2: assumes rc: "invariant_2 x" "invariant_2 y" shows "compare_2 x y = compare (real_of_2 x) (real_of_2 y)" proof (cases x) case (Rational r) note xx = this show ?thesis proof (cases y) case (Rational q) note yy = this show ?thesis unfolding xx yy by (simp add: compare_rat_def compare_real_def comparator_of_def of_rat_less) next case (Irrational n yy) note yy = this from compare_rat_1 rc show ?thesis unfolding xx yy by (simp add: of_rat_1) qed next case (Irrational n xx) note xx = this show ?thesis proof (cases y) case (Rational q) note yy = this from compare_rat_1 rc show ?thesis unfolding xx yy by simp next case (Irrational m yy) note yy = this obtain p l r where xxx: "xx = (p,l,r)" by (cases xx) obtain q l' r' where yyy: "yy = (q,l',r')" by (cases yy) note rc = rc[unfolded xx xxx yy yyy] from rc have I: "invariant_1_2 (p,l,r)" "invariant_1_2 (q,l',r')" by auto then have "unique_root (p,l,r)" "unique_root (q,l',r')" "poly_cond2 p" "poly_cond2 q" by auto from compare_1[OF this _ refl refl] show ?thesis using equal_2[OF rc] unfolding xx xxx yy yyy by simp qed qed fun sgn_2 :: "real_alg_2 \ rat" where "sgn_2 (Rational r) = sgn r" | "sgn_2 (Irrational n rai) = sgn_1 rai" lemma sgn_2: "invariant_2 x \ real_of_rat (sgn_2 x) = sgn (real_of_2 x)" using sgn_1 by (cases x, auto simp: real_of_rat_sgn) fun floor_2 :: "real_alg_2 \ int" where "floor_2 (Rational r) = floor r" | "floor_2 (Irrational n rai) = floor_1 rai" lemma floor_2: "invariant_2 x \ floor_2 x = floor (real_of_2 x)" by (cases x, auto simp: floor_1) (* *************** *) subsubsection \Definitions and Algorithms on Type with Invariant\ lift_definition of_rat_3 :: "rat \ real_alg_3" is of_rat_2 by (auto simp: of_rat_2) lemma of_rat_3: "real_of_3 (of_rat_3 x) = of_rat x" by (transfer, auto simp: of_rat_2) lift_definition root_3 :: "nat \ real_alg_3 \ real_alg_3" is root_2 by (auto simp: root_2) lemma root_3: "real_of_3 (root_3 n x) = root n (real_of_3 x)" by (transfer, auto simp: root_2) lift_definition equal_3 :: "real_alg_3 \ real_alg_3 \ bool" is equal_2 . lemma equal_3: "equal_3 x y = (real_of_3 x = real_of_3 y)" by (transfer, auto) lift_definition compare_3 :: "real_alg_3 \ real_alg_3 \ order" is compare_2 . lemma compare_3: "compare_3 x y = (compare (real_of_3 x) (real_of_3 y))" by (transfer, auto simp: compare_2) lift_definition add_3 :: "real_alg_3 \ real_alg_3 \ real_alg_3" is add_2 by (auto simp: add_2) lemma add_3: "real_of_3 (add_3 x y) = real_of_3 x + real_of_3 y" by (transfer, auto simp: add_2) lift_definition mult_3 :: "real_alg_3 \ real_alg_3 \ real_alg_3" is mult_2 by (auto simp: mult_2) lemma mult_3: "real_of_3 (mult_3 x y) = real_of_3 x * real_of_3 y" by (transfer, auto simp: mult_2) lift_definition sgn_3 :: "real_alg_3 \ rat" is sgn_2 . lemma sgn_3: "real_of_rat (sgn_3 x) = sgn (real_of_3 x)" by (transfer, auto simp: sgn_2) lift_definition to_rat_3 :: "real_alg_3 \ rat option" is to_rat_2 . lemma to_rat_3: "to_rat_3 x = (if real_of_3 x \ \ then Some (THE q. real_of_3 x = of_rat q) else None)" by (transfer, simp add: to_rat_2) lift_definition floor_3 :: "real_alg_3 \ int" is floor_2 . lemma floor_3: "floor_3 x = floor (real_of_3 x)" by (transfer, auto simp: floor_2) (* *************** *) (* info *) lift_definition info_3 :: "real_alg_3 \ rat + int poly \ nat" is info_2 . lemma info_3_fun: "real_of_3 x = real_of_3 y \ info_3 x = info_3 y" by (transfer, intro info_2_unique, auto) lift_definition info_real_alg :: "real_alg \ rat + int poly \ nat" is info_3 by (metis info_3_fun) lemma info_real_alg: "info_real_alg x = Inr (p,n) \ p represents (real_of x) \ card {y. y \ real_of x \ ipoly p y = 0} = n \ irreducible p" "info_real_alg x = Inl q \ real_of x = of_rat q" proof (atomize(full), transfer, transfer, goal_cases) case (1 x p n q) from 1 have x: "invariant_2 x" by auto note info = info_2_card[OF this] show ?case proof (cases x) case irr: (Irrational m rai) from info(1)[of p n] show ?thesis unfolding irr by (cases rai, auto simp: poly_cond_def) qed (insert 1 info, auto) qed (* add *) instantiation real_alg :: plus begin lift_definition plus_real_alg :: "real_alg \ real_alg \ real_alg" is add_3 by (simp add: add_3) instance .. end lemma plus_real_alg: "(real_of x) + (real_of y) = real_of (x + y)" by (transfer, rule add_3[symmetric]) (* minus *) instantiation real_alg :: minus begin definition minus_real_alg :: "real_alg \ real_alg \ real_alg" where "minus_real_alg x y = x + (-y)" instance .. end lemma minus_real_alg: "(real_of x) - (real_of y) = real_of (x - y)" unfolding minus_real_alg_def minus_real_def uminus_real_alg plus_real_alg .. (* of_rat *) lift_definition of_rat_real_alg :: "rat \ real_alg" is of_rat_3 . lemma of_rat_real_alg: "real_of_rat x = real_of (of_rat_real_alg x)" by (transfer, rule of_rat_3[symmetric]) (* zero *) instantiation real_alg :: zero begin definition zero_real_alg :: "real_alg" where "zero_real_alg \ of_rat_real_alg 0" instance .. end lemma zero_real_alg: "0 = real_of 0" unfolding zero_real_alg_def by (simp add: of_rat_real_alg[symmetric]) (* one *) instantiation real_alg :: one begin definition one_real_alg :: "real_alg" where "one_real_alg \ of_rat_real_alg 1" instance .. end lemma one_real_alg: "1 = real_of 1" unfolding one_real_alg_def by (simp add: of_rat_real_alg[symmetric]) (* times *) instantiation real_alg :: times begin lift_definition times_real_alg :: "real_alg \ real_alg \ real_alg" is mult_3 by (simp add: mult_3) instance .. end lemma times_real_alg: "(real_of x) * (real_of y) = real_of (x * y)" by (transfer, rule mult_3[symmetric]) (* inverse *) instantiation real_alg :: inverse begin lift_definition inverse_real_alg :: "real_alg \ real_alg" is inverse_3 by (simp add: inverse_3) definition divide_real_alg :: "real_alg \ real_alg \ real_alg" where "divide_real_alg x y = x * inverse y" (* TODO: better to use poly_div *) instance .. end lemma inverse_real_alg: "inverse (real_of x) = real_of (inverse x)" by (transfer, rule inverse_3[symmetric]) lemma divide_real_alg: "(real_of x) / (real_of y) = real_of (x / y)" unfolding divide_real_alg_def times_real_alg[symmetric] divide_real_def inverse_real_alg .. (* group *) instance real_alg :: ab_group_add apply intro_classes apply (transfer, unfold add_3, force) apply (unfold zero_real_alg_def, transfer, unfold add_3 of_rat_3, force) apply (transfer, unfold add_3 of_rat_3, force) apply (transfer, unfold add_3 uminus_3 of_rat_3, force) apply (unfold minus_real_alg_def, force) done (* field *) instance real_alg :: field apply intro_classes apply (transfer, unfold mult_3, force) apply (transfer, unfold mult_3, force) apply (unfold one_real_alg_def, transfer, unfold mult_3 of_rat_3, force) apply (transfer, unfold mult_3 add_3, force simp: field_simps) apply (unfold zero_real_alg_def, transfer, unfold of_rat_3, force) apply (transfer, unfold mult_3 inverse_3 of_rat_3, force simp: field_simps) apply (unfold divide_real_alg_def, force) apply (transfer, unfold inverse_3 of_rat_3, force) done (* numeral *) instance real_alg :: numeral .. (* root *) lift_definition root_real_alg :: "nat \ real_alg \ real_alg" is root_3 by (simp add: root_3) lemma root_real_alg: "root n (real_of x) = real_of (root_real_alg n x)" by (transfer, rule root_3[symmetric]) (* sgn *) lift_definition sgn_real_alg_rat :: "real_alg \ rat" is sgn_3 by (insert sgn_3, metis to_rat_of_rat) lemma sgn_real_alg_rat: "real_of_rat (sgn_real_alg_rat x) = sgn (real_of x)" by (transfer, auto simp: sgn_3) instantiation real_alg :: sgn begin definition sgn_real_alg :: "real_alg \ real_alg" where "sgn_real_alg x = of_rat_real_alg (sgn_real_alg_rat x)" instance .. end lemma sgn_real_alg: "sgn (real_of x) = real_of (sgn x)" unfolding sgn_real_alg_def of_rat_real_alg[symmetric] by (transfer, simp add: sgn_3) (* equal *) instantiation real_alg :: equal begin lift_definition equal_real_alg :: "real_alg \ real_alg \ bool" is equal_3 by (simp add: equal_3) instance proof fix x y :: real_alg show "equal_class.equal x y = (x = y)" by (transfer, simp add: equal_3) qed end lemma equal_real_alg: "HOL.equal (real_of x) (real_of y) = (x = y)" unfolding equal_real_def by (transfer, auto) (* comparisons *) instantiation real_alg :: ord begin definition less_real_alg :: "real_alg \ real_alg \ bool" where [code del]: "less_real_alg x y = (real_of x < real_of y)" definition less_eq_real_alg :: "real_alg \ real_alg \ bool" where [code del]: "less_eq_real_alg x y = (real_of x \ real_of y)" instance .. end lemma less_real_alg: "less (real_of x) (real_of y) = (x < y)" unfolding less_real_alg_def .. lemma less_eq_real_alg: "less_eq (real_of x) (real_of y) = (x \ y)" unfolding less_eq_real_alg_def .. instantiation real_alg :: compare_order begin lift_definition compare_real_alg :: "real_alg \ real_alg \ order" is compare_3 by (simp add: compare_3) lemma compare_real_alg: "compare (real_of x) (real_of y) = (compare x y)" by (transfer, simp add: compare_3) instance proof (intro_classes, unfold compare_real_alg[symmetric, abs_def]) show "le_of_comp (\x y. compare (real_of x) (real_of y)) = (\)" by (intro ext, auto simp: compare_real_def comparator_of_def le_of_comp_def less_eq_real_alg_def) show "lt_of_comp (\x y. compare (real_of x) (real_of y)) = (<)" by (intro ext, auto simp: compare_real_def comparator_of_def lt_of_comp_def less_real_alg_def) show "comparator (\x y. compare (real_of x) (real_of y))" unfolding comparator_def proof (intro conjI impI allI) fix x y z :: "real_alg" let ?r = real_of note rc = comparator_compare[where 'a = real, unfolded comparator_def] from rc show "invert_order (compare (?r x) (?r y)) = compare (?r y) (?r x)" by blast from rc show "compare (?r x) (?r y) = Lt \ compare (?r y) (?r z) = Lt \ compare (?r x) (?r z) = Lt" by blast assume "compare (?r x) (?r y) = Eq" with rc have "?r x = ?r y" by blast thus "x = y" unfolding real_of_inj . qed qed end lemma less_eq_real_alg_code[code]: "(less_eq :: real_alg \ real_alg \ bool) = le_of_comp compare" "(less :: real_alg \ real_alg \ bool) = lt_of_comp compare" by (rule ord_defs(1)[symmetric], rule ord_defs(2)[symmetric]) instantiation real_alg :: abs begin definition abs_real_alg :: "real_alg \ real_alg" where "abs_real_alg x = (if real_of x < 0 then uminus x else x)" instance .. end lemma abs_real_alg: "abs (real_of x) = real_of (abs x)" unfolding abs_real_alg_def abs_real_def if_distrib by (auto simp: uminus_real_alg) lemma sgn_real_alg_sound: "sgn x = (if x = 0 then 0 else if 0 < real_of x then 1 else - 1)" (is "_ = ?r") proof - have "real_of (sgn x) = sgn (real_of x)" by (simp add: sgn_real_alg) also have "\ = real_of ?r" unfolding sgn_real_def if_distrib by (auto simp: less_real_alg_def zero_real_alg_def one_real_alg_def of_rat_real_alg[symmetric] equal_real_alg[symmetric] equal_real_def uminus_real_alg[symmetric]) finally show "sgn x = ?r" unfolding equal_real_alg[symmetric] equal_real_def by simp qed lemma real_of_of_int: "real_of_rat (rat_of_int z) = real_of (of_int z)" proof (cases "z \ 0") case True define n where "n = nat z" from True have z: "z = int n" unfolding n_def by simp show ?thesis unfolding z by (induct n, auto simp: zero_real_alg plus_real_alg[symmetric] one_real_alg hom_distribs) next case False define n where "n = nat (-z)" from False have z: "z = - int n" unfolding n_def by simp show ?thesis unfolding z by (induct n, auto simp: zero_real_alg plus_real_alg[symmetric] one_real_alg uminus_real_alg[symmetric] minus_real_alg[symmetric] hom_distribs) qed instance real_alg :: linordered_field apply standard apply (unfold less_eq_real_alg_def plus_real_alg[symmetric], force) apply (unfold abs_real_alg_def less_real_alg_def zero_real_alg[symmetric], rule refl) apply (unfold less_real_alg_def times_real_alg[symmetric], force) apply (rule sgn_real_alg_sound) done instantiation real_alg :: floor_ceiling begin lift_definition floor_real_alg :: "real_alg \ int" is floor_3 by (auto simp: floor_3) lemma floor_real_alg: "floor (real_of x) = floor x" by (transfer, auto simp: floor_3) instance proof fix x :: real_alg show "of_int \x\ \ x \ x < of_int (\x\ + 1)" unfolding floor_real_alg[symmetric] using floor_correct[of "real_of x"] unfolding less_eq_real_alg_def less_real_alg_def real_of_of_int[symmetric] by (auto simp: hom_distribs) hence "x \ of_int (\x\ + 1)" by auto thus "\z. x \ of_int z" by blast qed end instantiation real_alg :: "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}" begin definition [simp]: "normalize_real_alg = (normalize_field :: real_alg \ _)" definition [simp]: "unit_factor_real_alg = (unit_factor_field :: real_alg \ _)" definition [simp]: "modulo_real_alg = (mod_field :: real_alg \ _)" definition [simp]: "euclidean_size_real_alg = (euclidean_size_field :: real_alg \ _)" definition [simp]: "division_segment (x :: real_alg) = 1" instance by standard (simp_all add: dvd_field_iff field_split_simps split: if_splits) end instantiation real_alg :: euclidean_ring_gcd begin definition gcd_real_alg :: "real_alg \ real_alg \ real_alg" where "gcd_real_alg = Euclidean_Algorithm.gcd" definition lcm_real_alg :: "real_alg \ real_alg \ real_alg" where "lcm_real_alg = Euclidean_Algorithm.lcm" definition Gcd_real_alg :: "real_alg set \ real_alg" where "Gcd_real_alg = Euclidean_Algorithm.Gcd" definition Lcm_real_alg :: "real_alg set \ real_alg" where "Lcm_real_alg = Euclidean_Algorithm.Lcm" instance by standard (simp_all add: gcd_real_alg_def lcm_real_alg_def Gcd_real_alg_def Lcm_real_alg_def) end instance real_alg :: field_gcd .. definition min_int_poly_real_alg :: "real_alg \ int poly" where "min_int_poly_real_alg x = (case info_real_alg x of Inl r \ poly_rat r | Inr (p,_) \ p)" lemma min_int_poly_real_alg_real_of: "min_int_poly_real_alg x = min_int_poly (real_of x)" proof (cases "info_real_alg x") case (Inl r) show ?thesis unfolding info_real_alg(2)[OF Inl] min_int_poly_real_alg_def Inl by (simp add: min_int_poly_of_rat) next case (Inr pair) then obtain p n where Inr: "info_real_alg x = Inr (p,n)" by (cases pair, auto) hence "poly_cond p" by (transfer, transfer, auto simp: info_2_card) hence "min_int_poly (real_of x) = p" using info_real_alg(1)[OF Inr] by (intro min_int_poly_unique, auto) thus ?thesis unfolding min_int_poly_real_alg_def Inr by simp qed lemma min_int_poly_real_code: "min_int_poly_real (real_of x) = min_int_poly_real_alg x" by (simp add: min_int_poly_real_alg_real_of) lemma min_int_poly_real_of: "min_int_poly (real_of x) = min_int_poly x" proof (rule min_int_poly_unique[OF _ min_int_poly_irreducible lead_coeff_min_int_poly_pos]) show "min_int_poly x represents real_of x" oops (* TODO: this gives an implementation of min-int-poly on type real-alg qed lemma min_int_poly_real_alg_code_unfold [code_unfold]: "min_int_poly = min_int_poly_real_alg" by (intro ext, unfold min_int_poly_real_alg_real_of, simp add: min_int_poly_real_of) *) definition real_alg_of_real :: "real \ real_alg" where "real_alg_of_real x = (if (\ y. x = real_of y) then (THE y. x = real_of y) else 0)" lemma real_alg_of_real_code[code]: "real_alg_of_real (real_of x) = x" using real_of_inj unfolding real_alg_of_real_def by auto lift_definition to_rat_real_alg_main :: "real_alg \ rat option" is to_rat_3 by (simp add: to_rat_3) lemma to_rat_real_alg_main: "to_rat_real_alg_main x = (if real_of x \ \ then Some (THE q. real_of x = of_rat q) else None)" by (transfer, simp add: to_rat_3) definition to_rat_real_alg :: "real_alg \ rat" where "to_rat_real_alg x = (case to_rat_real_alg_main x of Some q \ q | None \ 0)" definition is_rat_real_alg :: "real_alg \ bool" where "is_rat_real_alg x = (case to_rat_real_alg_main x of Some q \ True | None \ False)" lemma is_rat_real_alg: "is_rat (real_of x) = (is_rat_real_alg x)" unfolding is_rat_real_alg_def is_rat to_rat_real_alg_main by auto lemma to_rat_real_alg: "to_rat (real_of x) = (to_rat_real_alg x)" unfolding to_rat to_rat_real_alg_def to_rat_real_alg_main by auto - -definition algebraic_real :: "real \ bool" where - [simp]: "algebraic_real = algebraic" - -lemma algebraic_real_iff[code_unfold]: "algebraic = algebraic_real" by simp - lemma algebraic_real_code[code]: "algebraic_real (real_of x) = True" proof (cases "info_real_alg x") case (Inl r) show ?thesis using info_real_alg(2)[OF Inl] by (auto simp: algebraic_of_rat) next case (Inr pair) then obtain p n where Inr: "info_real_alg x = Inr (p,n)" by (cases pair, auto) from info_real_alg(1)[OF Inr] have "p represents (real_of x)" by auto thus ?thesis by (auto simp: algebraic_altdef_ipoly) qed subsection \Real Algebraic Numbers as Implementation for Real Numbers\ lemmas real_alg_code_eqns = one_real_alg zero_real_alg uminus_real_alg root_real_alg minus_real_alg plus_real_alg times_real_alg inverse_real_alg divide_real_alg equal_real_alg less_real_alg less_eq_real_alg compare_real_alg sgn_real_alg abs_real_alg floor_real_alg is_rat_real_alg to_rat_real_alg min_int_poly_real_code code_datatype real_of declare [[code drop: "plus :: real \ real \ real" "uminus :: real \ real" "minus :: real \ real \ real" "times :: real \ real \ real" "inverse :: real \ real" "divide :: real \ real \ real" "floor :: real \ int" "HOL.equal :: real \ real \ bool" "compare :: real \ real \ order" "less_eq :: real \ real \ bool" "less :: real \ real \ bool" "0 :: real" "1 :: real" "sgn :: real \ real" "abs :: real \ real" min_int_poly_real root]] declare real_alg_code_eqns [code equation] lemma Ratreal_code[code]: "Ratreal = real_of \ of_rat_real_alg" by (transfer, transfer) (simp add: fun_eq_iff of_rat_2) lemma real_of_post[code_post]: "real_of (Real_Alg_Quotient (Real_Alg_Invariant (Rational x))) = of_rat x" proof (transfer) fix x show "real_of_3 (Real_Alg_Invariant (Rational x)) = real_of_rat x" by (simp add: Real_Alg_Invariant_inverse real_of_3.rep_eq) qed end diff --git a/thys/Algebraic_Numbers/Real_Roots.thy b/thys/Algebraic_Numbers/Real_Roots.thy --- a/thys/Algebraic_Numbers/Real_Roots.thy +++ b/thys/Algebraic_Numbers/Real_Roots.thy @@ -1,595 +1,432 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) section \Real Roots\ text \This theory contains an algorithm to determine the set of real roots of a rational polynomial. For polynomials with real coefficients, we refer to the AFP entry "Factor-Algebraic-Polynomial".\ theory Real_Roots -imports - Real_Algebraic_Numbers + imports + Cauchy_Root_Bound + Real_Algebraic_Numbers begin hide_const (open) UnivPoly.coeff hide_const (open) Module.smult - -text \Division of integers, rounding to the upper value.\ -definition div_ceiling :: "int \ int \ int" where - "div_ceiling x y = (let q = x div y in if q * y = x then q else q + 1)" - -definition root_bound :: "int poly \ rat" where - "root_bound p \ let - n = degree p; - m = 1 + div_ceiling (max_list_non_empty (map (\i. abs (coeff p i)) [0.. \round to the next higher number \2^n\, so that bisection will\ - \ \stay on integers for as long as possible\ - in of_int (2 ^ (log_ceiling 2 m))" partial_function (tailrec) roots_of_2_main :: "int poly \ root_info \ (rat \ rat \ nat) \ (rat \ rat)list \ real_alg_2 list \ real_alg_2 list" where [code]: "roots_of_2_main p ri cr lrs rais = (case lrs of Nil \ rais | (l,r) # lrs \ let c = cr l r in if c = 0 then roots_of_2_main p ri cr lrs rais else if c = 1 then roots_of_2_main p ri cr lrs (real_alg_2'' ri p l r # rais) else let m = (l + r) / 2 in roots_of_2_main p ri cr ((m,r) # (l,m) # lrs) rais)" definition roots_of_2_irr :: "int poly \ real_alg_2 list" where "roots_of_2_irr p = (if degree p = 1 then [Rational (Rat.Fract (- coeff p 0) (coeff p 1)) ] else let ri = root_info p; cr = root_info.l_r ri; B = root_bound p in (roots_of_2_main p ri cr [(-B,B)] []))" - -lemma root_imp_deg_nonzero: assumes "p \ 0" "poly p x = 0" - shows "degree p \ 0" -proof - assume "degree p = 0" - from degree0_coeffs[OF this] assms show False by auto -qed - -lemma cauchy_root_bound: fixes x :: "'a :: real_normed_field" - assumes x: "poly p x = 0" and p: "p \ 0" - shows "norm x \ 1 + max_list_non_empty (map (\ i. norm (coeff p i)) [0 ..< degree p]) - / norm (lead_coeff p)" (is "_ \ _ + ?max / ?nlc") -proof - - let ?n = "degree p" - let ?p = "coeff p" - let ?lc = "lead_coeff p" - define ml where "ml = ?max / ?nlc" - from p have lc: "?lc \ 0" by auto - hence nlc: "norm ?lc > 0" by auto - from root_imp_deg_nonzero[OF p x] have *: "0 \ set [0 ..< degree p]" by auto - have "0 \ norm (?p 0)" by simp - also have "\ \ ?max" - by (rule max_list_non_empty, insert *, auto) - finally have max0: "?max \ 0" . - with nlc have ml0: "ml \ 0" unfolding ml_def by auto - hence easy: "norm x \ 1 \ ?thesis" unfolding ml_def[symmetric] by auto - show ?thesis - proof (cases "norm x \ 1") - case True - thus ?thesis using easy by auto - next - case False - hence nx: "norm x > 1" by simp - hence x0: "x \ 0" by auto - hence xn0: "0 < norm x ^ ?n" by auto - from x[unfolded poly_altdef] have "x ^ ?n * ?lc = x ^ ?n * ?lc - (\i\?n. x ^ i * ?p i)" - unfolding poly_altdef by (simp add: ac_simps) - also have "(\i\?n. x ^ i * ?p i) = x ^ ?n * ?lc + (\i < ?n. x ^ i * ?p i)" - by (subst sum.remove[of _ ?n], auto intro: sum.cong) - finally have "x ^ ?n * ?lc = - (\i < ?n. x ^ i * ?p i)" by simp - with lc have "x ^ ?n = - (\i < ?n. x ^ i * ?p i) / ?lc" by (simp add: field_simps) - from arg_cong[OF this, of norm] - have "norm x ^ ?n = norm ((\i < ?n. x ^ i * ?p i) / ?lc)" unfolding norm_power by simp - also have "(\i < ?n. x ^ i * ?p i) / ?lc = (\i < ?n. x ^ i * ?p i / ?lc)" - by (rule sum_divide_distrib) - also have "norm \ \ (\i < ?n. norm (x ^ i * (?p i / ?lc)))" - by (simp add: field_simps, rule norm_sum) - also have "\ = (\i < ?n. norm x ^ i * norm (?p i / ?lc))" - unfolding norm_mult norm_power .. - also have "\ \ (\i < ?n. norm x ^ i * ml)" - proof (rule sum_mono) - fix i - assume "i \ {.. norm x ^ i * ml" - proof (rule mult_left_mono) - show "0 \ norm x ^ i" using nx by auto - show "norm (?p i / ?lc) \ ml" unfolding norm_divide ml_def - by (rule divide_right_mono[OF max_list_non_empty], insert nlc i, auto) - qed - qed - also have "\ = ml * (\i < ?n. norm x ^ i)" - unfolding sum_distrib_right[symmetric] by simp - also have "(\i < ?n. norm x ^ i) = (norm x ^ ?n - 1) / (norm x - 1)" - by (rule geometric_sum, insert nx, auto) - finally have "norm x ^ ?n \ ml * (norm x ^ ?n - 1) / (norm x - 1)" by simp - from mult_left_mono[OF this, of "norm x - 1"] - have "(norm x - 1) * (norm x ^ ?n) \ ml * (norm x ^ ?n - 1)" using nx by auto - also have "\ = (ml * (1 - 1 / (norm x ^ ?n))) * norm x ^ ?n" - using nx False x0 by (simp add: field_simps) - finally have "(norm x - 1) * (norm x ^ ?n) \ (ml * (1 - 1 / (norm x ^ ?n))) * norm x ^ ?n" . - from mult_right_le_imp_le[OF this xn0] - have "norm x - 1 \ ml * (1 - 1 / (norm x ^ ?n))" by simp - hence "norm x \ 1 + ml - ml / (norm x ^ ?n)" by (simp add: field_simps) - also have "\ \ 1 + ml" using ml0 xn0 by auto - finally show ?thesis unfolding ml_def . - qed -qed - -lemma div_le_div_ceiling: "x div y \ div_ceiling x y" - unfolding div_ceiling_def Let_def by auto -lemma div_ceiling: assumes q: "q \ 0" - shows "(of_int x :: 'a :: floor_ceiling) / of_int q \ of_int (div_ceiling x q)" -proof (cases "q dvd x") - case True - then obtain k where xqk: "x = q * k" unfolding dvd_def by auto - hence id: "div_ceiling x q = k" unfolding div_ceiling_def Let_def using q by auto - show ?thesis unfolding id unfolding xqk using q by simp -next - case False - { - assume "x div q * q = x" - hence "x = q * (x div q)" by (simp add: ac_simps) - hence "q dvd x" unfolding dvd_def by auto - with False have False by simp - } - hence id: "div_ceiling x q = x div q + 1" - unfolding div_ceiling_def Let_def using q by auto - show ?thesis unfolding id - by (metis floor_divide_of_int_eq le_less add1_zle_eq floor_less_iff) -qed - -lemma max_list_non_empty_map: assumes hom: "\ x y. max (f x) (f y) = f (max x y)" - shows "xs \ [] \ max_list_non_empty (map f xs) = f (max_list_non_empty xs)" - by (induct xs rule: max_list_non_empty.induct, auto simp: hom) - -lemma root_bound: assumes "root_bound p = B" and deg: "degree p > 0" - shows "ipoly p (x :: real) = 0 \ norm x \ of_rat B" "B \ 0" -proof - - let ?r = real_of_rat - let ?i = real_of_int - let ?p = "real_of_int_poly p" - define n where "n = degree p" - let ?lc = "coeff p n" - let ?list = "map (\i. abs (coeff p i)) [0.. 0" by auto - from p0 have alc0: "abs ?lc \ 0" unfolding n_def by auto - from deg have mem: "abs (coeff p 0) \ set ?list" unfolding n_def by auto - from max_list_non_empty[OF this, folded m_def] - have m0: "m \ 0" by auto - have "div_ceiling m (abs ?lc) \ 0" - by (rule order_trans[OF _ div_le_div_ceiling[of m "abs ?lc"]], subst - pos_imp_zdiv_nonneg_iff, insert p0 m0, auto simp: n_def) - hence mup: "m_up \ 1" unfolding m_up_def by auto - have "m_up \ 2 ^ (log_ceiling 2 m_up)" using mup log_ceiling_sound(1) by auto - hence Cmup: "C \ of_int m_up" unfolding C_def by linarith - with mup have C: "C \ 1" by auto - from assms(1)[unfolded root_bound_def Let_def] - have B: "C = of_rat B" unfolding C_def m_up_def n_def m_def by auto - note dc = div_le_div_ceiling[of m "abs ?lc"] - with C show "B \ 0" unfolding B by auto - assume "ipoly p x = 0" - hence rt: "poly ?p x = 0" by simp - from root_imp_deg_nonzero[OF _ this] p0 have n0: "n \ 0" unfolding n_def by auto - from cauchy_root_bound[OF rt] p0 - have "norm x \ 1 + max_list_non_empty ?list' / ?i (abs ?lc)" - by (simp add: n_def) - also have "?list' = map ?i ?list" by simp - also have "max_list_non_empty \ = ?i m" unfolding m_def - by (rule max_list_non_empty_map, insert mem, auto) - also have "1 + m / ?i (abs ?lc) \ ?i m_up" - unfolding m_up_def using div_ceiling[OF alc0, of m] by auto - also have "\ \ ?r C" using Cmup using of_rat_less_eq by force - finally have "norm x \ ?r C" . - thus "norm x \ ?r B" unfolding B by simp -qed - fun pairwise_disjoint :: "'a set list \ bool" where "pairwise_disjoint [] = True" | "pairwise_disjoint (x # xs) = ((x \ (\ y \ set xs. y) = {}) \ pairwise_disjoint xs)" lemma roots_of_2_irr: assumes pc: "poly_cond p" and deg: "degree p > 0" shows "real_of_2 ` set (roots_of_2_irr p) = {x. ipoly p x = 0}" (is ?one) "Ball (set (roots_of_2_irr p)) invariant_2" (is ?two) "distinct (map real_of_2 (roots_of_2_irr p))" (is ?three) proof - note d = roots_of_2_irr_def from poly_condD[OF pc] have mon: "lead_coeff p > 0" and irr: "irreducible p" by auto let ?norm = "real_alg_2'" have "?one \ ?two \ ?three" proof (cases "degree p = 1") case True define c where "c = coeff p 0" define d where "d = coeff p 1" from True have rr: "roots_of_2_irr p = [Rational (Rat.Fract (- c) (d))]" unfolding d d_def c_def by auto from degree1_coeffs[OF True] have p: "p = [:c,d:]" and d: "d \ 0" unfolding c_def d_def by auto have *: "real_of_int c + x * real_of_int d = 0 \ x = - (real_of_int c / real_of_int d)" for x using d by (simp add: field_simps) show ?thesis unfolding rr using d * unfolding p using of_rat_1[of "Rat.Fract (- c) (d)"] by (auto simp: Fract_of_int_quotient hom_distribs) next case False let ?r = real_of_rat let ?rp = "map_poly ?r" let ?rr = "set (roots_of_2_irr p)" define ri where "ri = root_info p" define cr where "cr = root_info.l_r ri" define bnds where "bnds = [(-root_bound p, root_bound p)]" define empty where "empty = (Nil :: real_alg_2 list)" have empty: "Ball (set empty) invariant_2 \ distinct (map real_of_2 empty)" unfolding empty_def by auto from mon have p: "p \ 0" by auto from root_info[OF irr deg] have ri: "root_info_cond ri p" unfolding ri_def . from False have rr: "roots_of_2_irr p = roots_of_2_main p ri cr bnds empty" unfolding d ri_def cr_def Let_def bnds_def empty_def by auto note root_bound = root_bound[OF refl deg] from root_bound(2) have bnds: "\ l r. (l,r) \ set bnds \ l \ r" unfolding bnds_def by auto have "ipoly p x = 0 \ ?r (- root_bound p) \ x \ x \ ?r (root_bound p)" for x using root_bound(1)[of x] by (auto simp: hom_distribs) hence rts: "{x. ipoly p x = 0} = real_of_2 ` set empty \ {x. \ l r. root_cond (p,l,r) x \ (l,r) \ set bnds}" unfolding empty_def bnds_def by (force simp: root_cond_def) define rts where "rts lr = Collect (root_cond (p,lr))" for lr have disj: "pairwise_disjoint (real_of_2 ` set empty # map rts bnds)" unfolding empty_def bnds_def by auto from deg False have deg1: "degree p > 1" by auto define delta where "delta = ipoly_root_delta p" note delta = ipoly_root_delta[OF p, folded delta_def] define rel' where "rel' = ({(x, y). 0 \ y \ delta_gt delta x y})^-1" define mm where "mm = (\bnds. mset (map (\ (l,r). ?r r - ?r l) bnds))" define rel where "rel = inv_image (mult1 rel') mm" have wf: "wf rel" unfolding rel_def rel'_def by (rule wf_inv_image[OF wf_mult1[OF SN_imp_wf[OF delta_gt_SN[OF delta(1)]]]]) let ?main = "roots_of_2_main p ri cr" have "real_of_2 ` set (?main bnds empty) = real_of_2 ` set empty \ {x. \l r. root_cond (p, l, r) x \ (l, r) \ set bnds} \ Ball (set (?main bnds empty)) invariant_2 \ distinct (map real_of_2 (?main bnds empty))" (is "?one' \ ?two' \ ?three'") using empty bnds disj proof (induct bnds arbitrary: empty rule: wf_induct[OF wf]) case (1 lrss rais) note rais = 1(2)[rule_format] note lrs = 1(3) note disj = 1(4) note IH = 1(1)[rule_format] note simp = roots_of_2_main.simps[of p ri cr lrss rais] show ?case proof (cases lrss) case Nil with rais show ?thesis unfolding simp by auto next case (Cons lr lrs) obtain l r where lr': "lr = (l,r)" by force { fix lr' assume lt: "\ l' r'. (l',r') \ set lr' \ l' \ r' \ delta_gt delta (?r r - ?r l) (?r r' - ?r l')" have l: "mm (lr' @ lrs) = mm lrs + mm lr'" unfolding mm_def by (auto simp: ac_simps) have r: "mm lrss = mm lrs + {# ?r r - ?r l #}" unfolding Cons lr' rel_def mm_def by auto have "(mm (lr' @ lrs), mm lrss) \ mult1 rel'" unfolding l r mult1_def proof (rule, unfold split, intro exI conjI, unfold add_mset_add_single[symmetric], rule refl, rule refl, intro allI impI) fix d assume "d \# mm lr'" then obtain l' r' where d: "d = ?r r' - ?r l'" and lr': "(l',r') \ set lr'" unfolding mm_def in_multiset_in_set by auto from lt[OF lr'] show "(d, ?r r - ?r l) \ rel'" unfolding d rel'_def by (auto simp: of_rat_less_eq) qed hence "(lr' @ lrs, lrss) \ rel" unfolding rel_def by auto } note rel = this from rel[of Nil] have easy_rel: "(lrs,lrss) \ rel" by auto define c where "c = cr l r" from simp Cons lr' have simp: "?main lrss rais = (if c = 0 then ?main lrs rais else if c = 1 then ?main lrs (real_alg_2' ri p l r # rais) else let m = (l + r) / 2 in ?main ((m, r) # (l, m) # lrs) rais)" unfolding c_def simp Cons lr' using real_alg_2''[OF False] by auto note lrs = lrs[unfolded Cons lr'] from lrs have lr: "l \ r" by auto from root_info_condD(1)[OF ri lr, folded cr_def] have c: "c = card {x. root_cond (p,l,r) x}" unfolding c_def by auto let ?rt = "\ lrs. {x. \l r. root_cond (p, l, r) x \ (l, r) \ set lrs}" have rts: "?rt lrss = ?rt lrs \ {x. root_cond (p,l,r) x}" (is "?rt1 = ?rt2 \ ?rt3") unfolding Cons lr' by auto show ?thesis proof (cases "c = 0") case True with simp have simp: "?main lrss rais = ?main lrs rais" by simp from disj have disj: "pairwise_disjoint (real_of_2 ` set rais # map rts lrs)" unfolding Cons by auto from finite_ipoly_roots[OF p] True[unfolded c] have empty: "?rt3 = {}" unfolding root_cond_def[abs_def] split by simp with rts have rts: "?rt1 = ?rt2" by auto show ?thesis unfolding simp rts by (rule IH[OF easy_rel rais lrs disj], auto) next case False show ?thesis proof (cases "c = 1") case True let ?rai = "real_alg_2' ri p l r" from True simp have simp: "?main lrss rais = ?main lrs (?rai # rais)" by auto from card_1_Collect_ex1[OF c[symmetric, unfolded True]] have ur: "unique_root (p,l,r)" . from real_alg_2'[OF ur pc ri] have rai: "invariant_2 ?rai" "real_of_2 ?rai = the_unique_root (p, l, r)" by auto with rais have rais: "\ x. x \ set (?rai # rais) \ invariant_2 x" and dist: "distinct (map real_of_2 rais)" by auto have rt3: "?rt3 = {real_of_2 ?rai}" using ur rai by (auto intro: the_unique_root_eqI theI') have "real_of_2 ` set (roots_of_2_main p ri cr lrs (?rai # rais)) = real_of_2 ` set (?rai # rais) \ ?rt2 \ Ball (set (roots_of_2_main p ri cr lrs (?rai # rais))) invariant_2 \ distinct (map real_of_2 (roots_of_2_main p ri cr lrs (?rai # rais)))" (is "?one \ ?two \ ?three") proof (rule IH[OF easy_rel, of "?rai # rais", OF conjI lrs]) show "Ball (set (real_alg_2' ri p l r # rais)) invariant_2" using rais by auto have "real_of_2 (real_alg_2' ri p l r) \ set (map real_of_2 rais)" using disj rt3 unfolding Cons lr' rts_def by auto thus "distinct (map real_of_2 (real_alg_2' ri p l r # rais))" using dist by auto show "pairwise_disjoint (real_of_2 ` set (real_alg_2' ri p l r # rais) # map rts lrs)" using disj rt3 unfolding Cons lr' rts_def by auto qed auto hence ?one ?two ?three by blast+ show ?thesis unfolding simp rts rt3 by (rule conjI[OF _ conjI[OF \?two\ \?three\]], unfold \?one\, auto) next case False let ?m = "(l+r)/2" let ?lrs = "[(?m,r),(l,?m)] @ lrs" from False \c \ 0\ have simp: "?main lrss rais = ?main ?lrs rais" unfolding simp by (auto simp: Let_def) from False \c \ 0\ have "c \ 2" by auto from delta(2)[OF this[unfolded c]] have delta: "delta \ ?r (r - l) / 4" by auto have lrs: "\ l r. (l,r) \ set ?lrs \ l \ r" using lr lrs by (fastforce simp: field_simps) have "?r ?m \ \" unfolding Rats_def by blast with poly_cond_degree_gt_1[OF pc deg1, of "?r ?m"] have disj1: "?r ?m \ rts lr" for lr unfolding rts_def root_cond_def by auto have disj2: "rts (?m, r) \ rts (l, ?m) = {}" using disj1[of "(l,?m)"] disj1[of "(?m,r)"] unfolding rts_def root_cond_def by auto have disj3: "(rts (l,?m) \ rts (?m,r)) = rts (l,r)" unfolding rts_def root_cond_def by (auto simp: hom_distribs) have disj4: "real_of_2 ` set rais \ rts (l,r) = {}" using disj unfolding Cons lr' by auto have disj: "pairwise_disjoint (real_of_2 ` set rais # map rts ([(?m, r), (l, ?m)] @ lrs))" using disj disj2 disj3 disj4 by (auto simp: Cons lr') have "(?lrs,lrss) \ rel" proof (rule rel, intro conjI) fix l' r' assume mem: "(l', r') \ set [(?m,r),(l,?m)]" from mem lr show "l' \ r'" by auto from mem have diff: "?r r' - ?r l' = (?r r - ?r l) / 2" by auto (metis eq_diff_eq minus_diff_eq mult_2_right of_rat_add of_rat_diff, metis of_rat_add of_rat_mult of_rat_numeral_eq) show "delta_gt delta (?r r - ?r l) (?r r' - ?r l')" unfolding diff delta_gt_def by (rule order.trans[OF delta], insert lr, auto simp: field_simps of_rat_diff of_rat_less_eq) qed note IH = IH[OF this, of rais, OF rais lrs disj] have "real_of_2 ` set (?main ?lrs rais) = real_of_2 ` set rais \ ?rt ?lrs \ Ball (set (?main ?lrs rais)) invariant_2 \ distinct (map real_of_2 (?main ?lrs rais))" (is "?one \ ?two") by (rule IH) hence ?one ?two by blast+ have cong: "\ a b c. b = c \ a \ b = a \ c" by auto have id: "?rt ?lrs = ?rt lrs \ ?rt [(?m,r),(l,?m)]" by auto show ?thesis unfolding rts simp \?one\ id proof (rule conjI[OF cong[OF cong] conjI]) have "\ x. root_cond (p,l,r) x = (root_cond (p,l,?m) x \ root_cond (p,?m,r) x)" unfolding root_cond_def by (auto simp:hom_distribs) hence id: "Collect (root_cond (p,l,r)) = {x. (root_cond (p,l,?m) x \ root_cond (p,?m,r) x)}" by auto show "?rt [(?m,r),(l,?m)] = Collect (root_cond (p,l,r))" unfolding id list.simps by blast show "\ a \ set (?main ?lrs rais). invariant_2 a" using \?two\ by auto show "distinct (map real_of_2 (?main ?lrs rais))" using \?two\ by auto qed qed qed qed qed hence idd: "?one'" and cond: ?two' ?three' by blast+ define res where "res = roots_of_2_main p ri cr bnds empty" have e: "set empty = {}" unfolding empty_def by auto from idd[folded res_def] e have idd: "real_of_2 ` set res = {} \ {x. \l r. root_cond (p, l, r) x \ (l, r) \ set bnds}" by auto show ?thesis unfolding rr unfolding rts id e norm_def using cond unfolding res_def[symmetric] image_empty e idd[symmetric] by auto qed thus ?one ?two ?three by blast+ qed definition roots_of_2 :: "int poly \ real_alg_2 list" where "roots_of_2 p = concat (map roots_of_2_irr (factors_of_int_poly p))" lemma roots_of_2: shows "p \ 0 \ real_of_2 ` set (roots_of_2 p) = {x. ipoly p x = 0}" "Ball (set (roots_of_2 p)) invariant_2" "distinct (map real_of_2 (roots_of_2 p))" proof - let ?rr = "roots_of_2 p" note d = roots_of_2_def note frp1 = factors_of_int_poly { fix q r assume "q \ set ?rr" then obtain s where s: "s \ set (factors_of_int_poly p)" and q: "q \ set (roots_of_2_irr s)" unfolding d by auto from frp1(1)[OF refl s] have "poly_cond s" "degree s > 0" by (auto simp: poly_cond_def) from roots_of_2_irr[OF this] q have "invariant_2 q" by auto } thus "Ball (set ?rr) invariant_2" by auto { assume p: "p \ 0" have "real_of_2 ` set ?rr = (\ ((\ p. real_of_2 ` set (roots_of_2_irr p)) ` (set (factors_of_int_poly p))))" (is "_ = ?rrr") unfolding d set_concat set_map by auto also have "\ = {x. ipoly p x = 0}" proof - { fix x assume "x \ ?rrr" then obtain q s where s: "s \ set (factors_of_int_poly p)" and q: "q \ set (roots_of_2_irr s)" and x: "x = real_of_2 q" by auto from frp1(1)[OF refl s] have s0: "s \ 0" and pt: "poly_cond s" "degree s > 0" by (auto simp: poly_cond_def) from roots_of_2_irr[OF pt] q have rt: "ipoly s x = 0" unfolding x by auto from frp1(2)[OF refl p, of x] rt s have rt: "ipoly p x = 0" by auto } moreover { fix x :: real assume rt: "ipoly p x = 0" from rt frp1(2)[OF refl p, of x] obtain s where s: "s \ set (factors_of_int_poly p)" and rt: "ipoly s x = 0" by auto from frp1(1)[OF refl s] have s0: "s \ 0" and ty: "poly_cond s" "degree s > 0" by (auto simp: poly_cond_def) from roots_of_2_irr(1)[OF ty] rt obtain q where q: "q \ set (roots_of_2_irr s)" and x: "x = real_of_2 q" by blast have "x \ ?rrr" unfolding x using q s by auto } ultimately show ?thesis by auto qed finally show "real_of_2 ` set ?rr = {x. ipoly p x = 0}" by auto } show "distinct (map real_of_2 (roots_of_2 p))" proof (cases "p = 0") case True from factors_of_int_poly_const[of 0] True show ?thesis unfolding roots_of_2_def by auto next case p: False note frp1 = frp1[OF refl] let ?fp = "factors_of_int_poly p" let ?cc = "concat (map roots_of_2_irr ?fp)" show ?thesis unfolding roots_of_2_def distinct_conv_nth length_map proof (intro allI impI notI) fix i j assume ij: "i < length ?cc" "j < length ?cc" "i \ j" and id: "map real_of_2 ?cc ! i = map real_of_2 ?cc ! j" from ij id have id: "real_of_2 (?cc ! i) = real_of_2 (?cc ! j)" by auto from nth_concat_diff[OF ij, unfolded length_map] obtain j1 k1 j2 k2 where *: "(j1,k1) \ (j2,k2)" "j1 < length ?fp" "j2 < length ?fp" and "k1 < length (map roots_of_2_irr ?fp ! j1)" "k2 < length (map roots_of_2_irr ?fp ! j2)" "?cc ! i = map roots_of_2_irr ?fp ! j1 ! k1" "?cc ! j = map roots_of_2_irr ?fp ! j2 ! k2" by blast hence **: "k1 < length (roots_of_2_irr (?fp ! j1))" "k2 < length (roots_of_2_irr (?fp ! j2))" "?cc ! i = roots_of_2_irr (?fp ! j1) ! k1" "?cc ! j = roots_of_2_irr (?fp ! j2) ! k2" by auto from * have mem: "?fp ! j1 \ set ?fp" "?fp ! j2 \ set ?fp" by auto from frp1(1)[OF mem(1)] frp1(1)[OF mem(2)] have pc1: "poly_cond (?fp ! j1)" "degree (?fp ! j1) > 0" and pc10: "?fp ! j1 \ 0" and pc2: "poly_cond (?fp ! j2)" "degree (?fp ! j2) > 0" by (auto simp: poly_cond_def) show False proof (cases "j1 = j2") case True with * have neq: "k1 \ k2" by auto from **[unfolded True] id * have "map real_of_2 (roots_of_2_irr (?fp ! j2)) ! k1 = real_of_2 (?cc ! j)" "map real_of_2 (roots_of_2_irr (?fp ! j2)) ! k1 = real_of_2 (?cc ! j)" by auto hence "\ distinct (map real_of_2 (roots_of_2_irr (?fp ! j2)))" unfolding distinct_conv_nth using * ** True by auto with roots_of_2_irr(3)[OF pc2] show False by auto next case neq: False with frp1(4)[of p] * have neq: "?fp ! j1 \ ?fp ! j2" unfolding distinct_conv_nth by auto let ?x = "real_of_2 (?cc ! i)" define x where "x = ?x" from ** have "x \ real_of_2 ` set (roots_of_2_irr (?fp ! j1))" unfolding x_def by auto with roots_of_2_irr(1)[OF pc1] have x1: "ipoly (?fp ! j1) x = 0" by auto from ** id have "x \ real_of_2 ` set (roots_of_2_irr (?fp ! j2))" unfolding x_def by (metis image_eqI nth_mem) with roots_of_2_irr(1)[OF pc2] have x2: "ipoly (?fp ! j2) x = 0" by auto have "ipoly p x = 0" using x1 mem unfolding roots_of_2_def by (metis frp1(2) p) from frp1(3)[OF p this] x1 x2 neq mem show False by blast qed qed qed qed lift_definition (code_dt) roots_of_3 :: "int poly \ real_alg_3 list" is roots_of_2 by (insert roots_of_2, auto simp: list_all_iff) lemma roots_of_3: shows "p \ 0 \ real_of_3 ` set (roots_of_3 p) = {x. ipoly p x = 0}" "distinct (map real_of_3 (roots_of_3 p))" proof - show "p \ 0 \ real_of_3 ` set (roots_of_3 p) = {x. ipoly p x = 0}" by (transfer; intro roots_of_2, auto) show "distinct (map real_of_3 (roots_of_3 p))" by (transfer; insert roots_of_2, auto) qed lift_definition roots_of_real_alg :: "int poly \ real_alg list" is roots_of_3 . lemma roots_of_real_alg: "p \ 0 \ real_of ` set (roots_of_real_alg p) = {x. ipoly p x = 0}" "distinct (map real_of (roots_of_real_alg p))" proof - show "p \ 0 \ real_of ` set (roots_of_real_alg p) = {x. ipoly p x = 0}" by (transfer', insert roots_of_3, auto) show "distinct (map real_of (roots_of_real_alg p))" by (transfer, insert roots_of_3(2), auto) qed definition real_roots_of_int_poly :: "int poly \ real list" where "real_roots_of_int_poly p = map real_of (roots_of_real_alg p)" definition real_roots_of_rat_poly :: "rat poly \ real list" where "real_roots_of_rat_poly p = map real_of (roots_of_real_alg (snd (rat_to_int_poly p)))" abbreviation rpoly :: "rat poly \ 'a :: field_char_0 \ 'a" where "rpoly f \ poly (map_poly of_rat f)" lemma real_roots_of_int_poly: "p \ 0 \ set (real_roots_of_int_poly p) = {x. ipoly p x = 0}" "distinct (real_roots_of_int_poly p)" unfolding real_roots_of_int_poly_def using roots_of_real_alg[of p] by auto lemma real_roots_of_rat_poly: "p \ 0 \ set (real_roots_of_rat_poly p) = {x. rpoly p x = 0}" "distinct (real_roots_of_rat_poly p)" proof - obtain c q where cq: "rat_to_int_poly p = (c,q)" by force from rat_to_int_poly[OF this] have pq: "p = smult (inverse (of_int c)) (of_int_poly q)" and c: "c \ 0" by auto have id: "{x. rpoly p x = (0 :: real)} = {x. ipoly q x = 0}" unfolding pq by (simp add: c of_rat_of_int_poly hom_distribs) show "distinct (real_roots_of_rat_poly p)" unfolding real_roots_of_rat_poly_def cq snd_conv using roots_of_real_alg(2)[of q] . assume "p \ 0" with pq c have q: "q \ 0" by auto show "set (real_roots_of_rat_poly p) = {x. rpoly p x = 0}" unfolding id unfolding real_roots_of_rat_poly_def cq snd_conv using roots_of_real_alg(1)[OF q] by auto qed end