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