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