# Theory Strands_and_Constraints

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

section ‹Strands and Symbolic Intruder Constraints›
theory Strands_and_Constraints
imports Messages More_Unification Intruder_Deduction
begin

subsection ‹Constraints, Strands and Related Definitions›
datatype poscheckvariant = Assign ("assign") | Check ("check")

text ‹
A strand (or constraint) step is either a message transmission (either a message being sent ‹Send›
or being received ‹Receive›) or a check on messages (a positive check ‹Equality›---which can be
either an "assignment" or just a check---or a negative check ‹Inequality›)
›
datatype (funs⇩s⇩t⇩p: 'a, vars⇩s⇩t⇩p: 'b) strand_step =
Send       "('a,'b) term list" ("send⟨_⟩⇩s⇩t" 80)
| Equality   poscheckvariant "('a,'b) term" "('a,'b) term" ("⟨_: _ ≐ _⟩⇩s⇩t" [80,80])
| Inequality (bvars⇩s⇩t⇩p: "'b list") "(('a,'b) term × ('a,'b) term) list" ("∀_⟨∨≠: _⟩⇩s⇩t" [80,80])
where
"bvars⇩s⇩t⇩p (Send _) = []"
| "bvars⇩s⇩t⇩p (Receive _) = []"
| "bvars⇩s⇩t⇩p (Equality _ _ _) = []"

abbreviation "Send1 t ≡ Send [t]"

text ‹
A strand is a finite sequence of strand steps (constraints and strands share the same datatype)
›
type_synonym ('a,'b) strand = "('a,'b) strand_step list"

type_synonym ('a,'b) strands = "('a,'b) strand set"

abbreviation "trms⇩p⇩a⇩i⇩r⇩s F ≡ ⋃(t,t') ∈ set F. {t,t'}"

fun trms⇩s⇩t⇩p::"('a,'b) strand_step ⇒ ('a,'b) terms" where
"trms⇩s⇩t⇩p (Send ts) = set ts"
| "trms⇩s⇩t⇩p (Receive ts) = set ts"
| "trms⇩s⇩t⇩p (Equality _ t t') = {t,t'}"
| "trms⇩s⇩t⇩p (Inequality _ F) = trms⇩p⇩a⇩i⇩r⇩s F"

lemma vars⇩s⇩t⇩p_unfold[simp]: "vars⇩s⇩t⇩p x = fv⇩s⇩e⇩t (trms⇩s⇩t⇩p x) ∪ set (bvars⇩s⇩t⇩p x)"
by (cases x) auto

text ‹The set of terms occurring in a strand›
definition trms⇩s⇩t where "trms⇩s⇩t S ≡ ⋃(trms⇩s⇩t⇩p ` set S)"

fun trms_list⇩s⇩t⇩p::"('a,'b) strand_step ⇒ ('a,'b) term list" where
"trms_list⇩s⇩t⇩p (Send ts) = ts"
| "trms_list⇩s⇩t⇩p (Receive ts) = ts"
| "trms_list⇩s⇩t⇩p (Equality _ t t') = [t,t']"
| "trms_list⇩s⇩t⇩p (Inequality _ F) = concat (map (λ(t,t'). [t,t']) F)"

text ‹The set of terms occurring in a strand (list variant)›
definition trms_list⇩s⇩t where "trms_list⇩s⇩t S ≡ remdups (concat (map trms_list⇩s⇩t⇩p S))"

text ‹The set of variables occurring in a sent message›
definition fv⇩s⇩n⇩d::"('a,'b) strand_step ⇒ 'b set" where
"fv⇩s⇩n⇩d x ≡ case x of Send t ⇒ fv⇩s⇩e⇩t (set t) | _ ⇒ {}"

text ‹The set of variables occurring in a received message›
definition fv⇩r⇩c⇩v::"('a,'b) strand_step ⇒ 'b set" where
"fv⇩r⇩c⇩v x ≡ case x of Receive t ⇒ fv⇩s⇩e⇩t (set t) | _ ⇒ {}"

text ‹The set of variables occurring in an equality constraint›
definition fv⇩e⇩q::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
"fv⇩e⇩q ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv s ∪ fv t else {} | _ ⇒ {}"

text ‹The set of variables occurring at the left-hand side of an equality constraint›
definition fv_l⇩e⇩q::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
"fv_l⇩e⇩q ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv s else {} | _ ⇒ {}"

text ‹The set of variables occurring at the right-hand side of an equality constraint›
definition fv_r⇩e⇩q::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
"fv_r⇩e⇩q ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv t else {} | _ ⇒ {}"

text ‹The free variables of inequality constraints›
definition fv⇩i⇩n⇩e⇩q::"('a,'b) strand_step ⇒ 'b set" where
"fv⇩i⇩n⇩e⇩q x ≡ case x of Inequality X F ⇒ fv⇩p⇩a⇩i⇩r⇩s F - set X | _ ⇒ {}"

fun fv⇩s⇩t⇩p::"('a,'b) strand_step ⇒ 'b set" where
"fv⇩s⇩t⇩p (Send t) = fv⇩s⇩e⇩t (set t)"
| "fv⇩s⇩t⇩p (Receive t) = fv⇩s⇩e⇩t (set t)"
| "fv⇩s⇩t⇩p (Equality _ t t') = fv t ∪ fv t'"
| "fv⇩s⇩t⇩p (Inequality X F) = (⋃(t,t') ∈ set F. fv t ∪ fv t') - set X"

text ‹The set of free variables of a strand›
definition fv⇩s⇩t::"('a,'b) strand ⇒ 'b set" where
"fv⇩s⇩t S ≡ ⋃(set (map fv⇩s⇩t⇩p S))"

text ‹The set of bound variables of a strand›
definition bvars⇩s⇩t::"('a,'b) strand ⇒ 'b set" where
"bvars⇩s⇩t S ≡ ⋃(set (map (set ∘ bvars⇩s⇩t⇩p) S))"

text ‹The set of all variables occurring in a strand›
definition vars⇩s⇩t::"('a,'b) strand ⇒ 'b set" where
"vars⇩s⇩t S ≡ ⋃(set (map vars⇩s⇩t⇩p S))"

abbreviation wfrestrictedvars⇩s⇩t⇩p::"('a,'b) strand_step ⇒ 'b set" where
"wfrestrictedvars⇩s⇩t⇩p x ≡
case x of Inequality _ _ ⇒ {} | Equality Check _ _ ⇒ {} | _ ⇒ vars⇩s⇩t⇩p x"

text ‹The variables of a strand whose occurrences might be restricted by well-formedness constraints›
definition wfrestrictedvars⇩s⇩t::"('a,'b) strand ⇒ 'b set" where
"wfrestrictedvars⇩s⇩t S ≡ ⋃(set (map wfrestrictedvars⇩s⇩t⇩p S))"

abbreviation wfvarsoccs⇩s⇩t⇩p where
"wfvarsoccs⇩s⇩t⇩p x ≡ case x of Send t ⇒ fv⇩s⇩e⇩t (set t) | Equality Assign s t ⇒ fv s | _ ⇒ {}"

text ‹The variables of a strand that occur in sent messages or in assignments›
definition wfvarsoccs⇩s⇩t where
"wfvarsoccs⇩s⇩t S ≡ ⋃(set (map wfvarsoccs⇩s⇩t⇩p S))"

