PETRI_2: Cell Petri Net Concepts

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

begin

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 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 means :Def2: :: PETRI_2:def 2
ex Bo being Subset of 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 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 equals :: PETRI_2:def 3
{ D where D is Subset of : 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
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
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
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 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 ex Bo1 being Subset of 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 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 ex Bo1 being Subset of 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 means :: PETRI_2:def 6
ex Bo being Subset of 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 :

begin

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(# Places, Transitions, 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

let CPNT be Colored_PT_net_Str ;
let t0 be transition of ;
attr t0 is outbound means :Def8: :: PETRI_2:def 8
{t0} *' = {} ;

end;

:: deftheorem Def8 defines outbound PETRI_2:def 8 :

definition

let CPNT1 be Colored_PT_net_Str ;
func Outbds CPNT1 -> Subset of equals :: PETRI_2:def 9
{ x where x is transition of : x is outbound } ;
coherence

proof end;

end;

:: deftheorem defines Outbds PETRI_2:def 9 :

definition

let CPNT be Colored_PT_net_Str ;
attr CPNT is Colored-PT-net-like means :Def10: :: PETRI_2:def 10
( dom the firing-rule of CPNT c= the Transitions of CPNT \ (Outbds CPNT) & ( for t being transition of st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of CPNT . t is Function of thin_cylinders CS,I, thin_cylinders CS,O ) );

end;

:: deftheorem Def10 defines Colored-PT-net-like PETRI_2:def 10 :

theorem :: PETRI_2:6

for CPNT being Colored_PT_net_Str
for t being transition of st CPNT is Colored-PT-net-like & t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of CPNT . t is Function of thin_cylinders CS,I, thin_cylinders CS,O by Def10;

theorem Th7: :: PETRI_2:7

for CPNT1, CPNT2 being Colored_PT_net_Str
for t1 being transition of
for t2 being transition of st the Places of CPNT1 c= the Places 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 strict Colored-PT-net-like Colored_PT_net_Str ;
existence

proof end;

end;

definition

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

end;

begin

definition

let CPNT1, CPNT2 be Colored_PT_net_Str ;
pred CPNT1 misses CPNT2 means :Def11: :: PETRI_2:def 11
( the Places of CPNT1 /\ the Places of CPNT2 = {} & the Transitions of CPNT1 /\ the Transitions of CPNT2 = {} );
symmetry ;

end;

:: deftheorem Def11 defines misses PETRI_2:def 11 :

begin

definition

let CPNT1, CPNT2 be Colored_PT_net_Str ;
mode connecting-mapping of CPNT1,CPNT2 -> set means :Def12: :: PETRI_2:def 12
ex O12 being Function of Outbds CPNT1,the Places of CPNT2 ex O21 being Function of Outbds CPNT2,the Places of CPNT1 st it = [O12,O21];
correctness

proof end;

end;

:: deftheorem Def12 defines connecting-mapping PETRI_2:def 12 :

begin

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 :Def13: :: PETRI_2:def 13
ex q12, q21 being Function ex O12 being Function of Outbds CPNT1,the Places of CPNT2 ex O21 being Function of Outbds CPNT2,the Places of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of 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 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 Def13 defines connecting-firing-rule PETRI_2:def 13 :

begin

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 14
ex q12, q21 being Function ex O12 being Function of Outbds CPNT1,the Places of CPNT2 ex O21 being Function of Outbds CPNT2,the Places of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of 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 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 Places of it = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of it = the Transitions of CPNT1 \/ the Transitions 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 14 :