src/HOL/Random.thy
 changeset 31261 900ebbc35e30 parent 31205 98370b26c2ce child 31268 3ced22320ceb
```     1.1 --- a/src/HOL/Random.thy	Tue May 26 17:29:32 2009 +0200
1.2 +++ b/src/HOL/Random.thy	Tue May 26 17:29:33 2009 +0200
1.3 @@ -119,7 +119,7 @@
1.4  qed
1.5
1.6  lemma select_weigth_drop_zero:
1.7 -  "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
1.8 +  "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
1.9  proof -
1.10    have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
1.11      by (induct xs) auto
1.12 @@ -128,9 +128,9 @@
1.13
1.14  lemma select_weigth_select:
1.15    assumes "xs \<noteq> []"
1.16 -  shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
1.17 +  shows "select_weight (map (Pair 1) xs) = select xs"
1.18  proof -
1.19 -  have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
1.20 +  have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
1.21      using assms by (intro range) simp
1.22    moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
1.23      by (induct xs) simp_all
```