:: Some Elementary Notions of the Theory of Petri Nets :: by Waldemar Korczy\'nski :: :: Received August 10, 1990 :: Copyright (c) 1990-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 RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, NET_1, STRUCT_0, PETRI; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, PARTIT_2, STRUCT_0, PETRI; constructors TARSKI, SUBSET_1, RELAT_1, STRUCT_0, PETRI, PARTIT_2; registrations XBOOLE_0, SUBSET_1, RELAT_1; requirements SUBSET, BOOLE; begin definition let P be PT_net_Str; func Flow P -> set equals :: NET_1:def 1 (the S-T_Arcs of P) \/ the T-S_Arcs of P; end; registration let P be PT_net_Str; cluster Flow P -> Relation-like; end; ::The above definition describes a "structure of a Petri net" which ::is a kind of relational system. reserve x,y for set; reserve N for PT_net_Str; definition let N be PT_net_Str; attr N is Petri means :: NET_1:def 2 the carrier of N misses the carrier' of N & ( Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]; end; :: A Petri net is defined as a triple of the form :: N = (carrier, carrier', Flow) :: with carrier and carrier' being disjoint sets and :: Flow c= (carrier' x carrier) U (carrier x carrier') :: It is allowed that both sets carrier and carrier' are empty. :: A Petri net is here described as a predicate defined in the set :: (on the mode) PT_net_Str. definition let N be PT_net_Str; func Elements(N) -> set equals :: NET_1:def 3 (the carrier of N) \/ (the carrier' of N); end; theorem :: NET_1:1 Elements(N) <> {} implies (x is Element of Elements(N) implies x is Element of the carrier of N or x is Element of the carrier' of N); theorem :: NET_1:2 x is Element of the carrier of N & the carrier of N <> {} implies x is Element of Elements(N); theorem :: NET_1:3 x is Element of the carrier' of N & the carrier' of N <> {} implies x is Element of Elements(N); registration cluster PT_net_Str (#{}, {}, {}({},{}), {}({},{})#) -> Petri; end; :: This lemma is of rather "technical" nature. It allows a definition :: of a "subtype" of the type PT_net_Str. (see the following definition of the :: type Pnet). registration cluster strict Petri for PT_net_Str; end; definition mode Pnet is Petri PT_net_Str; end; :: The above definition defines a Petri net as a TYPE of the structure :: PT_net_Str. The type is not empty. theorem :: NET_1:4 for N being Pnet holds not (x in the carrier of N & x in the carrier' of N); :: This lemma is of rather "technical" character. It will be used in the :: proof of the correctness of a definition of a function bellow. (See :: the definition of the functions Enter and Exit.) theorem :: NET_1:5 for N being Pnet holds [x,y] in Flow N & x in the carrier' of N implies y in the carrier of N; theorem :: NET_1:6 for N being Pnet holds [x,y] in Flow N & y in the carrier' of N implies x in the carrier of N; theorem :: NET_1:7 for N being Pnet holds [x,y] in Flow N & x in the carrier of N implies y in the carrier' of N; theorem :: NET_1:8 for N being Pnet holds [x,y] in Flow N & y in the carrier of N implies x in the carrier' of N; definition let N be Pnet; let x,y; pred pre N,x,y means :: NET_1:def 4 [y,x] in Flow N & x in the carrier' of N; pred post N,x,y means :: NET_1:def 5 [x,y] in Flow N & x in the carrier' of N; end; definition let N be PT_net_Str; let x be Element of Elements(N); func Pre(N,x) -> set means :: NET_1:def 6 for y being object holds y in it iff y in Elements(N) & [y,x] in Flow N; func Post(N,x) -> set means :: NET_1:def 7 for y being object holds y in it iff y in Elements(N) & [x,y] in Flow N; end; theorem :: NET_1:9 for N being Pnet for x being Element of Elements(N) holds Pre(N, x) c= Elements(N); theorem :: NET_1:10 for N being Pnet for x being Element of Elements N holds Pre(N,x) c= Elements N; theorem :: NET_1:11 for N being Pnet for x being Element of Elements(N) holds Post(N ,x) c= Elements(N); theorem :: NET_1:12 for N being Pnet for x being Element of Elements N holds Post(N,x) c= Elements N; theorem :: NET_1:13 for N being Pnet for y being Element of Elements(N) holds y in the carrier' of N implies (x in Pre(N,y) iff pre N,y,x); theorem :: NET_1:14 for N being Pnet for y being Element of Elements(N) holds y in the carrier' of N implies (x in Post(N,y) iff post N,y,x); definition let N be Pnet; let x be Element of Elements(N); assume Elements(N) <> {}; func enter(N,x) -> set means :: NET_1:def 8 (x in the carrier of N implies it = {x}) & (x in the carrier' of N implies it = Pre(N,x)); end; theorem :: NET_1:15 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies enter(N,x) ={x} or enter(N,x) = Pre(N,x); theorem :: NET_1:16 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies enter(N,x) c= Elements(N); theorem :: NET_1:17 for N being Pnet for x being Element of Elements N holds Elements N <> {} implies enter(N,x) c= Elements N; definition let N be Pnet; let x be Element of Elements(N); assume Elements(N) <> {}; func exit(N,x) -> set means :: NET_1:def 9 (x in the carrier of N implies it = {x}) & (x in the carrier' of N implies it = Post(N,x)); end; theorem :: NET_1:18 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies exit(N,x) ={x} or exit(N,x) = Post(N,x); theorem :: NET_1:19 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies exit(N,x) c= Elements(N); theorem :: NET_1:20 for N being Pnet for x being Element of Elements N holds Elements N <> {} implies exit(N,x) c= Elements N; definition let N be Pnet; let x be Element of Elements(N); func field(N,x) -> set equals :: NET_1:def 10 enter(N,x) \/ exit(N,x); end; definition let N be PT_net_Str; let x be Element of the carrier' of N; func Prec(N,x) -> set means :: NET_1:def 11 for y being object holds y in it iff y in the carrier of N & [y,x] in Flow N; func Postc(N,x) -> set means :: NET_1:def 12 for y being object holds y in it iff y in the carrier of N & [x,y] in Flow N; end; definition let N be Pnet; let X be set; func Entr(N,X) -> set means :: NET_1:def 13 x in it iff x c= Elements N & ex y being Element of Elements N st y in X & x = enter(N,y); func Ext(N,X) -> set means :: NET_1:def 14 x in it iff x c= Elements N & ex y being Element of Elements N st y in X & x = exit(N,y); end; theorem :: NET_1:21 for N being Pnet for x being Element of Elements(N) for X being set holds Elements(N) <> {} & x in X implies enter(N,x) in Entr(N,X); theorem :: NET_1:22 for N being Pnet for x being Element of Elements(N) for X being set holds Elements(N) <> {} & x in X implies exit(N,x) in Ext(N,X); definition let N be Pnet; let X be set; func Input(N,X) -> set equals :: NET_1:def 15 union Entr(N,X); func Output(N,X) -> set equals :: NET_1:def 16 union Ext(N,X); end; theorem :: NET_1:23 for N being Pnet for x for X being set holds X c= Elements(N) implies (x in Input(N,X) iff ex y being Element of Elements(N) st y in X & x in enter(N ,y)); theorem :: NET_1:24 for N being Pnet for x for X being set holds X c= Elements(N) implies (x in Output(N,X) iff ex y being Element of Elements(N) st y in X & x in exit(N ,y)); theorem :: NET_1:25 for N being Pnet for X being Subset of Elements(N) for x being Element of Elements(N) holds Elements(N) <> {} implies (x in Input(N,X) iff (x in X & x in the carrier of N or ex y being Element of Elements(N) st y in X & y in the carrier' of N & pre N,y,x)); theorem :: NET_1:26 for N being Pnet for X being Subset of Elements(N) for x being Element of Elements(N) holds Elements(N) <> {} implies (x in Output(N,X) iff (x in X & x in the carrier of N or ex y being Element of Elements(N) st y in X & y in the carrier' of N & post N,y,x));