用Isabelle证明谓词逻辑

Question

我想证明以下引理:

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"

我试图从消除forall量词开始，所以这是我尝试的:

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
apply(rule iffI)
apply ( erule_tac x="x" in allE)
apply (rule allE)
(*goal now: get rid of conj on both sides and the quantifiers on right*)
apply (erule conjE) (*isn't conjE supposed to be used with elim/erule?*)
apply (rule allI)
apply (assumption)


apply ( rule conjI) (*at this point, the following starts to make no sense... *)

apply (rule conjE) (*should be erule?*)
apply ( rule conjI)
apply ( rule conjI)
...

最后我只是根据之前的申请结果开始行动，但在我看来这是错误的，可能是因为一开始就有一些错误…有人能解释一下我的错误，以及如何正确地完成这个证明吗?

Thanks in advance

Answer 1

在这个早期阶段消除通用量词并不是一个好主意，因为你甚至没有任何值可以在那个时候插入(你给出的x在那个时候不在范围内，这就是为什么它在Isabelle/jEdit中打印为橙色背景)。

在你做了iffI之后，你有两个目标:

goal (2 subgoals):
1. ∀x. A x ∧ B x ⟹ (∀x. A x) ∧ (∀x. B x)
2. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

现在让我们关注第一个。首先应用右边的引入规则，即conjI和allI。剩下

goal (3 subgoals):
1. ⋀x. ∀x. A x ∧ B x ⟹ A x
2. ⋀x. ∀x. A x ∧ B x ⟹ B x
3. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

现在你可以应用x实例化的allE，第一个目标变成⋀x. A x ∧ B x ⟹ A x，然后你可以用erule conjE和assumption来解决。第二个目标的工作原理类似。

对于最后一个目标，也是类似的:首先应用引入规则，然后应用消除规则和assumption，这样就完成了。

当然，Isabelle的所有标准证明器，如auto、force、blast，甚至简单的证明器，如metis、meson、iprover，都可以很容易地自动解决这个问题，但这可能不是你想要的。