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
let_simp_betaeta.bundle
Description: Binary data
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
