author | wenzelm |
Wed, 06 Dec 2006 01:12:43 +0100 | |
changeset 21672 | 29c346b165d4 |
parent 21545 | 54cc492d80a9 |
child 22507 | 3572bc633d9a |
permissions | -rw-r--r-- |
17024 | 1 |
(* Title: HOL/Extraction/Pigeonhole.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* The pigeonhole principle *} |
|
7 |
||
8 |
theory Pigeonhole imports EfficientNat begin |
|
9 |
||
10 |
text {* |
|
11 |
We formalize two proofs of the pigeonhole principle, which lead |
|
12 |
to extracted programs of quite different complexity. The original |
|
13 |
formalization of these proofs in {\sc Nuprl} is due to |
|
14 |
Aleksey Nogin \cite{Nogin-ENTCS-2000}. |
|
15 |
||
16 |
We need decidability of equality on natural numbers: |
|
17 |
*} |
|
18 |
||
21127 | 19 |
lemma nat_eq_dec: "(m\<Colon>nat) = n \<or> m \<noteq> n" |
20 |
apply (induct m arbitrary: n) |
|
17024 | 21 |
apply (case_tac n) |
22 |
apply (case_tac [3] n) |
|
17604 | 23 |
apply (simp only: nat.simps, iprover?)+ |
17024 | 24 |
done |
25 |
||
26 |
text {* |
|
17027 | 27 |
We can decide whether an array @{term "f"} of length @{term "l"} |
17024 | 28 |
contains an element @{term "x"}. |
29 |
*} |
|
30 |
||
31 |
lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)" |
|
32 |
proof (induct l) |
|
33 |
case 0 |
|
34 |
have "\<not> (\<exists>j<0. x = f j)" |
|
35 |
proof |
|
36 |
assume "\<exists>j<0. x = f j" |
|
17604 | 37 |
then obtain j where j: "j < (0::nat)" by iprover |
17024 | 38 |
thus "False" by simp |
39 |
qed |
|
40 |
thus ?case .. |
|
41 |
next |
|
42 |
case (Suc l) |
|
43 |
thus ?case |
|
44 |
proof |
|
45 |
assume "\<exists>j<l. x = f j" |
|
46 |
then obtain j where j: "j < l" |
|
17604 | 47 |
and eq: "x = f j" by iprover |
17024 | 48 |
from j have "j < Suc l" by simp |
17604 | 49 |
with eq show ?case by iprover |
17024 | 50 |
next |
51 |
assume nex: "\<not> (\<exists>j<l. x = f j)" |
|
52 |
from nat_eq_dec show ?case |
|
53 |
proof |
|
54 |
assume eq: "x = f l" |
|
55 |
have "l < Suc l" by simp |
|
17604 | 56 |
with eq show ?case by iprover |
17024 | 57 |
next |
58 |
assume neq: "x \<noteq> f l" |
|
59 |
have "\<not> (\<exists>j<Suc l. x = f j)" |
|
60 |
proof |
|
61 |
assume "\<exists>j<Suc l. x = f j" |
|
62 |
then obtain j where j: "j < Suc l" |
|
17604 | 63 |
and eq: "x = f j" by iprover |
17024 | 64 |
show False |
65 |
proof cases |
|
66 |
assume "j = l" |
|
67 |
with eq have "x = f l" by simp |
|
68 |
with neq show False .. |
|
69 |
next |
|
70 |
assume "j \<noteq> l" |
|
71 |
with j have "j < l" by simp |
|
17604 | 72 |
with nex and eq show False by iprover |
17024 | 73 |
qed |
74 |
qed |
|
75 |
thus ?case .. |
|
76 |
qed |
|
77 |
qed |
|
78 |
qed |
|
79 |
||
80 |
text {* |
|
81 |
This proof yields a polynomial program. |
|
82 |
*} |
|
83 |
||
84 |
theorem pigeonhole: |
|
85 |
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j" |
|
86 |
proof (induct n) |
|
87 |
case 0 |
|
88 |
hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp |
|
17604 | 89 |
thus ?case by iprover |
17024 | 90 |
next |
91 |
case (Suc n) |
|
92 |
{ |
|
93 |
fix k |
|
94 |
have |
|
95 |
"k \<le> Suc (Suc n) \<Longrightarrow> |
|
96 |
(\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow> |
|
97 |
(\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" |
|
98 |
proof (induct k) |
|
99 |
case 0 |
|
100 |
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" |
|
101 |
have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)" |
|
102 |
proof |
|
103 |
assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" |
|
104 |
then obtain i j where i: "i \<le> Suc n" and j: "j < i" |
|
17604 | 105 |
and f: "?f i = ?f j" by iprover |
17024 | 106 |
from j have i_nz: "Suc 0 \<le> i" by simp |
107 |
from i have iSSn: "i \<le> Suc (Suc n)" by simp |
|
108 |
have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp |
|
109 |
show False |
|
110 |
proof cases |
|
111 |
assume fi: "f i = Suc n" |
|
112 |
show False |
|
113 |
proof cases |
|
114 |
assume fj: "f j = Suc n" |
|
115 |
from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0) |
|
116 |
moreover from fi have "f i = f j" |
|
117 |
by (simp add: fj [symmetric]) |
|
118 |
ultimately show ?thesis .. |
|
119 |
next |
|
120 |
from i and j have "j < Suc (Suc n)" by simp |
|
121 |
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j" |
|
122 |
by (rule 0) |
|
123 |
moreover assume "f j \<noteq> Suc n" |
|
124 |
with fi and f have "f (Suc (Suc n)) = f j" by simp |
|
125 |
ultimately show False .. |
|
126 |
qed |
|
127 |
next |
|
128 |
assume fi: "f i \<noteq> Suc n" |
|
129 |
show False |
|
130 |
proof cases |
|
131 |
from i have "i < Suc (Suc n)" by simp |
|
132 |
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i" |
|
133 |
by (rule 0) |
|
134 |
moreover assume "f j = Suc n" |
|
135 |
with fi and f have "f (Suc (Suc n)) = f i" by simp |
|
136 |
ultimately show False .. |
|
137 |
next |
|
138 |
from i_nz and iSSn and j |
|
139 |
have "f i \<noteq> f j" by (rule 0) |
|
140 |
moreover assume "f j \<noteq> Suc n" |
|
141 |
with fi and f have "f i = f j" by simp |
|
142 |
ultimately show False .. |
|
143 |
qed |
|
144 |
qed |
|
145 |
qed |
|
146 |
moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n" |
|
147 |
proof - |
|
148 |
fix i assume "i \<le> Suc n" |
|
149 |
hence i: "i < Suc (Suc n)" by simp |
|
150 |
have "f (Suc (Suc n)) \<noteq> f i" |
|
151 |
by (rule 0) (simp_all add: i) |
|
152 |
moreover have "f (Suc (Suc n)) \<le> Suc n" |
|
153 |
by (rule Suc) simp |
|
154 |
moreover from i have "i \<le> Suc (Suc n)" by simp |
|
155 |
hence "f i \<le> Suc n" by (rule Suc) |
|
156 |
ultimately show "?thesis i" |
|
157 |
by simp |
|
158 |
qed |
|
159 |
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" |
|
160 |
by (rule Suc) |
|
161 |
ultimately show ?case .. |
|
162 |
next |
|
163 |
case (Suc k) |
|
164 |
from search show ?case |
|
165 |
proof |
|
166 |
assume "\<exists>j<Suc k. f (Suc k) = f j" |
|
17604 | 167 |
thus ?case by (iprover intro: le_refl) |
17024 | 168 |
next |
169 |
assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)" |
|
170 |
have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j" |
|
171 |
proof (rule Suc) |
|
172 |
from Suc show "k \<le> Suc (Suc n)" by simp |
|
173 |
fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)" |
|
174 |
and j: "j < i" |
|
175 |
show "f i \<noteq> f j" |
|
176 |
proof cases |
|
177 |
assume eq: "i = Suc k" |
|
178 |
show ?thesis |
|
179 |
proof |
|
180 |
assume "f i = f j" |
|
181 |
hence "f (Suc k) = f j" by (simp add: eq) |
|
17604 | 182 |
with nex and j and eq show False by iprover |
17024 | 183 |
qed |
184 |
next |
|
185 |
assume "i \<noteq> Suc k" |
|
186 |
with k have "Suc (Suc k) \<le> i" by simp |
|
187 |
thus ?thesis using i and j by (rule Suc) |
|
188 |
qed |
|
189 |
qed |
|
17604 | 190 |
thus ?thesis by (iprover intro: le_SucI) |
17024 | 191 |
qed |
192 |
qed |
|
193 |
} |
|
194 |
note r = this |
|
195 |
show ?case by (rule r) simp_all |
|
196 |
qed |
|
197 |
||
198 |
text {* |
|
199 |
The following proof, although quite elegant from a mathematical point of view, |
|
200 |
leads to an exponential program: |
|
201 |
*} |
|
202 |
||
203 |
theorem pigeonhole_slow: |
|
204 |
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j" |
|
205 |
proof (induct n) |
|
206 |
case 0 |
|
207 |
have "Suc 0 \<le> Suc 0" .. |
|
208 |
moreover have "0 < Suc 0" .. |
|
209 |
moreover from 0 have "f (Suc 0) = f 0" by simp |
|
17604 | 210 |
ultimately show ?case by iprover |
17024 | 211 |
next |
212 |
case (Suc n) |
|
213 |
from search show ?case |
|
214 |
proof |
|
215 |
assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j" |
|
17604 | 216 |
thus ?case by (iprover intro: le_refl) |
17024 | 217 |
next |
218 |
assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)" |
|
17604 | 219 |
hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover |
17024 | 220 |
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" |
221 |
have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n" |
|
222 |
proof - |
|
223 |
fix i assume i: "i \<le> Suc n" |
|
224 |
show "?thesis i" |
|
225 |
proof (cases "f i = Suc n") |
|
226 |
case True |
|
227 |
from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp |
|
228 |
with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp |
|
229 |
moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp |
|
230 |
ultimately have "f (Suc (Suc n)) \<le> n" by simp |
|
231 |
with True show ?thesis by simp |
|
232 |
next |
|
233 |
case False |
|
234 |
from Suc and i have "f i \<le> Suc n" by simp |
|
235 |
with False show ?thesis by simp |
|
236 |
qed |
|
237 |
qed |
|
238 |
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc) |
|
239 |
then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j" |
|
17604 | 240 |
by iprover |
17024 | 241 |
have "f i = f j" |
242 |
proof (cases "f i = Suc n") |
|
243 |
case True |
|
244 |
show ?thesis |
|
245 |
proof (cases "f j = Suc n") |
|
246 |
assume "f j = Suc n" |
|
247 |
with True show ?thesis by simp |
|
248 |
next |
|
249 |
assume "f j \<noteq> Suc n" |
|
250 |
moreover from i ji nex have "f (Suc (Suc n)) \<noteq> f j" by simp |
|
251 |
ultimately show ?thesis using True f by simp |
|
252 |
qed |
|
253 |
next |
|
254 |
case False |
|
255 |
show ?thesis |
|
256 |
proof (cases "f j = Suc n") |
|
257 |
assume "f j = Suc n" |
|
258 |
moreover from i nex have "f (Suc (Suc n)) \<noteq> f i" by simp |
|
259 |
ultimately show ?thesis using False f by simp |
|
260 |
next |
|
261 |
assume "f j \<noteq> Suc n" |
|
262 |
with False f show ?thesis by simp |
|
263 |
qed |
|
264 |
qed |
|
265 |
moreover from i have "i \<le> Suc (Suc n)" by simp |
|
17604 | 266 |
ultimately show ?thesis using ji by iprover |
17024 | 267 |
qed |
268 |
qed |
|
269 |
||
270 |
extract pigeonhole pigeonhole_slow |
|
271 |
||
272 |
text {* |
|
273 |
The programs extracted from the above proofs look as follows: |
|
274 |
@{thm [display] pigeonhole_def} |
|
275 |
@{thm [display] pigeonhole_slow_def} |
|
276 |
The program for searching for an element in an array is |
|
277 |
@{thm [display,eta_contract=false] search_def} |
|
278 |
The correctness statement for @{term "pigeonhole"} is |
|
279 |
@{thm [display] pigeonhole_correctness [no_vars]} |
|
280 |
||
281 |
In order to analyze the speed of the above programs, |
|
282 |
we generate ML code from them. |
|
283 |
*} |
|
284 |
||
285 |
consts_code |
|
286 |
arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}") |
|
287 |
||
17145 | 288 |
code_module PH |
289 |
contains |
|
17024 | 290 |
test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)" |
291 |
test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)" |
|
292 |
sel = "op !" |
|
293 |
||
17145 | 294 |
ML "timeit (fn () => PH.test 10)" |
295 |
ML "timeit (fn () => PH.test' 10)" |
|
296 |
ML "timeit (fn () => PH.test 20)" |
|
297 |
ML "timeit (fn () => PH.test' 20)" |
|
298 |
ML "timeit (fn () => PH.test 25)" |
|
299 |
ML "timeit (fn () => PH.test' 25)" |
|
300 |
ML "timeit (fn () => PH.test 500)" |
|
17024 | 301 |
|
17145 | 302 |
ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])" |
17024 | 303 |
|
20837 | 304 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21127
diff
changeset
|
305 |
arbitrary_nat :: "nat \<times> nat" where |
21062 | 306 |
[symmetric, code inline]: "arbitrary_nat = arbitrary" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21127
diff
changeset
|
307 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21127
diff
changeset
|
308 |
arbitrary_nat_subst :: "nat \<times> nat" where |
20933 | 309 |
"arbitrary_nat_subst = (0, 0)" |
20837 | 310 |
|
21062 | 311 |
code_axioms |
20933 | 312 |
arbitrary_nat \<equiv> arbitrary_nat_subst |
20837 | 313 |
|
314 |
definition |
|
315 |
"test n = pigeonhole n (\<lambda>m. m - 1)" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21127
diff
changeset
|
316 |
definition |
20837 | 317 |
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)" |
318 |
||
21545 | 319 |
code_gen test test' "op !" (SML #) |
20837 | 320 |
|
321 |
ML "timeit (fn () => ROOT.Pigeonhole.test 10)" |
|
322 |
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)" |
|
323 |
ML "timeit (fn () => ROOT.Pigeonhole.test 20)" |
|
324 |
ML "timeit (fn () => ROOT.Pigeonhole.test' 20)" |
|
325 |
ML "timeit (fn () => ROOT.Pigeonhole.test 25)" |
|
326 |
ML "timeit (fn () => ROOT.Pigeonhole.test' 25)" |
|
327 |
ML "timeit (fn () => ROOT.Pigeonhole.test 500)" |
|
328 |
||
329 |
ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])" |
|
330 |
||
17024 | 331 |
end |