# Re: [isabelle] FuncSet without extensional? (Joachim Breitner)

List.thy contains an inductively defined set "lists A" which is
equivalent to your "List A". Strangely enough, the equality "lists A =
{xs. set xs <= A}" is not present, but can be proved automatically.

Tobias

Andrei Popescu schrieb:
> Dear Joachim,
>
>>> You define
>>> definition List :: "'a set => 'a list set"
>>> where "List A ≡ {l. set l ≤ A}"
>
>>> This is a definition that I could use in the development of Free Groups.
>>> Assuming I would not need the cardinality lemmas, what is the best
>>> practice: Importing your theory nevertheless, copying the definition or
>>> pushing to add this definition in a more standard, common place, i.e.
>>> HOL or HOL/Library?
>
> IMO, if you only need that simple function, it is better to just redefine it
> rather than
>
> importing the whole theory of cardinals.
> I agree that its presence is desirable in the standard library though.
> (Or maybe it even exists, but I was not able to find it.)
>
> Best regards,
>    Andrei
>
>
>
>
>
> ----- Original Message ----
> From: Joachim Breitner <mail at joachim-breitner.de>
> To: Andrei Popescu <uuomul at yahoo.com>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Sent: Mon, September 20, 2010 3:41:30 AM
> Subject: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
>
> Dear Andrei,
>
> Am Sonntag, den 19.09.2010, 20:20 -0700 schrieb Andrei Popescu:
>>>> BTW, are there already theories about uncountable sets? I?d need, as a
>>>> lemma, the fact that the M* (the set of finite words) of a uncountably
>>>> infinte set M has the same cardinality.
>> Actually, quite a bit of the ZF theory of cardinals can be done in HOL.
>> I have already set the basis of such a theory: it is in the Isabelle AFP, and
>> is
>>
>>
>> fairly well documented.
>>
>> http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml
>>
>> Your lemma is stated there in the theory Cardinal_order_relation, in subsection
>>
>> "Cardinals versus lists", as
>>
>>
>> List_infinite_bij_betw
>>
>> (NB: it holds for any infinite set, including the countably infinite ones.)
>
> Thanks for the pointer. This is what I need... I need to get better at
> finding existing theories :-)
>
> You define
> definition List :: "'a set => 'a list set"
> where "List A ≡ {l. set l ≤ A}"
>
> This is a definition that I could use in the development of Free Groups.
> Assuming I would not need the cardinality lemmas, what is the best
> practice: Importing your theory nevertheless, copying the definition or
> pushing to add this definition in a more standard, common place, i.e.
> HOL or HOL/Library?
>
> Greetings,
> Joachim
>

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