6.6 Mode Definition

At last, we will explain the mode definition.
Let us assume that we will newly define a mode nlt2_elements.

definition
mode nlt2_elements　->　set means
:DF2:
ex a,b st a in it & b in it & a <> b;
existence
proof
take B = NAT;
thus ex a,b st a in B & b in B & a <> b
proof
take a= 1, b = 2;
thus a in B & b in B & a <> b;
end;
end;
end;

In the demonstration section of the mode definition, only the demonstration of existence will be needed. Also, when the mode is defined, its natural property can be defined by (attribute) or (cluster). For instance:

definition
attr nlt2_elements -> set means :DF2:
ex a,b st a in it & b in it & a <> b;
end;
definition
cluster nlt2_elements set;
existence
proof
take B=NAT;
ex a,b st a in B & b in B & a <> b
proof
take a=1, b=2;
thus a in B & b in B & a <> b;
end;
hence thesis by DF2;
end;
end;

Generally, attribute takes the following predicate form:

A is non-empty

non-empty set

In this case, non-empty is the same with non empty.
Also, in the definition blocks of attribute, we can define symbols that possess the same meaning (synonym) and the opposite meaning(antonym).

Example (this is not actual)

definition
attr empty -&gt　set means :A1:
not ex x st x∈it;
...
synonym (void);
antonym (non-empty);
end;

When we want to use by attaching multiple attributes to one mode, that cluster needs to be defined. If this is not done, the following inconsistent combination will appear.

finite infinite set
empty non-empty set

As it has been stated before, new functor, mode, attribute, cluster (cf. §6.7), and others can be defined in Mizar; however, each demonstration needs to include the following elements.

 Existence Uniqueness Mode ○ Pred Functor ○ ○ Attr Cluster ○ ○