13497
|
1 |
% latex main
|
|
2 |
% dvips -Pprosper -o main.ps main.dvi
|
|
3 |
% ps2pdf main.ps main.pdf
|
|
4 |
\documentclass[pdf,nototal,myframes,slideColor,colorBG]{prosper}
|
|
5 |
|
|
6 |
\usepackage{pstricks,pst-node,pst-text,pst-3d}
|
40945
|
7 |
\usepackage[utf8]{inputenc}
|
13497
|
8 |
\usepackage{amsmath}
|
|
9 |
|
|
10 |
|
|
11 |
\usepackage{graphicx,color,latexsym}
|
|
12 |
|
|
13 |
\newenvironment{cslide}[1]{\begin{slide}{\blue #1}}{\end{slide}}
|
|
14 |
\newcommand{\emcolorbox}[1]{\colorbox{yellow}{#1}}
|
|
15 |
|
|
16 |
\slideCaption{}
|
|
17 |
|
|
18 |
\begin{document}
|
|
19 |
|
|
20 |
\title{Isabelle/HOL --- A Practical Introduction}
|
|
21 |
\author{Tobias Nipkow
|
|
22 |
\\{\small joint work with Larry Paulson and Markus Wenzel}
|
|
23 |
}
|
40945
|
24 |
\institution{Technische Universität München
|
13497
|
25 |
\\ \vspace{0.5cm}\includegraphics[scale=.4]{isabelle_hol}
|
|
26 |
}
|
|
27 |
\maketitle
|
|
28 |
|
|
29 |
%-----------------------------------------------------------------------------
|
|
30 |
\begin{cslide}{What is {\blue Isabelle}?}
|
|
31 |
\begin{itemize}
|
|
32 |
\item A \emph{logical framwork}
|
|
33 |
\item A generic theorem prover
|
|
34 |
\item A system for implementing proof assistants
|
|
35 |
\end{itemize}
|
|
36 |
\end{cslide}
|
|
37 |
%-----------------------------------------------------------------------------
|
|
38 |
\overlays{5}{
|
|
39 |
\begin{cslide}{What is {\blue Isabelle/HOL}?}
|
|
40 |
\FromSlide{2}
|
|
41 |
\begin{itemize}
|
|
42 |
\item An interactive proof assistant
|
|
43 |
\FromSlide{3}
|
|
44 |
\item {\small for higher-order logic}
|
|
45 |
\FromSlide{4}
|
|
46 |
\item Similar to HOL, PVS, Coq, \dots
|
|
47 |
\FromSlide{5}
|
|
48 |
\item But different enough (e.g. \emph{structured proofs})
|
|
49 |
\end{itemize}
|
|
50 |
\end{cslide}}
|
|
51 |
%-----------------------------------------------------------------------------
|
|
52 |
\overlays{2}{
|
|
53 |
\begin{cslide}{Why Theorem Proving/Verification/\dots?}
|
|
54 |
\FromSlide{2}
|
|
55 |
\vfill
|
|
56 |
\begin{center}
|
|
57 |
\Large \emph{\red Because!}
|
|
58 |
\end{center}
|
|
59 |
\vfill
|
|
60 |
\end{cslide}}
|
|
61 |
%-----------------------------------------------------------------------------
|
|
62 |
\overlays{2}{
|
|
63 |
\begin{cslide}{Overview of course}
|
|
64 |
\begin{enumerate}
|
|
65 |
\item Introduction to Isabelle/HOL (LNCS 2283)
|
|
66 |
\begin{itemize}
|
|
67 |
\item Definitions (datatypes, functions, relations, \dots)
|
|
68 |
\item Proofs (tactic style)
|
|
69 |
\end{itemize}
|
|
70 |
\FromSlide{2}
|
|
71 |
\item Structured proofs (\emph{Isar})
|
|
72 |
\end{enumerate}
|
|
73 |
\end{cslide}}
|
|
74 |
%-----------------------------------------------------------------------------
|
|
75 |
\overlays{2}{
|
|
76 |
\begin{cslide}{Proof styles}
|
|
77 |
\begin{tabular}{cc}
|
|
78 |
\begin{tabular}{l}
|
|
79 |
\texttt{apply(induct\_tac $x$)}\\
|
|
80 |
\texttt{apply simp}\\
|
|
81 |
\texttt{apply(rule allI)+}\\
|
|
82 |
\texttt{apply assumption}\\
|
|
83 |
\vdots
|
|
84 |
\end{tabular}
|
|
85 |
&
|
|
86 |
\FromSlide{2}
|
|
87 |
\begin{tabular}{l}
|
|
88 |
\texttt{proof (induct $x$)}\\
|
|
89 |
\quad \texttt{show $P(0)$ by simp}\\
|
|
90 |
\texttt{next}\\
|
|
91 |
\quad \texttt{assume $P(n)$}\\
|
|
92 |
\quad \texttt{hence $Q$ by simp}\\
|
|
93 |
\quad \texttt{thus $P(n+1)$ by blast}\\
|
|
94 |
\texttt{qed}
|
|
95 |
\end{tabular}\\\\
|
|
96 |
Tactic style & \FromSlide{2} Structured (Mizar, Isar)
|
|
97 |
\end{tabular}
|
|
98 |
\end{cslide}}
|
|
99 |
%-----------------------------------------------------------------------------
|
|
100 |
\begin{cslide}{}
|
|
101 |
\vfill
|
|
102 |
\begin{center}
|
|
103 |
\Large Part 1\\[2em]
|
|
104 |
Introduction to Isabelle/HOL
|
|
105 |
\end{center}
|
|
106 |
\end{cslide}
|
|
107 |
%-----------------------------------------------------------------------------
|
|
108 |
\begin{cslide}{Overview of Part 1}
|
|
109 |
\begin{itemize}
|
|
110 |
\item Functional Programming
|
|
111 |
\item Logic
|
|
112 |
\item Sets and Relations
|
|
113 |
\end{itemize}
|
|
114 |
\end{cslide}
|
|
115 |
%-----------------------------------------------------------------------------
|
13562
|
116 |
\overlays{2}{
|
13497
|
117 |
\begin{cslide}{Functional Programming}
|
|
118 |
\begin{itemize}
|
|
119 |
\item An introductory example
|
|
120 |
\item Proof by simplification
|
|
121 |
\item Case study: Expression compiler
|
|
122 |
\item Advanced datatypes
|
|
123 |
\item Advanced recursive functions
|
|
124 |
\end{itemize}
|
13562
|
125 |
\FromSlide{2}
|
|
126 |
There is more:\\
|
|
127 |
\emph{\blue records},
|
|
128 |
\emph{\blue (axiomatic) type classes},
|
|
129 |
\emph{\blue program extraction}, \dots!
|
|
130 |
\end{cslide}}
|
13497
|
131 |
%-----------------------------------------------------------------------------
|
|
132 |
\begin{cslide}{Logic (Natural Deduction)}
|
|
133 |
\begin{itemize}
|
|
134 |
\item Propositional logic
|
|
135 |
\item Quantifiers
|
|
136 |
\item Automation
|
|
137 |
\item Forward proof
|
|
138 |
\end{itemize}
|
|
139 |
\end{cslide}
|
|
140 |
%-----------------------------------------------------------------------------
|
|
141 |
\begin{cslide}{Sets and Relations}
|
|
142 |
\begin{itemize}
|
|
143 |
\item Introduction to the library
|
|
144 |
\item Case study: verified model checking
|
|
145 |
\item Inductively defined sets
|
|
146 |
\end{itemize}
|
|
147 |
\end{cslide}
|
|
148 |
%-----------------------------------------------------------------------------
|
|
149 |
\begin{cslide}{}
|
|
150 |
\vfill
|
|
151 |
\begin{center}
|
|
152 |
\Large Part 2\\[2em]
|
|
153 |
Structured Proofs in Isabelle/Isar/HOL
|
|
154 |
\end{center}
|
|
155 |
\end{cslide}
|
|
156 |
%-----------------------------------------------------------------------------
|
|
157 |
\begin{cslide}{Motto}
|
|
158 |
\vfill
|
|
159 |
\begin{center}
|
|
160 |
\Large\emcolorbox{Proofs should be readable}
|
|
161 |
\end{center}
|
|
162 |
\end{cslide}
|
|
163 |
%-----------------------------------------------------------------------------
|
|
164 |
\begin{cslide}{Why Readable Proofs?}
|
|
165 |
\begin{itemize}
|
|
166 |
\item Communication
|
|
167 |
\item Maintenance
|
|
168 |
\end{itemize}
|
|
169 |
\end{cslide}
|
|
170 |
%-----------------------------------------------------------------------------
|
|
171 |
\overlays{2}{
|
|
172 |
\begin{cslide}{A Proof Skeleton}
|
|
173 |
\begin{tabular}{l}
|
|
174 |
\textbf{proof}\\
|
|
175 |
\quad\textbf{assume} {\blue\sl assumption}\\
|
|
176 |
\quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\
|
|
177 |
\quad\vdots\\
|
|
178 |
\quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\
|
13562
|
179 |
\quad\textbf{show} {\blue\sl conclusion} \textbf{by} ...\\
|
13497
|
180 |
\textbf{qed}
|
|
181 |
\end{tabular}
|
|
182 |
\bigskip
|
|
183 |
|
|
184 |
\FromSlide{2}
|
|
185 |
Proves {\blue\sl assumption $\Longrightarrow$ conclusion}
|
|
186 |
\end{cslide}}
|
|
187 |
%-----------------------------------------------------------------------------
|
|
188 |
\overlays{2}{
|
|
189 |
\begin{cslide}{Proofs and Statements}
|
|
190 |
\begin{center}
|
|
191 |
\begin{tabular}{@{}lrl@{}}
|
|
192 |
\emph{proof} & ::= & \textbf{proof} \emph{statement}* \textbf{qed} \\
|
|
193 |
&$\mid$& \textbf{by} \emph{method}\\[2ex]
|
|
194 |
\FromSlide{2}
|
|
195 |
\emph{statement} &\FromSlide{2}::= & \FromSlide{2}\textbf{assume} \emph{propositions} \\
|
|
196 |
&\FromSlide{2}$\mid$& \FromSlide{2}(\textbf{show} $\mid$ \textbf{have})
|
|
197 |
\emph{proposition} \emph{proof}
|
|
198 |
\end{tabular}
|
|
199 |
\end{center}
|
|
200 |
\end{cslide}}
|
|
201 |
%-----------------------------------------------------------------------------
|
|
202 |
\begin{cslide}{Overview of Part 2}
|
|
203 |
\begin{itemize}
|
|
204 |
\item Logic
|
|
205 |
\item Induction
|
13562
|
206 |
\item Calculation
|
13497
|
207 |
\end{itemize}
|
|
208 |
\end{cslide}
|
|
209 |
%-----------------------------------------------------------------------------
|
|
210 |
|
|
211 |
\end{document}
|
|
212 |
|
|
213 |
%%% Local Variables:
|
|
214 |
%%% mode: latex
|
|
215 |
%%% TeX-master: t
|
|
216 |
%%% End:
|