# HG changeset patch
# User hoelzl
# Date 1361358282 -3600
# Node ID 4a3c453f99a13544452824753a4e0eb5fedb3827
# Parent  d63ec23c9125f7203e48807f204c8b42c9914dd8
split dense into inner_dense_order and no_top/no_bot

diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Int.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -303,6 +303,18 @@
 qed
 
 
+instance int :: no_top
+  apply default
+  apply (rule_tac x="x + 1" in exI)
+  apply simp
+  done
+
+instance int :: no_bot
+  apply default
+  apply (rule_tac x="x - 1" in exI)
+  apply simp
+  done
+
 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
 
 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -26,6 +26,18 @@
   "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
+lemma le_Sup_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+  unfolding le_SUP_iff
+  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
+lemma Inf_le_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  unfolding INF_le_iff
+  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
 subsection {* Definition and basic properties *}
 
 datatype ereal = ereal real | PInfty | MInfty
@@ -295,6 +307,12 @@
 
 end
 
+lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
+  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
+
+instance ereal :: inner_dense_linorder
+  by default (blast dest: ereal_dense2)
+
 instance ereal :: ordered_ab_semigroup_add
 proof
   fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
@@ -389,14 +407,6 @@
   fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   by (cases rule: ereal2_cases[of a]) auto
 
-lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
-  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
-
-lemma ereal_dense:
-  fixes x y :: ereal assumes "x < y"
-  shows "\<exists>z. x < z \<and> z < y"
-  using ereal_dense2[OF `x < y`] by blast
-
 lemma ereal_add_strict_mono:
   fixes a b c d :: ereal
   assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
@@ -725,18 +735,6 @@
   shows "y <= x"
 by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
 
-lemma ereal_le_ereal:
-  fixes x y :: ereal
-  assumes "\<And>B. B < x \<Longrightarrow> B <= y"
-  shows "x <= y"
-by (metis assms ereal_dense leD linorder_le_less_linear)
-
-lemma ereal_ge_ereal:
-  fixes x y :: ereal
-  assumes "ALL B. B>x --> B >= y"
-  shows "x >= y"
-by (metis assms ereal_dense leD linorder_le_less_linear)
-
 lemma setprod_ereal_0:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
@@ -1126,11 +1124,11 @@
 definition "bot = (-\<infinity>::ereal)"
 definition "top = (\<infinity>::ereal)"
 
-definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)"
-definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)"
+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))"
+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))"
 
 lemma ereal_complete_Sup:
-  fixes S :: "ereal set" assumes "S \<noteq> {}"
+  fixes S :: "ereal set"
   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
 proof cases
   assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
@@ -1138,69 +1136,23 @@
   then have "\<infinity> \<notin> S" by force
   show ?thesis
   proof cases
-    assume "S = {-\<infinity>}"
-    then show ?thesis by (auto intro!: exI[of _ "-\<infinity>"])
-  next
-    assume "S \<noteq> {-\<infinity>}"
-    with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
-    with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
-      by (auto simp: real_of_ereal_ord_simps)
-    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
-    obtain s where s:
-       "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
-       by auto
+    assume "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}"
+    with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>" by auto
+    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"
+    proof (atomize_elim, rule complete_real)
+      show "\<exists>x. x \<in> ereal -` S" using x by auto
+      show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z" by (auto dest: y intro!: exI[of _ y])
+    qed
     show ?thesis
     proof (safe intro!: exI[of _ "ereal s"])
-      fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> ereal s"
-      proof (cases z)
-        case (real r)
-        then show ?thesis
-          using s(1)[rule_format, of z] `z \<in> S` `z = ereal r` by auto
-      qed auto
+      fix y assume "y \<in> S" with s `\<infinity> \<notin> S` show "y \<le> ereal s"
+        by (cases y) auto
     next
-      fix z assume *: "\<forall>y\<in>S. y \<le> z"
-      with `S \<noteq> {-\<infinity>}` `S \<noteq> {}` show "ereal s \<le> z"
-      proof (cases z)
-        case (real u)
-        with * have "s \<le> u"
-          by (intro s(2)[of u]) (auto simp: real_of_ereal_ord_simps)
-        then show ?thesis using real by simp
-      qed auto
+      fix z assume "\<forall>y\<in>S. y \<le> z" with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
+        by (cases z) (auto intro!: s)
     qed
