6.3 predicate の定義


まず,predicate の定義について説明します.例えば,k,lを自然数として,いま,kはlの因子である,という定義をしたいとします.これは predicate です.k is factor of l ,このような定義をしたいとします.これは二項演算子の様な形をしてますけれども,k ,l と2つ変数を持っているわけです.この場合どうやって定義を書くかというと,


definition

let k,l be Nat;

pred k is_factor_of l

means

:FACTOR:

ex t being Nat st l=k ・ t;

となります.let k,l be Nat の Nat は,k,l の Mode が自然数であることをあらわしています.:FACTOR: はラベルで,後で引用するときにこのラベルを使います.定義のなかのラベルは両側をコロンではさみます.そして,これは abstract file をここから抜きだして作るときには,def に数字がついたものに変えられます.ふつうの定理のラベルは単なる数字に変えられます.また,k ・ t の ・ はかけ算です.

これで,k is_factor_of l という predicate とは ex t being Nat st l=k ・ t ということを意味しています.