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

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
;
proof end;
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 ;
correctness
coherence
PTempty_f_net (X,{}) is strict Pnet
;
;
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 object ;
correctness
coherence
PTempty_f_net ({},{x}) is strict Pnet
;
;
correctness
coherence
PTempty_f_net ({x},{}) is strict Pnet
;
;
end;

:: deftheorem defines Tsingle_f_net FF_SIEC:def 4 :
for x being object holds Tsingle_f_net x = PTempty_f_net ({},{x});

:: deftheorem defines Psingle_f_net FF_SIEC:def 5 :
for x being object holds Psingle_f_net x = PTempty_f_net ({x},{});

definition
correctness
coherence ;
;
end;

:: deftheorem defines empty_f_net FF_SIEC:def 6 :

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

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

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

theorem :: FF_SIEC:4
for x being object holds
( the carrier of () = {} & the carrier' of () = {x} & Flow () = {} )
proof end;

theorem :: FF_SIEC:5
for x being object holds
( the carrier of () = {x} & the carrier' of () = {} & Flow () = {} )
proof end;

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

theorem Th7: :: FF_SIEC:7
for x, y being object
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 ) ) )
proof end;

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

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 )
proof end;

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) )
proof end;

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

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

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

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

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 )
proof end;

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) ~ )
proof end;

:: 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= [:(),():] & f_enter M c= [:(),():] )
proof end;

theorem :: FF_SIEC:18
for M being Pnet holds
( dom () c= Elements M & rng () c= Elements M & dom () c= Elements M & rng () c= Elements M )
proof end;

theorem :: FF_SIEC:19
for M being Pnet holds
( () * () = f_exit M & () * () = f_exit M & () * () = f_enter M & () * () = f_enter M )
proof end;

theorem :: FF_SIEC:20
for M being Pnet holds
( () * (() \ (id ())) = {} & () * (() \ (id ())) = {} )
proof end;

::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 ());
correctness
coherence
(Flow M) \/ (id ()) 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 ());

theorem :: FF_SIEC:21
for M being Pnet holds
( () * () = f_prox M & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) )
proof end;

::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_post M c= [:(),():] )
proof end;

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

::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= [:(),():] & f_entrance M c= [:(),():] )
proof end;

theorem :: FF_SIEC:25
for M being Pnet holds
( dom () c= Elements M & rng () c= Elements M & dom () c= Elements M & rng () c= Elements M )
proof end;

theorem :: FF_SIEC:26
for M being Pnet holds
( () * () = f_escape M & () * () = f_escape M & () * () = f_entrance M & () * () = f_entrance M )
proof end;

theorem :: FF_SIEC:27
for M being Pnet holds
( () * (() \ (id ())) = {} & () * (() \ (id ())) = {} )
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 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 & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) )
proof end;