section ‹Normalization Equivalence›
theory Normalization_Equivalence
imports
QTRS.Encompassment
Representative_System
"../Orderings/Reduction_Order"
begin
definition "left_reduced R ⟷ (∀(l, r)∈R. l ∈ NF (rstep (R - {(l, r)})))"
definition "right_reduced R ⟷ (∀(l, r)∈R. r ∈ NF (rstep R))"
definition "reduced R ⟷ left_reduced R ∧ right_reduced R"
definition "canonical R ⟷ reduced R ∧ SN (rstep R) ∧ CR (rstep R)"
definition variant_free_trs :: "('f, 'v :: infinite) trs ⇒ bool"
where
"variant_free_trs R ⟷ (∀l r l' r'.
(l, r) ∈ R ∧ (l', r') ∈ R ∧ (∃p. p ∙ l = l' ∧ p ∙ r = r') ⟶ l = l' ∧ r = r')"
lemma litsim_mem:
assumes "R ≐ S" and "r ∈ R"
obtains p where "p ∙ r ∈ S"
using assms by (auto simp: subsumable_trs.litsim_def)
lemma variant_free_trs_insert:
assumes "variant_free_trs R" and "∀p. (p ∙ l, p ∙ r) ∉ R"
shows "variant_free_trs (insert (l, r) R)"
using assms
unfolding variant_free_trs_def eqvt [symmetric]
by (metis (no_types, lifting) assms(2) insert_iff prod.sel(1) prod.sel(2) term_pt.permute_minus_cancel(2))
lemma variant_free_trs_diff:
"variant_free_trs R ⟹ variant_free_trs (R - S)"
unfolding variant_free_trs_def by blast
lemma litsim_rstep_eq:
fixes R S :: "('f, 'v::infinite) trs"
assumes "R ≐ S"
shows "rstep R = rstep S"
proof -
{ fix R S s t C l r and σ :: "('f, 'v) subst" assume "R ≐ S" and "(l, r) ∈ R"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
then obtain π where "(π ∙ l, π ∙ r) ∈ S"
by (metis rule_pt.permute_prod.simps subsumable_trs.litsim_def subsumeseq_trsE)
moreover have "s = C⟨π ∙ l ⋅ sop (-π) ∘⇩s σ⟩" and "t = C⟨π ∙ r ⋅ sop (-π) ∘⇩s σ⟩"
using s and t
by (simp_all add: eqvt [symmetric])
ultimately have "(s, t) ∈ rstep S" by blast }
then show ?thesis using assms by (auto elim!: rstepE dest: subsumable_trs.litsim_sym)
qed
lemma litsim_insert:
assumes "R ≐ R'" and "r' = p ∙ r "
shows "insert r R ≐ insert r' R'"
using assms
apply (auto simp: subsumeseq_trs_def subsumable_trs.litsim_def)
using rule_pt.permute_minus_cancel(2) by blast
lemma litsim_insert':
assumes "R ≐ R'" and "p ∙ r ∈ R'"
shows "insert r R ≐ R'"
using assms
by (auto simp: subsumeseq_trs_def subsumable_trs.litsim_def)
lemma litsim_diff1:
assumes "R ≐ R'" and "variant_free_trs R" and "variant_free_trs R'" and "r' = p ∙ r"
and "r ∈ R" and "r' ∈ R'"
shows "R - {r} ≐ R' - {r'}"
proof -
{ fix s assume "s ∈ R - {r}"
then have "∃p. p ∙ s ∈ R' - {r'}"
using assms
apply (cases "s = r")
apply (force simp: variant_free_trs_def)
apply (auto elim!: litsim_mem)
apply (rule_tac x = pa in exI)
unfolding variant_free_trs_def
by (metis (no_types, hide_lams) prod.collapse rule_pt.fst_eqvt rule_pt.permute_minus_cancel(2) rule_pt.permute_plus rule_pt.snd_eqvt) }
moreover
{ fix s assume "s ∈ R' - {r'}"
moreover have "R' ≐ R" and "r = -p ∙ r'" using assms by (auto dest: subsumable_trs.litsim_sym)
ultimately have "∃p. p ∙ s ∈ R - {r}"
using assms(2-3,5-)
apply (cases "s = r'")
apply (force simp: variant_free_trs_def)
apply (auto elim!: litsim_mem)
apply (rule_tac x = pa in exI)
unfolding variant_free_trs_def
by (metis (no_types, hide_lams) prod.collapse rule_pt.fst_eqvt rule_pt.permute_minus_cancel(2) rule_pt.permute_plus rule_pt.snd_eqvt) }
ultimately
show ?thesis
by (auto simp: subsumable_trs.litsim_def subsumeseq_trs_def)
qed
lemma litsim_union:
assumes "R ≐ R'" and "S ≐ S'"
shows "R ∪ S ≐ R' ∪ S'"
using assms by (auto simp: subsumeseq_trs_def subsumable_trs.litsim_def)
lemma litsim_symcl:
assumes "R ≐ R'"
shows "R⇧↔ ≐ R'⇧↔"
using assms
apply (auto simp: subsumable_trs.litsim_def subsumeseq_trs_def)
apply (metis converse.intros rule_pt.permute_prod.simps)+
done
definition rm_variants :: "('f, 'v :: infinite) trs ⇒ ('f, 'v) trs"
where
"rm_variants R = repsys R (rule_pt.variants ∩ R × R)"
definition "dot' R = {(l, some_NF (rstep R) r) | l r. (l, r) ∈ R}"
definition "dot R = rm_variants (dot' R)"
definition "ddot R = {(l, r) ∈ dot R. l ∈ NF (rstep (dot R - {(l, r)}))}"
lemma rm_variants_subset:
"rm_variants R ⊆ R"
using rule_pt.variants_equiv_on_TRS [of R, THEN repsys_subset] by (simp add: rm_variants_def)
lemma rm_variants_unique_modulo:
assumes "x ∈ rm_variants R" and "y ∈ rm_variants R" and "x ≠ y"
shows "¬ (∃p. p ∙ x = y)"
using repsys_unique_modulo [of R, OF rule_pt.variants_equiv_on_TRS, folded rm_variants_def, OF assms]
and assms and rm_variants_subset [of R]
by (auto simp: rule_pt.variants_def)
lemma rm_variants_representative:
"(l, r) ∈ R ⟹ ∃p. ∃(l', r') ∈ rm_variants R. p ∙ (l, r) = (l', r')"
using repsys_representative [of R, OF rule_pt.variants_equiv_on_TRS, folded rm_variants_def]
by (fastforce simp: eqvt rule_pt.variants_def)
lemma variant_free_rm_variants:
"variant_free_trs (rm_variants R)"
using rm_variants_unique_modulo [of _ R] by (fastforce simp: variant_free_trs_def eqvt)
lemma variant_free_ddot:
shows "variant_free_trs (ddot R)"
using variant_free_rm_variants
unfolding ddot_def dot_def variant_free_trs_def by fast
lemma right_reduced_mono:
assumes "R ⊆ S" and "right_reduced S"
shows "right_reduced R"
using assms apply (auto simp: right_reduced_def)
by (metis NF_anti_mono in_mono rstep_mono split_conv)
lemma ddot_subset_dot:
"ddot R ⊆ dot R"
by (auto simp: ddot_def)
lemma lhss_dot:
"lhss (dot R) ⊆ lhss R"
using rm_variants_subset by (force simp: dot_def dot'_def)
lemma lhss_variants:
"∀l ∈ lhss R. ∃p. ∃l' ∈ lhss (dot R). p ∙ l = l'"
proof
fix l
assume *: "l ∈ lhss R"
from * obtain r where "(l, r) ∈ dot' R" by (force simp: dot'_def)
with rm_variants_representative [of l r "dot' R"] obtain p l' r'
where "(l', r') ∈ rm_variants (dot' R)"
and "p ∙ l = l'" by (force simp: eqvt)
moreover then have "l' ∈ lhss (dot R)" by (force simp add: dot_def dot'_def eqvt)
ultimately show "∃p. ∃l' ∈ lhss (dot R). p ∙ l = l'" by blast
qed
lemma lhss_eq_imp_NF_subset:
assumes "∀l ∈ lhss S. ∃p. ∃l' ∈ lhss R. p ∙ l = l'"
shows "NF (rstep R) ⊆ NF (rstep S)"
proof
fix t
assume "t ∈ NF (rstep R)"
show "t ∈ NF (rstep S)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain s where "(t, s) ∈ rstep S" by blast
then obtain C σ l r where "(l, r) ∈ S"
and [simp]: "t = C⟨l ⋅ σ⟩" and [simp]: "s = C⟨r ⋅ σ⟩" by auto
with assms obtain p l' r' where "(l', r') ∈ R" and "p ∙ l = l'" by force
then have "(p ∙ l, r') ∈ rstep R" by auto
from rstep.subst [OF this, of "sop (-p)"]
have "(l, -p ∙ r') ∈ rstep R" by simp
then have "(t, C⟨(-p ∙ r') ⋅ σ⟩) ∈ rstep R" by auto
with ‹t ∈ NF (rstep R)› show False by blast
qed
qed
lemma NF_rstep_dot:
"NF (rstep (dot R)) = NF (rstep R)"
using term_set_pt.subset_imp_ex_perm [OF lhss_dot, THEN lhss_eq_imp_NF_subset, of R]
and lhss_eq_imp_NF_subset [OF lhss_variants, of R] by blast
lemma NF_eq_imp_left_reduced:
assumes "NF (rstep (ddot R)) = NF (rstep (dot R))"
shows "left_reduced (ddot R)"
proof (unfold left_reduced_def, intro ballI2)
fix l r
assume "(l, r) ∈ ddot R"
then have "(l, r) ∈ dot R"
and *: "l ∈ NF (rstep (dot R - {(l, r)}))" by (auto simp: ddot_def)
show "l ∈ NF (rstep (ddot R - {(l, r)}))"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain u where "(l, u) ∈ rstep (ddot R - {(l, r)})" by auto
from rstepE [OF this]
obtain C σ l' r' where "(l', r') ∈ ddot R - {(l, r)}"
and [simp]: "l = C⟨l' ⋅ σ⟩" "u = C⟨r' ⋅ σ⟩" by metis
then have "(l', r') ∈ dot R - {(l, r)}" using ddot_subset_dot [of R] by auto
then have "(l, u) ∈ rstep (dot R - {(l, r)})" by auto
with * show False by blast
qed
qed
locale SN_ars =
fixes A :: "'a rel"
assumes SN: "SN A"
begin
lemma some_NF_rtrancl:
"(x, some_NF A x) ∈ A⇧*"
apply (auto simp: some_NF_def normalizability_def)
by (metis (lifting) SN SN_imp_WN UNIV_I WN_onD normalizability_E someI)
lemma Ex_NF:
"∃y. (x, y) ∈ A⇧!"
by (metis SN SN_imp_WN UNIV_I WN_on_def)
lemma some_NF_NF:
"some_NF A x ∈ NF A"
apply (auto simp: some_NF_def)
by (metis (lifting, no_types) Ex_NF normalizability_E someI)
lemma some_NF_NF':
"(x, some_NF A x) ∈ A⇧!"
using some_NF_rtrancl [of x] and some_NF_NF [of x] by (simp add: normalizability_def)
end
locale SN_trs =
SN_ars "rstep R" for R :: "('f, 'v :: infinite) trs"
begin
lemma dot_imp_rhs_NF:
assumes "(l, r) ∈ dot R"
shows "r ∈ NF (rstep (dot R))"
using assms and rm_variants_subset
unfolding NF_rstep_dot by (auto simp: dot_def dot'_def intro: some_NF_NF)
lemma dot_right_reduced:
"right_reduced (dot R)"
by (auto simp: right_reduced_def dest: dot_imp_rhs_NF)
end
lemma WN_NE_imp_step_subset_conv:
assumes "WN A"
and "A⇧! = B⇧!"
shows "A ⊆ B⇧↔⇧*"
proof
fix a b assume "(a, b) ∈ A"
moreover obtain c where "(b, c) ∈ A⇧!" using ‹WN A› by blast
ultimately have "(a, c) ∈ A⇧!" by blast
with ‹(b, c) ∈ A⇧!› show "(a, b) ∈ B⇧↔⇧*"
unfolding assms
unfolding normalizability_def
by (auto intro: join_imp_conversion [THEN subsetD])
qed
text ‹Normalization equivalent normalizing ARSs are equivalent.›
lemma WN_NE_imp_conv_eq:
assumes "WN A" and "WN B"
and NE: "A⇧! = B⇧!"
shows "A⇧↔⇧* = B⇧↔⇧*"
using WN_NE_imp_step_subset_conv [OF assms(1) NE, THEN conversion_mono]
and WN_NE_imp_step_subset_conv [OF assms(2) NE [symmetric], THEN conversion_mono]
by simp
locale complete_ars =
SN_ars A for A :: "'a rel" +
assumes CR: "CR A"
begin
lemma complete_NE_intro2:
assumes "SN B" and "B⇧! ⊆ A⇧!"
shows "complete_ars B ∧ A⇧! = B⇧!"
proof -
have "A⇧! ⊆ B⇧!"
proof
interpret SN_ars B by standard fact
fix a b
obtain c where "(a, c) ∈ B⇧!" using Ex_NF by blast
with ‹B⇧! ⊆ A⇧!› have "(a, c) ∈ A⇧!" by blast
moreover
assume "(a, b) ∈ A⇧!"
ultimately have [simp]: "b = c" using CR by (metis CR_imp_UNF UNF_onD UNIV_I)
with ‹(a, c) ∈ B⇧!› show "(a, b) ∈ B⇧!" by simp
qed
with ‹B⇧! ⊆ A⇧!› have **: "A⇧! = B⇧!" by blast
with ‹SN B› [THEN SN_imp_WN] and ‹B⇧! ⊆ A⇧!› have "B ⊆ A⇧↔⇧*"
by (metis SN [THEN SN_imp_WN] WN_NE_imp_conv_eq conversionI' r_into_rtrancl subrelI)
have "CR B"
proof (rule Newman [OF ‹SN B›], rule)
fix x y z
assume "(x, y) ∈ B" and "(x, z) ∈ B"
with subsetD[OF ‹B ⊆ A⇧↔⇧*›] rtrancl_trans have "(y, z) ∈ A⇧↔⇧*"
by (metis converse.intros conversion_converse conversion_rtrancl)
then obtain u where "(y, u) ∈ A⇧*" and "(z, u) ∈ A⇧*"
unfolding CR_imp_conversionIff_join[OF CR] by auto
moreover obtain v where "(u, v) ∈ A⇧!" using Ex_NF by blast
ultimately have "(y, v) ∈ A⇧!" and "(z, v) ∈ A⇧!" by (metis normalizability_I')+
then have "(y, v) ∈ B⇧!" and "(z, v) ∈ B⇧!" unfolding ** by auto
then show "(y, z) ∈ B⇧↓" by auto
qed
have "complete_ars B" by standard fact+
with ** show ?thesis by simp
qed
lemma complete_NE_intro1:
assumes "B ⊆ A⇧↔⇧*" and "SN B" and "NF B ⊆ NF A"
shows "complete_ars B ∧ A⇧! = B⇧!"
proof -
from ‹B ⊆ A⇧↔⇧*› conversion_rtrancl in_rtrancl_UnI have "B⇧! ⊆ A⇧↔⇧*"
by (metis normalizability_E subrelI subset_Un_eq)
with CR_NF_conv[OF CR] have "B⇧! ⊆ A⇧!"
by (meson ‹NF B ⊆ NF A› normalizability_E set_mp subrelI)
from complete_NE_intro2[OF ‹SN B› this] show ?thesis .
qed
lemma complete_NE_intro:
assumes "B ⊆ A⇧+" and "NF B ⊆ NF A"
shows "complete_ars B ∧ A⇧! = B⇧!"
proof -
have "SN B" by (rule SN_subset [OF SN_imp_SN_trancl [OF SN] ‹B ⊆ A⇧+›])
moreover have "B⇧* ⊆ A⇧*" using ‹B ⊆ A⇧+›
by (auto) (metis rtrancl_mono set_rev_mp trancl_rtrancl_absorb)
ultimately have "B⇧! ⊆ A⇧!" using ‹NF B ⊆ NF A› by best
from complete_NE_intro2[OF ‹SN B› this] show ?thesis .
qed
end
locale complete_trs =
complete_ars "rstep R" for R :: "('f, 'v :: infinite) trs"
begin
lemma dot_subset_rstep_trancl:
"dot R ⊆ (rstep R)⇧+"
proof
fix l r
assume "(l, r) ∈ dot R"
then obtain "(l, r) ∈ dot' R" using rm_variants_subset by (auto simp: dot_def)
{ fix l r
assume "(l, r) ∈ R"
then have "(l, r) ∈ rstep R" by auto
moreover have "(r, some_NF (rstep R) r) ∈ (rstep R)⇧*" by (rule some_NF_rtrancl)
ultimately have "(l, some_NF (rstep R) r) ∈ (rstep R)⇧+" by auto }
then have "dot' R ⊆ (rstep R)⇧+" by (auto simp: dot'_def)
with ‹(l, r) ∈ dot' R› show "(l, r) ∈ (rstep R)⇧+" by auto
qed
lemma rstep_dot_subset_rstep_trancl:
"rstep (dot R) ⊆ (rstep R)⇧+"
using dot_subset_rstep_trancl
by (auto elim!: rstepE)
(metis rsteps_subst_closed set_rev_mp trancl_rstep_ctxt)
lemma
complete_ars_rstep_dot: "complete_ars (rstep (dot R))" and
NE_dot [simp]: "(rstep (dot R))⇧! = (rstep R)⇧!"
using complete_NE_intro [OF rstep_dot_subset_rstep_trancl] by (auto simp: NF_rstep_dot)
end
lemma not_NF_minus_rule:
assumes "l ∉ NF (rstep (R - {(l, r)}))"
shows "∃(l', r') ∈ R. (l, r) ≠ (l', r') ∧ l ⋅⊵ l'"
proof -
from assms obtain u where "(l, u) ∈ rstep (R - {(l, r)})" by auto
from rstepE [OF this] obtain C σ l' r'
where "(l', r') ∈ R - {(l, r)}" and [simp]: "l = C⟨l' ⋅ σ⟩" "u = C⟨r' ⋅ σ⟩" by metis
then show ?thesis by (blast)
qed
sublocale complete_trs ⊆ SN_trs ..
sublocale complete_trs ⊆ complete_ars "rstep R" ..
context complete_trs
begin
lemma variant_free_dot:
"variant_free_trs (dot R)"
using variant_free_rm_variants by (simp add: dot_def)
text ‹If @{term R} is a complete TRS than @{term "ddot R"} is a (normalization) equivalent
canonical TRS.›
lemma canonical_NE_conv_eq:
"canonical (ddot R) ∧ (rstep (ddot R))⇧! = (rstep R)⇧! ∧ (rstep (ddot R))⇧↔⇧* = (rstep R)⇧↔⇧*"
proof (intro conjI)
interpret dot_ars: complete_ars "(rstep (dot R))" by (rule complete_ars_rstep_dot)
interpret dot_trs: complete_trs "dot R" ..
from ddot_subset_dot [THEN rstep_mono, of R]
have SN_ddot: "SN (rstep (ddot R))" by (metis SN_subset dot_ars.SN)
have "NF (rstep R) = NF (rstep (dot R))"
using NF_rstep_dot [of R] by simp
{ fix s t
assume "(s, t) ∈ rstep (dot R)"
then obtain C σ l r where "(l, r) ∈ dot R"
and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" by auto
from ‹(l, r) ∈ dot R› have "l ∉ NF (rstep (ddot R))"
proof (induct l arbitrary: r rule: encomp_induct)
case (1 l)
show ?case
proof (cases "(l, r) ∈ ddot R")
assume "(l, r) ∉ ddot R"
then have "l ∉ NF (rstep (dot R - {(l, r)}))"
using ‹(l, r) ∈ dot R› by (auto simp: ddot_def)
from not_NF_minus_rule [OF this] obtain l' r'
where "(l', r') ∈ dot R"
and "(l, r) ≠ (l', r')"
and "l ⋅⊵ l'" using ‹(l, r) ∈ dot R› by auto
then have "l ⋅⊳ l' ∨ l ≐ l'" by (auto simp: term_subsumable.litsim_def dest: encompeq_cases)
then show ?thesis
proof
assume "l ⋅⊳ l'"
with 1 and ‹(l', r') ∈ dot R› have "l' ∉ NF (rstep (ddot R))" by auto
with ‹l ⋅⊳ l'› show ?thesis
by (auto simp: encomp_def NF_iff_no_step elim!: encompeq.cases)
(metis rstep.ctxt rstep.subst)
next
assume "l ≐ l'"
then obtain π where π_l: "π ∙ l = l'" by (auto simp: litsim_term_iff)
have "r ∈ NF (rstep (dot R))" and "r' ∈ NF (rstep (dot R))"
using ‹(l, r) ∈ dot R› and ‹(l', r') ∈ dot R› and dot_imp_rhs_NF by blast+
then have "π ∙ r ∈ NF (rstep (dot R))"
by (auto simp: NF_iff_no_step) (metis perm_rstep_imp_rstep perm_rstep_perm)
have "(π ∙ l, π ∙ r) ∈ (rstep (dot R))⇧*"
and "(l', r') ∈ (rstep (dot R))⇧*" using ‹(l, r) ∈ dot R› and ‹(l', r') ∈ dot R› by auto
with dot_ars.CR and ‹π ∙ r ∈ NF (rstep (dot R))› and ‹r' ∈ NF (rstep (dot R))›
have "π ∙ r = r'"
by (auto simp: π_l CR_defs NF_iff_no_step) (metis converse_rtranclE joinD)
then have "π ∙ (l, r) = (l', r')" by (simp add: eqvt π_l)
with ‹(l, r) ∈ dot R› and ‹(l', r') ∈ dot R› and variant_free_dot
have False
by (simp add: variant_free_trs_def) (metis π_l ‹π ∙ r = r'› ‹(l, r) ≠ (l', r')›)
then show ?thesis by blast
qed
qed auto
qed
then have "s ∉ NF (rstep (ddot R))" by (auto simp: NF_iff_no_step) (metis rstep.simps) }
then have *: "NF (rstep (ddot R)) ⊆ NF (rstep (dot R))" by blast
then have **: "NF (rstep (ddot R)) = NF (rstep (dot R))"
using ddot_subset_dot [of R]
by (auto) (metis NF_anti_mono order_class.order.antisym rstep_mono)
from complete_NE_intro [OF _ * [simplified NF_rstep_dot]]
and ddot_subset_dot [THEN rstep_mono, of R] and rstep_dot_subset_rstep_trancl
have "complete_ars (rstep (ddot R))" and ***: "(rstep (ddot R))⇧! = (rstep R)⇧!" by auto
then interpret ddot_trs: complete_ars "rstep (ddot R)" by simp
interpret ddot_trs: complete_trs "ddot R" ..
show "(rstep (ddot R))⇧! = (rstep R)⇧!" by fact
from WN_NE_imp_conv_eq [OF SN_ddot [THEN SN_imp_WN] SN [THEN SN_imp_WN] ***]
show "(rstep (ddot R))⇧↔⇧* = (rstep R)⇧↔⇧*" .
have "right_reduced (ddot R)" by (fact right_reduced_mono [OF ddot_subset_dot dot_right_reduced])
from NF_eq_imp_left_reduced [OF **]
have "left_reduced (ddot R)" .
have "reduced (ddot R)" by (auto simp: reduced_def) fact+
show "canonical (ddot R)" by (auto simp: canonical_def) fact+
qed
end
lemma size_permute_term [simp]:
fixes t :: "('f, 'v :: infinite) term"
shows "size (p ∙ t) = size t"
proof (induct t)
case (Fun g ts)
then have *: "⋀t. t ∈ set ts ⟹ size (p ∙ t) ≤ size t"
and **: "⋀t. t ∈ set ts ⟹ size t ≤ size (p ∙ t)" by auto
from size_list_pointwise [of ts _ size, OF *]
and size_list_pointwise [of ts size, OF **]
show ?case by (simp add: o_def)
qed simp
lemma permute_term_size:
fixes s t :: "('f, 'v :: infinite) term"
assumes "p ∙ s = t"
shows "size s = size t"
unfolding assms [symmetric] by simp
lemma size_ctxt_Hole [simp]:
assumes "size (C⟨t⟩) = size t"
shows "C = □"
using assms
apply (induct C) apply (auto)
using supteq_size [OF ctxt_imp_supteq, of t]
by (metis Suc_n_not_le_n le_SucI add.commute trans_le_add2)
lemma ctxt_permute_term:
assumes "s = C⟨l ⋅ σ⟩" and "p ∙ l = s"
shows "C = □ ∧ (∀x ∈ vars_term l. sop p x = σ x)"
proof -
from ‹s = C⟨l ⋅ σ⟩› have "s ⊵ l ⋅ σ" by auto
then have "size s ≥ size (l ⋅ σ)" using supteq_size by blast
moreover have "size s = size l" using permute_term_size [OF ‹p ∙ l = s›] ..
moreover have "size (l ⋅ σ) ≥ size l" by (auto simp: size_subst)
ultimately have "size (C⟨l ⋅ σ⟩) = size (l ⋅ σ)" unfolding assms by auto
then have "C = □" by simp
moreover then have "∀x ∈ vars_term l. sop p x = σ x" using ‹p ∙ l = s›
using assms
by (metis assms(1) ctxt_apply_term.simps(1) term_apply_subst_Var_Rep_perm term_subst_eq_rev)
ultimately show ?thesis by blast
qed
lemma right_reduced_min_step_rule:
assumes vc: "∀(l, r) ∈ R. vars_term r ⊆ vars_term l"
and rr: "right_reduced R"
and min: "∀t. s ⋅⊳ t ⟶ t ∈ NF (rstep R)"
and steps: "(s, t) ∈ (rstep R)⇧+"
shows "∃p. ∃(l, r) ∈ R. s = p ∙ l ∧ t = p ∙ r"
proof -
from steps obtain u
where "(s, u) ∈ rstep R" and "(u, t) ∈ (rstep R)⇧*" by (auto dest: tranclD)
then obtain C σ l r where "(l, r) ∈ R"
and [simp]: "s = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" by auto
then have "s ⋅⊵ l" by auto
moreover have "l ∉ NF (rstep R)" using ‹(l, r) ∈ R› by auto
ultimately have "l ≐ s" using min unfolding encompeq_litsim_encomp_iff by auto
then obtain p where "s = p ∙ l" unfolding litsim_term_iff by blast
then have [simp]: "C = □"
and *: "∀x ∈ vars_term l. sop p x = σ x" using ctxt_permute_term [of s]
by auto metis+
then have "s = l ⋅ σ" by simp
have "∀x ∈ vars_term r. sop p x = σ x" using * and vc and ‹(l, r) ∈ R› by blast
then have "p ∙ r = r ⋅ σ"
by (metis term_apply_subst_Var_Rep_perm term_subst_eq)
then have "(s, p ∙ r) ∈ rstep R" and "u = p ∙ r" using ‹(l, r) ∈ R› by auto
have "r ∈ NF (rstep R)" using ‹(l, r) ∈ R› and rr by (auto simp: right_reduced_def)
then have "p ∙ r ∈ NF (rstep R)"
by (auto simp: NF_iff_no_step) (metis perm_rstep_perm rstep_permute_iff)
with ‹(u, t) ∈ (rstep R)⇧*› [unfolded ‹u = p ∙ r›, THEN NF_not_suc]
have "t = p ∙ r" by simp
with ‹(l, r) ∈ R› and ‹s = p ∙ l›
show ?thesis by auto
qed
lemma left_reduced_imp_lhs_min:
assumes "left_reduced R"
and "(l, r) ∈ R"
shows "∀t. l ⋅⊳ t ⟶ t ∈ NF (rstep R)"
proof (intro allI impI)
fix t
have *: "l ∈ NF (rstep (R - {(l, r)}))" using assms by (auto simp: left_reduced_def)
assume "l ⋅⊳ t"
show "t ∈ NF (rstep R)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain C σ l' r' where "(l', r') ∈ R"
and [simp]: "t = C⟨l' ⋅ σ⟩" by (auto simp: NF_iff_no_step)
have "(l', r') ∈ R - {(l, r)}"
proof (rule ccontr)
assume "¬ ?thesis"
with ‹(l', r') ∈ R› have [simp]: "l' = l" "r' = r" by auto
with ‹t = C⟨l' ⋅ σ⟩› have "t ⋅⊵ l" by (auto simp: encompeq.intros)
with ‹l ⋅⊳ t› show False by (auto simp: encomp_def)
qed
then have "(t, C⟨r' ⋅ σ⟩) ∈ rstep (R - {(l, r)})" by auto
moreover from ‹l ⋅⊳ t› obtain D τ where "l = D⟨t ⋅ τ⟩"
by (auto simp: encomp_def elim: encompeq.cases)
ultimately have "(l, D⟨(C⟨r' ⋅ σ⟩)⋅τ⟩) ∈ rstep (R - {(l, r)})" by blast
with * show False by (auto simp: NF_iff_no_step)
qed
qed
lemma reduced_NE_imp_unique':
assumes vc: "∀(l, r) ∈ S. vars_term r ⊆ vars_term l"
assumes "reduced R" and "right_reduced S"
and NE: "(rstep R)⇧! = (rstep S)⇧!"
shows "R ≤⋅ S"
proof
fix rule assume "rule ∈ R"
then obtain l and r where [simp]: "rule = (l, r)" and "(l, r) ∈ R" by (cases rule) auto
with ‹reduced R› have "r ∈ NF (rstep R)"
and "(l, r) ∈ rstep R" by (auto simp: reduced_def right_reduced_def)
then have "l ≠ r" and "(l, r) ∈ (rstep R)⇧!" by (auto simp: NF_iff_no_step)
then have "(l, r) ∈ (rstep S)⇧+" and "r ∈ NF (rstep S)"
unfolding NE by (auto dest: rtranclD simp: normalizability_def)
from left_reduced_imp_lhs_min [OF _ ‹(l, r) ∈ R›] and ‹reduced R›
have "∀t. l ⋅⊳ t ⟶ t ∈ NF (rstep R)" by (auto simp: reduced_def)
with NE have "∀t. l ⋅⊳ t ⟶ t ∈ NF (rstep S)" by auto
from right_reduced_min_step_rule [OF vc ‹right_reduced S› this ‹(l, r) ∈ (rstep S)⇧+›]
obtain p and l' r' where "(l', r') ∈ S" and "l = p ∙ l'" and "r = p ∙ r'" by blast
then have "-p ∙ rule ∈ S" by simp
then show "∃p. p ∙ rule ∈ S" by blast
qed
text ‹Normalization equivalent reduced TRSs are unique up to renaming.›
lemma reduced_NE_imp_unique:
assumes vc: "∀(l, r) ∈ R. vars_term r ⊆ vars_term l" "∀(l, r) ∈ S. vars_term r ⊆ vars_term l"
and "reduced R" and "reduced S"
and NE: "(rstep R)⇧! = (rstep S)⇧!"
shows "R ≐ S"
using reduced_NE_imp_unique' [OF vc(2) ‹reduced R› _ NE]
and reduced_NE_imp_unique' [OF vc(1) ‹reduced S› _ NE [symmetric]]
and ‹reduced R› and ‹reduced S› unfolding reduced_def subsumable_trs.litsim_def by force
locale reduction_order_infinite =
reduction_order less
for less :: "('f, 'v :: infinite) term ⇒ ('f, 'v) term ⇒ bool" (infix "≻" 50)
begin
lemma EQ_compat_imp_NE:
assumes "canonical R" and "canonical S"
and EQ: "(rstep R)⇧↔⇧* = (rstep S)⇧↔⇧*"
and compat: "R ⊆ {(x, y). x ≻ y}" "S ⊆ {(x, y). x ≻ y}"
shows "(rstep R)⇧! ⊆ (rstep S)⇧!"
proof -
have "reduced R" and "SN (rstep R)" and "CR (rstep R)"
using ‹canonical R› by (auto simp: canonical_def)
have "reduced S" and "SN (rstep S)" and "CR (rstep S)"
using ‹canonical S› by (auto simp: canonical_def)
interpret cR: complete_trs R by standard fact+
interpret cS: complete_trs S by standard fact+
show "(rstep R)⇧! ⊆ (rstep S)⇧!"
proof
fix s t
assume "(s, t) ∈ (rstep R)⇧!"
then have "t ∈ NF (rstep R)" by auto
define u where "u = some_NF (rstep S) t"
have "(t, u) ∈ (rstep S)⇧!" unfolding u_def by (rule cS.some_NF_NF')
then have "(t, u) ∈ (rstep R)⇧↔⇧*" by (auto simp: EQ)
then have "(u, t) ∈ (rstep R)⇧↔⇧*" by (metis conversion_inv)
with ‹t ∈ NF (rstep R)› have "(u, t) ∈ (rstep R)⇧!"
using CR_NF_conv [OF cR.CR] by blast
have "t = u"
proof (rule ccontr)
assume "t ≠ u"
with ‹(t, u) ∈ (rstep S)⇧!› and ‹(u, t) ∈ (rstep R)⇧!›
have "(t, u) ∈ (rstep S)⇧+" and "(u, t) ∈ (rstep R)⇧+" by (metis normalizability_E rtranclD)+
with compatible_rstep_trancl_imp_less and compat
have "t ≻ u" and "u ≻ t" by auto
then show False by (metis irrefl trans)
qed
with ‹(t, u) ∈ (rstep S)⇧!› have "t ∈ NF (rstep S)" by auto
moreover have "(s, t) ∈ (rstep R)⇧↔⇧*" using ‹(s, t) ∈ (rstep R)⇧!› by auto
ultimately show "(s, t) ∈ (rstep S)⇧!"
unfolding EQ using CR_NF_conv [OF cS.CR] by blast
qed
qed
lemma EQ_imp_litsim:
assumes vc: "∀(l, r) ∈ R. vars_term r ⊆ vars_term l"
"∀(l, r) ∈ S. vars_term r ⊆ vars_term l"
and canonical: "canonical R" "canonical S"
and "(rstep R)⇧↔⇧* = (rstep S)⇧↔⇧*"
and "R ⊆ {≻}" and "S ⊆ {≻}"
shows "R ≐ S"
proof -
from EQ_compat_imp_NE and assms(2-) have "(rstep R)⇧! = (rstep S)⇧!" by blast
from reduced_NE_imp_unique [OF vc _ _ this] and canonical
show ?thesis by (auto simp: canonical_def)
qed
end
end