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



Peter's point is that the *given* conversions are not as modular as one may wish
them to be and that it would be nice to improve on that. And as Thomas pointed
out, improvement in user space is suboptimal.

Tobias

Am 22/10/2012 22:40, schrieb Lawrence Paulson:
> 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")
>> *)
>>
>> *}
>>
>>
>>
>>
>>
>>
> 





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