(* (C) Copyright Andreas Viktor Hess, DTU, 2015-2018 All Rights Reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: - Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. - Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. - Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* Based on src/HOL/ex/Unification.thy packaged with Isabelle/HOL 2015 having the following license: ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. Copyright (c) 1986-2015, University of Cambridge, Technische Universitaet Muenchen, and contributors. All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. * Neither the name of the University of Cambridge or the Technische Universitaet Muenchen nor the names of their contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* Title: Unification.thy Author: Andreas Viktor Hess, DTU Originally based on src/HOL/ex/Unification.thy (Isabelle/HOL 2015) by: Author: Martin Coen, Cambridge University Computer Laboratory Author: Konrad Slind, TUM & Cambridge University Computer Laboratory Author: Alexander Krauss, TUM These theories depend on the IsaFoR library v2.27 (licensed under the LGPLv3) available at: http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/23ac5f5c26ed Download into the directory IsaFoR and move it to your Isabelle installation or change the path in the imports. *) section {* Theory: Substitution and Unification *} theory Unification2 imports Messages "~~/IsaFoR/thys/Rewriting/Unification" (* Path to IsaFoR *) begin subsection {* Substitutions *} abbreviation subst_more_general_than (infixl "\\<^sub>\" 50) where "\ \\<^sub>\ \' \ \\. \' = \ \\<^sub>s \" abbreviation subst_support (infix "supports" 50) where "\ supports \ \ (\x. \ x \ \ = \ x)" abbreviation rm_var where "rm_var v s \ s(v := Var v)" abbreviation rm_vars where "rm_vars vs \ \ (\v. if v \ vs then Var v else \ v)" definition elim where "elim \ v \ \t. v \ FV (t \ \)" definition Idem where "Idem s \ s \\<^sub>s s = s" declare elim_def[simp] lemma subst_support_def: "\ supports \ \ \ = \ \\<^sub>s \" unfolding subst_compose_def by metis lemma subst_supportD: "\ supports \ \ \ \\<^sub>\ \" using assms subst_support_def by auto lemma rm_vars_empty: "rm_vars {} s = s" by simp lemma rm_vars_singleton: "rm_vars {v} s = rm_var v s" by auto lemma var_subst_id: "t \ Var = t" by (induct t) (auto simp add: map_idI) lemma var_subst_id_set: "M \set Var = M" by simp lemma subst_agreement: "(t \ r = t \ s) \ (\v \ FV t. Var v \ r = Var v \ s)" by (induct t) auto lemma repl_invariance[dest?]: "v \ FV t \ t \ s(v := u) = t \ s" by (simp add: subst_agreement) lemma subst_remove_var: "v \ FV s \ v \ FV (t \ Var(v := s))" by (induct t) simp_all lemma subst_set_map: "x \ set X \ x \ s \ set (map (\x. x \ s) X)" by simp lemma subst_all_member: "x \ M \ x \ \ \ (M \set \)" by simp lemma subst_all_union: "(M \ N) \set \ = (M \set \) \ (N \set \)" by auto lemma subst_allE: assumes "t \ M \set s" obtains t' where "t' \ M" "t = t' \ s" using assms by (rule imageE) lemma subst_mono: "t \ u \ t \ s \ u \ s" by (induct u) auto lemma subst_mono_neq: assumes "t \ u" shows "t \ s \ u \ s" proof (cases u) case (Var v) hence False using \t \ u\ by simp thus ?thesis .. next case (Fun f X) then obtain x where "x \ set X" "t \ x" using \t \ u\ by auto hence "t \ s \ x \ s" using subst_mono by simp obtain Y where "Fun f X \ s = Fun f Y" by auto hence "x \ s \ set Y" using \x \ set X\ by auto hence "x \ s \ Fun f X \ s" using \Fun f X \ s = Fun f Y\ Fun_param_is_subterm by simp hence "t \ s \ Fun f X \ s" using \t \ s \ x \ s\ by (metis subtermeq_subterm_trans) thus ?thesis using \u = Fun f X\ \t \ u\ by metis qed lemma subst_no_occs[dest]: "\Var v \ t \ t \ Var(v := s) = t" by (induct t) (simp_all add: map_idI) lemma var_comp[simp]: "\ \\<^sub>s Var = \" "Var \\<^sub>s \ = \" unfolding subst_compose_def by simp_all lemma subst_comp[simp]: "t \ (r \\<^sub>s s) = t \ r \ s" unfolding subst_compose_def by (induct t) auto lemma subst_comp_all: "M \set (\ \\<^sub>s \) = (M \set \) \set \" using subst_comp[of _ \ \] by auto lemma subst_all_mono: "M \ M' \ M \set s \ M' \set s" by auto lemma subst_ground_ident[dest?]: "FV t = {} \ t \ s = t" by (induct t, simp, metis subst_agreement empty_iff var_subst_id) lemma subst_all_ground_ident[dest?]: "ground M \ M \set s = M" proof - assume "ground M" hence "\t. t \ M \ FV t = {}" unfolding ground_def FV\<^sub>s\<^sub>e\<^sub>t_def by auto hence "\t. t \ M \ t \ s = t" by (metis subst_ground_ident) moreover have "\t. t \ M \ t \ s \ M \set s" by (metis subst_all_member) ultimately show "M \set s = M" by (simp add: image_cong) qed lemma subst_eqI[intro]: "(\t. t \ \ = t \ \) \ \ = \" proof - assume "\t. t \ \ = t \ \" hence "\v. Var v \ \ = Var v \ \" by auto thus "\ = \" by auto qed lemma comp_assoc: "(a \\<^sub>s b) \\<^sub>s c = a \\<^sub>s (b \\<^sub>s c)" by auto lemma subst_cong: "\\ = \'; \ = \'\ \ (\ \\<^sub>s \) = (\' \\<^sub>s \')" by auto lemma subst_mgt_bot[simp]: "Var \\<^sub>\ \" by simp lemma subst_mgt_refl[simp]: "\ \\<^sub>\ \" by (metis var_comp(1)) lemma subst_mgt_trans: "\\ \\<^sub>\ \; \ \\<^sub>\ \\ \ \ \\<^sub>\ \" by (metis comp_assoc) lemma subst_mgt_comp: "\ \\<^sub>\ \ \\<^sub>s \" by auto lemma subst_mgt_comp': "\ \\<^sub>s \ \\<^sub>\ \ \ \ \\<^sub>\ \" using comp_assoc by metis lemma var_self: "(\w. if w = v then Var v else Var w) = Var" using subst_agreement by auto lemma var_same[simp]: "Var(v := t) = Var \ t = Var v" by (intro iffI, metis fun_upd_same, simp add: var_self) lemma subst_eq_if_eq_vars: "(\v. (Var v) \ \ = (Var v) \ \) \ \ = \" by (auto simp add: subst_agreement) lemma subst_all_empty[simp]: "{} \set \ = {}" by simp lemma subst_all_insert:"(insert t M) \set \ = insert (t \ \) (M \set \)" by auto lemma subst_apply_FV_subset: "FV t \ V \ FV (t \ \) \ FV\<^sub>s\<^sub>e\<^sub>t (\ ` V)" unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by (induct t) auto lemma subst_apply_FV_unfold: "FV (t \ \) = FV\<^sub>s\<^sub>e\<^sub>t (\ ` FV t)" by (induct t) auto lemma subst_apply_FV_unfold': "FV (t \ \) = (\v \ FV t. FV (\ v))" by (simp add: subst_apply_FV_unfold) lemma subst_apply_FV_union: "FV\<^sub>s\<^sub>e\<^sub>t (\ ` V) \ FV (t \ \) = FV\<^sub>s\<^sub>e\<^sub>t (\ ` (V \ FV t))" proof - have "FV\<^sub>s\<^sub>e\<^sub>t (\ ` (V \ FV t)) = FV\<^sub>s\<^sub>e\<^sub>t (\ ` V) \ FV\<^sub>s\<^sub>e\<^sub>t (\ ` FV t)" by auto thus ?thesis using subst_apply_FV_unfold by metis qed lemma elimI[intro]: "(\t. v \ FV (t \ \)) \ elim \ v" by auto lemma elim_intro'[intro]: "(\w. v \ FV (Var w \ \)) \ elim \ v" by (simp add: subst_apply_FV_unfold') lemma elim_dest[dest]: "elim \ v \ v \ FV (t \ \)" by auto lemma elim_dest'[dest]: "elim \ v \ \ v \ Var v" by (metis elim_def subst_apply_term.simps(1) term.set_intros(3)) lemma elim_dest''[dest]: "elim \ v \ v \ FV (\ w)" by (metis elim_def subst_apply_term.simps(1)) lemma elim_rm_vars_dest[dest]: "elim (\::('a,'b) subst) v \ v \ vs \ elim (rm_vars vs \) v" proof - assume assms: "elim \ v" "v \ vs" obtain f::"('a, 'b) subst \ 'b \ 'b" where "\\ v. (\w. v \ FV (Var w \ \)) = (v \ FV (Var (f \ v) \ \))" by moura hence *: "\a \. a \ FV (Var (f \ a) \ \) \ elim \ a" by blast have "Var (f (rm_vars vs \) v) \ \ \ Var (f (rm_vars vs \) v) \ rm_vars vs \ \ v \ FV (Var (f (rm_vars vs \) v) \ rm_vars vs \)" using assms(1) by fastforce moreover { assume "Var (f (rm_vars vs \) v) \ \ \ Var (f (rm_vars vs \) v) \ rm_vars vs \" hence "rm_vars vs \ (f (rm_vars vs \) v) \ \ (f (rm_vars vs \) v)" by auto hence "f (rm_vars vs \) v \ vs" by meson hence ?thesis using * assms(2) by force } ultimately show ?thesis using * by blast qed lemma occs_elim: "\Var v \ t \ elim (Var(v := t)) v \ (Var(v := t)) = Var" proof (cases "Var v = t") assume "Var v \ t" "\Var v \ t" hence "v \ FV t" by (simp add: vars_iff_subterm_or_eq) thus ?thesis by (auto simp add: subst_remove_var) qed auto lemma occs_elim': "\Var v \ t \ elim (Var(v := t)) v" proof - assume "\Var v \ t" hence "v \ FV t" by (auto simp add: vars_iff_subterm_or_eq) thus "elim (Var(v := t)) v" by (simp add: subst_remove_var) qed lemma elim_comp: "elim \ v \ elim (\ \\<^sub>s \) v" by auto lemma var_Idem: "Idem Var" by (simp add: Idem_def) lemma var_upd_Idem: assumes "\Var v \ t" shows "Idem (Var(v := t))" unfolding Idem_def proof let ?\ = "Var(v := t)" from assms have t_\_id: "t \ ?\ = t" by blast fix s show "s \ (?\ \\<^sub>s ?\) = s \ ?\" unfolding subst_compose_def by (induction s, metis t_\_id fun_upd_def subst_apply_term.simps(1), simp) qed subsection {* Domain and image of substitutions *} definition dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \ 'v set" where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ {v. s v \ Var v}" definition img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \ ('f,'v) terms" where "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ s ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" abbreviation FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \ 'v set" where "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" declare dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def[simp] lemma subst_dom_var_empty[simp]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var = {}" by simp lemma subst_dom_var_finite[simp]: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var)" by simp lemma finite_subst_img_if_finite_dom: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ finite (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma finite_subst_img_if_finite_dom': "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ finite (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_img_alt_def: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {t. \v. s v = t \ t \ Var v}" using img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_FV_img_alt_def: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = (\t \ {t. \v. s v = t \ t \ Var v}. FV t)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_domI[intro]: "\ v \ Var v \ v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by simp lemma subst_imgI[intro]: "\ v \ Var v \ \ v \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp lemma subst_FV_imgI[intro]: "\ v \ Var v \ FV (\ v) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_FV_dom_img_subset: "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (t \ \) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (induct t) auto lemma subst_FV_dom_img_subset_set: "FV\<^sub>s\<^sub>e\<^sub>t M \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>e\<^sub>t (M \set \) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - assume assms: "FV\<^sub>s\<^sub>e\<^sub>t M \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" obtain f::"'a set \ (('b, 'a) term \ 'a set) \ ('b, 'a) terms \ ('b, 'a) term" where "\x y z. (\v. v \ z \ \ y v \ x) \ (f x y z \ z \ \ y (f x y z) \ x)" by moura hence *: "\T g A. (\ UNION T g \ A \ (\t. t \ T \ g t \ A)) \ (UNION T g \ A \ f A g T \ T \ \ g (f A g T) \ A)" by (metis (no_types) SUP_le_iff) hence **: "\t. t \ M \ FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (metis (no_types) assms FV\<^sub>s\<^sub>e\<^sub>t_def) have "\t::('b, 'a) term. \f T. t \ f ` T \ (\t'::('b, 'a) term. t = f t' \ t' \ T)" by blast hence "f (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) FV (M \set \) \ M \set \ \ FV (f (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) FV (M \set \)) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (metis (full_types) ** subst_FV_dom_img_subset) thus ?thesis by (metis (no_types) * FV\<^sub>s\<^sub>e\<^sub>t_def) qed lemma subst_FV_dom_ground_if_ground_img: assumes "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" shows "FV (t \ s) = {}" using subst_FV_dom_img_subset[OF assms(1)] assms(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force lemma subst_FV_dom_ground_if_ground_img': assumes "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "\x. x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ FV (s x) = {}" shows "FV (t \ s) = {}" using subst_FV_dom_ground_if_ground_img[OF assms(1)] assms(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_FV_unfold: "FV (t \ s) = (FV t - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \ FV\<^sub>s\<^sub>e\<^sub>t (s ` (FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s))" proof (induction t) case (Var v) thus ?case proof (cases "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s") case False hence "FV (Var v \ s) = {v}" "FV (Var v) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}" by auto thus ?thesis by auto qed auto qed auto lemma subst_FV_unfold_ground_img: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {} \ FV (t \ s) = FV t - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" using assms subst_FV_unfold[of t s] by auto lemma subst_img_update: "\\ v = Var v; t \ Var v\ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t" proof - assume "\ v = Var v" "t \ Var v" hence "(\s \ {s. \w. (\(v := t)) w = s \ s \ Var w}. FV s) = FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto thus "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t" by (metis Un_commute subst_FV_img_alt_def) qed lemma subst_dom_update1: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := Var v)) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto lemma subst_dom_update2: "t \ Var v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by auto lemma subst_dom_update3: "t = Var v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ - {v}" by auto lemma var_not_in_subst_dom[elim]: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ s v = Var v" by simp lemma subst_dom_vars_in_subst[elim]: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ s v \ Var v" by simp lemma subst_not_dom_fixed: "\v \ FV t; v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ \ v \ FV (t \ s)" by (induct t) auto lemma subst_not_img_fixed: "\v \ FV (t \ s); v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ \ v \ FV t" by (induct t) force+ lemma ground_subst_no_var[intro]: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \ x \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by simp lemma subst_Var_notin_img: "x \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ t \ s = Var x \ t = Var x" using subst_not_img_fixed[of x t s] by (induct t) auto lemma FV_in_subst_img: "\s v = t; t \ Var v\ \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma empty_dom_iff_empty_subst: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ \ = Var" by auto lemma subst_dom_cong: "(\v t. \ v = t \ \ v = t) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto lemma subst_img_cong: "(\v t. \ v = t \ \ v = t) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_dom_elim: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {} \ FV (t \ s) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}" proof (induction t) case (Var v) thus ?case using FV_in_subst_img[of s] by (cases "s v = Var v") auto qed auto lemma subst_dom_insert_finite: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) = finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))" proof assume "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)) \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" by auto thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))" by (meson \finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)\ finite_insert rev_finite_subset) next assume *: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))" hence "finite (insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s))" proof (cases "t = Var v") case True hence "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s - {v})" by (metis * subst_dom_update3) thus ?thesis by simp qed (metis * subst_dom_update2[of t v s]) thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" by simp qed lemma trm_subst_disj: "t \ \ = t \ FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" proof (induction t) case (Fun f X) hence "map (\x. x \ \) X = X" by simp hence "\x. x \ set X \ x \ \ = x" using map_eq_conv by fastforce thus ?case using Fun.IH by auto qed simp lemma trm_subst_ident[intro]: "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ t \ \ = t" proof - assume "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" hence "\v \ FV t. \w \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. v \ w" by auto thus ?thesis by (metis subst_agreement subst_apply_term.simps(1) var_subst_id subst_domI) qed lemma trm_subst_ident'[intro]: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (Var v) \ \ = Var v" using trm_subst_ident by simp lemma trm_subst_ident''[intro]: "(\x. x \ FV t \ \ x = Var x) \ t \ \ = t" proof - assume "\x. x \ FV t \ \ x = Var x" hence "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by auto thus ?thesis using trm_subst_ident by auto qed lemma set_subst_ident: "FV\<^sub>s\<^sub>e\<^sub>t M \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ M \set \ = M" proof - assume "FV\<^sub>s\<^sub>e\<^sub>t M \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" hence "\t \ M. t \ \ = t" unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by blast thus ?thesis by force qed lemma set_subst_all_ident: "FV\<^sub>s\<^sub>e\<^sub>t (M \set \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ M \set (\ \\<^sub>s \) = M \set \" by (metis set_subst_ident subst_comp_all) lemma rm_vars_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s - V" by auto lemma rm_vars_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) = s ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma rm_vars_img_subset: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma rm_vars_apply: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) \ (rm_vars V s) v = s v" by auto lemma rm_vars_apply': "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vs = {} \ rm_vars vs \ = \" by force lemma rm_vars_ident: "FV t \ vs = {} \ t \ (rm_vars vs \) = t \ \" by (induct t) auto lemma rm_vars_ground_supports: assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" shows "rm_vars X \ supports \" proof fix x have *: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \))" using rm_vars_img_subset[of X \] assms by auto show "rm_vars X \ x \ \ = \ x " proof (cases "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \)") case True hence "FV (rm_vars X \ x) = {}" using * unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto thus ?thesis using True by auto qed simp qed lemma subst_apply_dom_ident: "t \ \ = t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ t \ \ = t" proof (induction t) case (Fun f T) thus ?case by (induct T) auto qed auto lemma rm_vars_subst_apply_ident: assumes "t \ \ = t" shows "t \ (rm_vars vs \) = t" using rm_vars_dom[of vs \] subst_apply_dom_ident[OF assms, of "rm_vars vs \"] by auto lemma rm_vars_comp: assumes "FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ vs = {}" shows "t \ rm_vars vs (\ \\<^sub>s \) = t \ (rm_vars vs \ \\<^sub>s rm_vars vs \)" using assms proof (induction t) case (Var x) thus ?case proof (cases "x \ vs") case False have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars vs \) \ vs = {}" by auto moreover have "FV (\ x) \ vs = {}" using Var False by force ultimately have "\ x \ (rm_vars vs \) = \ x \ \" using rm_vars_ident by simp moreover have "(rm_vars vs (\ \\<^sub>s \)) x = (\ \\<^sub>s \) x" by (metis False) ultimately show ?thesis using subst_compose by auto qed auto qed auto lemma disj_dom_img_var_notin: assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "\ v = t" "t \ Var v" shows "v \ FV t" "\v \ FV (t \ \). v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - have "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using FV_in_subst_img[of \ v t, OF assms(2)] assms(2,3) by simp_all thus "v \ FV t" using assms(1) by auto have *: "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using assms(1) \FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ by auto hence "t \ \ = t" by blast thus "\v \ FV (t \ \). v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using * by auto qed lemma subst_sends_dom_to_img: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (Var v \ \) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_sends_FV_to_img: "FV (t \ s) \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" proof (induction t) case (Var v) thus ?case proof (cases "Var v \ s = Var v") case False hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by (meson trm_subst_ident') hence "FV (Var v \ s) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" using subst_sends_dom_to_img by simp thus ?thesis by auto qed simp qed auto lemma ident_comp_subst_trm_if_disj: assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "(\ \\<^sub>s \) v = \ v" proof - from assms have " dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (\ v) = {}" using FV_in_subst_img by fastforce thus "(\ \\<^sub>s \) v = \ v" unfolding subst_compose_def by blast qed lemma ident_comp_subst_trm_if_disj': "FV (\ v) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ (\ \\<^sub>s \) v = \ v" unfolding subst_compose_def by blast lemma IdemI[intro]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ Idem \" using ident_comp_subst_trm_if_disj[of \ \] var_not_in_subst_dom[of _ \] subst_eq_if_eq_vars[of \] by (metis Idem_def subst_compose_def var_comp(2)) lemma IdemI'[intro]: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ Idem \" unfolding ground_def by auto lemma IdemE: "Idem \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" proof - assume "Idem \" hence "\v. FV (\ v) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" unfolding Idem_def subst_compose_def by (metis trm_subst_disj) thus ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto qed lemma Idem_rm_vars: "Idem \ \ Idem (rm_vars X \)" proof - assume "Idem \" hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by (metis IdemE) moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately show ?thesis by (fastforce intro!: IdemI) qed lemma subst_FV_bounded_if_img_bounded: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t \ V \ FV (t \ \) \ FV t \ V" proof (induction t) case (Var v) thus ?case by (cases "\ v = Var v") auto qed (metis (no_types, lifting) Un_assoc Un_commute subst_sends_FV_to_img sup.absorb_iff2) lemma subst_FV_bound_singleton: "FV (t \ Var(v := t')) \ FV t \ FV t'" using subst_FV_bounded_if_img_bounded[of "Var(v := t')" t "FV t'"] unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma subst_FV_bounded_if_img_bounded': assumes "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>e\<^sub>t M" shows "FV\<^sub>s\<^sub>e\<^sub>t (M \set \) \ FV\<^sub>s\<^sub>e\<^sub>t M" proof fix v assume *: "v \ FV\<^sub>s\<^sub>e\<^sub>t (M \set \)" obtain t where t: "t \ M" "t \ \ \ M \set \" "v \ FV (t \ \)" proof - assume **: "\t. \t \ M; t \ \ \ M \set \; v \ FV (t \ \)\ \ thesis" have "v \ UNION ((\t. t \ \) ` M) FV" using * unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by metis hence "\t. t \ M \ v \ FV (t \ \)" by blast thus ?thesis using ** subst_all_member by blast qed from \t \ M\ obtain M' where "t \ M'" "M = insert t M'" by (meson Set.set_insert) hence "FV\<^sub>s\<^sub>e\<^sub>t M = FV t \ FV\<^sub>s\<^sub>e\<^sub>t M'" by simp hence "FV (t \ \) \ FV\<^sub>s\<^sub>e\<^sub>t M" using subst_FV_bounded_if_img_bounded assms by simp thus "v \ FV\<^sub>s\<^sub>e\<^sub>t M" using assms \v \ FV (t \ \)\ by auto qed lemma ground_img_if_ground_subst: "(\v t. s v = t \ FV t = {}) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma ground_subst_FV_subset: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ FV (t \ \) \ FV t" using subst_FV_bounded_if_img_bounded by fastforce lemma ground_subst_FV_subset': "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>e\<^sub>t (M \set \) \ FV\<^sub>s\<^sub>e\<^sub>t M" using subst_FV_bounded_if_img_bounded'[of \ M] unfolding ground_def by auto lemma subst_to_var_is_var[elim]: "t \ s = Var v \ \w. t = Var w" using subst_apply_term.elims by blast lemma subst_dom_comp_subset[simp]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" unfolding subst_compose_def by auto lemma subst_dom_comp_eq: assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof (rule ccontr) assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using subst_dom_comp_subset[of \ \] by simp then obtain v where "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto hence v_in_some_subst: "\ v \ Var v \ \ v \ Var v" and "\ v \ \ = Var v" unfolding subst_compose_def by auto then obtain w where "\ v = Var w" using subst_to_var_is_var by fastforce show False proof (cases "v = w") case True hence "\ v = Var v" using \\ v = Var w\ by simp hence "\ v \ Var v" using v_in_some_subst by simp thus False using \\ v = Var v\ \\ v \ \ = Var v\ by simp next case False hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using v_in_some_subst \\ v \ \ = Var v\ by auto hence "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using assms by auto moreover have "\ w = Var v" using \\ v \ \ = Var v\ \\ v = Var w\ by simp hence "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \v \ w\ subst_FV_imgI[of \ w] by simp ultimately show False .. qed qed lemma subst_img_comp_subset[simp]: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" proof let ?img = "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t" fix x assume "x \ ?img (\1 \\<^sub>s \2)" then obtain v t where vt: "x \ FV t" "t = (\1 \\<^sub>s \2) v" "t \ Var v" unfolding subst_compose_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto { assume "x \ ?img \1" hence "x \ ?img \2" by (metis (no_types, hide_lams) FV_in_subst_img Un_iff subst_compose_def vt subsetCE subst_apply_term.simps(1) subst_sends_FV_to_img) } thus "x \ ?img \1 \ ?img \2" by auto qed lemma subst_img_comp_subset': assumes "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" shows "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 \ (\t' \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1. t = t' \ \2)" proof - obtain x where x: "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" "(\1 \\<^sub>s \2) x = t" "t \ Var x" using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto { assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1" hence "(\1 \\<^sub>s \2) x = \2 x" unfolding subst_compose_def by auto hence ?thesis using x by auto } moreover { assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1" hence ?thesis using subst_compose x(2) by fastforce } ultimately show ?thesis by metis qed lemma subst_img_comp_subset_const: assumes "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" shows "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 \ Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ (\x. Var x \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ \2 x = Fun c [])" proof (cases "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2") case False then obtain t where t: "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1" "Fun c [] = t \ \2" using subst_img_comp_subset'[OF assms] by auto thus ?thesis by (cases t) auto qed (simp add: subst_img_comp_subset'[OF assms]) lemma subst_img_comp_subset_const': fixes \ \::"('f,'v) subst" assumes "(\ \\<^sub>s \) x = Fun c []" shows "\ x = Fun c [] \ (\z. \ x = Var z \ \ z = Fun c [])" proof (cases "\ x = Fun c []") case False then obtain t where "\ x = t" "t \ \ = Fun c []" using assms unfolding subst_compose_def by auto thus ?thesis by (cases t) auto qed simp lemma subst_FV_dom_img_single: assumes "v \ FV t" "\ v = t" "\w. v \ w \ \ w = Var w" shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {v}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = FV t" proof - show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {v}" using assms by fastforce have "FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (metis FV_in_subst_img assms(1,2) vars_iff_subterm_or_eq) moreover have "\v. \ v \ Var v \ \ v = t" using assms by fastforce ultimately show "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = FV t" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto qed lemma subst_comp_upd1: "\(v := t) \\<^sub>s \ = (\ \\<^sub>s \)(v := t \ \)" unfolding subst_compose_def by auto lemma subst_comp_upd2: assumes "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" shows "s(v := t) = s \\<^sub>s (Var(v := t))" unfolding subst_compose_def proof - { fix w have "(s(v := t)) w = s w \ Var(v := t)" proof (cases "w = v") case True hence "s w = Var w" using \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ by simp thus ?thesis using \w = v\ by simp next case False hence "(s(v := t)) w = s w" by simp moreover have "s w \ Var(v := t) = s w" using \w \ v\ \v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ by (metis FV_in_subst_img fun_upd_apply insert_absorb insert_subset repl_invariance subst_apply_term.simps(1) var_subst_id) ultimately show ?thesis .. qed } thus "s(v := t) = (\w. s w \ Var(v := t))" by auto qed lemma ground_subst_dom_iff_img: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ x \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using assms by auto lemma finite_dom_subst_exists: "finite S \ \\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S" proof (induction S rule: finite.induct) case (insertI A a) then obtain \::"('f,'v) subst" where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = A" by blast fix f::'f have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(a := Fun f [])) = insert a A" using \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = A\ by auto thus ?case by metis qed auto lemma subst_inj_is_bij_betw_dom_img_if_ground_img: assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" shows "inj \ \ bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" (is "?A \ ?B") proof show "?A \ ?B" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (meson bij_betw_def injD inj_onI) next assume ?B hence "inj_on \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" unfolding bij_betw_def by auto moreover have "\x. x \ UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ x = Var x" by auto hence "inj_on \ (UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using inj_onI[of "UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \"] by (metis term.inject(1)) moreover have "\x y. x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ x \ \ y" using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately show ?A by (metis injI inj_onD subst_domI term.inject(1)) qed lemma bij_finite_ground_subst_exists: assumes "finite (S::'v set)" "infinite (U::('f,'v) term set)" "ground U" shows "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S \ bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ U" proof - obtain T' where "T' \ U" "card T' = card S" "finite T'" by (meson assms(2) finite_Diff2 infinite_arbitrarily_large) then obtain f::"'v \ ('f,'v) term" where f_bij: "bij_betw f S T'" using finite_same_card_bij[OF assms(1)] by metis hence *: "\v. v \ S \ f v \ Var v" using \ground U\ \T' \ U\ bij_betwE by fastforce let ?\ = "\v. if v \ S then f v else Var v" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S" proof show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ \ S" by auto { fix v assume "v \ S" "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\" hence "f v = Var v" by simp hence False using *[OF \v \ S\] by metis } thus "S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\" by blast qed hence "\v w. \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\; w \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\\ \ ?\ w \ ?\ v" using \ground U\ bij_betwE[OF f_bij] set_rev_mp[OF _ \T' \ U\] unfolding ground_def FV\<^sub>s\<^sub>e\<^sub>t_def by (metis (no_types, lifting) UN_iff empty_iff vars_iff_subterm_or_eq) hence "inj_on ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" using f_bij \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S\ unfolding bij_betw_def inj_on_def by metis hence "bij_betw ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\] by simp moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = T'" using \bij_betw f S T'\ \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S\ unfolding bij_betw_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ \ U" using \T' \ U\ by auto ultimately show ?thesis using \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S\ by (metis (lifting)) qed lemma bij_finite_const_subst_exists: assumes "finite (S::'v set)" "finite (T::'f set)" "infinite (U::'f set)" shows "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S \ bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\c. Fun c []) ` (U - T)" proof - obtain T' where "T' \ U - T" "card T' = card S" "finite T'" by (meson assms(2,3) finite_Diff2 infinite_arbitrarily_large) then obtain f::"'v \ 'f" where f_bij: "bij_betw f S T'" using finite_same_card_bij[OF assms(1)] by metis let ?\ = "\v. if v \ S then Fun (f v) [] else Var v" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S" by simp moreover have "\v w. \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\; w \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\\ \ ?\ w \ ?\ v" by auto hence "inj_on ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" using f_bij unfolding bij_betw_def inj_on_def by (metis \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S\ term.inject(2)) hence "bij_betw ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\] by simp moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = ((\c. Fun c []) ` T')" using \bij_betw f S T'\ unfolding bij_betw_def inj_on_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ \ ((\c. Fun c []) ` (U - T))" using \T' \ U - T\ by auto ultimately show ?thesis by (metis (lifting)) qed lemma bij_finite_const_subst_exists': assumes "finite (S::'v set)" "finite (T::('f,'v) terms)" "infinite (U::'f set)" shows "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S \ bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ((\c. Fun c []) ` U) - T" proof - have "finite (\(funs_term ` T))" using assms(2) by auto then obtain \ where \: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S" "bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\c. Fun c []) ` (U - (\(funs_term ` T)))" using bij_finite_const_subst_exists[OF assms(1) _ assms(3)] by blast moreover have "(\c. Fun c []) ` (U - (\(funs_term ` T))) \ ((\c. Fun c []) ` U) - T" by auto ultimately show ?thesis by blast qed lemma bij_betw_countably_infinite: assumes "countable (S::'a set)" "infinite S" and "countable (T::'b set)" "infinite T" obtains f::"'a \ 'b" where "bij_betw f S T" proof - have "bij_betw (to_nat_on S) S UNIV" by (fact to_nat_on_infinite[OF assms(1,2)]) moreover have "bij_betw (from_nat_into T) UNIV T" by (fact bij_betw_from_nat_into[OF assms(3,4)]) ultimately have "bij_betw (from_nat_into T \ to_nat_on S) S T" by (simp add: bij_betw_trans) thus "(\f. bij_betw f S T \ thesis) \ thesis" .. qed lemma bij_betw_iteI: assumes "bij_betw f A B" "bij_betw g C D" "A \ C = {}" "B \ D = {}" shows "bij_betw (\x. if x \ A then f x else g x) (A \ C) (B \ D)" proof - have "bij_betw (\x. if x \ A then f x else g x) A B" "bij_betw (\x. if x \ A then f x else g x) C D" apply (metis bij_betw_cong[of A f "\x. if x \ A then f x else g x" B] assms(1)) using bij_betw_cong[of C g "\x. if x \ A then f x else g x" D] assms(2,3) by force thus ?thesis using bij_betw_combine[OF _ _ assms(4)] by metis qed lemma bij_countable_infinite_nonvar_subst_exists: assumes "countable (S::'v set)" "infinite S" and "countable (T::('f,'v) term set)" "infinite T" and nonvar: "\x. Var x \ T" obtains \::"('f,'v) subst" where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = T" "bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" proof - obtain f::"'v \ ('f,'v) term" where f_bij: "bij_betw f S T" by (fact bij_betw_countably_infinite[OF assms(1,2,3,4)]) hence f_nonvar: "\x y. x \ S \ f x \ Var y" using nonvar unfolding bij_betw_def by force let ?\ = "\v. if v \ S then f v else Var v" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S" using f_nonvar by simp moreover have "\v w. \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\; w \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\\ \ ?\ w \ ?\ v" using f_nonvar by auto hence "inj_on ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" using f_bij unfolding bij_betw_def inj_on_def by (metis \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = S\) hence "bij_betw ?\ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\] by simp moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = T" using f_bij f_nonvar unfolding bij_betw_def inj_on_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately show thesis using that by (metis (lifting)) qed lemma bij_countable_infinite_const_subst_exists: assumes "countable (S::'v set)" "infinite S" and "countable (T::'f set)" "infinite T" shows "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = S \ bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = (\c. Fun c []) ` T" proof - from assms(3,4) have *: "countable ((\c. Fun c []) ` T)" "infinite ((\c. Fun c []) ` T)" using finite_imageD unfolding inj_on_def by (blast, auto) show ?thesis by (blast intro: bij_countable_infinite_nonvar_subst_exists[OF assms(1,2) *]) qed lemma subst_comp_split: assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" shows "\ = (rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ - V) \) \\<^sub>s (rm_vars V \)" (is ?P) and "\ = (rm_vars V \) \\<^sub>s (rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ - V) \)" (is ?Q) proof - let ?rm1 = "rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ - V) \" and ?rm2 = "rm_vars V \" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 = {}" using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+ hence *: "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \ (?rm1 \\<^sub>s ?rm2) v = \ v" "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \ (?rm2 \\<^sub>s ?rm1) v = \ v" using ident_comp_subst_trm_if_disj[of ?rm2 ?rm1] ident_comp_subst_trm_if_disj[of ?rm1 ?rm2] by auto hence "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \ (?rm1 \\<^sub>s ?rm2) v = \ v" "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \ (?rm2 \\<^sub>s ?rm1) v = \ v" unfolding subst_compose_def by auto hence "\v. (?rm1 \\<^sub>s ?rm2) v = \ v" "\v. (?rm2 \\<^sub>s ?rm1) v = \ v" using * by blast+ thus ?P ?Q by auto qed lemma subst_comp_eq_if_disjoint_vars: assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) = {}" shows "\ \\<^sub>s \ = \ \\<^sub>s \" proof - { fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "(\ \\<^sub>s \) x = \ x" "(\ \\<^sub>s \) x = \ x" using assms by (force simp add: subst_compose)+ hence "(\ \\<^sub>s \) x = (\ \\<^sub>s \) x" by metis } moreover { fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "(\ \\<^sub>s \) x = \ x" "(\ \\<^sub>s \) x = \ x" using assms by (auto simp add: subst_compose) hence "(\ \\<^sub>s \) x = (\ \\<^sub>s \) x" by metis } moreover { fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "(\ \\<^sub>s \) x = (\ \\<^sub>s \) x" by (simp add: subst_compose) } ultimately show ?thesis by auto qed lemma subst_eq_if_disjoint_vars_ground: fixes \ \::"('f,'v) subst" assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" shows "t \ \ \ \ = t \ \ \ \" by (metis assms ground_def subst_comp_eq_if_disjoint_vars subst_compose_apply_term_distrib sup_bot.right_neutral) lemma subst_img_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (t \ \)" proof - assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t" hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t" by blast thus ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (metis (no_types) le_iff_sup subst_apply_FV_unfold subst_apply_FV_union) qed lemma subst_all_FV_subset: "FV t \ FV\<^sub>s\<^sub>e\<^sub>t M \ FV (t \ \) \ FV\<^sub>s\<^sub>e\<^sub>t (M \set \)" proof - assume *: "FV t \ FV\<^sub>s\<^sub>e\<^sub>t M" { fix v assume "v \ FV t" hence "v \ FV\<^sub>s\<^sub>e\<^sub>t M" using * by auto then obtain t' where "t' \ M" "v \ FV t'" by auto hence "FV (\ v) \ FV (t' \ \)" by (metis subst_apply_term.simps(1) subst_apply_FV_subset subst_apply_FV_unfold subtermeq_vars_subset vars_iff_subtermeq) hence "FV (\ v) \ FV\<^sub>s\<^sub>e\<^sub>t (M \set \)" using \t' \ M\ by auto } thus ?thesis by (auto simp add: subst_apply_FV_unfold) qed lemma subst_support_if_mgt_Idem: assumes "\ \\<^sub>\ \" "Idem \" shows "\ supports \" proof - from \\ \\<^sub>\ \\ obtain \ where \: "\ = \ \\<^sub>s \" by blast hence "\v. \ v \ \ = Var v \ (\ \\<^sub>s \ \\<^sub>s \)" by simp hence "\v. \ v \ \ = Var v \ (\ \\<^sub>s \)" using \Idem \ \ unfolding Idem_def by simp hence "\v. \ v \ \ = Var v \ \" using \ by simp thus "\ supports \" by simp qed lemma subst_support_iff_mgt_if_Idem: assumes "Idem \" shows "\ \\<^sub>\ \ \ \ supports \" proof show "\ \\<^sub>\ \ \ \ supports \" by (fact subst_support_if_mgt_Idem[OF _ \Idem \\]) show "\ supports \ \ \ \\<^sub>\ \" by (fact subst_supportD) qed lemma subst_support_comp: fixes \ \ \::"('a,'b) subst" assumes "\ supports \" "\ supports \" shows "(\ \\<^sub>s \) supports \" by (metis (no_types) assms subst_agreement subst_apply_term.simps(1) subst_comp) lemma subst_support_comp': fixes \ \ \::"('a,'b) subst" assumes "\ supports \" shows "\ supports (\ \\<^sub>s \)" "\ supports \ \ \ supports (\ \\<^sub>s \)" using assms unfolding subst_support_def by (metis comp_assoc, metis) lemma subst_support_comp_split: fixes \ \ \::"('a,'b) subst" assumes "(\ \\<^sub>s \) supports \" shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ \ supports \" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ \ supports \" proof - assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" hence "Idem \" by (metis IdemI) have "\ \\<^sub>\ \" using assms comp_assoc[of \ \ \] unfolding subst_compose_def by metis show "\ supports \" using subst_support_if_mgt_Idem[OF \\ \\<^sub>\ \\ \Idem \\] by auto next assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" moreover have "\v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \). (\ \\<^sub>s \) v \ \ = \ v" using assms by metis ultimately have "\v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \ v \ \ = \ v" using var_not_in_subst_dom unfolding subst_compose_def by (metis IntI empty_iff subst_apply_term.simps(1)) thus "\ supports \" by force qed lemma Idem_support: "Idem \ \ \ supports \ \\<^sub>s \" unfolding Idem_def by (metis subst_support_def comp_assoc) lemma Idem_iff_self_support: "Idem \ \ \ supports \" using subst_support_def[of \ \] unfolding Idem_def by auto lemma subterm_subst_neq: "t \ t' \ t \ s \ t' \ s" by (metis subst_mono_neq subterm_def) lemma subterm_subst_unfold: assumes "t \ s \ \" shows "(\s'. s' \ s \ t = s' \ \) \ (\x \ FV s. t \ \ x)" using assms proof (induction s) case (Fun f T) thus ?case proof (cases "t = Fun f T \ \") case True thus ?thesis using Fun by auto next case False then obtain s' where s': "s' \ set T" "t \ s' \ \" using Fun by auto hence "(\s''. s'' \ s' \ t = s'' \ \) \ (\x \ FV s'. t \ \ x)" by (metis Fun.IH) thus ?thesis using s'(1) by auto qed qed simp lemma subterm_subst_img_subterm: assumes "t \ s \ \" "\s'. s' \ s \ t \ s' \ \" shows "\w \ FV s. t \ \ w" using subterm_subst_unfold[OF assms(1)] assms(2) by force lemma subterm_subst_not_img_subterm: assumes "t \ s \ \" "\(\w \ FV s. t \ \ w)" shows "\f T. Fun f T \ s \ t = Fun f T \ \" proof (rule ccontr) assume "\(\f T. Fun f T \ s \ t = Fun f T \ \)" hence "\f T. Fun f T \ s \ t \ Fun f T \ \" by simp moreover have "\x. Var x \ s \ t \ Var x \ \" using assms(2) vars_iff_subtermeq by force ultimately have "\s'. s' \ s \ t \ s' \ \" by (metis "term.exhaust") thus False using assms subterm_subst_img_subterm by force qed lemma subst_apply_img_var: assumes "v \ FV (t \ \)" "v \ FV t" obtains w where "w \ FV t" "v \ FV (\ w)" using assms by (induct t) auto subsection {* Finite Substitutions *} inductive_set fsubst::"('a,'b) subst set" where FVar: "Var \ fsubst" | FUpdate: "\\ \ fsubst; v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; t \ Var v\ \ \(v := t) \ fsubst" lemma finite_dom_iff_fsubst: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ \ \ fsubst" proof assume "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" thus "\ \ fsubst" proof (induction "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" arbitrary: \ rule: finite.induct) case emptyI hence "\ = Var" using empty_dom_iff_empty_subst by metis thus ?case using FVar by simp next case (insertI \'\<^sub>d\<^sub>o\<^sub>m v) thus ?case proof (cases "v \ \'\<^sub>d\<^sub>o\<^sub>m") case True hence "\'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \insert v \'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ by auto thus ?thesis using insertI.hyps(2) by metis next case False let ?\' = "\w. if w \ \'\<^sub>d\<^sub>o\<^sub>m then \ w else Var w" have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\' = \'\<^sub>d\<^sub>o\<^sub>m" using \v \ \'\<^sub>d\<^sub>o\<^sub>m\ \insert v \'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ by auto hence "?\' \ fsubst" using insertI.hyps(2) by simp moreover have "?\'(v := \ v) = (\w. if w \ insert v \'\<^sub>d\<^sub>o\<^sub>m then \ w else Var w)" by auto hence "?\'(v := \ v) = \" using \insert v \'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ by auto ultimately show ?thesis using FUpdate[of ?\' v "\ v"] using False insertI.hyps(3) by auto qed qed next assume "\ \ fsubst" thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by (induct \, simp, metis subst_dom_insert_finite) qed lemma fsubst_induct[case_names FVar FUpdate, induct set: finite]: assumes "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "P Var" and "\\ v t. \finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \); v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; t \ Var v; P \\ \ P (\(v := t))" shows "P \" using assms finite_dom_iff_fsubst fsubst.induct by metis lemma fun_upd_fsubst: "s(v := t) \ fsubst \ s \ fsubst" using subst_dom_insert_finite[of s] finite_dom_iff_fsubst by blast lemma finite_img_if_fsubst: "s \ fsubst \ finite (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" using finite_dom_iff_fsubst finite_subst_img_if_finite_dom' by blast subsection {* Unifiers and Most General Unifiers *} abbreviation Unifier::"('f,'v) subst \ ('f,'v) term \ ('f,'v) term \ bool" where "Unifier \ t u \ (t \ \ = u \ \)" abbreviation MGU::"('f,'v) subst \ ('f,'v) term \ ('f,'v) term \ bool" where "MGU \ t u \ Unifier \ t u \ (\\. Unifier \ t u \ \ \\<^sub>\ \)" lemma MGUI[intro]: shows "\t \ \ = u \ \; \\::('f,'v) subst. t \ \ = u \ \ \ \ \\<^sub>\ \\ \ MGU \ t u" by auto lemma UnifierD[dest]: fixes \::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list" assumes "Unifier \ (Fun f X) (Fun g Y)" shows "f = g" "length X = length Y" proof - from assms show "f = g" by auto from assms have "Fun f X \ \ = Fun g Y \ \" by auto hence "length (map (\x. x \ \) X) = length (map (\x. x \ \) Y)" by auto thus "length X = length Y" by auto qed lemma UnifierD'[dest]: fixes \::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list" assumes "Fun f X \ \ = Fun g Y \ \" shows "f = g" "length X = length Y" using assms UnifierD by simp_all lemma MGUD[dest]: fixes \::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list" assumes "MGU \ (Fun f X) (Fun g Y)" shows "f = g" "length X = length Y" using assms by (auto intro!: UnifierD[of f X \ g Y]) lemma MGU_sym[sym]: "MGU \ s t \ MGU \ t s" by auto lemma Unifier_sym[sym]: "Unifier \ s t \ Unifier \ t s" by auto lemma MGU_nil: "MGU Var s t \ s = t" by fastforce lemma Unifier_comp: "Unifier (\ \\<^sub>s \) t u \ Unifier \ (t \ \) (u \ \)" by simp lemma Unifier_comp': "Unifier \ (t \ \) (u \ \) \ Unifier (\ \\<^sub>s \) t u" by simp lemma Unifier_excludes_subterm: assumes \: "Unifier \ t u" shows "\t \ u" proof assume "t \ u" hence "t \ \ \ u \ \" using subst_mono_neq by simp hence "t \ \ \ u \ \" by simp moreover from \ have "t \ \ = u \ \" by auto ultimately show False .. qed lemma MGU_is_Unifier: "MGU \ t u \ Unifier \ t u" by (rule conjunct1) lemma MGU_Var1: assumes "\Var v \ t" shows "MGU (Var(v := t)) (Var v) t" proof (intro MGUI exI) show "Var v \ (Var(v := t)) = t \ (Var(v := t))" using assms subst_no_occs by fastforce next fix \::"('a,'b) subst" assume th: "Var v \ \ = t \ \" show "\ = (Var(v := t)) \\<^sub>s \" proof fix s show "s \ \ = s \ ((Var(v := t)) \\<^sub>s \)" using th by (induct s) auto qed qed lemma MGU_Var2: "v \ FV t \ MGU (Var(v := t)) (Var v) t" by (metis (no_types) MGU_Var1 vars_iff_subterm_or_eq) lemma MGU_Var3: "MGU Var (Var v) (Var w) \ v = w" by fastforce lemma MGU_Const1: "MGU Var (Fun c []) (Fun d []) \ c = d" by fastforce lemma MGU_Const2: "MGU \ (Fun c []) (Fun d []) \ c = d" by auto lemma MGU_Fun: assumes "MGU \ (Fun f X) (Fun g Y)" shows "f = g" "length X = length Y" proof - let ?F = "\\ X. map (\x. x \ \) X" from assms have "\f = g; ?F \ X = ?F \ Y; \\'. f = g \ ?F \' X = ?F \' Y \ \ \\<^sub>\ \'\ \ length X = length Y" using map_eq_imp_length_eq by auto thus "f = g" "length X = length Y" using assms by auto qed lemma Unifier_Fun: assumes "Unifier \ (Fun f (x#X)) (Fun g (y#Y))" shows "Unifier \ x y" "Unifier \ (Fun f X) (Fun g Y)" using assms by simp_all lemma Unifier_Idem_subst: "Idem r \ Unifier s (t \ r) (u \ r) \ Unifier (r \\<^sub>s s) (t \ r) (u \ r)" by (metis (no_types, lifting) Idem_def subst_comp) lemma Idem_comp: "Idem r \ Unifier s (t \ r) (u \ r) \ (\q. Unifier q (t \ r) (u \ r) \ s \\<^sub>s q = q) \ Idem (r \\<^sub>s s)" by (frule Unifier_Idem_subst, blast, metis Idem_def comp_assoc) lemma Unifier_mgt: "\Unifier \ t u; \ \\<^sub>\ \\ \ Unifier \ t u" by auto lemma Unifier_support: "\Unifier \ t u; \ supports \\ \ Unifier \ t u" using subst_supportD Unifier_mgt by metis lemma MGU_mgt: "\MGU \ t u; MGU \ t u\ \ \ \\<^sub>\ \" by auto lemma Unifier_trm_FV_bound: "\Unifier s t u; v \ FV t\ \ v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ FV u" proof (induction t arbitrary: s u) case Var thus ?case by (metis UnI1 UnI2 subsetCE no_var_subterm subst_sends_dom_to_img subst_to_var_is_var trm_subst_ident' vars_iff_subterm_or_eq) next case (Fun f X) hence "v \ FV (u \ s) \ v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by (metis subst_not_dom_fixed) thus ?case by (metis (no_types) Un_iff contra_subsetD subst_sends_FV_to_img) qed lemma Unifier_rm_var: "\Unifier \ s t; v \ FV s \ FV t\ \ Unifier (rm_var v \) s t" using assms by (auto simp add: repl_invariance) lemma Unifier_ground_rm_vars: assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" "Unifier (rm_vars X s) t t'" shows "Unifier s t t'" by (rule Unifier_support[OF assms(2) rm_vars_ground_supports[OF assms(1)]]) lemma Unifier_dom_restrict: assumes "Unifier s t t'" "FV t \ FV t' \ S" shows "Unifier (rm_vars (UNIV - S) s) t t'" proof - let ?s = "rm_vars (UNIV - S) s" show ?thesis using term_subst_eq_conv[of t s ?s] term_subst_eq_conv[of t' s ?s] assms by auto qed subsection {* Term positions and substitutions *} lemma subst_Fun_index_eq: assumes "i < length T" "Fun f T \ \ = Fun g T' \ \" shows "T ! i \ \ = T' ! i \ \" proof - have "map (\x. x \ \) T = map (\x. x \ \) T'" using assms by simp thus ?thesis by (metis assms(1) length_map nth_map) qed lemma poss_unified_iff_unifiable: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" shows "t \ \ = t' \ \ \ (\p \ poss t \ poss t'. (t |_ p) \ \ = (t' |_ p) \ \)" proof { fix p assume "p \ poss t \ poss t'" hence "t \ \ = t' \ \ \ t |_ p \ \ = t' |_ p \ \" proof (induction p arbitrary: t t') case (PCons i p) hence *: "i <# p \ poss t" "i <# p \ poss t'" by auto from *(1) obtain f T where t_fun: "t = Fun f T" by (cases t) auto from *(2) obtain g S where t'_fun: "t' = Fun g S" by (cases t') auto have "t |_ = T ! i" "t' |_ = S ! i" by (auto simp add: t'_fun t_fun) hence "t |_ \ \ = t' |_ \ \" by (metis * PCons.prems(1) empty_pos_in_poss poss_PCons_poss subt_at_subst) moreover have "p \ poss (t |_ )" "p \ poss (t' |_ )" using * poss_cons_param by metis+ ultimately have "(t |_ ) |_ p \ \ = (t' |_ ) |_ p \ \" using PCons.IH by blast thus ?case by (simp add: t'_fun t_fun) qed simp } thus "t \ \ = t' \ \ \ (\p \ poss t \ poss t'. (t |_ p) \ \ = (t' |_ p) \ \)" by auto show "(\p \ poss t \ poss t'. (t |_ p) \ \ = (t' |_ p) \ \) \ t \ \ = t' \ \" by (metis Int_iff empty_pos_in_poss subt_at.simps(1)) qed lemma varposs_unified_if_unifiable: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" assumes "t \ \ = t' \ \" shows "\p \ (varposs t \ poss t') \ (poss t \ varposs t'). (t |_ p) \ \ = (t' |_ p) \ \" using assms poss_unified_iff_unifiable[of t \ t'] varposs_imp_poss by auto lemma varposs_funposs_unified_iff_unifiable: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" shows "t \ \ = t' \ \ \ ( (\p \ (varposs t \ poss t') \ (poss t \ varposs t'). (t |_ p) \ \ = (t' |_ p) \ \) \ (\p \ funposs t \ funposs t'. (t |_ p) \ \ = (t' |_ p) \ \))" by (metis IntE IntI UnCI Un_iff funposs_imp_poss poss_simps(1) poss_unified_iff_unifiable) lemma poss_neq_if_poss_neq_subst: assumes "t \ s |_ p \ t' \ s |_ p" obtains p' where "p' \ poss t \ poss t'" "t |_ p' \ t' |_ p'" by (metis assms poss_unified_iff_unifiable subst_apply_term_empty) lemma subst_neq_if_varposs_neq: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" assumes "p \ poss t \ poss t'" "t |_ p = Var x" "t |_ p \ \ \ t' |_ p \ \" shows "t \ \ \ t' \ \" proof - have "p \ varposs t \ poss t'" using assms(1,2) varposs_iff by auto thus ?thesis using varposs_unified_if_unifiable[of t \ t'] assms(3) by auto qed lemma FV_exists_if_unifiable_and_neq: fixes t t'::"('a,'b) term" and \ \::"('a,'b) subst" assumes "t \ t'" "t \ \ = t' \ \" shows "FV t \ FV t' \ {}" proof assume "FV t \ FV t' = {}" hence "FV t = {}" "FV t' = {}" by auto hence "t \ \ = t" "t' \ \ = t'" by auto hence "t = t'" using assms(2) by metis thus False using assms(1) by auto qed lemma poss_funs_ident_if_unifiable: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" and p::pos assumes "t \ \ = t' \ \" "p \ poss t \ poss t'" "t |_p = Fun f T" "t |_p = Fun g S" shows "f = g" "length T = length S" using assms poss_unified_iff_unifiable by auto lemma term_eq_if_varposs_poss_eq: fixes t t'::"('a,'b) term" and \::"('a,'b) subst" assumes "\p \ (varposs t \ poss t') \ (poss t \ varposs t'). (t |_ p) = (t' |_ p)" and "t \ \ = t' \ \" shows "t = t'" using assms proof (induction t arbitrary: t') case (Fun f T t') let ?S = "\t t'. (varposs t \ poss t') \ (poss t \ varposs t')" note IH = Fun.IH note prems = Fun.prems thus ?case proof (cases t') case (Fun g S) hence *: "f = g" "length S = length T" "Fun f T \ \ = Fun g S \ \" using prems UnifierD[of f T \ g S] by metis+ hence "map (\t. t \ \) T = map (\t. t \ \) S" by auto with * have **: "\i. i < length T \ (Fun f T |_ ) \ \ = (Fun g S |_ ) \ \" "\i. i < length T \ (T ! i) \ \ = (S ! i) \ \" using map_nth_conv by force+ from * have "\i p. i < length T \ p \ ?S (Fun f T |_ ) (Fun g S |_ ) \ i<#p \ ?S (Fun f T) (Fun g S)" by auto with Fun prems(1) have ***: "\i. i < length T \ \p \ ?S (Fun f T |_ ) (Fun g S |_ ). Fun f T |_ (i<#p) = Fun g S |_ (i<#p)" by blast have "\i. i < length T \ Fun f T |_ = Fun g S |_ " using IH * ** *** by force thus ?thesis using Fun * by (simp add: nth_equalityI) qed auto qed auto lemma inj_const_subst_neq_aux: assumes "inj_on \ (FV (Var x) \ FV t)" "Var x \ t" "\s \ subterms (Var x) \ subterms t. s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. s = Fun c []" shows "Var x \ \ \ t \ \" using assms proof (cases t) case (Fun f T) hence *: "Fun f T \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using assms by auto show ?thesis proof (cases "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \") case True then obtain c where c: "Var x \ \ = Fun c []" "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using Fun assms(4) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "Fun c [] \ Fun f T \ \" using * by auto thus ?thesis by (metis Fun c(1)) qed (auto simp add: Fun) qed simp lemma inj_const_subst_neq: assumes "inj_on \ (FV t \ FV t')" "t \ t'" "\s \ subterms t \ subterms t'. s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. s = Fun c []" shows "t \ \ \ t' \ \" proof - { fix p assume p: "p \ (varposs t \ poss t') \ (poss t \ varposs t')" "t |_ p \ t' |_ p" then obtain x where x: "t |_ p = Var x \ t' |_ p = Var x" by (meson Int_iff UnE varposs_iff) have subt: "t |_ p \ t" "t' |_ p \ t'" using p(1) poss_is_subtermeq varposs_imp_poss by auto hence "FV (t |_ p) \ FV (t' |_ p) \ FV t \ FV t'" "subterms (t |_ p) \ subterms (t' |_ p) \ subterms t \ subterms t'" using subterms_subset subtermeq_vars_subset by fastforce+ hence *: "inj_on \ (FV (t |_ p) \ FV (t' |_ p))" "\s \ subterms (t |_ p) \ subterms (t' |_ p). s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using assms(1,3) unfolding inj_on_def by blast+ have "t |_ p \ \ \ t' |_ p \ \" using x proof assume **: "t |_ p = Var x" hence "inj_on \ (FV (Var x) \ FV (t' |_ p))" "Var x \ t' |_ p" "\s \ subterms (Var x) \ subterms (t' |_ p). s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using * p(2) by simp_all thus "t |_ p \ \ \ t' |_ p \ \" using inj_const_subst_neq_aux[OF _ _ _ assms(4)] ** by metis next assume **: "t' |_ p = Var x" hence "inj_on \ (FV (Var x) \ FV (t |_ p))" "Var x \ t |_ p" "\s \ subterms (Var x) \ subterms (t |_ p). s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using * p(2) by simp_all thus "t |_ p \ \ \ t' |_ p \ \" using inj_const_subst_neq_aux[OF _ _ _ assms(4)] ** by metis qed hence ?thesis using p(1) varposs_unified_if_unifiable[of t \ t'] by auto } thus ?thesis using term_eq_if_varposs_poss_eq[of t t' \] assms(2) by auto qed lemma varposs_ground_empty: assumes "FV t = {}" shows "varposs t = {}" using assms by (induct t) auto lemma varposs_poss_ground_subst_subset: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \ varposs (t \ s) \ poss (t \ s) \ varposs t \ poss t" using assms varposs_ground_empty by (induct t rule: varposs.induct) fastforce+ lemma varposs_ground_subst_subset: assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" shows "varposs (t \ s) \ varposs t" proof (induction t rule: varposs.induct) case (1 x) thus ?case proof (cases "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s") case True thus ?thesis using assms varposs_ground_empty by fastforce qed simp qed auto lemma subt_at_subst': assumes "p \ poss t \ poss t'" "t \ s = t' \ s" shows "t |_ p \ s = t' |_ p \ s" using assms subt_at_subst[of p t s] subt_at_subst[of p t' s] by simp lemma poss_subst_var: assumes "p \ poss (t \ s)" "t \ s |_ p = Var x" "x \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" shows "p \ poss t" using assms(1,2) proof (induction t arbitrary: p rule: poss.induct) case (1 y p) thus ?case using assms(3) subst_FV_imgI vars_term_subt_at by fastforce next case (2 f T p) then obtain i p' where *: "p = i <# p'" "i < length T" by auto hence **: "p' \ poss (T ! i \ s)" "T ! i \ s |_ p' = Var x" using 2 by fastforce+ have IH: "p' \ poss (T ! i)" by (rule "2.IH"[OF * **]) thus ?case using * by auto qed lemma preordered_finite_set_has_maxima: assumes "finite A" "A \ {}" shows "\a::'a::{preorder} \ A. \b \ A. \(a < b)" using assms proof (induction A rule: finite_induct) case (insert a A) thus ?case by (cases "A = {}", simp, metis insert_iff order_trans less_le_not_le) qed simp lemma pos_deep_neq_if_term_neq: fixes t t'::"('f,'v) term" assumes "t \ t'" obtains p where "p \ poss t \ poss t'" "t |_ p \ t' |_ p" "\p' \ poss t \ poss t'. p < p' \ t |_ p' = t' |_ p'" proof - { fix Q M let ?P = "\M p. \p' \ M. p < p' \ t |_ p' = t' |_ p'" assume Q: "Q = (\p \ poss t \ poss t'. t |_ p \ t' |_ p \ ?P (poss t \ poss t') p)" assume M[simp]: "M = {p \ poss t \ poss t'. t |_ p \ t' |_ p}" have "Q" proof (rule ccontr) assume "\Q" hence "\p \ M. \p' \ M. p < p'" using Q by auto moreover have "finite M" by simp moreover have "\ \ M" using assms(1) by simp hence "M \ {}" by fastforce ultimately show False using preordered_finite_set_has_maxima by metis qed } thus ?thesis by (metis that) qed lemma const_subst_poss_eq: assumes "\s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. s = Fun c []" shows "poss t = poss (t \ \)" proof (induction t) case (Var x) show ?case proof (cases "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \") case True then obtain c where "\ x = Fun c []" using assms by auto thus ?thesis by auto qed auto qed auto subsection {* Well-formedness of substitutions and unifiers *} inductive_set wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set::"('a,'b) subst set" where Empty[simp]: "Var \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" | Insert[simp]: "\\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set; v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; FV t \ (insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)) = {}\ \ \(v := t) \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" definition wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('a,'b) subst \ bool" where "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" definition wf\<^sub>M\<^sub>G\<^sub>U::"('a,'b) subst \ ('a,'b) term \ ('a,'b) term \ bool" where "wf\<^sub>M\<^sub>G\<^sub>U \ s t \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ MGU \ s t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV s \ FV t" declare wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def[simp] wf\<^sub>M\<^sub>G\<^sub>U_def[simp] lemma wf_subst_Idem: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ Idem \" using IdemI by auto lemma wf_subst_properties: "\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set = wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof show "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def proof - assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" hence "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by auto thus "\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" proof (induction \ rule: fsubst_induct) case (FUpdate \ v t) have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t))" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t))" using FUpdate.hyps(2,3) subst_img_update by fastforce+ hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using FUpdate.prems(1) by blast hence "\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" using FUpdate.IH by metis have *: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t" using FUpdate.hyps(2) subst_img_update[OF _ FUpdate.hyps(3)] by fastforce hence "FV t \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) = {}" using FUpdate.prems subst_dom_update2[OF FUpdate.hyps(3)] by blast moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by (meson FUpdate.hyps(3) subst_dom_update2) hence "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using FUpdate.prems * by blast ultimately show ?case using Insert[OF \\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set\ \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\] by metis qed simp qed show "\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def proof (induction \ rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.induct) case (Insert \ v t) hence 1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by simp hence 2: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using Insert.hyps(3) by auto have 3: "FV t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = {}" using Insert.hyps(4) by auto have 4: "\ v = Var v" using \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ by simp from Insert.IH have "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by simp hence 5: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)))" using subst_dom_insert_finite[of \] by simp have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = {}" proof (cases "t = Var v") case True hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using 4 fun_upd_triv term.inject(1) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto thus "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = {}" using 1 2 3 by auto next case False hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = FV t \ (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using 4 subst_img_update[of \ v] by auto thus "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(v := t)) = {}" using 1 2 3 by blast qed thus ?case using 5 unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp qed simp qed lemma wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct[consumes 1, case_names Empty Insert]: assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "P Var" and "\\ v t. \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; P \; v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; FV t \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) = {}\ \ P (\(v := t))" shows "P \" proof - from assms(1,3) wf_subst_properties have "\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" "\\ v t. \\ \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set; P \; v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; FV t \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) = {}\ \ P (\(v := t))" by blast+ thus "P \" using wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.induct assms(2) by blast qed lemma wf_subst_fsubst: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ \ fsubst" unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using finite_dom_iff_fsubst by blast lemma wf_subst_nil: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" by simp lemma wf_MGU_nil: "MGU Var s t \ wf\<^sub>M\<^sub>G\<^sub>U Var s t" using subst_FV_img_alt_def[of Var] by fastforce lemma wf_MGU_dom_bound: "wf\<^sub>M\<^sub>G\<^sub>U \ s t \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV s \ FV t" unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by blast lemma wf_subst_single: assumes "v \ FV t" "\ v = t" "\w. v \ w \ \ w = Var w" shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {v}" using subst_FV_dom_img_single[of v t \, OF assms] by simp hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using assms(1,2,3) subst_FV_dom_img_single(2) by (metis inf_bot_left insert_disjoint(1), simp) thus ?thesis by simp qed lemma wf_subst_reduction: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \ wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s)" proof - assume "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by auto moreover have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) = {}" by (meson compl_le_compl_iff disjoint_eq_subset_Compl subset_trans wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) moreover have "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s))" using \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\ rev_finite_subset unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast ultimately show "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s)" by simp qed lemma wf_subst_compose: assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" using assms proof (induction \1 rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct) case (Insert \1 v t) have "t \ Var v" using Insert.hyps(4) by auto hence dom1v_unfold: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1)" using subst_dom_update2 by metis hence doms_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using Insert.prems(2) disjoint_insert(1) by blast moreover have dom_img_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using Insert.hyps(2) Insert.prems(3) by fastforce ultimately have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" using Insert.IH[OF \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2\] by metis have dom_comp_is_union: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" using subst_dom_comp_eq[OF dom_img_disj] . have "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" using Insert.prems(2) \t \ Var v\ by fastforce hence "\2 v = Var v" "\1 v = Var v" using Insert.hyps(2) by simp_all hence "(\1 \\<^sub>s \2) v = Var v" "(\1(v := t) \\<^sub>s \2) v = t \ \2" "((\1 \\<^sub>s \2)(v := t)) v = t" unfolding subst_compose_def by simp_all have FV_t2_bound: "FV (t \ \2) \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" by (meson subst_sends_FV_to_img) have 1: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" using \(\1 \\<^sub>s \2) v = Var v\ by auto have "insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using Insert.prems(3) dom1v_unfold by blast hence "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" using Insert.hyps(3) by blast hence 2: "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)" by (meson set_rev_mp subst_img_comp_subset) have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2\ by simp hence "FV (t \ \2) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using subst_dom_elim by simp moreover have "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" using Insert.prems(3) dom1v_unfold by blast hence "v \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" using Insert.hyps(4) by blast hence "v \ FV (t \ \2)" using \FV (t \ \2) \ FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2\ by blast moreover have "FV (t \ \2) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 = {}" using dom_img_disj FV_t2_bound \FV t \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1) = {}\ by blast ultimately have 3: "FV (t \ \2) \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)) = {}" using dom_comp_is_union by blast have "\1(v := t) \\<^sub>s \2 = (\1 \\<^sub>s \2)(v := t \ \2)" using subst_comp_upd1[of \1 v t \2] . moreover have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ((\1 \\<^sub>s \2)(v := t \ \2))" using "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.Insert"[OF _ 1 2 3] \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1 \\<^sub>s \2)\ wf_subst_properties by metis ultimately show ?case by presburger qed simp lemma wf_subst_append: fixes \1 \2::"('f,'v) subst" assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" and "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\v. if \1 v = Var v then \2 v else \1 v)" using assms proof (induction \1 rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct) case (Insert \1 v t) let ?if = "\w. if \1 w = Var w then \2 w else \1 w" let ?if_upd = "\w. if (\1(v := t)) w = Var w then \2 w else (\1(v := t)) w" from Insert.hyps(4) have "?if_upd = ?if(v := t)" by fastforce have dom_insert: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1)" using Insert.hyps(4) by auto have "\1 v = Var v" "t \ Var v" using Insert.hyps(2,4) by auto hence img_insert: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\1(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV t" using subst_img_update by metis from Insert.prems(2) dom_insert have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" by auto moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using Insert.prems(3) dom_insert by simp moreover have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 = {}" using Insert.prems(4) img_insert unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if" using Insert.IH[OF Insert.prems(1)] by metis have dom_union: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \1 \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" by auto hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if" using Insert.hyps(2) Insert.prems(2) dom_insert by auto moreover have "v \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if" using Insert.prems(3) Insert.hyps(3) dom_insert unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto moreover have "FV t \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if) = {}" using Insert.hyps(4) Insert.prems(4) img_insert unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto ultimately show ?case using wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.Insert \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if\ \?if_upd = ?if(v := t)\ wf_subst_properties by (metis (no_types, lifting)) qed simp lemma wf_subst_elim_append: assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "elim \ v" "v \ FV t" shows "elim (\(w := t)) v" using assms proof (induction \ rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct) case (Insert \ v' t') hence "\q. v \ FV (Var q \ \(v' := t'))" using elim_dest by blast hence "\q. v \ FV (Var q \ \(v' := t', w := t))" using \v \ FV t\ by simp thus ?case by (metis elim_intro' subst_apply_term.simps(1)) qed simp lemma wf_subst_elim_dom: assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "\v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. elim \ v" using assms proof (induction \ rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct) case (Insert \ w t) have dom_insert: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\(w := t)) \ insert w (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by auto hence "\v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. elim (\(w := t)) v" using Insert.IH Insert.hyps(2,4) by (metis Insert.hyps(1) IntI disjoint_insert(2) empty_iff wf_subst_elim_append) moreover have "w \ FV t" using Insert.hyps(4) by simp hence "\q. w \ FV (Var q \ \(w := t))" by (metis FV_simps(1) FV_in_subst_img Insert.hyps(3) contra_subsetD fun_upd_def singletonD subst_apply_term.simps(1)) hence "elim (\(w := t)) w" by (metis elim_intro') ultimately show ?case using dom_insert by blast qed simp lemma wf_subst_support_iff_mgt: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ supports \ \ \ \\<^sub>\ \" using subst_support_def subst_support_if_mgt_Idem wf_subst_Idem by blast subsection {* Interpretations *} abbreviation interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('a,'b) subst \ bool" where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = UNIV \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" lemma interpretation_substI: "(\v. FV (\ v) = {}) \ interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - assume "\v. FV (\ v) = {}" moreover { fix v assume "FV (\ v) = {}" hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto } ultimately show ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto qed lemma interpretation_grounds[simp]: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (t \ \) = {}" by (simp add: subst_FV_dom_ground_if_ground_img) lemma interpretation_grounds_all: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\v. FV (\ v) = {})" unfolding ground_def by (metis UNIV_I FV_in_subst_img subset_empty subst_dom_vars_in_subst) lemma interpretation_grounds_all': "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ground (M \set \)" by (simp add: subst_FV_dom_ground_if_ground_img) lemma interpretation_comp: assumes "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" proof - have \_FV: "\v. FV (\ v) = {}" using interpretation_grounds_all[OF assms] by simp hence \_FV': "\t. FV (t \ \) = {}" by (metis all_not_in_conv elim_dest elim_intro' subst_apply_term.simps(1)) from assms have "\v. (\ \\<^sub>s \) v \ Var v" unfolding subst_compose_def by (metis FV_simps(1) \_FV' insert_not_empty) hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \) = UNIV" by simp moreover have "\v. FV ((\ \\<^sub>s \) v) = {}" unfolding subst_compose_def using \_FV' by simp hence "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \))" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp ultimately show "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" .. from assms have "\v. (\ \\<^sub>s \) v \ Var v" unfolding subst_compose_def by (metis FV_simps(1) \_FV insert_not_empty subst_to_var_is_var) hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \) = UNIV" by simp moreover have "\v. FV ((\ \\<^sub>s \) v) = {}" unfolding subst_compose_def by (simp add: \_FV trm_subst_ident) hence "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \))" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp ultimately show "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" .. qed lemma interpretation_subst_exists: "\\::('f,'v) subst. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - obtain c::"'f" where "c \ UNIV" by simp then obtain \::"('f,'v) subst" where "\v. \ v = Fun c []" by simp hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = UNIV" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" by (simp_all add: img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) thus ?thesis by auto qed lemma interpretation_subst_exists': "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = X \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" proof - obtain \::"('f,'v) subst" where \: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = UNIV" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using interpretation_subst_exists by moura let ?\ = "rm_vars (UNIV - X) \" have 1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = X" using \ by auto hence 2: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" using \ unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force show ?thesis using 1 2 by metis qed lemma interpretation_Idem: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ Idem \" unfolding Idem_def using interpretation_grounds_all[of \] by (simp add: trm_subst_ident subst_eq_if_eq_vars) lemma Idem_comp_upd_eq: assumes "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "Idem \" shows "\ \\<^sub>s \ = \(v := \ v) \\<^sub>s \" proof - from assms(1) have "(\ \\<^sub>s \) v = \ v" unfolding subst_compose_def by auto moreover have "\w. w \ v \ (\ \\<^sub>s \) w = (\(v := \ v) \\<^sub>s \) w" unfolding subst_compose_def by auto moreover have "(\(v := \ v) \\<^sub>s \) v = \ v" using assms(2) unfolding Idem_def subst_compose_def by (metis fun_upd_same) ultimately show ?thesis by (metis fun_upd_same fun_upd_triv subst_comp_upd1) qed lemma interpretation_dom_img_disjoint: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by simp subsection {* IsaFoR Unification Theory Linking *} lemma MGU_is_mgu_singleton: "MGU \ t u = is_mgu \ {(t,u)}" unfolding is_mgu_def unifiers_def by auto lemma Unifier_in_unifiers_singleton: "Unifier \ s t \ \ \ unifiers {(s,t)}" unfolding unifiers_def by auto lemma subst_dom_conv: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = subst_domain s" by (metis subst_domain_def dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) lemma subst_ran_img_conv: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = subst_range s" by (metis subst_range.simps img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_dom_conv) lemma subst_range_vars_img_FV_conv: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = range_vars s" by (simp add: range_vars_def subst_ran_img_conv) declare subst_list_def[simp] lemma subst_list_singleton_FV_subset: "(\x \ set (subst_list (subst v t) E). FV (fst x) \ FV (snd x)) \ FV t \ (\x \ set E. FV (fst x) \ FV (snd x))" proof (induction E) case (Cons x E) let ?FVs = "\L. \x \ set L. FV (fst x) \ FV (snd x)" let ?FVx = "FV (fst x) \ FV (snd x)" let ?FVxsubst = "FV (fst x \ Var(v := t)) \ FV (snd x \ Var(v := t))" have "?FVs (subst_list (subst v t) (x#E)) = ?FVxsubst \ ?FVs (subst_list (subst v t) E)" unfolding subst_list_def subst_def by auto hence "?FVs (subst_list (subst v t) (x#E)) \ ?FVxsubst \ FV t \ ?FVs E" using Cons.IH by blast moreover have "?FVs (x#E) = ?FVx \ ?FVs E" by auto moreover have "?FVxsubst \ ?FVx \ FV t" using subst_FV_bound_singleton[of _ v t] by blast ultimately show ?case by blast qed simp lemma subst_of_dom_subset: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of L) \ set (map fst L)" proof (induction L rule: List.rev_induct) case (snoc x L) then obtain v t where x: "x = (v,t)" by (metis surj_pair) hence "subst_of (L@[x]) = Var(v := t) \\<^sub>s subst_of L" using subst_of_simps(3)[of x "[]"] unfolding subst_def by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of (L@[x])) \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of L))" using x subst_dom_comp_subset[of "Var(v := t)" "subst_of L"] by auto thus ?case using snoc.IH x by auto qed simp lemma wf_MGU_is_imgu_singleton: "wf\<^sub>M\<^sub>G\<^sub>U \ s t \ is_imgu \ {(s,t)}" proof - assume "wf\<^sub>M\<^sub>G\<^sub>U \ s t" hence "Idem \" "\\' \ unifiers {(s,t)}. \ \\<^sub>\ \'" "\ \ unifiers {(s,t)}" using wf_subst_Idem Unifier_in_unifiers_singleton unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by auto hence "\\ \ unifiers {(s,t)}. \ = \ \\<^sub>s \" by (metis Idem_def comp_assoc) thus "is_imgu \ {(s,t)}" by (metis is_imgu_def \\ \ unifiers {(s,t)}\) qed lemma mgu_subst_range_vars: assumes "mgu s t = Some \" shows "range_vars \ \ vars_term s \ vars_term t" proof - obtain xs where *: "Unification.unify [(s, t)] [] = Some xs" and [simp]: "subst_of xs = \" using assms by (simp split: option.splits) from unify_Some_UNIF [OF *] obtain ss where "compose ss = \" and "UNIF ss {#(s, t)#} {#}" by auto with UNIF_range_vars_subset [of ss "{#(s, t)#}" "{#}"] show ?thesis by simp qed lemma mgu_subst_domain_range_vars_disjoint: assumes "mgu s t = Some \" shows "subst_domain \ \ range_vars \ = {}" proof - have "is_imgu \ {(s, t)}" using assms mgu_sound by simp hence "\ = \ \\<^sub>s \" unfolding is_imgu_def by blast thus ?thesis by (metis \\ = \ \\<^sub>s \\ subst_idemp_iff) qed lemma mgu_gives_wellformed_subst: assumes "mgu s t = Some \" shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using mgu_finite_subst_domain[OF assms] mgu_subst_domain_range_vars_disjoint[OF assms] subst_range_vars_img_FV_conv[of \] subst_dom_conv[of \] unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma mgu_gives_wellformed_MGU: assumes "mgu s t = Some \" shows "wf\<^sub>M\<^sub>G\<^sub>U \ s t" using mgu_subst_domain[OF assms] mgu_sound[OF assms] mgu_subst_range_vars[OF assms] subst_range_vars_img_FV_conv[of \] subst_dom_conv[of \] MGU_is_mgu_singleton[of s \ t] is_imgu_imp_is_mgu[of \ "{(s,t)}"] mgu_gives_wellformed_subst[OF assms] unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by auto lemma mgu_vars_bounded[dest?]: "mgu M N = Some \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV M \ FV N" using mgu_gives_wellformed_MGU unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by blast lemma mgu_gives_Idem: "mgu s t = Some \ \ Idem \" using mgu_sound[of s t \] unfolding is_imgu_def Idem_def by auto lemma mgu_always_unifies: "Unifier \ M N \ \\. mgu M N = Some \" using mgu_complete Unifier_in_unifiers_singleton by blast lemma mgu_gives_MGU: "mgu s t = Some \ \ MGU \ s t" using mgu_sound[of s t \, THEN is_imgu_imp_is_mgu] MGU_is_mgu_singleton by metis lemma mgu_same_empty: "mgu (t::('a,'b) term) t = Some Var" proof - { fix E::"('a,'b) equation list" and U::"('b \ ('a,'b) term) list" assume "\(s,t) \ set E. s = t" hence "Unification.unify E U = Some U" proof (induction E U rule: Unification.unify.induct) case (2 f S g T E U) hence *: "f = g" "S = T" by auto moreover have "\(s,t) \ set (zip T T). s = t" by (induct T) auto hence "\(s,t) \ set (zip T T@E). s = t" using "2.prems"(1) by auto moreover have "zip_option S T = Some (zip S T)" using \S = T\ by (induct S T rule: zip_induct) auto hence **: "decompose (Fun f S) (Fun g T) = Some (zip S T)" using \f = g\ unfolding decompose_def by auto ultimately have "Unification.unify (zip S T@E) U = Some U" using "2.IH" * by auto thus ?case using ** by auto qed auto } hence "Unification.unify [(t,t)] [] = Some []" by auto thus ?thesis by auto qed lemma mgu_var: assumes "x \ FV t" shows "mgu (Var x) t = Some (Var(x := t))" proof - have "unify [(Var x,t)] [] = Some [(x,t)]" using assms by auto moreover have "subst_of [(x,t)] = Var(x := t)" unfolding subst_of_def subst_def by simp ultimately show ?thesis by simp qed lemma mgu_eliminates[dest?]: assumes "mgu M N = Some \" shows "(\v \ FV M \ FV N. elim \ v) \ \ = Var" (is "?P M N \") proof (cases "\ = Var") case False then obtain v where v: "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto hence "v \ FV M \ FV N" using mgu_vars_bounded[OF assms] by auto thus ?thesis using wf_subst_elim_dom[OF mgu_gives_wellformed_subst[OF assms]] v by blast qed simp lemma mgu_eliminates_dom: assumes "mgu x y = Some \" "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "elim \ v" using mgu_gives_wellformed_subst[OF assms(1)] unfolding wf\<^sub>M\<^sub>G\<^sub>U_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def elim_def by (metis disjoint_iff_not_equal subst_dom_elim assms(2)) lemma unify_list_distinct: assumes "Unification.unify E B = Some U" "distinct (map fst B)" and "(\x \ set E. FV (fst x) \ FV (snd x)) \ set (map fst B) = {}" shows "distinct (map fst U)" using assms proof (induction E B arbitrary: U rule: Unification.unify.induct) case 1 thus ?case by simp next case (2 f X g Y E B U) let ?FVs = "\L. \x \ set L. FV (fst x) \ FV (snd x)" from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'" and [simp]: "f = g" "length X = length Y" "E' = zip X Y" and **: "Unification.unify (E'@E) B = Some U" by (auto split: option.splits) hence "\t t'. (t,t') \ set E' \ FV t \ FV (Fun f X) \ FV t' \ FV (Fun g Y)" by (metis zip_arg_subterm subtermseq_if_subterms subtermeq_vars_subset) hence "?FVs E' \ FV (Fun f X) \ FV (Fun g Y)" by fastforce moreover have "FV (Fun f X) \ set (map fst B) = {}" "FV (Fun g Y) \ set (map fst B) = {}" using "2.prems"(3) by auto ultimately have "?FVs E' \ set (map fst B) = {}" by blast moreover have "?FVs E \ set (map fst B) = {}" using "2.prems"(3) by auto ultimately have "?FVs (E'@E) \ set (map fst B) = {}" by auto thus ?case using "2.IH"[OF * ** "2.prems"(2)] by metis next case (3 v t E B) let ?FVs = "\L. \x \ set L. FV (fst x) \ FV (snd x)" let ?E' = "subst_list (subst v t) E" from "3.prems"(3) have "v \ set (map fst B)" "FV t \ set (map fst B) = {}" by force+ hence *: "distinct (map fst ((v, t)#B))" using "3.prems"(2) by auto show ?case proof (cases "t = Var v") case True thus ?thesis using "3.prems" "3.IH"(1) by auto next case False hence "v \ FV t" using "3.prems"(1) by auto hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U" using \t \ Var v\ "3.prems"(1) by auto moreover have "?FVs ?E' \ set (map fst ((v, t)#B)) = {}" proof - have "v \ ?FVs ?E'" unfolding subst_list_def subst_def by (simp add: \v \ FV t\ subst_remove_var) moreover have "?FVs ?E' \ FV t \ ?FVs E" by (metis subst_list_singleton_FV_subset) hence "?FVs ?E' \ set (map fst B) = {}" using "3.prems"(3) by auto ultimately show ?thesis by auto qed ultimately show ?thesis using "3.IH"(2)[OF \t \ Var v\ \v \ FV t\ _ *] by metis qed next case (4 f X v E B U) let ?FVs = "\L. \x \ set L. FV (fst x) \ FV (snd x)" let ?E' = "subst_list (subst v (Fun f X)) E" have *: "?FVs E \ set (map fst B) = {}" using "4.prems"(3) by auto from "4.prems"(1) have "v \ FV (Fun f X)" by force from "4.prems"(3) have **: "v \ set (map fst B)" "FV (Fun f X) \ set (map fst B) = {}" by force+ hence ***: "distinct (map fst ((v, Fun f X)#B))" using "4.prems"(2) by auto from "4.prems"(3) have ****: "?FVs ?E' \ set (map fst ((v, Fun f X)#B)) = {}" proof - have "v \ ?FVs ?E'" unfolding subst_list_def subst_def using \v \ FV (Fun f X)\ subst_remove_var[of v "Fun f X"] by simp moreover have "?FVs ?E' \ FV (Fun f X) \ ?FVs E" by (metis subst_list_singleton_FV_subset) hence "?FVs ?E' \ set (map fst B) = {}" using * ** by blast ultimately show ?thesis by auto qed have "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, Fun f X) # B) = Some U" using \v \ FV (Fun f X)\ "4.prems"(1) by auto thus ?case using "4.IH"[OF \v \ FV (Fun f X)\ _ *** ****] by metis qed lemma mgu_None_is_subst_neq: fixes s t::"('a,'b) term" and \::"('a,'b) subst" assumes "mgu s t = None" shows "s \ \ \ t \ \" using assms mgu_always_unifies by force lemma mgu_None_if_neq_ground: assumes "t \ t'" "FV t = {}" "FV t' = {}" shows "mgu t t' = None" proof (rule ccontr) assume "mgu t t' \ None" then obtain \ where \: "mgu t t' = Some \" by auto hence "t \ \ = t" "t' \ \ = t'" using assms subst_ground_ident by auto thus False using assms(1) MGU_is_Unifier[OF mgu_gives_MGU[OF \]] by auto qed lemma const_subst_subterm: assumes "Fun c [] \ t \ \" shows "Fun c [] \ t \ (\s \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. Fun c [] \ s)" using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (induction t) force+ lemma subst_of_const: assumes "(subst_of D) z = Fun c []" shows "\z. (z, Fun c []) \ set D" using assms proof (induction D arbitrary: z) case (Cons d D) then obtain x t where d: "d = (x, t)" by moura hence *: "subst_of (d#D) = subst_of D \\<^sub>s Var(x := t)" using subst_of_simps(3)[of d D] unfolding subst_def by simp from Cons show ?case proof (cases "\z. subst_of D z = Fun c []") case False hence "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of D)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto moreover have "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of D \\<^sub>s Var(x := t))" using * Cons.prems unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto moreover have "\y. (Var(x := t)) y = Fun c [] \ t = Fun c []" by (metis fun_upd_apply term.distinct(1)) ultimately have "t = Fun c []" using subst_img_comp_subset_const[of c "subst_of D" "Var(x := t)"] by (metis imageE img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) thus ?thesis using d by auto qed auto qed simp lemma mgu_img_consts: fixes \::"('f,'v) subst" and s t::"('f,'v) term" and c::'f and z::'v assumes "mgu s t = Some \" "\ z = Fun c []" shows "Fun c [] \ s \ Fun c [] \ t" proof - { fix E::"('f,'v) equation list" and B U::"('v \ ('f,'v) term) list" and z::'v assume "Unification.unify E B = Some U" "(z, Fun c []) \ set U" hence "(z,Fun c []) \ set B \ (\(s,t) \ set E. Fun c [] \ s \ Fun c [] \ t)" proof (induction E B arbitrary: U rule: Unification.unify.induct) case 1 thus ?case by simp next case (2 f X g Y E B U) from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'" and **[simp]: "f = g" "length X = length Y" "E' = zip X Y" and ***: "Unification.unify (E'@E) B = Some U" by (auto split: option.splits) hence IH: "(z,Fun c []) \ set B \ (\(s,t) \ set (E'@E). Fun c [] \ s \ Fun c [] \ t)" using "2.IH" "2.prems" by blast moreover have "\(s,t) \ set E'. (Fun c [] \ s \ Fun c [] \ t) \ Fun c [] \ Fun f X \ Fun c [] \ Fun g Y" proof - assume "\(s, t)\set E'. Fun c [] \ s \ Fun c [] \ t" then obtain p::"('f, 'v) equation" where f1: "p \ set E' \ (case p of (t, t') \ Fun c [] \ t \ Fun c [] \ t')" by blast have f2: "\p. (fst p::('f,'v) term, snd p::('f,'v) Term.term) = p" by auto have f3: "Fun c [] \ fst p \ Fun c [] \ snd p" using f1 by force have f4: "\p f. p \ set E' \ snd p \ Fun f Y" by (metis (lifting) f2 **(3) zip_arg_subterm(2)) have "fst p \ Fun f X" by (metis (no_types) f2 f1 **(3) zip_arg_subterm(1)) thus ?thesis using f4 f3 f1 by (meson subtermeq_trans subtermseq_if_subterms) qed ultimately show ?case using \E' = zip X Y\ by auto next case (3 v t E B) show ?case proof (cases "t = Var v") case True thus ?thesis using "3.prems" "3.IH"(1) by auto next case False hence "v \ FV t" using "3.prems"(1) by auto hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U" using \t \ Var v\ "3.prems"(1) by auto hence IH: "(z, Fun c []) \ set ((v, t)#B) \ (\(s,t) \ set (subst_list (subst v t) E). Fun c [] \ s \ Fun c [] \ t)" using "3.IH"(2)[OF \t \ Var v\ \v \ FV t\ _ "3.prems"(2)] by metis show ?thesis proof (cases "(z, Fun c []) \ set ((v, t)#B)") case False hence "\p \ set E. Fun c [] \ fst p \ Var(v := t) \ Fun c [] \ snd p \ Var(v := t)" using IH unfolding subst_list_def subst_def by auto then obtain s s' where *: "(s, s') \ set E" "Fun c [] \ s \ Var(v := t) \ Fun c [] \ s' \ Var(v := t)" by auto moreover { assume "\Fun c [] \ t" hence "\(\s\img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (Var(v := t)). Fun c [] \ s)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "Fun c [] \ s \ Fun c [] \ s'" using *(2) const_subst_subterm[of c _ "Var(v := t)"] by metis } ultimately show ?thesis by auto qed auto qed next case (4 f X v E B U) have "v \ FV (Fun f X)" using "4.prems"(1) not_None_eq by fastforce hence "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U" using "4.prems"(1) by auto hence IH: "(z, Fun c []) \ set ((v, Fun f X)#B) \ (\(s,s') \ set (subst_list (subst v (Fun f X)) E). Fun c [] \ s \ Fun c [] \ s')" using "4.IH"[OF \v \ FV (Fun f X)\ _ "4.prems"(2)] by metis show ?case proof (cases "(z, Fun c []) \ set ((v, Fun f X)#B)") case False hence "\p \ set E. Fun c [] \ fst p \ Var(v := Fun f X) \ Fun c [] \ snd p \ Var(v := Fun f X)" using IH unfolding subst_list_def subst_def by auto then obtain s s' where *: "(s, s') \ set E" "Fun c [] \ s \ Var(v := Fun f X) \ Fun c [] \ s' \ Var(v := Fun f X)" by auto moreover { assume "\Fun c [] \ Fun f X" hence "\(\s\img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (Var(v := Fun f X)). Fun c [] \ s)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "Fun c [] \ s \ Fun c [] \ s'" using *(2) const_subst_subterm[of c _ "Var(v := Fun f X)"] by metis } ultimately show ?thesis by auto qed auto qed } moreover obtain D where "unify [(s, t)] [] = Some D" "\ = subst_of D" using assms(1) by (cases "unify [(s, t)] []") auto moreover have "\z. (z,Fun c []) \ set D" using \\ = subst_of D\ assms(2) subst_of_const by metis ultimately show ?thesis by fastforce qed lemma inj_const_subst_unif: fixes \ \ \::"('f,'v) subst" and s t::"('f,'v) term" assumes \: "inj \" "\u \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. u = Fun c []" "\u \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. u \ subterms s \ subterms t" and \: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" and unif: "Unifier \ (s \ \) (t \ \)" shows "\\. Unifier \ (s \ \) (t \ \)" proof - let ?xs = "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" let ?ys = "(FV s \ FV t) - ?xs" have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using \(2) by auto have "\\::('f,'v) subst. s \ \ = t \ \" by (metis subst_comp unif) then obtain \::"('f,'v) subst" where \: "mgu s t = Some \" using mgu_always_unifies by moura have 1: "\\::('f,'v) subst. s \ \ \ \ = t \ \ \ \" by (metis unif) have 2: "\\::('f,'v) subst. s \ \ \ \ = t \ \ \ \ \ \ \\<^sub>\ \ \\<^sub>s \" using mgu_gives_MGU[OF \] by simp have 3: "\(z::'v) (c::'f). \ z = Fun c [] \ Fun c [] \ s \ Fun c [] \ t" by (rule mgu_img_consts[OF \]) have 4: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using mgu_gives_wellformed_subst[OF \] by auto have 5: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV s \ FV t" using mgu_gives_wellformed_MGU[OF \] by auto { fix x and \::"('f,'v) subst" assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "(\ \\<^sub>s \) x = \ x" using \ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)\ by (simp add: ident_comp_subst_trm_if_disj) } then obtain \::"('f,'v) subst" where \: "\x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \ x = (\ \\<^sub>s \) x" using 1 2 by moura have *: "\x. x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \y \ ?ys. \ x = Var y" proof - fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs" hence x: "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto then obtain c where c: "\ x = Fun c []" using \(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by moura hence *: "(\ \\<^sub>s \) x = Fun c []" using \ x by fastforce hence **: "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" "Fun c [] \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto have "\ x = Fun c [] \ (\z. \ x = Var z \ \ z = Fun c [])" by (rule subst_img_comp_subset_const'[OF *]) moreover have "\ x \ Fun c []" proof (rule ccontr) assume "\\ x \ Fun c []" hence "Fun c [] \ s \ Fun c [] \ t" using 3 by metis moreover have "Fun c [] \ subterms s \ subterms t" by (metis c \ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)\ \(3) x(2) ground_subst_dom_iff_img) ultimately show False by auto qed moreover have "\x' \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \ x \ Var x'" proof (rule ccontr) assume "\(\x' \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \ x \ Var x')" then obtain x' where x': "x' \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ x = Var x'" by moura hence "\ x' = Fun c []" "(\ \\<^sub>s \) x = Fun c []" using * unfolding subst_compose_def by auto moreover have "x \ x'" using x(1) x'(2) 4 by auto moreover have "x' \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using x'(2) mgu_eliminates_dom[OF \] by (metis (no_types) elim_def subst_apply_term.simps(1) vars_iff_subterm_or_eq ) moreover have "(\ \\<^sub>s \) x = \ x" "(\ \\<^sub>s \) x' = \ x'" using \ x(2) x'(1) by auto ultimately show False using \(1) * unfolding inj_on_def by (simp add: subst_compose_def x'(2)) qed ultimately show "\y \ ?ys. \ x = Var y" by (metis 5 x(2) DiffI Un_iff subst_FV_imgI subtermeqI' sup.orderE vars_iff_subtermeq) qed have **: "inj_on \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs)" proof (intro inj_onI) fix x y assume *: "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ x = \ y" hence "(\ \\<^sub>s \) x = (\ \\<^sub>s \) y" unfolding subst_compose_def by auto hence "\ x = \ y" using \ * by auto thus "x = y" using \(1) inj_onD[of \ UNIV x y] by simp qed def \ \ "\y'. if Var y' \ \ ` (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs) then Var ((inv_into (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs) \) (Var y')) else Var y'::('f,'v) term" have a1: "Unifier (\ \\<^sub>s \) s t" using mgu_gives_MGU[OF \] by auto def \' \ "\ \\<^sub>s \" have d1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' \ ?ys" proof fix z assume z: "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" have "z \ ?xs \ z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" proof (cases "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \") case True moreover assume "z \ ?xs" ultimately have z_in: "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs" by simp then obtain y where y: "\ z = Var y" "y \ ?ys" using * by moura hence "\ y = Var ((inv_into (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ?xs) \) (Var y))" using \_def z_in by simp hence "\ y = Var z" by (metis y(1) z_in ** inv_into_f_eq) hence "\' z = Var z" using \'_def y(1) subst_compose_def[of \ \] by simp thus ?thesis by auto next case False hence "\ z = Var z" by simp moreover assume "z \ ?xs" hence "\ z = Var z" using \_def * by force ultimately show ?thesis using \'_def subst_compose_def[of \ \] by simp qed moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" unfolding \'_def \_def by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using subst_dom_comp_subset \'_def by fastforce ultimately show "z \ ?ys" using 5 z by auto qed have d2: "Unifier (\' \\<^sub>s \) s t" using a1 \'_def by auto have d3: "\ \\<^sub>s \' \\<^sub>s \ = \' \\<^sub>s \" proof - { fix z::'v assume z: "z \ ?xs" then obtain u where u: "\ z = u" "FV u = {}" using \ by auto hence "(\ \\<^sub>s \' \\<^sub>s \) z = u" by (simp add: subst_compose subst_ground_ident) moreover have "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" using d1 z by auto hence "\' z = Var z" by simp hence "(\' \\<^sub>s \) z = u" using u(1) by (simp add: subst_compose) ultimately have "(\ \\<^sub>s \' \\<^sub>s \) z = (\' \\<^sub>s \) z" by metis } moreover { fix z::'v assume "z \ ?ys" hence "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \(2) by auto hence "(\ \\<^sub>s \' \\<^sub>s \) z = (\' \\<^sub>s \) z" by (simp add: subst_compose) } moreover { fix z::'v assume "z \ ?xs" "z \ ?ys" hence "\ z = Var z" "\' z = Var z" using \(2) d1 by blast+ hence "(\ \\<^sub>s \' \\<^sub>s \) z = (\' \\<^sub>s \) z" by (simp add: subst_compose) } ultimately show ?thesis by auto qed from d2 d3 have "Unifier (\' \\<^sub>s \) (s \ \) (t \ \)" by (metis subst_comp) thus ?thesis by metis qed lemma sat_ineq_inj_const_subst_aux: fixes \::"('f,'v) subst" assumes "Unifier \ (s \ \) (t \ \)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "(FV s \ FV t) - X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ X = {}" shows "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = X \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ s \ \ \ \ = t \ \ \ \" proof - have "\\. Unifier \ (s \ \) (t \ \) \ interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - obtain \'::"('f,'v) subst" where *: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" using interpretation_subst_exists by metis hence "Unifier (\ \\<^sub>s \') (s \ \) (t \ \)" using assms(1) by simp thus ?thesis using * interpretation_comp by blast qed then obtain \' where \': "Unifier \' (s \ \) (t \ \)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" by moura def \'' \ "rm_vars (UNIV - X) \'" have *: "FV (s \ \) \ X" "FV (t \ \) \ X" using assms(2,3) by (simp_all add: Diff_subset_conv Un_commute subst_FV_unfold_ground_img) hence **: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'' = X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'')" using rm_vars_img_subset[of "UNIV - X" \'] rm_vars_dom[of "UNIV - X" \'] \'(2) \''_def by auto hence "\t. t \ \ \ \'' = t \ \'' \ \" using subst_eq_if_disjoint_vars_ground[OF _ _ assms(2)] assms(4) by blast moreover have "Unifier \'' (s \ \) (t \ \)" using Unifier_dom_restrict[OF \'(1)] \''_def * by blast ultimately show ?thesis using ** by auto qed lemma sat_ineq_inj_const_subst: fixes \ \ \::"('f,'v) subst" assumes \: "inj \" "\t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. t = Fun c []" "\u \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. u \ subterms s \ subterms t" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ X = {}" and \: "\\::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = X \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ s \ \ \ \ \ t \ \ \ \" "(FV s \ FV t) - X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ X = {}" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" and \: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" shows "s \ \ \ \ \ t \ \ \ \" proof - have "\\. \Unifier \ (s \ \) (t \ \)" by (metis \(1) sat_ineq_inj_const_subst_aux[OF _ \(4,2,3)]) hence "\Unifier \ (s \ \) (t \ \)" by (metis inj_const_subst_unif[OF \(1,2,3) \(4,5)]) moreover have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using \(2,4) \(1) by auto ultimately show ?thesis using \ subst_eq_if_disjoint_vars_ground[OF _ _ \(2)] by metis qed end