:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura

::

:: Received November 27, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

:: Redefinition of Element for Non-empty Relation

definition

let A, B be non empty set ;

let r be non empty Relation of A,B;

:: original: Element

redefine mode Element of r -> Element of [:A,B:];

coherence

for b_{1} being Element of r holds b_{1} is Element of [:A,B:]

end;
let r be non empty Relation of A,B;

:: original: Element

redefine mode Element of r -> Element of [:A,B:];

coherence

for b

proof end;

:: Place/Transition Net Structure

definition

attr c_{1} is strict ;

struct PT_net_Str -> 2-sorted ;

aggr PT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs #) -> PT_net_Str ;

sel S-T_Arcs c_{1} -> Relation of the carrier of c_{1}, the carrier' of c_{1};

sel T-S_Arcs c_{1} -> Relation of the carrier' of c_{1}, the carrier of c_{1};

end;
struct PT_net_Str -> 2-sorted ;

aggr PT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs #) -> PT_net_Str ;

sel S-T_Arcs c

sel T-S_Arcs c

:: deftheorem Def1 defines with_S-T_arc PETRI:def 1 :

for N being PT_net_Str holds

( N is with_S-T_arc iff not the S-T_Arcs of N is empty );

for N being PT_net_Str holds

( N is with_S-T_arc iff not the S-T_Arcs of N is empty );

:: deftheorem Def2 defines with_T-S_arc PETRI:def 2 :

for N being PT_net_Str holds

( N is with_T-S_arc iff not the T-S_Arcs of N is empty );

for N being PT_net_Str holds

( N is with_T-S_arc iff not the T-S_Arcs of N is empty );

definition

PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #) is PT_net_Str ;

end;

func TrivialPetriNet -> PT_net_Str equals :: PETRI:def 3

PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);

coherence PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);

PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #) is PT_net_Str ;

:: deftheorem defines TrivialPetriNet PETRI:def 3 :

TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);

TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);

registration

coherence

( TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void ) ;

end;
( TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void ) ;

registration

existence

ex b_{1} being PT_net_Str st

( not b_{1} is empty & not b_{1} is void & b_{1} is with_S-T_arc & b_{1} is with_T-S_arc & b_{1} is strict )

end;
ex b

