Theory CR.Okui_subsumes_DC

text‹Okui Subsumes Development Closedness›

theory Okui_subsumes_DC
imports
  Development_Closed_Impl
  Okui_Criterion
begin

text‹Introduce definition to abbreviate Okui's criterion.›
definition
  "sim_cp_closed ren R ⟷ left_lin_wf_trs R ∧ 
  (∀A B. (A, B) ∈ ren.sim_cp ren R R ⟶ (∃v. (target A, v) ∈ (rstep R)⇧* ∧ (target B, v) ∈ mstep R))"

text‹Use definition from above to show confluence.›
lemma sim_cp_closed:
  assumes "sim_cp_closed renN R" 
  shows "CR (rstep R)" 
  using assms okui_imp_CR unfolding sim_cp_closed_def by auto

text‹Any TRS that passes the check for development closedness fulfills all requirements for Okui's 
criterion›
lemma dc_imp_sim_cp_closed:
  assumes "isOK(check_development_closed ren2 R n)" 
  shows "sim_cp_closed renN (set R)" 
proof-
  note assms = assms[unfolded check_development_closed_def, simplified, unfolded wf_trs_def']
  from assms have "⋀l r. (l, r) ∈ set R ⟹ is_Fun l" by auto
  moreover from assms have "⋀l r. (l, r) ∈ set R ⟹ vars_term r ⊆ vars_term l" by auto 
  moreover from assms have "left_linear_trs (set R)" by auto
  ultimately have wf_trs:"left_lin_wf_trs (set R)" 
    unfolding left_lin_wf_trs_def left_lin_def wf_trs_def no_var_lhs_def var_rhs_subset_lhs_def by blast
  moreover from assms have "⋀s t. (True, s, t) ∈ critical_pairs ren2 (set R) (set R) ⟹ ∃v. (s, v) ∈ mstep (set R) ∧ (t, v) ∈ (rstep (set R))⇧*" 
    using is_mstep_join by fastforce
  moreover from assms have "⋀s t. (False, s, t) ∈ critical_pairs ren2 (set R) (set R) ⟹ (s,t) ∈ mstep (set R)"
    by fastforce
  ultimately have "strongly_commute (mstep (set R)) (mstep (set R))" 
    using mstep_closed_strongly_commute by (metis (full_types) mstep_imp_rsteps mstep_refl) 
  from wf_trs this[unfolded strongly_commute_iff_sim_cps_joinable[OF wf_trs wf_trs, of renN]]
  show ?thesis unfolding sim_cp_closed_def by simp
qed

end