807 with Cons.hyps have "length xs = length (remove1 x ys)" . |
807 with Cons.hyps have "length xs = length (remove1 x ys)" . |
808 with `x \<in> set ys` show ?case |
808 with `x \<in> set ys` show ?case |
809 by (auto simp add: length_remove1 dest: length_pos_if_in_set) |
809 by (auto simp add: length_remove1 dest: length_pos_if_in_set) |
810 qed |
810 qed |
811 |
811 |
812 lemma (in linorder) multiset_of_insort [simp]: |
812 lemma multiset_of_eq_length_filter: |
813 "multiset_of (insort x xs) = {#x#} + multiset_of xs" |
813 assumes "multiset_of xs = multiset_of ys" |
|
814 shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" |
|
815 proof (cases "z \<in># multiset_of xs") |
|
816 case False |
|
817 moreover have "\<not> z \<in># multiset_of ys" using assms False by simp |
|
818 ultimately show ?thesis by (simp add: count_filter) |
|
819 next |
|
820 case True |
|
821 moreover have "z \<in># multiset_of ys" using assms True by simp |
|
822 show ?thesis using assms proof (induct xs arbitrary: ys) |
|
823 case Nil then show ?case by simp |
|
824 next |
|
825 case (Cons x xs) |
|
826 from `multiset_of (x # xs) = multiset_of ys` [symmetric] |
|
827 have *: "multiset_of xs = multiset_of (remove1 x ys)" |
|
828 and "x \<in> set ys" |
|
829 by (auto simp add: mem_set_multiset_eq) |
|
830 from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps) |
|
831 moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv) |
|
832 ultimately show ?case using `x \<in> set ys` |
|
833 by (simp add: filter_remove1) (auto simp add: length_remove1) |
|
834 qed |
|
835 qed |
|
836 |
|
837 context linorder |
|
838 begin |
|
839 |
|
840 lemma multiset_of_insort_key [simp]: |
|
841 "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" |
814 by (induct xs) (simp_all add: ac_simps) |
842 by (induct xs) (simp_all add: ac_simps) |
815 |
843 |
816 lemma (in linorder) multiset_of_sort [simp]: |
844 lemma multiset_of_sort_key [simp]: |
817 "multiset_of (sort xs) = multiset_of xs" |
845 "multiset_of (sort_key k xs) = multiset_of xs" |
818 by (induct xs) (simp_all add: ac_simps) |
846 by (induct xs) (simp_all add: ac_simps) |
819 |
847 |
820 text {* |
848 text {* |
821 This lemma shows which properties suffice to show that a function |
849 This lemma shows which properties suffice to show that a function |
822 @{text "f"} with @{text "f xs = ys"} behaves like sort. |
850 @{text "f"} with @{text "f xs = ys"} behaves like sort. |
823 *} |
851 *} |
824 |
852 |
825 lemma (in linorder) properties_for_sort: |
853 lemma properties_for_sort_key: |
826 "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys" |
854 assumes "multiset_of ys = multiset_of xs" |
827 proof (induct xs arbitrary: ys) |
855 and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs" |
|
856 and "sorted (map f ys)" |
|
857 shows "sort_key f xs = ys" |
|
858 using assms proof (induct xs arbitrary: ys) |
828 case Nil then show ?case by simp |
859 case Nil then show ?case by simp |
829 next |
860 next |
830 case (Cons x xs) |
861 case (Cons x xs) |
831 then have "x \<in> set ys" |
862 from Cons.prems(2) have |
832 by (auto simp add: mem_set_multiset_eq intro!: ccontr) |
863 "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs" |
833 with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case |
864 by (simp add: filter_remove1) |
834 by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) |
865 with Cons.prems have "sort_key f xs = remove1 x ys" |
835 qed |
866 by (auto intro!: Cons.hyps simp add: sorted_map_remove1) |
|
867 moreover from Cons.prems have "x \<in> set ys" |
|
868 by (auto simp add: mem_set_multiset_eq intro!: ccontr) |
|
869 ultimately show ?case using Cons.prems by (simp add: insort_key_remove1) |
|
870 qed |
|
871 |
|
872 lemma properties_for_sort: |
|
873 assumes multiset: "multiset_of ys = multiset_of xs" |
|
874 and "sorted ys" |
|
875 shows "sort xs = ys" |
|
876 proof (rule properties_for_sort_key) |
|
877 from multiset show "multiset_of ys = multiset_of xs" . |
|
878 from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp |
|
879 from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" |
|
880 by (rule multiset_of_eq_length_filter) |
|
881 then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k" |
|
882 by simp |
|
883 then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" |
|
884 by (simp add: replicate_length_filter) |
|
885 qed |
|
886 |
|
887 end |
836 |
888 |
837 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs" |
889 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs" |
838 by (induct xs) (auto intro: order_trans) |
890 by (induct xs) (auto intro: order_trans) |
839 |
891 |
840 lemma multiset_of_update: |
892 lemma multiset_of_update: |