src/HOL/NatDef.thy
author nipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 10212 33fe2d701ddd
parent 8943 a4f8be72f585
child 10832 e33b47e4246d
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/NatDef.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Definition of types ind and nat.
     7 
     8 Type nat is defined as a set Nat over type ind.
     9 *)
    10 
    11 NatDef = Wellfounded_Recursion +
    12 
    13 (** type ind **)
    14 
    15 global
    16 
    17 types
    18   ind
    19 
    20 arities
    21   ind :: term
    22 
    23 consts
    24   Zero_Rep      :: ind
    25   Suc_Rep       :: ind => ind
    26 
    27 rules
    28   (*the axiom of infinity in 2 parts*)
    29   inj_Suc_Rep           "inj(Suc_Rep)"
    30   Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
    31 
    32 
    33 
    34 (** type nat **)
    35 
    36 (* type definition *)
    37 
    38 typedef (Nat)
    39   nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    40 
    41 instance
    42   nat :: {ord, zero}
    43 
    44 
    45 (* abstract constants and syntax *)
    46 
    47 consts
    48   Suc       :: nat => nat
    49   pred_nat  :: "(nat * nat) set"
    50 
    51 syntax
    52   "1"       :: nat                ("1")
    53   "2"       :: nat                ("2")
    54 
    55 translations
    56   "1"  == "Suc 0"
    57   "2"  == "Suc 1"
    58 
    59 
    60 local
    61 
    62 defs
    63   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    64   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    65 
    66   (*nat operations*)
    67   pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
    68 
    69   less_def      "m<n == (m,n):trancl(pred_nat)"
    70 
    71   le_def        "m<=(n::nat) == ~(n<m)"
    72 
    73 end