doc-src/TutorialI/Misc/document/natsum.tex

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
 \newcommand{\mystar}{*%
 }
+\index{arithmetic operations!for \protect\isa{nat}}%
 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
 \sdx{div}, \sdx{mod}, \cdx{min} and
 \cdx{max} are predefined, as are the relations
 \indexboldpos{\isasymle}{$HOL2arithrel} and
 \ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
 \isa{m\ {\isacharless}\ n}. There is even a least number operation
-\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
-Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
+\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}. 
+\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
+ The following needs changing with our new system of numbers.}
+Note that \isa{{\isadigit{1}}}
 and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
 \isa{Suc}-expressions. If you need the full set of numerals,
 see~\S\ref{sec:numerals}.
 
-\begin{warn}
+\begin{warn}\index{overloading}
   The constant \cdx{0} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available

   For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
   Table~\ref{tab:overloading} in the appendix shows the most important overloaded
   operations.
 \end{warn}
 
-Simple arithmetic goals are proved automatically by both \isa{auto} and the
-simplification method introduced in \S\ref{sec:Simplification}.  For
-example,%
+Both \isa{auto} and \isa{simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove 
+simple arithmetic goals automatically:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
+For efficiency's sake, this built-in prover ignores quantified formulae and all 
+arithmetic operations apart from addition.
 
-For more complex goals, there is the special method \methdx{arith}
-(which attacks the first subgoal). It proves arithmetic goals involving the
+The method \methdx{arith} is more general.  It attempts to prove
+the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
+Such formulas may involve the
 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
 and the operations
-\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
-known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
+\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. 
 For example,%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}%
 \begin{isamarkuptext}%

 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is not even proved by \isa{arith} because the proof relies essentially
+is not proved even by \isa{arith} because the proof relies 
 on properties of multiplication.
 
 \begin{warn}
   The running time of \isa{arith} is exponential in the number of occurrences
   of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   \cdx{max} because they are first eliminated by case distinctions.
 
-  \isa{arith} is incomplete even for the restricted class of
-  linear arithmetic formulae. If divisibility plays a
+  Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   role, it may fail to prove a valid formula, for example
-  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
+  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare.
 \end{warn}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex