Theory Unification_More

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2013-2015, 2017)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2014, 2015)
License: LGPL (see file COPYING.LESSER)
*)

section ‹A Concrete Unification Algorithm›

theory Unification_More
  imports
    First_Order_Terms.Unification
    Term_More
begin

lemma set_subst_list [simp]:
  "set (subst_list σ E) = subst_set σ (set E)"
  by (simp add: subst_list_def subst_set_def)

lemma finite_subst_domain_subst:
  "finite (subst_domain (subst x y))"
  by simp

lemma finite_subst_domain_subst_of:
  "finite (subst_domain (subst_of xs))"
proof (induct xs)
  case (Cons x xs)
  moreover have "finite (subst_domain (subst (fst x) (snd x)))" by (metis finite_subst_domain_subst)
  ultimately show ?case
    using subst_domain_compose [of "subst_of xs" "subst (fst x) (snd x)"]
    by (simp del: subst_subst_domain) (metis finite_subset infinite_Un)
qed simp

text ‹Computing the mgu of two terms.›
fun mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) subst option" where
  "mgu s t =
    (case unify [(s, t)] [] of   
      None ⇒ None
    | Some res ⇒ Some (subst_of res))"

text ‹Computing the mgu of two terms (to be used if it is guaranteed that
the terms are unifiable).›
definition the_mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f ,'v) subst" where
  "the_mgu s t = (case mgu s t of None ⇒ Var | Some δ ⇒ δ)"

lemma mgu_sound:
  assumes "mgu s t = Some σ"
  shows "is_imgu σ {(s, t)}"
proof -
  obtain ss where "unify [(s, t)] [] = Some ss"
    and "σ = subst_of ss"
    using assms by (auto split: option.splits)
  then have "is_imgu σ (set [(s, t)])" by (metis unify_sound)
  then show ?thesis by simp
qed

lemma mgu_complete:
  "mgu s t = None ⟹ unifiers {(s, t)} = {}"
proof -
  assume "mgu s t = None" 
  then have "unify [(s, t)] [] = None" by (cases "unify [(s, t)] []", auto)
  then have "unifiers (set [(s, t)]) = {}" by (rule unify_complete)
  then show ?thesis by simp
qed

lemma the_mgu_is_imgu:
  fixes σ :: "('f, 'v) subst"
  assumes "s ⋅ σ = t ⋅ σ"
  shows "is_imgu (the_mgu s t) {(s, t)}"
proof -
  from assms have "unifiers {(s, t)} ≠ {}" by (force simp: unifiers_def)
  then obtain τ where "mgu s t = Some τ"
    and "the_mgu s t = τ"
    using mgu_complete by (auto simp: the_mgu_def)
  with mgu_sound show ?thesis by blast
qed

lemma the_mgu:
  fixes σ :: "('f, 'v) subst"
  assumes "s ⋅ σ = t ⋅ σ"
  shows "s ⋅ the_mgu s t = t ⋅ the_mgu s t ∧ σ = the_mgu s t ∘⇩s σ" 
proof -
  have *: "σ ∈ unifiers {(s, t)}" by (force simp: assms unifiers_def)
  show ?thesis
  proof (cases "mgu s t")
    assume "mgu s t = None"
    then have "unifiers {(s, t)} = {}" by (rule mgu_complete)
    with * show ?thesis by simp
  next
    fix τ
    assume "mgu s t = Some τ"
    moreover then have "is_imgu τ {(s, t)}" by (rule mgu_sound)
    ultimately have "is_imgu (the_mgu s t) {(s, t)}" by (unfold the_mgu_def, simp)
    with * show ?thesis by (auto simp: is_imgu_def unifiers_def)
  qed
qed

