1 (* ========================================================================= *)
\r
2 (* Formalization of Electromagnetic Optics *)
\r
4 (* (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)
\r
5 (* Hardware Verification Group, *)
\r
6 (* Concordia University *)
\r
8 (* Contact: <s_khanaf@encs.concordia.ca> *)
\r
9 (* <vincent@encs.concordia.ca> *)
\r
11 (* Extentions of the vector library. *)
\r
12 (* ========================================================================= *)
\r
15 prioritize_vector ();;
\r
17 (** Additions to euclidean space *)
\r
19 let [ORTHOGONAL_RZERO;ORTHOGONAL_RMUL;ORTHOGONAL_RNEG;ORTHOGONAL_RADD;
\r
20 ORTHOGONAL_RSUB;ORTHOGONAL_LZERO;ORTHOGONAL_LMUL;ORTHOGONAL_LNEG;
\r
21 ORTHOGONAL_LADD;ORTHOGONAL_LSUB] =
\r
22 CONJUNCTS ORTHOGONAL_CLAUSES;;
\r
24 let NON_VEC0 = prove
\r
25 (`!x:real^N. ~(x=vec 0) <=> ?i. 1 <= i /\ i <= dimindex(:N) /\ ~(x$i = &0)`,
\r
26 GEN_TAC THEN EQ_TAC THEN SIMP_TAC[vec;CART_EQ;LAMBDA_BETA]
\r
27 THEN ASM_MESON_TAC[]);;
\r
29 let NON_VEC0_DIM3 = prove
\r
30 (`!x:real^3. ~(x=vec 0) <=> ~(x$1= &0) \/ ~(x$2= &0) \/ ~(x$3= &0)`,
\r
31 REWRITE_TAC[NON_VEC0;DIMINDEX_3]
\r
32 THEN MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> i = 1 \/ i = 2 \/ i = 3`]);;
\r
34 let ORTHOGONAL_SQR_NORM = prove
\r
35 (`!x y:real^N. orthogonal (x-y) y ==> x dot x = (x-y) dot (x-y) + y dot y`,
\r
36 REWRITE_TAC[orthogonal] THEN REPEAT STRIP_TAC
\r
37 THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)
\r
38 [VECTOR_ARITH `x dot x = (x-y) dot (x-y) + y dot y + &2 * (x-y) dot y`]
\r
39 THEN ASM_REWRITE_TAC[REAL_MUL_RZERO;REAL_ADD_RID]);;
\r
41 let COLLINEAR_VEC0 = prove
\r
42 (`!s:real^N->bool. collinear s /\ vec 0 IN s ==> ?u. !x. x IN s
\r
44 REWRITE_TAC[collinear] THEN REPEAT (STRIP_TAC ORELSE EXISTS_TAC `u:real^N`)
\r
45 THEN ASM_MESON_TAC[VECTOR_SUB_RZERO]);;
\r
47 let CROSS_NORM_ORTHOGONAL = prove
\r
48 (`!x y. orthogonal x y ==> norm (x cross y) = norm x * norm y`,
\r
49 ONCE_REWRITE_TAC[GSYM (REWRITE_RULE[GSYM REAL_ABS_REFL] NORM_POS_LE)]
\r
50 THEN SIMP_TAC[GSYM REAL_ABS_MUL;REAL_EQ_SQUARE_ABS;GSYM NORM_CROSS_DOT;
\r
51 orthogonal;REAL_POW_2]
\r
52 THEN REAL_ARITH_TAC);;
\r
55 let COLLINEAR_DEPENDENT = prove
\r
56 (`!x y:real^N. ~(x=y) /\ collinear {vec 0,x,y} ==> dependent {x,y}`,
\r
57 REWRITE_TAC[collinear;dependent;IN_INSERT;IN_SING] THEN REPEAT STRIP_TAC
\r
58 THEN ASM_CASES_TAC `x=vec 0:real^N`
\r
59 THENL ON_FIRST_GOAL (ASM_MESON_TAC[SPAN_0])
\r
60 THEN ASM_CASES_TAC `y=vec 0:real^N`
\r
61 THENL ON_FIRST_GOAL (ASM_MESON_TAC[SPAN_0])
\r
62 THEN SUBGOAL_THEN `?c. x = c % y :real^N` STRIP_ASSUME_TAC THENL [
\r
63 FIRST_ASSUM (fun x -> MAP_EVERY (STRIP_ASSUME_TAC o
\r
64 REWRITE_RULE[IN_INSERT;IN_SING;VECTOR_SUB_RZERO] o C SPECL x) [
\r
65 [`x:real^N`;`vec 0:real^N`]; [`y:real^N`;`vec 0:real^N`]])
\r
66 THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC;VECTOR_MUL_RCANCEL]
\r
67 THEN SUBGOAL_THEN `~(c'= &0)` ASSUME_TAC
\r
68 THENL [ ASM_MESON_TAC[VECTOR_MUL_LZERO]; EXISTS_TAC `c/c':real`
\r
69 THEN ASM_SIMP_TAC[REAL_DIV_RMUL] ];
\r
70 SUBGOAL_TAC "" `~(y=c%y:real^N)` [ASM_MESON_TAC[]]
\r
71 THEN EXISTS_TAC `c%y:real^N`
\r
72 THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE]
\r
73 THEN MESON_TAC[SUBSPACE_MUL;SUBSET;SPAN_INC;IN_SING;SUBSPACE_SPAN]
\r
76 let ORTHOGONAL_DIFFERENT = prove
\r
77 (`!x y:real^N. orthogonal x y /\ ~(x=vec 0) /\ ~(y=vec 0) ==> ~(x=y)`,
\r
78 REWRITE_TAC[orthogonal] THEN MESON_TAC[DOT_EQ_0]);;
\r
80 let ORTHOGONAL_NON_COLLINEAR = prove
\r
81 (`!x y:real^N. orthogonal x y /\ ~(x=vec 0) /\ ~(y=vec 0)
\r
82 ==> ~(collinear {vec 0,x,y})`,
\r
84 THEN SUBGOAL_THEN `independent {x,y:real^N}` ASSUME_TAC THENL [
\r
85 MATCH_MP_TAC PAIRWISE_ORTHOGONAL_INDEPENDENT
\r
86 THEN REWRITE_TAC[pairwise;IN_INSERT;IN_SING]
\r
87 THEN ASM_MESON_TAC[ORTHOGONAL_SYM];
\r
88 POP_ASSUM (MP_TAC o REWRITE_RULE[independent])
\r
89 THEN REWRITE_TAC[] THEN MATCH_MP_TAC COLLINEAR_DEPENDENT
\r
90 THEN ASM_SIMP_TAC[ORTHOGONAL_DIFFERENT]
\r
93 (* NORMALIZING VECTORS *)
\r
95 let unit = new_definition `unit v = inv(norm v) % v`;;
\r
97 let UNIT_THM = prove
\r
98 (`!v. ~(v = vec 0) ==> norm(unit v) = &1`,
\r
99 SIMP_TAC[unit;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM;GSYM NORM_EQ_0;
\r
102 let UNIT_INTRO = prove
\r
103 (`!v. ~(v = vec 0) ==> v = norm v % unit v`,
\r
104 SIMP_TAC[unit;VECTOR_MUL_ASSOC;GSYM NORM_EQ_0;REAL_MUL_RINV;
\r
107 let UNIT_ELIM = GSYM UNIT_INTRO;;
\r
109 let UNIT_ZERO = prove
\r
110 (`unit(vec 0) = vec 0`, REWRITE_TAC[unit;VECTOR_MUL_RZERO]);;
\r
112 let UNIT_EQ_ZERO = prove
\r
113 (`!v. unit v = vec 0 <=> v = vec 0`,
\r
114 REWRITE_TAC[unit;VECTOR_MUL_EQ_0;REAL_INV_EQ_0;NORM_EQ_0]);;
\r
116 let UNIT_UNIT = prove
\r
117 (`!v. ~(v = vec 0) ==> unit (unit v) = unit v`,
\r
118 SIMP_TAC[unit;UNIT_THM;REAL_INV_1;VECTOR_MUL_LID]);;
\r
120 let UNIT_DOT_UNIT_SELF = prove
\r
121 (`!v. ~(v = vec 0) ==> unit v dot unit v = &1`,
\r
122 SIMP_TAC[GSYM NORM_EQ_1;UNIT_THM]);;
\r
124 let DOT_UNIT_SELF = prove
\r
125 (`!v. ~(v=vec 0) ==> v dot unit v = norm v`,
\r
126 SIMP_TAC[MESON[UNIT_INTRO] `!v. ~(v = vec 0) ==>
\r
127 v dot unit v = (norm v % unit v) dot unit v`;DOT_LMUL;UNIT_DOT_UNIT_SELF;
\r
130 let ORTHOGONAL_UNIT = prove
\r
131 (`!x y:real^N. (orthogonal x (unit y) <=> orthogonal x y)
\r
132 /\ (orthogonal (unit x) y <=> orthogonal x y)`,
\r
136 RULE_ASSUM_TAC (REWRITE_RULE[NORM_EQ_0]) THEN ASM_REWRITE_TAC[UNIT_ZERO];
\r
137 ASM_SIMP_TAC[unit;orthogonal;DOT_RMUL;DOT_LMUL;REAL_ENTIRE;REAL_INV_EQ_0]
\r
140 REPEAT GEN_TAC THEN CONJ_TAC
\r
141 THENL [ common `norm (y:real^N) = &0`; common `norm (x:real^N) = &0` ]);;
\r
143 let ORTHOGONAL_RUNIT = prove
\r
144 (`!x y:real^N. orthogonal x (unit y) <=> orthogonal x y`,
\r
145 MESON_TAC[ORTHOGONAL_UNIT]);;
\r
147 let ORTHOGONAL_LUNIT = prove
\r
148 (`!x y:real^N. orthogonal (unit x) y <=> orthogonal x y`,
\r
149 MESON_TAC[ORTHOGONAL_UNIT]);;
\r
151 let ORTHOGONAL_LRUNIT = prove
\r
152 (`!x y:real^N. orthogonal (unit x) (unit y) <=> orthogonal x y`,
\r
153 MESON_TAC[ORTHOGONAL_UNIT]);;
\r
155 let COLLINEAR_UNIT = prove
\r
156 (`!x y:real^N. collinear {vec 0,x,y} <=> collinear {vec 0,unit x,unit y}`,
\r
157 REPEAT (STRIP_TAC ORELSE EQ_TAC)
\r
158 THEN ASM_CSQ_THEN (REWRITE_RULE[GSYM IMP_IMP] COLLINEAR_VEC0)
\r
159 (STRIP_ASSUME_TAC o REWRITE_RULE[IN_INSERT;IN_SING])
\r
160 THEN ASM_CSQ_THEN ~remove:true (MESON[] `(!x. x=a \/ x=b \/ x=c ==> p x) ==>
\r
161 p b /\ p c`) STRIP_ASSUME_TAC
\r
164 MAP_EVERY ASM_CASES_TAC [`x=vec 0:real^N`;`y=vec 0:real^N`]
\r
165 THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)
\r
166 THEN REWRITE_TAC[INSERT_AC;COLLINEAR_SING;COLLINEAR_2]
\r
167 THEN SUBGOAL_THEN `collinear {x:real^N, y, vec 0}
\r
168 <=> collinear {norm x % unit x, norm y % unit y, vec 0}`
\r
169 (SINGLE REWRITE_TAC)
\r
170 THENL ON_FIRST_GOAL (ASM_SIMP_TAC[GSYM UNIT_INTRO])
\r
172 THEN REWRITE_TAC[collinear;IN_INSERT;IN_SING]
\r
173 THEN EXISTS_TAC `u:real^N` THEN REPEAT STRIP_TAC
\r
174 THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC;VECTOR_SUB_RZERO;VECTOR_SUB_LZERO;
\r
175 VECTOR_NEG_0;GSYM VECTOR_MUL_LNEG;GSYM VECTOR_SUB_RDISTRIB]
\r
176 THEN MESON_TAC[VECTOR_MUL_LZERO]);;
\r
178 let DOT_RUNIT_POS,DOT_LUNIT_POS = CONJ_PAIR(prove
\r
179 (`(!x y. &0 < x dot (unit y) <=> &0 < x dot y)
\r
180 /\ (!x y. &0 < (unit x) dot y <=> &0 < x dot y)`,
\r
181 REWRITE_TAC[unit;DOT_RMUL;DOT_LMUL;REAL_MUL_POS_LT;REAL_LT_INV_EQ;
\r
182 NORM_POS_LT;REWRITE_RULE[REAL_INV_NEG;REAL_NEG_GT0]
\r
183 (SPEC `--x:real` REAL_LT_INV_EQ);
\r
184 REWRITE_RULE[REWRITE_RULE[MESON[]`(p<=> ~q) <=> (q<=> ~p)`] real_lt]
\r
186 THEN MESON_TAC[DOT_RZERO;DOT_LZERO;REAL_LT_REFL]));;
\r
188 let DOT_RUNIT_EQ0,DOT_LUNIT_EQ0 = CONJ_PAIR(prove
\r
189 (`(!x y. x dot (unit y) = &0 <=> x dot y = &0)
\r
190 /\ (!x y. (unit x) dot y = &0 <=> x dot y = &0)`,
\r
191 REWRITE_TAC[GSYM orthogonal;ORTHOGONAL_LUNIT;ORTHOGONAL_RUNIT]));;
\r
193 let DOT_RUNIT_LT0,DOT_LUNIT_LT0 = CONJ_PAIR(prove
\r
194 (`(!x y. x dot (unit y) < &0 <=> x dot y < &0)
\r
195 /\ (!x y. (unit x) dot y < &0 <=> x dot y < &0)`,
\r
196 REWRITE_TAC[real_lt;MESON[] `(~p <=> ~q) <=> (p <=> q)`]
\r
197 THEN REWRITE_TAC[REAL_LE_LT]
\r
198 THEN MESON_TAC[DOT_RUNIT_EQ0;DOT_LUNIT_EQ0;DOT_RUNIT_POS;DOT_LUNIT_POS]));;
\r
200 let DOT_RUNIT_LE0,DOT_LUNIT_LE0 = CONJ_PAIR(prove
\r
201 (`(!x y. x dot (unit y) <= &0 <=> x dot y <= &0)
\r
202 /\ (!x y. (unit x) dot y <= &0 <=> x dot y <= &0)`,
\r
203 MESON_TAC[REAL_LE_LT;DOT_RUNIT_LT0;DOT_LUNIT_LT0;DOT_RUNIT_EQ0;
\r
206 let DOT_RUNIT_GE0,DOT_LUNIT_GE0 = CONJ_PAIR(prove
\r
207 (`(!x y. &0 <= x dot (unit y) <=> &0 <= x dot y)
\r
208 /\ (!x y. &0 <= (unit x) dot y <=> &0 <= x dot y)`,
\r
209 REWRITE_TAC[REAL_LE_LT]
\r
210 THEN MESON_TAC[DOT_RUNIT_POS;DOT_LUNIT_POS;DOT_RUNIT_EQ0;DOT_LUNIT_EQ0]));;
\r
212 let DOT_RUNIT_EQ = prove
\r
213 (`!x y z:real^N. x dot (unit z) = y dot (unit z) <=> x dot z = y dot z`,
\r
214 REPEAT GEN_TAC THEN ASM_CASES_TAC `z=vec 0:real^N`
\r
215 THEN ASM_REWRITE_TAC[unit;DOT_RMUL;REAL_EQ_MUL_LCANCEL;REAL_INV_EQ_0;
\r
216 NORM_EQ_0;DOT_RZERO]);;
\r
218 let DOT_LUNIT_EQ = prove
\r
219 (`!x y z:real^N. (unit z) dot x = (unit z) dot y <=> z dot x = z dot y`,
\r
220 REPEAT GEN_TAC THEN ASM_CASES_TAC `z=vec 0:real^N`
\r
221 THEN ASM_REWRITE_TAC[unit;DOT_LMUL;REAL_EQ_MUL_LCANCEL;REAL_INV_EQ_0;
\r
222 NORM_EQ_0;DOT_LZERO]);;
\r
225 (* CONNECTION BETWEEN SPANS AND PLANES *)
\r
227 new_type_abbrev("point",`:real^3`);;
\r
228 new_type_abbrev("plane",`:point->bool`);;
\r
230 let PLANE_NON_EMPTY = prove
\r
231 (`!p:plane. plane p ==> ~(p={})`,
\r
232 REWRITE_TAC[plane;GSYM MEMBER_NOT_EMPTY] THEN REPEAT STRIP_TAC
\r
233 THEN EXISTS_TAC `u:point`
\r
234 THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (REWRITE_RULE[SUBSET] HULL_SUBSET)
\r
237 let is_plane_basis = new_definition
\r
238 `is_plane_basis s p <=>
\r
239 ?u v:real^3. s = {u,v} /\ ~(collinear {vec 0,u,v}) /\ !pt:point. pt IN p
\r
240 ==> !pt':point. pt' IN p <=> ?a b:real. pt' = pt + a % u + b % v`;;
\r
242 (* That theorem is (one of) the last which makes use of the affine definition of `plane` *)
\r
243 let EXISTS_PLANE_BASIS = prove
\r
244 (`!p. plane p ==> ?b. is_plane_basis b p`,
\r
246 THEN DISCH_THEN (fun x ->
\r
247 STRIP_ASSUME_TAC (REWRITE_RULE[plane;AFFINE_HULL_3] x)
\r
248 THEN STRIP_ASSUME_TAC (MATCH_MP (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]
\r
249 PLANE_NON_EMPTY) x))
\r
250 THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[is_plane_basis] THEN DISCH_TAC
\r
251 THEN MAP_EVERY EXISTS_TAC [`{v-u,w-u:real^3}`;`v-u:real^3`; `w-u:real^3`]
\r
252 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
\r
254 ASM_MESON_TAC[INSERT_AC;COLLINEAR_3];
\r
255 POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC
\r
256 THEN EQ_TAC THEN STRIP_TAC
\r
258 RULE_ASSUM_TAC (REWRITE_RULE[REAL_ARITH `x+y+z= &1 <=> x= &1-y-z`])
\r
259 THEN MAP_EVERY EXISTS_TAC [`v''-v':real`; `w''-w':real`]
\r
260 THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;
\r
261 MAP_EVERY EXISTS_TAC [`u'-a-b:real`;`v'+a:real`;`w'+b:real`]
\r
265 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN VECTOR_ARITH_TAC]
\r
269 let BASIS_NON_NULL = prove
\r
270 (`!p. plane p ==> !b. is_plane_basis b p ==> !u. u IN b ==> ~(u=vec 0)`,
\r
271 REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC
\r
272 THEN SUBGOAL_THEN `(u':real^3) IN {u,v}` MP_TAC
\r
273 THENL ON_FIRST_GOAL (ASM_MESON_TAC[])
\r
274 THEN REWRITE_TAC[IN_INSERT;IN_SING]
\r
275 THEN ASM_MESON_TAC[INSERT_AC;COLLINEAR_2]);;
\r
277 let PAIR_SETS_EQ = prove
\r
278 (`!x y z t. {x,y} = {z,t} ==> (x=z /\ y=t) \/ (x=t /\ y=z)`,
\r
281 let NON_COLLINEAR3_IMPLIES_DIFFERENT = prove
\r
282 (`!x y z. ~(collinear {x,y,z}) ==> ~(x=y) /\ ~(y=z) /\ ~(x=z)`,
\r
283 MESON_TAC[COLLINEAR_2;INSERT_AC]);;
\r
285 let BASIS_DIFFERENT = prove
\r
286 (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==> ~(u=v)`,
\r
287 REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC
\r
288 THEN ASM_MESON_TAC[PAIR_SETS_EQ;NON_COLLINEAR3_IMPLIES_DIFFERENT]);;
\r
290 let UNIT_OF_BASIS_IS_BASIS = prove
\r
291 (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==> is_plane_basis {unit u,unit v} p`,
\r
292 REPEAT STRIP_TAC THEN REWRITE_TAC[is_plane_basis]
\r
293 THEN MAP_EVERY EXISTS_TAC [`unit u:real^3`; `unit v:real^3`]
\r
296 (DISTRIB [ASSUME_TAC;STRIP_ASSUME_TAC o REWRITE_RULE[is_plane_basis]])
\r
297 THEN ASM_REWRITE_TAC[GSYM COLLINEAR_UNIT]
\r
298 THEN ASM_CSQ_THEN ~remove:true PAIR_SETS_EQ STRIP_ASSUME_TAC
\r
299 THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)
\r
300 THEN ASM_CSQ_THEN BASIS_NON_NULL (C ASM_CSQ_THEN (STRIP_ASSUME_TAC
\r
301 o REWRITE_RULE[IN_INSERT;IN_SING;
\r
302 MESON[]`(!u. u=a \/ u=b ==> p u) <=> p a /\ p b`]))
\r
304 THEN DISCH_THEN (fun x -> FIRST_X_ASSUM (ASSUME_TAC o C MATCH_MP x))
\r
305 THEN ASM_REWRITE_TAC[unit;VECTOR_MUL_ASSOC]
\r
306 THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[]
\r
308 MAP_EVERY EXISTS_TAC [`a*norm(u':real^3)`;`b*norm(v':real^3)`]
\r
309 THEN RULE_ASSUM_TAC (REWRITE_RULE[GSYM NORM_EQ_0])
\r
310 THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC;REAL_MUL_RINV] THEN VECTOR_ARITH_TAC;
\r
312 MAP_EVERY EXISTS_TAC [`b*norm(v':real^3)`;`a*norm(u':real^3)`]
\r
313 THEN RULE_ASSUM_TAC (REWRITE_RULE[GSYM NORM_EQ_0])
\r
314 THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC;REAL_MUL_RINV] THEN VECTOR_ARITH_TAC;
\r
315 MESON_TAC[VECTOR_ADD_AC];
\r
318 (* This theorem makes the connection between the (affine) notion of plane and the (vector) notion of span.
\r
319 * From now on, we can generally rely only on this result to reason about the spanning set of a plane.
\r
321 let PLANE_AS_SPAN = prove
\r
322 (`!p. plane p ==> !b. is_plane_basis b p ==> !pt:point. pt IN p
\r
323 ==> p = { pt + y | y IN span b }`,
\r
324 REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC
\r
325 THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;SPAN_2;UNIV]
\r
326 THEN ASM_MESON_TAC[]);;
\r
328 let PLANE_SPAN = prove
\r
329 (`!p. plane p ==> !b. is_plane_basis b p ==> !pt:point. pt IN p
\r
330 ==> { pt' - pt | pt' IN p } = span b`,
\r
331 REPEAT STRIP_TAC THEN ASM_CSQ_THEN PLANE_AS_SPAN (C ASM_CSQ_THEN (C
\r
332 ASM_CSQ_THEN (SINGLE (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)))))
\r
333 THEN REWRITE_TAC[IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC
\r
335 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH `(x + y)-x = y:real^N`];
\r
336 DISCH_TAC THEN EXISTS_TAC `x+pt:real^3` THEN REWRITE_TAC (map VECTOR_ARITH
\r
337 [`(x + y) - y = x:real^N`; `x+z=z+y <=> x=y:real^N`]) THEN ASM_MESON_TAC[]
\r
340 let ALL_BASIS_SAME_SPAN = prove
\r
341 (`!p. plane p ==> !b1. is_plane_basis b1 p ==> !b2. is_plane_basis b2 p
\r
342 ==> span b1 = span b2`,
\r
344 THEN ASM_CSQ_THEN PLANE_SPAN (fun x ->
\r
345 ASM_CSQ_THEN ~match_:false (SPEC `b1:real^3->bool` x) ASSUME_TAC
\r
346 THEN ASM_CSQ_THEN (SPEC `b2:real^3->bool` x) ASSUME_TAC)
\r
347 THEN ASM_MESON_TAC[PLANE_NON_EMPTY;MEMBER_NOT_EMPTY]);;
\r
349 let PLANE_SUBSPACE = prove
\r
350 (`!p. plane p ==> !pt:point. pt IN p ==> subspace { pt' - pt | pt' IN p }`,
\r
351 REPEAT STRIP_TAC THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC
\r
352 THEN ASM_SIMP_TAC[PLANE_SPAN;SUBSPACE_SPAN]);;
\r
354 let PLANE_SING = prove
\r
355 (`!x:real^N. ~(plane{x})`,
\r
356 REWRITE_TAC[plane;NOT_EXISTS_THM;MESON[] `~(A/\B) <=> (A ==> ~B)`]
\r
357 THEN REPEAT STRIP_TAC
\r
358 THEN ASM_CSQ_THEN NON_COLLINEAR3_IMPLIES_DIFFERENT ASSUME_TAC
\r
359 THEN MATCH_MP_TAC (SET_RULE `~(u=v:real^N) /\ u IN {x} /\ v IN {x} ==> F`)
\r
360 THEN ASM_REWRITE_TAC[]
\r
361 THEN CONJ_TAC THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);;
\r
363 let NON_COLLINEAR_INDEPENDENT = prove
\r
364 (`!x y:real^N. ~(collinear {vec 0,x,y}) ==> independent{x,y}`,
\r
365 MAP_EVERY (SINGLE ONCE_REWRITE_TAC) [independent;CONTRAPOS_THM;NOT_CLAUSES]
\r
366 THEN REPEAT GEN_TAC
\r
367 THEN ASM_CASES_TAC `x=y:real^N` THENL [
\r
368 ASM_REWRITE_TAC[INSERT_AC;COLLINEAR_2];
\r
369 REWRITE_TAC[dependent;IN_INSERT;IN_SING] THEN STRIP_TAC THENL
\r
370 let common main_var exist_list =
\r
372 THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE;SPAN_SING;IN_ELIM_THM;
\r
375 THEN REWRITE_TAC[collinear;IN_INSERT;IN_SING] THEN EXISTS_TAC main_var
\r
376 THEN REPEAT STRIP_TAC
\r
377 THENL map (fun t ->
\r
378 EXISTS_TAC t THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC) exist_list
\r
380 [ common `y:real^N`
\r
381 [`&0`;`--u:real`;`-- &1`;`u:real`;`&0`;`u- &1`;`&1`;`&1-u`;`&0`];
\r
383 [`&0`;`-- &1`;`--u:real`;`&1`;`&0`;`&1-u`;`u:real`;`u- &1`;`&0`]
\r
386 let DIM_OF_PLANE_SPAN = prove
\r
387 (`!p:plane. plane p ==> !b. is_plane_basis b p ==> dim (span b) = 2`,
\r
388 REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC
\r
389 THEN ASM_CSQ_THEN NON_COLLINEAR_INDEPENDENT ASSUME_TAC
\r
390 THEN ASM_CSQ_THEN NON_COLLINEAR3_IMPLIES_DIFFERENT ASSUME_TAC
\r
391 THEN SUBGOAL_THEN `{u,v:real^3} HAS_SIZE (dim (span {u,v}))` MP_TAC
\r
393 MATCH_MP_TAC BASIS_HAS_SIZE_DIM THEN ASM_REWRITE_TAC[];
\r
394 ASM_SIMP_TAC[HAS_SIZE;FINITE_INSERT;FINITE_EMPTY;CARD_CLAUSES;IN_INSERT;
\r
395 IN_SING;NOT_IN_EMPTY] THEN ARITH_TAC
\r
398 let DIM_OF_PLANE_SUBSPACE = prove
\r
399 (`!p. plane p ==> !pt:point. pt IN p ==> dim { pt' - pt | pt' IN p } = 2`,
\r
400 MESON_TAC[PLANE_SPAN;DIM_OF_PLANE_SPAN;EXISTS_PLANE_BASIS]);;
\r
402 let PLANE_SPAN_DECOMPOS = prove
\r
403 (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==>
\r
404 !x. x IN span {u,v} <=> ?a b. x = a % u + b % v`,
\r
405 REPEAT STRIP_TAC THEN POP_ASSUM (SINGLE REWRITE_TAC o GSYM)
\r
406 THEN REWRITE_TAC[SPAN_2;IN_ELIM_THM;UNIV]);;
\r
408 let units = new_definition `units = { x | norm x = &1 }`;;
\r
410 let IN_UNITS = prove
\r
411 (`!x. x IN units ==> norm x = &1`,
\r
412 REWRITE_TAC[units;IN_ELIM_THM]);;
\r
414 let is_normal_to_plane = new_definition
\r
415 `is_normal_to_plane (n:real^3) (p:plane) <=> ~(n=vec 0)
\r
416 /\ !b. is_plane_basis b p ==> !v. v IN (span b) ==> orthogonal v n`;;
\r
418 let IS_NORMAL_TO_PLANE_UNIT = prove
\r
419 (`!p n. is_normal_to_plane (unit n) p <=> is_normal_to_plane n p`,
\r
420 REWRITE_TAC[is_normal_to_plane;ORTHOGONAL_RUNIT;UNIT_EQ_ZERO]);;
\r
422 let EXISTS_NORMAL_OF_PLANE = prove
\r
423 (`!p:plane. plane p ==> ?n:real^3. is_normal_to_plane n p`,
\r
424 REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC
\r
425 THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS (CHOOSE_THEN (fun x ->
\r
426 MAP_EVERY STRIP_ASSUME_TAC [x;REWRITE_RULE[is_plane_basis] x]))
\r
427 THEN EXISTS_TAC `u cross v` THEN ASM_REWRITE_TAC[CROSS_EQ_0]
\r
428 THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
\r
429 THEN ASM_CSQ_THEN ALL_BASIS_SAME_SPAN (C (ASM_CSQ_THEN ~remove:true) (C
\r
430 ASM_CSQ_THEN (SINGLE REWRITE_TAC)))
\r
431 THEN ASM_REWRITE_TAC[SPAN_2;IN_ELIM_THM;UNIV]
\r
432 THEN REPEAT STRIP_TAC
\r
433 THEN ASM_REWRITE_TAC[orthogonal;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF]
\r
434 THEN SIMPLE_COMPLEX_ARITH_TAC);;
\r
436 let NORMAL_OF_PLANE_IS_NORMAL_TO_BASIS = prove
\r
437 (`!p. plane p ==> !b. is_plane_basis b p ==> !u. u IN b ==>
\r
438 !n. is_normal_to_plane n p ==> orthogonal u n`,
\r
439 MESON_TAC[is_normal_to_plane;SPAN_SUPERSET;]);;
\r
441 let NORMAL_OF_PLANE_NON_NULL = prove
\r
442 (`!p. plane p ==> !n. is_normal_to_plane n p ==> ~(n=vec 0)`,
\r
443 MESON_TAC[is_normal_to_plane]);;
\r
445 let NORMAL_OF_PLANE_IS_ORTHOGONAL_TO_SEGMENT = prove
\r
446 (`!p. plane p ==> !n. is_normal_to_plane n p
\r
447 ==> !pt1 pt2. pt1 IN p /\ pt2 IN p ==> orthogonal (pt1-pt2) n`,
\r
448 REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC
\r
449 THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC
\r
451 (fun x -> FIRST_X_ASSUM (MATCH_MP_TAC o C MATCH_MP x) THEN ASSUME_TAC x)
\r
452 THEN FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV is_plane_basis))
\r
453 THEN POP_ASSUM (C (ASM_CSQ_THEN ~remove:true) (fun x ->
\r
454 FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV x))))
\r
455 THEN ASM_REWRITE_TAC[SPAN_2;UNIV;IN_ELIM_THM;VECTOR_ARITH
\r
456 `(x+y+z)-x = y+z:real^N`]
\r
457 THEN MESON_TAC[]);;
\r
459 let DIM_OF_NORMAL_SPAN = prove
\r
460 (`!p:plane. plane p ==> !n. is_normal_to_plane n p ==> dim (span {n}) = 1`,
\r
461 REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC
\r
462 THEN SUBGOAL_THEN `{n:real^3} HAS_SIZE dim (span {n})` MP_TAC
\r
464 MATCH_MP_TAC BASIS_HAS_SIZE_DIM
\r
465 THEN REWRITE_TAC[independent;dependent;NOT_EXISTS_THM;
\r
466 MESON[] `~(p/\q) <=> p ==> ~q`;IN_SING]
\r
467 THEN GEN_TAC THEN DISCH_TAC
\r
468 THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE;SPAN_EMPTY;IN_SING];
\r
469 ASM_SIMP_TAC[HAS_SIZE;FINITE_INSERT;FINITE_EMPTY;CARD_CLAUSES;IN_INSERT;
\r
470 IN_SING;NOT_IN_EMPTY]
\r
473 let DIM_OF_ORTHOGONAL = prove
\r
474 (`!p. plane p ==> !b. is_plane_basis b p
\r
475 ==> dim {z:real^3 | !x. x IN span b ==> orthogonal z x} = 1`,
\r
478 `(:real^3) = { x+y
\r
479 | x IN span b /\ y IN {z:real^3 | !x. x IN span b ==> orthogonal z x}}`
\r
480 (ASSUME_TAC o REWRITE_RULE[DIM_UNIV;DIMINDEX_3] o
\r
481 AP_TERM `dim:(real^3->bool)->num`)
\r
482 THENL ON_FIRST_GOAL
\r
483 (REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ;SUBSET;UNIV;IN;IN_ELIM_THM]
\r
484 THEN MESON_TAC[ORTHOGONAL_SUBSPACE_DECOMP_EXISTS;IN])
\r
487 INTER {z:real^3 | !x. x IN span b ==> orthogonal z x} SUBSET {vec 0}`
\r
488 (ASSUME_TAC o GSYM o REWRITE_RULE[GSYM DIM_EQ_0])
\r
489 THENL ON_FIRST_GOAL
\r
490 (REWRITE_TAC[INTER;SUBSET;IN_SING;IN_ELIM_THM]
\r
491 THEN MESON_TAC[ORTHOGONAL_REFL])
\r
492 THEN ASM_CSQ_THEN DIM_OF_PLANE_SPAN (fun x ->
\r
493 ASM_SIMP_TAC[ARITH_RULE `x=1 <=> 3+0=2+x`;GSYM x])
\r
494 THEN MATCH_MP_TAC DIM_SUMS_INTER
\r
495 THEN REWRITE_TAC[SUBSPACE_ORTHOGONAL_TO_VECTORS;ORTHOGONAL_SYM;
\r
499 let NORMAL_SPAN_SUBSET_ORTHOGONAL_SUBSPACE = prove
\r
500 (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p
\r
501 ==> span {n} SUBSET {z:real^3 | !x. x IN span b ==> orthogonal z x}`,
\r
502 REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC
\r
503 THEN POP_ASSUM (C ASM_CSQ_THEN ASSUME_TAC)
\r
504 THEN REWRITE_TAC[SUBSET;SPAN_SING;IN_ELIM_THM;UNIV]
\r
505 THEN ASM_MESON_TAC[ORTHOGONAL_CLAUSES;ORTHOGONAL_SYM]);;
\r
507 let ORTHOGONAL_SUBSPACE_IS_NORMAL_SPAN = prove
\r
508 (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p
\r
509 ==> {z:real^3 | !x. x IN span b ==> orthogonal z x} = span {n}`,
\r
510 MAP_EVERY (SINGLE ONCE_REWRITE_TAC) [
\r
511 ORTHOGONAL_SYM; MESON[SPAN_SPAN] `span{x}=span(span{x})`;
\r
512 GSYM (REWRITE_RULE[GSYM SPAN_EQ_SELF] SUBSPACE_ORTHOGONAL_TO_VECTORS)]
\r
513 THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_SYM
\r
514 THEN MATCH_MP_TAC DIM_EQ_SPAN THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM]
\r
516 THENL ON_FIRST_GOAL (ASM_MESON_TAC[NORMAL_SPAN_SUBSET_ORTHOGONAL_SUBSPACE])
\r
517 THEN MAP_EVERY (fun x ->
\r
518 ASM_CSQ_THEN x (C ASM_CSQ_THEN (SINGLE REWRITE_TAC)))
\r
519 [DIM_OF_ORTHOGONAL;DIM_OF_NORMAL_SPAN]
\r
522 let PLANE_DECOMP = prove
\r
523 (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p
\r
524 ==> !v. ?w x. v = w + x % n /\ w IN span b`,
\r
526 THEN MP_TAC (ISPEC `b:real^3->bool` ORTHOGONAL_SUBSPACE_DECOMP)
\r
527 THEN ASM_CSQ_THEN ORTHOGONAL_SUBSPACE_IS_NORMAL_SPAN
\r
528 (C ASM_CSQ_THEN (C ASM_CSQ_THEN (SINGLE REWRITE_TAC)))
\r
529 THEN REWRITE_TAC[SPAN_SING;IN_ELIM_THM;EXISTS_UNIQUE_DEF;EXISTS_PAIRED_THM]
\r
530 THEN MESON_TAC[]);;
\r
532 let NORMAL_ORTHOGONAL_IN_PLANE_SPAN = prove
\r
533 (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p
\r
534 ==> !v. orthogonal v n <=> v IN span b`,
\r
536 MATCH_MP (MESON[] `(!x y. p x y <=> q x y) ==> (!x y. p x y ==> q x y)`)
\r
539 THEN ASM_CSQ_THEN PLANE_DECOMP (C ASM_CSQ_THEN (C ASM_CSQ_THEN
\r
540 (STRIP_ASSUME_TAC o SPEC `v:real^3`)))
\r
541 THEN ASM_CSQ_THEN (EQ_IMPLY is_normal_to_plane) STRIP_ASSUME_TAC
\r
542 THEN POP_ASSUM (C ASM_CSQ_THEN ASSUME_TAC) THEN EQ_TAC THEN ASM_REWRITE_TAC[]
\r
543 THEN ASM_CSQ_THEN (EQ_IMPLY is_plane_basis) STRIP_ASSUME_TAC
\r
544 THEN RULE_ASSUM_TAC (REWRITE_RULE[orthogonal])
\r
545 THEN ASM_SIMP_TAC[orthogonal;DOT_LADD;DOT_LMUL;REAL_ADD_LID;REAL_ENTIRE;
\r
546 DOT_EQ_0;VECTOR_MUL_LZERO;VECTOR_ADD_RID] THEN ASM_MESON_TAC[]);;
\r
548 let PLANE_DECOMP_DOT_NORMAL = prove
\r
549 (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p
\r
550 ==> !v. ?w. w IN span b /\ v = w + (v dot (unit n)) % (unit n)`,
\r
552 THEN FIRST_ASSUM (ASSUME_TAC o CONJUNCT1 o CONV_RULE (REWR_CONV
\r
553 is_normal_to_plane))
\r
554 THEN ASM_CSQ_THEN (GSYM NORMAL_ORTHOGONAL_IN_PLANE_SPAN) (C ASM_CSQ_THEN
\r
555 (C ASM_CSQ_THEN ASSUME_TAC))
\r
556 THEN EXISTS_TAC `v - (v dot unit n) % unit n :real^3`
\r
557 THEN ASM_REWRITE_TAC[VECTOR_ARITH `x=x-y+z <=> y=z:real^N`]
\r
558 THEN ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RUNIT]
\r
559 THEN REWRITE_TAC[orthogonal;DOT_LSUB;DOT_LMUL]
\r
560 THEN ASM_MESON_TAC[UNIT_DOT_UNIT_SELF;REAL_MUL_RID;REAL_SUB_0]);;
\r
562 let SUB_UNIT_NORMAL_IS_ORTHOGONAL_TO_NORMAL = prove
\r
563 (`!p. plane p ==> !n. is_normal_to_plane n p
\r
564 ==> !x. orthogonal (x - (x dot unit n) % unit n) n`,
\r
565 REPEAT STRIP_TAC THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC
\r
566 THEN ASM_CSQ_THEN PLANE_DECOMP_DOT_NORMAL
\r
567 (C ASM_CSQ_THEN (C ASM_CSQ_THEN ASSUME_TAC))
\r
568 THEN RULE_ASSUM_TAC (REWRITE_RULE[VECTOR_ARITH `x=y+z <=> x-z=y`])
\r
569 THEN ASM_MESON_TAC[NORMAL_ORTHOGONAL_IN_PLANE_SPAN]);;
\r
571 let is_orthogonal_plane_basis = new_definition
\r
572 `is_orthogonal_plane_basis b p
\r
573 <=> is_plane_basis b p /\ pairwise orthogonal b`;;
\r
575 let EXISTS_ORTHOGONAL_PLANE_BASIS = prove
\r
576 (`!p. plane p ==> ?b. is_orthogonal_plane_basis b p`,
\r
577 REWRITE_TAC[is_orthogonal_plane_basis;is_plane_basis] THEN REPEAT STRIP_TAC
\r
578 THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS (CHOOSE_THEN (fun x -> ASSUME_TAC x
\r
579 THEN STRIP_ASSUME_TAC (REWRITE_RULE[is_plane_basis] x)))
\r
580 THEN ASM_CSQ_THEN EXISTS_NORMAL_OF_PLANE (CHOOSE_THEN (fun x ->
\r
581 let x' = REWRITE_RULE[is_normal_to_plane] x in
\r
582 ASSUME_TAC x THEN ASM_CSQ_THEN (CONJUNCT2 x') ASSUME_TAC
\r
583 THEN ASSUME_TAC (CONJUNCT1 x')))
\r
584 THEN SUBGOAL_TAC "" `~((u:real^3)=vec 0)` [ASM SET_TAC[BASIS_NON_NULL]]
\r
585 THEN SUBGOAL_TAC "" `orthogonal u (n:real^3)` [
\r
586 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC SPAN_SUPERSET
\r
587 THEN ASM SET_TAC [SPAN_SUPERSET]
\r
589 THEN SUBGOAL_TAC "" `~(u cross n = vec 0)` [
\r
590 ASM_SIMP_TAC[CROSS_EQ_0;ORTHOGONAL_NON_COLLINEAR] ]
\r
591 THEN EXISTS_TAC `{u, u cross n}` THEN CONJ_TAC
\r
593 MAP_EVERY EXISTS_TAC [`u:real^3`;`u cross n`] THEN REWRITE_TAC[]
\r
594 THEN CONJ_TAC THENL ON_FIRST_GOAL
\r
595 (MATCH_MP_TAC ORTHOGONAL_NON_COLLINEAR
\r
596 THEN ASM_REWRITE_TAC[orthogonal;DOT_CROSS_SELF])
\r
597 THEN SUBGOAL_THEN `?a b. u cross n = a % u + b % v` STRIP_ASSUME_TAC
\r
598 THENL ON_FIRST_GOAL
\r
599 (ASM_MESON_TAC[GSYM PLANE_SPAN_DECOMPOS;
\r
600 GSYM NORMAL_ORTHOGONAL_IN_PLANE_SPAN;orthogonal;DOT_CROSS_SELF])
\r
601 THEN SUBGOAL_THEN `~(b'= &0)` (fun x -> POP_ASSUM MP_TAC THEN ASSUME_TAC x)
\r
602 THENL ON_FIRST_GOAL
\r
603 (ASM_CASES_TAC `a= &0` THENL [
\r
604 ASM_MESON_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID];
\r
605 DISCH_THEN (fun x -> POP_ASSUM (fun y -> POP_ASSUM (MP_TAC
\r
606 o REWRITE_RULE[x;VECTOR_MUL_LZERO;VECTOR_ADD_RID])
\r
607 THEN ASSUME_TAC y))
\r
608 THEN DISCH_THEN (MP_TAC o AP_TERM `(dot) (u:real^3)`)
\r
609 THEN REWRITE_TAC[DOT_CROSS_SELF;DOT_RMUL]
\r
610 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]
\r
611 THEN ASM_REWRITE_TAC[REAL_ENTIRE;DOT_EQ_0]
\r
613 THEN DISCH_THEN (fun x ->
\r
614 ASM_SIMP_TAC[x;VECTOR_ARITH `a%x+b%(c%x+d%y)=(a+b*c)%x+(b*d)%y`])
\r
615 THEN REPEAT STRIP_TAC THEN EQ_TAC THENL [
\r
617 THEN MAP_EVERY EXISTS_TAC [`a'-b''/b'*a:real`;`b''/b':real`]
\r
618 THEN ASM_SIMP_TAC[REAL_SUB_ADD;VECTOR_ARITH `x+y=x+z <=> y=z`;
\r
622 REWRITE_TAC[pairwise;orthogonal] THEN SET_TAC [DOT_CROSS_SELF]
\r
625 let ORTHOGONAL_PLANE_BASIS_AS_PAIR = prove
\r
626 (`!b p. is_orthogonal_plane_basis b p ==> ?u v. is_orthogonal_plane_basis {u,v} p`,
\r
627 MESON_TAC[is_orthogonal_plane_basis;is_plane_basis]);;
\r
629 let BASIS_OF_PLANE_ORTHONORMAL_DECOMPOS = prove
\r
630 (`!p. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p ==>
\r
631 !x. x IN span {u,v}
\r
632 <=> x = (x dot unit u) % unit u + (x dot unit v) % unit v`,
\r
633 REWRITE_TAC [is_orthogonal_plane_basis] THEN REPEAT STRIP_TAC
\r
634 THEN ASM_CSQ_THEN PLANE_SPAN_DECOMPOS (C ASM_CSQ_THEN (SINGLE REWRITE_TAC))
\r
635 THEN EQ_TAC THENL [
\r
637 THEN SUBGOAL_TAC "" `~(u = vec 0:real^3) /\ ~(v = vec 0:real^3)`
\r
638 [ASM_MESON_TAC[BASIS_NON_NULL;IN_INSERT]]
\r
640 `orthogonal (u:real^3) (unit v) /\ orthogonal v (unit u)`
\r
641 (ASSUME_TAC o REWRITE_RULE[orthogonal])
\r
642 THENL ON_FIRST_GOAL
\r
643 (RULE_ASSUM_TAC (REWRITE_RULE[pairwise;orthogonal])
\r
644 THEN REWRITE_TAC[ORTHOGONAL_UNIT;orthogonal]
\r
645 THEN SUBGOAL_TAC "" `~(u=v:real^3)` [ASM_MESON_TAC[BASIS_DIFFERENT]]
\r
646 THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASSUM_LIST SET_TAC)
\r
647 THEN ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;REAL_MUL_RZERO;REAL_ADD_RID;
\r
648 REAL_ADD_LID;DOT_UNIT_SELF;GSYM VECTOR_MUL_ASSOC;GSYM UNIT_INTRO];
\r
649 REWRITE_TAC[unit;VECTOR_MUL_ASSOC] THEN MESON_TAC[]
\r
652 let PLANE_DECOMP_DOT = prove
\r
653 (`!p:plane. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p
\r
654 ==> !n. is_normal_to_plane n p ==> !x:real^3.
\r
655 x = (x dot unit u) % unit u + (x dot unit v) % unit v
\r
656 + (x dot unit n) % unit n`,
\r
658 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV
\r
659 is_orthogonal_plane_basis))
\r
660 THEN ASM_CSQ_THEN PLANE_DECOMP_DOT_NORMAL
\r
661 (C ASM_CSQ_THEN (C ASM_CSQ_THEN (STRIP_ASSUME_TAC o SPEC `x:real^3`)))
\r
663 `(x:real^3) dot unit u = w dot unit u /\ x dot unit v = w dot unit v`
\r
665 THENL ON_FIRST_GOAL
\r
667 SUBGOAL_THEN `(u:real^3) IN {u,v} /\ v IN {u,v}` STRIP_ASSUME_TAC
\r
668 THENL ON_FIRST_GOAL (ASSUM_LIST SET_TAC)
\r
669 THEN ASM_CSQ_THEN NORMAL_OF_PLANE_IS_NORMAL_TO_BASIS
\r
670 (C ASM_CSQ_THEN ASSUME_TAC)
\r
671 THEN POP_ASSUM (fun x -> ASM_CSQ_THEN ~remove:true x
\r
672 (C ASM_CSQ_THEN ASSUME_TAC)
\r
673 THEN ASM_CSQ_THEN x (C ASM_CSQ_THEN ASSUME_TAC))
\r
674 THEN RULE_ASSUM_TAC (REWRITE_RULE[orthogonal]
\r
675 o ONCE_REWRITE_RULE[GSYM ORTHOGONAL_LRUNIT]
\r
676 o ONCE_REWRITE_RULE[ORTHOGONAL_SYM])
\r
677 THEN ASM ONCE_REWRITE_TAC[]
\r
678 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_LMUL;REAL_MUL_RZERO;REAL_ADD_RID]
\r
680 THEN ASM_CSQ_THEN (REWRITE_RULE[GSYM IMP_IMP]
\r
681 BASIS_OF_PLANE_ORTHONORMAL_DECOMPOS) (C ASM_CSQ_THEN (ASSUME_TAC
\r
682 o SPEC `w:real^3`))
\r
683 THEN ASSUM_LIST (GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV))
\r
684 THEN ASM_REWRITE_TAC[VECTOR_ARITH `x+y=z+t+y <=> x=z+t`]
\r
685 THEN ASM_MESON_TAC[]);;
\r
687 let UNIT_OF_ORTHOGONAL_BASIS_IS_ORTHOGONAL_BASIS = prove
\r
688 (`!p. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p
\r
689 ==> is_orthogonal_plane_basis {unit u,unit v} p`,
\r
690 SIMP_TAC[is_orthogonal_plane_basis;UNIT_OF_BASIS_IS_BASIS;pairwise;IN_INSERT;
\r
692 THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]
\r
693 THEN ASM_MESON_TAC[ORTHOGONAL_LRUNIT]);;
\r
695 let EXISTS_UNIT_ORTHOGONAL_PLANE_BASIS = prove
\r
696 (`!p. plane p ==> ?u v. is_orthogonal_plane_basis {unit u,unit v} p`,
\r
698 THEN ASM_CSQ_THEN EXISTS_ORTHOGONAL_PLANE_BASIS (CHOOSE_THEN
\r
699 (DISTRIB (map (fun xs -> STRIP_ASSUME_TAC o REWRITE_RULE xs) [
\r
701 [is_orthogonal_plane_basis];
\r
702 [is_orthogonal_plane_basis;is_plane_basis]])))
\r
703 THEN FIRST_X_ASSUM SUBST_VAR_TAC
\r
704 THEN ASM_MESON_TAC[UNIT_OF_ORTHOGONAL_BASIS_IS_ORTHOGONAL_BASIS]);;
\r
706 let FORALL_PLANE_THM = prove
\r
708 ?u v. is_orthogonal_plane_basis {unit u,unit v} p /\ !P pt0. pt0 IN p
\r
709 ==> ((!pt. pt IN p ==> P pt)
\r
710 <=> (!a b. P (pt0 + a % unit u + b % unit v)))`,
\r
712 THEN ASM_CSQ_THEN EXISTS_UNIT_ORTHOGONAL_PLANE_BASIS (CHOOSE_THEN
\r
713 (CHOOSE_THEN (DISTRIB (map (fun xs -> STRIP_ASSUME_TAC o REWRITE_RULE xs) [
\r
715 [is_orthogonal_plane_basis];
\r
716 [is_orthogonal_plane_basis;is_plane_basis]]))))
\r
717 THEN MAP_EVERY EXISTS_TAC [`u:real^3`;`v:real^3`]
\r
718 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
\r
719 THEN ASM_CSQ_THEN PAIR_SETS_EQ STRIP_ASSUME_TAC
\r
720 THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)
\r
721 THEN ASM_CSQ_THEN PLANE_AS_SPAN (C ASM_CSQ_THEN (C ASM_CSQ_THEN (ASSUME_TAC
\r
722 o REWRITE_RULE[SPAN_2;UNIV;IN_ELIM_THM])))
\r
723 THEN ASSUM_LIST SET_TAC);;
\r
725 let FORALL_PLANE_THM_2 = prove
\r
727 ?u v pt0. is_orthogonal_plane_basis {unit u,unit v} p /\ pt0 IN p
\r
728 /\ !P. (!pt. pt IN p ==> P pt)
\r
729 <=> (!a b. P (pt0 + a % unit u + b % unit v))`,
\r
730 REPEAT STRIP_TAC THEN ASM_CSQ_THEN FORALL_PLANE_THM STRIP_ASSUME_TAC
\r
731 THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC o REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) THEN ASM_MESON_TAC[]);;
\r
733 (** Is u the projection of v on the hyperplane represented by the non-null vector w? *)
\r
734 let is_projection_on_hyperplane = new_definition
\r
735 `is_projection_on_hyperplane u v (w:real^N)
\r
736 <=> norm w = &1 ==> u = v - (v dot w) % w`;;
\r
738 let projection_on_hyperplane = new_definition
\r
739 `projection_on_hyperplane v w = @u. is_projection_on_hyperplane u v w`;;
\r
741 let PROJECTION_ON_HYPERPLANE_THM = prove
\r
742 (`!v w. norm w = &1
\r
743 ==> projection_on_hyperplane v w = v - (v dot w) % w`,
\r
744 REWRITE_TAC[projection_on_hyperplane;is_projection_on_hyperplane]
\r
745 THEN SELECT_ELIM_TAC THEN MESON_TAC[]);;
\r
747 let PROJECTION_ON_HYPERPLANE_THM_LNEG = prove
\r
748 (`!v w. norm w = &1
\r
749 ==> projection_on_hyperplane (--v) w = --(projection_on_hyperplane v w)`,
\r
750 SIMP_TAC[PROJECTION_ON_HYPERPLANE_THM;VECTOR_NEG_SUB;DOT_LNEG;
\r
752 THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
\r
754 let PROJECTION_ON_HYPERPLANE_DECOMPOS = prove
\r
755 (`!v w. norm w = &1 ==> projection_on_hyperplane v w + (v dot w) % w = v`,
\r
756 SIMP_TAC[projection_on_hyperplane;is_projection_on_hyperplane]
\r
757 THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
\r
759 let symetric_vectors_wrt = new_definition
\r
760 `symetric_vectors_wrt u v (w:real^3)
\r
761 <=> norm w = &1 ==> u + v = (&2 * u dot w) % w`;;
\r
763 let SYMETRIC_VECTORS_WRT_SYM = prove
\r
764 (`!u v w. symetric_vectors_wrt u v w <=> symetric_vectors_wrt v u w`,
\r
765 REWRITE_TAC[symetric_vectors_wrt] THEN REPEAT GEN_TAC THEN EQ_TAC
\r
766 THEN DISCH_THEN (fun x -> DISCH_THEN (DISTRIB (map ((o) ASSUME_TAC)
\r
767 [MP x; REWRITE_RULE[NORM_EQ_1]])))
\r
768 THEN ASSUM_LIST (GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV)
\r
769 o map (REWRITE_RULE[VECTOR_ARITH `x+y=z <=> y=z-x:real^N`]))
\r
770 THEN ASM_REWRITE_TAC[DOT_LSUB;DOT_LMUL;REAL_ARITH `(&2 * x) * &1 - x = x`]
\r
771 THEN ONCE_REWRITE_TAC[VECTOR_ADD_SYM] THEN ASM_REWRITE_TAC[]);;
\r
773 let SYMETRIC_VECTORS_PROJECTION_ON_HYPERPLANE = prove
\r
774 (`!u v w. norm w = &1 ==> symetric_vectors_wrt u v w
\r
775 ==> --(projection_on_hyperplane v w) = projection_on_hyperplane u w`,
\r
776 ONCE_REWRITE_TAC[MATCH_MP (MESON[] `(p <=> q) ==> (p <=> p /\ q)`)
\r
777 (SPEC_ALL SYMETRIC_VECTORS_WRT_SYM)]
\r
778 THEN SIMP_TAC[symetric_vectors_wrt;projection_on_hyperplane;
\r
779 is_projection_on_hyperplane;
\r
780 VECTOR_ARITH `x = (&2 * y) % z <=> y%z = inv(&2) % x`]
\r
781 THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
\r
783 let SYMETRIC_VECTORS_PROJECTION_ON_AXIS = prove
\r
784 (`!u v w. norm w = &1 ==> symetric_vectors_wrt u v w ==> u dot w = v dot w`,
\r
786 THEN ASM_CSQ_THEN (GEQ_IMP SYMETRIC_VECTORS_WRT_SYM) ASSUME_TAC
\r
787 THEN REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC[symetric_vectors_wrt]
\r
788 THEN REWRITE_TAC[IMP_IMP;GSYM CONJ_ASSOC;REAL_EQ_MUL_LCANCEL;
\r
789 VECTOR_ARITH `u+v=w /\ v+u=x <=> u+v=x /\ x=w`;VECTOR_MUL_RCANCEL]
\r
790 THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[DOT_RZERO] THEN POP_ASSUM MP_TAC
\r
791 THEN REAL_ARITH_TAC);;
\r
794 (** Additions to affine spaces *)
\r
796 let AFFINE_HULL_3_ZERO = prove
\r
797 (`affine hull {vec 0, a, b} = {u % a + v % b | u IN (:real) /\ v IN(:real)}`,
\r
798 REWRITE_TAC[AFFINE_HULL_3;UNIV;EXTENSION;IN_ELIM_THM;VECTOR_MUL_RZERO;
\r
799 VECTOR_ADD_LID;REAL_ARITH `x+y+z=t <=> x=t-y-z:real`]
\r
800 THEN MESON_TAC[]);;
\r
802 let LSUB_PLANE_EQ_RSUB_PLANE = prove
\r
803 (`!p:plane. plane p ==> !x. x IN p ==> {y - x | y IN p} = {x - y | y IN p}`,
\r
805 EXISTS_TAC t THEN CONJ_TAC THEN TRY VECTOR_ARITH_TAC
\r
806 THEN SUBGOAL_TAC "" `(x':real^3) IN span b` [ASM SET_TAC []]
\r
808 REWRITE_TAC[GSPEC;SETSPEC;FUN_EQ_THM] THEN REPEAT STRIP_TAC
\r
809 THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC
\r
810 THEN ASM_CSQS_THEN PLANE_AS_SPAN ASSUME_TAC THEN EQ_TAC THENL [
\r
811 ASM_CSQS_THEN PLANE_SPAN ASSUME_TAC THEN STRIP_TAC
\r
812 THEN COMMON_TAC `x-x':point` THEN REWRITE_TAC[VECTOR_SUB]
\r
813 THEN POP_ASSUM (ASSUME_TAC o MATCH_MP SPAN_NEG)
\r
814 THEN ASSUM_LIST (FIRST o List.rev_map (CHANGED_TAC o SINGLE REWRITE_TAC))
\r
815 THEN ASSUM_LIST SET_TAC;
\r
816 STRIP_TAC THEN ASM_CSQS_THEN PLANE_SPAN ASSUME_TAC
\r
817 THEN COMMON_TAC `x+x':point` THEN ASSUM_LIST SET_TAC]);;
\r
819 let EXISTS_MULTIPLE_OF_NORMAL_IN_PLANE = prove
\r
820 (`!p:plane. plane p ==> !n. is_normal_to_plane n p ==> ?a. a % unit n IN p`,
\r
822 THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC
\r
823 o REWRITE_RULE[GSYM MEMBER_NOT_EMPTY])
\r
824 THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC
\r
825 THEN ASM_CSQS_THEN (GSYM PLANE_SPAN) (fun x ->
\r
826 ASM_CSQS_THEN PLANE_DECOMP_DOT_NORMAL
\r
827 (MP_TAC o SPEC `x:point` o REWRITE_RULE[x]))
\r
828 THEN ASM_SIMP_TAC[LSUB_PLANE_EQ_RSUB_PLANE] THEN REWRITE_TAC[IN_ELIM_THM]
\r
829 THEN STRIP_TAC THEN EXISTS_TAC `(x:point) dot unit n`
\r
830 THEN MATCH_MP_TAC (MESON[] `(pt':point) IN p /\ pt' = y ==> y IN p`)
\r
831 THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (POP_ASSUM MP_TAC)
\r
832 THEN VECTOR_ARITH_TAC);;
\r
834 (* Additional functions *)
\r
835 let map_triple = new_definition `map_triple (f:A->B) (x1,x2,x3) = (f x1,f x2,f x3)`;;
\r