--- a/src/HOL/Library/ContNotDenum.thy Tue Dec 17 22:34:26 2013 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Wed Dec 18 11:53:40 2013 +0100
@@ -31,270 +31,43 @@
subsection {* Closed Intervals *}
-text {* This section formalises some properties of closed intervals. *}
-
-subsubsection {* Definition *}
-
-definition
- closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
- "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
-
-subsubsection {* Properties *}
-
-lemma closed_int_subset:
- assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
- shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
-proof -
- {
- fix x::real
- assume "x \<in> closed_int x1 y1"
- hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
- with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
- hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
- }
- thus ?thesis by auto
-qed
-
-lemma closed_int_least:
- assumes a: "a \<le> b"
- shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
-proof
- from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
- thus "a \<in> closed_int a b" by (unfold closed_int_def)
-next
- have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
- thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
-qed
-
-lemma closed_int_most:
- assumes a: "a \<le> b"
- shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
-proof
- from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
- thus "b \<in> closed_int a b" by (unfold closed_int_def)
-next
- have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
- thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
-qed
-
-lemma closed_not_empty:
- shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
- by (auto dest: closed_int_least)
-
-lemma closed_mem:
- assumes "a \<le> c" and "c \<le> b"
- shows "c \<in> closed_int a b"
- using assms unfolding closed_int_def by auto
-
-lemma closed_subset:
- assumes ac: "a \<le> b" "c \<le> d"
- assumes closed: "closed_int a b \<subseteq> closed_int c d"
- shows "b \<ge> c"
-proof -
- from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
- hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
- with ac have "c\<le>b \<and> b\<le>d" by simp
- thus ?thesis by auto
-qed
-
-
subsection {* Nested Interval Property *}
theorem NIP:
fixes f::"nat \<Rightarrow> real set"
assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
- and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
+ and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
shows "(\<Inter>n. f n) \<noteq> {}"
proof -
- let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
- have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
- proof
- fix n
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
- then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
- hence "a \<le> b" ..
- with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
- with fn show "\<exists>x. x\<in>(f n)" by simp
- qed
-
- have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
- proof
- fix n
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
- then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
- hence "a \<le> b" by simp
- hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
- with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
- hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
- thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
- qed
-
- -- "A denotes the set of all left-most points of all the intervals ..."
- moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
- ultimately have "A \<noteq> {}"
- proof -
- have "(0::nat) \<in> \<nat>" by simp
- with Adef show ?thesis
- by blast
- qed
-
- -- "Now show that A is bounded above ..."
- moreover have "bdd_above A"
- proof -
- {
- fix n
- from ne have ex: "\<exists>x. x\<in>(f n)" ..
- from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
- moreover
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
- then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
- hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
- ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
- with ex have "(?g n) \<le> b" by auto
- hence "\<exists>b. (?g n) \<le> b" by auto
- }
- hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
-
- have fs: "\<forall>n::nat. f n \<subseteq> f 0"
- proof (rule allI, induct_tac n)
- show "f 0 \<subseteq> f 0" by simp
- next
- fix n
- assume "f n \<subseteq> f 0"
- moreover from subset have "f (Suc n) \<subseteq> f n" ..
- ultimately show "f (Suc n) \<subseteq> f 0" by simp
- qed
- have "\<forall>n. (?g n)\<in>(f 0)"
- proof
- fix n
- from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
- hence "?g n \<in> f n" ..
- with fs show "?g n \<in> f 0" by auto
- qed
- moreover from closed
- obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
- ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
- with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
- with Adef show "bdd_above A" by auto
- qed
-
- -- "denote this least upper bound as t ..."
- def tdef: t == "Sup A"
-
- -- "and finally show that this least upper bound is in all the intervals..."
- have "\<forall>n. t \<in> f n"
- proof
- fix n::nat
- from closed obtain a and b where
- int: "f n = closed_int a b" and alb: "a \<le> b" by blast
+ let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
+ { fix n
+ from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
+ by auto
+ then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
+ by auto }
+ note f_eq = this
+ { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
+ by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
+ note subset' = this
- have "t \<ge> a"
- proof -
- have "a \<in> A"
- proof -
- (* by construction *)
- from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
- using closed_int_least by blast
- moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
- proof clarsimp
- fix e
- assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
- from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
-
- from ein aux have "a \<le> e \<and> e \<le> e" by auto
- moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
- ultimately show "e = a" by simp
- qed
- hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
- ultimately have "(?g n) = a" by (rule some_equality)
- moreover
- {
- have "n = of_nat n" by simp
- moreover have "of_nat n \<in> \<nat>" by simp
- ultimately have "n \<in> \<nat>"
- apply -
- apply (subst(asm) eq_sym_conv)
- apply (erule subst)
- .
- }
- with Adef have "(?g n) \<in> A" by auto
- ultimately show ?thesis by simp
- qed
- with `bdd_above A` show "a \<le> t"
- unfolding tdef by (intro cSup_upper)
+ have "compact (f 0)"
+ by (subst f_eq) (rule compact_Icc)
+ then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
+ proof (rule compact_imp_fip_image)
+ fix I :: "nat set" assume I: "finite I"
+ have "{} \<subset> f (Max (insert 0 I))"
+ using f_eq[of "Max (insert 0 I)"] by auto
+ also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
+ proof (rule INF_greatest)
+ fix i assume "i \<in> insert 0 I"
+ with I show "f (Max (insert 0 I)) \<subseteq> f i"
+ by (intro subset') auto
qed
- moreover have "t \<le> b"
- unfolding tdef
- proof (rule cSup_least)
- {
- from alb int have
- ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
-
- have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
- proof (rule allI, induct_tac m)
- show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
- next
- fix m n
- assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
- {
- fix p
- from pp have "f (p + n) \<subseteq> f p" by simp
- moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
- hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
- ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
- }
- thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
- qed
- have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
- proof ((rule allI)+, rule impI)
- fix \<alpha>::nat and \<beta>::nat
- assume "\<beta> \<le> \<alpha>"
- hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
- then obtain k where "\<alpha> = \<beta> + k" ..
- moreover
- from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
- ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
- qed
-
- fix m
- {
- assume "m \<ge> n"
- with subsetm have "f m \<subseteq> f n" by simp
- with ain have "\<forall>x\<in>f m. x \<le> b" by auto
- moreover
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
- ultimately have "?g m \<le> b" by auto
- }
- moreover
- {
- assume "\<not>(m \<ge> n)"
- hence "m < n" by simp
- with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
- from closed obtain ma and mb where
- "f m = closed_int ma mb \<and> ma \<le> mb" by blast
- hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
- from one alb sub fm int have "ma \<le> b" using closed_subset by blast
- moreover have "(?g m) = ma"
- proof -
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
- moreover from one have
- "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
- by (rule closed_int_least)
- with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
- ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
- thus "?g m = ma" by auto
- qed
- ultimately have "?g m \<le> b" by simp
- }
- ultimately have "?g m \<le> b" by (rule case_split)
- }
- with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
- qed fact
- ultimately have "t \<in> closed_int a b" by (rule closed_mem)
- with int show "t \<in> f n" by simp
- qed
- hence "t \<in> (\<Inter>n. f n)" by auto
- thus ?thesis by auto
+ finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
+ by auto
+ qed (subst f_eq, auto)
+ then show "(\<Inter>n. f n) \<noteq> {}"
+ by auto
qed
subsection {* Generating the intervals *}
@@ -309,14 +82,14 @@
lemma closed_subset_ex:
fixes c::real
assumes "a < b"
- shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
+ shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
proof (cases "c < b")
case True
show ?thesis
proof (cases "c < a")
case True
- with `a < b` `c < b` have "c \<notin> closed_int a b"
- unfolding closed_int_def by auto
+ with `a < b` `c < b` have "c \<notin> {a..b}"
+ by auto
with `a < b` show ?thesis by auto
next
case False
@@ -325,11 +98,11 @@
from ka_def `c < b` have kalb: "ka < b" by auto
moreover from ka_def `c < b` have kagc: "ka > c" by simp
- ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
+ ultimately have "c\<notin>{ka..b}" by auto
moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
- hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+ hence "{ka..b} \<subseteq> {a..b}" by auto
ultimately have
- "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+ "ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
using kalb by auto
then show ?thesis
by auto
@@ -341,11 +114,11 @@
def kb \<equiv> "(a + b)/2"
with `a < b` have "kb < b" by auto
with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
- from `kb < c` have c: "c \<notin> closed_int a kb"
- unfolding closed_int_def by auto
- with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
- unfolding closed_int_def by auto
- with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
+ from `kb < c` have c: "c \<notin> {a..kb}"
+ by auto
+ with `kb < b` have "{a..kb} \<subseteq> {a..b}"
+ by auto
+ with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
by simp
then show ?thesis by auto
qed
@@ -360,13 +133,13 @@
subsubsection {* Definition *}
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
- "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+ "newInt 0 f = {f 0 + 1..f 0 + 2}"
| "newInt (Suc n) f =
(SOME e. (\<exists>e1 e2.
e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> (newInt n f) \<and>
- (f (Suc n)) \<notin> e)
+ e = {e1..e2} \<and>
+ e \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> e)
)"
@@ -377,7 +150,7 @@
lemma newInt_ex:
"\<exists>a b. a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f = {a..b} \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f"
proof (induct n)
@@ -385,68 +158,67 @@
let ?e = "SOME e. \<exists>e1 e2.
e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
f (Suc 0) \<notin> e"
have "newInt (Suc 0) f = ?e" by auto
moreover
have "f 0 + 1 < f 0 + 2" by simp
with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
- f (Suc 0) \<notin> (closed_int ka kb)" .
+ "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+ f (Suc 0) \<notin> {ka..kb}" .
hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+ e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
hence
- "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
- ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
+ "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
by (rule someI_ex)
ultimately have "\<exists>e1 e2. e1 < e2 \<and>
- newInt (Suc 0) f = closed_int e1 e2 \<and>
- newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ newInt (Suc 0) f = {e1..e2} \<and>
+ newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
f (Suc 0) \<notin> newInt (Suc 0) f" by simp
thus
- "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
+ "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
by simp
next
case (Suc n)
hence "\<exists>a b.
a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f = {a..b} \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f" by simp
then obtain a and b where ab: "a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f = {a..b} \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f" by auto
- hence cab: "closed_int a b = newInt (Suc n) f" by simp
+ hence cab: "{a..b} = newInt (Suc n) f" by simp
let ?e = "SOME e. \<exists>e1 e2.
e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> closed_int a b \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {a..b} \<and>
f (Suc (Suc n)) \<notin> e"
from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
from ab have "a < b" by simp
with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
- f (Suc (Suc n)) \<notin> closed_int ka kb" .
+ "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
+ f (Suc (Suc n)) \<notin> {ka..kb}" .
hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+ {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
by simp
hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+ e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
hence
- "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
- ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
+ "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
+ ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
with ab ni show
"\<exists>ka kb. ka < kb \<and>
- newInt (Suc (Suc n)) f = closed_int ka kb \<and>
+ newInt (Suc (Suc n)) f = {ka..kb} \<and>
newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
qed
@@ -466,8 +238,8 @@
fix n::nat
{
assume n0: "n = 0"
- moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
- ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
+ moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
+ ultimately have "f n \<notin> newInt n f" by simp
}
moreover
{
@@ -476,7 +248,7 @@
then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
from newInt_ex have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
with ndef have "f n \<notin> newInt n f" by simp
@@ -495,15 +267,15 @@
fix n
show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
qed
- moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
+ moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
proof
fix n::nat
{
assume "n = 0"
then have
- "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
+ "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
by simp
- hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
}
moreover
{
@@ -512,15 +284,15 @@
then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
(newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
by (rule newInt_ex)
then obtain a and b where
- "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
- with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
- hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
+ with nd have "?g n = {a..b} \<and> a \<le> b" by auto
+ hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
}
- ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
+ ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
qed
ultimately show ?thesis by (rule NIP)
qed
@@ -542,3 +314,4 @@
qed
end
+