[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.