Email Gateway (Aug 19 2022 at 11:13): Email Gateway (Aug 19 2022 at 11:13):From: "Roger H." <s57076@hotmail.com>
Hello,
how do you denote the set of all functions from nat to nat?
what about the set of all partial functions from nat to nat?
Thank you!
Email Gateway (Aug 19 2022 at 11:13):From: Lars Noschinski <noschinl@in.tum.de>
On 22.05.2013 21:37, Roger H. wrote:
how do you denote the set of all functions from nat to nat?
For some type 'a, (UNIV :: 'a) denotes all values of this type. So "UNIV
:: nat => nat" are all functions from nat to nat.
what about the set of all partial functions from nat to nat?
Isabelle/HOL is a logic of total functions, i.e. there are no partial
functions. One way to model partial functions is to carry around an
explicit domain. Another way is to use functions from 'a to 'b option.
-- Lars
Email Gateway (Aug 19 2022 at 11:13):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Roger,
I would take the UNIV constants, which is the set of all elements
of a given type.
I.e., in your case you will require
term "UNIV :: (nat => nat) set"
term "UNIV :: (nat => nat option) set"
Cheers,
René
Last updated: Apr 26 2024 at 16:20 UTC