# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1425646083 0
# Node ID fdfdf89a83a6185953f9ebec28fd3a170ee3dddb
# Parent  452458cf8506b408ffaee54b83c1c643c0fa3b47
A few new lemmas and a bit of tidying up

diff -r 452458cf8506 -r fdfdf89a83a6 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Deriv.thy	Fri Mar 06 12:48:03 2015 +0000
@@ -842,10 +842,6 @@
      by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
 qed
 
-text {*
- Let's do the standard proof, though theorem
- @{text "LIM_mult2"} follows from a NS proof
-*}
 
 subsection {* Local extrema *}
 
diff -r 452458cf8506 -r fdfdf89a83a6 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Groups_Big.thy	Fri Mar 06 12:48:03 2015 +0000
@@ -953,8 +953,9 @@
 apply (auto simp add: algebra_simps)
 done
 
-lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
-using setsum.distrib[of f "%_. 1" A] by(simp)
+lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
+  using setsum.distrib[of f "\<lambda>_. 1" A] 
+  by simp
 
 lemma setsum_bounded:
   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
diff -r 452458cf8506 -r fdfdf89a83a6 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Mar 06 12:48:03 2015 +0000
@@ -201,6 +201,12 @@
     shows "DERIV g a :> f'"
   by (blast intro: assms DERIV_transform_within)
 
+(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
+lemma DERIV_zero_UNIV_unique:
+  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
+  shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a" 
+by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
+
 subsection {*Some limit theorems about real part of real series etc.*}
 
 (*MOVE? But not to Finite_Cartesian_Product*)
@@ -553,7 +559,7 @@
 apply (simp add: algebra_simps)
 done
 
-subsection{*analyticity on a set*}
+subsection{*Analyticity on a set*}
 
 definition analytic_on (infixl "(analytic'_on)" 50)  
   where
diff -r 452458cf8506 -r fdfdf89a83a6 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Fri Mar 06 12:48:03 2015 +0000
@@ -17,11 +17,15 @@
   by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
 
 lemma setsum_gp0:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
- shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
-using setsum_gp_basic[of x n]
-apply (simp add: real_of_nat_def)
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_eq_divide_eq)
+  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
+  using setsum_gp_basic[of x n]
+  by (simp add: real_of_nat_def mult.commute divide_simps)
+
+lemma setsum_power_add:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
+  by (simp add: setsum_right_distrib power_add)
 
 lemma setsum_power_shift:
   fixes x :: "'a::{comm_ring,monoid_mult}"
@@ -67,6 +71,11 @@
   using setsum_gp [of x m "m+n"]
   by (auto simp: power_add algebra_simps)
 
+lemma setsum_gp_strict:
+  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
+  by (induct n) (auto simp: algebra_simps divide_simps)
+    
 subsection{*Basics about polynomial functions: extremal behaviour and root counts.*}
 
 lemma sub_polyfun: