*To*: bianca.lutz at gmx.net*Subject*: Re: [isabelle] structured induction proofs using customized induction scheme*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 5 Feb 2010 10:50:15 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5002b9521002041011j25ac2243lf2c4fee7b7c86957@mail.gmail.com>*References*: <5002b9521001260735x47fbe207ueb0dea8877c73695@mail.gmail.com> <1265201904.2234.97.camel@macbroy12.informatik.tu-muenchen.de> <5002b9521002031304n7ebc5980vd70deba346bc1e55@mail.gmail.com> <4B6AB6AD.8070802@kit.edu> <5002b9521002041011j25ac2243lf2c4fee7b7c86957@mail.gmail.com>

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

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 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. > <Sigma.thy>

**Follow-Ups**:

**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

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

- Previous by Date: Re: [isabelle] structured induction proofs using customized induction scheme
- Next by Date: Re: [isabelle] structured induction proofs using customized induction scheme
- 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