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
clasohm@923
     1
(*  Title:      HOL/Nat.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1991  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Definition of types ind and nat.
clasohm@923
     7
clasohm@923
     8
Type nat is defined as a set Nat over type ind.
clasohm@923
     9
*)
clasohm@923
    10
clasohm@923
    11
Nat = WF +
clasohm@923
    12
clasohm@923
    13
(** type ind **)
clasohm@923
    14
clasohm@923
    15
types
clasohm@923
    16
  ind
clasohm@923
    17
clasohm@923
    18
arities
clasohm@923
    19
  ind :: term
clasohm@923
    20
clasohm@923
    21
consts
clasohm@1370
    22
  Zero_Rep      :: ind
clasohm@1370
    23
  Suc_Rep       :: ind => ind
clasohm@923
    24
clasohm@923
    25
rules
clasohm@923
    26
  (*the axiom of infinity in 2 parts*)
clasohm@923
    27
  inj_Suc_Rep           "inj(Suc_Rep)"
clasohm@923
    28
  Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
clasohm@923
    29
clasohm@923
    30
clasohm@923
    31
clasohm@923
    32
(** type nat **)
clasohm@923
    33
clasohm@923
    34
(* type definition *)
clasohm@923
    35
clasohm@1475
    36
typedef (Nat)
clasohm@923
    37
  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
clasohm@923
    38
clasohm@923
    39
instance
clasohm@923
    40
  nat :: ord
clasohm@923
    41
clasohm@923
    42
clasohm@923
    43
(* abstract constants and syntax *)
clasohm@923
    44
clasohm@923
    45
consts
nipkow@1531
    46
  "0"       :: nat                ("0")
nipkow@1531
    47
  Suc       :: nat => nat
nipkow@1531
    48
  nat_case  :: ['a, nat => 'a, nat] => 'a
nipkow@1531
    49
  pred_nat  :: "(nat * nat) set"
berghofe@1824
    50
  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
nipkow@1531
    51
nipkow@1531
    52
  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
clasohm@923
    53
wenzelm@2258
    54
syntax
wenzelm@2258
    55
  "1"       :: nat                ("1")
wenzelm@2258
    56
  "2"       :: nat                ("2")
wenzelm@2258
    57
clasohm@923
    58
translations
oheimb@2393
    59
   "1"  == "Suc 0"
oheimb@2393
    60
   "2"  == "Suc 1"
oheimb@2393
    61
  "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
oheimb@2393
    62
oheimb@2393
    63
(*
oheimb@2393
    64
syntax (symbols)
oheimb@2393
    65
oheimb@2393
    66
  "LEAST "	:: [idts, bool] => nat		("(3\\<mu>_./ _)" [0, 10] 10)
oheimb@2393
    67
*)
clasohm@923
    68
clasohm@923
    69
defs
clasohm@923
    70
  Zero_def      "0 == Abs_Nat(Zero_Rep)"
clasohm@923
    71
  Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
clasohm@923
    72
clasohm@923
    73
  (*nat operations and recursion*)
clasohm@1151
    74
  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
oheimb@2393
    75
                                        & (!x. n=Suc x --> z=f(x))"
oheimb@2393
    76
  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
clasohm@923
    77
nipkow@1531
    78
  less_def      "m<n == (m,n):trancl(pred_nat)"
nipkow@1531
    79
nipkow@1531
    80
  le_def        "m<=(n::nat) == ~(n<m)"
clasohm@923
    81
berghofe@1824
    82
  nat_rec_def   "nat_rec c d ==
berghofe@1824
    83
                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
nipkow@1531
    84
  (*least number operator*)
oheimb@2393
    85
  Least_def     "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
oheimb@1660
    86
clasohm@923
    87
end