イザベルで理論をインポートすることはできませんか？

Question

私は自分のリストタイプをListという名前の理論で定義したいと思っていますが、すでにその名前の理論があります。 Mainよりも軽量な理論がありますか？

Answer 1

Isabelleには何もインポートできません（インポートは基本ロジックでも必要です）。 IsabelleのHOLの実装には、Main,Complex_Main（これにはMainといくつかの分析を加えたもの）とPlainという3つのエントリポイントがサポートされていますが、最初の2つのみが通常の使用を意図しています。

プレーンには基本ロジックが既に含まれていますが、標準ライブラリ（例：リストなし）ではほとんどありません。しかし、QuickCheck、Sledgehammer、コードジェネレータなどの重要なツールもありません。さらに、Plainから自分の理論リストに名前を付けることができるようになると、あなたの理論はMain（ほとんどすべてである）上のどの建物とも互換性がないことに注意してください。

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

Answer 2

あなたは私が頻繁にテストやイザベルについての調査のためにそれを行う

theory Test_Theory 
imports HOL 
begin 
    … 
end 

にとして、HOLのみインポートすることがあります。

ただし、データ型の定義を欠いて、おそらくDatatypeをインポートする必要があります（とさえRecordかもしれない）あなたのList理論を書くことができるようにするために、同様。両方DatatypeとRecord輸入HOLとして

theory Test_Theory 
imports HOL Datatype Record 
begin 
    … 
end 

は、単に持っていることがあります。

理論 Mainなしに行うことは簡単ですが、不可能ではないではありません

theory Test_Theory 
imports Datatype Record 
begin 
    … 
end 

。ちょうどあなたが広く使われている定理なしでやらなければならないことに気づいて、あなた自身のことを書いて証明しなければならないかもしれません。

Answer 3

$ISABELLE_HOME/src/HOL/ex/Seq.thyは、Mainエントリポイントの下でシステムを操作する方法を微妙に質問することなく、実験用に独自のリストデータ型を定義する最小の例を示しています。

理論的には、あなたがインポートできる最も基本的な理論はPureですが、それはまだ素人の論理フレームワークであり、HOLのようなオブジェクトロジックはまだありません。好奇心のために、Pureから始まる$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thyを見て、最小のバージョンのH.O.Lを定義します。あなたが完全なIsabelle/HOLから期待する先進的な理論やツールがなくても、それに加えて、