Theory First_Order_Clause.Ground_Term_Rewrite_System

theory Ground_Term_Rewrite_System
  imports 
    Generic_Context 
    "Abstract-Rewriting.Abstract_Rewriting"
begin

locale ground_term_rewrite_system = 
  "context" where apply_context = apply_context 
  for apply_context :: "'c ⇒ 't ⇒ 't"
begin

definition compatible_with_context :: "'t rel ⇒ bool" where
  "compatible_with_context I ⟷ (∀t t' c. (t, t') ∈ I ⟶ (c⟨t⟩, c⟨t'⟩) ∈ I)"

lemma compatible_with_contextD:
  "compatible_with_context I ⟹ (t, t') ∈ I ⟹ (c⟨t⟩, c⟨t'⟩) ∈ I"
  by (simp add: compatible_with_context_def)

lemma compatible_with_context_converse:
  assumes "compatible_with_context I"
  shows "compatible_with_context (I¯)"
  unfolding compatible_with_context_def
proof (intro allI impI)
  fix t t' c
  assume "(t, t') ∈ I¯"
  thus "(c⟨t⟩, c⟨t'⟩) ∈ I¯"
    by (simp add: assms compatible_with_contextD)
qed

lemma compatible_with_context_symcl:
  assumes "compatible_with_context I"
  shows "compatible_with_context (I⇧↔)"
  unfolding compatible_with_context_def
proof (intro allI impI)
  fix t t' c
  assume "(t, t') ∈ I⇧↔"
  thus "(c⟨t⟩, c⟨t'⟩) ∈ I⇧↔"
    using assms compatible_with_contextD 
    by auto
qed

lemma compatible_with_context_rtrancl:
  assumes "compatible_with_context I"
  shows "compatible_with_context (I⇧*)"
  unfolding compatible_with_context_def
