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