src/ZF/ex/Brouwer.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
permissions -rw-r--r--
expanded tabs
     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