proof (intro allI impI)
  fix t t' c
  assume "(t, t') ∈ I⇧*"
  thus "(c⟨t⟩, c⟨t'⟩) ∈ I⇧*"
  proof (induction t' rule: rtrancl_induct)
    case base

    show ?case
      by simp
  next
    case (step y z)

    thus ?case
      using assms[unfolded compatible_with_context_def]
      by (meson rtrancl.rtrancl_into_rtrancl)
  qed
qed

lemma compatible_with_context_relcomp:
  assumes "compatible_with_context I1" and "compatible_with_context I2"
  shows "compatible_with_context (I1 O I2)"
  unfolding compatible_with_context_def
proof (intro allI impI)
  fix t t'' c
  assume "(t, t'') ∈ I1 O I2"

  then obtain t' where "(t, t') ∈ I1" and "(t', t'') ∈ I2"
    by auto

  have "(c⟨t⟩, c⟨t'⟩) ∈ I1"
    using ‹(t, t') ∈ I1› assms(1) compatible_with_contextD 
    by blast

  moreover have "(c⟨t'⟩, c⟨t''⟩) ∈ I2"
    using ‹(t', t'') ∈ I2› assms(2) compatible_with_contextD 
    by blast

  ultimately show "(c⟨t⟩, c⟨t''⟩) ∈ I1 O I2"
    by auto
qed

lemma compatible_with_context_join:
  assumes "compatible_with_context I"
  shows "compatible_with_context (I⇧↓)"
  using assms
  unfolding join_def
  by (simp add: compatible_with_context_relcomp compatible_with_context_rtrancl
        compatible_with_context_converse)

lemma compatible_with_context_conversion:
  assumes "compatible_with_context I"
  shows "compatible_with_context (I⇧↔⇧*)"
  using  assms
  unfolding conversion_def
  by (simp add: compatible_with_context_rtrancl compatible_with_context_symcl)

definition rewrite_in_context :: "'t rel ⇒ 't rel" where
  "rewrite_in_context R = {(c⟨t⇩1⟩, c⟨t⇩2⟩) | c t⇩1 t⇩2. (t⇩1, t⇩2) ∈ R}"

lemma mem_rewrite_in_context_if_mem_rewrite_rules[intro]:
  "(l, r) ∈ R ⟹ (l, r) ∈ rewrite_in_context R"   
  unfolding rewrite_in_context_def mem_Collect_eq
  by (metis apply_hole)

lemma context_mem_rewrite_in_context_if_mem_rewrite_rules[intro]:
  "(l, r) ∈ R ⟹ (c⟨l⟩, c⟨r⟩) ∈ rewrite_in_context R"
  by (auto simp: rewrite_in_context_def)

lemma rewrite_in_context_mono: "R ⊆ S ⟹ rewrite_in_context R ⊆ rewrite_in_context S"
  by (auto simp add: rewrite_in_context_def)

lemma rewrite_in_context_union:
  "rewrite_in_context (R ∪ S) = rewrite_in_context R ∪ rewrite_in_context S"
  by (auto simp add: rewrite_in_context_def)

lemma rewrite_in_context_insert:
  "rewrite_in_context (insert r R) = rewrite_in_context {r} ∪ rewrite_in_context R"
  using rewrite_in_context_union[of "{r}" R, simplified] .

lemma converse_rewrite_steps: "(rewrite_in_context R)¯ = rewrite_in_context (R¯)"
  by (auto simp: rewrite_in_context_def)

lemma rhs_lt_lhs_if_rule_in_rewrite_in_context:
  fixes less_trm :: "'t ⇒ 't ⇒ bool" (infix "≺⇩t" 50)
  assumes
    rule_in: "(t1, t2) ∈ rewrite_in_context R" and
    ball_R_rhs_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R ⟹ t2 ≺⇩t t1" and
    compatible_with_context: "⋀t1 t2 c. t2 ≺⇩t t1 ⟹ c⟨t2⟩ ≺⇩t c⟨t1⟩"
  shows "t2 ≺⇩t t1"
proof -
  from rule_in obtain t1' t2' c where
    "(t1', t2') ∈ R" and
    "t1 = c⟨t1'⟩" and
    "t2 = c⟨t2'⟩"
    by (auto simp: rewrite_in_context_def)

  from ball_R_rhs_lt_lhs have "t2' ≺⇩t t1'"
    using ‹(t1', t2') ∈ R› 
    by simp

  with compatible_with_context have "c⟨t2'⟩ ≺⇩t c⟨t1'⟩"
    by metis

  thus ?thesis
    using ‹t1 = c⟨t1'⟩› ‹t2 = c⟨t2'⟩› 
    by metis
qed

lemma mem_rewrite_step_union_NF:
  assumes "(t, t') ∈ rewrite_in_context (R1 ∪ R2)"
    "t ∈ NF (rewrite_in_context R2)"
  shows "(t, t') ∈ rewrite_in_context R1"
  using assms
  unfolding rewrite_in_context_union
  by blast

lemma predicate_holds_of_mem_rewrite_in_context:
  assumes rule_in: "(t1, t2) ∈ rewrite_in_context R" and
    ball_P: "⋀t1 t2. (t1, t2) ∈ R ⟹ P t1 t2" and
    preservation: "⋀t1 t2 c. (t1, t2) ∈ R ⟹ P t1 t2 ⟹ P c⟨t1⟩ c⟨t2⟩"
  shows "P t1 t2"
proof -
  from rule_in obtain t1' t2' c where
    "(t1', t2') ∈ R" and
    "t1 = c⟨t1'⟩" and
    "t2 = c⟨t2'⟩"
    by (auto simp: rewrite_in_context_def)

  thus ?thesis
    using ball_P[OF ‹(t1', t2') ∈ R›]
    using preservation[OF ‹(t1', t2') ∈ R›]
    by simp
qed

lemma compatible_with_context_rewrite_in_context [simp]:
  "compatible_with_context (rewrite_in_context E)"
  unfolding compatible_with_context_def rewrite_in_context_def mem_Collect_eq
  by (metis Pair_inject compose_context_iff)

lemma subset_rewrite_in_context [simp]: "E ⊆ rewrite_in_context E"
proof (rule Set.subsetI)
  fix e 
  assume e_in: "e ∈ E"

  moreover obtain s t where e_def: "e = (s, t)"
    by fastforce

  show "e ∈ rewrite_in_context E"
    unfolding rewrite_in_context_def mem_Collect_eq
  proof (intro exI conjI)
    show "e = (□⟨s⟩, □⟨t⟩)"
      unfolding e_def
      by simp
  next
    show "(s, t) ∈ E"
      using e_in
      unfolding e_def .
  qed
qed

lemma wf_converse_rewrite_in_context:
  fixes E :: "'t rel"
  assumes
    wfP_R: "wfP R" and
    R_compatible_with_context: "⋀c t t'. R t t' ⟹ R c⟨t⟩ c⟨t'⟩" and
    equations_subset_R: "⋀x y. (x, y) ∈ E ⟹ R y x"
  shows "wf ((rewrite_in_context E)¯)"
proof (rule wf_subset)
  from wfP_R show "wf {(x, y). R x y}"
    by (simp add: wfp_def)
next
  show "(rewrite_in_context E)¯ ⊆ {(x, y). R x y}"
  proof (rule Set.subsetI)
    fix e 
    assume "e ∈ (rewrite_in_context E)¯"

    then obtain c s t where e_def: "e = (c⟨s⟩, c⟨t⟩)" and "(t, s) ∈ E"
      by (smt (verit) Pair_inject converseE mem_Collect_eq rewrite_in_context_def)

    hence "R s t"
      using equations_subset_R 
      by simp

    hence "R c⟨s⟩ c⟨t⟩"
      using R_compatible_with_context 
      by simp

    then show "e ∈ {(x, y). R x y}"
      by (simp add: e_def)
  qed
qed

lemma rewrite_in_context_add_context [intro]:
  assumes "(s, t) ∈ (rewrite_in_context R)"
  shows "(c⟨s⟩, c⟨t⟩) ∈ (rewrite_in_context R)"
  using assms 
  unfolding rewrite_in_context_def mem_Collect_eq
  by (metis compose_context_iff prod.inject)

lemma rewrite_in_context_trancl_add_context [intro]:
  assumes "(s, t) ∈ (rewrite_in_context R)⇧*"
  shows "(c⟨s⟩, c⟨t⟩) ∈ (rewrite_in_context R)⇧*"
  using assms
proof (induction s t rule: rtrancl.induct)
  case rtrancl_refl

  show ?case
    by simp
next
  case (rtrancl_into_rtrancl t⇩1 t⇩2 t⇩3)

  then have "(c⟨t⇩2⟩, c⟨t⇩3⟩) ∈ rewrite_in_context R"
    by fast
 
  then show ?case
    using rtrancl_into_rtrancl(3)
    by simp
qed

end

end