Theory Typing

theory Typing
  imports Main
begin

locale predicate_typed =
  fixes typed :: "'expr ⇒ 'ty ⇒ bool"
  assumes right_unique: "right_unique typed"
begin

abbreviation is_typed where
  "is_typed expr ≡ ∃τ. typed expr τ"

lemmas right_uniqueD [dest] = right_uniqueD[OF right_unique]

end

definition uniform_typed_lifting where
  "uniform_typed_lifting to_set sub_typed expr ≡ ∃τ. ∀sub ∈ to_set expr. sub_typed sub τ"

definition is_typed_lifting where
  "is_typed_lifting to_set sub_is_typed expr ≡ ∀sub ∈ to_set expr. sub_is_typed sub"

locale typing =
  fixes is_typed is_welltyped
  assumes is_typed_if_is_welltyped:
    "⋀expr. is_welltyped expr ⟹ is_typed expr"

locale explicit_typing =
  typed: predicate_typed where typed = typed +
  welltyped: predicate_typed where typed = welltyped
for typed welltyped :: "'expr ⇒ 'ty ⇒ bool" +
assumes typed_if_welltyped: "⋀expr τ. welltyped expr τ ⟹ typed expr τ"
begin

abbreviation is_typed where
  "is_typed ≡ typed.is_typed"

abbreviation is_welltyped where
  "is_welltyped ≡ welltyped.is_typed"

sublocale typing where is_typed = is_typed and is_welltyped = is_welltyped
   using typed_if_welltyped
   by unfold_locales auto

lemma typed_welltyped_same_type:
  assumes "typed expr τ" "welltyped expr τ'"
  shows "τ = τ'"
  using assms typed_if_welltyped
  by blast

end

locale uniform_typing_lifting =
  sub: explicit_typing where typed = sub_typed and welltyped = sub_welltyped
for sub_typed sub_welltyped :: "'sub ⇒ 'ty ⇒ bool" +
fixes to_set :: "'expr ⇒ 'sub set"
begin

abbreviation is_typed where
  "is_typed ≡ uniform_typed_lifting to_set sub_typed"

lemmas is_typed_def = uniform_typed_lifting_def[of to_set sub_typed]

abbreviation is_welltyped where
  "is_welltyped ≡ uniform_typed_lifting to_set sub_welltyped"

lemmas is_welltyped_def = uniform_typed_lifting_def[of to_set sub_welltyped]

sublocale typing where is_typed = is_typed and is_welltyped = is_welltyped
proof unfold_locales
  fix expr
  assume "is_welltyped expr"
  then show "is_typed expr"
    using sub.typed_if_welltyped
    unfolding is_typed_def is_welltyped_def
    by auto
qed

end

locale typing_lifting =
  sub: typing where is_typed = sub_is_typed and is_welltyped = sub_is_welltyped
for sub_is_typed sub_is_welltyped :: "'sub ⇒ bool" +
fixes
  to_set :: "'expr ⇒ 'sub set"
begin

abbreviation is_typed where
  "is_typed ≡ is_typed_lifting to_set sub_is_typed"

lemmas is_typed_def = is_typed_lifting_def[of to_set sub_is_typed]

abbreviation is_welltyped where
  "is_welltyped ≡ is_typed_lifting to_set sub_is_welltyped"

lemmas is_welltyped_def = is_typed_lifting_def[of to_set sub_is_welltyped]

sublocale typing where is_typed = is_typed and is_welltyped = is_welltyped
proof unfold_locales
  fix expr
  assume "is_welltyped expr"
  then show "is_typed expr"
    using sub.is_typed_if_is_welltyped
    unfolding is_typed_def is_welltyped_def
    by simp
qed

end

end