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;
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
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
     3
session ZF (main timing) = 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
  *}
66444
6d2d993fa76e clarified imports;
wenzelm
parents: 65569
diff changeset
    45
  sessions
6d2d993fa76e clarified imports;
wenzelm
parents: 65569
diff changeset
    46
    FOL
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    47
  theories
65527
0d8a7013bf36 more global theories;
wenzelm
parents: 65449
diff changeset
    48
    ZF (global)
0d8a7013bf36 more global theories;
wenzelm
parents: 65449
diff changeset
    49
    ZFC (global)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 51403
diff changeset
    50
  document_files "root.tex"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    51
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
    52
session "ZF-AC" in AC = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    53
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    54
    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
    55
    Copyright   1995  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    56
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    57
    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
    58
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    59
    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
    60
    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
    61
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    62
    The report
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    63
    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
    64
    "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
    65
    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
    66
  *}
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
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 51403
diff changeset
    78
  document_files "root.tex" "root.bib"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    79
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
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
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
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
  *}
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 58623
diff changeset
   126
  theories
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 58623
diff changeset
   127
    DPow_absolute
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 58623
diff changeset
   128
    AC_in_L
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 58623
diff changeset
   129
    Rank_Separation
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 51403
diff changeset
   130
  document_files "root.tex" "root.bib"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   131
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   132
session "ZF-IMP" in IMP = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   133
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   134
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   135
    Copyright   1994 TUM
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   136
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   137
    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
   138
    simple while-language, including an equivalence proof.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   139
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   140
    The whole development essentially formalizes/transcribes
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   141
    chapters 2 and 5 of
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   142
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   143
    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
   144
    MIT Press, 1993.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   145
  *}
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   146
  theories Equiv
66750
41fbe4a3aac9 proper document;
wenzelm
parents: 66444
diff changeset
   147
  document_files
41fbe4a3aac9 proper document;
wenzelm
parents: 66444
diff changeset
   148
    "root.tex"
41fbe4a3aac9 proper document;
wenzelm
parents: 66444
diff changeset
   149
    "root.bib"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   150
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   151
session "ZF-Induct" in Induct = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   152
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   153
    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
   154
    Copyright   2001  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   155
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   156
    Inductive definitions.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   157
  *}
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   158
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   159
    (** Datatypes **)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   160
    Datatypes       (*sample datatypes*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   161
    Binary_Trees    (*binary trees*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   162
    Term            (*recursion over the list functor*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   163
    Ntree           (*variable-branching trees; function demo*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   164
    Tree_Forest     (*mutual recursion*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   165
    Brouwer         (*Infinite-branching trees*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   166
    Mutil           (*mutilated chess board*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   167
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   168
    (*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
   169
    finite sets*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   170
    Multiset
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   171
    Rmap            (*mapping a relation over a list*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   172
    PropLog         (*completeness of propositional logic*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   173
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   174
    (*two Coq examples by Christine Paulin-Mohring*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   175
    ListN
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   176
    Acc
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   177
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   178
    Comb            (*Combinatory Logic example*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   179
    Primrec         (*Primitive recursive functions*)
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 56781
diff changeset
   180
  document_files
2db1df2c8467 more bibtex entries;
wenzelm
parents: 56781
diff changeset
   181
    "root.bib"
2db1df2c8467 more bibtex entries;
wenzelm
parents: 56781
diff changeset
   182
    "root.tex"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   183
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   184
session "ZF-Resid" in Resid = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   185
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   186
    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
   187
    Copyright   1995  University of Cambridge
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
    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
   190
    untyped lambda-calculus.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   191
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   192
    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
   193
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   194
    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
   195
    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
   196
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   197
    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
   198
    Porting Experiment.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   199
    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
   200
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   201
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   202
  theories Confluence
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   203
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   204
session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   205
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   206
    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
   207
    Copyright   1998  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   208
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   209
    ZF/UNITY proofs.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   210
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   211
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   212
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   213
    (*Simple examples: no composition*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   214
    Mutex
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   215
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   216
    (*Basic meta-theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   217
    Guar
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   218
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   219
    (*Prefix relation; the Allocator example*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   220
    Distributor Merge ClientImpl AllocImpl
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   221
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   222
session "ZF-ex" in ex = ZF +
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   223
  description {*
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   224
    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
   225
    Copyright   1993  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   226
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   227
    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
   228
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   229
    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
   230
    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
   231
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   232
    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
   233
    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
   234
    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
   235
    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
   236
    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
   237
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
   238
  options [document = false]
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   239
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   240
    misc
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   241
    Ring             (*abstract algebra*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   242
    Commutation      (*abstract Church-Rosser theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   243
    Primes           (*GCD theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   244
    NatSum           (*Summing integers, squares, cubes, etc.*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   245
    Ramsey           (*Simple form of Ramsey's theorem*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   246
    Limit            (*Inverse limit construction of domains*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   247
    BinEx            (*Binary integer arithmetic*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   248
    LList CoUnit     (*CoDatatypes*)