Theory Real

(*  Title:      HOL/Real.thy
    Author:     Jacques D. Fleuriot, University of Edinburgh, 1998
    Author:     Larry Paulson, University of Cambridge
    Author:     Jeremy Avigad, Carnegie Mellon University
    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    Construction of Cauchy Reals by Brian Huffman, 2010
*)

section Development of the Reals using Cauchy Sequences

theory Real
imports Rat
begin

text 
  This theory contains a formalization of the real numbers as equivalence
  classes of Cauchy sequences of rationals. See the AFP entry
  @{text Dedekind_Real} for an alternative construction using
  Dedekind cuts.



subsection Preliminary lemmas

textUseful in convergence arguments
lemma inverse_of_nat_le:
  fixes n::nat shows "n  m; n0  1 / of_nat m  (1::'a::linordered_field) / of_nat n"
  by (simp add: frac_le)

lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)"
  for a b c d :: "'a::ab_group_add"
  by simp

lemma minus_diff_minus: "- a - - b = - (a - b)"
  for a b :: "'a::ab_group_add"
  by simp

lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b"
  for x y a b :: "'a::ring"
  by (simp add: algebra_simps)

lemma inverse_diff_inverse:
  fixes a b :: "'a::division_ring"
  assumes "a  0" and "b  0"
  shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
  using assms by (simp add: algebra_simps)

lemma obtain_pos_sum:
  fixes r :: rat assumes r: "0 < r"
  obtains s t where "0 < s" and "0 < t" and "r = s + t"
proof
  from r show "0 < r/2" by simp
  from r show "0 < r/2" by simp
  show "r = r/2 + r/2" by simp
qed


subsection Sequences that converge to zero

definition vanishes :: "(nat  rat)  bool"
  where "vanishes X  (r>0. k. nk. ¦X n¦ < r)"

lemma vanishesI: "(r. 0 < r  k. nk. ¦X n¦ < r)  vanishes X"
  unfolding vanishes_def by simp

lemma vanishesD: "vanishes X  0 < r  k. nk. ¦X n¦ < r"
  unfolding vanishes_def by simp

lemma vanishes_const [simp]: "vanishes (λn. c)  c = 0"
proof (cases "c = 0")
  case True
  then show ?thesis
    by (simp add: vanishesI)    
next
  case False
  then show ?thesis
    unfolding vanishes_def
    using zero_less_abs_iff by blast
qed

lemma vanishes_minus: "vanishes X  vanishes (λn. - X n)"
  unfolding vanishes_def by simp

lemma vanishes_add:
  assumes X: "vanishes X"
    and Y: "vanishes Y"
  shows "vanishes (λn. X n + Y n)"
proof (rule vanishesI)
  fix r :: rat
  assume "0 < r"
  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
    by (rule obtain_pos_sum)
  obtain i where i: "ni. ¦X n¦ < s"
    using vanishesD [OF X s] ..
  obtain j where j: "nj. ¦Y n¦ < t"
    using vanishesD [OF Y t] ..
  have "nmax i j. ¦X n + Y n¦ < r"
  proof clarsimp
    fix n
    assume n: "i  n" "j  n"
    have "¦X n + Y n¦  ¦X n¦ + ¦Y n¦"
      by (rule abs_triangle_ineq)
    also have " < s + t"
      by (simp add: add_strict_mono i j n)
    finally show "¦X n + Y n¦ < r"
      by (simp only: r)
  qed
  then show "k. nk. ¦X n + Y n¦ < r" ..
qed

lemma vanishes_diff:
  assumes "vanishes X" "vanishes Y"
  shows "vanishes (λn. X n - Y n)"
  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms)

lemma vanishes_mult_bounded:
  assumes X: "a>0. n. ¦X n¦ < a"
  assumes Y: "vanishes (λn. Y n)"
  shows "vanishes (λn. X n * Y n)"
proof (rule vanishesI)
  fix r :: rat
  assume r: "0 < r"
  obtain a where a: "0 < a" "n. ¦X n¦ < a"
    using X by blast
  obtain b where b: "0 < b" "r = a * b"
  proof
    show "0 < r / a" using r a by simp
    show "r = a * (r / a)" using a by simp
  qed
  obtain k where k: "nk. ¦Y n¦ < b"
    using vanishesD [OF Y b(1)] ..
  have "nk. ¦X n * Y n¦ < r"
    by (simp add: b(2) abs_mult mult_strict_mono' a k)
  then show "k. nk. ¦X n * Y n¦ < r" ..
qed


subsection Cauchy sequences

definition cauchy :: "(nat  rat)  bool"
  where "cauchy X  (r>0. k. mk. nk. ¦X m - X n¦ < r)"

lemma cauchyI: "(r. 0 < r  k. mk. nk. ¦X m - X n¦ < r)  cauchy X"
  unfolding cauchy_def by simp

lemma cauchyD: "cauchy X  0 < r  k. mk. nk. ¦X m - X n¦ < r"
  unfolding cauchy_def by simp

lemma cauchy_const [simp]: "cauchy (λn. x)"
  unfolding cauchy_def by simp

lemma cauchy_add [simp]:
  assumes X: "cauchy X" and Y: "cauchy Y"
  shows "cauchy (λn. X n + Y n)"
proof (rule cauchyI)
  fix r :: rat
  assume "0 < r"
  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
    by (rule obtain_pos_sum)
  obtain i where i: "mi. ni. ¦X m - X n¦ < s"
    using cauchyD [OF X s] ..
  obtain j where j: "mj. nj. ¦Y m - Y n¦ < t"
    using cauchyD [OF Y t] ..
  have "mmax i j. nmax i j. ¦(X m + Y m) - (X n + Y n)¦ < r"
  proof clarsimp
    fix m n
    assume *: "i  m" "j  m" "i  n" "j  n"
    have "¦(X m + Y m) - (X n + Y n)¦  ¦X m - X n¦ + ¦Y m - Y n¦"
      unfolding add_diff_add by (rule abs_triangle_ineq)
    also have " < s + t"
      by (rule add_strict_mono) (simp_all add: i j *)
    finally show "¦(X m + Y m) - (X n + Y n)¦ < r" by (simp only: r)
  qed
  then show "k. mk. nk. ¦(X m + Y m) - (X n + Y n)¦ < r" ..
qed

lemma cauchy_minus [simp]:
  assumes X: "cauchy X"
  shows "cauchy (λn. - X n)"
  using assms unfolding cauchy_def
  unfolding minus_diff_minus abs_minus_cancel .

lemma cauchy_diff [simp]:
  assumes "cauchy X" "cauchy Y"
  shows "cauchy (λn. X n - Y n)"
  using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff)

lemma cauchy_imp_bounded:
  assumes "cauchy X"
  shows "b>0. n. ¦X n¦ < b"
