doc-src/TutorialI/document/natsum.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/natsum.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,232 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{natsum}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\begin{isamarkuptext}%
+\noindent
+In particular, there are \isa{case}-expressions, for example
+\begin{isabelle}%
+\ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ m\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ m%
+\end{isabelle}
+primitive recursion, for example%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ sum\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}sum\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}sum\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n\ {\isaliteral{2B}{\isacharplus}}\ sum\ n{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+and induction, for example%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}sum\ n\ {\isaliteral{2B}{\isacharplus}}\ sum\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\newcommand{\mystar}{*%
+}
+\index{arithmetic operations!for \protect\isa{nat}}%
+The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
+\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
+\sdx{div}, \sdx{mod}, \cdx{min} and
+\cdx{max} are predefined, as are the relations
+\isadxboldpos{\isasymle}{$HOL2arithrel} and
+\isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isaliteral{2D}{\isacharminus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} if
+\isa{m\ {\isaliteral{3C}{\isacharless}}\ n}. There is even a least number operation
+\sdx{LEAST}\@.  For example, \isa{{\isaliteral{28}{\isacharparenleft}}LEAST\ n{\isaliteral{2E}{\isachardot}}\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isadigit{0}}}.
+\begin{warn}\index{overloading}
+  The constants \cdx{0} and \cdx{1} and the operations
+  \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
+  \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+  \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
+  \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
+  not just for natural numbers but for other types as well.
+  For example, given the goal \isa{x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{0}}\ {\isaliteral{3D}{\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{{\isaliteral{2B}{\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\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x}. (In the absence of a numeral,
+  it may take you some time to realize what has happened if \pgmenu{Show
+  Types} is not set).  In this particular example, you need to include
+  an explicit type constraint, for example \isa{x{\isaliteral{2B}{\isacharplus}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}}. If there
+  is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isaliteral{3D}{\isacharequal}}\ x} automatically implies \isa{x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat} because \isa{Suc} is not
+  overloaded.
+
+  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}
+  The symbols \isadxboldpos{>}{$HOL2arithrel} and
+  \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isaliteral{3E}{\isachargreater}}\ y}
+  stands for \isa{y\ {\isaliteral{3C}{\isacharless}}\ x} and similary for \isa{{\isaliteral{5C3C67653E}{\isasymge}}} and
+  \isa{{\isaliteral{5C3C6C653E}{\isasymle}}}.
+\end{warn}
+\begin{warn}
+  Constant \isa{{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat} is defined to equal \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 \isa{Suc}.}
+\end{warn}
+
+Both \isa{auto} and \isa{simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove 
+simple arithmetic goals automatically:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+For efficiency's sake, this built-in prover ignores quantified formulae,
+many logical connectives, and all arithmetic operations apart from addition.
+In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C6F723E}{\isasymor}}\ n\ {\isaliteral{3C}{\isacharless}}\ m{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent The method \methdx{arith} is more general.  It attempts to
+prove the first subgoal provided it is a \textbf{linear arithmetic} formula.
+Such formulas may involve the usual logical connectives (\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}},
+\isa{{\isaliteral{5C3C616E643E}{\isasymand}}}, \isa{{\isaliteral{5C3C6F723E}{\isasymor}}}, \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}, \isa{{\isaliteral{3D}{\isacharequal}}},
+\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}}), the relations \isa{{\isaliteral{3D}{\isacharequal}}},
+\isa{{\isaliteral{5C3C6C653E}{\isasymle}}} and \isa{{\isaliteral{3C}{\isacharless}}}, and the operations \isa{{\isaliteral{2B}{\isacharplus}}}, \isa{{\isaliteral{2D}{\isacharminus}}},
+\isa{min} and \isa{max}.  For example,%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}min\ i\ {\isaliteral{28}{\isacharparenleft}}max\ j\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2A}{\isacharasterisk}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ max\ {\isaliteral{28}{\isacharparenleft}}min\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2A}{\isacharasterisk}}k{\isaliteral{29}{\isacharparenright}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}min\ i\ {\isaliteral{28}{\isacharparenleft}}j{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}arith{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+succeeds because \isa{k\ {\isaliteral{2A}{\isacharasterisk}}\ k} can be treated as atomic. In contrast,%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{2A}{\isacharasterisk}}n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+is not proved by \isa{arith} because the proof relies 
+on properties of multiplication. Only multiplication by numerals (which is
+the same as iterated addition) is taken into account.
+
+\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.
+
+If \isa{k} is a numeral, \sdx{div}~\isa{k}, \sdx{mod}~\isa{k} and
+\isa{k}~\sdx{dvd} are also supported, where the former two are eliminated
+by case distinctions, again blowing up the running time.
+
+If the formula involves quantifiers, \isa{arith} may take
+super-exponential time and space.
+\end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: