*To*: bianca.lutz at gmx.net*Subject*: Re: [isabelle] structured induction proofs using customized induction scheme*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Fri, 05 Feb 2010 10:28:07 +0100*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>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Bianca,

proof (induct taking: ... rule: beta_induct[where ?'a="unit" and ?'b="unit"]) case UpdR Best regards, Andreas Bianca Lutz schrieb:

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.

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Gebäude 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-8352 Fax: +49 721 608-8457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**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] Word32/64 ?
- 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