revisions to limits and derivatives, plus new lemmas
authorpaulson
Thu Jan 07 17:40:55 2016 +0000 (2016-01-07)
changeset 6208744841d07ef1d
parent 62084 969119292e25
child 62088 8463e386eaec
revisions to limits and derivatives, plus new lemmas
src/HOL/Library/Countable.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Sinc_Integral.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Relation.thy
src/HOL/Series.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Jan 06 16:17:50 2016 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Jan 07 17:40:55 2016 +0000
     1.3 @@ -7,7 +7,7 @@
     1.4  section \<open>Encoding (almost) everything into natural numbers\<close>
     1.5  
     1.6  theory Countable
     1.7 -imports Old_Datatype Rat Nat_Bijection
     1.8 +imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
     1.9  begin
    1.10  
    1.11  subsection \<open>The class of countable types\<close>
     2.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Wed Jan 06 16:17:50 2016 +0100
     2.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Jan 07 17:40:55 2016 +0000
     2.3 @@ -72,7 +72,7 @@
     2.4  
     2.5  interpretation lifting_syntax .
     2.6  
     2.7 -lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp 
     2.8 +lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
     2.9  
    2.10  lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
    2.11    is subset_eq parametric subset_transfer .
    2.12 @@ -81,7 +81,7 @@
    2.13  where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
    2.14  
    2.15  lemma less_cset_transfer[transfer_rule]:
    2.16 -  assumes [transfer_rule]: "bi_unique A" 
    2.17 +  assumes [transfer_rule]: "bi_unique A"
    2.18    shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
    2.19  unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    2.20  
    2.21 @@ -201,7 +201,7 @@
    2.22  lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
    2.23  lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
    2.24  lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred]
    2.25 -lemmas cDiff_single_cinsert = diff_single_insert[Transfer.transferred]
    2.26 +lemmas cDiff_single_cinsert = Diff_single_insert[Transfer.transferred]
    2.27  lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
    2.28  lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred]
    2.29  lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred]
    2.30 @@ -389,14 +389,14 @@
    2.31  subsubsection \<open>\<open>cimage\<close>\<close>
    2.32  
    2.33  lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)"
    2.34 -by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) 
    2.35 +by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE)
    2.36  
    2.37  subsubsection \<open>bounded quantification\<close>
    2.38  
    2.39  lemma cBex_simps [simp, no_atp]:
    2.40 -  "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)" 
    2.41 +  "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
    2.42    "\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)"
    2.43 -  "\<And>P. cBex cempty P = False" 
    2.44 +  "\<And>P. cBex cempty P = False"
    2.45    "\<And>a B P. cBex (cinsert a B) P = (P a \<or> cBex B P)"
    2.46    "\<And>A P f. cBex (cimage f A) P = cBex A (\<lambda>x. P (f x))"
    2.47    "\<And>A P. (\<not> cBex A P) = cBall A (\<lambda>x. \<not> P x)"
    2.48 @@ -498,7 +498,7 @@
    2.49  
    2.50  lemma cInt_parametric [transfer_rule]:
    2.51    "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt"
    2.52 -unfolding rel_fun_def 
    2.53 +unfolding rel_fun_def
    2.54  using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
    2.55  by blast
    2.56  
     3.1 --- a/src/HOL/Library/FSet.thy	Wed Jan 06 16:17:50 2016 +0100
     3.2 +++ b/src/HOL/Library/FSet.thy	Thu Jan 07 17:40:55 2016 +0000
     3.3 @@ -286,7 +286,7 @@
     3.4  lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
     3.5  lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
     3.6  lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred]
     3.7 -lemmas fminus_single_finsert = diff_single_insert[Transfer.transferred]
     3.8 +lemmas fminus_single_finsert = Diff_single_insert[Transfer.transferred]
     3.9  lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
    3.10  lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred]
    3.11  lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred]
     4.1 --- a/src/HOL/Limits.thy	Wed Jan 06 16:17:50 2016 +0100
     4.2 +++ b/src/HOL/Limits.thy	Thu Jan 07 17:40:55 2016 +0000
     4.3 @@ -137,7 +137,7 @@
     4.4      by (auto elim!: allE[of _ n])
     4.5  qed
     4.6  
     4.7 -lemma Bseq_bdd_above': 
     4.8 +lemma Bseq_bdd_above':
     4.9    "Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
    4.10  proof (elim BseqE, intro bdd_aboveI2)
    4.11    fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
    4.12 @@ -152,7 +152,7 @@
    4.13  
    4.14  lemma Bseq_eventually_mono:
    4.15    assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
    4.16 -  shows   "Bseq f" 
    4.17 +  shows   "Bseq f"
    4.18  proof -
    4.19    from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
    4.20      by (auto simp: eventually_at_top_linorder)
    4.21 @@ -162,7 +162,7 @@
    4.22      apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
    4.23      apply (rule max.coboundedI1, force intro: order.trans[OF N K])
    4.24      done
    4.25 -  thus ?thesis by (blast intro: BseqI') 
    4.26 +  thus ?thesis by (blast intro: BseqI')
    4.27  qed
    4.28  
    4.29  lemma lemma_NBseq_def:
    4.30 @@ -243,7 +243,7 @@
    4.31  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    4.32    by (simp add: Bseq_def)
    4.33  
    4.34 -lemma Bseq_add: 
    4.35 +lemma Bseq_add:
    4.36    assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    4.37    shows   "Bseq (\<lambda>x. f x + c)"
    4.38  proof -
    4.39 @@ -260,12 +260,12 @@
    4.40  lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    4.41    using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
    4.42  
    4.43 -lemma Bseq_mult: 
    4.44 +lemma Bseq_mult:
    4.45    assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
    4.46    assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
    4.47    shows   "Bseq (\<lambda>x. f x * g x)"
    4.48  proof -
    4.49 -  from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0" 
    4.50 +  from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
    4.51      unfolding Bseq_def by blast
    4.52    hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
    4.53    thus ?thesis by (rule BseqI')
    4.54 @@ -794,7 +794,7 @@
    4.55  
    4.56  lemma tendsto_add_const_iff:
    4.57    "((\<lambda>x. c + f x :: 'a :: real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
    4.58 -  using tendsto_add[OF tendsto_const[of c], of f d] 
    4.59 +  using tendsto_add[OF tendsto_const[of c], of f d]
    4.60          tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
    4.61  
    4.62  
    4.63 @@ -1001,11 +1001,11 @@
    4.64  
    4.65  lemma not_tendsto_and_filterlim_at_infinity:
    4.66    assumes "F \<noteq> bot"
    4.67 -  assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F" 
    4.68 +  assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F"
    4.69    assumes "filterlim f at_infinity F"
    4.70    shows   False
    4.71  proof -
    4.72 -  from tendstoD[OF assms(2), of "1/2"] 
    4.73 +  from tendstoD[OF assms(2), of "1/2"]
    4.74      have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
    4.75    moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
    4.76      have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
    4.77 @@ -1037,7 +1037,7 @@
    4.78    thus ?thesis by eventually_elim auto
    4.79  qed
    4.80  
    4.81 -lemma tendsto_of_nat [tendsto_intros]: 
    4.82 +lemma tendsto_of_nat [tendsto_intros]:
    4.83    "filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
    4.84  proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
    4.85    fix r :: real assume r: "r > 0"
    4.86 @@ -1164,7 +1164,7 @@
    4.87    fix r :: real assume r: "r > 0"
    4.88    from assms(1) have "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" by (rule tendsto_norm)
    4.89    hence "eventually (\<lambda>x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all
    4.90 -  moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all 
    4.91 +  moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all
    4.92    with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F"
    4.93      unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all
    4.94    ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F"
    4.95 @@ -1506,7 +1506,7 @@
    4.96  
    4.97  lemma eventually_at2:
    4.98    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    4.99 -  unfolding eventually_at dist_nz by auto
   4.100 +  unfolding eventually_at by auto
   4.101  
   4.102  lemma Lim_transform:
   4.103    fixes a b :: "'a::real_normed_vector"
   4.104 @@ -1526,28 +1526,16 @@
   4.105    done
   4.106  
   4.107  lemma Lim_transform_within:
   4.108 -  assumes "0 < d"
   4.109 -    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
   4.110 -    and "(f \<longlongrightarrow> l) (at x within S)"
   4.111 +  assumes "(f \<longlongrightarrow> l) (at x within S)"
   4.112 +    and "0 < d"
   4.113 +    and "\<And>x'. \<lbrakk>x'\<in>S; 0 < dist x' x; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   4.114    shows "(g \<longlongrightarrow> l) (at x within S)"
   4.115  proof (rule Lim_transform_eventually)
   4.116    show "eventually (\<lambda>x. f x = g x) (at x within S)"
   4.117 -    using assms(1,2) by (auto simp: dist_nz eventually_at)
   4.118 +    using assms by (auto simp: eventually_at)
   4.119    show "(f \<longlongrightarrow> l) (at x within S)" by fact
   4.120  qed
   4.121  
   4.122 -lemma Lim_transform_at:
   4.123 -  assumes "0 < d"
   4.124 -    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
   4.125 -    and "(f \<longlongrightarrow> l) (at x)"
   4.126 -  shows "(g \<longlongrightarrow> l) (at x)"
   4.127 -  using _ assms(3)
   4.128 -proof (rule Lim_transform_eventually)
   4.129 -  show "eventually (\<lambda>x. f x = g x) (at x)"
   4.130 -    unfolding eventually_at2
   4.131 -    using assms(1,2) by auto
   4.132 -qed
   4.133 -
   4.134  text\<open>Common case assuming being away from some crucial point like 0.\<close>
   4.135  
   4.136  lemma Lim_transform_away_within:
   4.137 @@ -1574,15 +1562,15 @@
   4.138  text\<open>Alternatively, within an open set.\<close>
   4.139  
   4.140  lemma Lim_transform_within_open:
   4.141 -  assumes "open S" and "a \<in> S"
   4.142 -    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
   4.143 -    and "(f \<longlongrightarrow> l) (at a)"
   4.144 -  shows "(g \<longlongrightarrow> l) (at a)"
   4.145 +  assumes "(f \<longlongrightarrow> l) (at a within T)"
   4.146 +    and "open s" and "a \<in> s"
   4.147 +    and "\<And>x. \<lbrakk>x\<in>s; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
   4.148 +  shows "(g \<longlongrightarrow> l) (at a within T)"
   4.149  proof (rule Lim_transform_eventually)
   4.150 -  show "eventually (\<lambda>x. f x = g x) (at a)"
   4.151 +  show "eventually (\<lambda>x. f x = g x) (at a within T)"
   4.152      unfolding eventually_at_topological
   4.153 -    using assms(1,2,3) by auto
   4.154 -  show "(f \<longlongrightarrow> l) (at a)" by fact
   4.155 +    using assms by auto
   4.156 +  show "(f \<longlongrightarrow> l) (at a within T)" by fact
   4.157  qed
   4.158  
   4.159  text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
   4.160 @@ -1642,7 +1630,7 @@
   4.161    fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   4.162    have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
   4.163    also note n
   4.164 -  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e 
   4.165 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
   4.166      by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
   4.167  qed
   4.168  
   4.169 @@ -1660,9 +1648,9 @@
   4.170  
   4.171  lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
   4.172  proof (rule Lim_transform_eventually)
   4.173 -  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 
   4.174 +  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
   4.175                          of_nat n / of_nat (Suc n)) sequentially"
   4.176 -    using eventually_gt_at_top[of "0::nat"] 
   4.177 +    using eventually_gt_at_top[of "0::nat"]
   4.178      by eventually_elim (simp add: field_simps del: of_nat_Suc)
   4.179    have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> inverse 1"
   4.180      by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
   4.181 @@ -1738,11 +1726,11 @@
   4.182    thus ?thesis by (auto simp: convergent_def)
   4.183  qed
   4.184  
   4.185 -lemma convergent_of_real: 
   4.186 +lemma convergent_of_real:
   4.187    "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
   4.188    unfolding convergent_def by (blast intro!: tendsto_of_real)
   4.189  
   4.190 -lemma convergent_add_const_iff: 
   4.191 +lemma convergent_add_const_iff:
   4.192    "convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   4.193  proof
   4.194    assume "convergent (\<lambda>n. c + f n)"
   4.195 @@ -1752,11 +1740,11 @@
   4.196    from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
   4.197  qed
   4.198  
   4.199 -lemma convergent_add_const_right_iff: 
   4.200 +lemma convergent_add_const_right_iff:
   4.201    "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   4.202    using convergent_add_const_iff[of c f] by (simp add: add_ac)
   4.203  
   4.204 -lemma convergent_diff_const_right_iff: 
   4.205 +lemma convergent_diff_const_right_iff:
   4.206    "convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   4.207    using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
   4.208  
   4.209 @@ -1772,7 +1760,7 @@
   4.210    shows   "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
   4.211  proof
   4.212    assume "convergent (\<lambda>n. c * f n)"
   4.213 -  from assms convergent_mult[OF this convergent_const[of "inverse c"]] 
   4.214 +  from assms convergent_mult[OF this convergent_const[of "inverse c"]]
   4.215      show "convergent f" by (simp add: field_simps)
   4.216  next
   4.217    assume "convergent f"
     5.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Jan 06 16:17:50 2016 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Thu Jan 07 17:40:55 2016 +0000
     5.3 @@ -99,21 +99,21 @@
     5.4        case le show ?diff_fg
     5.5          apply (rule differentiable_transform_within [where d = "dist x c" and f = f])
     5.6          using x le st
     5.7 -        apply (simp_all add: dist_real_def dist_nz [symmetric])
     5.8 +        apply (simp_all add: dist_real_def)
     5.9          apply (rule differentiable_at_withinI)
    5.10          apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all)
    5.11          apply (blast intro: open_greaterThanLessThan finite_imp_closed)
    5.12 -        apply (force elim!: differentiable_subset)
    5.13 +        apply (force elim!: differentiable_subset)+
    5.14          done
    5.15      next
    5.16        case ge show ?diff_fg
    5.17          apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
    5.18          using x ge st
    5.19 -        apply (simp_all add: dist_real_def dist_nz [symmetric])
    5.20 +        apply (simp_all add: dist_real_def)
    5.21          apply (rule differentiable_at_withinI)
    5.22          apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all)
    5.23          apply (blast intro: open_greaterThanLessThan finite_imp_closed)
    5.24 -        apply (force elim!: differentiable_subset)
    5.25 +        apply (force elim!: differentiable_subset)+
    5.26          done
    5.27      qed
    5.28    }
    5.29 @@ -351,11 +351,11 @@
    5.30      have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg")
    5.31      proof (cases x c rule: le_cases)
    5.32        case le show ?diff_fg
    5.33 -        apply (rule differentiable_transform_at [of "dist x c" _ f])
    5.34 +        apply (rule differentiable_transform_within [where f=f and d = "dist x c"])
    5.35          using x dist_real_def le st by (auto simp: C1_differentiable_on_eq)
    5.36      next
    5.37        case ge show ?diff_fg
    5.38 -        apply (rule differentiable_transform_at [of "dist x c" _ g])
    5.39 +        apply (rule differentiable_transform_within [where f=g and d = "dist x c"])
    5.40          using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq)
    5.41      qed
    5.42    }
    5.43 @@ -370,18 +370,20 @@
    5.44        apply (rule continuous_on_eq [OF fcon])
    5.45        apply (simp add:)
    5.46        apply (rule vector_derivative_at [symmetric])
    5.47 -      apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at)
    5.48 +      apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
    5.49        apply (simp_all add: dist_norm vector_derivative_works [symmetric])
    5.50 -      using f_diff
    5.51 -      by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1))
    5.52 +      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1))
    5.53 +      apply auto
    5.54 +      done
    5.55      moreover have "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
    5.56        apply (rule continuous_on_eq [OF gcon])
    5.57        apply (simp add:)
    5.58        apply (rule vector_derivative_at [symmetric])
    5.59 -      apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at)
    5.60 +      apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
    5.61        apply (simp_all add: dist_norm vector_derivative_works [symmetric])
    5.62 -      using g_diff
    5.63 -      by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2))
    5.64 +      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2))
    5.65 +      apply auto
    5.66 +      done
    5.67      ultimately have "continuous_on ({a<..<b} - insert c (s \<union> t))
    5.68          (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
    5.69        apply (rule continuous_on_subset [OF continuous_on_open_Un], auto)
    5.70 @@ -435,7 +437,7 @@
    5.71               and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
    5.72      using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    5.73    then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
    5.74 -    apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at)
    5.75 +    apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_within)
    5.76      using that
    5.77      apply (simp_all add: dist_real_def joinpaths_def)
    5.78      apply (rule differentiable_chain_at derivative_intros | force)+
    5.79 @@ -450,9 +452,10 @@
    5.80      using co12 by (rule continuous_on_subset) force
    5.81    then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))"
    5.82      apply (rule continuous_on_eq [OF _ vector_derivative_at])
    5.83 -    apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at)
    5.84 +    apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
    5.85      apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric])
    5.86      apply (force intro: g1D differentiable_chain_at)
    5.87 +    apply auto
    5.88      done
    5.89    have "continuous_on ({0..1} - insert 1 (op * 2 ` s))
    5.90                        ((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))"
    5.91 @@ -481,7 +484,7 @@
    5.92               and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
    5.93      using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    5.94    then have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
    5.95 -    apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at)
    5.96 +    apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_within)
    5.97      using that
    5.98      apply (simp_all add: dist_real_def joinpaths_def)
    5.99      apply (auto simp: dist_real_def joinpaths_def field_simps)
   5.100 @@ -496,7 +499,7 @@
   5.101      using co12 by (rule continuous_on_subset) force
   5.102    then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
   5.103      apply (rule continuous_on_eq [OF _ vector_derivative_at])
   5.104 -    apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at)
   5.105 +    apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
   5.106      apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
   5.107                  intro!: g2D differentiable_chain_at)
   5.108      done
   5.109 @@ -755,7 +758,7 @@
   5.110    have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
   5.111              vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
   5.112              2 *\<^sub>R vector_derivative g1 (at (z*2))" for z
   5.113 -    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
   5.114 +    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z - 1/2\<bar>"]])
   5.115      apply (simp_all add: dist_real_def abs_if split: split_if_asm)
   5.116      apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
   5.117      apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
   5.118 @@ -765,7 +768,7 @@
   5.119    have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
   5.120              vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
   5.121              2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z
   5.122 -    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"]])
   5.123 +    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x - 1))" and d = "\<bar>z - 1/2\<bar>"]])
   5.124      apply (simp_all add: dist_real_def abs_if split: split_if_asm)
   5.125      apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
   5.126      apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
   5.127 @@ -816,7 +819,7 @@
   5.128    have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow>
   5.129              vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
   5.130              2 *\<^sub>R vector_derivative g1 (at z)"  for z
   5.131 -    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
   5.132 +    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z-1)/2\<bar>"]])
   5.133      apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
   5.134      apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def])
   5.135      using s1
   5.136 @@ -850,7 +853,7 @@
   5.137    have g2: "\<lbrakk>0 < z; z < 1; z \<notin> s2\<rbrakk> \<Longrightarrow>
   5.138              vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
   5.139              2 *\<^sub>R vector_derivative g2 (at z)" for z
   5.140 -    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z/2\<bar>" _ "(\<lambda>x. g2(2*x-1))"]])
   5.141 +    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x-1))" and d = "\<bar>z/2\<bar>"]])
   5.142      apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
   5.143      apply (rule vector_diff_chain_at [of "\<lambda>x. x*2-1" 2 _ g2, simplified o_def])
   5.144      using s2
   5.145 @@ -916,7 +919,7 @@
   5.146      have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a) ` s \<Longrightarrow>
   5.147           vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
   5.148        unfolding shiftpath_def
   5.149 -      apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1-a) x" _ "(\<lambda>x. g(a+x))"]])
   5.150 +      apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x))" and d = "dist(1-a) x"]])
   5.151          apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
   5.152        apply (rule vector_diff_chain_at [of "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one])
   5.153         apply (intro derivative_eq_intros | simp)+
   5.154 @@ -929,7 +932,7 @@
   5.155      have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a + 1) ` s \<Longrightarrow>
   5.156            vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
   5.157        unfolding shiftpath_def
   5.158 -      apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1-a) x" _ "(\<lambda>x. g(a+x-1))"]])
   5.159 +      apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x-1))" and d = "dist (1-a) x"]])
   5.160          apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
   5.161        apply (rule vector_diff_chain_at [of "\<lambda>x. x+a-1" 1 _ g, simplified o_def scaleR_one])
   5.162         apply (intro derivative_eq_intros | simp)+
   5.163 @@ -986,12 +989,12 @@
   5.164            vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
   5.165        apply (rule vector_derivative_at_within_ivl
   5.166                    [OF has_vector_derivative_transform_within_open
   5.167 -                      [of "{0<..<1}-s" _ "(shiftpath (1 - a) (shiftpath a g))"]])
   5.168 +                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
   5.169        using s g assms x
   5.170        apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
   5.171                          vector_derivative_within_interior vector_derivative_works [symmetric])
   5.172 -      apply (rule Derivative.differentiable_transform_at [of "min x (1-x)", OF _ _ gx])
   5.173 -      apply (auto simp: dist_real_def shiftpath_shiftpath abs_if)
   5.174 +      apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
   5.175 +      apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: split_if_asm)
   5.176        done
   5.177    } note vd = this
   5.178    have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
   5.179 @@ -4041,14 +4044,16 @@
   5.180        using pi_ge_two e
   5.181        by (force simp: winding_number_valid_path p field_simps norm_divide norm_mult intro: less_le_trans)
   5.182    } note cmod_wn_diff = this
   5.183 -  show ?thesis
   5.184 -    apply (rule continuous_transform_at [of "min d e / 2" _ "winding_number p"])
   5.185 -    apply (auto simp: \<open>d>0\<close> \<open>e>0\<close> dist_norm wnwn simp del: less_divide_eq_numeral1)
   5.186 +  then have "isCont (winding_number p) z"
   5.187      apply (simp add: continuous_at_eps_delta, clarify)
   5.188      apply (rule_tac x="min (pe/4) (e/2*pe^2/L/4)" in exI)
   5.189      using \<open>pe>0\<close> \<open>L>0\<close>
   5.190      apply (simp add: dist_norm cmod_wn_diff)
   5.191      done
   5.192 +  then show ?thesis
   5.193 +    apply (rule continuous_transform_within [where d = "min d e / 2"])
   5.194 +    apply (auto simp: \<open>d>0\<close> \<open>e>0\<close> dist_norm wnwn)
   5.195 +    done
   5.196  qed
   5.197  
   5.198  corollary continuous_on_winding_number:
   5.199 @@ -4393,14 +4398,15 @@
   5.200        done
   5.201    next
   5.202      case False
   5.203 -    then have dxz: "dist x z > 0" using dist_nz by blast
   5.204 +    then have dxz: "dist x z > 0" by auto
   5.205      have cf: "continuous (at x within s) f"
   5.206        using conf continuous_on_eq_continuous_within that by blast
   5.207 -    show ?thesis
   5.208 -      apply (rule continuous_transform_within [OF dxz that, of "\<lambda>w::complex. (f w - f z)/(w - z)"])
   5.209 +    have "continuous (at x within s) (\<lambda>w. (f w - f z) / (w - z))"
   5.210 +      by (rule cf continuous_intros | simp add: False)+
   5.211 +    then show ?thesis
   5.212 +      apply (rule continuous_transform_within [OF _ dxz that, of "\<lambda>w::complex. (f w - f z)/(w - z)"])
   5.213        apply (force simp: dist_commute)
   5.214 -      apply (rule cf continuous_intros)+
   5.215 -      using False by auto
   5.216 +      done
   5.217    qed
   5.218    have fink': "finite (insert z k)" using \<open>finite k\<close> by blast
   5.219    have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \<gamma>"
   5.220 @@ -5485,7 +5491,7 @@
   5.221      done
   5.222    show ?thes2
   5.223      apply (simp add: DERIV_within_iff del: power_Suc)
   5.224 -    apply (rule Lim_transform_at [OF \<open>0 < d\<close> _ tendsto_mult_left [OF *]])
   5.225 +    apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
   5.226      apply (simp add: \<open>k \<noteq> 0\<close> **)
   5.227      done
   5.228  qed
   5.229 @@ -5566,7 +5572,7 @@
   5.230        by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
   5.231      have holf_ball: "f holomorphic_on ball z r" using holf_cball
   5.232        using ball_subset_cball holomorphic_on_subset by blast
   5.233 -    { fix w  assume w: "w \<in> ball z r"  
   5.234 +    { fix w  assume w: "w \<in> ball z r"
   5.235        have intf: "(\<lambda>u. f u / (u - w)\<^sup>2) contour_integrable_on circlepath z r"
   5.236          by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
   5.237        have fder': "(f has_field_derivative 1 / (2 * of_real pi * \<i>) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2))
   5.238 @@ -5595,7 +5601,7 @@
   5.239      by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
   5.240  qed
   5.241  
   5.242 -lemma holomorphic_deriv [holomorphic_intros]: 
   5.243 +lemma holomorphic_deriv [holomorphic_intros]:
   5.244      "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
   5.245  by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
   5.246  
   5.247 @@ -5608,10 +5614,10 @@
   5.248  lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
   5.249    unfolding analytic_on_def using holomorphic_higher_deriv by blast
   5.250  
   5.251 -lemma has_field_derivative_higher_deriv: 
   5.252 -     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> 
   5.253 +lemma has_field_derivative_higher_deriv:
   5.254 +     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
   5.255        \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
   5.256 -by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply 
   5.257 +by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply
   5.258           funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
   5.259  
   5.260  
   5.261 @@ -5627,7 +5633,7 @@
   5.262    shows "f analytic_on s"
   5.263  proof -
   5.264    { fix z  assume "z \<in> s"
   5.265 -    with assms obtain e a where 
   5.266 +    with assms obtain e a where
   5.267              "0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
   5.268          and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
   5.269                        \<Longrightarrow> contour_integral (linepath a b) f +
   5.270 @@ -5661,14 +5667,14 @@
   5.271    shows "f analytic_on s"
   5.272  proof -
   5.273    { fix z  assume "z \<in> s"
   5.274 -    with assms obtain t where 
   5.275 +    with assms obtain t where
   5.276              "open t" and z: "z \<in> t" and contf: "continuous_on t f"
   5.277          and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
   5.278                        \<Longrightarrow> contour_integral (linepath a b) f +
   5.279                            contour_integral (linepath b c) f +
   5.280                            contour_integral (linepath c a) f = 0"
   5.281        by force
   5.282 -    then obtain e where "e>0" and e: "ball z e \<subseteq> t" 
   5.283 +    then obtain e where "e>0" and e: "ball z e \<subseteq> t"
   5.284        using open_contains_ball by blast
   5.285      have [simp]: "continuous_on (ball z e) f" using contf
   5.286        using continuous_on_subset e by blast
   5.287 @@ -5689,7 +5695,7 @@
   5.288  qed
   5.289  
   5.290  proposition Morera_triangle:
   5.291 -    "\<lbrakk>continuous_on s f; open s; 
   5.292 +    "\<lbrakk>continuous_on s f; open s;
   5.293        \<And>a b c. convex hull {a,b,c} \<subseteq> s
   5.294                \<longrightarrow> contour_integral (linepath a b) f +
   5.295                    contour_integral (linepath b c) f +
   5.296 @@ -5701,7 +5707,7 @@
   5.297  
   5.298  subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
   5.299  
   5.300 -lemma higher_deriv_linear [simp]: 
   5.301 +lemma higher_deriv_linear [simp]:
   5.302      "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
   5.303    by (induction n) (auto simp: deriv_const deriv_linear)
   5.304  
   5.305 @@ -5718,21 +5724,21 @@
   5.306       "(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)"
   5.307    by (simp add: id_def)
   5.308  
   5.309 -lemma has_complex_derivative_funpow_1: 
   5.310 +lemma has_complex_derivative_funpow_1:
   5.311       "\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (f^^n has_field_derivative 1) (at z)"
   5.312    apply (induction n)
   5.313    apply auto
   5.314    apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one)
   5.315    by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
   5.316  
   5.317 -proposition higher_deriv_uminus: 
   5.318 +proposition higher_deriv_uminus:
   5.319    assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
   5.320      shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
   5.321  using z
   5.322  proof (induction n arbitrary: z)
   5.323    case 0 then show ?case by simp
   5.324  next
   5.325 -  case (Suc n z) 
   5.326 +  case (Suc n z)
   5.327    have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   5.328      using Suc.prems assms has_field_derivative_higher_deriv by auto
   5.329    show ?case
   5.330 @@ -5744,7 +5750,7 @@
   5.331      done
   5.332  qed
   5.333  
   5.334 -proposition higher_deriv_add: 
   5.335 +proposition higher_deriv_add:
   5.336    fixes z::complex
   5.337    assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   5.338      shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
   5.339 @@ -5752,7 +5758,7 @@
   5.340  proof (induction n arbitrary: z)
   5.341    case 0 then show ?case by simp
   5.342  next
   5.343 -  case (Suc n z) 
   5.344 +  case (Suc n z)
   5.345    have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   5.346            "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
   5.347      using Suc.prems assms has_field_derivative_higher_deriv by auto
   5.348 @@ -5765,7 +5771,7 @@
   5.349      done
   5.350  qed
   5.351  
   5.352 -corollary higher_deriv_diff: 
   5.353 +corollary higher_deriv_diff:
   5.354    fixes z::complex
   5.355    assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   5.356      shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
   5.357 @@ -5781,13 +5787,13 @@
   5.358  proposition higher_deriv_mult:
   5.359    fixes z::complex
   5.360    assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   5.361 -    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
   5.362 +    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
   5.363             (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
   5.364  using z
   5.365  proof (induction n arbitrary: z)
   5.366    case 0 then show ?case by simp
   5.367  next
   5.368 -  case (Suc n z) 
   5.369 +  case (Suc n z)
   5.370    have *: "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   5.371            "\<And>n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
   5.372      using Suc.prems assms has_field_derivative_higher_deriv by auto
   5.373 @@ -5801,7 +5807,7 @@
   5.374    show ?case
   5.375      apply (simp only: funpow.simps o_apply)
   5.376      apply (rule DERIV_imp_deriv)
   5.377 -    apply (rule DERIV_transform_within_open 
   5.378 +    apply (rule DERIV_transform_within_open
   5.379               [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
   5.380      apply (simp add: algebra_simps)
   5.381      apply (rule DERIV_cong [OF DERIV_setsum])
   5.382 @@ -5817,7 +5823,7 @@
   5.383        and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
   5.384      shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
   5.385  using z
   5.386 -by (induction i arbitrary: z) 
   5.387 +by (induction i arbitrary: z)
   5.388     (auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
   5.389  
   5.390  proposition higher_deriv_compose_linear:
   5.391 @@ -5829,7 +5835,7 @@
   5.392  proof (induction n arbitrary: z)
   5.393    case 0 then show ?case by simp
   5.394  next
   5.395 -  case (Suc n z) 
   5.396 +  case (Suc n z)
   5.397    have holo0: "f holomorphic_on op * u ` s"
   5.398      by (meson fg f holomorphic_on_subset image_subset_iff)
   5.399    have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
   5.400 @@ -5867,7 +5873,7 @@
   5.401      by simp
   5.402  qed
   5.403  
   5.404 -lemma higher_deriv_add_at: 
   5.405 +lemma higher_deriv_add_at:
   5.406    assumes "f analytic_on {z}" "g analytic_on {z}"
   5.407      shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
   5.408  proof -
   5.409 @@ -5877,7 +5883,7 @@
   5.410      by (auto simp: analytic_at_two)
   5.411  qed
   5.412  
   5.413 -lemma higher_deriv_diff_at: 
   5.414 +lemma higher_deriv_diff_at:
   5.415    assumes "f analytic_on {z}" "g analytic_on {z}"
   5.416      shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
   5.417  proof -
   5.418 @@ -5887,14 +5893,14 @@
   5.419      by (auto simp: analytic_at_two)
   5.420  qed
   5.421  
   5.422 -lemma higher_deriv_uminus_at: 
   5.423 +lemma higher_deriv_uminus_at:
   5.424     "f analytic_on {z}  \<Longrightarrow> (deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
   5.425    using higher_deriv_uminus
   5.426      by (auto simp: analytic_at)
   5.427  
   5.428 -lemma higher_deriv_mult_at: 
   5.429 +lemma higher_deriv_mult_at:
   5.430    assumes "f analytic_on {z}" "g analytic_on {z}"
   5.431 -    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
   5.432 +    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
   5.433             (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
   5.434  proof -
   5.435    have "f analytic_on {z} \<and> g analytic_on {z}"
   5.436 @@ -5911,17 +5917,17 @@
   5.437    assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
   5.438      shows "f holomorphic_on s"
   5.439  proof -
   5.440 -  { fix z 
   5.441 +  { fix z
   5.442      assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
   5.443      have "f complex_differentiable at z"
   5.444      proof (cases "z \<in> k")
   5.445        case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
   5.446      next
   5.447        case True
   5.448 -      with finite_set_avoid [OF k, of z] 
   5.449 +      with finite_set_avoid [OF k, of z]
   5.450        obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
   5.451          by blast
   5.452 -      obtain e where "e>0" and e: "ball z e \<subseteq> s" 
   5.453 +      obtain e where "e>0" and e: "ball z e \<subseteq> s"
   5.454          using  s \<open>z \<in> s\<close> by (force simp add: open_contains_ball)
   5.455        have fde: "continuous_on (ball z (min d e)) f"
   5.456          by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
   5.457 @@ -5930,7 +5936,7 @@
   5.458          apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
   5.459           apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
   5.460          apply (rule cdf)
   5.461 -        apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset 
   5.462 +        apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
   5.463                 interior_mono interior_subset subset_hull)
   5.464          done
   5.465        then have "f holomorphic_on ball z (min d e)"
   5.466 @@ -5952,8 +5958,8 @@
   5.467        shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
   5.468    apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
   5.469    apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
   5.470 -  using no_isolated_singularity [where s = "interior s"] 
   5.471 -  apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset 
   5.472 +  using no_isolated_singularity [where s = "interior s"]
   5.473 +  apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset
   5.474                 has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
   5.475    using assms
   5.476    apply auto
   5.477 @@ -6021,7 +6027,7 @@
   5.478      by simp
   5.479    show ?thes1 using *
   5.480      using contour_integrable_on_def by blast
   5.481 -  show ?thes2 
   5.482 +  show ?thes2
   5.483      unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
   5.484  qed
   5.485  
   5.486 @@ -6065,13 +6071,13 @@
   5.487      done
   5.488    obtain B where "0 < B" and B: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> B"
   5.489      by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
   5.490 -  obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k" 
   5.491 +  obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
   5.492               and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
   5.493      apply (rule_tac k = "r - dist z w" in that)
   5.494      using w
   5.495      apply (auto simp: dist_norm norm_minus_commute)
   5.496      by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   5.497 -  have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r). 
   5.498 +  have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
   5.499                  norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
   5.500            if "0 < e" for e
   5.501    proof -
   5.502 @@ -6111,7 +6117,7 @@
   5.503        also have "... < e * k"
   5.504          using \<open>0 < B\<close> N by (simp add: divide_simps)
   5.505        also have "... \<le> e * norm (u - w)"
   5.506 -        using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm) 
   5.507 +        using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm)
   5.508        finally show ?thesis
   5.509          by (simp add: divide_simps norm_divide del: power_Suc)
   5.510      qed
   5.511 @@ -6140,10 +6146,10 @@
   5.512    then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
   5.513               sums (2 * of_real pi * ii * f w)"
   5.514      using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
   5.515 -  then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2))) 
   5.516 +  then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
   5.517              sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
   5.518      by (rule Series.sums_divide)
   5.519 -  then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2))) 
   5.520 +  then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
   5.521              sums f w"
   5.522      by (simp add: field_simps)
   5.523    then show ?thesis
   5.524 @@ -6155,7 +6161,7 @@
   5.525  
   5.526  text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
   5.527  
   5.528 -lemma Liouville_weak_0: 
   5.529 +lemma Liouville_weak_0:
   5.530    assumes holf: "f holomorphic_on UNIV" and inf: "(f \<longlongrightarrow> 0) at_infinity"
   5.531      shows "f z = 0"
   5.532  proof (rule ccontr)
   5.533 @@ -6181,14 +6187,14 @@
   5.534      by (auto simp: norm_mult norm_divide divide_simps)
   5.535  qed
   5.536  
   5.537 -proposition Liouville_weak: 
   5.538 +proposition Liouville_weak:
   5.539    assumes "f holomorphic_on UNIV" and "(f \<longlongrightarrow> l) at_infinity"
   5.540      shows "f z = l"
   5.541    using Liouville_weak_0 [of "\<lambda>z. f z - l"]
   5.542    by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
   5.543  
   5.544  
   5.545 -proposition Liouville_weak_inverse: 
   5.546 +proposition Liouville_weak_inverse:
   5.547    assumes "f holomorphic_on UNIV" and unbounded: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
   5.548      obtains z where "f z = 0"
   5.549  proof -
   5.550 @@ -6210,7 +6216,7 @@
   5.551  
   5.552  text\<open> In particular we get the Fundamental Theorem of Algebra.\<close>
   5.553  
   5.554 -theorem fundamental_theorem_of_algebra: 
   5.555 +theorem fundamental_theorem_of_algebra:
   5.556      fixes a :: "nat \<Rightarrow> complex"
   5.557    assumes "a 0 = 0 \<or> (\<exists>i \<in> {1..n}. a i \<noteq> 0)"
   5.558    obtains z where "(\<Sum>i\<le>n. a i * z^i) = 0"
   5.559 @@ -6257,7 +6263,7 @@
   5.560         if w: "w \<in> ball z r" for w
   5.561    proof -
   5.562      def d \<equiv> "(r - norm(w - z))"
   5.563 -    have "0 < d"  "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm) 
   5.564 +    have "0 < d"  "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
   5.565      have dle: "\<And>u. cmod (z - u) = r \<Longrightarrow> d \<le> cmod (u - w)"
   5.566        unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   5.567      have ev_int: "\<forall>\<^sub>F n in F. (\<lambda>u. f n u / (u - w)) contour_integrable_on circlepath z r"
   5.568 @@ -6308,17 +6314,17 @@
   5.569  
   5.570  proposition has_complex_derivative_uniform_limit:
   5.571    fixes z::complex
   5.572 -  assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> 
   5.573 +  assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
   5.574                                 (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
   5.575        and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
   5.576        and F:  "~ trivial_limit F" and "0 < r"
   5.577    obtains g' where
   5.578 -      "continuous_on (cball z r) g" 
   5.579 +      "continuous_on (cball z r) g"
   5.580        "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
   5.581  proof -
   5.582    let ?conint = "contour_integral (circlepath z r)"
   5.583    have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
   5.584 -    by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; 
   5.585 +    by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
   5.586               auto simp: holomorphic_on_open complex_differentiable_def)+
   5.587    then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
   5.588      using DERIV_deriv_iff_has_field_derivative
   5.589 @@ -6327,8 +6333,8 @@
   5.590      by (simp add: DERIV_imp_deriv)
   5.591    have tends_f'n_g': "((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F" if w: "w \<in> ball z r" for w
   5.592    proof -
   5.593 -    have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)" 
   5.594 -             if cont_fn: "continuous_on (cball z r) (f n)" 
   5.595 +    have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
   5.596 +             if cont_fn: "continuous_on (cball z r) (f n)"
   5.597               and fnd: "\<And>w. w \<in> ball z r \<Longrightarrow> (f n has_field_derivative f' n w) (at w)" for n
   5.598      proof -
   5.599        have hol_fn: "f n holomorphic_on ball z r"
   5.600 @@ -6336,7 +6342,7 @@
   5.601        have "(f n has_field_derivative 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)) (at w)"
   5.602          by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w])
   5.603        then have f': "f' n w = 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)"
   5.604 -        using DERIV_unique [OF fnd] w by blast 
   5.605 +        using DERIV_unique [OF fnd] w by blast
   5.606        show ?thesis
   5.607          by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps)
   5.608      qed
   5.609 @@ -6358,7 +6364,7 @@
   5.610        apply (simp add: \<open>0 < d\<close>)
   5.611        apply (force simp add: dist_norm dle intro: less_le_trans)
   5.612        done
   5.613 -    have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2)) 
   5.614 +    have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
   5.615               \<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
   5.616        by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
   5.617      then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
     6.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Jan 06 16:17:50 2016 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Jan 07 17:40:55 2016 +0000
     6.3 @@ -907,7 +907,7 @@
     6.4    from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
     6.5      by (simp add: has_field_derivative_def s)
     6.6    have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
     6.7 -    by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
     6.8 +    by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
     6.9         (insert g, auto simp: sums_iff)
    6.10    thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
    6.11      by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
     7.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Jan 06 16:17:50 2016 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jan 07 17:40:55 2016 +0000
     7.3 @@ -1345,9 +1345,9 @@
     7.4      by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
     7.5    then show ?thesis
     7.6      apply (simp add: continuous_at)
     7.7 -    apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
     7.8 +    apply (rule Lim_transform_within_open [where s= "-{z. z \<in> \<real> & 0 \<le> Re z}" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
     7.9 +    apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
    7.10      apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
    7.11 -    apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
    7.12      done
    7.13  qed
    7.14  
     8.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jan 06 16:17:50 2016 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jan 07 17:40:55 2016 +0000
     8.3 @@ -1368,9 +1368,7 @@
     8.4    have "x \<in> s" using assms(1,3) by auto
     8.5    assume "\<not> ?thesis"
     8.6    then obtain y where "y\<in>s" and y: "f x > f y" by auto
     8.7 -  then have xy: "0 < dist x y"
     8.8 -    by (auto simp add: dist_nz[symmetric])
     8.9 -
    8.10 +  then have xy: "0 < dist x y"  by auto
    8.11    then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
    8.12      using real_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
    8.13    then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
    8.14 @@ -3401,8 +3399,8 @@
    8.15    also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
    8.16      by (auto simp: continuous_on_closed_vimage)
    8.17    hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
    8.18 -  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
    8.19 -qed 
    8.20 +  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
    8.21 +qed
    8.22  
    8.23  lemma interior_real_semiline':
    8.24    fixes a :: real
    8.25 @@ -3434,7 +3432,7 @@
    8.26  lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
    8.27  proof-
    8.28    have "{a..b} = {a..} \<inter> {..b}" by auto
    8.29 -  also have "interior ... = {a<..} \<inter> {..<b}" 
    8.30 +  also have "interior ... = {a<..} \<inter> {..<b}"
    8.31      by (simp add: interior_real_semiline interior_real_semiline')
    8.32    also have "... = {a<..<b}" by auto
    8.33    finally show ?thesis .
     9.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jan 06 16:17:50 2016 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 07 17:40:55 2016 +0000
     9.3 @@ -165,36 +165,23 @@
     9.4  subsubsection \<open>Limit transformation for derivatives\<close>
     9.5  
     9.6  lemma has_derivative_transform_within:
     9.7 -  assumes "0 < d"
     9.8 +  assumes "(f has_derivative f') (at x within s)"
     9.9 +    and "0 < d"
    9.10      and "x \<in> s"
    9.11 -    and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
    9.12 -    and "(f has_derivative f') (at x within s)"
    9.13 +    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
    9.14    shows "(g has_derivative f') (at x within s)"
    9.15    using assms
    9.16 -  unfolding has_derivative_within
    9.17 -  apply clarify
    9.18 -  apply (rule Lim_transform_within, auto)
    9.19 -  done
    9.20 -
    9.21 -lemma has_derivative_transform_at:
    9.22 -  assumes "0 < d"
    9.23 -    and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
    9.24 -    and "(f has_derivative f') (at x)"
    9.25 -  shows "(g has_derivative f') (at x)"
    9.26 -  using has_derivative_transform_within [of d x UNIV f g f'] assms
    9.27 -  by simp
    9.28 +  unfolding has_derivative_within  
    9.29 +  by (force simp add: intro: Lim_transform_within)
    9.30  
    9.31  lemma has_derivative_transform_within_open:
    9.32 -  assumes "open s"
    9.33 +  assumes "(f has_derivative f') (at x)"
    9.34 +    and "open s"
    9.35      and "x \<in> s"
    9.36 -    and "\<forall>y\<in>s. f y = g y"
    9.37 -    and "(f has_derivative f') (at x)"
    9.38 +    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
    9.39    shows "(g has_derivative f') (at x)"
    9.40 -  using assms
    9.41 -  unfolding has_derivative_at
    9.42 -  apply clarify
    9.43 -  apply (rule Lim_transform_within_open[OF assms(1,2)], auto)
    9.44 -  done
    9.45 +  using assms  unfolding has_derivative_at
    9.46 +  by (force simp add: intro: Lim_transform_within_open)
    9.47  
    9.48  subsection \<open>Differentiability\<close>
    9.49  
    9.50 @@ -234,24 +221,13 @@
    9.51    by (metis at_within_interior interior_open)
    9.52  
    9.53  lemma differentiable_transform_within:
    9.54 -  assumes "0 < d"
    9.55 +  assumes "f differentiable (at x within s)"
    9.56 +    and "0 < d"
    9.57      and "x \<in> s"
    9.58 -    and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
    9.59 -  assumes "f differentiable (at x within s)"
    9.60 +    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
    9.61    shows "g differentiable (at x within s)"
    9.62 -  using assms(4)
    9.63 -  unfolding differentiable_def
    9.64 -  by (auto intro!: has_derivative_transform_within[OF assms(1-3)])
    9.65 -
    9.66 -lemma differentiable_transform_at:
    9.67 -  assumes "0 < d"
    9.68 -    and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
    9.69 -    and "f differentiable at x"
    9.70 -  shows "g differentiable at x"
    9.71 -  using assms(3)
    9.72 -  unfolding differentiable_def
    9.73 -  using has_derivative_transform_at[OF assms(1-2)]
    9.74 -  by auto
    9.75 +   using assms has_derivative_transform_within unfolding differentiable_def
    9.76 +   by blast
    9.77  
    9.78  
    9.79  subsection \<open>Frechet derivative and Jacobian matrix\<close>
    9.80 @@ -2263,7 +2239,7 @@
    9.81    from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
    9.82      by (simp add: has_field_derivative_def s)
    9.83    have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
    9.84 -    by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
    9.85 +    by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
    9.86         (insert g, auto simp: sums_iff)
    9.87    thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
    9.88      by (auto simp: summable_def differentiable_def has_field_derivative_def)
    9.89 @@ -2475,29 +2451,20 @@
    9.90  qed
    9.91  
    9.92  lemma has_vector_derivative_transform_within:
    9.93 -  assumes "0 < d"
    9.94 +  assumes "(f has_vector_derivative f') (at x within s)"
    9.95 +    and "0 < d"
    9.96      and "x \<in> s"
    9.97 -    and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
    9.98 -  assumes "(f has_vector_derivative f') (at x within s)"
    9.99 -  shows "(g has_vector_derivative f') (at x within s)"
   9.100 +    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   9.101 +    shows "(g has_vector_derivative f') (at x within s)"
   9.102    using assms
   9.103    unfolding has_vector_derivative_def
   9.104    by (rule has_derivative_transform_within)
   9.105  
   9.106 -lemma has_vector_derivative_transform_at:
   9.107 -  assumes "0 < d"
   9.108 -    and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
   9.109 -    and "(f has_vector_derivative f') (at x)"
   9.110 -  shows "(g has_vector_derivative f') (at x)"
   9.111 -  using assms
   9.112 -  unfolding has_vector_derivative_def
   9.113 -  by (rule has_derivative_transform_at)
   9.114 -
   9.115  lemma has_vector_derivative_transform_within_open:
   9.116 -  assumes "open s"
   9.117 +  assumes "(f has_vector_derivative f') (at x)"
   9.118 +    and "open s"
   9.119      and "x \<in> s"
   9.120 -    and "\<forall>y\<in>s. f y = g y"
   9.121 -    and "(f has_vector_derivative f') (at x)"
   9.122 +    and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
   9.123    shows "(g has_vector_derivative f') (at x)"
   9.124    using assms
   9.125    unfolding has_vector_derivative_def
    10.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Jan 06 16:17:50 2016 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Jan 07 17:40:55 2016 +0000
    10.3 @@ -843,7 +843,7 @@
    10.4      apply (rule that [OF \<open>path h\<close>])
    10.5      using assms h
    10.6      apply auto
    10.7 -    apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
    10.8 +    apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
    10.9      done
   10.10  qed
   10.11  
    11.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jan 06 16:17:50 2016 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 07 17:40:55 2016 +0000
    11.3 @@ -13,7 +13,7 @@
    11.4    "~~/src/HOL/Library/FuncSet"
    11.5    Linear_Algebra
    11.6    Norm_Arith
    11.7 -  
    11.8 +
    11.9  begin
   11.10  
   11.11  lemma image_affinity_interval:
   11.12 @@ -51,6 +51,11 @@
   11.13    shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
   11.14    by (fact tendsto_within_open)
   11.15  
   11.16 +lemma Lim_within_open_NO_MATCH:
   11.17 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   11.18 +  shows "a \<in> S \<Longrightarrow> NO_MATCH UNIV S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
   11.19 +using tendsto_within_open by blast
   11.20 +
   11.21  lemma continuous_on_union:
   11.22    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   11.23    by (fact continuous_on_closed_Un)
   11.24 @@ -1486,7 +1491,7 @@
   11.25      case False
   11.26      let ?d = "min d (dist a x)"
   11.27      have dp: "?d > 0"
   11.28 -      using False d(1) using dist_nz by auto
   11.29 +      using False d(1) by auto
   11.30      from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
   11.31        by auto
   11.32      with dp False show ?thesis
   11.33 @@ -1511,7 +1516,7 @@
   11.34        by blast
   11.35      let ?m = "min (e/2) (dist x y) "
   11.36      from e2 y(2) have mp: "?m > 0"
   11.37 -      by (simp add: dist_nz[symmetric])
   11.38 +      by simp
   11.39      from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
   11.40        by blast
   11.41      have th: "dist z y < e" using z y
   11.42 @@ -2312,11 +2317,11 @@
   11.43  
   11.44  lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
   11.45      (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
   11.46 -  by (auto simp add: tendsto_iff eventually_at_le dist_nz)
   11.47 +  by (auto simp add: tendsto_iff eventually_at_le)
   11.48  
   11.49  lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
   11.50      (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
   11.51 -  by (auto simp add: tendsto_iff eventually_at dist_nz)
   11.52 +  by (auto simp add: tendsto_iff eventually_at)
   11.53  
   11.54  lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
   11.55      (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   11.56 @@ -2665,9 +2670,9 @@
   11.57    by (metis closure_contains_Inf closure_minimal subset_eq)
   11.58  
   11.59  lemma atLeastAtMost_subset_contains_Inf:
   11.60 -  fixes A :: "real set" and a b :: real 
   11.61 +  fixes A :: "real set" and a b :: real
   11.62    shows "A \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {a..b}"
   11.63 -  by (rule closed_subset_contains_Inf) 
   11.64 +  by (rule closed_subset_contains_Inf)
   11.65       (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
   11.66  
   11.67  lemma not_trivial_limit_within_ball:
   11.68 @@ -2940,8 +2945,7 @@
   11.69              by (auto simp add: norm_minus_commute)
   11.70            also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
   11.71              unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
   11.72 -            unfolding distrib_right using \<open>x\<noteq>y\<close>[unfolded dist_nz, unfolded dist_norm]
   11.73 -            by auto
   11.74 +            unfolding distrib_right using \<open>x\<noteq>y\<close>  by auto
   11.75            also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
   11.76              by (auto simp add: dist_norm)
   11.77            finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
   11.78 @@ -3019,8 +3023,8 @@
   11.79      apply (simp only: dist_norm [symmetric])
   11.80      apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
   11.81      apply (rule mult_strict_right_mono)
   11.82 -    apply (simp add: k_def zero_less_dist_iff \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
   11.83 -    apply (simp add: zero_less_dist_iff \<open>x \<noteq> y\<close>)
   11.84 +    apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
   11.85 +    apply (simp add: \<open>x \<noteq> y\<close>)
   11.86      done
   11.87    then have "z \<in> ball x (dist x y)"
   11.88      by simp
   11.89 @@ -3055,14 +3059,14 @@
   11.90    shows "interior (cball x e) = ball x e"
   11.91  proof (cases "e \<ge> 0")
   11.92    case False note cs = this
   11.93 -  from cs have "ball x e = {}"
   11.94 +  from cs have null: "ball x e = {}"
   11.95      using ball_empty[of e x] by auto
   11.96    moreover
   11.97    {
   11.98      fix y
   11.99      assume "y \<in> cball x e"
  11.100      then have False
  11.101 -      unfolding mem_cball using dist_nz[of x y] cs by auto
  11.102 +      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)
  11.103    }
  11.104    then have "cball x e = {}" by auto
  11.105    then have "interior (cball x e) = {}"
  11.106 @@ -3088,9 +3092,7 @@
  11.107      then have "y \<in> ball x e"
  11.108      proof (cases "x = y")
  11.109        case True
  11.110 -      then have "e > 0"
  11.111 -        using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball]
  11.112 -        by (auto simp add: dist_commute)
  11.113 +      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
  11.114        then show "y \<in> ball x e"
  11.115          using \<open>x = y \<close> by simp
  11.116      next
  11.117 @@ -5165,7 +5167,6 @@
  11.118        assume "y \<in> f ` (ball x d \<inter> s)"
  11.119        then have "y \<in> ball (f x) e"
  11.120          using d(2)
  11.121 -        unfolding dist_nz[symmetric]
  11.122          apply (auto simp add: dist_commute)
  11.123          apply (erule_tac x=xa in ballE)
  11.124          apply auto
  11.125 @@ -5200,9 +5201,7 @@
  11.126      apply (rule_tac x=d in exI)
  11.127      apply auto
  11.128      apply (erule_tac x=xa in allE)
  11.129 -    apply (auto simp add: dist_commute dist_nz)
  11.130 -    unfolding dist_nz[symmetric]
  11.131 -    apply auto
  11.132 +    apply (auto simp add: dist_commute)
  11.133      done
  11.134  next
  11.135    assume ?rhs
  11.136 @@ -5214,7 +5213,7 @@
  11.137      apply (rule_tac x=d in exI)
  11.138      apply auto
  11.139      apply (erule_tac x="f xa" in allE)
  11.140 -    apply (auto simp add: dist_commute dist_nz)
  11.141 +    apply (auto simp add: dist_commute)
  11.142      done
  11.143  qed
  11.144  
  11.145 @@ -5285,14 +5284,14 @@
  11.146      fix T :: "'b set"
  11.147      assume "open T" and "f a \<in> T"
  11.148      with \<open>?lhs\<close> obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
  11.149 -      unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
  11.150 +      unfolding continuous_within tendsto_def eventually_at by auto
  11.151      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
  11.152        using x(2) \<open>d>0\<close> by simp
  11.153      then have "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
  11.154      proof eventually_elim
  11.155        case (elim n)
  11.156        then show ?case
  11.157 -        using d x(1) \<open>f a \<in> T\<close> unfolding dist_nz[symmetric] by auto
  11.158 +        using d x(1) \<open>f a \<in> T\<close> by auto
  11.159      qed
  11.160    }
  11.161    then show ?rhs
  11.162 @@ -5414,30 +5413,15 @@
  11.163  
  11.164  lemma continuous_transform_within:
  11.165    fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
  11.166 -  assumes "0 < d"
  11.167 +  assumes "continuous (at x within s) f"
  11.168 +    and "0 < d"
  11.169      and "x \<in> s"
  11.170 -    and "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
  11.171 -    and "continuous (at x within s) f"
  11.172 +    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
  11.173    shows "continuous (at x within s) g"
  11.174 +  using assms
  11.175    unfolding continuous_within
  11.176 -proof (rule Lim_transform_within)
  11.177 -  show "0 < d" by fact
  11.178 -  show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
  11.179 -    using assms(3) by auto
  11.180 -  have "f x = g x"
  11.181 -    using assms(1,2,3) by auto
  11.182 -  then show "(f \<longlongrightarrow> g x) (at x within s)"
  11.183 -    using assms(4) unfolding continuous_within by simp
  11.184 -qed
  11.185 -
  11.186 -lemma continuous_transform_at:
  11.187 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
  11.188 -  assumes "0 < d"
  11.189 -    and "\<forall>x'. dist x' x < d --> f x' = g x'"
  11.190 -    and "continuous (at x) f"
  11.191 -  shows "continuous (at x) g"
  11.192 -  using continuous_transform_within [of d x UNIV f g] assms by simp
  11.193 -
  11.194 +  by (force simp add: intro: Lim_transform_within)
  11.195 + 
  11.196  
  11.197  subsubsection \<open>Structural rules for pointwise continuity\<close>
  11.198  
  11.199 @@ -5762,7 +5746,7 @@
  11.200      done
  11.201  qed
  11.202  
  11.203 -lemma isCont_indicator: 
  11.204 +lemma isCont_indicator:
  11.205    fixes x :: "'a::t2_space"
  11.206    shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
  11.207  proof auto
  11.208 @@ -6243,7 +6227,6 @@
  11.209    shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
  11.210    unfolding continuous_at
  11.211    unfolding Lim_at
  11.212 -  unfolding dist_nz[symmetric]
  11.213    unfolding dist_norm
  11.214    apply auto
  11.215    apply (erule_tac x=e in allE)
    12.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Wed Jan 06 16:17:50 2016 +0100
    12.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Thu Jan 07 17:40:55 2016 +0000
    12.3 @@ -126,7 +126,7 @@
    12.4      by (auto simp: isCont_def sinc_at_0)
    12.5  next
    12.6    assume "x \<noteq> 0" show ?thesis
    12.7 -    by (rule continuous_transform_at [where d = "abs x" and f = "\<lambda>x. sin x / x"])
    12.8 +    by (rule continuous_transform_within [where d = "abs x" and f = "\<lambda>x. sin x / x"])
    12.9         (auto simp add: dist_real_def \<open>x \<noteq> 0\<close>)
   12.10  qed
   12.11  
    13.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jan 06 16:17:50 2016 +0100
    13.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jan 07 17:40:55 2016 +0000
    13.3 @@ -1056,6 +1056,8 @@
    13.4    shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    13.5  by (simp add: zero_less_dist_iff)
    13.6  
    13.7 +declare dist_nz [symmetric, simp]
    13.8 +
    13.9  lemma dist_triangle_le:
   13.10    shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
   13.11  by (rule order_trans [OF dist_triangle2])
   13.12 @@ -1673,7 +1675,7 @@
   13.13  lemma eventually_at:
   13.14    fixes a :: "'a :: metric_space"
   13.15    shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
   13.16 -  unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
   13.17 +  unfolding eventually_at_filter eventually_nhds_metric by auto
   13.18  
   13.19  lemma eventually_at_le:
   13.20    fixes a :: "'a::metric_space"
    14.1 --- a/src/HOL/Relation.thy	Wed Jan 06 16:17:50 2016 +0100
    14.2 +++ b/src/HOL/Relation.thy	Thu Jan 07 17:40:55 2016 +0000
    14.3 @@ -515,6 +515,8 @@
    14.4  lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
    14.5    by (simp add: total_on_def)
    14.6  
    14.7 +lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
    14.8 +  by force
    14.9  
   14.10  subsubsection \<open>Diagonal: identity over a set\<close>
   14.11  
   14.12 @@ -873,6 +875,12 @@
   14.13  lemma snd_eq_Range: "snd ` R = Range R"
   14.14    by force
   14.15  
   14.16 +lemma range_fst [simp]: "range fst = UNIV"
   14.17 +  by (auto simp: fst_eq_Domain)
   14.18 +
   14.19 +lemma range_snd [simp]: "range snd = UNIV"
   14.20 +  by (auto simp: snd_eq_Range)
   14.21 +
   14.22  lemma Domain_empty [simp]: "Domain {} = {}"
   14.23    by auto
   14.24  
    15.1 --- a/src/HOL/Series.thy	Wed Jan 06 16:17:50 2016 +0100
    15.2 +++ b/src/HOL/Series.thy	Thu Jan 07 17:40:55 2016 +0000
    15.3 @@ -30,6 +30,12 @@
    15.4  where
    15.5    "suminf f = (THE s. f sums s)"
    15.6  
    15.7 +lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
    15.8 +  apply (simp add: sums_def)
    15.9 +  apply (subst LIMSEQ_Suc_iff [symmetric])
   15.10 +  apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
   15.11 +  done
   15.12 +
   15.13  subsection \<open>Infinite summability on topological monoids\<close>
   15.14  
   15.15  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
   15.16 @@ -674,7 +680,7 @@
   15.17  
   15.18  text\<open>Relations among convergence and absolute convergence for power series.\<close>
   15.19  
   15.20 -lemma abel_lemma:
   15.21 +lemma Abel_lemma:
   15.22    fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
   15.23    assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
   15.24      shows "summable (\<lambda>n. norm (a n) * r^n)"
   15.25 @@ -792,10 +798,10 @@
   15.26    by (rule Cauchy_product_sums [THEN sums_unique])
   15.27  
   15.28  lemma summable_Cauchy_product:
   15.29 -  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))" 
   15.30 +  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
   15.31            "summable (\<lambda>k. norm (b k))"
   15.32    shows   "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
   15.33 -  using Cauchy_product_sums[OF assms] by (simp add: sums_iff)  
   15.34 +  using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
   15.35  
   15.36  subsection \<open>Series on @{typ real}s\<close>
   15.37  
    16.1 --- a/src/HOL/Set.thy	Wed Jan 06 16:17:50 2016 +0100
    16.2 +++ b/src/HOL/Set.thy	Thu Jan 07 17:40:55 2016 +0000
    16.3 @@ -846,7 +846,10 @@
    16.4  lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
    16.5    by blast
    16.6  
    16.7 -lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
    16.8 +lemma Diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
    16.9 +  by blast
   16.10 +
   16.11 +lemma subset_Diff_insert: "A \<subseteq> B - (insert x C) \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
   16.12    by blast
   16.13  
   16.14  lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"