text ‹The variables occurring at the right-hand side of assignment steps›
fun assignment_rhs⇩s⇩t where
"assignment_rhs⇩s⇩t [] = {}"
| "assignment_rhs⇩s⇩t (Equality Assign t t'#S) = insert t' (assignment_rhs⇩s⇩t S)"
| "assignment_rhs⇩s⇩t (x#S) = assignment_rhs⇩s⇩t S"

text ‹The set of function symbols occurring in a strand›
definition funs⇩s⇩t::"('a,'b) strand ⇒ 'a set" where
"funs⇩s⇩t S ≡ ⋃(set (map funs⇩s⇩t⇩p S))"

fun subst_apply_strand_step::"('a,'b) strand_step ⇒ ('a,'b) subst ⇒ ('a,'b) strand_step"
(infix "⋅⇩s⇩t⇩p" 51) where
"Send t ⋅⇩s⇩t⇩p θ = Send (t ⋅⇩l⇩i⇩s⇩t θ)"
| "Equality a t t' ⋅⇩s⇩t⇩p θ = Equality a (t ⋅ θ) (t' ⋅ θ)"
| "Inequality X F ⋅⇩s⇩t⇩p θ = Inequality X (F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ)"

text ‹Substitution application for strands›
definition subst_apply_strand::"('a,'b) strand ⇒ ('a,'b) subst ⇒ ('a,'b) strand"
(infix "⋅⇩s⇩t" 51) where
"S ⋅⇩s⇩t θ ≡ map (λx. x ⋅⇩s⇩t⇩p θ) S"

text ‹The semantics of inequality constraints›
definition
"ineq_model (ℐ::('a,'b) subst) X F ≡
(∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶
(∃(t,t') ∈ set F. t ⋅ δ ∘⇩s ℐ ≠ t' ⋅ δ ∘⇩s ℐ))"

fun simple⇩s⇩t⇩p where
| "simple⇩s⇩t⇩p (Send [Var v]) = True"
| "simple⇩s⇩t⇩p (Inequality X F) = (∃ℐ. ineq_model ℐ X F)"
| "simple⇩s⇩t⇩p _ = False"

text ‹Simple constraints›
definition simple where "simple S ≡ list_all simple⇩s⇩t⇩p S"

text ‹The intruder knowledge of a constraint›
fun ik⇩s⇩t::"('a,'b) strand ⇒ ('a,'b) terms" where
"ik⇩s⇩t [] = {}"
| "ik⇩s⇩t (Receive t#S) = set t ∪ (ik⇩s⇩t S)"
| "ik⇩s⇩t (_#S) = ik⇩s⇩t S"

text ‹Strand well-formedness›
fun wf⇩s⇩t::"'b set ⇒ ('a,'b) strand ⇒ bool" where
"wf⇩s⇩t V [] = True"
| "wf⇩s⇩t V (Receive ts#S) = (fv⇩s⇩e⇩t (set ts) ⊆ V ∧ wf⇩s⇩t V S)"
| "wf⇩s⇩t V (Send ts#S) = wf⇩s⇩t (V ∪ fv⇩s⇩e⇩t (set ts)) S"
| "wf⇩s⇩t V (Equality Assign s t#S) = (fv t ⊆ V ∧ wf⇩s⇩t (V ∪ fv s) S)"
| "wf⇩s⇩t V (Equality Check s t#S) = wf⇩s⇩t V S"
| "wf⇩s⇩t V (Inequality _ _#S) = wf⇩s⇩t V S"

text ‹Well-formedness of constraint states›
definition wf⇩c⇩o⇩n⇩s⇩t⇩r::"('a,'b) strand ⇒ ('a,'b) subst ⇒ bool" where
"wf⇩c⇩o⇩n⇩s⇩t⇩r S θ ≡ (wf⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩s⇩t {} S ∧ subst_domain θ ∩ vars⇩s⇩t S = {} ∧
range_vars θ ∩ bvars⇩s⇩t S = {} ∧ fv⇩s⇩t S ∩ bvars⇩s⇩t S = {})"

declare trms⇩s⇩t_def[simp]
declare fv⇩s⇩n⇩d_def[simp]
declare fv⇩r⇩c⇩v_def[simp]
declare fv⇩e⇩q_def[simp]
declare fv_l⇩e⇩q_def[simp]
declare fv_r⇩e⇩q_def[simp]
declare fv⇩i⇩n⇩e⇩q_def[simp]
declare fv⇩s⇩t_def[simp]
declare vars⇩s⇩t_def[simp]
declare bvars⇩s⇩t_def[simp]
declare wfrestrictedvars⇩s⇩t_def[simp]
declare wfvarsoccs⇩s⇩t_def[simp]

lemmas wf⇩s⇩t_induct = wf⇩s⇩t.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsEq2 ConsIneq]
lemmas ik⇩s⇩t_induct = ik⇩s⇩t.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsIneq]
lemmas assignment_rhs⇩s⇩t_induct = assignment_rhs⇩s⇩t.induct[case_names Nil ConsEq2 ConsSnd ConsRcv ConsEq ConsIneq]

subsubsection ‹Lexicographical measure on strands›
definition size⇩s⇩t::"('a,'b) strand ⇒ nat" where
"size⇩s⇩t S ≡ size_list (λx. Max (insert 0 (size ` trms⇩s⇩t⇩p x))) S"

definition measure⇩s⇩t::"((('a, 'b) strand × ('a,'b) subst) × ('a, 'b) strand × ('a,'b) subst) set"
where
"measure⇩s⇩t ≡ measures [λ(S,θ). card (fv⇩s⇩t S), λ(S,θ). size⇩s⇩t S]"

lemma measure⇩s⇩t_alt_def:
"((s,x),(t,y)) ∈ measure⇩s⇩t =
(card (fv⇩s⇩t s) < card (fv⇩s⇩t t) ∨ (card (fv⇩s⇩t s) = card (fv⇩s⇩t t) ∧ size⇩s⇩t s < size⇩s⇩t t))"

lemma measure⇩s⇩t_trans: "trans measure⇩s⇩t"
by (simp add: trans_def measure⇩s⇩t_def size⇩s⇩t_def)

subsubsection ‹Some lemmata›
lemma trms_list⇩s⇩t_is_trms⇩s⇩t: "trms⇩s⇩t S = set (trms_list⇩s⇩t S)"
unfolding trms⇩s⇩t_def trms_list⇩s⇩t_def
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma subst_apply_strand_step_def:
"s ⋅⇩s⇩t⇩p θ = (case s of
Send t ⇒ Send (t ⋅⇩l⇩i⇩s⇩t θ)
| Equality a t t' ⇒ Equality a (t ⋅ θ) (t' ⋅ θ)
| Inequality X F ⇒ Inequality X (F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ))"
by (cases s) simp_all

lemma subst_apply_strand_nil[simp]: "[] ⋅⇩s⇩t δ = []"
unfolding subst_apply_strand_def by simp

