Theory Term_Rewrite_System

theory Term_Rewrite_System
  imports
    Regular_Tree_Relations.Ground_Ctxt
begin

definition compatible_with_gctxt :: "'f gterm rel ⇒ bool" where
  "compatible_with_gctxt I ⟷ (∀t t' ctxt. (t, t') ∈ I ⟶ (ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ I)"

lemma compatible_with_gctxtD:
  "compatible_with_gctxt I ⟹ (t, t') ∈ I ⟹ (ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ I"
  by (simp add: compatible_with_gctxt_def)

lemma compatible_with_gctxt_converse:
  assumes "compatible_with_gctxt I"
  shows "compatible_with_gctxt (I¯)"
  unfolding compatible_with_gctxt_def
proof (intro allI impI)
  fix t t' ctxt
  assume "(t, t') ∈ I¯"
  thus "(ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ I¯"
    by (simp add: assms compatible_with_gctxtD)
qed

lemma compatible_with_gctxt_symcl:
  assumes "compatible_with_gctxt I"
  shows "compatible_with_gctxt (I⇧↔)"
  unfolding compatible_with_gctxt_def
proof (intro allI impI)
  fix t t' ctxt
  assume "(t, t') ∈ I⇧↔"
  thus "(ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ I⇧↔"
  proof (induction ctxt arbitrary: t t')
    case GHole
    thus ?case by simp
  next
    case (GMore f ts1 ctxt ts2)
    thus ?case
      using assms[unfolded compatible_with_gctxt_def, rule_format]
      by blast
  qed
qed

lemma compatible_with_gctxt_rtrancl:
  assumes "compatible_with_gctxt I"
  shows "compatible_with_gctxt (I⇧*)"
  unfolding compatible_with_gctxt_def
proof (intro allI impI)
  fix t t' ctxt
  assume "(t, t') ∈ I⇧*"
  thus "(ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ 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_gctxt_def, rule_format]
      by (meson rtrancl.rtrancl_into_rtrancl)
  qed
qed

lemma compatible_with_gctxt_relcomp:
  assumes "compatible_with_gctxt I1" and "compatible_with_gctxt I2"
  shows "compatible_with_gctxt (I1 O I2)"
  unfolding compatible_with_gctxt_def
proof (intro allI impI)
  fix t t'' ctxt
  assume "(t, t'') ∈ I1 O I2"
  then obtain t' where "(t, t') ∈ I1" and "(t', t'') ∈ I2"
    by auto

  have "(ctxt⟨t⟩⇩G, ctxt⟨t'⟩⇩G) ∈ I1"
    using ‹(t, t') ∈ I1› assms(1) compatible_with_gctxtD by blast
  moreover have "(ctxt⟨t'⟩⇩G, ctxt⟨t''⟩⇩G) ∈ I2"
    using ‹(t', t'') ∈ I2› assms(2) compatible_with_gctxtD by blast
  ultimately show "(ctxt⟨t⟩⇩G, ctxt⟨t''⟩⇩G) ∈ I1 O I2"
    by auto
qed

lemma compatible_with_gctxt_join:
  assumes "compatible_with_gctxt I"
  shows "compatible_with_gctxt (I⇧↓)"
  using assms
  by (simp_all add: join_def compatible_with_gctxt_relcomp compatible_with_gctxt_rtrancl
      compatible_with_gctxt_converse)

lemma compatible_with_gctxt_conversion:
  assumes "compatible_with_gctxt I"
  shows "compatible_with_gctxt (I⇧↔⇧*)"
  by (simp add: assms compatible_with_gctxt_rtrancl compatible_with_gctxt_symcl conversion_def)

definition rewrite_inside_gctxt :: "'f gterm rel ⇒ 'f gterm rel" where
  "rewrite_inside_gctxt R = {(ctxt⟨t1⟩⇩G, ctxt⟨t2⟩⇩G) | ctxt t1 t2. (t1, t2) ∈ R}"

lemma mem_rewrite_inside_gctxt_if_mem_rewrite_rules[intro]:
  "(l, r) ∈ R ⟹ (l, r) ∈ rewrite_inside_gctxt R"
  by (metis (mono_tags, lifting) CollectI gctxt_apply_term.simps(1) rewrite_inside_gctxt_def)

lemma ctxt_mem_rewrite_inside_gctxt_if_mem_rewrite_rules[intro]:
  "(l, r) ∈ R ⟹ (ctxt⟨l⟩⇩G, ctxt⟨r⟩⇩G) ∈ rewrite_inside_gctxt R"
  by (auto simp: rewrite_inside_gctxt_def)

lemma rewrite_inside_gctxt_mono: "R ⊆ S ⟹ rewrite_inside_gctxt R ⊆ rewrite_inside_gctxt S"
  by (auto simp add: rewrite_inside_gctxt_def)

lemma rewrite_inside_gctxt_union:
  "rewrite_inside_gctxt (R ∪ S) = rewrite_inside_gctxt R ∪ rewrite_inside_gctxt S"
  by (auto simp add: rewrite_inside_gctxt_def)

lemma rewrite_inside_gctxt_insert:
  "rewrite_inside_gctxt (insert r R) = rewrite_inside_gctxt {r} ∪ rewrite_inside_gctxt R"
  using rewrite_inside_gctxt_union[of "{r}" R, simplified] .

lemma converse_rewrite_steps: "(rewrite_inside_gctxt R)¯ = rewrite_inside_gctxt (R¯)"
  by (auto simp: rewrite_inside_gctxt_def)

lemma rhs_lt_lhs_if_rule_in_rewrite_inside_gctxt:
  fixes less_trm :: "'f gterm ⇒ 'f gterm ⇒ bool" (infix "≺⇩t" 50)
  assumes
    rule_in: "(t1, t2) ∈ rewrite_inside_gctxt R" and
    ball_R_rhs_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R ⟹ t2 ≺⇩t t1" and
    compatible_with_gctxt: "⋀t1 t2 ctxt. t2 ≺⇩t t1 ⟹ ctxt⟨t2⟩⇩G ≺⇩t ctxt⟨t1⟩⇩G"
  shows "t2 ≺⇩t t1"
proof -
  from rule_in obtain t1' t2' ctxt where
    "(t1', t2') ∈ R" and
    "t1 = ctxt⟨t1'⟩⇩G" and
    "t2 = ctxt⟨t2'⟩⇩G"
    by (auto simp: rewrite_inside_gctxt_def)

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

  with compatible_with_gctxt have "ctxt⟨t2'⟩⇩G ≺⇩t ctxt⟨t1'⟩⇩G"
    by metis

  thus ?thesis
    using ‹t1 = ctxt⟨t1'⟩⇩G› ‹t2 = ctxt⟨t2'⟩⇩G› by metis
qed

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

lemma predicate_holds_of_mem_rewrite_inside_gctxt:
  assumes rule_in: "(t1, t2) ∈ rewrite_inside_gctxt R" and
    ball_P: "⋀t1 t2. (t1, t2) ∈ R ⟹ P t1 t2" and
    preservation: "⋀t1 t2 ctxt σ. (t1, t2) ∈ R ⟹ P t1 t2 ⟹ P ctxt⟨t1⟩⇩G ctxt⟨t2⟩⇩G"
  shows "P t1 t2"
proof -
  from rule_in obtain t1' t2' ctxt σ where
    "(t1', t2') ∈ R" and
    "t1 = ctxt⟨t1'⟩⇩G" and
    "t2 = ctxt⟨t2'⟩⇩G"
    by (auto simp: rewrite_inside_gctxt_def)
  thus ?thesis
    using ball_P[OF ‹(t1', t2') ∈ R›]
    using preservation[OF ‹(t1', t2') ∈ R›, of ctxt]
    by simp
qed

lemma compatible_with_gctxt_rewrite_inside_gctxt[simp]: "compatible_with_gctxt (rewrite_inside_gctxt E)"
  unfolding compatible_with_gctxt_def rewrite_inside_gctxt_def
  unfolding mem_Collect_eq
  by (metis Pair_inject ctxt_ctxt)

lemma subset_rewrite_inside_gctxt[simp]: "E ⊆ rewrite_inside_gctxt 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_inside_gctxt E"
    unfolding rewrite_inside_gctxt_def
    unfolding mem_Collect_eq
  proof (intro exI conjI)
    show "e = (□⇩G⟨s⟩⇩G, □⇩G⟨t⟩⇩G)"
      unfolding e_def gctxt_apply_term.simps ..
  next
    show "(s, t) ∈ E"
      using e_in
      unfolding e_def .
  qed
qed

lemma wf_converse_rewrite_inside_gctxt:
  fixes E :: "'f gterm rel"
  assumes
    wfP_R: "wfP R" and
    R_compatible_with_gctxt: "⋀ctxt t t'. R t t' ⟹ R ctxt⟨t⟩⇩G ctxt⟨t'⟩⇩G" and
    equations_subset_R: "⋀x y. (x, y) ∈ E ⟹ R y x"
  shows "wf ((rewrite_inside_gctxt E)¯)"
proof (rule wf_subset)
  from wfP_R show "wf {(x, y). R x y}"
    by (simp add: wfP_def)
next
  show "(rewrite_inside_gctxt E)¯ ⊆ {(x, y). R x y}"
  proof (rule Set.subsetI)
    fix e assume "e ∈ (rewrite_inside_gctxt E)¯"
    then obtain ctxt s t where e_def: "e = (ctxt⟨s⟩⇩G, ctxt⟨t⟩⇩G)" and "(t, s) ∈ E"
      by (smt (verit) Pair_inject converseE mem_Collect_eq rewrite_inside_gctxt_def)
    hence "R s t"
      using equations_subset_R by simp
    hence "R ctxt⟨s⟩⇩G ctxt⟨t⟩⇩G"
      using R_compatible_with_gctxt by simp
    then show "e ∈ {(x, y). R x y}"
      by (simp add: e_def)
  qed
qed

end