Email Gateway (Aug 18 2022 at 13:59): Email Gateway (Aug 18 2022 at 13:59):From: Tobias Nipkow <nipkow@in.tum.de>
You cannot use sets as types. You have to use the underlying type of the
set. Thus you need to define
F :: "t set => t"
where A is of type "t set". If F has no sensible extension to arbitrary
sets, you may need to define something like
"F B = (if finite B then ... else undefined)"
where "undefined" is a predefined constant whose value is not known.
Regards
Tobias
Bart Kastermans schrieb:
Email Gateway (Aug 18 2022 at 13:59):From: Tobias Nipkow <nipkow@in.tum.de>
PS If the definition of the function follows the inductive definition of
the set, it may be better to define your function as an inductive
relation, possibly turning it into a function via THE afterwards.
Tobias
Bart Kastermans schrieb:
Email Gateway (Aug 18 2022 at 13:59):From: Slawomir Kolodynski <skokodyn@yahoo.com>
In Isabelle/ZF Fin(A) -> A is a set of functions whose domain is Fin(A) and values are in A. The statement "F : Fin(A) -> A" is the same as "F \<in> Fin(A) -> A" and means that F is in this set (i.e. is such function).
Slawekk
http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 18 2022 at 14:05):From: Bart Kastermans <Bart.Kastermans@Colorado.EDU>
In
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Finite.html
the collection of finite subsets Fin(A) of a set A is defined. I want
to define a function
F : Fin(A) => A.
What is the best way to go about this? None of my attempts parse. I
realize that Fin(A) is not a type, but am not sure how to work around this.
Best,
Bart
Last updated: Apr 24 2024 at 12:33 UTC