proof -
  obtain k where k: "mk. nk. ¦X m - X n¦ < 1"
    using cauchyD [OF assms zero_less_one] ..
  show "b>0. n. ¦X n¦ < b"
  proof (intro exI conjI allI)
    have "0  ¦X 0¦" by simp
    also have "¦X 0¦  Max (abs ` X ` {..k})" by simp
    finally have "0  Max (abs ` X ` {..k})" .
    then show "0 < Max (abs ` X ` {..k}) + 1" by simp
  next
    fix n :: nat
    show "¦X n¦ < Max (abs ` X ` {..k}) + 1"
    proof (rule linorder_le_cases)
      assume "n  k"
      then have "¦X n¦  Max (abs ` X ` {..k})" by simp
      then show "¦X n¦ < Max (abs ` X ` {..k}) + 1" by simp
    next
      assume "k  n"
      have "¦X n¦ = ¦X k + (X n - X k)¦" by simp
      also have "¦X k + (X n - X k)¦  ¦X k¦ + ¦X n - X k¦"
        by (rule abs_triangle_ineq)
      also have " < Max (abs ` X ` {..k}) + 1"
        by (rule add_le_less_mono) (simp_all add: k k  n)
      finally show "¦X n¦ < Max (abs ` X ` {..k}) + 1" .
    qed
  qed
qed

lemma cauchy_mult [simp]:
  assumes X: "cauchy X" and Y: "cauchy Y"
  shows "cauchy (λn. X n * Y n)"
proof (rule cauchyI)
  fix r :: rat assume "0 < r"
  then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
    by (rule obtain_pos_sum)
  obtain a where a: "0 < a" "n. ¦X n¦ < a"
    using cauchy_imp_bounded [OF X] by blast
  obtain b where b: "0 < b" "n. ¦Y n¦ < b"
    using cauchy_imp_bounded [OF Y] by blast
  obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
  proof
    show "0 < v/b" using v b(1) by simp
    show "0 < u/a" using u a(1) by simp
    show "r = a * (u/a) + (v/b) * b"
      using a(1) b(1) r = u + v by simp
  qed
  obtain i where i: "mi. ni. ¦X m - X n¦ < s"
    using cauchyD [OF X s] ..
  obtain j where j: "mj. nj. ¦Y m - Y n¦ < t"
    using cauchyD [OF Y t] ..
  have "mmax i j. nmax i j. ¦X m * Y m - X n * Y n¦ < r"
  proof clarsimp
    fix m n
    assume *: "i  m" "j  m" "i  n" "j  n"
    have "¦X m * Y m - X n * Y n¦ = ¦X m * (Y m - Y n) + (X m - X n) * Y n¦"
      unfolding mult_diff_mult ..
    also have "  ¦X m * (Y m - Y n)¦ + ¦(X m - X n) * Y n¦"
      by (rule abs_triangle_ineq)
    also have " = ¦X m¦ * ¦Y m - Y n¦ + ¦X m - X n¦ * ¦Y n¦"
      unfolding abs_mult ..
    also have " < a * t + s * b"
      by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
    finally show "¦X m * Y m - X n * Y n¦ < r"
      by (simp only: r)
  qed
  then show "k. mk. nk. ¦X m * Y m - X n * Y n¦ < r" ..
qed

lemma cauchy_not_vanishes_cases:
  assumes X: "cauchy X"
  assumes nz: "¬ vanishes X"
  shows "b>0. k. (nk. b < - X n)  (nk. b < X n)"
proof -
  obtain r where "0 < r" and r: "k. nk. r  ¦X n¦"
    using nz unfolding vanishes_def by (auto simp add: not_less)
  obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"
    using 0 < r by (rule obtain_pos_sum)
  obtain i where i: "mi. ni. ¦X m - X n¦ < s"
    using cauchyD [OF X s] ..
  obtain k where "i  k" and "r  ¦X k¦"
    using r by blast
  have k: "nk. ¦X n - X k¦ < s"
    using i i  k by auto
  have "X k  - r  r  X k"
    using r  ¦X k¦ by auto
  then have "(nk. t < - X n)  (nk. t < X n)"
    unfolding r = s + t using k by auto
  then have "k. (nk. t < - X n)  (nk. t < X n)" ..
  then show "t>0. k. (nk. t < - X n)  (nk. t < X n)"
    using t by auto
qed

lemma cauchy_not_vanishes:
  assumes X: "cauchy X"
    and nz: "¬ vanishes X"
  shows "b>0. k. nk. b < ¦X n¦"
  using cauchy_not_vanishes_cases [OF assms]
  by (elim ex_forward conj_forward asm_rl) auto

lemma cauchy_inverse [simp]:
  assumes X: "cauchy X"
    and nz: "¬ vanishes X"
  shows "cauchy (λn. inverse (X n))"
proof (rule cauchyI)
  fix r :: rat
  assume "0 < r"
  obtain b i where b: "0 < b" and i: "ni. b < ¦X n¦"
    using cauchy_not_vanishes [OF X nz] by blast
  from b i have nz: "ni. X n  0" by auto
  obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
  proof
    show "0 < b * r * b" by (simp add: 0 < r b)
    show "r = inverse b * (b * r * b) * inverse b"
      using b by simp
  qed
  obtain j where j: "mj. nj. ¦X m - X n¦ < s"
    using cauchyD [OF X s] ..
  have "mmax i j. nmax i j. ¦inverse (X m) - inverse (X n)¦ < r"
  proof clarsimp
    fix m n
    assume *: "i  m" "j  m" "i  n" "j  n"
    have "¦inverse (X m) - inverse (X n)¦ = inverse ¦X m¦ * ¦X m - X n¦ * inverse ¦X n¦"
      by (simp add: inverse_diff_inverse nz * abs_mult)
    also have " < inverse b * s * inverse b"
      by (simp add: mult_strict_mono less_imp_inverse_less i j b * s)
    finally show "¦inverse (X m) - inverse (X n)¦ < r" by (simp only: r)
  qed
  then show "k. mk. nk. ¦inverse (X m) - inverse (X n)¦ < r" ..
qed

lemma vanishes_diff_inverse:
  assumes X: "cauchy X" "¬ vanishes X"
    and Y: "cauchy Y" "¬ vanishes Y"
    and XY: "vanishes (λn. X n - Y n)"
  shows "vanishes (λn. inverse (X n) - inverse (Y n))"
