src/HOL/Library/Extended_Real.thy

--- 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"
+by(simp_all add: zero_ereal_def[symmetric])
+
 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"
+      by(rule ereal_mult_right_mono)(simp add: x)
+    also have "\<dots> = ?rhs" using False ereal_divide_eq mult.commute by force
+    also have "(?lhs / x) * x = ?lhs" using False ereal_divide_eq mult.commute by force
+    finally show "?lhs \<le> ?rhs" .
+  qed
+qed
 
 subsubsection {* Tests for code generator *}