10 zero and successor, so it works well with inductive proofs and primitive |
10 zero and successor, so it works well with inductive proofs and primitive |
11 recursive function definitions. HOL also provides the type |
11 recursive function definitions. HOL also provides the type |
12 \isa{int} of \textbf{integers}, which lack induction but support true |
12 \isa{int} of \textbf{integers}, which lack induction but support true |
13 subtraction. The integers are preferable to the natural numbers for reasoning about |
13 subtraction. The integers are preferable to the natural numbers for reasoning about |
14 complicated arithmetic expressions, even for some expressions whose |
14 complicated arithmetic expressions, even for some expressions whose |
15 value is non-negative. The logic HOL-Real also has the type |
15 value is non-negative. The logic HOL-Complex also has the types |
16 \isa{real} of real numbers. Isabelle has no subtyping, so the numeric |
16 \isa{real} and \isa{complex}: the real and complex numbers. Isabelle has no |
17 types are distinct and there are functions to convert between them. |
17 subtyping, so the numeric |
|
18 types are distinct and there are functions to convert between them. |
18 Fortunately most numeric operations are overloaded: the same symbol can be |
19 Fortunately most numeric operations are overloaded: the same symbol can be |
19 used at all numeric types. Table~\ref{tab:overloading} in the appendix |
20 used at all numeric types. Table~\ref{tab:overloading} in the appendix |
20 shows the most important operations, together with the priorities of the |
21 shows the most important operations, together with the priorities of the |
21 infix symbols. |
22 infix symbols. |
22 |
23 |
361 is |
362 is |
362 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of |
363 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of |
363 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.% |
364 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.% |
364 \index{integers|)}\index{*int (type)|)} |
365 \index{integers|)}\index{*int (type)|)} |
365 |
366 |
366 Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound. There are four rules for integer induction, corresponding to the possible relations of the bound ($\ge$, $>$, $\le$ and $<$): |
367 Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound. There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$): |
367 \begin{isabelle} |
368 \begin{isabelle} |
368 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
369 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
369 \rulename{int_ge_induct}\isanewline |
370 \rulename{int_ge_induct}\isanewline |
370 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
371 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
371 \rulename{int_gr_induct}\isanewline |
372 \rulename{int_gr_induct}\isanewline |