# Theory Stateful_Compositionality

```(*  Title:      Stateful_Compositionality.thy
Author:     Andreas Viktor Hess, DTU
*)

section ‹Stateful Protocol Compositionality›

theory Stateful_Compositionality
imports Stateful_Typing Parallel_Compositionality Labeled_Stateful_Strands
begin

subsection ‹Small Lemmata›
lemma (in typed_model) wt_subst_sstp_vars_type_subset:
fixes a::"('fun,'var) stateful_strand_step"
assumes "wt⇩s⇩u⇩b⇩s⇩t δ"
and "∀t ∈ subst_range δ. fv t = {} ∨ (∃x. t = Var x)"
shows "Γ ` Var ` fv⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ) ⊆ Γ ` Var ` fv⇩s⇩s⇩t⇩p a" (is ?A)
and "Γ ` Var ` set (bvars⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ)) = Γ ` Var ` set (bvars⇩s⇩s⇩t⇩p a)" (is ?B)
and "Γ ` Var ` vars⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ) ⊆ Γ ` Var ` vars⇩s⇩s⇩t⇩p a" (is ?C)
proof -
show ?A
proof
fix τ assume τ: "τ ∈ Γ ` Var ` fv⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ)"
then obtain x where x: "x ∈ fv⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ)" "Γ (Var x) = τ" by moura

show "τ ∈ Γ ` Var ` fv⇩s⇩s⇩t⇩p a"
proof (cases "x ∈ fv⇩s⇩s⇩t⇩p a")
case False
hence "∃y ∈ fv⇩s⇩s⇩t⇩p a. δ y = Var x"
proof (cases a)
case (NegChecks X F G)
hence *: "x ∈ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ) ∪ fv⇩p⇩a⇩i⇩r⇩s (G ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ)"
"x ∉ set X"
using fv⇩s⇩s⇩t⇩p_NegCheck(1)[of X "F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ" "G ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ"]
fv⇩s⇩s⇩t⇩p_NegCheck(1)[of X F G] False x(1)
by fastforce+

obtain y where y: "y ∈ fv⇩p⇩a⇩i⇩r⇩s F ∪ fv⇩p⇩a⇩i⇩r⇩s G" "x ∈ fv (rm_vars (set X) δ y)"
using fv⇩p⇩a⇩i⇩r⇩s_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
fv⇩p⇩a⇩i⇩r⇩s_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
*(1)
by blast

have "fv (rm_vars (set X) δ z) = {} ∨ (∃u. rm_vars (set X) δ z = Var u)" for z
using assms(2) rm_vars_img_subset[of "set X" δ] by blast
hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
hence "∃y ∈ fv⇩s⇩s⇩t⇩p a. rm_vars (set X) δ y = Var x"
using y fv⇩s⇩s⇩t⇩p_NegCheck(1)[of X F G] NegChecks *(2) by fastforce
thus ?thesis by (metis (full_types) *(2) term.inject(1))
qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
then obtain y where y: "y ∈ fv⇩s⇩s⇩t⇩p a" "δ y = Var x" by moura
hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wt⇩s⇩u⇩b⇩s⇩t_def)
thus ?thesis using y(1) by auto
qed (use x in auto)
qed

show ?B by (metis bvars⇩s⇩s⇩t⇩p_subst)

show ?C
proof
fix τ assume τ: "τ ∈ Γ ` Var ` vars⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ)"
then obtain x where x: "x ∈ vars⇩s⇩s⇩t⇩p (a ⋅⇩s⇩s⇩t⇩p δ)" "Γ (Var x) = τ" by moura

show "τ ∈ Γ ` Var ` vars⇩s⇩s⇩t⇩p a"
proof (cases "x ∈ vars⇩s⇩s⇩t⇩p a")
case False
hence "∃y ∈ vars⇩s⇩s⇩t⇩p a. δ y = Var x"
proof (cases a)
case (NegChecks X F G)
hence *: "x ∈ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ) ∪ fv⇩p⇩a⇩i⇩r⇩s (G ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ)"
"x ∉ set X"
using vars⇩s⇩s⇩t⇩p_NegCheck[of X "F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ" "G ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) δ"]
vars⇩s⇩s⇩t⇩p_NegCheck[of X F G] False x(1)
by (fastforce, blast)

obtain y where y: "y ∈ fv⇩p⇩a⇩i⇩r⇩s F ∪ fv⇩p⇩a⇩i⇩r⇩s G" "x ∈ fv (rm_vars (set X) δ y)"
using fv⇩p⇩a⇩i⇩r⇩s_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
fv⇩p⇩a⇩i⇩r⇩s_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
*(1)
by blast

have "fv (rm_vars (set X) δ z) = {} ∨ (∃u. rm_vars (set X) δ z = Var u)" for z
using assms(2) rm_vars_img_subset[of "set X" δ] by blast
hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
hence "∃y ∈ vars⇩s⇩s⇩t⇩p a. rm_vars (set X) δ y = Var x"
using y vars⇩s⇩s⇩t⇩p_NegCheck[of X F G] NegChecks by blast
thus ?thesis by (metis (full_types) *(2) term.inject(1))
qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
then obtain y where y: "y ∈ vars⇩s⇩s⇩t⇩p a" "δ y = Var x" by moura
hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wt⇩s⇩u⇩b⇩s⇩t_def)
thus ?thesis using y(1) by auto
qed (use x in auto)
qed
qed

lemma (in typed_model) wt_subst_lsst_vars_type_subset:
fixes A::"('fun,'var,'a) labeled_stateful_strand"
assumes "wt⇩s⇩u⇩b⇩s⇩t δ"
and "∀t ∈ subst_range δ. fv t = {} ∨ (∃x. t = Var x)"
shows "Γ ` Var ` fv⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ) ⊆ Γ ` Var ` fv⇩l⇩s⇩s⇩t A" (is ?A)
and "Γ ` Var ` bvars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ) = Γ ` Var ` bvars⇩l⇩s⇩s⇩t A" (is ?B)
and "Γ ` Var ` vars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ) ⊆ Γ ` Var ` vars⇩l⇩s⇩s⇩t A" (is ?C)
proof -
have "vars⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) = vars⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ) ∪ vars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"vars⇩l⇩s⇩s⇩t (a#A) = vars⇩s⇩s⇩t⇩p b ∪ vars⇩l⇩s⇩s⇩t A"
"fv⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) = fv⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ) ∪ fv⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"fv⇩l⇩s⇩s⇩t (a#A) = fv⇩s⇩s⇩t⇩p b ∪ fv⇩l⇩s⇩s⇩t A"
"bvars⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) = set (bvars⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ)) ∪ bvars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"bvars⇩l⇩s⇩s⇩t (a#A) = set (bvars⇩s⇩s⇩t⇩p b) ∪ bvars⇩l⇩s⇩s⇩t A"
when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
using that unlabel_Cons(1)[of l b A] unlabel_subst[of "a#A" δ]
subst_lsst_cons[of a A δ] subst_sst_cons[of b "unlabel A" δ]
subst_apply_labeled_stateful_strand_step.simps(1)[of l b δ]
vars⇩s⇩s⇩t_unlabel_Cons[of l b A] vars⇩s⇩s⇩t_unlabel_Cons[of l "b ⋅⇩s⇩s⇩t⇩p δ" "A ⋅⇩l⇩s⇩s⇩t δ"]
fv⇩s⇩s⇩t_unlabel_Cons[of l b A] fv⇩s⇩s⇩t_unlabel_Cons[of l "b ⋅⇩s⇩s⇩t⇩p δ" "A ⋅⇩l⇩s⇩s⇩t δ"]
bvars⇩s⇩s⇩t_unlabel_Cons[of l b A] bvars⇩s⇩s⇩t_unlabel_Cons[of l "b ⋅⇩s⇩s⇩t⇩p δ" "A ⋅⇩l⇩s⇩s⇩t δ"]
by simp_all
hence *: "Γ ` Var ` vars⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) =
Γ ` Var ` vars⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ) ∪ Γ ` Var ` vars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"Γ ` Var ` vars⇩l⇩s⇩s⇩t (a#A) = Γ ` Var ` vars⇩s⇩s⇩t⇩p b ∪ Γ ` Var ` vars⇩l⇩s⇩s⇩t A"
"Γ ` Var ` fv⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) =
Γ ` Var ` fv⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ) ∪ Γ ` Var ` fv⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"Γ ` Var ` fv⇩l⇩s⇩s⇩t (a#A) = Γ ` Var ` fv⇩s⇩s⇩t⇩p b ∪ Γ ` Var ` fv⇩l⇩s⇩s⇩t A"
"Γ ` Var ` bvars⇩l⇩s⇩s⇩t (a#A ⋅⇩l⇩s⇩s⇩t δ) =
Γ ` Var ` set (bvars⇩s⇩s⇩t⇩p (b ⋅⇩s⇩s⇩t⇩p δ)) ∪ Γ ` Var ` bvars⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
"Γ ` Var ` bvars⇩l⇩s⇩s⇩t (a#A) = Γ ` Var ` set (bvars⇩s⇩s⇩t⇩p b) ∪ Γ ` Var ` bvars⇩l⇩s⇩s⇩t A"
when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
using that by fast+

have "?A ∧ ?B ∧ ?C"
proof (induction A)
case (Cons a A)
obtain l b where a: "a = (l,b)" by (metis surj_pair)

show ?case
using Cons.IH wt_subst_sstp_vars_type_subset[OF assms, of b] *[OF a, of A]
by (metis Un_mono)
qed simp
thus ?A ?B ?C by metis+
qed

lemma (in stateful_typed_model) fv_pair_fv⇩p⇩a⇩i⇩r⇩s_subset:
assumes "d ∈ set D"
shows "fv (pair (snd d)) ⊆ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
using assms unfolding pair_def by (induct D) (auto simp add: unlabel_def)

lemma (in stateful_typed_model) labeled_sat_ineq_lift:
assumes "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t) [d←dbproj i D. d ∉ set Di]⟧⇩d ℐ"
(is "?R1 D")
and "∀(j,p) ∈ {(i,t,s)} ∪ set D ∪ set Di. ∀(k,q) ∈ {(i,t,s)} ∪ set D ∪ set Di.
(∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?R2 D")
shows "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t) [d←D. d ∉ set Di]⟧⇩d ℐ"
using assms
proof (induction D)
case (Cons dl D)
obtain d l where dl: "dl = (l,d)" by (metis surj_pair)

have 1: "?R1 D"
proof (cases "i = l")
case True thus ?thesis
using Cons.prems(1) dl by (cases "dl ∈ set Di") (auto simp add: dbproj_def)
next
case False thus ?thesis using Cons.prems(1) dl by (auto simp add: dbproj_def)
qed

have "set D ⊆ set (dl#D)" by auto
hence 2: "?R2 D" using Cons.prems(2) by blast

have "i ≠ l ∨ dl ∈ set Di ∨ ⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd dl))]⟩⇩s⇩t]⟧⇩d ℐ"
using Cons.prems(1) dl by (auto simp add: ineq_model_def dbproj_def)
moreover have "∃δ. Unifier δ (pair (t,s)) (pair d) ⟹ i = l"
using Cons.prems(2) dl by force
ultimately have 3: "dl ∈ set Di ∨ ⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd dl))]⟩⇩s⇩t]⟧⇩d ℐ"
using strand_sem_not_unif_is_sat_ineq[of "pair (t,s)" "pair d"] dl by fastforce

show ?case using Cons.IH[OF 1 2] 3 dl by auto
qed simp

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj:
assumes "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t) [d←D. d ∉ set Di]⟧⇩d ℐ"
(is "?P D")
shows "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t) [d←dbproj i D. d ∉ set Di]⟧⇩d ℐ"
(is "?Q D")
using assms
proof (induction D)
case (Cons di D)
obtain d j where di: "di = (j,d)" by (metis surj_pair)

have "?P D" using Cons.prems by (cases "di ∈ set Di") auto
hence IH: "?Q D" by (metis Cons.IH)

show ?case using di IH
proof (cases "i = j ∧ di ∉ set Di")
case True
have 1: "⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd di))]⟩⇩s⇩t]⟧⇩d ℐ"
using Cons.prems True by auto
have 2: "dbproj i (di#D) = di#dbproj i D" using True dbproj_Cons(1) di by auto
show ?thesis using 1 2 IH by auto
qed (auto simp add: dbproj_def)
qed (simp add: dbproj_def)

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj_sem_equiv:
assumes "∀(j,p) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D.
∀(k,q) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D.
(∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k"
and "fv⇩p⇩a⇩i⇩r⇩s (map snd D) ∩ set X = {}"
shows "⟦M; map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' (map snd D))⟧⇩d ℐ ⟷
⟦M; map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' (map snd (dbproj i D)))⟧⇩d ℐ"
proof -
let ?A = "set (map snd D) ⋅⇩p⇩s⇩e⇩t ℐ"
let ?B = "set (map snd (dbproj i D)) ⋅⇩p⇩s⇩e⇩t ℐ"
let ?C = "set (map snd D) - set (map snd (dbproj i D))"
let ?F = "(λ(t, s). (i, t, s)) ` set F'"
let ?P = "λδ. subst_domain δ = set X ∧ ground (subst_range δ)"

