1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:44:57 2013 +0100
1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:44:58 2013 +0100
1.3 @@ -1,6 +1,7 @@
1.4 (* Title: HOL/Conditionally_Complete_Lattices.thy
1.5 Author: Amine Chaieb and L C Paulson, University of Cambridge
1.6 Author: Johannes Hölzl, TU München
1.7 + Author: Luke S. Serafin, Carnegie Mellon University
1.8 *)
1.9
1.10 header {* Conditionally-complete Lattices *}
1.11 @@ -15,6 +16,118 @@
1.12 lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
1.13 by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
1.14
1.15 +context preorder
1.16 +begin
1.17 +
1.18 +definition "bdd_above A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<le> M)"
1.19 +definition "bdd_below A \<longleftrightarrow> (\<exists>m. \<forall>x \<in> A. m \<le> x)"
1.20 +
1.21 +lemma bdd_aboveI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A"
1.22 + by (auto simp: bdd_above_def)
1.23 +
1.24 +lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
1.25 + by (auto simp: bdd_below_def)
1.26 +
1.27 +lemma bdd_above_empty [simp, intro]: "bdd_above {}"
1.28 + unfolding bdd_above_def by auto
1.29 +
1.30 +lemma bdd_below_empty [simp, intro]: "bdd_below {}"
1.31 + unfolding bdd_below_def by auto
1.32 +
1.33 +lemma bdd_above_mono: "bdd_above B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_above A"
1.34 + by (metis (full_types) bdd_above_def order_class.le_neq_trans psubsetD)
1.35 +
1.36 +lemma bdd_below_mono: "bdd_below B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_below A"
1.37 + by (metis bdd_below_def order_class.le_neq_trans psubsetD)
1.38 +
1.39 +lemma bdd_above_Int1 [simp]: "bdd_above A \<Longrightarrow> bdd_above (A \<inter> B)"
1.40 + using bdd_above_mono by auto
1.41 +
1.42 +lemma bdd_above_Int2 [simp]: "bdd_above B \<Longrightarrow> bdd_above (A \<inter> B)"
1.43 + using bdd_above_mono by auto
1.44 +
1.45 +lemma bdd_below_Int1 [simp]: "bdd_below A \<Longrightarrow> bdd_below (A \<inter> B)"
1.46 + using bdd_below_mono by auto
1.47 +
1.48 +lemma bdd_below_Int2 [simp]: "bdd_below B \<Longrightarrow> bdd_below (A \<inter> B)"
1.49 + using bdd_below_mono by auto
1.50 +
1.51 +lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}"
1.52 + by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le)
1.53 +
1.54 +lemma bdd_above_Ico [simp, intro]: "bdd_above {a ..< b}"
1.55 + by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le)
1.56 +
1.57 +lemma bdd_above_Iio [simp, intro]: "bdd_above {..< b}"
1.58 + by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)
1.59 +
1.60 +lemma bdd_above_Ioc [simp, intro]: "bdd_above {a <.. b}"
1.61 + by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)
1.62 +
1.63 +lemma bdd_above_Icc [simp, intro]: "bdd_above {a .. b}"
1.64 + by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)
1.65 +
1.66 +lemma bdd_above_Iic [simp, intro]: "bdd_above {.. b}"
1.67 + by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)
1.68 +
1.69 +lemma bdd_below_Ioo [simp, intro]: "bdd_below {a <..< b}"
1.70 + by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le)
1.71 +
1.72 +lemma bdd_below_Ioc [simp, intro]: "bdd_below {a <.. b}"
1.73 + by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le)
1.74 +
1.75 +lemma bdd_below_Ioi [simp, intro]: "bdd_below {a <..}"
1.76 + by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)
1.77 +
1.78 +lemma bdd_below_Ico [simp, intro]: "bdd_below {a ..< b}"
1.79 + by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)
1.80 +
1.81 +lemma bdd_below_Icc [simp, intro]: "bdd_below {a .. b}"
1.82 + by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)
1.83 +
1.84 +lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}"
1.85 + by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)
1.86 +
1.87 +end
1.88 +
1.89 +context lattice
1.90 +begin
1.91 +
1.92 +lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A"
1.93 + by (auto simp: bdd_above_def intro: le_supI2 sup_ge1)
1.94 +
1.95 +lemma bdd_below_insert [simp]: "bdd_below (insert a A) = bdd_below A"
1.96 + by (auto simp: bdd_below_def intro: le_infI2 inf_le1)
1.97 +
1.98 +lemma bdd_finite [simp]:
1.99 + assumes "finite A" shows bdd_above_finite: "bdd_above A" and bdd_below_finite: "bdd_below A"
1.100 + using assms by (induct rule: finite_induct, auto)
1.101 +
1.102 +lemma bdd_above_Un [simp]: "bdd_above (A \<union> B) = (bdd_above A \<and> bdd_above B)"
1.103 +proof
1.104 + assume "bdd_above (A \<union> B)"
1.105 + thus "bdd_above A \<and> bdd_above B" unfolding bdd_above_def by auto
1.106 +next
1.107 + assume "bdd_above A \<and> bdd_above B"
1.108 + then obtain a b where "\<forall>x\<in>A. x \<le> a" "\<forall>x\<in>B. x \<le> b" unfolding bdd_above_def by auto
1.109 + hence "\<forall>x \<in> A \<union> B. x \<le> sup a b" by (auto intro: Un_iff le_supI1 le_supI2)
1.110 + thus "bdd_above (A \<union> B)" unfolding bdd_above_def ..
1.111 +qed
1.112 +
1.113 +lemma bdd_below_Un [simp]: "bdd_below (A \<union> B) = (bdd_below A \<and> bdd_below B)"
1.114 +proof
1.115 + assume "bdd_below (A \<union> B)"
1.116 + thus "bdd_below A \<and> bdd_below B" unfolding bdd_below_def by auto
1.117 +next
1.118 + assume "bdd_below A \<and> bdd_below B"
1.119 + then obtain a b where "\<forall>x\<in>A. a \<le> x" "\<forall>x\<in>B. b \<le> x" unfolding bdd_below_def by auto
1.120 + hence "\<forall>x \<in> A \<union> B. inf a b \<le> x" by (auto intro: Un_iff le_infI1 le_infI2)
1.121 + thus "bdd_below (A \<union> B)" unfolding bdd_below_def ..
1.122 +qed
1.123 +
1.124 +end
1.125 +
1.126 +
1.127 text {*
1.128
1.129 To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
1.130 @@ -23,24 +136,22 @@
1.131 *}
1.132
1.133 class conditionally_complete_lattice = lattice + Sup + Inf +
1.134 - assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
1.135 + assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x"
1.136 and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
1.137 - assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
1.138 + assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X"
1.139 and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
1.140 begin
1.141
1.142 -lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
1.143 - "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
1.144 - by (blast intro: antisym cSup_upper cSup_least)
1.145 +lemma cSup_eq_maximum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
1.146 + by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto
1.147
1.148 -lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
1.149 - "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
1.150 - by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
1.151 +lemma cInf_eq_minimum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
1.152 + by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto
1.153
1.154 -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)"
1.155 +lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
1.156 by (metis order_trans cSup_upper cSup_least)
1.157
1.158 -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)"
1.159 +lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
1.160 by (metis order_trans cInf_lower cInf_greatest)
1.161
1.162 lemma cSup_singleton [simp]: "Sup {x} = x"
1.163 @@ -49,20 +160,12 @@
1.164 lemma cInf_singleton [simp]: "Inf {x} = x"
1.165 by (intro cInf_eq_minimum) auto
1.166
1.167 -lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
1.168 - "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
1.169 +lemma cSup_upper2: "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> bdd_above X \<Longrightarrow> y \<le> Sup X"
1.170 by (metis cSup_upper order_trans)
1.171
1.172 -lemma cInf_lower2:
1.173 - "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
1.174 +lemma cInf_lower2: "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> y"
1.175 by (metis cInf_lower order_trans)
1.176
1.177 -lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
1.178 - by (blast intro: cSup_upper)
1.179 -
1.180 -lemma cInf_lower_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
1.181 - by (blast intro: cInf_lower)
1.182 -
1.183 lemma cSup_eq_non_empty:
1.184 assumes 1: "X \<noteq> {}"
1.185 assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
1.186 @@ -77,67 +180,41 @@
1.187 shows "Inf X = a"
1.188 by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
1.189
1.190 -lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
1.191 - by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least)
1.192 +lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
1.193 + by (rule cInf_eq_non_empty) (auto intro!: cSup_upper cSup_least simp: bdd_below_def)
1.194
1.195 -lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}"
1.196 - by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest)
1.197 +lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}"
1.198 + by (rule cSup_eq_non_empty) (auto intro!: cInf_lower cInf_greatest simp: bdd_above_def)
1.199
1.200 -lemma cSup_insert:
1.201 - assumes x: "X \<noteq> {}"
1.202 - and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
1.203 - shows "Sup (insert a X) = sup a (Sup X)"
1.204 -proof (intro cSup_eq_non_empty)
1.205 - 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)
1.206 -qed (auto intro: le_supI2 z cSup_upper)
1.207 +lemma cSup_insert: "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> Sup (insert a X) = sup a (Sup X)"
1.208 + by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least)
1.209
1.210 -lemma cInf_insert:
1.211 - assumes x: "X \<noteq> {}"
1.212 - and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
1.213 - shows "Inf (insert a X) = inf a (Inf X)"
1.214 -proof (intro cInf_eq_non_empty)
1.215 - 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)
1.216 -qed (auto intro: le_infI2 z cInf_lower)
1.217 +lemma cInf_insert: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf (insert a X) = inf a (Inf X)"
1.218 + by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest)
1.219
1.220 -lemma cSup_insert_If:
1.221 - "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
1.222 - using cSup_insert[of X z] by simp
1.223 +lemma cSup_insert_If: "bdd_above X \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
1.224 + using cSup_insert[of X] by simp
1.225
1.226 -lemma cInf_insert_if:
1.227 - "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
1.228 - using cInf_insert[of X z] by simp
1.229 +lemma cInf_insert_if: "bdd_below X \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
1.230 + using cInf_insert[of X] by simp
1.231
1.232 lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
1.233 proof (induct X arbitrary: x rule: finite_induct)
1.234 case (insert x X y) then show ?case
1.235 - apply (cases "X = {}")
1.236 - apply simp
1.237 - apply (subst cSup_insert[of _ "Sup X"])
1.238 - apply (auto intro: le_supI2)
1.239 - done
1.240 + by (cases "X = {}") (auto simp: cSup_insert intro: le_supI2)
1.241 qed simp
1.242
1.243 lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
1.244 proof (induct X arbitrary: x rule: finite_induct)
1.245 case (insert x X y) then show ?case
1.246 - apply (cases "X = {}")
1.247 - apply simp
1.248 - apply (subst cInf_insert[of _ "Inf X"])
1.249 - apply (auto intro: le_infI2)
1.250 - done
1.251 + by (cases "X = {}") (auto simp: cInf_insert intro: le_infI2)
1.252 qed simp
1.253
1.254 lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
1.255 -proof (induct X rule: finite_ne_induct)
1.256 - case (insert x X) then show ?case
1.257 - using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
1.258 -qed simp
1.259 + by (induct X rule: finite_ne_induct) (simp_all add: cSup_insert)
1.260
1.261 lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
1.262 -proof (induct X rule: finite_ne_induct)
1.263 - case (insert x X) then show ?case
1.264 - using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
1.265 -qed simp
1.266 + by (induct X rule: finite_ne_induct) (simp_all add: cInf_insert)
1.267
1.268 lemma cSup_atMost[simp]: "Sup {..x} = x"
1.269 by (auto intro!: cSup_eq_maximum)
1.270 @@ -165,7 +242,7 @@
1.271 lemma isLub_cSup:
1.272 "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
1.273 by (auto simp add: isLub_def setle_def leastP_def isUb_def
1.274 - intro!: setgeI intro: cSup_upper cSup_least)
1.275 + intro!: setgeI cSup_upper cSup_least)
1.276
1.277 lemma cSup_eq:
1.278 fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
1.279 @@ -195,10 +272,10 @@
1.280 begin
1.281
1.282 lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
1.283 - "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
1.284 + "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
1.285 by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
1.286
1.287 -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)"
1.288 +lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
1.289 by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
1.290
1.291 lemma less_cSupE:
1.292 @@ -207,11 +284,11 @@
1.293
1.294 lemma less_cSupD:
1.295 "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
1.296 - by (metis less_cSup_iff not_leE)
1.297 + by (metis less_cSup_iff not_leE bdd_above_def)
1.298
1.299 lemma cInf_lessD:
1.300 "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
1.301 - by (metis cInf_less_iff not_leE)
1.302 + by (metis cInf_less_iff not_leE bdd_below_def)
1.303
1.304 lemma complete_interval:
1.305 assumes "a < b" and "P a" and "\<not> P b"
1.306 @@ -219,7 +296,7 @@
1.307 (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
1.308 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
1.309 show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.310 - by (rule cSup_upper [where z=b], auto)
1.311 + by (rule cSup_upper, auto simp: bdd_above_def)
1.312 (metis `a < b` `\<not> P b` linear less_le)
1.313 next
1.314 show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
1.315 @@ -240,7 +317,7 @@
1.316 fix d
1.317 assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
1.318 thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.319 - by (rule_tac z="b" in cSup_upper, auto)
1.320 + by (rule_tac cSup_upper, auto simp: bdd_above_def)
1.321 (metis `a<b` `~ P b` linear less_le)
1.322 qed
1.323
2.1 --- a/src/HOL/Library/FSet.thy Tue Nov 05 09:44:57 2013 +0100
2.2 +++ b/src/HOL/Library/FSet.thy Tue Nov 05 09:44:58 2013 +0100
2.3 @@ -101,19 +101,25 @@
2.4 lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)"
2.5 by (auto intro: finite_subset)
2.6
2.7 +lemma transfer_bdd_below[transfer_rule]: "(set_rel (pcr_fset op =) ===> op =) bdd_below bdd_below"
2.8 + by auto
2.9 +
2.10 instance
2.11 proof
2.12 fix x z :: "'a fset"
2.13 fix X :: "'a fset set"
2.14 {
2.15 - assume "x \<in> X" "(\<And>a. a \<in> X \<Longrightarrow> z |\<subseteq>| a)"
2.16 + assume "x \<in> X" "bdd_below X"
2.17 then show "Inf X |\<subseteq>| x" by transfer auto
2.18 next
2.19 assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)"
2.20 then show "z |\<subseteq>| Inf X" by transfer (clarsimp, blast)
2.21 next
2.22 - assume "x \<in> X" "(\<And>a. a \<in> X \<Longrightarrow> a |\<subseteq>| z)"
2.23 - then show "x |\<subseteq>| Sup X" by transfer (auto intro!: finite_Sup)
2.24 + assume "x \<in> X" "bdd_above X"
2.25 + then obtain z where "x \<in> X" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)"
2.26 + by (auto simp: bdd_above_def)
2.27 + then show "x |\<subseteq>| Sup X"
2.28 + by transfer (auto intro!: finite_Sup)
2.29 next
2.30 assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)"
2.31 then show "Sup X |\<subseteq>| z" by transfer (clarsimp, blast)
3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:44:57 2013 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:44:58 2013 +0100
3.3 @@ -8724,7 +8724,7 @@
3.4 using interior_subset[of I] `x \<in> interior I` by auto
3.5
3.6 have "Inf (?F x) \<le> (f x - f y) / (x - y)"
3.7 - proof (rule cInf_lower2)
3.8 + proof (intro bdd_belowI cInf_lower2)
3.9 show "(f x - f t) / (x - t) \<in> ?F x"
3.10 using `t \<in> I` `x < t` by auto
3.11 show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
4.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 09:44:57 2013 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 09:44:58 2013 +0100
4.3 @@ -660,7 +660,7 @@
4.4 assume "S \<noteq> {}"
4.5 { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
4.6 then have *: "\<forall>x\<in>S. Inf S \<le> x"
4.7 - using cInf_lower_EX[of _ S] ex by metis
4.8 + using cInf_lower[of _ S] ex by (metis bdd_below_def)
4.9 then have "Inf S \<in> S"
4.10 apply (subst closed_contains_Inf)
4.11 using ex `S \<noteq> {}` `closed S`
5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:44:57 2013 +0100
5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:44:58 2013 +0100
5.3 @@ -13,7 +13,7 @@
5.4 lemma cSup_abs_le: (* TODO: is this really needed? *)
5.5 fixes S :: "real set"
5.6 shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
5.7 - by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2)
5.8 + by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)
5.9
5.10 lemma cInf_abs_ge: (* TODO: is this really needed? *)
5.11 fixes S :: "real set"
5.12 @@ -86,7 +86,7 @@
5.13 apply (insert assms)
5.14 apply (erule exE)
5.15 apply (rule_tac x = b in exI)
5.16 - apply (auto simp: isLb_def setge_def intro: cInf_lower cInf_greatest)
5.17 + apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
5.18 done
5.19
5.20 lemma real_ge_sup_subset:
5.21 @@ -100,7 +100,7 @@
5.22 apply (insert assms)
5.23 apply (erule exE)
5.24 apply (rule_tac x = b in exI)
5.25 - apply (auto simp: isUb_def setle_def intro: cSup_upper cSup_least)
5.26 + apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
5.27 done
5.28
5.29 (*declare not_less[simp] not_le[simp]*)
5.30 @@ -12728,8 +12728,8 @@
5.31 assume x: "x \<in> s"
5.32 have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
5.33 show "Inf {f j x |j. n \<le> j} \<le> f n x"
5.34 - apply (rule cInf_lower[where z="- h x"])
5.35 - defer
5.36 + apply (intro cInf_lower bdd_belowI)
5.37 + apply auto []
5.38 apply (rule *)
5.39 using assms(3)[rule_format,OF x]
5.40 unfolding real_norm_def abs_le_iff
5.41 @@ -12741,8 +12741,7 @@
5.42 fix x
5.43 assume x: "x \<in> s"
5.44 show "f n x \<le> Sup {f j x |j. n \<le> j}"
5.45 - apply (rule cSup_upper[where z="h x"])
5.46 - defer
5.47 + apply (rule cSup_upper)
5.48 using assms(3)[rule_format,OF x]
5.49 unfolding real_norm_def abs_le_iff
5.50 apply auto
6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:44:57 2013 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:44:58 2013 +0100
6.3 @@ -1909,17 +1909,17 @@
6.4
6.5 lemma closure_contains_Inf:
6.6 fixes S :: "real set"
6.7 - assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
6.8 + assumes "S \<noteq> {}" "bdd_below S"
6.9 shows "Inf S \<in> closure S"
6.10 proof -
6.11 have *: "\<forall>x\<in>S. Inf S \<le> x"
6.12 - using cInf_lower_EX[of _ S] assms by metis
6.13 + using cInf_lower[of _ S] assms by metis
6.14 {
6.15 fix e :: real
6.16 assume "e > 0"
6.17 then have "Inf S < Inf S + e" by simp
6.18 with assms obtain x where "x \<in> S" "x < Inf S + e"
6.19 - by (subst (asm) cInf_less_iff[of _ B]) auto
6.20 + by (subst (asm) cInf_less_iff) auto
6.21 with * have "\<exists>x\<in>S. dist x (Inf S) < e"
6.22 by (intro bexI[of _ x]) (auto simp add: dist_real_def)
6.23 }
6.24 @@ -1928,12 +1928,9 @@
6.25
6.26 lemma closed_contains_Inf:
6.27 fixes S :: "real set"
6.28 - assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
6.29 - and "closed S"
6.30 - shows "Inf S \<in> S"
6.31 + shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
6.32 by (metis closure_contains_Inf closure_closed assms)
6.33
6.34 -
6.35 lemma not_trivial_limit_within_ball:
6.36 "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
6.37 (is "?lhs = ?rhs")
6.38 @@ -1977,27 +1974,20 @@
6.39
6.40 definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
6.41
6.42 +lemma bdd_below_infdist[intro, simp]: "bdd_below {dist x a|a. a \<in> A}"
6.43 + by (auto intro!: zero_le_dist)
6.44 +
6.45 lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
6.46 by (simp add: infdist_def)
6.47
6.48 lemma infdist_nonneg: "0 \<le> infdist x A"
6.49 by (auto simp add: infdist_def intro: cInf_greatest)
6.50
6.51 -lemma infdist_le:
6.52 - assumes "a \<in> A"
6.53 - and "d = dist x a"
6.54 - shows "infdist x A \<le> d"
6.55 - using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
6.56 -
6.57 -lemma infdist_zero[simp]:
6.58 - assumes "a \<in> A"
6.59 - shows "infdist a A = 0"
6.60 -proof -
6.61 - from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0"
6.62 - by auto
6.63 - with infdist_nonneg[of a A] assms show "infdist a A = 0"
6.64 - by auto
6.65 -qed
6.66 +lemma infdist_le: "a \<in> A \<Longrightarrow> d = dist x a \<Longrightarrow> infdist x A \<le> d"
6.67 + using assms by (auto intro: cInf_lower simp add: infdist_def)
6.68 +
6.69 +lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
6.70 + by (auto intro!: antisym infdist_nonneg infdist_le)
6.71
6.72 lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
6.73 proof (cases "A = {}")
6.74 @@ -2021,13 +2011,7 @@
6.75 using `a \<in> A` by auto
6.76 show "dist x a \<le> d"
6.77 unfolding d by (rule dist_triangle)
6.78 - fix d
6.79 - assume "d \<in> {dist x a |a. a \<in> A}"
6.80 - then obtain a where "a \<in> A" "d = dist x a"
6.81 - by auto
6.82 - then show "infdist x A \<le> d"
6.83 - by (rule infdist_le)
6.84 - qed
6.85 + qed simp
6.86 qed
6.87 also have "\<dots> = dist x y + infdist y A"
6.88 proof (rule cInf_eq, safe)
6.89 @@ -2651,11 +2635,19 @@
6.90
6.91 text{* Some theorems on sups and infs using the notion "bounded". *}
6.92
6.93 -lemma bounded_real:
6.94 - fixes S :: "real set"
6.95 - shows "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x \<le> a)"
6.96 +lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
6.97 by (simp add: bounded_iff)
6.98
6.99 +lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
6.100 + by (auto simp: bounded_def bdd_above_def dist_real_def)
6.101 + (metis abs_le_D1 abs_minus_commute diff_le_eq)
6.102 +
6.103 +lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
6.104 + by (auto simp: bounded_def bdd_below_def dist_real_def)
6.105 + (metis abs_le_D1 add_commute diff_le_eq)
6.106 +
6.107 +(* TODO: remove the following lemmas about Inf and Sup, is now in conditionally complete lattice *)
6.108 +
6.109 lemma bounded_has_Sup:
6.110 fixes S :: "real set"
6.111 assumes "bounded S"
6.112 @@ -2663,22 +2655,14 @@
6.113 shows "\<forall>x\<in>S. x \<le> Sup S"
6.114 and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
6.115 proof
6.116 - fix x
6.117 - assume "x\<in>S"
6.118 - then show "x \<le> Sup S"
6.119 - by (metis cSup_upper abs_le_D1 assms(1) bounded_real)
6.120 -next
6.121 show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
6.122 using assms by (metis cSup_least)
6.123 -qed
6.124 +qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
6.125
6.126 lemma Sup_insert:
6.127 fixes S :: "real set"
6.128 shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
6.129 - apply (subst cSup_insert_If)
6.130 - apply (rule bounded_has_Sup(1)[of S, rule_format])
6.131 - apply (auto simp: sup_max)
6.132 - done
6.133 + by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
6.134
6.135 lemma Sup_insert_finite:
6.136 fixes S :: "real set"
6.137 @@ -2695,24 +2679,14 @@
6.138 shows "\<forall>x\<in>S. x \<ge> Inf S"
6.139 and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
6.140 proof
6.141 - fix x
6.142 - assume "x \<in> S"
6.143 - from assms(1) obtain a where a: "\<forall>x\<in>S. \<bar>x\<bar> \<le> a"
6.144 - unfolding bounded_real by auto
6.145 - then show "x \<ge> Inf S" using `x \<in> S`
6.146 - by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
6.147 -next
6.148 show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
6.149 using assms by (metis cInf_greatest)
6.150 -qed
6.151 +qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
6.152
6.153 lemma Inf_insert:
6.154 fixes S :: "real set"
6.155 shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
6.156 - apply (subst cInf_insert_if)
6.157 - apply (rule bounded_has_Inf(1)[of S, rule_format])
6.158 - apply (auto simp: inf_min)
6.159 - done
6.160 + by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_if)
6.161
6.162 lemma Inf_insert_finite:
6.163 fixes S :: "real set"
6.164 @@ -5738,12 +5712,16 @@
6.165 from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
6.166 unfolding bounded_def by auto
6.167 have "dist x y \<le> Sup ?D"
6.168 - proof (rule cSup_upper, safe)
6.169 - fix a b
6.170 - assume "a \<in> s" "b \<in> s"
6.171 - with z[of a] z[of b] dist_triangle[of a b z]
6.172 - show "dist a b \<le> 2 * d"
6.173 - by (simp add: dist_commute)
6.174 + proof (rule cSup_upper)
6.175 + show "bdd_above ?D"
6.176 + unfolding bdd_above_def
6.177 + proof (safe intro!: exI)
6.178 + fix a b
6.179 + assume "a \<in> s" "b \<in> s"
6.180 + with z[of a] z[of b] dist_triangle[of a b z]
6.181 + show "dist a b \<le> 2 * d"
6.182 + by (simp add: dist_commute)
6.183 + qed
6.184 qed (insert s, auto)
6.185 with `x \<in> s` show ?thesis
6.186 by (auto simp add: diameter_def)
7.1 --- a/src/HOL/Real.thy Tue Nov 05 09:44:57 2013 +0100
7.2 +++ b/src/HOL/Real.thy Tue Nov 05 09:44:58 2013 +0100
7.3 @@ -919,6 +919,12 @@
7.4 using 1 2 3 by (rule_tac x="Real B" in exI, simp)
7.5 qed
7.6
7.7 +(* TODO: generalize to ordered group *)
7.8 +lemma bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below (X::real set)"
7.9 + by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
7.10 +
7.11 +lemma bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above (X::real set)"
7.12 + by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
7.13
7.14 instantiation real :: linear_continuum
7.15 begin
7.16 @@ -933,10 +939,10 @@
7.17
7.18 instance
7.19 proof
7.20 - { fix z x :: real and X :: "real set"
7.21 - assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
7.22 + { fix x :: real and X :: "real set"
7.23 + assume x: "x \<in> X" "bdd_above X"
7.24 then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
7.25 - using complete_real[of X] by blast
7.26 + using complete_real[of X] unfolding bdd_above_def by blast
7.27 then show "x \<le> Sup X"
7.28 unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
7.29 note Sup_upper = this
7.30 @@ -953,9 +959,9 @@
7.31 note Sup_least = this
7.32
7.33 { fix x z :: real and X :: "real set"
7.34 - assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
7.35 + assume x: "x \<in> X" and [simp]: "bdd_below X"
7.36 have "-x \<le> Sup (uminus ` X)"
7.37 - by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
7.38 + by (rule Sup_upper) (auto simp add: image_iff x)
7.39 then show "Inf X \<le> x"
7.40 by (auto simp add: Inf_real_def) }
7.41
7.42 @@ -976,7 +982,7 @@
7.43 *}
7.44
7.45 lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
7.46 - by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
7.47 + by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
7.48
7.49
7.50 subsection {* Hiding implementation details *}
8.1 --- a/src/HOL/Topological_Spaces.thy Tue Nov 05 09:44:57 2013 +0100
8.2 +++ b/src/HOL/Topological_Spaces.thy Tue Nov 05 09:44:58 2013 +0100
8.3 @@ -2112,7 +2112,7 @@
8.4 with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
8.5 by (auto simp: subset_eq)
8.6 then show False
8.7 - using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
8.8 + using cInf_lower[OF `c \<in> A`] bnd by (metis not_le less_imp_le bdd_belowI)
8.9 qed
8.10
8.11 lemma Sup_notin_open:
8.12 @@ -2125,7 +2125,7 @@
8.13 with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
8.14 by (auto simp: subset_eq)
8.15 then show False
8.16 - using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
8.17 + using cSup_upper[OF `c \<in> A`] bnd by (metis less_imp_le not_le bdd_aboveI)
8.18 qed
8.19
8.20 end
8.21 @@ -2151,7 +2151,7 @@
8.22 let ?z = "Inf (B \<inter> {x <..})"
8.23
8.24 have "x \<le> ?z" "?z \<le> y"
8.25 - using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
8.26 + using `y \<in> B` `x < y` by (auto intro: cInf_lower cInf_greatest)
8.27 with `x \<in> U` `y \<in> U` have "?z \<in> U"
8.28 by (rule *)
8.29 moreover have "?z \<notin> B \<inter> {x <..}"
8.30 @@ -2163,11 +2163,11 @@
8.31 obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
8.32 using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
8.33 moreover obtain b where "b \<in> B" "x < b" "b < min a y"
8.34 - using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
8.35 + using cInf_less_iff[of "B \<inter> {x <..}" "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
8.36 by (auto intro: less_imp_le)
8.37 moreover have "?z \<le> b"
8.38 using `b \<in> B` `x < b`
8.39 - by (intro cInf_lower[where z=x]) auto
8.40 + by (intro cInf_lower) auto
8.41 moreover have "b \<in> U"
8.42 using `x \<le> ?z` `?z \<le> b` `b < min a y`
8.43 by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)