summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.thy

changeset 48619 | 558e4e77ce69 |

parent 47841 | 179b5e7c9803 |

child 48828 | 441a4eed7823 |

1.1 --- a/src/HOL/List.thy Thu Jul 26 15:55:19 2012 +0200 1.2 +++ b/src/HOL/List.thy Tue Jul 31 13:55:39 2012 +0200 1.3 @@ -2458,6 +2458,28 @@ 1.4 "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" 1.5 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) 1.6 1.7 +lemma (in ab_semigroup_mult) fold1_distinct_set_fold: 1.8 + assumes "xs \<noteq> []" 1.9 + assumes d: "distinct xs" 1.10 + shows "Finite_Set.fold1 times (set xs) = List.fold times (tl xs) (hd xs)" 1.11 +proof - 1.12 + interpret comp_fun_commute times by (fact comp_fun_commute) 1.13 + from assms obtain y ys where xs: "xs = y # ys" 1.14 + by (cases xs) auto 1.15 + then have *: "y \<notin> set ys" using assms by simp 1.16 + from xs d have **: "remdups ys = ys" by safe (induct ys, auto) 1.17 + show ?thesis 1.18 + proof (cases "set ys = {}") 1.19 + case True with xs show ?thesis by simp 1.20 + next 1.21 + case False 1.22 + then have "fold1 times (Set.insert y (set ys)) = Finite_Set.fold times y (set ys)" 1.23 + by (simp_all add: fold1_eq_fold *) 1.24 + with xs show ?thesis 1.25 + by (simp add: fold_set_fold_remdups **) 1.26 + qed 1.27 +qed 1.28 + 1.29 lemma (in comp_fun_idem) fold_set_fold: 1.30 "Finite_Set.fold f y (set xs) = fold f xs y" 1.31 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)