# Theory Lazy_Intruder

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

section ‹The Lazy Intruder›
theory Lazy_Intruder
imports Strands_and_Constraints Intruder_Deduction
begin

context intruder_model
begin

subsection ‹Definition of the Lazy Intruder›
text ‹The lazy intruder constraint reduction system, defined as a relation on constraint states›
inductive_set LI_rel::
"((('fun,'var) strand × (('fun,'var) subst)) ×
('fun,'var) strand × (('fun,'var) subst)) set"
and LI_rel' (infix "↝" 50)
and LI_rel_trancl (infix "↝⇧+" 50)
and LI_rel_rtrancl (infix "↝⇧*" 50)
where
"A ↝ B ≡ (A,B) ∈ LI_rel"
| "A ↝⇧+ B ≡ (A,B) ∈ LI_rel⇧+"
| "A ↝⇧* B ≡ (A,B) ∈ LI_rel⇧*"

| Compose: "⟦simple S; length T = arity f; public f⟧
⟹ (S@Send [Fun f T]#S',θ) ↝ (S@(map Send1 T)@S',θ)"
| Unify: "⟦simple S; Fun f T' ∈ ik⇩s⇩t S; Some δ = mgu (Fun f T) (Fun f T')⟧
⟹ (S@Send [Fun f T]#S',θ) ↝ ((S@S') ⋅⇩s⇩t δ,θ ∘⇩s δ)"
| Equality: "⟦simple S; Some δ = mgu t t'⟧
⟹ (S@Equality _ t t'#S',θ) ↝ ((S@S') ⋅⇩s⇩t δ,θ ∘⇩s δ)"

text ‹A "pre-processing step" to be applied before constraint reduction. It transforms constraints
such that exactly one message is transmitted in each message transmission step. It is sound and
complete and preserves the various well-formedness properties required by the lazy intruder.›
fun LI_preproc where
"LI_preproc [] = []"
| "LI_preproc (Send ts#S) = map Send1 ts@LI_preproc S"
| "LI_preproc (x#S) = x#LI_preproc S"

definition LI_preproc_prop where
"LI_preproc_prop S ≡ ∀ts. Send ts ∈ set S ∨ Receive ts ∈ set S ⟶ (∃t. ts = [t])"

subsection ‹Lemmata: Preprocessing ›
lemma LI_preproc_preproc_prop:
"LI_preproc_prop (LI_preproc S)"
by (induct S rule: LI_preproc.induct) (auto simp add: LI_preproc_prop_def)

lemma LI_preproc_sem_eq:
"⟦M; S⟧⇩c ℐ ⟷ ⟦M; LI_preproc S⟧⇩c ℐ" (is "?A ⟷ ?B")
proof
show "?A ⟹ ?B"
proof (induction S rule: strand_sem_induct)
case (ConsSnd M ts S)
hence "⟦M; LI_preproc S⟧⇩c ℐ" "⟦M; map Send1 ts⟧⇩c ℐ" using strand_sem_Send_map(5) by auto
moreover have "ik⇩s⇩t (map Send1 ts) ⋅⇩s⇩e⇩t ℐ = {}" unfolding ik⇩s⇩t_is_rcv_set by fastforce
ultimately show ?case using strand_sem_append(1) by simp
next
case (ConsRcv M ts S)
hence "⟦(set ts ⋅⇩s⇩e⇩t ℐ) ∪ M; LI_preproc S⟧⇩c ℐ" "⟦M; map Receive1 ts⟧⇩c ℐ"
moreover have "ik⇩s⇩t (map Receive1 ts) ⋅⇩s⇩e⇩t ℐ = set ts ⋅⇩s⇩e⇩t ℐ" unfolding ik⇩s⇩t_is_rcv_set by force
ultimately show ?case using strand_sem_append(1) by (simp add: Un_commute)
qed simp_all

show "?B ⟹ ?A"
proof (induction S arbitrary: M rule: LI_preproc.induct)
case (2 ts S)
have "ik⇩s⇩t (map Send1 ts) ⋅⇩s⇩e⇩t ℐ = {}" unfolding ik⇩s⇩t_is_rcv_set by fastforce
hence "⟦M; S⟧⇩c ℐ" "⟦M; map Send1 ts⟧⇩c ℐ" using 2 strand_sem_append(1) by auto
thus ?case using strand_sem_Send_map(5) by simp
next
case (3 ts S)
have "ik⇩s⇩t (map Receive1 ts) ⋅⇩s⇩e⇩t ℐ = set ts ⋅⇩s⇩e⇩t ℐ" unfolding ik⇩s⇩t_is_rcv_set by force
hence "⟦M ∪ (set ts ⋅⇩s⇩e⇩t ℐ); S⟧⇩c ℐ" "⟦M; map Receive1 ts⟧⇩c ℐ"
using 3 strand_sem_append(1) by auto
qed simp_all
qed

lemma LI_preproc_sem_eq':
"(ℐ ⊨⇩c ⟨S, θ⟩) ⟷ (ℐ ⊨⇩c ⟨LI_preproc S, θ⟩)"
using LI_preproc_sem_eq unfolding constr_sem_c_def by simp

lemma LI_preproc_vars_eq:
"fv⇩s⇩t (LI_preproc S) = fv⇩s⇩t S"
"bvars⇩s⇩t (LI_preproc S) = bvars⇩s⇩t S"
"vars⇩s⇩t (LI_preproc S) = vars⇩s⇩t S"
by (induct S rule: LI_preproc.induct) auto

lemma LI_preproc_trms_eq:
"trms⇩s⇩t (LI_preproc S) = trms⇩s⇩t S"
by (induct S rule: LI_preproc.induct) auto

lemma LI_preproc_wf⇩s⇩t:
assumes "wf⇩s⇩t X S"
shows "wf⇩s⇩t X (LI_preproc S)"
using assms
proof (induction S arbitrary: X rule: wf⇩s⇩t_induct)
case (ConsRcv X ts S)
hence "fv⇩s⇩e⇩t (set ts) ⊆ X" "wf⇩s⇩t X (LI_preproc S)" by auto
thus ?case using wf_Receive1_prefix by simp
next
case (ConsSnd X ts S)
hence "wf⇩s⇩t (X ∪ fv⇩s⇩e⇩t (set ts)) (LI_preproc S)" by simp
thus ?case using wf_Send1_prefix by simp
qed simp_all

lemma LI_preproc_preserves_wellformedness:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ"
shows "wf⇩c⇩o⇩n⇩s⇩t⇩r (LI_preproc S) θ"
using assms LI_preproc_vars_eq[of S] LI_preproc_wf⇩s⇩t[of "{}" S] unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def by argo

lemma LI_preproc_prop_SendE:
assumes "LI_preproc_prop S"
and "Send ts ∈ set S"
shows "(∃x. ts = [Var x]) ∨ (∃f T. ts = [Fun f T])"
proof -
obtain t where "ts = [t]" using assms unfolding LI_preproc_prop_def by auto
thus ?thesis by (cases t) auto
qed

lemma LI_preproc_prop_split:
"LI_preproc_prop (S@S') ⟷ LI_preproc_prop S ∧ LI_preproc_prop S'" (is "?A ⟷ ?B")
proof
show "?A ⟹ ?B"
proof (induction S)
case (Cons x S) thus ?case unfolding LI_preproc_prop_def by (cases x) auto

show "?B ⟹ ?A"
proof (induction S)
case (Cons x S) thus ?case unfolding LI_preproc_prop_def by (cases x) auto
qed

subsection ‹Lemma: The Lazy Intruder is Well-founded›
context
begin
private lemma LI_compose_measure_lt:
"((S@(map Send1 T)@S',θ⇩1), (S@Send [Fun f T]#S',θ⇩2)) ∈ measure⇩s⇩t"
using strand_fv_card_map_fun_eq[of S f T S'] strand_size_map_fun_lt[of T f]

private lemma LI_unify_measure_lt:
assumes "Some δ = mgu (Fun f T) t" "fv t ⊆ fv⇩s⇩t S"
shows "(((S@S') ⋅⇩s⇩t δ,θ⇩1), (S@Send [Fun f T]#S',θ⇩2)) ∈ measure⇩s⇩t"
proof (cases "δ = Var")
assume "δ = Var"
hence "(S@S') ⋅⇩s⇩t δ = S@S'" by blast
thus ?thesis
using strand_fv_card_rm_fun_le[of S S' f T]
by (auto simp add: measure⇩s⇩t_def size⇩s⇩t_def)
next
assume "δ ≠ Var"
then obtain v where "v ∈ fv (Fun f T) ∪ fv t" "subst_elim δ v"
using mgu_eliminates[OF assms(1)[symmetric]] by metis
hence v_in: "v ∈ fv⇩s⇩t (S@Send [Fun f T]#S')"
using assms(2) by (auto simp add: measure⇩s⇩t_def size⇩s⇩t_def)

have "range_vars δ ⊆ fv (Fun f T) ∪ fv⇩s⇩t S"
using assms(2) mgu_vars_bounded[OF assms(1)[symmetric]] by auto
hence img_bound: "range_vars δ ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')" by auto

have finite_fv: "finite (fv⇩s⇩t (S@Send [Fun f T]#S'))" by auto

have "v ∉ fv⇩s⇩t ((S@Send [Fun f T]#S') ⋅⇩s⇩t δ)"
using strand_fv_subst_subset_if_subst_elim[OF ‹subst_elim δ v›] v_in by metis
hence v_not_in: "v ∉ fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ)" by auto

have "fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ) ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
using strand_subst_fv_bounded_if_img_bounded[OF img_bound] by simp
hence "fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ) ⊂ fv⇩s⇩t (S@Send [Fun f T]#S')" using v_in v_not_in by blast
hence "card (fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ)) < card (fv⇩s⇩t (S@Send [Fun f T]#S'))"
using psubset_card_mono[OF finite_fv] by simp
thus ?thesis by (auto simp add: measure⇩s⇩t_def size⇩s⇩t_def)
qed

private lemma LI_equality_measure_lt:
assumes "Some δ = mgu t t'"
shows "(((S@S') ⋅⇩s⇩t δ,θ⇩1), (S@Equality a t t'#S',θ⇩2)) ∈ measure⇩s⇩t"
proof (cases "δ = Var")
assume "δ = Var"
hence "(S@S') ⋅⇩s⇩t δ = S@S'" by blast
thus ?thesis
using strand_fv_card_rm_eq_le[of S S' a t t']
by (auto simp add: measure⇩s⇩t_def size⇩s⇩t_def)
next
assume "δ ≠ Var"
then obtain v where "v ∈ fv t ∪ fv t'" "subst_elim δ v"
using mgu_eliminates[OF assms(1)[symmetric]] by metis
hence v_in: "v ∈ fv⇩s⇩t (S@Equality a t t'#S')" using assms by auto

have "range_vars δ ⊆ fv t ∪ fv t' ∪ fv⇩s⇩t S"
using assms mgu_vars_bounded[OF assms(1)[symmetric]] by auto
hence img_bound: "range_vars δ ⊆ fv⇩s⇩t (S@Equality a t t'#S')" by auto

have finite_fv: "finite (fv⇩s⇩t (S@Equality a t t'#S'))" by auto

have "v ∉ fv⇩s⇩t ((S@Equality a t t'#S') ⋅⇩s⇩t δ)"
using strand_fv_subst_subset_if_subst_elim[OF ‹subst_elim δ v›] v_in by metis
hence v_not_in: "v ∉ fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ)" by auto

have "fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ) ⊆ fv⇩s⇩t (S@Equality a t t'#S')"
using strand_subst_fv_bounded_if_img_bounded[OF img_bound] by simp
hence "fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ) ⊂ fv⇩s⇩t (S@Equality a t t'#S')" using v_in v_not_in by blast
hence "card (fv⇩s⇩t ((S@S') ⋅⇩s⇩t δ)) < card (fv⇩s⇩t (S@Equality a t t'#S'))"
using psubset_card_mono[OF finite_fv] by simp
thus ?thesis by (auto simp add: measure⇩s⇩t_def size⇩s⇩t_def)
qed

private lemma LI_in_measure: "(S⇩1,θ⇩1) ↝ (S⇩2,θ⇩2) ⟹ ((S⇩2,θ⇩2),(S⇩1,θ⇩1)) ∈ measure⇩s⇩t"
proof (induction rule: LI_rel.induct)
case (Compose S T f S' θ) thus ?case using LI_compose_measure_lt[of S T S'] by metis
next
case (Unify S f U δ T S' θ)
hence "fv (Fun f U) ⊆ fv⇩s⇩t S"
using fv_snd_rcv_strand_subset(2)[of S] by force
thus ?case using LI_unify_measure_lt[OF Unify.hyps(3), of S S'] by metis
qed (metis LI_equality_measure_lt)

private lemma LI_in_measure_trans: "(S⇩1,θ⇩1) ↝⇧+ (S⇩2,θ⇩2) ⟹ ((S⇩2,θ⇩2),(S⇩1,θ⇩1)) ∈ measure⇩s⇩t"
by (induction rule: trancl.induct, metis surjective_pairing LI_in_measure)
(metis (no_types, lifting) surjective_pairing LI_in_measure measure⇩s⇩t_trans trans_def)

private lemma LI_converse_wellfounded_trans: "wf ((LI_rel⇧+)¯)"
proof -
have "(LI_rel⇧+)¯ ⊆ measure⇩s⇩t" using LI_in_measure_trans by auto
thus ?thesis using measure⇩s⇩t_wellfounded wf_subset by metis
qed

private lemma LI_acyclic_trans: "acyclic (LI_rel⇧+)"
using wf_acyclic[OF LI_converse_wellfounded_trans] acyclic_converse by metis

private lemma LI_acyclic: "acyclic LI_rel"
using LI_acyclic_trans acyclic_subset by (simp add: acyclic_def)

lemma LI_no_infinite_chain: "¬(∃f. ∀i. f i ↝⇧+ f (Suc i))"
proof -
have "¬(∃f. ∀i. (f (Suc i), f i) ∈ (LI_rel⇧+)¯)"
using wf_iff_no_infinite_down_chain LI_converse_wellfounded_trans by metis
thus ?thesis by simp
qed

private lemma LI_unify_finite:
assumes "finite M"
shows "finite {((S@Send [Fun f T]#S',θ), ((S@S') ⋅⇩s⇩t δ,θ ∘⇩s δ)) | δ T'.
simple S ∧ Fun f T' ∈ M ∧ Some δ = mgu (Fun f T) (Fun f T')}"
using assms
proof (induction M rule: finite_induct)
case (insert m M) thus ?case
proof (cases m)
case (Fun g U)
let ?a = "λδ. ((S@Send [Fun f T]#S',θ), ((S@S') ⋅⇩s⇩t δ,θ ∘⇩s δ))"
let ?A = "λB. {?a δ | δ T'. simple S ∧ Fun f T' ∈ B ∧ Some δ = mgu (Fun f T) (Fun f T')}"

have "?A (insert m M) = (?A M) ∪ (?A {m})" by auto
moreover have "finite (?A {m})"
proof (cases "∃δ. Some δ = mgu (Fun f T) (Fun g U)")
case True
then obtain δ where δ: "Some δ = mgu (Fun f T) (Fun g U)" by blast

have A_m_eq: "⋀δ'. ?a δ' ∈ ?A {m} ⟹ ?a δ = ?a δ'"
proof -
fix δ' assume "?a δ' ∈ ?A {m}"
hence "∃σ. Some σ = mgu (Fun f T) (Fun g U) ∧ ?a σ = ?a δ'"
using ‹m = Fun g U› by auto
thus "?a δ = ?a δ'" by (metis δ option.inject)
qed

have "?A {m} = {} ∨ ?A {m} = {?a δ}"
proof (cases "simple S ∧ ?A {m} ≠ {}")
case True
hence "simple S" "?A {m} ≠ {}" by meson+
hence "?A {m} = {?a δ | δ. Some δ = mgu (Fun f T) (Fun g U)}" using ‹m = Fun g U› by auto
hence "?a δ ∈ ?A {m}" using δ by auto
show ?thesis
proof (rule ccontr)
assume "¬(?A {m} = {} ∨ ?A {m} = {?a δ})"
then obtain B where B: "?A {m} = insert (?a δ) B" "?a δ ∉ B" "B ≠ {}"
using ‹?A {m} ≠ {}› ‹?a δ ∈ ?A {m}› by (metis (no_types, lifting) Set.set_insert)
then obtain b where b: "?a δ ≠ b" "b ∈ B" by (metis (no_types, lifting) ex_in_conv)
then obtain δ' where δ': "b = ?a δ'" using B(1) by blast
moreover have "?a δ' ∈ ?A {m}" using B(1) b(2) δ' by auto
hence "?a δ = ?a δ'" by (blast dest!: A_m_eq)
ultimately show False using b(1) by simp
qed
qed auto
thus ?thesis by (metis (no_types, lifting) finite.emptyI finite_insert)
next
case False
hence "?A {m} = {}" using ‹m = Fun g U› by blast
thus ?thesis by (metis finite.emptyI)
qed
ultimately show ?thesis using insert.IH by auto
qed simp
qed fastforce
end

subsection ‹Lemma: The Lazy Intruder Preserves Well-formedness›
context
begin
private lemma LI_preserves_subst_wf_single:
assumes "(S⇩1,θ⇩1) ↝ (S⇩2,θ⇩2)" "fv⇩s⇩t S⇩1 ∩ bvars⇩s⇩t S⇩1 = {}" "wf⇩s⇩u⇩b⇩s⇩t θ⇩1"
and "subst_domain θ⇩1 ∩ vars⇩s⇩t S⇩1 = {}" "range_vars θ⇩1 ∩ bvars⇩s⇩t S⇩1 = {}"
shows "fv⇩s⇩t S⇩2 ∩ bvars⇩s⇩t S⇩2 = {}" "wf⇩s⇩u⇩b⇩s⇩t θ⇩2"
and "subst_domain θ⇩2 ∩ vars⇩s⇩t S⇩2 = {}" "range_vars θ⇩2 ∩ bvars⇩s⇩t S⇩2 = {}"
using assms
proof (induction rule: LI_rel.induct)
case (Compose S X f S' θ)
{ case 1 thus ?case using vars_st_snd_map by auto }
{ case 2 thus ?case using vars_st_snd_map by auto }
{ case 3 thus ?case using vars_st_snd_map by force }
{ case 4 thus ?case using vars_st_snd_map by auto }
next
case (Unify S f U δ T S' θ)
hence "fv (Fun f U) ⊆ fv⇩s⇩t S" using fv_subset_if_in_strand_ik' by blast
hence *: "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]]
unfolding range_vars_alt_def by (fastforce simp del: subst_range.simps)

have "fv⇩s⇩t (S@S') ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')" "vars⇩s⇩t (S@S') ⊆ vars⇩s⇩t (S@Send [Fun f T]#S')"
by auto
hence **: "fv⇩s⇩t (S@S' ⋅⇩s⇩t δ) ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
"vars⇩s⇩t (S@S' ⋅⇩s⇩t δ) ⊆ vars⇩s⇩t (S@Send [Fun f T]#S')"
using subst_sends_strand_fv_to_img[of "S@S'" δ]
strand_subst_vars_union_bound[of "S@S'" δ] *
by blast+

have "wf⇩s⇩u⇩b⇩s⇩t δ" by (fact mgu_gives_wellformed_subst[OF Unify.hyps(3)[symmetric]])

{ case 1
have "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Send [Fun f T]#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
thus ?case using 1 ** by blast
}
{ case 2
hence "subst_domain θ ∩ subst_domain δ = {}" "subst_domain θ ∩ range_vars δ = {}"
using * by blast+
thus ?case by (metis wf_subst_compose[OF ‹wf⇩s⇩u⇩b⇩s⇩t θ› ‹wf⇩s⇩u⇩b⇩s⇩t δ›])
}
{ case 3
hence "subst_domain θ ∩ vars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using ** by blast
moreover have "v ∈ fv⇩s⇩t (S@Send [Fun f T]#S')" when "v ∈ subst_domain δ" for v
using * that by blast
hence "subst_domain δ ∩ fv⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
using mgu_eliminates_dom[OF Unify.hyps(3)[symmetric],
THEN strand_fv_subst_subset_if_subst_elim, of _ "S@Send [Fun f T]#S'"]
unfolding subst_elim_def by auto
moreover have "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Send [Fun f T]#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
hence "subst_domain δ ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using 3(1) * by blast
ultimately show ?case
using ** * subst_domain_compose[of θ δ] vars⇩s⇩t_is_fv⇩s⇩t_bvars⇩s⇩t[of "S@S' ⋅⇩s⇩t δ"]
by blast
}
{ case 4
have ***: "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Send [Fun f T]#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
hence "range_vars δ ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using 4(1) * by blast
thus ?case using subst_img_comp_subset[of θ δ] 4(4) *** by blast
}
next
case (Equality S δ t t' a S' θ)
hence *: "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Equality a t t'#S')"
using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]]
unfolding range_vars_alt_def by fastforce

have "fv⇩s⇩t (S@S') ⊆ fv⇩s⇩t (S@Equality a t t'#S')" "vars⇩s⇩t (S@S') ⊆ vars⇩s⇩t (S@Equality a t t'#S')"
by auto
hence **: "fv⇩s⇩t (S@S' ⋅⇩s⇩t δ) ⊆ fv⇩s⇩t (S@Equality a t t'#S')"
"vars⇩s⇩t (S@S' ⋅⇩s⇩t δ) ⊆ vars⇩s⇩t (S@Equality a t t'#S')"
using subst_sends_strand_fv_to_img[of "S@S'" δ]
strand_subst_vars_union_bound[of "S@S'" δ] *
by blast+

have "wf⇩s⇩u⇩b⇩s⇩t δ" by (fact mgu_gives_wellformed_subst[OF Equality.hyps(2)[symmetric]])

{ case 1
have "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Equality a t t'#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
thus ?case using 1 ** by blast
}
{ case 2
hence "subst_domain θ ∩ subst_domain δ = {}" "subst_domain θ ∩ range_vars δ = {}"
using * by blast+
thus ?case by (metis wf_subst_compose[OF ‹wf⇩s⇩u⇩b⇩s⇩t θ› ‹wf⇩s⇩u⇩b⇩s⇩t δ›])
}
{ case 3
hence "subst_domain θ ∩ vars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using ** by blast
moreover have "v ∈ fv⇩s⇩t (S@Equality a t t'#S')" when "v ∈ subst_domain δ" for v
using * that by blast
hence "subst_domain δ ∩ fv⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
using mgu_eliminates_dom[OF Equality.hyps(2)[symmetric],
THEN strand_fv_subst_subset_if_subst_elim, of _ "S@Equality a t t'#S'"]
unfolding subst_elim_def by auto
moreover have "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Equality a t t'#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
hence "subst_domain δ ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using 3(1) * by blast
ultimately show ?case
using ** * subst_domain_compose[of θ δ] vars⇩s⇩t_is_fv⇩s⇩t_bvars⇩s⇩t[of "S@S' ⋅⇩s⇩t δ"]
by blast
}
{ case 4
have ***: "bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = bvars⇩s⇩t (S@Equality a t t'#S')"
using bvars_subst_ident[of "S@S'" δ] by auto
hence "range_vars δ ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}" using 4(1) * by blast
thus ?case using subst_img_comp_subset[of θ δ] 4(4) *** by blast
}
qed

private lemma LI_preserves_subst_wf:
assumes "(S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2)" "fv⇩s⇩t S⇩1 ∩ bvars⇩s⇩t S⇩1 = {}" "wf⇩s⇩u⇩b⇩s⇩t θ⇩1"
and "subst_domain θ⇩1 ∩ vars⇩s⇩t S⇩1 = {}" "range_vars θ⇩1 ∩ bvars⇩s⇩t S⇩1 = {}"
shows "fv⇩s⇩t S⇩2 ∩ bvars⇩s⇩t S⇩2 = {}" "wf⇩s⇩u⇩b⇩s⇩t θ⇩2"
and "subst_domain θ⇩2 ∩ vars⇩s⇩t S⇩2 = {}" "range_vars θ⇩2 ∩ bvars⇩s⇩t S⇩2 = {}"
using assms
proof (induction S⇩2 θ⇩2 rule: rtrancl_induct2)
case (step S⇩i θ⇩i S⇩j θ⇩j)
{ case 1 thus ?case using LI_preserves_subst_wf_single[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›] step.IH by metis }
{ case 2 thus ?case using LI_preserves_subst_wf_single[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›] step.IH by metis }
{ case 3 thus ?case using LI_preserves_subst_wf_single[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›] step.IH by metis }
{ case 4 thus ?case using LI_preserves_subst_wf_single[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›] step.IH by metis }
qed metis

lemma LI_preserves_wellformedness:
assumes "(S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2)" "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1"
shows "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩2 θ⇩2"
proof -
have *: "wf⇩s⇩t {} S⇩j"
when "(S⇩i, θ⇩i) ↝ (S⇩j, θ⇩j)" "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩i θ⇩i" for S⇩i θ⇩i S⇩j θ⇩j
using that
proof (induction rule: LI_rel.induct)
case (Compose S T f S' θ) thus ?case by (metis wf_send_compose wf⇩c⇩o⇩n⇩s⇩t⇩r_def)
next
case (Unify S f U δ T S' θ)
have "fv (Fun f T) ∪ fv (Fun f U) ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')" using Unify.hyps(2) by force
hence "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by (metis subset_trans)
hence "(subst_domain δ ∪ range_vars δ) ∩ bvars⇩s⇩t (S@Send [Fun f T]#S') = {}"
using Unify.prems unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def by blast
thus ?case
using wf_unify[OF _ Unify.hyps(2) MGU_is_Unifier[OF mgu_gives_MGU], of "{}",
OF _ Unify.hyps(3)[symmetric], of S'] Unify.prems(1)
next
case (Equality S δ t t' a S' θ)
have "fv t ∪ fv t' ⊆ fv⇩s⇩t (S@Equality a t t'#S')" using Equality.hyps(2) by force
hence "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Equality a t t'#S')"
using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by (metis subset_trans)
hence "(subst_domain δ ∪ range_vars δ) ∩ bvars⇩s⇩t (S@Equality a t t'#S') = {}"
using Equality.prems unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def by blast
thus ?case
using wf_equality[OF _ Equality.hyps(2)[symmetric], of "{}" S a S'] Equality.prems(1)
qed

show ?thesis using assms
proof (induction rule: rtrancl_induct2)
case (step S⇩i θ⇩i S⇩j θ⇩j) thus ?case
using LI_preserves_subst_wf_single[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›] *[OF ‹(S⇩i,θ⇩i) ↝ (S⇩j,θ⇩j)›]
by (metis wf⇩c⇩o⇩n⇩s⇩t⇩r_def)
qed simp
qed

lemma LI_preserves_trm_wf:
assumes "(S,θ) ↝⇧* (S',θ')" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
shows "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S')"
proof -
{ fix S θ S' θ'
assume "(S,θ) ↝ (S',θ')" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
hence "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S')"
proof (induction rule: LI_rel.induct)
case (Compose S T f S' θ)
hence "wf⇩t⇩r⇩m (Fun f T)"
and *: "t ∈ set S ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p t)" "t ∈ set S' ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p t)" for t
by auto
hence "wf⇩t⇩r⇩m t" when "t ∈ set T" for t using that unfolding wf⇩t⇩r⇩m_def by auto
hence "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p t)" when "t ∈ set (map Send1 T)" for t
using that unfolding wf⇩t⇩r⇩m_def by auto
thus ?case using * by force
next
case (Unify S f U δ T S' θ)
have "wf⇩t⇩r⇩m (Fun f T)" "wf⇩t⇩r⇩m (Fun f U)"
using Unify.prems(1) Unify.hyps(2) wf_trm_subterm[of _ "Fun f U"]
by (simp, force)
hence range_wf: "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Unify.hyps(3)[symmetric]] by simp

{ fix s assume "s ∈ set (S@S' ⋅⇩s⇩t δ)"
hence "∃s' ∈ set (S@S'). s = s' ⋅⇩s⇩t⇩p δ ∧ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')"
using Unify.prems(1) by (auto simp add: subst_apply_strand_def)
moreover {
fix s' assume s': "s = s' ⋅⇩s⇩t⇩p δ" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')" "s' ∈ set (S@S')"
from s'(2) have "trms⇩s⇩t⇩p (s' ⋅⇩s⇩t⇩p δ) = trms⇩s⇩t⇩p s' ⋅⇩s⇩e⇩t (rm_vars (set (bvars⇩s⇩t⇩p s')) δ)"
proof (induction s')
case (Inequality X F) thus ?case by (induct F) (auto simp add: subst_apply_pairs_def)
qed auto
hence "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s)"
using wf_trm_subst[OF wf_trms_subst_rm_vars'[OF range_wf]] ‹wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')› s'(1)
by simp
}
ultimately have "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s)" by auto
}
thus ?case by auto
next
case (Equality S δ t t' a S' θ)
hence "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m t'" by simp_all
hence range_wf: "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Equality.hyps(2)[symmetric]] by simp

{ fix s assume "s ∈ set (S@S' ⋅⇩s⇩t δ)"
hence "∃s' ∈ set (S@S'). s = s' ⋅⇩s⇩t⇩p δ ∧ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')"
using Equality.prems(1) by (auto simp add: subst_apply_strand_def)
moreover {
fix s' assume s': "s = s' ⋅⇩s⇩t⇩p δ" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')" "s' ∈ set (S@S')"
from s'(2) have "trms⇩s⇩t⇩p (s' ⋅⇩s⇩t⇩p δ) = trms⇩s⇩t⇩p s' ⋅⇩s⇩e⇩t (rm_vars (set (bvars⇩s⇩t⇩p s')) δ)"
proof (induction s')
case (Inequality X F) thus ?case by (induct F) (auto simp add: subst_apply_pairs_def)
qed auto
hence "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s)"
using wf_trm_subst[OF wf_trms_subst_rm_vars'[OF range_wf]] ‹wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s')› s'(1)
by simp
}
ultimately have "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p s)" by auto
}
thus ?case by auto
qed
}
with assms show ?thesis by (induction rule: rtrancl_induct2) metis+
qed

lemma LI_preproc_prop_subst:
"LI_preproc_prop S ⟷ LI_preproc_prop (S ⋅⇩s⇩t δ)"
proof (induction S)
case (Cons x S) thus ?case unfolding LI_preproc_prop_def by (cases x) auto

lemma LI_preserves_LI_preproc_prop:
assumes "(S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2)" "LI_preproc_prop S⇩1"
shows "LI_preproc_prop S⇩2"
using assms
proof (induction rule: rtrancl_induct2)
case (step S⇩i θ⇩i S⇩j θ⇩j)
hence "LI_preproc_prop S⇩i" by metis
with step.hyps(2) show ?case
proof (induction rule: LI_rel.induct)
case (Unify S f T' δ T S' θ) thus ?case
using LI_preproc_prop_subst LI_preproc_prop_split
by (metis append.left_neutral append_Cons)
next
case (Equality S δ t t' uu S' θ) thus ?case
using LI_preproc_prop_subst LI_preproc_prop_split
by (metis append.left_neutral append_Cons)
qed simp

end

subsection ‹Theorem: Soundness of the Lazy Intruder›
context
begin
private lemma LI_soundness_single:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1" "(S⇩1,θ⇩1) ↝ (S⇩2,θ⇩2)" "ℐ ⊨⇩c ⟨S⇩2,θ⇩2⟩"
shows "ℐ ⊨⇩c ⟨S⇩1,θ⇩1⟩"
using assms(2,1,3)
proof (induction rule: LI_rel.induct)
case (Compose S T f S' θ)
have "ik⇩s⇩t (map Send1 T) ⋅⇩s⇩e⇩t θ = {}" by fastforce
hence *: "⟦{}; S⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; map Send1 T⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ"
using Compose unfolding constr_sem_c_def
by (force, force, fastforce)

have "ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ ⊢⇩c Fun f T ⋅ ℐ"
using *(2) Compose.hyps(2) ComposeC[OF _ Compose.hyps(3), of "map (λx. x ⋅ ℐ) T"]
unfolding subst_compose_def by force
thus "ℐ ⊨⇩c ⟨S@Send [Fun f T]#S',θ⟩"
using *(1,3) ‹ℐ ⊨⇩c ⟨S@map Send1 T@S',θ⟩›
next
case (Unify S f U δ T S' θ)
have "(θ ∘⇩s δ) supports ℐ" "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ"
using Unify.prems(2) unfolding constr_sem_c_def by metis+
then obtain σ where σ: "θ ∘⇩s δ ∘⇩s σ = ℐ" unfolding subst_compose_def by auto

have θfun_id: "Fun f U ⋅ θ = Fun f U" "Fun f T ⋅ θ = Fun f T"
using Unify.prems(1) trm_subst_ident[of "Fun f U" θ]
fv_subset_if_in_strand_ik[of "Fun f U" S] Unify.hyps(2)
fv_snd_rcv_strand_subset(2)[of S]
strand_vars_split(1)[of S "Send [Fun f T]#S'"]
unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def apply blast
using Unify.prems(1) trm_subst_ident[of "Fun f T" θ]
unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def by fastforce
hence θδ_disj:
"subst_domain θ ∩ subst_domain δ = {}"
"subst_domain θ ∩ range_vars δ = {}"
"subst_domain θ ∩ range_vars θ = {}"
using trm_subst_disj mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] apply (blast,blast)
using Unify.prems(1) unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def wf⇩s⇩u⇩b⇩s⇩t_def by blast
hence θδ_support: "θ supports ℐ" "δ supports ℐ"
by (simp_all add: subst_support_comp_split[OF ‹(θ ∘⇩s δ) supports ℐ›])

have "fv (Fun f T) ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')" "fv (Fun f U) ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
using Unify.hyps(2) by force+
hence δ_vars_bound: "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Send [Fun f T]#S')"
using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by blast

have "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; [Send [Fun f T]]⟧⇩c ℐ"
proof -
from Unify.hyps(2) have "Fun f U ⋅ ℐ ∈ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ" by blast
hence "Fun f U ⋅ ℐ ∈ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ" by blast
moreover have "Unifier δ (Fun f T) (Fun f U)"
by (fact MGU_is_Unifier[OF mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]])
ultimately have "Fun f T ⋅ ℐ ∈ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ"
using σ by (metis θfun_id subst_subst_compose)
thus ?thesis by simp
qed

have "⟦{}; S⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ"
proof -
have "(S@S' ⋅⇩s⇩t δ) ⋅⇩s⇩t θ = S@S' ⋅⇩s⇩t δ" "(S@S') ⋅⇩s⇩t θ = S@S'"
proof -
have "subst_domain θ ∩ vars⇩s⇩t (S@S') = {}"
using Unify.prems(1) by (auto simp add: wf⇩c⇩o⇩n⇩s⇩t⇩r_def)
hence "subst_domain θ ∩ vars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
using θδ_disj(2) strand_subst_vars_union_bound[of "S@S'" δ] by blast
thus "(S@S' ⋅⇩s⇩t δ) ⋅⇩s⇩t θ = S@S' ⋅⇩s⇩t δ" "(S@S') ⋅⇩s⇩t θ = S@S'"
using strand_subst_comp ‹subst_domain θ ∩ vars⇩s⇩t (S@S') = {}› by (blast,blast)
qed
moreover have "subst_idem δ" by (fact mgu_gives_subst_idem[OF Unify.hyps(3)[symmetric]])
moreover have
"(subst_domain θ ∪ range_vars θ) ∩ bvars⇩s⇩t (S@S') = {}"
"(subst_domain θ ∪ range_vars θ) ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
"(subst_domain δ ∪ range_vars δ) ∩ bvars⇩s⇩t (S@S') = {}"
using wf_constr_bvars_disj[OF Unify.prems(1)]
wf_constr_bvars_disj'[OF Unify.prems(1) δ_vars_bound]
by auto
ultimately have "⟦{}; S@S'⟧⇩c ℐ"
using ‹⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ› σ
strand_sem_subst(1)[of θ "S@S' ⋅⇩s⇩t δ" "{}" "δ ∘⇩s σ"]
strand_sem_subst(2)[of θ "S@S'" "{}" "δ ∘⇩s σ"]
strand_sem_subst_subst_idem[of δ "S@S'" "{}" σ]
unfolding constr_sem_c_def
by (metis subst_compose_assoc)
thus "⟦{}; S⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ" by auto
qed

show "ℐ ⊨⇩c ⟨S@Send [Fun f T]#S',θ⟩"
using θδ_support(1) ‹⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; [Send [Fun f T]]⟧⇩c ℐ› ‹⟦{}; S⟧⇩c ℐ› ‹⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ›
next
case (Equality S δ t t' a S' θ)
have "(θ ∘⇩s δ) supports ℐ" "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ"
using Equality.prems(2) unfolding constr_sem_c_def by metis+
then obtain σ where σ: "θ ∘⇩s δ ∘⇩s σ = ℐ" unfolding subst_compose_def by auto

have "fv t ⊆ vars⇩s⇩t (S@Equality a t t'#S')" "fv t' ⊆ vars⇩s⇩t (S@Equality a t t'#S')"
by auto
moreover have "subst_domain θ ∩ vars⇩s⇩t (S@Equality a t t'#S') = {}"
using Equality.prems(1) unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def by auto
ultimately have θfun_id: "t ⋅ θ = t" "t' ⋅ θ = t'"
using trm_subst_ident[of t θ] trm_subst_ident[of t' θ]
by auto
hence θδ_disj:
"subst_domain θ ∩ subst_domain δ = {}"
"subst_domain θ ∩ range_vars δ = {}"
"subst_domain θ ∩ range_vars θ = {}"
using trm_subst_disj mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] apply (blast,blast)
using Equality.prems(1) unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def wf⇩s⇩u⇩b⇩s⇩t_def by blast
hence θδ_support: "θ supports ℐ" "δ supports ℐ"
by (simp_all add: subst_support_comp_split[OF ‹(θ ∘⇩s δ) supports ℐ›])

have "fv t ⊆ fv⇩s⇩t (S@Equality a t t'#S')" "fv t' ⊆ fv⇩s⇩t (S@Equality a t t'#S')" by auto
hence δ_vars_bound: "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t (S@Equality a t t'#S')"
using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by blast

have "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; [Equality a t t']⟧⇩c ℐ"
proof -
have "t ⋅ δ = t' ⋅ δ"
using MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
by metis
hence "t ⋅ (θ ∘⇩s δ) = t' ⋅ (θ ∘⇩s δ)" by (metis θfun_id subst_subst_compose)
hence "t ⋅ ℐ = t' ⋅ ℐ" by (metis σ subst_subst_compose)
thus ?thesis by simp
qed

have "⟦{}; S⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ"
proof -
have "(S@S' ⋅⇩s⇩t δ) ⋅⇩s⇩t θ = S@S' ⋅⇩s⇩t δ" "(S@S') ⋅⇩s⇩t θ = S@S'"
proof -
have "subst_domain θ ∩ vars⇩s⇩t (S@S') = {}"
using Equality.prems(1)
by (fastforce simp add: wf⇩c⇩o⇩n⇩s⇩t⇩r_def simp del: subst_range.simps)
hence "subst_domain θ ∩ fv⇩s⇩t (S@S') = {}" by blast
hence "subst_domain θ ∩ fv⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
using θδ_disj(2) subst_sends_strand_fv_to_img[of "S@S'" δ] by blast
thus "(S@S' ⋅⇩s⇩t δ) ⋅⇩s⇩t θ = S@S' ⋅⇩s⇩t δ" "(S@S') ⋅⇩s⇩t θ = S@S'"
using strand_subst_comp ‹subst_domain θ ∩ vars⇩s⇩t (S@S') = {}› by (blast,blast)
qed
moreover have
"(subst_domain θ ∪ range_vars θ) ∩ bvars⇩s⇩t (S@S') = {}"
"(subst_domain θ ∪ range_vars θ) ∩ bvars⇩s⇩t (S@S' ⋅⇩s⇩t δ) = {}"
"(subst_domain δ ∪ range_vars δ) ∩ bvars⇩s⇩t (S@S') = {}"
using wf_constr_bvars_disj[OF Equality.prems(1)]
wf_constr_bvars_disj'[OF Equality.prems(1) δ_vars_bound]
by auto
ultimately have "⟦{}; S@S'⟧⇩c ℐ"
using ‹⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ› σ
strand_sem_subst(1)[of θ "S@S' ⋅⇩s⇩t δ" "{}" "δ ∘⇩s σ"]
strand_sem_subst(2)[of θ "S@S'" "{}" "δ ∘⇩s σ"]
strand_sem_subst_subst_idem[of δ "S@S'" "{}" σ]
mgu_gives_subst_idem[OF Equality.hyps(2)[symmetric]]
unfolding constr_sem_c_def
by (metis subst_compose_assoc)
thus "⟦{}; S⟧⇩c ℐ" "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ" by auto
qed

show "ℐ ⊨⇩c ⟨S@Equality a t t'#S',θ⟩"
using θδ_support(1) ‹⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; [Equality a t t']⟧⇩c ℐ› ‹⟦{}; S⟧⇩c ℐ› ‹⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ›
qed

theorem LI_soundness:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1" "(LI_preproc S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2)" "ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩"
shows "ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩"
using assms(2,1,3)
proof (induction S⇩2 θ⇩2 rule: rtrancl_induct2)
case (step S⇩i θ⇩i S⇩j θ⇩j) thus ?case
using LI_preproc_preserves_wellformedness[OF ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1›]
LI_preserves_wellformedness[OF ‹(LI_preproc S⇩1, θ⇩1) ↝⇧* (S⇩i, θ⇩i)›]
LI_soundness_single[OF _ ‹(S⇩i, θ⇩i) ↝ (S⇩j, θ⇩j)› ‹ℐ ⊨⇩c ⟨S⇩j, θ⇩j⟩›]
by metis
qed (metis LI_preproc_sem_eq')
end

subsection ‹Theorem: Completeness of the Lazy Intruder›
context
begin
private lemma LI_completeness_single:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1" "ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩" "¬simple S⇩1" "LI_preproc_prop S⇩1"
shows "∃S⇩2 θ⇩2. (S⇩1,θ⇩1) ↝ (S⇩2,θ⇩2) ∧ (ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩)"
using not_simple_elim[OF ‹¬simple S⇩1›]
proof -
{ ― ‹In this case ‹S⇩1› isn't simple because it contains an equality constraint,
so we can simply proceed with the reduction by computing the MGU for the equation›
assume "∃S' S'' a t t'. S⇩1 = S'@Equality a t t'#S'' ∧ simple S'"
then obtain S a t t' S' where S⇩1: "S⇩1 = S@Equality a t t'#S'" "simple S" by moura
hence *: "wf⇩s⇩t {} S" "ℐ ⊨⇩c ⟨S, θ⇩1⟩" "θ⇩1 supports ℐ" "t ⋅ ℐ = t' ⋅ ℐ"
using ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1› wf_eq_fv[of "{}" S t t' S']
fv_snd_rcv_strand_subset(5)[of S]
by (auto simp add: constr_sem_c_def wf⇩c⇩o⇩n⇩s⇩t⇩r_def)

from * have "Unifier ℐ t t'" by simp
then obtain δ where δ:
"Some δ = mgu t t'" "subst_idem δ" "subst_domain δ ∪ range_vars δ ⊆ fv t ∪ fv t'"
using mgu_always_unifies mgu_gives_subst_idem mgu_vars_bounded by metis+

have "δ ≼⇩∘ ℐ"
using mgu_gives_MGU[OF δ(1)[symmetric]]
by (metis ‹Unifier ℐ t t'›)
hence "δ supports ℐ" using subst_support_if_mgt_subst_idem[OF _ δ(2)] by metis
hence "(θ⇩1 ∘⇩s δ) supports ℐ" using subst_support_comp ‹θ⇩1 supports ℐ› by metis

have "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ"
proof -
have "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t S⇩1" using δ(3) S⇩1(1) by auto
hence "⟦{}; S⇩1 ⋅⇩s⇩t δ⟧⇩c ℐ"
using ‹subst_idem δ› ‹δ ≼⇩∘ ℐ› ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› strand_sem_subst
wf_constr_bvars_disj'(1)[OF assms(1)]
unfolding subst_idem_def constr_sem_c_def
by (metis (no_types) subst_compose_assoc)
thus "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ" using S⇩1(1) by force
qed
moreover have "(S@Equality a t t'#S', θ⇩1) ↝ (S@S' ⋅⇩s⇩t δ, θ⇩1 ∘⇩s δ)"
using LI_rel.Equality[OF ‹simple S› δ(1)] S⇩1 by metis
ultimately have ?thesis
using S⇩1(1) ‹(θ⇩1 ∘⇩s δ) supports ℐ›
} moreover {
― ‹In this case ‹S⇩1› isn't simple because it contains a deduction constraint for a composed
term, so we must look at how this composed term is derived under the interpretation ‹ℐ››
assume "∃S' S'' ts. S⇩1 = S'@Send ts#S'' ∧ (∄x. ts = [Var x]) ∧ simple S'"
hence "∃S' S'' f T. S⇩1 = S'@Send [Fun f T]#S'' ∧ simple S'"
using LI_preproc_prop_SendE[OF ‹LI_preproc_prop S⇩1›]
by fastforce
with assms obtain S f T S' where S⇩1: "S⇩1 = S@Send [Fun f T]#S'" "simple S" by moura
hence "wf⇩s⇩t {} S" "ℐ ⊨⇩c ⟨S, θ⇩1⟩" "θ⇩1 supports ℐ"
using ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1›
by (auto simp add: constr_sem_c_def wf⇩c⇩o⇩n⇩s⇩t⇩r_def)

― ‹Lemma for a common subcase›
have fun_sat: "ℐ ⊨⇩c ⟨S@(map Send1 T)@S', θ⇩1⟩"
when T: "⋀t. t ∈ set T ⟹ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ ⊢⇩c t ⋅ ℐ"
proof -
have "⋀t. t ∈ set T ⟹ ⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; [Send1 t]⟧⇩c ℐ" using T by simp
hence "⟦ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ; map Send1 T⟧⇩c ℐ"
using ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› strand_sem_Send_map by blast
moreover have "ik⇩s⇩t (S@[Send1 (Fun f T)]) ⋅⇩s⇩e⇩t ℐ = ik⇩s⇩t (S@(map Send1 T)) ⋅⇩s⇩e⇩t ℐ" by auto
hence "⟦ik⇩s⇩t (S@(map Send1 T)) ⋅⇩s⇩e⇩t ℐ; S'⟧⇩c ℐ"
using ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› unfolding S⇩1(1) constr_sem_c_def by force
ultimately show ?thesis
using ‹ℐ ⊨⇩c ⟨S, θ⇩1⟩› strand_sem_append(1)[of "{}" S ℐ "map Send1 T"]
strand_sem_append(1)[of "{}" "S@map Send1 T" ℐ S']
unfolding constr_sem_c_def by simp
qed

from S⇩1 ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› have "ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ ⊢⇩c Fun f T ⋅ ℐ" by (auto simp add: constr_sem_c_def)
hence ?thesis
proof cases
― ‹Case 1: ‹ℐ(f(T))› has been derived using the ‹AxiomC› rule.›
case AxiomC
hence ex_t: "∃t. t ∈ ik⇩s⇩t S ∧ Fun f T ⋅ ℐ = t ⋅ ℐ" by auto
show ?thesis
proof (cases "∀T'. Fun f T' ∈ ik⇩s⇩t S ⟶ Fun f T ⋅ ℐ ≠ Fun f T' ⋅ ℐ")
― ‹Case 1.1: ‹f(T)› is equal to a variable in the intruder knowledge under ‹ℐ›.
Hence there must exists a deduction constraint in the simple prefix of the constraint
in which this variable occurs/"is sent" for the first time. Since this variable itself
cannot have been derived from the ‹AxiomC› rule (because it must be equal under the
interpretation to ‹f(T)›, which is by assumption not in the intruder knowledge under
‹ℐ›) it must be the case that we can derive it using the ‹ComposeC› rule. Hence we can
apply the ‹Compose› rule of the lazy intruder to ‹f(T)›.›
case True
have "∃v. Var v ∈ ik⇩s⇩t S ∧ Fun f T ⋅ ℐ = ℐ v"
proof -
obtain t where "t ∈ ik⇩s⇩t S" "Fun f T ⋅ ℐ = t ⋅ ℐ" using ex_t by moura
thus ?thesis
using ‹∀T'. Fun f T' ∈ ik⇩s⇩t S ⟶ Fun f T ⋅ ℐ ≠ Fun f T' ⋅ ℐ›
by (cases t) auto
qed
hence "∃v ∈ wfrestrictedvars⇩s⇩t S. Fun f T ⋅ ℐ = ℐ v"
using vars_subset_if_in_strand_ik2[of _ S] by fastforce
then obtain v S⇩p⇩r⇩e S⇩s⇩u⇩f
where S: "S = S⇩p⇩r⇩e@Send [Var v]#S⇩s⇩u⇩f" "Fun f T ⋅ ℐ = ℐ v"
"¬(∃w ∈ wfrestrictedvars⇩s⇩t S⇩p⇩r⇩e. Fun f T ⋅ ℐ = ℐ w)"
using ‹wf⇩s⇩t {} S› wf_simple_strand_first_Send_var_split[OF _ ‹simple S›, of "Fun f T" ℐ]
by auto
hence "∀w. Var w ∈ ik⇩s⇩t S⇩p⇩r⇩e ⟶ ℐ v ≠ Var w ⋅ ℐ" by force
moreover have "∀T'. Fun f T' ∈ ik⇩s⇩t S⇩p⇩r⇩e ⟶ Fun f T ⋅ ℐ ≠ Fun f T' ⋅ ℐ"
using ‹∀T'. Fun f T' ∈ ik⇩s⇩t S ⟶ Fun f T ⋅ ℐ ≠ Fun f T' ⋅ ℐ› S(1)
by (meson contra_subsetD ik_append_subset(1))
hence "∀g T'. Fun g T' ∈ ik⇩s⇩t S⇩p⇩r⇩e ⟶ ℐ v ≠ Fun g T' ⋅ ℐ" using S(2) by simp
ultimately have "∀t ∈ ik⇩s⇩t S⇩p⇩r⇩e. ℐ v ≠ t ⋅ ℐ" by (metis term.exhaust)
hence "ℐ v ∉ (ik⇩s⇩t S⇩p⇩r⇩e) ⋅⇩s⇩e⇩t ℐ" by auto

have "ik⇩s⇩t S⇩p⇩r⇩e ⋅⇩s⇩e⇩t ℐ ⊢⇩c ℐ v"
using S⇩1(1) S(1) ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩›
hence "ik⇩s⇩t S⇩p⇩r⇩e ⋅⇩s⇩e⇩t ℐ ⊢⇩c Fun f T ⋅ ℐ" using ‹Fun f T ⋅ ℐ = ℐ v› by metis
hence "length T = arity f" "public f" "⋀t. t ∈ set T ⟹ ik⇩s⇩t S⇩p⇩r⇩e ⋅⇩s⇩e⇩t ℐ ⊢⇩c t ⋅ ℐ"
using ‹Fun f T ⋅ ℐ = ℐ v› ‹ℐ v ∉ ik⇩s⇩t S⇩p⇩r⇩e ⋅⇩s⇩e⇩t ℐ›
intruder_synth.simps[of "ik⇩s⇩t S⇩p⇩r⇩e ⋅⇩s⇩e⇩t ℐ" "ℐ v"]
by auto
hence *: "⋀t. t ∈ set T ⟹ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ ⊢⇩c t ⋅ ℐ"
using S(1) by (auto intro: ideduct_synth_mono)
hence "ℐ ⊨⇩c ⟨S@(map Send1 T)@S', θ⇩1⟩" by (metis fun_sat)
moreover have "(S@Send [Fun f T]#S', θ⇩1) ↝ (S@map Send1 T@S', θ⇩1)"
by (metis LI_rel.Compose[OF ‹simple S› ‹length T = arity f› ‹public f›])
ultimately show ?thesis using S⇩1 by auto
next
― ‹Case 1.2: ‹ℐ(f(T))› can be derived from an interpreted composed term in the intruder
knowledge. Use the ‹Unify› rule on this composed term to further reduce the constraint.›
case False
then obtain T' where t: "Fun f T' ∈ ik⇩s⇩t S" "Fun f T ⋅ ℐ = Fun f T' ⋅ ℐ"
by auto
hence "fv (Fun f T') ⊆ fv⇩s⇩t S⇩1"
using S⇩1(1) fv_subset_if_in_strand_ik'[OF t(1)]
fv_snd_rcv_strand_subset(2)[of S]
by auto
from t have "Unifier ℐ (Fun f T) (Fun f T')" by simp
then obtain δ where δ:
"Some δ = mgu (Fun f T) (Fun f T')" "subst_idem δ"
"subst_domain δ ∪ range_vars δ ⊆ fv (Fun f T) ∪ fv (Fun f T')"
using mgu_always_unifies mgu_gives_subst_idem mgu_vars_bounded by metis+

have "δ ≼⇩∘ ℐ"
using mgu_gives_MGU[OF δ(1)[symmetric]]
by (metis ‹Unifier ℐ (Fun f T) (Fun f T')›)
hence "δ supports ℐ" using subst_support_if_mgt_subst_idem[OF _ δ(2)] by metis
hence "(θ⇩1 ∘⇩s δ) supports ℐ" using subst_support_comp ‹θ⇩1 supports ℐ› by metis

have "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ"
proof -
have "subst_domain δ ∪ range_vars δ ⊆ fv⇩s⇩t S⇩1"
using δ(3) S⇩1(1) ‹fv (Fun f T') ⊆ fv⇩s⇩t S⇩1›
unfolding range_vars_alt_def by (fastforce simp del: subst_range.simps)
hence "⟦{}; S⇩1 ⋅⇩s⇩t δ⟧⇩c ℐ"
using ‹subst_idem δ› ‹δ ≼⇩∘ ℐ› ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› strand_sem_subst
wf_constr_bvars_disj'(1)[OF assms(1)]
unfolding subst_idem_def constr_sem_c_def
by (metis (no_types) subst_compose_assoc)
thus "⟦{}; S@S' ⋅⇩s⇩t δ⟧⇩c ℐ" using S⇩1(1) by force
qed
moreover have "(S@Send [Fun f T]#S', θ⇩1) ↝ (S@S' ⋅⇩s⇩t δ, θ⇩1 ∘⇩s δ)"
using LI_rel.Unify[OF ‹simple S› t(1) δ(1)] S⇩1 by metis
ultimately show ?thesis
using S⇩1(1) ‹(θ⇩1 ∘⇩s δ) supports ℐ›
qed
next
― ‹Case 2: ‹ℐ(f(T))› has been derived using the ‹ComposeC› rule.
Simply use the ‹Compose› rule of the lazy intruder to proceed with the reduction.›
case (ComposeC T' g)
hence "f = g" "length T = arity f" "public f"
and "⋀x. x ∈ set T ⟹ ik⇩s⇩t S ⋅⇩s⇩e⇩t ℐ ⊢⇩c x ⋅ ℐ"
by auto
hence "ℐ ⊨⇩c ⟨S@(map Send1 T)@S', θ⇩1⟩" using fun_sat by metis
moreover have "(S⇩1, θ⇩1) ↝ (S@(map Send1 T)@S', θ⇩1)"
using S⇩1 LI_rel.Compose[OF ‹simple S› ‹length T = arity f› ‹public f›]
by metis
ultimately show ?thesis by metis
qed
} moreover have "⋀A B X F. S⇩1 = A@Inequality X F#B ⟹ ineq_model ℐ X F"
using assms(2) by (auto simp add: constr_sem_c_def)
ultimately show ?thesis using not_simple_elim[OF ‹¬simple S⇩1›] by metis
qed

theorem LI_completeness:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1" "ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩"
shows "∃S⇩2 θ⇩2. (LI_preproc S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2) ∧ simple S⇩2 ∧ (ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩)"
proof (cases "simple (LI_preproc S⇩1)")
case False
let ?Stuck = "λS⇩2 θ⇩2. ¬(∃S⇩3 θ⇩3. (S⇩2,θ⇩2) ↝ (S⇩3,θ⇩3) ∧ (ℐ ⊨⇩c ⟨S⇩3, θ⇩3⟩))"
let ?Sats = "{((S,θ),(S',θ')). (S,θ) ↝ (S',θ') ∧ (ℐ ⊨⇩c ⟨S, θ⟩) ∧ (ℐ ⊨⇩c ⟨S', θ'⟩)}"

have simple_if_stuck:
"⋀S⇩2 θ⇩2. ⟦(LI_preproc S⇩1,θ⇩1) ↝⇧+ (S⇩2,θ⇩2); ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩; ?Stuck S⇩2 θ⇩2⟧ ⟹ simple S⇩2"
using LI_preproc_preserves_wellformedness[OF ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1›]
LI_preserves_LI_preproc_prop[OF _ LI_preproc_preproc_prop]
LI_completeness_single[OF LI_preserves_wellformedness]
trancl_into_rtrancl
by metis

have base: "∃b. ((LI_preproc S⇩1,θ⇩1),b) ∈ ?Sats"
using LI_preproc_preserves_wellformedness[OF ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1›]
LI_completeness_single[OF _ _ False LI_preproc_preproc_prop]
LI_preproc_sem_eq' ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩›
by auto

have *: "⋀S θ S' θ'. ((S,θ),(S',θ')) ∈ ?Sats⇧+ ⟹ (S,θ) ↝⇧+ (S',θ') ∧ (ℐ ⊨⇩c ⟨S', θ'⟩)"
proof -
fix S θ S' θ'
assume "((S,θ),(S',θ')) ∈ ?Sats⇧+"
thus "(S,θ) ↝⇧+ (S',θ') ∧ (ℐ ⊨⇩c ⟨S', θ'⟩)"
by (induct rule: trancl_induct2) auto
qed

have "∃S⇩2 θ⇩2. ((LI_preproc S⇩1,θ⇩1),(S⇩2,θ⇩2)) ∈ ?Sats⇧+ ∧ ?Stuck S⇩2 θ⇩2"
proof (rule ccontr)
assume "¬(∃S⇩2 θ⇩2. ((LI_preproc S⇩1,θ⇩1),(S⇩2,θ⇩2)) ∈ ?Sats⇧+ ∧ ?Stuck S⇩2 θ⇩2)"
hence sat_not_stuck: "⋀S⇩2 θ⇩2. ((LI_preproc S⇩1,θ⇩1),(S⇩2,θ⇩2)) ∈ ?Sats⇧+ ⟹ ¬?Stuck S⇩2 θ⇩2" by blast

have "∀S θ. ((LI_preproc S⇩1,θ⇩1),(S,θ)) ∈ ?Sats⇧+ ⟶ (∃b. ((S,θ),b) ∈ ?Sats)"
proof (intro allI impI)
fix S θ assume a: "((LI_preproc S⇩1,θ⇩1),(S,θ)) ∈ ?Sats⇧+"
have "⋀b. ((LI_preproc S⇩1,θ⇩1),b) ∈ ?Sats⇧+ ⟹ ∃c. b ↝ c ∧ ((LI_preproc S⇩1,θ⇩1),c) ∈ ?Sats⇧+"
proof -
fix b assume in_sat: "((LI_preproc S⇩1,θ⇩1),b) ∈ ?Sats⇧+"
hence "∃c. (b,c) ∈ ?Sats" using * sat_not_stuck by (cases b) blast
thus "∃c. b ↝ c ∧ ((LI_preproc S⇩1,θ⇩1),c) ∈ ?Sats⇧+"
using trancl_into_trancl[OF in_sat] by blast
qed
hence "∃S' θ'. (S,θ) ↝ (S',θ') ∧ ((LI_preproc S⇩1,θ⇩1),(S',θ')) ∈ ?Sats⇧+" using a by auto
then obtain S' θ' where S'θ': "(S,θ) ↝ (S',θ')" "((LI_preproc S⇩1,θ⇩1),(S',θ')) ∈ ?Sats⇧+" by auto
hence "ℐ ⊨⇩c ⟨S', θ'⟩" using * by blast
moreover have "(LI_preproc S⇩1, θ⇩1) ↝⇧+ (S,θ)" using a trancl_mono by blast
ultimately have "((S,θ),(S',θ')) ∈ ?Sats" using S'θ'(1) * a by blast
thus "∃b. ((S,θ),b) ∈ ?Sats" using S'θ'(2) by blast
qed
hence "∃f. ∀i::nat. (f i, f (Suc i)) ∈ ?Sats"
using infinite_chain_intro'[OF base] by blast
moreover have "?Sats ⊆ LI_rel⇧+" by auto
hence "¬(∃f. ∀i::nat. (f i, f (Suc i)) ∈ ?Sats)"
using LI_no_infinite_chain infinite_chain_mono by blast
ultimately show False by auto
qed
hence "∃S⇩2 θ⇩2. (LI_preproc S⇩1, θ⇩1) ↝⇧+ (S⇩2, θ⇩2) ∧ simple S⇩2 ∧ (ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩)"
using simple_if_stuck * by blast
thus ?thesis by (meson trancl_into_rtrancl)
qed (use LI_preproc_sem_eq' ‹ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩› in blast)
end

subsection ‹Corollary: Soundness and Completeness as a Single Theorem›
corollary LI_soundness_and_completeness:
assumes "wf⇩c⇩o⇩n⇩s⇩t⇩r S⇩1 θ⇩1"
shows "ℐ ⊨⇩c ⟨S⇩1, θ⇩1⟩ ⟷ (∃S⇩2 θ⇩2. (LI_preproc S⇩1,θ⇩1) ↝⇧* (S⇩2,θ⇩2) ∧ simple S⇩2 ∧ (ℐ ⊨⇩c ⟨S⇩2, θ⇩2⟩))"
by (metis LI_soundness[OF assms] LI_completeness[OF assms])

end

end
```