proof (rule vanishesI)
  fix r :: rat
  assume r: "0 < r"
  obtain a i where a: "0 < a" and i: "ni. a < ¦X n¦"
    using cauchy_not_vanishes [OF X] by blast
  obtain b j where b: "0 < b" and j: "nj. b < ¦Y n¦"
    using cauchy_not_vanishes [OF Y] by blast
  obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
  proof
    show "0 < a * r * b"
      using a r b by simp
    show "inverse a * (a * r * b) * inverse b = r"
      using a r b by simp
  qed
  obtain k where k: "nk. ¦X n - Y n¦ < s"
    using vanishesD [OF XY s] ..
  have "nmax (max i j) k. ¦inverse (X n) - inverse (Y n)¦ < r"
  proof clarsimp
    fix n
    assume n: "i  n" "j  n" "k  n"
    with i j a b have "X n  0" and "Y n  0"
      by auto
    then have "¦inverse (X n) - inverse (Y n)¦ = inverse ¦X n¦ * ¦X n - Y n¦ * inverse ¦Y n¦"
      by (simp add: inverse_diff_inverse abs_mult)
    also have " < inverse a * s * inverse b"
      by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n)
    also note inverse a * s * inverse b = r
    finally show "¦inverse (X n) - inverse (Y n)¦ < r" .
  qed
  then show "k. nk. ¦inverse (X n) - inverse (Y n)¦ < r" ..
qed


subsection Equivalence relation on Cauchy sequences

definition realrel :: "(nat  rat)  (nat  rat)  bool"
  where "realrel = (λX Y. cauchy X  cauchy Y  vanishes (λn. X n - Y n))"

lemma realrelI [intro?]: "cauchy X  cauchy Y  vanishes (λn. X n - Y n)  realrel X Y"
  by (simp add: realrel_def)

lemma realrel_refl: "cauchy X  realrel X X"
  by (simp add: realrel_def)

lemma symp_realrel: "symp realrel"
  by (simp add: abs_minus_commute realrel_def symp_def vanishes_def)

lemma transp_realrel: "transp realrel"
  unfolding realrel_def
  by (rule transpI) (force simp add: dest: vanishes_add)

lemma part_equivp_realrel: "part_equivp realrel"
  by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const)


subsection The field of real numbers

quotient_type real = "nat  rat" / partial: realrel
  morphisms rep_real Real
  by (rule part_equivp_realrel)

lemma cr_real_eq: "pcr_real = (λx y. cauchy x  Real x = y)"
  unfolding real.pcr_cr_eq cr_real_def realrel_def by auto

lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
  assumes "X. cauchy X  P (Real X)"
  shows "P x"
proof (induct x)
  case (1 X)
  then have "cauchy X" by (simp add: realrel_def)
  then show "P (Real X)" by (rule assms)
qed

lemma eq_Real: "cauchy X  cauchy Y  Real X = Real Y  vanishes (λn. X n - Y n)"
  using real.rel_eq_transfer
  unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp

lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
  by (simp add: real.domain_eq realrel_def)

instantiation real :: field
begin

lift_definition zero_real :: "real" is "λn. 0"
  by (simp add: realrel_refl)

lift_definition one_real :: "real" is "λn. 1"
  by (simp add: realrel_refl)

lift_definition plus_real :: "real  real  real" is "λX Y n. X n + Y n"
  unfolding realrel_def add_diff_add
  by (simp only: cauchy_add vanishes_add simp_thms)

lift_definition uminus_real :: "real  real" is "λX n. - X n"
  unfolding realrel_def minus_diff_minus
  by (simp only: cauchy_minus vanishes_minus simp_thms)

lift_definition times_real :: "real  real  real" is "λX Y n. X n * Y n"
proof -
  fix f1 f2 f3 f4
  have "cauchy f1; cauchy f4; vanishes (λn. f1 n - f2 n); vanishes (λn. f3 n - f4 n)
        vanishes (λn. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))"
    by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded)
  then show "realrel f1 f2; realrel f3 f4  realrel (λn. f1 n * f3 n) (λn. f2 n * f4 n)"
    by (simp add: mult.commute realrel_def mult_diff_mult)
qed

lift_definition inverse_real :: "real  real"
  is "λX. if vanishes X then (λn. 0) else (λn. inverse (X n))"
proof -
  fix X Y
  assume "realrel X Y"
  then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (λn. X n - Y n)"
    by (simp_all add: realrel_def)
  have "vanishes X  vanishes Y"
  proof
    assume "vanishes X"
    from vanishes_diff [OF this XY] show "vanishes Y"
      by simp
  next
    assume "vanishes Y"
    from vanishes_add [OF this XY] show "vanishes X"
      by simp
  qed
  then show "?thesis X Y"
    by (simp add: vanishes_diff_inverse X Y XY realrel_def)
qed

definition "x - y = x + - y" for x y :: real

definition "x div y = x * inverse y" for x y :: real

lemma add_Real: "cauchy X  cauchy Y  Real X + Real Y = Real (λn. X n + Y n)"
  using plus_real.transfer by (simp add: cr_real_eq rel_fun_def)

lemma minus_Real: "cauchy X  - Real X = Real (λn. - X n)"
  using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def)

lemma diff_Real: "cauchy X  cauchy Y  Real X - Real Y = Real (λn. X n - Y n)"
  by (simp add: minus_Real add_Real minus_real_def)

lemma mult_Real: "cauchy X  cauchy Y  Real X * Real Y = Real (λn. X n * Y n)"
  using times_real.transfer by (simp add: cr_real_eq rel_fun_def)

lemma inverse_Real:
  "cauchy X  inverse (Real X) = (if vanishes X then 0 else Real (λn. inverse (X n)))"
  using inverse_real.transfer zero_real.transfer
  unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis)

instance
proof
  fix a b c :: real
  show "a + b = b + a"
    by transfer (simp add: ac_simps realrel_def)
  show "(a + b) + c = a + (b + c)"
    by transfer (simp add: ac_simps realrel_def)
  show "0 + a = a"
    by transfer (simp add: realrel_def)
  show "- a + a = 0"
    by transfer (simp add: realrel_def)
  show "a - b = a + - b"
    by (rule minus_real_def)
  show "(a * b) * c = a * (b * c)"
    by transfer (simp add: ac_simps realrel_def)
  show "a * b = b * a"
    by transfer (simp add: ac_simps realrel_def)
  show "1 * a = a"
    by transfer (simp add: ac_simps realrel_def)
  show "(a + b) * c = a * c + b * c"
    by transfer (simp add: distrib_right realrel_def)
  show "(0::real)  (1::real)"
    by transfer (simp add: realrel_def)
  have "vanishes (λn. inverse (X n) * X n - 1)" if X: "cauchy X" "¬ vanishes X" for X
  proof (rule vanishesI)
    fix r::rat
    assume "0 < r"
    obtain b k where "b>0" "nk. b < ¦X n¦"
      using X cauchy_not_vanishes by blast
    then show "k. nk. ¦inverse (X n) * X n - 1¦ < r" 
      using 0 < r by force
  qed
  then show "a  0  inverse a * a = 1"
    by transfer (simp add: realrel_def)
  show "a div b = a * inverse b"
    by (rule divide_real_def)
  show "inverse (0::real) = 0"
    by transfer (simp add: realrel_def)
qed

end


subsection Positive reals

lift_definition positive :: "real  bool"
  is "λX. r>0. k. nk. r < X n"
