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