src/ZF/ex/Brouwer.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 528 61dc99226f8f
child 1155 928a16e02f9f
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/Brouwer.thy
     2     ID:         $ $
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Infinite branching datatype definitions
     7   (1) the Brouwer ordinals
     8   (2) the Martin-Löf wellordering type
     9 *)
    10 
    11 Brouwer = InfDatatype +
    12 consts
    13   brouwer :: "i"
    14   Well    :: "[i,i=>i]=>i"
    15  
    16 datatype <= "Vfrom(0, csucc(nat))"
    17   "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
    18   monos	      "[Pi_mono]"
    19   type_intrs  "inf_datatype_intrs"
    20 
    21 (*The union with nat ensures that the cardinal is infinite*)
    22 datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
    23   "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
    24   monos	      "[Pi_mono]"
    25   type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   \
    26 \	       @ inf_datatype_intrs"
    27 
    28 
    29 end