Email Gateway (Aug 18 2022 at 09:40): Email Gateway (Aug 18 2022 at 09:40):From: Christian Urban <urbanc@in.tum.de>
Hi Temesghen,
Temesghen Kahsai writes:
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)
Regardless of whether A is an inductive set or not, there is no
difference with between the formulas in the sense that they
are interderivable:
lemma no_difference:
shows "(\<forall>x \<in>A. P(x)) = (\<forall>x. x \<in> A --> P(x))"
by auto
I even think (1) is defined in terms of (2). You can find out
by having a quick look at HOL.thy.
Hope this is helpful,
Christian
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:42):From: Christian Urban <urbanc@in.tum.de>
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 .
I forgot the most important information you need: you
can help Isabelle to prove monotonicity by providing
explicit theorems with the keyword "monos". See
Section 7.3.2 in the tutorial.
Christian
Last updated: May 03 2024 at 04:19 UTC