Isar 联合证明

Question

我正在尝试使用 Isar 来证明一些事情；到目前为止，我已经达到了一个看起来像这样的目标：

(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R)) 

（这里plmeets 是我定义的一个函数，其中plmeets P l 是仿射平面中“点P 位于l 线上”的简写，但我认为这对我的问题并不重要。 )

这个目标是三件事的结合。实际上，我已经证明了在我看来与这些事情非常接近的引理。例如，我有

lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"

产生输出

theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l

您可以看到几乎正是三个连体项目中的第一个。 （我承认我的其他引理与其他两项并不完全匹配，但我会努力解决的）。

我想说“由于引理four_points_a1，我们剩下要证明的就是item2 ∧ item3”，我很确定有办法做到这一点。但是看“编程和证明”这本书对我没有任何建议。在伊莎贝尔，而不是伊萨尔，我想我会应用conjI 两次将一个目标分成三个，然后解决第一个目标。

但我看不到如何在 Isar 中执行此操作。

Answer 1

根据@xanonec：

我想我会应用 conjI 两次将一个目标分成三个，然后解决第一个目标。

在 Isar 证明中可以做到这一点。但是，最好使用证明方法介绍而不是规则conjI 的多次应用，即您可以使用apply(intro conjI) 将目标分成3 个子目标。然后您可以使用subgoal 单独为每个子目标提供证明。但是，除非您提供整个应用程序，否则很难说是否存在更好的方法。

---

根据@John： 这个过程的实际工作语法是这样的：

  proposition four_points_sufficient: "affine_plane plmeets"
    unfolding affine_plane_def
    apply (intro conjI)
    subgoal using four_points_a1 by blast

我不清楚“在 Isar 证明中如何做到这一点 [即，应用 conjI 两次]”，但也许我现在不需要知道。