src/HOL/Library/Extended_Nonnegative_Real.thy

   by (simp add: ennreal_mult_eq_top_iff)
 
 lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
   by transfer (simp add: top_ereal_def)
 
-lemma enn2ereal_top: "enn2ereal top = \<infinity>"
+lemma enn2ereal_top[simp]: "enn2ereal top = \<infinity>"
   by transfer (simp add: top_ereal_def)
 
-lemma e2ennreal_infty: "e2ennreal \<infinity> = top"
+lemma e2ennreal_infty[simp]: "e2ennreal \<infinity> = top"
   by (simp add: top_ennreal.abs_eq top_ereal_def)
 
 lemma ennreal_top_minus[simp]: "top - x = (top::ennreal)"
   by transfer (auto simp: top_ereal_def max_def)
 

 lemma enn2ereal_ennreal[simp]: "0 \<le> x \<Longrightarrow> enn2ereal (ennreal x) = x"
   by transfer (simp add: max_absorb2)
 
 lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
   by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
+
+lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
+by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
 
 lemma ennreal_0[simp]: "ennreal 0 = 0"
   by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
 
 lemma ennreal_1[simp]: "ennreal 1 = 1"

   by transfer
      (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
 
 lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
   by (simp add: minus_top_ennreal)
+
+lemma e2eenreal_enn2ereal_diff [simp]:
+  "e2ennreal(enn2ereal x - enn2ereal y) = x - y" for x y
+by (cases x, cases y, auto simp add: ennreal_minus e2ennreal_neg)
 
 lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
   by transfer (simp add: max_absorb2)
 
 lemma ennreal_mult': "0 \<le> a \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"

   fix y :: ennreal assume "y < top"
   then obtain r where "y = ennreal r"
     by (cases y rule: ennreal_cases) auto
   then show "\<exists>i\<in>UNIV. y < of_nat i"
     using reals_Archimedean2[of "max 1 r"] zero_less_one
-    by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
-             dest!: one_less_of_natD intro: less_trans)
+    by (simp add: ennreal_Ex_less_of_nat)
 qed
 
 lemma ennreal_SUP_eq_top:
   fixes f :: "'a \<Rightarrow> ennreal"
   assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"