(* ========================================================================= *)
(* Geometric algebra. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/vectors.ml";;
needs "Library/binary.ml";;
prioritize_real();;
(* ------------------------------------------------------------------------- *)
(* Some basic lemmas, mostly set theory. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Index type for "multivectors" (k-vectors for all k <= N). *)
(* ------------------------------------------------------------------------- *)
let multivector_tybij =
new_type_definition "multivector" ("mk_multivector","dest_multivector")
multivector_tybij_th;;
let DEST_MK_MULTIVECTOR = prove
(`!s. s
SUBSET 1..dimindex(:N)
==> dest_multivector(mk_multivector s :(N)multivector) = s`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [GSYM multivector_tybij] THEN
ASM_REWRITE_TAC[]);;
let LINEAR_EQ_MBASIS = prove
(`!f:real^(M)multivector->real^N g b s.
linear f /\ linear g /\
(!s. s
SUBSET 1..dimindex(:M) ==> f(mbasis s) = g(mbasis s))
==> f = g`,
let BILINEAR_EQ_MBASIS = prove
(`!f:real^(M)multivector->real^(N)multivector->real^P g b s.
bilinear f /\ bilinear g /\
(!s t. s
SUBSET 1..dimindex(:M) /\ t
SUBSET 1..dimindex(:N)
==> f (mbasis s) (mbasis t) = g (mbasis s) (mbasis t))
==> f = g`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN
`!x y. x
IN UNIV /\ y
IN UNIV
==> (f:real^(M)multivector->real^(N)multivector->real^P) x y = g x y`
(fun th -> MP_TAC th THEN REWRITE_TAC[
FUN_EQ_THM;
IN_UNIV]) THEN
MATCH_MP_TAC
BILINEAR_EQ THEN
EXISTS_TAC `{mbasis s :real^(M)multivector | s
SUBSET 1..dimindex(:M)}` THEN
EXISTS_TAC `{mbasis t :real^(N)multivector | t
SUBSET 1..dimindex(:N)}` THEN
ASM_REWRITE_TAC[
SPAN_MBASIS;
SUBSET_REFL;
IN_ELIM_THM] THEN
ASM_MESON_TAC[]);;
let MBASIS_EXTENSION = prove
(`!P. (!s. s
SUBSET 1..dimindex(:N) ==> P(mbasis s)) /\
(!c x. P x ==> P(c % x)) /\ (!x y. P x /\ P y ==> P(x + y))
==> !x:real^(N)multivector. P x`,
let Product_DEF = new_definition
`(Product mult op
:real^(N)multivector->real^(N)multivector->real^(N)multivector) x y =
vsum {s | s SUBSET 1..dimindex(:N)}
(\s. vsum {s | s SUBSET 1..dimindex(:N)}
(\t. (x$$s * y$$t * mult s t) % mbasis (op s t)))`;;let PRODUCT_ASSOCIATIVE = prove
(`!op mult. (!s t. s
SUBSET 1..dimindex(:N) /\ t
SUBSET 1..dimindex(:N)
==> (op s t)
SUBSET 1..dimindex(:N)) /\
(!s t u. op s (op t u) = op (op s t) u) /\
(!s t u. mult t u * mult s (op t u) = mult s t * mult (op s t) u)
==> !x y z:real^(N)multivector.
Product mult op x (Product mult op y z) =
Product mult op (Product mult op x y) z`,
let SUM_SWAP_POWERSET =
SIMP_RULE[
FINITE_POWERSET;
FINITE_NUMSEG]
(repeat(SPEC `{s | s
SUBSET 1..dimindex(:N)}`)
(ISPEC `f:(num->bool)->(num->bool)->real`
SUM_SWAP)) in
let SWAP_TAC cnv n =
GEN_REWRITE_TAC (cnv o funpow n BINDER_CONV) [SUM_SWAP_POWERSET] THEN
REWRITE_TAC[] in
let SWAPS_TAC cnv ns x =
MAP_EVERY (SWAP_TAC cnv) ns THEN MATCH_MP_TAC
SUM_EQ THEN X_GEN_TAC x THEN
REWRITE_TAC[
IN_ELIM_THM] THEN STRIP_TAC in
REWRITE_TAC[
Product_DEF] THEN REPEAT STRIP_TAC THEN
SIMP_TAC[
MULTIVECTOR_EQ;
MULTIVECTOR_VSUM_COMPONENT;
MBASIS_COMPONENT;
MULTIVECTOR_MUL_COMPONENT] THEN
SIMP_TAC[GSYM
SUM_LMUL; GSYM
SUM_RMUL] THEN
X_GEN_TAC `r:num->bool` THEN STRIP_TAC THEN
SWAPS_TAC RAND_CONV [1;0] `s:num->bool` THEN
SWAP_TAC LAND_CONV 0 THEN SWAPS_TAC RAND_CONV [1;0] `t:num->bool` THEN
SWAP_TAC RAND_CONV 0 THEN SWAPS_TAC LAND_CONV [0] `u:num->bool` THEN
REWRITE_TAC[GSYM REAL_MUL_ASSOC;
REAL_ARITH `(if p then a else &0) * b = if p then a * b else &0`;
REAL_ARITH `a * (if p then b else &0) = if p then a * b else &0`] THEN
SIMP_TAC[
SUM_DELTA] THEN ASM_SIMP_TAC[
IN_ELIM_THM] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LID;
REAL_MUL_RID] THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
REAL_MUL_AC]);;
let geom_mul = new_definition
`(x:real^(N)multivector) * y =
Product (\s t. --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
j IN 1..dimindex(:N) /\
i IN s /\ j IN t /\ i > j})
(\s t. (s DIFF t) UNION (t DIFF s))
x y`;;let OUTER = prove
(`!x y:real^(N)multivector.
x outer y =
Product (\s t. if ~(s
INTER t = {}) then &0
else --(&1) pow
CARD {i,j | i
IN 1..dimindex(:N) /\
j
IN 1..dimindex(:N) /\
i
IN s /\ j
IN t /\ i > j})
(
UNION)
x y`,
let OUTER_ASSOC = prove
(`!x y z:real^(N)multivector. x outer (y outer z) = (x outer y) outer z`,
let inner = new_definition
`!x y:real^(N)multivector.
x inner y =
Product (\s t. if s = {} \/ t = {} \/
~((s DIFF t) = {} /\ ~(t DIFF s = {}))
then &0
else --(&1) pow CARD {i,j | i IN 1..dimindex(:N) /\
j IN 1..dimindex(:N) /\
i IN s /\ j IN t /\ i > j})
(\s t. (s DIFF t) UNION (t DIFF s))
x y`;;let PRODUCT_MBASIS = prove
(`!s t. Product mult op (mbasis s) (mbasis t) :real^(N)multivector =
if s
SUBSET 1..dimindex(:N) /\ t
SUBSET 1..dimindex(:N)
then mult s t % mbasis(op s t)
else vec 0`,
let PRODUCT_MBASIS_SING = prove
(`!i j. Product mult op (mbasis{i}) (mbasis{j}) :real^(N)multivector =
if i
IN 1..dimindex(:N) /\ j
IN 1..dimindex(:N)
then mult {i} {j} % mbasis(op {i} {j})
else vec 0`,
let GEOM_MBASIS_SING = prove
(`!i j. mbasis{i} * mbasis{j} :real^(N)multivector =
if i
IN 1..dimindex(:N) /\ j
IN 1..dimindex(:N)
then if i = j then mbasis{}
else if i < j then mbasis{i,j}
else --(mbasis{i,j})
else vec 0`,
let OUTER_MBASIS_SING = prove
(`!i j. mbasis{i} outer mbasis{j} :real^(N)multivector =
if i
IN 1..dimindex(:N) /\ j
IN 1..dimindex(:N) /\ ~(i = j)
then if i < j then mbasis{i,j} else --(mbasis{i,j})
else vec 0`,
let OUTER_MBASIS_SKEWSYM = prove
(`!i j. mbasis{i} outer mbasis{j} = --(mbasis{j} outer mbasis{i})`,
REPEAT GEN_TAC THEN REWRITE_TAC[
OUTER_MBASIS_SING] THEN
ASM_CASES_TAC `i:num = j` THEN ASM_REWRITE_TAC[
VECTOR_NEG_0] THEN
FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`~(i:num = j) ==> i < j /\ ~(j < i) \/ j < i /\ ~(i < j)`)) THEN
ASM_REWRITE_TAC[
CONJ_ACI] THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[
VECTOR_NEG_NEG;
VECTOR_NEG_0] THEN
REPEAT AP_TERM_TAC THEN SET_TAC[]);;
let OUTER_ACI = prove
(`(!x y z. (x outer y) outer z = x outer (y outer z)) /\
(!i j. i > j
==> mbasis{i} outer mbasis{j} =
--(&1) % (mbasis{j} outer mbasis{i})) /\
(!i j x. i > j
==> mbasis{i} outer mbasis{j} outer x =
--(&1) % (mbasis{j} outer mbasis{i} outer x)) /\
(!i. mbasis{i} outer mbasis{i} = vec 0) /\
(!i x. mbasis{i} outer mbasis{i} outer x = vec 0) /\
(!x. mbasis{} outer x = x) /\
(!x. x outer mbasis{} = x)`,
let seqiterate_EXISTS = prove
(`!op f. ?h.
!s. h s = if
INFINITE s \/ s = {} then neutral op else
let i = minimal x. x
IN s in
if s = {i} then f(i) else op (f i) (h (s
DELETE i))`,
REPEAT GEN_TAC THEN REWRITE_TAC[
INFINITE] THEN
MATCH_MP_TAC(MATCH_MP
WF_REC (ISPEC `CARD:(num->bool)->num`
WF_MEASURE)) THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
LET_TAC THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[
MEASURE] THEN
RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
SUBGOAL_THEN `?i:num. i
IN s` MP_TAC THENL
[ASM_MESON_TAC[
MEMBER_NOT_EMPTY]; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [
MINIMAL] THEN
ASM_SIMP_TAC[
CARD_DELETE;
CARD_EQ_0; ARITH_RULE `n - 1 < n <=> ~(n = 0)`]);;
let EXISTS_SWAP = prove
(`!P. (?f. P f) <=> (?f:A->B->C. P (\b a. f a b))`,
GEN_TAC THEN EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
[EXISTS_TAC `\a b. (f:B->A->C) b a` THEN ASM_REWRITE_TAC[ETA_AX];
ASM_MESON_TAC[]]);;
let SEQITERATE_CLAUSES = prove
(`(!op f. seqiterate op {} f = neutral op) /\
(!op f i. seqiterate op {i} f = f(i)) /\
(!op f i s.
FINITE s /\ ~(s = {}) /\ (!j. j
IN s ==> i < j)
==> seqiterate op (i
INSERT s) f =
op (f i) (seqiterate op s f))`,