src/ZF/ROOT
author wenzelm
Fri, 06 Sep 2019 10:28:29 +0200
changeset 70656 774cc139b1f4
parent 70634 0f8742b5a9e8
child 70703 edd856e6051a
permissions -rw-r--r--
more central checkpoint;
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     4
  description "
48280
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)
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    44
  "
66444
6d2d993fa76e clarified imports;
wenzelm
parents: 65569
diff changeset
    45
  sessions
6d2d993fa76e clarified imports;
wenzelm
parents: 65569
diff changeset
    46
    FOL
70656
774cc139b1f4 more central checkpoint;
wenzelm
parents: 70634
diff changeset
    47
  theories [dump_checkpoint]
65527
0d8a7013bf36 more global theories;
wenzelm
parents: 65449
diff changeset
    48
    ZF (global)
70656
774cc139b1f4 more central checkpoint;
wenzelm
parents: 70634
diff changeset
    49
  theories
65527
0d8a7013bf36 more global theories;
wenzelm
parents: 65449
diff changeset
    50
    ZFC (global)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 51403
diff changeset
    51
  document_files "root.tex"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    52
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
    53
session "ZF-AC" in AC = ZF +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 66946
diff changeset
    54
  description \<open>
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    55
    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
    56
    Copyright   1995  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    57
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    58
    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
    59
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    60
    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
    61
    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
    62
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    63
    The report
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    64
    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
    65
    "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
    66
    development and ZF's theories of cardinals.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    67
  \<close>
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    68
  theories
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    69
    WO6_WO1
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    70
    WO1_WO7
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    71
    AC7_AC9
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    72
    WO1_AC
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    73
    AC15_WO6
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    74
    WO2_AC16
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    75
    AC16_WO4
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    76
    AC17_AC1
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    77
    AC18_AC19
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48462
diff changeset
    78
    DC
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 51403
diff changeset
    79
  document_files "root.tex" "root.bib"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    80
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
    81
session "ZF-Coind" in Coind = ZF +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    82
  description "
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    83
    Author:     Jacob Frost, Cambridge University Computer Laboratory
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    84
    Copyright   1995  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    85
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    86
    Coind -- A Coinduction Example.
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    87
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    88
    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
    89
    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
    90
    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
    91
    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
    92
    variables into values.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    93
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    94
    Based upon the article
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    95
        Robin Milner and Mads Tofte,
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    96
        Co-induction in Relational Semantics,
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    97
        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
    98
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    99
    Written up as
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   100
        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
   101
        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
   102
        http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   103
  "
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   107
  description "
51403
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
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   133
  description "
48280
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.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   145
  "
48280
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   152
  description "
48280
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.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   157
  "
48280
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   185
  description "
48280
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
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   200
  "
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   201
  theories Confluence
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   202
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   203
session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   204
  description "
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   205
    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
   206
    Copyright   1998  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   207
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   208
    ZF/UNITY proofs.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   209
  "
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   210
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   211
    (*Simple examples: no composition*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   212
    Mutex
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   213
    (*Basic meta-theory*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   214
    Guar
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   215
    (*Prefix relation; the Allocator example*)
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   216
    Distributor Merge ClientImpl AllocImpl
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   217
66778
cf0187ca3a57 discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;
wenzelm
parents: 66750
diff changeset
   218
session "ZF-ex" in ex = ZF +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 66946
diff changeset
   219
  description \<open>
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   220
    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
   221
    Copyright   1993  University of Cambridge
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   222
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
   223
    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
   224
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   225
    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
   226
    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
   227
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   228
    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
   229
    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
   230
    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
   231
    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
   232
    describes the package that automates their declaration.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   233
  \<close>
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*)