Theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset

(*
  File:                      Duplicate_Free_Multiset.thy
  Authors and contributors:  Mathias Fleury, Daniela Kaufmann, JKU;
                             Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
*)

theory Duplicate_Free_Multiset
imports Multiset_More
begin

section ‹Duplicate Free Multisets›

text ‹Duplicate free multisets are isomorphic to finite sets, but it can be useful to reason about
  duplication to speak about intermediate execution steps in the refinements.
›

definition distinct_mset :: "'a multiset ⇒ bool" where
  "distinct_mset S ⟷ (∀a. a ∈# S ⟶ count S a = 1)"

lemma distinct_mset_count_less_1: "distinct_mset S ⟷ (∀a. count S a ≤ 1)"
  using eq_iff nat_le_linear unfolding distinct_mset_def by fastforce

lemma distinct_mset_empty[simp]: "distinct_mset {#}"
  unfolding distinct_mset_def by auto

lemma distinct_mset_singleton: "distinct_mset {#a#}"
  unfolding distinct_mset_def by auto

lemma distinct_mset_union:
  assumes dist: "distinct_mset (A + B)"
  shows "distinct_mset A"
  unfolding distinct_mset_count_less_1
proof (rule allI)
  fix a
  have ‹count A a ≤ count (A + B) a› by auto
  moreover have ‹count (A + B) a ≤ 1›
    using dist unfolding distinct_mset_count_less_1 by auto
  ultimately show ‹count A a ≤ 1›
    by simp
qed

lemma distinct_mset_minus[simp]: "distinct_mset A ⟹ distinct_mset (A - B)"
  by (metis diff_subset_eq_self mset_subset_eq_exists_conv distinct_mset_union)

lemma distinct_mset_rempdups_union_mset:
  assumes "distinct_mset A" and "distinct_mset B"
  shows "A ∪# B = remdups_mset (A + B)"
  using assms nat_le_linear unfolding remdups_mset_def
  by (force simp add: multiset_eq_iff max_def count_mset_set_if distinct_mset_def not_in_iff)

lemma distinct_mset_add_mset[simp]: "distinct_mset (add_mset a L) ⟷ a ∉# L ∧ distinct_mset L"
  unfolding distinct_mset_def
  apply (rule iffI)
   apply (auto split: if_split_asm; fail)[]
  by (auto simp: not_in_iff; fail)

lemma distinct_mset_size_eq_card: "distinct_mset C ⟹ size C = card (set_mset C)"
  by (induction C) auto

