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