# Theory Real_Algebraic_Numbers

(*
Author:      Sebastiaan Joosten
René Thiemann
*)
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›
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 ⟹ 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 ⟹ 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 ⟹ 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 ⟹ 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⇩d p" by auto
from irreducible⇩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)
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"