Theory Typed_Substitution

theory Typed_Substitution
  imports
    Typing
    Abstract_Substitution.Based_Substitution
    Infinite_Variables_Per_Type
begin

(* TODO: Move Typed_Substitution to own AFP Entry *)

type_synonym ('v, 'ty) var_types = "'v ⇒ 'ty"

locale base_typed_substitution =
  base_substitution where id_subst = id_subst and apply_subst = apply_subst
for
  id_subst :: "'subst" and
  welltyped :: "('v, 'ty) var_types ⇒ 'base ⇒ 'ty ⇒ bool" and
  apply_subst :: "'v ⇒ 'subst ⇒ 'base" (infixl "⋅v" 69) +
assumes
  "⋀𝒱. typing (welltyped 𝒱)" and
  welltyped_id_subst [intro]: 
  "⋀𝒱 x. welltyped 𝒱 (x ⋅v id_subst) (𝒱 x) ∨ (∄τ. welltyped 𝒱 (x ⋅v id_subst) τ)" 
begin

notation welltyped (‹_ ⊢ _ : _› [1000, 0, 50] 50)

sublocale typing "welltyped 𝒱"
  using base_typed_substitution_axioms
  unfolding base_typed_substitution_axioms_def base_typed_substitution_def
  by metis

abbreviation type_preserving_on :: "'v set ⇒ ('v, 'ty) var_types ⇒ 'subst ⇒ bool" where
  "type_preserving_on X 𝒱 σ ≡ ∀x ∈ X. 𝒱 ⊢ x ⋅v id_subst : 𝒱 x ⟶ 𝒱 ⊢ x ⋅v σ : 𝒱 x"

(* TODO: Could this definition make my life easier in proofs?
   I can recover the other one using `welltyped_id_subst` *)
abbreviation type_preserving_on' :: "'v set ⇒ ('v, 'ty) var_types ⇒ 'subst ⇒ bool" where
  "type_preserving_on' X 𝒱 σ ≡ ∀x ∈ X. ∀τ. 𝒱 ⊢ x ⋅v id_subst : τ ⟶ 𝒱 ⊢ x ⋅v σ : τ"

lemma "type_preserving_on X 𝒱 σ ⟷ type_preserving_on' X 𝒱 σ"
  using welltyped_id_subst 
  by blast

abbreviation type_preserving where
  "type_preserving ≡ type_preserving_on UNIV"

lemma type_preserving_on_subst_update: 
  assumes "type_preserving_on X 𝒱 σ" "x ∈ X ⟶ 𝒱 ⊢ x ⋅v id_subst : 𝒱 x ⟶ 𝒱 ⊢ update : 𝒱 x"
  shows "type_preserving_on X 𝒱 (σ⟦x := update⟧)"
  using assms
  by (metis subst_update)  

lemma type_preserving_on_subset:
  assumes "type_preserving_on Y 𝒱 σ" "X ⊆ Y"
  shows "type_preserving_on X 𝒱 σ"
  using assms
  by blast

lemma type_preserving_on_union [simp]: 
  "type_preserving_on (X ∪ Y) 𝒱 μ ⟷ type_preserving_on X 𝒱 μ ∧ type_preserving_on Y 𝒱 μ"
  by auto

lemma type_preserving_on_id_subst [intro]: "type_preserving_on X 𝒱 id_subst"
  by auto

