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


begin

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

definition
let IT be G_Net ;
attrIT 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
proofend;
end;

definition
mode gg_net is GG G_Net ;
end;

definition
let IT be G_Net ;
attrIT 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
proofend;
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 )
proofend;
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
proofend;

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

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

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 set ;
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 set holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);

:: deftheorem  defines Tsingle_e_net E_SIEC:def_7_:_
 for x being set holds Tsingle_e_net x = G_Net(# {x},{},{} #);

theorem :: E_SIEC:8
for x being set 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 set 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
proofend;

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

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

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

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

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)) = {} )
proofend;

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)) = {} )
proofend;

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 set
for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) &amp; x <> y holds
( x in e_Transitions N &amp; y in e_Places N )
proofend;

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):] &amp; the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )
proofend;

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

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):] &amp; 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):] &amp; e_flow N c= [:(e_shore N),(e_shore N):] )
proofend;

theorem :: E_SIEC:22
for N being e_net holds
( (e_prox N) * (e_prox N) = e_prox N &amp; ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} &amp; ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
proofend;

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) &amp; (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) )
proofend;

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)) = {} &amp; ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} &amp; ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} &amp; ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} )
proofend;

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)) ~) = {} &amp; (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
proofend;

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)) ~ &amp; (( 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)) ~ )
proofend;

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))) = {} &amp; ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} )
proofend;

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)) ~) = {} &amp; (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
proofend;

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 &amp; (e_entrance N) * (e_escape N) = e_entrance N &amp; (e_escape N) * (e_entrance N) = e_escape N &amp; (e_escape N) * (e_escape N) = e_escape N )
proofend;

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

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):] &amp; e_flow N c= [:(e_shore N),(e_shore N):] )
proofend;

theorem :: E_SIEC:32
for N being e_net holds
( (e_adjac N) * (e_adjac N) = e_adjac N &amp; ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} &amp; ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
proofend;

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):] &amp; ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] )
proofend;

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):] &amp; s_pre N c= [:(e_Places N),(e_Transitions N):] ) by Th33;