A few new lemmas and a bit of tidying up
authorpaulson <lp15@cam.ac.uk>
Fri Mar 06 12:48:03 2015 +0000 (2015-03-06)
changeset 59615fdfdf89a83a6
parent 59614 452458cf8506
child 59620 92d7d8e4f1bf
A few new lemmas and a bit of tidying up
src/HOL/Deriv.thy
src/HOL/Groups_Big.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/PolyRoots.thy
     1.1 --- a/src/HOL/Deriv.thy	Thu Mar 05 17:39:04 2015 +0000
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 06 12:48:03 2015 +0000
     1.3 @@ -842,10 +842,6 @@
     1.4       by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
     1.5  qed
     1.6  
     1.7 -text {*
     1.8 - Let's do the standard proof, though theorem
     1.9 - @{text "LIM_mult2"} follows from a NS proof
    1.10 -*}
    1.11  
    1.12  subsection {* Local extrema *}
    1.13  
     2.1 --- a/src/HOL/Groups_Big.thy	Thu Mar 05 17:39:04 2015 +0000
     2.2 +++ b/src/HOL/Groups_Big.thy	Fri Mar 06 12:48:03 2015 +0000
     2.3 @@ -953,8 +953,9 @@
     2.4  apply (auto simp add: algebra_simps)
     2.5  done
     2.6  
     2.7 -lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
     2.8 -using setsum.distrib[of f "%_. 1" A] by(simp)
     2.9 +lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
    2.10 +  using setsum.distrib[of f "\<lambda>_. 1" A] 
    2.11 +  by simp
    2.12  
    2.13  lemma setsum_bounded:
    2.14    assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Mar 05 17:39:04 2015 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Mar 06 12:48:03 2015 +0000
     3.3 @@ -201,6 +201,12 @@
     3.4      shows "DERIV g a :> f'"
     3.5    by (blast intro: assms DERIV_transform_within)
     3.6  
     3.7 +(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
     3.8 +lemma DERIV_zero_UNIV_unique:
     3.9 +  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    3.10 +  shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a" 
    3.11 +by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
    3.12 +
    3.13  subsection {*Some limit theorems about real part of real series etc.*}
    3.14  
    3.15  (*MOVE? But not to Finite_Cartesian_Product*)
    3.16 @@ -553,7 +559,7 @@
    3.17  apply (simp add: algebra_simps)
    3.18  done
    3.19  
    3.20 -subsection{*analyticity on a set*}
    3.21 +subsection{*Analyticity on a set*}
    3.22  
    3.23  definition analytic_on (infixl "(analytic'_on)" 50)  
    3.24    where
     4.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Thu Mar 05 17:39:04 2015 +0000
     4.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Fri Mar 06 12:48:03 2015 +0000
     4.3 @@ -17,11 +17,15 @@
     4.4    by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
     4.5  
     4.6  lemma setsum_gp0:
     4.7 - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
     4.8 - shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
     4.9 -using setsum_gp_basic[of x n]
    4.10 -apply (simp add: real_of_nat_def)
    4.11 -by (metis eq_iff_diff_eq_0 mult.commute nonzero_eq_divide_eq)
    4.12 +  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
    4.13 +  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
    4.14 +  using setsum_gp_basic[of x n]
    4.15 +  by (simp add: real_of_nat_def mult.commute divide_simps)
    4.16 +
    4.17 +lemma setsum_power_add:
    4.18 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    4.19 +  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
    4.20 +  by (simp add: setsum_right_distrib power_add)
    4.21  
    4.22  lemma setsum_power_shift:
    4.23    fixes x :: "'a::{comm_ring,monoid_mult}"
    4.24 @@ -67,6 +71,11 @@
    4.25    using setsum_gp [of x m "m+n"]
    4.26    by (auto simp: power_add algebra_simps)
    4.27  
    4.28 +lemma setsum_gp_strict:
    4.29 +  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
    4.30 +  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
    4.31 +  by (induct n) (auto simp: algebra_simps divide_simps)
    4.32 +    
    4.33  subsection{*Basics about polynomial functions: extremal behaviour and root counts.*}
    4.34  
    4.35  lemma sub_polyfun: