# HG changeset patch # User haftmann # Date 1291534442 -3600 # Node ID 08939f7b62622f4caf3415d6d01fc0b79ef957f6 # Parent 9e54eb514a4618b49f13114615a1f570b24e377f# Parent 069cd1c1f39b4dc474ba932ee4d4d679cc034b37 merged diff -r 9e54eb514a46 -r 08939f7b6262 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Sat Dec 04 21:26:55 2010 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Sun Dec 05 08:34:02 2010 +0100 @@ -74,16 +74,27 @@ where "rsp_fold f \ (\u v. f u \ f v = f v \ f u)" -primrec - fold_list :: "('a \ 'b \ 'b) \ 'b \ 'a list \ 'b" +lemma rsp_foldI: + "(\u v. f u \ f v = f v \ f u) \ rsp_fold f" + by (simp add: rsp_fold_def) + +lemma rsp_foldE: + assumes "rsp_fold f" + obtains "f u \ f v = f v \ f u" + using assms by (simp add: rsp_fold_def) + +definition + fold_once :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where - "fold_list f z [] = z" -| "fold_list f z (a # xs) = - (if (rsp_fold f) then - if a \ set xs then fold_list f z xs - else f a (fold_list f z xs) - else z)" + "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)" +lemma fold_once_default [simp]: + "\ rsp_fold f \ fold_once f xs = id" + by (simp add: fold_once_def) + +lemma fold_once_fold_remdups: + "rsp_fold f \ fold_once f xs = fold f (remdups xs)" + by (simp add: fold_once_def) section {* Quotient composition lemmas *} @@ -223,36 +234,39 @@ shows "(op = ===> op \ ===> op \) filter filter" by (auto intro!: fun_relI) -lemma member_commute_fold_list: - assumes a: "rsp_fold f" - and b: "x \ set xs" - shows "fold_list f y xs = f x (fold_list f y (removeAll x xs))" - using a b by (induct xs) (auto simp add: rsp_fold_def fun_eq_iff) +lemma remdups_removeAll: (*FIXME move*) + "remdups (removeAll x xs) = remove1 x (remdups xs)" + by (induct xs) auto + +lemma member_commute_fold_once: + assumes "rsp_fold f" + and "x \ set xs" + shows "fold_once f xs = fold_once f (removeAll x xs) \ f x" +proof - + from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \ f x" + by (auto intro!: fold_remove1_split elim: rsp_foldE) + then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll) +qed -lemma fold_list_rsp_pre: - assumes a: "set xs = set ys" - shows "fold_list f z xs = fold_list f z ys" - using a - apply (induct xs arbitrary: ys) - apply (simp) - apply (simp (no_asm_use)) - apply (rule conjI) - apply (rule_tac [!] impI) - apply (rule_tac [!] conjI) - apply (rule_tac [!] impI) - apply (metis insert_absorb) - apply (metis List.insert_def List.set.simps(2) List.set_insert fold_list.simps(2)) - apply (metis Diff_insert_absorb insertI1 member_commute_fold_list set_removeAll) - apply(drule_tac x="removeAll a ys" in meta_spec) - apply(auto) - apply(drule meta_mp) - apply(blast) - by (metis List.set.simps(2) emptyE fold_list.simps(2) in_listsp_conv_set listsp.simps mem_def) +lemma fold_once_set_equiv: + assumes "xs \ ys" + shows "fold_once f xs = fold_once f ys" +proof (cases "rsp_fold f") + case False then show ?thesis by simp +next + case True + then have "\x y. x \ set (remdups xs) \ y \ set (remdups xs) \ f x \ f y = f y \ f x" + by (rule rsp_foldE) + moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" + by (simp add: set_eq_iff_multiset_of_remdups_eq) + ultimately have "fold f (remdups xs) = fold f (remdups ys)" + by (rule fold_multiset_equiv) + with True show ?thesis by (simp add: fold_once_fold_remdups) +qed -lemma fold_list_rsp [quot_respect]: - shows "(op = ===> op = ===> op \ ===> op =) fold_list fold_list" - unfolding fun_rel_def - by(auto intro: fold_list_rsp_pre) +lemma fold_once_rsp [quot_respect]: + shows "(op = ===> op \ ===> op =) fold_once fold_once" + unfolding fun_rel_def by (auto intro: fold_once_set_equiv) lemma concat_rsp_pre: assumes a: "list_all2 op \ x x'" @@ -439,8 +453,8 @@ is "set" quotient_definition - "fold_fset :: ('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" - is fold_list + "fold_fset :: ('a \ 'b \ 'b) \ 'a fset \ 'b \ 'b" + is fold_once quotient_definition "concat_fset :: ('a fset) fset \ 'a fset" @@ -903,15 +917,15 @@ subsection {* filter_fset *} lemma subset_filter_fset: - shows "filter_fset P xs |\| filter_fset Q xs = (\ x. x |\| xs \ P x \ Q x)" - by (descending) (auto) + "filter_fset P xs |\| filter_fset Q xs = (\ x. x |\| xs \ P x \ Q x)" + by descending auto lemma eq_filter_fset: - shows "(filter_fset P xs = filter_fset Q xs) = (\x. x |\| xs \ P x = Q x)" - by (descending) (auto) + "(filter_fset P xs = filter_fset Q xs) = (\x. x |\| xs \ P x = Q x)" + by descending auto lemma psubset_filter_fset: - shows "(\x. x |\| xs \ P x \ Q x) \ (x |\| xs & \ P x & Q x) \ + "(\x. x |\| xs \ P x \ Q x) \ (x |\| xs & \ P x & Q x) \ filter_fset P xs |\| filter_fset Q xs" unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset) @@ -919,16 +933,16 @@ subsection {* fold_fset *} lemma fold_empty_fset: - shows "fold_fset f z {||} = z" - by (descending) (simp) + "fold_fset f {||} = id" + by descending (simp add: fold_once_def) -lemma fold_insert_fset: "fold_fset f z (insert_fset a A) = - (if rsp_fold f then if a |\| A then fold_fset f z A else f a (fold_fset f z A) else z)" - by (descending) (simp) +lemma fold_insert_fset: "fold_fset f (insert_fset a A) = + (if rsp_fold f then if a |\| A then fold_fset f A else fold_fset f A \ f a else id)" + by descending (simp add: fold_once_fold_remdups) lemma in_commute_fold_fset: - "\rsp_fold f; h |\| b\ \ fold_fset f z b = f h (fold_fset f z (remove_fset h b))" - by (descending) (simp add: member_commute_fold_list) + "rsp_fold f \ h |\| b \ fold_fset f b = fold_fset f (remove_fset h b) \ f h" + by descending (simp add: member_commute_fold_once) subsection {* Choice in fsets *}