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 \ Random.seed \ letter list \ 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 ((-) 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 {
_ \<leftarrow> 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 _ = []"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
