Search code examples
isabelle

What is `ind` type in Isabelle

In Isabelle natural numbers are defined as follows

typedecl ind

axiomatization Zero_Rep :: ind and Suc_Rep :: "ind ⇒ ind"
  ― ‹The axiom of infinity in 2 parts:›
  where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y ⟹ x = y"
    and Suc_Rep_not_Zero_Rep: "Suc_Rep x ≠ Zero_Rep"


subsection ‹Type nat›

text ‹Type definition›

inductive Nat :: "ind ⇒ bool"
  where
    Zero_RepI: "Nat Zero_Rep"
  | Suc_RepI: "Nat i ⟹ Nat (Suc_Rep i)"

That's a lot of code to write what's effectively just

datatype nat = Zero | Suc nat

Is there some greater purpose to ind or maybe it is there just for historical reasons?

Solution

  • The datatype package needs a whole lot of maths to do all those internal constructions that are required to give you the datatype you want in the end. In particular, it needs natural numbers.

    So the reason why the datatype package is not used to define the naturals is that it simply isn't available yet at that point.

    One could of course just axiomatise the nat type directly. I think the idea to instead axiomatise some infinite type and then carve the naturals out of that is a standard one, I think it is done similarly in Zermelo–Fraenkel logic.

    Side note: In fact one could even make the datatype package itself axiomatic. But the common philosophy in interactive theorem provers, especially in the LCF family, is to work from a small set of axioms and that everything that can be constructed should be constructed instead of axiomatised. This reduces the amount of "trusted code".

    A direct axiomatisation of the natural numbers would not be very controversial I think, but for something as complicated as the datatype package an axiomatic implementation would h introduce lots of possibilities for subtle soundness bugs.