:: NET_1 semantic presentation

definition

attr a₁ 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 c₁ be Net ;
attr a₁ is Petri means :Def1: :: NET_1:def 1
( the Places of a₁ misses the Transitions of a₁ & the Flow of a₁ c= [:the Places of a₁,the Transitions of a₁:] \/ [:the Transitions of a₁,the Places of a₁:] );

end;

:: deftheorem Def1 defines Petri NET_1:def 1 :

notation

let c₁ be Net ;
synonym c₁ is_Petri_net for Petri c₁;

end;

definition

let c₁ be Net ;
func Elements c₁ -> set equals :: NET_1:def 2
the Places of a₁ \/ the Transitions of a₁;
correctness ;

end;

:: deftheorem Def2 defines Elements NET_1:def 2 :

theorem Th1: :: NET_1:1

canceled;

theorem Th2: :: NET_1:2

canceled;

theorem Th3: :: NET_1:3

canceled;

theorem Th4: :: NET_1:4

for b₁ being Net holds the Places of b₁ c= Elements b₁ by XBOOLE_1:7;

theorem Th5: :: NET_1:5

for b₁ being Net holds the Transitions of b₁ c= Elements b₁ by XBOOLE_1:7;

theorem Th6: :: NET_1:6

for b₁ being set
for b₂ being Net holds
( b₁ in Elements b₂ iff ( b₁ in the Places of b₂ or b₁ in the Transitions of b₂ ) ) by XBOOLE_0:def 2;

theorem Th7: :: NET_1:7

for b₁ being set
for b₂ being Net holds
( not Elements b₂ <> {} or not b₁ is Element of Elements b₂ or b₁ is Element of the Places of b₂ or b₁ is Element of the Transitions of b₂ ) by Th6;

theorem Th8: :: NET_1:8

for b₁ being set
for b₂ being Net st b₁ is Element of the Places of b₂ & the Places of b₂ <> {} holds
b₁ is Element of Elements b₂

proof end;

theorem Th9: :: NET_1:9

for b₁ being set
for b₂ being Net st b₁ is Element of the Transitions of b₂ & the Transitions of b₂ <> {} holds
b₁ is Element of Elements b₂

proof end;

Lemma5: Net(# {} ,{} ,{} #) is_Petri_net

proof end;

registration

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

end;

registration

cluster strict Petri Net ;
existence

proof end;

end;

definition

mode Pnet is Petri Net ;

end;

theorem Th10: :: NET_1:10

canceled;

theorem Th11: :: NET_1:11

for b₁ being set
for b₂ being Pnet holds
( not b₁ in the Places of b₂ or not b₁ in the Transitions of b₂ )

proof end;

theorem Th12: :: NET_1:12

for b₁, b₂ being set
for b₃ being Pnet st [b₁,b₂] in the Flow of b₃ & b₁ in the Transitions of b₃ holds
b₂ in the Places of b₃

proof end;

theorem Th13: :: NET_1:13

for b₁, b₂ being set
for b₃ being Pnet st [b₁,b₂] in the Flow of b₃ & b₂ in the Transitions of b₃ holds
b₁ in the Places of b₃

proof end;

theorem Th14: :: NET_1:14

for b₁, b₂ being set
for b₃ being Pnet st [b₁,b₂] in the Flow of b₃ & b₁ in the Places of b₃ holds
b₂ in the Transitions of b₃

proof end;

theorem Th15: :: NET_1:15

for b₁, b₂ being set
for b₃ being Pnet st [b₁,b₂] in the Flow of b₃ & b₂ in the Places of b₃ holds
b₁ in the Transitions of b₃

proof end;

definition

let c₁ be Pnet;
let c₂, c₃ be set ;
canceled;
canceled;
pred pre c₁,c₂,c₃ means :Def5: :: NET_1:def 5
( [a₃,a₂] in the Flow of a₁ & a₂ in the Transitions of a₁ );
pred post c₁,c₂,c₃ means :Def6: :: NET_1:def 6
( [a₂,a₃] in the Flow of a₁ & a₂ in the Transitions of a₁ );

end;

:: deftheorem Def3 NET_1:def 3 :

:: deftheorem Def4 NET_1:def 4 :

:: deftheorem Def5 defines pre NET_1:def 5 :

:: deftheorem Def6 defines post NET_1:def 6 :

definition

let c₁ be Net ;
let c₂ be Element of Elements c₁;
func Pre c₁,c₂ -> set means :Def7: :: NET_1:def 7
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in Elements a₁ & [b₁,a₂] in the Flow of a₁ ) );
existence

