Theory Rewriting

section ‹Rewriting›

theory Rewriting
  imports Regular_Tree_Relations.Term_Context
    Regular_Tree_Relations.Ground_Terms
    Utils
    First_Order_Rewriting.Trs
    First_Order_Rewriting.Parallel_Rewriting
begin

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.
›


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



end