author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
permissions | -rw-r--r-- |
515 | 1 |
(* Title: ZF/ex/Brouwer.thy |
2 |
ID: $ $ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
528
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
6 |
Infinite branching datatype definitions |
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
7 |
(1) the Brouwer ordinals |
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
8 |
(2) the Martin-Löf wellordering type |
515 | 9 |
*) |
10 |
||
11 |
Brouwer = InfDatatype + |
|
12 |
consts |
|
1401 | 13 |
brouwer :: i |
14 |
Well :: [i,i=>i]=>i |
|
515 | 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 |
||
528
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
21 |
(*The union with nat ensures that the cardinal is infinite*) |
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
22 |
datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))" |
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
23 |
"Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)") |
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
24 |
monos "[Pi_mono]" |
1155 | 25 |
type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans] |
26 |
@ inf_datatype_intrs" |
|
528
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
27 |
|
61dc99226f8f
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp
parents:
515
diff
changeset
|
28 |
|
515 | 29 |
end |