proof end;

uniqueness

proof end;

func Post c₁,c₂ -> set means :Def8: :: NET_1:def 8
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in Elements a₁ & [a₂,b₁] in the Flow of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Pre NET_1:def 7 :

:: deftheorem Def8 defines Post NET_1:def 8 :

theorem Th16: :: NET_1:16

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds Pre b₁,b₂ c= Elements b₁

proof end;

theorem Th17: :: NET_1:17

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds Pre b₁,b₂ c= Elements b₁ by Th16;

theorem Th18: :: NET_1:18

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds Post b₁,b₂ c= Elements b₁

proof end;

theorem Th19: :: NET_1:19

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds Post b₁,b₂ c= Elements b₁ by Th18;

theorem Th20: :: NET_1:20

for b₁ being set
for b₂ being Pnet
for b₃ being Element of Elements b₂ st b₃ in the Transitions of b₂ holds
( b₁ in Pre b₂,b₃ iff pre b₂,b₃,b₁ )

proof end;

theorem Th21: :: NET_1:21

for b₁ being set
for b₂ being Pnet
for b₃ being Element of Elements b₂ st b₃ in the Transitions of b₂ holds
( b₁ in Post b₂,b₃ iff post b₂,b₃,b₁ )

proof end;

definition

let c₁ be Pnet;
let c₂ be Element of Elements c₁;
assume E15: Elements c₁ <> {} ;
func enter c₁,c₂ -> set means :Def9: :: NET_1:def 9
( ( a₂ in the Places of a₁ implies a₃ = {a₂} ) & ( a₂ in the Transitions of a₁ implies a₃ = Pre a₁,a₂ ) );
existence

proof end;

uniqueness by E15, Th6;

end;

:: deftheorem Def9 defines enter NET_1:def 9 :

theorem Th22: :: NET_1:22

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds
( not Elements b₁ <> {} or enter b₁,b₂ = {b₂} or enter b₁,b₂ = Pre b₁,b₂ )

proof end;

theorem Th23: :: NET_1:23

for b₁ being Pnet
for b₂ being Element of Elements b₁ st Elements b₁ <> {} holds
enter b₁,b₂ c= Elements b₁

proof end;

theorem Th24: :: NET_1:24

for b₁ being Pnet
for b₂ being Element of Elements b₁ st Elements b₁ <> {} holds
enter b₁,b₂ c= Elements b₁ by Th23;

definition

let c₁ be Pnet;
let c₂ be Element of Elements c₁;
assume E18: Elements c₁ <> {} ;
func exit c₁,c₂ -> set means :Def10: :: NET_1:def 10
( ( a₂ in the Places of a₁ implies a₃ = {a₂} ) & ( a₂ in the Transitions of a₁ implies a₃ = Post a₁,a₂ ) );
existence

proof end;

uniqueness by E18, Th6;

end;

:: deftheorem Def10 defines exit NET_1:def 10 :

theorem Th25: :: NET_1:25

for b₁ being Pnet
for b₂ being Element of Elements b₁ holds
( not Elements b₁ <> {} or exit b₁,b₂ = {b₂} or exit b₁,b₂ = Post b₁,b₂ )

proof end;

theorem Th26: :: NET_1:26

for b₁ being Pnet
for b₂ being Element of Elements b₁ st Elements b₁ <> {} holds
exit b₁,b₂ c= Elements b₁

