src/HOL/NatDef.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10212 33fe2d701ddd
child 10832 e33b47e4246d
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatDef.thy
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     5
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     6
Definition of types ind and nat.
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     7
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     8
Type nat is defined as a set Nat over type ind.
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
     9
*)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    10
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 8943
diff changeset
    11
NatDef = Wellfounded_Recursion +
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    12
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    13
(** type ind **)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    14
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    15
global
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    16
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    17
types
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    18
  ind
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    19
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    20
arities
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    21
  ind :: term
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    22
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    23
consts
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    24
  Zero_Rep      :: ind
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    25
  Suc_Rep       :: ind => ind
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    26
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    27
rules
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    28
  (*the axiom of infinity in 2 parts*)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    29
  inj_Suc_Rep           "inj(Suc_Rep)"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    30
  Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    31
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    32
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    33
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    34
(** type nat **)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    35
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    36
(* type definition *)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    37
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    38
typedef (Nat)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    39
  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    40
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    41
instance
8943
a4f8be72f585 now 0 is overloaded
paulson
parents: 7872
diff changeset
    42
  nat :: {ord, zero}
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    43
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    44
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    45
(* abstract constants and syntax *)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    46
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    47
consts
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    48
  Suc       :: nat => nat
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    49
  pred_nat  :: "(nat * nat) set"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    50
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    51
syntax
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    52
  "1"       :: nat                ("1")
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    53
  "2"       :: nat                ("2")
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    54
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    55
translations
5187
55f07169cf5f Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents: 3947
diff changeset
    56
  "1"  == "Suc 0"
55f07169cf5f Removed nat_case, nat_rec, and natE (now provided by datatype
berghofe
parents: 3947
diff changeset
    57
  "2"  == "Suc 1"
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    58
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    59
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    60
local
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    61
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    62
defs
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    63
  Zero_def      "0 == Abs_Nat(Zero_Rep)"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    64
  Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    65
7872
2e2d7e80fb07 Removed obsolete comment.
berghofe
parents: 5187
diff changeset
    66
  (*nat operations*)
3236
882e125ed7da New pattern-matching definition of pred_nat
paulson
parents: 2608
diff changeset
    67
  pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    68
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    69
  less_def      "m<n == (m,n):trancl(pred_nat)"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    70
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    71
  le_def        "m<=(n::nat) == ~(n<m)"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    72
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents:
diff changeset
    73
end