2013-12-12 66 views
2

之間的轉換有兩種樣式伊莎貝爾證明:舊的「適用」的風格,證明僅僅是一個伊莎貝爾:「結構化」和「應用式」證據

apply (this method) 
apply (that method) 

陳述鏈,和新的「結構化」伊薩爾風格。我自己,我覺得有用; 「應用」風格更加簡潔,因此適用於無趣的技術語法,而「結構化」風格則適用於主要定理。

有時我喜歡從一種風格切換到另一種風格,中等防護。從「應用」風格切換到「結構化」風格很簡單:我只需在我的應用鏈中插入

proof - 

。我的問題是:我怎樣才能從「結構化」風格切換回「適用」風格?

舉一個更具體的例子:假設我有五個子目標。我發佈了一些「適用」指令來發送前兩個子目標。然後,我發起了一個結構化的證明,取消第三個。我還有兩個子目標:我如何返回到「應用」風格?

回答

3

通過使用apply_end而不是apply,您可以繼續使用結構化證明中的「應用」風格,但這在實踐中並且僅在探索性工作中很少見到。在拋光證明中,您只需挑選符合Isar證明的子目標,並在qed之後用一個方法調用完成所有剩餘子目標,因爲不需要按任何特定順序處理子目標。

或者,你可以使用deferproof啓動結構化的證明,並在「應用」的風格,即其它子目標立即繼續之前,推遲與結構化的證據,直到最後的目標。

最後,您當然可以在fix/assume/show的結構化證明中重新表達您的目標,並繼續在那裏應用風格。但是你必須分別爲每個剩餘的子目標執行此操作,所以這可能有點乏味。默認案例名稱goal1,goal2等在打字時會有所幫助,但這種證明通常難以維護(尤其是apply_end更改了目標編號goal<n>)。