src/HOL/Analysis/Cross3.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69683 8b3458ca0762
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
lp15@68466
     1
(* Title:      HOL/Analysis/Cross3.thy
lp15@68466
     2
   Author:     L C Paulson, University of Cambridge
lp15@68466
     3
lp15@68466
     4
Ported from HOL Light
lp15@68466
     5
*)
lp15@68466
     6
nipkow@68902
     7
section\<open>Vector Cross Products in 3 Dimensions\<close>
lp15@68466
     8
lp15@68465
     9
theory "Cross3"
immler@69675
    10
  imports Determinants Cartesian_Euclidean_Space
lp15@68465
    11
begin
lp15@68465
    12
lp15@68467
    13
context includes no_Set_Product_syntax 
lp15@68467
    14
begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
lp15@68467
    15
ak2110@68833
    16
definition%important cross3 :: "[real^3, real^3] \<Rightarrow> real^3"  (infixr "\<times>" 80)
lp15@68465
    17
  where "a \<times> b \<equiv>
lp15@68465
    18
    vector [a$2 * b$3 - a$3 * b$2,
lp15@68465
    19
            a$3 * b$1 - a$1 * b$3,
lp15@68465
    20
            a$1 * b$2 - a$2 * b$1]"
lp15@68465
    21
lp15@68467
    22
end
lp15@68467
    23
lp15@68467
    24
bundle cross3_syntax begin
lp15@68467
    25
notation cross3 (infixr "\<times>" 80)
lp15@68467
    26
no_notation Product_Type.Times (infixr "\<times>" 80)
lp15@68467
    27
end
lp15@68467
    28
lp15@68467
    29
bundle no_cross3_syntax begin
lp15@68467
    30
no_notation cross3 (infixr "\<times>" 80)
lp15@68467
    31
notation Product_Type.Times (infixr "\<times>" 80)
lp15@68467
    32
end
lp15@68467
    33
lp15@68467
    34
unbundle cross3_syntax
lp15@68467
    35
immler@69683
    36
subsection\<open> Basic lemmas\<close>
lp15@68465
    37
lp15@68465
    38
lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
lp15@68465
    39
nipkow@68902
    40
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"
lp15@68465
    41
  by (simp_all add: orthogonal_def cross3_simps)
lp15@68465
    42
nipkow@68902
    43
lemma  orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y"  
lp15@68465
    44
                        "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x"
lp15@68465
    45
  by (simp_all add: orthogonal_def dot_cross_self)
lp15@68465
    46
nipkow@68902
    47
lemma  cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3"
lp15@68465
    48
  by (simp_all add: cross3_simps)
lp15@68465
    49
nipkow@68902
    50
lemma  cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3"
lp15@68465
    51
  by (simp add: cross3_simps)
lp15@68465
    52
nipkow@68902
    53
lemma  cross_refl [simp]: "x \<times> x = 0" for x::"real^3"
lp15@68465
    54
  by (simp add: cross3_simps)
lp15@68465
    55
nipkow@68902
    56
lemma  cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3"
lp15@68465
    57
  by (simp add: cross3_simps)
lp15@68465
    58
nipkow@68902
    59
lemma  cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3"
lp15@68465
    60
  by (simp add: cross3_simps)
lp15@68465
    61
nipkow@68902
    62
lemma  cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3"
lp15@68465
    63
  by (simp add: cross3_simps)
lp15@68465
    64
nipkow@68902
    65
lemma  cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3"
lp15@68465
    66
  by (simp add: cross3_simps)
lp15@68465
    67
nipkow@68902
    68
lemma  cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3"
lp15@68465
    69
  by (simp add: cross3_simps)
lp15@68465
    70
nipkow@68902
    71
lemma  cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3"
lp15@68465
    72
  by (simp add: cross3_simps)
lp15@68465
    73
nipkow@68902
    74
lemma  left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3"
lp15@68465
    75
  by (simp add: cross3_simps)
lp15@68465
    76
nipkow@68902
    77
lemma  right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
lp15@68465
    78
  by (simp add: cross3_simps)
lp15@68465
    79
lp15@68467
    80
hide_fact (open) left_diff_distrib right_diff_distrib
lp15@68467
    81
immler@69681
    82
