doc-src/TutorialI/tutorial.tex
 author nipkow Thu Nov 30 13:56:46 2000 +0100 (2000-11-30) changeset 10543 8e4307d1207a parent 10524 270b285d48ee child 10597 29dd6ac8c223 permissions -rw-r--r--
*** empty log message ***
1 \documentclass{article}
2 \newif\ifremarks
3 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
4 \usepackage{cl2emono-modified,isabelle,isabellesym}
5 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
6 \usepackage{../proof,amsmath}
7 \usepackage{../pdfsetup}    %last package!
9 %\newtheorem{theorem}{Theorem}[section]
10 \newtheorem{Exercise}{Exercise}[section]
11 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
12 \newcommand{\ttlbr}{\texttt{[|}}
13 \newcommand{\ttrbr}{\texttt{|]}}
14 \newcommand{\ttor}{\texttt{|}}
15 \newcommand{\ttall}{\texttt{!}}
16 \newcommand{\ttuniquex}{\texttt{?!}}
17 \newcommand{\ttEXU}{\texttt{EX!}}
18 \newcommand{\ttAnd}{\texttt{!!}}
20 \newcommand{\isasymimp}{\isasymlongrightarrow}
21 \newcommand{\isasymImp}{\isasymLongrightarrow}
22 \newcommand{\isasymFun}{\isasymRightarrow}
23 \newcommand{\isasymuniqex}{\isamath{\exists!\,}}
25 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
27 %% lcp's macros
28 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
29 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
30 \let\bigisa=\isa
31 %% was previously
32 %% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}}
33 %% because \isa is too small for variables, but does it really matter?
36 %%% to index derived rls:  ^$$[a-zA-Z0-9][a-zA-Z0-9_]*$$        \\tdx{\1}
37 %%% to index rulenames:   ^ *($$[a-zA-Z0-9][a-zA-Z0-9_]*$$,     \\tdx{\1}
38 %%% to index constants:   \\tt $$[a-zA-Z0-9][a-zA-Z0-9_]*$$     \\cdx{\1}
39 %%% to deverbify:         \\verb|$$[^|]*$$|     \\ttindex{\1}
40 %% run    ../sedindex logics    to prepare index file
42 \makeindex
43 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
44 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
45 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
46 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
48 \index{product type|see{pair}}
49 \index{tuple|see{pair}}
51 \underscoreoff
53 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
56 %\sloppy
57 %\binperiod     %%%treat . like a binary operator
59 \begin{document}
60 \title{\includegraphics[scale=.8]{isabelle_hol}
61        \\ \vspace{0.5cm} The Tutorial
62        \\ --- DRAFT ---}
63 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
64 Technische Universit{\"a}t M{\"u}nchen \\
65 Institut f{\"u}r Informatik \\[1ex]
66 University of Cambridge\\
67 Computer Laboratory}
68 \maketitle
70 \pagenumbering{roman}
71 \tableofcontents
73 \subsubsection*{Acknowledgements}
74 This tutorial owes a lot to the constant discussions with and the valuable
75 feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
76 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
77 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
78 read and comment on a draft version.
79 \clearfirst
81 \input{basics}
82 \input{fp}
83 \input{Rules/rules}
84 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
85 \input{Inductive/inductive}
87 \input{Types/types}
88 \chapter{Theory Presentation}
89 \chapter{Case Study: The Needhamd-Schroeder Protocol}
90 \chapter{Structured Proofs}
91 \chapter{Case Study: UNIX File-System Security}
92 %\chapter{The Tricks of the Trade}
93 \input{appendix}
95 \bibliographystyle{plain}
96 \bibliography{../manual}
97 \printindex
98 \end{document}