src/HOL/Random.thy
changeset 31268 3ced22320ceb
parent 31261 900ebbc35e30
child 31633 ea47e2b63588
     1.1 --- a/src/HOL/Random.thy	Wed May 27 22:11:05 2009 +0200
     1.2 +++ b/src/HOL/Random.thy	Wed May 27 22:11:06 2009 +0200
     1.3 @@ -118,6 +118,10 @@
     1.4    then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
     1.5  qed
     1.6  
     1.7 +lemma select_weight_cons_zero:
     1.8 +  "select_weight ((0, x) # xs) = select_weight xs"
     1.9 +  by (simp add: select_weight_def)
    1.10 +
    1.11  lemma select_weigth_drop_zero:
    1.12    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
    1.13  proof -