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› in "AlgNumbers".›


theory Real_Algebraic_Numbers
imports 
  Algebraic_Numbers_Pre_Impl
begin

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

lemma bij_imp_card: assumes bij: "bij f" shows "card {x. P (f x)} = card {x. P x}"
unfolding bij_imp_Collect_image[OF bij] bij_imp_card_image[OF bij_imp_bij_inv[OF bij]]..

lemma bij_add: "bij (λx. x + y :: 'a :: group_add)" (is ?g1)
  and bij_minus: "bij (λx. x - y :: 'a)" (is ?g2)
  and inv_add[simp]: "Hilbert_Choice.inv (λx. x + y) = (λx. x - y)" (is ?g3)
  and inv_minus[simp]: "Hilbert_Choice.inv (λx. x - y) = (λx. x + y)" (is ?g4)
proof-
  have 1: "(λx. x - y)  (λx. x + y) = id" and 2: "(λx. x + y)  (λx. x - y) = id" by auto
  from o_bij[OF 1 2] show ?g1.
  from o_bij[OF 2 1] show ?g2.
  from inv_unique_comp[OF 2 1] show ?g3.
  from inv_unique_comp[OF 1 2] show ?g4.
qed

lemmas ex1_shift[simp] = bij_imp_ex1_iff[OF bij_add] bij_imp_ex1_iff[OF bij_minus]

lemma ex1_the_shift:
  assumes ex1: "∃!y :: 'a :: group_add. P y"
  shows "(THE x. P (x + d)) = (THE y. P y) - d"
    and "(THE x. P (x - d)) = (THE y. P y) + d"
  unfolding bij_ex1_imp_the_shift[OF bij_add ex1] bij_ex1_imp_the_shift[OF bij_minus ex1] by auto

lemma card_shift_image[simp]:
  shows "card ((λx :: 'a :: group_add. x + d) ` X) = card X"
    and "card ((λx. x - d) ` X) = card X"
  by (auto simp: bij_imp_card_image[OF bij_add] bij_imp_card_image[OF bij_minus])

lemma irreducible_root_free:
  fixes p :: "'a :: {idom,comm_ring_1} poly"
  assumes irr: "irreducible p" shows "root_free p"
proof (cases "degree p" "1::nat" rule: linorder_cases)
  case greater
  {
    fix x
    assume "poly p x = 0"
    hence "[:-x,1:] dvd p" using poly_eq_0_iff_dvd by blast
    then obtain r where p: "p = r * [:-x,1:]" by (elim dvdE, auto)
    have deg: "degree [:-x,1:] = 1" by simp
    have dvd: "¬ [:-x,1:] dvd 1" by (auto simp: poly_dvd_1)
    from greater have "degree r  0" using degree_mult_le[of r "[:-x,1:]", unfolded deg, folded p] by auto
    then have "¬ r dvd 1" by (auto simp: poly_dvd_1)
    with p irr irreducibleD[OF irr p] dvd have False by auto
  }
  thus ?thesis unfolding root_free_def by auto
next
  case less then have deg: "degree p = 0" by auto
  from deg obtain p0 where p: "p = [:p0:]" using degree0_coeffs by auto
  with irr have "p  0" by auto
  with p have "poly p x  0" for x by auto
  thus ?thesis by (auto simp: root_free_def)
qed (auto simp: root_free_def)


(* **************************************************************** *)
subsection ‹Real Algebraic Numbers -- Innermost Layer›

text ‹We represent a real algebraic number α› by a tuple (p,l,r):
    α› is the unique root in the interval [l,r]
    and l and r have the same sign. We always assume that p is normalized, i.e.,
    p is the unique irreducible and positive content-free polynomial 
    which represents the algebraic number.

  This representation clearly admits duplicate representations for the same number, e.g.
  (...,x-3, 3,3) is equivalent to (...,x-3,2,10).›

subsubsection ‹Basic Definitions›

type_synonym real_alg_1 = "int poly × rat × rat"

fun poly_real_alg_1 :: "real_alg_1  int poly" where "poly_real_alg_1 (p,_,_) = p"
fun rai_ub :: "real_alg_1  rat" where "rai_ub (_,_,r) = r"
fun rai_lb :: "real_alg_1  rat" where "rai_lb (_,l,_) = l"

abbreviation "roots_below p x  {y :: real. y  x  ipoly p y = 0}"

abbreviation(input) unique_root :: "real_alg_1  bool" where
  "unique_root plr  (∃! x. root_cond plr x)"

abbreviation the_unique_root :: "real_alg_1  real" where
  "the_unique_root plr  (THE x. root_cond plr x)"

abbreviation real_of_1 where "real_of_1  the_unique_root"

lemma root_condI[intro]:
  assumes "of_rat (rai_lb plr)  x" and "x  of_rat (rai_ub plr)" and "ipoly (poly_real_alg_1 plr) x = 0"
  shows "root_cond plr x"
  using assms by (auto simp: root_cond_def)

lemma root_condE[elim]:
  assumes "root_cond plr x"
      and "of_rat (rai_lb plr)  x  x  of_rat (rai_ub plr)  ipoly (poly_real_alg_1 plr) x = 0  thesis"
  shows thesis
  using assms by (auto simp: root_cond_def)

lemma
  assumes ur: "unique_root plr"
  defines "x  the_unique_root plr" and "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  shows unique_rootD: "of_rat l  x" "x  of_rat r" "ipoly p x = 0" "root_cond plr x"
        "x = y  root_cond plr y" "y = x  root_cond plr y"
    and the_unique_root_eqI: "root_cond plr y  y = x" "root_cond plr y  x = y"
