Quelle  Eudoxus.thy

(*  Author: Ata Keskin, TU München 
*)

theory Eudoxus
  imports Slope
begin

section ‹Eudoxus Reals›

subsection ‹Type Definition›

text ‹Two slopes are said to be equivalent if their difference is bounded.›
definition eudoxus_rel :: "(int ==> int) ==> (int ==> int) ==> bool" (infix ‹∼_e› 50) where 
  "f ∼_e g ≡ slope f ∧ slope g ∧ bounded (λn. f n - g n)"

lemma eudoxus_rel_equivp:
  "part_equivp eudoxus_rel"
proof (rule part_equivpI)
  show "∃x. x ∼_e x" unfolding eudoxus_rel_def slope_def bounded_def by fast
  show "symp (∼_e)"  unfolding eudoxus_rel_def by (force intro: sympI dest: bounded_uminus simp: fun_Compl_def) 
  show "transp (∼_e)"  unfolding eudoxus_rel_def by (force intro!: transpI dest: bounded_add)
qed

text ‹We define the reals as the set of all equivalence classes of the relation term‹eudoxus_rel›.›
quotient_type real = "(int ==> int)" / partial: eudoxus_rel
  by (rule eudoxus_rel_equivp)

lemma real_quot_type: "quot_type (∼_e) Abs_real Rep_real"
  using Rep_real Abs_real_inverse Rep_real_inverse Rep_real_inject eudoxus_rel_equivp by (auto intro!: quot_type.intro)

lemma slope_refl: "slope f = (f ∼_e f)"
  unfolding eudoxus_rel_def by (fastforce simp add: bounded_constant)

declare slope_refl[THEN iffD2, simp]

lemmas slope_reflI = slope_refl[THEN iffD1]

lemma slope_induct[consumes 0, case_names slope]: 
  assumes "∧f. slope f ==> P (abs_real f)"
  shows "P x"
  using assms by induct force

lemma abs_real_eq_iff: "f ∼_e g ⟷ slope f ∧ slope g ∧ abs_real f = abs_real g" 
  by (metis Quotient_real Quotient_rel slope_refl)

lemma abs_real_eqI[intro]: "f ∼_e g ==> abs_real f = abs_real g" using abs_real_eq_iff by blast

lemmas eudoxus_rel_sym[sym] = Quotient_symp[OF Quotient_real, THEN sympD]
lemmas eudoxus_rel_trans[trans] = Quotient_transp[OF Quotient_real, THEN transpD]

lemmas rep_real_abs_real_refl = Quotient_rep_abs[OF Quotient_real, OF slope_refl[THEN iffD1], intro!]
lemmas rep_real_iff = Quotient_rel_rep[OF Quotient_real, iff]

declare Quotient_abs_rep[OF Quotient_real, simp]

lemma slope_rep_real: "slope (rep_real x)" by simp

lemma eudoxus_relI:
  assumes "slope f" "slope g" "∧n. n ≥ N ==> ∣f n - g n∣ ≤ C"
  shows "f ∼_e g"
proof -
  have C_nonneg: "C ≥ 0" using assms by force

  obtain C_f where C_f: "∣f (n + (- n)) - (f n + f (- n))∣ ≤ C_f" "0 ≤ C_f" for n using assms by fast

  obtain C_g where C_g: "∣g (n + (- n)) - (g n + g (- n))∣ ≤ C_g" "0 ≤ C_g" for n using assms by fast
  
  have bound: "∣f (- n) - g (- n)∣ ≤ ∣f n - g n∣ + ∣f 0∣ + ∣g 0∣ + C_f + C_g" for n using C_f(1)[of n] C_g(1)[of n] by simp

  define C' where "C' = Sup {∣f n - g n∣ | n. n ∈ {0..max 0 N}} + C + ∣f 0∣ + ∣g 0∣ + C_f + C_g"
  have *: "bdd_above {∣f n - g n∣ |n. n ∈ {0..max 0 N}}" by simp
  have "Sup {∣f n - g n∣ |n. n ∈ {0..max 0 N}} ∈ {∣f n - g n∣ |n. n ∈ {0..max 0 N}}" using C_nonneg by (intro int_Sup_mem[OF _ *]) auto
  hence Sup_nonneg: "Sup {∣f n - g n∣ | n. n ∈ {0..max 0 N}} ≥ 0" by fastforce

  have *: "∣f n - g n∣ ≤ Sup {∣f n - g n∣ | n. n ∈ {0..max 0 N}} + C" if "n ≥ 0" for n unfolding C'_def using cSup_upper[OF _ *] that C_nonneg Sup_nonneg by (cases "n ≤ N") (fastforce simp add: add.commute add_increasing2 assms(3))+
  {
    fix n
    have "∣f n - g n∣ ≤ C'"
    proof (cases "n ≥ 0")
      case True
      thus ?thesis unfolding C'_def using * C_f C_g by fastforce
    next
      case False
      hence "- n ≥ 0" by simp
      hence "∣f (- n) - g (- n)∣ ≤ Sup {∣f n - g n∣ | n. n ∈ {0..max 0 N}} + C" using *[of "- n"] by blast
      hence "∣f (- (- n)) - g (- (- n))∣ ≤ C'" unfolding C'_def using bound[of "- n"] by linarith
      thus ?thesis by simp
    qed
  }
  thus ?thesis using assms unfolding eudoxus_rel_def by (auto intro: boundedI)
qed

subsection ‹Addition and Subtraction›

text ‹We define addition, subtraction and the additive identity as follows.›
instantiation real :: "{zero, plus, minus, uminus}"
begin

quotient_definition
  "0 :: real" is "abs_real (λ_. 0)" .

declare slope_zero[intro!, simp]

lemma zero_iff_bounded: "f ∼_e (λ_. 0) ⟷ bounded f" by (metis (no_types, lifting) boundedE boundedI diff_zero eudoxus_rel_def slope_zero bounded_slopeI)
lemma zero_iff_bounded': "x = 0 ⟷ bounded (rep_real x)" by (metis (mono_tags) abs_real_eq_iff id_apply rep_real_abs_real_refl rep_real_iff slope_zero zero_iff_bounded zero_real_def)

lemma zero_def: "0 = abs_real (λ_. 0)" unfolding zero_real_def by simp

definition eudoxus_plus :: "(int ==> int) ==> (int ==> int) ==> (int ==> int)" (infixl ‹+_e› 60) where
  "(f :: int ==> int) +_e g = (λz. f z + g z)"

declare slope_add[intro, simp]

quotient_definition
  "(+) :: (real ==> real ==> real)" is "(+_e)" 
proof -
  fix x x' y y' assume "x ∼_e x'" "y ∼_e y'"
  hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" and rel_y: "slope y" "slope y'" "bounded (λz. y z - y' z)" unfolding eudoxus_rel_def by blast+
  thus "(x +_e y) ∼_e (x' +_e y')" unfolding eudoxus_rel_def eudoxus_plus_def by (fastforce intro: back_subst[of bounded, OF bounded_add[OF rel_x(3) rel_y(3)]])
qed

lemmas eudoxus_plus_cong = apply_rsp'[OF plus_real.rsp, THEN rel_funD, intro]

lemma abs_real_plus[simp]:
  assumes "slope f" "slope g"
  shows "abs_real f + abs_real g = abs_real (f +_e g)"
  using assms unfolding plus_real_def by auto

definition eudoxus_uminus :: "(int ==> int) ==> (int ==> int)" (‹-_e›) where
  "-_e (f :: int ==> int) = (λx. - f x)"

declare slope_uminus'[intro, simp]

quotient_definition
  "(uminus) :: (real ==> real)" is "-_e"
proof -
  fix x x' assume "x ∼_e x'"
  hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" unfolding eudoxus_rel_def by blast+
  thus "-_e x ∼_e -_e x'" unfolding eudoxus_rel_def eudoxus_uminus_def by (fastforce intro: back_subst[of bounded, OF bounded_uminus[OF rel_x(3)]])
qed

lemmas eudoxus_uminus_cong = apply_rsp'[OF uminus_real.rsp, simplified, intro]

lemma abs_real_uminus[simp]: 
  assumes "slope f"
  shows "- abs_real f = abs_real (-_e f)"
  using assms unfolding uminus_real_def by auto

definition "x - (y::real) = x + - y"

declare slope_minus[intro, simp]

lemma abs_real_minus[simp]:
  assumes "slope g" "slope f"
  shows "abs_real g - abs_real f = abs_real (g +_e (-_e f))" 
  using assms by (simp add: minus_real_def slope_refl eudoxus_uminus_cong)

instance ..
end

