Theory Rewriting_Term

section ‹Higher-order term rewriting using de-Bruijn indices›

theory Rewriting_Term
imports
  "../Terms/General_Rewriting"
  "../Terms/Strong_Term"
begin

subsection ‹Matching and rewriting›

type_synonym rule = "term × term"

inductive rewrite :: "rule fset ⇒ term ⇒ term ⇒ bool" (‹_/ ⊢/ _ ⟶/ _› [50,0,50] 50) for rs where
step: "r |∈| rs ⟹ r ⊢ t → u ⟹ rs ⊢ t ⟶ u" |
beta: "rs ⊢ (Λ t $ t') ⟶ t [t']⇩β" |
"fun": "rs ⊢ t ⟶ t'⟹ rs ⊢ t $ u ⟶ t' $ u" |
arg: "rs ⊢ u ⟶ u'⟹ rs ⊢ t $ u ⟶ t $ u'"

global_interpretation rewrite: rewriting "rewrite rs" for rs
by standard (auto intro: rewrite.intros simp: app_term_def)+

abbreviation rewrite_rt :: "rule fset ⇒ term ⇒ term ⇒ bool" (‹_/ ⊢/ _ ⟶*/ _› [50,0,50] 50) where
"rewrite_rt rs ≡ (rewrite rs)⇧*⇧*"

lemma rewrite_beta_alt: "t [t']⇩β = u ⟹ wellformed t' ⟹ rs ⊢ (Λ t $ t') ⟶ u"
by (metis rewrite.beta)

subsection ‹Wellformedness›

primrec rule :: "rule ⇒ bool" where
"rule (lhs, rhs) ⟷ basic_rule (lhs, rhs) ∧ Term.wellformed rhs"

lemma ruleI[intro]:
  assumes "basic_rule (lhs, rhs)"
  assumes "Term.wellformed rhs"
  shows "rule (lhs, rhs)"
using assms by simp

lemma split_rule_fst: "fst (split_rule r) = head (fst r)"
unfolding head_def by (smt (z3) prod.case_eq_if prod.collapse prod.inject split_rule.simps)

locale rules = constants C_info "heads_of rs" for C_info and rs :: "rule fset" +
  assumes all_rules: "fBall rs rule"
  assumes arity: "arity_compatibles rs"
  assumes fmap: "is_fmap rs"
  assumes patterns: "pattern_compatibles rs"
  assumes nonempty: "rs ≠ {||}"
  assumes not_shadows: "fBall rs (λ(lhs, _). ¬ shadows_consts lhs)"
  assumes welldefined_rs: "fBall rs (λ(_, rhs). welldefined rhs)"
begin

lemma rewrite_wellformed:
  assumes "rs ⊢ t ⟶ t'" "wellformed t"
  shows "wellformed t'"
using assms
proof (induction rule: rewrite.induct)
  case (step r t u)
  obtain lhs rhs where "r = (lhs, rhs)"
    by force
  hence "wellformed rhs"
    using all_rules step by force
  show ?case
    apply (rule wellformed.rewrite_step)
      apply (rule step(2)[unfolded ‹r = _›])
     apply fact+
    done
next
  case (beta u t)
  show ?case
    unfolding wellformed_term_def
    apply (rule replace_bound_wellformed)
    using beta by auto
qed auto

lemma rewrite_rt_wellformed: "rs ⊢ t ⟶* t' ⟹ wellformed t ⟹ wellformed t'"
by (induction rule: rtranclp.induct) (auto intro: rewrite_wellformed simp del: wellformed_term_def)

lemma rewrite_closed: "rs ⊢ t ⟶ t' ⟹ closed t ⟹ closed t'"
proof (induction t t' rule: rewrite.induct)
  case (step r t u)
  obtain lhs rhs where "r = (lhs, rhs)"
    by force
  with step have "rule (lhs, rhs)"
    using all_rules by blast
  hence "frees rhs |⊆| frees lhs"
    by simp
  moreover have "(lhs, rhs) ⊢ t → u"
    using step unfolding ‹r = _› by simp
  show ?case
    apply (rule rewrite_step_closed)
    apply fact+
    done
next
  case (beta t t')
  have "frees t [t']⇩β |⊆| frees t |∪| frees t'"
    by (rule replace_bound_frees)
  with beta show ?case
    unfolding closed_except_def by auto
qed (auto simp: closed_except_def)

lemma rewrite_rt_closed: "rs ⊢ t ⟶* t' ⟹ closed t ⟹ closed t'"
by (induction rule: rtranclp.induct) (auto intro: rewrite_closed)

end

end