I have
theory Even
imports Main
begin
inductive
structural_even :: "nat ⇒ bool"
where
"structural_even 0"
| "structural_even n ⟹ structural_even (Suc(Suc n))"
fun
computational_even :: "nat ⇒ bool"
where
"computational_even 0 = True"
| "computational_even (Suc 0) = False"
| "computational_even (Suc(Suc n)) = computational_even n"
lemma "computational_even n ⟹ structural_even n"
proof (induct n rule: computational_even.induct)
show "computational_even 0 ⟹ structural_even 0"
by (metis structural_even.intros(1))
next
After proof I get
goal (3 subgoals):
1. computational_even 0 ⟹ structural_even 0
2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))
I got the metis call from sledgehammer where
structural_even.intros(1) = structural_even 0
I get
show computational_even 0 ⟹ structural_even 0
Successful attempt to solve goal by exported rule:
computational_even 0 ⟹ structural_even 0
proof (state): depth 0
then. However, after next I get
goal (3 subgoals):
1. computational_even 0 ⟹ computational_even 0
2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))
So there is a trivial residual subgoal at 1., despite the system said "Successful attempt to solve goal by exported rule".
Why this happens, and how can I fix it?
Sledgehammer has found a correct proof (though you may want to use simp instead). In fact you can continue with the second and third subgoals (that will be reduced to similar new subgoals as you have for #1 after you prove them) and to finally finish the proof with qed.
The issue is how Isabelle handles assumptions. If, as in you case, they are not listed explicitly, it is left to the user to prove them. This effect is more explicit if
show "computational_even 0 ⟹ structural_even 0"
is replaced with equivalent
presume "computational_even 0"
show "structural_even 0"
Your proof shows that structural_even 0 is true as soon as computational_even 0 is true, but Isabelle "has no idea" why the latter is true. Therefore it leaves you with the new subgoal that the assumption stated in the proof can be derived from the assumption stated in the subgoal. This subgoal will be handled by qed that finishes the proof by taking assumptions into account.
BTW, the assumption for this case is not required at all, because structural_even 0 is true by its definition. So the assumption can be safely removed, leaving only
show "structural_even 0"
Moreover, you can specify arbitrary assumptions with presume, but you will have to prove them later. For example, you can prove the goal
presume "computational_even (Suc 0)"
show "structural_even 0"
but then you will have to prove the (false) goal computational_even 0 ⟹ computational_even (Suc 0).
In order to unify assumption with a premise of a goal, assume is used instead:
assume "computational_even 0"
show "structural_even 0"
In that case there is no need to prove assumption of the subgoal (this is already done by the unification step with assume). As a result after finishing the proof of the subgoal, only 2 subgoals will be left as you expected.
As a free bonus, when assume is used with a wrong assumption (e.g., as in the earlier erroneous case, computational_even (Suc 0)), Isabelle will complain that the corresponding show statement fails to refine any pending goal and you will not be able to proceed.