如何在Isabelle中引入forall

Question

我正在尝试从 a previous question 证明 Isabelle (2021) 中的以下推理规则：

特别是，我试图以正向方式证明这一点，首先使用两个假设得到 A(y) 和 B(y)，因此 A(y) /\ B(y)，对于任意选择的y。但是，我无法弄清楚在最后一步中引入 ∀ 的正确方法是什么，如下面的问题行所示。

theorem "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)"
proof (rule allI) ―‹forward›
  fix y
  assume "∀x. A(x)"
  from this have 1:"A(y)" by (rule allE)
  assume " ∀x. B(x)"
  from this have 2:"B(y)" by (rule allE)
  from 1 2 have "A(y) ∧ B(y)" by (rule conjI)
  ―‹problem line: applying allI›
  from this have "∀x. A(x) ∧ B(x)" by (rule allI)

有人可以帮忙解释什么是假设的正确方法然后抽象掉这里的任意变量y吗？

Answer 1

Can someone help explain what is the right way to assume and then abstract away the arbitrary variable y here?

我不会说只有一种“正确的方法”可以做到这一点。 “正确的方法”将取决于您要解决的问题的背景。

一般来说，你要证明的定理可以证明simp:

theorem 0: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
  by simp

在大多数情况下，当试图证明这样的结果时，simp 是最好的方法。

但是，例如，如果您正在编写说明文 article/tutorial 并希望展示如何执行证明的各个步骤，那么，当然，显式规则应用就成为必要。不过，这样的话，还是有很多可能的。

首先，您可以使用显式块，如下例所示：

(*naive variant*)
theorem 1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then have "∀y. A y ∧ B y" by (rule allI)
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

(*more natural variant*)
theorem 2: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

(*HOL-style*)
theorem 3: "(∀x. A x) ⟶ (∀x. B x) ⟶ (∀x. A x ∧ B x)"
proof(intro impI)
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

然而，proof- ... qed 通常是更好的选择，并且更符合 Isabelle 中传统的阐述风格，例如

theorem alt_1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  have "∀y. A y ∧ B y"
  proof(rule allI)
    fix y
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By show "A y ∧ B y" by (rule conjI)
  qed
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

作为一般参考，我建议 The Isabelle/Isar Reference Manual 中的第 2.2 节。

如何在Isabelle中引入forall

How to introduce forall in Isabelle

isabelle

hol