*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 23 Oct 2012 13:07:06 +0200*In-reply-to*: <CAAMXsiYtk-FyKBTA05e=TnvAAgR1Hx=GLuC-Vt=GufP-6e=UMQ@mail.gmail.com>*References*: <1350924337.3906.54.camel@lapbroy33> <7588B83F-3006-45D4-ACBC-2EB0693E79BD@cam.ac.uk> <5085F0E7.9070207@nicta.com.au> <CAAMXsiYtk-FyKBTA05e=TnvAAgR1Hx=GLuC-Vt=GufP-6e=UMQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121010 Thunderbird/16.0.1

Am 23/10/2012 07:38, schrieb Brian Huffman: > Peter neatly stated the behavior that we all expect of conversions: > > On Mon, 22 Oct 2012, Peter Lammich wrote: >> > my understanding of conversions is, that "conv ct" either throws an >> > exception or returns a theorem of the form "ct == ...". > The current situation is this: Conv.rewr_conv only satisfies this > property if a side-condition is met, namely that the input cterm must > be already in beta-normal form. > > The proposal is to modify rewr_conv to remove the side-condition: It > should satisfy the basic property also for non-beta-normal cterms. On > beta-normal cterms, rewr_conv should behave exactly as it did before. > (Thomas's fix_conv would be one possible implementation of this > proposal.) > > So far, I haven't seen any good arguments against this change. This is the essence: rewr_conv only satisfies "A conversion is any function that maps a term t to a theorem |-t==u." LCP, 1983 up to beta-equivalence. Since conversions are low-level proof methods which are sensitive to the precise term structure, this is a wart that causes non-modularity. This non-modularity only shows up (to refine Brian's analysis) if the lhs of the rewrite rule has a free variable F in an applied position: F t. This does not happen very often, but if it does, rewr_conv should still behave nicely. It should do a non-normalizing instantiation followed by a beta-normalization. Tobias

**Follow-Ups**:

**References**:**[isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Peter Lammich

**Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Lawrence Paulson

**Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Thomas Sewell

**Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Brian Huffman

- Previous by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Next by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Previous by Thread: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Next by Thread: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Cl-isabelle-users October 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