(*  Title:      HOL/Proofs/Extraction/Higman.thy+
−
    Author:     Stefan Berghofer, TU Muenchen+
−
    Author:     Monika Seisenberger, LMU Muenchen+
−
*)+
−
+
−
header {* Higman's lemma *}+
−
+
−
theory Higman2+
−
imports Main+
−
begin+
−
+
−
text {*+
−
  Formalization by Stefan Berghofer and Monika Seisenberger,+
−
  based on Coquand and Fridlender \cite{Coquand93}.+
−
*}+
−
+
−
datatype letter = A | B+
−
+
−
inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"+
−
where+
−
   emb0 [Pure.intro]: "emb [] bs"+
−
 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"+
−
 | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"+
−
+
−
inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"+
−
  for v :: "letter list"+
−
where+
−
   L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"+
−
 | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"+
−
+
−
inductive good :: "letter list list \<Rightarrow> bool"+
−
where+
−
    good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"+
−
  | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"+
−
+
−
inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"+
−
  for a :: letter+
−
where+
−
    R0 [Pure.intro]: "R a [] []"+
−
  | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"+
−
+
−
inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"+
−
  for a :: letter+
−
where+
−
    T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"+
−
  | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"+
−
  | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"+
−
+
−
inductive bar :: "letter list list \<Rightarrow> bool"+
−
where+
−
    bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"+
−
  | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"+
−
+
−
theorem prop1: "bar ([] # ws)" by iprover+
−
+
−
theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws"+
−
  by (erule L.induct, iprover+)+
−
+
−
lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"+
−
  apply (induct set: R)+
−
  apply (erule L.cases)+
−
  apply simp++
−
  apply (erule L.cases)+
−
  apply simp_all+
−
  apply (rule L0)+
−
  apply (erule emb2)+
−
  apply (erule L1)+
−
  done+
−
+
−
lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws"+
−
  apply (induct set: R)+
−
  apply iprover+
−
  apply (erule good.cases)+
−
  apply simp_all+
−
  apply (rule good0)+
−
  apply (erule lemma2')+
−
  apply assumption+
−
  apply (erule good1)+
−
  done+
−
+
−
lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"+
−
  apply (induct set: T)+
−
  apply (erule L.cases)+
−
  apply simp_all+
−
  apply (rule L0)+
−
  apply (erule emb2)+
−
  apply (rule L1)+
−
  apply (erule lemma1)+
−
  apply (erule L.cases)+
−
  apply simp_all+
−
  apply iprover++
−
  done+
−
+
−
lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs"+
−
  apply (induct set: T)+
−
  apply (erule good.cases)+
−
  apply simp_all+
−
  apply (rule good0)+
−
  apply (erule lemma1)+
−
  apply (erule good1)+
−
  apply (erule good.cases)+
−
  apply simp_all+
−
  apply (rule good0)+
−
  apply (erule lemma3')+
−
  apply iprover++
−
  done+
−
+
−
lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"+
−
  apply (induct set: R)+
−
  apply iprover+
−
  apply (case_tac vs)+
−
  apply (erule R.cases)+
−
  apply simp+
−
  apply (case_tac a)+
−
  apply (rule_tac b=B in T0)+
−
  apply simp+
−
  apply (rule R0)+
−
  apply (rule_tac b=A in T0)+
−
  apply simp+
−
  apply (rule R0)+
−
  apply simp+
−
  apply (rule T1)+
−
  apply simp+
−
  done+
−
+
−
lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"+
−
  apply (case_tac a)+
−
  apply (case_tac b)+
−
  apply (case_tac c, simp, simp)+
−
  apply (case_tac c, simp, simp)+
−
  apply (case_tac b)+
−
  apply (case_tac c, simp, simp)+
−
  apply (case_tac c, simp, simp)+
−
  done+
−
+
−
lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"+
−
  apply (case_tac a)+
−
  apply (case_tac b)+
−
  apply simp+
−
  apply simp+
−
  apply (case_tac b)+
−
  apply simp+
−
  apply simp+
−
  done+
−
+
−
theorem prop2:+
−
  assumes ab: "a \<noteq> b" and bar: "bar xs"+
−
  shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar+
−
proof induct+
−
  fix xs zs assume "T a xs zs" and "good xs"+
−
  hence "good zs" by (rule lemma3)+
−
  then show "bar zs" by (rule bar1)+
−
next+
−
  fix xs ys+
−
  assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"+
−
  assume "bar ys"+
−
  thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"+
−
  proof induct+
−
    fix ys zs assume "T b ys zs" and "good ys"+
−
    then have "good zs" by (rule lemma3)+
−
    then show "bar zs" by (rule bar1)+
−
  next+
−
    fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"+
−
    and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"+
−
    show "bar zs"+
−
    proof (rule bar2)+
−
      fix w+
−
      show "bar (w # zs)"+
−
      proof (cases w)+
−
        case Nil+
−
        thus ?thesis by simp (rule prop1)+
−
      next+
−
        case (Cons c cs)+
−
        from letter_eq_dec show ?thesis+
−
        proof+
−
          assume ca: "c = a"+
−
          from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb)+
−
          thus ?thesis by (simp add: Cons ca)+
−
        next+
−
          assume "c \<noteq> a"+
−
          with ab have cb: "c = b" by (rule letter_neq)+
−
          from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb)+
−
          thus ?thesis by (simp add: Cons cb)+
−
        qed+
−
      qed+
−
    qed+
−
  qed+
−
qed+
−
+
−
theorem prop3:+
−
  assumes bar: "bar xs"+
−
  shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar+
−
proof induct+
−
  fix xs zs+
−
  assume "R a xs zs" and "good xs"+
−
  then have "good zs" by (rule lemma2)+
−
  then show "bar zs" by (rule bar1)+
−
next+
−
  fix xs zs+
−
  assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"+
−
  and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"+
−
  show "bar zs"+
−
  proof (rule bar2)+
−
    fix w+
−
    show "bar (w # zs)"+
−
    proof (induct w)+
−
      case Nil+
−
      show ?case by (rule prop1)+
−
    next+
−
      case (Cons c cs)+
−
      from letter_eq_dec show ?case+
−
      proof+
−
        assume "c = a"+
−
        thus ?thesis by (iprover intro: I [simplified] R)+
−
      next+
−
        from R xsn have T: "T a xs zs" by (rule lemma4)+
−
        assume "c \<noteq> a"+
−
        thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)+
