src/ZF/ROOT
author wenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 49566 66cbf8bb4693
parent 48738 f8c1a5b9488f
child 50574 0706797501a0
permissions -rw-r--r--
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
wenzelm@48738
     1
session ZF = Pure +
wenzelm@48280
     2
  description {*
wenzelm@48280
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
     4
    Copyright   1995  University of Cambridge
wenzelm@48280
     5
wenzelm@48280
     6
    Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
wenzelm@48280
     7
wenzelm@48280
     8
    This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
wenzelm@48280
     9
  *}
wenzelm@48280
    10
  options [document_graph]
wenzelm@48483
    11
  theories
wenzelm@48483
    12
    Main
wenzelm@48483
    13
    Main_ZFC
wenzelm@48280
    14
  files "document/root.tex"
wenzelm@48280
    15
wenzelm@48738
    16
session "ZF-AC" in AC = ZF +
wenzelm@48280
    17
  description {*
wenzelm@48280
    18
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
    19
    Copyright   1995  University of Cambridge
wenzelm@48280
    20
wenzelm@48280
    21
    Proofs of AC-equivalences, due to Krzysztof Grabczewski.
wenzelm@48280
    22
  *}
wenzelm@48280
    23
  options [document_graph]
wenzelm@48483
    24
  theories
wenzelm@48483
    25
    WO6_WO1
wenzelm@48483
    26
    WO1_WO7
wenzelm@48483
    27
    AC7_AC9
wenzelm@48483
    28
    WO1_AC
wenzelm@48483
    29
    AC15_WO6
wenzelm@48483
    30
    WO2_AC16
wenzelm@48483
    31
    AC16_WO4
wenzelm@48483
    32
    AC17_AC1
wenzelm@48483
    33
    AC18_AC19
wenzelm@48483
    34
    DC
wenzelm@48280
    35
  files "document/root.tex" "document/root.bib"
wenzelm@48280
    36
wenzelm@48738
    37
session "ZF-Coind" in Coind = ZF +
wenzelm@48280
    38
  description {*
wenzelm@48280
    39
    Author:     Jacob Frost, Cambridge University Computer Laboratory
wenzelm@48280
    40
    Copyright   1995  University of Cambridge
wenzelm@48280
    41
wenzelm@48280
    42
    Coind -- A Coinduction Example.
wenzelm@48280
    43
wenzelm@48280
    44
    Based upon the article
wenzelm@48280
    45
        Robin Milner and Mads Tofte,
wenzelm@48280
    46
        Co-induction in Relational Semantics,
wenzelm@48280
    47
        Theoretical Computer Science 87 (1991), pages 209-220.
wenzelm@48280
    48
wenzelm@48280
    49
    Written up as
wenzelm@48280
    50
        Jacob Frost, A Case Study of Co_induction in Isabelle
wenzelm@48280
    51
        Report, Computer Lab, University of Cambridge (1995).
wenzelm@48280
    52
  *}
wenzelm@48483
    53
  options [document = false]
wenzelm@48280
    54
  theories ECR
wenzelm@48280
    55
wenzelm@48738
    56
session "ZF-Constructible" in Constructible = ZF +
wenzelm@48280
    57
  description {* Inner Models, Absoluteness and Consistency Proofs. *}
wenzelm@48280
    58
  options [document_graph]
wenzelm@48280
    59
  theories DPow_absolute AC_in_L Rank_Separation
wenzelm@48280
    60
  files "document/root.tex" "document/root.bib"
wenzelm@48280
    61
wenzelm@48738
    62
session "ZF-IMP" in IMP = ZF +
wenzelm@48280
    63
  description {*
wenzelm@48280
    64
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
wenzelm@48280
    65
    Copyright   1994 TUM
wenzelm@48280
    66
wenzelm@48280
    67
    Formalization of the denotational and operational semantics of a
wenzelm@48280
    68
    simple while-language, including an equivalence proof.
wenzelm@48280
    69
wenzelm@48280
    70
    The whole development essentially formalizes/transcribes
wenzelm@48280
    71
    chapters 2 and 5 of
wenzelm@48280
    72
wenzelm@48280
    73
    Glynn Winskel. The Formal Semantics of Programming Languages.
wenzelm@48280
    74
    MIT Press, 1993.
wenzelm@48280
    75
  *}
wenzelm@48483
    76
  options [document = false]
wenzelm@48280
    77
  theories Equiv
wenzelm@48280
    78
  files "document/root.tex" "document/root.bib"
wenzelm@48280
    79
wenzelm@48738
    80