proof -
  from ur show x: "root_cond plr x" unfolding x_def by (rule theI')
  have "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def)
  from x[unfolded this] show "of_rat l  x" "x  of_rat r" "ipoly p x = 0" by auto
  from x ur
  show "root_cond plr y  y = x" and "root_cond plr y  x = y"
   and "x = y  root_cond plr y" and "y = x  root_cond plr y" by auto
qed

lemma unique_rootE:
  assumes ur: "unique_root plr"
  defines "x  the_unique_root plr" and "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  assumes main: "of_rat l  x  x  of_rat r  ipoly p x = 0  root_cond plr x 
        (y. x = y  root_cond plr y)  (y. y = x  root_cond plr y)  thesis"
  shows thesis by (rule main, unfold x_def p_def l_def r_def; rule unique_rootD[OF ur])

lemma unique_rootI:
  assumes " y. root_cond plr y  x = y" "root_cond plr x"
  shows "unique_root plr" using assms by blast

definition invariant_1 :: "real_alg_1  bool" where
  "invariant_1 tup  case tup of (p,l,r) 
    unique_root (p,l,r)  sgn l = sgn r  poly_cond p"


lemma invariant_1I:
  assumes "unique_root plr" and "sgn (rai_lb plr) = sgn (rai_ub plr)" and "poly_cond (poly_real_alg_1 plr)"
  shows "invariant_1 plr"
  using assms by (auto simp: invariant_1_def)

lemma
  assumes "invariant_1 plr"
  defines "x  the_unique_root plr" and "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  shows invariant_1D: "root_cond plr x"
    "sgn l = sgn r" "sgn x = of_rat (sgn r)" "unique_root plr" "poly_cond p" "degree p > 0" "primitive p"
    and invariant_1_root_cond: " y. root_cond plr y  y = x"
proof -
  let ?l = "of_rat l :: real"
  let ?r = "of_rat r :: real"
  have plr: "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def)
  from assms
  show ur: "unique_root plr" and sgn: "sgn l = sgn r" and pc: "poly_cond p" by (auto simp: invariant_1_def)
  from ur show rc: "root_cond plr x" by (auto simp add: x_def plr intro: theI')
  from this[unfolded plr] have x: "ipoly p x = 0" and bnd: "?l  x" "x  ?r" by auto
  show "sgn x = of_rat (sgn r)"
  proof (cases "0::real" "x" rule:linorder_cases)
    case less
    with bnd(2) have "0 < ?r" by arith
    thus ?thesis using less by simp
  next
    case equal
    with bnd have "?l  0" "?r  0" by auto
    hence "l  0" "r  0" by auto
    with sgn l = sgn r have "l = 0" "r = 0" unfolding sgn_rat_def by (auto split: if_splits)
    with rc[unfolded plr]
    show ?thesis by auto
  next
    case greater
    with bnd(1) have "?l < 0" by arith
    thus ?thesis unfolding sgn l = sgn r[symmetric] using greater by simp
  qed
  from the_unique_root_eqI[OF ur] rc
  show " y. root_cond plr y  y = x" by metis
  {
    assume "degree p = 0"
    with poly_zero[OF x, simplified] sgn bnd have "p = 0" by auto
    with pc have "False" by auto
  }
  then show "degree p > 0" by auto
  with pc show "primitive p" by (intro irreducible_imp_primitive, auto)
qed

lemma invariant_1E[elim]:
  assumes "invariant_1 plr"
  defines "x  the_unique_root plr" and "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  assumes main: "root_cond plr x 
      sgn l = sgn r  sgn x = of_rat (sgn r)  unique_root plr  poly_cond p  degree p > 0 
      primitive p  thesis"
  shows thesis apply (rule main)
  using assms(1) unfolding x_def p_def l_def r_def by (auto dest: invariant_1D)

lemma invariant_1_realI:
  fixes plr :: real_alg_1
  defines "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  assumes x: "root_cond plr x" and "sgn l = sgn r"
      and ur: "unique_root plr"
      and "poly_cond p"
  shows "invariant_1 plr  real_of_1 plr = x"
  using the_unique_root_eqI[OF ur x] assms by (cases plr, auto intro: invariant_1I)
    
lemma real_of_1_0:
  assumes "invariant_1 (p,l,r)"
  shows [simp]: "the_unique_root (p,l,r) = 0  r = 0"
    and [dest]: "l = 0  r = 0"
    and [intro]: "r = 0  l = 0"
  using assms by (auto simp: sgn_0_0)


lemma invariant_1_pos: assumes rc: "invariant_1 (p,l,r)"
  shows [simp]:"the_unique_root (p,l,r) > 0  r > 0" (is "?x > 0  _")
    and [simp]:"the_unique_root (p,l,r) < 0  r < 0"
    and [simp]:"the_unique_root (p,l,r)  0  r  0"
    and [simp]:"the_unique_root (p,l,r)  0  r  0"
    and [intro]: "r > 0  l > 0"
    and [dest]: "l > 0  r > 0"
    and [intro]: "r < 0  l < 0"
    and [dest]: "l < 0  r < 0"
proof(atomize(full),goal_cases)
  case 1
  let ?r = "real_of_rat"
  from assms[unfolded invariant_1_def]
  have ur: "unique_root (p,l,r)" and sgn: "sgn l = sgn r" by auto
  from unique_rootD(1-2)[OF ur] have le: "?r l  ?x" "?x  ?r r" by auto
  from rc show ?case
  proof (cases r "0::rat" rule:linorder_cases)
    case greater
    with sgn have "sgn l = 1" by simp
    hence l0: "l > 0" by (auto simp: sgn_1_pos)
    hence "?r l > 0" by auto
    hence "?x > 0" using le(1) by arith
    with greater l0 show ?thesis by auto
  next
    case equal
    with real_of_1_0[OF rc] show ?thesis by auto
  next
    case less
    hence "?r r < 0" by auto
    with le(2) have "?x < 0" by arith
    with less sgn show ?thesis by (auto simp: sgn_1_neg)
  qed
qed

definition invariant_1_2 where
  "invariant_1_2 rai  invariant_1 rai  degree (poly_real_alg_1 rai) > 1"

definition poly_cond2 where "poly_cond2 p  poly_cond p  degree p > 1"

lemma poly_cond2I[intro!]: "poly_cond p  degree p > 1  poly_cond2 p" by (simp add: poly_cond2_def)

lemma poly_cond2D:
  assumes "poly_cond2 p"
  shows "poly_cond p" and "degree p > 1" using assms by (auto simp: poly_cond2_def)

lemma poly_cond2E[elim!]:
  assumes "poly_cond2 p" and "poly_cond p  degree p > 1  thesis" shows thesis
  using assms by (auto simp: poly_cond2_def)

lemma invariant_1_2_poly_cond2: "invariant_1_2 rai  poly_cond2 (poly_real_alg_1 rai)"
  unfolding invariant_1_def invariant_1_2_def poly_cond2_def by auto

lemma invariant_1_2I[intro!]:
  assumes "invariant_1 rai" and "degree (poly_real_alg_1 rai) > 1" shows "invariant_1_2 rai"
  using assms by (auto simp: invariant_1_2_def)

lemma invariant_1_2E[elim!]:
  assumes "invariant_1_2 rai"
      and "invariant_1 rai  degree (poly_real_alg_1 rai) > 1  thesis"
  shows thesis using assms[unfolded invariant_1_2_def] by auto


lemma invariant_1_2_realI:
  fixes plr :: real_alg_1
  defines "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  assumes x: "root_cond plr x" and sgn: "sgn l = sgn r" and ur: "unique_root plr" and p: "poly_cond2 p"
  shows "invariant_1_2 plr  real_of_1 plr = x"
  using invariant_1_realI[OF x] p sgn ur unfolding p_def l_def r_def by auto
  
subsection ‹Real Algebraic Numbers = Rational + Irrational Real Algebraic Numbers›

text ‹In the next representation of real algebraic numbers, we distinguish between
  rational and irrational numbers. The advantage is that whenever we only work on
  rational numbers, there is not much overhead involved in comparison to the 
  existing implementation of real numbers which just supports the rational numbers.
  For irrational numbers we additionally store the number of the root, counting from
  left to right. For instance $-\sqrt{2}$ and $\sqrt{2}$ would be root number 1 and 2
  of $x^2 - 2$.›

subsubsection ‹Definitions and Algorithms on Raw Type›
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 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 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:
  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)" 
proof -
  have plr: "plr = (p,l,r)" by (cases plr, auto simp: p_def l_def r_def)
  show ?thesis
  proof (rule gt_rat_sign_change_square_free[OF ur plr _ in_interval])
    note nz = poly_cond2_no_rat_root[OF p]
    from nz[of y] show "ipoly p y  0" by auto
    from nz[of r] show "ipoly p r  0" by auto
    from p have "irreducible p" by auto
    thus "square_free p" by (rule irreducible_imp_square_free)
  qed
qed
  
definition tighten_poly_bounds :: "rat  rat  rat  rat × rat × rat" where
  "tighten_poly_bounds l r sr = (let m = (l + r) / 2; sm = sgn (ipoly p m) in 
    if sm = sr
     then (l,m,sm) else (m,r,sr))"

