Theory Term_Typing

theory Term_Typing
  imports Typing Context_Extra
begin

type_synonym ('f, 'ty) fun_types = "'f ⇒ 'ty list × 'ty"

locale context_compatible_typing =
  fixes Fun typed
  assumes
   context_compatible [intro]:
    "⋀t t' c τ τ'.
      typed t τ' ⟹
      typed t' τ' ⟹
      typed (Fun⟨c; t⟩) τ ⟹
      typed (Fun⟨c; t'⟩) τ"

locale subterm_typing =
  fixes Fun typed
  assumes
    subterm': "⋀f ts τ . typed (Fun f ts) τ ⟹ ∀t∈set ts. ∃τ'. typed t τ'"
begin

lemma subterm: "typed (Fun⟨c; t⟩) τ ⟹ ∃τ. typed t τ"
proof(induction c arbitrary: τ)
  case Hole
  then show ?case
    by auto
next
  case (More f ss1 c ss2)

 then have "typed (Fun f (ss1 @ Fun⟨c;t⟩ # ss2)) τ"
    by simp

  then have "∃τ. typed (Fun⟨c;t⟩) τ"
    using subterm'
    by simp

  then obtain τ' where "typed (Fun⟨c;t⟩) τ'"
    by blast

  then show ?case
    using More.IH
    by simp
qed

end

locale term_typing =
  explicit_typing +
  typed: context_compatible_typing where typed = typed +
  welltyped: context_compatible_typing where typed = welltyped +
  welltyped: subterm_typing where typed = welltyped +
assumes all_terms_are_typed: "⋀t. is_typed t"
begin

sublocale typed: subterm_typing
  by unfold_locales (auto intro: all_terms_are_typed)

end

end