lemma finite_funs⇩s⇩t⇩p[simp]: "finite (funs⇩s⇩t⇩p x)" by (cases x) auto
lemma finite_funs⇩s⇩t[simp]: "finite (funs⇩s⇩t S)" unfolding funs⇩s⇩t_def by simp
lemma finite_trms⇩p⇩a⇩i⇩r⇩s[simp]: "finite (trms⇩p⇩a⇩i⇩r⇩s x)" by (induct x) auto
lemma finite_trms⇩s⇩t⇩p[simp]: "finite (trms⇩s⇩t⇩p x)" by (cases x) auto
lemma finite_vars⇩s⇩t⇩p[simp]: "finite (vars⇩s⇩t⇩p x)" by auto
lemma finite_bvars⇩s⇩t⇩p[simp]: "finite (set (bvars⇩s⇩t⇩p x))" by rule
lemma finite_fv⇩s⇩n⇩d[simp]: "finite (fv⇩s⇩n⇩d x)" by (cases x) auto
lemma finite_fv⇩r⇩c⇩v[simp]: "finite (fv⇩r⇩c⇩v x)" by (cases x) auto
lemma finite_fv⇩s⇩t⇩p[simp]: "finite (fv⇩s⇩t⇩p x)" by (cases x) auto
lemma finite_vars⇩s⇩t[simp]: "finite (vars⇩s⇩t S)" by simp
lemma finite_bvars⇩s⇩t[simp]: "finite (bvars⇩s⇩t S)" by simp
lemma finite_fv⇩s⇩t[simp]: "finite (fv⇩s⇩t S)" by simp

lemma finite_wfrestrictedvars⇩s⇩t⇩p[simp]: "finite (wfrestrictedvars⇩s⇩t⇩p x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfrestrictedvars⇩s⇩t[simp]: "finite (wfrestrictedvars⇩s⇩t S)"
using finite_wfrestrictedvars⇩s⇩t⇩p by auto

lemma finite_wfvarsoccs⇩s⇩t⇩p[simp]: "finite (wfvarsoccs⇩s⇩t⇩p x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfvarsoccs⇩s⇩t[simp]: "finite (wfvarsoccs⇩s⇩t S)"
using finite_wfvarsoccs⇩s⇩t⇩p by auto

lemma finite_ik⇩s⇩t[simp]: "finite (ik⇩s⇩t S)"
by (induct S rule: ik⇩s⇩t.induct) simp_all

lemma finite_assignment_rhs⇩s⇩t[simp]: "finite (assignment_rhs⇩s⇩t S)"
by (induct S rule: assignment_rhs⇩s⇩t.induct) simp_all

lemma ik⇩s⇩t_is_rcv_set: "ik⇩s⇩t A = {t | ts t. Receive ts ∈ set A ∧ t ∈ set ts}"
by (induct A rule: ik⇩s⇩t.induct) auto

shows "ik⇩s⇩t (A@[a]) ⋅⇩s⇩e⇩t ℐ = ik⇩s⇩t A ⋅⇩s⇩e⇩t ℐ"
using assms unfolding ik⇩s⇩t_is_rcv_set
by (metis (no_types, lifting) Un_iff append_Nil2 set_ConsD set_append)

lemma ik⇩s⇩tD[dest]: "t ∈ ik⇩s⇩t S ⟹ ∃ts. t ∈ set ts ∧ Receive ts ∈ set S"
by (induct S rule: ik⇩s⇩t.induct) auto

lemma ik⇩s⇩tD'[dest]: "t ∈ ik⇩s⇩t S ⟹ t ∈ trms⇩s⇩t S"
by (induct S rule: ik⇩s⇩t.induct) auto

lemma ik⇩s⇩tD''[dest]: "t ∈ subterms⇩s⇩e⇩t (ik⇩s⇩t S) ⟹ t ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t S)"
by (induct S rule: ik⇩s⇩t.induct) auto

lemma ik⇩s⇩t_subterm_exD:
assumes "t ∈ ik⇩s⇩t S"
shows "∃x ∈ set S. t ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t⇩p x)"
using assms ik⇩s⇩tD by force

lemma assignment_rhs⇩s⇩tD[dest]: "t ∈ assignment_rhs⇩s⇩t S ⟹ ∃t'. Equality Assign t' t ∈ set S"
by (induct S rule: assignment_rhs⇩s⇩t.induct) auto

lemma assignment_rhs⇩s⇩tD'[dest]: "t ∈ subterms⇩s⇩e⇩t (assignment_rhs⇩s⇩t S) ⟹ t ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t S)"
by (induct S rule: assignment_rhs⇩s⇩t.induct) auto

lemma bvars⇩s⇩t_split: "bvars⇩s⇩t (S@S') = bvars⇩s⇩t S ∪ bvars⇩s⇩t S'"
unfolding bvars⇩s⇩t_def by auto

lemma bvars⇩s⇩t_singleton: "bvars⇩s⇩t [x] = set (bvars⇩s⇩t⇩p x)"
unfolding bvars⇩s⇩t_def by auto

lemma strand_fv_bvars_disjointD:
assumes "fv⇩s⇩t S ∩ bvars⇩s⇩t S = {}" "Inequality X F ∈ set S"
shows "set X ⊆ bvars⇩s⇩t S" "fv⇩p⇩a⇩i⇩r⇩s F - set X ⊆ fv⇩s⇩t S"
using assms by (induct S) fastforce+

lemma strand_fv_bvars_disjoint_unfold:
assumes "fv⇩s⇩t S ∩ bvars⇩s⇩t S = {}" "Inequality X F ∈ set S" "Inequality Y G ∈ set S"
shows "set Y ∩ (fv⇩p⇩a⇩i⇩r⇩s F - set X) = {}"
proof -
have "set X ⊆ bvars⇩s⇩t S" "set Y ⊆ bvars⇩s⇩t S"
"fv⇩p⇩a⇩i⇩r⇩s F - set X ⊆ fv⇩s⇩t S" "fv⇩p⇩a⇩i⇩r⇩s G - set Y ⊆ fv⇩s⇩t S"
using strand_fv_bvars_disjointD[OF assms(1)] assms(2,3) by auto
thus ?thesis using assms(1) by fastforce
qed

lemma strand_subst_hom[iff]:
"(S@S') ⋅⇩s⇩t θ = (S ⋅⇩s⇩t θ)@(S' ⋅⇩s⇩t θ)" "(x#S) ⋅⇩s⇩t θ = (x ⋅⇩s⇩t⇩p θ)#(S ⋅⇩s⇩t θ)"
unfolding subst_apply_strand_def by auto

lemma strand_subst_comp: "range_vars δ ∩ bvars⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t δ ∘⇩s θ = ((S ⋅⇩s⇩t δ) ⋅⇩s⇩t θ)"
proof (induction S)
case (Cons x S)
have *: "range_vars δ ∩ bvars⇩s⇩t S = {}" "range_vars δ ∩ (set (bvars⇩s⇩t⇩p x)) = {}"
using Cons bvars⇩s⇩t_split[of "[x]" S] append_Cons inf_sup_absorb
by (metis (no_types, lifting) Int_iff Un_commute disjoint_iff_not_equal self_append_conv2,
metis append_self_conv2 bvars⇩s⇩t_singleton inf_bot_right inf_left_commute)
hence IH: "S ⋅⇩s⇩t δ ∘⇩s θ = (S ⋅⇩s⇩t δ) ⋅⇩s⇩t θ" using Cons.IH by auto
have "(x#S ⋅⇩s⇩t δ ∘⇩s θ) = (x ⋅⇩s⇩t⇩p δ ∘⇩s θ)#(S ⋅⇩s⇩t δ ∘⇩s θ)" by (metis strand_subst_hom(2))
hence "... = (x ⋅⇩s⇩t⇩p δ ∘⇩s θ)#((S ⋅⇩s⇩t δ) ⋅⇩s⇩t θ)" by (metis IH)
hence "... = ((x ⋅⇩s⇩t⇩p δ) ⋅⇩s⇩t⇩p θ)#((S ⋅⇩s⇩t δ) ⋅⇩s⇩t θ)" using rm_vars_comp[OF *(2)]
proof (induction x)
case (Inequality X F) thus ?case
by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
thus ?case using IH by auto

