Theory Unifiers

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
section ‹Unification›

subsection ‹Unifiers›

text ‹Definition and properties of (most general) unifiers›

theory Unifiers
  imports Term
begin

(*TODO: move*)
lemma map_eq_set_zipD [dest]:
  assumes "map f xs = map f ys"
    and "(x, y)  set (zip xs ys)"
  shows "f x = f y"
using assms
proof (induct xs arbitrary: ys)
  case (Cons x xs)
  then show ?case by (cases ys) auto
qed simp

type_synonym ('f, 'v) equation = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) equations = "('f, 'v) equation set"

text ‹The set of unifiers for a given set of equations.›
definition unifiers :: "('f, 'v) equations  ('f, 'v) subst set"
  where
    "unifiers E = {σ. pE. fst p  σ = snd p  σ}"

text ‹Check whether a set of equations is unifiable.›
definition "unifiable E  (σ. σ  unifiers E)"

lemma in_unifiersE [elim]:
  "σ  unifiers E; (e. e  E  fst e  σ = snd e  σ)  P  P"
  by (force simp: unifiers_def)

text ‹Applying a substitution to a set of equations.›
definition subst_set :: "('f, 'v) subst  ('f, 'v) equations  ('f, 'v) equations"
  where
    "subst_set σ E = (λe. (fst e  σ, snd e  σ)) ` E"

text ‹Check whether a substitution is a most-general unifier (mgu) of a set of equations.›
definition is_mgu :: "('f, 'v) subst  ('f, 'v) equations  bool"
  where
    "is_mgu σ E  σ  unifiers E  (τ  unifiers E. (γ. τ = σ s γ))"

text ‹The following property characterizes idempotent mgus, that is,
  mgus termσ for which propσ s σ = σ holds.›
definition is_imgu :: "('f, 'v) subst  ('f, 'v) equations  bool"
  where
    "is_imgu σ E  σ  unifiers E  (τ  unifiers E. τ = σ s τ)"


subsubsection ‹Properties of sets of unifiers›

lemma unifiers_Un [simp]:
  "unifiers (s  t) = unifiers s  unifiers t"
  by (auto simp: unifiers_def)

lemma unifiers_empty [simp]:
  "unifiers {} = UNIV"
  by (auto simp: unifiers_def)

lemma unifiers_insert: (* "simp not added for readability (and termination)" *)
  "unifiers (insert p t) = {σ. fst p  σ = snd p  σ}  unifiers t"
  by (auto simp: unifiers_def)

lemma unifiers_insert_ident [simp]:
  "unifiers (insert (t, t) E) = unifiers E" 
  by (auto simp: unifiers_insert)

lemma unifiers_insert_swap:
  "unifiers (insert (s, t) E) = unifiers (insert (t, s) E)"
  by (auto simp: unifiers_insert)

lemma unifiers_insert_Var_swap [simp]:
  "unifiers (insert (t, Var x) E) = unifiers (insert (Var x, t) E)"
  by (rule unifiers_insert_swap)

lemma unifiers_subst_set [simp]:
  "τ  unifiers (subst_set σ E)  σ s τ  unifiers E"
  by (auto simp: unifiers_def subst_set_def)

lemma unifiers_insert_VarD:
  shows "σ  unifiers (insert (Var x, t) E)  subst x t s σ = σ"
    and "σ  unifiers (insert (t, Var x) E)  subst x t s σ = σ"
  by (auto simp: unifiers_def)

lemma unifiers_insert_Var_left:
  "σ  unifiers (insert (Var x, t) E)  σ  unifiers (subst_set (subst x t) E)"
  by (auto simp: unifiers_def subst_set_def)

lemma unifiers_set_zip [simp]:
  assumes "length ss = length ts"
  shows "unifiers (set (zip ss ts)) = {σ. map (λt. t  σ) ss = map (λt. t  σ) ts}"
  using assms by (induct ss ts rule: list_induct2) (auto simp: unifiers_def)

lemma unifiers_Fun [simp]:
  "σ  unifiers {(Fun f ss, Fun g ts)} 
    length ss = length ts  f = g  σ  unifiers (set (zip ss ts))"
  by (auto simp: unifiers_def dest: map_eq_imp_length_eq)
    (induct ss ts rule: list_induct2, simp_all)

