Theory First_Order_Clause.Nonground_Term_Typing

theory Nonground_Term_Typing
  imports
    Term_Typing
    Typed_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_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 ` var_subst ρ ` X)) 𝒱 σ"
proof (intro ballI impI)
  fix y

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

  obtain x where y: "y ⋅v id_subst = x ⋅v ρ" 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: "𝒱 ⊢ x ⋅v id_subst : 𝒱 (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  "𝒱 ⊢ x ⋅v ρ ⊙ σ : 𝒱 (rename ρ x)"
    by (metis ρ_σ_type_preserving right_uniqueD welltyped_id_subst x_in_X)

  then show "𝒱 ⊢ y ⋅v σ : 𝒱 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 term_vars = term_vars +
  base_typed_substitution where
     subst = term_subst and vars = term_vars and welltyped = welltyped +
  "term": base_typing_properties where 
     subst = term_subst and vars = term_vars 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 subst = term_subst and vars = term_vars 
for 
  welltyped :: "('v, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool" and
  term_vars :: "'t ⇒ 'v set"
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_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 term_vars = term_vars +
  term_typing_properties where welltyped = welltyped and term_vars = term_vars
for
  welltyped :: "('v, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool" and
  term_vars :: "'t ⇒ 'v set" +
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