(*FIXME: polish old part below*)
(* checking ∃ σ δ. s σ = t δ via mgu's and variable renamings *)
(* important note: given s and t :: ('f,'v)term, 
   of course, it would be convinient if one can just
   internally switch to pairs and then afterwards present mgu's μ1
   and μ2 for lhs and rhs of type ('f,'v)subst with result
   ∃τ1. σ = μ1 ∘⇩s τ1 and ∃τ2. δ = μ2 ∘⇩s τ2.
   However, this is not possible for arbitrary 'v: consider the
   example where UNIV :: 'v set = {x,y,z}, s = f(x,g(y,z)), t = f(g(y,z),x)
   a mgu μ1 for the lhs s obviously must replace x/g(_,_) y/_, z/_ where each _ 
   is a variable (because a solution is σ = τ = {x/g(y,z)}).
   However, there is also a solution σ = {x/g(a,b), y/c, z/d} and τ = {y/a,z/b,x/g(a,b)}
   then have, all four variables _ in the rhss of μ1 must be different.
   But since the universe consists only of three variables, this is not possible!

   Conclusion: to unify var disjoint one definitely requires a way to generate new variables,
      since the variables of the terms do not suffice to express the unifier of even one side.
   This can be done by enlarging the type (as done in the following) or by some fresh name generator.
*)
definition
  mgu_var_disjoint_generic ::
    "('v ⇒ 'u) ⇒ ('w ⇒ 'u) ⇒ ('f, 'v) term ⇒ ('f, 'w) term ⇒
      (('f, 'v, 'u) gsubst × ('f, 'w, 'u) gsubst) option"
where
  "mgu_var_disjoint_generic vu wu s t =
    (case mgu (map_vars_term vu s) (map_vars_term wu t) of
      None ⇒ None 
    | Some γ ⇒ Some (γ ∘ vu, γ ∘ wu))"

lemma mgu_var_disjoint_generic_sound: 
  assumes unif: "mgu_var_disjoint_generic vu wu s t = Some (γ1, γ2)"
  shows "s ⋅ γ1 = t ⋅ γ2"
proof -
  from unif[unfolded mgu_var_disjoint_generic_def] obtain γ where
    unif2: "mgu (map_vars_term vu s) (map_vars_term wu t) = Some γ"
    by (cases "mgu (map_vars_term vu s) (map_vars_term wu t)", auto)
  from mgu_sound[OF unif2[unfolded mgu_var_disjoint_generic_def], unfolded is_imgu_def unifiers_def]
  have "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" by auto
  from this[unfolded apply_subst_map_vars_term] unif[unfolded mgu_var_disjoint_generic_def unif2] 
  show ?thesis by simp
qed

(* if terms s and t can become identical via two substitutions σ and δ 
   then mgu_var_disjoint yields two more general substitutions μ1 μ2 *)
lemma mgu_var_disjoint_generic_complete:
  fixes σ :: "('f, 'v, 'u) gsubst" and τ :: "('f, 'w, 'u) gsubst" 
    and vu :: "'v ⇒ 'u" and wu:: "'w ⇒ 'u"
  assumes inj: "inj vu" "inj wu"
    and vwu: "range vu ∩ range wu = {}"
    and unif_disj: "s ⋅ σ = t ⋅ τ"
  shows "∃μ1 μ2 δ. mgu_var_disjoint_generic vu wu s t = Some (μ1, μ2) ∧ 
    σ = μ1 ∘⇩s δ ∧
    τ = μ2 ∘⇩s δ ∧
    s ⋅ μ1 = t ⋅ μ2"
proof -
  note inv1[simp] = the_inv_f_f[OF inj(1)]
  note inv2[simp] = the_inv_f_f[OF inj(2)]
  obtain γ :: "('f,'u)subst" where gamma: "γ = (λ x. if x ∈ range vu then σ (the_inv vu x) else τ (the_inv wu x))" by auto 
  have ids: "s ⋅ σ = map_vars_term vu s ⋅ γ" unfolding gamma
    by (induct s, auto)
  have idt: "t ⋅ τ = map_vars_term wu t ⋅ γ" unfolding gamma
    by (induct t, insert vwu, auto)
  from unif_disj ids idt
  have unif: "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" (is "?s ⋅ γ = ?t ⋅ γ") by auto
  from the_mgu[OF unif] have unif2: "?s ⋅ the_mgu ?s ?t = ?t ⋅ the_mgu ?s ?t" and inst: "γ = the_mgu ?s ?t ∘⇩s γ" by auto
  have "mgu ?s ?t = Some (the_mgu ?s ?t)" unfolding the_mgu_def
    using mgu_complete[unfolded unifiers_def] unif
    by (cases "mgu ?s ?t", auto)
  with inst obtain μ where mu: "mgu ?s ?t = Some μ" and gamma_mu: "γ = μ ∘⇩s γ" by auto
  let ?tau1 = "μ ∘ vu"
  let ?tau2 = "μ ∘ wu"
  show ?thesis unfolding mgu_var_disjoint_generic_def mu option.simps
  proof (intro exI conjI, rule refl)
    show "σ = ?tau1 ∘⇩s γ"
    proof (rule ext)
      fix x
      have "(?tau1 ∘⇩s γ) x = γ (vu x)" using fun_cong[OF gamma_mu, of "vu x"] by (simp add: subst_compose_def)
      also have "... = σ x" unfolding gamma by simp
      finally show "σ x = (?tau1 ∘⇩s γ) x" by simp
    qed
  next
    show "τ = ?tau2 ∘⇩s γ"
    proof (rule ext)
      fix x
      have "(?tau2 ∘⇩s γ) x = γ (wu x)" using fun_cong[OF gamma_mu, of "wu x"] by (simp add: subst_compose_def)
      also have "... = τ x" unfolding gamma using vwu by auto
      finally show "τ x = (?tau2 ∘⇩s γ) x" by simp
    qed
  next
    have "s ⋅ ?tau1 = map_vars_term vu s ⋅ μ" unfolding apply_subst_map_vars_term ..
    also have "... = map_vars_term wu t ⋅ μ"
      unfolding unif2[unfolded the_mgu_def mu option.simps] ..
    also have "... = t ⋅ ?tau2" unfolding apply_subst_map_vars_term ..
    finally show "s ⋅ ?tau1 = t ⋅ ?tau2" .
  qed
qed

abbreviation "mgu_var_disjoint_pair ≡ mgu_var_disjoint_generic Inl Inr"

lemma mgu_var_disjoint_pair_sound: 
  "mgu_var_disjoint_pair s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
  by (rule mgu_var_disjoint_generic_sound)

lemma mgu_var_disjoint_pair_complete:
  fixes σ :: "('f, 'v, 'v + 'w) gsubst" and τ :: "('f, 'w, 'v + 'w) gsubst"
  assumes unif_disj: "s ⋅ σ = t ⋅ τ"
  shows "∃μ1 μ2 δ. mgu_var_disjoint_pair s t = Some (μ1, μ2) ∧ 
    σ = μ1 ∘⇩s δ ∧
    τ = μ2 ∘⇩s δ ∧
    s ⋅ μ1 = t ⋅ μ2"
  by (rule mgu_var_disjoint_generic_complete[OF _ _ _ unif_disj], auto simp: inj_on_def)

lemma mgu_var_disjoint_pair_instance:
  fixes σ :: "('f, 'v) subst" and δ :: "('f, 'v) subst"
  assumes unif_disj: "s ⋅ σ = t ⋅ δ"
  shows "∃μ1 μ2 τ. mgu_var_disjoint_pair s t = Some (μ1, μ2) ∧
    σ = μ1 ∘⇩s τ ∧
    δ = μ2 ∘⇩s τ ∧ 
    s ⋅ μ1 = t ⋅ μ2"
proof -
  let ?m = "map_vars_subst_ran (Inl :: ('v ⇒ 'v + 'v))"
  let ?m' = "map_vars_subst_ran (case_sum (λ x. x) (λ x. x))"
  from unif_disj have id: "map_vars_term Inl (s ⋅ σ) = map_vars_term Inl (t ⋅ δ)" by simp
  from mgu_var_disjoint_pair_complete[OF id[unfolded map_vars_subst_ran]]
  obtain μ1 μ2 τ where mgu: "mgu_var_disjoint_pair s t = Some (μ1,μ2)"
    and σ: "?m σ = μ1 ∘⇩s τ" 
    and δ: "?m δ = μ2 ∘⇩s τ"
    and unif: "s ⋅ μ1 = t ⋅ μ2" by blast
  {
    fix σ :: "('f, 'v) subst"
    have "?m' (?m σ) = σ" by (simp add: map_vars_term_compose o_def term.map_ident)
  } note id = this
  {
    fix μ :: "('f,'v,'v+'v)gsubst" and τ :: "('f,'v + 'v)subst"
    have "?m' (μ ∘⇩s τ) = μ ∘⇩s ?m' τ"
      by (rule ext, unfold subst_compose_def, simp add: map_vars_subst_ran)
  } note id' = this
  from arg_cong[OF σ, of ?m', unfolded id id'] have σ: "σ = μ1 ∘⇩s ?m' τ" .
  from arg_cong[OF δ, of ?m', unfolded id id'] have δ: "δ = μ2 ∘⇩s ?m' τ" .
  show ?thesis
    by (intro exI conjI, rule mgu, rule σ, rule δ, rule unif)
qed

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'')"

