equal
deleted
inserted
replaced
1 \documentclass[11pt,a4paper]{article} |
|
2 \usepackage{isabelle,isabellesym,pdfsetup} |
|
3 |
|
4 %for best-style documents ... |
|
5 \urlstyle{rm} |
|
6 %\isabellestyle{it} |
|
7 |
|
8 \newtheorem{Exercise}{Exercise}[section] |
|
9 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
10 |
|
11 \begin{document} |
|
12 |
|
13 \title{A Compact Overview of Isabelle/HOL} |
|
14 \author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\ |
|
15 \small\url{http://www.in.tum.de/~nipkow/}} |
|
16 \date{} |
|
17 \maketitle |
|
18 |
|
19 \noindent |
|
20 This document is a very compact introduction to the proof assistant |
|
21 Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283} |
|
22 where full explanations and a wealth of additional material can be found. |
|
23 |
|
24 While reading this document it is recommended to single-step through the |
|
25 corresponding theories using Isabelle/HOL to follow the proofs. |
|
26 |
|
27 \section{Functional Programming/Modelling} |
|
28 |
|
29 \subsection{An Introductory Theory} |
|
30 \input{FP0.tex} |
|
31 |
|
32 \begin{exercise} |
|
33 Define a datatype of binary trees and a function \isa{mirror} |
|
34 that mirrors a binary tree by swapping subtrees recursively. Prove |
|
35 \isa{mirror(mirror t) = t}. |
|
36 |
|
37 Define a function \isa{flatten} that flattens a tree into a list |
|
38 by traversing it in infix order. Prove |
|
39 \isa{flatten(mirror t) = rev(flatten t)}. |
|
40 \end{exercise} |
|
41 |
|
42 \subsection{More Constructs} |
|
43 \input{FP1.tex} |
|
44 |
|
45 \input{RECDEF.tex} |
|
46 |
|
47 \input{Rules.tex} |
|
48 |
|
49 \input{Sets.tex} |
|
50 |
|
51 \input{Ind.tex} |
|
52 |
|
53 %\input{Isar.tex} |
|
54 |
|
55 %%% Local Variables: |
|
56 %%% mode: latex |
|
57 %%% TeX-master: "root" |
|
58 %%% End: |
|
59 |
|
60 |
|
61 \bibliographystyle{plain} |
|
62 \bibliography{root} |
|
63 |
|
64 \end{document} |
|