Isabelle/HOL proof by rule inversion

Question

I'm starting out with Isabelle/HOL and working through the prog-prove.pdf tutorial included in the distribution. I'm stumped in Section 4.4.5, "Rule Inversion". The tutorial gives (essentially) the following example:

theory Structured
imports Main
begin

inductive ev :: "nat ⇒ bool" where
ev0:  "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"

notepad
begin
  assume "ev n"
  from this have "ev (n - 2)"
  proof cases
    case ev0 thus "ev (n - 2)" by (simp add: ev.ev0)
  next
    case (evSS k) thus "ev (n - 2)" by (simp add: ev.evSS)
  qed
end

This works, although I had to put the notepad around the proof because Isabelle didn't like assume at the top level. But now I would like to use the same proof technique by stating the same fact as a lemma, and this doesn't work:

lemma "ev n ⟹ ev (n - 2)"
proof cases
  case ev0 thus "ev (n - 2)" by (simp add: ev.ev0)
  (* ... *)

Isabelle stops at ev0, complaining Undefined case: "ev0", and then Illegal application of proof command in "state" mode at the by.

What's the difference between the two ways of stating this goal? How can I use the above proof technique with the lemma statement? (I know that I can prove the lemma using sledgehammer, but I am trying to understand Isar proofs.)

Joachim Breitner Joachim Breitner · Accepted Answer · 2015-07-04T11:46:43

The cases method tries to pick the right case analysis rule based on ”given facts”. Given facts are those that that you provide using then or from or using.

If you put your cursor on have "ev (n - 2)" you see this goal state

proof (prove): depth 1

using this:
  ev n

goal (1 subgoal):
 1. ev (n - 2)

while on lemma "ev n ⟹ ev (n - 2)" you get

proof (prove): depth 0

goal (1 subgoal):
 1. ev n ⟹ ev (n - 2)

The solution is to avoid meta-impliciation (==>) when you can use proper Isar commands to specify the assumptions of the lemma separately, and feed them to the proof using using:

lemma 
  assumes "ev n"
  shows "ev (n - 2)"
using assms

Isabelle/HOL proof by rule inversion

1 Answers