src/ZF/ex/Brouwer.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     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