證明A ==>乙==>ç==>乙在伊莎貝爾

Question

我困惑有關伊莎貝爾證明

A ==> B ==> C ==> B 

。顯然你可以

apply simp 

但我怎麼能證明這與使用規則？

或者，有沒有辦法轉儲使用的規則simp？謝謝。

Answer 1

如果您真的想了解證據是如何工作的，那麼您應該忘記關於有趣的策略和自動推理工具。

聲明A ==> B ==> C ==> B（使用這一特殊==>結締組織）伊莎貝爾的/純立即真實的，所以其在伊莎貝爾證明/ ISAR是：

lemma "A ==> B ==> C ==> B" . 

就是這樣，只是.（其簡寫爲by this，但this這裏實際上是空的）。

由於少許空洞的證據使用實際的Isabelle/HOL連接詞，您可以通過標準的引入或刪除步驟來處理。例如。像這樣：

lemma "A --> B --> C --> B" 
proof 
    show "B --> C --> B" 
    proof 
    assume b: B 
    show "C --> B" 
    proof 
     show B by (rule b) 
    qed 
    qed 
qed 

但事實並非如此有趣或者：你建立了一個沉悶的暗示，其隨後分解，直至完成。

要找到更有趣的伊莎貝爾/伊薩爾證據只是做一些網絡搜索，或通過系統隨附的來源。 完全是任意的例子在這裏：Drinker。

也有很多的手冊，其中有太多的手冊。

Answer 2

您可以啓用簡化器跟蹤;在Proof General中，你可以通過Isabelle→Settings→Tracing→Trace Simplifier來做到這一點，我不知道jEdit。

編輯：在這種情況下，簡單跟蹤將不會很有幫助，因爲simp不使用重寫規則來解決這個問題，而是它在場所中「看到」A，B和C，並得出結論：在本聲明的上下文中，重寫了A = True,B = True和C = True，然後它將目標B重寫爲True，就完成了。

但是，證明此類語句的「正常」方法是使用assumption方法，該方法與目標與前提匹配，在此情況下爲B。可能還有一種方法可以使用rule來證明這一點，但這樣做會不必要的複雜。 assumption使用assume_tac，這反過來只是非常基本的函數Thm.assumption的包裝，所以這實際上可以被認爲是Isabelle中最基本的證明方法之一。 所以只寫by assumption。