( not b

proof end;

registration
end;

registration
end;

:: Place, Transition, and Arc (s->t, t->s) Elements

definition

let PTN be Petri_net;

mode place of PTN is Element of the carrier of PTN;

mode places of PTN is Element of the carrier of PTN;

mode transition of PTN is Element of the carrier' of PTN;

mode transitions of PTN is Element of the carrier' of PTN;

mode S-T_arc of PTN is Element of the S-T_Arcs of PTN;

mode T-S_arc of PTN is Element of the T-S_Arcs of PTN;

end;
mode place of PTN is Element of the carrier of PTN;

mode places of PTN is Element of the carrier of PTN;

mode transition of PTN is Element of the carrier' of PTN;

mode transitions of PTN is Element of the carrier' of PTN;

mode S-T_arc of PTN is Element of the S-T_Arcs of PTN;

mode T-S_arc of PTN is Element of the T-S_Arcs of PTN;

:: Redefinition of Relation for s->t Arcs

definition

let PTN be Petri_net;

let x be S-T_arc of PTN;

:: original: `1

redefine func x `1 -> place of PTN;

coherence

x `1 is place of PTN

redefine func x `2 -> transition of PTN;

coherence

x `2 is transition of PTN

end;
let x be S-T_arc of PTN;

:: original: `1

redefine func x `1 -> place of PTN;

coherence

x `1 is place of PTN

proof end;

:: original: `2redefine func x `2 -> transition of PTN;

coherence

x `2 is transition of PTN

proof end;

:: Redefinition of Relation for t->s Arcs

definition

let PTN be Petri_net;

let x be T-S_arc of PTN;

:: original: `1

redefine func x `1 -> transition of PTN;

coherence

x `1 is transition of PTN

redefine func x `2 -> place of PTN;

coherence

x `2 is place of PTN

end;
let x be T-S_arc of PTN;

:: original: `1

redefine func x `1 -> transition of PTN;

coherence

x `1 is transition of PTN

proof end;

:: original: `2redefine func x `2 -> place of PTN;

coherence

x `2 is place of PTN

proof end;

definition

let PTN be Petri_net;

let S0 be Subset of the carrier of PTN;

{ t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } is Subset of the carrier' of PTN

;

{ t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } is Subset of the carrier' of PTN

;

end;
let S0 be Subset of the carrier of PTN;

func *' S0 -> Subset of the carrier' of PTN equals :: PETRI:def 4

{ t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } ;

coherence { t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } ;

{ t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } is Subset of the carrier' of PTN

proof end;

correctness ;

func S0 *' -> Subset of the carrier' of PTN equals :: PETRI:def 5

{ t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } ;

coherence { t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } ;

{ t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } is Subset of the carrier' of PTN

proof end;

correctness ;

:: deftheorem defines *' PETRI:def 4 :

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds *' S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } ;

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds *' S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [t,s] ) } ;

:: deftheorem defines *' PETRI:def 5 :

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds S0 *' = { t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } ;

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds S0 *' = { t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,t] ) } ;

theorem :: PETRI:1

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds *' S0 = { (f `1) where f is T-S_arc of PTN : f `2 in S0 }

for S0 being Subset of the carrier of PTN holds *' S0 = { (f `1) where f is T-S_arc of PTN : f `2 in S0 }

proof end;

theorem Th2: :: PETRI:2

for PTN being Petri_net

for S0 being Subset of the carrier of PTN

for x being object holds

( x in *' S0 iff ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [x,s] ) )

for S0 being Subset of the carrier of PTN

for x being object holds

( x in *' S0 iff ex f being T-S_arc of PTN ex s being place of PTN st

( s in S0 & f = [x,s] ) )

proof end;

theorem :: PETRI:3

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds S0 *' = { (f `2) where f is S-T_arc of PTN : f `1 in S0 }

for S0 being Subset of the carrier of PTN holds S0 *' = { (f `2) where f is S-T_arc of PTN : f `1 in S0 }

proof end;

theorem Th4: :: PETRI:4

for PTN being Petri_net

for S0 being Subset of the carrier of PTN

for x being object holds

( x in S0 *' iff ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,x] ) )

for S0 being Subset of the carrier of PTN

for x being object holds

( x in S0 *' iff ex f being S-T_arc of PTN ex s being place of PTN st

( s in S0 & f = [s,x] ) )

proof end;

definition

let PTN be Petri_net;

let T0 be Subset of the carrier' of PTN;

{ s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } is Subset of the carrier of PTN

;

{ s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } is Subset of the carrier of PTN

;

end;
let T0 be Subset of the carrier' of PTN;

func *' T0 -> Subset of the carrier of PTN equals :: PETRI:def 6

{ s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } ;

coherence { s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } ;

{ s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } is Subset of the carrier of PTN

proof end;

correctness ;

func T0 *' -> Subset of the carrier of PTN equals :: PETRI:def 7

{ s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } ;

coherence { s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } ;

{ s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } is Subset of the carrier of PTN

proof end;

correctness ;

:: deftheorem defines *' PETRI:def 6 :

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds *' T0 = { s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } ;

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds *' T0 = { s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [s,t] ) } ;

:: deftheorem defines *' PETRI:def 7 :

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds T0 *' = { s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } ;

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds T0 *' = { s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,s] ) } ;

theorem :: PETRI:5

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds *' T0 = { (f `1) where f is S-T_arc of PTN : f `2 in T0 }

for T0 being Subset of the carrier' of PTN holds *' T0 = { (f `1) where f is S-T_arc of PTN : f `2 in T0 }

proof end;

theorem Th6: :: PETRI:6

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN

for x being set holds

( x in *' T0 iff ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [x,t] ) )

for T0 being Subset of the carrier' of PTN

for x being set holds

( x in *' T0 iff ex f being S-T_arc of PTN ex t being transition of PTN st

( t in T0 & f = [x,t] ) )

proof end;

theorem :: PETRI:7

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds T0 *' = { (f `2) where f is T-S_arc of PTN : f `1 in T0 }

for T0 being Subset of the carrier' of PTN holds T0 *' = { (f `2) where f is T-S_arc of PTN : f `1 in T0 }

proof end;

theorem Th8: :: PETRI:8

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN

for x being set holds

( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,x] ) )

for T0 being Subset of the carrier' of PTN

for x being set holds

( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st

( t in T0 & f = [t,x] ) )

proof end;

:: Deadlock-like Attribute for Place Sets

:: deftheorem defines Deadlock-like PETRI:def 8 :

for PTN being Petri_net

for IT being Subset of the carrier of PTN holds

( IT is Deadlock-like iff *' IT is Subset of (IT *') );

for PTN being Petri_net

for IT being Subset of the carrier of PTN holds

( IT is Deadlock-like iff *' IT is Subset of (IT *') );

:: With_Deadlocks Mode for Place\Transition Nets

definition

let IT be Petri_net;

end;
attr IT is With_Deadlocks means :: PETRI:def 9

ex S being Subset of the carrier of IT st S is Deadlock-like ;

ex S being Subset of the carrier of IT st S is Deadlock-like ;

:: deftheorem defines With_Deadlocks PETRI:def 9 :

for IT being Petri_net holds

( IT is With_Deadlocks iff ex S being Subset of the carrier of IT st S is Deadlock-like );

for IT being Petri_net holds

( IT is With_Deadlocks iff ex S being Subset of the carrier of IT st S is Deadlock-like );

:: Trap-like Attribute for Place Sets

:: deftheorem defines Trap-like PETRI:def 10 :

for PTN being Petri_net

for IT being Subset of the carrier of PTN holds

( IT is Trap-like iff IT *' is Subset of (*' IT) );

for PTN being Petri_net

for IT being Subset of the carrier of PTN holds

( IT is Trap-like iff IT *' is Subset of (*' IT) );