proposition Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3"
immler@69682
    83
  by (simp add: cross3_simps)
lp15@68465
    84
immler@69682
    85
proposition Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
immler@69682
    86
  by (simp add: cross3_simps) (metis (full_types) exhaust_3)
lp15@68465
    87
immler@69682
    88
proposition cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
immler@69682
    89
  by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
lp15@68465
    90
nipkow@68902
    91
lemma  cross_components:
lp15@68465
    92
   "(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"
lp15@68465
    93
  by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
lp15@68465
    94
nipkow@68902
    95
lemma  cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)" 
lp15@68465
    96
                   "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)" 
lp15@68465
    97
                   "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)"
lp15@68465
    98
  using exhaust_3
lp15@68465
    99
  by (force simp add: axis_def cross3_simps)+
lp15@68465
   100
nipkow@68902
   101
lemma  cross_basis_nonzero:
nipkow@69508
   102
  "u \<noteq> 0 \<Longrightarrow> u \<times> axis 1 1 \<noteq> 0 \<or> u \<times> axis 2 1 \<noteq> 0 \<or> u \<times> axis 3 1 \<noteq> 0"
lp15@68465
   103
  by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
lp15@68465
   104
nipkow@68902
   105
lemma  cross_dot_cancel:
lp15@68465
   106
  fixes x::"real^3"
lp15@68465
   107
  assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0"
lp15@68465
   108
  shows "y = z" 
lp15@68465
   109
proof -
lp15@68465
   110
  have "x \<bullet> x \<noteq> 0"
lp15@68465
   111
    by (simp add: x)
lp15@68465
   112
  then have "y - z = 0"
lp15@68465
   113
    using veq
lp15@68465
   114
    by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff)
lp15@68465
   115
  then show ?thesis
lp15@68465
   116
    using eq_iff_diff_eq_0 by blast
lp15@68465
   117
qed
lp15@68465
   118
nipkow@68902
   119
lemma  norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2"
lp15@68465
   120
  unfolding power2_norm_eq_inner power_mult_distrib
lp15@68465
   121
  by (simp add: cross3_simps power2_eq_square)
lp15@68465
   122
nipkow@68902
   123
lemma  dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])"
lp15@68465
   124
  by (simp add: cross3_simps) 
lp15@68465
   125
nipkow@68902
   126
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"
lp15@68465
   127
  using exhaust_3 by (force simp add: cross3_simps) 
lp15@68465
   128
immler@69681
   129
proposition  dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)"
immler@69682
   130
  by (force simp add: cross3_simps)
lp15@68465
   131
immler@69681
   132
proposition  norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
lp15@68465
   133
  unfolding power2_norm_eq_inner power_mult_distrib
lp15@68465
   134
  by (simp add: cross3_simps power2_eq_square)
lp15@68465
   135
immler@69681
   136
lemma  cross_eq_0: "x \<times> y = 0 \<longleftrightarrow> collinear{0,x,y}"
immler@69681
   137
proof -
lp15@68465
   138
  have "x \<times> y = 0 \<longleftrightarrow> norm (x \<times> y) = 0"
lp15@68465
   139
    by simp
lp15@68465
   140
  also have "... \<longleftrightarrow> (norm x * norm y)\<^sup>2 = (x \<bullet> y)\<^sup>2"
lp15@68465
   141
    using norm_cross [of x y] by (auto simp: power_mult_distrib)
lp15@68465
   142
  also have "... \<longleftrightarrow> \<bar>x \<bullet> y\<bar> = norm x * norm y"
lp15@68465
   143
    using power2_eq_iff
lp15@68465
   144
    by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def) 
lp15@68465
   145
  also have "... \<longleftrightarrow> collinear {0, x, y}"
lp15@68465
   146
    by (rule norm_cauchy_schwarz_equal)
lp15@68465
   147
  finally show ?thesis .
lp15@68465
   148
qed
lp15@68465
   149
nipkow@68902
   150
lemma  cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0"
lp15@68465
   151
  apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff)
lp15@68465
   152
  by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff)
lp15@68465
   153
nipkow@68902
   154
lemma  norm_and_cross_eq_0:
lp15@68465
   155
   "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs")
lp15@68465
   156
proof 
lp15@68465
   157
  assume ?lhs