proof -
  have 1: "r>0. k. nk. r < Y n"
    if *: "realrel X Y" and **: "r>0. k. nk. r < X n" for X Y
  proof -
    from * have XY: "vanishes (λn. X n - Y n)"
      by (simp_all add: realrel_def)
    from ** obtain r i where "0 < r" and i: "ni. r < X n"
      by blast
    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
      using 0 < r by (rule obtain_pos_sum)
    obtain j where j: "nj. ¦X n - Y n¦ < s"
      using vanishesD [OF XY s] ..
    have "nmax i j. t < Y n"
    proof clarsimp
      fix n
      assume n: "i  n" "j  n"
      have "¦X n - Y n¦ < s" and "r < X n"
        using i j n by simp_all
      then show "t < Y n" by (simp add: r)
    qed
    then show ?thesis using t by blast
  qed
  fix X Y assume "realrel X Y"
  then have "realrel X Y" and "realrel Y X"
    using symp_realrel by (auto simp: symp_def)
  then show "?thesis X Y"
    by (safe elim!: 1)
qed

lemma positive_Real: "cauchy X  positive (Real X)  (r>0. k. nk. r < X n)"
  using positive.transfer by (simp add: cr_real_eq rel_fun_def)

lemma positive_zero: "¬ positive 0"
  by transfer auto

lemma positive_add: 
  assumes "positive x" "positive y" shows "positive (x + y)"
proof -
  have *: "ni. a < x n; nj. b < y n; 0 < a; 0 < b; n  max i j
        a+b < x n + y n" for x y and a b::rat and i j n::nat
    by (simp add: add_strict_mono)
  show ?thesis
    using assms
    by transfer (blast intro: * pos_add_strict)
qed

lemma positive_mult: 
  assumes "positive x" "positive y" shows "positive (x * y)"
proof -
  have *: "ni. a < x n; nj. b < y n; 0 < a; 0 < b; n  max i j
        a*b < x n * y n" for x y and a b::rat and i j n::nat
    by (simp add: mult_strict_mono')
  show ?thesis
    using assms
    by transfer (blast intro: *  mult_pos_pos)
qed

lemma positive_minus: "¬ positive x  x  0  positive (- x)"
  apply transfer
  apply (simp add: realrel_def)
  apply (blast dest: cauchy_not_vanishes_cases)
  done

instantiation real :: linordered_field
begin

definition "x < y  positive (y - x)"

definition "x  y  x < y  x = y" for x y :: real

definition "¦a¦ = (if a < 0 then - a else a)" for a :: real

definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real

instance
proof
  fix a b c :: real
  show "¦a¦ = (if a < 0 then - a else a)"
    by (rule abs_real_def)
  show "a < b  a  b  ¬ b  a"
       "a  b  b  c  a  c"  "a  a" 
       "a  b  b  a  a = b"
       "a  b  c + a  c + b"
    unfolding less_eq_real_def less_real_def
    by (force simp add: positive_zero dest: positive_add)+
  show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
    by (rule sgn_real_def)
  show "a  b  b  a"
    by (auto dest!: positive_minus simp: less_eq_real_def less_real_def)
  show "a < b  0 < c  c * a < c * b"
    unfolding less_real_def
    by (force simp add: algebra_simps dest: positive_mult)
qed

end

instantiation real :: distrib_lattice
begin

definition "(inf :: real  real  real) = min"

definition "(sup :: real  real  real) = max"

instance
  by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)

end

lemma of_nat_Real: "of_nat x = Real (λn. of_nat x)"
  by (induct x) (simp_all add: zero_real_def one_real_def add_Real)

lemma of_int_Real: "of_int x = Real (λn. of_int x)"
  by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real)

lemma of_rat_Real: "of_rat x = Real (λn. x)"
proof (induct x)
  case (Fract a b)
  then show ?case 
  apply (simp add: Fract_of_int_quotient of_rat_divide)
  apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real)
  done
qed

instance real :: archimedean_field
proof
  show "z. x  of_int z" for x :: real
  proof (induct x)
    case (1 X)
    then obtain b where "0 < b" and b: "n. ¦X n¦ < b"
      by (blast dest: cauchy_imp_bounded)
    then have "Real X < of_int (b + 1)"
      using 1
      apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
      apply (rule_tac x=1 in exI)
      apply (simp add: algebra_simps)
      by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le)
    then show ?case
      using less_eq_real_def by blast 
  qed
qed

instantiation real :: floor_ceiling
begin

definition [code del]: "x::real = (THE z. of_int z  x  x < of_int (z + 1))"

