31 notation Product_Type.Times (infixr "\<times>" 80) |
31 notation Product_Type.Times (infixr "\<times>" 80) |
32 end |
32 end |
33 |
33 |
34 unbundle cross3_syntax |
34 unbundle cross3_syntax |
35 |
35 |
36 subsection%important\<open> Basic lemmas.\<close> |
36 subsection%important\<open> Basic lemmas\<close> |
37 |
37 |
38 lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps |
38 lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps |
39 |
39 |
40 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" |
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" |
41 by (simp_all add: orthogonal_def cross3_simps) |
41 by (simp_all add: orthogonal_def cross3_simps) |
42 |
42 |
43 lemma%unimportant orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y" |
43 lemma orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y" |
44 "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x" |
44 "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x" |
45 by (simp_all add: orthogonal_def dot_cross_self) |
45 by (simp_all add: orthogonal_def dot_cross_self) |
46 |
46 |
47 lemma%unimportant cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3" |
47 lemma cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3" |
48 by (simp_all add: cross3_simps) |
48 by (simp_all add: cross3_simps) |
49 |
49 |
50 lemma%unimportant cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3" |
50 lemma cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3" |
51 by (simp add: cross3_simps) |
51 by (simp add: cross3_simps) |
52 |
52 |
53 lemma%unimportant cross_refl [simp]: "x \<times> x = 0" for x::"real^3" |
53 lemma cross_refl [simp]: "x \<times> x = 0" for x::"real^3" |
54 by (simp add: cross3_simps) |
54 by (simp add: cross3_simps) |
55 |
55 |
56 lemma%unimportant cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3" |
56 lemma cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3" |
57 by (simp add: cross3_simps) |
57 by (simp add: cross3_simps) |
58 |
58 |
59 lemma%unimportant cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3" |
59 lemma cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3" |
60 by (simp add: cross3_simps) |
60 by (simp add: cross3_simps) |
61 |
61 |
62 lemma%unimportant cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3" |
62 lemma cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3" |
63 by (simp add: cross3_simps) |
63 by (simp add: cross3_simps) |
64 |
64 |
65 lemma%unimportant cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3" |
65 lemma cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3" |
66 by (simp add: cross3_simps) |
66 by (simp add: cross3_simps) |
67 |
67 |
68 lemma%unimportant cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3" |
68 lemma cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3" |
69 by (simp add: cross3_simps) |
69 by (simp add: cross3_simps) |
70 |
70 |
71 lemma%unimportant cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3" |
71 lemma cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3" |
72 by (simp add: cross3_simps) |
72 by (simp add: cross3_simps) |
73 |
73 |
74 lemma%unimportant left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3" |
74 lemma left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3" |
75 by (simp add: cross3_simps) |
75 by (simp add: cross3_simps) |
76 |
76 |
77 lemma%unimportant right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3" |
77 lemma right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3" |
78 by (simp add: cross3_simps) |
78 by (simp add: cross3_simps) |
79 |
79 |
80 hide_fact (open) left_diff_distrib right_diff_distrib |
80 hide_fact (open) left_diff_distrib right_diff_distrib |
81 |
81 |
82 lemma%important Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3" |
82 lemma%important Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3" |
83 by%unimportant (simp add: cross3_simps) |
83 by%unimportant (simp add: cross3_simps) |
84 |
84 |
85 lemma%important Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z" |
85 lemma%important Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z" |
86 by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3) |
86 by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3) |
87 |
87 |
88 lemma%unimportant cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x" |
88 lemma cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x" |
89 by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) |
89 by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) |
90 |
90 |
91 lemma%unimportant cross_components: |
91 lemma cross_components: |
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" |
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" |
93 by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) |
93 by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) |
94 |
94 |
95 lemma%unimportant cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)" |
95 lemma cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)" |
96 "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)" |
96 "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)" |
97 "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)" |
97 "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)" |
98 using exhaust_3 |
98 using exhaust_3 |
99 by (force simp add: axis_def cross3_simps)+ |
99 by (force simp add: axis_def cross3_simps)+ |
100 |
100 |
101 lemma%unimportant cross_basis_nonzero: |
101 lemma cross_basis_nonzero: |
102 "u \<noteq> 0 \<Longrightarrow> ~(u \<times> axis 1 1 = 0) \<or> ~(u \<times> axis 2 1 = 0) \<or> ~(u \<times> axis 3 1 = 0)" |
102 "u \<noteq> 0 \<Longrightarrow> ~(u \<times> axis 1 1 = 0) \<or> ~(u \<times> axis 2 1 = 0) \<or> ~(u \<times> axis 3 1 = 0)" |
103 by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3) |
103 by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3) |
104 |
104 |
105 lemma%unimportant cross_dot_cancel: |
105 lemma cross_dot_cancel: |
106 fixes x::"real^3" |
106 fixes x::"real^3" |
107 assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0" |
107 assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0" |
108 shows "y = z" |
108 shows "y = z" |
109 proof - |
109 proof - |
110 have "x \<bullet> x \<noteq> 0" |
110 have "x \<bullet> x \<noteq> 0" |
114 by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff) |
114 by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff) |
115 then show ?thesis |
115 then show ?thesis |
116 using eq_iff_diff_eq_0 by blast |
116 using eq_iff_diff_eq_0 by blast |
117 qed |
117 qed |
118 |
118 |
119 lemma%unimportant norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2" |
119 lemma norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2" |
120 unfolding power2_norm_eq_inner power_mult_distrib |
120 unfolding power2_norm_eq_inner power_mult_distrib |
121 by (simp add: cross3_simps power2_eq_square) |
121 by (simp add: cross3_simps power2_eq_square) |
122 |
122 |
123 lemma%unimportant dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])" |
123 lemma dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])" |
124 by (simp add: cross3_simps) |
124 by (simp add: cross3_simps) |
125 |
125 |
126 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" |
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" |
127 using exhaust_3 by (force simp add: cross3_simps) |
127 using exhaust_3 by (force simp add: cross3_simps) |
128 |
128 |
129 lemma%important dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)" |
129 lemma%important dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)" |
130 by%unimportant (force simp add: cross3_simps) |
130 by%unimportant (force simp add: cross3_simps) |
131 |
131 |
132 lemma%unimportant norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2" |
132 lemma norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2" |
133 unfolding power2_norm_eq_inner power_mult_distrib |
133 unfolding power2_norm_eq_inner power_mult_distrib |
134 by (simp add: cross3_simps power2_eq_square) |
134 by (simp add: cross3_simps power2_eq_square) |
135 |
135 |
136 lemma%important cross_eq_0: "x \<times> y = 0 \<longleftrightarrow> collinear{0,x,y}" |
136 lemma%important cross_eq_0: "x \<times> y = 0 \<longleftrightarrow> collinear{0,x,y}" |
137 proof%unimportant - |
137 proof%unimportant - |
145 also have "... \<longleftrightarrow> collinear {0, x, y}" |
145 also have "... \<longleftrightarrow> collinear {0, x, y}" |
146 by (rule norm_cauchy_schwarz_equal) |
146 by (rule norm_cauchy_schwarz_equal) |
147 finally show ?thesis . |
147 finally show ?thesis . |
148 qed |
148 qed |
149 |
149 |
150 lemma%unimportant cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0" |
150 lemma cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0" |
151 apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff) |
151 apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff) |
152 by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff) |
152 by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff) |
153 |
153 |
154 lemma%unimportant norm_and_cross_eq_0: |
154 lemma norm_and_cross_eq_0: |
155 "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs") |
155 "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs") |
156 proof |
156 proof |
157 assume ?lhs |
157 assume ?lhs |
158 then show ?rhs |
158 then show ?rhs |
159 by (metis cross_dot_cancel cross_zero_right inner_zero_right) |
159 by (metis cross_dot_cancel cross_zero_right inner_zero_right) |
160 qed auto |
160 qed auto |
161 |
161 |
162 lemma%unimportant bilinear_cross: "bilinear(\<times>)" |
162 lemma bilinear_cross: "bilinear(\<times>)" |
163 apply (auto simp add: bilinear_def linear_def) |
163 apply (auto simp add: bilinear_def linear_def) |
164 apply unfold_locales |
164 apply unfold_locales |
165 apply (simp add: cross_add_right) |
165 apply (simp add: cross_add_right) |
166 apply (simp add: cross_mult_right) |
166 apply (simp add: cross_mult_right) |
167 apply (simp add: cross_add_left) |
167 apply (simp add: cross_add_left) |
168 apply (simp add: cross_mult_left) |
168 apply (simp add: cross_mult_left) |
169 done |
169 done |
170 |
170 |
171 subsection%important \<open>Preservation by rotation, or other orthogonal transformation up to sign.\<close> |
171 subsection%important \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close> |
172 |
172 |
173 lemma%unimportant cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)" |
173 lemma cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)" |
174 apply (simp add: vec_eq_iff ) |
174 apply (simp add: vec_eq_iff ) |
175 apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps) |
175 apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps) |
176 done |
176 done |
177 |
177 |
178 lemma%important cross_orthogonal_matrix: |
178 lemma%important cross_orthogonal_matrix: |
201 using assms orthogonal_transformation_matrix by force |
201 using assms orthogonal_transformation_matrix by force |
202 with cross_orthogonal_matrix [OF orth] show ?thesis |
202 with cross_orthogonal_matrix [OF orth] show ?thesis |
203 by simp |
203 by simp |
204 qed |
204 qed |
205 |
205 |
206 lemma%unimportant cross_linear_image: |
206 lemma cross_linear_image: |
207 "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk> |
207 "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk> |
208 \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)" |
208 \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)" |
209 by (simp add: cross_orthogonal_transformation orthogonal_transformation) |
209 by (simp add: cross_orthogonal_transformation orthogonal_transformation) |
210 |
210 |
211 subsection%unimportant \<open>Continuity\<close> |
211 subsection%unimportant \<open>Continuity\<close> |
212 |
212 |
213 lemma%unimportant continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))" |
213 lemma continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))" |
214 apply (subst continuous_componentwise) |
214 apply (subst continuous_componentwise) |
215 apply (clarsimp simp add: cross3_simps) |
215 apply (clarsimp simp add: cross3_simps) |
216 apply (intro continuous_intros; simp) |
216 apply (intro continuous_intros; simp) |
217 done |
217 done |
218 |
218 |
219 lemma%unimportant continuous_on_cross: |
219 lemma continuous_on_cross: |
220 fixes f :: "'a::t2_space \<Rightarrow> real^3" |
220 fixes f :: "'a::t2_space \<Rightarrow> real^3" |
221 shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))" |
221 shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))" |
222 by (simp add: continuous_on_eq_continuous_within continuous_cross) |
222 by (simp add: continuous_on_eq_continuous_within continuous_cross) |
223 |
223 |
224 unbundle no_cross3_syntax |
224 unbundle no_cross3_syntax |