author paulson Thu, 30 Apr 2015 15:28:01 +0100 changeset 60162 645058aa9d6f parent 60155 91477b3a2d6b child 60163 1d218c3e84e2
tidying some messy proofs
 src/HOL/GCD.thy file | annotate | diff | comparison | revisions src/HOL/Int.thy file | annotate | diff | comparison | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/Library/Library.thy file | annotate | diff | comparison | revisions src/HOL/Library/Quadratic_Discriminant.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Linear_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Real.thy file | annotate | diff | comparison | revisions src/HOL/Set_Interval.thy file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/GCD.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/GCD.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -755,24 +755,16 @@
done

lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
-  by (induct n, simp_all add: coprime_mult_nat)
+  by (induct n, simp_all add: power_Suc coprime_mult_nat)

lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
-  by (induct n, simp_all add: coprime_mult_int)
+  by (induct n, simp_all add: power_Suc coprime_mult_int)

lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
-  apply (rule coprime_exp_nat)
-  apply (subst gcd_commute_nat)
-  apply (rule coprime_exp_nat)
-  apply (subst gcd_commute_nat, assumption)
-done
+  by (simp add: coprime_exp_nat gcd_nat.commute)

lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
-  apply (rule coprime_exp_int)
-  apply (subst gcd_commute_int)
-  apply (rule coprime_exp_int)
-  apply (subst gcd_commute_int, assumption)
-done
+  by (simp add: coprime_exp_int gcd_int.commute)

lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
proof (cases)
@@ -783,24 +775,11 @@
by (auto simp:div_gcd_coprime_nat)
hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
-    apply (subst (1 2) mult.commute)
-    apply (subst gcd_mult_distrib_nat [symmetric])
-    apply simp
-    done
+    by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
-    apply (subst div_power)
-    apply auto
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply auto
-    done
+    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
-    apply (subst div_power)
-    apply auto
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply auto
-    done
+    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
finally show ?thesis .
qed

@@ -908,7 +887,7 @@
have "a' dvd a'^n" by (simp add: m)
with th0 have "a' dvd b'^n"
using dvd_trans[of a' "a'^n" "b'^n"] by simp
-    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
+    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute power_Suc)
from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
have "a' dvd b'" by (subst (asm) mult.commute, blast)
hence "a'*?g dvd b'*?g" by simp
@@ -947,21 +926,13 @@
qed

lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
-  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
-  apply force
-  apply (rule dvd_diff_nat)
-  apply auto
-done

lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
using coprime_plus_one_nat by (simp add: One_nat_def)

lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
-  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
-  apply force
-  apply (rule dvd_diff)
-  apply auto
-done

lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
using coprime_plus_one_nat [of "n - 1"]
@@ -985,36 +956,23 @@
done

-lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
-    x dvd b \<Longrightarrow> x = 1"
-  apply (subgoal_tac "x dvd gcd a b")
-  apply simp
-  apply (erule (1) gcd_greatest)
-done
+lemma coprime_common_divisor_nat:
+    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+  by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)

-lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
-    x dvd b \<Longrightarrow> abs x = 1"
-  apply (subgoal_tac "x dvd gcd a b")
-  apply simp
-  apply (erule (1) gcd_greatest)
-done
+lemma coprime_common_divisor_int:
+    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
+  using gcd_greatest by fastforce

-lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
-    coprime d e"
-  apply (auto simp add: dvd_def)
-  apply (frule coprime_lmult_int)
-  apply (subst gcd_commute_int)
-  apply (subst (asm) (2) gcd_commute_int)
-  apply (erule coprime_lmult_int)
-done
+lemma coprime_divisors_nat:
+    "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
+  by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)

lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
-apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
-done
+by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)

lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
-apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
-done
+by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)

