src/HOL/NatDef.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5187 55f07169cf5f
child 7872 2e2d7e80fb07
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 = WF +
    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
    43 
    44 
    45 (* abstract constants and syntax *)
    46 
    47 consts
    48   "0"       :: nat                ("0")
    49   Suc       :: nat => nat
    50   pred_nat  :: "(nat * nat) set"
    51 
    52 syntax
    53   "1"       :: nat                ("1")
    54   "2"       :: nat                ("2")
    55 
    56 translations
    57   "1"  == "Suc 0"
    58   "2"  == "Suc 1"
    59 
    60 
    61 local
    62 
    63 defs
    64   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    65   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    66 
    67   (*nat operations and recursion*)
    68   pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
    69 
    70   less_def      "m<n == (m,n):trancl(pred_nat)"
    71 
    72   le_def        "m<=(n::nat) == ~(n<m)"
    73 
    74 end