:: Representation Theorem for Stacks :: by Grzegorz Bancerek :: :: Received February 22, 2011 :: Copyright (c) 2011-2018 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 STACKS_1, XBOOLE_0, STRUCT_0, ZFMISC_1, SUBSET_1, FUNCT_1, NUMBERS, NAT_1, TARSKI, ARYTM_3, RELAT_1, FINSEQ_1, FINSEQ_3, ORDINAL4, FUNCOP_1, PARTFUN1, CARD_1, XXREAL_0, COMPLEX1, GLIB_000, RELAT_2, EQREL_1, FILTER_1, BINOP_1, MCART_1, ORDERS_1, WELLORD1, ARYTM_1, SETFAM_1, FUNCT_2, AOFA_000, PBOOLE, FUNCT_4, MATRIX_7, REWRITE1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, ORDERS_1, FUNCT_4, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FINSEQ_1, FINSEQ_2, EQREL_1, FINSEQ_3, PBOOLE, FUNCT_7, STRUCT_0, FILTER_1, REWRITE1, ABCMIZ_1, AOFA_000; constructors BINOP_1, DOMAIN_1, XXREAL_0, RELSET_1, FILTER_1, FUNCT_7, REWRITE1, ABCMIZ_1, POLYNOM3, NAT_D; registrations XBOOLE_0, RELSET_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, NAT_1, ORDINAL1, XXREAL_0, XREAL_0, CARD_1, EQREL_1, SUBSET_1, REWRITE1, FUNCT_4; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries reserve i,j for Nat; reserve x,y for set; definition let A be set; let s1,s2 be FinSequence of A; redefine func s1^s2 -> Element of A*; end; definition let A be set; let i be Nat; let s be FinSequence of A; redefine func Del(s,i) -> Element of A*; end; theorem :: STACKS_1:1 Del({},i) = {}; scheme :: STACKS_1:sch 1 IndSeqD{D()->non empty set, P[set]}: for p being FinSequence of D() holds P[p] provided P[<*> D()] and for p being FinSequence of D() for x being Element of D() st P[p] holds P[<*x*>^p]; definition let C,D be non empty set; let R be Relation; mode BinOp of C,D,R -> Function of [:C,D:],D means :: STACKS_1:def 1 for x being Element of C,y1,y2 being Element of D st [y1,y2] in R holds [it.(x,y1),it.(x,y2)] in R; end; scheme :: STACKS_1:sch 2 LambdaD2{ A,B,C() -> non empty set, F(object,object) -> Element of C() }: ex M being Function of [:A(),B():],C() st for i being Element of A(), j being Element of B() holds M.(i,j) = F(i,j); definition let C,D be non empty set; let R be Equivalence_Relation of D; let b be Function of [:C,D:],D; assume b is BinOp of C,D,R; func b /\/ R -> Function of [:C, Class R:], Class R means :: STACKS_1:def 2 for x,y,y1 be set st x in C & y in Class R & y1 in y holds it.(x,y) = Class(R,b.(x,y1)); end; definition let A,B be non empty set; let C be Subset of A; let D be Subset of B; let f be Function of A,B; let g be Function of C,D; redefine func f+*g -> Function of A,B; end; begin :: Stack Algebra definition struct(2-sorted) StackSystem(# carrier -> set, :: elements carrier' -> set, :: stacks s_empty -> Subset of the carrier', s_push -> Function of [:the carrier, the carrier':], the carrier', s_pop -> Function of the carrier', the carrier', s_top -> Function of the carrier', the carrier #); end; registration let a1 be non empty set, a2 be set, a3 be Subset of a2, a4 be Function of [:a1, a2:], a2, a5 be Function of a2, a2, a6 be Function of a2, a1; cluster StackSystem(#a1,a2,a3,a4,a5,a6#) -> non empty; end; registration let a1 be set, a2 be non empty set, a3 be Subset of a2, a4 be Function of [:a1, a2:], a2, a5 be Function of a2, a2, a6 be Function of a2, a1; cluster StackSystem(#a1,a2,a3,a4,a5,a6#) -> non void; end; registration cluster non empty non void strict for StackSystem; end; definition let X be StackSystem; mode stack of X is Element of the carrier' of X; end; definition let X be StackSystem; let s be stack of X; pred emp s means :: STACKS_1:def 3 s in the s_empty of X; end; definition let X be non void StackSystem; let s be stack of X; func pop s -> stack of X equals :: STACKS_1:def 4 (the s_pop of X).s; func top s -> Element of X equals :: STACKS_1:def 5 (the s_top of X).s; end; definition let X be non empty non void StackSystem; let s be stack of X; let e be Element of X; func push(e,s) -> stack of X equals :: STACKS_1:def 6 (the s_push of X).(e,s); end; definition let A be non empty set; func StandardStackSystem A -> non empty non void strict StackSystem means :: STACKS_1:def 7 the carrier of it = A & the carrier' of it = A* & for s being stack of it holds (emp s iff s is empty) & for g being FinSequence st g = s holds (not emp s implies top s = g.1 & pop s = Del(g,1)) & (emp s implies top s = the Element of it & pop s = {}) & for e being Element of it holds push(e,s) = <*e*>^g; end; reserve A for non empty set; reserve c for Element of StandardStackSystem A; reserve m for stack of StandardStackSystem A; registration let A; cluster the carrier' of StandardStackSystem A -> functional; end; registration let A; cluster -> FinSequence-like for stack of StandardStackSystem A; end; ::\$H- reserve X for non empty non void StackSystem; reserve s,s1,s2 for stack of X; reserve e,e1,e2 for Element of X; definition let X; attr X is pop-finite means :: STACKS_1:def 8 for f being sequence of the carrier' of X ex i being Nat, s st f.i = s & (not emp s implies f.(i+1) <> pop s); attr X is push-pop means :: STACKS_1:def 9 not emp s implies s = push(top s, pop s); attr X is top-push means :: STACKS_1:def 10 e = top push(e,s); attr X is pop-push means :: STACKS_1:def 11 s = pop push(e,s); attr X is push-non-empty means :: STACKS_1:def 12 not emp push(e,s); end; registration let A be non empty set; cluster StandardStackSystem A -> pop-finite; cluster StandardStackSystem A -> push-pop; cluster StandardStackSystem A -> top-push; cluster StandardStackSystem A -> pop-push; cluster StandardStackSystem A -> push-non-empty; end; registration cluster pop-finite push-pop top-push pop-push push-non-empty strict for non empty non void StackSystem; end; definition mode StackAlgebra is pop-finite push-pop top-push pop-push push-non-empty non empty non void StackSystem; end; theorem :: STACKS_1:2 for X being non empty non void StackSystem st X is pop-finite ex s being stack of X st emp s; registration let X be pop-finite non empty non void StackSystem; cluster the s_empty of X -> non empty; end; theorem :: STACKS_1:3 X is top-push pop-push & push(e1,s1) = push(e2,s2) implies e1 = e2 & s1 = s2; theorem :: STACKS_1:4 X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 implies s1 = s2; begin :: Schemes of Induction scheme :: STACKS_1:sch 3 INDsch{X() -> StackAlgebra, s() -> stack of X(), P[set]}: P[s()] provided for s being stack of X() st emp s holds P[s] and for s being stack of X(), e being Element of X() st P[s] holds P[push(e,s)]; scheme :: STACKS_1:sch 4 EXsch{X() -> StackAlgebra, s() -> stack of X(), A() -> non empty set, e() -> Element of A(), d(set,set) -> Element of A()}: ex a being Element of A() st ex F being Function of the carrier' of X(), A() st a = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) & for s1 being stack of X(), e being Element of X() holds F.push(e,s1) = d(e,F.s1); scheme :: STACKS_1:sch 5 UNIQsch{X() -> StackAlgebra, s() -> stack of X(), A() -> non empty set, e() -> Element of A(), d(set,set) -> Element of A()}: for a1,a2 being Element of A() st (ex F being Function of the carrier' of X(), A() st a1 = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) & for s1 being stack of X(), e being Element of X() holds F.push(e,s1) = d(e,F.s1)) & (ex F being Function of the carrier' of X(), A() st a2 = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) & for s1 being stack of X(), e being Element of X() holds F.push(e,s1) = d(e,F.s1)) holds a1 = a2; begin :: Stack Congruence reserve X for StackAlgebra; reserve s,s1,s2,s3 for stack of X; reserve e,e1,e2,e3 for Element of X; definition let X,s; func |.s.| -> Element of (the carrier of X)* means :: STACKS_1:def 13 ex F being Function of the carrier' of X, (the carrier of X)* st it = F.s & (for s1 st emp s1 holds F.s1 = {}) & for s1, e holds F.push(e,s1) = <*e*>^(F.s1); end; theorem :: STACKS_1:5 emp s implies |.s.| = {}; theorem :: STACKS_1:6 not emp s implies |.s.| = <*top s*>^|.pop s.|; theorem :: STACKS_1:7 not emp s implies |.pop s.| = Del(|.s.|,1); theorem :: STACKS_1:8 |.push(e,s).| = <*e*>^|.s.|; theorem :: STACKS_1:9 not emp s implies top s = |.s.|.1; theorem :: STACKS_1:10 |.s.| = {} implies emp s; theorem :: STACKS_1:11 for s being stack of StandardStackSystem A holds |.s.| = s; theorem :: STACKS_1:12 for x being Element of (the carrier of X)* ex s st |.s.| = x; definition let X,s1,s2; pred s1 == s2 means :: STACKS_1:def 14 |.s1.| = |.s2.|; reflexivity; symmetry; end; theorem :: STACKS_1:13 s1 == s2 & s2 == s3 implies s1 == s3; theorem :: STACKS_1:14 s1 == s2 & emp s1 implies emp s2; theorem :: STACKS_1:15 emp s1 & emp s2 implies s1 == s2; theorem :: STACKS_1:16 s1 == s2 implies push(e,s1) == push(e,s2); theorem :: STACKS_1:17 s1 == s2 & not emp s1 implies pop s1 == pop s2; theorem :: STACKS_1:18 s1 == s2 & not emp s1 implies top s1 = top s2; definition let X; attr X is proper-for-identity means :: STACKS_1:def 15 for s1,s2 st s1 == s2 holds s1 = s2; end; registration let A; cluster StandardStackSystem A -> proper-for-identity; end; definition let X; func ==_X -> Relation of the carrier' of X means :: STACKS_1:def 16 [s1,s2] in it iff s1 == s2; end; registration let X; cluster ==_X -> total symmetric transitive; end; theorem :: STACKS_1:19 emp s implies Class(==_X, s) = the s_empty of X; definition let X,s; func coset s -> Subset of the carrier' of X means :: STACKS_1:def 17 s in it & (for e,s1 st s1 in it holds push(e,s1) in it & (not emp s1 implies pop s1 in it)) & for A being Subset of the carrier' of X st s in A & (for e,s1 st s1 in A holds push(e,s1) in A & (not emp s1 implies pop s1 in A)) holds it c= A; end; theorem :: STACKS_1:20 (push(e,s) in coset s1 implies s in coset s1) & (not emp s & pop s in coset s1 implies s in coset s1); theorem :: STACKS_1:21 s in coset push(e,s) & (not emp s implies s in coset pop s); theorem :: STACKS_1:22 ex s1 st emp s1 & s1 in coset s; registration let A; let R be Relation of A; cluster A-valued for RedSequence of R; end; definition let X; func ConstructionRed X -> Relation of the carrier' of X means :: STACKS_1:def 18 [s1,s2] in it iff (not emp s1 & s2 = pop s1) or ex e st s2 = push(e,s1); end; theorem :: STACKS_1:23 for R being Relation of A for t being RedSequence of R holds t.1 in A iff t is A-valued; scheme :: STACKS_1:sch 6 PathIND{X() -> non empty set, x1,x2() -> Element of X(), R() -> (Relation of X()), P[set]}: P[x2()] provided P[x1()] and R() reduces x1(),x2() and for x,y being Element of X() st R() reduces x1(),x & [x,y] in R() & P[x] holds P[y]; theorem :: STACKS_1:24 for t being RedSequence of ConstructionRed X st s = t.1 holds rng t c= coset s; theorem :: STACKS_1:25 coset s = {s1: ConstructionRed X reduces s,s1}; definition let X,s; func core s -> stack of X means :: STACKS_1:def 19 emp it & ex t being the carrier' of X-valued RedSequence of ConstructionRed X st t.1 = s & t.len t = it & for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i); end; theorem :: STACKS_1:26 emp s implies core s = s; theorem :: STACKS_1:27 core push(e,s) = core s; theorem :: STACKS_1:28 not emp s implies core pop s = core s; theorem :: STACKS_1:29 core s in coset s; theorem :: STACKS_1:30 for x being Element of (the carrier of X)* ex s1 st |.s1.| = x & s1 in coset s; theorem :: STACKS_1:31 s1 in coset s implies core s1 = core s; theorem :: STACKS_1:32 s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2; theorem :: STACKS_1:33 ex s st (coset s1)/\Class(==_X, s2) = {s}; begin :: Quotient Stack System definition let X; func X/== -> strict StackSystem means :: STACKS_1:def 20 the carrier of it = the carrier of X & the carrier' of it = Class(==_X) & the s_empty of it = {the s_empty of X} & the s_push of it = (the s_push of X)/\/==_X & the s_pop of it = ((the s_pop of X)+*(id the s_empty of X))/\/==_X & for f being Choice_Function of Class(==_X) holds the s_top of it = ((the s_top of X)*f)+*(the s_empty of X,the Element of the carrier of X); end; registration let X; cluster X/== -> non empty non void; end; theorem :: STACKS_1:34 for S being stack of X/== ex s st S = Class(==_X, s); theorem :: STACKS_1:35 Class(==_X, s) is stack of X/==; theorem :: STACKS_1:36 for S being stack of X/== st S = Class(==_X, s) holds emp s iff emp S; theorem :: STACKS_1:37 for S being stack of X/== holds emp S iff S = the s_empty of X; theorem :: STACKS_1:38 for S being stack of X/==, E being Element of X/== st S = Class(==_X, s) & E = e holds push(e, s) in push(E, S) & Class(==_X, push(e, s)) = push(E, S); theorem :: STACKS_1:39 for S being stack of X/== st S = Class(==_X, s) & not emp s holds pop s in pop S & Class(==_X, pop s) = pop S; theorem :: STACKS_1:40 for S being stack of X/== st S = Class(==_X, s) & not emp s holds top S = top s; registration let X; cluster X/== -> pop-finite; cluster X/== -> push-pop; cluster X/== -> top-push; cluster X/== -> pop-push; cluster X/== -> push-non-empty; end; theorem :: STACKS_1:41 for S being stack of X/== st S = Class(==_X, s) holds |.S.| = |.s.|; registration let X; cluster X/== -> proper-for-identity; end; registration cluster proper-for-identity for StackAlgebra; end; begin :: Representation Theorem for Stacks definition let X1,X2 be StackAlgebra; let F,G be Function; pred F,G form_isomorphism_between X1,X2 means :: STACKS_1:def 21 dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one & dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one & for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1 holds (emp s1 iff emp s2) & (not emp s1 implies pop s2 = G.pop s1 & top s2 = F.top s1) & for e1 being Element of X1, e2 being Element of X2 st e2 = F.e1 holds push(e2,s2) = G.push(e1,s1); end; reserve X1,X2,X3 for StackAlgebra; reserve F,F1,F2,G,G1,G2 for Function; theorem :: STACKS_1:42 id the carrier of X, id the carrier' of X form_isomorphism_between X,X; theorem :: STACKS_1:43 F,G form_isomorphism_between X1,X2 implies F",G" form_isomorphism_between X2,X1; theorem :: STACKS_1:44 F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 implies F2*F1,G2*G1 form_isomorphism_between X1,X3; theorem :: STACKS_1:45 F,G form_isomorphism_between X1,X2 implies for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1 holds |.s2.| = F*|.s1.|; definition let X1,X2 be StackAlgebra; pred X1,X2 are_isomorphic means :: STACKS_1:def 22 ex F,G being Function st F,G form_isomorphism_between X1,X2; reflexivity; symmetry; end; theorem :: STACKS_1:46 X1,X2 are_isomorphic & X2,X3 are_isomorphic implies X1,X3 are_isomorphic; theorem :: STACKS_1:47 X1,X2 are_isomorphic & X1 is proper-for-identity implies X2 is proper-for-identity; theorem :: STACKS_1:48 for X being proper-for-identity StackAlgebra holds ex G st (for s being stack of X holds G.s = |.s.|) & id the carrier of X, G form_isomorphism_between X, StandardStackSystem the carrier of X; theorem :: STACKS_1:49 for X being proper-for-identity StackAlgebra holds X, StandardStackSystem the carrier of X are_isomorphic;