subsection {* Bezout's theorem *}```
```--- a/src/HOL/Int.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Int.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -3,7 +3,7 @@
Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
*)

-section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
+section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}

theory Int
imports Equiv_Relations Power Quotient Fun_Def
@@ -338,10 +338,10 @@

text{*An alternative condition is @{term "0 \<le> w"} *}
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])

corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])

lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
by transfer (clarsimp, arith)
@@ -355,7 +355,7 @@
lemma nat_eq_iff:
"nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
-
+
corollary nat_eq_iff2:
"m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
using nat_eq_iff [of w m] by auto
@@ -378,7 +378,7 @@

lemma nat_2: "nat 2 = Suc (Suc 0)"
by simp
-
+
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
by transfer (clarsimp, arith)

@@ -404,7 +404,7 @@
lemma nat_diff_distrib':
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
by transfer clarsimp
-
+
lemma nat_diff_distrib:
"0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
by (rule nat_diff_distrib') auto
@@ -415,7 +415,7 @@
lemma le_nat_iff:
"k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
by transfer auto
-
+
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
by transfer (clarsimp simp add: less_diff_conv)

@@ -427,7 +427,7 @@

end

-lemma diff_nat_numeral [simp]:
+lemma diff_nat_numeral [simp]:
"(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)

@@ -550,7 +550,7 @@

text {* Preliminaries *}

-lemma le_imp_0_less:
+lemma le_imp_0_less:
assumes le: "0 \<le> z"
shows "(0::int) < 1 + z"
proof -
@@ -565,7 +565,7 @@
proof (cases z)
case (nonneg n)
-                             le_imp_0_less [THEN order_less_imp_le])
+                             le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
@@ -580,19 +580,19 @@
"1 + z + z \<noteq> (0::int)"
proof (cases z)
case (nonneg n)
thus ?thesis using  le_imp_0_less [OF le]
next
case (neg n)
show ?thesis
proof
assume eq: "1 + z + z = 0"
have "(0::int) < 1 + (int n + int n)"
-    also have "... = - (1 + z + z)"
-    also have "... = 0" by (simp add: eq)
+    also have "... = - (1 + z + z)"
+    also have "... = 0" by (simp add: eq)
finally have "0<0" ..
thus False by blast
qed
@@ -699,12 +699,12 @@
hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
with odd_nonzero show False by blast
qed
-qed
+qed

lemma Nats_numeral [simp]: "numeral w \<in> Nats"
using of_nat_in_Nats [of "numeral w"] by simp

-lemma Ints_odd_less_0:
+lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
proof -
@@ -787,9 +787,7 @@
text{*Simplify the term @{term "w + - z"}*}

lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
-apply (insert zless_nat_conj [of 1 z])
-apply auto
-done
+  using zless_nat_conj [of 1 z] by auto

text{*This simplifies expressions of the form @{term "int n = z"} where
z is an integer literal.*}
@@ -857,7 +855,7 @@

lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
apply (cases "z=0 | w=0")
-apply (auto simp add: abs_if nat_mult_distrib [symmetric]
+apply (auto simp add: abs_if nat_mult_distrib [symmetric]
nat_mult_distrib_neg [symmetric] mult_less_0_iff)
done

@@ -867,9 +865,9 @@
done

lemma diff_nat_eq_if:
-     "nat z - nat z' =
-        (if z' < 0 then nat z
-         else let d = z-z' in
+     "nat z - nat z' =
+        (if z' < 0 then nat z
+         else let d = z-z' in
if d < 0 then 0 else nat d)"
by (simp add: Let_def nat_diff_distrib [symmetric])

@@ -891,8 +889,8 @@
proof -
have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
-  thus ?thesis
-    by (rule wf_subset [OF wf_measure])
+  thus ?thesis
+    by (rule wf_subset [OF wf_measure])
qed

text{*This variant looks odd, but is typical of the relations suggested
@@ -905,10 +903,10 @@

theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
proof -
-  have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
+  have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
-  thus ?thesis
-    by (rule wf_subset [OF wf_measure])
+  thus ?thesis
+    by (rule wf_subset [OF wf_measure])
qed

(* `set:int': dummy construction *)
@@ -1009,7 +1007,7 @@
subsection{*Intermediate value theorems*}

lemma int_val_lemma:
-     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
+     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
unfolding One_nat_def
apply (induct n)
@@ -1027,9 +1025,9 @@
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]

