summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/ZF/ROOT

author | wenzelm |

Sat, 07 Oct 2017 15:21:25 +0200 | |

changeset 66778 | cf0187ca3a57 |

parent 66750 | 41fbe4a3aac9 |

child 66946 | 3d8fd98c7c86 |

permissions | -rw-r--r-- |

discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;

chapter ZF session ZF (main timing) = Pure + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. Isabelle/ZF formalizes the greater part of elementary set theory, including relations, functions, injections, surjections, ordinals and cardinals. Results proved include Cantor's Theorem, the Recursion Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions. It supports inductive definitions of infinite-branching trees for any cardinality of branching. Useful references for Isabelle/ZF: Lawrence C. Paulson, Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353-389. Lawrence C. Paulson, Set theory for verification: II. Induction and recursion. Report 312, Computer Lab (1993). Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive definitions. In: A. Bundy (editor), CADE-12: 12th International Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161. Useful references on ZF set theory: Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) Patrick Suppes, Axiomatic Set Theory (Dover, 1972) Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979) Kenneth Kunen, Set Theory: An Introduction to Independence Proofs, (North-Holland, 1980) *} sessions FOL theories ZF (global) ZFC (global) document_files "root.tex" session "ZF-AC" in AC = ZF + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Proofs of AC-equivalences, due to Krzysztof Grabczewski. See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and J.E. Rubin, 1985. The report http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals. *} theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6 WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC document_files "root.tex" "root.bib" session "ZF-Coind" in Coind = ZF + description {* Author: Jacob Frost, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Coind -- A Coinduction Example. It involves proving the consistency of the dynamic and static semantics for a small functional language. A codatatype definition specifies values and value environments in mutual recursion: non-well-founded values represent recursive functions; value environments are variant functions from variables into values. Based upon the article Robin Milner and Mads Tofte, Co-induction in Relational Semantics, Theoretical Computer Science 87 (1991), pages 209-220. Written up as Jacob Frost, A Case Study of Co_induction in Isabelle Report, Computer Lab, University of Cambridge (1995). http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz *} options [document = false] theories ECR session "ZF-Constructible" in Constructible = ZF + description {* Relative Consistency of the Axiom of Choice: Inner Models, Absoluteness and Consistency Proofs. GĂ¶del's proof of the relative consistency of the axiom of choice is mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem (see http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy reliance on metatheory in the original proof makes the formalization unusually long, and not entirely satisfactory: two parts of the proof do not fit together. It seems impossible to solve these problems without formalizing the metatheory. However, the present development follows a standard textbook, Kunen's Set Theory, and could support the formalization of further material from that book. It also serves as an example of what to expect when deep mathematics is formalized. A paper describing this development is http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf *} theories DPow_absolute AC_in_L Rank_Separation document_files "root.tex" "root.bib" session "ZF-IMP" in IMP = ZF + description {* Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM Formalization of the denotational and operational semantics of a simple while-language, including an equivalence proof. The whole development essentially formalizes/transcribes chapters 2 and 5 of Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. *} theories Equiv document_files "root.tex" "root.bib" session "ZF-Induct" in Induct = ZF + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge Inductive definitions. *} theories (** Datatypes **) Datatypes (*sample datatypes*) Binary_Trees (*binary trees*) Term (*recursion over the list functor*) Ntree (*variable-branching trees; function demo*) Tree_Forest (*mutual recursion*) Brouwer (*Infinite-branching trees*) Mutil (*mutilated chess board*) (*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for finite sets*) Multiset Rmap (*mapping a relation over a list*) PropLog (*completeness of propositional logic*) (*two Coq examples by Christine Paulin-Mohring*) ListN Acc Comb (*Combinatory Logic example*) Primrec (*Primitive recursive functions*) document_files "root.bib" "root.tex" session "ZF-Resid" in Resid = ZF + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Residuals -- a proof of the Church-Rosser Theorem for the untyped lambda-calculus. By Ole Rasmussen, following the Coq proof given in Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. J. Functional Programming 4(3) 1994, 371-394. See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment. http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz *} options [document = false] theories Confluence session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge ZF/UNITY proofs. *} options [document = false] theories (*Simple examples: no composition*) Mutex (*Basic meta-theory*) Guar (*Prefix relation; the Allocator example*) Distributor Merge ClientImpl AllocImpl session "ZF-ex" in ex = ZF + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Miscellaneous examples for Zermelo-Fraenkel Set Theory. Includes a simple form of Ramsey's theorem. A report is available: http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z Several (co)inductive and (co)datatype definitions are presented. The report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz describes the theoretical foundations of datatypes while href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz describes the package that automates their declaration. *} options [document = false] theories misc Ring (*abstract algebra*) Commutation (*abstract Church-Rosser theory*) Primes (*GCD theory*) NatSum (*Summing integers, squares, cubes, etc.*) Ramsey (*Simple form of Ramsey's theorem*) Limit (*Inverse limit construction of domains*) BinEx (*Binary integer arithmetic*) LList CoUnit (*CoDatatypes*)