author  wenzelm 
Sat, 07 Oct 2017 15:21:25 +0200  
changeset 66778  cf0187ca3a57 
parent 66750  41fbe4a3aac9 
child 66946  3d8fd98c7c86 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50574
diff
changeset

1 
chapter ZF 
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50574
diff
changeset

2 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

3 
session ZF (main timing) = Pure + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

4 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

5 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

6 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

7 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

8 
ZermeloFraenkel Set Theory. This theory is the work of Martin Coen, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

9 
Philippe Noel and Lawrence Paulson. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

10 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

11 
Isabelle/ZF formalizes the greater part of elementary set theory, including 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

12 
relations, functions, injections, surjections, ordinals and cardinals. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

13 
Results proved include Cantor's Theorem, the Recursion Theorem, the 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

14 
SchroederBernstein Theorem, and (assuming AC) the Wellordering Theorem. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

15 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

16 
Isabelle/ZF also provides theories of lists, trees, etc., for formalizing 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

17 
computational notions. It supports inductive definitions of 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

18 
infinitebranching trees for any cardinality of branching. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

19 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

20 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

21 
Useful references for Isabelle/ZF: 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

22 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

23 
Lawrence C. Paulson, Set theory for verification: I. From foundations to 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

24 
functions. J. Automated Reasoning 11 (1993), 353389. 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

25 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

26 
Lawrence C. Paulson, Set theory for verification: II. Induction and 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

27 
recursion. Report 312, Computer Lab (1993). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

28 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

29 
Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

30 
definitions. In: A. Bundy (editor), CADE12: 12th International 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

31 
Conference on Automated Deduction, (Springer LNAI 814, 1994), 148161. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

32 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

33 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

34 
Useful references on ZF set theory: 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

35 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

36 
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

37 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

38 
Patrick Suppes, Axiomatic Set Theory (Dover, 1972) 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

39 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

40 
Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979) 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

41 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

42 
Kenneth Kunen, Set Theory: An Introduction to Independence Proofs, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

43 
(NorthHolland, 1980) 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

44 
*} 
66444  45 
sessions 
46 
FOL 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

47 
theories 
65527  48 
ZF (global) 
49 
ZFC (global) 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
51403
diff
changeset

50 
document_files "root.tex" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

51 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

52 
session "ZFAC" in AC = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

53 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

54 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

55 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

56 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

57 
Proofs of ACequivalences, due to Krzysztof Grabczewski. 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

58 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

59 
See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

60 
J.E. Rubin, 1985. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

61 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

62 
The report 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

63 
http://www.cl.cam.ac.uk/Research/Reports/TR377lcpmechanisingsettheory.ps.gz 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

64 
"Mechanizing Set Theory", by Paulson and Grabczewski, describes both this 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

65 
development and ZF's theories of cardinals. 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

66 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

67 
theories 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

68 
WO6_WO1 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

69 
WO1_WO7 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

70 
AC7_AC9 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

71 
WO1_AC 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

72 
AC15_WO6 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

73 
WO2_AC16 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

74 
AC16_WO4 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

75 
AC17_AC1 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

76 
AC18_AC19 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

77 
DC 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
51403
diff
changeset

78 
document_files "root.tex" "root.bib" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

79 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

80 
session "ZFCoind" in Coind = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

81 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

82 
Author: Jacob Frost, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

83 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

84 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

85 
Coind  A Coinduction Example. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

86 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

87 
It involves proving the consistency of the dynamic and static semantics for 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

88 
a small functional language. A codatatype definition specifies values and 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

89 
value environments in mutual recursion: nonwellfounded values represent 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

90 
recursive functions; value environments are variant functions from 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

91 
variables into values. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

92 

48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

93 
Based upon the article 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

94 
Robin Milner and Mads Tofte, 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

95 
Coinduction in Relational Semantics, 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

96 
Theoretical Computer Science 87 (1991), pages 209220. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

97 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

98 
Written up as 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

99 
Jacob Frost, A Case Study of Co_induction in Isabelle 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

100 
Report, Computer Lab, University of Cambridge (1995). 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

101 
http://www.cl.cam.ac.uk/Research/Reports/TR359jf10008coinductioninisabelle.dvi.gz 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

102 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

103 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

104 
theories ECR 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

105 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

106 
session "ZFConstructible" in Constructible = ZF + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

107 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

108 
Relative Consistency of the Axiom of Choice: 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

109 
Inner Models, Absoluteness and Consistency Proofs. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

110 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

111 
GÃ¶del's proof of the relative consistency of the axiom of choice is 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

112 
mechanized using Isabelle/ZF. The proof builds upon a previous 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

