(* Author: Christian Sternagel <c.sternagel@gmail.com> Author: René Thiemann <rene.thiemann@uibk.ac.at> License: LGPL *) subsection ‹A Concrete Unification Algorithm› theory Unification imports Abstract_Unification Option_Monad Renaming2 begin definition "decompose s t = (case (s, t) of (Fun f ss, Fun g ts) ⇒ if f = g then zip_option ss ts else None | _ ⇒ None)" lemma decompose_same_Fun[simp]: ✐‹contributor ‹Martin Desharnais›› "decompose (Fun f ss) (Fun f ss) = Some (zip ss ss)" by (simp add: decompose_def) lemma decompose_Some [dest]: "decompose (Fun f ss) (Fun g ts) = Some E ⟹ f = g ∧ length ss = length ts ∧ E = zip ss ts" by (cases "f = g") (auto simp: decompose_def) lemma decompose_None [dest]: "decompose (Fun f ss) (Fun g ts) = None ⟹ f ≠ g ∨ length ss ≠ length ts" by (cases "f = g") (auto simp: decompose_def) text ‹Applying a substitution to a list of equations.› definition subst_list :: "('f, 'v) subst ⇒ ('f, 'v) equation list ⇒ ('f, 'v) equation list" where "subst_list σ ys = map (λp. (fst p ⋅ σ, snd p ⋅ σ)) ys" lemma mset_subst_list [simp]: "mset (subst_list (subst x t) ys) = subst_mset (subst x t) (mset ys)" by (auto simp: subst_mset_def subst_list_def) lemma subst_list_append: "subst_list σ (xs @ ys) = subst_list σ xs @ subst_list σ ys" by (auto simp: subst_list_def) function (sequential) unify :: "('f, 'v) equation list ⇒ ('v × ('f, 'v) term) list ⇒ ('v × ('f, 'v) term) list option" where "unify [] bs = Some bs" | "unify ((Fun f ss, Fun g ts) # E) bs = (case decompose (Fun f ss) (Fun g ts) of None ⇒ None | Some us ⇒ unify (us @ E) bs)" | "unify ((Var x, t) # E) bs = (if t = Var x then unify E bs else if x ∈ vars_term t then None else unify (subst_list (subst x t) E) ((x, t) # bs))" | "unify ((t, Var x) # E) bs = (if x ∈ vars_term t then None else unify (subst_list (subst x t) E) ((x, t) # bs))" by pat_completeness auto termination by (standard, rule wf_inv_image [of "unif¯" "mset ∘ fst", OF wf_converse_unif]) (force intro: UNIF1.intros simp: unif_def union_commute)+ lemma unify_append_prefix_same: ✐‹contributor ‹Martin Desharnais›› "(∀e ∈ set es1. fst e = snd e) ⟹ unify (es1 @ es2) bs = unify es2 bs" proof (induction "es1 @ es2" bs arbitrary: es1 es2 bs rule: unify.induct) case (1 bs) thus ?case by simp next case (2 f ss g ts E bs) show ?case proof (cases es1) case Nil thus ?thesis by simp next case (Cons e es1') hence e_def: "e = (Fun f ss, Fun g ts)" and E_def: "E = es1' @ es2" using "2" by simp_all hence "f = g" and "ss = ts" using "2.prems" local.Cons by auto hence "unify (es1 @ es2) bs = unify ((zip ts ts @ es1') @ es2) bs" by (simp add: Cons e_def) also have "… = unify es2 bs" proof (rule "2.hyps"(1)) show "decompose (Fun f ss) (Fun g ts) = Some (zip ts ts)" by (simp add: ‹f = g› ‹ss = ts›) next show "zip ts ts @ E = (zip ts ts @ es1') @ es2" by (simp add: E_def) next show "∀e∈set (zip ts ts @ es1'). fst e = snd e" using "2.prems" by (auto simp: Cons zip_same) qed finally show ?thesis . qed next case (3 x t E bs) show ?case proof (cases es1) case Nil thus ?thesis by simp next case (Cons e es1') hence e_def: "e = (Var x, t)" and E_def: "E = es1' @ es2" using 3 by simp_all show ?thesis proof (cases "t = Var x") case True show ?thesis using 3(1)[OF True E_def] using "3.hyps"(3) "3.prems" local.Cons by fastforce next case False thus ?thesis using "3.prems" e_def local.Cons by force qed qed next case (4 v va x E bs) then show ?case proof (cases es1) case Nil thus ?thesis by simp next case (Cons e es1') hence e_def: "e = (Fun v va, Var x)" and E_def: "E = es1' @ es2" using 4 by simp_all thus ?thesis using "4.prems" local.Cons by fastforce qed qed corollary unify_Cons_same: ✐‹contributor ‹Martin Desharnais›› "fst e = snd e ⟹ unify (e # es) bs = unify es bs" by (rule unify_append_prefix_same[of "[_]", simplified]) corollary unify_same: ✐‹contributor ‹Martin Desharnais›› "(∀e ∈ set es. fst e = snd e) ⟹ unify es bs = Some bs" by (rule unify_append_prefix_same[of _ "[]", simplified]) definition subst_of :: "('v × ('f, 'v) term) list ⇒ ('f, 'v) subst" where "subst_of ss = List.foldr (λ(x, t) σ. σ ∘⇩_{s}subst x t) ss Var" text ‹Computing the mgu of two terms.› definition mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) subst option" where "mgu s t = (case unify [(s, t)] [] of None ⇒ None | Some res ⇒ Some (subst_of res))" lemma subst_of_simps [simp]: "subst_of [] = Var" "subst_of ((x, Var x) # ss) = subst_of ss" "subst_of (b # ss) = subst_of ss ∘⇩_{s}subst (fst b) (snd b)" by (simp_all add: subst_of_def split: prod.splits) lemma subst_of_append [simp]: "subst_of (ss @ ts) = subst_of ts ∘⇩_{s}subst_of ss" by (induct ss) (auto simp: ac_simps) text ‹The concrete algorithm ‹unify› can be simulated by the inference rules of ‹UNIF›.› lemma unify_Some_UNIF: assumes "unify E bs = Some cs" shows "∃ds ss. cs = ds @ bs ∧ subst_of ds = compose ss ∧ UNIF ss (mset E) {#}" using assms proof (induction E bs arbitrary: cs rule: unify.induct) case (2 f ss g ts E bs) then obtain us where "decompose (Fun f ss) (Fun g ts) = Some us" and [simp]: "f = g" "length ss = length ts" "us = zip ss ts" and "unify (us @ E) bs = Some cs" by (auto split: option.splits) from "2.IH" [OF this(1, 5)] obtain xs ys where "cs = xs @ bs" and [simp]: "subst_of xs = compose ys" and *: "UNIF ys (mset (us @ E)) {#}" by auto then have "UNIF (Var # ys) (mset ((Fun f ss, Fun g ts) # E)) {#}" by (force intro: UNIF1.decomp simp: ac_simps) moreover have "cs = xs @ bs" by fact moreover have "subst_of xs = compose (Var # ys)" by simp ultimately show ?case by blast next case (3 x t E bs) show ?case proof (cases "t = Var x") assume "t = Var x" then show ?case using 3 by auto (metis UNIF.step compose_simps(2) UNIF1.trivial) next assume "t ≠ Var x" with 3 obtain xs ys where [simp]: "cs = (ys @ [(x, t)]) @ bs" and [simp]: "subst_of ys = compose xs" and "x ∉ vars_term t" and "UNIF xs (mset (subst_list (subst x t) E)) {#}" by (cases "x ∈ vars_term t") force+ then have "UNIF (subst x t # xs) (mset ((Var x, t) # E)) {#}" by (force intro: UNIF1.Var_left simp: ac_simps) moreover have "cs = (ys @ [(x, t)]) @ bs" by simp moreover have "subst_of (ys @ [(x, t)]) = compose (subst x t # xs)" by simp ultimately show ?case by blast qed next case (4 f ss x E bs) with 4 obtain xs ys where [simp]: "cs = (ys @ [(x, Fun f ss)]) @ bs" and [simp]: "subst_of ys = compose xs" and "x ∉ vars_term (Fun f ss)" and "UNIF xs (mset (subst_list (subst x (Fun f ss)) E)) {#}" by (cases "x ∈ vars_term (Fun f ss)") force+ then have "UNIF (subst x (Fun f ss) # xs) (mset ((Fun f ss, Var x) # E)) {#}" by (force intro: UNIF1.Var_right simp: ac_simps) moreover have "cs = (ys @ [(x, Fun f ss)]) @ bs" by simp moreover have "subst_of (ys @ [(x, Fun f ss)]) = compose (subst x (Fun f ss) # xs)" by simp ultimately show ?case by blast qed force lemma unify_sound: assumes "unify E [] = Some cs" shows "is_imgu (subst_of cs) (set E)" proof - from unify_Some_UNIF [OF assms] obtain ss where "subst_of cs = compose ss" and "UNIF ss (mset E) {#}" by auto with UNIF_empty_imp_is_mgu_compose [OF this(2)] and UNIF_idemp [OF this(2)] show ?thesis by (auto simp add: is_imgu_def is_mgu_def) (metis subst_compose_assoc) qed lemma mgu_sound: assumes "mgu s t = Some σ" shows "is_imgu σ {(s, t)}" proof - obtain ss where "unify [(s, t)] [] = Some ss" and "σ = subst_of ss" using assms by (auto simp: mgu_def split: option.splits) then have "is_imgu σ (set [(s, t)])" by (metis unify_sound) then show ?thesis by simp qed text ‹If ‹unify› gives up, then the given set of equations cannot be reduced to the empty set by ‹UNIF›.› lemma unify_None: assumes "unify E ss = None" shows "∃E'. E' ≠ {#} ∧ (mset E, E') ∈ unif⇧^{!}" using assms proof (induction E ss rule: unify.induct) case (1 bs) then show ?case by simp next case (2 f ss g ts E bs) moreover { assume *: "decompose (Fun f ss) (Fun g ts) = None" have ?case proof (cases "unifiable (set E)") case True then have "(mset E, {#}) ∈ unif⇧^{*}" by (simp add: unifiable_imp_empty) from unif_rtrancl_mono [OF this, of "{#(Fun f ss, Fun g ts)#}"] obtain σ where "(mset E + {#(Fun f ss, Fun g ts)#}, {#(Fun f ss ⋅ σ, Fun g ts ⋅ σ)#}) ∈ unif⇧^{*}" by (auto simp: subst_mset_def) moreover have "{#(Fun f ss ⋅ σ, Fun g ts ⋅ σ)#} ∈ NF unif" using decompose_None [OF *] by (auto simp: single_is_union NF_def unif_def elim!: UNIF1.cases) (metis length_map) ultimately show ?thesis by auto (metis normalizability_I add_mset_not_empty) next case False moreover have "¬ unifiable {(Fun f ss, Fun g ts)}" using * by (auto simp: unifiable_def) ultimately have "¬ unifiable (set ((Fun f ss, Fun g ts) # E))" by (auto simp: unifiable_def unifiers_def) then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF) qed } moreover { fix us assume *: "decompose (Fun f ss) (Fun g ts) = Some us" and "unify (us @ E) bs = None" from "2.IH" [OF this] obtain E' where "E' ≠ {#}" and "(mset (us @ E), E') ∈ unif⇧^{!}" by blast moreover have "(mset ((Fun f ss, Fun g ts) # E), mset (us @ E)) ∈ unif" proof - have "g = f" and "length ss = length ts" and "us = zip ss ts" using * by auto then show ?thesis by (auto intro: UNIF1.decomp simp: unif_def ac_simps) qed ultimately have ?case by auto } ultimately show ?case by (auto split: option.splits) next case (3 x t E bs) { assume [simp]: "t = Var x" obtain E' where "E' ≠ {#}" and "(mset E, E') ∈ unif⇧^{!}" using 3 by auto moreover have "(mset ((Var x, t) # E), mset E) ∈ unif" by (auto intro: UNIF1.trivial simp: unif_def) ultimately have ?case by auto } moreover { assume *: "t ≠ Var x" "x ∉ vars_term t" then obtain E' where "E' ≠ {#}" and "(mset (subst_list (subst x t) E), E') ∈ unif⇧^{!}" using 3 by auto moreover have "(mset ((Var x, t) # E), mset (subst_list (subst x t) E)) ∈ unif" using * by (auto intro: UNIF1.Var_left simp: unif_def) ultimately have ?case by auto } moreover { assume *: "t ≠ Var x" "x ∈ vars_term t" then have "x ∈ vars_term t" "is_Fun t" by auto then have "¬ unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable) then have **: "¬ unifiable {(Var x ⋅ σ, t ⋅ σ)}" for σ :: "('b, 'a) subst" using subst_set_reflects_unifiable [of σ "{(Var x, t)}"] by (auto simp: subst_set_def) have ?case proof (cases "unifiable (set E)") case True then have "(mset E, {#}) ∈ unif⇧^{*}" by (simp add: unifiable_imp_empty) from unif_rtrancl_mono [OF this, of "{#(Var x, t)#}"] obtain σ where "(mset E + {#(Var x, t)#}, {#(Var x ⋅ σ, t ⋅ σ)#}) ∈ unif⇧^{*}" by (auto simp: subst_mset_def) moreover obtain E' where "E' ≠ {#}" and "({#(Var x ⋅ σ, t ⋅ σ)#}, E') ∈ unif⇧^{!}" using not_unifiable_imp_not_empty_NF and ** by (metis set_mset_single) ultimately show ?thesis by auto next case False moreover have "¬ unifiable {(Var x, t)}" using * by (force simp: unifiable_def) ultimately have "¬ unifiable (set ((Var x, t) # E))" by (auto simp: unifiable_def unifiers_def) then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF) qed } ultimately show ?case by blast next case (4 f ss x E bs) define t where "t = Fun f ss" { assume *: "x ∉ vars_term t" then obtain E' where "E' ≠ {#}" and "(mset (subst_list (subst x t) E), E') ∈ unif⇧^{!}" using 4 by (auto simp: t_def) moreover have "(mset ((t, Var x) # E), mset (subst_list (subst x t) E)) ∈ unif" using * by (auto intro: UNIF1.Var_right simp: unif_def) ultimately have ?case by (auto simp: t_def) } moreover { assume "x ∈ vars_term t" then have *: "x ∈ vars_term t" "t ≠ Var x" by (auto simp: t_def) then have "x ∈ vars_term t" "is_Fun t" by auto then have "¬ unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable) then have **: "¬ unifiable {(Var x ⋅ σ, t ⋅ σ)}" for σ :: "('b, 'a) subst" using subst_set_reflects_unifiable [of σ "{(Var x, t)}"] by (auto simp: subst_set_def) have ?case proof (cases "unifiable (set E)") case True then have "(mset E, {#}) ∈ unif⇧^{*}" by (simp add: unifiable_imp_empty) from unif_rtrancl_mono [OF this, of "{#(t, Var x)#}"] obtain σ where "(mset E + {#(t, Var x)#}, {#(t ⋅ σ, Var x ⋅ σ)#}) ∈ unif⇧^{*}" by (auto simp: subst_mset_def) moreover obtain E' where "E' ≠ {#}" and "({#(t ⋅ σ, Var x ⋅ σ)#}, E') ∈ unif⇧^{!}" using not_unifiable_imp_not_empty_NF and ** by (metis unifiable_insert_swap set_mset_single) ultimately show ?thesis by (auto simp: t_def) next case False moreover have "¬ unifiable {(t, Var x)}" using * by (simp add: unifiable_def) ultimately have "¬ unifiable (set ((t, Var x) # E))" by (auto simp: unifiable_def unifiers_def) then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF t_def) qed } ultimately show ?case by blast qed lemma unify_complete: assumes "unify E bs = None" shows "unifiers (set E) = {}" proof - from unify_None [OF assms] obtain E' where "E' ≠ {#}" and "(mset E, E') ∈ unif⇧^{!}" by blast then have "¬ unifiable (set E)" using irreducible_reachable_imp_not_unifiable by force then show ?thesis by (auto simp: unifiable_def) qed corollary ex_unify_if_unifiers_not_empty: ✐‹contributor ‹Martin Desharnais›› "unifiers es ≠ {} ⟹ set xs = es ⟹ ∃ys. unify xs [] = Some ys" using unify_complete by auto lemma mgu_complete: "mgu s t = None ⟹ unifiers {(s, t)} = {}" proof - assume "mgu s t = None" then have "unify [(s, t)] [] = None" by (cases "unify [(s, t)] []", auto simp: mgu_def) then have "unifiers (set [(s, t)]) = {}" by (rule unify_complete) then show ?thesis by simp qed corollary ex_mgu_if_unifiers_not_empty: ✐‹contributor ‹Martin Desharnais›› "unifiers {(t,u)} ≠ {} ⟹ ∃μ. mgu t u = Some μ" using mgu_complete by auto corollary ex_mgu_if_subst_apply_term_eq_subst_apply_term: ✐‹contributor ‹Martin Desharnais›› fixes t u :: "('f, 'v) Term.term" and σ :: "('f, 'v) subst" assumes t_eq_u: "t ⋅ σ = u ⋅ σ" shows "∃μ :: ('f, 'v) subst. Unification.mgu t u = Some μ" proof - from t_eq_u have "unifiers {(t, u)} ≠ {}" unfolding unifiers_def by auto thus ?thesis by (rule ex_mgu_if_unifiers_not_empty) qed lemma finite_subst_domain_subst_of: "finite (subst_domain (subst_of xs))" proof (induct xs) case (Cons x xs) moreover have "finite (subst_domain (subst (fst x) (snd x)))" by (metis finite_subst_domain_subst) ultimately show ?case using subst_domain_compose [of "subst_of xs" "subst (fst x) (snd x)"] by (simp del: subst_subst_domain) (metis finite_subset infinite_Un) qed simp lemma unify_subst_domain: ✐‹contributor ‹Martin Desharnais›› assumes unif: "unify E [] = Some xs" shows "subst_domain (subst_of xs) ⊆ (⋃e ∈ set E. vars_term (fst e) ∪ vars_term (snd e))" proof - from unify_Some_UNIF[OF unif] obtain xs' where "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}" by auto thus ?thesis using UNIF_subst_domain_subset by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def) qed lemma mgu_subst_domain: assumes "mgu s t = Some σ" shows "subst_domain σ ⊆ vars_term s ∪ vars_term t" proof - obtain xs where "unify [(s, t)] [] = Some xs" and "σ = subst_of xs" using assms by (simp add: mgu_def split: option.splits) thus ?thesis using unify_subst_domain by fastforce qed lemma mgu_finite_subst_domain: "mgu s t = Some σ ⟹ finite (subst_domain σ)" by (drule mgu_subst_domain) (simp add: finite_subset) lemma unify_range_vars: ✐‹contributor ‹Martin Desharnais›› assumes unif: "unify E [] = Some xs" shows "range_vars (subst_of xs) ⊆ (⋃e ∈ set E. vars_term (fst e) ∪ vars_term (snd e))" proof - from unify_Some_UNIF[OF unif] obtain xs' where "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}" by auto thus ?thesis using UNIF_range_vars_subset by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def) qed lemma mgu_range_vars: ✐‹contributor ‹Martin Desharnais›› assumes "mgu s t = Some μ" shows "range_vars μ ⊆ vars_term s ∪ vars_term t" proof - obtain xs where "unify [(s, t)] [] = Some xs" and "μ = subst_of xs" using assms by (simp add: mgu_def split: option.splits) thus ?thesis using unify_range_vars by fastforce qed lemma unify_subst_domain_range_vars_disjoint: ✐‹contributor ‹Martin Desharnais›› assumes unif: "unify E [] = Some xs" shows "subst_domain (subst_of xs) ∩ range_vars (subst_of xs) = {}" proof - from unify_Some_UNIF[OF unif] obtain xs' where "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}" by auto thus ?thesis using UNIF_subst_domain_range_vars_Int by metis qed lemma mgu_subst_domain_range_vars_disjoint: ✐‹contributor ‹Martin Desharnais›› assumes "mgu s t = Some μ" shows "subst_domain μ ∩ range_vars μ = {}" proof - obtain xs where "unify [(s, t)] [] = Some xs" and "μ = subst_of xs" using assms by (simp add: mgu_def split: option.splits) thus ?thesis using unify_subst_domain_range_vars_disjoint by metis qed corollary subst_apply_term_eq_subst_apply_term_if_mgu: ✐‹contributor ‹Martin Desharnais›› assumes mgu_t_u: "mgu t u = Some μ" shows "t ⋅ μ = u ⋅ μ" using mgu_sound[OF mgu_t_u] by (simp add: is_imgu_def unifiers_def) lemma mgu_same: "mgu t t = Some Var" ✐‹contributor ‹Martin Desharnais›› by (simp add: mgu_def unify_same) lemma mgu_is_Var_if_not_in_equations: ✐‹contributor ‹Martin Desharnais›› fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and x :: 'v assumes mgu_μ: "is_mgu μ E" and x_not_in: "x ∉ (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))" shows "is_Var (μ x)" proof - from mgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. ∃γ. τ = μ ∘⇩_{s}γ" by (simp_all add: is_mgu_def) define τ :: "('f, 'v) subst" where "τ = (λx. if x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)) then μ x else Var x)" have ‹τ ∈ unifiers E› unfolding unifiers_def mem_Collect_eq proof (rule ballI) fix e assume "e ∈ E" with unif_μ have "fst e ⋅ μ = snd e ⋅ μ" by blast moreover from ‹e ∈ E› have "fst e ⋅ τ = fst e ⋅ μ" and "snd e ⋅ τ = snd e ⋅ μ" unfolding term_subst_eq_conv by (auto simp: τ_def) ultimately show "fst e ⋅ τ = snd e ⋅ τ" by simp qed with minimal_μ obtain γ where "μ ∘⇩_{s}γ = τ" by auto with x_not_in have "(μ ∘⇩_{s}γ) x = Var x" by (simp add: τ_def) thus "is_Var (μ x)" by (metis subst_apply_eq_Var subst_compose term.disc(1)) qed corollary mgu_ball_is_Var: ✐‹contributor ‹Martin Desharnais›› "is_mgu μ E ⟹ ∀x ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e)). is_Var (μ x)" by (rule ballI) (rule mgu_is_Var_if_not_in_equations[folded Compl_iff]) lemma mgu_inj_on: ✐‹contributor ‹Martin Desharnais›› fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" assumes mgu_μ: "is_mgu μ E" shows "inj_on μ (- (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)))" proof (rule inj_onI) fix x y assume x_in: "x ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))" and y_in: "y ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))" and "μ x = μ y" from mgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. ∃γ. τ = μ ∘⇩_{s}γ" by (simp_all add: is_mgu_def) define τ :: "('f, 'v) subst" where "τ = (λx. if x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)) then μ x else Var x)" have ‹τ ∈ unifiers E› unfolding unifiers_def mem_Collect_eq proof (rule ballI) fix e assume "e ∈ E" with unif_μ have "fst e ⋅ μ = snd e ⋅ μ" by blast moreover from ‹e ∈ E› have "fst e ⋅ τ = fst e ⋅ μ" and "snd e ⋅ τ = snd e ⋅ μ" unfolding term_subst_eq_conv by (auto simp: τ_def) ultimately show "fst e ⋅ τ = snd e ⋅ τ" by simp qed with minimal_μ obtain γ where "μ ∘⇩_{s}γ = τ" by auto hence "(μ ∘⇩_{s}γ) x = Var x" and "(μ ∘⇩_{s}γ) y = Var y" using ComplD[OF x_in] ComplD[OF y_in] by (simp_all add: τ_def) with ‹μ x = μ y› show "x = y" by (simp add: subst_compose_def) qed lemma imgu_subst_domain_subset: ✐‹contributor ‹Martin Desharnais›› fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set" assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E" defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))" shows "subst_domain μ ⊆ Evars" proof (intro Set.subsetI) from imgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. μ ∘⇩_{s}τ = τ" by (simp_all add: is_imgu_def) from fin_E obtain es :: "('f, 'v) equation list" where "set es = E" using finite_list by auto then obtain xs :: "('v × ('f, 'v) Term.term) list" where unify_es: "unify es [] = Some xs" using unif_μ ex_unify_if_unifiers_not_empty by blast define τ :: "('f, 'v) subst" where "τ = subst_of xs" have dom_τ: "subst_domain τ ⊆ Evars" using unify_subst_domain[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] . have range_vars_τ: "range_vars τ ⊆ Evars" using unify_range_vars[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] . have "τ ∈ unifiers E" using ‹set es = E› unify_es τ_def is_imgu_def unify_sound by blast with minimal_μ have μ_comp_τ: "⋀x. (μ ∘⇩_{s}τ) x = τ x" by auto fix x :: 'v assume "x ∈ subst_domain μ" hence "μ x ≠ Var x" by (simp add: subst_domain_def) show "x ∈ Evars" proof (cases "x ∈ subst_domain τ") case True thus ?thesis using dom_τ by auto next case False hence "τ x = Var x" by (simp add: subst_domain_def) hence "μ x ⋅ τ = Var x" using μ_comp_τ[of x] by (simp add: subst_compose) thus ?thesis proof (rule subst_apply_eq_Var) show "⋀y. μ x = Var y ⟹ τ y = Var x ⟹ ?thesis" using ‹μ x ≠ Var x› range_vars_τ mem_range_varsI[of τ _ x] by auto qed qed qed lemma imgu_range_vars_of_equations_vars_subset: ✐‹contributor ‹Martin Desharnais›› fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set" assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E" defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))" shows "(⋃x ∈ Evars. vars_term (μ x)) ⊆ Evars" proof (rule Set.subsetI) from imgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. μ ∘⇩_{s}τ = τ" by (simp_all add: is_imgu_def) from fin_E obtain es :: "('f, 'v) equation list" where "set es = E" using finite_list by auto then obtain xs :: "('v × ('f, 'v) Term.term) list" where unify_es: "unify es [] = Some xs" using unif_μ ex_unify_if_unifiers_not_empty by blast define τ :: "('f, 'v) subst" where "τ = subst_of xs" have dom_τ: "subst_domain τ ⊆ Evars" using unify_subst_domain[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] . have range_vars_τ: "range_vars τ ⊆ Evars" using unify_range_vars[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] . hence ball_vars_apply_τ_subset: "∀x ∈ subst_domain τ. vars_term (τ x) ⊆ Evars" unfolding range_vars_def by (simp add: SUP_le_iff) have "τ ∈ unifiers E" using ‹set es = E› unify_es τ_def is_imgu_def unify_sound by blast with minimal_μ have μ_comp_τ: "⋀x. (μ ∘⇩_{s}τ) x = τ x" by auto fix y :: 'v assume "y ∈ (⋃x ∈ Evars. vars_term (μ x))" then obtain x :: 'v where x_in: "x ∈ Evars" and y_in: "y ∈ vars_term (μ x)" by (auto simp: subst_domain_def) have vars_τ_x: "vars_term (τ x) ⊆ Evars" using ball_vars_apply_τ_subset subst_domain_def x_in by fastforce show "y ∈ Evars" proof (rule ccontr) assume "y ∉ Evars" hence "y ∉ vars_term (τ x)" using vars_τ_x by blast moreover have "y ∈ vars_term ((μ ∘⇩_{s}τ) x)" proof - have "τ y = Var y" using ‹y ∉ Evars› dom_τ by (auto simp add: subst_domain_def) thus ?thesis unfolding subst_compose_def vars_term_subst_apply_term UN_iff using y_in by force qed ultimately show False using μ_comp_τ[of x] by simp qed qed lemma imgu_range_vars_subset: ✐‹contributor ‹Martin Desharnais›› fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E" shows "range_vars μ ⊆ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))" proof - have "range_vars μ = (⋃x ∈ subst_domain μ. vars_term (μ x))" by (simp add: range_vars_def) also have "… ⊆ (⋃x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)). vars_term (μ x))" using imgu_subst_domain_subset[OF imgu_μ fin_E] by fast also have "… ⊆ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))" using imgu_range_vars_of_equations_vars_subset[OF imgu_μ fin_E] by metis finally show ?thesis . qed definition the_mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f ,'v) subst" where "the_mgu s t = (case mgu s t of None ⇒ Var | Some δ ⇒ δ)" lemma the_mgu_is_imgu: fixes σ :: "('f, 'v) subst" assumes "s ⋅ σ = t ⋅ σ" shows "is_imgu (the_mgu s t) {(s, t)}" proof - from assms have "unifiers {(s, t)} ≠ {}" by (force simp: unifiers_def) then obtain τ where "mgu s t = Some τ" and "the_mgu s t = τ" using mgu_complete by (auto simp: the_mgu_def) with mgu_sound show ?thesis by blast qed lemma the_mgu: fixes σ :: "('f, 'v) subst" assumes "s ⋅ σ = t ⋅ σ" shows "s ⋅ the_mgu s t = t ⋅ the_mgu s t ∧ σ = the_mgu s t ∘⇩_{s}σ" proof - have *: "σ ∈ unifiers {(s, t)}" by (force simp: assms unifiers_def) show ?thesis proof (cases "mgu s t") assume "mgu s t = None" then have "unifiers {(s, t)} = {}" by (rule mgu_complete) with * show ?thesis by simp next fix τ assume "mgu s t = Some τ" moreover then have "is_imgu τ {(s, t)}" by (rule mgu_sound) ultimately have "is_imgu (the_mgu s t) {(s, t)}" by (unfold the_mgu_def, simp) with * show ?thesis by (auto simp: is_imgu_def unifiers_def) qed qed subsubsection ‹Unification of two terms where variables should be considered disjoint› definition mgu_var_disjoint_generic :: "('v ⇒ 'u) ⇒ ('w ⇒ 'u) ⇒ ('f, 'v) term ⇒ ('f, 'w) term ⇒ (('f, 'v, 'u) gsubst × ('f, 'w, 'u) gsubst) option" where "mgu_var_disjoint_generic vu wu s t = (case mgu (map_vars_term vu s) (map_vars_term wu t) of None ⇒ None | Some γ ⇒ Some (γ ∘ vu, γ ∘ wu))" lemma mgu_var_disjoint_generic_sound: assumes unif: "mgu_var_disjoint_generic vu wu s t = Some (γ1, γ2)" shows "s ⋅ γ1 = t ⋅ γ2" proof - from unif[unfolded mgu_var_disjoint_generic_def] obtain γ where unif2: "mgu (map_vars_term vu s) (map_vars_term wu t) = Some γ" by (cases "mgu (map_vars_term vu s) (map_vars_term wu t)", auto) from mgu_sound[OF unif2[unfolded mgu_var_disjoint_generic_def], unfolded is_imgu_def unifiers_def] have "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" by auto from this[unfolded apply_subst_map_vars_term] unif[unfolded mgu_var_disjoint_generic_def unif2] show ?thesis by simp qed (* if terms s and t can become identical via two substitutions σ and δ then mgu_var_disjoint yields two more general substitutions μ1 μ2 *) lemma mgu_var_disjoint_generic_complete: fixes σ :: "('f, 'v, 'u) gsubst" and τ :: "('f, 'w, 'u) gsubst" and vu :: "'v ⇒ 'u" and wu:: "'w ⇒ 'u" assumes inj: "inj vu" "inj wu" and vwu: "range vu ∩ range wu = {}" and unif_disj: "s ⋅ σ = t ⋅ τ" shows "∃μ1 μ2 δ. mgu_var_disjoint_generic vu wu s t = Some (μ1, μ2) ∧ σ = μ1 ∘⇩_{s}δ ∧ τ = μ2 ∘⇩_{s}δ ∧ s ⋅ μ1 = t ⋅ μ2" proof - note inv1[simp] = the_inv_f_f[OF inj(1)] note inv2[simp] = the_inv_f_f[OF inj(2)] obtain γ :: "('f,'u)subst" where gamma: "γ = (λ x. if x ∈ range vu then σ (the_inv vu x) else τ (the_inv wu x))" by auto have ids: "s ⋅ σ = map_vars_term vu s ⋅ γ" unfolding gamma by (induct s, auto) have idt: "t ⋅ τ = map_vars_term wu t ⋅ γ" unfolding gamma by (induct t, insert vwu, auto) from unif_disj ids idt have unif: "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" (is "?s ⋅ γ = ?t ⋅ γ") by auto from the_mgu[OF unif] have unif2: "?s ⋅ the_mgu ?s ?t = ?t ⋅ the_mgu ?s ?t" and inst: "γ = the_mgu ?s ?t ∘⇩_{s}γ" by auto have "mgu ?s ?t = Some (the_mgu ?s ?t)" unfolding the_mgu_def using mgu_complete[unfolded unifiers_def] unif by (cases "mgu ?s ?t", auto) with inst obtain μ where mu: "mgu ?s ?t = Some μ" and gamma_mu: "γ = μ ∘⇩_{s}γ" by auto let ?tau1 = "μ ∘ vu" let ?tau2 = "μ ∘ wu" show ?thesis unfolding mgu_var_disjoint_generic_def mu option.simps proof (intro exI conjI, rule refl) show "σ = ?tau1 ∘⇩_{s}γ" proof (rule ext) fix x have "(?tau1 ∘⇩_{s}γ) x = γ (vu x)" using fun_cong[OF gamma_mu, of "vu x"] by (simp add: subst_compose_def) also have "... = σ x" unfolding gamma by simp finally show "σ x = (?tau1 ∘⇩_{s}γ) x" by simp qed next show "τ = ?tau2 ∘⇩_{s}γ" proof (rule ext) fix x have "(?tau2 ∘⇩_{s}γ) x = γ (wu x)" using fun_cong[OF gamma_mu, of "wu x"] by (simp add: subst_compose_def) also have "... = τ x" unfolding gamma using vwu by auto finally show "τ x = (?tau2 ∘⇩_{s}γ) x" by simp qed next have "s ⋅ ?tau1 = map_vars_term vu s ⋅ μ" unfolding apply_subst_map_vars_term .. also have "... = map_vars_term wu t ⋅ μ" unfolding unif2[unfolded the_mgu_def mu option.simps] .. also have "... = t ⋅ ?tau2" unfolding apply_subst_map_vars_term .. finally show "s ⋅ ?tau1 = t ⋅ ?tau2" . qed qed abbreviation "mgu_var_disjoint_sum ≡ mgu_var_disjoint_generic Inl Inr" lemma mgu_var_disjoint_sum_sound: "mgu_var_disjoint_sum s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2" by (rule mgu_var_disjoint_generic_sound) lemma mgu_var_disjoint_sum_complete: fixes σ :: "('f, 'v, 'v + 'w) gsubst" and τ :: "('f, 'w, 'v + 'w) gsubst" assumes unif_disj: "s ⋅ σ = t ⋅ τ" shows "∃μ1 μ2 δ. mgu_var_disjoint_sum s t = Some (μ1, μ2) ∧ σ = μ1 ∘⇩_{s}δ ∧ τ = μ2 ∘⇩_{s}δ ∧ s ⋅ μ1 = t ⋅ μ2" by (rule mgu_var_disjoint_generic_complete[OF _ _ _ unif_disj], auto simp: inj_on_def) lemma mgu_var_disjoint_sum_instance: fixes σ :: "('f, 'v) subst" and δ :: "('f, 'v) subst" assumes unif_disj: "s ⋅ σ = t ⋅ δ" shows "∃μ1 μ2 τ. mgu_var_disjoint_sum s t = Some (μ1, μ2) ∧ σ = μ1 ∘⇩_{s}τ ∧ δ = μ2 ∘⇩_{s}τ ∧ s ⋅ μ1 = t ⋅ μ2" proof - let ?map = "λ m σ v. map_vars_term m (σ v)" let ?m = "?map (Inl :: ('v ⇒ 'v + 'v))" let ?m' = "?map (case_sum (λ x. x) (λ x. x))" from unif_disj have id: "map_vars_term Inl (s ⋅ σ) = map_vars_term Inl (t ⋅ δ)" by simp from mgu_var_disjoint_sum_complete[OF id[unfolded map_vars_term_subst]] obtain μ1 μ2 τ where mgu: "mgu_var_disjoint_sum s t = Some (μ1,μ2)" and σ: "?m σ = μ1 ∘⇩_{s}τ" and δ: "?m δ = μ2 ∘⇩_{s}τ" and unif: "s ⋅ μ1 = t ⋅ μ2" by blast { fix σ :: "('f, 'v) subst" have "?m' (?m σ) = σ" by (simp add: map_vars_term_compose o_def term.map_ident) } note id = this { fix μ :: "('f,'v,'v+'v)gsubst" and τ :: "('f,'v + 'v)subst" have "?m' (μ ∘⇩_{s}τ) = μ ∘⇩_{s}?m' τ" by (rule ext, unfold subst_compose_def, simp add: map_vars_term_subst) } note id' = this from arg_cong[OF σ, of ?m', unfolded id id'] have σ: "σ = μ1 ∘⇩_{s}?m' τ" . from arg_cong[OF δ, of ?m', unfolded id id'] have δ: "δ = μ2 ∘⇩_{s}?m' τ" . show ?thesis by (intro exI conjI, rule mgu, rule σ, rule δ, rule unif) qed subsubsection ‹A variable disjoint unification algorithm without changing the type› text ‹We pass the renaming function as additional argument› definition mgu_vd :: "'v :: infinite renaming2 ⇒ _ ⇒ _" where "mgu_vd r = mgu_var_disjoint_generic (rename_1 r) (rename_2 r)" lemma mgu_vd_sound: "mgu_vd r s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2" unfolding mgu_vd_def by (rule mgu_var_disjoint_generic_sound) lemma mgu_vd_complete: fixes σ :: "('f, 'v :: infinite) subst" and τ :: "('f, 'v) subst" assumes unif_disj: "s ⋅ σ = t ⋅ τ" shows "∃μ1 μ2 δ. mgu_vd r s t = Some (μ1, μ2) ∧ σ = μ1 ∘⇩_{s}δ ∧ τ = μ2 ∘⇩_{s}δ ∧ s ⋅ μ1 = t ⋅ μ2" unfolding mgu_vd_def by (rule mgu_var_disjoint_generic_complete[OF rename_12 unif_disj]) end