:: Definitions of Petri Net - Part II
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users


definition
attr c1 is strict ;
struct G_Net -> 1-sorted ;
aggr G_Net(# carrier, entrance, escape #) -> G_Net ;
sel entrance c1 -> Relation;
sel escape c1 -> Relation;
end;

definition
let IT be G_Net ;
attr IT is GG means :Def1: :: 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;

:: deftheorem Def1 defines GG E_SIEC:def 1 :
for IT being G_Net holds
( IT is GG iff ( 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 ) );

registration
cluster GG for G_Net ;
existence
ex b1 being G_Net st b1 is GG
proof end;
end;

definition
mode gg_net is GG G_Net ;
end;

definition
let IT be G_Net ;
attr IT is EE means :Def2: :: 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;

:: deftheorem Def2 defines EE E_SIEC:def 2 :
for IT being G_Net holds
( IT is EE iff ( 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)) = {} ) );

registration
cluster EE for G_Net ;
existence
ex b1 being G_Net st b1 is EE
proof end;
end;

registration
cluster strict GG EE for G_Net ;
existence
ex b1 being G_Net st
( b1 is strict & b1 is GG & b1 is EE )
proof end;
end;

definition
mode e_net is GG EE G_Net ;
end;

theorem :: E_SIEC:1
for X being set
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)) = {} ) ) by Def1, Def2;

