*To*: "Tjark Weber" <tjark.weber at gmx.de>, Isabelle <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] SOME simplification*From*: "Gabriele Pozzani" <gabriele.pozzani at gmail.com>*Date*: Thu, 21 Dec 2006 15:44:25 +0100*In-reply-to*: <200612211330.28841.tjark.weber@gmx.de>*References*: <b3262abf0612200648k12d1fcc0xa50e81df7aa0d84c@mail.gmail.com> <200612211330.28841.tjark.weber@gmx.de>

Hello, I'm not familiar with the IOA theory, but it seems the problem is that

"SOME i. L i e" is a particular natural number only after e has been fixed. In your assumption g however, i is quantified at the outermost level, and hence may not depend on e.

Yes, probably the problem is here! One possible solution is to modify your assumption g:

g': "ALL (i'::('a Seq => bool)=>nat). prob (%e. (L (i' e) e) ~> Q, q)" Now you can instantiate i' in g' with "%e. SOME i. L i e" to show a.

Ok, thank you very much for your help. Bests Gabriele

**References**:**[isabelle] SOME simplification***From:*Gabriele Pozzani

**Re: [isabelle] SOME simplification***From:*Tjark Weber

- Previous by Date: Re: [isabelle] SOME simplification
- Next by Date: Re: [isabelle] Problem installing on an intel mac
- Previous by Thread: Re: [isabelle] SOME simplification
- Next by Thread: Re: [isabelle] Problem installing on an intel mac
- Cl-isabelle-users December 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list