Theory Real_Algebraic_Numbers

(*  
    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
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: "irreducibled p" by auto
  from irreducibled_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


(* ********************* *)
subsubsectionNegation

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])

(* ********************* *)
subsubsectionInverse

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"