src/HOL/Proofs/Extraction/Higman_Extraction.thy

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

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

subsection \<open>Extracting the program\<close>

theory Higman_Extraction
imports Higman "HOL-Library.Old_Datatype" "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 \<open>
  Program extracted from the proof of \<open>higman_idx\<close>:
  @{thm [display] higman_idx_def [no_vars]}
  Corresponding correctness theorem:
  @{thm [display] higman_idx_correctness [no_vars]}
  Program extracted from the proof of \<open>higman\<close>:
  @{thm [display] higman_def [no_vars]}
  Program extracted from the proof of \<open>prop1\<close>:
  @{thm [display] prop1_def [no_vars]}
  Program extracted from the proof of \<open>prop2\<close>:
  @{thm [display] prop2_def [no_vars]}
  Program extracted from the proof of \<open>prop3\<close>:
  @{thm [display] prop3_def [no_vars]}
\<close>


subsection \<open>Some examples\<close>

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_val \<open>
  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;
\<close>

end