我如何证明 4 甚至在使用 Isabelle

Question

假设我对 Even 有这个归纳定义

inductive_set Even :: "Int.int set"
  where null: "0 ∈ Even"
  | plus: "x ∈ Even ⟹ x+2 ∈ Even" 
  | min: "x ∈ Even ⟹ x-2 ∈ Even"

如何证明这个引理 lemma four_is_even: "4 ∈ Even" ?

我对证明助手比较陌生

Answer 1

正如@Mathias Fleury 上面非正式解释的那样，有几种方法可以证明你的引理：

使用正向推理

您可以先使用 OF 事实组合子证明以下辅助引理：

lemma four_is_even_fwd': "0+2+2 ∈ Even"
  by (fact plus [OF plus [OF null]])

然后让简化器负责证明 0+2+2 = 4:

lemma four_is_even_fwd: "4 ∈ Even"
  using four_is_even_fwd' by simp

此外，您可以使用 Isabelle/Isar 证明语言来生成更加结构化和教学的证明：

lemma four_is_even_fwd_str: "4 ∈ Even"
proof -
  have "0 ∈ Even"
    by (fact null)
  then have "0+2 ∈ Even"
    by (fact plus)
  then have "0+2+2 ∈ Even"
    by (fact plus)
  then show ?thesis
    by simp
qed

使用反向推理

类似于上面第一个正向推理的例子，你可以使用apply-scripts证明下面的辅助引理：

lemma four_is_even_bwd': "0+2+2 ∈ Even"
  apply (rule plus) (* subgoal: 0+2 ∈ Even *)
  apply (rule plus) (* subgoal: 0 ∈ Even *)
  apply (rule null) (* no subgoals! *)
  done

然后再次让简化器负责证明 0+2+2 = 4:

lemma four_is_even_bwd: "4 ∈ Even"
  using four_is_even_bwd' by simp

当然，尝试使用 Even.min 来证明你的引理要复杂得多。

我如何证明 4 甚至在使用 Isabelle

How do I prove that 4 is even using Isabelle

isabelle