Why can't we do case analysis on inductively defined predicates *directly* when doing rule inversion?

Question

There seems to be something about inductive predicates I don't understand since I keep getting issues with them. My most recent struggle is to understand case analysis with inductively defined predicates on ev from chapter 5 of the concrete semantics books.

Assume I am proving

lemma
  shows "ev n ⟹ ev (n - 2)"

I've tried to start the proof immediately in Isabelle/HOL but it complains when I try or gives weird goals:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

which shows:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2) 

which is not what I expected.

When I pass n to cases we instead induct on the definition of natural numbers (note other times it does the induction on ev correctly, see later example):

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases n)

gives:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; n = 0⟧ ⟹ ev (n - 2)
 2. ⋀nat. ⟦ev n; n = Suc nat⟧ ⟹ ev (n - 2) 

which is not what I expected. Note however that the following DOES work (i.e. it inducts on ev not on natural numbers) even with n as a parameter:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof -
  assume 0: "ev n"
  from this show "ev (n - 2)"
  proof (cases n)

I realize that there must be some magic about assuming ev n first and then stating to show ev (n-2) otherwise the error wouldn't occur.

I understand the idea of rule inversion (of arriving at a given fact to be proven in reverse, by analysis the cases that could have lead to it). For the "even" predicate the rule inversion is:

ev n ==> n = 0 ∨ (∃k. n = Suc (Suc k) ∧ ev k)

which makes sense based on the inductively defined predicate:

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

but I don't understand. Why wouldn't directly doing the cases work? or why is this syntax invalid:

proof (cases ev)

or this:

proof (cases ev.case)

etc.

I think the crux is that at the heart I don't know when dealing with inductively define predicates if this induction is applied to the goal or the assumption, but from the writing on of the textbook:

The name rule inversion emphasizes that we are reasoning backwards: by which rules could some given fact have been proved?

I'd assume it's applying rule inversion to the goals since it says "by which rules could some given fact have been proved".

In addition, this example ev ==> ev (n-2) froom the book does not help because both the premise and conclusion have ev involved.

How is case analysis with rule inversion really working and why do we need to assume things first for Isabelle to give sensible goal for case analysis?

Answer 1

Not sure I understand the entire question but this:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

Gives you:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2) 

because Isabelle is splitting on the truth of ev n, i.e. either true or false. I believe the syntax you are looking for is:

proof (cases rule: ev.cases)

Which is how you tell Isabelle explicitly what rule it should use for a proof by cases.

Answer 2

The way to do it is as the answer Ben Sheffield said:

proof (cases rule: ev.cases)

I also noticed that:

apply (rule ev.cases)

works, but I think it would be helpful to go through a small example to see the cases explicitly outlined:

Consider:

lemma "ev n ⟹ ev (n - 2)"

first inspect it's cases theorem:

thm ev.cases
⟦ev ?a; ?a = 0 ⟹ ?P; ⋀n. ⟦?a = Suc (Suc n); ev n⟧ ⟹ ?P⟧ ⟹ ?P 

then it unifies the goal and introduces the new goals with the original assumptions and all the assumption for the cases. That is why there is a ev n in all of them.

  apply (rule ev.cases)

has goals:

proof (prove)
goal (3 subgoals):
 1. ev n ⟹ ev ?a
 2. ⟦ev n; ?a = 0⟧ ⟹ ev (n - 2)
 3. ⋀na. ⟦ev n; ?a = Suc (Suc na); ev na⟧ ⟹ ev (n - 2)

and you can do simp and proceed the proof as normal.