add lemmas for extended nats and reals

--- a/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 09:48:24 2015 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 10:07:27 2015 +0100
@@ -459,6 +459,10 @@
 lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
   by (cases n) simp_all
 
+lemma iadd_le_enat_iff:
+  "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)"
+by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
+
 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
 apply (induct_tac k)
  apply (simp (no_asm) only: enat_0)

--- a/src/HOL/Library/Extended_Real.thy	Wed Nov 11 09:48:24 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Nov 11 10:07:27 2015 +0100
@@ -311,7 +311,6 @@
   shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
   by auto
 
-
 subsubsection "Addition"
 
 instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
@@ -593,6 +592,11 @@
 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
   by (cases x) auto
 
+lemma ereal_abs_leI:
+  fixes x y :: ereal 
+  shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
+by(cases x y rule: ereal2_cases)(simp_all)
+
 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
   by (cases x) auto
 
@@ -877,6 +881,11 @@
 
 end
 
+lemma [simp]: 
+  shows ereal_1_times: "ereal 1 * x = x"
+  and times_ereal_1: "x * ereal 1 = x"
+by(simp_all add: one_ereal_def[symmetric])
+
 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
   by (simp add: one_ereal_def zero_ereal_def)
 
@@ -1045,6 +1054,10 @@
   apply (simp only: numeral_inc ereal_plus_1)
   done
 
+lemma distrib_left_ereal_nn:
+  "c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c"
+by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)
+
 lemma setsum_ereal_right_distrib:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
@@ -1054,6 +1067,10 @@
   "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
   using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
 
+lemma setsum_left_distrib_ereal:
+  "c \<ge> 0 \<Longrightarrow> setsum f A * ereal c = (\<Sum>x\<in>A. f x * c :: ereal)"
+by(subst setsum_comp_morphism[where h="\<lambda>x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn)
+
 lemma ereal_le_epsilon:
   fixes x y :: ereal
   assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
@@ -1384,6 +1401,26 @@
   shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
   by (cases x y rule: ereal2_cases) simp_all
 
+lemma ereal_diff_add_eq_diff_diff_swap:
+  fixes x y z :: ereal 
+  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z"
+by(cases x y z rule: ereal3_cases) simp_all
+
+lemma ereal_diff_add_assoc2:
+  fixes x y z :: ereal
+  shows "x + y - z = x - z + y"
+by(cases x y z rule: ereal3_cases) simp_all
+
+lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
+by(cases x y rule: ereal2_cases) simp_all
+
+lemma ereal_minus_diff_eq: 
+  fixes x y :: ereal 
+  shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
+by(cases x y rule: ereal2_cases) simp_all
+
+lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
+by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
 
 subsubsection \<open>Division\<close>
 
@@ -1451,6 +1488,9 @@
 lemma ereal_inverse_nonneg_iff: "0 \<le> inverse (x :: ereal) \<longleftrightarrow> 0 \<le> x \<or> x = -\<infinity>"
   by (cases x) auto
 
+lemma inverse_ereal_ge0I: "0 \<le> (x :: ereal) \<Longrightarrow> 0 \<le> inverse x"
+by(cases x) simp_all
+
 lemma zero_le_divide_ereal[simp]:
   fixes a :: ereal
   assumes "0 \<le> a"
@@ -2191,6 +2231,9 @@
 lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
 lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
 
+lemma ereal_of_enat_nonneg: "ereal_of_enat n \<ge> 0"
+by(cases n) simp_all
+
 lemma ereal_of_enat_Sup:
   assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
 proof (intro antisym mono_Sup)
@@ -2808,6 +2851,10 @@
   qed
 qed
 
+lemma Sup_ereal_mult_left':
+  "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i:Y. f i) = (SUP i:Y. ereal x * f i)"
+by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
+
 lemma sup_continuous_add[order_continuous_intros]:
   fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
   assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"