src/HOL/Nat.thy
author oheimb
Fri Dec 13 18:40:50 1996 +0100 (1996-12-13)
changeset 2393 651fce76c86c
parent 2258 8ad8ee759d9f
child 2541 70aa00ed3025
permissions -rw-r--r--
adaptions for symbol font
     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 syntax (symbols)
    65 
    66   "LEAST "	:: [idts, bool] => nat		("(3\\<mu>_./ _)" [0, 10] 10)
    67 *)
    68 
    69 defs
    70   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    71   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    72 
    73   (*nat operations and recursion*)
    74   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    75                                         & (!x. n=Suc x --> z=f(x))"
    76   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
    77 
    78   less_def      "m<n == (m,n):trancl(pred_nat)"
    79 
    80   le_def        "m<=(n::nat) == ~(n<m)"
    81 
    82   nat_rec_def   "nat_rec c d ==
    83                  wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    84   (*least number operator*)
    85   Least_def     "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
    86 
    87 end