Theory First_Order_Clause.Monomorphic_Typing_Compatibility

theory Monomorphic_Typing_Compatibility
  imports 
    Nonground_Term_Typing 
    IsaFoR_Nonground_Term
begin

interpretation "term": compatibility where
  id_subst = "Var :: 'v ⇒ ('f, 'v) term" and comp_subst = "(∘⇩s)" and subst = "(⋅)" and
  vars = term.vars and is_ground = term.is_ground and apply_subst = apply_subst and
  subst_update = fun_upd
proof unfold_locales
  fix u and t :: "('f, 'v) term" and σ :: "('f, 'v) subst"
  assume "∀x∈term.vars t. fmlookup u x = Some (σ x)"

  then show "t ⋅ term.subst_updates Var u = t ⋅ σ"
    by (induction t) (auto simp: exists_nonground_term term.subst_updates_var)
next
  fix t :: "('f, 'v) term" and γ :: "('f, 'v) subst"
  assume "∀x∈term.vars t. term.is_ground (γ x)"

  then show "term.is_ground (t ⋅ γ)"
    by (meson ground_subst term_context_ground_iff_term_is_ground)
qed (simp add: eval_same_vars)

end