Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] proof assistant discussion on the Founations o...

Email Gateway (Aug 19 2022 at 13:58):

From: Andrei Popescu <uuomul@yahoo.com>
FYI

Andrei

Message: 1

Email Gateway (Aug 19 2022 at 13:58):

From: Gottfried Barrow <igbi@gmx.com>
Did I hear my name tangentially called? That is so unnecessary.

Without a doubt, a function, in which the domain is a set, must
foundationally be a set of ordered pairs. Here it is:

definition funS ::"('a => 'b) => 'a set => 'b set => ('a * 'b) set" where
"funS f D C == {(x,y). (!x. x : D --> f x : C) & x : D & y = f x}"

But HOL functions, as rules, are so much easier to work with, so here
are the rules:

definition funR :: "('a => 'b) => 'a set => 'b set => 'a => 'b" where
"funR f D C == (%x. if (!x. x : D --> f x : C) & x : D then f x else
uDf)"

definition funR_img :: "('a => 'b) => 'a set => 'a => 'b" where
"funR_img f D = (%x. if x : D then f x else uDf)"

The work comes from the fact that the image of the domain of a funR can
contain exactly one more element, uDf, than the range of funS. However,
when the codomain is the image of the domain, the image of funR and the
range of funS are equal.

The solutions in dealing with complexity lie in notation as much as in
logic, and notation happens to be one of Isar's strengths.

Do I hear a refrain? "Give me nested sets, give me nested sets..."

Was it not myself who posted a use of datatype_new for nested sets ,
even before datatype_new was released as part of Isabelle2013-1? Yes.
That was me. I remember. Not even vaguely.

Here is countably infinite nestable sets of reals, built from atoms,
where the UNIV of reals is, of course, uncountable:

datatype_new rD = rA real | rS "real cset"

Will it work out? That is not important.

What is a set? It is an abstract thought. The infrastructure for the
bulk of working with functions as sets, and working with nested sets, is
already in Fun.thy, Set.thy, and Finite_Set.thy.

It is the blurring of traditional thought. The convergence of ideas.

There is nothing left to do, other than several years of tedious work.

Please marvel at my innovative use of Isar notation in the attached
screen shot. I am a true artiste, as is possible for anyone who uses the
notational abilities of Isar.

Regards,
GB
funS_funR.png

Last updated: Apr 25 2024 at 08:20 UTC