doc-src/TutorialI/tutorial.tex
 author nipkow Mon Mar 19 12:38:36 2001 +0100 (2001-03-19) changeset 11213 aeb5c72dd72a parent 11207 08188224c24e child 11249 a0e3c67c1394 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 \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 %\chapter{Case Study: Verifying a Cryptographic 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}