have 1: "∀(t, t') ∈ set (map snd D). (fv t ∪ fv t') ∩ set X = {}"
"∀(t, t') ∈ set (map snd (dbproj i D)). (fv t ∪ fv t') ∩ set X = {}"
using assms(2) dbproj_subset[of i D] unfolding unlabel_def by force+

have 2: "?B ⊆ ?A" unfolding dbproj_def by auto

have 3: "¬Unifier δ (pair f) (pair d)"
when f: "f ∈ set F'" and d: "d ∈ set (map snd D) - set (map snd (dbproj i D))"
for f d and δ::"('fun,'var) subst"
proof -
obtain k where k: "(k,d) ∈ set D - set (dbproj i D)"
using d by force

have "(i,f) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D"
"(k,d) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D"
using f k by auto
hence "i = k" when "Unifier δ (pair f) (pair d)" for δ
using assms(1) that by blast
moreover have "k ≠ i" using k d unfolding dbproj_def by simp
ultimately show ?thesis by metis
qed

have "f ⋅⇩p δ ≠ d ⋅⇩p δ"
when "f ∈ set F'" "d ∈ ?C" for f d and δ::"('fun,'var) subst"
by (metis fun_pair_eq_subst 3[OF that])
hence "f ⋅⇩p (δ ∘⇩s ℐ) ∉ ?C ⋅⇩p⇩s⇩e⇩t (δ ∘⇩s ℐ)"
when "f ∈ set F'" for f and δ::"('fun,'var) subst"
using that by blast
moreover have "?C ⋅⇩p⇩s⇩e⇩t δ ⋅⇩p⇩s⇩e⇩t ℐ = ?C ⋅⇩p⇩s⇩e⇩t ℐ"
when "?P δ" for δ
using assms(2) that pairs_substI[of δ "(set (map snd D) - set (map snd (dbproj i D)))"]
by blast
ultimately have 4: "f ⋅⇩p (δ ∘⇩s ℐ) ∉ ?C ⋅⇩p⇩s⇩e⇩t ℐ"
when "f ∈ set F'" "?P δ" for f and δ::"('fun,'var) subst"
by (metis that subst_pairs_compose)

{ fix f and δ::"('fun,'var) subst"
assume "f ∈ set F'" "?P δ"
hence "f ⋅⇩p (δ ∘⇩s ℐ) ∉ ?C ⋅⇩p⇩s⇩e⇩t ℐ" by (metis 4)
hence "f ⋅⇩p (δ ∘⇩s ℐ) ∉ ?A - ?B" by force
} hence 5: "∀f∈set F'. ∀δ. ?P δ ⟶ f ⋅⇩p (δ ∘⇩s ℐ) ∉ ?A - ?B" by metis

show ?thesis
using negchecks_model_db_subset[OF 2]
negchecks_model_db_supset[OF 2 5]
tr⇩p⇩a⇩i⇩r⇩s_sem_equiv[OF 1(1)]
tr⇩p⇩a⇩i⇩r⇩s_sem_equiv[OF 1(2)]
tr_NegChecks_constr_iff(1)
strand_sem_eq_defs(2)
by (metis (no_types, lifting))
qed

