The Mizar abstract of FINSEQOP

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Binary Operations Applied to Finite Sequences
by
Czeslaw Bylinski
Received May 4, 1990
MML identifier: FINSEQOP
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_1, PARTFUN1, BOOLE, RELAT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
      BINOP_1, SETWISEO, FINSEQOP;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1,
      FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2,
      SETWISEO;
 constructors NAT_1, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO, RELAT_2,
      PARTFUN1, XBOOLE_0;
 clusters SUBSET_1, RELAT_1, FUNCT_1, FINSEQ_2, RELSET_1, FUNCOP_1, ARYTM_3,
      ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET;


begin

 reserve x,y for set;
 reserve C,C',D,D',E for non empty set;
 reserve c for Element of C;
 reserve c' for Element of C';
 reserve d,d1,d2,d3,d4,e for Element of D;
 reserve d' for Element of D';

:: Auxiliary theorems

theorem :: FINSEQOP:1
   for f being Function holds <:{},f:> = {} & <:f,{}:> = {};

theorem :: FINSEQOP:2
     for f being Function holds [:{},f:] = {} & [:f,{}:] = {};

canceled;

theorem :: FINSEQOP:4
   for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {};

theorem :: FINSEQOP:5
     for F being Function holds F[:]({},x) = {};

theorem :: FINSEQOP:6
     for F being Function holds F[;](x,{}) = {};

theorem :: FINSEQOP:7
   for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[x1,x2];

theorem :: FINSEQOP:8
   for F being Function,X being set, x1,x2 being set st [x1,x2] in dom F
    holds F.:(X-->x1,X-->x2) = X -->(F.[x1,x2]);

 reserve i,j for Nat;

 reserve F for Function of [:D,D':],E;
 reserve p,q for FinSequence of D, p',q' for FinSequence of D';

definition let D,D',E,F,p,p';
 redefine func F.:(p,p') -> FinSequence of E;
end;

definition let D,D',E,F,p,d';
 redefine func F[:](p,d') -> FinSequence of E;
end;

definition let D,D',E,F,d,p';
 redefine func F[;](d,p') -> FinSequence of E;
end;

definition let D,i,d;
 redefine func i|-> d -> Element of i-tuples_on D;
end;

 reserve f,f' for Function of C,D,
         h for Function of D,E;

definition let D,E be set, p be FinSequence of D, h be Function of D,E;
 redefine func h*p -> FinSequence of E;
end;

theorem :: FINSEQOP:9
   h*(p^<*d*>) = (h*p)^<*h.d*>;

theorem :: FINSEQOP:10
     h*(p^q) = (h*p)^(h*q);

 reserve T,T1,T2,T3 for Element of i-tuples_on D;
 reserve T' for Element of i-tuples_on D';
 reserve S,S1 for Element of j-tuples_on D;
 reserve S',S1' for Element of j-tuples_on D';

theorem :: FINSEQOP:11
   F.:(T^<*d*>,T'^<*d'*>) = (F.:(T,T'))^<*F.(d,d')*>;

theorem :: FINSEQOP:12
     F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S'));

theorem :: FINSEQOP:13
   F[;](d,p'^<*d'*>) = (F[;](d,p'))^<*F.(d,d')*>;

theorem :: FINSEQOP:14
     F[;](d,p'^q') = (F[;](d,p'))^(F[;](d,q'));

theorem :: FINSEQOP:15
   F[:](p^<*d*>,d') = (F[:](p,d'))^<*F.(d,d')*>;

theorem :: FINSEQOP:16
     F[:](p^q,d') = (F[:](p,d'))^(F[:](q,d'));

theorem :: FINSEQOP:17
     for h being Function of D,E holds h*(i|->d) = i|->(h.d);

theorem :: FINSEQOP:18
   F.:(i|->d,i|->d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:19
     F[;](d,i|->d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:20
     F[:](i|->d,d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:21
     F.:(i|->d,T') = F[;](d,T');

theorem :: FINSEQOP:22
     F.:(T,i|->d) = F[:](T,d);

theorem :: FINSEQOP:23
     F[;](d,T') = F[;](d,id D')*T';

theorem :: FINSEQOP:24
     F[:](T,d) = F[:](id D,d)*T;

:: Binary Operations

 reserve F,G for BinOp of D;
 reserve u for UnOp of D;
 reserve H for BinOp of E;

theorem :: FINSEQOP:25
   F is associative implies F[;](d,id D)*(F.:(f,f')) = F.:(F[;](d,id D)*f,f');

theorem :: FINSEQOP:26
   F is associative implies F[:](id D,d)*(F.:(f,f')) = F.:(f,F[:](id D,d)*f');

theorem :: FINSEQOP:27
 F is associative implies F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*T1,T2);

theorem :: FINSEQOP:28
 F is associative implies F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,d)*T2);

theorem :: FINSEQOP:29
 F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3));

theorem :: FINSEQOP:30
     F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2));

theorem :: FINSEQOP:31
     F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2));

theorem :: FINSEQOP:32
     F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T));

theorem :: FINSEQOP:33
     F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2);

