equal
deleted
inserted
replaced
288 @{thm [display] prop2_def [no_vars]} |
288 @{thm [display] prop2_def [no_vars]} |
289 Program extracted from the proof of @{text prop3}: |
289 Program extracted from the proof of @{text prop3}: |
290 @{thm [display] prop3_def [no_vars]} |
290 @{thm [display] prop3_def [no_vars]} |
291 *} |
291 *} |
292 |
292 |
293 generate_code |
293 code_module Higman |
|
294 contains |
294 test = good_prefix |
295 test = good_prefix |
295 |
296 |
296 ML {* |
297 ML {* |
|
298 local open Higman in |
|
299 |
297 val a = 16807.0; |
300 val a = 16807.0; |
298 val m = 2147483647.0; |
301 val m = 2147483647.0; |
299 |
302 |
300 fun nextRand seed = |
303 fun nextRand seed = |
301 let val t = a*seed |
304 let val t = a*seed |
307 val i = Real.round (r / m * 10.0); |
310 val i = Real.round (r / m * 10.0); |
308 in if i > 7 andalso l > 2 then (r, []) else |
311 in if i > 7 andalso l > 2 then (r, []) else |
309 apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1)) |
312 apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1)) |
310 end; |
313 end; |
311 |
314 |
312 fun f s id0 = mk_word s 0 |
315 fun f s id_0 = mk_word s 0 |
313 | f s (Suc n) = f (fst (mk_word s 0)) n; |
316 | f s (Suc n) = f (fst (mk_word s 0)) n; |
314 |
317 |
315 val g1 = snd o (f 20000.0); |
318 val g1 = snd o (f 20000.0); |
316 |
319 |
317 val g2 = snd o (f 50000.0); |
320 val g2 = snd o (f 50000.0); |
318 |
321 |
319 fun f1 id0 = [A,A] |
322 fun f1 id_0 = [A,A] |
320 | f1 (Suc id0) = [B] |
323 | f1 (Suc id_0) = [B] |
321 | f1 (Suc (Suc id0)) = [A,B] |
324 | f1 (Suc (Suc id_0)) = [A,B] |
322 | f1 _ = []; |
325 | f1 _ = []; |
323 |
326 |
324 fun f2 id0 = [A,A] |
327 fun f2 id_0 = [A,A] |
325 | f2 (Suc id0) = [B] |
328 | f2 (Suc id_0) = [B] |
326 | f2 (Suc (Suc id0)) = [B,A] |
329 | f2 (Suc (Suc id_0)) = [B,A] |
327 | f2 _ = []; |
330 | f2 _ = []; |
328 |
331 |
329 val xs1 = test g1; |
332 val xs1 = test g1; |
330 val xs2 = test g2; |
333 val xs2 = test g2; |
331 val xs3 = test f1; |
334 val xs3 = test f1; |
332 val xs4 = test f2; |
335 val xs4 = test f2; |
|
336 |
|
337 end; |
333 *} |
338 *} |
334 |
339 |
335 end |
340 end |