1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Even}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isadelimML |
|
19 % |
|
20 \endisadelimML |
|
21 % |
|
22 \isatagML |
|
23 % |
|
24 \endisatagML |
|
25 {\isafoldML}% |
|
26 % |
|
27 \isadelimML |
|
28 % |
|
29 \endisadelimML |
|
30 % |
|
31 \isamarkupsection{The Set of Even Numbers% |
|
32 } |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \begin{isamarkuptext}% |
|
36 \index{even numbers!defining inductively|(}% |
|
37 The set of even numbers can be inductively defined as the least set |
|
38 containing 0 and closed under the operation $+2$. Obviously, |
|
39 \emph{even} can also be expressed using the divides relation (\isa{dvd}). |
|
40 We shall prove below that the two formulations coincide. On the way we |
|
41 shall examine the primary means of reasoning about inductively defined |
|
42 sets: rule induction.% |
|
43 \end{isamarkuptext}% |
|
44 \isamarkuptrue% |
|
45 % |
|
46 \isamarkupsubsection{Making an Inductive Definition% |
|
47 } |
|
48 \isamarkuptrue% |
|
49 % |
|
50 \begin{isamarkuptext}% |
|
51 Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be |
|
52 a set of natural numbers with the desired properties.% |
|
53 \end{isamarkuptext}% |
|
54 \isamarkuptrue% |
|
55 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
|
56 \ even\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
57 zero{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
58 step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}% |
|
59 \begin{isamarkuptext}% |
|
60 An inductive definition consists of introduction rules. The first one |
|
61 above states that 0 is even; the second states that if $n$ is even, then so |
|
62 is~$n+2$. Given this declaration, Isabelle generates a fixed point |
|
63 definition for \isa{even} and proves theorems about it, |
|
64 thus following the definitional approach (see {\S}\ref{sec:definitional}). |
|
65 These theorems |
|
66 include the introduction rules specified in the declaration, an elimination |
|
67 rule for case analysis and an induction rule. We can refer to these |
|
68 theorems by automatically-generated names. Here are two examples: |
|
69 \begin{isabelle}% |
|
70 {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\rulename{even{\isaliteral{2E}{\isachardot}}zero}\par\smallskip% |
|
71 n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\rulename{even{\isaliteral{2E}{\isachardot}}step}% |
|
72 \end{isabelle} |
|
73 |
|
74 The introduction rules can be given attributes. Here |
|
75 both rules are specified as \isa{intro!},% |
|
76 \index{intro"!@\isa {intro"!} (attribute)} |
|
77 directing the classical reasoner to |
|
78 apply them aggressively. Obviously, regarding 0 as even is safe. The |
|
79 \isa{step} rule is also safe because $n+2$ is even if and only if $n$ is |
|
80 even. We prove this equivalence later.% |
|
81 \end{isamarkuptext}% |
|
82 \isamarkuptrue% |
|
83 % |
|
84 \isamarkupsubsection{Using Introduction Rules% |
|
85 } |
|
86 \isamarkuptrue% |
|
87 % |
|
88 \begin{isamarkuptext}% |
|
89 Our first lemma states that numbers of the form $2\times k$ are even. |
|
90 Introduction rules are used to show that specific values belong to the |
|
91 inductive set. Such proofs typically involve |
|
92 induction, perhaps over some other inductive set.% |
|
93 \end{isamarkuptext}% |
|
94 \isamarkuptrue% |
|
95 \isacommand{lemma}\isamarkupfalse% |
|
96 \ two{\isaliteral{5F}{\isacharunderscore}}times{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}k\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
97 % |
|
98 \isadelimproof |
|
99 % |
|
100 \endisadelimproof |
|
101 % |
|
102 \isatagproof |
|
103 \isacommand{apply}\isamarkupfalse% |
|
104 \ {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ k{\isaliteral{29}{\isacharparenright}}\isanewline |
|
105 \ \isacommand{apply}\isamarkupfalse% |
|
106 \ auto\isanewline |
|
107 \isacommand{done}\isamarkupfalse% |
|
108 % |
|
109 \endisatagproof |
|
110 {\isafoldproof}% |
|
111 % |
|
112 \isadelimproof |
|
113 % |
|
114 \endisadelimproof |
|
115 % |
|
116 \isadelimproof |
|
117 % |
|
118 \endisadelimproof |
|
119 % |
|
120 \isatagproof |
|
121 % |
|
122 \begin{isamarkuptxt}% |
|
123 \noindent |
|
124 The first step is induction on the natural number \isa{k}, which leaves |
|
125 two subgoals: |
|
126 \begin{isabelle}% |
|
127 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline |
|
128 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ Suc\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
129 \end{isabelle} |
|
130 Here \isa{auto} simplifies both subgoals so that they match the introduction |
|
131 rules, which are then applied automatically. |
|
132 |
|
133 Our ultimate goal is to prove the equivalence between the traditional |
|
134 definition of \isa{even} (using the divides relation) and our inductive |
|
135 definition. One direction of this equivalence is immediate by the lemma |
|
136 just proved, whose \isa{intro{\isaliteral{21}{\isacharbang}}} attribute ensures it is applied automatically.% |
|
137 \end{isamarkuptxt}% |
|
138 \isamarkuptrue% |
|
139 % |
|
140 \endisatagproof |
|
141 {\isafoldproof}% |
|
142 % |
|
143 \isadelimproof |
|
144 % |
|
145 \endisadelimproof |
|
146 \isacommand{lemma}\isamarkupfalse% |
|
147 \ dvd{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ dvd\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
148 % |
|
149 \isadelimproof |
|
150 % |
|
151 \endisadelimproof |
|
152 % |
|
153 \isatagproof |
|
154 \isacommand{by}\isamarkupfalse% |
|
155 \ {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
|
156 \endisatagproof |
|
157 {\isafoldproof}% |
|
158 % |
|
159 \isadelimproof |
|
160 % |
|
161 \endisadelimproof |
|
162 % |
|
163 \isamarkupsubsection{Rule Induction \label{sec:rule-induction}% |
|
164 } |
|
165 \isamarkuptrue% |
|
166 % |
|
167 \begin{isamarkuptext}% |
|
168 \index{rule induction|(}% |
|
169 From the definition of the set |
|
170 \isa{even}, Isabelle has |
|
171 generated an induction rule: |
|
172 \begin{isabelle}% |
|
173 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
174 \isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ P\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
175 {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\rulename{even{\isaliteral{2E}{\isachardot}}induct}% |
|
176 \end{isabelle} |
|
177 A property \isa{P} holds for every even number provided it |
|
178 holds for~\isa{{\isadigit{0}}} and is closed under the operation |
|
179 \isa{Suc(Suc \(\cdot\))}. Then \isa{P} is closed under the introduction |
|
180 rules for \isa{even}, which is the least set closed under those rules. |
|
181 This type of inductive argument is called \textbf{rule induction}. |
|
182 |
|
183 Apart from the double application of \isa{Suc}, the induction rule above |
|
184 resembles the familiar mathematical induction, which indeed is an instance |
|
185 of rule induction; the natural numbers can be defined inductively to be |
|
186 the least set containing \isa{{\isadigit{0}}} and closed under~\isa{Suc}. |
|
187 |
|
188 Induction is the usual way of proving a property of the elements of an |
|
189 inductively defined set. Let us prove that all members of the set |
|
190 \isa{even} are multiples of two.% |
|
191 \end{isamarkuptext}% |
|
192 \isamarkuptrue% |
|
193 \isacommand{lemma}\isamarkupfalse% |
|
194 \ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ dvd\ n{\isaliteral{22}{\isachardoublequoteclose}}% |
|
195 \isadelimproof |
|
196 % |
|
197 \endisadelimproof |
|
198 % |
|
199 \isatagproof |
|
200 % |
|
201 \begin{isamarkuptxt}% |
|
202 We begin by applying induction. Note that \isa{even{\isaliteral{2E}{\isachardot}}induct} has the form |
|
203 of an elimination rule, so we use the method \isa{erule}. We get two |
|
204 subgoals:% |
|
205 \end{isamarkuptxt}% |
|
206 \isamarkuptrue% |
|
207 \isacommand{apply}\isamarkupfalse% |
|
208 \ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}% |
|
209 \begin{isamarkuptxt}% |
|
210 \begin{isabelle}% |
|
211 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline |
|
212 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ {\isadigit{2}}\ dvd\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ dvd\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}% |
|
213 \end{isabelle} |
|
214 We unfold the definition of \isa{dvd} in both subgoals, proving the first |
|
215 one and simplifying the second:% |
|
216 \end{isamarkuptxt}% |
|
217 \isamarkuptrue% |
|
218 \isacommand{apply}\isamarkupfalse% |
|
219 \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
|
220 \begin{isamarkuptxt}% |
|
221 \begin{isabelle}% |
|
222 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k% |
|
223 \end{isabelle} |
|
224 The next command eliminates the existential quantifier from the assumption |
|
225 and replaces \isa{n} by \isa{{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k}.% |
|
226 \end{isamarkuptxt}% |
|
227 \isamarkuptrue% |
|
228 \isacommand{apply}\isamarkupfalse% |
|
229 \ clarify% |
|
230 \begin{isamarkuptxt}% |
|
231 \begin{isabelle}% |
|
232 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n\ k{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}ka{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ ka% |
|
233 \end{isabelle} |
|
234 To conclude, we tell Isabelle that the desired value is |
|
235 \isa{Suc\ k}. With this hint, the subgoal falls to \isa{simp}.% |
|
236 \end{isamarkuptxt}% |
|
237 \isamarkuptrue% |
|
238 \isacommand{apply}\isamarkupfalse% |
|
239 \ {\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ k{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ exI{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}% |
|
240 \endisatagproof |
|
241 {\isafoldproof}% |
|
242 % |
|
243 \isadelimproof |
|
244 % |
|
245 \endisadelimproof |
|
246 % |
|
247 \begin{isamarkuptext}% |
|
248 Combining the previous two results yields our objective, the |
|
249 equivalence relating \isa{even} and \isa{dvd}. |
|
250 % |
|
251 %we don't want [iff]: discuss?% |
|
252 \end{isamarkuptext}% |
|
253 \isamarkuptrue% |
|
254 \isacommand{theorem}\isamarkupfalse% |
|
255 \ even{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ dvd\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
256 % |
|
257 \isadelimproof |
|
258 % |
|
259 \endisadelimproof |
|
260 % |
|
261 \isatagproof |
|
262 \isacommand{by}\isamarkupfalse% |
|
263 \ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even\ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{29}{\isacharparenright}}% |
|
264 \endisatagproof |
|
265 {\isafoldproof}% |
|
266 % |
|
267 \isadelimproof |
|
268 % |
|
269 \endisadelimproof |
|
270 % |
|
271 \isamarkupsubsection{Generalization and Rule Induction \label{sec:gen-rule-induction}% |
|
272 } |
|
273 \isamarkuptrue% |
|
274 % |
|
275 \begin{isamarkuptext}% |
|
276 \index{generalizing for induction}% |
|
277 Before applying induction, we typically must generalize |
|
278 the induction formula. With rule induction, the required generalization |
|
279 can be hard to find and sometimes requires a complete reformulation of the |
|
280 problem. In this example, our first attempt uses the obvious statement of |
|
281 the result. It fails:% |
|
282 \end{isamarkuptext}% |
|
283 \isamarkuptrue% |
|
284 \isacommand{lemma}\isamarkupfalse% |
|
285 \ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
286 % |
|
287 \isadelimproof |
|
288 % |
|
289 \endisadelimproof |
|
290 % |
|
291 \isatagproof |
|
292 \isacommand{apply}\isamarkupfalse% |
|
293 \ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
|
294 \isacommand{oops}\isamarkupfalse% |
|
295 % |
|
296 \endisatagproof |
|
297 {\isafoldproof}% |
|
298 % |
|
299 \isadelimproof |
|
300 % |
|
301 \endisadelimproof |
|
302 % |
|
303 \isadelimproof |
|
304 % |
|
305 \endisadelimproof |
|
306 % |
|
307 \isatagproof |
|
308 % |
|
309 \begin{isamarkuptxt}% |
|
310 Rule induction finds no occurrences of \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} in the |
|
311 conclusion, which it therefore leaves unchanged. (Look at |
|
312 \isa{even{\isaliteral{2E}{\isachardot}}induct} to see why this happens.) We have these subgoals: |
|
313 \begin{isabelle}% |
|
314 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline |
|
315 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}na{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}na\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
316 \end{isabelle} |
|
317 The first one is hopeless. Rule induction on |
|
318 a non-variable term discards information, and usually fails. |
|
319 How to deal with such situations |
|
320 in general is described in {\S}\ref{sec:ind-var-in-prems} below. |
|
321 In the current case the solution is easy because |
|
322 we have the necessary inverse, subtraction:% |
|
323 \end{isamarkuptxt}% |
|
324 \isamarkuptrue% |
|
325 % |
|
326 \endisatagproof |
|
327 {\isafoldproof}% |
|
328 % |
|
329 \isadelimproof |
|
330 % |
|
331 \endisadelimproof |
|
332 \isacommand{lemma}\isamarkupfalse% |
|
333 \ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
334 % |
|
335 \isadelimproof |
|
336 % |
|
337 \endisadelimproof |
|
338 % |
|
339 \isatagproof |
|
340 \isacommand{apply}\isamarkupfalse% |
|
341 \ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
|
342 \ \isacommand{apply}\isamarkupfalse% |
|
343 \ auto\isanewline |
|
344 \isacommand{done}\isamarkupfalse% |
|
345 % |
|
346 \endisatagproof |
|
347 {\isafoldproof}% |
|
348 % |
|
349 \isadelimproof |
|
350 % |
|
351 \endisadelimproof |
|
352 % |
|
353 \isadelimproof |
|
354 % |
|
355 \endisadelimproof |
|
356 % |
|
357 \isatagproof |
|
358 % |
|
359 \begin{isamarkuptxt}% |
|
360 This lemma is trivially inductive. Here are the subgoals: |
|
361 \begin{isabelle}% |
|
362 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline |
|
363 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
364 \end{isabelle} |
|
365 The first is trivial because \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}} simplifies to \isa{{\isadigit{0}}}, which is |
|
366 even. The second is trivial too: \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}} simplifies to |
|
367 \isa{n}, matching the assumption.% |
|
368 \index{rule induction|)} %the sequel isn't really about induction |
|
369 |
|
370 \medskip |
|
371 Using our lemma, we can easily prove the result we originally wanted:% |
|
372 \end{isamarkuptxt}% |
|
373 \isamarkuptrue% |
|
374 % |
|
375 \endisatagproof |
|
376 {\isafoldproof}% |
|
377 % |
|
378 \isadelimproof |
|
379 % |
|
380 \endisadelimproof |
|
381 \isacommand{lemma}\isamarkupfalse% |
|
382 \ Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
383 % |
|
384 \isadelimproof |
|
385 % |
|
386 \endisadelimproof |
|
387 % |
|
388 \isatagproof |
|
389 \isacommand{by}\isamarkupfalse% |
|
390 \ {\isaliteral{28}{\isacharparenleft}}drule\ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}% |
|
391 \endisatagproof |
|
392 {\isafoldproof}% |
|
393 % |
|
394 \isadelimproof |
|
395 % |
|
396 \endisadelimproof |
|
397 % |
|
398 \begin{isamarkuptext}% |
|
399 We have just proved the converse of the introduction rule \isa{even{\isaliteral{2E}{\isachardot}}step}. |
|
400 This suggests proving the following equivalence. We give it the |
|
401 \attrdx{iff} attribute because of its obvious value for simplification.% |
|
402 \end{isamarkuptext}% |
|
403 \isamarkuptrue% |
|
404 \isacommand{lemma}\isamarkupfalse% |
|
405 \ {\isaliteral{5B}{\isacharbrackleft}}iff{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
406 % |
|
407 \isadelimproof |
|
408 % |
|
409 \endisadelimproof |
|
410 % |
|
411 \isatagproof |
|
412 \isacommand{by}\isamarkupfalse% |
|
413 \ {\isaliteral{28}{\isacharparenleft}}blast\ dest{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{29}{\isacharparenright}}% |
|
414 \endisatagproof |
|
415 {\isafoldproof}% |
|
416 % |
|
417 \isadelimproof |
|
418 % |
|
419 \endisadelimproof |
|
420 % |
|
421 \isamarkupsubsection{Rule Inversion \label{sec:rule-inversion}% |
|
422 } |
|
423 \isamarkuptrue% |
|
424 % |
|
425 \begin{isamarkuptext}% |
|
426 \index{rule inversion|(}% |
|
427 Case analysis on an inductive definition is called \textbf{rule |
|
428 inversion}. It is frequently used in proofs about operational |
|
429 semantics. It can be highly effective when it is applied |
|
430 automatically. Let us look at how rule inversion is done in |
|
431 Isabelle/HOL\@. |
|
432 |
|
433 Recall that \isa{even} is the minimal set closed under these two rules: |
|
434 \begin{isabelle}% |
|
435 {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isasep\isanewline% |
|
436 n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
437 \end{isabelle} |
|
438 Minimality means that \isa{even} contains only the elements that these |
|
439 rules force it to contain. If we are told that \isa{a} |
|
440 belongs to |
|
441 \isa{even} then there are only two possibilities. Either \isa{a} is \isa{{\isadigit{0}}} |
|
442 or else \isa{a} has the form \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}, for some suitable \isa{n} |
|
443 that belongs to |
|
444 \isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves |
|
445 for us when it accepts an inductive definition: |
|
446 \begin{isabelle}% |
|
447 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ a\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
448 \isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
449 {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{even{\isaliteral{2E}{\isachardot}}cases}% |
|
450 \end{isabelle} |
|
451 This general rule is less useful than instances of it for |
|
452 specific patterns. For example, if \isa{a} has the form |
|
453 \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} then the first case becomes irrelevant, while the second |
|
454 case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate |
|
455 this instance for us:% |
|
456 \end{isamarkuptext}% |
|
457 \isamarkuptrue% |
|
458 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse% |
|
459 \ Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}% |
|
460 \begin{isamarkuptext}% |
|
461 The \commdx{inductive\protect\_cases} command generates an instance of |
|
462 the \isa{cases} rule for the supplied pattern and gives it the supplied name: |
|
463 \begin{isabelle}% |
|
464 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases}% |
|
465 \end{isabelle} |
|
466 Applying this as an elimination rule yields one case where \isa{even{\isaliteral{2E}{\isachardot}}cases} |
|
467 would yield two. Rule inversion works well when the conclusions of the |
|
468 introduction rules involve datatype constructors like \isa{Suc} and \isa{{\isaliteral{23}{\isacharhash}}} |
|
469 (list ``cons''); freeness reasoning discards all but one or two cases. |
|
470 |
|
471 In the \isacommand{inductive\_cases} command we supplied an |
|
472 attribute, \isa{elim{\isaliteral{21}{\isacharbang}}}, |
|
473 \index{elim"!@\isa {elim"!} (attribute)}% |
|
474 indicating that this elimination rule can be |
|
475 applied aggressively. The original |
|
476 \isa{cases} rule would loop if used in that manner because the |
|
477 pattern~\isa{a} matches everything. |
|
478 |
|
479 The rule \isa{Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases} is equivalent to the following implication: |
|
480 \begin{isabelle}% |
|
481 Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
482 \end{isabelle} |
|
483 Just above we devoted some effort to reaching precisely |
|
484 this result. Yet we could have obtained it by a one-line declaration, |
|
485 dispensing with the lemma \isa{even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}}. |
|
486 This example also justifies the terminology |
|
487 \textbf{rule inversion}: the new rule inverts the introduction rule |
|
488 \isa{even{\isaliteral{2E}{\isachardot}}step}. In general, a rule can be inverted when the set of elements |
|
489 it introduces is disjoint from those of the other introduction rules. |
|
490 |
|
491 For one-off applications of rule inversion, use the \methdx{ind_cases} method. |
|
492 Here is an example:% |
|
493 \end{isamarkuptext}% |
|
494 \isamarkuptrue% |
|
495 % |
|
496 \isadelimproof |
|
497 % |
|
498 \endisadelimproof |
|
499 % |
|
500 \isatagproof |
|
501 \isacommand{apply}\isamarkupfalse% |
|
502 \ {\isaliteral{28}{\isacharparenleft}}ind{\isaliteral{5F}{\isacharunderscore}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}% |
|
503 \endisatagproof |
|
504 {\isafoldproof}% |
|
505 % |
|
506 \isadelimproof |
|
507 % |
|
508 \endisadelimproof |
|
509 % |
|
510 \begin{isamarkuptext}% |
|
511 The specified instance of the \isa{cases} rule is generated, then applied |
|
512 as an elimination rule. |
|
513 |
|
514 To summarize, every inductive definition produces a \isa{cases} rule. The |
|
515 \commdx{inductive\protect\_cases} command stores an instance of the |
|
516 \isa{cases} rule for a given pattern. Within a proof, the |
|
517 \isa{ind{\isaliteral{5F}{\isacharunderscore}}cases} method applies an instance of the \isa{cases} |
|
518 rule. |
|
519 |
|
520 The even numbers example has shown how inductive definitions can be |
|
521 used. Later examples will show that they are actually worth using.% |
|
522 \index{rule inversion|)}% |
|
523 \index{even numbers!defining inductively|)}% |
|
524 \end{isamarkuptext}% |
|
525 \isamarkuptrue% |
|
526 % |
|
527 \isadelimtheory |
|
528 % |
|
529 \endisadelimtheory |
|
530 % |
|
531 \isatagtheory |
|
532 % |
|
533 \endisatagtheory |
|
534 {\isafoldtheory}% |
|
535 % |
|
536 \isadelimtheory |
|
537 % |
|
538 \endisadelimtheory |
|
539 \end{isabellebody}% |
|
540 %%% Local Variables: |
|
541 %%% mode: latex |
|
542 %%% TeX-master: "root" |
|
543 %%% End: |
|