doc-src/TutorialI/Misc/document/natsum.tex
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 27168 9a9cc62932d9
child 40685 313a24b66a8d
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{natsum}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 %
    11 \endisatagtheory
    12 {\isafoldtheory}%
    13 %
    14 \isadelimtheory
    15 %
    16 \endisadelimtheory
    17 %
    18 \begin{isamarkuptext}%
    19 \noindent
    20 In particular, there are \isa{case}-expressions, for example
    21 \begin{isabelle}%
    22 \ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
    23 \end{isabelle}
    24 primitive recursion, for example%
    25 \end{isamarkuptext}%
    26 \isamarkuptrue%
    27 \isacommand{primrec}\isamarkupfalse%
    28 \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    29 {\isachardoublequoteopen}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
    30 {\isachardoublequoteopen}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequoteclose}%
    31 \begin{isamarkuptext}%
    32 \noindent
    33 and induction, for example%
    34 \end{isamarkuptext}%
    35 \isamarkuptrue%
    36 \isacommand{lemma}\isamarkupfalse%
    37 \ {\isachardoublequoteopen}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
    38 %
    39 \isadelimproof
    40 %
    41 \endisadelimproof
    42 %
    43 \isatagproof
    44 \isacommand{apply}\isamarkupfalse%
    45 {\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
    46 \isacommand{apply}\isamarkupfalse%
    47 {\isacharparenleft}auto{\isacharparenright}\isanewline
    48 \isacommand{done}\isamarkupfalse%
    49 %
    50 \endisatagproof
    51 {\isafoldproof}%
    52 %
    53 \isadelimproof
    54 %
    55 \endisadelimproof
    56 %
    57 \begin{isamarkuptext}%
    58 \newcommand{\mystar}{*%
    59 }
    60 \index{arithmetic operations!for \protect\isa{nat}}%
    61 The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
    62 \isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
    63 \sdx{div}, \sdx{mod}, \cdx{min} and
    64 \cdx{max} are predefined, as are the relations
    65 \isadxboldpos{\isasymle}{$HOL2arithrel} and
    66 \isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
    67 \isa{m\ {\isacharless}\ n}. There is even a least number operation
    68 \sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
    69 \begin{warn}\index{overloading}
    70   The constants \cdx{0} and \cdx{1} and the operations
    71   \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
    72   \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    73   \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
    74   \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
    75   not just for natural numbers but for other types as well.
    76   For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
    77   that you are talking about natural numbers. Hence Isabelle can only infer
    78   that \isa{x} is of some arbitrary type where \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are
    79   declared. As a consequence, you will be unable to prove the
    80   goal. To alert you to such pitfalls, Isabelle flags numerals without a
    81   fixed type in its output: \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x}. (In the absence of a numeral,
    82   it may take you some time to realize what has happened if \pgmenu{Show
    83   Types} is not set).  In this particular example, you need to include
    84   an explicit type constraint, for example \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there
    85   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
    86   overloaded.
    87 
    88   For details on overloading see \S\ref{sec:overloading}.
    89   Table~\ref{tab:overloading} in the appendix shows the most important
    90   overloaded operations.
    91 \end{warn}
    92 \begin{warn}
    93   The symbols \isadxboldpos{>}{$HOL2arithrel} and
    94   \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isachargreater}\ y}
    95   stands for \isa{y\ {\isacharless}\ x} and similary for \isa{{\isasymge}} and
    96   \isa{{\isasymle}}.
    97 \end{warn}
    98 \begin{warn}
    99   Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition
   100   (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
   101   tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
   102   others (especially the single step tactics in Chapter~\ref{chap:rules}).
   103   If you need the full set of numerals, see~\S\ref{sec:numerals}.
   104   \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and \isa{Suc}.}
   105 \end{warn}
   106 
   107 Both \isa{auto} and \isa{simp}
   108 (a method introduced below, \S\ref{sec:Simplification}) prove 
   109 simple arithmetic goals automatically:%
   110 \end{isamarkuptext}%
   111 \isamarkuptrue%
   112 \isacommand{lemma}\isamarkupfalse%
   113 \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequoteclose}%
   114 \isadelimproof
   115 %
   116 \endisadelimproof
   117 %
   118 \isatagproof
   119 %
   120 \endisatagproof
   121 {\isafoldproof}%
   122 %
   123 \isadelimproof
   124 %
   125 \endisadelimproof
   126 %
   127 \begin{isamarkuptext}%
   128 \noindent
   129 For efficiency's sake, this built-in prover ignores quantified formulae,
   130 many logical connectives, and all arithmetic operations apart from addition.
   131 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
   132 \end{isamarkuptext}%
   133 \isamarkuptrue%
   134 \isacommand{lemma}\isamarkupfalse%
   135 \ {\isachardoublequoteopen}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequoteclose}%
   136 \isadelimproof
   137 %
   138 \endisadelimproof
   139 %
   140 \isatagproof
   141 %
   142 \endisatagproof
   143 {\isafoldproof}%
   144 %
   145 \isadelimproof
   146 %
   147 \endisadelimproof
   148 %
   149 \begin{isamarkuptext}%
   150 \noindent The method \methdx{arith} is more general.  It attempts to
   151 prove the first subgoal provided it is a \textbf{linear arithmetic} formula.
   152 Such formulas may involve the usual logical connectives (\isa{{\isasymnot}},
   153 \isa{{\isasymand}}, \isa{{\isasymor}}, \isa{{\isasymlongrightarrow}}, \isa{{\isacharequal}},
   154 \isa{{\isasymforall}}, \isa{{\isasymexists}}), the relations \isa{{\isacharequal}},
   155 \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations \isa{{\isacharplus}}, \isa{{\isacharminus}},
   156 \isa{min} and \isa{max}.  For example,%
   157 \end{isamarkuptext}%
   158 \isamarkuptrue%
   159 \isacommand{lemma}\isamarkupfalse%
   160 \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
   161 %
   162 \isadelimproof
   163 %
   164 \endisadelimproof
   165 %
   166 \isatagproof
   167 \isacommand{apply}\isamarkupfalse%
   168 {\isacharparenleft}arith{\isacharparenright}%
   169 \endisatagproof
   170 {\isafoldproof}%
   171 %
   172 \isadelimproof
   173 %
   174 \endisadelimproof
   175 %
   176 \begin{isamarkuptext}%
   177 \noindent
   178 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
   179 \end{isamarkuptext}%
   180 \isamarkuptrue%
   181 \isacommand{lemma}\isamarkupfalse%
   182 \ {\isachardoublequoteopen}n{\isacharasterisk}n\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}%
   183 \isadelimproof
   184 %
   185 \endisadelimproof
   186 %
   187 \isatagproof
   188 %
   189 \endisatagproof
   190 {\isafoldproof}%
   191 %
   192 \isadelimproof
   193 %
   194 \endisadelimproof
   195 %
   196 \begin{isamarkuptext}%
   197 \noindent
   198 is not proved by \isa{arith} because the proof relies 
   199 on properties of multiplication. Only multiplication by numerals (which is
   200 the same as iterated addition) is taken into account.
   201 
   202 \begin{warn} The running time of \isa{arith} is exponential in the number
   203   of occurrences of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   204   \cdx{max} because they are first eliminated by case distinctions.
   205 
   206 If \isa{k} is a numeral, \sdx{div}~\isa{k}, \sdx{mod}~\isa{k} and
   207 \isa{k}~\sdx{dvd} are also supported, where the former two are eliminated
   208 by case distinctions, again blowing up the running time.
   209 
   210 If the formula involves quantifiers, \isa{arith} may take
   211 super-exponential time and space.
   212 \end{warn}%
   213 \end{isamarkuptext}%
   214 \isamarkuptrue%
   215 %
   216 \isadelimtheory
   217 %
   218 \endisadelimtheory
   219 %
   220 \isatagtheory
   221 %
   222 \endisatagtheory
   223 {\isafoldtheory}%
   224 %
   225 \isadelimtheory
   226 %
   227 \endisadelimtheory
   228 \end{isabellebody}%
   229 %%% Local Variables:
   230 %%% mode: latex
   231 %%% TeX-master: "root"
   232 %%% End: