[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
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>
More information about the isabelle-dev
mailing list