*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rewr_conv*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 24 Oct 2012 17:50:53 +0200*In-reply-to*: <50875CFE.2080406@nicta.com.au>*References*: <1350924337.3906.54.camel@lapbroy33> <7588B83F-3006-45D4-ACBC-2EB0693E79BD@cam.ac.uk> <5085F0E7.9070207@nicta.com.au> <alpine.LNX.2.00.1210231256560.23478@macbroy20.informatik.tu-muenchen.de> <50875CFE.2080406@nicta.com.au>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121010 Thunderbird/16.0.1

After a false start and some experiments I have now converged on (essentially) Thomas' solution, but integrated into rewr_conv. It lets resolution do the work and is thus immune against funny matchers. No point in doing anything cleverer. No theory in the distribution or the AFP were affected and Peter's example works fine now. Enjoy Tobias Am 24/10/2012 05:14, schrieb Thomas Sewell: > >>> fun fix_conv conv ct = let >>> val thm = conv ct >>> val eq = Logic.mk_equals (term_of ct, term_of ct) |> head_of >>> in if (term_of (Thm.lhs_of thm) aconv term_of ct) >>> then thm >>> else thm RS trivial >>> (Thm.mk_binop (cterm_of (theory_of_cterm ct) eq) ct (Thm.rhs_of thm)) >>> end >> You should explain what "_ RS trivial" does. It is the conventional way >> to let Larry's rule composition calculus do its normalization for you. > Admittedly this is not beautiful code. I just happened to have it. > > What "thm RS trivial P" does is constructs the trivial theorem "P ==> P" and > then discharges its assumption using thm. > > The point here is to specify the conclusion we want (Thm.mk_binop ...) with the > original cterm on the left hand side, construct a theorem with that conclusion, > and then "prove" it by resolution with a theorem we have (which is > alpha-beta-eta- equivalent). Yes, that is a big hammer to apply, but it won't be > applied all that often. The major cost here is checking whether it is needed all > the time. > >> Thinking in terms of "broken" and "fixed" is unwise. Which is actually my >> main complaint on this thread. > > Some things are neither broken nor fixed, they are just surprising, but > surprising for good reason. This is broken. As others have pointed out, there is > a clear contract for convs to follow so that then_conv can chain them using > Thm.transitive. This contract is not followed by rewr_conv. > > This is one solution. An alternative would be to broaden the contract by having > then_conv catch the exception from Thm.transitive and switch to a more general > mechanism (possibly by doing the above). This might create problems for some > other consumers of convs, which I have not taken time to investigate. > > Yours, > Thomas. >

**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:*Makarius

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

- Previous by Date: [isabelle] mergesort (was: BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue)
- Next by Date: [isabelle] Print proof of theorem
- 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