theorem Th2: :: E_SIEC:2
for X being set holds G_Net(# X,{},{} #) is e_net
proof end;

theorem Th3: :: E_SIEC:3
for X being set holds G_Net(# X,(id X),(id X) #) is e_net
proof end;

theorem :: E_SIEC:4
G_Net(# {},{},{} #) is e_net by Th2;

theorem :: E_SIEC:5
for X, Y being set holds G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net
proof end;

definition
func empty_e_net -> strict e_net equals :: E_SIEC:def 3
 G_Net(# {},{},{} #);
correctness
coherence
G_Net(# {},{},{} #) is strict e_net;
by Th2;
end;

:: deftheorem defines empty_e_net E_SIEC:def 3 :
empty_e_net = G_Net(# {},{},{} #);

definition
let X be set ;
func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 4
 G_Net(# X,(id X),(id X) #);
coherence
G_Net(# X,(id X),(id X) #) is strict e_net by Th3;
func Pempty_e_net X -> strict e_net equals :: E_SIEC:def 5
 G_Net(# X,{},{} #);
coherence
G_Net(# X,{},{} #) is strict e_net by Th2;
end;

:: deftheorem defines Tempty_e_net E_SIEC:def 4 :
for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #);

:: deftheorem defines Pempty_e_net E_SIEC:def 5 :
for X being set holds Pempty_e_net X = G_Net(# X,{},{} #);

theorem :: E_SIEC:6
for X being set holds
( 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
for X being set holds
( 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 be object ;
func Psingle_e_net x -> strict e_net equals :: E_SIEC:def 6
 G_Net(# {x},(id {x}),(id {x}) #);
coherence
G_Net(# {x},(id {x}),(id {x}) #) is strict e_net by Th3;
func Tsingle_e_net x -> strict e_net equals :: E_SIEC:def 7
 G_Net(# {x},{},{} #);
coherence
G_Net(# {x},{},{} #) is strict e_net by Th2;
end;

:: deftheorem defines Psingle_e_net E_SIEC:def 6 :
for x being object holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);

:: deftheorem defines Tsingle_e_net E_SIEC:def 7 :
for x being object holds Tsingle_e_net x = G_Net(# {x},{},{} #);

theorem :: E_SIEC:8
for x being object holds
( 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
for x being object holds
( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;

theorem Th10: :: E_SIEC:10
for X, Y being set holds G_Net(# (X \/ Y),(id X),(id X) #) is e_net
proof end;

definition
let X, Y be set ;
func PTempty_e_net (X,Y) -> strict e_net equals :: E_SIEC:def 8
 G_Net(# (X \/ Y),(id X),(id X) #);
coherence
G_Net(# (X \/ Y),(id X),(id X) #) is strict e_net by Th10;
end;

:: deftheorem defines PTempty_e_net E_SIEC:def 8 :
for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #);

theorem Th11: :: E_SIEC:11
for N being e_net holds
( 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) )
proof end;

theorem Th12: :: E_SIEC:12
for N being e_net holds CL the entrance of N = CL the escape of N
proof end;

theorem Th13: :: E_SIEC:13
for N being e_net holds
( 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 )
proof end;

theorem Th14: :: E_SIEC:14
for N being e_net holds
( 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 )
proof end;

theorem Th15: :: E_SIEC:15
for N being e_net holds
( 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)) = {} )
proof end;

theorem :: E_SIEC:16
for N being e_net holds
( ( 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)) = {} )
proof end;

definition
let N be e_net;
func e_Places N -> set equals :: E_SIEC:def 9
 rng the entrance of N;
correctness
coherence
rng the entrance of N is set ;
;
end;

:: deftheorem defines e_Places E_SIEC:def 9 :
for N being e_net holds e_Places N = rng the entrance of N;

definition
let N be e_net;
func e_Transitions N -> set equals :: E_SIEC:def 10
 the carrier of N \ (e_Places N);
correctness
coherence
the carrier of N \ (e_Places N) is set ;
;
end;

:: deftheorem defines e_Transitions E_SIEC:def 10 :
for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);

theorem Th17: :: E_SIEC:17
for x, y being object
for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds
( x in e_Transitions N & y in e_Places N )
proof end;

theorem Th18: :: E_SIEC:18
for N being e_net holds
( 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):] )
proof end;

definition
let N be e_net;
func e_Flow N -> Relation equals :: E_SIEC:def 11
(( the entrance of N ~) \/ the escape of N) \ (id N);
correctness
coherence
(( the entrance of N ~) \/ the escape of N) \ (id N) is Relation;
;
end;

:: deftheorem defines e_Flow E_SIEC:def 11 :
for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N);

theorem :: E_SIEC:19
for N being e_net holds e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):]
proof end;

definition
let N be e_net;
func e_pre N -> Relation equals :: E_SIEC:def 12
 the entrance of N \ (id the carrier of N);
correctness
coherence
the entrance of N \ (id the carrier of N) is Relation;
;
func e_post N -> Relation equals :: E_SIEC:def 13
 the escape of N \ (id the carrier of N);
correctness
coherence
the escape of N \ (id the carrier of N) is Relation;
;
end;

:: deftheorem defines e_pre E_SIEC:def 12 :
for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N);

:: deftheorem defines e_post E_SIEC:def 13 :
for N being e_net holds e_post N = the escape of N \ (id the carrier of N);

theorem :: E_SIEC:20
for N being e_net holds
( e_pre N c= [:(e_Transitions N),(e_Places N):] & e_post N c= [:(e_Transitions N),(e_Places N):] ) by Th18;

definition
let N be e_net;
func e_shore N -> set equals :: E_SIEC:def 14
 the carrier of N;
correctness
coherence
the carrier of N is set ;
;
func e_prox N -> Relation equals :: E_SIEC:def 15
( the entrance of N \/ the escape of N) ~ ;
correctness
coherence
( the entrance of N \/ the escape of N) ~ is Relation;
;
func e_flow N -> Relation equals :: E_SIEC:def 16
(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);
correctness
coherence
(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N) is Relation;
;
end;

:: deftheorem defines e_shore E_SIEC:def 14 :
for N being e_net holds e_shore N = the carrier of N;

:: deftheorem defines e_prox E_SIEC:def 15 :
for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ;

:: deftheorem defines e_flow E_SIEC:def 16 :
for N being e_net holds e_flow N = (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

theorem :: E_SIEC:21
for N being e_net holds
( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
proof end;

theorem :: E_SIEC:22
for N being e_net holds
( (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) ~) )
proof end;

theorem Th23: :: E_SIEC:23
for N being e_net holds
( (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) )
proof end;

theorem Th24: :: E_SIEC:24
for N being e_net holds
( ( 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)) = {} )
proof end;

theorem Th25: :: E_SIEC:25
for N being e_net holds
( (( 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)) ~) = {} )
proof end;

theorem :: E_SIEC:26
for N being e_net holds
( (( 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)) ~ )
proof end;

theorem Th27: :: E_SIEC:27
for N being e_net holds
( ( 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))) = {} )
proof end;

theorem Th28: :: E_SIEC:28
for N being e_net holds
( (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)) ~) = {} )
proof end;

definition
let N be e_net;
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)));
correctness
coherence
(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))) is Relation;
;
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)));
correctness
coherence
(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;
;
end;

:: deftheorem defines e_entrance E_SIEC:def 17 :
for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

:: deftheorem defines e_escape E_SIEC:def 18 :
for N being e_net holds e_escape N = (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:29
for N being e_net holds
( (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 )
proof end;

theorem :: E_SIEC:30
for N being e_net holds
( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
proof end;

definition
let N be e_net;
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)));
correctness
coherence
(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;
;
end;

:: deftheorem defines e_adjac E_SIEC:def 19 :
for N being e_net holds e_adjac N = (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:31
for N being e_net holds
( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
proof end;

theorem :: E_SIEC:32
for N being e_net holds
( (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) ~) )
proof end;

theorem Th33: :: E_SIEC:33
for N being e_net holds
( ( 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):] )
proof end;

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)) ~ ;
coherence
( the escape of N \ (id the carrier of N)) ~ is Relation ;
func s_post N -> Relation equals :: E_SIEC:def 21
( the entrance of N \ (id the carrier of N)) ~ ;
coherence
( the entrance of N \ (id the carrier of N)) ~ is Relation ;
end;

:: deftheorem defines s_pre E_SIEC:def 20 :
for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ;

:: deftheorem defines s_post E_SIEC:def 21 :
for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;

theorem :: E_SIEC:34
for N being e_net holds
( s_post N c= [:(e_Places N),(e_Transitions N):] & s_pre N c= [:(e_Places N),(e_Transitions N):] ) by Th33;