PETRI_2: Cell Petri Net Concepts

:: Cell Petri Net Concepts
:: by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,
::
:: Received October 14, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users

definition

let A be non empty set ;
let B, Bo be set ;
let yo be Function of Bo,A;
assume A1: Bo c= B ;

func cylinder0 (A,B,Bo,yo) -> non empty Subset of (Funcs (B,A)) equals :Def1: :: PETRI_2:def 1
{ y where y is Function of B,A : y | Bo = yo } ;

correctness

proof end;

end;

:: deftheorem Def1 defines cylinder0 PETRI_2:def 1 :

definition

let A be non empty set ;
let B be set ;

mode thin_cylinder of A,B -> non empty Subset of (Funcs (B,A)) means :Def2: :: PETRI_2:def 2
ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & it = cylinder0 (A,B,Bo,yo) );

existence

proof end;

end;

:: deftheorem Def2 defines thin_cylinder PETRI_2:def 2 :

theorem Th1: :: PETRI_2:1

for A being non empty set
for B being set
for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } )

proof end;

theorem :: PETRI_2:2

for A1, A2 being non empty set
for B being set
for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2

proof end;

definition

let A be non empty set ;
let B be set ;

func thin_cylinders (A,B) -> non empty Subset-Family of (Funcs (B,A)) equals :: PETRI_2:def 3
{ D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;

correctness

proof end;

end;

:: deftheorem defines thin_cylinders PETRI_2:def 3 :

Lm1: for A being non empty set
for B, C being set st B c= C holds
thin_cylinders (A,B) c= bool (PFuncs (C,A))

proof end;

Lm2: for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )

proof end;

Lm3: for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )

proof end;

Lm4: for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }

proof end;

theorem Th3: :: PETRI_2:3

for A being non trivial set
for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )

proof end;

theorem Th4: :: PETRI_2:4

for A1, A2 being non empty set
for B1, B2 being set st A1 c= A2 & B1 c= B2 holds
ex F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) )

proof end;

theorem Th5: :: PETRI_2:5

for A1, A2 being non empty set
for B1, B2 being set ex G being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) )

proof end;

definition

let A1, A2 be non trivial set ;
let B1, B2 be set ;
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ;

func Extcylinders (A1,B1,A2,B2) -> Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) means :: PETRI_2:def 4
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & it . x = cylinder0 (A2,B2,Bo,yo2) );

existence by A1, A2, Th4;
uniqueness

proof end;

end;

:: deftheorem defines Extcylinders PETRI_2:def 4 :

definition

let A1 be non empty set ;
let A2 be non trivial set ;
let B1, B2 be set ;

func Ristcylinders (A1,B1,A2,B2) -> Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) means :: PETRI_2:def 5
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & it . x = cylinder0 (A1,B1,Bo1,yo1) );

existence by Th5;
uniqueness

proof end;

end;

:: deftheorem defines Ristcylinders PETRI_2:def 5 :

definition

let A be non trivial set ;
let B be set ;
let D be thin_cylinder of A,B;

func loc D -> finite Subset of B means :: PETRI_2:def 6
ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & it = Bo );

existence

proof end;

uniqueness by Lm4;

end;

:: deftheorem defines loc PETRI_2:def 6 :

definition

let A1, A2 be non trivial set ;
let B1, B2 be set ;
let C1, C2 be non trivial set ;
let D1, D2 be set ;
let F be Function of (thin_cylinders (A1,B1)),(thin_cylinders (C1,D1));

func CylinderFunc (A1,B1,A2,B2,C1,D1,C2,D2,F) -> Function of (thin_cylinders (A2,B2)),(thin_cylinders (C2,D2)) equals :: PETRI_2:def 7
((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2));

correctness ;

end;

:: deftheorem defines CylinderFunc PETRI_2:def 7 :

definition