−
      qed+
−
    qed+
−
  qed+
−
qed+
−
+
−
theorem higman: "bar []"+
−
proof (rule bar2)+
−
  fix w+
−
  show "bar [w]"+
−
  proof (induct w)+
−
    show "bar [[]]" by (rule prop1)+
−
  next+
−
    fix c cs assume "bar [cs]"+
−
    thus "bar [c # cs]" by (rule prop3) (simp, iprover)+
−
  qed+
−
qed+
−
+
−
notation+
−
  emb ("_ \<preceq> _")+
−
+
−
+
−
+
−
lemma substring_refl:+
−
  "x \<preceq> x"+
−
apply(induct x)+
−
apply(auto intro: emb.intros)+
−
done+
−
+
−
lemma substring_trans:+
−
  assumes a: "x1 \<preceq> x2" and b: "x2 \<preceq> x3"+
−
  shows "x1 \<preceq> x3"+
−
using a b+
−
apply(induct arbitrary: x3)+
−
apply(auto intro: emb.intros)+
−
apply(rotate_tac 2)+
−
apply(erule emb.cases)+
−
apply(simp_all)+
−
sorry +
−
+
−
definition+
−
 "SUBSEQ C \<equiv> {x. \<exists>y \<in> C. x \<preceq> y}"+
−
+
−
lemma+
−
 "SUBSEQ (SUBSEQ C) = SUBSEQ C"+
−
unfolding SUBSEQ_def+
−
apply(auto)+
−
apply(erule emb.induct)+
−
apply(rule_tac x="xb" in bexI)+
−
apply(rule emb.intros)+
−
apply(simp)+
−
apply(erule bexE)+
−
apply(rule_tac x="y" in bexI)+
−
apply(auto)[2]+
−
apply(erule bexE)+
−
sorry+
−
+
−
lemma substring_closed:+
−
  "x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C"+
