(* Title: HOL/Proofs/Extraction/Higman_Extraction.thy
Author: Stefan Berghofer, TU Muenchen
Author: Monika Seisenberger, LMU Muenchen
*)
(*<*)
theory Higman_Extraction
imports Higman "~~/src/HOL/Library/State_Monad" Random
begin
(*>*)
subsection \<open>Extracting the program\<close>
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