author | haftmann |
Wed, 27 May 2009 22:11:06 +0200 | |
changeset 31268 | 3ced22320ceb |
parent 31267 | 4a85a4afc97d |
child 31269 | dcbe1f9fe2cd |
--- a/src/HOL/Random.thy Wed May 27 22:11:05 2009 +0200 +++ b/src/HOL/Random.thy Wed May 27 22:11:06 2009 +0200 @@ -118,6 +118,10 @@ then show ?thesis by (simp add: select_weight_def scomp_def split_def) qed +lemma select_weight_cons_zero: + "select_weight ((0, x) # xs) = select_weight xs" + by (simp add: select_weight_def) + lemma select_weigth_drop_zero: "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" proof -