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


begin

:::definition
::: struct(2-sorted) PT_net_Str (# carrier, carrier' -> set, Flow -> Relation #);
:::end;
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 ;
cluster Flow P ->  Relation-like ;
coherence
 Flow P is Relation-like ;
end;

definition
let N be PT_net_Str ;
attrN 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 &amp; the carrier of N <> {} holds
x is Element of Elements N
proofend;

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

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

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
cluster strict Petri for PT_net_Str ;
existence
 ex b1 being PT_net_Str st
( b1 is strict &amp; b1 is Petri )
proofend;
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 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 )
proofend;

:: 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 &amp; x in the carrier' of N holds
y in the carrier of N
proofend;

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

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

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

definition
let N be Pnet;
let x, y be set ;
pred pre N,x,y means :Def4: :: NET_1:def 4
( [y,x] in Flow N &amp; x in the carrier' of N );
pred post N,x,y means :Def5: :: NET_1:def 5
( [x,y] in Flow N &amp; x in the carrier' of N );
end;

:: deftheorem Def4 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 &amp; x in the carrier' of N ) );

:: deftheorem Def5 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 &amp; 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 set holds
( y in it iff ( y in Elements N &amp; [y,x] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N &amp; [y,x] in Flow N ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N &amp; [y,x] in Flow N ) ) ) &amp; ( for y being set holds
( y in b2 iff ( y in Elements N &amp; [y,x] in Flow N ) ) ) holds
b1 = b2
proofend;
func Post (N,x) ->  set  means :Def7: :: NET_1:def 7
 for y being set holds
( y in it iff ( y in Elements N &amp; [x,y] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N &amp; [x,y] in Flow N ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N &amp; [x,y] in Flow N ) ) ) &amp; ( for y being set holds
( y in b2 iff ( y in Elements N &amp; [x,y] in Flow N ) ) ) holds
b1 = b2
proofend;
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 set holds
( y in b3 iff ( y in Elements N &amp; [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 set holds
( y in b3 iff ( y in Elements N &amp; [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
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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} ) &amp; ( 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} ) &amp; ( x in the carrier' of N implies b1 = Pre (N,x) ) )
proofend;
uniqueness
 for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) &amp; ( x in the carrier' of N implies b1 = Pre (N,x) ) &amp; ( x in the carrier of N implies b2 = {x} ) &amp; ( x in the carrier' of N implies b2 = Pre (N,x) ) holds
b1 = b2 by A1, XBOOLE_0:def_3;
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} ) &amp; ( 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) )
proofend;

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
proofend;

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} ) &amp; ( 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} ) &amp; ( x in the carrier' of N implies b1 = Post (N,x) ) )
proofend;
uniqueness
 for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) &amp; ( x in the carrier' of N implies b1 = Post (N,x) ) &amp; ( x in the carrier of N implies b2 = {x} ) &amp; ( x in the carrier' of N implies b2 = Post (N,x) ) holds
b1 = b2 by A1, XBOOLE_0:def_3;
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} ) &amp; ( 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) )
proofend;

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
proofend;

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 set holds
( y in it iff ( y in the carrier of N &amp; [y,x] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N &amp; [y,x] in Flow N ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N &amp; [y,x] in Flow N ) ) ) &amp; ( for y being set holds
( y in b2 iff ( y in the carrier of N &amp; [y,x] in Flow N ) ) ) holds
b1 = b2
proofend;
func Postc (N,x) ->  set  means :: NET_1:def 12
 for y being set holds
( y in it iff ( y in the carrier of N &amp; [x,y] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N &amp; [x,y] in Flow N ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N &amp; [x,y] in Flow N ) ) ) &amp; ( for y being set holds
( y in b2 iff ( y in the carrier of N &amp; [x,y] in Flow N ) ) ) holds
b1 = b2
proofend;
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 set holds
( y in b3 iff ( y in the carrier of N &amp; [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 set holds
( y in b3 iff ( y in the carrier of N &amp; [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 &amp; ex y being Element of Elements N st
( y in X &amp; x = enter (N,y) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = enter (N,y) ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = enter (N,y) ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = enter (N,y) ) ) ) ) holds
b1 = b2
proofend;
func Ext (N,X) ->  set  means :Def14: :: NET_1:def 14
 for x being set holds
( x in it iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = exit (N,y) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = exit (N,y) ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = exit (N,y) ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; x = exit (N,y) ) ) ) ) holds
b1 = b2
proofend;
end;

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

:: deftheorem Def14 defines Ext NET_1:def_14_:_
 for N being Pnet
for X being set
for b3 being set holds
( b3 = Ext (N,X) iff for x being set holds
( x in b3 iff ( x c= Elements N &amp; ex y being Element of Elements N st
( y in X &amp; 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 <> {} &amp; x in X holds
enter (N,x) in Entr (N,X)
proofend;

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

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 &amp; x in enter (N,y) ) )
proofend;

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 &amp; x in exit (N,y) ) )
proofend;

theorem :: NET_1:25
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Input (N,X) iff ( ( x in X &amp; x in the carrier of N ) or ex y being Element of Elements N st
( y in X &amp; y in the carrier' of N &amp; pre N,y,x ) ) )
proofend;

theorem :: NET_1:26
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Output (N,X) iff ( ( x in X &amp; x in the carrier of N ) or ex y being Element of Elements N st
( y in X &amp; y in the carrier' of N &amp; post N,y,x ) ) )
proofend;