113 
mechanization of the reflection theorem (see 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

114 
http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

115 
reliance on metatheory in the original proof makes the formalization 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

116 
unusually long, and not entirely satisfactory: two parts of the proof do 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

117 
not fit together. It seems impossible to solve these problems without 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

118 
formalizing the metatheory. However, the present development follows a 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

119 
standard textbook, Kunen's Set Theory, and could support the formalization 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

120 
of further material from that book. It also serves as an example of what to 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

121 
expect when deep mathematics is formalized. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

122 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

123 
A paper describing this development is 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

124 
http://www.cl.cam.ac.uk/TechReports/UCAMCLTR551.pdf 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

125 
*} 
59446  126 
theories 
127 
DPow_absolute 

128 
AC_in_L 

129 
Rank_Separation 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
51403
diff
changeset

130 
document_files "root.tex" "root.bib" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

131 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

132 
session "ZFIMP" in IMP = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

133 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

134 
Author: Heiko Loetzbeyer & Robert Sandner, TUM 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

135 
Copyright 1994 TUM 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

136 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

137 
Formalization of the denotational and operational semantics of a 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

138 
simple whilelanguage, including an equivalence proof. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

139 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

140 
The whole development essentially formalizes/transcribes 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

141 
chapters 2 and 5 of 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

142 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

143 
Glynn Winskel. The Formal Semantics of Programming Languages. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

144 
MIT Press, 1993. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

145 
*} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

146 
theories Equiv 
66750  147 
document_files 
148 
"root.tex" 

149 
"root.bib" 

48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

150 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

151 
session "ZFInduct" in Induct = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

152 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

153 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

154 
Copyright 2001 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

155 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

156 
Inductive definitions. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

157 
*} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

158 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

159 
(** Datatypes **) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

160 
Datatypes (*sample datatypes*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

161 
Binary_Trees (*binary trees*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

162 
Term (*recursion over the list functor*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

163 
Ntree (*variablebranching trees; function demo*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

164 
Tree_Forest (*mutual recursion*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

165 
Brouwer (*Infinitebranching trees*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

166 
Mutil (*mutilated chess board*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

167 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

168 
(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

169 
finite sets*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

170 
Multiset 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

171 
Rmap (*mapping a relation over a list*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

172 
PropLog (*completeness of propositional logic*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

173 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

174 
(*two Coq examples by Christine PaulinMohring*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

175 
ListN 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

176 
Acc 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

177 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

178 
Comb (*Combinatory Logic example*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

179 
Primrec (*Primitive recursive functions*) 
58623  180 
document_files 
181 
"root.bib" 

182 
"root.tex" 

48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

183 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

184 
session "ZFResid" in Resid = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

185 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

186 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

187 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

188 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

189 
Residuals  a proof of the ChurchRosser Theorem for the 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

190 
untyped lambdacalculus. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

191 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

192 
By Ole Rasmussen, following the Coq proof given in 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

193 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

194 
Gerard Huet. Residual Theory in LambdaCalculus: A Formal Development. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

195 
J. Functional Programming 4(3) 1994, 371394. 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

196 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

197 
See Rasmussen's report: The ChurchRosser Theorem in Isabelle: A Proof 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

198 
Porting Experiment. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

199 
http://www.cl.cam.ac.uk/ftp/papers/reports/TR364or200churchrosserisabelle.ps.gz 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

200 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

201 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

202 
theories Confluence 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

203 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

204 
session "ZFUNITY" (timing) in UNITY = "ZFInduct" + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

205 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

206 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

207 
Copyright 1998 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

208 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

209 
ZF/UNITY proofs. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

210 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

211 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

212 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

213 
(*Simple examples: no composition*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

214 
Mutex 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

215 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

216 
(*Basic metatheory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

217 
Guar 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

218 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

219 
(*Prefix relation; the Allocator example*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

220 
Distributor Merge ClientImpl AllocImpl 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

221 

66778
cf0187ca3a57
discontinued somewhat pointless session group: g ZF may be replaced by D ~~/src/ZF;
wenzelm
parents:
66750
diff
changeset

222 
session "ZFex" in ex = ZF + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

223 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

224 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

225 
Copyright 1993 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

226 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

227 
Miscellaneous examples for ZermeloFraenkel Set Theory. 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

228 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

229 
Includes a simple form of Ramsey's theorem. A report is available: 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

230 
http://www.cl.cam.ac.uk/Research/Reports/TR271lcpsettheory.dvi.Z 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

231 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

232 
Several (co)inductive and (co)datatype definitions are presented. The 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

233 
report http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

234 
describes the theoretical foundations of datatypes while 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

235 
href="http://www.cl.cam.ac.uk/Research/Reports/TR320lcpisabelleinddefs.dvi.gz 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

236 
describes the package that automates their declaration. 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

237 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

238 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

239 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

240 
misc 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

241 
Ring (*abstract algebra*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

242 
Commutation (*abstract ChurchRosser theory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

243 
Primes (*GCD theory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

244 
NatSum (*Summing integers, squares, cubes, etc.*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

245 
Ramsey (*Simple form of Ramsey's theorem*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

246 
Limit (*Inverse limit construction of domains*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

247 
BinEx (*Binary integer arithmetic*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

248 
LList CoUnit (*CoDatatypes*) 