:: Definitions of Petri Net - Part I :: by Waldemar Korczy\'nski :: :: Received January 31, 1992 :: Copyright (c) 1992-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 NET_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, FF_SIEC, STRUCT_0, PETRI; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, PARTIT_2, STRUCT_0, PETRI, NET_1; constructors NET_1, PARTIT_2; registrations RELAT_1, NET_1, PARTIT_2; requirements SUBSET, BOOLE; begin :: F - Nets reserve x,y for object,X,Y for set; reserve M for Pnet; definition let X,Y; assume X misses Y; func PTempty_f_net(X,Y) -> strict Pnet equals :: FF_SIEC:def 1 PT_net_Str (# X, Y, {}(X,Y), {}(Y,X) #); end; definition let X; func Tempty_f_net(X) -> strict Pnet equals :: FF_SIEC:def 2 PTempty_f_net(X,{}); func Pempty_f_net(X) -> strict Pnet equals :: FF_SIEC:def 3 PTempty_f_net({},X); end; definition let x; func Tsingle_f_net(x) -> strict Pnet equals :: FF_SIEC:def 4 PTempty_f_net({},{x}); func Psingle_f_net(x) -> strict Pnet equals :: FF_SIEC:def 5 PTempty_f_net({x},{}); end; definition func empty_f_net -> strict Pnet equals :: FF_SIEC:def 6 PTempty_f_net({},{}); end; theorem :: FF_SIEC:1 X misses Y implies the carrier of PTempty_f_net(X,Y) = X & the carrier' of PTempty_f_net(X,Y) = Y & Flow PTempty_f_net(X,Y) = {}; theorem :: FF_SIEC:2 the carrier of Tempty_f_net(X) = X & the carrier' of Tempty_f_net(X) = {} & Flow Tempty_f_net(X) = {}; theorem :: FF_SIEC:3 for X holds the carrier of Pempty_f_net(X) = {} & the carrier' of Pempty_f_net(X) = X & Flow Pempty_f_net(X) = {}; theorem :: FF_SIEC:4 for x holds the carrier of (Tsingle_f_net(x)) = {} & the carrier' of (Tsingle_f_net(x)) = {x} & Flow Tsingle_f_net x = {}; theorem :: FF_SIEC:5 for x holds the carrier of (Psingle_f_net(x)) = {x} & the carrier' of (Psingle_f_net(x)) = {} & Flow (Psingle_f_net(x)) = {}; theorem :: FF_SIEC:6 the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & Flow empty_f_net = {}; theorem :: FF_SIEC:7 ( [x,y] in Flow M & x in the carrier' of M implies not x in the carrier of M & not y in the carrier' of M & y in the carrier of M) & ( [x,y] in Flow M & y in the carrier' of M implies not y in the carrier of M & not x in the carrier' of M & x in the carrier of M) & ( [x,y] in Flow M & x in the carrier of M implies not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M) & ( [x,y] in Flow M & y in the carrier of M implies not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M); theorem :: FF_SIEC:8 (Flow M) c= [:Elements(M), Elements(M):] & (Flow M)~ c= [:Elements(M), Elements(M):]; theorem :: FF_SIEC:9 rng ((Flow M)|(the carrier' of M)) c= (the carrier of M) & rng ((Flow M)~|(the carrier' of M)) c= (the carrier of M) & rng ((Flow M)|(the carrier of M)) c= (the carrier' of M) & rng ((Flow M)~|(the carrier of M)) c= (the carrier' of M) & rng id(the carrier' of M) c= (the carrier' of M) & dom id(the carrier' of M) c= (the carrier' of M) & rng id(the carrier of M) c= (the carrier of M) & dom id(the carrier of M) c= (the carrier of M); theorem :: FF_SIEC:10 rng ((Flow M)|(the carrier' of M)) misses dom((Flow M)|(the carrier' of M)) & rng ((Flow M)|(the carrier' of M)) misses dom((Flow M)~|(the carrier' of M)) & rng ((Flow M)|(the carrier' of M)) misses dom(id(the carrier' of M)) & rng ((Flow M)~|(the carrier' of M)) misses dom((Flow M)|(the carrier' of M)) & rng ((Flow M)~|(the carrier' of M)) misses dom((Flow M)~|(the carrier' of M)) & rng ((Flow M)~|(the carrier' of M)) misses dom(id(the carrier' of M)) & dom ((Flow M)|(the carrier' of M)) misses rng((Flow M)|(the carrier' of M)) & dom ((Flow M)|(the carrier' of M)) misses rng((Flow M)~|(the carrier' of M)) & dom ((Flow M)|(the carrier' of M)) misses rng(id(the carrier of M)) & dom ((Flow M)~|(the carrier' of M)) misses rng((Flow M)|(the carrier' of M)) & dom ((Flow M)~|(the carrier' of M)) misses rng((Flow M)~|(the carrier' of M)) & dom ((Flow M)~|(the carrier' of M)) misses rng(id(the carrier of M)) & rng ((Flow M)|(the carrier of M)) misses dom((Flow M)|(the carrier of M)) & rng ((Flow M)|(the carrier of M)) misses dom((Flow M)~|(the carrier of M)) & rng ((Flow M)|(the carrier of M)) misses dom(id(the carrier of M)) & rng ((Flow M)~|(the carrier of M)) misses dom((Flow M)|(the carrier of M)) & rng ((Flow M)~|(the carrier of M)) misses dom((Flow M)~|(the carrier of M)) & rng ((Flow M)~|(the carrier of M)) misses dom(id(the carrier of M)) & dom ((Flow M)|(the carrier of M)) misses rng((Flow M)|(the carrier of M)) & dom ((Flow M)|(the carrier of M)) misses rng((Flow M)~|(the carrier of M)) & dom ((Flow M)|(the carrier of M)) misses rng(id(the carrier' of M)) & dom ((Flow M)~|(the carrier of M)) misses rng((Flow M)|(the carrier of M)) & dom ((Flow M)~|(the carrier of M)) misses rng((Flow M)~|(the carrier of M)) & dom ((Flow M)~|(the carrier of M)) misses rng(id(the carrier' of M)); theorem :: FF_SIEC:11 ((Flow M)|(the carrier' of M)) * ((Flow M)|(the carrier' of M)) = {} & ((Flow M)~|(the carrier' of M)) * ((Flow M)~|(the carrier' of M)) = {} & ((Flow M)|(the carrier' of M)) * ((Flow M)~|(the carrier' of M)) = {} & ((Flow M)~|(the carrier' of M)) * ((Flow M)|(the carrier' of M)) = {} & ((Flow M)|(the carrier of M)) * ((Flow M)|(the carrier of M)) = {} & ((Flow M)~|(the carrier of M)) * ((Flow M)~|(the carrier of M)) = {} & ((Flow M)|(the carrier of M)) * ((Flow M)~|(the carrier of M)) = {} & ((Flow M)~|(the carrier of M)) * ((Flow M)|(the carrier of M)) = {}; theorem :: FF_SIEC:12 ((Flow M)|(the carrier' of M)) * id(the carrier of M) = (Flow M)|(the carrier' of M) & ((Flow M)~|(the carrier' of M)) * id(the carrier of M) = (Flow M)~|(the carrier' of M) & (id(the carrier' of M) * ((Flow M)|(the carrier' of M))) = (Flow M)|(the carrier' of M) & (id(the carrier' of M) * ((Flow M)~|(the carrier' of M))) = (Flow M)~|(the carrier' of M) & ((Flow M)|(the carrier of M)) * id(the carrier' of M) = (Flow M)|(the carrier of M) & ((Flow M)~|(the carrier of M)) * id(the carrier' of M) = (Flow M)~|(the carrier of M) & (id(the carrier of M)) * ((Flow M)|(the carrier of M)) = (Flow M)|(the carrier of M) & (id(the carrier of M)) * ((Flow M)~|(the carrier of M)) = (Flow M)~|(the carrier of M) & ((Flow M)|(the carrier of M)) * id(the carrier' of M) = (Flow M)|(the carrier of M) & ((Flow M)~|(the carrier of M)) * id(the carrier' of M) = (Flow M)~|(the carrier of M) & (id(the carrier' of M) * ((Flow M)|(the carrier of M))) = {} & (id(the carrier' of M) * ((Flow M)~|(the carrier of M))) = {} & ((Flow M)|(the carrier of M)) * id(the carrier of M) = {} & ((Flow M)~|(the carrier of M)) * id(the carrier of M) = {} & (id(the carrier of M)) * ((Flow M)|(the carrier' of M)) = {} & (id(the carrier of M)) * ((Flow M)~|(the carrier' of M)) = {} & ((Flow M)|(the carrier' of M)) * (id(the carrier' of M)) = {} & ((Flow M)~|(the carrier' of M)) * (id(the carrier' of M)) = {}; theorem :: FF_SIEC:13 ((Flow M)~|(the carrier' of M)) misses (id(Elements(M))) & ((Flow M)|(the carrier' of M)) misses (id(Elements(M))) & ((Flow M)~|(the carrier of M)) misses (id(Elements(M))) & ((Flow M)|(the carrier of M)) misses (id(Elements(M))); theorem :: FF_SIEC:14 ((Flow M)~|(the carrier' of M)) \/ (id(the carrier of M)) \ id(Elements(M)) = (Flow M)~|(the carrier' of M) & ((Flow M)|(the carrier' of M)) \/ (id(the carrier of M)) \ id(Elements(M)) = (Flow M)|(the carrier' of M) & (((Flow M)~|(the carrier of M)) \/ (id(the carrier of M))) \ id(Elements(M)) = (Flow M)~|(the carrier of M) & (((Flow M)|(the carrier of M)) \/ (id(the carrier of M))) \ id(Elements(M)) = (Flow M)|(the carrier of M) & ((Flow M)~|(the carrier of M)) \/ (id(the carrier' of M)) \ id(Elements(M)) = (Flow M)~|(the carrier of M) & ((Flow M)|(the carrier of M)) \/ (id(the carrier' of M)) \ id(Elements(M)) = (Flow M)|(the carrier of M) & (((Flow M)~|(the carrier' of M)) \/ (id(the carrier' of M))) \ id(Elements(M)) = (Flow M)~|(the carrier' of M) & (((Flow M)|(the carrier' of M)) \/ (id(the carrier' of M))) \ id(Elements(M)) = (Flow M)|(the carrier' of M); theorem :: FF_SIEC:15 ((Flow M)|(the carrier of M))~ = ((Flow M)~)|(the carrier' of M) & ((Flow M)|(the carrier' of M))~ = ((Flow M)~)|(the carrier of M); theorem :: FF_SIEC:16 ((Flow M)|(the carrier of M)) \/ ((Flow M)|(the carrier' of M)) = (Flow M) & ((Flow M)|(the carrier' of M)) \/ ((Flow M)|(the carrier of M)) = (Flow M) & (((Flow M)|(the carrier of M))~) \/ (((Flow M)|(the carrier' of M))~) = (Flow M)~ & (((Flow M)|(the carrier' of M))~) \/ (((Flow M)|(the carrier of M))~) = (Flow 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 7 ((Flow M)~|(the carrier' of M)) \/ id(the carrier of M); func f_exit(M) -> Relation equals :: FF_SIEC:def 8 ((Flow M)|(the carrier' of M)) \/ id(the carrier of M); end; theorem :: FF_SIEC:17 f_exit(M) c= [:Elements(M),Elements(M):] & f_enter(M) c= [:Elements(M),Elements(M):]; theorem :: FF_SIEC:18 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:19 (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:20 (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 9 ((Flow M)|(the carrier of M) \/ (Flow M)~|(the carrier of M)) \/ id(the carrier of M); func f_flow(M) -> Relation equals :: FF_SIEC:def 10 (Flow M) \/ id(Elements(M)); end; theorem :: FF_SIEC:21 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 11 the carrier of M; func f_transitions(M) -> set equals :: FF_SIEC:def 12 the carrier' of M; func f_pre(M) -> Relation equals :: FF_SIEC:def 13 (Flow M)|(the carrier' of M); func f_post(M) -> Relation equals :: FF_SIEC:def 14 (Flow M)~|(the carrier' of M); end; theorem :: FF_SIEC:22 f_pre(M) c= [:f_transitions(M),f_places(M):] & f_post(M) c= [:f_transitions(M),f_places(M):]; theorem :: FF_SIEC:23 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 15 ((Flow M)~|(the carrier of M)) \/ id(the carrier' of M); func f_escape(M) -> Relation equals :: FF_SIEC:def 16 ((Flow M)|(the carrier of M)) \/ id(the carrier' of M); end; theorem :: FF_SIEC:24 f_escape(M) c= [:Elements(M),Elements(M):] & f_entrance(M) c= [:Elements(M),Elements(M):]; theorem :: FF_SIEC:25 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:26 (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:27 (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {} & (f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = {}; ::B [F ->R] notation let M; synonym f_circulation(M) for f_flow(M); end; definition let M; func f_adjac(M) -> Relation equals :: FF_SIEC:def 17 ((Flow M)|(the carrier' of M) \/ (Flow M)~|(the carrier' of M)) \/ id(the carrier' of M); end; theorem :: FF_SIEC:28 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))~;