2718 lemma mset_swap: |
2718 lemma mset_swap: |
2719 "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow> |
2719 "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow> |
2720 mset (ls[j := ls ! i, i := ls ! j]) = mset ls" |
2720 mset (ls[j := ls ! i, i := ls ! j]) = mset ls" |
2721 by (cases "i = j") (simp_all add: mset_update nth_mem_mset) |
2721 by (cases "i = j") (simp_all add: mset_update nth_mem_mset) |
2722 |
2722 |
2723 lemma mset_eq_permutation: |
2723 lemma mset_eq_finite: |
2724 assumes \<open>mset xs = mset ys\<close> |
|
2725 obtains f where |
|
2726 \<open>bij_betw f {..<length xs} {..<length ys}\<close> |
|
2727 \<open>ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> |
|
2728 proof - |
|
2729 from assms have \<open>length ys = length xs\<close> |
|
2730 by (auto dest: mset_eq_length) |
|
2731 from assms have \<open>\<exists>f. f ` {..<length xs} = {..<length xs} \<and> ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> |
|
2732 proof (induction xs arbitrary: ys rule: rev_induct) |
|
2733 case Nil |
|
2734 then show ?case by simp |
|
2735 next |
|
2736 case (snoc x xs) |
|
2737 from snoc.prems have \<open>x \<in> set ys\<close> |
|
2738 by (auto dest: union_single_eq_member) |
|
2739 then obtain zs ws where split: \<open>ys = zs @ x # ws\<close> and \<open>x \<notin> set zs\<close> |
|
2740 by (auto dest: split_list_first) |
|
2741 then have \<open>remove1 x ys = zs @ ws\<close> |
|
2742 by (simp add: remove1_append) |
|
2743 moreover from snoc.prems [symmetric] have \<open>mset xs = mset (remove1 x ys)\<close> |
|
2744 by simp |
|
2745 ultimately have \<open>mset xs = mset (zs @ ws)\<close> |
|
2746 by simp |
|
2747 then have \<open>\<exists>f. f ` {..<length xs} = {..<length xs} \<and> zs @ ws = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> |
|
2748 by (rule snoc.IH) |
|
2749 then obtain f where |
|
2750 raw_surj: \<open>f ` {..<length xs} = {..<length xs}\<close> |
|
2751 and hyp: \<open>zs @ ws = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> by blast |
|
2752 define l and k where \<open>l = length zs\<close> and \<open>k = length ws\<close> |
|
2753 then have [simp]: \<open>length zs = l\<close> \<open>length ws = k\<close> |
|
2754 by simp_all |
|
2755 from \<open>mset xs = mset (zs @ ws)\<close> have \<open>length xs = length (zs @ ws)\<close> |
|
2756 by (rule mset_eq_length) |
|
2757 then have [simp]: \<open>length xs = l + k\<close> |
|
2758 by simp |
|
2759 from raw_surj have f_surj: \<open>f ` {..<l + k} = {..<l + k}\<close> |
|
2760 by simp |
|
2761 have [simp]: \<open>[0..<l + k] = [0..<l] @ [l..<l + k]\<close> |
|
2762 by (rule nth_equalityI) (simp_all add: nth_append) |
|
2763 have [simp]: \<open>[l..<l + k] @ [l + k] = [l] @ [Suc l..<Suc (l + k)]\<close> |
|
2764 by (rule nth_equalityI) |
|
2765 (auto simp add: nth_append nth_Cons split: nat.split) |
|
2766 define g :: \<open>nat \<Rightarrow> nat\<close> |
|
2767 where \<open>g n = (if n < l then f n |
|
2768 else if n = l then l + k |
|
2769 else f (n - 1))\<close> for n |
|
2770 have \<open>{..<Suc (l + k)} = {..<l} \<union> {l} \<union> {Suc l..<Suc (l + k)}\<close> |
|
2771 by auto |
|
2772 then have \<open>g ` {..<Suc (l + k)} = g ` {..<l} \<union> {g l} \<union> g ` {Suc l..<Suc (l + k)}\<close> |
|
2773 by auto |
|
2774 also have \<open>g ` {Suc l..<Suc (l + k)} = f ` {l..<l + k}\<close> |
|
2775 apply (auto simp add: g_def Suc_le_lessD) |
|
2776 apply (auto simp add: image_def) |
|
2777 apply (metis Suc_le_mono atLeastLessThan_iff diff_Suc_Suc diff_zero lessI less_trans_Suc) |
|
2778 done |
|
2779 finally have \<open>g ` {..<Suc (l + k)} = f ` {..<l} \<union> {l + k} \<union> f ` {l..<l + k}\<close> |
|
2780 by (simp add: g_def) |
|
2781 also have \<open>\<dots> = {..<Suc (l + k)}\<close> |
|
2782 by simp (metis atLeastLessThan_add_Un f_surj image_Un le_add1 le_add_same_cancel1 lessThan_Suc lessThan_atLeast0) |
|
2783 finally have g_surj: \<open>g ` {..<Suc (l + k)} = {..<Suc (l + k)}\<close> . |
|
2784 from hyp have zs_f: \<open>zs = map (\<lambda>n. xs ! f n) [0..<l]\<close> |
|
2785 and ws_f: \<open>ws = map (\<lambda>n. xs ! f n) [l..<l + k]\<close> |
|
2786 by simp_all |
|
2787 have \<open>zs = map (\<lambda>n. (xs @ [x]) ! g n) [0..<l]\<close> |
|
2788 proof (rule sym, rule map_upt_eqI) |
|
2789 fix n |
|
2790 assume \<open>n < length zs\<close> |
|
2791 then have \<open>n < l\<close> |
|
2792 by simp |
|
2793 with f_surj have \<open>f n < l + k\<close> |
|
2794 by auto |
|
2795 with \<open>n < l\<close> show \<open>zs ! n = (xs @ [x]) ! g (0 + n)\<close> |
|
2796 by (simp add: zs_f g_def nth_append) |
|
2797 qed simp |
|
2798 moreover have \<open>x = (xs @ [x]) ! g l\<close> |
|
2799 by (simp add: g_def nth_append) |
|
2800 moreover have \<open>ws = map (\<lambda>n. (xs @ [x]) ! g n) [Suc l..<Suc (l + k)]\<close> |
|
2801 proof (rule sym, rule map_upt_eqI) |
|
2802 fix n |
|
2803 assume \<open>n < length ws\<close> |
|
2804 then have \<open>n < k\<close> |
|
2805 by simp |
|
2806 with f_surj have \<open>f (l + n) < l + k\<close> |
|
2807 by auto |
|
2808 with \<open>n < k\<close> show \<open>ws ! n = (xs @ [x]) ! g (Suc l + n)\<close> |
|
2809 by (simp add: ws_f g_def nth_append) |
|
2810 qed simp |
|
2811 ultimately have \<open>zs @ x # ws = map (\<lambda>n. (xs @ [x]) ! g n) [0..<length (xs @ [x])]\<close> |
|
2812 by simp |
|
2813 with g_surj show ?case |
|
2814 by (auto simp add: split) |
|
2815 qed |
|
2816 then obtain f where |
|
2817 surj: \<open>f ` {..<length xs} = {..<length xs}\<close> |
|
2818 and hyp: \<open>ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> by blast |
|
2819 from surj have \<open>bij_betw f {..<length xs} {..<length ys}\<close> |
|
2820 by (simp add: bij_betw_def \<open>length ys = length xs\<close> eq_card_imp_inj_on) |
|
2821 then show thesis |
|
2822 using hyp .. |
|
2823 qed |
|
2824 |
|
2825 proposition mset_eq_finite: |
|
2826 \<open>finite {ys. mset ys = mset xs}\<close> |
2724 \<open>finite {ys. mset ys = mset xs}\<close> |
2827 proof - |
2725 proof - |
2828 have \<open>{ys. mset ys = mset xs} \<subseteq> {ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs}\<close> |
2726 have \<open>{ys. mset ys = mset xs} \<subseteq> {ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs}\<close> |
2829 by (auto simp add: dest: mset_eq_setD mset_eq_length) |
2727 by (auto simp add: dest: mset_eq_setD mset_eq_length) |
2830 moreover have \<open>finite {ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs}\<close> |
2728 moreover have \<open>finite {ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs}\<close> |