Commit ce276ad1 authored by Simon Wimmer's avatar Simon Wimmer
Browse files

Merged

......@@ -226,18 +226,29 @@ lemma poly_x_minus_y_as_comp: "poly_x_minus_y = (\<lambda>p. p \<circ>\<^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 \<Rightarrow> 'a poly poly"
proof-
interpret x_y_hom: bijective "\<lambda>p :: 'a poly poly. p \<circ>\<^sub>p x_y"
proof (unfold bijective_eq_bij, rule id_imp_bij)
fix p :: "'a poly poly" show "p \<circ>\<^sub>p x_y \<circ>\<^sub>p x_y = p"
apply (induct p,simp)
apply(unfold x_y_def hom_distribs pcompose_pCons) by (simp)
proof -
have \<open>p \<circ>\<^sub>p x_y \<circ>\<^sub>p x_y = p\<close> for p :: \<open>'a poly poly\<close>
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 "\<lambda>p :: 'a poly poly. p \<circ>\<^sub>p x_y" by (unfold_locales, auto)
show "factor_preserving_hom (poly_x_minus_y :: 'a poly \<Rightarrow> _)"
by (unfold poly_x_minus_y_as_comp, rule factor_preserving_hom_comp, unfold_locales)
then interpret x_y_hom: bijective "\<lambda>p :: 'a poly poly. p \<circ>\<^sub>p x_y"
by (unfold bijective_eq_bij) (rule involuntory_imp_bij)
interpret x_y_hom: idom_isom "\<lambda>p :: 'a poly poly. p \<circ>\<^sub>p x_y"
by standard simp_all
have \<open>factor_preserving_hom (\<lambda>p :: 'a poly poly. p \<circ>\<^sub>p x_y)\<close>
and \<open>factor_preserving_hom (poly_lift :: 'a poly \<Rightarrow> 'a poly poly)\<close>
..
then show "factor_preserving_hom (poly_x_minus_y :: 'a poly \<Rightarrow> _)"
by (unfold poly_x_minus_y_as_comp) (rule factor_preserving_hom_comp)
qed
text \<open>
......
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 \<open>Missing muiltiset\<close>
lemma id_imp_bij:
assumes id: "\<And>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 \<longleftrightarrow> Y = {#}" and "rel_mset rel X {#} \<longleftrightarrow> X = {#}"
using rel_mset_Zero rel_mset_size by (fastforce, fastforce)
definition "is_mset_set X \<equiv> \<forall>x \<in># X. count X x = 1"
lemma is_mset_setD[dest]: "is_mset_set X \<Longrightarrow> x \<in># X \<Longrightarrow> count X x = 1"
unfolding is_mset_set_def by auto
lemma is_mset_setI[intro]:
assumes "\<And>x. x \<in># X \<Longrightarrow> 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#}) \<longleftrightarrow> is_mset_set X \<and> x \<notin># X" (is "?L \<longleftrightarrow> ?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 \<notin># X"
proof
assume "x \<in># 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' \<in># X + {#x#}"
show "count (X + {#x#}) x' = 1"
proof(cases "x' \<in># 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 "\<exists>ys. mset ys = Y \<and> 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 {..<length xs'}" and xs': "permute_list f xs' = xs".
then have [simp]: "length xs' = length xs" by auto
from permute_list_nth[OF perm, unfolded xs'] have *: "\<And>i. i < length xs \<Longrightarrow> 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 \<equiv> map (nth ys' \<circ> f) [0..<length ys']"
then have [simp]: "length ys = length ys'" by auto
have "mset ys = mset (map (nth ys') (map f [0..<length ys']))"
unfolding ys_def by auto
also have "... = image_mset (nth ys') (image_mset f (mset [0..<length ys']))"
by (simp add: multiset.map_comp)
also have "(mset [0..<length ys']) = mset_set {0..<length ys'}"
by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set sorted_list_of_set_range)
also have "image_mset f (...) = mset_set (f ` {..<length ys'})"
using subset_inj_on[OF bij_is_inj[OF bij]] by (subst image_mset_mset_set, auto)
also have "... = mset [0..<length ys']" using perm by (simp add: permutes_image)
also have "image_mset (nth ys') ... = mset ys'" by(fold mset_map, unfold map_nth, auto)
finally have "mset ys = Y" using ys' by auto
moreover have "list_all2 rel xs ys"
proof(rule list_all2_all_nthI)
fix i assume i: "i < length xs"
with * have "xs ! i = xs' ! f i" by auto
also from i permutes_in_image[OF perm]
have "rel (xs' ! f i) (ys' ! f i)" by (intro list_all2_nthD[OF xsys'], auto)
finally show "rel (xs ! i) (ys ! i)" unfolding ys_def using i by simp
qed simp
ultimately show ?thesis by auto
qed
lemma mset_set_id[simp]:
assumes "is_mset_set X"
shows "mset_set (set_mset X) = X"
using assms unfolding is_mset_set_def
by (metis count_eq_zero_iff count_mset_set(1) count_mset_set(3) finite_set_mset multiset_eqI)
lemma count_image_mset:
shows "count (image_mset f X) y = (\<Sum>x | x \<in># X \<and> y = f x. count X x)"
proof(induct X)
case empty show ?case by auto
next
case (add x X)
define X' where "X' \<equiv> X + {#x#}"
have "(\<Sum>z | z \<in># X' \<and> y = f z. count (X + {#x#}) z) =
(\<Sum>z | z \<in># X' \<and> y = f z. count X z) + (\<Sum>z | z \<in># X' \<and> y = f z. count {#x#} z)"
unfolding plus_multiset.rep_eq sum.distrib..
also have split:
"{z. z \<in># X' \<and> y = f z} =
{z. z \<in># X' \<and> y = f z \<and> z \<noteq> x} \<union> {z. z \<in># X' \<and> y = f z \<and> z = x}" by blast
then have "(\<Sum>z | z \<in># X' \<and> y = f z. count {#x#} z) =
(\<Sum>z | z \<in># X' \<and> y = f z \<and> 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 "(\<Sum>z | z \<in># X' \<and> y = f z. count X z) = (\<Sum>z | z \<in># X \<and> y = f z. count X z)"
proof(cases "x \<in># X")
case True then have "z \<in># X' \<longleftrightarrow> z \<in># X" for z by (auto simp: X'_def)
then show ?thesis by auto
next
case False
have split: "{z. z \<in># X' \<and> y = f z} = {z. z \<in># X \<and> y = f z} \<union> {z. z = x \<and> y = f z}"
by (auto simp: X'_def)
also have "sum (count X) ... = (\<Sum>z | z \<in># X \<and> y = f z. count X z) + (\<Sum>z | z = x \<and> y = f z. count X z)"
by (subst sum.union_disjoint, auto simp: False)
also with False have "\<And>z. z = x \<and> y = f z \<Longrightarrow> count X z = 0" by (meson count_inI)
with sum.neutral_const have "(\<Sum>z | z = x \<and> 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 "\<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> 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' \<equiv> 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 \<in># image_mset f X'"
then have "y \<in> f ` set_mset X'" by auto
with inj have "\<exists>!x'. x' \<in># X' \<and> y = f x'" by (meson imageE inj_onD)
then obtain x' where x': "{x'. x' \<in># X' \<and> 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 "\<exists>ys. mset ys = Y \<and> 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 {..<length xs'}" and xs': "permute_list f xs' = xs".
then have [simp]: "length xs' = length xs" by auto
from permute_list_nth[OF perm, unfolded xs'] have *: "\<And>i. i < length xs \<Longrightarrow> 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 \<equiv> map (nth ys' \<circ> f) [0..<length ys']"
then have [simp]: "length ys = length ys'" by auto
have "mset ys = mset (map (nth ys') (map f [0..<length ys']))"
unfolding ys_def by auto
also have "... = image_mset (nth ys') (image_mset f (mset [0..<length ys']))"
by (simp add: multiset.map_comp)
also have "(mset [0..<length ys']) = mset_set {0..<length ys'}"
by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set sorted_list_of_set_range)
also have "image_mset f (...) = mset_set (f ` {..<length ys'})"
using subset_inj_on[OF bij_is_inj[OF bij]] by (subst image_mset_mset_set, auto)
also have "... = mset [0..<length ys']" using perm by (simp add: permutes_image)
also have "image_mset (nth ys') ... = mset ys'" by(fold mset_map, unfold map_nth, auto)
finally have "mset ys = Y" using ys' by auto
moreover have "list_all2 rel xs ys"
proof(rule list_all2_all_nthI)
fix i assume i: "i < length xs"
with * have "xs ! i = xs' ! f i" by auto
also from i permutes_in_image[OF perm]
have "rel (xs' ! f i) (ys' ! f i)" by (intro list_all2_nthD[OF xsys'], auto)
finally show "rel (xs ! i) (ys ! i)" unfolding ys_def using i by simp
qed simp
ultimately show ?thesis by auto
qed
lemma rel_mset_split:
assumes rel: "rel_mset rel (X1+X2) Y"
shows "\<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> 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
......
(*
File: Duplicate_Free_Multiset.thy
Authors and contributors: Mathias Fleury, Daniela Kaufmann, JKU;
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
*)
theory Duplicate_Free_Multiset
imports Multiset_More
begin
section \<open>Duplicate Free Multisets\<close>
text \<open>Duplicate free multisets are isomorphic to finite sets, but it can be useful to reason about
duplication to speak about intermediate execution steps in the refinements.
\<close>
definition distinct_mset :: "'a multiset \<Rightarrow> bool" where
"distinct_mset S \<longleftrightarrow> (\<forall>a. a \<in># S \<longrightarrow> count S a = 1)"
lemma distinct_mset_count_less_1: "distinct_mset S \<longleftrightarrow> (\<forall>a. count S a \<le> 1)"
using eq_iff nat_le_linear unfolding distinct_mset_def by fastforce
lemma distinct_mset_empty[simp]: "distinct_mset {#}"
unfolding distinct_mset_def by auto
lemma distinct_mset_singleton: "distinct_mset {#a#}"
unfolding distinct_mset_def by auto
lemma distinct_mset_union:
assumes dist: "distinct_mset (A + B)"
shows "distinct_mset A"
unfolding distinct_mset_count_less_1
proof (rule allI)
fix a
have \<open>count A a \<le> count (A + B) a\<close> by auto
moreover have \<open>count (A + B) a \<le> 1\<close>
using dist unfolding distinct_mset_count_less_1 by auto
ultimately show \<open>count A a \<le> 1\<close>
by simp
qed
lemma distinct_mset_minus[simp]: "distinct_mset A \<Longrightarrow> distinct_mset (A - B)"
by (metis diff_subset_eq_self mset_subset_eq_exists_conv distinct_mset_union)
lemma distinct_mset_rempdups_union_mset:
assumes "distinct_mset A" and "distinct_mset B"
shows "A \<union># B = remdups_mset (A + B)"
using assms nat_le_linear unfolding remdups_mset_def
by (force simp add: multiset_eq_iff max_def count_mset_set_if distinct_mset_def not_in_iff)
lemma distinct_mset_add_mset[simp]: "distinct_mset (add_mset a L) \<longleftrightarrow> a \<notin># L \<and> distinct_mset L"
unfolding distinct_mset_def
apply (rule iffI)
apply (auto split: if_split_asm; fail)[]
by (auto simp: not_in_iff; fail)
lemma distinct_mset_size_eq_card: "distinct_mset C \<Longrightarrow> size C = card (set_mset C)"
by (induction C) auto
lemma distinct_mset_add:
"distinct_mset (L + L') \<longleftrightarrow> distinct_mset L \<and> distinct_mset L' \<and> L \<inter># L' = {#}"
by (induction L arbitrary: L') auto
lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M \<Longrightarrow> mset_set (set_mset M) = M"
by (induction M) auto
lemma distinct_finite_set_mset_subseteq_iff[iff]:
assumes "distinct_mset M" "finite N"
shows "set_mset M \<subseteq> N \<longleftrightarrow> M \<subseteq># mset_set N"
by (metis assms distinct_mset_set_mset_ident finite_set_mset msubset_mset_set_iff)
lemma distinct_mem_diff_mset:
assumes dist: "distinct_mset M" and mem: "x \<in> set_mset (M - N)"
shows "x \<notin> set_mset N"
proof -
have "count M x = 1"
using dist mem by (meson distinct_mset_def in_diffD)
then show ?thesis
using mem by (metis count_greater_eq_one_iff in_diff_count not_less)
qed
lemma distinct_set_mset_eq:
assumes "distinct_mset M" "distinct_mset N" "set_mset M = set_mset N"
shows "M = N"
using assms distinct_mset_set_mset_ident by fastforce
lemma distinct_mset_union_mset[simp]:
\<open>distinct_mset (D \<union># C) \<longleftrightarrow> distinct_mset D \<and> distinct_mset C\<close>
unfolding distinct_mset_count_less_1 by force
lemma distinct_mset_inter_mset:
"distinct_mset C \<Longrightarrow> distinct_mset (C \<inter># D)"
"distinct_mset D \<Longrightarrow> distinct_mset (C \<inter># D)"
by (auto simp add: distinct_mset_def min_def count_eq_zero_iff elim!: le_SucE)
lemma distinct_mset_remove1_All: "distinct_mset C \<Longrightarrow> remove1_mset L C = removeAll_mset L C"
by (auto simp: multiset_eq_iff distinct_mset_count_less_1)
lemma distinct_mset_size_2: "distinct_mset {#a, b#} \<longleftrightarrow> a \<noteq> b"
by auto
lemma distinct_mset_filter: "distinct_mset M \<Longrightarrow> distinct_mset {# L \<in># M. P L#}"
by (simp add: distinct_mset_def)
lemma distinct_mset_mset_distinct[simp]: \<open>distinct_mset (mset xs) = distinct xs\<close>
by (induction xs) auto
lemma distinct_image_mset_inj:
\<open>inj_on f (set_mset M) \<Longrightarrow> distinct_mset (image_mset f M) \<longleftrightarrow> distinct_mset M\<close>
by (induction M) (auto simp: inj_on_def)
lemma distinct_mset_remdups_mset_id: \<open>distinct_mset C \<Longrightarrow> remdups_mset C = C\<close>
by (induction C) auto
lemma distinct_mset_image_mset:
\<open>distinct_mset (image_mset f (mset xs)) \<longleftrightarrow> distinct (map f xs)\<close>
apply (subst mset_map[symmetric])
apply (subst distinct_mset_mset_distinct)
..
lemma distinct_mset_mono: \<open>D' \<subseteq># D \<Longrightarrow> distinct_mset D \<Longrightarrow> distinct_mset D'\<close>
by (metis distinct_mset_union subset_mset.le_iff_add)
lemma distinct_mset_mono_strict: \<open>D' \<subset># D \<Longrightarrow> distinct_mset D \<Longrightarrow> distinct_mset D'\<close>
using distinct_mset_mono by auto
lemma distinct_set_mset_eq_iff:
assumes \<open>distinct_mset M\<close> \<open>distinct_mset N\<close>
shows \<open>set_mset M = set_mset N \<longleftrightarrow> M = N\<close>
using assms distinct_mset_set_mset_ident by fastforce
lemma distinct_mset_union2:
\<open>distinct_mset (A + B) \<Longrightarrow> distinct_mset B\<close>
using distinct_mset_union[of B A]
by (auto simp: ac_simps)
lemma distinct_mset_mset_set: \<open>distinct_mset (mset_set A)\<close>
unfolding distinct_mset_def count_mset_set_if by (auto simp: not_in_iff)
lemma distinct_mset_inter_remdups_mset:
assumes dist: \<open>distinct_mset A\<close>
shows \<open>A \<inter># remdups_mset B = A \<inter># B\<close>
proof -
have [simp]: \<open>A' \<inter># remove1_mset a (remdups_mset Aa) = A' \<inter># Aa\<close>
if
\<open>A' \<inter># remdups_mset Aa = A' \<inter># Aa\<close> and
\<open>a \<notin># A'\<close> and
\<open>a \<in># Aa\<close>
for A' Aa :: \<open>'a multiset\<close> and a
by (metis insert_DiffM inter_add_right1 set_mset_remdups_mset that)
show ?thesis
using dist
apply (induction A)
subgoal by auto
subgoal for a A'
by (cases \<open>a \<in># B\<close>)
(use multi_member_split[of a \<open>B\<close>] multi_member_split[of a \<open>A\<close>] in
\<open>auto simp: mset_set.insert_remove\<close>)
done
qed
abbreviation (input) is_mset_set :: \<open>'a multiset \<Rightarrow> bool\<close>
where \<open>is_mset_set \<equiv> distinct_mset\<close>
lemma is_mset_set_def:
\<open>is_mset_set X \<longleftrightarrow> (\<forall>x \<in># X. count X x = 1)\<close>
by (auto simp add: distinct_mset_def)
lemma is_mset_setD[dest]: "is_mset_set X \<Longrightarrow> x \<in># X \<Longrightarrow> count X x = 1"
unfolding is_mset_set_def by auto
lemma is_mset_setI[intro]:
assumes "\<And>x. x \<in># X \<Longrightarrow> 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)"
by (fact distinct_mset_mset_set)
lemma is_mset_set_add[simp]:
"is_mset_set (X + {#x#}) \<longleftrightarrow> is_mset_set X \<and> x \<notin># X" (is "?L \<longleftrightarrow> ?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 \<notin># X"
proof
assume "x \<in># 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' \<in># X + {#x#}"
show "count (X + {#x#}) x' = 1"
proof(cases "x' \<in># 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
qed
lemma mset_set_id:
assumes "is_mset_set X"
shows "mset_set (set_mset X) = X"
using assms by (fact distinct_mset_set_mset_ident)
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' \<equiv> 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 \<in># image_mset f X'"
then have "y \<in> f ` set_mset X'" by auto
with inj have "\<exists>!x'. x' \<in># X' \<and> y = f x'" by (meson imageE inj_onD)
then obtain x' where x': "{x'. x' \<in># X' \<and> y = f x'} = {x'}" by auto
then have "count (image_mset f X') y = count X' x'"
by (simp add: count_image_mset')
also from X' x' have "... = 1" by auto
finally show "count (image_mset f X') y = 1".
qed
qed
end
......@@ -74,6 +74,16 @@ proof (induct xs arbitrary: ys)
qed simp
qed simp
lemma finite_mset_set_inter:
\<open>finite A \<Longrightarrow> finite B \<Longrightarrow> mset_set (A \<inter> B) = mset_set A \<inter># mset_set B\<close>
apply (induction A rule: finite_induct)
subgoal by auto
subgoal for a A
by (cases \<open>a \<in> B\<close>; cases \<open>a \<in># mset_set B\<close>)
(use multi_member_split[of a \<open>mset_set B\<close>] in
\<open>auto simp: mset_set.insert_remove\<close>)
done
subsection \<open>Lemmas about Filter and Image\<close>
......@@ -337,6 +347,37 @@ proof -
by (metis add_less_cancel_right add_mset_add_single diff_single_trivial insert_DiffM2 xM_lt_N)
qed
lemma remove_diff_multiset[simp]: \<open>x13 \<notin># A \<Longrightarrow> A - add_mset x13 B = A - B\<close>
by (metis diff_intersect_left_idem inter_add_right1)
lemma removeAll_notin: \<open>a \<notin># A \<Longrightarrow> removeAll_mset a A = A\<close>
using count_inI by force
lemma mset_drop_upto: \<open>mset (drop a N) = {#N!i. i \<in># mset_set {a..<length N}#}\<close>
proof (induction N arbitrary: a)
case Nil
then show ?case by simp
next
case (Cons c N)
have upt: \<open>{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}\<close>
by auto
then have H: \<open>mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})\<close>
unfolding upt by auto
have mset_case_Suc: \<open>{#case x of 0 \<Rightarrow> c | Suc x \<Rightarrow> N ! x . x \<in># mset_set {Suc a..<Suc b}#} =
{#N ! (x-1) . x \<in># mset_set {Suc a..<Suc b}#}\<close> for a b
by (rule image_mset_cong) (auto split: nat.splits)
have Suc_Suc: \<open>{Suc a..<Suc b} = Suc ` {a..<b}\<close> for a b
by auto
then have mset_set_Suc_Suc: \<open>mset_set {Suc a..<Suc b} = {#Suc n. n \<in># mset_set {a..<b}#}\<close> for a b
unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
have *: \<open>{#N ! (x-Suc 0) . x \<in># mset_set {Suc a..<Suc b}#} = {#N ! x . x \<in># mset_set {a..<b}#}\<close>
for a b
by (auto simp add: mset_set_Suc_Suc)
show ?case
apply (cases a)
using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
qed