equal
deleted
inserted
replaced
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
3 |
2 |
4 section \<open>A HOL random engine\<close> |
3 section \<open>A HOL random engine\<close> |
5 |
4 |
6 theory Random |
5 theory Random |
116 |
115 |
117 lemma select_weight_drop_zero: |
116 lemma select_weight_drop_zero: |
118 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
117 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
119 proof - |
118 proof - |
120 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |
119 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |
121 by (induct xs) (auto simp add: less_natural_def, simp add: plus_natural_def) |
120 by (induct xs) (auto simp add: less_natural_def natural_eq_iff) |
122 then show ?thesis by (simp only: select_weight_def pick_drop_zero) |
121 then show ?thesis by (simp only: select_weight_def pick_drop_zero) |
123 qed |
122 qed |
124 |
123 |
125 lemma select_weight_select: |
124 lemma select_weight_select: |
126 assumes "xs \<noteq> []" |
125 assumes "xs \<noteq> []" |