:: Definitions of Petri Net - Part II
:: by Waldemar Korczy\'nski
::
:: 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 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
existence
ex b1 being G_Net st
( b1 is strict & b1 is GG & b1 is EE )
proof end;
end;

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

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 () = X & the entrance of () = id X & the escape of () = id X ) ;

theorem :: E_SIEC:7
for X being set holds
( the carrier of () = X & the entrance of () = {} & the escape of () = {} ) ;

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 () = {x} & the entrance of () = id {x} & the escape of () = id {x} ) ;

theorem :: E_SIEC:9
for x being object holds
( the carrier of () = {x} & the entrance of () = {} & the escape of () = {} ) ;

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 \ ();
correctness
coherence
the carrier of 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 \ ();

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= [:(),():] & the escape of N \ (id the carrier of N) c= [:(),():] )
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= [:(),():] \/ [:(),():]
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_post N c= [:(),():] ) 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_flow N c= [:(),():] )
proof end;

theorem :: E_SIEC:22
for N being e_net holds
( () * () = e_prox N & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) )
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_escape N & () * () = e_escape N )
proof end;

theorem :: E_SIEC:30
for N being e_net holds
( () * (() \ (id ())) = {} & () * (() \ (id ())) = {} )
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_flow N c= [:(),():] )
proof end;

theorem :: E_SIEC:32
for N being e_net holds
( () * () = e_adjac N & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) )
proof end;

theorem Th33: :: E_SIEC:33
for N being e_net holds
( ( the entrance of N \ (id the carrier of N)) ~ c= [:(),():] & ( the escape of N \ (id the carrier of N)) ~ c= [:(),():] )
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= [:(),():] & s_pre N c= [:(),():] ) by Th33;