*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*: Makarius <makarius at sketis.net>*Date*: Mon, 22 Oct 2012 21:27:08 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1350924337.3906.54.camel@lapbroy33>*References*: <1350924337.3906.54.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 22 Oct 2012, Peter Lammich wrote:

my understanding of conversions is, that "conv ct" either throws anexception or returns a theorem of the form "ct == ...". Here is aminimal example where rewr_conv actually returns a theorem that does notsatisfy this condition, and thus, a subsequent then_conv failsunexpectedly.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.

(ML *raises* exceptions, other languages like Java *throw* them.)

I consider this a bug, because it is nowhere documented that the user ofconversions has to take care of beta-normalization manually.

(* single rewrite step, cf. REWR_CONV in HOL *) fun rewr_conv rule ct = let val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; val lhs = Thm.lhs_of rule1; val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; in Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2 handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]) end;

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.

* The system knows alpha, beta, eta conversion. * Some layers use alpha (kernel). * Some layers use alpha + beta + eta (simplifier, resolution) but normalize in different directions. * Insisting too much in one way or the other causes trouble. * It is possible not to insist too much. * What is your concrete application anyway? Makarius

**Follow-Ups**:

**References**:

- Previous by Date: [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: [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