Theory Substitution_First_Order_Term

theory Substitution_First_Order_Term
  imports
    Based_Substitution
    "First_Order_Terms.Unification"
    "Regular_Tree_Relations.Ground_Terms"
begin

section ‹Substitutions for first order terms›

subsection ‹Interpretations for first order terms› ✐‹contributor ‹Balazs Toth›› 

abbreviation (input) subst_updates where
  "subst_updates σ update x ≡ get_or (update x) (σ x)"

abbreviation (input) apply_subst where
  "apply_subst x σ ≡ σ x"

global_interpretation "term": base_substitution where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and vars = vars_term and
  subst_update = fun_upd and apply_subst = apply_subst
proof unfold_locales
  fix t :: "('f, 'v) term"  and σ τ :: "('f, 'v) subst"

  assume "⋀x. x ∈ vars_term t ⟹ σ x = τ x"

  then show "t ⋅ σ = t ⋅ τ"
    by (rule term_subst_eq)
next
  fix x :: 'v

  show "vars_term (Var x) = {x}"
    by simp
next
  fix σ σ' :: "('f, 'v) subst" and x

  show "(σ ∘⇩s σ') x = σ x ⋅ σ'"
    unfolding subst_compose_def ..
next
  fix t :: "('f, 'v) term" and ρ :: "('f, 'v) subst"

  show "vars_term (t ⋅ ρ) = ⋃ (vars_term ` ρ ` vars_term t)"
    using vars_term_subst .
next
  fix t :: "('f, 'v) term"

  assume "vars_term t = {}"

  then show "∀σ. t ⋅ σ = t"
    by (simp add: ground_term_subst)
qed auto

locale term_properties =
  base_substitution +
  all_subst_ident_iff_ground +
  exists_non_ident_subst +
  grounding +
  finite_variables +
  renaming_variables +
  base_exists_ground_subst

global_interpretation "term": term_properties where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and subst_update = fun_upd and
  subst_updates = subst_updates and apply_subst = apply_subst and vars = vars_term and
  to_ground = gterm_of_term and from_ground = term_of_gterm
proof unfold_locales
  fix t :: "('f, 'v) term"

  show "finite (vars_term t)"
    by simp
next
  fix t :: "('f, 'v) term"

  show "term.is_ground 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
next
  fix t :: "('f, 'v) term" and ts :: "('f, 'v) term set"

  assume "finite ts" "¬term.is_ground t"

  then show "∃σ. t ⋅ σ ≠ t ∧ t ⋅ σ ∉ ts"
  proof(induction t arbitrary: ts)
    case (Var x)

    obtain t' where t': "t' ∉ ts" "is_Fun t'"
      using Var.prems(1) finite_list by blast

    define σ :: "('f, 'v) subst" where "⋀x. σ x = t'"

    have "Var x ⋅ σ ≠ Var x"
      using t'
      unfolding σ_def
      by auto

    moreover have "Var x ⋅ σ ∉ ts"
      using t'
      unfolding σ_def
      by simp

    ultimately show ?case
      using Var
      by blast
  next
    case (Fun f args)

    obtain a where a: "a ∈ set args" and a_vars: "vars_term a ≠ {}"
      using Fun.prems
      by fastforce

    then obtain σ where
      σ: "a ⋅ σ ≠ a" and
      a_σ_not_in_args: "a ⋅ σ ∉ ⋃ (set `  term.args ` ts)"
      by (metis Fun.IH Fun.prems(1) List.finite_set finite_UN finite_imageI)

    then have "Fun f args ⋅ σ ≠ Fun f args"
       using a map_eq_conv
       by fastforce

    moreover have "Fun f args ⋅ σ ∉ ts"
      using a a_σ_not_in_args
      by auto

    ultimately show ?case
      using Fun
      by blast
  qed
next
   {
    fix t :: "('f, 'v) term"
    assume t_is_ground: "term.is_ground t"

    have "∃g. term_of_gterm g = t"
    proof(intro exI)

      from t_is_ground
      show "term_of_gterm (gterm_of_term t) = t"
        by (induction t) (simp_all add: map_idI)

    qed
  }

  then show "{t :: ('f, 'v) term. term.is_ground t} = range term_of_gterm"
    by fastforce
next
  fix t⇩G :: "'f gterm"

  show "gterm_of_term (term_of_gterm t⇩G) = t⇩G"
    by simp
next
  fix ρ :: "('f, 'v) subst" and t

  show is_renaming_iff: "term.is_renaming ρ ⟷ inj ρ ∧ (∀x. ∃x'. ρ x = Var x')"
  proof (rule iffI)

    show "term.is_renaming ρ ⟹ inj ρ ∧ (∀x. ∃x'. ρ x = Var x')"
      unfolding term.is_renaming_def
      unfolding subst_compose_def inj_def
      by (metis subst_apply_eq_Var term.inject(1))
  next

    show "inj ρ ∧ (∀x. ∃x'. ρ x = Var x') ⟹ term.is_renaming ρ"
      using ex_inverse_of_renaming
      unfolding term.is_renaming_def is_Var_def
      by metis
  qed

  assume ρ: "term.is_renaming ρ"

  show "vars_term (t ⋅ ρ) = term.rename ρ ` vars_term t"
  proof(induction t)
    case (Var x)
    have "ρ x = Var (term.rename ρ x)"
      using ρ
      unfolding term.rename_def[OF ρ] is_renaming_iff is_Var_def
      by (meson someI_ex)

    then show ?case
      by auto
  next
    case (Fun f ts)
    then show ?case
      by auto
  qed
next

  show "∃t. term.is_ground t"
    by (metis vars_term_of_gterm)
