Theory Multiset_Extension_Pair
section ‹Multiset extension of an order pair›
text ‹Given a well-founded order $\prec$ and a compatible non-strict order $\precsim$,
we define the corresponding multiset-extension of these orders.›
theory Multiset_Extension_Pair
imports
"HOL-Library.Multiset"
"Regular-Sets.Regexp_Method"
"Abstract-Rewriting.Abstract_Rewriting"
Relations
begin
lemma mult_locally_cancel:
assumes "trans s " and "locally_irrefl s (X + Z)" and "locally_irrefl s (Y + Z)"
shows "(X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s" (is "?L ⟷ ?R")
proof
assume ?L thus ?R using assms(2, 3)
proof (induct Z arbitrary: X Y)
case (add z Z)
obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' ≠ {#}"
"∀x ∈ set_mset X'. ∃y ∈ set_mset Y'. (x, y) ∈ s"
using mult_implies_one_step[OF ‹trans s› add(2)] by auto
consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
thus ?case
proof (cases)
case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
(metis add.hyps add.prems(2) add.prems(3) add_mset_add_single li_trans_l union_mset_add_mset_right)
next
case 2 then obtain y where "y ∈ set_mset Y2" "(z, y) ∈ s" using *(4) add(3, 4)
by (auto simp: locally_irrefl_def)
moreover from this transD[OF ‹trans s› _ this(2)]
have "x' ∈ set_mset X2 ⟹ ∃y ∈ set_mset Y2. (x', y) ∈ s" for x'
using 2 *(4)[rule_format, of x'] by auto
ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2 add(3, 4)
by (force simp: locally_irrefl_def add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
qed
qed auto
next
assume ?R then obtain I J K
where "Y = I + J" "X = I + K" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ s"
using mult_implies_one_step[OF ‹trans s›] by blast
thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed
lemma mult_locally_cancelL:
assumes "trans s" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)"
shows "(Z + X, Z + Y) ∈ mult s ⟷ (X, Y) ∈ mult s"
using mult_locally_cancel[OF assms] by (simp only: union_commute)
lemma mult_cancelL:
assumes "trans s" "irrefl s" shows "(Z + X, Z + Y) ∈ mult s ⟷ (X, Y) ∈ mult s"
using assms
by (auto simp: union_commute intro!: mult_cancel elim: irrefl_on_subset)
lemma wf_trancl_conv:
shows "wf (r⇧+) ⟷ wf r"
using wf_subset[of "r⇧+" r] by (force simp: wf_trancl)
subsection ‹Pointwise multiset order›
inductive_set multpw :: "'a rel ⇒ 'a multiset rel" for ns :: "'a rel" where
empty: "({#}, {#}) ∈ multpw ns"
| add: "(x, y) ∈ ns ⟹ (X, Y) ∈ multpw ns ⟹ (add_mset x X, add_mset y Y) ∈ multpw ns"
lemma multpw_emptyL [simp]:
"({#}, X) ∈ multpw ns ⟷ X = {#}"
by (cases X) (auto elim: multpw.cases intro: multpw.intros)
lemma multpw_emptyR [simp]:
"(X, {#}) ∈ multpw ns ⟷ X = {#}"
by (cases X) (auto elim: multpw.cases intro: multpw.intros)
lemma refl_multpw:
assumes "refl ns" shows "refl (multpw ns)"
proof -
have "(X, X) ∈ multpw ns" for X using assms
by (induct X) (auto intro: multpw.intros simp: refl_on_def)
then show ?thesis by (auto simp: refl_on_def)
qed
lemma multpw_Id_Id [simp]:
"multpw Id = Id"
proof -
have "(X, Y) ∈ multpw (Id :: 'a rel) ⟹ X = Y" for X Y by (induct X Y rule: multpw.induct) auto
then show ?thesis using refl_multpw[of Id] by (auto simp: refl_on_def)
qed
lemma mono_multpw:
assumes "ns ⊆ ns'" shows "multpw ns ⊆ multpw ns'"
proof -
have "(X, Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw ns'" for X Y
by (induct X Y rule: multpw.induct) (insert assms, auto intro: multpw.intros)
then show ?thesis by auto
qed
lemma multpw_converse:
"multpw (ns¯) = (multpw ns)¯"
proof -
have "(X, Y) ∈ multpw (ns¯) ⟹ (X, Y) ∈ (multpw ns)¯" for X Y and ns :: "'a rel"
by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)
then show ?thesis by auto
qed
lemma multpw_local:
"(X, Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw (ns ∩ set_mset X × set_mset Y)"
proof (induct X Y rule: multpw.induct)
case (add x y X Y) then show ?case
using mono_multpw[of "ns ∩ set_mset X × set_mset Y" "ns ∩ insert x (set_mset X) × insert y (set_mset Y)"]
by (auto intro: multpw.intros)
qed auto
lemma multpw_split1R:
assumes "(add_mset x X, Y) ∈ multpw ns"
obtains z Z where "Y = add_mset z Z" and "(x, z) ∈ ns" and "(X, Z) ∈ multpw ns"
using assms
proof (induct "add_mset x X" Y arbitrary: X thesis rule: multpw.induct)
case (add x' y' X' Y') then show ?case
proof (cases "x = x'")
case False
obtain X'' where [simp]: "X = add_mset x' X''"
using add(4) False
by (metis add_eq_conv_diff)
have "X' = add_mset x X''" using add(4) by (auto simp: add_eq_conv_ex)
with add(2) obtain Y'' y where "Y' = add_mset y Y''" "(x,y) ∈ ns" "(X'', Y'') ∈ multpw ns"
by (auto intro: add(3))
then show ?thesis using add(1) add(5)[of y "add_mset y' Y''"]
by (auto simp: ac_simps intro: multpw.intros)
qed auto
qed auto
lemma multpw_splitR:
assumes "(X1 + X2, Y) ∈ multpw ns"
obtains Y1 Y2 where "Y = Y1 + Y2" and "(X1, Y1) ∈ multpw ns" and "(X2, Y2) ∈ multpw ns"
using assms
proof (induct X2 arbitrary: Y thesis)
case (add x2 X2)
from add(3) obtain Y' y2 where "(X1 + X2, Y') ∈ multpw ns" "(x2, y2) ∈ ns" "Y = add_mset y2 Y'"
by (auto elim: multpw_split1R simp: union_assoc[symmetric])
moreover then obtain Y1 Y2 where "(X1, Y1) ∈ multpw ns" "(X2, Y2) ∈ multpw ns" "Y' = Y1 + Y2"
by (auto elim: add(1)[rotated])
ultimately show ?case by (intro add(2)) (auto simp: union_assoc intro: multpw.intros)
qed auto
lemma multpw_split1L:
assumes "(X, add_mset y Y) ∈ multpw ns"
obtains z Z where "X = add_mset z Z" and "(z, y) ∈ ns" and "(Z, Y) ∈ multpw ns"
using assms multpw_split1R[of y Y X "ns¯" thesis] by (auto simp: multpw_converse)
lemma multpw_splitL:
assumes "(X, Y1 + Y2) ∈ multpw ns"
obtains X1 X2 where "X = X1 + X2" and "(X1, Y1) ∈ multpw ns" and "(X2, Y2) ∈ multpw ns"
using assms multpw_splitR[of Y1 Y2 X "ns¯" thesis] by (auto simp: multpw_converse)
lemma locally_trans_multpw:
assumes "locally_trans ns S T U"
and "(S, T) ∈ multpw ns"
and "(T, U) ∈ multpw ns"
shows "(S, U) ∈ multpw ns"
using assms(2,3,1)
proof (induct S T arbitrary: U rule: multpw.induct)
case (add x y X Y)
then show ?case unfolding locally_trans_def
by (auto 0 3 intro: multpw.intros elim: multpw_split1R)
qed blast
lemma trans_multpw:
assumes "trans ns" shows "trans (multpw ns)"
using locally_trans_multpw unfolding locally_trans_def trans_def
by (meson assms locally_trans_multpw tr_ltr)
lemma multpw_add:
assumes "(X1, Y1) ∈ multpw ns" "(X2, Y2) ∈ multpw ns" shows "(X1 + X2, Y1 + Y2) ∈ multpw ns"
using assms(2,1)
by (induct X2 Y2 rule: multpw.induct) (auto intro: multpw.intros simp: add.assoc[symmetric])
lemma multpw_single:
"(x, y) ∈ ns ⟹ ({#x#}, {#y#}) ∈ multpw ns"
using multpw.intros(2)[OF _ multpw.intros(1)] .
lemma multpw_mult1_commute:
assumes compat: "s O ns ⊆ s" and reflns: "refl ns"
shows "mult1 s O multpw ns ⊆ multpw ns O mult1 s"
proof -
{ fix X Y Z assume 1: "(X, Y) ∈ mult1 s" "(Y, Z) ∈ multpw ns"
then obtain X' Y' y where 2: "X = Y' + X'" "Y = add_mset y Y'" "∀x. x ∈# X' ⟶ (x, y) ∈ s"
by (auto simp: mult1_def)
moreover obtain Z' z where 3: "Z = add_mset z Z'" "(y, z) ∈ ns" "(Y', Z') ∈ multpw ns"
using 1(2) 2(2) by (auto elim: multpw_split1R)
moreover have "∀x. x ∈# X' ⟶ (x, z) ∈ s" using 2(3) 3(2) compat by blast
ultimately have "∃Y'. (X, Y') ∈ multpw ns ∧ (Y', Z) ∈ mult1 s" unfolding mult1_def
using refl_multpw[OF reflns]
by (intro exI[of _ "Z' + X'"]) (auto intro: multpw_add simp: refl_on_def)
}
then show ?thesis by fast
qed
lemma multpw_mult_commute:
assumes "s O ns ⊆ s" "refl ns" shows "mult s O multpw ns ⊆ multpw ns O mult s"
proof -
{ fix X Y Z assume 1: "(X, Y) ∈ mult s" "(Y, Z) ∈ multpw ns"
then have "∃Y'. (X, Y') ∈ multpw ns ∧ (Y', Z) ∈ mult s" unfolding mult_def
using multpw_mult1_commute[OF assms] by (induct rule: converse_trancl_induct) (auto 0 3)
}
then show ?thesis by fast
qed
lemma wf_mult_rel_multpw:
assumes "wf s" "s O ns ⊆ s" "refl ns" shows "wf ((multpw ns)⇧* O mult s O (multpw ns)⇧*)"
using assms(1) multpw_mult_commute[OF assms(2,3)] by (subst qc_wf_relto_iff) (auto simp: wf_mult)
lemma multpw_cancel1:
assumes "trans ns" "(y, x) ∈ ns"
shows "(add_mset x X, add_mset y Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw ns" (is "?L ⟹ ?R")
proof -
assume ?L then obtain x' X' where X: "(x', y) ∈ ns" "add_mset x' X' = add_mset x X" "(X', Y) ∈ multpw ns"
by (auto elim: multpw_split1L simp: union_assoc[symmetric])
then show ?R
proof (cases "x = x'")
case False then obtain X2 where X2: "X' = add_mset x X2" "X = add_mset x' X2"
using X(2) by (auto simp: add_eq_conv_ex)
then obtain y' Y' where Y: "(x, y') ∈ ns" "Y = add_mset y' Y'" "(X2, Y') ∈ multpw ns"
using X(3) by (auto elim: multpw_split1R)
have "(x', y') ∈ ns" using X(1) Y(1) ‹trans ns› assms(2) by (metis trans_def)
then show ?thesis using Y by (auto intro: multpw.intros simp: X2)
qed auto
qed
lemma multpw_cancel:
assumes "refl ns" "trans ns"
shows "(X + Z, Y + Z) ∈ multpw ns ⟷ (X, Y) ∈ multpw ns" (is "?L ⟷ ?R")
proof
assume ?L then show ?R
proof (induct Z)
case (add z Z) then show ?case using multpw_cancel1[of ns z z "X + Z" "Y + Z"] assms
by (auto simp: refl_on_def union_assoc)
qed auto
next
assume ?R then show ?L using assms refl_multpw by (auto intro: multpw_add simp: refl_on_def)
qed
lemma multpw_cancelL:
assumes "refl ns" "trans ns" shows "(Z + X, Z + Y) ∈ multpw ns ⟷ (X, Y) ∈ multpw ns"
using multpw_cancel[OF assms, of X Z Y] by (simp only: union_commute)
subsection ‹Multiset extension for order pairs via the pointwise order and @{const mult}›
definition "mult2_s ns s ≡ multpw ns O mult s"
definition "mult2_ns ns s ≡ multpw ns O (mult s)⇧="
lemma mult2_ns_conv:
shows "mult2_ns ns s = mult2_s ns s ∪ multpw ns"
by (auto simp: mult2_s_def mult2_ns_def)
lemma mono_mult2_s:
assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_s ns s ⊆ mult2_s ns' s'"
using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_s_def by auto
lemma mono_mult2_ns:
assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_ns ns s ⊆ mult2_ns ns' s'"
using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_ns_def by auto
lemma wf_mult2_s:
assumes "wf s" "s O ns ⊆ s" "refl ns"
shows "wf (mult2_s ns s)"
using wf_mult_rel_multpw[OF assms] assms by (auto simp: mult2_s_def wf_mult intro: wf_subset)
lemma refl_mult2_ns:
assumes "refl ns" shows "refl (mult2_ns ns s)"
using refl_multpw[OF assms] unfolding mult2_ns_def refl_on_def by fast
lemma trans_mult2_s:
assumes "s O ns ⊆ s" "refl ns" "trans ns"
shows "trans (mult2_s ns s)"
using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
unfolding mult2_s_def trans_O_iff by (blast 8)
lemma trans_mult2_ns:
assumes "s O ns ⊆ s" "refl ns" "trans ns"
shows "trans (mult2_ns ns s)"
using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
unfolding mult2_ns_def trans_O_iff by (blast 8)
lemma compat_mult2:
assumes "s O ns ⊆ s" "refl ns" "trans ns"
shows "mult2_ns ns s O mult2_s ns s ⊆ mult2_s ns s" "mult2_s ns s O mult2_ns ns s ⊆ mult2_s ns s"
using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
unfolding mult2_s_def mult2_ns_def trans_O_iff by (blast 8)+
text ‹Trivial inclusions›
lemma mult_implies_mult2_s:
assumes "refl ns" "(X, Y) ∈ mult s"
shows "(X, Y) ∈ mult2_s ns s"
using refl_multpw[of ns] assms unfolding mult2_s_def refl_on_def by blast
lemma mult_implies_mult2_ns:
assumes "refl ns" "(X, Y) ∈ (mult s)⇧="
shows "(X, Y) ∈ mult2_ns ns s"
using refl_multpw[of ns] assms unfolding mult2_ns_def refl_on_def by blast
lemma multpw_implies_mult2_ns:
assumes "(X, Y) ∈ multpw ns"
shows "(X, Y) ∈ mult2_ns ns s"
unfolding mult2_ns_def using assms by simp
subsection ‹One-step versions of the multiset extensions›
lemma mult2_s_one_step:
assumes "ns O s ⊆ s" "refl ns" "trans s"
shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ Y2 ≠ {#} ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))" (is "?L ⟷ ?R")
proof
assume ?R then obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns" and
"Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by blast
then have "(Y1 + X2, Y1 + Y2) ∈ mult s"
using ‹trans s› by (auto intro: one_step_implies_mult)
moreover have "(X1 + X2, Y1 + X2) ∈ multpw ns"
using ‹refl ns› refl_multpw[of ns] by (auto intro: multpw_add simp: refl_on_def *)
ultimately show ?L by (auto simp: mult2_s_def *)
next
assume ?L then obtain X1 X2 Z1 Z2 Y2 where *: "X = X1 + X2" "Y = Z1 + Y2" "(X1, Z1) ∈ multpw ns"
"(X2, Z2) ∈ multpw ns" "Y2 ≠ {#}" "∀x. x ∈# Z2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
by (auto 0 3 dest!: mult_implies_one_step[OF ‹trans s›] simp: mult2_s_def elim!: multpw_splitL) metis
have "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x,y) ∈ s)"
proof (intro allI impI)
fix x assume "x ∈# X2"
then obtain X2' where "X2 = add_mset x X2'" by (metis multi_member_split)
then obtain z Z2' where "Z2 = add_mset z Z2'" "(x, z) ∈ ns" using *(4) by (auto elim: multpw_split1R)
then have "z ∈# Z2" "(x, z) ∈ ns" by auto
then show "∃y. y ∈# Y2 ∧ (x,y) ∈ s" using *(6) ‹ns O s ⊆ s› by blast
qed
then show ?R using * by auto
qed
lemma mult2_ns_one_step:
assumes "ns O s ⊆ s" "refl ns" "trans s"
shows "(X, Y) ∈ mult2_ns ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))" (is "?L ⟷ ?R")
proof
assume ?L then consider "(X, Y) ∈ multpw ns" | "(X, Y) ∈ mult2_s ns s"
by (auto simp: mult2_s_def mult2_ns_def)
then show ?R using mult2_s_one_step[OF assms]
by (cases, intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
next
assume ?R then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2"
"(X1, Y1) ∈ multpw ns" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by blast
then show ?L using mult2_s_one_step[OF assms, of X Y] count_inject[of X2 "{#}"]
by (cases "Y2 = {#}") (auto simp: mult2_s_def mult2_ns_def)
qed
lemma mult2_s_locally_one_step':
assumes "ns O s ⊆ s" "refl ns" "locally_irrefl s X" "locally_irrefl s Y" "trans s"
shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ mult s)" (is "?L ⟷ ?R")
proof
assume ?L then show ?R unfolding mult2_s_one_step[OF assms(1,2,5)]
using one_step_implies_mult[of _ _ s "{#}"] by auto metis
next
assume ?R then obtain X1 X2 Y1 Y2 where x: "X = X1 + X2" and y: "Y = Y1 + Y2" and
ns: "(X1, Y1) ∈ multpw ns" and s: "(X2, Y2) ∈ mult s" by blast
then have l: "locally_irrefl s (X2 + Y1)" and r: "locally_irrefl s (Y2 + Y1)"
using assms(3, 4) by (auto simp add: locally_irrefl_def)
show ?L using ns s mult_locally_cancelL[OF assms(5) l r] multpw_add[OF ns, of X2 X2] refl_multpw[OF ‹refl ns›]
unfolding mult2_s_def refl_on_def x y by auto
qed
lemma mult2_s_one_step':
assumes "ns O s ⊆ s" "refl ns" "irrefl s" "trans s"
shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ mult s)" (is "?L ⟷ ?R")
using assms mult2_s_locally_one_step' by (simp add: mult2_s_locally_one_step' irrefl_def locally_irrefl_def)
lemma mult2_ns_one_step':
assumes "ns O s ⊆ s" "refl ns" "irrefl s" "trans s"
shows "(X, Y) ∈ mult2_ns ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ (mult s)⇧=)" (is "?L ⟷ ?R")
proof -
have "(X, Y) ∈ multpw ns ⟹ ?R"
by (intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
moreover have "X = X1 + Y2 ∧ Y = Y1 + Y2 ∧ (X1, Y1) ∈ multpw ns ⟹ ?L" for X1 Y1 Y2
using multpw_add[of X1 Y1 ns Y2 Y2] refl_multpw[OF ‹refl ns›] by (auto simp: mult2_ns_def refl_on_def)
ultimately show ?thesis using mult2_s_one_step'[OF assms] unfolding mult2_ns_conv
by auto blast
qed
subsection ‹Cancellation›
lemma mult2_s_locally_cancel1:
assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "locally_irrefl s (add_mset z X)" "locally_irrefl s (add_mset z Y)" "trans s"
"(add_mset z X, add_mset z Y) ∈ mult2_s ns s"
shows "(X, Y) ∈ mult2_s ns s"
proof -
obtain X1 X2 Y1 Y2 where *: "add_mset z X = X1 + X2" "add_mset z Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
"(X2, Y2) ∈ mult s" using assms(8) unfolding mult2_s_locally_one_step'[OF assms(2,3,5,6,7)] by blast
from union_single_eq_member[OF this(1)] union_single_eq_member[OF this(2)] multi_member_split
consider X1' where "X1 = add_mset z X1'" | Y1' where "Y1 = add_mset z Y1'"
| X2' Y2' where "X2 = add_mset z X2'" "Y2 = add_mset z Y2'"
unfolding set_mset_union Un_iff by metis
then show ?thesis
proof (cases)
case 1 then obtain Y1' z' where **: "(X1', Y1') ∈ multpw ns" "Y1 = add_mset z' Y1'" "(z, z') ∈ ns"
using * by (auto elim: multpw_split1R)
then have "(X, Y1' + Y2) ∈ mult2_s ns s" using * 1
by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step')
moreover
have "(Y1' + Y2, Y) ∈ multpw ns"
using refl_multpw[OF ‹refl ns›] * ** multpw_cancel1[OF ‹trans ns› **(3), of "Y1' + Y2" Y]
by (auto simp: refl_on_def)
ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
next
case 2 then obtain X1' z' where **: "(X1', Y1') ∈ multpw ns" "X1 = add_mset z' X1'" "(z', z) ∈ ns"
using * by (auto elim: multpw_split1L)
then have "(X1' + X2, Y) ∈ mult2_s ns s" using * 2
by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step')
moreover
have "(X, X1' + X2) ∈ multpw ns"
using refl_multpw[OF ‹refl ns›] * ** multpw_cancel1[OF ‹trans ns› **(3), of X "X1' + X2"]
by (auto simp: refl_on_def)
ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
next
case 3 then show ?thesis using assms *
by (auto simp: mult2_s_locally_one_step' union_commute[of "{#_#}"] union_assoc[symmetric] mult_cancel mult_cancel_add_mset)
(metis "*"(1) "*"(2) add_mset_add_single li_trans_l li_trans_r mult2_s_locally_one_step' mult_locally_cancel)
qed
qed
lemma mult2_s_cancel1:
assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "irrefl s" "trans s" "(add_mset z X, add_mset z Y) ∈ mult2_s ns s"
shows "(X, Y) ∈ mult2_s ns s"
using assms mult2_s_locally_cancel1 by (metis irrefl_def locally_irrefl_def)
lemma mult2_s_locally_cancel:
assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)" "trans s"
shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_s ns s"
using assms(5, 6)
proof (induct Z)
case (add z Z) then show ?case
using mult2_s_locally_cancel1[OF assms(1-4), of z "X + Z" "Y + Z"]
by auto (metis add_mset_add_single assms(7) li_trans_l)
qed auto
lemma mult2_s_cancel:
assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "irrefl s" "trans s"
shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_s ns s"
using mult2_s_locally_cancel assms by (metis irrefl_def locally_irrefl_def)
lemma mult2_ns_cancel:
assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans s" "irrefl s" "trans ns"
shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_ns ns s"
unfolding mult2_ns_conv using assms mult2_s_cancel multpw_cancel by blast
subsection ‹Implementation friendly versions of @{const mult2_s} and @{const mult2_ns}›
definition mult2_alt :: "bool ⇒ 'a rel ⇒ 'a rel ⇒ 'a multiset rel" where
"mult2_alt b ns s = {(X, Y). (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw ns ∧ (b ∨ Y2 ≠ {#}) ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))}"
lemma mult2_altI:
assumes "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
"b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
shows "(X, Y) ∈ mult2_alt b ns s"
using assms unfolding mult2_alt_def by blast
lemma mult2_altE:
assumes "(X, Y) ∈ mult2_alt b ns s"
obtains X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
"b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
using assms unfolding mult2_alt_def by blast
lemma mono_mult2_alt:
assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_alt b ns s ⊆ mult2_alt b ns' s'"
unfolding mult2_alt_def using mono_multpw[OF assms(1)] assms by (blast 19)
abbreviation "mult2_alt_s ≡ mult2_alt False"
abbreviation "mult2_alt_ns ≡ mult2_alt True"
lemmas mult2_alt_s_def = mult2_alt_def[where b = False, unfolded simp_thms]
lemmas mult2_alt_ns_def = mult2_alt_def[where b = True, unfolded simp_thms]
lemmas mult2_alt_sI = mult2_altI[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsI = mult2_altI[where b = True, unfolded simp_thms True_implies_equals]
lemmas mult2_alt_sE = mult2_altE[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsE = mult2_altE[where b = True, unfolded simp_thms True_implies_equals]
paragraph ‹Equivalence to @{const mult2_s} and @{const mult2_ns}›
lemma mult2_s_eq_mult2_s_alt:
assumes "ns O s ⊆ s" "refl ns" "trans s"
shows "mult2_alt_s ns s = mult2_s ns s"
using mult2_s_one_step[OF assms] unfolding mult2_alt_s_def by blast
lemma mult2_ns_eq_mult2_ns_alt:
assumes "ns O s ⊆ s" "refl ns" "trans s"
shows "mult2_alt_ns ns s = mult2_ns ns s"
using mult2_ns_one_step[OF assms] unfolding mult2_alt_ns_def by blast
lemma mult2_alt_local:
assumes "(X, Y) ∈ mult2_alt b ns s"
shows "(X, Y) ∈ mult2_alt b (ns ∩ set_mset X × set_mset Y) (s ∩ set_mset X × set_mset Y)"
proof -
from assms obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" and
"(X1, Y1) ∈ multpw ns" "(b ∨ Y2 ≠ {#})" "(∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s))"
unfolding mult2_alt_def by blast
then have "X = X1 + X2 ∧ Y = Y1 + Y2 ∧
(X1, Y1) ∈ multpw (ns ∩ set_mset X × set_mset Y) ∧ (b ∨ Y2 ≠ {#}) ∧
(∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s ∩ set_mset X × set_mset Y))"
using multpw_local[of X1 Y1 ns]
mono_multpw[of "ns ∩ set_mset X1 × set_mset Y1" "ns ∩ set_mset X × set_mset Y"] assms
unfolding * set_mset_union unfolding set_mset_def by blast
then show ?thesis unfolding mult2_alt_def by blast
qed
subsection ‹Local well-foundedness: restriction to downward closure of a set›
definition wf_below :: "'a rel ⇒ 'a set ⇒ bool" where
"wf_below r A = wf (Restr r ((r⇧*)¯ `` A))"
lemma wf_below_UNIV[simp]:
shows "wf_below r UNIV ⟷ wf r"
by (auto simp: wf_below_def rtrancl_converse[symmetric] Image_closed_trancl[OF subset_UNIV])
lemma wf_below_mono1:
assumes "r ⊆ r'" "wf_below r' A" shows "wf_below r A"
using assms unfolding wf_below_def
by (intro wf_subset[OF assms(2)[unfolded wf_below_def]] Int_mono Sigma_mono Image_mono
iffD2[OF converse_mono] rtrancl_mono subset_refl)
lemma wf_below_mono2:
assumes "A ⊆ A'" "wf_below r A'" shows "wf_below r A"
using assms unfolding wf_below_def
by (intro wf_subset[OF assms(2)[unfolded wf_below_def]]) blast
lemma wf_below_pointwise:
"wf_below r A ⟷ (∀a. a ∈ A ⟶ wf_below r {a})" (is "?L ⟷ ?R")
proof
assume ?L then show ?R using wf_below_mono2[of "{_}" A r] by blast
next
have *: "(r⇧*)¯ `` A = ⋃{(r⇧*)¯ `` {a} |a. a ∈ A}" unfolding Image_def by blast
assume ?R
{ fix x X assume *: "X ⊆ Restr r ((r⇧*)¯ `` A) `` X" "x ∈ X"
then obtain a where **: "a ∈ A" "(x, a) ∈ r⇧*" unfolding Image_def by blast
from * have "X ∩ ((r⇧*)¯ `` {a}) ⊆ (Restr r ((r⇧*)¯ `` A) `` X) ∩ ((r⇧*)¯ `` {a})" by auto
also have "... ⊆ Restr r ((r⇧*)¯ `` {a}) `` (X ∩ ((r⇧*)¯ `` {a}))" unfolding Image_def by fastforce
finally have "X ∩ ((r⇧*)¯ `` {a}) = {}" using ‹?R› **(1) unfolding wf_below_def
by (intro wfE_pf[of "Restr r ((r⇧*)¯ `` {a})"]) (auto simp: Image_def)
then have False using *(2) ** unfolding Image_def by blast
}
then show ?L unfolding wf_below_def by (intro wfI_pf) auto
qed
lemma SN_on_Image_rtrancl_conv:
"SN_on r A ⟷ SN_on r (r⇧* `` A)" (is "?L ⟷ ?R")
proof
assume ?L then show ?R by (auto simp: SN_on_Image_rtrancl)
next
assume ?R then show ?L by (auto simp: SN_on_def)
qed
lemma SN_on_iff_wf_below:
"SN_on r A ⟷ wf_below (r¯) A"
proof -
{ fix f
assume "f 0 ∈ r⇧* `` A" and **: "(f i, f (Suc i)) ∈ r" for i
then have "f i ∈ r⇧* `` A" for i
by (induct i) (auto simp: Image_def, metis UnCI relcomp.relcompI rtrancl_unfold)
then have "(f i, f (Suc i)) ∈ Restr r (r⇧* `` A)" for i using ** by auto
}
moreover then have "SN_on r (r⇧* `` A) ⟷ SN_on (Restr r (r⇧* `` A)) (r⇧* `` A)"
unfolding SN_on_def by auto blast
moreover have "(⋀i. (f i, f (Suc i)) ∈ Restr r (r⇧* `` A)) ⟹ f 0 ∈ r⇧* `` A" for f by auto
then have "SN_on (Restr r (r⇧* `` A)) (r⇧* `` A) ⟷ SN_on (Restr r (r⇧* `` A)) UNIV"
unfolding SN_on_def by auto
ultimately show ?thesis unfolding SN_on_Image_rtrancl_conv [of _ A]
by (simp add: wf_below_def SN_iff_wf rtrancl_converse converse_Int converse_Times)
qed
lemma restr_trancl_under:
shows "Restr (r⇧+) ((r⇧*)¯ `` A) = (Restr r ((r⇧*)¯ `` A))⇧+"
proof (intro equalityI subrelI, elim IntE conjE[OF iffD1[OF mem_Sigma_iff]])
fix a b assume *: "(a, b) ∈ r⇧+" "b ∈ (r⇧*)¯ `` A"
then have "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+ ∧ a ∈ (r⇧*)¯ `` A"
proof (induct rule: trancl_trans_induct[consumes 1])
case 1 then show ?case by (auto simp: Image_def intro: converse_rtrancl_into_rtrancl)
next
case 2 then show ?case by (auto simp del: Int_iff del: ImageE)
qed
then show "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+" by simp
next
fix a b assume "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+"
then show "(a, b) : Restr (r⇧+) ((r⇧*)¯ `` A)" by induct auto
qed
lemma wf_below_trancl:
shows "wf_below (r⇧+) A ⟷ wf_below r A"
using restr_trancl_under[of r A] by (simp add: wf_below_def wf_trancl_conv)
lemma wf_below_mult_local:
assumes "wf_below r (set_mset X)" shows "wf_below (mult r) {X}"
proof -
have foo: "mult r ⊆ mult (r⇧+)" using mono_mult[of r "r⇧+"] by force
have "(Y, X) ∈ (mult (r⇧+))⇧* ⟹ set_mset Y ⊆ ((r⇧+)⇧*)¯ `` set_mset X" for Y
proof (induct rule: converse_rtrancl_induct)
case (step Z Y)
obtain I J K where *: "Y = I + J" "Z = I + K" "(∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ r⇧+)"
using mult_implies_one_step[OF _ step(1)] by auto
{ fix k assume "k ∈# K"
then obtain j where "j ∈# J" "(k, j) ∈ r⇧+" using *(3) by auto
moreover then obtain x where "x ∈# X" "(j, x) ∈ r⇧*" using step(3) by (auto simp: *)
ultimately have "∃x. x ∈# X ∧ (k, x) ∈ r⇧*" by auto
}
then show ?case using * step(3) by (auto simp: Image_def) metis
qed auto
then have q: "(Y, X) ∈ (mult (r⇧+))⇧* ⟹ y ∈# Y ⟹ y ∈ ((r⇧+)⇧*)¯ `` set_mset X" for Y y by force
have "Restr (mult (r⇧+)) (((mult (r⇧+))⇧*)¯ `` {X}) ⊆ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
proof (intro subrelI)
fix N M assume "(N, M) ∈ Restr (mult (r⇧+)) (((mult (r⇧+))⇧*)¯ `` {X})"
then have **: "(N, X) ∈ (mult (r⇧+))⇧*" "(M, X) ∈ (mult (r⇧+))⇧*" "(N, M) ∈ mult (r⇧+)" by auto
obtain I J K where *: "M = I + J" "N = I + K" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ r⇧+"
using mult_implies_one_step[OF _ ‹(N, M) ∈ mult (r⇧+)›] by auto
then show "(N, M) ∈ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
using q[OF **(1)] q[OF **(2)] unfolding * by (auto intro: one_step_implies_mult)
qed
note bar = subset_trans[OF Int_mono[OF foo Sigma_mono] this]
have "((mult r)⇧*)¯ `` {X} ⊆ ((mult (r⇧+))⇧*)¯ `` {X}" using foo by (simp add: Image_mono rtrancl_mono)
then have "Restr (mult r) (((mult r)⇧*)¯ `` {X}) ⊆ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
by (intro bar) auto
then show ?thesis using wf_mult assms wf_subset
unfolding wf_below_trancl[of r, symmetric] unfolding wf_below_def by blast
qed
lemma qc_wf_below:
assumes "s O ns ⊆ (s ∪ ns)⇧* O s" "wf_below s A"
shows "wf_below (ns⇧* O s O ns⇧*) A"
unfolding wf_below_def
proof (intro wfI_pf)
let ?A' = "((ns⇧* O s O ns⇧*)⇧*)¯ `` A"
fix X assume X: "X ⊆ Restr (ns⇧* O s O ns⇧*) ?A' `` X"
let ?X' = "((s ∪ ns)⇧* ∩ UNIV × ((s⇧*)¯ `` A)) `` X"
have *: "s O (s ∪ ns)⇧* ⊆ (s ∪ ns)⇧* O s"
proof -
{ fix x y z assume "(y, z) ∈ (s ∪ ns)⇧*" and "(x, y) ∈ s"
then have "(x, z) ∈ (s ∪ ns)⇧* O s"
proof (induct y z)
case rtrancl_refl then show ?case by auto
next
case (rtrancl_into_rtrancl a b c)
then have "(x, c) ∈ ((s ∪ ns)⇧* O (s ∪ ns)⇧*) O s" using assms by blast
then show ?case by simp
qed }
then show ?thesis by auto
qed
{ fix x assume "x ∈ Restr (ns⇧* O s O ns⇧*) ?A' `` X"
then obtain y z where **: "y ∈ X" "z ∈ A" "(y, x) ∈ ns⇧* O s O ns⇧*" "(x, z) ∈ (ns⇧* O s O ns⇧*)⇧*" by blast
have "(ns⇧* O s O ns⇧*) O (ns⇧* O s O ns⇧*)⇧* ⊆ (s ∪ ns)⇧*" by regexp
then have "(y, z) ∈ (s ∪ ns)⇧*" using **(3,4) by blast
moreover have "?X' = {}"
proof (intro wfE_pf[OF assms(2)[unfolded wf_below_def]] subsetI)
fix x assume "x ∈ ?X'"
then have "x ∈ ((s ∪ ns)⇧* ∩ UNIV × ((s⇧*)¯ `` A)) `` Restr (ns⇧* O s O ns⇧*) ?A' `` X" using X by auto
then obtain x0 y z where **: "z ∈ X" "x0 ∈ A" "(z, y) ∈ ns⇧* O s O ns⇧*" "(y, x) ∈ (s ∪ ns)⇧*" "(x, x0) ∈ s⇧*"
unfolding Image_def by blast
have "(ns⇧* O s O ns⇧*) O (s ∪ ns)⇧* ⊆ ns⇧* O (s O (s ∪ ns)⇧*)" by regexp
with **(3,4) have "(z, x) ∈ ns⇧* O (s O (s ∪ ns)⇧*)" by blast
moreover have "ns⇧* O ((s ∪ ns)⇧* O s) ⊆ (s ∪ ns)⇧* O s" by regexp
ultimately have "(z, x) ∈ (s ∪ ns)⇧* O s" using * by blast
then obtain x' where "z ∈ X" "(z, x') ∈ (s ∪ ns)⇧*" "(x', x) ∈ s" "(x', x0) ∈ s⇧*" "(x, x0) ∈ s⇧*" "x0 ∈ A"
using **(1,2,5) converse_rtrancl_into_rtrancl[OF _ **(5)] by blast
then show "x ∈ Restr s ((s⇧*)¯ `` A) `` ?X'"
unfolding Image_def by blast
qed
ultimately have False using **(1,2) unfolding Image_def by blast
}
then show "X = {}" using X by blast
qed
lemma wf_below_mult2_s_local:
assumes "wf_below s (set_mset X)" "s O ns ⊆ s" "refl ns" "trans ns"
shows "wf_below (mult2_s ns s) {X}"
using wf_below_mult_local[of s X] assms multpw_mult_commute[of s ns]
wf_below_mono1[of "multpw ns O mult s" "(multpw ns)⇧* O mult s O (multpw ns)⇧*" "{X}"]
qc_wf_below[of "mult s" "multpw ns" "{X}"]
unfolding mult2_s_def by blast
subsection ‹Trivial cases›
lemma mult2_alt_emptyL:
"({#}, Y) ∈ mult2_alt b ns s ⟷ b ∨ Y ≠ {#}"
unfolding mult2_alt_def by auto
lemma mult2_alt_emptyR:
"(X, {#}) ∈ mult2_alt b ns s ⟷ b ∧ X = {#}"
unfolding mult2_alt_def by (auto intro: multiset_eqI)
lemma mult2_alt_s_single:
"(a, b) ∈ s ⟹ ({#a#}, {#b#}) ∈ mult2_alt_s ns s"
using mult2_altI[of _ "{#}" _ _ "{#}" _ ns False s] by auto
lemma multpw_implies_mult2_alt_ns:
assumes "(X, Y) ∈ multpw ns"
shows "(X, Y) ∈ mult2_alt_ns ns s"
using assms by (intro mult2_alt_nsI[of X X "{#}" Y Y "{#}"]) auto
lemma mult2_alt_ns_conv:
"mult2_alt_ns ns s = mult2_alt_s ns s ∪ multpw ns" (is "?l = ?r")
proof (intro equalityI subrelI)
fix X Y assume "(X, Y) ∈ ?l"
thm mult2_alt_nsE
then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
"∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by (auto elim: mult2_alt_nsE)
then show "(X, Y) ∈ ?r" using count_inject[of X2 "{#}"]
by (cases "Y2 = {#}") (auto intro: mult2_alt_sI elim: mult2_alt_nsE mult2_alt_sE)
next
fix X Y assume "(X, Y) ∈ ?r" then show "(X, Y) ∈ ?l"
by (auto intro: mult2_alt_nsI multpw_implies_mult2_alt_ns elim: mult2_alt_sE)
qed
lemma mult2_alt_s_implies_mult2_alt_ns:
assumes "(X, Y) ∈ mult2_alt_s ns s"
shows "(X, Y) ∈ mult2_alt_ns ns s"
using assms by (auto intro: mult2_alt_nsI elim: mult2_alt_sE)
lemma mult2_alt_add:
assumes "(X1, Y1) ∈ mult2_alt b1 ns s" and "(X2, Y2) ∈ mult2_alt b2 ns s"
shows "(X1 + X2, Y1 + Y2) ∈ mult2_alt (b1 ∧ b2) ns s"
proof -
from assms obtain X11 X12 Y11 Y12 X21 X22 Y21 Y22 where
"X1 = X11 + X12" "Y1 = Y11 + Y12"
"(X11, Y11) ∈ multpw ns" "(b1 ∨ Y12 ≠ {#})" "(∀x. x ∈# X12 ⟶ (∃y. y ∈# Y12 ∧ (x, y) ∈ s))"
"X2 = X21 + X22" "Y2 = Y21 + Y22"
"(X21, Y21) ∈ multpw ns" "(b2 ∨ Y22 ≠ {#})" "(∀x. x ∈# X22 ⟶ (∃y. y ∈# Y22 ∧ (x, y) ∈ s))"
unfolding mult2_alt_def by (blast 9)
then show ?thesis
by (intro mult2_altI[of _ "X11 + X21" "X12 + X22" _ "Y11 + Y21" "Y12 + Y22"])
(auto intro: multpw_add simp: ac_simps)
qed
lemmas mult2_alt_s_s_add = mult2_alt_add[of _ _ False _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_ns_s_add = mult2_alt_add[of _ _ True _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_s_ns_add = mult2_alt_add[of _ _ False _ _ _ _ True, unfolded simp_thms]
lemmas mult2_alt_ns_ns_add = mult2_alt_add[of _ _ True _ _ _ _ True, unfolded simp_thms]
lemma multpw_map:
assumes "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ ns ⟹ (f x, g y) ∈ ns'"
and "(X, Y) ∈ multpw ns"
shows "(image_mset f X, image_mset g Y) ∈ multpw ns'"
using assms(2,1) by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)
lemma mult2_alt_map:
assumes "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ ns ⟹ (f x, g y) ∈ ns'"
and "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ s ⟹ (f x, g y) ∈ s'"
and "(X, Y) ∈ mult2_alt b ns s"
shows "(image_mset f X, image_mset g Y) ∈ mult2_alt b ns' s'"
proof -
from assms(3) obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
"b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by (auto elim: mult2_altE)
moreover from this(1,2,5) have "∀x. x ∈# image_mset f X2 ⟶ (∃y. y ∈# image_mset g Y2 ∧ (x, y) ∈ s')"
using assms(2) by (simp add: in_image_mset image_iff) blast
ultimately show ?thesis using assms multpw_map[of X1 Y1 ns f g]
by (intro mult2_altI[of _ "image_mset f X1" "image_mset f X2" _ "image_mset g Y1" "image_mset g Y2"]) auto
qed
text ‹Local transitivity of @{const mult2_alt}›
lemma trans_mult2_alt_local:
assumes ss: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ s ⟹ (y, z) ∈ s ⟹ (x, z) ∈ s"
and ns: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ ns ⟹ (y, z) ∈ s ⟹ (x, z) ∈ s"
and sn: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ s ⟹ (y, z) ∈ ns ⟹ (x, z) ∈ s"
and nn: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ ns ⟹ (y, z) ∈ ns ⟹ (x, z) ∈ ns"
and xyz: "(X, Y) ∈ mult2_alt b1 ns s" "(Y, Z) ∈ mult2_alt b2 ns s"
shows "(X, Z) ∈ mult2_alt (b1 ∧ b2) ns s"
proof -
let ?a1 = Enum.finite_3.a⇩1 and ?a2 = Enum.finite_3.a⇩2 and ?a3 = Enum.finite_3.a⇩3
let ?t = "{(?a1, ?a2), (?a1, ?a3), (?a2, ?a3)}"
let ?A = "{(?a1, x) |x. x ∈# X} ∪ {(?a2, y) |y. y ∈# Y} ∪ {(?a3, z) |z. z ∈# Z}"
define s' where "s' = Restr {((a, x), (b, y)) |a x b y. (a, b) ∈ ?t ∧ (x, y) ∈ s} ?A"
define ns' where "ns' = (Restr {((a, x), (b, y)) |a x b y. (a, b) ∈ ?t ∧ (x, y) ∈ ns} ?A)⇧="
have *: "refl ns'" "trans ns'" "trans s'" "s' O ns' ⊆ s'" "ns' O s' ⊆ s'"
by (force simp: trans_def ss ns sn nn s'_def ns'_def)+
have "({#(?a1, x). x ∈# X#}, {#(?a2, y). y ∈# Y#}) ∈ mult2_alt b1 ns' s'"
by (auto intro: mult2_alt_map[OF _ _ xyz(1)] simp: s'_def ns'_def)
moreover have "({#(?a2, y). y ∈# Y#}, {#(?a3, z). z ∈# Z#}) ∈ mult2_alt b2 ns' s'"
by (auto intro: mult2_alt_map[OF _ _ xyz(2)] simp: s'_def ns'_def)
ultimately have "({#(?a1, x). x ∈# X#}, {#(?a3, z). z ∈# Z#}) ∈ mult2_alt (b1 ∧ b2) ns' s'"
using mult2_s_eq_mult2_s_alt[OF *(5,1,3)] mult2_ns_eq_mult2_ns_alt[OF *(5,1,3)]
trans_mult2_s[OF *(4,1,2)] trans_mult2_ns[OF *(4,1,2)] compat_mult2[OF *(4,1,2)]
by (cases b1; cases b2) (auto simp: trans_O_iff)
from mult2_alt_map[OF _ _ this, of snd snd ns s]
show ?thesis by (auto simp: s'_def ns'_def image_mset.compositionality comp_def in_image_mset image_iff)
qed
lemmas trans_mult2_alt_s_s_local = trans_mult2_alt_local[of _ _ _ _ _ False False, unfolded simp_thms]
lemmas trans_mult2_alt_ns_s_local = trans_mult2_alt_local[of _ _ _ _ _ True False, unfolded simp_thms]
lemmas trans_mult2_alt_s_ns_local = trans_mult2_alt_local[of _ _ _ _ _ False True, unfolded simp_thms]
lemmas trans_mult2_alt_ns_ns_local = trans_mult2_alt_local[of _ _ _ _ _ True True, unfolded simp_thms]
end