lemma strand_substI[intro]:
"subst_domain θ ∩ fv⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
"subst_domain θ ∩ vars⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
proof -
show "subst_domain θ ∩ vars⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
proof (induction S)
case (Cons x S)
hence "S ⋅⇩s⇩t θ = S" by auto
moreover have "vars⇩s⇩t⇩p x ∩ subst_domain θ = {}" using Cons.prems by auto
hence "x ⋅⇩s⇩t⇩p θ = x"
proof (induction x)
case (Send ts) thus ?case by (induct ts) auto
next
case (Receive ts) thus ?case by (induct ts) auto
next
case (Inequality X F) thus ?case
by (induct F) (force simp add: subst_apply_pairs_def)+
qed auto
ultimately show ?case by simp

show "subst_domain θ ∩ fv⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
proof (induction S)
case (Cons x S)
hence "S ⋅⇩s⇩t θ = S" by auto
moreover have "fv⇩s⇩t⇩p x ∩ subst_domain θ = {}"
using Cons.prems by auto
hence "x ⋅⇩s⇩t⇩p θ = x"
proof (induction x)
case (Send ts) thus ?case by (induct ts) auto
next
case (Receive ts) thus ?case by (induct ts) auto
next
case (Inequality X F) thus ?case
by (induct F) (force simp add: subst_apply_pairs_def)+
qed auto
ultimately show ?case by simp
qed

lemma strand_substI':
"fv⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
"vars⇩s⇩t S = {} ⟹ S ⋅⇩s⇩t θ = S"
by (metis inf_bot_right strand_substI(1),
metis inf_bot_right strand_substI(2))

lemma strand_subst_set: "(set (S ⋅⇩s⇩t θ)) = ((λx. x ⋅⇩s⇩t⇩p θ) ` (set S))"

lemma strand_map_inv_set_snd_rcv_subst:
assumes "finite (M::('a,'b) terms)"
shows "set ((map Send1 (inv set M)) ⋅⇩s⇩t θ) = Send1 ` (M ⋅⇩s⇩e⇩t θ)" (is ?A)
"set ((map Receive1 (inv set M)) ⋅⇩s⇩t θ) = Receive1 ` (M ⋅⇩s⇩e⇩t θ)" (is ?B)
proof -
{ fix f::"('a,'b) term ⇒ ('a,'b) strand_step"
assume f: "f = Send1 ∨ f = Receive1"
from assms have "set ((map f (inv set M)) ⋅⇩s⇩t θ) = f ` (M ⋅⇩s⇩e⇩t θ)"
proof (induction rule: finite_induct)
case empty thus ?case unfolding inv_def by auto
next
case (insert m M)
have "set (map f (inv set (insert m M)) ⋅⇩s⇩t θ) =
insert (f m ⋅⇩s⇩t⇩p θ) (set (map f (inv set M) ⋅⇩s⇩t θ))"
by (simp add: insert.hyps(1) inv_set_fset subst_apply_strand_def)
thus ?case using f insert.IH by auto
qed
}
thus "?A" "?B" by auto
qed

lemma strand_ground_subst_vars_subset:
assumes "ground (subst_range θ)" shows "vars⇩s⇩t (S ⋅⇩s⇩t θ) ⊆ vars⇩s⇩t S"
proof (induction S)
case (Cons x S)
have "vars⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p θ) ⊆ vars⇩s⇩t⇩p x" using ground_subst_fv_subset[OF assms]
proof (cases x)
case (Inequality X F)
let ?θ = "rm_vars (set X) θ"
have "fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) ⊆ fv⇩p⇩a⇩i⇩r⇩s F"
proof (induction F)
case (Cons f F)
obtain t t' where f: "f = (t,t')" by (metis surj_pair)
hence "fv⇩p⇩a⇩i⇩r⇩s (f#F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) = fv (t ⋅ ?θ) ∪ fv (t' ⋅ ?θ) ∪ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ)"
"fv⇩p⇩a⇩i⇩r⇩s (f#F) = fv t ∪ fv t' ∪ fv⇩p⇩a⇩i⇩r⇩s F"
thus ?case
using ground_subst_fv_subset[OF ground_subset[OF rm_vars_img_subset assms, of "set X"]]
Cons.IH
by (metis (no_types, lifting) Un_mono)
moreover have
"vars⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p θ) = fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ) ∪ set X"
"vars⇩s⇩t⇩p x = fv⇩p⇩a⇩i⇩r⇩s F ∪ set X"
using Inequality
ultimately show ?thesis by auto
qed auto
thus ?case using Cons.IH by auto

lemma ik_union_subset: "⋃(P ` ik⇩s⇩t S) ⊆ (⋃x ∈ (set S). ⋃(P ` trms⇩s⇩t⇩p x))"
by (induct S rule: ik⇩s⇩t.induct) auto

lemma ik_snd_empty[simp]: "ik⇩s⇩t (map Send X) = {}"
by (induct "map Send X" arbitrary: X rule: ik⇩s⇩t.induct) auto

lemma ik_snd_empty'[simp]: "ik⇩s⇩t [Send t] = {}" by simp

lemma ik_append[iff]: "ik⇩s⇩t (S@S') = ik⇩s⇩t S ∪ ik⇩s⇩t S'" by (induct S rule: ik⇩s⇩t.induct) auto

lemma ik_cons: "ik⇩s⇩t (x#S) = ik⇩s⇩t [x] ∪ ik⇩s⇩t S" using ik_append[of "[x]" S] by simp

lemma assignment_rhs_append[iff]: "assignment_rhs⇩s⇩t (S@S') = assignment_rhs⇩s⇩t S ∪ assignment_rhs⇩s⇩t S'"
by (induct S rule: assignment_rhs⇩s⇩t.induct) auto

lemma eqs_rcv_map_empty: "assignment_rhs⇩s⇩t (map Receive M) = {}"
by auto

lemma ik_rcv_map: assumes "ts ∈ set L" shows "set ts ⊆ ik⇩s⇩t (map Receive L)"
proof -
{ fix L L'
have "set ts ⊆ ik⇩s⇩t [Receive ts]" by auto
hence "set ts ⊆ ik⇩s⇩t (map Receive (L@ts#L'))" by auto
}
thus ?thesis using assms split_list_last by force
qed

lemma ik_subst: "ik⇩s⇩t (S ⋅⇩s⇩t δ) = ik⇩s⇩t S ⋅⇩s⇩e⇩t δ"
by (induct rule: ik⇩s⇩t_induct) auto

lemma ik_rcv_map': assumes "t ∈ ik⇩s⇩t (map Receive L)" shows "∃ts ∈ set L. t ∈ set ts"
using assms by force

lemma ik_append_subset[simp]: "ik⇩s⇩t S ⊆ ik⇩s⇩t (S@S')" "ik⇩s⇩t S' ⊆ ik⇩s⇩t (S@S')"
by (induct S rule: ik⇩s⇩t.induct) auto

lemma assignment_rhs_append_subset[simp]:
"assignment_rhs⇩s⇩t S ⊆ assignment_rhs⇩s⇩t (S@S')"
"assignment_rhs⇩s⇩t S' ⊆ assignment_rhs⇩s⇩t (S@S')"
by (induct S rule: assignment_rhs⇩s⇩t.induct) auto