instance
proof
  show "of_int x  x  x < of_int (x + 1)" for x :: real
    unfolding floor_real_def using floor_exists1 by (rule theI')
qed

end


subsection Completeness

lemma not_positive_Real: 
  assumes "cauchy X" shows "¬ positive (Real X)  (r>0. k. nk. X n  r)" (is "?lhs = ?rhs")
  unfolding positive_Real [OF assms]
proof (intro iffI allI notI impI)
  show "k. nk. X n  r" if r: "¬ (r>0. k. nk. r < X n)" and "0 < r" for r
  proof -
    obtain s t where "s > 0" "t > 0" "r = s+t"
      using r > 0 obtain_pos_sum by blast
    obtain k where k: "m n. mk; nk  ¦X m - X n¦ < t"
      using cauchyD [OF assms t > 0] by blast
    obtain n where "n  k" "X n  s"
      by (meson r 0 < s not_less)
    then have "X l  r" if "l  n" for l
      using k [OF n  k, of l] that r = s+t by linarith
    then show ?thesis
      by blast
    qed
qed (meson le_cases not_le)

lemma le_Real:
  assumes "cauchy X" "cauchy Y"
  shows "Real X  Real Y = (r>0. k. nk. X n  Y n + r)"
  unfolding not_less [symmetric, where 'a=real] less_real_def
  apply (simp add: diff_Real not_positive_Real assms)
  apply (simp add: diff_le_eq ac_simps)
  done

lemma le_RealI:
  assumes Y: "cauchy Y"
  shows "n. x  of_rat (Y n)  x  Real Y"
proof (induct x)
  fix X
  assume X: "cauchy X" and "n. Real X  of_rat (Y n)"
  then have le: "m r. 0 < r  k. nk. X n  Y m + r"
    by (simp add: of_rat_Real le_Real)
  then have "k. nk. X n  Y n + r" if "0 < r" for r :: rat
  proof -
    from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
      by (rule obtain_pos_sum)
    obtain i where i: "mi. ni. ¦Y m - Y n¦ < s"
      using cauchyD [OF Y s] ..
    obtain j where j: "nj. X n  Y i + t"
      using le [OF t] ..
    have "nmax i j. X n  Y n + r"
    proof clarsimp
      fix n
      assume n: "i  n" "j  n"
      have "X n  Y i + t"
        using n j by simp
      moreover have "¦Y i - Y n¦ < s"
        using n i by simp
      ultimately show "X n  Y n + r"
        unfolding r by simp
    qed
    then show ?thesis ..
  qed
  then show "Real X  Real Y"
    by (simp add: of_rat_Real le_Real X Y)
qed

lemma Real_leI:
  assumes X: "cauchy X"
  assumes le: "n. of_rat (X n)  y"
  shows "Real X  y"
proof -
  have "- y  - Real X"
    by (simp add: minus_Real X le_RealI of_rat_minus le)
  then show ?thesis by simp
qed

lemma less_RealD:
  assumes "cauchy Y"
  shows "x < Real Y  n. x < of_rat (Y n)"
  apply (erule contrapos_pp)
  apply (simp add: not_less)
  apply (erule Real_leI [OF assms])
  done

lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n"
  apply (induct n)
   apply simp
  apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
  done

lemma complete_real:
  fixes S :: "real set"
  assumes "x. x  S" and "z. xS. x  z"
  shows "y. (xS. x  y)  (z. (xS. x  z)  y  z)"
proof -
  obtain x where x: "x  S" using assms(1) ..
  obtain z where z: "xS. x  z" using assms(2) ..

  define P where "P x  (yS. y  of_rat x)" for x
  obtain a where a: "¬ P a"
  proof
    have "of_int x - 1  x - 1" by (rule of_int_floor_le)
    also have "x - 1 < x" by simp
    finally have "of_int x - 1 < x" .
    then have "¬ x  of_int x - 1" by (simp only: not_le)
    then show "¬ P (of_int x - 1)"
      unfolding P_def of_rat_of_int_eq using x by blast
  qed
  obtain b where b: "P b"
  proof
    show "P (of_int z)"
    unfolding P_def of_rat_of_int_eq
    proof
      fix y assume "y  S"
      then have "y  z" using z by simp
      also have "z  of_int z" by (rule le_of_int_ceiling)
      finally show "y  of_int z" .
    qed
  qed

  define avg where "avg x y = x/2 + y/2" for x y :: rat
  define bisect where "bisect = (λ(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))"
  define A where "A n = fst ((bisect ^^ n) (a, b))" for n
  define B where "B n = snd ((bisect ^^ n) (a, b))" for n
  define C where "C n = avg (A n) (B n)" for n
  have A_0 [simp]: "A 0 = a" unfolding A_def by simp
  have B_0 [simp]: "B 0 = b" unfolding B_def by simp
  have A_Suc [simp]: "n. A (Suc n) = (if P (C n) then A n else C n)"
    unfolding A_def B_def C_def bisect_def split_def by simp
  have B_Suc [simp]: "n. B (Suc n) = (if P (C n) then C n else B n)"
    unfolding A_def B_def C_def bisect_def split_def by simp

  have width: "B n - A n = (b - a) / 2^n" for n
  proof (induct n)
    case (Suc n)
    then show ?case
      by (simp add: C_def eq_divide_eq avg_def algebra_simps)
  qed simp
  have twos: "n. y / 2 ^ n < r" if "0 < r" for y r :: rat
  proof -
    obtain n where "y / r < rat_of_nat n"
      using 0 < r reals_Archimedean2 by blast
    then have "n. y < r * 2 ^ n"
      by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that)
    then show ?thesis
      by (simp add: field_split_simps)
  qed
  have PA: "¬ P (A n)" for n
    by (induct n) (simp_all add: a)
  have PB: "P (B n)" for n
    by (induct n) (simp_all add: b)
  have ab: "a < b"
    using a b unfolding P_def
    by (meson leI less_le_trans of_rat_less)
  have AB: "A n < B n" for n
    by (induct n) (simp_all add: ab C_def avg_def)
  have  "A i  A j   B j  B i" if "i < j" for i j
    using that
  proof (induction rule: less_Suc_induct)
    case (1 i)
    then show ?case
      apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric])
      apply (rule AB [THEN less_imp_le])
      done  
  qed simp
  then have A_mono: "A i  A j" and B_mono: "B j  B i" if "i  j" for i j
    by (metis eq_refl le_neq_implies_less that)+
  have cauchy_lemma: "cauchy X" if *: "n i. in  A n  X i  X i  B n" for X
  proof (rule cauchyI)
    fix r::rat
    assume "0 < r"
    then obtain k where k: "(b - a) / 2 ^ k < r"
      using twos by blast
    have "¦X m - X n¦ < r" if "mk" "nk" for m n
    proof -
      have "¦X m - X n¦  B k - A k"
        by (simp add: * abs_rat_def diff_mono that)
      also have "... < r"
        by (simp add: k width)
      finally show ?thesis .
    qed
    then show "k. mk. nk. ¦X m - X n¦ < r"
      by blast 
  qed
  have "cauchy A"
    by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans)
  have "cauchy B"
    by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans)
  have "xS. x  Real B"
  proof
    fix x
    assume "x  S"
    then show "x  Real B"
      using PB [unfolded P_def] cauchy B
      by (simp add: le_RealI)
  qed
  moreover have "z. (xS. x  z)  Real A  z"
    by (meson PA Real_leI P_def cauchy A le_cases order.trans)
  moreover have "vanishes (λn. (b - a) / 2 ^ n)"
  proof (rule vanishesI)
    fix r :: rat
    assume "0 < r"
    then obtain k where k: "¦b - a¦ / 2 ^ k < r"
      using twos by blast
    have "nk. ¦(b - a) / 2 ^ n¦ < r"
    proof clarify
      fix n
      assume n: "k  n"
      have "¦(b - a) / 2 ^ n¦ = ¦b - a¦ / 2 ^ n"
        by simp
      also have "  ¦b - a¦ / 2 ^ k"
        using n by (simp add: divide_left_mono)
      also note k
      finally show "¦(b - a) / 2 ^ n¦ < r" .
    qed
    then show "k. nk. ¦(b - a) / 2 ^ n¦ < r" ..
  qed
  then have "Real B = Real A"
    by (simp add: eq_Real cauchy A cauchy B width)
  ultimately show "y. (xS. x  y)  (z. (xS. x  z)  y  z)"
    by force
qed

instantiation real :: linear_continuum
begin

subsection Supremum of a set of reals

definition "Sup X = (LEAST z::real. xX. x  z)"
definition "Inf X = - Sup (uminus ` X)" for X :: "real set"

instance
proof
  show Sup_upper: "x  Sup X"
    if "x  X" "bdd_above X"
    for x :: real and X :: "real set"
  proof -
    from that obtain s where s: "yX. y  s" "z. yX. y  z  s  z"
      using complete_real[of X] unfolding bdd_above_def by blast
    then show ?thesis
      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that)
  qed
  show Sup_least: "Sup X  z"
    if "X  {}" and z: "x. x  X  x  z"
    for z :: real and X :: "real set"
  proof -
    from that obtain s where s: "yX. y  s" "z. yX. y  z  s  z"
      using complete_real [of X] by blast
    then have "Sup X = s"
      unfolding Sup_real_def by (best intro: Least_equality)
    also from s z have "  z"
      by blast
    finally show ?thesis .
  qed
  show "Inf X  x" if "x  X" "bdd_below X"
    for x :: real and X :: "real set"
    using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that)
  show "z  Inf X" if "X  {}" "x. x  X  z  x"
    for z :: real and X :: "real set"
    using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that)
  show "a b::real. a  b"
    using zero_neq_one by blast
