# HG changeset patch
# User ballarin
# Date 1125043266 -7200
# Node ID e2b19c92ef51ce665e4462c1b86125d05af172d6
# Parent  858cab621db2139227534a2d9a731753fe6127e3
Lemmas on dvd, power and finite summation added or strengthened.

diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 26 08:42:52 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 26 10:01:06 2005 +0200
@@ -1144,6 +1144,7 @@
 done
 
 (* FIXME: this is distributitivty, name as such! *)
+(* suggested name: setsum_right_distrib (CB) *)
 
 lemma setsum_mult: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
@@ -1160,6 +1161,34 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
+lemma setsum_left_distrib:
+  "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
+proof (cases "finite A")
+  case True
+  then show ?thesis
+  proof induct
+    case empty thus ?case by simp
+  next
+    case (insert x A) thus ?case by (simp add: left_distrib)
+  qed
+next
+  case False thus ?thesis by (simp add: setsum_def)
+qed
+
+lemma setsum_divide_distrib:
+  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
+proof (cases "finite A")
+  case True
+  then show ?thesis
+  proof induct
+    case empty thus ?case by simp
+  next
+    case (insert x A) thus ?case by (simp add: add_divide_distrib)
+  qed
+next
+  case False thus ?thesis by (simp add: setsum_def)
+qed
+
 lemma setsum_abs[iff]: 
   fixes f :: "'a => ('b::lordered_ab_group_abs)"
   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
@@ -1213,6 +1242,33 @@
 qed
 
 
+text {* Commuting outer and inner summation *}
+
+lemma swap_inj_on:
+  "inj_on (%(i, j). (j, i)) (A \<times> B)"
+  by (unfold inj_on_def) fast
+
+lemma swap_product:
+  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
+  by (simp add: split_def image_def) blast
+
+lemma setsum_commute:
+  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
+proof (simp add: setsum_cartesian_product)
+  have "(\<Sum>z\<in>A \<times> B. f (fst z) (snd z)) =
+    (\<Sum>z\<in>(%(i, j). (j, i)) ` (A \<times> B). f (snd z) (fst z))"
+    (is "?s = _")
+    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
+    apply (simp add: split_def)
+    done
+  also have "... = (\<Sum>z\<in>B \<times> A. f (snd z) (fst z))"
+    (is "_ = ?t")
+    apply (simp add: swap_product)
+    done
+  finally show "?s = ?t" .
+qed
+
+
 subsection {* Generalized product over a set *}
 
 constdefs
diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Aug 26 08:42:52 2005 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Fri Aug 26 10:01:06 2005 +0200
@@ -334,13 +334,7 @@
 
 text{*Sum of a geometric progression.*}
 
-lemma sumr_geometric:
- "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)"
-apply (induct "n", auto)
-apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
-apply (auto simp add: mult_assoc left_distrib)
-apply (simp add: right_distrib diff_minus mult_commute)
-done
+lemmas sumr_geometric = geometric_sum [where 'a = real]
 
 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
 apply (case_tac "x = 1")
diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Fri Aug 26 08:42:52 2005 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Fri Aug 26 10:01:06 2005 +0200
@@ -362,6 +362,13 @@
 
 lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
 
+(* The following lemma should appear in Divides.thy, but there the proof
+   doesn't work. *)
+
+lemma nat_dvd_not_less:
+  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
+  by (unfold dvd_def) auto
+
 ML
 {*
 val divide_minus1 = thm "divide_minus1";
diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Aug 26 08:42:52 2005 +0200
+++ b/src/HOL/Power.thy	Fri Aug 26 10:01:06 2005 +0200
@@ -351,6 +351,13 @@
 apply (erule dvd_imp_le, simp)
 done
 
+lemma power_diff:
+  assumes nz: "a ~= 0"
+  shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
+  by (induct m n rule: diff_induct)
+    (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz)
+
+
 text{*ML bindings for the general exponentiation theorems*}
 ML
 {*
diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Aug 26 08:42:52 2005 +0200
+++ b/src/HOL/SetInterval.thy	Fri Aug 26 10:01:06 2005 +0200
@@ -709,6 +709,18 @@
   "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
 by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
 
+subsection {* The formula for geometric sums *}
+
+lemma geometric_sum:
+  "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
+  (x ^ n - 1) / (x - 1::'a::{field, recpower, division_by_zero})"
+  apply (induct "n", auto)
+  apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
+  apply (auto simp add: mult_assoc left_distrib)
+  apply (simp add: right_distrib diff_minus mult_commute power_Suc)
+  done
+
+
 
 ML
 {*