--- a/src/HOL/Library/Multiset.thy Sat Apr 22 12:52:16 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Apr 22 12:52:55 2017 +0200
@@ -3783,11 +3783,10 @@
subsection \<open>Size setup\<close>
-lemma multiset_size_o_map:
- "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
-apply (rule ext)
-subgoal for x by (induct x) auto
-done
+lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
+ apply (rule ext)
+ subgoal for x by (induct x) auto
+ done
setup \<open>
BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
@@ -3797,6 +3796,44 @@
@{thms multiset_size_o_map}
\<close>
+subsection \<open>Lemmas about Size\<close>
+
+lemma size_mset_SucE: "size A = Suc n \<Longrightarrow> (\<And>a B. A = {#a#} + B \<Longrightarrow> size B = n \<Longrightarrow> P) \<Longrightarrow> P"
+ by (cases A) (auto simp add: ac_simps)
+
+lemma size_Suc_Diff1: "x \<in># M \<Longrightarrow> Suc (size (M - {#x#})) = size M"
+ using arg_cong[OF insert_DiffM, of _ _ size] by simp
+
+lemma size_Diff_singleton: "x \<in># M \<Longrightarrow> size (M - {#x#}) = size M - 1"
+ by (simp add: size_Suc_Diff1 [symmetric])
+
+lemma size_Diff_singleton_if: "size (A - {#x#}) = (if x \<in># A then size A - 1 else size A)"
+ by (simp add: diff_single_trivial size_Diff_singleton)
+
+lemma size_Un_Int: "size A + size B = size (A \<union># B) + size (A \<inter># B)"
+ by (metis inter_subset_eq_union size_union subset_mset.diff_add union_diff_inter_eq_sup)
+
+lemma size_Un_disjoint: "A \<inter># B = {#} \<Longrightarrow> size (A \<union># B) = size A + size B"
+ using size_Un_Int[of A B] by simp
+
+lemma size_Diff_subset_Int: "size (M - M') = size M - size (M \<inter># M')"
+ by (metis diff_intersect_left_idem size_Diff_submset subset_mset.inf_le1)
+
+lemma diff_size_le_size_Diff: "size (M :: _ multiset) - size M' \<le> size (M - M')"
+ by (simp add: diff_le_mono2 size_Diff_subset_Int size_mset_mono)
+
+lemma size_Diff1_less: "x\<in># M \<Longrightarrow> size (M - {#x#}) < size M"
+ by (rule Suc_less_SucD) (simp add: size_Suc_Diff1)
+
+lemma size_Diff2_less: "x\<in># M \<Longrightarrow> y\<in># M \<Longrightarrow> size (M - {#x#} - {#y#}) < size M"
+ by (metis less_imp_diff_less size_Diff1_less size_Diff_subset_Int)
+
+lemma size_Diff1_le: "size (M - {#x#}) \<le> size M"
+ by (cases "x \<in># M") (simp_all add: size_Diff1_less less_imp_le diff_single_trivial)
+
+lemma size_psubset: "M \<subseteq># M' \<Longrightarrow> size M < size M' \<Longrightarrow> M \<subset># M'"
+ using less_irrefl subset_mset_def by blast
+
hide_const (open) wcount
end
--- a/src/HOL/Library/Multiset_Order.thy Sat Apr 22 12:52:16 2017 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Sat Apr 22 12:52:55 2017 +0200
@@ -9,7 +9,7 @@
imports Multiset
begin
-subsection \<open>Alternative characterizations\<close>
+subsection \<open>Alternative Characterizations\<close>
context preorder
begin
@@ -228,6 +228,95 @@
end
+lemma all_lt_Max_imp_lt_mset: "N \<noteq> {#} \<Longrightarrow> (\<forall>a \<in># M. a < Max (set_mset N)) \<Longrightarrow> M < N"
+ by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff)
+
+lemma lt_imp_ex_count_lt: "M < N \<Longrightarrow> \<exists>y. count M y < count N y"
+ by (meson less_eq_multiset\<^sub>H\<^sub>O less_le_not_le)
+
+lemma subset_imp_less_mset: "A \<subset># B \<Longrightarrow> A < B"
+ by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)
+
+lemma image_mset_strict_mono:
+ assumes
+ mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
+ less: "M < N"
+ shows "image_mset f M < image_mset f N"
+proof -
+ obtain Y X where
+ y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
+ ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
+ using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast
+
+ have x_sub_M: "X \<subseteq># M"
+ using M_eq by simp
+
+ let ?fY = "image_mset f Y"
+ let ?fX = "image_mset f X"
+
+ show ?thesis
+ unfolding less_multiset\<^sub>D\<^sub>M
+ proof (intro exI conjI)
+ show "image_mset f M = image_mset f N - ?fY + ?fX"
+ using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
+ by (metis image_mset_Diff image_mset_union)
+ next
+ obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
+ using ex_y by moura
+
+ show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
+ proof (intro allI impI)
+ fix fx
+ assume "fx \<in># ?fX"
+ then obtain x where fx: "fx = f x" and x_in: "x \<in># X"
+ by auto
+ hence y_in: "y x \<in># Y" and y_gt: "x < y x"
+ using y[rule_format, OF x_in] by blast+
+ hence "f (y x) \<in># ?fY \<and> f x < f (y x)"
+ using mono_f y_sub_N x_sub_M x_in
+ by (metis image_eqI in_image_mset mset_subset_eqD)
+ thus "\<exists>fy. fy \<in># ?fY \<and> fx < fy"
+ unfolding fx by auto
+ qed
+ qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
+qed
+
+lemma image_mset_mono:
+ assumes
+ mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
+ less: "M \<le> N"
+ shows "image_mset f M \<le> image_mset f N"
+ by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)
+
+lemma mset_lt_single_right_iff[simp]: "M < {#y#} \<longleftrightarrow> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
+proof (rule iffI)
+ assume M_lt_y: "M < {#y#}"
+ show "\<forall>x \<in># M. x < y"
+ proof
+ fix x
+ assume x_in: "x \<in># M"
+ hence M: "M - {#x#} + {#x#} = M"
+ by (meson insert_DiffM2)
+ hence "\<not> {#x#} < {#y#} \<Longrightarrow> x < y"
+ using x_in M_lt_y
+ by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans)
+ also have "\<not> {#y#} < M"
+ using M_lt_y mset_le_not_sym by blast
+ ultimately show "x < y"
+ by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE
+ less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert
+ set_mset_eq_empty_iff x_in)
+ qed
+next
+ assume y_max: "\<forall>x \<in># M. x < y"
+ show "M < {#y#}"
+ by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max)
+qed
+
+lemma mset_le_single_right_iff[simp]:
+ "M \<le> {#y#} \<longleftrightarrow> M = {#y#} \<or> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
+ by (meson less_eq_multiset_def mset_lt_single_right_iff)
+
subsection \<open>Simprocs\<close>
@@ -279,7 +368,6 @@
lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
unfolding less_eq_multiset\<^sub>H\<^sub>O by force
-
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
@@ -320,4 +408,18 @@
instance multiset :: (preorder) ordered_cancel_comm_monoid_add
by standard
+instantiation multiset :: (linorder) distrib_lattice
+begin
+
+definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+ "inf_multiset A B = (if A < B then A else B)"
+
+definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+ "sup_multiset A B = (if B > A then B else A)"
+
+instance
+ by intro_classes (auto simp: inf_multiset_def sup_multiset_def)
+
end
+
+end