6.5 mode の定義

最後に mode の定義について説明をします．

いま，あらたに nlt2_elements という mode を定義するとします．



   definition



    mode nlt2_elements -> set means



    :DF2:



    ex a,b st a ∈ it & b ∈ it & a <> b;



     existence



     proof



      take B = NAT



      thus ex a,b st a ∈ B & b ∈ B & a <> b 



       proof



        take a = 1, b = 2;



        thus a ∈ B & b ∈ B & a <> b;



       end;



     end;



    end;

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



   definition



   attr nlt2_elements -> set means :DF2:



   ex a,b st a ∈ it & b ∈ it & a<>b;



   end;



   definition



   cluster nlt2_elements set;



   existence



   proof



     take B=NAT;



     ex a,b st a ∈ B & b ∈ B & a<>b



     proof



      take a=1 , b=2;



      thus a ∈ B & b ∈ B & a<>b;



     end;



    hence thesis by DF2;



    end;



   end;

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





           A is non_empty

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



           non-empty set

この場合，non-empty は，non empty と同様です．

また，attribute の definition ブロックの中で，それと同じ意味を持つシンボル（synonym）と反対の意味を持つシンボル（antonym）を定義する事ができます．



     definition
                         


       attr empty -> set means :A1:
     


         not ex x st x ∈ it;
 


         ...
                            


       synonym (symbol);
                


       antonym (symbol);



     end;

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



     finite infinite set



     empty non-empty set

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

Existence Uniqueness
Mode ○
Pred
Functor ○ ○
Attr