src/ZF/OrderType.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/OrderType.thy
lcp@435
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     4
    Copyright   1994  University of Cambridge
lcp@435
     5
lcp@850
     6
Order types and ordinal arithmetic.
lcp@435
     7
lcp@435
     8
The order type of a well-ordering is the least ordinal isomorphic to it.
lcp@435
     9
*)
lcp@435
    10
lcp@467
    11
OrderType = OrderArith + Ordinal + 
lcp@435
    12
consts
clasohm@1401
    13
  ordermap  :: [i,i]=>i
clasohm@1401
    14
  ordertype :: [i,i]=>i
lcp@435
    15
clasohm@1401
    16
  Ord_alt   :: i => o   
lcp@850
    17
clasohm@1401
    18
  "**"      :: [i,i]=>i           (infixl 70)
clasohm@1401
    19
  "++"      :: [i,i]=>i           (infixl 65)
clasohm@1401
    20
  "--"      :: [i,i]=>i           (infixl 65)
lcp@850
    21
 
lcp@850
    22
lcp@753
    23
defs
lcp@435
    24
  ordermap_def
lcp@435
    25
      "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
lcp@435
    26
lcp@435
    27
  ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
lcp@435
    28
lcp@850
    29
  Ord_alt_def    (*alternative definition of ordinal numbers*)
lcp@850
    30
  "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
lcp@850
    31
  
lcp@850
    32
  (*ordinal multiplication*)
lcp@850
    33
  omult_def     "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
lcp@850
    34
lcp@850
    35
  (*ordinal addition*)
lcp@850
    36
  oadd_def      "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
lcp@850
    37
lcp@1033
    38
  (*ordinal subtraction*)
lcp@1033
    39
  odiff_def     "i -- j == ordertype(i-j, Memrel(i))"
lcp@1033
    40
lcp@435
    41
end