isabelle - イザベルに理論をインポートしないことは可能ですか?

Question

という名前の理論で独自のリスト型を定義したいのですがList、その名前の理論は既に存在します。より軽量な理論はありMainますか？

Answer 1

実験用に独自のリスト データ型を定義する最小限の例を示していることに注意してください。システムのエントリ ポイント$ISABELLE_HOME/src/HOL/ex/Seq.thy以下でどのように動作するかというデリケートな問題に着手することはありません。Main（初心者は混乱し、専門家はそれをしません。）

理論的には、インポートできる最も原始的な理論は ですが、これは必要Pure最小限の論理フレームワークであり、HOL のようなオブジェクト ロジックはまだありません。好奇心のために、完全な Isabelle/HOL に期待される高度な理論やツールを使用せずに、HOL の最小バージョン$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thyから始まり、その上に定義されているものを見ることができます。Pure

Answer 2

イザベルでは何もインポートできません (基本的なロジックでもインポートが必要なため)。Isabelle での HOL の実装には、3 つのエントリ ポイントがサポートされていMainます。Complex_MainMainPlain

Plain にはすでに基本的なロジックが含まれていますが、標準ライブラリに関してはほとんど何も含まれていません (たとえば、リストはありません)。しかし、QuickCheck、Sledgehammer、コード ジェネレーターなどの重要なツールも欠落しています。さらに、自分の理論リストに名前を付けることができるように Plain から始める場合、その理論は Main (ほとんどすべて) で構築されている作業と互換性がないことに注意してください。

したがって、そうする正当な理由がない限り、Raphael のコメントに従って、リスト理論に別の名前を付けることをお勧めします。