lemma trms⇩s⇩t_cons: "trms⇩s⇩t (x#S) = trms⇩s⇩t⇩p x ∪ trms⇩s⇩t S" by simp

lemma trm_strand_subst_cong:
"t ∈ trms⇩s⇩t S ⟹ t ⋅ δ ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ)
∨ (∃X F. Inequality X F ∈ set S ∧ t ⋅ rm_vars (set X) δ ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ))"
(is "t ∈ trms⇩s⇩t S ⟹ ?P t δ S")
"t ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ) ⟹ (∃t'. t = t' ⋅ δ ∧ t' ∈ trms⇩s⇩t S)
∨ (∃X F. Inequality X F ∈ set S ∧ (∃t' ∈ trms⇩p⇩a⇩i⇩r⇩s F. t = t' ⋅ rm_vars (set X) δ))"
(is "t ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ) ⟹ ?Q t δ S")
proof -
show "t ∈ trms⇩s⇩t S ⟹ ?P t δ S"
proof (induction S)
case (Cons x S) show ?case
proof (cases "t ∈ trms⇩s⇩t S")
case True
hence "?P t δ S" using Cons by simp
thus ?thesis
by (cases x)
(metis (no_types, lifting) Un_iff list.set_intros(2) strand_subst_hom(2) trms⇩s⇩t_cons)+
next
case False
hence "t ∈ trms⇩s⇩t⇩p x" using Cons.prems by auto
thus ?thesis
proof (induction x)
case (Inequality X F)
hence "t ⋅ rm_vars (set X) δ ∈ trms⇩s⇩t⇩p (Inequality X F ⋅⇩s⇩t⇩p δ)"
by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
thus ?case by fastforce
qed
qed simp

show "t ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ) ⟹ ?Q t δ S"
proof (induction S)
case (Cons x S) show ?case
proof (cases "t ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ)")
case True
hence "?Q t δ S" using Cons by simp
thus ?thesis by (cases x) force+
next
case False
hence "t ∈ trms⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p δ)" using Cons.prems by auto
thus ?thesis
proof (induction x)
case (Inequality X F)
hence "t ∈ trms⇩s⇩t⇩p (Inequality X F) ⋅⇩s⇩e⇩t rm_vars (set X) δ"
by (induct F) (force simp add: subst_apply_pairs_def)+
thus ?case by fastforce
qed
qed simp
qed

subsection ‹Lemmata: Free Variables of Strands›
lemma fv_trm_snd_rcv[simp]:
"fv⇩s⇩e⇩t (trms⇩s⇩t⇩p (Send ts)) = fv⇩s⇩e⇩t (set ts)" "fv⇩s⇩e⇩t (trms⇩s⇩t⇩p (Receive ts)) = fv⇩s⇩e⇩t (set ts)"
by simp_all

lemma in_strand_fv_subset: "x ∈ set S ⟹ vars⇩s⇩t⇩p x ⊆ vars⇩s⇩t S"
by fastforce

lemma in_strand_fv_subset_snd: "Send ts ∈ set S ⟹ fv⇩s⇩e⇩t (set ts) ⊆ ⋃(set (map fv⇩s⇩n⇩d S))"
by fastforce

lemma in_strand_fv_subset_rcv: "Receive ts ∈ set S ⟹ fv⇩s⇩e⇩t (set ts) ⊆ ⋃(set (map fv⇩r⇩c⇩v S))"
by fastforce

lemma fv⇩s⇩n⇩dE:
assumes "v ∈ ⋃(set (map fv⇩s⇩n⇩d S))"
obtains ts where "send⟨ts⟩⇩s⇩t ∈ set S" "v ∈ fv⇩s⇩e⇩t (set ts)"
proof -
have "∃ts. send⟨ts⟩⇩s⇩t ∈ set S ∧ v ∈ fv⇩s⇩e⇩t (set ts)"
by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
fv⇩s⇩n⇩d_def strand_step.collapse(1))
thus ?thesis by (metis that)
qed

lemma fv⇩r⇩c⇩vE:
assumes "v ∈ ⋃(set (map fv⇩r⇩c⇩v S))"
obtains ts where "receive⟨ts⟩⇩s⇩t ∈ set S" "v ∈ fv⇩s⇩e⇩t (set ts)"
proof -
have "∃ts. receive⟨ts⟩⇩s⇩t ∈ set S ∧ v ∈ fv⇩s⇩e⇩t (set ts)"
by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
fv⇩r⇩c⇩v_def strand_step.collapse(2))
thus ?thesis by (metis that)
qed

lemma vars⇩s⇩t⇩pI[intro]: "x ∈ fv⇩s⇩t⇩p s ⟹ x ∈ vars⇩s⇩t⇩p s"
by (induct s rule: fv⇩s⇩t⇩p.induct) auto

lemma vars⇩s⇩tI[intro]: "x ∈ fv⇩s⇩t S ⟹ x ∈ vars⇩s⇩t S" using vars⇩s⇩t⇩pI by fastforce

lemma fv⇩s⇩t_subset_vars⇩s⇩t[simp]: "fv⇩s⇩t S ⊆ vars⇩s⇩t S" using vars⇩s⇩tI by force

lemma vars⇩s⇩t_is_fv⇩s⇩t_bvars⇩s⇩t: "vars⇩s⇩t S = fv⇩s⇩t S ∪ bvars⇩s⇩t S"
proof (induction S)
case (Cons x S) thus ?case
proof (induction x)
case (Inequality X F) thus ?case by (induct F) auto
qed auto
qed simp

lemma fv⇩s⇩t⇩p_is_subterm_trms⇩s⇩t⇩p: "x ∈ fv⇩s⇩t⇩p a ⟹ Var x ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t⇩p a)"
using var_is_subterm by (cases a) force+

lemma fv⇩s⇩t_is_subterm_trms⇩s⇩t: "x ∈ fv⇩s⇩t A ⟹ Var x ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t A)"
proof (induction A)
case (Cons a A) thus ?case using fv⇩s⇩t⇩p_is_subterm_trms⇩s⇩t⇩p by (cases "x ∈ fv⇩s⇩t A") auto
qed simp

lemma vars_st_snd_map: "vars⇩s⇩t (map Send tss) = fv⇩s⇩e⇩t (Fun f ` set tss)" by auto

lemma vars_st_rcv_map: "vars⇩s⇩t (map Receive tss) = fv⇩s⇩e⇩t (Fun f ` set tss)" by auto

lemma vars_snd_rcv_union:
"vars⇩s⇩t⇩p x = fv⇩s⇩n⇩d x ∪ fv⇩r⇩c⇩v x ∪ fv⇩e⇩q assign x ∪ fv⇩e⇩q check x ∪ fv⇩i⇩n⇩e⇩q x ∪ set (bvars⇩s⇩t⇩p x)"
proof (cases x)
case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_union:
"fv⇩s⇩t⇩p x = fv⇩s⇩n⇩d x ∪ fv⇩r⇩c⇩v x ∪ fv⇩e⇩q assign x ∪ fv⇩e⇩q check x ∪ fv⇩i⇩n⇩e⇩q x"
proof (cases x)
case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_empty[simp]: "fv⇩s⇩n⇩d x = {} ∨ fv⇩r⇩c⇩v x = {}" by (cases x) simp_all

