# HG changeset patch
# User haftmann
# Date 1242398356 -7200
# Node ID dae7be64d61476f88ab565ae57501031be91e127
# Parent  ced8171602837304b205a20e12857efe0bb42841
hide names in theory Random

diff -r ced817160283 -r dae7be64d614 src/HOL/Extraction/Higman.thy
--- 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;
diff -r ced817160283 -r dae7be64d614 src/HOL/Library/Random.thy
--- 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)