How do I prove that 4 is even using Isabelle

0
votes

Assuming that I have this inductive definition for Even

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

How do I prove this lemma lemma four_is_even: "4 ∈ Even" ?

I am relatively new to proof assistant.

isabelle