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”，我很确定有办法做到这一点。但是看着“编程和证明”这本书并没有给我任何启示。在Isabelle，而不是Isar，我想我会应用conjI两次，将一个目标分成三个，然后解决第一个目标。

但我看不到如何在Isar中做到这一点。

Answer 1

根据@xanonec：

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

可以在Isar证明中做到这一点。然而，最好使用证明方法intro，而不是规则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”，但也许我现在不需要知道。