subsection \<open>The Typing Result for the Composition-Only Intruder\<close>
context typed_model
begin
subsubsection \<open>Well-typedness and Type-Flaw Resistance Preservation\<close>
context
begin
private lemma LI_preserves_tfr_stp_all_single:
assumes "(S,\<theta>) \<leadsto> (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
and "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t S)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t S)"
shows "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'"
using assms
proof (induction rule: LI_rel.induct)
case (Compose S X f S' \<theta>)
hence "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'" by simp_all
moreover have "list_all tfr\<^sub>s\<^sub>t\<^sub>p (map Send X)" by (induct X) auto
ultimately show ?case by simp
next
case (Unify S f Y \<delta> X S' \<theta>)
hence "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S')" by simp
have "fv\<^sub>s\<^sub>t (S@Send (Fun f X)#S') \<inter> bvars\<^sub>s\<^sub>t (S@S') = {}"
using Unify.prems(1) by (auto simp add: wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def)
moreover have "fv (Fun f X) \<subseteq> fv\<^sub>s\<^sub>t (S@Send (Fun f X)#S')" by auto
moreover have "fv (Fun f Y) \<subseteq> fv\<^sub>s\<^sub>t (S@Send (Fun f X)#S')"
using Unify.hyps(2) fv_subset_if_in_strand_ik'[of "Fun f Y" S] by force
ultimately have bvars_disj:
"bvars\<^sub>s\<^sub>t (S@S') \<inter> fv (Fun f X) = {}" "bvars\<^sub>s\<^sub>t (S@S') \<inter> fv (Fun f Y) = {}"
by blast+
have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(5) by simp
moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)"
proof -
obtain x where "x \<in> set S" "Fun f Y \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t\<^sub>p x)"
using Unify.hyps(2) Unify.prems(5) by force+
thus ?thesis using wf_trm_subterm by auto
qed
moreover have
"Fun f X \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))" "Fun f Y \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))"
using SMP_append[of S "Send (Fun f X)#S'"] SMP_Cons[of "Send (Fun f X)" S']
SMP_ikI[OF Unify.hyps(2)]
by auto
hence "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
moreover have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
using mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>]
by (metis wf_trm_subst_range_iff)
moreover have "bvars\<^sub>s\<^sub>t (S@S') \<inter> range_vars \<delta> = {}"
using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] bvars_disj by fast
ultimately show ?case using tfr_stp_all_wt_subst_apply[OF \<open>list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S')\<close>] by metis
next
case (Equality S \<delta> t t' a S' \<theta>)
have "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S')" "\<Gamma> t = \<Gamma> t'"
hence "SMP (trms\<^sub>s\<^sub>t [Send (Fun f X)]) \<subseteq> SMP M"
proof -
have "SMP (trms\<^sub>s\<^sub>t [Send (Fun f X)]) \<subseteq> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))"
using trms\<^sub>s\<^sub>t_append SMP_mono by auto
thus ?thesis
using SMP_union[of "trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S')" M]
SMP_subset_union_eq[OF Compose.prems(6)]
by auto
qed
thus ?case using Compose.prems(6) by auto
next
case (Unify S f Y \<delta> X S' \<theta>)
have "Fun f X \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))" by auto
moreover have "MGU \<delta> (Fun f X) (Fun f Y)"
by (metis mgu_gives_MGU[OF Unify.hyps(3)[symmetric]])
moreover have
"\<And>x. x \<in> set S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)"
using Unify.prems(4) by force+
moreover have "Fun f Y \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))"
by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1))
ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
using ik\<^sub>s\<^sub>t_subterm_exD[OF \<open>Fun f Y \<in> ik\<^sub>s\<^sub>t S\<close>] \<open>tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))\<close>
unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by (metis (full_types) SMP_wf_trm Unify.prems(4), blast)
hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close>])
moreover have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
using mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>] by simp
ultimately have "trms\<^sub>s\<^sub>t ((S@Send (Fun f X)#S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP M"
using SMP.Substitution Unify.prems(6) wt_subst_SMP_subset by metis
thus ?case by auto
next
case (Equality S \<delta> t t' a S' \<theta>)
hence "\<Gamma> t = \<Gamma> t'"
using tfr_stp_all_same_type MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
by metis
moreover have "t \<in> SMP (trms\<^sub>s\<^sub>t (S@Equality a t t'#S'))" "t' \<in> SMP (trms\<^sub>s\<^sub>t (S@Equality a t t'#S'))"
using Equality.prems(1) by auto
moreover have "MGU \<delta> t t'" using mgu_gives_MGU[OF Equality.hyps(2)[symmetric]] by metis
moreover have "\<And>x. x \<in> set S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'"
using Equality.prems(4) by force+
ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>])
moreover have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
using mgu_wf_trm[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m t'\<close>] by simp
ultimately have "trms\<^sub>s\<^sub>t ((S@Equality a t t'#S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP M"
using SMP.Substitution Equality.prems wt_subst_SMP_subset by metis
have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(5) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by simp
moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)"
proof -
obtain x where "x \<in> set S" "Fun f Y \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t\<^sub>p x)"
using Unify.hyps(2) Unify.prems(5) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by force
thus ?thesis using wf_trm_subterm by auto
qed
moreover have
"Fun f X \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))" "Fun f Y \<in> SMP (trms\<^sub>s\<^sub>t (S@Send (Fun f X)#S'))"
using SMP_append[of S "Send (Fun f X)#S'"] SMP_Cons[of "Send (Fun f X)" S']
SMP_ikI[OF Unify.hyps(2)]
by auto
hence "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>]
show ?thesis using pgwt_wellformed interpretation_grounds[OF \<theta>(1)] \<theta>(2,3) by blast
qed
private fun fresh_pgwt::"'fun set \<Rightarrow> ('fun,'atom) term_type \<Rightarrow> ('fun,'var) term" where
"fresh_pgwt S (TAtom a) =
Fun (SOME c. c \<notin> S \<and> \<Gamma> (Fun c []) = TAtom a \<and> public c) []"
| "fresh_pgwt S (TComp f T) = Fun f (map (fresh_pgwt S) T)"
private lemma fresh_pgwt_same_type:
assumes "finite S" "wf\<^sub>t\<^sub>r\<^sub>m t"
shows "\<Gamma> (fresh_pgwt S (\<Gamma> t)) = \<Gamma> t"
proof -
let ?P = "\<lambda>\<tau>::('fun,'atom) term_type. wf\<^sub>t\<^sub>r\<^sub>m \<tau> \<and> (\<forall>f T. TComp f T \<sqsubseteq> \<tau> \<longrightarrow> 0 < arity f)"
hence "\<exists>c. ?P c" using not_finite_existsD by blast
thus ?case using someI_ex[of ?P] by auto
next
case (Fun f T)
have f: "0 < arity f" using Fun.prems fun_type_inv by auto
have "\<And>t. t \<in> set T \<Longrightarrow> ?P t"
using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
by metis
hence "\<And>t. t \<in> set T \<Longrightarrow> \<Gamma> (fresh_pgwt S t) = t" using Fun.prems Fun.IH by auto
hence "map \<Gamma> (map (fresh_pgwt S) T) = T" by (induct T) auto
thus ?case using fun_type[OF f] by simp
qed
} thus ?thesis using assms(1) \<Gamma>_wf'[OF assms(2)] \<Gamma>_wf(1) by auto
qed
private lemma fresh_pgwt_empty_synth:
assumes "finite S" "wf\<^sub>t\<^sub>r\<^sub>m t"
shows "{} \<turnstile>\<^sub>c fresh_pgwt S (\<Gamma> t)"
proof -
let ?P = "\<lambda>\<tau>::('fun,'atom) term_type. wf\<^sub>t\<^sub>r\<^sub>m \<tau> \<and> (\<forall>f T. TComp f T \<sqsubseteq> \<tau> \<longrightarrow> 0 < arity f)"
using Fun.prems fun_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
have "\<And>t. t \<in> set T \<Longrightarrow> ?P t"
using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
by metis
hence "\<And>t. t \<in> set T \<Longrightarrow> {} \<turnstile>\<^sub>c fresh_pgwt S t" using Fun.prems Fun.IH by auto
moreover have "length (map (fresh_pgwt S) T) = arity f" using f(2) by auto
ultimately show ?case using intruder_synth.ComposeC[of "map (fresh_pgwt S) T" f] f by auto
qed
} thus ?thesis using assms(1) \<Gamma>_wf'[OF assms(2)] \<Gamma>_wf(1) by auto
qed
private lemma fresh_pgwt_has_fresh_const:
assumes "finite S" "wf\<^sub>t\<^sub>r\<^sub>m t"
obtains c where "Fun c [] \<sqsubseteq> fresh_pgwt S (\<Gamma> t)" "c \<notin> S"
proof -
let ?P = "\<lambda>\<tau>::('fun,'atom) term_type. wf\<^sub>t\<^sub>r\<^sub>m \<tau> \<and> (\<forall>f T. TComp f T \<sqsubseteq> \<tau> \<longrightarrow> 0 < arity f)"
{ fix \<tau> assume "?P \<tau>" hence "\<exists>c. Fun c [] \<sqsubseteq> fresh_pgwt S \<tau> \<and> c \<notin> S"
proof (induction \<tau>)
case (Var a)
let ?P = "\<lambda>c. c \<notin> S \<and> \<Gamma> (Fun c []) = Var a \<and> public c"
let ?Q = "\<lambda>c. \<Gamma> (Fun c []) = Var a \<and> public c"
shows "s \<notin> subterms (fresh_pgwt S (\<Gamma> t))"
proof -
let ?P = "\<lambda>\<tau>::('fun,'atom) term_type. wf\<^sub>t\<^sub>r\<^sub>m \<tau> \<and> (\<forall>f T. TComp f T \<sqsubseteq> \<tau> \<longrightarrow> 0 < arity f)"
"\<forall>s \<in> subst_range \<sigma>. \<forall>u \<in> subst_range \<sigma>. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u"
} thus ?thesis using \<sigma>(3) \<theta> \<theta>_img by auto
qed
moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using \<theta> t(1) \<sigma>(5) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
moreover have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
using \<theta> \<sigma>(6) t(2) pgwt_is_empty_synth pgwt_wellformed
moreover have "\<forall>s\<in>subst_range \<theta>. \<forall>u\<in>subst_range \<theta>. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u"
using \<sigma>(4) \<theta>_img t(3) by (auto simp del: subst_range.simps)
hence "y \<noteq> x" "z \<noteq> x" using x_dom by auto
hence "\<theta> y = \<sigma> y" "\<theta> z = \<sigma> z" using \<theta> by auto
thus ?thesis using \<open>\<theta> y = \<theta> z\<close> \<sigma>(2) ** unfolding bij_betw_def inj_on_def by auto
qed (metis \<theta> * \<open>\<theta> y = \<theta> z\<close> \<theta>_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
}
thus "(\<theta> y = \<theta> z) = (y = z)" by auto
next
fix y assume "y \<in> subst_domain \<theta>" thus "\<theta> y \<in> subst_range \<theta>" by auto
next
fix t assume "t \<in> subst_range \<theta>" thus "\<exists>z \<in> subst_domain \<theta>. t = \<theta> z" by auto
qed
moreover have "subst_range \<theta> \<subseteq> (\<lambda>c. Fun c []) ` \<C>\<^sub>p\<^sub>u\<^sub>b - T"
using \<sigma>(3) \<delta>(3) \<theta> by (auto simp add: subst_domain_def)
moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using \<sigma>(4) \<delta>(4) \<theta> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
moreover have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
using \<theta> \<sigma>(5) \<delta>(5) wf_trm_subst_range_iff[of \<delta>]
and \<I>': "\<forall>X F. Inequality X F \<in> set S \<longrightarrow> ineq_model \<I>' X F"
"ground (subst_range \<I>')"
"subst_domain \<I>' = {x \<in> vars\<^sub>s\<^sub>t S. \<exists>X F. Inequality X F \<in> set S \<and> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X}"
and tfr_stp_all: "list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
from \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> have "wf\<^sub>s\<^sub>t {} S" "subst_idem \<theta>" and S_\<theta>_disj: "\<forall>v \<in> vars\<^sub>s\<^sub>t S. \<theta> v = Var v"
using subst_idemI[of \<theta>] unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
where \<I>: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "subst_range \<I> \<subseteq> public_ground_wf_terms"
using wt_interpretation_exists by blast
hence \<I>_deduct: "\<And>x M. M \<turnstile>\<^sub>c \<I> x" and \<I>_wf_trm: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)"
using pgwt_deducible pgwt_wellformed by fastforce+
let ?P = "\<lambda>\<delta> X. subst_domain \<delta> = set X \<and> ground (subst_range \<delta>)"
let ?Sineqsvars = "{x \<in> vars\<^sub>s\<^sub>t S. \<exists>X F. Inequality X F \<in> set S \<and> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<and> x \<notin> set X}"
let ?Strms = "subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t S)"
have finite_vars: "finite ?Sineqsvars" "finite ?Strms" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s ?Strms"
using wf_trm_subtermeq assms(5) by fastforce+
define Q1 where "Q1 = (\<lambda>(F::(('fun,'var) term \<times> ('fun,'var) term) list) X.
\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>a. \<Gamma> (Var x) = TAtom a)"
define Q2 where "Q2 = (\<lambda>(F::(('fun,'var) term \<times> ('fun,'var) term) list) X.
\<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X))"
define Q1' where "Q1' = (\<lambda>(t::('fun,'var) term) (t'::('fun,'var) term) X.
\<forall>x \<in> (fv t \<union> fv t') - set X. \<exists>a. \<Gamma> (Var x) = TAtom a)"
define Q2' where "Q2' = (\<lambda>(t::('fun,'var) term) (t'::('fun,'var) term) X.
\<forall>f T. Fun f T \<in> subterms t \<union> subterms t' \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X))"
have ex_P: "\<forall>X. \<exists>\<delta>. ?P \<delta> X" using interpretation_subst_exists' by blast
have tfr_ineq: "\<forall>X F. Inequality X F \<in> set S \<longrightarrow> Q1 F X \<or> Q2 F X"
using tfr_stp_all Q1_def Q2_def tfr\<^sub>s\<^sub>t\<^sub>p_list_all_alt_def[of S] by blast
have S_fv_bvars_disj: "fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}" using \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by metis
hence ineqs_vars_not_bound: "\<forall>X F x. Inequality X F \<in> set S \<longrightarrow> x \<in> ?Sineqsvars \<longrightarrow> x \<notin> set X"
using strand_fv_bvars_disjoint_unfold by blast
have \<theta>_vars_S_bvars_disj: "(subst_domain \<theta> \<union> range_vars \<theta>) \<inter> set X = {}"
when "Inequality X F \<in> set S" for F X
using wf_constr_bvars_disj[OF \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close>]
have \<sigma>_img_subterms: "\<forall>s \<in> subst_range \<sigma>. \<forall>u \<in> subst_range \<sigma>. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u"
by (metis \<sigma>_subterm_inj subterm_inj_on_alt_def')
have "subst_range \<sigma> \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>)" by auto
using \<sigma>_fresh_pub_img pgwt_is_empty_synth by blast+
have \<sigma>_img_ground: "ground (subst_range \<sigma>)"
using \<sigma>_pgwt_img pgwt_ground by auto
hence \<sigma>_inj: "inj \<sigma>"
using \<sigma>_bij_dom_img subst_inj_is_bij_betw_dom_img_if_ground_img by auto
have \<sigma>_ineqs_fv_dom: "\<And>X F. Inequality X F \<in> set S \<Longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> subst_domain \<sigma>"
using \<sigma>_fv_dom by fastforce
have \<sigma>_dom_bvars_disj: "\<forall>X F. Inequality X F \<in> set S \<longrightarrow> subst_domain \<sigma> \<inter> set X = {}"
using ineqs_vars_not_bound \<sigma>_fv_dom by fastforce
have \<I>'1: "\<forall>X F \<delta>. Inequality X F \<in> set S \<longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> subst_domain \<I>'"
have doms_eq: "subst_domain \<I>' = subst_domain \<sigma>" using \<I>'(3) \<sigma>_fv_dom by simp
have \<sigma>_ineqs_neq: "ineq_model \<sigma> X F" when "Inequality X F \<in> set S" for X F
proof -
obtain a::"'fun" where a: "a \<notin> \<Union>(funs_term ` subterms\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>))"
using exists_fun_notin_funs_terms[OF subterms_union_finite[OF \<sigma>_finite_img]]
by moura
hence a': "\<And>T. Fun a T \<notin> subterms\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>)"
"\<And>S. Fun a [] \<in> set (Fun a []#S)" "Fun a [] \<notin> Var ` set X"
by (meson a UN_I term.set_intros(1), auto)
define t where "t \<equiv> Fun a (Fun a []#map fst F)"
define t' where "t' \<equiv> Fun a (Fun a []#map snd F)"
note F_in = that
have t_fv: "fv t \<union> fv t' \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
unfolding t_def t'_def by force
have t_subterms: "subterms t \<union> subterms t' \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<union> {t, t', Fun a []}"
unfolding t_def t'_def by force
have "t \<cdot> \<delta> \<cdot> \<sigma> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma>" when "?P \<delta> X" for \<delta>
proof -
have tfr_assms: "Q1 F X \<or> Q2 F X" using tfr_ineq F_in by metis
using g that(2) by (simp_all add: subst_fv_unfold_ground_img range_vars_alt_def)
moreover have "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) \<subseteq> subst_domain \<sigma>" using Cons by auto
ultimately show ?case using Cons.prems that(2) by auto
qed (simp add: subst_apply_pairs_def)
have \<sigma>_ineqs_ground: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ((F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<sigma>) = {}"
when "Inequality X F \<in> set S" and "?P \<delta> X" for F \<delta> X
using \<sigma>_ineqs_fv_dom'[OF that]
proof (induction F)
case (Cons g G)
obtain t t' where g: "g = (t,t')" by (metis surj_pair)
have "ineq_model (\<sigma> \<circ>\<^sub>s \<I>) X F"
proof -
have "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) \<subseteq> subst_domain \<sigma>" when "?P \<delta> X" for \<delta>
using ConsIneq.prems(3)[OF _ that] by simp
hence "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> subst_domain \<sigma>"
using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_subset ex_P
by (metis Diff_subset_conv Un_commute)
thus ?thesis by (metis ineq_model_ground_subst[OF _ \<sigma>_img_ground **])
qed
hence "ineq_model (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>) X F"
using * ineq_model_subst' subst_compose_assoc ConsIneq.prems(4)
by (metis UnCI list.set_intros(1) set_append)
thus ?case using IH by (auto simp add: ineq_model_def)
using LI_preserves_welltypedness[OF *(2) assms(3,4,7) tfr]
LI_preserves_wellformedness[OF *(2) assms(3)]
LI_preserves_tfr[OF *(2) assms(3,4,7) tfr]
by metis+
define A where "A \<equiv> {x \<in> vars\<^sub>s\<^sub>t S'. \<exists>X F. Inequality X F \<in> set S' \<and> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<and> x \<notin> set X}"
define B where "B \<equiv> UNIV - A"
let ?\<I> = "rm_vars B \<I>"
have gr\<I>: "ground (subst_range \<I>)" "ground (subst_range ?\<I>)"
using assms(1) rm_vars_img_subset[of B \<I>] by (auto simp add: subst_domain_def)
{ fix X F
assume "Inequality X F \<in> set S'"
hence *: "ineq_model \<I> X F"
using strand_sem_c_imp_ineq_model[OF *(3)]
by (auto simp del: subst_range.simps)
hence "ineq_model ?\<I> X F"
proof -
{ fix \<delta>
assume 1: "subst_domain \<delta> = set X" "ground (subst_range \<delta>)"
and 2: "list_ex (\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> snd f \<cdot> \<delta> \<circ>\<^sub>s \<I>) F"
have "list_ex (\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s rm_vars B \<I> \<noteq> snd f \<cdot> \<delta> \<circ>\<^sub>s rm_vars B \<I>) F" using 2
proof (induction F)
case (Cons g G)
obtain t t' where g: "g = (t,t')" by (metis surj_pair)
thus ?case
using Cons Unifier_ground_rm_vars[OF gr\<I>(1), of "t \<cdot> \<delta>" B "t' \<cdot> \<delta>"]
by auto
qed simp
} thus ?thesis using * unfolding ineq_model_def by simp
qed
} moreover have "subst_domain \<I> = UNIV" using assms(1) by metis
hence "subst_domain ?\<I> = A" using rm_vars_dom[of B \<I>] B_def by blast
using wt_attack_if_tfr_attack[OF _ _ assms(2,3,4,5,6)] assms(1) by metis
end
subsection \<open>Lifting the Composition-Only Typing Result to the Full Intruder Model\<close>
context typed_model
begin
subsubsection \<open>Analysis Invariance\<close>
definition (in typed_model) Ana_invar_subst where
"Ana_invar_subst \<M> \<equiv>
(\<forall>f T K M \<delta>. Fun f T \<in> (subterms\<^sub>s\<^sub>e\<^sub>t \<M>) \<longrightarrow>
Ana (Fun f T) = (K, M) \<longrightarrow> Ana (Fun f T \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>))"
lemma (in typed_model) Ana_invar_subst_subset:
assumes "Ana_invar_subst M" "N \<subseteq> M"
shows "Ana_invar_subst N"
using assms unfolding Ana_invar_subst_def by blast
lemma (in typed_model) Ana_invar_substD:
assumes "Ana_invar_subst \<M>"
and "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t \<M>" "Ana (Fun f T) = (K, M)"
shows "Ana (Fun f T \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)"
private abbreviation trms\<^sub>e\<^sub>s\<^sub>t where "trms\<^sub>e\<^sub>s\<^sub>t S \<equiv> \<Union>(trms\<^sub>e\<^sub>s\<^sub>t\<^sub>p ` set S)"
| Decomp: "\<lbrakk>\<D> \<in> decomps\<^sub>e\<^sub>s\<^sub>t \<M> \<N> \<I>; Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<M> \<union> \<N>);
Ana (Fun f T) = (K,M); M \<noteq> [];
(\<M> \<union> ik\<^sub>e\<^sub>s\<^sub>t \<D>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c Fun f T \<cdot> \<I>;
\<And>k. k \<in> set K \<Longrightarrow> (\<M> \<union> ik\<^sub>e\<^sub>s\<^sub>t \<D>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>\<rbrakk>
\<Longrightarrow> \<D>@[Decomp (Fun f T)] \<in> decomps\<^sub>e\<^sub>s\<^sub>t \<M> \<N> \<I>"
private fun decomp_rm\<^sub>e\<^sub>s\<^sub>t::"('fun,'var) extstrand \<Rightarrow> ('fun,'var) extstrand" where
| Decompose: "sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \<I> S \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t S \<union> M\<^sub>0) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I> \<Longrightarrow> Ana t = (K, M)
\<Longrightarrow> (\<And>k. k \<in> set K \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t S \<union> M\<^sub>0) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k \<cdot> \<I>) \<Longrightarrow> sem\<^sub>e\<^sub>s\<^sub>t_d M\<^sub>0 \<I> (S@[Decomp t])"
| Decompose: "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \<I> S \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t S \<union> M\<^sub>0) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c t \<cdot> \<I> \<Longrightarrow> Ana t = (K, M)
\<Longrightarrow> (\<And>k. k \<in> set K \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t S \<union> M\<^sub>0) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>) \<Longrightarrow> sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \<I> (S@[Decomp t])"
"t \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A \<Longrightarrow> t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t A)"
proof (induction A rule: to_st.induct)
case (2 x S) thus ?case
proof (cases x)
case (Equality ac t t') thus ?thesis using 2 by (cases ac) auto
qed auto
next
case (3 t' A)
obtain K M where Ana: "Ana t' = (K,M)" by (metis surj_pair)
show ?case
using 3 decomp_ik[OF Ana] decomp_assignment_rhs_empty[OF Ana] Ana_subterm[OF Ana]
have "fv\<^sub>e\<^sub>s\<^sub>t (A@[Decomp t]) = fv\<^sub>e\<^sub>s\<^sub>t A \<union> 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 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<subseteq> fv\<^sub>e\<^sub>s\<^sub>t A" by force
moreover have "fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)"
thus ?case using ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f T)]"] using Decomp.IH by auto
qed simp
private lemma decomps\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_empty: "D \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I> \<Longrightarrow> 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)
assumes "A \<in> decomps\<^sub>e\<^sub>s\<^sub>t S N \<I>" "B \<in> decomps\<^sub>e\<^sub>s\<^sub>t S N \<I>"
shows "A@B \<in> decomps\<^sub>e\<^sub>s\<^sub>t S N \<I>"
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 \<union> ik\<^sub>e\<^sub>s\<^sub>t B \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> S \<union> ik\<^sub>e\<^sub>s\<^sub>t (A@B) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" 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)]
assumes "finite M" "M \<subseteq> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>"
shows "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. ik\<^sub>e\<^sub>s\<^sub>t D = (\<Union>m \<in> M. ik\<^sub>e\<^sub>s\<^sub>t m)"
using assms
proof (induction M rule: finite_induct)
case empty
moreover have "[] \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" "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 \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" "ik\<^sub>e\<^sub>s\<^sub>t D = (\<Union>m\<in>M. ik\<^sub>s\<^sub>t (to_st m))" by moura
moreover have "m \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" using insert.prems(1) by blast
ultimately show ?case using decomps\<^sub>e\<^sub>s\<^sub>t_append[of D A N \<I> m] ik\<^sub>e\<^sub>s\<^sub>t_append[of D m] by blast
qed
private lemma decomp_snd_exists[simp]: "\<exists>D. decomp t = send\<langle>t\<rangle>\<^sub>s\<^sub>t#D"
by (metis (mono_tags, lifting) decomp_def prod.case surj_pair)
private lemma decomp_nonnil[simp]: "decomp t \<noteq> []"
using decomp_snd_exists[of t] by fastforce
private lemma to_st_nil_inv[dest]: "to_st A = [] \<Longrightarrow> A = []"
by (induct A rule: to_st.induct) auto
private lemma well_analyzedD:
assumes "well_analyzed A" "Decomp t \<in> set A"
shows "\<exists>f T. t = Fun f T"
using assms
proof (induction A rule: well_analyzed.induct)
case (Decomp A t')
hence "\<exists>f T. t' = Fun f T" by (cases t') auto
moreover have "Decomp t \<in> set A \<or> t = t'" using Decomp by auto
ultimately show ?case using Decomp.IH by auto
qed auto
private lemma well_analyzed_inv:
assumes "well_analyzed (A@[Decomp t])"
shows "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) - (Var ` \<V>)"
using assms well_analyzed.cases[of "A@[Decomp t]"] by fastforce
hence "\<And>k. k \<in> set K \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t \<A> \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k \<cdot> \<I>"
using *
by (metis (full_types) strand_sem_d.simps(2) strand_sem_eq_defs(2) strand_sem_Send_split(2))
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 \<I> \<A> \<Longrightarrow> \<lbrakk>M\<^sub>0; to_st \<A>\<rbrakk>\<^sub>d' \<I>"
have "\<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); decomp t\<rbrakk>\<^sub>d' \<I>"
proof -
have "\<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); [send\<langle>t\<rangle>\<^sub>s\<^sub>t]\<rbrakk>\<^sub>d' \<I>"
using Decompose.hyps(2) by (auto simp add: sup.commute)
moreover have "\<And>k. k \<in> set K \<Longrightarrow> M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k \<cdot> \<I>"
using Decompose by (metis sup.commute)
hence "\<And>k. k \<in> set K \<Longrightarrow> \<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); [Send k]\<rbrakk>\<^sub>d' \<I>" by auto
hence "\<And>k. k \<in> set K \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t \<A> \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>"
using * strand_sem_Send_split(1) strand_sem_eq_defs(1)
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 \<I> \<A> \<Longrightarrow> \<lbrakk>M\<^sub>0; to_st \<A>\<rbrakk>\<^sub>c' \<I>"
have "\<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); decomp t\<rbrakk>\<^sub>c' \<I>"
proof -
have "\<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); [send\<langle>t\<rangle>\<^sub>s\<^sub>t]\<rbrakk>\<^sub>c' \<I>"
using Decompose.hyps(2) by (auto simp add: sup.commute)
moreover have "\<And>k. k \<in> set K \<Longrightarrow> M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>"
using Decompose by (metis sup.commute)
hence "\<And>k. k \<in> set K \<Longrightarrow> \<lbrakk>M\<^sub>0 \<union> ik\<^sub>s\<^sub>t (to_st \<A>); [Send k]\<rbrakk>\<^sub>c' \<I>" by auto
assumes "sem\<^sub>e\<^sub>s\<^sub>t_c M\<^sub>0 \<I> A" "t \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" "t \<notin> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
shows "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t"
using assms
proof (induction M\<^sub>0 \<I> A arbitrary: t rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct)
case (Send M\<^sub>0 \<I> 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 \<I> A t')
hence "t \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" "t \<notin> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
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) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> 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 \<I> 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 \<I> 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 \<I> A t' K M t)
have *: "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t' \<cdot> \<I>" using Decompose.hyps(2)
proof (induction rule: intruder_synth_induct)
case (AxiomC t'')
moreover {
assume "t'' \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" "t'' \<notin> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
hence "ik\<^sub>e\<^sub>s\<^sub>t A \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>" using Decompose.hyps by auto
hence "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k \<cdot> \<I>"
proof (induction rule: intruder_synth_induct)
case (AxiomC t'')
moreover {
assume "t'' \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" "t'' \<notin> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
hence ?case using Decompose.IH by auto
}
ultimately show ?case by force
qed simp
}
hence **: "\<And>k. k \<in> set (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>) \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k" by auto
proof (cases "t \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>")
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 \<in> ik\<^sub>s\<^sub>t (decomp t') \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" using Decompose.prems(1) ik\<^sub>e\<^sub>s\<^sub>t_append by auto
hence ***: "t \<in> set (M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)" using Decompose.hyps(3) decomp_ik by auto
hence "M \<noteq> []" by auto
hence ****: "Ana (t' \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)" 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) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t" by (rule intruder_deduct.Decompose[OF * **** ** ***])
thus ?thesis using ideduct_mono decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto
proof (induction M\<^sub>0 \<I> A rule: sem\<^sub>e\<^sub>s\<^sub>t_c.induct)
case (Send M\<^sub>0 \<I> 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 t) 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 \<I> 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 \<I> 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
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 {} \<I> (A @ D)" "ik\<^sub>e\<^sub>s\<^sub>t (A@D) \<union> {} \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c Fun f T \<cdot> \<I>"
"\<And>k. k \<in> set K \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t (A @ D) \<union> {} \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>"
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
assumes "D \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<I>" "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 "wfrestrictedvars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)"
using decomp_vars fv_subset_subterms[OF Decomp.hyps(2)] by fast
hence "wfrestrictedvars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t A"
using ik\<^sub>s\<^sub>t_assignment_rhs\<^sub>s\<^sub>t_wfrestrictedvars_subset[of "to_st A"] by blast
assumes "D \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile> t" "\<not>(M \<union> (ik\<^sub>e\<^sub>s\<^sub>t D) \<turnstile>\<^sub>c t)"
obtains D' where
"D@D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@D') \<turnstile>\<^sub>c t" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<subset> M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@D')"
proof -
have "\<exists>D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>. M \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<turnstile>\<^sub>c t" using assms(2)
proof (induction t rule: intruder_deduct_induct)
case (Compose X f)
from Compose.IH have "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>. \<forall>x \<in> set X. M \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile>\<^sub>c x"
proof (induction X)
case (Cons t X)
then obtain D' D'' where
D': "D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<turnstile>\<^sub>c t" and
D'': "D'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "\<forall>x \<in> set X. M \<union> ik\<^sub>e\<^sub>s\<^sub>t D'' \<turnstile>\<^sub>c x"
by moura
hence "M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^sub>c t" "\<forall>x \<in> set X. M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^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)
have "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>. \<forall>k \<in> set K. M \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile>\<^sub>c k" using Decompose.IH
proof (induction K)
case (Cons t X)
then obtain D' D'' where
D': "D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<turnstile>\<^sub>c t" and
D'': "D'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "\<forall>x \<in> set X. M \<union> ik\<^sub>e\<^sub>s\<^sub>t D'' \<turnstile>\<^sub>c x"
using assms(1) by moura
hence "M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^sub>c t" "\<forall>x \<in> set X. M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^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' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "\<And>k. k \<in> set K \<Longrightarrow> M \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<turnstile>\<^sub>c k" by metis
obtain D'' where D'': "D'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D'' \<turnstile>\<^sub>c t" by (metis Decompose.IH(1))
obtain f X where fX: "t = Fun f X" "t\<^sub>i \<in> 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'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "\<And>k. k \<in> set K \<Longrightarrow> M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^sub>c k"
by (auto intro: ideduct_synth_mono simp add: ik\<^sub>e\<^sub>s\<^sub>t_append)
hence **: "\<And>k. k \<in> set K \<Longrightarrow> M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>"
using ideduct_synth_subst by auto
have "t\<^sub>i \<in> ik\<^sub>s\<^sub>t (decomp t)" using Decompose.hyps(2,4) ik_rcv_map unfolding decomp_def by auto
shows "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. \<forall>D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. ik\<^sub>e\<^sub>s\<^sub>t D' \<subseteq> ik\<^sub>e\<^sub>s\<^sub>t D"
proof -
let ?IK = "\<lambda>M. \<Union>D \<in> M. ik\<^sub>e\<^sub>s\<^sub>t D"
have "?IK (decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>) \<subseteq> (\<Union>t \<in> A \<union> 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 \<I>))"
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 \<subseteq> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" "?IK M = ?IK (decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>)"
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
shows "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. \<forall>t. A \<turnstile> t \<longrightarrow> A \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile>\<^sub>c t"
proof (rule ccontr)
assume neg: "\<not>(\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. \<forall>t. A \<turnstile> t \<longrightarrow> A \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile>\<^sub>c t)"
obtain D where D: "D \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" "\<forall>D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>. ik\<^sub>e\<^sub>s\<^sub>t D' \<subseteq> 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 \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile> t" "\<not>(A \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<turnstile>\<^sub>c t)"
using neg by (fastforce intro: ideduct_mono)
obtain D' where D':
"D@D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>" "A \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@D') \<turnstile>\<^sub>c t"
"A \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<subset> A \<union> 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 \<subset> 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') \<subseteq> ik\<^sub>e\<^sub>s\<^sub>t D" using D(2) D'(1) by auto
assumes "ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>"
and "sem\<^sub>e\<^sub>s\<^sub>t_c {} \<I> A" "wf\<^sub>e\<^sub>s\<^sub>t {} A" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
and "Ana_invar_subst (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)"
and "well_analyzed A"
shows "\<exists>D \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<I>. ik\<^sub>e\<^sub>s\<^sub>t (A@D) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c t \<cdot> \<I>"
proof -
have ik_eq: "ik\<^sub>e\<^sub>s\<^sub>t (A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<I>) = ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" 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 \<union> assignment_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 assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append
have "ik\<^sub>e\<^sub>s\<^sub>t [a \<cdot>\<^sub>e\<^sub>s\<^sub>t\<^sub>p \<I>] = ik\<^sub>e\<^sub>s\<^sub>t [a] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
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 \<in> subterms\<^sub>s\<^sub>e\<^sub>t ((ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \<union> assignment_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 assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
hence "Ana (Fun f T \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)"
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 assignment_rhs_eq: "assignment_rhs\<^sub>e\<^sub>s\<^sub>t (A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<I>) = assignment_rhs\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
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 \<union> assignment_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 assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append
unfolding Ana_invar_subst_def by simp
hence "assignment_rhs\<^sub>e\<^sub>s\<^sub>t (A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<I>) = assignment_rhs\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
using snoc.IH well_analyzed_split_left[OF snoc.prems(2)]
by (metis assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append_subst(1), metis assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append_subst(2))
have "assignment_rhs\<^sub>e\<^sub>s\<^sub>t [a \<cdot>\<^sub>e\<^sub>s\<^sub>t\<^sub>p \<I>] = assignment_rhs\<^sub>e\<^sub>s\<^sub>t [a] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
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 \<in> subterms\<^sub>s\<^sub>e\<^sub>t ((ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \<union> assignment_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 assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
hence "Ana (Fun f T \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)"
ultimately show ?thesis using Decomp t by (auto simp add: decomp_assignment_rhs_empty)
qed
thus ?case using IH unfolding subst_apply_extstrand_def by simp
qed simp
ultimately obtain D where D:
"D \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) Var"
"(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D) \<turnstile>\<^sub>c t \<cdot> \<I>"
using decomps\<^sub>e\<^sub>s\<^sub>t_exist[OF ik\<^sub>e\<^sub>s\<^sub>t_finite assignment_rhs\<^sub>e\<^sub>s\<^sub>t_finite, of "A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<I>" "A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<I>"]
let ?P = "\<lambda>D D'. \<forall>t. (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D) \<turnstile>\<^sub>c t \<longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t"
have "\<exists>D' \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<I>. ?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 [] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" 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' \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<I>" "?P D D'"
using Decomp.IH by auto
hence IH: "\<And>k. k \<in> set K \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c k"
"(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c Fun f T"
using Decomp.hyps(5,6) by auto
have D'_ik: "ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t ((ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
"ik\<^sub>e\<^sub>s\<^sub>t D' \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_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 \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<union> ik\<^sub>e\<^sub>s\<^sub>t D'" "Fun f T = s \<cdot> \<I>" using AxiomC.prems by blast
hence fT_s_in: "Fun f T \<in> (subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
"s \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)"
using AxiomC D'_ik subset_subterms_Union[of "ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A"]
subst_all_mono[OF subset_subterms_Union, of \<I>]
by (metis (no_types) Un_iff image_eqI subset_Un_eq, metis (no_types) Un_iff 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')" "\<lbrakk>{}; to_st (A@D')\<rbrakk>\<^sub>c \<I>"
using decomps\<^sub>e\<^sub>s\<^sub>t_preserves_model_c[OF D'(1) assms(2)]
\<comment> \<open>In this case \<open>\<I> x\<close> (is a subterm of something that) was derived from an
"earlier intruder knowledge" because \<open>A\<close> is well-formed and has \<open>\<I>\<close> as a model.
So either the intruder composed \<open>Fun f T\<close> himself (making \<open>Decomp (Fun f T)\<close>
unnecessary) or \<open>Fun f T\<close> is an instance of something else in the intruder
knowledge (in which case the "something" can be used in place of \<open>Fun f T\<close>)\<close>
hence "Var x \<in> ik\<^sub>e\<^sub>s\<^sub>t (A@D')" "\<I> x = Fun f T" using s ik\<^sub>e\<^sub>s\<^sub>t_append by auto
show ?thesis
proof (cases "\<forall>m \<in> set M. ik\<^sub>e\<^sub>s\<^sub>t A \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c m")
case True
\<comment> \<open>All terms acquired by decomposing \<open>Fun f T\<close> are already derivable.
Hence there is no need to consider decomposition of \<open>Fun f T\<close> at all.\<close>
have *: "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) = (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<union> set M"
using decomp_ik[OF \<open>Ana (Fun f T) = (K,M)\<close>] ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f T)]"]
{ fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<union> set M \<turnstile>\<^sub>c t'"
hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t'"
proof (induction t' rule: intruder_synth_induct)
case (AxiomC t') thus ?case
proof
assume "t' \<in> set M"
moreover have "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) = ik\<^sub>e\<^sub>s\<^sub>t A \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" 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
\<comment> \<open>Some term acquired by decomposition of \<open>Fun f T\<close> cannot be derived in \<open>\<turnstile>\<^sub>c\<close>.
\<open>Fun f T\<close> must therefore be an instance of something else in the intruder knowledge,
because of well-formedness.\<close>
then obtain t\<^sub>i where t\<^sub>i: "t\<^sub>i \<in> set T" "\<not>ik\<^sub>e\<^sub>s\<^sub>t (A@D') \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c t\<^sub>i"
using Ana_fun_subterm[OF \<open>Ana (Fun f T) = (K,M)\<close>] by (auto simp add: ik\<^sub>e\<^sub>s\<^sub>t_append)
obtain S where fS:
"Fun f S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t (A@D')) \<or>
Fun f S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (assignment_rhs\<^sub>e\<^sub>s\<^sub>t (A@D'))"
"\<I> x = Fun f S \<cdot> \<I>"
using strand_sem_wf_ik_or_assignment_rhs_fun_subterm[
OF AD'_props \<open>Var x \<in> ik\<^sub>e\<^sub>s\<^sub>t (A@D')\<close> _ t\<^sub>i \<open>interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<close>]
\<open>\<I> x = Fun f T\<close>
by moura
hence fS_in: "Fun f S \<cdot> \<I> \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
"Fun f S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t A)"
using imageI[OF s(1), of "\<lambda>x. x \<cdot> \<I>"] Var
ik\<^sub>e\<^sub>s\<^sub>t_append[of A D'] assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append[of A D']
s(2) fS(2) \<open>s = Var x\<close> \<open>Ana (Fun f T) = (K,M)\<close>
by simp_all
hence "MS \<noteq> []" using \<open>M \<noteq> []\<close> by simp
have "\<And>k. k \<in> set KS \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t A \<union> ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>"
using AxiomC.prems(1) \<open>K = KS \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>\<close> by (simp add: image_Un)
hence D'': "D'@[Decomp (Fun f S)] \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t A) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t A) \<I>"
using decomps\<^sub>e\<^sub>s\<^sub>t.Decomp[OF D'(1) fS_in(2) Ana_fS \<open>MS \<noteq> []\<close>] AxiomC.prems(1)
intruder_synth.AxiomC[OF fS_in(1)]
by simp
moreover {
fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) \<turnstile>\<^sub>c t'"
hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun f S)]) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t'"
proof (induction t' rule: intruder_synth_induct)
case (AxiomC t')
hence "t' \<in> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<or> t' \<in> 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' \<in> ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f T)]"
hence "t' \<in> ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
using decomp_ik \<open>Ana (Fun f T) = (K,M)\<close> \<open>Ana (Fun f S) = (KS,MS)\<close> \<open>M = MS \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>\<close>
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)] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"],
of "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun f S)]) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)"]
by (auto simp add: ik\<^sub>e\<^sub>s\<^sub>t_append)
next
assume "t' \<in> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D"
hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t'"
by (metis D'(2) intruder_synth.AxiomC)
hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun f S)] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^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)]"]
image_Un[of "\<lambda>x. x \<cdot> \<I>" "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) \<comment> \<open>Hence \<open>Decomp (Fun f T)\<close> can be substituted for \<open>Decomp (Fun g S)\<close>\<close>
hence KM: "K = Ks \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>" "M = Ms \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>" "set K = set Ks \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" "set M = set Ms \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
using fT_s_in(2) \<open>Ana (Fun f T) = (K,M)\<close> Ana_s s(2)
Ana_invar_substD[OF assms(5), of g S]
by auto
hence Ms_nonempty: "Ms \<noteq> []" using \<open>M \<noteq> []\<close> by auto
{ fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) \<turnstile>\<^sub>c t'"
hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t (D'@[Decomp (Fun g S)]) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t'" using AxiomC
proof (induction t' rule: intruder_synth_induct)
case (AxiomC t')
hence "t' \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<or> t' \<in> ik\<^sub>e\<^sub>s\<^sub>t D \<or> t' \<in> set M"
by (simp add: decomp_ik ik\<^sub>e\<^sub>s\<^sub>t_append)
thus ?case
proof (elim disjE)
assume "t' \<in> ik\<^sub>e\<^sub>s\<^sub>t D"
hence *: "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^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' \<in> set M"
hence "t' \<in> ik\<^sub>e\<^sub>s\<^sub>t [Decomp (Fun g S)] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
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(3) 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 *: "\<And>m. m \<in> set M \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c m"
using Ana_fun_subterm[OF \<open>Ana (Fun f T) = (K, M)\<close>] ComposeC.hyps(3)
let ?S = "send\<langle>t\<rangle>\<^sub>s\<^sub>t#S"
let ?A = "\<A>@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]"
have \<S>: "\<And>S'. S' \<in> update\<^sub>s\<^sub>t \<S> ?S \<Longrightarrow> S' = S \<or> S' \<in> \<S>" by auto
have 1: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_split(2) by (auto simp add: Un_assoc)
ultimately have 3: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono)
have 4: "\<forall>S \<in> \<S>. \<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> 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 (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto
let ?S = "receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S"
let ?A = "\<A>@[Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]"
have \<S>: "\<And>S'. S' \<in> update\<^sub>s\<^sub>t \<S> ?S \<Longrightarrow> S' = S \<or> S' \<in> \<S>" by auto
have 1: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_split(2) by (auto simp add: Un_assoc)
ultimately have 3: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis wf_vars_mono)
have 4: "\<forall>S \<in> \<S>. \<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> 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 (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto
assumes "wf\<^sub>s\<^sub>t\<^sub>s' \<S> \<A>" "\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>"
shows "wf\<^sub>s\<^sub>t\<^sub>s' (update\<^sub>s\<^sub>t \<S> (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S)) (\<A>@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])"
unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def
proof (intro conjI)
let ?S = "\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S"
let ?A = "\<A>@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)]"
have \<S>: "\<And>S'. S' \<in> update\<^sub>s\<^sub>t \<S> ?S \<Longrightarrow> S' = S \<or> S' \<in> \<S>" by auto
have 1: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto
moreover have 2:
"a = Assign \<Longrightarrow> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A> \<union> fv t \<union> fv t'"
"a = Check \<Longrightarrow> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>"
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_split(2) by (auto simp add: Un_assoc)
have 4: "\<forall>S \<in> \<S>. \<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> 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 (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by (cases a) auto
let ?S = "\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t#S"
let ?A = "\<A>@[Step (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t)]"
have \<S>: "\<And>S'. S' \<in> update\<^sub>s\<^sub>t \<S> ?S \<Longrightarrow> S' = S \<or> S' \<in> \<S>" by auto
have 1: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>) (dual\<^sub>s\<^sub>t S)" using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by auto
moreover have 2: "wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \<A>"
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_split(2) by (auto simp add: Un_assoc)
ultimately have 3: "\<forall>S \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by metis
have 4: "\<forall>S \<in> \<S>. \<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> 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 (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto
have "fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}"
"\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S' = {}"
"\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S' \<inter> bvars\<^sub>s\<^sub>t S = {}"
using 4 assms(2) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by force+
thus "\<forall>S \<in> update\<^sub>s\<^sub>t \<S> ?S. \<forall>S' \<in> update\<^sub>s\<^sub>t \<S> ?S. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S' = {}" by (metis 4 \<S>)
have "\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t ?S \<inter> bvars\<^sub>s\<^sub>t S' = {}" "\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S' \<inter> bvars\<^sub>s\<^sub>t ?S = {}"
using assms unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by metis+
moreover have "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> fv\<^sub>s\<^sub>t (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S)" by auto
ultimately have 5:
"\<forall>S' \<in> \<S>. (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X) \<inter> bvars\<^sub>s\<^sub>t S' = {}"
"fv\<^sub>e\<^sub>s\<^sub>t ?A = fv\<^sub>e\<^sub>s\<^sub>t \<A> \<union> (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X)" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = set X \<union> bvars\<^sub>e\<^sub>s\<^sub>t \<A>"
"\<forall>S \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> set X = {}"
using to_st_append
by (blast, force, force, force)
have *: "\<forall>S \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using 5(3,4) assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by blast
hence "fv\<^sub>s\<^sub>t ?S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" using assms(2) by metis
hence "fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by auto
thus "\<forall>S \<in> update\<^sub>s\<^sub>t \<S> ?S. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t ?A = {}" by (metis * \<S>)
have **: "\<forall>S \<in> \<S>. fv\<^sub>e\<^sub>s\<^sub>t ?A \<inter> bvars\<^sub>s\<^sub>t S = {}"
using 5(1,2) assms(1) unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def by fast
hence "fv\<^sub>e\<^sub>s\<^sub>t ?A \<inter> bvars\<^sub>s\<^sub>t ?S = {}" using assms(2) by metis
hence "fv\<^sub>e\<^sub>s\<^sub>t ?A \<inter> bvars\<^sub>s\<^sub>t S = {}" by auto
thus "\<forall>S \<in> update\<^sub>s\<^sub>t \<S> ?S. fv\<^sub>e\<^sub>s\<^sub>t ?A \<inter> bvars\<^sub>s\<^sub>t S = {}" by (metis ** \<S>)
hence "t' \<in> (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>')) \<union> (ik\<^sub>e\<^sub>s\<^sub>t \<A>)" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto
have 1: "t' \<in> (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>)) \<union> (ik\<^sub>e\<^sub>s\<^sub>t \<A>)"
when "t' \<in> (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>')) \<union> (ik\<^sub>e\<^sub>s\<^sub>t \<A>')"
for t'
proof -
have "t' \<in> (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>')) \<union> (ik\<^sub>e\<^sub>s\<^sub>t \<A>)" using that assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto
thus ?thesis using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset[OF assms(1)] assms(2) by auto
qed
have 2: "t'' \<in> (\<Union>(assignment_rhs\<^sub>s\<^sub>t ` \<S>)) \<union> (assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>)"
when "t'' \<in> (\<Union>(assignment_rhs\<^sub>s\<^sub>t ` \<S>')) \<union> (assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>')" "a = Assign"
hence "t' \<in> (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>')) \<union> (ik\<^sub>e\<^sub>s\<^sub>t \<A>)" using assms ik\<^sub>e\<^sub>s\<^sub>t_append by auto
| Decompose[simp]: "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A> \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>)
\<Longrightarrow> (\<S>,\<A>) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>,\<A>@[Decomp (Fun f T)])"
abbreviation pts_symbolic_rtrancl (infix "\<Rightarrow>\<^sup>\<bullet>\<^sup>*" 50) where "a \<Rightarrow>\<^sup>\<bullet>\<^sup>* b \<equiv> pts_symbolic\<^sup>*\<^sup>* a b"
private abbreviation pts_symbolic_c_rtrancl (infix "\<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>*" 50) where "a \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* b \<equiv> pts_symbolic_c\<^sup>*\<^sup>* a b"
and "\<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (send\<langle>t\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[receive\<langle>t\<rangle>\<^sub>s\<^sub>t]\<rbrakk> \<Longrightarrow> P"
and "\<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[send\<langle>t\<rangle>\<^sub>s\<^sub>t]\<rbrakk> \<Longrightarrow> P"
and "\<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]\<rbrakk> \<Longrightarrow> P"
and "\<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]\<rbrakk> \<Longrightarrow> P"
and "\<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (send\<langle>t\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]\<rbrakk> \<Longrightarrow> P"
and "\<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]\<rbrakk> \<Longrightarrow> P"
and "\<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)]\<rbrakk> \<Longrightarrow> P"
and "\<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t#S \<in> \<S>; \<S>' = update\<^sub>s\<^sub>t \<S> (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t#S); \<A>' = \<A>@[Step (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t)]\<rbrakk> \<Longrightarrow> P"
and "\<And>f T. \<lbrakk>Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A> \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>); \<S>' = \<S>; \<A>' = \<A>@[Decomp (Fun f T)]\<rbrakk> \<Longrightarrow> P"
from step.hyps(2) step.IH[OF step.prems] show ?case
proof (induction rule: pts_symbolic_c_induct)
case Nil
have 1: "\<forall>S \<in> {to_st \<A>2}. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Nil by simp
have 2: "\<S>2 = \<S>1 - {[]}" "\<forall>S \<in> \<S>1. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Nil by simp_all
have "\<forall>S \<in> \<S>2. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
proof
fix S assume "S \<in> \<S>2"
hence "S \<in> \<S>1" using 2(1) by simp
thus "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using 2(2) by simp
qed
thus ?case using 1 by auto
next
case (Send t S)
have 1: "\<forall>S \<in> {to_st \<A>2}. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Send by (simp add: to_st_append)
have 2: "\<S>2 = insert S (\<S>1 - {send\<langle>t\<rangle>\<^sub>s\<^sub>t#S})" "\<forall>S \<in> \<S>1. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Send by simp_all
have 3: "\<forall>S \<in> \<S>2. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
proof
fix S' assume "S' \<in> \<S>2"
hence "S' \<in> \<S>1 \<or> S' = S" using 2(1) by auto
moreover have "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Send.hyps 2(2) by auto
ultimately show "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'" using 2(2) by blast
qed
thus ?case using 1 by auto
next
case (Receive t S)
have 1: "\<forall>S \<in> {to_st \<A>2}. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Receive by (simp add: to_st_append)
have 2: "\<S>2 = insert S (\<S>1 - {receive\<langle>t\<rangle>\<^sub>s\<^sub>t#S})" "\<forall>S \<in> \<S>1. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
using Receive by simp_all
have 3: "\<forall>S \<in> \<S>2. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
proof
fix S' assume "S' \<in> \<S>2"
hence "S' \<in> \<S>1 \<or> S' = S" using 2(1) by auto
moreover have "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Receive.hyps 2(2) by auto
ultimately show "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'" using 2(2) by blast
qed
show ?case using 1 3 by auto
next
case (Equality a t t' S)
have 1: "to_st \<A>2 = to_st \<A>1@[\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]" "list_all tfr\<^sub>s\<^sub>t\<^sub>p (to_st \<A>1)"
using Equality by (simp_all add: to_st_append)
have 2: "list_all tfr\<^sub>s\<^sub>t\<^sub>p [\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]" using Equality by fastforce
have 3: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (to_st \<A>2)"
using tfr_stp_all_append[of "to_st \<A>1" "[\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]"] 1 2 by metis
hence 4: "\<forall>S \<in> {to_st \<A>2}. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Equality by simp
have 5: "\<S>2 = insert S (\<S>1 - {\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S})" "\<forall>S \<in> \<S>1. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
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)
next
case Send thus ?case by (metis well_analyzed_singleton(2) well_analyzed_append)
next
case Equality thus ?case by (metis well_analyzed_singleton(3) well_analyzed_append)
next
case Inequality thus ?case by (metis well_analyzed_singleton(4) well_analyzed_append)
next
case (Decompose f T)
hence "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1) - (Var`\<V>)" by auto
thus ?case by (metis well_analyzed.Decomp Decompose.prems Decompose.hyps(3))
using ik\<^sub>e\<^sub>s\<^sub>t_append assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append decomp_ik
decomp_assignment_rhs_empty Decompose.hyps(3)
by auto
{ fix g S assume "Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t`\<S>2) \<union> ik\<^sub>e\<^sub>s\<^sub>t \<A>2 \<union> ?X)"
hence "Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>1) \<union> ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> set M \<union> ?X)"
using * Decompose.hyps(2) by auto
hence "Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>1))
\<or> Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1)
\<or> Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (set M)
\<or> Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(assignment_rhs\<^sub>s\<^sub>t`\<S>1))
\<or> Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
using Decompose * Ana_fun_subterm[OF Ana] by auto
moreover have "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
by (meson Un_upper2 Ana_subterm[OF Ana] subterms_subset_set psubsetE subset_trans)
ultimately have "Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>1) \<union> ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> ?Y)"
by auto
}
thus ?case using Decompose unfolding Ana_invar_subst_def by metis
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 "\<forall>S\<in>S. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^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 wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_decomp_rm\<^sub>e\<^sub>s\<^sub>t_subset
wf_vars_mono le_iff_sup)
show "\<forall>Sa\<in>S. \<forall>S'\<in>S. fv\<^sub>s\<^sub>t Sa \<inter> bvars\<^sub>s\<^sub>t S' = {}" by (metis assms(2) wf\<^sub>s\<^sub>t\<^sub>s'_def)
show "\<forall>S\<in>S. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t A = {}" by (metis assms(2) wf\<^sub>s\<^sub>t\<^sub>s'_def bvars_decomp_rm)
show "\<forall>S\<in>S. fv\<^sub>e\<^sub>s\<^sub>t A \<inter> 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)
using ik\<^sub>e\<^sub>s\<^sub>t_append[of A B] assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append[of A B]
by auto
hence "Fun f X \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t (A@B) \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t (A@B))" using Decomp.hyps by auto
hence "(S,A@B) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (S,A@B@[Decomp (Fun f X)])"
hence "(\<S>, \<A>\<^sub>d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \<A>1d)" using \<A>1d pts_symbolic_c.Nil[OF Nil.hyps(1), of \<A>1d] by simp
thus ?case using \<A>1d Nil by auto
next
case (Send t S)
hence "sem\<^sub>e\<^sub>s\<^sub>t_c {} \<I> (\<A>1d@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)])" using sem\<^sub>e\<^sub>s\<^sub>t_c.Receive[OF \<A>1d(3)] by simp
moreover have "(\<S>1, \<A>1d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \<A>1d@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)])"
using Send.hyps(2) pts_symbolic_c.Send[OF Send.hyps(1), of \<A>1d] by simp
moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\<A>1d@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)])) = \<A>2"
using step.prems sem\<^sub>e\<^sub>s\<^sub>t_d_eq_sem_st[of "{}" \<I> "to_est \<A>2"]
to_st_append to_est_append to_st_to_est_inv
by auto
hence "sem\<^sub>e\<^sub>s\<^sub>t_c {} \<I> (\<A>1d@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])" using sem\<^sub>e\<^sub>s\<^sub>t_c.Equality[OF \<A>1d(3)] by simp
moreover have "(\<S>1, \<A>1d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \<A>1d@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])"
using Equality.hyps(2) pts_symbolic_c.Equality[OF Equality.hyps(1), of \<A>1d] by simp
moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\<A>1d@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])) = \<A>2"
moreover have "ik\<^sub>s\<^sub>t \<A>1 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> ik\<^sub>e\<^sub>s\<^sub>t \<A>1d \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>" using \<A>1d(1) decomp_rm\<^sub>e\<^sub>s\<^sub>t_ik_subset by auto
ultimately have *: "ik\<^sub>e\<^sub>s\<^sub>t \<A>1d \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>" using ideduct_mono by auto
have "wf\<^sub>s\<^sub>t\<^sub>s' \<S> \<A>\<^sub>d" by (rule wf\<^sub>s\<^sub>t\<^sub>s'_decomp_rm[OF wa assms(4)])
have "(\<S>, \<A>\<^sub>d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>1, \<A>1d@D)" using \<A>1d(2) decomps\<^sub>e\<^sub>s\<^sub>t_pts_symbolic_c[OF D(1), of \<S>1] by auto
show "(\<S>,to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>)) \<Rightarrow>\<^sup>\<bullet>\<^sup>* (\<S>',to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>'))" using assms(1)
proof (induction rule: rtranclp_induct2)
case (step \<S>1 \<A>1 \<S>2 \<A>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 \<A>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 \<A>1)"]
by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append)
hence IH: "\<forall>t \<in> 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) \<subseteq> {t} \<union> set K \<union> set T" using decomp_set_unfold[OF Ana_t] by force
moreover have "\<forall>t \<in> set T. wf\<^sub>t\<^sub>r\<^sub>m t" using Ana_subterm[OF Ana_t] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> wf_trm_subterm by auto
ultimately have "\<forall>t \<in> trms\<^sub>s\<^sub>t (decomp t). wf\<^sub>t\<^sub>r\<^sub>m t" using Ana_keys_wf'[OF Ana_t] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> by auto
thus ?thesis using IH Decomp by auto
qed auto
qed simp
private lemma to_st_trms_SMP_subset: "trms\<^sub>s\<^sub>t (to_st A) \<subseteq> SMP (trms\<^sub>e\<^sub>s\<^sub>t A)"
hence *: "t \<in> trms\<^sub>s\<^sub>t (to_st [x]) \<union> 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) \<subseteq> trms\<^sub>s\<^sub>t (to_st (x#A))" "trms\<^sub>e\<^sub>s\<^sub>t A \<subseteq> trms\<^sub>e\<^sub>s\<^sub>t (x#A)"
have *: "trms\<^sub>s\<^sub>t (to_st A) \<subseteq> SMP (trms\<^sub>e\<^sub>s\<^sub>t A)"
using to_st_trms_wf to_st_trms_SMP_subset assms unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by auto
have "trms\<^sub>s\<^sub>t (to_st A) = trms\<^sub>s\<^sub>t (to_st A) \<union> trms\<^sub>e\<^sub>s\<^sub>t A" by (blast dest!: trms\<^sub>e\<^sub>s\<^sub>tD)
hence "SMP (trms\<^sub>e\<^sub>s\<^sub>t A) = SMP (trms\<^sub>s\<^sub>t (to_st A))" using SMP_subset_union_eq[OF *] by auto
thus ?thesis using * assms unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by presburger
by (metis dual\<^sub>s\<^sub>t_append List.append_assoc List.append_Nil List.append_Cons)
moreover have "({x#S}, A) \<Rightarrow>\<^sup>\<bullet> ({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 0: "({dual\<^sub>s\<^sub>t \<A>},[]) \<Rightarrow>\<^sup>\<bullet>\<^sup>* ({},\<A>)" using dual\<^sub>s\<^sub>t_self_inverse by (metis List.append_Nil)
have "fv\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \<A>) \<inter> bvars\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \<A>) = {}" using assms(2) dual\<^sub>s\<^sub>t_fv dual\<^sub>s\<^sub>t_bvars by metis+
hence 1: "wf\<^sub>s\<^sub>t\<^sub>s {dual\<^sub>s\<^sub>t \<A>}" using assms(1,2) dual\<^sub>s\<^sub>t_self_inverse[of \<A>] unfolding wf\<^sub>s\<^sub>t\<^sub>s_def by auto