Theory Algebraic_Numbers.Real_Algebraic_Numbers
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› in "AlgNumbers"›.›
theory Real_Algebraic_Numbers
imports
Algebraic_Numbers_Pre_Impl
begin
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)
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 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›