text ‹The Eudoxus reals equipped with addition and negation specified as above constitute an Abelian group.›
instance real :: ab_group_add
proof
  fix x y z :: real
  show "x + y + z = x + (y + z)" by (induct x, induct y, induct z) (simp add: eudoxus_plus_cong eudoxus_plus_def add.assoc)
  show "x + y = y + x" by (induct x, induct y) (simp add: eudoxus_plus_def add.commute)
  show "0 + x = x" by (induct x) (simp add: zero_real_def eudoxus_plus_def)
  show "- x + x = 0" by (induct x) (simp add: eudoxus_uminus_cong, simp add: zero_real_def eudoxus_plus_def eudoxus_uminus_def)
qed (simp add: minus_real_def)

subsection ‹Multiplication›

text ‹We define multiplication as the composition of two slopes.›
instantiation real :: "{one, times}"
begin

quotient_definition
  "1 :: real" is "abs_real id" .

declare slope_one[intro!, simp]

lemma one_def: "1 = abs_real id" unfolding one_real_def by simp

definition eudoxus_times :: "(int ==> int) ==> (int ==> int) ==> int ==> int" (infixl ‹*_e› 60) where
  "f *_e g = f o g"

declare slope_comp[intro, simp]
declare slope_scale[intro, simp]

quotient_definition
  "(*) :: real \ real \ real" is "(*\<^sub>e)"
proof -
  fix x x' y y' assume "x ∼_e x'" "y ∼_e y'"
  hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" and rel_y: "slope y" "slope y'" "bounded (λz. y z - y' z)" unfolding eudoxus_rel_def by blast+

  obtain C where x'_bound: "∣x' (m + n) - (x' m + x' n)∣ ≤ C" for m n using rel_x(2) unfolding slope_def by fastforce
  
  obtain A B where x'_lin_bound: "∣x' n∣ ≤ A * ∣n∣ + B" "0 ≤ A" "0 ≤ B" for n using slope_linear_bound[OF rel_x(2)] by blast

  obtain C' where y_y'_bound: "∣y z - y' z∣ ≤ C'" for z using rel_y(3) unfolding slope_def by fastforce

  have "bounded (λz. x' (y z) - x' (y' z))" 
  proof (rule boundedI)
    fix z
    have "∣x' (y z) - x' (y' z)∣ ≤ ∣x' (y z - y' z)∣ + C" using x'_bound[of "y z - y' z" "y' z"] by fastforce
    also have "... ≤ A * ∣y z - y' z∣ + B + C" using x'_lin_bound by force
    also have "... ≤ A * C' + B + C" using mult_left_mono[OF y_y'_bound x'_lin_bound(2)] by fastforce
    finally show "∣x' (y z) - x' (y' z)∣ ≤ A * C' + B + C" by blast
  qed
  hence "bounded (λz. x (y z) - x' (y' z))" using bounded_add[OF bounded_comp(1)[OF rel_x(3), of y]] by force
  thus "(x *_e y) ∼_e (x' *_e y')" unfolding eudoxus_rel_def eudoxus_times_def using rel_x rel_y by simp
qed

lemmas eudoxus_times_cong = apply_rsp'[OF times_real.rsp, THEN rel_funD, intro]
lemmas eudoxus_rel_comp = eudoxus_times_cong[unfolded eudoxus_times_def]

lemma eudoxus_times_commute:
  assumes "slope f" "slope g"
  shows "(f *_e g) ∼_e (g *_e f)"
  unfolding eudoxus_rel_def eudoxus_times_def
  using slope_comp slope_comp_commute assms by blast

lemma abs_real_times[simp]: 
  assumes "slope f" "slope g"
  shows "abs_real f * abs_real g = abs_real (f *_e g)"
  using assms unfolding times_real_def by auto

instance ..
end

lemma neg_one_def: "- 1 = abs_real (-_e id)" unfolding one_real_def by (simp add: eudoxus_uminus_def)
lemma slope_neg_one[intro, simp]: "slope (-_e id)" using slope_refl by blast

text ‹With the definitions provided above, the Eudoxus reals are a commutative ring with unity.›
instance real :: comm_ring_1
proof
  fix x y z :: real
  show "x * y * z = x * (y * z)" by (induct x, induct y, induct z) (simp add: eudoxus_times_cong eudoxus_times_def comp_assoc)
  show "x * y = y * x" by (induct x, induct y) (force simp add: slope_refl eudoxus_times_commute)
  show "1 * x = x" by (induct x) (simp add: one_real_def eudoxus_times_def)
  show "(x + y) * z = x * z + y * z" by (induct x, induct y, induct z) (simp add: eudoxus_times_cong eudoxus_plus_cong, simp add: eudoxus_times_def eudoxus_plus_def comp_def)
  have "¬bounded (λx. x)" by (metis add.inverse_inverse boundedE_strict less_irrefl neg_less_0_iff_less zabs_def)
  thus "(0 :: real) ≠ (1 :: real)" using abs_real_eq_iff[of id "λ_. 0"] unfolding one_real_def zero_real_def eudoxus_rel_def by simp
qed

lemma real_of_nat:
  "of_nat n = abs_real ((*) (of_nat n))"
proof (induction n)
  case 0
  then show ?case by (simp add: zero_real_def)
next
  case (Suc n)
  then show ?case by (simp add: one_real_def distrib_right eudoxus_plus_def)
qed

lemma real_of_int:
  "of_int z = abs_real ((*) z)"
proof (induction z rule: int_induct[where ?k=0])
  case base
  then show ?case by (simp add: zero_real_def)
next
  case (step1 i)
  then show ?case by (simp add: one_real_def distrib_right eudoxus_plus_def)
next
  case (step2 i)
  then show ?case by (simp add: one_real_def eudoxus_plus_def left_diff_distrib eudoxus_uminus_def)
qed

text ‹The Eudoxus reals are a ring of characteristic term‹0›.›
instance real :: ring_char_0
proof
  show "inj (λn. of_nat n :: real)"
  proof (intro inj_onI)
    fix x y assume "(of_nat x :: real) = of_nat y"
    hence "((*) (int x)) ∼_e ((*) (int y))" unfolding abs_real_eq_iff real_of_nat using slope_scale by blast
    hence "bounded (λz. (int x - int y) * z)" unfolding eudoxus_rel_def by (simp add: left_diff_distrib)
    then obtain C where bound: "∣(int x - int y) * z∣ ≤ C" and C_nonneg: "0 ≤ C" for z by blast
    hence "∣int x - int y∣ * ∣C + 1∣ ≤ C"  using abs_mult by metis
    hence *: "∣int x - int y∣ * (C + 1) ≤ C" using C_nonneg by force
    thus "x = y" using order_trans[OF mult_right_mono *, of 1] C_nonneg by fastforce
  qed
qed

subsection ‹Ordering›

text ‹We call a slope positive, if it tends to infinity. Similarly, we call a slope negative if it tends to negative infinity.›
instantiation real :: "{ord, abs, sgn}"
begin

definition pos :: "(int ==> int) ==> bool" where
  "pos f = (∀C ≥ 0. ∃N. ∀n ≥ N. f n ≥ C)"

definition neg :: "(int ==> int) ==> bool" where
  "neg f = (∀C ≥ 0. ∃N. ∀n ≥ N. f n ≤ -C)"
                                  
lemma pos_neg_exclusive: "¬ (pos f ∧ neg f)" unfolding neg_def pos_def by (metis int_one_le_iff_zero_less linorder_not_less nle_le uminus_int_code(1) zero_less_one_class.zero_le_one)

lemma pos_iff_neg_uminus: "pos f = neg (-_e f)" unfolding neg_def pos_def eudoxus_uminus_def by simp

lemma neg_iff_pos_uminus: "neg f = pos (-_e f)" unfolding neg_def pos_def eudoxus_uminus_def by fastforce

lemma pos_iff:
  assumes "slope f"
  shows "pos f = infinite (f ` {0..} ∩ {0<..})" (is "?lhs = ?rhs")
proof (rule iffI)
  assume pos: ?lhs
  {
    fix C assume C_nonneg: "0 ≤ (C :: int)"
    hence "∃z ≥ 0. (C + 1) ≤ f z" by (metis add_increasing2 nle_le zero_less_one_class.zero_le_one pos pos_def)
    hence "∃z ≥ 0. C ≤ f z ∧ 0 < f z" using C_nonneg by fastforce
    hence "∃N≥C. ∃z. N = f z ∧ 0 < f z ∧ 0 ≤ z" by blast
  }
  thus ?rhs by (blast intro!: int_set_infiniteI)
