如何使用 Isar 中的基本命题规则来证明 `A ⟶ A ∨ B`？

Question

我想仅使用命题逻辑中的基本自然演绎规则 (ND)（例如 notI、notE、impI、impE...等）。

我可以在应用脚本中轻松完成：

lemma very_simple0: "A ⟶ A ∨ B"
  apply (rule impI) (* A ⟹ A ∨ B *)
  thm disjI1 (* ?P ⟹ ?P ∨ ?Q *)
  apply (rule disjI1) (* A ⟹ A *)
  by assumption

但我对 Isar 证明的尝试失败了：

lemma very_simple1: "A ⟶ A ∨ B"
proof (* TODO why/how does this introduce A by itself*)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

我的主要错误是：

Undefined method: "disjI1"⌂

这对我来说似乎很神秘，因为规则在之前的应用脚本中运行得很好。

我做错了什么？

注意这也会导致错误：

lemma very_simple2: "A ⟶ A ∨ B"
proof impI
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

同上错误：

Undefined method: "impI"⌂

为什么？

编辑：

我了解到 'method' 仍然需要工作 rule impI 或 metis etc 但脚本仍然失败：

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by (rule disjI1)
  show "A ⟹ A" by assumption
qed

编辑2：

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  have 0: "A ⟹ A ∨ B" by (rule disjI1)
  have 1: "A ⟹ A" by assumption
  from 1 show "True" by assumption
qed

我还是无法完成证明。

Answer 1

你有几个问题。

让我们考虑这个例子：

have "A ⟹ A" by (rule disjI1)

失败了，那么首先定理 disjI1 实际上是什么？

thm disjI1
(* ?P ⟹ ?P ∨ ?Q *)

由于规则的运作方式，它尝试将目标 "A" 与“?P ∨ ?Q”相匹配，但失败了。现在，如果您的目标形式正确：

have "A ⟹ A ∨ B" by (rule disjI1)

有效！

第二题：

 proof

默认等价于 "proof standard" 并且默认应用一些定理。通常，您将使用 "proof -" 来应用任何定理。

最后，让我们考虑一下你的例子

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)

在状态视图中，您看到：

proof (state)
goal (1 subgoal):
 1. A ⟹ A ∨ B

这意味着 Isar 必须看起来像

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  show ‹A ∨ B›
    sorry
qed

显示有效的事实表明证明块具有正确的形式。

注意：这是重要的一步，尤其是在开始的时候。总是从假设和表演开始。不要做任何其他事情。如果显示不起作用，则由 Isar 证明（假设和显示）导出的结构与预期证明不匹配（可以在状态面板中看到）。

你可以从那里做任何你想做的事（包括开始一个新的证明块），但是你不能在不改变应用的规则的情况下改变那个结构。

让我们完成证明。我们要用假设（所以加了一个then）和规则来证明目标

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  then show ‹A ∨ B›
    by (rule disjI1)
qed

总的来说，我认为您应该阅读 Concrete Semantics 的 Isar 部分。

编辑：最重要的问题是你误解了 Isar 是什么：Isar 不是来帮助你完成不同的证明步骤的（比如证明 "A ==> A"）。它在这里做一个前向证明：你从假设（这里是A）开始，然后得出结论。所以 Isar 证明看起来像

  assume A
  show "A \/ B"

您永远不必在证明中重复假设 A！

如何使用 Isar 中的基本命题规则来证明 `A ⟶ A ∨ B`？

How does one use basic propositional rules in Isar to prove `A ⟶ A ∨ B`?

isabelle

isar