Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] introduction rule for order bounded quantifiers.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:04):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:06):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

Last updated: Apr 20 2024 at 04:19 UTC