theorem :: FINSEQOP:34
     F is commutative implies F.:(T1,T2) = F.:(T2,T1);

theorem :: FINSEQOP:35
     F is commutative implies F[;](d,T) = F[:](T,d);

theorem :: FINSEQOP:36
   F is_distributive_wrt G implies F[;](G.(d1,d2),f) = G.:(F[;](d1,f),F[;]
(d2,f));

theorem :: FINSEQOP:37
   F is_distributive_wrt G implies F[:](f,G.(d1,d2)) = G.:(F[:](f,d1),F[:]
(f,d2));

theorem :: FINSEQOP:38
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F.:(f,f')) = H.:(h*f,h*f');

theorem :: FINSEQOP:39
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F[;](d,f)) = H[;](h.d,h*f);

theorem :: FINSEQOP:40
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F[:](f,d)) = H[:](h*f,h.d);

theorem :: FINSEQOP:41
     u is_distributive_wrt F implies u*(F.:(f,f')) = F.:(u*f,u*f');

theorem :: FINSEQOP:42
     u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f);

theorem :: FINSEQOP:43
     u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d);

theorem :: FINSEQOP:44
   F has_a_unity implies
     F.:(C-->the_unity_wrt F,f) = f & F.:(f,C-->the_unity_wrt F) = f;

theorem :: FINSEQOP:45
   F has_a_unity implies F[;](the_unity_wrt F,f) = f;

theorem :: FINSEQOP:46
   F has_a_unity implies F[:](f,the_unity_wrt F) = f;

theorem :: FINSEQOP:47
     F is_distributive_wrt G implies F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F[;]
(d2,T));

theorem :: FINSEQOP:48
     F is_distributive_wrt G implies F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F[:]
(T,d2));

theorem :: FINSEQOP:49
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F.:(T1,T2)) = H.:(h*T1,h*T2);

theorem :: FINSEQOP:50
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F[;](d,T)) = H[;](h.d,h*T);

theorem :: FINSEQOP:51
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h*(F[:](T,d)) = H[:](h*T,h.d);

theorem :: FINSEQOP:52
     u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2);

theorem :: FINSEQOP:53
     u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T);

theorem :: FINSEQOP:54
     u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d);

theorem :: FINSEQOP:55
     G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F
;

theorem :: FINSEQOP:56
     G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F
;

theorem :: FINSEQOP:57
     F has_a_unity implies
      F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T;

theorem :: FINSEQOP:58
     F has_a_unity implies F[;](the_unity_wrt F,T) = T;

theorem :: FINSEQOP:59
     F has_a_unity implies F[:](T,the_unity_wrt F) = T;

definition let D,u,F;
 pred u is_an_inverseOp_wrt F means
:: FINSEQOP:def 1

   for d holds F.(d,u.d) = the_unity_wrt F & F.(u.d,d) = the_unity_wrt F;
end;

definition let D,F;
 attr F is having_an_inverseOp means
:: FINSEQOP:def 2
 ex u st u is_an_inverseOp_wrt F;
  synonym F has_an_inverseOp;
end;

definition let D,F;
 assume that
 F has_a_unity and
 F is associative and
 F has_an_inverseOp;
 func the_inverseOp_wrt F -> UnOp of D means
:: FINSEQOP:def 3
 it is_an_inverseOp_wrt F;
end;

canceled 3;

theorem :: FINSEQOP:63
   F has_a_unity & F is associative & F has_an_inverseOp
    implies F.((the_inverseOp_wrt F).d,d) = the_unity_wrt F &
      F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F;

