src/HOL/Library/Multiset_Order.thy
changeset 65546 7c58f69451b0
parent 65031 52e2c99f3711
child 67020 c32254ab1901
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Fri Apr 21 21:06:02 2017 +0200
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Fri Apr 21 21:30:48 2017 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Multiset
     1.5  begin
     1.6  
     1.7 -subsection \<open>Alternative characterizations\<close>
     1.8 +subsection \<open>Alternative Characterizations\<close>
     1.9  
    1.10  context preorder
    1.11  begin
    1.12 @@ -228,6 +228,95 @@
    1.13  
    1.14  end
    1.15  
    1.16 +lemma all_lt_Max_imp_lt_mset: "N \<noteq> {#} \<Longrightarrow> (\<forall>a \<in># M. a < Max (set_mset N)) \<Longrightarrow> M < N"
    1.17 +  by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff)
    1.18 +
    1.19 +lemma lt_imp_ex_count_lt: "M < N \<Longrightarrow> \<exists>y. count M y < count N y"
    1.20 +  by (meson less_eq_multiset\<^sub>H\<^sub>O less_le_not_le)
    1.21 +
    1.22 +lemma subset_imp_less_mset: "A \<subset># B \<Longrightarrow> A < B"
    1.23 +  by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)
    1.24 +
    1.25 +lemma image_mset_strict_mono:
    1.26 +  assumes
    1.27 +    mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
    1.28 +    less: "M < N"
    1.29 +  shows "image_mset f M < image_mset f N"
    1.30 +proof -
    1.31 +  obtain Y X where
    1.32 +    y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
    1.33 +    ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
    1.34 +    using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast
    1.35 +
    1.36 +  have x_sub_M: "X \<subseteq># M"
    1.37 +    using M_eq by simp
    1.38 +
    1.39 +  let ?fY = "image_mset f Y"
    1.40 +  let ?fX = "image_mset f X"
    1.41 +
    1.42 +  show ?thesis
    1.43 +    unfolding less_multiset\<^sub>D\<^sub>M
    1.44 +  proof (intro exI conjI)
    1.45 +    show "image_mset f M = image_mset f N - ?fY + ?fX"
    1.46 +      using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
    1.47 +      by (metis image_mset_Diff image_mset_union)
    1.48 +  next
    1.49 +    obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
    1.50 +      using ex_y by moura
    1.51 +
    1.52 +    show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
    1.53 +    proof (intro allI impI)
    1.54 +      fix fx
    1.55 +      assume "fx \<in># ?fX"
    1.56 +      then obtain x where fx: "fx = f x" and x_in: "x \<in># X"
    1.57 +        by auto
    1.58 +      hence y_in: "y x \<in># Y" and y_gt: "x < y x"
    1.59 +        using y[rule_format, OF x_in] by blast+
    1.60 +      hence "f (y x) \<in># ?fY \<and> f x < f (y x)"
    1.61 +        using mono_f y_sub_N x_sub_M x_in
    1.62 +        by (metis image_eqI in_image_mset mset_subset_eqD)
    1.63 +      thus "\<exists>fy. fy \<in># ?fY \<and> fx < fy"
    1.64 +        unfolding fx by auto
    1.65 +    qed
    1.66 +  qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
    1.67 +qed
    1.68 +
    1.69 +lemma image_mset_mono:
    1.70 +  assumes
    1.71 +    mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
    1.72 +    less: "M \<le> N"
    1.73 +  shows "image_mset f M \<le> image_mset f N"
    1.74 +  by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)
    1.75 +
    1.76 +lemma mset_lt_single_right_iff[simp]: "M < {#y#} \<longleftrightarrow> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
    1.77 +proof (rule iffI)
    1.78 +  assume M_lt_y: "M < {#y#}"
    1.79 +  show "\<forall>x \<in># M. x < y"
    1.80 +  proof
    1.81 +    fix x
    1.82 +    assume x_in: "x \<in># M"
    1.83 +    hence M: "M - {#x#} + {#x#} = M"
    1.84 +      by (meson insert_DiffM2)
    1.85 +    hence "\<not> {#x#} < {#y#} \<Longrightarrow> x < y"
    1.86 +      using x_in M_lt_y
    1.87 +      by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans)
    1.88 +    also have "\<not> {#y#} < M"
    1.89 +      using M_lt_y mset_le_not_sym by blast
    1.90 +    ultimately show "x < y"
    1.91 +      by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE
    1.92 +        less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert
    1.93 +        set_mset_eq_empty_iff x_in)
    1.94 +  qed
    1.95 +next
    1.96 +  assume y_max: "\<forall>x \<in># M. x < y"
    1.97 +  show "M < {#y#}"
    1.98 +    by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max)
    1.99 +qed
   1.100 +
   1.101 +lemma mset_le_single_right_iff[simp]:
   1.102 +  "M \<le> {#y#} \<longleftrightarrow> M = {#y#} \<or> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
   1.103 +  by (meson less_eq_multiset_def mset_lt_single_right_iff)
   1.104 +
   1.105  
   1.106  subsection \<open>Simprocs\<close>
   1.107  
   1.108 @@ -279,7 +368,6 @@
   1.109  lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
   1.110    unfolding less_eq_multiset\<^sub>H\<^sub>O by force
   1.111  
   1.112 -
   1.113  instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
   1.114    by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
   1.115  
   1.116 @@ -320,4 +408,18 @@
   1.117  instance multiset :: (preorder) ordered_cancel_comm_monoid_add
   1.118    by standard
   1.119  
   1.120 +instantiation multiset :: (linorder) distrib_lattice
   1.121 +begin
   1.122 +
   1.123 +definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   1.124 +  "inf_multiset A B = (if A < B then A else B)"
   1.125 +
   1.126 +definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   1.127 +  "sup_multiset A B = (if B > A then B else A)"
   1.128 +
   1.129 +instance
   1.130 +  by intro_classes (auto simp: inf_multiset_def sup_multiset_def)
   1.131 +
   1.132  end
   1.133 +
   1.134 +end