Re: [isabelle] structured induction proofs using customized induction scheme

Hi all.

On Thu, Feb 4, 2010 at 12:59 PM, Andreas Lochbihler
<andreas.lochbihler at> wrote:
> 3. Your induction rule R_induct involves the free variable P2 that does not
> occur in the conclusion nor in the consumed facts. This is usually the cause
> for your error message "unbound schematic variable(s) in case 2".

Actually, the error doesn't concern unbound schematic variables but
"illegal" ones.
Which is just odd since there is no schematic variable besides "?case" ...

Anyway, I refactored my code according to your advices.
In addition I updated my Isabelle environment to the latest version
(just in case that my installation was corrupted). Unfortunately, the
error still occurs.

Since Andreas was unable to reproduce the error I assume that the
induction rule doesn't cause the error but something else I missed.
Therefore, I stripped off anything that is not involved in the failing
proof (the corresponding lemma is called beta_lc). Nevertheless, this
minimal version fails on my machine.
Attached you will find the source file including an apply style proof
of beta_lc that works just fine. I would be grateful if anyone could
try to reproduce the error using this.


Attachment: Sigma.thy
Description: Binary data

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