Theory 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_updates = subst_updates
proof unfold_locales
    fix t :: "('f, 'v) term" and X σ b
  assume "term.vars t ⊆ X"

  then show "t ⋅ (λx. get_or (if x ∈ X then Some (σ x) else b x) (Var x)) = t ⋅ σ"
    by (simp add: eval_same_vars subset_iff)
next
  fix t :: "('f, 'v) term" and X σ b
  assume "term.vars t ∩ X = {}"

  then show "t ⋅ (λx. get_or (if x ∈ X then b x else Some (σ x)) (Var x)) = t ⋅ σ"
    by (induction t) auto
next
  fix t :: "('f, 'v) term" and σ τ :: "('f, 'v) subst"
  assume "⋀x. x ∈ term.vars t ⟹ σ x = τ x" 

  then show "t ⋅ σ = t ⋅ τ"
    by (simp add: eval_same_vars)
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

end