1 (* Title: HOL/Induct/Common_Patterns.thy |
1 (* Title: HOL/Induct/Common_Patterns.thy |
2 Author: Makarius |
2 Author: Makarius |
3 *) |
3 *) |
4 |
4 |
5 section {* Common patterns of induction *} |
5 section \<open>Common patterns of induction\<close> |
6 |
6 |
7 theory Common_Patterns |
7 theory Common_Patterns |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text \<open> |
12 The subsequent Isar proof schemes illustrate common proof patterns |
12 The subsequent Isar proof schemes illustrate common proof patterns |
13 supported by the generic @{text "induct"} method. |
13 supported by the generic @{text "induct"} method. |
14 |
14 |
15 To demonstrate variations on statement (goal) structure we refer to |
15 To demonstrate variations on statement (goal) structure we refer to |
16 the induction rule of Peano natural numbers: @{thm nat.induct |
16 the induction rule of Peano natural numbers: @{thm nat.induct |
17 [no_vars]}, which is the simplest case of datatype induction. We |
17 [no_vars]}, which is the simplest case of datatype induction. We |
18 shall also see more complex (mutual) datatype inductions involving |
18 shall also see more complex (mutual) datatype inductions involving |
19 several rules. Working with inductive predicates is similar, but |
19 several rules. Working with inductive predicates is similar, but |
20 involves explicit facts about membership, instead of implicit |
20 involves explicit facts about membership, instead of implicit |
21 syntactic typing. |
21 syntactic typing. |
22 *} |
22 \<close> |
23 |
23 |
24 |
24 |
25 subsection {* Variations on statement structure *} |
25 subsection \<open>Variations on statement structure\<close> |
26 |
26 |
27 subsubsection {* Local facts and parameters *} |
27 subsubsection \<open>Local facts and parameters\<close> |
28 |
28 |
29 text {* |
29 text \<open> |
30 Augmenting a problem by additional facts and locally fixed variables |
30 Augmenting a problem by additional facts and locally fixed variables |
31 is a bread-and-butter method in many applications. This is where |
31 is a bread-and-butter method in many applications. This is where |
32 unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in |
32 unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in |
33 the past. The @{text "induct"} method works with primary means of |
33 the past. The @{text "induct"} method works with primary means of |
34 the proof language instead. |
34 the proof language instead. |
35 *} |
35 \<close> |
36 |
36 |
37 lemma |
37 lemma |
38 fixes n :: nat |
38 fixes n :: nat |
39 and x :: 'a |
39 and x :: 'a |
40 assumes "A n x" |
40 assumes "A n x" |
41 shows "P n x" using `A n x` |
41 shows "P n x" using \<open>A n x\<close> |
42 proof (induct n arbitrary: x) |
42 proof (induct n arbitrary: x) |
43 case 0 |
43 case 0 |
44 note prem = `A 0 x` |
44 note prem = \<open>A 0 x\<close> |
45 show "P 0 x" sorry |
45 show "P 0 x" sorry |
46 next |
46 next |
47 case (Suc n) |
47 case (Suc n) |
48 note hyp = `\<And>x. A n x \<Longrightarrow> P n x` |
48 note hyp = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close> |
49 and prem = `A (Suc n) x` |
49 and prem = \<open>A (Suc n) x\<close> |
50 show "P (Suc n) x" sorry |
50 show "P (Suc n) x" sorry |
51 qed |
51 qed |
52 |
52 |
53 |
53 |
54 subsubsection {* Local definitions *} |
54 subsubsection \<open>Local definitions\<close> |
55 |
55 |
56 text {* |
56 text \<open> |
57 Here the idea is to turn sub-expressions of the problem into a |
57 Here the idea is to turn sub-expressions of the problem into a |
58 defined induction variable. This is often accompanied with fixing |
58 defined induction variable. This is often accompanied with fixing |
59 of auxiliary parameters in the original expression, otherwise the |
59 of auxiliary parameters in the original expression, otherwise the |
60 induction step would refer invariably to particular entities. This |
60 induction step would refer invariably to particular entities. This |
61 combination essentially expresses a partially abstracted |
61 combination essentially expresses a partially abstracted |
62 representation of inductive expressions. |
62 representation of inductive expressions. |
63 *} |
63 \<close> |
64 |
64 |
65 lemma |
65 lemma |
66 fixes a :: "'a \<Rightarrow> nat" |
66 fixes a :: "'a \<Rightarrow> nat" |
67 assumes "A (a x)" |
67 assumes "A (a x)" |
68 shows "P (a x)" using `A (a x)` |
68 shows "P (a x)" using \<open>A (a x)\<close> |
69 proof (induct n \<equiv> "a x" arbitrary: x) |
69 proof (induct n \<equiv> "a x" arbitrary: x) |
70 case 0 |
70 case 0 |
71 note prem = `A (a x)` |
71 note prem = \<open>A (a x)\<close> |
72 and defn = `0 = a x` |
72 and defn = \<open>0 = a x\<close> |
73 show "P (a x)" sorry |
73 show "P (a x)" sorry |
74 next |
74 next |
75 case (Suc n) |
75 case (Suc n) |
76 note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)` |
76 note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close> |
77 and prem = `A (a x)` |
77 and prem = \<open>A (a x)\<close> |
78 and defn = `Suc n = a x` |
78 and defn = \<open>Suc n = a x\<close> |
79 show "P (a x)" sorry |
79 show "P (a x)" sorry |
80 qed |
80 qed |
81 |
81 |
82 text {* |
82 text \<open> |
83 Observe how the local definition @{text "n = a x"} recurs in the |
83 Observe how the local definition @{text "n = a x"} recurs in the |
84 inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"}, |
84 inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"}, |
85 according to underlying induction rule. |
85 according to underlying induction rule. |
86 *} |
86 \<close> |
87 |
87 |
88 |
88 |
89 subsubsection {* Simple simultaneous goals *} |
89 subsubsection \<open>Simple simultaneous goals\<close> |
90 |
90 |
91 text {* |
91 text \<open> |
92 The most basic simultaneous induction operates on several goals |
92 The most basic simultaneous induction operates on several goals |
93 one-by-one, where each case refers to induction hypotheses that are |
93 one-by-one, where each case refers to induction hypotheses that are |
94 duplicated according to the number of conclusions. |
94 duplicated according to the number of conclusions. |
95 *} |
95 \<close> |
96 |
96 |
97 lemma |
97 lemma |
98 fixes n :: nat |
98 fixes n :: nat |
99 shows "P n" and "Q n" |
99 shows "P n" and "Q n" |
100 proof (induct n) |
100 proof (induct n) |
103 next |
103 next |
104 case 0 case 2 |
104 case 0 case 2 |
105 show "Q 0" sorry |
105 show "Q 0" sorry |
106 next |
106 next |
107 case (Suc n) case 1 |
107 case (Suc n) case 1 |
108 note hyps = `P n` `Q n` |
108 note hyps = \<open>P n\<close> \<open>Q n\<close> |
109 show "P (Suc n)" sorry |
109 show "P (Suc n)" sorry |
110 next |
110 next |
111 case (Suc n) case 2 |
111 case (Suc n) case 2 |
112 note hyps = `P n` `Q n` |
112 note hyps = \<open>P n\<close> \<open>Q n\<close> |
113 show "Q (Suc n)" sorry |
113 show "Q (Suc n)" sorry |
114 qed |
114 qed |
115 |
115 |
116 text {* |
116 text \<open> |
117 The split into subcases may be deferred as follows -- this is |
117 The split into subcases may be deferred as follows -- this is |
118 particularly relevant for goal statements with local premises. |
118 particularly relevant for goal statements with local premises. |
119 *} |
119 \<close> |
120 |
120 |
121 lemma |
121 lemma |
122 fixes n :: nat |
122 fixes n :: nat |
123 shows "A n \<Longrightarrow> P n" |
123 shows "A n \<Longrightarrow> P n" |
124 and "B n \<Longrightarrow> Q n" |
124 and "B n \<Longrightarrow> Q n" |
125 proof (induct n) |
125 proof (induct n) |
126 case 0 |
126 case 0 |
127 { |
127 { |
128 case 1 |
128 case 1 |
129 note `A 0` |
129 note \<open>A 0\<close> |
130 show "P 0" sorry |
130 show "P 0" sorry |
131 next |
131 next |
132 case 2 |
132 case 2 |
133 note `B 0` |
133 note \<open>B 0\<close> |
134 show "Q 0" sorry |
134 show "Q 0" sorry |
135 } |
135 } |
136 next |
136 next |
137 case (Suc n) |
137 case (Suc n) |
138 note `A n \<Longrightarrow> P n` |
138 note \<open>A n \<Longrightarrow> P n\<close> |
139 and `B n \<Longrightarrow> Q n` |
139 and \<open>B n \<Longrightarrow> Q n\<close> |
140 { |
140 { |
141 case 1 |
141 case 1 |
142 note `A (Suc n)` |
142 note \<open>A (Suc n)\<close> |
143 show "P (Suc n)" sorry |
143 show "P (Suc n)" sorry |
144 next |
144 next |
145 case 2 |
145 case 2 |
146 note `B (Suc n)` |
146 note \<open>B (Suc n)\<close> |
147 show "Q (Suc n)" sorry |
147 show "Q (Suc n)" sorry |
148 } |
148 } |
149 qed |
149 qed |
150 |
150 |
151 |
151 |
152 subsubsection {* Compound simultaneous goals *} |
152 subsubsection \<open>Compound simultaneous goals\<close> |
153 |
153 |
154 text {* |
154 text \<open> |
155 The following pattern illustrates the slightly more complex |
155 The following pattern illustrates the slightly more complex |
156 situation of simultaneous goals with individual local assumptions. |
156 situation of simultaneous goals with individual local assumptions. |
157 In compound simultaneous statements like this, local assumptions |
157 In compound simultaneous statements like this, local assumptions |
158 need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure |
158 need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure |
159 framework. In contrast, local parameters do not require separate |
159 framework. In contrast, local parameters do not require separate |
160 @{text "\<And>"} prefixes here, but may be moved into the common context |
160 @{text "\<And>"} prefixes here, but may be moved into the common context |
161 of the whole statement. |
161 of the whole statement. |
162 *} |
162 \<close> |
163 |
163 |
164 lemma |
164 lemma |
165 fixes n :: nat |
165 fixes n :: nat |
166 and x :: 'a |
166 and x :: 'a |
167 and y :: 'b |
167 and y :: 'b |
169 and "B n y \<Longrightarrow> Q n y" |
169 and "B n y \<Longrightarrow> Q n y" |
170 proof (induct n arbitrary: x y) |
170 proof (induct n arbitrary: x y) |
171 case 0 |
171 case 0 |
172 { |
172 { |
173 case 1 |
173 case 1 |
174 note prem = `A 0 x` |
174 note prem = \<open>A 0 x\<close> |
175 show "P 0 x" sorry |
175 show "P 0 x" sorry |
176 } |
176 } |
177 { |
177 { |
178 case 2 |
178 case 2 |
179 note prem = `B 0 y` |
179 note prem = \<open>B 0 y\<close> |
180 show "Q 0 y" sorry |
180 show "Q 0 y" sorry |
181 } |
181 } |
182 next |
182 next |
183 case (Suc n) |
183 case (Suc n) |
184 note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y` |
184 note hyps = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close> \<open>\<And>y. B n y \<Longrightarrow> Q n y\<close> |
185 then have some_intermediate_result sorry |
185 then have some_intermediate_result sorry |
186 { |
186 { |
187 case 1 |
187 case 1 |
188 note prem = `A (Suc n) x` |
188 note prem = \<open>A (Suc n) x\<close> |
189 show "P (Suc n) x" sorry |
189 show "P (Suc n) x" sorry |
190 } |
190 } |
191 { |
191 { |
192 case 2 |
192 case 2 |
193 note prem = `B (Suc n) y` |
193 note prem = \<open>B (Suc n) y\<close> |
194 show "Q (Suc n) y" sorry |
194 show "Q (Suc n) y" sorry |
195 } |
195 } |
196 qed |
196 qed |
197 |
197 |
198 text {* |
198 text \<open> |
199 Here @{text "induct"} provides again nested cases with numbered |
199 Here @{text "induct"} provides again nested cases with numbered |
200 sub-cases, which allows to share common parts of the body context. |
200 sub-cases, which allows to share common parts of the body context. |
201 In typical applications, there could be a long intermediate proof of |
201 In typical applications, there could be a long intermediate proof of |
202 general consequences of the induction hypotheses, before finishing |
202 general consequences of the induction hypotheses, before finishing |
203 each conclusion separately. |
203 each conclusion separately. |
204 *} |
204 \<close> |
205 |
205 |
206 |
206 |
207 subsection {* Multiple rules *} |
207 subsection \<open>Multiple rules\<close> |
208 |
208 |
209 text {* |
209 text \<open> |
210 Multiple induction rules emerge from mutual definitions of |
210 Multiple induction rules emerge from mutual definitions of |
211 datatypes, inductive predicates, functions etc. The @{text |
211 datatypes, inductive predicates, functions etc. The @{text |
212 "induct"} method accepts replicated arguments (with @{text "and"} |
212 "induct"} method accepts replicated arguments (with @{text "and"} |
213 separator), corresponding to each projection of the induction |
213 separator), corresponding to each projection of the induction |
214 principle. |
214 principle. |
215 |
215 |
216 The goal statement essentially follows the same arrangement, |
216 The goal statement essentially follows the same arrangement, |
217 although it might be subdivided into simultaneous sub-problems as |
217 although it might be subdivided into simultaneous sub-problems as |
218 before! |
218 before! |
219 *} |
219 \<close> |
220 |
220 |
221 datatype foo = Foo1 nat | Foo2 bar |
221 datatype foo = Foo1 nat | Foo2 bar |
222 and bar = Bar1 bool | Bar2 bazar |
222 and bar = Bar1 bool | Bar2 bazar |
223 and bazar = Bazar foo |
223 and bazar = Bazar foo |
224 |
224 |
225 text {* |
225 text \<open> |
226 The pack of induction rules for this datatype is: @{thm [display] |
226 The pack of induction rules for this datatype is: @{thm [display] |
227 foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]} |
227 foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]} |
228 |
228 |
229 This corresponds to the following basic proof pattern: |
229 This corresponds to the following basic proof pattern: |
230 *} |
230 \<close> |
231 |
231 |
232 lemma |
232 lemma |
233 fixes foo :: foo |
233 fixes foo :: foo |
234 and bar :: bar |
234 and bar :: bar |
235 and bazar :: bazar |
235 and bazar :: bazar |
239 proof (induct foo and bar and bazar) |
239 proof (induct foo and bar and bazar) |
240 case (Foo1 n) |
240 case (Foo1 n) |
241 show "P (Foo1 n)" sorry |
241 show "P (Foo1 n)" sorry |
242 next |
242 next |
243 case (Foo2 bar) |
243 case (Foo2 bar) |
244 note `Q bar` |
244 note \<open>Q bar\<close> |
245 show "P (Foo2 bar)" sorry |
245 show "P (Foo2 bar)" sorry |
246 next |
246 next |
247 case (Bar1 b) |
247 case (Bar1 b) |
248 show "Q (Bar1 b)" sorry |
248 show "Q (Bar1 b)" sorry |
249 next |
249 next |
250 case (Bar2 bazar) |
250 case (Bar2 bazar) |
251 note `R bazar` |
251 note \<open>R bazar\<close> |
252 show "Q (Bar2 bazar)" sorry |
252 show "Q (Bar2 bazar)" sorry |
253 next |
253 next |
254 case (Bazar foo) |
254 case (Bazar foo) |
255 note `P foo` |
255 note \<open>P foo\<close> |
256 show "R (Bazar foo)" sorry |
256 show "R (Bazar foo)" sorry |
257 qed |
257 qed |
258 |
258 |
259 text {* |
259 text \<open> |
260 This can be combined with the previous techniques for compound |
260 This can be combined with the previous techniques for compound |
261 statements, e.g.\ like this. |
261 statements, e.g.\ like this. |
262 *} |
262 \<close> |
263 |
263 |
264 lemma |
264 lemma |
265 fixes x :: 'a and y :: 'b and z :: 'c |
265 fixes x :: 'a and y :: 'b and z :: 'c |
266 and foo :: foo |
266 and foo :: foo |
267 and bar :: bar |
267 and bar :: bar |
365 { case 1 show "P1 0" sorry } |
365 { case 1 show "P1 0" sorry } |
366 { case 2 show "P2 0" sorry } |
366 { case 2 show "P2 0" sorry } |
367 { case 3 show "P3 0" sorry } |
367 { case 3 show "P3 0" sorry } |
368 next |
368 next |
369 case (succ_Evn n) |
369 case (succ_Evn n) |
370 note `Evn n` and `P1 n` `P2 n` `P3 n` |
370 note \<open>Evn n\<close> and \<open>P1 n\<close> \<open>P2 n\<close> \<open>P3 n\<close> |
371 { case 1 show "Q1 (Suc n)" sorry } |
371 { case 1 show "Q1 (Suc n)" sorry } |
372 { case 2 show "Q2 (Suc n)" sorry } |
372 { case 2 show "Q2 (Suc n)" sorry } |
373 next |
373 next |
374 case (succ_Odd n) |
374 case (succ_Odd n) |
375 note `Odd n` and `Q1 n` `Q2 n` |
375 note \<open>Odd n\<close> and \<open>Q1 n\<close> \<open>Q2 n\<close> |
376 { case 1 show "P1 (Suc n)" sorry } |
376 { case 1 show "P1 (Suc n)" sorry } |
377 { case 2 show "P2 (Suc n)" sorry } |
377 { case 2 show "P2 (Suc n)" sorry } |
378 { case 3 show "P3 (Suc n)" sorry } |
378 { case 3 show "P3 (Suc n)" sorry } |
379 qed |
379 qed |
380 |
380 |
381 |
381 |
382 text {* |
382 text \<open> |
383 Cases and hypotheses in each case can be named explicitly. |
383 Cases and hypotheses in each case can be named explicitly. |
384 *} |
384 \<close> |
385 |
385 |
386 inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r |
386 inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r |
387 where |
387 where |
388 refl: "star r x x" |
388 refl: "star r x x" |
389 | step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
389 | step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
390 |
390 |
391 text {* Underscores are replaced by the default name hyps: *} |
391 text \<open>Underscores are replaced by the default name hyps:\<close> |
392 |
392 |
393 lemmas star_induct = star.induct [case_names base step[r _ IH]] |
393 lemmas star_induct = star.induct [case_names base step[r _ IH]] |
394 |
394 |
395 lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
395 lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
396 proof (induct rule: star_induct) print_cases |
396 proof (induct rule: star_induct) print_cases |