Theory Abstract_Unification

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

section ‹Abstract Unification›

theory Abstract_Unification
imports
  Unifiers
  Term_Pair_Multiset
begin

subsection ‹Inference Rules›

text ‹Inference rules with explicit substitutions.›
inductive
  UNIF1 :: "('f, 'v) subst ⇒ ('f, 'v) equation multiset ⇒ ('f, 'v) equation multiset ⇒ bool"
where
  trivial: "UNIF1 Var (E + {#(t, t)#}) E" |
  decomp: "⟦length ss = length ts⟧ ⟹
    UNIF1 Var (E + {#(Fun f ss, Fun f ts)#}) (E + mset (zip ss ts))" |
  Var_left: "⟦x ∉ vars_term t⟧ ⟹
    UNIF1 (subst x t) (E + {#(Var x, t)#}) (subst_mset (subst x t) E)" |
  Var_right: "⟦x ∉ vars_term t⟧ ⟹
    UNIF1 (subst x t) (E + {#(t, Var x)#}) (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)

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)

definition vars_mset_less :: "(('f, 'v) equation multiset × ('f, 'v) equation multiset) set"
where
  "vars_mset_less = {(x, y). vars_mset x ⊂ vars_mset y}"

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 vars_mset_psubset_uniflessI [intro]:
  "vars_mset M ⊂ vars_mset N ⟹ (M, N) ∈ unifless"
  by (auto simp: unifless_def finite_vars_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 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
      by cases
      (auto intro!: Var_left_vars_mset_less Var_right_vars_mset_less intro: decomp_size_mset_less)
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 (op ∘⇩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 "op ∘⇩s" ss Var "foldr op ∘⇩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 UNIF_vars_mset_leq:
  assumes "UNIF ss E E'"
  shows "vars_mset E' ⊆ vars_mset E"
  using assms by (induct) (auto dest: UNIF1_vars_mset_leq)


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

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

lemma UNIF1_singleton_trivial [intro]:
  "UNIF1 Var {#(t, t)#} {#}"
  using UNIF1.trivial [of "{#}" t] by simp

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 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 unifiable_imp_empty_or_unif:
  assumes "unifiable (set_mset E)"
  shows "E = {#} ∨ (∃E'. (E, E') ∈ unif)"
proof (cases E)
  fix E' and e
  assume [simp]: "E = 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 unif_imp_converse_unifless [dest]:
  "(x, y) ∈ unif ⟹ (y, x) ∈ unifless"
  by (metis UNIF1_unifless unif_UNIF1_conv)


subsubsection ‹Completeness of the Inference Rules›

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

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

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 finite_compose:
  assumes "∀σ∈set ss. finite (subst_domain σ)"
  shows "finite (subst_domain (compose ss))"
  using assms by (induct ss) (auto simp: subst_domain_subst_compose)

lemma UNIF1_finite_subst_domain:
  assumes "UNIF1 σ E E'"
  shows "finite (subst_domain σ)"
  using assms by (cases) auto

lemma UNIF_finite_subst_domain:
  assumes "UNIF ss E E'"
  shows "∀σ∈set ss. finite (subst_domain σ)"
  using assms by (induct) (auto intro: UNIF1_finite_subst_domain)

text ‹The inference rules generate substitutions with finite domain.›
lemma UNIF_finite_subst_domain_compose:
  assumes "UNIF ss E E'"
  shows "finite (subst_domain (compose ss))"
  using UNIF_finite_subst_domain [OF assms] and finite_compose by blast

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

lemma UNIF_subst_domain_Int:
  assumes "UNIF ss E E'"
  shows "subst_domain (compose ss) ∩ vars_mset E' = {}"
  using assms
  by (induct)
     (auto dest!: UNIF1_subst_domain_Int UNIF_vars_mset_leq simp: subst_domain_subst_compose)

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 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 UNIF1_subst_domain_range_vars_Int:
  assumes "UNIF1 σ E E'"
  shows "subst_domain σ ∩ range_vars σ = {}"
  using assms by (cases) auto

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

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

end