2010-04-29から1日間の記事一覧

Isabelle Tutorial その19

7. Inductively Defined Setsこの章では集合の帰納的定義を紹介します。 7.1 The Set of Even Numbers 偶数の集合は、定数0と演算子+2からなる最小の集合として帰納的に定義できます。もちろん、整除関係(dvd)を使用しても定義できます。それぞれの方法で定…