section ‹Peak Decreasingness›
theory Peak_Decreasingness
imports
"Abstract-Rewriting.Abstract_Rewriting"
"Well_Quasi_Orders.Multiset_Extension"
QTRS.Util
begin
lemma SN_mulex: "SN {(x, y). P x y} ⟹ SN {(x, y). mulex P¯¯ y x}"
using wfp_on_mulex_on_multisets [of "P¯¯" UNIV]
by (auto simp: wfP_def SN_iff_wf converse_def)
text ‹ARSs whose relation is the union of an indexed set of relations.›
locale ars_labeled =
fixes r :: "'a ⇒ 'b rel"
and I :: "'a set"
begin
abbreviation "R ≡ (⋃a∈I. r a)"
inductive conv where
empty [simp, intro!]: "conv {#} x x" |
step [intro]: "a ∈ I ⟹ (x, y) ∈ (r a)⇧↔ ⟹ conv M y z ⟹ conv (add_mset a M) x z"
lemma conv_in_I [simp, dest]:
"conv M x y ⟹ set_mset M ⊆ I"
by (induct rule: conv.induct) simp_all
lemma conversion_conv_iff:
assumes "A ⊆ I"
shows "(x, y) ∈ (⋃a∈A. r a)⇧↔⇧* ⟷ (∃M. set_mset M ⊆ A ∧ conv M x y)"
(is "_ ∈ ?R⇧↔⇧* ⟷ _")
proof
assume "(x, y) ∈ ?R⇧↔⇧*"
then have "(x, y) ∈ (?R ∪ ?R¯)⇧*" by auto
then show "∃M. set_mset M ⊆ A ∧ conv M x y"
proof (induct rule: converse_rtrancl_induct)
case (step w x)
moreover then obtain a and M where "a ∈ A" and "(w, x) ∈ (r a)⇧↔"
and "set_mset M ⊆ A" and "conv M x y" by blast
ultimately show ?case using assms by (intro exI [of _ "M + {#a#}"]) auto
qed (auto intro: exI [of _ "{#}"])
next
assume "∃M. set_mset M ⊆ A ∧ conv M x y"
then obtain M where "conv M x y" and "set_mset M ⊆ A" by auto
then show "(x, y) ∈ ?R⇧↔⇧*"
by (induct) (auto simp: conversion_def intro: converse_rtrancl_into_rtrancl)
qed
lemma conversion_R_conv_iff: "(x, y) ∈ R⇧↔⇧* ⟷ (∃M. set_mset M ⊆ I ∧ conv M x y)"
using conversion_conv_iff[OF subset_refl] .
lemma conv_singleton [intro]:
"a ∈ I ⟹ (x, y) ∈ (r a)⇧↔ ⟹ conv {#a#} x y"
by (metis conv.empty conv.step empty_neutral(1))
lemma conv_step' [intro, simp]:
assumes "a ∈ I" and "(y, z) ∈ (r a)⇧↔" and "conv M x y"
shows "conv (add_mset a M) x z"
using assms (3, 2, 1) by (induct) (auto simp: add_mset_commute)
lemma conv_trans:
assumes "conv M x y" and "conv N y z"
shows "conv (M + N) x z"
using assms(2, 1)
apply (induct arbitrary: M)
apply (auto simp: ac_simps)
apply (metis UnCI conv_step' union_mset_add_mset_right)
by (metis UnCI conv_step' converse_iff union_mset_add_mset_right)
lemma conv_commute:
assumes "conv M x y" shows "conv M y x"
using assms by (induct) auto
inductive seql where
empty [simp, intro!]: "seql {#} x x" |
step [intro]: "a ∈ I ⟹ (z, y) ∈ r a ⟹ seql M x y ⟹ seql (add_mset a M) x z"
lemma rtrancl_seql_iff:
"(x, y) ∈ R⇧* ⟷ (∃M. seql M y x)"
proof
assume "(x, y) ∈ R⇧*"
then show "∃M. seql M y x"
by (induct rule: converse_rtrancl_induct) (auto)
next
assume "∃M. seql M y x"
then obtain M where "seql M y x" ..
then show "(x, y) ∈ R⇧*"
by (induct) (auto simp: rtrancl_converse intro: converse_rtrancl_into_rtrancl)
qed
lemma seql_singleton [intro]:
"a ∈ I ⟹ (x, y) ∈ r a ⟹ seql {#a#} y x"
by (metis empty_neutral(1) seql.empty seql.step)
lemma seql_imp_conv:
assumes "seql M x y" shows "conv M x y"
using assms by (induct) auto
lemma seql_add_mset [simp]:
"a ∈ I ⟹ (z, y) ∈ r a ⟹ seql M x y ⟹ seql (add_mset a M) x z"
by auto
lemma seql_left' [intro]:
assumes "a ∈ I" and "(y, x) ∈ r a" and "seql M y z"
shows "seql (add_mset a M) x z"
using assms(3, 2, 1) by (induct) (auto simp: add_mset_commute)
inductive valley where
seql [simp, intro]: "seql M x y ⟹ valley M x y" |
left [intro]: "⟦a ∈ I; (x, y) ∈ r a; valley M y z⟧ ⟹ valley (add_mset a M) x z"
lemma join_valley_iff:
"(x, y) ∈ R⇧↓ ⟷ (∃M. valley M x y)"
proof
assume "(x, y) ∈ R⇧↓"
then obtain z where "(x, z) ∈ R⇧*" and "(y, z) ∈ R⇧*" by auto
then obtain N where "(x, z) ∈ R⇧*" and "seql N z y" by (auto simp: rtrancl_seql_iff)
then show "∃M. valley M x y"
by (induct arbitrary: y rule: converse_rtrancl_induct)
(auto dest: valley.left)
next
assume "∃M. valley M x y"
then obtain M where "valley M x y" by auto
then show "(x, y) ∈ R⇧↓"
by (induct) (auto iff: rtrancl_seql_iff intro: rtrancl_join_join)
qed
lemma valley_imp_conv:
assumes "valley M x y" shows "conv M x y"
using assms by (induct) (auto intro: seql_imp_conv)
text ‹A conversion is either a valley or contains a peak.›
lemma conv_valley_peak_cases:
assumes "conv M x y"
obtains
(valley) "valley M x y" |
(peak) K L a b t u v
where "M = K + L + {#a, b#}"
and "conv K x t"
and "a ∈ I" and "(u, t) ∈ r a"
and "b ∈ I" and "(u, v) ∈ r b"
and "conv L v y"
using assms
proof (induct)
case (empty x) then show ?case by auto
next
case (step a x y M z)
show ?case
proof (rule step.hyps)
assume *: "valley M y z"
from ‹(x, y) ∈ (r a)⇧↔› show ?thesis
proof
assume "(x, y) ∈ r a"
with * and ‹a ∈ I› have "valley (add_mset a M) x z" by auto
then show ?thesis by fact
next
assume "(x, y) ∈ (r a)¯"
then have "(y, x) ∈ r a" by simp
from * show ?thesis
proof (cases)
assume "seql M y z"
then have "valley (add_mset a M) x z" using step by blast
then show ?thesis by fact
next
fix b u N
assume "b ∈ I" and "(y, u) ∈ r b"
and [simp]: "M = add_mset b N"
and "valley N u z"
then have *: "M - {#b#} = N" by simp
have "add_mset a M = {#} + (M - {#b#}) + {#a, b#}" by (simp add: ac_simps)
moreover have "conv {#} x x" by blast
moreover have "a ∈ I" and "(y, x) ∈ r a" by fact+
moreover have "b ∈ I" and "(y, u) ∈ r b" by fact+
moreover have "conv (M - {#b#}) u z"
unfolding * by (rule valley_imp_conv) fact
ultimately show ?thesis by fact
qed
qed
next
fix K L b c t u v
assume [simp]: "M = K + L + {#b, c#}"
and "conv K y t" and "b ∈ I" and "(u, t) ∈ r b"
and "c ∈ I" and "(u, v) ∈ r c" and "conv L v z"
moreover with step have "conv (add_mset a K) x t" by blast
moreover have "add_mset a M = add_mset a K + L + {#b, c#}" by (auto simp: ac_simps)
show ?thesis by (rule step.prems) fact+
qed
qed
end
text ‹ARSs as unions of relations over an index set equipped with a well-founded order.›
locale ars_labeled_sn = ars_labeled +
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "≻" 50)
assumes SN_less: "SN {(x, y). x ≻ y}"
begin
abbreviation label_less_set ("{≻}")
where
"{≻} ≡ {(x, y). x ≻ y}"
definition mless :: "'a multiset ⇒ 'a multiset ⇒ bool" (infix "≻⇩M" 50) where
"x ≻⇩M y ⟷ mulex (op ≻)¯¯ y x"
abbreviation mlesseq (infix "≽⇩M" 50) where
"x ≽⇩M y ≡ mless⇧=⇧= x y"
lemma SN_mless: "SN {(x, y). x ≻⇩M y}"
using SN_mulex [OF SN_less] by (auto simp: SN_defs mless_def)
lemma mless_mono:
"M ≻⇩M N ⟹ K + M ≻⇩M K + N"
unfolding mless_def by (metis UNIV_I mulex_on_union multisets_UNIV)
lemma mless_trans:
"as ≻⇩M bs ⟹ bs ≻⇩M cs ⟹ as ≻⇩M cs"
unfolding mless_def by (metis mulex_on_trans)
lemma mless_empty [simp]:
"M ≠ {#} ⟹ M ≻⇩M {#}"
by (auto simp: mless_def)
lemma mless_all_strict:
"M ≠ {#} ⟹ ∀y. y ∈# N ⟶ (∃x. x ∈# M ∧ x ≻ y) ⟹ M ≻⇩M N"
using mulex_on_all_strict [of M UNIV N "op ≻¯¯"] by (simp add: mless_def)
abbreviation downset1 :: "'a ⇒ 'a set" ("'(_')≻")
where
"(a)≻ ≡ {b ∈ I. a ≻ b}"
abbreviation downset2 :: "'a ⇒ 'a ⇒ 'a set" ("∨'(_,/ _')")
where
"∨(a, b) ≡ {c ∈ I. a ≻ c ∨ b ≻ c}"
lemma downset2_multiset:
assumes "∀c. c ∈# M ⟶ a ≻ c ∨ b ≻ c"
shows "{#a, b#} ≻⇩M M"
using assms
by (metis add_mset_add_single add_mset_commute add_mset_not_empty ars_labeled_sn.mless_all_strict ars_labeled_sn_axioms multi_member_this)
lemma Union_downset2_trans:
"(s, t) ∈ (⋃c∈∨(a, b). (r c))⇧↔⇧* ⟹
(t, u) ∈ (⋃c∈∨(a, b). (r c))⇧↔⇧* ⟹
(s, u) ∈ (⋃c∈∨(a, b). (r c))⇧↔⇧*"
by (auto simp: conversion_def)
lemma sym_step_in_downset2:
assumes "(s, t) ∈ (r c)⇧↔" and "c ∈ I" and "a ≻ c ∨ b ≻ c"
shows "(s, t) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*"
using assms by (auto)
lemma sym_steps_in_downset2:
assumes "(s, t) ∈ ((r c)⇧↔)⇧*" and "c ∈ I" and "a ≻ c ∨ b ≻ c"
shows "(s, t) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*"
using assms
by (induct s t, simp) (metis (mono_tags) Union_downset2_trans sym_step_in_downset2)
lemma conversion_in_downset2:
assumes "(s, t) ∈ (r c)⇧↔⇧*" and "c ∈ I" and "a ≻ c ∨ b ≻ c"
shows "(s, t) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*"
using sym_steps_in_downset2 [OF assms [unfolded conversion_def]] .
lemma downset2_conversion_imp_conv:
assumes "(t, u) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*"
shows "∃M. {#a, b#} ≻⇩M M ∧ conv M t u"
proof -
from assms [unfolded conversion_def]
have "∃M. (∀c. c ∈# M ⟶ a ≻ c ∨ b ≻ c) ∧ conv M t u"
proof (induct)
case base
show ?case
by (metis add_mset_not_empty ars_labeled.conv.empty mset_add)
next
case (step u v)
then obtain M where *: "∀c. c ∈# M ⟶ a ≻ c ∨ b ≻ c" and "conv M t u" by blast
from step(2) obtain c where "c ∈ I" and "a ≻ c ∨ b ≻ c"
and "(u, v) ∈ (r c)⇧↔" by auto
with ‹conv M t u› have "conv (add_mset c M) t v" by (metis conv_step')
moreover have "∀d. d ∈# add_mset c M ⟶ a ≻ d ∨ b ≻ d"
using * and ‹a ≻ c ∨ b ≻ c› by (auto)
ultimately show ?case by blast
qed
with downset2_multiset [of _ a b]
show ?thesis by blast
qed
end
locale ars_labelled_partially_sn = ars_labeled_sn +
fixes B :: "'a set"
assumes B_subset_I:"B ⊆ I"
begin
abbreviation downsetB :: "'a ⇒ 'a set" ("B≻'(_')")
where
"B≻(a) ≡ B ∪ {b ∈ I. a ≻ b}"
lemma aux:
assumes "⋀a x y. a ∈ A ⟹ (x, y) ∈ r a ⟹ (∃M. set_mset M ⊆ J ∧ conv M x y)"
shows "set_mset M ⊆ A ∧ conv M x y ⟹ (∃M. set_mset M ⊆ J ∧ conv M x y)"
proof-
assume conv:"set_mset M ⊆ A ∧ conv M x y"
let ?A = "⋃a∈set_mset M. r a"
from conv conversion_conv_iff[of "set_mset M"] have "(x, y) ∈ ?A⇧↔⇧*" by auto
then obtain n where "(x, y) ∈ ?A⇧↔ ^^ n" by fast
then show "∃M. set_mset M ⊆ J ∧ conv M x y" proof(induct n arbitrary:x)
case 0
hence "x=y" unfolding relpow.simps(1) by auto
then show ?case by (intro exI[of _ "{#}"]) auto
next
case (Suc n)
from relpow_Suc_D2[OF Suc(2)] obtain z where z:"(x,z) ∈ ?A⇧↔" "(z,y) ∈ ?A⇧↔ ^^ n" by blast
from symcl_Un have "?A⇧↔ = (⋃a∈set_mset M. (r a)⇧↔)" by blast
from z(1)[unfolded this UN_iff] obtain c where c:"(x, z) ∈ (r c)⇧↔" "c ∈ set_mset M" by blast
from c(1) have xz:"(x, z) ∈ r c ∨ (z, x) ∈ r c" by auto
from conv c(2) assms have step:"⋀x y.(x, y) ∈ r c ⟹ ∃M. set_mset M ⊆ J ∧ conv M x y" by blast
from xz step[of x z] step[of z x] conv_commute
obtain N1 where N1:"set_mset N1 ⊆ J" "conv N1 x z" by meson
from Suc(1)[OF z(2)] obtain N2 where N2:"set_mset N2 ⊆ J" "conv N2 z y" by auto
from N1(1) N2(1) have subset:"set_mset (N1 + N2) ⊆ J" unfolding set_mset_union by simp
from N1(2) N2(2) have "conv (N1 + N2) x y" using conv_trans by simp
with subset show ?case using conv_trans set_mset_union by blast
qed
qed
lemma conv_eq:
assumes "⋀a x y. (x, y) ∈ r a ⟹ (∃M. set_mset M ⊆ B≻(a) ∧ conv M x y)"
shows "set_mset M ⊆ I ∧ conv M x y ⟹ (∃M. set_mset M ⊆ B ∧ conv M x y)"
proof-
assume conv:"set_mset M ⊆ I ∧ conv M x y"
{ fix b x y
have "(x, y) ∈ r b ⟹ (∃M. set_mset M ⊆ B ∧ conv M x y)"
proof (induct arbitrary: x y rule:SN_induct[OF SN_less])
case (1 a)
from assms[OF 1(2)] obtain M where M:"set_mset M ⊆ B ∪ (a)≻ ∧ conv M x y" by auto
from B_subset_I have "B ∪ (a)≻ ⊆ I" by blast
from M conversion_conv_iff[OF this] have "(x, y) ∈ (⋃a ∈ B ∪ (a)≻. r a)⇧↔⇧*" by auto
{ fix c x y
assume c:"c ∈ B ∪ (a)≻" and rc:"(x, y) ∈ r c"
have "∃M. set_mset M ⊆ B ∧ conv M x y" proof (cases "c ∈ B")
case True
with c rc B_subset_I conv_singleton show ?thesis by (intro exI[of _ "{#c#}"]) auto
next
case False
with c have "a ≻ c" by auto
from rc have xz:"(x, y) ∈ r c ∨ (y, x) ∈ r c" by auto
from 1(1)[of c] ‹a ≻ c› have
ih:"⋀x y. (x, y) ∈ r c ⟹ ∃M. set_mset M ⊆ B ∧ conv M x y" by auto
from ih[of x y] ih[of y x] xz conv_commute show ?thesis by blast
qed
}
with aux[OF _ M, of B] show ?case by argo
qed
} note step = this
let ?A = "⋃a∈set_mset M. r a"
from aux[OF _ conv] step show "∃M. set_mset M ⊆ B ∧ conv M x y" by force
qed
end
locale ars_peak_decreasing = ars_labeled_sn +
assumes peak_decreasing:
"⟦a ∈ I; b ∈ I; (x, y) ∈ r a; (x, z) ∈ r b⟧ ⟹ (y, z) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*"
begin
lemma conv_join_mless_convD:
assumes "conv M x y"
shows "valley M x y ∨ (∃N. M ≻⇩M N ∧ conv N x y)"
using assms
proof (cases rule: conv_valley_peak_cases)
case (peak K L a b t u v)
with peak_decreasing
have "(t, v) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*" by blast
from downset2_conversion_imp_conv [OF this] obtain N
where "{#a, b#} ≻⇩M N" and "conv N t v" by blast
then have "M ≻⇩M K + L + N"
unfolding peak by (intro mless_mono) auto
then have "M ≻⇩M K + N + L" by (auto simp: ac_simps)
moreover have "conv (K + N + L) x y"
using peak and ‹conv N t v› by (blast intro: conv_trans)
ultimately show ?thesis by blast
qed simp
text ‹A conversion is either a valley or can be made smaller w.r.t.\ @{const mless}.›
lemma conv_join_mless_conv_cases:
assumes "conv M x y"
obtains
(valley) "valley M x y" |
(conv) N
where "M ≻⇩M N" and "conv N x y"
using conv_join_mless_convD [OF assms] by blast
lemma conv_imp_valley:
assumes "conv M x y"
shows "∃N. M ≽⇩M N ∧ valley N x y"
using SN_mless and assms
proof (induct)
case (IH M)
from ‹conv M x y› show ?case
proof (cases rule: conv_join_mless_conv_cases)
case valley then show ?thesis by auto
next
case (conv N)
with IH(1) [of N] show ?thesis by (auto elim: mless_trans)
qed
qed
text ‹Every peak decreasing ARS is confluent.›
lemma CR: "CR R"
proof
fix x y z
assume "x ∈ UNIV" and "(x, y) ∈ R⇧*" and "(x, z) ∈ R⇧*"
then have "(y, z) ∈ R⇧↔⇧*" by (metis in_mono meetI meet_imp_conversion)
then obtain M where "conv M y z" by (auto simp: conversion_conv_iff)
from conv_imp_valley [OF this]
show "(y, z) ∈ R⇧↓" by (auto iff: join_valley_iff)
qed
end
context ars_labeled_sn
begin
lemma mset_replicate_Suc:
"(∀x. x ∈# mset (replicate (Suc n) y) ⟶ P x) ⟷ P y"
by (induct n) auto
lemma same_label_conversion_imp_conv:
assumes "(t, u) ∈ (r c)⇧↔⇧*" and "c ∈ I" and "a ≻ c ∨ b ≻ c"
shows "∃M. {#a, b#} ≻⇩M M ∧ conv M t u"
proof -
let ?M = "λn. mset (replicate n c)"
have "⋀n. ∀y. y ∈# ?M (Suc n) ⟶ (∃x. x ∈# {#a, b#} ∧ x ≻ y)"
unfolding mset_replicate_Suc using ‹a ≻ c ∨ b ≻ c› by auto
from mulex_on_all_strict [OF _ _ _ this, of UNIV]
have mless: "⋀n. {#a, b#} ≻⇩M ?M (Suc n)"
by (auto simp: mless_def intro: mulex_on_mono)
from assms(1) have "(t, u) ∈ (r c ∪ (r c)¯)⇧*" by auto
then have "∃n. {#a, b#} ≻⇩M ?M n ∧ conv (?M n) t u"
proof (induct)
case base
have "{#a, b#} ≻⇩M ?M 0" by (simp add: mless_def)
moreover have "conv (?M 0) t t" by simp
ultimately show ?case by blast
next
case (step y z)
then obtain n where "conv (?M n) t y" by blast
moreover from ‹(y, z) ∈ r c ∪ (r c)¯› and ‹c ∈ I›
have "conv {#c#} y z" by (auto)
ultimately have "conv (?M n + {#c#}) t z" by (rule conv_trans)
then have "conv (?M (Suc n)) t z" by simp
with mless show ?case by blast
qed
then show ?thesis by blast
qed
lemma ars_peak_decreasing_alt_intro:
assumes *: "⋀a b x y z.
⟦a ∈ I; b ∈ I; (x, y) ∈ r a; (x, z) ∈ r b⟧ ⟹ ∃c. c ∈ ∨(a, b) ∧ (y, z) ∈ (r c)⇧↔⇧*"
shows "ars_peak_decreasing r I less"
proof (unfold_locales)
fix a b x y z
assume "a ∈ I" and "b ∈ I" and "(x, y) ∈ r a" and "(x, z) ∈ r b"
from * [OF this] obtain c
where "(y, z) ∈ (r c)⇧↔⇧*" and "c ∈ I" and "a ≻ c ∨ b ≻ c" by blast
from conversion_in_downset2 [OF this]
show "(y, z) ∈ (⋃c∈∨(a, b). r c)⇧↔⇧*" .
qed
end
text ‹Partitioning of a relation that labels steps by their source.›
definition source_step :: "'a rel ⇒ 'a ⇒ 'a rel"
where
"source_step R x = {(x, y) | y. (x, y) ∈ R}"
lemma source_step_label [iff]:
"(x, y) ∈ source_step R z ⟷ (x, y) ∈ R ∧ z = x"
by (auto simp: source_step_def)
lemma UN_source_step: "(⋃x. source_step R x) = R"
by auto
locale ars_source_decreasing =
ars_labeled_sn "source_step R" I for R I +
assumes *: "⋀a b c. a ∈ I ⟹ (a, b) ∈ source_step R a ⟹ (a, c) ∈ source_step R a ⟹
(b, c) ∈ (⋃b∈(a)≻. source_step R b)⇧↔⇧*"
sublocale ars_source_decreasing ⊆ ars_peak_decreasing "source_step R"
proof
fix a b x y z assume "a ∈ I" and "b ∈ I"
and "(x, y) ∈ source_step R a" and "(x, z) ∈ source_step R b"
with * have "(⋃b∈(a)≻. source_step R b) ⊆ (⋃c∈∨(a, b). source_step R c)"
and "(y, z) ∈ (⋃b∈(a)≻. source_step R b)⇧↔⇧*" by auto
then show "(y, z) ∈ (⋃c∈∨(a, b). source_step R c)⇧↔⇧*" by (rule conversion_mono [THEN subsetD])
qed
locale ars_mod_labeled = r: ars_labeled r I + s: ars_labeled s J
for r s :: "'a ⇒ 'b rel"
and I J :: "'a set"
begin
inductive valley_mod where
seql [simp, intro]: " s.conv N z y ⟹ r.seql M y x ⟹ valley_mod (N + M) z x" |
left [intro]: "⟦a ∈ I; (x, y) ∈ r a; valley_mod M y z⟧ ⟹ valley_mod (add_mset a M) x z"
lemma[simp]: "valley_mod {#} x x"
using valley_mod.seql[OF s.conv.empty r.seql.empty] by auto
abbreviation "R ≡ (⋃a∈I. r a)"
abbreviation "S ≡ (⋃a∈J. s a)"
lemma join_mod_valley_mod_iff:
"(x, y) ∈ R⇧* O S⇧↔⇧* O (R¯)⇧* ⟷ (∃M. valley_mod M x y)"
proof
assume "(x, y) ∈ R⇧* O S⇧↔⇧* O (R¯)⇧*"
then obtain z⇩1 where z⇩1:"(x, z⇩1) ∈ R⇧*" and "(z⇩1, y) ∈ S⇧↔⇧* O ((R¯)⇧*)" by auto
from this(2) obtain z⇩2 where z⇩2:"(z⇩1, z⇩2) ∈ S⇧↔⇧*" and "(y, z⇩2) ∈ R⇧*"
unfolding relcomp.simps using rtrancl_converseD by metis
then obtain M N where MN:"s.conv M z⇩1 z⇩2" "r.seql N z⇩2 y"
unfolding r.rtrancl_seql_iff s.conversion_R_conv_iff by auto
with z⇩1 have "(x, z⇩1) ∈ R⇧*" "valley_mod (M + N) z⇩1 y" using valley_mod.seql[OF MN] by auto
then show "∃M. valley_mod M x y" by (induct arbitrary: z⇩1 rule: converse_rtrancl_induct, auto)
next
assume "∃M. valley_mod M x y"
then obtain M where M:"valley_mod M x y" by auto
have *:"⋀N z y. s.conv N z y ⟹ (z, y) ∈ S⇧↔⇧*" using s.conversion_R_conv_iff by auto
have **:"⋀y M x. r.seql M y x ⟹ (y, x) ∈ (R¯)⇧*" using
r.rtrancl_seql_iff rtrancl_converseI by metis
from M show "(x, y) ∈ R⇧* O S⇧↔⇧* O (R¯)⇧*"
by induct (auto iff: r.rtrancl_seql_iff dest!:*, auto dest!:**)
qed
abbreviation sr where "sr ≡ (λi. (if i ∈ I then r i else {}) ∪ (if i ∈ J then s i else {}))"
lemma RS_subset_sr: "R ∪ S ⊆ (⋃a∈I ∪ J. sr a)"
by auto
lemma sr_cases:"(x, y) ∈ (sr a) ⟹ ((x,y) ∈ r a ∧ a ∈ I) ∨ ((x,y) ∈ s a ∧ a ∈ J)"
by (smt Un_iff empty_iff)
sublocale sr: ars_labeled sr "I ∪ J" by unfold_locales
lemma rconv: assumes "r.conv M x y" shows "sr.conv M x y"
using assms by (induct, auto)
lemma sconv: assumes "s.conv M x y" shows "sr.conv M x y"
using assms by (induct, auto)
lemma valley_imp_conv:
assumes "valley_mod M x y"
shows "sr.conv M x y" using assms
proof(induct)
case (seql N z y M x)
from rconv[OF r.seql_imp_conv[OF this(2)]] sconv[OF this(1)] sr.conv_trans sr.conv_commute
show ?case by auto
next
case (left a x y M z)
from r.conv_singleton left have "r.conv {#a#} x y" by auto
with rconv have "sr.conv {#a#} x y" by auto
from sr.conv_trans[OF this left(4)] show ?case by auto
qed
definition mod_peak where "mod_peak t a u b v ≡
(a ∈ I ∧ b ∈ I ∧ (u, t) ∈ r a ∧ (u, v) ∈ r b) ∨
(a ∈ I ∧ b ∈ J ∧ (u, t) ∈ r a ∧ (u, v) ∈ (s b)⇧↔) ∨
(a ∈ I ∧ b ∈ J ∧ (u, t) ∈ (s b)⇧↔ ∧ (u, v) ∈ r a)"
lemma conv_valley_mod_peak_cases:
assumes "sr.conv M x y"
obtains
(valley) "valley_mod M x y" |
(peak) K L a b t u v
where "M = K + L + {#a, b#}"
and "sr.conv K x t"
and "mod_peak t a u b v"
and "sr.conv L v y"
using assms
proof (induct)
case (empty x) then show ?case by auto
next
case (step a x y M z)
let ?peak = "λ K L c b t u v.
add_mset a M = K + L + {#c, b#} ∧ sr.conv K x t ∧ mod_peak t c u b v ∧ sr.conv L v z"
have conv_seql[simp]:"⋀M x y. r.seql M x y ⟹ sr.conv M x y" using r.seql_imp_conv rconv by auto
show ?case
proof (rule step.hyps)
assume *: "valley_mod M y z"
from ‹(x, y) ∈ (sr a)⇧↔› consider "(x, y) ∈ sr a" | "(y, x) ∈ sr a" by auto
thus ?thesis
proof(cases)
case 1
from sr_cases[OF 1] consider "(x, y) ∈ r a ∧ a ∈ I" | "(x, y) ∈ s a ∧ a ∈ J" by auto
then show ?thesis proof(cases)
case 1
with * have "valley_mod (add_mset a M) x z" by auto
then show ?thesis by fact
next
case 2
from * show ?thesis proof(cases)
case (seql N w M')
from seql(2) s.conv.step[of a x y] 2 have "s.conv (add_mset a N) x w" by auto
from valley_mod.seql[OF this] seql(3) have "valley_mod (add_mset a M) x z"
unfolding seql(1) by auto
thus ?thesis by fact
next
case (left b w M')
from this(2) this(3) 2 have 1:"mod_peak x b y a w" unfolding mod_peak_def by auto
from valley_imp_conv[OF left(4)] have 3:"sr.conv M' w z" by auto
from left(1) have 4:"add_mset a M = M' + {#b, a#}" by auto
from 4 1 3 have *:"?peak {#} M' b a x y w" by auto
thus ?thesis using step.prems(2)[of "{#}" M' b a] by blast
qed
qed
next
case 2
from sr_cases[OF 2] consider "(y, x) ∈ r a ∧ a ∈ I" | "(y, x) ∈ s a ∧ a ∈ J" by auto
then show ?thesis proof(cases)
case 1
from * show ?thesis proof(cases)
case (seql N y' M')
from this(2) show ?thesis proof(cases)
case empty
from seql(3) 1 have "r.seql (add_mset a M') x z"
using r.seql.step[of a y x] unfolding empty(2) by auto
with valley_mod.seql have "valley_mod (add_mset a M) x z"
unfolding seql empty by fastforce
then show ?thesis by fact
next
case (step b w K)
with 1 have 1:"mod_peak x a y b w" unfolding mod_peak_def by auto
from step(1) seql(1) have 2:"add_mset a M = K + M' + {#a, b#}" by auto
from sconv[OF step(4)] seql(3) sr.conv_trans have 3:"sr.conv (K + M') w z" by auto
from 1 2 3 have *:"?peak {#} (K + M') a b x y w" by auto
then show ?thesis using step.prems(2) by blast
qed
next
case (left b w M')
with 1 have 1:"mod_peak x a y b w" unfolding mod_peak_def by auto
from valley_imp_conv[OF left(4)] have 3:"sr.conv M' w z" by auto
from left(1) have 4:"add_mset a M = M' + {#a, b#}" by auto
from 4 1 3 have *:"?peak {#} M' a b x y w" by auto
thus ?thesis using step.prems(2) by blast
qed
next
case 2
from * show ?thesis proof(cases)
case (seql N w M')
with 2 have "s.conv (add_mset a N) x w" using s.conv.step by auto
from valley_mod.seql[OF this] seql have "valley_mod (add_mset a M) x z" by auto
then show ?thesis by fact
next
case (left b w M')
with 2 have 1:"mod_peak x b y a w" unfolding mod_peak_def by auto
from valley_imp_conv[OF left(4)] have 3:"sr.conv M' w z" by auto
from left(1) have 4:"add_mset a M = M' + {#b, a#}" by auto
from 4 1 3 have *:"?peak {#} M' b a x y w" by auto
thus ?thesis using step.prems(2) by blast
qed
qed
qed
next
fix K L b c t u v
assume [simp]: "M = K + L + {#b, c#}"
and "sr.conv K y t" and peak:"mod_peak t b u c v" "sr.conv L v z"
with step have 1:"sr.conv (add_mset a K) x t" by blast
have [simp]:"add_mset a M = add_mset a K + L + {#b, c#}" by (auto simp: ac_simps)
show ?thesis by (rule step.prems) fact+
qed
qed
end
definition CRm where
"CRm A B ⟷ (A ∪ B)⇧↔⇧* ⊆ (A⇧* O B⇧↔⇧* O (A¯)⇧*)"
locale ars_mod_labeled_sn = ars_mod_labeled r s I J
for r s :: "'a ⇒ 'b rel"
and I J :: "'a set" +
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "≻" 50)
assumes SN_less: "SN {(x, y). x ≻ y}"
begin
sublocale ars_labeled_sn sr "I ∪ J" less using SN_less by unfold_locales
context
assumes peak_decreasing_mod: "mod_peak x a y b z ⟹ (x, z) ∈ (⋃c∈downset2 a b. sr c)⇧↔⇧*"
begin
lemma conv_join_mod_mless_convD:
assumes "sr.conv M x y"
shows "valley_mod M x y ∨ (∃N. M ≻⇩M N ∧ sr.conv N x y)"
using assms
proof (cases rule: conv_valley_mod_peak_cases)
case (peak K L a b t u v)
with peak_decreasing_mod consider "(t, v) ∈ (⋃c∈ downset2 a b. sr c)⇧↔⇧*" by presburger
hence "(t, v) ∈ (⋃c∈ downset2 a b. sr c)⇧↔⇧*" by auto
with downset2_conversion_imp_conv obtain N where "{#a, b#} ≻⇩M N" and "sr.conv N t v" by blast
then have "M ≻⇩M K + L + N"
unfolding peak by (intro mless_mono) auto
then have "M ≻⇩M K + N + L" by (auto simp: ac_simps)
moreover have "sr.conv (K + N + L) x y"
using peak and ‹sr.conv N t v› by (blast intro: sr.conv_trans)
ultimately show ?thesis by blast
qed simp
text ‹A mixed conversion is either a valley modulo or can be made smaller w.r.t.\ @{const mless}.›
lemma conv_join_mod_mless_conv_cases:
assumes "sr.conv M x y"
obtains
(valley) "valley_mod M x y" |
(conv) N
where "M ≻⇩M N" and "sr.conv N x y"
using conv_join_mod_mless_convD [OF assms] by blast
lemma conv_imp_valley_mod:
assumes "sr.conv M x y"
shows "∃N. M ≽⇩M N ∧ valley_mod N x y"
using SN_mless and assms
proof (induct)
case (IH M)
from ‹sr.conv M x y› show ?case
proof (cases rule: conv_join_mod_mless_conv_cases)
case valley then show ?thesis by auto
next
case (conv N)
with IH(1) [of N] show ?thesis by (auto elim: mless_trans)
qed
qed
text ‹A pair of ARSs which is peak decreasing modulo is Church-Rosser modulo.›
lemma CRm: "CRm R S"
proof-
{ fix x y
assume "(x,y) ∈ (R ∪ S)⇧↔⇧*"
with conversion_mono[OF RS_subset_sr] have "(x,y) ∈ (⋃a∈I ∪ J. sr a)⇧↔⇧*" by auto
then obtain M where M:"sr.conv M x y" using sr.conversion_R_conv_iff by auto
hence "(x,y) ∈ R⇧* O S⇧↔⇧* O (R¯)⇧*" proof(induct M rule: SN_induct [OF SN_mless])
case (1 M)
from 1(2) show ?case proof (cases rule:conv_join_mod_mless_conv_cases)
case valley
then show ?thesis unfolding join_mod_valley_mod_iff by auto
next
case (conv N)
with 1(1)[OF _ conv(2)] show ?thesis by auto
qed
qed }
thus ?thesis unfolding CRm_def by auto
qed
end
end
end