doc-src/TutorialI/tutorial.tex
author paulson
Tue Apr 10 16:11:01 2001 +0200 (2001-04-10)
changeset 11249 a0e3c67c1394
parent 11213 aeb5c72dd72a
child 11389 55e2aef8909b
permissions -rw-r--r--
Protocols chapter
paulson@10399
     1
\documentclass{article}
paulson@10298
     2
\newif\ifremarks
wenzelm@11110
     3
%\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
wenzelm@11110
     4
\remarksfalse
paulson@10399
     5
\usepackage{cl2emono-modified,isabelle,isabellesym}
paulson@10597
     6
\usepackage{../proof,amsmath,amsfonts}
wenzelm@9695
     7
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
wenzelm@8847
     8
\usepackage{../pdfsetup}    %last package!
nipkow@8743
     9
nipkow@8743
    10
%\newtheorem{theorem}{Theorem}[section]
nipkow@8743
    11
\newtheorem{Exercise}{Exercise}[section]
nipkow@8743
    12
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
nipkow@8743
    13
\newcommand{\ttlbr}{\texttt{[|}}
nipkow@8743
    14
\newcommand{\ttrbr}{\texttt{|]}}
nipkow@8743
    15
\newcommand{\ttor}{\texttt{|}}
nipkow@8743
    16
\newcommand{\ttall}{\texttt{!}}
nipkow@8743
    17
\newcommand{\ttuniquex}{\texttt{?!}}
nipkow@8743
    18
\newcommand{\ttEXU}{\texttt{EX!}}
nipkow@8743
    19
\newcommand{\ttAnd}{\texttt{!!}}
nipkow@8743
    20
nipkow@8743
    21
\newcommand{\isasymimp}{\isasymlongrightarrow}
nipkow@8743
    22
\newcommand{\isasymImp}{\isasymLongrightarrow}
nipkow@8743
    23
\newcommand{\isasymFun}{\isasymRightarrow}
wenzelm@10272
    24
\newcommand{\isasymuniqex}{\isamath{\exists!\,}}
paulson@10885
    25
\renewcommand{\S}{Sect.\ts}
nipkow@8743
    26
nipkow@8743
    27
\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
nipkow@8743
    28
paulson@10298
    29
%% lcp's macros
paulson@10399
    30
\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
paulson@10298
    31
\newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
paulson@10298
    32
\let\bigisa=\isa
paulson@10298
    33
%% was previously
paulson@10298
    34
%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} 
paulson@10298
    35
%% because \isa is too small for variables, but does it really matter?
paulson@10298
    36
paulson@10298
    37
nipkow@8743
    38
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
nipkow@8743
    39
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
nipkow@8743
    40
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
nipkow@8743
    41
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
nipkow@8743
    42
%% run    ../sedindex logics    to prepare index file
nipkow@8743
    43
nipkow@8743
    44
\makeindex
nipkow@8743
    45
\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
nipkow@8743
    46
\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
nipkow@8743
    47
\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
nipkow@8743
    48
\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
nipkow@8743
    49
nipkow@10654
    50
\index{termination|see{total function}}
nipkow@10543
    51
\index{product type|see{pair}}
nipkow@10543
    52
\index{tuple|see{pair}}
nipkow@10654
    53
\index{*<*lex*>|see{lexicographic product}}
nipkow@10543
    54
nipkow@8743
    55
\underscoreoff
nipkow@8743
    56
nipkow@8743
    57
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
nipkow@8743
    58
nipkow@8743
    59
\pagestyle{headings}
nipkow@8743
    60
%\sloppy
nipkow@8743
    61
%\binperiod     %%%treat . like a binary operator
nipkow@8743
    62
nipkow@8743
    63
\begin{document}
nipkow@8743
    64
\title{\includegraphics[scale=.8]{isabelle_hol}
nipkow@8743
    65
       \\ \vspace{0.5cm} The Tutorial
nipkow@8743
    66
       \\ --- DRAFT ---}
nipkow@10340
    67
\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
nipkow@10178
    68
Technische Universit{\"a}t M{\"u}nchen \\
nipkow@10340
    69
Institut f{\"u}r Informatik \\[1ex]
nipkow@10340
    70
University of Cambridge\\
nipkow@10340
    71
Computer Laboratory}
nipkow@8743
    72
\maketitle
nipkow@8743
    73
nipkow@8743
    74
\pagenumbering{roman}
nipkow@8743
    75
\tableofcontents
nipkow@8743
    76
nipkow@8743
    77
\subsubsection*{Acknowledgements}
nipkow@8743
    78
This tutorial owes a lot to the constant discussions with and the valuable
nipkow@10971
    79
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
nipkow@11213
    80
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch,
nipkow@11213
    81
Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to
nipkow@8743
    82
read and comment on a draft version.
nipkow@8743
    83
\clearfirst
nipkow@8743
    84
nipkow@8743
    85
\input{basics}
nipkow@8743
    86
\input{fp}
paulson@10298
    87
\input{Rules/rules}
paulson@10298
    88
\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212
    89
\input{Inductive/inductive}
nipkow@10676
    90
\input{Types/types}
nipkow@9958
    91
\input{Advanced/advanced}
nipkow@11207
    92
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
paulson@11249
    93
\input{Protocol/protocol}
wenzelm@11067
    94
%\chapter{Structured Proofs}
wenzelm@11067
    95
%\label{ch:Isar}
nipkow@10971
    96
%\chapter{Case Study: UNIX File-System Security}
nipkow@9958
    97
%\chapter{The Tricks of the Trade}
nipkow@8743
    98
\input{appendix}
nipkow@8743
    99
nipkow@8743
   100
\bibliographystyle{plain}
nipkow@8743
   101
\bibliography{../manual}
wenzelm@8828
   102
\printindex
nipkow@8743
   103
\end{document}