lemma (in stateful_typed_model) labeled_sat_eqs_list_all:
assumes "∀(j, p) ∈ {(i,t,s)} ∪ set D. ∀(k,q) ∈ {(i,t,s)} ∪ set D.
(∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?P D")
and "⟦M; map (λd. ⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t) D⟧⇩d ℐ" (is "?Q D")
shows "list_all (λd. fst d = i) D"
using assms
proof (induction D rule: List.rev_induct)
case (snoc di D)
obtain d j where di: "di = (j,d)" by (metis surj_pair)
have "pair (t,s) ⋅ ℐ = pair d ⋅ ℐ" using di snoc.prems(2) by auto
hence "∃δ. Unifier δ (pair (t,s)) (pair d)" by auto
hence 1: "i = j" using snoc.prems(1) di by fastforce

have "set D ⊆ set (D@[di])" by auto
hence 2: "?P D" using snoc.prems(1) by blast

have 3: "?Q D" using snoc.prems(2) by auto

show ?case using di 1 snoc.IH[OF 2 3] by simp
qed simp

lemma (in stateful_typed_model) labeled_sat_eqs_subseqs:
assumes "Di ∈ set (subseqs D)"
and "∀(j, p) ∈ {(i,t,s)} ∪ set D. ∀(k, q) ∈ {(i,t,s)} ∪ set D.
(∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?P D")
and "⟦M; map (λd. ⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t) Di⟧⇩d ℐ"
shows "Di ∈ set (subseqs (dbproj i D))"
proof -
have "set Di ⊆ set D" by (rule subseqs_subset[OF assms(1)])
hence "?P Di" using assms(2) by blast
thus ?thesis using labeled_sat_eqs_list_all[OF _ assms(3)] subseqs_mem_dbproj[OF assms(1)] by simp
qed

lemma (in stateful_typing_result) dual⇩l⇩s⇩s⇩t_tfr⇩s⇩s⇩t⇩p:
assumes "list_all tfr⇩s⇩s⇩t⇩p (unlabel S)"
shows "list_all tfr⇩s⇩s⇩t⇩p (unlabel (dual⇩l⇩s⇩s⇩t S))"
using assms
proof (induction S)
case (Cons a S)
have prems: "tfr⇩s⇩s⇩t⇩p (snd a)" "list_all tfr⇩s⇩s⇩t⇩p (unlabel S)"
using Cons.prems unlabel_Cons(2)[of a S] by simp_all
hence IH: "list_all tfr⇩s⇩s⇩t⇩p (unlabel (dual⇩l⇩s⇩s⇩t S))" by (metis Cons.IH)

obtain l b where a: "a = (l,b)" by (metis surj_pair)
with Cons show ?case
proof (cases b)
case (Equality c t t')
hence "dual⇩l⇩s⇩s⇩t (a#S) = a#dual⇩l⇩s⇩s⇩t S" by (metis dual⇩l⇩s⇩s⇩t_Cons(3) a)
thus ?thesis using a IH prems by fastforce
next
case (NegChecks X F G)
hence "dual⇩l⇩s⇩s⇩t (a#S) = a#dual⇩l⇩s⇩s⇩t S" by (metis dual⇩l⇩s⇩s⇩t_Cons(7) a)
thus ?thesis using a IH prems by fastforce
qed auto
qed simp

lemma (in stateful_typed_model) setops⇩s⇩s⇩t_unlabel_dual⇩l⇩s⇩s⇩t_eq:
"setops⇩s⇩s⇩t (unlabel (dual⇩l⇩s⇩s⇩t A)) = setops⇩s⇩s⇩t (unlabel A)"
proof (induction A)
case (Cons a A)
obtain l b where a: "a = (l,b)" by (metis surj_pair)
thus ?case using Cons.IH by (cases b) (simp_all add: setops⇩s⇩s⇩t_def)
qed simp

subsection ‹Locale Setup and Definitions›
locale labeled_stateful_typed_model =
stateful_typed_model arity public Ana Γ Pair
+ labeled_typed_model arity public Ana Γ label_witness1 label_witness2
for arity::"'fun ⇒ nat"
and public::"'fun ⇒ bool"
and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
and Pair::"'fun"
and label_witness1::"'lbl"
and label_witness2::"'lbl"
begin

definition lpair where
"lpair lp ≡ case lp of (i,p) ⇒ (i,pair p)"

lemma setops⇩l⇩s⇩s⇩t⇩p_pair_image[simp]:
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,send⟨ts⟩)) = {}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,receive⟨ts⟩)) = {}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,⟨ac: t ≐ t'⟩)) = {}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,insert⟨t,s⟩)) = {(i, pair (t,s))}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,delete⟨t,s⟩)) = {(i, pair (t,s))}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,⟨ac: t ∈ s⟩)) = {(i, pair (t,s))}"
"lpair ` (setops⇩l⇩s⇩s⇩t⇩p (i,∀X⟨∨≠: F ∨∉: F'⟩)) = ((λ(t,s). (i, pair (t,s))) ` set F')"
unfolding lpair_def by force+

definition par_comp⇩l⇩s⇩s⇩t where
"par_comp⇩l⇩s⇩s⇩t (𝒜::('fun,'var,'lbl) labeled_stateful_strand) (Secrets::('fun,'var) terms) ≡
(∀l1 l2. l1 ≠ l2 ⟶
GSMP_disjoint (trms⇩s⇩s⇩t (proj_unl l1 𝒜) ∪ pair ` setops⇩s⇩s⇩t (proj_unl l1 𝒜))
(trms⇩s⇩s⇩t (proj_unl l2 𝒜) ∪ pair ` setops⇩s⇩s⇩t (proj_unl l2 𝒜)) Secrets) ∧
(∀s ∈ Secrets. ¬{} ⊢⇩c s) ∧ ground Secrets ∧
(∀(i,p) ∈ setops⇩l⇩s⇩s⇩t 𝒜. ∀(j,q) ∈ setops⇩l⇩s⇩s⇩t 𝒜.
(∃δ. Unifier δ (pair p) (pair q)) ⟶ i = j)"

definition declassified⇩l⇩s⇩s⇩t where
"declassified⇩l⇩s⇩s⇩t 𝒜 ℐ ≡ {s. ⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (𝒜 ⋅⇩l⇩s⇩s⇩t ℐ)} ⊢ s}"

definition strand_leaks⇩l⇩s⇩s⇩t ("_ leaks _ under _") where
"(𝒜::('fun,'var,'lbl) labeled_stateful_strand) leaks Secrets under ℐ ≡
(∃t ∈ Secrets - declassified⇩l⇩s⇩s⇩t 𝒜 ℐ. ∃n. ℐ ⊨⇩s (proj_unl n 𝒜@[send⟨[t]⟩]))"

type_synonym ('a,'b,'c) labeleddbstate = "('c strand_label × (('a,'b) term × ('a,'b) term)) set"
type_synonym ('a,'b,'c) labeleddbstatelist = "('c strand_label × (('a,'b) term × ('a,'b) term)) list"

definition typing_cond⇩s⇩s⇩t where
"typing_cond⇩s⇩s⇩t 𝒜 ≡ wf⇩s⇩s⇩t 𝒜 ∧ wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t 𝒜) ∧ tfr⇩s⇩s⇩t 𝒜"

