src/ZF/OrderType.thy
 author lcp Thu, 13 Apr 1995 11:33:57 +0200 changeset 1033 437728256de3 parent 850 a744f9749885 child 1401 0c439768f45c permissions -rw-r--r--
Defined ordinal difference, --
```
(*  Title: 	ZF/OrderType.thy
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Order types and ordinal arithmetic.

The order type of a well-ordering is the least ordinal isomorphic to it.
*)

OrderType = OrderArith + Ordinal +
consts
ordermap  :: "[i,i]=>i"
ordertype :: "[i,i]=>i"

Ord_alt   :: "i => o"

"**"      :: "[i,i]=>i"           (infixl 70)
"++"      :: "[i,i]=>i"           (infixl 65)
"--"      :: "[i,i]=>i"           (infixl 65)

defs
ordermap_def
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"

ordertype_def "ordertype(A,r) == ordermap(A,r)``A"

Ord_alt_def    (*alternative definition of ordinal numbers*)
"Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"

(*ordinal multiplication*)
omult_def     "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"