Isabelle中可以不導入任何理論嗎？

我想在一個名爲List的理論中定義我自己的列表類型，但已經有一個名稱爲理論。有沒有比Main更輕量級的理論？Isabelle中可以不導入任何理論嗎？

2012-07-05 user1494846

僅供參考，如果您沒有得到您要查找的答案，可能值得它在cs.stackexchange.com或cstheory.stackexchange.com上提問... – reuben

@reuben：都不是網站有工具支持。 Isabelle的[文檔]（http://isabelle.in.tum.de/documentation.html）和[community]（https://isabelle.in.tum.de/community）是正確的地方。 – Raphael

關閉窗口的注意事項：這個問題是關於Stack Overflow的正題。 Isabelle是一個定理證明者，它們是一種特殊的編程環境（[tag：coq]和[tag：agda]是其他例子，它們在SO上有一個小的但是現有的社區）。使用編程工具是關於堆棧溢出的主題。（@Raphael不，這裏的問題很好。） – Gilles

不能在Isabelle中導入任何內容（即使對於基本邏輯，導入也是必需的）。在Isabelle中實施HOL有三個支持的入口點：Main,Complex_Main（它是Main加上一些分析）和Plain，但只有前兩個用於常規用法。

Plain已包含基本邏輯，但在標準庫（如無列表）方面幾乎沒有任何內容。但是重要的工具，如QuickCheck，Sledgehammer和代碼生成器也不見了。此外，如果您從Plain開始，能夠列出您自己的理論列表，請注意您的理論與Main上的任何工作建築（幾乎所有內容）都不兼容。

所以，除非你真的有很好的理由這樣做，否則我會建議遵循Raphael的評論，給你的列表理論另一個名字。

來源

2012-12-06 23:44:04

你可能只進口HOL，如

theory Test_Theory 
imports HOL 
begin 
    … 
end

我經常這樣做的測試和調查有關伊莎貝爾。

但是，您將缺少數據類型定義，並且可能需要導入Datatype（甚至可能是Record），以便能夠編寫您的List理論。

theory Test_Theory 
imports HOL Datatype Record 
begin 
    … 
end

由於兩個Datatype和Record進口HOL，你可能只是：

theory Test_Theory 
imports Datatype Record 
begin 
    … 
end

這並不容易沒有理論Main做，但並非不可能。請注意，你將不得不做許多廣泛使用的定理，並且可能必須寫出並證明你的擁有者。

來源

2013-02-23 06:12:35 Hibou57

我不知道'FunDef'，謝謝你的提示，會看看它。我的確對此感興趣的是「不那麼臃腫」的基礎理論，至少因爲它消耗了大量的內存（我正在運行一個1G內存的機器，這對於Isabelle來說很小......我打算獲得更多內存，特別是伊莎貝爾）。此外，另一個尋找另一個理論集合的理由比'Main'提供的理論更有一些理論不適合某種證明。作爲一個例子，我覺得集合論使用的公理化並不方便，並且希望建立我自己的（如果可能的話）。 – Hibou57

請注意，在Main'HOL下面導入任何內容都是未指定的，並且會出現奇怪的效果。 1 GB RAM是進入Isabelle/HOL引導內部的一個不好的理由。 – Makarius

與「Pure」不一樣嗎？（我會看，謝謝你的觀點）。 – Hibou57

請注意，$ISABELLE_HOME/src/HOL/ex/Seq.thy給出了一個爲實驗定義自己的列表數據類型的簡單示例，而沒有着手於如何在低於Main入口點的系統上使用這個微妙的問題。（初學者感到困惑，專家不這樣做）。

從理論上講，你可以導入的最原始的理論是Pure，但這只是一個基本的邏輯框架，沒有像HOL這樣的任何對象邏輯。只是爲了好奇，你可以看看$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy，它從Pure開始，並定義了H.O.L的最小版本。除此之外，沒有你期望從Isabelle/HOL那裏獲得的任何先進的理論和工具。

來源

2013-02-28 21:21:37 Makarius

對'Higher_Order_Logic'的引用非常好。 –

Isabelle中可以不導入任何理論嗎？

回答

相關問題