doc-src/Logics/logics.toc
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 465 d4bf81734dfe
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
     1
\contentsline {chapter}{\numberline {1}Basic Concepts}{1}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
     2
\contentsline {section}{\numberline {1.1}Syntax definitions}{2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\contentsline {section}{\numberline {1.2}Proof procedures}{3}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
     4
\contentsline {chapter}{\numberline {2}First-Order Logic}{4}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
\contentsline {section}{\numberline {2.2}Generic packages}{8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
\contentsline {section}{\numberline {2.4}Classical proof procedures}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\contentsline {section}{\numberline {2.5}An intuitionistic example}{11}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
\contentsline {section}{\numberline {2.7}A classical example}{14}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    12
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    13
\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    14
\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    15
\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    16
\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    17
\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    18
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    19
\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    20
\contentsline {section}{\numberline {3.3}Binding operators}{25}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    21
\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    22
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    23
\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    24
\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    25
\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    26
\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    27
\contentsline {subsection}{\numberline {3.5.5}Relations}{36}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    28
\contentsline {subsection}{\numberline {3.5.6}Functions}{37}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    29
\contentsline {section}{\numberline {3.6}Further developments}{38}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    30
\contentsline {section}{\numberline {3.7}Simplification rules}{47}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    31
\contentsline {section}{\numberline {3.8}The examples directory}{47}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    32
\contentsline {section}{\numberline {3.9}A proof about powersets}{48}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    33
\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    34
\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    35
\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    36
\contentsline {section}{\numberline {4.1}Syntax}{55}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    37
\contentsline {subsection}{\numberline {4.1.1}Types}{57}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    38
\contentsline {subsection}{\numberline {4.1.2}Binders}{58}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    39
\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    40
\contentsline {section}{\numberline {4.2}Rules of inference}{58}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    41
\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    42
\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    43
\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}
359
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    44
\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
b5a2e9503a7a final Springer version
lcp
parents: 136
diff changeset
    45
\contentsline {section}{\numberline {4.5}Types}{73}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    46
\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    47
\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    48
\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    49
\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    50
\contentsline {section}{\numberline {4.6}Datatype declarations}{79}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    51
\contentsline {subsection}{\numberline {4.6.1}Foundations}{79}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    52
\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    53
\contentsline {subsection}{\numberline {4.6.3}Examples}{82}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    54
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    55
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    56
\contentsline {subsubsection}{Defining functions on datatypes}{83}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    57
\contentsline {subsubsection}{A datatype for weekdays}{84}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    58
\contentsline {section}{\numberline {4.7}The examples directories}{84}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    59
\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    60
\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    61
\contentsline {section}{\numberline {5.1}Unification for lists}{88}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    62
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    63
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    64
\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    65
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    66
\contentsline {section}{\numberline {5.6}Proof procedures}{94}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    67
\contentsline {subsection}{\numberline {5.6.1}Method A}{95}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    68
\contentsline {subsection}{\numberline {5.6.2}Method B}{95}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    69
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    70
\contentsline {section}{\numberline {5.8}A more complex proof}{97}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    71
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    72
\contentsline {section}{\numberline {6.1}Syntax}{101}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    73
\contentsline {section}{\numberline {6.2}Rules of inference}{101}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    74
\contentsline {section}{\numberline {6.3}Rule lists}{107}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    75
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    76
\contentsline {section}{\numberline {6.5}Rewriting tactics}{108}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    77
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    78
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    79
\contentsline {section}{\numberline {6.8}The examples directory}{111}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    80
\contentsline {section}{\numberline {6.9}Example: type inference}{111}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    81
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    82
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 359
diff changeset
    83
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}