# 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

"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#}"

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'›

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)›

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)

"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
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
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'"
also from X' x' have "... = 1" by auto
finally show "count (image_mset f X') y = 1".
qed
qed

end
```