remove several redundant and unused theorems about derivatives
authorhuffman
Wed Aug 10 16:35:50 2011 -0700 (2011-08-10)
changeset 441402c10c35dd4be
parent 44139 abccf1b7ea4b
child 44141 0697c01ff3ea
remove several redundant and unused theorems about derivatives
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 15:56:48 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 16:35:50 2011 -0700
     1.3 @@ -1526,9 +1526,9 @@
     1.4  
     1.5  lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
     1.6    assumes "(c has_derivative c') net"
     1.7 -  shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net" 
     1.8 -  using has_derivative_vmul_component[OF assms] 
     1.9 -  unfolding nth_conv_component .
    1.10 +  shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net"
    1.11 +  unfolding nth_conv_component
    1.12 +  by (intro has_derivative_intros assms)
    1.13  
    1.14  lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
    1.15    unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
    1.16 @@ -1641,8 +1641,6 @@
    1.17  lemma vec1_component[simp]: "(vec1 x)$1 = x"
    1.18    by (simp_all add:  vec_eq_iff)
    1.19  
    1.20 -declare vec1_dest_vec1(1) [simp]
    1.21 -
    1.22  lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
    1.23    by (metis vec1_dest_vec1(1))
    1.24  
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Aug 10 15:56:48 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Aug 10 16:35:50 2011 -0700
     2.3 @@ -97,7 +97,7 @@
     2.4    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
     2.5      by (simp add: Lim_null[symmetric])
     2.6    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
     2.7 -    by (intro Lim_cong_within) (simp_all add: times_divide_eq field_simps)
     2.8 +    by (intro Lim_cong_within) (simp_all add: field_simps)
     2.9    finally show ?thesis
    2.10      by (simp add: mult.bounded_linear_right has_derivative_within)
    2.11  qed
    2.12 @@ -116,43 +116,34 @@
    2.13  
    2.14  subsubsection {* Combining theorems. *}
    2.15  
    2.16 -lemma (in bounded_linear) has_derivative: "(f has_derivative f) net"
    2.17 -  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
    2.18 -  unfolding diff by (simp add: tendsto_const)
    2.19 -
    2.20  lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
    2.21 -  apply(rule bounded_linear.has_derivative) using bounded_linear_ident[unfolded id_def] by simp
    2.22 +  unfolding has_derivative_def
    2.23 +  by (simp add: bounded_linear_ident tendsto_const)
    2.24  
    2.25  lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
    2.26    unfolding has_derivative_def
    2.27 -  by (rule, rule bounded_linear_zero, simp add: tendsto_const)
    2.28 +  by (simp add: bounded_linear_zero tendsto_const)
    2.29  
    2.30 -lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
    2.31 -proof -
    2.32 -  have "bounded_linear (\<lambda>x. c *\<^sub>R x)"
    2.33 -    by (rule scaleR.bounded_linear_right)
    2.34 -  moreover have "bounded_linear f" ..
    2.35 -  ultimately show ?thesis
    2.36 -    by (rule bounded_linear_compose)
    2.37 -qed
    2.38 +lemma (in bounded_linear) has_derivative': "(f has_derivative f) net"
    2.39 +  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
    2.40 +  unfolding diff by (simp add: tendsto_const)
    2.41 +
    2.42 +lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
    2.43  
    2.44 -lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
    2.45 -  unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
    2.46 -  using assms[unfolded has_derivative_def]
    2.47 -  using scaleR.tendsto[OF tendsto_const assms[unfolded has_derivative_def,THEN conjunct2]]
    2.48 -  unfolding scaleR_right_diff_distrib scaleR_right_distrib by auto 
    2.49 -
    2.50 -lemma has_derivative_cmul_eq: assumes "c \<noteq> 0" 
    2.51 -  shows "(((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net \<longleftrightarrow> (f has_derivative f') net)"
    2.52 -  apply(rule) defer apply(rule has_derivative_cmul,assumption) 
    2.53 -  apply(drule has_derivative_cmul[where c="1/c"]) using assms by auto
    2.54 +lemma (in bounded_linear) has_derivative:
    2.55 +  assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
    2.56 +  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
    2.57 +  using assms unfolding has_derivative_def
    2.58 +  apply safe
    2.59 +  apply (erule bounded_linear_compose [OF local.bounded_linear])
    2.60 +  apply (drule local.tendsto)
    2.61 +  apply (simp add: local.scaleR local.diff local.add local.zero)
    2.62 +  done
    2.63  
    2.64  lemma has_derivative_neg:
    2.65 - "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
    2.66 -  apply(drule has_derivative_cmul[where c="-1"]) by auto
    2.67 -
    2.68 -lemma has_derivative_neg_eq: "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net \<longleftrightarrow> (f has_derivative f') net"
    2.69 -  apply(rule, drule_tac[!] has_derivative_neg) by auto
    2.70 +  assumes "(f has_derivative f') net"
    2.71 +  shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
    2.72 +  using scaleR_right.has_derivative [where r="-1", OF assms] by auto
    2.73  
    2.74  lemma has_derivative_add:
    2.75    assumes "(f has_derivative f') net" and "(g has_derivative g') net"
    2.76 @@ -161,11 +152,12 @@
    2.77    note as = assms[unfolded has_derivative_def]
    2.78    show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
    2.79      using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
    2.80 -    by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib)
    2.81 +    by (auto simp add: algebra_simps)
    2.82  qed
    2.83  
    2.84 -lemma has_derivative_add_const:"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
    2.85 -  apply(drule has_derivative_add) apply(rule has_derivative_const) by auto
    2.86 +lemma has_derivative_add_const:
    2.87 +  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
    2.88 +  by (drule has_derivative_add, rule has_derivative_const, auto)
    2.89  
    2.90  lemma has_derivative_sub:
    2.91    assumes "(f has_derivative f') net" and "(g has_derivative g') net"
    2.92 @@ -176,82 +168,22 @@
    2.93    assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
    2.94    shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
    2.95    using assms by (induct, simp_all add: has_derivative_const has_derivative_add)
    2.96 -
    2.97 -lemma has_derivative_setsum_numseg:
    2.98 -  "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> ((f i) has_derivative (f' i)) net \<Longrightarrow>
    2.99 -  ((\<lambda>x. setsum (\<lambda>i. f i x) {m..n::nat}) has_derivative (\<lambda>h. setsum (\<lambda>i. f' i h) {m..n})) net"
   2.100 -  by (rule has_derivative_setsum) simp_all
   2.101 -
   2.102  text {* Somewhat different results for derivative of scalar multiplier. *}
   2.103  
   2.104  (** move **)
   2.105 -lemma linear_vmul_component:
   2.106 +lemma linear_vmul_component: (* TODO: delete *)
   2.107    assumes lf: "linear f"
   2.108    shows "linear (\<lambda>x. f x $$ k *\<^sub>R v)"
   2.109    using lf
   2.110    by (auto simp add: linear_def algebra_simps)
   2.111  
   2.112 -lemma bounded_linear_euclidean_component: "bounded_linear (\<lambda>x. x $$ k)"
   2.113 -  unfolding euclidean_component_def
   2.114 -  by (rule inner.bounded_linear_right)
   2.115 -
   2.116 -lemma has_derivative_vmul_component:
   2.117 -  fixes c::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" and v::"'c::real_normed_vector"
   2.118 -  assumes "(c has_derivative c') net"
   2.119 -  shows "((\<lambda>x. c(x)$$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$$k *\<^sub>R v)) net" proof-
   2.120 -  have *:"\<And>y. (c y $$ k *\<^sub>R v - (c (netlimit net) $$ k *\<^sub>R v + c' (y - netlimit net) $$ k *\<^sub>R v)) = 
   2.121 -        (c y $$ k - (c (netlimit net) $$ k + c' (y - netlimit net) $$ k)) *\<^sub>R v" 
   2.122 -    unfolding scaleR_left_diff_distrib scaleR_left_distrib by auto
   2.123 -  show ?thesis unfolding has_derivative_def and *
   2.124 -    apply (rule conjI)
   2.125 -    apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
   2.126 -    apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
   2.127 -    apply (rule derivative_linear [OF assms])
   2.128 -    apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR
   2.129 -    apply (intro tendsto_intros)
   2.130 -    using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
   2.131 -    apply(rule,assumption,rule disjI2,rule,rule) proof-
   2.132 -    have *:"\<And>x. x - 0 = (x::'a)" by auto 
   2.133 -    have **:"\<And>d x. d * (c x $$ k - (c (netlimit net) $$ k + c' (x - netlimit net) $$ k)) =
   2.134 -      (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) $$k" by(auto simp add:field_simps)
   2.135 -    fix e assume "\<not> trivial_limit net" "0 < (e::real)"
   2.136 -    then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R
   2.137 -      (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
   2.138 -      using assms[unfolded has_derivative_def Lim] by auto
   2.139 -    thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) *
   2.140 -      (c x $$ k - (c (netlimit net) $$ k + c' (x - netlimit net) $$ k))) 0 < e) net"
   2.141 -      proof (rule eventually_elim1)
   2.142 -      case goal1 thus ?case apply - unfolding dist_norm  apply(rule le_less_trans)
   2.143 -        prefer 2 apply assumption unfolding * **
   2.144 -        using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R
   2.145 -          (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
   2.146 -    qed
   2.147 -  qed
   2.148 -qed
   2.149 -
   2.150 -lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real"
   2.151 -  assumes "(c has_derivative c') (at x within s)"
   2.152 -  shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x within s)"
   2.153 -  using has_derivative_vmul_component[OF assms, of 0 v] by auto
   2.154 -
   2.155 -lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real"
   2.156 -  assumes "(c has_derivative c') (at x)"
   2.157 -  shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x)"
   2.158 -  using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV)
   2.159 -
   2.160 -lemma has_derivative_lift_dot:
   2.161 -  assumes "(f has_derivative f') net"
   2.162 -  shows "((\<lambda>x. inner v (f x)) has_derivative (\<lambda>t. inner v (f' t))) net" proof-
   2.163 -  show ?thesis using assms unfolding has_derivative_def apply- apply(erule conjE,rule)
   2.164 -    apply(rule bounded_linear_compose[of _ f']) apply(rule inner.bounded_linear_right,assumption)
   2.165 -    apply(drule Lim_inner[where a=v]) unfolding o_def
   2.166 -    by(auto simp add:inner.scaleR_right inner.add_right inner.diff_right) qed
   2.167 -
   2.168  lemmas has_derivative_intros =
   2.169 -  has_derivative_sub has_derivative_add has_derivative_cmul has_derivative_id
   2.170 -  has_derivative_const has_derivative_neg has_derivative_vmul_component
   2.171 -  has_derivative_vmul_at has_derivative_vmul_within has_derivative_cmul 
   2.172 -  bounded_linear.has_derivative has_derivative_lift_dot
   2.173 +  has_derivative_id has_derivative_const
   2.174 +  has_derivative_add has_derivative_sub has_derivative_neg
   2.175 +  has_derivative_add_const
   2.176 +  scaleR_left.has_derivative scaleR_right.has_derivative
   2.177 +  inner_left.has_derivative inner_right.has_derivative
   2.178 +  euclidean_component.has_derivative
   2.179  
   2.180  subsubsection {* Limit transformation for derivatives *}
   2.181  
   2.182 @@ -359,7 +291,7 @@
   2.183      apply (erule_tac x=e in allE)
   2.184      apply (erule impE | assumption)+
   2.185      apply (erule exE, rule_tac x=d in exI)
   2.186 -    by (auto simp add: zero * elim!: allE)
   2.187 +    by (auto simp add: zero *)
   2.188  qed
   2.189  
   2.190  lemma differentiable_imp_continuous_at:
   2.191 @@ -527,7 +459,7 @@
   2.192    "f differentiable net \<Longrightarrow>
   2.193    (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
   2.194    unfolding differentiable_def
   2.195 -  apply(erule exE, drule has_derivative_cmul) by auto
   2.196 +  apply(erule exE, drule scaleR_right.has_derivative) by auto
   2.197  
   2.198  lemma differentiable_neg [intro]:
   2.199    "f differentiable net \<Longrightarrow>
   2.200 @@ -836,8 +768,8 @@
   2.201    proof
   2.202      fix x assume x:"x \<in> {a<..<b}"
   2.203      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
   2.204 -      by(rule has_derivative_intros assms(3)[rule_format,OF x]
   2.205 -        has_derivative_cmul[where 'b=real, unfolded real_scaleR_def])+
   2.206 +      by (intro has_derivative_intros assms(3)[rule_format,OF x]
   2.207 +        mult_right.has_derivative)
   2.208    qed(insert assms(1), auto simp add:field_simps)
   2.209    then guess x ..
   2.210    thus ?thesis apply(rule_tac x=x in bexI)
   2.211 @@ -882,7 +814,7 @@
   2.212    have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
   2.213      apply(rule mvt) apply(rule assms(1))
   2.214      apply(rule continuous_on_inner continuous_on_intros assms(2))+
   2.215 -    unfolding o_def apply(rule,rule has_derivative_lift_dot)
   2.216 +    unfolding o_def apply(rule,rule has_derivative_intros)
   2.217      using assms(3) by auto
   2.218    then guess x .. note x=this
   2.219    show ?thesis proof(cases "f a = f b")
   2.220 @@ -1361,12 +1293,12 @@
   2.221            unfolding o_def and diff using f'g' by auto
   2.222          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
   2.223            unfolding ph' * apply(rule diff_chain_within) defer
   2.224 -          apply(rule bounded_linear.has_derivative[OF assms(3)])
   2.225 +          apply(rule bounded_linear.has_derivative'[OF assms(3)])
   2.226            apply(rule has_derivative_intros) defer
   2.227            apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
   2.228            apply(rule has_derivative_at_within)
   2.229            using assms(5) and `u\<in>s` `a\<in>s`
   2.230 -          by(auto intro!: has_derivative_intros derivative_linear)
   2.231 +          by(auto intro!: has_derivative_intros bounded_linear.has_derivative' derivative_linear)
   2.232          have **:"bounded_linear (\<lambda>x. f' u x - f' a x)"
   2.233            "bounded_linear (\<lambda>x. f' a x - f' u x)"
   2.234            apply(rule_tac[!] bounded_linear_sub)
   2.235 @@ -1807,7 +1739,8 @@
   2.236  
   2.237  lemma has_vector_derivative_cmul:
   2.238    "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
   2.239 -  unfolding has_vector_derivative_def apply(drule has_derivative_cmul)
   2.240 +  unfolding has_vector_derivative_def
   2.241 +  apply (drule scaleR_right.has_derivative)
   2.242    by (auto simp add: algebra_simps)
   2.243  
   2.244  lemma has_vector_derivative_cmul_eq:
     3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 15:56:48 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 16:35:50 2011 -0700
     3.3 @@ -3763,8 +3763,9 @@
     3.4        using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
     3.5      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
     3.6        apply(rule diff_chain_within) apply(rule has_derivative_add)
     3.7 -      unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
     3.8 -      apply(rule has_derivative_vmul_within,rule has_derivative_id)+ 
     3.9 +      unfolding scaleR_simps
    3.10 +      apply(intro has_derivative_intros)
    3.11 +      apply(intro has_derivative_intros)
    3.12        apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
    3.13        apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
    3.14      thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .