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


begin

definition
let X, Y be set ;
assume A1: X misses Y ;
func PTempty_f_net (X,Y) ->  strict Pnet equals :Def1: :: FF_SIEC:def 1
 PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);
correctness
coherence
PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #) is strict Pnet;
proofend;
end;

:: deftheorem Def1 defines PTempty_f_net FF_SIEC:def_1_:_
 for X, Y being set st X misses Y holds
PTempty_f_net (X,Y) = PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);

definition
let X be set ;
func Tempty_f_net X ->  strict Pnet equals :: FF_SIEC:def 2
 PTempty_f_net (X,{});
correctness
coherence
PTempty_f_net (X,{}) is strict Pnet;
;
func Pempty_f_net X ->  strict Pnet equals :: FF_SIEC:def 3
 PTempty_f_net ({},X);
correctness
coherence
PTempty_f_net ({},X) is strict Pnet;
;
end;

:: deftheorem  defines Tempty_f_net FF_SIEC:def_2_:_
 for X being set holds Tempty_f_net X = PTempty_f_net (X,{});

:: deftheorem  defines Pempty_f_net FF_SIEC:def_3_:_
 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 4
 PTempty_f_net ({},{x});
correctness
coherence
PTempty_f_net ({},{x}) is strict Pnet;
;
func Psingle_f_net x ->  strict Pnet equals :: FF_SIEC:def 5
 PTempty_f_net ({x},{});
correctness
coherence
PTempty_f_net ({x},{}) is strict Pnet;
;
end;

:: deftheorem  defines Tsingle_f_net FF_SIEC:def_4_:_
 for x being set holds Tsingle_f_net x = PTempty_f_net ({},{x});

:: deftheorem  defines Psingle_f_net FF_SIEC:def_5_:_
 for x being set holds Psingle_f_net x = PTempty_f_net ({x},{});

definition
func empty_f_net  ->  strict Pnet equals :: FF_SIEC:def 6
 PTempty_f_net ({},{});
correctness
coherence
PTempty_f_net ({},{}) is strict Pnet;
;
end;

:: deftheorem  defines empty_f_net FF_SIEC:def_6_:_
 empty_f_net = PTempty_f_net ({},{});

theorem :: FF_SIEC:1
for X, Y being set st X misses Y holds
( the carrier of (PTempty_f_net (X,Y)) = X & the carrier' of (PTempty_f_net (X,Y)) = Y & Flow (PTempty_f_net (X,Y)) = {} )
proofend;

theorem :: FF_SIEC:2
for X being set holds
( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} )
proofend;

theorem :: FF_SIEC:3
for X being set holds
( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} )
proofend;

theorem :: FF_SIEC:4
for x being set holds
( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} )
proofend;

theorem :: FF_SIEC:5
for x being set holds
( the carrier of (Psingle_f_net x) = {x} & the carrier' of (Psingle_f_net x) = {} & Flow (Psingle_f_net x) = {} )
proofend;

theorem :: FF_SIEC:6
( the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & Flow empty_f_net = {} )
proofend;

theorem Th7: :: FF_SIEC:7
for x, y being set
for M being Pnet holds
( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
proofend;

theorem Th8: :: FF_SIEC:8
for M being Pnet holds
( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] )
proofend;

theorem Th9: :: FF_SIEC:9
for M being Pnet holds
( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M )
proofend;

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

theorem Th10: :: FF_SIEC:10
for M being Pnet holds
( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) )
proofend;

theorem Th11: :: FF_SIEC:11
for M being Pnet holds
( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} )
proofend;

theorem Th12: :: FF_SIEC:12
for M being Pnet holds
( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} )
proofend;

theorem Th13: :: FF_SIEC:13
for M being Pnet holds
( ((Flow M) ~) | the carrier' of M misses id (Elements M) & (Flow M) | the carrier' of M misses id (Elements M) & ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )
proofend;

theorem Th14: :: FF_SIEC:14
for M being Pnet holds
( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M )
proofend;

