section ‹Ordered Rewriting›
theory Ordered_Rewriting
imports
"../Orderings/Reduction_Order"
QTRS.Renaming_Interpretations
TA.Multihole_Context
begin
hide_const (open) Restricted_Predicates.total_on
hide_fact (open) Restricted_Predicates.total_on_def
lemma rtrancl_Restr:
assumes "(x, y) ∈ (Restr r A)⇧*"
shows "(x, y) ∈ r⇧*"
using assms by (induct) auto
lemma join_mono:
assumes "r ⊆ s"
shows "r⇧↓ ⊆ s⇧↓"
using rtrancl_mono [OF assms] by (auto simp: join_def rtrancl_converse)
lemma join_subst:
"subst.closed r ⟹ (s, t) ∈ r⇧↓ ⟹ (s ⋅ σ, t ⋅ σ) ∈ r⇧↓"
by (simp add: join_def subst.closedD subst.closed_comp subst.closed_converse subst.closed_rtrancl)
lemma replace_at_subst_steps:
fixes σ τ :: "('f, 'v) subst"
assumes acc: "all_ctxt_closed UNIV r"
and refl: "refl r"
and *: "⋀x. (σ x, τ x) ∈ r"
and "p ∈ poss t"
and "t |_ p = Var x"
shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ r"
using assms(4-)
proof (induction t arbitrary: p)
case (Var x)
then show ?case using refl by (simp add: refl_on_def)
next
case (Fun f ts)
then obtain i q where [simp]: "p = i <# q" and i: "i < length ts"
and q: "q ∈ poss (ts ! i)" and [simp]: "ts ! i |_ q = Var x" by (cases p) auto
let ?C = "ctxt_of_pos_term q (ts ! i ⋅ σ)"
let ?ts = "map (λt. t ⋅ τ) ts"
let ?ss = "take i (map (λt. t ⋅ σ) ts) @ ?C⟨τ x⟩ # drop (Suc i) (map (λt. t ⋅ σ) ts)"
have "∀j<length ts. (?ss ! j, ?ts ! j) ∈ r"
proof (intro allI impI)
fix j
assume j: "j < length ts"
moreover
{ assume [simp]: "j = i"
have "?ss ! j = ?C⟨τ x⟩" using i by (simp add: nth_append_take)
with Fun.IH [of "ts ! i" q]
have "(?ss ! j, ?ts ! j) ∈ r" using q and i by simp }
moreover
{ assume "j < i"
with i have "?ss ! j = ts ! j ⋅ σ"
and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_take_is_nth_conv)
then have "(?ss ! j, ?ts ! j) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
moreover
{ assume "j > i"
with i and j have "?ss ! j = ts ! j ⋅ σ"
and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_drop_is_nth_conv)
then have "(?ss ! j, ?ts ! j) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
ultimately show "(?ss ! j, ?ts ! j) ∈ r" by arith
qed
moreover have "i < length ts" by fact
ultimately show ?case
by (auto intro: all_ctxt_closedD [OF acc])
qed
inductive_set ordstep for ord :: "('f, 'v) term rel" and R :: "('f, 'v) trs"
where
"(l, r) ∈ R ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (l ⋅ σ, r ⋅ σ) ∈ ord ⟹ (s, t) ∈ ordstep ord R"
lemma ordstep_Un:
"ordstep ord (R ∪ R') = ordstep ord R ∪ ordstep ord R'"
by (auto intro: ordstep.intros elim: ordstep.cases)
lemma ordstep_imp_rstep:
"(s, t) ∈ ordstep ord R ⟹ (s, t) ∈ rstep R"
by (auto elim: ordstep.cases)
lemma ordstep_rstep_conv:
assumes "subst.closed ord" and "R ⊆ ord"
shows "ordstep ord R = rstep R"
using assms by (fast elim: ordstep.cases intro: ordstep.intros)
lemma ordstep_subst:
"subst.closed ord ⟹ (s, t) ∈ ordstep ord R ⟹ (s ⋅ σ, t ⋅ σ) ∈ ordstep ord R"
by (elim ordstep.cases, intro ordstep.intros [where C = "C ⋅⇩c σ" and σ = "τ ∘⇩s σ" for C τ]) auto
lemma subst_closed_ordstep [intro]:
"subst.closed ord ⟹ subst.closed (ordstep ord R)"
by (auto simp: ordstep_subst)
lemma ordstep_ctxt:
"(s, t) ∈ ordstep ord R ⟹ (C⟨s⟩, C⟨t⟩) ∈ ordstep ord R"
by (elim ordstep.cases, intro ordstep.intros [where C = "C ∘⇩c D" for D]) auto
lemma ordstep_subst_ctxt:
"subst.closed ord ⟹ (s, t) ∈ ordstep ord R ⟹ (C⟨s ⋅ σ⟩, C⟨t ⋅ σ⟩) ∈ ordstep ord R"
using ordstep_ctxt[OF ordstep_subst] by fast
lemma ordsteps_ctxt:
assumes "(s, t) ∈ (ordstep ord R)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (ordstep ord R)⇧*"
using assms by (induct) (auto simp: ordstep_ctxt rtrancl_into_rtrancl)
lemma ctxt_closed_ordstep [intro]:
"ctxt.closed (ordstep ord R)"
by (auto simp: ordstep_ctxt)
lemma all_ctxt_closed_ordsteps [simp]:
"all_ctxt_closed UNIV ((ordstep ord R)⇧*)"
by (rule trans_ctxt_imp_all_ctxt_closed) (auto simp: trans_def refl_on_def)
lemma ordstep_mono:
"R ⊆ R' ⟹ ord ⊆ ord' ⟹ ordstep ord R ⊆ ordstep ord' R'"
by (auto elim!: ordstep.cases intro: ordstep.intros)
lemma ordstep_imp_ord:
"ctxt.closed ord ⟹ (s, t) ∈ ordstep ord R ⟹ (s, t) ∈ ord"
by (elim ordstep.cases) auto
lemma ordsteps_imp_ordeq:
assumes "ctxt.closed ord" and "trans ord" and "(s, t) ∈ (ordstep ord R)⇧*"
shows "(s, t) ∈ ord⇧="
using assms(3) by (induct) (auto dest: ordstep_imp_ord [OF assms(1)] assms(2) [THEN transD])
lemma ordstep_rstep_conv':
assumes "subst.closed ord"
shows "ordstep ord R = rstep {(l ⋅ σ, r ⋅ σ) | l r σ. (l, r) ∈ R ∧ (l ⋅ σ, r ⋅ σ) ∈ ord}"
proof -
{ fix l r σ τ C assume "(l, r) ∈ R" and "(l ⋅ σ, r ⋅ σ) ∈ ord"
then have "(l ⋅ (σ ∘⇩s τ), r ⋅ (σ ∘⇩s τ)) ∈ ord" using ‹subst.closed ord› by auto
with ‹(l, r) ∈ R› have "(C⟨l ⋅ (σ ∘⇩s τ)⟩, C⟨r ⋅ (σ ∘⇩s τ)⟩) ∈ ordstep ord R"
by (intro ordstep.intros [where C = C and l = l and r = r and σ = "σ ∘⇩s τ"]) auto }
then show ?thesis
by (auto elim!: ordstep.cases) blast
qed
lemma ordstep_permute:
"(π ∙ s, π ∙ t) ∈ ordstep (π ∙ ord) (π ∙ R) ⟷ (s, t) ∈ ordstep ord R"
proof
assume "(π ∙ s, π ∙ t) ∈ ordstep (π ∙ ord) (π ∙ R)"
then obtain C l r σ where "(l, r) ∈ π ∙ R" and "π ∙ s = C⟨l ⋅ σ⟩" and "π ∙ t = C⟨r ⋅ σ⟩"
and "(l ⋅ σ, r ⋅ σ) ∈ π ∙ ord" by (cases)
moreover define D and τ where "D = -π ∙ C" and "τ = sop π ∘⇩s σ ∘⇩s sop (-π)"
ultimately have "s = D⟨-π ∙ l ⋅ τ⟩" and "t = D⟨-π ∙ r ⋅ τ⟩"
and "(-π ∙ l, -π ∙ r) ∈ R" and "(-π ∙ l ⋅ τ, -π ∙ r ⋅ τ) ∈ ord"
by (auto simp: eqvt [symmetric] term_pt.permute_flip)
then show "(s, t) ∈ ordstep ord R" by (intro ordstep.intros)
next
assume "(s, t) ∈ ordstep ord R"
then show "(π ∙ s, π ∙ t) ∈ ordstep (π ∙ ord) (π ∙ R)"
by (cases) (auto simp: eqvt, metis ordstep.intros rule_mem_trs_iff term_apply_subst_eqvt)
qed
definition "Req (R :: ('f, 'v) trs) eq true false s t =
{(Fun eq [Var (SOME x. True), Var (SOME x. True)], Fun true [])} ∪
{(Fun eq [s, t], Fun false [])} ∪ R"
lemma rstep_Req_true:
"(Fun eq [u, u], Fun true []) ∈ rstep (Req R eq true false s t)" (is "_ ∈ rstep ?R")
using rstepI [of "Fun eq [Var (SOME x. True), Var (SOME x. True)]" "Fun true []" ?R, OF _ refl refl, of □ "subst (SOME x. True) u"]
by (simp add: Req_def)
lemma rstep_Req_false:
"(Fun eq [s ⋅ σ, t ⋅ σ], Fun false []) ∈ rstep (Req R eq true false s t)" (is "_ ∈ rstep ?R")
using rstepI [of "Fun eq [s, t]" "Fun false []" ?R, OF _ refl refl, of □ σ]
by (simp add: Req_def)
lemma subset_Req: "R ⊆ Req R eq true false s t" by (auto simp: Req_def)
lemma subst_apply_set_const [simp]:
"A ⋅⇩s⇩e⇩t (λx. Fun f []) ⊆ {t. ground t}"
by auto
definition "GROUND R = Restr R {t. ground t}"
text ‹Ground confluence›
abbreviation "GCR R ≡ CR (GROUND R)"
lemma gterm_conv_GROUND_conv:
fixes s t :: "('f, 'v) term"
assumes ground: "ground s" "ground t"
assumes conv: "(s, t) ∈ (rstep R)⇧↔⇧*" (is "_ ∈ ?R⇧↔⇧*")
shows "(s, t) ∈ (GROUND (rstep R))⇧↔⇧*"
proof -
define c :: "('f, 'v) term" where "c = Fun (SOME f. True) []"
then have [simp]: "ground c" by simp
let ?γ = "λt. t ⋅ (λx. c)"
have "(?γ s, ?γ t) ∈ (GROUND ?R)⇧↔⇧*"
unfolding conversion_def
by (intro rtrancl_map [OF _ conv [unfolded conversion_def], of ?γ "(GROUND ?R)⇧↔"])
(force simp: GROUND_def)
then show ?thesis
using ground by (simp add: ground_subst_apply)
qed
lemma conversion_imp_ground_NF_eq:
fixes R :: "('f, 'v) trs"
assumes GCR: "GCR (ordstep ord S)"
and "subst.closed ord"
and gconv: "(GROUND (rstep (Req R eq true false s t)))⇧↔⇧* ⊆
(GROUND (ordstep ord S))⇧↔⇧*" (is "(GROUND ?R)⇧↔⇧* ⊆ (GROUND ?S)⇧↔⇧*")
and conv: "∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧↔⇧*"
shows "∀u v. (Fun true [], u) ∈ (GROUND (ordstep ord S))⇧! ∧
(Fun false [], v) ∈ (GROUND (ordstep ord S))⇧! ⟶ u = v"
proof (intro allI impI; elim conjE)
let ?true = "Fun true []"
fix u v assume "(Fun true [], u) ∈ (GROUND ?S)⇧!" (is "(?true, _) ∈ _")
and "(Fun false [], v) ∈ (GROUND ?S)⇧!" (is "(?false, _) ∈ _")
then have NFs: "u ∈ NF (GROUND ?S)" "v ∈ NF (GROUND ?S)" by auto
let ?γ = "λt. t ⋅ (λx. ?true)"
obtain σ where "(s ⋅ σ, t ⋅ σ) ∈ ?R⇧↔⇧*"
using conv and conversion_mono [of _ ?R, OF subset_Req [THEN rstep_mono]] by blast
then have "(Fun eq [s ⋅ σ, s ⋅ σ], Fun eq [s ⋅ σ, t ⋅ σ]) ∈ ?R⇧↔⇧*"
unfolding conversion_def by (intro args_steps_imp_steps) (auto simp: nth_Cons')
moreover have "(?true, Fun eq [s ⋅ σ, s ⋅ σ]) ∈ ?R⇧↔⇧*" and "(Fun eq [s ⋅ σ, t ⋅ σ], ?false) ∈ ?R⇧↔⇧*"
using rstep_Req_true [of eq "s ⋅ σ"] and rstep_Req_false
by (force simp: conversion_inv [of "Fun true []"])+
ultimately have "(?true, ?false) ∈ ?R⇧↔⇧*" by (blast dest: rtrancl_trans)
from gterm_conv_GROUND_conv [OF _ _ this]
have "(?γ ?true, ?γ ?false) ∈ (GROUND ?R)⇧↔⇧*" by simp
then have "(?true, ?false) ∈ (GROUND ?R)⇧↔⇧*" by simp
with gconv have "(?true, ?false) ∈ (GROUND ?S)⇧↔⇧*" by blast
with CR_imp_conversionIff_join [OF GCR [unfolded GROUND_def], folded GROUND_def]
obtain w where "(?true, w) ∈ (GROUND ?S)⇧*"
and "(?false, w) ∈ (GROUND ?S)⇧*" by blast
moreover have "ground ?true" and "ground ?false" by auto
ultimately have "(w, u) ∈ (GROUND ?S)⇧*" and "(w, v) ∈ (GROUND ?S)⇧*"
using GCR and ‹(?true, u) ∈ (GROUND ?S)⇧!› and ‹(?false, v) ∈ (GROUND ?S)⇧!›
by (meson CR_join_right_I NF_join_imp_reach joinI_right normalizability_E)+
then show "u = v"
using GCR and NFs by (auto simp: CR_defs dest: join_NF_imp_eq simp del: ground_subst)
qed
lemma infeasibility_via_GCR:
assumes "GCR (ordstep ord S)"
and "subst.closed ord"
and "(GROUND (rstep (Req R eq true false s t)))⇧↔⇧* ⊆
(GROUND (ordstep ord S))⇧↔⇧*" (is "(GROUND ?R)⇧↔⇧* ⊆ (GROUND ?S)⇧↔⇧*")
and "(Fun true [], u) ∈ (GROUND (ordstep ord S))⇧! ∧
(Fun false [], v) ∈ (GROUND (ordstep ord S))⇧! ∧ u ≠ v"
shows "¬ (∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧*)"
using conversion_imp_ground_NF_eq [OF assms(1-3)] and assms(4) by blast
locale least_element =
fixes r A
assumes SN: "SN (Restr r A)"
and total: "total_on A r"
and trans: "trans (Restr r A)"
begin
definition "least_elt = (THE x. x ∈ A ∧ (∀y. (x, y) ∈ (Restr r A) ⟶ y = x))"
lemma least_ex:
assumes "x ∈ A"
shows "∃y. (x, y) ∈ (Restr r A)⇧= ∧ (∀z. (y, z) ∈ (Restr r A) ⟶ z = y)"
using SN and assms
proof (induct rule: SN_induct [consumes 1])
case (1 x)
then show ?case
proof (cases "∀y. (x, y) ∈ (Restr r A) ⟶ y = x")
case False
then obtain y where "(x, y) ∈ (Restr r A)" "y ∈ A" and "y ≠ x" by blast
with 1 show ?thesis using trans [THEN transD] by blast
qed blast
qed
lemma least_ex1:
assumes "x ∈ A"
shows "∃!y. y ∈ A ∧ (∀z. (y, z) ∈ (Restr r A) ⟶ z = y)"
using least_ex [OF assms] and total [unfolded total_on_def] and assms by blast
lemma least_elt:
assumes "x ∈ A"
shows "least_elt ∈ A ∧ (∀y. (least_elt, y) ∈ (Restr r A) ⟶ y = least_elt)"
using theI' [OF least_ex1 [OF assms], folded least_elt_def] .
end
context reduction_order
begin
lemma infeasibility_via_GCR:
assumes "GCR (ordstep {≻} S)"
and "(GROUND (rstep (Req R eq true false s t)))⇧↔⇧* ⊆ (GROUND (ordstep {≻} S))⇧↔⇧*"
and "(Fun true [], u) ∈ (GROUND (ordstep {≻} S))⇧!"
and "(Fun false [], v) ∈ (GROUND (ordstep {≻} S))⇧!"
and "u ≠ v"
shows "¬ (∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧*)"
using infeasibility_via_GCR [OF assms(1) subst_closed_less assms(2)] and assms(3-) by simp
end
definition "ooverlap ord R r r' p μ u v ⟷
(∃p. p ∙ r ∈ R) ∧ (∃p. p ∙ r' ∈ R) ∧ vars_rule r ∩ vars_rule r' = {} ∧
p ∈ funposs (fst r') ∧
mgu (fst r) (fst r' |_ p) = Some μ ∧
(snd r ⋅ μ, fst r ⋅ μ) ∉ ord ∧ (snd r' ⋅ μ, fst r' ⋅ μ) ∉ ord ∧
u = replace_at (fst r' ⋅ μ) p (snd r ⋅ μ) ∧
v = snd r' ⋅ μ"
lemma ooverlapI:
"π ∙ (l, r) ∈ R ⟹ π' ∙ (l', r') ∈ R ⟹ vars_rule (l, r) ∩ vars_rule (l', r') = {} ⟹
p ∈ funposs l' ⟹ mgu l (l' |_ p) = Some μ ⟹
(r ⋅ μ, l ⋅ μ) ∉ ord ⟹ (r' ⋅ μ, l' ⋅ μ) ∉ ord ⟹
ooverlap ord R (l, r) (l', r') p μ (replace_at (l' ⋅ μ) p (r ⋅ μ)) (r' ⋅ μ)"
by (force simp: ooverlap_def)
lemma GROUND_subset: "GROUND R ⊆ R" by (auto simp: GROUND_def)
lemma GROUND_not_ground:
assumes "(s, t) ∈ (GROUND R)⇧*" and "¬ ground s"
shows "t = s"
using assms by (induct) (auto simp: GROUND_def)
lemma GROUND_rtrancl:
assumes "(s, t) ∈ (GROUND R)⇧*" and "ground s"
shows "ground t ∧ (s, t) ∈ R⇧*"
using assms by (induct) (auto simp: GROUND_def)
context reduction_order
begin
lemma ground_less:
assumes "ground s" and "s ≻ t"
shows "ground t"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain x where "x ∈ vars_term t" by (induct t) auto
then obtain C where "t = C⟨Var x⟩" by (auto dest: supteq_Var)
then have [simp]: "s ≻ (C ⋅⇩c subst x s)⟨s⟩"
using ‹s ≻ t› [THEN subst, of "subst x s"] and ‹ground s› by (simp add: ground_subst_apply)
define f where "f n = ((C ⋅⇩c subst x s) ^ n)⟨s⟩" for n
then have "f i ≻ f (Suc i)" for i
by (induct i) (simp_all add: ctxt)
with SN_less show False by (auto simp: SN_defs)
qed
lemma ordstep_GROUND:
"ground s ⟹ (s, t) ∈ ordstep {≻} R ⟹ (s, t) ∈ GROUND (ordstep {≻} R)"
by (auto simp: GROUND_def dest: ordstep_imp_ord [OF ctxt_closed_less] ground_less)
lemma ordsteps_GROUND:
assumes "(s, t) ∈ (ordstep {≻} R)⇧*" and "ground s"
shows "ground t ∧ (s, t) ∈ (GROUND (ordstep {≻} R))⇧*"
using assms
by (induct rule: rtrancl_induct)
(auto dest!: ordstep_GROUND, auto simp: GROUND_def)
lemma ordstep_join_GROUND:
assumes "ground s" and "ground t" and "(s, t) ∈ (ordstep {≻} R)⇧↓"
shows "(s, t) ∈ (GROUND (ordstep {≻} R))⇧↓"
using assms by (auto simp: join_def rtrancl_converse dest: ordsteps_GROUND)
lemma GCR_eq_CR_GROUND:
"GCR (ordstep {≻} R) = CR (GROUND (ordstep {≻} R))"
by (auto simp: CR_defs dest!: ordsteps_GROUND)
end
locale gtotal_reduction_order_inf =
gtotal_reduction_order less
for less :: "('a, 'b::infinite) term ⇒ ('a, 'b) term ⇒ bool" (infix "≻" 50)
begin
lemma ordstep_join:
assumes ground: "ground s" "ground t"
and R: "⋀s t. (s, t) ∈ R ⟹ s ≻ t ∨ (t, s) ∈ R"
and *: "(s, t) ∈ (ordstep {≻} R)⇧↓ ∨ (∃l r σ. (l, r) ∈ R⇧↔ ∧ s = l ⋅ σ ∧ t = r ⋅ σ)"
shows "(s, t) ∈ (ordstep {≻} R)⇧↓"
using *
proof (elim disjE exE conjE)
fix l r σ assume "(l, r) ∈ R⇧↔" and "s = l ⋅ σ" and "t = r ⋅ σ"
then have "(s, t) ∈ ((ordstep {≻} R)⇧↔)⇧="
using gtotal [OF ground]
apply (auto simp del: ground_subst intro: ordstep.intros [where C = □ and σ = σ] simp: subst)
apply (frule R)
apply (auto intro: ordstep.intros [where C = □ and σ = σ] simp: subst)
apply (frule R)
apply (auto intro: ordstep.intros [where C = □ and σ = σ] simp: subst)
done
then show "(s, t) ∈ (ordstep {≻} R)⇧↓" by blast
qed
lemma perm_less:
"π ∙ s ≻ π ∙ t ⟷ s ≻ t"
using subst [of "π ∙ s" "π ∙ t" "sop (-π)"]
and subst [of s t "sop π"]
by auto
lemma non_ooverlap_GROUND_joinable:
assumes R: "⋀s t. (s, t) ∈ R ⟹ s ≻ t ∨ (t, s) ∈ R"
and s1: "s = C⇩1⟨l⇩1 ⋅ σ⇩1⟩" and s2: "s = C⇩2⟨l⇩2 ⋅ σ⇩2⟩"
and vpos: "hole_pos C ∉ funposs l⇩2"
and [simp]: "C⇩1 = C⇩2 ∘⇩c C"
and lr⇩1: "(l⇩1 ⋅ σ⇩1, r⇩1 ⋅ σ⇩1) ∈ ordstep {≻} R" (is "_ ∈ ?R")
and lr⇩2: "(l⇩2 ⋅ σ⇩2, r⇩2 ⋅ σ⇩2) ∈ ordstep {≻} R"
and t: "t = C⇩1⟨r⇩1 ⋅ σ⇩1⟩"
and u: "u = C⇩2⟨r⇩2 ⋅ σ⇩2⟩"
and ground: "ground t" "ground u"
and "π ∙ (l⇩2, r⇩2) ∈ R"
shows "(t, u) ∈ (GROUND ?R)⇧↓" (is "_ ∈ ?G⇧↓")
proof -
note ordstep = ordstep.intros [where C = □ and ord = "{≻}", OF _ refl refl, simplified]
have rule⇩2: "(π ∙ l⇩2, π ∙ r⇩2) ∈ R" using assms by (auto simp: eqvt)
show ?thesis
proof(cases "C = □")
case True
hence "hole_pos C = ε" by auto
with vpos obtain x where x: "l⇩2 = Var x" using poss_is_Fun_funposs
by (metis empty_pos_in_poss is_VarE subt_at.simps(1))
show ?thesis
proof (cases "x ∈ vars_term r⇩2")
case True
then obtain C where C:"r⇩2 = C⟨Var x⟩" by (auto dest: vars_term_supteq)
from lr⇩2 ctxt have [simp]: "l⇩2 ⋅ σ⇩2 ≻ (C ⋅⇩c σ⇩2)⟨l⇩2 ⋅ σ⇩2⟩" unfolding ordstep.simps x C by auto
define h where "h n = ((C ⋅⇩c σ⇩2) ^ n)⟨l⇩2 ⋅ σ⇩2⟩" for n
then have "h i ≻ h (Suc i)" for i by (induct i) (simp_all add: ctxt)
with SN_less show ?thesis by (auto simp: SN_defs)
next
case False
with R [OF rule⇩2] and subst [of l⇩2 r⇩2 "subst x r⇩2"] and SN_less
have rl2: "(π ∙ r⇩2, π ∙ l⇩2) ∈ R"
using perm_less [of π "Var x" r⇩2]
by (force simp: x)
define τ where "τ = (λz. if z = x then r⇩1 ⋅ σ⇩1 else σ⇩2 z)"
have t1:"l⇩2 ⋅ τ = r⇩1 ⋅ σ⇩1" unfolding x τ_def by auto
with assms have g1: "ground (l⇩2 ⋅ τ)" by simp
from False have t2: "r⇩2 ⋅ τ = r⇩2 ⋅ σ⇩2" unfolding τ_def by (simp add: term_subst_eq_conv)
with assms have g2: "ground (r⇩2 ⋅ τ)" by simp
from gtotal [OF g2 g1] and ordstep [OF rl2, of "sop (-π) ∘⇩s τ"]
and ordstep [OF rule⇩2, of "sop (-π) ∘⇩s τ"]
have "(l⇩2 ⋅ τ, r⇩2 ⋅ τ) ∈ ?R ∨ (r⇩2 ⋅ τ, l⇩2 ⋅ τ) ∈ ?R ∨ r⇩2 ⋅ τ = l⇩2 ⋅ τ" by force
with ordstep_ctxt have "(u, t) ∈ ?R ∨ (t, u) ∈ ?R ∨ u = t"
unfolding assms True t1 t2 by fastforce
then show ?thesis
using ground by (auto dest: ordstep_GROUND)
qed
next
case False
have eq: "l⇩2 ⋅ σ⇩2 = C⟨l⇩1 ⋅ σ⇩1⟩" using s1 and s2 by simp
define p where "p = hole_pos C"
have C: "C = ctxt_of_pos_term p (l⇩2 ⋅ σ⇩2)" by (simp add: p_def eq)
have "p ∉ funposs l⇩2" using vpos by (simp add: p_def)
moreover have "p ∈ poss (l⇩2 ⋅ σ⇩2)" by (simp add: eq p_def)
ultimately obtain q⇩1 and q⇩2 and x where p: "p = q⇩1 <#> q⇩2" and q⇩1: "q⇩1 ∈ poss l⇩2"
and lq⇩1: "l⇩2 |_ q⇩1 = Var x" and q⇩2: "q⇩2 ∈ poss (σ⇩2 x)"
by (blast intro: poss_subst_apply_term)
moreover have [simp]: "l⇩2 ⋅ σ⇩2 |_ p = l⇩1 ⋅ σ⇩1" by (simp add: eq p_def)
ultimately have [simp]: "σ⇩2 x |_ q⇩2 = l⇩1 ⋅ σ⇩1" by simp
define δ where "δ y = (if y = x then replace_at (σ⇩2 x) q⇩2 (r⇩1 ⋅ σ⇩1) else σ⇩2 y)" for y
have δ_x: "δ x = replace_at (σ⇩2 x) q⇩2 (r⇩1 ⋅ σ⇩1)" by (simp add: δ_def)
have "(σ⇩2 x, δ x) ∈ ?R"
using ordstep_ctxt [OF lr⇩1, of "ctxt_of_pos_term q⇩2 (σ⇩2 x)"] and q⇩2
by (simp add: δ_def replace_at_ident)
then have *: "⋀x. (σ⇩2 x, δ x) ∈ ?R⇧*" by (auto simp: δ_def)
then have "(r⇩2 ⋅ σ⇩2, r⇩2 ⋅ δ) ∈ ?R⇧*"
using all_ctxt_closed_subst_step [OF all_ctxt_closed_ordsteps] by metis
then have u1: "(u, C⇩2⟨r⇩2 ⋅ δ⟩) ∈ ?R⇧*" by (auto simp: u ordsteps_ctxt)
have t1: "(t, C⇩2⟨l⇩2 ⋅ δ⟩) ∈ ?R⇧*"
proof -
have "C⟨r⇩1 ⋅ σ⇩1⟩ = replace_at (l⇩2 ⋅ σ⇩2) q⇩1 (δ x)"
using q⇩1 and q⇩2 by (simp add: δ_def ctxt_of_pos_term_append lq⇩1 C p)
moreover
have "(replace_at (l⇩2 ⋅ σ⇩2) q⇩1 (δ x), l⇩2 ⋅ δ) ∈ ?R⇧*"
by (rule replace_at_subst_steps [OF all_ctxt_closed_ordsteps refl_rtrancl * q⇩1 lq⇩1])
ultimately show ?thesis by (simp add: t ordsteps_ctxt)
qed
consider "(C⇩2⟨l⇩2 ⋅ δ⟩, C⇩2⟨r⇩2 ⋅ δ⟩) ∈ ?R⇧=" | "(C⇩2⟨r⇩2 ⋅ δ⟩, C⇩2⟨l⇩2 ⋅ δ⟩) ∈ ?R"
proof -
have "ground (l⇩2 ⋅ δ)" and "ground (r⇩2 ⋅ δ)"
using ‹ground t› and ‹ground u› and t1 and u1 by (auto dest: ordsteps_GROUND)
from gtotal [OF this]
show ?thesis
using R [OF rule⇩2] and ordstep [OF rule⇩2, of "sop (-π) ∘⇩s δ", simplified]
and ordstep [of "π ∙ r⇩2" "π ∙ l⇩2" R "sop (-π) ∘⇩s δ", simplified]
and irrefl
by (auto dest: subst trans simp: perm_less ordstep_ctxt intro: that)
qed
then show ?thesis
proof (cases)
case 1
with t1 have "(t, C⇩2⟨r⇩2 ⋅ δ⟩) ∈ ?R⇧*" by auto
with u1 show ?thesis using ‹ground u› and ‹ground t› by (auto dest!: ordsteps_GROUND)
next
case 2
with u1 have "(u, C⇩2⟨l⇩2 ⋅ δ⟩) ∈ ?R⇧*" by auto
with t1 show ?thesis using ‹ground u› and ‹ground t› by (auto dest!: ordsteps_GROUND)
qed
qed
qed
lemma GCR_ordstep:
assumes ooverlaps: "⋀r r' p μ u v. ooverlap {≻} R r r' p μ u v ⟹
(u, v) ∈ (ordstep {≻} R)⇧↓ ∨ (∃l r σ. (l, r) ∈ R⇧↔ ∧ u = l ⋅ σ ∧ v = r ⋅ σ)"
and R: "⋀s t. (s, t) ∈ R ⟹ s ≻ t ∨ (t, s) ∈ R"
shows "GCR (ordstep {≻} R)" (is "CR (GROUND ?R)" is "CR ?G")
proof
fix s t' u' assume st: "(s, t') ∈ ?G⇧*" and su: "(s, u') ∈ ?G⇧*"
then show "(t', u') ∈ ?G⇧↓"
proof (induct s arbitrary: t' u' rule: SN_induct [OF SN_less])
case less: (1 s)
have *: "r⇧* = r O r⇧* ∪ Id" for r :: "('a, 'b) term rel" by regexp
consider t and u where "ground s"
and "(s, t) ∈ ?G" and "(t, t') ∈ ?G⇧*" and "ground t"
and "(s, u) ∈ ?G" and "(u, u') ∈ ?G⇧*" and "ground u" | "s = t'" | "s = u'"
using less.prems by (subst (asm) (3 4) *) (auto simp: GROUND_def)
then show ?case using less.prems
proof (cases)
case 1
moreover have "s ≻ t" and "s ≻ u"
using 1 by (auto simp: GROUND_def dest: ordstep_imp_ord [OF ctxt_closed_less])
moreover obtain v where tv: "(t, v) ∈ ?G⇧*" and "(u, v) ∈ ?G⇧*"
proof -
obtain C⇩1 and C⇩2 and σ and σ⇩2 and l and l⇩2 and r and r⇩2
where "(l, r) ∈ R" and "l ⋅ σ ≻ r ⋅ σ" and s1: "s = C⇩1⟨l ⋅ σ⟩" and t: "t = C⇩1⟨r ⋅ σ⟩"
and "(l⇩2, r⇩2) ∈ R" and "l⇩2 ⋅ σ⇩2 ≻ r⇩2 ⋅ σ⇩2" and s2: "s = C⇩2⟨l⇩2 ⋅ σ⇩2⟩" and u: "u = C⇩2⟨r⇩2 ⋅ σ⇩2⟩"
using 1(2, 5) by (auto simp: GROUND_def) (fast elim: ordstep.cases)
then have lr: "(l ⋅ σ, r ⋅ σ) ∈ ?R" and lr⇩2: "(l⇩2 ⋅ σ⇩2, r⇩2 ⋅ σ⇩2) ∈ ?R"
and "0 ∙ (l, r) ∈ R"
by (auto intro: ordstep.intros [where C = □])
obtain π where "vars_rule (π ∙ (l, r)) ∩ vars_rule (l⇩2, r⇩2) = {}"
using vars_rule_disjoint by blast
moreover define l⇩1 and r⇩1 and σ⇩1 where "l⇩1 = π ∙ l" and "r⇩1 = π ∙ r" and "σ⇩1 = sop (-π) ∘⇩s σ"
ultimately have disj: "vars_rule (l⇩1, r⇩1) ∩ vars_rule (l⇩2, r⇩2) = {}" by (auto simp: eqvt)
have "l⇩1 ⋅ σ⇩1 ≻ r⇩1 ⋅ σ⇩1" using ‹l ⋅ σ ≻ r ⋅ σ› by (simp add: l⇩1_def σ⇩1_def r⇩1_def)
have t': "t = C⇩1⟨r⇩1 ⋅ σ⇩1⟩" by (auto simp: t r⇩1_def σ⇩1_def)
have rule⇩1: "-π ∙ (l⇩1, r⇩1) ∈ R" and rule⇩2: "0 ∙ (l⇩2, r⇩2) ∈ R"
using ‹(l, r) ∈ R› and ‹(l⇩2, r⇩2) ∈ R› unfolding l⇩1_def r⇩1_def by simp_all
define τ where "τ x = (if x ∈ vars_rule (l⇩1, r⇩1) then σ⇩1 x else σ⇩2 x)" for x
then have τ: "l⇩1 ⋅ τ = l⇩1 ⋅ σ⇩1" "l⇩2 ⋅ τ = l⇩2 ⋅ σ⇩2" "r⇩1 ⋅ τ = r⇩1 ⋅ σ⇩1" "r⇩2 ⋅ τ = r⇩2 ⋅ σ⇩2"
using disj by (auto simp: vars_defs term_subst_eq_conv)
have s_mctxt: "s = fill_holes (mctxt_of_ctxt C⇩1) [l ⋅ σ]" by (simp add: s1)
have t_mctxt: "t = fill_holes (mctxt_of_ctxt C⇩1) [r ⋅ σ]" by (simp add: t)
have u_mctxt: "u = fill_holes (mctxt_of_ctxt C⇩2) [r⇩2 ⋅ σ⇩2]" by (simp add: u)
show ?thesis using s1 and s2
proof (cases rule: two_subterms_cases)
case eq
then have "l⇩2 ⋅ τ = l⇩1 ⋅ τ" unfolding τ by (auto simp: l⇩1_def σ⇩1_def)
then obtain μ where mgu: "mgu l⇩2 l⇩1 = Some μ"
using mgu_complete by (auto simp: unifiers_def simp del: mgu.simps)
then have "is_mgu μ {(l⇩2, l⇩1)}" by (simp add: mgu_sound is_imgu_imp_is_mgu)
with ‹l⇩2 ⋅ τ = l⇩1 ⋅ τ› obtain δ where τ': "τ = μ ∘⇩s δ" by (auto simp: is_mgu_def unifiers_def)
then have τ'': "t ⋅ μ ⋅ δ = t ⋅ τ" for t by simp
have not_less: "(r⇩1 ⋅ μ, l⇩1 ⋅ μ) ∉ {≻}" "(r⇩2 ⋅ μ, l⇩2 ⋅ μ) ∉ {≻}"
using ‹l⇩1 ⋅ σ⇩1 ≻ r⇩1 ⋅ σ⇩1› and ‹l⇩2 ⋅ σ⇩2 ≻ r⇩2 ⋅ σ⇩2› and irrefl
by (auto dest!: subst [of "r⇩1 ⋅ μ" "l⇩1 ⋅ μ" δ] subst [of "r⇩2 ⋅ μ" "l⇩2 ⋅ μ" δ] simp: τ'' τ dest: trans)
show ?thesis
proof (cases l⇩1)
case (Fun f ls)
with ooverlapI [OF rule⇩2 rule⇩1 _ _ _ not_less(2,1), of ε] and mgu and disj
have "ooverlap {≻} R (l⇩2, r⇩2) (l⇩1, r⇩1) ε μ (r⇩2 ⋅ μ) (r⇩1 ⋅ μ)" by auto
from ooverlaps [OF this]
have "(r⇩1 ⋅ τ, r⇩2 ⋅ τ) ∈ ?R⇧↓ ∨ (∃l r σ. (l, r) ∈ R⇧↔ ∧ r⇩1 ⋅ τ = l ⋅ σ ∧ r⇩2 ⋅ τ = r ⋅ σ)"
using join_subst [OF subst_closed_ordstep [OF subst_closed_less], of _ _ R]
apply (auto simp: τ')
using subst_subst apply blast+
done
from ordstep_join [OF _ _ R this] and 1 have "(r⇩1 ⋅ σ⇩1, r⇩2 ⋅ σ⇩2) ∈ ?R⇧↓" by (auto simp: τ t' u)
then have "(t, u) ∈ ?R⇧↓" apply (auto simp: t' u)
by (simp add: eq(1) join_ctxt ordstep_rstep_conv' subst_closed_less)
then obtain v where "(t, v) ∈ ?G⇧*" and "(u, v) ∈ ?G⇧*"
using 1 by (auto dest!: ordsteps_GROUND)
then show ?thesis by (intro that)
next
case (Var x)
with ‹l⇩1 = π ∙ l› have "hole_pos □ ∉ funposs l"
by (metis equals0D funposs.simps(1) funposs_perm_simp)
from non_ooverlap_GROUND_joinable [OF R s2 s1 this _ lr⇩2 lr u t ‹ground u› ‹ground t› ‹0 ∙ (l, r) ∈ R›]
have ut:"(t, u) ∈ ?G⇧↓" unfolding eq by auto
then show ?thesis by (elim joinE) (blast intro: that)
qed
next
case [simp]: (parallel1 C)
have "fill_holes C [r ⋅ σ, l⇩2 ⋅ σ⇩2] =⇩f (mctxt_of_ctxt C⇩1, concat [[r ⋅ σ],[]])"
unfolding parallel1 by (intro fill_holes_mctxt_sound) (auto, case_tac i, auto)
then have t: "t = fill_holes C [r ⋅ σ, l⇩2 ⋅ σ⇩2]" using t_mctxt by (auto dest: eqfE)
have "fill_holes C [l ⋅ σ, r⇩2 ⋅ σ⇩2] =⇩f (mctxt_of_ctxt C⇩2, concat [[], [r⇩2 ⋅ σ⇩2]])"
unfolding parallel1 by (intro fill_holes_mctxt_sound) (auto, case_tac i, auto)
then have u: "u = fill_holes C [l ⋅ σ, r⇩2 ⋅ σ⇩2]" using u_mctxt by (auto dest: eqfE)
from ctxt_imp_mctxt [OF _ lr, of C "[]" "[r⇩2 ⋅ σ⇩2]"] and ordstep_ctxt [of _ _ "{≻}" R]
have "(u, fill_holes C [r ⋅ σ, r⇩2 ⋅ σ⇩2]) ∈ ?G⇧*" using 1 by (auto simp: u ordstep_GROUND)
moreover from ctxt_imp_mctxt [OF _ lr⇩2, of C "[r ⋅ σ]" "[]"] and ordstep_ctxt [of _ _ "{≻}" R]
have "(t, fill_holes C [r ⋅ σ, r⇩2 ⋅ σ⇩2]) ∈ ?G⇧*" using 1 by (auto simp: t ordstep_GROUND)
ultimately show ?thesis by (intro that)
next
case [simp]: (parallel2 C)
have "fill_holes C [l⇩2 ⋅ σ⇩2, r ⋅ σ] =⇩f (mctxt_of_ctxt C⇩1, concat [[], [r ⋅ σ]])"
unfolding parallel2 by (intro fill_holes_mctxt_sound) (auto, case_tac i, auto)
then have t: "t = fill_holes C [l⇩2 ⋅ σ⇩2, r ⋅ σ]" using t_mctxt by (auto dest: eqfE)
have "fill_holes C [r⇩2 ⋅ σ⇩2, l ⋅ σ] =⇩f (mctxt_of_ctxt C⇩2, concat [[r⇩2 ⋅ σ⇩2], []])"
unfolding parallel2 by (intro fill_holes_mctxt_sound) (auto, case_tac i, auto)
then have u: "u = fill_holes C [r⇩2 ⋅ σ⇩2, l ⋅ σ]" using u_mctxt by (auto dest: eqfE)
from ctxt_imp_mctxt [OF _ lr, of C "[r⇩2 ⋅ σ⇩2]" "[]"] and ordstep_ctxt [of _ _ "{≻}" R]
have "(u, fill_holes C [r⇩2 ⋅ σ⇩2, r ⋅ σ]) ∈ ?G⇧*" using 1 by (auto simp: u ordstep_GROUND)
moreover from ctxt_imp_mctxt [OF _ lr⇩2, of C "[]" "[r ⋅ σ]"] and ordstep_ctxt [of _ _ "{≻}" R]
have "(t, fill_holes C [r⇩2 ⋅ σ⇩2, r ⋅ σ]) ∈ ?G⇧*" using 1 by (auto simp: t ordstep_GROUND)
ultimately show ?thesis by (intro that)
next
case [simp]: (nested1 C)
have eq: "l⇩2 ⋅ σ⇩2 = C⟨l ⋅ σ⟩" using s1 and s2 by simp
define p where "p = hole_pos C"
have C: "C = ctxt_of_pos_term p (l⇩2 ⋅ σ⇩2)" by (simp add: p_def eq)
show ?thesis
proof (cases "p ∈ funposs l⇩2")
case False
from non_ooverlap_GROUND_joinable [OF R s1 s2 False [unfolded p_def] nested1(2) lr lr⇩2 t u ‹ground t› ‹ground u› ‹0 ∙ (l⇩2, r⇩2) ∈ R›]
have "(t, u) ∈ ?G⇧↓" .
then show ?thesis by (elim joinE) (blast intro: that)
next
case True
have "l⇩1 ⋅ τ = l⇩2 |_ p ⋅ τ"
unfolding funposs_imp_poss [OF True, THEN subt_at_subst, symmetric] τ eq
by (simp add: l⇩1_def σ⇩1_def p_def)
then obtain μ where mgu: "mgu l⇩1 (l⇩2 |_ p) = Some μ"
using mgu_complete by (auto simp: unifiers_def simp del: mgu.simps)
then have "is_mgu μ {(l⇩1, l⇩2 |_ p)}" by (simp add: mgu_sound is_imgu_imp_is_mgu)
with ‹l⇩1 ⋅ τ = l⇩2 |_ p ⋅ τ› obtain δ where τ': "τ = μ ∘⇩s δ" by (auto simp: is_mgu_def unifiers_def)
then have τ'': "t ⋅ μ ⋅ δ = t ⋅ τ" for t by auto
have not_less: "(r⇩1 ⋅ μ, l⇩1 ⋅ μ) ∉ {≻}" "(r⇩2 ⋅ μ, l⇩2 ⋅ μ) ∉ {≻}"
using ‹l⇩1 ⋅ σ⇩1 ≻ r⇩1 ⋅ σ⇩1› and ‹l⇩2 ⋅ σ⇩2 ≻ r⇩2 ⋅ σ⇩2› and irrefl
by (auto dest!: subst [of "r⇩1 ⋅ μ" "l⇩1 ⋅ μ" δ] subst [of "r⇩2 ⋅ μ" "l⇩2 ⋅ μ" δ] simp: τ'' τ dest: trans)
let ?u = "r⇩2 ⋅ μ" and ?v = "(ctxt_of_pos_term p (l⇩2 ⋅ μ))⟨r⇩1 ⋅ μ⟩"
from ooverlapI [OF rule⇩1 rule⇩2 disj True mgu not_less, THEN ooverlaps] and disj
have *: "(?u ⋅ δ, ?v ⋅ δ) ∈ ?R⇧↓ ∨ (∃l r σ. (l, r) ∈ R⇧↔ ∧ ?u ⋅ δ = l ⋅ σ ∧ ?v ⋅ δ = r ⋅ σ)"
using join_subst [OF subst_closed_ordstep [OF subst_closed_less], of _ _ R]
by (metis (no_types, lifting) converse.intros join_sym subst_subst symcl_converse)
have "(?u ⋅ δ, ?v ⋅ δ) ∈ ?R⇧↓"
using 1 and τ' and t' and u and τ and funposs_imp_poss [OF True]
apply (intro ordstep_join [OF _ _ R *])
apply (auto simp: C)
by (metis ctxt_of_pos_term_subst poss_imp_subst_poss)
then have "(u, t) ∈ ?R⇧↓"
using funposs_imp_poss [OF True]
by (auto simp: t' u τ'' ctxt_of_pos_term_subst [symmetric] τ C join_ctxt ordstep_rstep_conv' subst_closed_less)
then obtain v where "(t, v) ∈ ?G⇧*" and "(u, v) ∈ ?G⇧*"
using 1 by (auto dest!: ordsteps_GROUND)
then show ?thesis by (intro that)
qed
next
case [simp]: (nested2 C)
have eq: "l ⋅ σ = C⟨l⇩2 ⋅ σ⇩2⟩" using s1 and s2 by (simp)
have eq⇩1: "l⇩1 ⋅ σ⇩1 = C⟨l⇩2 ⋅ σ⇩2⟩" using s1 and s2 by (simp add: l⇩1_def σ⇩1_def)
define p where "p = hole_pos C"
have C: "C = ctxt_of_pos_term p (l ⋅ σ)" by (simp add: p_def eq)
have C': "C = ctxt_of_pos_term p (l⇩1 ⋅ σ⇩1)" by (simp add: p_def eq l⇩1_def σ⇩1_def)
show ?thesis
proof (cases "p ∈ funposs l")
case False
from non_ooverlap_GROUND_joinable [OF R s2 s1 False [unfolded p_def] nested2(2) lr⇩2 lr u t ‹ground u› ‹ground t› ‹0 ∙ (l, r) ∈ R›]
have "(u, t) ∈ ?G⇧↓" .
then show ?thesis by (elim joinE) (blast intro: that)
next
case True
then have funposs: "p ∈ funposs l⇩1" by (auto simp: l⇩1_def)
have "l⇩2 ⋅ τ = l⇩1 |_ p ⋅ τ"
unfolding funposs_imp_poss [OF funposs, THEN subt_at_subst, symmetric] τ eq⇩1
by (simp add: p_def)
then obtain μ where mgu: "mgu l⇩2 (l⇩1 |_ p) = Some μ"
using mgu_complete by (auto simp: unifiers_def simp del: mgu.simps)
then have "is_mgu μ {(l⇩2, l⇩1 |_ p)}" by (simp add: mgu_sound is_imgu_imp_is_mgu)
with ‹l⇩2 ⋅ τ = l⇩1 |_ p ⋅ τ› obtain δ where τ': "τ = μ ∘⇩s δ" by (auto simp: is_mgu_def unifiers_def)
then have τ'': "t ⋅ μ ⋅ δ = t ⋅ τ" for t by auto
have not_less: "(r⇩1 ⋅ μ, l⇩1 ⋅ μ) ∉ {≻}" "(r⇩2 ⋅ μ, l⇩2 ⋅ μ) ∉ {≻}"
using ‹l⇩1 ⋅ σ⇩1 ≻ r⇩1 ⋅ σ⇩1› and ‹l⇩2 ⋅ σ⇩2 ≻ r⇩2 ⋅ σ⇩2› and irrefl
by (auto dest!: subst [of "r⇩1 ⋅ μ" "l⇩1 ⋅ μ" δ] subst [of "r⇩2 ⋅ μ" "l⇩2 ⋅ μ" δ] simp: τ'' τ dest: trans)
let ?u = "r⇩1 ⋅ μ" and ?v = "(ctxt_of_pos_term p (l⇩1 ⋅ μ))⟨r⇩2 ⋅ μ⟩"
from ooverlapI [OF rule⇩2 rule⇩1 _ funposs mgu not_less(2,1), THEN ooverlaps] and disj
have *: "(?u ⋅ δ, ?v ⋅ δ) ∈ ?R⇧↓ ∨ (∃l r σ. (l, r) ∈ R⇧↔ ∧ ?u ⋅ δ = l ⋅ σ ∧ ?v ⋅ δ = r ⋅ σ)"
using join_subst [OF subst_closed_ordstep [OF subst_closed_less], of _ _ R]
by (metis (no_types, lifting) converse.intros inf_commute join_sym subst_subst symcl_converse)
have "(?u ⋅ δ, ?v ⋅ δ) ∈ ?R⇧↓"
using 1 and τ' and t' and u and τ and funposs_imp_poss [OF funposs]
apply (intro ordstep_join [OF _ _ R *])
apply (auto simp: C)
by (metis ctxt_of_pos_term_subst eq eq⇩1 poss_imp_subst_poss)
then have "(u, t) ∈ ?R⇧↓"
using funposs_imp_poss [OF funposs]
by (auto simp: t' u τ'' ctxt_of_pos_term_subst [symmetric] τ C' join_ctxt ordstep_rstep_conv' subst_closed_less)
then obtain v where "(t, v) ∈ ?G⇧*" and "(u, v) ∈ ?G⇧*"
using 1 by (auto dest!: ordsteps_GROUND)
then show ?thesis by (intro that)
qed
qed
qed
ultimately have "(t', v) ∈ ?G⇧↓" and "(v, u') ∈ ?G⇧↓" by (auto simp: less.hyps)
then obtain t'' and u'' where t't'': "(t', t'') ∈ ?G⇧*" and "(v, t'') ∈ ?G⇧*"
and "(v, u'') ∈ ?G⇧*" and u'u'': "(u', u'') ∈ ?G⇧*" by blast
moreover have "s ≻ v"
using 1 and tv
by (auto simp: GROUND_def dest!: ordstep_imp_ord [OF ctxt_closed_less] ordsteps_imp_ordeq [OF ctxt_closed_less trans_less] rtrancl_Restr)
(auto dest: trans)
ultimately have "(t'', u'') ∈ ?G⇧↓" by (auto simp: less.hyps)
then show ?thesis using t't'' and u'u'' by (blast dest: join_rtrancl_join rtrancl_join_join)
qed auto
qed
qed
end
text ‹Minimal ordered rewrite steps.›
inductive_set mordstep for c and ord :: "('f, 'v) term rel" and R :: "('f, 'v) trs"
where
"(l, r) ∈ R ⟹ (l ⋅ σ, r ⋅ σ) ∈ ord ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹
∀x ∈ vars_term r - vars_term l. σ x = Fun c [] ⟹
(s, t) ∈ mordstep c ord R"
lemma mordstep_mono:
"ord ⊆ ord' ⟹ mordstep c ord R ⊆ mordstep c ord' R"
by (auto elim!: mordstep.cases intro: mordstep.intros)
lemma mordstep_ordstep:
"mordstep c ord R ⊆ ordstep ord R"
by (auto elim!: mordstep.cases intro: ordstep.intros)
definition "ext_subst σ t c x = (if x ∈ vars_term t then σ x else Fun c [])"
lemma subst_ext_subst:
"vars_term s ⊆ vars_term t ⟹ s ⋅ ext_subst σ t c = s ⋅ σ"
by (intro term_subst_eq) (auto simp: ext_subst_def)
lemma subst_ext_subst': "t ⋅ ext_subst σ t c = t ⋅ σ"
by (auto simp: subst_ext_subst)
lemma ext_subst_restrict [simp]:
"ext_subst (σ |s vars_term t) t c = ext_subst σ t c"
by (auto simp: ext_subst_def)
lemma ext_subst:
"∀x ∈ vars_term r - vars_term l. ext_subst σ l c x = Fun c []"
by (auto simp: ext_subst_def)
lemma (in reduction_order) ext_subst_less:
assumes min_const: "∀t. ground t ⟶ t ≽ Fun c []"
and "ground (t ⋅ σ)"
shows "t ⋅ σ ≽ t ⋅ ext_subst σ s c"
using assms(2)
proof (induct t)
case (Var x)
then show ?case using min_const by (auto simp: ext_subst_def)
next
case (Fun f ts)
let ?Σ = "λi. drop i (map (λt. t ⋅ σ) ts)"
let ?C = "λi. take i (map (λt. t ⋅ ext_subst σ s c) ts)"
have *: "∀t ∈ set ts. t ⋅ σ ≽ t ⋅ ext_subst σ s c" using Fun by auto
have "Fun f ts ⋅ σ ≽ Fun f (?C i @ ?Σ i)" if "i ≤ length ts" for i
using that
proof (induct i)
case (Suc i)
then have "ts ! i ⋅ σ ≽ ts ! i ⋅ ext_subst σ s c" using * by force
with ctxt [of "ts ! i ⋅ σ" "ts ! i ⋅ ext_subst σ s c" "More f (?C i) □ (?Σ (Suc i))"]
have "Fun f (?C i @ ?Σ i) ≽ Fun f (?C (Suc i) @ ?Σ (Suc i))"
using Suc.prems and Cons_nth_drop_Suc [of i "map (λt. t ⋅ σ) ts"]
by (cases "i < length ts") (auto simp add: take_Suc_conv_app_nth)
moreover have "Fun f ts ⋅ σ ≽ Fun f (?C i @ ?Σ i)" using Suc by simp
ultimately show ?case by (auto dest: trans)
qed simp
from this [of "length ts"] show ?case by simp
qed
lemma (in reduction_order) mordstep_complete:
assumes min_const: "∀t. ground t ⟶ t ≽ Fun c []"
and ground: "ground s"
and step: "(s, t) ∈ ordstep {≻} R"
shows "∃u. (s, u) ∈ mordstep c {≻} R"
using ordstep_GROUND [OF ground step] and step
apply (auto elim!: ordstep.cases)
apply (rule_tac x = "C⟨r ⋅ ext_subst σ l c⟩" in exI)
apply (rule_tac l = l and r = r and σ = "ext_subst σ l c" and C = C in mordstep.intros)
apply (auto simp: subst_ext_subst)
apply (subgoal_tac "r ⋅ σ ≽ r ⋅ ext_subst σ l c")
apply (auto dest: trans)
using ext_subst_less [OF min_const]
apply (auto simp: GROUND_def ext_subst_def)
done
lemma FGROUND_subset: "FGROUND F R ⊆ R" by (auto simp: FGROUND_def)
lemma mordstep_FGROUND:
assumes "(c, 0) ∈ F" "funas_trs R ⊆ F" "fground F s"
and "(s, t) ∈ mordstep c ord R"
shows "(s, t) ∈ (FGROUND F (mordstep c ord R))"
using assms
apply (auto elim!: mordstep.cases simp: FGROUND_def fground_def)
apply blast
apply (auto simp: funas_term_subst)
apply (meson contra_subsetD rhs_wf)
apply (case_tac "x ∈ vars_term r - vars_term l")
apply auto
done
lemma FGROUND_GROUND:
"(s, t) ∈ FGROUND F R ⟹ (s, t) ∈ GROUND R"
by (auto simp: FGROUND_def GROUND_def fground_def)
lemma GROUND_mono:
"R ⊆ S ⟹ GROUND R ⊆ GROUND S"
by (auto simp: GROUND_def)
lemma FGROUND_mono:
"R ⊆ S ⟹ FGROUND F R ⊆ FGROUND F S"
by (auto simp: FGROUND_def)
lemma rtrancl_FGROUND_GROUND:
assumes "(s, t) ∈ (FGROUND F R)⇧*"
shows "(s, t) ∈ (GROUND R)⇧*"
using assms by (induct) (auto dest: FGROUND_GROUND)
lemma rtrancl_FGROUND_fground:
assumes "(s, t) ∈ (FGROUND F R)⇧*" and "fground F s"
shows "fground F t ∧ (s, t) ∈ R⇧*"
using assms by (induct) (auto simp: FGROUND_def)
lemma mordsteps_FGROUND:
assumes "(c, 0) ∈ F" "funas_trs R ⊆ F" "fground F s"
and "(s, t) ∈ (mordstep c ord R)⇧*"
shows "(s, t) ∈ (FGROUND F (mordstep c ord R))⇧*"
using assms(4, 1-3) by (induct) (auto dest: rtrancl_FGROUND_fground mordstep_FGROUND)
lemma (in reduction_order) suborder_mordstep_NF:
assumes *: "{(x, y). ord x y} ⊆ {≻}" (is "?O ⊆ {≻}") and "reduction_order ord"
and fground: "∀s t. fground F s ∧ fground F t ⟶ s = t ∨ ord s t ∨ ord t s"
and min: "∀t. ground t ⟶ t ≽ Fun c []"
and F: "(c, 0) ∈ F" "funas_trs R ⊆ F" "fground F t"
and NF: "t ∈ NF (FGROUND F (mordstep c {(x, y). ord x y} R))"
shows "t ∈ NF (GROUND (ordstep {≻} R))"
proof (rule ccontr)
interpret ord: reduction_order ord by fact
assume "¬ ?thesis"
then obtain u' where "(t, u') ∈ GROUND (ordstep {≻} R)" by blast
then have "ground t" and "(t, u') ∈ ordstep {≻} R" by (auto simp: GROUND_def)
from mordstep_complete [OF min this] obtain u where "(t, u) ∈ mordstep c {≻} R" by blast
from mordstep_FGROUND [OF F this] have "(t, u) ∈ FGROUND F (mordstep c {≻} R)" .
with * and fground have "(t, u) ∈ FGROUND F (mordstep c ?O R)"
apply (auto simp: FGROUND_def fground_def simp del: ground_subst elim!: mordstep.cases)
apply (subgoal_tac "ord (l ⋅ σ) (r ⋅ σ)")
apply (auto simp del: ground_subst intro: mordstep.intros)
by (metis (mono_tags, hide_lams) Collect_mono_iff irrefl local.trans old.prod.case)
then show False using NF by blast
qed
lemma (in reduction_order) SN_ordstep:
"SN (ordstep {≻} R)"
by (rule SN_subset [OF SN_less]) (auto dest: ordstep_imp_ord [OF ctxt_closed_less])
lemma (in reduction_order) SN_mordstep:
"SN (mordstep c {≻} R)"
by (rule SN_subset [OF SN_less])
(auto dest: mordstep_ordstep [THEN subsetD] ordstep_imp_ord [OF ctxt_closed_less])
lemma (in reduction_order) SN_FGROUND_ordstep:
"SN (FGROUND F (ordstep {≻} R))"
by (rule SN_subset [OF SN_ordstep, of _ R]) (rule FGROUND_subset)
lemma (in reduction_order) SN_FGROUND_mordstep:
"SN (FGROUND F (mordstep c {≻} R))"
by (rule SN_subset [OF SN_mordstep, of _ _ R]) (rule FGROUND_subset)
lemma (in reduction_order) GCR_imp_CR_FGROUND:
assumes *: "{(x, y). ord x y} ⊆ {≻}" (is "?O ⊆ _")
and ro: "reduction_order ord"
and fground: "∀s t. fground F s ∧ fground F t ⟶ s = t ∨ ord s t ∨ ord t s"
and min: "∀t. ground t ⟶ t ≽ Fun c []"
and F: "(c, 0) ∈ F" "funas_trs R ⊆ F"
and GCR: "GCR (ordstep {≻} R)" (is "CR (GROUND ?R)" is "CR ?G")
shows "CR (FGROUND F (ordstep ?O R))" (is "CR (FGROUND F ?S)" is "CR ?F")
proof
let ?M = "mordstep c ?O R"
have [dest!]: "⋀s t. (s, t) ∈ (GROUND (ordstep ?O R))⇧* ⟹ (s, t) ∈ ?G⇧*"
by (rule rtrancl_mono [of "GROUND (ordstep ?O R)", THEN subsetD], rule GROUND_mono)
(auto dest!: mordstep_ordstep [THEN subsetD] ordstep_mono [OF subset_refl *, THEN subsetD])
have [dest!]: "⋀s t. (s, t) ∈ (FGROUND F ?M)⇧* ⟹ (s, t) ∈ ?F⇧*"
by (rule rtrancl_mono [of "FGROUND F ?M", THEN subsetD], rule FGROUND_mono)
(auto dest: mordstep_ordstep [THEN subsetD])
have [dest!]: "⋀s t. (s, t) ∈ (GROUND ?M)⇧* ⟹ (s, t) ∈ ?G⇧*"
by (rule rtrancl_mono [of "GROUND ?M", THEN subsetD], rule GROUND_mono)
(auto dest!: mordstep_ordstep [THEN subsetD] ordstep_mono [OF subset_refl *, THEN subsetD])
fix s t u assume st: "(s, t) ∈ ?F⇧*" and su: "(s, u) ∈ ?F⇧*"
then consider "s = t" | "fground F s"
by (metis FGROUND_def Int_iff converse_rtranclE mem_Collect_eq mem_Sigma_iff)
then show "(t, u) ∈ ?F⇧↓"
proof (cases)
case 1 then show ?thesis using st and su by auto
next
case 2
interpret ord: reduction_order ord by fact
obtain t' and u' where tt': "(t, t') ∈ (FGROUND F ?M)⇧!"
and uu': "(u, u') ∈ (FGROUND F ?M)⇧!"
using SN_imp_WN [OF ord.SN_FGROUND_mordstep, of F c R]
by (force simp: WN_on_def)
then have "fground F t'" and "fground F u'"
using st and su
using 2 by (auto simp: normalizability_def dest: rtrancl_FGROUND_fground)
then have "(s, t') ∈ ?G⇧*" and "t' ∈ NF ?G" and "(s, u') ∈ ?G⇧*" and "u' ∈ NF ?G"
using tt' and uu' and st and su
by (auto simp: normalizability_def dest!: rtrancl_FGROUND_GROUND
intro!: suborder_mordstep_NF [OF * ro fground min F])
with GCR have "t' = u'"
by (meson CR_divergence_imp_join join_NF_imp_eq)
then show ?thesis using tt' and uu' by (auto simp: normalizability_def)
qed
qed
lemma GCR_imp_conversion_imp_join:
assumes "GCR (rstep ℛ)" and "ground s" and "ground t" and "(s, t) ∈ (rstep ℛ)⇧↔⇧*"
shows "(s, t) ∈ (rstep ℛ)⇧↓"
proof -
from assms and gterm_conv_GROUND_conv have "(s, t) ∈ (GROUND (rstep ℛ))⇧↔⇧*" by auto
with assms(1) have "(s, t) ∈ (GROUND (rstep ℛ))⇧↓" unfolding CR_iff_conversion_imp_join by force
with GROUND_subset [THEN join_mono] show ?thesis by auto
qed
end