# HG changeset patch
# User huffman
# Date 1314212217 25200
# Node ID d02b01e5ab8ffc281258fa6870408724ed2665f6
# Parent  266dfd7f4e8263eb8a6210491761d0130ca151ce
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used

diff -r 266dfd7f4e82 -r d02b01e5ab8f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 24 09:23:26 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 24 11:56:57 2011 -0700
@@ -4462,6 +4462,61 @@
   proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
     show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
 
+subsection {* Geometric progression *}
+
+text {* FIXME: Should one or more of these theorems be moved to @{file
+"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+
+lemma sum_gp_basic:
+  fixes x :: "'a::ring_1"
+  shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+proof-
+  def y \<equiv> "1 - x"
+  have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
+    by (induct n, simp, simp add: algebra_simps)
+  thus ?thesis
+    unfolding y_def by simp
+qed
+
+lemma sum_gp_multiplied: assumes mn: "m <= n"
+  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+  (is "?lhs = ?rhs")
+proof-
+  let ?S = "{0..(n - m)}"
+  from mn have mn': "n - m \<ge> 0" by arith
+  let ?f = "op + m"
+  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
+  have f: "?f ` ?S = {m..n}"
+    using mn apply (auto simp add: image_iff Bex_def) by arith
+  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
+    by (rule ext, simp add: power_add power_mult)
+  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
+  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
+  then show ?thesis unfolding sum_gp_basic using mn
+    by (simp add: field_simps power_add[symmetric])
+qed
+
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
+   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
+                    else (x^ m - x^ (Suc n)) / (1 - x))"
+proof-
+  {assume nm: "n < m" hence ?thesis by simp}
+  moreover
+  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
+    {assume x: "x = 1"  hence ?thesis by simp}
+    moreover
+    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
+      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+    ultimately have ?thesis by metis
+  }
+  ultimately show ?thesis by metis
+qed
+
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
+  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+  unfolding sum_gp[of x m "m + n"] power_Suc
+  by (simp add: field_simps power_add)
+
 subsection {* monotone convergence (bounded interval first). *}
 
 lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
diff -r 266dfd7f4e82 -r d02b01e5ab8f src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 09:23:26 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 11:56:57 2011 -0700
@@ -702,65 +702,6 @@
   then show ?thesis by blast
 qed
 
-subsection {* Geometric progression *}
-
-lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
-  (is "?lhs = ?rhs")
-proof-
-  {assume x1: "x = 1" hence ?thesis by simp}
-  moreover
-  {assume x1: "x\<noteq>1"
-    hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
-    from geometric_sum[OF x1, of "Suc n", unfolded x1']
-    have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
-      unfolding atLeastLessThanSuc_atLeastAtMost
-      using x1' apply (auto simp only: field_simps)
-      apply (simp add: field_simps)
-      done
-    then have ?thesis by (simp add: field_simps) }
-  ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_multiplied: assumes mn: "m <= n"
-  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
-  (is "?lhs = ?rhs")
-proof-
-  let ?S = "{0..(n - m)}"
-  from mn have mn': "n - m \<ge> 0" by arith
-  let ?f = "op + m"
-  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
-  have f: "?f ` ?S = {m..n}"
-    using mn apply (auto simp add: image_iff Bex_def) by arith
-  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
-    by (rule ext, simp add: power_add power_mult)
-  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
-  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
-  then show ?thesis unfolding sum_gp_basic using mn
-    by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
-   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
-                    else (x^ m - x^ (Suc n)) / (1 - x))"
-proof-
-  {assume nm: "n < m" hence ?thesis by simp}
-  moreover
-  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
-    {assume x: "x = 1"  hence ?thesis by simp}
-    moreover
-    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
-      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
-    ultimately have ?thesis by metis
-  }
-  ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
-  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
-  unfolding sum_gp[of x m "m + n"] power_Suc
-  by (simp add: field_simps power_add)
-
-
 subsection{* A bit of linear algebra. *}
 
 definition (in real_vector)