(* (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: ProtocolTransitionSystem.thy Author: Andreas Viktor Hess, DTU *) section {* Theory: Formalization of the Main Typing Result *} theory ProtocolTransitionSystem imports TypedModel begin (* Strands extended with "decomposition steps" *) datatype (funs\<^sub>e\<^sub>s\<^sub>t\<^sub>p: 'a, vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p: 'b) extstrand_step = Step "('a,'b) strand_step" | Decomp (trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") where "trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p (Step x) = trm\<^sub>s\<^sub>t\<^sub>p x" fun trm_r\<^sub>e\<^sub>s\<^sub>t\<^sub>p where "trm_r\<^sub>e\<^sub>s\<^sub>t\<^sub>p (Step x) = trm_r\<^sub>s\<^sub>t\<^sub>p x" | "trm_r\<^sub>e\<^sub>s\<^sub>t\<^sub>p (Decomp t) = t" context typed_model begin subsection {* Preliminary definitions *} type_synonym ('a,'b) protocol = "('a,'b) strands" definition decomp::"('fun,'var) term \ ('fun,'var) strand" where "decomp t \ (case (Ana t) of (K,T) \ snd\t\#map Send (inv set K)@map Receive (inv set T))" definition trms\<^sub>e\<^sub>s\<^sub>t where "trms\<^sub>e\<^sub>s\<^sub>t S \ trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p ` set S \ trm_r\<^sub>e\<^sub>s\<^sub>t\<^sub>p ` set S" declare trms\<^sub>e\<^sub>s\<^sub>t_def[simp] type_synonym ('a,'b) extstrand = "('a,'b) extstrand_step list" type_synonym ('a,'b) extstrands = "('a,'b) extstrand set" fun to_st where "to_st [] = []" | "to_st (Step x#S) = x#(to_st S)" | "to_st (Decomp t#S) = (decomp t)@(to_st S)" fun to_est where "to_est [] = []" | "to_est (x#S) = Step x#to_est S" abbreviation ik\<^sub>e\<^sub>s\<^sub>t where "ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>s\<^sub>t (to_st A)" abbreviation wf\<^sub>e\<^sub>s\<^sub>t where "wf\<^sub>e\<^sub>s\<^sub>t V A \ wf\<^sub>s\<^sub>t V (to_st A)" abbreviation eqs_rhs\<^sub>e\<^sub>s\<^sub>t where "eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>s\<^sub>t (to_st A)" abbreviation vars\<^sub>e\<^sub>s\<^sub>t where "vars\<^sub>e\<^sub>s\<^sub>t A \ vars\<^sub>s\<^sub>t (to_st A)" abbreviation vars2\<^sub>e\<^sub>s\<^sub>t where "vars2\<^sub>e\<^sub>s\<^sub>t A \ vars2\<^sub>s\<^sub>t (to_st A)" abbreviation bvars\<^sub>e\<^sub>s\<^sub>t where "bvars\<^sub>e\<^sub>s\<^sub>t A \ bvars\<^sub>s\<^sub>t (to_st A)" abbreviation FV\<^sub>e\<^sub>s\<^sub>t where "FV\<^sub>e\<^sub>s\<^sub>t A \ FV\<^sub>s\<^sub>t (to_st A)" abbreviation funs\<^sub>e\<^sub>s\<^sub>t where "funs\<^sub>e\<^sub>s\<^sub>t A \ funs\<^sub>s\<^sub>t (to_st A)" fun dual\<^sub>s\<^sub>t::"('a,'b) strand \ ('a,'b) strand" where "dual\<^sub>s\<^sub>t [] = []" | "dual\<^sub>s\<^sub>t (rcv\t\#S) = snd\t\#(dual\<^sub>s\<^sub>t S)" | "dual\<^sub>s\<^sub>t (snd\t\#S) = rcv\t\#(dual\<^sub>s\<^sub>t S)" | "dual\<^sub>s\<^sub>t (x#S) = x#(dual\<^sub>s\<^sub>t S)" definition wf\<^sub>s\<^sub>t\<^sub>s'::"('fun,'var) protocol \ ('fun,'var) extstrand \ bool" where "wf\<^sub>s\<^sub>t\<^sub>s' \ \ \ (\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t S)) \ (\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}) \ (\S \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t \ = {}) \ (\S \ \. FV\<^sub>s\<^sub>t (to_st \) \ bvars\<^sub>s\<^sub>t S = {})" definition wf\<^sub>s\<^sub>t\<^sub>s::"('fun,'var) protocol \ bool" where "wf\<^sub>s\<^sub>t\<^sub>s \ \ (\S \ \. wf\<^sub>s\<^sub>t {} (dual\<^sub>s\<^sub>t S)) \ (\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {})" inductive well_analyzed::"('fun,'var) extstrand \ bool" where Nil[simp]: "well_analyzed []" | Step: "well_analyzed A \ well_analyzed (A@[Step x])" | Decomp: "\well_analyzed A; t \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)) - (Var ` \)\ \ well_analyzed (A@[Decomp t])" definition Ana_invar_subst: "Ana_invar_subst \ \ (\f T K M \. Fun f T \ \(subterms ` \) \ Ana (Fun f T) = (K, M) \ Ana (Fun f T \ \) = (K \set \, M \set \))" declare Ana_invar_subst[simp] fun subst_apply_extstrandstep where "subst_apply_extstrandstep (Step x) \ = Step (x \\<^sub>s\<^sub>t\<^sub>p \)" | "subst_apply_extstrandstep (Decomp t) \ = Decomp (t \ \)" definition subst_apply_extstrandstep' (infix "\\<^sub>e\<^sub>s\<^sub>t\<^sub>p" 51) where "x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ \ subst_apply_extstrandstep x \" declare subst_apply_extstrandstep'_def[simp] lemma subst_apply_extstrandstep'_simps[simp]: "(Step (Send t)) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = Step (Send (t \ \))" "(Step (Receive t)) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = Step (Receive (t \ \))" "(Step (Equality t t')) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = Step (Equality (t \ \) (t' \ \))" "(Step (Inequality X t t')) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = Step (Inequality X (t \ rm_vars (set X) \) (t' \ rm_vars (set X) \))" by simp_all lemma vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p_subst_apply_simps[simp]: "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p ((Step (Send t)) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = FV (t \ \)" "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p ((Step (Receive t)) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = FV (t \ \)" "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p ((Step (Equality t t')) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = FV (t \ \) \ FV (t' \ \)" "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p ((Step (Inequality X t t')) \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = set X \ FV (t \ rm_vars (set X) \) \ FV (t' \ rm_vars (set X) \)" by simp_all definition subst_apply_extstrand (infix "\\<^sub>e\<^sub>s\<^sub>t" 51) where "S \\<^sub>e\<^sub>s\<^sub>t \ \ map (\x. x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) S" abbreviation update\<^sub>s\<^sub>t::"('fun,'var) protocol \ ('fun,'var) strand \ ('fun,'var) protocol" where "update\<^sub>s\<^sub>t \ S \ (case S of Nil \ \ - {S} | Cons _ S' \ insert S' (\ - {S}))" inductive_set decomps\<^sub>e\<^sub>s\<^sub>t::"('fun,'var) terms \ ('fun,'var) terms \ ('fun,'var) subst \ ('fun,'var) extstrands" (* \: intruder knowledge \: additional messages *) for \ and \ and \ where Nil: "[] \ decomps\<^sub>e\<^sub>s\<^sub>t \ \ \" | Decomp: "\\ \ decomps\<^sub>e\<^sub>s\<^sub>t \ \ \; Fun f T \ \(subterms ` (\ \ \)); Ana (Fun f T) = (K,M); M \ {}; (\ \ ik\<^sub>e\<^sub>s\<^sub>t \) \set \ \\<^sub>c Fun f T \ \; \k. k \ K \ (\ \ ik\<^sub>e\<^sub>s\<^sub>t \) \set \ \\<^sub>c k \ \\ \ \@[Decomp (Fun f T)] \ decomps\<^sub>e\<^sub>s\<^sub>t \ \ \" fun decomp_rm\<^sub>e\<^sub>s\<^sub>t::"('fun,'var) extstrand \ ('fun,'var) extstrand" where "decomp_rm\<^sub>e\<^sub>s\<^sub>t [] = []" | "decomp_rm\<^sub>e\<^sub>s\<^sub>t (Decomp t#S) = decomp_rm\<^sub>e\<^sub>s\<^sub>t S" | "decomp_rm\<^sub>e\<^sub>s\<^sub>t (Step x#S) = Step x#(decomp_rm\<^sub>e\<^sub>s\<^sub>t S)" inductive sem\<^sub>e\<^sub>s\<^sub>t_d::"('fun,'var) terms \ ('fun,'var) subst \ ('fun,'var) extstrand \ bool" where Nil[simp]: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ []" | Send: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ S \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \ t \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (S@[Step (Send t)])" | Receive: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ S \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (S@[Step (Receive t)])" | Equality: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ S \ t \ \ = t' \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (S@[Step (Equality t t')])" | Inequality: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ 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' \ \ \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (S@[Step (Inequality X t t')])" | Decompose: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ S \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \ t \ \ \ Ana t = (K, M) \ (\k. k \ K \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \ k \ \) \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (S@[Decomp t])" inductive sem\<^sub>e\<^sub>s\<^sub>t_c::"('fun,'var) terms \ ('fun,'var) subst \ ('fun,'var) extstrand \ bool" where Nil[simp]: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ []" | Send: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ S \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \\<^sub>c t \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (S@[Step (Send t)])" | Receive: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ S \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (S@[Step (Receive t)])" | Equality: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ S \ t \ \ = t' \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (S@[Step (Equality t t')])" | Inequality: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ 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' \ \ \ \ \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (S@[Step (Inequality X t t')])" | Decompose: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ S \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \\<^sub>c t \ \ \ Ana t = (K, M) \ (\k. k \ K \ (ik\<^sub>e\<^sub>s\<^sub>t S \ M\<^sub>0) \set \ \\<^sub>c k \ \) \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (S@[Decomp t])" subsection {* Preliminary lemmas *} lemma wf\<^sub>s\<^sub>t\<^sub>s_wf\<^sub>s\<^sub>t\<^sub>s': "wf\<^sub>s\<^sub>t\<^sub>s \ = wf\<^sub>s\<^sub>t\<^sub>s' \ []" unfolding wf\<^sub>s\<^sub>t\<^sub>s_def wf\<^sub>s\<^sub>t\<^sub>s'_def by auto lemma decomp_ik: assumes "Ana t = (K,M)" shows "ik\<^sub>s\<^sub>t (decomp t) = M" proof - have "set (inv set M) = M" using someI_ex[OF finite_list[OF Ana_finite(2)[OF assms]]] unfolding inv_def by metis hence "ik\<^sub>s\<^sub>t (map Receive (inv set M)) = M" using ik_rcv_map[of _ "inv set M"] ik_rcv_map'[of _ "inv set M"] by blast thus "ik\<^sub>s\<^sub>t (decomp t) = M" unfolding decomp_def inv_def using assms by simp qed lemma decomp_ik_subset: "ik\<^sub>s\<^sub>t (decomp (Fun f T)) \ set T" proof - obtain K M where Ana: "Ana (Fun f T) = (K, M)" by moura show ?thesis using decomp_ik[OF Ana] Ana_fun_subterm[OF Ana] by blast qed lemma decomp_eqs_rhs_empty: assumes "Ana t = (K,M)" shows "eqs_rhs\<^sub>s\<^sub>t (decomp t) = {}" proof - have "set (inv set K) = K" "set (inv set M) = M" using someI_ex[OF finite_list[OF Ana_finite(1)[OF assms]]] someI_ex[OF finite_list[OF Ana_finite(2)[OF assms]]] unfolding inv_def by metis+ hence "eqs_rhs\<^sub>s\<^sub>t (map Receive (inv set K)) = {}" "eqs_rhs\<^sub>s\<^sub>t (map Receive (inv set M)) = {}" by auto thus "eqs_rhs\<^sub>s\<^sub>t (decomp t) = {}" unfolding decomp_def inv_def using assms by auto qed lemma trms\<^sub>e\<^sub>s\<^sub>t_append: "trms\<^sub>e\<^sub>s\<^sub>t (A@B) = trms\<^sub>e\<^sub>s\<^sub>t A \ trms\<^sub>e\<^sub>s\<^sub>t B" by auto lemma trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ikI: "t \ ik\<^sub>e\<^sub>s\<^sub>t A \ t \ \(subterms ` (trms\<^sub>e\<^sub>s\<^sub>t A))" proof (induction A rule: to_st.induct) case (2 x S) thus ?case by (cases x) auto next case (3 t' A) obtain K M where Ana: "Ana t' = (K,M)" by (metis surj_pair) from 3 show ?case proof (cases "t \ ik\<^sub>e\<^sub>s\<^sub>t A") case False hence "t \ ik\<^sub>s\<^sub>t (to_st [Decomp t'])" using 3 by auto hence "t \ M" using decomp_ik[OF Ana] by simp thus ?thesis using Ana_subterm[OF Ana] by auto qed auto qed auto lemma trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhsI: "t \ ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \ t \ \(subterms ` (trms\<^sub>e\<^sub>s\<^sub>t A))" proof (induction A rule: to_st.induct) case (2 x S) thus ?case by (cases x) auto next case (3 t' A) obtain K M where Ana: "Ana t' = (K,M)" by (metis surj_pair) from 3 show ?case proof (cases "t \ ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A") case False hence "t \ ik\<^sub>e\<^sub>s\<^sub>t [Decomp t'] \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t [Decomp t']" using 3(2) by auto hence "t \ M" using decomp_ik[OF Ana] decomp_eqs_rhs_empty[OF Ana] by simp thus ?thesis using Ana_subterm[OF Ana] by auto qed auto qed auto lemma trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_subtermsI: assumes "t \ \(subterms ` ik\<^sub>e\<^sub>s\<^sub>t A)" shows "t \ \(subterms ` (trms\<^sub>e\<^sub>s\<^sub>t A))" proof - obtain t' where "t' \ ik\<^sub>e\<^sub>s\<^sub>t A" "t \ t'" using trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ikI assms by auto thus ?thesis by (meson contra_subsetD in_subterms_subset_Union subtermeq_def trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ikI) qed lemma trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhs_subtermsI: assumes "t \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))" shows "t \ \(subterms ` (trms\<^sub>e\<^sub>s\<^sub>t A))" proof - obtain t' where "t' \ ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A" "t \ t'" using trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhsI assms by auto thus ?thesis by (meson contra_subsetD in_subterms_subset_Union subtermeq_def trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhsI) qed lemma trm\<^sub>e\<^sub>s\<^sub>t\<^sub>pD: "t \ trms\<^sub>e\<^sub>s\<^sub>t A \ t \ trms\<^sub>s\<^sub>t (to_st A)" proof (induction A) case (Cons a A) obtain K M where Ana: "Ana t = (K,M)" by (metis surj_pair) hence "\C. decomp t = snd\t\#C" unfolding decomp_def by simp hence *: "t \ trms\<^sub>s\<^sub>t (decomp t)" unfolding trms\<^sub>s\<^sub>t_def by force show ?case proof (cases "t \ trms\<^sub>e\<^sub>s\<^sub>t A") case True thus ?thesis using Cons.IH by (cases a) auto next case False thus ?thesis using * Cons.prems by (cases a) auto qed qed simp lemma subst_apply_extstrand_nil[simp]: "[] \\<^sub>e\<^sub>s\<^sub>t \ = []" unfolding subst_apply_extstrand_def by simp lemma subst_apply_extstrand_singleton[simp]: "[Step (Receive t)] \\<^sub>e\<^sub>s\<^sub>t \ = [Step (Receive (t \ \))]" "[Step (Send t)] \\<^sub>e\<^sub>s\<^sub>t \ = [Step (Send (t \ \))]" "[Step (Equality t t')] \\<^sub>e\<^sub>s\<^sub>t \ = [Step (Equality (t \ \) (t' \ \))]" "[Decomp t] \\<^sub>e\<^sub>s\<^sub>t \ = [Decomp (t \ \)]" unfolding subst_apply_extstrand_def by auto lemma vars\<^sub>e\<^sub>s\<^sub>t_nil[simp]: "vars\<^sub>e\<^sub>s\<^sub>t [] = {}" by simp lemma extstrand_subst_hom: "(S@S') \\<^sub>e\<^sub>s\<^sub>t \ = (S \\<^sub>e\<^sub>s\<^sub>t \)@(S' \\<^sub>e\<^sub>s\<^sub>t \)" "(x#S) \\<^sub>e\<^sub>s\<^sub>t \ = (x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \)#(S \\<^sub>e\<^sub>s\<^sub>t \)" unfolding subst_apply_extstrand_def by auto lemma decomp_vars: "vars2\<^sub>s\<^sub>t (decomp t) = FV t" "vars\<^sub>s\<^sub>t (decomp t) = FV t" "bvars\<^sub>s\<^sub>t (decomp t) = {}" "FV\<^sub>s\<^sub>t (decomp t) = FV t" proof - obtain K M where Ana: "Ana t = (K,M)" "finite K" "finite M" by (metis surj_pair Ana_finite) hence "decomp t = snd\t\#map Send (inv set K)@map Receive (inv set M)" unfolding decomp_def by simp moreover have "\set (map FV (inv set K)) = FV\<^sub>s\<^sub>e\<^sub>t K" "\set (map FV (inv set M)) = FV\<^sub>s\<^sub>e\<^sub>t M" using inv_set_FV[OF \finite K\] inv_set_FV[OF \finite M\] by auto moreover have "FV\<^sub>s\<^sub>e\<^sub>t K \ FV t" "FV\<^sub>s\<^sub>e\<^sub>t M \ FV t" using Ana_subterm[OF Ana(1)] Ana_keys_FV[OF Ana(1)] by (simp_all add: UN_least psubsetD subtermeq_vars_subset) ultimately show "vars2\<^sub>s\<^sub>t (decomp t) = FV t" "vars\<^sub>s\<^sub>t (decomp t) = FV t" "bvars\<^sub>s\<^sub>t (decomp t) = {}" "FV\<^sub>s\<^sub>t (decomp t) = FV t" by auto qed lemma bvars\<^sub>e\<^sub>s\<^sub>t_cons: "bvars\<^sub>e\<^sub>s\<^sub>t (x#X) = bvars\<^sub>e\<^sub>s\<^sub>t [x] \ bvars\<^sub>e\<^sub>s\<^sub>t X" by (cases x) auto lemma bvars\<^sub>e\<^sub>s\<^sub>t_append: "bvars\<^sub>e\<^sub>s\<^sub>t (A@B) = bvars\<^sub>e\<^sub>s\<^sub>t A \ bvars\<^sub>e\<^sub>s\<^sub>t B" proof (induction A) case (Cons x A) hence "bvars\<^sub>e\<^sub>s\<^sub>t ((x#A)@B) = bvars\<^sub>e\<^sub>s\<^sub>t [x] \ bvars\<^sub>e\<^sub>s\<^sub>t A \ bvars\<^sub>e\<^sub>s\<^sub>t B" using bvars\<^sub>e\<^sub>s\<^sub>t_cons[of x "A@B"] by auto thus ?case using bvars\<^sub>e\<^sub>s\<^sub>t_cons[of x A] by auto qed simp lemma FV\<^sub>e\<^sub>s\<^sub>t_cons: "FV\<^sub>e\<^sub>s\<^sub>t (x#X) = FV\<^sub>e\<^sub>s\<^sub>t [x] \ FV\<^sub>e\<^sub>s\<^sub>t X" by (cases x) auto lemma FV\<^sub>e\<^sub>s\<^sub>t_append: "FV\<^sub>e\<^sub>s\<^sub>t (A@B) = FV\<^sub>e\<^sub>s\<^sub>t A \ FV\<^sub>e\<^sub>s\<^sub>t B" proof (induction A) case (Cons x A) hence "FV\<^sub>e\<^sub>s\<^sub>t ((x#A)@B) = FV\<^sub>e\<^sub>s\<^sub>t [x] \ FV\<^sub>e\<^sub>s\<^sub>t A \ FV\<^sub>e\<^sub>s\<^sub>t B" using FV\<^sub>e\<^sub>s\<^sub>t_cons[of x "A@B"] by auto thus ?case using FV\<^sub>e\<^sub>s\<^sub>t_cons[of x A] by auto qed simp lemma vars\<^sub>e\<^sub>s\<^sub>t_cons: "vars\<^sub>e\<^sub>s\<^sub>t (x#X) = vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p x \ vars\<^sub>e\<^sub>s\<^sub>t X" using decomp_vars proof (cases x) case (Step y) thus ?thesis by (cases y) auto qed auto lemma vars\<^sub>e\<^sub>s\<^sub>t_append: "vars\<^sub>e\<^sub>s\<^sub>t (A@B) = vars\<^sub>e\<^sub>s\<^sub>t A \ vars\<^sub>e\<^sub>s\<^sub>t B" using vars\<^sub>e\<^sub>s\<^sub>t_cons by (induct A) auto lemma vars\<^sub>e\<^sub>s\<^sub>t_cons_subst: "vars\<^sub>e\<^sub>s\<^sub>t (x#X \\<^sub>e\<^sub>s\<^sub>t \) = vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) \ vars\<^sub>e\<^sub>s\<^sub>t (X \\<^sub>e\<^sub>s\<^sub>t \)" using vars\<^sub>e\<^sub>s\<^sub>t_cons extstrand_subst_hom(2)[of x X \] by simp lemma vars\<^sub>e\<^sub>s\<^sub>t_append_subst: "vars\<^sub>e\<^sub>s\<^sub>t (A@B \\<^sub>e\<^sub>s\<^sub>t \) = vars\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) \ vars\<^sub>e\<^sub>s\<^sub>t (B \\<^sub>e\<^sub>s\<^sub>t \)" using vars\<^sub>e\<^sub>s\<^sub>t_append extstrand_subst_hom(1)[of A B] by simp lemma vars\<^sub>e\<^sub>s\<^sub>t_append_rcv[simp]: "vars\<^sub>e\<^sub>s\<^sub>t (S@[Step (Receive t)]) = vars\<^sub>e\<^sub>s\<^sub>t S \ FV t" using vars\<^sub>e\<^sub>s\<^sub>t_append by auto lemma vars\<^sub>e\<^sub>s\<^sub>t_append_snd[simp]: "vars\<^sub>e\<^sub>s\<^sub>t (S@[Step (Send t)]) = vars\<^sub>e\<^sub>s\<^sub>t S \ FV t" using vars\<^sub>e\<^sub>s\<^sub>t_append by auto lemma vars\<^sub>e\<^sub>s\<^sub>t_append_decomp[simp]: "vars\<^sub>e\<^sub>s\<^sub>t (S@[Decomp t]) = vars\<^sub>e\<^sub>s\<^sub>t S \ FV t" using vars\<^sub>e\<^sub>s\<^sub>t_append decomp_vars by auto lemma bvars_decomp: "bvars\<^sub>e\<^sub>s\<^sub>t (A@[Decomp t]) = bvars\<^sub>e\<^sub>s\<^sub>t A" "bvars\<^sub>e\<^sub>s\<^sub>t (Decomp t#A) = bvars\<^sub>e\<^sub>s\<^sub>t A" using bvars\<^sub>e\<^sub>s\<^sub>t_append decomp_vars(3) by simp_all lemma bvars_decomp_rm: "bvars\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) = bvars\<^sub>e\<^sub>s\<^sub>t A" using bvars_decomp by (induct A rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) simp_all lemma FV_decomp_rm: "FV\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ FV\<^sub>e\<^sub>s\<^sub>t A" by (induct A rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma ik_eqs_rhs_decomp_FV: assumes "t \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))" shows "FV\<^sub>e\<^sub>s\<^sub>t (A@[Decomp t]) = FV\<^sub>e\<^sub>s\<^sub>t A" proof - have "FV\<^sub>e\<^sub>s\<^sub>t (A@[Decomp t]) = FV\<^sub>e\<^sub>s\<^sub>t A \ FV t" using FV\<^sub>e\<^sub>s\<^sub>t_append decomp_vars by simp moreover have "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \ FV\<^sub>e\<^sub>s\<^sub>t A" by force moreover have "FV t \ FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" using FV_subset_subterms[OF assms(1)] by simp ultimately show ?thesis by blast qed lemma vars\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_subset: "vars\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ vars\<^sub>e\<^sub>s\<^sub>t A" by (induct A rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma vars2\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_subset: "vars2\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ vars2\<^sub>e\<^sub>s\<^sub>t A" by (induct A rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma vars\<^sub>e\<^sub>s\<^sub>t_eq_vars\<^sub>s\<^sub>t: "vars\<^sub>e\<^sub>s\<^sub>t A = vars\<^sub>s\<^sub>t (to_st A)" by simp lemma vars2\<^sub>e\<^sub>s\<^sub>t_eq_vars2\<^sub>s\<^sub>t: "vars2\<^sub>e\<^sub>s\<^sub>t A = vars2\<^sub>s\<^sub>t (to_st A)" by simp lemma decomp_set_unfold: assumes "Ana t = (K, M)" shows "set (decomp t) = {snd\t\} \ (Send ` K) \ (Receive ` M)" using Ana_finite[OF assms] inv_set_fset assms unfolding decomp_def by auto lemma decomp_subst_unfold: assumes "Ana t = (K, M)" shows "decomp t \\<^sub>s\<^sub>t \ = snd\t \ \\#((map Send (inv set K)) \\<^sub>s\<^sub>t \)@((map Receive (inv set M)) \\<^sub>s\<^sub>t \)" using assms unfolding decomp_def by auto lemma ik\<^sub>e\<^sub>s\<^sub>t_finite: "finite (ik\<^sub>e\<^sub>s\<^sub>t A)" by (rule finite_ik\<^sub>s\<^sub>t) lemma eqs_rhs\<^sub>e\<^sub>s\<^sub>t_finite: "finite (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" by (rule finite_eqs_rhs\<^sub>s\<^sub>t) lemma to_est_append: "to_est (A@B) = to_est A@to_est B" by (induct A rule: to_est.induct) auto lemma to_est_vars\<^sub>e\<^sub>s\<^sub>t: "vars\<^sub>e\<^sub>s\<^sub>t (to_est A) = vars\<^sub>s\<^sub>t A" by (induct A rule: to_est.induct) auto lemma to_est_vars2\<^sub>e\<^sub>s\<^sub>t: "vars2\<^sub>e\<^sub>s\<^sub>t (to_est A) = vars2\<^sub>s\<^sub>t A" by (induct A rule: to_est.induct) auto lemma to_est_to_st_decomp_rm\<^sub>e\<^sub>s\<^sub>t_inv: "to_est (to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t A)) = decomp_rm\<^sub>e\<^sub>s\<^sub>t A" by (induct A rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma to_st_to_est_inv: "to_st (to_est A) = A" by (induct A rule: to_est.induct) auto lemma to_st_append: "to_st (A@B) = (to_st A)@(to_st B)" by (induct A rule: to_st.induct) auto lemma to_st_cons: "to_st (a#B) = (to_st [a])@(to_st B)" using to_st_append[of "[a]" B] by simp lemma vars2\<^sub>e\<^sub>s\<^sub>t_split: "vars2\<^sub>e\<^sub>s\<^sub>t (x#S) = vars2\<^sub>e\<^sub>s\<^sub>t [x] \ vars2\<^sub>e\<^sub>s\<^sub>t S" "vars2\<^sub>e\<^sub>s\<^sub>t (S@S') = vars2\<^sub>e\<^sub>s\<^sub>t S \ vars2\<^sub>e\<^sub>s\<^sub>t S'" using to_st_cons[of x S] to_st_append[of S S'] by auto lemma ik\<^sub>e\<^sub>s\<^sub>t_append: "ik\<^sub>e\<^sub>s\<^sub>t (A@B) = ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t B" by (metis ik_append to_st_append) lemma eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append: "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B) = eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t B" by (metis eqs_rhs_append to_st_append) lemma ik\<^sub>e\<^sub>s\<^sub>t_cons: "ik\<^sub>e\<^sub>s\<^sub>t (a#A) = ik\<^sub>e\<^sub>s\<^sub>t [a] \ ik\<^sub>e\<^sub>s\<^sub>t A" by (metis ik_append to_st_cons) lemma ik\<^sub>e\<^sub>s\<^sub>t_append_subst: "ik\<^sub>e\<^sub>s\<^sub>t (A@B \\<^sub>e\<^sub>s\<^sub>t \) = ik\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) \ ik\<^sub>e\<^sub>s\<^sub>t (B \\<^sub>e\<^sub>s\<^sub>t \)" "ik\<^sub>e\<^sub>s\<^sub>t (A@B) \set \ = (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t B \set \)" apply (metis ik\<^sub>e\<^sub>s\<^sub>t_append extstrand_subst_hom(1)) by (simp add: image_Un to_st_append) lemma eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append_subst: "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B \\<^sub>e\<^sub>s\<^sub>t \) = eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (B \\<^sub>e\<^sub>s\<^sub>t \)" "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B) \set \ = (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t B \set \)" apply (metis eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append extstrand_subst_hom(1)) using eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by blast lemma ik\<^sub>e\<^sub>s\<^sub>t_cons_subst: "ik\<^sub>e\<^sub>s\<^sub>t (a#A \\<^sub>e\<^sub>s\<^sub>t \) = ik\<^sub>e\<^sub>s\<^sub>t ([a \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \]) \ ik\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \)" "ik\<^sub>e\<^sub>s\<^sub>t (a#A) \set \ = (ik\<^sub>e\<^sub>s\<^sub>t [a] \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \)" apply (metis ik\<^sub>e\<^sub>s\<^sub>t_cons extstrand_subst_hom(2)) by (metis image_Un ik\<^sub>e\<^sub>s\<^sub>t_cons) lemma to_st_vars: "vars\<^sub>s\<^sub>t (to_st A) = vars\<^sub>e\<^sub>s\<^sub>t A" proof (induction A) case (Cons x A) hence "vars\<^sub>s\<^sub>t (to_st (x#A)) = vars\<^sub>s\<^sub>t (to_st [x]) \ vars\<^sub>e\<^sub>s\<^sub>t A" "vars\<^sub>e\<^sub>s\<^sub>t (x#A) = vars\<^sub>e\<^sub>s\<^sub>t [x] \ vars\<^sub>e\<^sub>s\<^sub>t A" using to_st_cons[of x A] by simp_all thus ?case using decomp_vars by (cases x) auto qed simp lemma to_st_vars2: "vars2\<^sub>s\<^sub>t (to_st A) = vars2\<^sub>e\<^sub>s\<^sub>t A" proof (induction A) case (Cons x A) hence "vars2\<^sub>s\<^sub>t (to_st (x#A)) = vars2\<^sub>s\<^sub>t (to_st [x]) \ vars2\<^sub>e\<^sub>s\<^sub>t A" "vars2\<^sub>e\<^sub>s\<^sub>t (x#A) = vars2\<^sub>e\<^sub>s\<^sub>t [x] \ vars2\<^sub>e\<^sub>s\<^sub>t A" by (metis strand_vars_split(2) to_st_cons, metis vars2\<^sub>e\<^sub>s\<^sub>t_split(1)) thus ?case using decomp_vars by (cases x) auto qed simp lemma ik\<^sub>e\<^sub>s\<^sub>t_vars_subset: "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) \ vars\<^sub>e\<^sub>s\<^sub>t A" using to_st_vars[of A] by fastforce lemma ik\<^sub>e\<^sub>s\<^sub>t_vars2_subset: "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) \ vars2\<^sub>e\<^sub>s\<^sub>t A" by (metis FV_ik_subset_FV_st to_st_vars2) lemma eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset: "FV\<^sub>s\<^sub>e\<^sub>t (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \ vars2\<^sub>e\<^sub>s\<^sub>t A" by (metis FV_eqs_rhs_subset_FV_st to_st_vars2) lemma ik\<^sub>e\<^sub>s\<^sub>t_eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset: "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \ vars2\<^sub>e\<^sub>s\<^sub>t A" using ik\<^sub>e\<^sub>s\<^sub>t_vars2_subset eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset by simp lemma ik\<^sub>e\<^sub>s\<^sub>t_vars_subst_img_subset: assumes "vars\<^sub>e\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \ \set \) \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" proof - { fix t assume "t \ ik\<^sub>s\<^sub>t (to_st \) \set \" then obtain t' where "t' \ ik\<^sub>s\<^sub>t (to_st \)" "t = t' \ \" by moura hence "FV t' \ FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \)" by auto hence "FV t \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" using assms \t = t' \ \\ ik\<^sub>e\<^sub>s\<^sub>t_vars_subset[of \] subst_FV_dom_img_subset[of t' \] by blast } thus ?thesis by auto qed lemma decomp_rm\<^sub>e\<^sub>s\<^sub>t_decomp_free: "Decomp t \ set (decomp_rm\<^sub>e\<^sub>s\<^sub>t S)" by (induct S rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma decomp_rm\<^sub>e\<^sub>s\<^sub>t_append: "decomp_rm\<^sub>e\<^sub>s\<^sub>t (S@S') = (decomp_rm\<^sub>e\<^sub>s\<^sub>t S)@(decomp_rm\<^sub>e\<^sub>s\<^sub>t S')" by (induct S rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma decomp_rm\<^sub>e\<^sub>s\<^sub>t_single[simp]: "decomp_rm\<^sub>e\<^sub>s\<^sub>t [Step (Send t)] = [Step (Send t)]" "decomp_rm\<^sub>e\<^sub>s\<^sub>t [Step (Receive t)] = [Step (Receive t)]" "decomp_rm\<^sub>e\<^sub>s\<^sub>t [Decomp t] = []" by auto lemma decomp_rm\<^sub>e\<^sub>s\<^sub>t_idem: "decomp_rm\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t S) = decomp_rm\<^sub>e\<^sub>s\<^sub>t S" by (induct S rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma decomp_rm\<^sub>e\<^sub>s\<^sub>t_ik_subset: "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t S) \ ik\<^sub>e\<^sub>s\<^sub>t S" proof (induction S rule: decomp_rm\<^sub>e\<^sub>s\<^sub>t.induct) case (3 x S) thus ?case by (cases x) auto qed auto lemma decomp_ground_subst: assumes "FV t = {}" shows "decomp (t \ \) = decomp t \\<^sub>s\<^sub>t \" proof - from assms have "t \ \ = t" by auto thus ?thesis using assms decomp_vars(1,2) strand_substI' by fastforce qed lemma decomp_no_eqs: "t \ t' \ set (decomp s)" "\X\t \ t'\ \ set (decomp s)" unfolding decomp_def by auto lemma extstrand_subst_vars_disj: "bvars\<^sub>e\<^sub>s\<^sub>t S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {} \ S \\<^sub>e\<^sub>s\<^sub>t \ = S \ vars\<^sub>e\<^sub>s\<^sub>t S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" proof (induction S) case (Cons x S) hence "bvars\<^sub>e\<^sub>s\<^sub>t S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" and *: "bvars\<^sub>e\<^sub>s\<^sub>t [x] \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using to_st_append[of "[x]" S] by auto hence **: "x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = x" and "vars\<^sub>e\<^sub>s\<^sub>t S \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using extstrand_subst_hom(2)[of x S \] Cons by auto moreover have "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" proof (cases x) case (Step y) thus ?thesis using trm_subst_disj[of _ \] \x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = x\ proof (cases y) case (Inequality X t t') hence "set X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using Step * by simp hence "rm_vars (set X) \ = \" using rm_vars_apply'[of \ "set X"] by (simp_all add: Int_commute) hence "t \ \ = t" "t' \ \ = t'" using Step Inequality ** by auto moreover have "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p x = set X \ FV t \ FV t'" using Inequality Step by simp ultimately show ?thesis using Step \set X \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}\ trm_subst_disj[of _ \] by auto qed auto next case Decomp thus ?thesis using \x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = x\ trm_subst_disj by auto qed ultimately show ?case using vars\<^sub>e\<^sub>s\<^sub>t_cons[of x S] by auto qed simp lemma ik\<^sub>e\<^sub>s\<^sub>t_subst_ground: assumes "\t. Decomp t \ set A \ FV t = {}" shows "ik\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = ik\<^sub>s\<^sub>t ((to_st A) \\<^sub>s\<^sub>t \)" using assms proof (induction A) case (Cons x S) have "ik\<^sub>s\<^sub>t (to_st (x#S \\<^sub>e\<^sub>s\<^sub>t \)) = ik\<^sub>s\<^sub>t (to_st (([x] \\<^sub>e\<^sub>s\<^sub>t \)@(S \\<^sub>e\<^sub>s\<^sub>t \)))" by (simp add: subst_apply_extstrand_def) hence "ik\<^sub>s\<^sub>t (to_st (x#S \\<^sub>e\<^sub>s\<^sub>t \)) = ik\<^sub>s\<^sub>t (to_st ([x] \\<^sub>e\<^sub>s\<^sub>t \)) \ ik\<^sub>s\<^sub>t (to_st S \\<^sub>s\<^sub>t \)" using ik\<^sub>e\<^sub>s\<^sub>t_append Cons.IH Cons.prems by simp moreover have "ik\<^sub>s\<^sub>t (to_st ([x] \\<^sub>e\<^sub>s\<^sub>t \)) = ik\<^sub>s\<^sub>t (to_st [x] \\<^sub>s\<^sub>t \)" proof (cases x) case (Decomp t) hence "FV t = {}" using Cons.prems by simp hence "to_st ([x] \\<^sub>e\<^sub>s\<^sub>t \) = decomp (t \ \)" "to_st [x] \\<^sub>s\<^sub>t \ = decomp t \\<^sub>s\<^sub>t \" by (simp_all add: \x = Decomp t\ subst_apply_extstrand_def) thus ?thesis using decomp_ground_subst[OF \FV t = {}\] by simp qed (auto simp add: subst_apply_extstrand_def) moreover have "ik\<^sub>s\<^sub>t (to_st (x#S) \\<^sub>s\<^sub>t \) = ik\<^sub>s\<^sub>t (to_st [x] \\<^sub>s\<^sub>t \) \ ik\<^sub>s\<^sub>t (to_st S \\<^sub>s\<^sub>t \)" by (metis append_Cons append_Nil ik\<^sub>e\<^sub>s\<^sub>t_append ik_subst subst_all_union) ultimately show ?case by simp qed (auto simp add: subst_apply_extstrand_def) lemma decomps\<^sub>e\<^sub>s\<^sub>t_ik_subset: "D \ decomps\<^sub>e\<^sub>s\<^sub>t M N \ \ ik\<^sub>e\<^sub>s\<^sub>t D \ \(subterms ` (M \ N))" proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f T K M') have "ik\<^sub>s\<^sub>t (decomp (Fun f T)) \ subterms (Fun f T)" "ik\<^sub>s\<^sub>t (decomp (Fun f T)) = ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f T)]" using decomp_ik[OF Decomp.hyps(3)] Ana_subterm[OF Decomp.hyps(3)] by auto hence "ik\<^sub>s\<^sub>t (to_st [Decomp (Fun f T)]) \ \(subterms ` (M \ N))" using in_subterms_subset_Union[OF Decomp.hyps(2)] by blast thus ?case using ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f T)]"] using Decomp.IH by auto qed simp lemma decomps\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_empty: "D \ decomps\<^sub>e\<^sub>s\<^sub>t M N \ \ decomp_rm\<^sub>e\<^sub>s\<^sub>t D = []" by (induct D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) (auto simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append) lemma decomps\<^sub>e\<^sub>s\<^sub>t_append: assumes "A \ decomps\<^sub>e\<^sub>s\<^sub>t S N \" "B \ decomps\<^sub>e\<^sub>s\<^sub>t S N \" shows "A@B \ decomps\<^sub>e\<^sub>s\<^sub>t S N \" using assms(2) proof (induction B rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case Nil show ?case using assms(1) by simp next case (Decomp B f X K T) hence "S \ ik\<^sub>e\<^sub>s\<^sub>t B \set \ \ S \ ik\<^sub>e\<^sub>s\<^sub>t (A@B) \set \" using ik\<^sub>e\<^sub>s\<^sub>t_append by auto thus ?case using decomps\<^sub>e\<^sub>s\<^sub>t.Decomp[OF Decomp.IH(1) Decomp.hyps(2,3,4)] ideduct_synth_mono[OF Decomp.hyps(5)] ideduct_synth_mono[OF Decomp.hyps(6)] by auto qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_subterms: assumes "A' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" shows "\(subterms ` ik\<^sub>e\<^sub>s\<^sub>t A') \ \(subterms ` (M \ N))" using assms proof (induction A' rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f X K T) hence "Fun f X \ \(subterms ` (M \ N))" by auto hence "\(subterms ` set X) \ \(subterms ` (M \ N))" using in_subterms_subset_Union[of "Fun f X" "M \ N"] params_subterms_Union[of X f] by blast moreover have "ik\<^sub>s\<^sub>t (to_st [Decomp (Fun f X)]) = T" using Decomp.hyps(3) decomp_ik by simp hence "\(subterms ` ik\<^sub>s\<^sub>t (to_st [Decomp (Fun f X)])) \ \(subterms ` set X)" using Ana_fun_subterm[OF Decomp.hyps(3)] by auto ultimately show ?case using ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f X)]"] Decomp.IH by auto qed simp lemma decomps\<^sub>e\<^sub>s\<^sub>t_eqs_rhs_empty: assumes "A' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" shows "eqs_rhs\<^sub>e\<^sub>s\<^sub>t A' = {}" using assms apply (induction A' rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) by (simp_all add: decomp_eqs_rhs_empty eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append) lemma decomps\<^sub>e\<^sub>s\<^sub>t_empty_strand[simp]: "decomps\<^sub>e\<^sub>s\<^sub>t {} {} \ = {[]}" proof show "{[]} \ decomps\<^sub>e\<^sub>s\<^sub>t {} {} \" using decomps\<^sub>e\<^sub>s\<^sub>t.Nil by auto show "decomps\<^sub>e\<^sub>s\<^sub>t {} {} \ \ {[]}" proof fix x assume "x \ decomps\<^sub>e\<^sub>s\<^sub>t {} {} \" thus "x \ {[]}" by (induct x rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) auto qed qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_finite_ik_append: assumes "finite M" "M \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" shows "\D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. ik\<^sub>e\<^sub>s\<^sub>t D = (\m \ M. ik\<^sub>e\<^sub>s\<^sub>t m)" using assms proof (induction M rule: finite_induct) case empty moreover have "[] \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" "ik\<^sub>s\<^sub>t (to_st []) = {}" using decomps\<^sub>e\<^sub>s\<^sub>t.Nil by auto ultimately show ?case by blast next case (insert m M) then obtain D where "D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" "ik\<^sub>e\<^sub>s\<^sub>t D = (\m\M. ik\<^sub>s\<^sub>t (to_st m))" by moura moreover have "m \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" using insert.prems(1) by blast ultimately show ?case using decomps\<^sub>e\<^sub>s\<^sub>t_append[of D A N \ m] ik\<^sub>e\<^sub>s\<^sub>t_append[of D m] by blast qed lemma decomp_snd_exists[simp]: "\D. decomp t = snd\t\#D" by (metis (mono_tags, lifting) decomp_def prod.case surj_pair) lemma decomp_nonnil[simp]: "decomp t \ []" using decomp_snd_exists[of t] by fastforce lemma to_st_nil_inv[dest]: "to_st A = [] \ A = []" by (induct A rule: to_st.induct) auto lemma well_analyzedD: assumes "well_analyzed A" "Decomp t \ set A" shows "\f T. t = Fun f T" using assms proof (induction A rule: well_analyzed.induct) case (Decomp A t') hence "\f T. t' = Fun f T" by (cases t') auto moreover have "Decomp t \ set A \ t = t'" using Decomp by auto ultimately show ?case using Decomp.IH by auto qed auto lemma well_analyzed_inv: assumes "well_analyzed (A@[Decomp t])" shows "t \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)) - (Var ` \)" using assms well_analyzed.cases[of "A@[Decomp t]"] by fastforce lemma well_analyzed_split_left_single: "well_analyzed (A@[a]) \ well_analyzed A" by (induction "A@[a]" rule: well_analyzed.induct) auto lemma well_analyzed_split_left: "well_analyzed (A@B) \ well_analyzed A" proof (induction B rule: List.rev_induct) case (snoc b B) thus ?case using well_analyzed_split_left_single[of "A@B" b] by simp qed simp lemma well_analyzed_append: assumes "well_analyzed A" "well_analyzed B" shows "well_analyzed (A@B)" using assms(2,1) proof (induction B rule: well_analyzed.induct) case (Step B x) show ?case using well_analyzed.Step[OF Step.IH[OF Step.prems]] by simp next case (Decomp B t) thus ?case using well_analyzed.Decomp[OF Decomp.IH[OF Decomp.prems]] ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by auto qed simp_all lemma well_analyzed_singleton: "well_analyzed [Step (Send t)]" "well_analyzed [Step (Receive t)]" "well_analyzed [Step (Equality t t')]" "well_analyzed [Step (Inequality X t t')]" "\well_analyzed [Decomp t]" proof - show "well_analyzed [Step (Send t)]" "well_analyzed [Step (Receive t)]" "well_analyzed [Step (Equality t t')]" "well_analyzed [Step (Inequality X t t')]" using well_analyzed.Step[OF well_analyzed.Nil] by simp_all show "\well_analyzed [Decomp t]" using well_analyzed.cases[of "[Decomp t]"] by auto qed lemma well_analyzed_decomp_rm\<^sub>e\<^sub>s\<^sub>t: "well_analyzed A \ well_analyzed (decomp_rm\<^sub>e\<^sub>s\<^sub>t A)" apply (induction A rule: well_analyzed.induct) using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append well_analyzed.Step by auto lemma well_analyzed_decomp_rm\<^sub>e\<^sub>s\<^sub>t_FV: "well_analyzed A \ FV\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) = FV\<^sub>e\<^sub>s\<^sub>t A" proof assume "well_analyzed A" thus "FV\<^sub>e\<^sub>s\<^sub>t A \ FV\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A)" proof (induction A rule: well_analyzed.induct) case Decomp thus ?case using ik_eqs_rhs_decomp_FV decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto next case (Step A x) have "FV\<^sub>e\<^sub>s\<^sub>t (A@[Step x]) = FV\<^sub>e\<^sub>s\<^sub>t A \ FV\<^sub>s\<^sub>t\<^sub>p x" "FV\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t (A@[Step x])) = FV\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ FV\<^sub>s\<^sub>t\<^sub>p x" using FV\<^sub>e\<^sub>s\<^sub>t_append decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto thus ?case using Step by auto qed simp qed (rule FV_decomp_rm) lemma sem\<^sub>e\<^sub>s\<^sub>t_c_split_left[dest]: assumes "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (\@\')" shows "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \" using assms sem\<^sub>e\<^sub>s\<^sub>t_c.cases by (induction \' rule: List.rev_induct) fastforce+ lemma sem\<^sub>e\<^sub>s\<^sub>t_d_split_left[dest]: assumes "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (\@\')" shows "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \" using assms sem\<^sub>e\<^sub>s\<^sub>t_d.cases by (induction \' rule: List.rev_induct) fastforce+ lemma sem\<^sub>e\<^sub>s\<^sub>t_c_append: assumes "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \" "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \'" shows "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (\@\')" using assms(2,1) proof (induction rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct) case Nil thus ?case by simp next case (Send M\<^sub>0 \ \' t) have "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \\<^sub>c t \ \" using ik\<^sub>e\<^sub>s\<^sub>t_append[of \ \'] ideduct_synth_mono[OF Send.hyps(2), of "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \"] by blast thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Send[OF Send.IH[OF Send.prems]] by simp next case (Receive M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Receive[OF Receive.IH[OF Receive.prems]] by simp next case (Equality M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Equality[OF Equality.IH[OF Equality.prems]] by simp next case (Inequality M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Inequality[OF Inequality.IH[OF Inequality.prems]] by simp next case (Decompose M\<^sub>0 \ \' t K M) hence "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \\<^sub>c t \ \" "\k. k \ K \ ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \\<^sub>c k \ \" using ik\<^sub>e\<^sub>s\<^sub>t_append[of \ \'] ideduct_synth_mono[of "ik\<^sub>e\<^sub>s\<^sub>t \' \ M\<^sub>0 \set \" _ "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \"] by auto thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Decompose[OF Decompose.IH[OF Decompose.prems] _ Decompose.hyps(3)] by simp qed lemma sem\<^sub>e\<^sub>s\<^sub>t_d_append: assumes "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \" "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \'" shows "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (\@\')" using assms(2,1) proof (induction rule: sem\<^sub>e\<^sub>s\<^sub>t_d.induct) case Nil thus ?case by simp next case (Send M\<^sub>0 \ \' t) have "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \ t \ \" using ik\<^sub>e\<^sub>s\<^sub>t_append[of \ \'] ideduct_mono[OF Send.hyps(2), of "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \"] by blast thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Send[OF Send.IH[OF Send.prems]] by simp next case (Receive M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Receive[OF Receive.IH[OF Receive.prems]] by simp next case (Equality M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Equality[OF Equality.IH[OF Equality.prems]] by simp next case (Inequality M\<^sub>0 \ \' t) thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Inequality[OF Inequality.IH[OF Inequality.prems]] by simp next case (Decompose M\<^sub>0 \ \' t K M) hence "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \ t \ \" "\k. k \ K \ ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \ \ k \ \" using ik\<^sub>e\<^sub>s\<^sub>t_append[of \ \'] ideduct_mono[of "ik\<^sub>e\<^sub>s\<^sub>t \' \ M\<^sub>0 \set \" _ "ik\<^sub>s\<^sub>t (to_st (\@\')) \ M\<^sub>0 \set \"] by auto thus ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Decompose[OF Decompose.IH[OF Decompose.prems] _ Decompose.hyps(3)] by simp qed lemma sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \ = \M\<^sub>0; to_st \\\<^sub>d \" proof show "\M\<^sub>0; to_st \\\<^sub>d \ \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \" proof (induction \ arbitrary: M\<^sub>0 rule: List.rev_induct) case Nil show ?case using to_st_nil_inv by simp next case (snoc a \) hence IH: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \" and *: "\ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0; to_st [a]\\<^sub>d \" using strand_sem_split_left_d[of M\<^sub>0 "to_st \" "to_st [a]"] to_st_append strand_sem_split_right_d[of M\<^sub>0 "to_st \" "to_st [a]"] by (auto simp add: sup.commute) thus ?case using snoc proof (cases a) case (Step b) thus ?thesis proof (cases b) case (Send t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_d.Send[OF IH] * Step by auto next case (Receive t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_d.Receive[OF IH] Step by auto next case (Equality t t') thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_d.Equality[OF IH] * Step by auto next case (Inequality t t') thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_d.Inequality[OF IH] * Step by auto qed next case (Decomp t) obtain K M where Ana: "Ana t = (K,M)" by moura have "to_st [a] = decomp t" using Decomp by auto hence "to_st [a] = snd\t\#map Send (inv set K)@map Receive (inv set M)" using Ana unfolding decomp_def by auto hence **: "ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0 \set \ \ t \ \" and "\ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0; map Send (inv set K)\\<^sub>d \" using * by auto hence "\k. k \ K \ ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0 \set \ \ k \ \" using * inv_set_fset[OF Ana_finite(1)[OF Ana]] strand_sem_snd_split_d by auto thus ?thesis using Decomp sem\<^sub>e\<^sub>s\<^sub>t_d.Decompose[OF IH ** Ana] by metis qed qed show "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ \ \ \M\<^sub>0; to_st \\\<^sub>d \" proof (induction rule: sem\<^sub>e\<^sub>s\<^sub>t_d.induct) case Nil thus ?case by simp next case (Send M\<^sub>0 \ \ t) thus ?case using strand_sem_append_d[of M\<^sub>0 "to_st \" \ "[snd\t\]"] to_st_append[of \ "[Step (Send t)]"] by (simp add: sup.commute) next case (Receive M\<^sub>0 \ \ t) thus ?case using strand_sem_append_d[of M\<^sub>0 "to_st \" \ "[rcv\t\]"] to_st_append[of \ "[Step (Receive t)]"] by (simp add: sup.commute) next case (Equality M\<^sub>0 \ \ t t') thus ?case using strand_sem_append_d[of M\<^sub>0 "to_st \" \ "[t \ t']"] to_st_append[of \ "[Step (Equality t t')]"] by (simp add: sup.commute) next case (Inequality M\<^sub>0 \ \ X t t') thus ?case using strand_sem_append_d[of M\<^sub>0 "to_st \" \ "[\X\t \ t'\]"] to_st_append[of \ "[Step (Inequality X t t')]"] by (auto simp add: sup.commute) next case (Decompose M\<^sub>0 \ \ t K M) have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); decomp t\\<^sub>d \" proof - have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); [snd\t\]\\<^sub>d \" using Decompose.hyps(2) by (auto simp add: sup.commute) moreover have "\k. k \ K \ M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \) \set \ \ k \ \" using Decompose by (metis sup.commute) hence "\k. k \ K \ \M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); [snd\k\]\\<^sub>d \" by auto hence "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); map Send (inv set K)\\<^sub>d \" using strand_sem_snd_map_d[of "inv set K", of "M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \)" \] inv_set_fset[OF Ana_finite(1)[OF Decompose.hyps(3)]] by auto moreover have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); map Receive (inv set M)\\<^sub>d \" by (metis strand_sem_rcv_map_d) ultimately have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); snd\t\#map Send (inv set K)@map Receive (inv set M)\\<^sub>d \" by auto thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto qed hence "\M\<^sub>0; to_st \@decomp t\\<^sub>d \" using strand_sem_append_d[of M\<^sub>0 "to_st \" \ "decomp t"] Decompose.IH by simp thus ?case using to_st_append[of \ "[Decomp t]"] by simp qed qed lemma sem\<^sub>e\<^sub>s\<^sub>t_c_eq_sem_st: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \ = \M\<^sub>0; to_st \\\<^sub>c \" proof show "\M\<^sub>0; to_st \\\<^sub>c \ \ sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \" proof (induction \ arbitrary: M\<^sub>0 rule: List.rev_induct) case Nil show ?case using to_st_nil_inv by simp next case (snoc a \) hence IH: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \" and *: "\ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0; to_st [a]\\<^sub>c \" using strand_sem_split_left[of M\<^sub>0 "to_st \" "to_st [a]"] to_st_append strand_sem_split_right[of M\<^sub>0 "to_st \" "to_st [a]"] by (auto simp add: sup.commute) thus ?case using snoc proof (cases a) case (Step b) thus ?thesis proof (cases b) case (Send t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_c.Send[OF IH] * Step by auto next case (Receive t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_c.Receive[OF IH] Step by auto next case (Equality t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_c.Equality[OF IH] * Step by auto next case (Inequality t) thus ?thesis using sem\<^sub>e\<^sub>s\<^sub>t_c.Inequality[OF IH] * Step by auto qed next case (Decomp t) obtain K M where Ana: "Ana t = (K,M)" by moura have "to_st [a] = decomp t" using Decomp by auto hence "to_st [a] = snd\t\#map Send (inv set K)@map Receive (inv set M)" using Ana unfolding decomp_def by auto hence **: "ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0 \set \ \\<^sub>c t \ \" and "\ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0; map Send (inv set K)\\<^sub>c \" using * by auto hence "\k. k \ K \ ik\<^sub>e\<^sub>s\<^sub>t \ \ M\<^sub>0 \set \ \\<^sub>c k \ \" using * inv_set_fset[OF Ana_finite(1)[OF Ana]] strand_sem_snd_split by auto thus ?thesis using Decomp sem\<^sub>e\<^sub>s\<^sub>t_c.Decompose[OF IH ** Ana] by metis qed qed show "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ \ \ \M\<^sub>0; to_st \\\<^sub>c \" proof (induction rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct) case Nil thus ?case by simp next case (Send M\<^sub>0 \ \ t) thus ?case using strand_sem_append[of M\<^sub>0 "to_st \" \ "[snd\t\]"] to_st_append[of \ "[Step (Send t)]"] by (simp add: sup.commute) next case (Receive M\<^sub>0 \ \ t) thus ?case using strand_sem_append[of M\<^sub>0 "to_st \" \ "[rcv\t\]"] to_st_append[of \ "[Step (Receive t)]"] by (simp add: sup.commute) next case (Equality M\<^sub>0 \ \ t t') thus ?case using strand_sem_append[of M\<^sub>0 "to_st \" \ "[t \ t']"] to_st_append[of \ "[Step (Equality t t')]"] by (simp add: sup.commute) next case (Inequality M\<^sub>0 \ \ X t t') thus ?case using strand_sem_append[of M\<^sub>0 "to_st \" \ "[\X\t \ t'\]"] to_st_append[of \ "[Step (Inequality X t t')]"] by (auto simp add: sup.commute) next case (Decompose M\<^sub>0 \ \ t K M) have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); decomp t\\<^sub>c \" proof - have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); [snd\t\]\\<^sub>c \" using Decompose.hyps(2) by (auto simp add: sup.commute) moreover have "\k. k \ K \ M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \) \set \ \\<^sub>c k \ \" using Decompose by (metis sup.commute) hence "\k. k \ K \ \M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); [snd\k\]\\<^sub>c \" by auto hence "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); map Send (inv set K)\\<^sub>c \" using strand_sem_snd_map[of "inv set K", of "M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \)" \] inv_set_fset[OF Ana_finite(1)[OF Decompose.hyps(3)]] by auto moreover have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); map Receive (inv set M)\\<^sub>c \" by (metis strand_sem_rcv_map) ultimately have "\M\<^sub>0 \ ik\<^sub>s\<^sub>t (to_st \); snd\t\#map Send (inv set K)@map Receive (inv set M)\\<^sub>c \" by auto thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto qed hence "\M\<^sub>0; to_st \@decomp t\\<^sub>c \" using strand_sem_append[of M\<^sub>0 "to_st \" \ "decomp t"] Decompose.IH by simp thus ?case using to_st_append[of \ "[Decomp t]"] by simp qed qed lemma sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct_aux: assumes "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ A" "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" shows "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ t" using assms proof (induction M\<^sub>0 \ A arbitrary: t rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct) case (Send M\<^sub>0 \ A t') thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append ik\<^sub>e\<^sub>s\<^sub>t_append by auto next case (Receive M\<^sub>0 \ A t') hence "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append ik\<^sub>e\<^sub>s\<^sub>t_append by auto hence IH: "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ t" using Receive.IH by auto show ?case using ideduct_mono[OF IH] decomp_rm\<^sub>e\<^sub>s\<^sub>t_append ik\<^sub>e\<^sub>s\<^sub>t_append by auto next case (Equality M\<^sub>0 \ A t') thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append ik\<^sub>e\<^sub>s\<^sub>t_append by auto next case (Inequality M\<^sub>0 \ A t') thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append ik\<^sub>e\<^sub>s\<^sub>t_append by auto next case (Decompose M\<^sub>0 \ A t' K M t) have *: "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ t' \ \" using Decompose.hyps(2) proof (induction rule: intruder_synth_induct) case (AxiomC t'') moreover { assume "t'' \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t'' \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" hence ?case using Decompose.IH by auto } ultimately show ?case by force qed simp { fix k assume "k \ K" hence "ik\<^sub>e\<^sub>s\<^sub>t A \ M\<^sub>0 \set \ \\<^sub>c k \ \" using Decompose.hyps by auto hence "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ k \ \" proof (induction rule: intruder_synth_induct) case (AxiomC t'') moreover { assume "t'' \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t'' \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" hence ?case using Decompose.IH by auto } ultimately show ?case by force qed simp } hence **: "\k. k \ K \set \ \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ k" by auto show ?case proof (cases "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \") case True thus ?thesis using Decompose.IH Decompose.prems(2) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto next case False hence "t \ ik\<^sub>s\<^sub>t (decomp t') \set \" using Decompose.prems(1) ik\<^sub>e\<^sub>s\<^sub>t_append by auto hence ***: "t \ M \set \" using Decompose.hyps(3) decomp_ik by auto hence "M \ {}" by auto hence ****: "Ana (t' \ \) = (K \set \, M \set \)" using Ana_subst[OF Decompose.hyps(3)] by auto have "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ t" by (rule intruder_deduct.Decompose[OF * **** ** ***]) thus ?thesis using ideduct_mono decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto qed qed simp lemma sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct: assumes "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ A" "ik\<^sub>e\<^sub>s\<^sub>t A \ M\<^sub>0 \set \ \\<^sub>c t" shows "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \ M\<^sub>0 \set \ \ t" using assms(2) proof (induction t rule: intruder_synth_induct) case (AxiomC t) hence "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \ \ t \ M\<^sub>0 \set \" by auto moreover { assume "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" hence ?case using ideduct_mono[OF intruder_deduct.Axiom] by auto } moreover { assume "t \ ik\<^sub>e\<^sub>s\<^sub>t A \set \" "t \ ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \set \" hence ?case using sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct_aux[OF assms(1)] by auto } ultimately show ?case by auto qed simp lemma sem\<^sub>e\<^sub>s\<^sub>t_d_decomp_rm\<^sub>e\<^sub>s\<^sub>t_if_sem\<^sub>e\<^sub>s\<^sub>t_c: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ A \ sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (decomp_rm\<^sub>e\<^sub>s\<^sub>t A)" proof (induction M\<^sub>0 \ A rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct) case (Send M\<^sub>0 \ A t) thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append sem\<^sub>e\<^sub>s\<^sub>t_d.Send[OF Send.IH] sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct by auto next case Receive thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append sem\<^sub>e\<^sub>s\<^sub>t_d.Receive by auto next case (Equality M\<^sub>0 \ A t) thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append sem\<^sub>e\<^sub>s\<^sub>t_d.Equality[OF Equality.IH] sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct by auto next case (Inequality M\<^sub>0 \ A t) thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append sem\<^sub>e\<^sub>s\<^sub>t_d.Inequality[OF Inequality.IH] sem\<^sub>e\<^sub>s\<^sub>t_c_decomp_rm\<^sub>e\<^sub>s\<^sub>t_deduct by auto next case Decompose thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto qed auto lemma sem\<^sub>e\<^sub>s\<^sub>t_c_decomps\<^sub>e\<^sub>s\<^sub>t_append: assumes "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ A" "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \) \" shows "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (A@D)" using assms(2,1) proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f T K M) hence *: "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (A @ D)" "ik\<^sub>e\<^sub>s\<^sub>t (A@D) \ {} \set \ \\<^sub>c Fun f T \ \" "\k. k \ K \ ik\<^sub>e\<^sub>s\<^sub>t (A @ D) \ {} \set \ \\<^sub>c k \ \" using ik\<^sub>e\<^sub>s\<^sub>t_append by auto show ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Decompose[OF *(1,2) Decomp.hyps(3) *(3)] by simp qed auto lemma strand_subst_set: "(set (S \\<^sub>s\<^sub>t \)) = ((\x. x \\<^sub>s\<^sub>t\<^sub>p \) ` (set S))" by auto lemma strand_map_inv_set_snd_rcv_subst: assumes "finite (M::('a,'b) terms)" shows "set ((map Send (inv set M)) \\<^sub>s\<^sub>t \) = Send ` (M \set \)" (is ?A) "set ((map Receive (inv set M)) \\<^sub>s\<^sub>t \) = Receive ` (M \set \)" (is ?B) proof - { fix f::"('a,'b) term \ ('a,'b) strand_step" assume f: "f = Send \ f = Receive" from assms have "set ((map f (inv set M)) \\<^sub>s\<^sub>t \) = f ` (M \set \)" proof (induction rule: finite_induct) case empty thus ?case unfolding inv_def by auto next case (insert m M) have "set (map f (inv set (insert m M)) \\<^sub>s\<^sub>t \) = insert (f m \\<^sub>s\<^sub>t\<^sub>p \) (set (map f (inv set M) \\<^sub>s\<^sub>t \))" by (simp add: insert.hyps(1) inv_set_fset) thus ?case using f insert.IH by auto qed } thus "?A" "?B" by auto qed lemma Ana_invar_subst_subset: assumes "Ana_invar_subst M" "N \ M" shows "Ana_invar_subst N" using assms unfolding Ana_invar_subst by blast lemma Ana_invar_subst_decomp_subst: assumes "Ana_invar_subst M" "Fun f T \ M" shows "set (decomp (Fun f T \ \)) = set (decomp (Fun f T) \\<^sub>s\<^sub>t \)" proof - obtain K M where Ana: "Ana (Fun f T) = (K, M)" by (metis surj_pair) hence Ana': "Ana (Fun f T \ \) = (K \set \, M \set \)" using assms in_subterms_Union unfolding Ana_invar_subst by blast have "set (decomp (Fun f T \ \)) = {snd\Fun f T \ \\} \ (Send`(K \set \)) \ (Receive`(M \set \))" by (metis decomp_set_unfold[OF Ana']) moreover have "decomp (Fun f T) \\<^sub>s\<^sub>t \ = snd\Fun f T \ \\#(map Send (inv set K) \\<^sub>s\<^sub>t \)@(map Receive (inv set M) \\<^sub>s\<^sub>t \)" using Ana unfolding decomp_def by auto hence "set (decomp (Fun f T) \\<^sub>s\<^sub>t \) = {snd\Fun f T \ \\} \ (Send`(K \set \)) \ (Receive`(M \set \))" using strand_map_inv_set_snd_rcv_subst(1)[OF Ana_finite(1)[OF Ana], of \] strand_map_inv_set_snd_rcv_subst(2)[OF Ana_finite(2)[OF Ana], of \] by auto ultimately show ?thesis by auto qed lemma Ana_invar_substD: assumes "Ana_invar_subst \" and "Fun f T \ \(subterms ` \)" "Ana (Fun f T) = (K, M)" shows "Ana (Fun f T \ \) = (K \set \, M \set \)" using assms Ana_invar_subst by blast lemma decomps\<^sub>e\<^sub>s\<^sub>t_preserves_wf: assumes "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" "wf\<^sub>e\<^sub>s\<^sub>t V A" shows "wf\<^sub>e\<^sub>s\<^sub>t V (A@D)" using assms proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f T K M) have "vars2\<^sub>s\<^sub>t (decomp (Fun f T)) \ FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" using decomp_vars FV_subset_subterms[OF Decomp.hyps(2)] by simp moreover have "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \ vars2\<^sub>e\<^sub>s\<^sub>t A" using ik\<^sub>e\<^sub>s\<^sub>t_vars2_subset eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset by simp ultimately have "vars2\<^sub>s\<^sub>t (decomp (Fun f T)) \ vars2\<^sub>e\<^sub>s\<^sub>t A" by blast hence "vars2\<^sub>s\<^sub>t (decomp (Fun f T)) \ vars2\<^sub>s\<^sub>t (to_st (A@D)) \ V" using to_st_append[of A D] strand_vars_split(2)[of "to_st A" "to_st D"] by (metis le_supI1 vars2\<^sub>e\<^sub>s\<^sub>t_eq_vars2\<^sub>s\<^sub>t) thus ?case using wf_append_suffix[OF Decomp.IH[OF Decomp.prems], of "decomp (Fun f T)"] to_st_append[of "A@D" "[Decomp (Fun f T)]"] by auto qed auto lemma decomps\<^sub>e\<^sub>s\<^sub>t_preserves_model_c: assumes "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ A" shows "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \ (A@D)" using assms proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f T K M) show ?case using sem\<^sub>e\<^sub>s\<^sub>t_c.Decompose[OF Decomp.IH[OF Decomp.prems] _ Decomp.hyps(3)] Decomp.hyps(5,6) ideduct_synth_mono ik\<^sub>e\<^sub>s\<^sub>t_append by (metis (mono_tags, lifting) List.append_assoc image_Un sup_ge1) qed auto lemma decomps\<^sub>e\<^sub>s\<^sub>t_preserves_model_d: assumes "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ A" shows "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \ (A@D)" using assms proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp D f T K M) show ?case using sem\<^sub>e\<^sub>s\<^sub>t_d.Decompose[OF Decomp.IH[OF Decomp.prems] _ Decomp.hyps(3)] Decomp.hyps(5,6) ideduct_synth_mono ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append deduct_if_synth by (metis (mono_tags, lifting) List.append_assoc image_Un sup_ge1) qed auto lemma decomps\<^sub>e\<^sub>s\<^sub>t_exist_aux: assumes "D \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "M \ ik\<^sub>e\<^sub>s\<^sub>t D \ t" "\(M \ (ik\<^sub>e\<^sub>s\<^sub>t D) \\<^sub>c t)" obtains D' where "D@D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "M \ ik\<^sub>e\<^sub>s\<^sub>t (D@D') \\<^sub>c t" "M \ ik\<^sub>e\<^sub>s\<^sub>t D \ M \ ik\<^sub>e\<^sub>s\<^sub>t (D@D')" proof - have "\D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \. M \ ik\<^sub>e\<^sub>s\<^sub>t D' \\<^sub>c t" using assms(2) proof (induction t rule: intruder_deduct_induct) case (Compose X f) from Compose.IH have "\D \ decomps\<^sub>e\<^sub>s\<^sub>t M N \. \x \ set X. M \ ik\<^sub>e\<^sub>s\<^sub>t D \\<^sub>c x" proof (induction X) case (Cons t X) then obtain D' D'' where D': "D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "M \ ik\<^sub>e\<^sub>s\<^sub>t D' \\<^sub>c t" and D'': "D'' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "\x \ set X. M \ ik\<^sub>e\<^sub>s\<^sub>t D'' \\<^sub>c x" by moura hence "M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c t" "\x \ set X. M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c x" by (auto intro: ideduct_synth_mono simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) thus ?case using decomps\<^sub>e\<^sub>s\<^sub>t_append[OF D'(1) D''(1)] by (metis set_ConsD) qed (auto intro: decomps\<^sub>e\<^sub>s\<^sub>t.Nil) thus ?case using intruder_synth.ComposeC[OF Compose.hyps(1,2)] by metis next case (Decompose t K T t\<^sub>i) hence "finite K" "finite T" by (simp_all add: Ana_finite[OF Decompose.hyps(2)]) from \finite K\ have "\D \ decomps\<^sub>e\<^sub>s\<^sub>t M N \. \k \ K. M \ ik\<^sub>e\<^sub>s\<^sub>t D \\<^sub>c k" using Decompose.IH proof (induction K rule: finite_induct) case (insert t X) then obtain D' D'' where D': "D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "M \ ik\<^sub>e\<^sub>s\<^sub>t D' \\<^sub>c t" and D'': "D'' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "\x \ X. M \ ik\<^sub>e\<^sub>s\<^sub>t D'' \\<^sub>c x" using assms(1) by moura hence "M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c t" "\x \ X. M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c x" by (auto intro: ideduct_synth_mono simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) thus ?case using decomps\<^sub>e\<^sub>s\<^sub>t_append[OF D'(1) D''(1)] by auto qed auto then obtain D' where D': "D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "\k. k \ K \ M \ ik\<^sub>e\<^sub>s\<^sub>t D' \\<^sub>c k" by metis obtain D'' where D'': "D'' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "M \ ik\<^sub>e\<^sub>s\<^sub>t D'' \\<^sub>c t" by (metis Decompose.IH(1)) obtain f X where fX: "t = Fun f X" "t\<^sub>i \ set X" using Decompose.hyps(2,4) by (cases t) (auto dest: Ana_fun_subterm) from decomps\<^sub>e\<^sub>s\<^sub>t_append[OF D'(1) D''(1)] D'(2) D''(2) have *: "D'@D'' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" "\k. k \ K \ M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c k" "M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \\<^sub>c t" by (auto intro: ideduct_synth_mono simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) hence **: "\k. k \ K \ M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \set \ \\<^sub>c k \ \" using ideduct_synth_subst by auto have "t\<^sub>i \ set (inv set T)" unfolding inv_def by (metis (mono_tags) \finite T\ Decompose.hyps(4) finite_list someI_ex) hence "t\<^sub>i \ ik\<^sub>s\<^sub>t (decomp t)" using Decompose.hyps(2) ik_rcv_map unfolding decomp_def by auto with *(3) fX(1) Decompose.hyps(2) show ?case proof (induction t rule: intruder_synth_induct) case (AxiomC t) hence t_in_subterms: "t \ \(subterms ` (M \ N))" using decomps\<^sub>e\<^sub>s\<^sub>t_ik_subset[OF *(1)] subset_subterms_Union by auto have "M \ ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \set \ \\<^sub>c t \ \" using ideduct_synth_subst[OF intruder_synth.AxiomC[OF AxiomC.hyps(1)]] by metis moreover have "T \ {}" using decomp_ik[OF \Ana t = (K,T)\] \t\<^sub>i \ ik\<^sub>s\<^sub>t (decomp t)\ by auto ultimately have "D'@D''@[Decomp (Fun f X)] \ decomps\<^sub>e\<^sub>s\<^sub>t M N \" using AxiomC decomps\<^sub>e\<^sub>s\<^sub>t.Decomp[OF *(1) _ _ _ _ **] subset_subterms_Union t_in_subterms by (simp add: subset_eq) moreover have "decomp t = to_st [Decomp (Fun f X)]" using AxiomC.prems(1,2) by auto ultimately show ?case by (metis AxiomC.prems(3) UnCI intruder_synth.AxiomC ik\<^sub>e\<^sub>s\<^sub>t_append to_st_append) qed (auto intro!: fX(2) *(1)) qed (fastforce intro: intruder_synth.AxiomC assms(1)) hence "\D' \ decomps\<^sub>e\<^sub>s\<^sub>t M N \. M \ ik\<^sub>e\<^sub>s\<^sub>t (D@D') \\<^sub>c t" by (auto intro: ideduct_synth_mono simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) thus thesis using that[OF decomps\<^sub>e\<^sub>s\<^sub>t_append[OF assms(1)]] assms ik\<^sub>e\<^sub>s\<^sub>t_append by moura qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_ik_max_exist: assumes "finite A" "finite N" shows "\D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. \D' \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. ik\<^sub>e\<^sub>s\<^sub>t D' \ ik\<^sub>e\<^sub>s\<^sub>t D" proof - let ?IK = "\M. \D \ M. ik\<^sub>e\<^sub>s\<^sub>t D" have "?IK (decomps\<^sub>e\<^sub>s\<^sub>t A N \) \ (\t \ A \ N. subterms t)" by (auto dest!: decomps\<^sub>e\<^sub>s\<^sub>t_ik_subset) hence "finite (?IK (decomps\<^sub>e\<^sub>s\<^sub>t A N \))" using subterms_union_finite[OF assms(1)] subterms_union_finite[OF assms(2)] infinite_super by auto then obtain M where M: "finite M" "M \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" "?IK M = ?IK (decomps\<^sub>e\<^sub>s\<^sub>t A N \)" using finite_subset_Union by moura show ?thesis using decomps\<^sub>e\<^sub>s\<^sub>t_finite_ik_append[OF M(1,2)] M(3) by auto qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_exist: assumes "finite A" "finite N" shows "\D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. \t. A \ t \ A \ ik\<^sub>e\<^sub>s\<^sub>t D \\<^sub>c t" proof (rule ccontr) assume neg: "\(\D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. \t. A \ t \ A \ ik\<^sub>e\<^sub>s\<^sub>t D \\<^sub>c t)" obtain D where D: "D \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" "\D' \ decomps\<^sub>e\<^sub>s\<^sub>t A N \. ik\<^sub>e\<^sub>s\<^sub>t D' \ ik\<^sub>e\<^sub>s\<^sub>t D" using decomps\<^sub>e\<^sub>s\<^sub>t_ik_max_exist[OF assms] by moura then obtain t where t: "A \ ik\<^sub>e\<^sub>s\<^sub>t D \ t" "\(A \ ik\<^sub>e\<^sub>s\<^sub>t D \\<^sub>c t)" using neg by (fastforce intro: ideduct_mono) obtain D' where D': "D@D' \ decomps\<^sub>e\<^sub>s\<^sub>t A N \" "A \ ik\<^sub>e\<^sub>s\<^sub>t (D@D') \\<^sub>c t" "A \ ik\<^sub>e\<^sub>s\<^sub>t D \ A \ ik\<^sub>e\<^sub>s\<^sub>t (D@D')" by (metis decomps\<^sub>e\<^sub>s\<^sub>t_exist_aux t D(1)) hence "ik\<^sub>e\<^sub>s\<^sub>t D \ ik\<^sub>e\<^sub>s\<^sub>t (D@D')" using ik\<^sub>e\<^sub>s\<^sub>t_append by auto moreover have "ik\<^sub>e\<^sub>s\<^sub>t (D@D') \ ik\<^sub>e\<^sub>s\<^sub>t D" using D(2) D'(1) by auto ultimately show False by simp qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_exist_subst: assumes "ik\<^sub>e\<^sub>s\<^sub>t A \set \ \ t \ \" and "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ A" "wf\<^sub>e\<^sub>s\<^sub>t {} A" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" and "Ana_invar_subst (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" and "well_analyzed A" shows "\D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \. ik\<^sub>e\<^sub>s\<^sub>t (A@D) \set \ \\<^sub>c t \ \" proof - have ik_eq: "ik\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = ik\<^sub>e\<^sub>s\<^sub>t A \set \" using assms(5,6) proof (induction A rule: List.rev_induct) case (snoc a A) hence "Ana_invar_subst (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" using Ana_invar_subst_subset[OF snoc.prems(1)] ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by simp with snoc have IH: "ik\<^sub>e\<^sub>s\<^sub>t (A@[a] \\<^sub>e\<^sub>s\<^sub>t \) = (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t ([a] \\<^sub>e\<^sub>s\<^sub>t \)" "ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \set \ = (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t [a] \set \)" using well_analyzed_split_left[OF snoc.prems(2)] by (auto simp add: to_st_append ik\<^sub>e\<^sub>s\<^sub>t_append_subst) have "ik\<^sub>e\<^sub>s\<^sub>t [a \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \] = ik\<^sub>e\<^sub>s\<^sub>t [a] \set \" proof (cases a) case (Step b) thus ?thesis by (cases b) auto next case (Decomp t) then obtain f T where t: "t = Fun f T" using well_analyzedD[OF snoc.prems(2)] by force obtain K M where Ana_t: "Ana (Fun f T) = (K,M)" by (metis surj_pair) moreover have "Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@[a])))" using t Decomp snoc.prems(2) by (auto dest: well_analyzed_inv simp add: ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append) hence "Ana (Fun f T \ \) = (K \set \, M \set \)" using Ana_t snoc.prems(1) by force ultimately show ?thesis using Decomp t by (auto simp add: decomp_ik) qed thus ?case using IH unfolding subst_apply_extstrand_def by simp qed simp moreover have eqs_rhs_eq: "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \" using assms(5,6) proof (induction A rule: List.rev_induct) case (snoc a A) hence "Ana_invar_subst (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)" using Ana_invar_subst_subset[OF snoc.prems(1)] ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by simp hence "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \" using snoc.IH well_analyzed_split_left[OF snoc.prems(2)] by simp hence IH: "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@[a] \\<^sub>e\<^sub>s\<^sub>t \) = (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t ([a] \\<^sub>e\<^sub>s\<^sub>t \)" "eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@[a]) \set \ = (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t [a] \set \)" by (metis eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append_subst)+ have "eqs_rhs\<^sub>e\<^sub>s\<^sub>t [a \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \] = eqs_rhs\<^sub>e\<^sub>s\<^sub>t [a] \set \" proof (cases a) case (Step b) thus ?thesis by (cases b) auto next case (Decomp t) then obtain f T where t: "t = Fun f T" using well_analyzedD[OF snoc.prems(2)] by force obtain K M where Ana_t: "Ana (Fun f T) = (K,M)" by (metis surj_pair) moreover have "Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@[a])))" using t Decomp snoc.prems(2) by (auto dest: well_analyzed_inv simp add: ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append) hence "Ana (Fun f T \ \) = (K \set \, M \set \)" using Ana_t snoc.prems(1) by force ultimately show ?thesis using Decomp t by (auto simp add: decomp_eqs_rhs_empty) qed thus ?case using IH unfolding subst_apply_extstrand_def by simp qed simp ultimately obtain D where D: "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \set \) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \set \) Var" "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D) \\<^sub>c t \ \" using decomps\<^sub>e\<^sub>s\<^sub>t_exist[OF ik\<^sub>e\<^sub>s\<^sub>t_finite eqs_rhs\<^sub>e\<^sub>s\<^sub>t_finite, of "A \\<^sub>e\<^sub>s\<^sub>t \" "A \\<^sub>e\<^sub>s\<^sub>t \"] ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append assms(1) by force let ?P = "\D D'. \t. (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D) \\<^sub>c t \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c t" have "\D' \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \. ?P D D'" using D(1) proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case Nil have "ik\<^sub>e\<^sub>s\<^sub>t [] = ik\<^sub>e\<^sub>s\<^sub>t [] \set \" by auto thus ?case by (metis decomps\<^sub>e\<^sub>s\<^sub>t.Nil) next case (Decomp D f T K M) obtain D' where D': "D' \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" "?P D D'" using Decomp.IH by auto hence IH: "\k. k \ K \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c k" "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c Fun f T" using Decomp.hyps(5,6) by auto have D'_ik: "ik\<^sub>e\<^sub>s\<^sub>t D' \set \ \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)) \set \" "ik\<^sub>e\<^sub>s\<^sub>t D' \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))" using decomps\<^sub>e\<^sub>s\<^sub>t_ik_subset[OF D'(1)] by (metis subst_all_mono, metis) show ?case using IH(2,1) Decomp.hyps(2,3,4) proof (induction "Fun f T" arbitrary: f T K M rule: intruder_synth_induct) case (AxiomC f T) then obtain s where s: "s \ ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t D'" "Fun f T = s \ \" using AxiomC.prems by blast hence fT_s_in: "Fun f T \ (\(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))) \set \" "s \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))" using AxiomC D'_ik subset_subterms_Union[of "ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A"] subst_all_mono[OF subset_subterms_Union, of \] by (metis Un_iff image_eqI subset_Un_eq)+ obtain Ks Ms where Ana_s: "Ana s = (Ks,Ms)" by moura have AD'_props: "wf\<^sub>e\<^sub>s\<^sub>t {} (A@D')" "\{}; to_st (A@D')\\<^sub>c \" using decomps\<^sub>e\<^sub>s\<^sub>t_preserves_model_c[OF D'(1) assms(2)] decomps\<^sub>e\<^sub>s\<^sub>t_preserves_wf[OF D'(1) assms(3)] sem\<^sub>e\<^sub>s\<^sub>t_c_eq_sem_st by auto show ?case proof (cases s) case (Var x) (* In this case \ x (is a subterm of something that) was derived from an "earlier intruder knowledge" because A is well-formed and has \ as a model. So either the intruder composed Fun f T himself (making Decomp (Fun f T) unnecessary) or Fun f T is an instance of something else in the intruder knowledge (in which case the "something" can be used in place of Fun f T) *) hence "Var x \ ik\<^sub>e\<^sub>s\<^sub>t (A@D')" "\ x = Fun f T" using s ik\<^sub>e\<^sub>s\<^sub>t_append by auto show ?thesis proof (cases "\m \ M. ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t D' \set \ \\<^sub>c m") case True (* All terms acquired by decomposing Fun f T are already derivable. Hence there is no need to consider decomposition of Fun f T at all. *) have *: "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) = (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t D \ M" using decomp_ik[OF \Ana (Fun f T) = (K,M)\] ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f T)]"] by auto { fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t D \ M \\<^sub>c t'" hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c t'" proof (induction t' rule: intruder_synth_induct) case (AxiomC t') thus ?case proof assume "t' \ M" moreover have "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) = ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t D' \set \" by auto ultimately show ?case using True by auto qed (metis D'(2) intruder_synth.AxiomC) qed auto } thus ?thesis using D'(1) * by metis next case False (* Some term acquired by decomposition of Fun f T cannot be derived in \\<^sub>c. Fun f T must therefore be an instance of something else in the IK, because of well-formedness. *) then obtain t\<^sub>i where t\<^sub>i: "t\<^sub>i \ set T" "\ik\<^sub>e\<^sub>s\<^sub>t (A@D') \set \ \\<^sub>c t\<^sub>i" using Ana_fun_subterm[OF \Ana (Fun f T) = (K,M)\] by (auto simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) obtain S where fS: "Fun f S \ \(subterms ` ik\<^sub>e\<^sub>s\<^sub>t (A@D')) \ Fun f S \ \(subterms ` eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@D'))" "\ x = Fun f S \ \" using strand_sem_wf_ik_or_eqs_rhs_fun_subterm[ OF AD'_props \Var x \ ik\<^sub>e\<^sub>s\<^sub>t (A@D')\ _ t\<^sub>i \interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\] \\ x = Fun f T\ by moura hence fS_in: "Fun f S \ \ \ ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t D' \set \" "Fun f S \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A))" using subst_all_member[OF s(1), of \] Var ik\<^sub>e\<^sub>s\<^sub>t_append[of A D'] eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append[of A D'] decomps\<^sub>e\<^sub>s\<^sub>t_subterms[OF D'(1)] decomps\<^sub>e\<^sub>s\<^sub>t_eqs_rhs_empty[OF D'(1)] by auto obtain KS MS where Ana_fS: "Ana (Fun f S) = (KS, MS)" by moura hence "K = KS \set \" "M = MS \set \" using Ana_invar_substD[OF assms(5) fS_in(2)] s(2) fS(2) \s = Var x\ \Ana (Fun f T) = (K,M)\ by simp_all hence "MS \ {}" using \M \ {}\ by simp have "\k. k \ KS \ ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t D' \set \ \\<^sub>c k \ \" using AxiomC.prems(1) \K = KS \set \\ by (simp add: subst_all_union[of \]) hence D'': "D'@[Decomp (Fun f S)] \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" using decomps\<^sub>e\<^sub>s\<^sub>t.Decomp[OF D'(1) fS_in(2) Ana_fS \MS \ {}\] AxiomC.prems(1) intruder_synth.AxiomC[OF fS_in(1)] by simp moreover { fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) \\<^sub>c t'" hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun f S)]) \set \) \\<^sub>c t'" proof (induction t' rule: intruder_synth_induct) case (AxiomC t') hence "t' \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t D \ t' \ ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f T)]" by (simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) thus ?case proof assume "t' \ ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f T)]" hence "t' \ ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)] \set \" using decomp_ik \Ana (Fun f T) = (K,M)\ \Ana (Fun f S) = (KS,MS)\ \M = MS \set \\ by simp thus ?case using ideduct_synth_mono[ OF intruder_synth.AxiomC[of t' "ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)] \set \"], of "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun f S)]) \set \)"] by (auto simp add: ik\<^sub>e\<^sub>s\<^sub>t_append) next assume "t' \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t D" hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c t'" by (metis D'(2) intruder_synth.AxiomC) hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)] \set \) \\<^sub>c t'" by (simp add: ideduct_synth_mono) thus ?case using ik\<^sub>e\<^sub>s\<^sub>t_append[of D' "[Decomp (Fun f S)]"] subst_all_union[of \ "ik\<^sub>e\<^sub>s\<^sub>t D'" "ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)]"] by (simp add: sup_aci(2)) qed qed auto } ultimately show ?thesis using D'' by auto qed next case (Fun g S) (* Hence Decomp (Fun f T) can be substituted for Decomp (Fun g S) *) hence KM: "K = Ks \set \" "M = Ms \set \" using fT_s_in(2) \Ana (Fun f T) = (K,M)\ Ana_s s(2) Ana_invar_substD[OF assms(5), of g S] by auto hence Ms_nonempty: "Ms \ {}" using \M \ {}\ by auto { fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) \\<^sub>c t'" hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun g S)]) \set \) \\<^sub>c t'" using AxiomC proof (induction t' rule: intruder_synth_induct) case (AxiomC t') hence "t' \ ik\<^sub>e\<^sub>s\<^sub>t A \set \ \ t' \ ik\<^sub>e\<^sub>s\<^sub>t D \ t' \ M" by (simp add: decomp_ik ik\<^sub>e\<^sub>s\<^sub>t_append) thus ?case proof (elim disjE) assume "t' \ ik\<^sub>e\<^sub>s\<^sub>t D" hence *: "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c t'" using D'(2) by simp show ?case by (auto intro: ideduct_synth_mono[OF *] simp add: ik\<^sub>e\<^sub>s\<^sub>t_append_subst(2)) next assume "t' \ M" hence "t' \ ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun g S)] \set \" using KM(2) Fun decomp_ik[OF Ana_s] by auto thus ?case by (simp add: image_Un ik\<^sub>e\<^sub>s\<^sub>t_append) qed (simp add: ideduct_synth_mono[OF intruder_synth.AxiomC]) qed auto } thus ?thesis using s Fun Ana_s AxiomC.prems(1) KM(1) fT_s_in decomps\<^sub>e\<^sub>s\<^sub>t.Decomp[OF D'(1) _ _ Ms_nonempty, of g S Ks] by (metis AxiomC.hyps image_Un image_eqI intruder_synth.AxiomC) qed next case (ComposeC T f) have *: "\m. m \ M \ (ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c m" using Ana_fun_subterm[OF \Ana (Fun f T) = (K, M)\] ComposeC.hyps(3) by auto have **: "ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) = ik\<^sub>e\<^sub>s\<^sub>t D \ M" using decomp_ik[OF \Ana (Fun f T) = (K, M)\] ik\<^sub>e\<^sub>s\<^sub>t_append by auto { fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) \\<^sub>c t'" hence "(ik\<^sub>e\<^sub>s\<^sub>t A \set \) \ (ik\<^sub>e\<^sub>s\<^sub>t D' \set \) \\<^sub>c t'" by (induct rule: intruder_synth_induct) (auto simp add: D'(2) * **) } thus ?case using D'(1) by auto qed qed thus ?thesis using D(2) assms(1) by (auto simp add: ik\<^sub>e\<^sub>s\<^sub>t_append_subst(2)) qed lemma extstrand_substI[intro]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>e\<^sub>s\<^sub>t S = {} \ S \\<^sub>e\<^sub>s\<^sub>t \ = S" proof (induction S) case (Cons x S) hence "S \\<^sub>e\<^sub>s\<^sub>t \ = S" by (cases x) auto moreover have *: "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p x \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using Cons.prems vars\<^sub>e\<^sub>s\<^sub>t_cons by auto hence "x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \ = x" proof (cases x) case (Step b) thus ?thesis proof (cases b) case (Send t) hence "t \ \ = t" using * trm_subst_ident[of t \] Step by auto hence "snd\t\ \\<^sub>s\<^sub>t\<^sub>p \ = snd\t\" by (simp add: strand_step.case_eq_if) thus ?thesis using Step Send by simp next case (Receive t) hence "t \ \ = t" using * trm_subst_ident[of t \] Step by auto hence "rcv\t\ \\<^sub>s\<^sub>t\<^sub>p \ = rcv\t\" by (simp add: strand_step.case_eq_if) thus ?thesis using Step Receive by simp next case (Equality t t') hence "t \ \ = t" "t' \ \ = t'" using * trm_subst_ident[of _ \] Step by auto hence "t \ t' \\<^sub>s\<^sub>t\<^sub>p \ = t \ t'" by (simp add: strand_step.case_eq_if) thus ?thesis using Step Equality by simp next case (Inequality X t t') hence "t \ rm_vars (set X) \ = t" "t' \ rm_vars (set X) \ = t'" using * trm_subst_ident[of _ "rm_vars (set X) \"] rm_vars_dom[of "set X" \] Step by auto hence "\X\t \ t'\ \\<^sub>s\<^sub>t\<^sub>p \ = \X\t \ t'\" by (simp add: strand_step.case_eq_if) thus ?thesis using Step Inequality by simp qed next case (Decomp t) hence "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p x = FV t" by simp hence "t \ \ = t" using * trm_subst_ident[of t \] by metis thus ?thesis using \x = Decomp t\ by simp qed ultimately show ?case by (simp add: subst_apply_extstrand_def) qed simp lemma extstrandstep_subst_Idem: assumes "Idem \" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t [x] = {}" shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = {}" proof (cases x) case (Step y) thus ?thesis using subst_dom_elim[OF IdemE[OF assms(1)]] proof (cases y) case (Inequality X t t') hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ set X = {}" using Step assms(2) by simp hence **: "rm_vars (set X) \ = \" using rm_vars_apply'[of \ "set X"] by (simp_all add: Int_commute) hence ***: "\t. FV (t \ \) \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" by (metis subst_dom_elim[OF IdemE[OF Idem_rm_vars[OF assms(1)]], of _ "set X"]) have "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = set X \ FV (t \ \) \ FV (t' \ \)" using ** Step Inequality by simp thus ?thesis using Step Inequality * ***[of t] ***[of t'] by auto qed auto next case (Decomp t) hence "vars\<^sub>e\<^sub>s\<^sub>t\<^sub>p (x \\<^sub>e\<^sub>s\<^sub>t\<^sub>p \) = FV (t \ \)" by fastforce thus ?thesis using \x = Decomp t\ IdemE[OF assms(1)] using subst_dom_elim by fastforce qed lemma extstrand_subst_Idem: assumes "Idem \" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t A = {}" shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = {}" using assms(2) proof (induction A) case (Cons x A) have **: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t [x] = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t A = {}" using Cons bvars\<^sub>e\<^sub>s\<^sub>t_cons[of x A] by auto show ?case using extstrandstep_subst_Idem[OF assms(1) **(1)] Cons.IH[OF **(2)] vars\<^sub>e\<^sub>s\<^sub>t_cons_subst[of x A \] by auto qed simp lemma decomps\<^sub>e\<^sub>s\<^sub>t_vars: "B \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \ \ vars\<^sub>e\<^sub>s\<^sub>t B \ vars\<^sub>e\<^sub>s\<^sub>t A" proof (induction B rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp B f T K M) hence "FV (Fun f T) \ FV\<^sub>s\<^sub>e\<^sub>t (\(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t (A@B) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B))))" using FV_subset[of "Fun f T" "\(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ ik\<^sub>e\<^sub>s\<^sub>t B \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t B))"] ik\<^sub>e\<^sub>s\<^sub>t_append[of A B] eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append[of A B] by auto hence "FV (Fun f T) \ vars2\<^sub>s\<^sub>t (to_st (A@B))" by (metis FV_set_subterms_eq ik\<^sub>e\<^sub>s\<^sub>t_eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset subset_trans) hence "FV (Fun f T) \ vars\<^sub>e\<^sub>s\<^sub>t (A@B)" using to_st_vars[of "A@B"] vars2\<^sub>s\<^sub>t_subset_vars\<^sub>s\<^sub>t[of "to_st (A@B)"] by blast hence "vars\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f T)] \ vars\<^sub>e\<^sub>s\<^sub>t (A@B)" using decomp_vars by simp thus ?case using Decomp.IH vars\<^sub>e\<^sub>s\<^sub>t_append by auto qed simp lemma decomps\<^sub>e\<^sub>s\<^sub>t_funs_only: "\B \ decomps\<^sub>e\<^sub>s\<^sub>t A N \; Decomp t \ set B\ \ \f T. t = Fun f T" by (induct B rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) auto lemma decomps\<^sub>e\<^sub>s\<^sub>t_idem_subst: assumes "B \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \)) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \)) \" and "Idem \" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t A = {}" shows "B \\<^sub>e\<^sub>s\<^sub>t \ = B" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \) = {}" by (rule extstrand_subst_Idem[OF assms(2,3)]) moreover have "vars\<^sub>e\<^sub>s\<^sub>t B \ vars\<^sub>e\<^sub>s\<^sub>t (A \\<^sub>e\<^sub>s\<^sub>t \)" using decomps\<^sub>e\<^sub>s\<^sub>t_vars[OF assms(1)] by metis ultimately have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>e\<^sub>s\<^sub>t B = {}" by blast thus ?thesis using extstrand_substI by metis qed lemma dual\<^sub>s\<^sub>t_append: "dual\<^sub>s\<^sub>t (A@B) = (dual\<^sub>s\<^sub>t A)@(dual\<^sub>s\<^sub>t B)" by (induct A rule: dual\<^sub>s\<^sub>t.induct) auto lemma dual\<^sub>s\<^sub>t_self_inverse: "dual\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S) = S" proof (induction S) case (Cons x S) thus ?case by (cases x) auto qed simp lemma dual\<^sub>s\<^sub>t_trms_eq: "trms\<^sub>s\<^sub>t S = trms\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S)" proof (induction S) case (Cons x S) thus ?case by (cases x) auto qed simp lemma dual\<^sub>s\<^sub>t_eqs_tfr: "eqs_tfr\<^sub>s\<^sub>t S \ eqs_tfr\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S)" proof (induction S) case (Cons x S) have "eqs_tfr\<^sub>s\<^sub>t S" using Cons.prems by simp hence IH: "eqs_tfr\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S)" using Cons.IH by metis from Cons show ?case proof (cases x) case Equality thus ?thesis using Cons by fastforce next case (Inequality X t t') have "set (dual\<^sub>s\<^sub>t (x#S)) = insert x (set (dual\<^sub>s\<^sub>t S))" using Inequality by auto moreover have "\x\set X \ FV t \ FV t'. \a. \ (Var x) = Var a" using Cons.prems Inequality by auto ultimately show ?thesis using Inequality IH by auto qed auto qed simp lemma update\<^sub>s\<^sub>t_nil[simp]: "[] \ update\<^sub>s\<^sub>t \ []" by simp lemma update\<^sub>s\<^sub>t_snd[simp]: "snd\t\#S \ update\<^sub>s\<^sub>t \ (snd\t\#S)" "S \ update\<^sub>s\<^sub>t \ (snd\t\#S)" by simp_all lemma update\<^sub>s\<^sub>t_rcv[simp]: "rcv\t\#S \ update\<^sub>s\<^sub>t \ (rcv\t\#S)" "S \ update\<^sub>s\<^sub>t \ (rcv\t\#S)" by simp_all lemma wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_nil: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \ []) \" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto lemma wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_snd: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "snd\t\#S \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \ (snd\t\#S)) (\@[Step (Receive t)])" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def proof (intro conjI) let ?S = "snd\t\#S" let ?A = "\@[Step (Receive t)]" have \: "\S'. S' \ update\<^sub>s\<^sub>t \ ?S \ S' = S \ S' \ \" by auto have 1: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto moreover have 2: "vars2\<^sub>e\<^sub>s\<^sub>t ?A = vars2\<^sub>e\<^sub>s\<^sub>t \ \ FV t" using vars2\<^sub>e\<^sub>s\<^sub>t_split(2) by (simp add: Un_assoc) ultimately have 3: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono) have 4: "\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by simp have "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis 3 \) have "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t S = {}" using 4 assms(2) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce+ thus "\S \ update\<^sub>s\<^sub>t \ ?S. \S' \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" by (metis 4 \) have "\S' \ \. FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t ?S = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by metis+ hence 5: "FV\<^sub>e\<^sub>s\<^sub>t ?A = FV\<^sub>e\<^sub>s\<^sub>t \ \ FV t" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = bvars\<^sub>e\<^sub>s\<^sub>t \" "\S' \ \. FV t \ bvars\<^sub>s\<^sub>t S' = {}" using to_st_append by force+ have *: "\S \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using assms(2) by metis hence "FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by (metis * \) have **: "\S \ \. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t ?S = {}" using assms(2) by metis hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by (metis ** \) qed lemma wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_rcv: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "rcv\t\#S \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \ (rcv\t\#S)) (\@[Step (Send t)])" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def proof (intro conjI) let ?S = "rcv\t\#S" let ?A = "\@[Step (Send t)]" have \: "\S'. S' \ update\<^sub>s\<^sub>t \ ?S \ S' = S \ S' \ \" by auto have 1: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto moreover have 2: "vars2\<^sub>e\<^sub>s\<^sub>t ?A = vars2\<^sub>e\<^sub>s\<^sub>t \ \ FV t" using vars2\<^sub>e\<^sub>s\<^sub>t_split(2) by (simp add: Un_assoc) ultimately have 3: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono) have 4: "\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by simp have "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis 3 \) have "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t S = {}" using 4 assms(2) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce+ thus "\S \ update\<^sub>s\<^sub>t \ ?S. \S' \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" by (metis 4 \) have "\S' \ \. FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t ?S = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by metis+ hence 5: "FV\<^sub>e\<^sub>s\<^sub>t ?A = FV\<^sub>e\<^sub>s\<^sub>t \ \ FV t" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = bvars\<^sub>e\<^sub>s\<^sub>t \" "\S' \ \. FV t \ bvars\<^sub>s\<^sub>t S' = {}" using to_st_append by force+ have *: "\S \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using assms(2) by metis hence "FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by (metis * \) have **: "\S \ \. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t ?S = {}" using assms(2) by metis hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by (metis ** \) qed lemma wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_eq: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "t \ t'#S \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \ (t \ t'#S)) (\@[Step (Equality t t')])" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def proof (intro conjI) let ?S = "t \ t'#S" let ?A = "\@[Step (Equality t t')]" have \: "\S'. S' \ update\<^sub>s\<^sub>t \ ?S \ S' = S \ S' \ \" by auto have 1: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto moreover have 2: "vars2\<^sub>e\<^sub>s\<^sub>t ?A = vars2\<^sub>e\<^sub>s\<^sub>t \ \ FV t \ FV t'" using vars2\<^sub>e\<^sub>s\<^sub>t_split(2) by (simp add: Un_assoc) ultimately have 3: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono) have 4: "\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by simp have "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis 3 \) have "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t S = {}" using 4 assms(2) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce+ thus "\S \ update\<^sub>s\<^sub>t \ ?S. \S' \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" by (metis 4 \) have "\S' \ \. FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t ?S = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by metis+ hence 5: "FV\<^sub>e\<^sub>s\<^sub>t ?A = FV\<^sub>e\<^sub>s\<^sub>t \ \ FV t \ FV t'" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = bvars\<^sub>e\<^sub>s\<^sub>t \" "\S' \ \. FV t \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV t' \ bvars\<^sub>s\<^sub>t S' = {}" using to_st_append by force+ have *: "\S \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using assms(2) by metis hence "FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by (metis * \) have **: "\S \ \. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" using 5 assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t ?S = {}" using assms(2) by metis hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by (metis ** \) qed lemma wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_ineq: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "\X\t \ t'\#S \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \ (\X\t \ t'\#S)) (\@[Step (Inequality X t t')])" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def proof (intro conjI) let ?S = "\X\t \ t'\#S" let ?A = "\@[Step (Inequality X t t')]" have \: "\S'. S' \ update\<^sub>s\<^sub>t \ ?S \ S' = S \ S' \ \" by auto have 1: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto moreover have 2: "vars2\<^sub>e\<^sub>s\<^sub>t ?A = vars2\<^sub>e\<^sub>s\<^sub>t \" using vars2\<^sub>e\<^sub>s\<^sub>t_split(2) by (simp add: Un_assoc) ultimately have 3: "\S \ \. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono) have 4: "\S \ \. \S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by simp have "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis 3 \) have "FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S = {}" "\S' \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t S = {}" using 4 assms(2) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce+ thus "\S \ update\<^sub>s\<^sub>t \ ?S. \S' \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>s\<^sub>t S' = {}" by (metis 4 \) have "\S' \ \. FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. FV\<^sub>s\<^sub>t S' \ bvars\<^sub>s\<^sub>t ?S = {}" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by metis+ hence 5: "FV\<^sub>e\<^sub>s\<^sub>t ?A = FV\<^sub>e\<^sub>s\<^sub>t \ \ (FV t \ FV t' - set X)" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = set X \ bvars\<^sub>e\<^sub>s\<^sub>t \" "\S' \ \. (FV t - set X) \ bvars\<^sub>s\<^sub>t S' = {}" "\S' \ \. (FV t' - set X) \ bvars\<^sub>s\<^sub>t S' = {}" "\S \ \. FV\<^sub>s\<^sub>t S \ set X = {}" using to_st_append by force+ hence 6: "\S' \ \. (FV t \ FV t' - set X) \ bvars\<^sub>s\<^sub>t S' = {}" by blast have *: "\S \ \. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using 5(2,5) assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by blast hence "FV\<^sub>s\<^sub>t ?S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using assms(2) by metis hence "FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by (metis * \) have **: "\S \ \. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" using 5(1) 6(1) assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (simp add: inf_sup_distrib2) hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t ?S = {}" using assms(2) by metis hence "FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by auto thus "\S \ update\<^sub>s\<^sub>t \ ?S. FV\<^sub>e\<^sub>s\<^sub>t ?A \ bvars\<^sub>s\<^sub>t S = {}" by (metis ** \) qed lemma wf\<^sub>s\<^sub>t\<^sub>s'_snd_vars: assumes "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "snd\t\#S \ \" shows "FV t \ vars2\<^sub>e\<^sub>s\<^sub>t \" proof - from assms have "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \) (dual\<^sub>s\<^sub>t (snd\t\#S))" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by blast thus ?thesis by auto qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq: assumes "x#S \ \" shows "\(trms\<^sub>s\<^sub>t ` update\<^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 ` \)" (is "?A = ?B") proof show "?B \ ?A" proof have "trm\<^sub>s\<^sub>t\<^sub>p x \ trms\<^sub>s\<^sub>t (x#S)" "trm_r\<^sub>s\<^sub>t\<^sub>p x \ trms\<^sub>s\<^sub>t (x#S)" by auto hence "\t'. t' \ ?B \ t' = trm\<^sub>s\<^sub>t\<^sub>p x \ t' \ ?A" "\t'. t' \ ?B \ t' = trm_r\<^sub>s\<^sub>t\<^sub>p x \ t' \ ?A" by simp_all moreover { fix t' assume t': "t' \ ?B" "t' \ trm\<^sub>s\<^sub>t\<^sub>p x" "t' \ trm_r\<^sub>s\<^sub>t\<^sub>p x" then obtain S' where S': "t' \ trms\<^sub>s\<^sub>t S'" "S' \ \" by auto hence "S' = x#S \ S' \ update\<^sub>s\<^sub>t \ (x#S)" by auto moreover { assume "S' = x#S" hence "t' \ trms\<^sub>s\<^sub>t S" using S' t' by simp hence "t' \ ?A" by auto } ultimately have "t' \ ?A" using t' S' by auto } ultimately show "\t'. t' \ ?B \ t' \ ?A" by metis qed show "?A \ ?B" proof have "\t'. t' \ ?A \ t' = trm\<^sub>s\<^sub>t\<^sub>p x \ trm\<^sub>s\<^sub>t\<^sub>p x \ ?B" "\t'. t' \ ?A \ t' = trm_r\<^sub>s\<^sub>t\<^sub>p x \ trm_r\<^sub>s\<^sub>t\<^sub>p x \ ?B" using assms by force+ moreover { fix t' assume t': "t' \ ?A" "t' \ trm\<^sub>s\<^sub>t\<^sub>p x" "t' \ trm_r\<^sub>s\<^sub>t\<^sub>p x" then obtain S' where "t' \ trms\<^sub>s\<^sub>t S'" "S' \ update\<^sub>s\<^sub>t \ (x#S)" by auto hence "S' = S \ S' \ \" by auto moreover have "trms\<^sub>s\<^sub>t S \ ?B" using assms trms\<^sub>s\<^sub>t_cons[of x S] by blast ultimately have "t' \ ?B" using t' by fastforce } ultimately show "\t'. t' \ ?A \ t' \ ?B" by metis qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_snd: assumes "snd\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (snd\t\#S)" "\' = \@[Step (Receive t)]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>e\<^sub>s\<^sub>t \') = (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using assms(1,3) to_st_append[of \ "[Step (Receive t)]"] by force+ { fix t' assume "t' \ trms\<^sub>e\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ {t}" using * by auto hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t' assume "t' \ (trms\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t}" using * by auto hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_rcv: assumes "rcv\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (rcv\t\#S)" "\' = \@[Step (Send t)]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>e\<^sub>s\<^sub>t \') = (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using assms(1,3) to_st_append[of \ "[Step (Receive t)]"] by force+ { fix t' assume "t' \ trms\<^sub>e\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ {t}" using * by auto hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t' assume "t' \ (trms\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t}" using * by auto hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq: assumes "t \ t'#S \ \" "\' = update\<^sub>s\<^sub>t \ (t \ t'#S)" "\' = \@[Step (Equality t t')]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>e\<^sub>s\<^sub>t \') = (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t} \ {t'}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}= \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" "t' \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using assms(1,3) by force+ { fix t' assume "t' \ trms\<^sub>e\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}" using * by auto hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t'' assume "t'' \ (trms\<^sub>e\<^sub>s\<^sub>t \')" hence "t'' \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t} \ {t'}" using * by auto hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_ineq: assumes "\X\t \ t'\#S \ \" "\' = update\<^sub>s\<^sub>t \ (\X\t \ t'\#S)" "\' = \@[Step (Inequality X t t')]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>e\<^sub>s\<^sub>t \') = (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t} \ {t'}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}= \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" "t' \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using assms(1,3) by force+ { fix t' assume "t' \ trms\<^sub>e\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}" using * by auto hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>e\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t'' assume "t'' \ (trms\<^sub>e\<^sub>s\<^sub>t \')" hence "t'' \ (trms\<^sub>e\<^sub>s\<^sub>t \) \ {t} \ {t'}" using * by auto hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_snd': assumes "snd\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (snd\t\#S)" "\' = \@[Receive t]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" proof - have *: "trms\<^sub>s\<^sub>t \' = trms\<^sub>s\<^sub>t \ \ {t}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using assms(1,3) to_est_append[of \ "[Receive t]"] by force+ { fix t' assume "t' \ trms\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ {t}" using * by auto hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t' assume "t' \ (trms\<^sub>s\<^sub>t \')" hence "t' \ (trms\<^sub>s\<^sub>t \) \ {t}" using * by auto hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_rcv': assumes "rcv\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (rcv\t\#S)" "\' = \@[Send t]" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>s\<^sub>t \') = (trms\<^sub>s\<^sub>t \) \ {t}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using assms(1,3) to_est_append[of \ "[Receive t]"] by force+ { fix t' assume "t' \ trms\<^sub>s\<^sub>t \" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ {t}" using * by auto hence "t' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t' assume "t' \ (trms\<^sub>s\<^sub>t \')" hence "t' \ (trms\<^sub>s\<^sub>t \) \ {t}" using * by auto hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t' assume "t' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq': assumes "t \ t'#S \ \" "\' = update\<^sub>s\<^sub>t \ (t \ t'#S)" "\' = \@[Equality t t']" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>s\<^sub>t \') = (trms\<^sub>s\<^sub>t \) \ {t} \ {t'}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" "t' \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using assms(1,3) to_est_append[of \ "[Receive t]"] by force+ { fix t'' assume "t'' \ trms\<^sub>s\<^sub>t \" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}" using * by auto hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t'' assume "t'' \ (trms\<^sub>s\<^sub>t \')" hence "t'' \ (trms\<^sub>s\<^sub>t \) \ {t} \ {t'}" using * by auto hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_ineq': assumes "\X\t \ t'\#S \ \" "\' = update\<^sub>s\<^sub>t \ (\X\t \ t'\#S)" "\' = \@[Inequality X t t']" shows "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) = (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" proof - have *: "(trms\<^sub>s\<^sub>t \') = (trms\<^sub>s\<^sub>t \) \ {t} \ {t'}" "\(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'} = \(trms\<^sub>s\<^sub>t ` \)" using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto show ?thesis proof have t_in: "t \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" "t' \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" "t' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using assms(1,3) to_est_append[of \ "[Receive t]"] by force+ { fix t'' assume "t'' \ trms\<^sub>s\<^sub>t \" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using * by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \)" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ {t} \ {t'}" using * by auto hence "t'' \ \(trms\<^sub>s\<^sub>t ` \') \ (trms\<^sub>s\<^sub>t \')" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \) \ (\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \')" by (meson Un_iff subsetI) { fix t'' assume "t'' \ (trms\<^sub>s\<^sub>t \')" hence "t'' \ (trms\<^sub>s\<^sub>t \) \ {t} \ {t'}" using * by auto hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } moreover { fix t'' assume "t'' \ \(trms\<^sub>s\<^sub>t ` \')" hence "t'' \ \(trms\<^sub>s\<^sub>t ` \) \ {t}" using * by blast hence "t'' \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" using t_in by auto } ultimately show "(\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \') \ (\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \)" by (meson Un_iff subsetI) qed qed lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset: assumes "x#S \ \" shows "\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \ (x#S))) \ \(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" (is ?A) "\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \ (x#S))) \ \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" (is ?B) proof - { fix t assume "t \ \(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \ (x#S)))" then obtain S' where S': "S' \ update\<^sub>s\<^sub>t \ (x#S)" "t \ ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S')" by auto have *: "ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S) \ ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t (x#S))" using ik_append[of "dual\<^sub>s\<^sub>t [x]" "dual\<^sub>s\<^sub>t S"] dual\<^sub>s\<^sub>t_append[of "[x]" S] by auto hence "t \ \(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" proof (cases "S' = S") case True thus ?thesis using * assms S' by auto next case False thus ?thesis using S' by auto qed } moreover { fix t assume "t \ \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \ (x#S)))" then obtain S' where S': "S' \ update\<^sub>s\<^sub>t \ (x#S)" "t \ eqs_rhs\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S')" by auto have *: "eqs_rhs\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S) \ eqs_rhs\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t (x#S))" using eqs_rhs_append[of "dual\<^sub>s\<^sub>t [x]" "dual\<^sub>s\<^sub>t S"] dual\<^sub>s\<^sub>t_append[of "[x]" S] by auto hence "t \ \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" proof (cases "S' = S") case True thus ?thesis using * assms S' by auto next case False thus ?thesis using S' by auto qed } ultimately show ?A ?B by (metis subsetI)+ qed lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_snd: assumes "snd\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (snd\t\#S)" "\' = \@[Step (Receive t)]" shows "(\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \') \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" (is ?A) "(\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \') \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" (is ?B) proof - { fix t' assume t'_in: "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \) \ {t}" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto moreover have "t \ \(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" using assms(1) by force ultimately have "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } moreover { fix t' assume t'_in: "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using assms eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } ultimately show ?A ?B by (metis subsetI)+ qed lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_rcv: assumes "rcv\t\#S \ \" "\' = update\<^sub>s\<^sub>t \ (rcv\t\#S)" "\' = \@[Step (Send t)]" shows "(\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \') \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" (is ?A) "(\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \') \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" (is ?B) proof - { fix t' assume t'_in: "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } moreover { fix t' assume t'_in: "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using assms eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } ultimately show ?A ?B by (metis subsetI)+ qed lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_eq: assumes "t \ t'#S \ \" "\' = update\<^sub>s\<^sub>t \ (t \ t'#S)" "\' = \@[Step (Equality t t')]" shows "(\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \') \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" (is ?A) "(\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \') \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" (is ?B) proof - { fix t' assume t'_in: "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } moreover { fix t'' assume t''_in: "t'' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \')" hence "t'' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \) \ {t'}" using assms eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by auto moreover have "t' \ \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)" using assms(1) by force ultimately have "t'' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } ultimately show ?A ?B by (metis subsetI)+ qed lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_ineq: assumes "\X\t \ t'\#S \ \" "\' = update\<^sub>s\<^sub>t \ (\X\t \ t'\#S)" "\' = \@[Step (Inequality X t t')]" shows "(\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \') \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" (is ?A) "(\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \') \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" (is ?B) proof - { fix t' assume t'_in: "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (ik\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } moreover { fix t' assume t'_in: "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \')" hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \')) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using assms eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append by auto hence "t' \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \)) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)" using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto } ultimately show ?A ?B by (metis subsetI)+ qed subsection {* Transition systems definitions *} inductive pts_symbolic:: "(('fun,'var) protocol \ ('fun,'var) strand) \ (('fun,'var) protocol \ ('fun,'var) strand) \ bool" (infix "\\<^sup>\" 50) where Nil[simp]: "[] \ \ \ (\,\) \\<^sup>\ (update\<^sub>s\<^sub>t \ [],\)" | Send[simp]: "snd\t\#S \ \ \ (\,\) \\<^sup>\ (update\<^sub>s\<^sub>t \ (snd\t\#S),\@[Receive t])" | Receive[simp]: "rcv\t\#S \ \ \ (\,\) \\<^sup>\ (update\<^sub>s\<^sub>t \ (rcv\t\#S),\@[Send t])" | Equality[simp]: "t \ t'#S \ \ \ (\,\) \\<^sup>\ (update\<^sub>s\<^sub>t \ (t \ t'#S),\@[Equality t t'])" | Inequality[simp]: "\X\t \ t'\#S \ \ \ (\,\) \\<^sup>\ (update\<^sub>s\<^sub>t \ (\X\t \ t'\#S),\@[Inequality X t t'])" inductive pts_symbolic_c:: "(('fun,'var) protocol \ ('fun,'var) extstrand) \ (('fun,'var) protocol \ ('fun,'var) extstrand) \ bool" (infix "\\<^sup>\\<^sub>c" 50) where Nil[simp]: "[] \ \ \ (\,\) \\<^sup>\\<^sub>c (update\<^sub>s\<^sub>t \ [],\)" | Send[simp]: "snd\t\#S \ \ \ (\,\) \\<^sup>\\<^sub>c (update\<^sub>s\<^sub>t \ (snd\t\#S),\@[Step (rcv\t\)])" | Receive[simp]: "rcv\t\#S \ \ \ (\,\) \\<^sup>\\<^sub>c (update\<^sub>s\<^sub>t \ (rcv\t\#S),\@[Step (snd\t\)])" | Equality[simp]: "t \ t'#S \ \ \ (\,\) \\<^sup>\\<^sub>c (update\<^sub>s\<^sub>t \ (t \ t'#S),\@[Step (t \ t')])" | Inequality[simp]: "\X\t \ t'\#S \ \ \ (\,\) \\<^sup>\\<^sub>c (update\<^sub>s\<^sub>t \ (\X\t \ t'\#S),\@[Step (\X\t \ t'\)])" | Decompose[simp]: "Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \ \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)) \ (\,\) \\<^sup>\\<^sub>c (\,\@[Decomp (Fun f T)])" abbreviation pts_symbolic_trancl (infix "\\<^sup>\\<^sup>+" 50) where "a \\<^sup>\\<^sup>+ b \ pts_symbolic\<^sup>+\<^sup>+ a b" abbreviation pts_symbolic_rtrancl (infix "\\<^sup>\\<^sup>*" 50) where "a \\<^sup>\\<^sup>* b \ pts_symbolic\<^sup>*\<^sup>* a b" abbreviation pts_symbolic_c_trancl (infix "\\<^sup>\\<^sub>c\<^sup>+" 50) where "a \\<^sup>\\<^sub>c\<^sup>+ b \ pts_symbolic_c\<^sup>+\<^sup>+ a b" abbreviation pts_symbolic_c_rtrancl (infix "\\<^sup>\\<^sub>c\<^sup>*" 50) where "a \\<^sup>\\<^sub>c\<^sup>* b \ pts_symbolic_c\<^sup>*\<^sup>* a b" lemma pts_symbolic_induct[consumes 1, case_names Nil Send Receive Equality Inequality]: assumes "(\,\) \\<^sup>\ (\',\')" and "\[] \ \; \' = update\<^sub>s\<^sub>t \ []; \' = \\ \ P" and "\t S. \snd\t\#S \ \; \' = update\<^sub>s\<^sub>t \ (snd\t\#S); \' = \@[rcv\t\]\ \ P" and "\t S. \rcv\t\#S \ \; \' = update\<^sub>s\<^sub>t \ (rcv\t\#S); \' = \@[snd\t\]\ \ P" and "\t t' S. \t \ t'#S \ \; \' = update\<^sub>s\<^sub>t \ (t \ t'#S); \' = \@[t \ t']\ \ P" and "\X t t' S. \\X\t \ t'\#S \ \; \' = update\<^sub>s\<^sub>t \ (\X\t \ t'\#S); \' = \@[\X\t \ t'\]\ \ P" shows "P" apply (rule pts_symbolic.cases[OF assms(1)]) using assms(2,3,4,5,6) by simp_all lemma pts_symbolic_c_induct[consumes 1, case_names Nil Send Receive Equality Inequality Decompose]: assumes "(\,\) \\<^sup>\\<^sub>c (\',\')" and "\[] \ \; \' = update\<^sub>s\<^sub>t \ []; \' = \\ \ P" and "\t S. \snd\t\#S \ \; \' = update\<^sub>s\<^sub>t \ (snd\t\#S); \' = \@[Step (Receive t)]\ \ P" and "\t S. \rcv\t\#S \ \; \' = update\<^sub>s\<^sub>t \ (rcv\t\#S); \' = \@[Step (Send t)]\ \ P" and "\t t' S. \t \ t'#S \ \; \' = update\<^sub>s\<^sub>t \ (t \ t'#S); \' = \@[Step (Equality t t')]\ \ P" and "\X t t' S. \\X\t \ t'\#S \ \; \' = update\<^sub>s\<^sub>t \ (\X\t \ t'\#S); \' = \@[Step (Inequality X t t')]\ \ P" and "\f T. \Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \ \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)); \' = \; \' = \@[Decomp (Fun f T)]\ \ P" shows "P" apply (rule pts_symbolic_c.cases[OF assms(1)]) using assms(2,3,4,5,6,7) by simp_all lemma pts_symbolic_preserves_wf_prot: assumes "(\,\) \\<^sup>\\<^sup>* (\',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \ (to_est \)" shows "wf\<^sub>s\<^sub>t\<^sub>s' \' (to_est \')" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case apply (induction rule: pts_symbolic_induct) by (metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_nil, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_snd to_est_append to_est.simps, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_rcv to_est_append to_est.simps, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_eq to_est_append to_est.simps, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_ineq to_est_append to_est.simps) qed metis lemma pts_symbolic_c_preserves_wf_prot: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \ \" shows "wf\<^sub>s\<^sub>t\<^sub>s' \' \'" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Decompose hence "FV\<^sub>e\<^sub>s\<^sub>t \2 = FV\<^sub>e\<^sub>s\<^sub>t \1" "bvars\<^sub>e\<^sub>s\<^sub>t \2 = bvars\<^sub>e\<^sub>s\<^sub>t \1" using bvars_decomp ik_eqs_rhs_decomp_FV by auto thus ?case using Decompose unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by (metis wf_vars_mono vars2\<^sub>e\<^sub>s\<^sub>t_split(2)) qed (metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_nil, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_snd, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_rcv, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_eq, metis wf\<^sub>s\<^sub>t\<^sub>s'_update\<^sub>s\<^sub>t_ineq) qed metis lemma pts_symbolic_preserves_wf_is: assumes "(\,\) \\<^sup>\\<^sup>* (\',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \ (to_est \)" "wf\<^sub>s\<^sub>t V \" shows "wf\<^sub>s\<^sub>t V \'" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) hence "(\, \) \\<^sup>\\<^sup>* (\2, \2)" by auto hence *: "wf\<^sub>s\<^sub>t\<^sub>s' \1 (to_est \1)" "wf\<^sub>s\<^sub>t\<^sub>s' \2 (to_est \2)" using pts_symbolic_preserves_wf_prot[OF _ step.prems(1)] step.hyps(1) by auto from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_induct) case Nil thus ?case by auto next case (Send t S) hence "wf\<^sub>s\<^sub>t (vars2\<^sub>s\<^sub>t \1) (rcv\t\#(dual\<^sub>s\<^sub>t S))" using *(1) to_est_vars2\<^sub>e\<^sub>s\<^sub>t unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce hence "FV t \ vars2\<^sub>s\<^sub>t \1 \ V" by auto thus ?case using Send wf_rcv_append''' to_st_append by simp next case Receive thus ?case using wf_snd_append to_st_append by simp next case (Equality t t' S) hence "wf\<^sub>s\<^sub>t (vars2\<^sub>s\<^sub>t \1) (t \ t'#(dual\<^sub>s\<^sub>t S))" using *(1) to_est_vars2\<^sub>e\<^sub>s\<^sub>t unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce hence "FV t' \ vars2\<^sub>s\<^sub>t \1 \ V" by auto thus ?case using Equality wf_eq_append''' to_st_append by simp next case (Inequality t t' S) thus ?case using wf_ineq_append'' by simp qed qed metis lemma pts_symbolic_c_preserves_wf_is: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "wf\<^sub>s\<^sub>t V (to_st \)" shows "wf\<^sub>s\<^sub>t V (to_st \')" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) hence "(\, \) \\<^sup>\\<^sub>c\<^sup>* (\2, \2)" by auto hence *: "wf\<^sub>s\<^sub>t\<^sub>s' \1 \1" "wf\<^sub>s\<^sub>t\<^sub>s' \2 \2" using pts_symbolic_c_preserves_wf_prot[OF _ step.prems(1)] step.hyps(1) by auto from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Nil thus ?case by auto next case (Send t S) hence "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \1) (rcv\t\#(dual\<^sub>s\<^sub>t S))" using *(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce hence "FV t \ vars2\<^sub>s\<^sub>t (to_st \1) \ V" using vars2\<^sub>e\<^sub>s\<^sub>t_eq_vars2\<^sub>s\<^sub>t by auto thus ?case using Send wf_rcv_append''' to_st_append by simp next case Receive thus ?case using wf_snd_append to_st_append by simp next case (Equality t t' S) hence "wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t \1) (t \ t'#(dual\<^sub>s\<^sub>t S))" using *(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fastforce hence "FV t' \ vars2\<^sub>s\<^sub>t (to_st \1) \ V" using vars2\<^sub>e\<^sub>s\<^sub>t_eq_vars2\<^sub>s\<^sub>t by auto thus ?case using Equality wf_eq_append''' to_st_append by simp next case (Inequality t t' S) thus ?case using wf_ineq_append'' to_st_append by simp next case (Decompose f T) hence "FV (Fun f T) \ vars2\<^sub>e\<^sub>s\<^sub>t \1" by (metis FV_set_subterms_eq FV_subset subset_trans ik\<^sub>e\<^sub>s\<^sub>t_eqs_rhs\<^sub>e\<^sub>s\<^sub>t_vars2_subset) hence "vars\<^sub>s\<^sub>t (decomp (Fun f T)) \ vars2\<^sub>s\<^sub>t (to_st \1) \ V" using decomp_vars[of "Fun f T"] vars2\<^sub>e\<^sub>s\<^sub>t_eq_vars2\<^sub>s\<^sub>t[of \1] by auto thus ?case using to_st_append[of \1 "[Decomp (Fun f T)]"] wf_append_suffix[OF Decompose.prems] Decompose.hyps(3) by (metis append_Nil2 decomp_vars to_st.simps(1,3)) qed qed metis lemma pts_symbolic_preserves_tfr: assumes "(\,\) \\<^sup>\\<^sup>* (\',\')" "tfr\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>s\<^sub>t \))" shows "tfr\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>s\<^sub>t \'))" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_induct) case Nil hence "\(trms\<^sub>s\<^sub>t ` \1) = \(trms\<^sub>s\<^sub>t ` \2)" by force thus ?case using Nil by metis next case Send thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_snd') next case Receive thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_rcv') next case Equality thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq') next case Inequality thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_ineq') qed qed metis lemma pts_symbolic_c_preserves_tfr: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "tfr\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \)) \ (trms\<^sub>e\<^sub>s\<^sub>t \))" shows "tfr\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \')) \ (trms\<^sub>e\<^sub>s\<^sub>t \'))" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Nil hence "\(trms\<^sub>s\<^sub>t ` \1) = \(trms\<^sub>s\<^sub>t ` \2)" by force thus ?case using Nil by metis next case Send thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_snd) next case Receive thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_rcv) next case Equality thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq) next case Inequality thus ?case by (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_ineq) next case (Decompose f T) obtain t where t: "t \ ik\<^sub>e\<^sub>s\<^sub>t \1 \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1" "Fun f T \ t" using subterms_UnionE[OF Decompose.hyps(1)] by auto have t_wf: "wf\<^sub>t\<^sub>r\<^sub>m t" using Decompose.prems subterms_UnionE[OF trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhsI[OF t(1)]] wf_trm_subterm[of _ t] unfolding subterm_def subtermeq_def by (metis Un_iff) have "t \ \(subterms ` trms\<^sub>e\<^sub>s\<^sub>t \1)" using trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_eqs_rhsI t by auto hence "Fun f T \ SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \1)" by (metis SMP\<^sub>s\<^sub>t.MP SMP\<^sub>s\<^sub>t.Subterm subterm_def subterms_UnionE t(2)) hence "{Fun f T} \ SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \1)" using SMP\<^sub>s\<^sub>t.Subterm[of "Fun f T"] by auto moreover have "trms\<^sub>e\<^sub>s\<^sub>t \2 = insert (Fun f T) (trms\<^sub>e\<^sub>s\<^sub>t \1)" using Decompose.hyps(3) by auto ultimately have *: "SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \1) = SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \2)" using SMP_subset_union_eq[of "{Fun f T}"] by (simp add: Un_commute) hence "SMP\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \1)) \ (trms\<^sub>e\<^sub>s\<^sub>t \1)) = SMP\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \2)) \ (trms\<^sub>e\<^sub>s\<^sub>t \2))" using Decompose.hyps(2) SMP_append' by auto moreover have "\t \ trms\<^sub>e\<^sub>s\<^sub>t \1. wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" using Decompose.prems wf_trm_subterm t(2) t_wf by auto hence "\t \ trms\<^sub>e\<^sub>s\<^sub>t \2. wf\<^sub>t\<^sub>r\<^sub>m t" by (metis * SMP\<^sub>s\<^sub>t.MP SMP_wf_trm) hence "\t \ (\(trms\<^sub>s\<^sub>t ` \2)) \ (trms\<^sub>e\<^sub>s\<^sub>t \2). wf\<^sub>t\<^sub>r\<^sub>m t" using Decompose.prems Decompose.hyps(2) by force ultimately show ?thesis using Decompose.prems by presburger qed qed lemma pts_symbolic_c_preserves_eqs_tfr: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "\S \ \ \ {to_st \}. eqs_tfr\<^sub>s\<^sub>t S" shows "\S \ \' \ {to_st \'}. eqs_tfr\<^sub>s\<^sub>t S" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Nil have "\S \ {to_st \2}. eqs_tfr\<^sub>s\<^sub>t S" using Nil by simp moreover have "\2 = \1 - {[]}" "\S \ \1. eqs_tfr\<^sub>s\<^sub>t S" using Nil by simp_all hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" using Nil by auto ultimately show ?case by auto next case (Send t S) have "\S \ {to_st \2}. eqs_tfr\<^sub>s\<^sub>t S" using Send by (simp add: to_st_append) moreover have "\2 = insert S (\1 - {snd\t\#S})" "\S \ \1. eqs_tfr\<^sub>s\<^sub>t S" using Send by simp_all hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" using Send by auto ultimately show ?case by auto next case (Receive t S) have "\S \ {to_st \2}. eqs_tfr\<^sub>s\<^sub>t S" using Receive by (simp add: to_st_append) moreover have "\2 = insert S (\1 - {rcv\t\#S})" "\S \ \1. eqs_tfr\<^sub>s\<^sub>t S" using Receive by simp_all hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" using Receive by auto ultimately show ?case by auto next case (Equality t t' S) have "to_st \2 = to_st \1@[t \ t']" "eqs_tfr\<^sub>s\<^sub>t (to_st \1)" using Equality by (simp_all add: to_st_append) moreover have "eqs_tfr\<^sub>s\<^sub>t [t \ t']" using Equality by simp ultimately have "eqs_tfr\<^sub>s\<^sub>t (to_st \2)" using eqs_tfr_append by metis hence "\S \ {to_st \2}. eqs_tfr\<^sub>s\<^sub>t S" using Equality by simp moreover have "\2 = insert S (\1 - {t \ t'#S})" "\S \ \1. eqs_tfr\<^sub>s\<^sub>t S" using Equality by simp_all hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" using Equality by auto ultimately show ?case by auto next case (Inequality X t t' S) have "to_st \2 = to_st \1@[\X\t \ t'\]" "eqs_tfr\<^sub>s\<^sub>t (to_st \1)" using Inequality by (simp_all add: to_st_append) moreover have "eqs_tfr\<^sub>s\<^sub>t [\X\t \ t'\]" using Inequality by auto ultimately have "eqs_tfr\<^sub>s\<^sub>t (to_st \2)" using eqs_tfr_append by metis hence "\S \ {to_st \2}. eqs_tfr\<^sub>s\<^sub>t S" using Inequality by simp moreover have "\2 = insert S (\1 - {\X\t \ t'\#S})" "\S \ \1. eqs_tfr\<^sub>s\<^sub>t S" using Inequality by simp_all hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" using Inequality by auto ultimately show ?case by auto next case (Decompose f T) hence "\S \ \2. eqs_tfr\<^sub>s\<^sub>t S" by blast moreover have "eqs_tfr\<^sub>s\<^sub>t (to_st \1)" "eqs_tfr\<^sub>s\<^sub>t (to_st [Decomp (Fun f T)])" using Decompose.prems decomp_no_eqs by auto hence "eqs_tfr\<^sub>s\<^sub>t (to_st \1@to_st [Decomp (Fun f T)])" by (metis eqs_tfr_append[of "to_st \1" "to_st [Decomp (Fun f T)]"]) hence "eqs_tfr\<^sub>s\<^sub>t (to_st \2)" using Decompose.hyps(3) to_st_append[of \1 "[Decomp (Fun f T)]"] by auto ultimately show ?case by blast qed qed lemma pts_symbolic_c_preserves_well_analyzed: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "well_analyzed \" shows "well_analyzed \'" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Receive thus ?case by (metis well_analyzed_singleton(1) well_analyzed_append Receive.prems Receive.hyps(3)) next case Send thus ?case by (metis well_analyzed_singleton(2) well_analyzed_append Send.prems Send.hyps(3)) next case Equality thus ?case by (metis well_analyzed_singleton(3) well_analyzed_append Equality.prems Equality.hyps(3)) next case Inequality thus ?case by (metis well_analyzed_singleton(4) well_analyzed_append Inequality.prems Inequality.hyps(3)) next case (Decompose f T) hence "Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \1 \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1)) - (Var`\)" by auto thus ?case by (metis well_analyzed.Decomp Decompose.prems Decompose.hyps(3)) qed simp qed metis lemma pts_symbolic_c_preserves_fun_decomps\<^sub>e\<^sub>s\<^sub>t_only: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "\t. Decomp t \ set \ \ \f T. t = Fun f T" "Decomp t \ set \'" shows "\f T. t = Fun f T" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) hence "Decomp t \ set \1 \ \f T. t = Fun f T" by auto with step.hyps(2) step.prems show ?case by (induct rule: pts_symbolic_c_induct) auto qed metis lemma pts_symbolic_c_preserves_Ana_invar_subst: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" and "Ana_invar_subst ((\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \) \ (ik\<^sub>e\<^sub>s\<^sub>t \)) \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \)))" shows "Ana_invar_subst ((\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \') \ (ik\<^sub>e\<^sub>s\<^sub>t \')) \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \') \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \')))" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Nil hence "\(ik\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \1) = \(ik\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \2)" "\(eqs_rhs\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \1) = \(eqs_rhs\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \2)" by auto thus ?case using Nil by metis next case Send show ?case using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_snd[OF Send.hyps] Ana_invar_subst_subset[OF Send.prems] by (metis Un_mono) next case Receive show ?case using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_rcv[OF Receive.hyps] Ana_invar_subst_subset[OF Receive.prems] by (metis Un_mono) next case Equality show ?case using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_eq[OF Equality.hyps] Ana_invar_subst_subset[OF Equality.prems] by (metis Un_mono) next case Inequality show ?case using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_ineq[OF Inequality.hyps] Ana_invar_subst_subset[OF Inequality.prems] by (metis Un_mono) next case (Decompose f T) let ?X = "\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\2) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \2" let ?Y = "\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\1) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1" obtain K M where Ana: "Ana (Fun f T) = (K,M)" by moura hence *: "ik\<^sub>e\<^sub>s\<^sub>t \2 = ik\<^sub>e\<^sub>s\<^sub>t \1 \ M" "eqs_rhs\<^sub>e\<^sub>s\<^sub>t \2 = eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1" using ik\<^sub>e\<^sub>s\<^sub>t_append eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append decomp_ik decomp_eqs_rhs_empty Decompose.hyps(3) by auto { fix g S assume "Fun g S \ \(subterms ` (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\2) \ ik\<^sub>e\<^sub>s\<^sub>t \2 \ ?X))" hence "Fun g S \ \(subterms ` (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \1) \ ik\<^sub>e\<^sub>s\<^sub>t \1 \ M \ ?X))" using * Decompose.hyps(2) by auto hence "Fun g S \ \(subterms ` (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \1))) \ Fun g S \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \1)) \ Fun g S \ \(subterms ` M) \ Fun g S \ \(subterms ` \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\1)) \ Fun g S \ \(subterms ` (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1))" using Decompose * Ana_fun_subterm[OF Ana] by auto moreover have "Fun f T \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \1 \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1))" using trm\<^sub>e\<^sub>s\<^sub>t\<^sub>p_ik_subtermsI Decompose.hyps(1) by auto hence "subterms (Fun f T) \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \1 \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1))" by (metis in_subterms_subset_Union) hence "\(subterms ` M) \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t \1 \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1))" by (meson Un_upper2 Ana_subterm[OF Ana] in_subterms_subset' psubsetE subset_trans) ultimately have "Fun g S \ \(subterms ` (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \1) \ ik\<^sub>e\<^sub>s\<^sub>t \1 \ ?Y))" by auto } thus ?case using Decompose unfolding Ana_invar_subst by metis qed qed lemma pts_symbolic_c_preserves_constr_disj_vars: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \ \" "FV\<^sub>e\<^sub>s\<^sub>t \ \ bvars\<^sub>e\<^sub>s\<^sub>t \ = {}" shows "FV\<^sub>e\<^sub>s\<^sub>t \' \ bvars\<^sub>e\<^sub>s\<^sub>t \' = {}" using assms proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) have *: "\S. S \ \1 \ FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t \1 = {}" "\S. S \ \1 \ FV\<^sub>e\<^sub>s\<^sub>t \1 \ bvars\<^sub>s\<^sub>t S = {}" using pts_symbolic_c_preserves_wf_prot[OF step.hyps(1) step.prems(1)] unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto from step.hyps(2) step.IH[OF step.prems] show ?case proof (induction rule: pts_symbolic_c_induct) case Nil thus ?case by auto next case (Send t S) hence "FV\<^sub>e\<^sub>s\<^sub>t \2 = FV\<^sub>e\<^sub>s\<^sub>t \1 \ FV t" "bvars\<^sub>e\<^sub>s\<^sub>t \2 = bvars\<^sub>e\<^sub>s\<^sub>t \1" "FV\<^sub>s\<^sub>t (snd\t\#S) = FV t \ FV\<^sub>s\<^sub>t S" using FV\<^sub>e\<^sub>s\<^sub>t_append bvars\<^sub>e\<^sub>s\<^sub>t_append by simp_all thus ?case using *(1)[OF Send(1)] Send(4) by auto next case (Receive t S) hence "FV\<^sub>e\<^sub>s\<^sub>t \2 = FV\<^sub>e\<^sub>s\<^sub>t \1 \ FV t" "bvars\<^sub>e\<^sub>s\<^sub>t \2 = bvars\<^sub>e\<^sub>s\<^sub>t \1" "FV\<^sub>s\<^sub>t (rcv\t\#S) = FV t \ FV\<^sub>s\<^sub>t S" using FV\<^sub>e\<^sub>s\<^sub>t_append bvars\<^sub>e\<^sub>s\<^sub>t_append by simp_all thus ?case using *(1)[OF Receive(1)] Receive(4) by auto next case (Equality t t' S) hence "FV\<^sub>e\<^sub>s\<^sub>t \2 = FV\<^sub>e\<^sub>s\<^sub>t \1 \ FV t \ FV t'" "bvars\<^sub>e\<^sub>s\<^sub>t \2 = bvars\<^sub>e\<^sub>s\<^sub>t \1" "FV\<^sub>s\<^sub>t (t \ t'#S) = FV t \ FV t' \ FV\<^sub>s\<^sub>t S" using FV\<^sub>e\<^sub>s\<^sub>t_append bvars\<^sub>e\<^sub>s\<^sub>t_append by auto thus ?case using *(1)[OF Equality(1)] Equality(4) by auto next case (Inequality X t t' S) hence "FV\<^sub>e\<^sub>s\<^sub>t \2 = FV\<^sub>e\<^sub>s\<^sub>t \1 \ (FV t \ FV t' - set X)" "bvars\<^sub>e\<^sub>s\<^sub>t \2 = bvars\<^sub>e\<^sub>s\<^sub>t \1 \ set X" "FV\<^sub>s\<^sub>t (\X\t \ t'\#S) = (FV t \ FV t' - set X) \ FV\<^sub>s\<^sub>t S" using FV\<^sub>e\<^sub>s\<^sub>t_append bvars\<^sub>e\<^sub>s\<^sub>t_append by auto moreover have "FV\<^sub>e\<^sub>s\<^sub>t \1 \ set X = {}" using *(2)[OF Inequality(1)] by auto ultimately show ?case using *(1)[OF Inequality(1)] Inequality(4) by auto next case (Decompose f T) thus ?case using Decompose(3,4) bvars_decomp ik_eqs_rhs_decomp_FV[OF Decompose(1)] by auto qed qed subsection {* Typing result lifted to the transition systems *} lemma wf\<^sub>s\<^sub>t\<^sub>s'_decomp_rm: assumes "well_analyzed A" "wf\<^sub>s\<^sub>t\<^sub>s' S (decomp_rm\<^sub>e\<^sub>s\<^sub>t A)" shows "wf\<^sub>s\<^sub>t\<^sub>s' S A" unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def proof (intro conjI) show "\S\S. wf\<^sub>s\<^sub>t (vars2\<^sub>e\<^sub>s\<^sub>t A) (dual\<^sub>s\<^sub>t S)" by (metis (no_types) assms(2) wf\<^sub>s\<^sub>t\<^sub>s'_def vars2\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_subset wf_vars_mono le_iff_sup) show "\Sa\S. \S'\S. FV\<^sub>s\<^sub>t Sa \ bvars\<^sub>s\<^sub>t S' = {}" by (metis assms(2) wf\<^sub>s\<^sub>t\<^sub>s'_def) show "\S\S. FV\<^sub>s\<^sub>t S \ bvars\<^sub>e\<^sub>s\<^sub>t A = {}" by (metis assms(2) wf\<^sub>s\<^sub>t\<^sub>s'_def bvars_decomp_rm) show "\S\S. FV\<^sub>e\<^sub>s\<^sub>t A \ bvars\<^sub>s\<^sub>t S = {}" by (metis assms wf\<^sub>s\<^sub>t\<^sub>s'_def well_analyzed_decomp_rm\<^sub>e\<^sub>s\<^sub>t_FV) qed lemma decomps\<^sub>e\<^sub>s\<^sub>t_pts_symbolic_c: assumes "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t A) \" shows "(S,A) \\<^sup>\\<^sub>c\<^sup>* (S,A@D)" using assms(1) proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct) case (Decomp B f X K T) have "\(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t A \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t A)) \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t (A@B) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B)))" using ik\<^sub>e\<^sub>s\<^sub>t_append[of A B] eqs_rhs\<^sub>e\<^sub>s\<^sub>t_append[of A B] by auto hence "Fun f X \ \(subterms ` (ik\<^sub>e\<^sub>s\<^sub>t (A@B) \ eqs_rhs\<^sub>e\<^sub>s\<^sub>t (A@B)))" using Decomp.hyps by auto hence "(S,A@B) \\<^sup>\\<^sub>c (S,A@B@[Decomp (Fun f X)])" using pts_symbolic_c.Decompose[of f X "A@B"] by simp thus ?case using Decomp.IH rtrancl_into_rtrancl rtranclp_rtrancl_eq[of pts_symbolic_c "(S,A)" "(S,A@B)"] by auto qed simp lemma pts_symbolic_to_pts_symbolic_c: assumes "(\,to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)) \\<^sup>\\<^sup>* (\',\')" "sem\<^sub>e\<^sub>s\<^sub>t_d {} \ (to_est \')" "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ \\<^sub>d" and wf: "wf\<^sub>s\<^sub>t\<^sub>s' \ (decomp_rm\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)" "wf\<^sub>e\<^sub>s\<^sub>t {} \\<^sub>d" and tar: "Ana_invar_subst ((\(ik\<^sub>s\<^sub>t` dual\<^sub>s\<^sub>t` \) \ (ik\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)) \ (\(eqs_rhs\<^sub>s\<^sub>t` dual\<^sub>s\<^sub>t` \) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)))" and wa: "well_analyzed \\<^sub>d" and \: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "\\\<^sub>d'. \' = to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \\<^sub>d') \ (\,\\<^sub>d) \\<^sup>\\<^sub>c\<^sup>* (\',\\<^sub>d') \ sem\<^sub>e\<^sub>s\<^sub>t_c {} \ \\<^sub>d'" using assms(1,2) proof (induction rule: rtranclp_induct2) case refl thus ?case using assms by auto next case (step \1 \1 \2 \2) have "sem\<^sub>e\<^sub>s\<^sub>t_d {} \ (to_est \1)" using step.hyps(2) step.prems by (induct rule: pts_symbolic_induct, metis, (metis sem\<^sub>e\<^sub>s\<^sub>t_d_split_left to_est_append)+) then obtain \1d where \1d: "\1 = to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1d)" "(\, \\<^sub>d) \\<^sup>\\<^sub>c\<^sup>* (\1, \1d)" "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ \1d" using step.IH by moura show ?case using step.hyps(2) proof (induction rule: pts_symbolic_induct) case Nil hence "(\, \\<^sub>d) \\<^sup>\\<^sub>c\<^sup>* (\2, \1d)" using \1d pts_symbolic_c.Nil[OF Nil.hyps(1), of \1d] by simp thus ?case using \1d Nil by auto next case (Send t S) hence "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (\1d@[Step (Receive t)])" using sem\<^sub>e\<^sub>s\<^sub>t_c.Receive[OF \1d(3)] by simp moreover have "(\1, \1d) \\<^sup>\\<^sub>c (\2, \1d@[Step (Receive t)])" using Send.hyps(2) pts_symbolic_c.Send[OF Send.hyps(1), of \1d] by simp moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\1d@[Step (Receive t)])) = \2" using Send.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \1d(1) by (simp add: to_st_append) ultimately show ?case using \1d(2) by auto next case (Equality t t' S) hence "t \ \ = t' \ \" using step.prems sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \ "to_est \2"] to_st_append to_est_append to_st_to_est_inv by auto hence "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (\1d@[Step (Equality t t')])" using sem\<^sub>e\<^sub>s\<^sub>t_c.Equality[OF \1d(3)] by simp moreover have "(\1, \1d) \\<^sup>\\<^sub>c (\2, \1d@[Step (Equality t t')])" using Equality.hyps(2) pts_symbolic_c.Equality[OF Equality.hyps(1), of \1d] by simp moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\1d@[Step (Equality t t')])) = \2" using Equality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \1d(1) by (simp add: to_st_append) ultimately show ?case using \1d(2) by auto next case (Inequality X t t' S) hence "\\. 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' \ \ \ \" using step.prems sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \ "to_est \2"] to_st_append to_est_append to_st_to_est_inv by auto hence "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (\1d@[Step (Inequality X t t')])" using sem\<^sub>e\<^sub>s\<^sub>t_c.Inequality[OF \1d(3)] by simp moreover have "(\1, \1d) \\<^sup>\\<^sub>c (\2, \1d@[Step (Inequality X t t')])" using Inequality.hyps(2) pts_symbolic_c.Inequality[OF Inequality.hyps(1), of \1d] by simp moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\1d@[Step (Inequality X t t')])) = \2" using Inequality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \1d(1) by (simp add: to_st_append) ultimately show ?case using \1d(2) by auto next case (Receive t S) hence "ik\<^sub>s\<^sub>t \1 \set \ \ t \ \" using step.prems sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \ "to_est \2"] strand_sem_split_right_d[of "{}" \1 "[snd\t\]" \] to_st_append to_est_append to_st_to_est_inv by auto moreover have "ik\<^sub>s\<^sub>t \1 \set \ \ ik\<^sub>e\<^sub>s\<^sub>t \1d \set \" using \1d(1) decomp_rm\<^sub>e\<^sub>s\<^sub>t_ik_subset by auto ultimately have *: "ik\<^sub>e\<^sub>s\<^sub>t \1d \set \ \ t \ \" using ideduct_mono by auto have "wf\<^sub>s\<^sub>t\<^sub>s' \ \\<^sub>d" by (rule wf\<^sub>s\<^sub>t\<^sub>s'_decomp_rm[OF wa assms(4)]) hence **: "wf\<^sub>e\<^sub>s\<^sub>t {} \1d" by (rule pts_symbolic_c_preserves_wf_is[OF \1d(2) _ assms(5)]) have "Ana_invar_subst (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\1) \ (ik\<^sub>e\<^sub>s\<^sub>t \1d) \ (\(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\1) \ (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1d)))" using tar \1d(2) pts_symbolic_c_preserves_Ana_invar_subst by metis hence "Ana_invar_subst (ik\<^sub>e\<^sub>s\<^sub>t \1d)" "Ana_invar_subst (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1d)" using Ana_invar_subst_subset by blast+ moreover have "well_analyzed \1d" using pts_symbolic_c_preserves_well_analyzed[OF \1d(2) wa] by metis ultimately obtain D where D: "D \ decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \1d) (eqs_rhs\<^sub>e\<^sub>s\<^sub>t \1d) \" "ik\<^sub>e\<^sub>s\<^sub>t (\1d@D) \set \ \\<^sub>c t \ \" using decomps\<^sub>e\<^sub>s\<^sub>t_exist_subst[OF * \1d(3) ** assms(8)] by auto have "(\, \\<^sub>d) \\<^sup>\\<^sub>c\<^sup>* (\1, \1d@D)" using \1d(2) decomps\<^sub>e\<^sub>s\<^sub>t_pts_symbolic_c[OF D(1), of \1] by auto hence "(\, \\<^sub>d) \\<^sup>\\<^sub>c\<^sup>* (\2, \1d@D@[Step (Send t)])" using Receive(2) pts_symbolic_c.Receive[OF Receive.hyps(1), of "\1d@D"] by auto moreover have "\2 = to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\1d@D@[Step (Send t)]))" using Receive.hyps(3) \1d(1) decomps\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_empty[OF D(1)] decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append by auto moreover have "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ (\1d@D@[Step (Send t)])" using D(2) sem\<^sub>e\<^sub>s\<^sub>t_c.Send[OF sem\<^sub>e\<^sub>s\<^sub>t_c_decomps\<^sub>e\<^sub>s\<^sub>t_append[OF \1d(3) D(1)]] by simp ultimately show ?case by auto qed qed lemma pts_symbolic_c_to_pts_symbolic: assumes "(\,\) \\<^sup>\\<^sub>c\<^sup>* (\',\')" "sem\<^sub>e\<^sub>s\<^sub>t_c {} \ \'" shows "(\,to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \)) \\<^sup>\\<^sup>* (\',to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \'))" "sem\<^sub>e\<^sub>s\<^sub>t_d {} \ (decomp_rm\<^sub>e\<^sub>s\<^sub>t \')" proof - show "(\,to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \)) \\<^sup>\\<^sup>* (\',to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \'))" using assms(1) proof (induction rule: rtranclp_induct2) case (step \1 \1 \2 \2) show ?case using step.hyps(2,1) step.IH proof (induction rule: pts_symbolic_c_induct) case Nil thus ?case using pts_symbolic.Nil[OF Nil.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1)"] by simp next case (Send t S) thus ?case using pts_symbolic.Send[OF Send.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1)"] by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append) next case (Receive t S) thus ?case using pts_symbolic.Receive[OF Receive.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1)"] by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append) next case (Equality t t' S) thus ?case using pts_symbolic.Equality[OF Equality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1)"] by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append) next case (Inequality t t' S) thus ?case using pts_symbolic.Inequality[OF Inequality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \1)"] by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append) next case (Decompose t) thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by simp qed qed simp qed (rule sem\<^sub>e\<^sub>s\<^sub>t_d_decomp_rm\<^sub>e\<^sub>s\<^sub>t_if_sem\<^sub>e\<^sub>s\<^sub>t_c[OF assms(2)]) lemma pts_symbolic_to_pts_symbolic_c_from_initial: assumes "(\\<^sub>0,[]) \\<^sup>\\<^sup>* (\,\)" "\ \ \\\" "wf\<^sub>s\<^sub>t\<^sub>s' \\<^sub>0 []" and "Ana_invar_subst (\(ik\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \\<^sub>0) \ \(eqs_rhs\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \\<^sub>0))" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" shows "\\\<^sub>d. \ = to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \\<^sub>d) \ (\\<^sub>0,[]) \\<^sup>\\<^sub>c\<^sup>* (\,\\<^sub>d) \ (\ \\<^sub>c \to_st \\<^sub>d\)" using assms pts_symbolic_to_pts_symbolic_c[of \\<^sub>0 "[]" \ \ \] sem\<^sub>e\<^sub>s\<^sub>t_c_eq_sem_st[of "{}" \] sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \] to_st_to_est_inv[of \] by auto lemma pts_symbolic_c_to_pts_symbolic_from_initial: assumes "(\\<^sub>0,[]) \\<^sup>\\<^sub>c\<^sup>* (\,\)" "\ \\<^sub>c \to_st \\" shows "(\\<^sub>0,[]) \\<^sup>\\<^sup>* (\,to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \))" "\ \ \to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \)\" using assms pts_symbolic_c_to_pts_symbolic[of \\<^sub>0 "[]" \ \ \] sem\<^sub>e\<^sub>s\<^sub>t_c_eq_sem_st[of "{}" \] sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \] by auto lemma to_st_trms_wf: assumes "\t \ trms\<^sub>e\<^sub>s\<^sub>t A. wf\<^sub>t\<^sub>r\<^sub>m t" shows "\t \ trms\<^sub>s\<^sub>t (to_st A). wf\<^sub>t\<^sub>r\<^sub>m t" using assms proof (induction A) case (Cons x A) hence IH: "\t \ trms\<^sub>s\<^sub>t (to_st A). wf\<^sub>t\<^sub>r\<^sub>m t" by auto with Cons show ?case proof (cases x) case (Decomp t) hence "wf\<^sub>t\<^sub>r\<^sub>m t" using Cons.prems by auto obtain K T where Ana_t: "Ana t = (K,T)" by moura hence "trms\<^sub>s\<^sub>t (decomp t) \ {t} \ K \ T" using decomp_set_unfold[OF Ana_t] by force moreover have "\t \ T. wf\<^sub>t\<^sub>r\<^sub>m t" using Ana_subterm[OF Ana_t] \wf\<^sub>t\<^sub>r\<^sub>m t\ wf_trm_subterm by auto ultimately have "\t \ trms\<^sub>s\<^sub>t (decomp t). wf\<^sub>t\<^sub>r\<^sub>m t" using Ana_keys_wf'[OF Ana_t] \wf\<^sub>t\<^sub>r\<^sub>m t\ by auto thus ?thesis using IH Decomp by auto qed auto qed simp lemma to_st_trms_SMP_subset: "trms\<^sub>s\<^sub>t (to_st A) \ SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A)" proof fix t assume "t \ trms\<^sub>s\<^sub>t (to_st A)" thus "t \ SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A)" proof (induction A) case Nil thus ?case by auto next case (Cons x A) hence *: "t \ trms\<^sub>s\<^sub>t (to_st [x]) \ trms\<^sub>s\<^sub>t (to_st A)" using to_st_append[of "[x]" A] by auto have **: "trms\<^sub>s\<^sub>t (to_st A) \ trms\<^sub>s\<^sub>t (to_st (x#A))" "trms\<^sub>e\<^sub>s\<^sub>t A \ trms\<^sub>e\<^sub>s\<^sub>t (x#A)" using to_st_append[of "[x]" A] by auto show ?case proof (cases "t \ trms\<^sub>s\<^sub>t (to_st A)") case True thus ?thesis using Cons.IH SMP_mono[OF **(2)] by auto next case False hence ***: "t \ trms\<^sub>s\<^sub>t (to_st [x])" using * by auto thus ?thesis proof (cases x) case (Decomp t') hence ****: "t \ trms\<^sub>s\<^sub>t (decomp t')" "t' \ trms\<^sub>e\<^sub>s\<^sub>t (x#A)" using *** by auto obtain K T where Ana_t': "Ana t' = (K,T)" by moura hence "t \ {t'} \ K \ T" using decomp_set_unfold[OF Ana_t'] ****(1) by force moreover { assume "t = t'" hence ?thesis using SMP\<^sub>s\<^sub>t.MP[OF ****(2)] by simp } moreover { assume "t \ K" hence ?thesis using SMP\<^sub>s\<^sub>t.Ana[OF SMP\<^sub>s\<^sub>t.MP[OF ****(2)] Ana_t'] by auto } moreover { assume "t \ T" "t \ t'" hence "t \ t'" using Ana_subterm[OF Ana_t'] by blast hence ?thesis using SMP\<^sub>s\<^sub>t.Subterm[OF SMP\<^sub>s\<^sub>t.MP[OF ****(2)]] by auto } ultimately show ?thesis using Decomp by auto qed auto qed qed qed lemma to_st_trms_tfr: assumes "tfr\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A)" shows "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (to_st A))" proof - have *: "\t \ trms\<^sub>s\<^sub>t (to_st A). wf\<^sub>t\<^sub>r\<^sub>m t" "trms\<^sub>s\<^sub>t (to_st A) \ SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A)" using to_st_trms_wf to_st_trms_SMP_subset assms by auto have "trms\<^sub>s\<^sub>t (to_st A) = trms\<^sub>s\<^sub>t (to_st A) \ trms\<^sub>e\<^sub>s\<^sub>t A" by (blast dest: trm\<^sub>e\<^sub>s\<^sub>t\<^sub>pD) hence "SMP\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (to_st A))" using SMP_subset_union_eq[OF *(2)] by auto thus ?thesis using * assms by presburger qed theorem wt_attack_if_tfr_attack_pts: assumes "wf\<^sub>s\<^sub>t\<^sub>s \\<^sub>0" "tfr\<^sub>s\<^sub>t (\(trms\<^sub>s\<^sub>t ` \\<^sub>0))" "\S \ \\<^sub>0. eqs_tfr\<^sub>s\<^sub>t S" and "Ana_invar_subst (\(ik\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \\<^sub>0) \ \(eqs_rhs\<^sub>s\<^sub>t ` dual\<^sub>s\<^sub>t ` \\<^sub>0))" and "(\\<^sub>0,[]) \\<^sup>\\<^sup>* (\,\)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ \ \\, Var\" shows "\\\<^sub>\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ (\\<^sub>\ \ \\, Var\) \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\\<^sub>\ x))" proof - have "(\(trms\<^sub>s\<^sub>t ` \\<^sub>0)) \ (trms\<^sub>e\<^sub>s\<^sub>t []) = \(trms\<^sub>s\<^sub>t ` \\<^sub>0)" "to_st [] = []" "eqs_tfr\<^sub>s\<^sub>t []" using assms by simp_all hence *: "tfr\<^sub>s\<^sub>t ((\(trms\<^sub>s\<^sub>t ` \\<^sub>0)) \ (trms\<^sub>e\<^sub>s\<^sub>t []))" "wf\<^sub>s\<^sub>t\<^sub>s' \\<^sub>0 []" "\S\\\<^sub>0 \ {to_st []}. eqs_tfr\<^sub>s\<^sub>t S" using assms wf\<^sub>s\<^sub>t\<^sub>s_wf\<^sub>s\<^sub>t\<^sub>s' by (metis, metis, simp) obtain \\<^sub>d where \\<^sub>d: "\ = to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)" "(\\<^sub>0,[]) \\<^sup>\\<^sub>c\<^sup>* (\,\\<^sub>d)" "\ \\<^sub>c \to_st \\<^sub>d\" using pts_symbolic_to_pts_symbolic_c_from_initial assms *(2) by metis hence "tfr\<^sub>s\<^sub>t (\(trms\<^sub>s\<^sub>t ` \) \ (trms\<^sub>e\<^sub>s\<^sub>t \\<^sub>d))" using pts_symbolic_c_preserves_tfr[OF _ *(1)] unfolding trms\<^sub>e\<^sub>s\<^sub>t_def by blast hence "tfr\<^sub>s\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \\<^sub>d)" by (metis DiffE DiffI SMP_append' UnCI) hence "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (to_st \\<^sub>d))" using to_st_trms_tfr by metis moreover have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r (to_st \\<^sub>d) Var" proof - have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" "\v. wf\<^sub>t\<^sub>r\<^sub>m (Var v)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var \ vars\<^sub>e\<^sub>s\<^sub>t \\<^sub>d = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var \ bvars\<^sub>e\<^sub>s\<^sub>t \\<^sub>d = {}" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp_all moreover have "wf\<^sub>e\<^sub>s\<^sub>t {} \\<^sub>d" using pts_symbolic_c_preserves_wf_is[OF \\<^sub>d(2) *(2), of "{}"] by auto moreover have "FV\<^sub>s\<^sub>t (to_st \\<^sub>d) \ bvars\<^sub>e\<^sub>s\<^sub>t \\<^sub>d = {}" using pts_symbolic_c_preserves_constr_disj_vars[OF \\<^sub>d(2)] assms(1) wf\<^sub>s\<^sub>t\<^sub>s_wf\<^sub>s\<^sub>t\<^sub>s' by simp ultimately show ?thesis by simp qed moreover have "eqs_tfr\<^sub>s\<^sub>t (to_st \\<^sub>d)" using pts_symbolic_c_preserves_eqs_tfr[OF \\<^sub>d(2) *(3)] by blast moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" "\v. wf\<^sub>t\<^sub>r\<^sub>m (Var v)" by simp_all ultimately obtain \\<^sub>\ where \\<^sub>\: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\" "\\<^sub>\ \\<^sub>c \to_st \\<^sub>d, Var\" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\" "\x. wf\<^sub>t\<^sub>r\<^sub>m (\\<^sub>\ x)" using wt_attack_if_tfr_attack[OF assms(6) \\<^sub>d(3) _ _ \tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (to_st \\<^sub>d))\ \eqs_tfr\<^sub>s\<^sub>t (to_st \\<^sub>d)\] by metis hence "\\<^sub>\ \ \\, Var\" using pts_symbolic_c_to_pts_symbolic_from_initial \\<^sub>d by metis thus ?thesis using \\<^sub>\(1,3,4) by metis qed subsubsection {* The typing result stated without referencing transition systems *} lemma dual\<^sub>s\<^sub>t_FV: "FV\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t A) = FV\<^sub>s\<^sub>t A" by (induct A rule: dual\<^sub>s\<^sub>t.induct) auto lemma dual\<^sub>s\<^sub>t_bvars: "bvars\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t A) = bvars\<^sub>s\<^sub>t A" by (induct A rule: dual\<^sub>s\<^sub>t.induct) auto corollary wt_attack_if_tfr_attack_d: assumes "wf\<^sub>s\<^sub>t {} \" "FV\<^sub>s\<^sub>t \ \ bvars\<^sub>s\<^sub>t \ = {}" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t \)" "eqs_tfr\<^sub>s\<^sub>t \" and "Ana_invar_subst (ik\<^sub>s\<^sub>t \ \ eqs_rhs\<^sub>s\<^sub>t \)" and "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" "\ \ \\\" shows "\\\<^sub>\. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ (\\<^sub>\ \ \\\) \ wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>\ \ (\x. wf\<^sub>t\<^sub>r\<^sub>m (\\<^sub>\ x))" proof - { fix S A have "({S},A) \\<^sup>\\<^sup>* ({},A@dual\<^sub>s\<^sub>t S)" proof (induction S arbitrary: A) case Nil thus ?case using pts_symbolic.Nil[of "{[]}"] by auto next case (Cons x S) hence "({S}, A@dual\<^sub>s\<^sub>t [x]) \\<^sup>\\<^sup>* ({}, A@dual\<^sub>s\<^sub>t (x#S))" by (metis dual\<^sub>s\<^sub>t_append List.append_assoc List.append_Nil List.append_Cons) moreover have "({x#S}, A) \\<^sup>\ ({S}, A@dual\<^sub>s\<^sub>t [x])" using pts_symbolic.Send[of _ S "{x#S}"] pts_symbolic.Receive[of _ S "{x#S}"] pts_symbolic.Equality[of _ _ S "{x#S}"] pts_symbolic.Inequality[of _ _ _ S "{x#S}"] by (cases x) auto ultimately show ?case by simp qed } hence *: "({dual\<^sub>s\<^sub>t \},[]) \\<^sup>\\<^sup>* ({},\)" using dual\<^sub>s\<^sub>t_self_inverse by (metis List.append_Nil) have "\A. A \ {dual\<^sub>s\<^sub>t \} \ A = dual\<^sub>s\<^sub>t \" by simp have "FV\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \) = {}" using assms(2) dual\<^sub>s\<^sub>t_FV dual\<^sub>s\<^sub>t_bvars by metis+ hence "wf\<^sub>s\<^sub>t\<^sub>s {dual\<^sub>s\<^sub>t \}" using assms(1,2) dual\<^sub>s\<^sub>t_self_inverse[of \] unfolding wf\<^sub>s\<^sub>t\<^sub>s_def by auto moreover have "\(trms\<^sub>s\<^sub>t ` {\}) = trms\<^sub>s\<^sub>t \" "\(trms\<^sub>s\<^sub>t ` {dual\<^sub>s\<^sub>t \}) = trms\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \)" by auto hence "tfr\<^sub>s\<^sub>t (\(trms\<^sub>s\<^sub>t ` {\}))" "(\(trms\<^sub>s\<^sub>t ` {\})) = \(trms\<^sub>s\<^sub>t ` {dual\<^sub>s\<^sub>t \})" by (metis assms(3), metis dual\<^sub>s\<^sub>t_trms_eq) hence "tfr\<^sub>s\<^sub>t (\(trms\<^sub>s\<^sub>t ` {dual\<^sub>s\<^sub>t \}))" by metis moreover have "\S \ {dual\<^sub>s\<^sub>t \}. eqs_tfr\<^sub>s\<^sub>t S" using dual\<^sub>s\<^sub>t_eqs_tfr[OF assms(4)] by blast moreover have "Ana_invar_subst (\(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`{dual\<^sub>s\<^sub>t \}) \ \(eqs_rhs\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`{dual\<^sub>s\<^sub>t \}))" using assms(5) dual\<^sub>s\<^sub>t_self_inverse[of \] by auto ultimately show ?thesis using wt_attack_if_tfr_attack_pts[OF _ _ _ _ * assms(6,7)] by blast qed end end