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}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ m\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ m% |
|
23 \end{isabelle} |
|
24 primitive recursion, for example% |
|
25 \end{isamarkuptext}% |
|
26 \isamarkuptrue% |
|
27 \isacommand{primrec}\isamarkupfalse% |
|
28 \ sum\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
29 {\isaliteral{22}{\isachardoublequoteopen}}sum\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
30 {\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}}% |
|
31 \begin{isamarkuptext}% |
|
32 \noindent |
|
33 and induction, for example% |
|
34 \end{isamarkuptext}% |
|
35 \isamarkuptrue% |
|
36 \isacommand{lemma}\isamarkupfalse% |
|
37 \ {\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 |
|
38 % |
|
39 \isadelimproof |
|
40 % |
|
41 \endisadelimproof |
|
42 % |
|
43 \isatagproof |
|
44 \isacommand{apply}\isamarkupfalse% |
|
45 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
46 \isacommand{apply}\isamarkupfalse% |
|
47 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\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\ {\isaliteral{2D}{\isacharminus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} if |
|
67 \isa{m\ {\isaliteral{3C}{\isacharless}}\ n}. There is even a least number operation |
|
68 \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}}}. |
|
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\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{0}}\ {\isaliteral{3D}{\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{{\isaliteral{2B}{\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\ {\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, |
|
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{\isaliteral{2B}{\isacharplus}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}}. If there |
|
85 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 |
|
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\ {\isaliteral{3E}{\isachargreater}}\ y} |
|
95 stands for \isa{y\ {\isaliteral{3C}{\isacharless}}\ x} and similary for \isa{{\isaliteral{5C3C67653E}{\isasymge}}} and |
|
96 \isa{{\isaliteral{5C3C6C653E}{\isasymle}}}. |
|
97 \end{warn} |
|
98 \begin{warn} |
|
99 Constant \isa{{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\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 \ {\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}}% |
|
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 \ {\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}}% |
|
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{{\isaliteral{5C3C6E6F743E}{\isasymnot}}}, |
|
153 \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}, \isa{{\isaliteral{5C3C6F723E}{\isasymor}}}, \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}, \isa{{\isaliteral{3D}{\isacharequal}}}, |
|
154 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}}), the relations \isa{{\isaliteral{3D}{\isacharequal}}}, |
|
155 \isa{{\isaliteral{5C3C6C653E}{\isasymle}}} and \isa{{\isaliteral{3C}{\isacharless}}}, and the operations \isa{{\isaliteral{2B}{\isacharplus}}}, \isa{{\isaliteral{2D}{\isacharminus}}}, |
|
156 \isa{min} and \isa{max}. For example,% |
|
157 \end{isamarkuptext}% |
|
158 \isamarkuptrue% |
|
159 \isacommand{lemma}\isamarkupfalse% |
|
160 \ {\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 |
|
161 % |
|
162 \isadelimproof |
|
163 % |
|
164 \endisadelimproof |
|
165 % |
|
166 \isatagproof |
|
167 \isacommand{apply}\isamarkupfalse% |
|
168 {\isaliteral{28}{\isacharparenleft}}arith{\isaliteral{29}{\isacharparenright}}% |
|
169 \endisatagproof |
|
170 {\isafoldproof}% |
|
171 % |
|
172 \isadelimproof |
|
173 % |
|
174 \endisadelimproof |
|
175 % |
|
176 \begin{isamarkuptext}% |
|
177 \noindent |
|
178 succeeds because \isa{k\ {\isaliteral{2A}{\isacharasterisk}}\ k} can be treated as atomic. In contrast,% |
|
179 \end{isamarkuptext}% |
|
180 \isamarkuptrue% |
|
181 \isacommand{lemma}\isamarkupfalse% |
|
182 \ {\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}}% |
|
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: |
|