* include generalised MVT in HyperReal (contributed by Benjamin Porter)
* add non-denumerability of continuum in Real, includes closed intervals on real
(contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)
--- a/src/HOL/Hyperreal/Lim.thy Sun Feb 12 10:42:19 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy Sun Feb 12 12:29:01 2006 +0100
@@ -3,6 +3,7 @@
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+ GMVT by Benjamin Porter, 2005
*)
header{*Limits, Continuity and Differentiation*}
@@ -15,16 +16,16 @@
constdefs
LIM :: "[real=>real,real,real] => bool"
- ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
+ ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
"f -- a --> L ==
\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
- --> \<bar>f x + -L\<bar> < r"
+ --> \<bar>f x + -L\<bar> < r"
NSLIM :: "[real=>real,real,real] => bool"
- ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
+ ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
"f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
- x @= hypreal_of_real a -->
- ( *f* f) x @= hypreal_of_real L))"
+ x @= hypreal_of_real a -->
+ ( *f* f) x @= hypreal_of_real L))"
isCont :: "[real=>real,real] => bool"
"isCont f a == (f -- a --> (f a))"
@@ -32,29 +33,29 @@
isNSCont :: "[real=>real,real] => bool"
--{*NS definition dispenses with limit notions*}
"isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
- ( *f* f) y @= hypreal_of_real (f a))"
+ ( *f* f) y @= hypreal_of_real (f a))"
deriv:: "[real=>real,real,real] => bool"
--{*Differentiation: D is derivative of function f at x*}
- ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+ ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
"DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
nsderiv :: "[real=>real,real,real] => bool"
- ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+ ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
"NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
- (( *f* f)(hypreal_of_real x + h) +
- - hypreal_of_real (f x))/h @= hypreal_of_real D)"
+ (( *f* f)(hypreal_of_real x + h) +
+ - hypreal_of_real (f x))/h @= hypreal_of_real D)"
differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60)
"f differentiable x == (\<exists>D. DERIV f x :> D)"
- NSdifferentiable :: "[real=>real,real] => bool"
+ NSdifferentiable :: "[real=>real,real] => bool"
(infixl "NSdifferentiable" 60)
"f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
increment :: "[real=>real,real,hypreal] => hypreal"
"increment f x h == (@inc. f NSdifferentiable x &
- inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
+ inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
isUCont :: "(real=>real) => bool"
"isUCont f == \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
@@ -133,7 +134,7 @@
lemma LIM_diff:
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
-by (simp add: diff_minus LIM_add_minus)
+by (simp add: diff_minus LIM_add_minus)
lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
@@ -146,7 +147,7 @@
assume s: "0<s"
{ from s show "s/2 + a < a \<or> a < s/2 + a" by arith
next
- from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
+ from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
next
from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
qed
@@ -159,7 +160,7 @@
assume s: "0<s"
{ from s show "s/2 + a < a \<or> a < s/2 + a" by arith
next
- from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
+ from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
next
from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
qed
@@ -167,11 +168,11 @@
lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
apply (rule ccontr)
-apply (blast dest: LIM_const_not_eq)
+apply (blast dest: LIM_const_not_eq)
done
lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M"
-apply (drule LIM_diff, assumption)
+apply (drule LIM_diff, assumption)
apply (auto dest!: LIM_const_eq)
done
@@ -198,7 +199,7 @@
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
with fs_lt gs_lt
have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
- hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
+ hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
qed
qed
@@ -228,7 +229,7 @@
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
apply (rule_tac x = xa in star_cases)
apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)
+apply (rule bexI [OF _ Rep_star_star_n], clarify)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
@@ -594,7 +595,7 @@
lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
apply clarify
-apply (cut_tac n1 = n
+apply (cut_tac n1 = n
in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
done
@@ -772,8 +773,8 @@
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
apply (auto simp add: diff_minus
- approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
- Infinitesimal_subset_HFinite [THEN subsetD])
+ approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
+ Infinitesimal_subset_HFinite [THEN subsetD])
done
lemma NSDERIVD4:
@@ -881,7 +882,7 @@
==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
apply (auto dest!: spec
- simp add: starfun_lambda_cancel lemma_nsderiv1)
+ simp add: starfun_lambda_cancel lemma_nsderiv1)
apply (simp (no_asm) add: add_divide_distrib)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
apply (auto simp add: times_divide_eq_right [symmetric]
@@ -1330,7 +1331,7 @@
apply (auto simp add: Bolzano_bisect_le Let_def split_def)
done
-lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
+lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
apply (auto)
apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
apply (simp)
@@ -1498,7 +1499,7 @@
lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
(\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
-apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
+apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
in lemma_reals_complete)
apply auto
apply (drule isCont_bounded, assumption)
@@ -1601,12 +1602,12 @@
assume "0 < h" "h < s"
with all [of h] show "f x < f (x+h)"
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
- split add: split_if_asm)
+ split add: split_if_asm)
assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
with l
have "0 < (f (x+h) - f x) / h" by arith
thus "f x < f (x+h)"
- by (simp add: pos_less_divide_eq h)
+ by (simp add: pos_less_divide_eq h)
qed
qed
qed
@@ -1630,12 +1631,12 @@
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
- split add: split_if_asm)
+ split add: split_if_asm)
assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l
have "0 < (f (x-h) - f x) / h" by arith
thus "f x < f (x-h)"
- by (simp add: pos_less_divide_eq h)
+ by (simp add: pos_less_divide_eq h)
qed
qed
qed
@@ -1742,9 +1743,9 @@
hence ax': "a<x'" and x'b: "x'<b" by auto
from lemma_interval [OF ax' x'b]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
- by blast
+ by blast
hence bound': "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min
- by blast
+ by blast
from differentiableD [OF dif [OF ax'b]]
obtain l where der: "DERIV f x' :> l" ..
have "l=0" by (rule DERIV_local_min [OF der d bound'])
@@ -1759,7 +1760,7 @@
obtain r where ar: "a < r" and rb: "r < b" by blast
from lemma_interval [OF ar rb]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
- by blast
+ by blast
have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b"
proof (clarify)
fix z::real
@@ -1798,7 +1799,7 @@
hence ba: "b-a \<noteq> 0" by arith
show ?thesis
by (rule real_mult_left_cancel [OF ba, THEN iffD1],
- simp add: right_diff_distrib,
+ simp add: right_diff_distrib,
simp add: left_diff_distrib)
qed
@@ -1888,10 +1889,10 @@
done
lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
-by (simp)
+by (simp)
lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
-by (simp)
+by (simp)
text{*Gallileo's "trick": average velocity = av. of end velocities*}
@@ -2060,6 +2061,319 @@
qed
qed
+
+lemma differentiable_const: "(\<lambda>z. a) differentiable x"
+ apply (unfold differentiable_def)
+ apply (rule_tac x=0 in exI)
+ apply simp
+ done
+
+lemma differentiable_sum:
+ assumes "f differentiable x"
+ and "g differentiable x"
+ shows "(\<lambda>x. f x + g x) differentiable x"
+proof -
+ from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+ then obtain df where "DERIV f x :> df" ..
+ moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+ then obtain dg where "DERIV g x :> dg" ..
+ ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
+ hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
+ thus ?thesis by (fold differentiable_def)
+qed
+
+lemma differentiable_diff:
+ assumes "f differentiable x"
+ and "g differentiable x"
+ shows "(\<lambda>x. f x - g x) differentiable x"
+proof -
+ from prems have "f differentiable x" by simp
+ moreover
+ from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+ then obtain dg where "DERIV g x :> dg" ..
+ then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
+ hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
+ hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
+ ultimately
+ show ?thesis
+ by (auto simp: real_diff_def dest: differentiable_sum)
+qed
+
+lemma differentiable_mult:
+ assumes "f differentiable x"
+ and "g differentiable x"
+ shows "(\<lambda>x. f x * g x) differentiable x"
+proof -
+ from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+ then obtain df where "DERIV f x :> df" ..
+ moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+ then obtain dg where "DERIV g x :> dg" ..
+ ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
+ hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
+ thus ?thesis by (fold differentiable_def)
+qed
+
+
+theorem GMVT:
+ assumes alb: "a < b"
+ and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
+ and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
+ and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
+ and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
+ shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
+proof -
+ let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
+ from prems have "a < b" by simp
+ moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
+ proof -
+ have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
+ with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
+ by (auto intro: isCont_mult)
+ moreover
+ have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
+ with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
+ by (auto intro: isCont_mult)
+ ultimately show ?thesis
+ by (fastsimp intro: isCont_diff)
+ qed
+ moreover
+ have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
+ proof -
+ have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
+ with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult)
+ moreover
+ have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
+ with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult)
+ ultimately show ?thesis by (simp add: differentiable_diff)
+ qed
+ ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
+ then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
+ then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
+
+ from cdef have cint: "a < c \<and> c < b" by auto
+ with gd have "g differentiable c" by simp
+ hence "\<exists>D. DERIV g c :> D" by (rule differentiableD)
+ then obtain g'c where g'cdef: "DERIV g c :> g'c" ..
+
+ from cdef have "a < c \<and> c < b" by auto
+ with fd have "f differentiable c" by simp
+ hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
+ then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
+
+ from cdef have "DERIV ?h c :> l" by auto
+ moreover
+ {
+ from g'cdef have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
+ apply (insert DERIV_const [where k="f b - f a"])
+ apply (drule meta_spec [of _ c])
+ apply (drule DERIV_mult [where f="(\<lambda>x. f b - f a)" and g=g])
+ by simp_all
+ moreover from f'cdef have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
+ apply (insert DERIV_const [where k="g b - g a"])
+ apply (drule meta_spec [of _ c])
+ apply (drule DERIV_mult [where f="(\<lambda>x. g b - g a)" and g=f])
+ by simp_all
+ ultimately have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)"
+ by (simp add: DERIV_diff)
+ }
+ ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
+
+ {
+ from cdef have "?h b - ?h a = (b - a) * l" by auto
+ also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
+ finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
+ }
+ moreover
+ {
+ have "?h b - ?h a =
+ ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) -
+ ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))"
+ by (simp add: mult_ac add_ac real_diff_mult_distrib)
+ hence "?h b - ?h a = 0" by auto
+ }
+ ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
+ with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
+ hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
+ hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
+
+ with g'cdef f'cdef cint show ?thesis by auto
+qed
+
+
+lemma LIMSEQ_SEQ_conv1:
+ assumes "X -- a --> L"
+ shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
+proof -
+ {
+ from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by (unfold LIM_def)
+
+ fix S
+ assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
+ then have "S ----> a" by auto
+ then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < r))" by (unfold LIMSEQ_def)
+ {
+ fix r
+ from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
+ {
+ assume rgz: "0 < r"
+
+ from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by simp
+ then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r)" by auto
+ then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r" by auto
+ {
+ fix n
+ from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
+ with as have imp2: "\<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" by auto
+ }
+ hence "\<forall>n. \<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" ..
+ moreover
+ from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
+ then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
+ ultimately have "\<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
+ hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by auto
+ }
+ }
+ hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X (S n) + -L\<bar> < r))" by simp
+ hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
+ }
+ thus ?thesis by simp
+qed
+
+lemma LIMSEQ_SEQ_conv2:
+ assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ shows "X -- a --> L"
+proof (rule ccontr)
+ assume "\<not> (X -- a --> L)"
+ hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by (unfold LIM_def)
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" by (simp add: linorder_not_less)
+ then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r))" by auto
+
+ let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ have "?F ----> a"
+ proof -
+ {
+ fix e::real
+ assume "0 < e"
+ (* choose no such that inverse (real (Suc n)) < e *)
+ have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
+ then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
+ {
+ fix n
+ assume mlen: "m \<le> n"
+ then have
+ "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
+ by auto
+ moreover have
+ "\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
+ proof -
+ from rdef have
+ "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ by simp
+ hence
+ "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X (?F n) + -L\<bar> \<ge> r"
+ by (simp add: some_eq_ex [symmetric])
+ thus ?thesis by simp
+ qed
+ moreover from nodef have
+ "inverse (real (Suc m)) < e" .
+ ultimately have "\<bar>?F n + -a\<bar> < e" by arith
+ }
+ then have "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n + -a\<bar> < e" by auto
+ }
+ thus ?thesis by (unfold LIMSEQ_def, simp)
+ qed
+
+ moreover have "\<forall>n. ?F n \<noteq> a"
+ proof -
+ {
+ fix n
+ from rdef have
+ "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ by simp
+ hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
+ }
+ thus ?thesis ..
+ qed
+ moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
+ ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
+
+ moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
+ proof -
+ {
+ fix no::nat
+ obtain n where "n = no + 1" by simp
+ then have nolen: "no \<le> n" by simp
+ (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
+ from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" ..
+
+ then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r" by simp
+
+ hence "\<bar>X (?F n) + -L\<bar> \<ge> r" by (simp add: some_eq_ex [symmetric])
+ with nolen have "\<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r" by auto
+ }
+ then have "(\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r)" by simp
+ with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> e)" by auto
+ thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
+ qed
+ ultimately show False by simp
+qed
+
+
+lemma LIMSEQ_SEQ_conv:
+ "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
+proof
+ assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
+next
+ assume "(X -- a --> L)"
+ show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
+qed
+
+lemma real_sqz:
+ fixes a::real
+ assumes "a < c"
+ shows "\<exists>b. a < b \<and> b < c"
+proof
+ let ?b = "(a + c) / 2"
+ have "a < ?b" by simp
+ moreover
+ have "?b < c" by simp
+ ultimately
+ show "a < ?b \<and> ?b < c" by simp
+qed
+
+lemma LIM_offset:
+ assumes "(\<lambda>x. f x) -- a --> L"
+ shows "(\<lambda>x. f (x+c)) -- (a-c) --> L"
+proof -
+ have "f -- a --> L" .
+ hence
+ fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r"
+ by (unfold LIM_def)
+ {
+ fix r::real
+ assume rgz: "0 < r"
+ with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r" by simp
+ then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>f x + -L\<bar> < r" by auto
+ from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+ {
+ fix x::real
+ from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
+ moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
+ moreover have "((x+c) + -a) = (x + -(a-c))" by simp
+ ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by simp
+ }
+ then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
+ with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+ }
+ then have
+ "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp
+ thus ?thesis by (fold LIM_def)
+qed
+
+
+
ML
{*
val LIM_def = thm"LIM_def";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ContNotDenum.thy Sun Feb 12 12:29:01 2006 +0100
@@ -0,0 +1,578 @@
+(* Title : HOL/Real/ContNonDenum
+ ID : $Id$
+ Author : Benjamin Porter, Monash University, NICTA, 2005
+*)
+
+header {* Non-denumerability of the Continuum. *}
+
+theory ContNotDenum
+imports RComplete
+begin
+
+section {* Abstract *}
+
+text {* The following document presents a proof that the Continuum is
+uncountable. It is formalised in the Isabelle/Isar theorem proving
+system.
+
+{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
+words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
+surjective.
+
+{\em Outline:} An elegant informal proof of this result uses Cantor's
+Diagonalisation argument. The proof presented here is not this
+one. First we formalise some properties of closed intervals, then we
+prove the Nested Interval Property. This property relies on the
+completeness of the Real numbers and is the foundation for our
+argument. Informally it states that an intersection of countable
+closed intervals (where each successive interval is a subset of the
+last) is non-empty. We then assume a surjective function f:@{text
+"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
+by generating a sequence of closed intervals then using the NIP. *}
+
+section {* Closed Intervals *}
+
+text {* This section formalises some properties of closed intervals. *}
+
+subsection {* Definition *}
+
+constdefs closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
+ "closed_int x y \<equiv> {z. x \<le> z \<and> z \<le> y}"
+
+subsection {* Properties *}
+
+lemma closed_int_subset:
+ assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
+ shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
+proof -
+ {
+ fix x::real
+ assume "x \<in> closed_int x1 y1"
+ hence "x \<ge> x1 \<and> x \<le> y1" by (unfold closed_int_def, simp)
+ with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
+ hence "x \<in> closed_int x0 y0" by (unfold closed_int_def, simp)
+ }
+ thus ?thesis by auto
+qed
+
+lemma closed_int_least:
+ assumes a: "a \<le> b"
+ shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
+proof
+ from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
+ thus "a \<in> closed_int a b" by (unfold closed_int_def)
+next
+ have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
+ thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
+qed
+
+lemma closed_int_most:
+ assumes a: "a \<le> b"
+ shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
+proof
+ from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
+ thus "b \<in> closed_int a b" by (unfold closed_int_def)
+next
+ have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
+ thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
+qed
+
+lemma closed_not_empty:
+ shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
+ by (auto dest: closed_int_least)
+
+lemma closed_mem:
+ assumes "a \<le> c" and "c \<le> b"
+ shows "c \<in> closed_int a b"
+ by (unfold closed_int_def) auto
+
+lemma closed_subset:
+ assumes ac: "a \<le> b" "c \<le> d"
+ assumes closed: "closed_int a b \<subseteq> closed_int c d"
+ shows "b \<ge> c"
+proof -
+ from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
+ hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
+ with ac have "c\<le>b \<and> b\<le>d" by simp
+ thus ?thesis by auto
+qed
+
+
+section {* Nested Interval Property *}
+
+theorem NIP:
+ fixes f::"nat \<Rightarrow> real set"
+ assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
+ and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
+ shows "(\<Inter>n. f n) \<noteq> {}"
+proof -
+ let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
+ have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
+ proof
+ fix n
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
+ then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
+ hence "a \<le> b" ..
+ with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
+ with fn show "\<exists>x. x\<in>(f n)" by simp
+ qed
+
+ have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
+ proof
+ fix n
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
+ then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
+ hence "a \<le> b" by simp
+ hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
+ with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
+ hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
+ thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
+ qed
+
+ -- "A denotes the set of all left-most points of all the intervals ..."
+ moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
+ ultimately have "\<exists>x. x\<in>A"
+ proof -
+ have "(0::nat) \<in> \<nat>" by simp
+ moreover have "?g 0 = ?g 0" by simp
+ ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
+ with Adef have "?g 0 \<in> A" by simp
+ thus ?thesis ..
+ qed
+
+ -- "Now show that A is bounded above ..."
+ moreover have "\<exists>y. isUb (UNIV::real set) A y"
+ proof -
+ {
+ fix n
+ from ne have ex: "\<exists>x. x\<in>(f n)" ..
+ from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
+ moreover
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
+ then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
+ hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
+ ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
+ with ex have "(?g n) \<le> b" by auto
+ hence "\<exists>b. (?g n) \<le> b" by auto
+ }
+ hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
+
+ have fs: "\<forall>n::nat. f n \<subseteq> f 0"
+ proof (rule allI, induct_tac n)
+ show "f 0 \<subseteq> f 0" by simp
+ next
+ fix n
+ assume "f n \<subseteq> f 0"
+ moreover from subset have "f (Suc n) \<subseteq> f n" ..
+ ultimately show "f (Suc n) \<subseteq> f 0" by simp
+ qed
+ have "\<forall>n. (?g n)\<in>(f 0)"
+ proof
+ fix n
+ from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
+ hence "?g n \<in> f n" ..
+ with fs show "?g n \<in> f 0" by auto
+ qed
+ moreover from closed
+ obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
+ ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
+ with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
+ with Adef have "\<forall>y\<in>A. y\<le>b" by auto
+ hence "A *<= b" by (unfold setle_def)
+ moreover have "b \<in> (UNIV::real set)" by simp
+ ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
+ hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
+ thus ?thesis by auto
+ qed
+ -- "by the Axiom Of Completeness, A has a least upper bound ..."
+ ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
+
+ -- "denote this least upper bound as t ..."
+ then obtain t where tdef: "isLub UNIV A t" ..
+
+ -- "and finally show that this least upper bound is in all the intervals..."
+ have "\<forall>n. t \<in> f n"
+ proof
+ fix n::nat
+ from closed obtain a and b where
+ int: "f n = closed_int a b" and alb: "a \<le> b" by blast
+
+ have "t \<ge> a"
+ proof -
+ have "a \<in> A"
+ proof -
+ (* by construction *)
+ from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
+ using closed_int_least by blast
+ moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
+ proof clarsimp
+ fix e
+ assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
+ from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
+
+ from ein aux have "a \<le> e \<and> e \<le> e" by auto
+ moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
+ ultimately show "e = a" by simp
+ qed
+ hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
+ ultimately have "(?g n) = a" by (rule some_equality)
+ moreover
+ {
+ have "n = of_nat n" by simp
+ moreover have "of_nat n \<in> \<nat>" by simp
+ ultimately have "n \<in> \<nat>"
+ apply -
+ apply (subst(asm) eq_sym_conv)
+ apply (erule subst)
+ .
+ }
+ with Adef have "(?g n) \<in> A" by auto
+ ultimately show ?thesis by simp
+ qed
+ with tdef show "a \<le> t" by (rule isLubD2)
+ qed
+ moreover have "t \<le> b"
+ proof -
+ have "isUb UNIV A b"
+ proof -
+ {
+ from alb int have
+ ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
+
+ have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
+ proof (rule allI, induct_tac m)
+ show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
+ next
+ fix m n
+ assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
+ {
+ fix p
+ from pp have "f (p + n) \<subseteq> f p" by simp
+ moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
+ hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
+ ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
+ }
+ thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
+ qed
+ have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
+ proof ((rule allI)+, rule impI)
+ fix \<alpha>::nat and \<beta>::nat
+ assume "\<beta> \<le> \<alpha>"
+ hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
+ then obtain k where "\<alpha> = \<beta> + k" ..
+ moreover
+ from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
+ ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
+ qed
+
+ fix m
+ {
+ assume "m \<ge> n"
+ with subsetm have "f m \<subseteq> f n" by simp
+ with ain have "\<forall>x\<in>f m. x \<le> b" by auto
+ moreover
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
+ ultimately have "?g m \<le> b" by auto
+ }
+ moreover
+ {
+ assume "\<not>(m \<ge> n)"
+ hence "m < n" by simp
+ with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
+ from closed obtain ma and mb where
+ "f m = closed_int ma mb \<and> ma \<le> mb" by blast
+ hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
+ from one alb sub fm int have "ma \<le> b" using closed_subset by blast
+ moreover have "(?g m) = ma"
+ proof -
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
+ moreover from one have
+ "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
+ by (rule closed_int_least)
+ with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
+ ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
+ thus "?g m = ma" by auto
+ qed
+ ultimately have "?g m \<le> b" by simp
+ }
+ ultimately have "?g m \<le> b" by (rule case_split)
+ }
+ with Adef have "\<forall>y\<in>A. y\<le>b" by auto
+ hence "A *<= b" by (unfold setle_def)
+ moreover have "b \<in> (UNIV::real set)" by simp
+ ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
+ thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
+ qed
+ with tdef show "t \<le> b" by (rule isLub_le_isUb)
+ qed
+ ultimately have "t \<in> closed_int a b" by (rule closed_mem)
+ with int show "t \<in> f n" by simp
+ qed
+ hence "t \<in> (\<Inter>n. f n)" by auto
+ thus ?thesis by auto
+qed
+
+section {* Generating the intervals *}
+
+subsubsection {* Existence of non-singleton closed intervals *}
+
+text {* This lemma asserts that given any non-singleton closed
+interval (a,b) and any element c, there exists a closed interval that
+is a subset of (a,b) and that does not contain c and is a
+non-singleton itself. *}
+
+lemma closed_subset_ex:
+ fixes c::real
+ assumes alb: "a < b"
+ shows
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+proof -
+ {
+ assume clb: "c < b"
+ {
+ assume cla: "c < a"
+ from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
+ with alb have
+ "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
+ by auto
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+ }
+ moreover
+ {
+ assume ncla: "\<not>(c < a)"
+ with clb have cdef: "a \<le> c \<and> c < b" by simp
+ obtain ka where kadef: "ka = (c + b)/2" by blast
+
+ from kadef clb have kalb: "ka < b" by auto
+ moreover from kadef cdef have kagc: "ka > c" by simp
+ ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
+ moreover from cdef kagc have "ka \<ge> a" by simp
+ hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+ ultimately have
+ "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+ using kalb by auto
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+
+ }
+ ultimately have
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by (rule case_split)
+ }
+ moreover
+ {
+ assume "\<not> (c < b)"
+ hence cgeb: "c \<ge> b" by simp
+
+ obtain kb where kbdef: "kb = (a + b)/2" by blast
+ with alb have kblb: "kb < b" by auto
+ with kbdef cgeb have "a < kb \<and> kb < c" by auto
+ moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
+ moreover from kblb have
+ "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+ ultimately have
+ "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
+ by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+ }
+ ultimately show ?thesis by (rule case_split)
+qed
+
+subsection {* newInt: Interval generation *}
+
+text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
+closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
+does not contain @{text "f (Suc n)"}. With the base case defined such
+that @{text "(f 0)\<notin>newInt 0 f"}. *}
+
+subsubsection {* Definition *}
+
+consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
+primrec
+"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+"newInt (Suc n) f =
+ (SOME e. (\<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> (newInt n f) \<and>
+ (f (Suc n)) \<notin> e)
+ )"
+
+subsubsection {* Properties *}
+
+text {* We now show that every application of newInt returns an
+appropriate interval. *}
+
+lemma newInt_ex:
+ "\<exists>a b. a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+proof (induct n)
+ case 0
+
+ let ?e = "SOME e. \<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> e"
+
+ have "newInt (Suc 0) f = ?e" by auto
+ moreover
+ have "f 0 + 1 < f 0 + 2" by simp
+ with closed_subset_ex have
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> (closed_int ka kb)" .
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
+ ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
+ by (rule someI_ex)
+ ultimately have "\<exists>e1 e2. e1 < e2 \<and>
+ newInt (Suc 0) f = closed_int e1 e2 \<and>
+ newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> newInt (Suc 0) f" by simp
+ thus
+ "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
+ newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
+ by simp
+next
+ case (Suc n)
+ hence "\<exists>a b.
+ a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f" by simp
+ then obtain a and b where ab: "a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f" by auto
+ hence cab: "closed_int a b = newInt (Suc n) f" by simp
+
+ let ?e = "SOME e. \<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> closed_int a b \<and>
+ f (Suc (Suc n)) \<notin> e"
+ from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
+
+ from ab have "a < b" by simp
+ with closed_subset_ex have
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
+ f (Suc (Suc n)) \<notin> closed_int ka kb" .
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
+ by simp
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
+ ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
+ with ab ni show
+ "\<exists>ka kb. ka < kb \<and>
+ newInt (Suc (Suc n)) f = closed_int ka kb \<and>
+ newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
+ f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
+qed
+
+lemma newInt_subset:
+ "newInt (Suc n) f \<subseteq> newInt n f"
+ using newInt_ex by auto
+
+
+text {* Another fundamental property is that no element in the range
+of f is in the intersection of all closed intervals generated by
+newInt. *}
+
+lemma newInt_inter:
+ "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+proof
+ fix n::nat
+ {
+ assume n0: "n = 0"
+ moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
+ ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
+ }
+ moreover
+ {
+ assume "\<not> n = 0"
+ hence "n > 0" by simp
+ then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
+
+ from newInt_ex have
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
+ then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
+ with ndef have "f n \<notin> newInt n f" by simp
+ }
+ ultimately have "f n \<notin> newInt n f" by (rule case_split)
+ thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
+qed
+
+
+lemma newInt_notempty:
+ "(\<Inter>n. newInt n f) \<noteq> {}"
+proof -
+ let ?g = "\<lambda>n. newInt n f"
+ have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
+ proof
+ fix n
+ show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
+ qed
+ moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
+ proof
+ fix n::nat
+ {
+ assume "n = 0"
+ then have
+ "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
+ by simp
+ hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ }
+ moreover
+ {
+ assume "\<not> n = 0"
+ then have "n > 0" by simp
+ then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
+
+ have
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
+ by (rule newInt_ex)
+ then obtain a and b where
+ "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
+ with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
+ hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ }
+ ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
+ qed
+ ultimately show ?thesis by (rule NIP)
+qed
+
+
+section {* Final Theorem *}
+
+theorem real_non_denum:
+ shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
+proof -- "by contradiction"
+ assume "\<exists>f::nat\<Rightarrow>real. surj f"
+ then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
+ hence rangeF: "range f = UNIV" by (rule surj_range)
+ -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
+ have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
+ moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
+ ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
+ moreover from rangeF have "x \<in> range f" by simp
+ ultimately show False by blast
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Real/Real.thy Sun Feb 12 10:42:19 2006 +0100
+++ b/src/HOL/Real/Real.thy Sun Feb 12 12:29:01 2006 +0100
@@ -1,4 +1,4 @@
theory Real
-imports RComplete RealPow
+imports ContNotDenum RealPow
begin
end
\ No newline at end of file
--- a/src/HOL/Real/RealDef.thy Sun Feb 12 10:42:19 2006 +0100
+++ b/src/HOL/Real/RealDef.thy Sun Feb 12 12:29:01 2006 +0100
@@ -929,7 +929,6 @@
instance real :: number_ring
by (intro_classes, simp add: real_number_of_def)
-
text{*Collapse applications of @{term real} to @{term number_of}*}
lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
by (simp add: real_of_int_def of_int_number_of_eq)
@@ -945,6 +944,19 @@
setup real_arith_setup
+
+lemma real_diff_mult_distrib:
+ fixes a::real
+ shows "a * (b - c) = a * b - a * c"
+proof -
+ have "a * (b - c) = a * (b + -c)" by simp
+ also have "\<dots> = (b + -c) * a" by simp
+ also have "\<dots> = b*a + (-c)*a" by (rule real_add_mult_distrib)
+ also have "\<dots> = a*b - a*c" by simp
+ finally show ?thesis .
+qed
+
+
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
text{*Needed in this non-standard form by Hyperreal/Transcendental*}
@@ -1027,7 +1039,6 @@
done
-
ML
{*
val real_lbound_gt_zero = thm"real_lbound_gt_zero";