(* (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. *) (* Title: TypedModel.thy Author: Andreas Viktor Hess, DTU *) section {* Theory: The Typed Model *} theory TypedModel imports LazyIntruder begin subsection {* Term types and well-formed types *} type_synonym ('f,'v) term_type = "('f,'v) term" abbreviation (input) TAtom::"'v \ ('f,'v) term_type" where "TAtom a \ Var a" abbreviation (input) TComp::"['f, ('f,'v) term_type list] \ ('f,'v) term_type" where "TComp f T \ Fun f T" locale typed_model = intruder_model arity public Ana for arity::"'fun::countable \ nat" and public::"'fun \ bool" and Ana::"('fun,'var::countable) term \ (('fun,'var) terms \ ('fun,'var) terms)" + fixes \::"('fun,'var) term \ ('fun,'atom::finite) term_type" assumes const_type: "\c. arity c = 0 \ \a. \X. \ (Fun c X) = TAtom a" and fun_type: "\f X. arity f > 0 \ \ (Fun f X) = TComp f (map \ X)" and infinite_typed_consts: "\a. infinite {c. \ (Fun c []) = TAtom a \ public c}" and \_wf: "\t f T. TComp f T \ \ t \ arity f > 0" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ (Var x))" begin lemma infinite_typed_consts': "\a. infinite {c. \ (Fun c []) = TAtom a \ public c \ arity c = 0}" proof - fix a { fix c assume "\ (Fun c []) = TAtom a" "public c" hence "arity c = 0" using const_type[of c] fun_type[of c "[]"] by auto } hence "{c. \ (Fun c []) = TAtom a \ public c \ arity c = 0} = {c. \ (Fun c []) = TAtom a \ public c}" by auto thus "infinite {c. \ (Fun c []) = TAtom a \ public c \ arity c = 0}" using infinite_typed_consts[of a] by metis qed lemma \_wf': "wf\<^sub>t\<^sub>r\<^sub>m t \ wf\<^sub>t\<^sub>r\<^sub>m (\ t)" proof (induction t) case (Fun f T) hence *: "arity f = length T" "\t. t \ set T \ wf\<^sub>t\<^sub>r\<^sub>m (\ t)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto { assume "arity f = 0" hence ?case using const_type[of f] by auto } moreover { assume "arity f > 0" hence ?case using fun_type[of f] * by force } ultimately show ?case by auto qed (metis \_wf(2)) subsection {* Definitions *} abbreviation "\\<^sub>a \ UNIV::('atom set)" (* Well-typed substitutions *) definition wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t where "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\v. \ (Var v) = \ (\ v))" (* Sub-message patterns *) inductive_set SMP\<^sub>s\<^sub>t::"('fun,'var) terms \ ('fun,'var) terms" for M where MP[intro]: "t \ M \ t \ SMP\<^sub>s\<^sub>t M" | Subterm[intro]: "\t \ SMP\<^sub>s\<^sub>t M; t' \ t\ \ t' \ SMP\<^sub>s\<^sub>t M" | Substitution[intro]: "\t \ SMP\<^sub>s\<^sub>t M; wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; \v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\ \ (t \ \) \ SMP\<^sub>s\<^sub>t M" | Ana[intro]: "\t \ SMP\<^sub>s\<^sub>t M; Ana t = (K,T); t' \ K\ \ t' \ SMP\<^sub>s\<^sub>t M" (* Type-flaw resistance *) abbreviation tfr\<^sub>s\<^sub>t where "tfr\<^sub>s\<^sub>t M \ (\s \ SMP\<^sub>s\<^sub>t M - (Var`\). \t \ SMP\<^sub>s\<^sub>t M - (Var`\). (\\. Unifier \ s t) \ \ s = \ t) \ (\x \ M. wf\<^sub>t\<^sub>r\<^sub>m x)" (* (In)equalities must have the same type, and all variables in inequalities must additionally have atomic type *) abbreviation eqs_tfr\<^sub>s\<^sub>t where "eqs_tfr\<^sub>s\<^sub>t S \ (\t t'. t \ t' \ set S \ (\\. Unifier \ t t') \ \ t = \ t') \ (\X t t'. \X\t \ t'\ \ set S \ (\x \ set X \ FV t \ FV t'. \a. \ (Var x) = TAtom a))" subsection {* Small Lemmata *} lemma fun_type_inv: assumes "\ t = TComp f T" shows "arity f > 0" "public f" using \_wf(1)[of f T t] assms by simp_all lemma fun_type_inv_wf: assumes "\ t = TComp f T" "wf\<^sub>t\<^sub>r\<^sub>m t" shows "arity f = length T" using \_wf'[OF assms(2)] assms(1) unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto lemma const_type_inv: "\ (Fun c X) = TAtom a \ arity c = 0" by (rule ccontr, simp add: fun_type) lemma const_type': "\c \ \. \a \ \\<^sub>a. \X. \ (Fun c X) = TAtom a" using const_type by simp lemma fun_type': "\f \ \\<^sub>f. \X. \ (Fun f X) = TComp f (map \ X)" using fun_type by simp lemma atypes_inhabited: "\c. \ (Fun c []) = TAtom a \ wf\<^sub>t\<^sub>r\<^sub>m (Fun c []) \ public c \ arity c = 0" proof - obtain c where "\ (Fun c []) = TAtom a" "public c" "arity c = 0" using infinite_typed_consts'(1)[of a] not_finite_existsD by blast thus ?thesis using const_type_inv[OF \\ (Fun c []) = TAtom a\] unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto qed lemma atype_ground_term_ex: "\t. FV t = {} \ \ t = TAtom a \ wf\<^sub>t\<^sub>r\<^sub>m t" using atypes_inhabited[of a] by force lemma tatom_set_finite: "finite \\<^sub>a" by (fact Finite_Set.finite_class.finite) lemma fun_type_id_eq: "\ (Fun f X) = TComp g Y \ f = g" by (metis const_type fun_type neq0_conv "term.inject"(2) "term.simps"(4)) lemma type_ground_inhabited: "\t'. FV t' = {} \ \ t = \ t'" proof - { fix \::"('fun, 'atom) term_type" assume "\f T. Fun f T \ \ \ 0 < arity f" hence "\t'. FV t' = {} \ \ = \ t'" proof (induction \) case (Fun f T) hence "arity f > 0" by auto from Fun.IH Fun.prems(1) have "\Y. map \ Y = T \ (\x \ set Y. FV x = {})" proof (induction T) case (Cons x X) hence "\g Y. Fun g Y \ Fun f X \ 0 < arity g" by auto hence "\Y. map \ Y = X \ (\x\set Y. FV x = {})" using Cons by auto moreover have "\t'. FV t' = {} \ x = \ t'" using Cons by auto ultimately obtain y Y where "FV y = {}" "\ y = x" "map \ Y = X" "\x\set Y. FV x = {}" using Cons by moura hence "map \ (y#Y) = x#X \ (\x\set (y#Y). FV x = {})" by auto thus ?case by meson qed simp then obtain Y where "map \ Y = T" "\x \ set Y. FV x = {}" by metis hence "FV (Fun f Y) = {}" "\ (Fun f Y) = TComp f T" using fun_type[OF \arity f > 0\] by auto thus ?case by (metis exI[of "\t. FV t = {} \ \ t = TComp f T" "Fun f Y"]) qed (metis atype_ground_term_ex) } thus ?thesis by (metis \_wf(1)) qed lemma type_wfttype_inhabited: assumes "\f T. Fun f T \ \ \ 0 < arity f" "wf\<^sub>t\<^sub>r\<^sub>m \" shows "\t. \ t = \ \ wf\<^sub>t\<^sub>r\<^sub>m t" using assms proof (induction \) case (Var a) thus ?case using atypes_inhabited wf\<^sub>t\<^sub>r\<^sub>m_def by blast next case (Fun f Y) hence "\y. y \ set Y \ wf\<^sub>t\<^sub>r\<^sub>m y" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (metis Fun_param_is_subterm subtermeq_subterm_trans subtermseq_if_subterms) moreover have "\y. y \ set Y \ (\g Z. Fun g Z \ y \ 0 < arity g)" using Fun by auto ultimately have IH: "\y. y \ set Y \ \t. \ t = y \ wf\<^sub>t\<^sub>r\<^sub>m t" using Fun.IH by auto from Fun have "arity f = length Y" "arity f > 0" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by force+ moreover from IH have "\X. map \ X = Y \ (\x \ set X. wf\<^sub>t\<^sub>r\<^sub>m x)" by (induct Y, simp_all, metis list.simps(9) set_ConsD) ultimately show ?case by (metis fun_type length_map wf_trmI) qed lemma type_pgwt_inhabited: "wf\<^sub>t\<^sub>r\<^sub>m t \ \t'. \ t = \ t' \ public_ground_wf_term t'" proof - assume "wf\<^sub>t\<^sub>r\<^sub>m t" { fix \ assume "\ t = \" hence "\t'. \ t = \ t' \ public_ground_wf_term t'" using \wf\<^sub>t\<^sub>r\<^sub>m t\ proof (induction \ arbitrary: t) case (Var a t) then obtain c where "\ t = \ (Fun c [])" "arity c = 0" "public c" using const_type_inv[of _ "[]" a] infinite_typed_consts(1)[of a] not_finite_existsD by force thus ?case using PGWT[OF \public c\, of "[]"] by auto next case (Fun f Y t) have *: "arity f > 0" "public f" "arity f = length Y" using fun_type_inv[OF \\ t = TComp f Y\] fun_type_inv_wf[OF \\ t = TComp f Y\ \wf\<^sub>t\<^sub>r\<^sub>m t\] by auto have "\y. y \ set Y \ \t'. y = \ t' \ public_ground_wf_term t'" using Fun.prems(1) Fun.IH \_wf(1)[of _ _ t] \_wf'[OF \wf\<^sub>t\<^sub>r\<^sub>m t\] type_wfttype_inhabited by (metis Fun_param_is_subterm subterm_def subtermeq_trans wf_trm_subtermeq) hence "\X. map \ X = Y \ (\x \ set X. public_ground_wf_term x)" by (induct Y, simp_all, metis list.simps(9) set_ConsD) then obtain X where X: "map \ X = Y" "\x. x \ set X \ public_ground_wf_term x" by moura hence "arity f = length X" using *(3) by auto have "\ t = \ (Fun f X)" "public_ground_wf_term (Fun f X)" using fun_type[OF *(1), of X] Fun.prems(1) X(1) apply simp using PGWT[OF *(2) \arity f = length X\ X(2)] by metis thus ?case by metis qed } thus ?thesis using \wf\<^sub>t\<^sub>r\<^sub>m t\ by auto qed lemma pgwt_type_map: assumes "public_ground_wf_term t" shows "\ t = TAtom a \ \f. t = Fun f []" "\ t = TComp g Y \ \X. t = Fun g X \ map \ X = Y" proof - let ?A = "\ t = TAtom a \ (\f. t = Fun f [])" let ?B = "\ t = TComp g Y \ (\X. t = Fun g X \ map \ X = Y)" have "?A \ ?B" proof (cases "\ t") case (Var a) obtain f X where "t = Fun f X" "arity f = length X" using pgwt_fun[OF assms(1)] pgwt_arity[OF assms(1)] by fastforce+ thus ?thesis using const_type_inv \\ t = TAtom a\ by auto next case (Fun g Y) obtain f X where *: "t = Fun f X" using pgwt_fun[OF assms(1)] by force hence "f = g" "map \ X = Y" using fun_type_id_eq \\ t = TComp g Y\ fun_type[OF fun_type_inv(1)[OF \\ t = TComp g Y\]] by fastforce+ thus ?thesis using *(1) \\ t = TComp g Y\ by auto qed thus "\ t = TAtom a \ \f. t = Fun f []" "\ t = TComp g Y \ \X. t = Fun g X \ map \ X = Y" by auto qed lemma wt_subst_Var[simp]: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" by (metis wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) lemma wt_subst_trm: "(\v. v \ FV t \ \ (Var v) = \ (\ v)) \ \ t = \ (t \ \)" proof (induction t) case (Fun f X) hence *: "\x. x \ set X \ \ x = \ (x \ \)" by auto show ?case proof (cases "f \ \\<^sub>f") case True hence "\X. \ (Fun f X) = TComp f (map \ X)" using fun_type' by auto thus ?thesis using * by auto next case False hence "\a \ \\<^sub>a. \X. \ (Fun f X) = TAtom a" using const_type' by auto thus ?thesis by auto qed qed auto lemma wt_subst_trm': "\wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \; \ s = \ t\ \ \ (s \ \) = \ (t \ \)" by (metis wt_subst_trm wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) lemma wt_subst_compose: assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \)" proof - have "\v. \ (\ v) = \ (\ v \ \)" using wt_subst_trm \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by metis moreover have "\v. \ (Var v) = \ (\ v)" using \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by metis ultimately have "\v. \ (Var v) = \ (\ v \ \)" by metis thus ?thesis unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_compose_def by metis qed lemma wt_subst_TAtom_FV: assumes \: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" and "\x \ FV t. \a. \ (Var x) = TAtom a" shows "\x \ FV (t \ \). \a. \ (Var x) = TAtom a" using assms(3) proof (induction t) case (Var x) then obtain a where "\ (Var x) = TAtom a" by moura hence *: "\ (\ x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using \ unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto show ?case proof (cases "\ x") case (Var y) thus ?thesis using * by auto next case (Fun f T) hence "T = []" using * const_type_inv[of f T a] unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto thus ?thesis using Fun by auto qed qed auto lemma TComp_term_cases: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "\ t = TComp f T" shows "(\v. t = Var v) \ (\T'. t = Fun f T' \ T = map \ T')" using assms fun_type[OF fun_type_inv(1)[OF assms(2)]] fun_type_id_eq by (cases t) force+ lemma TAtom_term_cases: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "\ t = TAtom \" shows "(\v. t = Var v) \ (\f. t = Fun f [])" using assms const_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (cases t) auto lemma subtermeq_imp_subtermtypeeq: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \ t" shows "\ s \ \ t" using assms(2,1) proof (induction t) case (Fun f T) thus ?case proof (cases "s = Fun f T") case False then obtain x where x: "x \ set T" "s \ x" using Fun.prems(1) by auto hence "wf\<^sub>t\<^sub>r\<^sub>m x" using wf_trm_subtermeq[OF Fun.prems(2)] Fun_param_is_subterm[of _ T f] by auto hence "\ s \ \ x" using Fun.IH[OF x] by simp moreover have "arity f > 0" using x fun_type_inv_wf Fun.prems by (metis length_pos_if_in_set subtermeq_refl wf\<^sub>t\<^sub>r\<^sub>m_def) ultimately show ?thesis using x Fun.prems fun_type[of f T] by auto qed simp qed simp lemma subterm_funs_term_in_type: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "Fun f T \ t" "\ (Fun f T) = TComp f (map \ T)" shows "f \ funs_term (\ t)" using assms(2,1,3) proof (induction t) case (Fun f' T') hence [simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" by (metis wf_trm_subtermeq) { fix a assume \: "\ (Fun f' T') = TAtom a" hence "Fun f T = Fun f' T'" using Fun TAtom_term_cases subtermeq_Var_const by blast hence False using Fun.prems(3) \ by simp } moreover { fix g S assume \: "\ (Fun f' T') = TComp g S" hence "g = f'" "S = map \ T'" using Fun.prems(2) fun_type_id_eq[OF \] fun_type[OF fun_type_inv(1)[OF \]] by auto hence \': "\ (Fun f' T') = TComp f' (map \ T')" using \ by auto hence "g \ funs_term (\ (Fun f' T'))" using \ by auto moreover { assume "Fun f T \ Fun f' T'" then obtain x where "x \ set T'" "Fun f T \ x" using Fun.prems(1) by auto hence "f \ funs_term (\ x)" using Fun.IH[OF _ _ _ Fun.prems(3), of x] wf_trm_subtermeq[OF \wf\<^sub>t\<^sub>r\<^sub>m (Fun f' T')\, of x] by force moreover have "\ x \ set (map \ T')" using \' \x \ set T'\ by auto ultimately have "f \ funs_term (\ (Fun f' T'))" using \' by auto } ultimately have ?case by (cases "Fun f T = Fun f' T'") (auto simp add: \g = f'\) } ultimately show ?case by (cases "\ (Fun f' T')") auto qed simp lemma wf_trm_TAtom_subterms: "\wf\<^sub>t\<^sub>r\<^sub>m t; \ t = TAtom \\ \ subterms t = {t}" using const_type_inv wf\<^sub>t\<^sub>r\<^sub>m_def by (cases t) fastforce+ lemma wf_trm_TComp_subterm: assumes "wf\<^sub>t\<^sub>r\<^sub>m s" "t \ s" obtains f T where "\ s = TComp f T" proof (cases s) case (Var x) thus ?thesis using \t \ s\ by simp next case (Fun g S) hence "length S > 0" using assms Fun_subterm_inside_params[of t g S] by auto hence "arity g > 0" by (metis \wf\<^sub>t\<^sub>r\<^sub>m s\ \s = Fun g S\ subtermeq_refl wf\<^sub>t\<^sub>r\<^sub>m_def) thus ?thesis using fun_type \s = Fun g S\ that by auto qed lemma SMP_I: assumes "s \ M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "t \ s \ \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "t \ SMP\<^sub>s\<^sub>t M" using SMP\<^sub>s\<^sub>t.Substitution[OF SMP\<^sub>s\<^sub>t.MP[OF assms(1)] assms(2)] SMP\<^sub>s\<^sub>t.Subterm[of "s \ \" M t] assms(3,4) unfolding subtermeq_def by (cases "t = s \ \") simp_all lemma SMP_wf_trm: assumes "t \ SMP\<^sub>s\<^sub>t M" "\m. m \ M \ wf\<^sub>t\<^sub>r\<^sub>m m" shows "wf\<^sub>t\<^sub>r\<^sub>m t" using assms(1) proof (induction t rule: SMP\<^sub>s\<^sub>t.induct) case MP thus ?case using assms(2) by simp next case Subterm thus ?case using wf_trm_subterm by simp next case Substitution thus ?case using wf_trm_subst by auto next case Ana thus ?case using Ana_keys_wf' by auto qed lemma SMP_ikI[intro]: "t \ ik\<^sub>s\<^sub>t S \ t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" by auto lemma SMP_ik_trpI[intro]: "t \ trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \ t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" proof - assume "t \ trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)" then obtain t' where "t' \ ik\<^sub>s\<^sub>t S" "t \ t'" using trpD by blast hence "t' \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" by auto show "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" proof (cases "t = t'") case True thus ?thesis using SMP_ikI unfolding trms\<^sub>s\<^sub>t_def by (auto simp add: \t' \ ik\<^sub>s\<^sub>t S\) next case False hence "t \ t'" using \t \ t'\ by simp thus ?thesis using SMP\<^sub>s\<^sub>t.Subterm[OF \t' \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)\] by metis qed qed lemma MP_setI[intro]: "x \ set S \ trm\<^sub>s\<^sub>t\<^sub>p x \ trms\<^sub>s\<^sub>t S" unfolding trms\<^sub>s\<^sub>t_def by blast lemma SMP_setI[intro]: "x \ set S \ trm\<^sub>s\<^sub>t\<^sub>p x \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" by blast lemma SMP_append[simp]: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S')) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" proof { fix t assume "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" hence "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" by induct auto } thus "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S')) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" by blast { fix t assume "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" hence "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by induct auto } moreover { fix t assume "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" hence "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by induct auto } ultimately show "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S') \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by blast qed lemma SMP_append': "SMP\<^sub>s\<^sub>t (A \ B) = SMP\<^sub>s\<^sub>t A \ SMP\<^sub>s\<^sub>t B" proof { fix t assume "t \ SMP\<^sub>s\<^sub>t (A \ B)" hence "t \ SMP\<^sub>s\<^sub>t A \ SMP\<^sub>s\<^sub>t B" by induct auto } thus "SMP\<^sub>s\<^sub>t (A \ B) \ SMP\<^sub>s\<^sub>t A \ SMP\<^sub>s\<^sub>t B" by blast { fix t assume "t \ SMP\<^sub>s\<^sub>t A" hence "t \ SMP\<^sub>s\<^sub>t (A \ B)" by induct auto } moreover { fix t assume "t \ SMP\<^sub>s\<^sub>t B" hence "t \ SMP\<^sub>s\<^sub>t (A \ B)" by induct auto } ultimately show "SMP\<^sub>s\<^sub>t A \ SMP\<^sub>s\<^sub>t B \ SMP\<^sub>s\<^sub>t (A \ B)" by blast qed lemma SMP_Cons: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (x#S)) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [x]) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" using SMP_append[of "[x]" S] by auto lemma SMP_Nil[simp]: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t []) = {}" proof - { fix t assume "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [])" hence False by induct auto } thus ?thesis by blast qed lemma trms\<^sub>s\<^sub>t_cons: "trms\<^sub>s\<^sub>t (x#S) = {trm\<^sub>s\<^sub>t\<^sub>p x} \ {trm_r\<^sub>s\<^sub>t\<^sub>p x} \ trms\<^sub>s\<^sub>t S" by simp lemma SMP_subset_union_eq: assumes "M \ SMP\<^sub>s\<^sub>t N" shows "SMP\<^sub>s\<^sub>t N = SMP\<^sub>s\<^sub>t (M \ N)" proof - { fix t assume "t \ SMP\<^sub>s\<^sub>t (M \ N)" hence "t \ SMP\<^sub>s\<^sub>t N" using assms by (induction rule: SMP\<^sub>s\<^sub>t.induct) auto } thus ?thesis using SMP_append' by auto qed lemma SMP_subterms_subset: "\(subterms ` M) \ SMP\<^sub>s\<^sub>t M" proof fix t assume "t \ \(subterms ` M)" then obtain m where "m \ M" "t \ m" by auto thus "t \ SMP\<^sub>s\<^sub>t M" using SMP_I[of _ _ Var] by auto qed lemma trm_strand_subst_cong: "t \ trms\<^sub>s\<^sub>t S \ t \ \ \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \) \ (\X t' t''. \X\t' \ t''\ \ set S \ t \ rm_vars (set X) \ \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \))" "t \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \) \ (\t'. t = t' \ \ \ t' \ trms\<^sub>s\<^sub>t S) \ (\X t' t''. \X\t' \ t''\ \ set S \ (t = t' \ rm_vars (set X) \ \ t = t'' \ rm_vars (set X) \))" proof - let ?P = "\t \ S. t \ \ \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \) \ (\X t' t''. \X\t' \ t''\ \ set S \ t \ rm_vars (set X) \ \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \))" let ?Q = "\t \ S. (\t'. t = t' \ \ \ t' \ trms\<^sub>s\<^sub>t S) \ (\X t' t''. \X\t' \ t''\ \ set S \ (t = t' \ rm_vars (set X) \ \ t = t'' \ rm_vars (set X) \))" show "t \ trms\<^sub>s\<^sub>t S \ ?P t \ S" proof (induction S) case (Cons x S) show ?case proof (cases "t \ trms\<^sub>s\<^sub>t S") case True hence "?P t \ S" using Cons by simp thus ?thesis apply (cases x) by (metis (no_types, lifting) Un_iff list.set_intros(2) strand_subst_hom(2) trms\<^sub>s\<^sub>t_cons)+ next case False hence **: "t = trm\<^sub>s\<^sub>t\<^sub>p x \ t = trm_r\<^sub>s\<^sub>t\<^sub>p x" using Cons.prems by auto thus ?thesis proof (cases x) case (Inequality X s s') hence "t \ rm_vars (set X) \ = trm\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>s\<^sub>t\<^sub>p \) \ t \ rm_vars (set X) \ = trm_r\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>s\<^sub>t\<^sub>p \)" using ** by auto moreover have "\X\s \ s'\ \ set (x#S)" using Inequality by simp ultimately show ?thesis using Inequality by force qed auto qed qed simp show "t \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \) \ ?Q t \ S" proof (induction S) case (Cons x S) show ?case proof (cases "t \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \)") case True hence "?Q t \ S" using Cons by simp thus ?thesis by (cases x) auto next case False hence **: "t = trm\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>s\<^sub>t\<^sub>p \) \ t = trm_r\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>s\<^sub>t\<^sub>p \)" using Cons.prems by auto thus ?thesis proof (cases x) case (Inequality X s s') hence "t = trm\<^sub>s\<^sub>t\<^sub>p x \ rm_vars (set X) \ \ t = trm_r\<^sub>s\<^sub>t\<^sub>p x \ rm_vars (set X) \" using ** by auto moreover have "\X\s \ s'\ \ set (x#S)" using Inequality by simp ultimately show ?thesis using Inequality by auto qed auto qed qed simp qed lemma wf_trm_subst_rm_vars: "wf\<^sub>t\<^sub>r\<^sub>m (\ v) \ wf\<^sub>t\<^sub>r\<^sub>m (rm_vars X \ v)" by auto lemma wt_subst_rm_vars: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \)" using rm_vars_dom unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto lemma SMP_mono: assumes "A \ B" shows "SMP\<^sub>s\<^sub>t A \ SMP\<^sub>s\<^sub>t B" proof fix t assume "t \ SMP\<^sub>s\<^sub>t A" thus "t \ SMP\<^sub>s\<^sub>t B" using assms by (induct t rule: SMP\<^sub>s\<^sub>t.induct) auto qed lemma wt_subst_SMP_subset: assumes "trms\<^sub>s\<^sub>t S \ SMP\<^sub>s\<^sub>t S'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \) \ SMP\<^sub>s\<^sub>t S'" proof fix t assume *: "t \ trms\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \)" { fix t' assume "t = t' \ \" "t' \ trms\<^sub>s\<^sub>t S" hence "t \ SMP\<^sub>s\<^sub>t S'" using assms SMP\<^sub>s\<^sub>t.Substitution by auto } moreover { fix X t' t'' assume "\X\t' \ t''\ \ set S" "t = t' \ rm_vars (set X) \ \ t = t'' \ rm_vars (set X) \" hence "t \ SMP\<^sub>s\<^sub>t S'" using assms(1,3) SMP\<^sub>s\<^sub>t.Substitution[OF _ wt_subst_rm_vars[OF assms(2), of "set X"]] wf_trm_subst_rm_vars by auto } ultimately show "t \ SMP\<^sub>s\<^sub>t S'" using trm_strand_subst_cong(2)[OF *] by blast qed lemma MP_singleton: "trms\<^sub>s\<^sub>t [x] = {trm\<^sub>s\<^sub>t\<^sub>p x} \ {trm_r\<^sub>s\<^sub>t\<^sub>p x}" by simp lemma MP_subset_SMP: "trm\<^sub>s\<^sub>t\<^sub>p ` set S \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "trms\<^sub>s\<^sub>t S \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" by auto lemma SMP_fun_map_snd_subset: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (map Send X)) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [snd\Fun f X\])" proof fix t assume "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (map Send X))" thus "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [snd\Fun f X\])" proof induction case (MP t) hence "t \ set X" by auto hence "t \ Fun f X" by (metis subtermI') thus ?case using SMP\<^sub>s\<^sub>t.Subterm[of "Fun f X" "trms\<^sub>s\<^sub>t [snd\Fun f X\]" t] using SMP\<^sub>s\<^sub>t.MP by auto qed auto qed lemma SMP_wt_subst_subset: assumes "t \ SMP\<^sub>s\<^sub>t (M \set \)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "t \ SMP\<^sub>s\<^sub>t M" using assms by (induct t rule: SMP\<^sub>s\<^sub>t.induct) auto lemma id_type_eq: assumes "\ (Fun f X) = \ (Fun g Y)" shows "f \ \ \ g \ \" "f \ \\<^sub>f \ g \ \\<^sub>f" using assms const_type' fun_type' id_union_univ(1) by (metis UNIV_I UnE "term.distinct"(1))+ lemma fun_type_arg_cong: assumes "f \ \\<^sub>f" "g \ \\<^sub>f" "\ (Fun f (x#X)) = \ (Fun g (y#Y))" shows "\ x = \ y" "\ (Fun f X) = \ (Fun g Y)" using assms fun_type' by auto lemma fun_type_arg_cong': assumes "f \ \\<^sub>f" "g \ \\<^sub>f" "\ (Fun f (X@x#X')) = \ (Fun g (Y@y#Y'))" "length X = length Y" shows "\ x = \ y" using assms proof (induction X arbitrary: Y) case Nil thus ?case using fun_type_arg_cong(1)[of f g x X' y Y'] by auto next case (Cons x' X Y'') then obtain y' Y where "Y'' = y'#Y" by (metis length_Suc_conv) hence "\ (Fun f (X@x#X')) = \ (Fun g (Y@y#Y'))" "length X = length Y" using Cons.prems(3,4) fun_type_arg_cong(2)[OF Cons.prems(1,2), of x' "X@x#X'"] by auto thus ?thesis using Cons.IH[OF Cons.prems(1,2)] by auto qed lemma eqs_tfr_cons_split: assumes "eqs_tfr\<^sub>s\<^sub>t (x#S)" shows "eqs_tfr\<^sub>s\<^sub>t [x]" "eqs_tfr\<^sub>s\<^sub>t S" using assms by fastforce+ lemma eqs_tfr_append_split: assumes "eqs_tfr\<^sub>s\<^sub>t (S@S')" shows "eqs_tfr\<^sub>s\<^sub>t S" "eqs_tfr\<^sub>s\<^sub>t S'" using assms by fastforce+ lemma eqs_tfr_append_split': assumes "eqs_tfr\<^sub>s\<^sub>t (S@x#S')" shows "eqs_tfr\<^sub>s\<^sub>t (S@S')" using assms by fastforce lemma eqs_tfr_append: assumes "eqs_tfr\<^sub>s\<^sub>t S" "eqs_tfr\<^sub>s\<^sub>t S'" shows "eqs_tfr\<^sub>s\<^sub>t (S@S')" using assms by fastforce lemma eqs_tfr_wt_subst_apply: assumes "eqs_tfr\<^sub>s\<^sub>t S" and \: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" shows "eqs_tfr\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \)" using assms(1) proof (induction S) case (Cons x S) hence IH: "eqs_tfr\<^sub>s\<^sub>t (S \\<^sub>s\<^sub>t \)" using eqs_tfr_cons_split(2)[of x S] by fastforce thus ?case proof (cases x) case (Equality t t') hence "(\\. Unifier \ t t') \ \ t = \ t'" using Cons.prems by auto hence "(\\. Unifier \ (t \ \) (t' \ \)) \ \ (t \ \) = \ (t' \ \)" by (metis Unifier_comp' wt_subst_trm'[OF assms(2)]) moreover have "(x#S) \\<^sub>s\<^sub>t \ = ((t \ \) \ (t' \ \))#(S \\<^sub>s\<^sub>t \)" using \x = t \ t'\ by auto ultimately show ?thesis using IH by auto next case (Inequality X t t') hence "\x \ set X \ FV t \ FV t'. \a. \ (Var x) = TAtom a" using Cons.prems by fastforce+ hence "\x \ set X \ FV (t \ rm_vars (set X) \) \ FV (t' \ rm_vars (set X) \). \a. \ (Var x) = TAtom a" using wt_subst_TAtom_FV[OF wt_subst_rm_vars[OF \(1), of "set X"]] wt_subst_trm'[OF wt_subst_rm_vars[OF \(1), of "set X"]] wf_trm_subst_rm_vars[of \ _ "set X"] \(2) by blast moreover have "(x#S) \\<^sub>s\<^sub>t \ = \X\(t \ rm_vars (set X) \) \ (t' \ rm_vars (set X) \)\#(S \\<^sub>s\<^sub>t \)" using \x = \X\t \ t'\\ by auto ultimately show ?thesis using IH by simp qed auto qed simp lemma eqs_tfr_same_type: "eqs_tfr\<^sub>s\<^sub>t (S@t \ t'#S') \ Unifier \ t t' \ \ t = \ t'" by force+ lemma tfr_union_subset: "tfr\<^sub>s\<^sub>t (A \ B) \ tfr\<^sub>s\<^sub>t A" using assms SMP_append'[of A B] by simp subsection {* Well-typedness and type-flaw resistance preservation *} lemma unify_list_wt_if_same_type: assumes "Unification.unify E B = Some U" "\(s,t) \ set E. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t \ \ s = \ t" and "\(v,t) \ set B. \ (Var v) = \ t" shows "\(v,t) \ set U. \ (Var v) = \ t" using assms proof (induction E B arbitrary: U rule: Unification.unify.induct) case (2 f X g Y E B U) hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)" "\ (Fun f X) = \ (Fun g Y)" by auto 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) have "\(s,t) \ set E'. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t \ \ s = \ t" proof - { fix s t assume "(s,t) \ set E'" then obtain X' X'' Y' Y'' where "X = X'@s#X''" "Y = Y'@t#Y''" "length X' = length Y'" using zip_arg_subterm_split[of s t X Y] \E' = zip X Y\ by metis hence "\ (Fun f (X'@s#X'')) = \ (Fun g (Y'@t#Y''))" by (metis \\ (Fun f X) = \ (Fun g Y)\) from \E' = zip X Y\ have "\(s,t) \ set E'. s \ Fun f X \ t \ Fun g Y" using zip_arg_subterm[of _ _ X Y] by blast with \(s,t) \ set E'\ have "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" using wf_trm_subterm \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ \wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)\ by (blast,blast) moreover have "f \ \\<^sub>f" proof (rule ccontr) assume "f \ \\<^sub>f" hence "f \ \" "arity f = 0" using const_arity_eq_zero[of f] by simp_all thus False using \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ * \(s,t) \ set E'\ unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto qed hence "\ s = \ t" using fun_type_arg_cong' \f \ \\<^sub>f\ \\ (Fun f (X'@s#X'')) = \ (Fun g (Y'@t#Y''))\ \length X' = length Y'\ \f = g\ by metis ultimately have "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" "\ s = \ t" by metis+ } thus ?thesis by blast qed moreover have "\(s,t) \ set E. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t \ \ s = \ t" using "2.prems"(2) by auto ultimately show ?case using "2.IH"[OF * ** _ "2.prems"(3)] by fastforce next case (3 v t E B U) hence "\ (Var v) = \ t" "wf\<^sub>t\<^sub>r\<^sub>m t" by auto hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t)" and *: "\(v, t) \ set ((v,t)#B). \ (Var v) = \ t" "\t t'. (t,t') \ set E \ \ t = \ t'" using "3.prems"(2,3) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_def by auto show ?case proof (cases "t = Var v") assume "t = Var v" thus ?case using 3 by auto next assume "t \ Var v" 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 Unification.unify.simps(3)[of v t E B] "3.prems"(1) \t \ Var v\ by auto have "\(s, t) \ set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" using wf_trm_subst_singleton[OF _ \wf\<^sub>t\<^sub>r\<^sub>m t\] "3.prems"(2) unfolding subst_list_def subst_def by auto moreover have "\(s, t) \ set (subst_list (subst v t) E). \ s = \ t" using *(2)[THEN wt_subst_trm'[OF \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t)\]] by simp ultimately show ?thesis using "3.IH"(2)[OF \t \ Var v\ \v \ FV t\ ** _ *(1)] by auto qed next case (4 f X v E B U) hence "\ (Var v) = \ (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" by auto hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v (Fun f X))" and *: "\(v, t) \ set ((v,(Fun f X))#B). \ (Var v) = \ t" "\t t'. (t,t') \ set E \ \ t = \ t'" using "4.prems"(2,3) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_def by auto have "v \ FV (Fun f X)" using "4.prems"(1) by force hence **: "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U" using Unification.unify.simps(3)[of v "Fun f X" E B] "4.prems"(1) by auto have "\(s, t) \ set (subst_list (subst v (Fun f X)) E). wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" using wf_trm_subst_singleton[OF _ \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\] "4.prems"(2) unfolding subst_list_def subst_def by auto moreover have "\(s, t) \ set (subst_list (subst v (Fun f X)) E). \ s = \ t" using *(2)[THEN wt_subst_trm'[OF \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v (Fun f X))\]] by simp ultimately show ?case using "4.IH"[OF \v \ FV (Fun f X)\ ** _ *(1)] by auto qed auto lemma mgu_wt_if_same_type: assumes "mgu s t = Some \" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" "\ s = \ t" shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - let ?FV_disj = "\v t S. \(\(v',t') \ S - {(v,t)}. (insert v (FV t)) \ (insert v' (FV t')) \ {})" from assms(1) obtain \' where "Unification.unify [(s,t)] [] = Some \'" "subst_of \' = \" by (auto split: option.splits) hence "\(v,t) \ set \'. \ (Var v) = \ t" "distinct (map fst \')" using assms(2,3,4) unify_list_wt_if_same_type unify_list_distinct[of "[(s,t)]"] by auto thus "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \subst_of \' = \\ unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def proof (induction \' arbitrary: \ rule: List.rev_induct) case (snoc tt \' \) then obtain v t where tt: "tt = (v,t)" by (metis surj_pair) hence \: "\ = subst v t \\<^sub>s subst_of \'" using snoc.prems(3) by simp have "\(v,t) \ set \'. \ (Var v) = \ t" "distinct (map fst \')" using snoc.prems(1,2) by auto then obtain \'' where \'': "subst_of \' = \''" "\v. \ (Var v) = \ (\'' v)" by (metis snoc.IH) hence "\t. \ t = \ (t \ \'')" using wt_subst_trm by blast hence "\ (Var v) = \ (\'' v)" "\ t = \ (t \ \'')" using \''(2) by auto moreover have "\ (Var v) = \ t" using snoc.prems(1) tt by simp moreover have \2: "\ = Var(v := t) \\<^sub>s \'' " using \ \''(1) unfolding subst_def by simp ultimately have "\ (Var v) = \ (\ v)" unfolding subst_compose_def by simp have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t) \ {v}" unfolding subst_def by auto hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'')" using tt \ \''(1) snoc.prems(2) subst_dom_comp_subset[of _ \''] by auto have "v \ set (map fst \')" using tt snoc.prems(2) by auto hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \''" using \''(1) subst_of_dom_subset[of \'] by auto { fix w assume "w \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \''" hence "\ w = \'' w" using \2 \''(1) \v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \''\ unfolding subst_compose_def by auto hence "\ (Var w) = \ (\ w)" using \''(2) by simp } thus ?case using \\ (Var v) = \ (\ v)\ * by force qed simp qed lemma LI_preserves_eqs_tfr_single: assumes "(S,\) \ (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" and "eqs_tfr\<^sub>s\<^sub>t S" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" shows "eqs_tfr\<^sub>s\<^sub>t S'" using assms proof (induction rule: LI_rel.induct) case (Compose S X f S' \) { fix t t' assume *: "t \ t' \ set (S@map Send X@S')" "\\. Unifier \ t t'" hence "t \ t' \ set (S@S')" by auto hence "\ t = \ t'" using Compose.prems(4) *(2) by simp } moreover { fix Y t t' assume "\Y\t \ t'\ \ set (S@map Send X@S')" hence "\Y\t \ t'\ \ set (S@S')" by auto hence "\x\set Y \ FV t \ FV t'. \a. \ (Var x) = Var a" using Compose.prems(4) by auto } ultimately show ?case by metis next case (Unify S f Y \ X S' \) have "eqs_tfr\<^sub>s\<^sub>t (S@S')" using eqs_tfr_append_split'[OF Unify.prems(4)] by metis have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(5) by simp moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" proof - obtain x where True "x \ set S" "Fun f Y \ trm\<^sub>s\<^sub>t\<^sub>p x" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" using Unify.hyps(2) Unify.prems(5) by auto thus ?thesis using wf_trm_subterm[OF \wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)\, of "Fun f Y"] by (cases "Fun f Y = trm\<^sub>s\<^sub>t\<^sub>p x", auto) qed moreover have "Fun f X \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" "Fun f Y \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" using SMP_append[of S "snd\Fun f X\#S'"] SMP_Cons[of "snd\Fun f X\" S'] SMP_ikI[OF Unify.hyps(2)] by auto hence "\ (Fun f X) = \ (Fun f Y)" using Unify.prems(5) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]] by blast ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis moreover have "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" by (rule mgu_wf_trm[OF Unify.hyps(3)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ \wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\]) ultimately show ?case using eqs_tfr_wt_subst_apply[OF \eqs_tfr\<^sub>s\<^sub>t (S@S')\] by metis next case (Equality S \ t t' S' \) have "eqs_tfr\<^sub>s\<^sub>t (S@S')" "\ t = \ t'" using eqs_tfr_same_type[of S t t' S'] eqs_tfr_append_split'[of S _ S'] MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]] Equality.prems(4) by blast+ moreover have "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" using Equality.prems(5) by auto ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis moreover have "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" by (rule mgu_wf_trm[OF Equality.hyps(2)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m t\ \wf\<^sub>t\<^sub>r\<^sub>m t'\]) ultimately show ?case using eqs_tfr_wt_subst_apply[OF \eqs_tfr\<^sub>s\<^sub>t (S@S')\] by metis qed lemma LI_in_SMP_subset_single: assumes "(S,\) \ (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" and "trms\<^sub>s\<^sub>t S \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "trms\<^sub>s\<^sub>t S' \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" using assms proof (induction rule: LI_rel.induct) case (Compose S X f S' \) hence "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [snd\Fun f X\]) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" proof - have *: "\S S'. SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S \ trms\<^sub>s\<^sub>t S') = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S @ S'))" using SMP_append SMP_append' by presburger hence **: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t ((S@snd\Fun f X\#S')@S'')) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" by (metis (no_types) Compose.prems(5) SMP_subset_union_eq) have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'') \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" by simp thus ?thesis by (metis (no_types) * ** SMP_Cons SMP_append' Un_subset_iff) qed thus ?case using Compose.prems(5) by force next case (Unify S f Y \ X S' \) have "Fun f X \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" by auto moreover have "MGU \ (Fun f X) (Fun f Y)" by (metis mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]) moreover have "\x. x \ set S \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(1,2,3) by force+ moreover have "Fun f Y \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1)) ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" "\ (Fun f X) = \ (Fun f Y)" using trp_ik_subterm_exD[OF trpI[OF \Fun f Y \ ik\<^sub>s\<^sub>t S\]] \tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))\ by (metis subterm_def wf_trm_subterm, blast) hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\]) moreover have "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" by (fact mgu_wf_trm[OF Unify.hyps(3)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ \wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\]) ultimately have "trms\<^sub>s\<^sub>t ((S@snd\Fun f X\#S') \\<^sub>s\<^sub>t \) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" using SMP\<^sub>s\<^sub>t.Substitution Unify.prems(5) wt_subst_SMP_subset by metis thus ?case by auto next case (Equality S \ t t' S' \) hence "\ t = \ t'" using eqs_tfr_same_type MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]] by metis moreover have "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \ t'#S'))" "t' \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \ t'#S'))" using Equality.prems(1) by auto moreover have "MGU \ t t'" using mgu_gives_MGU[OF Equality.hyps(2)[symmetric]] by metis moreover have "\x. x \ set S \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" using Equality.prems(1,2,3) by force+ ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m t\]) moreover have "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" by (fact mgu_wf_trm[OF Equality.hyps(2)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m t\ \wf\<^sub>t\<^sub>r\<^sub>m t'\]) ultimately have "trms\<^sub>s\<^sub>t ((S@t \ t'#S') \\<^sub>s\<^sub>t \) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" using SMP\<^sub>s\<^sub>t.Substitution Equality.prems wt_subst_SMP_subset by metis thus ?case by auto qed lemma LI_preserves_tfr_single: assumes "(S,\) \ (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" shows "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" using assms proof (induction rule: LI_rel.induct) case (Compose S X f S' \) let ?SMPmap = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@map Send X@S')) - (Var`\)" have "?SMPmap \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S')) - (Var`\)" using SMP_fun_map_snd_subset[of X f] SMP_append[of "map Send X" S'] SMP_Cons[of "snd\Fun f X\" S'] SMP_append[of S "snd\Fun f X\#S'"] SMP_append[of S "map Send X@S'"] by auto hence "\s \ ?SMPmap. \t \ ?SMPmap. (\\. Unifier \ s t) \ \ s = \ t" using Compose by (meson subsetCE) thus ?case using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Compose[OF Compose.hyps]], of S'] Compose.prems(4) unfolding trms\<^sub>s\<^sub>t_def by blast next case (Unify S f Y \ X S' \) let ?SMP\ = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \)) - (Var`\)" have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \)) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" proof fix s assume "s \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \))" thus "s \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" using LI_in_SMP_subset_single[ OF LI_rel.Unify[OF Unify.hyps] Unify.prems(1,2,4,5) MP_subset_SMP(2)[of "S@snd\Fun f X\#S'"] Unify.prems(3)] by (metis SMP_append' SMP_subset_union_eq Un_iff) qed hence "\s \ ?SMP\. \t \ ?SMP\. (\\. Unifier \ s t) \ \ s = \ t" using Unify.prems(4) by (meson Diff_iff subsetCE) thus ?case using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Unify[OF Unify.hyps]], of S'] Unify.prems(4) unfolding trms\<^sub>s\<^sub>t_def by blast next case (Equality S \ t t' S' \) let ?SMP\ = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \)) - (Var`\)" have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \)) \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \ t'#S'))" proof fix s assume "s \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \))" thus "s \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \ t'#S'))" using LI_in_SMP_subset_single[ OF LI_rel.Equality[OF Equality.hyps] Equality.prems(1,2,4,5) MP_subset_SMP(2)[of "S@t \ t'#S'"] Equality.prems(3)] by (metis SMP_append' SMP_subset_union_eq Un_iff) qed hence "\s \ ?SMP\. \t \ ?SMP\. (\\. Unifier \ s t) \ \ s = \ t" using Equality.prems by (meson Diff_iff subsetCE) thus ?case using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Equality[OF Equality.hyps]], of S'] Equality.prems unfolding trms\<^sub>s\<^sub>t_def by blast qed lemma LI_preserves_welltypedness_single: assumes "(S,\) \ (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' \ (\v. wf\<^sub>t\<^sub>r\<^sub>m (\' v))" using assms proof (induction rule: LI_rel.induct) case (Unify S f Y \ X S' \) have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(4) by simp moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" proof - obtain x where True "x \ set S" "Fun f Y \ trm\<^sub>s\<^sub>t\<^sub>p x" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" using Unify.hyps(2) Unify.prems(4) by auto thus ?thesis using wf_trm_subterm[OF \wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)\, of "Fun f Y"] by (cases "Fun f Y = trm\<^sub>s\<^sub>t\<^sub>p x", auto) qed moreover have "Fun f X \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" "Fun f Y \ SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" using SMP_append[of S "snd\Fun f X\#S'"] SMP_Cons[of "snd\Fun f X\" S'] SMP_ikI[OF Unify.hyps(2)] by auto hence "\ (Fun f X) = \ (Fun f Y)" using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]] by blast ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis have "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ \wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\]) hence "\v. wf\<^sub>t\<^sub>r\<^sub>m ((\ \\<^sub>s \) v)" unfolding subst_compose_def by (simp add: wf_trm_subst \\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\) thus ?case by (metis wt_subst_compose[OF \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\]) next case (Equality S \ t t' S' \) have "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" using Equality.prems(4) by simp_all moreover have "\ t = \ t'" using \eqs_tfr\<^sub>s\<^sub>t (S@t \ t'#S')\ MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]] by auto ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis have "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" by (meson mgu_wf_trm[OF Equality.hyps(2)[symmetric] \wf\<^sub>t\<^sub>r\<^sub>m t\ \wf\<^sub>t\<^sub>r\<^sub>m t'\]) hence "\v. wf\<^sub>t\<^sub>r\<^sub>m ((\ \\<^sub>s \) v)" unfolding subst_compose_def by (simp add: wf_trm_subst \\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\) thus ?case by (metis wt_subst_compose[OF \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\]) qed metis lemma LI_preserves_welltypedness: assumes "(S,\) \\<^sup>* (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' \ (\v. wf\<^sub>t\<^sub>r\<^sub>m (\' v))" using assms proof (induction S \ rule: converse_rtrancl_induct2) case (step S1 \1 S2 \2) hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2 \ (\v. wf\<^sub>t\<^sub>r\<^sub>m (\2 v))" using LI_preserves_welltypedness_single by presburger moreover have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \2" by (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)]) moreover have "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)" using LI_preserves_tfr_single[OF step.hyps(1)] step.prems by presburger moreover have "eqs_tfr\<^sub>s\<^sub>t S2" using LI_preserves_eqs_tfr_single[OF step.hyps(1)] step.prems by fastforce ultimately show ?case using step.IH by presburger qed simp lemma LI_preserves_tfr: assumes "(S,\) \\<^sup>* (S',\')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" shows "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" "eqs_tfr\<^sub>s\<^sub>t S'" using assms proof (induction S \ rule: converse_rtrancl_induct2) case refl { case 1 thus ?case by blast } { case 2 thus ?case by blast } next case (step S1 \1 S2 \2) { case 1 have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \2" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)" "eqs_tfr\<^sub>s\<^sub>t S2" apply (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] "1.prems"(1)]) apply (metis LI_preserves_tfr_single[OF step.hyps(1) "1.prems"(1,2)] "1.prems"(3,4,5)) by (metis LI_preserves_eqs_tfr_single[OF step.hyps(1) "1.prems"(1,2)] "1.prems"(3,4,5)) moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\2 v)" using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] "1.prems"] by simp_all ultimately show ?case using step.IH by presburger } { case 2 have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \2" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)" "eqs_tfr\<^sub>s\<^sub>t S2" apply (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] "2.prems"(1)]) apply (metis LI_preserves_tfr_single[OF step.hyps(1) "2.prems"(1,2)] "2.prems"(3,4,5)) by (metis LI_preserves_eqs_tfr_single[OF step.hyps(1) "2.prems"(1,2)] "2.prems"(3,4,5)) moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \2" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\2 v)" using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] "2.prems"] by simp_all ultimately show ?case using step.IH by presburger } qed subsection {* Well-typed satisfiable if simple *} (* Proving the existence of a well-typed, but not bijective, interpretation *) definition wt_interpretation_nonunique::"('fun,'var) subst" where "wt_interpretation_nonunique v \ (SOME t. \ (Var v) = \ t \ public_ground_wf_term t)" lemma wt_interpretation_nonunique_properties: "wt_interpretation_nonunique v = t \ \ (Var v) = \ t \ public_ground_wf_term t" using someI_ex[of "\t. \ (Var v) = \ t \ public_ground_wf_term t", OF type_pgwt_inhabited[of "Var v"]] unfolding wt_interpretation_nonunique_def wf\<^sub>t\<^sub>r\<^sub>m_def by simp lemma wt_interpretation_exists: obtains \::"('fun,'var) subst" where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ public_ground_wf_terms" proof - have "\v. wt_interpretation_nonunique v \ Var v" using wt_interpretation_nonunique_properties pgwt_ground by force hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique = UNIV" by auto moreover have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (simp add: wt_interpretation_nonunique_properties pgwt_ground) ultimately have "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique" by metis moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique" unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using wt_interpretation_nonunique_properties by simp moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique \ public_ground_wf_terms" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (auto simp add: wt_interpretation_nonunique_properties) ultimately show ?thesis using that by auto qed lemma wt_bij_finite_tatom_subst_exists_single: assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)" and "\x. x \ S \ \ (Var x) = TAtom a" shows "\\::('fun,'var) 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 []) ` {c. \ (Fun c []) = TAtom a \ public c \ arity c = 0}) - T \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x))" proof - let ?U = "{c. \ (Fun c []) = TAtom a \ public c \ arity c = 0}" 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) - T" using bij_finite_const_subst_exists'[OF assms(1,2) infinite_typed_consts'[of a]] by auto { fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "\ (Var x) = \ (\ x)" by auto } moreover { fix x assume "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "\c \ ?U. \ x = Fun c [] \ arity c = 0" using \ by auto hence "\ (\ x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using assms(3) const_type wf_trmI[of "[]"] by auto hence "\ (Var x) = \ (\ x)" "wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using assms(3) \(1) by force+ } ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+ thus ?thesis using \ by auto qed lemma wt_bij_finite_tatom_subst_exists: assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)" and "\x. x \ S \ \a. \ (Var x) = TAtom a" shows "\\::('fun,'var) 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 []) ` \\<^sub>p\<^sub>u\<^sub>b) - T \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x))" using assms proof (induction rule: finite_induct) case empty have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var = {}" "bij_betw Var (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var)" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var \ ((\c. Fun c []) ` \\<^sub>p\<^sub>u\<^sub>b) - T" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" "\x. wf\<^sub>t\<^sub>r\<^sub>m (Var x)" unfolding bij_betw_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto thus ?case by auto next case (insert x S) then obtain a where a: "\ (Var x) = TAtom a" by fastforce from insert 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 []) ` \\<^sub>p\<^sub>u\<^sub>b) - T" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" by auto let ?S' = "{y \ S. \ (Var y) = TAtom a}" let ?T' = "T \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" have *: "finite (insert x ?S')" using insert by simp have **: "finite ?T'" using insert.prems(1) insert.hyps(1) \(1) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp have ***: "\y. y \ insert x ?S' \ \ (Var y) = TAtom a" using a by auto obtain \ where \: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = insert x ?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 []) ` \\<^sub>p\<^sub>u\<^sub>b) - ?T'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using wt_bij_finite_tatom_subst_exists_single[OF * ** ***] const_type_inv[of _ "[]" a] unfolding \\<^sub>p\<^sub>u\<^sub>b_def \_def \n_def by blast obtain \ where \: "\ \ \y. if x = y then \ y else \ y" by simp have x_dom: "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using insert.hyps(2) \(1) \(1) \ by auto moreover have ground_imgs: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using pgwt_ground \(3) \(3) by auto ultimately have x_img: "\ x \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ x \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using ground_subst_dom_iff_img by auto have "ground (insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \))" using ground_imgs x_dom by auto have \_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = insert x (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using \(1) \ by auto have \_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" proof show "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" proof fix t assume "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" then obtain y where "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "t = \ y" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto thus "t \ insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using \ by auto qed show "insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof fix t assume t: "t \ insert (\ x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" hence "FV t = {}" using ground_imgs x_img(2) by auto hence "t \ Var x" by auto show "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof (cases "t = \ x") case True thus ?thesis using subst_imgI \ \t \ Var x\ by metis next case False hence "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using t by auto then obtain y where "\ y \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "t = \ y" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto hence "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "t \ Var y" using ground_subst_dom_iff_img[OF ground_imgs(1)] by auto hence "x \ y" using x_dom by auto hence "\ y = \ y" unfolding \ by auto thus ?thesis using \t \ Var y\ \t = \ y\ subst_imgI[of \ y] by auto qed qed qed hence \_ground_img: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using ground_imgs x_img by auto have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = insert x S" using \_dom \(1) by auto moreover have "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 (intro bij_betwI') fix y z assume *: "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" hence "FV (\ y) = {}" "FV (\ z) = {}" using \_ground_img by auto { assume "\ y = \ z" hence "y = z" proof (cases "\ y \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ z \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \") case True hence **: "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \ \_dom x_img(2) \(3) True by (metis *(1) DiffE Un_upper2 insertE subsetCE, metis *(2) DiffE Un_upper2 insertE subsetCE) hence "y \ x" "z \ x" using x_dom by auto hence "\ y = \ y" "\ z = \ z" using \ by auto thus ?thesis using \\ y = \ z\ \(2) ** unfolding bij_betw_def inj_on_def by auto qed (metis \ * \\ y = \ z\ \_dom ground_imgs(1) ground_subst_dom_iff_img insertE) } thus "(\ y = \ z) = (y = z)" by auto next fix y assume "y \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" thus "\ y \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by auto next fix t assume "t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" thus "\z \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. t = \ z" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto qed moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\c. Fun c []) ` \\<^sub>p\<^sub>u\<^sub>b - T" using \(3) \(3) \ unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \(4) \(4) \ unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto moreover have "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using \ \(5) \(5) by simp ultimately show ?case by blast qed lemma strand_FV_bvars_disjointD: assumes "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\X\t \ t'\ \ set S" shows "set X \ bvars\<^sub>s\<^sub>t S" "(FV t \ FV t') - set X \ FV\<^sub>s\<^sub>t S" using assms by (induct S) auto lemma strand_FV_bvars_disjoint_unfold: assumes "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\X\t \ t'\ \ set S" "\Y\u \ u'\ \ set S" shows "set Y \ ((FV t \ FV t') - set X) = {}" proof - have "set X \ bvars\<^sub>s\<^sub>t S" "set Y \ bvars\<^sub>s\<^sub>t S" "(FV t \ FV t') - set X \ FV\<^sub>s\<^sub>t S" "(FV u \ FV u') - set Y \ FV\<^sub>s\<^sub>t S" using strand_FV_bvars_disjointD[OF assms(1)] assms(2,3) by auto thus ?thesis using assms(1) by auto qed theorem wt_sat_if_simple: assumes "simple S" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" and \': "\X t t' \. \X\t \ t'\ \ set S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = set X \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ t \ \ \ \' \ t' \ \ \ \'" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \')" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' = {x \ vars\<^sub>s\<^sub>t S. \X t t'. \X\t \ t'\ \ set S \ x \ FV t \ FV t' \ x \ set X}" and eqs_tfr: "eqs_tfr\<^sub>s\<^sub>t S" shows "\\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ \\<^sub>c \S, \\ \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x))" proof - from \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \\ have "wf\<^sub>s\<^sub>t {} S" "Idem \" and S_\_disj: "\v. v \ vars\<^sub>s\<^sub>t S \ \ v = Var v" using IdemI[of \] by auto obtain \::"('fun,'var) subst" where \: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ public_ground_wf_terms" using wt_interpretation_exists by blast hence \_deduct: "\x M. M \\<^sub>c \ x" and \_wf_trm: "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using pgwt_deducible pgwt_wellformed by fastforce+ let ?P = "\\ X. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = set X \ ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" let ?Sineqsvars = "{x \ vars\<^sub>s\<^sub>t S. \X t t'. \X\t \ t'\ \ set S \ x \ FV t \ FV t' \ x \ set X}" let ?Strms = "\(subterms ` trms\<^sub>s\<^sub>t S)" have *: "finite ?Sineqsvars" "finite ?Strms" "\x. x \ ?Sineqsvars \ \a. \ (Var x) = TAtom a" using eqs_tfr by auto have "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" using \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \\ unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by metis hence ineqs_vars_not_bound: "\X t t' x. \X\t \ t'\ \ set S \ x \ ?Sineqsvars \ x \ set X" using strand_FV_bvars_disjoint_unfold by blast obtain \::"('fun,'var) subst" where \_FV_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = ?Sineqsvars" and \_bij_dom_img: "bij_betw \ (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" and \_fresh_pub_consts_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ ((\c. Fun c []) ` \\<^sub>p\<^sub>u\<^sub>b) - ?Strms" and \_wt: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" and \_wf_trm: "\x. wf\<^sub>t\<^sub>r\<^sub>m (\ x)" using wt_bij_finite_tatom_subst_exists[OF *] by blast have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ public_ground_wf_terms - ?Strms" and \_pgwt_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ public_ground_wf_terms" using \_fresh_pub_consts_img pgwt_is_empty_synth public_const_deduct(2) by auto have \_img_ground: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" using \_pgwt_img pgwt_ground by auto hence "inj \" using \_bij_dom_img subst_inj_is_bij_betw_dom_img_if_ground_img unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto have "\t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. t = Fun c []" using \_fresh_pub_consts_img by auto have \_ineqs_FV_dom: "\X t t'. \X\t \ t'\ \ set S \ FV t \ FV t' - set X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \_FV_dom by fastforce have "\X t t'. \X\t \ t'\ \ set S \ \u \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. u \ subterms t \ subterms t'" using \_pgwt_img PGWT[of _ "[]"] \img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ public_ground_wf_terms - ?Strms\ by force moreover have "\X t t'. \X\t \ t'\ \ set S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ set X = {}" using ineqs_vars_not_bound \_FV_dom by fastforce moreover have "\X t t' \. \X\t \ t'\ \ set S \ FV t \ FV t' - set X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" using \'(3) ineqs_vars_not_bound by fastforce moreover have "\X t t'. \X\t \ t'\ \ set S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' \ set X = {}" using \'(3) ineqs_vars_not_bound by blast moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \' = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using \'(3) \_FV_dom by metis ultimately have \_ineqs_neq: "\X t t' \. \X\t \ t'\ \ set S \ ?P \ X \ t \ \ \ \ \ t' \ \ \ \" using \'(1,2) sat_ineq_inj_const_subst[OF \inj \\ \\t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. \c. t = Fun c []\] by meson from \_ineqs_FV_dom have \_ineqs_FV_dom': "\X t t' \. \X\t \ t'\ \ set S \ ?P \ X \ FV (t \ \) \ FV (t' \ \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (simp add: Un_Diff subst_FV_unfold_ground_img) hence \_ineqs_ground: "\X t t' \. \X\t \ t'\ \ set S \ ?P \ X \ FV (t \ \ \ \) = {}" "\X t t' \. \X\t \ t'\ \ set S \ ?P \ X \ FV (t' \ \ \ \) = {}" using subst_FV_dom_ground_if_ground_img \_img_ground by (metis Un_subset_iff)+ from \_pgwt_img \_ineqs_neq have \_deduct: "\x M. x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ M \\<^sub>c \ x" using pgwt_deducible by fastforce { fix M::"('fun,'var) terms" have "\M; S\\<^sub>c (\ \\<^sub>s \ \\<^sub>s \)" using \wf\<^sub>s\<^sub>t {} S\ \simple S\ S_\_disj \_ineqs_neq \_ineqs_FV_dom' proof (induction S arbitrary: M rule: wf\<^sub>s\<^sub>t_simple_induct) case (ConsSnd v S) hence S_sat: "\M; S\\<^sub>c (\ \\<^sub>s \ \\<^sub>s \)" and "\ v = Var v" by auto have "\M. M \\<^sub>c Var v \ (\ \\<^sub>s \ \\<^sub>s \)" proof (cases "\ v = Var v") case True thus "\M. M \\<^sub>c Var v \ (\ \\<^sub>s \ \\<^sub>s \)" using \_deduct \\ v = Var v\ by auto next case False hence "v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "Var v \ (\ \\<^sub>s \ \\<^sub>s \) = \ v" using \_pgwt_img \\ v = Var v\ pgwt_ground by auto thus "\M. M \\<^sub>c Var v \ (\ \\<^sub>s \ \\<^sub>s \)" by (metis \_deduct) qed thus ?case using strand_sem_append[OF S_sat] by (metis strand_sem_c.simps(1,2)) next case (ConsIneq X t t' S) from ConsIneq.prems(1) have "t \ \ = t" "t' \ \ = t'" by auto hence *: "\\. ?P \ X \ t \ \ \ \ = t \ \" "\\. ?P \ X \ t' \ \ \ \ = t' \ \" by (metis ground_subst_FV_subset subst_apply_term_empty vars_term_subset_subst_eq)+ from ConsIneq have "\\. ?P \ X \ t \ \ \ \ \ t' \ \ \ \" and IH: "\M; S\\<^sub>c (\ \\<^sub>s \ \\<^sub>s \)" by (meson in_set_conv_decomp, fastforce) moreover have "\\. ?P \ X \ FV (t \ \ \ \) = {}" "\\. ?P \ X \ FV (t' \ \ \ \) = {}" using ConsIneq.prems(3)[of X t t'] subst_FV_dom_ground_if_ground_img[OF _ \_img_ground] by auto ultimately have "\\. ?P \ X \ t \ \ \ \ \ \ \ t' \ \ \ \ \ \" by (simp add: subst_ground_ident) hence "\\. ?P \ X \ t \ \ \ (\ \\<^sub>s \ \\<^sub>s \) \ t' \ \ \ (\ \\<^sub>s \ \\<^sub>s \)" using * by simp thus ?case using IH by auto qed auto } moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\ \\<^sub>s \ \\<^sub>s \)" by (metis wt_subst_compose \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\) moreover have "\x. wf\<^sub>t\<^sub>r\<^sub>m ((\ \\<^sub>s \ \\<^sub>s \) x)" using assms(4) \_wf_trm \_wf_trm by (simp add: subst_compose_def wf_trm_subst) ultimately show ?thesis using interpretation_comp(1)[OF \interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\, of "\ \\<^sub>s \"] Idem_support[OF \Idem \\, of "\ \\<^sub>s \"] comp_assoc unfolding constr_sem_c_def by metis qed subsection {* The typing result *} theorem wt_attack_if_tfr_attack: assumes "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ \\<^sub>c \S, \\" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" and "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "\\\<^sub>\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ \\<^sub>\ \\<^sub>c \S, \\ \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\\<^sub>\ x))" proof - obtain S' \' where *: "simple S'" "(S,\) \\<^sup>* (S',\')" "\{}; S'\\<^sub>c \" using LI_completeness[OF assms(3,2)] unfolding constr_sem_c_def by (meson in_subterms_refl) have **: "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S' \'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \'" "eqs_tfr\<^sub>s\<^sub>t S'" "\v. wf\<^sub>t\<^sub>r\<^sub>m (\' v)" using LI_preserves_welltypedness[OF *(2) assms(3,4,7)] assms(5,6) LI_preserves_wellformedness[OF *(2) assms(3)] LI_preserves_tfr[OF *(2) assms(3,4,7,5,6)] apply (blast,blast,blast) by (metis LI_preserves_welltypedness[OF *(2) assms(3,4,7)] assms(5,6)) def A \ "{x \ vars\<^sub>s\<^sub>t S'. \X t t'. \X\t \ t'\ \ set S' \ x \ FV t \ FV t' \ x \ set X}" def B \ "UNIV - A" let ?\ = "rm_vars B \" have gr\: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\)" using assms(1) rm_vars_img_subset[of B \] by auto { fix X t t' and \::"('fun,'var) subst" assume "\X\t \ t'\ \ set S'" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = set X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \)" hence "t \ \ \ \ \ t' \ \ \ \" using strand_sem_c_imp_ineqs_neq[OF *(3)] by auto hence "t \ \ \ ?\ \ t' \ \ \ ?\" using Unifier_ground_rm_vars[OF gr\(1), of "t \ \" B "t' \ \"] by auto } moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = UNIV" using assms(1) by metis hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\ = A" using rm_vars_dom[of B \] B_def by blast ultimately obtain \\<^sub>\ where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\" "\\<^sub>\ \\<^sub>c \S', \'\" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\\<^sub>\ x)" using wt_sat_if_simple[OF *(1) **(1,2,4) _ gr\(2) _ **(3)] A_def by moura thus ?thesis using LI_soundness[OF assms(3) *(2)] by metis qed corollary secure_if_wt_secure: assumes "\(\\\<^sub>\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ \\<^sub>\ \\<^sub>c \S, \\ \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\)" and "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S" and "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" shows "\(\\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ \ \\<^sub>c \S, \\)" using wt_attack_if_tfr_attack[OF _ _ assms(2,3,4,5)] assms(1,6) by blast end end