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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/OrderType.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     6
Order types.  
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     8
The order type of a well-ordering is the least ordinal isomorphic to it.
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     9
*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    11
OrderType = OrderArith + Ordinal + 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    12
consts
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
  ordermap  :: "[i,i]=>i"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
  ordertype :: "[i,i]=>i"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    15
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    16
rules
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    17
  ordermap_def
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
      "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    19
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    20
  ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    21
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
end