src/HOL/Library/ContNotDenum.thy
 changeset 54263 c4159fe6fa46 parent 53372 f5a6313c7fe4 child 54797 be020ec8560c
```     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -131,17 +131,15 @@
1.4
1.5    -- "A denotes the set of all left-most points of all the intervals ..."
1.6    moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
1.7 -  ultimately have "\<exists>x. x\<in>A"
1.8 +  ultimately have "A \<noteq> {}"
1.9    proof -
1.10      have "(0::nat) \<in> \<nat>" by simp
1.11 -    moreover have "?g 0 = ?g 0" by simp
1.12 -    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
1.13 -    with Adef have "?g 0 \<in> A" by simp
1.14 -    thus ?thesis ..
1.15 +    with Adef show ?thesis
1.16 +      by blast
1.17    qed
1.18
1.19    -- "Now show that A is bounded above ..."
1.20 -  moreover have "\<exists>y. isUb (UNIV::real set) A y"
1.21 +  moreover have "bdd_above A"
1.22    proof -
1.23      {
1.24        fix n
1.25 @@ -177,18 +175,11 @@
1.26        obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
1.27      ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
1.28      with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
1.29 -    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
1.30 -    hence "A *<= b" by (unfold setle_def)
1.31 -    moreover have "b \<in> (UNIV::real set)" by simp
1.32 -    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
1.33 -    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
1.34 -    thus ?thesis by auto
1.35 +    with Adef show "bdd_above A" by auto
1.36    qed
1.37 -  -- "by the Axiom Of Completeness, A has a least upper bound ..."
1.38 -  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
1.39
1.40    -- "denote this least upper bound as t ..."
1.41 -  then obtain t where tdef: "isLub UNIV A t" ..
1.42 +  def tdef: t == "Sup A"
1.43
1.44    -- "and finally show that this least upper bound is in all the intervals..."
1.45    have "\<forall>n. t \<in> f n"
1.46 @@ -229,82 +220,76 @@
1.47          with Adef have "(?g n) \<in> A" by auto
1.48          ultimately show ?thesis by simp
1.49        qed
1.50 -      with tdef show "a \<le> t" by (rule isLubD2)
1.51 +      with `bdd_above A` show "a \<le> t"
1.52 +        unfolding tdef by (intro cSup_upper)
1.53      qed
1.54      moreover have "t \<le> b"
1.55 -    proof -
1.56 -      have "isUb UNIV A b"
1.57 -      proof -
1.58 -        {
1.59 -          from alb int have
1.60 -            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
1.61 -
1.62 -          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
1.63 -          proof (rule allI, induct_tac m)
1.64 -            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
1.65 -          next
1.66 -            fix m n
1.67 -            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
1.68 -            {
1.69 -              fix p
1.70 -              from pp have "f (p + n) \<subseteq> f p" by simp
1.71 -              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
1.72 -              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
1.73 -              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
1.74 -            }
1.75 -            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
1.76 -          qed
1.77 -          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
1.78 -          proof ((rule allI)+, rule impI)
1.79 -            fix \<alpha>::nat and \<beta>::nat
1.80 -            assume "\<beta> \<le> \<alpha>"
1.81 -            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
1.82 -            then obtain k where "\<alpha> = \<beta> + k" ..
1.83 -            moreover
1.84 -            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
1.85 -            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
1.86 -          qed
1.87 -
1.88 -          fix m
1.89 +      unfolding tdef
1.90 +    proof (rule cSup_least)
1.91 +      {
1.92 +        from alb int have
1.93 +          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
1.94 +
1.95 +        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
1.96 +        proof (rule allI, induct_tac m)
1.97 +          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
1.98 +        next
1.99 +          fix m n
1.100 +          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
1.101            {
1.102 -            assume "m \<ge> n"
1.103 -            with subsetm have "f m \<subseteq> f n" by simp
1.104 -            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
1.105 -            moreover
1.106 -            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
1.107 -            ultimately have "?g m \<le> b" by auto
1.108 +            fix p
1.109 +            from pp have "f (p + n) \<subseteq> f p" by simp
1.110 +            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
1.111 +            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
1.112 +            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
1.113            }
1.114 +          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
1.115 +        qed
1.116 +        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
1.117 +        proof ((rule allI)+, rule impI)
1.118 +          fix \<alpha>::nat and \<beta>::nat
1.119 +          assume "\<beta> \<le> \<alpha>"
1.120 +          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
1.121 +          then obtain k where "\<alpha> = \<beta> + k" ..
1.122 +          moreover
1.123 +          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
1.124 +          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
1.125 +        qed
1.126 +
1.127 +        fix m
1.128 +        {
1.129 +          assume "m \<ge> n"
1.130 +          with subsetm have "f m \<subseteq> f n" by simp
1.131 +          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
1.132            moreover
1.133 -          {
1.134 -            assume "\<not>(m \<ge> n)"
1.135 -            hence "m < n" by simp
1.136 -            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
1.137 -            from closed obtain ma and mb where
1.138 -              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
1.139 -            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
1.140 -            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
1.141 -            moreover have "(?g m) = ma"
1.142 -            proof -
1.143 -              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
1.144 -              moreover from one have
1.145 -                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
1.146 -                by (rule closed_int_least)
1.147 -              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
1.148 -              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
1.149 -              thus "?g m = ma" by auto
1.150 -            qed
1.151 -            ultimately have "?g m \<le> b" by simp
1.152 -          }
1.153 -          ultimately have "?g m \<le> b" by (rule case_split)
1.154 +          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
1.155 +          ultimately have "?g m \<le> b" by auto
1.156          }
1.157 -        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
1.158 -        hence "A *<= b" by (unfold setle_def)
1.159 -        moreover have "b \<in> (UNIV::real set)" by simp
1.160 -        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
1.161 -        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
1.162 -      qed
1.163 -      with tdef show "t \<le> b" by (rule isLub_le_isUb)
1.164 -    qed
1.165 +        moreover
1.166 +        {
1.167 +          assume "\<not>(m \<ge> n)"
1.168 +          hence "m < n" by simp
1.169 +          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
1.170 +          from closed obtain ma and mb where
1.171 +            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
1.172 +          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
1.173 +          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
1.174 +          moreover have "(?g m) = ma"
1.175 +          proof -
1.176 +            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
1.177 +            moreover from one have
1.178 +              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
1.179 +              by (rule closed_int_least)
1.180 +            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
1.181 +            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
1.182 +            thus "?g m = ma" by auto
1.183 +          qed
1.184 +          ultimately have "?g m \<le> b" by simp
1.185 +        }
1.186 +        ultimately have "?g m \<le> b" by (rule case_split)
1.187 +      }
1.188 +      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
1.189 +    qed fact
1.190      ultimately have "t \<in> closed_int a b" by (rule closed_mem)
1.191      with int show "t \<in> f n" by simp
1.192    qed
```