[isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

Hi Isabelle-dev,

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

  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:
  http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c

@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?

Greetings,
  Johannes

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