equal
deleted
inserted
replaced
1837 subsubsection \<open>Comparing multisets\<close> |
1837 subsubsection \<open>Comparing multisets\<close> |
1838 |
1838 |
1839 lemma (in monoid) fmset_perm_cong: |
1839 lemma (in monoid) fmset_perm_cong: |
1840 assumes prm: "as <~~> bs" |
1840 assumes prm: "as <~~> bs" |
1841 shows "fmset G as = fmset G bs" |
1841 shows "fmset G as = fmset G bs" |
1842 using perm_map[OF prm] |
1842 using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast |
1843 by (simp add: mset_eq_perm fmset_def) |
|
1844 |
1843 |
1845 lemma (in comm_monoid_cancel) eqc_listassoc_cong: |
1844 lemma (in comm_monoid_cancel) eqc_listassoc_cong: |
1846 assumes "as [\<sim>] bs" |
1845 assumes "as [\<sim>] bs" |
1847 and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" |
1846 and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" |
1848 shows "map (assocs G) as = map (assocs G) bs" |
1847 shows "map (assocs G) as = map (assocs G) bs" |
1903 assumes prm: "cas <~~> cbs" |
1902 assumes prm: "cas <~~> cbs" |
1904 and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs" |
1903 and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs" |
1905 shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> |
1904 shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> |
1906 cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" |
1905 cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)" |
1907 apply (rule perm.induct[of cas cbs], rule prm) |
1906 apply (rule perm.induct[of cas cbs], rule prm) |
1908 apply safe apply simp_all |
1907 apply safe apply (simp_all del: mset_map) |
1909 apply (simp add: map_eq_Cons_conv, blast) |
1908 apply (simp add: map_eq_Cons_conv, blast) |
1910 apply force |
1909 apply force |
1911 proof - |
1910 proof - |
1912 fix ys as bs |
1911 fix ys as bs |
1913 assume p1: "map (assocs G) as <~~> ys" |
1912 assume p1: "map (assocs G) as <~~> ys" |
1922 \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)" |
1921 \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)" |
1923 and p3: "map (assocs G) as <~~> map (assocs G) bs" |
1922 and p3: "map (assocs G) as <~~> map (assocs G) bs" |
1924 |
1923 |
1925 from p1 |
1924 from p1 |
1926 have "mset (map (assocs G) as) = mset ys" |
1925 have "mset (map (assocs G) as) = mset ys" |
1927 by (simp add: mset_eq_perm) |
1926 by (simp add: mset_eq_perm del: mset_map) |
1928 hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD) |
1927 hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD) |
1929 |
1928 |
1930 have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast |
1929 have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast |
1931 with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp |
1930 with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp |
1932 hence "\<exists>yy. ys = map (assocs G) yy" |
1931 hence "\<exists>yy. ys = map (assocs G) yy" |
1978 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" |
1977 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" |
1979 shows "essentially_equal G as bs" |
1978 shows "essentially_equal G as bs" |
1980 proof - |
1979 proof - |
1981 from mset |
1980 from mset |
1982 have mpp: "map (assocs G) as <~~> map (assocs G) bs" |
1981 have mpp: "map (assocs G) as <~~> map (assocs G) bs" |
1983 by (simp add: fmset_def mset_eq_perm) |
1982 by (simp add: fmset_def mset_eq_perm del: mset_map) |
1984 |
1983 |
1985 have "\<exists>cas. cas = map (assocs G) as" by simp |
1984 have "\<exists>cas. cas = map (assocs G) as" by simp |
1986 from this obtain cas where cas: "cas = map (assocs G) as" by simp |
1985 from this obtain cas where cas: "cas = map (assocs G) as" by simp |
1987 |
1986 |
1988 have "\<exists>cbs. cbs = map (assocs G) bs" by simp |
1987 have "\<exists>cbs. cbs = map (assocs G) bs" by simp |
2036 |
2035 |
2037 have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs" |
2036 have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs" |
2038 using elems |
2037 using elems |
2039 unfolding Cs |
2038 unfolding Cs |
2040 apply (induct Cs', simp) |
2039 apply (induct Cs', simp) |
2041 proof clarsimp |
2040 proof (clarsimp simp del: mset_map) |
2042 fix a Cs' cs |
2041 fix a Cs' cs |
2043 assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x" |
2042 assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x" |
2044 and csP: "\<forall>x\<in>set cs. P x" |
2043 and csP: "\<forall>x\<in>set cs. P x" |
2045 and mset: "mset (map (assocs G) cs) = mset Cs'" |
2044 and mset: "mset (map (assocs G) cs) = mset Cs'" |
2046 from ih |
2045 from ih |