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

第4節 型の階層

目次


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

第2節 型の宣言や変換

第3節 変数の同等な型

第4節 型の階層


テスト

Logをみる

Back
 

第2章 証明の実行 第4節 型の階層

 前節のように見かけが異なるが同一な型があり、それぞれの型について実数に関する定理が分散していることがあります。他の型を宣言してしまうと、「*103: Unknown functor 関数が認識されない」というようなエラーが出るので初心者は気をつけてください。

 また型には階層があり得ます。

set

 という型は最も下位にある基本的な型です。すべての変数は無条件にこの型も併せもちます。

 また

 Nat ならば Real、Real なら Element of COMPLEX です。そしてset でもあります。

 Real なら Element of COMPLEX のところだけ証明が必要になっています。

 A c< B という記号は、A がB の真部分集合、という意味です。

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

begin

reserve x for Nat;

theorem x is Real;

theorem x is Element of COMPLEX
proof x is Element of REAL;then
  A2: x in REAL by SUBSET_1:def 2;then
  REAL c< COMPLEX by NUMBERS:1;then
  REAL c= COMPLEX by XBOOLE_0:def 8;then
  x in COMPLEX by A2,TARSKI:def 3;
 hence x is Element of COMPLEX by SUBSET_1:def 2;
end;

theorem x is set;

−−−