theorem Th15: :: FF_SIEC:15
for M being Pnet holds
( ((Flow M) | the carrier of M) ~ = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier' of M) ~ = ((Flow M) ~) | the carrier of M )
proofend;

theorem Th16: :: FF_SIEC:16
for M being Pnet holds
( ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M & ((Flow M) | the carrier' of M) \/ ((Flow M) | the carrier of M) = Flow M & (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) = (Flow M) ~ & (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) = (Flow M) ~ )
proofend;

:: T R A N S F O R M A T I O N S
:: A [F -> E]
definition
let M be Pnet;
func f_enter M ->  Relation equals :: FF_SIEC:def 7
(((Flow M) ~) | the carrier' of M) \/ (id the carrier of M);
correctness
coherence
(((Flow M) ~) | the carrier' of M) \/ (id the carrier of M) is Relation;
;
func f_exit M ->  Relation equals :: FF_SIEC:def 8
((Flow M) | the carrier' of M) \/ (id the carrier of M);
correctness
coherence
((Flow M) | the carrier' of M) \/ (id the carrier of M) is Relation;
;
end;

:: deftheorem  defines f_enter FF_SIEC:def_7_:_
 for M being Pnet holds f_enter M = (((Flow M) ~) | the carrier' of M) \/ (id the carrier of M);

:: deftheorem  defines f_exit FF_SIEC:def_8_:_
 for M being Pnet holds f_exit M = ((Flow M) | the carrier' of M) \/ (id the carrier of M);

theorem :: FF_SIEC:17
for M being Pnet holds
( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
proofend;

theorem :: FF_SIEC:18
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 )
proofend;

theorem :: FF_SIEC:19
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 )
proofend;

theorem :: FF_SIEC:20
for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )
proofend;

::B [F ->R]
definition
let M be Pnet;
func f_prox M ->  Relation equals :: FF_SIEC:def 9
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M);
correctness
coherence
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M) is Relation;
;
func f_flow M ->  Relation equals :: FF_SIEC:def 10
(Flow M) \/ (id (Elements M));
correctness
coherence
(Flow M) \/ (id (Elements M)) is Relation;
;
end;

:: deftheorem  defines f_prox FF_SIEC:def_9_:_
 for M being Pnet holds f_prox M = (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M);

:: deftheorem  defines f_flow FF_SIEC:def_10_:_
 for M being Pnet holds f_flow M = (Flow M) \/ (id (Elements M));

theorem :: FF_SIEC:21
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) ~) )
proofend;

::C [F ->P]
definition
let M be Pnet;
func f_places M ->  set  equals :: FF_SIEC:def 11
 the carrier of M;
correctness
coherence
the carrier of M is set ;
;
func f_transitions M ->  set  equals :: FF_SIEC:def 12
 the carrier' of M;
correctness
coherence
the carrier' of M is set ;
;
func f_pre M ->  Relation equals :: FF_SIEC:def 13
(Flow M) | the carrier' of M;
correctness
coherence
(Flow M) | the carrier' of M is Relation;
;
func f_post M ->  Relation equals :: FF_SIEC:def 14
((Flow M) ~) | the carrier' of M;
correctness
coherence
((Flow M) ~) | the carrier' of M is Relation;
;
end;

:: deftheorem  defines f_places FF_SIEC:def_11_:_
 for M being Pnet holds f_places M = the carrier of M;

:: deftheorem  defines f_transitions FF_SIEC:def_12_:_
 for M being Pnet holds f_transitions M = the carrier' of M;

:: deftheorem  defines f_pre FF_SIEC:def_13_:_
 for M being Pnet holds f_pre M = (Flow M) | the carrier' of M;

:: deftheorem  defines f_post FF_SIEC:def_14_:_
 for M being Pnet holds f_post M = ((Flow M) ~) | the carrier' of M;

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

theorem :: FF_SIEC:23
for M being Pnet holds
( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
proofend;

::A [F -> E]
definition
let M be Pnet;
func f_entrance M ->  Relation equals :: FF_SIEC:def 15
(((Flow M) ~) | the carrier of M) \/ (id the carrier' of M);
correctness
coherence
(((Flow M) ~) | the carrier of M) \/ (id the carrier' of M) is Relation;
;
func f_escape M ->  Relation equals :: FF_SIEC:def 16
((Flow M) | the carrier of M) \/ (id the carrier' of M);
correctness
coherence
((Flow M) | the carrier of M) \/ (id the carrier' of M) is Relation;
;
end;

:: deftheorem  defines f_entrance FF_SIEC:def_15_:_
 for M being Pnet holds f_entrance M = (((Flow M) ~) | the carrier of M) \/ (id the carrier' of M);

:: deftheorem  defines f_escape FF_SIEC:def_16_:_
 for M being Pnet holds f_escape M = ((Flow M) | the carrier of M) \/ (id the carrier' of M);

theorem :: FF_SIEC:24
for M being Pnet holds
( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )
proofend;

theorem :: FF_SIEC:25
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 )
proofend;

theorem :: FF_SIEC:26
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 )
proofend;

theorem :: FF_SIEC:27
for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )
proofend;

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 17
(((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M);
correctness
coherence
(((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M) is Relation;
;
end;

:: deftheorem  defines f_adjac FF_SIEC:def_17_:_
 for M being Pnet holds f_adjac M = (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M);

theorem :: FF_SIEC:28
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) ~) )
proofend;