summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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