equal
deleted
inserted
replaced
115 have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" . |
115 have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" . |
116 with pick_member |
116 with pick_member |
117 have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" . |
117 have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" . |
118 then show ?thesis by (simp add: select_weight_def scomp_def split_def) |
118 then show ?thesis by (simp add: select_weight_def scomp_def split_def) |
119 qed |
119 qed |
|
120 |
|
121 lemma select_weight_cons_zero: |
|
122 "select_weight ((0, x) # xs) = select_weight xs" |
|
123 by (simp add: select_weight_def) |
120 |
124 |
121 lemma select_weigth_drop_zero: |
125 lemma select_weigth_drop_zero: |
122 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
126 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
123 proof - |
127 proof - |
124 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |
128 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |