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_Times:
  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_Union_Times:
  assumes "∀X∈ XX. finite X"
  shows "term_subst.is_unifier_set μ XX ⟷ μ ∈ unifiers (⋃X∈XX. X × X)"
  using term_subst_is_unifier_iff_unifiers_Times assms
  unfolding term_subst.is_unifier_set_def unifiers_def
  by fast

lemma term_subst_is_mgu_iff_is_mgu_Union_Times:
  assumes fin: "∀X∈ XX. finite X"
  shows "term_subst.is_mgu μ XX ⟷ is_mgu μ (⋃X∈XX. X × X)"
  unfolding term_subst.is_mgu_def is_mgu_def
  unfolding term_subst_is_unifier_set_iff_unifiers_Union_Times[OF fin]
  by auto

lemma term_subst_is_imgu_iff_is_imgu_Union_Times:
  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_Union_Times[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_Union_Times[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 (smt (verit, ccfv_SIG) is_VarI subst_apply_eq_Var substitution_ops.is_renaming_def term.inject(1))
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 is_unifier_the_mgu: ✐‹contributor ‹Balazs Toth››
  assumes "t ⋅ the_mgu t t' = t' ⋅ the_mgu t t'"
  shows "term_subst.is_unifier (the_mgu t t') {t, t'}"
  using assms
  unfolding term_subst.is_unifier_def the_mgu_def
  by simp

lemma obtains_imgu_from_unifier_and_the_mgu: ✐‹contributor ‹Balazs Toth››
  fixes υ :: "('f, 'v) subst"
  assumes "t ⋅ υ = t' ⋅ υ" "P t t' (Unification.the_mgu t t')"
  obtains μ :: "('f, 'v) subst"
  where "υ = μ ∘⇩s υ" "term_subst.is_imgu μ {{t, t'}}" "P t t' μ"
proof
  have finite: "finite {t, t'}"
    by simp

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

  moreover have "⋀σ. term_subst.is_unifier_set σ {{t, t'}} ⟹ σ = the_mgu t t' ∘⇩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 t t') {{t, t'}}"
    unfolding term_subst.is_imgu_def
    by metis

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

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

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

lemma obtains_imgu: ✐‹contributor ‹Balazs Toth››
  fixes υ :: "('f, 'v) subst"
  assumes "t ⋅ υ = t' ⋅ υ"
  obtains μ :: "('f, 'v) subst"
  where "υ = μ ∘⇩s υ" "term_subst.is_imgu μ {{t, t'}}"
  using obtains_imgu_from_unifier_and_the_mgu[OF assms, of "(λ_ _ _. True)"]
  by auto

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

lemma is_mgu_iff_term_subst_is_imgu_image_set_prod: ✐‹contributor ‹Balazs Toth››
  fixes μ :: "('f, 'v) subst" and X :: "(('f, 'v) term × ('f, 'v) term) set"
  shows "Unifiers.is_imgu μ X ⟷ term_subst.is_imgu μ (set_prod ` X)"
proof (rule iffI)
  assume "is_imgu μ X"

  moreover then have
    "∀e∈X. fst e ⋅ μ = snd e ⋅ μ"
    "∀τ :: ('f, 'v) subst. (∀e∈X. fst e ⋅ τ = snd e ⋅ τ) ⟶ τ = μ ∘⇩s τ"
    unfolding is_imgu_def unifiers_def
    by auto

  moreover then have
    "⋀τ :: ('f, 'v) subst. ∀e∈X. ∀t t'. e = (t, t') ⟶ card {t ⋅ τ, t' ⋅ τ} ≤ Suc 0 ⟹ μ ∘⇩s τ = τ"
    by (metis Suc_n_not_le_n card_1_singleton_iff card_Suc_eq insert_iff prod.collapse)

  ultimately show "term_subst.is_imgu μ (set_prod ` X)"
    unfolding term_subst.is_imgu_def term_subst.is_unifier_set_def term_subst.is_unifier_def
    by (auto split: prod.splits)
next
  assume is_imgu: "term_subst.is_imgu μ (set_prod ` X)"

  show "is_imgu μ X"
  proof(unfold is_imgu_def unifiers_def, intro conjI ballI)

    show "μ ∈ {σ. ∀e∈X. fst e ⋅ σ = snd e ⋅ σ}"
      using term_subst.is_imgu_unifies[OF is_imgu]
      by fastforce
  next
    fix τ :: "('f, 'v) subst"
    assume "τ ∈ {σ. ∀e∈X. fst e ⋅ σ = snd e ⋅ σ}"

    then have "∀e∈X. fst e ⋅ τ = snd e ⋅ τ"
      by blast

    then show "τ = μ ∘⇩s τ"
      using is_imgu
      unfolding term_subst.is_imgu_def term_subst.is_unifier_set_def
      by (smt (verit, del_insts) case_prod_conv empty_iff finite.emptyI finite.insertI image_iff
          insert_iff prod.collapse term_subst.is_unifier_iff_if_finite)
  qed
qed

lemma the_mgu_term_subst_is_imgu: ✐‹contributor ‹Balazs Toth››
  fixes υ :: "('f, 'v) subst"
  assumes "s ⋅ υ = t ⋅ υ"
  shows "term_subst.is_imgu (Unification.the_mgu s t) {{s, t}}"
  using the_mgu_is_imgu[OF assms]
  unfolding is_mgu_iff_term_subst_is_imgu_image_set_prod
  by simp

end