# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430404081 -3600
# Node ID 645058aa9d6ff2158cf4478eaa9a6893d822a5d1
# Parent  91477b3a2d6b6656fb54fc6e89c2234259787faa
tidying some messy proofs

diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/GCD.thy
--- 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
+  by (simp add: gcd_nat.commute)
 
 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
+  by (simp add: gcd_int.commute)
 
 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 @@
   apply (auto simp add: gcd_mult_cancel_int)
 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 *}
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Int.thy
--- 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)"
   by transfer (clarsimp simp add: le_imp_diff_is_add)
- 
+
 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)
   thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing
-                             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)
-  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
+  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
   thus ?thesis using  le_imp_0_less [OF le]
-    by (auto simp add: add.assoc) 
+    by (auto simp add: add.assoc)
 next
   case (neg n)
   show ?thesis
   proof
     assume eq: "1 + z + z = 0"
     have "(0::int) < 1 + (int n + int n)"
-      by (simp add: le_imp_0_less add_increasing) 
-    also have "... = - (1 + z + z)" 
-      by (simp add: neg add.assoc [symmetric]) 
-    also have "... = 0" by (simp add: eq) 
+      by (simp add: le_imp_0_less add_increasing)
+    also have "... = - (1 + z + z)"
+      by (simp add: neg add.assoc [symmetric])
+    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))"
     by (auto simp add: int_ge_less_than_def)
-  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))"
     by (auto simp add: int_ge_less_than2_def)
-  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>"
       by (simp add: abs_mult)
     also have "... = 1"
       by (simp add: mn)
@@ -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))"
   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
@@ -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
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Library/Formal_Power_Series.thy
--- 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 @@
     by (auto simp add: expand_fps_eq)
 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)"
   by (induct n) (auto simp add: field_simps E_add_mult)
 
@@ -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 @@
 lemma fps_cos_nth_add_2:
   "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 (simp add: nat_add_1_add_1 fps_sin_nth_add_2
               del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
   apply (subst minus_divide_left)
-  apply (subst eq_divide_iff)
+  apply (subst nonzero_eq_divide_eq)
   apply (simp del: of_nat_add of_nat_Suc)
   apply (simp only: ac_simps)
   done
@@ -3518,7 +3499,7 @@
   apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2
               del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
   apply (subst minus_divide_left)
-  apply (subst eq_divide_iff)
+  apply (subst nonzero_eq_divide_eq)
   apply (simp del: of_nat_add of_nat_Suc)
   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)
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Library/Library.thy
--- 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
+  Quadratic_Discriminant
   Quotient_List
   Quotient_Option
   Quotient_Product
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Library/Quadratic_Discriminant.thy
--- /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
+*)
+
+section "Roots of real quadratics"
+
+theory Quadratic_Discriminant
+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
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- 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 add: power_Suc)
+      by simp
   qed
 qed
 
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- 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))"
   by (simp add: arccos_arctan arcsin_arccos_eq)
 
-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))"
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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]
     apply (simp add: field_simps)
-    using mult_left_mono[OF p Suc.prems]
-    apply simp
     done
   finally show ?case
     by (simp add: real_of_nat_Suc field_simps)
@@ -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"
   by (metis subspace_add subspace_span)
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Real.thy
--- 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 (drule (1) add_le_less_mono, simp)
-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 (simp add: eq_divide_eq)
     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 (auto simp add: real_of_nat_Suc)
-apply (subst mult_2)
-apply (erule add_less_le_mono)
-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"
-by (simp add: power_commutes split add: nat_diff_split)
+by (simp add: power_Suc power_commutes split add: nat_diff_split)
 
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma real_two_squares_add_zero_iff [simp]:
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Set_Interval.thy
--- 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)"
+    by (simp add: power_Suc)
+  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
diff -r 91477b3a2d6b -r 645058aa9d6f src/HOL/Transcendental.thy
--- 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)"
-    by (simp add: 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: 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)"
   by (simp add: setsum_subtractf)
 
+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 (simp add: mult.assoc [symmetric])
   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 (simp add: less_iff_Suc_add)
   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])
   apply (simp add: ac_simps)
@@ -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"
-    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
+    by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute)
+
+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"
-  by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
-
 text {* Strict monotonicity of exponential. *}
 
 lemma exp_ge_add_one_self_aux:
@@ -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
+  by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc)
 
 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)
-apply (simp add: ac_simps)
-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))))"
     by (simp add: fact_num_eq_if realpow_num_eq_if)
   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))"
         by (simp add: inverse_eq_divide less_divide_eq)
-    }
-    note *** = this
-    have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
-    from ** show ?thesis by (rule sumr_pos_lt_pair)
-      (simp add: divide_inverse mult.assoc [symmetric] ***)
+    } 
+    then show ?thesis
+      by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps)
   qed
   ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
     by (rule order_less_trans)