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