Theory First_Order_Terms.Abstract_Unification

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

text ‹We formalize an inference system for unification.›

theory Abstract_Unification
  imports
    Unifiers
    Term_Pair_Multiset
    "Abstract-Rewriting.Abstract_Rewriting"
begin

(*TODO: move*)
lemma foldr_assoc:
  assumes "⋀f g h. b (b f g) h = b f (b g h)"
  shows "foldr b xs (b y z) = b (foldr b xs y) z"
  using assms by (induct xs) simp_all

(*TODO: move*)
lemma union_commutes:
  "M + {#x#} + N = M + N + {#x#}"
  "M + mset xs + N = M + N + mset xs"
  by (auto simp: ac_simps)


subsubsection ‹Inference Rules›

text ‹Inference rules with explicit substitutions.›
inductive
  UNIF1 :: "('f, 'v) subst ⇒ ('f, 'v) equation multiset ⇒ ('f, 'v) equation multiset ⇒ bool"
where
  trivial [simp]: "UNIF1 Var (add_mset (t, t) E) E" |
  decomp: "⟦length ss = length ts⟧ ⟹
    UNIF1 Var (add_mset (Fun f ss, Fun f ts) E) (E + mset (zip ss ts))" |
  Var_left: "⟦x ∉ vars_term t⟧ ⟹
    UNIF1 (subst x t) (add_mset (Var x, t) E) (subst_mset (subst x t) E)" |
  Var_right: "⟦x ∉ vars_term t⟧ ⟹
    UNIF1 (subst x t) (add_mset (t, Var x) E) (subst_mset (subst x t) E)"

text ‹Relation version of @{const UNIF1} with implicit substitutions.›
definition "unif = {(x, y). ∃σ. UNIF1 σ x y}"

lemma unif_UNIF1_conv:
  "(E, E') ∈ unif ⟷ (∃σ. UNIF1 σ E E')"
  by (auto simp: unif_def)

lemma UNIF1_unifD:
  "UNIF1 σ E E' ⟹ (E, E') ∈ unif"
  by (auto simp: unif_def)

text ‹A termination order for @{const UNIF1}.›
definition unifless :: "(('f, 'v) equation multiset × ('f, 'v) equation multiset) set" where
  "unifless = inv_image (finite_psubset <*lex*> measure size_mset) (λx. (vars_mset x, x))"

lemma wf_unifless:
  "wf unifless"
  by (auto simp: unifless_def)

lemma UNIF1_vars_mset_leq:
  assumes "UNIF1 σ E E'"
  shows "vars_mset E' ⊆ vars_mset E"
  using assms by (cases) (auto dest: mem_vars_mset_subst_mset)

lemma vars_mset_subset_size_mset_uniflessI [intro]:
  "vars_mset M ⊆ vars_mset N ⟹ size_mset M < size_mset N ⟹ (M, N) ∈ unifless"
  by (auto simp: unifless_def finite_vars_mset)

lemma vars_mset_psubset_uniflessI [intro]:
  "vars_mset M ⊂ vars_mset N ⟹ (M, N) ∈ unifless"
  by (auto simp: unifless_def finite_vars_mset)

lemma UNIF1_unifless:
  assumes "UNIF1 σ E E'"
  shows "(E', E) ∈ unifless"
proof -
  have "vars_mset E' ⊆ vars_mset E"
    using UNIF1_vars_mset_leq [OF assms] .
  with assms
  show ?thesis
    apply cases
       apply (auto simp: pair_size_def intro!: Var_left_vars_mset_less Var_right_vars_mset_less)
    apply (rule vars_mset_subset_size_mset_uniflessI)
     apply auto
    using size_mset_Fun_less by fastforce
qed

lemma converse_unif_subset_unifless:
  "unif¯ ⊆ unifless"
  using UNIF1_unifless by (auto simp: unif_def)


subsubsection ‹Termination of the Inference Rules›

lemma wf_converse_unif:
  "wf (unif¯)"
  by (rule wf_subset [OF wf_unifless converse_unif_subset_unifless])

text ‹Reflexive and transitive closure of @{const UNIF1} collecting substitutions
produced by single steps.›
inductive
  UNIF :: "('f, 'v) subst list ⇒ ('f, 'v) equation multiset ⇒ ('f, 'v) equation multiset ⇒ bool"
where
  empty [simp, intro!]: "UNIF [] E E" |
  step [intro]: "UNIF1 σ E E' ⟹ UNIF ss E' E'' ⟹ UNIF (σ # ss) E E''"