lemma vars_snd_rcv_strand[iff]:
"vars⇩s⇩t (S::('a,'b) strand) =
(⋃(set (map fv⇩s⇩n⇩d S))) ∪ (⋃(set (map fv⇩r⇩c⇩v S))) ∪ (⋃(set (map (fv⇩e⇩q assign) S)))
∪ (⋃(set (map (fv⇩e⇩q check) S))) ∪ (⋃(set (map fv⇩i⇩n⇩e⇩q S))) ∪ bvars⇩s⇩t S"
unfolding bvars⇩s⇩t_def
proof (induction S)
case (Cons x S)
have "⋀s V. vars⇩s⇩t⇩p (s::('a,'b) strand_step) ∪ V =
fv⇩s⇩n⇩d s ∪ fv⇩r⇩c⇩v s ∪ fv⇩e⇩q assign s ∪ fv⇩e⇩q check s ∪ fv⇩i⇩n⇩e⇩q s ∪ set (bvars⇩s⇩t⇩p s) ∪ V"
by (metis vars_snd_rcv_union)
thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma fv_snd_rcv_strand[iff]:
"fv⇩s⇩t (S::('a,'b) strand) =
(⋃(set (map fv⇩s⇩n⇩d S))) ∪ (⋃(set (map fv⇩r⇩c⇩v S))) ∪ (⋃(set (map (fv⇩e⇩q assign) S)))
∪ (⋃(set (map (fv⇩e⇩q check) S))) ∪ (⋃(set (map fv⇩i⇩n⇩e⇩q S)))"
unfolding bvars⇩s⇩t_def
proof (induction S)
case (Cons x S)
have "⋀s V. fv⇩s⇩t⇩p (s::('a,'b) strand_step) ∪ V =
fv⇩s⇩n⇩d s ∪ fv⇩r⇩c⇩v s ∪ fv⇩e⇩q assign s ∪ fv⇩e⇩q check s ∪ fv⇩i⇩n⇩e⇩q s ∪ V"
by (metis fv_snd_rcv_union)
thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma vars_snd_rcv_strand2[iff]:
"wfrestrictedvars⇩s⇩t (S::('a,'b) strand) =
(⋃(set (map fv⇩s⇩n⇩d S))) ∪ (⋃(set (map fv⇩r⇩c⇩v S))) ∪ (⋃(set (map (fv⇩e⇩q assign) S)))"
by (induct S) (auto simp add: split: strand_step.split poscheckvariant.split)

lemma fv_snd_rcv_strand_subset[simp]:
"⋃(set (map fv⇩s⇩n⇩d S)) ⊆ fv⇩s⇩t S" "⋃(set (map fv⇩r⇩c⇩v S)) ⊆ fv⇩s⇩t S"
"⋃(set (map (fv⇩e⇩q ac) S)) ⊆ fv⇩s⇩t S" "⋃(set (map fv⇩i⇩n⇩e⇩q S)) ⊆ fv⇩s⇩t S"
"wfvarsoccs⇩s⇩t S ⊆ fv⇩s⇩t S"
proof -
show "⋃(set (map fv⇩s⇩n⇩d S)) ⊆ fv⇩s⇩t S" "⋃(set (map fv⇩r⇩c⇩v S)) ⊆ fv⇩s⇩t S" "⋃(set (map fv⇩i⇩n⇩e⇩q S)) ⊆ fv⇩s⇩t S"
using fv_snd_rcv_strand[of S] by auto

show "⋃(set (map (fv⇩e⇩q ac) S)) ⊆ fv⇩s⇩t S"
by (induct S) (auto split: strand_step.split poscheckvariant.split)

show "wfvarsoccs⇩s⇩t S ⊆ fv⇩s⇩t S"
by (induct S) (auto split: strand_step.split poscheckvariant.split)
qed

lemma vars_snd_rcv_strand_subset2[simp]:
"⋃(set (map fv⇩s⇩n⇩d S)) ⊆ wfrestrictedvars⇩s⇩t S" "⋃(set (map fv⇩r⇩c⇩v S)) ⊆ wfrestrictedvars⇩s⇩t S"
"⋃(set (map (fv⇩e⇩q assign) S)) ⊆ wfrestrictedvars⇩s⇩t S" "wfvarsoccs⇩s⇩t S ⊆ wfrestrictedvars⇩s⇩t S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma wfrestrictedvars⇩s⇩t_subset_vars⇩s⇩t: "wfrestrictedvars⇩s⇩t S ⊆ vars⇩s⇩t S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma subst_sends_strand_step_fv_to_img: "fv⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p δ) ⊆ fv⇩s⇩t⇩p x ∪ range_vars δ"
using subst_sends_fv_to_img[of _ δ]
proof (cases x)
case (Inequality X F)
let ?θ = "rm_vars (set X) δ"
have "fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) ⊆ fv⇩p⇩a⇩i⇩r⇩s F ∪ range_vars ?θ"
proof (induction F)
case (Cons f F) thus ?case
using subst_sends_fv_to_img[of _ ?θ]
hence "fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) ⊆ fv⇩p⇩a⇩i⇩r⇩s F ∪ range_vars δ"
using rm_vars_img_subset[of "set X" δ] fv_set_mono
unfolding range_vars_alt_def by blast+
thus ?thesis using Inequality by (auto simp add: subst_apply_strand_step_def)

lemma subst_sends_strand_fv_to_img: "fv⇩s⇩t (S ⋅⇩s⇩t δ) ⊆ fv⇩s⇩t S ∪ range_vars δ"
proof (induction S)
case (Cons x S)
have *: "fv⇩s⇩t (x#S ⋅⇩s⇩t δ) = fv⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p δ) ∪ fv⇩s⇩t (S ⋅⇩s⇩t δ)"
"fv⇩s⇩t (x#S) ∪ range_vars δ = fv⇩s⇩t⇩p x ∪ fv⇩s⇩t S ∪ range_vars δ"
by auto
thus ?case using Cons.IH subst_sends_strand_step_fv_to_img[of x δ] by auto
qed simp

lemma ineq_apply_subst:
assumes "subst_domain δ ∩ set X = {}"
shows "(Inequality X F) ⋅⇩s⇩t⇩p δ = Inequality X (F ⋅⇩p⇩a⇩i⇩r⇩s δ)"
using rm_vars_apply'[OF assms] by (simp add: subst_apply_strand_step_def)

lemma fv_strand_step_subst:
assumes "P = fv⇩s⇩t⇩p ∨ P = fv⇩r⇩c⇩v ∨ P = fv⇩s⇩n⇩d ∨ P = fv⇩e⇩q ac ∨ P = fv⇩i⇩n⇩e⇩q"
and "set (bvars⇩s⇩t⇩p x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv⇩s⇩e⇩t (δ ` (P x)) = P (x ⋅⇩s⇩t⇩p δ)"
proof (cases x)
case (Send ts)
hence "vars⇩s⇩t⇩p x = fv⇩s⇩e⇩t (set ts)" "fv⇩s⇩n⇩d x = fv⇩s⇩e⇩t (set ts)" by auto
thus ?thesis using assms Send subst_apply_fv_unfold[of _ δ] by fastforce
next
hence "vars⇩s⇩t⇩p x = fv⇩s⇩e⇩t (set ts)" "fv⇩r⇩c⇩v x = fv⇩s⇩e⇩t (set ts)" by auto
thus ?thesis using assms Receive subst_apply_fv_unfold[of _ δ] by fastforce
next
case (Equality ac' t t') show ?thesis
proof (cases "ac = ac'")
case True
hence "vars⇩s⇩t⇩p x = fv t ∪ fv t'" "fv⇩e⇩q ac x = fv t ∪ fv t'"
using Equality
by auto
thus ?thesis
using assms Equality subst_apply_fv_unfold[of _ δ] True
by auto
next
case False
hence "vars⇩s⇩t⇩p x = fv t ∪ fv t'" "fv⇩e⇩q ac x = {}"
using Equality
by auto
thus ?thesis
using assms Equality subst_apply_fv_unfold[of _ δ] False
by auto
qed
next
case (Inequality X F)
hence 1: "set X ∩ (subst_domain δ ∪ range_vars δ) = {}"
"x ⋅⇩s⇩t⇩p δ = Inequality X (F ⋅⇩p⇩a⇩i⇩r⇩s δ)"
"rm_vars (set X) δ = δ"
using assms ineq_apply_subst[of δ X F] rm_vars_apply'[of δ "set X"]
unfolding range_vars_alt_def by force+

have 2: "fv⇩i⇩n⇩e⇩q x = fv⇩p⇩a⇩i⇩r⇩s F - set X" using Inequality by auto
hence "fv⇩s⇩e⇩t (δ ` fv⇩i⇩n⇩e⇩q x) = fv⇩s⇩e⇩t (δ ` fv⇩p⇩a⇩i⇩r⇩s F) - set X"
using fv⇩s⇩e⇩t_subst_img_eq[OF 1(1), of "fv⇩p⇩a⇩i⇩r⇩s F"] by simp
hence 3: "fv⇩s⇩e⇩t (δ ` fv⇩i⇩n⇩e⇩q x) = fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s δ) - set X" by (metis fv⇩p⇩a⇩i⇩r⇩s_step_subst)

have 4: "fv⇩i⇩n⇩e⇩q (x ⋅⇩s⇩t⇩p δ) = fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s δ) - set X" using 1(2) by auto

show ?thesis
using assms(1) Inequality subst_apply_fv_unfold[of _ δ] 1(2) 2 3 4
unfolding fv⇩e⇩q_def fv⇩r⇩c⇩v_def fv⇩s⇩n⇩d_def
by (metis (no_types) Sup_empty image_empty fv⇩p⇩a⇩i⇩r⇩s.simps fv⇩s⇩e⇩t.simps
fv⇩s⇩t⇩p.simps(4) strand_step.simps(20))
qed

lemma fv_strand_subst:
assumes "P = fv⇩s⇩t⇩p ∨ P = fv⇩r⇩c⇩v ∨ P = fv⇩s⇩n⇩d ∨ P = fv⇩e⇩q ac ∨ P = fv⇩i⇩n⇩e⇩q"
and "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv⇩s⇩e⇩t (δ ` (⋃(set (map P S)))) = ⋃(set (map P (S ⋅⇩s⇩t δ)))"
using assms(2)
proof (induction S)
case (Cons x S)
hence *: "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
"set (bvars⇩s⇩t⇩p x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
unfolding bvars⇩s⇩t_def by force+
hence **: "fv⇩s⇩e⇩t (δ ` P x) = P (x ⋅⇩s⇩t⇩p δ)" using fv_strand_step_subst[OF assms(1), of x δ] by auto
have "fv⇩s⇩e⇩t (δ ` (⋃(set (map P (x#S))))) = fv⇩s⇩e⇩t (δ ` P x) ∪ (⋃(set (map P ((S ⋅⇩s⇩t δ)))))"
using Cons unfolding range_vars_alt_def bvars⇩s⇩t_def by force
hence "fv⇩s⇩e⇩t (δ ` (⋃(set (map P (x#S))))) = P (x ⋅⇩s⇩t⇩p δ) ∪ fv⇩s⇩e⇩t (δ ` (⋃(set (map P S))))"
using ** by simp
thus ?case using Cons.IH[OF *(1)] unfolding bvars⇩s⇩t_def by simp
qed simp

lemma fv_strand_subst2:
assumes "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv⇩s⇩e⇩t (δ ` (wfrestrictedvars⇩s⇩t S)) = wfrestrictedvars⇩s⇩t (S ⋅⇩s⇩t δ)"
by (metis (no_types, lifting) assms fv⇩s⇩e⇩t.simps vars_snd_rcv_strand2 fv_strand_subst UN_Un image_Un)

lemma fv_strand_subst':
assumes "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv⇩s⇩e⇩t (δ ` (fv⇩s⇩t S)) = fv⇩s⇩t (S ⋅⇩s⇩t δ)"
by (metis assms fv_strand_subst fv⇩s⇩t_def)

lemma fv_trms⇩p⇩a⇩i⇩r⇩s_is_fv⇩p⇩a⇩i⇩r⇩s:
"fv⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F) = fv⇩p⇩a⇩i⇩r⇩s F"
by auto

lemma fv⇩p⇩a⇩i⇩r⇩s_in_fv_trms⇩p⇩a⇩i⇩r⇩s: "x ∈ fv⇩p⇩a⇩i⇩r⇩s F ⟹ x ∈ fv⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F)"
using fv_trms⇩p⇩a⇩i⇩r⇩s_is_fv⇩p⇩a⇩i⇩r⇩s[of F] by blast

lemma trms⇩s⇩t_append: "trms⇩s⇩t (A@B) = trms⇩s⇩t A ∪ trms⇩s⇩t B"
by auto

lemma trms⇩p⇩a⇩i⇩r⇩s_subst: "trms⇩p⇩a⇩i⇩r⇩s (a ⋅⇩p⇩a⇩i⇩r⇩s θ) = trms⇩p⇩a⇩i⇩r⇩s a ⋅⇩s⇩e⇩t θ"

lemma trms⇩p⇩a⇩i⇩r⇩s_fv_subst_subset:
"t ∈ trms⇩p⇩a⇩i⇩r⇩s F ⟹ fv (t ⋅ θ) ⊆ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s θ)"

lemma trms⇩p⇩a⇩i⇩r⇩s_fv_subst_subset':
fixes t::"('a,'b) term" and θ::"('a,'b) subst"
assumes "t ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F)"
shows "fv (t ⋅ θ) ⊆ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s θ)"
proof -
{ fix x assume "x ∈ fv t"
hence "x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
using fv_subset[OF assms] fv_subterms_set[of "trms⇩p⇩a⇩i⇩r⇩s F"] fv_trms⇩p⇩a⇩i⇩r⇩s_is_fv⇩p⇩a⇩i⇩r⇩s[of F]
by blast
hence "fv (θ x) ⊆ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s θ)" using fv⇩p⇩a⇩i⇩r⇩s_subst_fv_subset by fast
} thus ?thesis by (meson fv_subst_obtain_var subset_iff)
qed

lemma trms⇩p⇩a⇩i⇩r⇩s_funs_term_cases:
assumes "t ∈ trms⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s θ)" "f ∈ funs_term t"
shows "(∃u ∈ trms⇩p⇩a⇩i⇩r⇩s F. f ∈ funs_term u) ∨ (∃x ∈ fv⇩p⇩a⇩i⇩r⇩s F. f ∈ funs_term (θ x))"
using assms(1)
proof (induction F)
case (Cons g F)
obtain s u where g: "g = (s,u)" by (metis surj_pair)
show ?case
proof (cases "t ∈ trms⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s θ)")
case False
thus ?thesis
using assms(2) Cons.prems g funs_term_subst[of _ θ]
qed (use Cons.IH in fastforce)
qed simp

