*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 22 Oct 2012 18:45:37 +0200

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

- Previous by Date: [isabelle] Formalization of Social network(SN)
- Next by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Previous by Thread: [isabelle] Formalization of Social network(SN)
- 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