--- a/src/HOL/Library/Extended_Real.thy Tue Mar 05 15:43:21 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Mar 05 15:43:22 2013 +0100
@@ -131,10 +131,11 @@
subsubsection "Addition"
-instantiation ereal :: comm_monoid_add
+instantiation ereal :: "{one, comm_monoid_add}"
begin
definition "0 = ereal 0"
+definition "1 = ereal 1"
function plus_ereal where
"ereal r + ereal p = ereal (r + p)" |
@@ -173,6 +174,8 @@
qed
end
+instance ereal :: numeral ..
+
lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
unfolding real_of_ereal_def zero_ereal_def by simp
@@ -474,9 +477,7 @@
instantiation ereal :: "{comm_monoid_mult, sgn}"
begin
-definition "1 = ereal 1"
-
-function sgn_ereal where
+function sgn_ereal :: "ereal \<Rightarrow> ereal" where
"sgn (ereal r) = ereal (sgn r)"
| "sgn (\<infinity>::ereal) = 1"
| "sgn (-\<infinity>::ereal) = -1"
@@ -661,8 +662,6 @@
using assms
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
-instance ereal :: numeral ..
-
lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
apply (induct w rule: num_induct)
apply (simp only: numeral_One one_ereal_def)
@@ -1811,9 +1810,16 @@
"f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
by (intro LIMSEQ_le_const2) auto
+lemma Lim_bounded2_ereal:
+ assumes lim:"f ----> (l :: 'a::linorder_topology)" and ge: "ALL n>=N. f n >= C"
+ shows "l>=C"
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
+
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal shows "real (a * b) = real a * real b"
by (cases rule: ereal2_cases[of a b]) auto