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

*)

header {* Development of the Reals using Cauchy Sequences *}

theory Real

imports Rat Conditionally_Complete_Lattices

begin

text {*

  This theory contains a formalization of the real numbers as

  equivalence classes of Cauchy sequences of rationals.  See

  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative

  construction using Dedekind cuts.

*}

subsection {* Preliminary lemmas *}

lemma add_diff_add:

  fixes a b c d :: "'a::ab_group_add"

  shows "(a + c) - (b + d) = (a - b) + (c - d)"

  by simp

lemma minus_diff_minus:

  fixes a b :: "'a::ab_group_add"

  shows "- a - - b = - (a - b)"

  by simp

lemma mult_diff_mult:

  fixes x y a b :: "'a::ring"

  shows "(x * y - a * b) = x * (y - b) + (x - a) * b"

  by (simp add: algebra_simps)

lemma inverse_diff_inverse:

  fixes a b :: "'a::division_ring"

  assumes "a \<noteq> 0" and "b \<noteq> 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 \<Rightarrow> rat) \<Rightarrow> bool"

where

  "vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"

lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"

  unfolding vanishes_def by simp

lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"

  unfolding vanishes_def by simp

lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"

  unfolding vanishes_def

  apply (cases "c = 0", auto)

  apply (rule exI [where x="\<bar>c\<bar>"], auto)

  done

lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"

  unfolding vanishes_def by simp

lemma vanishes_add:

  assumes X: "vanishes X" and Y: "vanishes Y"

  shows "vanishes (\<lambda>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: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"

    using vanishesD [OF X s] ..

  obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"

    using vanishesD [OF Y t] ..

  have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"

  proof (clarsimp)

    fix n assume n: "i \<le> n" "j \<le> n"

    have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)

    also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)

    finally show "\<bar>X n + Y n\<bar> < r" unfolding r .

  qed

  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..

qed

lemma vanishes_diff:

  assumes X: "vanishes X" and Y: "vanishes Y"

  shows "vanishes (\<lambda>n. X n - Y n)"

  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y)

lemma vanishes_mult_bounded:

  assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"

  assumes Y: "vanishes (\<lambda>n. Y n)"

  shows "vanishes (\<lambda>n. X n * Y n)"

proof (rule vanishesI)

  fix r :: rat assume r: "0 < r"

  obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"

    using X by fast

  obtain b where b: "0 < b" "r = a * b"

  proof

    show "0 < r / a" using r a by (simp add: divide_pos_pos)

    show "r = a * (r / a)" using a by simp

  qed

  obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"

    using vanishesD [OF Y b(1)] ..

  have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"

    by (simp add: b(2) abs_mult mult_strict_mono' a k)

  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..

qed

subsection {* Cauchy sequences *}

definition

  cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"

where

  "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"

lemma cauchyI:

  "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X"

  unfolding cauchy_def by simp

lemma cauchyD:

  "\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"

  unfolding cauchy_def by simp

lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"

  unfolding cauchy_def by simp

lemma cauchy_add [simp]:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "cauchy (\<lambda>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: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"

    using cauchyD [OF X s] ..

  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"

    using cauchyD [OF Y t] ..

  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"

  proof (clarsimp)

    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"

    have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"

      unfolding add_diff_add by (rule abs_triangle_ineq)

    also have "\<dots> < s + t"

      by (rule add_strict_mono, simp_all add: i j *)

    finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .

  qed

  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..

qed

lemma cauchy_minus [simp]:

  assumes X: "cauchy X"

  shows "cauchy (\<lambda>n. - X n)"

using assms unfolding cauchy_def

unfolding minus_diff_minus abs_minus_cancel .

lemma cauchy_diff [simp]:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "cauchy (\<lambda>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 "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"

proof -

  obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"

    using cauchyD [OF assms zero_less_one] ..

  show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"

  proof (intro exI conjI allI)

    have "0 \<le> \<bar>X 0\<bar>" by simp

    also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp

    finally have "0 \<le> Max (abs ` X ` {..k})" .

    thus "0 < Max (abs ` X ` {..k}) + 1" by simp

  next

    fix n :: nat

    show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"

    proof (rule linorder_le_cases)

      assume "n \<le> k"

      hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp

      thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp

    next

      assume "k \<le> n"

      have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp

      also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"

        by (rule abs_triangle_ineq)

      also have "\<dots> < Max (abs ` X ` {..k}) + 1"

        by (rule add_le_less_mono, simp, simp add: k `k \<le> n`)

      finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .

    qed

  qed

qed

lemma cauchy_mult [simp]:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "cauchy (\<lambda>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" "\<forall>n. \<bar>X n\<bar> < a"

    using cauchy_imp_bounded [OF X] by fast

  obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"

    using cauchy_imp_bounded [OF Y] by fast

  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 (rule divide_pos_pos)

    show "0 < u/a" using u a(1) by (rule divide_pos_pos)

    show "r = a * (u/a) + (v/b) * b"

      using a(1) b(1) `r = u + v` by simp

  qed

  obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"

    using cauchyD [OF X s] ..

  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"

    using cauchyD [OF Y t] ..

  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"

  proof (clarsimp)

    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"

    have "\<bar>X m * Y m - X n * Y n\<bar> = \<bar>X m * (Y m - Y n) + (X m - X n) * Y n\<bar>"

      unfolding mult_diff_mult ..

    also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"

      by (rule abs_triangle_ineq)

    also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>"

      unfolding abs_mult ..

    also have "\<dots> < a * t + s * b"

      by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)

    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .

  qed

  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..

