# [isabelle] introduction rule for order bounded quantifiers.

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] introduction rule for order bounded quantifiers.
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Thu, 02 Sep 2010 12:56:49 +0300
*In-reply-to*: <4C7D35DE.6030104@in.tum.de>
*References*: <4C7D2E98.4080303@uni-muenster.de> <4C7D35DE.6030104@in.tum.de>
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*