:: With_Traps Mode for Place\Transition Nets

definition

let IT be Petri_net;

end;
attr IT is With_Traps means :: PETRI:def 11

ex S being Subset of the carrier of IT st S is Trap-like ;

ex S being Subset of the carrier of IT st S is Trap-like ;

:: deftheorem defines With_Traps PETRI:def 11 :

for IT being Petri_net holds

( IT is With_Traps iff ex S being Subset of the carrier of IT st S is Trap-like );

for IT being Petri_net holds

( IT is With_Traps iff ex S being Subset of the carrier of IT st S is Trap-like );

definition

let A, B be non empty set ;

let r be non empty Relation of A,B;

:: original: ~

redefine func r ~ -> non empty Relation of B,A;

coherence

r ~ is non empty Relation of B,A

end;
let r be non empty Relation of A,B;

:: original: ~

redefine func r ~ -> non empty Relation of B,A;

coherence

r ~ is non empty Relation of B,A

proof end;

:: Duality Definitions and Theorems for Place/Transition Nets

definition

let PTN be PT_net_Str ;

coherence

PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #) is strict PT_net_Str ;

;

end;
func PTN .: -> strict PT_net_Str equals :: PETRI:def 12

PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);

correctness PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);

coherence

PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #) is strict PT_net_Str ;

;

:: deftheorem defines .: PETRI:def 12 :

for PTN being PT_net_Str holds PTN .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);

for PTN being PT_net_Str holds PTN .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);

registration

let PTN be Petri_net;

coherence

( PTN .: is with_S-T_arc & PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )

end;
coherence

( PTN .: is with_S-T_arc & PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )

proof end;

theorem :: PETRI:13

theorem :: PETRI:14

definition

let PTN be Petri_net;

