:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines Petri NET_1:def 1 :
:: deftheorem defines Elements NET_1:def 2 :
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
theorem :: NET_1:8
theorem :: NET_1:9
Lm1:
Net(# {} ,{} ,{} #) is Petri
theorem :: NET_1:10
canceled;
theorem Th11: :: NET_1:11
theorem Th12: :: NET_1:12
theorem Th13: :: NET_1:13
theorem :: NET_1:14
theorem :: NET_1:15
:: deftheorem NET_1:def 3 :
canceled;
:: deftheorem NET_1:def 4 :
canceled;
:: deftheorem Def5 defines pre NET_1:def 5 :
:: deftheorem Def6 defines post NET_1:def 6 :
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 b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [y,x] in the Flow of N ) ) ) holds
b1 = b2
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 b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [x,y] in the Flow of N ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines Pre NET_1:def 7 :
:: deftheorem Def8 defines Post NET_1:def 8 :
theorem Th16: :: NET_1:16
theorem :: NET_1:17
theorem Th18: :: NET_1:18
theorem :: NET_1:19
theorem :: NET_1:20
theorem :: NET_1:21
:: deftheorem Def9 defines enter NET_1:def 9 :
theorem Th22: :: NET_1:22
theorem Th23: :: NET_1:23
theorem :: NET_1:24
:: deftheorem Def10 defines exit NET_1:def 10 :
theorem Th25: :: NET_1:25
theorem Th26: :: NET_1:26
theorem :: NET_1:27
:: deftheorem defines field NET_1:def 11 :
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 b1 being set st
for y being set holds
( y in b1 iff ( y in the Places of N & [y,x] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) holds
b1 = b2
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 b1 being set st
for y being set holds
( y in b1 iff ( y in the Places of N & [x,y] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) holds
b1 = b2
end;
:: deftheorem defines Prec NET_1:def 12 :
:: deftheorem defines Postc NET_1:def 13 :
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 b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) ) holds
b1 = b2
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 b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def14 defines Entr NET_1:def 14 :
:: deftheorem Def15 defines Ext NET_1:def 15 :
theorem Th28: :: NET_1:28
theorem Th29: :: NET_1:29
:: deftheorem defines Input NET_1:def 16 :
:: deftheorem defines Output NET_1:def 17 :
theorem :: NET_1:30
theorem :: NET_1:31
theorem :: NET_1:32
theorem :: NET_1:33