src/HOL/Library/ContNotDenum.thy
 changeset 60500 903bb1495239 parent 60308 f7e406aba90d child 61585 a9599d3d7610
```     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Wed Jun 17 10:57:11 2015 +0200
1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Jun 17 11:03:05 2015 +0200
1.3 @@ -3,15 +3,15 @@
1.4      Author:     Johannes Hölzl, TU München
1.5  *)
1.6
1.7 -section {* Non-denumerability of the Continuum. *}
1.8 +section \<open>Non-denumerability of the Continuum.\<close>
1.9
1.10  theory ContNotDenum
1.11  imports Complex_Main Countable_Set
1.12  begin
1.13
1.14 -subsection {* Abstract *}
1.15 +subsection \<open>Abstract\<close>
1.16
1.17 -text {* The following document presents a proof that the Continuum is
1.18 +text \<open>The following document presents a proof that the Continuum is
1.19  uncountable. It is formalised in the Isabelle/Isar theorem proving
1.20  system.
1.21
1.22 @@ -28,14 +28,14 @@
1.23  closed intervals (where each successive interval is a subset of the
1.24  last) is non-empty. We then assume a surjective function @{text
1.25  "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
1.26 -by generating a sequence of closed intervals then using the NIP. *}
1.27 +by generating a sequence of closed intervals then using the NIP.\<close>
1.28
1.29  theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
1.30  proof
1.31    assume "\<exists>f::nat \<Rightarrow> real. surj f"
1.32    then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
1.33
1.34 -  txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
1.35 +  txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
1.36
1.37    have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
1.38      using assms
1.39 @@ -55,7 +55,7 @@
1.40      "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
1.41      unfolding ivl_def by simp_all
1.42
1.43 -  txt {* This is a decreasing sequence of non-empty intervals. *}
1.44 +  txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
1.45
1.46    { fix n have "fst (ivl n) < snd (ivl n)"
1.47        by (induct n) (auto intro!: ij) }
1.48 @@ -64,7 +64,7 @@
1.49    have "decseq I"
1.50      unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
1.51
1.52 -  txt {* Now we apply the finite intersection property of compact sets. *}
1.53 +  txt \<open>Now we apply the finite intersection property of compact sets.\<close>
1.54
1.55    have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
1.56    proof (rule compact_imp_fip_image)
1.57 @@ -72,7 +72,7 @@
1.58      have "{} \<subset> I (Max (insert 0 S))"
1.59        unfolding I_def using less[of "Max (insert 0 S)"] by auto
1.60      also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
1.61 -      using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
1.62 +      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
1.63      also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
1.64        by auto
1.65      finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
1.66 @@ -80,7 +80,7 @@
1.67    qed (auto simp: I_def)
1.68    then obtain x where "\<And>n. x \<in> I n"
1.69      by blast
1.70 -  moreover from `surj f` obtain j where "x = f j"
1.71 +  moreover from \<open>surj f\<close> obtain j where "x = f j"
1.72      by blast
1.73    ultimately have "f j \<in> I (Suc j)"
1.74      by blast
1.75 @@ -124,7 +124,7 @@
1.76    show "uncountable {a<..<b}"
1.77    proof -
1.78      obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
1.79 -      using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
1.80 +      using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
1.81      then show ?thesis
1.82        by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
1.83    qed
```