# HG changeset patch
# User wenzelm
# Date 1492858375 -7200
# Node ID d164c4fc0d2c0f3cde402872ac2bb84151e79117
# Parent  701bb74c5f97ba13263470a964b7582883d5a279# Parent  e957b1f004499d859cba5da826cbf1e0b57c8a3f
merged

diff -r e957b1f00449 -r d164c4fc0d2c src/HOL/Library/Multiset.thy
--- 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
diff -r e957b1f00449 -r d164c4fc0d2c src/HOL/Library/Multiset_Order.thy
--- 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