Re: [isabelle] proving monotonicity



On Friday 01 September 2006 09:31, Christian Urban wrote:
> Temesghen Kahsai writes:
>  > 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.

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





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