(*  Title:      HOL/Proofs/Extraction/Higman_Extraction.thy
    Author:     Stefan Berghofer, TU Muenchen
    Author:     Monika Seisenberger, LMU Muenchen
*)

subsection ‹Extracting the program›

theory Higman_Extraction
imports Higman "HOL-Library.Realizers" "HOL-Library.Open_State_Syntax"
begin

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 ‹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 ‹higman›:
 @{thm [display] higman_def [no_vars]}
 Program extracted from the proof of ‹prop1›:
 @{thm [display] prop1_def [no_vars]}
 Program extracted from the proof of ‹prop2›:
 @{thm [display] prop2_def [no_vars]}
 Program extracted from the proof of ‹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 → Random.seed → letter list × Random.seed"
where
  "mk_word_aux k = exec {
     i ← Random.range 10;
     (if i > 7 ∧ k > 2 ∨ k > 1000 then Pair []
      else exec {
        let l = (if i mod 2 = 0 then A else B);
        ls ← mk_word_aux (Suc k);
        Pair (l # ls)
      })}"
  by pat_completeness auto
termination
  by (relation "measure ((-) 1001)") auto

definition mk_word :: "Random.seed → letter list × Random.seed"
  where "mk_word = mk_word_aux 0"

primrec mk_word_s :: "nat → Random.seed → letter list × Random.seed"
where
  "mk_word_s 0 = mk_word"
| "mk_word_s (Suc n) = exec {
     _ ← mk_word;
     mk_word_s n
   }"

definition g1 :: "nat → letter list"
  where "g1 s = fst (mk_word_s s (20000, 1))"

definition g2 :: "nat → letter list"
  where "g2 s = fst (mk_word_s s (50000, 1))"

fun f1 :: "nat → letter list"
where
  "f1 0 = [A, A]"
| "f1 (Suc 0) = [B]"
| "f1 (Suc (Suc 0)) = [A, B]"
| "f1 _ = []"

fun f2 :: "nat → letter list"
where
  "f2 0 = [A, A]"
| "f2 (Suc 0) = [B]"
| "f2 (Suc (Suc 0)) = [B, A]"
| "f2 _ = []"

ML_val ‹
 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;
 ›

end