*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Strange eta-expansion on induction*From*: Makarius <makarius at sketis.net>*Date*: Mon, 12 Mar 2012 14:09:04 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1330684873.2614.11.camel@lapbroy33>*References*: <1330624422.2056.28.camel@lapbroy33> <4F4FC660.1010302@in.tum.de> <alpine.LNX.2.00.1203012141260.6158@macbroy22.informatik.tu-muenchen.de> <1330684873.2614.11.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 2 Mar 2012, Peter Lammich wrote:

As Tobias points out, the Pure Isabelle system conceptually works modulo eta (and beta and alpha) conversion -- although there are well known traps. So to continue the thread, I would also like to see the other part -- the proof tool by Peter that fails here.It's no custom "proof tool" involved here. My setting is roughly like this: I have assertions of type "heap => addr set => bool", and hoare-tripels of type "assertion => program => assertion => bool" (syntax: {P} S {Q}) I defined the assertion definition [simp]: "false h as == False" Moreover, I have a rule lemma [simp]: "{false} S {Q}" The proof that fails has the form: lemma "{is_list xs p} S Q" proof (induct xs arbitrary: p) case Nil show ?case by (cases p, simp_all) ...Here, depending on the case for p, "is_list [] p" simplifies to false,which is then simplified to \lambda _ _. False, before the rule for{false} S {Q} is applied.

Makarius

**References**:**[isabelle] Strange eta-expansion on induction***From:*Peter Lammich

**Re: [isabelle] Strange eta-expansion on induction***From:*Tobias Nipkow

**Re: [isabelle] Strange eta-expansion on induction***From:*Makarius

**Re: [isabelle] Strange eta-expansion on induction***From:*Peter Lammich

- Previous by Date: [isabelle] Install Isabelle under Windows (with Cygwin)
- Next by Date: Re: [isabelle] Attribute code called 3 times
- Previous by Thread: Re: [isabelle] Strange eta-expansion on induction
- Next by Thread: [isabelle] New AFP entry: Abortable Linearizable Modules
- Cl-isabelle-users March 2012 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