:: Reper Algebras
:: by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992-2017 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 SUBSET_1, NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_3, ORDINAL4,
XXREAL_0, NAT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_2, FUNCT_4, MIDSP_1,
STRUCT_0, BINOP_1, QC_LANG1, PRE_TOPC, CARD_1, TARSKI, MIDSP_2, VECTSP_1,
GROUP_4, SUPINF_2, ROBBINS1, MIDSP_3;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FUNCT_1, FUNCT_2, BINOP_1,
STRUCT_0, ALGSTR_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, ORDINAL1, NUMBERS,
NAT_1, FUNCT_7, MIDSP_1, MIDSP_2, XXREAL_0;
constructors BINOP_1, NAT_1, FINSEQ_2, FUNCT_7, MIDSP_2, RELSET_1;
registrations RELSET_1, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve n,i,j,k,l for Nat;
reserve D for non empty set;
reserve c,d for Element of D;
reserve p,q,q9,r for FinSequence of D;
theorem :: MIDSP_3:1
len p = j+1+k implies ex q,r,c st len q = j & len r = k & p = q^<*c*>^ r;
theorem :: MIDSP_3:2
i in Seg n implies ex j,k st n = j+1+k & i = j+1;
theorem :: MIDSP_3:3
p = q^<*c*>^r & i = len q + 1 implies (for l st 1 <= l & l <= len q
holds p.l = q.l) & p.i = c & for l st i + 1 <= l & l <= len p holds p.l = r.(l-
i);
theorem :: MIDSP_3:4
l<=j or l=j+1 or j+2<=l;
theorem :: MIDSP_3:5
l in Seg(n)\{i} & i=j+1 implies 1<=l & l<=j or i+1<=l & l<=n;
definition
let D,n;
let p be Element of n-tuples_on D;
let i,d;
redefine func p+*(i,d) -> Element of n-tuples_on D;
end;
::Section 2: Reper Algebra Structure and its properties
begin
definition
let n;
struct(MidStr) ReperAlgebraStr over n (#carrier -> set, MIDPOINT -> BinOp of
the carrier, reper -> Function of n-tuples_on the carrier, the carrier#);
end;
registration
let n;
let A be non empty set, m be BinOp of A, r be Function of n-tuples_on A,A;
cluster ReperAlgebraStr(#A,m,r#) -> non empty;
end;
registration
let n;
cluster non empty for ReperAlgebraStr over n;
end;
registration
let n;
cluster MidSp-like for non empty ReperAlgebraStr over n+2;
end;
reserve RAS for MidSp-like non empty ReperAlgebraStr over n+2;
reserve a,b,d,pii,p9i for Point of RAS;
definition
let n,RAS,i;
mode Tuple of i,RAS is Element of i-tuples_on the carrier of RAS;
end;
reserve p,q for Tuple of (n+1),RAS;
definition
let n,RAS,a;
redefine func <*a*> -> Tuple of 1,RAS;
end;
definition
let n,RAS,i,j;
let p be Tuple of i,RAS, q be Tuple of j,RAS;
redefine func p^q -> Tuple of (i+j),RAS;
end;
definition
let n,RAS,a,p;
func *'(a,p) -> Point of RAS equals
:: MIDSP_3:def 1
(the reper of RAS).(<*a*>^p);
end;
theorem :: MIDSP_3:6
i in Seg(n+1) implies (p+*(i,d)).i = d & for l st l in (dom p)\{i}
holds (p+*(i,d)).l = p.l;
definition
let n;
mode Nat of n -> Nat means
:: MIDSP_3:def 2
1<=it & it<=n+1;
end;
reserve m for Nat of n;
theorem :: MIDSP_3:7
i is Nat of n iff i in Seg(n+1);
theorem :: MIDSP_3:8
i<=n implies i+1 is Nat of n;
theorem :: MIDSP_3:9
(for m holds p.m = q.m) implies p = q;
theorem :: MIDSP_3:10
for l being Nat of n st l=i holds (p+*(i,d)).l = d;
definition
let n,D;
let p be Element of (n+1)-tuples_on D;
let m;
redefine func p.m -> Element of D;
end;
definition
let n,RAS;
attr RAS is being_invariance means
:: MIDSP_3:def 3
for a,b,p,q st (for m holds a@(q.m ) = b@(p.m)) holds a@*'(b,q) = b@*'(a,p);
end;
definition
let n,RAS,p,i,a;
redefine func p+*(i,a) -> Tuple of (n+1),RAS;
end;
definition
let n,i,RAS;
pred RAS has_property_of_zero_in i means
:: MIDSP_3:def 4
for a,p holds *'(a,(p+*(i,a) )) = a;
end;
definition
let n,i,RAS;
pred RAS is_semi_additive_in i means
:: MIDSP_3:def 5
for a,pii,p st p.i = pii holds *'(a,(p+*(i,a@pii))) = a@*'(a,p);
end;
theorem :: MIDSP_3:11
RAS is_semi_additive_in m implies for a,d,p,q st q = (p+*(m,d))
holds *'(a,(p+*(m,a@d))) = a@*'(a,q);
definition
let n,i,RAS;
pred RAS is_additive_in i means
:: MIDSP_3:def 6
for a,pii,p9i,p st p.i = pii holds *'
(a,(p+*(i,pii@p9i))) = *'(a,p)@*'(a,(p+*(i,p9i)));
end;
definition
let n,i,RAS;
pred RAS is_alternative_in i means
:: MIDSP_3:def 7
for a,p,pii st p.i = pii holds *'( a,(p+*(i+1,pii))) = a;
end;
reserve W for ATLAS of RAS;
reserve v for Vector of W;
definition
let n,RAS,W,i;
mode Tuple of i,W is Element of i-tuples_on the carrier of the algebra of W;
end;
reserve x,y for Tuple of (n+1),W;
theorem :: MIDSP_3:12
i in Seg(n+1) implies (x+*(i,v)).i = v & for l st l in (dom x)\{i}
holds (x+*(i,v)).l = x.l;
theorem :: MIDSP_3:13
(for l being Nat of n st l=i holds (x+*(i,v)).l = v) & for l,i
being Nat of n st l<>i holds (x+*(i,v)).l = x.l;
theorem :: MIDSP_3:14
(for m holds x.m = y.m) implies x = y;
scheme :: MIDSP_3:sch 1
SeqLambdaD9{n()->Nat,D()->non empty set, F(set)->Element of D()}:
ex z being FinSequence of D() st len z = n()+1 & for j being Nat of n() holds z
.j = F(j);
definition
let n,RAS,W,a,x;
func (a,x).W -> Tuple of (n+1),RAS means
:: MIDSP_3:def 8
it.m = (a,x.m).W;
end;
definition
let n,RAS,W,a,p;
func W.(a,p) -> Tuple of (n+1),W means
:: MIDSP_3:def 9
it.m = W.(a,p.m);
end;
theorem :: MIDSP_3:15
W.(a,p) = x iff (a,x).W = p;
theorem :: MIDSP_3:16
W.(a,(a,x).W) = x;
theorem :: MIDSP_3:17
(a,W.(a,p)).W = p;
definition
let n,RAS,W,a,x;
func Phi(a,x) -> Vector of W equals
:: MIDSP_3:def 10
W.(a,*'(a,(a,x).W));
end;
theorem :: MIDSP_3:18
W.(a,p) = x & W.(a,b) = v implies (*'(a,p) = b iff Phi(a,x) = v);
theorem :: MIDSP_3:19
RAS is being_invariance iff for a,b,x holds Phi(a,x) = Phi(b,x);
theorem :: MIDSP_3:20
1 in Seg(n+1);
theorem :: MIDSP_3:21
1 is Nat of n;
::Section 3: Reper Algebra and its atlas
begin
definition
let n;
mode ReperAlgebra of n -> MidSp-like non empty ReperAlgebraStr over n+2
means
:: MIDSP_3:def 11
it is being_invariance;
end;
reserve RAS for ReperAlgebra of n;
reserve a,b,pm,p9m,p99m for Point of RAS;
reserve p for Tuple of (n+1),RAS;
reserve W for ATLAS of RAS;
reserve v for Vector of W;
reserve x for Tuple of (n+1),W;
theorem :: MIDSP_3:22
Phi(a,x) = Phi(b,x);
definition
let n,RAS,W,x;
func Phi(x) -> Vector of W means
:: MIDSP_3:def 12
for a holds it = Phi(a,x);
end;
theorem :: MIDSP_3:23
W.(a,p) = x & W.(a,b) = v & Phi(x) = v implies *'(a,p) = b;
theorem :: MIDSP_3:24
(a,x).W = p & (a,v).W = b & *'(a,p) = b implies Phi(x) = v;
theorem :: MIDSP_3:25
W.(a,p) = x & W.(a,b) = v implies W.(a,(p+*(m,b))) = (x+*(m,v));
theorem :: MIDSP_3:26
(a,x).W = p & (a,v).W = b implies (a,(x+*(m,v))).W = (p+*(m,b));
theorem :: MIDSP_3:27
RAS has_property_of_zero_in m iff for x holds Phi((x+*(m,0.W))) = 0.W;
theorem :: MIDSP_3:28
RAS is_semi_additive_in m iff for x holds Phi((x+*(m,Double(x.m)
))) = Double Phi(x);
theorem :: MIDSP_3:29
RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS
is_semi_additive_in m;
theorem :: MIDSP_3:30
RAS has_property_of_zero_in m implies (RAS is_additive_in m iff for x,
v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi ((x+*(m,v))));
theorem :: MIDSP_3:31
W.(a,p) = x & m<= n implies W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m) );
theorem :: MIDSP_3:32
(a,x).W = p & m<=n implies (a,(x+*(m+1,x.m))).W = (p+*(m+1,p.m));
theorem :: MIDSP_3:33
m<=n implies (RAS is_alternative_in m iff for x holds Phi((x+*(m+1,x.m
))) = 0. W );