qed

lemma cauchy_not_vanishes_cases:

  assumes X: "cauchy X"

  assumes nz: "\<not> vanishes X"

  shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)"

proof -

  obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>"

    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: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"

    using cauchyD [OF X s] ..

  obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"

    using r by fast

  have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"

    using i `i \<le> k` by auto

  have "X k \<le> - r \<or> r \<le> X k"

    using `r \<le> \<bar>X k\<bar>` by auto

  hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"

    unfolding `r = s + t` using k by auto

  hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..

  thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"

    using t by auto

qed

lemma cauchy_not_vanishes:

  assumes X: "cauchy X"

  assumes nz: "\<not> vanishes X"

  shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"

using cauchy_not_vanishes_cases [OF assms]

by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)

lemma cauchy_inverse [simp]:

  assumes X: "cauchy X"

  assumes nz: "\<not> vanishes X"

  shows "cauchy (\<lambda>n. inverse (X n))"

proof (rule cauchyI)

  fix r :: rat assume "0 < r"

  obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"

    using cauchy_not_vanishes [OF X nz] by fast

  from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 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 mult_pos_pos)

    show "r = inverse b * (b * r * b) * inverse b"

      using b by simp

  qed

  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"

    using cauchyD [OF X s] ..

  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"

  proof (clarsimp)

    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"

    have "\<bar>inverse (X m) - inverse (X n)\<bar> =

          inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"

      by (simp add: inverse_diff_inverse nz * abs_mult)

    also have "\<dots> < inverse b * s * inverse b"

      by (simp add: mult_strict_mono less_imp_inverse_less

                    mult_pos_pos i j b * s)

    finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .

  qed

  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..

qed

lemma vanishes_diff_inverse:

  assumes X: "cauchy X" "\<not> vanishes X"

  assumes Y: "cauchy Y" "\<not> vanishes Y"

  assumes XY: "vanishes (\<lambda>n. X n - Y n)"

  shows "vanishes (\<lambda>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: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"

    using cauchy_not_vanishes [OF X] by fast

  obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"

    using cauchy_not_vanishes [OF Y] by fast

  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 add: mult_pos_pos)

    show "inverse a * (a * r * b) * inverse b = r"

      using a r b by simp

  qed

  obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"

    using vanishesD [OF XY s] ..

  have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"

  proof (clarsimp)

    fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"

    have "X n \<noteq> 0" and "Y n \<noteq> 0"

      using i j a b n by auto

    hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =

        inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"

      by (simp add: inverse_diff_inverse abs_mult)

    also have "\<dots> < inverse a * s * inverse b"

      apply (intro mult_strict_mono' less_imp_inverse_less)

      apply (simp_all add: a b i j k n mult_nonneg_nonneg)

      done

    also note `inverse a * s * inverse b = r`

    finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .

  qed

  thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..

qed

subsection {* Equivalence relation on Cauchy sequences *}

definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool"

  where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))"

