|
1 session ZF in "." = FOL + |
|
2 name ZF |
|
3 description {* |
|
4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
5 Copyright 1995 University of Cambridge |
|
6 |
|
7 Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. |
|
8 |
|
9 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. |
|
10 *} |
|
11 options [document_graph] |
|
12 theories Main Main_ZFC |
|
13 files "document/root.tex" |
|
14 |
|
15 session AC = ZF + |
|
16 description {* |
|
17 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
18 Copyright 1995 University of Cambridge |
|
19 |
|
20 Proofs of AC-equivalences, due to Krzysztof Grabczewski. |
|
21 *} |
|
22 options [document_graph] |
|
23 theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6 |
|
24 WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC |
|
25 files "document/root.tex" "document/root.bib" |
|
26 |
|
27 session Coind = ZF + |
|
28 description {* |
|
29 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
30 Copyright 1995 University of Cambridge |
|
31 |
|
32 Coind -- A Coinduction Example. |
|
33 |
|
34 Based upon the article |
|
35 Robin Milner and Mads Tofte, |
|
36 Co-induction in Relational Semantics, |
|
37 Theoretical Computer Science 87 (1991), pages 209-220. |
|
38 |
|
39 Written up as |
|
40 Jacob Frost, A Case Study of Co_induction in Isabelle |
|
41 Report, Computer Lab, University of Cambridge (1995). |
|
42 *} |
|
43 theories ECR |
|
44 |
|
45 session Constructible = ZF + |
|
46 description {* Inner Models, Absoluteness and Consistency Proofs. *} |
|
47 options [document_graph] |
|
48 theories DPow_absolute AC_in_L Rank_Separation |
|
49 files "document/root.tex" "document/root.bib" |
|
50 |
|
51 session IMP = ZF + |
|
52 description {* |
|
53 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
54 Copyright 1994 TUM |
|
55 |
|
56 Formalization of the denotational and operational semantics of a |
|
57 simple while-language, including an equivalence proof. |
|
58 |
|
59 The whole development essentially formalizes/transcribes |
|
60 chapters 2 and 5 of |
|
61 |
|
62 Glynn Winskel. The Formal Semantics of Programming Languages. |
|
63 MIT Press, 1993. |
|
64 *} |
|
65 theories Equiv |
|
66 files "document/root.tex" "document/root.bib" |
|
67 |
|
68 session Induct = ZF + |
|
69 description {* |
|
70 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
71 Copyright 2001 University of Cambridge |
|
72 |
|
73 Inductive definitions. |
|
74 *} |
|
75 theories |
|
76 (** Datatypes **) |
|
77 Datatypes (*sample datatypes*) |
|
78 Binary_Trees (*binary trees*) |
|
79 Term (*recursion over the list functor*) |
|
80 Ntree (*variable-branching trees; function demo*) |
|
81 Tree_Forest (*mutual recursion*) |
|
82 Brouwer (*Infinite-branching trees*) |
|
83 Mutil (*mutilated chess board*) |
|
84 |
|
85 (*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for |
|
86 finite sets*) |
|
87 Multiset |
|
88 Rmap (*mapping a relation over a list*) |
|
89 PropLog (*completeness of propositional logic*) |
|
90 |
|
91 (*two Coq examples by Christine Paulin-Mohring*) |
|
92 ListN |
|
93 Acc |
|
94 |
|
95 Comb (*Combinatory Logic example*) |
|
96 Primrec (*Primitive recursive functions*) |
|
97 files "document/root.tex" |
|
98 |
|
99 session Resid = ZF + |
|
100 description {* |
|
101 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
102 Copyright 1995 University of Cambridge |
|
103 |
|
104 Residuals -- a proof of the Church-Rosser Theorem for the |
|
105 untyped lambda-calculus. |
|
106 |
|
107 By Ole Rasmussen, following the Coq proof given in |
|
108 |
|
109 Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. |
|
110 J. Functional Programming 4(3) 1994, 371-394. |
|
111 *} |
|
112 theories Confluence |
|
113 |
|
114 session UNITY = ZF + |
|
115 description {* |
|
116 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
117 Copyright 1998 University of Cambridge |
|
118 |
|
119 ZF/UNITY proofs. |
|
120 *} |
|
121 theories |
|
122 (*Simple examples: no composition*) |
|
123 Mutex |
|
124 |
|
125 (*Basic meta-theory*) |
|
126 Guar |
|
127 |
|
128 (*Prefix relation; the Allocator example*) |
|
129 Distributor Merge ClientImpl AllocImpl |
|
130 |
|
131 session ex = ZF + |
|
132 description {* |
|
133 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
134 Copyright 1993 University of Cambridge |
|
135 |
|
136 Miscellaneous examples for Zermelo-Fraenkel Set Theory. |
|
137 *} |
|
138 theories |
|
139 misc |
|
140 Ring (*abstract algebra*) |
|
141 Commutation (*abstract Church-Rosser theory*) |
|
142 Primes (*GCD theory*) |
|
143 NatSum (*Summing integers, squares, cubes, etc.*) |
|
144 Ramsey (*Simple form of Ramsey's theorem*) |
|
145 Limit (*Inverse limit construction of domains*) |
|
146 BinEx (*Binary integer arithmetic*) |
|
147 LList CoUnit (*CoDatatypes*) |
|
148 |