added lemma select_weight_cons_zero
authorhaftmann
Wed, 27 May 2009 22:11:06 +0200
changeset 31268 3ced22320ceb
parent 31267 4a85a4afc97d
child 31269 dcbe1f9fe2cd
added lemma select_weight_cons_zero
src/HOL/Random.thy
--- 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 -