2010-05-06から1日間の記事一覧

Isabelle Tutorial その20

7.2 The Reflexive Transitive Closure 帰納的定義はパラメータを取り、集合を作るための関数とすることができます。また関係はペアの集合であることから、これも帰納的に定義できます。例として関係から反射推移閉包への写像関数を考えます。 inductive_set…