(* 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 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›