Reputation: 9378
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.)
Upvotes: 3
Views: 1301
Reputation: 25763
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
Upvotes: 4