-  qed
-next
-  assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> ereal x)"
-  show ?thesis
-  proof (safe intro!: exI[of _ \<infinity>])
-    fix y assume **: "\<forall>z\<in>S. z \<le> y"
-    with * show "\<infinity> \<le> y"
-    proof (cases y)
-      case MInf with * ** show ?thesis by (force simp: not_le)
-    qed auto
-  qed simp
-qed
-
-lemma ereal_complete_Inf:
-  fixes S :: "ereal set" assumes "S ~= {}"
-  shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)"
-proof-
-def S1 == "uminus ` S"
-hence "S1 ~= {}" using assms by auto
-then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
-   using ereal_complete_Sup[of S1] by auto
-{ fix z assume "ALL y:S. z <= y"
-  hence "ALL y:S1. y <= -z" unfolding S1_def by auto
-  hence "x <= -z" using x_def by auto
-  hence "z <= -x"
-    apply (subst ereal_uminus_uminus[symmetric])
-    unfolding ereal_minus_le_minus . }
-moreover have "(ALL y:S. -x <= y)"
-   using x_def unfolding S1_def
-   apply simp
-   apply (subst (3) ereal_uminus_uminus[symmetric])
-   unfolding ereal_minus_le_minus by simp
-ultimately show ?thesis by auto
-qed
+  qed (auto intro!: exI[of _ "-\<infinity>"])
+qed (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
 
 lemma ereal_complete_uminus_eq:
   fixes S :: "ereal set"
@@ -1208,100 +1160,40 @@
      \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
   by simp (metis ereal_minus_le_minus ereal_uminus_uminus)
 
-lemma ereal_Sup_uminus_image_eq:
-  fixes S :: "ereal set"
-  shows "Sup (uminus ` S) = - Inf S"
-proof cases
-  assume "S = {}"
-  moreover have "(THE x. All (op \<le> x)) = (-\<infinity>::ereal)"
-    by (rule the_equality) (auto intro!: ereal_bot)
-  moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::ereal)"
-    by (rule some_equality) (auto intro!: ereal_top)
-  ultimately show ?thesis unfolding Inf_ereal_def Sup_ereal_def
-    Least_def Greatest_def GreatestM_def by simp
-next
-  assume "S \<noteq> {}"
-  with ereal_complete_Sup[of "uminus`S"]
-  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)"
-    unfolding ereal_complete_uminus_eq by auto
-  show "Sup (uminus ` S) = - Inf S"
-    unfolding Inf_ereal_def Greatest_def GreatestM_def
-  proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) = - x"])
-    show "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> -x)"
-      using x .
-    fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')"
-    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)"
-      unfolding ereal_complete_uminus_eq by simp
-    then show "Sup (uminus ` S) = -x'"
-      unfolding Sup_ereal_def ereal_uminus_eq_iff
-      by (intro Least_equality) auto
-  qed
-qed
+lemma ereal_complete_Inf:
+  "\<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)"
+  using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
 
 instance
-proof
-  { fix x :: ereal and A
-    show "bot <= x" by (cases x) (simp_all add: bot_ereal_def)
-    show "x <= top" by (simp add: top_ereal_def) }
-
-  { fix x :: ereal and A assume "x : A"
-    with ereal_complete_Sup[of A]
-    obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
-    hence "x <= s" using `x : A` by auto
-    also have "... = Sup A" using s unfolding Sup_ereal_def
-      by (auto intro!: Least_equality[symmetric])
-    finally show "x <= Sup A" . }
-  note le_Sup = this
-
-  { fix x :: ereal and A assume *: "!!z. (z : A ==> z <= x)"
-    show "Sup A <= x"
-    proof (cases "A = {}")
-      case True
-      hence "Sup A = -\<infinity>" unfolding Sup_ereal_def
-        by (auto intro!: Least_equality)
-      thus "Sup A <= x" by simp
-    next
-      case False
-      with ereal_complete_Sup[of A]
-      obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
-      hence "Sup A = s"
-        unfolding Sup_ereal_def by (auto intro!: Least_equality)
-      also have "s <= x" using * s by auto
-      finally show "Sup A <= x" .
-    qed }
-  note Sup_le = this
-
-  { fix x :: ereal and A assume "x \<in> A"
-    with le_Sup[of "-x" "uminus`A"] show "Inf A \<le> x"
-      unfolding ereal_Sup_uminus_image_eq by simp }
-
-  { fix x :: ereal and A assume *: "!!z. (z : A ==> x <= z)"
-    with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
-      unfolding ereal_Sup_uminus_image_eq by force }
-qed
+  by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
+                   simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
 
 end
 
 instance ereal :: complete_linorder ..
 
+lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
+  by (auto intro!: Sup_eqI
+           simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
+           intro!: complete_lattice_class.Inf_lower2)
+
+lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
+  by (auto intro!: inj_onI)
+
+lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
+  using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
+
 lemma ereal_SUPR_uminus:
   fixes f :: "'a => ereal"
   shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
-  unfolding SUP_def INF_def
   using ereal_Sup_uminus_image_eq[of "f`R"]
-  by (simp add: image_image)
+  by (simp add: SUP_def INF_def image_image)
 
 lemma ereal_INFI_uminus:
   fixes f :: "'a => ereal"
   shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
   using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
 
-lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::ereal set)"
-  using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image)
-
-lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
-  by (auto intro!: inj_onI)
-
 lemma ereal_image_uminus_shift:
   fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
 proof
@@ -1319,14 +1211,7 @@
 
 lemma Sup_eq_MInfty:
   fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
-proof
-  assume a: "Sup S = -\<infinity>"
-  with complete_lattice_class.Sup_upper[of _ S]
-  show "S={} \<or> S={-\<infinity>}" by auto
-next
-  assume "S={} \<or> S={-\<infinity>}" then show "Sup S = -\<infinity>"
-    unfolding Sup_ereal_def by (auto intro!: Least_equality)
-qed
+  unfolding bot_ereal_def[symmetric] by auto
 
 lemma Inf_eq_PInfty:
   fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
@@ -1335,13 +1220,11 @@
 
 lemma Inf_eq_MInfty: 
   fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
-  unfolding Inf_ereal_def
-  by (auto intro!: Greatest_equality)
+  unfolding bot_ereal_def[symmetric] by auto
 
 lemma Sup_eq_PInfty:
   fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
-  unfolding Sup_ereal_def
-  by (auto intro!: Least_equality)
+  unfolding top_ereal_def[symmetric] by auto
 
 lemma Sup_ereal_close:
   fixes e :: ereal
@@ -2007,39 +1890,6 @@
 lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
   using assms by auto
 
-lemma ereal_le_ereal_bounded:
-  fixes x y z :: ereal
-  assumes "z \<le> y"
-  assumes *: "\<And>B. z < B \<Longrightarrow> B < x \<Longrightarrow> B \<le> y"
-  shows "x \<le> y"
-proof (rule ereal_le_ereal)
-  fix B assume "B < x"
-  show "B \<le> y"
-  proof cases
-    assume "z < B" from *[OF this `B < x`] show "B \<le> y" .
-  next
-    assume "\<not> z < B" with `z \<le> y` show "B \<le> y" by auto
-  qed
-qed
-
-lemma fixes x y :: ereal
-  shows Sup_atMost[simp]: "Sup {.. y} = y"
-    and Sup_lessThan[simp]: "Sup {..< y} = y"
-    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
-    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
-    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
-  by (auto simp: Sup_ereal_def intro!: Least_equality
-           intro: ereal_le_ereal ereal_le_ereal_bounded[of x])
-
-lemma Sup_greaterThanlessThan[simp]:
-  fixes x y :: ereal assumes "x < y" shows "Sup { x <..< y} = y"
-  unfolding Sup_ereal_def
-proof (intro Least_equality ereal_le_ereal_bounded[of _ _ y])
-  fix z assume z: "\<forall>u\<in>{x<..<y}. u \<le> z"
-  from ereal_dense[OF `x < y`] guess w .. note w = this
-  with z[THEN bspec, of w] show "x \<le> z" by auto
-qed auto
-
 lemma real_ereal_id: "real o ereal = id"
 proof-
   { fix x have "(real o ereal) x = id x" by auto }
@@ -2109,6 +1959,7 @@
   assumes "f ----> f0"
   assumes "open S" "f0 : S"
   obtains N where "ALL n>=N. f n : S"
+  using assms using tendsto_def
   using tendsto_explicit[of f f0] assms by auto
 
 lemma ereal_LimI_finite_iff:
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -82,7 +82,7 @@
     case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
     from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
     then obtain b where b_def: "a<b & b<a+e"
-      using fin ereal_between ereal_dense[of a "a+e"] by auto
+      using fin ereal_between dense[of a "a+e"] by auto
     then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
     then show False using b_def e by auto
   qed
