Re: [isabelle] residual subgoals

You need not modify the lemma statement and "proof" line at all. Induction is very happy with implicational goals.


On 03/02/2016 11:50, Buday Gergely wrote:
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:


Thanks. Re-formulating my goal I wrote

  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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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