[isabelle-dev] Problem with let-simproc

Johannes Hölzl hoelzl at in.tum.de
Tue Feb 5 14:48:50 CET 2013

Hi Isabelle-dev,

there is a bugproblem with the let-simproc, resulting in a non
terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of

  theory Scratch imports Complex_Main begin

  lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
    using [[simp_trace]]
    apply simp

The attached hg-bundle changes this behaviour to a terminating simproc. 
(The bundle can be applied to a repo containing #58e2d0cd81ae by
"hg pull let_simp_betaeta.bundle")

It currently runs in the testboard:

@Makarius: Is it possible to include this patch in Isabelle2013, when
the testboard run is green?

== Analysis ==

The let-simproc produces:
  (let x = Collect P in R x x ∧ (Ball s P)) ==
  (let x = Collect P in R x x ∧ (ALL t : s. P t))

So it looks like the simproc forgets a eta-conversion step.

== Solution ==

The problematic part is (in HOL.thy, let_simp):

  if (Term.betapply (f, x)) aconv g then NONE (*avoid identity conversion*)

I would apply Envir.beta_eta_contract on both sides:

  if (Envir.beta_eta_contract (Term.betapply (f, x))) aconv (Envir.beta_eta_contract g) then NONE (*avoid identity conversion*)

Or is there a better way to do this?


-------------- next part --------------
A non-text attachment was scrubbed...
Name: let_simp_betaeta.bundle
Type: application/octet-stream
Size: 597 bytes
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130205/d0e559cf/attachment.obj>

More information about the isabelle-dev mailing list