Isabelle Tutorial その5 - caeruiro
2.6 Some Basic Types 2.6.1 Natural Numbers 自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。 case n of 0 => 0 | Suc m => m 原始再帰関数の定義と、帰納法による証明の例も示します。 primrec sum :: "nat => nat" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done +, -, *, div, mod, min, max, <=, <などが定義されています。最小値演算LEASTも定義されています。例えば(LEAST n. 0 < n) = Suc 0です。 定数0や1
Isabelle Tutorial その3 - caeruiro
2. Functional Programming in HOL ここからはHOLでどのように関数プログラムを書き、どのように検証するのか見ていきます。Isabelle/HOLを使う目的はシステムをモデル化し検証することなので、関数を実行可能なかたちで定義する必要はないのですが、まずは実行可能な定義を書くことにします。ただし、HOLでは必ず全域的でなければならないことに注意してください。 2.1 An Introductory Theory MLやHaskellと同じようにデータ型と関数を定義することができます。簡単なリストを定義しながら、方法を一つ一つ見ていきます。 theory ToyList imports Datatype begin HOLには既にリストが定義されています。多くの場合Mainをインポートしますが、定義済みのリストもインポートしてしまうため、ここではDatatype
Isabelle Tutorial その1 - caeruiro
1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。 theory T imports B1, ..., Bn begin 宣言、定義、証明などなど end B1, ..., Bnは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。 既存の理論ファイルは次のページで探すことができますし、Isabelleをインストー
Isabelle
What is Isabelle? Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle ov
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ProofSummit2011(仮題) - [PARTAKE]
