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])

abbreviation (input) x_var :: "string  string" where "x_var  Cons (CHR ''x'')"
abbreviation (input) y_var :: "string  string" where "y_var  Cons (CHR ''y'')"
abbreviation (input) z_var :: "string  string" where "z_var  Cons (CHR ''z'')"

text ‹Here, only the t-term is renamed.›
lemma mgu_var_disjoint_right_string:
  fixes s t :: "('f, string) term" and σ τ :: "('f, string) subst"
  assumes s: "vars_term s  range x_var  range z_var"
    and id: "s  σ = t  τ"
  shows " μ δ. mgu s (map_vars_term y_var t) = Some μ 
    s  σ = s  μ  δ  (t::('f, string) term. t  τ = map_vars_term y_var t  μ  δ) 
    (x  range x_var  range z_var. σ x = μ x  δ)"
proof -
  have inj: "inj y_var" unfolding inj_on_def by simp
  show ?thesis
    by (rule mgu_var_disjoint_right[OF s inj _ id], auto)
qed

end