src/ZF/ex/Brouwer.thy
author lcp
Mon Aug 15 18:37:25 1994 +0200 (1994-08-15)
changeset 528 61dc99226f8f
parent 515 abcc438e7c27
child 1155 928a16e02f9f
permissions -rw-r--r--
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp@515
     1
(*  Title: 	ZF/ex/Brouwer.thy
lcp@515
     2
    ID:         $ $
lcp@515
     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
lcp@515
    13
  brouwer :: "i"
lcp@528
    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")
lcp@515
    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)")
lcp@528
    24
  monos	      "[Pi_mono]"
lcp@528
    25
  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   \
lcp@528
    26
\	       @ inf_datatype_intrs"
lcp@528
    27
lcp@528
    28
lcp@515
    29
end