Theory Rewriting

section ‹Rewriting›

theory Rewriting
  imports Regular_Tree_Relations.Term_Context
    Regular_Tree_Relations.Ground_Terms
    Utils
begin

subsection ‹Type definitions and rewrite relation definitions›
type_synonym 'f sig = "('f × nat) set"
type_synonym ('f, 'v) rule = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) trs  = "('f, 'v) rule set"


definition "sig_step ℱ ℛ = {(s, t). funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ ∧ (s, t) ∈ ℛ}"

inductive_set rstep :: "_ ⇒ ('f, 'v) term rel" for R :: "('f, 'v) trs"
  where
    rstep: "⋀C σ l r. (l, r) ∈ R ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep R"

definition rstep_r_p_s :: "('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) subst ⇒ ('f, 'v) trs" where
  "rstep_r_p_s R r p σ = {(s, t). p ∈ poss s ∧ p ∈ poss t ∧ r ∈ R ∧ ctxt_at_pos s p = ctxt_at_pos t p ∧
     s[p ← (fst r ⋅ σ)] = s ∧ t[p ← (snd r ⋅ σ)] = t}"

text ‹Rewriting steps below the root position.›
definition nrrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
  "nrrstep R = {(s,t). ∃r i ps σ. (s,t) ∈ rstep_r_p_s R r (i#ps) σ}"

text ‹Rewriting step at the root position.›
definition rrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
  "rrstep R = {(s,t). ∃r σ. (s,t) ∈ rstep_r_p_s R r [] σ}"

text ‹the parallel rewrite relation›
inductive_set par_rstep :: "('f,'v)trs ⇒ ('f,'v)trs" for R :: "('f,'v)trs"
  where root_step[intro]: "(s,t) ∈ R ⟹ (s ⋅ σ,t ⋅ σ) ∈ par_rstep R"
     |  par_step_fun[intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i,ts ! i) ∈ par_rstep R⟧ ⟹ length ss = length ts
             ⟹ (Fun f ss, Fun f ts) ∈ par_rstep R"
     |  par_step_var[intro]: "(Var x, Var x) ∈ par_rstep R"


subsection ‹Ground variants connecting to FORT›

definition grrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "grrstep ℛ = inv_image (rrstep ℛ) term_of_gterm"

definition gnrrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "gnrrstep ℛ = inv_image (nrrstep ℛ) term_of_gterm"

definition grstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "grstep ℛ = inv_image (rstep ℛ) term_of_gterm"

definition gpar_rstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "gpar_rstep ℛ = inv_image (par_rstep ℛ) term_of_gterm"


text ‹
  An alternative induction scheme that treats the rule-case, the
  substition-case, and the context-case separately.
›
lemma rstep_induct [consumes 1, case_names rule subst ctxt]:
  assumes "(s, t) ∈ rstep R"
    and rule: "⋀l r. (l, r) ∈ R ⟹ P l r"
    and subst: "⋀s t σ. P s t ⟹ P (s ⋅ σ) (t ⋅ σ)"
    and ctxt: "⋀s t C. P s t ⟹ P (C⟨s⟩) (C⟨t⟩)"
  shows "P s t"
  using assms by (induct) auto


lemmas rstepI = rstep.intros [intro]

lemmas rstepE = rstep.cases [elim]

lemma rstep_ctxt [intro]: "(s, t) ∈ rstep R ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep R"
  by (force simp flip: ctxt_ctxt_compose)

lemma rstep_rule [intro]: "(l, r) ∈ R ⟹ (l, r) ∈ rstep R"
  using rstep.rstep [where C = □ and σ = Var and R = R] by simp

lemma rstep_subst [intro]: "(s, t) ∈ rstep R ⟹ (s ⋅ σ, t ⋅ σ) ∈ rstep R"
  by (force simp flip: subst_subst_compose)

lemma nrrstep_def':
  "nrrstep R = {(s, t). ∃l r C σ. (l, r) ∈ R ∧ C ≠ □ ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩}" (is "?Ls = ?Rs")
proof
  show "?Ls ⊆ ?Rs"
  proof (rule subrelI)
    fix s t assume "(s, t) ∈ ?Ls"
    then obtain l r i ps σ where step: "(s, t) ∈ rstep_r_p_s R (l, r) (i # ps) σ"
          unfolding nrrstep_def by best
    let ?C = "ctxt_at_pos s (i # ps)"
    from step have"i # ps ∈ poss s" and "(l, r) ∈ R" and "s = ?C⟨l⋅σ⟩" and "t = ?C⟨r⋅σ⟩"
      unfolding rstep_r_p_s_def Let_def by (auto simp flip: replace_term_at_replace_at_conv)
    moreover from ‹i # ps ∈ poss s› have "?C ≠ □" by (induct s) auto
    ultimately show "(s, t) ∈ ?Rs" by auto
  qed
next
  show "?Rs ⊆ ?Ls"
  proof (rule subrelI)
    fix s t assume "(s, t) ∈ ?Rs"
    then obtain l r C σ where in_R: "(l, r) ∈ R" and "C ≠ □"
      and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
    from ‹C ≠ □› obtain i p where ip: "hole_pos C = i # p" by (induct C) auto
    have "i # p ∈ poss s" unfolding s ip[symmetric] by simp
    then have C: "C = ctxt_at_pos s (i # p) "
      unfolding s ip[symmetric] by simp
    from ‹i # p ∈ poss s› in_R s t have "(s, t) ∈ rstep_r_p_s R (l, r) (i # p) σ"
      unfolding rstep_r_p_s_def C[symmetric] ip[symmetric] by simp
    then show "(s, t) ∈ nrrstep R" unfolding nrrstep_def by best
  qed
qed

lemma rrstep_def': "rrstep R = {(s, t). ∃l r σ. (l, r) ∈ R ∧ s = l⋅σ ∧ t = r⋅σ}"
  by (auto simp: rrstep_def rstep_r_p_s_def)


lemma rstep_imp_C_s_r:
  assumes "(s,t) ∈ rstep R"
  shows "∃C σ l r. (l,r) ∈ R ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩" using assms
  by (induct) auto

lemma rhs_wf:
  assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
  shows "funas_term r ⊆ F"
  using assms by (force simp: funas_trs_def)

abbreviation "linear_sys ℛ ≡ (∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r)"
abbreviation "const_subt c ≡ λ x. Fun c []"



end