Quelle Real.thy Sprache: Isabelle

(*  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 \<open>Development of the Reals using Cauchy Sequences\<close>

theory Real
imports Rat
begin

text \<open>
  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.
\<close>

subsection \<open>Preliminary lemmas\<close>

text\<open>Useful in convergence arguments\<close>
lemma inverse_of_nat_le:
  fixes n::nat shows "\n \ m; n\0\ \ 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 \<open>Sequences that converge to zero\<close>

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

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

lemma vanishesD: "vanishes X \ 0 < r \ \k. \n\k. \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: "\n\i. \X n\ < s"
    using vanishesD [OF X s] ..
  obtain j where j: "\n\j. \Y n\ < t"
    using vanishesD [OF Y t] ..
  have "\n\max 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. \n\k. \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: "\n\k. \Y n\ < b"
    using vanishesD [OF Y b(1)] ..
  have "\n\k. \X n * Y n\ < r"
    by (simp add: b(2) abs_mult mult_strict_mono' a k)
  then show "\k. \n\k. \X n * Y n\ < r" ..
qed

subsection \<open>Cauchy sequences\<close>

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

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

lemma cauchyD: "cauchy X \ 0 < r \ \k. \m\k. \n\k. \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: "\m\i. \n\i. \X m - X n\ < s"
    using cauchyD [OF X s] ..
  obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t"
    using cauchyD [OF Y t] ..
  have "\m\max i j. \n\max 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. \m\k. \n\k. \(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: "\m\k. \n\k. \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 \<open>k \<le> n\<close>)
      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) \<open>r = u + v\<close> by simp
  qed
  obtain i where i: "\m\i. \n\i. \X m - X n\ < s"
    using cauchyD [OF X s] ..
  obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t"
    using cauchyD [OF Y t] ..
  have "\m\max i j. \n\max 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. \m\k. \n\k. \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. (\n\k. b < - X n) \ (\n\k. b < X n)"
proof -
  obtain r where "0 < r" and r: "\k. \n\k. 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 \<open>0 < r\<close> by (rule obtain_pos_sum)
  obtain i where i: "\m\i. \n\i. \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: "\n\k. \X n - X k\ < s"
    using i \<open>i \<le> k\<close> by auto
  have "X k \ - r \ r \ X k"
    using \<open>r \<le> \<bar>X k\<bar>\<close> by auto
  then have "(\n\k. t < - X n) \ (\n\k. t < X n)"
    unfolding \<open>r = s + t\<close> using k by auto
  then have "\k. (\n\k. t < - X n) \ (\n\k. t < X n)" ..
  then show "\t>0. \k. (\n\k. t < - X n) \ (\n\k. t < X n)"
    using t by auto
qed

lemma cauchy_not_vanishes:
  assumes X: "cauchy X"
    and nz: "\ vanishes X"
  shows "\b>0. \k. \n\k. 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: "\n\i. b < \X n\"
    using cauchy_not_vanishes [OF X nz] by blast
  from b i have nz: "\n\i. 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: \<open>0 < r\<close> b)
    show "r = inverse b * (b * r * b) * inverse b"
      using b by simp
  qed
  obtain j where j: "\m\j. \n\j. \X m - X n\ < s"
    using cauchyD [OF X s] ..
  have "\m\max i j. \n\max 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. \m\k. \n\k. \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: "\n\i. a < \X n\"
    using cauchy_not_vanishes [OF X] by blast
  obtain b j where b: "0 < b" and j: "\n\j. 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: "\n\k. \X n - Y n\ < s"
    using vanishesD [OF XY s] ..
  have "\n\max (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 \<open>inverse a * s * inverse b = r\<close>
    finally show "\inverse (X n) - inverse (Y n)\ < r" .
  qed
  then show "\k. \n\k. \inverse (X n) - inverse (Y n)\ < r" ..
qed

