[isabelle] proving monotonicity
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
shows "(\<forall>x \<in>A. P(x)) = (\<forall>x. x \<in> A --> P(x))"
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,
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and