--- a/src/HOL/Library/Extended_Real.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Nov 16 18:45:57 2012 +0100
@@ -124,7 +124,6 @@
fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
qed auto
-
instantiation ereal :: abs
begin
function abs_ereal where
@@ -145,6 +144,9 @@
lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
by (cases x) auto
+lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
+ by auto
+
subsubsection "Addition"
instantiation ereal :: comm_monoid_add
@@ -530,6 +532,9 @@
qed
end
+lemma real_ereal_1[simp]: "real (1::ereal) = 1"
+ unfolding one_ereal_def by simp
+
lemma real_of_ereal_le_1:
fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
by (cases a) (auto simp: one_ereal_def)
@@ -659,6 +664,16 @@
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
+lemma ereal_left_mult_cong:
+ fixes a b c :: ereal
+ shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
+ by (cases "c = 0") simp_all
+
+lemma ereal_right_mult_cong:
+ fixes a b c :: ereal
+ shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
+ by (cases "c = 0") simp_all
+
lemma ereal_distrib:
fixes a b c :: ereal
assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
@@ -941,6 +956,10 @@
using assms apply (cases x, cases e) apply auto
done
+lemma ereal_minus_eq_PInfty_iff:
+ fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
+ by (cases x y rule: ereal2_cases) simp_all
+
subsubsection {* Division *}
instantiation ereal :: inverse