:: Binary Operations on Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2,
RELAT_1, FINSEQ_2, SETWISEO, XXREAL_0, CARD_1, ARYTM_3, FUNCOP_1, TARSKI,
FUNCT_4, FINSUB_1, ORDINAL4, NAT_1, ARYTM_1, PARTFUN1, FINSOP_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, BINOP_1,
PARTFUN1, FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1,
FINSUB_1, SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4, XXREAL_0;
constructors BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4, SETWISEO, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_2, FINSEQ_4, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, XXREAL_0,
XREAL_0, FINSEQ_1, CARD_1, FINSEQ_2, NAT_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 sequence of D,
g for BinOp of D,
k,n,i,l for Nat,
P for Permutation of dom F;
definition
let D,F,g;
assume
g is having_a_unity or len F >= 1;
func g "**" F -> Element of D means
:: FINSOP_1:def 1
it = the_unity_wrt g if g is having_a_unity & len F = 0
otherwise ex f st f.1 = F.1 & (for n being Nat st 0 <> n & n <
len F holds f.(n + 1) = g.(f.n,F.(n + 1))) & it = f.(len F);
end;
theorem :: FINSOP_1:1
len F >= 1 implies ex f st f.1 = F.1 &
(for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n + 1))) & g "**" F = f.(len F);
theorem :: FINSOP_1:2
len F >= 1 & (ex f st f.1 = F.1 &
(for n being Nat 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 A be non empty set, F be sequence of A, p be FinSequence of A;
redefine func F +* p -> sequence of A;
end;
notation
let f be FinSequence;
synonym findom f for dom f;
end;
definition
let f be FinSequence;
redefine func findom f -> Element of Fin NAT;
end;
theorem :: FINSOP_1:3
(g is having_a_unity or len F >= 1) & g is associative & g is
commutative implies g "**" F = g $$(findom F,(NAT-->the_unity_wrt g)+*F);
theorem :: FINSOP_1:4
g is having_a_unity or len F >= 1 implies g "**" (F ^ <* d *>) =
g.(g "**" F,d);
theorem :: FINSOP_1:5
g is associative & (g is having_a_unity or len F >= 1 & len G >=
1) implies g "**" (F ^ G) = g.(g "**" F,g "**" G);
theorem :: FINSOP_1:6
g is associative & (g is having_a_unity or len F >= 1) implies g
"**" (<* d *> ^ F) = g.(d,g "**" F);
theorem :: FINSOP_1:7
g is commutative associative & (g is having_a_unity or len F >= 1
) & G = F * P implies g "**" F = g "**" G;
theorem :: FINSOP_1:8
(g is having_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:9
g is associative commutative & (g is having_a_unity or len F >= 1) &
len F = len G & len F = len H &
(for k being Nat st k in dom F holds F.k = g.(G.k,H.k))
implies g "**" F = g.(g "**" G,g "**" H);
theorem :: FINSOP_1:10
g is having_a_unity implies g "**" <*>D = the_unity_wrt g;
theorem :: FINSOP_1:11
g "**" <* d *> = d;
theorem :: FINSOP_1:12
g "**" <* d1,d2 *> = g.(d1,d2);
theorem :: FINSOP_1:13
g is commutative implies g "**" <* d1,d2 *> = g "**" <* d2,d1 *>;
theorem :: FINSOP_1:14
g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3);
theorem :: FINSOP_1:15
g is commutative implies g "**" <* d1,d2,d3 *> = g "**" <* d2,d1,d3 *>;
theorem :: FINSOP_1:16
g "**" (1 |-> d) = d;
theorem :: FINSOP_1:17
g "**" (2 |-> d) = g.(d,d);
theorem :: FINSOP_1:18
g is associative & (g is having_a_unity or k <> 0 & l <> 0)
implies g "**" ((k + l) |-> d) = g.(g "**" (k |-> d),g "**" (l |-> d));
theorem :: FINSOP_1:19
g is associative & (g is having_a_unity or k <> 0 & l <> 0) implies g
"**" (k * l |-> d) = g "**" (l |-> (g "**" (k |-> d)));
theorem :: FINSOP_1:20
len F = 1 implies g "**" F = F.1;
theorem :: FINSOP_1:21
len F = 2 implies g "**" F = g.(F.1,F.2);