add lemmas for extended nats and reals
authorAndreas Lochbihler
Wed Nov 11 10:07:27 2015 +0100 (2015-11-11)
changeset 616314f7ef088c4ed
parent 61630 608520e0e8e2
child 61632 ec580491c5d2
add lemmas for extended nats and reals
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 09:48:24 2015 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 10:07:27 2015 +0100
     1.3 @@ -459,6 +459,10 @@
     1.4  lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
     1.5    by (cases n) simp_all
     1.6  
     1.7 +lemma iadd_le_enat_iff:
     1.8 +  "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)"
     1.9 +by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
    1.10 +
    1.11  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
    1.12  apply (induct_tac k)
    1.13   apply (simp (no_asm) only: enat_0)
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Nov 11 09:48:24 2015 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Nov 11 10:07:27 2015 +0100
     2.3 @@ -311,7 +311,6 @@
     2.4    shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
     2.5    by auto
     2.6  
     2.7 -
     2.8  subsubsection "Addition"
     2.9  
    2.10  instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
    2.11 @@ -593,6 +592,11 @@
    2.12  lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
    2.13    by (cases x) auto
    2.14  
    2.15 +lemma ereal_abs_leI:
    2.16 +  fixes x y :: ereal 
    2.17 +  shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
    2.18 +by(cases x y rule: ereal2_cases)(simp_all)
    2.19 +
    2.20  lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
    2.21    by (cases x) auto
    2.22  
    2.23 @@ -877,6 +881,11 @@
    2.24  
    2.25  end
    2.26  
    2.27 +lemma [simp]: 
    2.28 +  shows ereal_1_times: "ereal 1 * x = x"
    2.29 +  and times_ereal_1: "x * ereal 1 = x"
    2.30 +by(simp_all add: one_ereal_def[symmetric])
    2.31 +
    2.32  lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
    2.33    by (simp add: one_ereal_def zero_ereal_def)
    2.34  
    2.35 @@ -1045,6 +1054,10 @@
    2.36    apply (simp only: numeral_inc ereal_plus_1)
    2.37    done
    2.38  
    2.39 +lemma distrib_left_ereal_nn:
    2.40 +  "c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c"
    2.41 +by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)
    2.42 +
    2.43  lemma setsum_ereal_right_distrib:
    2.44    fixes f :: "'a \<Rightarrow> ereal"
    2.45    shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
    2.46 @@ -1054,6 +1067,10 @@
    2.47    "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
    2.48    using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
    2.49  
    2.50 +lemma setsum_left_distrib_ereal:
    2.51 +  "c \<ge> 0 \<Longrightarrow> setsum f A * ereal c = (\<Sum>x\<in>A. f x * c :: ereal)"
    2.52 +by(subst setsum_comp_morphism[where h="\<lambda>x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn)
    2.53 +
    2.54  lemma ereal_le_epsilon:
    2.55    fixes x y :: ereal
    2.56    assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
    2.57 @@ -1384,6 +1401,26 @@
    2.58    shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
    2.59    by (cases x y rule: ereal2_cases) simp_all
    2.60  
    2.61 +lemma ereal_diff_add_eq_diff_diff_swap:
    2.62 +  fixes x y z :: ereal 
    2.63 +  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z"
    2.64 +by(cases x y z rule: ereal3_cases) simp_all
    2.65 +
    2.66 +lemma ereal_diff_add_assoc2:
    2.67 +  fixes x y z :: ereal
    2.68 +  shows "x + y - z = x - z + y"
    2.69 +by(cases x y z rule: ereal3_cases) simp_all
    2.70 +
    2.71 +lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
    2.72 +by(cases x y rule: ereal2_cases) simp_all
    2.73 +
    2.74 +lemma ereal_minus_diff_eq: 
    2.75 +  fixes x y :: ereal 
    2.76 +  shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
    2.77 +by(cases x y rule: ereal2_cases) simp_all
    2.78 +
    2.79 +lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
    2.80 +by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
    2.81  
    2.82  subsubsection \<open>Division\<close>
    2.83  
    2.84 @@ -1451,6 +1488,9 @@
    2.85  lemma ereal_inverse_nonneg_iff: "0 \<le> inverse (x :: ereal) \<longleftrightarrow> 0 \<le> x \<or> x = -\<infinity>"
    2.86    by (cases x) auto
    2.87  
    2.88 +lemma inverse_ereal_ge0I: "0 \<le> (x :: ereal) \<Longrightarrow> 0 \<le> inverse x"
    2.89 +by(cases x) simp_all
    2.90 +
    2.91  lemma zero_le_divide_ereal[simp]:
    2.92    fixes a :: ereal
    2.93    assumes "0 \<le> a"
    2.94 @@ -2191,6 +2231,9 @@
    2.95  lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
    2.96  lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
    2.97  
    2.98 +lemma ereal_of_enat_nonneg: "ereal_of_enat n \<ge> 0"
    2.99 +by(cases n) simp_all
   2.100 +
   2.101  lemma ereal_of_enat_Sup:
   2.102    assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
   2.103  proof (intro antisym mono_Sup)
   2.104 @@ -2808,6 +2851,10 @@
   2.105    qed
   2.106  qed
   2.107  
   2.108 +lemma Sup_ereal_mult_left':
   2.109 +  "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i:Y. f i) = (SUP i:Y. ereal x * f i)"
   2.110 +by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
   2.111 +
   2.112  lemma sup_continuous_add[order_continuous_intros]:
   2.113    fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
   2.114    assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"