Theory Hereditary_Multiset

theory Hereditary_Multiset
imports Multiset_More Nested_Multiset
(*  Title:       Hereditar(il)y (Finite) Multisets
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Hereditar(il)y (Finite) Multisets›

theory Hereditary_Multiset
imports Multiset_More Nested_Multiset
begin


subsection ‹Type Definition›

datatype hmultiset =
  HMSet (hmsetmset: "hmultiset multiset")

lemma hmsetmset_inject[simp]: "hmsetmset A = hmsetmset B ⟷ A = B"
  by (blast intro: hmultiset.expand)

primrec Rep_hmultiset :: "hmultiset ⇒ unit nmultiset" where
  "Rep_hmultiset (HMSet M) = MSet (image_mset Rep_hmultiset M)"

primrec (nonexhaustive) Abs_hmultiset :: "unit nmultiset ⇒ hmultiset" where
  "Abs_hmultiset (MSet M) = HMSet (image_mset Abs_hmultiset M)"

lemma type_definition_hmultiset: "type_definition Rep_hmultiset Abs_hmultiset {X. no_elem X}"
proof (unfold_locales, unfold mem_Collect_eq)
  fix X
  show "no_elem (Rep_hmultiset X)"
    by (induct X) (auto intro!: no_elem.intros)
  show "Abs_hmultiset (Rep_hmultiset X) = X"
    by (induct X) auto
next
  fix Y :: "unit nmultiset"
  assume "no_elem Y"
  thus "Rep_hmultiset (Abs_hmultiset Y) = Y"
    by (induct Y rule: no_elem.induct) auto
qed

setup_lifting type_definition_hmultiset

lemma HMSet_alt: "HMSet = Abs_hmultiset o MSet o image_mset Rep_hmultiset"
  by (auto simp: type_definition.Rep_inverse[OF type_definition_hmultiset])

lemma HMSet_transfer[transfer_rule]: "rel_fun (rel_mset pcr_hmultiset) pcr_hmultiset MSet HMSet"
  unfolding HMSet_alt by (force simp: rel_fun_def multiset.in_rel nmultiset.rel_eq
    pcr_hmultiset_def cr_hmultiset_def
    type_definition.Rep_inverse[OF type_definition_hmultiset] intro!: multiset.map_cong)


subsection ‹Restriction of Dershowitz and Manna's Nested Multiset Order›

instantiation hmultiset :: linorder
begin

lift_definition less_hmultiset :: "hmultiset ⇒ hmultiset ⇒ bool" is "(<)" .
lift_definition less_eq_hmultiset :: "hmultiset ⇒ hmultiset ⇒ bool" is "(≤)" .

instance
  by (intro_classes; transfer) auto

end

lemma less_HMSet_iff_less_multiset_extDM: "HMSet M < HMSet N ⟷ less_multiset_extDM (<) M N"
  unfolding less_multiset_extDM_def
proof (transfer, unfold less_nmultiset.simps less_multiset_extDM_def, safe)
  fix M N :: "unit nmultiset multiset" and X Y
  assume *: "pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "X ≠ {#}"
    "X ⊆# N" "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)"
  then have "X ∈ Collect (pred_mset no_elem)"
    unfolding multiset.pred_set mem_Collect_eq by (metis rev_subsetD set_mset_mono)
  from *(1) have "Y ∈ Collect (pred_mset no_elem)"
    unfolding multiset.pred_set mem_Collect_eq by (metis add_diff_cancel_left' in_diffD)
  show
    "∃X'∈Collect (pred_mset no_elem). ∃Y'∈Collect (pred_mset no_elem).
      X' ≠ {#} ∧ filter_mset no_elem X' ⊆# filter_mset no_elem N ∧ N - X + Y = N - X' + Y' ∧
      (∀k∈Collect no_elem. k ∈# Y' ⟶ (∃a∈Collect no_elem. a ∈# X' ∧ k < a))"
    by (rule bexI[OF _ ‹X ∈ Collect (pred_mset no_elem)›],
        rule bexI[OF _ ‹Y ∈ Collect (pred_mset no_elem)›])
      (insert *; force simp: set_mset_diff multiset.pred_set multiset_filter_mono)
next
  fix M N :: "unit nmultiset multiset" and X Y
  assume *:
    "pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "pred_mset no_elem X" "pred_mset no_elem Y"
    "X ≠ {#}" "filter_mset no_elem X ⊆# filter_mset no_elem N"
    "∀k∈Collect no_elem.  k ∈# Y ⟶ (∃a∈Collect no_elem. a ∈# X ∧ k < a)"
  then have [simp]: "filter_mset no_elem X = X" "filter_mset no_elem N = N"
    unfolding filter_mset_eq_conv by (auto simp: multiset.pred_set)
  show
    "∃X' Y'. X' ≠ {#} ∧ X' ⊆# N ∧  N - X + Y = N - X' + Y' ∧
     (∀k. k ∈# Y' ⟶ (∃a. a ∈# X' ∧ k < a))"
    by (rule exI[of _ X], rule exI[of _ Y]) (insert *; auto simp: multiset.pred_set)
qed

lemma hmsetmset_less[simp]: "hmsetmset M < hmsetmset N ⟷ M < N"
  by (cases M, cases N, simp add: less_multiset_extDM_less less_HMSet_iff_less_multiset_extDM)

lemma hmsetmset_le[simp]: "hmsetmset M ≤ hmsetmset N ⟷ M ≤ N"
  unfolding le_less hmsetmset_less by (metis hmultiset.collapse)

lemma wf_less_hmultiset: "wf {(X :: hmultiset, Y :: hmultiset). X < Y}"
  unfolding wf_eq_minimal by transfer (insert wf_less_nmultiset[unfolded wf_eq_minimal], fast)

instance hmultiset :: wellorder
  using wf_less_hmultiset unfolding wf_def mem_Collect_eq prod.case by intro_classes metis

lemma HMSet_less[simp]: "HMSet M < HMSet N ⟷ M < N"
  by (simp add: less_HMSet_iff_less_multiset_extDM less_multiset_extDM_less)

lemma HMSet_le[simp]: "HMSet M ≤ HMSet N ⟷ M ≤ N"
  by (simp add: hmsetmset_le[symmetric])

lemma mem_imp_less_HMSet: "k ∈# L ⟹ k < HMSet L"
  by (induct k arbitrary: L) (auto intro: ex_gt_imp_less_multiset)

lemma mem_hmsetmset_imp_less: "M ∈# hmsetmset N ⟹ M < N"
  using mem_imp_less_HMSet by force


subsection ‹Disjoint Union and Truncated Difference›

instantiation hmultiset :: cancel_comm_monoid_add
begin

definition zero_hmultiset :: hmultiset where
  "0 = HMSet {#}"

lemma hmsetmset_empty_iff[simp]: "hmsetmset n = {#} ⟷ n = 0"
  unfolding zero_hmultiset_def by (cases n) simp

lemma hmsetmset_0[simp]: "hmsetmset 0 = {#}"
  by simp

lemma
  HMSet_eq_0_iff[simp]: "HMSet m = 0 ⟷ m = {#}" and
  zero_eq_HMSet[simp]: "0 = HMSet m ⟷ m = {#}"
  by (cases m) (auto simp: zero_hmultiset_def)

definition plus_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
  "A + B = HMSet (hmsetmset A + hmsetmset B)"

definition minus_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
  "A - B = HMSet (hmsetmset A - hmsetmset B)"

instance
  by intro_classes (auto simp: zero_hmultiset_def plus_hmultiset_def minus_hmultiset_def)

end

lemma HMSet_plus: "HMSet (A + B) = HMSet A + HMSet B"
  by (simp add: plus_hmultiset_def)

lemma HMSet_diff: "HMSet (A - B) = HMSet A - HMSet B"
  by (simp add: minus_hmultiset_def)

lemma hmsetmset_plus: "hmsetmset (M + N) = hmsetmset M + hmsetmset N"
  by (simp add: plus_hmultiset_def)

lemma hmsetmset_diff: "hmsetmset (M - N) = hmsetmset M - hmsetmset N"
  by (simp add: minus_hmultiset_def)

lemma diff_diff_add_hmset[simp]: "a - b - c = a - (b + c)" for a b c :: hmultiset
  by (fact diff_diff_add)

instance hmultiset :: comm_monoid_diff
  by intro_classes (auto simp: zero_hmultiset_def minus_hmultiset_def)

simproc_setup hmseteq_cancel
  ("(l::hmultiset) + m = n" | "(l::hmultiset) = m + n") =
  ‹fn phi => Cancel_Simprocs.eq_cancel›

simproc_setup hmsetdiff_cancel
  ("((l::hmultiset) + m) - n" | "(l::hmultiset) - (m + n)") =
  ‹fn phi => Cancel_Simprocs.diff_cancel›

simproc_setup hmsetless_cancel
  ("(l::hmultiset) + m < n" | "(l::hmultiset) < m + n") =
  ‹fn phi => Cancel_Simprocs.less_cancel›

simproc_setup hmsetless_eq_cancel
  ("(l::hmultiset) + m ≤ n" | "(l::hmultiset) ≤ m + n") =
  ‹fn phi => Cancel_Simprocs.less_eq_cancel›

instance hmultiset :: ordered_cancel_comm_monoid_add
  by intro_classes (simp del: hmsetmset_less add: plus_hmultiset_def order_le_less
    hmsetmset_less[symmetric] less_multiset_extDM_less)

instance hmultiset :: ordered_ab_semigroup_add_imp_le
  by intro_classes (simp add: plus_hmultiset_def order_le_less less_multiset_extDM_less)

instantiation hmultiset :: order_bot
begin

definition bot_hmultiset :: hmultiset where
  "bot_hmultiset = 0"

instance
proof (intro_classes, unfold bot_hmultiset_def zero_hmultiset_def, transfer, goal_cases bot_least)
  case (bot_least x)
  thus ?case
    by (induct x rule: no_elem.induct) (auto simp: less_eq_nmultiset_def less_multiset_extDM_less)
qed

end

instance hmultiset :: no_top
proof (intro_classes, goal_cases gt_ex)
  case (gt_ex a)
  have "a < a + HMSet {#0#}"
    by (simp add: zero_hmultiset_def)
  thus ?case
    by (rule exI)
qed


lemma le_minus_plus_same_hmset: "m ≤ m - n + n" for m n :: hmultiset
proof (cases m n rule: hmultiset.exhaust[case_product hmultiset.exhaust])
  case (HMSet_HMSet m0 n0)
  note m = this(1) and n = this(2)

  {
    assume "n0 ⊆# m0"
    hence "m0 = m0 - n0 + n0"
      by simp
  }
  moreover
  {
    assume "¬ n0 ⊆# m0"
    hence "m0 ⊂# m0 - n0 + n0"
      by (metis mset_subset_eq_add_right subset_eq_diff_conv subset_mset.dual_order.refl
        subset_mset_def)
    hence "m0 < m0 - n0 + n0"
      by (rule subset_imp_less_mset)
  }
  ultimately show ?thesis
    by (simp (no_asm) add: m n order_le_less plus_hmultiset_def minus_hmultiset_def) blast
qed


subsection ‹Infimum and Supremum›

instantiation hmultiset :: distrib_lattice
begin

definition inf_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
  "inf_hmultiset A B = (if A < B then A else B)"

definition sup_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
  "sup_hmultiset A B = (if B > A then B else A)"

instance
  by intro_classes (auto simp: inf_hmultiset_def sup_hmultiset_def)

end


subsection ‹Inequalities›

lemma zero_le_hmset[simp]: "0 ≤ M" for M :: hmultiset
  by (simp add: order_le_less) (metis hmsetmset_less le_multiset_empty_left hmsetmset_empty_iff)

lemma
  le_add1_hmset: "n ≤ n + m" and
  le_add2_hmset: "n ≤ m + n" for n :: hmultiset
  by simp+

lemma le_zero_eq_hmset[simp]: "M ≤ 0 ⟷ M = 0" for M :: hmultiset
  by (simp add: dual_order.antisym)

lemma not_less_zero_hmset[simp]: "¬ M < 0" for M :: hmultiset
  using not_le zero_le_hmset by blast

lemma not_gr_zero_hmset[simp]: "¬ 0 < M ⟷ M = 0" for M :: hmultiset
  using neqE not_less_zero_hmset by blast

lemma zero_less_iff_neq_zero_hmset: "0 < M ⟷ M ≠ 0" for M :: hmultiset
  using not_gr_zero_hmset by blast

lemma zero_less_HMSet_iff[simp]: "0 < HMSet M ⟷ M ≠ {#}"
  by (simp only: zero_less_iff_neq_zero_hmset HMSet_eq_0_iff)

lemma gr_zeroI_hmset: "(M = 0 ⟹ False) ⟹ 0 < M" for M :: hmultiset
  using not_gr_zero_hmset by blast

lemma gr_implies_not_zero_hmset: "M < N ⟹ N ≠ 0" for M N :: hmultiset
  by auto

lemma add_eq_0_iff_both_eq_0_hmset[simp]: "M + N = 0 ⟷ M = 0 ∧ N = 0" for M N :: hmultiset
  by (intro add_nonneg_eq_0_iff zero_le_hmset)

lemma trans_less_add1_hmset: "i < j ⟹ i < j + m" for i j m :: hmultiset
  by (metis add_increasing2 leD le_less not_gr_zero_hmset)

lemma trans_less_add2_hmset: "i < j ⟹ i < m + j" for i j m :: hmultiset
  by (simp add: add.commute trans_less_add1_hmset)

lemma trans_le_add1_hmset: "i ≤ j ⟹ i ≤ j + m" for i j m :: hmultiset
  by (simp add: add_increasing2)

lemma trans_le_add2_hmset: "i ≤ j ⟹ i ≤ m + j" for i j m :: hmultiset
  by (simp add: add_increasing)

lemma diff_le_self_hmset: "m - n ≤ m" for m n :: hmultiset
  by (metis add.commute add.right_neutral diff_add_zero diff_diff_add_hmset
    le_minus_plus_same_hmset)

end