src/HOL/Nat.thy
author wenzelm
Thu Jan 23 12:55:31 1997 +0100 (1997-01-23)
changeset 2541 70aa00ed3025
parent 2393 651fce76c86c
child 2608 450c9b682a92
permissions -rw-r--r--
removed \<mu> syntax;
     1 (*  Title:      HOL/Nat.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 Nat = WF +
    12 
    13 (** type ind **)
    14 
    15 types
    16   ind
    17 
    18 arities
    19   ind :: term
    20 
    21 consts
    22   Zero_Rep      :: ind
    23   Suc_Rep       :: ind => ind
    24 
    25 rules
    26   (*the axiom of infinity in 2 parts*)
    27   inj_Suc_Rep           "inj(Suc_Rep)"
    28   Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
    29 
    30 
    31 
    32 (** type nat **)
    33 
    34 (* type definition *)
    35 
    36 typedef (Nat)
    37   nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    38 
    39 instance
    40   nat :: ord
    41 
    42 
    43 (* abstract constants and syntax *)
    44 
    45 consts
    46   "0"       :: nat                ("0")
    47   Suc       :: nat => nat
    48   nat_case  :: ['a, nat => 'a, nat] => 'a
    49   pred_nat  :: "(nat * nat) set"
    50   nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
    51 
    52   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    53 
    54 syntax
    55   "1"       :: nat                ("1")
    56   "2"       :: nat                ("2")
    57 
    58 translations
    59    "1"  == "Suc 0"
    60    "2"  == "Suc 1"
    61   "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
    62 
    63 
    64 defs
    65   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    66   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    67 
    68   (*nat operations and recursion*)
    69   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    70                                         & (!x. n=Suc x --> z=f(x))"
    71   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
    72 
    73   less_def      "m<n == (m,n):trancl(pred_nat)"
    74 
    75   le_def        "m<=(n::nat) == ~(n<m)"
    76 
    77   nat_rec_def   "nat_rec c d ==
    78                  wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    79   (*least number operator*)
    80   Least_def     "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
    81 
    82 end