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)