lemma unifiers_occur_left_is_Fun:
  fixes t :: "('f, 'v) term"
  assumes "x  vars_term t" and "is_Fun t"
  shows "unifiers (insert (Var x, t) E) = {}"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain σ :: "('f, 'v) subst" where "σ x = t  σ" by (auto simp: unifiers_def)
  with is_Fun_num_funs_less [OF assms, of σ] show False by auto
qed

lemma unifiers_occur_left_not_Var:
  "x  vars_term t  t  Var x  unifiers (insert (Var x, t) E) = {}"
  using unifiers_occur_left_is_Fun [of x t] by (cases t) simp_all

lemma unifiers_occur_left_Fun:
  "x  (tset ts. vars_term t)  unifiers (insert (Var x, Fun f ts) E) = {}"
  using unifiers_occur_left_is_Fun [of x "Fun f ts"] by simp

lemmas unifiers_occur_left_simps [simp] =
  unifiers_occur_left_is_Fun
  unifiers_occur_left_not_Var
  unifiers_occur_left_Fun


subsubsection ‹Properties of unifiability›

lemma in_vars_is_Fun_not_unifiable:
  assumes "x  vars_term t" and "is_Fun t"
  shows "¬ unifiable {(Var x, t)}"
proof
  assume "unifiable {(Var x, t)}"
  then obtain σ where "σ  unifiers {(Var x, t)}"
    by (auto simp: unifiable_def)
  then have "σ x = t  σ" by (auto)
  moreover have "num_funs (σ x) < num_funs (t  σ)"
    using is_Fun_num_funs_less [OF assms] by auto
  ultimately show False by auto
qed

lemma unifiable_insert_swap:
  "unifiable (insert (s, t) E) = unifiable (insert (t, s) E)"
  by (auto simp: unifiable_def unifiers_insert_swap)

lemma subst_set_reflects_unifiable:
  fixes σ :: "('f, 'v) subst"
  assumes "unifiable (subst_set σ E)"
  shows "unifiable E"
proof -
  { fix τ :: "('f, 'v) subst" assume "pE. fst p  σ  τ = snd p  σ  τ"
    then have "σ :: ('f, 'v) subst. pE. fst p  σ = snd p  σ"
      by (intro exI [of _ "σ s τ"]) auto }
  then show ?thesis using assms by (auto simp: unifiable_def unifiers_def subst_set_def)
qed


subsubsection ‹Properties of termis_mgu

lemma is_mgu_empty [simp]:
  "is_mgu Var {}"
  by (auto simp: is_mgu_def)

lemma is_mgu_insert_trivial [simp]:
  "is_mgu σ (insert (t, t) E) = is_mgu σ E"
  by (auto simp: is_mgu_def)

lemma is_mgu_insert_decomp [simp]:
  assumes "length ss = length ts"
  shows "is_mgu σ (insert (Fun f ss, Fun f ts) E) 
    is_mgu σ (E  set (zip ss ts))"
  using assms by (auto simp: is_mgu_def unifiers_insert)

lemma is_mgu_insert_swap:
  "is_mgu σ (insert (s, t) E) = is_mgu σ (insert (t, s) E)"
  by (auto simp: is_mgu_def unifiers_def)

lemma is_mgu_insert_Var_swap [simp]:
  "is_mgu σ (insert (t, Var x) E) = is_mgu σ (insert (Var x, t) E)"
  by (rule is_mgu_insert_swap)

lemma is_mgu_subst_set_subst:
  assumes "x  vars_term t"
    and "is_mgu σ (subst_set (subst x t) E)" (is "is_mgu σ ?E")
  shows "is_mgu (subst x t s σ) (insert (Var x, t) E)" (is "is_mgu  ?E'")
proof -
  from is_mgu σ ?E
    have "  unifiers E"
    and *: "τ. (subst x t s τ)  unifiers E  (μ. τ = σ s μ)"
    by (auto simp: is_mgu_def)
  then have "  unifiers ?E'" using assms by (simp add: unifiers_insert subst_compose)
  moreover have "τ. τ  unifiers ?E'  (μ. τ =  s μ)"
  proof (intro allI impI)
    fix τ
    assume **: "τ  unifiers ?E'"
    then have [simp]: "subst x t s τ = τ" by (blast dest: unifiers_insert_VarD)
    from unifiers_insert_Var_left [OF **]
      have "subst x t s τ  unifiers E" by (simp)
    with * obtain μ where "τ = σ s μ" by blast
    then have "subst x t s τ = subst x t s σ s μ" by (auto simp: ac_simps)
    then show "μ. τ = subst x t s σ s μ" by auto
  qed
  ultimately show "is_mgu  ?E'" by (simp add: is_mgu_def)
qed

lemma is_imgu_imp_is_mgu:
  assumes "is_imgu σ E"
  shows "is_mgu σ E"
  using assms by (auto simp: is_imgu_def is_mgu_def)


subsubsection ‹Properties of termis_imgu

lemma rename_subst_domain_range_preserves_is_imgu: contributor ‹Martin Desharnais›
  fixes E :: "('f, 'v) equations" and μ ρ :: "('f, 'v) subst"
  assumes imgu_μ: "is_imgu μ E" and is_var_ρ: "x. is_Var (ρ x)" and "inj ρ"
  shows "is_imgu (rename_subst_domain_range ρ μ) (subst_set ρ E)"
proof (unfold is_imgu_def, intro conjI ballI)
  from imgu_μ have unif_μ: "μ  unifiers E"
    by (simp add: is_imgu_def)

  show "rename_subst_domain_range ρ μ  unifiers (subst_set ρ E)"
    unfolding unifiers_subst_set unifiers_def mem_Collect_eq
  proof (rule ballI)
    fix eρ assume "eρ  subst_set ρ E"
    then obtain e where "e  E" and "eρ = (fst e  ρ, snd e  ρ)"
      by (auto simp: subst_set_def)
    then show "fst eρ  rename_subst_domain_range ρ μ = snd eρ  rename_subst_domain_range ρ μ"
      using unif_μ subst_apply_term_renaming_rename_subst_domain_range[OF is_var_ρ inj ρ, of _ μ]
      by (simp add: unifiers_def)
  qed
next
  fix υ :: "('f, 'v) subst"
  assume "υ  unifiers (subst_set ρ E)"
  hence "(ρ s υ)  unifiers E"
    by (simp add: subst_set_def unifiers_def)
  with imgu_μ have μ_ρ_υ: "μ s ρ s υ = ρ s υ"
    by (simp add: is_imgu_def subst_compose_assoc)

  show "υ = rename_subst_domain_range ρ μ s υ"
  proof (rule ext)
    fix x
    show "υ x = (rename_subst_domain_range ρ μ s υ) x"
    proof (cases "Var x  ρ ` subst_domain μ")
      case True
      hence "(rename_subst_domain_range ρ μ s υ) x = (μ s ρ s υ) (the_inv ρ (Var x))"
        by (simp add: rename_subst_domain_range_def subst_compose_def)
      also have " = (ρ s υ) (the_inv ρ (Var x))"
        by (simp add: μ_ρ_υ)
      also have " = (ρ (the_inv ρ (Var x)))  υ"
        by (simp add: subst_compose)
      also have " = Var x  υ"
        using True f_the_inv_into_f[OF inj ρ, of "Var x"] by force
      finally show ?thesis
        by simp
    next
      case False
      thus ?thesis
        by (simp add: rename_subst_domain_range_def subst_compose)
    qed
  qed
qed

corollary rename_subst_domain_range_preserves_is_imgu_singleton: contributor ‹Martin Desharnais›
  fixes t u :: "('f, 'v) term" and μ ρ :: "('f, 'v) subst"
  assumes imgu_μ: "is_imgu μ {(t, u)}" and is_var_ρ: "x. is_Var (ρ x)" and "inj ρ"
  shows "is_imgu (rename_subst_domain_range ρ μ) {(t  ρ, u  ρ)}"
  by (rule rename_subst_domain_range_preserves_is_imgu[OF imgu_μ is_var_ρ inj ρ,
        unfolded subst_set_def, simplified])

end