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.
I will add that equality.

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.