:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

definition

attr c₁ is strict ;
struct Net -> ;
aggr Net(# Places, Transitions, Flow #) -> Net ;
sel Places c₁ -> set ;
sel Transitions c₁ -> set ;
sel Flow c₁ -> Relation;

end;

definition

let N be Net ;
attr N is Petri means :Def1: :: NET_1:def 1
( the Places of N misses the Transitions of N & the Flow of N c= [:the Places of N,the Transitions of N:] \/ [:the Transitions of N,the Places of N:] );

end;

:: deftheorem Def1 defines Petri NET_1:def 1 :

for N being Net holds
( N is Petri iff ( the Places of N misses the Transitions of N & the Flow of N c= [:the Places of N,the Transitions of N:] \/ [:the Transitions of N,the Places of N:] ) );

definition

let N be Net ;
func Elements N -> set equals :: NET_1:def 2
the Places of N \/ the Transitions of N;
correctness
coherence
the Places of N \/ the Transitions of N is set ;
;

end;

:: deftheorem defines Elements NET_1:def 2 :

for N being Net holds Elements N = the Places of N \/ the Transitions of N;

theorem :: NET_1:1

canceled;

theorem :: NET_1:2

canceled;

theorem :: NET_1:3

canceled;

theorem :: NET_1:4

canceled;

theorem :: NET_1:5

canceled;

theorem :: NET_1:6

canceled;

theorem :: NET_1:7

for x being set
for N being Net holds
( not Elements N <> {} or not x is Element of Elements N or x is Element of the Places of N or x is Element of the Transitions of N ) by XBOOLE_0:def 3;

theorem :: NET_1:8

for x being set
for N being Net st x is Element of the Places of N & the Places of N <> {} holds
x is Element of Elements N

proof end;

theorem :: NET_1:9

for x being set
for N being Net st x is Element of the Transitions of N & the Transitions of N <> {} holds
x is Element of Elements N

proof end;

Lm1: Net(# {} ,{} ,{} #) is Petri

proof end;

registration

cluster Net(# {} ,{} ,{} #) -> Petri ;
coherence
Net(# {} ,{} ,{} #) is Petri by Lm1;

end;

registration

cluster strict Petri Net ;
existence
ex b₁ being Net st
( b₁ is strict & b₁ is Petri )

proof end;

end;

definition

mode Pnet is Petri Net ;

end;

theorem :: NET_1:10

canceled;

theorem Th11: :: NET_1:11

for x being set
for N being Pnet holds
( not x in the Places of N or not x in the Transitions of N )

proof end;

theorem Th12: :: NET_1:12

for x, y being set
for N being Pnet st [x,y] in the Flow of N & x in the Transitions of N holds
y in the Places of N

proof end;

theorem Th13: :: NET_1:13

for x, y being set
for N being Pnet st [x,y] in the Flow of N & y in the Transitions of N holds
x in the Places of N

proof end;

theorem :: NET_1:14

for x, y being set
for N being Pnet st [x,y] in the Flow of N & x in the Places of N holds
y in the Transitions of N

proof end;

theorem :: NET_1:15

for x, y being set
for N being Pnet st [x,y] in the Flow of N & y in the Places of N holds
x in the Transitions of N

proof end;

definition

let N be Pnet;
let x, y be set ;
canceled;
canceled;
pred pre N,x,y means :Def5: :: NET_1:def 5
( [y,x] in the Flow of N & x in the Transitions of N );
pred post N,x,y means :Def6: :: NET_1:def 6
( [x,y] in the Flow of N & x in the Transitions of N );

end;

:: deftheorem NET_1:def 3 :

canceled;

:: deftheorem NET_1:def 4 :

canceled;

:: deftheorem Def5 defines pre NET_1:def 5 :

for N being Pnet
for x, y being set holds
( pre N,x,y iff ( [y,x] in the Flow of N & x in the Transitions of N ) );

:: deftheorem Def6 defines post NET_1:def 6 :

for N being Pnet
for x, y being set holds
( post N,x,y iff ( [x,y] in the Flow of N & x in the Transitions of N ) );

definition

let N be Net ;
let x be Element of Elements N;
func Pre N,x -> set means :Def7: :: NET_1:def 7
for y being set holds
( y in it iff ( y in Elements N & [y,x] in the Flow of N ) );
existence
ex b₁ being set st
for y being set holds
( y in b₁ iff ( y in Elements N & [y,x] in the Flow of N ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being set holds
( y in b₁ iff ( y in Elements N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b₂ iff ( y in Elements N & [y,x] in the Flow of N ) ) ) holds
b₁ = b₂

proof end;

func Post N,x -> set means :Def8: :: NET_1:def 8
for y being set holds
( y in it iff ( y in Elements N & [x,y] in the Flow of N ) );
existence
ex b₁ being set st
for y being set holds
( y in b₁ iff ( y in Elements N & [x,y] in the Flow of N ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being set holds
( y in b₁ iff ( y in Elements N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b₂ iff ( y in Elements N & [x,y] in the Flow of N ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Pre NET_1:def 7 :

for N being Net
for x being Element of Elements N
for b₃ being set holds
( b₃ = Pre N,x iff for y being set holds
( y in b₃ iff ( y in Elements N & [y,x] in the Flow of N ) ) );

:: deftheorem Def8 defines Post NET_1:def 8 :

for N being Net
for x being Element of Elements N
for b₃ being set holds
( b₃ = Post N,x iff for y being set holds
( y in b₃ iff ( y in Elements N & [x,y] in the Flow of N ) ) );

theorem Th16: :: NET_1:16

for N being Pnet
for x being Element of Elements N holds Pre N,x c= Elements N

proof end;

theorem :: NET_1:17

for N being Pnet
for x being Element of Elements N holds Pre N,x c= Elements N by Th16;

theorem Th18: :: NET_1:18

for N being Pnet
for x being Element of Elements N holds Post N,x c= Elements N

proof end;

theorem :: NET_1:19

for N being Pnet
for x being Element of Elements N holds Post N,x c= Elements N by Th18;

theorem :: NET_1:20

for x being set
for N being Pnet
for y being Element of Elements N st y in the Transitions of N holds
( x in Pre N,y iff pre N,y,x )

proof end;

theorem :: NET_1:21

for x being set
for N being Pnet
for y being Element of Elements N st y in the Transitions of N holds
( x in Post N,y iff post N,y,x )

proof end;

definition

let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func enter N,x -> set means :Def9: :: NET_1:def 9
( ( x in the Places of N implies it = {x} ) & ( x in the Transitions of N implies it = Pre N,x ) );
existence
ex b₁ being set st
( ( x in the Places of N implies b₁ = {x} ) & ( x in the Transitions of N implies b₁ = Pre N,x ) )

proof end;

uniqueness
for b₁, b₂ being set st ( x in the Places of N implies b₁ = {x} ) & ( x in the Transitions of N implies b₁ = Pre N,x ) & ( x in the Places of N implies b₂ = {x} ) & ( x in the Transitions of N implies b₂ = Pre N,x ) holds
b₁ = b₂ by A1, XBOOLE_0:def 3;

end;

:: deftheorem Def9 defines enter NET_1:def 9 :

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b₃ being set holds
( b₃ = enter N,x iff ( ( x in the Places of N implies b₃ = {x} ) & ( x in the Transitions of N implies b₃ = Pre N,x ) ) );

theorem Th22: :: NET_1:22

for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or enter N,x = {x} or enter N,x = Pre N,x )

proof end;

theorem Th23: :: NET_1:23

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter N,x c= Elements N

proof end;

theorem :: NET_1:24

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter N,x c= Elements N by Th23;

definition

let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func exit N,x -> set means :Def10: :: NET_1:def 10
( ( x in the Places of N implies it = {x} ) & ( x in the Transitions of N implies it = Post N,x ) );
existence
ex b₁ being set st
( ( x in the Places of N implies b₁ = {x} ) & ( x in the Transitions of N implies b₁ = Post N,x ) )

proof end;

uniqueness
for b₁, b₂ being set st ( x in the Places of N implies b₁ = {x} ) & ( x in the Transitions of N implies b₁ = Post N,x ) & ( x in the Places of N implies b₂ = {x} ) & ( x in the Transitions of N implies b₂ = Post N,x ) holds
b₁ = b₂ by A1, XBOOLE_0:def 3;

end;

:: deftheorem Def10 defines exit NET_1:def 10 :

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b₃ being set holds
( b₃ = exit N,x iff ( ( x in the Places of N implies b₃ = {x} ) & ( x in the Transitions of N implies b₃ = Post N,x ) ) );

theorem Th25: :: NET_1:25

for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or exit N,x = {x} or exit N,x = Post N,x )

proof end;

theorem Th26: :: NET_1:26

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit N,x c= Elements N

proof end;

theorem :: NET_1:27

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit N,x c= Elements N by Th26;

definition

let N be Pnet;
let x be Element of Elements N;
func field N,x -> set equals :: NET_1:def 11
(enter N,x) \/ (exit N,x);
correctness
coherence
(enter N,x) \/ (exit N,x) is set ;
;

end;

:: deftheorem defines field NET_1:def 11 :

for N being Pnet
for x being Element of Elements N holds field N,x = (enter N,x) \/ (exit N,x);

definition

let N be Net ;
let x be Element of the Transitions of N;
func Prec N,x -> set means :: NET_1:def 12
for y being set holds
( y in it iff ( y in the Places of N & [y,x] in the Flow of N ) );
existence
ex b₁ being set st
for y being set holds
( y in b₁ iff ( y in the Places of N & [y,x] in the Flow of N ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being set holds
( y in b₁ iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b₂ iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) holds
b₁ = b₂

proof end;

func Postc N,x -> set means :: NET_1:def 13
for y being set holds
( y in it iff ( y in the Places of N & [x,y] in the Flow of N ) );
existence
ex b₁ being set st
for y being set holds
( y in b₁ iff ( y in the Places of N & [x,y] in the Flow of N ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being set holds
( y in b₁ iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b₂ iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Prec NET_1:def 12 :

for N being Net
for x being Element of the Transitions of N
for b₃ being set holds
( b₃ = Prec N,x iff for y being set holds
( y in b₃ iff ( y in the Places of N & [y,x] in the Flow of N ) ) );

:: deftheorem defines Postc NET_1:def 13 :

for N being Net
for x being Element of the Transitions of N
for b₃ being set holds
( b₃ = Postc N,x iff for y being set holds
( y in b₃ iff ( y in the Places of N & [x,y] in the Flow of N ) ) );

definition

let N be Pnet;
let X be set ;
func Entr N,X -> set means :Def14: :: NET_1:def 14
for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) ) & ( for x being set holds
( x in b₂ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) ) holds
b₁ = b₂

proof end;

func Ext N,X -> set means :Def15: :: NET_1:def 15
for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) ) & ( for x being set holds
( x in b₂ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines Entr NET_1:def 14 :

for N being Pnet
for X being set
for b₃ being set holds
( b₃ = Entr N,X iff for x being set holds
( x in b₃ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) );

:: deftheorem Def15 defines Ext NET_1:def 15 :

for N being Pnet
for X being set
for b₃ being set holds
( b₃ = Ext N,X iff for x being set holds
( x in b₃ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) );

theorem Th28: :: NET_1:28

for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
enter N,x in Entr N,X

proof end;

theorem Th29: :: NET_1:29

for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
exit N,x in Ext N,X

proof end;

definition

let N be Pnet;
let X be set ;
func Input N,X -> set equals :: NET_1:def 16
union (Entr N,X);
correctness
coherence
union (Entr N,X) is set ;
;
func Output N,X -> set equals :: NET_1:def 17
union (Ext N,X);
correctness
coherence
union (Ext N,X) is set ;
;

end;

:: deftheorem defines Input NET_1:def 16 :

for N being Pnet
for X being set holds Input N,X = union (Entr N,X);

:: deftheorem defines Output NET_1:def 17 :

for N being Pnet
for X being set holds Output N,X = union (Ext N,X);

theorem :: NET_1:30

for N being Pnet
for x, X being set st X c= Elements N holds
( x in Input N,X iff ex y being Element of Elements N st
( y in X & x in enter N,y ) )

proof end;

theorem :: NET_1:31

for N being Pnet
for x, X being set st X c= Elements N holds
( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) )

proof end;

theorem :: NET_1:32

for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Input N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )

proof end;

theorem :: NET_1:33

for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Output N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & post N,y,x ) ) )

proof end;