src/HOL/Library/Extended_Real.thy
changeset 44918 6a80fbc4e72c
parent 44890 22f665a2e91c
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 13 13:17:52 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 13 16:21:48 2011 +0200
     1.3 @@ -1506,7 +1506,8 @@
     1.4        proof cases
     1.5          assume "\<forall>i. f i = 0"
     1.6          moreover then have "range f = {0}" by auto
     1.7 -        ultimately show "c * SUPR UNIV f \<le> y" using * by (auto simp: SUPR_def)
     1.8 +        ultimately show "c * SUPR UNIV f \<le> y" using *
     1.9 +          by (auto simp: SUPR_def min_max.sup_absorb1)
    1.10        next
    1.11          assume "\<not> (\<forall>i. f i = 0)"
    1.12          then obtain i where "f i \<noteq> 0" by auto
    1.13 @@ -1568,7 +1569,8 @@
    1.14          hence "0 < r" using `0 < e` by auto
    1.15          then obtain n ::nat where *: "1 / real n < r" "0 < n"
    1.16            using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide)
    1.17 -        have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n] by auto
    1.18 +        have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n]
    1.19 +          by auto
    1.20          also have "1 / ereal (real n) \<le> e" using real * by (auto simp: one_ereal_def )
    1.21          with bound have "f n + 1 / ereal (real n) \<le> y + e" by (rule add_mono) simp
    1.22          finally show "Sup A \<le> y + e" .
    1.23 @@ -1625,7 +1627,7 @@
    1.24    then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
    1.25    show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
    1.26    proof (cases a)
    1.27 -    case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant)
    1.28 +    case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1)
    1.29    next
    1.30      case (real r)
    1.31      then have **: "op + (- a) ` op + a ` A = A"