text ‹
For proving the compositionality theorem for stateful constraints the idea is to first define a
variant of the reduction technique that was used to establish the stateful typing result. This
variant performs database-state projections, and it allows us to reduce the compositionality
problem for stateful constraints to ordinary constraints.
›
fun tr⇩p⇩c::
"('fun,'var,'lbl) labeled_stateful_strand ⇒ ('fun,'var,'lbl) labeleddbstatelist
⇒ ('fun,'var,'lbl) labeled_strand list"
where
"tr⇩p⇩c [] D = [[]]"
| "tr⇩p⇩c ((i,send⟨ts⟩)#A) D = map ((#) (i,send⟨ts⟩⇩s⇩t)) (tr⇩p⇩c A D)"
| "tr⇩p⇩c ((i,receive⟨ts⟩)#A) D = map ((#) (i,receive⟨ts⟩⇩s⇩t)) (tr⇩p⇩c A D)"
| "tr⇩p⇩c ((i,⟨ac: t ≐ t'⟩)#A) D = map ((#) (i,⟨ac: t ≐ t'⟩⇩s⇩t)) (tr⇩p⇩c A D)"
| "tr⇩p⇩c ((i,insert⟨t,s⟩)#A) D = tr⇩p⇩c A (List.insert (i,(t,s)) D)"
| "tr⇩p⇩c ((i,delete⟨t,s⟩)#A) D = (
concat (map (λDi. map (λB. (map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)) Di)@
(map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t))
[d←dbproj i D. d ∉ set Di])@B)
(tr⇩p⇩c A [d←D. d ∉ set Di]))
(subseqs (dbproj i D))))"
| "tr⇩p⇩c ((i,⟨ac: t ∈ s⟩)#A) D =
concat (map (λB. map (λd. (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)#B) (dbproj i D)) (tr⇩p⇩c A D))"
| "tr⇩p⇩c ((i,∀X⟨∨≠: F ∨∉: F' ⟩)#A) D =
map ((@) (map (λG. (i,∀X⟨∨≠: (F@G)⟩⇩s⇩t)) (tr⇩p⇩a⇩i⇩r⇩s F' (map snd (dbproj i D))))) (tr⇩p⇩c A D)"

end

locale labeled_stateful_typing =
labeled_stateful_typed_model arity public Ana Γ Pair label_witness1 label_witness2
+ stateful_typing_result arity public Ana Γ Pair
for arity::"'fun ⇒ nat"
and public::"'fun ⇒ bool"
and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
and Pair::"'fun"
and label_witness1::"'lbl"
and label_witness2::"'lbl"
begin

sublocale labeled_typing
by unfold_locales

end

subsection ‹Small Lemmata›
context labeled_stateful_typed_model
begin

lemma declassified⇩l⇩s⇩s⇩t_alt_def:
"declassified⇩l⇩s⇩s⇩t 𝒜 ℐ = {s. ⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set 𝒜} ⋅⇩s⇩e⇩t ℐ ⊢ s}"
proof -
have "(l, receive⟨ts⟩) ∈ set (𝒜 ⋅⇩l⇩s⇩s⇩t ℐ) = (∃ts'. (l, receive⟨ts'⟩) ∈ set 𝒜 ∧ ts = ts' ⋅⇩l⇩i⇩s⇩t ℐ)"
(is "?A 𝒜 = ?B 𝒜")
for ts l
proof
show "?A 𝒜 ⟹ ?B 𝒜"
proof (induction 𝒜)
case (Cons a 𝒜)
obtain k b where a: "a = (k,b)" by (metis surj_pair)
show ?case
proof (cases "?A 𝒜")
case False
hence "(l,receive⟨ts⟩) = a ⋅⇩l⇩s⇩s⇩t⇩p ℐ" using Cons.prems subst_lsst_cons[of a 𝒜 ℐ] by auto
thus ?thesis unfolding a by (cases b) auto
qed (use Cons.IH in auto)
qed simp

show "?B 𝒜 ⟹ ?A 𝒜"
proof (induction 𝒜)
case (Cons a 𝒜)
obtain k b where a: "a = (k,b)" by (metis surj_pair)
show ?case
proof (cases "?B 𝒜")
case False
hence "∃ts'. a = (l, receive⟨ts'⟩) ∧ ts = ts' ⋅⇩l⇩i⇩s⇩t ℐ" using Cons.prems by auto
thus ?thesis using subst_lsst_cons[of a 𝒜 ℐ] unfolding a by (cases b) auto
qed (use Cons.IH subst_lsst_cons[of a 𝒜 ℐ] in auto)
qed simp
qed
thus ?thesis
unfolding declassified⇩l⇩s⇩s⇩t_def
by (smt Collect_cong image_Union list.set_map setcompr_eq_image)
qed

lemma declassified⇩l⇩s⇩s⇩t_prefix_subset:
assumes AB: "prefix A B"
shows "declassified⇩l⇩s⇩s⇩t A I ⊆ declassified⇩l⇩s⇩s⇩t B I"
proof
fix t assume t: "t ∈ declassified⇩l⇩s⇩s⇩t A I"
obtain C where C: "B = A@C" using prefixE[OF AB] by metis
show "t ∈ declassified⇩l⇩s⇩s⇩t B I"
using t ideduct_mono[of
"⋃{set ts |ts. (⋆, receive⟨ts⟩) ∈ set A} ⋅⇩s⇩e⇩t I" t
"⋃{set ts |ts. (⋆, receive⟨ts⟩) ∈ set B} ⋅⇩s⇩e⇩t I"]
unfolding C declassified⇩l⇩s⇩s⇩t_alt_def by auto
qed

"{t | t ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set 𝒜 ∧ t ∈ set ts} ⋅⇩s⇩e⇩t ℐ ⊆ declassified⇩l⇩s⇩s⇩t 𝒜 ℐ"
unfolding declassified⇩l⇩s⇩s⇩t_alt_def by (fastforce intro: intruder_deduct.Axiom)

lemma declassified⇩l⇩s⇩s⇩t_proj_eq:
"declassified⇩l⇩s⇩s⇩t A I = declassified⇩l⇩s⇩s⇩t (proj n A) I"
using proj_mem_iff(2)[of _ A] unfolding declassified⇩l⇩s⇩s⇩t_alt_def by simp

lemma par_comp⇩l⇩s⇩s⇩t_nil:
assumes "ground Sec" "∀s ∈ Sec. ∀s'∈subterms s. {} ⊢⇩c s' ∨ s' ∈ Sec" "∀s ∈ Sec. ¬{} ⊢⇩c s"
shows "par_comp⇩l⇩s⇩s⇩t [] Sec"
using assms unfolding par_comp⇩l⇩s⇩s⇩t_def by simp

lemma par_comp⇩l⇩s⇩s⇩t_subset:
assumes A: "par_comp⇩l⇩s⇩s⇩t A Sec"
and BA: "set B ⊆ set A"
shows "par_comp⇩l⇩s⇩s⇩t B Sec"
proof -
let ?L = "λn A. trms⇩s⇩s⇩t (proj_unl n A) ∪ pair ` setops⇩s⇩s⇩t (proj_unl n A)"

have "?L n B ⊆ ?L n A" for n
using trms⇩s⇩s⇩t_mono[OF proj_set_mono(2)[OF BA]] setops⇩s⇩s⇩t_mono[OF proj_set_mono(2)[OF BA]]
by blast
hence "GSMP_disjoint (?L m B) (?L n B) Sec" when nm: "m ≠ n" for n m::'lbl
using GSMP_disjoint_subset[of "?L m A" "?L n A" Sec "?L m B" "?L n B"] A nm
unfolding par_comp⇩l⇩s⇩s⇩t_def by simp
thus "par_comp⇩l⇩s⇩s⇩t B Sec"
using A setops⇩l⇩s⇩s⇩t_mono[OF BA]
unfolding par_comp⇩l⇩s⇩s⇩t_def by blast
qed

lemma par_comp⇩l⇩s⇩s⇩t_split:
assumes "par_comp⇩l⇩s⇩s⇩t (A@B) Sec"
shows "par_comp⇩l⇩s⇩s⇩t A Sec" "par_comp⇩l⇩s⇩s⇩t B Sec"
using par_comp⇩l⇩s⇩s⇩t_subset[OF assms] by simp_all

lemma par_comp⇩l⇩s⇩s⇩t_proj:
assumes "par_comp⇩l⇩s⇩s⇩t A Sec"
shows "par_comp⇩l⇩s⇩s⇩t (proj n A) Sec"
using par_comp⇩l⇩s⇩s⇩t_subset[OF assms] by simp

lemma par_comp⇩l⇩s⇩s⇩t_dual⇩l⇩s⇩s⇩t:
assumes A: "par_comp⇩l⇩s⇩s⇩t A S"
shows "par_comp⇩l⇩s⇩s⇩t (dual⇩l⇩s⇩s⇩t A) S"
proof (unfold par_comp⇩l⇩s⇩s⇩t_def case_prod_unfold; intro conjI)
show "ground S" "∀s ∈ S. ¬{} ⊢⇩c s"
using A unfolding par_comp⇩l⇩s⇩s⇩t_def by fast+

let ?M = "λl B. (trms⇩l⇩s⇩s⇩t (proj l B) ∪ pair ` setops⇩s⇩s⇩t (proj_unl l B))"
let ?P = "λB. ∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (?M l1 B) (?M l2 B) S"
let ?Q = "λB. ∀p ∈ setops⇩l⇩s⇩s⇩t B. ∀q ∈ setops⇩l⇩s⇩s⇩t B.
(∃δ. Unifier δ (pair (snd p)) (pair (snd q))) ⟶ fst p = fst q"

have "?P A" "?Q A" using A unfolding par_comp⇩l⇩s⇩s⇩t_def case_prod_unfold by blast+
thus "?P (dual⇩l⇩s⇩s⇩t A)" "?Q (dual⇩l⇩s⇩s⇩t A)"
by (metis setops⇩s⇩s⇩t_unlabel_dual⇩l⇩s⇩s⇩t_eq trms⇩s⇩s⇩t_unlabel_dual⇩l⇩s⇩s⇩t_eq proj_dual⇩l⇩s⇩s⇩t,
metis setops⇩l⇩s⇩s⇩t_dual⇩l⇩s⇩s⇩t_eq)
qed

lemma par_comp⇩l⇩s⇩s⇩t_subst:
assumes A: "par_comp⇩l⇩s⇩s⇩t A S"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" "subst_domain δ ∩ bvars⇩l⇩s⇩s⇩t A = {}"
shows "par_comp⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ) S"
proof (unfold par_comp⇩l⇩s⇩s⇩t_def case_prod_unfold; intro conjI)
show "ground S" "∀s ∈ S. ¬{} ⊢⇩c s"
using A unfolding par_comp⇩l⇩s⇩s⇩t_def by fast+

let ?N = "λl B. trms⇩l⇩s⇩s⇩t (proj l B) ∪ pair ` setops⇩s⇩s⇩t (proj_unl l B)"
define M where "M ≡ λl (B::('fun,'var,'lbl) labeled_stateful_strand). ?N l B"
let ?P = "λp q. ∃δ. Unifier δ (pair (snd p)) (pair (snd q))"
let ?Q = "λB. ∀p ∈ setops⇩l⇩s⇩s⇩t B. ∀q ∈ setops⇩l⇩s⇩s⇩t B. ?P p q ⟶ fst p = fst q"
let ?R = "λB. ∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (?N l1 B) (?N l2 B) S"

have d: "bvars⇩l⇩s⇩s⇩t (proj l A) ∩ subst_domain δ = {}" for l
using δ(3) unfolding proj_def bvars⇩s⇩s⇩t_def unlabel_def by auto

have "GSMP_disjoint (M l1 A) (M l2 A) S" when l: "l1 ≠ l2" for l1 l2
using l A unfolding par_comp⇩l⇩s⇩s⇩t_def M_def by presburger
moreover have "M l (A ⋅⇩l⇩s⇩s⇩t δ) = (M l A) ⋅⇩s⇩e⇩t δ" for l
using fun_pair_subst_set[of δ "setops⇩s⇩s⇩t (proj_unl l A)", symmetric]
trms⇩s⇩s⇩t_subst[OF d[of l]] setops⇩s⇩s⇩t_subst[OF d[of l]] proj_subst[of l A δ]
unfolding M_def unlabel_subst by auto
ultimately have "GSMP_disjoint (M l1 (A ⋅⇩l⇩s⇩s⇩t δ)) (M l2 (A ⋅⇩l⇩s⇩s⇩t δ)) S" when l: "l1 ≠ l2" for l1 l2
using l GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l1 A"]
GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l2 A"]
unfolding GSMP_disjoint_def by fastforce
thus "?R (A ⋅⇩l⇩s⇩s⇩t δ)" unfolding M_def by blast

have "?Q A" using A unfolding par_comp⇩l⇩s⇩s⇩t_def by force
thus "?Q (A ⋅⇩l⇩s⇩s⇩t δ)" using δ(3)
proof (induction A)
case (Cons a A)
obtain l b where a: "a = (l,b)" by (metis surj_pair)

have 0: "bvars⇩l⇩s⇩s⇩t (a#A) = set (bvars⇩s⇩s⇩t⇩p (snd a)) ∪ bvars⇩l⇩s⇩s⇩t A"
unfolding bvars⇩s⇩s⇩t_def unlabel_def by simp

have "?Q A" "subst_domain δ ∩ bvars⇩l⇩s⇩s⇩t A = {}"
using Cons.prems 0 unfolding setops⇩l⇩s⇩s⇩t_def by auto
hence IH: "?Q (A ⋅⇩l⇩s⇩s⇩t δ)" using Cons.IH unfolding setops⇩l⇩s⇩s⇩t_def by blast

have 1: "fst p = fst q"
when p: "p ∈ setops⇩l⇩s⇩s⇩t⇩p (a ⋅⇩l⇩s⇩s⇩t⇩p δ)"
and q: "q ∈ setops⇩l⇩s⇩s⇩t⇩p (a ⋅⇩l⇩s⇩s⇩t⇩p δ)"
and pq: "?P p q"
for p q
using a p q pq by (cases b) auto

have 2: "fst p = fst q"
when p: "p ∈ setops⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
and q: "q ∈ setops⇩l⇩s⇩s⇩t⇩p (a ⋅⇩l⇩s⇩s⇩t⇩p δ)"
and pq: "?P p q"
for p q
proof -
obtain p' X where p':
"p' ∈ setops⇩l⇩s⇩s⇩t A" "fst p = fst p'"
"X ⊆ bvars⇩l⇩s⇩s⇩t (a#A)" "snd p = snd p' ⋅⇩p rm_vars X δ"
using setops⇩l⇩s⇩s⇩t_in_subst[OF p] 0 by blast

obtain q' Y where q':
"q' ∈ setops⇩l⇩s⇩s⇩t⇩p a" "fst q = fst q'"
"Y ⊆ bvars⇩l⇩s⇩s⇩t (a#A)" "snd q = snd q' ⋅⇩p rm_vars Y δ"
using setops⇩l⇩s⇩s⇩t⇩p_in_subst[OF q] 0 by blast

have "pair (snd p) = pair (snd p') ⋅ δ"
"pair (snd q) = pair (snd q') ⋅ δ"
using fun_pair_subst[of "snd p'" "rm_vars X δ"] fun_pair_subst[of "snd q'" "rm_vars Y δ"]
p'(3,4) q'(3,4) Cons.prems(2) rm_vars_apply'[of δ X] rm_vars_apply'[of δ Y]
by fastforce+
hence "∃δ. Unifier δ (pair (snd p')) (pair (snd q'))"
using pq Unifier_comp' by metis
thus ?thesis using Cons.prems p'(1,2) q'(1,2) by simp
qed

show ?case by (metis 1 2 IH Un_iff setops⇩l⇩s⇩s⇩t_cons subst_lsst_cons)
qed simp
qed

lemma wf_pair_negchecks_map':
assumes "wf⇩s⇩t X (unlabel A)"
shows "wf⇩s⇩t X (unlabel (map (λG. (i,∀Y⟨∨≠: (F@G)⟩⇩s⇩t)) M@A))"
using assms by (induct M) auto

lemma wf_pair_eqs_ineqs_map':
fixes A::"('fun,'var,'lbl) labeled_strand"
assumes "wf⇩s⇩t X (unlabel A)"
"Di ∈ set (subseqs (dbproj i D))"
"fv⇩p⇩a⇩i⇩r⇩s (unlabel D) ⊆ X"
shows "wf⇩s⇩t X (unlabel (
(map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)) Di)@
(map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t)) [d←dbproj i D. d ∉ set Di])@A))"
proof -
let ?f = "[d←dbproj i D. d ∉ set Di]"
define c1 where c1: "c1 = map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)) Di"
define c2 where c2: "c2 = map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t)) ?f"
define c3 where c3: "c3 = map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) (unlabel Di)"
define c4 where c4: "c4 = map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩⇩s⇩t) (unlabel ?f)"
have ci_eqs: "c3 = unlabel c1" "c4 = unlabel c2" unfolding c1 c2 c3 c4 unlabel_def by auto
have 1: "wf⇩s⇩t X (unlabel (c2@A))"
using wf_fun_pair_ineqs_map[OF assms(1)] ci_eqs(2) unlabel_append[of c2 A] c4
by metis
have 2: "fv⇩p⇩a⇩i⇩r⇩s (unlabel Di) ⊆ X"
using assms(3) subseqs_set_subset(1)[OF assms(2)]
unfolding unlabel_def dbproj_def
by fastforce
{ fix B::"('fun,'var) strand" assume "wf⇩s⇩t X B"
hence "wf⇩s⇩t X (unlabel c1@B)" using 2 unfolding c1 unlabel_def by (induct Di) auto
} thus ?thesis using 1 unfolding c1 c2 unlabel_def by simp
qed

