--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 13:33:45 2001 +0100
@@ -39,37 +39,38 @@
\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}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} if
+\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}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.
-\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}}{\isasymColon}{\isacharprime}a}
-and \isa{{\isadigit{2}}{\isasymColon}{\isacharprime}a} are available as abbreviations for the corresponding
-\isa{Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{sec:numerals}.
-
+\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
\begin{warn}\index{overloading}
- The constant \cdx{0} and the operations
+ The constants \cdx{0} and \cdx{1} 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
not just for natural numbers but at other types as well.
- For example, given the goal \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x},
- there is nothing to indicate that you are talking about natural numbers.
- Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
- \isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
- to prove the goal (although it may take you some time to realize what has
- happened if \isa{show{\isacharunderscore}types} is not set). In this particular example,
- you need to include an explicit type constraint, for example
- \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this
- may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
- \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
+ For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
+ that you are talking about natural numbers. Hence Isabelle can only infer
+ that \isa{x} is of some arbitrary type where \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are
+ declared. As a consequence, you will be unable to prove the
+ goal. To alert you to such pitfalls, Isabelle flags numerals without a
+ fixed type in its output: \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x}. (In the absence of a numeral,
+ it may take you some time to realize what has happened if \isa{show{\isacharunderscore}types} is not set). In this particular example, you need to include
+ an explicit type constraint, for example \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there
+ is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not
+ overloaded.
- 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.
+ For details on overloading see \S\ref{sec:overloading}.
+ Table~\ref{tab:overloading} in the appendix shows the most important
+ overloaded operations.
+\end{warn}
+\begin{warn}
+ Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to be \isa{Suc\ {\isadigit{0}}}. This definition
+ (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
+ tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
+ others (especially the single step tactics in Chapter~\ref{chap:rules}).
+ If you need the full set of numerals, see~\S\ref{sec:numerals}.
+ \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and of \isa{Suc}.}
\end{warn}
Both \isa{auto} and \isa{simp}