src/HOL/NatDef.thy
author wenzelm
Mon Oct 20 11:25:39 1997 +0200 (1997-10-20)
changeset 3947 eb707467f8c5
parent 3842 b55686a7b22c
child 5187 55f07169cf5f
permissions -rw-r--r--
adapted to qualified names;
nipkow@2608
     1
(*  Title:      HOL/NatDef.thy
nipkow@2608
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
nipkow@2608
     4
    Copyright   1991  University of Cambridge
nipkow@2608
     5
nipkow@2608
     6
Definition of types ind and nat.
nipkow@2608
     7
nipkow@2608
     8
Type nat is defined as a set Nat over type ind.
nipkow@2608
     9
*)
nipkow@2608
    10
nipkow@2608
    11
NatDef = WF +
nipkow@2608
    12
nipkow@2608
    13
(** type ind **)
nipkow@2608
    14
wenzelm@3947
    15
global
wenzelm@3947
    16
nipkow@2608
    17
types
nipkow@2608
    18
  ind
nipkow@2608
    19
nipkow@2608
    20
arities
nipkow@2608
    21
  ind :: term
nipkow@2608
    22
nipkow@2608
    23
consts
nipkow@2608
    24
  Zero_Rep      :: ind
nipkow@2608
    25
  Suc_Rep       :: ind => ind
nipkow@2608
    26
nipkow@2608
    27
rules
nipkow@2608
    28
  (*the axiom of infinity in 2 parts*)
nipkow@2608
    29
  inj_Suc_Rep           "inj(Suc_Rep)"
nipkow@2608
    30
  Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
nipkow@2608
    31
nipkow@2608
    32
nipkow@2608
    33
nipkow@2608
    34
(** type nat **)
nipkow@2608
    35
nipkow@2608
    36
(* type definition *)
nipkow@2608
    37
nipkow@2608
    38
typedef (Nat)
nipkow@2608
    39
  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
nipkow@2608
    40
nipkow@2608
    41
instance
nipkow@2608
    42
  nat :: ord
nipkow@2608
    43
nipkow@2608
    44
nipkow@2608
    45
(* abstract constants and syntax *)
nipkow@2608
    46
nipkow@2608
    47
consts
nipkow@2608
    48
  "0"       :: nat                ("0")
nipkow@2608
    49
  Suc       :: nat => nat
nipkow@2608
    50
  nat_case  :: ['a, nat => 'a, nat] => 'a
nipkow@2608
    51
  pred_nat  :: "(nat * nat) set"
nipkow@2608
    52
  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
nipkow@2608
    53
nipkow@2608
    54
syntax
nipkow@2608
    55
  "1"       :: nat                ("1")
nipkow@2608
    56
  "2"       :: nat                ("2")
nipkow@2608
    57
nipkow@2608
    58
translations
nipkow@2608
    59
   "1"  == "Suc 0"
nipkow@2608
    60
   "2"  == "Suc 1"
wenzelm@3842
    61
  "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
nipkow@2608
    62
nipkow@2608
    63
wenzelm@3947
    64
local
wenzelm@3947
    65
nipkow@2608
    66
defs
nipkow@2608
    67
  Zero_def      "0 == Abs_Nat(Zero_Rep)"
nipkow@2608
    68
  Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
nipkow@2608
    69
nipkow@2608
    70
  (*nat operations and recursion*)
nipkow@2608
    71
  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
nipkow@2608
    72
                                        & (!x. n=Suc x --> z=f(x))"
paulson@3236
    73
  pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
nipkow@2608
    74
nipkow@2608
    75
  less_def      "m<n == (m,n):trancl(pred_nat)"
nipkow@2608
    76
nipkow@2608
    77
  le_def        "m<=(n::nat) == ~(n<m)"
nipkow@2608
    78
nipkow@2608
    79
  nat_rec_def   "nat_rec c d ==
nipkow@2608
    80
                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
nipkow@2608
    81
end