Theory General_Rewriting

theory General_Rewriting
imports Terms_Extras
begin

locale rewriting =
  fixes R :: "'a::term ⇒ 'a ⇒ bool"
  assumes R_fun: "R t t' ⟹ R (app t u) (app t' u)"
  assumes R_arg: "R u u' ⟹ R (app t u) (app t u')"
begin

lemma rt_fun:
  "R⇧*⇧* t t' ⟹ R⇧*⇧* (app t u) (app t' u)"
by (induct rule: rtranclp.induct) (auto intro: rtranclp.rtrancl_into_rtrancl R_fun)

lemma rt_arg:
  "R⇧*⇧* u u' ⟹ R⇧*⇧* (app t u) (app t u')"
by (induct rule: rtranclp.induct) (auto intro: rtranclp.rtrancl_into_rtrancl R_arg)

lemma rt_comb:
  "R⇧*⇧* t⇩1 u⇩1 ⟹ R⇧*⇧* t⇩2 u⇩2 ⟹ R⇧*⇧* (app t⇩1 t⇩2) (app u⇩1 u⇩2)"
by (metis rt_fun rt_arg rtranclp_trans)

lemma rt_list_comb:
  assumes "list_all2 R⇧*⇧* ts us" "R⇧*⇧* t u"
  shows "R⇧*⇧* (list_comb t ts) (list_comb u us)"
using assms
by (induction ts us arbitrary: t u rule: list.rel_induct) (auto intro: rt_comb)

end

end