[isabelle] Type definitions

Deal all,

I would like to get some ideas from you on the following type definitio in

I have the following constant:

 real_lower_bound_of :: "real set => real => bool"
 "real_lower_bound_of S u == \<forall>s \<in> S. u \<le> s"

And I am willing to define my own type of elements that are lower bounds of
a given subset S of real numbers.
The following was my first try, which failed due to the "illegal" variale S
on rhs:

typedef Lower_Bound ="{x. (real_lower_bound_of S x)}"

Is there a way to define such a type Lower_Bound for real numbers that are
lower bounds of a given real set S?
I would be very interested to know whether that is possible.
Thanks a lot.

Fulya Horozal

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