# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID ebf9d4fd00ba84ab425d9562f483beb94a29af5f
# Parent  1e9e68247ad1af5d48bd35784d494e7d842770d9
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it

diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Fashoda.thy
--- 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))"
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Integration.thy
--- 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
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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 .
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- 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)"
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/Probability/Probability_Measure.thy
--- 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
diff -r 1e9e68247ad1 -r ebf9d4fd00ba src/HOL/SupInf.thy
--- 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