src/ZF/ROOT
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58623 2db1df2c8467
child 59446 4427f04fca57
permissions -rw-r--r--
proper context for match_tac etc.;
     1 chapter ZF
     2 
     3 session ZF (main) = Pure +
     4   description {*
     5     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6     Copyright   1995  University of Cambridge
     7 
     8     Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
     9     Philippe Noel and Lawrence Paulson.
    10 
    11     Isabelle/ZF formalizes the greater part of elementary set theory, including
    12     relations, functions, injections, surjections, ordinals and cardinals.
    13     Results proved include Cantor's Theorem, the Recursion Theorem, the
    14     Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
    15 
    16     Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
    17     computational notions. It supports inductive definitions of
    18     infinite-branching trees for any cardinality of branching.
    19 
    20 
    21     Useful references for Isabelle/ZF:
    22 
    23     Lawrence C. Paulson, Set theory for verification: I. From foundations to
    24     functions. J. Automated Reasoning 11 (1993), 353-389.
    25 
    26     Lawrence C. Paulson, Set theory for verification: II. Induction and
    27     recursion. Report 312, Computer Lab (1993).
    28 
    29     Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive
    30     definitions. In: A. Bundy (editor), CADE-12: 12th International
    31     Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161.
    32 
    33 
    34     Useful references on ZF set theory:
    35 
    36     Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
    37 
    38     Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
    39 
    40     Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
    41 
    42     Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
    43     (North-Holland, 1980)
    44   *}
    45   options [document_graph]
    46   theories
    47     Main
    48     Main_ZFC
    49   document_files "root.tex"
    50 
    51 session "ZF-AC" in AC = ZF +
    52   description {*
    53     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54     Copyright   1995  University of Cambridge
    55 
    56     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    57 
    58     See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
    59     J.E. Rubin, 1985.
    60 
    61     The report
    62     http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
    63     "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
    64     development and ZF's theories of cardinals.
    65   *}
    66   options [document_graph]
    67   theories
    68     WO6_WO1
    69     WO1_WO7
    70     AC7_AC9
    71     WO1_AC
    72     AC15_WO6
    73     WO2_AC16
    74     AC16_WO4
    75     AC17_AC1
    76     AC18_AC19
    77     DC
    78   document_files "root.tex" "root.bib"
    79 
    80 session "ZF-Coind" in Coind = ZF +
    81   description {*
    82     Author:     Jacob Frost, Cambridge University Computer Laboratory
    83     Copyright   1995  University of Cambridge
    84 
    85     Coind -- A Coinduction Example.
    86 
    87     It involves proving the consistency of the dynamic and static semantics for
    88     a small functional language. A codatatype definition specifies values and
    89     value environments in mutual recursion: non-well-founded values represent
    90     recursive functions; value environments are variant functions from
    91     variables into values.
    92 
    93     Based upon the article
    94         Robin Milner and Mads Tofte,
    95         Co-induction in Relational Semantics,
    96         Theoretical Computer Science 87 (1991), pages 209-220.
    97 
    98     Written up as
    99         Jacob Frost, A Case Study of Co_induction in Isabelle
   100         Report, Computer Lab, University of Cambridge (1995).
   101         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   102   *}
   103   options [document = false]
   104   theories ECR
   105 
   106 session "ZF-Constructible" in Constructible = ZF +
   107   description {*
   108     Relative Consistency of the Axiom of Choice:
   109     Inner Models, Absoluteness and Consistency Proofs.
   110 
   111     Gödel's proof of the relative consistency of the axiom of choice is
   112     mechanized using Isabelle/ZF. The proof builds upon a previous
   113     mechanization of the reflection theorem (see
   114     http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
   115     reliance on metatheory in the original proof makes the formalization
   116     unusually long, and not entirely satisfactory: two parts of the proof do
   117     not fit together. It seems impossible to solve these problems without
   118     formalizing the metatheory. However, the present development follows a
   119     standard textbook, Kunen's Set Theory, and could support the formalization
   120     of further material from that book. It also serves as an example of what to
   121     expect when deep mathematics is formalized.
   122 
   123     A paper describing this development is
   124     http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
   125   *}
   126   options [document_graph]
   127   theories DPow_absolute AC_in_L Rank_Separation
   128   document_files "root.tex" "root.bib"
   129 
   130 session "ZF-IMP" in IMP = ZF +
   131   description {*
   132     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   133     Copyright   1994 TUM
   134 
   135     Formalization of the denotational and operational semantics of a
   136     simple while-language, including an equivalence proof.
   137 
   138     The whole development essentially formalizes/transcribes
   139     chapters 2 and 5 of
   140 
   141     Glynn Winskel. The Formal Semantics of Programming Languages.
   142     MIT Press, 1993.
   143   *}
   144   options [document = false]
   145   theories Equiv
   146   document_files "root.tex" "root.bib"
   147 
   148 session "ZF-Induct" in Induct = ZF +
   149   description {*
   150     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   151     Copyright   2001  University of Cambridge
   152 
   153     Inductive definitions.
   154   *}
   155   theories
   156     (** Datatypes **)
   157     Datatypes       (*sample datatypes*)
   158     Binary_Trees    (*binary trees*)
   159     Term            (*recursion over the list functor*)
   160     Ntree           (*variable-branching trees; function demo*)
   161     Tree_Forest     (*mutual recursion*)
   162     Brouwer         (*Infinite-branching trees*)
   163     Mutil           (*mutilated chess board*)
   164 
   165     (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
   166     finite sets*)
   167     Multiset
   168     Rmap            (*mapping a relation over a list*)
   169     PropLog         (*completeness of propositional logic*)
   170 
   171     (*two Coq examples by Christine Paulin-Mohring*)
   172     ListN
   173     Acc
   174 
   175     Comb            (*Combinatory Logic example*)
   176     Primrec         (*Primitive recursive functions*)
   177   document_files
   178     "root.bib"
   179     "root.tex"
   180 
   181 session "ZF-Resid" in Resid = ZF +
   182   description {*
   183     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   184     Copyright   1995  University of Cambridge
   185 
   186     Residuals -- a proof of the Church-Rosser Theorem for the
   187     untyped lambda-calculus.
   188 
   189     By Ole Rasmussen, following the Coq proof given in
   190 
   191     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
   192     J. Functional Programming 4(3) 1994, 371-394.
   193 
   194     See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
   195     Porting Experiment.
   196     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   197   *}
   198   options [document = false]
   199   theories Confluence
   200 
   201 session "ZF-UNITY" in UNITY = ZF +
   202   description {*
   203     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   204     Copyright   1998  University of Cambridge
   205 
   206     ZF/UNITY proofs.
   207   *}
   208   options [document = false]
   209   theories
   210     (*Simple examples: no composition*)
   211     Mutex
   212 
   213     (*Basic meta-theory*)
   214     Guar
   215 
   216     (*Prefix relation; the Allocator example*)
   217     Distributor Merge ClientImpl AllocImpl
   218 
   219 session "ZF-ex" in ex = ZF +
   220   description {*
   221     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   222     Copyright   1993  University of Cambridge
   223 
   224     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   225 
   226     Includes a simple form of Ramsey's theorem. A report is available:
   227     http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
   228 
   229     Several (co)inductive and (co)datatype definitions are presented. The
   230     report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
   231     describes the theoretical foundations of datatypes while
   232     href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
   233     describes the package that automates their declaration.
   234   *}
   235   options [document = false]
   236   theories
   237     misc
   238     Ring             (*abstract algebra*)
   239     Commutation      (*abstract Church-Rosser theory*)
   240     Primes           (*GCD theory*)
   241     NatSum           (*Summing integers, squares, cubes, etc.*)
   242     Ramsey           (*Simple form of Ramsey's theorem*)
   243     Limit            (*Inverse limit construction of domains*)
   244     BinEx            (*Binary integer arithmetic*)
   245     LList CoUnit     (*CoDatatypes*)
   246