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