:: Preliminaries to Structures
:: by Library Committee
::
:: Received January 6, 1995
:: Copyright (c) 1995 Association of Mizar Users


begin

definition
attr c1 is strict ;
struct 1-sorted -> ;
aggr 1-sorted(# carrier #) -> 1-sorted ;
sel carrier c1 -> set ;
end;

definition
let S be 1-sorted ;
attr S is empty means :Def1: :: STRUCT_0:def 1
 the carrier of S is empty ;
end;

:: deftheorem Def1 defines empty STRUCT_0:def 1 :
for S being 1-sorted holds
( S is empty iff the carrier of S is empty );

registration
cluster strict empty 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is empty )
proof end;
end;

registration
cluster strict non empty 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
let S be empty 1-sorted ;
cluster the carrier of S -> empty ;
coherence
the carrier of S is empty by Def1;
end;

registration
let S be non empty 1-sorted ;
cluster the carrier of S -> non empty ;
coherence
not the carrier of S is empty by Def1;
end;

definition
let S be 1-sorted ;
mode Element of S is Element of the carrier of S;
mode Subset of S is Subset of the carrier of S;
mode Subset-Family of S is Subset-Family of the carrier of S;
end;

definition
let S be 1-sorted ;
let X be set ;
mode Function of S,X is Function of the carrier of S,X;
mode Function of X,S is Function of X, the carrier of S;
end;

definition
let S, T be 1-sorted ;
mode Function of S,T is Function of the carrier of S, the carrier of T;
end;

definition
let T be 1-sorted ;
func {} T -> Subset of T equals :: STRUCT_0:def 2
 {} ;
