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.
\input{style}
\usepackage{graphicx}
\usepackage[colorlinks,hyperindex]{hyperref}
\newcommand{\aufgabe}[3]{
\input{#1/#2/generated/#3}
%\newpage
}
\title{Isabelle/HOL Exercises}
\date{\today}
\author{Gertrud Bauer, Gerwin Klein, Farhad Mehta, Tobias Nipkow,\\
Martin Strecker, Michael Wahler, Markus Wenzel}
\begin{document}
\maketitle
This document presents a collection of exercises for getting
acquainted with the proof assistant
Isabelle/HOL~\cite{isabelle-tutorial}. The exercises come out of an
annual Isabelle/HOL course taught at the Technical University of
Munich. They are arranged in chronological order, and in each year in
ascending order of difficulty.
\tableofcontents
%--------------------------------------------
\newpage
\section{2000}
\aufgabe{2000}{a1}{Snoc}
\aufgabe{2000}{a1}{Arithmetic}
\aufgabe{2000}{a1}{Hanoi}
%\aufgabe{2000}{a2}{BDT}
%\aufgabe{2000}{a2}{OBDT}
%\aufgabe{2000}{a3}{NaturalDeduction}
%\aufgabe{2000}{a3}{HoareLogic}
%\aufgabe{2000}{a4}{CTLexample}
%\aufgabe{2000}{a5}{Unix}
%\section{L{\"o}sungen}
%\aufgabe{2000}{l1}{Snoc}
%\aufgabe{2000}{l1}{Arithmetic}
%\aufgabe{2000}{l1}{Hanoi}
%\aufgabe{2000}{l2}{BDT}
%\aufgabe{2000}{l2}{OBDT}
%\aufgabe{2000}{l3}{NaturalDeduction}
%\aufgabe{2000}{l3}{HoareLogic}
%\aufgabe{2000}{l4}{CTLexample}
%\aufgabe{2000}{l5}{Unix}
%--------------------------------------------
\newpage
\section{2001}
\aufgabe{2001}{a1}{Aufgabe1}
\aufgabe{2001}{a2}{Aufgabe2}
\aufgabe{2001}{a3}{Trie1}
\aufgabe{2001}{a3}{Trie2}
\aufgabe{2001}{a3}{Trie3}
%\aufgabe{2001}{a4}{Aufgabe4}
\aufgabe{2001}{a5}{Aufgabe5}
%\aufgabe{2001}{a5}{PL}
%\aufgabe{2001}{a6}{Aufgabe6}
%\section{L{\"o}sungen}
%\aufgabe{2001}{l1}{Aufgabe1}
%\aufgabe{2001}{l2}{Loesung2}
%\aufgabe{2001}{l3}{Trie1}
%\aufgabe{2001}{l3}{Trie2}
%\aufgabe{2001}{l3}{Trie3}
%\aufgabe{2001}{l4}{Loesung4}
%\aufgabe{2001}{l5}{Loesung5}
%\aufgabe{2001}{l5}{PL}
%\aufgabe{2001}{l6}{Loesung6}
%--------------------------------------------
\newpage
\section{2002}
\aufgabe{2002}{a1}{a1}
\aufgabe{2002}{a2}{a2}
\aufgabe{2002}{a3}{a3}
%\aufgabe{2002}{a4}{a4}
\aufgabe{2002}{a5}{a5}
\aufgabe{2002}{a6}{a6}
%\aufgabe{2002}{a7}{a7}
%\newpage
%\section{L{\"o}sungen}
%\aufgabe{2002}{l1}{l1}
%\aufgabe{2002}{l2}{l2}
%\aufgabe{2002}{l3}{l3}
%\aufgabe{2002}{l4}{l4}
%\aufgabe{2002}{l5}{l5}
%\aufgabe{2002}{l6}{l6}
%\aufgabe{2002}{l7}{ABP}
%\newpage
%\part{Anhang}
%\section{Zu 2000}
%\aufgabe{2000}{a4}{GfpLfp}
%\aufgabe{2000}{a4}{CTL}
%\aufgabe{2000}{a5}{Env}
%\section{Zu 2001}
%\aufgabe{2001}{a6}{Hoare}
%--------------------------------------------
\newpage
\section{2003}
\aufgabe{2003}{a1}{a1}
\aufgabe{2003}{a2}{a2}
\aufgabe{2003}{a3}{a3}
\aufgabe{2003}{a5}{a5}
\aufgabe{2003}{a6}{a6}
%--------------------------------------------
\newpage
\section{2003/2004}
\aufgabe{0304}{a1}{a1}
\aufgabe{0304}{a2}{a2}
\aufgabe{0304}{a3}{a3}
\aufgabe{0304}{a4}{a4}
\aufgabe{0304}{a5}{a5}
%--------------------------------------------
\newpage
\bibliographystyle{abbrv}
\bibliography{exercises}
\end{document}