(* 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 Conditional_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 \ 0" and "b \ 0"
shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
using assms by (simp add: algebra_simps)
lemma obtain_pos_sum:
fixes r :: rat assumes r: "0 < r"
obtains s t where "0 < s" and "0 < t" and "r = s + t"
proof
from r show "0 < r/2" by simp
from r show "0 < r/2" by simp
show "r = r/2 + r/2" by simp
qed
subsection {* Sequences that converge to zero *}
definition
vanishes :: "(nat \ rat) \ bool"
where
"vanishes X = (\r>0. \k. \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"
unfolding vanishes_def
apply (cases "c = 0", auto)
apply (rule exI [where x="\c\"], auto)
done
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" unfolding r .
qed
thus "\k. \n\k. \X n + Y n\ < r" ..
qed
lemma vanishes_diff:
assumes X: "vanishes X" and Y: "vanishes Y"
shows "vanishes (\n. X n - Y n)"
unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
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 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: "\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)
thus "\k. \n\k. \X n * Y n\ < r" ..
qed
subsection {* Cauchy sequences *}
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" unfolding r .
qed
thus "\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 X: "cauchy X" and Y: "cauchy Y"
shows "cauchy (\n. X n - Y n)"
using assms unfolding diff_minus by simp
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})" .
thus "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"
hence "\X n\ \ Max (abs ` X ` {..k})" by simp
thus "\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, simp add: k `k \ n`)
finally show "\X n\ < Max (abs ` X ` {..k}) + 1" .
qed
qed
qed
lemma cauchy_mult [simp]:
assumes X: "cauchy X" and Y: "cauchy Y"
shows "cauchy (\n. X n * Y n)"
proof (rule cauchyI)
fix r :: rat assume "0 < r"
then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
by (rule obtain_pos_sum)
obtain a where a: "0 < a" "\n. \X n\ < a"
using cauchy_imp_bounded [OF X] by fast
obtain b where b: "0 < b" "\n. \Y n\ < 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: "\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" unfolding r .
qed
thus "\