# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1393256755 0
# Node ID 34618f031ba9ab9f53ad9f822cd78703366698f2
# Parent  601ea66c5bcdda5c878a0f032b8ae6edf926d92b
A few lemmas about summations, etc.

diff -r 601ea66c5bcd -r 34618f031ba9 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Feb 24 13:52:48 2014 +0100
+++ b/src/HOL/Fields.thy	Mon Feb 24 15:45:55 2014 +0000
@@ -1156,6 +1156,12 @@
   apply (simp add: order_less_imp_le)
 done
 
+lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)" 
+by (auto simp: zero_le_divide_iff)
+
+lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)" 
+by (auto simp: divide_le_0_iff)
+
 lemma field_le_mult_one_interval:
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
   shows "x \<le> y"
diff -r 601ea66c5bcd -r 34618f031ba9 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Feb 24 13:52:48 2014 +0100
+++ b/src/HOL/Power.thy	Mon Feb 24 15:45:55 2014 +0000
@@ -610,6 +610,11 @@
 
 subsection {* Miscellaneous rules *}
 
+lemma self_le_power:
+  fixes x::"'a::linordered_semidom" 
+  shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
+  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
+
 lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 
diff -r 601ea66c5bcd -r 34618f031ba9 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Feb 24 13:52:48 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Feb 24 15:45:55 2014 +0000
@@ -1459,6 +1459,14 @@
   finally show ?case .
 qed
 
+lemma setsum_last_plus: "n \<noteq> 0 \<Longrightarrow> (\<Sum>i = 0..n. f i) = f n + (\<Sum>i = 0..n - Suc 0. f i)"
+  using atLeastAtMostSuc_conv [of 0 "n - 1"]
+  by auto
+
+lemma nested_setsum_swap:
+     "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
+  by (induction n) (auto simp: setsum_addf)
+
 
 subsection {* The formula for geometric sums *}
 
@@ -1565,6 +1573,14 @@
   show ?case by simp
 qed
 
+lemma nat_diff_setsum_reindex:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "(\<Sum>i=0..<n. f (n - Suc i)) = (\<Sum>i=0..<n. f i)"
+apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{0..< n}"])
+apply (auto simp: inj_on_def)
+apply (rule_tac x="n - Suc x" in image_eqI, auto)
+done
+
 subsection {* Products indexed over intervals *}
 
 syntax
@@ -1649,4 +1665,9 @@
     by auto
 qed
 
+lemma setprod_power_distrib:
+  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
+  shows "finite A \<Longrightarrow> setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
+  by (induct set: finite) (auto simp: power_mult_distrib)
+
 end