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



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

-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de










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