lemma distinct_mset_add:
  "distinct_mset (L + L') ⟷ distinct_mset L ∧ distinct_mset L' ∧ L ∩# L' = {#}"
  by (induction L arbitrary: L') auto

lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M ⟹ mset_set (set_mset M) = M"
  by (induction M) auto

lemma distinct_finite_set_mset_subseteq_iff[iff]:
  assumes "distinct_mset M" "finite N"
  shows "set_mset M ⊆ N ⟷ M ⊆# mset_set N"
  by (metis assms distinct_mset_set_mset_ident finite_set_mset msubset_mset_set_iff)

lemma distinct_mem_diff_mset:
  assumes dist: "distinct_mset M" and mem: "x ∈ set_mset (M - N)"
  shows "x ∉ set_mset N"
proof -
  have "count M x = 1"
    using dist mem by (meson distinct_mset_def in_diffD)
  then show ?thesis
    using mem by (metis count_greater_eq_one_iff in_diff_count not_less)
qed

lemma distinct_set_mset_eq:
  assumes "distinct_mset M" "distinct_mset N" "set_mset M = set_mset N"
  shows "M = N"
  using assms distinct_mset_set_mset_ident by fastforce

lemma distinct_mset_union_mset[simp]:
  ‹distinct_mset (D ∪# C) ⟷ distinct_mset D ∧ distinct_mset C›
  unfolding distinct_mset_count_less_1 by force

lemma distinct_mset_inter_mset:
  "distinct_mset C ⟹ distinct_mset (C ∩# D)"
  "distinct_mset D ⟹ distinct_mset (C ∩# D)"
  by (auto simp add: distinct_mset_def min_def count_eq_zero_iff elim!: le_SucE)

lemma distinct_mset_remove1_All: "distinct_mset C ⟹ remove1_mset L C = removeAll_mset L C"
  by (auto simp: multiset_eq_iff distinct_mset_count_less_1)

lemma distinct_mset_size_2: "distinct_mset {#a, b#} ⟷ a ≠ b"
  by auto

lemma distinct_mset_filter: "distinct_mset M ⟹ distinct_mset {# L ∈# M. P L#}"
  by (simp add: distinct_mset_def)

lemma distinct_mset_mset_distinct[simp]: ‹distinct_mset (mset xs) = distinct xs›
  by (induction xs) auto

lemma distinct_image_mset_inj:
  ‹inj_on f (set_mset M) ⟹ distinct_mset (image_mset f M) ⟷ distinct_mset M›
  by (induction M) (auto simp: inj_on_def)

lemma distinct_mset_remdups_mset_id: ‹distinct_mset C ⟹ remdups_mset C = C›
  by (induction C)  auto

lemma distinct_mset_image_mset:
  ‹distinct_mset (image_mset f (mset xs)) ⟷ distinct (map f xs)›
  apply (subst mset_map[symmetric])
  apply (subst distinct_mset_mset_distinct)
  ..

lemma distinct_mset_mono: ‹D' ⊆# D ⟹ distinct_mset D ⟹ distinct_mset D'›
  by (metis distinct_mset_union subset_mset.le_iff_add)

lemma distinct_mset_mono_strict: ‹D' ⊂# D ⟹ distinct_mset D ⟹ distinct_mset D'›
  using distinct_mset_mono by auto

lemma distinct_set_mset_eq_iff:
  assumes ‹distinct_mset M› ‹distinct_mset N›
  shows ‹set_mset M = set_mset N ⟷ M = N›
  using assms distinct_mset_set_mset_ident by fastforce

lemma distinct_mset_union2:
  ‹distinct_mset (A + B) ⟹ distinct_mset B›
  using distinct_mset_union[of B A]
  by (auto simp: ac_simps)

lemma distinct_mset_mset_set: ‹distinct_mset (mset_set A)›
  unfolding distinct_mset_def count_mset_set_if by (auto simp: not_in_iff)

lemma distinct_mset_inter_remdups_mset:
  assumes dist: ‹distinct_mset A›
  shows ‹A ∩# remdups_mset B = A ∩# B›
proof -
  have [simp]: ‹A' ∩# remove1_mset a (remdups_mset Aa) = A' ∩# Aa›
    if
      ‹A' ∩# remdups_mset Aa = A' ∩# Aa› and
      ‹a ∉# A'› and
      ‹a ∈# Aa›
    for A' Aa :: ‹'a multiset› and a
  by (metis insert_DiffM inter_add_right1 set_mset_remdups_mset that)

  show ?thesis
    using dist
    apply (induction A)
    subgoal by auto
     subgoal for a A'
       by (cases ‹a ∈# B›)
         (use multi_member_split[of a ‹B›]  multi_member_split[of a ‹A›] in
           ‹auto simp: mset_set.insert_remove›)
    done
qed

abbreviation (input) is_mset_set :: ‹'a multiset ⇒ bool›
  where ‹is_mset_set ≡ distinct_mset›

lemma is_mset_set_def:
  ‹is_mset_set X ⟷ (∀x ∈# X. count X x = 1)›
  by (auto simp add: distinct_mset_def)

lemma is_mset_setD[dest]: "is_mset_set X ⟹ x ∈# X ⟹ count X x = 1"
  unfolding is_mset_set_def by auto

lemma is_mset_setI[intro]:
  assumes "⋀x. x ∈# X ⟹ count X x = 1"
  shows "is_mset_set X"
  using assms unfolding is_mset_set_def by auto

lemma is_mset_set[simp]: "is_mset_set (mset_set X)"
  by (fact distinct_mset_mset_set)

lemma is_mset_set_add[simp]:
  "is_mset_set (X + {#x#}) ⟷ is_mset_set X ∧ x ∉# X" (is "?L ⟷ ?R")
proof(intro iffI conjI)
  assume L: ?L
  with count_eq_zero_iff count_single show "is_mset_set X"
    unfolding is_mset_set_def
    by (metis (no_types, opaque_lifting) add_mset_add_single count_add_mset nat.inject set_mset_add_mset_insert union_single_eq_member)
  show "x ∉# X"
  proof
    assume "x ∈# X"
    then have "count (X + {#x#}) x > 1" by auto
    with L show False by (auto simp: is_mset_set_def)
  qed
next
  assume R: ?R show ?L
  proof
    fix x' assume x': "x' ∈# X + {#x#}"
    show "count (X + {#x#}) x' = 1"
    proof(cases "x' ∈# X")
      case True with R have "count X x' = 1" by auto
        moreover from True R have "count {#x#} x' = 0" by auto
        ultimately show ?thesis by auto
    next
      case False then have "count X x' = 0" by (simp add: not_in_iff)
        with R x' show ?thesis by auto
    qed
  qed
qed

lemma mset_set_id:
  assumes "is_mset_set X"
  shows "mset_set (set_mset X) = X"
  using assms by (fact distinct_mset_set_mset_ident)

lemma is_mset_set_image:
  assumes "inj_on f (set_mset X)" and "is_mset_set X"
  shows "is_mset_set (image_mset f X)"
proof (cases X)
  case empty then show ?thesis by auto
next
  case (add x X)
    define X' where "X' ≡ add_mset x X"
    with assms add have inj:"inj_on f (set_mset X')"
          and X': "is_mset_set X'" by auto
  show ?thesis
  proof(unfold add, intro is_mset_setI, fold X'_def)
    fix y assume "y ∈# image_mset f X'"
    then have "y ∈ f ` set_mset X'" by auto 
    with inj have "∃!x'. x' ∈# X' ∧ y = f x'" by (meson imageE inj_onD)
    then obtain x' where x': "{x'. x' ∈# X' ∧ y = f x'} = {x'}" by auto
    then have "count (image_mset f X') y = count X' x'"
      by (simp add: count_image_mset')
    also from X' x' have "... = 1" by auto
    finally show "count (image_mset f X') y = 1".
  qed
qed

end