lemma nat_intermed_int_val:
-     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
+     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
-apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
+apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
in int_val_lemma)
unfolding One_nat_def
apply simp
@@ -1053,8 +1051,8 @@
proof
assume "2 \<le> \<bar>m\<bar>"
hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
-      by (simp add: mult_mono 0)
-    also have "... = \<bar>m*n\<bar>"
+      by (simp add: mult_mono 0)
+    also have "... = \<bar>m*n\<bar>"
also have "... = 1"
@@ -1077,10 +1075,10 @@
qed

lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
-apply (rule iffI)
+apply (rule iffI)
apply (frule pos_zmult_eq_1_iff_lemma)
- apply (simp add: mult.commute [of m])
- apply (frule pos_zmult_eq_1_iff_lemma, auto)
+ apply (simp add: mult.commute [of m])
+ apply (frule pos_zmult_eq_1_iff_lemma, auto)
done

lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
@@ -1226,14 +1224,14 @@
apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
done

-lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
+lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
proof cases
assume "a = 0" with assms show ?thesis by simp
next
assume "a \<noteq> 0"
-  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
-  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
+  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
+  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
from k k' have "a = a*k*k'" by simp
with mult_cancel_left1[where c="a" and b="k*k'"]
have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
@@ -1242,7 +1240,7 @@
qed

lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
-  using dvd_add_right_iff [of k "- n" m] by simp
+  using dvd_add_right_iff [of k "- n" m] by simp

lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
@@ -1317,10 +1315,10 @@
then show "x dvd 1" by (auto intro: dvdI)
qed

-lemma zdvd_mult_cancel1:
+lemma zdvd_mult_cancel1:
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
proof
-  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
+  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
by (cases "n >0") (auto simp add: minus_equation_iff)
next
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp```
```--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -742,32 +742,28 @@
qed

-lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
-    = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
-  apply (rule fps_inverse_unique)
-  apply simp
-  apply (simp add: fps_eq_iff fps_mult_nth)
-  apply clarsimp
+lemma setsum_zero_lemma:
+  fixes n::nat
+  assumes "0 < n"
+  shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
proof -
-  fix n :: nat
-  assume n: "n > 0"
-  let ?f = "\<lambda>i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0"
-  let ?g = "\<lambda>i. if i = n then 1 else if i=n - 1 then - 1 else 0"
+  let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
+  let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
have th1: "setsum ?f {0..n} = setsum ?g {0..n}"
by (rule setsum.cong) auto
have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}"
-    apply (insert n)
apply (rule setsum.cong)
+    using assms
apply auto
done
have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
by auto
-  from n have d: "{0.. n - 1} \<inter> {n} = {}"
+  from assms have d: "{0.. n - 1} \<inter> {n} = {}"
by auto
have f: "finite {0.. n - 1}" "finite {n}"
by auto
-  show "setsum ?f {0..n} = 0"
+  show ?thesis
unfolding th1
apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
unfolding th2
@@ -775,6 +771,12 @@
done
qed

+lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
+    = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
+  apply (rule fps_inverse_unique)
+  apply (simp_all add: fps_eq_iff fps_mult_nth setsum_zero_lemma)
+  done
+

subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *}

@@ -2885,8 +2887,7 @@
unfolding th
using fact_gt_zero
apply (simp add: field_simps del: of_nat_Suc fact_Suc)
-      apply (drule sym)
-      apply (simp add: field_simps of_nat_mult)
+      apply simp
done
}
note th' = this
@@ -2894,11 +2895,7 @@
next
assume h: ?rhs
show ?lhs
-    apply (subst h)
-    apply simp
-    apply (simp only: h[symmetric])
-    apply simp
-    done
+    by (metis E_deriv fps_deriv_mult_const_left h mult.left_commute)
qed

lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
@@ -2949,16 +2946,6 @@
apply auto
done

