Theory Weak_Typing

theory Weak_Typing
  imports Typing 
begin

locale weakly_welltyped = typing where welltyped = welltyped
for
  welltyped :: "'expr ⇒ 'ty ⇒ bool" and
  weakly_welltyped :: "'expr ⇒ bool" +
assumes
  weakly_welltyped_if_welltyped [intro]: "⋀expr. ∃τ. welltyped expr τ ⟹ weakly_welltyped expr"
  
locale weakly_welltyped_base = typing_lifting
begin

definition weakly_welltyped where
  "weakly_welltyped expr ≡
    ∀τ. ∀sub ∈ to_set expr. ∀sub' ∈ to_set expr. sub_welltyped sub τ ⟷ sub_welltyped sub' τ"

lemma all_sub_not_welltyped:
  assumes "¬is_welltyped expr" "weakly_welltyped expr"
  shows "∀sub ∈ to_set expr. ∀τ. ¬sub_welltyped sub τ"
  using assms
  unfolding is_welltyped_def weakly_welltyped_def
  by blast

sublocale weakly_welltyped where weakly_welltyped = weakly_welltyped and welltyped = welltyped
proof unfold_locales 
  fix expr
  assume "∃τ. welltyped expr τ"

  then show "weakly_welltyped expr"
    using is_welltyped_def weakly_welltyped_def
    by auto
qed

end

locale weakly_welltyped_lifting =
  sub: weakly_welltyped where
  weakly_welltyped = sub_weakly_welltyped and welltyped = sub_welltyped +
  typing_lifting where to_set = to_set
for 
  to_set :: "'expr ⇒ 'sub set" and
  sub_weakly_welltyped 
begin

definition weakly_welltyped :: "'expr ⇒ bool" where
  "weakly_welltyped expr ≡ ∀sub ∈ to_set expr. sub_weakly_welltyped sub"

sublocale weakly_welltyped where
  weakly_welltyped = weakly_welltyped and welltyped = welltyped
proof unfold_locales
  fix expr

  show "∃τ. welltyped expr τ ⟹ weakly_welltyped expr"
    using sub.weakly_welltyped_if_welltyped
    unfolding is_welltyped_def weakly_welltyped_def
    by auto
qed

(*
TODO: 
lemma ex_sub_not_welltyped:
  "¬is_welltyped expr ⟹ weakly_welltyped expr ⟹ ∃sub ∈ to_set expr. ¬sub.is_welltyped sub"
  using is_welltyped_def
  by simp*)

end

end