15 Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this |
15 Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this |
16 tutorial initially concentrates on functional programming, do not be |
16 tutorial initially concentrates on functional programming, do not be |
17 misled: HOL can express most mathematical concepts, and functional programming |
17 misled: HOL can express most mathematical concepts, and functional programming |
18 is just one particularly simple and ubiquitous instance. |
18 is just one particularly simple and ubiquitous instance. |
19 |
19 |
20 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. |
20 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has |
21 This has influenced some of HOL's concrete syntax but is otherwise |
21 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant |
22 irrelevant for us because this tutorial is based on |
22 for us because this tutorial is based on |
23 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle |
23 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with |
24 with structured proofs.\footnote{Thus the full name of the system should be |
24 structured proofs. Thus the full name of the system should be |
25 Isabelle/Isar/HOL, but that is a bit of a mouthful.} |
25 Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other |
|
26 implementations of HOL, in particular the one by Mike Gordon \emph{et al.}, |
|
27 which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us, |
|
28 HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL. |
26 |
29 |
27 A tutorial is by definition incomplete. Currently the tutorial only |
30 A tutorial is by definition incomplete. Currently the tutorial only |
28 introduces the rudiments of Isar's proof language. To fully exploit the power |
31 introduces the rudiments of Isar's proof language. To fully exploit the power |
29 of Isar you need to consult the Isabelle/Isar Reference |
32 of Isar you need to consult the Isabelle/Isar Reference |
30 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level |
33 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level |