doc-src/TutorialI/tutorial.sty

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

% tutorial.sty : Isabelle Tutorial Page Layout
%
\typeout{Document Style tutorial. Released 9 July 2001}

\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
\hyphenation{data-type data-types co-data-type co-data-types }

%usage: \iflabelundefined{LABEL}{if not defined}{if defined}
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}


%%%INDEXING  use isa-index to process the index

\newcommand\seealso[2]{\emph{see also} #1}
\usepackage{makeidx}

%index, putting page numbers of definitions in boldface
\def\bold#1{\textbf{#1}}
\newcommand\fnote[1]{#1n}
\newcommand\indexbold[1]{\index{#1|bold}}

% The alternative to \protect\isa in the indexing macros is
% \noexpand\noexpand \noexpand\isa
% need TWO levels of \noexpand to delay the expansion of \isa:
%  the \noexpand\noexpand will leave one \noexpand, to be given to the
%  (still unexpanded) \isa token.  See TeX by Topic, page 122.

%%%% for indexing constants, symbols, theorems, ...
\newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}}
\newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}}

\newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}}
\newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}

\newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}}
\newcommand\tydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type)}}
\newcommand\tcdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type class)}}
\newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}}

\newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}}
\newcommand\cmmdx[1]{\index{#1@\protect\isacommand{#1} (command)}}
\newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1} (command)}}
\newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}}
\newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}}
\newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}}

%set argument in \bf font and index in ROMAN font (for definitions in text!)
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}

\newcommand\rmindex[1]{{#1}\index{#1}\@}
\newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
\newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}

%Commented-out the original versions to see what the index looks like without them.
%   In any event, they need to use \isa or \protect\isa rather than \texttt.
%%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
%%\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
\newcommand{\indexboldpos}[2]{#1\@}
\newcommand{\ttindexboldpos}[2]{\isa{#1}\@}

%\newtheorem{theorem}{Theorem}[section]
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
\newcommand{\ttlbr}{\texttt{[|}}
\newcommand{\ttrbr}{\texttt{|]}}
\newcommand{\ttor}{\texttt{|}}
\newcommand{\ttall}{\texttt{!}}
\newcommand{\ttuniquex}{\texttt{?!}}
\newcommand{\ttEXU}{\texttt{EX!}}
\newcommand{\ttAnd}{\texttt{!!}}

\newcommand{\isasymignore}{}
\newcommand{\isasymimp}{\isasymlongrightarrow}
\newcommand{\isasymImp}{\isasymLongrightarrow}
\newcommand{\isasymFun}{\isasymRightarrow}
\newcommand{\isasymuniqex}{\isamath{\exists!\,}}
\renewcommand{\S}{Sect.\ts}

\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}

\newif\ifremarks
\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}

%names of Isabelle rules
\newcommand{\rulename}[1]{\hfill(#1)}
\newcommand{\rulenamedx}[1]{\hfill(#1\index{#1@\protect\isa{#1} (theorem)|bold})}

%%%% meta-logical connectives

\let\Forall=\bigwedge
\let\Imp=\Longrightarrow
\let\To=\Rightarrow
\newcommand{\Var}[1]{{?\!#1}}

%%% underscores as ordinary characters, not for subscripting
%%  use @ or \sb for subscripting; use \at for @
%%  only works in \tt font
%%  must not make _ an active char; would make \ttindex fail!
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
\gdef\underscoreon{\catcode`\_=8\makeatother}
\chardef\other=12
\chardef\at=`\@

% alternative underscore
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}


%%%% ``WARNING'' environment
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
         \small %%WAS\baselineskip=0.9\baselineskip
         \noindent \hangindent\parindent \hangafter=-2 
         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
        {\par\endgroup\medbreak}


%%%% Standard logical symbols
\let\turn=\vdash
\let\conj=\wedge
\let\disj=\vee
\let\imp=\rightarrow
\let\bimp=\leftrightarrow
\newcommand\all[1]{\forall#1.}  %quantification
\newcommand\ex[1]{\exists#1.}
\newcommand{\pair}[1]{\langle#1\rangle}

\newcommand{\lparr}{\mathopen{(\!|}}
\newcommand{\rparr}{\mathclose{|\!)}}
\newcommand{\fs}{\mathpunct{,\,}}
\newcommand{\ty}{\mathrel{::}}
\newcommand{\asn}{\mathrel{:=}}
\newcommand{\more}{\ldots}
\newcommand{\record}[1]{\lparr #1 \rparr}
\newcommand{\dtt}{\mathord.}

\newcommand\lbrakk{\mathopen{[\![}}
\newcommand\rbrakk{\mathclose{]\!]}}
\newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
\newcommand{\Text}[1]{\mbox{#1}}

\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\mathit{\dshsym}}

\let\int=\cap
\let\un=\cup
\let\inter=\bigcap
\let\union=\bigcup

\def\ML{{\sc ml}}
\def\AST{{\sc ast}}

%macros to change the treatment of symbols
\def\relsemicolon{\mathcode`\;="303B}   %treat ; like a relation
\def\binperiod{\mathcode`\.="213A}   %treat . like a binary operator
\def\binvert{\mathcode`\|="226A}     %treat | like a binary operator

%redefinition of \sloppy and \fussy to use \emergencystretch
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}

%non-bf version of description
\def\descrlabel#1{\hspace\labelsep #1}
\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
\let\enddescr\endlist

% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
% generate text italic rather than math italic by default. This makes
% multi-letter identifiers look better. The mathcode for character c
% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
%
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
        \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
        \advance\count0 by1 \advance\count1 by1 \repeat}}
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}