lemma realrelI [intro?]:

  assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n - Y n)"

  shows "realrel X Y"

  using assms unfolding realrel_def by simp

lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X"

  unfolding realrel_def by simp

lemma symp_realrel: "symp realrel"

  unfolding realrel_def

  by (rule sympI, clarify, drule vanishes_minus, simp)

lemma transp_realrel: "transp realrel"

  unfolding realrel_def

  apply (rule transpI, clarify)

  apply (drule (1) vanishes_add)

  apply (simp add: algebra_simps)

  done

lemma part_equivp_realrel: "part_equivp realrel"

  by (fast intro: part_equivpI symp_realrel transp_realrel

    realrel_refl cauchy_const)

subsection {* The field of real numbers *}

quotient_type real = "nat \<Rightarrow> rat" / partial: realrel

  morphisms rep_real Real

  by (rule part_equivp_realrel)

lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> 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 "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"

proof (induct x)

  case (1 X)

  hence "cauchy X" by (simp add: realrel_def)

  thus "P (Real X)" by (rule assms)

qed

lemma eq_Real:

  "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"

  using real.rel_eq_transfer

  unfolding real.pcr_cr_eq cr_real_def fun_rel_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_inverse_zero

begin

lift_definition zero_real :: "real" is "\<lambda>n. 0"

  by (simp add: realrel_refl)

lift_definition one_real :: "real" is "\<lambda>n. 1"

  by (simp add: realrel_refl)

lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>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 \<Rightarrow> real" is "\<lambda>X n. - X n"

  unfolding realrel_def minus_diff_minus

  by (simp only: cauchy_minus vanishes_minus simp_thms)

lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"

  unfolding realrel_def mult_diff_mult

  by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add

    vanishes_mult_bounded cauchy_imp_bounded simp_thms)

lift_definition inverse_real :: "real \<Rightarrow> real"

  is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"

proof -

  fix X Y assume "realrel X Y"

  hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"

    unfolding realrel_def by simp_all

  have "vanishes X \<longleftrightarrow> 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

  thus "?thesis X Y"

    unfolding realrel_def

    by (simp add: vanishes_diff_inverse X Y XY)

qed

definition

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

definition

  "x / y = (x::real) * inverse y"

lemma add_Real:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"

  using assms plus_real.transfer

  unfolding cr_real_eq fun_rel_def by simp

lemma minus_Real:

  assumes X: "cauchy X"

  shows "- Real X = Real (\<lambda>n. - X n)"

  using assms uminus_real.transfer

  unfolding cr_real_eq fun_rel_def by simp

lemma diff_Real:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"

  unfolding minus_real_def

  by (simp add: minus_Real add_Real X Y)

lemma mult_Real:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"

  using assms times_real.transfer

  unfolding cr_real_eq fun_rel_def by simp

lemma inverse_Real:

  assumes X: "cauchy X"

  shows "inverse (Real X) =

    (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"

  using assms inverse_real.transfer zero_real.transfer

  unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)

instance proof

  fix a b c :: real

  show "a + b = b + a"

    by transfer (simp add: add_ac realrel_def)

  show "(a + b) + c = a + (b + c)"

    by transfer (simp add: add_ac 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: mult_ac realrel_def)

  show "a * b = b * a"

    by transfer (simp add: mult_ac realrel_def)

  show "1 * a = a"

    by transfer (simp add: mult_ac realrel_def)

  show "(a + b) * c = a * c + b * c"

    by transfer (simp add: distrib_right realrel_def)

  show "(0\<Colon>real) \<noteq> (1\<Colon>real)"

    by transfer (simp add: realrel_def)

  show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

    apply transfer

    apply (simp add: realrel_def)

    apply (rule vanishesI)

    apply (frule (1) cauchy_not_vanishes, clarify)

    apply (rule_tac x=k in exI, clarify)

    apply (drule_tac x=n in spec, simp)

    done

  show "a / 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 \<Rightarrow> bool"

  is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"

