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