src/HOL/Analysis/Inner_Product.thy
changeset 63971 da89140186e2
parent 63886 685fb01256af
child 64267 b9a1486e79be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Fri Sep 30 15:35:37 2016 +0200
     1.3 @@ -0,0 +1,402 @@
     1.4 +(*  Title:      HOL/Analysis/Inner_Product.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +section \<open>Inner Product Spaces and the Gradient Derivative\<close>
     1.9 +
    1.10 +theory Inner_Product
    1.11 +imports "~~/src/HOL/Complex_Main"
    1.12 +begin
    1.13 +
    1.14 +subsection \<open>Real inner product spaces\<close>
    1.15 +
    1.16 +text \<open>
    1.17 +  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
    1.18 +  @{term dist}, and @{term norm}.
    1.19 +\<close>
    1.20 +
    1.21 +setup \<open>Sign.add_const_constraint
    1.22 +  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
    1.23 +
    1.24 +setup \<open>Sign.add_const_constraint
    1.25 +  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    1.26 +
    1.27 +setup \<open>Sign.add_const_constraint
    1.28 +  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    1.29 +
    1.30 +setup \<open>Sign.add_const_constraint
    1.31 +  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    1.32 +
    1.33 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    1.34 +  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.35 +  assumes inner_commute: "inner x y = inner y x"
    1.36 +  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    1.37 +  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    1.38 +  and inner_ge_zero [simp]: "0 \<le> inner x x"
    1.39 +  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    1.40 +  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    1.41 +begin
    1.42 +
    1.43 +lemma inner_zero_left [simp]: "inner 0 x = 0"
    1.44 +  using inner_add_left [of 0 0 x] by simp
    1.45 +
    1.46 +lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    1.47 +  using inner_add_left [of x "- x" y] by simp
    1.48 +
    1.49 +lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    1.50 +  using inner_add_left [of x "- y" z] by simp
    1.51 +
    1.52 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    1.53 +  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    1.54 +
    1.55 +text \<open>Transfer distributivity rules to right argument.\<close>
    1.56 +
    1.57 +lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    1.58 +  using inner_add_left [of y z x] by (simp only: inner_commute)
    1.59 +
    1.60 +lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    1.61 +  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    1.62 +
    1.63 +lemma inner_zero_right [simp]: "inner x 0 = 0"
    1.64 +  using inner_zero_left [of x] by (simp only: inner_commute)
    1.65 +
    1.66 +lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    1.67 +  using inner_minus_left [of y x] by (simp only: inner_commute)
    1.68 +
    1.69 +lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    1.70 +  using inner_diff_left [of y z x] by (simp only: inner_commute)
    1.71 +
    1.72 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    1.73 +  using inner_setsum_left [of f A x] by (simp only: inner_commute)
    1.74 +
    1.75 +lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    1.76 +lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    1.77 +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    1.78 +
    1.79 +text \<open>Legacy theorem names\<close>
    1.80 +lemmas inner_left_distrib = inner_add_left
    1.81 +lemmas inner_right_distrib = inner_add_right
    1.82 +lemmas inner_distrib = inner_left_distrib inner_right_distrib
    1.83 +
    1.84 +lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    1.85 +  by (simp add: order_less_le)
    1.86 +
    1.87 +lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    1.88 +  by (simp add: norm_eq_sqrt_inner)
    1.89 +
    1.90 +text \<open>Identities involving real multiplication and division.\<close>
    1.91 +
    1.92 +lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    1.93 +  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    1.94 +
    1.95 +lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    1.96 +  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    1.97 +
    1.98 +lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    1.99 +  by (simp add: of_real_def)
   1.100 +
   1.101 +lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
   1.102 +  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
   1.103 +
   1.104 +lemma Cauchy_Schwarz_ineq:
   1.105 +  "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   1.106 +proof (cases)
   1.107 +  assume "y = 0"
   1.108 +  thus ?thesis by simp
   1.109 +next
   1.110 +  assume y: "y \<noteq> 0"
   1.111 +  let ?r = "inner x y / inner y y"
   1.112 +  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
   1.113 +    by (rule inner_ge_zero)
   1.114 +  also have "\<dots> = inner x x - inner y x * ?r"
   1.115 +    by (simp add: inner_diff)
   1.116 +  also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
   1.117 +    by (simp add: power2_eq_square inner_commute)
   1.118 +  finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
   1.119 +  hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   1.120 +    by (simp add: le_diff_eq)
   1.121 +  thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   1.122 +    by (simp add: pos_divide_le_eq y)
   1.123 +qed
   1.124 +
   1.125 +lemma Cauchy_Schwarz_ineq2:
   1.126 +  "\<bar>inner x y\<bar> \<le> norm x * norm y"
   1.127 +proof (rule power2_le_imp_le)
   1.128 +  have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   1.129 +    using Cauchy_Schwarz_ineq .
   1.130 +  thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   1.131 +    by (simp add: power_mult_distrib power2_norm_eq_inner)
   1.132 +  show "0 \<le> norm x * norm y"
   1.133 +    unfolding norm_eq_sqrt_inner
   1.134 +    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   1.135 +qed
   1.136 +
   1.137 +lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   1.138 +  using Cauchy_Schwarz_ineq2 [of x y] by auto
   1.139 +
   1.140 +subclass real_normed_vector
   1.141 +proof
   1.142 +  fix a :: real and x y :: 'a
   1.143 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   1.144 +    unfolding norm_eq_sqrt_inner by simp
   1.145 +  show "norm (x + y) \<le> norm x + norm y"
   1.146 +    proof (rule power2_le_imp_le)
   1.147 +      have "inner x y \<le> norm x * norm y"
   1.148 +        by (rule norm_cauchy_schwarz)
   1.149 +      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   1.150 +        unfolding power2_sum power2_norm_eq_inner
   1.151 +        by (simp add: inner_add inner_commute)
   1.152 +      show "0 \<le> norm x + norm y"
   1.153 +        unfolding norm_eq_sqrt_inner by simp
   1.154 +    qed
   1.155 +  have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   1.156 +    by (simp add: real_sqrt_mult_distrib)
   1.157 +  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   1.158 +    unfolding norm_eq_sqrt_inner
   1.159 +    by (simp add: power2_eq_square mult.assoc)
   1.160 +qed
   1.161 +
   1.162 +end
   1.163 +
   1.164 +lemma inner_divide_left:
   1.165 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
   1.166 +  shows "inner (a / of_real m) b = (inner a b) / m"
   1.167 +  by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
   1.168 +
   1.169 +lemma inner_divide_right:
   1.170 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
   1.171 +  shows "inner a (b / of_real m) = (inner a b) / m"
   1.172 +  by (metis inner_commute inner_divide_left)
   1.173 +
   1.174 +text \<open>
   1.175 +  Re-enable constraints for @{term "open"}, @{term "uniformity"},
   1.176 +  @{term dist}, and @{term norm}.
   1.177 +\<close>
   1.178 +
   1.179 +setup \<open>Sign.add_const_constraint
   1.180 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   1.181 +
   1.182 +setup \<open>Sign.add_const_constraint
   1.183 +  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
   1.184 +
   1.185 +setup \<open>Sign.add_const_constraint
   1.186 +  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   1.187 +
   1.188 +setup \<open>Sign.add_const_constraint
   1.189 +  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   1.190 +
   1.191 +lemma bounded_bilinear_inner:
   1.192 +  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   1.193 +proof
   1.194 +  fix x y z :: 'a and r :: real
   1.195 +  show "inner (x + y) z = inner x z + inner y z"
   1.196 +    by (rule inner_add_left)
   1.197 +  show "inner x (y + z) = inner x y + inner x z"
   1.198 +    by (rule inner_add_right)
   1.199 +  show "inner (scaleR r x) y = scaleR r (inner x y)"
   1.200 +    unfolding real_scaleR_def by (rule inner_scaleR_left)
   1.201 +  show "inner x (scaleR r y) = scaleR r (inner x y)"
   1.202 +    unfolding real_scaleR_def by (rule inner_scaleR_right)
   1.203 +  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   1.204 +  proof
   1.205 +    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   1.206 +      by (simp add: Cauchy_Schwarz_ineq2)
   1.207 +  qed
   1.208 +qed
   1.209 +
   1.210 +lemmas tendsto_inner [tendsto_intros] =
   1.211 +  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   1.212 +
   1.213 +lemmas isCont_inner [simp] =
   1.214 +  bounded_bilinear.isCont [OF bounded_bilinear_inner]
   1.215 +
   1.216 +lemmas has_derivative_inner [derivative_intros] =
   1.217 +  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   1.218 +
   1.219 +lemmas bounded_linear_inner_left =
   1.220 +  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   1.221 +
   1.222 +lemmas bounded_linear_inner_right =
   1.223 +  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   1.224 +
   1.225 +lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
   1.226 +
   1.227 +lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
   1.228 +
   1.229 +lemmas has_derivative_inner_right [derivative_intros] =
   1.230 +  bounded_linear.has_derivative [OF bounded_linear_inner_right]
   1.231 +
   1.232 +lemmas has_derivative_inner_left [derivative_intros] =
   1.233 +  bounded_linear.has_derivative [OF bounded_linear_inner_left]
   1.234 +
   1.235 +lemma differentiable_inner [simp]:
   1.236 +  "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
   1.237 +  unfolding differentiable_def by (blast intro: has_derivative_inner)
   1.238 +
   1.239 +
   1.240 +subsection \<open>Class instances\<close>
   1.241 +
   1.242 +instantiation real :: real_inner
   1.243 +begin
   1.244 +
   1.245 +definition inner_real_def [simp]: "inner = op *"
   1.246 +
   1.247 +instance
   1.248 +proof
   1.249 +  fix x y z r :: real
   1.250 +  show "inner x y = inner y x"
   1.251 +    unfolding inner_real_def by (rule mult.commute)
   1.252 +  show "inner (x + y) z = inner x z + inner y z"
   1.253 +    unfolding inner_real_def by (rule distrib_right)
   1.254 +  show "inner (scaleR r x) y = r * inner x y"
   1.255 +    unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   1.256 +  show "0 \<le> inner x x"
   1.257 +    unfolding inner_real_def by simp
   1.258 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   1.259 +    unfolding inner_real_def by simp
   1.260 +  show "norm x = sqrt (inner x x)"
   1.261 +    unfolding inner_real_def by simp
   1.262 +qed
   1.263 +
   1.264 +end
   1.265 +
   1.266 +lemma
   1.267 +  shows real_inner_1_left[simp]: "inner 1 x = x"
   1.268 +    and real_inner_1_right[simp]: "inner x 1 = x"
   1.269 +  by simp_all
   1.270 +
   1.271 +instantiation complex :: real_inner
   1.272 +begin
   1.273 +
   1.274 +definition inner_complex_def:
   1.275 +  "inner x y = Re x * Re y + Im x * Im y"
   1.276 +
   1.277 +instance
   1.278 +proof
   1.279 +  fix x y z :: complex and r :: real
   1.280 +  show "inner x y = inner y x"
   1.281 +    unfolding inner_complex_def by (simp add: mult.commute)
   1.282 +  show "inner (x + y) z = inner x z + inner y z"
   1.283 +    unfolding inner_complex_def by (simp add: distrib_right)
   1.284 +  show "inner (scaleR r x) y = r * inner x y"
   1.285 +    unfolding inner_complex_def by (simp add: distrib_left)
   1.286 +  show "0 \<le> inner x x"
   1.287 +    unfolding inner_complex_def by simp
   1.288 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   1.289 +    unfolding inner_complex_def
   1.290 +    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   1.291 +  show "norm x = sqrt (inner x x)"
   1.292 +    unfolding inner_complex_def complex_norm_def
   1.293 +    by (simp add: power2_eq_square)
   1.294 +qed
   1.295 +
   1.296 +end
   1.297 +
   1.298 +lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   1.299 +  unfolding inner_complex_def by simp
   1.300 +
   1.301 +lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   1.302 +  unfolding inner_complex_def by simp
   1.303 +
   1.304 +lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
   1.305 +  unfolding inner_complex_def by simp
   1.306 +
   1.307 +lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
   1.308 +  unfolding inner_complex_def by simp
   1.309 +
   1.310 +
   1.311 +subsection \<open>Gradient derivative\<close>
   1.312 +
   1.313 +definition
   1.314 +  gderiv ::
   1.315 +    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   1.316 +          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   1.317 +where
   1.318 +  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   1.319 +
   1.320 +lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   1.321 +  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   1.322 +
   1.323 +lemma GDERIV_DERIV_compose:
   1.324 +    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   1.325 +     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   1.326 +  unfolding gderiv_def has_field_derivative_def
   1.327 +  apply (drule (1) has_derivative_compose)
   1.328 +  apply (simp add: ac_simps)
   1.329 +  done
   1.330 +
   1.331 +lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   1.332 +  by simp
   1.333 +
   1.334 +lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   1.335 +  by simp
   1.336 +
   1.337 +lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   1.338 +  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   1.339 +
   1.340 +lemma GDERIV_add:
   1.341 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   1.342 +     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   1.343 +  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   1.344 +
   1.345 +lemma GDERIV_minus:
   1.346 +    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   1.347 +  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   1.348 +
   1.349 +lemma GDERIV_diff:
   1.350 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   1.351 +     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   1.352 +  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   1.353 +
   1.354 +lemma GDERIV_scaleR:
   1.355 +    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   1.356 +     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   1.357 +      :> (scaleR (f x) dg + scaleR df (g x))"
   1.358 +  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   1.359 +  apply (rule has_derivative_subst)
   1.360 +  apply (erule (1) has_derivative_scaleR)
   1.361 +  apply (simp add: ac_simps)
   1.362 +  done
   1.363 +
   1.364 +lemma GDERIV_mult:
   1.365 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   1.366 +     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   1.367 +  unfolding gderiv_def
   1.368 +  apply (rule has_derivative_subst)
   1.369 +  apply (erule (1) has_derivative_mult)
   1.370 +  apply (simp add: inner_add ac_simps)
   1.371 +  done
   1.372 +
   1.373 +lemma GDERIV_inverse:
   1.374 +    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   1.375 +     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   1.376 +  apply (erule GDERIV_DERIV_compose)
   1.377 +  apply (erule DERIV_inverse [folded numeral_2_eq_2])
   1.378 +  done
   1.379 +
   1.380 +lemma GDERIV_norm:
   1.381 +  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   1.382 +proof -
   1.383 +  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   1.384 +    by (intro has_derivative_inner has_derivative_ident)
   1.385 +  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   1.386 +    by (simp add: fun_eq_iff inner_commute)
   1.387 +  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   1.388 +  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   1.389 +    by (rule DERIV_real_sqrt)
   1.390 +  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   1.391 +    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   1.392 +  show ?thesis
   1.393 +    unfolding norm_eq_sqrt_inner
   1.394 +    apply (rule GDERIV_subst [OF _ 4])
   1.395 +    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   1.396 +    apply (subst gderiv_def)
   1.397 +    apply (rule has_derivative_subst [OF _ 2])
   1.398 +    apply (rule 1)
   1.399 +    apply (rule 3)
   1.400 +    done
   1.401 +qed
   1.402 +
   1.403 +lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   1.404 +
   1.405 +end