qed

end


subsection Hiding implementation details

hide_const (open) vanishes cauchy positive Real

declare Real_induct [induct del]
declare Abs_real_induct [induct del]
declare Abs_real_cases [cases del]

lifting_update real.lifting
lifting_forget real.lifting


subsection Embedding numbers into the Reals

abbreviation real_of_nat :: "nat  real"
  where "real_of_nat  of_nat"

abbreviation real :: "nat  real"
  where "real  of_nat"

abbreviation real_of_int :: "int  real"
  where "real_of_int  of_int"

abbreviation real_of_rat :: "rat  real"
  where "real_of_rat  of_rat"

declare [[coercion_enabled]]

declare [[coercion "of_nat :: nat  int"]]
declare [[coercion "of_nat :: nat  real"]]
declare [[coercion "of_int :: int  real"]]

(* We do not add rat to the coerced types, this has often unpleasant side effects when writing
inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *)

declare [[coercion_map map]]
declare [[coercion_map "λf g h x. g (h (f x))"]]
declare [[coercion_map "λf g (x,y). (f x, g y)"]]

declare of_int_eq_0_iff [algebra, presburger]
declare of_int_eq_1_iff [algebra, presburger]
declare of_int_eq_iff [algebra, presburger]
declare of_int_less_0_iff [algebra, presburger]
declare of_int_less_1_iff [algebra, presburger]
declare of_int_less_iff [algebra, presburger]
declare of_int_le_0_iff [algebra, presburger]
declare of_int_le_1_iff [algebra, presburger]
declare of_int_le_iff [algebra, presburger]
declare of_int_0_less_iff [algebra, presburger]
declare of_int_0_le_iff [algebra, presburger]
declare of_int_1_less_iff [algebra, presburger]
declare of_int_1_le_iff [algebra, presburger]

lemma int_less_real_le: "n < m  real_of_int n + 1  real_of_int m"
proof -
  have "(0::real)  1"
    by (metis less_eq_real_def zero_less_one)
  then show ?thesis
    by (metis floor_of_int less_floor_iff)
qed

lemma int_le_real_less: "n  m  real_of_int n < real_of_int m + 1"
  by (meson int_less_real_le not_le)

lemma real_of_int_div_aux:
  "(real_of_int x) / (real_of_int d) =
    real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)"
proof -
  have "x = (x div d) * d + x mod d"
    by auto
  then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)"
    by (metis of_int_add of_int_mult)
  then have "real_of_int x / real_of_int d =  / real_of_int d"
    by simp
  then show ?thesis
    by (auto simp add: add_divide_distrib algebra_simps)
qed

lemma real_of_int_div:
  "d dvd n  real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int
  by (simp add: real_of_int_div_aux)

lemma real_of_int_div2: "0  real_of_int n / real_of_int x - real_of_int (n div x)"
proof (cases "x = 0")
  case False
  then show ?thesis
    by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le)
qed simp

lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x)  1"
  apply (simp add: algebra_simps)
  by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add)

lemma real_of_int_div4: "real_of_int (n div x)  real_of_int n / real_of_int x"
  using real_of_int_div2 [of n x] by simp


subsection Embedding the Naturals into the Reals

lemma real_of_card: "real (card A) = sum (λx. 1) A"
  by simp

lemma nat_less_real_le: "n < m  real n + 1  real m"
  by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)

lemma nat_le_real_less: "n  m  real n < real m + 1"
  for m n :: nat
  by (meson nat_less_real_le not_le)

lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d"
proof -
  have "x = (x div d) * d + x mod d"
    by auto
  then have "real x = real (x div d) * real d + real(x mod d)"
    by (metis of_nat_add of_nat_mult)
  then have "real x / real d =  / real d"
    by simp
  then show ?thesis
    by (auto simp add: add_divide_distrib algebra_simps)
qed

lemma real_of_nat_div: "d dvd n  real(n div d) = real n / real d"
  by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric])

lemma real_of_nat_div2: "0  real n / real x - real (n div x)" for n x :: nat
  apply (simp add: algebra_simps)
  by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq)

lemma real_of_nat_div3: "real n / real x - real (n div x)  1" for n x :: nat
proof (cases "x = 0")
  case False
  then show ?thesis
    by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int)
qed auto

lemma real_of_nat_div4: "real (n div x)  real n / real x" for n x :: nat
  using real_of_nat_div2 [of n x] by simp


subsection The Archimedean Property of the Reals

lemma real_arch_inverse: "0 < e  (n::nat. n  0  0 < inverse (real n)  inverse (real n) < e)"
  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)

lemma reals_Archimedean3: "0 < x  y. n. y < real n * x"
  by (auto intro: ex_less_of_nat_mult)

lemma real_archimedian_rdiv_eq_0:
  assumes x0: "x  0"
    and c: "c  0"
    and xc: "m::nat. m > 0  real m * x  c"
  shows "x = 0"
  by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)


subsection Rationals

lemma Rats_abs_iff[simp]:
  "¦(x::real)¦    x  "
by(simp add: abs_real_def split: if_splits)

lemma Rats_eq_int_div_int: " = {real_of_int i / real_of_int j | i j. j  0}"  (is "_ = ?S")
proof
  show "  ?S"
  proof
    fix x :: real
    assume "x  "
    then obtain r where "x = of_rat r"
      unfolding Rats_def ..
    have "of_rat r  ?S"
      by (cases r) (auto simp add: of_rat_rat)
    then show "x  ?S"
      using x = of_rat r by simp
  qed
next
  show "?S  "
  proof (auto simp: Rats_def)
    fix i j :: int
    assume "j  0"
    then have "real_of_int i / real_of_int j = of_rat (Fract i j)"
      by (simp add: of_rat_rat)
    then show "real_of_int i / real_of_int j  range of_rat"
      by blast
  qed
qed

lemma Rats_eq_int_div_nat: " = { real_of_int i / real n | i n. n  0}"
proof (auto simp: Rats_eq_int_div_int)
  fix i j :: int
  assume "j  0"
  show "(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n  0 < n"
  proof (cases "j > 0")
    case True
    then have "real_of_int i / real_of_int j = real_of_int i / real (nat j)  0 < nat j"
      by simp
    then show ?thesis by blast
  next
    case False
    with j  0
    have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j))  0 < nat (- j)"
      by simp
    then show ?thesis by blast
  qed
next
  fix i :: int and n :: nat
  assume "0 < n"
  then have "real_of_int i / real n = real_of_int i / real_of_int(int n)  int n  0"
    by simp
  then show "i' j. real_of_int i / real n = real_of_int i' / real_of_int j  j  0"
    by blast