session "ZF-Induct" in Induct = ZF +
wenzelm@48280
    81
  description {*
wenzelm@48280
    82
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
    83
    Copyright   2001  University of Cambridge
wenzelm@48280
    84
wenzelm@48280
    85
    Inductive definitions.
wenzelm@48280
    86
  *}
wenzelm@48280
    87
  theories
wenzelm@48280
    88
    (** Datatypes **)
wenzelm@48280
    89
    Datatypes       (*sample datatypes*)
wenzelm@48280
    90
    Binary_Trees    (*binary trees*)
wenzelm@48280
    91
    Term            (*recursion over the list functor*)
wenzelm@48280
    92
    Ntree           (*variable-branching trees; function demo*)
wenzelm@48280
    93
    Tree_Forest     (*mutual recursion*)
wenzelm@48280
    94
    Brouwer         (*Infinite-branching trees*)
wenzelm@48280
    95
    Mutil           (*mutilated chess board*)
wenzelm@48280
    96
wenzelm@48280
    97
    (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
wenzelm@48280
    98
    finite sets*)
wenzelm@48280
    99
    Multiset
wenzelm@48280
   100
    Rmap            (*mapping a relation over a list*)
wenzelm@48280
   101
    PropLog         (*completeness of propositional logic*)
wenzelm@48280
   102
wenzelm@48280
   103
    (*two Coq examples by Christine Paulin-Mohring*)
wenzelm@48280
   104
    ListN
wenzelm@48280
   105
    Acc
wenzelm@48280
   106
wenzelm@48280
   107
    Comb            (*Combinatory Logic example*)
wenzelm@48280
   108
    Primrec         (*Primitive recursive functions*)
wenzelm@48280
   109
  files "document/root.tex"
wenzelm@48280
   110
wenzelm@48738
   111
session "ZF-Resid" in Resid = ZF +
wenzelm@48280
   112
  description {*
wenzelm@48280
   113
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
   114
    Copyright   1995  University of Cambridge
wenzelm@48280
   115
wenzelm@48280
   116
    Residuals -- a proof of the Church-Rosser Theorem for the
wenzelm@48280
   117
    untyped lambda-calculus.
wenzelm@48280
   118
wenzelm@48280
   119
    By Ole Rasmussen, following the Coq proof given in
wenzelm@48280
   120
wenzelm@48280
   121
    Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
wenzelm@48280
   122
    J. Functional Programming 4(3) 1994, 371-394.
wenzelm@48280
   123
  *}
wenzelm@48483
   124
  options [document = false]
wenzelm@48280
   125
  theories Confluence
wenzelm@48280
   126
wenzelm@48738
   127
session "ZF-UNITY" in UNITY = ZF +
wenzelm@48280
   128
  description {*
wenzelm@48280
   129
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
   130
    Copyright   1998  University of Cambridge
wenzelm@48280
   131
wenzelm@48280
   132
    ZF/UNITY proofs.
wenzelm@48280
   133
  *}
wenzelm@48483
   134
  options [document = false]
wenzelm@48280
   135
  theories
wenzelm@48280
   136
    (*Simple examples: no composition*)
wenzelm@48280
   137
    Mutex
wenzelm@48280
   138
wenzelm@48280
   139
    (*Basic meta-theory*)
wenzelm@48280
   140
    Guar
wenzelm@48280
   141
wenzelm@48280
   142
    (*Prefix relation; the Allocator example*)
wenzelm@48280
   143
    Distributor Merge ClientImpl AllocImpl
wenzelm@48280
   144
wenzelm@48738
   145
session "ZF-ex" in ex = ZF +
wenzelm@48280
   146
  description {*
wenzelm@48280
   147
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48280
   148
    Copyright   1993  University of Cambridge
wenzelm@48280
   149
wenzelm@48280
   150
    Miscellaneous examples for Zermelo-Fraenkel Set Theory.
wenzelm@48280
   151
  *}
wenzelm@48483
   152
  options [document = false]
wenzelm@48280
   153
  theories
wenzelm@48280
   154
    misc
wenzelm@48280
   155
    Ring             (*abstract algebra*)
wenzelm@48280
   156
    Commutation      (*abstract Church-Rosser theory*)
wenzelm@48280
   157
    Primes           (*GCD theory*)
wenzelm@48280
   158
    NatSum           (*Summing integers, squares, cubes, etc.*)
wenzelm@48280
   159
    Ramsey           (*Simple form of Ramsey's theorem*)
wenzelm@48280
   160
    Limit            (*Inverse limit construction of domains*)
wenzelm@48280
   161
    BinEx            (*Binary integer arithmetic*)
wenzelm@48280
   162
    LList CoUnit     (*CoDatatypes*)
wenzelm@48280
   163