3 \def\isabellecontext{natsum}%
18 \begin{isamarkuptext}%
20 In particular, there are \isa{case}-expressions, for example
22 \ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
24 primitive recursion, for example%
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}%
33 and induction, for example%
36 \isacommand{lemma}\isamarkupfalse%
37 \ {\isachardoublequoteopen}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
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%
57 \begin{isamarkuptext}%
58 \newcommand{\mystar}{*%
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
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.
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
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}.}
107 Both \isa{auto} and \isa{simp}
108 (a method introduced below, \S\ref{sec:Simplification}) prove
109 simple arithmetic goals automatically:%
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}%
127 \begin{isamarkuptext}%
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:%
134 \isacommand{lemma}\isamarkupfalse%
135 \ {\isachardoublequoteopen}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequoteclose}%
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,%
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
167 \isacommand{apply}\isamarkupfalse%
168 {\isacharparenleft}arith{\isacharparenright}%
176 \begin{isamarkuptext}%
178 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
181 \isacommand{lemma}\isamarkupfalse%
182 \ {\isachardoublequoteopen}n{\isacharasterisk}n\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}%
196 \begin{isamarkuptext}%
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.
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.
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.
210 If the formula involves quantifiers, \isa{arith} may take
211 super-exponential time and space.
231 %%% TeX-master: "root"