Re: [isabelle] the hereditarily finite sets

Hi Larry,

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


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.