如何证明一个元素不属于inductive_set

Question

假设我已经定义了一个 inductive_set，例如，归纳集“Even”使得：

inductive_set Even :: "int set" 
  where  ZERO : "0 ∈ Even"
          | PLUS :"x ∈ Even ⟹x+2 ∈ Even"
          | MIN :"x ∈ Even ⟹ x-2 ∈ Even"

lemma aux : "x= ((x::int)-2) + 2" by simp

通过用 2-2+2

代替 2 来证明 lemma : "2 ∈ Even" 相当容易

但是我想知道如何证明lemma : "1 ∉ Even"？

编辑：

(*Javier Diaz's answer*)
lemma Even_divisible_by_2: "n ∈ Even ⟹ 2 dvd n"
  by (induction rule: Even.induct) (simp, presburger+)
lemma "1 ∉ Even"
proof
  assume "1 ∈ Even"
  then have "2 dvd 1"
    using Even_divisible_by_2 by fastforce
  then show False
    using odd_one by blast 
qed

3 的等效方法是什么？

lemma "3 ∉ Even"
proof
  assume "3 ∈ Even"
  then have "2 dvd 3"
(*how to continue?*)
qed

提前致谢

Answer 1

我先证明一个中间结果，即你的归纳集中的每个数字都可以被 2 整除：

lemma Even_divisible_by_2: "n ∈ Even ⟹ 2 dvd n"
  by (induction rule: Even.induct) simp_all

然后用反证法证明你的结果：

lemma "1 ∉ Even"
proof
  assume "1 ∈ Even"
  then have "2 dvd 1"
    using Even_divisible_by_2 by fastforce
  then show False
    using odd_one by blast 
qed

我强烈建议您使用 Isabelle/Isar 而不是证明脚本。

注意：应 post 作者的要求，我将按照上述证明的样式添加 3 ∉ Even 的证明：

lemma "3 ∉ Even"
proof
  assume "3 ∈ Even"
  then have "2 dvd 3"
    using Even_divisible_by_2 by fastforce
  then show False
    using odd_numeral by blast
qed

替代解决方案：@user9716869 根据 Even_divisible_by_2 的使用提供了以下更通用和有效的解决方案：

lemma n2k1_not_Even: "odd n ⟹ n ∉ Even"
  using Even_divisible_by_2 by auto

lemma "1 ∉ Even" and "3 ∉ Even" and "11 ∉ Even"
  by (simp_all add: n2k1_not_Even)

如何证明一个元素不属于inductive_set

How to prove an element does not belong to an inductive_set

isabelle

induction