lemma unif_rtrancl_UNIF_conv:
  "(E, E') ∈ unif⇧* ⟷ (∃ss. UNIF ss E E')"
proof
  assume "(E, E') ∈ unif⇧*"
  then show "∃ss. UNIF ss E E'"
    by (induct rule: converse_rtrancl_induct) (auto simp: unif_UNIF1_conv)
next
  assume "∃ss. UNIF ss E E'"
  then obtain ss where "UNIF ss E E'" ..
  then show "(E, E') ∈ unif⇧*" by (induct) (auto dest: UNIF1_unifD)
qed

text ‹Compose a list of substitutions.›
definition compose :: "('f, 'v) subst list ⇒ ('f, 'v) subst"
  where
    "compose ss = List.foldr (∘⇩s) ss Var"

lemma compose_simps [simp]:
  "compose [] = Var"
  "compose (Var # ss) = compose ss"
  "compose (σ # ss) = σ ∘⇩s compose ss"
  by (simp_all add: compose_def)

lemma compose_append [simp]:
  "compose (ss @ ts) = compose ss ∘⇩s compose ts"
    using foldr_assoc [of "(∘⇩s)" ss Var "foldr (∘⇩s) ts Var"]
    by (simp add: compose_def ac_simps)

lemma set_mset_subst_mset [simp]:
  "set_mset (subst_mset σ E) = subst_set σ (set_mset E)"
  by (auto simp: subst_set_def subst_mset_def)

lemma UNIF1_subst_domain_Int:
  assumes "UNIF1 σ E E'"
  shows "subst_domain σ ∩ vars_mset E' = {}"
  using assms by (cases) simp+

lemma UNIF1_subst_domain_subset:
  assumes "UNIF1 σ E E'"
  shows "subst_domain σ ⊆ vars_mset E"
  using assms by (cases) simp+

lemma UNIF_subst_domain_subset:
  assumes "UNIF ss E E'"
  shows "subst_domain (compose ss) ⊆ vars_mset E"
  using assms
  by (induct)
     (auto dest: UNIF1_subst_domain_subset UNIF1_vars_mset_leq simp: subst_domain_subst_compose)

lemma UNIF1_range_vars_subset:
  assumes "UNIF1 σ E E'"
  shows "range_vars σ ⊆ vars_mset E"
  using assms by (cases) (auto simp: range_vars_def)

lemma UNIF1_subst_domain_range_vars_Int:
  assumes "UNIF1 σ E E'"
  shows "subst_domain σ ∩ range_vars σ = {}"
  using assms by (cases) auto

lemma UNIF_range_vars_subset:
  assumes "UNIF ss E E'"
  shows "range_vars (compose ss) ⊆ vars_mset E"
  using assms
  by (induct)
     (auto dest: UNIF1_range_vars_subset UNIF1_vars_mset_leq
           dest!: range_vars_subst_compose_subset [THEN subsetD])

lemma UNIF_subst_domain_range_vars_Int:
  assumes "UNIF ss E E'"
  shows "subst_domain (compose ss) ∩ range_vars (compose ss) = {}"
