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) apply_subst where
  "apply_subst x σ ≡ σ x"

abbreviation (input) is_ground where
  "is_ground t ≡ vars_term t = {}"

global_interpretation "term": base_substitution where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and vars = vars_term and
  apply_subst = apply_subst and is_ground = is_ground
proof unfold_locales
  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)
next
  fix t and γ :: "('f, 'v) subst"
  assume "is_ground (t ⋅ γ)"

  then show "∀x∈vars_term t. is_ground (γ x)"
    by (meson ground_substD ground_vars_term_empty)
qed auto

lemma term_is_renaming_iff: "term.is_renaming ρ ⟷ inj ρ ∧ (∀x. ∃x'. ρ x = Var x')"
  unfolding term.is_renaming_def
  by (metis eval_subst_def ex_inverse_of_renaming injI is_Var_def subst_apply_eq_Var term.inject(1))

locale term_properties =
  base_substitution +
  all_subst_ident_iff_ground +
  exists_non_ident_subst +
  grounding +
  finite_variables +
  renaming_variables +
  exists_ground +
  create_renaming where
  base_vars = vars and base_subst = subst and base_is_ground = is_ground

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

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

  show "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" "¬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: "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. 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

  assume ρ: "term.is_renaming ρ"

  then show "inj ρ ∧ (∀x. ∃x'. ρ x = Var x')"
    unfolding term_is_renaming_iff .

  show "vars_term (t ⋅ ρ) = term.rename ρ ` vars_term t"
  proof (induction t)
    case (Var x)

    have "ρ x = Var (term.rename ρ x)"
      using ρ
      unfolding term_is_renaming_iff term.rename_def[OF ρ] 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. is_ground t"
    by (metis vars_term_of_gterm)
next
  fix x  update and t :: "('f, 'v) term" and σ :: "('f, 'v) subst"
  assume "x ∉ vars_term t"

  then show "t ⋅ σ(x := update) = t ⋅ σ"
    by (simp add: eval_with_fresh_var)
next
  fix γ :: "('f, 'v) subst" and t u :: "('f, 'v) term" and x
  assume "vars_term u = {}" "vars_term (t ⋅ γ) = {}" "x ∈ vars_term t" 
  
  then show "vars_term (t ⋅ γ(x := u)) = {}"
    by (metis fun_upd_apply ground_subst ground_vars_term_empty) 
qed auto

lemma exists_nonground_term [intro]: "∃t. vars_term t ≠ {}"
  using term.set_intros(3)
  by fastforce

lemmas term_id_subst_rename = term.id_subst_rename[OF exists_nonground_term]

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]

lemmas term_context_ground_iff_term_is_ground [simp] = ground_vars_term_empty

text ‹The other direction does not hold!›
lemma Term_is_renaming_if_is_renaming:
  assumes "term.is_renaming ρ"
  shows "Term.is_renaming ρ"
  using assms
  unfolding is_renaming_def term_is_renaming_iff
  by (metis inj_on_subset is_VarI top_greatest)

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: 
  "μ ∈ Unifiers.unifiers (X × X) ⟷ term.is_unifier μ X "
  unfolding term.is_unifier_iff unifiers_def
  by simp

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

lemma Unifiers_is_mgu_Union_Times_iff_is_mgu:
  "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
  by (metis (mono_tags, lifting))

lemma Unifiers_is_imgu_Union_Times_iff_is_imgu:
  "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
  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 fastforce
  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
  apply_subst = apply_subst and vars = vars_term and is_ground = is_ground
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
  apply_subst = apply_subst and vars = vars_term and is_ground = is_ground
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›

lemmas infinite_terms [intro] = term.infinite_exprs[OF exists_nonground_term]

lemma is_renaming_iff_ex_inj_fun_on_vars: "term.is_renaming ρ ⟷ (∃f. inj f ∧ ρ = Var ∘ f)"
  unfolding term_is_renaming_iff
  by (metis (no_types, lifting) ext comp_def inj_compose inj_on_Var inj_on_imageI2)

end