:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

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;
coherence
the S-T_Arcs of P \/ the T-S_Arcs of P is set
;
end;

:: deftheorem defines Flow NET_1:def 1 :
for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P;

registration
let P be PT_net_Str ;
coherence ;
end;

definition
let N be PT_net_Str ;
attr N is Petri means :Def2: :: 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;

:: deftheorem Def2 defines Petri NET_1:def 2 :
for N being PT_net_Str holds
( N is Petri iff ( 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:] ) );

:: 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;
correctness
coherence
the carrier of N \/ the carrier' of N is set
;
;
end;

:: deftheorem defines Elements NET_1:def 3 :
for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;

theorem :: NET_1:1
for x being set
for N being PT_net_Str holds
( not Elements N <> {} or not x is Element of Elements N or x is Element of the carrier of N or x is Element of the carrier' of N ) by XBOOLE_0:def 3;

theorem :: NET_1:2
for x being set
for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds
x is Element of Elements N by ;

theorem :: NET_1:3
for x being set
for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds
x is Element of Elements N by ;

Lm1: PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri
proof end;

registration
cluster PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) -> Petri ;
coherence
PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri
by Lm1;
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
existence
ex b1 being PT_net_Str st
( b1 is strict & b1 is Petri )
proof end;
end;

definition end;

:: The above definition defines a Petri net as a TYPE of the structure
:: PT_net_Str. The type is not empty.
theorem Th4: :: NET_1:4
for x being set
for N being Pnet holds
( not x in the carrier of N or not x in the carrier' of N ) by ;

:: 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 Th5: :: NET_1:5
for x, y being set
for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds
y in the carrier of N
proof end;

theorem Th6: :: NET_1:6
for x, y being set
for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds
x in the carrier of N
proof end;

theorem :: NET_1:7
for x, y being set
for N being Pnet st [x,y] in Flow N & x in the carrier of N holds
y in the carrier' of N
proof end;

theorem :: NET_1:8
for x, y being set
for N being Pnet st [x,y] in Flow N & y in the carrier of N holds
x in the carrier' of N
proof end;

definition
let N be Pnet;
let x, y be set ;
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;

:: deftheorem defines pre NET_1:def 4 :
for N being Pnet
for x, y being set holds
( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) );

:: deftheorem defines post NET_1:def 5 :
for N being Pnet
for x, y being set holds
( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) );

definition
let N be PT_net_Str ;
let x be Element of Elements N;
func Pre (N,x) -> set means :Def6: :: NET_1:def 6
for y being object holds
( y in it iff ( y in Elements N & [y,x] in Flow N ) );
existence
ex b1 being set st
for y being object holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being object holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being object holds
( y in b2 iff ( y in Elements N & [y,x] in Flow N ) ) ) holds
b1 = b2
proof end;
func Post (N,x) -> set means :Def7: :: NET_1:def 7
for y being object holds
( y in it iff ( y in Elements N & [x,y] in Flow N ) );
existence
ex b1 being set st
for y being object holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being object holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being object holds
( y in b2 iff ( y in Elements N & [x,y] in Flow N ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Pre NET_1:def 6 :
for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Pre (N,x) iff for y being object holds
( y in b3 iff ( y in Elements N & [y,x] in Flow N ) ) );

:: deftheorem Def7 defines Post NET_1:def 7 :
for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Post (N,x) iff for y being object holds
( y in b3 iff ( y in Elements N & [x,y] in Flow N ) ) );

theorem Th9: :: NET_1:9
for N being Pnet
for x being Element of Elements N holds Pre (N,x) c= Elements N
proof end;

theorem :: NET_1:10
for N being Pnet
for x being Element of Elements N holds Pre (N,x) c= Elements N by Th9;

theorem Th11: :: NET_1:11
for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N
proof end;

theorem :: NET_1:12
for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N by Th11;

theorem :: NET_1:13
for x being set
for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Pre (N,y) iff pre N,y,x )
proof end;

