Theory Abstract_Substitution.Substitution_First_Order_Term

theory Substitution_First_Order_Term
  imports
    Substitution
    "First_Order_Terms.Unification"
begin

abbreviation is_ground_trm where
  "is_ground_trm t ≡ vars_term t = {}"

lemma is_ground_iff: "is_ground_trm (t ⋅ γ) ⟷ (∀x ∈ vars_term t. is_ground_trm (γ x))"
  by (induction t) simp_all

lemma is_ground_trm_iff_ident_forall_subst: "is_ground_trm t ⟷ (∀σ. t ⋅ σ = t)"
proof(induction t)
  case Var
  then show ?case 
    by auto
next
  case Fun

  moreover have "⋀xs x σ. ∀σ. map (λs. s ⋅ σ) xs = xs ⟹ x ∈ set xs ⟹ x ⋅ σ = x"
    by (metis list.map_ident map_eq_conv)

  ultimately show ?case
    by (auto simp: map_idI)
qed

global_interpretation term_subst: substitution where
  subst = subst_apply_term and id_subst = Var and comp_subst = subst_compose and
  is_ground = is_ground_trm
proof unfold_locales
  show "⋀x. x ⋅ Var = x"
    by simp
next
  show "⋀x σ τ. x ⋅ σ ∘⇩s τ = x ⋅ σ ⋅ τ"
    by simp
next
  show "⋀x. is_ground_trm x ⟹ ∀σ. x ⋅ σ = x"
    using is_ground_trm_iff_ident_forall_subst ..
qed
                      
lemma term_subst_is_unifier_iff_unifiers:
  assumes "finite X"
  shows "term_subst.is_unifier μ X ⟷ μ ∈ unifiers (X × X)"
  unfolding term_subst.is_unifier_iff_if_finite[OF assms] unifiers_def
  by simp

lemma term_subst_is_unifier_set_iff_unifiers:
  assumes "∀X∈ XX. finite X"
  shows "term_subst.is_unifier_set μ XX ⟷ μ ∈ unifiers (⋃X∈XX. X × X)"
  using term_subst_is_unifier_iff_unifiers assms 
  unfolding term_subst.is_unifier_set_def unifiers_def 
  by fast

lemma term_subst_is_imgu_iff_is_imgu:
  assumes "∀X∈ XX. finite X"
  shows "term_subst.is_imgu μ XX ⟷ is_imgu μ (⋃X∈XX. X × X)"
  using term_subst_is_unifier_set_iff_unifiers[OF assms]
  unfolding term_subst.is_imgu_def is_imgu_def
  by auto

lemma range_vars_subset_if_is_imgu:
  assumes "term_subst.is_imgu μ XX" "∀X∈XX. finite X" "finite XX"
  shows "range_vars μ ⊆ (⋃t∈⋃XX. vars_term t)"
proof-
  have is_imgu: "is_imgu μ (⋃X∈XX. X × X)"
    using term_subst_is_imgu_iff_is_imgu[of "XX"] assms
    by simp

  have finite_prod: "finite (⋃X∈XX. X × X)"
    using assms
    by blast

  have "(⋃e∈⋃X∈XX. X × X. vars_term (fst e) ∪ vars_term (snd e)) = (⋃t∈⋃XX. vars_term t)"
    by fastforce

  then show ?thesis
    using imgu_range_vars_subset[OF is_imgu finite_prod]
    by argo
qed

lemma term_subst_is_renaming_iff:
  "term_subst.is_renaming ρ ⟷ inj ρ ∧ (∀x. is_Var (ρ x))"
proof (rule iffI)
  show "term_subst.is_renaming ρ ⟹ inj ρ ∧ (∀x. is_Var (ρ x))"
    unfolding term_subst.is_renaming_def subst_compose_def inj_def
    by (metis term.sel(1) is_VarI subst_apply_eq_Var) 
next
  show "inj ρ ∧ (∀x. is_Var (ρ x)) ⟹ term_subst.is_renaming ρ"
    unfolding term_subst.is_renaming_def
    using ex_inverse_of_renaming by metis