lemma tighten_poly_bounds: assumes res: "tighten_poly_bounds l r sr = (l',r',sr')"
  and ur: "unique_root (p,l,r)"
  and p:  "poly_cond2 p"   
  and sr: "sr = sgn (ipoly p r)" 
  shows "root_cond (p,l',r') (the_unique_root (p,l,r))" "l  l'" "l'  r'" "r'  r" 
    "(r' - l') = (r - l) / 2" "sr' = sgn (ipoly p r')" 
proof -
  let ?x = "the_unique_root (p,l,r)"
  let ?x' = "the_unique_root (p,l',r')"
  let ?m = "(l + r) / 2"
  note d = tighten_poly_bounds_def Let_def
  from unique_root_lr[OF ur] have lr: "l  r" by auto
  thus "l  l'" "l'  r'" "r'  r" "(r' - l') = (r - l) / 2" "sr' = sgn (ipoly p r')"
    using res sr unfolding d by (auto split: if_splits)
  hence "l  ?m" "?m  r" by auto
  note le = gt_rat_sign_change[OF ur,simplified,OF p this]
  note urD = unique_rootD[OF ur]
  show "root_cond (p,l',r') ?x"
  proof (cases "sgn (ipoly p ?m) = sgn (ipoly p r)")
    case *: False
    with res sr have id: "l' = ?m" "r' = r" unfolding d by auto
    from *[unfolded le] urD show ?thesis unfolding id by auto
  next
    case *: True 
    with res sr have id: "l' = l" "r' = ?m" unfolding d by auto
    from *[unfolded le] urD show ?thesis unfolding id by auto
  qed
qed

partial_function (tailrec) tighten_poly_bounds_epsilon :: "rat  rat  rat  rat × rat × rat" where
  [code]: "tighten_poly_bounds_epsilon l r sr = (if r - l  x then (l,r,sr) else
    (case tighten_poly_bounds l r sr of (l',r',sr')  tighten_poly_bounds_epsilon l' r' sr'))"
    
partial_function (tailrec) tighten_poly_bounds_for_x :: "rat  rat  rat 
  rat × rat × rat" where 
  [code]: "tighten_poly_bounds_for_x l r sr = (if x < l  r < x then (l, r, sr) else
     (case tighten_poly_bounds l r sr of (l',r',sr')  tighten_poly_bounds_for_x l' r' sr'))"

lemma tighten_poly_bounds_epsilon:
  assumes ur: "unique_root (p,l,r)"
  defines u: "u  the_unique_root (p,l,r)"
  assumes p: "poly_cond2 p"
      and res: "tighten_poly_bounds_epsilon l r sr = (l',r',sr')"
      and sr: "sr = sgn (ipoly p r)" 
      and x: "x > 0"
  shows "l  l'" "r'  r" "root_cond (p,l',r') u" "r' - l'  x" "sr' = sgn (ipoly p r')" 
