# Theory Higman

Up to index of Isabelle/HOL/Extraction

theory Higman
imports Main
begin

    (*  Title:      HOL/Extraction/Higman.thy
        ID:         $Id: Higman.thy,v 1.9 2005/09/23 14:05:42 nipkow Exp $
        Author:     Stefan Berghofer, TU Muenchen
                    Monika Seisenberger, LMU Muenchen
    *)

    header {* Higman's lemma *}

    theory Higman imports Main begin

    text {*
      Formalization by Stefan Berghofer and Monika Seisenberger,
      based on Coquand and Fridlender \cite{Coquand93}.
    *}

    datatype letter = A | B

    consts
      emb :: "(letter list × letter list) set"

    inductive emb
    intros
      emb0 [Pure.intro]: "([], bs) ∈ emb"
      emb1 [Pure.intro]: "(as, bs) ∈ emb ==> (as, b # bs) ∈ emb"
      emb2 [Pure.intro]: "(as, bs) ∈ emb ==> (a # as, a # bs) ∈ emb"

    consts
      L :: "letter list => letter list list set"

    inductive "L v"
    intros
      L0 [Pure.intro]: "(w, v) ∈ emb ==> w # ws ∈ L v"
      L1 [Pure.intro]: "ws ∈ L v ==> w # ws ∈ L v"

    consts
      good :: "letter list list set"

    inductive good
    intros
      good0 [Pure.intro]: "ws ∈ L w ==> w # ws ∈ good"
      good1 [Pure.intro]: "ws ∈ good ==> w # ws ∈ good"

    consts
      R :: "letter => (letter list list × letter list list) set"

    inductive "R a"
    intros
      R0 [Pure.intro]: "([], []) ∈ R a"
      R1 [Pure.intro]: "(vs, ws) ∈ R a ==> (w # vs, (a # w) # ws) ∈ R a"

    consts
      T :: "letter => (letter list list × letter list list) set"

    inductive "T a"
    intros
      T0 [Pure.intro]: "a ≠ b ==> (ws, zs) ∈ R b ==> (w # zs, (a # w) # zs) ∈ T a"
      T1 [Pure.intro]: "(ws, zs) ∈ T a ==> (w # ws, (a # w) # zs) ∈ T a"
      T2 [Pure.intro]: "a ≠ b ==> (ws, zs) ∈ T a ==> (ws, (b # w) # zs) ∈ T a"

    consts
      bar :: "letter list list set"

    inductive bar
    intros
      bar1 [Pure.intro]: "ws ∈ good ==> ws ∈ bar"
      bar2 [Pure.intro]: "(!!w. w # ws ∈ bar) ==> ws ∈ bar"

    theorem prop1: "([] # ws) ∈ bar" by iprover

    theorem lemma1: "ws ∈ L as ==> ws ∈ L (a # as)"
      by (erule L.induct, iprover+)

    lemma lemma2': "(vs, ws) ∈ R a ==> vs ∈ L as ==> ws ∈ L (a # as)"
      apply (induct set: R)
      apply (erule L.elims)
      apply simp+
      apply (erule L.elims)
      apply simp_all
      apply (rule L0)
      apply (erule emb2)
      apply (erule L1)
      done

    lemma lemma2: "(vs, ws) ∈ R a ==> vs ∈ good ==> ws ∈ good"
      apply (induct set: R)
      apply iprover
      apply (erule good.elims)
      apply simp_all
      apply (rule good0)
      apply (erule lemma2')
      apply assumption
      apply (erule good1)
      done

    lemma lemma3': "(vs, ws) ∈ T a ==> vs ∈ L as ==> ws ∈ L (a # as)"
      apply (induct set: T)
      apply (erule L.elims)
      apply simp_all
      apply (rule L0)
      apply (erule emb2)
      apply (rule L1)
      apply (erule lemma1)
      apply (erule L.elims)
      apply simp_all
      apply iprover+
      done

    lemma lemma3: "(ws, zs) ∈ T a ==> ws ∈ good ==> zs ∈ good"
      apply (induct set: T)
      apply (erule good.elims)
      apply simp_all
      apply (rule good0)
      apply (erule lemma1)
      apply (erule good1)
      apply (erule good.elims)
      apply simp_all
      apply (rule good0)
      apply (erule lemma3')
      apply iprover+
      done

    lemma lemma4: "(ws, zs) ∈ R a ==> ws ≠ [] ==> (ws, zs) ∈ T a"
      apply (induct set: R)
      apply iprover
      apply (case_tac vs)
      apply (erule R.elims)
      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) ≠ b ==> c ≠ a ==> 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 ∨ a ≠ 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 ≠ b" and bar: "xs ∈ bar"
      shows "!!ys zs. ys ∈ bar ==> (xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar" using bar
    proof induct
      fix xs zs assume "xs ∈ good" and "(xs, zs) ∈ T a"
      show "zs ∈ bar" by (rule bar1) (rule lemma3)
    next
      fix xs ys
      assume I: "!!w ys zs. ys ∈ bar ==> (w # xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar"
      assume "ys ∈ bar"
      thus "!!zs. (xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar"
      proof induct
        fix ys zs assume "ys ∈ good" and "(ys, zs) ∈ T b"
        show "zs ∈ bar" by (rule bar1) (rule lemma3)
      next
        fix ys zs assume I': "!!w zs. (xs, zs) ∈ T a ==> (w # ys, zs) ∈ T b ==> zs ∈ bar"
        and ys: "!!w. w # ys ∈ bar" and Ta: "(xs, zs) ∈ T a" and Tb: "(ys, zs) ∈ T b"
        show "zs ∈ bar"
        proof (rule bar2)
          fix w
          show "w # zs ∈ bar"
          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 "(a # cs) # zs ∈ bar" by (iprover intro: I ys Ta Tb)
              thus ?thesis by (simp add: Cons ca)
            next
              assume "c ≠ a"
              with ab have cb: "c = b" by (rule letter_neq)
              from ab have "(b # cs) # zs ∈ bar" by (iprover intro: I' Ta Tb)
              thus ?thesis by (simp add: Cons cb)
            qed
          qed
        qed
      qed
    qed

    theorem prop3:
      assumes bar: "xs ∈ bar"
      shows "!!zs. xs ≠ [] ==> (xs, zs) ∈ R a ==> zs ∈ bar" using bar
    proof induct
      fix xs zs
      assume "xs ∈ good" and "(xs, zs) ∈ R a"
      show "zs ∈ bar" by (rule bar1) (rule lemma2)
    next
      fix xs zs
      assume I: "!!w zs. w # xs ≠ [] ==> (w # xs, zs) ∈ R a ==> zs ∈ bar"
      and xsb: "!!w. w # xs ∈ bar" and xsn: "xs ≠ []" and R: "(xs, zs) ∈ R a"
      show "zs ∈ bar"
      proof (rule bar2)
        fix w
        show "w # zs ∈ bar"
        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: "(xs, zs) ∈ T a" by (rule lemma4)
            assume "c ≠ 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 "[w] ∈ bar"
      proof (induct w)
        show "[[]] ∈ bar" by (rule prop1)
      next
        fix c cs assume "[cs] ∈ bar"
        thus "[c # cs] ∈ bar" by (rule prop3) (simp, iprover)
      qed
    qed

    consts
      is_prefix :: "'a list => (nat => 'a) => bool"

    primrec
      "is_prefix [] f = True"
      "is_prefix (x # xs) f = (x = f (length xs) ∧ is_prefix xs f)"

    theorem good_prefix_lemma:
      assumes bar: "ws ∈ bar"
      shows "is_prefix ws f ==> ∃vs. is_prefix vs f ∧ vs ∈ good" using bar
    proof induct
      case bar1
      thus ?case by iprover
    next
      case (bar2 ws)
      have "is_prefix (f (length ws) # ws) f" by simp
      thus ?case by (iprover intro: bar2)
    qed

    theorem good_prefix: "∃vs. is_prefix vs f ∧ vs ∈ good"
      using higman
      by (rule good_prefix_lemma) simp+

    subsection {* Extracting the program *}

    declare bar.induct [ind_realizer]

    extract good_prefix

    text {*
      Program extracted from the proof of @{text good_prefix}:
      @{thm [display] good_prefix_def [no_vars]}
      Corresponding correctness theorem:
      @{thm [display] good_prefix_correctness [no_vars]}
      Program extracted from the proof of @{text good_prefix_lemma}:
      @{thm [display] good_prefix_lemma_def [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]}
    *}

    code_module Higman
    contains
      test = good_prefix

    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 id_0 = 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 id_0 = [A,A]
      | f1 (Suc id_0) = [B]
      | f1 (Suc (Suc id_0)) = [A,B]
      | f1 _ = [];

    fun f2 id_0 = [A,A]
      | f2 (Suc id_0) = [B]
      | f2 (Suc (Suc id_0)) = [B,A]
      | f2 _ = [];

    val xs1 = test g1;
    val xs2 = test g2;
    val xs3 = test f1;
    val xs4 = test f2;

    end;
    *}

    end

theorem prop1:

      [] # ws ∈ bar

theorem lemma1:

      ws ∈ L as ==> ws ∈ L (a # as)

lemma lemma2':

      [| (vs, ws) ∈ R a; vs ∈ L as |] ==> ws ∈ L (a # as)

lemma lemma2:

      [| (vs, ws) ∈ R a; vs ∈ good |] ==> ws ∈ good

lemma lemma3':

      [| (vs, ws) ∈ T a; vs ∈ L as |] ==> ws ∈ L (a # as)

lemma lemma3:

      [| (ws, zs) ∈ T a; ws ∈ good |] ==> zs ∈ good

lemma lemma4:

      [| (ws, zs) ∈ R a; ws ≠ [] |] ==> (ws, zs) ∈ T a

lemma letter_neq:

      [| a ≠ b; c ≠ a |] ==> c = b

lemma letter_eq_dec:

      a = b ∨ a ≠ b

theorem prop2:

      [| a ≠ b; xs ∈ bar; ys ∈ bar; (xs, zs) ∈ T a; (ys, zs) ∈ T b |] ==> zs ∈ bar

theorem prop3:

      [| xs ∈ bar; xs ≠ []; (xs, zs) ∈ R a |] ==> zs ∈ bar

theorem higman:

      [] ∈ bar

theorem good_prefix_lemma:

      [| ws ∈ bar; is_prefix ws f |] ==> ∃vs. is_prefix vs f ∧ vs ∈ good

theorem good_prefix:

      ∃vs. is_prefix vs f ∧ vs ∈ good

### Extracting the program