1395 |
1395 |
1396 |
1396 |
1397 \subsection{Numerical types and numerical reasoning} |
1397 \subsection{Numerical types and numerical reasoning} |
1398 |
1398 |
1399 The integers (type \tdx{int}) are also available in HOL, and the reals (type |
1399 The integers (type \tdx{int}) are also available in HOL, and the reals (type |
1400 \tdx{real}) are available in the logic image \texttt{HOL-Real}. They support |
1400 \tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support |
1401 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and |
1401 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and |
1402 multiplication (\texttt{*}), and much else. Type \tdx{int} provides the |
1402 multiplication (\texttt{*}), and much else. Type \tdx{int} provides the |
1403 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real |
1403 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real |
1404 division and other operations. Both types belong to class \cldx{linorder}, so |
1404 division and other operations. Both types belong to class \cldx{linorder}, so |
1405 they inherit the relational operators and all the usual properties of linear |
1405 they inherit the relational operators and all the usual properties of linear |
1406 orderings. For full details, please survey the theories in subdirectories |
1406 orderings. For full details, please survey the theories in subdirectories |
1407 \texttt{Integ} and \texttt{Real}. |
1407 \texttt{Integ}, \texttt{Real}, and \texttt{Complex}. |
1408 |
1408 |
1409 All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, |
1409 All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, |
1410 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. |
1410 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. |
1411 Numerals are represented internally by a datatype for binary notation, which |
1411 Numerals are represented internally by a datatype for binary notation, which |
1412 allows numerical calculations to be performed by rewriting. For example, the |
1412 allows numerical calculations to be performed by rewriting. For example, the |