Theory Rewriting_Nterm

section ‹Higher-order term rewriting using explicit bound variable names›

theory Rewriting_Nterm
imports
  Rewriting_Term
  Higher_Order_Terms.Term_to_Nterm
  "../Terms/Strong_Term"
begin

subsection ‹Definitions›

type_synonym nrule = "term × nterm"

abbreviation nrule :: "nrule ⇒ bool" where
"nrule ≡ basic_rule"

fun (in constants) not_shadowing :: "nrule ⇒ bool" where
"not_shadowing (lhs, rhs) ⟷ ¬ shadows_consts lhs ∧ ¬ shadows_consts rhs"

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


subsection ‹Matching and rewriting›

inductive nrewrite :: "nrule fset ⇒ nterm ⇒ nterm ⇒ bool" (‹_/ ⊢⇩n/ _ ⟶/ _› [50,0,50] 50) for rs where
step: "r |∈| rs ⟹ r ⊢ t → u ⟹ rs ⊢⇩n t ⟶ u" |
beta: "rs ⊢⇩n ((Λ⇩n x. t) $⇩n t') ⟶ subst t (fmap_of_list [(x, t')])" |
"fun": "rs ⊢⇩n t ⟶ t' ⟹ rs ⊢⇩n t $⇩n u ⟶ t' $⇩n u" |
arg: "rs ⊢⇩n u ⟶ u' ⟹ rs ⊢⇩n t $⇩n u ⟶ t $⇩n u'"

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

abbreviation nrewrite_rt :: "nrule fset ⇒ nterm ⇒ nterm ⇒ bool" (‹_/ ⊢⇩n/ _ ⟶*/ _› [50,0,50] 50) where
"nrewrite_rt rs ≡ (nrewrite rs)⇧*⇧*"

lemma (in nrules) nrewrite_closed:
  assumes "rs ⊢⇩n t ⟶ t'" "closed t"
  shows "closed t'"
using assms proof induction
  case (step r t u)
  obtain lhs rhs where "r = (lhs, rhs)"
    by force
  with step have "nrule (lhs, rhs)"
    using all_rules by blast
  hence "frees rhs |⊆| frees lhs"
    by simp
  have "(lhs, rhs) ⊢ t → u"
    using step unfolding ‹r = _› by simp

  show ?case
    apply (rule rewrite_step_closed)
      apply fact+
    done
next
  case beta
  show ?case
    apply simp
    apply (subst closed_except_def)
    apply (subst subst_frees)
    using beta unfolding closed_except_def by auto
qed (auto simp: closed_except_def)

corollary (in nrules) nrewrite_rt_closed:
  assumes "rs ⊢⇩n t ⟶* t'" "closed t"
  shows "closed t'"
using assms
by induction (auto intro: nrewrite_closed)

subsection ‹Translation from @{typ term} to @{typ nterm}›

context begin

private lemma term_to_nterm_all_vars0:
  assumes "wellformed' (length Γ) t"
  shows "∃T. all_frees (fst (run_state (term_to_nterm Γ t) x)) |⊆| fset_of_list Γ |∪| frees t |∪| T ∧ fBall T (λy. y > x)"
using assms proof (induction Γ t arbitrary: x rule: term_to_nterm_induct)
  case (bound Γ i)
  hence "Γ ! i |∈| fset_of_list Γ"
    by (simp add: fset_of_list_elem)
  with bound show ?case
    by (auto simp: State_Monad.return_def)
next
  case (abs Γ t)

  obtain T
    where "all_frees (fst (run_state (term_to_nterm (next x # Γ) t) (next x))) |⊆| fset_of_list (next x # Γ) |∪| frees t |∪| T"
      and "fBall T ((<) (next x))"
    apply atomize_elim
    apply (rule abs(1))
    using abs by auto

  show ?case
    apply (simp add: split_beta create_alt_def)
    apply (rule exI[where x = "finsert (next x) T"])
    apply (intro conjI)
    subgoal by auto
    subgoal using ‹all_frees (fst (run_state _ (next x))) |⊆| _› by simp
    subgoal
      apply simp
      apply (rule conjI)
       apply (rule next_ge)
      using ‹fBall T ((<) (next x))›
      by (metis fBallE fBallI fresh_class.next_ge order.strict_trans)
    done