theorem :: NET_1:14
for x being set
for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Post (N,y) iff post N,y,x )
proof end;

definition
let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func enter (N,x) -> set means :Def8: :: NET_1:def 8
( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Pre (N,x) ) );
existence
ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) )
proof end;
uniqueness
for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Pre (N,x) ) holds
b1 = b2
by ;
end;

:: deftheorem Def8 defines enter NET_1:def 8 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = enter (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Pre (N,x) ) ) );

theorem Th15: :: NET_1:15
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
proof end;

theorem Th16: :: NET_1:16
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N
proof end;

theorem :: NET_1:17
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N by Th16;

definition
let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func exit (N,x) -> set means :Def9: :: NET_1:def 9
( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Post (N,x) ) );
existence
ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) )
proof end;
uniqueness
for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Post (N,x) ) holds
b1 = b2
by ;
end;

:: deftheorem Def9 defines exit NET_1:def 9 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = exit (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Post (N,x) ) ) );

theorem Th18: :: NET_1:18
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )
proof end;

theorem Th19: :: NET_1:19
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N
proof end;

theorem :: NET_1:20
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N by Th19;

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));
correctness
coherence
(enter (N,x)) \/ (exit (N,x)) is set
;
;
end;

:: deftheorem defines field NET_1:def 10 :
for N being Pnet
for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x));

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 ) );
existence
ex b1 being set st
for y being object holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being object holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being object holds
( y in b2 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) holds
b1 = b2
proof end;
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 ) );
existence
ex b1 being set st
for y being object holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being object holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being object holds
( y in b2 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Prec NET_1:def 11 :
for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Prec (N,x) iff for y being object holds
( y in b3 iff ( y in the carrier of N & [y,x] in Flow N ) ) );

:: deftheorem defines Postc NET_1:def 12 :
for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Postc (N,x) iff for y being object holds
( y in b3 iff ( y in the carrier of N & [x,y] in Flow N ) ) );

definition
let N be Pnet;
let X be set ;
func Entr (N,X) -> set means :Def13: :: NET_1:def 13
for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) holds
b1 = b2
proof end;
func Ext (N,X) -> set means :Def14: :: NET_1:def 14
for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Entr NET_1:def 13 :
for N being Pnet
for X, b3 being set holds
( b3 = Entr (N,X) iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) );

:: deftheorem Def14 defines Ext NET_1:def 14 :
for N being Pnet
for X, b3 being set holds
( b3 = Ext (N,X) iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) );

theorem Th21: :: NET_1:21
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
enter (N,x) in Entr (N,X)
proof end;

theorem Th22: :: NET_1:22
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
exit (N,x) in Ext (N,X)
proof end;

definition
let N be Pnet;
let X be set ;
func Input (N,X) -> set equals :: NET_1:def 15
union (Entr (N,X));
correctness
coherence
union (Entr (N,X)) is set
;
;
func Output (N,X) -> set equals :: NET_1:def 16
union (Ext (N,X));
correctness
coherence
union (Ext (N,X)) is set
;
;
end;

:: deftheorem defines Input NET_1:def 15 :
for N being Pnet
for X being set holds Input (N,X) = union (Entr (N,X));

:: deftheorem defines Output NET_1:def 16 :
for N being Pnet
for X being set holds Output (N,X) = union (Ext (N,X));

theorem :: NET_1:23
for N being Pnet
for x, X being set st X c= Elements N holds
( x in Input (N,X) iff ex y being Element of Elements N st
( y in X & x in enter (N,y) ) )
proof end;

theorem :: NET_1:24
for N being Pnet
for x, X being set st X c= Elements N holds
( x in Output (N,X) iff ex y being Element of Elements N st
( y in X & x in exit (N,y) ) )
proof end;

theorem :: NET_1:25
for N being Pnet
for X being Subset of ()
for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
proof end;

theorem :: NET_1:26
for N being Pnet
for X being Subset of ()
for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
proof end;