認識到子目標被證明

Question

我想了解Isar虛擬機的狀態機。

Page 48 of Markus Wenzel's doctoral thesis給出了一個很好的概述，但沒有在「輸出」面板中詳細說明它的消息。這可能是該系統的後續附錄。

我有一個簡單的伊薩爾證明：

theory Propositional 
imports Main 
begin 

lemma nj2: assumes p: P and q: Q shows "P ∧ (Q ∧ P)" 
proof - 
    from q p have qp: "Q ∧ P" by (rule conjI) 
    from p qp show "P ∧ (Q ∧ P)" by (rule conjI) 
qed 

第二by (rule conjI)輸出面板後說

show (P::bool) /\ (Q::bool) /\ P 
Successful attempt to solve goal by exported rule: 
    (P::bool) /\ (Q::bool) /\ P 
proof (state): depth 0 

this: 
    (P::bool) /\ (Q::bool) /\ P 

goal: 
No subgoals! 
variables: 
    P, Q :: bool 

所以它明確地認識到目標的解決方案。然而，在第一by (rule conjI)它說

have qp: (Q::bool) /\ (P::bool) 
proof (state): depth 0 

this: 
    (Q::bool) /\ (P::bool) 

goal (1 subgoal): 
1. P /\ Q /\ P 
variables: 
    P, Q :: bool 

我看不出有任何跡象表明次級目標已被證明。或者，have聲明與this註冊簿中的聲明相同的事實應該提醒我，它已被證明？

Answer 1

那麼，輸出面板中的子目標對應於上下文的子目標。在這種情況下，上下文是完整的引理之一，從proof -開始。在這種情況下，只有一個子目標，這是要證明的引理。

當你與have說出你的中間屬性，系統不會驗證相對於目標的任何東西，一旦它被證明，它只是給你訪問這個屬性（通過名稱this和qp），因爲你有證明了它與by (rule conjI)和沒有錯誤的事實意味着它被證明。

另一方面，當您使用show表示屬性時，系統會驗證您最終假設的屬性（使用assume）實際上是否與其中一個子目標相對應，否則將失敗。

當它到達的qed命令，它終於驗證上下文的所有子目標已被證明。

另一種方式來寫這個證明是這樣的（我沒有檢查它的工作，但它應該...）：

theory Propositional 
imports Main 
begin 

lemma nj2: assumes p: P and q: Q shows "P ∧ (Q ∧ P)" 
proof (rule conjI) 
    from p show P by assumption 
next 
    from q p show "Q ∧ P" by (rule conjI) 
qed 

在這種情況下，proof (rule conjI)創建2分目標P和Q ∧ P和輸出面板應該確認這一點。