theorem :: FINSEQOP:64
   F has_a_unity & F is associative &
     F has_an_inverseOp & F.(d1,d2) = the_unity_wrt F
    implies d1 = (the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2;

theorem :: FINSEQOP:65
   F has_a_unity & F is associative & F has_an_inverseOp
    implies (the_inverseOp_wrt F).(the_unity_wrt F) = the_unity_wrt F;

theorem :: FINSEQOP:66
   F has_a_unity & F is associative & F has_an_inverseOp
    implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d;

theorem :: FINSEQOP:67
   F has_a_unity & F is associative & F is commutative & F has_an_inverseOp
    implies (the_inverseOp_wrt F) is_distributive_wrt F;

theorem :: FINSEQOP:68
   F has_a_unity & F is associative & F has_an_inverseOp &
    (F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 = d2;

theorem :: FINSEQOP:69
   F has_a_unity & F is associative & F has_an_inverseOp &
    (F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 = the_unity_wrt F;

theorem :: FINSEQOP:70
   F is associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F & e = the_unity_wrt F
     implies for d holds G.(e,d) = e & G.(d,e) = e;

theorem :: FINSEQOP:71
   F has_a_unity & F is associative & F has_an_inverseOp &
     u = the_inverseOp_wrt F & G is_distributive_wrt F
      implies u.(G.(d1,d2)) = G.(u.d1,d2) & u.(G.(d1,d2)) = G.(d1,u.d2);

theorem :: FINSEQOP:72
     F has_a_unity & F is associative & F has_an_inverseOp &
     u = the_inverseOp_wrt F & G is_distributive_wrt F & G has_a_unity
      implies G[;](u.(the_unity_wrt G),id D) = u;

theorem :: FINSEQOP:73
     F is associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
     implies G[;](d,id D).the_unity_wrt F = the_unity_wrt F;

theorem :: FINSEQOP:74
     F is associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
     implies G[:](id D,d).the_unity_wrt F = the_unity_wrt F;

theorem :: FINSEQOP:75
   F has_a_unity & F is associative & F has_an_inverseOp implies
     F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F &
     F.:((the_inverseOp_wrt F)*f,f) = C-->the_unity_wrt F;

theorem :: FINSEQOP:76
   F is associative & F has_an_inverseOp &
    F has_a_unity & F.:(f,f') = C-->the_unity_wrt F implies
     f = (the_inverseOp_wrt F)*f' & (the_inverseOp_wrt F)*f = f';

theorem :: FINSEQOP:77
     F has_a_unity & F is associative & F has_an_inverseOp implies
     F.:(T,(the_inverseOp_wrt F)*T) = i|->the_unity_wrt F &
     F.:((the_inverseOp_wrt F)*T,T) = i|->the_unity_wrt F;

theorem :: FINSEQOP:78
     F is associative & F has_an_inverseOp &
    F has_a_unity & F.:(T1,T2) = i|->the_unity_wrt F implies
     T1 = (the_inverseOp_wrt F)*T2 & (the_inverseOp_wrt F)*T1 = T2;

theorem :: FINSEQOP:79
   F is associative & F has_a_unity & e = the_unity_wrt F &
    F has_an_inverseOp & G is_distributive_wrt F
     implies G[;](e,f) = C-->e;

theorem :: FINSEQOP:80
     F is associative & F has_a_unity & e = the_unity_wrt F &
    F has_an_inverseOp & G is_distributive_wrt F
     implies G[;](e,T) = i|->e;

definition
 let F,f,g be Function;
  func F*(f,g) -> Function equals
:: FINSEQOP:def 4
  F*[:f,g:];
end;

canceled;

theorem :: FINSEQOP:82
   for F,f,g being Function st [x,y] in dom(F*(f,g))
    holds (F*(f,g)).[x,y] = F.[f.x,g.y];

theorem :: FINSEQOP:83
   for F,f,g being Function st [x,y] in dom(F*(f,g))
     holds (F*(f,g)).(x,y) = F.(f.x,g.y);

theorem :: FINSEQOP:84
   for F being Function of [:D,D':],E,
       f being Function of C,D, g being Function of C',D'
     holds F*(f,g) is Function of [:C,C':],E;

theorem :: FINSEQOP:85
    for u,u' being Function of D,D holds F*(u,u') is BinOp of D;

definition let D,F; let f,f' be Function of D,D;
 redefine func F*(f,f') -> BinOp of D;
end;

theorem :: FINSEQOP:86
   for F being Function of [:D,D':],E,
       f being Function of C,D, g being Function of C',D'
     holds (F*(f,g)).(c,c') = F.(f.c,g.c');

theorem :: FINSEQOP:87
   for u being Function of D,D holds
    (F*(id D,u)).(d1,d2) = F.(d1,u.d2) & (F*(u,id D)).(d1,d2) = F.(u.d1,d2);

theorem :: FINSEQOP:88
   (F*(id D,u)).:(f,f') = F.:(f,u*f');

theorem :: FINSEQOP:89
     (F*(id D,u)).:(T1,T2) = F.:(T1,u*T2);

theorem :: FINSEQOP:90
     F is associative & F has_a_unity & F is commutative &
    F has_an_inverseOp & u = the_inverseOp_wrt F
      implies u.(F*(id D,u).(d1,d2)) = F*(u,id D).(d1,d2) &
         F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2));

theorem :: FINSEQOP:91
     F is associative & F has_a_unity & F has_an_inverseOp implies
     (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F;


theorem :: FINSEQOP:92
     F is associative & F has_a_unity & F has_an_inverseOp
     implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d;

theorem :: FINSEQOP:93
     F is associative & F has_a_unity &
     F has_an_inverseOp & u = the_inverseOp_wrt F
      implies (F*(id D,u)).(the_unity_wrt F,d) = u.d;

theorem :: FINSEQOP:94
     F is commutative & F is associative & F has_a_unity &
    F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies
     for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4));
The abstract of the Mizar article:

Binary Operations Applied to Finite Sequences
