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