Okay, this fails in HOL-IMP. The check I introduced is to strong. I relaxed the check now and it should check if f =beta-eta-alpha= g, where g is the simplified version of f.
The testboard changeset is: http://isabelle.in.tum.de/testboard/Isabelle/rev/e9827a6f934e - Johannes Am Dienstag, den 05.02.2013, 14:48 +0100 schrieb 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 > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
let_simp_betaeta2.bundle
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
