:: Definitions of Petri Net - Part II :: 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 STRUCT_0, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, SYSREL, E_SIEC; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0; constructors SYSREL, STRUCT_0, XTUPLE_0; registrations XBOOLE_0, RELAT_1; requirements SUBSET, BOOLE; begin reserve x,y,z for object,X,Y for set; definition struct (1-sorted) G_Net (# carrier -> set, entrance, escape -> Relation #); end; definition let IT be G_Net; attr IT is GG means :: E_SIEC:def 1 the entrance of IT c= [:the carrier of IT,the carrier of IT:] & the escape of IT c= [:the carrier of IT,the carrier of IT:] & (the entrance of IT) * (the entrance of IT) = the entrance of IT & (the entrance of IT) * (the escape of IT) = the entrance of IT & (the escape of IT) * (the escape of IT) = the escape of IT & (the escape of IT) * (the entrance of IT) = the escape of IT; end; registration cluster GG for G_Net; end; definition mode gg_net is GG G_Net; end; definition let IT be G_Net; attr IT is EE means :: E_SIEC:def 2 (the entrance of IT) * ((the entrance of IT) \ id the carrier of IT) = {} & (the escape of IT) * ((the escape of IT) \ id the carrier of IT) = {}; end; registration cluster EE for G_Net; end; registration cluster strict GG EE for G_Net; end; definition mode e_net is EE GG G_Net; end; reserve N for e_net; theorem :: E_SIEC:1 for R, S being Relation holds G_Net (# X, R, S #) is e_net iff R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ id X) = {} & S * (S \ id X) = {}; theorem :: E_SIEC:2 G_Net (# X, {}, {} #) is e_net; theorem :: E_SIEC:3 G_Net (# X, id X, id X #) is e_net; theorem :: E_SIEC:4 G_Net (# {}, {}, {} #) is e_net; theorem :: E_SIEC:5 G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net; definition func empty_e_net -> strict e_net equals :: E_SIEC:def 3 G_Net (# {}, {}, {} #); end; definition let X; func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 4 G_Net (# X, id X, id X #); func Pempty_e_net(X) -> strict e_net equals :: E_SIEC:def 5 G_Net (# X, {}, {} #); end; theorem :: E_SIEC:6 the carrier of Tempty_e_net(X) = X & the entrance of Tempty_e_net(X) = id X & the escape of Tempty_e_net(X) = id X; theorem :: E_SIEC:7 the carrier of Pempty_e_net(X) = X & the entrance of Pempty_e_net(X) = {} & the escape of Pempty_e_net(X) = {}; definition let x; func Psingle_e_net(x) -> strict e_net equals :: E_SIEC:def 6 G_Net (#{x}, id{x}, id{x}#); func Tsingle_e_net(x) -> strict e_net equals :: E_SIEC:def 7 G_Net (# {x}, {}, {} #); end; theorem :: E_SIEC:8 the carrier of Psingle_e_net(x) = {x} & the entrance of Psingle_e_net(x) = id{x} & the escape of Psingle_e_net(x) = id{x}; theorem :: E_SIEC:9 the carrier of Tsingle_e_net(x) = {x} & the entrance of Tsingle_e_net(x) = {} & the escape of Tsingle_e_net(x) = {}; theorem :: E_SIEC:10 G_Net (# X \/ Y, id X, id X #) is e_net; definition let X,Y; func PTempty_e_net(X,Y) -> strict e_net equals :: E_SIEC:def 8 G_Net (#X \/ Y, id(X), id(X)#); end; theorem :: E_SIEC:11 (the entrance of N) \ id(dom(the entrance of N)) = (the entrance of N) \ id the carrier of N & (the escape of N) \ id(dom(the escape of N)) = (the escape of N) \ id the carrier of N & (the entrance of N) \ id(rng(the entrance of N)) = (the entrance of N) \ id the carrier of N & (the escape of N) \ id(rng(the escape of N)) = (the escape of N) \ id the carrier of N; theorem :: E_SIEC:12 CL the entrance of N = CL the escape of N; theorem :: E_SIEC:13 rng (the entrance of N) = rng (CL(the entrance of N)) & rng (the entrance of N) = dom (CL(the entrance of N)) & rng (the escape of N) = rng (CL(the escape of N)) & rng (the escape of N) = dom (CL(the escape of N)) & rng the entrance of N = rng the escape of N; theorem :: E_SIEC:14 dom (the entrance of N) c= the carrier of N & rng (the entrance of N) c= the carrier of N & dom (the escape of N) c= the carrier of N & rng ( the escape of N) c= the carrier of N; theorem :: E_SIEC:15 (the entrance of N) * ((the escape of N) \ id the carrier of N) = {} & (the escape of N) * ((the entrance of N) \ id the carrier of N) = {}; theorem :: E_SIEC:16 ((the entrance of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {} & ((the escape of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {} & ((the entrance of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {} & ((the escape of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {}; definition let N; func e_Places(N) -> set equals :: E_SIEC:def 9 rng (the entrance of N); end; definition let N; func e_Transitions(N) -> set equals :: E_SIEC:def 10 (the carrier of N) \ e_Places(N); end; theorem :: E_SIEC:17 ([x,y] in the entrance of N or [x,y] in the escape of N) & x <> y implies x in e_Transitions(N) & y in e_Places(N); theorem :: E_SIEC:18 (the entrance of N) \ id(the carrier of N) c= [:e_Transitions(N),e_Places(N):] & (the escape of N) \ id(the carrier of N) c= [:e_Transitions(N),e_Places(N):]; definition let N; func e_Flow N -> Relation equals :: E_SIEC:def 11 ((the entrance of N)~ \/ (the escape of N)) \ id N; end; theorem :: E_SIEC:19 e_Flow N c= [:e_Places(N), e_Transitions(N):] \/ [:e_Transitions(N), e_Places(N):]; definition let N; func e_pre(N) -> Relation equals :: E_SIEC:def 12 (the entrance of N) \ id(the carrier of N); func e_post(N) -> Relation equals :: E_SIEC:def 13 (the escape of N) \ id(the carrier of N); end; theorem :: E_SIEC:20 e_pre(N) c= [:e_Transitions(N),e_Places(N):] & e_post(N) c= [:e_Transitions(N),e_Places(N):]; definition let N; func e_shore(N) -> set equals :: E_SIEC:def 14 the carrier of N; func e_prox(N) -> Relation equals :: E_SIEC:def 15 ((the entrance of N) \/ (the escape of N))~; func e_flow(N) -> Relation equals :: E_SIEC:def 16 ((the entrance of N)~ \/ (the escape of N)) \/ id(the carrier of N); end; theorem :: E_SIEC:21 e_prox(N) c= [:e_shore(N),e_shore(N):] & e_flow(N) c= [:e_shore(N),e_shore(N):]; theorem :: E_SIEC:22 (e_prox(N)) * (e_prox(N)) = e_prox(N) & (e_prox(N) \ id(e_shore(N))) * e_prox(N) = {} & (e_prox(N) \/ (e_prox(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~; theorem :: E_SIEC:23 id((the carrier of N) \ rng(the escape of N)) * ((the escape of N) \ id(the carrier of N)) = ((the escape of N) \ id(the carrier of N)) & id((the carrier of N) \ rng(the entrance of N)) * ((the entrance of N) \ id(the carrier of N)) = ((the entrance of N) \ id(the carrier of N)); theorem :: E_SIEC:24 ((the escape of N) \ id the carrier of N) * ((the escape of N) \ id the carrier of N) = {} & ((the entrance of N) \ id the carrier of N) * ((the entrance of N) \ id the carrier of N) = {} & ((the escape of N) \ id(the carrier of N)) * ((the entrance of N) \ id the carrier of N) = {} & ((the entrance of N) \ id the carrier of N) * ((the escape of N) \ id the carrier of N) = {}; theorem :: E_SIEC:25 ((the escape of N) \ id(the carrier of N))~ * ((the escape of N) \ id(the carrier of N))~ = {} & ((the entrance of N) \ id(the carrier of N))~ * ((the entrance of N) \ id(the carrier of N))~ = {}; theorem :: E_SIEC:26 ((the escape of N) \ id(the carrier of N))~ * id((the carrier of N) \ rng(the escape of N))~ = ((the escape of N) \ id(the carrier of N))~ & ((the entrance of N) \ id(the carrier of N))~ * id((the carrier of N) \ rng(the entrance of N))~ = ((the entrance of N) \ id(the carrier of N))~; theorem :: E_SIEC:27 ((the escape of N) \ id(the carrier of N)) * (id((the carrier of N) \ rng(the escape of N))) = {} & ((the entrance of N) \ id(the carrier of N)) * (id((the carrier of N) \ rng(the entrance of N))) = {}; theorem :: E_SIEC:28 id((the carrier of N) \ rng(the escape of N)) * ((the escape of N) \ id(the carrier of N))~ = {} & id((the carrier of N) \ rng(the entrance of N)) * ((the entrance of N) \ id(the carrier of N))~ = {}; definition let N; func e_entrance(N) -> Relation equals :: E_SIEC:def 17 (((the escape of N) \ id(the carrier of N))~) \/ id((the carrier of N) \ rng(the escape of N)); func e_escape(N) -> Relation equals :: E_SIEC:def 18 (((the entrance of N) \ id(the carrier of N))~) \/ id((the carrier of N) \ rng(the entrance of N)); end; theorem :: E_SIEC:29 e_entrance(N) * e_entrance(N) = e_entrance(N) & e_entrance(N) * e_escape(N) = e_entrance(N) & e_escape(N) * e_entrance(N) = e_escape(N) & e_escape(N) * e_escape(N) = e_escape(N); theorem :: E_SIEC:30 e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = {} & e_escape(N) * (e_escape(N) \ id(e_shore N)) = {}; definition let N; func e_adjac(N) -> Relation equals :: E_SIEC:def 19 (((the entrance of N) \/ (the escape of N)) \ id(the carrier of N)) \/ id((the carrier of N) \ rng(the entrance of N)); end; theorem :: E_SIEC:31 e_adjac(N) c= [:e_shore(N),e_shore(N):] & e_flow(N) c= [:e_shore(N),e_shore(N):]; theorem :: E_SIEC:32 (e_adjac(N)) * (e_adjac(N)) = e_adjac(N) & (e_adjac(N) \ id(e_shore(N))) * e_adjac(N) = {} & (e_adjac(N) \/ (e_adjac(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~; reserve N for e_net; theorem :: E_SIEC:33 ((the entrance of N) \ id(the carrier of N))~ c= [:e_Places(N), e_Transitions(N):] & ((the escape of N) \ id(the carrier of N))~ c= [:e_Places(N),e_Transitions(N):]; definition let N be G_Net; func s_pre(N) -> Relation equals :: E_SIEC:def 20 ((the escape of N) \ id(the carrier of N))~; func s_post(N) -> Relation equals :: E_SIEC:def 21 ((the entrance of N) \ id(the carrier of N))~; end; theorem :: E_SIEC:34 s_post(N) c= [:e_Places(N),e_Transitions(N):] & s_pre(N) c= [:e_Places(N),e_Transitions(N):];