Robert Soeldner (Oct 21 2022 at 15:33): Robert Soeldner (Oct 21 2022 at 15:33):If from_nat is restricted to the same type, shouldn't this behave as the identity?
lemma ‹to_nat ((from_nat x) :: nat) = (x :: nat)›
sorry
I don't think this holds.
to_nat is defined as to_nat = (SOME f. inj f)", i.e. some arbitrary injection embedding the elements of a type into nat. from_nat is just the inverse of to_nat. Even if you restrict yourself to going from nat to nat, to_nat could still happen to be for example (λn :: nat . 2*n). Then from_nat 3 would be undefined for example.
Manuel Eberl (Oct 21 2022 at 16:37):No. to_nat :: 'a :: countable ⇒ nat is defined via the choice operator as ‘some injective function from 'a to nat’. It is not required to be bijective (that would only work for countably infinite types, but we only assumed countable).
Now, because of that, even to_nat :: nat ⇒ nat can only be assumed to be injective, but not surjective. So there can be natural numbers x that are not in the range of to_nat, and for those your statement clearly cannot hold.
Manuel Eberl (Oct 21 2022 at 16:39):Note that the to_nat_on function from HOL-Library.Countable_Set indeed provides a bijection, not just an injection.
Last updated: Apr 24 2024 at 08:20 UTC