src/HOL/Nat.thy
author clasohm
Wed Jun 21 15:47:10 1995 +0200 (1995-06-21)
changeset 1151 c820b3cc3df0
parent 972 e61b058d58d2
child 1370 7361ac9b024d
permissions -rw-r--r--
removed \...\ inside strings
     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 subtype (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 translations
    53   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    54 
    55 defs
    56   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    57   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    58 
    59   (*nat operations and recursion*)
    60   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    61                                         & (!x. n=Suc(x) --> z=f(x))"
    62   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    63 
    64   less_def "m<n == (m,n):trancl(pred_nat)"
    65 
    66   le_def   "m<=(n::nat) == ~(n<m)"
    67 
    68   nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
    69                         (nat_case (%g.c) (%m g.(d m (g m))))"
    70 end