lp15@68465
   158
  then show ?rhs
lp15@68465
   159
    by (metis cross_dot_cancel cross_zero_right inner_zero_right)
lp15@68465
   160
qed auto
lp15@68465
   161
nipkow@68902
   162
lemma  bilinear_cross: "bilinear(\<times>)"
lp15@68465
   163
  apply (auto simp add: bilinear_def linear_def)
lp15@68465
   164
  apply unfold_locales
lp15@68465
   165
  apply (simp add: cross_add_right)
lp15@68465
   166
  apply (simp add: cross_mult_right)
lp15@68465
   167
  apply (simp add: cross_add_left)
lp15@68465
   168
  apply (simp add: cross_mult_left)
lp15@68465
   169
  done
lp15@68465
   170
immler@69683
   171
subsection   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
lp15@68465
   172
nipkow@68902
   173
lemma  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
lp15@68465
   174
  apply (simp add: vec_eq_iff   )
lp15@68465
   175
  apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps)
lp15@68465
   176
  done
lp15@68465
   177
immler@69681
   178
lemma  cross_orthogonal_matrix:
lp15@68465
   179
  assumes "orthogonal_matrix A"
lp15@68465
   180
  shows "(A *v x) \<times> (A *v y) = det A *\<^sub>R (A *v (x \<times> y))"
immler@69681
   181
proof -
lp15@68465
   182
  have "mat 1 = transpose (A ** transpose A)"
lp15@68465
   183
    by (metis (no_types) assms orthogonal_matrix_def transpose_mat)
lp15@68465
   184
  then show ?thesis
lp15@68465
   185
    by (metis (no_types) vector_matrix_mul_rid vector_transpose_matrix cross_matrix_mult matrix_vector_mul_assoc matrix_vector_mult_scaleR)
lp15@68465
   186
qed
lp15@68465
   187
nipkow@68902
   188
lemma  cross_rotation_matrix: "rotation_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) =  A *v (x \<times> y)"
lp15@68465
   189
  by (simp add: rotation_matrix_def cross_orthogonal_matrix)
lp15@68465
   190
nipkow@68902
   191
lemma  cross_rotoinversion_matrix: "rotoinversion_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) = - A *v (x \<times> y)"
lp15@68465
   192
  by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc)
lp15@68465
   193
immler@69681
   194
lemma  cross_orthogonal_transformation:
lp15@68465
   195
  assumes "orthogonal_transformation f"
lp15@68465
   196
  shows   "(f x) \<times> (f y) = det(matrix f) *\<^sub>R f(x \<times> y)"
immler@69681
   197
proof -
lp15@68465
   198
  have orth: "orthogonal_matrix (matrix f)"
lp15@68465
   199
    using assms orthogonal_transformation_matrix by blast
lp15@68465
   200
  have "matrix f *v z = f z" for z
lp15@68465
   201
    using assms orthogonal_transformation_matrix by force
lp15@68465
   202
  with cross_orthogonal_matrix [OF orth] show ?thesis
lp15@68465
   203
    by simp
lp15@68465
   204
qed
lp15@68465
   205
nipkow@68902
   206
lemma  cross_linear_image:
lp15@68465
   207
   "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk>
lp15@68465
   208
           \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
lp15@68465
   209
  by (simp add: cross_orthogonal_transformation orthogonal_transformation)
lp15@68465
   210
immler@69683
   211
subsection \<open>Continuity\<close>
lp15@68465
   212
nipkow@68902
   213
lemma  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
lp15@68465
   214
  apply (subst continuous_componentwise)
lp15@68465
   215
  apply (clarsimp simp add: cross3_simps)
lp15@68465
   216
  apply (intro continuous_intros; simp)
lp15@68465
   217
  done
lp15@68465
   218
nipkow@68902
   219
lemma  continuous_on_cross:
lp15@68465
   220
  fixes f :: "'a::t2_space \<Rightarrow> real^3"
lp15@68465
   221
  shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
lp15@68465
   222
  by (simp add: continuous_on_eq_continuous_within continuous_cross)
lp15@68465
   223
lp15@68467
   224
unbundle no_cross3_syntax
lp15@68467
   225
lp15@68465
   226
end
lp15@68465
   227