abbreviation "mgu_var_disjoint_string ≡ mgu_var_disjoint_generic x_var y_var"

lemma mgu_var_disjoint_string_sound: 
  "mgu_var_disjoint_string s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
  by (rule mgu_var_disjoint_generic_sound)

lemma mgu_var_disjoint_string_complete:
  fixes σ :: "('f, string) subst" and τ :: "('f, string) subst" 
  assumes unif_disj: "s ⋅ σ = t ⋅ τ"
  shows "∃μ1 μ2 δ. mgu_var_disjoint_string s t = Some (μ1, μ2) ∧
    σ = μ1 ∘⇩s δ ∧
    τ = μ2 ∘⇩s δ ∧
    s ⋅ μ1 = t ⋅ μ2"
  by (rule mgu_var_disjoint_generic_complete[OF _ _ _ unif_disj], auto simp: inj_on_def)

lemma mgu_var_disjoint_right:
  fixes s t :: "('f, 'v) term" and σ τ :: "('f, 'v) subst" and T 
  assumes s: "vars_term s ⊆ S"
    and inj: "inj T"
    and ST: "S ∩ range T = {}"
    and id: "s ⋅ σ = t ⋅ τ"
  shows "∃ μ δ. mgu s (map_vars_term T t) = Some μ ∧
    s ⋅ σ = s ⋅ μ ⋅ δ ∧
    (∀t::('f, 'v) term. t ⋅ τ = map_vars_term T t ⋅ μ ⋅ δ) ∧
    (∀x∈S. σ x = μ x ⋅ δ)"
