2

在 Isar 中，人们使用assume目标的前提，以便她可以使用它来构建结论。

伊莎贝尔/伊萨尔参考 说

assume expects to be able to unify with existing premises in the goal

这是 的唯一用途assume，即从目标的前提中获取事实吗？

更新：由于有些人认为这太宽泛了，我不明白，我试图重新提出这个问题。

该手册描述了assume. 但它的用途是什么？这是否仅限于我从目标的前提中获得事实的情况？

4

1 回答 1

1

我看到了assume关键字的两种用法，它们当然是同一过程的两个实例：说明要证明的属性的前提。

如果我们举一个愚蠢的例子：

lemma "∀A B C D. A ⟶ B ⟶ C ⟶ D ⟶ (A ∧ B) ∧ (C ∧ D)"
using assms
proof (intro allI impI)
  fix A B C D
  assume A B
  then have "A ∧ B" .. (* or "by rule", "by default", "by simp", ... *)

  { fix E F
    assume E and F
    then have "E ∧ F" ..
  } note H = this

  assume C D then have "C ∧ D" ..
  from H[OF `A ∧ B` `C ∧ D`] show "(A ∧ B) ∧ (C ∧ D)" . (* or "by fact" *)
qed

  • 要么assume似乎陈述了proof命令 生成的前提proof和show或之间的任何地方thus。这些假定的属性必须是proof命令生成的前提的子集（此处A B C和D）。

  • 或assume出现在由 分隔的块{中}，您可以在其中假设任何您想要的东西，然后证明用 .P声明的属性have。当块关闭时，会产生一个局部事实，该事实由作为前提的假设和P作为结论的属性组成。在示例中，我将其命名H并用它来证明最后一个连词。

于 2014-07-17T23:32:35.510 回答