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