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

definition

let X, Y be set ;
assume A1: X misses Y ;
canceled;
canceled;
canceled;
func PTempty_f_net X,Y -> strict Pnet equals :Def4: :: FF_SIEC:def 4
Net(# X,Y,{} #);
correctness
coherence
Net(# X,Y,{} #) is strict Pnet;

proof end;

end;

:: deftheorem FF_SIEC:def 1 :

canceled;

:: deftheorem FF_SIEC:def 2 :

canceled;

:: deftheorem FF_SIEC:def 3 :

canceled;

:: deftheorem Def4 defines PTempty_f_net FF_SIEC:def 4 :

for X, Y being set st X misses Y holds
PTempty_f_net X,Y = Net(# X,Y,{} #);

definition

let X be set ;
func Tempty_f_net X -> strict Pnet equals :: FF_SIEC:def 5
PTempty_f_net X,{} ;
correctness
coherence
PTempty_f_net X,{} is strict Pnet;
;
func Pempty_f_net X -> strict Pnet equals :: FF_SIEC:def 6
PTempty_f_net {} ,X;
correctness
coherence
PTempty_f_net {} ,X is strict Pnet;
;

end;

:: deftheorem defines Tempty_f_net FF_SIEC:def 5 :

for X being set holds Tempty_f_net X = PTempty_f_net X,{} ;

:: deftheorem defines Pempty_f_net FF_SIEC:def 6 :

for X being set holds Pempty_f_net X = PTempty_f_net {} ,X;

definition

let x be set ;
func Tsingle_f_net x -> strict Pnet equals :: FF_SIEC:def 7
PTempty_f_net {} ,{x};
correctness
coherence
PTempty_f_net {} ,{x} is strict Pnet;
;
func Psingle_f_net x -> strict Pnet equals :: FF_SIEC:def 8
PTempty_f_net {x},{} ;
correctness
coherence
PTempty_f_net {x},{} is strict Pnet;
;

end;

:: deftheorem defines Tsingle_f_net FF_SIEC:def 7 :

for x being set holds Tsingle_f_net x = PTempty_f_net {} ,{x};

:: deftheorem defines Psingle_f_net FF_SIEC:def 8 :

for x being set holds Psingle_f_net x = PTempty_f_net {x},{} ;

definition

func empty_f_net -> strict Pnet equals :: FF_SIEC:def 9
PTempty_f_net {} ,{} ;
correctness
coherence
PTempty_f_net {} ,{} is strict Pnet;
;

end;

:: deftheorem defines empty_f_net FF_SIEC:def 9 :

empty_f_net = PTempty_f_net {} ,{} ;

theorem :: FF_SIEC:1

canceled;

theorem :: FF_SIEC:2

for X, Y being set st X misses Y holds
( the Places of (PTempty_f_net X,Y) = X & the Transitions of (PTempty_f_net X,Y) = Y & the Flow of (PTempty_f_net X,Y) = {} )

proof end;

theorem :: FF_SIEC:3

for X being set holds
( the Places of (Tempty_f_net X) = X & the Transitions of (Tempty_f_net X) = {} & the Flow of (Tempty_f_net X) = {} )

proof end;

theorem :: FF_SIEC:4

for X being set holds
( the Places of (Pempty_f_net X) = {} & the Transitions of (Pempty_f_net X) = X & the Flow of (Pempty_f_net X) = {} )

proof end;

theorem :: FF_SIEC:5

for x being set holds
( the Places of (Tsingle_f_net x) = {} & the Transitions of (Tsingle_f_net x) = {x} & the Flow of (Tsingle_f_net x) = {} )

proof end;

theorem :: FF_SIEC:6

for x being set holds
( the Places of (Psingle_f_net x) = {x} & the Transitions of (Psingle_f_net x) = {} & the Flow of (Psingle_f_net x) = {} )

proof end;

theorem :: FF_SIEC:7

( the Places of empty_f_net = {} & the Transitions of empty_f_net = {} & the Flow of empty_f_net = {} )

proof end;

theorem :: FF_SIEC:8

canceled;

theorem :: FF_SIEC:9

canceled;

theorem :: FF_SIEC:10

canceled;

theorem Th11: :: FF_SIEC:11

for x, y being set
for M being Pnet holds
( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) )

proof end;

theorem :: FF_SIEC:12

canceled;

theorem Th13: :: FF_SIEC:13

for M being Pnet holds
( the Flow of M c= [:(Elements M),(Elements M):] & the Flow of M ~ c= [:(Elements M),(Elements M):] )

proof end;

theorem Th14: :: FF_SIEC:14

for M being Pnet holds
( rng (the Flow of M | the Transitions of M) c= the Places of M & rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M & rng (the Flow of M | the Places of M) c= the Transitions of M & rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M & rng (id the Transitions of M) c= the Transitions of M & dom (id the Transitions of M) c= the Transitions of M & rng (id the Places of M) c= the Places of M & dom (id the Places of M) c= the Places of M )

proof end;

Lm1: for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C

proof end;

theorem Th15: :: FF_SIEC:15

for M being Pnet holds
( rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (id the Places of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (id the Places of M) & rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M) & rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng (the Flow of M | the Places of M) misses dom (id the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) & dom (the Flow of M | the Places of M) misses rng (the Flow of M | the Places of M) & dom (the Flow of M | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (the Flow of M | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) )

proof end;

theorem Th16: :: FF_SIEC:16

for M being Pnet holds
( (the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & (the Flow of M | the Places of M) * (the Flow of M | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M) = {} )

proof end;

theorem Th17: :: FF_SIEC:17

for M being Pnet holds
( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} )

proof end;

theorem Th18: :: FF_SIEC:18

for M being Pnet holds
( (the Flow of M ~ ) | the Transitions of M misses id (Elements M) & the Flow of M | the Transitions of M misses id (Elements M) & (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )

proof end;

theorem Th19: :: FF_SIEC:19

for M being Pnet holds
( (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M )

proof end;

theorem Th20: :: FF_SIEC:20

for M being Pnet holds
( (the Flow of M | the Places of M) ~ = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Transitions of M) ~ = (the Flow of M ~ ) | the Places of M )

proof end;

theorem Th21: :: FF_SIEC:21

for M being Pnet holds
( (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M & (the Flow of M | the Transitions of M) \/ (the Flow of M | the Places of M) = the Flow of M & ((the Flow of M | the Places of M) ~ ) \/ ((the Flow of M | the Transitions of M) ~ ) = the Flow of M ~ & ((the Flow of M | the Transitions of M) ~ ) \/ ((the Flow of M | the Places of M) ~ ) = the Flow of M ~ )

proof end;

definition

let M be Pnet;
func f_enter M -> Relation equals :: FF_SIEC:def 10
((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M);
correctness
coherence
((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M) is Relation;
;
func f_exit M -> Relation equals :: FF_SIEC:def 11
(the Flow of M | the Transitions of M) \/ (id the Places of M);
correctness
coherence
(the Flow of M | the Transitions of M) \/ (id the Places of M) is Relation;
;

end;

:: deftheorem defines f_enter FF_SIEC:def 10 :

for M being Pnet holds f_enter M = ((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M);

:: deftheorem defines f_exit FF_SIEC:def 11 :

for M being Pnet holds f_exit M = (the Flow of M | the Transitions of M) \/ (id the Places of M);

theorem :: FF_SIEC:22

for M being Pnet holds
( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )

proof end;

theorem :: FF_SIEC:23

for M being Pnet holds
( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )

proof end;

theorem :: FF_SIEC:24

for M being Pnet holds
( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )

proof end;

theorem :: FF_SIEC:25

for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )

proof end;

definition

let M be Pnet;
func f_prox M -> Relation equals :: FF_SIEC:def 12
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M);
correctness
coherence
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M) is Relation;
;
func f_flow M -> Relation equals :: FF_SIEC:def 13
the Flow of M \/ (id (Elements M));
correctness
coherence
the Flow of M \/ (id (Elements M)) is Relation;
;

end;

:: deftheorem defines f_prox FF_SIEC:def 12 :

for M being Pnet holds f_prox M = ((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M);

:: deftheorem defines f_flow FF_SIEC:def 13 :

for M being Pnet holds f_flow M = the Flow of M \/ (id (Elements M));

theorem :: FF_SIEC:26

for M being Pnet holds
( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~ ) )

proof end;

definition

let M be Pnet;
func f_places M -> set equals :: FF_SIEC:def 14
the Places of M;
correctness
coherence
the Places of M is set ;
;
func f_transitions M -> set equals :: FF_SIEC:def 15
the Transitions of M;
correctness
coherence
the Transitions of M is set ;
;
func f_pre M -> Relation equals :: FF_SIEC:def 16
the Flow of M | the Transitions of M;
correctness
coherence
the Flow of M | the Transitions of M is Relation;
;
func f_post M -> Relation equals :: FF_SIEC:def 17
(the Flow of M ~ ) | the Transitions of M;
correctness
coherence
(the Flow of M ~ ) | the Transitions of M is Relation;
;

end;

:: deftheorem defines f_places FF_SIEC:def 14 :

for M being Pnet holds f_places M = the Places of M;

:: deftheorem defines f_transitions FF_SIEC:def 15 :

for M being Pnet holds f_transitions M = the Transitions of M;

:: deftheorem defines f_pre FF_SIEC:def 16 :

for M being Pnet holds f_pre M = the Flow of M | the Transitions of M;

:: deftheorem defines f_post FF_SIEC:def 17 :

for M being Pnet holds f_post M = (the Flow of M ~ ) | the Transitions of M;

theorem :: FF_SIEC:27

for M being Pnet holds
( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )

proof end;

theorem :: FF_SIEC:28

canceled;

theorem :: FF_SIEC:29

for M being Pnet holds
( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )

proof end;

definition

let M be Pnet;
func f_entrance M -> Relation equals :: FF_SIEC:def 18
((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M);
correctness
coherence
((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M) is Relation;
;
func f_escape M -> Relation equals :: FF_SIEC:def 19
(the Flow of M | the Places of M) \/ (id the Transitions of M);
correctness
coherence
(the Flow of M | the Places of M) \/ (id the Transitions of M) is Relation;
;

end;

:: deftheorem defines f_entrance FF_SIEC:def 18 :

for M being Pnet holds f_entrance M = ((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M);

:: deftheorem defines f_escape FF_SIEC:def 19 :

for M being Pnet holds f_escape M = (the Flow of M | the Places of M) \/ (id the Transitions of M);

theorem :: FF_SIEC:30

for M being Pnet holds
( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )

proof end;

theorem :: FF_SIEC:31

for M being Pnet holds
( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )

proof end;

theorem :: FF_SIEC:32

for M being Pnet holds
( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )

proof end;

theorem :: FF_SIEC:33

for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )

proof end;

notation

let M be Pnet;
synonym f_circulation M for f_flow M;

end;

definition

let M be Pnet;
func f_adjac M -> Relation equals :: FF_SIEC:def 20
((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M);
correctness
coherence
((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M) is Relation;
;

end;

:: deftheorem defines f_adjac FF_SIEC:def 20 :

for M being Pnet holds f_adjac M = ((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M);

theorem :: FF_SIEC:34

for M being Pnet holds
( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~ )) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~ ) )

proof end;