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)