-lemma inverse_one_plus_X:
-  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::field)^n)"
-  (is "inverse ?l = ?r")
-proof -
-  have th: "?l * ?r = 1"
-    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
-  have th': "?l \$ 0 \<noteq> 0" by (simp add: )
-  from fps_inverse_unique[OF th' th] show ?thesis .
-qed
-
lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"

@@ -2993,7 +2980,7 @@
where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"

lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
-  unfolding inverse_one_plus_X
+  unfolding fps_inverse_X_plus1
by (simp add: L_def fps_eq_iff del: of_nat_Suc)

lemma L_nth: "L c \$ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
@@ -3438,12 +3425,6 @@
finally show ?thesis .
qed

-lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
-  by auto
-
-lemma eq_divide_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x = y / a \<longleftrightarrow> x * a = y"
-  by auto
-
lemma fps_sin_nth_0 [simp]: "fps_sin c \$ 0 = 0"
unfolding fps_sin_def by simp

@@ -3454,7 +3435,7 @@
"fps_sin c \$ (n + 2) = - (c * c * fps_sin c \$ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_sin_def
apply (cases n, simp)
-  apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done

@@ -3467,7 +3448,7 @@
"fps_cos c \$ (n + 2) = - (c * c * fps_cos c \$ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_cos_def
-  apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done

@@ -3500,7 +3481,7 @@
apply (subst minus_divide_left)
-  apply (subst eq_divide_iff)
+  apply (subst nonzero_eq_divide_eq)
apply (simp only: ac_simps)
done
@@ -3518,7 +3499,7 @@
apply (subst minus_divide_left)
-  apply (subst eq_divide_iff)
+  apply (subst nonzero_eq_divide_eq)
apply (simp only: ac_simps)
done
@@ -3793,7 +3774,8 @@
THEN spec, of "\<lambda>x. x < e"]
have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
unfolding eventually_nhds
-        apply safe
+        apply clarsimp
+        apply (rule FalseE)
apply auto --{*slow*}
done
then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)```
```--- a/src/HOL/Library/Library.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Library/Library.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -54,6 +54,7 @@
Polynomial
Preorder
Product_Vector
Quotient_List
Quotient_Option
Quotient_Product```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quadratic_Discriminant.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -0,0 +1,182 @@
+(*  Title:       Roots of real quadratics
+    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
+
+Originally from the AFP entry Tarskis_Geometry
+*)
+
+
+imports Complex_Main
+begin
+
+definition discrim :: "[real,real,real] \<Rightarrow> real" where
+  "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
+
+lemma complete_square:
+  fixes a b c x :: "real"
+  assumes "a \<noteq> 0"
+  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
+proof -
+  have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
+    by (simp add: algebra_simps power2_eq_square)
+  with `a \<noteq> 0`
+  have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0"
+    by simp
+  thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
+    unfolding discrim_def
+    by (simp add: power2_eq_square algebra_simps)
+qed
+
+lemma discriminant_negative:
+  fixes a b c x :: real
+  assumes "a \<noteq> 0"
+  and "discrim a b c < 0"
+  shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
+proof -
+  have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
+  with `discrim a b c < 0` have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
+  with complete_square and `a \<noteq> 0` show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
+qed
+
+lemma plus_or_minus_sqrt:
+  fixes x y :: real
+  assumes "y \<ge> 0"
+  shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
+proof
+  assume "x\<^sup>2 = y"
+  hence "sqrt (x\<^sup>2) = sqrt y" by simp
+  hence "sqrt y = \<bar>x\<bar>" by simp
+  thus "x = sqrt y \<or> x = - sqrt y" by auto
+next
+  assume "x = sqrt y \<or> x = - sqrt y"
+  hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
+  with `y \<ge> 0` show "x\<^sup>2 = y" by simp
+qed
+
+lemma divide_non_zero:
+  fixes x y z :: real
+  assumes "x \<noteq> 0"
+  shows "x * y = z \<longleftrightarrow> y = z / x"
+proof
+  assume "x * y = z"
+  with `x \<noteq> 0` show "y = z / x" by (simp add: field_simps)
+next
+  assume "y = z / x"
+  with `x \<noteq> 0` show "x * y = z" by simp
+qed
+
+lemma discriminant_nonneg:
+  fixes a b c x :: real
+  assumes "a \<noteq> 0"
+  and "discrim a b c \<ge> 0"
+  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+  x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+  x = (-b - sqrt (discrim a b c)) / (2 * a)"
+proof -
+  from complete_square and plus_or_minus_sqrt and assms
+  have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+    (2 * a) * x + b = sqrt (discrim a b c) \<or>
+    (2 * a) * x + b = - sqrt (discrim a b c)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
+    (2 * a) * x = (-b - sqrt (discrim a b c))"
+    by auto
+  also from `a \<noteq> 0` and divide_non_zero [of "2 * a" x]
+  have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a)"
+    by simp
+  finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+    x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a)" .
+qed
+
+lemma discriminant_zero:
+  fixes a b c x :: real
+  assumes "a \<noteq> 0"
+  and "discrim a b c = 0"
+  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
+  using discriminant_nonneg and assms
+  by simp
+
+theorem discriminant_iff:
+  fixes a b c x :: real
+  assumes "a \<noteq> 0"
+  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+  discrim a b c \<ge> 0 \<and>
+  (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+  x = (-b - sqrt (discrim a b c)) / (2 * a))"
+proof
+  assume "a * x\<^sup>2 + b * x + c = 0"
+  with discriminant_negative and `a \<noteq> 0` have "\<not>(discrim a b c < 0)" by auto
+  hence "discrim a b c \<ge> 0" by simp
+  with discriminant_nonneg and `a * x\<^sup>2 + b * x + c = 0` and `a \<noteq> 0`
+  have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a)"
+    by simp
+  with `discrim a b c \<ge> 0`
+  show "discrim a b c \<ge> 0 \<and>
+    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
+next
+  assume "discrim a b c \<ge> 0 \<and>
+    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a))"
+  hence "discrim a b c \<ge> 0" and
+    "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+    x = (-b - sqrt (discrim a b c)) / (2 * a)"
+    by simp_all
+  with discriminant_nonneg and `a \<noteq> 0` show "a * x\<^sup>2 + b * x + c = 0" by simp
+qed
+
+lemma discriminant_nonneg_ex:
+  fixes a b c :: real
+  assumes "a \<noteq> 0"
+  and "discrim a b c \<ge> 0"
+  shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
+  using discriminant_nonneg and assms
+  by auto
+
+lemma discriminant_pos_ex:
+  fixes a b c :: real
+  assumes "a \<noteq> 0"
+  and "discrim a b c > 0"
+  shows "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
+proof -
+  let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
+  let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
+  from `discrim a b c > 0` have "sqrt (discrim a b c) \<noteq> 0" by simp
+  hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
+  with `a \<noteq> 0` have "?x \<noteq> ?y" by simp
+  moreover
+  from discriminant_nonneg [of a b c ?x]
+    and discriminant_nonneg [of a b c ?y]
+    and assms
+  have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
+  ultimately
+  show "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0" by blast
+qed
+
+lemma discriminant_pos_distinct:
+  fixes a b c x :: real
+  assumes "a \<noteq> 0" and "discrim a b c > 0"
+  shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
+proof -
+  from discriminant_pos_ex and `a \<noteq> 0` and `discrim a b c > 0`
+  obtain w and z where "w \<noteq> z"
+    and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
+    by blast
+  show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
+  proof cases
+    assume "x = w"
+    with `w \<noteq> z` have "x \<noteq> z" by simp
+    with `a * z\<^sup>2 + b * z + c = 0`
+    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+  next
+    assume "x \<noteq> w"
+    with `a * w\<^sup>2 + b * w + c = 0`
+    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+  qed
+qed
+
+end```
```--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -1200,7 +1200,7 @@
also have "... \<le> (e * norm z) * norm z ^ Suc n"
by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
+      by simp
qed
qed
```
```--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -458,9 +458,6 @@

subsection{* Taylor series for complex exponential, sine and cosine.*}

-context
-begin
-
declare power_Suc [simp del]

lemma Taylor_exp:
@@ -522,8 +519,9 @@
have *: "cmod (sin z -
(\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
-  proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
-simplified])
+  proof (rule complex_taylor [of "closed_segment 0 z" n
+                                 "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
+                                 "exp\<bar>Im z\<bar>" 0 z,  simplified])
show "convex (closed_segment 0 z)"
by (rule convex_segment [of 0 z])
next
@@ -600,7 +598,7 @@
done
qed

-end (* of context *)
+declare power_Suc [simp]

text{*32-bit Approximation to e*}
lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
@@ -2626,13 +2624,13 @@
lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"

-lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)

lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
apply (subst Arcsin_Arccos_csqrt_pos)
-  apply (auto simp: power_le_one zz)
+  apply (auto simp: power_le_one csqrt_1_diff_eq)
done

lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
@@ -2642,7 +2640,7 @@
lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
apply (subst Arccos_Arcsin_csqrt_pos)
-  apply (auto simp: power_le_one zz)
+  apply (auto simp: power_le_one csqrt_1_diff_eq)
done

lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"```
```--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -575,9 +575,8 @@
by simp
also have "\<dots> \<le> (1 + x) ^ Suc n"
apply (subst diff_le_0_iff_le[symmetric])
+    using mult_left_mono[OF p Suc.prems]
-    using mult_left_mono[OF p Suc.prems]
-    apply simp
done
finally show ?case
@@ -887,10 +886,8 @@
assumes "0 \<in> A"
shows "dependent A"
unfolding dependent_def
-  apply (rule_tac x=0 in bexI)
using assms span_0
-  apply auto
-  done
+  by auto

lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
```--- a/src/HOL/Real.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Real.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -757,10 +757,7 @@
"of_nat n < (2::'a::linordered_idom) ^ n"
apply (induct n)
apply simp
-apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
-apply simp
-done
+by (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)

