src/ZF/OrderType.thy
author lcp
Tue, 12 Jul 1994 18:05:03 +0200
changeset 467 92868dab2939
parent 435 ca5356bd315a
child 753 ec86863e87c8
permissions -rw-r--r--
new cardinal arithmetic developments

(*  Title: 	ZF/OrderType.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Order types.  

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"

rules
  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"

end