move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -7,7 +7,7 @@
1.4 header {* Conditionally-complete Lattices *}
1.5
1.6 theory Conditionally_Complete_Lattices
1.7 -imports Main Lubs
1.8 +imports Main
1.9 begin
1.10
1.11 lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
1.12 @@ -28,6 +28,12 @@
1.13 lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
1.14 by (auto simp: bdd_below_def)
1.15
1.16 +lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
1.17 + by force
1.18 +
1.19 +lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
1.20 + by force
1.21 +
1.22 lemma bdd_above_empty [simp, intro]: "bdd_above {}"
1.23 unfolding bdd_above_def by auto
1.24
1.25 @@ -298,6 +304,12 @@
1.26 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
1.27 by (metis cSUP_least cSUP_upper assms order_trans)
1.28
1.29 +lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
1.30 + by (metis cINF_lower less_le_trans)
1.31 +
1.32 +lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
1.33 + by (metis cSUP_upper le_less_trans)
1.34 +
1.35 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
1.36 by (metis INF_def cInf_insert assms empty_is_image image_insert)
1.37
1.38 @@ -347,11 +359,6 @@
1.39 instance complete_lattice \<subseteq> conditionally_complete_lattice
1.40 by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
1.41
1.42 -lemma isLub_cSup:
1.43 - "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
1.44 - by (auto simp add: isLub_def setle_def leastP_def isUb_def
1.45 - intro!: setgeI cSup_upper cSup_least)
1.46 -
1.47 lemma cSup_eq:
1.48 fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
1.49 assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
1.50 @@ -370,12 +377,6 @@
1.51 assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
1.52 qed (intro cInf_eq_non_empty assms)
1.53
1.54 -lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
1.55 - by (metis cSup_least setle_def)
1.56 -
1.57 -lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
1.58 - by (metis cInf_greatest setge_def)
1.59 -
1.60 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
1.61 begin
1.62
1.63 @@ -386,6 +387,12 @@
1.64 lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
1.65 by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
1.66
1.67 +lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
1.68 + unfolding INF_def using cInf_less_iff[of "f`A"] by auto
1.69 +
1.70 +lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
1.71 + unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
1.72 +
1.73 lemma less_cSupE:
1.74 assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
1.75 by (metis cSup_least assms not_le that)
1.76 @@ -437,27 +444,6 @@
1.77 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
1.78 using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
1.79
1.80 -lemma cSup_bounds:
1.81 - fixes S :: "'a :: conditionally_complete_lattice set"
1.82 - assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
1.83 - shows "a \<le> Sup S \<and> Sup S \<le> b"
1.84 -proof-
1.85 - from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
1.86 - hence b: "Sup S \<le> b" using u
1.87 - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
1.88 - from Se obtain y where y: "y \<in> S" by blast
1.89 - from lub l have "a \<le> Sup S"
1.90 - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
1.91 - (metis le_iff_sup le_sup_iff y)
1.92 - with b show ?thesis by blast
1.93 -qed
1.94 -
1.95 -lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
1.96 - by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
1.97 -
1.98 -lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
1.99 - by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
1.100 -
1.101 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
1.102 by (auto intro!: cSup_eq_non_empty intro: dense_le)
1.103
2.1 --- a/src/HOL/Hahn_Banach/Bounds.thy Tue Nov 05 09:45:00 2013 +0100
2.2 +++ b/src/HOL/Hahn_Banach/Bounds.thy Tue Nov 05 09:45:02 2013 +0100
2.3 @@ -57,25 +57,7 @@
2.4 finally show ?thesis .
2.5 qed
2.6
2.7 -lemma lub_compat: "lub A x = isLub UNIV A x"
2.8 -proof -
2.9 - have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
2.10 - by (rule ext) (simp only: isUb_def)
2.11 - then show ?thesis
2.12 - by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
2.13 -qed
2.14 -
2.15 -lemma real_complete:
2.16 - fixes A :: "real set"
2.17 - assumes nonempty: "\<exists>a. a \<in> A"
2.18 - and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
2.19 - shows "\<exists>x. lub A x"
2.20 -proof -
2.21 - from ex_upper have "\<exists>y. isUb UNIV A y"
2.22 - unfolding isUb_def setle_def by blast
2.23 - with nonempty have "\<exists>x. isLub UNIV A x"
2.24 - by (rule reals_complete)
2.25 - then show ?thesis by (simp only: lub_compat)
2.26 -qed
2.27 +lemma real_complete: "\<exists>a::real. a \<in> A \<Longrightarrow> \<exists>y. \<forall>a \<in> A. a \<le> y \<Longrightarrow> \<exists>x. lub A x"
2.28 + by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def)
2.29
2.30 end
3.1 --- a/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:00 2013 +0100
3.2 +++ b/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:02 2013 +0100
3.3 @@ -131,17 +131,15 @@
3.4
3.5 -- "A denotes the set of all left-most points of all the intervals ..."
3.6 moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
3.7 - ultimately have "\<exists>x. x\<in>A"
3.8 + ultimately have "A \<noteq> {}"
3.9 proof -
3.10 have "(0::nat) \<in> \<nat>" by simp
3.11 - moreover have "?g 0 = ?g 0" by simp
3.12 - ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
3.13 - with Adef have "?g 0 \<in> A" by simp
3.14 - thus ?thesis ..
3.15 + with Adef show ?thesis
3.16 + by blast
3.17 qed
3.18
3.19 -- "Now show that A is bounded above ..."
3.20 - moreover have "\<exists>y. isUb (UNIV::real set) A y"
3.21 + moreover have "bdd_above A"
3.22 proof -
3.23 {
3.24 fix n
3.25 @@ -177,18 +175,11 @@
3.26 obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
3.27 ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
3.28 with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
3.29 - with Adef have "\<forall>y\<in>A. y\<le>b" by auto
3.30 - hence "A *<= b" by (unfold setle_def)
3.31 - moreover have "b \<in> (UNIV::real set)" by simp
3.32 - ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
3.33 - hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
3.34 - thus ?thesis by auto
3.35 + with Adef show "bdd_above A" by auto
3.36 qed
3.37 - -- "by the Axiom Of Completeness, A has a least upper bound ..."
3.38 - ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
3.39
3.40 -- "denote this least upper bound as t ..."
3.41 - then obtain t where tdef: "isLub UNIV A t" ..
3.42 + def tdef: t == "Sup A"
3.43
3.44 -- "and finally show that this least upper bound is in all the intervals..."
3.45 have "\<forall>n. t \<in> f n"
3.46 @@ -229,82 +220,76 @@
3.47 with Adef have "(?g n) \<in> A" by auto
3.48 ultimately show ?thesis by simp
3.49 qed
3.50 - with tdef show "a \<le> t" by (rule isLubD2)
3.51 + with `bdd_above A` show "a \<le> t"
3.52 + unfolding tdef by (intro cSup_upper)
3.53 qed
3.54 moreover have "t \<le> b"
3.55 - proof -
3.56 - have "isUb UNIV A b"
3.57 - proof -
3.58 + unfolding tdef
3.59 + proof (rule cSup_least)
3.60 + {
3.61 + from alb int have
3.62 + ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
3.63 +
3.64 + have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
3.65 + proof (rule allI, induct_tac m)
3.66 + show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
3.67 + next
3.68 + fix m n
3.69 + assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
3.70 + {
3.71 + fix p
3.72 + from pp have "f (p + n) \<subseteq> f p" by simp
3.73 + moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
3.74 + hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
3.75 + ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
3.76 + }
3.77 + thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
3.78 + qed
3.79 + have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
3.80 + proof ((rule allI)+, rule impI)
3.81 + fix \<alpha>::nat and \<beta>::nat
3.82 + assume "\<beta> \<le> \<alpha>"
3.83 + hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
3.84 + then obtain k where "\<alpha> = \<beta> + k" ..
3.85 + moreover
3.86 + from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
3.87 + ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
3.88 + qed
3.89 +
3.90 + fix m
3.91 {
3.92 - from alb int have
3.93 - ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
3.94 -
3.95 - have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
3.96 - proof (rule allI, induct_tac m)
3.97 - show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
3.98 - next
3.99 - fix m n
3.100 - assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
3.101 - {
3.102 - fix p
3.103 - from pp have "f (p + n) \<subseteq> f p" by simp
3.104 - moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
3.105 - hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
3.106 - ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
3.107 - }
3.108 - thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
3.109 - qed
3.110 - have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
3.111 - proof ((rule allI)+, rule impI)
3.112 - fix \<alpha>::nat and \<beta>::nat
3.113 - assume "\<beta> \<le> \<alpha>"
3.114 - hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
3.115 - then obtain k where "\<alpha> = \<beta> + k" ..
3.116 - moreover
3.117 - from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
3.118 - ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
3.119 - qed
3.120 -
3.121 - fix m
3.122 - {
3.123 - assume "m \<ge> n"
3.124 - with subsetm have "f m \<subseteq> f n" by simp
3.125 - with ain have "\<forall>x\<in>f m. x \<le> b" by auto
3.126 - moreover
3.127 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
3.128 - ultimately have "?g m \<le> b" by auto
3.129 - }
3.130 + assume "m \<ge> n"
3.131 + with subsetm have "f m \<subseteq> f n" by simp
3.132 + with ain have "\<forall>x\<in>f m. x \<le> b" by auto
3.133 moreover
3.134 - {
3.135 - assume "\<not>(m \<ge> n)"
3.136 - hence "m < n" by simp
3.137 - with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
3.138 - from closed obtain ma and mb where
3.139 - "f m = closed_int ma mb \<and> ma \<le> mb" by blast
3.140 - hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
3.141 - from one alb sub fm int have "ma \<le> b" using closed_subset by blast
3.142 - moreover have "(?g m) = ma"
3.143 - proof -
3.144 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
3.145 - moreover from one have
3.146 - "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
3.147 - by (rule closed_int_least)
3.148 - with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
3.149 - ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
3.150 - thus "?g m = ma" by auto
3.151 - qed
3.152 - ultimately have "?g m \<le> b" by simp
3.153 - }
3.154 - ultimately have "?g m \<le> b" by (rule case_split)
3.155 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
3.156 + ultimately have "?g m \<le> b" by auto
3.157 }
3.158 - with Adef have "\<forall>y\<in>A. y\<le>b" by auto
3.159 - hence "A *<= b" by (unfold setle_def)
3.160 - moreover have "b \<in> (UNIV::real set)" by simp
3.161 - ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
3.162 - thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
3.163 - qed
3.164 - with tdef show "t \<le> b" by (rule isLub_le_isUb)
3.165 - qed
3.166 + moreover
3.167 + {
3.168 + assume "\<not>(m \<ge> n)"
3.169 + hence "m < n" by simp
3.170 + with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
3.171 + from closed obtain ma and mb where
3.172 + "f m = closed_int ma mb \<and> ma \<le> mb" by blast
3.173 + hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
3.174 + from one alb sub fm int have "ma \<le> b" using closed_subset by blast
3.175 + moreover have "(?g m) = ma"
3.176 + proof -
3.177 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
3.178 + moreover from one have
3.179 + "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
3.180 + by (rule closed_int_least)
3.181 + with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
3.182 + ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
3.183 + thus "?g m = ma" by auto
3.184 + qed
3.185 + ultimately have "?g m \<le> b" by simp
3.186 + }
3.187 + ultimately have "?g m \<le> b" by (rule case_split)
3.188 + }
3.189 + with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
3.190 + qed fact
3.191 ultimately have "t \<in> closed_int a b" by (rule closed_mem)
3.192 with int show "t \<in> f n" by simp
3.193 qed
4.1 --- a/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:00 2013 +0100
4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:02 2013 +0100
4.3 @@ -451,7 +451,7 @@
4.4
4.5 definition
4.6 dist_fps_def: "dist (a::'a fps) b =
4.7 - (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
4.8 + (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
4.9
4.10 lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
4.11 by (simp add: dist_fps_def)
4.12 @@ -467,34 +467,6 @@
4.13
4.14 end
4.15
4.16 -lemma fps_nonzero_least_unique:
4.17 - assumes a0: "a \<noteq> 0"
4.18 - shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n"
4.19 -proof -
4.20 - from fps_nonzero_nth_minimal [of a] a0
4.21 - obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast
4.22 - then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n"
4.23 - by (auto simp add: leastP_def setge_def not_le [symmetric])
4.24 - moreover
4.25 - {
4.26 - fix m
4.27 - assume "leastP (\<lambda>n. a $ n \<noteq> 0) m"
4.28 - then have "m = n" using ln
4.29 - apply (auto simp add: leastP_def setge_def)
4.30 - apply (erule allE[where x=n])
4.31 - apply (erule allE[where x=m])
4.32 - apply simp
4.33 - done
4.34 - }
4.35 - ultimately show ?thesis by blast
4.36 -qed
4.37 -
4.38 -lemma fps_eq_least_unique:
4.39 - assumes "(a::('a::ab_group_add) fps) \<noteq> b"
4.40 - shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
4.41 - using fps_nonzero_least_unique[of "a - b"] assms
4.42 - by auto
4.43 -
4.44 instantiation fps :: (comm_ring_1) metric_space
4.45 begin
4.46
4.47 @@ -540,31 +512,15 @@
4.48 moreover
4.49 {
4.50 assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
4.51 - let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
4.52 - from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac]
4.53 - fps_eq_least_unique[OF bc]
4.54 - obtain nab nac nbc where nab: "leastP (?P a b) nab"
4.55 - and nac: "leastP (?P a c) nac"
4.56 - and nbc: "leastP (?P b c) nbc" by blast
4.57 - from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab"
4.58 - by (auto simp add: leastP_def setge_def)
4.59 - from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac"
4.60 - by (auto simp add: leastP_def setge_def)
4.61 - from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc"
4.62 - by (auto simp add: leastP_def setge_def)
4.63 -
4.64 - have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
4.65 - by (simp add: fps_eq_iff)
4.66 - from ab ac bc nab nac nbc
4.67 - have dab: "dist a b = inverse (2 ^ nab)"
4.68 - and dac: "dist a c = inverse (2 ^ nac)"
4.69 - and dbc: "dist b c = inverse (2 ^ nbc)"
4.70 - unfolding th0
4.71 - apply (simp_all add: dist_fps_def)
4.72 - apply (erule the1_equality[OF fps_eq_least_unique[OF ab]])
4.73 - apply (erule the1_equality[OF fps_eq_least_unique[OF ac]])
4.74 - apply (erule the1_equality[OF fps_eq_least_unique[OF bc]])
4.75 - done
4.76 + def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
4.77 + then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
4.78 + by (auto dest: not_less_Least)
4.79 +
4.80 + from ab ac bc
4.81 + have dab: "dist a b = inverse (2 ^ n a b)"
4.82 + and dac: "dist a c = inverse (2 ^ n a c)"
4.83 + and dbc: "dist b c = inverse (2 ^ n b c)"
4.84 + by (simp_all add: dist_fps_def n_def fps_eq_iff)
4.85 from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
4.86 unfolding th by simp_all
4.87 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
4.88 @@ -575,11 +531,13 @@
4.89 assume h: "dist a b > dist a c + dist b c"
4.90 then have gt: "dist a b > dist a c" "dist a b > dist b c"
4.91 using pos by auto
4.92 - from gt have gtn: "nab < nbc" "nab < nac"
4.93 + from gt have gtn: "n a b < n b c" "n a b < n a c"
4.94 unfolding dab dbc dac by (auto simp add: th1)
4.95 - from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)]
4.96 - have "a $ nab = b $ nab" by simp
4.97 - with nab'(2) have False by simp
4.98 + from n'[OF gtn(2)] n'(1)[OF gtn(1)]
4.99 + have "a $ n a b = b $ n a b" by simp
4.100 + moreover have "a $ n a b \<noteq> b $ n a b"
4.101 + unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff)
4.102 + ultimately have False by contradiction
4.103 }
4.104 then have "dist a b \<le> dist a c + dist b c"
4.105 by (auto simp add: not_le[symmetric])
4.106 @@ -649,17 +607,12 @@
4.107 moreover
4.108 {
4.109 assume neq: "?s n \<noteq> a"
4.110 - from fps_eq_least_unique[OF neq]
4.111 - obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast
4.112 - have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
4.113 - by (simp add: fps_eq_iff)
4.114 + def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i"
4.115 from neq have dth: "dist (?s n) a = (1/2)^k"
4.116 - unfolding th0 dist_fps_def
4.117 - unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k]
4.118 - by (auto simp add: inverse_eq_divide power_divide)
4.119 -
4.120 - from k have kn: "k > n"
4.121 - by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
4.122 + by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
4.123 +
4.124 + from neq have kn: "k > n"
4.125 + by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
4.126 then have "dist (?s n) a < (1/2)^n" unfolding dth
4.127 by (auto intro: power_strict_decreasing)
4.128 also have "\<dots> <= (1/2)^n0" using nn0
4.129 @@ -3797,20 +3750,14 @@
4.130 assumes "dist f g < inverse (2 ^ i)"
4.131 and"j \<le> i"
4.132 shows "f $ j = g $ j"
4.133 -proof (cases "f = g")
4.134 - case False
4.135 - hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
4.136 - with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
4.137 +proof (rule ccontr)
4.138 + assume "f $ j \<noteq> g $ j"
4.139 + then have "\<exists>n. f $ n \<noteq> g $ n" by auto
4.140 + with assms have "i < (LEAST n. f $ n \<noteq> g $ n)"
4.141 by (simp add: split_if_asm dist_fps_def)
4.142 - moreover
4.143 - from fps_eq_least_unique[OF `f \<noteq> g`]
4.144 - obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
4.145 - moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
4.146 - by (auto simp add: leastP_def setge_def)
4.147 - ultimately show ?thesis using `j \<le> i` by simp
4.148 -next
4.149 - case True
4.150 - then show ?thesis by simp
4.151 + also have "\<dots> \<le> j"
4.152 + using `f $ j \<noteq> g $ j` by (auto intro: Least_le)
4.153 + finally show False using `j \<le> i` by simp
4.154 qed
4.155
4.156 lemma nth_equal_imp_dist_less:
4.157 @@ -3819,18 +3766,13 @@
4.158 proof (cases "f = g")
4.159 case False
4.160 hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
4.161 - with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
4.162 + with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))"
4.163 by (simp add: split_if_asm dist_fps_def)
4.164 moreover
4.165 - from fps_eq_least_unique[OF `f \<noteq> g`]
4.166 - obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
4.167 - with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
4.168 - by (metis (full_types) leastPD1 not_le)
4.169 + from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)"
4.170 + by (metis (mono_tags) LeastI not_less)
4.171 ultimately show ?thesis by simp
4.172 -next
4.173 - case True
4.174 - then show ?thesis by simp
4.175 -qed
4.176 +qed simp
4.177
4.178 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
4.179 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
5.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 05 09:45:00 2013 +0100
5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 05 09:45:02 2013 +0100
5.3 @@ -156,28 +156,11 @@
5.4 text{* An alternative useful formulation of completeness of the reals *}
5.5 lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
5.6 shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
5.7 -proof-
5.8 - from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y" by blast
5.9 - from ex have thx:"\<exists>x. x \<in> Collect P" by blast
5.10 - from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
5.11 - by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
5.12 - from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
5.13 - by blast
5.14 - from Y[OF x] have xY: "x < Y" .
5.15 - from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.16 - from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
5.17 - apply (clarsimp, atomize (full)) by auto
5.18 - from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.19 - {fix y
5.20 - {fix z assume z: "P z" "y < z"
5.21 - from L' z have "y < L" by auto }
5.22 - moreover
5.23 - {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
5.24 - hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
5.25 - from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.26 - with yL(1) have False by arith}
5.27 - ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
5.28 - thus ?thesis by blast
5.29 +proof
5.30 + from bz have "bdd_above (Collect P)"
5.31 + by (force intro: less_imp_le)
5.32 + then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
5.33 + using ex bz by (subst less_cSup_iff) auto
5.34 qed
5.35
5.36 subsection {* Fundamental theorem of algebra *}
6.1 --- a/src/HOL/Library/Glbs.thy Tue Nov 05 09:45:00 2013 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,79 +0,0 @@
6.4 -(* Author: Amine Chaieb, University of Cambridge *)
6.5 -
6.6 -header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
6.7 -
6.8 -theory Glbs
6.9 -imports Lubs
6.10 -begin
6.11 -
6.12 -definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
6.13 - where "greatestP P x = (P x \<and> Collect P *<= x)"
6.14 -
6.15 -definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
6.16 - where "isLb R S x = (x <=* S \<and> x: R)"
6.17 -
6.18 -definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
6.19 - where "isGlb R S x = greatestP (isLb R S) x"
6.20 -
6.21 -definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
6.22 - where "lbs R S = Collect (isLb R S)"
6.23 -
6.24 -
6.25 -subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
6.26 - and @{term isGlb} *}
6.27 -
6.28 -lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
6.29 - by (simp add: greatestP_def)
6.30 -
6.31 -lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
6.32 - by (simp add: greatestP_def)
6.33 -
6.34 -lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
6.35 - by (blast dest!: greatestPD2 setleD)
6.36 -
6.37 -lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
6.38 - by (simp add: isGlb_def isLb_def greatestP_def)
6.39 -
6.40 -lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
6.41 - by (simp add: isGlb_def isLb_def greatestP_def)
6.42 -
6.43 -lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
6.44 - unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
6.45 -
6.46 -lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
6.47 - by (blast dest!: isGlbD1 setgeD)
6.48 -
6.49 -lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
6.50 - by (simp add: isGlb_def)
6.51 -
6.52 -lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
6.53 - by (simp add: isGlb_def)
6.54 -
6.55 -lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
6.56 - by (simp add: isGlb_def greatestP_def)
6.57 -
6.58 -lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
6.59 - by (simp add: isLb_def setge_def)
6.60 -
6.61 -lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
6.62 - by (simp add: isLb_def)
6.63 -
6.64 -lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
6.65 - by (simp add: isLb_def)
6.66 -
6.67 -lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
6.68 - by (simp add: isLb_def)
6.69 -
6.70 -lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
6.71 - unfolding isGlb_def by (blast intro!: greatestPD3)
6.72 -
6.73 -lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
6.74 - unfolding lbs_def isGlb_def by (rule greatestPD2)
6.75 -
6.76 -lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
6.77 - apply (frule isGlb_isLb)
6.78 - apply (frule_tac x = y in isGlb_isLb)
6.79 - apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
6.80 - done
6.81 -
6.82 -end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Library/Lubs_Glbs.thy Tue Nov 05 09:45:02 2013 +0100
7.3 @@ -0,0 +1,245 @@
7.4 +(* Title: HOL/Library/Lubs_Glbs.thy
7.5 + Author: Jacques D. Fleuriot, University of Cambridge
7.6 + Author: Amine Chaieb, University of Cambridge *)
7.7 +
7.8 +header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
7.9 +
7.10 +theory Lubs_Glbs
7.11 +imports Complex_Main
7.12 +begin
7.13 +
7.14 +text {* Thanks to suggestions by James Margetson *}
7.15 +
7.16 +definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70)
7.17 + where "S *<= x = (ALL y: S. y \<le> x)"
7.18 +
7.19 +definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70)
7.20 + where "x <=* S = (ALL y: S. x \<le> y)"
7.21 +
7.22 +
7.23 +subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
7.24 +
7.25 +lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
7.26 + by (simp add: setle_def)
7.27 +
7.28 +lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
7.29 + by (simp add: setle_def)
7.30 +
7.31 +lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
7.32 + by (simp add: setge_def)
7.33 +
7.34 +lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
7.35 + by (simp add: setge_def)
7.36 +
7.37 +
7.38 +definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.39 + where "leastP P x = (P x \<and> x <=* Collect P)"
7.40 +
7.41 +definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.42 + where "isUb R S x = (S *<= x \<and> x: R)"
7.43 +
7.44 +definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.45 + where "isLub R S x = leastP (isUb R S) x"
7.46 +
7.47 +definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
7.48 + where "ubs R S = Collect (isUb R S)"
7.49 +
7.50 +
7.51 +subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
7.52 +
7.53 +lemma leastPD1: "leastP P x \<Longrightarrow> P x"
7.54 + by (simp add: leastP_def)
7.55 +
7.56 +lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
7.57 + by (simp add: leastP_def)
7.58 +
7.59 +lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
7.60 + by (blast dest!: leastPD2 setgeD)
7.61 +
7.62 +lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
7.63 + by (simp add: isLub_def isUb_def leastP_def)
7.64 +
7.65 +lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
7.66 + by (simp add: isLub_def isUb_def leastP_def)
7.67 +
7.68 +lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
7.69 + unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
7.70 +
7.71 +lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
7.72 + by (blast dest!: isLubD1 setleD)
7.73 +
7.74 +lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
7.75 + by (simp add: isLub_def)
7.76 +
7.77 +lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
7.78 + by (simp add: isLub_def)
7.79 +
7.80 +lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
7.81 + by (simp add: isLub_def leastP_def)
7.82 +
7.83 +lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
7.84 + by (simp add: isUb_def setle_def)
7.85 +
7.86 +lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
7.87 + by (simp add: isUb_def)
7.88 +
7.89 +lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
7.90 + by (simp add: isUb_def)
7.91 +
7.92 +lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
7.93 + by (simp add: isUb_def)
7.94 +
7.95 +lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
7.96 + unfolding isLub_def by (blast intro!: leastPD3)
7.97 +
7.98 +lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
7.99 + unfolding ubs_def isLub_def by (rule leastPD2)
7.100 +
7.101 +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
7.102 + apply (frule isLub_isUb)
7.103 + apply (frule_tac x = y in isLub_isUb)
7.104 + apply (blast intro!: order_antisym dest!: isLub_le_isUb)
7.105 + done
7.106 +
7.107 +lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
7.108 + by (simp add: isUbI setleI)
7.109 +
7.110 +
7.111 +definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.112 + where "greatestP P x = (P x \<and> Collect P *<= x)"
7.113 +
7.114 +definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.115 + where "isLb R S x = (x <=* S \<and> x: R)"
7.116 +
7.117 +definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
7.118 + where "isGlb R S x = greatestP (isLb R S) x"
7.119 +
7.120 +definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
7.121 + where "lbs R S = Collect (isLb R S)"
7.122 +
7.123 +
7.124 +subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *}
7.125 +
7.126 +lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
7.127 + by (simp add: greatestP_def)
7.128 +
7.129 +lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
7.130 + by (simp add: greatestP_def)
7.131 +
7.132 +lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
7.133 + by (blast dest!: greatestPD2 setleD)
7.134 +
7.135 +lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
7.136 + by (simp add: isGlb_def isLb_def greatestP_def)
7.137 +
7.138 +lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
7.139 + by (simp add: isGlb_def isLb_def greatestP_def)
7.140 +
7.141 +lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
7.142 + unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
7.143 +
7.144 +lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
7.145 + by (blast dest!: isGlbD1 setgeD)
7.146 +
7.147 +lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
7.148 + by (simp add: isGlb_def)
7.149 +
7.150 +lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
7.151 + by (simp add: isGlb_def)
7.152 +
7.153 +lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
7.154 + by (simp add: isGlb_def greatestP_def)
7.155 +
7.156 +lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
7.157 + by (simp add: isLb_def setge_def)
7.158 +
7.159 +lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
7.160 + by (simp add: isLb_def)
7.161 +
7.162 +lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
7.163 + by (simp add: isLb_def)
7.164 +
7.165 +lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
7.166 + by (simp add: isLb_def)
7.167 +
7.168 +lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
7.169 + unfolding isGlb_def by (blast intro!: greatestPD3)
7.170 +
7.171 +lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
7.172 + unfolding lbs_def isGlb_def by (rule greatestPD2)
7.173 +
7.174 +lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
7.175 + apply (frule isGlb_isLb)
7.176 + apply (frule_tac x = y in isGlb_isLb)
7.177 + apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
7.178 + done
7.179 +
7.180 +lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
7.181 + by (auto simp: bdd_above_def setle_def)
7.182 +
7.183 +lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
7.184 + by (auto simp: bdd_below_def setge_def)
7.185 +
7.186 +lemma isLub_cSup:
7.187 + "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
7.188 + by (auto simp add: isLub_def setle_def leastP_def isUb_def
7.189 + intro!: setgeI cSup_upper cSup_least)
7.190 +
7.191 +lemma isGlb_cInf:
7.192 + "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
7.193 + by (auto simp add: isGlb_def setge_def greatestP_def isLb_def
7.194 + intro!: setleI cInf_lower cInf_greatest)
7.195 +
7.196 +lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
7.197 + by (metis cSup_least setle_def)
7.198 +
7.199 +lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
7.200 + by (metis cInf_greatest setge_def)
7.201 +
7.202 +lemma cSup_bounds:
7.203 + fixes S :: "'a :: conditionally_complete_lattice set"
7.204 + shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
7.205 + using cSup_least[of S b] cSup_upper2[of _ S a]
7.206 + by (auto simp: bdd_above_setle setge_def setle_def)
7.207 +
7.208 +lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
7.209 + by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
7.210 +
7.211 +lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
7.212 + by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
7.213 +
7.214 +text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*}
7.215 +
7.216 +lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
7.217 + by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
7.218 +
7.219 +lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
7.220 + by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
7.221 +
7.222 +lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
7.223 + by (blast intro: reals_complete Bseq_isUb)
7.224 +
7.225 +lemma isLub_mono_imp_LIMSEQ:
7.226 + fixes X :: "nat \<Rightarrow> real"
7.227 + assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
7.228 + assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
7.229 + shows "X ----> u"
7.230 +proof -
7.231 + have "X ----> (SUP i. X i)"
7.232 + using u[THEN isLubD1] X
7.233 + by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
7.234 + also have "(SUP i. X i) = u"
7.235 + using isLub_cSup[of "range X"] u[THEN isLubD1]
7.236 + by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
7.237 + finally show ?thesis .
7.238 +qed
7.239 +
7.240 +lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
7.241 +
7.242 +lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
7.243 + by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
7.244 +
7.245 +lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
7.246 + by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
7.247 +
7.248 +end
8.1 --- a/src/HOL/Library/RBT_Set.thy Tue Nov 05 09:45:00 2013 +0100
8.2 +++ b/src/HOL/Library/RBT_Set.thy Tue Nov 05 09:45:02 2013 +0100
8.3 @@ -756,7 +756,8 @@
8.4 declare Inf_Set_fold[folded Inf'_def, code]
8.5
8.6 lemma INFI_Set_fold [code]:
8.7 - "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
8.8 + fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
8.9 + shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
8.10 proof -
8.11 have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
8.12 by default (auto simp add: fun_eq_iff ac_simps)
8.13 @@ -796,7 +797,8 @@
8.14 declare Sup_Set_fold[folded Sup'_def, code]
8.15
8.16 lemma SUPR_Set_fold [code]:
8.17 - "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
8.18 + fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
8.19 + shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
8.20 proof -
8.21 have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
8.22 by default (auto simp add: fun_eq_iff ac_simps)
9.1 --- a/src/HOL/Limits.thy Tue Nov 05 09:45:00 2013 +0100
9.2 +++ b/src/HOL/Limits.thy Tue Nov 05 09:45:02 2013 +0100
9.3 @@ -138,6 +138,18 @@
9.4 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
9.5 by (auto simp add: Bseq_def)
9.6
9.7 +lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
9.8 +proof (elim BseqE, intro bdd_aboveI2)
9.9 + fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
9.10 + by (auto elim!: allE[of _ n])
9.11 +qed
9.12 +
9.13 +lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
9.14 +proof (elim BseqE, intro bdd_belowI2)
9.15 + fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
9.16 + by (auto elim!: allE[of _ n])
9.17 +qed
9.18 +
9.19 lemma lemma_NBseq_def:
9.20 "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
9.21 proof safe
9.22 @@ -210,18 +222,6 @@
9.23
9.24 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
9.25
9.26 -lemma Bseq_isUb:
9.27 - "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
9.28 -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
9.29 -
9.30 -text{* Use completeness of reals (supremum property)
9.31 - to show that any bounded sequence has a least upper bound*}
9.32 -
9.33 -lemma Bseq_isLub:
9.34 - "!!(X::nat=>real). Bseq X ==>
9.35 - \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
9.36 -by (blast intro: reals_complete Bseq_isUb)
9.37 -
9.38 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
9.39 by (simp add: Bseq_def)
9.40
9.41 @@ -1358,40 +1358,29 @@
9.42
9.43 text {* A monotone sequence converges to its least upper bound. *}
9.44
9.45 -lemma isLub_mono_imp_LIMSEQ:
9.46 - fixes X :: "nat \<Rightarrow> real"
9.47 - assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
9.48 - assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
9.49 - shows "X ----> u"
9.50 -proof (rule LIMSEQ_I)
9.51 - have 1: "\<forall>n. X n \<le> u"
9.52 - using isLubD2 [OF u] by auto
9.53 - have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
9.54 - using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
9.55 - hence 2: "\<forall>y<u. \<exists>n. y < X n"
9.56 - by (metis not_le)
9.57 - fix r :: real assume "0 < r"
9.58 - hence "u - r < u" by simp
9.59 - hence "\<exists>m. u - r < X m" using 2 by simp
9.60 - then obtain m where "u - r < X m" ..
9.61 - with X have "\<forall>n\<ge>m. u - r < X n"
9.62 - by (fast intro: less_le_trans)
9.63 - hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
9.64 - thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
9.65 - using 1 by (simp add: diff_less_eq add_commute)
9.66 -qed
9.67 +lemma LIMSEQ_incseq_SUP:
9.68 + fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
9.69 + assumes u: "bdd_above (range X)"
9.70 + assumes X: "incseq X"
9.71 + shows "X ----> (SUP i. X i)"
9.72 + by (rule order_tendstoI)
9.73 + (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
9.74
9.75 -text{*A standard proof of the theorem for monotone increasing sequence*}
9.76 -
9.77 -lemma Bseq_mono_convergent:
9.78 - "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
9.79 - by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
9.80 +lemma LIMSEQ_decseq_INF:
9.81 + fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
9.82 + assumes u: "bdd_below (range X)"
9.83 + assumes X: "decseq X"
9.84 + shows "X ----> (INF i. X i)"
9.85 + by (rule order_tendstoI)
9.86 + (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
9.87
9.88 text{*Main monotonicity theorem*}
9.89
9.90 lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
9.91 - by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
9.92 - Bseq_mono_convergent)
9.93 + by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
9.94 +
9.95 +lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
9.96 + by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
9.97
9.98 lemma Cauchy_iff:
9.99 fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
10.1 --- a/src/HOL/Lubs.thy Tue Nov 05 09:45:00 2013 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,103 +0,0 @@
10.4 -(* Title: HOL/Lubs.thy
10.5 - Author: Jacques D. Fleuriot, University of Cambridge
10.6 -*)
10.7 -
10.8 -header {* Definitions of Upper Bounds and Least Upper Bounds *}
10.9 -
10.10 -theory Lubs
10.11 -imports Main
10.12 -begin
10.13 -
10.14 -text {* Thanks to suggestions by James Margetson *}
10.15 -
10.16 -definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70)
10.17 - where "S *<= x = (ALL y: S. y \<le> x)"
10.18 -
10.19 -definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70)
10.20 - where "x <=* S = (ALL y: S. x \<le> y)"
10.21 -
10.22 -definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
10.23 - where "leastP P x = (P x \<and> x <=* Collect P)"
10.24 -
10.25 -definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
10.26 - where "isUb R S x = (S *<= x \<and> x: R)"
10.27 -
10.28 -definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
10.29 - where "isLub R S x = leastP (isUb R S) x"
10.30 -
10.31 -definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
10.32 - where "ubs R S = Collect (isUb R S)"
10.33 -
10.34 -
10.35 -subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
10.36 -
10.37 -lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
10.38 - by (simp add: setle_def)
10.39 -
10.40 -lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
10.41 - by (simp add: setle_def)
10.42 -
10.43 -lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
10.44 - by (simp add: setge_def)
10.45 -
10.46 -lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
10.47 - by (simp add: setge_def)
10.48 -
10.49 -
10.50 -subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
10.51 -
10.52 -lemma leastPD1: "leastP P x \<Longrightarrow> P x"
10.53 - by (simp add: leastP_def)
10.54 -
10.55 -lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
10.56 - by (simp add: leastP_def)
10.57 -
10.58 -lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
10.59 - by (blast dest!: leastPD2 setgeD)
10.60 -
10.61 -lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
10.62 - by (simp add: isLub_def isUb_def leastP_def)
10.63 -
10.64 -lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
10.65 - by (simp add: isLub_def isUb_def leastP_def)
10.66 -
10.67 -lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
10.68 - unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
10.69 -
10.70 -lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
10.71 - by (blast dest!: isLubD1 setleD)
10.72 -
10.73 -lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
10.74 - by (simp add: isLub_def)
10.75 -
10.76 -lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
10.77 - by (simp add: isLub_def)
10.78 -
10.79 -lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
10.80 - by (simp add: isLub_def leastP_def)
10.81 -
10.82 -lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
10.83 - by (simp add: isUb_def setle_def)
10.84 -
10.85 -lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
10.86 - by (simp add: isUb_def)
10.87 -
10.88 -lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
10.89 - by (simp add: isUb_def)
10.90 -
10.91 -lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
10.92 - by (simp add: isUb_def)
10.93 -
10.94 -lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
10.95 - unfolding isLub_def by (blast intro!: leastPD3)
10.96 -
10.97 -lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
10.98 - unfolding ubs_def isLub_def by (rule leastPD2)
10.99 -
10.100 -lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
10.101 - apply (frule isLub_isUb)
10.102 - apply (frule_tac x = y in isLub_isUb)
10.103 - apply (blast intro!: order_antisym dest!: isLub_le_isUb)
10.104 - done
10.105 -
10.106 -end
11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:45:00 2013 +0100
11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:45:02 2013 +0100
11.3 @@ -4506,38 +4506,30 @@
11.4 apply (erule_tac x="x - y" in ballE)
11.5 apply (auto simp add: inner_diff)
11.6 done
11.7 - def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
11.8 + def k \<equiv> "SUP x:t. a \<bullet> x"
11.9 show ?thesis
11.10 apply (rule_tac x="-a" in exI)
11.11 apply (rule_tac x="-(k + b / 2)" in exI)
11.12 - apply rule
11.13 - apply rule
11.14 - defer
11.15 - apply rule
11.16 + apply (intro conjI ballI)
11.17 unfolding inner_minus_left and neg_less_iff_less
11.18 proof -
11.19 - from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
11.20 - apply (erule_tac x=y in ballE)
11.21 - apply (rule setleI)
11.22 - using `y \<in> s`
11.23 - apply auto
11.24 - done
11.25 - then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k"
11.26 + fix x assume "x \<in> t"
11.27 + then have "inner a x - b / 2 < k"
11.28 unfolding k_def
11.29 - apply (rule_tac isLub_cSup)
11.30 - using assms(5)
11.31 - apply auto
11.32 - done
11.33 - fix x
11.34 - assume "x \<in> t"
11.35 - then show "inner a x < (k + b / 2)"
11.36 - using `0<b` and isLubD2[OF k, of "inner a x"] by auto
11.37 + proof (subst less_cSUP_iff)
11.38 + show "t \<noteq> {}" by fact
11.39 + show "bdd_above (op \<bullet> a ` t)"
11.40 + using ab[rule_format, of y] `y \<in> s`
11.41 + by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
11.42 + qed (auto intro!: bexI[of _ x] `0<b`)
11.43 + then show "inner a x < k + b / 2"
11.44 + by auto
11.45 next
11.46 fix x
11.47 assume "x \<in> s"
11.48 then have "k \<le> inner a x - b"
11.49 unfolding k_def
11.50 - apply (rule_tac cSup_least)
11.51 + apply (rule_tac cSUP_least)
11.52 using assms(5)
11.53 using ab[THEN bspec[where x=x]]
11.54 apply auto
11.55 @@ -4626,20 +4618,14 @@
11.56 from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
11.57 obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
11.58 using assms(3-5) by auto
11.59 - then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
11.60 + then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
11.61 by (force simp add: inner_diff)
11.62 - then show ?thesis
11.63 - apply (rule_tac x=a in exI)
11.64 - apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI)
11.65 + then have bdd: "bdd_above ((op \<bullet> a)`s)"
11.66 + using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *])
11.67 + show ?thesis
11.68 using `a\<noteq>0`
11.69 - apply auto
11.70 - apply (rule isLub_cSup[THEN isLubD2])
11.71 - prefer 4
11.72 - apply (rule cSup_least)
11.73 - using assms(3-5)
11.74 - apply (auto simp add: setle_def)
11.75 - apply metis
11.76 - done
11.77 + by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
11.78 + (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *)
11.79 qed
11.80
11.81
12.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:00 2013 +0100
12.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:02 2013 +0100
12.3 @@ -28,10 +28,10 @@
12.4 proof -
12.5 have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
12.6 by arith
12.7 - then show ?thesis
12.8 - using S b cSup_bounds[of S "l - e" "l+e"]
12.9 - unfolding th
12.10 - by (auto simp add: setge_def setle_def)
12.11 + have "bdd_above S"
12.12 + using b by (auto intro!: bdd_aboveI[of _ "l + e"])
12.13 + with S b show ?thesis
12.14 + unfolding th by (auto intro!: cSup_upper2 cSup_least)
12.15 qed
12.16
12.17 lemma cInf_asclose: (* TODO: is this really needed? *)
12.18 @@ -70,39 +70,6 @@
12.19 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
12.20 by (metis cInf_eq_Min Min_le_iff)
12.21
12.22 -lemma Inf: (* rename *)
12.23 - fixes S :: "real set"
12.24 - shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
12.25 - by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
12.26 - intro: cInf_lower cInf_greatest)
12.27 -
12.28 -lemma real_le_inf_subset:
12.29 - assumes "t \<noteq> {}"
12.30 - and "t \<subseteq> s"
12.31 - and "\<exists>b. b <=* s"
12.32 - shows "Inf s \<le> Inf (t::real set)"
12.33 - apply (rule isGlb_le_isLb)
12.34 - apply (rule Inf[OF assms(1)])
12.35 - apply (insert assms)
12.36 - apply (erule exE)
12.37 - apply (rule_tac x = b in exI)
12.38 - apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
12.39 - done
12.40 -
12.41 -lemma real_ge_sup_subset:
12.42 - fixes t :: "real set"
12.43 - assumes "t \<noteq> {}"
12.44 - and "t \<subseteq> s"
12.45 - and "\<exists>b. s *<= b"
12.46 - shows "Sup s \<ge> Sup t"
12.47 - apply (rule isLub_le_isUb)
12.48 - apply (rule isLub_cSup[OF assms(1)])
12.49 - apply (insert assms)
12.50 - apply (erule exE)
12.51 - apply (rule_tac x = b in exI)
12.52 - apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
12.53 - done
12.54 -
12.55 (*declare not_less[simp] not_le[simp]*)
12.56
12.57 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
12.58 @@ -486,24 +453,24 @@
12.59 subsection {* Bounds on intervals where they exist. *}
12.60
12.61 definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
12.62 - where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
12.63 + where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
12.64
12.65 definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
12.66 - where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
12.67 + where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
12.68
12.69 lemma interval_upperbound[simp]:
12.70 "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
12.71 interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
12.72 unfolding interval_upperbound_def euclidean_representation_setsum
12.73 - by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
12.74 - intro!: cSup_unique)
12.75 + by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
12.76 + intro!: cSup_eq)
12.77
12.78 lemma interval_lowerbound[simp]:
12.79 "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
12.80 interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
12.81 unfolding interval_lowerbound_def euclidean_representation_setsum
12.82 - by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
12.83 - intro!: cInf_unique)
12.84 + by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
12.85 + intro!: cInf_eq)
12.86
12.87 lemmas interval_bounds = interval_upperbound interval_lowerbound
12.88
12.89 @@ -6627,7 +6594,7 @@
12.90 lemma interval_bound_sing[simp]:
12.91 "interval_upperbound {a} = a"
12.92 "interval_lowerbound {a} = a"
12.93 - unfolding interval_upperbound_def interval_lowerbound_def
12.94 + unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
12.95 by (auto simp: euclidean_representation)
12.96
12.97 lemma additive_tagged_division_1:
12.98 @@ -11236,37 +11203,26 @@
12.99 lemma bounded_variation_absolutely_integrable_interval:
12.100 fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
12.101 assumes "f integrable_on {a..b}"
12.102 - and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
12.103 + and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
12.104 shows "f absolutely_integrable_on {a..b}"
12.105 proof -
12.106 - let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
12.107 - def i \<equiv> "Sup ?S"
12.108 - have i: "isLub UNIV ?S i"
12.109 - unfolding i_def
12.110 - apply (rule isLub_cSup)
12.111 - apply (rule elementary_interval)
12.112 - defer
12.113 - apply (rule_tac x=B in exI)
12.114 - apply (rule setleI)
12.115 - using assms(2)
12.116 - apply auto
12.117 - done
12.118 + let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
12.119 + have D_1: "?D \<noteq> {}"
12.120 + by (rule elementary_interval[of a b]) auto
12.121 + have D_2: "bdd_above (?f`?D)"
12.122 + by (metis * mem_Collect_eq bdd_aboveI2)
12.123 + note D = D_1 D_2
12.124 + let ?S = "SUP x:?D. ?f x"
12.125 show ?thesis
12.126 apply rule
12.127 apply (rule assms)
12.128 apply rule
12.129 - apply (subst has_integral[of _ i])
12.130 + apply (subst has_integral[of _ ?S])
12.131 proof safe
12.132 case goal1
12.133 - then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
12.134 - {d. d division_of {a..b}}))"
12.135 - using isLub_ubs[OF i,rule_format]
12.136 - unfolding setge_def ubs_def
12.137 - by auto
12.138 - then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
12.139 - unfolding mem_Collect_eq isUb_def setle_def
12.140 - by (simp add: not_le)
12.141 - then guess d .. note d=conjunctD2[OF this]
12.142 + then have "?S - e / 2 < ?S" by simp
12.143 + then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
12.144 + unfolding less_cSUP_iff[OF D] by auto
12.145 note d' = division_ofD[OF this(1)]
12.146
12.147 have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
12.148 @@ -11451,21 +11407,17 @@
12.149 done
12.150 note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
12.151
12.152 - have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
12.153 - sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
12.154 + have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
12.155 + sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
12.156 by arith
12.157 - show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
12.158 + show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
12.159 unfolding real_norm_def
12.160 apply (rule *[rule_format,OF **])
12.161 apply safe
12.162 apply(rule d(2))
12.163 proof -
12.164 - case goal1
12.165 - show ?case unfolding sum_p'
12.166 - apply (rule isLubD2[OF i])
12.167 - using division_of_tagged_division[OF p'']
12.168 - apply auto
12.169 - done
12.170 + case goal1 show ?case
12.171 + by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
12.172 next
12.173 case goal2
12.174 have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
12.175 @@ -11756,18 +11708,13 @@
12.176 and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
12.177 shows "f absolutely_integrable_on UNIV"
12.178 proof (rule absolutely_integrable_onI, fact, rule)
12.179 - let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of (\<Union>d)}"
12.180 - def i \<equiv> "Sup ?S"
12.181 - have i: "isLub UNIV ?S i"
12.182 - unfolding i_def
12.183 - apply (rule isLub_cSup)
12.184 - apply (rule elementary_interval)
12.185 - defer
12.186 - apply (rule_tac x=B in exI)
12.187 - apply (rule setleI)
12.188 - using assms(2)
12.189 - apply auto
12.190 - done
12.191 + let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
12.192 + have D_1: "?D \<noteq> {}"
12.193 + by (rule elementary_interval) auto
12.194 + have D_2: "bdd_above (?f`?D)"
12.195 + by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
12.196 + note D = D_1 D_2
12.197 + let ?S = "SUP d:?D. ?f d"
12.198 have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
12.199 apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
12.200 apply (rule integrable_on_subinterval[OF assms(1)])
12.201 @@ -11776,7 +11723,7 @@
12.202 apply (rule assms(2)[rule_format])
12.203 apply auto
12.204 done
12.205 - show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
12.206 + show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
12.207 apply (subst has_integral_alt')
12.208 apply safe
12.209 proof -
12.210 @@ -11785,16 +11732,11 @@
12.211 using f_int[of a b] by auto
12.212 next
12.213 case goal2
12.214 - have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
12.215 + have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
12.216 proof (rule ccontr)
12.217 assume "\<not> ?thesis"
12.218 - then have "i \<le> i - e"
12.219 - apply -
12.220 - apply (rule isLub_le_isUb[OF i])
12.221 - apply (rule isUbI)
12.222 - unfolding setle_def
12.223 - apply auto
12.224 - done
12.225 + then have "?S \<le> ?S - e"
12.226 + by (intro cSUP_least[OF D(1)]) auto
12.227 then show False
12.228 using goal2 by auto
12.229 qed
12.230 @@ -11811,9 +11753,9 @@
12.231 proof -
12.232 fix a b :: 'n
12.233 assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
12.234 - have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
12.235 + have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
12.236 by arith
12.237 - show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
12.238 + show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
12.239 unfolding real_norm_def
12.240 apply (rule *[rule_format])
12.241 apply safe
12.242 @@ -11865,10 +11807,10 @@
12.243 from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
12.244 from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
12.245 note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
12.246 - have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
12.247 - abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
12.248 + have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
12.249 + abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
12.250 by arith
12.251 - show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
12.252 + show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
12.253 apply (subst if_P)
12.254 apply rule
12.255 proof (rule *[rule_format])
12.256 @@ -11891,18 +11833,12 @@
12.257 apply (subst abs_of_nonneg)
12.258 apply auto
12.259 done
12.260 - show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
12.261 + show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
12.262 + using partial_division_of_tagged_division[of p "{a..b}"] p(1)
12.263 apply (subst setsum_over_tagged_division_lemma[OF p(1)])
12.264 - defer
12.265 - apply (rule isLubD2[OF i])
12.266 - unfolding image_iff
12.267 - apply (rule_tac x="snd ` p" in bexI)
12.268 - unfolding mem_Collect_eq
12.269 - defer
12.270 - apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
12.271 - using p(1)
12.272 - unfolding tagged_division_of_def
12.273 - apply auto
12.274 + apply (simp add: integral_null)
12.275 + apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
12.276 + apply (auto simp: tagged_partial_division_of_def)
12.277 done
12.278 qed
12.279 qed
12.280 @@ -12378,11 +12314,22 @@
12.281 lemma dominated_convergence:
12.282 fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
12.283 assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
12.284 - and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
12.285 + and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
12.286 and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
12.287 shows "g integrable_on s"
12.288 and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
12.289 proof -
12.290 + have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
12.291 + proof (safe intro!: bdd_belowI)
12.292 + fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
12.293 + using assms(3)[rule_format, of x n] by simp
12.294 + qed
12.295 + have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
12.296 + proof (safe intro!: bdd_aboveI)
12.297 + fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
12.298 + using assms(3)[rule_format, of x n] by simp
12.299 + qed
12.300 +
12.301 have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
12.302 ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
12.303 integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
12.304 @@ -12422,66 +12369,32 @@
12.305 fix x
12.306 assume x: "x \<in> s"
12.307 show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
12.308 - apply (rule cInf_ge)
12.309 - unfolding setge_def
12.310 - defer
12.311 - apply rule
12.312 - apply (subst cInf_finite_le_iff)
12.313 - prefer 3
12.314 - apply (rule_tac x=xa in bexI)
12.315 - apply auto
12.316 - done
12.317 - let ?S = "{f j x| j. m \<le> j}"
12.318 - def i \<equiv> "Inf ?S"
12.319 - show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
12.320 + by (rule cInf_superset_mono) auto
12.321 + let ?S = "{f j x| j. m \<le> j}"
12.322 + show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
12.323 proof (rule LIMSEQ_I)
12.324 case goal1
12.325 note r = this
12.326 - have i: "isGlb UNIV ?S i"
12.327 - unfolding i_def
12.328 - apply (rule Inf)
12.329 - defer
12.330 - apply (rule_tac x="- h x - 1" in exI)
12.331 - unfolding setge_def
12.332 - proof safe
12.333 - case goal1
12.334 - then show ?case using assms(3)[rule_format,OF x, of j] by auto
12.335 - qed auto
12.336 -
12.337 - have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
12.338 - proof(rule ccontr)
12.339 - assume "\<not> ?thesis"
12.340 - then have "i \<ge> i + r"
12.341 - apply -
12.342 - apply (rule isGlb_le_isLb[OF i])
12.343 - apply (rule isLbI)
12.344 - unfolding setge_def
12.345 - apply fastforce+
12.346 - done
12.347 - then show False using r by auto
12.348 - qed
12.349 - then guess y .. note y=this[unfolded not_le]
12.350 - from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
12.351 +
12.352 + have "\<exists>y\<in>?S. y < Inf ?S + r"
12.353 + by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
12.354 + then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
12.355 + by blast
12.356
12.357 show ?case
12.358 apply (rule_tac x=N in exI)
12.359 proof safe
12.360 case goal1
12.361 - have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
12.362 + have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
12.363 by arith
12.364 show ?case
12.365 unfolding real_norm_def
12.366 - apply (rule *[rule_format,OF y(2)])
12.367 - unfolding i_def
12.368 - apply (rule real_le_inf_subset)
12.369 - prefer 3
12.370 - apply (rule,rule isGlbD1[OF i])
12.371 - prefer 3
12.372 - apply (subst cInf_finite_le_iff)
12.373 - prefer 3
12.374 - apply (rule_tac x=y in bexI)
12.375 + apply (rule *[rule_format, OF N(1)])
12.376 + apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
12.377 + apply (rule cInf_lower)
12.378 using N goal1
12.379 - apply auto
12.380 + apply auto []
12.381 + apply simp
12.382 done
12.383 qed
12.384 qed
12.385 @@ -12525,65 +12438,27 @@
12.386 fix x
12.387 assume x: "x\<in>s"
12.388 show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
12.389 - apply (rule cSup_le)
12.390 - unfolding setle_def
12.391 - defer
12.392 - apply rule
12.393 - apply (subst cSup_finite_ge_iff)
12.394 - prefer 3
12.395 - apply (rule_tac x=y in bexI)
12.396 - apply auto
12.397 - done
12.398 - let ?S = "{f j x| j. m \<le> j}"
12.399 - def i \<equiv> "Sup ?S"
12.400 - show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
12.401 + by (rule cSup_subset_mono) auto
12.402 + let ?S = "{f j x| j. m \<le> j}"
12.403 + show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
12.404 proof (rule LIMSEQ_I)
12.405 case goal1 note r=this
12.406 - have i: "isLub UNIV ?S i"
12.407 - unfolding i_def
12.408 - apply (rule isLub_cSup)
12.409 - defer
12.410 - apply (rule_tac x="h x" in exI)
12.411 - unfolding setle_def
12.412 - proof safe
12.413 - case goal1
12.414 - then show ?case
12.415 - using assms(3)[rule_format,OF x, of j] by auto
12.416 - qed auto
12.417 -
12.418 - have "\<exists>y\<in>?S. \<not> y \<le> i - r"
12.419 - proof (rule ccontr)
12.420 - assume "\<not> ?thesis"
12.421 - then have "i \<le> i - r"
12.422 - apply -
12.423 - apply (rule isLub_le_isUb[OF i])
12.424 - apply (rule isUbI)
12.425 - unfolding setle_def
12.426 - apply fastforce+
12.427 - done
12.428 - then show False
12.429 - using r by auto
12.430 - qed
12.431 - then guess y .. note y=this[unfolded not_le]
12.432 - from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
12.433 + have "\<exists>y\<in>?S. Sup ?S - r < y"
12.434 + by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
12.435 + then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
12.436 + by blast
12.437
12.438 show ?case
12.439 apply (rule_tac x=N in exI)
12.440 proof safe
12.441 case goal1
12.442 - have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
12.443 + have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
12.444 by arith
12.445 show ?case
12.446 - unfolding real_norm_def
12.447 - apply (rule *[rule_format,OF y(2)])
12.448 - unfolding i_def
12.449 - apply (rule real_ge_sup_subset)
12.450 - prefer 3
12.451 - apply (rule, rule isLubD1[OF i])
12.452 - prefer 3
12.453 - apply (subst cSup_finite_ge_iff)
12.454 - prefer 3
12.455 - apply (rule_tac x = y in bexI)
12.456 + apply simp
12.457 + apply (rule *[rule_format, OF N(1)])
12.458 + apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
12.459 + apply (subst cSup_upper)
12.460 using N goal1
12.461 apply auto
12.462 done
12.463 @@ -12616,17 +12491,7 @@
12.464
12.465 have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
12.466 show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
12.467 - apply -
12.468 - apply (rule real_le_inf_subset)
12.469 - prefer 3
12.470 - unfolding setge_def
12.471 - apply (rule_tac x="- h x" in exI)
12.472 - apply safe
12.473 - apply (rule *)
12.474 - using assms(3)[rule_format,OF x]
12.475 - unfolding real_norm_def abs_le_iff
12.476 - apply auto
12.477 - done
12.478 + by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
12.479
12.480 show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
12.481 proof (rule LIMSEQ_I)
12.482 @@ -12674,16 +12539,7 @@
12.483 assume x: "x \<in> s"
12.484
12.485 show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
12.486 - apply -
12.487 - apply (rule real_ge_sup_subset)
12.488 - prefer 3
12.489 - unfolding setle_def
12.490 - apply (rule_tac x="h x" in exI)
12.491 - apply safe
12.492 - using assms(3)[rule_format,OF x]
12.493 - unfolding real_norm_def abs_le_iff
12.494 - apply auto
12.495 - done
12.496 + by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
12.497 show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
12.498 proof (rule LIMSEQ_I)
12.499 case goal1
12.500 @@ -12712,41 +12568,18 @@
12.501 from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
12.502 from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
12.503 show ?case
12.504 - apply (rule_tac x="N1+N2" in exI, safe)
12.505 - proof -
12.506 + proof (rule_tac x="N1+N2" in exI, safe)
12.507 fix n
12.508 assume n: "n \<ge> N1 + N2"
12.509 have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
12.510 by arith
12.511 show "norm (integral s (f n) - integral s g) < r"
12.512 unfolding real_norm_def
12.513 - apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
12.514 - proof -
12.515 + proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
12.516 show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
12.517 - proof (rule integral_le[OF dec1(1) assms(1)], safe)
12.518 - fix x
12.519 - assume x: "x \<in> s"
12.520 - have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
12.521 - show "Inf {f j x |j. n \<le> j} \<le> f n x"
12.522 - apply (intro cInf_lower bdd_belowI)
12.523 - apply auto []
12.524 - apply (rule *)
12.525 - using assms(3)[rule_format,OF x]
12.526 - unfolding real_norm_def abs_le_iff
12.527 - apply auto
12.528 - done
12.529 - qed
12.530 + by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
12.531 show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
12.532 - proof (rule integral_le[OF assms(1) inc1(1)], safe)
12.533 - fix x
12.534 - assume x: "x \<in> s"
12.535 - show "f n x \<le> Sup {f j x |j. n \<le> j}"
12.536 - apply (rule cSup_upper)
12.537 - using assms(3)[rule_format,OF x]
12.538 - unfolding real_norm_def abs_le_iff
12.539 - apply auto
12.540 - done
12.541 - qed
12.542 + by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
12.543 qed (insert n, auto)
12.544 qed
12.545 qed
13.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Tue Nov 05 09:45:00 2013 +0100
13.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Tue Nov 05 09:45:02 2013 +0100
13.3 @@ -8,7 +8,7 @@
13.4 imports Linear_Algebra
13.5 begin
13.6
13.7 -definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
13.8 +definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
13.9
13.10 lemma norm_bound_generalize:
13.11 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
13.12 @@ -67,25 +67,22 @@
13.13 shows "norm (f x) \<le> onorm f * norm x"
13.14 and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
13.15 proof -
13.16 - let ?S = "{norm (f x) |x. norm x = 1}"
13.17 + let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
13.18 have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
13.19 by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
13.20 then have Se: "?S \<noteq> {}"
13.21 by auto
13.22 - from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
13.23 - unfolding norm_bound_generalize[OF lf, symmetric]
13.24 - by (auto simp add: setle_def)
13.25 - from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
13.26 - show "norm (f x) \<le> onorm f * norm x"
13.27 + from linear_bounded[OF lf] have b: "bdd_above ?S"
13.28 + unfolding norm_bound_generalize[OF lf, symmetric] by auto
13.29 + then show "norm (f x) \<le> onorm f * norm x"
13.30 apply -
13.31 apply (rule spec[where x = x])
13.32 unfolding norm_bound_generalize[OF lf, symmetric]
13.33 - apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
13.34 + apply (auto simp: onorm_def intro!: cSUP_upper)
13.35 done
13.36 show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
13.37 - using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
13.38 unfolding norm_bound_generalize[OF lf, symmetric]
13.39 - by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
13.40 + using Se by (auto simp: onorm_def intro!: cSUP_least b)
13.41 qed
13.42
13.43 lemma onorm_pos_le:
13.44 @@ -107,18 +104,8 @@
13.45 apply arith
13.46 done
13.47
13.48 -lemma onorm_const:
13.49 - "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
13.50 -proof -
13.51 - let ?f = "\<lambda>x::'a. y::'b"
13.52 - have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
13.53 - by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
13.54 - show ?thesis
13.55 - unfolding onorm_def th
13.56 - apply (rule cSup_unique)
13.57 - apply (simp_all add: setle_def)
13.58 - done
13.59 -qed
13.60 +lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
13.61 + using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
13.62
13.63 lemma onorm_pos_lt:
13.64 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:45:00 2013 +0100
14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:45:02 2013 +0100
14.3 @@ -10,7 +10,6 @@
14.4 imports
14.5 Complex_Main
14.6 "~~/src/HOL/Library/Countable_Set"
14.7 - "~~/src/HOL/Library/Glbs"
14.8 "~~/src/HOL/Library/FuncSet"
14.9 Linear_Algebra
14.10 Norm_Arith
14.11 @@ -28,8 +27,6 @@
14.12 lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
14.13 by (rule LIMSEQ_subseq_LIMSEQ)
14.14
14.15 -lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
14.16 -
14.17 lemma countable_PiE:
14.18 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
14.19 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
14.20 @@ -1555,7 +1552,7 @@
14.21 fix y
14.22 assume "y \<in> {x<..} \<inter> I"
14.23 with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
14.24 - by (auto intro: cInf_lower)
14.25 + by (auto intro!: cInf_lower bdd_belowI2)
14.26 with a have "a < f y"
14.27 by (blast intro: less_le_trans)
14.28 }
15.1 --- a/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:00 2013 +0100
15.2 +++ b/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:02 2013 +0100
15.3 @@ -6,7 +6,7 @@
15.4 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
15.5
15.6 theory NSA
15.7 -imports HyperDef
15.8 +imports HyperDef "~~/src/HOL/Library/Lubs_Glbs"
15.9 begin
15.10
15.11 definition
16.1 --- a/src/HOL/Real.thy Tue Nov 05 09:45:00 2013 +0100
16.2 +++ b/src/HOL/Real.thy Tue Nov 05 09:45:02 2013 +0100
16.3 @@ -970,13 +970,6 @@
16.4 qed
16.5 end
16.6
16.7 -text {*
16.8 - \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
16.9 -*}
16.10 -
16.11 -lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
16.12 - by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
16.13 -
16.14
16.15 subsection {* Hiding implementation details *}
16.16
17.1 --- a/src/HOL/Real_Vector_Spaces.thy Tue Nov 05 09:45:00 2013 +0100
17.2 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Nov 05 09:45:02 2013 +0100
17.3 @@ -1425,9 +1425,6 @@
17.4 @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
17.5 *}
17.6
17.7 -lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
17.8 -by (simp add: isUbI setleI)
17.9 -
17.10 lemma increasing_LIMSEQ:
17.11 fixes f :: "nat \<Rightarrow> real"
17.12 assumes inc: "\<And>n. f n \<le> f (Suc n)"
17.13 @@ -1454,40 +1451,33 @@
17.14 then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
17.15
17.16 { fix N x assume N: "\<forall>n\<ge>N. X n < x"
17.17 - have "isUb UNIV S x"
17.18 - proof (rule isUb_UNIV_I)
17.19 fix y::real assume "y \<in> S"
17.20 hence "\<exists>M. \<forall>n\<ge>M. y < X n"
17.21 by (simp add: S_def)
17.22 then obtain M where "\<forall>n\<ge>M. y < X n" ..
17.23 hence "y < X (max M N)" by simp
17.24 also have "\<dots> < x" using N by simp
17.25 - finally show "y \<le> x"
17.26 - by (rule order_less_imp_le)
17.27 - qed }
17.28 + finally have "y \<le> x"
17.29 + by (rule order_less_imp_le) }
17.30 note bound_isUb = this
17.31
17.32 - have "\<exists>u. isLub UNIV S u"
17.33 - proof (rule reals_complete)
17.34 obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
17.35 using X[THEN metric_CauchyD, OF zero_less_one] by auto
17.36 hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
17.37 - show "\<exists>x. x \<in> S"
17.38 - proof
17.39 + have [simp]: "S \<noteq> {}"
17.40 + proof (intro exI ex_in_conv[THEN iffD1])
17.41 from N have "\<forall>n\<ge>N. X N - 1 < X n"
17.42 by (simp add: abs_diff_less_iff dist_real_def)
17.43 thus "X N - 1 \<in> S" by (rule mem_S)
17.44 qed
17.45 - show "\<exists>u. isUb UNIV S u"
17.46 + have [simp]: "bdd_above S"
17.47 proof
17.48 from N have "\<forall>n\<ge>N. X n < X N + 1"
17.49 by (simp add: abs_diff_less_iff dist_real_def)
17.50 - thus "isUb UNIV S (X N + 1)"
17.51 + thus "\<And>s. s \<in> S \<Longrightarrow> s \<le> X N + 1"
17.52 by (rule bound_isUb)
17.53 qed
17.54 - qed
17.55 - then obtain x where x: "isLub UNIV S x" ..
17.56 - have "X ----> x"
17.57 + have "X ----> Sup S"
17.58 proof (rule metric_LIMSEQ_I)
17.59 fix r::real assume "0 < r"
17.60 hence r: "0 < r/2" by simp
17.61 @@ -1499,17 +1489,18 @@
17.62
17.63 from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
17.64 hence "X N - r/2 \<in> S" by (rule mem_S)
17.65 - hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
17.66 + hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
17.67
17.68 from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
17.69 - hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
17.70 - hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
17.71 + from bound_isUb[OF this]
17.72 + have 2: "Sup S \<le> X N + r/2"
17.73 + by (intro cSup_least) simp_all
17.74
17.75 - show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
17.76 + show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r"
17.77 proof (intro exI allI impI)
17.78 fix n assume n: "N \<le> n"
17.79 from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
17.80 - thus "dist (X n) x < r" using 1 2
17.81 + thus "dist (X n) (Sup S) < r" using 1 2
17.82 by (simp add: abs_diff_less_iff dist_real_def)
17.83 qed
17.84 qed
18.1 --- a/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:00 2013 +0100
18.2 +++ b/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:02 2013 +0100
18.3 @@ -1506,7 +1506,6 @@
18.4 instance real :: linorder
18.5 by (intro_classes, rule real_le_linear)
18.6
18.7 -
18.8 lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
18.9 apply (cases x, cases y)
18.10 apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
18.11 @@ -1657,7 +1656,6 @@
18.12 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
18.13 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
18.14
18.15 -
18.16 subsection {* Completeness of Positive Reals *}
18.17
18.18 text {*
18.19 @@ -1759,107 +1757,23 @@
18.20 qed
18.21
18.22 text {*
18.23 - \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
18.24 -*}
18.25 -
18.26 -lemma posreals_complete:
18.27 - assumes positive_S: "\<forall>x \<in> S. 0 < x"
18.28 - and not_empty_S: "\<exists>x. x \<in> S"
18.29 - and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
18.30 - shows "\<exists>t. isLub (UNIV::real set) S t"
18.31 -proof
18.32 - let ?pS = "{w. real_of_preal w \<in> S}"
18.33 -
18.34 - obtain u where "isUb UNIV S u" using upper_bound_Ex ..
18.35 - hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
18.36 -
18.37 - obtain x where x_in_S: "x \<in> S" using not_empty_S ..
18.38 - hence x_gt_zero: "0 < x" using positive_S by simp
18.39 - have "x \<le> u" using sup and x_in_S ..
18.40 - hence "0 < u" using x_gt_zero by arith
18.41 -
18.42 - then obtain pu where u_is_pu: "u = real_of_preal pu"
18.43 - by (auto simp add: real_gt_zero_preal_Ex)
18.44 -
18.45 - have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
18.46 - proof
18.47 - fix pa
18.48 - assume "pa \<in> ?pS"
18.49 - then obtain a where a: "a \<in> S" "a = real_of_preal pa"
18.50 - by simp
18.51 - then have "a \<le> u" using sup by simp
18.52 - with a show "pa \<le> pu"
18.53 - using sup and u_is_pu by (simp add: real_of_preal_le_iff)
18.54 - qed
18.55 -
18.56 - have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
18.57 - proof
18.58 - fix y
18.59 - assume y_in_S: "y \<in> S"
18.60 - hence "0 < y" using positive_S by simp
18.61 - then obtain py where y_is_py: "y = real_of_preal py"
18.62 - by (auto simp add: real_gt_zero_preal_Ex)
18.63 - hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
18.64 - with pS_less_pu have "py \<le> psup ?pS"
18.65 - by (rule preal_psup_le)
18.66 - thus "y \<le> real_of_preal (psup ?pS)"
18.67 - using y_is_py by (simp add: real_of_preal_le_iff)
18.68 - qed
18.69 -
18.70 - moreover {
18.71 - fix x
18.72 - assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
18.73 - have "real_of_preal (psup ?pS) \<le> x"
18.74 - proof -
18.75 - obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
18.76 - hence s_pos: "0 < s" using positive_S by simp
18.77 -
18.78 - hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
18.79 - then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
18.80 - hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
18.81 -
18.82 - from x_ub_S have "s \<le> x" using s_in_S ..
18.83 - hence "0 < x" using s_pos by simp
18.84 - hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
18.85 - then obtain "px" where x_is_px: "x = real_of_preal px" ..
18.86 -
18.87 - have "\<forall>pe \<in> ?pS. pe \<le> px"
18.88 - proof
18.89 - fix pe
18.90 - assume "pe \<in> ?pS"
18.91 - hence "real_of_preal pe \<in> S" by simp
18.92 - hence "real_of_preal pe \<le> x" using x_ub_S by simp
18.93 - thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
18.94 - qed
18.95 -
18.96 - moreover have "?pS \<noteq> {}" using ps_in_pS by auto
18.97 - ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
18.98 - thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
18.99 - qed
18.100 - }
18.101 - ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
18.102 - by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
18.103 -qed
18.104 -
18.105 -text {*
18.106 - \medskip reals Completeness (again!)
18.107 + \medskip Completeness
18.108 *}
18.109
18.110 lemma reals_complete:
18.111 + fixes S :: "real set"
18.112 assumes notempty_S: "\<exists>X. X \<in> S"
18.113 - and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
18.114 - shows "\<exists>t. isLub (UNIV :: real set) S t"
18.115 + and exists_Ub: "bdd_above S"
18.116 + shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)"
18.117 proof -
18.118 obtain X where X_in_S: "X \<in> S" using notempty_S ..
18.119 - obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
18.120 - using exists_Ub ..
18.121 + obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y"
18.122 + using exists_Ub by (auto simp: bdd_above_def)
18.123 let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
18.124
18.125 {
18.126 fix x
18.127 - assume "isUb (UNIV::real set) S x"
18.128 - hence S_le_x: "\<forall> y \<in> S. y <= x"
18.129 - by (simp add: isUb_def setle_def)
18.130 + assume S_le_x: "\<forall>s\<in>S. s \<le> x"
18.131 {
18.132 fix s
18.133 assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
18.134 @@ -1868,86 +1782,74 @@
18.135 then have "x1 \<le> x" using S_le_x by simp
18.136 with x1 have "s \<le> x + - X + 1" by arith
18.137 }
18.138 - then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
18.139 - by (auto simp add: isUb_def setle_def)
18.140 + then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
18.141 + by auto
18.142 } note S_Ub_is_SHIFT_Ub = this
18.143
18.144 - hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
18.145 - hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
18.146 + have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub)
18.147 + have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2"
18.148 + proof
18.149 + fix s assume "s\<in>?SHIFT"
18.150 + with * have "s \<le> Y + (-X) + 1" by simp
18.151 + also have "\<dots> < Y + (-X) + 2" by simp
18.152 + finally show "s < Y + (-X) + 2" .
18.153 + qed
18.154 moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
18.155 moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
18.156 using X_in_S and Y_isUb by auto
18.157 - ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
18.158 - using posreals_complete [of ?SHIFT] by blast
18.159 + ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)"
18.160 + using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast
18.161
18.162 show ?thesis
18.163 proof
18.164 - show "isLub UNIV S (t + X + (-1))"
18.165 - proof (rule isLubI2)
18.166 - {
18.167 - fix x
18.168 - assume "isUb (UNIV::real set) S x"
18.169 - hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
18.170 - using S_Ub_is_SHIFT_Ub by simp
18.171 - hence "t \<le> (x + (-X) + 1)"
18.172 - using t_is_Lub by (simp add: isLub_le_isUb)
18.173 - hence "t + X + -1 \<le> x" by arith
18.174 - }
18.175 - then show "(t + X + -1) <=* Collect (isUb UNIV S)"
18.176 - by (simp add: setgeI)
18.177 + show "(\<forall>s\<in>S. s \<le> (t + X + (-1))) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> (t + X + (-1)) \<le> y)"
18.178 + proof safe
18.179 + fix x
18.180 + assume "\<forall>s\<in>S. s \<le> x"
18.181 + hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
18.182 + using S_Ub_is_SHIFT_Ub by simp
18.183 + then have "\<not> x + (-X) + 1 < t"
18.184 + by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less)
18.185 + thus "t + X + -1 \<le> x" by arith
18.186 next
18.187 - show "isUb UNIV S (t + X + -1)"
18.188 - proof -
18.189 - {
18.190 - fix y
18.191 - assume y_in_S: "y \<in> S"
18.192 - have "y \<le> t + X + -1"
18.193 - proof -
18.194 - obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
18.195 - hence "\<exists> x \<in> S. u = x + - X + 1" by simp
18.196 - then obtain "x" where x_and_u: "u = x + - X + 1" ..
18.197 - have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
18.198 + fix y
18.199 + assume y_in_S: "y \<in> S"
18.200 + obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
18.201 + hence "\<exists> x \<in> S. u = x + - X + 1" by simp
18.202 + then obtain "x" where x_and_u: "u = x + - X + 1" ..
18.203 + have u_le_t: "u \<le> t"
18.204 + proof (rule dense_le)
18.205 + fix x assume "x < u" then have "x < t"
18.206 + using u_in_shift t_is_Lub by auto
18.207 + then show "x \<le> t" by simp
18.208 + qed
18.209
18.210 - show ?thesis
18.211 - proof cases
18.212 - assume "y \<le> x"
18.213 - moreover have "x = u + X + - 1" using x_and_u by arith
18.214 - moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
18.215 - ultimately show "y \<le> t + X + -1" by arith
18.216 - next
18.217 - assume "~(y \<le> x)"
18.218 - hence x_less_y: "x < y" by arith
18.219 + show "y \<le> t + X + -1"
18.220 + proof cases
18.221 + assume "y \<le> x"
18.222 + moreover have "x = u + X + - 1" using x_and_u by arith
18.223 + moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
18.224 + ultimately show "y \<le> t + X + -1" by arith
18.225 + next
18.226 + assume "~(y \<le> x)"
18.227 + hence x_less_y: "x < y" by arith
18.228
18.229 - have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
18.230 - hence "0 < x + (-X) + 1" by simp
18.231 - hence "0 < y + (-X) + 1" using x_less_y by arith
18.232 - hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
18.233 - hence "y + (-X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2)
18.234 - thus ?thesis by simp
18.235 - qed
18.236 - qed
18.237 - }
18.238 - then show ?thesis by (simp add: isUb_def setle_def)
18.239 + have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
18.240 + hence "0 < x + (-X) + 1" by simp
18.241 + hence "0 < y + (-X) + 1" using x_less_y by arith
18.242 + hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
18.243 + have "y + (-X) + 1 \<le> t"
18.244 + proof (rule dense_le)
18.245 + fix x assume "x < y + (-X) + 1" then have "x < t"
18.246 + using * t_is_Lub by auto
18.247 + then show "x \<le> t" by simp
18.248 + qed
18.249 + thus ?thesis by simp
18.250 qed
18.251 qed
18.252 qed
18.253 qed
18.254
18.255 -text{*A version of the same theorem without all those predicates!*}
18.256 -lemma reals_complete2:
18.257 - fixes S :: "(real set)"
18.258 - assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
18.259 - shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) &
18.260 - (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
18.261 -proof -
18.262 - have "\<exists>x. isLub UNIV S x"
18.263 - by (rule reals_complete)
18.264 - (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
18.265 - thus ?thesis
18.266 - by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
18.267 -qed
18.268 -
18.269 -
18.270 subsection {* The Archimedean Property of the Reals *}
18.271
18.272 theorem reals_Archimedean:
18.273 @@ -1969,34 +1871,30 @@
18.274 by (rule mult_right_mono)
18.275 thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
18.276 qed
18.277 - hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
18.278 - by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
18.279 - hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
18.280 - by (simp add: isUbI)
18.281 - hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
18.282 - moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
18.283 - ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
18.284 - by (simp add: reals_complete)
18.285 - then obtain "t" where
18.286 - t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
18.287 + hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}"
18.288 + by (auto intro!: bdd_aboveI[of _ 1])
18.289 + have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
18.290 + obtain t where
18.291 + upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and
18.292 + least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y"
18.293 + using reals_complete[OF 1 2] by auto
18.294
18.295 - have "\<forall>n::nat. x * of_nat n \<le> t + - x"
18.296 - proof
18.297 - fix n
18.298 - from t_is_Lub have "x * of_nat (Suc n) \<le> t"
18.299 - by (simp add: isLubD2)
18.300 - hence "x * (of_nat n) + x \<le> t"
18.301 - by (simp add: distrib_left)
18.302 - thus "x * (of_nat n) \<le> t + - x" by arith
18.303 +
18.304 + have "t \<le> t + - x"
18.305 + proof (rule least)
18.306 + fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}"
18.307 + have "\<forall>n::nat. x * of_nat n \<le> t + - x"
18.308 + proof
18.309 + fix n
18.310 + have "x * of_nat (Suc n) \<le> t"
18.311 + by (simp add: upper)
18.312 + hence "x * (of_nat n) + x \<le> t"
18.313 + by (simp add: distrib_left)
18.314 + thus "x * (of_nat n) \<le> t + - x" by arith
18.315 + qed hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
18.316 + with a show "a \<le> t + - x"
18.317 + by auto
18.318 qed
18.319 -
18.320 - hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
18.321 - hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= (t + - x)"
18.322 - by (auto simp add: setle_def)
18.323 - hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
18.324 - by (simp add: isUbI)
18.325 - hence "t \<le> t + - x"
18.326 - using t_is_Lub by (simp add: isLub_le_isUb)
18.327 thus False using x_pos by arith
18.328 qed
18.329