subsection \<open>Equivalence relation on Cauchy sequences\<close>

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 \<open>The field of real numbers\<close>

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)\
       \<Longrightarrow> vanishes (\<lambda>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" "\n\k. b < \X n\"
      using X cauchy_not_vanishes by blast
    then show "\k. \n\k. \inverse (X n) * X n - 1\ < r"
      using \<open>0 < r\<close> 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 \<open>Positive reals\<close>

lift_definition positive :: "real \ bool"
  is "\X. \r>0. \k. \n\k. r < X n"
proof -
  have 1: "\r>0. \k. \n\k. r < Y n"
    if *: "realrel X Y" and **: "\r>0. \k. \n\k. 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: "\n\i. r < X n"
      by blast
    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
      using \<open>0 < r\<close> by (rule obtain_pos_sum)
    obtain j where j: "\n\j. \X n - Y n\ < s"
      using vanishesD [OF XY s] ..
    have "\n\max 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. \n\k. 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 *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\
       \<Longrightarrow> 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 *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\
       \<Longrightarrow> 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 \<open>Completeness\<close>

lemma not_positive_Real:
  assumes "cauchy X" shows "\ positive (Real X) \ (\r>0. \k. \n\k. X n \ r)" (is "?lhs = ?rhs")
  unfolding positive_Real [OF assms]
proof (intro iffI allI notI impI)
  show "\k. \n\k. X n \ r" if r: "\ (\r>0. \k. \n\k. r < X n)" and "0 < r" for r
  proof -
    obtain s t where "s > 0" "t > 0" "r = s+t"
      using \<open>r > 0\<close> obtain_pos_sum by blast
    obtain k where k: "\m n. \m\k; n\k\ \ \X m - X n\ < t"
      using cauchyD [OF assms \<open>t > 0\<close>] by blast
    obtain n where "n \ k" "X n \ s"
      by (meson r \<open>0 < s\<close> not_less)
    then have "X l \ r" if "l \ n" for l
      using k [OF \<open>n \<ge> k\<close>, of l] that \<open>r = s+t\<close> 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. \n\k. 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. \n\k. X n \ Y m + r"
    by (simp add: of_rat_Real le_Real)
  then have "\k. \n\k. 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: "\m\i. \n\i. \Y m - Y n\ < s"
      using cauchyD [OF Y s] ..
    obtain j where j: "\n\j. X n \ Y i + t"
      using le [OF t] ..
    have "\n\max 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)"
  by (meson Real_leI assms leD leI)

lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n"
  by auto

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

  define P where "P x \ (\y\S. 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 \<open>0 < r\<close> 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. i\n \ 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 "m\k" "n\k" 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. \m\k. \n\k. \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 "\x\S. x \ Real B"
  proof
    fix x
    assume "x \ S"
    then show "x \ Real B"
      using PB [unfolded P_def] \<open>cauchy B\<close>
      by (simp add: le_RealI)
  qed
  moreover have "\z. (\x\S. x \ z) \ Real A \ z"
    by (meson PA Real_leI P_def \<open>cauchy A\<close> 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 "\n\k. \(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. \n\k. \(b - a) / 2 ^ n\ < r" ..
  qed
  then have "Real B = Real A"
    by (simp add: eq_Real \<open>cauchy A\<close> \<open>cauchy B\<close> width)
  ultimately show "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)"
    by force
qed

instantiation real :: linear_continuum
begin

subsection \<open>Supremum of a set of reals\<close>

definition "Sup X = (LEAST z::real. \x\X. 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: "\y\X. y \ s" "\z. \y\X. 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: "\y\X. y \ s" "\z. \y\X. 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 \<open>Hiding implementation details\<close>

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 \<open>Embedding numbers into the Reals\<close>

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 (in field_char_0) of_int_div_aux:
  "(of_int x) / (of_int d) =
    of_int (x div d) + (of_int (x mod d)) / (of_int d)"
proof -
  have "x = (x div d) * d + x mod d"
    by auto
  then have "of_int x = of_int (x div d) * of_int d + of_int(x mod d)"
    by (metis local.of_int_add local.of_int_mult)
  then show ?thesis
    by (simp add: divide_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 auto

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 \<open>Embedding the Naturals into the Reals\<close>

lemma (in field_char_0) of_nat_of_nat_div_aux:
  "of_nat x / of_nat d = of_nat (x div d) + of_nat (x mod d) / of_nat d"
  by (metis add_divide_distrib diff_add_cancel of_nat_div)

lemma(in field_char_0) of_nat_of_nat_div: "d dvd n \ of_nat(n div d) = of_nat n / of_nat d"
  by auto

lemma (in linordered_field) of_nat_div_le_of_nat: "of_nat (n div x) \ of_nat n / of_nat x"
  by (metis le_add_same_cancel1 of_nat_0_le_iff of_nat_of_nat_div_aux zero_le_divide_iff)

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 less_iff_succ_less_eq of_nat_1 of_nat_add of_nat_le_iff)

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

lemma real_of_nat_div: "d dvd n \ real(n div d) = real n / real d"
  by auto

lemma real_binomial_eq_mult_binomial_Suc:
  assumes "k \ n"
  shows "real(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)"
  using assms
  by (simp add: of_nat_binomial_eq_mult_binomial_Suc [of k n] add.commute)

subsection \<open>The Archimedean Property of the Reals\<close>

text \<open>Not actually the reals any more!\<close>
lemma real_arch_inverse:
  fixes e::"'a::archimedean_field"
  shows "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (of_nat n) < e)"
  using reals_Archimedean[of e] less_trans[of 0 "1 / of_nat n" e for n::nat]
  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)

lemma reals_Archimedean3:
  fixes x::"'a::archimedean_field"
  shows "0 < x \ \y. \n. y < of_nat n * x"
  by (auto intro: ex_less_of_nat_mult)

lemma real_archimedian_rdiv_eq_0:
  fixes x::"'a::archimedean_field"
  assumes "x \ 0" and "\m::nat. m > 0 \ of_nat m * x \ c"
  shows "x = 0"
  by (metis (no_types, opaque_lifting) reals_Archimedean3 order.order_iff_strict le0 le_less_trans not_le assms)

lemma inverse_Suc: "inverse (of_nat (Suc n)) > (0::'a::archimedean_field)"
  using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast

lemma Archimedean_eventually_inverse:
  fixes \<epsilon>::"'a::archimedean_field" shows "(\<forall>\<^sub>F n in sequentially. inverse (of_nat (Suc n)) < \<epsilon>) \<longleftrightarrow> 0 < \<epsilon>"
  (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding eventually_at_top_dense
    by (metis (no_types, lifting) gt_ex inverse_Suc nat.distinct(1) real_arch_inverse)
next
  assume ?rhs
  then obtain N where "inverse (of_nat (Suc N)) < \"
    using reals_Archimedean by blast
  then have "inverse (of_nat (Suc n)) < \" if "n \ N" for n
    using that Suc_le_mono inverse_Suc inverse_less_imp_less
    by (meson inverse_positive_iff_positive linorder_not_less of_nat_less_iff order_le_less_trans)
  then show ?lhs
    unfolding eventually_sequentially by blast
qed

(*HOL Light's FORALL_POS_MONO_1_EQ*)
text \<open>On the relationship between two different ways of converting to 0\<close>
lemma Inter_eq_Inter_inverse_Suc:
  assumes "\r' r. r' < r \ A r' \ A r"
  shows "\ (A ` {0<..}) = (\n. A(inverse(Suc n)))"
proof
  have "x \ A \"
    if x: "\n. x \ A (inverse (Suc n))" and "\>0" for x and \ :: real
  proof -
    obtain n where "inverse (Suc n) < \"
      using \<open>\<epsilon>>0\<close> reals_Archimedean by blast
    with assms x show ?thesis
      by blast
  qed
  then show "(\n. A(inverse(Suc n))) \ (\\\{0<..}. A \)"
    by auto
qed (use inverse_Suc in fastforce)

subsection \<open>Rationals\<close>

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 \<open>x = of_rat r\<close> 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 \<open>j \<noteq> 0\<close>
    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 \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 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 \<open>n \<noteq> 0\<close> have gcd: "?gcd \<noteq> 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 \<open>n \<noteq> 0\<close> and gcd_l have "?gcd * ?l \<noteq> 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 \<open>Density of the Rational Reals in the Reals\<close>

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

lemma Rats_dense_in_real:
  fixes x :: real
  assumes "x < y"
  shows "\r\\. x < r \ r < y"
proof -
  from \<open>x < y\<close> 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 \<open>0 < q\<close> have "y - inverse (real q) \<le> r"
    by (simp add: r_def p_def le_divide_eq left_diff_distrib)
  finally have "x < r" .
  moreover from \<open>0 < q\<close> 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 \<open>x < y\<close>]
  by (auto elim: Rats_cases)

subsection \<open>Numerals and Arithmetic\<close>

declaration \<open>
  K (Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
\<close>

subsection \<open>Simprules combining \<open>x + y\<close> and \<open>0\<close>\<close> (* 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

lemma mult_ge1_I: "\x\1; y\1\ \ x*y \ (1::real)"
  using mult_mono by fastforce

subsection \<open>Lemmas about powers\<close>

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

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]: "- u\<^sup>2 \ x\<^sup>2"
  for u x :: real
  by (auto simp add: power2_eq_square)

subsection \<open>Density of the Reals\<close>

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 \<open>Archimedean properties and useful consequences\<close>

text\<open>Bernoulli's inequality\<close>
proposition Bernoulli_inequality:
  fixes x :: "'a :: linordered_field"
  assumes "-1 \ x"
    shows "1 + of_nat n * x \ (1 + x) ^ n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "1 + of_nat (Suc n) * x \ 1 + of_nat(Suc n) * x + of_nat n * x^2"
    by simp
  also have "... = (1 + x) * (1 + of_nat 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 :: "'a :: linordered_field"
  assumes "even n"
    shows "1 + of_nat 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 "of_nat n \ (1::'a)"
    by simp
  with False have "of_nat 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 + of_nat n * x \ 0"
    by auto
  also have "... \ (1 + x) ^ n"
    using assms 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 \<open>x > 0\<close>
    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) \
    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
  by (metis real_arch_inverse)

lemma forall_pos_mono_1:
  "(\d e::real. d < e \ P d \ P e) \
    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
  using reals_Archimedean by blast

lemma Archimedean_eventually_pow:
  fixes x::real
  assumes "1 < x"
  shows "\\<^sub>F n in sequentially. b < x ^ n"
proof -
  obtain N where "\n. n\N \ b < x ^ n"
    by (metis assms le_less order_less_trans power_strict_increasing_iff real_arch_pow)
  then show ?thesis
    using eventually_sequentially by blast
qed

lemma Archimedean_eventually_pow_inverse:
  fixes x::real
  assumes "\x\ < 1" "\ > 0"
  shows "\\<^sub>F n in sequentially. \x^n\ < \"
proof (cases "x = 0")
  case True
  then show ?thesis
    by (simp add: assms eventually_at_top_dense zero_power)
next
  case False
  then have "\\<^sub>F n in sequentially. inverse \ < inverse \x\ ^ n"
    by (simp add: Archimedean_eventually_pow assms(1) one_less_inverse)
  then show ?thesis
    by eventually_elim (metis \<open>\<epsilon> > 0\<close> inverse_less_imp_less power_abs power_inverse)
qed

subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>

(* 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 of_int_floor [simp]: "a \ \ \ of_int (floor a) = a"
  by (metis Ints_cases of_int_floor_cancel)

lemma floor_frac [simp]: "\frac r\ = 0"
  by (simp add: frac_def)

lemma frac_1 [simp]: "frac 1 = 0"
  by (simp add: frac_def)

lemma frac_in_Rats_iff [simp]:
  fixes r::"'a::{floor_ceiling,field_char_0}"
  shows "frac r \ \ \ r \ \"
  by (metis Rats_add Rats_diff Rats_of_int diff_add_cancel frac_def)

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 \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> 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 of_int_ceiling [simp]: "a \ \ \ of_int (ceiling a) = a"
  by (metis Ints_cases of_int_ceiling_cancel)

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 \<open>
  The following lemmas are remnants of the erstwhile functions natfloor
  and natceiling.
\<close>

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

lemma floor_ceiling_diff_le: "0 \ r \ nat\real k - r\ \ k - nat\r\"
  by linarith

lemma floor_ceiling_diff_le': "nat\r - real k\ \ nat\r\ - k"
  by linarith

lemma ceiling_floor_diff_ge: "nat\r - real k\ \ nat\r\ - k"
  by linarith

lemma ceiling_floor_diff_ge': "r \ k \ nat\r - real k\ \ k - nat\r\"
  by linarith

subsection \<open>Exponentiation with floor\<close>

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 \<open>Implementation of rational real numbers\<close>

text \<open>Formal constructor\<close>

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

code_datatype Ratreal

text \<open>Quasi-Numerals\<close>

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 / numeral k"
  "real_of_rat (numeral k / numeral l) = numeral k / numeral l"
  "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)"
  "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)"
  by (simp_all add: of_rat_divide of_rat_minus)

text \<open>Operations\<close>

lemma zero_real_code [code]: "0 = Ratreal 0"
  by simp

lemma one_real_code [code]: "1 = Ratreal 1"
  by simp

instantiation real :: equal
begin

definition "HOL.equal x y \ x - y = 0" for x :: real

instance by standard (simp add: equal_real_def)

lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \ HOL.equal x y"
  by (simp add: equal_real_def equal)

lemma [code nbe]: "HOL.equal x x \ True"
  for x :: real
  by (rule equal_refl)

end

lemma real_less_eq_code [code]: "Ratreal x \ Ratreal y \ x \ y"
  by (simp add: of_rat_less_eq)

lemma real_less_code [code]: "Ratreal x < Ratreal y \ x < y"
  by (simp add: of_rat_less)

lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"
  by (simp add: of_rat_add)

lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)"
  by (simp add: of_rat_mult)

lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)"
  by (simp add: of_rat_minus)

lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"
  by (simp add: of_rat_diff)

lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
  by (simp add: of_rat_inverse)

lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
  by (simp add: of_rat_divide)

lemma real_floor_code [code]: "\Ratreal x\ = \x\"
  by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff
      of_int_floor_le of_rat_of_int_eq real_less_eq_code)

text \<open>Quickcheck\<close>

context
  includes term_syntax
begin

definition
  valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)"
  where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k"

