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