@@ -157,7 +157,7 @@
   { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
     from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
     then obtain b where b_def: "Inf S-e<b & b<Inf S"
-      using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
+      using fin ereal_between[of "Inf S" e] dense[of "Inf S-e"] by auto
     then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
       by auto
     then have "b:S" using e by auto
@@ -335,7 +335,7 @@
   assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
   show "l \<le> y"
-  proof (rule ereal_le_ereal)
+  proof (rule dense_le)
     fix B assume "B < l"
     then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
       by (intro S[rule_format]) auto
@@ -369,7 +369,7 @@
   assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   show "y \<le> l"
-  proof (rule ereal_ge_ereal, safe)
+  proof (rule dense_ge)
     fix B assume "l < B"
     then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
       by (intro S[rule_format]) auto
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -455,6 +455,9 @@
 
 end
 
+instance nat :: no_top
+  by default (auto intro: less_Suc_eq_le[THEN iffD2])
+
 subsubsection {* Introduction properties *}
 
 lemma lessI [iff]: "n < Suc n"
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -1135,10 +1135,10 @@
 
 subsection {* Dense orders *}
 
-class dense_linorder = linorder + 
-  assumes gt_ex: "\<exists>y. x < y" 
-  and lt_ex: "\<exists>y. y < x"
-  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+class inner_dense_order = order +
+  assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+
+class inner_dense_linorder = linorder + inner_dense_order
 begin
 
 lemma dense_le:
@@ -1175,8 +1175,50 @@
   qed
 qed
 
+lemma dense_ge:
+  fixes y z :: 'a
+  assumes "\<And>x. z < x \<Longrightarrow> y \<le> x"
+  shows "y \<le> z"
+proof (rule ccontr)
+  assume "\<not> ?thesis"
+  hence "z < y" by simp
+  from dense[OF this]
+  obtain x where "x < y" and "z < x" by safe
+  moreover have "y \<le> x" using assms[OF `z < x`] .
+  ultimately show False by auto
+qed
+
+lemma dense_ge_bounded:
+  fixes x y z :: 'a
+  assumes "z < x"
+  assumes *: "\<And>w. \<lbrakk> z < w ; w < x \<rbrakk> \<Longrightarrow> y \<le> w"
+  shows "y \<le> z"
+proof (rule dense_ge)
+  fix w assume "z < w"
+  from dense[OF `z < x`] obtain u where "z < u" "u < x" by safe
+  from linear[of u w]
+  show "y \<le> w"
+  proof (rule disjE)
+    assume "w \<le> u"
+    from `z < w` le_less_trans[OF `w \<le> u` `u < x`]
+    show "y \<le> w" by (rule *)
+  next
+    assume "u \<le> w"
+    from *[OF `z < u` `u < x`] `u \<le> w`
+    show "y \<le> w" by (rule order_trans)
+  qed
+qed
+
 end
 
+class no_top = order + 
+  assumes gt_ex: "\<exists>y. x < y"
+
+class no_bot = order + 
+  assumes lt_ex: "\<exists>y. y < x"
+
+class dense_linorder = inner_dense_linorder + no_top + no_bot
+
 subsection {* Wellorders *}
 
 class wellorder = linorder +
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -363,8 +363,7 @@
   assumes posf: "positive M f" and ca: "countably_additive M f"
       and s: "s \<in> M"
   shows "Inf (measure_set M f s) = f s"
-  unfolding Inf_ereal_def
-proof (safe intro!: Greatest_equality)
+proof (intro Inf_eqI)
   fix z
   assume z: "z \<in> measure_set M f s"
   from this obtain A where
@@ -394,12 +393,7 @@
     qed
   also have "... = z" by (rule si)
   finally show "f s \<le> z" .
-next
-  fix y
-  assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
-  thus "y \<le> f s"
-    by (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
-qed
+qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
 
 lemma measure_set_pos:
   assumes posf: "positive M f" "r \<in> measure_set M f X"
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -57,7 +57,7 @@
   proof
     fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
       using measure[of i] emeasure_nonneg[of M "A i"]
-      by (auto intro!: ereal_dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
+      by (auto intro!: dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
   qed
   from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
     "\<And>i. n i < inverse (2^Suc i * emeasure M (A i))" by auto
diff -r d63ec23c9125 -r 4a3c453f99a1 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -267,7 +267,7 @@
 
 end
 
-context dense_linorder
+context inner_dense_linorder
 begin
 
 lemma greaterThanLessThan_empty_iff[simp]:
@@ -310,6 +310,22 @@
 
 end
 
+context no_top
+begin
+
+lemma greaterThan_non_empty: "{x <..} \<noteq> {}"
+  using gt_ex[of x] by auto
+
+end
+
+context no_bot
+begin
+
+lemma lessThan_non_empty: "{..< x} \<noteq> {}"
+  using lt_ex[of x] by auto
+
+end
+
 lemma (in linorder) atLeastLessThan_subset_iff:
   "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
 apply (auto simp:subset_eq Ball_def)
@@ -378,6 +394,36 @@
 
 end
 
+context complete_lattice
+begin
+
+lemma
+  shows Sup_atLeast[simp]: "Sup {x ..} = top"
+    and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top"
+    and Sup_atMost[simp]: "Sup {.. y} = y"
+    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
+    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
+  by (auto intro!: Sup_eqI)
+
+lemma
+  shows Inf_atMost[simp]: "Inf {.. x} = bot"
+    and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot"
+    and Inf_atLeast[simp]: "Inf {x ..} = x"
+    and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x"
+    and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x"
+  by (auto intro!: Inf_eqI)
+
+end
+
+lemma
+  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+  shows Sup_lessThan[simp]: "Sup {..< y} = y"
+    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
+    and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
+    and Inf_greaterThan[simp]: "Inf {x <..} = x"
+    and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x"
+    and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x"
+  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)
 
 subsection {* Intervals of natural numbers *}