equal
deleted
inserted
replaced
1 \chapter{Basic Concepts} |
1 \chapter{Basic Concepts} |
2 |
2 |
3 \section{Introduction} |
3 \section{Introduction} |
4 |
4 |
5 This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and |
5 This book is a tutorial on how to use the theorem prover Isabelle/HOL as a |
6 verification system. Isabelle is a generic system for implementing logical |
6 specification and verification system. Isabelle is a generic system for |
7 formalisms, and Isabelle/HOL is the specialization of Isabelle for |
7 implementing logical formalisms, and Isabelle/HOL is the specialization |
8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step |
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
9 following the equation |
9 HOL step by step following the equation |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
11 We do not assume that the reader is familiar with mathematical logic but that |
11 We do not assume that the reader is familiar with mathematical logic but that |
12 (s)he is used to logical and set theoretic notation, such as covered |
12 (s)he is used to logical and set theoretic notation, such as covered |
13 in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume |
13 in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume |
14 that the reader is familiar with the basic concepts of functional |
14 that the reader is familiar with the basic concepts of functional |