−
unfolding SUBSEQ_def+
−
apply(auto)+
−
apply(rule_tac x="xa" in bexI)+
−
apply(rule substring_trans)+
−
apply(auto)+
−
done+
−
+
−
lemma "SUBSEQ C \<subseteq> UNIV"+
−
unfolding SUBSEQ_def+
−
apply(auto)+
−
done+
−
+
−
+
−
+
−
ML {*+
−
@{term "UNIV - (C::string set)"}+
−
*}+
−
+
−
lemma+
−
  assumes "finite S"+
−
  shows "finite (UNIV - {y. \<forall>z \<in> S. \<not>(z \<preceq> y)})"+
−
oops+
−
 +
−
+
−
+
−
lemma a: "\<forall>x \<in> SUBSEQ C. \<exists>y \<in> C. x \<preceq> y"+
−
unfolding SUBSEQ_def +
−
apply(auto)+
−
done+
−
+
−
lemma b:+
−
  shows "\<exists>S \<subseteq> SUBSEQ C. S \<noteq>{} \<and> (y \<in> C \<longleftrightarrow> (\<forall>z \<in> S. \<not>(z \<preceq> y)))"+
−
sorry+
−
+
−
lemma "False"+
−
using b a+
−
apply(blast)+
−
done+
−
+
−
definition+
−
 "CLOSED C \<equiv> C = SUBSEQ C"+
−
+
−
+
−
+
−
+
−
+
−
+
−
primrec+
−
  is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"+
−
where+
−
    "is_prefix [] f = True"+
−
  | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"+
−
+
−
theorem L_idx:+
−
  assumes L: "L w ws"+
−
  shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L+
−
proof induct+
−
  case (L0 v ws)+
−
  hence "emb (f (length ws)) w" by simp+
−
  moreover have "length ws < length (v # ws)" by simp+
−
  ultimately show ?case by iprover+
−
next+
−
  case (L1 ws v)+
−
  then obtain i where emb: "emb (f i) w" and "i < length ws"+
−
    by simp iprover+
−
  hence "i < length (v # ws)" by simp+
−
  with emb show ?case by iprover+
−
qed+
−
+
−
theorem good_idx:+
−
  assumes good: "good ws"+
−
  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good+
−
proof induct+
−
  case (good0 w ws)+
−
  hence "w = f (length ws)" and "is_prefix ws f" by simp_all+
−
  with good0 show ?case by (iprover dest: L_idx)+
−
next+
−
  case (good1 ws w)+
−
  thus ?case by simp+
−
qed+
−
+
−
theorem bar_idx:+
−
  assumes bar: "bar ws"+
−
  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar+
−
proof induct+
−
  case (bar1 ws)+
−
  thus ?case by (rule good_idx)+
−
next+
−
  case (bar2 ws)+
−
  hence "is_prefix (f (length ws) # ws) f" by simp+
−
  thus ?case by (rule bar2)+
−
qed+
−
+
−
text {*+
−
Strong version: yields indices of words that can be embedded into each other.+
−
*}+
−
+
−
theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"+
−
proof (rule bar_idx)+
−
  show "bar []" by (rule higman)+
−
  show "is_prefix [] f" by simp+
−
qed+
−
+
−
definition+
−
  myeq ("~~")+
−
where+
−
  "~~ \<equiv> {(x, y). x \<preceq> y \<and> y \<preceq> x}"+
−
+
−
abbreviation+
−
  myeq_applied ("_ ~~~ _")+
−
where+
−
  "x ~~~ y \<equiv> (x, y) \<in> ~~"+
−
+
−
+
−
definition+
−
 "minimal x Y \<equiv> (x \<in> Y \<and> (\<forall>y \<in> Y. y \<preceq> x \<longrightarrow> x \<preceq> y))"+
−
+
−
definition+
−
 "downclosed Y \<equiv> (\<forall>x \<in> Y. \<forall>y. y \<preceq> x \<longrightarrow> y \<in> Y)" +
−
+
−
+
−
lemma g:+
−
  assumes "minimal x Y" "y ~~~ x" "downclosed Y"+
