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
clasohm@1478
     1
(*  Title:      ZF/ex/Brouwer.thy
lcp@515
     2
    ID:         $ $
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@528
     6
Infinite branching datatype definitions
lcp@528
     7
  (1) the Brouwer ordinals
lcp@528
     8
  (2) the Martin-Löf wellordering type
lcp@515
     9
*)
lcp@515
    10
lcp@515
    11
Brouwer = InfDatatype +
lcp@515
    12
consts
clasohm@1401
    13
  brouwer :: i
clasohm@1401
    14
  Well    :: [i,i=>i]=>i
lcp@515
    15
 
lcp@515
    16
datatype <= "Vfrom(0, csucc(nat))"
lcp@515
    17
  "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
clasohm@1478
    18
  monos       "[Pi_mono]"
lcp@515
    19
  type_intrs  "inf_datatype_intrs"
lcp@515
    20
lcp@528
    21
(*The union with nat ensures that the cardinal is infinite*)
lcp@528
    22
datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
lcp@528
    23
  "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
clasohm@1478
    24
  monos       "[Pi_mono]"
clasohm@1155
    25
  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
clasohm@1478
    26
               @ inf_datatype_intrs"
lcp@528
    27
lcp@528
    28
lcp@515
    29
end