let S0 be Subset of the carrier of PTN;

coherence

S0 is Subset of the carrier of (PTN .:) ;

end;
let S0 be Subset of the carrier of PTN;

coherence

S0 is Subset of the carrier of (PTN .:) ;

:: deftheorem defines .: PETRI:def 13 :

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds S0 .: = S0;

for PTN being Petri_net

for S0 being Subset of the carrier of PTN holds S0 .: = S0;

:: deftheorem defines .: PETRI:def 14 :

for PTN being Petri_net

for s being place of PTN holds s .: = s;

for PTN being Petri_net

for s being place of PTN holds s .: = s;

definition

let PTN be Petri_net;

let S0 be Subset of the carrier of (PTN .:);

coherence

S0 is Subset of the carrier of PTN ;

end;
let S0 be Subset of the carrier of (PTN .:);

coherence

S0 is Subset of the carrier of PTN ;

:: deftheorem defines .: PETRI:def 15 :

for PTN being Petri_net

for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;

for PTN being Petri_net

for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;

:: deftheorem defines .: PETRI:def 16 :

for PTN being Petri_net

for s being place of (PTN .:) holds .: s = s;

for PTN being Petri_net

for s being place of (PTN .:) holds .: s = s;

definition

let PTN be Petri_net;

let T0 be Subset of the carrier' of PTN;

coherence

T0 is Subset of the carrier' of (PTN .:) ;

end;
let T0 be Subset of the carrier' of PTN;

coherence

T0 is Subset of the carrier' of (PTN .:) ;

:: deftheorem defines .: PETRI:def 17 :

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds T0 .: = T0;

for PTN being Petri_net

for T0 being Subset of the carrier' of PTN holds T0 .: = T0;

definition
end;

:: deftheorem defines .: PETRI:def 18 :

for PTN being Petri_net

for t being transition of PTN holds t .: = t;

for PTN being Petri_net

for t being transition of PTN holds t .: = t;

definition

let PTN be Petri_net;

let T0 be Subset of the carrier' of (PTN .:);

coherence

T0 is Subset of the carrier' of PTN ;

end;
let T0 be Subset of the carrier' of (PTN .:);

coherence

T0 is Subset of the carrier' of PTN ;

:: deftheorem defines .: PETRI:def 19 :

for PTN being Petri_net

for T0 being Subset of the carrier' of (PTN .:) holds .: T0 = T0;

for PTN being Petri_net

for T0 being Subset of the carrier' of (PTN .:) holds .: T0 = T0;

definition
end;

:: deftheorem defines .: PETRI:def 20 :

for PTN being Petri_net

for t being transition of (PTN .:) holds .: t = t;

for PTN being Petri_net

for t being transition of (PTN .:) holds .: t = t;

theorem :: PETRI:17

for PTN being Petri_net

for S being Subset of the carrier of PTN holds

( S is Deadlock-like iff S .: is Trap-like )

for S being Subset of the carrier of PTN holds

( S is Deadlock-like iff S .: is Trap-like )

proof end;

theorem :: PETRI:18

for PTN being Petri_net

for S being Subset of the carrier of PTN holds

( S is Trap-like iff S .: is Deadlock-like )

for S being Subset of the carrier of PTN holds

( S is Trap-like iff S .: is Deadlock-like )

proof end;

theorem :: PETRI:19

for PTN being Petri_net

for t being transition of PTN

for S0 being Subset of the carrier of PTN holds

( t in S0 *' iff *' {t} meets S0 )

for t being transition of PTN

for S0 being Subset of the carrier of PTN holds

( t in S0 *' iff *' {t} meets S0 )

proof end;

theorem :: PETRI:20

for PTN being Petri_net

for t being transition of PTN

for S0 being Subset of the carrier of PTN holds

( t in *' S0 iff {t} *' meets S0 )

for t being transition of PTN

for S0 being Subset of the carrier of PTN holds

( t in *' S0 iff {t} *' meets S0 )

proof end;