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"
```