Theory Nonground_Term_Typing

theory Nonground_Term_Typing
  imports
    Term_Typing
    Typed_Functional_Substitution
    Nonground_Context
begin

locale base_typing_properties =
  base_typed_renaming +
  base_typed_subst_stability +
  replaceable_𝒱 where
    base_subst = subst and base_vars = vars and base_welltyped = welltyped +
  typed_grounding_functional_substitution where 
    base_subst = subst and base_vars = vars and base_welltyped = welltyped
begin

lemma type_preserving_on_subst_compose_renaming:
  assumes
    ρ: "is_renaming ρ" and
    ρ_type_preserving: "type_preserving_on X 𝒱 ρ" and 
    ρ_σ_type_preserving: "type_preserving_on X 𝒱 (ρ ⊙ σ)" 
  shows "type_preserving_on (⋃(vars `ρ ` X)) 𝒱 σ"
proof (intro ballI impI)
  fix y

  assume y_in_ρ_X: "y ∈ ⋃ (vars ` ρ ` X)" and y_welltyped: "𝒱 ⊢ id_subst y : 𝒱 y"

  obtain x where y: "id_subst y = ρ x" and x_in_X: "x ∈ X"
    using obtain_renamed_variable[OF ρ] vars_id_subst y_in_ρ_X
    by (smt (verit, best) UN_E UN_simps(10) singletonD)

  then have x_is_welltyped: "𝒱 ⊢ id_subst x : 𝒱 (rename ρ x)"
    using ρ ρ_type_preserving y_welltyped
    by (smt (verit, del_insts) comp_subst_iff id_subst_rename left_neutral
        singletonD vars_id_subst welltyped_id_subst welltyped_subst_stability)

  then have  "𝒱 ⊢ (comp_subst ρ σ) x : 𝒱 (rename ρ x)"
    by (metis ρ_σ_type_preserving right_uniqueD welltyped_id_subst x_in_X)

  then show "𝒱 ⊢ σ y : 𝒱 y" 
    unfolding comp_subst_iff
    using y_welltyped y
    by (metis (full_types) ρ comp_subst_iff id_subst_rename inv_renaming left_neutral)
qed

end

locale term_typing_properties = 
  "term": nonground_term where Var = Var +
  base_typed_functional_substitution where
  id_subst = Var and subst = term_subst and vars = term_vars and 
  welltyped = welltyped +
  "term": base_typing_properties where 
  subst = term_subst and vars = term_vars and id_subst = Var and comp_subst = "(⊙)" and 
  to_ground = term_to_ground and from_ground = term_from_ground and welltyped = welltyped  +
  type_preserving_imgu where
  welltyped = welltyped and id_subst = Var and subst = term_subst and vars = term_vars 
for 
  welltyped :: "('v, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool" and
  Var :: "'v ⇒ 't"
begin

(* TODO: Move as far up as possible *)
notation welltyped (‹_ ⊢ _ : _› [1000, 0, 50] 50)

sublocale "term": base_typing where welltyped = "welltyped 𝒱" for 𝒱
  using typing_axioms
  unfolding base_typing_def .

end

locale base_witnessed_typing_properties =
  base_typing_properties +
  witnessed_typed_functional_substitution where 
  welltyped = welltyped and base_subst = subst and base_vars = vars and base_welltyped = welltyped

locale context_compatible_term_typing_properties = 
  nonground_term_with_context where Var = Var +
  term_typing_properties where Var = Var and welltyped = welltyped
for 
  welltyped :: "('v, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool" and
  Var :: "'v ⇒ 't" +
assumes "⋀𝒱. term_typing (welltyped 𝒱) apply_context"
begin

sublocale "term": term_typing where 
  welltyped = "welltyped 𝒱" and apply_context = apply_context for 𝒱
  using
    context_compatible_term_typing_properties_axioms 
    context_compatible_term_typing_properties_axioms_def 
    context_compatible_term_typing_properties_def
  by metis

end

end