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

The two problematical subgoals contain schematic type variables. Enabling "show types" reveals them. See attachment.
Larry Paulson

PNG image

On 4 Feb 2010, at 18:11, Bianca Lutz wrote:

> 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.
> Thanks,
> Bianca.
> <Sigma.thy>

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