Re: [isabelle] bijections to/from the natural numbers



Florian Haftmann wrote:
I have only one comment: the standard naming scheme should be (as in
Isabelle/ML)

  foo_of_bar :: bar => foo

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





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