next
  assume infinite: ?rhs
  then obtain D where D_bound: "∣f (m + n) - (f m + f n)∣ < D" "0 < D" for m n using assms by (fastforce simp: slope_def elim: boundedE_strict)
 
  obtain M where M_bound: "∀m>0. (m + 1) * D ≤ f (m * M)" "0 < M" using slope_positive_lower_bound[OF assms infinite] D_bound(2) by blast

  define g where "g = (λz. f ((z div M) * M))"
  define E where "E = Sup ((abs o f) ` {z. 0 ≤ z ∧ z < M})"
  
  have E_bound: "∣f (z mod M)∣ ≤ E" for z
  proof -
    have "(z mod M) ∈ {z. 0 ≤ z ∧ z < M}" by (simp add: M_bound(2))
    hence "∣f (z mod M)∣ ∈ (abs o f) ` {z. 0 ≤ z ∧ z < M}" by fastforce
    thus "∣f (z mod M)∣ ≤ E" unfolding E_def by (simp add: le_cSup_finite)
  qed
  hence E_nonneg: "0 ≤ E" by fastforce

  have diff_bound: "∣f z - g z∣ ≤ E + D" for z
  proof-
    let ?d = "z div M" and ?r = "z mod M"
    have z_is: "z = ?d * M + ?r" by presburger
    hence "∣f z - g z∣ = ∣f (?d * M + ?r) - g (?d * M + ?r)∣" by argo
    also have "... = ∣(f (?d*M + ?r) - (f (?d * M) + f ?r)) + (f (?d * M) + f ?r) - g (?d * M + ?r)∣" by auto
    also have "... = ∣f ?r + (f (?d*M + ?r) - (f (?d * M) + f ?r))∣" unfolding g_def by force
    also have "... ≤ ∣f ?r∣ + D" using D_bound(1)[of "?d * M" "?r"] by linarith
    also have "... ≤ E + D" using E_bound by simp
    finally show "∣f z - g z∣ ≤ E + D" .
  qed
  {
    fix C assume C_nonneg: "0 ≤ (C :: int)"
  
    define n where "n = (E + D + C) div D"
    hence zero_less_n: "n > 0" using D_bound(2) E_nonneg C_nonneg using pos_imp_zdiv_pos_iff by fastforce
   
    have "E + C < E + D + C - (E + D + C) mod D" using diff_strict_left_mono[OF pos_mod_bound[OF D_bound(2)]] by simp
    also have "... = n * D" unfolding n_def using div_mod_decomp_int[of "E + D + C" D] by algebra
    finally have *: "(n + 1) * D > E + D + C" by (simp add: add.commute distrib_right)
  
    have "C ≤ f m" if "m ≥ n * M" for m
    proof -
      let ?d = "m div M" and ?r = "m mod M"
      have d_pos: "?d > 0" using zero_less_n M_bound that dual_order.trans pos_imp_zdiv_pos_iff by fastforce
      have n_le_d: "?d ≥ n" using zdiv_mono1 M_bound that by fastforce
      have "E + D + C < (?d + 1) * D" using D_bound n_le_d by (intro *[THEN order.strict_trans2]) simp
      also have "... ≤ g m" unfolding g_def using M_bound d_pos by blast
      finally have "E + D + C < g m" .
      hence "∣f m - g m∣ + C < g m" using diff_bound[of m] by fastforce
      thus ?thesis by fastforce
    qed
    hence "∃N. ∀p≥N. C ≤ f p" using add1_zle_eq by blast
  }
  thus ?lhs unfolding pos_def by blast
qed

lemma neg_iff:
  assumes "slope f"
  shows "neg f = infinite (f ` {0..} ∩ {..<0})" (is "?lhs = ?rhs")
