doc-src/TutorialI/tutorial.tex
 author nipkow Thu Mar 15 10:41:32 2001 +0100 (2001-03-15) changeset 11207 08188224c24e parent 11110 306beb99e192 child 11213 aeb5c72dd72a permissions -rw-r--r--
*** empty log message ***
 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@8743  80 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch  nipkow@10971  81 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!  wenzelm@11067  93 %\chapter{Case Study: Verifying a Cryptographic 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}