author Andreas Lochbihler Tue, 14 Apr 2015 11:44:17 +0200 changeset 60060 3630ecde4e7c parent 60059 8a6d947cc756 child 60061 279472fa0b1d
```--- a/src/HOL/Library/Extended_Real.thy	Tue Apr 14 11:36:03 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Apr 14 11:44:17 2015 +0200
@@ -298,6 +298,10 @@

end

+lemma ereal_0_plus [simp]: "ereal 0 + x = x"
+  and plus_ereal_0 [simp]: "x + ereal 0 = x"
+
instance ereal :: numeral ..

lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
@@ -1286,6 +1290,9 @@
shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
by (cases rule: ereal2_cases[of a b]) auto

+lemma real_of_ereal_minus': "\<bar>x\<bar> = \<infinity> \<longleftrightarrow> \<bar>y\<bar> = \<infinity> \<Longrightarrow> real x - real y = real (x - y :: ereal)"
+by(subst real_of_ereal_minus) auto
+
lemma ereal_diff_positive:
fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b - a"
by (cases rule: ereal2_cases[of a b]) auto
@@ -1428,6 +1435,14 @@
shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
by (cases x) auto

+lemma ereal_inverse_le_0_iff:
+  fixes x :: ereal
+  shows "inverse x \<le> 0 \<longleftrightarrow> x < 0 \<or> x = \<infinity>"
+  by(cases x) auto
+
+lemma ereal_divide_eq_0_iff: "x / y = 0 \<longleftrightarrow> x = 0 \<or> \<bar>y :: ereal\<bar> = \<infinity>"
+by(cases x y rule: ereal2_cases) simp_all
+
lemma ereal_mult_less_right:
fixes a b c :: ereal
assumes "b * a < c * a"
@@ -1971,7 +1986,7 @@
assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
proof cases
-  assume "(SUP i:I. f i) = 0"
+  assume "(SUP i: I. f i) = 0"
moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
by (metis SUP_upper f antisym)
ultimately show ?thesis
@@ -2646,6 +2661,38 @@
finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
qed

+lemma Sup_ereal_mult_right':
+  assumes nonempty: "Y \<noteq> {}"
+  and x: "x \<ge> 0"
+  shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
+proof(cases "x = 0")
+  case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
+next
+  case False
+  show ?thesis
+  proof(rule antisym)
+    show "?rhs \<le> ?lhs"
+      by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
+  next
+    have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
+    also have "\<dots> = (SUP i:Y. f i)" using False by simp
+    also have "\<dots> \<le> ?rhs / x"
+    proof(rule SUP_least)
+      fix i
+      assume "i \<in> Y"
+      have "f i = f i * (ereal x / ereal x)" using False by simp
+      also have "\<dots> = f i * x / x" by(simp only: ereal_times_divide_eq)
+      also from \<open>i \<in> Y\<close> have "f i * x \<le> ?rhs" by(rule SUP_upper)
+      hence "f i * x / x \<le> ?rhs / x" using x False by simp
+      finally show "f i \<le> ?rhs / x" .
+    qed
+    finally have "(?lhs / x) * x \<le> (?rhs / x) * x"