−
  shows "minimal y Y"+
−
using assms+
−
apply(simp add: minimal_def)+
−
apply(rule conjI)+
−
apply(simp add: downclosed_def)+
−
apply(simp add: myeq_def)+
−
apply(auto)[1]+
−
apply(rule ballI)+
−
apply(rule impI)+
−
apply(simp add: downclosed_def)+
−
apply(simp add: myeq_def)+
−
apply(erule conjE)+
−
apply(rotate_tac 5)+
−
apply(drule_tac x="ya" in bspec)+
−
apply(auto)[1]+
−
apply(drule mp)+
−
apply(erule conjE)+
−
apply(rule substring_trans)+
−
apply(auto)[2]+
−
apply(rule substring_trans)+
−
apply(auto)[2]+
−
done+
−
+
−
thm Least_le+
−
+
−
lemma+
−
  assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"+
−
  and "downclosed Y"+
−
  shows "\<exists>S. finite S \<and> (\<forall>x \<in> Y. \<exists>y \<in> S. \<not> (y \<preceq> x))"+
−
proof -+
−
  def Ymin \<equiv> "{x. minimal x Y}"+
−
  have "downclosed Ymin"+
−
  unfolding Ymin_def downclosed_def+
−
  apply(auto)+
−
  apply(simp add: minimal_def)+
−
  apply(rule conjI)+
−
  using assms(2)+
−
  apply(simp add: downclosed_def)+
−
  apply(auto)[1]+
−
  apply(rule ballI) +
−
  apply(rule impI)+
−
  apply(erule conjE)+
−
  apply(drule_tac x="ya" in bspec)+
−
  apply(simp)+
−
  apply(drule mp)+
−
  apply(rule substring_trans)+
−
  apply(auto)[2]+
−
  apply(rule substring_trans)+
−
  apply(auto)[2]+
−
  done+
−
  def Yeq \<equiv> "Ymin // ~~"+
−
  def Ypick \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Yeq" +
−
  have "finite Ypick" sorry+
−
  moreover+
−
  thm LeastI_ex+
−
  have "(\<forall>x \<in> Y. \<exists>y \<in> Ypick. (\<not> (y \<preceq> x)))"+
−
  apply(rule ballI)+
−
  apply(subgoal_tac "\<exists>y. y \<in> Ypick")+
−
  apply(erule exE)+
−
  apply(rule_tac x="y" in bexI)+
−
  apply(subgoal_tac "y \<in> Ymin")+
−
  apply(simp add: Ymin_def minimal_def)+
−
  apply(subgoal_tac "~~ `` {y} \<in> Yeq")+
−
  apply(simp add: Yeq_def quotient_def Image_def)+
−
  apply(erule bexE)+
−
  apply(simp add: Ymin_def)+
−
  apply(subgoal_tac "y ~~~ xa")+
−
  apply(drule g)+
−
  apply(assumption)+
−
  apply(rule assms(2))+
−
  apply(simp add: minimal_def)+
−
  apply(erule conjE)+
−
  apply(drule_tac x="x" in bspec)+
−
  apply(assumption)+
−
  +
−
lemma+
−
  assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"+
−
  and b: "downclosed Y" +
−
  and c: "Y \<noteq> {}"+
−
  shows "\<exists>S. finite S \<and> (Y = {y. (\<forall>z \<in> S. \<not>(z \<preceq> y))})"+
−
proof -+
−
  def Ybar \<equiv> "- Y"+
−
  def M \<equiv> "{x \<in> Ybar. minimal x Ybar}"+
−
  def Cpre \<equiv> "M // ~~"+
−
  def C \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Cpre"+
−
  have "finite C" sorry+
−
  moreover+
−
  have "\<forall>x \<in> Y. \<exists>y \<in> C.  y \<preceq> x" sorry+
−
  then have "\<forall>x. (x \<in> Ybar) \<longleftrightarrow> (\<exists>z \<in> C. z \<preceq> x)"+
−
  apply(auto simp add: Ybar_def)+
−
    apply(rule allI)+
−
    apply(rule iffI)+
−
    prefer 2+
−
    apply(erule bexE)+