coherence
{} is Subset of T
proof end;
func [#] T -> Subset of T equals :: STRUCT_0:def 3
 the carrier of T;
coherence
the carrier of T is Subset of T
proof end;
end;

:: deftheorem defines {} STRUCT_0:def 2 :
for T being 1-sorted holds {} T = {} ;

:: deftheorem defines [#] STRUCT_0:def 3 :
for T being 1-sorted holds [#] T = the carrier of T;

registration
let T be 1-sorted ;
cluster {} T -> empty ;
coherence
{} T is empty ;
end;

registration
let T be empty 1-sorted ;
cluster [#] T -> empty ;
coherence
[#] T is empty ;
end;

registration
let T be non empty 1-sorted ;
cluster [#] T -> non empty ;
coherence
not [#] T is empty ;
end;

registration
let S be non empty 1-sorted ;
cluster non empty Element of K21( the carrier of S);
existence
not for b1 being Subset of S holds b1 is empty
proof end;
end;

definition
let S be 1-sorted ;
mode FinSequence of S is FinSequence of the carrier of S;
end;

definition
let S be 1-sorted ;
mode ManySortedSet of S is ManySortedSet of the carrier of S;
end;

definition
let S be 1-sorted ;
func id S -> Function of S,S equals :: STRUCT_0:def 4
 id the carrier of S;
coherence
id the carrier of S is Function of S,S ;
end;

:: deftheorem defines id STRUCT_0:def 4 :
for S being 1-sorted holds id S = id the carrier of S;

definition
let S be 1-sorted ;
mode sequence of S is sequence of the carrier of S;
end;

definition
let S, T be 1-sorted ;
mode PartFunc of S,T is PartFunc of the carrier of S, the carrier of T;
end;

definition
let S be 1-sorted ;
let x be set ;
pred x in S means :: STRUCT_0:def 5
x in the carrier of S;
end;

:: deftheorem defines in STRUCT_0:def 5 :
for S being 1-sorted
for x being set holds
( x in S iff x in the carrier of S );

definition
attr c1 is strict ;
struct ZeroStr -> 1-sorted ;
aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;
sel ZeroF c1 -> Element of the carrier of c1;
end;

registration
cluster non empty strict ZeroStr ;
existence
ex b1 being ZeroStr st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
attr c1 is strict ;
struct OneStr -> 1-sorted ;
aggr OneStr(# carrier, OneF #) -> OneStr ;
sel OneF c1 -> Element of the carrier of c1;
end;

definition
attr c1 is strict ;
struct ZeroOneStr -> ZeroStr , OneStr ;
aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;
end;

definition
let S be ZeroStr ;
func 0. S -> Element of S equals :: STRUCT_0:def 6
 the ZeroF of S;
coherence
the ZeroF of S is Element of S ;
end;

:: deftheorem defines 0. STRUCT_0:def 6 :
for S being ZeroStr holds 0. S = the ZeroF of S;

definition
let S be OneStr ;
func 1. S -> Element of S equals :: STRUCT_0:def 7
 the OneF of S;
coherence
the OneF of S is Element of S ;
end;

:: deftheorem defines 1. STRUCT_0:def 7 :
for S being OneStr holds 1. S = the OneF of S;

definition
let S be ZeroOneStr ;
attr S is degenerated means :Def8: :: STRUCT_0:def 8
 0. S = 1. S;
end;

:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :
for S being ZeroOneStr holds
( S is degenerated iff 0. S = 1. S );

definition
let IT be 1-sorted ;
attr IT is trivial means :Def9: :: STRUCT_0:def 9
 the carrier of IT is trivial ;
end;

:: deftheorem Def9 defines trivial STRUCT_0:def 9 :
for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );

registration
cluster empty -> trivial 1-sorted ;
coherence
for b1 being 1-sorted st b1 is empty holds
b1 is trivial
proof end;
cluster non trivial -> non empty 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty ;
end;

definition
let S be 1-sorted ;
redefine attr S is trivial means :Def10: :: STRUCT_0:def 10
 for x, y being Element of S holds x = y;
compatibility
( S is trivial iff for x, y being Element of S holds x = y )
proof end;
end;

:: deftheorem Def10 defines trivial STRUCT_0:def 10 :
for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y );

registration
cluster non degenerated -> non trivial ZeroOneStr ;
coherence
for b1 being ZeroOneStr st not b1 is degenerated holds
not b1 is trivial
proof end;
end;

registration
cluster non empty trivial 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is trivial & not b1 is empty )
proof end;
cluster non empty non trivial 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is trivial & not b1 is empty )
proof end;
end;

registration
let S be non trivial 1-sorted ;
cluster the carrier of S -> non trivial ;
coherence
not the carrier of S is trivial by Def9;
end;

registration
let S be trivial 1-sorted ;
cluster the carrier of S -> trivial ;
coherence
the carrier of S is trivial by Def9;
end;

begin

definition
let S be 1-sorted ;
attr S is finite means :Def11: :: STRUCT_0:def 11
 the carrier of S is finite ;
end;

:: deftheorem Def11 defines finite STRUCT_0:def 11 :
for S being 1-sorted holds
( S is finite iff the carrier of S is finite );

registration
cluster strict non empty finite 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is finite & not b1 is empty )
proof end;
end;

registration
let S be finite 1-sorted ;
cluster the carrier of S -> finite ;
coherence
the carrier of S is finite by Def11;
end;

registration
cluster empty -> empty finite 1-sorted ;
coherence
for b1 being empty 1-sorted holds b1 is finite
proof end;
end;

notation
let S be 1-sorted ;
antonym infinite S for finite ;
end;

registration
cluster strict infinite 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is finite )
proof end;
end;

registration
let S be infinite 1-sorted ;
cluster the carrier of S -> infinite ;
coherence
not the carrier of S is finite by Def11;
end;

registration
cluster infinite -> non empty infinite 1-sorted ;
coherence
for b1 being infinite 1-sorted holds not b1 is empty ;
end;

registration
cluster trivial -> finite 1-sorted ;
coherence
for b1 being 1-sorted st b1 is trivial holds
b1 is finite
proof end;
end;

registration
cluster infinite -> non trivial 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is finite holds
not b1 is trivial ;
end;

definition
let S be ZeroStr ;
let x be Element of S;
attr x is zero means :Def12: :: STRUCT_0:def 12
x = 0. S;
end;

:: deftheorem Def12 defines zero STRUCT_0:def 12 :
for S being ZeroStr
for x being Element of S holds
( x is zero iff x = 0. S );

registration
let S be ZeroStr ;
cluster 0. S -> zero ;
coherence
0. S is zero by Def12;
end;

registration
cluster strict non degenerated ZeroOneStr ;
existence
ex b1 being ZeroOneStr st
( b1 is strict & not b1 is degenerated )
proof end;
end;

registration
let S be non degenerated ZeroOneStr ;
cluster 1. S -> non zero ;
coherence
not 1. S is zero
proof end;
end;

definition
let S be 1-sorted ;
mode Cover of S is Cover of the carrier of S;
end;

registration
let S be 1-sorted ;
cluster [#] S -> non proper ;
coherence
not [#] S is proper
proof end;
end;

begin

definition
attr c1 is strict ;
struct 2-sorted -> 1-sorted ;
aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;
sel carrier' c1 -> set ;
end;

definition
let S be 2-sorted ;
attr S is void means :Def13: :: STRUCT_0:def 13
 the carrier' of S is empty ;
end;

:: deftheorem Def13 defines void STRUCT_0:def 13 :
for S being 2-sorted holds
( S is void iff the carrier' of S is empty );

registration
cluster empty strict void 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void )
proof end;
end;

registration
let S be void 2-sorted ;
cluster the carrier' of S -> empty ;
coherence
the carrier' of S is empty by Def13;
end;

registration
cluster non empty strict non void 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void )
proof end;
end;

registration
let S be non void 2-sorted ;
cluster the carrier' of S -> non empty ;
coherence
not the carrier' of S is empty by Def13;
end;

definition
let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;
func X --> y -> Function of X,Y equals :: STRUCT_0:def 14
 the carrier of X --> y;
coherence
the carrier of X --> y is Function of X,Y ;
end;

:: deftheorem defines --> STRUCT_0:def 14 :
for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;

registration
let S be ZeroStr ;
cluster zero Element of the carrier of S;
existence
ex b1 being Element of S st b1 is zero
proof end;
end;

registration
cluster strict non trivial ZeroStr ;
existence
ex b1 being ZeroStr st
( b1 is strict & not b1 is trivial )
proof end;
end;

registration
let S be non trivial ZeroStr ;
cluster non zero Element of the carrier of S;
existence
not for b1 being Element of S holds b1 is zero
proof end;
end;

definition
canceled;
let X be set ;
let S be ZeroStr ;
let R be Relation of X, the carrier of S;
attr R is non-zero means :: STRUCT_0:def 16
 not 0. S in rng R;
end;

:: deftheorem STRUCT_0:def 15 :
canceled;

:: deftheorem defines non-zero STRUCT_0:def 16 :
for X being set
for S being ZeroStr
for R being Relation of X, the carrier of S holds
( R is non-zero iff not 0. S in rng R );

definition
let S be 1-sorted ;
func card S -> Cardinal equals :: STRUCT_0:def 17
 card the carrier of S;
coherence
card the carrier of S is Cardinal ;
end;

:: deftheorem defines card STRUCT_0:def 17 :
for S being 1-sorted holds card S = card the carrier of S;

definition
let S be 1-sorted ;
mode UnOp of S is UnOp of the carrier of S;
mode BinOp of S is BinOp of the carrier of S;
end;

definition
let S be ZeroStr ;
func NonZero S -> Subset of S equals :: STRUCT_0:def 18
([#] S) \ {(0. S)};
coherence
([#] S) \ {(0. S)} is Subset of S ;
end;

:: deftheorem defines NonZero STRUCT_0:def 18 :
for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

theorem :: STRUCT_0:1
for S being non empty ZeroStr
for u being Element of S holds
( u in NonZero S iff not u is zero )
proof end;

definition
let V be non empty ZeroStr ;
redefine attr V is trivial means :Def19: :: STRUCT_0:def 19
 for u being Element of V holds u = 0. V;
compatibility
( V is trivial iff for u being Element of V holds u = 0. V )
proof end;
end;

:: deftheorem Def19 defines trivial STRUCT_0:def 19 :
for V being non empty ZeroStr holds
( V is trivial iff for u being Element of V holds u = 0. V );

registration
let V be non trivial ZeroStr ;
cluster NonZero V -> non empty ;
coherence
not NonZero V is empty
proof end;
end;

registration
let S be non empty 1-sorted ;
cluster non empty trivial Element of K21( the carrier of S);
existence
ex b1 being Subset of S st
( not b1 is empty & b1 is trivial )
proof end;
end;

theorem :: STRUCT_0:2
for F being non degenerated ZeroOneStr holds 1. F in NonZero F
proof end;