attr c₁ is strict ;
struct Colored_PT_net_Str -> PT_net_Str ;
aggr Colored_PT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs, ColoredSet, firing-rule #) -> Colored_PT_net_Str ;
sel ColoredSet c₁ -> non empty finite set ;
sel firing-rule c₁ -> Function;

end;

definition

func TrivialColoredPetriNet -> Colored_PT_net_Str equals :: PETRI_2:def 8
Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

coherence ;

end;

:: deftheorem defines TrivialColoredPetriNet PETRI_2:def 8 :

registration

cluster TrivialColoredPetriNet -> non empty non void with_S-T_arc with_T-S_arc ;

coherence ;

end;

registration

cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str ;

existence

proof end;

end;

definition

mode Colored_Petri_net is non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str ;

end;

definition

let CPNT be Colored_Petri_net;
let t0 be transition of CPNT;

attr t0 is outbound means :: PETRI_2:def 9
{t0} *' = {} ;

end;

:: deftheorem defines outbound PETRI_2:def 9 :

definition

let CPNT1 be Colored_Petri_net;

func Outbds CPNT1 -> Subset of the carrier' of CPNT1 equals :: PETRI_2:def 10
{ x where x is transition of CPNT1 : x is outbound } ;

coherence

proof end;

end;

:: deftheorem defines Outbds PETRI_2:def 10 :

definition

let CPNT be Colored_Petri_net;

attr CPNT is Colored-PT-net-like means :Def11: :: PETRI_2:def 11
( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) );

end;

:: deftheorem Def11 defines Colored-PT-net-like PETRI_2:def 11 :

theorem :: PETRI_2:6

for CPNT being Colored_Petri_net
for t being transition of CPNT st CPNT is Colored-PT-net-like & t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ;

theorem Th7: :: PETRI_2:7

for CPNT1, CPNT2 being Colored_Petri_net
for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )

proof end;

Lm5: for f1, f2, f3, f4, g being Function st (dom f1) /\ (dom f2) = {} & (dom f1) /\ (dom f3) = {} & (dom f1) /\ (dom f4) = {} & (dom f2) /\ (dom f3) = {} & (dom f2) /\ (dom f4) = {} & (dom f3) /\ (dom f4) = {} & g = ((f1 +* f2) +* f3) +* f4 holds
( ( for x being set st x in dom f1 holds
g . x = f1 . x ) & ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )

proof end;

Lm6: for A, B, C, D, X1, X2, X3, X4 being set st A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D holds
( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )

proof end;

registration

cluster non empty non void V52() with_S-T_arc with_T-S_arc strict Colored-PT-net-like for Colored_PT_net_Str ;

existence

proof end;

end;

definition

mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;

end;

definition

let CPNT1, CPNT2 be Colored_Petri_net;

pred CPNT1 misses CPNT2 means :: PETRI_2:def 12
( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} );

symmetry ;

end;

:: deftheorem defines misses PETRI_2:def 12 :

definition

let CPNT1, CPNT2 be Colored_Petri_net;

mode connecting-mapping of CPNT1,CPNT2 -> set means :Def13: :: PETRI_2:def 13
ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st it = [O12,O21];

correctness

proof end;

end;

:: deftheorem Def13 defines connecting-mapping PETRI_2:def 13 :

definition

let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;

mode connecting-firing-rule of CPNT1,CPNT2,O -> set means :Def14: :: PETRI_2:def 14
ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) & it = [q12,q21] );

correctness

proof end;

end;

:: deftheorem Def14 defines connecting-firing-rule PETRI_2:def 14 :

definition

let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;
let q be connecting-firing-rule of CPNT1,CPNT2,O;
assume A1: CPNT1 misses CPNT2 ;

func synthesis (CPNT1,CPNT2,O,q) -> strict Colored-PT-net means :: PETRI_2:def 15
ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) & q = [q12,q21] & the carrier of it = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of it = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of it = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of it = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of it = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of it = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines synthesis PETRI_2:def 15 :