Email Gateway (Aug 18 2022 at 09:51): Email Gateway (Aug 18 2022 at 09:51):From: Fulya <fulyahorozal@gmail.com>
Deal all,
I would like to get some ideas from you on the following type definitio in
Isabelle:
I have the following constant:
constdefs
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
Email Gateway (Aug 18 2022 at 09:53):From: Tobias Nipkow <nipkow@in.tum.de>
You are trying to define a type that depends on a set (S). This is not
possible in HOL. Types and sets are completely independent. In your case
I would advise to write everything in terms of sets, not types.
Tobias
Fulya schrieb:
Last updated: May 03 2024 at 08:18 UTC