doc-src/springer.tex
author wenzelm
Tue, 25 Jan 2011 20:06:32 +0100
changeset 41629 5490dc4d999d
parent 8828 5be2d1745c61
permissions -rw-r--r--
workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
     1
%% $ lcp Exp $
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     2
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
358
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
     3
%\includeonly{Ref/simplifier}
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
     4
%%  index{\(\w+\)\!meta-level     index{meta-\1
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     5
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     6
%% run    sedindex springer    to prepare index file
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     7
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
     8
\sloppy
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     9
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    10
\title{Isabelle\\A Generic Theorem Prover}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    11
\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    12
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    13
\date{} 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    14
\makeindex
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    15
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    16
\def\S{Sect.\thinspace}%This is how Springer like it
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    17
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    18
\underscoreoff
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    19
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    20
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    21
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    22
\binperiod     %%%treat . like a binary operator
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    23
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    24
\begin{document}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    25
\maketitle
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    26
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    27
\pagenumbering{Roman}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    28
\include{preface}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    29
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    30
\tableofcontents
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    31
\newpage
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    32
\listoffigures
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    33
\newpage
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    34
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    35
\markboth{}{}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    36
\newfont{\sanssi}{cmssi12}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    37
\vspace*{2.5cm}
358
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    38
\begin{quote}\raggedleft
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    39
{\em To Nathan and Sarah}
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    40
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    41
\vspace*{1.2cm}
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    42
{\sanssi
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    43
You can only find truth with logic\\
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    44
if you have already found truth without it.}\\
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    45
\bigskip
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    46
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    47
G.K. Chesterton, {\em The Man who was Orthodox}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    48
\end{quote}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    49
358
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    50
\thispagestyle{empty}
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    51
\newpage
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    52
\pagenumbering{arabic}
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    53
\part{Introduction to Isabelle}   
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    54
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    55
\index{hypotheses|see{assumptions}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    56
\index{rewriting|see{simplification}}
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    57
\index{variables!schematic|see{unknowns}} 
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    58
\index{abstract syntax trees|see{ASTs}}
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    59
358
df8f0fbf7dbd post-CRC corrections
lcp
parents: 328
diff changeset
    60
\begingroup%things local to Intro -- especially, redefining \part!!
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    61
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    62
\newcommand{\nand}{\mathbin{\lnot\&}} 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    63
\newcommand{\xor}{\mathbin{\#}}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    64
\let\part=\chapter
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    65
\include{Intro/foundations}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    66
\include{Intro/getting}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    67
\include{Intro/advanced}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    68
\endgroup
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    69
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    70
\part{The Isabelle Reference Manual} 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    71
\include{Ref/introduction}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    72
\include{Ref/goals}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    73
\include{Ref/tactic}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    74
\include{Ref/tctical}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    75
\include{Ref/thm}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    76
\include{Ref/theories}
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    77
\include{Ref/defining}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    78
\include{Ref/syntax}
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    79
\include{Ref/substitution}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    80
\include{Ref/simplifier}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    81
\include{Ref/classical}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    82
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    83
\part{Isabelle's Object-Logics} 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    84
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    85
  \hrule\bigskip}
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    86
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    87
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    88
\include{Logics/intro}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    89
\include{Logics/FOL}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    90
\include{Logics/ZF}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    91
\include{Logics/HOL}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    92
\include{Logics/LK}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    93
\include{Logics/CTT}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    94
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    95
\include{Ref/theory-syntax}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    96
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    97
%%seealso's must be last so that they appear last in the index entries
328
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    98
\index{backtracking|seealso{{\tt back} command, search}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
    99
\index{classes|seealso{sorts}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
   100
\index{sorts|seealso{arities}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
   101
\index{axioms|seealso{rules, theorems}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
   102
\index{theorems|seealso{rules}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
   103
\index{definitions|seealso{meta-rewriting}}
2d1b460dbb62 penultimate Springer draft
lcp
parents: 304
diff changeset
   104
\index{equality|seealso{simplification}}
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   105
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   106
\bibliographystyle{springer} \small\raggedright\frenchspacing
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   107
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   108
8828
5be2d1745c61 improved indexing;
wenzelm
parents: 358
diff changeset
   109
\printindex
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   110
\end{document}