# HG changeset patch # User Andreas Lochbihler # Date 1447232847 -3600 # Node ID 4f7ef088c4eddba1a6734b85eb5b3a3fbb893dba # Parent 608520e0e8e28ea3d23dfa53990140b583c1eaae add lemmas for extended nats and reals diff -r 608520e0e8e2 -r 4f7ef088c4ed src/HOL/Library/Extended_Nat.thy --- 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 \ \k. n = enat k" by (cases n) simp_all +lemma iadd_le_enat_iff: + "x + y \ enat n \ (\y' x'. x = enat x' \ y = enat y' \ x' + y' \ n)" +by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all + lemma chain_incr: "\i. \j. Y i < Y j ==> \j. enat k < Y j" apply (induct_tac k) apply (simp (no_asm) only: enat_0) diff -r 608520e0e8e2 -r 4f7ef088c4ed src/HOL/Library/Extended_Real.thy --- 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 \ \ \ a \ -\ \ \a\ \ \" by auto - subsubsection "Addition" instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}" @@ -593,6 +592,11 @@ lemma abs_ereal_pos[simp]: "0 \ \x :: ereal\" by (cases x) auto +lemma ereal_abs_leI: + fixes x y :: ereal + shows "\ x \ y; -x \ y \ \ \x\ \ y" +by(cases x y rule: ereal2_cases)(simp_all) + lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \ 0 \ x \ 0 \ x = \" 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]: "\ (1 \ (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 \ 0 \ (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 \ ereal" shows "(\i. i \ A \ 0 \ f i) \ r * setsum f A = (\n\A. r * f n)" @@ -1054,6 +1067,10 @@ "(\i. i \ A \ 0 \ f i) \ setsum f A * r = (\n\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 \ 0 \ setsum f A * ereal c = (\x\A. f x * c :: ereal)" +by(subst setsum_comp_morphism[where h="\x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn) + lemma ereal_le_epsilon: fixes x y :: ereal assumes "\e. 0 < e \ x \ y + e" @@ -1384,6 +1401,26 @@ shows "x - y = \ \ y = -\ \ x = \" by (cases x y rule: ereal2_cases) simp_all +lemma ereal_diff_add_eq_diff_diff_swap: + fixes x y z :: ereal + shows "\y\ \ \ \ 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 "\ x = \ \ y \ \; x = -\ \ y \ - \ \ \ - (x - y) = y - x" +by(cases x y rule: ereal2_cases) simp_all + +lemma ediff_le_self [simp]: "x - y \ (x :: enat)" +by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all subsubsection \Division\ @@ -1451,6 +1488,9 @@ lemma ereal_inverse_nonneg_iff: "0 \ inverse (x :: ereal) \ 0 \ x \ x = -\" by (cases x) auto +lemma inverse_ereal_ge0I: "0 \ (x :: ereal) \ 0 \ inverse x" +by(cases x) simp_all + lemma zero_le_divide_ereal[simp]: fixes a :: ereal assumes "0 \ 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 \ 0" +by(cases n) simp_all + lemma ereal_of_enat_Sup: assumes "A \ {}" 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': + "\ Y \ {}; x \ 0 \ \ 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 \ ereal" assumes nn: "\x. 0 \ f x" "\x. 0 \ g x" and cont: "sup_continuous f" "sup_continuous g"