--- a/src/HOL/Extraction/Higman.thy Fri May 15 16:39:16 2009 +0200
+++ b/src/HOL/Extraction/Higman.thy Fri May 15 16:39:16 2009 +0200
@@ -349,9 +349,9 @@
end
-function mk_word_aux :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_aux k = (do
- i \<leftarrow> range 10;
+ i \<leftarrow> Random.range 10;
(if i > 7 \<and> k > 2 \<or> k > 1000 then return []
else do
let l = (if i mod 2 = 0 then A else B);
@@ -362,10 +362,10 @@
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
-definition mk_word :: "seed \<Rightarrow> letter list \<times> seed" where
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word = mk_word_aux 0"
-primrec mk_word_s :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+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) = (do
_ \<leftarrow> mk_word;
--- a/src/HOL/Library/Random.thy Fri May 15 16:39:16 2009 +0200
+++ b/src/HOL/Library/Random.thy Fri May 15 16:39:16 2009 +0200
@@ -87,6 +87,32 @@
by (simp add: scomp_apply split_beta select_def)
qed
+primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+ "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
+
+lemma pick_member:
+ "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
+ by (induct xs arbitrary: i) simp_all
+
+lemma pick_drop_zero:
+ "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
+ by (induct xs) (auto simp add: expand_fun_eq)
+
+definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+ "select_weight xs = range (listsum (map fst xs))
+ o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
+
+lemma select_weight_member:
+ assumes "0 < listsum (map fst xs)"
+ shows "fst (select_weight xs s) \<in> set (map snd xs)"
+proof -
+ from range assms
+ have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
+ with pick_member
+ have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
+ then show ?thesis by (simp add: select_weight_def scomp_def split_def)
+qed
+
definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
[code del]: "select_default k x y = range k
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
@@ -140,6 +166,10 @@
end;
*}
+hide (open) type seed
+hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
+ iterate range select pick select_weight select_default
+
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)