colo12-c703.uibk.ac.at Git - Multivariate Analysis/.git/blob - Multivariate/clifford.ml

   1 (* ========================================================================= *)
   2 (* Geometric algebra.                                                        *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2008                       *)
   5 (* ========================================================================= *)
   6
   7 needs "Multivariate/vectors.ml";;
   8 needs "Library/binary.ml";;
   9
  10 prioritize_real();;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Some basic lemmas, mostly set theory.                                     *)
  14 (* ------------------------------------------------------------------------- *)
  15
  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]);;
  21
  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[]);;
  26
  27 let CARD_ADD_SYMDIFF_INTER = prove
  28  (`!s t:A->bool.
  29         FINITE s /\ FINITE t
  30         ==> CARD s + CARD t =
  31             CARD((s DIFF t) UNION (t DIFF s)) + 2 * CARD(s INTER t)`,
  32   REPEAT STRIP_TAC THEN
  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[]);;
  40
  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]);;
  47
  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]);;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* Index type for "multivectors" (k-vectors for all k <= N).                 *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let multivector_tybij_th = prove
  60  (`?s. s SUBSET (1..dimindex(:N))`,
  61   MESON_TAC[EMPTY_SUBSET]);;
  62
  63 let multivector_tybij =
  64   new_type_definition "multivector" ("mk_multivector","dest_multivector")
  65     multivector_tybij_th;;
  66
  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]);;
  71
  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]);;
  77
  78 let FINITE_MULTIVECTOR = prove
  79  (`FINITE(:(N)multivector)`,
  80   MESON_TAC[HAS_SIZE; HAS_SIZE_MULTIVECTOR]);;
  81
  82 let DIMINDEX_MULTIVECTOR = prove
  83  (`dimindex(:(N)multivector) = 2 EXP dimindex(:N)`,
  84   MESON_TAC[DIMINDEX_UNIQUE; HAS_SIZE_MULTIVECTOR]);;
  85
  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
  90   ASM_REWRITE_TAC[]);;
  91
  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
  99   ASM_MESON_TAC[]);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* The bijections we use for indexing.                                       *)
 103 (*                                                                           *)
 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 (* ------------------------------------------------------------------------- *)
 107
 108 let setcode = new_definition
 109  `setcode s = 1 + binarysum (IMAGE PRE s)`;;
 110
 111 let codeset = new_definition
 112  `codeset n = IMAGE SUC (bitset(n - 1))`;;
 113
 114 let CODESET_SETCODE_BIJECTIONS = prove
 115  (`(!i. i IN 1..(2 EXP n)
 116         ==> codeset i SUBSET 1..n /\ setcode(codeset i) = i) /\
 117    (!s. s SUBSET (1..n)
 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];
 127     ALL_TAC] THEN
 128   DISCH_TAC THEN
 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;
 135     ALL_TAC] THEN
 136   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `IMAGE SUC (IMAGE PRE s)` THEN
 137   CONJ_TAC THENL
 138    [ASM_MESON_TAC[FINITE_IMAGE; FINITE_SUBSET; FINITE_NUMSEG; BITSET_BINARYSUM];
 139     ALL_TAC] THEN
 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`]);;
 143
 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]);;
 147
 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]);;
 151
 152 (* ------------------------------------------------------------------------- *)
 153 (* Indexing directly via subsets.                                            *)
 154 (* ------------------------------------------------------------------------- *)
 155
 156 parse_as_infix("$$",(25,"left"));;
 157
 158 let sindex = new_definition
 159   `(x:real^(N)multivector)$$s = x$(setcode s)`;;
 160
 161 parse_as_binder "lambdas";;
 162
 163 let lambdas = new_definition
 164  `(lambdas) (g:(num->bool)->real) =
 165     (lambda i. g(codeset i)):real^(N)multivector`;;
 166
 167 (* ------------------------------------------------------------------------- *)
 168 (* Crucial properties.                                                       *)
 169 (* ------------------------------------------------------------------------- *)
 170
 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]);;
 176
 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]);;
 183
 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[]);;
 189
 190 let MULTIVECTOR_ETA = prove
 191  (`(lambdas s. m$$s) = m`,
 192   SIMP_TAC[MULTIVECTOR_EQ; MULTIVECTOR_BETA]);;
 193
 194 (* ------------------------------------------------------------------------- *)
 195 (* Also componentwise operations; they all work in this style.               *)
 196 (* ------------------------------------------------------------------------- *)
 197
 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]);;
 203
 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]);;
 209
 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]);;
 214
 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]);;
 221
 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]);;
 225
 226 (* ------------------------------------------------------------------------- *)
 227 (* Basis vectors indexed by subsets of 1..N.                                 *)
 228 (* ------------------------------------------------------------------------- *)
 229
 230 let mbasis = new_definition
 231  `mbasis i = lambdas s. if i = s then &1 else &0`;;
 232
 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[]);;
 237
 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)`]);;
 243
 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]);;
 247
 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]);;
 257
 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
 266   ASM_MESON_TAC[]);;
 267
 268 (* ------------------------------------------------------------------------- *)
 269 (* Linear and bilinear functions are determined by their effect on basis.    *)
 270 (* ------------------------------------------------------------------------- *)
 271
 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))
 276         ==> f = g`,
 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
 283   ASM_MESON_TAC[]);;
 284
 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))
 290         ==> f = g`,
 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
 299   ASM_MESON_TAC[]);;
 300
 301 (* ------------------------------------------------------------------------- *)
 302 (* A way of proving linear properties by extension from basis.               *)
 303 (* ------------------------------------------------------------------------- *)
 304
 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]);;
 311
 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]);;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* Injection from regular vectors.                                           *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let multivec = new_definition
 326  `(multivec:real^N->real^(N)multivector) x =
 327       vsum(1..dimindex(:N)) (\i. x$i % mbasis{i})`;;
 328
 329 (* ------------------------------------------------------------------------- *)
 330 (* Subspace of k-vectors.                                                    *)
 331 (* ------------------------------------------------------------------------- *)
 332
 333 parse_as_infix("multivector",(12,"right"));;
 334
 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`;;
 338
 339 (* ------------------------------------------------------------------------- *)
 340 (* k-grade part of a multivector.                                            *)
 341 (* ------------------------------------------------------------------------- *)
 342
 343 parse_as_infix("grade",(22,"right"));;
 344
 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`;;
 348
 349 let MULTIVECTOR_GRADE = prove
 350  (`!k x. k multivector (k grade x)`,
 351   SIMP_TAC[multivector; grade; MULTIVECTOR_BETA; IMP_CONJ] THEN
 352   MESON_TAC[]);;
 353
 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
 358   REAL_ARITH_TAC);;
 359
 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
 364   REAL_ARITH_TAC);;
 365
 366 (* ------------------------------------------------------------------------- *)
 367 (* General product construct.                                                *)
 368 (* ------------------------------------------------------------------------- *)
 369
 370 let Product_DEF = new_definition
 371  `(Product mult op
 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)))`;;
 376
 377 (* ------------------------------------------------------------------------- *)
 378 (* This is always bilinear.                                                  *)
 379 (* ------------------------------------------------------------------------- *)
 380
 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);;
 391
 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;;
 400
 401 (* ------------------------------------------------------------------------- *)
 402 (* Under suitable conditions, it's also associative.                         *)
 403 (* ------------------------------------------------------------------------- *)
 404
 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
 417   let SWAP_TAC cnv n =
 418     GEN_REWRITE_TAC (cnv o funpow n BINDER_CONV) [SUM_SWAP_POWERSET] THEN
 419     REWRITE_TAC[] in
 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]);;
 437
 438 (* ------------------------------------------------------------------------- *)
 439 (* Geometric product.                                                        *)
 440 (* ------------------------------------------------------------------------- *)
 441
 442 overload_interface
 443  ("*",
 444   `geom_mul:real^(N)multivector->real^(N)multivector->real^(N)multivector`);;
 445
 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))
 452                 x y`;;
 453
 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);;
 458
 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;;
 467
 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
 481   CONJ_TAC THENL
 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
 488   CONV_TAC TAUT);;
 489
 490 (* ------------------------------------------------------------------------- *)
 491 (* Outer product.                                                            *)
 492 (* ------------------------------------------------------------------------- *)
 493
 494 parse_as_infix("outer",(20,"right"));;
 495
 496 let outer = new_definition
 497  `!x y:real^(N)multivector.
 498     x outer y =
 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))
 504                 x y`;;
 505
 506 let OUTER = prove
 507  (`!x y:real^(N)multivector.
 508     x outer y =
 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})
 513                 (UNION)
 514                 x y`,
 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`]);;
 521
 522 let BILINEAR_OUTER = prove
 523  (`bilinear(outer)`,
 524   REWRITE_TAC[REWRITE_RULE[GSYM FUN_EQ_THM; ETA_AX] outer] THEN
 525   MATCH_ACCEPT_TAC BILINEAR_PRODUCT);;
 526
 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;;
 535
 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 []);;
 552
 553 (* ------------------------------------------------------------------------- *)
 554 (* Inner product.                                                            *)
 555 (* ------------------------------------------------------------------------- *)
 556
 557 parse_as_infix("inner",(20,"right"));;
 558
 559 let inner = new_definition
 560  `!x y:real^(N)multivector.
 561     x inner y =
 562         Product (\s t. if s = {} \/ t = {} \/
 563                           ~((s DIFF t) = {} /\ ~(t DIFF s = {}))
 564                        then &0
 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))
 569                 x y`;;
 570
 571 let BILINEAR_INNER = prove
 572  (`bilinear(inner)`,
 573   REWRITE_TAC[REWRITE_RULE[GSYM FUN_EQ_THM; ETA_AX] inner] THEN
 574   MATCH_ACCEPT_TAC BILINEAR_PRODUCT);;
 575
 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;;
 584
 585 (* ------------------------------------------------------------------------- *)
 586 (* Actions of products on basis and singleton basis.                         *)
 587 (* ------------------------------------------------------------------------- *)
 588
 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)
 593             else vec 0`,
 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
 599   REPEAT
 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[]));;
 604
 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})
 609             else vec 0`,
 610   REWRITE_TAC[PRODUCT_MBASIS; SET_RULE `{x} SUBSET s <=> x IN s`]);;
 611
 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))
 617                 else vec 0`,
 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]);;
 623
 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}
 629                      else --(mbasis{i,j})
 630                 else vec 0`,
 631   REPEAT GEN_TAC THEN REWRITE_TAC[geom_mul; PRODUCT_MBASIS_SING] THEN
 632   COND_CASES_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN
 633   SUBGOAL_THEN
 634    `{i',j' | i' IN 1 .. dimindex (:N) /\
 635              j' IN 1 .. dimindex (:N) /\
 636              i' = i /\
 637              j' = j /\
 638              i' > j'} =
 639     if i > j then {(i,j)} else {}`
 640   SUBST1_TAC THENL
 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];
 644     ALL_TAC] THEN
 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[];
 648     ALL_TAC] THEN
 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;
 655                NOT_IN_EMPTY] THEN
 656   VECTOR_ARITH_TAC);;
 657
 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) /\
 661                    s INTER t = {}
 662                 then --(&1) pow CARD {i,j | i IN s /\ j IN t /\ i > j} %
 663                      mbasis(s UNION t)
 664                 else vec 0`,
 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]);;
 672
 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})
 677                 else vec 0`,
 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
 683   SUBGOAL_THEN
 684    `{i',j' | i' IN 1 .. dimindex (:N) /\
 685              j' IN 1 .. dimindex (:N) /\
 686              i' = i /\
 687              j' = j /\
 688              i' > j'} =
 689     if i > j then {(i,j)} else {}`
 690   SUBST1_TAC THENL
 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];
 694     ALL_TAC] THEN
 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;
 700                NOT_IN_EMPTY] THEN
 701   VECTOR_ARITH_TAC);;
 702
 703 (* ------------------------------------------------------------------------- *)
 704 (* Some simple consequences.                                                 *)
 705 (* ------------------------------------------------------------------------- *)
 706
 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[]);;
 716
 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);;
 722
 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]);;
 729
 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]);;
 736
 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;
 749               NOT_IN_EMPTY] THEN
 750   ASM_MESON_TAC[ARITH_RULE `~(n < m /\ n:num > m)`]);;
 751
 752 (* ------------------------------------------------------------------------- *)
 753 (* Just for generality, normalize a set enumeration.                         *)
 754 (* ------------------------------------------------------------------------- *)
 755
 756 let SETENUM_NORM_CONV =
 757   let 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
 762   fun tm ->
 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
 767     EQT_ELIM(conv eq);;
 768
 769 (* ------------------------------------------------------------------------- *)
 770 (* Conversion to split extended basis combinations.                          *)
 771 (*                                                                           *)
 772 (* Also 1-step merge from left, which can be DEPTH_CONV'd. In this case the  *)
 773 (* order must be correct.                                                    *)
 774 (* ------------------------------------------------------------------------- *)
 775
 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
 781   let SET_CHECK_CONV =
 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
 785   let rec conv tm =
 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
 789     TRANS th th' in
 790   (fun tm ->
 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
 794         else fail()
 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");;
 798
 799 (* ------------------------------------------------------------------------- *)
 800 (* Convergent (if slow) rewrite set to bubble into position.                 *)
 801 (* ------------------------------------------------------------------------- *)
 802
 803 let OUTER_ACI = prove
 804  (`(!x y z. (x outer y) outer z = x outer (y outer z)) /\
 805    (!i j. i > j
 806           ==> mbasis{i} outer mbasis{j} =
 807               --(&1) % (mbasis{j} outer mbasis{i})) /\
 808    (!i j x. i > j
 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]);;
 821
 822 (* ------------------------------------------------------------------------- *)
 823 (* Group the final "c1 % mbasis s1 + ... + cn % mbasis sn".                  *)
 824 (* ------------------------------------------------------------------------- *)
 825
 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))
 834                  mset in
 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'))
 837   and th2 =
 838    (GEN_REWRITE_CONV DEPTH_CONV [GSYM VECTOR_ADD_RDISTRIB] THENC
 839     DEPTH_BINOP_CONV vadd_tm (LAND_CONV REAL_POLY_CONV)) tm' in
 840   TRANS th1 th2;;
 841
 842 (* ------------------------------------------------------------------------- *)
 843 (* Overall conversion.                                                       *)
 844 (* ------------------------------------------------------------------------- *)
 845
 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
 859   PURE_REWRITE_CONV
 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;;
 866
 867 (* ------------------------------------------------------------------------- *)
 868 (* Iterated operation in order.                                              *)
 869 (* I guess this ought to be added to the core...                             *)
 870 (* ------------------------------------------------------------------------- *)
 871
 872 let seqiterate_EXISTS = prove
 873  (`!op f. ?h.
 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)`]);;
 888
 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];
 893     ASM_MESON_TAC[]]);;
 894
 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)));;
 899
 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]);;
 905
 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})`]);;
 919
 920 (* ------------------------------------------------------------------------- *)
 921 (* In the "common" case this agrees with ordinary iteration.                 *)
 922 (* ------------------------------------------------------------------------- *)
 923
 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]);;
 944
 945 (* ------------------------------------------------------------------------- *)
 946 (* Outermorphism extension.                                                  *)
 947 (* ------------------------------------------------------------------------- *)
 948
 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))`;;
 953
 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]);;
 958
 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]);;
 967
 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]);;
 972
 973 (* ------------------------------------------------------------------------- *)
 974 (* Reversion operation.                                                      *)
 975 (* ------------------------------------------------------------------------- *)
 976
 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`;;