lemma trms⇩s⇩s⇩t_setops⇩s⇩s⇩t_wt_instance_ex:
defines "M ≡ λA. trms⇩l⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t (unlabel A)"
assumes B: "∀b ∈ set B. ∃a ∈ set A. ∃δ. b = a ⋅⇩l⇩s⇩s⇩t⇩p δ ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "∀t ∈ M B. ∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"
proof
let ?P = "λδ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"

fix t assume "t ∈ M B"
then obtain b where b: "b ∈ set B" "t ∈ trms⇩s⇩s⇩t⇩p (snd b) ∪ pair ` setops⇩s⇩s⇩t⇩p (snd b)"
unfolding M_def unfolding unlabel_def trms⇩s⇩s⇩t_def setops⇩s⇩s⇩t_def by auto
then obtain a δ where a: "a ∈ set A" "b = a ⋅⇩l⇩s⇩s⇩t⇩p δ" and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using B by meson

note δ' = wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)]

have "t ∈ M (A ⋅⇩l⇩s⇩s⇩t δ)"
using b(2) a
unfolding M_def subst_apply_labeled_stateful_strand_def unlabel_def trms⇩s⇩s⇩t_def setops⇩s⇩s⇩t_def
by auto
moreover have "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" when "t ∈ trms⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
using trms⇩s⇩s⇩t_unlabel_subst'[OF that] δ' unfolding M_def by blast
moreover have "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" when t: "t ∈ pair ` setops⇩s⇩s⇩t (unlabel A ⋅⇩s⇩s⇩t δ)"
proof -
obtain p where p: "p ∈ setops⇩s⇩s⇩t (unlabel A ⋅⇩s⇩s⇩t δ)" "t = pair p" using t by blast
then obtain q X where q: "q ∈ setops⇩s⇩s⇩t (unlabel A)" "p = q ⋅⇩p rm_vars (set X) δ"
using setops⇩s⇩s⇩t_subst'[OF p(1)] by blast
hence "t = pair q ⋅ rm_vars (set X) δ"
using fun_pair_subst[of q "rm_vars (set X) δ"] p(2) by presburger
thus ?thesis using δ'[of "set X"] q(1) unfolding M_def by blast
qed
ultimately show "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" unfolding M_def unlabel_subst by fast
qed