proof -

  { fix X Y

    assume "realrel X Y"

    hence XY: "vanishes (\<lambda>n. X n - Y n)"

      unfolding realrel_def by simp_all

    assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"

    then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"

      by fast

    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: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"

      using vanishesD [OF XY s] ..

    have "\<forall>n\<ge>max i j. t < Y n"

    proof (clarsimp)

      fix n assume n: "i \<le> n" "j \<le> n"

      have "\<bar>X n - Y n\<bar> < s" and "r < X n"

        using i j n by simp_all

      thus "t < Y n" unfolding r by simp

    qed

    hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast

  } note 1 = this

  fix X Y assume "realrel X Y"

  hence "realrel X Y" and "realrel Y X"

    using symp_realrel unfolding symp_def by auto

  thus "?thesis X Y"

    by (safe elim!: 1)

qed

lemma positive_Real:

  assumes X: "cauchy X"

  shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"

  using assms positive.transfer

  unfolding cr_real_eq fun_rel_def by simp

lemma positive_zero: "\<not> positive 0"

  by transfer auto

lemma positive_add:

  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"

apply transfer

apply (clarify, rename_tac a b i j)

apply (rule_tac x="a + b" in exI, simp)

apply (rule_tac x="max i j" in exI, clarsimp)

apply (simp add: add_strict_mono)

done

lemma positive_mult:

  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"

apply transfer

apply (clarify, rename_tac a b i j)

apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)

apply (rule_tac x="max i j" in exI, clarsimp)

apply (rule mult_strict_mono, auto)

done

lemma positive_minus:

  "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"

apply transfer

apply (simp add: realrel_def)

apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)

done

instantiation real :: linordered_field_inverse_zero

begin

definition

  "x < y \<longleftrightarrow> positive (y - x)"

definition

  "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"

definition

  "abs (a::real) = (if a < 0 then - a else a)"

definition

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

instance proof

  fix a b c :: real

  show "\<bar>a\<bar> = (if a < 0 then - a else a)"

    by (rule abs_real_def)

  show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"

    unfolding less_eq_real_def less_real_def

    by (auto, drule (1) positive_add, simp_all add: positive_zero)

  show "a \<le> a"

    unfolding less_eq_real_def by simp

  show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"

    unfolding less_eq_real_def less_real_def

    by (auto, drule (1) positive_add, simp add: algebra_simps)

  show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"

    unfolding less_eq_real_def less_real_def

    by (auto, drule (1) positive_add, simp add: positive_zero)

  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"

    unfolding less_eq_real_def less_real_def by auto

    (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)

    (* Should produce c + b - (c + a) \<equiv> b - a *)

  show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"

    by (rule sgn_real_def)

  show "a \<le> b \<or> b \<le> a"

    unfolding less_eq_real_def less_real_def

    by (auto dest!: positive_minus)

  show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

    unfolding less_real_def

    by (drule (1) positive_mult, simp add: algebra_simps)

qed

end

instantiation real :: distrib_lattice

begin

definition

  "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"

definition

  "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"

instance proof

qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)

end

lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"

apply (induct x)

apply (simp add: zero_real_def)

apply (simp add: one_real_def add_Real)

done

lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"

apply (cases x rule: int_diff_cases)

apply (simp add: of_nat_Real diff_Real)

done

lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"

apply (induct x)

apply (simp add: Fract_of_int_quotient of_rat_divide)

apply (simp add: of_int_Real divide_inverse)

apply (simp add: inverse_Real mult_Real)

done

instance real :: archimedean_field

proof

  fix x :: real

  show "\<exists>z. x \<le> of_int z"

    apply (induct x)

    apply (frule cauchy_imp_bounded, clarify)

    apply (rule_tac x="ceiling b + 1" in exI)

    apply (rule less_imp_le)

    apply (simp add: of_int_Real less_real_def diff_Real positive_Real)

    apply (rule_tac x=1 in exI, simp add: algebra_simps)

    apply (rule_tac x=0 in exI, clarsimp)

    apply (rule le_less_trans [OF abs_ge_self])

    apply (rule less_le_trans [OF _ le_of_int_ceiling])

    apply simp

    done

qed

instantiation real :: floor_ceiling

begin

definition [code del]:

  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"

