Theory HOL-Library.Multiset_Order

(*  Title:      HOL/Library/Multiset_Order.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
*)

section More Theorems about the Multiset Order

theory Multiset_Order
imports Multiset
begin

subsection Alternative Characterizations

subsubsection The Dershowitz--Manna Ordering

definition multpDM where
  "multpDM r M N 
   (X Y. X  {#}  X ⊆# N  M = (N - X) + Y  (k. k ∈# Y  (a. a ∈# X  r k a)))"

lemma multpDM_imp_multp:
  "multpDM r M N  multp r M N"
proof -
  assume "multpDM r M N"
  then obtain X Y where
    "X  {#}" and "X ⊆# N" and "M = N - X + Y" and "k. k ∈# Y  (a. a ∈# X  r k a)"
    unfolding multpDM_def by blast
  then have "multp r (N - X + Y) (N - X + X)"
    by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
  with M = N - X + Y X ⊆# N show "multp r M N"
    by (metis subset_mset.diff_add)
qed

subsubsection The Huet--Oppen Ordering

definition multpHO where
  "multpHO r M N  M  N  (y. count N y < count M y  (x. r y x  count M x < count N x))"

lemma multp_imp_multpHO:
  assumes "asymp r" and "transp r"
  shows "multp r M N  multpHO r M N"
  unfolding multp_def mult_def
proof (induction rule: trancl_induct)
  case (base P)
  then show ?case
    using asymp r
    by (auto elim!: mult1_lessE simp: count_eq_zero_iff multpHO_def split: if_splits
        dest!: Suc_lessD)
next
  case (step N P)
  from step(3) have "M  N" and
    **: "y. count N y < count M y  (x. r y x  count M x < count N x)"
    by (simp_all add: multpHO_def)
  from step(2) obtain M0 a K where
    *: "P = add_mset a M0" "N = M0 + K" "a ∉# K" "b. b ∈# K  r b a"
    using asymp r by (auto elim: mult1_lessE)
  from M  N ** *(1,2,3) have "M  P"
    using *(4) asymp r
    by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
        count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
  moreover
  { assume "count P a  count M a"
    with a ∉# K have "count N a < count M a" unfolding *(1,2)
      by (auto simp add: not_in_iff)
      with ** obtain z where z: "r a z" "count M z < count N z"
        by blast
      with * have "count N z  count P z"
        using asymp r
        by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
            diff_single_trivial in_diff_count not_le_imp_less)
      with z have "z. r a z  count M z < count P z" by auto
  } note count_a = this
  { fix y
    assume count_y: "count P y < count M y"
    have "x. r y x  count M x < count P x"
    proof (cases "y = a")
      case True
      with count_y count_a show ?thesis by auto
    next
      case False
      show ?thesis
      proof (cases "y ∈# K")
        case True
        with *(4) have "r y a" by simp
        then show ?thesis
          by (cases "count P a  count M a") (auto dest: count_a intro: transp r[THEN transpD])
      next
        case False
        with y  a have "count P y = count N y" unfolding *(1,2)
          by (simp add: not_in_iff)
        with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
        show ?thesis
        proof (cases "z ∈# K")
          case True
          with *(4) have "r z a" by simp
          with z(1) show ?thesis
            by (cases "count P a  count M a") (auto dest!: count_a intro: transp r[THEN transpD])
        next
          case False
          with a ∉# K have "count N z  count P z" unfolding *
            by (auto simp add: not_in_iff)
          with z show ?thesis by auto
        qed
      qed
    qed
  }
  ultimately show ?case unfolding multpHO_def by blast
qed

lemma multpHO_imp_multpDM: "multpHO r M N  multpDM r M N"
unfolding multpDM_def
proof (intro iffI exI conjI)
  assume "multpHO r M N"
  then obtain z where z: "count M z < count N z"
    unfolding multpHO_def by (auto simp: multiset_eq_iff nat_neq_iff)
  define X where "X = N - M"
  define Y where "Y = M - N"
  from z show "X  {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
  from z show "X ⊆# N" unfolding X_def by auto
  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
  show "k. k ∈# Y  (a. a ∈# X  r k a)"
  proof (intro allI impI)
    fix k
    assume "k ∈# Y"
    then have "count N k < count M k" unfolding Y_def
      by (auto simp add: in_diff_count)
    with multpHO r M N obtain a where "r k a" and "count M a < count N a"
      unfolding multpHO_def by blast
    then show "a. a ∈# X  r k a" unfolding X_def
      by (auto simp add: in_diff_count)
  qed
qed

lemma multp_eq_multpDM: "asymp r  transp r  multp r = multpDM r"
  using multpDM_imp_multp multp_imp_multpHO[THEN multpHO_imp_multpDM]
  by blast

lemma multp_eq_multpHO: "asymp r  transp r  multp r = multpHO r"
  using multpHO_imp_multpDM[THEN multpDM_imp_multp] multp_imp_multpHO
  by blast

subsubsection Properties of Preorders

context preorder
begin

lemma order_mult: "class.order
  (λM N. (M, N)  mult {(x, y). x < y}  M = N)
  (λM N. (M, N)  mult {(x, y). x < y})"
  (is "class.order ?le ?less")
proof -
  have irrefl: "M :: 'a multiset. ¬ ?less M M"
  proof
    fix M :: "'a multiset"
    have "trans {(x'::'a, x). x' < x}"
      by (rule transI) (blast intro: less_trans)
    moreover
    assume "(M, M)  mult {(x, y). x < y}"
    ultimately have "I J K. M = I + J  M = I + K
       J  {#}  (kset_mset K. jset_mset J. (k, j)  {(x, y). x < y})"
      by (rule mult_implies_one_step)
    then obtain I J K where "M = I + J" and "M = I + K"
      and "J  {#}" and "(kset_mset K. jset_mset J. (k, j)  {(x, y). x < y})" by blast
    then have aux1: "K  {#}" and aux2: "kset_mset K. jset_mset K. k < j" by auto
    have "finite (set_mset K)" by simp
    moreover note aux2
    ultimately have "set_mset K = {}"
      by (induct rule: finite_induct)
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    with aux1 show False by simp
  qed
  have trans: "K M N :: 'a multiset. ?less K M  ?less M N  ?less K N"
    unfolding mult_def by (blast intro: trancl_trans)
  show "class.order ?le ?less"
    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
qed

text The Dershowitz--Manna ordering:

definition less_multisetDM where
  "less_multisetDM M N 
   (X Y. X  {#}  X ⊆# N  M = (N - X) + Y  (k. k ∈# Y  (a. a ∈# X  k < a)))"


text The Huet--Oppen ordering:

definition less_multisetHO where
  "less_multisetHO M N  M  N  (y. count N y < count M y  (x. y < x  count M x < count N x))"

lemma mult_imp_less_multisetHO:
  "(M, N)  mult {(x, y). x < y}  less_multisetHO M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_imp_multpHO[of "(<)"]
  by (simp add: less_multisetHO_def multpHO_def)

lemma less_multisetDM_imp_mult:
  "less_multisetDM M N  (M, N)  mult {(x, y). x < y}"
  unfolding multp_def[of "(<)", symmetric]
  by (rule multpDM_imp_multp[of "(<)" M N]) (simp add: less_multisetDM_def multpDM_def)

lemma less_multisetHO_imp_less_multisetDM: "less_multisetHO M N  less_multisetDM M N"
  unfolding less_multisetDM_def less_multisetHO_def
  unfolding multpDM_def[symmetric] multpHO_def[symmetric]
  by (rule multpHO_imp_multpDM)

lemma mult_less_multisetDM: "(M, N)  mult {(x, y). x < y}  less_multisetDM M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multpDM[of "(<)", simplified]
  by (simp add: multpDM_def less_multisetDM_def)

lemma mult_less_multisetHO: "(M, N)  mult {(x, y). x < y}  less_multisetHO M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multpHO[of "(<)", simplified]
  by (simp add: multpHO_def less_multisetHO_def)

lemmas multDM = mult_less_multisetDM[unfolded less_multisetDM_def]
lemmas multHO = mult_less_multisetHO[unfolded less_multisetHO_def]

end

lemma less_multiset_less_multisetHO: "M < N  less_multisetHO M N"
  unfolding less_multiset_def multp_def multHO less_multisetHO_def ..

lemma less_multisetDM:
  "M < N  (X Y. X  {#}  X ⊆# N  M = N - X + Y  (k. k ∈# Y  (a. a ∈# X  k < a)))"
  by (rule multDM[folded multp_def less_multiset_def])

lemma less_multisetHO:
  "M < N  M  N  (y. count N y < count M y  (x>y. count M x < count N x))"
  by (rule multHO[folded multp_def less_multiset_def])

lemma subset_eq_imp_le_multiset:
  shows "M ⊆# N  M  N"
  unfolding less_eq_multiset_def less_multisetHO
  by (simp add: less_le_not_le subseteq_mset_def)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_right_total: "M < add_mset x M"
  unfolding less_eq_multiset_def less_multisetHO by simp

lemma less_eq_multiset_empty_left[simp]:
  shows "{#}  M"
  by (simp add: subset_eq_imp_le_multiset)

lemma ex_gt_imp_less_multiset: "(y. y ∈# N  (x. x ∈# M  x < y))  M < N"
  unfolding less_multisetHO
  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)

lemma less_eq_multiset_empty_right[simp]: "M  {#}  ¬ M  {#}"
  by (metis less_eq_multiset_empty_left antisym)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_left[simp]: "M  {#}  {#} < M"
  by (simp add: less_multisetHO)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "¬ M < {#}"
  using subset_mset.le_zero_eq less_multiset_def multp_def less_multisetDM by blast

(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P ⊆# M  N < P  M - P + N < M"
  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)

instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
begin

lemma less_eq_multisetHO:
  "M  N  (y. count N y < count M y  (x. y < x  count M x < count N x))"
  by (auto simp: less_eq_multiset_def less_multisetHO)

instance by standard (auto simp: less_eq_multisetHO)

lemma
  fixes M N :: "'a multiset"
  shows
    less_eq_multiset_plus_left: "N  (M + N)" and
    less_eq_multiset_plus_right: "M  (M + N)"
  by simp_all

lemma
  fixes M N :: "'a multiset"
  shows
    le_multiset_plus_left_nonempty: "M  {#}  N < M + N" and
    le_multiset_plus_right_nonempty: "N  {#}  M < M + N"
    by simp_all

end

lemma all_lt_Max_imp_lt_mset: "N  {#}  (a ∈# M. a < Max (set_mset N))  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  y. count M y < count N y"
  by (meson less_eq_multisetHO less_le_not_le)

lemma subset_imp_less_mset: "A ⊂# B  A < B"
  by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)

lemma image_mset_strict_mono:
  assumes
    mono_f: "x  set_mset M. y  set_mset N. x < y  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  {#}" and y_sub_N: "Y ⊆# N" and M_eq: "M = N - Y + X" and
    ex_y: "x. x ∈# X  (y. y ∈# Y  x < y)"
    using less[unfolded less_multisetDM] by blast

  have x_sub_M: "X ⊆# M"
    using M_eq by simp

  let ?fY = "image_mset f Y"
  let ?fX = "image_mset f X"

  show ?thesis
    unfolding less_multisetDM
  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: "x. x ∈# X  y x ∈# Y  x < y x"
      using ex_y by moura

    show "fx. fx ∈# ?fX  (fy. fy ∈# ?fY  fx < fy)"
    proof (intro allI impI)
      fix fx
      assume "fx ∈# ?fX"
      then obtain x where fx: "fx = f x" and x_in: "x ∈# X"
        by auto
      hence y_in: "y x ∈# Y" and y_gt: "x < y x"
        using y[rule_format, OF x_in] by blast+
      hence "f (y x) ∈# ?fY  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 "fy. fy ∈# ?fY  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: "x  set_mset M. y  set_mset N. x < y  f x < f y" and
    less: "M  N"
  shows "image_mset f M  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#}  (x ∈# M. x < y)" for y :: "'a::linorder"
proof (rule iffI)
  assume M_lt_y: "M < {#y#}"
  show "x ∈# M. x < y"
  proof
    fix x
    assume x_in: "x ∈# M"
    hence M: "M - {#x#} + {#x#} = M"
      by (meson insert_DiffM2)
    hence "¬ {#x#} < {#y#}  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 "¬ {#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: "x ∈# 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  {#y#}  M = {#y#}  (x ∈# M. x < y)" for y :: "'a::linorder"
  by (meson less_eq_multiset_def mset_lt_single_right_iff)


subsection Simprocs

lemma mset_le_add_iff1:
  "j  (i::nat)  (repeat_mset i u + m  repeat_mset j u + n) = (repeat_mset (i-j) u + m  n)"
proof -
  assume "j  i"
  then have "j + (i - j) = i"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

lemma mset_le_add_iff2:
  "i  (j::nat)  (repeat_mset i u + m  repeat_mset j u + n) = (m  repeat_mset (j-i) u + n)"
proof -
  assume "i  j"
  then have "i + (j - i) = j"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

simproc_setup msetless_cancel
  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
   "add_mset a m < n" | "m < add_mset a n" |
   "replicate_mset p a < n" | "m < replicate_mset p a" |
   "repeat_mset p m < n" | "m < repeat_mset p n") =
  fn phi => Cancel_Simprocs.less_cancel

simproc_setup msetle_cancel
  ("(l::'a::preorder multiset) + m  n" | "(l::'a multiset)  m + n" |
   "add_mset a m  n" | "m  add_mset a n" |
   "replicate_mset p a  n" | "m  replicate_mset p a" |
   "repeat_mset p m  n" | "m  repeat_mset p n") =
  fn phi => Cancel_Simprocs.less_eq_cancel


subsection Additional facts and instantiations

lemma ex_gt_count_imp_le_multiset:
  "(y :: 'a :: order. y ∈# M + N  y  x)  count M x < count N x  M < N"
  unfolding less_multisetHO
  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)

lemma mset_lt_single_iff[iff]: "{#x#} < {#y#}  x < y"
  unfolding less_multisetHO by simp

lemma mset_le_single_iff[iff]: "{#x#}  {#y#}  x  y" for x y :: "'a::order"
  unfolding less_eq_multisetHO by force

instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
  by standard (metis less_eq_multisetHO not_less_iff_gr_or_eq)

lemma less_eq_multiset_total:
  fixes M N :: "'a :: linorder multiset"
  shows "¬ M  N  N  M"
  by simp

instantiation multiset :: (wellorder) wellorder
begin

lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
  unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)

instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)

end

instantiation multiset :: (preorder) order_bot
begin

definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"

instance by standard (simp add: bot_multiset_def)

end

instance multiset :: (preorder) no_top
proof standard
  fix x :: "'a multiset"
  obtain a :: 'a where True by simp
  have "x < x + (x + {#a#})"
    by simp
  then show "y. x < y"
    by blast
qed

instance multiset :: (preorder) ordered_cancel_comm_monoid_add
  by standard

instantiation multiset :: (linorder) distrib_lattice
begin

definition inf_multiset :: "'a multiset  'a multiset  'a multiset" where
  "inf_multiset A B = (if A < B then A else B)"

definition sup_multiset :: "'a multiset  'a multiset  '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