A few lemmas about summations, etc.
authorpaulson <lp15@cam.ac.uk>
Mon Feb 24 15:45:55 2014 +0000 (2014-02-24)
changeset 5571834618f031ba9
parent 55717 601ea66c5bcd
child 55719 cdddd073bff8
A few lemmas about summations, etc.
src/HOL/Fields.thy
src/HOL/Power.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Fields.thy	Mon Feb 24 13:52:48 2014 +0100
     1.2 +++ b/src/HOL/Fields.thy	Mon Feb 24 15:45:55 2014 +0000
     1.3 @@ -1156,6 +1156,12 @@
     1.4    apply (simp add: order_less_imp_le)
     1.5  done
     1.6  
     1.7 +lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)" 
     1.8 +by (auto simp: zero_le_divide_iff)
     1.9 +
    1.10 +lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)" 
    1.11 +by (auto simp: divide_le_0_iff)
    1.12 +
    1.13  lemma field_le_mult_one_interval:
    1.14    assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
    1.15    shows "x \<le> y"
     2.1 --- a/src/HOL/Power.thy	Mon Feb 24 13:52:48 2014 +0100
     2.2 +++ b/src/HOL/Power.thy	Mon Feb 24 15:45:55 2014 +0000
     2.3 @@ -610,6 +610,11 @@
     2.4  
     2.5  subsection {* Miscellaneous rules *}
     2.6  
     2.7 +lemma self_le_power:
     2.8 +  fixes x::"'a::linordered_semidom" 
     2.9 +  shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
    2.10 +  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
    2.11 +
    2.12  lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
    2.13    unfolding One_nat_def by (cases m) simp_all
    2.14  
     3.1 --- a/src/HOL/Set_Interval.thy	Mon Feb 24 13:52:48 2014 +0100
     3.2 +++ b/src/HOL/Set_Interval.thy	Mon Feb 24 15:45:55 2014 +0000
     3.3 @@ -1459,6 +1459,14 @@
     3.4    finally show ?case .
     3.5  qed
     3.6  
     3.7 +lemma setsum_last_plus: "n \<noteq> 0 \<Longrightarrow> (\<Sum>i = 0..n. f i) = f n + (\<Sum>i = 0..n - Suc 0. f i)"
     3.8 +  using atLeastAtMostSuc_conv [of 0 "n - 1"]
     3.9 +  by auto
    3.10 +
    3.11 +lemma nested_setsum_swap:
    3.12 +     "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
    3.13 +  by (induction n) (auto simp: setsum_addf)
    3.14 +
    3.15  
    3.16  subsection {* The formula for geometric sums *}
    3.17  
    3.18 @@ -1565,6 +1573,14 @@
    3.19    show ?case by simp
    3.20  qed
    3.21  
    3.22 +lemma nat_diff_setsum_reindex:
    3.23 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    3.24 +  shows "(\<Sum>i=0..<n. f (n - Suc i)) = (\<Sum>i=0..<n. f i)"
    3.25 +apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{0..< n}"])
    3.26 +apply (auto simp: inj_on_def)
    3.27 +apply (rule_tac x="n - Suc x" in image_eqI, auto)
    3.28 +done
    3.29 +
    3.30  subsection {* Products indexed over intervals *}
    3.31  
    3.32  syntax
    3.33 @@ -1649,4 +1665,9 @@
    3.34      by auto
    3.35  qed
    3.36  
    3.37 +lemma setprod_power_distrib:
    3.38 +  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
    3.39 +  shows "finite A \<Longrightarrow> setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
    3.40 +  by (induct set: finite) (auto simp: power_mult_distrib)
    3.41 +
    3.42  end