Theory Abstract_Unification

```(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)
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"

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

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