proof end;

theorem Th27: :: NET_1:27

for b₁ being Pnet
for b₂ being Element of Elements b₁ st Elements b₁ <> {} holds
exit b₁,b₂ c= Elements b₁ by Th26;

definition

let c₁ be Pnet;
let c₂ be Element of Elements c₁;
func field c₁,c₂ -> set equals :: NET_1:def 11
(enter a₁,a₂) \/ (exit a₁,a₂);
correctness ;

end;

:: deftheorem Def11 defines field NET_1:def 11 :

definition

let c₁ be Net ;
let c₂ be Element of the Transitions of c₁;
func Prec c₁,c₂ -> set means :: NET_1:def 12
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in the Places of a₁ & [b₁,a₂] in the Flow of a₁ ) );
existence

proof end;

uniqueness

proof end;

func Postc c₁,c₂ -> set means :: NET_1:def 13
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in the Places of a₁ & [a₂,b₁] in the Flow of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Prec NET_1:def 12 :

:: deftheorem Def13 defines Postc NET_1:def 13 :

definition

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

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Entr NET_1:def 14 :

:: deftheorem Def15 defines Ext NET_1:def 15 :

theorem Th28: :: NET_1:28

for b₁ being Pnet
for b₂ being Element of Elements b₁
for b₃ being set st Elements b₁ <> {} & b₃ c= Elements b₁ & b₂ in b₃ holds
enter b₁,b₂ in Entr b₁,b₃

proof end;

theorem Th29: :: NET_1:29

for b₁ being Pnet
for b₂ being Element of Elements b₁
for b₃ being set st Elements b₁ <> {} & b₃ c= Elements b₁ & b₂ in b₃ holds
exit b₁,b₂ in Ext b₁,b₃

proof end;

definition

let c₁ be Pnet;
let c₂ be set ;
func Input c₁,c₂ -> set equals :: NET_1:def 16
union (Entr a₁,a₂);
correctness ;
func Output c₁,c₂ -> set equals :: NET_1:def 17
union (Ext a₁,a₂);
correctness ;

end;

:: deftheorem Def16 defines Input NET_1:def 16 :

:: deftheorem Def17 defines Output NET_1:def 17 :

theorem Th30: :: NET_1:30

for b₁ being Pnet
for b₂, b₃ being set st Elements b₁ <> {} & b₃ c= Elements b₁ holds
( b₂ in Input b₁,b₃ iff ex b₄ being Element of Elements b₁ st
( b₄ in b₃ & b₂ in enter b₁,b₄ ) )

proof end;

theorem Th31: :: NET_1:31

for b₁ being Pnet
for b₂, b₃ being set st Elements b₁ <> {} & b₃ c= Elements b₁ holds
( b₂ in Output b₁,b₃ iff ex b₄ being Element of Elements b₁ st
( b₄ in b₃ & b₂ in exit b₁,b₄ ) )

proof end;

theorem Th32: :: NET_1:32

for b₁ being Pnet
for b₂ being Subset of (Elements b₁)
for b₃ being Element of Elements b₁ st Elements b₁ <> {} holds
( b₃ in Input b₁,b₂ iff ( ( b₃ in b₂ & b₃ in the Places of b₁ ) or ex b₄ being Element of Elements b₁ st
( b₄ in b₂ & b₄ in the Transitions of b₁ & pre b₁,b₄,b₃ ) ) )

proof end;

theorem Th33: :: NET_1:33

for b₁ being Pnet
for b₂ being Subset of (Elements b₁)
for b₃ being Element of Elements b₁ st Elements b₁ <> {} holds
( b₃ in Output b₁,b₂ iff ( ( b₃ in b₂ & b₃ in the Places of b₁ ) or ex b₄ being Element of Elements b₁ st
( b₄ in b₂ & b₄ in the Transitions of b₁ & post b₁,b₄,b₃ ) ) )

proof end;