# Theory Show_Real_Precise

```(*
Author:      René Thiemann
*)
section ‹Show for Real (Algebraic) Numbers -- Unique Representation›

text ‹We implement the show-function for real (algebraic) numbers by printing them
uniquely via their monic irreducible polynomial with a special cases for polynomials
of degree at most 2.›

theory Show_Real_Precise
imports
Show_Real_Alg
Show.Show_Instances
begin

datatype real_alg_show_info = Rat_Info rat | Sqrt_Info rat rat | Real_Alg_Info "int poly" nat

fun convert_info :: "rat + int poly × nat ⇒ real_alg_show_info" where
"convert_info (Inl q) = Rat_Info q"
| "convert_info (Inr (f,n)) = (if degree f = 2 then (let a = coeff f 2; b = coeff f 1; c = coeff f 0;
b2a = Rat.Fract (-b) (2 * a);
below = Rat.Fract (b*b - 4 * a * c) (4 * a * a)
in Sqrt_Info b2a (if n = 1 then -below else below))
else Real_Alg_Info f n)"

definition real_alg_show_info :: "real_alg ⇒ real_alg_show_info" where
"real_alg_show_info x = convert_info (info_real_alg x)"

text ‹We prove that the extracted information for showing an algebraic real number is correct.›
lemma real_alg_show_info: "real_alg_show_info x = Rat_Info r ⟹ real_of x = of_rat r"
"real_alg_show_info x = Sqrt_Info r sq ⟹ real_of x = of_rat r + sqrt (of_rat sq)"
"real_alg_show_info x = Real_Alg_Info p n ⟹ p represents (real_of x) ∧ n = card {y. y ≤ real_of x ∧ ipoly p y = 0}"
(is "?l ⟹ ?r")
proof (atomize(full), goal_cases)
case 1
note d = real_alg_show_info_def
show ?case
proof (cases "info_real_alg x")
case (Inl q)
from info_real_alg(2)[OF this] this show ?thesis unfolding d by auto
next
case (Inr qm)
then obtain p n where id: "info_real_alg x = Inr (p,n)" by (cases qm, auto)
from info_real_alg(1)[OF id]
have ap: "p represents (real_of x)" and n: "n = card {y. y ≤ real_of x ∧ ipoly p y = 0}"
and irr: "irreducible p" by auto
note id' = real_alg_show_info_def id convert_info.simps Fract_of_int_quotient Let_def
have last: "?l ⟹ ?r" unfolding id' using ap n by (auto split: if_splits)
{
assume *: "real_alg_show_info x = Sqrt_Info r sq"
from this[unfolded id'] have deg: "degree p = 2" by (auto split: if_splits)
from degree2_coeffs[OF this] obtain a b c where p: "p = [:c,b,a:]" and a: "a ≠ 0" by auto
hence coeffs: "coeff p 0 = c" "coeff p 1 = b" "coeff p (Suc (Suc 0)) = a" "2 = Suc (Suc 0)" by auto
let ?a = "real_of_int a"
let ?b = "real_of_int b"
let ?c = "real_of_int c"
define A where "A = ?a"
define B where "B = ?b"
define C where "C = ?c"
let ?r = "- (B / (2 * A))"
define R where "R = ?r"
let ?sq = "(B * B - 4 * A * C) / (4 * A * A)"
let ?p = "real_of_int_poly p"
let ?disc = "(B / (2 * A)) ^ Suc (Suc 0) - C / A"
define D where "D = ?disc"
from arg_cong[OF p, of "map_poly real_of_int"]
have rp: "?p = [: C, B, A :]"
using a by (auto simp: A_def B_def C_def)
from a have A: "A ≠ 0" unfolding A_def by auto
from *[unfolded id' deg, unfolded coeffs of_int_minus of_int_minus of_int_mult of_int_diff, simplified]
have r: "real_of_rat r = R" and sq: "sqrt (of_rat sq) = (if n = 1 then - sqrt ?sq else sqrt ?sq)"
by (auto simp: A_def B_def C_def R_def real_sqrt_minus hom_distribs)
note sq
also have "?sq = D" using A by (auto simp: field_simps D_def)
finally have sq: "sqrt (of_rat sq) = (if n = 1 then - sqrt D else sqrt D)" by simp
with rp have coeffs': "coeff ?p 0 = C" "coeff ?p 1 = B" "coeff ?p (Suc (Suc 0)) = A" "2 = Suc (Suc 0)" by auto
from rp A have "degree (real_of_int_poly p) = 2" by auto
note roots = rroots2[OF this, unfolded rroots2_def Let_def coeffs', folded D_def R_def]
from ap[unfolded represents_def] have root: "ipoly p (real_of x) = 0" by auto
from root roots have D: "(D < 0) = False" by auto
note roots = roots[unfolded this if_False, folded R_def]
have "real_of x = of_rat r + sqrt (of_rat sq)"
proof (cases "D = 0")
case True
show ?thesis using roots root unfolding sq r True by auto
next
case False
with D have D: "D > 0" by auto
from roots False have roots: "{x. ipoly p x = 0} = {R + sqrt D, R - sqrt D}" by auto
let ?Roots = "{y. y ≤ real_of x ∧ ipoly p y = 0}"
have x: "real_of x ∈ ?Roots" using root by auto
from root roots have choice: "real_of x = R + sqrt D ∨ real_of x = R - sqrt D" by auto
hence small: "R - sqrt D ∈ ?Roots" using roots D by auto
show ?thesis
proof (cases "n = 1")
case True
from card_1_singletonE[OF n[symmetric, unfolded this]] obtain y where id: "?Roots = {y}" by auto
from x small show ?thesis unfolding sq r id using True by auto
next
case False
from x obtain Y where Y: "?Roots = insert (real_of x) (Y - {real_of x})" by auto
with False[unfolded n] obtain z Z where Z: "Y - {real_of x} = insert z Z" by (cases "Y - {real_of x} = {}", auto)
from Y[unfolded Z] Z have sub: "{real_of x, z} ⊆ ?Roots" and z: "z ≠ real_of x" by auto
with roots choice D have "real_of x = R + sqrt D" by force
thus ?thesis unfolding sq r id using False by auto
qed
qed
}
with last show ?thesis unfolding d by (auto simp: id Let_def)
qed
qed

fun show_rai_info :: "int ⇒ real_alg_show_info ⇒ string" where
"show_rai_info fl (Rat_Info r) = show r"
| "show_rai_info fl (Sqrt_Info r sq) = (let sqrt = ''sqrt('' @ show (abs sq) @ '')''
in if r = 0 then (if sq < 0 then '' -'' else []) @ sqrt
else (''('' @ show r @ (if sq < 0 then ''-'' else ''+'') @ sqrt @ '')''))"
| "show_rai_info fl (Real_Alg_Info p n) =
''(root #'' @ show n @ '' of '' @ show p @ '', in ('' @ show fl @ '','' @ show (fl + 1) @ ''))''"