author paulson Fri, 18 Sep 2020 08:02:19 +0100 changeset 72268 71a8935eb5da parent 72267 121b838a0ba8 child 72269 88880eecd7fe child 72270 2af901e467da
removal of needless premises
 src/HOL/Set_Interval.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Set_Interval.thy	Thu Sep 17 18:48:37 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Sep 18 08:02:19 2020 +0100
@@ -2171,7 +2171,7 @@
subsubsection \<open>The formula for geometric sums\<close>

lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
-by (induction k) (auto simp: mult_2)
+  by (induction k) (auto simp: mult_2)

lemma geometric_sum:
assumes "x \<noteq> 1"
@@ -2205,31 +2205,31 @@

corollary power_diff_sumr2: \<comment> \<open>\<open>COMPLEX_POLYFUN\<close> in HOL Light\<close>
fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
+  shows "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
using diff_power_eq_sum[of x "n - 1" y]
by (cases "n = 0") (simp_all add: field_simps)

lemma power_diff_1_eq:
fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
+  shows "x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
using diff_power_eq_sum [of x _ 1]
by (cases n) auto

lemma one_diff_power_eq':
fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
+  shows "1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
using diff_power_eq_sum [of 1 _ x]
by (cases n) auto

lemma one_diff_power_eq:
fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
-by (metis one_diff_power_eq' [of n x] sum.nat_diff_reindex)
+  shows "1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
+by (metis one_diff_power_eq' sum.nat_diff_reindex)

lemma sum_gp_basic:
fixes x :: "'a::{comm_ring,monoid_mult}"
shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
-  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
+  by (simp only: one_diff_power_eq lessThan_Suc_atMost)

lemma sum_power_shift:
fixes x :: "'a::{comm_ring,monoid_mult}"```