*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Wed, 24 Oct 2012 14:14:06 +1100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1210231256560.23478@macbroy20.informatik.tu-muenchen.de>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

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)) endYou 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.

Thinking in terms of "broken" and "fixed" is unwise. Which is actually my main complaint on this thread.

Yours, Thomas.

**Follow-Ups**:**Re: [isabelle] rewr_conv***From:*Tobias Nipkow

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

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