using assms
proof (induct)
  case (step σ E E' ss E'')
  from UNIF1_subst_domain_Int [OF step(1)]
    and UNIF_subst_domain_subset [OF step(2)]
    and UNIF1_subst_domain_range_vars_Int [OF step(1)]
    and UNIF_range_vars_subset [OF step(2)]
    have "subst_domain σ ∩ range_vars σ = {}"
      and "subst_domain (compose ss) ∩ subst_domain σ = {}"
      and "subst_domain σ ∩ range_vars (compose ss) = {}" by blast+
  then have "(subst_domain σ ∪ subst_domain (compose ss)) ∩
    ((range_vars σ - subst_domain (compose ss)) ∪ range_vars (compose ss)) = {}"
    using step(3) by auto
  then show ?case
    using subst_domain_subst_compose [of σ "compose ss"]
    and range_vars_subst_compose_subset [of σ "compose ss"]
    by (auto)
qed simp

text ‹The inference rules generate idempotent substitutions.›
lemma UNIF_idemp:
  assumes "UNIF ss E E'"
  shows "compose ss ∘⇩s compose ss = compose ss"
  using UNIF_subst_domain_range_vars_Int [OF assms]
    by (simp only: subst_idemp_iff)

lemma UNIF1_mono:
  assumes "UNIF1 σ E E'"
  shows "UNIF1 σ (E + M) (E' + subst_mset σ M)"
  using assms
  by (cases) (auto intro: UNIF1.intros simp: union_commutes subst_mset_union [symmetric])

lemma unif_mono:
  assumes "(E, E') ∈ unif"
  shows "∃σ. (E + M, E' + subst_mset σ M) ∈ unif"
  using assms by (auto simp: unif_UNIF1_conv intro: UNIF1_mono)

lemma unif_rtrancl_mono:
  assumes "(E, E') ∈ unif⇧*"
  shows "∃σ. (E + M, E' + subst_mset σ M) ∈ unif⇧*"
using assms
proof (induction arbitrary: M rule: converse_rtrancl_induct)
  case base
  have "(E' + M, E' + subst_mset Var M) ∈ unif⇧*" by auto
  then show ?case by blast
next
  case (step E F)
  obtain σ where "(E + M, F + subst_mset σ M) ∈ unif"
    using unif_mono [OF ‹(E, F) ∈ unif›] ..
  moreover obtain τ
    where "(F + subst_mset σ M, E' + subst_mset τ (subst_mset σ M)) ∈ unif⇧*"
    using step.IH by blast
  ultimately have "(E + M, E' + subst_mset (σ ∘⇩s τ) M) ∈ unif⇧*" by simp
  then show ?case by blast
qed


subsubsection ‹Soundness of the Inference Rules›

text ‹The inference rules of unification are sound in the sense that
  when the empty set of equations is reached, a most general unifier
  is obtained.›
lemma UNIF_empty_imp_is_mgu_compose:
  fixes E :: "('f, 'v) equation multiset"
  assumes "UNIF ss E {#}"
  shows "is_mgu (compose ss) (set_mset E)"
using assms
proof (induct ss E "{#}::('f, 'v) equation multiset")
  case (step σ E E' ss)
  then show ?case
    by (cases) (auto simp: is_mgu_subst_set_subst)
qed simp


subsubsection ‹Completeness of the Inference Rules›

lemma UNIF1_singleton_decomp [intro]:
  assumes "length ss = length ts"
  shows "UNIF1 Var {#(Fun f ss, Fun f ts)#} (mset (zip ss ts))"
  using UNIF1.decomp [OF assms, of f "{#}"] by simp

lemma UNIF1_singleton_Var_left [intro]:
  "x ∉ vars_term t ⟹ UNIF1 (subst x t) {#(Var x, t)#} {#}"
  using UNIF1.Var_left [of x t "{#}"] by simp

lemma UNIF1_singleton_Var_right [intro]:
  "x ∉ vars_term t ⟹ UNIF1 (subst x t) {#(t, Var x)#} {#}"
  using UNIF1.Var_right [of x t "{#}"] by simp

lemma not_UNIF1_singleton_Var_right [dest]:
  "¬ UNIF1 Var {#(Var x, Var y)#} {#} ⟹ x ≠ y"
  "¬ UNIF1 (subst x (Var y)) {#(Var x, Var y)#} {#} ⟹ x = y"
  by auto

lemma not_unifD:
  assumes "¬ (∃E'. ({#e#}, E') ∈ unif)"
  shows "(∃x t. (e = (Var x, t) ∨ e = (t, Var x)) ∧ x ∈ vars_term t ∧ is_Fun t) ∨
    (∃f g ss ts. e = (Fun f ss, Fun g ts) ∧ (f ≠ g ∨ length ss ≠ length ts))"
proof (rule ccontr)
  assume *: "¬ ?thesis"
  show False
  proof (cases e)
    case (Pair s t)
    with assms and * show ?thesis
      by (cases s) (cases t, auto simp: unif_def simp del: term.simps, (blast | succeed))+
  qed
qed

lemma unifiable_imp_unif:
  assumes "unifiable {e}"
  shows "∃E'. ({#e#}, E') ∈ unif"
proof (rule ccontr)
  assume "¬ ?thesis"
  from not_unifD [OF this] and assms
  show False by (auto simp: unifiable_def)
qed

lemma unifiable_imp_empty_or_unif:
  assumes "unifiable (set_mset E)"
  shows "E = {#} ∨ (∃E'. (E, E') ∈ unif)"
proof (cases E)
  case [simp]: (add e E')
  from assms have "unifiable {e}" by (auto simp: unifiable_def unifiers_insert)
  from unifiable_imp_unif [OF this]
    obtain E'' where "({#e#}, E'') ∈ unif" ..
  then obtain σ where "UNIF1 σ {#e#} E''" by (auto simp: unif_UNIF1_conv)
  from UNIF1_mono [OF this] have "UNIF1 σ E (E'' + subst_mset σ E')" by (auto simp: ac_simps)
  then show ?thesis by (auto simp: unif_UNIF1_conv)
qed simp

lemma UNIF1_preserves_unifiers:
  assumes "UNIF1 σ E E'" and "τ ∈ unifiers (set_mset E)"
  shows "(σ ∘⇩s τ) ∈ unifiers (set_mset E')"
  using assms by (cases) (auto simp: unifiers_def subst_mset_def)

lemma unif_preserves_unifiable:
  assumes "(E, E') ∈ unif" and "unifiable (set_mset E)"
  shows "unifiable (set_mset E')"
  using UNIF1_preserves_unifiers [of _ E E'] and assms
  by (auto simp: unif_UNIF1_conv unifiable_def)

lemma unif_imp_converse_unifless [dest]:
  "(x, y) ∈ unif ⟹ (y, x) ∈ unifless"
  by (metis UNIF1_unifless unif_UNIF1_conv)

text ‹Every unifiable set of equations can be reduced to the empty
  set by applying the inference rules of unification.›

lemma unifiable_imp_empty:
  assumes "unifiable (set_mset E)"
  shows "(E, {#}) ∈ unif⇧*"
  using assms
proof (induct E rule: wf_induct [OF wf_unifless])
  fix E :: "('f, 'v) equation multiset"
  presume IH: "⋀E'. ⟦(E', E) ∈ unifless; unifiable (set_mset E')⟧ ⟹
    (E', {#}) ∈ unif⇧*"
    and *: "unifiable (set_mset E)"
  show "(E, {#}) ∈ unif⇧*"
  proof (cases "E = {#}")
    assume "E ≠ {#}"
    with unifiable_imp_empty_or_unif [OF *]
    obtain E' where "(E, E') ∈ unif" by auto
    with * have "(E', E) ∈ unifless" and "unifiable (set_mset E')"
      by (auto dest: unif_preserves_unifiable)
    from IH [OF this] and ‹(E, E') ∈ unif›
    show ?thesis by simp
  qed simp
qed simp

lemma unif_rtrancl_empty_imp_unifiable:
  assumes "(E, {#}) ∈ unif⇧*"
  shows "unifiable (set_mset E)"
  using assms
  by (auto simp: unif_rtrancl_UNIF_conv unifiable_def is_mgu_def
           dest!: UNIF_empty_imp_is_mgu_compose)

lemma not_unifiable_imp_not_empty_NF:
  assumes "¬ unifiable (set_mset E)"
  shows "∃E'. E' ≠ {#} ∧ (E, E') ∈ unif⇧!"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have *: "⋀E'. (E, E') ∈ unif⇧! ⟹ E' = {#}" by auto
  have "SN unif" using wf_converse_unif by (auto simp: SN_iff_wf)
  then obtain E' where "(E, E') ∈ unif⇧!"
    by (metis SN_imp_WN UNIV_I WN_onE)
  with * have "(E, {#}) ∈ unif⇧*" by auto
  from unif_rtrancl_empty_imp_unifiable [OF this] and assms
  show False by contradiction
qed

lemma unif_rtrancl_preserves_unifiable:
  assumes "(E, E') ∈ unif⇧*" and "unifiable (set_mset E)"
  shows "unifiable (set_mset E')"
  using assms by (induct) (auto simp: unif_preserves_unifiable)

text ‹The inference rules for unification are complete in the
  sense that whenever it is not possible to reduce a set of equations
  @{term E} to the empty set, then @{term E} is not unifiable.›

lemma empty_not_reachable_imp_not_unifiable:
  assumes "(E, {#}) ∉ unif⇧*"
  shows "¬ unifiable (set_mset E)"
  using unifiable_imp_empty [of E] and assms by blast

text ‹It is enough to reach an irreducible set of equations
  to conclude non-unifiability.›
lemma irreducible_reachable_imp_not_unifiable:
  assumes "(E, E') ∈ unif⇧!" and "E' ≠ {#}"
  shows "¬ unifiable (set_mset E)"
proof -
  have "(E, E') ∈ unif⇧*" and "(E', {#}) ∉ unif⇧*"
    using assms by (auto simp: NF_not_suc)
  moreover with empty_not_reachable_imp_not_unifiable
    have "¬ unifiable (set_mset E')" by fast
  ultimately show ?thesis
    using unif_rtrancl_preserves_unifiable by fast
qed

end