Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Binary Operations on Finite Sequences

by
Wojciech A. Trybulec

MML identifier: FINSOP_1
[ Mizar article, MML identifier index ]

environ

vocabulary FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2, RELAT_1, FINSEQ_2, SETWISEO,
FUNCOP_1, FUNCT_4, BOOLE, FINSUB_1, ARYTM_1, FINSEQ_4, FINSOP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, BINOP_1,
FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1, FINSUB_1,
SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4;
constructors BINOP_1, FINSEQ_4, SETWISEO, REAL_1, NAT_1, FUNCOP_1, FUNCT_4,
FINSEQ_2, XREAL_0, MEMBERED, XBOOLE_0;
clusters FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3, FUNCT_2, MEMBERED,
ZFMISC_1, XBOOLE_0, ORDINAL2, SUBSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve x,y,y1,y2 for set,
D for non empty set,
d,d1,d2,d3 for Element of D,
F,G,H,H1,H2 for FinSequence of D,
f,f1,f2 for Function of NAT,D,
g for BinOp of D,
k,n,i,j,l for Nat,
P for Permutation of dom F;

definition let D,n,d;
redefine func n |-> d -> FinSequence of D;
end;

definition let D,F,g;
assume  g has_a_unity or len F >= 1;
func g "**" F -> Element of D means
:: FINSOP_1:def 1
it = the_unity_wrt g if g has_a_unity & len F = 0 otherwise
ex f st f.1 = F.1 &
(for n st 0 <> n & n < len F holds
f.(n + 1) = g.(f.n,F.(n + 1))) & it = f.(len F);
end;

canceled;

theorem :: FINSOP_1:2
len F >= 1 implies ex f st f.1 = F.1 & (for n st 0 <> n & n < len F holds
f.(n + 1) = g.(f.n,F.(n + 1))) & g "**" F = f.(len F);

theorem :: FINSOP_1:3
len F >= 1 & (ex f st f.1 = F.1 & (for n st 0 <> n & n < len F holds
f.(n + 1) = g.(f.n,F.(n + 1))) & d = f.(len F)) implies d = g "**" F;

definition let B,A be non empty set, b be Element of B;
redefine func A --> b -> Function of A,B;
end;

definition let A be non empty set,
F be Function of NAT,A, p be FinSequence of A;
redefine func F +* p -> Function of NAT,A;
end;

definition let f be FinSequence;
redefine func dom f -> Element of Fin NAT;
end;

theorem :: FINSOP_1:4
(g has_a_unity or len F >= 1) & g is associative & g is commutative implies
g "**" F = g \$\$(dom F,(NAT-->the_unity_wrt g)+*F);

theorem :: FINSOP_1:5
g has_a_unity or len F >= 1 implies g "**" (F ^ <* d *>) = g.(g "**" F,d);

theorem :: FINSOP_1:6
g is associative & (g has_a_unity or len F >= 1 & len G >= 1) implies
g "**" (F ^ G) = g.(g "**" F,g "**" G);

theorem :: FINSOP_1:7
g is associative & (g has_a_unity or len F >= 1) implies
g "**" (<* d *> ^ F) = g.(d,g "**" F);

theorem :: FINSOP_1:8
g is commutative associative & (g has_a_unity or len F >= 1) &
G = F * P implies g "**" F = g "**" G;

theorem :: FINSOP_1:9
(g has_a_unity or len F >= 1) & g is associative commutative &
F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G
;

theorem :: FINSOP_1:10
g is associative commutative & (g has_a_unity or len F >= 1) &
len F = len G & len F = len H &
(for k st k in dom F holds F.k = g.(G.k,H.k)) implies
g "**" F = g.(g "**" G,g "**" H);

theorem :: FINSOP_1:11
g has_a_unity implies g "**" <*>D = the_unity_wrt g;

theorem :: FINSOP_1:12
g "**" <* d *> = d;

theorem :: FINSOP_1:13
g "**" <* d1,d2 *> = g.(d1,d2);

theorem :: FINSOP_1:14
g is commutative implies g "**" <* d1,d2 *> = g "**" <* d2,d1 *>;

theorem :: FINSOP_1:15
g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3);

theorem :: FINSOP_1:16
g is commutative implies g "**" <* d1,d2,d3 *> = g "**" <* d2,d1,d3 *>;

theorem :: FINSOP_1:17
g "**" (1 |-> d) = d;

theorem :: FINSOP_1:18
g "**" (2 |-> d) = g.(d,d);

theorem :: FINSOP_1:19
g is associative & (g has_a_unity or k <> 0 & l <> 0) implies
g "**" ((k + l) |-> d) = g.(g "**" (k |-> d),g "**" (l |-> d));

theorem :: FINSOP_1:20
g is associative & (g has_a_unity or k <> 0 & l <> 0) implies
g "**" (k * l |-> d) = g "**" (l |-> (g "**" (k |-> d)));

theorem :: FINSOP_1:21
len F = 1 implies g "**" F = F.1;

theorem :: FINSOP_1:22
len F = 2 implies g "**" F = g.(F.1,F.2);