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



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





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