Some new proofs. Tidying up, esp to remove "apply rule".
authorpaulson <lp15@cam.ac.uk>
Fri Mar 07 15:52:56 2014 +0000 (2014-03-07)
changeset 559706d123f0ae358
parent 55969 8820ddb8f9f4
child 55988 ffe88d72afae
Some new proofs. Tidying up, esp to remove "apply rule".
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Derivative.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 07 14:21:15 2014 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 07 15:52:56 2014 +0000
     1.3 @@ -790,7 +790,7 @@
     1.4  
     1.5  text {* Caratheodory formulation of derivative at a point *}
     1.6  
     1.7 -lemma CARAT_DERIV:
     1.8 +lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
     1.9    "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
    1.10        (is "?lhs = ?rhs")
    1.11  proof
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 07 14:21:15 2014 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 07 15:52:56 2014 +0000
     2.3 @@ -142,6 +142,48 @@
     2.4      by (simp add: bounded_linear_mult_right has_derivative_within)
     2.5  qed
     2.6  
     2.7 +subsubsection {*Caratheodory characterization*}
     2.8 +
     2.9 +lemma DERIV_within_iff:
    2.10 +  "(DERIV f a : s :> D) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
    2.11 +proof -
    2.12 +  have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
    2.13 +    by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
    2.14 +  show ?thesis
    2.15 +    apply (simp add: deriv_fderiv has_derivative_within bounded_linear_mult_left)
    2.16 +    apply (simp add: LIM_zero_iff [where l = D, symmetric])
    2.17 +    apply (simp add: Lim_within dist_norm)
    2.18 +    apply (simp add: nonzero_norm_divide [symmetric])
    2.19 +    apply (simp add: 1 diff_add_eq_diff_diff)
    2.20 +    done
    2.21 +qed
    2.22 +
    2.23 +lemma DERIV_caratheodory_within:
    2.24 +  "(DERIV f x : s :> l) \<longleftrightarrow> 
    2.25 +   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
    2.26 +      (is "?lhs = ?rhs")
    2.27 +proof
    2.28 +  assume der: "DERIV f x : s :> l"
    2.29 +  show ?rhs
    2.30 +  proof (intro exI conjI)
    2.31 +    let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
    2.32 +    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
    2.33 +    show "continuous (at x within s) ?g" using der
    2.34 +      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    2.35 +    show "?g x = l" by simp
    2.36 +  qed
    2.37 +next
    2.38 +  assume ?rhs
    2.39 +  then obtain g where
    2.40 +    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
    2.41 +  thus "(DERIV f x : s :> l)"
    2.42 +    by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    2.43 +qed
    2.44 +
    2.45 +lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*)
    2.46 +  "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
    2.47 +by (rule DERIV_caratheodory_within)
    2.48 +
    2.49  
    2.50  subsubsection {* Limit transformation for derivatives *}
    2.51  
    2.52 @@ -151,20 +193,10 @@
    2.53      and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
    2.54      and "(f has_derivative f') (at x within s)"
    2.55    shows "(g has_derivative f') (at x within s)"
    2.56 -  using assms(4)
    2.57 +  using assms
    2.58    unfolding has_derivative_within
    2.59 -  apply -
    2.60 -  apply (erule conjE)
    2.61 -  apply rule
    2.62 -  apply assumption
    2.63 -  apply (rule Lim_transform_within[OF assms(1)])
    2.64 -  defer
    2.65 -  apply assumption
    2.66 -  apply rule
    2.67 -  apply rule
    2.68 -  apply (drule assms(3)[rule_format])
    2.69 -  using assms(3)[rule_format, OF assms(2)]
    2.70 -  apply auto
    2.71 +  apply clarify
    2.72 +  apply (rule Lim_transform_within, auto)
    2.73    done
    2.74  
    2.75  lemma has_derivative_transform_at:
    2.76 @@ -181,20 +213,10 @@
    2.77      and "\<forall>y\<in>s. f y = g y"
    2.78      and "(f has_derivative f') (at x)"
    2.79    shows "(g has_derivative f') (at x)"
    2.80 -  using assms(4)
    2.81 +  using assms
    2.82    unfolding has_derivative_at
    2.83 -  apply -
    2.84 -  apply (erule conjE)
    2.85 -  apply rule
    2.86 -  apply assumption
    2.87 -  apply (rule Lim_transform_within_open[OF assms(1,2)])
    2.88 -  defer
    2.89 -  apply assumption
    2.90 -  apply rule
    2.91 -  apply rule
    2.92 -  apply (drule assms(3)[rule_format])
    2.93 -  using assms(3)[rule_format, OF assms(2)]
    2.94 -  apply auto
    2.95 +  apply clarify
    2.96 +  apply (rule Lim_transform_within_open[OF assms(1,2)], auto)
    2.97    done
    2.98  
    2.99  subsection {* Differentiability *}
   2.100 @@ -275,17 +297,11 @@
   2.101    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.102    shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f x) ---> 0) (at a within s)"
   2.103    unfolding Lim_within
   2.104 -  apply rule
   2.105 -  apply rule
   2.106 +  apply (auto simp: )
   2.107    apply (erule_tac x=e in allE)
   2.108 -  apply (erule impE)
   2.109 -  apply assumption
   2.110 -  apply (erule exE)
   2.111 -  apply (erule conjE)
   2.112 +  apply (auto simp: )
   2.113    apply (rule_tac x="min d 1" in exI)
   2.114 -  apply rule
   2.115 -  defer
   2.116 -  apply rule
   2.117 +  apply (auto simp: )
   2.118    apply (erule_tac x=x in ballE)
   2.119    unfolding dist_norm diff_0_right
   2.120    apply (auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
   2.121 @@ -334,24 +350,12 @@
   2.122  proof
   2.123    assume ?lhs
   2.124    then show ?rhs
   2.125 -    unfolding has_derivative_within
   2.126 -    apply -
   2.127 -    apply (erule conjE)
   2.128 -    apply rule
   2.129 -    apply assumption
   2.130 -    unfolding Lim_within
   2.131 -    apply rule
   2.132 +    unfolding has_derivative_within Lim_within
   2.133 +    apply clarify
   2.134      apply (erule_tac x=e in allE)
   2.135 -    apply rule
   2.136 -    apply (erule impE)
   2.137 -    apply assumption
   2.138 -    apply (erule exE)
   2.139 +    apply safe
   2.140      apply (rule_tac x=d in exI)
   2.141 -    apply (erule conjE)
   2.142 -    apply rule
   2.143 -    apply assumption
   2.144 -    apply rule
   2.145 -    apply rule
   2.146 +    apply clarify
   2.147    proof-
   2.148      fix x y e d
   2.149      assume as:
   2.150 @@ -384,39 +388,14 @@
   2.151  next
   2.152    assume ?rhs
   2.153    then show ?lhs
   2.154 -    unfolding has_derivative_within Lim_within
   2.155 -    apply -
   2.156 -    apply (erule conjE)
   2.157 -    apply rule
   2.158 -    apply assumption
   2.159 -    apply rule
   2.160 -    apply (erule_tac x="e/2" in allE)
   2.161 -    apply rule
   2.162 -    apply (erule impE)
   2.163 -    defer
   2.164 -    apply (erule exE)
   2.165 -    apply (rule_tac x=d in exI)
   2.166 -    apply (erule conjE)
   2.167 -    apply rule
   2.168 -    apply assumption
   2.169 -    apply rule
   2.170 -    apply rule
   2.171 +    apply (auto simp: has_derivative_within Lim_within)
   2.172 +    apply (erule_tac x="e/2" in allE, auto)
   2.173 +    apply (rule_tac x=d in exI, auto)
   2.174      unfolding dist_norm diff_0_right norm_scaleR
   2.175 -    apply (erule_tac x=xa in ballE)
   2.176 -    apply (erule impE)
   2.177 -  proof -
   2.178 -    fix e d y
   2.179 -    assume "bounded_linear f'"
   2.180 -      and "0 < e"
   2.181 -      and "0 < d"
   2.182 -      and "y \<in> s"
   2.183 -      and "0 < norm (y - x) \<and> norm (y - x) < d"
   2.184 -      and "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
   2.185 -    then show "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e"
   2.186 -      apply (rule_tac le_less_trans[of _ "e/2"])
   2.187 -      apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps)
   2.188 -      done
   2.189 -  qed auto
   2.190 +    apply (erule_tac x=xa in ballE, auto)
   2.191 +    apply (rule_tac y="e/2" in le_less_trans)
   2.192 +    apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps)
   2.193 +    done
   2.194  qed
   2.195  
   2.196  lemma has_derivative_at_alt:
   2.197 @@ -488,11 +467,8 @@
   2.198        done
   2.199    qed
   2.200    then have *: "netlimit (at x within s) = x"
   2.201 -    apply -
   2.202 -    apply (rule netlimit_within)
   2.203 -    unfolding trivial_limit_within
   2.204 -    apply simp
   2.205 -    done
   2.206 +    apply (auto intro!: netlimit_within)
   2.207 +    by (metis trivial_limit_within)
   2.208    show ?thesis
   2.209      apply (rule linear_eq_stdbasis)
   2.210      unfolding linear_conv_bounded_linear
   2.211 @@ -621,13 +597,8 @@
   2.212      and "x \<in> {a..b}"
   2.213      and "(f has_derivative f') (at x within {a..b})"
   2.214    shows "frechet_derivative f (at x within {a..b}) = f'"
   2.215 -  apply (rule frechet_derivative_unique_within_closed_interval[where f=f])
   2.216 -  apply (rule assms(1,2))+
   2.217 -  unfolding frechet_derivative_works[symmetric]
   2.218 -  unfolding differentiable_def
   2.219 -  using assms(3)
   2.220 -  apply auto
   2.221 -  done
   2.222 +  using assms
   2.223 +  by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
   2.224  
   2.225  
   2.226  subsection {* The traditional Rolle theorem in one dimension *}
   2.227 @@ -778,12 +749,7 @@
   2.228      proof (cases "d \<in> box a b \<or> c \<in> box a b")
   2.229        case True
   2.230        then show ?thesis
   2.231 -        apply (erule_tac disjE)
   2.232 -        apply (rule_tac x=d in bexI)
   2.233 -        apply (rule_tac[3] x=c in bexI)
   2.234 -        using d c
   2.235 -        apply (auto simp: box_real)
   2.236 -        done
   2.237 +        by (metis c(2) d(2) interval_open_subset_closed subset_iff)
   2.238      next
   2.239        def e \<equiv> "(a + b) /2"
   2.240        case False
   2.241 @@ -791,10 +757,7 @@
   2.242          using d c assms(2) by (auto simp: box_real)
   2.243        then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
   2.244          using c d
   2.245 -        apply -
   2.246 -        apply (erule_tac x=x in ballE)+
   2.247 -        apply auto
   2.248 -        done
   2.249 +        by force
   2.250        then show ?thesis
   2.251          apply (rule_tac x=e in bexI)
   2.252          unfolding e_def
   2.253 @@ -806,23 +769,11 @@
   2.254    then obtain x where x: "x \<in> box a b" "(\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)" ..
   2.255    then have "f' x = (\<lambda>v. 0)"
   2.256      apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
   2.257 -    defer
   2.258 -    apply (rule open_interval)
   2.259 -    apply (rule assms(4)[unfolded has_derivative_at[symmetric],THEN bspec[where x=x]])
   2.260 -    apply assumption
   2.261 -    unfolding o_def
   2.262 -    apply (erule disjE)
   2.263 -    apply (rule disjI2)
   2.264 +    using assms
   2.265      apply auto
   2.266      done
   2.267    then show ?thesis
   2.268 -    apply (rule_tac x=x in bexI)
   2.269 -    unfolding o_def
   2.270 -    apply rule
   2.271 -    apply (drule_tac x=v in fun_cong)
   2.272 -    using x(1)
   2.273 -    apply auto
   2.274 -    done
   2.275 +    by (metis x(1))
   2.276  qed
   2.277  
   2.278  
   2.279 @@ -847,10 +798,7 @@
   2.280      "x \<in> box a b"
   2.281      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
   2.282    then show ?thesis
   2.283 -    apply (rule_tac x=x in bexI)
   2.284 -    apply (drule fun_cong[of _ _ "b - a"])
   2.285 -    apply (auto simp: box_real)
   2.286 -    done
   2.287 +    by (metis (erased, hide_lams) assms(1) box_real diff_less_iff(1) eq_iff_diff_eq_0 linordered_field_class.sign_simps(41) nonzero_mult_divide_cancel_right not_real_square_gt_zero times_divide_eq_left)
   2.288  qed
   2.289  
   2.290  lemma mvt_simple:
   2.291 @@ -1196,11 +1144,7 @@
   2.292    proof -
   2.293      case goal1
   2.294      then have *: "e / B >0"
   2.295 -      apply -
   2.296 -      apply (rule divide_pos_pos)
   2.297 -      using `B > 0`
   2.298 -      apply auto
   2.299 -      done
   2.300 +      by (metis `0 < B` divide_pos_pos)
   2.301      obtain d' where d':
   2.302          "0 < d'"
   2.303          "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
   2.304 @@ -1209,10 +1153,7 @@
   2.305        using real_lbound_gt_zero[OF d(1) d'(1)] by blast
   2.306      show ?case
   2.307        apply (rule_tac x=k in exI)
   2.308 -      apply rule
   2.309 -      defer
   2.310 -      apply rule
   2.311 -      apply rule
   2.312 +      apply auto
   2.313      proof -
   2.314        fix z
   2.315        assume as: "norm (z - y) < k"
   2.316 @@ -1296,9 +1237,7 @@
   2.317      apply (rule continuous_on_interior[OF _ assms(3)])
   2.318      apply (rule continuous_on_inv[OF assms(4,1)])
   2.319      apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
   2.320 -    apply rule
   2.321 -    apply (rule *)
   2.322 -    apply assumption
   2.323 +    apply (metis *)
   2.324      done
   2.325  qed
   2.326  
   2.327 @@ -1554,9 +1493,7 @@
   2.328      using linear_inverse_left
   2.329      by auto
   2.330    moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
   2.331 -    apply rule
   2.332 -    apply rule
   2.333 -    apply rule
   2.334 +    apply clarify
   2.335      apply (rule sussmann_open_mapping)
   2.336      apply (rule assms ling)+
   2.337      apply auto
   2.338 @@ -1604,12 +1541,8 @@
   2.339      then show ?case
   2.340        using assms(4) by auto
   2.341    qed
   2.342 -  ultimately show ?thesis
   2.343 -    apply -
   2.344 -    apply (rule has_derivative_inverse_basic_x[OF assms(5)])
   2.345 -    using assms
   2.346 -    apply auto
   2.347 -    done
   2.348 +  ultimately show ?thesis using assms
   2.349 +    by (metis has_derivative_inverse_basic_x open_interior)
   2.350  qed
   2.351  
   2.352  text {* A rewrite based on the other domain. *}
   2.353 @@ -2078,10 +2011,7 @@
   2.354    show ?thesis
   2.355      apply (rule *)
   2.356      apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
   2.357 -    apply rule
   2.358 -    apply rule
   2.359 -    apply (rule has_derivative_add_const, rule assms(2)[rule_format])
   2.360 -    apply assumption
   2.361 +    apply (metis assms(2) has_derivative_add_const)
   2.362      apply (rule `a \<in> s`)
   2.363      apply auto
   2.364      done
   2.365 @@ -2097,11 +2027,7 @@
   2.366    have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
   2.367      (f has_derivative (f' x)) (at x within s) \<and>
   2.368      (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
   2.369 -    apply rule
   2.370 -    using assms(2)
   2.371 -    apply (erule_tac x="inverse (real (Suc n))" in allE)
   2.372 -    apply auto
   2.373 -    done
   2.374 +    by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
   2.375    obtain f where
   2.376      *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' xa \<and>
   2.377        (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
   2.378 @@ -2157,11 +2083,7 @@
   2.379    shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g' x) (at x within s)"
   2.380    unfolding sums_seq_def
   2.381    apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
   2.382 -  apply rule
   2.383 -  apply rule
   2.384 -  apply (rule has_derivative_setsum)
   2.385 -  apply (rule assms(2)[rule_format])
   2.386 -  apply assumption
   2.387 +  apply (metis assms(2) has_derivative_setsum)
   2.388    using assms(4-5)
   2.389    unfolding sums_seq_def
   2.390    apply auto
   2.391 @@ -2296,10 +2218,9 @@
   2.392  lemma has_vector_derivative_cmul_eq:
   2.393    assumes "c \<noteq> 0"
   2.394    shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
   2.395 -  apply rule
   2.396 +  apply (rule iffI)
   2.397    apply (drule has_vector_derivative_cmul[where c="1/c"])
   2.398 -  defer
   2.399 -  apply (rule has_vector_derivative_cmul)
   2.400 +  apply (rule_tac [2] has_vector_derivative_cmul)
   2.401    using assms
   2.402    apply auto
   2.403    done