Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 15:55):

From: Joachim Breitner <mail@joachim-breitner.de>
Hi Andrei,

just FYI: I finished my results using your theory and committed my
changes to the AFP mercurial repository. Thanks, it was exactly what I
was expecting.

In case you update your AFP entry to use List.lists instead of your own
List definition, my theory will probably not compile any more. You can
fix that by removing the lines:

moreover (* Remove this if Ordinals_and_Cardinals uses List.lists as well *)
have "|lists ((UNIV::bool set)\<times>X)| = |List ((UNIV::bool set)\<times>X)|"
by (simp add: List_def lists_eq_set)

from Free-Groups/Isomorphisms.thy

Also, it would be nice if the transitivity rules for <o, <=o, =o were
set up to work with Isar’s "also... also... finally". This would make my
lemma "free_group_card_infinite" a bit more straight-forward to
implement... but no big deal.

Thanks for your theory!
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:56):

From: Andrei Popescu <uuomul@yahoo.com>
Dear Joachim,

just FYI: I finished my results using your theory and committed my
changes to the AFP mercurial repository. Thanks, it was exactly what I
was expecting.

I am glad you found it useful. This was precisely the intended target:
the "working" mathematics, needing only basic cardinality results.

In case you update your AFP entry to use List.lists instead of your own
List definition,

Yes, I will soon.

Best regards,
Andrei

----- Original Message ----
From: Joachim Breitner <mail@joachim-breitner.de>
To: Andrei Popescu <uuomul@yahoo.com>
Cc: cl-isabelle-users@lists.cam.ac.uk
Sent: Wed, September 22, 2010 2:56:48 AM
Subject: Re: FuncSet without extensional? (Joachim Breitner)

Hi 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.)

just FYI: I finished my results using your theory and committed my
changes to the AFP mercurial repository. Thanks, it was exactly what I
was expecting.

In case you update your AFP entry to use List.lists instead of your own
List definition, my theory will probably not compile any more. You can
fix that by removing the lines:

moreover (* Remove this if Ordinals_and_Cardinals uses List.lists as well *)
have "|lists ((UNIV::bool set)\<times>X)| = |List ((UNIV::bool set)\<times>X)|"
by (simp add: List_def lists_eq_set)

from Free-Groups/Isomorphisms.thy

Also, it would be nice if the transitivity rules for <o, <=o, =o were
set up to work with Isar’s "also... also... finally". This would make my
lemma "free_group_card_infinite" a bit more straight-forward to
implement... but no big deal.

Thanks for your theory!
Joachim

view this post on Zulip Email Gateway (Aug 18 2022 at 16:09):

From: Andrei Popescu <uuomul@yahoo.com>
Hi Joachim,

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.)

Best regards,
Andrei

view this post on Zulip Email Gateway (Aug 18 2022 at 16:09):

From: Joachim Breitner <mail@joachim-breitner.de>
Dear Andrei,

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
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:09):

From: Andrei Popescu <uuomul@yahoo.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:09):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

Last updated: Apr 25 2024 at 20:15 UTC