lemma complete_real:
fixes S :: "real set"
@@ -807,7 +804,7 @@
have width: "\<And>n. B n - A n = (b - a) / 2^n"
apply (induct_tac n, simp)
-    apply (simp add: C_def avg_def algebra_simps)
+    apply (simp add: C_def avg_def power_Suc algebra_simps)
done

have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
@@ -1518,12 +1515,7 @@
by simp

lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
-apply (induct "n")
-apply (subst mult_2)
-apply (rule two_realpow_ge_one)
-done
+  by (simp add: of_nat_less_two_power real_of_nat_def)

text {* TODO: no longer real-specific; rename and move elsewhere *}
lemma realpow_Suc_le_self:
@@ -1535,7 +1527,7 @@
lemma realpow_minus_mult:
fixes x :: "'a::monoid_mult"
shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"

text {* FIXME: declare this [simp] for all types, or not at all *}
```--- a/src/HOL/Set_Interval.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -1519,6 +1519,9 @@
using setsum_triangle_reindex [of f "Suc n"]
by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)

+lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
+
subsection{* Shifting bounds *}

lemma setsum_shift_bounds_nat_ivl:
@@ -1598,10 +1601,53 @@
proof -
from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
-    by (induct n) (simp_all add: field_simps `y \<noteq> 0`)
+    by (induct n) (simp_all add: power_Suc field_simps `y \<noteq> 0`)
ultimately show ?thesis by simp
qed

+lemma diff_power_eq_setsum:
+  fixes y :: "'a::{comm_ring,monoid_mult}"
+  shows
+    "x ^ (Suc n) - y ^ (Suc n) =
+      (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
+proof (induct n)
+  case (Suc n)
+  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
+  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
+    by (simp add: power_Suc algebra_simps)
+  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
+    by (simp only: Suc)
+  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
+    by (simp only: mult.left_commute)
+  also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
+    by (simp add: power_Suc field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
+  finally show ?case .
+qed simp
+
+corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
+using diff_power_eq_setsum[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))"
+using diff_power_eq_setsum [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))"
+using diff_power_eq_setsum [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] nat_diff_setsum_reindex)
+

subsection {* The formula for arithmetic sums *}

@@ -1665,9 +1711,6 @@
lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
by (subst setsum_subtractf_nat) auto

-lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
-  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
-
subsection {* Products indexed over intervals *}

syntax```
```--- a/src/HOL/Transcendental.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Transcendental.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -53,63 +53,6 @@

subsection {* Properties of Power Series *}

-lemma lemma_realpow_diff:
-  fixes y :: "'a::monoid_mult"
-  shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
-proof -
-  assume "p \<le> n"
-  hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
-  thus ?thesis by (simp add: power_commutes)
-qed
-
-lemma lemma_realpow_diff_sumr2:
-  fixes y :: "'a::{comm_ring,monoid_mult}"
-  shows
-    "x ^ (Suc n) - y ^ (Suc n) =
-      (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
-proof (induct n)
-  case (Suc n)
-  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
-    by simp
-  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
-  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
-    by (simp only: Suc)
-  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
-    by (simp only: mult.left_commute)
-  also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
-    by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
-  finally show ?case .
-qed simp
-
-corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
-using lemma_realpow_diff_sumr2[of x "n - 1" y]
-by (cases "n = 0") (simp_all add: field_simps)
-
-lemma lemma_realpow_rev_sumr:
-   "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
-    (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
-  by (subst nat_diff_setsum_reindex[symmetric]) simp
-
-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))"
-using lemma_realpow_diff_sumr2 [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))"
-using lemma_realpow_diff_sumr2 [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] nat_diff_setsum_reindex)
-
lemma powser_zero:
fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1"
shows "(\<Sum>n. f n * 0 ^ n) = f 0"
@@ -533,6 +476,11 @@
"setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"

+lemma lemma_realpow_rev_sumr:
+   "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
+    (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
+  by (subst nat_diff_setsum_reindex[symmetric]) simp
+
lemma lemma_termdiff2:
fixes h :: "'a :: {field}"
assumes h: "h \<noteq> 0"
@@ -544,7 +492,7 @@
apply (simp add: right_diff_distrib diff_divide_distrib h)
apply (cases "n", simp)
-  apply (simp add: lemma_realpow_diff_sumr2 h
+  apply (simp add: diff_power_eq_setsum h
right_diff_distrib [symmetric] mult.assoc
del: power_Suc setsum_lessThan_Suc of_nat_Suc)
apply (subst lemma_realpow_rev_sumr)
@@ -554,7 +502,7 @@
apply (rule setsum.cong [OF refl])
apply (clarify)
-  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
+  apply (simp add: setsum_right_distrib diff_power_eq_setsum ac_simps
del: setsum_lessThan_Suc power_Suc)
apply (subst mult.assoc [symmetric], subst power_add [symmetric])
@@ -1043,7 +991,7 @@
proof -
have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
(\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
-            unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
+            unfolding right_diff_distrib[symmetric] diff_power_eq_setsum abs_mult
by auto
also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
proof (rule mult_left_mono)
@@ -1345,7 +1293,10 @@
lemma exp_of_nat_mult:
fixes x :: "'a::{real_normed_field,banach}"
shows "exp(of_nat n * x) = exp(x) ^ n"
+
+corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
+  by (simp add: exp_of_nat_mult real_of_nat_def)

lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
@@ -1374,10 +1325,6 @@
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
by simp

-(*FIXME: superseded by exp_of_nat_mult*)
-lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
-
text {* Strict monotonicity of exponential. *}

@@ -2361,10 +2308,7 @@
lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
apply (induct n)
apply simp
-  apply (subgoal_tac "real(Suc n) = real n + 1")
-  apply (erule ssubst)
-  apply (subst powr_add, simp, simp)
-  done

lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
@@ -3159,7 +3103,7 @@

lemmas realpow_num_eq_if = power_eq_if

-lemma sumr_pos_lt_pair:  (*FIXME A MESS, BUT THE REAL MESS IS THE NEXT THEOREM*)
+lemma sumr_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>summable f;
\<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
@@ -3169,11 +3113,7 @@
apply (drule_tac k=k in summable_ignore_initial_segment)
apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
apply simp
-apply (frule sums_unique)
-apply (drule sums_summable, simp)
-apply (erule suminf_pos)
-done
+by (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique)

lemma cos_two_less_zero [simp]:
"cos 2 < (0::real)"
@@ -3182,30 +3122,25 @@
from sums_minus [OF cos_paired]
have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
by simp
-  then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
+  then have sm: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule sums_summable)
have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n  * 2 ^ (2 * n) / (fact (2 * n))))
-    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
+                 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
proof -
{ fix d
-      have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
-            < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
-              fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+      let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))"
+      have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))"
unfolding real_of_nat_mult
by (rule mult_strict_mono) (simp_all add: fact_less_mono)
-      then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
-        <  (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
-        by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact)
-      then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
-        < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
+      then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))"
+        by (simp only: fact.simps(2) [of "Suc (?six4d)"] real_of_nat_def of_nat_mult of_nat_fact)
+      then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))"