Theory Unification_String

subsection ‹A variable disjoint unification algorithm for terms with string variables›

theory Unification_String
imports
  Unification
  Renaming2_String
begin
definition "mgu_vd_string = mgu_vd string_rename" 

lemma mgu_vd_string_code[code]: "mgu_vd_string = mgu_var_disjoint_generic (Cons (CHR ''x'')) (Cons (CHR ''y''))" 
  unfolding mgu_vd_string_def mgu_vd_def
  by (transfer, auto)

lemma mgu_vd_string_sound: 
  "mgu_vd_string s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
  unfolding mgu_vd_string_def by (rule mgu_vd_sound)

lemma mgu_vd_string_complete:
  fixes σ :: "('f, string) subst" and τ :: "('f, string) subst" 
  assumes "s ⋅ σ = t ⋅ τ"
  shows "∃μ1 μ2 δ. mgu_vd_string s t = Some (μ1, μ2) ∧
    σ = μ1 ∘⇩s δ ∧
    τ = μ2 ∘⇩s δ ∧
    s ⋅ μ1 = t ⋅ μ2"
  unfolding mgu_vd_string_def
  by (rule mgu_vd_complete[OF assms])
end