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