diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 16:08:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-%
-\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: