theory Multiset_Extension_Pair
imports "~~/src/HOL/Library/Multiset" "$AFP/Regular-Sets/Regexp_Method"
begin
section ‹Surely this must exist somewhere›
lemma trans_subset_iff:
"trans r ⟷ r O r ⊆ r"
unfolding trans_def by blast
lemma mult_cancelL:
assumes "trans s" "irrefl s" shows "(Z + X, Z + Y) ∈ mult s ⟷ (X, Y) ∈ mult s"
using mult_cancel[OF assms, of X Z Y] by (simp only: union_commute)
lemma wf_trancl_conv:
shows "wf (r⇧+) ⟷ wf r"
using wf_subset[of "r⇧+" r] by (force simp: wf_trancl)
section ‹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)
thus ?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
thus ?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)
thus ?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)
thus ?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) thus ?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') thus ?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))
thus ?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 trans_multpw:
assumes "trans ns" shows "trans (multpw ns)"
proof -
have "(X, Y) ∈ multpw ns ⟹ (Y, Z) ∈ multpw ns ⟹ (X, Z) ∈ multpw ns" for X Y Z
proof (induct X Y arbitrary: Z rule: multpw.induct)
case (add x y X Y) thus ?case using transD[OF assms, of x y]
by (auto 0 3 intro: multpw.intros elim: multpw_split1R)
qed simp
thus ?thesis by (metis trans_def)
qed
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)
}
thus ?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"
hence "∃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)
}
thus ?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])
thus ?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)
thus ?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 thus ?R
proof (induct Z)
case (add z Z) thus ?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 thus ?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)
section ‹Multiset extension for order pairs›
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_subset_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_subset_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_subset_iff by (blast 8)+
subsection ‹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›
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
hence "(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
thus "∃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)
thus ?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
thus ?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_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")
proof
assume ?L thus ?R unfolding mult2_s_one_step[OF assms(1,2,4)]
using one_step_implies_mult[of _ _ s "{#}"] by auto metis
next
assume ?R then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2"
"(X1, Y1) ∈ multpw ns" "(X2, Y2) ∈ mult s" by blast
thus ?L using mult_cancelL[OF assms(4,3)] multpw_add refl_multpw[OF `refl ns`]
unfolding mult2_s_def refl_on_def by blast
qed
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›
lemmas mult_cancel1 = mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right empty_neutral]
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"
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(7) unfolding mult2_s_one_step'[OF assms(2,3,5,6)] 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
thus ?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 simp: mult2_s_one_step'[OF assms(2,3,5,6)])
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 simp: mult2_s_one_step'[OF assms(2,3,5,6)])
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 thus ?thesis using assms *
by (auto simp: mult2_s_one_step' union_commute[of "{#_#}"] union_assoc[symmetric] mult_cancel mult_cancel1)
qed
qed
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"
proof (induct Z)
case (add z Z) thus ?case
using mult2_s_cancel1[OF assms, of z "X + Z" "Y + Z"] by auto
qed auto
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
section ‹Local well-founded-ness: 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 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 thus ?case by (auto simp: Image_def intro: converse_rtrancl_into_rtrancl)
next
case 2 thus ?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})"
hence **: "(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 fast
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 ‹Implementation friendly versions of @{term mult2_s} and @{term 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]
subsubsection ‹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
thus ?thesis unfolding mult2_alt_def by blast
qed
subsubsection ‹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)
thus "(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" thus "(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]
text ‹Congruences?›
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 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}"
def s' ≡ "Restr {((a, x), (b, y)) |a x b y. (a, b) ∈ ?t ∧ (x, y) ∈ s} ?A"
def 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_subset_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