qed

lemma term_subst_is_renaming_iff_ex_inj_fun_on_vars:
  "term_subst.is_renaming ρ ⟷ (∃f. inj f ∧ ρ = Var ∘ f)"
proof (rule iffI)
  assume "term_subst.is_renaming ρ"
  hence "inj ρ" and all_Var: "∀x. is_Var (ρ x)"
    unfolding term_subst_is_renaming_iff by simp_all
  from all_Var obtain f where "∀x. ρ x = Var (f x)"
    by (metis comp_apply term.collapse(1))
  hence "ρ = Var ∘ f"
    using ‹∀x. ρ x = Var (f x)›
    by (intro ext) simp
  moreover have "inj f"
      using ‹inj ρ› unfolding ‹ρ = Var ∘ f›
      using inj_on_imageI2 by metis
  ultimately show "∃f. inj f ∧ ρ = Var ∘ f"
    by metis
next
  show "∃f. inj f ∧ ρ = Var ∘ f ⟹ term_subst.is_renaming ρ"
    unfolding term_subst_is_renaming_iff comp_apply inj_def
    by auto
qed

lemma ground_imgu_equals: 
  assumes "is_ground_trm t⇩1" and "is_ground_trm t⇩2" and "term_subst.is_imgu μ {{t⇩1, t⇩2}}"
  shows "t⇩1 = t⇩2"
  using assms
  using term_subst.ground_eq_ground_if_unifiable
  by (metis insertCI term_subst.is_imgu_def term_subst.is_unifier_set_def)

lemma the_mgu_is_unifier: 
  assumes "term ⋅ the_mgu term term' = term' ⋅ the_mgu term term'" 
  shows "term_subst.is_unifier (the_mgu term term') {term, term'}"
  using assms
  unfolding term_subst.is_unifier_def the_mgu_def
  by simp

lemma imgu_exists_extendable:
  fixes υ :: "('f, 'v) subst"
  assumes "term ⋅ υ = term' ⋅ υ" "P term term' (the_mgu term term')"
  obtains μ :: "('f, 'v) subst"
  where "υ = μ ∘⇩s υ" "term_subst.is_imgu μ {{term, term'}}" "P term term' μ"
proof
  have finite: "finite {term, term'}"
    by simp

  have "term_subst.is_unifier_set (the_mgu term term') {{term, term'}}"
    unfolding term_subst.is_unifier_set_def
    using the_mgu_is_unifier[OF the_mgu[OF assms(1), THEN conjunct1]]
    by simp

  moreover have
    "⋀σ. term_subst.is_unifier_set σ {{term, term'}} ⟹ σ = the_mgu term term' ∘⇩s σ"
    unfolding term_subst.is_unifier_set_def
    using term_subst.is_unifier_iff_if_finite[OF finite] the_mgu
    by blast

  ultimately have is_imgu: "term_subst.is_imgu (the_mgu term term') {{term, term'}}"
    unfolding term_subst.is_imgu_def
    by metis

  show "υ = (the_mgu term term') ∘⇩s υ" 
    using the_mgu[OF assms(1)]
    by blast

  show "term_subst.is_imgu (the_mgu term term') {{term, term'}}"
    using is_imgu
    by blast

  show "P term term' (the_mgu term term')"
    using assms(2).
qed

lemma imgu_exists:
  fixes υ :: "('f, 'v) subst"
  assumes "term ⋅ υ = term' ⋅ υ"
  obtains μ :: "('f, 'v) subst"
  where "υ = μ ∘⇩s υ" "term_subst.is_imgu μ {{term, term'}}"
  using imgu_exists_extendable[OF assms, of "(λ_ _ _. True)"]
  by auto

(* The other way around it does not work! *)
lemma is_renaming_if_term_subst_is_renaming:
  assumes "term_subst.is_renaming ρ"
  shows "is_renaming ρ"
  using assms
  by (simp add: inj_on_def is_renaming_def term_subst_is_renaming_iff)

end