src/ZF/ROOT
author blanchet
Wed, 06 Nov 2013 22:50:12 +0100
changeset 54284 0b53378080d9
parent 51403 2ff3a5589b05
child 56781 f2eb0f22589f
permissions -rw-r--r--
simplified code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
50574
0706797501a0 offer sessions of group "main" first to increase chances that the user makes a sensible choice;
wenzelm
parents: 48738
diff changeset
     3
session ZF (main) = 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
    Zermelo-Fraenkel 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
    Schroeder-Bernstein 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
    infinite-branching 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), 353-389.
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), CADE-12: 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), 148-161.
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
    (North-Holland, 1980)
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    44
  *}
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    45
  options [document_graph]
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    46
  theories
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    47
    Main
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    48
    Main_ZFC
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    49
  files "document/root.tex"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    50
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
    51
session "ZF-AC" in AC = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    52
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    53
    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
    54
    Copyright   1995  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    55
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    56
    Proofs of AC-equivalences, 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
    57
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    58
    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
    59
    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
    60
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    61
    The report
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    62
    http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    63
    "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
    64
    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
    65
  *}
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    66
  options [document_graph]
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
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    78
  files "document/root.tex" "document/root.bib"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    79
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
    80
session "ZF-Coind" 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: non-well-founded 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
        Co-induction 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 209-220.
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/TR359-jf10008-co-induction-in-isabelle.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
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   106
session "ZF-Constructible" 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/UCAM-CL-TR-551.pdf
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   125
  *}
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   126
  options [document_graph]
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   127
  theories DPow_absolute AC_in_L Rank_Separation
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   128
  files "document/root.tex" "document/root.bib"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   129
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   130
session "ZF-IMP" in IMP = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   131
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   132
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   133
    Copyright   1994 TUM
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   134
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   135
    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
   136
    simple while-language, including an equivalence proof.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   137
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   138
    The whole development essentially formalizes/transcribes
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   139
    chapters 2 and 5 of
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   140
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   141
    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
   142
    MIT Press, 1993.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   143
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   144
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   145
  theories Equiv
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   146
  files "document/root.tex" "document/root.bib"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   147
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   148
session "ZF-Induct" in Induct = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   149
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   150
    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
   151
    Copyright   2001  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   152
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   153
    Inductive definitions.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   154
  *}
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   155
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   156
    (** Datatypes **)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   157
    Datatypes       (*sample datatypes*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   158
    Binary_Trees    (*binary trees*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   159
    Term            (*recursion over the list functor*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   160
    Ntree           (*variable-branching trees; function demo*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   161
    Tree_Forest     (*mutual recursion*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   162
    Brouwer         (*Infinite-branching trees*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   163
    Mutil           (*mutilated chess board*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   164
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   165
    (*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
   166
    finite sets*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   167
    Multiset
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   168
    Rmap            (*mapping a relation over a list*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   169
    PropLog         (*completeness of propositional logic*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   170
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   171
    (*two Coq examples by Christine Paulin-Mohring*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   172
    ListN
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   173
    Acc
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   174
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   175
    Comb            (*Combinatory Logic example*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   176
    Primrec         (*Primitive recursive functions*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   177
  files "document/root.tex"
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   178
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   179
session "ZF-Resid" in Resid = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   180
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   181
    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
   182
    Copyright   1995  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   183
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   184
    Residuals -- a proof of the Church-Rosser Theorem for the
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   185
    untyped lambda-calculus.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   186
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   187
    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
   188
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   189
    Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   190
    J. Functional Programming 4(3) 1994, 371-394.
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   191
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   192
    See Rasmussen's report: The Church-Rosser 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
   193
    Porting Experiment.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   194
    http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   195
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   196
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   197
  theories Confluence
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   198
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   199
session "ZF-UNITY" in UNITY = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   200
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   201
    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
   202
    Copyright   1998  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   203
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   204
    ZF/UNITY proofs.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   205
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   206
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   207
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   208
    (*Simple examples: no composition*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   209
    Mutex
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   210
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   211
    (*Basic meta-theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   212
    Guar
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   213
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   214
    (*Prefix relation; the Allocator example*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   215
    Distributor Merge ClientImpl AllocImpl
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   216
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
   217
session "ZF-ex" in ex = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   218
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   219
    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
   220
    Copyright   1993  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   221
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   222
    Miscellaneous examples for Zermelo-Fraenkel Set Theory.
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   223
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   224
    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
   225
    http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   226
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   227
    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
   228
    report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   229
    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
   230
    href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   231
    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
   232
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   233
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   234
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   235
    misc
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   236
    Ring             (*abstract algebra*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   237
    Commutation      (*abstract Church-Rosser theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   238
    Primes           (*GCD theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   239
    NatSum           (*Summing integers, squares, cubes, etc.*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   240
    Ramsey           (*Simple form of Ramsey's theorem*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   241
    Limit            (*Inverse limit construction of domains*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   242
    BinEx            (*Binary integer arithmetic*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   243
    LList CoUnit     (*CoDatatypes*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   244