introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
@@ -3491,11 +3491,11 @@
apply(rule,rule) defer apply(rule) 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` by auto
- hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
+ hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac isLub_cSup) using assms(5) by auto
fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
next
fix x assume "x\<in>s"
- hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
+ hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac cSup_least) using assms(5)
using ab[THEN bspec[where x=x]] by auto
thus "k + b / 2 < inner a x" using `0 < b` by auto
qed
@@ -3544,9 +3544,9 @@
thus ?thesis
apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
apply auto
- apply (rule Sup[THEN isLubD2])
+ apply (rule isLub_cSup[THEN isLubD2])
prefer 4
- apply (rule Sup_least)
+ apply (rule cSup_least)
using assms(3-5) apply (auto simp add: setle_def)
apply metis
done
@@ -6208,7 +6208,7 @@
using interior_subset[of I] `x \<in> interior I` by auto
have "Inf (?F x) \<le> (f x - f y) / (x - y)"
- proof (rule Inf_lower2)
+ proof (rule cInf_lower2)
show "(f x - f t) / (x - t) \<in> ?F x"
using `t \<in> I` `x < t` by auto
show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
@@ -6231,7 +6231,7 @@
with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
have "(f x - f y) / (x - y) \<le> Inf (?F x)"
- proof (rule Inf_greatest)
+ proof (rule cInf_greatest)
have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
using `y < x` by (auto simp: field_simps)
also
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Mar 22 10:41:43 2013 +0100
@@ -523,7 +523,7 @@
proof -
{ assume "S ~= {}"
{ assume ex: "EX B. ALL x:S. B<=x"
- then have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
+ then have *: "ALL x:S. Inf S <= x" using cInf_lower_EX[of _ S] ex by metis
then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
then have "S = {Inf S ..}" by auto
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Mar 22 10:41:43 2013 +0100
@@ -18,7 +18,7 @@
subsection {*Fashoda meet theorem. *}
lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
- unfolding infnorm_cart UNIV_2 apply(rule Sup_eq) by auto
+ unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto
lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
(abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 22 10:41:43 2013 +0100
@@ -8,6 +8,45 @@
"~~/src/HOL/Library/Indicator_Function"
begin
+lemma cSup_finite_ge_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
+by (metis Max_ge Se cSup_eq_Max Max_in fS linorder_not_le less_le_trans)
+
+lemma cSup_finite_le_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
+by (metis Max_ge Se cSup_eq_Max Max_in fS order_trans)
+
+lemma Inf: (* rename *)
+ fixes S :: "real set"
+ shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> 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> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
+ shows "Inf s <= 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:
+ assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b"
+ shows "Sup s >= Sup (t::real set)"
+ 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
@@ -49,33 +88,6 @@
shows "bounded_linear f"
unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
-lemma Inf: (* rename *)
- fixes S :: "real set"
- shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
-by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def)
-
-lemma real_le_inf_subset:
- assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
- shows "Inf s <= 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)
- done
-
-lemma real_ge_sup_subset:
- assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b"
- shows "Sup s >= Sup (t::real set)"
- apply (rule isLub_le_isUb)
- apply (rule Sup[OF assms(1)])
- apply (insert assms)
- apply (erule exE)
- apply (rule_tac x = b in exI)
- apply (auto simp: isUb_def setle_def)
- done
-
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
by (rule bounded_linear_inner_left)
@@ -387,14 +399,14 @@
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!: Sup_unique)
+ intro!: cSup_unique)
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!: Inf_unique)
+ intro!: cInf_unique)
lemmas interval_bounds = interval_upperbound interval_lowerbound
@@ -3201,7 +3213,7 @@
let ?goal = "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
{ presume "p\<noteq>{} \<Longrightarrow> ?goal" thus ?goal apply(cases "p={}") using goal1 by auto }
assume as':"p \<noteq> {}" from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
- hence N:"\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N" apply(subst(asm) Sup_finite_le_iff) using as as' by auto
+ hence N:"\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N" apply(subst(asm) cSup_finite_le_iff) using as as' by auto
have "\<forall>i. \<exists>q. q tagged_division_of {a..b} \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
apply(rule,rule tagged_division_finer[OF as(1) d(1)]) by auto
from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
@@ -5480,7 +5492,7 @@
"\<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 Sup)
+ 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) by auto
show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i])
@@ -5693,7 +5705,7 @@
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 Sup)
+ 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) by auto
have f_int:"\<And>a b. f absolutely_integrable_on {a..b}"
@@ -6044,7 +6056,7 @@
prefer 5
unfolding real_norm_def
apply rule
- apply (rule Inf_abs_ge)
+ apply (rule cInf_abs_ge)
prefer 5
apply rule
apply (rule_tac g = h in absolutely_integrable_integrable_bound_real)
@@ -6065,11 +6077,11 @@
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 Inf_ge)
+ apply (rule cInf_ge)
unfolding setge_def
defer
apply rule
- apply (subst Inf_finite_le_iff)
+ apply (subst cInf_finite_le_iff)
prefer 3
apply (rule_tac x=xa in bexI)
apply auto
@@ -6119,7 +6131,7 @@
prefer 3
apply (rule,rule isGlbD1[OF i])
prefer 3
- apply (subst Inf_finite_le_iff)
+ apply (subst cInf_finite_le_iff)
prefer 3
apply (rule_tac x=y in bexI)
using N goal1
@@ -6146,7 +6158,7 @@
apply(rule absolutely_integrable_sup_real)
prefer 5 unfolding real_norm_def
apply rule
- apply (rule Sup_abs_le)
+ apply (rule cSup_abs_le)
prefer 5
apply rule
apply (rule_tac g=h in absolutely_integrable_integrable_bound_real)
@@ -6167,11 +6179,11 @@
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 Sup_le)
+ apply (rule cSup_le)
unfolding setle_def
defer
apply rule
- apply (subst Sup_finite_ge_iff)
+ apply (subst cSup_finite_ge_iff)
prefer 3
apply (rule_tac x=y in bexI)
apply auto
@@ -6183,7 +6195,7 @@
case goal1 note r=this
have i: "isLub UNIV ?S i"
unfolding i_def
- apply (rule Sup)
+ apply (rule isLub_cSup)
defer
apply (rule_tac x="h x" in exI)
unfolding setle_def
@@ -6221,7 +6233,7 @@
prefer 3
apply (rule, rule isLubD1[OF i])
prefer 3
- apply (subst Sup_finite_ge_iff)
+ apply (subst cSup_finite_ge_iff)
prefer 3
apply (rule_tac x = y in bexI)
using N goal1
@@ -6246,7 +6258,7 @@
apply fact+
unfolding real_norm_def
apply rule
- apply (rule Inf_abs_ge)
+ apply (rule cInf_abs_ge)
using assms(3)
apply auto
done
@@ -6276,7 +6288,7 @@
apply (rule_tac x=N in exI,safe)
unfolding real_norm_def
apply (rule le_less_trans[of _ "r/2"])
- apply (rule Inf_asclose)
+ apply (rule cInf_asclose)
apply safe
defer
apply (rule less_imp_le)
@@ -6302,7 +6314,7 @@
apply fact+
unfolding real_norm_def
apply rule
- apply (rule Sup_abs_le)
+ apply (rule cSup_abs_le)
using assms(3)
apply auto
done
@@ -6330,7 +6342,7 @@
apply (rule_tac x=N in exI,safe)
unfolding real_norm_def
apply (rule le_less_trans[of _ "r/2"])
- apply (rule Sup_asclose)
+ apply (rule cSup_asclose)
apply safe
defer
apply (rule less_imp_le)
@@ -6364,7 +6376,7 @@
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 (rule Inf_lower[where z="- h x"])
+ apply (rule cInf_lower[where z="- h x"])
defer
apply (rule *)
using assms(3)[rule_format,OF x]
@@ -6377,7 +6389,7 @@
fix x
assume x: "x \<in> s"
show "f n x \<le> Sup {f j x |j. n \<le> j}"
- apply (rule Sup_upper[where z="h x"])
+ apply (rule cSup_upper[where z="h x"])
defer
using assms(3)[rule_format,OF x]
unfolding real_norm_def abs_le_iff
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Mar 22 10:41:43 2013 +0100
@@ -2498,6 +2498,9 @@
"{ abs ((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs(x \<bullet> i)) ` Basis"
by blast
+lemma infnorm_Max: "infnorm (x::'a::euclidean_space) = Max ((\<lambda>i. abs(x \<bullet> i)) ` Basis)"
+ by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
+
lemma infnorm_set_lemma:
shows "finite {abs((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis}"
and "{abs(x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
@@ -2505,41 +2508,22 @@
by auto
lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
- unfolding infnorm_def
- unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
- unfolding infnorm_set_image
- by (auto simp: ex_in_conv)
+ by (simp add: infnorm_Max Max_ge_iff ex_in_conv)
lemma infnorm_triangle: "infnorm ((x::'a::euclidean_space) + y) \<le> infnorm x + infnorm y"
proof -
- have th: "\<And>x y (z::real). x - y <= z \<longleftrightarrow> x - z <= y" by arith
- have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
- have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
+ have *: "\<And>a b c d :: real. \<bar>a\<bar> \<le> c \<Longrightarrow> \<bar>b\<bar> \<le> d \<Longrightarrow> \<bar>a + b\<bar> \<le> c + d"
+ by simp
show ?thesis
- unfolding infnorm_def
- unfolding Sup_finite_le_iff[ OF infnorm_set_lemma[where 'a='a]]
- apply (subst diff_le_eq[symmetric])
- unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
- unfolding infnorm_set_image bex_simps
- apply (subst th)
- unfolding th1
- unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma[where 'a='a]]
- unfolding infnorm_set_image ball_simps bex_simps
- apply (simp add: inner_add_left)
- apply (metis th2)
- done
+ by (auto simp: infnorm_Max inner_add_left intro!: *)
qed
lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::_::euclidean_space) = 0"
proof -
- have "infnorm x <= 0 \<longleftrightarrow> x = 0"
- unfolding infnorm_def
- unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image ball_simps
- apply (subst (1) euclidean_eq_iff)
- apply auto
- done
- then show ?thesis using infnorm_pos_le[of x] by simp
+ have "infnorm x \<le> 0 \<longleftrightarrow> x = 0"
+ unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
+ then show ?thesis
+ using infnorm_pos_le[of x] by simp
qed
lemma infnorm_0: "infnorm 0 = 0"
@@ -2573,40 +2557,24 @@
using infnorm_pos_le[of x] by arith
lemma Basis_le_infnorm:
- assumes b: "b \<in> Basis" shows "\<bar>x \<bullet> b\<bar> \<le> infnorm (x::'a::euclidean_space)"
- unfolding infnorm_def
-proof (subst Sup_finite_ge_iff)
- let ?S = "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
- show "finite ?S" by (rule infnorm_set_lemma)
- show "?S \<noteq> {}" by auto
- show "Bex ?S (op \<le> \<bar>x \<bullet> b\<bar>)"
- using b by (auto intro!: exI[of _ b])
-qed
-
-lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
- apply (subst infnorm_def)
- unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image ball_simps inner_scaleR abs_mult
- using Basis_le_infnorm[of _ x]
- apply (auto intro: mult_mono)
- done
+ "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm (x::'a::euclidean_space)"
+ by (simp add: infnorm_Max)
lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
-proof -
- { assume a0: "a = 0" then have ?thesis by (simp add: infnorm_0) }
- moreover
- { assume a0: "a \<noteq> 0"
- from a0 have th: "(1/a) *\<^sub>R (a *\<^sub>R x) = x" by simp
- from a0 have ap: "\<bar>a\<bar> > 0" by arith
- from infnorm_mul_lemma[of "1/a" "a *\<^sub>R x"]
- have "infnorm x \<le> 1/\<bar>a\<bar> * infnorm (a*\<^sub>R x)"
- unfolding th by simp
- with ap have "\<bar>a\<bar> * infnorm x \<le> \<bar>a\<bar> * (1/\<bar>a\<bar> * infnorm (a *\<^sub>R x))" by (simp add: field_simps)
- then have "\<bar>a\<bar> * infnorm x \<le> infnorm (a*\<^sub>R x)"
- using ap by (simp add: field_simps)
- with infnorm_mul_lemma[of a x] have ?thesis by arith }
- ultimately show ?thesis by blast
-qed
+ unfolding infnorm_Max
+proof (safe intro!: Max_eqI)
+ let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
+ show "\<And>b :: 'a. b \<in> Basis \<Longrightarrow> \<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
+ by (simp add: abs_mult mult_left_mono)
+
+ from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"
+ by (auto simp del: Max_in)
+ then show "\<bar>a\<bar> * Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis) \<in> (\<lambda>i. \<bar>a *\<^sub>R x \<bullet> i\<bar>) ` Basis"
+ by (intro image_eqI[where x=b]) (auto simp: abs_mult)
+qed simp
+
+lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) \<le> \<bar>a\<bar> * infnorm x"
+ unfolding infnorm_mul ..
lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
@@ -2614,15 +2582,13 @@
text {* Prove that it differs only up to a bound from Euclidean norm. *}
lemma infnorm_le_norm: "infnorm x \<le> norm x"
- unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image ball_simps
- by (metis Basis_le_norm)
+ by (simp add: Basis_le_norm infnorm_Max)
lemma euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
by (subst (1 2) euclidean_representation[symmetric, where 'a='a])
(simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
-lemma norm_le_infnorm: "norm(x) <= sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
+lemma norm_le_infnorm: "norm x \<le> sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
proof -
let ?d = "DIM('a)"
have "real ?d \<ge> 0" by simp
@@ -2639,10 +2605,7 @@
apply (auto simp add: power2_eq_square[symmetric])
apply (subst power2_abs[symmetric])
apply (rule power_mono)
- unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image bex_simps
- apply (rule_tac x=i in bexI)
- apply auto
+ apply (auto simp: infnorm_Max)
done
from real_le_lsqrt[OF inner_ge_zero th th1]
show ?thesis unfolding norm_eq_sqrt_inner id_def .
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Fri Mar 22 10:41:43 2013 +0100
@@ -58,7 +58,7 @@
hence 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 Sup[OF Se b, unfolded onorm_def[symmetric]]
+ { from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
show "norm (f x) <= onorm f * norm x"
apply -
apply (rule spec[where x = x])
@@ -66,7 +66,7 @@
by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
{
show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
- using Sup[OF Se b, unfolded onorm_def[symmetric]]
+ 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)}
}
@@ -93,7 +93,7 @@
by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
show ?thesis
unfolding onorm_def th
- apply (rule Sup_unique) by (simp_all add: setle_def)
+ apply (rule cSup_unique) by (simp_all add: setle_def)
qed
lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
@@ -1401,7 +1401,7 @@
show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
proof (rule LIMSEQ_I, rule ccontr)
fix r :: real assume "0 < r"
- with Inf_close[of "f ` ({x<..} \<inter> I)" r]
+ with cInf_close[of "f ` ({x<..} \<inter> I)" r]
obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
from `x < y` have "0 < y - x" by auto
from S(2)[THEN LIMSEQ_D, OF this]
@@ -1409,7 +1409,7 @@
assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
- using S bnd by (intro Inf_lower[where z=K]) auto
+ using S bnd by (intro cInf_lower[where z=K]) auto
ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
by (auto simp: not_less field_simps)
with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
@@ -1727,11 +1727,11 @@
unfolding closure_approachable
proof safe
have *: "\<forall>x\<in>S. Inf S \<le> x"
- using Inf_lower_EX[of _ S] assms by metis
+ using cInf_lower_EX[of _ S] assms by metis
fix e :: real assume "0 < e"
then obtain x where x: "x \<in> S" "x < Inf S + e"
- using Inf_close `S \<noteq> {}` by auto
+ using cInf_close `S \<noteq> {}` by auto
moreover then have "x > Inf S - e" using * by auto
ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
then show "\<exists>x\<in>S. dist x (Inf S) < e"
@@ -1785,13 +1785,13 @@
lemma infdist_nonneg:
shows "0 \<le> infdist x A"
- using assms by (auto simp add: infdist_def)
+ using assms by (auto simp add: infdist_def intro: cInf_greatest)
lemma infdist_le:
assumes "a \<in> A"
assumes "d = dist x a"
shows "infdist x A \<le> d"
- using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
+ using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
lemma infdist_zero[simp]:
assumes "a \<in> A" shows "infdist a A = 0"
@@ -1807,13 +1807,13 @@
next
assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
- proof
+ proof (rule cInf_greatest)
from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
show "infdist x A \<le> d"
unfolding infdist_notempty[OF `A \<noteq> {}`]
- proof (rule Inf_lower2)
+ proof (rule cInf_lower2)
show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
show "dist x a \<le> d" unfolding d by (rule dist_triangle)
fix d assume "d \<in> {dist x a |a. a \<in> A}"
@@ -1822,20 +1822,19 @@
qed
qed
also have "\<dots> = dist x y + infdist y A"
- proof (rule Inf_eq, safe)
+ proof (rule cInf_eq, safe)
fix a assume "a \<in> A"
thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
next
fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
- by (intro Inf_greatest) (auto simp: field_simps)
+ by (intro cInf_greatest) (auto simp: field_simps)
thus "i \<le> dist x y + infdist y A" by simp
qed
finally show ?thesis by simp
qed
-lemma
- in_closure_iff_infdist_zero:
+lemma in_closure_iff_infdist_zero:
assumes "A \<noteq> {}"
shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
proof
@@ -1859,13 +1858,12 @@
assume "\<not> (\<exists>y\<in>A. dist y x < e)"
hence "infdist x A \<ge> e" using `a \<in> A`
unfolding infdist_def
- by (force simp: dist_commute)
+ by (force simp: dist_commute intro: cInf_greatest)
with x `0 < e` show False by auto
qed
qed
-lemma
- in_closed_iff_infdist_zero:
+lemma in_closed_iff_infdist_zero:
assumes "closed A" "A \<noteq> {}"
shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
proof -
@@ -2326,16 +2324,19 @@
proof
fix x assume "x\<in>S"
thus "x \<le> Sup S"
- by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
+ by (metis cSup_upper abs_le_D1 assms(1) bounded_real)
next
show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
- by (metis SupInf.Sup_least)
+ by (metis cSup_least)
qed
lemma Sup_insert:
fixes S :: "real set"
shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
-by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal)
+ apply (subst cSup_insert_If)
+ apply (rule bounded_has_Sup(1)[of S, rule_format])
+ apply (auto simp: sup_max)
+ done
lemma Sup_insert_finite:
fixes S :: "real set"
@@ -2352,16 +2353,19 @@
fix x assume "x\<in>S"
from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
thus "x \<ge> Inf S" using `x\<in>S`
- by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
+ by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
next
show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
- by (metis SupInf.Inf_greatest)
+ by (metis cInf_greatest)
qed
lemma Inf_insert:
fixes S :: "real set"
shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
-by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
+ apply (subst cInf_insert_if)
+ apply (rule bounded_has_Inf(1)[of S, rule_format])
+ apply (auto simp: inf_min)
+ done
lemma Inf_insert_finite:
fixes S :: "real set"
@@ -3125,7 +3129,7 @@
lemma cauchy_def:
"Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
-unfolding Cauchy_def by blast
+unfolding Cauchy_def by metis
fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
"helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
@@ -5197,7 +5201,7 @@
from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
unfolding bounded_def by auto
have "dist x y \<le> Sup ?D"
- proof (rule Sup_upper, safe)
+ proof (rule cSup_upper, safe)
fix a b assume "a \<in> s" "b \<in> s"
with z[of a] z[of b] dist_triangle[of a b z]
show "dist a b \<le> 2 * d"
@@ -5219,7 +5223,7 @@
by (auto simp: diameter_def)
then have "?D \<noteq> {}" by auto
ultimately have "Sup ?D \<le> d"
- by (intro Sup_least) (auto simp: not_less)
+ by (intro cSup_least) (auto simp: not_less)
with `d < diameter s` `s \<noteq> {}` show False
by (auto simp: diameter_def)
qed
@@ -5239,7 +5243,7 @@
then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
using compact_sup_maxdistance[OF assms] by auto
hence "diameter s \<le> dist x y"
- unfolding diameter_def by clarsimp (rule Sup_least, fast+)
+ unfolding diameter_def by clarsimp (rule cSup_least, fast+)
thus ?thesis
by (metis b diameter_bounded_bound order_antisym xys)
qed
@@ -6675,5 +6679,4 @@
declare tendsto_const [intro] (* FIXME: move *)
-
end
--- a/src/HOL/Probability/Probability_Measure.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Mar 22 10:41:43 2013 +0100
@@ -159,11 +159,11 @@
moreover
{ fix y assume y: "y \<in> I"
with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
- by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
+ by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
by simp
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
- proof (rule Sup_least)
+ proof (rule cSup_least)
show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
using `I \<noteq> {}` by auto
next
--- a/src/HOL/SupInf.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/SupInf.thy Fri Mar 22 10:41:43 2013 +0100
@@ -6,210 +6,341 @@
imports RComplete
begin
-instantiation real :: Sup
+lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
+ by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
+
+lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
+ by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
+
+text {*
+
+To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
+@{const Inf} in theorem names with c.
+
+*}
+
+class conditional_complete_lattice = lattice + Sup + Inf +
+ assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
+ and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
+ assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
+ and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
begin
-definition
- Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
+
+lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
+ "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
+ by (blast intro: antisym cSup_upper cSup_least)
+
+lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
+ "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
+ by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
+
+lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
+ by (metis order_trans cSup_upper cSup_least)
+
+lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
+ by (metis order_trans cInf_lower cInf_greatest)
+
+lemma cSup_singleton [simp]: "Sup {x} = x"
+ by (intro cSup_eq_maximum) auto
+
+lemma cInf_singleton [simp]: "Inf {x} = x"
+ by (intro cInf_eq_minimum) auto
+
+lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
+ "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
+ by (metis cSup_upper order_trans)
+
+lemma cInf_lower2:
+ "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+ by (metis cInf_lower order_trans)
+
+lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
+ by (blast intro: cSup_upper)
+
+lemma cInf_lower_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+ by (blast intro: cInf_lower)
+
+lemma cSup_eq_non_empty:
+ assumes 1: "X \<noteq> {}"
+ assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+ assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+ shows "Sup X = a"
+ by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
+
+lemma cInf_eq_non_empty:
+ assumes 1: "X \<noteq> {}"
+ assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+ assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+ shows "Inf X = a"
+ by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
+
+lemma cSup_insert:
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup (insert a X) = sup a (Sup X)"
+proof (intro cSup_eq_non_empty)
+ fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
+qed (auto intro: le_supI2 z cSup_upper)
-instance ..
+lemma cInf_insert:
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf (insert a X) = inf a (Inf X)"
+proof (intro cInf_eq_non_empty)
+ fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
+qed (auto intro: le_infI2 z cInf_lower)
+
+lemma cSup_insert_If:
+ "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
+ using cSup_insert[of X z] by simp
+
+lemma cInf_insert_if:
+ "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
+ using cInf_insert[of X z] by simp
+
+lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
+proof (induct X arbitrary: x rule: finite_induct)
+ case (insert x X y) then show ?case
+ apply (cases "X = {}")
+ apply simp
+ apply (subst cSup_insert[of _ "Sup X"])
+ apply (auto intro: le_supI2)
+ done
+qed simp
+
+lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
+proof (induct X arbitrary: x rule: finite_induct)
+ case (insert x X y) then show ?case
+ apply (cases "X = {}")
+ apply simp
+ apply (subst cInf_insert[of _ "Inf X"])
+ apply (auto intro: le_infI2)
+ done
+qed simp
+
+lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
+proof (induct X rule: finite_ne_induct)
+ case (insert x X) then show ?case
+ using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
+qed simp
+
+lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
+proof (induct X rule: finite_ne_induct)
+ case (insert x X) then show ?case
+ using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
+qed simp
+
+lemma cSup_atMost[simp]: "Sup {..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cInf_atLeast[simp]: "Inf {x..} = x"
+ by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
+ by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
+ by (auto intro!: cInf_eq_minimum)
+
end
-instantiation real :: Inf
+instance complete_lattice \<subseteq> conditional_complete_lattice
+ by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
+
+lemma isLub_cSup:
+ "(S::'a :: conditional_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 intro: cSup_upper cSup_least)
+
+lemma cSup_eq:
+ fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
+ assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+ assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+ shows "Sup X = a"
+proof cases
+ assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
+qed (intro cSup_eq_non_empty assms)
+
+lemma cInf_eq:
+ fixes a :: "'a :: {conditional_complete_lattice, no_top}"
+ assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+ assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+ shows "Inf X = a"
+proof cases
+ 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::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+ by (metis cSup_least setle_def)
+
+lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+ by (metis cInf_greatest setge_def)
+
+class conditional_complete_linorder = conditional_complete_lattice + linorder
begin
+
+lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
+ "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
+ by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
+
+lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> 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 less_cSupE:
+ assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
+ by (metis cSup_least assms not_le that)
+
+lemma complete_interval:
+ assumes "a < b" and "P a" and "\<not> P b"
+ shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
+ (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
+ show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by (rule cSup_upper [where z=b], auto)
+ (metis `a < b` `\<not> P b` linear less_le)
+next
+ show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
+ apply (rule cSup_least)
+ apply auto
+ apply (metis less_le_not_le)
+ apply (metis `a<b` `~ P b` linear less_le)
+ done
+next
+ fix x
+ assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ show "P x"
+ apply (rule less_cSupE [OF lt], auto)
+ apply (metis less_le_not_le)
+ apply (metis x)
+ done
+next
+ fix d
+ assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+ thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by (rule_tac z="b" in cSup_upper, auto)
+ (metis `a<b` `~ P b` linear less_le)
+qed
+
+end
+
+lemma cSup_unique: "(S::'a :: {conditional_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 :: {conditional_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_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
+ using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
+
+lemma cInf_eq_Min: "finite (X::'a::conditional_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_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq_non_empty intro: dense_le)
+
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
+ by (auto intro!: cInf_eq intro: dense_ge)
+
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+instantiation real :: conditional_complete_linorder
+begin
+
+subsection{*Supremum of a set of reals*}
+
definition
- Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
+ Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
+
+definition
+ Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
+
+instance
+proof
+ { fix z x :: real and X :: "real set"
+ assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ show "x \<le> Sup X"
+ proof (auto simp add: Sup_real_def)
+ from complete_real[of X]
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: x z)
+ hence "x \<le> s"
+ by (blast intro: x z)
+ also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
+ by (fast intro: Least_equality [symmetric])
+ finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
+ qed }
+ note Sup_upper = this
-instance ..
+ { fix z :: real and X :: "real set"
+ assume x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ show "Sup X \<le> z"
+ proof (auto simp add: Sup_real_def)
+ from complete_real x
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: z)
+ hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
+ by (best intro: Least_equality)
+ also with s z have "... \<le> z"
+ by blast
+ finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
+ qed }
+ note Sup_least = this
+
+ { fix x z :: real and X :: "real set"
+ assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ show "Inf X \<le> x"
+ proof -
+ have "-x \<le> Sup (uminus ` X)"
+ by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
+ thus ?thesis
+ by (auto simp add: Inf_real_def)
+ qed }
+
+ { fix z :: real and X :: "real set"
+ assume x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ show "z \<le> Inf X"
+ proof -
+ have "Sup (uminus ` X) \<le> -z"
+ using x z by (force intro: Sup_least)
+ hence "z \<le> - Sup (uminus ` X)"
+ by simp
+ thus ?thesis
+ by (auto simp add: Inf_real_def)
+ qed }
+qed
end
subsection{*Supremum of a set of reals*}
-lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
- fixes x :: real
- assumes x: "x \<in> X"
- and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "x \<le> Sup X"
-proof (auto simp add: Sup_real_def)
- from complete_real
- obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
- by (blast intro: x z)
- hence "x \<le> s"
- by (blast intro: x z)
- also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
- by (fast intro: Least_equality [symmetric])
- finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
-qed
-
-lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
- fixes z :: real
- assumes x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "Sup X \<le> z"
-proof (auto simp add: Sup_real_def)
- from complete_real x
- obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
- by (blast intro: z)
- hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
- by (best intro: Least_equality)
- also with s z have "... \<le> z"
- by blast
- finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
-qed
-
-lemma less_SupE:
- fixes y :: real
- assumes "y < Sup X" "X \<noteq> {}"
- obtains x where "x\<in>X" "y < x"
-by (metis SupInf.Sup_least assms linorder_not_less that)
-
-lemma Sup_singleton [simp]: "Sup {x::real} = x"
- by (force intro: Least_equality simp add: Sup_real_def)
-
-lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
- fixes z :: real
- assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "Sup X = z"
- by (force intro: Least_equality X z simp add: Sup_real_def)
-
-lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
- fixes x :: real
- shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
- by (metis Sup_upper order_trans)
-
-lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
- fixes z :: real
- shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
- by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)
-
-lemma Sup_eq:
- fixes a :: real
- shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
- \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
- by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
- insert_not_empty order_antisym)
-
-lemma Sup_le:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
-by (metis SupInf.Sup_least setle_def)
-
-lemma Sup_upper_EX:
- fixes x :: real
- shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
- by blast
-
-lemma Sup_insert_nonempty:
- fixes x :: real
- assumes x: "x \<in> X"
- and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "Sup (insert a X) = max a (Sup X)"
-proof (cases "Sup X \<le> a")
- case True
- thus ?thesis
- apply (simp add: max_def)
- apply (rule Sup_eq_maximum)
- apply (rule insertI1)
- apply (metis Sup_upper [OF _ z] insertE linear order_trans)
- done
-next
- case False
- hence 1:"a < Sup X" by simp
- have "Sup X \<le> Sup (insert a X)"
- apply (rule Sup_least)
- apply (metis ex_in_conv x)
- apply (rule Sup_upper_EX)
- apply blast
- apply (metis insert_iff linear order_trans z)
- done
- moreover
- have "Sup (insert a X) \<le> Sup X"
- apply (rule Sup_least)
- apply blast
- apply (metis False Sup_upper insertE linear z)
- done
- ultimately have "Sup (insert a X) = Sup X"
- by (blast intro: antisym )
- thus ?thesis
- by (metis 1 min_max.le_iff_sup less_le)
-qed
-
-lemma Sup_insert_if:
- fixes X :: "real set"
- assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
-by auto (metis Sup_insert_nonempty z)
-
-lemma Sup:
- fixes S :: "real set"
- shows "S \<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)
-
-lemma Sup_finite_Max:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "Sup S = Max S"
-using fS Se
-proof-
- let ?m = "Max S"
- from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
- with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
- from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- moreover
- have "Sup S \<le> ?m" using Sm lub
- by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
- ultimately show ?thesis by arith
-qed
-
-lemma Sup_finite_in:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "Sup S \<in> S"
- using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
-
-lemma Sup_finite_ge_iff:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
-
-lemma Sup_finite_le_iff:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
-
-lemma Sup_finite_gt_iff:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
-by (metis Se Sup_finite_le_iff fS linorder_not_less)
-
-lemma Sup_finite_lt_iff:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
-by (metis Se Sup_finite_ge_iff fS linorder_not_less)
-
-lemma Sup_unique:
- fixes S :: "real set"
- shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
-unfolding setle_def
-apply (rule Sup_eq, auto)
-apply (metis linorder_not_less)
-done
-
-lemma Sup_abs_le:
+lemma cSup_abs_le:
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
-by (auto simp add: abs_le_interval_iff) (metis Sup_upper2)
+by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2)
-lemma Sup_bounds:
+lemma cSup_bounds:
fixes S :: "real 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 Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+ 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
@@ -219,203 +350,66 @@
with b show ?thesis by blast
qed
-lemma Sup_asclose:
+lemma cSup_asclose:
fixes S :: "real set"
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
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
- thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
+ thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
by (auto simp add: setge_def setle_def)
qed
-lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"
- by (auto intro!: Sup_eq intro: dense_le)
-
-lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)"
- by (auto intro!: Sup_eq intro: dense_le_bounded)
-
-lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)"
- by (auto intro!: Sup_eq intro: dense_le_bounded)
-
-lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"
- by (auto intro!: Sup_eq_maximum)
-
-lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)"
- by (auto intro!: Sup_eq_maximum)
-
-lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)"
- by (auto intro!: Sup_eq_maximum)
-
-
subsection{*Infimum of a set of reals*}
-lemma Inf_lower [intro]:
- fixes z :: real
- assumes x: "x \<in> X"
- and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "Inf X \<le> x"
-proof -
- have "-x \<le> Sup (uminus ` X)"
- by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
- thus ?thesis
- by (auto simp add: Inf_real_def)
-qed
-
-lemma Inf_greatest [intro]:
+lemma cInf_greater:
fixes z :: real
- assumes x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "z \<le> Inf X"
-proof -
- have "Sup (uminus ` X) \<le> -z" using x z by force
- hence "z \<le> - Sup (uminus ` X)"
- by simp
- thus ?thesis
- by (auto simp add: Inf_real_def)
-qed
-
-lemma Inf_singleton [simp]: "Inf {x::real} = x"
- by (simp add: Inf_real_def)
-
-lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
- fixes z :: real
- assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "Inf X = z"
-proof -
- have "Sup (uminus ` X) = -z" using x z
- by (force intro: Sup_eq_maximum x z)
- thus ?thesis
- by (simp add: Inf_real_def)
-qed
-
-lemma Inf_lower2:
- fixes x :: real
- shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
- by (metis Inf_lower order_trans)
-
-lemma Inf_real_iff:
- fixes z :: real
- shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
- by (metis Inf_greatest Inf_lower less_le_not_le linear
- order_less_le_trans)
+ shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
+ by (metis cInf_less_iff not_leE)
-lemma Inf_eq:
- fixes a :: real
- shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
- by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
- insert_absorb insert_not_empty order_antisym)
-
-lemma Inf_ge:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
-by (metis SupInf.Inf_greatest setge_def)
-
-lemma Inf_lower_EX:
- fixes x :: real
- shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
- by blast
-
-lemma Inf_insert_nonempty:
- fixes x :: real
- assumes x: "x \<in> X"
- and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "Inf (insert a X) = min a (Inf X)"
-proof (cases "a \<le> Inf X")
- case True
- thus ?thesis
- by (simp add: min_def)
- (blast intro: Inf_eq_minimum order_trans z)
-next
- case False
- hence 1:"Inf X < a" by simp
- have "Inf (insert a X) \<le> Inf X"
- apply (rule Inf_greatest)
- apply (metis ex_in_conv x)
- apply (rule Inf_lower_EX)
- apply (erule insertI2)
- apply (metis insert_iff linear order_trans z)
- done
- moreover
- have "Inf X \<le> Inf (insert a X)"
- apply (rule Inf_greatest)
- apply blast
- apply (metis False Inf_lower insertE linear z)
- done
- ultimately have "Inf (insert a X) = Inf X"
- by (blast intro: antisym )
- thus ?thesis
- by (metis False min_max.inf_absorb2 linear)
-qed
-
-lemma Inf_insert_if:
- fixes X :: "real set"
- assumes z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
-by auto (metis Inf_insert_nonempty z)
-
-lemma Inf_greater:
- fixes z :: real
- shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
- by (metis Inf_real_iff not_leE)
-
-lemma Inf_close:
+lemma cInf_close:
fixes e :: real
shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
- by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
+ by (metis add_strict_increasing add_commute cInf_greater linorder_not_le pos_add_strict)
-lemma Inf_finite_Min:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
-by (simp add: Inf_real_def Sup_finite_Max image_image)
-
-lemma Inf_finite_in:
+lemma cInf_finite_in:
fixes S :: "real set"
assumes fS: "finite S" and Se: "S \<noteq> {}"
shows "Inf S \<in> S"
- using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
+ using cInf_eq_Min[OF fS Se] Min_in[OF fS Se] by metis
-lemma Inf_finite_ge_iff:
+lemma cInf_finite_ge_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
+by (metis cInf_eq_Min cInf_finite_in Min_le order_trans)
-lemma Inf_finite_le_iff:
+lemma cInf_finite_le_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
-by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
- order_antisym linear)
+by (metis cInf_eq_Min cInf_finite_ge_iff cInf_finite_in Min_le order_antisym linear)
-lemma Inf_finite_gt_iff:
+lemma cInf_finite_gt_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
-by (metis Inf_finite_le_iff linorder_not_less)
+by (metis cInf_finite_le_iff linorder_not_less)
-lemma Inf_finite_lt_iff:
+lemma cInf_finite_lt_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
-by (metis Inf_finite_ge_iff linorder_not_less)
+by (metis cInf_finite_ge_iff linorder_not_less)
-lemma Inf_unique:
- fixes S :: "real set"
- shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
-unfolding setge_def
-apply (rule Inf_eq, auto)
-apply (metis less_le_not_le linorder_not_less)
-done
-
-lemma Inf_abs_ge:
+lemma cInf_abs_ge:
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
-by (simp add: Inf_real_def) (rule Sup_abs_le, auto)
+by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
-lemma Inf_asclose:
+lemma cInf_asclose:
fixes S :: "real set"
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
proof -
have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>"
by auto
also have "... \<le> e"
- apply (rule Sup_asclose)
+ apply (rule cSup_asclose)
apply (auto simp add: S)
apply (metis abs_minus_add_cancel b add_commute diff_minus)
done
@@ -424,73 +418,16 @@
by (simp add: Inf_real_def)
qed
-lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)"
- by (simp add: Inf_real_def)
-
-lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)"
- by (simp add: Inf_real_def)
-
-lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"
- by (simp add: Inf_real_def)
-
-lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)"
- by (simp add: Inf_real_def)
-
-lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)"
- by (simp add: Inf_real_def)
-
subsection{*Relate max and min to Sup and Inf.*}
-lemma real_max_Sup:
+lemma real_max_cSup:
fixes x :: real
shows "max x y = Sup {x,y}"
-proof-
- have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff)
- moreover
- have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)
- ultimately show ?thesis by arith
-qed
+ by (subst cSup_insert[of _ y]) (simp_all add: sup_max)
-lemma real_min_Inf:
+lemma real_min_cInf:
fixes x :: real
shows "min x y = Inf {x,y}"
-proof-
- have "Inf {x,y} \<le> min x y" by (simp add: linorder_linear Inf_finite_le_iff)
- moreover
- have "min x y \<le> Inf {x,y}" by (simp add: Inf_finite_ge_iff)
- ultimately show ?thesis by arith
-qed
-
-lemma reals_complete_interval:
- fixes a::real and b::real
- assumes "a < b" and "P a" and "~P b"
- shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
- (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
-proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
- show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- by (rule SupInf.Sup_upper [where z=b], auto)
- (metis `a < b` `\<not> P b` linear less_le)
-next
- show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
- apply (rule SupInf.Sup_least)
- apply (auto simp add: )
- apply (metis less_le_not_le)
- apply (metis `a<b` `~ P b` linear less_le)
- done
-next
- fix x
- assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- show "P x"
- apply (rule less_SupE [OF lt], auto)
- apply (metis less_le_not_le)
- apply (metis x)
- done
-next
- fix d
- assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
- thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- by (rule_tac z="b" in SupInf.Sup_upper, auto)
- (metis `a<b` `~ P b` linear less_le)
-qed
+ by (subst cInf_insert[of _ y]) (simp_all add: inf_min)
end