[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.email@example.com>
- References: <4C7D2E98.firstname.lastname@example.org> <4C7D35DE.email@example.com>
- User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:220.127.116.11) Gecko/20100802 Thunderbird/3.1.2
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and