Theory Nested_Multiset

(*  Title:       Nested Multisets
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Nested Multisets›

theory Nested_Multiset
imports "HOL-Library.Multiset_Order"
begin

declare multiset.map_comp [simp]
declare multiset.map_cong [cong]


subsection ‹Type Definition›

datatype 'a nmultiset =
  Elem 'a
| MSet "'a nmultiset multiset"

inductive no_elem :: "'a nmultiset ⇒ bool" where
  "(⋀X. X ∈# M ⟹ no_elem X) ⟹ no_elem (MSet M)"

inductive_set sub_nmset :: "('a nmultiset × 'a nmultiset) set" where
  "X ∈# M ⟹ (X, MSet M) ∈ sub_nmset"

lemma wf_sub_nmset[simp]: "wf sub_nmset"
proof (rule wfUNIVI)
  fix P :: "'a nmultiset ⇒ bool" and M :: "'a nmultiset"
  assume IH: "∀M. (∀N. (N, M) ∈ sub_nmset ⟶ P N) ⟶ P M"
  show "P M"
    by (induct M; rule IH[rule_format]) (auto simp: sub_nmset.simps)
qed

primrec depth_nmset :: "'a nmultiset ⇒ nat" (‹|_|›) where
  "|Elem a| = 0"
| "|MSet M| = (let X = set_mset (image_mset depth_nmset M) in if X = {} then 0 else Suc (Max X))"

lemma depth_nmset_MSet: "x ∈# M ⟹ |x| < |MSet M|"
  by (auto simp: less_Suc_eq_le)

declare depth_nmset.simps(2)[simp del]


subsection ‹Dershowitz and Manna's Nested Multiset Order›

text ‹The Dershowitz--Manna extension:›

definition less_multiset_ext⇩D⇩M :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
  "less_multiset_ext⇩D⇩M R M N ⟷
   (∃X Y. X ≠ {#} ∧ X ⊆# N ∧ M = (N - X) + Y ∧ (∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ R k a)))"

lemma less_multiset_ext⇩D⇩M_imp_mult:
  assumes
    N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and less: "less_multiset_ext⇩D⇩M R M N"
  shows "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
proof -
  from less obtain X Y where
    "X ≠ {#}" and "X ⊆# N" and "M = N - X + Y" and "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ R k a)"
    unfolding less_multiset_ext⇩D⇩M_def by blast
  with N_A M_A have "(N - X + Y, N - X + X) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
    by (intro one_step_implies_mult, blast,
      metis (mono_tags, lifting) case_prodI mem_Collect_eq mset_subset_eqD mset_subset_eq_add_right
        subsetCE)
  with ‹M = N - X + Y› ‹X ⊆# N› show "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
    by (simp add: subset_mset.diff_add)
qed

lemma mult_imp_less_multiset_ext⇩D⇩M:
  assumes
    N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and
    trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. R x y ⟶ R y z ⟶ R x z" and
    in_mult: "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
  shows "less_multiset_ext⇩D⇩M R M N"
  using in_mult N_A M_A unfolding mult_def less_multiset_ext⇩D⇩M_def
proof induct
  case (base N)
  then obtain y M0 X where "N = add_mset y M0" and "M = M0 + X" and "∀a. a ∈# X ⟶ R a y"
    unfolding mult1_def by auto
  thus ?case
    by (auto intro: exI[of _ "{#y#}"])
next
  case (step N N')
  note N_N'_in_mult1 = this(2) and ih = this(3) and N'_A = this(4) and M_A = this(5)

  have N_A: "set_mset N ⊆ A"
    using N_N'_in_mult1 N'_A unfolding mult1_def by auto

  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 ∧ R x y)"
    using ih[OF N_A M_A] by blast

  obtain z M0 Ya where N'_eq: "N' = M0 + {#z#}" and N_eq: "N = M0 + Ya" and
    z_gt: "∀y. y ∈# Ya ⟶ y ∈ A ∧ z ∈ A ∧ R y z"
    using N_N'_in_mult1[unfolded mult1_def] by auto

  let ?Za = "Y - Ya + {#z#}"
  let ?Xa = "X + Ya + (Y - Ya) - Y"

  have xa_sub_x_ya: "set_mset ?Xa ⊆ set_mset (X + Ya)"
    by (metis diff_subset_eq_self in_diffD subsetI subset_mset.diff_diff_right)

  have x_A: "set_mset X ⊆ A"
    using M_A M_eq by auto
  have ya_A: "set_mset Ya ⊆ A"
    by (simp add: subsetI z_gt)

  have ex_y': "∃y. y ∈# Y - Ya + {#z#} ∧ R x y" if x_in: "x ∈# X + Ya" for x
  proof (cases "x ∈# X")
    case True
    then obtain y where y_in: "y ∈# Y" and y_gt_x: "R x y"
      using ex_y by blast
    show ?thesis
    proof (cases "y ∈# Ya")
      case False
      hence "y ∈# Y - Ya + {#z#}"
        using y_in count_greater_zero_iff in_diff_count by fastforce
      thus ?thesis
        using y_gt_x by blast
    next
      case True
      hence "y ∈ A" and "z ∈ A" and "R y z"
        using z_gt by blast+
      hence "R x z"
        using trans y_gt_x x_A ya_A x_in by (meson subsetCE union_iff)
      thus ?thesis
        by auto
    qed
  next
    case False
    hence "x ∈# Ya"
      using x_in by auto
    hence "x ∈ A" and "z ∈ A" and "R x z"
      using z_gt by blast+
    thus ?thesis
      by auto
  qed

  show ?case
  proof (rule exI[of _ ?Za], rule exI[of _ ?Xa], intro conjI)
    show "Y - Ya + {#z#} ⊆# N'"
      using mset_subset_eq_mono_add subset_eq_diff_conv y_sub_N N_eq N'_eq
      by (simp add: subset_eq_diff_conv)
  next
    show "M = N' - (Y - Ya + {#z#}) + (X + Ya + (Y - Ya) - Y)"
      unfolding M_eq N_eq N'_eq by (auto simp: multiset_eq_iff)
  next
    show "∀x. x ∈# X + Ya + (Y - Ya) - Y ⟶ (∃y. y ∈# Y - Ya + {#z#} ∧ R x y)"
      using ex_y' xa_sub_x_ya by blast
  qed auto
qed

lemma less_multiset_ext⇩D⇩M_iff_mult:
  assumes
    N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and
    trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. R x y ⟶ R y z ⟶ R x z"
  shows "less_multiset_ext⇩D⇩M R M N ⟷ (M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
  using mult_imp_less_multiset_ext⇩D⇩M[OF assms] less_multiset_ext⇩D⇩M_imp_mult[OF N_A M_A] by blast

instantiation nmultiset :: (preorder) preorder
begin

lemma less_multiset_ext⇩D⇩M_cong[fundef_cong]:
  "(⋀X Y k a. X ≠ {#} ⟹ X ⊆# N ⟹ M = (N - X) + Y ⟹ k ∈# Y ⟹ R k a = S k a) ⟹
  less_multiset_ext⇩D⇩M R M N = less_multiset_ext⇩D⇩M S M N"
  unfolding less_multiset_ext⇩D⇩M_def by metis

function less_nmultiset :: "'a nmultiset ⇒ 'a nmultiset ⇒ bool" where
  "less_nmultiset (Elem a) (Elem b) ⟷ a < b"
| "less_nmultiset (Elem a) (MSet M) ⟷ True"
| "less_nmultiset (MSet M) (Elem a) ⟷ False"
| "less_nmultiset (MSet M) (MSet N) ⟷ less_multiset_ext⇩D⇩M less_nmultiset M N"
  by pat_completeness auto
termination
  by (relation "sub_nmset <*lex*> sub_nmset", fastforce,
    metis sub_nmset.simps in_lex_prod mset_subset_eqD mset_subset_eq_add_right)

lemmas less_nmultiset_induct =
  less_nmultiset.induct[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet]

lemmas less_nmultiset_cases =
  less_nmultiset.cases[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet]

lemma trans_less_nmultiset: "X < Y ⟹ Y < Z ⟹ X < Z" for X Y Z :: "'a nmultiset"
proof (induct "Max {|X|, |Y|, |Z|}" arbitrary: X Y Z
    rule: less_induct)
  case less
  from less(2,3) show ?case
  proof (cases X; cases Y; cases Z)
    fix M N N' :: "'a nmultiset multiset"
    define A where "A = set_mset M ∪ set_mset N ∪ set_mset N'"
    assume XYZ: "X = MSet M" "Y = MSet N" "Z = MSet N'"
    then have trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. x < y ⟶ y < z ⟶ x < z"
      by (auto elim!: less(1)[rotated -1] dest!: depth_nmset_MSet simp add: A_def)
    have "set_mset M ⊆ A" "set_mset N ⊆ A" "set_mset N' ⊆ A"
      unfolding A_def by auto
    with less(2,3) XYZ show "X < Z"
      by (auto simp: less_multiset_ext⇩D⇩M_iff_mult[OF _ _ trans] mult_def)
  qed (auto elim: less_trans)
qed

lemma irrefl_less_nmultiset:
  fixes X :: "'a nmultiset"
  shows "X < X ⟹ False"
proof (induct X)
  case (MSet M)
  from MSet(2) show ?case
  unfolding less_nmultiset.simps less_multiset_ext⇩D⇩M_def
  proof safe
    fix X Y :: "'a nmultiset multiset"
    define XY where "XY = {(x, y). x ∈# X ∧ y ∈# Y ∧ y < x}"
    then have fin: "finite XY" and trans: "trans XY"
      by (auto simp: trans_def intro: trans_less_nmultiset
        finite_subset[OF _ finite_cartesian_product])
    assume "X ≠ {#}" "X ⊆# M" "M = M - X + Y"
    then have "X = Y"
      by (auto simp: mset_subset_eq_exists_conv)
    with MSet(1) ‹X ⊆# M› have "irrefl XY"
      unfolding XY_def by (force dest: mset_subset_eqD simp: irrefl_def)
    with trans have "acyclic XY"
      by (simp add: acyclic_irrefl)
    moreover
    assume "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)"
    with ‹X = Y› ‹X ≠ {#}› have "¬ acyclic XY"
      by (intro notI, elim finite_acyclic_wf[OF fin, elim_format])
        (auto dest!: spec[of _ "set_mset Y"] simp: wf_eq_minimal XY_def)
    ultimately show False by blast
  qed
qed simp

lemma antisym_less_nmultiset:
  fixes X Y :: "'a nmultiset"
  shows "X < Y ⟹ Y < X ⟹ False"
  using trans_less_nmultiset irrefl_less_nmultiset by blast

definition less_eq_nmultiset :: "'a nmultiset ⇒ 'a nmultiset ⇒ bool" where
  "less_eq_nmultiset X Y = (X < Y ∨ X = Y)"

instance
proof (intro_classes, goal_cases less_def refl trans)
  case (less_def x y)
  then show ?case
    unfolding less_eq_nmultiset_def by (metis irrefl_less_nmultiset antisym_less_nmultiset)
next
  case (refl x)
  then show ?case
    unfolding less_eq_nmultiset_def by blast
next
  case (trans x y z)
  then show ?case
    unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset)
qed

lemma less_multiset_ext⇩D⇩M_less: "less_multiset_ext⇩D⇩M (<) = (<)"
  unfolding fun_eq_iff less_multiset_ext⇩D⇩M_def less_multiset⇩D⇩M by blast

end

instantiation nmultiset :: (order) order
begin

instance
proof (intro_classes, goal_cases antisym)
  case (antisym x y)
  then show ?case
    unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset irrefl_less_nmultiset)
qed

end

instantiation nmultiset :: (linorder) linorder
begin

lemma total_less_nmultiset:
  fixes X Y :: "'a nmultiset"
  shows "¬ X < Y ⟹ Y ≠ X ⟹ Y < X"
proof (induct X Y rule: less_nmultiset_induct)
  case (MSet_MSet M N)
  then show ?case
    unfolding nmultiset.inject less_nmultiset.simps less_multiset_ext⇩D⇩M_less less_multiset⇩H⇩O
    by (metis add_diff_cancel_left' count_inI diff_add_zero in_diff_count less_imp_not_less
      mset_subset_eq_multiset_union_diff_commute subset_mset.refl)
qed auto

instance
proof (intro_classes, goal_cases total)
  case (total x y)
  then show ?case
    unfolding less_eq_nmultiset_def by (metis total_less_nmultiset)
qed

end

lemma less_depth_nmset_imp_less_nmultiset: "|X| < |Y| ⟹ X < Y"
proof (induct X Y rule: less_nmultiset_induct)
  case (MSet_MSet M N)
  then show ?case
  proof (cases "M = {#}")
    case False
    with MSet_MSet show ?thesis
      by (auto 0 4 simp: depth_nmset.simps(2) less_multiset_ext⇩D⇩M_def not_le Max_gr_iff
        intro: exI[of _ N] split: if_splits)
  qed (auto simp: depth_nmset.simps(2) less_multiset_ext⇩D⇩M_less split: if_splits)
qed simp_all

lemma less_nmultiset_imp_le_depth_nmset: "X < Y ⟹ |X| ≤ |Y|"
proof (induct X Y rule: less_nmultiset_induct)
  case (MSet_MSet M N)
  then have "M < N" by (simp add: less_multiset_ext⇩D⇩M_less)
  then show ?case
  proof (cases "M = {#}" "N = {#}" rule: bool.exhaust[case_product bool.exhaust])
    case [simp]: False_False
    show ?thesis
    unfolding depth_nmset.simps(2) Let_def False_False Suc_le_mono set_image_mset image_is_empty
      set_mset_eq_empty_iff if_False
    proof (intro iffD2[OF Max_le_iff] ballI iffD2[OF Max_ge_iff]; (elim imageE)?; simp)
      fix X
      assume [simp]: "X ∈# M"
      with MSet_MSet(1)[of N M X, simplified] ‹M < N› show "∃Y∈#N. |X| ≤ |Y|"
        by (meson ex_gt_imp_less_multiset less_asym' less_depth_nmset_imp_less_nmultiset
          not_le_imp_less)
    qed
  qed (auto simp: depth_nmset.simps(2))
qed simp_all

lemma eq_mlex_I:
  fixes f :: "'a ⇒ nat" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "⋀X Y. f X < f Y ⟹ R X Y" and "antisymp R"
  shows "{(X, Y). R X Y} = f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
proof safe
  fix X Y
  assume "R X Y"
  show "(X, Y) ∈ f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
  proof (cases "f X" "f Y" rule: linorder_cases)
    case less
    with ‹R X Y› show ?thesis
      by (elim mlex_less)
  next
    case equal
    with ‹R X Y› show ?thesis
      by (intro mlex_leq) auto
  next
    case greater
    from ‹R X Y› assms(1)[OF greater] ‹antisymp R› greater show ?thesis
      unfolding antisymp_def by auto
  qed
next
  fix X Y
  assume "(X, Y) ∈ f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
  then show "R X Y"
    unfolding mlex_prod_def by (auto simp: assms(1))
qed

instantiation nmultiset :: (wellorder) wellorder
begin

lemma depth_nmset_eq_0[simp]: "|X| = 0 ⟷ (X = MSet {#} ∨ (∃x. X = Elem x))"
  by (cases X; simp add: depth_nmset.simps(2))

lemma depth_nmset_eq_Suc[simp]: "|X| = Suc n ⟷
  (∃N. X = MSet N ∧ (∃Y ∈# N. |Y| = n) ∧ (∀Y ∈# N. |Y| ≤ n))"
  by (cases X; auto simp add: depth_nmset.simps(2) intro!: Max_eqI)
    (metis (no_types, lifting) Max_in finite_imageI finite_set_mset imageE image_is_empty
      set_mset_eq_empty_iff)

lemma wf_less_nmultiset_depth:
  "wf {(X :: 'a nmultiset, Y). |X| = i ∧ |Y| = i ∧ X < Y}"
proof (induct i rule: less_induct)
  case (less i)
  define A :: "'a nmultiset set" where "A = {X. |X| < i}"
  from less have "wf ((depth_nmset :: 'a nmultiset ⇒ nat) <*mlex*>
      (⋃j < i. {(X, Y). |X| = j ∧ |Y| = j ∧ X < Y}))"
    by (intro wf_UN wf_mlex) auto
  then have *: "wf (mult {(X :: 'a nmultiset, Y). X ∈ A ∧ Y ∈ A ∧ X < Y})"
    by (intro wf_mult, elim wf_subset) (force simp: A_def mlex_prod_def not_less_iff_gr_or_eq
      dest!: less_depth_nmset_imp_less_nmultiset)
  show ?case
  proof (cases i)
    case 0
    then show ?thesis
      by (auto simp: inj_on_def intro!: wf_subset[OF
        wf_Un[OF wf_map_prod_image[OF wf, of Elem] wf_UN[of "Elem ` UNIV" "λx. {(x, MSet {#})}"]]])
  next
    case (Suc n)
    then show ?thesis
      by (intro wf_subset[OF wf_map_prod_image[OF *, of MSet]])
        (auto 0 4 simp: map_prod_def image_iff inj_on_def A_def
          dest!: less_multiset_ext⇩D⇩M_imp_mult[of _ A, rotated -1] split: prod.splits)
  qed
qed

lemma wf_less_nmultiset: "wf {(X :: 'a nmultiset, Y :: 'a nmultiset). X < Y}" (is "wf ?R")
proof -
  have "?R = depth_nmset <*mlex*> {(X, Y). |X| = |Y| ∧ X < Y}"
    by (rule eq_mlex_I) (auto simp: antisymp_def less_depth_nmset_imp_less_nmultiset)
  also have "{(X, Y). |X| = |Y| ∧ X < Y} = (⋃i. {(X, Y). |X| = i ∧ |Y| = i ∧ X < Y})"
    by auto
  finally show ?thesis
    by (fastforce intro: wf_mlex wf_Union wf_less_nmultiset_depth)
qed

instance using wf_less_nmultiset unfolding wf_def mem_Collect_eq prod.case by intro_classes metis

end

end