proof -
  let ?u = "the_unique_root (p,l,r)"
  define delta where "delta = x / 2"
  have delta: "delta > 0" unfolding delta_def using x by auto
  let ?dist = "λ (l,r,sr). r - l"
  let ?rel = "inv_image {(x, y). 0  y  delta_gt delta x y} ?dist"
  note SN = SN_inv_image[OF delta_gt_SN[OF delta], of ?dist]
  note simps = res[unfolded tighten_poly_bounds_for_x.simps[of l r]]
  let ?P = "λ (l,r,sr). unique_root (p,l,r)  u = the_unique_root (p,l,r) 
     tighten_poly_bounds_epsilon l r sr = (l',r',sr') 
     sr = sgn (ipoly p r)
     l  l'  r'  r  r' - l'  x  root_cond (p,l',r') u  sr' = sgn (ipoly p r')"
  have "?P (l,r,sr)"
  proof (induct rule: SN_induct[OF SN])
    case (1 lr)
    obtain l r sr where lr: "lr = (l,r,sr)" by (cases lr, auto)
    show ?case unfolding lr split
    proof (intro impI)
      assume ur: "unique_root (p, l, r)"
        and u: "u = the_unique_root (p, l, r)"
        and res: "tighten_poly_bounds_epsilon l r sr = (l', r', sr')"
        and sr: "sr = sgn (ipoly p r)" 
      note tur = unique_rootD[OF ur]
      note simps = tighten_poly_bounds_epsilon.simps[of l r sr]
      show "l  l'  r'  r  r' - l'  x  root_cond (p, l', r') u  sr' = sgn (ipoly p r')"
      proof (cases "r - l  x")
        case True
        with res[unfolded simps] ur tur(4) u sr
        show ?thesis by auto
      next
        case False 
        hence x: "r - l > x" by auto
        let ?tight = "tighten_poly_bounds l r sr"
        obtain L R SR where tight: "?tight = (L,R,SR)" by (cases ?tight, auto)
        note tighten = tighten_poly_bounds[OF tight[unfolded sr] ur p]
        from unique_root_sub_interval[OF ur tighten(1-2,4)] p
        have ur': "unique_root (p,L,R)" "u = the_unique_root (p,L,R)" unfolding u by auto
        from res[unfolded simps tight] False sr have "tighten_poly_bounds_epsilon L R SR = (l',r',sr')" by auto
        note IH = 1[of "(L,R,SR)", unfolded tight split lr, rule_format, OF _ ur' this]
        have "L  l'  r'  R  r' - l'  x  root_cond (p, l', r') u  sr' = sgn (ipoly p r')"
          by (rule IH, insert tighten False, auto simp: delta_gt_def delta_def)
        thus ?thesis using tighten by auto
      qed
    qed
  qed
  from this[unfolded split u, rule_format, OF ur refl res sr] 
  show "l  l'" "r'  r" "root_cond (p,l',r') u" "r' - l'  x" "sr' = sgn (ipoly p r')" using u by auto
qed

lemma tighten_poly_bounds_for_x:
  assumes ur: "unique_root (p,l,r)"
  defines u: "u  the_unique_root (p,l,r)"
  assumes p: "poly_cond2 p" 
      and res: "tighten_poly_bounds_for_x l r sr = (l',r',sr')"
      and sr: "sr = sgn (ipoly p r)" 
  shows "l  l'" "l'  r'" "r'  r" "root_cond (p,l',r') u" "¬ (l'  x  x  r')" "sr' = sgn (ipoly p r')" "unique_root (p,l',r')"
proof -
  let ?u = "the_unique_root (p,l,r)"
  let ?x = "real_of_rat x"
  define delta where "delta = abs ((u - ?x) / 2)"
  let ?p = "real_of_int_poly p"
  note ru = unique_rootD[OF ur]
  {
    assume "u = ?x"
    note u = this[unfolded u]
    from poly_cond2_no_rat_root[OF p] ur have False by (elim unique_rootE, auto simp: u)
  }
  hence delta: "delta > 0" unfolding delta_def by auto
  let ?dist = "λ (l,r,sr). real_of_rat (r - l)"
  let ?rel = "inv_image {(x, y). 0  y  delta_gt delta x y} ?dist"
  note SN = SN_inv_image[OF delta_gt_SN[OF delta], of ?dist]
  note simps = res[unfolded tighten_poly_bounds_for_x.simps[of l r]]
  let ?P = "λ (l,r,sr). unique_root (p,l,r)  u = the_unique_root (p,l,r) 
     tighten_poly_bounds_for_x l r sr = (l',r',sr') 
     sr = sgn (ipoly p r)
     l  l'  r'  r  ¬ (l'  x  x  r')  root_cond (p,l',r') u  sr' = sgn (ipoly p r')"
  have "?P (l,r,sr)"
  proof (induct rule: SN_induct[OF SN])
    case (1 lr)
    obtain l r sr where lr: "lr = (l,r,sr)" by (cases lr, auto)
    let ?l = "real_of_rat l"
    let ?r = "real_of_rat r"
    show ?case unfolding lr split
    proof (intro impI)
      assume ur: "unique_root (p, l, r)"
        and u: "u = the_unique_root (p, l, r)"
        and res: "tighten_poly_bounds_for_x l r sr = (l', r', sr')"
        and sr: "sr = sgn (ipoly p r)" 
      note tur = unique_rootD[OF ur]
      note simps = tighten_poly_bounds_for_x.simps[of l r]
      show "l  l'  r'  r  ¬ (l'  x  x  r')  root_cond (p, l', r') u  sr' = sgn (ipoly p r')"
      proof (cases "x < l  r < x")
        case True
        with res[unfolded simps] ur tur(4) u sr
        show ?thesis by auto
      next
        case False 
        hence x: "?l  ?x" "?x  ?r" by (auto simp: of_rat_less_eq)
        let ?tight = "tighten_poly_bounds l r sr"
        obtain L R SR where tight: "?tight = (L,R,SR)" by (cases ?tight, auto)
        note tighten = tighten_poly_bounds[OF tight ur p sr]
        from unique_root_sub_interval[OF ur tighten(1-2,4)] p
        have ur': "unique_root (p,L,R)" "u = the_unique_root (p,L,R)" unfolding u by auto
        from res[unfolded simps tight] False have "tighten_poly_bounds_for_x L R SR = (l',r',sr')" by auto
        note IH = 1[of ?tight, unfolded tight split lr, rule_format, OF _ ur' this]
        let ?DIFF = "real_of_rat (R - L)" let ?diff = "real_of_rat (r - l)"
        have diff0: "0  ?DIFF" using tighten(3)
          by (metis cancel_comm_monoid_add_class.diff_cancel diff_right_mono of_rat_less_eq of_rat_hom.hom_zero)
        have *: "r - l - (r - l) / 2 = (r - l) / 2" by (auto simp: field_simps)
        have "delta_gt delta ?diff ?DIFF = (abs (u - of_rat x)  real_of_rat (r - l) * 1)"
          unfolding delta_gt_def tighten(5) delta_def of_rat_diff[symmetric] * by (simp add: hom_distribs)
        also have "real_of_rat (r - l) * 1 = ?r - ?l" 
          unfolding of_rat_divide of_rat_mult of_rat_diff by auto
        also have "abs (u - of_rat x)  ?r - ?l" using x ur by (elim unique_rootE, auto simp: u)
        finally have delta: "delta_gt delta ?diff ?DIFF" .
        have "L  l'  r'  R  ¬ (l'  x  x  r')  root_cond (p, l', r') u  sr' = sgn (ipoly p r')"
          by (rule IH, insert delta diff0 tighten(6), auto)
        with l  L R  r show ?thesis by auto
      qed
    qed
  qed
  from this[unfolded split u, rule_format, OF ur refl res sr] 
  show *: "l  l'" "r'  r" "root_cond (p,l',r') u" "¬ (l'  x  x  r')" "sr' = sgn (ipoly p r')" unfolding u 
    by auto
  from *(3)[unfolded split] have "real_of_rat l'  of_rat r'" by auto
  thus "l'  r'" unfolding of_rat_less_eq .
  show "unique_root (p,l',r')" using ur *(1-3) p poly_condD(5) u unique_root_sub_interval(1) by blast
qed
end

definition real_alg_precision :: rat where
  "real_alg_precision  Rat.Fract 1 2"

lemma real_alg_precision: "real_alg_precision > 0" 
  by eval

definition normalize_bounds_1_main :: "rat  real_alg_1  real_alg_1" where
  "normalize_bounds_1_main eps rai = (case rai of (p,l,r) 
    let (l',r',sr') = tighten_poly_bounds_epsilon p eps l r (sgn (ipoly p r));
        fr = rat_of_int (floor r');
        (l'',r'',_) = tighten_poly_bounds_for_x p fr l' r' sr'
    in (p,l'',r''))"

definition normalize_bounds_1 :: "real_alg_1  real_alg_1" where 
  "normalize_bounds_1 = (normalize_bounds_1_main real_alg_precision)"

context
  fixes p q and l r :: rat
  assumes cong: " x. real_of_rat l  x  x  of_rat r  (ipoly p x = (0 :: real)) = (ipoly q x = 0)"
begin
lemma root_cond_cong: "root_cond (p,l,r) = root_cond (q,l,r)"
  by (intro ext, insert cong, auto simp: root_cond_def)

lemma the_unique_root_cong: 
  "the_unique_root (p,l,r) = the_unique_root (q,l,r)"
  unfolding root_cond_cong ..

lemma unique_root_cong: 
  "unique_root (p,l,r) = unique_root (q,l,r)"
  unfolding root_cond_cong ..
end

lemma normalize_bounds_1_main: assumes eps: "eps > 0" and rc: "invariant_1_2 x"
  defines y: "y  normalize_bounds_1_main eps x"
  shows "invariant_1_2 y  (real_of_1 y = real_of_1 x)"
proof -
  obtain p l r where x: "x = (p,l,r)" by (cases x) auto
  note rc = rc[unfolded x]
  obtain l' r' sr' where tb: "tighten_poly_bounds_epsilon p eps l r (sgn (ipoly p r)) = (l',r',sr')" 
    by (cases rule: prod_cases3, auto)
  let ?fr = "rat_of_int (floor r')"
  obtain l'' r'' sr'' where tbx: "tighten_poly_bounds_for_x p ?fr l' r' sr' = (l'',r'',sr'')"
    by (cases rule: prod_cases3, auto)
  from y[unfolded normalize_bounds_1_main_def x] tb tbx
  have y: "y = (p, l'', r'')" 
    by (auto simp: Let_def)
  from rc have "unique_root (p, l, r)" and p2: "poly_cond2 p" by auto
  from tighten_poly_bounds_epsilon[OF this tb refl eps]
  have bnd: "l  l'" "r'  r" and rc': "root_cond (p, l', r') (the_unique_root (p, l, r))" 
    and eps: "r' - l'  eps" (* currently not relevant for lemma *)
    and sr': "sr' = sgn (ipoly p r')" by auto
  from invariant_1_sub_interval[OF _ rc' bnd] rc
  have inv': "invariant_1 (p, l', r')" and eq: "real_of_1 (p, l', r') = real_of_1 (p, l, r)" by auto
  have bnd: "l'  l''" "r''  r'" and rc': "root_cond (p, l'', r'') (the_unique_root (p, l', r'))"
    by (rule tighten_poly_bounds_for_x[OF _ p2 tbx sr'], fact invariant_1D[OF inv'])+
  from invariant_1_sub_interval[OF inv' rc' bnd] p2 eq
  show ?thesis unfolding y x by auto
qed

lemma normalize_bounds_1: assumes x: "invariant_1_2 x"
  shows "invariant_1_2 (normalize_bounds_1 x)  (real_of_1 (normalize_bounds_1 x) = real_of_1 x)" 
proof(cases x)
  case xx:(fields p l r)
  let ?res = "(p,l,r)"
  have norm: "normalize_bounds_1 x = (normalize_bounds_1_main real_alg_precision ?res)" 
    unfolding normalize_bounds_1_def by (simp add: xx)
  from x have x: "invariant_1_2 ?res" "real_of_1 ?res = real_of_1 x" unfolding xx by auto
  from normalize_bounds_1_main[OF real_alg_precision x(1)] x(2-)
  show ?thesis unfolding normalize_bounds_1_def xx by auto
qed
  
lemma normalize_bound_1_poly: "poly_real_alg_1 (normalize_bounds_1 rai) = poly_real_alg_1 rai" 
  unfolding normalize_bounds_1_def normalize_bounds_1_main_def Let_def
  by (auto split: prod.splits)

definition real_alg_2_main :: "root_info  real_alg_1  real_alg_2" where 
  "real_alg_2_main ri rai  let p = poly_real_alg_1 rai
     in (if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1))
       else (case normalize_bounds_1 rai of (p',l,r) 
       Irrational (root_info.number_root ri r) (p',l,r)))"

definition real_alg_2 :: "real_alg_1  real_alg_2" where 
  "real_alg_2 rai  let p = poly_real_alg_1 rai
     in (if degree p = 1 then Rational (Rat.Fract (- coeff p 0) (coeff p 1))
       else (case normalize_bounds_1 rai of (p',l,r) 
       Irrational (root_info.number_root (root_info p) r) (p',l,r)))"

lemma degree_1_ipoly: assumes "degree p = Suc 0"
  shows "ipoly p x = 0  (x = real_of_rat (Rat.Fract (- coeff p 0) (coeff p 1)))"
proof -
  from roots1[of "map_poly real_of_int p"] assms
  have "ipoly p x = 0  x  {roots1 (real_of_int_poly p)}" by auto
  also have " = (x = real_of_rat (Rat.Fract (- coeff p 0) (coeff p 1)))" 
    unfolding Fract_of_int_quotient roots1_def hom_distribs
    by auto
  finally show ?thesis .
qed

lemma invariant_1_degree_0:
  assumes inv: "invariant_1 rai"
  shows "degree (poly_real_alg_1 rai)  0" (is "degree ?p  0")
proof (rule notI)
  assume deg: "degree ?p = 0"
  from inv have "ipoly ?p (real_of_1 rai) = 0" by auto
  with deg have "?p = 0" by (meson less_Suc0 representsI represents_degree)
  with inv show False by auto
qed

lemma real_alg_2_main:
  assumes inv: "invariant_1 rai"
  defines [simp]: "p  poly_real_alg_1 rai"
  assumes ric: "irreducible (poly_real_alg_1 rai)  root_info_cond ri (poly_real_alg_1 rai)" 
  shows "invariant_2 (real_alg_2_main ri rai)" "real_of_2 (real_alg_2_main ri rai) = real_of_1 rai"
proof (atomize(full))
  define l r where [simp]: "l  rai_lb rai" and [simp]: "r  rai_ub rai"
  show "invariant_2 (real_alg_2_main ri rai)  real_of_2 (real_alg_2_main ri rai) = real_of_1 rai" 
    unfolding id using invariant_1D
  proof (cases "degree p" "Suc 0" rule: linorder_cases)
    case deg: equal
    hence id: "real_alg_2_main ri rai = Rational (Rat.Fract (- coeff p 0) (coeff p 1))" 
      unfolding real_alg_2_main_def Let_def by auto
    note rc = invariant_1D[OF inv]
    from degree_1_ipoly[OF deg, of "the_unique_root rai"] rc(1)
    show ?thesis unfolding id by auto
  next
    case deg: greater
    with inv have inv: "invariant_1_2 rai" unfolding p_def by auto
    define rai' where "rai' = normalize_bounds_1 rai"
    have rai': "real_of_1 rai = real_of_1 rai'" and inv': "invariant_1_2 rai'" 
      unfolding rai'_def using normalize_bounds_1[OF inv] by auto
    obtain p' l' r' where "rai' = (p',l',r')" by (cases rai')
    with arg_cong[OF rai'_def, of poly_real_alg_1, unfolded normalize_bound_1_poly] split
    have split: "rai' = (p,l',r')" by auto
    from inv'[unfolded split]
    have "poly_cond p" by auto
    from poly_condD[OF this] have irr: "irreducible p" by simp
    from ric irr have ric: "root_info_cond ri p" by auto
    have id: "real_alg_2_main ri rai = (Irrational (root_info.number_root ri r') rai')" 
      unfolding real_alg_2_main_def Let_def using deg split rai'_def
      by (auto simp: rai'_def rai')
    show ?thesis unfolding id using rai' root_info_condD(2)[OF ric] 
         inv'[unfolded split]
      apply (elim invariant_1_2E invariant_1E) using inv'
      by(auto simp: split roots_below_the_unique_root)
  next
    case deg: less then have "degree p = 0" by auto
    from this invariant_1_degree_0[OF inv] have "p = 0" by simp
    with inv show ?thesis by auto
  qed
qed

lemma real_alg_2: assumes "invariant_1 rai" 
  shows "invariant_2 (real_alg_2 rai)" "real_of_2 (real_alg_2 rai) = real_of_1 rai"
proof -
  have deg: "0 < degree (poly_real_alg_1 rai)" using assms by auto
  have "real_alg_2 rai = real_alg_2_main (root_info (poly_real_alg_1 rai)) rai" 
    unfolding real_alg_2_def real_alg_2_main_def Let_def by auto
  from real_alg_2_main[OF assms root_info, folded this, simplified] deg
  show "invariant_2 (real_alg_2 rai)" "real_of_2 (real_alg_2 rai) = real_of_1 rai" by auto
qed

lemma invariant_2_realI:
  fixes plr :: real_alg_1
  defines "p  poly_real_alg_1 plr" and "l  rai_lb plr" and "r  rai_ub plr"
  assumes x: "root_cond plr x" and sgn: "sgn l = sgn r"
      and ur: "unique_root plr"
      and p: "poly_cond p"
  shows "invariant_2 (real_alg_2 plr)  real_of_2 (real_alg_2 plr) = x"
  using invariant_1_realI[OF x,folded p_def l_def r_def] sgn ur p
    real_alg_2[of plr] by auto

(* ********************* *)
subsubsection ‹Comparisons›

fun compare_rat_1 :: "rat  real_alg_1  order" where
  "compare_rat_1 x (p,l,r) = (if x < l then Lt else if x > r then Gt else
      if sgn (ipoly p x) = sgn(ipoly p r) then Gt else Lt)" 
  
lemma compare_rat_1: assumes rai: "invariant_1_2 y" 
  shows "compare_rat_1 x y = compare (of_rat x) (real_of_1 y)" 
proof-
  define p l r where "p  poly_real_alg_1 y" "l  rai_lb y" "r  rai_ub y"
  then have y [simp]: "y = (p,l,r)" by (cases y, auto)
  from rai have ur: "unique_root y" by auto
  show ?thesis 
  proof (cases "x < l  x > r")
    case True
    {
      assume xl: "x < l" 
      hence "real_of_rat x < of_rat l" unfolding of_rat_less by auto
      with rai have "of_rat x < the_unique_root y" by (auto elim!: invariant_1E)
      with xl rai have ?thesis by (cases y, auto simp: compare_real_def comparator_of_def)
    }
    moreover
    {
      assume xr: "¬ x < l" "x > r" 
      hence "real_of_rat x > of_rat r" unfolding of_rat_less by auto
      with rai have "of_rat x > the_unique_root y" by (auto elim!: invariant_1E)
      with xr rai have ?thesis by (cases y, auto simp: compare_real_def comparator_of_def)
    }
    ultimately show ?thesis using True by auto
  next
    case False
    have 0: "ipoly p (real_of_rat x)  0" by (rule poly_cond2_no_rat_root, insert rai, auto)
    with rai have diff: "real_of_1 y  of_rat x" by (auto elim!: invariant_1E)
    have " P. (1 < degree (poly_real_alg_1 y)  ∃!x. root_cond y x  poly_cond p  P)  P"
       using poly_real_alg_1.simps y rai invariant_1_2E invariant_1E by metis
    from this[OF gt_rat_sign_change] False
    have left: "compare_rat_1 x y = (if real_of_rat x  the_unique_root y then Lt else Gt)"
      by (auto simp:poly_cond2_def)
    also have " = compare (real_of_rat x) (real_of_1 y)" using diff
      by (auto simp: compare_real_def comparator_of_def)
    finally show ?thesis .
  qed
qed
  
lemma cf_pos_0[simp]: "¬ cf_pos 0" 
  unfolding cf_pos_def by auto


(* ********************* *)
subsubsection‹Negation›

fun uminus_1 :: "real_alg_1  real_alg_1" where
  "uminus_1 (p,l,r) = (abs_int_poly (poly_uminus p), -r, -l)"

lemma uminus_1: assumes x: "invariant_1 x"
  defines y: "y  uminus_1 x"
  shows "invariant_1 y  (real_of_1 y = - real_of_1 x)"
proof (cases x)
  case plr: (fields p l r)
  from x plr have inv: "invariant_1 (p,l,r)" by auto
  note * = invariant_1D[OF this]
  from plr have x: "x = (p,l,r)" by simp
  let ?p = "poly_uminus p"
  let ?mp = "abs_int_poly ?p"
  have y: "y = (?mp, -r , -l)" 
    unfolding y plr by (simp add: Let_def)
  {
    fix y
    assume "root_cond (?mp, - r, - l) y"
    hence mpy: "ipoly ?mp y = 0" and bnd: "- of_rat r  y" "y  - of_rat l"
      unfolding root_cond_def by (auto simp: of_rat_minus)
    from mpy have id: "ipoly p (- y) = 0" by auto
    from bnd have bnd: "of_rat l  - y" "-y  of_rat r" by auto
    from id bnd have "root_cond (p, l, r) (-y)" unfolding root_cond_def by auto
    with inv x have "real_of_1 x = -y" by (auto intro!: the_unique_root_eqI)
    then have "-real_of_1 x = y" by auto
  } note inj = this
  have rc: "root_cond (?mp, - r, - l) (- real_of_1 x)"
    using * unfolding root_cond_def y x by (auto simp: of_rat_minus sgn_minus_rat)
  from inj rc have ur': "unique_root (?mp, -r, -l)" by (auto intro: unique_rootI)
  with rc have the: "- real_of_1 x = the_unique_root (?mp, -r, -l)" by (auto intro: the_unique_root_eqI)
  have xp: "p represents (real_of_1 x)" using * unfolding root_cond_def split represents_def x by auto
  from * have mon: "lead_coeff ?mp > 0" by (unfold pos_poly_abs_poly, auto)
  from poly_uminus_irreducible * have mi: "irreducible ?mp" by auto
  from mi mon have pc': "poly_cond ?mp" by (auto simp: cf_pos_def)
  from poly_condD[OF pc'] have irr: "irreducible ?mp" by auto
  show ?thesis unfolding y apply (intro invariant_1_realI ur' rc) using pc' inv by auto
qed

lemma uminus_1_2:
  assumes x: "invariant_1_2 x"
  defines y: "y  uminus_1 x"
  shows "invariant_1_2 y  (real_of_1 y = - real_of_1 x)"
proof -
  from x have "invariant_1 x" by auto
  from uminus_1[OF this] have *: "real_of_1 y = - real_of_1 x" 
    "invariant_1 y" unfolding y by auto
  obtain p l r where id: "x = (p,l,r)" by (cases x)
  from x[unfolded id] have "degree p > 1" by auto
  moreover have "poly_real_alg_1 y = abs_int_poly (poly_uminus p)"
    unfolding y id uminus_1.simps split Let_def by auto
  ultimately have "degree (poly_real_alg_1 y) > 1" by simp
  with * show ?thesis by auto
qed
  
fun uminus_2 :: "real_alg_2  real_alg_2" where
  "uminus_2 (Rational r) = Rational (-r)"
| "uminus_2 (Irrational n x) = real_alg_2 (uminus_1 x)"

lemma uminus_2: assumes "invariant_2 x" 
  shows "real_of_2 (uminus_2 x) = uminus (real_of_2 x)"
  "invariant_2 (uminus_2 x)"
  using assms real_alg_2 uminus_1 by (atomize(full), cases x, auto simp: hom_distribs)

declare uminus_1.simps[simp del]


lift_definition uminus_3 :: "real_alg_3  real_alg_3" is uminus_2 
  by (auto simp: uminus_2)

lemma uminus_3: "real_of_3 (uminus_3 x) = - real_of_3 x"
  by (transfer, auto simp: uminus_2)
    
instantiation real_alg :: uminus
begin
lift_definition uminus_real_alg :: "real_alg  real_alg" is uminus_3
  by (simp add: uminus_3)
instance ..
end

lemma uminus_real_alg: "- (real_of x) = real_of (- x)"
  by (transfer, rule uminus_3[symmetric])

(* ********************* *)
subsubsection‹Inverse›

fun inverse_1 :: "real_alg_1  real_alg_2" where
  "inverse_1 (p,l,r) = real_alg_2 (abs_int_poly (reflect_poly p), inverse r, inverse l)"

lemma invariant_1_2_of_rat: assumes rc: "invariant_1_2 rai" 
  shows "real_of_1 rai  of_rat x" 
proof -
  obtain p l r where rai: "rai = (p, l, r)" by (cases rai, auto)
  from rc[unfolded rai]
  have "poly_cond2 p" "ipoly p (the_unique_root (p, l, r)) = 0" by (auto elim!: invariant_1E)
  from poly_cond2_no_rat_root[OF this(1), of x] this(2) show ?thesis unfolding rai by auto
qed
  
lemma inverse_1:
  assumes rcx: "invariant_1_2 x"
  defines y: "y  inverse_1 x"
  shows "invariant_2 y  (real_of_2 y = inverse (real_of_1 x))"
proof (cases x)
  case x: (fields p l r)
  from x rcx have rcx: "invariant_1_2 (p,l,r)" by auto
  from invariant_1_2_poly_cond2[OF rcx] have pc2: "poly_cond2 p" by simp
  have x0: "real_of_1 (p,l,r)  0" using invariant_1_2_of_rat[OF rcx, of 0] x by auto
  let ?x = "real_of_1 (p,l,r)"
  let ?mp = "abs_int_poly (reflect_poly p)"
  from x0 rcx have lr0: "l  0" and "r  0" by auto
  from x0 rcx have y: "y = real_alg_2 (?mp, inverse r, inverse l)"
    unfolding y x Let_def inverse_1.simps by auto
  from rcx have mon: "lead_coeff ?mp > 0" by (unfold lead_coeff_abs_int_poly, auto)
  {
    fix y
    assume "root_cond (?mp, inverse r, inverse l) y"
    hence mpy: "ipoly ?mp y = 0" and bnd: "inverse (of_rat r)  y" "y  inverse (of_rat l)"
      unfolding root_cond_def by (auto simp: of_rat_inverse)
    from sgn_real_mono[OF bnd(1)] sgn_real_mono[OF bnd(2)] 
    have "sgn (of_rat r)  sgn y" "sgn y  sgn (of_rat l)"
      by (simp_all add: algebra_simps)
    with rcx have sgn: "sgn (inverse (of_rat r)) = sgn y" "sgn y = sgn (inverse (of_rat l))" 
      unfolding sgn_inverse inverse_sgn
      by (auto simp add: real_of_rat_sgn intro: order_antisym)
    from sgn[simplified, unfolded real_of_rat_sgn] lr0 have "y  0" by (auto simp:sgn_0_0)
    with mpy have id: "ipoly p (inverse y) = 0" by (auto simp: ipoly_reflect_poly)
    from inverse_le_sgn[OF sgn(1) bnd(1)] inverse_le_sgn[OF sgn(2) bnd(2)]
    have bnd: "of_rat l  inverse y" "inverse y  of_rat r" by auto
    from id bnd have "root_cond (p,l,r) (inverse y)" unfolding root_cond_def by auto
    from rcx this x0 have "?x = inverse y" by auto
    then have "inverse ?x = y" by auto
  } note inj = this
  have rc: "root_cond (?mp, inverse r, inverse l) (inverse ?x)"
    using rcx x0 apply (elim invariant_1_2E invariant_1E)
    by (simp add: root_cond_def of_rat_inverse real_of_rat_sgn inverse_le_iff_sgn ipoly_reflect_poly)
  from inj rc have ur: "unique_root (?mp, inverse r, inverse l)" by (auto intro: unique_rootI)
  with rc have the: "the_unique_root (?mp, inverse r, inverse l) = inverse ?x" by (auto intro: the_unique_root_eqI)
  have xp: "p represents ?x" unfolding split represents_def using rcx by (auto elim!: invariant_1E)
  from reflect_poly_irreducible[OF _ xp x0] poly_condD rcx
  have mi: "irreducible ?mp" by auto
  from mi mon have un: "poly_cond ?mp" by (auto simp: poly_cond_def)
  show ?thesis using rcx rc ur unfolding y
    by (intro invariant_2_realI, auto simp: x y un)
qed
  
fun inverse_2 :: "real_alg_2  real_alg_2" where
  "inverse_2 (Rational r) = Rational (inverse r)"
| "inverse_2 (Irrational n x) = inverse_1 x"

lemma inverse_2: assumes "invariant_2 x"
  shows "real_of_2 (inverse_2 x) = inverse (real_of_2 x)"
  "invariant_2 (inverse_2 x)"
    using assms
    by (atomize(full), cases x, auto simp: real_alg_2 inverse_1 hom_distribs)

lift_definition inverse_3 :: "real_alg_3  real_alg_3" is inverse_2 
  by (auto simp: inverse_2)

lemma inverse_3: "real_of_3 (inverse_3 x) = inverse (real_of_3 x)"
  by (transfer, auto simp: inverse_2)
  

(* ********************* *)
subsubsection‹Floor›

fun floor_1 :: "real_alg_1  int" where
  "floor_1 (p,l,r) = (let
    (l',r',sr') = tighten_poly_bounds_epsilon p (1/2) l r (sgn (ipoly p r));
    fr = floor r';
    fl = floor l';
    fr' = rat_of_int fr
    in (if fr = fl then fr else
    let (l'',r'',sr'') = tighten_poly_bounds_for_x p fr' l' r' sr'
    in if fr' < l'' then fr else fl))"

lemma floor_1: assumes "invariant_1_2 x"
  shows "floor (real_of_1 x) = floor_1 x"
proof (cases x)
  case (fields p l r)
  obtain l' r' sr' where tbe: "tighten_poly_bounds_epsilon p (1 / 2) l r (sgn (ipoly p r)) = (l',r',sr')" 
    by (cases rule: prod_cases3, auto)    
  let ?fr = "floor r'"
  let ?fl = "floor l'"
  let ?fr' = "rat_of_int ?fr"
  obtain l'' r'' sr'' where tbx: "tighten_poly_bounds_for_x p ?fr' l' r' sr' = (l'',r'',sr'')" 
    by (cases rule: prod_cases3, auto)    
  note rc = assms[unfolded fields]
  hence rc1: "invariant_1 (p,l,r)" by auto
  have id: "floor_1 x = ((if ?fr = ?fl then ?fr 
    else if ?fr' < l'' then ?fr