proof -
  let ?σ = "λ x. if x ∈ S then σ x else τ ((the_inv T) x)"
  let ?t = "map_vars_term T t"
  have ids: "s ⋅ σ = s ⋅ ?σ"
    by (rule term_subst_eq, insert s, auto)
  have "t ⋅ τ = map_vars_term (the_inv T) ?t ⋅ τ"
    unfolding map_vars_term_compose o_def using the_inv_f_f[OF inj] by (auto simp: term.map_ident)
  also have "... = ?t ⋅ (τ ∘ the_inv T)" unfolding apply_subst_map_vars_term ..
  also have "... = ?t ⋅ ?σ"
  proof (rule term_subst_eq)
    fix x
    assume "x ∈ vars_term ?t"
    then have "x ∈ T ` UNIV" unfolding term.set_map by auto
    then have "x ∉ S" using ST by auto
    then show "(τ ∘ the_inv T) x = ?σ x" by simp
  qed
  finally have idt: "t ⋅ τ = ?t ⋅ ?σ" by simp
  from id[unfolded ids idt] have id: "s ⋅ ?σ = ?t ⋅ ?σ" .
  with mgu_complete[of s ?t] id obtain μ where μ: "mgu s ?t = Some μ"
    unfolding unifiers_def  by (cases "mgu s ?t", auto)
  from the_mgu[OF id] have id: "s ⋅ μ = map_vars_term T t ⋅ μ" and σ: "?σ = μ ∘⇩s ?σ"
    unfolding the_mgu_def μ by auto
  have "s ⋅ σ = s ⋅ (μ ∘⇩s ?σ)" unfolding ids using σ by simp
  also have "... = s ⋅ μ ⋅ ?σ" by simp
  finally have ids: "s ⋅ σ = s ⋅ μ ⋅ ?σ" .
  {
    fix x
    have "τ x = ?σ (T x)" using ST unfolding the_inv_f_f[OF inj] by auto
    also have "... = (μ ∘⇩s ?σ) (T x)" using σ by simp
    also have "... = μ (T x) ⋅ ?σ" unfolding subst_compose_def by simp
    finally have "τ x = μ (T x) ⋅ ?σ" .
  } note τ = this
  {
    fix t :: "('f,'v)term"
    have "t ⋅ τ = t ⋅ (λ x. μ (T x) ⋅ ?σ)" unfolding τ[symmetric] ..
    also have "... = map_vars_term T t ⋅ μ ⋅ ?σ" unfolding apply_subst_map_vars_term 
      subst_subst by (rule term_subst_eq, simp add: subst_compose_def)
    finally have "t ⋅ τ = map_vars_term T t ⋅ μ ⋅ ?σ" .
  } note idt = this
  {
    fix x 
    assume "x ∈ S"
    then have "σ x = ?σ x" by simp
    also have "... = (μ ∘⇩s ?σ) x" using σ by simp
    also have "... = μ x ⋅ ?σ" unfolding subst_compose_def ..
    finally have "σ x = μ x ⋅ ?σ" .
  } note σ = this
  show ?thesis 
    by (rule exI[of _ μ], rule exI[of _ ?σ], insert μ ids idt σ, auto)
qed

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

lemma mgu_finite_subst_domain:
  "mgu s t = Some σ ⟹ finite (subst_domain σ)"
  by (cases "unify [(s, t)] []")
     (auto simp: finite_subst_domain_subst_of)

lemma mgu_subst_domain:
  assumes "mgu s t = Some σ"
  shows "subst_domain σ ⊆ vars_term s ∪ vars_term t"
proof -
  obtain xs where *: "unify [(s, t)] [] = Some xs" and [simp]: "subst_of xs = σ"
    using assms by (simp split: option.splits)
  from unify_Some_UNIF [OF *] obtain ss
    where "compose ss = σ" and "UNIF ss {#(s, t)#} {#}" by auto
  with UNIF_subst_domain_subset [of ss "{#(s, t)#}" "{#}"]
    show ?thesis using vars_mset_singleton by fastforce
qed

end