1 (* ========================================================================= *)
2 (* Geometric algebra. *)
4 (* (c) Copyright, John Harrison 1998-2008 *)
5 (* ========================================================================= *)
7 needs "Multivariate/vectors.ml";;
8 needs "Library/binary.ml";;
12 (* ------------------------------------------------------------------------- *)
13 (* Some basic lemmas, mostly set theory. *)
14 (* ------------------------------------------------------------------------- *)
16 let CARD_UNION_LEMMA = prove
17 (`FINITE s /\ FINITE t /\ FINITE u /\ FINITE v /\
18 s INTER t = {} /\ u INTER v = {} /\ s UNION t = u UNION v
19 ==> CARD(s) + CARD(t) = CARD(u) + CARD(v)`,
20 MESON_TAC[CARD_UNION]);;
22 let CARD_DIFF_INTER = prove
23 (`!s t. FINITE s ==> CARD s = CARD(s DIFF t) + CARD(s INTER t)`,
24 REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
25 ASM_REWRITE_TAC[] THEN SET_TAC[]);;
27 let CARD_ADD_SYMDIFF_INTER = prove
31 CARD((s DIFF t) UNION (t DIFF s)) + 2 * CARD(s INTER t)`,
33 SUBST1_TAC(SPEC `t:A->bool`(MATCH_MP CARD_DIFF_INTER
34 (ASSUME `FINITE(s:A->bool)`))) THEN
35 SUBST1_TAC(SPEC `s:A->bool`(MATCH_MP CARD_DIFF_INTER
36 (ASSUME `FINITE(t:A->bool)`))) THEN
37 REWRITE_TAC[INTER_ACI] THEN
38 MATCH_MP_TAC(ARITH_RULE `c = a + b ==> (a + x) + (b + x) = c + 2 * x`) THEN
39 MATCH_MP_TAC CARD_UNION THEN ASM_SIMP_TAC[FINITE_DIFF] THEN SET_TAC[]);;
41 let SYMDIFF_PARITY_LEMMA = prove
42 (`!s t u. FINITE s /\ FINITE t /\ (s DIFF t) UNION (t DIFF s) = u
43 ==> EVEN(CARD u) = (EVEN(CARD s) <=> EVEN(CARD t))`,
44 ONCE_REWRITE_TAC[GSYM EVEN_ADD] THEN
45 SIMP_TAC[CARD_ADD_SYMDIFF_INTER] THEN
46 REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH]);;
48 let FINITE_CART_SUBSET_LEMMA = prove
49 (`!P m n. FINITE {i,j | i IN 1..m /\ j IN 1..n /\ P i j}`,
50 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
51 EXISTS_TAC `{i,j | i IN 1..m /\ j IN 1..n}` THEN
52 SIMP_TAC[SUBSET; FINITE_PRODUCT; FINITE_NUMSEG] THEN
53 SIMP_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM]);;
55 (* ------------------------------------------------------------------------- *)
56 (* Index type for "multivectors" (k-vectors for all k <= N). *)
57 (* ------------------------------------------------------------------------- *)
59 let multivector_tybij_th = prove
60 (`?s. s SUBSET (1..dimindex(:N))`,
61 MESON_TAC[EMPTY_SUBSET]);;
63 let multivector_tybij =
64 new_type_definition "multivector" ("mk_multivector","dest_multivector")
65 multivector_tybij_th;;
67 let MULTIVECTOR_IMAGE = prove
68 (`(:(N)multivector) = IMAGE mk_multivector {s | s SUBSET 1..dimindex(:N)}`,
69 REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE; IN_ELIM_THM] THEN
70 MESON_TAC[multivector_tybij]);;
72 let HAS_SIZE_MULTIVECTOR = prove
73 (`(:(N)multivector) HAS_SIZE (2 EXP dimindex(:N))`,
74 REWRITE_TAC[MULTIVECTOR_IMAGE] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
75 SIMP_TAC[HAS_SIZE_POWERSET; HAS_SIZE_NUMSEG_1; IN_ELIM_THM] THEN
76 MESON_TAC[multivector_tybij]);;
78 let FINITE_MULTIVECTOR = prove
79 (`FINITE(:(N)multivector)`,
80 MESON_TAC[HAS_SIZE; HAS_SIZE_MULTIVECTOR]);;
82 let DIMINDEX_MULTIVECTOR = prove
83 (`dimindex(:(N)multivector) = 2 EXP dimindex(:N)`,
84 MESON_TAC[DIMINDEX_UNIQUE; HAS_SIZE_MULTIVECTOR]);;
86 let DEST_MK_MULTIVECTOR = prove
87 (`!s. s SUBSET 1..dimindex(:N)
88 ==> dest_multivector(mk_multivector s :(N)multivector) = s`,
89 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [GSYM multivector_tybij] THEN
92 let FORALL_MULTIVECTOR = prove
93 (`(!s. s SUBSET 1..dimindex(:N) ==> P(mk_multivector s)) <=>
94 (!m:(N)multivector. P m)`,
95 EQ_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN DISCH_TAC THEN GEN_TAC THEN
96 MP_TAC(ISPEC `m:(N)multivector`
97 (REWRITE_RULE[EXTENSION] MULTIVECTOR_IMAGE)) THEN
98 REWRITE_TAC[IN_UNIV; IN_IMAGE; EXISTS_PAIR_THM; IN_ELIM_THM] THEN
101 (* ------------------------------------------------------------------------- *)
102 (* The bijections we use for indexing. *)
104 (* Note that we need a *single* bijection over the entire space that also *)
105 (* works for the various subsets. Hence the tedious explicit construction. *)
106 (* ------------------------------------------------------------------------- *)
108 let setcode = new_definition
109 `setcode s = 1 + binarysum (IMAGE PRE s)`;;
111 let codeset = new_definition
112 `codeset n = IMAGE SUC (bitset(n - 1))`;;
114 let CODESET_SETCODE_BIJECTIONS = prove
115 (`(!i. i IN 1..(2 EXP n)
116 ==> codeset i SUBSET 1..n /\ setcode(codeset i) = i) /\
118 ==> (setcode s) IN 1..(2 EXP n) /\ codeset(setcode s) = s)`,
119 REWRITE_TAC[codeset; setcode; ADD_SUB2; GSYM IMAGE_o; o_DEF; PRE] THEN
120 REWRITE_TAC[SET_RULE `IMAGE (\x. x) s = s`] THEN CONJ_TAC THEN GEN_TAC THENL
121 [REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_NUMSEG] THEN
122 SIMP_TAC[ARITH_RULE `1 <= i ==> (1 + b = i <=> b = i - 1)`] THEN
123 REWRITE_TAC[ARITH_RULE `1 <= SUC n /\ SUC n <= k <=> n < k`] THEN
124 DISCH_THEN(MP_TAC o MATCH_MP
125 (ARITH_RULE `1 <= i /\ i <= t ==> i - 1 < t`)) THEN
126 MESON_TAC[BITSET_BOUND; BINARYSUM_BITSET];
129 FIRST_ASSUM(MP_TAC o ISPEC `PRE` o MATCH_MP IMAGE_SUBSET) THEN
130 REWRITE_TAC[IN_NUMSEG; SUBSET] THEN DISCH_TAC THEN CONJ_TAC THENL
131 [MATCH_MP_TAC(ARITH_RULE `x < n ==> 1 <= 1 + x /\ 1 + x <= n`) THEN
132 MATCH_MP_TAC BINARYSUM_BOUND THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN
133 FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
134 ASM_REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ARITH_TAC;
136 MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `IMAGE SUC (IMAGE PRE s)` THEN
138 [ASM_MESON_TAC[FINITE_IMAGE; FINITE_SUBSET; FINITE_NUMSEG; BITSET_BINARYSUM];
140 UNDISCH_TAC `s SUBSET 1..n` THEN
141 REWRITE_TAC[SUBSET; EXTENSION; IN_IMAGE; IN_NUMSEG] THEN
142 MESON_TAC[ARITH_RULE `1 <= n ==> SUC(PRE n) = n`]);;
144 let FORALL_SETCODE = prove
145 (`(!s. s SUBSET (1..n) ==> P(setcode s)) <=> (!i. i IN 1..(2 EXP n) ==> P i)`,
146 MESON_TAC[CODESET_SETCODE_BIJECTIONS; SUBSET]);;
148 let SETCODE_BOUNDS = prove
149 (`!s n. s SUBSET 1..n ==> setcode s IN (1..(2 EXP n))`,
150 MESON_TAC[CODESET_SETCODE_BIJECTIONS]);;
152 (* ------------------------------------------------------------------------- *)
153 (* Indexing directly via subsets. *)
154 (* ------------------------------------------------------------------------- *)
156 parse_as_infix("$$",(25,"left"));;
158 let sindex = new_definition
159 `(x:real^(N)multivector)$$s = x$(setcode s)`;;
161 parse_as_binder "lambdas";;
163 let lambdas = new_definition
164 `(lambdas) (g:(num->bool)->real) =
165 (lambda i. g(codeset i)):real^(N)multivector`;;
167 (* ------------------------------------------------------------------------- *)
168 (* Crucial properties. *)
169 (* ------------------------------------------------------------------------- *)
171 let MULTIVECTOR_EQ = prove
172 (`!x y:real^(N)multivector.
173 x = y <=> !s. s SUBSET 1..dimindex(:N) ==> x$$s = y$$s`,
174 SIMP_TAC[CART_EQ; sindex; FORALL_SETCODE; GSYM IN_NUMSEG;
175 DIMINDEX_MULTIVECTOR]);;
177 let MULTIVECTOR_BETA = prove
178 (`!s. s SUBSET 1..dimindex(:N)
179 ==> ((lambdas) g :real^(N)multivector)$$s = g s`,
180 SIMP_TAC[sindex; lambdas; LAMBDA_BETA; SETCODE_BOUNDS;
181 DIMINDEX_MULTIVECTOR; GSYM IN_NUMSEG] THEN
182 MESON_TAC[CODESET_SETCODE_BIJECTIONS]);;
184 let MULTIVECTOR_UNIQUE = prove
185 (`!m:real^(N)multivector g.
186 (!s. s SUBSET 1..dimindex(:N) ==> m$$s = g s)
187 ==> (lambdas) g = m`,
188 SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_BETA] THEN MESON_TAC[]);;
190 let MULTIVECTOR_ETA = prove
191 (`(lambdas s. m$$s) = m`,
192 SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_BETA]);;
194 (* ------------------------------------------------------------------------- *)
195 (* Also componentwise operations; they all work in this style. *)
196 (* ------------------------------------------------------------------------- *)
198 let MULTIVECTOR_ADD_COMPONENT = prove
199 (`!x y:real^(N)multivector s.
200 s SUBSET (1..dimindex(:N)) ==> (x + y)$$s = x$$s + y$$s`,
201 SIMP_TAC[sindex; SETCODE_BOUNDS; DIMINDEX_MULTIVECTOR;
202 GSYM IN_NUMSEG; VECTOR_ADD_COMPONENT]);;
204 let MULTIVECTOR_MUL_COMPONENT = prove
205 (`!c x:real^(N)multivector s.
206 s SUBSET (1..dimindex(:N)) ==> (c % x)$$s = c * x$$s`,
207 SIMP_TAC[sindex; SETCODE_BOUNDS; DIMINDEX_MULTIVECTOR;
208 GSYM IN_NUMSEG; VECTOR_MUL_COMPONENT]);;
210 let MULTIVECTOR_VEC_COMPONENT = prove
211 (`!k s. s SUBSET (1..dimindex(:N)) ==> (vec k :real^(N)multivector)$$s = &k`,
212 SIMP_TAC[sindex; SETCODE_BOUNDS; DIMINDEX_MULTIVECTOR;
213 GSYM IN_NUMSEG; VEC_COMPONENT]);;
215 let MULTIVECTOR_VSUM_COMPONENT = prove
216 (`!f:A->real^(N)multivector t s.
217 s SUBSET (1..dimindex(:N))
218 ==> (vsum t f)$$s = sum t (\x. (f x)$$s)`,
219 SIMP_TAC[vsum; sindex; LAMBDA_BETA; SETCODE_BOUNDS; GSYM IN_NUMSEG;
220 DIMINDEX_MULTIVECTOR]);;
222 let MULTIVECTOR_VSUM = prove
223 (`!t f. vsum t f = lambdas s. sum t (\x. (f x)$$s)`,
224 SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_BETA; MULTIVECTOR_VSUM_COMPONENT]);;
226 (* ------------------------------------------------------------------------- *)
227 (* Basis vectors indexed by subsets of 1..N. *)
228 (* ------------------------------------------------------------------------- *)
230 let mbasis = new_definition
231 `mbasis i = lambdas s. if i = s then &1 else &0`;;
233 let MBASIS_COMPONENT = prove
234 (`!s t. s SUBSET (1..dimindex(:N))
235 ==> (mbasis t :real^(N)multivector)$$s = if s = t then &1 else &0`,
236 SIMP_TAC[mbasis; IN_ELIM_THM; MULTIVECTOR_BETA] THEN MESON_TAC[]);;
238 let MBASIS_EQ_0 = prove
239 (`!s. (mbasis s :real^(N)multivector = vec 0) <=>
240 ~(s SUBSET 1..dimindex(:N))`,
241 SIMP_TAC[MULTIVECTOR_EQ; MBASIS_COMPONENT; MULTIVECTOR_VEC_COMPONENT] THEN
242 MESON_TAC[REAL_ARITH `~(&1 = &0)`]);;
244 let MBASIS_NONZERO = prove
245 (`!s. s SUBSET 1..dimindex(:N) ==> ~(mbasis s :real^(N)multivector = vec 0)`,
246 REWRITE_TAC[MBASIS_EQ_0]);;
248 let MBASIS_EXPANSION = prove
249 (`!x:real^(N)multivector.
250 vsum {s | s SUBSET 1..dimindex(:N)} (\s. x$$s % mbasis s) = x`,
251 SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_VSUM_COMPONENT;
252 MULTIVECTOR_MUL_COMPONENT; MBASIS_COMPONENT] THEN
253 REPEAT STRIP_TAC THEN
254 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
255 ASM_SIMP_TAC[REAL_ARITH `x * (if p then &1 else &0) = if p then x else &0`;
256 SUM_DELTA; IN_ELIM_THM]);;
258 let SPAN_MBASIS = prove
259 (`span {mbasis s :real^(N)multivector | s SUBSET 1..dimindex(:N)} = UNIV`,
260 REWRITE_TAC[EXTENSION; IN_UNIV] THEN X_GEN_TAC `x:real^(N)multivector` THEN
261 GEN_REWRITE_TAC LAND_CONV [GSYM MBASIS_EXPANSION] THEN
262 MATCH_MP_TAC SPAN_VSUM THEN
263 SIMP_TAC[FINITE_NUMSEG; FINITE_POWERSET; IN_ELIM_THM] THEN
264 REPEAT STRIP_TAC THEN MATCH_MP_TAC SPAN_MUL THEN
265 MATCH_MP_TAC SPAN_SUPERSET THEN REWRITE_TAC[IN_ELIM_THM] THEN
268 (* ------------------------------------------------------------------------- *)
269 (* Linear and bilinear functions are determined by their effect on basis. *)
270 (* ------------------------------------------------------------------------- *)
272 let LINEAR_EQ_MBASIS = prove
273 (`!f:real^(M)multivector->real^N g b s.
274 linear f /\ linear g /\
275 (!s. s SUBSET 1..dimindex(:M) ==> f(mbasis s) = g(mbasis s))
277 REPEAT STRIP_TAC THEN
278 SUBGOAL_THEN `!x. x IN UNIV ==> (f:real^(M)multivector->real^N) x = g x`
279 (fun th -> MP_TAC th THEN REWRITE_TAC[FUN_EQ_THM; IN_UNIV]) THEN
280 MATCH_MP_TAC LINEAR_EQ THEN
281 EXISTS_TAC `{mbasis s :real^(M)multivector | s SUBSET 1..dimindex(:M)}` THEN
282 ASM_REWRITE_TAC[SPAN_MBASIS; SUBSET_REFL; IN_ELIM_THM] THEN
285 let BILINEAR_EQ_MBASIS = prove
286 (`!f:real^(M)multivector->real^(N)multivector->real^P g b s.
287 bilinear f /\ bilinear g /\
288 (!s t. s SUBSET 1..dimindex(:M) /\ t SUBSET 1..dimindex(:N)
289 ==> f (mbasis s) (mbasis t) = g (mbasis s) (mbasis t))
291 REPEAT STRIP_TAC THEN SUBGOAL_THEN
292 `!x y. x IN UNIV /\ y IN UNIV
293 ==> (f:real^(M)multivector->real^(N)multivector->real^P) x y = g x y`
294 (fun th -> MP_TAC th THEN REWRITE_TAC[FUN_EQ_THM; IN_UNIV]) THEN
295 MATCH_MP_TAC BILINEAR_EQ THEN
296 EXISTS_TAC `{mbasis s :real^(M)multivector | s SUBSET 1..dimindex(:M)}` THEN
297 EXISTS_TAC `{mbasis t :real^(N)multivector | t SUBSET 1..dimindex(:N)}` THEN
298 ASM_REWRITE_TAC[SPAN_MBASIS; SUBSET_REFL; IN_ELIM_THM] THEN
301 (* ------------------------------------------------------------------------- *)
302 (* A way of proving linear properties by extension from basis. *)
303 (* ------------------------------------------------------------------------- *)
305 let LINEAR_PROPERTY = prove
306 (`!P. P(vec 0) /\ (!x y. P x /\ P y ==> P(x + y))
307 ==> !f s. FINITE s /\ (!i. i IN s ==> P(f i)) ==> P(vsum s f)`,
308 GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
309 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
310 ASM_SIMP_TAC[VSUM_CLAUSES; IN_INSERT]);;
312 let MBASIS_EXTENSION = prove
313 (`!P. (!s. s SUBSET 1..dimindex(:N) ==> P(mbasis s)) /\
314 (!c x. P x ==> P(c % x)) /\ (!x y. P x /\ P y ==> P(x + y))
315 ==> !x:real^(N)multivector. P x`,
316 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM MBASIS_EXPANSION] THEN
317 MATCH_MP_TAC(SIMP_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP] LINEAR_PROPERTY) THEN
318 ASM_SIMP_TAC[FINITE_POWERSET; FINITE_NUMSEG; IN_ELIM_THM] THEN
319 ASM_MESON_TAC[EMPTY_SUBSET; VECTOR_MUL_LZERO]);;
321 (* ------------------------------------------------------------------------- *)
322 (* Injection from regular vectors. *)
323 (* ------------------------------------------------------------------------- *)
325 let multivec = new_definition
326 `(multivec:real^N->real^(N)multivector) x =
327 vsum(1..dimindex(:N)) (\i. x$i % mbasis{i})`;;
329 (* ------------------------------------------------------------------------- *)
330 (* Subspace of k-vectors. *)
331 (* ------------------------------------------------------------------------- *)
333 parse_as_infix("multivector",(12,"right"));;
335 let multivector = new_definition
336 `k multivector (p:real^(N)multivector) <=>
337 !s. s SUBSET (1..dimindex(:N)) /\ ~(p$$s = &0) ==> s HAS_SIZE k`;;
339 (* ------------------------------------------------------------------------- *)
340 (* k-grade part of a multivector. *)
341 (* ------------------------------------------------------------------------- *)
343 parse_as_infix("grade",(22,"right"));;
345 let grade = new_definition
346 `k grade (p:real^(N)multivector) =
347 (lambdas s. if s HAS_SIZE k then p$$s else &0):real^(N)multivector`;;
349 let MULTIVECTOR_GRADE = prove
350 (`!k x. k multivector (k grade x)`,
351 SIMP_TAC[multivector; grade; MULTIVECTOR_BETA; IMP_CONJ] THEN
354 let GRADE_ADD = prove
355 (`!x y k. k grade (x + y) = (k grade x) + (k grade y)`,
356 SIMP_TAC[grade; MULTIVECTOR_EQ; MULTIVECTOR_ADD_COMPONENT;
357 MULTIVECTOR_BETA; COND_COMPONENT] THEN
360 let GRADE_CMUL = prove
361 (`!c x k. k grade (c % x) = c % (k grade x)`,
362 SIMP_TAC[grade; MULTIVECTOR_EQ; MULTIVECTOR_MUL_COMPONENT;
363 MULTIVECTOR_BETA; COND_COMPONENT] THEN
366 (* ------------------------------------------------------------------------- *)
367 (* General product construct. *)
368 (* ------------------------------------------------------------------------- *)
370 let Product_DEF = new_definition
372 :real^(N)multivector->real^(N)multivector->real^(N)multivector) x y =
373 vsum {s | s SUBSET 1..dimindex(:N)}
374 (\s. vsum {s | s SUBSET 1..dimindex(:N)}
375 (\t. (x$$s * y$$t * mult s t) % mbasis (op s t)))`;;
377 (* ------------------------------------------------------------------------- *)
378 (* This is always bilinear. *)
379 (* ------------------------------------------------------------------------- *)
381 let BILINEAR_PRODUCT = prove
382 (`!mult op. bilinear(Product mult op)`,
383 REWRITE_TAC[bilinear; linear; Product_DEF] THEN
384 SIMP_TAC[GSYM VSUM_LMUL; MULTIVECTOR_MUL_COMPONENT] THEN
385 REWRITE_TAC[VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
386 REPEAT STRIP_TAC THEN REWRITE_TAC[Product_DEF] THEN
387 SIMP_TAC[GSYM VSUM_ADD; FINITE_POWERSET; FINITE_NUMSEG] THEN
388 REPEAT(MATCH_MP_TAC VSUM_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN
389 REPEAT STRIP_TAC) THEN
390 ASM_SIMP_TAC[MULTIVECTOR_ADD_COMPONENT] THEN VECTOR_ARITH_TAC);;
392 let PRODUCT_LADD = (MATCH_MP BILINEAR_LADD o SPEC_ALL) BILINEAR_PRODUCT;;
393 let PRODUCT_RADD = (MATCH_MP BILINEAR_RADD o SPEC_ALL) BILINEAR_PRODUCT;;
394 let PRODUCT_LMUL = (MATCH_MP BILINEAR_LMUL o SPEC_ALL) BILINEAR_PRODUCT;;
395 let PRODUCT_RMUL = (MATCH_MP BILINEAR_RMUL o SPEC_ALL) BILINEAR_PRODUCT;;
396 let PRODUCT_LNEG = (MATCH_MP BILINEAR_LNEG o SPEC_ALL) BILINEAR_PRODUCT;;
397 let PRODUCT_RNEG = (MATCH_MP BILINEAR_RNEG o SPEC_ALL) BILINEAR_PRODUCT;;
398 let PRODUCT_LZERO = (MATCH_MP BILINEAR_LZERO o SPEC_ALL) BILINEAR_PRODUCT;;
399 let PRODUCT_RZERO = (MATCH_MP BILINEAR_RZERO o SPEC_ALL) BILINEAR_PRODUCT;;
401 (* ------------------------------------------------------------------------- *)
402 (* Under suitable conditions, it's also associative. *)
403 (* ------------------------------------------------------------------------- *)
405 let PRODUCT_ASSOCIATIVE = prove
406 (`!op mult. (!s t. s SUBSET 1..dimindex(:N) /\ t SUBSET 1..dimindex(:N)
407 ==> (op s t) SUBSET 1..dimindex(:N)) /\
408 (!s t u. op s (op t u) = op (op s t) u) /\
409 (!s t u. mult t u * mult s (op t u) = mult s t * mult (op s t) u)
410 ==> !x y z:real^(N)multivector.
411 Product mult op x (Product mult op y z) =
412 Product mult op (Product mult op x y) z`,
413 let SUM_SWAP_POWERSET =
414 SIMP_RULE[FINITE_POWERSET; FINITE_NUMSEG]
415 (repeat(SPEC `{s | s SUBSET 1..dimindex(:N)}`)
416 (ISPEC `f:(num->bool)->(num->bool)->real` SUM_SWAP)) in
418 GEN_REWRITE_TAC (cnv o funpow n BINDER_CONV) [SUM_SWAP_POWERSET] THEN
420 let SWAPS_TAC cnv ns x =
421 MAP_EVERY (SWAP_TAC cnv) ns THEN MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC x THEN
422 REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC in
423 REWRITE_TAC[Product_DEF] THEN REPEAT STRIP_TAC THEN
424 SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_VSUM_COMPONENT; MBASIS_COMPONENT;
425 MULTIVECTOR_MUL_COMPONENT] THEN
426 SIMP_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL] THEN
427 X_GEN_TAC `r:num->bool` THEN STRIP_TAC THEN
428 SWAPS_TAC RAND_CONV [1;0] `s:num->bool` THEN
429 SWAP_TAC LAND_CONV 0 THEN SWAPS_TAC RAND_CONV [1;0] `t:num->bool` THEN
430 SWAP_TAC RAND_CONV 0 THEN SWAPS_TAC LAND_CONV [0] `u:num->bool` THEN
431 REWRITE_TAC[GSYM REAL_MUL_ASSOC;
432 REAL_ARITH `(if p then a else &0) * b = if p then a * b else &0`;
433 REAL_ARITH `a * (if p then b else &0) = if p then a * b else &0`] THEN
434 SIMP_TAC[SUM_DELTA] THEN ASM_SIMP_TAC[IN_ELIM_THM] THEN
435 COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RID] THEN
436 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_MUL_AC]);;
438 (* ------------------------------------------------------------------------- *)
439 (* Geometric product. *)
440 (* ------------------------------------------------------------------------- *)
444 `geom_mul:real^(N)multivector->real^(N)multivector->real^(N)multivector`);;
446 let geom_mul = new_definition
447 `(x:real^(N)multivector) * y =
448 Product (\s t. --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
449 j IN 1..dimindex(:N) /\
450 i IN s /\ j IN t /\ i > j})
451 (\s t. (s DIFF t) UNION (t DIFF s))
454 let BILINEAR_GEOM = prove
455 (`bilinear(geom_mul)`,
456 REWRITE_TAC[REWRITE_RULE[GSYM FUN_EQ_THM; ETA_AX] geom_mul] THEN
457 MATCH_ACCEPT_TAC BILINEAR_PRODUCT);;
459 let GEOM_LADD = (MATCH_MP BILINEAR_LADD o SPEC_ALL) BILINEAR_GEOM;;
460 let GEOM_RADD = (MATCH_MP BILINEAR_RADD o SPEC_ALL) BILINEAR_GEOM;;
461 let GEOM_LMUL = (MATCH_MP BILINEAR_LMUL o SPEC_ALL) BILINEAR_GEOM;;
462 let GEOM_RMUL = (MATCH_MP BILINEAR_RMUL o SPEC_ALL) BILINEAR_GEOM;;
463 let GEOM_LNEG = (MATCH_MP BILINEAR_LNEG o SPEC_ALL) BILINEAR_GEOM;;
464 let GEOM_RNEG = (MATCH_MP BILINEAR_RNEG o SPEC_ALL) BILINEAR_GEOM;;
465 let GEOM_LZERO = (MATCH_MP BILINEAR_LZERO o SPEC_ALL) BILINEAR_GEOM;;
466 let GEOM_RZERO = (MATCH_MP BILINEAR_RZERO o SPEC_ALL) BILINEAR_GEOM;;
468 let GEOM_ASSOC = prove
469 (`!x y z:real^(N)multivector. x * (y * z) = (x * y) * z`,
470 REWRITE_TAC[geom_mul] THEN MATCH_MP_TAC PRODUCT_ASSOCIATIVE THEN
471 REPEAT(CONJ_TAC THENL [SET_TAC[]; ALL_TAC]) THEN
472 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_POW_ADD] THEN
473 REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE] THEN
474 AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
475 REWRITE_TAC[EVEN_ADD] THEN
476 W(fun (_,w) -> let tu = funpow 2 lhand w in
477 let su = vsubst[`s:num->bool`,`t:num->bool`] tu in
478 let st = vsubst[`t:num->bool`,`u:num->bool`] su in
479 MATCH_MP_TAC EQ_TRANS THEN
480 EXISTS_TAC(end_itlist (curry mk_eq) [st; su; tu])) THEN
482 [MATCH_MP_TAC(TAUT `(x <=> y <=> z) ==> ((a <=> x) <=> (y <=> z <=> a))`);
483 AP_TERM_TAC THEN CONV_TAC SYM_CONV] THEN
484 MATCH_MP_TAC SYMDIFF_PARITY_LEMMA THEN
485 REWRITE_TAC[FINITE_CART_SUBSET_LEMMA] THEN
486 REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM;
487 IN_UNION; IN_DIFF] THEN
490 (* ------------------------------------------------------------------------- *)
492 (* ------------------------------------------------------------------------- *)
494 parse_as_infix("outer",(20,"right"));;
496 let outer = new_definition
497 `!x y:real^(N)multivector.
499 Product (\s t. if ~(s INTER t = {}) then &0
500 else --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
501 j IN 1..dimindex(:N) /\
502 i IN s /\ j IN t /\ i > j})
503 (\s t. (s DIFF t) UNION (t DIFF s))
507 (`!x y:real^(N)multivector.
509 Product (\s t. if ~(s INTER t = {}) then &0
510 else --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
511 j IN 1..dimindex(:N) /\
512 i IN s /\ j IN t /\ i > j})
515 REPEAT GEN_TAC THEN REWRITE_TAC[outer; Product_DEF] THEN
516 REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
517 ASM_CASES_TAC `s INTER t :num->bool = {}` THEN
518 ASM_REWRITE_TAC[REAL_MUL_RZERO; VECTOR_MUL_LZERO] THEN
519 ASM_SIMP_TAC[SET_RULE
520 `(s INTER t = {}) ==> (s DIFF t) UNION (t DIFF s) = s UNION t`]);;
522 let BILINEAR_OUTER = prove
524 REWRITE_TAC[REWRITE_RULE[GSYM FUN_EQ_THM; ETA_AX] outer] THEN
525 MATCH_ACCEPT_TAC BILINEAR_PRODUCT);;
527 let OUTER_LADD = (MATCH_MP BILINEAR_LADD o SPEC_ALL) BILINEAR_OUTER;;
528 let OUTER_RADD = (MATCH_MP BILINEAR_RADD o SPEC_ALL) BILINEAR_OUTER;;
529 let OUTER_LMUL = (MATCH_MP BILINEAR_LMUL o SPEC_ALL) BILINEAR_OUTER;;
530 let OUTER_RMUL = (MATCH_MP BILINEAR_RMUL o SPEC_ALL) BILINEAR_OUTER;;
531 let OUTER_LNEG = (MATCH_MP BILINEAR_LNEG o SPEC_ALL) BILINEAR_OUTER;;
532 let OUTER_RNEG = (MATCH_MP BILINEAR_RNEG o SPEC_ALL) BILINEAR_OUTER;;
533 let OUTER_LZERO = (MATCH_MP BILINEAR_LZERO o SPEC_ALL) BILINEAR_OUTER;;
534 let OUTER_RZERO = (MATCH_MP BILINEAR_RZERO o SPEC_ALL) BILINEAR_OUTER;;
536 let OUTER_ASSOC = prove
537 (`!x y z:real^(N)multivector. x outer (y outer z) = (x outer y) outer z`,
538 REWRITE_TAC[OUTER] THEN MATCH_MP_TAC PRODUCT_ASSOCIATIVE THEN
539 SIMP_TAC[UNION_SUBSET; UNION_ASSOC;
540 SET_RULE `s INTER (t UNION u) = (s INTER t) UNION (s INTER u)`;
541 SET_RULE `(t UNION u) INTER s = (t INTER s) UNION (u INTER s)`] THEN
542 REWRITE_TAC[EMPTY_UNION] THEN REPEAT GEN_TAC THEN
543 MAP_EVERY ASM_CASES_TAC
544 [`s INTER t :num->bool = {}`;
545 `s INTER u :num->bool = {}`;
546 `t INTER u :num->bool = {}`] THEN
547 ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
548 REWRITE_TAC[GSYM REAL_POW_ADD] THEN AP_TERM_TAC THEN
549 MATCH_MP_TAC CARD_UNION_LEMMA THEN REWRITE_TAC[FINITE_CART_SUBSET_LEMMA] THEN
550 SIMP_TAC[EXTENSION; FORALL_PAIR_THM; NOT_IN_EMPTY; IN_UNION; IN_INTER] THEN
551 REWRITE_TAC[IN_ELIM_PAIR_THM] THEN ASM SET_TAC []);;
553 (* ------------------------------------------------------------------------- *)
555 (* ------------------------------------------------------------------------- *)
557 parse_as_infix("inner",(20,"right"));;
559 let inner = new_definition
560 `!x y:real^(N)multivector.
562 Product (\s t. if s = {} \/ t = {} \/
563 ~((s DIFF t) = {} /\ ~(t DIFF s = {}))
565 else --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
566 j IN 1..dimindex(:N) /\
567 i IN s /\ j IN t /\ i > j})
568 (\s t. (s DIFF t) UNION (t DIFF s))
571 let BILINEAR_INNER = prove
573 REWRITE_TAC[REWRITE_RULE[GSYM FUN_EQ_THM; ETA_AX] inner] THEN
574 MATCH_ACCEPT_TAC BILINEAR_PRODUCT);;
576 let INNER_LADD = (MATCH_MP BILINEAR_LADD o SPEC_ALL) BILINEAR_INNER;;
577 let INNER_RADD = (MATCH_MP BILINEAR_RADD o SPEC_ALL) BILINEAR_INNER;;
578 let INNER_LMUL = (MATCH_MP BILINEAR_LMUL o SPEC_ALL) BILINEAR_INNER;;
579 let INNER_RMUL = (MATCH_MP BILINEAR_RMUL o SPEC_ALL) BILINEAR_INNER;;
580 let INNER_LNEG = (MATCH_MP BILINEAR_LNEG o SPEC_ALL) BILINEAR_INNER;;
581 let INNER_RNEG = (MATCH_MP BILINEAR_RNEG o SPEC_ALL) BILINEAR_INNER;;
582 let INNER_LZERO = (MATCH_MP BILINEAR_LZERO o SPEC_ALL) BILINEAR_INNER;;
583 let INNER_RZERO = (MATCH_MP BILINEAR_RZERO o SPEC_ALL) BILINEAR_INNER;;
585 (* ------------------------------------------------------------------------- *)
586 (* Actions of products on basis and singleton basis. *)
587 (* ------------------------------------------------------------------------- *)
589 let PRODUCT_MBASIS = prove
590 (`!s t. Product mult op (mbasis s) (mbasis t) :real^(N)multivector =
591 if s SUBSET 1..dimindex(:N) /\ t SUBSET 1..dimindex(:N)
592 then mult s t % mbasis(op s t)
594 REPEAT GEN_TAC THEN REWRITE_TAC[Product_DEF] THEN
595 SIMP_TAC[MULTIVECTOR_MUL_COMPONENT; MBASIS_COMPONENT] THEN
596 REWRITE_TAC[REAL_ARITH
597 `(if p then &1 else &0) * (if q then &1 else &0) * x =
598 if q then if p then x else &0 else &0`] THEN
600 (GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RAND] THEN
601 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RATOR] THEN
602 SIMP_TAC[VECTOR_MUL_LZERO; COND_ID; VSUM_DELTA; IN_ELIM_THM; VSUM_0] THEN
603 ASM_CASES_TAC `t SUBSET 1..dimindex(:N)` THEN ASM_REWRITE_TAC[]));;
605 let PRODUCT_MBASIS_SING = prove
606 (`!i j. Product mult op (mbasis{i}) (mbasis{j}) :real^(N)multivector =
607 if i IN 1..dimindex(:N) /\ j IN 1..dimindex(:N)
608 then mult {i} {j} % mbasis(op {i} {j})
610 REWRITE_TAC[PRODUCT_MBASIS; SET_RULE `{x} SUBSET s <=> x IN s`]);;
612 let GEOM_MBASIS = prove
613 (`!s t. mbasis s * mbasis t :real^(N)multivector =
614 if s SUBSET 1..dimindex(:N) /\ t SUBSET 1..dimindex(:N)
615 then --(&1) pow CARD {i,j | i IN s /\ j IN t /\ i > j} %
616 mbasis((s DIFF t) UNION (t DIFF s))
618 REPEAT GEN_TAC THEN REWRITE_TAC[geom_mul; PRODUCT_MBASIS] THEN
619 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
620 AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
621 REWRITE_TAC[EXTENSION; IN_ELIM_PAIR_THM; FORALL_PAIR_THM] THEN
622 ASM_MESON_TAC[SUBSET]);;
624 let GEOM_MBASIS_SING = prove
625 (`!i j. mbasis{i} * mbasis{j} :real^(N)multivector =
626 if i IN 1..dimindex(:N) /\ j IN 1..dimindex(:N)
627 then if i = j then mbasis{}
628 else if i < j then mbasis{i,j}
631 REPEAT GEN_TAC THEN REWRITE_TAC[geom_mul; PRODUCT_MBASIS_SING] THEN
632 COND_CASES_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN
634 `{i',j' | i' IN 1 .. dimindex (:N) /\
635 j' IN 1 .. dimindex (:N) /\
639 if i > j then {(i,j)} else {}`
641 [REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_SING] THEN
642 COND_CASES_TAC THEN ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; PAIR_EQ] THEN
643 ASM_MESON_TAC[LT_REFL];
645 ASM_CASES_TAC `i:num = j` THEN ASM_REWRITE_TAC[GT; LT_REFL] THENL
646 [REWRITE_TAC[CARD_CLAUSES; real_pow; VECTOR_MUL_LID] THEN
647 AP_TERM_TAC THEN SET_TAC[];
649 ASM_SIMP_TAC[SET_RULE
650 `~(i = j) ==> ({i} DIFF {j}) UNION ({j} DIFF {i}) = {i,j}`] THEN
651 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
652 `~(i:num = j) ==> (j < i <=> ~(i < j))`)) THEN
653 ASM_CASES_TAC `i:num < j` THEN
654 ASM_SIMP_TAC[CARD_CLAUSES; real_pow; VECTOR_MUL_LID; FINITE_RULES;
658 let OUTER_MBASIS = prove
659 (`!s t. (mbasis s) outer (mbasis t) :real^(N)multivector =
660 if s SUBSET 1..dimindex(:N) /\ t SUBSET 1..dimindex(:N) /\
662 then --(&1) pow CARD {i,j | i IN s /\ j IN t /\ i > j} %
665 REPEAT GEN_TAC THEN REWRITE_TAC[OUTER; PRODUCT_MBASIS] THEN
666 ASM_CASES_TAC `(s:num->bool) INTER t = {}` THEN
667 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; COND_ID] THEN
668 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
669 AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
670 REWRITE_TAC[EXTENSION; IN_ELIM_PAIR_THM; FORALL_PAIR_THM] THEN
671 ASM_MESON_TAC[SUBSET]);;
673 let OUTER_MBASIS_SING = prove
674 (`!i j. mbasis{i} outer mbasis{j} :real^(N)multivector =
675 if i IN 1..dimindex(:N) /\ j IN 1..dimindex(:N) /\ ~(i = j)
676 then if i < j then mbasis{i,j} else --(mbasis{i,j})
678 REPEAT GEN_TAC THEN REWRITE_TAC[OUTER; PRODUCT_MBASIS_SING] THEN
679 REWRITE_TAC[SET_RULE `{i} INTER {j} = {} <=> ~(i = j)`] THEN
680 ASM_CASES_TAC `i:num = j` THEN
681 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; COND_ID] THEN
682 COND_CASES_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN
684 `{i',j' | i' IN 1 .. dimindex (:N) /\
685 j' IN 1 .. dimindex (:N) /\
689 if i > j then {(i,j)} else {}`
691 [REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_SING] THEN
692 COND_CASES_TAC THEN ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; PAIR_EQ] THEN
693 ASM_MESON_TAC[LT_REFL];
695 ASM_SIMP_TAC[GT; SET_RULE `{i} UNION {j} = {i,j}`] THEN
696 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
697 `~(i:num = j) ==> (j < i <=> ~(i < j))`)) THEN
698 ASM_CASES_TAC `i:num < j` THEN
699 ASM_SIMP_TAC[CARD_CLAUSES; real_pow; VECTOR_MUL_LID; FINITE_RULES;
703 (* ------------------------------------------------------------------------- *)
704 (* Some simple consequences. *)
705 (* ------------------------------------------------------------------------- *)
707 let OUTER_MBASIS_SKEWSYM = prove
708 (`!i j. mbasis{i} outer mbasis{j} = --(mbasis{j} outer mbasis{i})`,
709 REPEAT GEN_TAC THEN REWRITE_TAC[OUTER_MBASIS_SING] THEN
710 ASM_CASES_TAC `i:num = j` THEN ASM_REWRITE_TAC[VECTOR_NEG_0] THEN
711 FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
712 `~(i:num = j) ==> i < j /\ ~(j < i) \/ j < i /\ ~(i < j)`)) THEN
713 ASM_REWRITE_TAC[CONJ_ACI] THEN COND_CASES_TAC THEN
714 ASM_REWRITE_TAC[VECTOR_NEG_NEG; VECTOR_NEG_0] THEN
715 REPEAT AP_TERM_TAC THEN SET_TAC[]);;
717 let OUTER_MBASIS_REFL = prove
718 (`!i. mbasis{i} outer mbasis{i} = vec 0`,
719 GEN_TAC THEN MATCH_MP_TAC(VECTOR_ARITH
720 `!x:real^N. x = --x ==> x = vec 0`) THEN
721 MATCH_ACCEPT_TAC OUTER_MBASIS_SKEWSYM);;
723 let OUTER_MBASIS_LSCALAR = prove
724 (`!x. mbasis{} outer x = x`,
725 MATCH_MP_TAC MBASIS_EXTENSION THEN SIMP_TAC[OUTER_RMUL; OUTER_RADD] THEN
726 SIMP_TAC[OUTER_MBASIS; EMPTY_SUBSET; INTER_EMPTY; UNION_EMPTY] THEN
727 REWRITE_TAC[SET_RULE `{i,j | i IN {} /\ j IN s /\ i:num > j} = {}`] THEN
728 REWRITE_TAC[CARD_CLAUSES; real_pow; VECTOR_MUL_LID]);;
730 let OUTER_MBASIS_RSCALAR = prove
731 (`!x. x outer mbasis{} = x`,
732 MATCH_MP_TAC MBASIS_EXTENSION THEN SIMP_TAC[OUTER_LMUL; OUTER_LADD] THEN
733 SIMP_TAC[OUTER_MBASIS; EMPTY_SUBSET; INTER_EMPTY; UNION_EMPTY] THEN
734 REWRITE_TAC[SET_RULE `{i,j | i IN s /\ j IN {} /\ i:num > j} = {}`] THEN
735 REWRITE_TAC[CARD_CLAUSES; real_pow; VECTOR_MUL_LID]);;
737 let MBASIS_SPLIT = prove
738 (`!a s. (!x. x IN s ==> a < x)
739 ==> mbasis (a INSERT s) = mbasis{a} outer mbasis s`,
740 REPEAT STRIP_TAC THEN REWRITE_TAC[OUTER_MBASIS] THEN
741 SUBGOAL_THEN `{a:num} INTER s = {}` SUBST1_TAC THENL
742 [ASM SET_TAC [LT_REFL]; ALL_TAC] THEN
743 SIMP_TAC[SET_RULE`{a} SUBSET t /\ s SUBSET t <=> (a INSERT s) SUBSET t`] THEN
744 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[MBASIS_EQ_0]] THEN
745 REWRITE_TAC[SET_RULE `{a} UNION s = a INSERT s`] THEN
746 SUBGOAL_THEN `{(i:num),(j:num) | i IN {a} /\ j IN s /\ i > j} = {}`
747 (fun th -> SIMP_TAC[th; CARD_CLAUSES; real_pow; VECTOR_MUL_LID]) THEN
748 REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_SING;
750 ASM_MESON_TAC[ARITH_RULE `~(n < m /\ n:num > m)`]);;
752 (* ------------------------------------------------------------------------- *)
753 (* Just for generality, normalize a set enumeration. *)
754 (* ------------------------------------------------------------------------- *)
756 let SETENUM_NORM_CONV =
758 GEN_REWRITE_CONV I [EXTENSION] THENC
759 GEN_REWRITE_CONV TOP_SWEEP_CONV [IN_SING; IN_INSERT] THENC
760 BINDER_CONV(EQT_INTRO o DISJ_ACI_RULE) THENC
761 GEN_REWRITE_CONV I [FORALL_SIMP] in
763 let nums = dest_setenum tm in
764 let nums' = map mk_numeral (sort (</) (map dest_numeral (setify nums))) in
765 if nums' = nums then REFL tm else
766 let eq = mk_eq(tm,mk_setenum(nums',fst(dest_fun_ty(type_of tm)))) in
769 (* ------------------------------------------------------------------------- *)
770 (* Conversion to split extended basis combinations. *)
772 (* Also 1-step merge from left, which can be DEPTH_CONV'd. In this case the *)
773 (* order must be correct. *)
774 (* ------------------------------------------------------------------------- *)
776 let MBASIS_SPLIT_CONV,MBASIS_MERGE_CONV =
777 let setlemma = SET_RULE
778 `((!x:num. x IN {} ==> a < x) <=> T) /\
779 ((!x:num. x IN (y INSERT s) ==> a < x) <=>
780 a < y /\ (!x. x IN s ==> a < x))` in
782 GEN_REWRITE_CONV TOP_SWEEP_CONV [setlemma] THENC NUM_REDUCE_CONV
783 and INST_SPLIT = PART_MATCH (lhs o rand) MBASIS_SPLIT
784 and INST_MERGE = PART_MATCH (lhs o rand) (GSYM MBASIS_SPLIT) in
786 if length(dest_setenum(rand tm)) <= 1 then REFL tm else
787 let th = MP_CONV SET_CHECK_CONV (INST_SPLIT tm) in
788 let th' = RAND_CONV conv (rand(concl th)) in
791 try let op,se = dest_comb tm in
792 if fst(dest_const op) = "mbasis" & forall is_numeral (dest_setenum se)
793 then (RAND_CONV SETENUM_NORM_CONV THENC conv) tm
795 with Failure _ -> failwith "MBASIS_SPLIT_CONV"),
796 (fun tm -> try MP_CONV SET_CHECK_CONV (INST_MERGE tm)
797 with Failure _ -> failwith "MBASIS_MERGE_CONV");;
799 (* ------------------------------------------------------------------------- *)
800 (* Convergent (if slow) rewrite set to bubble into position. *)
801 (* ------------------------------------------------------------------------- *)
803 let OUTER_ACI = prove
804 (`(!x y z. (x outer y) outer z = x outer (y outer z)) /\
806 ==> mbasis{i} outer mbasis{j} =
807 --(&1) % (mbasis{j} outer mbasis{i})) /\
809 ==> mbasis{i} outer mbasis{j} outer x =
810 --(&1) % (mbasis{j} outer mbasis{i} outer x)) /\
811 (!i. mbasis{i} outer mbasis{i} = vec 0) /\
812 (!i x. mbasis{i} outer mbasis{i} outer x = vec 0) /\
813 (!x. mbasis{} outer x = x) /\
814 (!x. x outer mbasis{} = x)`,
815 REWRITE_TAC[OUTER_ASSOC; OUTER_LZERO; OUTER_RZERO; OUTER_LADD;
816 OUTER_RADD; OUTER_LMUL; OUTER_RMUL; OUTER_LZERO; OUTER_RZERO] THEN
817 REWRITE_TAC[OUTER_MBASIS_REFL; OUTER_LZERO] THEN
818 REWRITE_TAC[OUTER_MBASIS_LSCALAR; OUTER_MBASIS_RSCALAR] THEN
819 SIMP_TAC[GSYM VECTOR_NEG_MINUS1; VECTOR_ARITH `x - y:real^N = x + --y`] THEN
820 MESON_TAC[OUTER_MBASIS_SKEWSYM; OUTER_LNEG]);;
822 (* ------------------------------------------------------------------------- *)
823 (* Group the final "c1 % mbasis s1 + ... + cn % mbasis sn". *)
824 (* ------------------------------------------------------------------------- *)
826 let MBASIS_GROUP_CONV tm =
827 let tms = striplist(dest_binary "vector_add") tm in
828 if length tms = 1 then LAND_CONV REAL_POLY_CONV tm else
829 let vadd_tm = rator(rator tm) in
830 let mk_vadd = mk_binop vadd_tm in
831 let mbs = map (snd o dest_binary "%") tms in
832 let tmbs = zip mbs tms and mset = setify mbs in
833 let grps = map (fun x -> map snd (filter (fun (x',_) -> x' = x) tmbs))
835 let tm' = end_itlist mk_vadd (map (end_itlist mk_vadd) grps) in
836 let th1 = AC VECTOR_ADD_AC (mk_eq(tm,tm'))
838 (GEN_REWRITE_CONV DEPTH_CONV [GSYM VECTOR_ADD_RDISTRIB] THENC
839 DEPTH_BINOP_CONV vadd_tm (LAND_CONV REAL_POLY_CONV)) tm' in
842 (* ------------------------------------------------------------------------- *)
843 (* Overall conversion. *)
844 (* ------------------------------------------------------------------------- *)
846 let OUTER_CANON_CONV =
847 ONCE_DEPTH_CONV MBASIS_SPLIT_CONV THENC
848 GEN_REWRITE_CONV TOP_DEPTH_CONV
849 [VECTOR_SUB; VECTOR_NEG_MINUS1;
850 OUTER_LADD; OUTER_RADD; OUTER_LMUL; OUTER_RMUL; OUTER_LZERO; OUTER_RZERO;
851 VECTOR_ADD_LDISTRIB; VECTOR_ADD_RDISTRIB; VECTOR_MUL_ASSOC;
852 VECTOR_MUL_LZERO; VECTOR_MUL_RZERO] THENC
853 REAL_RAT_REDUCE_CONV THENC
854 PURE_SIMP_CONV[OUTER_ACI; ARITH_GT; ARITH_GE; OUTER_LMUL; OUTER_RMUL;
855 OUTER_LZERO; OUTER_RZERO] THENC
856 PURE_REWRITE_CONV[VECTOR_MUL_LZERO; VECTOR_MUL_RZERO;
857 VECTOR_ADD_LID; VECTOR_ADD_RID; VECTOR_MUL_ASSOC] THENC
858 GEN_REWRITE_CONV I [GSYM VECTOR_MUL_LID] THENC
860 [VECTOR_ADD_LDISTRIB; VECTOR_ADD_RDISTRIB; VECTOR_MUL_ASSOC] THENC
861 REAL_RAT_REDUCE_CONV THENC PURE_REWRITE_CONV[GSYM VECTOR_ADD_ASSOC] THENC
862 DEPTH_CONV MBASIS_MERGE_CONV THENC
863 MBASIS_GROUP_CONV THENC
864 GEN_REWRITE_CONV DEPTH_CONV [GSYM VECTOR_ADD_RDISTRIB] THENC
865 REAL_RAT_REDUCE_CONV;;
867 (* ------------------------------------------------------------------------- *)
868 (* Iterated operation in order. *)
869 (* I guess this ought to be added to the core... *)
870 (* ------------------------------------------------------------------------- *)
872 let seqiterate_EXISTS = prove
874 !s. h s = if INFINITE s \/ s = {} then neutral op else
875 let i = minimal x. x IN s in
876 if s = {i} then f(i) else op (f i) (h (s DELETE i))`,
877 REPEAT GEN_TAC THEN REWRITE_TAC[INFINITE] THEN
878 MATCH_MP_TAC(MATCH_MP WF_REC (ISPEC `CARD:(num->bool)->num` WF_MEASURE)) THEN
879 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
880 LET_TAC THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
881 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
882 FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[MEASURE] THEN
883 RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
884 SUBGOAL_THEN `?i:num. i IN s` MP_TAC THENL
885 [ASM_MESON_TAC[MEMBER_NOT_EMPTY]; ALL_TAC] THEN
886 GEN_REWRITE_TAC LAND_CONV [MINIMAL] THEN
887 ASM_SIMP_TAC[CARD_DELETE; CARD_EQ_0; ARITH_RULE `n - 1 < n <=> ~(n = 0)`]);;
889 let EXISTS_SWAP = prove
890 (`!P. (?f. P f) <=> (?f:A->B->C. P (\b a. f a b))`,
891 GEN_TAC THEN EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
892 [EXISTS_TAC `\a b. (f:B->A->C) b a` THEN ASM_REWRITE_TAC[ETA_AX];
895 let seqiterate = new_specification ["seqiterate"]
896 (REWRITE_RULE[SKOLEM_THM]
897 (ONCE_REWRITE_RULE[EXISTS_SWAP]
898 (ONCE_REWRITE_RULE[SKOLEM_THM] seqiterate_EXISTS)));;
900 let MINIMAL_IN_INSERT = prove
901 (`!s i. (!j. j IN s ==> i < j) ==> (minimal j. j IN (i INSERT s)) = i`,
902 REPEAT STRIP_TAC THEN REWRITE_TAC[minimal] THEN
903 MATCH_MP_TAC SELECT_UNIQUE THEN
904 REWRITE_TAC[IN_INSERT] THEN ASM_MESON_TAC[LT_ANTISYM]);;
906 let SEQITERATE_CLAUSES = prove
907 (`(!op f. seqiterate op {} f = neutral op) /\
908 (!op f i. seqiterate op {i} f = f(i)) /\
909 (!op f i s. FINITE s /\ ~(s = {}) /\ (!j. j IN s ==> i < j)
910 ==> seqiterate op (i INSERT s) f =
911 op (f i) (seqiterate op s f))`,
912 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [seqiterate] THEN
913 ASM_SIMP_TAC[NOT_INSERT_EMPTY; INFINITE; FINITE_INSERT; FINITE_RULES] THEN
914 ASM_SIMP_TAC[MINIMAL_IN_INSERT; NOT_IN_EMPTY; LET_DEF; LET_END_DEF] THEN
915 SUBGOAL_THEN `~((i:num) IN s)` ASSUME_TAC THENL
916 [ASM_MESON_TAC[LT_REFL]; ALL_TAC] THEN
917 ASM_SIMP_TAC[DELETE_INSERT; SET_RULE
918 `~(i IN s) /\ ~(s = {}) ==> (s DELETE i = s) /\ ~(i INSERT s = {i})`]);;
920 (* ------------------------------------------------------------------------- *)
921 (* In the "common" case this agrees with ordinary iteration. *)
922 (* ------------------------------------------------------------------------- *)
924 let SEQITERATE_ITERATE = prove
925 (`!op f s. monoidal op /\ FINITE s ==> seqiterate op s f = iterate op s f`,
926 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
927 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
928 MATCH_MP_TAC FINITE_INDUCT_DELETE THEN
929 ASM_SIMP_TAC[SEQITERATE_CLAUSES; ITERATE_CLAUSES] THEN
930 GEN_TAC THEN STRIP_TAC THEN
931 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
932 GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
933 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `i:num` THEN
934 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
935 FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
936 `i IN s ==> s = i INSERT (s DELETE i)`)) THEN
937 ASM_SIMP_TAC[ITERATE_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
938 ASM_CASES_TAC `s DELETE (i:num) = {}` THEN
939 ASM_SIMP_TAC[SEQITERATE_CLAUSES; ITERATE_CLAUSES] THENL
940 [ASM_MESON_TAC[monoidal]; FIRST_X_ASSUM(SUBST1_TAC o SYM)] THEN
941 MATCH_MP_TAC(last(CONJUNCTS SEQITERATE_CLAUSES)) THEN
942 ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
943 ASM_MESON_TAC[LT_ANTISYM; LT_CASES]);;
945 (* ------------------------------------------------------------------------- *)
946 (* Outermorphism extension. *)
947 (* ------------------------------------------------------------------------- *)
949 let outermorphism = new_definition
950 `outermorphism(f:real^N->real^P) (x:real^(N)multivector) =
951 vsum {s | s SUBSET 1..dimindex(:N)}
952 (\s. x$$s % seqiterate(outer) s (multivec o f o basis))`;;
954 let NEUTRAL_OUTER = prove
955 (`neutral(outer) = mbasis{}`,
956 REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
957 MESON_TAC[OUTER_MBASIS_LSCALAR; OUTER_MBASIS_RSCALAR]);;
959 let OUTERMORPHISM_MBASIS = prove
960 (`!f:real^M->real^N s t.
961 s SUBSET 1..dimindex(:M)
962 ==> outermorphism f (mbasis s) =
963 seqiterate(outer) s (multivec o f o basis)`,
964 REWRITE_TAC[outermorphism] THEN SIMP_TAC[MBASIS_COMPONENT] THEN
965 ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
966 SIMP_TAC[VECTOR_MUL_LZERO; VSUM_DELTA; IN_ELIM_THM; VECTOR_MUL_LID]);;
968 let OUTERMORPHISM_MBASIS_EMPTY = prove
969 (`!f. outermorphism f (mbasis {}) = mbasis {}`,
970 SIMP_TAC[OUTERMORPHISM_MBASIS; EMPTY_SUBSET; SEQITERATE_CLAUSES] THEN
971 REWRITE_TAC[NEUTRAL_OUTER]);;
973 (* ------------------------------------------------------------------------- *)
974 (* Reversion operation. *)
975 (* ------------------------------------------------------------------------- *)
977 let reversion = new_definition
978 `(reversion:real^(N)multivector->real^(N)multivector) x =
979 lambdas s. --(&1) pow ((CARD(s) * (CARD(s) - 1)) DIV 2) * x$$s`;;