Re: [isabelle] Defining a function on an inductively defined set.



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:
> 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





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