# [isabelle] proving monotonicity

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

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