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

begin

definition

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

end;

definition

let IT be G_Net ;
canceled;
attr IT is GG means :Def2: :: E_SIEC:def 2
( 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 E_SIEC:def 1 :
canceled;

:: deftheorem Def2 defines GG E_SIEC:def 2 :
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 G_Net ;
existence
ex b₁ being G_Net st b₁ 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 :Def3: :: E_SIEC:def 3
( 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 Def3 defines EE E_SIEC:def 3 :
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 G_Net ;
existence
ex b₁ being G_Net st b₁ is EE

proof end;

end;

registration

cluster strict GG EE G_Net ;
existence
ex b₁ being G_Net st
( b₁ is strict & b₁ is GG & b₁ 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 Def2, Def3;

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

canceled;

theorem :: E_SIEC:6

canceled;

theorem :: E_SIEC:7

canceled;

theorem :: E_SIEC:8

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 4
G_Net(# {},{},{} #);
correctness
coherence
G_Net(# {},{},{} #) is strict e_net;
by Th2;

end;

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

definition

let X be set ;
func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 5
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 6
G_Net(# X,{},{} #);
coherence
G_Net(# X,{},{} #) is strict e_net by Th2;

end;

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

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

theorem :: E_SIEC:9

canceled;

theorem :: E_SIEC:10

canceled;

theorem :: E_SIEC:11

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:12

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 7
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 8
G_Net(# {x},{},{} #);
coherence
G_Net(# {x},{},{} #) is strict e_net by Th2;

end;

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

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

theorem :: E_SIEC:13

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:14

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 Th15: :: E_SIEC:15

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 9
G_Net(# (X \/ Y),(id X),(id X) #);
coherence
G_Net(# (X \/ Y),(id X),(id X) #) is strict e_net by Th15;

end;

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

theorem Th16: :: E_SIEC:16

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 Th17: :: E_SIEC:17

for N being e_net holds CL the entrance of N = CL the escape of N

proof end;

theorem Th18: :: E_SIEC:18

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 Th19: :: E_SIEC:19

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 Th20: :: E_SIEC:20

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:21

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 10
rng the entrance of N;
correctness
coherence
rng the entrance of N is set ;
;

end;

:: deftheorem defines e_Places E_SIEC:def 10 :
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 11
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 11 :
for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);

theorem :: E_SIEC:22

canceled;

theorem Th23: :: E_SIEC:23

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 ) & x <> y holds
( x in e_Transitions N & y in e_Places N )

proof end;

theorem Th24: :: E_SIEC:24

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 12
(( 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 12 :
for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N);

theorem :: E_SIEC:25

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;
canceled;
canceled;
func e_pre N -> Relation equals :: E_SIEC:def 15
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 16
the escape of N \ (id the carrier of N);
correctness
coherence
the escape of N \ (id the carrier of N) is Relation;
;

end;

:: deftheorem E_SIEC:def 13 :
canceled;

:: deftheorem E_SIEC:def 14 :
canceled;

:: deftheorem defines e_pre E_SIEC:def 15 :
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 16 :
for N being e_net holds e_post N = the escape of N \ (id the carrier of N);

theorem :: E_SIEC:26

canceled;

theorem :: E_SIEC:27

canceled;

theorem :: E_SIEC:28

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

definition

let N be e_net;
func e_shore N -> set equals :: E_SIEC:def 17
the carrier of N;
correctness
coherence
the carrier of N is set ;
;
func e_prox N -> Relation equals :: E_SIEC:def 18
( 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 19
(( 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 17 :
for N being e_net holds e_shore N = the carrier of N;

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

:: deftheorem defines e_flow E_SIEC:def 19 :
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:29

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:30

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 Th31: :: E_SIEC:31

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 Th32: :: E_SIEC:32

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 Th33: :: E_SIEC:33

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:34

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 Th35: :: E_SIEC:35

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 Th36: :: E_SIEC:36

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;
canceled;
func e_entrance N -> Relation equals :: E_SIEC:def 21
(( 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 22
(( 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 E_SIEC:def 20 :
canceled;

:: deftheorem defines e_entrance E_SIEC:def 21 :
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 22 :
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:37

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:38

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;
canceled;
func e_adjac N -> Relation equals :: E_SIEC:def 24
(( 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 E_SIEC:def 23 :
canceled;

:: deftheorem defines e_adjac E_SIEC:def 24 :
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:39

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:40

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 Th41: :: E_SIEC:41

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 25
( 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 26
( 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 25 :
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 26 :
for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;

theorem :: E_SIEC:42

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