Re: [isabelle] residual subgoals



Hi Lars,

> > Is it standard practice not to bother these but postpone solving them via
> the final qed?
> 
> I'd say it's not standard practice. Most Isabelle users prefer not using meta-
> implications and meta-quantification in Isar proofs if it can be avoided. See
> Lars Noschinski's answer here for a case where it actually doesn't work if you
> use meta-implication:
> 
>   <https://stackoverflow.com/a/25442787/4776939>

Thanks. Re-formulating my goal I wrote

lemma
 fixes n :: "nat"
 assumes "computational_even n"
 shows "structural_even n"
proof (induct n rule:computational_even.induct)

which results in 

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

where the 2nd subgoal is simply not true.

What is wrong with that lemma expression?

- Gergely


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