Re: [isabelle] the hereditarily finite sets



Hi Larry,

You are right, FinFun sets are ordinary finite sets or predicates.

Andreas

Am 25.03.2012 um 22:30 schrieb Lawrence Paulson:

> Thanks, but I believe that you are describing finite sets rather than hereditarily finite sets. I should have mentioned, the membership function should have the following type:
> 
> 	member  :: hf => hf => bool
> 
> That is, we have one single type rather than separate types of sets and elements.
> 
> It sounds like this hasn't been formalised before...?
> 
> Larry
> 
> On 25 Mar 2012, at 20:18, Andreas Lochbihler wrote:
> 
>> Hi Larry,
>> 
>> The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP.






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