proof (rule iffI)
  assume ?lhs
  hence "infinite ((- f) ` {0..} ∩ {0<..})" using pos_iff[OF slope_uminus'[OF assms]] unfolding neg_def pos_def by fastforce
  moreover have "inj (uminus :: int ==> int)" by simp
  moreover have "(- f) ` {0..} ∩ {0<..} = uminus ` (f ` {0..} ∩ {..<0})" by fastforce
  ultimately show ?rhs using finite_imageD by fastforce
next
  assume ?rhs
  moreover have "inj (uminus :: int ==> int)" by simp
  moreover have "f ` {0..} ∩ {..<0} = uminus ` ((- f) ` {0..} ∩ {0<..})" by force
  ultimately have "infinite ((- f) ` {0..} ∩ {0<..})" using finite_imageD by force
  thus ?lhs using pos_iff[OF slope_uminus'[OF assms]] unfolding pos_def neg_def by fastforce
qed

lemma pos_cong:
  assumes "f ∼_e g"
  shows "pos f = pos g"
proof -
  { 
    fix x y assume asm: "pos x" "x ∼_e y"
    fix D assume D: "0 ≤ D" "∀N. ∃p≥N. ¬ D ≤ y p"
    obtain C where bounds: "∀n. ∣x n - y n∣ ≤ C" "0 ≤ C" using asm unfolding eudoxus_rel_def by blast
    obtain N where "∀p≥N. C + D ≤ x p" using D bounds asm by (fastforce simp add: pos_def)
    hence "∀p≥N. ∣x p - y p∣ + D ≤ x p" by (metis add.commute add_left_mono bounds(1) dual_order.trans)
    hence "∀p≥N. D ≤ y p" by force
    hence False using D by blast
  }
  hence "pos x ==> pos y" if "x ∼_e y" for x y using that unfolding pos_def by metis
  thus ?thesis by (metis assms eudoxus_rel_equivp part_equivp_symp)
qed

lemma neg_cong:
  assumes "f ∼_e g"
  shows "neg f = neg g"
proof -
  { 
    fix x y assume asm: "neg x" "x ∼_e y"
    fix D assume D: "0 ≤ D" "∀N. ∃p≥N. ¬ - D ≥ y p"
    obtain C where bounds: "∣x n - y n∣ ≤ C" "0 ≤ C" for n using asm unfolding eudoxus_rel_def by blast
    obtain N where "∀p≥N. - (C + D) ≥ x p" using D bounds asm add_increasing2 unfolding neg_def by meson
    hence "∀p≥N. - ∣x p - y p∣ - D ≥ x p" using bounds(1)[THEN le_imp_neg_le, THEN diff_right_mono, THEN dual_order.trans] by simp
    hence "∀p≥N. - D ≥ y p" by force
    hence False using D by blast
  }
  hence "neg x ==> neg y" if "x ∼_e y" for x y using that unfolding neg_def by metis
  thus ?thesis by (metis assms eudoxus_rel_equivp part_equivp_symp)
qed

lemma pos_iff_nonneg_nonzero: 
  assumes "slope f"
  shows "pos f ⟷ (¬ neg f) ∧ (¬ bounded f)" (is "?lhs ⟷ ?rhs")
proof (rule iffI)
  assume pos: ?lhs
  then obtain N where "∀n≥N. f n > 0" unfolding pos_def by (metis int_one_le_iff_zero_less zero_less_one_class.zero_le_one)
  hence "f (max N m) > 0" for m by simp
  hence "¬ neg f" unfolding neg_def by (metis add.inverse_neutral dual_order.refl linorder_not_le max.cobounded2)
  thus ?rhs using pos unfolding pos_def bounded_def bdd_above_def by (metis abs_ge_self dual_order.trans gt_ex imageI iso_tuple_UNIV_I order.strict_iff_not)
next
  assume nonneg_nonzero: ?rhs
  hence finite: "finite (f ` {0..} ∩ {..<0})" using neg_iff assms by blast
  moreover have unbounded: "infinite (f ` {0..})" using nonneg_nonzero bounded_iff_finite_range slope_finite_range_iff assms by blast
  ultimately have "infinite (f ` {0..} ∩ {0..})" by (metis Compl_atLeast Diff_Diff_Int Diff_eq Diff_infinite_finite)
  moreover have "f ` {0..} ∩ {0<..} = f ` {0..} ∩ {0..} - {0}" by force
  ultimately show ?lhs unfolding pos_iff[OF assms] by simp
qed

lemma neg_iff_nonpos_nonzero: 
  assumes "slope f"
  shows "neg f ⟷ (¬ pos f) ∧ (¬ bounded f)"
  unfolding pos_iff_nonneg_nonzero[OF assms] neg_iff_pos_uminus uminus_apply 
            eudoxus_uminus_def pos_iff_nonneg_nonzero[OF slope_uminus', OF assms]
  by (force simp add: bounded_def bdd_above_def)

text ‹We define the sign of a slope to be term‹id› if it is positive, term‹-_e id› if it is negative and term‹(λ_. 0)› otherwise.›
definition eudoxus_sgn :: "(int ==> int) ==> (int ==> int)" where 
  "eudoxus_sgn f = (if pos f then id else if neg f then -_e id else (λ_. 0))"

lemma eudoxus_sgn_iff:
  assumes "slope f"
  shows "eudoxus_sgn f = (λ_. 0) ⟷ bounded f"
        "eudoxus_sgn f = id ⟷ pos f"
        "eudoxus_sgn f = (-_e id) ⟷ neg f" 
  using eudoxus_sgn_def neg_one_def one_def zero_def assms neg_iff_nonpos_nonzero pos_iff_nonneg_nonzero by auto

quotient_definition
  "(sgn :: real ==> real)" is eudoxus_sgn
  unfolding eudoxus_sgn_def
  using eudoxus_uminus_cong neg_cong pos_cong slope_one slope_refl by fastforce

lemmas eudoxus_sgn_cong = apply_rsp'[OF sgn_real.rsp, intro]

lemma eudoxus_sgn_cong'[cong]:
  assumes "f ∼_e g"
  shows "eudoxus_sgn f = eudoxus_sgn g" 
  using assms eudoxus_sgn_def neg_cong pos_cong by presburger 

lemma sgn_range: "sgn (x :: real) ∈ {-1, 0, 1}" unfolding sgn_real_def zero_def one_def neg_one_def eudoxus_sgn_def by simp

lemma sgn_abs_real_zero_iff:
  assumes "slope f"
  shows "sgn (abs_real f) = 0 ⟷ (eudoxus_sgn f = (λ_. 0))" (is "?lhs ⟷ ?rhs")
  using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def 
  by (auto simp add: sgn_real_def)

lemma sgn_zero_iff[simp]: "sgn (x :: real) = 0 ⟷ x = 0"
  using eudoxus_sgn_iff(1) sgn_abs_real_zero_iff zero_iff_bounded' slope_refl
  by (induct x) (metis (mono_tags) rep_real_abs_real_refl rep_real_iff)

lemma sgn_zero[simp]: "sgn (0 :: real) = 0" by simp

lemma sgn_abs_real_one_iff: 
  assumes "slope f"
  shows "sgn (abs_real f) = 1 ⟷ pos f"
  using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def 
  by (auto simp add: sgn_real_def)

lemmas sgn_pos = sgn_abs_real_one_iff[THEN iffD2, simp]

lemma sgn_one[simp]: "sgn (1 :: real) = 1" by (subst one_def) (fastforce simp add: pos_def iff: sgn_abs_real_one_iff)

lemma sgn_abs_real_neg_one_iff:
  assumes "slope f"
  shows "sgn (abs_real f) = - 1 ⟷ neg f"
  using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def pos_neg_exclusive
  by (auto simp add: sgn_real_def)

lemmas sgn_neg = sgn_abs_real_neg_one_iff[THEN iffD2, simp]

lemma sgn_neg_one[simp]: "sgn (- 1 :: real) = - 1" by (subst neg_one_def) (fastforce simp add: neg_def eudoxus_uminus_def iff: sgn_abs_real_neg_one_iff)

lemma sgn_plus:
  assumes "sgn x = (1 :: real)" "sgn y = 1"
  shows "sgn (x + y) = 1"
proof -
  have pos: "pos (rep_real x)" "pos (rep_real y)" using assms sgn_abs_real_one_iff[OF slope_rep_real] by simp+
  {
    fix C :: int assume C_nonneg: "C ≥ 0"
    then obtain N M where "∀n≥N. rep_real x n ≥ C" "∀n≥M. rep_real y n ≥ C" using pos unfolding pos_def by presburger
    hence "∀n≥ max N M. (rep_real x +_e rep_real y) n ≥ C" using C_nonneg unfolding eudoxus_plus_def by fastforce
    hence "∃N. ∀n ≥ N. (rep_real x +_e rep_real y) n ≥ C" by blast
  }
  thus ?thesis using pos_def by (simp add: eudoxus_plus_cong plus_real_def)
qed

lemma sgn_times: "sgn ((x :: real) * y) = sgn x * sgn y"
proof (cases "x = 0 ∨ y = 0")
  case False
  have *: "[x ≠ 0; pos (rep_real y)] ==> sgn ((x :: real) * y) = sgn x * sgn y" for x y
  proof (induct x rule: slope_induct, induct y rule: slope_induct)
    case (slope y x)
    hence pos_y: "pos y" using pos_cong by blast
    show ?case
    proof (cases "pos x")
      case pos_x: True
      {
        fix C :: int assume asm: "C ≥ 0"
        then obtain N where N: "∀n ≥ N. x n ≥ C" using pos_x unfolding pos_def by blast
        then obtain N' where "∀n≥ N'. y n ≥ max 0 N" using pos_y unfolding pos_def by (meson max.cobounded1)
        hence "∃N'. ∀n≥ N'. x (y n) ≥ C" using N by force
      }
      hence "pos (x *_e y)" unfolding pos_def eudoxus_times_def by simp
      thus ?thesis using pos_x pos_y slope by (simp add: eudoxus_times_def)
    next
      case _: False
      hence neg_x: "neg x" using slope by (metis abs_real_eqI neg_iff_nonpos_nonzero zero_def zero_iff_bounded)
      {
        fix C :: int assume "C ≥ 0"
        then obtain N where N: "∀n ≥ N. x n ≤ - C" using neg_x unfolding neg_def by blast
        then obtain N' where "∀n≥ N'. y n ≥ max 0 N" using pos_y unfolding pos_def by (meson max.cobounded1)
        hence "∃N'. ∀n≥ N'. x (y n) ≤ -C" using N by force
      }
      hence "neg (x *_e y)" unfolding neg_def eudoxus_times_def by simp
      thus ?thesis using neg_x pos_y slope by (simp add: eudoxus_times_def)
    qed
  qed
  moreover have "sgn ((x :: real) * y) = sgn x * sgn y" if neg_x: "neg (rep_real x)" and neg_y: "neg (rep_real y)" for x y
  proof -
    have pos_uminus_y: "pos (rep_real (- y))" by (metis abs_real_eq_iff eudoxus_uminus_cong map_fun_apply neg_iff_pos_uminus neg_y pos_cong rep_real_abs_real_refl rep_real_iff uminus_real_def)
    moreover have "x ≠ 0" using neg_iff_nonpos_nonzero neg_x zero_iff_bounded' by fastforce
    ultimately have "sgn (- (x * y)) = - 1" using sgn_neg[OF slope_rep_real neg_x] sgn_pos[OF slope_rep_real pos_uminus_y] * by fastforce
    hence "pos (rep_real (x * y))" by (metis eudoxus_uminus_cong map_fun_apply pos_iff_neg_uminus sgn_abs_real_neg_one_iff slope_refl slope_rep_real uminus_real_def)
    thus ?thesis using sgn_neg[OF slope_rep_real] sgn_pos[OF slope_rep_real] neg_x neg_y by simp
  qed
  ultimately show ?thesis using False neg_iff_nonpos_nonzero[OF slope_rep_real] zero_iff_bounded'
    by (cases "pos (rep_real x)" ; cases "pos (rep_real y)") (fastforce simp add: mult.commute)+
qed (force)

lemma sgn_uminus: "sgn (- (x :: real)) = - sgn x" by (metis (mono_tags, lifting) mult_minus1 sgn_neg_one sgn_times)

lemma sgn_plus':
  assumes "sgn x = (-1 :: real)" "sgn y = -1"
  shows "sgn (x + y) = -1"
  using assms sgn_uminus[of x] sgn_uminus[of y] sgn_uminus[of "x + y"] sgn_plus[of "- x" "- y"]
  by (simp add: equation_minus_iff)

lemma pos_dual_def: 
  assumes "slope f"
  shows "pos f = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≤ -C)"
proof-
  have "pos f = neg (f *_e (-_e id))" by (metis abs_real_eq_iff abs_real_times add.inverse_inverse assms eudoxus_times_commute mult_minus1_right neg_one_def sgn_abs_real_neg_one_iff sgn_abs_real_one_iff sgn_uminus slope_neg_one)
  also have "... = (∀C ≥ 0. ∃N. ∀n ≥ N. (f (- n)) ≤ -C)" unfolding neg_def eudoxus_times_def eudoxus_uminus_def by simp
  also have "... = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≤ -C)" by (metis add.inverse_inverse minus_le_iff)
  finally show ?thesis .
qed

lemma neg_dual_def:
  assumes "slope f"
  shows "neg f = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≥ C)"
  unfolding neg_iff_pos_uminus using assms by (subst pos_dual_def) (auto simp add: eudoxus_uminus_def)

lemma pos_representative:
  assumes "slope f" "pos f"
  obtains g where "f ∼_e g" "∧n. n ≥ N ==> g n ≥ C"
proof -
  obtain N' where N': "∀z≥N'. f z ≥ max 0 C" using assms unfolding pos_def by (meson max.cobounded1)
  have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
  hence "abs_real f * 1 = abs_real (f *_e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
  hence "f ∼_e (f *_e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
  moreover have "∀z≥N. (f *_e (λx. x + N' - N)) z ≥ C" unfolding eudoxus_times_def using N' by simp
  ultimately show ?thesis using that by blast
qed

lemma pos_representative':
  assumes "slope f" "pos f"
  obtains g where "f ∼_e g" "∧n. g n ≥ C ==> n ≥ N"
proof -
  obtain N' where  "∀z ≤ N'. f z ≤ - (max 0 (- C) + 1)" using assms unfolding pos_dual_def[OF assms(1)] by (metis max.cobounded1 add_increasing2 zero_less_one_class.zero_le_one)
  hence N': "∀z ≤ N'. f z < min 0 C" by fastforce
  have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
  hence "abs_real f * 1 = abs_real (f *_e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
  hence "f ∼_e (f *_e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
  moreover have "∀z<N. (f *_e (λx. x + N' - N)) z < C" unfolding eudoxus_times_def using N' by simp
  ultimately show ?thesis using that by (meson linorder_not_less)
qed

lemma neg_representative:
  assumes "slope f" "neg f"
  obtains g where "f ∼_e g" "∧n. n ≥ N ==> g n ≤ - C"
proof -
  obtain N' where "∀z≥N'. f z ≤ - max 0 C" using assms unfolding neg_def by (meson max.cobounded1)
  hence N': "∀z≥N'. f z ≤ min 0 (- C)" by force
  have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
  hence "abs_real f * 1 = abs_real (f *_e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
  hence "f ∼_e (f *_e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
  moreover have "∀z≥N. (f *_e (λx. x + N' - N)) z ≤ - C" unfolding eudoxus_times_def using N' by simp
  ultimately show ?thesis using that by blast
qed

lemma neg_representative':
  assumes "slope f" "neg f"
  obtains g where "f ∼_e g" "∧n. g n ≤ - C ==> n ≥ N"
proof -
  obtain N' where "∀z ≤ N'. f z ≥ max 0 (- C) + 1" using assms unfolding neg_dual_def[OF assms(1)] by (metis max.cobounded1 add_increasing2 zero_less_one_class.zero_le_one)
  hence N': "∀z ≤ N'. f z > max 0 (- C)" by fastforce
  have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
  hence "abs_real f * 1 = abs_real (f *_e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
  hence "f ∼_e (f *_e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
  moreover have "∀z < N. (f *_e (λx. x + N' - N)) z > - C" unfolding eudoxus_times_def using N' by simp
  ultimately show ?thesis using that by (meson linorder_not_less)
qed
                   
text ‹We call a real term‹x› less than another real term‹y›, if their difference is positive.›
definition
  "x < (y::real) ≡ sgn (y - x) = 1"

definition
  "x ≤ (y::real) ≡ x < y ∨ x = y"

definition
  abs_real: "∣x :: real∣ = (if 0 ≤ x then x else - x)"

instance ..
end

instance real :: linorder
proof
  fix x y z :: real
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] by fastforce
  show "x ≤ x" unfolding less_eq_real_def by blast
  show "[x ≤ y; y ≤ z] ==> x ≤ z" unfolding less_eq_real_def less_real_def using sgn_plus by fastforce
  show "[x ≤ y; y ≤ x] ==> x = y" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] by fastforce
  show "x ≤ y ∨ y ≤ x" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] sgn_range by force
