|
1 (* Title: HOL/Proofs/Extraction/Higman.thy |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 Author: Monika Seisenberger, LMU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Higman's lemma *} |
|
7 |
|
8 theory Higman2 |
|
9 imports Closures |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Formalization by Stefan Berghofer and Monika Seisenberger, |
|
14 based on Coquand and Fridlender \cite{Coquand93}. |
|
15 *} |
|
16 |
|
17 datatype letter = A | B |
|
18 |
|
19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
|
20 where |
|
21 emb0 [Pure.intro]: "emb [] bs" |
|
22 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |
|
23 | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)" |
|
24 |
|
25 inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
26 for v :: "letter list" |
|
27 where |
|
28 L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)" |
|
29 | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)" |
|
30 |
|
31 inductive good :: "letter list list \<Rightarrow> bool" |
|
32 where |
|
33 good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)" |
|
34 | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)" |
|
35 |
|
36 inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
37 for a :: letter |
|
38 where |
|
39 R0 [Pure.intro]: "R a [] []" |
|
40 | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)" |
|
41 |
|
42 inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
43 for a :: letter |
|
44 where |
|
45 T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)" |
|
46 | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)" |
|
47 | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)" |
|
48 |
|
49 inductive bar :: "letter list list \<Rightarrow> bool" |
|
50 where |
|
51 bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws" |
|
52 | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws" |
|
53 |
|
54 theorem prop1: "bar ([] # ws)" by iprover |
|
55 |
|
56 theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws" |
|
57 by (erule L.induct, iprover+) |
|
58 |
|
59 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" |
|
60 apply (induct set: R) |
|
61 apply (erule L.cases) |
|
62 apply simp+ |
|
63 apply (erule L.cases) |
|
64 apply simp_all |
|
65 apply (rule L0) |
|
66 apply (erule emb2) |
|
67 apply (erule L1) |
|
68 done |
|
69 |
|
70 lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws" |
|
71 apply (induct set: R) |
|
72 apply iprover |
|
73 apply (erule good.cases) |
|
74 apply simp_all |
|
75 apply (rule good0) |
|
76 apply (erule lemma2') |
|
77 apply assumption |
|
78 apply (erule good1) |
|
79 done |
|
80 |
|
81 lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" |
|
82 apply (induct set: T) |
|
83 apply (erule L.cases) |
|
84 apply simp_all |
|
85 apply (rule L0) |
|
86 apply (erule emb2) |
|
87 apply (rule L1) |
|
88 apply (erule lemma1) |
|
89 apply (erule L.cases) |
|
90 apply simp_all |
|
91 apply iprover+ |
|
92 done |
|
93 |
|
94 lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs" |
|
95 apply (induct set: T) |
|
96 apply (erule good.cases) |
|
97 apply simp_all |
|
98 apply (rule good0) |
|
99 apply (erule lemma1) |
|
100 apply (erule good1) |
|
101 apply (erule good.cases) |
|
102 apply simp_all |
|
103 apply (rule good0) |
|
104 apply (erule lemma3') |
|
105 apply iprover+ |
|
106 done |
|
107 |
|
108 lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs" |
|
109 apply (induct set: R) |
|
110 apply iprover |
|
111 apply (case_tac vs) |
|
112 apply (erule R.cases) |
|
113 apply simp |
|
114 apply (case_tac a) |
|
115 apply (rule_tac b=B in T0) |
|
116 apply simp |
|
117 apply (rule R0) |
|
118 apply (rule_tac b=A in T0) |
|
119 apply simp |
|
120 apply (rule R0) |
|
121 apply simp |
|
122 apply (rule T1) |
|
123 apply simp |
|
124 done |
|
125 |
|
126 lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b" |
|
127 apply (case_tac a) |
|
128 apply (case_tac b) |
|
129 apply (case_tac c, simp, simp) |
|
130 apply (case_tac c, simp, simp) |
|
131 apply (case_tac b) |
|
132 apply (case_tac c, simp, simp) |
|
133 apply (case_tac c, simp, simp) |
|
134 done |
|
135 |
|
136 lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b" |
|
137 apply (case_tac a) |
|
138 apply (case_tac b) |
|
139 apply simp |
|
140 apply simp |
|
141 apply (case_tac b) |
|
142 apply simp |
|
143 apply simp |
|
144 done |
|
145 |
|
146 theorem prop2: |
|
147 assumes ab: "a \<noteq> b" and bar: "bar xs" |
|
148 shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar |
|
149 proof induct |
|
150 fix xs zs assume "T a xs zs" and "good xs" |
|
151 hence "good zs" by (rule lemma3) |
|
152 then show "bar zs" by (rule bar1) |
|
153 next |
|
154 fix xs ys |
|
155 assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
|
156 assume "bar ys" |
|
157 thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
|
158 proof induct |
|
159 fix ys zs assume "T b ys zs" and "good ys" |
|
160 then have "good zs" by (rule lemma3) |
|
161 then show "bar zs" by (rule bar1) |
|
162 next |
|
163 fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs" |
|
164 and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs" |
|
165 show "bar zs" |
|
166 proof (rule bar2) |
|
167 fix w |
|
168 show "bar (w # zs)" |
|
169 proof (cases w) |
|
170 case Nil |
|
171 thus ?thesis by simp (rule prop1) |
|
172 next |
|
173 case (Cons c cs) |
|
174 from letter_eq_dec show ?thesis |
|
175 proof |
|
176 assume ca: "c = a" |
|
177 from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb) |
|
178 thus ?thesis by (simp add: Cons ca) |
|
179 next |
|
180 assume "c \<noteq> a" |
|
181 with ab have cb: "c = b" by (rule letter_neq) |
|
182 from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb) |
|
183 thus ?thesis by (simp add: Cons cb) |
|
184 qed |
|
185 qed |
|
186 qed |
|
187 qed |
|
188 qed |
|
189 |
|
190 theorem prop3: |
|
191 assumes bar: "bar xs" |
|
192 shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar |
|
193 proof induct |
|
194 fix xs zs |
|
195 assume "R a xs zs" and "good xs" |
|
196 then have "good zs" by (rule lemma2) |
|
197 then show "bar zs" by (rule bar1) |
|
198 next |
|
199 fix xs zs |
|
200 assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs" |
|
201 and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs" |
|
202 show "bar zs" |
|
203 proof (rule bar2) |
|
204 fix w |
|
205 show "bar (w # zs)" |
|
206 proof (induct w) |
|
207 case Nil |
|
208 show ?case by (rule prop1) |
|
209 next |
|
210 case (Cons c cs) |
|
211 from letter_eq_dec show ?case |
|
212 proof |
|
213 assume "c = a" |
|
214 thus ?thesis by (iprover intro: I [simplified] R) |
|
215 next |
|
216 from R xsn have T: "T a xs zs" by (rule lemma4) |
|
217 assume "c \<noteq> a" |
|
218 thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T) |
|
219 qed |
|
220 qed |
|
221 qed |
|
222 qed |
|
223 |
|
224 theorem higman: "bar []" |
|
225 proof (rule bar2) |
|
226 fix w |
|
227 show "bar [w]" |
|
228 proof (induct w) |
|
229 show "bar [[]]" by (rule prop1) |
|
230 next |
|
231 fix c cs assume "bar [cs]" |
|
232 thus "bar [c # cs]" by (rule prop3) (simp, iprover) |
|
233 qed |
|
234 qed |
|
235 |
|
236 inductive substring ("_ \<preceq> _") |
|
237 where |
|
238 "[] \<preceq> y" |
|
239 | "x \<preceq> y \<Longrightarrow> c # x \<preceq> y" |
|
240 | "x \<preceq> y \<Longrightarrow> c # x \<preceq> c # y" |
|
241 |
|
242 lemma substring_refl: |
|
243 "x \<preceq> x" |
|
244 apply(induct x) |
|
245 apply(auto intro: substring.intros) |
|
246 done |
|
247 |
|
248 definition |
|
249 "SUBSEQ C \<equiv> {x. \<exists>y \<in> C. x \<preceq> y}" |
|
250 |
|
251 lemma |
|
252 "SUBSEQ (SUBSEQ C) = SUBSEQ C" |
|
253 unfolding SUBSEQ_def |
|
254 apply(auto) |
|
255 apply(erule substring.induct) |
|
256 apply(rule_tac x="xb" in bexI) |
|
257 apply(rule substring.intros) |
|
258 apply(simp) |
|
259 apply(erule bexE) |
|
260 apply(rule_tac x="ya" in bexI) |
|
261 apply(rule substring.intros) |
|
262 apply(auto)[2] |
|
263 apply(erule bexE) |
|
264 apply(rule_tac x="ya" in bexI) |
|
265 apply(rule substring.intros) |
|
266 apply(auto)[2] |
|
267 apply(rule_tac x="x" in exI) |
|
268 apply(rule conjI) |
|
269 apply(rule_tac x="y" in bexI) |
|
270 apply(auto)[2] |
|
271 apply(rule substring_refl) |
|
272 done |
|
273 |
|
274 lemma |
|
275 "x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C" |
|
276 unfolding SUBSEQ_def |
|
277 apply(auto) |
|
278 |
|
279 |
|
280 definition |
|
281 "CLOSED C \<equiv> C = SUBSEQ C" |
|
282 |
|
283 |
|
284 |
|
285 |
|
286 |
|
287 |
|
288 primrec |
|
289 is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" |
|
290 where |
|
291 "is_prefix [] f = True" |
|
292 | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)" |
|
293 |
|
294 theorem L_idx: |
|
295 assumes L: "L w ws" |
|
296 shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L |
|
297 proof induct |
|
298 case (L0 v ws) |
|
299 hence "emb (f (length ws)) w" by simp |
|
300 moreover have "length ws < length (v # ws)" by simp |
|
301 ultimately show ?case by iprover |
|
302 next |
|
303 case (L1 ws v) |
|
304 then obtain i where emb: "emb (f i) w" and "i < length ws" |
|
305 by simp iprover |
|
306 hence "i < length (v # ws)" by simp |
|
307 with emb show ?case by iprover |
|
308 qed |
|
309 |
|
310 theorem good_idx: |
|
311 assumes good: "good ws" |
|
312 shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good |
|
313 proof induct |
|
314 case (good0 w ws) |
|
315 hence "w = f (length ws)" and "is_prefix ws f" by simp_all |
|
316 with good0 show ?case by (iprover dest: L_idx) |
|
317 next |
|
318 case (good1 ws w) |
|
319 thus ?case by simp |
|
320 qed |
|
321 |
|
322 theorem bar_idx: |
|
323 assumes bar: "bar ws" |
|
324 shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar |
|
325 proof induct |
|
326 case (bar1 ws) |
|
327 thus ?case by (rule good_idx) |
|
328 next |
|
329 case (bar2 ws) |
|
330 hence "is_prefix (f (length ws) # ws) f" by simp |
|
331 thus ?case by (rule bar2) |
|
332 qed |
|
333 |
|
334 text {* |
|
335 Strong version: yields indices of words that can be embedded into each other. |
|
336 *} |
|
337 |
|
338 theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j" |
|
339 proof (rule bar_idx) |
|
340 show "bar []" by (rule higman) |
|
341 show "is_prefix [] f" by simp |
|
342 qed |
|
343 |
|
344 text {* |
|
345 Weak version: only yield sequence containing words |
|
346 that can be embedded into each other. |
|
347 *} |
|
348 |
|
349 theorem good_prefix_lemma: |
|
350 assumes bar: "bar ws" |
|
351 shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar |
|
352 proof induct |
|
353 case bar1 |
|
354 thus ?case by iprover |
|
355 next |
|
356 case (bar2 ws) |
|
357 from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp |
|
358 thus ?case by (iprover intro: bar2) |
|
359 qed |
|
360 |
|
361 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs" |
|
362 using higman |
|
363 by (rule good_prefix_lemma) simp+ |
|
364 |
|
365 subsection {* Extracting the program *} |
|
366 |
|
367 declare R.induct [ind_realizer] |
|
368 declare T.induct [ind_realizer] |
|
369 declare L.induct [ind_realizer] |
|
370 declare good.induct [ind_realizer] |
|
371 declare bar.induct [ind_realizer] |
|
372 |
|
373 extract higman_idx |
|
374 |
|
375 text {* |
|
376 Program extracted from the proof of @{text higman_idx}: |
|
377 @{thm [display] higman_idx_def [no_vars]} |
|
378 Corresponding correctness theorem: |
|
379 @{thm [display] higman_idx_correctness [no_vars]} |
|
380 Program extracted from the proof of @{text higman}: |
|
381 @{thm [display] higman_def [no_vars]} |
|
382 Program extracted from the proof of @{text prop1}: |
|
383 @{thm [display] prop1_def [no_vars]} |
|
384 Program extracted from the proof of @{text prop2}: |
|
385 @{thm [display] prop2_def [no_vars]} |
|
386 Program extracted from the proof of @{text prop3}: |
|
387 @{thm [display] prop3_def [no_vars]} |
|
388 *} |
|
389 |
|
390 |
|
391 subsection {* Some examples *} |
|
392 |
|
393 instantiation LT and TT :: default |
|
394 begin |
|
395 |
|
396 definition "default = L0 [] []" |
|
397 |
|
398 definition "default = T0 A [] [] [] R0" |
|
399 |
|
400 instance .. |
|
401 |
|
402 end |
|
403 |
|
404 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where |
|
405 "mk_word_aux k = exec { |
|
406 i \<leftarrow> Random.range 10; |
|
407 (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair [] |
|
408 else exec { |
|
409 let l = (if i mod 2 = 0 then A else B); |
|
410 ls \<leftarrow> mk_word_aux (Suc k); |
|
411 Pair (l # ls) |
|
412 })}" |
|
413 by pat_completeness auto |
|
414 termination by (relation "measure ((op -) 1001)") auto |
|
415 |
|
416 definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where |
|
417 "mk_word = mk_word_aux 0" |
|
418 |
|
419 primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where |
|
420 "mk_word_s 0 = mk_word" |
|
421 | "mk_word_s (Suc n) = exec { |
|
422 _ \<leftarrow> mk_word; |
|
423 mk_word_s n |
|
424 }" |
|
425 |
|
426 definition g1 :: "nat \<Rightarrow> letter list" where |
|
427 "g1 s = fst (mk_word_s s (20000, 1))" |
|
428 |
|
429 definition g2 :: "nat \<Rightarrow> letter list" where |
|
430 "g2 s = fst (mk_word_s s (50000, 1))" |
|
431 |
|
432 fun f1 :: "nat \<Rightarrow> letter list" where |
|
433 "f1 0 = [A, A]" |
|
434 | "f1 (Suc 0) = [B]" |
|
435 | "f1 (Suc (Suc 0)) = [A, B]" |
|
436 | "f1 _ = []" |
|
437 |
|
438 fun f2 :: "nat \<Rightarrow> letter list" where |
|
439 "f2 0 = [A, A]" |
|
440 | "f2 (Suc 0) = [B]" |
|
441 | "f2 (Suc (Suc 0)) = [B, A]" |
|
442 | "f2 _ = []" |
|
443 |
|
444 ML {* |
|
445 local |
|
446 val higman_idx = @{code higman_idx}; |
|
447 val g1 = @{code g1}; |
|
448 val g2 = @{code g2}; |
|
449 val f1 = @{code f1}; |
|
450 val f2 = @{code f2}; |
|
451 in |
|
452 val (i1, j1) = higman_idx g1; |
|
453 val (v1, w1) = (g1 i1, g1 j1); |
|
454 val (i2, j2) = higman_idx g2; |
|
455 val (v2, w2) = (g2 i2, g2 j2); |
|
456 val (i3, j3) = higman_idx f1; |
|
457 val (v3, w3) = (f1 i3, f1 j3); |
|
458 val (i4, j4) = higman_idx f2; |
|
459 val (v4, w4) = (f2 i4, f2 j4); |
|
460 end; |
|
461 *} |
|
462 |
|
463 text {* The same story with the legacy SML code generator, |
|
464 this can be removed once the code generator is removed. *} |
|
465 |
|
466 code_module Higman |
|
467 contains |
|
468 higman = higman_idx |
|
469 |
|
470 ML {* |
|
471 local open Higman in |
|
472 |
|
473 val a = 16807.0; |
|
474 val m = 2147483647.0; |
|
475 |
|
476 fun nextRand seed = |
|
477 let val t = a*seed |
|
478 in t - m * real (Real.floor(t/m)) end; |
|
479 |
|
480 fun mk_word seed l = |
|
481 let |
|
482 val r = nextRand seed; |
|
483 val i = Real.round (r / m * 10.0); |
|
484 in if i > 7 andalso l > 2 then (r, []) else |
|
485 apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1)) |
|
486 end; |
|
487 |
|
488 fun f s zero = mk_word s 0 |
|
489 | f s (Suc n) = f (fst (mk_word s 0)) n; |
|
490 |
|
491 val g1 = snd o (f 20000.0); |
|
492 |
|
493 val g2 = snd o (f 50000.0); |
|
494 |
|
495 fun f1 zero = [A,A] |
|
496 | f1 (Suc zero) = [B] |
|
497 | f1 (Suc (Suc zero)) = [A,B] |
|
498 | f1 _ = []; |
|
499 |
|
500 fun f2 zero = [A,A] |
|
501 | f2 (Suc zero) = [B] |
|
502 | f2 (Suc (Suc zero)) = [B,A] |
|
503 | f2 _ = []; |
|
504 |
|
505 val (i1, j1) = higman g1; |
|
506 val (v1, w1) = (g1 i1, g1 j1); |
|
507 val (i2, j2) = higman g2; |
|
508 val (v2, w2) = (g2 i2, g2 j2); |
|
509 val (i3, j3) = higman f1; |
|
510 val (v3, w3) = (f1 i3, f1 j3); |
|
511 val (i4, j4) = higman f2; |
|
512 val (v4, w4) = (f2 i4, f2 j4); |
|
513 |
|
514 end; |
|
515 *} |
|
516 |
|
517 end |