|
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} |
|
7 \usepackage[latin1]{inputenc} |
|
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 } |
|
24 \institution{Technische Universität München |
|
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 %----------------------------------------------------------------------------- |
|
116 \begin{cslide}{Functional Programming} |
|
117 \begin{itemize} |
|
118 \item An introductory example |
|
119 \item Proof by simplification |
|
120 \item Case study: Expression compiler |
|
121 \item Advanced datatypes |
|
122 \item Advanced recursive functions |
|
123 \end{itemize} |
|
124 \end{cslide} |
|
125 %----------------------------------------------------------------------------- |
|
126 \begin{cslide}{Logic (Natural Deduction)} |
|
127 \begin{itemize} |
|
128 \item Propositional logic |
|
129 \item Quantifiers |
|
130 \item Automation |
|
131 \item Forward proof |
|
132 \end{itemize} |
|
133 \end{cslide} |
|
134 %----------------------------------------------------------------------------- |
|
135 \begin{cslide}{Sets and Relations} |
|
136 \begin{itemize} |
|
137 \item Introduction to the library |
|
138 \item Case study: verified model checking |
|
139 \item Inductively defined sets |
|
140 \end{itemize} |
|
141 \end{cslide} |
|
142 %----------------------------------------------------------------------------- |
|
143 \begin{cslide}{} |
|
144 \vfill |
|
145 \begin{center} |
|
146 \Large Part 2\\[2em] |
|
147 Structured Proofs in Isabelle/Isar/HOL |
|
148 \end{center} |
|
149 \end{cslide} |
|
150 %----------------------------------------------------------------------------- |
|
151 \begin{cslide}{Motto} |
|
152 \vfill |
|
153 \begin{center} |
|
154 \Large\emcolorbox{Proofs should be readable} |
|
155 \end{center} |
|
156 \end{cslide} |
|
157 %----------------------------------------------------------------------------- |
|
158 \begin{cslide}{Why Readable Proofs?} |
|
159 \begin{itemize} |
|
160 \item Communication |
|
161 \item Maintenance |
|
162 \end{itemize} |
|
163 \end{cslide} |
|
164 %----------------------------------------------------------------------------- |
|
165 \overlays{2}{ |
|
166 \begin{cslide}{A Proof Skeleton} |
|
167 \begin{tabular}{l} |
|
168 \textbf{proof}\\ |
|
169 \quad\textbf{assume} {\blue\sl assumption}\\ |
|
170 \quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\ |
|
171 \quad\vdots\\ |
|
172 \quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\ |
|
173 \quad\textbf{show} {\blue\sl conclusion}\\ |
|
174 \textbf{qed} |
|
175 \end{tabular} |
|
176 \bigskip |
|
177 |
|
178 \FromSlide{2} |
|
179 Proves {\blue\sl assumption $\Longrightarrow$ conclusion} |
|
180 \end{cslide}} |
|
181 %----------------------------------------------------------------------------- |
|
182 \overlays{2}{ |
|
183 \begin{cslide}{Proofs and Statements} |
|
184 \begin{center} |
|
185 \begin{tabular}{@{}lrl@{}} |
|
186 \emph{proof} & ::= & \textbf{proof} \emph{statement}* \textbf{qed} \\ |
|
187 &$\mid$& \textbf{by} \emph{method}\\[2ex] |
|
188 \FromSlide{2} |
|
189 \emph{statement} &\FromSlide{2}::= & \FromSlide{2}\textbf{assume} \emph{propositions} \\ |
|
190 &\FromSlide{2}$\mid$& \FromSlide{2}(\textbf{show} $\mid$ \textbf{have}) |
|
191 \emph{proposition} \emph{proof} |
|
192 \end{tabular} |
|
193 \end{center} |
|
194 \end{cslide}} |
|
195 %----------------------------------------------------------------------------- |
|
196 \begin{cslide}{Overview of Part 2} |
|
197 \begin{itemize} |
|
198 \item Logic |
|
199 \item Induction |
|
200 \end{itemize} |
|
201 \end{cslide} |
|
202 %----------------------------------------------------------------------------- |
|
203 |
|
204 \end{document} |
|
205 |
|
206 %%% Local Variables: |
|
207 %%% mode: latex |
|
208 %%% TeX-master: t |
|
209 %%% End: |