# [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.