*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] introduction rule for order bounded quantifiers.*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 02 Sep 2010 13:16:13 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C7F74E1.7060108@abo.fi>*References*: <4C7D2E98.4080303@uni-muenster.de> <4C7D35DE.6030104@in.tum.de> <4C7F74E1.7060108@abo.fi>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

Bounded quantifiers are not abbreviations but constants in themselves. The intro rules are bexI and ballI. The rules can be found in Set.thy. If you are wondering where a particular function or syntax comes from, I recommend to look up "What's in Main" http://isabelle.in.tum.de/dist/Isabelle/doc/main.pdf for locating it. Tobias Viorel Preoteasa schrieb: > Hello, > > I have a question about order bounded quantifiers. > > I have a goal like "i <= n ==> \<exists> j <= Suc n. x ^ j = x ^ i" > which should be trivial by instantiating j with i, however using > (rule_tac x = i in exI) does not work. What is the introduction > theorem for this kind of quantifiers? Where is this theorem > defined? > > Best regards, > > Viorel Preoteasa

**References**:**[isabelle] introduction rule for order bounded quantifiers.***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Post-Doc and PhD positions - Semantics of Real-World Computer Systems
- Next by Date: [isabelle] fixrec’s demand for continuity proofs
- Previous by Thread: [isabelle] introduction rule for order bounded quantifiers.
- Next by Thread: [isabelle] Post-Doc and PhD positions - Semantics of Real-World Computer Systems
- Cl-isabelle-users September 2010 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