qed


lemma real_leI:
  assumes "sgn (y - x) ∈ {0 :: real, 1}"
  shows "x ≤ y"
  using assms unfolding less_eq_real_def less_real_def by force

lemma real_lessI:
  assumes "sgn (y - x) = (1 :: real)"
  shows "x < y"
  using assms unfolding less_real_def by blast

lemma abs_real_leI:
  assumes "slope f" "slope g" "∧z. z ≥ N ==> f z ≥ g z"
  shows "abs_real f ≥ abs_real g"
proof -
  {
    assume "abs_real f ≠ abs_real g"
    hence "abs_real (f +_e -_e g) ≠ 0" by (metis abs_real_minus assms(1,2) eq_iff_diff_eq_0)
    hence "¬ bounded (f +_e -_e g)" by (metis abs_real_eqI zero_def zero_iff_bounded)
    hence "pos (f +_e -_e g) ∨ neg (f +_e -_e g)" using assms eudoxus_plus_cong eudoxus_uminus_cong neg_iff_nonpos_nonzero slope_refl by auto
    moreover
    {
      assume "neg (f +_e -_e g)"
      then obtain N' where "(f +_e -_e g) z ≤ - 1" if "z ≥ N'" for z unfolding neg_def by fastforce
      hence "f z < g z" if "z ≥ N'" for z using that unfolding eudoxus_plus_def eudoxus_uminus_def by fastforce
      hence False using assms by (metis linorder_not_less nle_le)      
    }
    ultimately have "abs_real f > abs_real g" using assms by (fastforce intro: real_lessI sgn_pos simp add: eudoxus_plus_def eudoxus_uminus_def)
  }
  thus ?thesis unfolding less_eq_real_def by argo
qed

lemma abs_real_lessI:
  assumes "slope f" "slope g" "∧z. z ≥ N ==> f z ≥ g z" "∧C. C ≥ 0 ==> ∃z. f z ≥ g z + C"
  shows "abs_real f > abs_real g"
proof -
  {
    assume "bounded (f +_e -_e g)"
    then obtain C where "∣f z - g z∣ ≤ C" "C ≥ 0" for z unfolding eudoxus_plus_def eudoxus_uminus_def by auto
    moreover obtain z where "f z ≥ g z + (C + 1)" using assms(4)[of "C + 1"] calculation by auto
    ultimately have False by (metis abs_le_D1 add.commute dual_order.trans le_diff_eq linorder_not_less zless_add1_eq)
  }
  moreover have "abs_real f ≥ abs_real g" using assms abs_real_leI by blast
  ultimately show ?thesis by (metis abs_real_minus assms(1,2) eq_iff_diff_eq_0 eudoxus_plus_cong eudoxus_sgn_iff(1) eudoxus_uminus_cong order_le_imp_less_or_eq sgn_abs_real_zero_iff sgn_zero slope_refl)
qed

lemma abs_real_lessD:
  assumes "slope f" "slope g" "abs_real f > abs_real g"
  obtains z where "z ≥ N" "f z > g z"
proof -
  {
    assume "∃N. ∀z≥N. f z ≤ g z"
    then obtain N where "f z ≤ g z" if "z ≥ N" for z by fastforce
    hence False using assms abs_real_leI by (metis linorder_not_le)
  }
  thus ?thesis using that by fastforce
qed

subsection ‹Multiplicative Inverse›

text ‹We now define the multiplicative inverse. We start by constructing a candidate for positive slopes first and then extend it to the entire domain using the choice function term‹Eps›.›
instantiation real :: "{inverse}"
begin

definition eudoxus_pos_inverse :: "(int ==> int) ==> (int ==> int)" where
  "eudoxus_pos_inverse f z = sgn z * Inf ({0..} ∩ {n. f n ≥ ∣z∣})"

lemma eudoxus_pos_inverse:
  assumes "slope f" "pos f"
  obtains g where "f ∼_e g" "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *_e f ∼_e id" 