next
  case (app Γ t⇩1 t⇩2 x⇩1)
  obtain t⇩1' x⇩2 where "run_state (term_to_nterm Γ t⇩1) x⇩1 = (t⇩1', x⇩2)"
    by fastforce
  moreover obtain T⇩1
    where "all_frees (fst (run_state (term_to_nterm Γ t⇩1) x⇩1)) |⊆| fset_of_list Γ |∪| frees t⇩1 |∪| T⇩1"
      and "fBall T⇩1 ((<) x⇩1)"
    apply atomize_elim
    apply (rule app(1))
    using app by auto
  ultimately have "all_frees t⇩1' |⊆| fset_of_list Γ |∪| frees t⇩1 |∪| T⇩1"
    by simp

  obtain T⇩2
    where "all_frees (fst (run_state (term_to_nterm Γ t⇩2) x⇩2)) |⊆| fset_of_list Γ |∪| frees t⇩2 |∪| T⇩2"
      and "fBall T⇩2 ((<) x⇩2)"
    apply atomize_elim
    apply (rule app(2))
    using app by auto
  moreover obtain t⇩2' x' where "run_state (term_to_nterm Γ t⇩2) x⇩2 = (t⇩2', x')"
    by fastforce
  ultimately have "all_frees t⇩2' |⊆| fset_of_list Γ |∪| frees t⇩2 |∪| T⇩2"
    by simp

  have "x⇩1 ≤ x⇩2"
    apply (rule state_io_relD[OF term_to_nterm_mono])
    apply fact
    done

  show ?case
    apply simp
    unfolding ‹run_state (term_to_nterm Γ t⇩1) x⇩1 = _›
    apply simp
    unfolding ‹run_state (term_to_nterm Γ t⇩2) x⇩2 = _›
    apply simp
    apply (rule exI[where x = "T⇩1 |∪| T⇩2"])
    apply (intro conjI)
    subgoal using ‹all_frees t⇩1' |⊆| _› by auto
    subgoal using ‹all_frees t⇩2' |⊆| _› by auto
    subgoal
      apply auto
      using ‹fBall T⇩1 ((<) x⇩1)› apply auto[]
      using ‹fBall T⇩2 ((<) x⇩2)› ‹x⇩1 ≤ x⇩2›
      by auto
    done
qed auto

lemma term_to_nterm_all_vars:
  assumes "wellformed t" "fdisjnt (frees t) S"
  shows "fdisjnt (all_frees (fresh_frun (term_to_nterm [] t) (T |∪| S))) S"
proof -
  let ?Γ = "[]"
  let ?x = "fresh_fNext (T |∪| S)"
  from assms have "wellformed' (length ?Γ) t"
    by simp
  then obtain F
    where "all_frees (fst (run_state (term_to_nterm ?Γ t) ?x)) |⊆| fset_of_list ?Γ |∪| frees t |∪| F"
      and "fBall F (λy. y > ?x)"
    by (metis term_to_nterm_all_vars0)

  have "fdisjnt F (T |∪| S)" if "S ≠ {||}"
    apply (rule fdisjnt_ge_max)
    apply (rule fBall_pred_weaken[OF _ ‹fBall F (λy. y > ?x)›])
    apply (rule less_trans)
     apply (rule fNext_ge_max)
    using that by auto
  show ?thesis
    apply (rule fdisjnt_subset_left)
     apply (subst fresh_frun_def)
     apply (subst fresh_fNext_def[symmetric])
     apply fact
    apply simp
    apply (rule fdisjnt_union_left)
     apply fact
    using ‹_ ⟹ fdisjnt F (T |∪| S)› by (auto simp: fdisjnt_alt_def)
qed

end

fun translate_rule :: "name fset ⇒ rule ⇒ nrule" where
"translate_rule S (lhs, rhs) = (lhs, fresh_frun (term_to_nterm [] rhs) (frees lhs |∪| S))"

lemma translate_rule_alt_def:
  "translate_rule S = (λ(lhs, rhs). (lhs, fresh_frun (term_to_nterm [] rhs) (frees lhs |∪| S)))"
by auto

