theory Multiset2
imports
"HOL-Library.Multiset"
Relations
Util
begin
lemma comp_fun_commute_plus[simp]: "comp_fun_commute (op + :: (('a :: comm_monoid_add) ⇒ 'a ⇒ 'a))"
by (standard, auto simp: ac_simps)
lemma union_commutes:
"M + {#x#} + N = M + N + {#x#}"
"M + mset xs + N = M + N + mset xs"
by (auto simp: ac_simps)
lemma in_mset: assumes "x ∈# mset xs"
shows "∃ bef aft. xs = bef @ x # aft"
proof -
from assms[unfolded in_multiset_in_set set_conv_nth]
obtain i where i: "i < length xs" and x: "xs ! i = x" by auto
from id_take_nth_drop[OF i, unfolded x]
show ?thesis by auto
qed
lemma in_mset_idx :
assumes "a ∈# mset as"
shows "∃i. i < length as ∧ a = as ! i"
proof-
from in_mset[OF assms] obtain bef aft where
as_part: "as = bef @ a # aft" by auto
with nth_append_length have a_eq: "a = as ! (length bef)" by auto
from as_part and length_append have i_bd: "(length bef) < length as" by auto
from a_eq and i_bd show ?thesis by blast
qed
lemma in_set_idx:
assumes "a ∈ set as"
shows "∃i. i < length as ∧ a = as ! i"
using assms and in_multiset_in_set[of a as] and in_mset_idx[of a as]
by simp
lemma mem_multiset_diff_compat:
assumes "x ∈# A"
and "x ≠ y"
shows "x ∈# (A - {#y#})"
using assms unfolding set_mset_def by (induct A) (auto)
lemma in_mset_eq: assumes "M + {#x#} = mset ys"
shows "∃ bef aft. ys = bef @ x # aft ∧ M = mset (bef @ aft)"
proof -
from assms[symmetric] have "x ∈# mset ys" by auto
from in_mset[OF this] obtain bef aft where ys: "ys = bef @ x # aft"
by auto
have "M + {#x#} = mset (bef @ aft) + {#x#}"
unfolding assms ys multiset_eq_iff by auto
hence "M = mset (bef @ aft)" by auto
from ys this show ?thesis by auto
qed
lemma mset_concat: assumes "mset xs = mset ys"
shows "mset (concat xs) = mset (concat ys)"
using assms
proof (induct xs arbitrary: ys)
case Nil thus ?case by auto
next
case (Cons x xs)
let ?m = "mset"
from in_mset_eq Cons(2)[simplified]
obtain bef aft where ys: "ys = bef @ x # aft" and xs: "?m xs = ?m (bef @ aft)"
by force
from Cons(1)[OF xs] show ?case unfolding ys by (auto simp: multiset_eq_iff)
qed
lemma in_map_mset[intro]:
"a ∈# A ⟹ f a ∈# image_mset f A"
unfolding in_image_mset by simp
lemma image_mset_Union_mset [simp]:
"⋃# image_mset f (⋃# M) = ⋃# image_mset (λN. ⋃# (image_mset f) N) M"
by (induct M) simp_all
lemma in_mset_subset_Union: "M ∈# ms ⟹ M ⊆# ⋃# ms"
using multi_member_split by force
lemma mset_replicate_mono: assumes "m1 ⊆# m2"
shows "⋃# (mset (replicate n m1))
⊆# ⋃# (mset (replicate n m2))"
proof (induct n)
case (Suc n)
have "⋃# (mset (replicate (Suc n) m1)) =
⋃# (mset (replicate n m1)) + m1" by simp
also have "… ⊆# ⋃# (mset (replicate n m1)) + m2" using ‹m1 ⊆# m2› by auto
also have "… ⊆# ⋃# (mset (replicate n m2)) + m2" using Suc by auto
finally show ?case by (simp add: union_commute)
qed simp
lemma multised_add_singleton[simp]: "{# a #} + M = N + {# a #} ⟷ M = N"
"M + {# a #} = {# a #} + N ⟷ M = N"
by (auto simp: ac_simps)
lemma mem_Union_mset[simp]: "x ∈# ⋃# ms ⟷ x ∈ ⋃ (set_mset ` (set_mset ms))"
by (induct ms, auto)
lemma diff_union_swap_multiset :
"a ∈# A ⟹ A - {#a#} + B = A + B - {#a#}"
by (intro multiset_eqI) auto
text‹In a multiset, there exists a local maxima.›
lemma local_maxima_multiset:
assumes "locally_trans s A A A" (is "?lt A")
and "locally_irrefl s A" (is "?li A")
and A_ne: "A ≠ {#}"
shows "∃a. a ∈# A ∧ (∀b. b ∈# A ⟶ (b,a) ∉ s)"
using assms
proof (induct A)
case empty thus ?case by auto
next
case (add x A)
from lt_trans_l ‹?lt (add_mset x A)› have lt_A: "?lt A" by (metis add_mset_add_single)
from li_trans_l ‹?li (add_mset x A)› have li_A: "?li A" by (metis add_mset_add_single)
note IH = add(1)[OF lt_A li_A]
show ?case
proof (cases "A = {#}")
case True
with ‹?li (add_mset x A)›[unfolded locally_irrefl_def, rule_format] show ?thesis
by simp
next
case False
from IH[OF this]
obtain a1 where
a1_in_A: "a1 ∈# A"
and a1_is_lm: "∀b. b ∈# A ⟶ (b,a1) ∉ s" by force
show ?thesis
proof (cases "(x,a1) ∈ s")
case True note sxa1 = this
have GL: "x ∈# A + {# x #}" by auto
from add(3)[unfolded locally_irrefl_def]
have GR1: "(x,x) ∉ s" by simp
{
fix b assume b_in_A: "b ∈# A"
have "(b,x) ∉ s"
proof (cases "(b,x) ∈ s")
case True
from b_in_A have b_in: "b ∈# A + {# x #}" by simp
from a1_in_A have a1_in: "a1 ∈# A + {# x #}" by simp
from b_in and a1_in and GL and True and sxa1 and
add(3)[unfolded locally_irrefl_def] and
add(2)[unfolded locally_trans_def]
have "(b,a1) ∈ s" by (metis add_mset_add_single)
with a1_is_lm and b_in_A show ?thesis by auto
qed
}
hence GR2: "∀b. b ∈# A ⟶ (b,x) ∉ s" by simp
from this and GL and GR1 show ?thesis by auto
next
case False
from this and a1_is_lm
have GR: "∀b. b ∈# A + {# x #} ⟶ (b,a1) ∉ s" by simp
from a1_in_A have GL: "a1 ∈# A + {# x #}" by simp
from GL and GR show ?thesis by (metis add_mset_add_single)
qed
qed
qed
lemma mult1_ab_a: "({#a#}, {#a,b#}) ∈ mult1 r"
unfolding mult1_def
proof(rule, unfold split, intro exI conjI)
show "{#a, b#} = add_mset b {#a#}"
by (simp add: ac_simps)
next
show "{#a#} = {# a #} + {#}" by simp
qed simp
lemma mult1_ab_b: "({#b#}, {#a,b#}) ∈ mult1 r"
proof -
have id: "{#a,b#} = {#b,a#}" by (simp add: ac_simps)
show ?thesis unfolding id by (rule mult1_ab_a)
qed
declare mult1_union[intro!]
lemma mult1_mono_right[intro!]: assumes "(M,N) ∈ mult1 r"
shows "((M + T, N + T) ∈ mult1 r)"
using mult1_union[OF assms, of T] by (simp add: ac_simps)
lemma mult1_singleton[simp]:
shows "((M, {# t #}) ∈ mult1 r) = (∀ a. a ∈# M ⟶ (a,t) ∈ r)" (is "?l = ?r")
proof
assume r: ?r
show ?l
unfolding mult1_def
by (rule, unfold split, rule exI[of _ t], rule exI[of _ "{#}"],
rule exI[of _ M], insert r, auto)
next
assume l: ?l
from this[unfolded mult1_def]
obtain a M0 K where id: "{#t#} = M0 + {#a#}"
"M = M0 + K" and rel: "∀ b. b ∈# K ⟶ (b,a) ∈ r" by auto
from id(1)[unfolded single_is_union] have "M0 = {#}" by simp
with id have id: "t = a" "M = K" by auto
show ?r unfolding id by (rule rel)
qed
inductive_set bounded_mult :: "nat ⇒ 'a rel ⇒ 'a multiset rel" for b and r where
bounded_mult: "J ≠ {#} ⟹ size K ≤ b ⟹
(⋀ k. k ∈ set_mset K ⟹ ∃j ∈ set_mset J. (k, j) ∈ r) ⟹ (I + K, I + J) ∈ bounded_mult b r"
lemma bounded_mult_into_mult:
"(M,N) ∈ bounded_mult b r ⟹ (M,N) ∈ mult r"
by (induct rule: bounded_mult.induct, intro one_step_implies_mult, auto)
definition bmult_less where "bmult_less b ≡ bounded_mult b {(x,y :: nat). x < y}"
definition bound_mset :: "nat ⇒ nat multiset ⇒ nat" where
"bound_mset b ≡ λ M. sum_mset (image_mset (λ x. (Suc b) ^ x) M)"
declare bound_mset_def[simp]
lemma bound_mset_linear_in_size:
assumes ij: "⋀ j. j ∈ set_mset J ⟹ j < i"
shows "bound_mset b J = 0 ∨ (∃ x. x < i ∧ bound_mset b J ≤ size J * (Suc b^x))"
using ij
proof (induct J rule: multiset_induct)
case (add x J)
show ?case
proof (cases "size J = 0")
case True
thus ?thesis using add by (intro disjI2 exI[of _ x], auto)
next
case False
let ?bb = "Suc b"
let ?bound_mset = "bound_mset b"
from add(1)[OF add(2)] False obtain y where yi: "y < i" and bound: "?bound_mset J ≤ size J * ?bb ^ y" by (cases J, auto)
let ?x = "max x y"
from yi add(2)[of x] have xi: "?x < i" by auto
have "y ≤ ?x" by simp
from power_increasing[OF this, of ?bb]
have "size J * ?bb ^ y ≤ size J * ?bb ^ ?x" by simp
with bound have *: "?bound_mset J ≤ size J * ?bb ^ ?x" by arith
have "x ≤ ?x" by simp
from power_increasing[OF this, of ?bb] *
have "?bound_mset (J + {# x #}) ≤ size (J + {# x #}) * ?bb ^ ?x" by simp
with xi show ?thesis by force
qed
qed simp
lemma bound_mset_bmult_less: "(M,N) ∈ bmult_less b ^^ k ⟹ k ≤ bound_mset b N"
proof (induct k arbitrary: M N)
case (Suc k)
let ?bound_mset = "bound_mset b"
from Suc(2) obtain K where mk: "(M,K) ∈ bmult_less b ^^ k" and kn: "(K,N) ∈ bmult_less b" by auto
from Suc(1)[OF mk] have k: "k ≤ ?bound_mset K" .
show ?case using kn unfolding bmult_less_def
proof (cases)
case (bounded_mult I J L)
from bounded_mult(3,5) have "∃ i. i ∈ set_mset I ∧ (∀ j ∈ set_mset J. i > j)"
proof (induct J rule: multiset_induct)
case empty
thus ?case by (cases I, auto)
next
case (add j J)
from add(3)[of j] obtain i1 where i1: "i1 ∈ set_mset I" and i1j: "i1 > j" by auto
from add(1)[OF add(2) add(3)] obtain i2 where i2: "i2 ∈ set_mset I" and i2J: "⋀ j. j ∈ set_mset J ⟹ i2 > j" by force
show ?case
proof (cases "i1 < i2")
case True
thus ?thesis
by (intro exI[of _ i2], insert i2 i2J i1j, auto)
next
case False
{
fix j
assume "j ∈ set_mset J"
from i2J[OF this] False have "i1 > j" by simp
}
thus ?thesis
by (intro exI[of _ i1], insert i1 i1j, auto)
qed
qed
then obtain i where i: "i ∈ set_mset I" and ij: "⋀ j. j ∈ set_mset J ⟹ i > j" by blast
define bb where "bb = Suc b"
have bb1: "1 ≤ bb" unfolding bb_def by simp
from i have I: "I = I - {# i #} + {# i #}" by auto
from arg_cong[OF this, of ?bound_mset]
have le: "bb^i ≤ ?bound_mset I" unfolding bb_def by simp
from bound_mset_linear_in_size[OF ij, of J b]
have choice: "?bound_mset J = 0 ∨ (∃ x. x < i ∧ ?bound_mset J ≤ size J * (bb^x))" unfolding bb_def .
have "?bound_mset J + 1 ≤ bb^i"
proof (cases "?bound_mset J = 0")
case True
thus ?thesis by (simp add: bb_def)
next
case False
with choice obtain x where xi: "x < i" and bound: "?bound_mset J ≤ size J * bb^x" by auto
have "size J * bb ^ x ≤ b * bb ^ x" using bound bounded_mult(4) by simp
with bound have bound: "?bound_mset J ≤ b * bb^x" by arith
also have "b * bb^x < (b+1) * bb^x" using bb1 by simp
also have "… = bb^(x + 1)" unfolding bb_def by simp
also have "… ≤ bb^i" by (rule power_increasing[OF _ bb1], insert xi, auto)
finally show ?thesis by simp
qed
with le
have "?bound_mset J + 1 ≤ ?bound_mset I" by arith
thus ?thesis using k unfolding bounded_mult(1-2)
by simp
qed
qed simp
lemma subset_imp_bounded_mult_refl: assumes "B ⊆# A"
shows "(B,A) ∈ (bounded_mult k f)^="
proof -
from assms[unfolded mset_subset_eq_exists_conv]
obtain C where A: "A = B + C" by auto
show ?thesis
proof (cases "C = {#}")
case True
with A show ?thesis by auto
next
case False
have id: "(B,A) = (B + {#}, B + C)" unfolding A by simp
have "(B,A) ∈ bounded_mult k f" unfolding id
by (rule bounded_mult, insert False, auto)
thus ?thesis by simp
qed
qed
lemma bound_mset_mono: assumes "A ⊆# B"
shows "bound_mset k A ≤ bound_mset k B"
proof -
from assms[unfolded mset_subset_eq_exists_conv]
obtain C where B: "B = A + C" by auto
show ?thesis unfolding B bound_mset_def by auto
qed
declare bound_mset_def[simp del]
lemma mult_subset_mult:
assumes "(A, B) ∈ mult r"
and "B ⊆# C"
shows "(A, C) ∈ mult r"
proof -
from assms(2) obtain D where D:"B + D = C"
using mset_subset_eq_exists_conv by metis
then show ?thesis
proof (cases "D = {#}")
case True
with D assms(1) show ?thesis by auto
next
case (False)
from D one_step_implies_mult[OF False, of "{#}"] have "(B, C) ∈ mult r"
by auto
with assms(1) show ?thesis unfolding mult_def by auto
qed
qed
lemma mset_remove_nth:
assumes "i < length ss"
shows "mset (remove_nth i ss) + {#ss ! i#} = mset ss"
by (metis add_mset_add_single assms id_take_nth_drop mset.simps(2) remove_nth_def union_code union_mset_add_mset_right)
lemma remove_nth_mult:
assumes "i < length ss"
shows "(mset (remove_nth i ss), mset ss) ∈ mult r"
proof -
have "mset ss = mset (remove_nth i ss) + {#ss ! i#}"
using assms mset_remove_nth by force
with one_step_implies_mult [rule_format, of "{#ss ! i#}" "{#}"]
show ?thesis by auto
qed
lemma non_empty_empty_mult:
assumes "A ≠ {#}"
shows "({#}, A) ∈ mult r"
using assms one_step_implies_mult[rule_format, of A "{#}" _ "{#}"]
by auto
lemma mset_concat_union:
"mset (concat xs) = ⋃# mset (map mset xs)"
proof (induct xs)
case (Cons x xs)
then show ?case by (simp add: union_commute)
qed auto
lemma pointwise_mult_imp_mult:
assumes "length Ms = length Ns"
and "∀i<length Ns. (Ms ! i, Ns ! i) ∈ (mult r)⇧="
and "trans r"
shows "(⋃#(mset Ms), ⋃#(mset Ns)) ∈ (mult r)⇧="
using assms(1,2)
proof (induct Ms Ns rule: list_induct2)
case (Cons M Ms N Ns)
from Cons(3) have "∀i<length Ns. (Ms ! i, Ns ! i) ∈ (mult r)⇧=" by auto
from Cons(2)[OF this] consider
(mult) "(⋃#mset Ms, ⋃#mset Ns) ∈ (mult r)"
| (eq) "⋃#mset Ms = ⋃#mset Ns"
by auto
then show ?case
proof (cases)
case mult
then obtain I J K where Ns:"⋃#mset Ns = I + J" and Ms:"⋃#mset Ms = I + K"
and J:"J ≠ {#}" and K:"(∀k∈set_mset K. ∃j∈set_mset J. (k, j) ∈ r)"
using mult_implies_one_step assms(3) by metis
from Cons(3) have "(M, N) ∈ (mult r) ∨ M = N" by auto
then show ?thesis
proof
assume "M = N"
with one_step_implies_mult[OF J K, of "I + M"] show ?thesis
by (auto simp: Ms Ns ac_simps)
next
assume "(M, N) ∈ (mult r)"
then obtain I' J' K' where N:"N = I' + J'" and M:"M = I' + K'"
and J':"J' ≠ {#}" and K':"(∀k∈set_mset K'. ∃j∈set_mset J'. (k, j) ∈ r)"
using mult_implies_one_step assms(3) by metis
from J J' have J:"J + J' ≠ {#}" by auto
from K K' have K:"(∀k∈set_mset (K + K'). ∃j∈set_mset (J + J'). (k, j) ∈ r)"
by auto
show ?thesis using one_step_implies_mult[OF J K, of "I + I'"]
by (auto simp: N M Ms Ns ac_simps)
qed
next
case eq
from Cons(3) have "(M, N) ∈ (mult r) ∨ M = N" by auto
then show ?thesis
proof
assume "(M, N) ∈ (mult r)"
then obtain I J K where "N = I + J" and "M = I + K"
and J:"J ≠ {#}" and K:"(∀k∈set_mset K. ∃j∈set_mset J. (k, j) ∈ r)"
using mult_implies_one_step assms(3) by metis
with eq show ?thesis
using one_step_implies_mult[OF J K, of "I + ⋃#mset Ms"] by (auto simp: ac_simps)
qed (insert eq, auto)
qed
qed auto
end