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

第2節 型の宣言や変換

目次


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

第2節 型の宣言や変換

第3節 変数の同等な型

第4節 型の階層


テスト

Logをみる

Back
 

第2章 証明の実行 第2節 型の宣言や変換

 よく考えてみますと、乗算に関する定義が2つのファイルに別々にあることに気づきます。XCMPLX_0:def 5 と COMPLEX1:def 10 です。XCMPLX_0:def 5 はcomplex numberに対するものですが、COMPLEX1:def 10 は Element of COMPLEX に対するものです。x^2の定義は前者を使い、x^3は後者を使っているのです。

 そこで次のように証明をあらためます。

−−−
reserve x for Element of COMPLEX;

theorem x^3=x*x*x
 proof 
   reconsider a=x as complex number by XCMPLX_0:def 2;
   A1: x^2=a*a by SQUARE_1:def 3;
  thus x^3=x^2*x by POLYEQ_3:def 4 
         .=x*x*x by A1;
 end;
−−−

x は最初、

reserve x for Element of COMPLEX

によって、Element of COMPLEX という型だと宣言します。そして証明中で

reconsider a=x as complex number by XCMPLX_0:def 2;

という文によってxをaというcomplex numberという型の変数に変換します。これは

XCMPLX_0:def 2 によって正当化されます。

 実はa*a=x*x は、COMPLEX1:def 10 がXCMPLX_0:def 5 の再定義(redefine)である(http://mizar.org/JFM/mmlident.html のabsファイルのWebページでCOMPLEX1を表示させ、def 10 の*印をクリックしてみればこのことが分かります)ことから、自動的にいえるのです。

全体を見ますと、以下のようになります。

−−−
environ
  vocabulary ARYTM, ARYTM_3, RELAT_1, ARYTM_1, ABSVALUE, SQUARE_1, XCMPLX_0,
     COMPLEX1,POLYEQ_3;
  notation TARSKI, SUBSET_1, ORDINAL1,NUMBERS,XCMPLX_0,XREAL_0,ABSVALUE,
     SQUARE_1,POLYEQ_3,COMPLEX1;
  constructors REAL_1, ABSVALUE, XCMPLX_0, XREAL_0, XBOOLE_0,SQUARE_1,POLYEQ_3,
     COMPLEX1;
   clusters XREAL_0, REAL_1, NUMBERS, ARYTM_3, ZFMISC_1, XBOOLE_0,XCMPLX_0;
  requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
  definitions TARSKI, REAL_1, XREAL_0;
  theorems AXIOMS, REAL_1, ABSVALUE, XREAL_0, XCMPLX_0, XCMPLX_1,POLYEQ_3,
        SQUARE_1;

begin
reserve x for Element of COMPLEX;

theorem x^3=x*x*x
 proof 
   reconsider a=x as complex number by XCMPLX_0:def 2;
   A1: x^2=a*a by SQUARE_1:def 3;
  thus x^3=x^2*x by POLYEQ_3:def 4 
         .=x*x*x by A1;
 end;

−−−