:: Lattice of Substitutions
:: by Adam Grabowski
::
:: Received May 21, 1997
:: Copyright (c) 1997-2011 Association of Mizar Users

begin

definition

let V, C be set ;
func SubstitutionSet (V,C) -> Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;
coherence
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } is Subset of (Fin (PFuncs (V,C)))

proof end;

end;

:: deftheorem defines SubstitutionSet SUBSTLAT:def 1 :
for V, C being set holds SubstitutionSet (V,C) = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;

Lm1: for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite

proof end;

theorem Th1: :: SUBSTLAT:1

for V, C being set holds {} in SubstitutionSet (V,C)

proof end;

theorem Th2: :: SUBSTLAT:2

for V, C being set holds {{}} in SubstitutionSet (V,C)

proof end;

registration

let V, C be set ;
cluster SubstitutionSet (V,C) -> non empty ;
coherence
not SubstitutionSet (V,C) is empty by Th2;

end;

definition

let V, C be set ;
let A, B be Element of SubstitutionSet (V,C);
:: original: \/
redefine func A \/ B -> Element of Fin (PFuncs (V,C));
coherence
A \/ B is Element of Fin (PFuncs (V,C))

proof end;

end;

registration

let V, C be set ;
cluster non empty Element of SubstitutionSet (V,C);
existence
not for b₁ being Element of SubstitutionSet (V,C) holds b₁ is empty

proof end;

end;

registration

let V, C be set ;
cluster -> finite Element of SubstitutionSet (V,C);
coherence
for b₁ being Element of SubstitutionSet (V,C) holds b₁ is finite ;

end;

definition

let V, C be set ;
let A be Element of Fin (PFuncs (V,C));
func mi A -> Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2
{ t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;
coherence
{ t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C)

proof end;

end;

:: deftheorem defines mi SUBSTLAT:def 2 :
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;

registration

let V, C be set ;
cluster -> functional Element of SubstitutionSet (V,C);
coherence
for b₁ being Element of SubstitutionSet (V,C) holds b₁ is functional

proof end;

end;

definition

let V, C be set ;
let A, B be Element of Fin (PFuncs (V,C));
func A ^ B -> Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
coherence
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C))

proof end;

end;

:: deftheorem defines ^ SUBSTLAT:def 3 :
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;

theorem Th3: :: SUBSTLAT:3

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A

proof end;

theorem Th4: :: SUBSTLAT:4

for V, C being set
for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A

proof end;

theorem Th5: :: SUBSTLAT:5

for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b

proof end;

theorem Th6: :: SUBSTLAT:6

for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )

proof end;

Lm2: for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B

proof end;

registration

let V, C be set ;
cluster V1() Function-like finite Element of PFuncs (V,C);
existence
ex b₁ being Element of PFuncs (V,C) st b₁ is finite

proof end;

end;

theorem Th7: :: SUBSTLAT:7

for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B

proof end;

theorem Th8: :: SUBSTLAT:8

for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A c= A

proof end;

theorem :: SUBSTLAT:9

for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by Th8, XBOOLE_1:3;

theorem Th10: :: SUBSTLAT:10

for V, C being set
for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )

proof end;

theorem Th11: :: SUBSTLAT:11

for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi K = K

proof end;

theorem Th12: :: SUBSTLAT:12

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B

proof end;

theorem Th13: :: SUBSTLAT:13

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)

proof end;

theorem Th14: :: SUBSTLAT:14

for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D

proof end;

theorem Th15: :: SUBSTLAT:15

for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )

proof end;

theorem :: SUBSTLAT:16

for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;

Lm3: for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )

proof end;

theorem Th17: :: SUBSTLAT:17

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B

proof end;

theorem Th18: :: SUBSTLAT:18

for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B

proof end;

theorem Th19: :: SUBSTLAT:19

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)

proof end;

theorem Th20: :: SUBSTLAT:20

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)

proof end;

theorem Th21: :: SUBSTLAT:21

for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M

proof end;

theorem Th22: :: SUBSTLAT:22

for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

proof end;

Lm4: for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )

proof end;

Lm5: for V, C being set
for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L

proof end;

theorem Th23: :: SUBSTLAT:23

for V, C being set
for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B

proof end;

theorem Th24: :: SUBSTLAT:24

for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A

proof end;

theorem :: SUBSTLAT:25

for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K

proof end;

begin

definition

let V, C be set ;
func SubstLatt (V,C) -> strict LattStr means :Def4: :: SUBSTLAT:def 4
( the carrier of it = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of it . (A,B) = mi (A \/ B) & the L_meet of it . (A,B) = mi (A ^ B) ) ) );
existence
ex b₁ being strict LattStr st
( the carrier of b₁ = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b₁ . (A,B) = mi (A \/ B) & the L_meet of b₁ . (A,B) = mi (A ^ B) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict LattStr st the carrier of b₁ = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b₁ . (A,B) = mi (A \/ B) & the L_meet of b₁ . (A,B) = mi (A ^ B) ) ) & the carrier of b₂ = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b₂ . (A,B) = mi (A \/ B) & the L_meet of b₂ . (A,B) = mi (A ^ B) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :
for V, C being set
for b₃ being strict LattStr holds
( b₃ = SubstLatt (V,C) iff ( the carrier of b₃ = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b₃ . (A,B) = mi (A \/ B) & the L_meet of b₃ . (A,B) = mi (A ^ B) ) ) ) );

registration

let V, C be set ;
cluster SubstLatt (V,C) -> non empty strict ;
coherence
not SubstLatt (V,C) is empty

proof end;

end;

Lm6: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a

proof end;

Lm7: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm8: for V, C being set
for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L

proof end;

Lm9: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b

proof end;

Lm10: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a

proof end;

Lm11: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm12: for V, C being set
for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))

proof end;

Lm13: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a

proof end;

registration

let V, C be set ;
cluster SubstLatt (V,C) -> strict Lattice-like ;
coherence
SubstLatt (V,C) is Lattice-like

proof end;

end;

registration

let V, C be set ;
cluster SubstLatt (V,C) -> strict distributive bounded ;
coherence
( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )

proof end;

end;

theorem :: SUBSTLAT:26

for V, C being set holds Bottom (SubstLatt (V,C)) = {}

proof end;

theorem :: SUBSTLAT:27

for V, C being set holds Top (SubstLatt (V,C)) = {{}}

proof end;