### collecting more lemmas concerning multisets

parent f8e89e956d62
 ... ... @@ -226,18 +226,29 @@ lemma poly_x_minus_y_as_comp: "poly_x_minus_y = (\p. p \\<^sub>p x context idom_isom begin sublocale comm_semiring_isom.. end interpretation poly_x_minus_y_hom: factor_preserving_hom "poly_x_minus_y :: 'a :: idom poly \ 'a poly poly" proof- interpret x_y_hom: bijective "\p :: 'a poly poly. p \\<^sub>p x_y" proof (unfold bijective_eq_bij, rule id_imp_bij) fix p :: "'a poly poly" show "p \\<^sub>p x_y \\<^sub>p x_y = p" apply (induct p,simp) apply(unfold x_y_def hom_distribs pcompose_pCons) by (simp) proof - have \p \\<^sub>p x_y \\<^sub>p x_y = p\ for p :: \'a poly poly\ proof (induction p) case 0 show ?case by simp next case (pCons a p) then show ?case by (unfold x_y_def hom_distribs pcompose_pCons) simp qed interpret x_y_hom: idom_isom "\p :: 'a poly poly. p \\<^sub>p x_y" by (unfold_locales, auto) show "factor_preserving_hom (poly_x_minus_y :: 'a poly \ _)" by (unfold poly_x_minus_y_as_comp, rule factor_preserving_hom_comp, unfold_locales) then interpret x_y_hom: bijective "\p :: 'a poly poly. p \\<^sub>p x_y" by (unfold bijective_eq_bij) (rule involuntory_imp_bij) interpret x_y_hom: idom_isom "\p :: 'a poly poly. p \\<^sub>p x_y" by standard simp_all have \factor_preserving_hom (\p :: 'a poly poly. p \\<^sub>p x_y)\ and \factor_preserving_hom (poly_lift :: 'a poly \ 'a poly poly)\ .. then show "factor_preserving_hom (poly_x_minus_y :: 'a poly \ _)" by (unfold poly_x_minus_y_as_comp) (rule factor_preserving_hom_comp) qed text \ ... ...
 theory Missing_Multiset2 imports "HOL-Combinatorics.Permutations" Containers.Containers_Auxiliary (* only for a lemma *) theory More_Missing_Multiset imports "HOL-Combinatorics.Permutations" Polynomial_Factorization.Missing_Multiset begin subsubsection \Missing muiltiset\ lemma id_imp_bij: assumes id: "\x. f (f x) = x" shows "bij f" proof (intro bijI injI surjI[of f, OF id]) fix x y assume "f x = f y" then have "f (f x) = f (f y)" by auto with id show "x = y" by auto qed lemma rel_mset_Zero_iff[simp]: shows "rel_mset rel {#} Y \ Y = {#}" and "rel_mset rel X {#} \ X = {#}" using rel_mset_Zero rel_mset_size by (fastforce, fastforce) definition "is_mset_set X \ \x \# X. count X x = 1" lemma is_mset_setD[dest]: "is_mset_set X \ x \# X \ count X x = 1" unfolding is_mset_set_def by auto lemma is_mset_setI[intro]: assumes "\x. x \# X \ count X x = 1" shows "is_mset_set X" using assms unfolding is_mset_set_def by auto lemma is_mset_set[simp]: "is_mset_set (mset_set X)" unfolding is_mset_set_def by (meson count_mset_set(1) count_mset_set(2) count_mset_set(3) not_in_iff) lemma is_mset_set_add[simp]: "is_mset_set (X + {#x#}) \ is_mset_set X \ x \# X" (is "?L \ ?R") proof(intro iffI conjI) assume L: ?L with count_eq_zero_iff count_single show "is_mset_set X" unfolding is_mset_set_def by (metis (no_types, hide_lams) add_mset_add_single count_add_mset nat.inject set_mset_add_mset_insert union_single_eq_member) show "x \# X" proof assume "x \# X" then have "count (X + {#x#}) x > 1" by auto with L show False by (auto simp: is_mset_set_def) qed next assume R: ?R show ?L proof fix x' assume x': "x' \# X + {#x#}" show "count (X + {#x#}) x' = 1" proof(cases "x' \# X") case True with R have "count X x' = 1" by auto moreover from True R have "count {#x#} x' = 0" by auto ultimately show ?thesis by auto next case False then have "count X x' = 0" by (simp add: not_in_iff) with R x' show ?thesis by auto qed qed lemma rel_mset_free: assumes rel: "rel_mset rel X Y" and xs: "mset xs = X" shows "\ys. mset ys = Y \ list_all2 rel xs ys" proof- from rel[unfolded rel_mset_def] obtain xs' ys' where xs': "mset xs' = X" and ys': "mset ys' = Y" and xsys': "list_all2 rel xs' ys'" by auto from xs' xs have "mset xs = mset xs'" by auto from mset_eq_permutation[OF this] obtain f where perm: "f permutes {..i. i < length xs \ xs ! i = xs' ! f i" by auto note [simp] = list_all2_lengthD[OF xsys',symmetric] note [simp] = atLeast0LessThan[symmetric] note bij = permutes_bij[OF perm] define ys where "ys \ map (nth ys' \ f) [0..x | x \# X \ y = f x. count X x)" proof(induct X) case empty show ?case by auto next case (add x X) define X' where "X' \ X + {#x#}" have "(\z | z \# X' \ y = f z. count (X + {#x#}) z) = (\z | z \# X' \ y = f z. count X z) + (\z | z \# X' \ y = f z. count {#x#} z)" unfolding plus_multiset.rep_eq sum.distrib.. also have split: "{z. z \# X' \ y = f z} = {z. z \# X' \ y = f z \ z \ x} \ {z. z \# X' \ y = f z \ z = x}" by blast then have "(\z | z \# X' \ y = f z. count {#x#} z) = (\z | z \# X' \ y = f z \ z = x. count {#x#} z)" unfolding split by (subst sum.union_disjoint, auto) also have "... = (if y = f x then 1 else 0)" using card_eq_Suc_0_ex1 by (auto simp: X'_def) also have "(\z | z \# X' \ y = f z. count X z) = (\z | z \# X \ y = f z. count X z)" proof(cases "x \# X") case True then have "z \# X' \ z \# X" for z by (auto simp: X'_def) then show ?thesis by auto next case False have split: "{z. z \# X' \ y = f z} = {z. z \# X \ y = f z} \ {z. z = x \ y = f z}" by (auto simp: X'_def) also have "sum (count X) ... = (\z | z \# X \ y = f z. count X z) + (\z | z = x \ y = f z. count X z)" by (subst sum.union_disjoint, auto simp: False) also with False have "\z. z = x \ y = f z \ count X z = 0" by (meson count_inI) with sum.neutral_const have "(\z | z = x \ y = f z. count X z) = 0" by auto finally show ?thesis by auto qed also have "... = count (image_mset f X) y" using add by auto finally show ?case by (simp add: X'_def) lemma rel_mset_split: assumes rel: "rel_mset rel (X1+X2) Y" shows "\Y1 Y2. Y = Y1 + Y2 \ rel_mset rel X1 Y1 \ rel_mset rel X2 Y2" proof- obtain xs1 where xs1: "mset xs1 = X1" using ex_mset by auto obtain xs2 where xs2: "mset xs2 = X2" using ex_mset by auto from xs1 xs2 have "mset (xs1 @ xs2) = X1 + X2" by auto from rel_mset_free[OF rel this] obtain ys where ys: "mset ys = Y" "list_all2 rel (xs1 @ xs2) ys" by auto then obtain ys1 ys2 where ys12: "ys = ys1 @ ys2" and xs1ys1: "list_all2 rel xs1 ys1" and xs2ys2: "list_all2 rel xs2 ys2" using list_all2_append1 by blast from ys12 ys have "Y = mset ys1 + mset ys2" by auto moreover from xs1 xs1ys1 have "rel_mset rel X1 (mset ys1)" unfolding rel_mset_def by auto moreover from xs2 xs2ys2 have "rel_mset rel X2 (mset ys2)" unfolding rel_mset_def by auto ultimately show ?thesis by (subst exI[of _ "mset ys1"], subst exI[of _ "mset ys2"],auto) qed lemma is_mset_set_image: assumes "inj_on f (set_mset X)" and "is_mset_set X" shows "is_mset_set (image_mset f X)" proof (cases X) case empty then show ?thesis by auto next case (add x X) define X' where "X' \ add_mset x X" with assms add have inj:"inj_on f (set_mset X')" and X': "is_mset_set X'" by auto show ?thesis proof(unfold add, intro is_mset_setI, fold X'_def) fix y assume "y \# image_mset f X'" then have "y \ f ` set_mset X'" by auto with inj have "\!x'. x' \# X' \ y = f x'" by (meson imageE inj_onD) then obtain x' where x': "{x'. x' \# X' \ y = f x'} = {x'}" by auto then have "count (image_mset f X') y = count X' x'" unfolding count_image_mset by auto also from X' x' have "... = 1" by auto finally show "count (image_mset f X') y = 1". qed lemma rel_mset_OO: assumes AB: "rel_mset R A B" and BC: "rel_mset S B C" shows "rel_mset (R OO S) A C" proof- from AB obtain as bs where A_as: "A = mset as" and B_bs: "B = mset bs" and as_bs: "list_all2 R as bs" by (auto simp: rel_mset_def) from rel_mset_free[OF BC] B_bs obtain cs where C_cs: "C = mset cs" and bs_cs: "list_all2 S bs cs" by auto from list_all2_trans[OF _ as_bs bs_cs, of "R OO S"] A_as C_cs show ?thesis by (auto simp: rel_mset_def) qed (* a variant for "right" *) ... ... @@ -197,74 +146,4 @@ next from this show ?case by force qed lemma rel_mset_free: assumes rel: "rel_mset rel X Y" and xs: "mset xs = X" shows "\ys. mset ys = Y \ list_all2 rel xs ys" proof- from rel[unfolded rel_mset_def] obtain xs' ys' where xs': "mset xs' = X" and ys': "mset ys' = Y" and xsys': "list_all2 rel xs' ys'" by auto from xs' xs have "mset xs = mset xs'" by auto from mset_eq_permutation[OF this] obtain f where perm: "f permutes {..i. i < length xs \ xs ! i = xs' ! f i" by auto note [simp] = list_all2_lengthD[OF xsys',symmetric] note [simp] = atLeast0LessThan[symmetric] note bij = permutes_bij[OF perm] define ys where "ys \ map (nth ys' \ f) [0..Y1 Y2. Y = Y1 + Y2 \ rel_mset rel X1 Y1 \ rel_mset rel X2 Y2" proof- obtain xs1 where xs1: "mset xs1 = X1" using ex_mset by auto obtain xs2 where xs2: "mset xs2 = X2" using ex_mset by auto from xs1 xs2 have "mset (xs1 @ xs2) = X1 + X2" by auto from rel_mset_free[OF rel this] obtain ys where ys: "mset ys = Y" "list_all2 rel (xs1 @ xs2) ys" by auto then obtain ys1 ys2 where ys12: "ys = ys1 @ ys2" and xs1ys1: "list_all2 rel xs1 ys1" and xs2ys2: "list_all2 rel xs2 ys2" using list_all2_append1 by blast from ys12 ys have "Y = mset ys1 + mset ys2" by auto moreover from xs1 xs1ys1 have "rel_mset rel X1 (mset ys1)" unfolding rel_mset_def by auto moreover from xs2 xs2ys2 have "rel_mset rel X2 (mset ys2)" unfolding rel_mset_def by auto ultimately show ?thesis by (subst exI[of _ "mset ys1"], subst exI[of _ "mset ys2"],auto) qed lemma rel_mset_OO: assumes AB: "rel_mset R A B" and BC: "rel_mset S B C" shows "rel_mset (R OO S) A C" proof- from AB obtain as bs where A_as: "A = mset as" and B_bs: "B = mset bs" and as_bs: "list_all2 R as bs" by (auto simp: rel_mset_def) from rel_mset_free[OF BC] B_bs obtain cs where C_cs: "C = mset cs" and bs_cs: "list_all2 S bs cs" by auto from list_all2_trans[OF _ as_bs bs_cs, of "R OO S"] A_as C_cs show ?thesis by (auto simp: rel_mset_def) qed end
 ... ... @@ -12,7 +12,7 @@ theory Poly_Mod_Finite_Field Finite_Field Polynomial_Interpolation.Ring_Hom_Poly "HOL-Types_To_Sets.Types_To_Sets" Missing_Multiset2 More_Missing_Multiset Poly_Mod begin ... ...
 ... ... @@ -5,7 +5,7 @@ theory Unique_Factorization "HOL-Combinatorics.Permutations" "HOL-Computational_Algebra.Euclidean_Algorithm" Containers.Containers_Auxiliary (* only for a lemma *) Missing_Multiset2 More_Missing_Multiset "HOL-Algebra.Divisibility" begin ... ...