section ‹Main result for left-linear TRSs›
theory LS_Left_Linear
imports LS_Common
begin
locale weakly_layered_induct_left_linear = weakly_layered_induct ℱ 𝔏 ℛ rk
for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" and ℛ :: "('f, 'v) trs" and
rk :: nat +
fixes R :: "('f, 'v) term rel"
assumes ll: "left_linear_trs ℛ"
defines "R ≡ {}"
begin
lemma expand_mirror_step:
assumes "C' ∈ shallow_context" "C ≤ C'" "C' ≤ mctxt_of_term s" "((s, C), (t, D)) ∈ mirror_step"
obtains D' where "D' ∈ shallow_context" "D ≤ D'" "D' ≤ mctxt_of_term t" "((s, C'), (t, D')) ∈ mirror_step"
proof -
obtain l r p σ τ where *: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
"(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p τ"
using mirror_step.cases[OF assms(4)] by metis
then have "linear_term l" using ll by (force simp: left_linear_trs_def case_prod_unfold)
moreover have 2: "p ∈ all_poss_mctxt C" using *(2)
by (metis hole_pos_poss poss_mctxt_term_conv rstep_r_p_s'.cases)
moreover then have 3: "subm_at C p ≤ subm_at C' p" "p ∈ all_poss_mctxt C'"
using `C ≤ C'` all_poss_mctxt_mono[OF `C ≤ C'`] by (auto simp: less_eq_subm_at)
moreover have "mctxt_term_conv C |_ p = l ⋅ τ" using *(2) by auto
ultimately obtain τ' where 4: "mctxt_term_conv C' |_ p = l ⋅ τ'"
using linear_weak_match[of l "mctxt_term_conv C' |_ p" "mctxt_term_conv C |_ p" τ]
weak_match_mctxt_term_conv_mono[of "subm_at C p" "subm_at C' p"]
by (auto simp: left_linear_trs_def case_prod_unfold subt_at_mctxt_term_conv)
let ?d' = "replace_at (mctxt_term_conv C') p (r ⋅ τ')"
have 5: "(replace_at (mctxt_term_conv C') p (l ⋅ τ'),?d') ∈ rstep_r_p_s' ℛ (l, r) p τ'"
by (metis *(2) 3(2) fst_conv hole_pos_ctxt_of_pos_term poss_mctxt_term_conv prod.sel(2) rstep_r_p_s'E rstep_r_p_s'I)
have "term_mctxt_conv ?d' ∈ shallow_context"
by (metis 3(2) 4 5 rstep'_iff_rstep_r_p_s' shallow_context_closed[OF assms(1)] mctxt_term_conv_inv ctxt_supt_id poss_mctxt_term_conv)
moreover have "((s, C'), t, term_mctxt_conv ?d') ∈ mirror_step"
using 3 5 *(1) by (auto simp: 4[symmetric] ctxt_supt_id)
moreover have "D ≤ term_mctxt_conv ?d'"
using 3 5 *(2) assms(2) by (auto simp: 4[symmetric] ctxt_supt_id mirrored_steps_preserve_prefix)
ultimately show ?thesis using assms(3)
by (auto intro!: that[of "term_mctxt_conv ?d'"] simp: mirror_step_preserves_prefix)
qed
lemma short_step_from_mirror_steps:
assumes "C ∈ shallow_context"
"C ≤ mctxt_of_term s" "(s0, s) ∈ (rstep ℛ)⇧*" "s ∈ native_terms" "((s, C), (t, D)) ∈ mirror_step⇧*"
shows "(s, t) ∈ short_step_s s0"
proof -
obtain B ss where B: "(B, ss) = base_decomp s" by (metis prod.collapse)
then have "B ∈ shallow_context" "C ≤ B" "B ≤ mctxt_of_term s" using assms(1,2,4)
by (auto simp: native_terms_def base_decomp_shallow base_decomp_max base_decomp_prefix)
with assms(5)
obtain D' where "((s, B), (t, D')) ∈ mirror_step⇧*"
proof (induct "(s, C)" arbitrary: s B C thesis rule: converse_rtrancl_induct)
case (step z) show ?case using step(3)[OF prod.collapse[symmetric]]
expand_mirror_step[OF step(5,6,7), of "fst z" "snd z"] step(1,4)
by (metis converse_rtrancl_into_rtrancl prod.collapse)
qed auto
from short_step_sI[OF assms(3,4) B this] show ?thesis .
qed
lemma short_short_peak:
assumes "(s, t) ∈ short_step_s s0" "(s, u) ∈ short_step_s s1"
shows "(t, u) ∈ ((⋃i∈under R s0. short_step_s i)⇧↔)⇧* O (short_step_s s1)⇧= O
((⋃i∈under R s0 ∪ under R s1. short_step_s i)⇧↔)⇧* O
((short_step_s s0)¯)⇧= O ((⋃i∈under R s1. short_step_s i)⇧↔)⇧*"
proof -
obtain C D E v where "C ∈ shallow_context" "C ≤ mctxt_of_term t"
"D ∈ shallow_context" "D ≤ mctxt_of_term u"
"t ∈ native_terms" "(s1, t) ∈ (rstep ℛ)⇧*" "((t, C), v, E) ∈ mirror_step⇧*"
"u ∈ native_terms" "(s0, u) ∈ (rstep ℛ)⇧*" "((u, D), v, E) ∈ mirror_step⇧*"
using short_short_pre[OF assms, of thesis] by blast
then have "(t, v) ∈ short_step_s s1" "(u, v) ∈ short_step_s s0"
by (auto intro: short_step_from_mirror_steps)
then have "(t, u) ∈ (short_step_s s1)⇧= O ((short_step_s s0)¯)⇧=" by blast
then show ?thesis by regexp
qed
sublocale weakly_layered_induct_dd
using short_short_peak by unfold_locales (auto simp: R_def)
end
sublocale weakly_layered ⊆ weakly_layered_cr_ll
proof (standard, unfold rstep_eq_rstep', intro CR_main_lemma[where R = "λ_. {}"], goal_cases _ step)
case (step rk)
then interpret weakly_layered_induct_left_linear ℱ 𝔏 ℛ rk "{}" by (unfold_locales) simp_all
show ?case by unfold_locales
qed simp_all
lemmas (in weakly_layered) CR_ll = CR_ll
text ‹@{cite ‹Theorem 4.1› FMZvO15}›
thm weakly_layered.CR_ll
end