Theory Typing

theory Typing
  imports Main
begin

locale typing =
  fixes welltyped :: "'expr ⇒ 'ty ⇒ bool" (* TODO: Notation *)
  assumes right_unique: "right_unique welltyped"
begin

lemmas right_uniqueD [dest] = right_uniqueD[OF right_unique]

end

locale base_typing = typing
begin

abbreviation is_welltyped where 
  "is_welltyped expr ≡ ∃τ. welltyped expr τ"

end

locale typing_lifting = sub: typing where welltyped = sub_welltyped 
  for sub_welltyped :: "'sub ⇒ 'ty ⇒ bool" +
  fixes to_set :: "'expr ⇒ 'sub set" 
begin

definition is_welltyped where
  "is_welltyped expr ≡ ∃τ. ∀sub ∈ to_set expr. sub_welltyped sub τ"

abbreviation welltyped where
  "welltyped expr (_::unit) ≡ is_welltyped expr"

sublocale typing where welltyped = welltyped
  by unfold_locales (auto simp: right_unique_def)

end

end