8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step |
8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step |
9 following the equation |
9 following the equation |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
11 We assume that the reader is familiar with the basic concepts of both fields. |
11 We assume that the reader is familiar with the basic concepts of both fields. |
12 For excellent introductions to functional programming consult the textbooks |
12 For excellent introductions to functional programming consult the textbooks |
13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although |
13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although |
14 this tutorial initially concentrates on functional programming, do not be |
14 this tutorial initially concentrates on functional programming, do not be |
15 misled: HOL can express most mathematical concepts, and functional |
15 misled: HOL can express most mathematical concepts, and functional |
16 programming is just one particularly simple and ubiquitous instance. |
16 programming is just one particularly simple and ubiquitous instance. |
17 |
17 |
18 A tutorial is by definition incomplete. To fully exploit the power of the |
18 A tutorial is by definition incomplete. To fully exploit the power of the |
19 system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man} |
19 system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref} |
20 for details about Isabelle and the HOL chapter of the Logics |
20 for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL} |
21 manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a |
21 for details relating to HOL. Both manuals have a comprehensive index. |
22 comprehensive index. |
|
23 |
22 |
24 \section{Theories, proofs and interaction} |
23 \section{Theories, proofs and interaction} |
25 \label{sec:Basic:Theories} |
24 \label{sec:Basic:Theories} |
26 |
25 |
27 Working with Isabelle means creating two different kinds of documents: |
26 Working with Isabelle means creating two different kinds of documents: |
56 \end{warn} |
55 \end{warn} |
57 |
56 |
58 This tutorial is concerned with introducing you to the different linguistic |
57 This tutorial is concerned with introducing you to the different linguistic |
59 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. |
58 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. |
60 A complete grammar of the basic constructs is found in Appendix~A |
59 A complete grammar of the basic constructs is found in Appendix~A |
61 of~\cite{Isa-Ref-Man}, for reference in times of doubt. |
60 of~\cite{isabelle-ref}, for reference in times of doubt. |
62 |
61 |
63 The tutorial is also concerned with showing you how to prove theorems about |
62 The tutorial is also concerned with showing you how to prove theorems about |
64 the concepts in a theory. This involves invoking predefined theorem proving |
63 the concepts in a theory. This involves invoking predefined theorem proving |
65 commands. Because Isabelle is written in the programming language |
64 commands. Because Isabelle is written in the programming language |
66 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not |
65 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not |