Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/OrderType.thy
author clasohm
Thu, 23 Mar 1995 15:39:13 +0100
changeset 971 f4815812665b
parent 850 a744f9749885
child 1033 437728256de3
permissions -rw-r--r--
fixed bug: parent theory wasn't loaded if .thy file was completly read before (regardless of the .ML file)

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

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)
 

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

  (*ordinal addition*)
  oadd_def      "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"

end
isabelle