Theory TRS.Mgu_generic
theory Mgu_generic
imports
First_Order_Terms.Unification_More
Auxx.RenamingN
begin
definition
mgu_var_disjoint_list_generic ::
"(nat ⇒ 'v ⇒ 'v) ⇒ ('v ⇒ 'v) ⇒ (('f, 'v) term × ('f, 'v) term)list ⇒
(('f,'v)subst list × ('f, 'v) subst) option"
where
"mgu_var_disjoint_list_generic rename_many' ren_l sls = (
let pairs = map (λ (i, (si, li)). (map_vars_term (rename_many' i) si, map_vars_term ren_l li)) (zip [0 ..< length sls] sls)
in case unify pairs [] of
None ⇒ None
| Some γlist ⇒ let γ = subst_of γlist in
Some (map (λ i. γ ∘ rename_many' i) [0 ..< length sls], γ ∘ ren_l))"
lemma mgu_var_disjoint_list_generic_sound:
assumes unif: "mgu_var_disjoint_list_generic rename_many' ren_l sls = Some (μ , τ)"
shows "i < length sls ⟹ fst(sls!i) ⋅ μ!i = snd(sls!i) ⋅ τ"
"length μ = length sls"
proof -
let ?pairs = "map (λ (i, (si, li)). (map_vars_term (rename_many' i) si, map_vars_term ren_l li)) (zip [0 ..< length sls] sls)"
obtain γlist where
unif2:"unify ?pairs [] = Some γlist" using assms
unfolding mgu_var_disjoint_list_generic_def by (auto split: option.splits)
let ?γ = "subst_of γlist"
from unif[unfolded mgu_var_disjoint_list_generic_def Let_def unif2, simplified]
have mu: "μ = map (λi. ?γ ∘ rename_many' i) [0..<length sls]"
and tau: "τ = ?γ ∘ ren_l" by auto
show "length μ = length sls" unfolding mu by simp
assume i: "i < length sls"
with mu have mui: "μ ! i = ?γ ∘ rename_many' i" by auto
from unify_sound[OF unif2]
have unify: "⋀ s t. (s, t) ∈ set ?pairs ⟹ s ⋅ ?γ = t ⋅ ?γ"
by (auto simp:is_imgu_def unifiers_def)
from i unify have "fst (?pairs ! i) ⋅ ?γ = snd (?pairs ! i) ⋅ ?γ"
unfolding set_conv_nth by force
also have "fst (?pairs ! i) = map_vars_term (rename_many' i) (fst (sls ! i))" using i
by (auto split: prod.splits)
also have "snd (?pairs ! i) = map_vars_term ren_l (snd (sls ! i))" using i
by (cases "sls ! i", auto)
finally
have "map_vars_term (rename_many' i) (fst(sls!i)) ⋅ ?γ = map_vars_term ren_l (snd(sls!i)) ⋅ ?γ" .
also have "map_vars_term (rename_many' i) (fst(sls!i)) ⋅ ?γ = fst (sls ! i) ⋅ (Var ∘ rename_many' i) ∘⇩s subst_of γlist"
unfolding map_vars_term_eq subst_subst ..
also have "(Var ∘ rename_many' i) ∘⇩s subst_of γlist = μ!i" unfolding mui subst_compose_def
by auto
also have "map_vars_term ren_l (snd(sls!i)) ⋅ ?γ = snd (sls ! i) ⋅ (Var ∘ ren_l) ∘⇩s subst_of γlist"
unfolding map_vars_term_eq subst_subst ..
also have "(Var ∘ ren_l) ∘⇩s subst_of γlist = τ" unfolding tau subst_compose_def
by auto
finally show "fst (sls ! i) ⋅ μ ! i = snd (sls ! i) ⋅ τ" .
qed
context
fixes ren :: "'v :: infinite renamingN"
begin
definition rename_many' where "rename_many' i == λ v. rename_many ren (i,v)"
abbreviation (input) ren_l where "ren_l == rename_single ren"
private lemma rdisj: "range (rename_many' i) ∩ range ren_l = {}"
unfolding rename_many'_def
using renameN by blast
private lemma rdisj2: "i ≠ j ⟹ range (rename_many' i) ∩ range (rename_many' j) = {}"
unfolding rename_many'_def
using renameN(1)[of ren]
using injD by fastforce
private lemma inj: "inj (rename_many' i)" "inj ren_l"
unfolding rename_many'_def
using renameN(1,2)[of ren]
by (meson Pair_inject injD injI)+
lemmas renameN = rdisj rdisj2 inj
lemma rename_many_disj:
assumes "i ≠ j"
shows "vars_term (map_vars_term (rename_many' i) t) ∩ vars_term (map_vars_term (rename_many' j) s) = {}"
by (smt (verit, best) renameN(2) assms disjoint_iff imageE rangeI term.set_map(2))
lemma mgu_var_disjoint_list_generic_complete_pre:
fixes σ :: "nat ⇒ ('f, 'v) subst" and θ :: "('f, 'v) subst"
and pairs :: "(('f, 'v)term × ('f,'v)term) list"
assumes unif_disj: "⋀ i. i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ"
shows "∃μ τ δ. mgu_var_disjoint_list_generic rename_many' ren_l pairs = Some (μ, τ) ∧
θ = τ ∘⇩s δ ∧
(∀ i < length pairs. σ i = μ!i ∘⇩s δ ∧ fst(pairs!i) ⋅ μ!i = snd(pairs!i) ⋅ τ)"
proof -
define δ where "δ x = (if (∃ i. i < length pairs ∧ x ∈ range (rename_many' i)) then
let i = (SOME i. i < length pairs ∧ x ∈ range (rename_many' i)) in
(σ i) (the_inv (rename_many' i) x) else θ (the_inv ren_l x))" for x
have ids: "⋀ i. i < length pairs ⟹ fst(pairs!i) ⋅ (σ i) = map_vars_term (rename_many' i) (fst(pairs!i)) ⋅ δ"
unfolding map_vars_term_eq
unfolding subst_subst o_def subst_compose_def
proof (rule term_subst_eq, simp)
fix i x
assume len: "i < length pairs"
let ?y = "rename_many' i x"
have cond: "(∃ i. i < length pairs ∧ ?y ∈ range (rename_many' i))" using len by auto
have some: "(SOME i. i < length pairs ∧ ?y ∈ range (rename_many' i)) = i"
proof (rule some_equality)
show i1: "i < length pairs ∧ rename_many' i x ∈ range (rename_many' i)" using len by auto
fix j
assume i2: "j < length pairs ∧ rename_many' i x ∈ range (rename_many' j)"
show "j = i" using i1 i2
by (meson i1 i2 disjoint_iff rdisj2)
qed
have delta: "δ ?y = (σ i) (the_inv (rename_many' i) ?y)" unfolding δ_def Let_def some using cond by auto
show "(σ i) x = δ ?y" unfolding delta the_inv_f_f[OF inj(1)] ..
qed
have idt: "⋀ i. i < length pairs ⟹ snd(pairs!i) ⋅ θ = map_vars_term (ren_l) (snd(pairs!i)) ⋅ δ"
unfolding map_vars_term_eq
unfolding subst_subst o_def subst_compose_def
proof (rule term_subst_eq, simp)
fix x
let ?z = "ren_l x"
have delta2: "δ ?z = θ (the_inv (ren_l) ?z)" unfolding δ_def Let_def
using rdisj by auto
show "θ x = δ ?z" unfolding delta2
by (simp add: renameN the_inv_f_f)
qed
from ids idt unif_disj
have unif: "⋀ i. i < length pairs ⟹ map_vars_term (rename_many' i) (fst(pairs!i)) ⋅ δ = map_vars_term ren_l (snd(pairs!i)) ⋅ δ" by auto
let ?E = "map2 (λi (si, li). (map_vars_term (rename_many' i) si, map_vars_term ren_l li)) [0..<length pairs] pairs"
from unif have unE:"δ ∈ unifiers (set ?E)" unfolding unifiers_def
by (smt (z3) add_0 case_prod_beta in_set_conv_nth length_map map_nth map_snd_zip mem_Collect_eq nth_map nth_upt nth_zip prod.sel(1) prod.sel(2))
hence "unify ?E [] ≠ None" using unify_complete by force
then obtain γ where unify: "unify ?E [] = Some γ" by (cases "unify ?E []", auto)
have mgu_var_defn:"mgu_var_disjoint_list_generic rename_many' ren_l pairs = Some (map (λi. subst_of γ ∘ rename_many' i) [0..<length pairs], subst_of γ ∘ ren_l)"
(is "_ = Some (?μ, ?τ)") unfolding mgu_var_disjoint_list_generic_def Let_def unify by simp
moreover have "⋀ i. i < length pairs ⟹ σ i = (?μ)!i ∘⇩s δ"
proof (rule ext)
fix i y
assume len2: "i < length pairs"
let ?w = "rename_many' i y"
have cond2: "(∃ i. i < length pairs ∧ ?w ∈ range (rename_many' i))" using len2 by auto
have some2: "(SOME i. i < length pairs ∧ ?w ∈ range (rename_many' i)) = i"
proof (rule some_equality)
show i1: "i < length pairs ∧ rename_many' i y ∈ range (rename_many' i)" using len2 by auto
fix j
assume i2: "j < length pairs ∧ rename_many' i y ∈ range (rename_many' j)"
show "j = i"
by (meson i1 i2 disjoint_iff renameN)
qed
have sub:"δ = subst_of γ ∘⇩s δ "
using unE is_imgu_def unify unify_sound by blast
then have ids1:"(?μ!i ∘⇩s δ) y = δ ?w" unfolding δ_def mgu_var_defn subst_compose_def rdisj2
using some2 fun_cong[OF sub, of ?w] cond2 len2 length_map map_nth nth_map nth_upt subst_compose_def
by (smt (verit, best) Eps_cong add_0 comp_eq_dest_lhs)
then have ids2:"δ ?w = σ i y" unfolding δ_def mgu_var_defn using inj(1) some2 cond2 len2 rdisj2
by (simp add: the_inv_f_f)
from ids1 ids2 show "σ i y = (?μ !i ∘⇩s δ) y" by simp
qed
moreover have "θ = ?τ ∘⇩s δ"
proof(rule ext)
fix z
have "(?τ ∘⇩s δ)z = δ(ren_l z)" unfolding subst_compose_def
by (metis (mono_tags, lifting) unE is_imgu_def o_apply subst_compose_def unify unify_sound)
also have "... = θ z" unfolding the_inv_f_f[OF inj(2)]
using rdisj δ_def inj(2) the_inv_f_f by fastforce
finally show "θ z = (?τ ∘⇩s δ)z" by simp
qed
moreover
{
fix i
assume i: "i < length pairs"
have "fst(pairs!i) ⋅ ?μ!i = map_vars_term (rename_many' i) (fst(pairs!i)) ⋅ (subst_of γ)"
unfolding mgu_var_defn unify apply_subst_map_vars_term using i by simp
also have "… = map_vars_term (ren_l) (snd(pairs!i)) ⋅ (subst_of γ)"
using i unfolding mgu_var_disjoint_list_generic_def unify apply_subst_map_vars_term unif_disj Let_def
using mgu_var_disjoint_list_generic_sound[OF mgu_var_defn] by simp
also have "… = snd(pairs!i) ⋅ ?τ"
unfolding mgu_var_disjoint_list_generic_def apply_subst_map_vars_term unify by simp
finally have "fst(pairs!i) ⋅ ?μ!i = snd(pairs!i) ⋅ ?τ" .
}
ultimately show ?thesis by auto
qed
lemma mgu_var_disjoint_list_generic_complete:
fixes σ :: "nat ⇒ ('f, 'v) subst" and θ :: "('f, 'v) subst"
and pairs :: "(('f, 'v)term × ('f,'v)term) list"
defines "V ≡ ⋃ (vars_term ` snd ` set pairs)"
defines "W ≡ UNIV - V"
assumes unif: "⋀ i. i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ"
shows "∃μ τ δ. mgu_var_disjoint_list_generic rename_many' ren_l pairs = Some (μ, τ) ∧
θ = τ ∘⇩s δ ∧
(∀ i < length pairs. σ i = μ!i ∘⇩s δ ∧ fst(pairs!i) ⋅ μ!i = snd(pairs!i) ⋅ τ) ∧
τ ` W ⊆ Var ` (UNIV - ⋃ (vars_term ` τ ` V) - (⋃ {⋃ (vars_term ` range (μ ! i)) | i. i < length pairs})) ∧ inj_on τ W"
proof -
let ?mgu = "mgu_var_disjoint_list_generic rename_many' ren_l"
from mgu_var_disjoint_list_generic_complete_pre[OF unif]
obtain μ τ δ where mgu: "?mgu pairs = Some (μ, τ)"
and theta: "θ = τ ∘⇩s δ" and rest: "(∀ i < length pairs. σ i = μ!i ∘⇩s δ ∧ fst(pairs!i) ⋅ μ!i = snd(pairs!i) ⋅ τ)" by auto
show ?thesis
proof (intro exI conjI, rule mgu, rule theta, rule rest)
{
fix x y
assume x: "x ∈ W" and y: "y ∈ W"
from x have x: "i < length pairs ⟹ x ∉ vars_term (snd (pairs ! i))" for i
unfolding W_def set_conv_nth V_def by fastforce
from y have y: "i < length pairs ⟹ y ∉ vars_term (snd (pairs ! i))" for i
unfolding W_def set_conv_nth V_def by fastforce
define θ' where "θ' = θ(y := Var y, x := Var x)"
have "i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ'" for i
using unif[of i] x[of i] y[of i] unfolding θ'_def
by (auto intro: term_subst_eq)
from mgu_var_disjoint_list_generic_complete_pre[OF this, unfolded mgu]
obtain δ' where "θ' = τ ∘⇩s δ'" by auto
from arg_cong[OF this, of "λ f. f x", unfolded θ'_def subst_compose_def]
arg_cong[OF this, of "λ f. f y", unfolded θ'_def subst_compose_def]
have x: "τ x ⋅ δ' = Var x" and y: "τ y ⋅ δ' = (if x = y then Var x else Var y)"
by (auto split: if_splits)
from x have ran: "τ x ∈ range Var" by (cases "τ x", auto)
from x y have inj: "τ x = τ y ⟹ x = y" by (cases "τ x"; cases "τ y", auto split: if_splits)
note ran inj
} note part_1 = this
from part_1 show "inj_on τ W" by (auto simp: inj_on_def)
from part_1 have "τ ` W ⊆ range Var" by auto
let ?Union = "⋃ {⋃ (vars_term ` range (μ ! i)) | i. i < length pairs}"
{
fix x
assume x: "x ∈ W"
from part_1[OF this this] obtain y where id: "τ x = Var y" by auto
{
assume "y ∈ ⋃ (vars_term ` τ ` V) ∪ ?Union"
hence "y ∈ ⋃ (vars_term ` τ ` V) ∨ y ∈ ?Union" by auto
hence False
proof
assume "y ∈ ?Union"
then obtain i z where i: "i < length pairs" and y: "y ∈ vars_term ((μ ! i) z)" by auto
let ?t = "(μ ! i) z"
from y obtain p where p: "p ∈ poss ?t" and eq: "?t |_ p = Var y" (is "_ = ?y") by (rule vars_term_poss_subt_at)
{
fix u
define θ' where "θ' = θ(x := u)"
from x have x: "i < length pairs ⟹ x ∉ vars_term (snd (pairs ! i))" for i
unfolding W_def set_conv_nth V_def by fastforce
have "i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ'" for i
using unif[of i] x[of i] unfolding θ'_def
by (auto intro: term_subst_eq)
from mgu_var_disjoint_list_generic_complete_pre[OF this, unfolded mgu] i
obtain δ' where theta': "θ' = τ ∘⇩s δ'" and sigma: "σ i = μ ! i ∘⇩s δ'" by auto
{
fix δ''
assume "δ'' ∈ {δ, δ'}"
hence "σ i z = ?t ⋅ δ''" using sigma rest[rule_format,OF i, THEN conjunct1]
by (metis insert_iff singletonD subst_compose)
hence "σ i z |_ p = ?t ⋅ δ'' |_ p" by simp
also have "… = δ'' y" using p eq by auto
finally have "σ i z |_ p = δ'' y" by auto
}
hence "δ y = δ' y" by (metis insertCI)
from this id have "τ x ⋅ δ = τ x ⋅ δ'" by auto
hence "θ x = θ' x" using theta theta' by (simp add: subst_compose_def)
hence "θ x = u" unfolding θ'_def by simp
}
from this[of "Fun _ _", unfolded this[of "Var undefined"]]
show False by simp
next
assume "y ∈ ⋃ (vars_term ` τ ` V)"
from this[unfolded V_def set_conv_nth] obtain i
where i: "i < length pairs" and y: "y ∈ ⋃ (vars_term ` τ ` vars_term (snd (pairs ! i)))"
by force
let ?t = "snd (pairs ! i) ⋅ τ"
from y have y: "y ∈ vars_term ?t"
by (metis vars_term_subst)
then obtain p where p: "p ∈ poss ?t" and eq: "?t |_ p = Var y" (is "_ = ?y") by (rule vars_term_poss_subt_at)
{
fix u
define θ' where "θ' = θ(x := u)"
from x have x: "i < length pairs ⟹ x ∉ vars_term (snd (pairs ! i))" for i
unfolding W_def set_conv_nth V_def by fastforce
have "i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ'" for i
using unif[of i] x[of i] unfolding θ'_def
by (auto intro: term_subst_eq)
from mgu_var_disjoint_list_generic_complete_pre[OF this, unfolded mgu]
obtain δ where theta: "θ' = τ ∘⇩s δ" by auto
from eq have "(?t |_ p) ⋅ δ = ?y ⋅ δ" by simp
also have "(?t |_ p) ⋅ δ = (?t ⋅ δ) |_ p" using p by auto
also have "?t ⋅ δ = snd (pairs ! i) ⋅ θ'" unfolding theta by simp
also have "… = snd (pairs ! i) ⋅ θ" unfolding θ'_def
by (rule term_subst_eq, insert x[OF i], auto)
also have "?y ⋅ δ = δ y" by simp
also have "… = θ' x" unfolding theta using id by (auto simp: subst_compose_def)
also have "… = u" unfolding θ'_def by simp
finally have "snd (pairs ! i) ⋅ θ |_ p = u" .
}
from this[of "Fun _ _", unfolded this[of "Var undefined"]]
show False by simp
qed
}
hence "τ x ∈ Var ` (UNIV - ⋃ (vars_term ` τ ` V) - ?Union)" using id by blast
}
with part_1 show "τ ` W ⊆ Var ` (UNIV - ⋃ (vars_term ` τ ` V) - ?Union)" by auto
qed
qed
end
definition "mgu_vd_list ren = mgu_var_disjoint_list_generic (rename_many' ren) (rename_single ren)"
lemma mgu_vd_list_sound:
assumes "mgu_vd_list ren pairs = Some (μ , τ)"
shows "i < length pairs ⟹ fst(pairs!i) ⋅ μ!i = snd(pairs!i) ⋅ τ"
"length μ = length pairs"
using assms mgu_var_disjoint_list_generic_sound
unfolding mgu_vd_list_def by blast+
lemma mgu_vd_list_complete:
fixes σ :: "nat ⇒ ('f, 'v :: infinite) subst" and θ :: "('f, 'v) subst"
and pairs :: "(('f, 'v)term × ('f,'v)term) list"
defines "V ≡ ⋃ (vars_term ` snd ` set pairs)"
defines "W ≡ UNIV - V"
assumes unif: "⋀ i. i < length pairs ⟹ fst(pairs!i) ⋅ σ i = snd(pairs!i) ⋅ θ"
shows "∃μ τ δ. mgu_vd_list ren pairs = Some (μ, τ) ∧
θ = τ ∘⇩s δ ∧
(∀ i < length pairs. σ i = μ!i ∘⇩s δ ∧ fst(pairs!i) ⋅ μ!i = snd(pairs!i) ⋅ τ) ∧
τ ` W ⊆ Var ` (UNIV - ⋃ (vars_term ` τ ` V) - (⋃ {⋃ (vars_term ` range (μ ! i)) | i. i < length pairs})) ∧ inj_on τ W"
unfolding mgu_vd_list_def V_def W_def
by (rule mgu_var_disjoint_list_generic_complete; (intro unif)?)
end