equal
deleted
inserted
replaced
82 "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)" |
82 "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)" |
83 by (induct xs arbitrary: i) (simp_all add: less_natural_def) |
83 by (induct xs arbitrary: i) (simp_all add: less_natural_def) |
84 |
84 |
85 lemma pick_drop_zero: |
85 lemma pick_drop_zero: |
86 "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs" |
86 "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs" |
87 by (induct xs) (auto simp add: fun_eq_iff less_natural_def minus_natural_def) |
87 apply (induct xs) |
|
88 apply (auto simp: fun_eq_iff less_natural.rep_eq split: prod.split) |
|
89 by (metis diff_zero of_nat_0 of_nat_of_natural) |
88 |
90 |
89 lemma pick_same: |
91 lemma pick_same: |
90 "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l" |
92 "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l" |
91 proof (induct xs arbitrary: l) |
93 proof (induct xs arbitrary: l) |
92 case Nil then show ?case by simp |
94 case Nil then show ?case by simp |