instance proof

  fix x :: real

  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"

    unfolding floor_real_def using floor_exists1 by (rule theI')

qed

end

subsection {* Completeness *}

lemma not_positive_Real:

  assumes X: "cauchy X"

  shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"

unfolding positive_Real [OF X]

apply (auto, unfold not_less)

apply (erule obtain_pos_sum)

apply (drule_tac x=s in spec, simp)

apply (drule_tac r=t in cauchyD [OF X], clarify)

apply (drule_tac x=k in spec, clarsimp)

apply (rule_tac x=n in exI, clarify, rename_tac m)

apply (drule_tac x=m in spec, simp)

apply (drule_tac x=n in spec, simp)

apply (drule spec, drule (1) mp, clarify, rename_tac i)

apply (rule_tac x="max i k" in exI, simp)

done

lemma le_Real:

  assumes X: "cauchy X" and Y: "cauchy Y"

  shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"

unfolding not_less [symmetric, where 'a=real] less_real_def

apply (simp add: diff_Real not_positive_Real X Y)

apply (simp add: diff_le_eq add_ac)

done

lemma le_RealI:

  assumes Y: "cauchy Y"

  shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"

proof (induct x)

  fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"

  hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"

    by (simp add: of_rat_Real le_Real)

  {

    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: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"

      using cauchyD [OF Y s] ..

    obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"

      using le [OF t] ..

    have "\<forall>n\<ge>max i j. X n \<le> Y n + r"

    proof (clarsimp)

      fix n assume n: "i \<le> n" "j \<le> n"

      have "X n \<le> Y i + t" using n j by simp

      moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp

      ultimately show "X n \<le> Y n + r" unfolding r by simp

    qed

    hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..

  }

  thus "Real X \<le> Real Y"

    by (simp add: of_rat_Real le_Real X Y)

qed

lemma Real_leI:

  assumes X: "cauchy X"

  assumes le: "\<forall>n. of_rat (X n) \<le> y"

  shows "Real X \<le> y"

proof -

  have "- y \<le> - Real X"

    by (simp add: minus_Real X le_RealI of_rat_minus le)

  thus ?thesis by simp

qed

lemma less_RealD:

  assumes Y: "cauchy Y"

  shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"

by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])

lemma of_nat_less_two_power:

  "of_nat n < (2::'a::linordered_idom) ^ n"

apply (induct n)

apply simp

apply (subgoal_tac "(1::'a) \<le> 2 ^ n")

apply (drule (1) add_le_less_mono, simp)

apply simp

done

lemma complete_real:

  fixes S :: "real set"

  assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z"

  shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"

proof -

  obtain x where x: "x \<in> S" using assms(1) ..

  obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..

  def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"

  obtain a where a: "\<not> P a"

  proof

    have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)

    also have "x - 1 < x" by simp

    finally have "of_int (floor (x - 1)) < x" .

    hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)

    then show "\<not> P (of_int (floor (x - 1)))"

      unfolding P_def of_rat_of_int_eq using x by fast

  qed

  obtain b where b: "P b"

  proof

    show "P (of_int (ceiling z))"

    unfolding P_def of_rat_of_int_eq

    proof

      fix y assume "y \<in> S"

      hence "y \<le> z" using z by simp

      also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)

      finally show "y \<le> of_int (ceiling z)" .

    qed

  qed

  def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"

  def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"

  def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"

  def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"

  def C \<equiv> "\<lambda>n. avg (A n) (B 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]: "\<And>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]: "\<And>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: "\<And>n. B n - A n = (b - a) / 2^n"

    apply (simp add: eq_divide_eq)

    apply (induct_tac n, simp)

    apply (simp add: C_def avg_def algebra_simps)

    done

  have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"

    apply (simp add: divide_less_eq)

    apply (subst mult_commute)

    apply (frule_tac y=y in ex_less_of_nat_mult)

    apply clarify

    apply (rule_tac x=n in exI)

    apply (erule less_trans)

    apply (rule mult_strict_right_mono)

    apply (rule le_less_trans [OF _ of_nat_less_two_power])

    apply simp

    apply assumption

    done

  have PA: "\<And>n. \<not> P (A n)"

    by (induct_tac n, simp_all add: a)

  have PB: "\<And>n. P (B n)"

    by (induct_tac n, simp_all add: b)

  have ab: "a < b"

    using a b unfolding P_def

    apply (clarsimp simp add: not_le)

    apply (drule (1) bspec)

    apply (drule (1) less_le_trans)

    apply (simp add: of_rat_less)

    done

  have AB: "\<And>n. A n < B n"

    by (induct_tac n, simp add: ab, simp add: C_def avg_def)

  have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"

    apply (auto simp add: le_less [where 'a=nat])

    apply (erule less_Suc_induct)

    apply (clarsimp simp add: C_def avg_def)

    apply (simp add: add_divide_distrib [symmetric])

    apply (rule AB [THEN less_imp_le])

    apply simp

    done

  have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"

    apply (auto simp add: le_less [where 'a=nat])

    apply (erule less_Suc_induct)

    apply (clarsimp simp add: C_def avg_def)

    apply (simp add: add_divide_distrib [symmetric])

    apply (rule AB [THEN less_imp_le])

    apply simp

    done

  have cauchy_lemma:

    "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"

    apply (rule cauchyI)

    apply (drule twos [where y="b - a"])

    apply (erule exE)

    apply (rule_tac x=n in exI, clarify, rename_tac i j)

    apply (rule_tac y="B n - A n" in le_less_trans) defer

    apply (simp add: width)

    apply (drule_tac x=n in spec)

    apply (frule_tac x=i in spec, drule (1) mp)

    apply (frule_tac x=j in spec, drule (1) mp)

    apply (frule A_mono, drule B_mono)

    apply (frule A_mono, drule B_mono)

    apply arith

    done

  have "cauchy A"

    apply (rule cauchy_lemma [rule_format])

    apply (simp add: A_mono)

    apply (erule order_trans [OF less_imp_le [OF AB] B_mono])

    done

  have "cauchy B"

    apply (rule cauchy_lemma [rule_format])

    apply (simp add: B_mono)

    apply (erule order_trans [OF A_mono less_imp_le [OF AB]])

    done

  have 1: "\<forall>x\<in>S. x \<le> Real B"

  proof

    fix x assume "x \<in> S"

    then show "x \<le> Real B"

      using PB [unfolded P_def] `cauchy B`

      by (simp add: le_RealI)

  qed

  have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"

    apply clarify

    apply (erule contrapos_pp)

    apply (simp add: not_le)

    apply (drule less_RealD [OF `cauchy A`], clarify)

    apply (subgoal_tac "\<not> P (A n)")

    apply (simp add: P_def not_le, clarify)

    apply (erule rev_bexI)

    apply (erule (1) less_trans)

    apply (simp add: PA)

    done

  have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"

  proof (rule vanishesI)

    fix r :: rat assume "0 < r"

    then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"

      using twos by fast

    have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"

    proof (clarify)

      fix n assume n: "k \<le> n"

      have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"

        by simp

      also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"

        using n by (simp add: divide_left_mono mult_pos_pos)

      also note k

      finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .

    qed

    thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..

  qed

  hence 3: "Real B = Real A"

    by (simp add: eq_Real `cauchy A` `cauchy B` width)

  show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"

    using 1 2 3 by (rule_tac x="Real B" in exI, simp)

qed

instantiation real :: linear_continuum

begin

subsection{*Supremum of a set of reals*}

definition

  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"

definition

  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"

instance

proof

  { fix x :: real and X :: "real set"

    assume x: "x \<in> X" "bdd_above X"

    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"

      using complete_real[of X] unfolding bdd_above_def by blast

    then show "x \<le> Sup X"

      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }

  note Sup_upper = this

  { fix z :: real and X :: "real set"

    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"

    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> 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 "... \<le> z"

      by blast

    finally show "Sup X \<le> z" . }

  note Sup_least = this

  { fix x z :: real and X :: "real set"

    assume x: "x \<in> X" and [simp]: "bdd_below X"

    have "-x \<le> Sup (uminus ` X)"

      by (rule Sup_upper) (auto simp add: image_iff x)

    then show "Inf X \<le> x" 

      by (auto simp add: Inf_real_def) }

  { fix z :: real and X :: "real set"

    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"

    have "Sup (uminus ` X) \<le> -z"

      using x z by (force intro: Sup_least)

    then show "z \<le> Inf X" 

        by (auto simp add: Inf_real_def) }

  show "\<exists>a b::real. a \<noteq> 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{*More Lemmas*}

text {* BH: These lemmas should not be necessary; they should be

covered by existing simp rules and simplification procedures. *}

lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"

by simp (* redundant with mult_cancel_left *)

lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"