Theory Redundant_Rules (Isabelle2017: October 2017)

(*
Author:  Julian Nagele <julian.nagele@uibk.ac.at> (2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Redundant_Rules
imports
  QTRS.Trs
begin

lemma rsteps_union_simulate:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)^*"
  shows "(rstep R)^* = (rstep (R ∪ S))^*"
proof
  show "(rstep R)^* ⊆ (rstep (R ∪ S))^*"
    using rstep_mono[of R "R ∪ S"] rtrancl_mono by blast
  show "(rstep R)^* ⊇ (rstep (R ∪ S))^*"
  proof
    fix s t
    assume "(s, t) ∈ (rstep (R ∪ S))^*"
    then show "(s, t) ∈ (rstep R)^*"
    proof (induct rule: rtrancl_induct)
      case (step u t)
      then obtain l r C σ where ut: "(u, t) ∈ rstep_r_c_s (l, r) C σ" and lr: "(l, r) ∈ R ∪ S"
        unfolding rstep_iff_rstep_r_c_s by auto
      from lr have "(u, t) ∈ (rstep R)^*"
      proof
        assume "(l, r) ∈ R"
        with ut have "(u, t) ∈ rstep R" unfolding rstep_iff_rstep_r_c_s by auto
        thus ?thesis by auto
      next
        assume "(l, r) ∈ S"
        with assms have "(l, r) ∈ (rstep R)^*" by auto
        moreover from ut have "u = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩" unfolding rstep_r_c_s_def by auto
        ultimately show ?thesis using rsteps_closed_ctxt rsteps_closed_subst by metis
      qed
      then show ?case using step(3) by auto
    qed auto
  qed
qed

corollary redundant_rules:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)^*"
  shows "CR (rstep (R ∪ S)) ⟷ CR (rstep R)"
  unfolding CR_on_def join_def rtrancl_converse
  using rsteps_union_simulate[OF assms] by auto

(* TODO: move *)
lemma conversion_ctxt_closed:
  assumes "(s, t) ∈ (rstep R)⇧^↔⇧^*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧^↔⇧^*"
using assms rsteps_closed_ctxt
unfolding conversion_def
by (simp only: rstep_simps(5)[symmetric])

lemma conversion_subst_closed:
  assumes "(s, t) ∈ (rstep R)⇧^↔⇧^*"
  shows "(s ⋅ σ,  t ⋅ σ) ∈ (rstep R)⇧^↔⇧^*"
using assms rsteps_closed_subst
unfolding conversion_def
by (simp only: rstep_simps(5)[symmetric])


lemma rstep_simulate_conv:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)⇧^↔⇧^*"
  shows "(rstep S) ⊆ (rstep R)⇧^↔⇧^*"
proof
  fix s t
  assume "(s, t) ∈ rstep S"
  then obtain l r C σ where s: "s = C⟨l ⋅ σ⟩" and t:"t = C⟨r ⋅ σ⟩" and lr: "(l, r) ∈ S"
    unfolding rstep_iff_rstep_r_c_s rstep_r_c_s_def by auto
  with assms have "(l, r) ∈ (rstep R)⇧^↔⇧^*" by auto
  thus "(s, t) ∈ (rstep R)⇧^↔⇧^*" using conversion_ctxt_closed conversion_subst_closed s t by metis
qed

lemma symcl_simulate_conv:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)⇧^↔⇧^*"
  shows "(rstep S)⇧^↔ ⊆ (rstep R)⇧^↔⇧^*"
using rstep_simulate_conv[OF assms]
by (auto) (metis converseD conversion_inv reverseTrs subset_iff)

lemma conv_union_simulate:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)⇧^↔⇧^*"
  shows "(rstep (R ∪ S))⇧^↔⇧^* = (rstep R)⇧^↔⇧^*"
proof
  show "(rstep (R ∪ S))⇧^↔⇧^* ⊆ (rstep R)⇧^↔⇧^*"
    unfolding conversion_def
  proof
    fix s t
    assume "(s, t) ∈ ((rstep (R ∪ S))⇧^↔)⇧^*"
    then show "(s, t) ∈ ((rstep R)⇧^↔)⇧^*"
    proof (induct rule: rtrancl_induct)
      case (step u t)
      then have "(u, t) ∈ (rstep R)⇧^↔ ∨ (u, t) ∈ (rstep S)⇧^↔" by auto
      thus ?case
      proof
        assume "(u, t) ∈ (rstep R)⇧^↔"
        with step show ?thesis using rtrancl_into_rtrancl by metis
      next
        assume "(u, t) ∈ (rstep S)⇧^↔"
        with symcl_simulate_conv[OF assms] have "(u, t) ∈ (rstep R)⇧^↔⇧^*" by auto
        with step show ?thesis by auto
      qed
    qed simp
  qed
next
  show "(rstep R)⇧^↔⇧^* ⊆ (rstep (R ∪ S))⇧^↔⇧^*"
    unfolding conversion_def
    using rstep_union rtrancl_mono sup.cobounded1 symcl_Un
    by metis
qed

(* TODO : move *)
lemma join_mono:
  assumes "r ⊆ s"
  shows "r⇧^↓ ⊆ s⇧^↓"
  unfolding join_def
  using assms relcomp_mono rtrancl_mono converse_mono
by metis

lemma redundant_rules_removal:
  assumes "∀(l, r) ∈ S. (l, r) ∈ (rstep R)⇧^↔⇧^*"
  and "CR (rstep R)"
  shows "CR (rstep (R ∪ S))"
  using conv_union_simulate[OF assms(1)]
    CR_imp_conversionIff_join[OF assms(2)]
    join_mono[OF rstep_mono[of R "R ∪ S"]]
  unfolding CR_iff_conversion_imp_join
  by simp

end