*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 22 Oct 2012 21:40:25 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1350924337.3906.54.camel@lapbroy33>*References*: <1350924337.3906.54.camel@lapbroy33>

This module was written long ago for a specific, internal purpose and was never intended for general use, so it's hard to say what is a bug and what isn't. The beauty of conversions is that they are highly modular, so you can write your own primitives that do exactly what you want. Larry Paulson On 22 Oct 2012, at 17:45, Peter Lammich <lammich at in.tum.de> wrote: > Hi, > > my understanding of conversions is, that "conv ct" either throws an > exception or returns a theorem of the form "ct == ...". Here is a > minimal example where rewr_conv actually returns a theorem that does not > satisfy this condition, and thus, a subsequent then_conv fails > unexpectedly. > > > definition "I x \<equiv> x" > definition "A f x \<equiv> f x" > > > ML_val {* > let > open Conv > > val cv1 = fun_conv (rewr_conv @{thm I_def}) > val cv2 = rewr_conv (@{thm A_def[symmetric]}) > in > (cv1 then_conv cv2) @{cterm "I (\<lambda>s::bool. s) True"} > end > > (* > *** exception THM 0 raised (line 835 of "thm.ML"): > *** transitive: middle term > *** I (\<lambda>s\<Colon>bool. s) True \<equiv> True > *** True \<equiv> A (\<lambda>s\<Colon>bool. s) True > *) > > *} > > > The reason is, that the term after applying cv1 is not beta-reduced, and > cv2 returns a theorem with a beta-reduced left-hand side. The exception > is thrown when then_conv tries to put the two theorems together. > > The issue can be observed when instrumenting then_conv, e.g. as attached > to the end of this mail. > > I consider this a bug, because it is nowhere documented that the user of > conversions has to take care of beta-normalization manually. My proposal > for solution is as follows: > What is the status of beta-equality within Isabelle? > Alternative 1) beta-equivalent terms are considered equal: then_conv > should just work modulo beta-equivalence > Alternative 2) They are not considered equal on this low-level: > rewr_conv should be forced to return an equal term. > > Anyway, if none of the two alternatives is appropriate, the rules for > composing conversions should be CLEANLY documented. > > Regards, > Peter > > > > > > -------------------------- > ML_val {* > let > open Conv > > (* Instrumenting then_conv to make the reason for the error visible: > *) > fun (cv1 then_conv cv2) ct = > let > val eq1 = cv1 ct; > val eq2 = cv2 (Thm.rhs_of eq1); > in > if Thm.is_reflexive eq1 then eq2 > else if Thm.is_reflexive eq2 then eq1 > else ( > tracing ("RHS1: "^PolyML.makestring (Thm.rhs_of eq1 |> > term_of)); > tracing ("LHS2: "^PolyML.makestring (Thm.lhs_of eq2 |> > term_of)); > Thm.transitive eq1 eq2 > ) > end; > in > let > val cv1 = fun_conv (rewr_conv @{thm I_def}) > val cv2 = rewr_conv (@{thm A_def[symmetric]}) > in > (cv1 then_conv cv2) @{cterm "I (\<lambda>s::bool. s) True"} > end > end > > (* TRACE: > > RHS1: Abs ("s", "bool", Bound 0) $ Const ("HOL.True", "bool") > > LHS2: Const ("HOL.True", "bool") > *) > > *} > > > > > >

**Follow-Ups**:**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:*Tobias Nipkow

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

**References**:

- 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