[isabelle] bijections to/from the natural numbers



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!
- Brian





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