112 |
112 |
113 lemma select_weight_cons_zero: |
113 lemma select_weight_cons_zero: |
114 "select_weight ((0, x) # xs) = select_weight xs" |
114 "select_weight ((0, x) # xs) = select_weight xs" |
115 by (simp add: select_weight_def) |
115 by (simp add: select_weight_def) |
116 |
116 |
117 lemma select_weigth_drop_zero: |
117 lemma select_weight_drop_zero: |
118 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
118 "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" |
119 proof - |
119 proof - |
120 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |
120 have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" |
121 by (induct xs) auto |
121 by (induct xs) auto |
122 then show ?thesis by (simp only: select_weight_def pick_drop_zero) |
122 then show ?thesis by (simp only: select_weight_def pick_drop_zero) |
123 qed |
123 qed |
124 |
124 |
125 lemma select_weigth_select: |
125 lemma select_weight_select: |
126 assumes "xs \<noteq> []" |
126 assumes "xs \<noteq> []" |
127 shows "select_weight (map (Pair 1) xs) = select xs" |
127 shows "select_weight (map (Pair 1) xs) = select xs" |
128 proof - |
128 proof - |
129 have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" |
129 have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" |
130 using assms by (intro range) simp |
130 using assms by (intro range) simp |