--- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:02 2013 +0100
@@ -7,7 +7,7 @@
header {* Conditionally-complete Lattices *}
theory Conditionally_Complete_Lattices
-imports Main Lubs
+imports Main
begin
lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
@@ -28,6 +28,12 @@
lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
by (auto simp: bdd_below_def)
+lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
+ by force
+
+lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
+ by force
+
lemma bdd_above_empty [simp, intro]: "bdd_above {}"
unfolding bdd_above_def by auto
@@ -298,6 +304,12 @@
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)"
by (metis cSUP_least cSUP_upper assms order_trans)
+lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
+ by (metis cINF_lower less_le_trans)
+
+lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
+ by (metis cSUP_upper le_less_trans)
+
lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
by (metis INF_def cInf_insert assms empty_is_image image_insert)
@@ -347,11 +359,6 @@
instance complete_lattice \<subseteq> conditionally_complete_lattice
by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
-lemma isLub_cSup:
- "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
- by (auto simp add: isLub_def setle_def leastP_def isUb_def
- intro!: setgeI cSup_upper cSup_least)
-
lemma cSup_eq:
fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
@@ -370,12 +377,6 @@
assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
qed (intro cInf_eq_non_empty assms)
-lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
- by (metis cSup_least setle_def)
-
-lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
- by (metis cInf_greatest setge_def)
-
class conditionally_complete_linorder = conditionally_complete_lattice + linorder
begin
@@ -386,6 +387,12 @@
lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
+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)"
+ unfolding INF_def using cInf_less_iff[of "f`A"] by auto
+
+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)"
+ unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
+
lemma less_cSupE:
assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
by (metis cSup_least assms not_le that)
@@ -437,27 +444,6 @@
lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-lemma cSup_bounds:
- fixes S :: "'a :: conditionally_complete_lattice set"
- assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> Sup S \<and> Sup S \<le> b"
-proof-
- from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
- hence b: "Sup S \<le> b" using u
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- from Se obtain y where y: "y \<in> S" by blast
- from lub l have "a \<le> Sup S"
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- (metis le_iff_sup le_sup_iff y)
- with b show ?thesis by blast
-qed
-
-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"
- by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
-
-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"
- by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
-
lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
by (auto intro!: cSup_eq_non_empty intro: dense_le)
--- a/src/HOL/Hahn_Banach/Bounds.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Hahn_Banach/Bounds.thy Tue Nov 05 09:45:02 2013 +0100
@@ -57,25 +57,7 @@
finally show ?thesis .
qed
-lemma lub_compat: "lub A x = isLub UNIV A x"
-proof -
- have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
- by (rule ext) (simp only: isUb_def)
- then show ?thesis
- by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
-qed
-
-lemma real_complete:
- fixes A :: "real set"
- assumes nonempty: "\<exists>a. a \<in> A"
- and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
- shows "\<exists>x. lub A x"
-proof -
- from ex_upper have "\<exists>y. isUb UNIV A y"
- unfolding isUb_def setle_def by blast
- with nonempty have "\<exists>x. isLub UNIV A x"
- by (rule reals_complete)
- then show ?thesis by (simp only: lub_compat)
-qed
+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"
+ by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def)
end
--- a/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:02 2013 +0100
@@ -131,17 +131,15 @@
-- "A denotes the set of all left-most points of all the intervals ..."
moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
- ultimately have "\<exists>x. x\<in>A"
+ ultimately have "A \<noteq> {}"
proof -
have "(0::nat) \<in> \<nat>" by simp
- moreover have "?g 0 = ?g 0" by simp
- ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
- with Adef have "?g 0 \<in> A" by simp
- thus ?thesis ..
+ with Adef show ?thesis
+ by blast
qed
-- "Now show that A is bounded above ..."
- moreover have "\<exists>y. isUb (UNIV::real set) A y"
+ moreover have "bdd_above A"
proof -
{
fix n
@@ -177,18 +175,11 @@
obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
- with Adef have "\<forall>y\<in>A. y\<le>b" by auto
- hence "A *<= b" by (unfold setle_def)
- moreover have "b \<in> (UNIV::real set)" by simp
- ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
- hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
- thus ?thesis by auto
+ with Adef show "bdd_above A" by auto
qed
- -- "by the Axiom Of Completeness, A has a least upper bound ..."
- ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
-- "denote this least upper bound as t ..."
- then obtain t where tdef: "isLub UNIV A t" ..
+ def tdef: t == "Sup A"
-- "and finally show that this least upper bound is in all the intervals..."
have "\<forall>n. t \<in> f n"
@@ -229,82 +220,76 @@
with Adef have "(?g n) \<in> A" by auto
ultimately show ?thesis by simp
qed
- with tdef show "a \<le> t" by (rule isLubD2)
+ with `bdd_above A` show "a \<le> t"
+ unfolding tdef by (intro cSup_upper)
qed
moreover have "t \<le> b"
- proof -
- have "isUb UNIV A b"
- proof -
- {
- from alb int have
- ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
-
- have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
- proof (rule allI, induct_tac m)
- show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
- next
- fix m n
- assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
- {
- fix p
- from pp have "f (p + n) \<subseteq> f p" by simp
- moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
- hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
- ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
- }
- thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
- qed
- have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
- proof ((rule allI)+, rule impI)
- fix \<alpha>::nat and \<beta>::nat
- assume "\<beta> \<le> \<alpha>"
- hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
- then obtain k where "\<alpha> = \<beta> + k" ..
- moreover
- from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
- ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
- qed
-
- fix m
+ unfolding tdef
+ proof (rule cSup_least)
+ {
+ from alb int have
+ ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
+
+ have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
+ proof (rule allI, induct_tac m)
+ show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
+ next
+ fix m n
+ assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
{
- assume "m \<ge> n"
- with subsetm have "f m \<subseteq> f n" by simp
- with ain have "\<forall>x\<in>f m. x \<le> b" by auto
- moreover
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
- ultimately have "?g m \<le> b" by auto
+ fix p
+ from pp have "f (p + n) \<subseteq> f p" by simp
+ moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
+ hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
+ ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
}
+ thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
+ qed
+ have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
+ proof ((rule allI)+, rule impI)
+ fix \<alpha>::nat and \<beta>::nat
+ assume "\<beta> \<le> \<alpha>"
+ hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
+ then obtain k where "\<alpha> = \<beta> + k" ..
+ moreover
+ from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
+ ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
+ qed
+
+ fix m
+ {
+ assume "m \<ge> n"
+ with subsetm have "f m \<subseteq> f n" by simp
+ with ain have "\<forall>x\<in>f m. x \<le> b" by auto
moreover
- {
- assume "\<not>(m \<ge> n)"
- hence "m < n" by simp
- with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
- from closed obtain ma and mb where
- "f m = closed_int ma mb \<and> ma \<le> mb" by blast
- hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
- from one alb sub fm int have "ma \<le> b" using closed_subset by blast
- moreover have "(?g m) = ma"
- proof -
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
- moreover from one have
- "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
- by (rule closed_int_least)
- with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
- ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
- thus "?g m = ma" by auto
- qed
- ultimately have "?g m \<le> b" by simp
- }
- ultimately have "?g m \<le> b" by (rule case_split)
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
+ ultimately have "?g m \<le> b" by auto
}
- with Adef have "\<forall>y\<in>A. y\<le>b" by auto
- hence "A *<= b" by (unfold setle_def)
- moreover have "b \<in> (UNIV::real set)" by simp
- ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
- thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
- qed
- with tdef show "t \<le> b" by (rule isLub_le_isUb)
- qed
+ moreover
+ {
+ assume "\<not>(m \<ge> n)"
+ hence "m < n" by simp
+ with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
+ from closed obtain ma and mb where
+ "f m = closed_int ma mb \<and> ma \<le> mb" by blast
+ hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
+ from one alb sub fm int have "ma \<le> b" using closed_subset by blast
+ moreover have "(?g m) = ma"
+ proof -
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
+ moreover from one have
+ "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
+ by (rule closed_int_least)
+ with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
+ ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
+ thus "?g m = ma" by auto
+ qed
+ ultimately have "?g m \<le> b" by simp
+ }
+ ultimately have "?g m \<le> b" by (rule case_split)
+ }
+ with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
+ qed fact
ultimately have "t \<in> closed_int a b" by (rule closed_mem)
with int show "t \<in> f n" by simp
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:02 2013 +0100
@@ -451,7 +451,7 @@
definition
dist_fps_def: "dist (a::'a fps) b =
- (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
+ (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
by (simp add: dist_fps_def)
@@ -467,34 +467,6 @@
end
-lemma fps_nonzero_least_unique:
- assumes a0: "a \<noteq> 0"
- shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n"
-proof -
- from fps_nonzero_nth_minimal [of a] a0
- obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast
- then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n"
- by (auto simp add: leastP_def setge_def not_le [symmetric])
- moreover
- {
- fix m
- assume "leastP (\<lambda>n. a $ n \<noteq> 0) m"
- then have "m = n" using ln
- apply (auto simp add: leastP_def setge_def)
- apply (erule allE[where x=n])
- apply (erule allE[where x=m])
- apply simp
- done
- }
- ultimately show ?thesis by blast
-qed
-
-lemma fps_eq_least_unique:
- assumes "(a::('a::ab_group_add) fps) \<noteq> b"
- shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
- using fps_nonzero_least_unique[of "a - b"] assms
- by auto
-
instantiation fps :: (comm_ring_1) metric_space
begin
@@ -540,31 +512,15 @@
moreover
{
assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
- let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
- from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac]
- fps_eq_least_unique[OF bc]
- obtain nab nac nbc where nab: "leastP (?P a b) nab"
- and nac: "leastP (?P a c) nac"
- and nbc: "leastP (?P b c) nbc" by blast
- from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab"
- by (auto simp add: leastP_def setge_def)
- from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac"
- by (auto simp add: leastP_def setge_def)
- from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc"
- by (auto simp add: leastP_def setge_def)
-
- have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
- by (simp add: fps_eq_iff)
- from ab ac bc nab nac nbc
- have dab: "dist a b = inverse (2 ^ nab)"
- and dac: "dist a c = inverse (2 ^ nac)"
- and dbc: "dist b c = inverse (2 ^ nbc)"
- unfolding th0
- apply (simp_all add: dist_fps_def)
- apply (erule the1_equality[OF fps_eq_least_unique[OF ab]])
- apply (erule the1_equality[OF fps_eq_least_unique[OF ac]])
- apply (erule the1_equality[OF fps_eq_least_unique[OF bc]])
- done
+ def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
+ then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
+ by (auto dest: not_less_Least)
+
+ from ab ac bc
+ have dab: "dist a b = inverse (2 ^ n a b)"
+ and dac: "dist a c = inverse (2 ^ n a c)"
+ and dbc: "dist b c = inverse (2 ^ n b c)"
+ by (simp_all add: dist_fps_def n_def fps_eq_iff)
from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
unfolding th by simp_all
from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
@@ -575,11 +531,13 @@
assume h: "dist a b > dist a c + dist b c"
then have gt: "dist a b > dist a c" "dist a b > dist b c"
using pos by auto
- from gt have gtn: "nab < nbc" "nab < nac"
+ from gt have gtn: "n a b < n b c" "n a b < n a c"
unfolding dab dbc dac by (auto simp add: th1)
- from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)]
- have "a $ nab = b $ nab" by simp
- with nab'(2) have False by simp
+ from n'[OF gtn(2)] n'(1)[OF gtn(1)]
+ have "a $ n a b = b $ n a b" by simp
+ moreover have "a $ n a b \<noteq> b $ n a b"
+ unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff)
+ ultimately have False by contradiction
}
then have "dist a b \<le> dist a c + dist b c"
by (auto simp add: not_le[symmetric])
@@ -649,17 +607,12 @@
moreover
{
assume neq: "?s n \<noteq> a"
- from fps_eq_least_unique[OF neq]
- obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast
- have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
- by (simp add: fps_eq_iff)
+ def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i"
from neq have dth: "dist (?s n) a = (1/2)^k"
- unfolding th0 dist_fps_def
- unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k]
- by (auto simp add: inverse_eq_divide power_divide)
-
- from k have kn: "k > n"
- by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
+ by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
+
+ from neq have kn: "k > n"
+ by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
then have "dist (?s n) a < (1/2)^n" unfolding dth
by (auto intro: power_strict_decreasing)
also have "\<dots> <= (1/2)^n0" using nn0
@@ -3797,20 +3750,14 @@
assumes "dist f g < inverse (2 ^ i)"
and"j \<le> i"
shows "f $ j = g $ j"
-proof (cases "f = g")
- case False
- hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
- with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+proof (rule ccontr)
+ assume "f $ j \<noteq> g $ j"
+ then have "\<exists>n. f $ n \<noteq> g $ n" by auto
+ with assms have "i < (LEAST n. f $ n \<noteq> g $ n)"
by (simp add: split_if_asm dist_fps_def)
- moreover
- from fps_eq_least_unique[OF `f \<noteq> g`]
- 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
- moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
- by (auto simp add: leastP_def setge_def)
- ultimately show ?thesis using `j \<le> i` by simp
-next
- case True
- then show ?thesis by simp
+ also have "\<dots> \<le> j"
+ using `f $ j \<noteq> g $ j` by (auto intro: Least_le)
+ finally show False using `j \<le> i` by simp
qed
lemma nth_equal_imp_dist_less:
@@ -3819,18 +3766,13 @@
proof (cases "f = g")
case False
hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
- with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
+ with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))"
by (simp add: split_if_asm dist_fps_def)
moreover
- from fps_eq_least_unique[OF `f \<noteq> g`]
- obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
- with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
- by (metis (full_types) leastPD1 not_le)
+ from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)"
+ by (metis (mono_tags) LeastI not_less)
ultimately show ?thesis by simp
-next
- case True
- then show ?thesis by simp
-qed
+qed simp
lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 05 09:45:02 2013 +0100
@@ -156,28 +156,11 @@
text{* An alternative useful formulation of completeness of the reals *}
lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
-proof-
- from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y" by blast
- from ex have thx:"\<exists>x. x \<in> Collect P" by blast
- from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
- by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
- from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
- by blast
- from Y[OF x] have xY: "x < Y" .
- 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)
- from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
- apply (clarsimp, atomize (full)) by auto
- from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
- {fix y
- {fix z assume z: "P z" "y < z"
- from L' z have "y < L" by auto }
- moreover
- {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
- hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
- from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
- with yL(1) have False by arith}
- ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
- thus ?thesis by blast
+proof
+ from bz have "bdd_above (Collect P)"
+ by (force intro: less_imp_le)
+ then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
+ using ex bz by (subst less_cSup_iff) auto
qed
subsection {* Fundamental theorem of algebra *}
--- a/src/HOL/Library/Glbs.thy Tue Nov 05 09:45:00 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Author: Amine Chaieb, University of Cambridge *)
-
-header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
-
-theory Glbs
-imports Lubs
-begin
-
-definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "greatestP P x = (P x \<and> Collect P *<= x)"
-
-definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "isLb R S x = (x <=* S \<and> x: R)"
-
-definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "isGlb R S x = greatestP (isLb R S) x"
-
-definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
- where "lbs R S = Collect (isLb R S)"
-
-
-subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
- and @{term isGlb} *}
-
-lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
- by (simp add: greatestP_def)
-
-lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
- by (simp add: greatestP_def)
-
-lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
- by (blast dest!: greatestPD2 setleD)
-
-lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
- by (simp add: isGlb_def isLb_def greatestP_def)
-
-lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
- by (simp add: isGlb_def isLb_def greatestP_def)
-
-lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
- unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
-
-lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
- by (blast dest!: isGlbD1 setgeD)
-
-lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
- by (simp add: isGlb_def)
-
-lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
- by (simp add: isGlb_def)
-
-lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
- by (simp add: isGlb_def greatestP_def)
-
-lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
- by (simp add: isLb_def setge_def)
-
-lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
- by (simp add: isLb_def)
-
-lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
- by (simp add: isLb_def)
-
-lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
- by (simp add: isLb_def)
-
-lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
- unfolding isGlb_def by (blast intro!: greatestPD3)
-
-lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
- unfolding lbs_def isGlb_def by (rule greatestPD2)
-
-lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
- apply (frule isGlb_isLb)
- apply (frule_tac x = y in isGlb_isLb)
- apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
- done
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Lubs_Glbs.thy Tue Nov 05 09:45:02 2013 +0100
@@ -0,0 +1,245 @@
+(* Title: HOL/Library/Lubs_Glbs.thy
+ Author: Jacques D. Fleuriot, University of Cambridge
+ Author: Amine Chaieb, University of Cambridge *)
+
+header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
+
+theory Lubs_Glbs
+imports Complex_Main
+begin
+
+text {* Thanks to suggestions by James Margetson *}
+
+definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70)
+ where "S *<= x = (ALL y: S. y \<le> x)"
+
+definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70)
+ where "x <=* S = (ALL y: S. x \<le> y)"
+
+
+subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
+
+lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
+ by (simp add: setle_def)
+
+lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
+ by (simp add: setle_def)
+
+lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
+ by (simp add: setge_def)
+
+lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
+ by (simp add: setge_def)
+
+
+definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "leastP P x = (P x \<and> x <=* Collect P)"
+
+definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "isUb R S x = (S *<= x \<and> x: R)"
+
+definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "isLub R S x = leastP (isUb R S) x"
+
+definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+ where "ubs R S = Collect (isUb R S)"
+
+
+subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
+
+lemma leastPD1: "leastP P x \<Longrightarrow> P x"
+ by (simp add: leastP_def)
+
+lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
+ by (simp add: leastP_def)
+
+lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
+ by (blast dest!: leastPD2 setgeD)
+
+lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
+ by (simp add: isLub_def isUb_def leastP_def)
+
+lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
+ by (simp add: isLub_def isUb_def leastP_def)
+
+lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
+ unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
+
+lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+ by (blast dest!: isLubD1 setleD)
+
+lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
+ by (simp add: isLub_def)
+
+lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
+ by (simp add: isLub_def)
+
+lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
+ by (simp add: isLub_def leastP_def)
+
+lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+ by (simp add: isUb_def setle_def)
+
+lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
+ by (simp add: isUb_def)
+
+lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
+ by (simp add: isUb_def)
+
+lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
+ by (simp add: isUb_def)
+
+lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
+ unfolding isLub_def by (blast intro!: leastPD3)
+
+lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
+ unfolding ubs_def isLub_def by (rule leastPD2)
+
+lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
+ apply (frule isLub_isUb)
+ apply (frule_tac x = y in isLub_isUb)
+ apply (blast intro!: order_antisym dest!: isLub_le_isUb)
+ done
+
+lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
+ by (simp add: isUbI setleI)
+
+
+definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "greatestP P x = (P x \<and> Collect P *<= x)"
+
+definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "isLb R S x = (x <=* S \<and> x: R)"
+
+definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+ where "isGlb R S x = greatestP (isLb R S) x"
+
+definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+ where "lbs R S = Collect (isLb R S)"
+
+
+subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *}
+
+lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
+ by (simp add: greatestP_def)
+
+lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
+ by (simp add: greatestP_def)
+
+lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
+ by (blast dest!: greatestPD2 setleD)
+
+lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
+ by (simp add: isGlb_def isLb_def greatestP_def)
+
+lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
+ by (simp add: isGlb_def isLb_def greatestP_def)
+
+lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
+ unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
+
+lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+ by (blast dest!: isGlbD1 setgeD)
+
+lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
+ by (simp add: isGlb_def)
+
+lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
+ by (simp add: isGlb_def)
+
+lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
+ by (simp add: isGlb_def greatestP_def)
+
+lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+ by (simp add: isLb_def setge_def)
+
+lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
+ by (simp add: isLb_def)
+
+lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
+ by (simp add: isLb_def)
+
+lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
+ by (simp add: isLb_def)
+
+lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
+ unfolding isGlb_def by (blast intro!: greatestPD3)
+
+lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
+ unfolding lbs_def isGlb_def by (rule greatestPD2)
+
+lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
+ apply (frule isGlb_isLb)
+ apply (frule_tac x = y in isGlb_isLb)
+ apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
+ done
+
+lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
+ by (auto simp: bdd_above_def setle_def)
+
+lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
+ by (auto simp: bdd_below_def setge_def)
+
+lemma isLub_cSup:
+ "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+ by (auto simp add: isLub_def setle_def leastP_def isUb_def
+ intro!: setgeI cSup_upper cSup_least)
+
+lemma isGlb_cInf:
+ "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
+ by (auto simp add: isGlb_def setge_def greatestP_def isLb_def
+ intro!: setleI cInf_lower cInf_greatest)
+
+lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+ by (metis cSup_least setle_def)
+
+lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+ by (metis cInf_greatest setge_def)
+
+lemma cSup_bounds:
+ fixes S :: "'a :: conditionally_complete_lattice set"
+ shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
+ using cSup_least[of S b] cSup_upper2[of _ S a]
+ by (auto simp: bdd_above_setle setge_def setle_def)
+
+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"
+ by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
+
+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"
+ by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
+
+text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*}
+
+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"
+ by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
+
+lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
+ by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
+
+lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
+ by (blast intro: reals_complete Bseq_isUb)
+
+lemma isLub_mono_imp_LIMSEQ:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+ assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+ shows "X ----> u"
+proof -
+ have "X ----> (SUP i. X i)"
+ using u[THEN isLubD1] X
+ by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
+ also have "(SUP i. X i) = u"
+ using isLub_cSup[of "range X"] u[THEN isLubD1]
+ by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
+ finally show ?thesis .
+qed
+
+lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
+
+lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
+ by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
+
+lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
+ by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
+
+end
--- a/src/HOL/Library/RBT_Set.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue Nov 05 09:45:02 2013 +0100
@@ -756,7 +756,8 @@
declare Inf_Set_fold[folded Inf'_def, code]
lemma INFI_Set_fold [code]:
- "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
+ fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
+ shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
proof -
have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
by default (auto simp add: fun_eq_iff ac_simps)
@@ -796,7 +797,8 @@
declare Sup_Set_fold[folded Sup'_def, code]
lemma SUPR_Set_fold [code]:
- "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
+ fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
+ shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
proof -
have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
by default (auto simp add: fun_eq_iff ac_simps)
--- a/src/HOL/Limits.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Limits.thy Tue Nov 05 09:45:02 2013 +0100
@@ -138,6 +138,18 @@
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
by (auto simp add: Bseq_def)
+lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
+proof (elim BseqE, intro bdd_aboveI2)
+ fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
+ by (auto elim!: allE[of _ n])
+qed
+
+lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
+proof (elim BseqE, intro bdd_belowI2)
+ fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
+ by (auto elim!: allE[of _ n])
+qed
+
lemma lemma_NBseq_def:
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
proof safe
@@ -210,18 +222,6 @@
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
-lemma Bseq_isUb:
- "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
-
-text{* Use completeness of reals (supremum property)
- to show that any bounded sequence has a least upper bound*}
-
-lemma Bseq_isLub:
- "!!(X::nat=>real). Bseq X ==>
- \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (blast intro: reals_complete Bseq_isUb)
-
lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
by (simp add: Bseq_def)
@@ -1358,40 +1358,29 @@
text {* A monotone sequence converges to its least upper bound. *}
-lemma isLub_mono_imp_LIMSEQ:
- fixes X :: "nat \<Rightarrow> real"
- assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
- assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
- shows "X ----> u"
-proof (rule LIMSEQ_I)
- have 1: "\<forall>n. X n \<le> u"
- using isLubD2 [OF u] by auto
- have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
- using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
- hence 2: "\<forall>y<u. \<exists>n. y < X n"
- by (metis not_le)
- fix r :: real assume "0 < r"
- hence "u - r < u" by simp
- hence "\<exists>m. u - r < X m" using 2 by simp
- then obtain m where "u - r < X m" ..
- with X have "\<forall>n\<ge>m. u - r < X n"
- by (fast intro: less_le_trans)
- hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
- thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
- using 1 by (simp add: diff_less_eq add_commute)
-qed
+lemma LIMSEQ_incseq_SUP:
+ fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+ assumes u: "bdd_above (range X)"
+ assumes X: "incseq X"
+ shows "X ----> (SUP i. X i)"
+ by (rule order_tendstoI)
+ (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
-text{*A standard proof of the theorem for monotone increasing sequence*}
-
-lemma Bseq_mono_convergent:
- "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
- by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
+lemma LIMSEQ_decseq_INF:
+ fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+ assumes u: "bdd_below (range X)"
+ assumes X: "decseq X"
+ shows "X ----> (INF i. X i)"
+ by (rule order_tendstoI)
+ (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
text{*Main monotonicity theorem*}
lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
- by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
- Bseq_mono_convergent)
+ by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
+
+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)"
+ by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
lemma Cauchy_iff:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
--- a/src/HOL/Lubs.thy Tue Nov 05 09:45:00 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(* Title: HOL/Lubs.thy
- Author: Jacques D. Fleuriot, University of Cambridge
-*)
-
-header {* Definitions of Upper Bounds and Least Upper Bounds *}
-
-theory Lubs
-imports Main
-begin
-
-text {* Thanks to suggestions by James Margetson *}
-
-definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70)
- where "S *<= x = (ALL y: S. y \<le> x)"
-
-definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70)
- where "x <=* S = (ALL y: S. x \<le> y)"
-
-definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "leastP P x = (P x \<and> x <=* Collect P)"
-
-definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "isUb R S x = (S *<= x \<and> x: R)"
-
-definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
- where "isLub R S x = leastP (isUb R S) x"
-
-definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
- where "ubs R S = Collect (isUb R S)"
-
-
-subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
-
-lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
- by (simp add: setle_def)
-
-lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
- by (simp add: setle_def)
-
-lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
- by (simp add: setge_def)
-
-lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
- by (simp add: setge_def)
-
-
-subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
-
-lemma leastPD1: "leastP P x \<Longrightarrow> P x"
- by (simp add: leastP_def)
-
-lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
- by (simp add: leastP_def)
-
-lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
- by (blast dest!: leastPD2 setgeD)
-
-lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
- by (simp add: isLub_def isUb_def leastP_def)
-
-lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
- by (simp add: isLub_def isUb_def leastP_def)
-
-lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
- unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
-
-lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
- by (blast dest!: isLubD1 setleD)
-
-lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
- by (simp add: isLub_def)
-
-lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
- by (simp add: isLub_def)
-
-lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
- by (simp add: isLub_def leastP_def)
-
-lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
- by (simp add: isUb_def setle_def)
-
-lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
- by (simp add: isUb_def)
-
-lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
- by (simp add: isUb_def)
-
-lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
- by (simp add: isUb_def)
-
-lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
- unfolding isLub_def by (blast intro!: leastPD3)
-
-lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
- unfolding ubs_def isLub_def by (rule leastPD2)
-
-lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
- apply (frule isLub_isUb)
- apply (frule_tac x = y in isLub_isUb)
- apply (blast intro!: order_antisym dest!: isLub_le_isUb)
- done
-
-end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:45:02 2013 +0100
@@ -4506,38 +4506,30 @@
apply (erule_tac x="x - y" in ballE)
apply (auto simp add: inner_diff)
done
- def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
+ def k \<equiv> "SUP x:t. a \<bullet> x"
show ?thesis
apply (rule_tac x="-a" in exI)
apply (rule_tac x="-(k + b / 2)" in exI)
- apply rule
- apply rule
- defer
- apply rule
+ apply (intro conjI ballI)
unfolding inner_minus_left and neg_less_iff_less
proof -
- from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
- apply (erule_tac x=y in ballE)
- apply (rule setleI)
- using `y \<in> s`
- apply auto
- done
- then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k"
+ fix x assume "x \<in> t"
+ then have "inner a x - b / 2 < k"
unfolding k_def
- apply (rule_tac isLub_cSup)
- using assms(5)
- apply auto
- done
- fix x
- assume "x \<in> t"
- then show "inner a x < (k + b / 2)"
- using `0<b` and isLubD2[OF k, of "inner a x"] by auto
+ proof (subst less_cSUP_iff)
+ show "t \<noteq> {}" by fact
+ show "bdd_above (op \<bullet> a ` t)"
+ using ab[rule_format, of y] `y \<in> s`
+ by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
+ qed (auto intro!: bexI[of _ x] `0<b`)
+ then show "inner a x < k + b / 2"
+ by auto
next
fix x
assume "x \<in> s"
then have "k \<le> inner a x - b"
unfolding k_def
- apply (rule_tac cSup_least)
+ apply (rule_tac cSUP_least)
using assms(5)
using ab[THEN bspec[where x=x]]
apply auto
@@ -4626,20 +4618,14 @@
from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
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"
using assms(3-5) by auto
- then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
+ then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
by (force simp add: inner_diff)
- then show ?thesis
- apply (rule_tac x=a in exI)
- apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI)
+ then have bdd: "bdd_above ((op \<bullet> a)`s)"
+ using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *])
+ show ?thesis
using `a\<noteq>0`
- apply auto
- apply (rule isLub_cSup[THEN isLubD2])
- prefer 4
- apply (rule cSup_least)
- using assms(3-5)
- apply (auto simp add: setle_def)
- apply metis
- done
+ by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
+ (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *)
qed
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:02 2013 +0100
@@ -28,10 +28,10 @@
proof -
have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
by arith
- then show ?thesis
- using S b cSup_bounds[of S "l - e" "l+e"]
- unfolding th
- by (auto simp add: setge_def setle_def)
+ have "bdd_above S"
+ using b by (auto intro!: bdd_aboveI[of _ "l + e"])
+ with S b show ?thesis
+ unfolding th by (auto intro!: cSup_upper2 cSup_least)
qed
lemma cInf_asclose: (* TODO: is this really needed? *)
@@ -70,39 +70,6 @@
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
by (metis cInf_eq_Min Min_le_iff)
-lemma Inf: (* rename *)
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
- by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
- intro: cInf_lower cInf_greatest)
-
-lemma real_le_inf_subset:
- assumes "t \<noteq> {}"
- and "t \<subseteq> s"
- and "\<exists>b. b <=* s"
- shows "Inf s \<le> Inf (t::real set)"
- apply (rule isGlb_le_isLb)
- apply (rule Inf[OF assms(1)])
- apply (insert assms)
- apply (erule exE)
- apply (rule_tac x = b in exI)
- apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
- done
-
-lemma real_ge_sup_subset:
- fixes t :: "real set"
- assumes "t \<noteq> {}"
- and "t \<subseteq> s"
- and "\<exists>b. s *<= b"
- shows "Sup s \<ge> Sup t"
- apply (rule isLub_le_isUb)
- apply (rule isLub_cSup[OF assms(1)])
- apply (insert assms)
- apply (erule exE)
- apply (rule_tac x = b in exI)
- apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
- done
-
(*declare not_less[simp] not_le[simp]*)
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -486,24 +453,24 @@
subsection {* Bounds on intervals where they exist. *}
definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
- where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
+ where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
- where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
+ where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
lemma interval_upperbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
unfolding interval_upperbound_def euclidean_representation_setsum
- by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
- intro!: cSup_unique)
+ by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
+ intro!: cSup_eq)
lemma interval_lowerbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
unfolding interval_lowerbound_def euclidean_representation_setsum
- by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
- intro!: cInf_unique)
+ by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
+ intro!: cInf_eq)
lemmas interval_bounds = interval_upperbound interval_lowerbound
@@ -6627,7 +6594,7 @@
lemma interval_bound_sing[simp]:
"interval_upperbound {a} = a"
"interval_lowerbound {a} = a"
- unfolding interval_upperbound_def interval_lowerbound_def
+ unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
by (auto simp: euclidean_representation)
lemma additive_tagged_division_1:
@@ -11236,37 +11203,26 @@
lemma bounded_variation_absolutely_integrable_interval:
fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
assumes "f integrable_on {a..b}"
- and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+ and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
shows "f absolutely_integrable_on {a..b}"
proof -
- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
- def i \<equiv> "Sup ?S"
- have i: "isLub UNIV ?S i"
- unfolding i_def
- apply (rule isLub_cSup)
- apply (rule elementary_interval)
- defer
- apply (rule_tac x=B in exI)
- apply (rule setleI)
- using assms(2)
- apply auto
- done
+ let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
+ have D_1: "?D \<noteq> {}"
+ by (rule elementary_interval[of a b]) auto
+ have D_2: "bdd_above (?f`?D)"
+ by (metis * mem_Collect_eq bdd_aboveI2)
+ note D = D_1 D_2
+ let ?S = "SUP x:?D. ?f x"
show ?thesis
apply rule
apply (rule assms)
apply rule
- apply (subst has_integral[of _ i])
+ apply (subst has_integral[of _ ?S])
proof safe
case goal1
- then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
- {d. d division_of {a..b}}))"
- using isLub_ubs[OF i,rule_format]
- unfolding setge_def ubs_def
- by auto
- then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
- unfolding mem_Collect_eq isUb_def setle_def
- by (simp add: not_le)
- then guess d .. note d=conjunctD2[OF this]
+ then have "?S - e / 2 < ?S" by simp
+ then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
+ unfolding less_cSUP_iff[OF D] by auto
note d' = division_ofD[OF this(1)]
have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
@@ -11451,21 +11407,17 @@
done
note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
- have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
- sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
+ have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
+ sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
by arith
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
+ show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
unfolding real_norm_def
apply (rule *[rule_format,OF **])
apply safe
apply(rule d(2))
proof -
- case goal1
- show ?case unfolding sum_p'
- apply (rule isLubD2[OF i])
- using division_of_tagged_division[OF p'']
- apply auto
- done
+ case goal1 show ?case
+ by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
next
case goal2
have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
@@ -11756,18 +11708,13 @@
and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
shows "f absolutely_integrable_on UNIV"
proof (rule absolutely_integrable_onI, fact, rule)
- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of (\<Union>d)}"
- def i \<equiv> "Sup ?S"
- have i: "isLub UNIV ?S i"
- unfolding i_def
- apply (rule isLub_cSup)
- apply (rule elementary_interval)
- defer
- apply (rule_tac x=B in exI)
- apply (rule setleI)
- using assms(2)
- apply auto
- done
+ let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
+ have D_1: "?D \<noteq> {}"
+ by (rule elementary_interval) auto
+ have D_2: "bdd_above (?f`?D)"
+ by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
+ note D = D_1 D_2
+ let ?S = "SUP d:?D. ?f d"
have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
apply (rule integrable_on_subinterval[OF assms(1)])
@@ -11776,7 +11723,7 @@
apply (rule assms(2)[rule_format])
apply auto
done
- show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
+ show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
apply (subst has_integral_alt')
apply safe
proof -
@@ -11785,16 +11732,11 @@
using f_int[of a b] by auto
next
case goal2
- have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
+ have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
proof (rule ccontr)
assume "\<not> ?thesis"
- then have "i \<le> i - e"
- apply -
- apply (rule isLub_le_isUb[OF i])
- apply (rule isUbI)
- unfolding setle_def
- apply auto
- done
+ then have "?S \<le> ?S - e"
+ by (intro cSUP_least[OF D(1)]) auto
then show False
using goal2 by auto
qed
@@ -11811,9 +11753,9 @@
proof -
fix a b :: 'n
assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
- have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
+ have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
by arith
- show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
+ show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
unfolding real_norm_def
apply (rule *[rule_format])
apply safe
@@ -11865,10 +11807,10 @@
from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
- have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
- abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
+ have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
+ abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
by arith
- show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
+ show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
apply (subst if_P)
apply rule
proof (rule *[rule_format])
@@ -11891,18 +11833,12 @@
apply (subst abs_of_nonneg)
apply auto
done
- show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
+ show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
+ using partial_division_of_tagged_division[of p "{a..b}"] p(1)
apply (subst setsum_over_tagged_division_lemma[OF p(1)])
- defer
- apply (rule isLubD2[OF i])
- unfolding image_iff
- apply (rule_tac x="snd ` p" in bexI)
- unfolding mem_Collect_eq
- defer
- apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
- using p(1)
- unfolding tagged_division_of_def
- apply auto
+ apply (simp add: integral_null)
+ apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
+ apply (auto simp: tagged_partial_division_of_def)
done
qed
qed
@@ -12378,11 +12314,22 @@
lemma dominated_convergence:
fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
- and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
+ and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
shows "g integrable_on s"
and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
proof -
+ have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
+ proof (safe intro!: bdd_belowI)
+ fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
+ using assms(3)[rule_format, of x n] by simp
+ qed
+ have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
+ proof (safe intro!: bdd_aboveI)
+ fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
+ using assms(3)[rule_format, of x n] by simp
+ qed
+
have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
@@ -12422,66 +12369,32 @@
fix x
assume x: "x \<in> s"
show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
- apply (rule cInf_ge)
- unfolding setge_def
- defer
- apply rule
- apply (subst cInf_finite_le_iff)
- prefer 3
- apply (rule_tac x=xa in bexI)
- apply auto
- done
- let ?S = "{f j x| j. m \<le> j}"
- def i \<equiv> "Inf ?S"
- show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+ by (rule cInf_superset_mono) auto
+ let ?S = "{f j x| j. m \<le> j}"
+ show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
proof (rule LIMSEQ_I)
case goal1
note r = this
- have i: "isGlb UNIV ?S i"
- unfolding i_def
- apply (rule Inf)
- defer
- apply (rule_tac x="- h x - 1" in exI)
- unfolding setge_def
- proof safe
- case goal1
- then show ?case using assms(3)[rule_format,OF x, of j] by auto
- qed auto
-
- have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
- proof(rule ccontr)
- assume "\<not> ?thesis"
- then have "i \<ge> i + r"
- apply -
- apply (rule isGlb_le_isLb[OF i])
- apply (rule isLbI)
- unfolding setge_def
- apply fastforce+
- done
- then show False using r by auto
- qed
- then guess y .. note y=this[unfolded not_le]
- from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+
+ have "\<exists>y\<in>?S. y < Inf ?S + r"
+ by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
+ then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
+ by blast
show ?case
apply (rule_tac x=N in exI)
proof safe
case goal1
- have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
+ have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
by arith
show ?case
unfolding real_norm_def
- apply (rule *[rule_format,OF y(2)])
- unfolding i_def
- apply (rule real_le_inf_subset)
- prefer 3
- apply (rule,rule isGlbD1[OF i])
- prefer 3
- apply (subst cInf_finite_le_iff)
- prefer 3
- apply (rule_tac x=y in bexI)
+ apply (rule *[rule_format, OF N(1)])
+ apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
+ apply (rule cInf_lower)
using N goal1
- apply auto
+ apply auto []
+ apply simp
done
qed
qed
@@ -12525,65 +12438,27 @@
fix x
assume x: "x\<in>s"
show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
- apply (rule cSup_le)
- unfolding setle_def
- defer
- apply rule
- apply (subst cSup_finite_ge_iff)
- prefer 3
- apply (rule_tac x=y in bexI)
- apply auto
- done
- let ?S = "{f j x| j. m \<le> j}"
- def i \<equiv> "Sup ?S"
- show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+ by (rule cSup_subset_mono) auto
+ let ?S = "{f j x| j. m \<le> j}"
+ show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
proof (rule LIMSEQ_I)
case goal1 note r=this
- have i: "isLub UNIV ?S i"
- unfolding i_def
- apply (rule isLub_cSup)
- defer
- apply (rule_tac x="h x" in exI)
- unfolding setle_def
- proof safe
- case goal1
- then show ?case
- using assms(3)[rule_format,OF x, of j] by auto
- qed auto
-
- have "\<exists>y\<in>?S. \<not> y \<le> i - r"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "i \<le> i - r"
- apply -
- apply (rule isLub_le_isUb[OF i])
- apply (rule isUbI)
- unfolding setle_def
- apply fastforce+
- done
- then show False
- using r by auto
- qed
- then guess y .. note y=this[unfolded not_le]
- from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+ have "\<exists>y\<in>?S. Sup ?S - r < y"
+ by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
+ then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
+ by blast
show ?case
apply (rule_tac x=N in exI)
proof safe
case goal1
- have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
+ have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
by arith
show ?case
- unfolding real_norm_def
- apply (rule *[rule_format,OF y(2)])
- unfolding i_def
- apply (rule real_ge_sup_subset)
- prefer 3
- apply (rule, rule isLubD1[OF i])
- prefer 3
- apply (subst cSup_finite_ge_iff)
- prefer 3
- apply (rule_tac x = y in bexI)
+ apply simp
+ apply (rule *[rule_format, OF N(1)])
+ apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
+ apply (subst cSup_upper)
using N goal1
apply auto
done
@@ -12616,17 +12491,7 @@
have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
- apply -
- apply (rule real_le_inf_subset)
- prefer 3
- unfolding setge_def
- apply (rule_tac x="- h x" in exI)
- apply safe
- apply (rule *)
- using assms(3)[rule_format,OF x]
- unfolding real_norm_def abs_le_iff
- apply auto
- done
+ by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
proof (rule LIMSEQ_I)
@@ -12674,16 +12539,7 @@
assume x: "x \<in> s"
show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
- apply -
- apply (rule real_ge_sup_subset)
- prefer 3
- unfolding setle_def
- apply (rule_tac x="h x" in exI)
- apply safe
- using assms(3)[rule_format,OF x]
- unfolding real_norm_def abs_le_iff
- apply auto
- done
+ by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
proof (rule LIMSEQ_I)
case goal1
@@ -12712,41 +12568,18 @@
from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
show ?case
- apply (rule_tac x="N1+N2" in exI, safe)
- proof -
+ proof (rule_tac x="N1+N2" in exI, safe)
fix n
assume n: "n \<ge> N1 + N2"
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"
by arith
show "norm (integral s (f n) - integral s g) < r"
unfolding real_norm_def
- apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
- proof -
+ proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
- proof (rule integral_le[OF dec1(1) assms(1)], safe)
- fix x
- assume x: "x \<in> s"
- have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
- show "Inf {f j x |j. n \<le> j} \<le> f n x"
- apply (intro cInf_lower bdd_belowI)
- apply auto []
- apply (rule *)
- using assms(3)[rule_format,OF x]
- unfolding real_norm_def abs_le_iff
- apply auto
- done
- qed
+ by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
- proof (rule integral_le[OF assms(1) inc1(1)], safe)
- fix x
- assume x: "x \<in> s"
- show "f n x \<le> Sup {f j x |j. n \<le> j}"
- apply (rule cSup_upper)
- using assms(3)[rule_format,OF x]
- unfolding real_norm_def abs_le_iff
- apply auto
- done
- qed
+ by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
qed (insert n, auto)
qed
qed
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Tue Nov 05 09:45:02 2013 +0100
@@ -8,7 +8,7 @@
imports Linear_Algebra
begin
-definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
+definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
lemma norm_bound_generalize:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -67,25 +67,22 @@
shows "norm (f x) \<le> onorm f * norm x"
and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
proof -
- let ?S = "{norm (f x) |x. norm x = 1}"
+ let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
then have Se: "?S \<noteq> {}"
by auto
- from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
- unfolding norm_bound_generalize[OF lf, symmetric]
- by (auto simp add: setle_def)
- from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
- show "norm (f x) \<le> onorm f * norm x"
+ from linear_bounded[OF lf] have b: "bdd_above ?S"
+ unfolding norm_bound_generalize[OF lf, symmetric] by auto
+ then show "norm (f x) \<le> onorm f * norm x"
apply -
apply (rule spec[where x = x])
unfolding norm_bound_generalize[OF lf, symmetric]
- apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
+ apply (auto simp: onorm_def intro!: cSUP_upper)
done
show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
- using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
unfolding norm_bound_generalize[OF lf, symmetric]
- by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
+ using Se by (auto simp: onorm_def intro!: cSUP_least b)
qed
lemma onorm_pos_le:
@@ -107,18 +104,8 @@
apply arith
done
-lemma onorm_const:
- "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
-proof -
- let ?f = "\<lambda>x::'a. y::'b"
- have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
- by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
- show ?thesis
- unfolding onorm_def th
- apply (rule cSup_unique)
- apply (simp_all add: setle_def)
- done
-qed
+lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
+ using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
lemma onorm_pos_lt:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:45:02 2013 +0100
@@ -10,7 +10,6 @@
imports
Complex_Main
"~~/src/HOL/Library/Countable_Set"
- "~~/src/HOL/Library/Glbs"
"~~/src/HOL/Library/FuncSet"
Linear_Algebra
Norm_Arith
@@ -28,8 +27,6 @@
lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
by (rule LIMSEQ_subseq_LIMSEQ)
-lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
-
lemma countable_PiE:
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
@@ -1555,7 +1552,7 @@
fix y
assume "y \<in> {x<..} \<inter> I"
with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
- by (auto intro: cInf_lower)
+ by (auto intro!: cInf_lower bdd_belowI2)
with a have "a < f y"
by (blast intro: less_le_trans)
}
--- a/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:02 2013 +0100
@@ -6,7 +6,7 @@
header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
theory NSA
-imports HyperDef
+imports HyperDef "~~/src/HOL/Library/Lubs_Glbs"
begin
definition
--- a/src/HOL/Real.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real.thy Tue Nov 05 09:45:02 2013 +0100
@@ -970,13 +970,6 @@
qed
end
-text {*
- \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
-*}
-
-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"
- by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
-
subsection {* Hiding implementation details *}
--- a/src/HOL/Real_Vector_Spaces.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Nov 05 09:45:02 2013 +0100
@@ -1425,9 +1425,6 @@
@{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
*}
-lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
-by (simp add: isUbI setleI)
-
lemma increasing_LIMSEQ:
fixes f :: "nat \<Rightarrow> real"
assumes inc: "\<And>n. f n \<le> f (Suc n)"
@@ -1454,40 +1451,33 @@
then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
{ fix N x assume N: "\<forall>n\<ge>N. X n < x"
- have "isUb UNIV S x"
- proof (rule isUb_UNIV_I)
fix y::real assume "y \<in> S"
hence "\<exists>M. \<forall>n\<ge>M. y < X n"
by (simp add: S_def)
then obtain M where "\<forall>n\<ge>M. y < X n" ..
hence "y < X (max M N)" by simp
also have "\<dots> < x" using N by simp
- finally show "y \<le> x"
- by (rule order_less_imp_le)
- qed }
+ finally have "y \<le> x"
+ by (rule order_less_imp_le) }
note bound_isUb = this
- have "\<exists>u. isLub UNIV S u"
- proof (rule reals_complete)
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
using X[THEN metric_CauchyD, OF zero_less_one] by auto
hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
- show "\<exists>x. x \<in> S"
- proof
+ have [simp]: "S \<noteq> {}"
+ proof (intro exI ex_in_conv[THEN iffD1])
from N have "\<forall>n\<ge>N. X N - 1 < X n"
by (simp add: abs_diff_less_iff dist_real_def)
thus "X N - 1 \<in> S" by (rule mem_S)
qed
- show "\<exists>u. isUb UNIV S u"
+ have [simp]: "bdd_above S"
proof
from N have "\<forall>n\<ge>N. X n < X N + 1"
by (simp add: abs_diff_less_iff dist_real_def)
- thus "isUb UNIV S (X N + 1)"
+ thus "\<And>s. s \<in> S \<Longrightarrow> s \<le> X N + 1"
by (rule bound_isUb)
qed
- qed
- then obtain x where x: "isLub UNIV S x" ..
- have "X ----> x"
+ have "X ----> Sup S"
proof (rule metric_LIMSEQ_I)
fix r::real assume "0 < r"
hence r: "0 < r/2" by simp
@@ -1499,17 +1489,18 @@
from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
hence "X N - r/2 \<in> S" by (rule mem_S)
- hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
+ hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
- hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
- hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
+ from bound_isUb[OF this]
+ have 2: "Sup S \<le> X N + r/2"
+ by (intro cSup_least) simp_all
- show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
+ show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r"
proof (intro exI allI impI)
fix n assume n: "N \<le> n"
from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
- thus "dist (X n) x < r" using 1 2
+ thus "dist (X n) (Sup S) < r" using 1 2
by (simp add: abs_diff_less_iff dist_real_def)
qed
qed
--- a/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:02 2013 +0100
@@ -1506,7 +1506,6 @@
instance real :: linorder
by (intro_classes, rule real_le_linear)
-
lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
apply (cases x, cases y)
apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
@@ -1657,7 +1656,6 @@
lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
-
subsection {* Completeness of Positive Reals *}
text {*
@@ -1759,107 +1757,23 @@
qed
text {*
- \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
-*}
-
-lemma posreals_complete:
- assumes positive_S: "\<forall>x \<in> S. 0 < x"
- and not_empty_S: "\<exists>x. x \<in> S"
- and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
- shows "\<exists>t. isLub (UNIV::real set) S t"
-proof
- let ?pS = "{w. real_of_preal w \<in> S}"
-
- obtain u where "isUb UNIV S u" using upper_bound_Ex ..
- hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
-
- obtain x where x_in_S: "x \<in> S" using not_empty_S ..
- hence x_gt_zero: "0 < x" using positive_S by simp
- have "x \<le> u" using sup and x_in_S ..
- hence "0 < u" using x_gt_zero by arith
-
- then obtain pu where u_is_pu: "u = real_of_preal pu"
- by (auto simp add: real_gt_zero_preal_Ex)
-
- have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
- proof
- fix pa
- assume "pa \<in> ?pS"
- then obtain a where a: "a \<in> S" "a = real_of_preal pa"
- by simp
- then have "a \<le> u" using sup by simp
- with a show "pa \<le> pu"
- using sup and u_is_pu by (simp add: real_of_preal_le_iff)
- qed
-
- have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
- proof
- fix y
- assume y_in_S: "y \<in> S"
- hence "0 < y" using positive_S by simp
- then obtain py where y_is_py: "y = real_of_preal py"
- by (auto simp add: real_gt_zero_preal_Ex)
- hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
- with pS_less_pu have "py \<le> psup ?pS"
- by (rule preal_psup_le)
- thus "y \<le> real_of_preal (psup ?pS)"
- using y_is_py by (simp add: real_of_preal_le_iff)
- qed
-
- moreover {
- fix x
- assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
- have "real_of_preal (psup ?pS) \<le> x"
- proof -
- obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
- hence s_pos: "0 < s" using positive_S by simp
-
- hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
- then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
- hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
-
- from x_ub_S have "s \<le> x" using s_in_S ..
- hence "0 < x" using s_pos by simp
- hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
- then obtain "px" where x_is_px: "x = real_of_preal px" ..
-
- have "\<forall>pe \<in> ?pS. pe \<le> px"
- proof
- fix pe
- assume "pe \<in> ?pS"
- hence "real_of_preal pe \<in> S" by simp
- hence "real_of_preal pe \<le> x" using x_ub_S by simp
- thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
- qed
-
- moreover have "?pS \<noteq> {}" using ps_in_pS by auto
- ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
- thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
- qed
- }
- ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
- by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-qed
-
-text {*
- \medskip reals Completeness (again!)
+ \medskip Completeness
*}
lemma reals_complete:
+ fixes S :: "real set"
assumes notempty_S: "\<exists>X. X \<in> S"
- and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
- shows "\<exists>t. isLub (UNIV :: real set) S t"
+ and exists_Ub: "bdd_above S"
+ shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)"
proof -
obtain X where X_in_S: "X \<in> S" using notempty_S ..
- obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
- using exists_Ub ..
+ obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y"
+ using exists_Ub by (auto simp: bdd_above_def)
let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
{
fix x
- assume "isUb (UNIV::real set) S x"
- hence S_le_x: "\<forall> y \<in> S. y <= x"
- by (simp add: isUb_def setle_def)
+ assume S_le_x: "\<forall>s\<in>S. s \<le> x"
{
fix s
assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
@@ -1868,86 +1782,74 @@
then have "x1 \<le> x" using S_le_x by simp
with x1 have "s \<le> x + - X + 1" by arith
}
- then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
- by (auto simp add: isUb_def setle_def)
+ then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
+ by auto
} note S_Ub_is_SHIFT_Ub = this
- hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
- hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
+ have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub)
+ have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2"
+ proof
+ fix s assume "s\<in>?SHIFT"
+ with * have "s \<le> Y + (-X) + 1" by simp
+ also have "\<dots> < Y + (-X) + 2" by simp
+ finally show "s < Y + (-X) + 2" .
+ qed
moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
using X_in_S and Y_isUb by auto
- ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
- using posreals_complete [of ?SHIFT] by blast
+ ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)"
+ using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast
show ?thesis
proof
- show "isLub UNIV S (t + X + (-1))"
- proof (rule isLubI2)
- {
- fix x
- assume "isUb (UNIV::real set) S x"
- hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
- using S_Ub_is_SHIFT_Ub by simp
- hence "t \<le> (x + (-X) + 1)"
- using t_is_Lub by (simp add: isLub_le_isUb)
- hence "t + X + -1 \<le> x" by arith
- }
- then show "(t + X + -1) <=* Collect (isUb UNIV S)"
- by (simp add: setgeI)
+ 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)"
+ proof safe
+ fix x
+ assume "\<forall>s\<in>S. s \<le> x"
+ hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
+ using S_Ub_is_SHIFT_Ub by simp
+ then have "\<not> x + (-X) + 1 < t"
+ by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less)
+ thus "t + X + -1 \<le> x" by arith
next
- show "isUb UNIV S (t + X + -1)"
- proof -
- {
- fix y
- assume y_in_S: "y \<in> S"
- have "y \<le> t + X + -1"
- proof -
- obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
- hence "\<exists> x \<in> S. u = x + - X + 1" by simp
- then obtain "x" where x_and_u: "u = x + - X + 1" ..
- have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
+ fix y
+ assume y_in_S: "y \<in> S"
+ obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
+ hence "\<exists> x \<in> S. u = x + - X + 1" by simp
+ then obtain "x" where x_and_u: "u = x + - X + 1" ..
+ have u_le_t: "u \<le> t"
+ proof (rule dense_le)
+ fix x assume "x < u" then have "x < t"
+ using u_in_shift t_is_Lub by auto
+ then show "x \<le> t" by simp
+ qed
- show ?thesis
- proof cases
- assume "y \<le> x"
- moreover have "x = u + X + - 1" using x_and_u by arith
- moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
- ultimately show "y \<le> t + X + -1" by arith
- next
- assume "~(y \<le> x)"
- hence x_less_y: "x < y" by arith
+ show "y \<le> t + X + -1"
+ proof cases
+ assume "y \<le> x"
+ moreover have "x = u + X + - 1" using x_and_u by arith
+ moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
+ ultimately show "y \<le> t + X + -1" by arith
+ next
+ assume "~(y \<le> x)"
+ hence x_less_y: "x < y" by arith
- have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
- hence "0 < x + (-X) + 1" by simp
- hence "0 < y + (-X) + 1" using x_less_y by arith
- hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
- hence "y + (-X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2)
- thus ?thesis by simp
- qed
- qed
- }
- then show ?thesis by (simp add: isUb_def setle_def)
+ have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
+ hence "0 < x + (-X) + 1" by simp
+ hence "0 < y + (-X) + 1" using x_less_y by arith
+ hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
+ have "y + (-X) + 1 \<le> t"
+ proof (rule dense_le)
+ fix x assume "x < y + (-X) + 1" then have "x < t"
+ using * t_is_Lub by auto
+ then show "x \<le> t" by simp
+ qed
+ thus ?thesis by simp
qed
qed
qed
qed
-text{*A version of the same theorem without all those predicates!*}
-lemma reals_complete2:
- fixes S :: "(real set)"
- assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
- shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) &
- (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
-proof -
- have "\<exists>x. isLub UNIV S x"
- by (rule reals_complete)
- (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
- thus ?thesis
- by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
-qed
-
-
subsection {* The Archimedean Property of the Reals *}
theorem reals_Archimedean:
@@ -1969,34 +1871,30 @@
by (rule mult_right_mono)
thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
qed
- hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
- by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
- hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
- by (simp add: isUbI)
- hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
- moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
- ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
- by (simp add: reals_complete)
- then obtain "t" where
- t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
+ hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}"
+ by (auto intro!: bdd_aboveI[of _ 1])
+ have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
+ obtain t where
+ upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and
+ least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y"
+ using reals_complete[OF 1 2] by auto
+
- have "\<forall>n::nat. x * of_nat n \<le> t + - x"
- proof
- fix n
- from t_is_Lub have "x * of_nat (Suc n) \<le> t"
- by (simp add: isLubD2)
- hence "x * (of_nat n) + x \<le> t"
- by (simp add: distrib_left)
- thus "x * (of_nat n) \<le> t + - x" by arith
+ have "t \<le> t + - x"
+ proof (rule least)
+ fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}"
+ have "\<forall>n::nat. x * of_nat n \<le> t + - x"
+ proof
+ fix n
+ have "x * of_nat (Suc n) \<le> t"
+ by (simp add: upper)
+ hence "x * (of_nat n) + x \<le> t"
+ by (simp add: distrib_left)
+ thus "x * (of_nat n) \<le> t + - x" by arith
+ qed hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
+ with a show "a \<le> t + - x"
+ by auto
qed
-
- hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
- hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= (t + - x)"
- by (auto simp add: setle_def)
- hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
- by (simp add: isUbI)
- hence "t \<le> t + - x"
- using t_is_Lub by (simp add: isLub_le_isUb)
thus False using x_pos by arith
qed