Theory First_Order_Clause.Term_Typing

theory Term_Typing
  imports
    Context_Notation
    Typing
begin

(* TODO: Notation for welltyped *)
locale context_compatible_typing =
  apply_context_notation +
  fixes welltyped
  assumes
   welltyped_context_compatible [intro]:
    "⋀t t' c τ τ'.
      welltyped t τ' ⟹
      welltyped t' τ' ⟹
      welltyped c⟨t⟩ τ ⟹
      welltyped c⟨t'⟩ τ"

locale subterm_typing =
  apply_context_notation +
  fixes welltyped
  assumes
   welltyped_subterm [intro]:
    "⋀c t τ. welltyped c⟨t⟩ τ ⟹ ∃τ'. welltyped t τ'"

locale term_typing =
  base_typing +
  context_compatible_typing +
  subterm_typing

end