[isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: let_simp_betaeta2.bundle
Type: application/octet-stream
Size: 678 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130205/4244c3ac/attachment-0002.obj>