abbreviation type_preserving_unifier where
  "type_preserving_unifier 𝒱 υ expr expr' ≡
    type_preserving_on (vars expr ∪ vars expr') 𝒱 υ ∧ expr ⋅ υ = expr' ⋅ υ"

end

locale typed_substitution =
  based_substitution where vars = vars and id_subst = id_subst and apply_subst = apply_subst +
  base: base_typed_substitution where
    subst = base_subst and vars = base_vars and welltyped = base_welltyped and
    id_subst = id_subst and apply_subst = apply_subst
for
  base_welltyped :: "('v, 'ty) var_types ⇒ 'base ⇒ 'ty ⇒ bool" and 
  vars :: "'expr ⇒ 'v set" and
  welltyped :: "('v, 'ty) var_types ⇒ 'expr ⇒ 'ty' ⇒ bool" and
  id_subst :: "'subst" and 
  apply_subst :: "'v ⇒ 'subst ⇒ 'base" (infixl "⋅v" 69) +
assumes "⋀𝒱. typing (welltyped 𝒱)"
begin

sublocale typing "welltyped 𝒱"
  using typed_substitution_axioms
  unfolding typed_substitution_axioms_def typed_substitution_def
  by metis

end

locale witnessed_typed_substitution =
 typed_substitution +
 subst_updates +
 assumes types_witnessed: "⋀𝒱 τ. ∃b. base.is_ground b ∧ base_welltyped 𝒱 b τ"
begin

lemma type_preserving_ground_subst_extension:
  assumes
    grounding: "is_ground (expr ⋅ γ)" and
    γ_type_preserving_on: "base.type_preserving_on (vars expr) 𝒱 γ"
  obtains γ'
  where
    "base.is_ground_subst γ'"
    "base.type_preserving_on UNIV 𝒱 γ'"
    "∀x ∈ vars expr. x ⋅v γ = x ⋅v γ'"
proof (rule that)

  (* TODO: Nicer notation *)
 define γ' where
    "γ' ≡ subst_updates γ (λx. if x ∈ vars expr
                               then None 
                               else Some (SOME b. base.is_ground b ∧ base_welltyped 𝒱 b (𝒱 x)))"

  show "base.is_ground_subst γ'"
  proof(unfold base.is_ground_subst_def, intro allI)
    fix b

    {
      fix x

      have "base.is_ground (x ⋅v γ')"
      proof(cases "x ∈ vars expr")
        case True

        then show ?thesis
          unfolding γ'_def
          using variable_grounding[OF grounding]
          by auto
      next
        case False

        then have "x ⋅v γ' = (SOME b. base.is_ground b ∧ base_welltyped 𝒱 b (𝒱 x))"
          unfolding γ'_def
          by simp

        then show ?thesis
          by (smt (verit) types_witnessed tfl_some)
      qed
    }

    then show "base.is_ground (base_subst b γ')"
      using base.is_grounding_iff_vars_grounded
      by auto
  qed

  show "base.type_preserving_on UNIV 𝒱 γ'"
    unfolding γ'_def
    using γ_type_preserving_on types_witnessed
    by (simp add: verit_sko_ex_indirect)

  show "∀x ∈ vars expr. x ⋅v γ = x ⋅v γ'"
    by (simp add: γ'_def)
qed

lemma type_preserving_on_ground_subst_extension:
  assumes
    grounding: "is_ground (expr ⋅ γ)" and
    γ_type_preserving_on: "base.type_preserving_on (vars expr) 𝒱 γ"
  obtains γ'
  where
    "is_ground (expr' ⋅ γ')"
    "base.type_preserving_on (vars expr') 𝒱 γ'"
    "∀x ∈ vars expr. x ⋅v γ = x ⋅v γ'"
  using type_preserving_ground_subst_extension[OF assms]
  unfolding base.is_ground_subst_def is_grounding_iff_vars_grounded
  by (metis UNIV_I base.comp_subst_iff left_neutral)

end

sublocale base_typed_substitution ⊆ typed_substitution where
  base_subst = subst and base_vars = vars and base_welltyped = welltyped
  by unfold_locales

locale typed_grounding_substitution = typed_substitution + grounding

locale typed_subst_stability = typed_substitution +
  assumes
    welltyped_subst_stability [simp]: "⋀𝒱 expr σ τ.
      base.type_preserving_on (vars expr) 𝒱 σ ⟹ welltyped 𝒱 (expr ⋅ σ) τ ⟷ welltyped 𝒱 expr τ"
begin

(* TODO: Name *)
lemma welltyped_subst_stability' [simp]:
  assumes "base.type_preserving_on X 𝒱 σ" "vars expr ⊆ X"
  shows "welltyped 𝒱 (expr ⋅ σ) τ ⟷ welltyped 𝒱 expr τ"
  using assms
  by (simp add: subset_iff)

lemma type_preserving_unifier:
  assumes 
    unifier: "expr ⋅ υ = expr' ⋅ υ" and
    type_preserving: "base.type_preserving_on (vars expr ∪ vars expr') 𝒱 υ"
  shows "⋀τ. welltyped 𝒱 expr τ ⟷ welltyped 𝒱 expr' τ"
  using assms
  by (metis UnCI welltyped_subst_stability)

lemma unifier_same_type:
  assumes "base.type_preserving_on (vars expr ∪ vars expr') 𝒱 μ" "is_unifier μ {expr, expr'}"
  shows "∀τ. welltyped 𝒱 expr τ ⟷ welltyped 𝒱 expr' τ"
  using assms type_preserving_unifier
  by simp
  
(*lemma imgu_same_type:
  assumes "base.type_preserving_on (vars expr ∪ vars expr') 𝒱 μ" "is_imgu μ {{expr, expr'}}"
  shows "∀τ. welltyped 𝒱 expr τ ⟷ welltyped 𝒱 expr' τ"
  using unifier_same_type assms
  unfolding is_imgu_def is_unifier_set_def
  by blast*)

(* TODO: Make this main *)
lemma imgu_same_type:
  assumes "base.type_preserving_on X 𝒱 μ" "is_imgu μ {{expr, expr'}}" "vars expr ∪ vars expr' ⊆ X" 
  shows "∀τ. welltyped 𝒱 expr τ ⟷ welltyped 𝒱 expr' τ"
  using unifier_same_type assms
  unfolding is_imgu_def is_unifier_set_def
  by blast

end

locale base_typed_subst_stability = 
  base_typed_substitution +
  typed_subst_stability where base_subst = subst and base_vars = vars and base_welltyped = welltyped
begin

lemma type_preserving_ground_compose_ground_subst:
  assumes "is_ground_subst γ'" "type_preserving_on UNIV 𝒱 γ'" "type_preserving_on X 𝒱 μ"
  shows "type_preserving_on X 𝒱 (μ ⊙ γ')"
  using assms
  by (smt (verit) UNIV_I all_subst_ident_if_ground comp_subst_iff type_preserving_unifier
      is_ground_subst_is_ground)

lemma type_preserving_on_subst_compose [intro]:
  assumes
    σ_type_preserving: "type_preserving_on X 𝒱 σ" and 
    σ'_type_preserving: "type_preserving_on (⋃(vars ` var_subst σ ` X)) 𝒱 σ'"
  shows "type_preserving_on X 𝒱 (σ ⊙ σ')"
proof (intro ballI impI)
  fix x
  assume 
    x_in_X: "x ∈ X" and
    welltyped_x: "𝒱 ⊢ x ⋅v id_subst : 𝒱 x"

  then have "𝒱 ⊢ x ⋅v σ : 𝒱 x"
    using assms
    by blast

  then show "𝒱 ⊢ x ⋅v (σ ⊙ σ') : 𝒱 x"
    unfolding comp_subst_iff
    using σ'_type_preserving x_in_X
    by fastforce
qed

lemma type_preserving_subst_compose [intro]:
  assumes
    σ_type_preserving: "type_preserving 𝒱 σ" and
    σ'_type_preserving: "type_preserving 𝒱 σ'"
  shows "type_preserving 𝒱 (σ ⊙ σ')"
  using type_preserving_on_subst_compose[OF σ_type_preserving] σ'_type_preserving
  by simp 

end

locale replaceable_𝒱 = typed_substitution +
  assumes replace_𝒱:
    "⋀expr 𝒱 𝒱' τ. ∀x∈ vars expr. 𝒱 x = 𝒱' x ⟹ welltyped 𝒱 expr τ ⟹ welltyped 𝒱' expr τ"
begin

lemma replace_𝒱_iff:
  assumes "∀x∈ vars expr. 𝒱 x = 𝒱' x"
  shows "welltyped 𝒱 expr τ ⟷ welltyped 𝒱' expr τ"
  using assms
  by (metis replace_𝒱)

lemma is_ground_replace_𝒱:
  assumes "is_ground expr"
  shows "welltyped 𝒱 expr τ ⟷ welltyped 𝒱' expr τ"
  using replace_𝒱_iff assms
  by blast

end

(* TODO: Could this be proven using replaceable_V and welltyped_subst_stability? *)
locale typed_renaming = 
  typed_substitution + 
  renaming_variables +
  assumes
    welltyped_renaming [simp]:
    "⋀𝒱 𝒱' expr ρ τ. is_renaming ρ ⟹
      ∀x ∈ vars expr. 𝒱 x = 𝒱' (rename ρ x) ⟹
      welltyped 𝒱' (expr ⋅ ρ) τ ⟷ welltyped 𝒱 expr τ"

locale base_typed_renaming =
  base_typed_substitution where
    welltyped = welltyped +
  typed_renaming where
    base_subst = subst and base_vars = vars and base_welltyped = welltyped and
    welltyped = welltyped +
  replaceable_𝒱 where
    base_subst = subst and base_vars = vars and base_welltyped = welltyped and
    welltyped = welltyped +
  subst_updates
  for welltyped :: "('v, 'ty) var_types ⇒ 'expr ⇒ 'ty ⇒ bool"
begin

lemma renaming_ground_subst:
  assumes
    ρ: "is_renaming ρ" and
    γ: "is_ground_subst γ" and
    welltyped_ρ: "type_preserving_on X 𝒱 ρ" and
    welltyped_γ: "type_preserving_on (⋃(vars ` var_subst ρ ` X)) 𝒱' γ" and
    rename: "∀x ∈ X. 𝒱 x = 𝒱' (rename ρ x)"
  shows "type_preserving_on X 𝒱 (ρ ⊙ γ)"
proof(intro ballI impI iffI)
  fix x
  assume 
    x_in_X: "x ∈ X" and 
    "𝒱 ⊢ x ⋅v id_subst : 𝒱 x"

  then have welltyped_ρ_x: "𝒱 ⊢ x ⋅v ρ : 𝒱 x"
    using welltyped_ρ
    by metis

  define y where "y ≡ (rename ρ x)"

  have "y ∈ ⋃(vars ` var_subst ρ ` X)"
    using x_in_X
    unfolding y_def
    by (metis UN_iff ρ id_subst_rename image_eqI singletonI vars_id_subst)

  moreover then have "𝒱 ⊢ y ⋅v γ : 𝒱' y"
    using replace_𝒱 γ welltyped_γ rename x_in_X welltyped_ρ_x id_subst_rename[OF ρ]
    unfolding y_def is_ground_subst_def
    by (metis is_ground_replace_𝒱 right_uniqueD singleton_iff variable_grounding vars_id_subst 
        welltyped_id_subst)
 
  ultimately have "𝒱 ⊢ y ⋅v γ : 𝒱 x"
    unfolding y_def
    using rename x_in_X
    by fastforce

  moreover have "y ⋅v γ = x ⋅v (ρ ⊙ γ)"
    unfolding y_def
    by (metis ρ comp_subst_iff id_subst_rename left_neutral)

  ultimately show "𝒱 ⊢ x ⋅v (ρ ⊙ γ) : 𝒱 x"
    by argo
qed

lemma obtain_type_preserving_renaming:
  fixes 𝒱 :: "'v ⇒ 'ty"
  assumes
    "finite X"
    "infinite_variables_per_type 𝒱"
  obtains ρ where
    "is_renaming ρ"
    "var_subst id_subst ` X ∩ var_subst ρ ` Y = {}"
    "type_preserving_on Y 𝒱 ρ"
proof-

  obtain renaming :: "'v ⇒ 'v" where
    inj: "inj renaming" and
    rename_apart: "X ∩ renaming ` Y = {}" and
    preserve_type: "∀x ∈ Y. 𝒱 (renaming x) = 𝒱 x"
    using obtain_type_preserving_inj[OF assms].

  (* TODO: Can I write this nicer? *)
  define ρ where
    "ρ ≡ subst_updates id_subst (λx. Some (renaming x ⋅v id_subst))"

  have ρ: "is_renaming ρ"
      using inj inj_id_subst
      unfolding ρ_def is_renaming_iff inj_def
      by auto

  then show ?thesis
  proof (rule that)

    show "var_subst id_subst ` X ∩ var_subst ρ ` Y = {}"
      using rename_apart inj_id_subst
      unfolding ρ_def inj_def
      by auto
  next

    {
      fix x
      assume x_in_Y: "x ∈ Y" and welltyped_x: "𝒱 ⊢ x ⋅v id_subst : 𝒱 x"

      have "∀x∈vars (x ⋅v id_subst). 𝒱 x = 𝒱 (rename ρ x)"
        using ρ
        unfolding ρ_def
        by (smt (verit, del_insts) empty_iff id_subst_rename insert_iff option.simps(5)
            preserve_type subst_updates vars_id_subst x_in_Y)

      then have "𝒱 ⊢ x ⋅v ρ : 𝒱 x"
        using welltyped_renaming[OF ρ] welltyped_x
        by (metis id_subst_subst)
    }

    then show "type_preserving_on Y 𝒱 ρ"
      by metis
  qed
qed

lemma obtain_type_preserving_renamings:
  fixes 𝒱⇩1 𝒱⇩2 :: "'v ⇒ 'ty"
  assumes
    "finite X"
    "infinite_variables_per_type 𝒱⇩2"
  obtains ρ⇩1 ρ⇩2 where
    "is_renaming ρ⇩1"
    "is_renaming ρ⇩2"
    "var_subst ρ⇩1 ` X ∩ var_subst ρ⇩2 ` Y = {}"
    "type_preserving_on X 𝒱⇩1 ρ⇩1"
    "type_preserving_on Y 𝒱⇩2 ρ⇩2"
  using obtain_type_preserving_renaming[OF assms] is_renaming_id_subst welltyped_id_subst
  by metis

lemma obtain_type_preserving_renamings':
  fixes 𝒱⇩1 𝒱⇩2 :: "'v ⇒ 'ty"
  assumes
    "finite Y"
    "infinite_variables_per_type 𝒱⇩1"
  obtains ρ⇩1 ρ⇩2 where
    "is_renaming ρ⇩1"
    "is_renaming ρ⇩2"
    "var_subst ρ⇩1 ` X ∩ var_subst ρ⇩2 ` Y = {}"
    "type_preserving_on X 𝒱⇩1 ρ⇩1"
    "type_preserving_on Y 𝒱⇩2 ρ⇩2"
  using obtain_type_preserving_renamings[OF assms]
  by (metis inf_commute)

end

lemma (in renaming_variables) obtain_merged_𝒱:
  assumes
    ρ⇩1: "is_renaming ρ⇩1" and
    ρ⇩2: "is_renaming ρ⇩2" and
    rename_apart: "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}" and
    finite_vars: "finite (vars expr)" "finite (vars expr')" and
    infinite_UNIV: "infinite (UNIV :: 'c set)"
  obtains 𝒱⇩3 where
    "infinite_variables_per_type_on X 𝒱⇩3"
    "∀x∈vars expr. 𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
    "∀x∈vars expr'. 𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
proof -

  have finite: "finite (vars (expr ⋅ ρ⇩1))" "finite (vars (expr' ⋅ ρ⇩2))"
    using finite_vars
    by (simp_all add: ρ⇩1 ρ⇩2 rename_variables)

  obtain 𝒱⇩3 where 
    𝒱⇩3: "infinite_variables_per_type_on X 𝒱⇩3" and
    𝒱⇩3_𝒱⇩1: "∀x∈vars (expr ⋅ ρ⇩1). 𝒱⇩3 x = 𝒱⇩1 (inv (var_subst ρ⇩1) (x ⋅v id_subst))" and
    𝒱⇩3_𝒱⇩2: "∀x∈vars (expr' ⋅ ρ⇩2). 𝒱⇩3 x = 𝒱⇩2 (inv (var_subst ρ⇩2) (x ⋅v id_subst))"
    using obtain_infinite_variables_per_type_on[OF infinite_UNIV finite rename_apart] .

  show ?thesis
  proof (rule that[OF 𝒱⇩3])

    show "∀x∈vars expr. 𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
      using 𝒱⇩3_𝒱⇩1 ρ⇩1 inv_renaming rename_variables
      by auto
  next

    show "∀x∈vars expr'. 𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
      using 𝒱⇩3_𝒱⇩2 ρ⇩2 inv_renaming rename_variables
      by auto
  qed
qed

lemma (in renaming_variables) obtain_merged_𝒱_infinite_variables_for_all_types:
  assumes
    ρ⇩1: "is_renaming ρ⇩1" and
    ρ⇩2: "is_renaming ρ⇩2" and
    rename_apart: "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}" and
    𝒱⇩2: "infinite_variables_for_all_types 𝒱⇩2" and
    finite_vars: "finite (vars expr)"
  obtains 𝒱⇩3 where
    "∀x∈vars expr. 𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
    "∀x∈vars expr'. 𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
    "infinite_variables_for_all_types 𝒱⇩3"
proof (rule that)

  define 𝒱⇩3 where
    "⋀x. 𝒱⇩3 x ≡
        if x ∈ vars (expr ⋅ ρ⇩1)
        then 𝒱⇩1 (inv (var_subst ρ⇩1) (x ⋅v id_subst))
        else 𝒱⇩2 (inv (var_subst ρ⇩2) (x ⋅v id_subst))"

  show "∀x∈vars expr. 𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
  proof (intro ballI)
    fix x
    assume "x ∈ vars expr"

    then have "rename ρ⇩1 x ∈ vars (expr ⋅ ρ⇩1)"
      using rename_variables[OF ρ⇩1]
      by blast

    then show "𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
      unfolding 𝒱⇩3_def
      by (simp add: ρ⇩1 inv_renaming)
  qed

  show "∀x∈vars expr'. 𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
  proof (intro ballI)
    fix x
    assume "x∈ vars expr'"

    then have "rename ρ⇩2 x ∈ vars (expr' ⋅ ρ⇩2)"
      using rename_variables[OF ρ⇩2]
      by blast

    then show "𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
      unfolding 𝒱⇩3_def
      using ρ⇩2 inv_renaming rename_apart
      by (metis (mono_tags, lifting) disjoint_iff id_subst_rename)
  qed

  have "finite {x. x ∈ vars (expr ⋅ ρ⇩1)}"
    using finite_vars
    by (simp add: ρ⇩1 rename_variables)

  moreover {
    fix τ

    have "infinite {x. 𝒱⇩2 (inv (var_subst ρ⇩2) (x ⋅v id_subst)) = τ}"
    proof(rule surj_infinite_set[OF surj_inv_renaming, OF ρ⇩2])

      show "infinite {x. 𝒱⇩2 x = τ}"
        using 𝒱⇩2
        unfolding infinite_variables_for_all_types_def
        by blast
    qed
  }

  ultimately show "infinite_variables_for_all_types 𝒱⇩3"
    unfolding infinite_variables_for_all_types_def 𝒱⇩3_def if_distrib if_distribR Collect_if_eq
      Collect_not_mem_conj_eq
    by auto
qed

lemma (in renaming_variables) obtain_merged_𝒱'_infinite_variables_for_all_types:
  assumes
    ρ⇩1: "is_renaming ρ⇩1" and
    ρ⇩2: "is_renaming ρ⇩2" and
    rename_apart: "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}" and
    𝒱⇩1: "infinite_variables_for_all_types 𝒱⇩1" and
    finite_vars: "finite (vars expr')"
  obtains 𝒱⇩3 where
    "∀x∈vars expr. 𝒱⇩1 x = 𝒱⇩3 (rename ρ⇩1 x)"
    "∀x∈vars expr'. 𝒱⇩2 x = 𝒱⇩3 (rename ρ⇩2 x)"
    "infinite_variables_for_all_types 𝒱⇩3"
  using obtain_merged_𝒱_infinite_variables_for_all_types[OF ρ⇩2 ρ⇩1 _ 𝒱⇩1 finite_vars] rename_apart
  by (metis disjoint_iff)

locale based_typed_renaming =
  base: base_typed_renaming where
    subst = base_subst and vars = "base_vars :: 'base ⇒ 'v set" and
    welltyped = "base_welltyped :: ('v ⇒ 'ty) ⇒ 'base ⇒ 'ty ⇒ bool" +
  typed_renaming
begin

lemma renaming_grounding:
  assumes
    renaming: "base.is_renaming ρ" and
    ρ_γ_type_preserving: "base.type_preserving_on (vars expr) 𝒱 (ρ ⊙ γ)" and
    grounding: "is_ground (expr ⋅ ρ ⊙ γ)" and
    𝒱_𝒱': "∀x ∈ vars expr. 𝒱 x = 𝒱' (rename ρ x)"
  shows "base.type_preserving_on (vars (expr ⋅ ρ)) 𝒱' γ"
proof(intro ballI impI)
  fix x

  define y where "y ≡ inv (var_subst ρ) (x ⋅v id_subst)"

  assume 
    x_in_expr: "x ∈ vars (expr ⋅ ρ)" and 
    welltyped_x: "base_welltyped 𝒱' (x ⋅v id_subst) (𝒱' x)"

  then have y_in_vars: "y ∈ vars expr"
    using base.renaming_inv_in_vars[OF renaming] base.vars_id_subst
    unfolding y_def base.vars_subst vars_subst
    by fastforce

  then have "base.is_ground (base_subst (y ⋅v id_subst) (ρ ⊙ γ))"
    using variable_grounding[OF grounding y_in_vars]
    by (metis base.comp_subst_iff base.left_neutral)

  moreover have inv_renaming: "(inv (λx. x ⋅v ρ) (x ⋅v id_subst) ⋅v ρ) = (x ⋅v id_subst)"
    using renaming renaming_inv_into x_in_expr
    by blast

  then have "base_welltyped 𝒱 (base_subst (y ⋅v id_subst) (ρ ⊙ γ)) (𝒱 y)"
    using ρ_γ_type_preserving y_in_vars welltyped_x x_in_expr 𝒱_𝒱'
    unfolding y_def
    by (smt (verit, del_insts) assms(1) base.id_subst_subst base.vars_id_subst 
        base.welltyped_renaming empty_iff id_subst_rename insert_iff)
   

  ultimately have "base_welltyped 𝒱' (base_subst (y ⋅v id_subst) (ρ ⊙ γ)) (𝒱 y)"
    using base.is_ground_replace_𝒱 
    by blast

  moreover have "base_subst (y ⋅v id_subst) (ρ ⊙ γ) = x ⋅v γ"
    using x_in_expr base.renaming_inv_into[OF renaming] base.left_neutral
    unfolding y_def vars_subst base.comp_subst_iff
    by (simp add: inv_renaming)

  ultimately show "base_welltyped 𝒱' (x ⋅v γ) (𝒱' x)"
    using 𝒱_𝒱'[rule_format] welltyped_x
    by (metis base.right_uniqueD base.welltyped_id_subst id_subst_rename renaming renaming_inv_into
        x_in_expr y_def y_in_vars)
qed

lemma obtain_merged_grounding:
  fixes 𝒱⇩1 𝒱⇩2 :: "'v ⇒ 'ty"
  assumes
    "base.type_preserving_on (vars expr) 𝒱⇩1 γ⇩1"
    "base.type_preserving_on (vars expr') 𝒱⇩2 γ⇩2"
    "is_ground (expr ⋅ γ⇩1)"
    "is_ground (expr' ⋅ γ⇩2)" and
    𝒱⇩2: "infinite_variables_per_type 𝒱⇩2" and
    finite_vars: "finite (vars expr)"
  obtains ρ⇩1 ρ⇩2 γ  where
    "base.is_renaming ρ⇩1"
    "base.is_renaming ρ⇩2"
    "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}"
    "base.type_preserving_on (vars expr) 𝒱⇩1 ρ⇩1"
    "base.type_preserving_on (vars expr') 𝒱⇩2 ρ⇩2"
    "∀x ∈ vars expr. x ⋅v γ⇩1 =  x ⋅v ρ⇩1 ⊙ γ"
    "∀x ∈ vars expr'. x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
proof -

  obtain ρ⇩1 ρ⇩2 where
    ρ⇩1: "base.is_renaming ρ⇩1" and
    ρ⇩2: "base.is_renaming ρ⇩2" and
    rename_apart: "var_subst ρ⇩1 ` (vars expr) ∩ var_subst ρ⇩2 ` (vars expr') = {}" and
    ρ⇩1_is_welltyped: "base.type_preserving_on (vars expr) 𝒱⇩1 ρ⇩1" and
    ρ⇩2_is_welltyped: "base.type_preserving_on (vars expr') 𝒱⇩2 ρ⇩2"
    using base.obtain_type_preserving_renamings[OF finite_vars 𝒱⇩2].

  have rename_apart: "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}"
    using rename_apart rename_variables_id_subst[OF ρ⇩1] rename_variables_id_subst[OF ρ⇩2]
    by blast

  from ρ⇩1 ρ⇩2 obtain ρ⇩1_inv ρ⇩2_inv where
    ρ⇩1_inv: "ρ⇩1 ⊙ ρ⇩1_inv = id_subst" and
    ρ⇩2_inv: "ρ⇩2 ⊙ ρ⇩2_inv = id_subst"
    unfolding base.is_renaming_def
    by blast

  define γ where
    "γ ≡ subst_updates id_subst (λx. if x ∈ vars (expr ⋅ ρ⇩1) then Some (x ⋅v ρ⇩1_inv ⊙ γ⇩1) else Some (x ⋅v ρ⇩2_inv ⊙ γ⇩2))"

  show ?thesis
  proof (rule that[OF ρ⇩1 ρ⇩2 rename_apart ρ⇩1_is_welltyped ρ⇩2_is_welltyped])

    have "∀x∈ vars expr.  x ⋅v γ⇩1 = x ⋅v ρ⇩1 ⊙ γ"
    proof (intro ballI)
      fix x
      assume x_in_vars: "x ∈ vars expr"

      obtain y where y: "x ⋅v ρ⇩1 = y ⋅v id_subst"
        using obtain_renamed_variable[OF ρ⇩1] .

      then have "y ∈ vars (expr ⋅ ρ⇩1)"
        using x_in_vars ρ⇩1 rename_variables_id_subst
        by (metis base.inj_id_subst image_eqI inj_image_mem_iff)

      then have "y ⋅v γ = base_subst (y ⋅v ρ⇩1_inv) γ⇩1"
        unfolding γ_def
        using base.comp_subst_iff
        by simp

      then show "x ⋅v γ⇩1 = x ⋅v ρ⇩1 ⊙ γ"
        by (metis ρ⇩1_inv base.comp_subst_iff base.left_neutral y)
    qed

    then show "∀x ∈ vars expr. x ⋅v γ⇩1 = x ⋅v ρ⇩1 ⊙ γ"
      by auto

  next

    have "∀x∈ vars expr'. x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
    proof (intro ballI)
      fix x
      assume x_in_vars: "x ∈ vars expr'"

      obtain y where y: "x ⋅v ρ⇩2 = y ⋅v id_subst"
        using obtain_renamed_variable[OF ρ⇩2].

      then have "y ∈ vars (expr' ⋅ ρ⇩2)"
        using x_in_vars ρ⇩2 rename_variables_id_subst
        by (metis base.inj_id_subst imageI inj_image_mem_iff)

      then have "y ⋅v γ = base_subst (y ⋅v ρ⇩2_inv) γ⇩2"
        unfolding γ_def
        using base.comp_subst_iff rename_apart
        by auto

      then show "x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
        by (metis ρ⇩2_inv base.comp_subst_iff base.left_neutral y)
    qed

    then show "∀x ∈ vars expr'. x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
      by auto
  qed
qed

lemma obtain_merged_grounding':
  fixes 𝒱⇩1 𝒱⇩2 :: "'v ⇒ 'ty"
  assumes
    typed_γ⇩1: "base.type_preserving_on (vars expr) 𝒱⇩1 γ⇩1" and
    typed_γ⇩2: "base.type_preserving_on (vars expr') 𝒱⇩2 γ⇩2" and
    expr_grounding: "is_ground (expr ⋅ γ⇩1)" and
    expr'_grounding: "is_ground (expr' ⋅ γ⇩2)" and
    𝒱⇩1: "infinite_variables_per_type 𝒱⇩1" and
    finite_vars: "finite (vars expr')"
  obtains ρ⇩1 ρ⇩2 γ  where
    "base.is_renaming ρ⇩1"
    "base.is_renaming ρ⇩2"
    "vars (expr ⋅ ρ⇩1) ∩ vars (expr' ⋅ ρ⇩2) = {}"
    "base.type_preserving_on (vars expr) 𝒱⇩1 ρ⇩1"
    "base.type_preserving_on (vars expr') 𝒱⇩2 ρ⇩2"
    "∀x ∈ vars expr. x ⋅v γ⇩1 = x ⋅v ρ⇩1 ⊙ γ"
    "∀x ∈ vars expr'. x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
  using obtain_merged_grounding[OF typed_γ⇩2 typed_γ⇩1 expr'_grounding expr_grounding 𝒱⇩1 finite_vars]
  by (smt (verit, ccfv_threshold) inf_commute)

end

sublocale base_typed_renaming ⊆
  based_typed_renaming where base_vars = vars and base_subst = subst and base_welltyped = welltyped
  by unfold_locales

locale type_preserving_imgu = base_typed_substitution +
  assumes
    exists_type_preserving_imgu: 
    "⋀𝒱 υ expr expr'. type_preserving_unifier 𝒱 υ expr expr' ⟹
      ∃μ. type_preserving 𝒱 μ ∧ is_imgu μ {{expr, expr'}}"
begin

lemma obtain_type_preserving_imgu:
  fixes υ 
  assumes "type_preserving_unifier 𝒱 υ expr expr'"
  obtains μ
  where "type_preserving 𝒱 μ" "is_imgu μ {{expr, expr'}}"
  using exists_type_preserving_imgu[OF assms] UNIV_I
  by metis

lemma obtain_type_preserving_on_imgu:
  fixes υ 
  assumes "type_preserving_unifier 𝒱 υ expr expr'"
  obtains μ
  where "type_preserving_on X 𝒱 μ" "is_imgu μ {{expr, expr'}}"
  using exists_type_preserving_imgu[OF assms] UNIV_I
  by metis

end

end