proof -
  let ?φ = eudoxus_pos_inverse
  obtain g where g: "f ∼_e g" "g z ≥ 0 ==> z > 1" for z using pos_representative'[OF assms] by (metis gt_ex order_less_le_trans)
  hence pos_g: "pos g" using assms pos_cong by blast
  have slope_g: "slope g" using g unfolding eudoxus_rel_def by simp

  have "∃n ≥ 0. g n ≥ ∣z∣" for z using pos_g unfolding pos_def by (metis abs_ge_self order_less_imp_le zero_less_abs_iff)
  hence nonempty_φ: "{0..} ∩ {n. ∣z∣ ≤ g n} ≠ {}" for z by blast
  have bdd_below_φ: "bdd_below ({0..} ∩ {n. g n ≥ ∣z∣})" for z by simp
  have φ_bound: "g n ≥ z ==> ?φ g z ≤ n" if "z ≥ 0" "n ≥ 0" for n z unfolding eudoxus_pos_inverse_def using cInf_lower[OF _ bdd_below_φ, of n z] that abs_of_nonneg zsgn_def by simp
  hence φ_bound': "?φ g z > n ==> g n < z" if "z ≥ 0" "n ≥ 0" for z n using that linorder_not_less by blast

  have φ_mem: "z > 0 ==> ?φ g z ∈ {0..} ∩ {n. g n ≥ ∣z∣}" for z unfolding eudoxus_pos_inverse_def using int_Inf_mem[OF nonempty_φ bdd_below_φ, of z] by simp

  obtain L where "∣g (1 + (z - 1)) - (g 1 + g (z - 1))∣ ≤ L" for z using slope_g by fast
  hence *: "∣g z - (g 1 + g (z - 1))∣ ≤ L" for z by simp
  hence L: "g z ≤ g (z - 1) + (L + g 1)" for z using abs_le_D1 *[of z] by linarith

  let ?γ = "λm n. (g (m + (- n)) - (g m + g (- n))) - (g (n + (- n)) - (g n + g (- n))) + g 0"
  
  obtain c where c: "∣g (m + (- n)) - (g m + g (- n))∣ ≤ c" for m n using slope_g by fast
  obtain c' where c': "∣g (n + (- n)) - (g n + g (- n))∣ ≤ c'" for n using slope_g by fast
  have "∣?γ m n∣ ≤ ∣g (m + (- n)) - (g m + g (- n))∣ + ∣g (n + (- n)) - (g n + g (- n))∣ + ∣g 0∣" for m n by linarith
  hence *: "∣?γ m n∣ ≤ c + c' + ∣g 0∣" for m n using c[of m n] c'[of n] by linarith

  define C where "C = 2 * (c + c' + ∣g 0∣)"
  have "g (m - (n + p)) - (g m - (g n + g p)) = ?γ (m - n) p + ?γ m n" for m n p by (simp add: algebra_simps)
  hence "∣g (m - (n + p)) - (g m - (g n + g p))∣ ≤ (c + c' + ∣g 0∣) + (c + c' + ∣g 0∣)" for m n p using *[of "m - n" p] *[of m n] by simp
  hence *: "∣g (m - (n + p)) - (g m - (g n + g p))∣ ≤ C" for m n p unfolding C_def by (metis mult_2)
  have C: "g (m - (n + p)) ≤ g m - (g n + g p) + C" "g m - (g n + g p) + (- C) ≤ g (m - (n + p))" for m n p using *[of m n p] abs_le_D1 abs_le_D2 by linarith+

  have bounded: "bounded h" if bounded: "bounded (g o h)" for h :: "'a ==> int"
  proof (rule ccontr)
    assume asm: "¬ bounded h"
    obtain C where C: "∣g (h z)∣ ≤ C" "C ≥ 0" for z using bounded by fastforce
    obtain N where N: "g z ≥ C + 1" if "z ≥ N" for z using C pos_g unfolding pos_def by fastforce
    obtain N' where N': "g z ≤ - (C + 1)" if "z ≤ N'" for z 
      using C pos_g unfolding pos_dual_def[OF slope_g] by (meson add_increasing2 zero_le_one)
    obtain z where "∣h z∣ > max ∣N∣ ∣N'∣" using asm unfolding bounded_alt_def by (meson leI)
    hence "h z ∈ {..N'} ∪ {N..}" by fastforce
    hence "g (h z) ∈ {..- (C + 1)} ∪ {C + 1..}" using N N' by blast
    hence "∣g (h z)∣ ≥ C + 1" by fastforce
    thus False using C(1)[of z] by simp
  qed

  define D where "D = max ∣- (C + (L + g 1) + (L + g 1))∣ ∣C + L + g 1∣"
  {
    fix m n :: int
    assume asm: "m > 0" "n > 0"

    have "g (?φ g m) ≥ m" using φ_mem asm by simp
    moreover have "?φ g m > 1" using calculation g asm by simp
    moreover have "m > g (?φ g m - 1)" using asm calculation by (intro φ_bound') auto
    ultimately have m: "m ∈ {g (?φ g m - 1)<..g (?φ g m)}" by simp

    have "g (?φ g n) ≥ n" using φ_mem asm by simp
    moreover have "?φ g n > 1" using calculation g asm by simp
    moreover have "n > g (?φ g n - 1)" using asm calculation by (intro φ_bound') auto
    ultimately have n: "n ∈ {g (?φ g n - 1)<..g (?φ g n)}" by simp

    have "g (?φ g (m + n)) ≥ m + n" using φ_mem asm by simp
    moreover have "?φ g (m + n) > 1" using calculation g asm by simp
    moreover have "(m + n) > g (?φ g (m + n) - 1)" using asm calculation by (intro φ_bound') auto
    ultimately have m_n: "m + n ∈ {g (?φ g (m + n) - 1)<..g (?φ g (m + n))}" by simp

    have *: "g (?φ g (m + n)) - (g (?φ g m - 1) + g (?φ g n - 1)) > 0" "g (?φ g (m + n) - 1) - (g (?φ g m) + g (?φ g n)) < 0" using m_n m n by simp+
    
    have "g (?φ g (m + n) - (?φ g m + ?φ g n)) ≤ g (?φ g (m + n)) - (g (?φ g m) + g (?φ g n)) + C" using C by blast
    also have "... ≤ g (?φ g (m + n) - 1) - g (?φ g m) - g (?φ g n) + (C + L + g 1)" using L by fastforce
    finally have upper: "g (?φ g (m + n) - (?φ g m + ?φ g n)) ≤ C + L + g 1" using * by fastforce

    have "- (C + (L + g 1) + (L + g 1)) ≤ g (?φ g (m + n)) - g (?φ g m - 1) - g (?φ g n - 1) - (C + (L + g 1) + (L + g 1))" using * by linarith
    also have "... ≤ g (?φ g (m + n)) - (g (?φ g m) + g (?φ g n)) + (- C)" using L[THEN le_imp_neg_le, of "?φ g m"] L[THEN le_imp_neg_le, of "?φ g n"] by linarith
    also have "... ≤ g (?φ g (m + n) - (?φ g m + ?φ g n))" using C by blast
    finally have lower: "- (C + (L + g 1) + (L + g 1)) ≤ g (?φ g (m + n) - (?φ g m + ?φ g n))" .

    have "∣g (?φ g (m + n) - (?φ g m + ?φ g n))∣ ≤ D" using upper lower unfolding D_def by simp
  }
  hence "bounded (g o (λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n)))" by (intro boundedI[of _ D]) auto
  hence "bounded ((λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n)))" by (metis (mono_tags, lifting) bounded comp_assoc)
  then obtain C where "∣((λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n))) (m, n)∣ ≤ C" for m n by blast
  hence "∣?φ g (m + n) - (?φ g m + ?φ g n)∣ ≤ C" if "m ≥ 1" "n ≥ 1" for m n using that[THEN max_absorb2] by (metis (no_types, lifting) comp_apply prod.case)
  hence slope: "slope (?φ g)" by (intro slope_odd[of _ C]) (auto simp add: eudoxus_pos_inverse_def)
  moreover 
  {
    obtain C where C: "∣g ((?φ g n - 1) + 1) - (g (?φ g n - 1) + g 1)∣ ≤ C" for n using slope_g by fast
    have C_bound: "g (?φ g n - 1) ≥ g (?φ g n) - (∣g 1∣ + C)" for n using C[of n] by fastforce
    {
      fix n :: int
      assume asm: "n > 0"
      have upper: "g (?φ g n) ≥ n" using φ_mem asm by simp
      moreover have "?φ g n > 1" using calculation g asm by simp
      moreover have "n > g (?φ g n - 1)" using calculation asm by (intro φ_bound') auto
      moreover have "n ≥ g (?φ g n) - (∣g 1∣ + C)" using calculation C_bound[of n] by force
      ultimately have "∣g (?φ g n) - n∣ ≤ ∣g 1∣ + C" by simp
    }
    hence id: "g *_e ?φ g ∼_e id" using slope_g slope by (intro eudoxus_relI[of _ _ 1 "∣g 1∣ + C"]) (auto simp add: eudoxus_times_def)
  }
  ultimately show ?thesis using g that eudoxus_rel_trans eudoxus_times_cong slope_reflI eudoxus_times_commute[OF slope slope_g] by metis
qed  

definition eudoxus_inverse :: "(int ==> int) ==> (int ==> int)" where
  "eudoxus_inverse f = (if ¬ bounded f then SOME g. slope g ∧ (g *_e f) ∼_e id else (λ_. 0))"

lemma 
  assumes "slope f"
  shows slope_eudoxus_inverse: "slope (eudoxus_inverse f)" (is "?slope") and
        eudoxus_inverse_id: "¬ bounded f ==> eudoxus_inverse f *_e f ∼_e id" (is "¬ bounded f ==> ?id")
proof -
  have *: "[slope g; (g *_e f) ∼_e id] ==> ?slope" "[slope g; (g *_e f) ∼_e id; ¬ bounded f] ==> ?id" for g 
    unfolding eudoxus_inverse_def using someI[where ?P="λg. slope g ∧ (g *_e f) ∼_e id"] by auto
  {
    assume pos: "pos f"
    then obtain g where "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *_e f ∼_e id" using eudoxus_pos_inverse[OF assms] by blast
    hence ?slope "¬ bounded f ==> ?id" using pos pos_iff_nonneg_nonzero[OF assms] * by blast+
  }
  moreover
  {
    assume nonpos: "¬ pos f"
    {
      assume nonzero: "¬ bounded f"
      hence uminus_f: "slope (-_e f)" "pos (-_e f)" using neg_iff_pos_uminus neg_iff_nonpos_nonzero assms slope_refl nonpos by auto
      then obtain g where g: "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *_e (-_e f) ∼_e id" using eudoxus_pos_inverse by metis
      hence "-_e (eudoxus_pos_inverse g) *_e f ∼_e id" by (metis (full_types) uminus_f(1) abs_real_eq_iff abs_real_times abs_real_uminus assms(1) eudoxus_times_commute minus_mult_commute rel_funE uminus_real.rsp)
      moreover have "slope (-_e (eudoxus_pos_inverse g))" using uminus_f eudoxus_uminus_cong slope_refl g by presburger
      ultimately have ?slope ?id using * nonzero by blast+
    }
    moreover have "bounded f ==> ?slope" unfolding eudoxus_inverse_def by simp
    ultimately have ?slope "¬ bounded f ==> ?id" by blast+
  }
  ultimately show ?slope "¬ bounded f ==> ?id" by blast+
qed

quotient_definition
  "(inverse :: real ==> real)" is eudoxus_inverse
proof -
  fix x x' assume asm: "x ∼_e x'"
  hence slopes: "slope x" "slope x'" unfolding eudoxus_rel_def by blast+
  show "eudoxus_inverse x ∼_e eudoxus_inverse x'"
  proof (cases "bounded x")
    case True
    hence "bounded x'" by (meson asm eudoxus_rel_sym eudoxus_rel_trans zero_iff_bounded)
    then show ?thesis unfolding eudoxus_inverse_def using True slope_zero slope_refl by auto
  next
    case False
    hence "¬ bounded x'" by (meson asm eudoxus_rel_sym eudoxus_rel_trans zero_iff_bounded)
    hence inverses: "eudoxus_inverse x *_e x ∼_e id" "eudoxus_inverse x' *_e x' ∼_e id" using slopes eudoxus_inverse_id False by blast+

    have alt_inverse: "eudoxus_inverse x *_e x' ∼_e id" 
      using inverses eudoxus_times_cong[OF slope_reflI, OF slope_eudoxus_inverse asm, OF slopes(1)]
            eudoxus_rel_sym eudoxus_rel_trans by blast

    have "eudoxus_inverse x ∼_e eudoxus_inverse x *_e (eudoxus_inverse x' *_e x')" 
      using eudoxus_times_cong[OF slope_reflI, OF slope_eudoxus_inverse inverses(2)[THEN eudoxus_rel_sym], OF slopes(1)]
      by (simp add: eudoxus_times_def)
    also have "... ∼_e eudoxus_inverse x' *_e (eudoxus_inverse x *_e x')"
      using eudoxus_times_commute[OF slope_eudoxus_inverse(1,1), OF slopes, THEN eudoxus_times_cong, OF slope_reflI, OF slopes(2)] 
      by (simp add: eudoxus_times_def comp_assoc)      
    also have "... ∼_e eudoxus_inverse x' *_e id" using alt_inverse eudoxus_times_cong[OF slope_reflI] slope_eudoxus_inverse slopes by blast
    also have "... = eudoxus_inverse x'" unfolding eudoxus_times_def by simp
    finally show ?thesis .
  qed
qed

definition 
  "x div (y::real) = inverse y * x"

instance ..
end

lemmas eudoxus_inverse_cong = apply_rsp'[OF inverse_real.rsp, intro]

lemma eudoxus_inverse_abs[simp]:
  assumes "slope f" "¬ bounded f"
  shows "inverse (abs_real f) * abs_real f = 1"
  unfolding inverse_real_def using eudoxus_inverse_id[OF assms]
  by (metis abs_real_eqI abs_real_times assms(1) eudoxus_inverse_cong map_fun_apply one_def rep_real_abs_real_refl slope_refl)

text ‹The Eudoxus reals are a field, with inverses defined as above.›
instance real :: field
proof
  fix x y :: real
  show "x ≠ 0 ==> inverse x * x = 1" using eudoxus_sgn_iff(1) sgn_abs_real_zero_iff by (induct x rule: slope_induct) force
  show "x / y = x * inverse y" unfolding divide_real_def by simp
  show "inverse (0 :: real) = 0" unfolding inverse_real_def eudoxus_inverse_def using zero_def zero_iff_bounded' by auto 
qed

instantiation real :: distrib_lattice
begin

definition
  "(inf :: real ==> real ==> real) = min"
                                   
definition
  "(sup :: real ==> real ==> real) = max"

instance by standard (auto simp: inf_real_def sup_real_def max_min_distrib2)

end

text ‹The ordering on the Eudoxus reals is linear.›
instance real :: linordered_field
proof
  fix x y z :: real
  show "z + x ≤ z + y" if "x ≤ y"
  proof (cases "x = y")
    case False
    hence "x < y" using that by simp
    thus ?thesis
    proof (induct x rule: slope_induct, induct y rule: slope_induct, induct z rule: slope_induct)
      case (slope h g f)
      hence "pos (g +_e (-_e f))" unfolding less_real_def using sgn_abs_real_one_iff by (force simp add: eudoxus_plus_def eudoxus_uminus_def) 
      thus ?case by (metis slope(4) less_real_def add_diff_cancel_left nless_le)
    qed
  qed (force)

  show "∣x∣ = (if x < 0 then -x else x)" by (metis abs_real less_eq_real_def not_less_iff_gr_or_eq)
  show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" using sgn_range sgn_zero_iff by (auto simp: less_real_def)
  show "[x < y; 0 < z] ==> z * x < z * y" by (metis (no_types, lifting) diff_zero less_real_def mult.right_neutral right_diff_distrib' sgn_times)
qed

text ‹The Eudoxus reals fulfill the Archimedean property.›
instance real :: archimedean_field
proof                         
  fix x :: real
  show "∃z. x ≤ of_int z"
  proof (induct x rule: slope_induct)
    case (slope y)
    then obtain A B where linear_bound: "∣y z∣ ≤ A * ∣z∣ + B" "0 ≤ A" "0 ≤ B" for z using slope_linear_bound by blast
    {
      fix C assume C_nonneg: "0 ≤ (C :: int)"
      {
        fix z assume asm: "z ≥ B + C"
        have "y z + C ≤ A * ∣z∣ + B + C" using abs_le_D1 linear_bound by auto
        also have "... ≤ (A + 1) * ∣z∣" using C_nonneg linear_bound(2,3) asm by (auto simp: distrib_right)
        finally have "y z + C ≤ (A + 1) * z" using add_nonneg_nonneg[OF C_nonneg linear_bound(3)] abs_of_nonneg[of z] asm by linarith
      }
      hence "∃N. ∀x ≥ N. (((*) (A + 1)) +_e -_e y) x ≥ C" unfolding eudoxus_plus_def eudoxus_uminus_def by fastforce
    }
    hence "pos (((*) (A + 1)) +_e -_e y)" unfolding pos_def by blast
    hence "pos (rep_real (of_int (A + 1) - abs_real y))" unfolding real_of_int using slope by (simp, subst pos_cong[OF rep_real_abs_real_refl]) (auto simp add: eudoxus_plus_def eudoxus_uminus_def)
    hence "abs_real y < of_int (A + 1)" unfolding less_real_def by (metis sgn_pos rep_real_abs_real_refl rep_real_iff slope_rep_real)
    thus ?case unfolding less_eq_real_def by blast
  qed
qed

subsection ‹Completeness›

text ‹To show that the Eudoxus reals are complete, we first introduce the floor function.›
instantiation real :: floor_ceiling
begin

definition 
  "(floor :: (real ==> int)) = (λx. (SOME z. of_int z ≤ x ∧ x < of_int z + 1))"

instance
proof
  fix x :: real
  show "of_int ⌊x⌋ ≤ x ∧ x < of_int (⌊x⌋ + 1)" using someI[of "λz. of_int z ≤ x ∧ x < of_int z + 1"] floor_exists by (fastforce simp add: floor_real_def)
qed
end

lemma eudoxus_dense_rational:
  fixes x y :: real
  assumes "x < y"
  obtains m n where "x < (of_int m / of_int n)" "(of_int m / of_int n) < y" "n > 0"
proof -
  obtain n :: int where n: "inverse (y - x) < of_int n" "n > 0" by (metis ex_less_of_int antisym_conv3 dual_order.strict_trans of_int_less_iff)
  hence *: "inverse (of_int n) < y - x" by (metis assms diff_gt_0_iff_gt inverse_inverse_eq inverse_less_iff_less inverse_positive_iff_positive of_int_0_less_iff)
  define m where "m = floor (x * of_int n) + 1"
  {
    assume "y ≤ of_int m / of_int n"
    hence "inverse (of_int n) < of_int m / of_int n - x" using * by linarith
    hence "x < (of_int m - 1) / of_int n" by (simp add: diff_divide_distrib inverse_eq_divide)
    hence False unfolding m_def using n(2) divide_le_eq linorder_not_less by fastforce
  }
  moreover have "x < of_int m / of_int n" unfolding m_def by (meson n(2) floor_correct mult_imp_less_div_pos of_int_pos)
  ultimately show ?thesis using that n by fastforce
qed
         
text ‹The Eudoxus reals are a complete field.›
lemma eudoxus_complete:
  assumes "S ≠ {}" "bdd_above S"
  obtains u :: real where "∧s. s ∈ S ==> s ≤ u" "∧y. (∧s. s ∈ S ==> s ≤ y) ==> u ≤ y"
proof (cases "∃u ∈ S. ∀s ∈ S. s ≤ u")
  case False
  hence no_greatest_element: "∃y ∈ S. x < y" if "x ∈ S" for x using that by force
  define u :: "int ==> int" where "u = (λz. sgn z * Sup ((λx. ⌊of_int ∣z∣ * x⌋) ` S))"
  
  have bdd_above_u: "bdd_above ((λx. ⌊of_int ∣z∣ * x⌋) ` S)" for z by (intro bdd_above_image_mono[OF _ assms(2)] monoI) (simp add: floor_mono mult.commute mult_right_mono)
  
  have u_Sup_nonneg: "z ≥ 0 ==> ⌊of_int z * s⌋ ≤ u z" and 
       u_Sup_nonpos: "z ≤ 0 ==> - ⌊of_int (- z) * s⌋ ≥ u z" if "s ∈ S" for s z 
    unfolding u_def using cSup_upper[OF _ bdd_above_u, of "⌊of_int ∣z∣ * s⌋" z] that abs_of_nonpos zsgn_def by force+

  have u_mem: "u z ∈ (λx. sgn z * ⌊of_int ∣z∣ * x⌋) ` S" for z unfolding u_def  using int_Sup_mem[OF _ bdd_above_u, of z] assms by auto

  have slope: "slope u"
  proof -
    {
      fix m n :: int assume asm: "m > 0" "n > 0"
      obtain x_m where x_m: "x_m ∈ S" "u m = ⌊of_int m * x_m⌋" using u_mem[of m] asm zsgn_def by auto
      obtain x_n where x_n: "x_n ∈ S" "u n = ⌊of_int n * x_n⌋" using u_mem[of n] asm zsgn_def by auto
      obtain x_m_n where x_m_n: "x_m_n ∈ S" "u (m + n) = ⌊of_int (m + n) * x_m_n⌋" using u_mem[of "m + n"] asm zsgn_def by auto

      define x where "x = max (max x_m x_n) x_m_n"
      have x: "x ∈ S" unfolding x_def using x_m x_n x_m_n by linarith

      have "x ≥ x_m" "x ≥ x_n" "x ≥ x_m_n" unfolding x_def by linarith+
      hence "u m ≤ ⌊of_int m * x⌋" "u n ≤ ⌊of_int n * x⌋" "u (m + n) ≤ ⌊of_int (m + n) * x⌋" 
        unfolding x_m x_n x_m_n by (meson asm floor_less_cancel linorder_not_less mult_le_cancel_left_pos of_int_0_less_iff add_pos_pos)+       
      hence "u m = ⌊of_int m * x⌋" "u n = ⌊of_int n * x⌋" "u (m + n) = ⌊of_int m * x + of_int n * x⌋" 
        using u_Sup_nonneg[OF x(1), of m] u_Sup_nonneg[OF x(1), of n] u_Sup_nonneg[OF x(1), of "m + n"] asm add_pos_pos[OF asm] by (force simp add: distrib_right)+
      moreover 
      {
        fix a b :: real
        have "a - of_int ⌊a⌋ ∈ {0..<1}" using floor_less_one by fastforce
        moreover have "b - of_int ⌊b⌋ ∈ {0..<1}" using floor_less_one by fastforce
        ultimately have "(a - of_int ⌊a⌋) + (b - of_int ⌊b⌋) ∈ {0..<2}" unfolding atLeastLessThan_def by simp
        hence "(a + b) - (of_int ⌊a⌋ + of_int ⌊b⌋) ∈ {0..<2}" by (simp add: diff_add_eq)
        hence "⌊a + b - (of_int ⌊a⌋ + of_int ⌊b⌋)⌋ ∈ {0..<2}" by simp
        hence "⌊a + b⌋ - (⌊a⌋ + ⌊b⌋) ∈ {0..<2}" by (metis floor_diff_of_int of_int_add)
      }
      ultimately have "∣u (m + n) - (u m + u n)∣ ≤ 2" by (metis abs_of_nonneg atLeastLessThan_iff nless_le)
    }
    moreover have "u z = - u (- z)" for z unfolding u_def by simp
    ultimately show ?thesis using slope_odd by blast
  qed
  {
    fix s assume "s ∈ S"
    then obtain y where y: "s < y" "y ∈ S" using no_greatest_element by blast
    then obtain m n :: int where *: "s < (of_int m / of_int n)" "(of_int m / of_int n) < y" "n > 0" using eudoxus_dense_rational by blast
    hence n_nonneg: "n ≥ 0" by simp
    {
      fix z :: int assume z_nonneg: "z ≥ 0"
      have "z * m = ⌊of_int (z * n) * (of_int m / of_int n) :: real⌋" using *(3) by simp (auto simp only: of_int_mult[symmetric] floor_of_int)
      also have "... ≤ ⌊of_int (z * n) * y⌋" using *(2) by (meson floor_mono mult_left_mono n_nonneg nless_le of_int_nonneg z_nonneg zero_le_mult_iff)
      also have "... ≤ u (z * n)" using u_Sup_nonneg[OF y(2)] mult_nonneg_nonneg[OF z_nonneg n_nonneg] by blast
      finally have "u (z * n) ≥ z * m" .
    }
    hence "abs_real (u *_e (*) n) ≥ of_int m" using slope unfolding real_of_int eudoxus_times_def by (intro abs_real_leI[where ?N=0]) (auto simp add: mult.commute) 
    moreover have "abs_real u * of_int n = abs_real (u *_e (*) n)" unfolding real_of_int using slope by (simp add: eudoxus_times_def comp_def)
    ultimately have "s ≤ abs_real u" using * by (metis leI mult_imp_div_pos_le of_int_0_less_iff order_le_less_trans order_less_asym)
  }
  moreover
  {
    fix y assume asm: "s ≤ y" if "s ∈ S" for s
    assume "abs_real u > y"
    then obtain m n :: int where *: "y < (of_int m / of_int n)" "(of_int m / of_int n) < abs_real u" "n > 0" using eudoxus_dense_rational by blast
    hence "of_int m < abs_real u * of_int n" by (simp add: pos_divide_less_eq)
    hence "of_int m < abs_real (u *_e (*) n)" unfolding real_of_int using slope by (simp add: eudoxus_times_def comp_def)
    moreover have "slope (u *_e (*) n)" using slope by (simp add: eudoxus_times_def)
    ultimately obtain z where z: "(u *_e (*) n) z > m * z" "z ≥ 1" unfolding real_of_int using abs_real_lessD by blast
    hence **: "u (n * z) > m * z" by (simp add: eudoxus_times_def comp_def)

    obtain x where x: "x ∈ S" "u (n * z) = ⌊of_int (n * z) * x⌋" using u_mem[of "n * z"] zsgn_def[of "n * z"] mult_pos_pos[OF *(3), of z] z(2) by fastforce
    
    have "of_int (n * z) * x ≤ of_int z * of_int n * y" using asm[OF x(1)] using * z by auto
    also have "... < of_int z * of_int m" using * z by (simp add: mult.commute pos_less_divide_eq)
    finally have "of_int (n * z) * x < of_int (m * z)" by (simp add: mult.commute)
    hence False using ** by (metis floor_less_iff less_le_not_le x(2))
  }
  ultimately show ?thesis using that by force
qed blast

end