doc-src/Exercises/exercises.tex
author kleing
Thu, 05 Dec 2002 17:12:07 +0100
changeset 13739 f5d0a66c8124
child 14498 c770a2f0ea78
permissions -rw-r--r--
exercise collection
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13739
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     1
\input{style}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     2
\usepackage{graphicx}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     3
\usepackage[colorlinks,hyperindex]{hyperref}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     4
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     5
\newcommand{\aufgabe}[3]{
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     6
\input{#1/#2/generated/#3}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     7
%\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     8
}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     9
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    10
\title{Isabelle/HOL Exercises}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    11
\date{\today}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    12
\author{Gertrud Bauer, Gerwin Klein, Tobias Nipkow,\\ Michael Wahler, Markus Wenzel}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    13
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    14
\begin{document}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    15
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    16
\maketitle
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    17
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    18
This document presents a collection of exercises for getting
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    19
acquainted with the proof assistant
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    20
Isabelle/HOL~\cite{isabelle-tutorial}.  The exercises come out of an
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    21
annual Isabelle/HOL course taught at the Technical University of
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    22
Munich. They are arranged in chronological order, and in each year in
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    23
ascending order of difficulty.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    24
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    25
\tableofcontents
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    26
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    27
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    28
%--------------------------------------------
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    29
\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    30
\section{2000}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    31
\aufgabe{2000}{a1}{Snoc}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    32
\aufgabe{2000}{a1}{Arithmetic}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    33
\aufgabe{2000}{a1}{Hanoi}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    34
%\aufgabe{2000}{a2}{BDT}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    35
%\aufgabe{2000}{a2}{OBDT}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    36
%\aufgabe{2000}{a3}{NaturalDeduction}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    37
%\aufgabe{2000}{a3}{HoareLogic}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    38
%\aufgabe{2000}{a4}{CTLexample}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    39
%\aufgabe{2000}{a5}{Unix}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    40
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    41
%\section{L{\"o}sungen}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    42
%\aufgabe{2000}{l1}{Snoc}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    43
%\aufgabe{2000}{l1}{Arithmetic}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    44
%\aufgabe{2000}{l1}{Hanoi}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    45
%\aufgabe{2000}{l2}{BDT}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    46
%\aufgabe{2000}{l2}{OBDT}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    47
%\aufgabe{2000}{l3}{NaturalDeduction}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    48
%\aufgabe{2000}{l3}{HoareLogic}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    49
%\aufgabe{2000}{l4}{CTLexample}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    50
%\aufgabe{2000}{l5}{Unix}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    51
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    52
%--------------------------------------------
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    53
\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    54
\section{2001}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    55
\aufgabe{2001}{a1}{Aufgabe1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    56
\aufgabe{2001}{a2}{Aufgabe2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    57
\aufgabe{2001}{a3}{Trie1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    58
\aufgabe{2001}{a3}{Trie2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    59
\aufgabe{2001}{a3}{Trie3}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    60
%\aufgabe{2001}{a4}{Aufgabe4}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    61
\aufgabe{2001}{a5}{Aufgabe5}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    62
%\aufgabe{2001}{a5}{PL}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    63
%\aufgabe{2001}{a6}{Aufgabe6}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    64
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    65
%\section{L{\"o}sungen}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    66
%\aufgabe{2001}{l1}{Aufgabe1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    67
%\aufgabe{2001}{l2}{Loesung2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    68
%\aufgabe{2001}{l3}{Trie1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    69
%\aufgabe{2001}{l3}{Trie2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    70
%\aufgabe{2001}{l3}{Trie3}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    71
%\aufgabe{2001}{l4}{Loesung4}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    72
%\aufgabe{2001}{l5}{Loesung5}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    73
%\aufgabe{2001}{l5}{PL}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    74
%\aufgabe{2001}{l6}{Loesung6}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    75
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    76
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    77
%--------------------------------------------
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    78
\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    79
\section{2002}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    80
\aufgabe{2002}{a1}{a1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    81
\aufgabe{2002}{a2}{a2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    82
\aufgabe{2002}{a3}{a3}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    83
%\aufgabe{2002}{a4}{a4}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    84
\aufgabe{2002}{a5}{a5}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    85
\aufgabe{2002}{a6}{a6}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    86
%\aufgabe{2002}{a7}{a7}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    87
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    88
%\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    89
%\section{L{\"o}sungen}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    90
%\aufgabe{2002}{l1}{l1}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    91
%\aufgabe{2002}{l2}{l2}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    92
%\aufgabe{2002}{l3}{l3}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    93
%\aufgabe{2002}{l4}{l4}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    94
%\aufgabe{2002}{l5}{l5}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    95
%\aufgabe{2002}{l6}{l6}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    96
%\aufgabe{2002}{l7}{ABP}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    97
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    98
%\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    99
%\part{Anhang}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   100
%\section{Zu 2000}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   101
%\aufgabe{2000}{a4}{GfpLfp}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   102
%\aufgabe{2000}{a4}{CTL}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   103
%\aufgabe{2000}{a5}{Env}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   104
%\section{Zu 2001}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   105
%\aufgabe{2001}{a6}{Hoare}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   106
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   107
\newpage
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   108
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   109
\bibliographystyle{abbrv}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   110
\bibliography{exercises}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   111
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   112
\end{document}