qed

lemma Rats_abs_nat_div_natE:
  assumes "x  "
  obtains m n :: nat where "n  0" and "¦x¦ = real m / real n" and "coprime m n"
proof -
  from x   obtain i :: int and n :: nat where "n  0" and "x = real_of_int i / real n"
    by (auto simp add: Rats_eq_int_div_nat)
  then have "¦x¦ = real (nat ¦i¦) / real n" by simp
  then obtain m :: nat where x_rat: "¦x¦ = real m / real n" by blast
  let ?gcd = "gcd m n"
  from n  0 have gcd: "?gcd  0" by simp
  let ?k = "m div ?gcd"
  let ?l = "n div ?gcd"
  let ?gcd' = "gcd ?k ?l"
  have "?gcd dvd m" ..
  then have gcd_k: "?gcd * ?k = m"
    by (rule dvd_mult_div_cancel)
  have "?gcd dvd n" ..
  then have gcd_l: "?gcd * ?l = n"
    by (rule dvd_mult_div_cancel)
  from n  0 and gcd_l have "?gcd * ?l  0" by simp
  then have "?l  0" by (blast dest!: mult_not_zero)
  moreover
  have "¦x¦ = real ?k / real ?l"
  proof -
    from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)"
      by (simp add: real_of_nat_div)
    also from gcd_k and gcd_l have " = real m / real n" by simp
    also from x_rat have " = ¦x¦" ..
    finally show ?thesis ..
  qed
  moreover
  have "?gcd' = 1"
  proof -
    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
      by (rule gcd_mult_distrib_nat)
    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    with gcd show ?thesis by auto
  qed
  then have "coprime ?k ?l"
    by (simp only: coprime_iff_gcd_eq_1)
  ultimately show ?thesis ..
qed


subsection Density of the Rational Reals in the Reals

text 
  This density proof is due to Stefan Richter and was ported by TN.  The
  original source is Real Analysis by H.L. Royden.
  It employs the Archimedean property of the reals.

lemma Rats_dense_in_real:
  fixes x :: real
  assumes "x < y"
  shows "r. x < r  r < y"
proof -
  from x < y have "0 < y - x" by simp
  with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q"
    by blast
  define p where "p = y * real q - 1"
  define r where "r = of_int p / real q"
  from q have "x < y - inverse (real q)"
    by simp
  also from 0 < q have "y - inverse (real q)  r"
    by (simp add: r_def p_def le_divide_eq left_diff_distrib)
  finally have "x < r" .
  moreover from 0 < q have "r < y"
    by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric])
  moreover have "r  "
    by (simp add: r_def)
  ultimately show ?thesis by blast
qed

lemma of_rat_dense:
  fixes x y :: real
  assumes "x < y"
  shows "q :: rat. x < of_rat q  of_rat q < y"
  using Rats_dense_in_real [OF x < y]
  by (auto elim: Rats_cases)


subsection Numerals and Arithmetic

declaration 
  K (Lin_Arith.add_inj_const (const_nameof_nat, typnat  real)
  #> Lin_Arith.add_inj_const (const_nameof_int, typint  real))



subsection Simprules combining x + y› and 0› (* FIXME ARE THEY NEEDED? *)

lemma real_add_minus_iff [simp]: "x + - a = 0  x = a"
  for x a :: real
  by arith

lemma real_add_less_0_iff: "x + y < 0  y < - x"
  for x y :: real
  by auto

lemma real_0_less_add_iff: "0 < x + y  - x < y"
  for x y :: real
  by auto

lemma real_add_le_0_iff: "x + y  0  y  - x"
  for x y :: real
  by auto

lemma real_0_le_add_iff: "0  x + y  - x  y"
  for x y :: real
  by auto


subsection Lemmas about powers

lemma two_realpow_ge_one: "(1::real)  2 ^ n"
  by simp

(* FIXME: declare this [simp] for all types, or not at all *)
declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp]

lemma real_minus_mult_self_le [simp]: "- (u * u)  x * x"
  for u x :: real
  by (rule order_trans [where y = 0]) auto

lemma realpow_square_minus_le [simp]: "- u2  x2"
  for u x :: real
  by (auto simp add: power2_eq_square)


subsection Density of the Reals

lemma field_lbound_gt_zero: "0 < d1  0 < d2  e. 0 < e  e < d1  e < d2"
  for d1 d2 :: "'a::linordered_field"
  by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)

lemma field_less_half_sum: "x < y  x < (x + y) / 2"
  for x y :: "'a::linordered_field"
  by auto

lemma field_sum_of_halves: "x / 2 + x / 2 = x"
  for x :: "'a::linordered_field"
  by simp


subsection Archimedean properties and useful consequences

textBernoulli's inequality
proposition Bernoulli_inequality:
  fixes x :: real
  assumes "-1  x"
    shows "1 + n * x  (1 + x) ^ n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "1 + Suc n * x  1 + (Suc n)*x + n * x^2"
    by (simp add: algebra_simps)
  also have "... = (1 + x) * (1 + n*x)"
    by (auto simp: power2_eq_square algebra_simps)
  also have "...  (1 + x) ^ Suc n"
    using Suc.hyps assms mult_left_mono by fastforce
  finally show ?case .
qed

corollary Bernoulli_inequality_even:
  fixes x :: real
  assumes "even n"
    shows "1 + n * x  (1 + x) ^ n"
proof (cases "-1  x  n=0")
  case True
  then show ?thesis
    by (auto simp: Bernoulli_inequality)
next
  case False
  then have "real n  1"
    by simp
  with False have "n * x  -1"
    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
  then have "1 + n * x  0"
    by auto
  also have "...  (1 + x) ^ n"
    using assms
    using zero_le_even_power by blast
  finally show ?thesis .
qed

corollary real_arch_pow:
  fixes x :: real
  assumes x: "1 < x"
  shows "n. y < x^n"
proof -
  from x have x0: "x - 1 > 0"
    by arith
  from reals_Archimedean3[OF x0, rule_format, of y]
  obtain n :: nat where n: "y < real n * (x - 1)" by metis
  from x0 have x00: "x- 1  -1" by arith
  from Bernoulli_inequality[OF x00, of n] n
  have "y < x^n" by auto
  then show ?thesis by metis
qed

corollary real_arch_pow_inv:
  fixes x y :: real
  assumes y: "y > 0"
    and x1: "x < 1"
  shows "n. x^n < y"
proof (cases "x > 0")
  case True
  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
  from real_arch_pow[OF ix, of "1/y"]
  obtain n where n: "1/y < (1/x)^n" by blast
  then show ?thesis using y x > 0
    by (auto simp add: field_simps)
next
  case False
  with y x1 show ?thesis
    by (metis less_le_trans not_less power_one_right)
qed

