# [isabelle] residual subgoals

```Hi,

following

http://stackoverflow.com/questions/35156803/sledgehammer-gives-insufficient-proof-tactic

I created

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
show "computational_even (Suc 0) â structural_even (Suc 0)"
by (metis computational_even.simps(2))
next
show "ân. (computational_even n â structural_even n) â computational_even (Suc (Suc n)) â structural_even (Suc (Suc n))"
proof
fix n
assume "computational_even n â structural_even n"
from this show "computational_even (Suc (Suc n)) â structural_even n"
by (simp only: computational_even.simps(3))
qed
qed

end

--

before the last qed, the Output window says

goal (4 subgoals):
1. computational_even 0 â computational_even 0
2. computational_even (Suc 0) â computational_even (Suc 0)
3. ân. (computational_even n â structural_even n) â
computational_even (Suc (Suc n)) â computational_even n â structural_even n
4. ân. (computational_even n â structural_even n) â
computational_even (Suc (Suc n)) â computational_even (Suc (Suc n))

These all seem trivial and qed does overcome them.

Is it standard practice not to bother these but postpone solving them via the final qed?

- Gergely

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.