*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Strange eta-expansion on induction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 01 Mar 2012 19:56:32 +0100*In-reply-to*: <1330624422.2056.28.camel@lapbroy33>*References*: <1330624422.2056.28.camel@lapbroy33>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2

The induct method itself does not eta-contract or expand. It merely uses primitives, in particular resolution, which in turn uses higher-order unification. And higher-order unification does indeed eta-expand. In certain situations. This is intentionally not fixed and you should not expect or rely on a particular behaviour. That is, you may have to ensure eta-contraction yourself if some part of your proof method is sensitive to it. Tobias Am 01/03/2012 18:53, schrieb Peter Lammich: > Hi, > > [Referring to Isabelle-2011-1] > > I recently encountered a quite strange behavior of the induct method. It > seems to arbitrarily eta-expand its subgoals under certain conditions > (If the induction variable is nested inside higher-order context ???). > > In the boiled-down example below, the first induct method fully > eta-expands its subgoals. In the second induct-method, the subgoals are > not eta-expanded, but the generated cases are. That is, on apply-style > scripts, you see eta-contracted goals, and when switching to ISAR, using > case-commands, you get eta-expanded goals. > > Is this behavior somehow documented? Can I switch it off? > In my concrete application, it kills my simplifier setup, as the > simplifier applies rules inside the eta-expanded terms that I do not > expect to be applied there. > > Regards, > Peter > > > -------------------------------------- > > declare [[eta_contract = false ]] (* Configure pretty-printer not to > eta-contract on pretty-printing *) > > consts > f :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" > i :: "('a list \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b > \<Rightarrow> bool)" > > lemma "f (i xs s)" > apply (induct xs) (* Subgoals are fully eta-expanded here *) > print_cases (* Cases are eta-expanded, too*) > oops > > lemma "f (i xs s)" > apply (induct xs arbitrary: s) (* Subgoals are *NOT* eta-expanded here > *) > print_cases (* Cases are eta-expanded *) > oops > >

**Follow-Ups**:**Re: [isabelle] Strange eta-expansion on induction***From:*Brian Huffman

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

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

- Previous by Date: [isabelle] Strange eta-expansion on induction
- Next by Date: Re: [isabelle] Strange eta-expansion on induction
- Previous by Thread: [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