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



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)


--- On Tue, 9/1/09, Bart Kastermans <Bart.Kastermans at Colorado.EDU> wrote:

> From: Bart Kastermans <Bart.Kastermans at Colorado.EDU>
> Subject: [isabelle] Defining a function on an inductively defined set.
> To: cl-isabelle-users at lists.cam.ac.uk
> Date: Tuesday, September 1, 2009, 11:07 AM
> 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.