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

src/HOL/Library/More_List.thy

changeset 40949 | 1d46d893d682 |

parent 39921 | 45f95e4de831 |

child 40951 | 6c35a88d8f61 |

1.1 --- a/src/HOL/Library/More_List.thy Fri Dec 03 22:08:14 2010 +0100 1.2 +++ b/src/HOL/Library/More_List.thy Fri Dec 03 22:34:20 2010 +0100 1.3 @@ -3,7 +3,7 @@ 1.4 header {* Operations on lists beyond the standard List theory *} 1.5 1.6 theory More_List 1.7 -imports Main 1.8 +imports Main Multiset 1.9 begin 1.10 1.11 hide_const (open) Finite_Set.fold 1.12 @@ -78,10 +78,32 @@ 1.13 "fold g (map f xs) = fold (g o f) xs" 1.14 by (induct xs) simp_all 1.15 1.16 +lemma fold_remove1_split: 1.17 + assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 1.18 + and x: "x \<in> set xs" 1.19 + shows "fold f xs = fold f (remove1 x xs) \<circ> f x" 1.20 + using assms by (induct xs) (auto simp add: o_assoc [symmetric]) 1.21 + 1.22 +lemma fold_multiset_equiv: 1.23 + assumes f: "\<And>x y. x \<in># multiset_of xs \<Longrightarrow> y \<in># multiset_of xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 1.24 + and equiv: "multiset_of xs = multiset_of ys" 1.25 + shows "fold f xs = fold f ys" 1.26 +using f equiv [symmetric] proof (induct xs arbitrary: ys) 1.27 + case Nil then show ?case by simp 1.28 +next 1.29 + case (Cons x xs) 1.30 + have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 1.31 + by (rule Cons.prems(1)) (simp_all add: mem_set_multiset_eq Cons.prems(2)) 1.32 + moreover from Cons.prems have "x \<in> set ys" by (simp add: mem_set_multiset_eq) 1.33 + ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) 1.34 + moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) 1.35 + ultimately show ?case by simp 1.36 +qed 1.37 + 1.38 lemma fold_rev: 1.39 assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" 1.40 shows "fold f (rev xs) = fold f xs" 1.41 - using assms by (induct xs) (simp_all del: o_apply add: fold_commute) 1.42 + by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set) 1.43 1.44 lemma foldr_fold: 1.45 assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"