lemma forall_pos_mono:
  "(d e::real. d < e  P d  P e) 
    (n::nat. n  0  P (inverse (real n)))  (e. 0 < e  P e)"
  by (metis real_arch_inverse)

lemma forall_pos_mono_1:
  "(d e::real. d < e  P d  P e) 
    (n. P (inverse (real (Suc n))))  0 < e  P e"
  apply (rule forall_pos_mono)
  apply auto
  apply (metis Suc_pred of_nat_Suc)
  done


subsection Floor and Ceiling Functions from the Reals to the Integers

(* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)

lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w  n < numeral w"
  for n :: nat
  by (metis of_nat_less_iff of_nat_numeral)

lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n  numeral w < n"
  for n :: nat
  by (metis of_nat_less_iff of_nat_numeral)

lemma numeral_le_real_of_nat_iff [simp]: "numeral n  real m  numeral n  m"
  for m :: nat
  by (metis not_le real_of_nat_less_numeral_iff)

lemma of_int_floor_cancel [simp]: "of_int x = x  (n::int. x = of_int n)"
  by (metis floor_of_int)

lemma floor_eq: "real_of_int n < x  x < real_of_int n + 1  x = n"
  by linarith

lemma floor_eq2: "real_of_int n  x  x < real_of_int n + 1  x = n"
  by (fact floor_unique)

lemma floor_eq3: "real n < x  x < real (Suc n)  nat x = n"
  by linarith

lemma floor_eq4: "real n  x  x < real (Suc n)  nat x = n"
  by linarith

lemma real_of_int_floor_ge_diff_one [simp]: "r - 1  real_of_int r"
  by linarith

lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int r"
  by linarith

lemma real_of_int_floor_add_one_ge [simp]: "r  real_of_int r + 1"
  by linarith

lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int r + 1"
  by linarith

lemma floor_divide_real_eq_div:
  assumes "0  b"
  shows "a / real_of_int b = a div b"
proof (cases "b = 0")
  case True
  then show ?thesis by simp
next
  case False
  with assms have b: "b > 0" by simp
  have "j = i div b"
    if "real_of_int i  a" "a < 1 + real_of_int i"
      "real_of_int j * real_of_int b  a" "a < real_of_int b + real_of_int j * real_of_int b"
    for i j :: int
  proof -
    from that have "i < b + j * b"
      by (metis le_less_trans of_int_add of_int_less_iff of_int_mult)
    moreover have "j * b < 1 + i"
    proof -
      have "real_of_int (j * b) < real_of_int i + 1"
        using a < 1 + real_of_int i real_of_int j * real_of_int b  a by force
      then show "j * b < 1 + i" by linarith
    qed
    ultimately have "(j - i div b) * b  i mod b" "i mod b < ((j - i div b) + 1) * b"
      by (auto simp: field_simps)
    then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
      using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i]
      by linarith+
    then show ?thesis using b unfolding mult_less_cancel_right by auto
  qed
  with b show ?thesis by (auto split: floor_split simp: field_simps)
qed

lemma floor_one_divide_eq_div_numeral [simp]:
  "1 / numeral b::real = 1 div numeral b"
by (metis floor_divide_of_int_eq of_int_1 of_int_numeral)

lemma floor_minus_one_divide_eq_div_numeral [simp]:
  "- (1 / numeral b)::real = - 1 div numeral b"
by (metis (mono_tags, opaque_lifting) div_minus_right minus_divide_right
    floor_divide_of_int_eq of_int_neg_numeral of_int_1)

lemma floor_divide_eq_div_numeral [simp]:
  "numeral a / numeral b::real = numeral a div numeral b"
by (metis floor_divide_of_int_eq of_int_numeral)

lemma floor_minus_divide_eq_div_numeral [simp]:
  "- (numeral a / numeral b)::real = - numeral a div numeral b"
by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)

lemma of_int_ceiling_cancel [simp]: "of_int x = x  (n::int. x = of_int n)"
  using ceiling_of_int by metis

lemma ceiling_eq: "of_int n < x  x  of_int n + 1  x = n + 1"
  by (simp add: ceiling_unique)

lemma of_int_ceiling_diff_one_le [simp]: "of_int r - 1  r"
  by linarith

lemma of_int_ceiling_le_add_one [simp]: "of_int r  r + 1"
  by linarith

lemma ceiling_le: "x  of_int a  x  a"
  by (simp add: ceiling_le_iff)

lemma ceiling_divide_eq_div: "of_int a / of_int b = - (- a div b)"
  by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus)

lemma ceiling_divide_eq_div_numeral [simp]:
  "numeral a / numeral b :: real = - (- numeral a div numeral b)"
  using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp

lemma ceiling_minus_divide_eq_div_numeral [simp]:
  "- (numeral a / numeral b :: real) = - (numeral a div numeral b)"
  using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp

text 
  The following lemmas are remnants of the erstwhile functions natfloor
  and natceiling.


lemma nat_floor_neg: "x  0  nat x = 0"
  for x :: real
  by linarith

lemma le_nat_floor: "real x  a  x  nat a"
  by linarith

lemma le_mult_nat_floor: "nat a * nat b  nat a * b"
  by (cases "0  a  0  b")
     (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)

lemma nat_ceiling_le_eq [simp]: "nat x  a  x  real a"
  by linarith

lemma real_nat_ceiling_ge: "x  real (nat x)"
  by linarith

lemma Rats_no_top_le: "q  . x  q"
  for x :: real
  by (auto intro!: bexI[of _ "of_nat (nat x)"]) linarith

lemma Rats_no_bot_less: "q  . q < x" for x :: real
  by (auto intro!: bexI[of _ "of_int (x - 1)"]) linarith


subsection Exponentiation with floor

lemma floor_power:
  assumes "x = of_int x"
  shows "x ^ n = x ^ n"
proof -
  have "x ^ n = of_int (x ^ n)"
    using assms by (induct n arbitrary: x) simp_all
  then show ?thesis by (metis floor_of_int)
qed

lemma floor_numeral_power [simp]: "numeral x ^ n = numeral x ^ n"
  by (metis floor_of_int of_int_numeral of_int_power)

lemma ceiling_numeral_power [simp]: "numeral x ^ n = numeral x ^ n"
  by (metis ceiling_of_int of_int_numeral of_int_power)


subsection Implementation of rational real numbers

text Formal constructor

definition Ratreal :: "rat  real"
  where [code_abbrev, simp]: "Ratreal = real_of_rat"

code_datatype Ratreal


text Quasi-Numerals

lemma [code_abbrev]:
  "real_of_rat (numeral k) = numeral k"
  "real_of_rat (- numeral k) = - numeral k"
  "real_of_rat (rat_of_int a) = real_of_int a"
  by simp_all

lemma [code_post]:
  "real_of_rat 0 = 0"
  "real_of_rat 1 = 1"
  "real_of_rat (- 1) = - 1"
  "real_of_rat (1 / numeral k) = 1