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

Or, the adjective form.

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 -> 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 | ○ | ○ |