情報証明論 第2章 証明の実行

第3節 変数の同等な型

目次


第1節 もう少し証明らしい証明

第2節 型の宣言や変換

第3節 変数の同等な型

第4節 型の階層


テスト

Logをみる

Back
 

第2章 証明の実行 第3節 変数の同等な型

 型(typeまたはmode)についてもう少し説明しましょう。Mizar の用語では型のことをモード(mode といいます。

 例えば実数型を定義しているのは REAL_1 というファイルの中です。そこに、

−−−
definition
  mode Real is Element of REAL;
end;
−−−
としてReal という型が定義されています。しかし、Mizarライブラリーの中にはもうひとつ別の実数型があります。それは

 real number

というものです。それはXREAL_0 というファイルの中で、

−−−
registration
  cluster real number;
existence
 proof
   consider r being Element of REAL;
   take r;
   thus r in REAL;
 end;
end;
−−−

という風に導入されているのです。この場合はmodeでなく、clusterというもので定義(登録 registration)されています。

それはreal number というのが、real と number という2つの(すでに定義された)用語の複合語であるためで、このようなときの型の定義にはclusterを使います。

 型が導入されれば、変数に対し、

−−−
reserve x for Real;
reserve y for real number;
−−−

 のように型をあらかじめ宣言することができます。

 実は見かけが異なってもこれらの型(Realとreal number)は同等なのです。

 同等、という意味は、x がReal型ならば、x is real numberという命題が証明されますし、その逆も言えるということです。次にそれを示します。ここでは適当な環境部をつけました。環境部によっては1番目の定理はわざわざ証明しなくても自明であることもあります。

−−−
environ
 vocabulary ORDINAL2,ARYTM,SUBSET_1,BOOLE,ASYMPT_0;
 notation ORDINAL2,NAT_1,ORDINAL1,NUMBERS,SUBSET_1,XBOOLE_0,XREAL_0,REAL_1;
 constructors ORDINAL2,NUMBERS,NAT_1,XREAL_0;
 clusters ORDINAL2,ARYTM_3,XREAL_0,NUMBERS;
 theorems ORDINAL2,SUBSET_1,XREAL_0;

begin
reserve x for Real;
reserve y for real number;

theorem x is real number
proof
  x in REAL by SUBSET_1:def 2;
 hence thesis by XREAL_0:def 1;
end;
theorem y is Real
proof
  y in REAL by XREAL_0:def 1;
 hence thesis by SUBSET_1:def 2;
end;
−−−

 同様に自然数を表すNat とnatural number も同等です。それを示す定理を次に挙げます。

−−−
environ
 vocabulary ORDINAL2,ARYTM,SUBSET_1;
 notation ORDINAL2,NAT_1,ORDINAL1,NUMBERS,SUBSET_1;
 constructors ORDINAL2,NUMBERS;
 clusters ORDINAL2,ARYTM_3;
 theorems ORDINAL2,SUBSET_1;

begin
reserve x for Nat;
theorem x is natural number;
reserve y for natural number;
theorem y is Nat
 proof
   y in NAT by ORDINAL2:def 21;
  hence y is Nat by SUBSET_1:def 2;
 end;
−−−

 ついでに複素数の型 Element of COMPLEX と complex number も同等です。

−−−
environ
 vocabulary ARYTM,XCMPLX_0,COMPLEX1;
 notation NAT_1,ORDINAL1,NUMBERS,SUBSET_1,XBOOLE_0,XREAL_0,REAL_1,COMPLEX1,
   XCMPLX_0;
 constructors ORDINAL2,NUMBERS,XREAL_0,NAT_1;
 clusters ORDINAL2,ARYTM_3,XREAL_0,NUMBERS;
 theorems SUBSET_1,XCMPLX_0;

begin
reserve z for Element of COMPLEX;
reserve u for complex number;
theorem z is complex number
proof
  z in COMPLEX by SUBSET_1:def 2;
 hence thesis by XCMPLX_0:def 2;
end;
theorem u is Element of COMPLEX
proof u in COMPLEX by XCMPLX_0:def 2;
 hence u is Element of COMPLEX by SUBSET_1:def 2;
end;
−−−