36 and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding |
36 and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding |
37 \isa{Suc}-expressions. If you need the full set of numerals, |
37 \isa{Suc}-expressions. If you need the full set of numerals, |
38 see~\S\ref{sec:numerals}. |
38 see~\S\ref{sec:numerals}. |
39 |
39 |
40 \begin{warn} |
40 \begin{warn} |
41 The constant \ttindexbold{0} and the operations |
41 The constant \cdx{0} and the operations |
42 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
42 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
43 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |
43 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |
44 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and |
44 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and |
45 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available |
45 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available |
46 not just for natural numbers but at other types as well. |
46 not just for natural numbers but at other types as well. |
68 \begin{isamarkuptext}% |
68 \begin{isamarkuptext}% |
69 \noindent |
69 \noindent |
70 is proved automatically. The main restriction is that only addition is taken |
70 is proved automatically. The main restriction is that only addition is taken |
71 into account; other arithmetic operations and quantified formulae are ignored. |
71 into account; other arithmetic operations and quantified formulae are ignored. |
72 |
72 |
73 For more complex goals, there is the special method \isaindexbold{arith} |
73 For more complex goals, there is the special method \methdx{arith} |
74 (which attacks the first subgoal). It proves arithmetic goals involving the |
74 (which attacks the first subgoal). It proves arithmetic goals involving the |
75 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}}, |
75 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}}, |
76 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}}, |
76 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}}, |
77 and the operations |
77 and the operations |
78 \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is |
78 \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is |