author nipkow Tue Sep 04 08:40:53 2018 +0200 (9 months ago) changeset 68902 8414bbd7bb46 parent 68901 4824cc40f42e child 68903 58525b08eed1 child 68911 7f2ebaa4c71f
tuned
```     1.1 --- a/src/HOL/Analysis/Cross3.thy	Mon Sep 03 22:38:23 2018 +0200
1.2 +++ b/src/HOL/Analysis/Cross3.thy	Tue Sep 04 08:40:53 2018 +0200
1.3 @@ -4,7 +4,7 @@
1.4  Ported from HOL Light
1.5  *)
1.6
1.7 -section\<open>Vector Cross Products in 3 Dimensions.\<close>
1.8 +section\<open>Vector Cross Products in 3 Dimensions\<close>
1.9
1.10  theory "Cross3"
1.11    imports Determinants
1.12 @@ -33,48 +33,48 @@
1.13
1.14  unbundle cross3_syntax
1.15
1.16 -subsection%important\<open> Basic lemmas.\<close>
1.17 +subsection%important\<open> Basic lemmas\<close>
1.18
1.19  lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
1.20
1.21 -lemma%unimportant dot_cross_self: "x \<bullet> (x \<times> y) = 0" "x \<bullet> (y \<times> x) = 0" "(x \<times> y) \<bullet> y = 0" "(y \<times> x) \<bullet> y = 0"
1.22 +lemma dot_cross_self: "x \<bullet> (x \<times> y) = 0" "x \<bullet> (y \<times> x) = 0" "(x \<times> y) \<bullet> y = 0" "(y \<times> x) \<bullet> y = 0"
1.23    by (simp_all add: orthogonal_def cross3_simps)
1.24
1.25 -lemma%unimportant  orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y"
1.26 +lemma  orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y"
1.27                          "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x"
1.28    by (simp_all add: orthogonal_def dot_cross_self)
1.29
1.30 -lemma%unimportant  cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3"
1.31 +lemma  cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3"
1.33
1.34 -lemma%unimportant  cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3"
1.35 +lemma  cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3"
1.37
1.38 -lemma%unimportant  cross_refl [simp]: "x \<times> x = 0" for x::"real^3"
1.39 +lemma  cross_refl [simp]: "x \<times> x = 0" for x::"real^3"
1.41
1.42 -lemma%unimportant  cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3"
1.43 +lemma  cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3"
1.45
1.46 -lemma%unimportant  cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3"
1.47 +lemma  cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3"
1.49
1.50 -lemma%unimportant  cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3"
1.51 +lemma  cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3"
1.53
1.54 -lemma%unimportant  cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3"
1.55 +lemma  cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3"
1.57
1.58 -lemma%unimportant  cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3"
1.59 +lemma  cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3"
1.61
1.62 -lemma%unimportant  cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3"
1.63 +lemma  cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3"
1.65
1.66 -lemma%unimportant  left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3"
1.67 +lemma  left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3"
1.69
1.70 -lemma%unimportant  right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
1.71 +lemma  right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
1.73
1.74  hide_fact (open) left_diff_distrib right_diff_distrib
1.75 @@ -85,24 +85,24 @@
1.76  lemma%important  Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
1.77    by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3)
1.78
1.79 -lemma%unimportant  cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
1.80 +lemma  cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
1.81    by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
1.82
1.83 -lemma%unimportant  cross_components:
1.84 +lemma  cross_components:
1.85     "(x \<times> y)\$1 = x\$2 * y\$3 - y\$2 * x\$3" "(x \<times> y)\$2 = x\$3 * y\$1 - y\$3 * x\$1" "(x \<times> y)\$3 = x\$1 * y\$2 - y\$1 * x\$2"
1.86    by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
1.87
1.88 -lemma%unimportant  cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)"
1.89 +lemma  cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)"
1.90                     "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)"
1.91                     "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)"
1.92    using exhaust_3
1.93    by (force simp add: axis_def cross3_simps)+
1.94
1.95 -lemma%unimportant  cross_basis_nonzero:
1.96 +lemma  cross_basis_nonzero:
1.97    "u \<noteq> 0 \<Longrightarrow> ~(u \<times> axis 1 1 = 0) \<or> ~(u \<times> axis 2 1 = 0) \<or> ~(u \<times> axis 3 1 = 0)"
1.98    by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
1.99
1.100 -lemma%unimportant  cross_dot_cancel:
1.101 +lemma  cross_dot_cancel:
1.102    fixes x::"real^3"
1.103    assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0"
1.104    shows "y = z"
1.105 @@ -116,20 +116,20 @@
1.106      using eq_iff_diff_eq_0 by blast
1.107  qed
1.108
1.109 -lemma%unimportant  norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2"
1.110 +lemma  norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2"
1.111    unfolding power2_norm_eq_inner power_mult_distrib
1.112    by (simp add: cross3_simps power2_eq_square)
1.113
1.114 -lemma%unimportant  dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])"
1.115 +lemma  dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])"
1.117
1.118 -lemma%unimportant  cross_cross_det: "(w \<times> x) \<times> (y \<times> z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z"
1.119 +lemma  cross_cross_det: "(w \<times> x) \<times> (y \<times> z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z"
1.120    using exhaust_3 by (force simp add: cross3_simps)
1.121
1.122  lemma%important  dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)"
1.123    by%unimportant (force simp add: cross3_simps)
1.124
1.125 -lemma%unimportant  norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
1.126 +lemma  norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
1.127    unfolding power2_norm_eq_inner power_mult_distrib
1.128    by (simp add: cross3_simps power2_eq_square)
1.129
1.130 @@ -147,11 +147,11 @@
1.131    finally show ?thesis .
1.132  qed
1.133
1.134 -lemma%unimportant  cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0"
1.135 +lemma  cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0"
1.136    apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff)
1.137    by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff)
1.138
1.139 -lemma%unimportant  norm_and_cross_eq_0:
1.140 +lemma  norm_and_cross_eq_0:
1.141     "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs")
1.142  proof
1.143    assume ?lhs
1.144 @@ -159,7 +159,7 @@
1.145      by (metis cross_dot_cancel cross_zero_right inner_zero_right)
1.146  qed auto
1.147
1.148 -lemma%unimportant  bilinear_cross: "bilinear(\<times>)"
1.149 +lemma  bilinear_cross: "bilinear(\<times>)"
1.150    apply (auto simp add: bilinear_def linear_def)
1.151    apply unfold_locales
1.153 @@ -168,9 +168,9 @@
1.155    done
1.156
1.157 -subsection%important   \<open>Preservation by rotation, or other orthogonal transformation up to sign.\<close>
1.158 +subsection%important   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
1.159
1.160 -lemma%unimportant  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
1.161 +lemma  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
1.162    apply (simp add: vec_eq_iff   )
1.163    apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps)
1.164    done
1.165 @@ -185,10 +185,10 @@
1.166      by (metis (no_types) vector_matrix_mul_rid vector_transpose_matrix cross_matrix_mult matrix_vector_mul_assoc matrix_vector_mult_scaleR)
1.167  qed
1.168
1.169 -lemma%unimportant  cross_rotation_matrix: "rotation_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) =  A *v (x \<times> y)"
1.170 +lemma  cross_rotation_matrix: "rotation_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) =  A *v (x \<times> y)"
1.171    by (simp add: rotation_matrix_def cross_orthogonal_matrix)
1.172
1.173 -lemma%unimportant  cross_rotoinversion_matrix: "rotoinversion_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) = - A *v (x \<times> y)"
1.174 +lemma  cross_rotoinversion_matrix: "rotoinversion_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) = - A *v (x \<times> y)"
1.175    by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc)
1.176
1.177  lemma%important  cross_orthogonal_transformation:
1.178 @@ -203,20 +203,20 @@
1.179      by simp
1.180  qed
1.181
1.182 -lemma%unimportant  cross_linear_image:
1.183 +lemma  cross_linear_image:
1.184     "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk>
1.185             \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
1.186    by (simp add: cross_orthogonal_transformation orthogonal_transformation)
1.187
1.188  subsection%unimportant \<open>Continuity\<close>
1.189
1.190 -lemma%unimportant  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
1.191 +lemma  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
1.192    apply (subst continuous_componentwise)
1.193    apply (clarsimp simp add: cross3_simps)
1.194    apply (intro continuous_intros; simp)
1.195    done
1.196
1.197 -lemma%unimportant  continuous_on_cross:
1.198 +lemma  continuous_on_cross:
1.199    fixes f :: "'a::t2_space \<Rightarrow> real^3"
1.200    shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
1.201    by (simp add: continuous_on_eq_continuous_within continuous_cross)
```