−
    apply(case_tac "x \<in> Y")+
−
    prefer 2+
−
    apply(simp add: Ybar_def)+
−
    apply(subgoal_tac "z \<in> Y")+
−
    apply(simp add: C_def)+
−
    apply(simp add: Cpre_def)+
−
    apply(simp add: M_def Ybar_def)+
−
    apply(simp add: quotient_def)+
−
    apply(simp add: myeq_def)+
−
    apply(simp add: image_def)+
−
    apply(rule_tac x="x" in exI)+
−
    apply(simp)+
−
    apply(rule conjI)+
−
    apply(simp add: minimal_def)+
−
    apply(rule ballI)+
−
    apply(simp)+
−
    apply(rule impI)+
−
    prefer 3+
−
    apply(simp add: Ybar_def)+
−
    apply(rule notI)+
−
    apply(simp add: C_def Cpre_def M_def Ybar_def quotient_def)+
−
+
−
    prefer 2+
−
    apply(rule someI2_ex)+
−
    apply(rule_tac x="x" in exI) +
−
    apply(simp add: substring_refl)+
−
    apply(auto)[1]+
−
    using b+
−
    apply -+
−
    sorry+
−
  ultimately+
−
  have "\<exists>S. finite S \<and> (\<forall>y. y \<in> Y  = (\<forall>z \<in> S. \<not>(z \<preceq> y)))"+
−
    apply -+
−
    apply(rule_tac x="C" in exI)+
−
    apply(simp)+
−
    apply(rule allI)+
−
    apply(rule iffI) +
−
    apply(drule_tac x="y" in spec)+
−
    apply(simp add: Ybar_def)+
−
    apply(simp add: Ybar_def)+
−
    apply(case_tac "y \<in> Y")+
−
    apply(simp)+
−
    apply(drule_tac x="y" in spec)+
−
    apply(simp)+
−
    done+
−
    then show ?thesis+
−
    by (auto)+
−
qed      +
−
+
−
+
−
thm higman_idx+
−
+
−
text {*+
−
Weak version: only yield sequence containing words+
−
that can be embedded into each other.+
−
*}+
−
+
−
theorem good_prefix_lemma:+
−
  assumes bar: "bar ws"+
−
  shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar+
−
proof induct+
−
  case bar1+
−
  thus ?case by iprover+
−
next+
−
  case (bar2 ws)+
−
  from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp+
−
  thus ?case by (iprover intro: bar2)+
−
qed+
−
+
−
theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs"+
−
  using higman+
−
  by (rule good_prefix_lemma) simp++
−
+
−
subsection {* Extracting the program *}+
−
+
−
declare R.induct [ind_realizer]+
−
declare T.induct [ind_realizer]+
−
declare L.induct [ind_realizer]+
−
declare good.induct [ind_realizer]+
−
declare bar.induct [ind_realizer]+
−
+
−
extract higman_idx+
−
+
−
text {*+
−
  Program extracted from the proof of @{text higman_idx}:+
−
  @{thm [display] higman_idx_def [no_vars]}+
−
  Corresponding correctness theorem:+
−
  @{thm [display] higman_idx_correctness [no_vars]}+
−
  Program extracted from the proof of @{text higman}:+
−
  @{thm [display] higman_def [no_vars]}+
−
  Program extracted from the proof of @{text prop1}:+
−
  @{thm [display] prop1_def [no_vars]}+
−
  Program extracted from the proof of @{text prop2}:+
−
  @{thm [display] prop2_def [no_vars]}+
−
  Program extracted from the proof of @{text prop3}:+
−
  @{thm [display] prop3_def [no_vars]}+
−
*}+
−
+
−
+
−
subsection {* Some examples *}+
−
+
−
instantiation LT and TT :: default+
−
begin+
−
+
−
definition "default = L0 [] []"+
−
+
−
definition "default = T0 A [] [] [] R0"+
−
+
−
instance ..+
−
+
−
end+
−
+
−
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where+
−
  "mk_word_aux k = exec {+
−
     i \<leftarrow> Random.range 10;+