lemma setops⇩l⇩s⇩s⇩t_wt_instance_ex:
assumes B: "∀b ∈ set B. ∃a ∈ set A. ∃δ. b = a ⋅⇩l⇩s⇩s⇩t⇩p δ ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "∀p ∈ setops⇩l⇩s⇩s⇩t B. ∃q ∈ setops⇩l⇩s⇩s⇩t A. ∃δ.
fst p = fst q ∧ snd p = snd q ⋅⇩p δ ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"
proof
let ?P = "λδ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ)"

fix p assume "p ∈ setops⇩l⇩s⇩s⇩t B"
then obtain b where b: "b ∈ set B" "p ∈ setops⇩l⇩s⇩s⇩t⇩p b" unfolding setops⇩l⇩s⇩s⇩t_def by blast
then obtain a δ where a: "a ∈ set A" "b = a ⋅⇩l⇩s⇩s⇩t⇩p δ" and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using B by meson
hence p: "p ∈ setops⇩l⇩s⇩s⇩t (A ⋅⇩l⇩s⇩s⇩t δ)"
using b(2) unfolding setops⇩l⇩s⇩s⇩t_def subst_apply_labeled_stateful_strand_def by auto

obtain X q where q:
"q ∈ setops⇩l⇩s⇩s⇩t A" "fst p = fst q" "snd p = snd q ⋅⇩p rm_vars X δ"
using setops⇩l⇩s⇩s⇩t_in_subst[OF p] by blast

show "∃q ∈ setops⇩l⇩s⇩s⇩t A. ∃δ. fst p = fst q ∧ snd p = snd q ⋅⇩p δ ∧ ?P δ"
using q wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)] by blast
qed

lemma deduct_proj_priv_term_prefix_ex_stateful:
assumes A: "ik⇩s⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t I ⊢ t"
and t: "¬{} ⊢⇩c t"
shows "∃B k s. (k = ⋆ ∨ k = ln l) ∧ prefix (B@[(k,receive⟨s⟩)]) A ∧
declassified⇩l⇩s⇩s⇩t ((B@[(k,receive⟨s⟩)])) I = declassified⇩l⇩s⇩s⇩t A I ∧
ik⇩s⇩s⇩t (proj_unl l (B@[(k,receive⟨s⟩)])) = ik⇩s⇩s⇩t (proj_unl l A)"
using A
proof (induction A rule: List.rev_induct)
case Nil
have "ik⇩s⇩s⇩t (proj_unl l []) ⋅⇩s⇩e⇩t I = {}" by auto
thus ?case using Nil t deducts_eq_if_empty_ik[of t] by argo
next
case (snoc a A)
obtain k b where a: "a = (k,b)" by (metis surj_pair)
let ?P = "k = ⋆ ∨ k = (ln l)"
let ?Q = "∃s. b = receive⟨s⟩"

have 0: "ik⇩s⇩s⇩t (proj_unl l (A@[a])) = ik⇩s⇩s⇩t (proj_unl l A)" when "?P ⟹ ¬?Q"
using that ik⇩s⇩s⇩t_snoc_no_receive_eq[OF that, of I "proj_unl l A"]
unfolding ik⇩s⇩s⇩t_def a by (cases "k = ⋆ ∨ k = (ln l)") auto

have 1: "declassified⇩l⇩s⇩s⇩t (A@[a]) I = declassified⇩l⇩s⇩s⇩t A I" when "?P ⟹ ¬?Q"
using that snoc.prems unfolding declassified⇩l⇩s⇩s⇩t_alt_def a
by (metis (no_types, lifting) UnCI UnE empty_iff insert_iff list.set prod.inject set_append)

note 2 = snoc.prems snoc.IH 0 1

show ?case
proof (cases ?P)
case True
note T = this
thus ?thesis
proof (cases ?Q)
case True thus ?thesis using T unfolding a by blast
qed (use 2 in auto)
qed (use 2 in auto)
qed

