Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Definitions of Petri Net. Part I

**by****Waldemar Korczynski**- Received January 31, 1992
- MML identifier: FF_SIEC

- [ Mizar article, MML identifier index ]

environ vocabulary NET_1, BOOLE, RELAT_1, FF_SIEC, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, NET_1; constructors TARSKI, NET_1, XBOOLE_0; clusters RELAT_1, NET_1, SYSREL, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: F - Nets reserve x,y,X,Y for set; definition let N be Net; canceled; func chaos(N) -> set equals :: FF_SIEC:def 2 Elements(N) \/ {Elements(N)}; end; reserve M for Pnet; definition let X,Y; assume X misses Y; canceled; func PTempty_f_net(X,Y) -> strict Pnet equals :: FF_SIEC:def 4 Net (# X, Y, {} #); end; definition let X; func Tempty_f_net(X) -> strict Pnet equals :: FF_SIEC:def 5 PTempty_f_net(X,{}); func Pempty_f_net(X) -> strict Pnet equals :: FF_SIEC:def 6 PTempty_f_net({},X); end; definition let x; func Tsingle_f_net(x) -> strict Pnet equals :: FF_SIEC:def 7 PTempty_f_net({},{x}); func Psingle_f_net(x) -> strict Pnet equals :: FF_SIEC:def 8 PTempty_f_net({x},{}); end; definition func empty_f_net -> strict Pnet equals :: FF_SIEC:def 9 PTempty_f_net({},{}); end; canceled; theorem :: FF_SIEC:2 X misses Y implies the Places of PTempty_f_net(X,Y) = X & the Transitions of PTempty_f_net(X,Y) = Y & the Flow of PTempty_f_net(X,Y) = {}; theorem :: FF_SIEC:3 the Places of Tempty_f_net(X) = X & the Transitions of Tempty_f_net(X) = {} & the Flow of Tempty_f_net(X) = {}; theorem :: FF_SIEC:4 for X holds the Places of Pempty_f_net(X) = {} & the Transitions of Pempty_f_net(X) = X & the Flow of Pempty_f_net(X) = {}; theorem :: FF_SIEC:5 for x holds the Places of (Tsingle_f_net(x)) = {} & the Transitions of (Tsingle_f_net(x)) = {x} & the Flow of (Tsingle_f_net(x)) = {}; theorem :: FF_SIEC:6 for x holds the Places of (Psingle_f_net(x)) = {x} & the Transitions of (Psingle_f_net(x)) = {} & the Flow of (Psingle_f_net(x)) = {}; theorem :: FF_SIEC:7 the Places of empty_f_net = {} & the Transitions of empty_f_net = {} & the Flow of empty_f_net = {}; theorem :: FF_SIEC:8 the Places of M c= Elements M & the Transitions of M c= Elements M; canceled 2; theorem :: FF_SIEC:11 (([x,y] in the Flow of M & x in the Transitions of M) implies not x in the Places of M & not y in the Transitions of M & y in the Places of M) & (([x,y] in the Flow of M & y in the Transitions of M) implies not y in the Places of M & not x in the Transitions of M & x in the Places of M) & (([x,y] in the Flow of M & x in the Places of M) implies not y in the Places of M & not x in the Transitions of M & y in the Transitions of M) & (([x,y] in the Flow of M & y in the Places of M) implies not x in the Places of M & not y in the Transitions of M & x in the Transitions of M); theorem :: FF_SIEC:12 chaos(M) <> {}; theorem :: FF_SIEC:13 (the Flow of M) c= [:Elements(M), Elements(M):] & (the Flow of M)~ c= [:Elements(M), Elements(M):]; theorem :: FF_SIEC:14 rng ((the Flow of M)|(the Transitions of M)) c= (the Places of M) & rng ((the Flow of M)~|(the Transitions of M)) c= (the Places of M) & dom ((the Flow of M)|(the Transitions of M)) c= (the Transitions of M) & dom ((the Flow of M)~|(the Transitions of M)) c= (the Transitions of M) & rng ((the Flow of M)|(the Places of M)) c= (the Transitions of M) & rng ((the Flow of M)~|(the Places of M)) c= (the Transitions of M) & dom ((the Flow of M)|(the Places of M)) c= (the Places of M) & dom ((the Flow of M)~|(the Places of M)) c= (the Places of M) & rng id(the Transitions of M) c= (the Transitions of M) & dom id(the Transitions of M) c= (the Transitions of M) & rng id(the Places of M) c= (the Places of M) & dom id(the Places of M) c= (the Places of M); theorem :: FF_SIEC:15 rng ((the Flow of M)|(the Transitions of M)) misses dom((the Flow of M)|(the Transitions of M)) & rng ((the Flow of M)|(the Transitions of M)) misses dom((the Flow of M)~|(the Transitions of M)) & rng ((the Flow of M)|(the Transitions of M)) misses dom(id(the Transitions of M)) & rng ((the Flow of M)~|(the Transitions of M)) misses dom((the Flow of M)|(the Transitions of M)) & rng ((the Flow of M)~|(the Transitions of M)) misses dom((the Flow of M)~|(the Transitions of M)) & rng ((the Flow of M)~|(the Transitions of M)) misses dom(id(the Transitions of M)) & dom ((the Flow of M)|(the Transitions of M)) misses rng((the Flow of M)|(the Transitions of M)) & dom ((the Flow of M)|(the Transitions of M)) misses rng((the Flow of M)~|(the Transitions of M)) & dom ((the Flow of M)|(the Transitions of M)) misses rng(id(the Places of M)) & dom ((the Flow of M)~|(the Transitions of M)) misses rng((the Flow of M)|(the Transitions of M)) & dom ((the Flow of M)~|(the Transitions of M)) misses rng((the Flow of M)~|(the Transitions of M)) & dom ((the Flow of M)~|(the Transitions of M)) misses rng(id(the Places of M)) & rng ((the Flow of M)|(the Places of M)) misses dom((the Flow of M)|(the Places of M)) & rng ((the Flow of M)|(the Places of M)) misses dom((the Flow of M)~|(the Places of M)) & rng ((the Flow of M)|(the Places of M)) misses dom(id(the Places of M)) & rng ((the Flow of M)~|(the Places of M)) misses dom((the Flow of M)|(the Places of M)) & rng ((the Flow of M)~|(the Places of M)) misses dom((the Flow of M)~|(the Places of M)) & rng ((the Flow of M)~|(the Places of M)) misses dom(id(the Places of M)) & dom ((the Flow of M)|(the Places of M)) misses rng((the Flow of M)|(the Places of M)) & dom ((the Flow of M)|(the Places of M)) misses rng((the Flow of M)~|(the Places of M)) & dom ((the Flow of M)|(the Places of M)) misses rng(id(the Transitions of M)) & dom ((the Flow of M)~|(the Places of M)) misses rng((the Flow of M)|(the Places of M)) & dom ((the Flow of M)~|(the Places of M)) misses rng((the Flow of M)~|(the Places of M)) & dom ((the Flow of M)~|(the Places of M)) misses rng(id(the Transitions of M)); theorem :: FF_SIEC:16 (((the Flow of M)|(the Transitions of M)) * ((the Flow of M)|(the Transitions of M)) = {}) & (((the Flow of M)~|(the Transitions of M)) * ((the Flow of M)~|(the Transitions of M)) = {}) & (((the Flow of M)|(the Transitions of M)) * ((the Flow of M)~|(the Transitions of M)) = {}) & (((the Flow of M)~|(the Transitions of M)) * ((the Flow of M)|(the Transitions of M)) = {}) & (((the Flow of M)|(the Places of M)) * ((the Flow of M)|(the Places of M)) = {}) & (((the Flow of M)~|(the Places of M)) * ((the Flow of M)~|(the Places of M)) = {}) & (((the Flow of M)|(the Places of M)) * ((the Flow of M)~|(the Places of M)) = {}) & (((the Flow of M)~|(the Places of M)) * ((the Flow of M)|(the Places of M)) = {}); theorem :: FF_SIEC:17 (((the Flow of M)|(the Transitions of M)) * id(the Places of M) = (the Flow of M)|(the Transitions of M)) & (((the Flow of M)~|(the Transitions of M)) * id(the Places of M) = (the Flow of M)~|(the Transitions of M)) & ((id(the Transitions of M) * ((the Flow of M)|(the Transitions of M))) = (the Flow of M)|(the Transitions of M)) & ((id(the Transitions of M) * ((the Flow of M)~|(the Transitions of M))) = (the Flow of M)~|(the Transitions of M)) & (((the Flow of M)|(the Places of M)) * id(the Transitions of M) = (the Flow of M)|(the Places of M)) & (((the Flow of M)~|(the Places of M)) * id(the Transitions of M) = (the Flow of M)~|(the Places of M)) & (id(the Places of M)) * ((the Flow of M)|(the Places of M)) = (the Flow of M)|(the Places of M) & (id(the Places of M)) * ((the Flow of M)~|(the Places of M)) = (the Flow of M)~|(the Places of M) & ((the Flow of M)|(the Places of M)) * id(the Transitions of M) = (the Flow of M)|(the Places of M) & ((the Flow of M)~|(the Places of M)) * id(the Transitions of M) = (the Flow of M)~|(the Places of M) & (id(the Transitions of M) * ((the Flow of M)|(the Places of M))) = {} & (id(the Transitions of M) * ((the Flow of M)~|(the Places of M))) = {} & ((the Flow of M)|(the Places of M)) * id(the Places of M) = {} & ((the Flow of M)~|(the Places of M)) * id(the Places of M) = {} & (id(the Places of M)) * ((the Flow of M)|(the Transitions of M)) = {} & (id(the Places of M)) * ((the Flow of M)~|(the Transitions of M)) = {} & ((the Flow of M)|(the Transitions of M)) * (id(the Transitions of M)) = {} & ((the Flow of M)~|(the Transitions of M)) * (id(the Transitions of M)) = {}; theorem :: FF_SIEC:18 (((the Flow of M)~|(the Transitions of M)) misses (id(Elements(M)))) & (((the Flow of M)|(the Transitions of M)) misses (id(Elements(M)))) & (((the Flow of M)~|(the Places of M)) misses (id(Elements(M)))) & (((the Flow of M)|(the Places of M)) misses (id(Elements(M)))); theorem :: FF_SIEC:19 ((the Flow of M)~|(the Transitions of M)) \/ (id(the Places of M)) \ id(Elements(M)) = (the Flow of M)~|(the Transitions of M) & ((the Flow of M)|(the Transitions of M)) \/ (id(the Places of M)) \ id(Elements(M)) = (the Flow of M)|(the Transitions of M) & (((the Flow of M)~|(the Places of M)) \/ (id(the Places of M))) \ id(Elements(M)) = (the Flow of M)~|(the Places of M) & (((the Flow of M)|(the Places of M)) \/ (id(the Places of M))) \ id(Elements(M)) = (the Flow of M)|(the Places of M) & ((the Flow of M)~|(the Places of M)) \/ (id(the Transitions of M)) \ id(Elements(M)) = (the Flow of M)~|(the Places of M) & ((the Flow of M)|(the Places of M)) \/ (id(the Transitions of M)) \ id(Elements(M)) = (the Flow of M)|(the Places of M) & (((the Flow of M)~|(the Transitions of M)) \/ (id(the Transitions of M))) \ id(Elements(M)) = (the Flow of M)~|(the Transitions of M) & (((the Flow of M)|(the Transitions of M)) \/ (id(the Transitions of M))) \ id(Elements(M)) = (the Flow of M)|(the Transitions of M); theorem :: FF_SIEC:20 ((the Flow of M)|(the Places of M))~ = ((the Flow of M)~)|(the Transitions of M) & ((the Flow of M)|(the Transitions of M))~ = ((the Flow of M)~)|(the Places of M); theorem :: FF_SIEC:21 ((the Flow of M)|(the Places of M)) \/ ((the Flow of M)|(the Transitions of M)) = (the Flow of M) & ((the Flow of M)|(the Transitions of M)) \/ ((the Flow of M)|(the Places of M)) = (the Flow of M) & (((the Flow of M)|(the Places of M))~) \/ (((the Flow of M)|(the Transitions of M))~) = (the Flow of M)~ & (((the Flow of M)|(the Transitions of M))~) \/ (((the Flow of M)|(the Places of M))~) = (the Flow of M)~; :: T R A N S F O R M A T I O N S :: A [F -> E] definition let M; func f_enter(M) -> Relation equals :: FF_SIEC:def 10 ((the Flow of M)~|(the Transitions of M)) \/ id(the Places of M); func f_exit(M) -> Relation equals :: FF_SIEC:def 11 ((the Flow of M)|(the Transitions of M)) \/ id(the Places of M); end; theorem :: FF_SIEC:22 f_exit(M) c= [:Elements(M),Elements(M):] & f_enter(M) c= [:Elements(M),Elements(M):]; theorem :: FF_SIEC:23 dom(f_exit(M)) c= Elements(M) & rng(f_exit(M)) c= Elements(M) & dom(f_enter(M)) c= Elements(M) & rng(f_enter(M)) c= Elements(M); theorem :: FF_SIEC:24 (f_exit(M)) * (f_exit(M)) = f_exit(M) & (f_exit(M)) * (f_enter(M)) = f_exit(M) & (f_enter(M)) * (f_enter(M)) = f_enter(M) & (f_enter(M)) * (f_exit(M)) = f_enter(M); theorem :: FF_SIEC:25 (f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {} & (f_enter(M)) * (f_enter(M) \ id(Elements(M))) = {}; ::B [F ->R] definition let M; func f_prox(M) -> Relation equals :: FF_SIEC:def 12 ((the Flow of M)|(the Places of M) \/ (the Flow of M)~|(the Places of M)) \/ id(the Places of M); func f_flow(M) -> Relation equals :: FF_SIEC:def 13 (the Flow of M) \/ id(Elements(M)); end; theorem :: FF_SIEC:26 f_prox(M) * f_prox(M) = f_prox(M) & (f_prox(M) \ id(Elements(M))) * f_prox(M) = {} & (f_prox(M) \/ ((f_prox(M))~)) \/ id(Elements(M)) = f_flow(M) \/ (f_flow(M))~; ::C [F ->P] definition let M; func f_places(M) -> set equals :: FF_SIEC:def 14 the Places of M; func f_transitions(M) -> set equals :: FF_SIEC:def 15 the Transitions of M; func f_pre(M) -> Relation equals :: FF_SIEC:def 16 (the Flow of M)|(the Transitions of M); func f_post(M) -> Relation equals :: FF_SIEC:def 17 (the Flow of M)~|(the Transitions of M); end; theorem :: FF_SIEC:27 f_pre(M) c= [:f_transitions(M),f_places(M):] & f_post(M) c= [:f_transitions(M),f_places(M):]; theorem :: FF_SIEC:28 f_places(M) misses f_transitions(M); theorem :: FF_SIEC:29 f_prox(M) c= [:Elements(M), Elements(M):] & f_flow(M) c= [:Elements(M), Elements(M):]; ::A [F -> E] definition let M; func f_entrance(M) -> Relation equals :: FF_SIEC:def 18 ((the Flow of M)~|(the Places of M)) \/ id(the Transitions of M); func f_escape(M) -> Relation equals :: FF_SIEC:def 19 ((the Flow of M)|(the Places of M)) \/ id(the Transitions of M); end; theorem :: FF_SIEC:30 f_escape(M) c= [:Elements(M),Elements(M):] & f_entrance(M) c= [:Elements(M),Elements(M):]; theorem :: FF_SIEC:31 dom(f_escape(M)) c= Elements(M) & rng(f_escape(M)) c= Elements(M) & dom(f_entrance(M)) c= Elements(M) & rng(f_entrance(M)) c= Elements(M); theorem :: FF_SIEC:32 (f_escape(M)) * (f_escape(M)) = f_escape(M) & (f_escape(M)) * (f_entrance(M)) = f_escape(M) & (f_entrance(M)) * (f_entrance(M)) =f_entrance(M) & (f_entrance(M)) * (f_escape(M)) = f_entrance(M); theorem :: FF_SIEC:33 (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {} & (f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = {}; ::B [F ->R] definition let M; func f_adjac(M) -> Relation equals :: FF_SIEC:def 20 ((the Flow of M)|(the Transitions of M) \/ (the Flow of M)~|(the Transitions of M)) \/ id(the Transitions of M); redefine func f_flow(M); synonym f_circulation(M); end; theorem :: FF_SIEC:34 f_adjac(M) * f_adjac(M) = f_adjac(M) & (f_adjac(M) \ id(Elements(M))) * f_adjac(M) = {} & (f_adjac(M) \/ ((f_adjac(M))~)) \/ id(Elements(M)) = f_circulation(M) \/ (f_circulation(M))~;

Back to top