−
     (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []+
−
     else exec {+
−
       let l = (if i mod 2 = 0 then A else B);+
−
       ls \<leftarrow> mk_word_aux (Suc k);+
−
       Pair (l # ls)+
−
     })}"+
−
by pat_completeness auto+
−
termination by (relation "measure ((op -) 1001)") auto+
−
+
−
definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where+
−
  "mk_word = mk_word_aux 0"+
−
+
−
primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where+
−
  "mk_word_s 0 = mk_word"+
−
  | "mk_word_s (Suc n) = exec {+
−
       _ \<leftarrow> mk_word;+
−
       mk_word_s n+
−
     }"+
−
+
−
definition g1 :: "nat \<Rightarrow> letter list" where+
−
  "g1 s = fst (mk_word_s s (20000, 1))"+
−
+
−
definition g2 :: "nat \<Rightarrow> letter list" where+
−
  "g2 s = fst (mk_word_s s (50000, 1))"+
−
+
−
fun f1 :: "nat \<Rightarrow> letter list" where+
−
  "f1 0 = [A, A]"+
−
  | "f1 (Suc 0) = [B]"+
−
  | "f1 (Suc (Suc 0)) = [A, B]"+
−
  | "f1 _ = []"+
−
+
−
fun f2 :: "nat \<Rightarrow> letter list" where+
−
  "f2 0 = [A, A]"+
−
  | "f2 (Suc 0) = [B]"+
−
  | "f2 (Suc (Suc 0)) = [B, A]"+
−
  | "f2 _ = []"+
−
+
−
ML {*+
−
local+
−
  val higman_idx = @{code higman_idx};+
−
  val g1 = @{code g1};+
−
  val g2 = @{code g2};+
−
  val f1 = @{code f1};+
−
  val f2 = @{code f2};+
−
in+
−
  val (i1, j1) = higman_idx g1;+
−
  val (v1, w1) = (g1 i1, g1 j1);+
−
  val (i2, j2) = higman_idx g2;+
−
  val (v2, w2) = (g2 i2, g2 j2);+
−
  val (i3, j3) = higman_idx f1;+
−
  val (v3, w3) = (f1 i3, f1 j3);+
−
  val (i4, j4) = higman_idx f2;+
−
  val (v4, w4) = (f2 i4, f2 j4);+
−
end;+
−
*}+
−
+
−
text {* The same story with the legacy SML code generator,+
−
this can be removed once the code generator is removed. *}+
−
+
−
code_module Higman+
−
contains+
−
  higman = higman_idx+
−
+
−
ML {*+
−
local open Higman in+
−
+
−
val a = 16807.0;+
−
val m = 2147483647.0;+
−
+
−
fun nextRand seed =+
−
  let val t = a*seed+
−
  in  t - m * real (Real.floor(t/m)) end;+
−
+
−
fun mk_word seed l =+
−
  let+
−
    val r = nextRand seed;+
−
    val i = Real.round (r / m * 10.0);+
−
  in if i > 7 andalso l > 2 then (r, []) else+
−
    apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))+
−
  end;+
−
+
−
fun f s zero = mk_word s 0+
−
  | f s (Suc n) = f (fst (mk_word s 0)) n;+
−
+
−
val g1 = snd o (f 20000.0);+
−
+
−
val g2 = snd o (f 50000.0);+
−
+
−
fun f1 zero = [A,A]+
−
  | f1 (Suc zero) = [B]+
−
  | f1 (Suc (Suc zero)) = [A,B]+
−
  | f1 _ = [];+
−
+
−
fun f2 zero = [A,A]+
−
  | f2 (Suc zero) = [B]+
−
  | f2 (Suc (Suc zero)) = [B,A]+
−
  | f2 _ = [];+
−
+
−
val (i1, j1) = higman g1;+
−
val (v1, w1) = (g1 i1, g1 j1);+
−
val (i2, j2) = higman g2;+
−
val (v2, w2) = (g2 i2, g2 j2);+
−
val (i3, j3) = higman f1;+
−
val (v3, w3) = (f1 i3, f1 j3);+
−
val (i4, j4) = higman f2;+
−
val (v4, w4) = (f2 i4, f2 j4);+
−
+
−
end;+
−
*}+
−
+
−
end+
−