Theory Min_Max_Least_Greatest.Min_Max_Least_Greatest_Multiset
theory Min_Max_Least_Greatest_Multiset
imports
Relation_Reachability
Min_Max_Least_Greatest_Set
"HOL-Library.Multiset"
"HOL-Library.Multiset_Order"
begin
section ‹Minimal and maximal elements›
definition is_minimal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
is_minimal_in_mset_wrt R X = is_minimal_in_set_wrt R (set_mset X)"
definition is_maximal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
is_maximal_in_mset_wrt R X = is_maximal_in_set_wrt R (set_mset X)"
definition is_strictly_minimal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
is_strictly_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {# x #}. ¬ (R⇧=⇧= y x))"
definition is_strictly_maximal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
is_strictly_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {# x #}. ¬ (R⇧=⇧= x y))"
context
fixes X R
assumes
trans: "transp_on (set_mset X) R" and
asym: "asymp_on (set_mset X) R"
begin
subsection ‹Conversions›
lemma is_minimal_in_mset_wrt_iff:
"is_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. y ≠ x ⟶ ¬ R y x)"
using is_minimal_in_set_wrt_iff[OF trans asym]
using is_minimal_in_mset_wrt_def[OF trans asym]
by simp
lemma "is_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. ¬ R y x)"
unfolding is_minimal_in_mset_wrt_iff
proof (rule refl_conj_eq, rule ball_cong)
show "set_mset X = set_mset X" ..
next
show "⋀y. y ∈# X ⟹ (y ≠ x ⟶ ¬ R y x) = (¬ R y x)"
using asym[THEN asymp_onD] by metis
qed
lemma is_maximal_in_mset_wrt_iff:
"is_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. y ≠ x ⟶ ¬ R x y)"
using is_maximal_in_set_wrt_iff[OF trans asym]
using is_maximal_in_mset_wrt_def[OF trans asym]
by simp
lemma "is_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. ¬ R x y)"
unfolding is_maximal_in_mset_wrt_iff
proof (rule refl_conj_eq, rule ball_cong)
show "set_mset X = set_mset X" ..
next
show "⋀y. y ∈# X ⟹ (y ≠ x ⟶ ¬ R x y) = (¬ R x y)"
using asym[THEN asymp_onD] by metis
qed
lemma is_strictly_minimal_in_mset_wrt_iff:
"is_strictly_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X- {# x #}. ¬ R⇧=⇧= y x)"
unfolding is_strictly_minimal_in_mset_wrt_def[OF trans asym]
by(rule refl)
lemma is_strictly_maximal_in_mset_wrt_iff:
"is_strictly_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X- {# x #}. ¬ R⇧=⇧= x y)"
unfolding is_strictly_maximal_in_mset_wrt_def[OF trans asym]
by(rule refl)
lemma is_minimal_in_mset_wrt_if_is_strictly_minimal_in_mset_wrt:
"is_strictly_minimal_in_mset_wrt R X x ⟹ is_minimal_in_mset_wrt R X x"
unfolding is_minimal_in_mset_wrt_iff is_strictly_minimal_in_mset_wrt_iff
using multi_member_split by fastforce
lemma is_maximal_in_mset_wrt_if_is_strictly_maximal_in_mset_wrt:
"is_strictly_maximal_in_mset_wrt R X x ⟹ is_maximal_in_mset_wrt R X x"
unfolding is_maximal_in_mset_wrt_iff is_strictly_maximal_in_mset_wrt_iff
using multi_member_split by fastforce
subsection ‹Existence›
lemma ex_minimal_in_mset_wrt:
"X ≠ {#} ⟹ ∃m. is_minimal_in_mset_wrt R X m"
using trans asym ex_minimal_in_set_wrt[of "set_mset X" R] is_minimal_in_mset_wrt_def
by (metis finite_set_mset set_mset_eq_empty_iff)
lemma ex_maximal_in_mset_wrt:
"X ≠ {#} ⟹ ∃m. is_maximal_in_mset_wrt R X m"
using trans asym ex_maximal_in_set_wrt[of "set_mset X" R] is_maximal_in_mset_wrt_def
by (metis finite_set_mset set_mset_eq_empty_iff)
subsection ‹Miscellaneous›
lemma explode_maximal_in_mset_wrt:
assumes max: "is_maximal_in_mset_wrt R X x"
obtains n :: nat where "replicate_mset (Suc n) x + {#y ∈# X. y ≠ x#} = X"
using max[unfolded is_maximal_in_mset_wrt_iff]
by (metis filter_eq_replicate_mset in_countE multiset_partition)
lemma explode_strictly_maximal_in_mset_wrt:
assumes max: "is_strictly_maximal_in_mset_wrt R X x"
shows "add_mset x {#y ∈# X. y ≠ x#} = X"
proof -
have "x ∈# X" and "∀y ∈# X - {#x#}. x ≠ y"
using max unfolding is_strictly_maximal_in_mset_wrt_iff by simp_all
have "add_mset x (X - {#x#}) = X"
using ‹x ∈# X› by (metis insert_DiffM)
moreover have "{#y ∈# X. y ≠ x#} = X - {#x#}"
using ‹∀y ∈# X - {#x#}. x ≠ y›
by (smt (verit, best) ‹x ∈# X› add_diff_cancel_left' diff_subset_eq_self filter_mset_eq_conv
insert_DiffM2 set_mset_add_mset_insert set_mset_empty singletonD)
ultimately show ?thesis
by (simp only:)
qed
end
lemma is_minimal_in_filter_mset_wrt_iff:
assumes
tran: "transp_on (set_mset (filter_mset P X)) R" and
asym: "asymp_on (set_mset (filter_mset P X)) R"
shows "is_minimal_in_mset_wrt R (filter_mset P X) x ⟷
(x ∈# X ∧ P x ∧ (∀y ∈# X - {#x#}. P y ⟶ ¬ R y x))"
proof -
have "is_minimal_in_mset_wrt R (filter_mset P X) x ⟷
is_minimal_in_set_wrt R ({y ∈ set_mset X. P y}) x"
using is_minimal_in_mset_wrt_iff[OF tran asym]
using is_minimal_in_set_wrt_iff[OF tran asym]
by auto
also have "… ⟷ x ∈# X ∧ P x ∧ (∀y ∈ set_mset X - {x}. P y ⟶ ¬ R y x)"
proof (rule is_minimal_in_set_wrt_filter_iff)
show "transp_on {y. y ∈# X ∧ P y} R"
using tran by simp
next
show "asymp_on {y. y ∈# X ∧ P y} R"
using asym by simp
qed
finally show ?thesis
by (metis (no_types, lifting) DiffD1 asym asymp_onD at_most_one_mset_mset_diff insertE
insert_Diff is_minimal_in_mset_wrt_iff more_than_one_mset_mset_diff tran)
qed
lemma multp_if_maximal_of_lhs_is_less:
assumes
trans: "transp R" and
asym: "asymp_on (set_mset M1) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
"x1 ∈# M1" and "x2 ∈# M2" and
"is_maximal_in_mset_wrt R M1 x1" and "R x1 x2"
shows "multp R M1 M2"
proof (rule one_step_implies_multp[of _ _ _ "{#}", simplified])
show "M2 ≠ {#}"
using ‹x2 ∈# M2› by auto
next
show "∀k∈#M1. ∃j∈#M2. R k j"
using assms
using is_maximal_in_mset_wrt_iff[OF transp_on_subset[OF trans subset_UNIV] asym]
by (metis Un_iff totalp_onD transpE)
qed
subsection ‹Nonuniqueness›
lemma
fixes x :: 'a and y :: 'a
assumes "x ≠ y"
shows
not_Uniq_is_minimal_in_mset_if_two_distinct_elements:
"¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x))" and
not_Uniq_is_maximal_in_mset_wrt_if_two_distinct_elements:
"¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x))" and
not_Uniq_is_strictly_minimal_in_mset_if_two_distinct_elements:
"¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_strictly_minimal_in_mset_wrt R X x))" and
not_Uniq_is_strictly_maximal_in_mset_wrt_if_two_distinct_elements:
"¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_strictly_maximal_in_mset_wrt R X x))"
proof -
let ?R = "λ_ _. False"
let ?X = "{#x, y#}"
have trans: "transp_on (set_mset ?X) ?R" and asym: "asymp_on (set_mset ?X) ?R"
by (simp_all add: transp_onI asymp_onI)
have "is_minimal_in_mset_wrt ?R ?X x" and "is_minimal_in_mset_wrt ?R ?X y"
using is_minimal_in_mset_wrt_iff[OF trans asym] by simp_all
thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x))"
using ‹x ≠ y› trans asym
by (metis Uniq_D)
have "is_maximal_in_mset_wrt ?R ?X x" and "is_maximal_in_mset_wrt ?R ?X y"
using is_maximal_in_mset_wrt_iff[OF trans asym] by simp_all
thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x))"
using ‹x ≠ y› trans asym
by (metis Uniq_D)
have "is_strictly_minimal_in_mset_wrt ?R ?X x" and "is_strictly_minimal_in_mset_wrt ?R ?X y"
using ‹x ≠ y› is_strictly_minimal_in_mset_wrt_iff[OF trans asym] by simp_all
thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_strictly_minimal_in_mset_wrt R X x))"
using ‹x ≠ y› trans asym
by (metis Uniq_D)
have "is_strictly_maximal_in_mset_wrt ?R ?X x" and "is_strictly_maximal_in_mset_wrt ?R ?X y"
using ‹x ≠ y› is_strictly_maximal_in_mset_wrt_iff[OF trans asym] by simp_all
thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
(∃⇩≤⇩1x. is_strictly_maximal_in_mset_wrt R X x))"
using ‹x ≠ y› trans asym
by (metis Uniq_D)
qed
section ‹Least and greatest elements›
definition is_least_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹ totalp_on (set_mset X) R ⟹
is_least_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"
definition is_greatest_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
"transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹ totalp_on (set_mset X) R ⟹
is_greatest_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R y x)"
context
fixes X R
assumes
trans: "transp_on (set_mset X) R" and
asym: "asymp_on (set_mset X) R" and
tot: "totalp_on (set_mset X) R"
begin
subsection ‹Conversions›
lemma is_least_in_mset_wrt_iff:
"is_least_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"
using is_least_in_mset_wrt_def[OF trans asym tot] .
lemma is_greatest_in_mset_wrt_iff:
"is_greatest_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R y x)"
using is_greatest_in_mset_wrt_def[OF trans asym tot] .
lemma is_minimal_in_mset_wrt_if_is_least_in_mset_wrt[intro]:
"is_least_in_mset_wrt R X x ⟹ is_minimal_in_mset_wrt R X x"
unfolding is_minimal_in_mset_wrt_iff[OF trans asym]
unfolding is_least_in_mset_wrt_def[OF trans asym tot]
by (metis add_mset_remove_trivial_eq asym asymp_onD insert_noteq_member)
lemma is_maximal_in_mset_wrt_if_is_greatest_in_mset_wrt[intro]:
"is_greatest_in_mset_wrt R X x ⟹ is_maximal_in_mset_wrt R X x"
unfolding is_maximal_in_mset_wrt_iff[OF trans asym]
unfolding is_greatest_in_mset_wrt_def[OF trans asym tot]
by (metis add_mset_remove_trivial_eq asym asymp_onD insert_noteq_member)
lemma is_strictly_minimal_in_mset_wrt_iff_is_least_in_mset_wrt:
"is_strictly_minimal_in_mset_wrt R X = is_least_in_mset_wrt R X"
unfolding is_strictly_minimal_in_mset_wrt_iff[OF trans asym] is_least_in_mset_wrt_iff
proof(intro ext iffI)
fix x
show "x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= y x) ⟹ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"
by (metis (mono_tags, lifting) in_diffD sup2CI tot totalp_onD)
next
fix x
show "x ∈# X ∧ (∀y ∈# X - {#x#}. R x y) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= y x)"
by (metis (full_types) asym asymp_onD in_diffD sup2E)
qed
lemma is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt:
"is_strictly_maximal_in_mset_wrt R X = is_greatest_in_mset_wrt R X"
unfolding is_strictly_maximal_in_mset_wrt_iff[OF trans asym] is_greatest_in_mset_wrt_iff
proof(intro ext iffI)
fix x
show "x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= x y) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. R y x)"
by (metis (mono_tags, lifting) in_diffD sup2CI tot totalp_onD)
next
fix x
show "x ∈# X ∧ (∀y∈#X - {#x#}. R y x) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= x y)"
by (metis (full_types) asym asymp_onD in_diffD sup2E)
qed
subsection ‹Uniqueness›
lemma Uniq_is_minimal_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x"
unfolding is_minimal_in_mset_wrt_iff[OF trans asym]
by (smt (verit, best) Uniq_I tot totalp_onD)
lemma Uniq_is_maximal_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x"
unfolding is_maximal_in_mset_wrt_iff[OF trans asym]
by (smt (verit, best) Uniq_I tot totalp_onD)
lemma Uniq_is_least_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_least_in_mset_wrt R X x"
using is_least_in_mset_wrt_iff
by (smt (verit, best) Uniq_I asym asymp_onD insert_DiffM insert_noteq_member)
lemma Uniq_is_greatest_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_greatest_in_mset_wrt R X x"
unfolding is_greatest_in_mset_wrt_iff
by (smt (verit, best) Uniq_I asym asymp_onD insert_DiffM insert_noteq_member)
lemma Uniq_is_strictly_minimal_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_strictly_minimal_in_mset_wrt R X x"
using Uniq_is_least_in_mset_wrt
unfolding is_strictly_minimal_in_mset_wrt_iff_is_least_in_mset_wrt.
lemma Uniq_is_strictly_maximal_in_mset_wrt[intro]:
"∃⇩≤⇩1x. is_strictly_maximal_in_mset_wrt R X x"
using Uniq_is_greatest_in_mset_wrt
unfolding is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt.
subsection ‹Miscellaneous›
lemma is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one:
"is_least_in_mset_wrt R X x ⟷ is_minimal_in_mset_wrt R X x ∧ count X x = 1"
proof (rule iffI)
assume "is_least_in_mset_wrt R X x"
thus "is_minimal_in_mset_wrt R X x ∧ count X x = 1"
unfolding is_least_in_mset_wrt_iff is_minimal_in_mset_wrt_iff[OF trans asym]
by (metis One_nat_def add_mset_remove_trivial_eq asym asymp_onD count_add_mset not_in_iff)
next
assume "is_minimal_in_mset_wrt R X x ∧ count X x = 1"
then show "is_least_in_mset_wrt R X x"
unfolding is_least_in_mset_wrt_iff is_minimal_in_mset_wrt_iff[OF trans asym]
by (metis count_single in_diffD in_diff_count nat_less_le tot totalp_onD)
qed
lemma is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one:
"is_greatest_in_mset_wrt R X x ⟷ is_maximal_in_mset_wrt R X x ∧ count X x = 1"
proof (rule iffI)
assume "is_greatest_in_mset_wrt R X x"
thus "is_maximal_in_mset_wrt R X x ∧ count X x = 1"
unfolding is_greatest_in_mset_wrt_iff is_maximal_in_mset_wrt_iff[OF trans asym]
by (metis One_nat_def add_mset_remove_trivial_eq asym asymp_onD count_add_mset not_in_iff)
next
assume "is_maximal_in_mset_wrt R X x ∧ count X x = 1"
then show "is_greatest_in_mset_wrt R X x"
unfolding is_greatest_in_mset_wrt_iff is_maximal_in_mset_wrt_iff[OF trans asym]
by (metis count_single in_diffD in_diff_count nat_less_le tot totalp_onD)
qed
lemma count_ge_2_if_minimal_in_mset_wrt_and_not_least_in_mset_wrt:
assumes "is_minimal_in_mset_wrt R X x" and "¬ is_least_in_mset_wrt R X x"
shows "count X x ≥ 2"
using assms
unfolding is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one
by (metis Suc_1 Suc_le_eq antisym_conv1 asym count_greater_eq_one_iff is_minimal_in_mset_wrt_iff
trans)
lemma count_ge_2_if_maximal_in_mset_wrt_and_not_greatest_in_mset_wrt:
assumes "is_maximal_in_mset_wrt R X x" and "¬ is_greatest_in_mset_wrt R X x"
shows "count X x ≥ 2"
using assms
unfolding is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one
by (metis Suc_1 Suc_le_eq antisym_conv1 asym count_greater_eq_one_iff is_maximal_in_mset_wrt_iff
trans)
lemma explode_greatest_in_mset_wrt:
assumes max: "is_greatest_in_mset_wrt R X x"
shows "add_mset x {#y ∈# X. y ≠ x#} = X"
using max[folded is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt]
using explode_strictly_maximal_in_mset_wrt[OF trans asym]
by metis
end
lemma multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
"R x1 x2"
shows "multp⇩H⇩O R M1 M2"
proof -
have
trans1: "transp_on (set_mset M1) R" and trans2: "transp_on (set_mset M2) R" and
asym1: "asymp_on (set_mset M1) R" and asym2: "asymp_on (set_mset M2) R" and
tot1: "totalp_on (set_mset M1) R" and tot2: "totalp_on (set_mset M2) R"
using trans[THEN transp_on_subset] asym[THEN asymp_on_subset] tot[THEN totalp_on_subset]
by simp_all
have x1_in: "x1 ∈# M1" and x1_gr: "∀y∈#M1. y ≠ x1 ⟶ ¬ R x1 y"
using x1_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans1 asym1]] by argo+
have x2_in: "x2 ∈# M2" and x2_gr: "∀y∈#M2. y ≠ x2 ⟶ ¬ R x2 y"
using x2_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans2 asym2]] by argo+
show "multp⇩H⇩O R M1 M2"
unfolding multp⇩H⇩O_def
proof (intro conjI)
show "M1 ≠ M2"
using x1_in x2_in x1_gr
by (metis ‹R x1 x2› asym2 asymp_onD)
next
show "∀y. count M2 y < count M1 y ⟶ (∃x. R y x ∧ count M1 x < count M2 x)"
using x1_in x2_in x1_gr x2_gr
by (smt (verit, best) assms(6) asym1 asymp_onD count_greater_zero_iff count_inI
dual_order.strict_trans local.trans subsetD sup_ge1 sup_ge2 tot1 totalp_onD transp_onD)
qed
qed
lemma multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
"R x1 x2"
shows "multp⇩D⇩M R M1 M2"
using multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt[OF assms, THEN multp⇩H⇩O_imp_multp⇩D⇩M] .
lemma multp_if_maximal_wrt_less_that_maximal_wrt:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
"R x1 x2"
shows "multp R M1 M2"
using multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt[OF assms, THEN multp⇩D⇩M_imp_multp] .
lemma multp⇩H⇩O_if_same_maximal_wrt_and_count_lt:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
x1_maximal: "is_maximal_in_mset_wrt R M1 x" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x" and
"count M1 x < count M2 x"
shows "multp⇩H⇩O R M1 M2"
by (metis assms(6) asym asymp_on_subset count_inI is_greatest_in_set_wrt_iff
is_maximal_in_mset_wrt_def is_maximal_in_set_wrt_eq_is_greatest_in_set_wrt less_zeroE
local.trans multp⇩H⇩O_def order_less_imp_not_less sup_ge1 tot totalp_on_subset transp_on_subset
x1_maximal)
lemma multp_if_same_maximal_wrt_and_count_lt:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
x1_maximal: "is_maximal_in_mset_wrt R M1 x" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x" and
"count M1 x < count M2 x"
shows "multp R M1 M2"
using multp⇩H⇩O_if_same_maximal_wrt_and_count_lt[
OF assms, THEN multp⇩H⇩O_imp_multp⇩D⇩M, THEN multp⇩D⇩M_imp_multp] .
lemma less_than_maximal_wrt_if_multp⇩H⇩O:
assumes
trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
asym: "asymp_on (set_mset M2) R" and
tot: "totalp_on (set_mset M2) R" and
x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
"multp⇩H⇩O R M1 M2" and
"x1 ∈# M1"
shows "R⇧=⇧= x1 x2"
proof -
have
trans2: "transp_on (set_mset M2) R" and
asym2: "asymp_on (set_mset M2) R" and
tot2: "totalp_on (set_mset M2) R"
using trans[THEN transp_on_subset] asym[THEN asymp_on_subset] tot[THEN totalp_on_subset]
by simp_all
have x2_in: "x2 ∈# M2" and x2_gr: "∀y∈#M2. y ≠ x2 ⟶ ¬ R x2 y"
using x2_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans2 asym2]] by argo+
show ?thesis
proof (cases "x1 ∈# M2")
case True
thus ?thesis
using x2_gr by (metis (mono_tags) sup2CI tot2 totalp_onD x2_in)
next
case False
hence "x1 ∈# M1 - M2"
using ‹x1 ∈# M1› by (simp add: in_diff_count not_in_iff)
moreover have "∀k∈#M1 - M2. ∃x∈#M2 - M1. R k x"
using multp⇩H⇩O_implies_one_step_strong(2)[OF ‹multp⇩H⇩O R M1 M2›] .
ultimately obtain x where "x ∈# M2 - M1" and "R x1 x"
by metis
hence "x ≠ x2 ⟶ ¬ R x2 x"
using x2_gr by (metis in_diffD)
hence "x ≠ x2 ⟶ R x x2"
by (metis ‹x ∈# M2 - M1› in_diffD tot2 totalp_onD x2_in)
thus ?thesis
using ‹R x1 x›
by (meson Un_iff ‹x ∈# M2 - M1› assms(6) in_diffD local.trans sup2I1 transp_onD x2_in)
qed
qed
section ‹Examples of duplicate handling in set and multiset definitions›
lemma
fixes M :: "nat multiset"
defines "M ≡ {#0, 0, 1, 1, 2, 2#}"
shows
"is_minimal_in_set_wrt (<) (set_mset M) 0"
"is_minimal_in_mset_wrt (<) M 0"
"is_least_in_set_wrt (<) (set_mset M) 0"
"∄y. is_least_in_mset_wrt (<) M y"
by (auto simp: M_def is_minimal_in_set_wrt_iff is_minimal_in_mset_wrt_def
is_least_in_set_wrt_iff is_least_in_mset_wrt_def)
lemma
fixes x y :: 'a and M :: "'a multiset"
defines "M ≡ {#x, y, y#}"
defines "R ≡ λ_ _. False"
assumes "x ≠ y"
shows
"is_maximal_in_mset_wrt R M x"
"is_maximal_in_mset_wrt R M y"
"is_strictly_maximal_in_mset_wrt R M x"
"¬ is_strictly_maximal_in_mset_wrt R M y"
proof -
have transp_on_False[simp]: "⋀A. transp_on A (λ_ _. False)"
by (simp add: transp_onI)
have asymp_on_False[simp]: "⋀A. asymp_on A (λ_ _. False)"
by (simp add: asymp_onI)
show
"is_maximal_in_mset_wrt R M x"
"is_maximal_in_mset_wrt R M y"
"is_strictly_maximal_in_mset_wrt R M x"
"¬ is_strictly_maximal_in_mset_wrt R M y"
unfolding is_maximal_in_mset_wrt_iff[of M R, unfolded R_def, simplified, folded R_def]
unfolding is_strictly_maximal_in_mset_wrt_iff[of M R, unfolded R_def, simplified, folded R_def]
unfolding atomize_conj
using ‹x ≠ y›
by (simp add: M_def)
qed
section ‹Hide stuff›
text ‹We restrict the public interface to ease future internal changes.›
hide_fact is_minimal_in_mset_wrt_def is_maximal_in_mset_wrt_def
hide_fact is_strictly_minimal_in_mset_wrt_def is_strictly_maximal_in_mset_wrt_def
hide_fact is_least_in_mset_wrt_def is_greatest_in_mset_wrt_def
section ‹Integration in type classes›
abbreviation (in order) is_minimal_in_mset where
"is_minimal_in_mset ≡ is_minimal_in_mset_wrt (<)"
abbreviation (in order) is_maximal_in_mset where
"is_maximal_in_mset ≡ is_maximal_in_mset_wrt (<)"
abbreviation (in order) is_strictly_minimal_in_mset where
"is_strictly_minimal_in_mset ≡ is_strictly_minimal_in_mset_wrt (<)"
abbreviation (in order) is_strictly_maximal_in_mset where
"is_strictly_maximal_in_mset ≡ is_strictly_maximal_in_mset_wrt (<)"
lemmas (in order) is_minimal_in_mset_iff =
is_minimal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]
lemmas (in order) is_maximal_in_mset_iff =
is_maximal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]
lemmas (in order) is_strictly_minimal_in_mset_iff =
is_strictly_minimal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]
lemmas (in order) is_strictly_maximal_in_mset_iff =
is_strictly_maximal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]
lemmas (in order) is_minimal_in_mset_if_is_strictly_minimal_in_mset[intro] =
is_minimal_in_mset_wrt_if_is_strictly_minimal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) is_maximal_in_mset_if_is_strictly_maximal_in_mset[intro] =
is_maximal_in_mset_wrt_if_is_strictly_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) ex_minimal_in_mset =
ex_minimal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) ex_maximal_in_mset =
ex_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) explode_maximal_in_mset =
explode_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) explode_strictly_maximal_in_mset =
explode_strictly_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]
lemmas (in order) is_minimal_in_filter_mset_iff =
is_minimal_in_filter_mset_wrt_iff[OF transp_on_less asymp_on_less]
abbreviation (in linorder) is_least_in_mset where
"is_least_in_mset ≡ is_least_in_mset_wrt (<)"
abbreviation (in linorder) is_greatest_in_mset where
"is_greatest_in_mset ≡ is_greatest_in_mset_wrt (<)"
lemmas (in linorder) is_least_in_mset_iff =
is_least_in_mset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) is_greatest_in_mset_iff =
is_greatest_in_mset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) is_minimal_in_mset_if_is_least_in_mset[intro] =
is_minimal_in_mset_wrt_if_is_least_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) is_maximal_in_mset_if_is_greatest_in_mset[intro] =
is_maximal_in_mset_wrt_if_is_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_minimal_in_mset[intro] =
Uniq_is_minimal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_maximal_in_mset[intro] =
Uniq_is_maximal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_least_in_mset[intro] =
Uniq_is_least_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_greatest_in_mset[intro] =
Uniq_is_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_strictly_minimal_in_mset[intro] =
Uniq_is_strictly_minimal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) Uniq_is_strictly_maximal_in_mset[intro] =
Uniq_is_strictly_maximal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) is_least_in_mset_iff_is_minimal_and_count_eq_one =
is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) is_greatest_in_mset_iff_is_maximal_and_count_eq_one =
is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) count_ge_2_if_minimal_in_mset_and_not_least_in_mset =
count_ge_2_if_minimal_in_mset_wrt_and_not_least_in_mset_wrt[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) count_ge_2_if_maximal_in_mset_and_not_greatest_in_mset =
count_ge_2_if_maximal_in_mset_wrt_and_not_greatest_in_mset_wrt[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) explode_greatest_in_mset =
explode_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) multp⇩H⇩O_if_maximal_less_that_maximal =
multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) multp⇩D⇩M_if_maximal_less_that_maximal =
multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) multp_if_maximal_less_that_maximal =
multp_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
totalp_on_less]
lemmas (in linorder) multp⇩H⇩O_if_same_maximal_and_count_lt =
multp⇩H⇩O_if_same_maximal_wrt_and_count_lt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) multp_if_same_maximal_and_count_lt =
multp_if_same_maximal_wrt_and_count_lt[OF transp_on_less asymp_on_less totalp_on_less]
lemmas (in linorder) less_than_maximal_if_multp⇩H⇩O =
less_than_maximal_wrt_if_multp⇩H⇩O[OF transp_on_less asymp_on_less totalp_on_less]
lemma (in linorder)
assumes"is_greatest_in_mset C L"
shows "C - {#L#} = {#K ∈# C. K ≠ L#}"
using assms
by (smt (verit, del_insts) add_diff_cancel_left' diff_subset_eq_self diff_zero filter_empty_mset
filter_mset_add_mset filter_mset_eq_conv insert_DiffM2 local.is_greatest_in_mset_iff
local.not_less_iff_gr_or_eq)
end