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