lemma trm⇩s⇩t⇩p_subst:
assumes "subst_domain θ ∩ set (bvars⇩s⇩t⇩p a) = {}"
shows "trms⇩s⇩t⇩p (a ⋅⇩s⇩t⇩p θ) = trms⇩s⇩t⇩p a ⋅⇩s⇩e⇩t θ"
proof -
have "rm_vars (set (bvars⇩s⇩t⇩p a)) θ = θ" using assms by force
thus ?thesis
using assms
by (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def
split: strand_step.splits)
qed

lemma trms⇩s⇩t_subst:
assumes "subst_domain θ ∩ bvars⇩s⇩t A = {}"
shows "trms⇩s⇩t (A ⋅⇩s⇩t θ) = trms⇩s⇩t A ⋅⇩s⇩e⇩t θ"
using assms
proof (induction A)
case (Cons a A)
have 1: "subst_domain θ ∩ bvars⇩s⇩t A = {}" "subst_domain θ ∩ set (bvars⇩s⇩t⇩p a) = {}"
using Cons.prems by auto
hence IH: "trms⇩s⇩t A ⋅⇩s⇩e⇩t θ = trms⇩s⇩t (A ⋅⇩s⇩t θ)" using Cons.IH by simp

have "trms⇩s⇩t (a#A) = trms⇩s⇩t⇩p a ∪ trms⇩s⇩t A" by auto
hence 2: "trms⇩s⇩t (a#A) ⋅⇩s⇩e⇩t θ = (trms⇩s⇩t⇩p a ⋅⇩s⇩e⇩t θ) ∪ (trms⇩s⇩t A ⋅⇩s⇩e⇩t θ)" by (metis image_Un)

have "trms⇩s⇩t (a#A ⋅⇩s⇩t θ) = (trms⇩s⇩t⇩p (a ⋅⇩s⇩t⇩p θ)) ∪ trms⇩s⇩t (A ⋅⇩s⇩t θ)"
hence 3: "trms⇩s⇩t (a#A ⋅⇩s⇩t θ) = (trms⇩s⇩t⇩p a ⋅⇩s⇩e⇩t θ) ∪ trms⇩s⇩t (A ⋅⇩s⇩t θ)"
using trm⇩s⇩t⇩p_subst[OF 1(2)] by auto

show ?case using IH 2 3 by metis

lemma strand_map_set_subst:
assumes δ: "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "⋃(set (map trms⇩s⇩t⇩p (S ⋅⇩s⇩t δ))) = (⋃(set (map trms⇩s⇩t⇩p S))) ⋅⇩s⇩e⇩t δ"
using assms
proof (induction S)
case (Cons x S)
hence "bvars⇩s⇩t [x] ∩ subst_domain δ = {}" "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
unfolding bvars⇩s⇩t_def by force+
hence *: "subst_domain δ ∩ set (bvars⇩s⇩t⇩p x) = {}"
"⋃(set (map trms⇩s⇩t⇩p (S ⋅⇩s⇩t δ))) = ⋃(set (map trms⇩s⇩t⇩p S)) ⋅⇩s⇩e⇩t δ"
using Cons.IH(1) bvars⇩s⇩t_singleton[of x] by auto
hence "trms⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p δ) = (trms⇩s⇩t⇩p x) ⋅⇩s⇩e⇩t δ"
proof (cases x)
case (Inequality X F)
thus ?thesis
using rm_vars_apply'[of δ "set X"] *
by (metis (no_types, lifting) image_cong trm⇩s⇩t⇩p_subst)
qed simp_all
thus ?case using * subst_all_insert by auto
qed simp

lemma subst_apply_fv_subset_strand_trm:
assumes P: "P = fv⇩s⇩t⇩p ∨ P = fv⇩r⇩c⇩v ∨ P = fv⇩s⇩n⇩d ∨ P = fv⇩e⇩q ac ∨ P = fv⇩i⇩n⇩e⇩q"
and fv_sub: "fv t ⊆ ⋃(set (map P S)) ∪ V"
and δ: "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv (t ⋅ δ) ⊆ ⋃(set (map P (S ⋅⇩s⇩t δ))) ∪ fv⇩s⇩e⇩t (δ ` V)"
using fv_strand_subst[OF P δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand_trm2:
assumes fv_sub: "fv t ⊆ wfrestrictedvars⇩s⇩t S ∪ V"
and δ: "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "fv (t ⋅ δ) ⊆ wfrestrictedvars⇩s⇩t (S ⋅⇩s⇩t δ) ∪ fv⇩s⇩e⇩t (δ ` V)"
using fv_strand_subst2[OF δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand:
assumes P: "P = fv⇩s⇩t⇩p ∨ P = fv⇩r⇩c⇩v ∨ P = fv⇩s⇩n⇩d ∨ P = fv⇩e⇩q ac ∨ P = fv⇩i⇩n⇩e⇩q"
and P_subset: "P x ⊆ ⋃(set (map P S)) ∪ V"
and δ: "bvars⇩s⇩t S ∩ (subst_domain δ ∪ range_vars δ) = {}"
"set (bvars⇩s⇩t⇩p x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
shows "P (x ⋅⇩s⇩t⇩p δ) ⊆ ⋃(set (map P (S ⋅⇩s⇩t δ))) ∪ fv⇩s⇩e⇩t (δ ` V)"
proof (cases x)
case (Send ts)
hence *: "fv⇩s⇩t⇩p x = fv⇩s⇩e⇩t (set ts)" "fv⇩s⇩t⇩p (x ⋅⇩s⇩t⇩p δ) = fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ)"
"fv⇩r⇩c⇩v x = {}" "fv⇩r⇩c⇩v (x ⋅⇩s⇩t⇩p δ) = {}"
"fv⇩s⇩n⇩d x = fv⇩s⇩e⇩t (set ts)" "fv⇩s⇩n⇩d (x ⋅⇩s⇩t⇩p δ) = fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ)"
"fv⇩e⇩q ac x = {}" "fv⇩e⇩q ac (x ⋅⇩s⇩t⇩p δ) = {}"
"fv⇩i⇩n⇩e⇩q x = {}" "fv⇩i⇩n⇩e⇩q (x ⋅⇩s⇩t⇩p δ) = {}"
by auto
hence **: "(P x = fv⇩s⇩e⇩t (set ts) ∧ P (x ⋅⇩s⇩t⇩p δ) = fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ)) ∨
(P x = {} ∧ P (x ⋅⇩s⇩t⇩p δ) = {})"
by (metis P)
moreover
{ assume "P x = {}" "P (x ⋅⇩s⇩t⇩p δ) = {}" hence ?thesis by simp }
moreover
{ assume "P x = fv⇩s⇩e⇩t (set ts)" "P (x ⋅⇩s⇩t⇩p δ) = fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ)"
hence "fv⇩s⇩e⇩t (set ts) ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
hence "fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ) ⊆ ⋃(set (map P (S ⋅⇩s⇩t δ))) ∪ fv⇩s⇩e⇩t (δ ` V)"
using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _ V] by fastforce
hence ?thesis using ‹P (x ⋅⇩s⇩t⇩p δ) = fv⇩s⇩e⇩t (set ts ⋅⇩s⇩e⇩t δ)› by force
}
ultimately show ?thesis by metis
next