认识到子目标被证明

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和输出面板应该确认这一点。