definition compile' where
"compile' C_info rs = translate_rule (pre_constants.all_consts C_info (heads_of rs)) |`| rs"

context rules begin

definition compile :: "nrule fset" where
"compile = translate_rule all_consts |`| rs"

lemma compile'_compile_eq[simp]: "compile' C_info rs = compile"
unfolding compile'_def compile_def ..

lemma compile_heads: "heads_of compile = heads_of rs"
unfolding compile_def translate_rule_alt_def head_def[abs_def]
by force

lemma compile_rules: "nrules C_info compile"
proof
  have "fBall compile (λ(lhs, rhs). nrule (lhs, rhs))"
    proof safe
      fix lhs rhs
      assume "(lhs, rhs) |∈| compile"
      then obtain rhs'
        where "(lhs, rhs') |∈| rs"
          and rhs: "rhs = fresh_frun (term_to_nterm [] rhs') (frees lhs |∪| all_consts)"
        unfolding compile_def by force
      then have rule: "rule (lhs, rhs')"
        using all_rules by blast

      show "nrule (lhs, rhs)"
        proof
          from rule show "linear lhs" "is_const (fst (strip_comb lhs))" "¬ is_const lhs" by auto

          have "frees rhs |⊆| frees rhs'"
            unfolding rhs using rule
            by (metis rule.simps term_to_nterm_vars)
          also have "frees rhs' |⊆| frees lhs"
            using rule by auto
          finally show "frees rhs |⊆| frees lhs" .
        qed
    qed

  thus "fBall compile nrule"
    by fast
next
  show "arity_compatibles compile"
    proof safe
      fix lhs⇩1 rhs⇩1 lhs⇩2 rhs⇩2
      assume "(lhs⇩1, rhs⇩1) |∈| compile" "(lhs⇩2, rhs⇩2) |∈| compile"
      then obtain rhs⇩1' rhs⇩2' where "(lhs⇩1, rhs⇩1') |∈| rs" "(lhs⇩2, rhs⇩2') |∈| rs"
        unfolding compile_def by force
      thus "arity_compatible lhs⇩1 lhs⇩2"
        using arity by (blast dest: fpairwiseD)
    qed
next
  have "is_fmap rs"
    using fmap by simp
  thus "is_fmap compile"
    unfolding compile_def translate_rule_alt_def
    by (rule is_fmap_image)
next
  have "pattern_compatibles rs"
    using patterns by simp
  thus "pattern_compatibles compile"
    unfolding compile_def translate_rule_alt_def
    by (auto dest: fpairwiseD)
next
  show "fdisjnt (heads_of compile) C"
    using disjnt by (simp add: compile_heads)
next
  have "fBall compile not_shadowing"
    proof safe
      fix lhs rhs
      assume "(lhs, rhs) |∈| compile"
      then obtain rhs'
        where "rhs = fresh_frun (term_to_nterm [] rhs') (frees lhs |∪| all_consts)"
          and "(lhs, rhs') |∈| rs"
        unfolding compile_def translate_rule_alt_def by auto
      hence "rule (lhs, rhs')" "¬ shadows_consts lhs"
        using all_rules not_shadows by blast+
      moreover hence "wellformed rhs'" "frees rhs' |⊆| frees lhs" "fdisjnt all_consts (frees lhs)"
        unfolding shadows_consts_def by simp+

      moreover have "¬ shadows_consts rhs"
        apply (subst shadows_consts_def)
        apply simp
        unfolding ‹rhs = _›
        apply (rule fdisjnt_swap)
        apply (rule term_to_nterm_all_vars)
         apply fact
        apply (rule fdisjnt_subset_left)
         apply fact
        apply (rule fdisjnt_swap)
        apply fact
        done

      ultimately show "not_shadowing (lhs, rhs)"
        unfolding compile_heads by simp
    qed
  thus "fBall compile (constants.not_shadowing C_info (heads_of compile))"
    unfolding compile_heads .

  have "fBall compile (λ(_, rhs). welldefined rhs)"
    unfolding compile_heads
    unfolding compile_def ball_simps
    apply (rule fBall_pred_weaken[OF _ welldefined_rs])
    subgoal for x
      apply (cases x)
      apply simp
      apply (subst fresh_frun_def)
      apply (subst term_to_nterm_consts[THEN pred_state_run_state])
      by auto
    done
  thus "fBall compile (λ(_, rhs). consts rhs |⊆| pre_constants.all_consts C_info (heads_of compile))"
    unfolding compile_heads .