lemma constr_sem_stateful_proj_priv_term_prefix_obtain:
assumes 𝒜': "prefix 𝒜' 𝒜" "constr_sem_stateful ℐ⇩τ (proj_unl n 𝒜'@[send⟨[t]⟩])"
and t: "t ∈ Sec - declassified⇩l⇩s⇩s⇩t 𝒜' ℐ⇩τ" "¬{} ⊢⇩c t" "t ⋅ ℐ⇩τ = t"
obtains B k' s where
"k' = ⋆ ∨ k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s⟩)] B"
"declassified⇩l⇩s⇩s⇩t B ℐ⇩τ = declassified⇩l⇩s⇩s⇩t 𝒜' ℐ⇩τ"
"ik⇩l⇩s⇩s⇩t (proj n B) = ik⇩l⇩s⇩s⇩t (proj n 𝒜')"
"constr_sem_stateful ℐ⇩τ (proj_unl n B@[send⟨[t]⟩])"
"prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s⟩)] (proj n B)"
"t ∈ Sec - declassified⇩l⇩s⇩s⇩t (proj n B) ℐ⇩τ"
proof -
have "ik⇩l⇩s⇩s⇩t (proj n 𝒜') ⋅⇩s⇩e⇩t ℐ⇩τ ⊢ t"
using 𝒜'(2) t(3) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]⟩]" ℐ⇩τ]
by simp
then obtain B k' s where B:
"k' = ⋆ ∨ k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s⟩)] B"
"declassified⇩l⇩s⇩s⇩t B ℐ⇩τ = declassified⇩l⇩s⇩s⇩t 𝒜' ℐ⇩τ"
"ik⇩l⇩s⇩s⇩t (proj n B) = ik⇩l⇩s⇩s⇩t (proj n 𝒜')"
using deduct_proj_priv_term_prefix_ex_stateful[OF _ t(2), of ℐ⇩τ n 𝒜']
unfolding suffix_def by blast

have B': "constr_sem_stateful ℐ⇩τ (proj_unl n B@[send⟨[t]⟩])"
using B(5) 𝒜'(2) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]⟩]" ℐ⇩τ]
strand_sem_append_stateful[of "{}" "{}" "proj_unl n B" _ ℐ⇩τ]
prefix_proj(2)[OF B(2), of n]
by (metis (no_types, lifting) append_Nil2 prefix_def strand_sem_stateful.simps(2))

have B'': "prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s⟩)] (proj n B)"
"t ∈ Sec - declassified⇩l⇩s⇩s⇩t (proj n B) ℐ⇩τ"
using 𝒜' t B(1-4) declassified⇩l⇩s⇩s⇩t_proj_eq[of B ℐ⇩τ n]
unfolding suffix_def prefix_def proj_def by auto

show ?thesis by (rule that[OF B B' B''])
qed

lemma constr_sem_stateful_star_proj_no_leakage:
fixes Sec P lbls k
defines "no_leakage ≡ λ𝒜. ∄ℐ⇩τ ℬ s.
prefix ℬ 𝒜 ∧ s ∈ Sec - declassified⇩l⇩s⇩s⇩t ℬ ℐ⇩τ ∧ ℐ⇩τ ⊨⇩s (unlabel ℬ@[send⟨[s]⟩])"
assumes Sec: "ground Sec"
and 𝒜: "∀(l,a) ∈ set 𝒜. l = ⋆"
shows "no_leakage 𝒜"
proof (rule ccontr)
assume "¬no_leakage 𝒜"
then obtain I B s where B:
"prefix B 𝒜" "s ∈ Sec - declassified⇩l⇩s⇩s⇩t B I" "I ⊨⇩s (unlabel B@[send⟨[s]⟩])"
unfolding no_leakage_def by blast

have 1: "¬(⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (B ⋅⇩l⇩s⇩s⇩t I)} ⊢ s)"
using B(2) unfolding declassified⇩l⇩s⇩s⇩t_def by fast

have 2: "ik⇩l⇩s⇩s⇩t (B ⋅⇩l⇩s⇩s⇩t I) ⊢ s"
using B(2,3) Sec strand_sem_append_stateful[of "{}" "{}" "unlabel B" "[send⟨[s]⟩]" I]
trm_subst_ident[of s I] unlabel_subst[of B] ik⇩s⇩s⇩t_subst[of "unlabel B"]
by force

have "l = ⋆" when "(l,c) ∈ set B" for l c
using that 𝒜 B(1) set_mono_prefix by blast
hence "l = ⋆" when "(l,c) ∈ set (B ⋅⇩l⇩s⇩s⇩t I)" for l c
using that unfolding subst_apply_labeled_stateful_strand_def by auto
hence 3: "ik⇩l⇩s⇩s⇩t (B ⋅⇩l⇩s⇩s⇩t I) = (⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (B ⋅⇩l⇩s⇩s⇩t I)})"
using in_ik⇩l⇩s⇩s⇩t_iff[of _ "B ⋅⇩l⇩s⇩s⇩t I"] unfolding ik⇩s⇩s⇩t_def unlabel_def by auto

show False using 1 2 3 by force
qed

end

subsection ‹Lemmata: Properties of the Constraint Translation Function›
context labeled_stateful_typed_model
begin

lemma tr_par_labeled_rcv_iff:
"B ∈ set (tr⇩p⇩c A D) ⟹ (i, receive⟨t⟩⇩s⇩t) ∈ set B ⟷ (i, receive⟨t⟩) ∈ set A"
by (induct A D arbitrary: B rule: tr⇩p⇩c.induct) auto

lemma tr_par_declassified_eq:
"B ∈ set (tr⇩p⇩c A D) ⟹ declassified⇩l⇩s⇩t B I = declassified⇩l⇩s⇩s⇩t A I"
using tr_par_labeled_rcv_iff unfolding declassified⇩l⇩s⇩t_alt_def declassified⇩l⇩s⇩s⇩t_alt_def by simp

lemma tr_par_ik_eq:
assumes "B ∈ set (tr⇩p⇩c A D)"
shows "ik⇩s⇩t (unlabel B) = ik⇩s⇩s⇩t (unlabel A)"
proof -
have "{t. ∃i. (i, receive⟨t⟩⇩s⇩t) ∈ set B} = {t. ∃i. (i, receive⟨t⟩) ∈ set A}"
using tr_par_labeled_rcv_iff[OF assms] by simp
moreover have
"⋀C. {t. ∃i. (i, receive⟨t⟩⇩s⇩t) ∈ set C} = {t. receive⟨t⟩⇩s⇩t ∈ set (unlabel C)}"
"⋀C. {t. ∃i. (i, receive⟨t⟩) ∈ set C} = {t. receive⟨t⟩ ∈ set (unlabel C)}"
unfolding unlabel_def by force+
ultimately show ?thesis unfolding ik⇩s⇩s⇩t_def ik⇩s⇩t_is_rcv_set by fast
qed

lemma tr_par_deduct_iff:
assumes "B ∈ set (tr⇩p⇩c A D)"
shows "ik⇩s⇩t (unlabel B) ⋅⇩s⇩e⇩t I ⊢ t ⟷ ik⇩s⇩s⇩t (unlabel A) ⋅⇩s⇩e⇩t I ⊢ t"
using tr_par_ik_eq[OF assms] by metis

lemma tr_par_vars_subset:
assumes "A' ∈ set (tr⇩p⇩c A D)"
shows "fv⇩l⇩s⇩t A' ⊆ fv⇩s⇩s⇩t (unlabel A) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)" (is ?P)
and "bvars⇩l⇩s⇩t A' ⊆ bvars⇩s⇩s⇩t (unlabel A)" (is ?Q)
proof -
show ?P using assms
proof (induction "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
case (ConsIn A' D ac t s AA A A')
then obtain i B where iB: "A = (i,⟨ac: t ∈ s⟩)#B" "AA = unlabel B"
unfolding unlabel_def by moura
then obtain A'' d where *:
"d ∈ set (dbproj i D)"
"A' = (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)#A''"
"A'' ∈ set (tr⇩p⇩c B D)"
using ConsIn.prems(1) by moura
hence "fv⇩l⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t (unlabel B) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
"fv (pair (snd d)) ⊆ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
apply (metis ConsIn.hyps(1)[OF iB(2)])
using fv⇩p⇩a⇩i⇩r⇩s_mono[OF dbproj_subset[of i D]]
fv_pair_fv⇩p⇩a⇩i⇩r⇩s_subset[OF *(1)]
by blast
thus ?case using * iB unfolding pair_def by auto
next
case (ConsDel A' D t s AA A A')
then obtain i B where iB: "A = (i,delete⟨t,s⟩)#B" "AA = unlabel B"
unfolding unlabel_def by moura

define fltD1 where "fltD1 = (λDi. filter (λd. d ∉ set Di) D)"
define fltD2 where "fltD2 = (λDi. filter (λd. d ∉ set Di) (dbproj i D))"
define constr where "constr =
(λDi. (map (λd. (i, ⟨check: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)) Di)@
(map (λd. (i, ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t)) (fltD2 Di)))"

from iB obtain A'' Di where *:
"Di ∈ set (subseqs (dbproj i D))" "A' = (constr Di)@A''" "A'' ∈ set (tr⇩p⇩c B (fltD1 Di))"
using ConsDel.prems(1) unfolding constr_def fltD1_def fltD2_def by moura
hence "fv⇩l⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t AA ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel (fltD1 Di))"
unfolding constr_def fltD1_def by (metis ConsDel.hyps(1) iB(2))
hence 1: "fv⇩l⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t AA ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
using fv⇩p⇩a⇩i⇩r⇩s_mono[of "unlabel (fltD1 Di)" "unlabel D"]
unfolding unlabel_def fltD1_def by force

have 2: "fv⇩p⇩a⇩i⇩r⇩s (unlabel Di) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel (fltD1 Di)) ⊆ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
using subseqs_set_subset(1)[OF *(1)]
unfolding fltD1_def unlabel_def dbproj_def
by auto

have 5: "fv⇩l⇩s⇩t A' = fv⇩l⇩s⇩t (constr Di) ∪ fv⇩l⇩s⇩t A''" using * unfolding unlabel_def by force

have "fv⇩l⇩s⇩t (constr Di) ⊆ fv t ∪ fv s ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel Di) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel (fltD1 Di))"
unfolding unlabel_def constr_def fltD1_def fltD2_def pair_def dbproj_def by auto
hence 3: "fv⇩l⇩s⇩t (constr Di) ⊆ fv t ∪ fv s ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)" using 2 by blast

have 4: "fv⇩s⇩s⇩t (unlabel A) = fv t ∪ fv s ∪ fv⇩s⇩s⇩t AA" using iB by auto

have "fv⇩s⇩t (unlabel A') ⊆ fv⇩s⇩s⇩t (unlabel A) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)" using 1 3 4 5 by blast
thus ?case by metis
next
case (ConsNegChecks A' D X F F' AA A A')
then obtain i B where iB: "A = (i,NegChecks X F F')#B" "AA = unlabel B"
unfolding unlabel_def by moura

define D' where "D' ≡ ⋃(fv⇩p⇩a⇩i⇩r⇩s ` set (tr⇩p⇩a⇩i⇩r⇩s F' (unlabel (dbproj i D))))"
define constr where "constr = map (λG. (i,∀X⟨∨≠: (F@G)⟩⇩s⇩t)) (tr⇩p⇩a⇩i⇩r⇩s F' (map snd (dbproj i D)))"

from iB obtain A'' where *: "A'' ∈ set (tr⇩p⇩c B D)" "A' = constr@A''"
using ConsNegChecks.prems(1) unfolding constr_def by moura
hence "fv⇩l⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t AA ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
by (metis ConsNegChecks.hyps(1) iB(2))
hence **: "fv⇩l⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t AA ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)" by auto

have 1: "fv⇩l⇩s⇩t constr ⊆ (D' ∪ fv⇩p⇩a⇩i⇩r⇩s F) - set X"
unfolding D'_def constr_def unlabel_def by auto

have "set (unlabel (dbproj i D)) ⊆ set (unlabel D)" unfolding unlabel_def dbproj_def by auto
hence 2: "D' ⊆ fv⇩p⇩a⇩i⇩r⇩s F' ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D)"
using tr⇩p⇩a⇩i⇩r⇩s_vars_subset'[of F' "unlabel (dbproj i D)"] fv⇩p⇩a⇩i⇩r⇩s_mono
unfolding D'_def by blast

have 3: "fv⇩l⇩s⇩t A' ⊆ ((fv⇩p⇩a⇩i⇩r⇩s F' ∪ fv⇩p⇩a⇩i⇩r⇩s F) - set X) ∪ fv⇩p⇩a⇩i⇩r⇩s (unlabel D) ∪ fv⇩l⇩s⇩t A''"
using 1 2 *(2) unfolding unlabel_def by fastforce

have 4: "fv⇩s⇩s⇩t AA ⊆ fv⇩s⇩s⇩t (unlabel A)" by (metis ConsNegChecks.hyps(2) fv⇩s⇩s⇩t_cons_subset)

have 5: "fv⇩p⇩a⇩i⇩r⇩s F' ∪ fv⇩p⇩a⇩i⇩r⇩s F - set X ⊆ fv⇩s⇩s⇩t (unlabel A)"
using ConsNegChecks.hyps(2) unfolding unlabel_def by force

show ?case using ** 3 4 5 by blast
qed (fastforce simp add: unlabel_def)+

show ?Q using assms
apply (induct "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
by (fastforce simp add: unlabel_def)+
qed

lemma tr_par_vars_disj:
assumes "A' ∈ set (tr⇩p⇩c A D)" "fv⇩p⇩a⇩i⇩r⇩s (unlabel D) ∩ bvars⇩s⇩s⇩t (unlabel A) = {}"
and "fv⇩s⇩s⇩t (unlabel A) ∩ bvars⇩s⇩s⇩t (unlabel A) = {}"
shows "fv⇩l⇩s⇩t A' ∩ bvars⇩l⇩s⇩t A' = {}"
using assms tr_par_vars_subset by fast

lemma tr_par_trms_subset:
assumes "A' ∈ set (tr⇩p⇩c A D)"
shows "trms⇩l⇩s⇩t A' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪ pair ` snd ` set D"
using assms
proof (induction A D arbitrary: A' rule: tr⇩p⇩c.induct)
case 1 thus ?case by simp
next
case (2 i t A D)
then obtain A'' where A'': "A' = (i,send⟨t⟩⇩s⇩t)#A''" "A'' ∈ set (tr⇩p⇩c A D)" by moura
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪ pair ` snd ` set D"
by (metis "2.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (3 i t A D)
then obtain A'' where A'': "A' = (i,receive⟨t⟩⇩s⇩t)#A''" "A'' ∈ set (tr⇩p⇩c A D)"
by moura
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪ pair ` snd ` set D"
by (metis "3.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (4 i ac t t' A D)
then obtain A'' where A'': "A' = (i,⟨ac: t ≐ t'⟩⇩s⇩t)#A''" "A'' ∈ set (tr⇩p⇩c A D)"
by moura
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪ pair ` snd ` set D"
by (metis "4.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (5 i t s A D)
hence "A' ∈ set (tr⇩p⇩c A (List.insert (i,t,s) D))" by simp
hence "trms⇩l⇩s⇩t A' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪
pair ` snd ` set (List.insert (i,t,s) D)"
by (metis "5.IH")
thus ?case by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (6 i t s A D)
from 6 obtain Di A'' B C where A'':
"Di ∈ set (subseqs (dbproj i D))" "A'' ∈ set (tr⇩p⇩c A [d←D. d ∉ set Di])" "A' = (B@C)@A''"
"B = map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)) Di"
"C = map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩⇩s⇩t)) [d←dbproj i D. d ∉ set Di]"
by moura
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪
pair ` snd ` set [d←D. d ∉ set Di]"
by (metis "6.IH")
moreover have "set [d←D. d ∉ set Di] ⊆ set D" using set_filter by auto
ultimately have
"trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` setops⇩s⇩s⇩t (unlabel A) ∪ pair ` snd ` set D"
by blast
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel ((i,delete⟨t,s⟩)#A)) ∪
pair ` setops⇩s⇩s⇩t (unlabel ((i,delete⟨t,s⟩)#A)) ∪
pair ` snd ` set D"
using setops⇩s⇩s⇩t_cons_subset trms⇩s⇩s⇩t_cons
by (auto simp add: setops⇩s⇩s⇩t_def)
moreover have "set Di ⊆ set D" "set [d←dbproj i D . d ∉ set Di] ⊆ set D"
using subseqs_set_subset[OF A''(1)] unfolding dbproj_def by auto
hence "trms⇩s⇩t (unlabel B) ⊆ insert (pair (t, s)) (pair ` snd ` set D)"
"trms⇩s⇩t (unlabel C) ⊆ insert (pair (t, s)) (pair ` snd ` set D)"
using A''(4,5) unfolding unlabel_def by auto
hence "trms⇩s⇩t (unlabel (B@C)) ⊆ insert (pair (t,s)) (pair ` snd ` set D)"
using unlabel_append[of B C] by auto
moreover have "pair (t,s) ∈ pair ` setops⇩s⇩s⇩t (delete⟨t,s⟩#unlabel A)" by (simp add: setops⇩s⇩s⇩t_def)
ultimately show ?case
using A''(3) trms⇩s⇩t_append[of "unlabel (B@C)" "unlabel A'"] unlabel_append[of "B@C" A'']
by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (7 i ac t s A D)
from 7 obtain d A'' where A'':
"d ∈ set (dbproj i D)" "A'' ∈ set (tr⇩p⇩c A D)"
"A' = (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩⇩s⇩t)#A''"
by moura
hence "trms⇩l⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (unlabel A) ∪ pair ` ```