isabelle: src/ZF/ex/Brouwer.thy@6acf3ff0f486 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/ex/Brouwer.thy
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $ $
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	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 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	9	*)
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	10
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	11	Brouwer = InfDatatype +
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	12	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	13	brouwer :: i
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	14	Well :: [i,i=>i]=>i
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	15
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	16	datatype <= "Vfrom(0, csucc(nat))"
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	17	"brouwer" = Zero \| Suc ("b: brouwer") \| Lim ("h: nat -> brouwer")
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	18	monos "[Pi_mono]"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	19	type_intrs "inf_datatype_intrs"
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	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)")
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	24	monos "[Pi_mono]"
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 528 diff changeset	25	type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	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 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	29	end

author	nipkow
	Thu, 26 Nov 1998 12:18:08 +0100
changeset 5974	6acf3ff0f486
parent 1478	2b8c2a7547ab
child 6117	f9aad8ccd590
permissions	-rw-r--r--