目次

第２節　型の宣言や変換

第３節　変数の同等な型

第４節　型の階層

テスト

Logをみる

Back
　

　前節のように見かけが異なるが同一な型があり、それぞれの型について実数に関する定理が分散していることがあります。他の型を宣言してしまうと、「*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;

−−−