[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")
*)

*}










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