Isabelle / HOL proof using rule inversion
I am getting started with Isabelle / HOL and am working on the tutorial prog-prove.pdf
included with the distribution. I'm puzzled in section 4.4.5 "Inverting a Rule". 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
It works, although I had to put the notepad
proof around because Isabella didn't like assume
the top level. But now I would like to use the same method of proof, specifying the same fact as the lemma, and it 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"
, then Illegal application of proof command in "state" mode
at by
.
What's the difference between the two ways to define this goal? How can I use the above proof technique with the lemma assertion? (I know I can prove the lemma using sledgehammer
, but I am trying to understand Isar's proofs.)
source to share
The method cases
tries to select the correct case analysis rule based on "given facts". The facts shown are those that you provide with then
either from
or using
.
If you put your cursor on have "ev (n - 2)"
you will see this target state
proof (prove): depth 1
using this:
ev n
goal (1 subgoal):
1. ev (n - 2)
until 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 the meta-implication ( ==>
) where you can use the correct Isar commands to separately specify the lemma's assumptions and submit them for proof with using
:
lemma
assumes "ev n"
shows "ev (n - 2)"
using assms
source to share