*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Strange eta-expansion on induction*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 02 Mar 2012 11:41:13 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1203012141260.6158@macbroy22.informatik.tu-muenchen.de>*References*: <1330624422.2056.28.camel@lapbroy33> <4F4FC660.1010302@in.tum.de> <alpine.LNX.2.00.1203012141260.6158@macbroy22.informatik.tu-muenchen.de>

> 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. So, if I have to expect eta-expansion at any point, I have to add additional rules to the simpset to make it confluent again. This certainly works, but may blow up the simpset. Just as a remark: The simpset setup from the standard library has such problems, too --- for example there is id_apply, that happily simplifies "%x. id x" to "%x. x", but not "id" (I already had problems with that). -- Peter

**Follow-Ups**:**Re: [isabelle] Strange eta-expansion on induction***From:*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

- Previous by Date: Re: [isabelle] Strange eta-expansion on induction
- Next by Date: [isabelle] New AFP entry: Abortable Linearizable Modules
- Previous by Thread: Re: [isabelle] Strange eta-expansion on induction
- Next by Thread: Re: [isabelle] Strange eta-expansion on induction
- 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