89 lemma ereal_uminus_eq_iff[simp]: |
89 lemma ereal_uminus_eq_iff[simp]: |
90 fixes a b :: ereal |
90 fixes a b :: ereal |
91 shows "-a = -b \<longleftrightarrow> a = b" |
91 shows "-a = -b \<longleftrightarrow> a = b" |
92 by (cases rule: ereal2_cases[of a b]) simp_all |
92 by (cases rule: ereal2_cases[of a b]) simp_all |
93 |
93 |
94 function of_ereal :: "ereal \<Rightarrow> real" where |
94 instantiation ereal :: real_of |
95 "of_ereal (ereal r) = r" |
95 begin |
96 | "of_ereal \<infinity> = 0" |
96 |
97 | "of_ereal (-\<infinity>) = 0" |
97 function real_ereal :: "ereal \<Rightarrow> real" where |
|
98 "real_ereal (ereal r) = r" |
|
99 | "real_ereal \<infinity> = 0" |
|
100 | "real_ereal (-\<infinity>) = 0" |
98 by (auto intro: ereal_cases) |
101 by (auto intro: ereal_cases) |
99 termination by default (rule wf_empty) |
102 termination by default (rule wf_empty) |
100 |
103 |
101 defs (overloaded) |
104 instance .. |
102 real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal" |
105 end |
103 |
106 |
104 lemma real_of_ereal[simp]: |
107 lemma real_of_ereal[simp]: |
105 "real (- x :: ereal) = - (real x)" |
108 "real (- x :: ereal) = - (real x)" |
106 "real (ereal r) = r" |
109 by (cases x) simp_all |
107 "real (\<infinity>::ereal) = 0" |
|
108 by (cases x) (simp_all add: real_of_ereal_def) |
|
109 |
110 |
110 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}" |
111 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}" |
111 proof safe |
112 proof safe |
112 fix x |
113 fix x |
113 assume "x \<notin> range ereal" "x \<noteq> \<infinity>" |
114 assume "x \<notin> range ereal" "x \<noteq> \<infinity>" |
214 end |
215 end |
215 |
216 |
216 instance ereal :: numeral .. |
217 instance ereal :: numeral .. |
217 |
218 |
218 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" |
219 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" |
219 unfolding real_of_ereal_def zero_ereal_def by simp |
220 unfolding zero_ereal_def by simp |
220 |
221 |
221 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)" |
222 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)" |
222 unfolding zero_ereal_def abs_ereal.simps by simp |
223 unfolding zero_ereal_def abs_ereal.simps by simp |
223 |
224 |
224 lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)" |
225 lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)" |