split dense into inner_dense_order and no_top/no_bot
authorhoelzl
Wed Feb 20 12:04:42 2013 +0100 (2013-02-20)
changeset 513294a3c453f99a1
parent 51328 d63ec23c9125
child 51333 2cfd028a2fd9
split dense into inner_dense_order and no_top/no_bot
src/HOL/Int.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Int.thy	Wed Feb 20 12:04:42 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Wed Feb 20 12:04:42 2013 +0100
     1.3 @@ -303,6 +303,18 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +instance int :: no_top
     1.8 +  apply default
     1.9 +  apply (rule_tac x="x + 1" in exI)
    1.10 +  apply simp
    1.11 +  done
    1.12 +
    1.13 +instance int :: no_bot
    1.14 +  apply default
    1.15 +  apply (rule_tac x="x - 1" in exI)
    1.16 +  apply simp
    1.17 +  done
    1.18 +
    1.19  subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
    1.20  
    1.21  lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Feb 20 12:04:42 2013 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 20 12:04:42 2013 +0100
     2.3 @@ -26,6 +26,18 @@
     2.4    "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
     2.5    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
     2.6  
     2.7 +lemma le_Sup_iff_less:
     2.8 +  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
     2.9 +  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    2.10 +  unfolding le_SUP_iff
    2.11 +  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    2.12 +
    2.13 +lemma Inf_le_iff_less:
    2.14 +  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
    2.15 +  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    2.16 +  unfolding INF_le_iff
    2.17 +  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    2.18 +
    2.19  subsection {* Definition and basic properties *}
    2.20  
    2.21  datatype ereal = ereal real | PInfty | MInfty
    2.22 @@ -295,6 +307,12 @@
    2.23  
    2.24  end
    2.25  
    2.26 +lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
    2.27 +  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
    2.28 +
    2.29 +instance ereal :: inner_dense_linorder
    2.30 +  by default (blast dest: ereal_dense2)
    2.31 +
    2.32  instance ereal :: ordered_ab_semigroup_add
    2.33  proof
    2.34    fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
    2.35 @@ -389,14 +407,6 @@
    2.36    fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
    2.37    by (cases rule: ereal2_cases[of a]) auto
    2.38  
    2.39 -lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
    2.40 -  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
    2.41 -
    2.42 -lemma ereal_dense:
    2.43 -  fixes x y :: ereal assumes "x < y"
    2.44 -  shows "\<exists>z. x < z \<and> z < y"
    2.45 -  using ereal_dense2[OF `x < y`] by blast
    2.46 -
    2.47  lemma ereal_add_strict_mono:
    2.48    fixes a b c d :: ereal
    2.49    assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
    2.50 @@ -725,18 +735,6 @@
    2.51    shows "y <= x"
    2.52  by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
    2.53  
    2.54 -lemma ereal_le_ereal:
    2.55 -  fixes x y :: ereal
    2.56 -  assumes "\<And>B. B < x \<Longrightarrow> B <= y"
    2.57 -  shows "x <= y"
    2.58 -by (metis assms ereal_dense leD linorder_le_less_linear)
    2.59 -
    2.60 -lemma ereal_ge_ereal:
    2.61 -  fixes x y :: ereal
    2.62 -  assumes "ALL B. B>x --> B >= y"
    2.63 -  shows "x >= y"
    2.64 -by (metis assms ereal_dense leD linorder_le_less_linear)
    2.65 -
    2.66  lemma setprod_ereal_0:
    2.67    fixes f :: "'a \<Rightarrow> ereal"
    2.68    shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
    2.69 @@ -1126,11 +1124,11 @@
    2.70  definition "bot = (-\<infinity>::ereal)"
    2.71  definition "top = (\<infinity>::ereal)"
    2.72  
    2.73 -definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)"
    2.74 -definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)"
    2.75 +definition "Sup S = (SOME x :: ereal. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z))"
    2.76 +definition "Inf S = (SOME x :: ereal. (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x))"
    2.77  
    2.78  lemma ereal_complete_Sup:
    2.79 -  fixes S :: "ereal set" assumes "S \<noteq> {}"
    2.80 +  fixes S :: "ereal set"
    2.81    shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
    2.82  proof cases
    2.83    assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
    2.84 @@ -1138,69 +1136,23 @@
    2.85    then have "\<infinity> \<notin> S" by force
    2.86    show ?thesis
    2.87    proof cases
    2.88 -    assume "S = {-\<infinity>}"
    2.89 -    then show ?thesis by (auto intro!: exI[of _ "-\<infinity>"])
    2.90 -  next
    2.91 -    assume "S \<noteq> {-\<infinity>}"
    2.92 -    with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
    2.93 -    with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
    2.94 -      by (auto simp: real_of_ereal_ord_simps)
    2.95 -    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
    2.96 -    obtain s where s:
    2.97 -       "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
    2.98 -       by auto
    2.99 +    assume "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}"
   2.100 +    with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>" by auto
   2.101 +    obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
   2.102 +    proof (atomize_elim, rule complete_real)
   2.103 +      show "\<exists>x. x \<in> ereal -` S" using x by auto
   2.104 +      show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z" by (auto dest: y intro!: exI[of _ y])
   2.105 +    qed
   2.106      show ?thesis
   2.107      proof (safe intro!: exI[of _ "ereal s"])
   2.108 -      fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> ereal s"
   2.109 -      proof (cases z)
   2.110 -        case (real r)
   2.111 -        then show ?thesis
   2.112 -          using s(1)[rule_format, of z] `z \<in> S` `z = ereal r` by auto
   2.113 -      qed auto
   2.114 +      fix y assume "y \<in> S" with s `\<infinity> \<notin> S` show "y \<le> ereal s"
   2.115 +        by (cases y) auto
   2.116      next
   2.117 -      fix z assume *: "\<forall>y\<in>S. y \<le> z"
   2.118 -      with `S \<noteq> {-\<infinity>}` `S \<noteq> {}` show "ereal s \<le> z"
   2.119 -      proof (cases z)
   2.120 -        case (real u)
   2.121 -        with * have "s \<le> u"
   2.122 -          by (intro s(2)[of u]) (auto simp: real_of_ereal_ord_simps)
   2.123 -        then show ?thesis using real by simp
   2.124 -      qed auto
   2.125 +      fix z assume "\<forall>y\<in>S. y \<le> z" with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
   2.126 +        by (cases z) (auto intro!: s)
   2.127      qed
   2.128 -  qed
   2.129 -next
   2.130 -  assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> ereal x)"
   2.131 -  show ?thesis
   2.132 -  proof (safe intro!: exI[of _ \<infinity>])
   2.133 -    fix y assume **: "\<forall>z\<in>S. z \<le> y"
   2.134 -    with * show "\<infinity> \<le> y"
   2.135 -    proof (cases y)
   2.136 -      case MInf with * ** show ?thesis by (force simp: not_le)
   2.137 -    qed auto
   2.138 -  qed simp
   2.139 -qed
   2.140 -
   2.141 -lemma ereal_complete_Inf:
   2.142 -  fixes S :: "ereal set" assumes "S ~= {}"
   2.143 -  shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)"
   2.144 -proof-
   2.145 -def S1 == "uminus ` S"
   2.146 -hence "S1 ~= {}" using assms by auto
   2.147 -then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
   2.148 -   using ereal_complete_Sup[of S1] by auto
   2.149 -{ fix z assume "ALL y:S. z <= y"
   2.150 -  hence "ALL y:S1. y <= -z" unfolding S1_def by auto
   2.151 -  hence "x <= -z" using x_def by auto
   2.152 -  hence "z <= -x"
   2.153 -    apply (subst ereal_uminus_uminus[symmetric])
   2.154 -    unfolding ereal_minus_le_minus . }
   2.155 -moreover have "(ALL y:S. -x <= y)"
   2.156 -   using x_def unfolding S1_def
   2.157 -   apply simp
   2.158 -   apply (subst (3) ereal_uminus_uminus[symmetric])
   2.159 -   unfolding ereal_minus_le_minus by simp
   2.160 -ultimately show ?thesis by auto
   2.161 -qed
   2.162 +  qed (auto intro!: exI[of _ "-\<infinity>"])
   2.163 +qed (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
   2.164  
   2.165  lemma ereal_complete_uminus_eq:
   2.166    fixes S :: "ereal set"
   2.167 @@ -1208,100 +1160,40 @@
   2.168       \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
   2.169    by simp (metis ereal_minus_le_minus ereal_uminus_uminus)
   2.170  
   2.171 -lemma ereal_Sup_uminus_image_eq:
   2.172 -  fixes S :: "ereal set"
   2.173 -  shows "Sup (uminus ` S) = - Inf S"
   2.174 -proof cases
   2.175 -  assume "S = {}"
   2.176 -  moreover have "(THE x. All (op \<le> x)) = (-\<infinity>::ereal)"
   2.177 -    by (rule the_equality) (auto intro!: ereal_bot)
   2.178 -  moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::ereal)"
   2.179 -    by (rule some_equality) (auto intro!: ereal_top)
   2.180 -  ultimately show ?thesis unfolding Inf_ereal_def Sup_ereal_def
   2.181 -    Least_def Greatest_def GreatestM_def by simp
   2.182 -next
   2.183 -  assume "S \<noteq> {}"
   2.184 -  with ereal_complete_Sup[of "uminus`S"]
   2.185 -  obtain x where x: "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
   2.186 -    unfolding ereal_complete_uminus_eq by auto
   2.187 -  show "Sup (uminus ` S) = - Inf S"
   2.188 -    unfolding Inf_ereal_def Greatest_def GreatestM_def
   2.189 -  proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) = - x"])
   2.190 -    show "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> -x)"
   2.191 -      using x .
   2.192 -    fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')"
   2.193 -    then have "(\<forall>y\<in>uminus`S. y \<le> - x') \<and> (\<forall>y. (\<forall>z\<in>uminus`S. z \<le> y) \<longrightarrow> - x' \<le> y)"
   2.194 -      unfolding ereal_complete_uminus_eq by simp
   2.195 -    then show "Sup (uminus ` S) = -x'"
   2.196 -      unfolding Sup_ereal_def ereal_uminus_eq_iff
   2.197 -      by (intro Least_equality) auto
   2.198 -  qed
   2.199 -qed
   2.200 +lemma ereal_complete_Inf:
   2.201 +  "\<exists>x. (\<forall>y\<in>S::ereal set. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
   2.202 +  using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
   2.203  
   2.204  instance
   2.205 -proof
   2.206 -  { fix x :: ereal and A
   2.207 -    show "bot <= x" by (cases x) (simp_all add: bot_ereal_def)
   2.208 -    show "x <= top" by (simp add: top_ereal_def) }
   2.209 -
   2.210 -  { fix x :: ereal and A assume "x : A"
   2.211 -    with ereal_complete_Sup[of A]
   2.212 -    obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
   2.213 -    hence "x <= s" using `x : A` by auto
   2.214 -    also have "... = Sup A" using s unfolding Sup_ereal_def
   2.215 -      by (auto intro!: Least_equality[symmetric])
   2.216 -    finally show "x <= Sup A" . }
   2.217 -  note le_Sup = this
   2.218 -
   2.219 -  { fix x :: ereal and A assume *: "!!z. (z : A ==> z <= x)"
   2.220 -    show "Sup A <= x"
   2.221 -    proof (cases "A = {}")
   2.222 -      case True
   2.223 -      hence "Sup A = -\<infinity>" unfolding Sup_ereal_def
   2.224 -        by (auto intro!: Least_equality)
   2.225 -      thus "Sup A <= x" by simp
   2.226 -    next
   2.227 -      case False
   2.228 -      with ereal_complete_Sup[of A]
   2.229 -      obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
   2.230 -      hence "Sup A = s"
   2.231 -        unfolding Sup_ereal_def by (auto intro!: Least_equality)
   2.232 -      also have "s <= x" using * s by auto
   2.233 -      finally show "Sup A <= x" .
   2.234 -    qed }
   2.235 -  note Sup_le = this
   2.236 -
   2.237 -  { fix x :: ereal and A assume "x \<in> A"
   2.238 -    with le_Sup[of "-x" "uminus`A"] show "Inf A \<le> x"
   2.239 -      unfolding ereal_Sup_uminus_image_eq by simp }
   2.240 -
   2.241 -  { fix x :: ereal and A assume *: "!!z. (z : A ==> x <= z)"
   2.242 -    with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
   2.243 -      unfolding ereal_Sup_uminus_image_eq by force }
   2.244 -qed
   2.245 +  by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
   2.246 +                   simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
   2.247  
   2.248  end
   2.249  
   2.250  instance ereal :: complete_linorder ..
   2.251  
   2.252 +lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
   2.253 +  by (auto intro!: Sup_eqI
   2.254 +           simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
   2.255 +           intro!: complete_lattice_class.Inf_lower2)
   2.256 +
   2.257 +lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
   2.258 +  by (auto intro!: inj_onI)
   2.259 +
   2.260 +lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
   2.261 +  using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
   2.262 +
   2.263  lemma ereal_SUPR_uminus:
   2.264    fixes f :: "'a => ereal"
   2.265    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
   2.266 -  unfolding SUP_def INF_def
   2.267    using ereal_Sup_uminus_image_eq[of "f`R"]
   2.268 -  by (simp add: image_image)
   2.269 +  by (simp add: SUP_def INF_def image_image)
   2.270  
   2.271  lemma ereal_INFI_uminus:
   2.272    fixes f :: "'a => ereal"
   2.273    shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
   2.274    using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
   2.275  
   2.276 -lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::ereal set)"
   2.277 -  using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image)
   2.278 -
   2.279 -lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
   2.280 -  by (auto intro!: inj_onI)
   2.281 -
   2.282  lemma ereal_image_uminus_shift:
   2.283    fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
   2.284  proof
   2.285 @@ -1319,14 +1211,7 @@
   2.286  
   2.287  lemma Sup_eq_MInfty:
   2.288    fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
   2.289 -proof
   2.290 -  assume a: "Sup S = -\<infinity>"
   2.291 -  with complete_lattice_class.Sup_upper[of _ S]
   2.292 -  show "S={} \<or> S={-\<infinity>}" by auto
   2.293 -next
   2.294 -  assume "S={} \<or> S={-\<infinity>}" then show "Sup S = -\<infinity>"
   2.295 -    unfolding Sup_ereal_def by (auto intro!: Least_equality)
   2.296 -qed
   2.297 +  unfolding bot_ereal_def[symmetric] by auto
   2.298  
   2.299  lemma Inf_eq_PInfty:
   2.300    fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
   2.301 @@ -1335,13 +1220,11 @@
   2.302  
   2.303  lemma Inf_eq_MInfty: 
   2.304    fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
   2.305 -  unfolding Inf_ereal_def
   2.306 -  by (auto intro!: Greatest_equality)
   2.307 +  unfolding bot_ereal_def[symmetric] by auto
   2.308  
   2.309  lemma Sup_eq_PInfty:
   2.310    fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
   2.311 -  unfolding Sup_ereal_def
   2.312 -  by (auto intro!: Least_equality)
   2.313 +  unfolding top_ereal_def[symmetric] by auto
   2.314  
   2.315  lemma Sup_ereal_close:
   2.316    fixes e :: ereal
   2.317 @@ -2007,39 +1890,6 @@
   2.318  lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
   2.319    using assms by auto
   2.320  
   2.321 -lemma ereal_le_ereal_bounded:
   2.322 -  fixes x y z :: ereal
   2.323 -  assumes "z \<le> y"
   2.324 -  assumes *: "\<And>B. z < B \<Longrightarrow> B < x \<Longrightarrow> B \<le> y"
   2.325 -  shows "x \<le> y"
   2.326 -proof (rule ereal_le_ereal)
   2.327 -  fix B assume "B < x"
   2.328 -  show "B \<le> y"
   2.329 -  proof cases
   2.330 -    assume "z < B" from *[OF this `B < x`] show "B \<le> y" .
   2.331 -  next
   2.332 -    assume "\<not> z < B" with `z \<le> y` show "B \<le> y" by auto
   2.333 -  qed
   2.334 -qed
   2.335 -
   2.336 -lemma fixes x y :: ereal
   2.337 -  shows Sup_atMost[simp]: "Sup {.. y} = y"
   2.338 -    and Sup_lessThan[simp]: "Sup {..< y} = y"
   2.339 -    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
   2.340 -    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
   2.341 -    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
   2.342 -  by (auto simp: Sup_ereal_def intro!: Least_equality
   2.343 -           intro: ereal_le_ereal ereal_le_ereal_bounded[of x])
   2.344 -
   2.345 -lemma Sup_greaterThanlessThan[simp]:
   2.346 -  fixes x y :: ereal assumes "x < y" shows "Sup { x <..< y} = y"
   2.347 -  unfolding Sup_ereal_def
   2.348 -proof (intro Least_equality ereal_le_ereal_bounded[of _ _ y])
   2.349 -  fix z assume z: "\<forall>u\<in>{x<..<y}. u \<le> z"
   2.350 -  from ereal_dense[OF `x < y`] guess w .. note w = this
   2.351 -  with z[THEN bspec, of w] show "x \<le> z" by auto
   2.352 -qed auto
   2.353 -
   2.354  lemma real_ereal_id: "real o ereal = id"
   2.355  proof-
   2.356    { fix x have "(real o ereal) x = id x" by auto }
   2.357 @@ -2109,6 +1959,7 @@
   2.358    assumes "f ----> f0"
   2.359    assumes "open S" "f0 : S"
   2.360    obtains N where "ALL n>=N. f n : S"
   2.361 +  using assms using tendsto_def
   2.362    using tendsto_explicit[of f f0] assms by auto
   2.363  
   2.364  lemma ereal_LimI_finite_iff:
     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Feb 20 12:04:42 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Feb 20 12:04:42 2013 +0100
     3.3 @@ -82,7 +82,7 @@
     3.4      case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
     3.5      from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
     3.6      then obtain b where b_def: "a<b & b<a+e"
     3.7 -      using fin ereal_between ereal_dense[of a "a+e"] by auto
     3.8 +      using fin ereal_between dense[of a "a+e"] by auto
     3.9      then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
    3.10      then show False using b_def e by auto
    3.11    qed
    3.12 @@ -157,7 +157,7 @@
    3.13    { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
    3.14      from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
    3.15      then obtain b where b_def: "Inf S-e<b & b<Inf S"
    3.16 -      using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
    3.17 +      using fin ereal_between[of "Inf S" e] dense[of "Inf S-e"] by auto
    3.18      then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
    3.19        by auto
    3.20      then have "b:S" using e by auto
    3.21 @@ -335,7 +335,7 @@
    3.22    assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
    3.23    assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
    3.24    show "l \<le> y"
    3.25 -  proof (rule ereal_le_ereal)
    3.26 +  proof (rule dense_le)
    3.27      fix B assume "B < l"
    3.28      then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
    3.29        by (intro S[rule_format]) auto
    3.30 @@ -369,7 +369,7 @@
    3.31    assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
    3.32    assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
    3.33    show "y \<le> l"
    3.34 -  proof (rule ereal_ge_ereal, safe)
    3.35 +  proof (rule dense_ge)
    3.36      fix B assume "l < B"
    3.37      then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
    3.38        by (intro S[rule_format]) auto
     4.1 --- a/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
     4.2 +++ b/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
     4.3 @@ -455,6 +455,9 @@
     4.4  
     4.5  end
     4.6  
     4.7 +instance nat :: no_top
     4.8 +  by default (auto intro: less_Suc_eq_le[THEN iffD2])
     4.9 +
    4.10  subsubsection {* Introduction properties *}
    4.11  
    4.12  lemma lessI [iff]: "n < Suc n"
     5.1 --- a/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
     5.2 +++ b/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
     5.3 @@ -1135,10 +1135,10 @@
     5.4  
     5.5  subsection {* Dense orders *}
     5.6  
     5.7 -class dense_linorder = linorder + 
     5.8 -  assumes gt_ex: "\<exists>y. x < y" 
     5.9 -  and lt_ex: "\<exists>y. y < x"
    5.10 -  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    5.11 +class inner_dense_order = order +
    5.12 +  assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    5.13 +
    5.14 +class inner_dense_linorder = linorder + inner_dense_order
    5.15  begin
    5.16  
    5.17  lemma dense_le:
    5.18 @@ -1175,8 +1175,50 @@
    5.19    qed
    5.20  qed
    5.21  
    5.22 +lemma dense_ge:
    5.23 +  fixes y z :: 'a
    5.24 +  assumes "\<And>x. z < x \<Longrightarrow> y \<le> x"
    5.25 +  shows "y \<le> z"
    5.26 +proof (rule ccontr)
    5.27 +  assume "\<not> ?thesis"
    5.28 +  hence "z < y" by simp
    5.29 +  from dense[OF this]
    5.30 +  obtain x where "x < y" and "z < x" by safe
    5.31 +  moreover have "y \<le> x" using assms[OF `z < x`] .
    5.32 +  ultimately show False by auto
    5.33 +qed
    5.34 +
    5.35 +lemma dense_ge_bounded:
    5.36 +  fixes x y z :: 'a
    5.37 +  assumes "z < x"
    5.38 +  assumes *: "\<And>w. \<lbrakk> z < w ; w < x \<rbrakk> \<Longrightarrow> y \<le> w"
    5.39 +  shows "y \<le> z"
    5.40 +proof (rule dense_ge)
    5.41 +  fix w assume "z < w"
    5.42 +  from dense[OF `z < x`] obtain u where "z < u" "u < x" by safe
    5.43 +  from linear[of u w]
    5.44 +  show "y \<le> w"
    5.45 +  proof (rule disjE)
    5.46 +    assume "w \<le> u"
    5.47 +    from `z < w` le_less_trans[OF `w \<le> u` `u < x`]
    5.48 +    show "y \<le> w" by (rule *)
    5.49 +  next
    5.50 +    assume "u \<le> w"
    5.51 +    from *[OF `z < u` `u < x`] `u \<le> w`
    5.52 +    show "y \<le> w" by (rule order_trans)
    5.53 +  qed
    5.54 +qed
    5.55 +
    5.56  end
    5.57  
    5.58 +class no_top = order + 
    5.59 +  assumes gt_ex: "\<exists>y. x < y"
    5.60 +
    5.61 +class no_bot = order + 
    5.62 +  assumes lt_ex: "\<exists>y. y < x"
    5.63 +
    5.64 +class dense_linorder = inner_dense_linorder + no_top + no_bot
    5.65 +
    5.66  subsection {* Wellorders *}
    5.67  
    5.68  class wellorder = linorder +
     6.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Feb 20 12:04:42 2013 +0100
     6.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Feb 20 12:04:42 2013 +0100
     6.3 @@ -363,8 +363,7 @@
     6.4    assumes posf: "positive M f" and ca: "countably_additive M f"
     6.5        and s: "s \<in> M"
     6.6    shows "Inf (measure_set M f s) = f s"
     6.7 -  unfolding Inf_ereal_def
     6.8 -proof (safe intro!: Greatest_equality)
     6.9 +proof (intro Inf_eqI)
    6.10    fix z
    6.11    assume z: "z \<in> measure_set M f s"
    6.12    from this obtain A where
    6.13 @@ -394,12 +393,7 @@
    6.14      qed
    6.15    also have "... = z" by (rule si)
    6.16    finally show "f s \<le> z" .
    6.17 -next
    6.18 -  fix y
    6.19 -  assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
    6.20 -  thus "y \<le> f s"
    6.21 -    by (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
    6.22 -qed
    6.23 +qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
    6.24  
    6.25  lemma measure_set_pos:
    6.26    assumes posf: "positive M f" "r \<in> measure_set M f X"
     7.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 20 12:04:42 2013 +0100
     7.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 20 12:04:42 2013 +0100
     7.3 @@ -57,7 +57,7 @@
     7.4    proof
     7.5      fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
     7.6        using measure[of i] emeasure_nonneg[of M "A i"]
     7.7 -      by (auto intro!: ereal_dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
     7.8 +      by (auto intro!: dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
     7.9    qed
    7.10    from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
    7.11      "\<And>i. n i < inverse (2^Suc i * emeasure M (A i))" by auto
     8.1 --- a/src/HOL/Set_Interval.thy	Wed Feb 20 12:04:42 2013 +0100
     8.2 +++ b/src/HOL/Set_Interval.thy	Wed Feb 20 12:04:42 2013 +0100
     8.3 @@ -267,7 +267,7 @@
     8.4  
     8.5  end
     8.6  
     8.7 -context dense_linorder
     8.8 +context inner_dense_linorder
     8.9  begin
    8.10  
    8.11  lemma greaterThanLessThan_empty_iff[simp]:
    8.12 @@ -310,6 +310,22 @@
    8.13  
    8.14  end
    8.15  
    8.16 +context no_top
    8.17 +begin
    8.18 +
    8.19 +lemma greaterThan_non_empty: "{x <..} \<noteq> {}"
    8.20 +  using gt_ex[of x] by auto
    8.21 +
    8.22 +end
    8.23 +
    8.24 +context no_bot
    8.25 +begin
    8.26 +
    8.27 +lemma lessThan_non_empty: "{..< x} \<noteq> {}"
    8.28 +  using lt_ex[of x] by auto
    8.29 +
    8.30 +end
    8.31 +
    8.32  lemma (in linorder) atLeastLessThan_subset_iff:
    8.33    "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
    8.34  apply (auto simp:subset_eq Ball_def)
    8.35 @@ -378,6 +394,36 @@
    8.36  
    8.37  end
    8.38  
    8.39 +context complete_lattice
    8.40 +begin
    8.41 +
    8.42 +lemma
    8.43 +  shows Sup_atLeast[simp]: "Sup {x ..} = top"
    8.44 +    and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top"
    8.45 +    and Sup_atMost[simp]: "Sup {.. y} = y"
    8.46 +    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
    8.47 +    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
    8.48 +  by (auto intro!: Sup_eqI)
    8.49 +
    8.50 +lemma
    8.51 +  shows Inf_atMost[simp]: "Inf {.. x} = bot"
    8.52 +    and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot"
    8.53 +    and Inf_atLeast[simp]: "Inf {x ..} = x"
    8.54 +    and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x"
    8.55 +    and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x"
    8.56 +  by (auto intro!: Inf_eqI)
    8.57 +
    8.58 +end
    8.59 +
    8.60 +lemma
    8.61 +  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
    8.62 +  shows Sup_lessThan[simp]: "Sup {..< y} = y"
    8.63 +    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
    8.64 +    and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
    8.65 +    and Inf_greaterThan[simp]: "Inf {x <..} = x"
    8.66 +    and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x"
    8.67 +    and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x"
    8.68 +  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)
    8.69  
    8.70  subsection {* Intervals of natural numbers *}
    8.71