qed simp


subsection ‹Compatibility with First\_Order\_Term› ✐‹contributor ‹Balazs Toth›› 

text ‹Prefer @{thm [source] term.subst_id_subst} to @{thm [source] subst_apply_term_empty}.›
declare subst_apply_term_empty[no_atp]

lemma term_context_ground_iff_term_is_ground [simp]: "ground t = term.is_ground t"
  by (induction t) simp_all

text ‹The other direction does not hold!›
lemma Term_is_renaming_if_is_renaming:
  assumes "term.is_renaming ρ"
  shows "Term.is_renaming ρ"
  using assms
  by (simp add: inj_on_def is_renaming_def term.is_renaming_iff is_Var_def)

lemma Term_subst_domain_eq_subst_domain [simp]: "Term.subst_domain σ = term.subst_domain σ"
  by (simp add: subst_domain_def term.subst_domain_def)

lemma Term_range_vars_eq_range_vars [simp]: "Term.range_vars σ = term.range_vars σ"
  by (simp add: range_vars_def term.range_vars_def)

lemma Unifiers_unifiers_Times_iff_is_unifier:
  assumes "finite X"
  shows "μ ∈ Unifiers.unifiers (X × X) ⟷ term.is_unifier μ X "
  unfolding term.is_unifier_iff_if_finite[OF assms] unifiers_def
  by simp

lemma Unifiers_unifiers_Union_Times_iff_is_unifier_set:
  assumes "∀X∈ XX. finite X"
  shows "μ ∈ Unifiers.unifiers (⋃X∈XX. X × X) ⟷ term.is_unifier_set μ XX "
  using Unifiers_unifiers_Times_iff_is_unifier assms
  unfolding term.is_unifier_set_def unifiers_def
  by fast

lemma Unifiers_is_mgu_Union_Times_iff_is_mgu:
  assumes "∀X∈ XX. finite X"
  shows "Unifiers.is_mgu μ (⋃X∈XX. X × X) ⟷ term.is_mgu μ XX"
  unfolding term.is_mgu_def is_mgu_def 
  using Unifiers_unifiers_Union_Times_iff_is_unifier_set[OF assms]
  by (metis (lifting))

lemma Unifiers_is_imgu_Union_Times_iff_is_imgu:
  assumes "∀X∈ XX. finite X"
  shows "Unifiers.is_imgu μ (⋃X∈XX. X × X) ⟷ term.is_imgu μ XX"
  unfolding term.is_imgu_def is_imgu_def
  using Unifiers_unifiers_Union_Times_iff_is_unifier_set[OF assms]
  by auto

lemma Unifiers_is_mgu_iff_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.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.is_imgu μ (set_prod ` X)"
    unfolding term.is_imgu_def term.is_unifier_set_def term.is_unifier_def
    by (auto split: prod.splits)
next
  assume is_imgu: "term.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.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.is_imgu_def term.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.is_unifier_iff_if_finite)
  qed
qed


subsection ‹Interpretations for IMGUs› ✐‹contributor ‹Balazs Toth›› 

text ‹We could also use @{locale base_variables_in_base_imgu},
      but would then require infinite variables.›
global_interpretation "term": range_vars_subset_if_is_imgu where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and subst_update = fun_upd and
  apply_subst = apply_subst and vars = vars_term
proof unfold_locales
  fix μ :: "('f, 'v) subst" and XX

  assume imgu: "term.is_imgu μ XX" and finite: "∀X∈XX. finite X" "finite XX"

  then have is_imgu: "Unifiers.is_imgu μ (⋃X∈XX. X × X)"
    using Unifiers_is_imgu_Union_Times_iff_is_imgu[of "XX"]
    by simp

  have finite_prod: "finite (⋃X∈XX. X × X)"
    using finite
    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 "term.range_vars μ ⊆ ⋃ (vars_term ` ⋃ XX)"
    using imgu_range_vars_subset[OF is_imgu finite_prod]
    by simp
qed

global_interpretation "term": exists_imgu where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and subst_update = fun_upd and
  apply_subst = apply_subst and vars = vars_term
proof unfold_locales
  fix υ :: "('f, 'v) subst" and t t'
  assume unifier: "t ⋅ υ = t' ⋅ υ"

  show "∃μ. term.is_imgu μ {{t, t'}}"
  proof (rule exI)

    show "term.is_imgu (the_mgu t t') {{t, t'}}"
      using the_mgu_is_imgu unifier
      unfolding Unifiers_is_mgu_iff_is_imgu_image_set_prod
      by auto
  qed
qed


subsection ‹Additional lemmas›

lemma infinite_terms [intro]: "infinite (UNIV :: ('f, 'v) term set)" ✐‹contributor ‹Balazs Toth›› 
proof -
  have "infinite (UNIV :: ('f, 'v) term list set)"
    using infinite_UNIV_listI .

  then have "⋀f :: 'f. infinite ((Fun f) ` (UNIV :: ('f, 'v) term list set))"
    by (meson finite_imageD injI term.inject(2))

  then show "infinite (UNIV :: ('f, 'v) term set)"
    using infinite_super top_greatest 
    by blast
qed

lemma is_renaming_iff_ex_inj_fun_on_vars: "term.is_renaming ρ ⟷ (∃f. inj f ∧ ρ = Var ∘ f)"
proof (rule iffI)
  assume "term.is_renaming ρ"

  hence "inj ρ" and all_Var: "∀x. is_Var (ρ x)"
    unfolding term.is_renaming_iff is_Var_def
    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.is_renaming ρ"
    unfolding term.is_renaming_iff comp_apply inj_def
    by auto
qed

end