Email Gateway (Aug 18 2022 at 14:52): Email Gateway (Aug 18 2022 at 14:52):From: Brian Huffman <brianh@cs.pdx.edu>
Hello all,
I have noticed some inconsistency and duplication in Isabelle's
standard libraries, as far as bijections to/from type nat are
concerned. Here is a list of the functions that I know about:
Library/Nat_Int_Bij.thy:
nat2_to_nat:: "(nat * nat) => nat"
nat_to_nat2:: "nat => (nat * nat)"
nat_to_int_bij :: "nat => int"
int_to_nat_bij :: "int => nat"
Library/Countable.thy:
pair_encode :: "nat * nat => nat"
nat_to_rat_surj :: "nat => rat" (* not injective; defined in terms
of nat_to_nat2 *)
HOLCF/NatIso.thy:
sum2nat :: "nat + nat => nat"
nat2sum :: "nat => nat + nat"
prod2nat :: "nat * nat => nat"
nat2prod :: "nat => nat * nat"
set2nat :: "nat set => nat" (* injective on the finite sets *)
nat2set :: "nat => nat set"
I would like to consolidate all these libraries and remove duplicate
functionality. (It turns out that prod2nat, pair_encode, and
nat2_to_nat are all equal as functions, even though they are defined
differently.) I would also like to come up with a consistent naming
scheme for the various functions and related lemmas.
Before doing anything, I'd like to get some input from the user
community. Who is using these libraries, and what are you using them
for? What kinds of function names do you like? What kinds of lemmas
about these functions do you need? Is there anything missing from
these libraries that you would like to have?
Thanks!
Email Gateway (Aug 18 2022 at 14:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Great!
I have only one comment: the standard naming scheme should be (as in
Isabelle/ML)
foo_of_bar :: bar =3D> foo
Cheers,
Florian
--=20
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de
signature.asc
Email Gateway (Aug 18 2022 at 14:52):From: Alexander Krauss <krauss@in.tum.de>
Florian Haftmann wrote:
I think this naming scheme would be inappropriate here, since it hints
at some kind of "obvious conversion". For example, the function
nat_to_int_bij is defined as
nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))
Naming it "int_of_nat" would be confusing IMO.
I added pair_encode together with class "countable" around 2007, not
knowing about the others. I think that function is only used to derive
the class instance, so it can safely be replaced by any other definition...
Other naming suggestions:
cantor_pair :: "nat * nat => nat"
cantor_unpair :: "nat => nat * nat"
(or cantor_split)
Alex
Email Gateway (Aug 18 2022 at 14:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I think this naming scheme would be inappropriate here, since it hints
at some kind of "obvious conversion".
of course you are right, I didn't full realize that we are taking about
Cantor here. Please ignore my suggestion.
there is also Library/Diagonalize.thy which has similar content
I have done this once. Either it should be integrated into the emerging
"Cantor toolbox" or been moved to ex/.
The main difference to other developments is that Diagonalize.thy avoids
choice.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 20:16 UTC