# HG changeset patch # User haftmann # Date 1349949402 -7200 # Node ID 0cfc1651be256629002839b45a0e5fe9e56230e9 # Parent 0aaed83532e1f4e52ee6967a9990ec7c23c290ad simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets diff -r 0aaed83532e1 -r 0cfc1651be25 NEWS --- a/NEWS Thu Oct 11 00:13:21 2012 +0200 +++ b/NEWS Thu Oct 11 11:56:42 2012 +0200 @@ -62,6 +62,16 @@ *** HOL *** +* Theory "Library/Multiset": + + - Renamed constants + fold_mset ~> Multiset.fold -- for coherence with other fold combinators + + - Renamed facts + fold_mset_commute ~> fold_mset_comm -- for coherence with fold_comm + +INCOMPATIBILITY. + * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. * Class "comm_monoid_diff" formalises properties of bounded diff -r 0aaed83532e1 -r 0cfc1651be25 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Oct 11 00:13:21 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Oct 11 11:56:42 2012 +0200 @@ -657,146 +657,82 @@ subsection {* The fold combinator *} -text {* - The intended behaviour is - @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\ (f x\<^isub>n z)\)"} - if @{text f} is associative-commutative. -*} - -text {* - The graph of @{text "fold_mset"}, @{text "z"}: the start element, - @{text "f"}: folding function, @{text "A"}: the multiset, @{text - "y"}: the result. -*} -inductive - fold_msetG :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" - for f :: "'a \ 'b \ 'b" - and z :: 'b +definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - emptyI [intro]: "fold_msetG f z {#} z" -| insertI [intro]: "fold_msetG f z A y \ fold_msetG f z (A + {#x#}) (f x y)" + "fold f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" -inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x" -inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" - -definition - fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - "fold_mset f z A = (THE x. fold_msetG f z A x)" - -lemma Diff1_fold_msetG: - "fold_msetG f z (A - {#x#}) y \ x \# A \ fold_msetG f z A (f x y)" -apply (frule_tac x = x in fold_msetG.insertI) -apply auto -done - -lemma fold_msetG_nonempty: "\x. fold_msetG f z A x" -apply (induct A) - apply blast -apply clarsimp -apply (drule_tac x = x in fold_msetG.insertI) -apply auto -done - -lemma fold_mset_empty[simp]: "fold_mset f z {#} = z" -unfolding fold_mset_def by blast +lemma fold_mset_empty [simp]: + "fold f s {#} = s" + by (simp add: fold_def) context comp_fun_commute begin -lemma fold_msetG_insertE_aux: - "fold_msetG f z A y \ a \# A \ \y'. y = f a y' \ fold_msetG f z (A - {#a#}) y'" -proof (induct set: fold_msetG) - case (insertI A y x) show ?case - proof (cases "x = a") - assume "x = a" with insertI show ?case by auto +lemma fold_mset_insert: + "fold f s (M + {#x#}) = f x (fold f s M)" +proof - + interpret mset: comp_fun_commute "\y. f y ^^ count M y" + by (fact comp_fun_commute_funpow) + interpret mset_union: comp_fun_commute "\y. f y ^^ count (M + {#x#}) y" + by (fact comp_fun_commute_funpow) + show ?thesis + proof (cases "x \ set_of M") + case False + then have *: "count (M + {#x#}) x = 1" by simp + from False have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s (set_of M) = + Finite_Set.fold (\y. f y ^^ count M y) s (set_of M)" + by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) + with False * show ?thesis + by (simp add: fold_def del: count_union) next - assume "x \ a" - then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'" - using insertI by auto - have "f x y = f a (f x y')" - unfolding y by (rule fun_left_comm) - moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')" - using y' and `x \ a` - by (simp add: diff_union_swap [symmetric] fold_msetG.insertI) - ultimately show ?case by fast + case True + def N \ "set_of M - {x}" + from N_def True have *: "set_of M = insert x N" "x \ N" "finite N" by auto + then have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s N = + Finite_Set.fold (\y. f y ^^ count M y) s N" + by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) + with * show ?thesis by (simp add: fold_def del: count_union) simp qed -qed simp - -lemma fold_msetG_insertE: - assumes "fold_msetG f z (A + {#x#}) v" - obtains y where "v = f x y" and "fold_msetG f z A y" -using assms by (auto dest: fold_msetG_insertE_aux [where a=x]) - -lemma fold_msetG_determ: - "fold_msetG f z A x \ fold_msetG f z A y \ y = x" -proof (induct arbitrary: y set: fold_msetG) - case (insertI A y x v) - from `fold_msetG f z (A + {#x#}) v` - obtain y' where "v = f x y'" and "fold_msetG f z A y'" - by (rule fold_msetG_insertE) - from `fold_msetG f z A y'` have "y' = y" by (rule insertI) - with `v = f x y'` show "v = f x y" by simp -qed fast - -lemma fold_mset_equality: "fold_msetG f z A y \ fold_mset f z A = y" -unfolding fold_mset_def by (blast intro: fold_msetG_determ) - -lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)" -proof - - from fold_msetG_nonempty fold_msetG_determ - have "\!x. fold_msetG f z A x" by (rule ex_ex1I) - then show ?thesis unfolding fold_mset_def by (rule theI') qed -lemma fold_mset_insert: - "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)" -by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset) +corollary fold_mset_single [simp]: + "fold f s {#x#} = f x s" +proof - + have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp + then show ?thesis by simp +qed -lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A" -by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x]) - -lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z" -using fold_mset_insert [of z "{#}"] by simp +lemma fold_mset_fun_comm: + "f x (fold f s M) = fold f (f x s) M" + by (induct M) (simp_all add: fold_mset_insert fun_left_comm) lemma fold_mset_union [simp]: - "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B" -proof (induct A) + "fold f s (M + N) = fold f (fold f s M) N" +proof (induct M) case empty then show ?case by simp next - case (add A x) - have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac) - then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" - by (simp add: fold_mset_insert) - also have "\ = fold_mset f (fold_mset f z (A + {#x#})) B" - by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert) - finally show ?case . + case (add M x) + have "M + {#x#} + N = (M + N) + {#x#}" + by (simp add: add_ac) + with add show ?case by (simp add: fold_mset_insert fold_mset_fun_comm) qed lemma fold_mset_fusion: assumes "comp_fun_commute g" - shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") + shows "(\x y. h (g x y) = f x (h y)) \ h (fold g w A) = fold f (h w) A" (is "PROP ?P") proof - interpret comp_fun_commute g by (fact assms) show "PROP ?P" by (induct A) auto qed -lemma fold_mset_rec: - assumes "a \# A" - shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))" -proof - - from assms obtain A' where "A = A' + {#a#}" - by (blast dest: multi_member_split) - then show ?thesis by simp -qed - end text {* A note on code generation: When defining some function containing a - subterm @{term"fold_mset F"}, code generation is not automatic. When + subterm @{term "fold F"}, code generation is not automatic. When interpreting locale @{text left_commutative} with @{text F}, the - would be code thms for @{const fold_mset} become thms like - @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but + would be code thms for @{const fold} become thms like + @{term "fold F z {#} = z"} where @{text F} is not a pattern but contains defined symbols, i.e.\ is not a code thm. Hence a separate constant with its own code thms needs to be introduced for @{text F}. See the image operator below. @@ -806,7 +742,7 @@ subsection {* Image *} definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where - "image_mset f = fold_mset (op + o single o f) {#}" + "image_mset f = fold (plus o single o f) {#}" interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f proof qed (simp add: add_ac fun_eq_iff) @@ -989,7 +925,7 @@ lemma fold_multiset_equiv: assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" and equiv: "multiset_of xs = multiset_of ys" - shows "fold f xs = fold f ys" + shows "List.fold f xs = List.fold f ys" using f equiv [symmetric] proof (induct xs arbitrary: ys) case Nil then show ?case by simp @@ -999,8 +935,8 @@ have "\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x" by (rule Cons.prems(1)) (simp_all add: *) moreover from * have "x \ set ys" by simp - ultimately have "fold f ys = fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) - moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) + ultimately have "List.fold f ys = List.fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) + moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps) ultimately show ?case by simp qed @@ -1915,5 +1851,7 @@ multiset_postproc *} +hide_const (open) fold + end