认识到子目标已被证明

Question

想了解Isar虚拟机的状态机

Page 48 of Markus Wenzel's doctoral thesis 提供了一个很好的概述，但没有在输出面板中详细说明其消息。它很可能是系统的后续附录。

我有一个简单的 Isar 证明：

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

认识到子目标已被证明

Recognising that a subgoal is proved

isabelle