isabelle - How to prove an element does not belong to an inductive_set

Question

Assuming I have already defined an inductive_set, for example, the inductive set "Even" such that:

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

It's fairly easy to prove lemma : "2 ∈ Even" by doing a subst to replace 2 by 2-2+2

But I'm wondering how do prove lemma : "1 ? Even"?

Edit:

(*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

What would be the equivalent way to do it for 3?

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

Thanks in advance

question from:https://stackoverflow.com/questions/65854122/how-to-prove-an-element-does-not-belong-to-an-inductive-set

Answer 1

I would prove an intermediate result first, namely that each number in your inductive set is divisible by 2:

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

And then prove your result by contradiction:

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

I strongly recommend that you use Isabelle/Isar instead of proof scripts.

NOTE: As request by the post author, I'm adding a proof that 3 ? Even in the style of the above proof:

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

Alternative solution: @user9716869 provided the following more general and efficient solution based on the use of 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)