src/HOL/Nat.thy
author paulson
Tue Mar 05 15:55:15 1996 +0100 (1996-03-05)
changeset 1540 eacaa07e9078
parent 1531 e5eb247ad13c
child 1625 40501958d0f6
permissions -rw-r--r--
Converted TABs to spaces
     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   :: [nat, 'a, [nat, 'a] => 'a] => 'a
    51 
    52   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    53 
    54 translations
    55   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    56 
    57 defs
    58   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    59   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    60 
    61   (*nat operations and recursion*)
    62   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    63                                         & (!x. n=Suc(x) --> z=f(x))"
    64   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    65 
    66   less_def      "m<n == (m,n):trancl(pred_nat)"
    67 
    68   le_def        "m<=(n::nat) == ~(n<m)"
    69 
    70   nat_rec_def   "nat_rec n c d ==
    71                  wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    72   (*least number operator*)
    73   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    74 
    75 end