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.
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
\begin{document}
\title{A Compact Overview of Isabelle/HOL}
\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
\small\url{http://www.in.tum.de/~nipkow/}}
\date{}
\maketitle
\noindent
This document is a very compact introduction to the proof assistant
Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
where full explanations and a wealth of additional material can be found.
While reading this document it is recommended to single-step through the
corresponding theories using Isabelle/HOL to follow the proofs.
\section{Functional Programming/Modelling}
\subsection{An Introductory Theory}
\input{FP0.tex}
\begin{exercise}
Define a datatype of binary trees and a function \isa{mirror}
that mirrors a binary tree by swapping subtrees recursively. Prove
\isa{mirror(mirror t) = t}.
Define a function \isa{flatten} that flattens a tree into a list
by traversing it in infix order. Prove
\isa{flatten(mirror t) = rev(flatten t)}.
\end{exercise}
\subsection{More Constructs}
\input{FP1.tex}
\input{RECDEF.tex}
\input{Rules.tex}
\input{Sets.tex}
\input{Ind.tex}
%\input{Isar.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
\bibliographystyle{plain}
\bibliography{root}
\end{document}