How do I prove that 4 is even using Isabelle

Question

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.

Answer 1

As @Mathias Fleury informally explained above, there are several ways in which you can prove your lemma:

Using forward-style reasoning

You can first prove the following auxiliary lemma using the OF fact combinator:

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

and then let the simplifier take care of proving 0+2+2 = 4:

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

Also, you can use the Isabelle/Isar proof language to produce a more structured and pedagogical proof:

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

Using backward-style reasoning

Similarly to the first example of the forward-style reasoning above, you can prove the following auxiliary lemma using 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

and then again let the simplifier take care of proving 0+2+2 = 4:

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

Of course, trying to prove your lemma using Even.min is much more involved.