src/HOL/Multivariate_Analysis/Integration.thy
changeset 54263 c4159fe6fa46
parent 54258 adfc759263ab
child 54411 f72e58a5a75f
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -28,10 +28,10 @@
     1.4  proof -
     1.5    have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
     1.6      by arith
     1.7 -  then show ?thesis
     1.8 -    using S b cSup_bounds[of S "l - e" "l+e"]
     1.9 -    unfolding th
    1.10 -    by (auto simp add: setge_def setle_def)
    1.11 +  have "bdd_above S"
    1.12 +    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
    1.13 +  with S b show ?thesis
    1.14 +    unfolding th by (auto intro!: cSup_upper2 cSup_least)
    1.15  qed
    1.16  
    1.17  lemma cInf_asclose: (* TODO: is this really needed? *)
    1.18 @@ -70,39 +70,6 @@
    1.19    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
    1.20    by (metis cInf_eq_Min Min_le_iff)
    1.21  
    1.22 -lemma Inf: (* rename *)
    1.23 -  fixes S :: "real set"
    1.24 -  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
    1.25 -  by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
    1.26 -    intro: cInf_lower cInf_greatest)
    1.27 -
    1.28 -lemma real_le_inf_subset:
    1.29 -  assumes "t \<noteq> {}"
    1.30 -    and "t \<subseteq> s"
    1.31 -    and "\<exists>b. b <=* s"
    1.32 -  shows "Inf s \<le> Inf (t::real set)"
    1.33 -  apply (rule isGlb_le_isLb)
    1.34 -  apply (rule Inf[OF assms(1)])
    1.35 -  apply (insert assms)
    1.36 -  apply (erule exE)
    1.37 -  apply (rule_tac x = b in exI)
    1.38 -  apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
    1.39 -  done
    1.40 -
    1.41 -lemma real_ge_sup_subset:
    1.42 -  fixes t :: "real set"
    1.43 -  assumes "t \<noteq> {}"
    1.44 -    and "t \<subseteq> s"
    1.45 -    and "\<exists>b. s *<= b"
    1.46 -  shows "Sup s \<ge> Sup t"
    1.47 -  apply (rule isLub_le_isUb)
    1.48 -  apply (rule isLub_cSup[OF assms(1)])
    1.49 -  apply (insert assms)
    1.50 -  apply (erule exE)
    1.51 -  apply (rule_tac x = b in exI)
    1.52 -  apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
    1.53 -  done
    1.54 -
    1.55  (*declare not_less[simp] not_le[simp]*)
    1.56  
    1.57  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    1.58 @@ -486,24 +453,24 @@
    1.59  subsection {* Bounds on intervals where they exist. *}
    1.60  
    1.61  definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
    1.62 -  where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
    1.63 +  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
    1.64  
    1.65  definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
    1.66 -  where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
    1.67 +  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
    1.68  
    1.69  lemma interval_upperbound[simp]:
    1.70    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
    1.71      interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
    1.72    unfolding interval_upperbound_def euclidean_representation_setsum
    1.73 -  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
    1.74 -      intro!: cSup_unique)
    1.75 +  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
    1.76 +           intro!: cSup_eq)
    1.77  
    1.78  lemma interval_lowerbound[simp]:
    1.79    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
    1.80      interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
    1.81    unfolding interval_lowerbound_def euclidean_representation_setsum
    1.82 -  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
    1.83 -      intro!: cInf_unique)
    1.84 +  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
    1.85 +           intro!: cInf_eq)
    1.86  
    1.87  lemmas interval_bounds = interval_upperbound interval_lowerbound
    1.88  
    1.89 @@ -6627,7 +6594,7 @@
    1.90  lemma interval_bound_sing[simp]:
    1.91    "interval_upperbound {a} = a"
    1.92    "interval_lowerbound {a} = a"
    1.93 -  unfolding interval_upperbound_def interval_lowerbound_def
    1.94 +  unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
    1.95    by (auto simp: euclidean_representation)
    1.96  
    1.97  lemma additive_tagged_division_1:
    1.98 @@ -11236,37 +11203,26 @@
    1.99  lemma bounded_variation_absolutely_integrable_interval:
   1.100    fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
   1.101    assumes "f integrable_on {a..b}"
   1.102 -    and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   1.103 +    and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   1.104    shows "f absolutely_integrable_on {a..b}"
   1.105  proof -
   1.106 -  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
   1.107 -  def i \<equiv> "Sup ?S"
   1.108 -  have i: "isLub UNIV ?S i"
   1.109 -    unfolding i_def
   1.110 -    apply (rule isLub_cSup)
   1.111 -    apply (rule elementary_interval)
   1.112 -    defer
   1.113 -    apply (rule_tac x=B in exI)
   1.114 -    apply (rule setleI)
   1.115 -    using assms(2)
   1.116 -    apply auto
   1.117 -    done
   1.118 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
   1.119 +  have D_1: "?D \<noteq> {}"
   1.120 +    by (rule elementary_interval[of a b]) auto
   1.121 +  have D_2: "bdd_above (?f`?D)"
   1.122 +    by (metis * mem_Collect_eq bdd_aboveI2)
   1.123 +  note D = D_1 D_2
   1.124 +  let ?S = "SUP x:?D. ?f x"
   1.125    show ?thesis
   1.126      apply rule
   1.127      apply (rule assms)
   1.128      apply rule
   1.129 -    apply (subst has_integral[of _ i])
   1.130 +    apply (subst has_integral[of _ ?S])
   1.131    proof safe
   1.132      case goal1
   1.133 -    then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
   1.134 -      {d. d division_of {a..b}}))"
   1.135 -      using isLub_ubs[OF i,rule_format]
   1.136 -      unfolding setge_def ubs_def
   1.137 -      by auto
   1.138 -    then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
   1.139 -      unfolding mem_Collect_eq isUb_def setle_def
   1.140 -      by (simp add: not_le)
   1.141 -    then guess d .. note d=conjunctD2[OF this]
   1.142 +    then have "?S - e / 2 < ?S" by simp
   1.143 +    then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
   1.144 +      unfolding less_cSUP_iff[OF D] by auto
   1.145      note d' = division_ofD[OF this(1)]
   1.146  
   1.147      have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   1.148 @@ -11451,21 +11407,17 @@
   1.149          done
   1.150        note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
   1.151  
   1.152 -      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
   1.153 -        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
   1.154 +      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
   1.155 +        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
   1.156          by arith
   1.157 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
   1.158 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
   1.159          unfolding real_norm_def
   1.160          apply (rule *[rule_format,OF **])
   1.161          apply safe
   1.162          apply(rule d(2))
   1.163        proof -
   1.164 -        case goal1
   1.165 -        show ?case unfolding sum_p'
   1.166 -          apply (rule isLubD2[OF i])
   1.167 -          using division_of_tagged_division[OF p'']
   1.168 -          apply auto
   1.169 -          done
   1.170 +        case goal1 show ?case
   1.171 +          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
   1.172        next
   1.173          case goal2
   1.174          have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
   1.175 @@ -11756,18 +11708,13 @@
   1.176      and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   1.177    shows "f absolutely_integrable_on UNIV"
   1.178  proof (rule absolutely_integrable_onI, fact, rule)
   1.179 -  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}"
   1.180 -  def i \<equiv> "Sup ?S"
   1.181 -  have i: "isLub UNIV ?S i"
   1.182 -    unfolding i_def
   1.183 -    apply (rule isLub_cSup)
   1.184 -    apply (rule elementary_interval)
   1.185 -    defer
   1.186 -    apply (rule_tac x=B in exI)
   1.187 -    apply (rule setleI)
   1.188 -    using assms(2)
   1.189 -    apply auto
   1.190 -    done
   1.191 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
   1.192 +  have D_1: "?D \<noteq> {}"
   1.193 +    by (rule elementary_interval) auto
   1.194 +  have D_2: "bdd_above (?f`?D)"
   1.195 +    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   1.196 +  note D = D_1 D_2
   1.197 +  let ?S = "SUP d:?D. ?f d"
   1.198    have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
   1.199      apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
   1.200      apply (rule integrable_on_subinterval[OF assms(1)])
   1.201 @@ -11776,7 +11723,7 @@
   1.202      apply (rule assms(2)[rule_format])
   1.203      apply auto
   1.204      done
   1.205 -  show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
   1.206 +  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
   1.207      apply (subst has_integral_alt')
   1.208      apply safe
   1.209    proof -
   1.210 @@ -11785,16 +11732,11 @@
   1.211        using f_int[of a b] by auto
   1.212    next
   1.213      case goal2
   1.214 -    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
   1.215 +    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
   1.216      proof (rule ccontr)
   1.217        assume "\<not> ?thesis"
   1.218 -      then have "i \<le> i - e"
   1.219 -        apply -
   1.220 -        apply (rule isLub_le_isUb[OF i])
   1.221 -        apply (rule isUbI)
   1.222 -        unfolding setle_def
   1.223 -        apply auto
   1.224 -        done
   1.225 +      then have "?S \<le> ?S - e"
   1.226 +        by (intro cSUP_least[OF D(1)]) auto
   1.227        then show False
   1.228          using goal2 by auto
   1.229      qed
   1.230 @@ -11811,9 +11753,9 @@
   1.231      proof -
   1.232        fix a b :: 'n
   1.233        assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
   1.234 -      have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
   1.235 +      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
   1.236          by arith
   1.237 -      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
   1.238 +      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
   1.239          unfolding real_norm_def
   1.240          apply (rule *[rule_format])
   1.241          apply safe
   1.242 @@ -11865,10 +11807,10 @@
   1.243          from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
   1.244          from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
   1.245          note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
   1.246 -        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
   1.247 -          abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
   1.248 +        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
   1.249 +          abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
   1.250            by arith
   1.251 -        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
   1.252 +        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
   1.253            apply (subst if_P)
   1.254            apply rule
   1.255          proof (rule *[rule_format])
   1.256 @@ -11891,18 +11833,12 @@
   1.257              apply (subst abs_of_nonneg)
   1.258              apply auto
   1.259              done
   1.260 -          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
   1.261 +          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
   1.262 +            using partial_division_of_tagged_division[of p "{a..b}"] p(1)
   1.263              apply (subst setsum_over_tagged_division_lemma[OF p(1)])
   1.264 -            defer
   1.265 -            apply (rule isLubD2[OF i])
   1.266 -            unfolding image_iff
   1.267 -            apply (rule_tac x="snd ` p" in bexI)
   1.268 -            unfolding mem_Collect_eq
   1.269 -            defer
   1.270 -            apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
   1.271 -            using p(1)
   1.272 -            unfolding tagged_division_of_def
   1.273 -            apply auto
   1.274 +            apply (simp add: integral_null)
   1.275 +            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
   1.276 +            apply (auto simp: tagged_partial_division_of_def)
   1.277              done
   1.278          qed
   1.279        qed
   1.280 @@ -12378,11 +12314,22 @@
   1.281  lemma dominated_convergence:
   1.282    fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
   1.283    assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
   1.284 -    and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
   1.285 +    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
   1.286      and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
   1.287    shows "g integrable_on s"
   1.288      and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   1.289  proof -
   1.290 +  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
   1.291 +  proof (safe intro!: bdd_belowI)
   1.292 +    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
   1.293 +      using assms(3)[rule_format, of x n] by simp
   1.294 +  qed
   1.295 +  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
   1.296 +  proof (safe intro!: bdd_aboveI)
   1.297 +    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
   1.298 +      using assms(3)[rule_format, of x n] by simp
   1.299 +  qed
   1.300 +
   1.301    have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
   1.302      ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
   1.303      integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
   1.304 @@ -12422,66 +12369,32 @@
   1.305      fix x
   1.306      assume x: "x \<in> s"
   1.307      show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
   1.308 -      apply (rule cInf_ge)
   1.309 -      unfolding setge_def
   1.310 -      defer
   1.311 -      apply rule
   1.312 -      apply (subst cInf_finite_le_iff)
   1.313 -      prefer 3
   1.314 -      apply (rule_tac x=xa in bexI)
   1.315 -      apply auto
   1.316 -      done
   1.317 -    let ?S = "{f j x| j.  m \<le> j}"
   1.318 -    def i \<equiv> "Inf ?S"
   1.319 -    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
   1.320 +      by (rule cInf_superset_mono) auto
   1.321 +    let ?S = "{f j x| j. m \<le> j}"
   1.322 +    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
   1.323      proof (rule LIMSEQ_I)
   1.324        case goal1
   1.325        note r = this
   1.326 -      have i: "isGlb UNIV ?S i"
   1.327 -        unfolding i_def
   1.328 -        apply (rule Inf)
   1.329 -        defer
   1.330 -        apply (rule_tac x="- h x - 1" in exI)
   1.331 -        unfolding setge_def
   1.332 -      proof safe
   1.333 -        case goal1
   1.334 -        then show ?case using assms(3)[rule_format,OF x, of j] by auto
   1.335 -      qed auto
   1.336 -
   1.337 -      have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
   1.338 -      proof(rule ccontr)
   1.339 -        assume "\<not> ?thesis"
   1.340 -        then have "i \<ge> i + r"
   1.341 -          apply -
   1.342 -          apply (rule isGlb_le_isLb[OF i])
   1.343 -          apply (rule isLbI)
   1.344 -          unfolding setge_def
   1.345 -          apply fastforce+
   1.346 -          done
   1.347 -        then show False using r by auto
   1.348 -      qed
   1.349 -      then guess y .. note y=this[unfolded not_le]
   1.350 -      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
   1.351 +
   1.352 +      have "\<exists>y\<in>?S. y < Inf ?S + r"
   1.353 +        by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
   1.354 +      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
   1.355 +        by blast
   1.356  
   1.357        show ?case
   1.358          apply (rule_tac x=N in exI)
   1.359        proof safe
   1.360          case goal1
   1.361 -        have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
   1.362 +        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
   1.363            by arith
   1.364          show ?case
   1.365            unfolding real_norm_def
   1.366 -            apply (rule *[rule_format,OF y(2)])
   1.367 -            unfolding i_def
   1.368 -            apply (rule real_le_inf_subset)
   1.369 -            prefer 3
   1.370 -            apply (rule,rule isGlbD1[OF i])
   1.371 -            prefer 3
   1.372 -            apply (subst cInf_finite_le_iff)
   1.373 -            prefer 3
   1.374 -            apply (rule_tac x=y in bexI)
   1.375 +            apply (rule *[rule_format, OF N(1)])
   1.376 +            apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
   1.377 +            apply (rule cInf_lower)
   1.378              using N goal1
   1.379 -            apply auto
   1.380 +            apply auto []
   1.381 +            apply simp
   1.382              done
   1.383        qed
   1.384      qed
   1.385 @@ -12525,65 +12438,27 @@
   1.386      fix x
   1.387      assume x: "x\<in>s"
   1.388      show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
   1.389 -      apply (rule cSup_le)
   1.390 -      unfolding setle_def
   1.391 -      defer
   1.392 -      apply rule
   1.393 -      apply (subst cSup_finite_ge_iff)
   1.394 -      prefer 3
   1.395 -      apply (rule_tac x=y in bexI)
   1.396 -      apply auto
   1.397 -      done
   1.398 -    let ?S = "{f j x| j.  m \<le> j}"
   1.399 -    def i \<equiv> "Sup ?S"
   1.400 -    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
   1.401 +      by (rule cSup_subset_mono) auto
   1.402 +    let ?S = "{f j x| j. m \<le> j}"
   1.403 +    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
   1.404      proof (rule LIMSEQ_I)
   1.405        case goal1 note r=this
   1.406 -      have i: "isLub UNIV ?S i"
   1.407 -        unfolding i_def
   1.408 -        apply (rule isLub_cSup)
   1.409 -        defer
   1.410 -        apply (rule_tac x="h x" in exI)
   1.411 -        unfolding setle_def
   1.412 -      proof safe
   1.413 -        case goal1
   1.414 -        then show ?case
   1.415 -          using assms(3)[rule_format,OF x, of j] by auto
   1.416 -      qed auto
   1.417 -
   1.418 -      have "\<exists>y\<in>?S. \<not> y \<le> i - r"
   1.419 -      proof (rule ccontr)
   1.420 -        assume "\<not> ?thesis"
   1.421 -        then have "i \<le> i - r"
   1.422 -          apply -
   1.423 -          apply (rule isLub_le_isUb[OF i])
   1.424 -          apply (rule isUbI)
   1.425 -          unfolding setle_def
   1.426 -          apply fastforce+
   1.427 -          done
   1.428 -        then show False
   1.429 -          using r by auto
   1.430 -      qed
   1.431 -      then guess y .. note y=this[unfolded not_le]
   1.432 -      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
   1.433 +      have "\<exists>y\<in>?S. Sup ?S - r < y"
   1.434 +        by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
   1.435 +      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
   1.436 +        by blast
   1.437  
   1.438        show ?case
   1.439          apply (rule_tac x=N in exI)
   1.440        proof safe
   1.441          case goal1
   1.442 -        have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
   1.443 +        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
   1.444            by arith
   1.445          show ?case
   1.446 -          unfolding real_norm_def
   1.447 -          apply (rule *[rule_format,OF y(2)])
   1.448 -          unfolding i_def
   1.449 -          apply (rule real_ge_sup_subset)
   1.450 -          prefer 3
   1.451 -          apply (rule, rule isLubD1[OF i])
   1.452 -          prefer 3
   1.453 -          apply (subst cSup_finite_ge_iff)
   1.454 -          prefer 3
   1.455 -          apply (rule_tac x = y in bexI)
   1.456 +          apply simp
   1.457 +          apply (rule *[rule_format, OF N(1)])
   1.458 +          apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
   1.459 +          apply (subst cSup_upper)
   1.460            using N goal1
   1.461            apply auto
   1.462            done
   1.463 @@ -12616,17 +12491,7 @@
   1.464  
   1.465      have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
   1.466      show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
   1.467 -      apply -
   1.468 -      apply (rule real_le_inf_subset)
   1.469 -      prefer 3
   1.470 -      unfolding setge_def
   1.471 -      apply (rule_tac x="- h x" in exI)
   1.472 -      apply safe
   1.473 -      apply (rule *)
   1.474 -      using assms(3)[rule_format,OF x]
   1.475 -      unfolding real_norm_def abs_le_iff
   1.476 -      apply auto
   1.477 -      done
   1.478 +      by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
   1.479  
   1.480      show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
   1.481      proof (rule LIMSEQ_I)
   1.482 @@ -12674,16 +12539,7 @@
   1.483      assume x: "x \<in> s"
   1.484  
   1.485      show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
   1.486 -      apply -
   1.487 -      apply (rule real_ge_sup_subset)
   1.488 -      prefer 3
   1.489 -      unfolding setle_def
   1.490 -      apply (rule_tac x="h x" in exI)
   1.491 -      apply safe
   1.492 -      using assms(3)[rule_format,OF x]
   1.493 -      unfolding real_norm_def abs_le_iff
   1.494 -      apply auto
   1.495 -      done
   1.496 +      by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
   1.497      show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
   1.498      proof (rule LIMSEQ_I)
   1.499        case goal1
   1.500 @@ -12712,41 +12568,18 @@
   1.501      from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
   1.502      from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
   1.503      show ?case
   1.504 -      apply (rule_tac x="N1+N2" in exI, safe)
   1.505 -    proof -
   1.506 +    proof (rule_tac x="N1+N2" in exI, safe)
   1.507        fix n
   1.508        assume n: "n \<ge> N1 + N2"
   1.509        have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
   1.510          by arith
   1.511        show "norm (integral s (f n) - integral s g) < r"
   1.512          unfolding real_norm_def
   1.513 -        apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
   1.514 -      proof -
   1.515 +      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
   1.516          show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
   1.517 -        proof (rule integral_le[OF dec1(1) assms(1)], safe)
   1.518 -          fix x
   1.519 -          assume x: "x \<in> s"
   1.520 -          have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
   1.521 -          show "Inf {f j x |j. n \<le> j} \<le> f n x"
   1.522 -            apply (intro cInf_lower bdd_belowI)
   1.523 -            apply auto []
   1.524 -            apply (rule *)
   1.525 -            using assms(3)[rule_format,OF x]
   1.526 -            unfolding real_norm_def abs_le_iff
   1.527 -            apply auto
   1.528 -            done
   1.529 -        qed
   1.530 +          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
   1.531          show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
   1.532 -        proof (rule integral_le[OF assms(1) inc1(1)], safe)
   1.533 -          fix x
   1.534 -          assume x: "x \<in> s"
   1.535 -          show "f n x \<le> Sup {f j x |j. n \<le> j}"
   1.536 -            apply (rule cSup_upper)
   1.537 -            using assms(3)[rule_format,OF x]
   1.538 -            unfolding real_norm_def abs_le_iff
   1.539 -            apply auto
   1.540 -            done
   1.541 -        qed
   1.542 +          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
   1.543        qed (insert n, auto)
   1.544      qed
   1.545    qed