*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] structured induction proofs using customized induction scheme*From*: Bianca Lutz <bianca.lutz at gmx.net>*Date*: Thu, 4 Feb 2010 19:11:10 +0100*In-reply-to*: <4B6AB6AD.8070802@kit.edu>*References*: <5002b9521001260735x47fbe207ueb0dea8877c73695@mail.gmail.com> <1265201904.2234.97.camel@macbroy12.informatik.tu-muenchen.de> <5002b9521002031304n7ebc5980vd70deba346bc1e55@mail.gmail.com> <4B6AB6AD.8070802@kit.edu>*Reply-to*: bianca.lutz at gmx.net*Sender*: bialut at googlemail.com

Hi all. On Thu, Feb 4, 2010 at 12:59 PM, Andreas Lochbihler <andreas.lochbihler at kit.edu> 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.

**Attachment:
Sigma.thy**

**Follow-Ups**:**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Andreas Lochbihler

**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Lawrence Paulson

**References**:**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Johannes Hölzl

**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Bianca Lutz

**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] structured induction proofs using customized induction scheme
- Next by Date: Re: [isabelle] Word32/64 ?
- Previous by Thread: Re: [isabelle] structured induction proofs using customized induction scheme
- Next by Thread: Re: [isabelle] structured induction proofs using customized induction scheme
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list