end

instantiation real :: random
begin

context
  includes state_combinator_syntax
begin

definition
  "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\r. Pair (valterm_ratreal r))"

instance ..

end

end

instantiation real :: exhaustive
begin

definition
  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\r. f (Ratreal r)) d"

instance ..

end

instantiation real :: full_exhaustive
begin

definition
  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\r. f (valterm_ratreal r)) d"

instance ..

end

instantiation real :: narrowing
begin

definition
  "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"

instance ..

end

subsection \<open>Setup for Nitpick\<close>

declaration \<open>
  Nitpick_HOL.register_frac_type \<^type_name>\<open>real\<close>
    [(\<^const_name>\<open>zero_real_inst.zero_real\<close>, \<^const_name>\<open>Nitpick.zero_frac\<close>),
     (\<^const_name>\<open>one_real_inst.one_real\<close>, \<^const_name>\<open>Nitpick.one_frac\<close>),
     (\<^const_name>\<open>plus_real_inst.plus_real\<close>, \<^const_name>\<open>Nitpick.plus_frac\<close>),
     (\<^const_name>\<open>times_real_inst.times_real\<close>, \<^const_name>\<open>Nitpick.times_frac\<close>),
     (\<^const_name>\<open>uminus_real_inst.uminus_real\<close>, \<^const_name>\<open>Nitpick.uminus_frac\<close>),
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.30Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.