src/HOL/Random.thy
 changeset 31203 5c8fb4fd67e0 parent 31196 82ff416d7d66 child 31205 98370b26c2ce
```     1.1 --- a/src/HOL/Random.thy	Tue May 19 13:57:31 2009 +0200
1.2 +++ b/src/HOL/Random.thy	Tue May 19 13:57:32 2009 +0200
1.3 @@ -3,7 +3,7 @@
1.4  header {* A HOL random engine *}
1.5
1.6  theory Random
1.7 -imports Code_Index
1.8 +imports Code_Index List
1.9  begin
1.10
1.11  notation fcomp (infixl "o>" 60)
1.12 @@ -42,9 +42,6 @@
1.13  primrec seed_invariant :: "seed \<Rightarrow> bool" where
1.14    "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
1.15
1.16 -lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
1.17 -  by (cases b) simp_all
1.18 -
1.19  definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
1.20    "split_seed s = (let
1.21       (v, w) = s;
1.22 @@ -98,6 +95,14 @@
1.23    "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
1.24    by (induct xs) (auto simp add: expand_fun_eq)
1.25
1.26 +lemma pick_same:
1.27 +  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
1.28 +proof (induct xs arbitrary: l)
1.29 +  case Nil then show ?case by simp
1.30 +next
1.31 +  case (Cons x xs) then show ?case by (cases l) simp_all
1.32 +qed
1.33 +
1.34  definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
1.35    "select_weight xs = range (listsum (map fst xs))
1.36     o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
1.37 @@ -113,6 +118,27 @@
1.38    then show ?thesis by (simp add: select_weight_def scomp_def split_def)
1.39  qed
1.40
1.41 +lemma select_weigth_drop_zero:
1.42 +  "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
1.43 +proof -
1.44 +  have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
1.45 +    by (induct xs) auto
1.46 +  then show ?thesis by (simp only: select_weight_def pick_drop_zero)
1.47 +qed
1.48 +
1.49 +lemma select_weigth_select:
1.50 +  assumes "xs \<noteq> []"
1.51 +  shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
1.52 +proof -
1.53 +  have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
1.54 +    using assms by (intro range) simp
1.55 +  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
1.56 +    by (induct xs) simp_all
1.57 +  ultimately show ?thesis
1.58 +    by (auto simp add: select_weight_def select_def scomp_def split_def
1.59 +      expand_fun_eq pick_same [symmetric])
1.60 +qed
1.61 +
1.62  definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
1.63    [code del]: "select_default k x y = range k
1.64       o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
1.65 @@ -169,7 +195,6 @@
1.66  hide (open) type seed
1.67  hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
1.68    iterate range select pick select_weight select_default
1.69 -hide (open) fact log_def
1.70
1.71  no_notation fcomp (infixl "o>" 60)
1.72  no_notation scomp (infixl "o\<rightarrow>" 60)
```