Email Gateway (Aug 18 2022 at 09:35): Email Gateway (Aug 18 2022 at 09:35):From: Temesghen Kahsai <lememta@gmail.com>
Hi all,
is there any difference in Isabelle\HOL the following two formulas:
1) \<forall>x \<in>A. P(x)
2) \<forall>x. x \<in> A --> P(x)
A is an inductive set.
I would like to use the first solution within a coinductive definition.
I don't get any error if I use the second solution, but if I use the
first one the coinductive definition fail to prove the monotonicity .
Any advice?
Thanks in advance for the collaboration.
Regards.
-T
Email Gateway (Aug 18 2022 at 09:45):From: Tjark Weber <tjark.weber@gmx.de>
The definition is in HOL/Set.thy, see theorem Ball_def and the subsection on
"Bounded Quantifiers". The translation that goes on behind the scenes is
perhaps a little bit obscure. (1) and (2) are logically equivalent, but it's
not the case that (1) is internally rewritten to (2). So it's well possible
that Isabelle shows different behavior for (1) and (2).
Best,
Tjark
Last updated: May 03 2024 at 04:19 UTC