next
  show "compile ≠ {||}"
    using nonempty unfolding compile_def by auto
next
  show "distinct all_constructors"
    by (fact distinct_ctr)
qed

sublocale rules_as_nrules: nrules C_info compile
by (fact compile_rules)

end

subsection ‹Correctness of translation›

theorem (in rules) compile_correct:
  assumes "compile ⊢⇩n u ⟶ u'" "closed u"
  shows "rs ⊢ nterm_to_term' u ⟶ nterm_to_term' u'"
using assms proof (induction u u')
  case (step r u u')
  moreover obtain pat rhs' where "r = (pat, rhs')"
    by force
  ultimately obtain nenv where "match pat u = Some nenv" "u' = subst rhs' nenv"
    by auto
  then obtain env where "nrelated.P_env [] env nenv" "match pat (nterm_to_term [] u) = Some env"
    by (metis nrelated.match_rel option.exhaust option.rel_distinct(1) option.rel_inject(2))

  have "closed_env nenv"
    using step ‹match pat u = Some nenv› by (intro closed.match)

  from step obtain rhs
    where "rhs' = fresh_frun (term_to_nterm [] rhs) (frees pat |∪| all_consts)" "(pat, rhs) |∈| rs"
    unfolding ‹r = _› compile_def by auto
  with assms have "rule (pat, rhs)"
    using all_rules by blast
  hence "rhs = nterm_to_term [] rhs'"
    unfolding ‹rhs' = _›
    by (simp add: term_to_nterm_nterm_to_term fresh_frun_def)

  have "compile ⊢⇩n u ⟶ u'"
    using step by (auto intro: nrewrite.step)
  hence "closed u'"
    by (rule rules_as_nrules.nrewrite_closed) fact

  show ?case
    proof (rule rewrite.step)
      show "(pat, rhs) ⊢ nterm_to_term [] u → nterm_to_term [] u'"
        apply (subst nterm_to_term_eq_closed)
         apply fact
        apply simp
        apply (rule exI[where x = env])
        apply (rule conjI)
         apply fact
        unfolding ‹rhs = _›
        apply (subst nrelated_subst)
           apply fact
          apply fact
        unfolding fdisjnt_alt_def apply simp
        unfolding ‹u' = subst rhs' nenv› by simp
    qed fact
next
  case beta
  show ?case
    apply simp
    apply (subst subst_single_eq[symmetric, simplified])
    apply (subst nterm_to_term_subst_replace_bound[where n = 0])
    subgoal using beta by (simp add: closed_except_def)
    subgoal by simp
    subgoal by simp
    subgoal by simp (rule rewrite.beta)
    done
qed (auto intro: rewrite.intros simp: closed_except_def)

subsection ‹Completeness of translation›

context rules begin

context
  notes [simp] = closed_except_def fdisjnt_alt_def
begin

private lemma compile_complete0:
  assumes "rs ⊢ t ⟶ t'" "closed t" "wellformed t"
  obtains u' where "compile ⊢⇩n fst (run_state (term_to_nterm [] t) s) ⟶ u'" "u' ≈⇩α fst (run_state (term_to_nterm [] t') s')"
