:: PETRI semantic presentation
begin
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 b1 being Element of r holds b1 is Element of [:A,B:]
proof
let a be Element of r; ::_thesis: a is Element of [:A,B:]
thus a is Element of [:A,B:] ; ::_thesis: verum
end;
end;
definition
attrc1 is strict ;
struct PT_net_Str -> 2-sorted ;
aggrPT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs #) -> PT_net_Str ;
sel S-T_Arcs c1 -> Relation of the carrier of c1, the carrier' of c1;
sel T-S_Arcs c1 -> Relation of the carrier' of c1, the carrier of c1;
end;
definition
let N be PT_net_Str ;
attrN is with_S-T_arc means :Def1: :: PETRI:def 1
not the S-T_Arcs of N is empty ;
attrN is with_T-S_arc means :Def2: :: PETRI:def 2
not the T-S_Arcs of N is empty ;
end;
:: 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 );
:: 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 );
definition
func TrivialPetriNet -> PT_net_Str equals :: PETRI:def 3
PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);
coherence
PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #) is PT_net_Str ;
end;
:: deftheorem defines TrivialPetriNet PETRI:def_3_:_
TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);
registration
cluster TrivialPetriNet -> non empty non void strict with_S-T_arc with_T-S_arc ;
coherence
( TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void )
proof
set N = TrivialPetriNet ;
thus not the S-T_Arcs of TrivialPetriNet is empty ; :: according to PETRI:def_1 ::_thesis: ( TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void )
thus not the T-S_Arcs of TrivialPetriNet is empty ; :: according to PETRI:def_2 ::_thesis: ( TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void )
thus ( TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void ) ; ::_thesis: verum
end;
end;
registration
cluster non empty non void strict with_S-T_arc with_T-S_arc for PT_net_Str ;
existence
ex b1 being PT_net_Str st
( not b1 is empty & not b1 is void & b1 is with_S-T_arc & b1 is with_T-S_arc & b1 is strict )
proof
take TrivialPetriNet ; ::_thesis: ( not TrivialPetriNet is empty & not TrivialPetriNet is void & TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict )
thus ( not TrivialPetriNet is empty & not TrivialPetriNet is void & TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict ) ; ::_thesis: verum
end;
end;
registration
let N be with_S-T_arc PT_net_Str ;
cluster the S-T_Arcs of N -> non empty ;
coherence
not the S-T_Arcs of N is empty by Def1;
end;
registration
let N be with_T-S_arc PT_net_Str ;
cluster the T-S_Arcs of N -> non empty ;
coherence
not the T-S_Arcs of N is empty by Def2;
end;
definition
mode Petri_net is non empty non void with_S-T_arc with_T-S_arc PT_net_Str ;
end;
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;
definition
let PTN be Petri_net;
let x be S-T_arc of PTN;
:: original: `1
redefine funcx `1 -> place of PTN;
coherence
x `1 is place of PTN
proof
thus x `1 is place of PTN ; ::_thesis: verum
end;
:: original: `2
redefine funcx `2 -> transition of PTN;
coherence
x `2 is transition of PTN
proof
thus x `2 is transition of PTN ; ::_thesis: verum
end;
end;
definition
let PTN be Petri_net;
let x be T-S_arc of PTN;
:: original: `1
redefine funcx `1 -> transition of PTN;
coherence
x `1 is transition of PTN
proof
thus x `1 is transition of PTN ; ::_thesis: verum
end;
:: original: `2
redefine funcx `2 -> place of PTN;
coherence
x `2 is place of PTN
proof
thus x `2 is place of PTN ; ::_thesis: verum
end;
end;
definition
let PTN be Petri_net;
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] ) } is Subset of the carrier' of PTN
proof
defpred S1[ set ] means ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [$1,s] );
{ t where t is transition of PTN : S1[t] } is Subset of the carrier' of PTN from DOMAIN_1:sch_7();
hence { 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 ; ::_thesis: verum
end;
correctness
;
funcS0 *' -> 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] ) } is Subset of the carrier' of PTN
proof
defpred S1[ set ] means ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,$1] );
{ t where t is transition of PTN : S1[t] } is Subset of the carrier' of PTN from DOMAIN_1:sch_7();
hence { 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 ; ::_thesis: verum
end;
correctness
;
end;
:: 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] ) } ;
:: 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] ) } ;
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 }
proof
let PTN be Petri_net; ::_thesis: 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 }
let S0 be Subset of the carrier of PTN; ::_thesis: *' S0 = { (f `1) where f is T-S_arc of PTN : f `2 in S0 }
thus *' S0 c= { (f `1) where f is T-S_arc of PTN : f `2 in S0 } :: according to XBOOLE_0:def_10 ::_thesis: { (f `1) where f is T-S_arc of PTN : f `2 in S0 } c= *' S0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in *' S0 or x in { (f `1) where f is T-S_arc of PTN : f `2 in S0 } )
assume x in *' S0 ; ::_thesis: x in { (f `1) where f is T-S_arc of PTN : f `2 in S0 }
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] ) ;
consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [t,s] by A2;
( f `1 = t & f `2 = s ) by A4, MCART_1:7;
hence x in { (f `1) where f is T-S_arc of PTN : f `2 in S0 } by A1, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f `1) where f is T-S_arc of PTN : f `2 in S0 } or x in *' S0 )
assume x in { (f `1) where f is T-S_arc of PTN : f `2 in S0 } ; ::_thesis: x in *' S0
then consider f being T-S_arc of PTN such that
A5: ( x = f `1 & f `2 in S0 ) ;
f = [(f `1),(f `2)] by MCART_1:21;
hence x in *' S0 by A5; ::_thesis: verum
end;
theorem Th2: :: PETRI:2
for PTN being Petri_net
for S0 being Subset of the carrier of PTN
for x being set 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
let PTN be Petri_net; ::_thesis: for S0 being Subset of the carrier of PTN
for x being set 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] ) )
let S0 be Subset of the carrier of PTN; ::_thesis: for x being set 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] ) )
let x be set ; ::_thesis: ( 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] ) )
thus ( x in *' S0 implies ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [x,s] ) ) ::_thesis: ( ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [x,s] ) implies x in *' S0 )
proof
assume x in *' S0 ; ::_thesis: ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [x,s] )
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] ) ;
consider f being T-S_arc of PTN, s being place of PTN such that
A3: ( s in S0 & f = [t,s] ) by A2;
take f ; ::_thesis: ex s being place of PTN st
( s in S0 & f = [x,s] )
take s ; ::_thesis: ( s in S0 & f = [x,s] )
thus ( s in S0 & f = [x,s] ) by A1, A3; ::_thesis: verum
end;
given f being T-S_arc of PTN, s being place of PTN such that A4: s in S0 and
A5: f = [x,s] ; ::_thesis: x in *' S0
x = f `1 by A5, MCART_1:7;
hence x in *' S0 by A4, A5; ::_thesis: verum
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 }
proof
let PTN be Petri_net; ::_thesis: 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 }
let S0 be Subset of the carrier of PTN; ::_thesis: S0 *' = { (f `2) where f is S-T_arc of PTN : f `1 in S0 }
thus S0 *' c= { (f `2) where f is S-T_arc of PTN : f `1 in S0 } :: according to XBOOLE_0:def_10 ::_thesis: { (f `2) where f is S-T_arc of PTN : f `1 in S0 } c= S0 *'
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S0 *' or x in { (f `2) where f is S-T_arc of PTN : f `1 in S0 } )
assume x in S0 *' ; ::_thesis: x in { (f `2) where f is S-T_arc of PTN : f `1 in S0 }
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] ) ;
consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [s,t] by A2;
( f `1 = s & f `2 = t ) by A4, MCART_1:7;
hence x in { (f `2) where f is S-T_arc of PTN : f `1 in S0 } by A1, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f `2) where f is S-T_arc of PTN : f `1 in S0 } or x in S0 *' )
assume x in { (f `2) where f is S-T_arc of PTN : f `1 in S0 } ; ::_thesis: x in S0 *'
then consider f being S-T_arc of PTN such that
A5: ( x = f `2 & f `1 in S0 ) ;
f = [(f `1),(f `2)] by MCART_1:21;
hence x in S0 *' by A5; ::_thesis: verum
end;
theorem Th4: :: PETRI:4
for PTN being Petri_net
for S0 being Subset of the carrier of PTN
for x being set 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
let PTN be Petri_net; ::_thesis: for S0 being Subset of the carrier of PTN
for x being set 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] ) )
let S0 be Subset of the carrier of PTN; ::_thesis: for x being set 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] ) )
let x be set ; ::_thesis: ( 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] ) )
thus ( x in S0 *' implies ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) ) ::_thesis: ( ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) implies x in S0 *' )
proof
assume x in S0 *' ; ::_thesis: ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] )
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] ) ;
consider f being S-T_arc of PTN, s being place of PTN such that
A3: ( s in S0 & f = [s,t] ) by A2;
take f ; ::_thesis: ex s being place of PTN st
( s in S0 & f = [s,x] )
take s ; ::_thesis: ( s in S0 & f = [s,x] )
thus ( s in S0 & f = [s,x] ) by A1, A3; ::_thesis: verum
end;
given f being S-T_arc of PTN, s being place of PTN such that A4: s in S0 and
A5: f = [s,x] ; ::_thesis: x in S0 *'
x = f `2 by A5, MCART_1:7;
hence x in S0 *' by A4, A5; ::_thesis: verum
end;
definition
let PTN be Petri_net;
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] ) } is Subset of the carrier of PTN
proof
defpred S1[ set ] means ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [$1,t] );
{ s where s is place of PTN : S1[s] } is Subset of the carrier of PTN from DOMAIN_1:sch_7();
hence { 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 ; ::_thesis: verum
end;
correctness
;
funcT0 *' -> 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] ) } is Subset of the carrier of PTN
proof
defpred S1[ set ] means ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,$1] );
{ s where s is place of PTN : S1[s] } is Subset of the carrier of PTN from DOMAIN_1:sch_7();
hence { 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 ; ::_thesis: verum
end;
correctness
;
end;
:: 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] ) } ;
:: 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] ) } ;
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 }
proof
let PTN be Petri_net; ::_thesis: 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 }
let T0 be Subset of the carrier' of PTN; ::_thesis: *' T0 = { (f `1) where f is S-T_arc of PTN : f `2 in T0 }
thus *' T0 c= { (f `1) where f is S-T_arc of PTN : f `2 in T0 } :: according to XBOOLE_0:def_10 ::_thesis: { (f `1) where f is S-T_arc of PTN : f `2 in T0 } c= *' T0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in *' T0 or x in { (f `1) where f is S-T_arc of PTN : f `2 in T0 } )
assume x in *' T0 ; ::_thesis: x in { (f `1) where f is S-T_arc of PTN : f `2 in T0 }
then consider s being place of PTN such that
A1: x = s and
A2: ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] ) ;
consider f being S-T_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [s,t] by A2;
( f `1 = s & f `2 = t ) by A4, MCART_1:7;
hence x in { (f `1) where f is S-T_arc of PTN : f `2 in T0 } by A1, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f `1) where f is S-T_arc of PTN : f `2 in T0 } or x in *' T0 )
assume x in { (f `1) where f is S-T_arc of PTN : f `2 in T0 } ; ::_thesis: x in *' T0
then consider f being S-T_arc of PTN such that
A5: ( x = f `1 & f `2 in T0 ) ;
f = [(f `1),(f `2)] by MCART_1:21;
hence x in *' T0 by A5; ::_thesis: verum
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] ) )
proof
let PTN be Petri_net; ::_thesis: 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] ) )
let T0 be Subset of the carrier' of PTN; ::_thesis: 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] ) )
let x be set ; ::_thesis: ( 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] ) )
thus ( x in *' T0 implies ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [x,t] ) ) ::_thesis: ( ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [x,t] ) implies x in *' T0 )
proof
assume x in *' T0 ; ::_thesis: ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [x,t] )
then consider s being place of PTN such that
A1: x = s and
A2: ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] ) ;
consider f being S-T_arc of PTN, t being transition of PTN such that
A3: ( t in T0 & f = [s,t] ) by A2;
take f ; ::_thesis: ex t being transition of PTN st
( t in T0 & f = [x,t] )
take t ; ::_thesis: ( t in T0 & f = [x,t] )
thus ( t in T0 & f = [x,t] ) by A1, A3; ::_thesis: verum
end;
given f being S-T_arc of PTN, t being transition of PTN such that A4: t in T0 and
A5: f = [x,t] ; ::_thesis: x in *' T0
x = f `1 by A5, MCART_1:7;
hence x in *' T0 by A4, A5; ::_thesis: verum
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 }
proof
let PTN be Petri_net; ::_thesis: 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 }
let T0 be Subset of the carrier' of PTN; ::_thesis: T0 *' = { (f `2) where f is T-S_arc of PTN : f `1 in T0 }
thus T0 *' c= { (f `2) where f is T-S_arc of PTN : f `1 in T0 } :: according to XBOOLE_0:def_10 ::_thesis: { (f `2) where f is T-S_arc of PTN : f `1 in T0 } c= T0 *'
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T0 *' or x in { (f `2) where f is T-S_arc of PTN : f `1 in T0 } )
assume x in T0 *' ; ::_thesis: x in { (f `2) where f is T-S_arc of PTN : f `1 in T0 }
then consider s being place of PTN such that
A1: x = s and
A2: ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] ) ;
consider f being T-S_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [t,s] by A2;
( f `1 = t & f `2 = s ) by A4, MCART_1:7;
hence x in { (f `2) where f is T-S_arc of PTN : f `1 in T0 } by A1, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f `2) where f is T-S_arc of PTN : f `1 in T0 } or x in T0 *' )
assume x in { (f `2) where f is T-S_arc of PTN : f `1 in T0 } ; ::_thesis: x in T0 *'
then consider f being T-S_arc of PTN such that
A5: ( x = f `2 & f `1 in T0 ) ;
f = [(f `1),(f `2)] by MCART_1:21;
hence x in T0 *' by A5; ::_thesis: verum
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] ) )
proof
let PTN be Petri_net; ::_thesis: 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] ) )
let T0 be Subset of the carrier' of PTN; ::_thesis: 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] ) )
let x be set ; ::_thesis: ( 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] ) )
thus ( x in T0 *' implies ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) ) ::_thesis: ( ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) implies x in T0 *' )
proof
assume x in T0 *' ; ::_thesis: ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] )
then consider s being place of PTN such that
A1: x = s and
A2: ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] ) ;
consider f being T-S_arc of PTN, t being transition of PTN such that
A3: ( t in T0 & f = [t,s] ) by A2;
take f ; ::_thesis: ex t being transition of PTN st
( t in T0 & f = [t,x] )
take t ; ::_thesis: ( t in T0 & f = [t,x] )
thus ( t in T0 & f = [t,x] ) by A1, A3; ::_thesis: verum
end;
given f being T-S_arc of PTN, t being transition of PTN such that A4: t in T0 and
A5: f = [t,x] ; ::_thesis: x in T0 *'
x = f `2 by A5, MCART_1:7;
hence x in T0 *' by A4, A5; ::_thesis: verum
end;
theorem :: PETRI:9
for PTN being Petri_net holds *' ({} the carrier of PTN) = {}
proof
let PTN be Petri_net; ::_thesis: *' ({} the carrier of PTN) = {}
set x = the Element of *' ({} the carrier of PTN);
assume not *' ({} the carrier of PTN) = {} ; ::_thesis: contradiction
then the Element of *' ({} the carrier of PTN) in *' ({} the carrier of PTN) ;
then ex t being transition of PTN st
( the Element of *' ({} the carrier of PTN) = t & ex f being T-S_arc of PTN ex s being place of PTN st
( s in {} the carrier of PTN & f = [t,s] ) ) ;
hence contradiction ; ::_thesis: verum
end;
theorem :: PETRI:10
for PTN being Petri_net holds ({} the carrier of PTN) *' = {}
proof
let PTN be Petri_net; ::_thesis: ({} the carrier of PTN) *' = {}
set x = the Element of ({} the carrier of PTN) *' ;
assume not ({} the carrier of PTN) *' = {} ; ::_thesis: contradiction
then the Element of ({} the carrier of PTN) *' in ({} the carrier of PTN) *' ;
then ex t being transition of PTN st
( the Element of ({} the carrier of PTN) *' = t & ex f being S-T_arc of PTN ex s being place of PTN st
( s in {} the carrier of PTN & f = [s,t] ) ) ;
hence contradiction ; ::_thesis: verum
end;
theorem :: PETRI:11
for PTN being Petri_net holds *' ({} the carrier' of PTN) = {}
proof
let PTN be Petri_net; ::_thesis: *' ({} the carrier' of PTN) = {}
set x = the Element of *' ({} the carrier' of PTN);
assume not *' ({} the carrier' of PTN) = {} ; ::_thesis: contradiction
then the Element of *' ({} the carrier' of PTN) in *' ({} the carrier' of PTN) ;
then ex s being place of PTN st
( the Element of *' ({} the carrier' of PTN) = s & ex f being S-T_arc of PTN ex t being transition of PTN st
( t in {} the carrier' of PTN & f = [s,t] ) ) ;
hence contradiction ; ::_thesis: verum
end;
theorem :: PETRI:12
for PTN being Petri_net holds ({} the carrier' of PTN) *' = {}
proof
let PTN be Petri_net; ::_thesis: ({} the carrier' of PTN) *' = {}
set x = the Element of ({} the carrier' of PTN) *' ;
assume not ({} the carrier' of PTN) *' = {} ; ::_thesis: contradiction
then the Element of ({} the carrier' of PTN) *' in ({} the carrier' of PTN) *' ;
then ex s being place of PTN st
( the Element of ({} the carrier' of PTN) *' = s & ex f being T-S_arc of PTN ex t being transition of PTN st
( t in {} the carrier' of PTN & f = [t,s] ) ) ;
hence contradiction ; ::_thesis: verum
end;
begin
definition
let PTN be Petri_net;
let IT be Subset of the carrier of PTN;
attrIT is Deadlock-like means :: PETRI:def 8
*' IT is Subset of (IT *');
end;
:: 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 *') );
definition
let IT be Petri_net;
attrIT is With_Deadlocks means :: PETRI:def 9
ex S being Subset of the carrier of IT st S is Deadlock-like ;
end;
:: 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 );
registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc With_Deadlocks for PT_net_Str ;
existence
ex b1 being Petri_net st b1 is With_Deadlocks
proof
take PTN1 = TrivialPetriNet ; ::_thesis: PTN1 is With_Deadlocks
reconsider s = {} as place of PTN1 by TARSKI:def_1;
reconsider t = {} as transition of PTN1 by TARSKI:def_1;
A1: [#] ({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def_1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1, TARSKI:def_1;
{{}} c= the carrier of PTN1 ;
then reconsider S = {{}} as Subset of the carrier of PTN1 ;
take S ; :: according to PETRI:def_9 ::_thesis: S is Deadlock-like
tsf = [t,s] ;
then t in *' S ;
then {t} c= *' S by ZFMISC_1:31;
then A2: {t} = *' S by XBOOLE_0:def_10;
stf = [s,t] ;
then t in S *' ;
hence *' S is Subset of (S *') by A2, ZFMISC_1:31; :: according to PETRI:def_8 ::_thesis: verum
end;
end;
begin
definition
let PTN be Petri_net;
let IT be Subset of the carrier of PTN;
attrIT is Trap-like means :: PETRI:def 10
IT *' is Subset of (*' IT);
end;
:: 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) );
definition
let IT be Petri_net;
attrIT is With_Traps means :: PETRI:def 11
ex S being Subset of the carrier of IT st S is Trap-like ;
end;
:: 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 );
registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc With_Traps for PT_net_Str ;
existence
ex b1 being Petri_net st b1 is With_Traps
proof
take PTN1 = TrivialPetriNet ; ::_thesis: PTN1 is With_Traps
reconsider s = {} as place of PTN1 by TARSKI:def_1;
reconsider t = {} as transition of PTN1 by TARSKI:def_1;
A1: [#] ({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def_1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1, TARSKI:def_1;
{{}} c= the carrier of PTN1 ;
then reconsider S = {{}} as Subset of the carrier of PTN1 ;
take S ; :: according to PETRI:def_11 ::_thesis: S is Trap-like
stf = [s,t] ;
then t in S *' ;
then {t} c= S *' by ZFMISC_1:31;
then A2: {t} = S *' by XBOOLE_0:def_10;
tsf = [t,s] ;
then t in *' S ;
hence S *' is Subset of (*' S) by A2, ZFMISC_1:31; :: according to PETRI:def_10 ::_thesis: verum
end;
end;
definition
let A, B be non empty set ;
let r be non empty Relation of A,B;
:: original: ~
redefine funcr ~ -> non empty Relation of B,A;
coherence
r ~ is non empty Relation of B,A
proof
set x = the Element of r;
consider y, z being set such that
A1: the Element of r = [y,z] by RELAT_1:def_1;
[z,y] in r ~ by A1, RELAT_1:def_7;
hence r ~ is non empty Relation of B,A ; ::_thesis: verum
end;
end;
begin
definition
let PTN be PT_net_Str ;
funcPTN .: -> 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
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;
:: 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 ~) #);
registration
let PTN be Petri_net;
clusterPTN .: -> non empty non void strict with_S-T_arc with_T-S_arc ;
coherence
( PTN .: is with_S-T_arc & PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )
proof
not the T-S_Arcs of PTN ~ is empty ;
hence not the S-T_Arcs of (PTN .:) is empty ; :: according to PETRI:def_1 ::_thesis: ( PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )
not the S-T_Arcs of PTN ~ is empty ;
hence not the T-S_Arcs of (PTN .:) is empty ; :: according to PETRI:def_2 ::_thesis: ( not PTN .: is empty & not PTN .: is void )
thus ( not PTN .: is empty & not PTN .: is void ) ; ::_thesis: verum
end;
end;
theorem :: PETRI:13
for PTN being Petri_net holds (PTN .:) .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN, the S-T_Arcs of PTN, the T-S_Arcs of PTN #) ;
theorem :: PETRI:14
for PTN being Petri_net holds
( the carrier of PTN = the carrier of (PTN .:) & the carrier' of PTN = the carrier' of (PTN .:) & the S-T_Arcs of PTN ~ = the T-S_Arcs of (PTN .:) & the T-S_Arcs of PTN ~ = the S-T_Arcs of (PTN .:) ) ;
definition
let PTN be Petri_net;
let S0 be Subset of the carrier of PTN;
funcS0 .: -> Subset of the carrier of (PTN .:) equals :: PETRI:def 13
S0;
coherence
S0 is Subset of the carrier of (PTN .:) ;
end;
:: deftheorem defines .: PETRI:def_13_:_
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 .: = S0;
definition
let PTN be Petri_net;
let s be place of PTN;
funcs .: -> place of (PTN .:) equals :: PETRI:def 14
s;
coherence
s is place of (PTN .:) ;
end;
:: deftheorem defines .: PETRI:def_14_:_
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 .:);
func .: S0 -> Subset of the carrier of PTN equals :: PETRI:def 15
S0;
coherence
S0 is Subset of the carrier of PTN ;
end;
:: deftheorem defines .: PETRI:def_15_:_
for PTN being Petri_net
for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;
definition
let PTN be Petri_net;
let s be place of (PTN .:);
func .: s -> place of PTN equals :: PETRI:def 16
s;
coherence
s is place of PTN ;
end;
:: deftheorem defines .: PETRI:def_16_:_
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;
funcT0 .: -> Subset of the carrier' of (PTN .:) equals :: PETRI:def 17
T0;
coherence
T0 is Subset of the carrier' of (PTN .:) ;
end;
:: deftheorem defines .: PETRI:def_17_:_
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 .: = T0;
definition
let PTN be Petri_net;
let t be transition of PTN;
funct .: -> transition of (PTN .:) equals :: PETRI:def 18
t;
coherence
t is transition of (PTN .:) ;
end;
:: deftheorem defines .: PETRI:def_18_:_
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 .:);
func .: T0 -> Subset of the carrier' of PTN equals :: PETRI:def 19
T0;
coherence
T0 is Subset of the carrier' of PTN ;
end;
:: deftheorem defines .: PETRI:def_19_:_
for PTN being Petri_net
for T0 being Subset of the carrier' of (PTN .:) holds .: T0 = T0;
definition
let PTN be Petri_net;
let t be transition of (PTN .:);
func .: t -> transition of PTN equals :: PETRI:def 20
t;
coherence
t is transition of PTN ;
end;
:: deftheorem defines .: PETRI:def_20_:_
for PTN being Petri_net
for t being transition of (PTN .:) holds .: t = t;
theorem Th15: :: PETRI:15
for PTN being Petri_net
for S being Subset of the carrier of PTN holds (S .:) *' = *' S
proof
let PTN be Petri_net; ::_thesis: for S being Subset of the carrier of PTN holds (S .:) *' = *' S
let S be Subset of the carrier of PTN; ::_thesis: (S .:) *' = *' S
thus (S .:) *' c= *' S :: according to XBOOLE_0:def_10 ::_thesis: *' S c= (S .:) *'
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S .:) *' or x in *' S )
assume x in (S .:) *' ; ::_thesis: x in *' S
then consider f being S-T_arc of (PTN .:), s being place of (PTN .:) such that
A1: s in S .: and
A2: f = [s,x] by Th4;
[x,(.: s)] is T-S_arc of PTN by A2, RELAT_1:def_7;
hence x in *' S by A1, Th2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in *' S or x in (S .:) *' )
assume x in *' S ; ::_thesis: x in (S .:) *'
then consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S and
A4: f = [x,s] by Th2;
[(s .:),x] is S-T_arc of (PTN .:) by A4, RELAT_1:def_7;
hence x in (S .:) *' by A3, Th4; ::_thesis: verum
end;
theorem Th16: :: PETRI:16
for PTN being Petri_net
for S being Subset of the carrier of PTN holds *' (S .:) = S *'
proof
let PTN be Petri_net; ::_thesis: for S being Subset of the carrier of PTN holds *' (S .:) = S *'
let S be Subset of the carrier of PTN; ::_thesis: *' (S .:) = S *'
thus *' (S .:) c= S *' :: according to XBOOLE_0:def_10 ::_thesis: S *' c= *' (S .:)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in *' (S .:) or x in S *' )
assume x in *' (S .:) ; ::_thesis: x in S *'
then consider f being T-S_arc of (PTN .:), s being place of (PTN .:) such that
A1: s in S .: and
A2: f = [x,s] by Th2;
[(.: s),x] is S-T_arc of PTN by A2, RELAT_1:def_7;
hence x in S *' by A1, Th4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S *' or x in *' (S .:) )
assume x in S *' ; ::_thesis: x in *' (S .:)
then consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S and
A4: f = [s,x] by Th4;
[x,(s .:)] is T-S_arc of (PTN .:) by A4, RELAT_1:def_7;
hence x in *' (S .:) by A3, Th2; ::_thesis: verum
end;
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 )
proof
let PTN be Petri_net; ::_thesis: for S being Subset of the carrier of PTN holds
( S is Deadlock-like iff S .: is Trap-like )
let S be Subset of the carrier of PTN; ::_thesis: ( S is Deadlock-like iff S .: is Trap-like )
A1: (S .:) *' = *' S by Th15;
thus ( S is Deadlock-like implies S .: is Trap-like ) ::_thesis: ( S .: is Trap-like implies S is Deadlock-like )
proof
assume *' S is Subset of (S *') ; :: according to PETRI:def_8 ::_thesis: S .: is Trap-like
hence (S .:) *' is Subset of (*' (S .:)) by A1, Th16; :: according to PETRI:def_10 ::_thesis: verum
end;
assume (S .:) *' is Subset of (*' (S .:)) ; :: according to PETRI:def_10 ::_thesis: S is Deadlock-like
hence *' S is Subset of (S *') by A1, Th16; :: according to PETRI:def_8 ::_thesis: verum
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 )
proof
let PTN be Petri_net; ::_thesis: for S being Subset of the carrier of PTN holds
( S is Trap-like iff S .: is Deadlock-like )
let S be Subset of the carrier of PTN; ::_thesis: ( S is Trap-like iff S .: is Deadlock-like )
A1: (S .:) *' = *' S by Th15;
thus ( S is Trap-like implies S .: is Deadlock-like ) ::_thesis: ( S .: is Deadlock-like implies S is Trap-like )
proof
assume S *' is Subset of (*' S) ; :: according to PETRI:def_10 ::_thesis: S .: is Deadlock-like
hence *' (S .:) is Subset of ((S .:) *') by A1, Th16; :: according to PETRI:def_8 ::_thesis: verum
end;
assume *' (S .:) is Subset of ((S .:) *') ; :: according to PETRI:def_8 ::_thesis: S is Trap-like
hence S *' is Subset of (*' S) by A1, Th16; :: according to PETRI:def_10 ::_thesis: verum
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 )
proof
let PTN be Petri_net; ::_thesis: for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in S0 *' iff *' {t} meets S0 )
let t be transition of PTN; ::_thesis: for S0 being Subset of the carrier of PTN holds
( t in S0 *' iff *' {t} meets S0 )
let S0 be Subset of the carrier of PTN; ::_thesis: ( t in S0 *' iff *' {t} meets S0 )
thus ( t in S0 *' implies *' {t} meets S0 ) ::_thesis: ( *' {t} meets S0 implies t in S0 *' )
proof
assume t in S0 *' ; ::_thesis: *' {t} meets S0
then consider f being S-T_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [s,t] by Th4;
t in {t} by TARSKI:def_1;
then s in *' {t} by A2;
hence (*' {t}) /\ S0 <> {} by A1, XBOOLE_0:def_4; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
assume (*' {t}) /\ S0 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: t in S0 *'
then consider s being place of PTN such that
A3: s in (*' {t}) /\ S0 by SUBSET_1:4;
A4: s in S0 by A3, XBOOLE_0:def_4;
s in *' {t} by A3, XBOOLE_0:def_4;
then consider f being S-T_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [s,t0] by Th6;
t0 = t by A5, TARSKI:def_1;
hence t in S0 *' by A4, A6; ::_thesis: verum
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 )
proof
let PTN be Petri_net; ::_thesis: for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in *' S0 iff {t} *' meets S0 )
let t be transition of PTN; ::_thesis: for S0 being Subset of the carrier of PTN holds
( t in *' S0 iff {t} *' meets S0 )
let S0 be Subset of the carrier of PTN; ::_thesis: ( t in *' S0 iff {t} *' meets S0 )
thus ( t in *' S0 implies {t} *' meets S0 ) ::_thesis: ( {t} *' meets S0 implies t in *' S0 )
proof
assume t in *' S0 ; ::_thesis: {t} *' meets S0
then consider f being T-S_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [t,s] by Th2;
t in {t} by TARSKI:def_1;
then s in {t} *' by A2;
hence ({t} *') /\ S0 <> {} by A1, XBOOLE_0:def_4; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
assume ({t} *') /\ S0 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: t in *' S0
then consider s being place of PTN such that
A3: s in ({t} *') /\ S0 by SUBSET_1:4;
A4: s in S0 by A3, XBOOLE_0:def_4;
s in {t} *' by A3, XBOOLE_0:def_4;
then consider f being T-S_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [t0,s] by Th8;
t0 = t by A5, TARSKI:def_1;
hence t in *' S0 by A4, A6; ::_thesis: verum
end;