diff r 52d332f8f909 r 5c8fb4fd67e0 src/HOL/Random.thy
 a/src/HOL/Random.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Random.thy Tue May 19 13:57:32 2009 +0200
@@ 3,7 +3,7 @@
header {* A HOL random engine *}
theory Random
imports Code_Index
+imports Code_Index List
begin
notation fcomp (infixl "o>" 60)
@@ 42,9 +42,6 @@
primrec seed_invariant :: "seed \ bool" where
"seed_invariant (v, w) \ 0 < v \ v < 9438322952 \ 0 < w \ True"
lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
 by (cases b) simp_all

definition split_seed :: "seed \ seed \ seed" where
"split_seed s = (let
(v, w) = s;
@@ 98,6 +95,14 @@
"pick (filter (\(k, _). k > 0) xs) = pick xs"
by (induct xs) (auto simp add: expand_fun_eq)
+lemma pick_same:
+ "l < length xs \ Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
+proof (induct xs arbitrary: l)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs) then show ?case by (cases l) simp_all
+qed
+
definition select_weight :: "(index \ 'a) list \ seed \ 'a \ seed" where
"select_weight xs = range (listsum (map fst xs))
o\ (\k. Pair (pick xs k))"
@@ 113,6 +118,27 @@
then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed
+lemma select_weigth_drop_zero:
+ "Random.select_weight (filter (\(k, _). k > 0) xs) = Random.select_weight xs"
+proof 
+ have "listsum (map fst [(k, _)\xs . 0 < k]) = listsum (map fst xs)"
+ by (induct xs) auto
+ then show ?thesis by (simp only: select_weight_def pick_drop_zero)
+qed
+
+lemma select_weigth_select:
+ assumes "xs \ []"
+ shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+proof 
+ have less: "\s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
+ using assms by (intro range) simp
+ moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
+ by (induct xs) simp_all
+ ultimately show ?thesis
+ by (auto simp add: select_weight_def select_def scomp_def split_def
+ expand_fun_eq pick_same [symmetric])
+qed
+
definition select_default :: "index \ 'a \ 'a \ seed \ 'a \ seed" where
[code del]: "select_default k x y = range k
o\ (\l. Pair (if l + 1 < k then x else y))"
@@ 169,7 +195,6 @@
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
hide (open) fact log_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\" 60)