apply atomize_elim
using assms proof (induction t t' arbitrary: s s')
  case (step r t t')
  let ?t⇩n = "fst (run_state (term_to_nterm [] t) s)"
  let ?t⇩n' = "fst (run_state (term_to_nterm [] t') s')"
  from step have "closed t" "closed ?t⇩n"
    using term_to_nterm_vars0[where Γ = "[]"]
    by force+
  from step have "nterm_to_term' ?t⇩n = t"
    by (auto intro!: term_to_nterm_nterm_to_term0)

  obtain pat rhs' where "r = (pat, rhs')"
    by fastforce
  with step obtain env' where "match pat t = Some env'" "t' = subst rhs' env'"
    by fastforce
  with ‹_ = t› have "rel_option (nrelated.P_env []) (match pat t) (match pat (?t⇩n))"
    by (metis nrelated.match_rel)
  with step ‹_ = Some env'›
    obtain env where "nrelated.P_env [] env' env" "match pat ?t⇩n = Some env"
    by (metis (no_types, lifting) option_rel_Some1)
  with ‹closed ?t⇩n› have "closed_env env"
    by (blast intro: closed.match)

  from step obtain rhs
    where "rhs = fresh_frun (term_to_nterm [] rhs') (frees pat |∪| all_consts)" "(pat, rhs) |∈| compile"
    unfolding ‹r = _› compile_def
    by force
  with step have "rule (pat, rhs')"
    unfolding ‹r = _›
    using all_rules by fast
  hence "nterm_to_term' rhs = rhs'"
    unfolding ‹rhs = _›
    by (simp add: fresh_frun_def term_to_nterm_nterm_to_term)
  obtain u' where "subst rhs env = u'"
    by simp
  have "t' = nterm_to_term' u'"
    unfolding ‹t' = _›
    unfolding ‹_ = rhs'›[symmetric]
    apply (subst nrelated_subst)
       apply fact+
    using ‹_ = u'›
    by simp+

  have "compile ⊢⇩n ?t⇩n ⟶ u'"
    apply (rule nrewrite.step)
     apply fact
    apply simp
    apply (intro conjI exI)
     apply fact+
    done
  with ‹closed ?t⇩n› have "closed u'"
    by (blast intro:rules_as_nrules.nrewrite_closed)
  with ‹t' = nterm_to_term' _› have "u' ≈⇩α ?t⇩n'"
    by (force intro: nterm_to_term_term_to_nterm[where Γ = "[]" and Γ' = "[]",simplified])

  show ?case
    apply (intro conjI exI)
     apply (rule nrewrite.step)
      apply fact
     apply simp
     apply (intro conjI exI)
      apply fact+
    done
next
  case (beta t t')
  let ?name = "next s"
  let ?t⇩n = "fst (run_state (term_to_nterm [?name] t) (?name))"
  let ?t⇩n' = "fst (run_state (term_to_nterm [] t') (snd (run_state (term_to_nterm [?name] t) (?name))))"

  from beta have "closed t" "closed (t [t']⇩β)"  "closed (Λ t $ t')" "closed  t'"
    using replace_bound_frees
    by fastforce+
  moreover from beta have "wellformed' (Suc 0) t" "wellformed t'"
    by simp+
  ultimately have "t = nterm_to_term [?name] ?t⇩n"
             and "t' = nterm_to_term' ?t⇩n'"
             and *:"frees ?t⇩n = {|?name|} ∨ frees ?t⇩n = fempty"
             and "closed ?t⇩n'"
    using term_to_nterm_vars0[where Γ = "[?name]"]
    using term_to_nterm_vars0[where Γ = "[]"]
    by (force simp: term_to_nterm_nterm_to_term0)+

  hence **:"t [t']⇩β = nterm_to_term' (subst_single ?t⇩n ?name ?t⇩n')"
    by (auto simp: nterm_to_term_subst_replace_bound[where n = 0])

  from ‹closed ?t⇩n'› have "closed_env (fmap_of_list [(?name, ?t⇩n')])"
    by auto

  show ?case
    apply (rule exI)
    apply (auto simp: split_beta create_alt_def)
     apply (rule nrewrite.beta)
    apply (subst subst_single_eq[symmetric])
    apply (subst **)
    apply (rule nterm_to_term_term_to_nterm[where Γ = "[]" and Γ' = "[]", simplified])
    apply (subst subst_single_eq)
    apply (subst subst_frees[OF ‹closed_env _›])
    using * by force
next
  case ("fun" t t' u)
  hence "closed  t" "closed u" "closed (t $ u)"
       and wellform:"wellformed t" "wellformed u"
    by fastforce+
  from "fun" obtain u'
    where "compile ⊢⇩n fst (run_state (term_to_nterm [] t) s) ⟶ u'"
          "u' ≈⇩α fst (run_state (term_to_nterm [] t') s')"
    by force
  show ?case
    apply (rule exI)
    apply (auto simp: split_beta create_alt_def)
     apply (rule nrewrite.fun)
     apply fact
    apply rule
     apply fact
    apply (subst term_to_nterm_alpha_equiv[of "[]" "[]", simplified])
    using ‹closed u› ‹wellformed u› by auto
next
  case (arg u u' t)
  hence "closed  t" "closed u" "closed (t $ u)"
       and wellform:"wellformed t" "wellformed u"
    by fastforce+
  from arg obtain t'
    where "compile ⊢⇩n fst (run_state (term_to_nterm [] u) (snd (run_state (term_to_nterm [] t) s))) ⟶ t'"
          "t' ≈⇩α  fst (run_state (term_to_nterm [] u') (snd (run_state (term_to_nterm [] t) s')))"
    by force
  show ?case
    apply (rule exI)
    apply (auto simp: split_beta create_alt_def)
     apply rule
     apply fact
    apply rule
     apply (subst term_to_nterm_alpha_equiv[of "[]" "[]", simplified])
    using ‹closed t› ‹wellformed t› apply force+
    by fact
qed

lemma compile_complete:
  assumes "rs ⊢ t ⟶ t'" "closed t" "wellformed t"
  obtains u' where "compile ⊢⇩n term_to_nterm' t ⟶ u'" "u' ≈⇩α term_to_nterm' t'"
unfolding term_to_nterm'_def
using assms by (metis compile_complete0)

end

end

subsection ‹Splitting into constants›

type_synonym crules = "(term list × nterm) fset"
type_synonym crule_set = "(name × crules) fset"

abbreviation arity_compatibles :: "(term list × 'a) fset ⇒ bool" where
"arity_compatibles ≡ fpairwise (λ(pats⇩1, _) (pats⇩2, _). length pats⇩1 = length pats⇩2)"

lemma arity_compatible_length:
  assumes "arity_compatibles rs" "(pats, rhs) |∈| rs"
  shows "length pats = arity rs"
proof -
  have "fBall rs (λ(pats⇩1, _). fBall rs (λ(pats⇩2, _). length pats⇩1 = length pats⇩2))"
    using assms unfolding fpairwise_alt_def by blast
  hence "fBall rs (λx. fBall rs (λy. (length ∘ fst) x = (length ∘ fst) y))"
    by force
  hence "(length ∘ fst) (pats, rhs) = arity rs"
    using assms(2) unfolding arity_def fthe_elem'_eq by (rule singleton_fset_holds)
  thus ?thesis
    by simp
qed

locale pre_crules = constants C_info "fst |`| rs" for C_info and rs :: "crule_set"

locale crules = pre_crules +
  assumes fmap: "is_fmap rs"
  assumes nonempty: "rs ≠ {||}"
  assumes inner:
    "fBall rs (λ(_, crs).
      arity_compatibles crs ∧
      is_fmap crs ∧
      patterns_compatibles crs ∧
      crs ≠ {||} ∧
      fBall crs (λ(pats, rhs).
        linears pats ∧
        pats ≠ [] ∧
        fdisjnt (freess pats) all_consts ∧
        ¬ shadows_consts rhs ∧
        frees rhs |⊆| freess pats ∧
        welldefined rhs))"

lemma (in pre_crules) crulesI:
  assumes "⋀name crs. (name, crs) |∈| rs ⟹ arity_compatibles crs"
  assumes "⋀name crs. (name, crs) |∈| rs ⟹ is_fmap crs"
  assumes "⋀name crs. (name, crs) |∈| rs ⟹ patterns_compatibles crs"
  assumes "⋀name crs. (name, crs) |∈| rs ⟹ crs ≠ {||}"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ linears pats"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ pats ≠ []"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ fdisjnt (freess pats) all_consts"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ ¬ shadows_consts rhs"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ frees rhs |⊆| freess pats"
  assumes "⋀name crs pats rhs. (name, crs) |∈| rs ⟹ (pats, rhs) |∈| crs ⟹ welldefined rhs"
  assumes "is_fmap rs" "rs ≠ {||}"
  shows "crules C_info rs"
proof unfold_locales
  show "is_fmap rs"
    using assms(11) .
next
  show "rs ≠ {||}"
    using assms(12) .
next
  show "fBall rs (λ(_, crs). Rewriting_Nterm.arity_compatibles crs ∧ is_fmap crs ∧
    patterns_compatibles crs ∧ crs ≠ {||} ∧
    fBall crs (λ(pats, rhs). linears pats ∧ pats ≠ [] ∧ fdisjnt (freess pats) all_consts ∧
      ¬ shadows_consts rhs ∧ frees rhs |⊆| freess pats ∧ consts rhs |⊆| all_consts))"
    using assms(1-10)
    by (intro prod_BallI conjI) metis+
qed

lemmas crulesI[intro!] = pre_crules.crulesI[unfolded pre_crules_def]

definition "consts_of" :: "nrule fset ⇒ crule_set" where
"consts_of = fgroup_by split_rule"

lemma consts_of_heads: "fst |`| consts_of rs = heads_of rs"
unfolding consts_of_def
by (simp add: split_rule_fst comp_def)

lemma (in nrules) consts_rules: "crules C_info (consts_of rs)"
proof
  have "is_fmap rs"
    using fmap by simp
  thus "is_fmap (consts_of rs)"
    unfolding consts_of_def by auto

  show "consts_of rs ≠ {||}"
    using nonempty unfolding consts_of_def
    by (meson fgroup_by_nonempty)

  show "constants C_info (fst |`| consts_of rs)"
    proof
      show "fdisjnt (fst |`| consts_of rs) C"
        using disjnt by (auto simp: consts_of_heads)
    next
      show "distinct all_constructors"
        by (fact distinct_ctr)
    qed

  fix name crs
  assume crs: "(name, crs) |∈| consts_of rs"

  thus "crs ≠ {||}"
    unfolding consts_of_def
    by (meson femptyE fgroup_by_nonempty_inner)

  show "arity_compatibles crs" "patterns_compatibles crs"
    proof safe
      fix pats⇩1 rhs⇩1 pats⇩2 rhs⇩2
      assume "(pats⇩1, rhs⇩1) |∈| crs" "(pats⇩2, rhs⇩2) |∈| crs"
      with crs obtain lhs⇩1 lhs⇩2
        where rs: "(lhs⇩1, rhs⇩1) |∈| rs" "(lhs⇩2, rhs⇩2) |∈| rs" and
              split: "split_rule (lhs⇩1, rhs⇩1) = (name, (pats⇩1, rhs⇩1))"
                     "split_rule (lhs⇩2, rhs⇩2) = (name, (pats⇩2, rhs⇩2))"
        unfolding consts_of_def by (force simp: split_beta)

      hence arity: "arity_compatible lhs⇩1 lhs⇩2"
        using arity by (force dest: fpairwiseD)

      from rs have const: "is_const (fst (strip_comb lhs⇩1))" "is_const (fst (strip_comb lhs⇩2))"
        using all_rules by force+

      have "name = const_name (fst (strip_comb lhs⇩1))" "name = const_name (fst (strip_comb lhs⇩2))"
        using split by (auto simp: split_beta)
      with const have "fst (strip_comb lhs⇩1) = Const name" "fst (strip_comb lhs⇩2) = Const name"
         apply (fold const_term_def)
        subgoal by simp
        subgoal by fastforce
        done
      hence fst: "fst (strip_comb lhs⇩1) = fst (strip_comb lhs⇩2)"
        by simp

      with arity have "length (snd (strip_comb lhs⇩1)) = length (snd (strip_comb lhs⇩2))"
        unfolding arity_compatible_def
        by (simp add: split_beta)

      with split show "length pats⇩1 = length pats⇩2"
        by (auto simp: split_beta)

      have "pattern_compatible lhs⇩1 lhs⇩2"
        using rs patterns by (auto dest: fpairwiseD)
      moreover have "lhs⇩1 = name $$ pats⇩1"
        using split(1) const(1) by (auto simp: split_beta)
      moreover have "lhs⇩2 = name $$ pats⇩2"
        using split(2) const(2) by (auto simp: split_beta)
      ultimately have "pattern_compatible (name $$ pats⇩1) (name $$ pats⇩2)"
        by simp
      thus "patterns_compatible pats⇩1 pats⇩2"
        using ‹length pats⇩1 = _› by (auto dest: pattern_compatible_combD)
    qed

  show "is_fmap crs"
    proof
      fix pats rhs⇩1 rhs⇩2
      assume "(pats, rhs⇩1) |∈| crs" "(pats, rhs⇩2) |∈| crs"
      with crs obtain lhs⇩1 lhs⇩2
        where rs: "(lhs⇩1, rhs⇩1) |∈| rs" "(lhs⇩2, rhs⇩2) |∈| rs" and
              split: "split_rule (lhs⇩1, rhs⇩1) = (name, (pats, rhs⇩1))"
                     "split_rule (lhs⇩2, rhs⇩2) = (name, (pats, rhs⇩2))"
        unfolding consts_of_def by (force simp: split_beta)

      have "lhs⇩1 = lhs⇩2"
        proof (rule ccontr)
          assume "lhs⇩1 ≠ lhs⇩2"
          then consider (fst) "fst (strip_comb lhs⇩1) ≠ fst (strip_comb lhs⇩2)"
                      | (snd) "snd (strip_comb lhs⇩1) ≠ snd (strip_comb lhs⇩2)"
            by (metis list_strip_comb)
          thus False
            proof cases
              case fst
              moreover have "is_const (fst (strip_comb lhs⇩1))" "is_const (fst (strip_comb lhs⇩2))"
                using rs all_rules by force+
              ultimately show ?thesis
                using split const_name_simps by (fastforce simp: split_beta)
            next
              case snd
              with split show ?thesis
                by (auto simp: split_beta)
            qed
        qed

      with rs show "rhs⇩1 = rhs⇩2"
        using ‹is_fmap rs› by (auto dest: is_fmapD)
    qed

  fix pats rhs
  assume "(pats, rhs) |∈| crs"
  then obtain lhs where "(lhs, rhs) |∈| rs" "pats = snd (strip_comb lhs)"
    using crs unfolding consts_of_def by (force simp: split_beta)
  hence "nrule (lhs, rhs)"
    using all_rules by blast
  hence "linear lhs" "frees rhs |⊆| frees lhs"
    by auto
  thus "linears pats"
    unfolding ‹pats = _› by (intro linears_strip_comb)

  have "¬ is_const lhs" "is_const (fst (strip_comb lhs))"
    using ‹nrule _› by auto
  thus "pats ≠ []"
    unfolding ‹pats = _› using ‹linear lhs›
    apply (cases lhs)
        apply (fold app_term_def)
    by (auto split: prod.splits)

  from ‹nrule (lhs, rhs)› have "frees (fst (strip_comb lhs)) = {||}"
    by (cases "fst (strip_comb lhs)") (auto simp: is_const_def)
  hence "frees lhs = freess (snd (strip_comb lhs))"
    by (subst frees_strip_comb) auto
  thus "frees rhs |⊆| freess pats"
    unfolding ‹pats = _› using ‹frees rhs |⊆| frees lhs› by simp

  have "¬ shadows_consts rhs"
    using ‹(lhs, rhs) |∈| rs› not_shadows
    by force
  thus "¬ pre_constants.shadows_consts C_info (fst |`| consts_of rs) rhs"
    by (simp add: consts_of_heads)

  have "fdisjnt all_consts (frees lhs)"
    using ‹(lhs, rhs) |∈| rs› not_shadows
    by (force simp: shadows_consts_def)
  moreover have "freess pats |⊆| frees lhs"
    unfolding ‹pats = _› ‹frees lhs = _›
    by simp
  ultimately have "fdisjnt (freess pats) all_consts"
    by (metis fdisjnt_subset_right fdisjnt_swap)

  thus "fdisjnt (freess pats) (pre_constants.all_consts C_info (fst |`| consts_of rs))"
    by (simp add: consts_of_heads)

  show "pre_constants.welldefined C_info (fst |`| consts_of rs) rhs"
    using welldefined_rs ‹(lhs, rhs) |∈| rs›
    by (force simp: consts_of_heads)
qed

sublocale nrules ⊆ nrules_as_crules?: crules C_info "consts_of rs"
by (fact consts_rules)

subsection ‹Computability›

export_code
  translate_rule consts_of arity nterm_to_term
  checking Scala

end