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

问题描述

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

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

提前致谢

解决方法

我将首先证明一个中间结果，即归纳集中的每个数字都可以被 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 而不是证明脚本。

注意：根据博文作者的要求，我将按照上述证明的风格添加 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)