locale stateful_typed_model = typed_model arity public Ana \<Gamma>
for arity::"'fun \<Rightarrow> nat"
and public::"'fun \<Rightarrow> bool"
and Ana::"('fun,'var) term \<Rightarrow> (('fun,'var) term list \<times> ('fun,'var) term list)"
and \<Gamma>::"('fun,'var) term \<Rightarrow> ('fun,'atom::finite) term_type"
+
fixes Pair::"'fun"
assumes Pair_arity: "arity Pair = 2"
and Ana_subst': "\<And>f T \<delta> K M. 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>)"
(\<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 \<union> pair ` set F') \<longrightarrow>
T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)))"
| "tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p _ = True"
text \<open>Type-flaw resistance of stateful constraints\<close>
definition tfr\<^sub>s\<^sub>s\<^sub>t where "tfr\<^sub>s\<^sub>s\<^sub>t S \<equiv> tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t S) \<and> list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p S"
subsection \<open>Small Lemmata\<close>
lemma pair_in_pair_image_iff:
"pair (s,t) \<in> pair ` P \<longleftrightarrow> (s,t) \<in> P"
unfolding pair_def by fast
lemma subst_apply_pairs_pair_image_subst:
"pair ` set (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>) = pair ` set F \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
unfolding subst_apply_pairs_def pair_def by (induct F) auto
shows "(\<exists>u \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. t = u \<cdot> \<theta> \<and> s \<in> set (snd (Ana u)) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>) \<or> (\<exists>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. t \<sqsubseteq> \<theta> x)"
proof (cases "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>")
case True
then obtain u where u: "u \<in> subterms\<^sub>s\<^sub>e\<^sub>t M" "t = u \<cdot> \<theta>" by moura
show ?thesis
proof (cases u)
case (Var x)
hence "x \<in> fv\<^sub>s\<^sub>e\<^sub>t M" using fv_subset_subterms[OF u(1)] by simp
(\<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 \<union> pair ` set F') \<longrightarrow>
T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)))))"
(is "?P S = ?Q S")
proof
show "?P S \<Longrightarrow> ?Q S"
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
show "?Q S \<Longrightarrow> ?P S"
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
qed
lemma fun_pair_eq[dest]: "pair d = pair d' \<Longrightarrow> d = d'"
proof -
obtain t s t' s' where "d = (t,s)" "d' = (t',s')" by moura
thus "pair d = pair d' \<Longrightarrow> d = d'" unfolding pair_def by simp
then obtain p where p: "p \<in> M" "t = pair (p \<cdot>\<^sub>p \<delta>)" by blast
thus "t \<in> pair ` M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>" using fun_pair_subst[of p \<delta>] by force
qed
qed
lemma fun_pair_eq_subst: "pair d \<cdot> \<delta> = pair d' \<cdot> \<theta> \<longleftrightarrow> d \<cdot>\<^sub>p \<delta> = d' \<cdot>\<^sub>p \<theta>"
by (metis fun_pair_subst fun_pair_eq[of "d \<cdot>\<^sub>p \<delta>" "d' \<cdot>\<^sub>p \<theta>"])
using SMP_mono[of ?M ?N] setops\<^sub>s\<^sub>s\<^sub>t_append[of A B]
by auto
{ fix s t assume **: "tfr\<^sub>s\<^sub>e\<^sub>t ?N" "s \<in> SMP ?M - Var`\<V>" "t \<in> SMP ?M - Var`\<V>" "(\<exists>\<delta>. Unifier \<delta> s t)"
hence "s \<in> SMP ?N - Var`\<V>" "t \<in> SMP ?N - Var`\<V>" using * by auto
hence "\<Gamma> s = \<Gamma> t" using **(1,4) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
} moreover have "\<forall>t \<in> ?N. wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> \<forall>t \<in> ?M. wf\<^sub>t\<^sub>r\<^sub>m t" using * by blast
ultimately have "tfr\<^sub>s\<^sub>e\<^sub>t ?N \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t ?M" unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
hence "tfr\<^sub>s\<^sub>e\<^sub>t ?M" using assms unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by metis
thus "tfr\<^sub>s\<^sub>s\<^sub>t A" using assms unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by simp
using SMP_mono[of ?M ?N] setops\<^sub>s\<^sub>s\<^sub>t_append[of A B]
by auto
{ fix s t assume **: "tfr\<^sub>s\<^sub>e\<^sub>t ?N" "s \<in> SMP ?M - Var`\<V>" "t \<in> SMP ?M - Var`\<V>" "(\<exists>\<delta>. Unifier \<delta> s t)"
hence "s \<in> SMP ?N - Var`\<V>" "t \<in> SMP ?N - Var`\<V>" using * by auto
hence "\<Gamma> s = \<Gamma> t" using **(1,4) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
} moreover have "\<forall>t \<in> ?N. wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> \<forall>t \<in> ?M. wf\<^sub>t\<^sub>r\<^sub>m t" using * by blast
ultimately have "tfr\<^sub>s\<^sub>e\<^sub>t ?N \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t ?M" unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
hence "tfr\<^sub>s\<^sub>e\<^sub>t ?M" using assms unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by metis
thus "tfr\<^sub>s\<^sub>s\<^sub>t B" using assms unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by simp
hence "\<exists>\<delta>. Unifier \<delta> t t'" by (metis subst_subst_compose[of _ \<theta>])
moreover have "\<Gamma> t = \<Gamma> (t \<cdot> \<theta>)" "\<Gamma> t' = \<Gamma> (t' \<cdot> \<theta>)" by (metis wt_subst_trm''[OF assms(2)])+
ultimately have "\<Gamma> (t \<cdot> \<theta>) = \<Gamma> (t' \<cdot> \<theta>)" using s Equality by simp
thus ?thesis using Equality True by simp
qed simp
next
case (NegChecks X F G)
let ?P = "\<lambda>F G. G = [] \<and> (\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F-set X. \<exists>a. \<Gamma> (Var x) = TAtom a)"
let ?Q = "\<lambda>F G. \<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 \<union> pair ` set G) \<longrightarrow>
T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)"
let ?\<theta> = "rm_vars (set X) \<theta>"
have "?P F G \<or> ?Q F G" using NegChecks assms(1) by simp
have "G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta> = []" using * by simp
moreover have "\<exists>a. \<Gamma> (Var x) = TAtom a" when x: "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>) - set X" for x
proof -
obtain t t' where t: "(t,t') \<in> set (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>)" "x \<in> fv t \<union> fv t' - set X"
using x(1) by auto
then obtain u u' where u: "(u,u') \<in> set F" "u \<cdot> ?\<theta> = t" "u' \<cdot> ?\<theta> = t'"
unfolding subst_apply_pairs_def by auto
obtain y where y: "y \<in> fv u \<union> fv u' - set X" "x \<in> fv (?\<theta> y)"
using t(2) u(2,3) rm_vars_fv_obtain by fast
hence a: "\<exists>a. \<Gamma> (Var y) = TAtom a" using u * by auto
have a': "\<Gamma> (Var y) = \<Gamma> (?\<theta> y)"
using wt_subst_trm''[OF wt_subst_rm_vars[OF \<theta>(1), of "set X"], of "Var y"]
by simp
have "(\<exists>z. ?\<theta> y = Var z) \<or> (\<exists>c. ?\<theta> y = Fun c [])"
proof (cases "?\<theta> y \<in> subst_range \<theta>")
case True thus ?thesis
using a a' \<theta>(2) const_type_inv_wf
by (cases "?\<theta> y") fastforce+
qed fastforce
hence "?\<theta> y = Var x" using y(2) by fastforce
hence "\<Gamma> (Var x) = \<Gamma> (Var y)" using a' by simp
thus ?thesis using a by presburger
qed
ultimately show ?thesis by simp
next
assume *: "?Q F G"
have **: "set X \<inter> range_vars ?\<theta> = {}"
using \<theta>(3) NegChecks rm_vars_img_fv_subset[of "set X" \<theta>] by auto
have "?Q (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>) (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>)"
using ineq_subterm_inj_cond_subst[OF ** *]
trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst[of F "rm_vars (set X) \<theta>"]
subst_apply_pairs_pair_image_subst[of G "rm_vars (set X) \<theta>"]
"G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D) \<Longrightarrow> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<subseteq> pair ` set F \<union> pair ` set D"
proof (induction F D arbitrary: G rule: tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s.induct)
case (2 s t F D G)
obtain d G' where G:
"d \<in> set D" "G' \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D)" "G = (pair (s,t), pair d)#G'"
"\<Union>(trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ` set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D)) \<subseteq> pair ` set F \<union> pair ` set D"
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_trms_subset by blast
lemma tr_trms_subset:
"A' \<in> set (tr A D) \<Longrightarrow> trms\<^sub>s\<^sub>t A' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D"
proof (induction A D arbitrary: A' rule: tr.induct)
case 1 thus ?case by simp
next
case (2 t A D)
then obtain A'' where A'': "A' = send\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)" by moura
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D" by (metis "2.IH")
thus ?case using A'' by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
next
case (3 t A D)
then obtain A'' where A'': "A' = receive\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)" by moura
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D" by (metis "3.IH")
thus ?case using A'' by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
next
case (4 ac t t' A D)
then obtain A'' where A'': "A' = \<langle>ac: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)" by moura
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D" by (metis "4.IH")
thus ?case using A'' by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
next
case (5 t s A D)
hence "A' \<in> set (tr A (List.insert (t,s) D))" by simp
hence "trms\<^sub>s\<^sub>t A' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set (List.insert (t, s) D)"
by (metis "5.IH")
thus ?case by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
next
case (6 t s A D)
from 6 obtain Di A'' B C where A'':
"Di \<in> set (subseqs D)" "A'' \<in> set (tr A [d\<leftarrow>D. d \<notin> set Di])" "A' = (B@C)@A''"
"C = map (\<lambda>d. Inequality [] [(pair (t,s) , pair d)]) [d\<leftarrow>D. d \<notin> set Di]"
by moura
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set [d\<leftarrow>D. d \<notin> set Di]"
by (metis "6.IH")
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) \<union> pair ` set D"
by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
moreover have "trms\<^sub>s\<^sub>t (B@C) \<subseteq> insert (pair (t,s)) (pair ` set D)"
using A''(4,5) subseqs_set_subset[OF A''(1)] by auto
moreover have "pair (t,s) \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t (Delete t s#A)" by (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
ultimately show ?case using A''(3) trms\<^sub>s\<^sub>t_append[of "B@C" A'] by auto
hence "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D" by (metis "7.IH")
moreover have "trms\<^sub>s\<^sub>t A' = {pair (t,s), pair d} \<union> trms\<^sub>s\<^sub>t A''"
using A''(1,3) by auto
ultimately show ?case using A''(1) by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
next
case (8 X F F' A D)
from 8 obtain A'' where A'':
"A'' \<in> set (tr A D)" "A' = (map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))@A''"
by moura
define B where "B \<equiv> \<Union>(trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ` set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))"
have "trms\<^sub>s\<^sub>t A'' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D" by (metis A''(1) "8.IH")
hence "trms\<^sub>s\<^sub>t A' \<subseteq> B \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D"
using A'' B_def by auto
moreover have "B \<subseteq> pair ` set F' \<union> pair ` set D"
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_trms_subset'[of F' D] B_def by simp
moreover have "pair ` setops\<^sub>s\<^sub>s\<^sub>t (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>#A) = pair ` set F' \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A"
by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
"G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D) \<Longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s D"
proof (induction F D arbitrary: G rule: tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s.induct)
case (2 s t F D G)
obtain d G' where G:
"d \<in> set D" "G' \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D)" "G = (pair (s,t), pair d)#G'"
using "2.prems"(1) by moura
show ?case using "2.IH"[OF G(1,2)] G(1,3) unfolding pair_def by auto
qed simp
lemma tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_vars_subset': "\<Union>(fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ` set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F D)) \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s D"
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_vars_subset[of _ F D] by blast
lemma tr_vars_subset:
assumes "A' \<in> set (tr A D)"
shows "fv\<^sub>s\<^sub>t A' \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t A \<union> (\<Union>(t,t') \<in> set D. fv t \<union> fv t')" (is ?P)
and "bvars\<^sub>s\<^sub>t A' \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t A" (is ?Q)
proof -
show ?P using assms
proof (induction A arbitrary: A' D rule: strand_sem_stateful_induct)
"Di \<in> set (subseqs D)" "A' = (constr Di)@A''" "A'' \<in> set (tr A (fltD Di))"
unfolding constr_def fltD_def by moura
hence "fv\<^sub>s\<^sub>t A'' \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t A \<union> Dfv (fltD Di)"
unfolding Dfv_def constr_def fltD_def by (metis ConsDel.IH)
moreover have "Dfv (fltD Di) \<subseteq> Dfv D" unfolding Dfv_def constr_def fltD_def by auto
moreover have "Dfv Di \<subseteq> Dfv D"
using subseqs_set_subset(1)[OF *(1)] unfolding Dfv_def constr_def fltD_def by fast
moreover have "fv\<^sub>s\<^sub>t (constr Di) \<subseteq> fv t \<union> fv s \<union> (Dfv Di \<union> Dfv (fltD Di))"
unfolding Dfv_def constr_def fltD_def pair_def by auto
moreover have "fv\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) = fv t \<union> fv s \<union> fv\<^sub>s\<^sub>s\<^sub>t A" by auto
moreover have "fv\<^sub>s\<^sub>t A' = fv\<^sub>s\<^sub>t (constr Di) \<union> fv\<^sub>s\<^sub>t A''" using * by force
ultimately have "fv\<^sub>s\<^sub>t A' \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) \<union> Dfv D" by auto
thus ?case unfolding Dfv_def fltD_def constr_def by simp
next
case (ConsNegChecks A' D X F F' A)
then obtain A'' where A'':
"A'' \<in> set (tr A D)" "A' = (map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))@A''"
by moura
define B where "B \<equiv> \<Union>(fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ` set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))"
have 1: "fv\<^sub>s\<^sub>t (map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D)) \<subseteq> (B \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) - set X"
unfolding B_def by auto
have 2: "B \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s D"
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_vars_subset'[of F' D]
unfolding B_def by simp
have "fv\<^sub>s\<^sub>t A' \<subseteq> ((fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s D \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) - set X) \<union> fv\<^sub>s\<^sub>t A''"
using 1 2 A''(2) by fastforce
thus ?case using ConsNegChecks.IH[OF A''(1)] by auto
qed fastforce+
show ?Q using assms by (induct A arbitrary: A' D rule: strand_sem_stateful_induct) fastforce+
qed
lemma tr_vars_disj:
assumes "A' \<in> set (tr A D)" "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
and "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
shows "fv\<^sub>s\<^sub>t A' \<inter> bvars\<^sub>s\<^sub>t A' = {}"
and t: "t \<in> trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
shows "\<exists>s \<delta>. s \<in> trms\<^sub>s\<^sub>s\<^sub>t S \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = s \<cdot> \<delta>"
using t
proof (induction S)
case (Cons s S) thus ?case
proof (cases "t \<in> trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)")
case False
hence "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
using Cons.prems trms\<^sub>s\<^sub>s\<^sub>t_subst_cons[of s S \<theta>]
by auto
then obtain u where u: "u \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p s" "t = u \<cdot> rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)) \<theta>"
using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst'' by blast
thus ?thesis
using trms\<^sub>s\<^sub>s\<^sub>t_subst_cons[of s S \<theta>]
wt_subst_rm_vars[OF \<theta>(1), of "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)"]
wf_trms_subst_rm_vars'[OF \<theta>(2), of "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)"]
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (pair ` setops\<^sub>s\<^sub>s\<^sub>t A)"
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A)"
proof -
show "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (pair ` setops\<^sub>s\<^sub>s\<^sub>t A)"
proof (induction A)
case (Cons a A)
hence 0: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (pair ` setops\<^sub>s\<^sub>s\<^sub>t A)" by auto
thus ?case
proof (cases a)
case (NegChecks X F F')
hence "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F')" using 0 by simp
thus ?thesis using NegChecks wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_pairs[of F'] 0 by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
qed (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def dest: fun_pair_wf\<^sub>t\<^sub>r\<^sub>m)
qed (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
thus "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A)" by fast
qed
lemma SMP_MP_split:
assumes "t \<in> SMP M"
and M: "\<forall>m \<in> M. is_Fun m"
shows "(\<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t \<in> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) \<or>
t \<in> SMP ((subterms\<^sub>s\<^sub>e\<^sub>t M \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M)) - M)"
(is "?P t \<or> ?Q t")
using assms(1)
proof (induction t rule: SMP.induct)
case (MP t)
have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range Var)" "M \<cdot>\<^sub>s\<^sub>e\<^sub>t Var = M" by simp_all
thus ?case using MP by metis
next
case (Subterm t t')
show ?case using Subterm.IH
proof
assume "?P t"
then obtain s \<delta> where s: "s \<in> M" "t = s \<cdot> \<delta>" and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" by moura
then obtain f T where fT: "s = Fun f T" using M by fast
have "(\<exists>s'. s' \<sqsubseteq> s \<and> t' = s' \<cdot> \<delta>) \<or> (\<exists>x \<in> fv s. t' \<sqsubset> \<delta> x)"
using subterm_subst_unfold[OF Subterm.hyps(2)[unfolded s(2)]] by blast
thus ?thesis
proof
assume "\<exists>s'. s' \<sqsubseteq> s \<and> t' = s' \<cdot> \<delta>"
then obtain s' where s': "s' \<sqsubseteq> s" "t' = s' \<cdot> \<delta>" by moura
show ?thesis
proof (cases "s' \<in> M")
case True thus ?thesis using s' \<delta> by blast
next
case False
hence "s' \<in> (subterms\<^sub>s\<^sub>e\<^sub>t M \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M)) - M" using s'(1) s(1) by force
thus ?thesis using SMP.Substitution[OF SMP.MP[of s'] \<delta>] s' by presburger
qed
next
assume "\<exists>x \<in> fv s. t' \<sqsubset> \<delta> x"
then obtain x where x: "x \<in> fv s" "t' \<sqsubset> \<delta> x" by moura
have "Var x \<notin> M" using M by blast
hence "Var x \<in> (subterms\<^sub>s\<^sub>e\<^sub>t M \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M)) - M"
using s(1) var_is_subterm[OF x(1)] by blast
hence "\<delta> x \<in> SMP ((subterms\<^sub>s\<^sub>e\<^sub>t M \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M)) - M)"
using SMP.Substitution[OF SMP.MP[of "Var x"] \<delta>] by auto
thus ?thesis using SMP.Subterm x(2) by presburger
qed
qed (metis SMP.Subterm[OF _ Subterm.hyps(2)])
next
case (Substitution t \<delta>)
show ?case using Substitution.IH
proof
assume "?P t"
then obtain \<theta> where "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "t \<in> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" by moura
using wt_subst_compose[of \<theta>, OF _ Substitution.hyps(2)]
wf_trm_subst_compose[of \<theta> _ \<delta>, OF _ wf_trm_subst_rangeD[OF Substitution.hyps(3)]]
wf_trm_subst_range_iff
by (argo, blast, auto)
thus ?thesis by blast
next
assume "?Q t" thus ?thesis using SMP.Substitution[OF _ Substitution.hyps(2,3)] by meson
qed
next
case (Ana t K T k)
show ?case using Ana.IH
proof
assume "?P t"
then obtain \<theta> where \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "t \<in> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" by moura
then obtain s where s: "s \<in> M" "t = s \<cdot> \<theta>" by auto
then obtain f S where fT: "s = Fun f S" using M by (cases s) auto
obtain K' T' where s_Ana: "Ana s = (K', T')" by (metis surj_pair)
hence "set K = set K' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" "set T = set T' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
using Ana_subst'[of f S K' T'] fT Ana.hyps(2) s(2) by auto
then obtain k' where k': "k' \<in> set K'" "k = k' \<cdot> \<theta>" using Ana.hyps(3) by fast
show ?thesis
proof (cases "k' \<in> M")
case True thus ?thesis using k' \<theta>(1,2) by blast
next
case False
hence "k' \<in> (subterms\<^sub>s\<^sub>e\<^sub>t M \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M)) - M" using k'(1) s_Ana s(1) by force
thus ?thesis using SMP.Substitution[OF SMP.MP[of k'] \<theta>(1,2)] k'(2) by presburger
qed
next
assume "?Q t" thus ?thesis using SMP.Ana[OF _ Ana.hyps(2,3)] by meson
and "\<forall>s \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t S. \<forall>t \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t S. (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t"
and "\<forall>s \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t S. \<forall>t \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t S.
Unifier \<rho> (s \<cdot> \<sigma>) (t \<cdot> \<theta>))
\<longrightarrow> (\<exists>\<delta>. Unifier \<delta> s t)"
and tfr: "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)"
shows "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t S)"
proof -
have 0: "t \<in> SMP (trms\<^sub>s\<^sub>s\<^sub>t S) - range Var \<or> t \<in> SMP (pair ` setops\<^sub>s\<^sub>s\<^sub>t S) - range Var"
when "t \<in> SMP (trms\<^sub>s\<^sub>s\<^sub>t S \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t S) - range Var" for t
using that SMP_union by blast
have 1: "s \<in> SMP (trms\<^sub>s\<^sub>s\<^sub>t S) - range Var"
when st: "s \<in> SMP (pair ` setops\<^sub>s\<^sub>s\<^sub>t S) - range Var"
"t \<in> SMP (trms\<^sub>s\<^sub>s\<^sub>t S) - range Var"
"\<exists>\<delta>. Unifier \<delta> s t"
for s t
proof -
have "(\<exists>\<delta>. s \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t S \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) \<or> s \<in> SMP (trms\<^sub>s\<^sub>s\<^sub>t S) - range Var"
using st setops_SMP_cases[of s S] assms(2) by blast
(\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}) \<and> fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {})"
have "P D A" using assms(1,4) by (simp add: P_def)
with assms(5,3,2) show ?thesis
proof (induction A arbitrary: A' D X rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct)
case 1 thus ?case by simp
next
case (2 X t A A')
then obtain A'' where A'': "A' = receive\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)" "fv t \<subseteq> X"
by moura
have *: "wf'\<^sub>s\<^sub>s\<^sub>t X A" "\<forall>(s,s') \<in> set D. fv s \<union> fv s' \<subseteq> X" "P D A"
using 2(1,2,3,4) apply (force, force)
using 2(5) unfolding P_def by force
show ?case using "2.IH"[OF A''(2) *] A''(1,3) by simp
next
case (3 X t A A')
then obtain A'' where A'': "A' = send\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)"
by moura
have *: "wf'\<^sub>s\<^sub>s\<^sub>t (X \<union> fv t) A" "\<forall>(s,s') \<in> set D. fv s \<union> fv s' \<subseteq> X \<union> fv t" "P D A"
using 3(1,2,3,4) apply (force, force)
using 3(5) unfolding P_def by force
show ?case using "3.IH"[OF A''(2) *] A''(1) by simp
next
case (4 X t t' A A')
then obtain A'' where A'': "A' = \<langle>assign: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)" "fv t' \<subseteq> X"
by moura
have *: "wf'\<^sub>s\<^sub>s\<^sub>t (X \<union> fv t) A" "\<forall>(s,s') \<in> set D. fv s \<union> fv s' \<subseteq> X \<union> fv t" "P D A"
using 4(1,2,3,4) apply (force, force)
using 4(5) unfolding P_def by force
show ?case using "4.IH"[OF A''(2) *] A''(1,3) by simp
next
case (5 X t t' A A')
then obtain A'' where A'': "A' = \<langle>check: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)"
by moura
have *: "wf'\<^sub>s\<^sub>s\<^sub>t X A" "P D A"
using 5(3) apply force
using 5(5) unfolding P_def by force
show ?case using "5.IH"[OF A''(2) *(1) 5(4) *(2)] A''(1) by simp
next
case (6 X t s A A')
hence A': "A' \<in> set (tr A (List.insert (t,s) D))" "fv t \<subseteq> X" "fv s \<subseteq> X" by auto
have *: "wf'\<^sub>s\<^sub>s\<^sub>t X A" "\<forall>(s,s') \<in> set (List.insert (t,s) D). fv s \<union> fv s' \<subseteq> X" using 6 by auto
have **: "P (List.insert (t,s) D) A" using 6(5) unfolding P_def by force
show ?case using "6.IH"[OF A'(1) * **] A'(2,3) by simp
have *: "wf'\<^sub>s\<^sub>s\<^sub>t (X \<union> fv t \<union> fv s) A" "\<forall>(t',s')\<in>set D. fv t' \<union> fv s' \<subseteq> X \<union> fv t \<union> fv s" "P D A"
using 8(1,2,3,4) apply (force, force)
using 8(5) unfolding P_def by force
have **: "fv (pair d) \<subseteq> X" using A''(3) "8.prems"(3) unfolding pair_def by fastforce
have ***: "fv (pair (t,s)) = fv s \<union> fv t" unfolding pair_def by auto
show ?case using "8.IH"[OF A''(2) *] A''(1) ** *** unfolding pair_def by (simp add: Un_assoc)
have **: "fv (pair d) \<subseteq> X" using A''(3) "9.prems"(3) unfolding pair_def by fastforce
have ***: "fv (pair (t,s)) = fv s \<union> fv t" unfolding pair_def by auto
show ?case using "9.IH"[OF A''(2) *(1) 9(4) *(2)] A''(1) ** *** by (simp add: Un_assoc)
next
case (10 X Y F F' A A')
from 10 obtain A'' where A'':
"A' = (map (\<lambda>G. \<forall>Y\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))@A''" "A'' \<in> set (tr A D)"
by moura
have *: "wf'\<^sub>s\<^sub>s\<^sub>t X A" "\<forall>(t',s') \<in> set D. fv t' \<union> fv s' \<subseteq> X" using 10 by auto
have "bvars\<^sub>s\<^sub>s\<^sub>t A \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t (\<forall>Y\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>#A)" "fv\<^sub>s\<^sub>s\<^sub>t A \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (\<forall>Y\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>#A)" by auto
hence **: "P D A" using 10 unfolding P_def by blast
show ?case using "10.IH"[OF A''(2) * **] A''(1) wf_fun_pair_negchecks_map by simp
assumes "A' \<in> set (tr A D)" "list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p A"
and "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" (is "?P0 A D")
and "\<forall>(t,s) \<in> set D. (fv t \<union> fv s) \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" (is "?P1 A D")
and "\<forall>t \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D. \<forall>t' \<in> pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set D.
(\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t'" (is "?P3 A D")
shows "list_all tfr\<^sub>s\<^sub>t\<^sub>p A'"
proof -
have sublmm: "list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p A" "?P0 A D" "?P1 A D" "?P3 A D"
using p(1) apply (simp add: tfr\<^sub>s\<^sub>s\<^sub>t_def)
using p(2) fv\<^sub>s\<^sub>s\<^sub>t_cons_subset bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset apply fast
using p(3) bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset apply fast
using p(4) setops\<^sub>s\<^sub>s\<^sub>t_cons_subset by fast
show ?thesis using assms
proof (induction A D arbitrary: A' rule: tr.induct)
case 1 thus ?case by simp
next
case (2 t A D)
note prems = "2.prems"
note IH = "2.IH"
from prems(1) obtain A'' where A'': "A' = send\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)"
by moura
have "list_all tfr\<^sub>s\<^sub>t\<^sub>p A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
thus ?case using A''(1) by simp
next
case (3 t A D)
note prems = "3.prems"
note IH = "3.IH"
from prems(1) obtain A'' where A'': "A' = receive\<langle>t\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)"
by moura
have "list_all tfr\<^sub>s\<^sub>t\<^sub>p A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
thus ?case using A''(1) by simp
next
case (4 ac t t' A D)
note prems = "4.prems"
note IH = "4.IH"
from prems(1) obtain A'' where A'':
"A' = \<langle>ac: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#A''" "A'' \<in> set (tr A D)"
by moura
have "list_all tfr\<^sub>s\<^sub>t\<^sub>p A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
moreover have "(\<exists>\<delta>. Unifier \<delta> t t') \<Longrightarrow> \<Gamma> t = \<Gamma> t'" using prems(2) by (simp add: tfr\<^sub>s\<^sub>s\<^sub>t_def)
ultimately show ?case using A''(1) by auto
next
case (5 t s A D)
note prems = "5.prems"
note IH = "5.IH"
from prems(1) have A': "A' \<in> set (tr A (List.insert (t,s) D))" by simp
have 1: "list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p A" using sublmm[OF prems(2,3,4,5)] by simp
have "pair ` setops\<^sub>s\<^sub>s\<^sub>t (Insert t s#A) \<union> pair`set D =
pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair`set (List.insert (t,s) D)"
by (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
hence 3: "?P3 A (List.insert (t,s) D)" using prems(5) by metis
moreover have "?P1 A (List.insert (t, s) D)" using prems(3,4) bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset[of A] by auto
ultimately have "list_all tfr\<^sub>s\<^sub>t\<^sub>p A'" using IH[OF A' sublmm(1,2)[OF prems(2,3,4,5)] _ 3] by metis
define Q2 where "Q2 \<equiv> (\<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))"
have "set [d\<leftarrow>D. d \<notin> set Di] \<subseteq> set D"
"pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` set [d\<leftarrow>D. d \<notin> set Di]
\<subseteq> pair ` setops\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) \<union> pair ` set D"
by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
hence *: "?P3 A [d\<leftarrow>D. d \<notin> set Di]" using prems(5) by blast
have **: "?P1 A [d\<leftarrow>D. d \<notin> set Di]" using prems(4,5) by auto
have 1: "list_all tfr\<^sub>s\<^sub>t\<^sub>p A''"
using IH[OF A''(3,2) sublmm(1,2)[OF prems(2,3,4,5)] ** *]
by metis
have 2: "\<langle>ac: u \<doteq> u'\<rangle>\<^sub>s\<^sub>t \<in> set A'' \<or>
(\<exists>d \<in> set Di. u = pair (t,s) \<and> u' = pair d)"
when "\<langle>ac: u \<doteq> u'\<rangle>\<^sub>s\<^sub>t \<in> set A'" for ac u u'
using that A''(1) unfolding constr by force
have 3: "Inequality X U \<in> set A' \<Longrightarrow> Inequality X U \<in> set A'' \<or>
(\<exists>d \<in> set [d\<leftarrow>D. d \<notin> set Di].
define Q2 where "Q2 \<equiv> (\<lambda>(M::('fun,'var) terms) X.
\<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X))"
have Q2_subset: "Q2 M' X" when "M' \<subseteq> M" "Q2 M X" for X M M'
using that unfolding Q2_def by auto
have Q2_supset: "Q2 (M \<union> M') X" when "Q2 M X" "Q2 M' X" for X M M'
using that unfolding Q2_def by auto
from prems(1) obtain A'' where A'': "A' = constr@A''" "A'' \<in> set (tr A D)"
using constr_def by moura
have 0: "F' = [] \<Longrightarrow> constr = [\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]" unfolding constr_def by simp
have 1: "list_all tfr\<^sub>s\<^sub>t\<^sub>p A''"
using IH[OF A''(2) sublmm(1,2,3)[OF prems(2,3,4,5)] sublmm(4)[OF prems(2,3,4,5)]]
by metis
have 2: "(F' = [] \<and> Q1 F X) \<or> Q2 (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> pair ` set F') X"
using prems(2) unfolding Q1_def Q2_def by simp
have 3: "list_all tfr\<^sub>s\<^sub>t\<^sub>p constr" when "F' = []" "Q1 F X"
using that 0 2 tfr\<^sub>s\<^sub>t\<^sub>p_list_all_alt_def[of constr] unfolding Q1_def by auto
{ fix c assume "c \<in> set constr"
hence "\<exists>G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D). c = \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t" unfolding constr_def by force
} moreover {
fix G
assume G: "G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D)"
and c: "\<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t \<in> set constr"
and e: "Q2 (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> pair ` set F') X"
have d_Q2: "Q2 (pair ` set D) X" unfolding Q2_def
proof (intro allI impI)
fix f T assume "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (pair ` set D)"
then obtain d where d: "d \<in> set D" "Fun f T \<in> subterms (pair d)" by auto
hence "fv (pair d) \<inter> set X = {}" using prems(4) unfolding pair_def by force
thus "T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)"
by (metis fv_disj_Fun_subterm_param_cases d(2))
qed
have "trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@G) \<subseteq> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> pair ` set F' \<union> pair ` set D"
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_trms_subset[OF G] by auto
hence "Q2 (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@G)) X" using Q2_subset[OF _ Q2_supset[OF e d_Q2]] by metis
hence "tfr\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t)" by (metis Q2_def tfr\<^sub>s\<^sub>t\<^sub>p.simps(2))
} ultimately have 4: "list_all tfr\<^sub>s\<^sub>t\<^sub>p constr" when "Q2 (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> pair ` set F') X"
using that Ball_set by blast
have 5: "list_all tfr\<^sub>s\<^sub>t\<^sub>p constr" using 2 3 4 by metis
show ?case using 1 5 A''(1) by simp
qed
qed
lemma tr_tfr:
assumes "A' \<in> set (tr A [])" and "tfr\<^sub>s\<^sub>s\<^sub>t A" and "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
shows "tfr\<^sub>s\<^sub>t A'"
proof -
have *: "trms\<^sub>s\<^sub>t A' \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A" using tr_trms_subset[OF assms(1)] by simp
hence "SMP (trms\<^sub>s\<^sub>t A') \<subseteq> SMP (trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A)" using SMP_mono by simp
moreover have "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A)" using assms(2) unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by fast
ultimately have 1: "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t A')" by (metis tfr_subset(2)[OF _ *])
have **: "list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p A" using assms(2) unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by fast
have "pair ` setops\<^sub>s\<^sub>s\<^sub>t A \<subseteq> SMP (trms\<^sub>s\<^sub>s\<^sub>t A \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t A) - Var`\<V>"
using setops\<^sub>s\<^sub>s\<^sub>t_are_pairs unfolding pair_def by auto
hence ***: "\<forall>t \<in> pair`setops\<^sub>s\<^sub>s\<^sub>t A. \<forall>t' \<in> pair`setops\<^sub>s\<^sub>s\<^sub>t A. (\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t'"
using assms(2) unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
have 2: "list_all tfr\<^sub>s\<^sub>t\<^sub>p A'"
using tr_tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p[OF assms(1) ** assms(3)] *** unfolding pair_def by fastforce
show ?thesis by (metis 1 2 tfr\<^sub>s\<^sub>t_def)
qed
private lemma fun_pair_ineqs:
assumes "d \<cdot>\<^sub>p \<delta> \<cdot>\<^sub>p \<theta> \<noteq> d' \<cdot>\<^sub>p \<I>"
shows "pair d \<cdot> \<delta> \<cdot> \<theta> \<noteq> pair d' \<cdot> \<I>"
proof -
have "d \<cdot>\<^sub>p (\<delta> \<circ>\<^sub>s \<theta>) \<noteq> d' \<cdot>\<^sub>p \<I>" using assms subst_pair_compose by metis
hence "pair d \<cdot> (\<delta> \<circ>\<^sub>s \<theta>) \<noteq> pair d' \<cdot> \<I>" using fun_pair_eq_subst by metis
thus ?thesis by simp
qed
private lemma tr_Delete_constr_iff_aux1:
assumes "\<forall>d \<in> set Di. (t,s) \<cdot>\<^sub>p \<I> = d \<cdot>\<^sub>p \<I>"
and "\<forall>d \<in> set D - set Di. (t,s) \<cdot>\<^sub>p \<I> \<noteq> d \<cdot>\<^sub>p \<I>"
(map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>D. d \<notin> set Di])\<rbrakk>\<^sub>d \<I>"
proof -
from assms(2) have
"\<lbrakk>M; map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>D. d \<notin> set Di]\<rbrakk>\<^sub>d \<I>"
proof (induction D)
case (Cons d D)
hence IH: "\<lbrakk>M; map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>D . d \<notin> set Di]\<rbrakk>\<^sub>d \<I>" by auto
thus ?case
proof (cases "d \<in> set Di")
case False
hence "(t,s) \<cdot>\<^sub>p \<I> \<noteq> d \<cdot>\<^sub>p \<I>" using Cons by simp
hence "pair (t,s) \<cdot> \<I> \<noteq> pair d \<cdot> \<I>" using fun_pair_eq_subst by metis
moreover have "\<And>t (\<delta>::('fun,'var) subst). subst_domain \<delta> = {} \<Longrightarrow> t \<cdot> \<delta> = t" by auto
ultimately have "\<forall>\<delta>. subst_domain \<delta> = {} \<longrightarrow> pair (t,s) \<cdot> \<delta> \<cdot> \<I> \<noteq> pair d \<cdot> \<delta> \<cdot> \<I>" by metis
thus ?thesis using IH by (simp add: ineq_model_def)
qed simp
qed simp
moreover {
fix B assume "\<lbrakk>M; B\<rbrakk>\<^sub>d \<I>"
with assms(1) have "\<lbrakk>M; (map (\<lambda>d. \<langle>check: (pair (t,s)) \<doteq> (pair d)\<rangle>\<^sub>s\<^sub>t) Di)@B\<rbrakk>\<^sub>d \<I>"
(map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>D. d \<notin> set Di])\<rbrakk>\<^sub>d \<I>"
shows "(\<forall>d \<in> set Di. (t,s) \<cdot>\<^sub>p \<I> = d \<cdot>\<^sub>p \<I>) \<and> (\<forall>d \<in> set D - set Di. (t,s) \<cdot>\<^sub>p \<I> \<noteq> d \<cdot>\<^sub>p \<I>)"
(map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>D. d \<notin> set Di])"
{ assume "set Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {(t,s) \<cdot>\<^sub>p \<I>}" "(t,s) \<cdot>\<^sub>p \<I> \<notin> (set D - set Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
hence "\<forall>d \<in> set Di. (t,s) \<cdot>\<^sub>p \<I> = d \<cdot>\<^sub>p \<I>" "\<forall>d \<in> set D - set Di. (t,s) \<cdot>\<^sub>p \<I> \<noteq> d \<cdot>\<^sub>p \<I>"
by auto
hence "\<lbrakk>M; ?constr\<rbrakk>\<^sub>d \<I>" using tr_Delete_constr_iff_aux1 by simp
hence "\<forall>d \<in> set Di. (t,s) \<cdot>\<^sub>p \<I> = d \<cdot>\<^sub>p \<I>" "\<forall>d \<in> set D - set Di. (t,s) \<cdot>\<^sub>p \<I> \<noteq> d \<cdot>\<^sub>p \<I>"
using assms tr_Delete_constr_iff_aux2 by auto
hence "set Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {(t,s) \<cdot>\<^sub>p \<I>} \<and> (t,s) \<cdot>\<^sub>p \<I> \<notin> (set D - set Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>" by force
} ultimately show ?thesis by metis
qed
private lemma tr_NotInSet_constr_iff:
fixes \<I>::"('fun,'var) subst"
assumes "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> set X = {}"
shows "(\<forall>\<delta>. subst_domain \<delta> = set X \<and> ground (subst_range \<delta>) \<longrightarrow> (t,s) \<cdot>\<^sub>p \<delta> \<cdot>\<^sub>p \<I> \<notin> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>)
using Cons d by (auto simp add: ineq_model_def simp del: subst_range.simps)
moreover have "pair d \<cdot> \<delta> = pair d"
using Cons.prems(1) fun_pair_subst[of d \<delta>] d \<delta>(1) unfolding pair_def by auto
ultimately show ?case unfolding pair_def by force
qed simp
} ultimately show ?thesis by metis
qed
lemma tr_NegChecks_constr_iff:
"(\<forall>G\<in>set L. ineq_model \<I> X (F@G)) \<longleftrightarrow> \<lbrakk>M; map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) L\<rbrakk>\<^sub>d \<I>" (is ?A)
"negchecks_model \<I> D X F F' \<longleftrightarrow> \<lbrakk>M; D; [\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>]\<rbrakk>\<^sub>s \<I>" (is ?B)
assumes "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> set X = {}"
shows "negchecks_model \<I> (set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) X F F' \<longleftrightarrow>
(\<forall>G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D). ineq_model \<I> X (F@G))"
proof -
define P where
"P \<equiv> \<lambda>\<delta>::('fun,'var) subst. subst_domain \<delta> = set X \<and> ground (subst_range \<delta>)"
define Ineq where
"Ineq \<equiv> \<lambda>(\<delta>::('fun,'var) subst) F. list_ex (\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> snd f \<cdot> \<delta> \<circ>\<^sub>s \<I>) F"
define Ineq' where
"Ineq' \<equiv> \<lambda>(\<delta>::('fun,'var) subst) F. list_ex (\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> snd f \<cdot> \<I>) F"
define Notin where
"Notin \<equiv> \<lambda>(\<delta>::('fun,'var) subst) D F'. list_ex (\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) F'"
have sublmm:
"((s,t) \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) \<longleftrightarrow> (list_all (\<lambda>d. Ineq' \<delta> [(pair (s,t),pair d)]) D)"
for s t \<delta> D
unfolding pair_def by (induct D) (auto simp add: Ineq'_def)
have "Notin \<delta> D F' \<longleftrightarrow> (\<forall>G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D). Ineq' \<delta> G)"
(is "?A \<longleftrightarrow> ?B")
when "P \<delta>" for \<delta>
proof
show "?A \<Longrightarrow> ?B"
proof (induction F' D rule: tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s.induct)
case (2 s t F' D)
show ?case
proof (cases "Notin \<delta> D F'")
case False
hence "(s,t) \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using "2.prems"
by (auto simp add: Notin_def)
hence "pair (s,t) \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> pair d \<cdot> \<I>" when "d \<in> set D" for d
using that sublmm Ball_set[of D "\<lambda>d. Ineq' \<delta> [(pair (s,t), pair d)]"]
by (simp add: Ineq'_def)
moreover have "\<exists>d \<in> set D. \<exists>G'. G = (pair (s,t), pair d)#G'"
when "G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ((s,t)#F') D)" for G
using that tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_index[OF that, of 0] by force
ultimately show ?thesis by (simp add: Ineq'_def)
qed (auto dest: "2.IH" simp add: Ineq'_def)
qed (simp add: Notin_def)
have "\<not>?A \<Longrightarrow> \<not>?B"
proof (induction F' D rule: tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s.induct)
case (2 s t F' D)
then obtain G where G: "G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D)" "\<not>Ineq' \<delta> G"
by (auto simp add: Notin_def)
obtain d where d: "d \<in> set D" "pair (s,t) \<cdot> \<delta> \<circ>\<^sub>s \<I> = pair d \<cdot> \<I>"
using "2.prems"
unfolding pair_def by (auto simp add: Notin_def)
thus ?case
using G(2) tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_cons[OF G(1) d(1)]
by (auto simp add: Ineq'_def)
qed (simp add: Ineq'_def)
thus "?B \<Longrightarrow> ?A" by metis
qed
hence *: "(\<forall>\<delta>. P \<delta> \<longrightarrow> Ineq \<delta> F \<or> Notin \<delta> D F') \<longleftrightarrow>
(\<forall>G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D). \<forall>\<delta>. P \<delta> \<longrightarrow> Ineq \<delta> F \<or> Ineq' \<delta> G)"
by auto
have "snd g \<cdot> \<delta> = snd g"
when "G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D)" "g \<in> set G" "P \<delta>"
for \<delta> g G
using assms that(3) tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_has_pair_lists[OF that(1,2)]
unfolding pair_def by (fastforce simp add: P_def)
hence **: "Ineq' \<delta> G = Ineq \<delta> G"
when "G \<in> set (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D)" "P \<delta>"
for \<delta> G
using Bex_set[of G "\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> snd f \<cdot> \<I>"]
Bex_set[of G "\<lambda>f. fst f \<cdot> \<delta> \<circ>\<^sub>s \<I> \<noteq> snd f \<cdot> \<delta> \<circ>\<^sub>s \<I>"]
that
by (simp add: Ineq_def Ineq'_def)
show ?thesis
using * **
by (simp add: Ineq_def Ineq'_def Notin_def P_def negchecks_model_def ineq_model_def)
qed
lemma tr_sem_equiv':
assumes "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
and "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
and "ground M"
and \<I>: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
shows "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I> \<longleftrightarrow> (\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>)" (is "?P \<longleftrightarrow> ?Q")
proof
have \<I>_grounds: "\<And>t. fv (t \<cdot> \<I>) = {}" by (rule interpretation_grounds[OF \<I>])
have "\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>" when ?P using that assms(1,2,3)
proof (induction A arbitrary: D rule: strand_sem_stateful_induct)
case (ConsRcv M D t A)
have "\<lbrakk>insert (t \<cdot> \<I>) M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground (insert (t \<cdot> \<I>) M)"
using \<I> ConsRcv.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
then obtain A' where A': "A' \<in> set (tr A D)" "\<lbrakk>insert (t \<cdot> \<I>) M; A'\<rbrakk>\<^sub>d \<I>" by (metis ConsRcv.IH)
thus ?case by auto
next
case (ConsSnd M D t A)
have "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "M \<turnstile> t \<cdot> \<I>"
using \<I> ConsSnd.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
then obtain A' where A': "A' \<in> set (tr A D)" "\<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>" by (metis ConsSnd.IH)
thus ?case using * by auto
next
case (ConsEq M D ac t t' A)
have "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "t \<cdot> \<I> = t' \<cdot> \<I>"
using \<I> ConsEq.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
then obtain A' where A': "A' \<in> set (tr A D)" "\<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>" by (metis ConsEq.IH)
thus ?case using * by auto
next
case (ConsIns M D t s A)
have "\<lbrakk>M; set (List.insert (t,s) D) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t') \<in> set (List.insert (t,s) D). (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
using ConsIns.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
then obtain A' where A': "A' \<in> set (tr A (List.insert (t,s) D))" "\<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>"
by (metis ConsIns.IH)
thus ?case by auto
next
case (ConsDel M D t s A)
have *: "\<lbrakk>M; (set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) - {(t,s) \<cdot>\<^sub>p \<I>}; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t')\<in>set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
using ConsDel.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
using constr_sat A'(2) subst_all_ground_ident[OF *(4)] by simp_all
ultimately show ?case
using strand_sem_append(2)[of _ _ \<I>]
subst_all_ground_ident[OF *(4), of \<I>]
by metis
next
case (ConsIn M D ac t s A)
have "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "(t,s) \<cdot>\<^sub>p \<I> \<in> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using \<I> ConsIn.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
then obtain A' where A': "A' \<in> set (tr A D)" "\<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>" by (metis ConsIn.IH)
moreover obtain d where "d \<in> set D" "pair (t,s) \<cdot> \<I> = pair d \<cdot> \<I>"
using * unfolding pair_def by auto
ultimately show ?case using * by auto
next
case (ConsNegChecks M D X F F' A)
let ?ineqs = "(map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))"
have 1: "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" "ground M" using ConsNegChecks by auto
have 2: "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
using ConsNegChecks.prems(2,3) \<I> unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by fastforce+
have 3: "negchecks_model \<I> (set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) X F F'" using ConsNegChecks.prems(1) by simp
from 1 2 obtain A' where A': "A' \<in> set (tr A D)" "\<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>" by (metis ConsNegChecks.IH)
have 4: "\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> set X = {}"
using ConsNegChecks.prems(2) unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def by auto
have "\<lbrakk>M; ?ineqs\<rbrakk>\<^sub>d \<I>"
using 3 tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_sem_equiv[OF 4] tr_NegChecks_constr_iff
by metis
moreover have "ik\<^sub>s\<^sub>t ?ineqs = {}" by auto
moreover have "M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> = M" using 1(2) \<I> by (simp add: subst_all_ground_ident)
ultimately show ?case
using strand_sem_append(2)[of M ?ineqs \<I> A'] A'
by force
qed simp
thus "?P \<Longrightarrow> ?Q" by metis
have "(\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>) \<Longrightarrow> ?P" using assms(1,2,3)
proof (induction A arbitrary: D rule: strand_sem_stateful_induct)
case (ConsRcv M D t A)
have "\<exists>A' \<in> set (tr A D). \<lbrakk>insert (t \<cdot> \<I>) M; A'\<rbrakk>\<^sub>d \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground (insert (t \<cdot> \<I>) M)"
using \<I> ConsRcv.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
hence "\<lbrakk>insert (t \<cdot> \<I>) M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" by (metis ConsRcv.IH)
thus ?case by auto
next
case (ConsSnd M D t A)
have "\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "M \<turnstile> t \<cdot> \<I>"
using \<I> ConsSnd.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
hence "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" by (metis ConsSnd.IH)
thus ?case using * by auto
next
case (ConsEq M D ac t t' A)
have "\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "t \<cdot> \<I> = t' \<cdot> \<I>"
using \<I> ConsEq.prems unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
hence "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" by (metis ConsEq.IH)
thus ?case using * by auto
next
case (ConsIns M D t s A)
hence "\<exists>A' \<in> set (tr A (List.insert (t,s) D)). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>"
"\<forall>(t,t') \<in> set (List.insert (t,s) D). (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by auto+
hence "\<lbrakk>M; set (List.insert (t,s) D) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" by (metis ConsIns.IH)
show "(set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) - {((t,s) \<cdot>\<^sub>p \<I>)} \<subseteq> set (?flt Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using * subseqs_set_subset[OF A'(3)] by force
qed
show ?case using 4 IH by simp
next
case (ConsIn M D ac t s A)
have "\<exists>A' \<in> set (tr A D). \<lbrakk>M; A'\<rbrakk>\<^sub>d \<I>"
"\<forall>(t,t') \<in> set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
"fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "ground M"
and *: "(t,s) \<cdot>\<^sub>p \<I> \<in> set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using ConsIn.prems(1,2,3,4) apply (fastforce, fastforce, fastforce, fastforce)
using ConsIn.prems(1) tr.simps(7)[of ac t s A D] unfolding pair_def by fastforce
hence "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>" by (metis ConsIn.IH)
moreover obtain d where "d \<in> set D" "pair (t,s) \<cdot> \<I> = pair d \<cdot> \<I>"
using * unfolding pair_def by auto
ultimately show ?case using * by auto
next
case (ConsNegChecks M D X F F' A)
let ?ineqs = "(map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' D))"
obtain B where B:
"?ineqs@B \<in> set (tr (NegChecks X F F'#A) D)" "\<lbrakk>M; ?ineqs@B\<rbrakk>\<^sub>d \<I>" "B \<in> set (tr A D)"
using ConsNegChecks.prems(1) by moura
moreover have "M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> = M"
using ConsNegChecks.prems(4) \<I> by (simp add: subst_all_ground_ident)
moreover have "ik\<^sub>s\<^sub>t ?ineqs = {}" by auto
ultimately have "\<lbrakk>M; B\<rbrakk>\<^sub>d \<I>" using strand_sem_split(4)[of M ?ineqs B \<I>] by simp
moreover have "\<forall>(t,t')\<in>set D. (fv t \<union> fv t') \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
using ConsNegChecks.prems(2,3) unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by force+
ultimately have "\<lbrakk>M; set D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>; A\<rbrakk>\<^sub>s \<I>"
by (metis ConsNegChecks.IH B(3) ConsNegChecks.prems(4))
moreover have "\<forall>(t, t')\<in>set D. (fv t \<union> fv t') \<inter> set X = {}"
using ConsNegChecks.prems(2) unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def by force
ultimately show ?case
using tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_sem_equiv tr_NegChecks_constr_iff
B(2) strand_sem_split(3)[of M ?ineqs B \<I>] \<open>M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> = M\<close>
by simp
qed simp
thus "?Q \<Longrightarrow> ?P" by metis
qed
lemma tr_sem_equiv:
assumes "fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}" and "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
shows "\<I> \<Turnstile>\<^sub>s A \<longleftrightarrow> (\<exists>A' \<in> set (tr A []). (\<I> \<Turnstile> \<langle>A'\<rangle>))"
using tr_sem_equiv'[OF _ assms(1) _ assms(2), of "[]" "{}"]
unfolding constr_sem_d_def
by auto
theorem stateful_typing_result:
assumes "wf\<^sub>s\<^sub>s\<^sub>t \<A>"
and "tfr\<^sub>s\<^sub>s\<^sub>t \<A>"
and "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t \<A>)"
and "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
and "\<I> \<Turnstile>\<^sub>s \<A>"
obtains \<I>\<^sub>\<tau>
where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>"
and "\<I>\<^sub>\<tau> \<Turnstile>\<^sub>s \<A>"
and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>"
and "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>)"
proof -
obtain \<A>' where \<A>':
"\<A>' \<in> set (tr \<A> [])" "\<I> \<Turnstile> \<langle>\<A>'\<rangle>"
assumes "comp_tfr\<^sub>s\<^sub>s\<^sub>t arity Ana \<Gamma> Pair M S"
shows "tfr\<^sub>s\<^sub>s\<^sub>t S"
unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def
proof
have comp_tfr\<^sub>s\<^sub>e\<^sub>t_M: "comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> M"
using assms unfolding comp_tfr\<^sub>s\<^sub>s\<^sub>t_def by blast
have wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
and wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_S: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t S \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t S)"
and S_trms_instance_M: "has_all_wt_instances_of \<Gamma> (trms\<^sub>s\<^sub>s\<^sub>t S \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t S) (set M)"
using assms setops\<^sub>s\<^sub>s\<^sub>t_wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s(2)[of S] trms_list\<^sub>s\<^sub>s\<^sub>t_is_trms\<^sub>s\<^sub>s\<^sub>t[of S]