src/HOL/Library/ContNotDenum.thy
 changeset 54797 be020ec8560c parent 54263 c4159fe6fa46 child 56796 9f84219715a7
```     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Dec 17 22:34:26 2013 +0100
1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 18 11:53:40 2013 +0100
1.3 @@ -31,270 +31,43 @@
1.4
1.5  subsection {* Closed Intervals *}
1.6
1.7 -text {* This section formalises some properties of closed intervals. *}
1.8 -
1.9 -subsubsection {* Definition *}
1.10 -
1.11 -definition
1.12 -  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
1.13 -  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
1.14 -
1.15 -subsubsection {* Properties *}
1.16 -
1.17 -lemma closed_int_subset:
1.18 -  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
1.19 -  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
1.20 -proof -
1.21 -  {
1.22 -    fix x::real
1.23 -    assume "x \<in> closed_int x1 y1"
1.24 -    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
1.25 -    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
1.26 -    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
1.27 -  }
1.28 -  thus ?thesis by auto
1.29 -qed
1.30 -
1.31 -lemma closed_int_least:
1.32 -  assumes a: "a \<le> b"
1.33 -  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
1.34 -proof
1.35 -  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
1.36 -  thus "a \<in> closed_int a b" by (unfold closed_int_def)
1.37 -next
1.38 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
1.39 -  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
1.40 -qed
1.41 -
1.42 -lemma closed_int_most:
1.43 -  assumes a: "a \<le> b"
1.44 -  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
1.45 -proof
1.46 -  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
1.47 -  thus "b \<in> closed_int a b" by (unfold closed_int_def)
1.48 -next
1.49 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
1.50 -  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
1.51 -qed
1.52 -
1.53 -lemma closed_not_empty:
1.54 -  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
1.55 -  by (auto dest: closed_int_least)
1.56 -
1.57 -lemma closed_mem:
1.58 -  assumes "a \<le> c" and "c \<le> b"
1.59 -  shows "c \<in> closed_int a b"
1.60 -  using assms unfolding closed_int_def by auto
1.61 -
1.62 -lemma closed_subset:
1.63 -  assumes ac: "a \<le> b"  "c \<le> d"
1.64 -  assumes closed: "closed_int a b \<subseteq> closed_int c d"
1.65 -  shows "b \<ge> c"
1.66 -proof -
1.67 -  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
1.68 -  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
1.69 -  with ac have "c\<le>b \<and> b\<le>d" by simp
1.70 -  thus ?thesis by auto
1.71 -qed
1.72 -
1.73 -
1.74  subsection {* Nested Interval Property *}
1.75
1.76  theorem NIP:
1.77    fixes f::"nat \<Rightarrow> real set"
1.78    assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
1.79 -  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
1.80 +  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
1.81    shows "(\<Inter>n. f n) \<noteq> {}"
1.82  proof -
1.83 -  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
1.84 -  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
1.85 -  proof
1.86 -    fix n
1.87 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
1.88 -    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
1.89 -    hence "a \<le> b" ..
1.90 -    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
1.91 -    with fn show "\<exists>x. x\<in>(f n)" by simp
1.92 -  qed
1.93 -
1.94 -  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
1.95 -  proof
1.96 -    fix n
1.97 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
1.98 -    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
1.99 -    hence "a \<le> b" by simp
1.100 -    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
1.101 -    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
1.102 -    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
1.103 -    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
1.104 -  qed
1.105 -
1.106 -  -- "A denotes the set of all left-most points of all the intervals ..."
1.107 -  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
1.108 -  ultimately have "A \<noteq> {}"
1.109 -  proof -
1.110 -    have "(0::nat) \<in> \<nat>" by simp
1.111 -    with Adef show ?thesis
1.112 -      by blast
1.113 -  qed
1.114 -
1.115 -  -- "Now show that A is bounded above ..."
1.116 -  moreover have "bdd_above A"
1.117 -  proof -
1.118 -    {
1.119 -      fix n
1.120 -      from ne have ex: "\<exists>x. x\<in>(f n)" ..
1.121 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
1.122 -      moreover
1.123 -      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
1.124 -      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
1.125 -      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
1.126 -      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
1.127 -      with ex have "(?g n) \<le> b" by auto
1.128 -      hence "\<exists>b. (?g n) \<le> b" by auto
1.129 -    }
1.130 -    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
1.131 -
1.132 -    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
1.133 -    proof (rule allI, induct_tac n)
1.134 -      show "f 0 \<subseteq> f 0" by simp
1.135 -    next
1.136 -      fix n
1.137 -      assume "f n \<subseteq> f 0"
1.138 -      moreover from subset have "f (Suc n) \<subseteq> f n" ..
1.139 -      ultimately show "f (Suc n) \<subseteq> f 0" by simp
1.140 -    qed
1.141 -    have "\<forall>n. (?g n)\<in>(f 0)"
1.142 -    proof
1.143 -      fix n
1.144 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
1.145 -      hence "?g n \<in> f n" ..
1.146 -      with fs show "?g n \<in> f 0" by auto
1.147 -    qed
1.148 -    moreover from closed
1.149 -      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
1.150 -    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
1.151 -    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
1.152 -    with Adef show "bdd_above A" by auto
1.153 -  qed
1.154 -
1.155 -  -- "denote this least upper bound as t ..."
1.156 -  def tdef: t == "Sup A"
1.157 -
1.158 -  -- "and finally show that this least upper bound is in all the intervals..."
1.159 -  have "\<forall>n. t \<in> f n"
1.160 -  proof
1.161 -    fix n::nat
1.162 -    from closed obtain a and b where
1.163 -      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
1.164 +  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
1.165 +  { fix n
1.166 +    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
1.167 +      by auto
1.168 +    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
1.169 +      by auto }
1.170 +  note f_eq = this
1.171 +  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
1.172 +      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
1.173 +  note subset' = this
1.174
1.175 -    have "t \<ge> a"
1.176 -    proof -
1.177 -      have "a \<in> A"
1.178 -      proof -
1.179 -          (* by construction *)
1.180 -        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
1.181 -          using closed_int_least by blast
1.182 -        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
1.183 -        proof clarsimp
1.184 -          fix e
1.185 -          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
1.186 -          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
1.187 -
1.188 -          from ein aux have "a \<le> e \<and> e \<le> e" by auto
1.189 -          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
1.190 -          ultimately show "e = a" by simp
1.191 -        qed
1.192 -        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
1.193 -        ultimately have "(?g n) = a" by (rule some_equality)
1.194 -        moreover
1.195 -        {
1.196 -          have "n = of_nat n" by simp
1.197 -          moreover have "of_nat n \<in> \<nat>" by simp
1.198 -          ultimately have "n \<in> \<nat>"
1.199 -            apply -
1.200 -            apply (subst(asm) eq_sym_conv)
1.201 -            apply (erule subst)
1.202 -            .
1.203 -        }
1.204 -        with Adef have "(?g n) \<in> A" by auto
1.205 -        ultimately show ?thesis by simp
1.206 -      qed
1.207 -      with `bdd_above A` show "a \<le> t"
1.208 -        unfolding tdef by (intro cSup_upper)
1.209 +  have "compact (f 0)"
1.210 +    by (subst f_eq) (rule compact_Icc)
1.211 +  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
1.212 +  proof (rule compact_imp_fip_image)
1.213 +    fix I :: "nat set" assume I: "finite I"
1.214 +    have "{} \<subset> f (Max (insert 0 I))"
1.215 +      using f_eq[of "Max (insert 0 I)"] by auto
1.216 +    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
1.217 +    proof (rule INF_greatest)
1.218 +      fix i assume "i \<in> insert 0 I"
1.219 +      with I show "f (Max (insert 0 I)) \<subseteq> f i"
1.220 +        by (intro subset') auto
1.221      qed
1.222 -    moreover have "t \<le> b"
1.223 -      unfolding tdef
1.224 -    proof (rule cSup_least)
1.225 -      {
1.226 -        from alb int have
1.227 -          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
1.228 -
1.229 -        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
1.230 -        proof (rule allI, induct_tac m)
1.231 -          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
1.232 -        next
1.233 -          fix m n
1.234 -          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
1.235 -          {
1.236 -            fix p
1.237 -            from pp have "f (p + n) \<subseteq> f p" by simp
1.238 -            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
1.239 -            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
1.240 -            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
1.241 -          }
1.242 -          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
1.243 -        qed
1.244 -        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
1.245 -        proof ((rule allI)+, rule impI)
1.246 -          fix \<alpha>::nat and \<beta>::nat
1.247 -          assume "\<beta> \<le> \<alpha>"
1.248 -          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
1.249 -          then obtain k where "\<alpha> = \<beta> + k" ..
1.250 -          moreover
1.251 -          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
1.252 -          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
1.253 -        qed
1.254 -
1.255 -        fix m
1.256 -        {
1.257 -          assume "m \<ge> n"
1.258 -          with subsetm have "f m \<subseteq> f n" by simp
1.259 -          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
1.260 -          moreover
1.261 -          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
1.262 -          ultimately have "?g m \<le> b" by auto
1.263 -        }
1.264 -        moreover
1.265 -        {
1.266 -          assume "\<not>(m \<ge> n)"
1.267 -          hence "m < n" by simp
1.268 -          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
1.269 -          from closed obtain ma and mb where
1.270 -            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
1.271 -          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
1.272 -          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
1.273 -          moreover have "(?g m) = ma"
1.274 -          proof -
1.275 -            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
1.276 -            moreover from one have
1.277 -              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
1.278 -              by (rule closed_int_least)
1.279 -            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
1.280 -            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
1.281 -            thus "?g m = ma" by auto
1.282 -          qed
1.283 -          ultimately have "?g m \<le> b" by simp
1.284 -        }
1.285 -        ultimately have "?g m \<le> b" by (rule case_split)
1.286 -      }
1.287 -      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
1.288 -    qed fact
1.289 -    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
1.290 -    with int show "t \<in> f n" by simp
1.291 -  qed
1.292 -  hence "t \<in> (\<Inter>n. f n)" by auto
1.293 -  thus ?thesis by auto
1.294 +    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
1.295 +      by auto
1.296 +  qed (subst f_eq, auto)
1.297 +  then show "(\<Inter>n. f n) \<noteq> {}"
1.298 +    by auto
1.299  qed
1.300
1.301  subsection {* Generating the intervals *}
1.302 @@ -309,14 +82,14 @@
1.303  lemma closed_subset_ex:
1.304    fixes c::real
1.305    assumes "a < b"
1.306 -  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
1.307 +  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
1.308  proof (cases "c < b")
1.309    case True
1.310    show ?thesis
1.311    proof (cases "c < a")
1.312      case True
1.313 -    with `a < b` `c < b` have "c \<notin> closed_int a b"
1.314 -      unfolding closed_int_def by auto
1.315 +    with `a < b` `c < b` have "c \<notin> {a..b}"
1.316 +      by auto
1.317      with `a < b` show ?thesis by auto
1.318    next
1.319      case False
1.320 @@ -325,11 +98,11 @@
1.321
1.322      from ka_def `c < b` have kalb: "ka < b" by auto
1.323      moreover from ka_def `c < b` have kagc: "ka > c" by simp
1.324 -    ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
1.325 +    ultimately have "c\<notin>{ka..b}" by auto
1.326      moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
1.327 -    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
1.328 +    hence "{ka..b} \<subseteq> {a..b}" by auto
1.329      ultimately have
1.330 -      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
1.331 +      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
1.332        using kalb by auto
1.333      then show ?thesis
1.334        by auto
1.335 @@ -341,11 +114,11 @@
1.336    def kb \<equiv> "(a + b)/2"
1.337    with `a < b` have "kb < b" by auto
1.338    with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
1.339 -  from `kb < c` have c: "c \<notin> closed_int a kb"
1.340 -    unfolding closed_int_def by auto
1.341 -  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
1.342 -    unfolding closed_int_def by auto
1.343 -  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
1.344 +  from `kb < c` have c: "c \<notin> {a..kb}"
1.345 +    by auto
1.346 +  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
1.347 +    by auto
1.348 +  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
1.349      by simp
1.350    then show ?thesis by auto
1.351  qed
1.352 @@ -360,13 +133,13 @@
1.353  subsubsection {* Definition *}
1.354
1.355  primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
1.356 -  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
1.357 +  "newInt 0 f = {f 0 + 1..f 0 + 2}"
1.358    | "newInt (Suc n) f =
1.359        (SOME e. (\<exists>e1 e2.
1.360         e1 < e2 \<and>
1.361 -       e = closed_int e1 e2 \<and>
1.362 -       e \<subseteq> (newInt n f) \<and>
1.363 -       (f (Suc n)) \<notin> e)
1.364 +       e = {e1..e2} \<and>
1.365 +       e \<subseteq> newInt n f \<and>
1.366 +       f (Suc n) \<notin> e)
1.367        )"
1.368
1.369
1.370 @@ -377,7 +150,7 @@
1.371
1.372  lemma newInt_ex:
1.373    "\<exists>a b. a < b \<and>
1.374 -   newInt (Suc n) f = closed_int a b \<and>
1.375 +   newInt (Suc n) f = {a..b} \<and>
1.376     newInt (Suc n) f \<subseteq> newInt n f \<and>
1.377     f (Suc n) \<notin> newInt (Suc n) f"
1.378  proof (induct n)
1.379 @@ -385,68 +158,67 @@
1.380
1.381    let ?e = "SOME e. \<exists>e1 e2.
1.382     e1 < e2 \<and>
1.383 -   e = closed_int e1 e2 \<and>
1.384 -   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
1.385 +   e = {e1..e2} \<and>
1.386 +   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
1.387     f (Suc 0) \<notin> e"
1.388
1.389    have "newInt (Suc 0) f = ?e" by auto
1.390    moreover
1.391    have "f 0 + 1 < f 0 + 2" by simp
1.392    with closed_subset_ex have
1.393 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
1.394 -     f (Suc 0) \<notin> (closed_int ka kb)" .
1.395 +    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
1.396 +     f (Suc 0) \<notin> {ka..kb}" .
1.397    hence
1.398 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
1.399 -     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
1.400 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
1.401 +     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
1.402    hence
1.403 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
1.404 -     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
1.405 +    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
1.406      by (rule someI_ex)
1.407    ultimately have "\<exists>e1 e2. e1 < e2 \<and>
1.408 -   newInt (Suc 0) f = closed_int e1 e2 \<and>
1.409 -   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
1.410 +   newInt (Suc 0) f = {e1..e2} \<and>
1.411 +   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
1.412     f (Suc 0) \<notin> newInt (Suc 0) f" by simp
1.413    thus
1.414 -    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
1.415 +    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
1.416       newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
1.417      by simp
1.418  next
1.419    case (Suc n)
1.420    hence "\<exists>a b.
1.421     a < b \<and>
1.422 -   newInt (Suc n) f = closed_int a b \<and>
1.423 +   newInt (Suc n) f = {a..b} \<and>
1.424     newInt (Suc n) f \<subseteq> newInt n f \<and>
1.425     f (Suc n) \<notin> newInt (Suc n) f" by simp
1.426    then obtain a and b where ab: "a < b \<and>
1.427 -   newInt (Suc n) f = closed_int a b \<and>
1.428 +   newInt (Suc n) f = {a..b} \<and>
1.429     newInt (Suc n) f \<subseteq> newInt n f \<and>
1.430     f (Suc n) \<notin> newInt (Suc n) f" by auto
1.431 -  hence cab: "closed_int a b = newInt (Suc n) f" by simp
1.432 +  hence cab: "{a..b} = newInt (Suc n) f" by simp
1.433
1.434    let ?e = "SOME e. \<exists>e1 e2.
1.435      e1 < e2 \<and>
1.436 -    e = closed_int e1 e2 \<and>
1.437 -    e \<subseteq> closed_int a b \<and>
1.438 +    e = {e1..e2} \<and>
1.439 +    e \<subseteq> {a..b} \<and>
1.440      f (Suc (Suc n)) \<notin> e"
1.441    from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
1.442
1.443    from ab have "a < b" by simp
1.444    with closed_subset_ex have
1.445 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
1.446 -     f (Suc (Suc n)) \<notin> closed_int ka kb" .
1.447 +    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
1.448 +     f (Suc (Suc n)) \<notin> {ka..kb}" .
1.449    hence
1.450 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
1.451 -     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
1.452 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
1.453 +     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
1.454      by simp
1.455    hence
1.456 -    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
1.457 -     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
1.458 +    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
1.459 +     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
1.460    hence
1.461 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
1.462 -     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
1.463 +    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
1.464 +     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
1.465    with ab ni show
1.466      "\<exists>ka kb. ka < kb \<and>
1.467 -     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
1.468 +     newInt (Suc (Suc n)) f = {ka..kb} \<and>
1.469       newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
1.470       f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
1.471  qed
1.472 @@ -466,8 +238,8 @@
1.473    fix n::nat
1.474    {
1.475      assume n0: "n = 0"
1.476 -    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
1.477 -    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
1.478 +    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
1.479 +    ultimately have "f n \<notin> newInt n f" by simp
1.480    }
1.481    moreover
1.482    {
1.483 @@ -476,7 +248,7 @@
1.484      then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
1.485
1.486      from newInt_ex have
1.487 -      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
1.488 +      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
1.489         newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
1.490      then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
1.491      with ndef have "f n \<notin> newInt n f" by simp
1.492 @@ -495,15 +267,15 @@
1.493      fix n
1.494      show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
1.495    qed
1.496 -  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
1.497 +  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
1.498    proof
1.499      fix n::nat
1.500      {
1.501        assume "n = 0"
1.502        then have
1.503 -        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
1.504 +        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
1.505          by simp
1.506 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
1.507 +      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
1.508      }
1.509      moreover
1.510      {
1.511 @@ -512,15 +284,15 @@
1.512        then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
1.513
1.514        have
1.515 -        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
1.516 +        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
1.517          (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
1.518          by (rule newInt_ex)
1.519        then obtain a and b where
1.520 -        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
1.521 -      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
1.522 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
1.523 +        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
1.524 +      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
1.525 +      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
1.526      }
1.527 -    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
1.528 +    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
1.529    qed
1.530    ultimately show ?thesis by (rule NIP)
1.531  qed
1.532 @@ -542,3 +314,4 @@
1.533  qed
1.534
1.535  end
1.536 +
```