6.6　modeの定義

　最後に mode の定義について説明をします．
　いま，あらたに nlt2_elements という mode を定義するとします．

　　　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;

　mode 定義の証明部では，existence についてのみ証明が必要となります．また mode が定義されると，その性質を (attribute) や (cluster) で定義する事ができます．例えば，

　　　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;

　一般には，attribute は次のような述語の形か,

　　　A is non-empty

形容詞の形で定義します．

　　　non-empty set

この場合，non-empty は，no nempty と同様です．
　また，attribute の definition ブロックの中で,それと同じ意味を持つ シンボル (synonym) と反対の意味を持つシンボル (antonym) を定義する事ができます．例 (これは実際のものではない):

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

　一つの mode に複数の attribute をつなげて使いたい時，その cluster を定義する必要があります．その場合，存在の証明が必要です．そうしなければ，次のような矛盾するコンビネーションが現れます．

　　　finite infinite set
　　　empty non-empty set

　このように，Mizar では新しい functor，mode，attribute，cluster (§6.7参照) などの定義が出来ますが，それぞれの証明は以下の要素を含む必要があります．