doc-src/TutorialI/Misc/document/natsum.tex
changeset 10654 458068404143
parent 10608 620647438780
child 10788 ea48dd8b0232
     1.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -29,7 +29,8 @@
     1.4  \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
     1.5  \isaindexbold{max} are predefined, as are the relations
     1.6  \indexboldpos{\isasymle}{$HOL2arithrel} and
     1.7 -\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
     1.8 +\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
     1.9 +\isa{m\ {\isacharless}\ n}. There is even a least number operation
    1.10  \isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
    1.11  Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
    1.12  and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
    1.13 @@ -69,7 +70,9 @@
    1.14  (which attacks the first subgoal). It proves arithmetic goals involving the
    1.15  usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
    1.16  \isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
    1.17 -\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. For example,%
    1.18 +\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
    1.19 +known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
    1.20 +For example,%
    1.21  \end{isamarkuptext}%
    1.22  \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
    1.23  \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}%
    1.24 @@ -88,8 +91,8 @@
    1.25    of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
    1.26    \isaindexbold{max} because they are first eliminated by case distinctions.
    1.27  
    1.28 -  \isa{arith} is incomplete even for the restricted class of formulae
    1.29 -  described above (known as ``linear arithmetic''). If divisibility plays a
    1.30 +  \isa{arith} is incomplete even for the restricted class of
    1.31 +  linear arithmetic formulae. If divisibility plays a
    1.32    role, it may fail to prove a valid formula, for example
    1.33    \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
    1.34  \end{warn}%