HOL-Analysis: move Product_Vector and Inner_Product from Library
authorhoelzl
Fri Sep 30 15:35:37 2016 +0200 (2016-09-30)
changeset 63971da89140186e2
parent 63970 3b6a3632e754
child 63972 c98d1dd7eba1
HOL-Analysis: move Product_Vector and Inner_Product from Library
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Library.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Mirabelle/ex/Ex.thy
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 30 15:35:32 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 30 15:35:37 2016 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  theory Convex_Euclidean_Space
     1.5  imports
     1.6    Topology_Euclidean_Space
     1.7 -  "~~/src/HOL/Library/Product_Vector"
     1.8    "~~/src/HOL/Library/Set_Algebras"
     1.9  begin
    1.10  
     2.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Fri Sep 30 15:35:32 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Sep 30 15:35:37 2016 +0200
     2.3 @@ -7,9 +7,7 @@
     2.4  
     2.5  theory Euclidean_Space
     2.6  imports
     2.7 -  L2_Norm
     2.8 -  "~~/src/HOL/Library/Inner_Product"
     2.9 -  "~~/src/HOL/Library/Product_Vector"
    2.10 +  L2_Norm Product_Vector
    2.11  begin
    2.12  
    2.13  subsection \<open>Type class of Euclidean spaces\<close>
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Fri Sep 30 15:35:37 2016 +0200
     3.3 @@ -0,0 +1,402 @@
     3.4 +(*  Title:      HOL/Analysis/Inner_Product.thy
     3.5 +    Author:     Brian Huffman
     3.6 +*)
     3.7 +
     3.8 +section \<open>Inner Product Spaces and the Gradient Derivative\<close>
     3.9 +
    3.10 +theory Inner_Product
    3.11 +imports "~~/src/HOL/Complex_Main"
    3.12 +begin
    3.13 +
    3.14 +subsection \<open>Real inner product spaces\<close>
    3.15 +
    3.16 +text \<open>
    3.17 +  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
    3.18 +  @{term dist}, and @{term norm}.
    3.19 +\<close>
    3.20 +
    3.21 +setup \<open>Sign.add_const_constraint
    3.22 +  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
    3.23 +
    3.24 +setup \<open>Sign.add_const_constraint
    3.25 +  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    3.26 +
    3.27 +setup \<open>Sign.add_const_constraint
    3.28 +  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    3.29 +
    3.30 +setup \<open>Sign.add_const_constraint
    3.31 +  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    3.32 +
    3.33 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    3.34 +  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    3.35 +  assumes inner_commute: "inner x y = inner y x"
    3.36 +  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    3.37 +  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    3.38 +  and inner_ge_zero [simp]: "0 \<le> inner x x"
    3.39 +  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    3.40 +  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    3.41 +begin
    3.42 +
    3.43 +lemma inner_zero_left [simp]: "inner 0 x = 0"
    3.44 +  using inner_add_left [of 0 0 x] by simp
    3.45 +
    3.46 +lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    3.47 +  using inner_add_left [of x "- x" y] by simp
    3.48 +
    3.49 +lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    3.50 +  using inner_add_left [of x "- y" z] by simp
    3.51 +
    3.52 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    3.53 +  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    3.54 +
    3.55 +text \<open>Transfer distributivity rules to right argument.\<close>
    3.56 +
    3.57 +lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    3.58 +  using inner_add_left [of y z x] by (simp only: inner_commute)
    3.59 +
    3.60 +lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    3.61 +  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    3.62 +
    3.63 +lemma inner_zero_right [simp]: "inner x 0 = 0"
    3.64 +  using inner_zero_left [of x] by (simp only: inner_commute)
    3.65 +
    3.66 +lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    3.67 +  using inner_minus_left [of y x] by (simp only: inner_commute)
    3.68 +
    3.69 +lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    3.70 +  using inner_diff_left [of y z x] by (simp only: inner_commute)
    3.71 +
    3.72 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    3.73 +  using inner_setsum_left [of f A x] by (simp only: inner_commute)
    3.74 +
    3.75 +lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    3.76 +lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    3.77 +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    3.78 +
    3.79 +text \<open>Legacy theorem names\<close>
    3.80 +lemmas inner_left_distrib = inner_add_left
    3.81 +lemmas inner_right_distrib = inner_add_right
    3.82 +lemmas inner_distrib = inner_left_distrib inner_right_distrib
    3.83 +
    3.84 +lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    3.85 +  by (simp add: order_less_le)
    3.86 +
    3.87 +lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    3.88 +  by (simp add: norm_eq_sqrt_inner)
    3.89 +
    3.90 +text \<open>Identities involving real multiplication and division.\<close>
    3.91 +
    3.92 +lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    3.93 +  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    3.94 +
    3.95 +lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    3.96 +  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    3.97 +
    3.98 +lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    3.99 +  by (simp add: of_real_def)
   3.100 +
   3.101 +lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
   3.102 +  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
   3.103 +
   3.104 +lemma Cauchy_Schwarz_ineq:
   3.105 +  "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   3.106 +proof (cases)
   3.107 +  assume "y = 0"
   3.108 +  thus ?thesis by simp
   3.109 +next
   3.110 +  assume y: "y \<noteq> 0"
   3.111 +  let ?r = "inner x y / inner y y"
   3.112 +  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
   3.113 +    by (rule inner_ge_zero)
   3.114 +  also have "\<dots> = inner x x - inner y x * ?r"
   3.115 +    by (simp add: inner_diff)
   3.116 +  also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
   3.117 +    by (simp add: power2_eq_square inner_commute)
   3.118 +  finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
   3.119 +  hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   3.120 +    by (simp add: le_diff_eq)
   3.121 +  thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   3.122 +    by (simp add: pos_divide_le_eq y)
   3.123 +qed
   3.124 +
   3.125 +lemma Cauchy_Schwarz_ineq2:
   3.126 +  "\<bar>inner x y\<bar> \<le> norm x * norm y"
   3.127 +proof (rule power2_le_imp_le)
   3.128 +  have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   3.129 +    using Cauchy_Schwarz_ineq .
   3.130 +  thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   3.131 +    by (simp add: power_mult_distrib power2_norm_eq_inner)
   3.132 +  show "0 \<le> norm x * norm y"
   3.133 +    unfolding norm_eq_sqrt_inner
   3.134 +    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   3.135 +qed
   3.136 +
   3.137 +lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   3.138 +  using Cauchy_Schwarz_ineq2 [of x y] by auto
   3.139 +
   3.140 +subclass real_normed_vector
   3.141 +proof
   3.142 +  fix a :: real and x y :: 'a
   3.143 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   3.144 +    unfolding norm_eq_sqrt_inner by simp
   3.145 +  show "norm (x + y) \<le> norm x + norm y"
   3.146 +    proof (rule power2_le_imp_le)
   3.147 +      have "inner x y \<le> norm x * norm y"
   3.148 +        by (rule norm_cauchy_schwarz)
   3.149 +      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   3.150 +        unfolding power2_sum power2_norm_eq_inner
   3.151 +        by (simp add: inner_add inner_commute)
   3.152 +      show "0 \<le> norm x + norm y"
   3.153 +        unfolding norm_eq_sqrt_inner by simp
   3.154 +    qed
   3.155 +  have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   3.156 +    by (simp add: real_sqrt_mult_distrib)
   3.157 +  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   3.158 +    unfolding norm_eq_sqrt_inner
   3.159 +    by (simp add: power2_eq_square mult.assoc)
   3.160 +qed
   3.161 +
   3.162 +end
   3.163 +
   3.164 +lemma inner_divide_left:
   3.165 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
   3.166 +  shows "inner (a / of_real m) b = (inner a b) / m"
   3.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)
   3.168 +
   3.169 +lemma inner_divide_right:
   3.170 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
   3.171 +  shows "inner a (b / of_real m) = (inner a b) / m"
   3.172 +  by (metis inner_commute inner_divide_left)
   3.173 +
   3.174 +text \<open>
   3.175 +  Re-enable constraints for @{term "open"}, @{term "uniformity"},
   3.176 +  @{term dist}, and @{term norm}.
   3.177 +\<close>
   3.178 +
   3.179 +setup \<open>Sign.add_const_constraint
   3.180 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   3.181 +
   3.182 +setup \<open>Sign.add_const_constraint
   3.183 +  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
   3.184 +
   3.185 +setup \<open>Sign.add_const_constraint
   3.186 +  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   3.187 +
   3.188 +setup \<open>Sign.add_const_constraint
   3.189 +  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   3.190 +
   3.191 +lemma bounded_bilinear_inner:
   3.192 +  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   3.193 +proof
   3.194 +  fix x y z :: 'a and r :: real
   3.195 +  show "inner (x + y) z = inner x z + inner y z"
   3.196 +    by (rule inner_add_left)
   3.197 +  show "inner x (y + z) = inner x y + inner x z"
   3.198 +    by (rule inner_add_right)
   3.199 +  show "inner (scaleR r x) y = scaleR r (inner x y)"
   3.200 +    unfolding real_scaleR_def by (rule inner_scaleR_left)
   3.201 +  show "inner x (scaleR r y) = scaleR r (inner x y)"
   3.202 +    unfolding real_scaleR_def by (rule inner_scaleR_right)
   3.203 +  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   3.204 +  proof
   3.205 +    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   3.206 +      by (simp add: Cauchy_Schwarz_ineq2)
   3.207 +  qed
   3.208 +qed
   3.209 +
   3.210 +lemmas tendsto_inner [tendsto_intros] =
   3.211 +  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   3.212 +
   3.213 +lemmas isCont_inner [simp] =
   3.214 +  bounded_bilinear.isCont [OF bounded_bilinear_inner]
   3.215 +
   3.216 +lemmas has_derivative_inner [derivative_intros] =
   3.217 +  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   3.218 +
   3.219 +lemmas bounded_linear_inner_left =
   3.220 +  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   3.221 +
   3.222 +lemmas bounded_linear_inner_right =
   3.223 +  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   3.224 +
   3.225 +lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
   3.226 +
   3.227 +lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
   3.228 +
   3.229 +lemmas has_derivative_inner_right [derivative_intros] =
   3.230 +  bounded_linear.has_derivative [OF bounded_linear_inner_right]
   3.231 +
   3.232 +lemmas has_derivative_inner_left [derivative_intros] =
   3.233 +  bounded_linear.has_derivative [OF bounded_linear_inner_left]
   3.234 +
   3.235 +lemma differentiable_inner [simp]:
   3.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"
   3.237 +  unfolding differentiable_def by (blast intro: has_derivative_inner)
   3.238 +
   3.239 +
   3.240 +subsection \<open>Class instances\<close>
   3.241 +
   3.242 +instantiation real :: real_inner
   3.243 +begin
   3.244 +
   3.245 +definition inner_real_def [simp]: "inner = op *"
   3.246 +
   3.247 +instance
   3.248 +proof
   3.249 +  fix x y z r :: real
   3.250 +  show "inner x y = inner y x"
   3.251 +    unfolding inner_real_def by (rule mult.commute)
   3.252 +  show "inner (x + y) z = inner x z + inner y z"
   3.253 +    unfolding inner_real_def by (rule distrib_right)
   3.254 +  show "inner (scaleR r x) y = r * inner x y"
   3.255 +    unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   3.256 +  show "0 \<le> inner x x"
   3.257 +    unfolding inner_real_def by simp
   3.258 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   3.259 +    unfolding inner_real_def by simp
   3.260 +  show "norm x = sqrt (inner x x)"
   3.261 +    unfolding inner_real_def by simp
   3.262 +qed
   3.263 +
   3.264 +end
   3.265 +
   3.266 +lemma
   3.267 +  shows real_inner_1_left[simp]: "inner 1 x = x"
   3.268 +    and real_inner_1_right[simp]: "inner x 1 = x"
   3.269 +  by simp_all
   3.270 +
   3.271 +instantiation complex :: real_inner
   3.272 +begin
   3.273 +
   3.274 +definition inner_complex_def:
   3.275 +  "inner x y = Re x * Re y + Im x * Im y"
   3.276 +
   3.277 +instance
   3.278 +proof
   3.279 +  fix x y z :: complex and r :: real
   3.280 +  show "inner x y = inner y x"
   3.281 +    unfolding inner_complex_def by (simp add: mult.commute)
   3.282 +  show "inner (x + y) z = inner x z + inner y z"
   3.283 +    unfolding inner_complex_def by (simp add: distrib_right)
   3.284 +  show "inner (scaleR r x) y = r * inner x y"
   3.285 +    unfolding inner_complex_def by (simp add: distrib_left)
   3.286 +  show "0 \<le> inner x x"
   3.287 +    unfolding inner_complex_def by simp
   3.288 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   3.289 +    unfolding inner_complex_def
   3.290 +    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   3.291 +  show "norm x = sqrt (inner x x)"
   3.292 +    unfolding inner_complex_def complex_norm_def
   3.293 +    by (simp add: power2_eq_square)
   3.294 +qed
   3.295 +
   3.296 +end
   3.297 +
   3.298 +lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   3.299 +  unfolding inner_complex_def by simp
   3.300 +
   3.301 +lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   3.302 +  unfolding inner_complex_def by simp
   3.303 +
   3.304 +lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
   3.305 +  unfolding inner_complex_def by simp
   3.306 +
   3.307 +lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
   3.308 +  unfolding inner_complex_def by simp
   3.309 +
   3.310 +
   3.311 +subsection \<open>Gradient derivative\<close>
   3.312 +
   3.313 +definition
   3.314 +  gderiv ::
   3.315 +    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   3.316 +          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   3.317 +where
   3.318 +  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   3.319 +
   3.320 +lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   3.321 +  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   3.322 +
   3.323 +lemma GDERIV_DERIV_compose:
   3.324 +    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   3.325 +     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   3.326 +  unfolding gderiv_def has_field_derivative_def
   3.327 +  apply (drule (1) has_derivative_compose)
   3.328 +  apply (simp add: ac_simps)
   3.329 +  done
   3.330 +
   3.331 +lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   3.332 +  by simp
   3.333 +
   3.334 +lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   3.335 +  by simp
   3.336 +
   3.337 +lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   3.338 +  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   3.339 +
   3.340 +lemma GDERIV_add:
   3.341 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   3.342 +     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   3.343 +  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   3.344 +
   3.345 +lemma GDERIV_minus:
   3.346 +    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   3.347 +  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   3.348 +
   3.349 +lemma GDERIV_diff:
   3.350 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   3.351 +     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   3.352 +  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   3.353 +
   3.354 +lemma GDERIV_scaleR:
   3.355 +    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   3.356 +     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   3.357 +      :> (scaleR (f x) dg + scaleR df (g x))"
   3.358 +  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   3.359 +  apply (rule has_derivative_subst)
   3.360 +  apply (erule (1) has_derivative_scaleR)
   3.361 +  apply (simp add: ac_simps)
   3.362 +  done
   3.363 +
   3.364 +lemma GDERIV_mult:
   3.365 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   3.366 +     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   3.367 +  unfolding gderiv_def
   3.368 +  apply (rule has_derivative_subst)
   3.369 +  apply (erule (1) has_derivative_mult)
   3.370 +  apply (simp add: inner_add ac_simps)
   3.371 +  done
   3.372 +
   3.373 +lemma GDERIV_inverse:
   3.374 +    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   3.375 +     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   3.376 +  apply (erule GDERIV_DERIV_compose)
   3.377 +  apply (erule DERIV_inverse [folded numeral_2_eq_2])
   3.378 +  done
   3.379 +
   3.380 +lemma GDERIV_norm:
   3.381 +  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   3.382 +proof -
   3.383 +  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   3.384 +    by (intro has_derivative_inner has_derivative_ident)
   3.385 +  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   3.386 +    by (simp add: fun_eq_iff inner_commute)
   3.387 +  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   3.388 +  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   3.389 +    by (rule DERIV_real_sqrt)
   3.390 +  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   3.391 +    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   3.392 +  show ?thesis
   3.393 +    unfolding norm_eq_sqrt_inner
   3.394 +    apply (rule GDERIV_subst [OF _ 4])
   3.395 +    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   3.396 +    apply (subst gderiv_def)
   3.397 +    apply (rule has_derivative_subst [OF _ 2])
   3.398 +    apply (rule 1)
   3.399 +    apply (rule 3)
   3.400 +    done
   3.401 +qed
   3.402 +
   3.403 +lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   3.404 +
   3.405 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:37 2016 +0200
     4.3 @@ -0,0 +1,371 @@
     4.4 +(*  Title:      HOL/Analysis/Product_Vector.thy
     4.5 +    Author:     Brian Huffman
     4.6 +*)
     4.7 +
     4.8 +section \<open>Cartesian Products as Vector Spaces\<close>
     4.9 +
    4.10 +theory Product_Vector
    4.11 +imports
    4.12 +  Inner_Product
    4.13 +  "~~/src/HOL/Library/Product_plus"
    4.14 +begin
    4.15 +
    4.16 +subsection \<open>Product is a real vector space\<close>
    4.17 +
    4.18 +instantiation prod :: (real_vector, real_vector) real_vector
    4.19 +begin
    4.20 +
    4.21 +definition scaleR_prod_def:
    4.22 +  "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"
    4.23 +
    4.24 +lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)"
    4.25 +  unfolding scaleR_prod_def by simp
    4.26 +
    4.27 +lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)"
    4.28 +  unfolding scaleR_prod_def by simp
    4.29 +
    4.30 +lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
    4.31 +  unfolding scaleR_prod_def by simp
    4.32 +
    4.33 +instance
    4.34 +proof
    4.35 +  fix a b :: real and x y :: "'a \<times> 'b"
    4.36 +  show "scaleR a (x + y) = scaleR a x + scaleR a y"
    4.37 +    by (simp add: prod_eq_iff scaleR_right_distrib)
    4.38 +  show "scaleR (a + b) x = scaleR a x + scaleR b x"
    4.39 +    by (simp add: prod_eq_iff scaleR_left_distrib)
    4.40 +  show "scaleR a (scaleR b x) = scaleR (a * b) x"
    4.41 +    by (simp add: prod_eq_iff)
    4.42 +  show "scaleR 1 x = x"
    4.43 +    by (simp add: prod_eq_iff)
    4.44 +qed
    4.45 +
    4.46 +end
    4.47 +
    4.48 +subsection \<open>Product is a metric space\<close>
    4.49 +
    4.50 +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
    4.51 +
    4.52 +instantiation prod :: (metric_space, metric_space) dist
    4.53 +begin
    4.54 +
    4.55 +definition dist_prod_def[code del]:
    4.56 +  "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
    4.57 +
    4.58 +instance ..
    4.59 +end
    4.60 +
    4.61 +instantiation prod :: (metric_space, metric_space) uniformity_dist
    4.62 +begin
    4.63 +
    4.64 +definition [code del]:
    4.65 +  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
    4.66 +    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    4.67 +
    4.68 +instance
    4.69 +  by standard (rule uniformity_prod_def)
    4.70 +end
    4.71 +
    4.72 +declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
    4.73 +
    4.74 +instantiation prod :: (metric_space, metric_space) metric_space
    4.75 +begin
    4.76 +
    4.77 +lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
    4.78 +  unfolding dist_prod_def by simp
    4.79 +
    4.80 +lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
    4.81 +  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
    4.82 +
    4.83 +lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
    4.84 +  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
    4.85 +
    4.86 +instance
    4.87 +proof
    4.88 +  fix x y :: "'a \<times> 'b"
    4.89 +  show "dist x y = 0 \<longleftrightarrow> x = y"
    4.90 +    unfolding dist_prod_def prod_eq_iff by simp
    4.91 +next
    4.92 +  fix x y z :: "'a \<times> 'b"
    4.93 +  show "dist x y \<le> dist x z + dist y z"
    4.94 +    unfolding dist_prod_def
    4.95 +    by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
    4.96 +        real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
    4.97 +next
    4.98 +  fix S :: "('a \<times> 'b) set"
    4.99 +  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   4.100 +  proof
   4.101 +    assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   4.102 +    proof
   4.103 +      fix x assume "x \<in> S"
   4.104 +      obtain A B where "open A" "open B" "x \<in> A \<times> B" "A \<times> B \<subseteq> S"
   4.105 +        using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
   4.106 +      obtain r where r: "0 < r" "\<forall>y. dist y (fst x) < r \<longrightarrow> y \<in> A"
   4.107 +        using \<open>open A\<close> and \<open>x \<in> A \<times> B\<close> unfolding open_dist by auto
   4.108 +      obtain s where s: "0 < s" "\<forall>y. dist y (snd x) < s \<longrightarrow> y \<in> B"
   4.109 +        using \<open>open B\<close> and \<open>x \<in> A \<times> B\<close> unfolding open_dist by auto
   4.110 +      let ?e = "min r s"
   4.111 +      have "0 < ?e \<and> (\<forall>y. dist y x < ?e \<longrightarrow> y \<in> S)"
   4.112 +      proof (intro allI impI conjI)
   4.113 +        show "0 < min r s" by (simp add: r(1) s(1))
   4.114 +      next
   4.115 +        fix y assume "dist y x < min r s"
   4.116 +        hence "dist y x < r" and "dist y x < s"
   4.117 +          by simp_all
   4.118 +        hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s"
   4.119 +          by (auto intro: le_less_trans dist_fst_le dist_snd_le)
   4.120 +        hence "fst y \<in> A" and "snd y \<in> B"
   4.121 +          by (simp_all add: r(2) s(2))
   4.122 +        hence "y \<in> A \<times> B" by (induct y, simp)
   4.123 +        with \<open>A \<times> B \<subseteq> S\<close> show "y \<in> S" ..
   4.124 +      qed
   4.125 +      thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
   4.126 +    qed
   4.127 +  next
   4.128 +    assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
   4.129 +    proof (rule open_prod_intro)
   4.130 +      fix x assume "x \<in> S"
   4.131 +      then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   4.132 +        using * by fast
   4.133 +      define r where "r = e / sqrt 2"
   4.134 +      define s where "s = e / sqrt 2"
   4.135 +      from \<open>0 < e\<close> have "0 < r" and "0 < s"
   4.136 +        unfolding r_def s_def by simp_all
   4.137 +      from \<open>0 < e\<close> have "e = sqrt (r\<^sup>2 + s\<^sup>2)"
   4.138 +        unfolding r_def s_def by (simp add: power_divide)
   4.139 +      define A where "A = {y. dist (fst x) y < r}"
   4.140 +      define B where "B = {y. dist (snd x) y < s}"
   4.141 +      have "open A" and "open B"
   4.142 +        unfolding A_def B_def by (simp_all add: open_ball)
   4.143 +      moreover have "x \<in> A \<times> B"
   4.144 +        unfolding A_def B_def mem_Times_iff
   4.145 +        using \<open>0 < r\<close> and \<open>0 < s\<close> by simp
   4.146 +      moreover have "A \<times> B \<subseteq> S"
   4.147 +      proof (clarify)
   4.148 +        fix a b assume "a \<in> A" and "b \<in> B"
   4.149 +        hence "dist a (fst x) < r" and "dist b (snd x) < s"
   4.150 +          unfolding A_def B_def by (simp_all add: dist_commute)
   4.151 +        hence "dist (a, b) x < e"
   4.152 +          unfolding dist_prod_def \<open>e = sqrt (r\<^sup>2 + s\<^sup>2)\<close>
   4.153 +          by (simp add: add_strict_mono power_strict_mono)
   4.154 +        thus "(a, b) \<in> S"
   4.155 +          by (simp add: S)
   4.156 +      qed
   4.157 +      ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
   4.158 +    qed
   4.159 +  qed
   4.160 +  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   4.161 +    unfolding * eventually_uniformity_metric
   4.162 +    by (simp del: split_paired_All add: dist_prod_def dist_commute)
   4.163 +qed
   4.164 +
   4.165 +end
   4.166 +
   4.167 +declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
   4.168 +
   4.169 +lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
   4.170 +  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
   4.171 +
   4.172 +lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
   4.173 +  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
   4.174 +
   4.175 +lemma Cauchy_Pair:
   4.176 +  assumes "Cauchy X" and "Cauchy Y"
   4.177 +  shows "Cauchy (\<lambda>n. (X n, Y n))"
   4.178 +proof (rule metric_CauchyI)
   4.179 +  fix r :: real assume "0 < r"
   4.180 +  hence "0 < r / sqrt 2" (is "0 < ?s") by simp
   4.181 +  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
   4.182 +    using metric_CauchyD [OF \<open>Cauchy X\<close> \<open>0 < ?s\<close>] ..
   4.183 +  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
   4.184 +    using metric_CauchyD [OF \<open>Cauchy Y\<close> \<open>0 < ?s\<close>] ..
   4.185 +  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
   4.186 +    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
   4.187 +  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
   4.188 +qed
   4.189 +
   4.190 +subsection \<open>Product is a complete metric space\<close>
   4.191 +
   4.192 +instance prod :: (complete_space, complete_space) complete_space
   4.193 +proof
   4.194 +  fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   4.195 +  have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
   4.196 +    using Cauchy_fst [OF \<open>Cauchy X\<close>]
   4.197 +    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   4.198 +  have 2: "(\<lambda>n. snd (X n)) \<longlonglongrightarrow> lim (\<lambda>n. snd (X n))"
   4.199 +    using Cauchy_snd [OF \<open>Cauchy X\<close>]
   4.200 +    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   4.201 +  have "X \<longlonglongrightarrow> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
   4.202 +    using tendsto_Pair [OF 1 2] by simp
   4.203 +  then show "convergent X"
   4.204 +    by (rule convergentI)
   4.205 +qed
   4.206 +
   4.207 +subsection \<open>Product is a normed vector space\<close>
   4.208 +
   4.209 +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
   4.210 +begin
   4.211 +
   4.212 +definition norm_prod_def[code del]:
   4.213 +  "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)"
   4.214 +
   4.215 +definition sgn_prod_def:
   4.216 +  "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
   4.217 +
   4.218 +lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
   4.219 +  unfolding norm_prod_def by simp
   4.220 +
   4.221 +instance
   4.222 +proof
   4.223 +  fix r :: real and x y :: "'a \<times> 'b"
   4.224 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   4.225 +    unfolding norm_prod_def
   4.226 +    by (simp add: prod_eq_iff)
   4.227 +  show "norm (x + y) \<le> norm x + norm y"
   4.228 +    unfolding norm_prod_def
   4.229 +    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
   4.230 +    apply (simp add: add_mono power_mono norm_triangle_ineq)
   4.231 +    done
   4.232 +  show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
   4.233 +    unfolding norm_prod_def
   4.234 +    apply (simp add: power_mult_distrib)
   4.235 +    apply (simp add: distrib_left [symmetric])
   4.236 +    apply (simp add: real_sqrt_mult_distrib)
   4.237 +    done
   4.238 +  show "sgn x = scaleR (inverse (norm x)) x"
   4.239 +    by (rule sgn_prod_def)
   4.240 +  show "dist x y = norm (x - y)"
   4.241 +    unfolding dist_prod_def norm_prod_def
   4.242 +    by (simp add: dist_norm)
   4.243 +qed
   4.244 +
   4.245 +end
   4.246 +
   4.247 +declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
   4.248 +
   4.249 +instance prod :: (banach, banach) banach ..
   4.250 +
   4.251 +subsubsection \<open>Pair operations are linear\<close>
   4.252 +
   4.253 +lemma bounded_linear_fst: "bounded_linear fst"
   4.254 +  using fst_add fst_scaleR
   4.255 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   4.256 +
   4.257 +lemma bounded_linear_snd: "bounded_linear snd"
   4.258 +  using snd_add snd_scaleR
   4.259 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   4.260 +
   4.261 +lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose]
   4.262 +
   4.263 +lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose]
   4.264 +
   4.265 +lemma bounded_linear_Pair:
   4.266 +  assumes f: "bounded_linear f"
   4.267 +  assumes g: "bounded_linear g"
   4.268 +  shows "bounded_linear (\<lambda>x. (f x, g x))"
   4.269 +proof
   4.270 +  interpret f: bounded_linear f by fact
   4.271 +  interpret g: bounded_linear g by fact
   4.272 +  fix x y and r :: real
   4.273 +  show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)"
   4.274 +    by (simp add: f.add g.add)
   4.275 +  show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)"
   4.276 +    by (simp add: f.scaleR g.scaleR)
   4.277 +  obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf"
   4.278 +    using f.pos_bounded by fast
   4.279 +  obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
   4.280 +    using g.pos_bounded by fast
   4.281 +  have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
   4.282 +    apply (rule allI)
   4.283 +    apply (simp add: norm_Pair)
   4.284 +    apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
   4.285 +    apply (simp add: distrib_left)
   4.286 +    apply (rule add_mono [OF norm_f norm_g])
   4.287 +    done
   4.288 +  then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
   4.289 +qed
   4.290 +
   4.291 +subsubsection \<open>Frechet derivatives involving pairs\<close>
   4.292 +
   4.293 +lemma has_derivative_Pair [derivative_intros]:
   4.294 +  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   4.295 +  shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
   4.296 +proof (rule has_derivativeI_sandwich[of 1])
   4.297 +  show "bounded_linear (\<lambda>h. (f' h, g' h))"
   4.298 +    using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   4.299 +  let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
   4.300 +  let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
   4.301 +  let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
   4.302 +
   4.303 +  show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)"
   4.304 +    using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm)
   4.305 +
   4.306 +  fix y :: 'a assume "y \<noteq> x"
   4.307 +  show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
   4.308 +    unfolding add_divide_distrib [symmetric]
   4.309 +    by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
   4.310 +qed simp
   4.311 +
   4.312 +lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
   4.313 +lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
   4.314 +
   4.315 +lemma has_derivative_split [derivative_intros]:
   4.316 +  "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   4.317 +  unfolding split_beta' .
   4.318 +
   4.319 +subsection \<open>Product is an inner product space\<close>
   4.320 +
   4.321 +instantiation prod :: (real_inner, real_inner) real_inner
   4.322 +begin
   4.323 +
   4.324 +definition inner_prod_def:
   4.325 +  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
   4.326 +
   4.327 +lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
   4.328 +  unfolding inner_prod_def by simp
   4.329 +
   4.330 +instance
   4.331 +proof
   4.332 +  fix r :: real
   4.333 +  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
   4.334 +  show "inner x y = inner y x"
   4.335 +    unfolding inner_prod_def
   4.336 +    by (simp add: inner_commute)
   4.337 +  show "inner (x + y) z = inner x z + inner y z"
   4.338 +    unfolding inner_prod_def
   4.339 +    by (simp add: inner_add_left)
   4.340 +  show "inner (scaleR r x) y = r * inner x y"
   4.341 +    unfolding inner_prod_def
   4.342 +    by (simp add: distrib_left)
   4.343 +  show "0 \<le> inner x x"
   4.344 +    unfolding inner_prod_def
   4.345 +    by (intro add_nonneg_nonneg inner_ge_zero)
   4.346 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   4.347 +    unfolding inner_prod_def prod_eq_iff
   4.348 +    by (simp add: add_nonneg_eq_0_iff)
   4.349 +  show "norm x = sqrt (inner x x)"
   4.350 +    unfolding norm_prod_def inner_prod_def
   4.351 +    by (simp add: power2_norm_eq_inner)
   4.352 +qed
   4.353 +
   4.354 +end
   4.355 +
   4.356 +lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
   4.357 +    by (cases x, simp)+
   4.358 +
   4.359 +lemma
   4.360 +  fixes x :: "'a::real_normed_vector"
   4.361 +  shows norm_Pair1 [simp]: "norm (0,x) = norm x"
   4.362 +    and norm_Pair2 [simp]: "norm (x,0) = norm x"
   4.363 +by (auto simp: norm_Pair)
   4.364 +
   4.365 +lemma norm_commute: "norm (x,y) = norm (y,x)"
   4.366 +  by (simp add: norm_Pair)
   4.367 +
   4.368 +lemma norm_fst_le: "norm x \<le> norm (x,y)"
   4.369 +  by (metis dist_fst_le fst_conv fst_zero norm_conv_dist)
   4.370 +
   4.371 +lemma norm_snd_le: "norm y \<le> norm (x,y)"
   4.372 +  by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
   4.373 +
   4.374 +end
     5.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Sep 30 15:35:32 2016 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,402 +0,0 @@
     5.4 -(*  Title:      HOL/Library/Inner_Product.thy
     5.5 -    Author:     Brian Huffman
     5.6 -*)
     5.7 -
     5.8 -section \<open>Inner Product Spaces and the Gradient Derivative\<close>
     5.9 -
    5.10 -theory Inner_Product
    5.11 -imports "~~/src/HOL/Complex_Main"
    5.12 -begin
    5.13 -
    5.14 -subsection \<open>Real inner product spaces\<close>
    5.15 -
    5.16 -text \<open>
    5.17 -  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
    5.18 -  @{term dist}, and @{term norm}.
    5.19 -\<close>
    5.20 -
    5.21 -setup \<open>Sign.add_const_constraint
    5.22 -  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
    5.23 -
    5.24 -setup \<open>Sign.add_const_constraint
    5.25 -  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    5.26 -
    5.27 -setup \<open>Sign.add_const_constraint
    5.28 -  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    5.29 -
    5.30 -setup \<open>Sign.add_const_constraint
    5.31 -  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    5.32 -
    5.33 -class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    5.34 -  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    5.35 -  assumes inner_commute: "inner x y = inner y x"
    5.36 -  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    5.37 -  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    5.38 -  and inner_ge_zero [simp]: "0 \<le> inner x x"
    5.39 -  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    5.40 -  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    5.41 -begin
    5.42 -
    5.43 -lemma inner_zero_left [simp]: "inner 0 x = 0"
    5.44 -  using inner_add_left [of 0 0 x] by simp
    5.45 -
    5.46 -lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    5.47 -  using inner_add_left [of x "- x" y] by simp
    5.48 -
    5.49 -lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    5.50 -  using inner_add_left [of x "- y" z] by simp
    5.51 -
    5.52 -lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    5.53 -  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    5.54 -
    5.55 -text \<open>Transfer distributivity rules to right argument.\<close>
    5.56 -
    5.57 -lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    5.58 -  using inner_add_left [of y z x] by (simp only: inner_commute)
    5.59 -
    5.60 -lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    5.61 -  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    5.62 -
    5.63 -lemma inner_zero_right [simp]: "inner x 0 = 0"
    5.64 -  using inner_zero_left [of x] by (simp only: inner_commute)
    5.65 -
    5.66 -lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    5.67 -  using inner_minus_left [of y x] by (simp only: inner_commute)
    5.68 -
    5.69 -lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    5.70 -  using inner_diff_left [of y z x] by (simp only: inner_commute)
    5.71 -
    5.72 -lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    5.73 -  using inner_setsum_left [of f A x] by (simp only: inner_commute)
    5.74 -
    5.75 -lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    5.76 -lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    5.77 -lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    5.78 -
    5.79 -text \<open>Legacy theorem names\<close>
    5.80 -lemmas inner_left_distrib = inner_add_left
    5.81 -lemmas inner_right_distrib = inner_add_right
    5.82 -lemmas inner_distrib = inner_left_distrib inner_right_distrib
    5.83 -
    5.84 -lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    5.85 -  by (simp add: order_less_le)
    5.86 -
    5.87 -lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    5.88 -  by (simp add: norm_eq_sqrt_inner)
    5.89 -
    5.90 -text \<open>Identities involving real multiplication and division.\<close>
    5.91 -
    5.92 -lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    5.93 -  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    5.94 -
    5.95 -lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    5.96 -  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    5.97 -
    5.98 -lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    5.99 -  by (simp add: of_real_def)
   5.100 -
   5.101 -lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
   5.102 -  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
   5.103 -
   5.104 -lemma Cauchy_Schwarz_ineq:
   5.105 -  "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   5.106 -proof (cases)
   5.107 -  assume "y = 0"
   5.108 -  thus ?thesis by simp
   5.109 -next
   5.110 -  assume y: "y \<noteq> 0"
   5.111 -  let ?r = "inner x y / inner y y"
   5.112 -  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
   5.113 -    by (rule inner_ge_zero)
   5.114 -  also have "\<dots> = inner x x - inner y x * ?r"
   5.115 -    by (simp add: inner_diff)
   5.116 -  also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
   5.117 -    by (simp add: power2_eq_square inner_commute)
   5.118 -  finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
   5.119 -  hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   5.120 -    by (simp add: le_diff_eq)
   5.121 -  thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   5.122 -    by (simp add: pos_divide_le_eq y)
   5.123 -qed
   5.124 -
   5.125 -lemma Cauchy_Schwarz_ineq2:
   5.126 -  "\<bar>inner x y\<bar> \<le> norm x * norm y"
   5.127 -proof (rule power2_le_imp_le)
   5.128 -  have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   5.129 -    using Cauchy_Schwarz_ineq .
   5.130 -  thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   5.131 -    by (simp add: power_mult_distrib power2_norm_eq_inner)
   5.132 -  show "0 \<le> norm x * norm y"
   5.133 -    unfolding norm_eq_sqrt_inner
   5.134 -    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   5.135 -qed
   5.136 -
   5.137 -lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   5.138 -  using Cauchy_Schwarz_ineq2 [of x y] by auto
   5.139 -
   5.140 -subclass real_normed_vector
   5.141 -proof
   5.142 -  fix a :: real and x y :: 'a
   5.143 -  show "norm x = 0 \<longleftrightarrow> x = 0"
   5.144 -    unfolding norm_eq_sqrt_inner by simp
   5.145 -  show "norm (x + y) \<le> norm x + norm y"
   5.146 -    proof (rule power2_le_imp_le)
   5.147 -      have "inner x y \<le> norm x * norm y"
   5.148 -        by (rule norm_cauchy_schwarz)
   5.149 -      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   5.150 -        unfolding power2_sum power2_norm_eq_inner
   5.151 -        by (simp add: inner_add inner_commute)
   5.152 -      show "0 \<le> norm x + norm y"
   5.153 -        unfolding norm_eq_sqrt_inner by simp
   5.154 -    qed
   5.155 -  have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   5.156 -    by (simp add: real_sqrt_mult_distrib)
   5.157 -  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   5.158 -    unfolding norm_eq_sqrt_inner
   5.159 -    by (simp add: power2_eq_square mult.assoc)
   5.160 -qed
   5.161 -
   5.162 -end
   5.163 -
   5.164 -lemma inner_divide_left:
   5.165 -  fixes a :: "'a :: {real_inner,real_div_algebra}"
   5.166 -  shows "inner (a / of_real m) b = (inner a b) / m"
   5.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)
   5.168 -
   5.169 -lemma inner_divide_right:
   5.170 -  fixes a :: "'a :: {real_inner,real_div_algebra}"
   5.171 -  shows "inner a (b / of_real m) = (inner a b) / m"
   5.172 -  by (metis inner_commute inner_divide_left)
   5.173 -
   5.174 -text \<open>
   5.175 -  Re-enable constraints for @{term "open"}, @{term "uniformity"},
   5.176 -  @{term dist}, and @{term norm}.
   5.177 -\<close>
   5.178 -
   5.179 -setup \<open>Sign.add_const_constraint
   5.180 -  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   5.181 -
   5.182 -setup \<open>Sign.add_const_constraint
   5.183 -  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
   5.184 -
   5.185 -setup \<open>Sign.add_const_constraint
   5.186 -  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   5.187 -
   5.188 -setup \<open>Sign.add_const_constraint
   5.189 -  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   5.190 -
   5.191 -lemma bounded_bilinear_inner:
   5.192 -  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   5.193 -proof
   5.194 -  fix x y z :: 'a and r :: real
   5.195 -  show "inner (x + y) z = inner x z + inner y z"
   5.196 -    by (rule inner_add_left)
   5.197 -  show "inner x (y + z) = inner x y + inner x z"
   5.198 -    by (rule inner_add_right)
   5.199 -  show "inner (scaleR r x) y = scaleR r (inner x y)"
   5.200 -    unfolding real_scaleR_def by (rule inner_scaleR_left)
   5.201 -  show "inner x (scaleR r y) = scaleR r (inner x y)"
   5.202 -    unfolding real_scaleR_def by (rule inner_scaleR_right)
   5.203 -  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   5.204 -  proof
   5.205 -    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   5.206 -      by (simp add: Cauchy_Schwarz_ineq2)
   5.207 -  qed
   5.208 -qed
   5.209 -
   5.210 -lemmas tendsto_inner [tendsto_intros] =
   5.211 -  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   5.212 -
   5.213 -lemmas isCont_inner [simp] =
   5.214 -  bounded_bilinear.isCont [OF bounded_bilinear_inner]
   5.215 -
   5.216 -lemmas has_derivative_inner [derivative_intros] =
   5.217 -  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   5.218 -
   5.219 -lemmas bounded_linear_inner_left =
   5.220 -  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   5.221 -
   5.222 -lemmas bounded_linear_inner_right =
   5.223 -  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   5.224 -
   5.225 -lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
   5.226 -
   5.227 -lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
   5.228 -
   5.229 -lemmas has_derivative_inner_right [derivative_intros] =
   5.230 -  bounded_linear.has_derivative [OF bounded_linear_inner_right]
   5.231 -
   5.232 -lemmas has_derivative_inner_left [derivative_intros] =
   5.233 -  bounded_linear.has_derivative [OF bounded_linear_inner_left]
   5.234 -
   5.235 -lemma differentiable_inner [simp]:
   5.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"
   5.237 -  unfolding differentiable_def by (blast intro: has_derivative_inner)
   5.238 -
   5.239 -
   5.240 -subsection \<open>Class instances\<close>
   5.241 -
   5.242 -instantiation real :: real_inner
   5.243 -begin
   5.244 -
   5.245 -definition inner_real_def [simp]: "inner = op *"
   5.246 -
   5.247 -instance
   5.248 -proof
   5.249 -  fix x y z r :: real
   5.250 -  show "inner x y = inner y x"
   5.251 -    unfolding inner_real_def by (rule mult.commute)
   5.252 -  show "inner (x + y) z = inner x z + inner y z"
   5.253 -    unfolding inner_real_def by (rule distrib_right)
   5.254 -  show "inner (scaleR r x) y = r * inner x y"
   5.255 -    unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   5.256 -  show "0 \<le> inner x x"
   5.257 -    unfolding inner_real_def by simp
   5.258 -  show "inner x x = 0 \<longleftrightarrow> x = 0"
   5.259 -    unfolding inner_real_def by simp
   5.260 -  show "norm x = sqrt (inner x x)"
   5.261 -    unfolding inner_real_def by simp
   5.262 -qed
   5.263 -
   5.264 -end
   5.265 -
   5.266 -lemma
   5.267 -  shows real_inner_1_left[simp]: "inner 1 x = x"
   5.268 -    and real_inner_1_right[simp]: "inner x 1 = x"
   5.269 -  by simp_all
   5.270 -
   5.271 -instantiation complex :: real_inner
   5.272 -begin
   5.273 -
   5.274 -definition inner_complex_def:
   5.275 -  "inner x y = Re x * Re y + Im x * Im y"
   5.276 -
   5.277 -instance
   5.278 -proof
   5.279 -  fix x y z :: complex and r :: real
   5.280 -  show "inner x y = inner y x"
   5.281 -    unfolding inner_complex_def by (simp add: mult.commute)
   5.282 -  show "inner (x + y) z = inner x z + inner y z"
   5.283 -    unfolding inner_complex_def by (simp add: distrib_right)
   5.284 -  show "inner (scaleR r x) y = r * inner x y"
   5.285 -    unfolding inner_complex_def by (simp add: distrib_left)
   5.286 -  show "0 \<le> inner x x"
   5.287 -    unfolding inner_complex_def by simp
   5.288 -  show "inner x x = 0 \<longleftrightarrow> x = 0"
   5.289 -    unfolding inner_complex_def
   5.290 -    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   5.291 -  show "norm x = sqrt (inner x x)"
   5.292 -    unfolding inner_complex_def complex_norm_def
   5.293 -    by (simp add: power2_eq_square)
   5.294 -qed
   5.295 -
   5.296 -end
   5.297 -
   5.298 -lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   5.299 -  unfolding inner_complex_def by simp
   5.300 -
   5.301 -lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   5.302 -  unfolding inner_complex_def by simp
   5.303 -
   5.304 -lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
   5.305 -  unfolding inner_complex_def by simp
   5.306 -
   5.307 -lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
   5.308 -  unfolding inner_complex_def by simp
   5.309 -
   5.310 -
   5.311 -subsection \<open>Gradient derivative\<close>
   5.312 -
   5.313 -definition
   5.314 -  gderiv ::
   5.315 -    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   5.316 -          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   5.317 -where
   5.318 -  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   5.319 -
   5.320 -lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   5.321 -  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   5.322 -
   5.323 -lemma GDERIV_DERIV_compose:
   5.324 -    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   5.325 -     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   5.326 -  unfolding gderiv_def has_field_derivative_def
   5.327 -  apply (drule (1) has_derivative_compose)
   5.328 -  apply (simp add: ac_simps)
   5.329 -  done
   5.330 -
   5.331 -lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   5.332 -  by simp
   5.333 -
   5.334 -lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   5.335 -  by simp
   5.336 -
   5.337 -lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   5.338 -  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   5.339 -
   5.340 -lemma GDERIV_add:
   5.341 -    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   5.342 -     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   5.343 -  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   5.344 -
   5.345 -lemma GDERIV_minus:
   5.346 -    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   5.347 -  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   5.348 -
   5.349 -lemma GDERIV_diff:
   5.350 -    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   5.351 -     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   5.352 -  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   5.353 -
   5.354 -lemma GDERIV_scaleR:
   5.355 -    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   5.356 -     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   5.357 -      :> (scaleR (f x) dg + scaleR df (g x))"
   5.358 -  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   5.359 -  apply (rule has_derivative_subst)
   5.360 -  apply (erule (1) has_derivative_scaleR)
   5.361 -  apply (simp add: ac_simps)
   5.362 -  done
   5.363 -
   5.364 -lemma GDERIV_mult:
   5.365 -    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   5.366 -     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   5.367 -  unfolding gderiv_def
   5.368 -  apply (rule has_derivative_subst)
   5.369 -  apply (erule (1) has_derivative_mult)
   5.370 -  apply (simp add: inner_add ac_simps)
   5.371 -  done
   5.372 -
   5.373 -lemma GDERIV_inverse:
   5.374 -    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   5.375 -     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   5.376 -  apply (erule GDERIV_DERIV_compose)
   5.377 -  apply (erule DERIV_inverse [folded numeral_2_eq_2])
   5.378 -  done
   5.379 -
   5.380 -lemma GDERIV_norm:
   5.381 -  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   5.382 -proof -
   5.383 -  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   5.384 -    by (intro has_derivative_inner has_derivative_ident)
   5.385 -  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   5.386 -    by (simp add: fun_eq_iff inner_commute)
   5.387 -  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   5.388 -  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   5.389 -    by (rule DERIV_real_sqrt)
   5.390 -  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   5.391 -    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   5.392 -  show ?thesis
   5.393 -    unfolding norm_eq_sqrt_inner
   5.394 -    apply (rule GDERIV_subst [OF _ 4])
   5.395 -    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   5.396 -    apply (subst gderiv_def)
   5.397 -    apply (rule has_derivative_subst [OF _ 2])
   5.398 -    apply (rule 1)
   5.399 -    apply (rule 3)
   5.400 -    done
   5.401 -qed
   5.402 -
   5.403 -lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   5.404 -
   5.405 -end
     6.1 --- a/src/HOL/Library/Library.thy	Fri Sep 30 15:35:32 2016 +0200
     6.2 +++ b/src/HOL/Library/Library.thy	Fri Sep 30 15:35:37 2016 +0200
     6.3 @@ -37,7 +37,6 @@
     6.4    Groups_Big_Fun
     6.5    Indicator_Function
     6.6    Infinite_Set
     6.7 -  Inner_Product
     6.8    IArray
     6.9    Lattice_Algebras
    6.10    Lattice_Syntax
    6.11 @@ -62,7 +61,7 @@
    6.12    Polynomial
    6.13    Polynomial_FPS
    6.14    Preorder
    6.15 -  Product_Vector
    6.16 +  Product_plus
    6.17    Quadratic_Discriminant
    6.18    Quotient_List
    6.19    Quotient_Option
     7.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Sep 30 15:35:32 2016 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,369 +0,0 @@
     7.4 -(*  Title:      HOL/Library/Product_Vector.thy
     7.5 -    Author:     Brian Huffman
     7.6 -*)
     7.7 -
     7.8 -section \<open>Cartesian Products as Vector Spaces\<close>
     7.9 -
    7.10 -theory Product_Vector
    7.11 -imports Inner_Product Product_plus
    7.12 -begin
    7.13 -
    7.14 -subsection \<open>Product is a real vector space\<close>
    7.15 -
    7.16 -instantiation prod :: (real_vector, real_vector) real_vector
    7.17 -begin
    7.18 -
    7.19 -definition scaleR_prod_def:
    7.20 -  "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"
    7.21 -
    7.22 -lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)"
    7.23 -  unfolding scaleR_prod_def by simp
    7.24 -
    7.25 -lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)"
    7.26 -  unfolding scaleR_prod_def by simp
    7.27 -
    7.28 -lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
    7.29 -  unfolding scaleR_prod_def by simp
    7.30 -
    7.31 -instance
    7.32 -proof
    7.33 -  fix a b :: real and x y :: "'a \<times> 'b"
    7.34 -  show "scaleR a (x + y) = scaleR a x + scaleR a y"
    7.35 -    by (simp add: prod_eq_iff scaleR_right_distrib)
    7.36 -  show "scaleR (a + b) x = scaleR a x + scaleR b x"
    7.37 -    by (simp add: prod_eq_iff scaleR_left_distrib)
    7.38 -  show "scaleR a (scaleR b x) = scaleR (a * b) x"
    7.39 -    by (simp add: prod_eq_iff)
    7.40 -  show "scaleR 1 x = x"
    7.41 -    by (simp add: prod_eq_iff)
    7.42 -qed
    7.43 -
    7.44 -end
    7.45 -
    7.46 -subsection \<open>Product is a metric space\<close>
    7.47 -
    7.48 -(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
    7.49 -
    7.50 -instantiation prod :: (metric_space, metric_space) dist
    7.51 -begin
    7.52 -
    7.53 -definition dist_prod_def[code del]:
    7.54 -  "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
    7.55 -
    7.56 -instance ..
    7.57 -end
    7.58 -
    7.59 -instantiation prod :: (metric_space, metric_space) uniformity_dist
    7.60 -begin
    7.61 -
    7.62 -definition [code del]:
    7.63 -  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
    7.64 -    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    7.65 -
    7.66 -instance
    7.67 -  by standard (rule uniformity_prod_def)
    7.68 -end
    7.69 -
    7.70 -declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
    7.71 -
    7.72 -instantiation prod :: (metric_space, metric_space) metric_space
    7.73 -begin
    7.74 -
    7.75 -lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
    7.76 -  unfolding dist_prod_def by simp
    7.77 -
    7.78 -lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
    7.79 -  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
    7.80 -
    7.81 -lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
    7.82 -  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
    7.83 -
    7.84 -instance
    7.85 -proof
    7.86 -  fix x y :: "'a \<times> 'b"
    7.87 -  show "dist x y = 0 \<longleftrightarrow> x = y"
    7.88 -    unfolding dist_prod_def prod_eq_iff by simp
    7.89 -next
    7.90 -  fix x y z :: "'a \<times> 'b"
    7.91 -  show "dist x y \<le> dist x z + dist y z"
    7.92 -    unfolding dist_prod_def
    7.93 -    by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
    7.94 -        real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
    7.95 -next
    7.96 -  fix S :: "('a \<times> 'b) set"
    7.97 -  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    7.98 -  proof
    7.99 -    assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   7.100 -    proof
   7.101 -      fix x assume "x \<in> S"
   7.102 -      obtain A B where "open A" "open B" "x \<in> A \<times> B" "A \<times> B \<subseteq> S"
   7.103 -        using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
   7.104 -      obtain r where r: "0 < r" "\<forall>y. dist y (fst x) < r \<longrightarrow> y \<in> A"
   7.105 -        using \<open>open A\<close> and \<open>x \<in> A \<times> B\<close> unfolding open_dist by auto
   7.106 -      obtain s where s: "0 < s" "\<forall>y. dist y (snd x) < s \<longrightarrow> y \<in> B"
   7.107 -        using \<open>open B\<close> and \<open>x \<in> A \<times> B\<close> unfolding open_dist by auto
   7.108 -      let ?e = "min r s"
   7.109 -      have "0 < ?e \<and> (\<forall>y. dist y x < ?e \<longrightarrow> y \<in> S)"
   7.110 -      proof (intro allI impI conjI)
   7.111 -        show "0 < min r s" by (simp add: r(1) s(1))
   7.112 -      next
   7.113 -        fix y assume "dist y x < min r s"
   7.114 -        hence "dist y x < r" and "dist y x < s"
   7.115 -          by simp_all
   7.116 -        hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s"
   7.117 -          by (auto intro: le_less_trans dist_fst_le dist_snd_le)
   7.118 -        hence "fst y \<in> A" and "snd y \<in> B"
   7.119 -          by (simp_all add: r(2) s(2))
   7.120 -        hence "y \<in> A \<times> B" by (induct y, simp)
   7.121 -        with \<open>A \<times> B \<subseteq> S\<close> show "y \<in> S" ..
   7.122 -      qed
   7.123 -      thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
   7.124 -    qed
   7.125 -  next
   7.126 -    assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
   7.127 -    proof (rule open_prod_intro)
   7.128 -      fix x assume "x \<in> S"
   7.129 -      then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   7.130 -        using * by fast
   7.131 -      define r where "r = e / sqrt 2"
   7.132 -      define s where "s = e / sqrt 2"
   7.133 -      from \<open>0 < e\<close> have "0 < r" and "0 < s"
   7.134 -        unfolding r_def s_def by simp_all
   7.135 -      from \<open>0 < e\<close> have "e = sqrt (r\<^sup>2 + s\<^sup>2)"
   7.136 -        unfolding r_def s_def by (simp add: power_divide)
   7.137 -      define A where "A = {y. dist (fst x) y < r}"
   7.138 -      define B where "B = {y. dist (snd x) y < s}"
   7.139 -      have "open A" and "open B"
   7.140 -        unfolding A_def B_def by (simp_all add: open_ball)
   7.141 -      moreover have "x \<in> A \<times> B"
   7.142 -        unfolding A_def B_def mem_Times_iff
   7.143 -        using \<open>0 < r\<close> and \<open>0 < s\<close> by simp
   7.144 -      moreover have "A \<times> B \<subseteq> S"
   7.145 -      proof (clarify)
   7.146 -        fix a b assume "a \<in> A" and "b \<in> B"
   7.147 -        hence "dist a (fst x) < r" and "dist b (snd x) < s"
   7.148 -          unfolding A_def B_def by (simp_all add: dist_commute)
   7.149 -        hence "dist (a, b) x < e"
   7.150 -          unfolding dist_prod_def \<open>e = sqrt (r\<^sup>2 + s\<^sup>2)\<close>
   7.151 -          by (simp add: add_strict_mono power_strict_mono)
   7.152 -        thus "(a, b) \<in> S"
   7.153 -          by (simp add: S)
   7.154 -      qed
   7.155 -      ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
   7.156 -    qed
   7.157 -  qed
   7.158 -  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   7.159 -    unfolding * eventually_uniformity_metric
   7.160 -    by (simp del: split_paired_All add: dist_prod_def dist_commute)
   7.161 -qed
   7.162 -
   7.163 -end
   7.164 -
   7.165 -declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
   7.166 -
   7.167 -lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
   7.168 -  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
   7.169 -
   7.170 -lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
   7.171 -  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
   7.172 -
   7.173 -lemma Cauchy_Pair:
   7.174 -  assumes "Cauchy X" and "Cauchy Y"
   7.175 -  shows "Cauchy (\<lambda>n. (X n, Y n))"
   7.176 -proof (rule metric_CauchyI)
   7.177 -  fix r :: real assume "0 < r"
   7.178 -  hence "0 < r / sqrt 2" (is "0 < ?s") by simp
   7.179 -  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
   7.180 -    using metric_CauchyD [OF \<open>Cauchy X\<close> \<open>0 < ?s\<close>] ..
   7.181 -  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
   7.182 -    using metric_CauchyD [OF \<open>Cauchy Y\<close> \<open>0 < ?s\<close>] ..
   7.183 -  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
   7.184 -    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
   7.185 -  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
   7.186 -qed
   7.187 -
   7.188 -subsection \<open>Product is a complete metric space\<close>
   7.189 -
   7.190 -instance prod :: (complete_space, complete_space) complete_space
   7.191 -proof
   7.192 -  fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   7.193 -  have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
   7.194 -    using Cauchy_fst [OF \<open>Cauchy X\<close>]
   7.195 -    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   7.196 -  have 2: "(\<lambda>n. snd (X n)) \<longlonglongrightarrow> lim (\<lambda>n. snd (X n))"
   7.197 -    using Cauchy_snd [OF \<open>Cauchy X\<close>]
   7.198 -    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   7.199 -  have "X \<longlonglongrightarrow> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
   7.200 -    using tendsto_Pair [OF 1 2] by simp
   7.201 -  then show "convergent X"
   7.202 -    by (rule convergentI)
   7.203 -qed
   7.204 -
   7.205 -subsection \<open>Product is a normed vector space\<close>
   7.206 -
   7.207 -instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
   7.208 -begin
   7.209 -
   7.210 -definition norm_prod_def[code del]:
   7.211 -  "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)"
   7.212 -
   7.213 -definition sgn_prod_def:
   7.214 -  "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
   7.215 -
   7.216 -lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
   7.217 -  unfolding norm_prod_def by simp
   7.218 -
   7.219 -instance
   7.220 -proof
   7.221 -  fix r :: real and x y :: "'a \<times> 'b"
   7.222 -  show "norm x = 0 \<longleftrightarrow> x = 0"
   7.223 -    unfolding norm_prod_def
   7.224 -    by (simp add: prod_eq_iff)
   7.225 -  show "norm (x + y) \<le> norm x + norm y"
   7.226 -    unfolding norm_prod_def
   7.227 -    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
   7.228 -    apply (simp add: add_mono power_mono norm_triangle_ineq)
   7.229 -    done
   7.230 -  show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
   7.231 -    unfolding norm_prod_def
   7.232 -    apply (simp add: power_mult_distrib)
   7.233 -    apply (simp add: distrib_left [symmetric])
   7.234 -    apply (simp add: real_sqrt_mult_distrib)
   7.235 -    done
   7.236 -  show "sgn x = scaleR (inverse (norm x)) x"
   7.237 -    by (rule sgn_prod_def)
   7.238 -  show "dist x y = norm (x - y)"
   7.239 -    unfolding dist_prod_def norm_prod_def
   7.240 -    by (simp add: dist_norm)
   7.241 -qed
   7.242 -
   7.243 -end
   7.244 -
   7.245 -declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
   7.246 -
   7.247 -instance prod :: (banach, banach) banach ..
   7.248 -
   7.249 -subsubsection \<open>Pair operations are linear\<close>
   7.250 -
   7.251 -lemma bounded_linear_fst: "bounded_linear fst"
   7.252 -  using fst_add fst_scaleR
   7.253 -  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   7.254 -
   7.255 -lemma bounded_linear_snd: "bounded_linear snd"
   7.256 -  using snd_add snd_scaleR
   7.257 -  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   7.258 -
   7.259 -lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose]
   7.260 -
   7.261 -lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose]
   7.262 -
   7.263 -lemma bounded_linear_Pair:
   7.264 -  assumes f: "bounded_linear f"
   7.265 -  assumes g: "bounded_linear g"
   7.266 -  shows "bounded_linear (\<lambda>x. (f x, g x))"
   7.267 -proof
   7.268 -  interpret f: bounded_linear f by fact
   7.269 -  interpret g: bounded_linear g by fact
   7.270 -  fix x y and r :: real
   7.271 -  show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)"
   7.272 -    by (simp add: f.add g.add)
   7.273 -  show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)"
   7.274 -    by (simp add: f.scaleR g.scaleR)
   7.275 -  obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf"
   7.276 -    using f.pos_bounded by fast
   7.277 -  obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
   7.278 -    using g.pos_bounded by fast
   7.279 -  have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
   7.280 -    apply (rule allI)
   7.281 -    apply (simp add: norm_Pair)
   7.282 -    apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
   7.283 -    apply (simp add: distrib_left)
   7.284 -    apply (rule add_mono [OF norm_f norm_g])
   7.285 -    done
   7.286 -  then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
   7.287 -qed
   7.288 -
   7.289 -subsubsection \<open>Frechet derivatives involving pairs\<close>
   7.290 -
   7.291 -lemma has_derivative_Pair [derivative_intros]:
   7.292 -  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   7.293 -  shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
   7.294 -proof (rule has_derivativeI_sandwich[of 1])
   7.295 -  show "bounded_linear (\<lambda>h. (f' h, g' h))"
   7.296 -    using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   7.297 -  let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
   7.298 -  let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
   7.299 -  let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
   7.300 -
   7.301 -  show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)"
   7.302 -    using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm)
   7.303 -
   7.304 -  fix y :: 'a assume "y \<noteq> x"
   7.305 -  show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
   7.306 -    unfolding add_divide_distrib [symmetric]
   7.307 -    by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
   7.308 -qed simp
   7.309 -
   7.310 -lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
   7.311 -lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
   7.312 -
   7.313 -lemma has_derivative_split [derivative_intros]:
   7.314 -  "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   7.315 -  unfolding split_beta' .
   7.316 -
   7.317 -subsection \<open>Product is an inner product space\<close>
   7.318 -
   7.319 -instantiation prod :: (real_inner, real_inner) real_inner
   7.320 -begin
   7.321 -
   7.322 -definition inner_prod_def:
   7.323 -  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
   7.324 -
   7.325 -lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
   7.326 -  unfolding inner_prod_def by simp
   7.327 -
   7.328 -instance
   7.329 -proof
   7.330 -  fix r :: real
   7.331 -  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
   7.332 -  show "inner x y = inner y x"
   7.333 -    unfolding inner_prod_def
   7.334 -    by (simp add: inner_commute)
   7.335 -  show "inner (x + y) z = inner x z + inner y z"
   7.336 -    unfolding inner_prod_def
   7.337 -    by (simp add: inner_add_left)
   7.338 -  show "inner (scaleR r x) y = r * inner x y"
   7.339 -    unfolding inner_prod_def
   7.340 -    by (simp add: distrib_left)
   7.341 -  show "0 \<le> inner x x"
   7.342 -    unfolding inner_prod_def
   7.343 -    by (intro add_nonneg_nonneg inner_ge_zero)
   7.344 -  show "inner x x = 0 \<longleftrightarrow> x = 0"
   7.345 -    unfolding inner_prod_def prod_eq_iff
   7.346 -    by (simp add: add_nonneg_eq_0_iff)
   7.347 -  show "norm x = sqrt (inner x x)"
   7.348 -    unfolding norm_prod_def inner_prod_def
   7.349 -    by (simp add: power2_norm_eq_inner)
   7.350 -qed
   7.351 -
   7.352 -end
   7.353 -
   7.354 -lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
   7.355 -    by (cases x, simp)+
   7.356 -
   7.357 -lemma
   7.358 -  fixes x :: "'a::real_normed_vector"
   7.359 -  shows norm_Pair1 [simp]: "norm (0,x) = norm x"
   7.360 -    and norm_Pair2 [simp]: "norm (x,0) = norm x"
   7.361 -by (auto simp: norm_Pair)
   7.362 -
   7.363 -lemma norm_commute: "norm (x,y) = norm (y,x)"
   7.364 -  by (simp add: norm_Pair)
   7.365 -
   7.366 -lemma norm_fst_le: "norm x \<le> norm (x,y)"
   7.367 -  by (metis dist_fst_le fst_conv fst_zero norm_conv_dist)
   7.368 -
   7.369 -lemma norm_snd_le: "norm y \<le> norm (x,y)"
   7.370 -  by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
   7.371 -
   7.372 -end
     8.1 --- a/src/HOL/Mirabelle/ex/Ex.thy	Fri Sep 30 15:35:32 2016 +0200
     8.2 +++ b/src/HOL/Mirabelle/ex/Ex.thy	Fri Sep 30 15:35:37 2016 +0200
     8.3 @@ -3,7 +3,7 @@
     8.4  
     8.5  ML \<open>
     8.6    val rc = Isabelle_System.bash
     8.7 -    "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy";
     8.8 +    "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy";
     8.9    if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
    8.10    else ();
    8.11  \<close> \<comment> "some arbitrary small test case"