Theory Stateful_Strands

(*  Title:      Stateful_Strands.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)


section ‹Stateful Strands›
theory Stateful_Strands
imports Strands_and_Constraints
begin

subsection ‹Stateful Constraints›
datatype (funssstp: 'a, varssstp: 'b) stateful_strand_step = 
  Send (the_msgs: "('a,'b) term list") ("send⟨_⟩" 80)
| Receive (the_msgs: "('a,'b) term list") ("receive⟨_⟩" 80)
| Equality (the_check: poscheckvariant) (the_lhs: "('a,'b) term") (the_rhs: "('a,'b) term")
    ("⟨_: _ ≐ _⟩" [80,80])
| Insert (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") ("insert⟨_,_⟩" 80)
| Delete (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") ("delete⟨_,_⟩" 80)
| InSet (the_check: poscheckvariant) (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term")
    ("⟨_: _ ∈ _⟩" [80,80])
| NegChecks (bvarssstp: "'b list")
    (the_eqs: "(('a,'b) term × ('a,'b) term) list")
    (the_ins: "(('a,'b) term × ('a,'b) term) list")
    ("∀_⟨∨≠: _ ∨∉: _⟩" [80,80])
where
  "bvarssstp (Send _) = []"
| "bvarssstp (Receive _) = []"
| "bvarssstp (Equality _ _ _) = []"
| "bvarssstp (Insert _ _) = []"
| "bvarssstp (Delete _ _) = []"
| "bvarssstp (InSet _ _ _) = []"

type_synonym ('a,'b) stateful_strand = "('a,'b) stateful_strand_step list"
type_synonym ('a,'b) dbstatelist = "(('a,'b) term × ('a,'b) term) list"
type_synonym ('a,'b) dbstate = "(('a,'b) term × ('a,'b) term) set"

abbreviation
  "is_Assignment x ≡ (is_Equality x ∨ is_InSet x) ∧ the_check x = Assign"

abbreviation
  "is_Check x ≡ ((is_Equality x ∨ is_InSet x) ∧ the_check x = Check) ∨ is_NegChecks x"

abbreviation
  "is_Check_or_Assignment x ≡ is_Equality x ∨ is_InSet x ∨ is_NegChecks x"

abbreviation
  "is_Update x ≡ is_Insert x ∨ is_Delete x"

abbreviation InSet_select ("select⟨_,_⟩") where "select⟨t,s⟩ ≡ InSet Assign t s"
abbreviation InSet_check ("⟨_ in _⟩") where "⟨t in s⟩ ≡ InSet Check t s"
abbreviation Equality_assign ("⟨_ := _⟩") where "⟨t := s⟩ ≡ Equality Assign t s"
abbreviation Equality_check ("⟨_ == _⟩") where "⟨t == s⟩ ≡ Equality Check t s"

abbreviation NegChecks_Inequality1 ("⟨_ != _⟩") where
  "⟨t != s⟩ ≡ NegChecks [] [(t,s)] []"

abbreviation NegChecks_Inequality2 ("∀_⟨_ != _⟩") where
  "∀x⟨t != s⟩ ≡ NegChecks [x] [(t,s)] []"

abbreviation NegChecks_Inequality3 ("∀_,_⟨_ != _⟩") where
  "∀x,y⟨t != s⟩ ≡ NegChecks [x,y] [(t,s)] []"

abbreviation NegChecks_Inequality4 ("∀_,_,_⟨_ != _⟩") where
  "∀x,y,z⟨t != s⟩ ≡ NegChecks [x,y,z] [(t,s)] []"

abbreviation NegChecks_NotInSet1 ("⟨_ not in _⟩") where
  "⟨t not in s⟩ ≡ NegChecks [] [] [(t,s)]"

abbreviation NegChecks_NotInSet2 ("∀_⟨_ not in _⟩") where
  "∀x⟨t not in s⟩ ≡ NegChecks [x] [] [(t,s)]"

abbreviation NegChecks_NotInSet3 ("∀_,_⟨_ not in _⟩") where
  "∀x,y⟨t not in s⟩ ≡ NegChecks [x,y] [] [(t,s)]"

abbreviation NegChecks_NotInSet4 ("∀_,_,_⟨_ not in _⟩") where
  "∀x,y,z⟨t not in s⟩ ≡ NegChecks [x,y,z] [] [(t,s)]"

fun trmssstp where
  "trmssstp (Send ts) = set ts"
| "trmssstp (Receive ts) = set ts"
| "trmssstp (Equality _ t t') = {t,t'}"
| "trmssstp (Insert t t') = {t,t'}"
| "trmssstp (Delete t t') = {t,t'}"
| "trmssstp (InSet _ t t') = {t,t'}"
| "trmssstp (NegChecks _ F F') = trmspairs F ∪ trmspairs F'"

definition trmssst where "trmssst S ≡ ⋃(trmssstp ` set S)"
declare trmssst_def[simp]

fun trms_listsstp where
  "trms_listsstp (Send ts) = ts"
| "trms_listsstp (Receive ts) = ts"
| "trms_listsstp (Equality _ t t') = [t,t']"
| "trms_listsstp (Insert t t') = [t,t']"
| "trms_listsstp (Delete t t') = [t,t']"
| "trms_listsstp (InSet _ t t') = [t,t']"
| "trms_listsstp (NegChecks _ F F') = concat (map (λ(t,t'). [t,t']) (F@F'))"

definition trms_listsst where "trms_listsst S ≡ remdups (concat (map trms_listsstp S))"

definition iksst where "iksst A ≡ {t | t ts. Receive ts ∈ set A ∧ t ∈ set ts}"

definition bvarssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "bvarssst S ≡ ⋃(set (map (set ∘ bvarssstp) S))"

fun fvsstp::"('a,'b) stateful_strand_step ⇒ 'b set" where
  "fvsstp (Send ts) = fvset (set ts)"
| "fvsstp (Receive ts) = fvset (set ts)"
| "fvsstp (Equality _ t t') = fv t ∪ fv t'"
| "fvsstp (Insert t t') = fv t ∪ fv t'"
| "fvsstp (Delete t t') = fv t ∪ fv t'"
| "fvsstp (InSet _ t t') = fv t ∪ fv t'"
| "fvsstp (NegChecks X F F') = fvpairs F ∪ fvpairs F' - set X"

definition fvsst::"('a,'b) stateful_strand ⇒ 'b set" where
  "fvsst S ≡ ⋃(set (map fvsstp S))"

fun fv_listsstp where
  "fv_listsstp (send⟨ts⟩) = concat (map fv_list ts)"
| "fv_listsstp (receive⟨ts⟩) = concat (map fv_list ts)"
| "fv_listsstp (⟨_: t ≐ s⟩) = fv_list t@fv_list s"
| "fv_listsstp (insert⟨t,s⟩) = fv_list t@fv_list s"
| "fv_listsstp (delete⟨t,s⟩) = fv_list t@fv_list s"
| "fv_listsstp (⟨_: t ∈ s⟩) = fv_list t@fv_list s"
| "fv_listsstp (∀X⟨∨≠: F ∨∉: F'⟩) = filter (λx. x ∉ set X) (fv_listpairs (F@F'))"

definition fv_listsst where
  "fv_listsst S ≡ remdups (concat (map fv_listsstp S))"

declare bvarssst_def[simp]
declare fvsst_def[simp]

definition varssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "varssst S ≡ ⋃(set (map varssstp S))"

abbreviation wfrestrictedvarssstp::"('a,'b) stateful_strand_step ⇒ 'b set" where
  "wfrestrictedvarssstp x ≡
    case x of
      NegChecks _ _ _ ⇒ {}
    | Equality Check _ _ ⇒ {}
    | InSet Check _ _ ⇒ {}
    | Delete _ _ ⇒ {}
    | _ ⇒ varssstp x"

definition wfrestrictedvarssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "wfrestrictedvarssst S ≡ ⋃(set (map wfrestrictedvarssstp S))"

abbreviation wfvarsoccssstp where
  "wfvarsoccssstp x ≡ 
    case x of
      Send ts ⇒ fvset (set ts)
    | Equality Assign s t ⇒ fv s
    | InSet Assign s t ⇒ fv s ∪ fv t
    | _ ⇒ {}"

definition wfvarsoccssst where
  "wfvarsoccssst S ≡ ⋃(set (map wfvarsoccssstp S))"

fun wf'sst::"'b set ⇒ ('a,'b) stateful_strand ⇒ bool" where
  "wf'sst V [] = True"
| "wf'sst V (Receive ts#S) = (fvset (set ts) ⊆ V ∧ wf'sst V S)"
| "wf'sst V (Send ts#S) = wf'sst (V ∪ fvset (set ts)) S"
| "wf'sst V (Equality Assign t t'#S) = (fv t' ⊆ V ∧ wf'sst (V ∪ fv t) S)"
| "wf'sst V (Equality Check _ _#S) = wf'sst V S"
| "wf'sst V (Insert t s#S) = (fv t ⊆ V ∧ fv s ⊆ V ∧ wf'sst V S)"
| "wf'sst V (Delete _ _#S) = wf'sst V S"
| "wf'sst V (InSet Assign t s#S) = wf'sst (V ∪ fv t ∪ fv s) S"
| "wf'sst V (InSet Check _ _#S) = wf'sst V S"
| "wf'sst V (NegChecks _ _ _#S) = wf'sst V S"

abbreviation "wfsst S ≡ wf'sst {} S ∧ fvsst S ∩ bvarssst S = {}"

fun subst_apply_stateful_strand_step::
  "('a,'b) stateful_strand_step ⇒ ('a,'b) subst ⇒ ('a,'b) stateful_strand_step"
  (infix "⋅sstp" 51) where
  "send⟨ts⟩ ⋅sstp θ = send⟨ts ⋅list θ⟩"
| "receive⟨ts⟩ ⋅sstp θ = receive⟨ts ⋅list θ⟩"
| "⟨a: t ≐ s⟩ ⋅sstp θ = ⟨a: (t ⋅ θ) ≐ (s ⋅ θ)⟩"
| "⟨a: t ∈ s⟩ ⋅sstp θ = ⟨a: (t ⋅ θ) ∈ (s ⋅ θ)⟩"
| "insert⟨t,s⟩ ⋅sstp θ = insert⟨t ⋅ θ, s ⋅ θ⟩"
| "delete⟨t,s⟩ ⋅sstp θ = delete⟨t ⋅ θ, s ⋅ θ⟩"
| "∀X⟨∨≠: F ∨∉: G⟩ ⋅sstp θ = ∀X⟨∨≠: (F ⋅pairs rm_vars (set X) θ) ∨∉: (G ⋅pairs rm_vars (set X) θ)⟩"

definition subst_apply_stateful_strand::
  "('a,'b) stateful_strand ⇒ ('a,'b) subst ⇒ ('a,'b) stateful_strand"
  (infix "⋅sst" 51) where
  "S ⋅sst θ ≡ map (λx. x ⋅sstp θ) S"

fun dbupdsst::"('f,'v) stateful_strand ⇒ ('f,'v) subst ⇒ ('f,'v) dbstate ⇒ ('f,'v) dbstate"
where
  "dbupdsst [] I D = D"
| "dbupdsst (Insert t s#A) I D = dbupdsst A I (insert ((t,s) ⋅p I) D)"
| "dbupdsst (Delete t s#A) I D = dbupdsst A I (D - {((t,s) ⋅p I)})"
| "dbupdsst (_#A) I D = dbupdsst A I D"

fun db'sst::"('f,'v) stateful_strand ⇒ ('f,'v) subst ⇒ ('f,'v) dbstatelist ⇒ ('f,'v) dbstatelist"
where
  "db'sst [] I D = D"
| "db'sst (Insert t s#A) I D = db'sst A I (List.insert ((t,s) ⋅p I) D)"
| "db'sst (Delete t s#A) I D = db'sst A I (List.removeAll ((t,s) ⋅p I) D)"
| "db'sst (_#A) I D = db'sst A I D"

definition dbsst where
  "dbsst S I ≡ db'sst S I []"

fun setopssstp where
  "setopssstp (Insert t s) = {(t,s)}"
| "setopssstp (Delete t s) = {(t,s)}"
| "setopssstp (InSet _ t s) = {(t,s)}"
| "setopssstp (NegChecks _ _ F') = set F'"
| "setopssstp _ = {}"

text ‹The set-operations of a stateful strand›
definition setopssst where
  "setopssst S ≡ ⋃(setopssstp ` set S)"

fun setops_listsstp where
  "setops_listsstp (Insert t s) = [(t,s)]"
| "setops_listsstp (Delete t s) = [(t,s)]"
| "setops_listsstp (InSet _ t s) = [(t,s)]"
| "setops_listsstp (NegChecks _ _ F') = F'"
| "setops_listsstp _ = []"

text ‹The set-operations of a stateful strand (list variant)›
definition setops_listsst where
  "setops_listsst S ≡ remdups (concat (map setops_listsstp S))"


subsection ‹Small Lemmata›
lemma is_Check_or_Assignment_iff[simp]:
  "is_Check x ∨ is_Assignment x ⟷ is_Check_or_Assignment x"
by (cases x) (blast intro: poscheckvariant.exhaust)+

lemma subst_apply_stateful_strand_step_Inequality[simp]:
  "⟨t != s⟩ ⋅sstp θ = ⟨t ⋅ θ != s ⋅ θ⟩"
  "∀x⟨t != s⟩ ⋅sstp θ = ∀x⟨t ⋅ rm_vars {x} θ != s ⋅ rm_vars {x} θ⟩"
  "∀x,y⟨t != s⟩ ⋅sstp θ = ∀x,y⟨t ⋅ rm_vars {x,y} θ != s ⋅ rm_vars {x,y} θ⟩"
  "∀x,y,z⟨t != s⟩ ⋅sstp θ = ∀x,y,z⟨t ⋅ rm_vars {x,y,z} θ != s ⋅ rm_vars {x,y,z} θ⟩"
by simp_all

lemma subst_apply_stateful_strand_step_NotInSet[simp]:
  "⟨t not in s⟩ ⋅sstp θ = ⟨t ⋅ θ not in s ⋅ θ⟩"
  "∀x⟨t not in s⟩ ⋅sstp θ = ∀x⟨t ⋅ rm_vars {x} θ not in s ⋅ rm_vars {x} θ⟩"
  "∀x,y⟨t not in s⟩ ⋅sstp θ = ∀x,y⟨t ⋅ rm_vars {x,y} θ not in s ⋅ rm_vars {x,y} θ⟩"
  "∀x,y,z⟨t not in s⟩ ⋅sstp θ = ∀x,y,z⟨t ⋅ rm_vars {x,y,z} θ not in s ⋅ rm_vars {x,y,z} θ⟩"
by simp_all

lemma trms_listsst_is_trmssst: "trmssst S = set (trms_listsst S)"
unfolding trmsst_def trms_listsst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma setops_listsst_is_setopssst: "setopssst S = set (setops_listsst S)"
unfolding setopssst_def setops_listsst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma fv_listsstp_is_fvsstp: "fvsstp a = set (fv_listsstp a)"
proof (cases a)
  case (NegChecks X F G) thus ?thesis
    using fvpairs_append[of F G] fv_listpairs_append[of F G]
          fv_listpairs_is_fvpairs[of "F@G"]
    by auto
qed (simp_all add: fv_listpairs_is_fvpairs fv_list_is_fv)

lemma fv_listsst_is_fvsst: "fvsst S = set (fv_listsst S)"
unfolding fvsst_def fv_listsst_def by (induct S) (simp_all add: fv_listsstp_is_fvsstp)

lemma trmssstp_finite[simp]: "finite (trmssstp x)"
by (cases x) auto

lemma trmssst_finite[simp]: "finite (trmssst S)"
using trmssstp_finite unfolding trmssst_def by (induct S) auto

lemma varssstp_finite[simp]: "finite (varssstp x)"
by (cases x) auto

lemma varssst_finite[simp]: "finite (varssst S)"
using varssstp_finite unfolding varssst_def by (induct S) auto

lemma fvsstp_finite[simp]: "finite (fvsstp x)"
by (cases x) auto

lemma fvsst_finite[simp]: "finite (fvsst S)"
using fvsstp_finite unfolding fvsst_def by (induct S) auto

lemma bvarssstp_finite[simp]: "finite (set (bvarssstp x))"
by (rule finite_set)

lemma bvarssst_finite[simp]: "finite (bvarssst S)"
using bvarssstp_finite unfolding bvarssst_def by (induct S) auto

lemma subst_sst_nil[simp]: "[] ⋅sst δ = []"
by (simp add: subst_apply_stateful_strand_def)

lemma dbsst_nil[simp]: "dbsst [] ℐ = []"
by (simp add: dbsst_def)

lemma iksst_nil[simp]: "iksst [] = {}"
by (simp add: iksst_def)

lemma in_iksst_iff: "t ∈ iksst A ⟷ (∃ts. receive⟨ts⟩ ∈ set A ∧ t ∈ set ts)"
unfolding iksst_def by blast

lemma iksst_append[simp]: "iksst (A@B) = iksst A ∪ iksst B"
by (auto simp add: iksst_def)

lemma iksst_concat: "iksst (concat xs) = ⋃(iksst ` set xs)"
by (induct xs) auto

lemma iksst_subst: "iksst (A ⋅sst δ) = iksst A ⋅set δ"
proof (induction A)
  case (Cons a A)
  have "iksst ([a] ⋅sst δ) = iksst [a] ⋅set δ"
  proof (cases a)
    case (Receive ts) thus ?thesis
      using in_iksst_iff[of _ "[a]"] in_iksst_iff[of _ "[a] ⋅sst δ"]
      unfolding subst_apply_stateful_strand_def by auto
  qed (simp_all add: iksst_def subst_apply_stateful_strand_def)
  thus ?case
    using Cons.IH iksst_append
    by (metis append_Cons append_Nil image_Un map_append subst_apply_stateful_strand_def) 
qed simp

lemma iksst_set_subset:
  "set A ⊆ set B ⟹ iksst A ⊆ iksst B"
unfolding iksst_def by blast

lemma iksst_prefix_subset:
  "prefix A B ⟹ iksst A ⊆ iksst B" (is "?P A B ⟹ ?P' A B")
  "prefix A (C@D) ⟹ ¬prefix A C ⟹ iksst C ⊆ iksst A" (is "?Q ⟹ ?Q' ⟹ ?Q''")
proof -
  show "?P A B ⟹ ?P' A B" for A B by (metis set_mono_prefix iksst_set_subset)
  thus "?Q ⟹ ?Q' ⟹ ?Q''" by (metis prefixI prefix_same_cases)
qed

lemma iksst_snoc_no_receive_empty:
  assumes "∀a ∈ set A. ¬is_Receive a"
  shows "iksst A ⋅set I = {}"
using assms in_iksst_iff[of _ A] by fastforce

lemma iksst_snoc_no_receive_eq:
  assumes "∄s. a = receive⟨s⟩"
  shows "iksst (A@[a]) ⋅set ℐ = iksst A ⋅set ℐ"
using assms iksst_snoc_no_receive_empty[of "[a]" ℐ] iksst_append[of A "[a]"]
unfolding is_Receive_def by auto

lemma dbsst_set_is_dbupdsst: "set (db'sst A I D) = dbupdsst A I (set D)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix t s show "(t,s) ∈ ?A ⟹ (t,s) ∈ ?B" by (induct rule: db'sst.induct) auto
  qed

  show "?B ⊆ ?A"
  proof
    fix t s show "(t,s) ∈ ?B ⟹ (t,s) ∈ ?A" by (induct arbitrary: D rule: dbupdsst.induct) auto
  qed
qed

lemma dbsst_no_upd:
  assumes "∀a ∈ set A. ¬is_Insert a ∧ ¬is_Delete a"
  shows "db'sst A I D = D"
using assms
proof (induction A)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbsst_no_upd_append:
  assumes "∀b ∈ set B. ¬is_Insert b ∧ ¬is_Delete b"
  shows "db'sst A = db'sst (A@B)"
  using assms
proof (induction A)
  case Nil thus ?case by (simp add: dbsst_no_upd)
next
  case (Cons a A) thus ?case by (cases a) simp_all
qed

lemma dbsst_append:
  "db'sst (A@B) I D = db'sst B I (db'sst A I D)"
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbsst_in_cases:
  assumes "(t,s) ∈ set (db'sst A I D)"
  shows "(t,s) ∈ set D ∨ (∃t' s'. insert⟨t',s'⟩ ∈ set A ∧ t = t' ⋅ I ∧ s = s' ⋅ I)"
  using assms
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) fastforce+
qed simp

lemma dbsst_in_cases':
  assumes "(t,s) ∈ set (db'sst A I D)"
    and "(t,s) ∉ set D"
  shows "∃B C t' s'. A = B@insert⟨t',s'⟩#C ∧ t = t' ⋅ I ∧ s = s' ⋅ I ∧
                     (∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I)"
  using assms(1)
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  note * = snoc dbsst_append[of A "[a]" I D]
  thus ?case
  proof (cases a)
    case (Insert t' s')
    thus ?thesis using * by (cases "(t,s) ∈ set (db'sst A I D)") force+
  next
    case (Delete t' s')
    hence **: "t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I" using * by simp

    have "(t,s) ∈ set (db'sst A I D)" using * Delete by force
    then obtain B C u v where B:
        "A = B@insert⟨u,v⟩#C" "t = u ⋅ I" "s = v ⋅ I"
        "∀t' s'. delete⟨t',s'⟩ ∈ set C ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
      using snoc.IH by moura

    have "A@[a] = B@insert⟨u,v⟩#(C@[a])"
         "∀t' s'. delete⟨t',s'⟩ ∈ set (C@[a]) ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
      using B(1,4) Delete ** by auto
    thus ?thesis using B(2,3) by blast
  qed force+
qed (simp add: assms(2))

lemma dbsst_filter:
  "db'sst A I D = db'sst (filter is_Update A) I D"
by (induct A I D rule: db'sst.induct) simp_all

lemma dbsst_subst_swap:
  assumes "∀x ∈ fvsst A. I x = J x"
  shows "db'sst A I D = db'sst A J D"
using assms
proof (induction A arbitrary: D)
  case (Cons a A)
  hence "∀x ∈ fvsstp a. I x = J x" "⋀D. db'sst A I D = db'sst A J D" by auto
  thus ?case by (cases a) (simp_all add: term_subst_eq[of _ I J])
qed simp

lemma dbupdsst_no_upd:
  assumes "∀a ∈ set A. ¬is_Insert a ∧ ¬is_Delete a"
  shows "dbupdsst A I D = D"
using assms
proof (induction A)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbupdsst_no_deletes:
  assumes "list_all (λa. ¬is_Delete a) A"
  shows "dbupdsst A I D = D ∪ {(t ⋅ I, s ⋅ I) | t s. insert⟨t,s⟩ ∈ set A}" (is "?Q A D")
using assms
proof (induction A arbitrary: D)
  case (Cons a A)
  hence IH: "?Q A D" for D by auto
  have "¬is_Delete a" using Cons.prems by simp
  thus ?case using IH by (cases a) auto
qed simp

lemma dbupdsst_append:
  "dbupdsst (A@B) I D = dbupdsst B I (dbupdsst A I D)"
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbupdsst_filter:
  "dbupdsst A I D = dbupdsst (filter is_Update A) I D"
by (induct A I D rule: dbupdsst.induct) simp_all

lemma dbupdsst_in_cases:
  assumes "(t,s) ∈ dbupdsst A I D"
  shows "(t,s) ∈ D ∨ (∃t' s'. insert⟨t',s'⟩ ∈ set A ∧ t = t' ⋅ I ∧ s = s' ⋅ I)" (is ?P)
    and "∀u v B. suffix (delete⟨u,v⟩#B) A ∧ (t,s) = (u,v) ⋅p I ⟶
                  (∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B)" (is ?Q)
proof -
  show ?P using assms
  proof (induction A arbitrary: D)
    case (Cons a A) thus ?case by (cases a) fastforce+
  qed simp

  show ?Q using assms
  proof (induction A arbitrary: D rule: List.rev_induct)
    case (snoc a A)
    note 0 = snoc.IH snoc.prems
    note 1 = suffix_snoc[of _ A a]

    have 2: "dbupdsst (A@[a]) I D = dbupdsst A I D" when "¬is_Update a"
      using that dbupdsst_append[of A "[a]" I D] by (cases a) auto

    have 3: "suffix (delete⟨u,v⟩#B) A ⟹ suffix (delete⟨u,v⟩#B@[a]) (A@[a])"
      when "¬is_Update a" for u v B
      using that by simp

    have 4: "∃C. B = C@[a] ∧ suffix (delete⟨u,v⟩#C) A"
      when a: "¬is_Delete a" "suffix (delete⟨u,v⟩#B) (A@[a])" for u v B
    proof -
      have a': "a ≠ delete⟨u,v⟩" using a(1) by force
      obtain C where C: "delete⟨u,v⟩#B = C@[a]" "suffix C A" using 1 a(2) by blast
      show ?thesis using a' C by (cases C) auto
    qed

    note 5 = dbupdsst_append[of A "[a]" I]

    show ?case
    proof (cases "is_Update a")
      case True
      then obtain u v where "a = insert⟨u,v⟩ ∨ a = delete⟨u,v⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨u,v⟩"
        hence a': "¬is_Delete a" by simp

        have 6: "insert⟨u,v⟩ ∈ set B"
          when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for u' v' B
          using 4[OF a' B] unfolding a by fastforce

        have 7: "(t,s) = (u,v) ⋅p I ∨ (t,s) ∈ dbupdsst A I D" using snoc.prems 5 a by auto
        show ?thesis
        proof (cases "(t,s) = (u,v) ⋅p I")
          case True
          have "insert⟨u,v⟩ ∈ set B"
            when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for u' v' B
            using 4[OF a' B] unfolding a by fastforce
          thus ?thesis using True by blast
        next
          case False
          hence 8: "(t,s) ∈ dbupdsst A I D" using 7 by blast
          have "∃u'' v''. (t,s) = (u'',v'') ⋅p I ∧ insert⟨u'',v''⟩ ∈ set B"
            when B: "suffix (delete⟨u',v'⟩#B) (A @ [a])" "(t,s) = (u',v') ⋅p I" for u' v' B
          proof -
            obtain C where C: "B = C@[a]" "suffix (delete⟨u',v'⟩#C) A" using 4[OF a' B(1)] by blast
            thus ?thesis using snoc.IH[OF 8] B(2) unfolding a by fastforce
          qed
          thus ?thesis by blast
        qed
      next
        assume a: "a = delete⟨u,v⟩"
        hence "(t,s) ∈ dbupdsst A I D - {((u,v) ⋅p I)}" using snoc.prems 5 by auto
        hence 6: "(t,s) ∈ dbupdsst A I D" "(t,s) ≠ (u,v) ⋅p I" by (blast,blast)
        
        have "(∃C. B = C@[a] ∧ suffix (delete⟨u',v'⟩#C) A) ∨ (B = [] ∧ u' = u ∧ v' = v)"
          when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for B u' v'
        proof -
          obtain C where C: "delete⟨u',v'⟩#B = C@[a]" "suffix C A" using B 1 by blast
          show ?thesis
          proof (cases "B = []")
            case True thus ?thesis using C unfolding a by simp
          next
            case False
            then obtain b B' where B': "B = B'@[b]" by (meson rev_exhaust)
            show ?thesis using C unfolding a B' by auto
          qed 
        qed
        hence "∃C. B = C@[a] ∧ suffix (delete⟨u',v'⟩#C) A"
          when "suffix (delete⟨u',v'⟩#B) (A@[a])" "(t,s) = (u',v') ⋅p I" for B u' v'
          using that 6 by blast
        thus ?thesis using snoc.IH[OF 6(1)] unfolding a by fastforce
      qed
    next
      case False
      have "∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B"
        when B: "suffix (delete⟨u,v⟩#B) (A@[a])" "(t,s) = (u,v) ⋅p I" for u v B
      proof -
        obtain C where C: "B = C@[a]" "suffix (delete⟨u,v⟩#C) A" using 4[OF _ B(1)] False by blast
        show ?thesis using B(2) snoc.IH[OF snoc.prems[unfolded 2[OF False]]] C by fastforce
      qed
      thus ?thesis by blast
    qed
  qed simp
qed

lemma dbupdsst_in_iff:
  "(t,s) ∈ dbupdsst A I D ⟷
   ((∀u v B. suffix (delete⟨u,v⟩#B) A ∧ (t,s) = (u,v) ⋅p I ⟶
              (∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B)) ∧
    ((t,s) ∈ D ∨ (∃u v. (t,s) = (u,v) ⋅p I ∧ insert⟨u,v⟩ ∈ set A)))"
  (is "?P A D ⟷ ?Q1 A ∧ ?Q2 A D")
proof
  show "?P A D ⟹ ?Q1 A ∧ ?Q2 A D" using dbupdsst_in_cases by fast

  show "?Q1 A ∧ ?Q2 A D ⟹ ?P A D"
  proof (induction A arbitrary: D)
    case (Cons a A)
    have Q1: "?Q1 A" using Cons.prems suffix_Cons[of _ a A] by blast

    show ?case
    proof (cases "is_Update a")
      case False thus ?thesis using Q1 Cons.IH Cons.prems by (cases a) auto
    next
      case True
      then obtain t' s' where "a = insert⟨t',s'⟩ ∨ a = delete⟨t',s'⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨t',s'⟩"
        hence "?Q2 A (insert ((t',s') ⋅p I) D)" using Cons.prems by auto
        thus ?thesis using Q1 Cons.IH unfolding a by auto
      next
        assume a: "a = delete⟨t',s'⟩"
        hence "?Q2 A (D - {(t',s') ⋅p I})" using Cons.prems by auto
        thus ?thesis using Q1 Cons.IH unfolding a by auto
      qed
    qed
  qed simp
qed

lemma dbupdsst_in_cases':
  fixes A::"('a,'b) stateful_strand"
  assumes "(t,s) ∈ dbupdsst A I D"
    and "(t,s) ∉ D"
  shows "∃B C t' s'. A = B@insert⟨t',s'⟩#C ∧ t = t' ⋅ I ∧ s = s' ⋅ I ∧
                     (∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I)"
using assms(1)
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  note 0 = dbupdsst_append[of A "[a]" I D]
  have 1: "(t,s) ∈ dbupdsst A I D" when "¬is_Update a" using that snoc.prems 0 by (cases a) auto
  show ?case
  proof (cases "is_Update a")
    case False
    obtain B C t' s' where B:
        "A = B@insert⟨t',s'⟩#C" "t = t' ⋅ I" "s = s' ⋅ I"
        "∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I"
      using snoc.IH[OF 1[OF False]] by blast

    have "A@[a] = B@insert⟨t',s'⟩#(C@[a])"
         "∀t'' s''. delete⟨t'',s''⟩ ∈ set (C@[a]) ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I"
      using False B(1,4) by auto
    thus ?thesis using B(2,3) by blast
  next
    case True
    then obtain t' s' where "a = insert⟨t',s'⟩ ∨ a = delete⟨t',s'⟩" by (cases a) auto
    thus ?thesis
    proof
      assume a: "a = insert⟨t',s'⟩"
      hence "dbupdsst (A@[a]) I D = insert ((t',s') ⋅p I) (dbupdsst A I D)" using 0 by simp
      hence "(t,s) = (t',s') ⋅p I ∨ (t,s) ∈ dbupdsst A I D" using snoc.prems by blast
      thus ?thesis
      proof
        assume 2: "(t,s) ∈ dbupdsst A I D" show ?thesis using snoc.IH[OF 2] unfolding a by force
      qed (force simp add: a)
    next
      assume a: "a = delete⟨t',s'⟩"
      hence 2: "t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I" using 0 snoc.prems by simp
  
      have "(t,s) ∈ dbupdsst A I D" using 0 snoc.prems a by force
      then obtain B C u v where B:
          "A = B@insert⟨u,v⟩#C" "t = u ⋅ I" "s = v ⋅ I"
          "∀t' s'. delete⟨t',s'⟩ ∈ set C ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
        using snoc.IH by moura
  
      have "A@[a] = B@insert⟨u,v⟩#(C@[a])"
           "∀t' s'. delete⟨t',s'⟩ ∈ set (C@[a]) ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
        using B(1,4) a 2 by auto
      thus ?thesis using B(2,3) by blast
    qed
  qed
qed (simp add: assms(2))

lemma dbupdsst_mono:
  assumes "D ⊆ E"
  shows "dbupdsst A I D ⊆ dbupdsst A I E"
using assms
proof (induction A arbitrary: D E)
  case (Cons a A) thus ?case
  proof (cases a)
    case (Insert t s)
    have "insert ((t,s) ⋅p I) D ⊆ insert ((t,s) ⋅p I) E" using Cons.prems by fast
    thus ?thesis using Cons.IH unfolding Insert by simp
  next
    case (Delete t s)
    have "D - {(t,s) ⋅p I} ⊆ E - {(t,s) ⋅p I}" using Cons.prems by fast
    thus ?thesis using Cons.IH unfolding Delete by simp
  qed auto
qed simp

lemma dbupdsst_db_narrow:
  assumes "(t,s) ∈ dbupdsst A I (D ∪ E)"
    and "(t,s) ∉ D"
  shows "(t,s) ∈ dbupdsst A I E"
using assms
proof (induction A arbitrary: D E)
  case (Cons a A) thus ?case
  proof (cases a)
    case (Delete t' s') thus ?thesis
      using Cons.prems Cons.IH[of "D - {(t',s') ⋅p I}" "E - {(t',s') ⋅p I}"] by (simp add: Un_Diff)
  qed auto
qed simp

lemma dbupdsst_set_term_neq_in_iff:
  assumes f: "f ≠ k"
    and A: "∀t s. insert⟨t,s⟩ ∈ set A ⟶ (∃g ts. s = Fun g ts)"
  shows "(t,Fun f ts) ∈ dbupdsst A I D ⟷
         (t,Fun f ts) ∈ dbupdsst (filter (λa. ∄s ss. a = insert⟨s,Fun k ss⟩) A) I D"
    (is "?P A D ⟷ ?P (?f A) D")
proof
  show "?P A D ⟹ ?P (?f A) D" using A
  proof (induction A arbitrary: D)
    case (Cons a A)
    have IH: "?P A D ⟹ ?P (?f A) D" for D
      using Cons.prems(2) Cons.IH by simp

    show ?case
    proof (cases "is_Update a")
      case True
      then obtain u s where "a = insert⟨u,s⟩ ∨ a = delete⟨u,s⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨u,s⟩"
        obtain g ss where s: "s = Fun g ss" using a Cons.prems(2) by fastforce

        have 0: "?P A (insert ((u, s) ⋅p I) D)" using a Cons.prems(1) by fastforce
        show ?thesis
        proof (cases "g = k")
          case g: True
          have "?f (a#A) = ?f A" unfolding a s g by force
          moreover have "(t,Fun f ts) ≠ (u, Fun g ss) ⋅p I" using f unfolding g by auto
          ultimately show ?thesis
            using IH[OF 0] dbupdsst_db_narrow[of t "Fun f ts" "?f A" I "{(u, s) ⋅p I}" D]
            unfolding a s g by force
        next
          case g: False
          have "?f (a#A) = a#?f A" using g unfolding a s by force
          thus ?thesis using Cons.prems Cons.IH g unfolding a s by force
        qed
      next
        assume a: "a = delete⟨u,s⟩"
        hence "?f (a#A) = a#?f A" by auto
        thus ?thesis using Cons.prems Cons.IH unfolding a by fastforce
      qed
    next
      case a: False
      hence "?P A D" using Cons.prems(1) by (cases a) auto
      hence "?P (?f A) D" using Cons.IH Cons.prems(2) a by fastforce
      thus ?thesis using a by (cases a) auto
    qed
  qed simp

  have "dbupdsst (?f A) I D ⊆ dbupdsst A I D"
  proof (induction A arbitrary: D)
    case (Cons a A) show ?case
    proof (cases a)
      case (Insert t s)
      have "?f (a#A) = a#?f A ∨ ?f (a#A) = ?f A" unfolding Insert by force
      hence "dbupdsst (?f (a#A)) I D ⊆ dbupdsst (?f A) I (insert ((t,s) ⋅p I) D)"
        using dbupdsst_mono[of D "insert ((t, s) ⋅p I) D"] unfolding Insert by auto
      thus ?thesis using Cons.IH unfolding Insert by fastforce
    qed (use Cons.prems Cons.IH in auto)
  qed simp
  thus "?P (?f A) D ⟹ ?P A D" by blast
qed

lemma dbupdsst_subst_const_swap:
  fixes t s
  defines "fvs ≡ λA D. fvsst A ∪ fv t ∪ fv s ∪ ⋃(fvpair ` D)"
  assumes "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ)" (is "?in δ A D")
    and "∀x ∈ fvs A D.
          δ x = θ x ∨
          (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ s) ∧ ¬(θ x ⊑ t) ∧ ¬(θ x ⊑ s) ∧
           (∀(u,v) ∈ D. ¬(δ x ⊑ u) ∧ ¬(δ x ⊑ v) ∧ ¬(θ x ⊑ u) ∧ ¬(θ x ⊑ v)) ∧
           (∀u v. insert⟨u,v⟩ ∈ set A ∨ delete⟨u,v⟩ ∈ set A ⟶
                    ¬(δ x ⊑ u) ∧ ¬(δ x ⊑ v) ∧ ¬(θ x ⊑ u) ∧ ¬(θ x ⊑ v)))"
      (is "?A δ θ D")
    and "∀x ∈ fvs A D. ∃c. δ x = Fun c []" (is "?B δ")
    and "∀x ∈ fvs A D. ∃c. θ x = Fun c []" (is "?B θ")
    and "∀x ∈ fvs A D. ∀y ∈ fvs A D. δ x = δ y ⟷ θ x = θ y" (is "?C δ θ A D")
  shows "(t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)" (is "?in θ A D")
using assms(2-)
proof (induction A arbitrary: D rule: List.rev_induct)
  case Nil
  then obtain u v where u: "(u,v) ∈ D" "t ⋅ δ = u ⋅ δ" "s ⋅ δ = v ⋅ δ" by auto

  let ?X = "fv t ∪ fv u"
  let ?Y = "fv s ∪ fv v"

  have 0: "fv u ⊆ fvs [] D" "fv v ⊆ fvs [] D" "fv t ⊆ fvs [] D" "fv s ⊆ fvs [] D"
    using u(1) unfolding fvs_def by (blast, blast, blast, blast)

  have 1: "∀x ∈ ?X. δ x = θ x ∨ (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ u))"
          "∀x ∈ ?Y. δ x = θ x ∨ (¬(δ x ⊑ s) ∧ ¬(δ x ⊑ v))"
    using Nil.prems(2) u(1) unfolding fvs_def by (blast,blast)

  have 2: "∀x ∈ ?X. ∃c. δ x = Fun c []" "∀x ∈ ?X. ∃c. θ x = Fun c []"
          "∀x ∈ ?Y. ∃c. δ x = Fun c []" "∀x ∈ ?Y. ∃c. θ x = Fun c []"
    using Nil.prems(3,4) 0 by (blast,blast,blast,blast)

  have 3: "∀x ∈ ?X. ∀y ∈ ?X. δ x = δ y ⟷ θ x = θ y"
          "∀x ∈ ?Y. ∀y ∈ ?Y. δ x = δ y ⟷ θ x = θ y"
    using Nil.prems(5) 0 by (blast,blast)

  have "t ⋅ θ = u ⋅ θ" "s ⋅ θ = v ⋅ θ"
    using subst_const_swap_eq'[OF u(2) 1(1) 2(1,2) 3(1)]
          subst_const_swap_eq'[OF u(3) 1(2) 2(3,4) 3(2)]
    by argo+
  thus ?case using u(1) by force
next
  case (snoc a A)
  have 0: "fvs A D ⊆ fvs (A@[a]) D" "set A ⊆ set (A@[a])" unfolding fvs_def by auto

  note 1 = dbupdsst_append[of A "[a]"]

  have IH: "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ) ⟹ (t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)"
    using snoc.IH[of D] snoc.prems(2-) 0 by blast

  let ?q0 = "λt s δ θ. ∀x ∈ fv t ∪ fv s. δ x = θ x ∨ (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ s))"
  let ?q1 = "λt s δ.   ∀x ∈ fv t ∪ fv s. ∃c. δ x = Fun c []"
  let ?q2 = "λt s δ θ. ∀x ∈ fv t ∪ fv s. ∀y ∈ fv t ∪ fv s. δ x = δ y ⟷ θ x = θ y"

  show ?case
  proof (cases "is_Update a")
    case False
    hence "dbupdsst (A@[a]) δ (D ⋅pset δ) = dbupdsst A δ (D ⋅pset δ)"
          "dbupdsst (A@[a]) θ (D ⋅pset θ) = dbupdsst A θ (D ⋅pset θ)"
      using 1 by (cases a; auto)+
    thus ?thesis using IH snoc.prems(1) by blast
  next
    case True
    then obtain u v where u: "a = insert⟨u,v⟩ ∨ a = delete⟨u,v⟩" by (cases a) auto

    have uv_in: "insert⟨u,v⟩ ∈ set (A@[a]) ∨ delete⟨u,v⟩ ∈ set (A@[a])" using u by force
    hence fv_uv: "fv u ⊆ fvs (A@[a]) D" "fv v ⊆ fvs (A@[a]) D" unfolding fvs_def by (force,force)

    have fv_ts: "fv t ⊆ fvs (A@[a]) D" "fv s ⊆ fvs (A@[a]) D" unfolding fvs_def by (blast,blast)

    have q0: "?q0 t u δ θ" "?q0 s v δ θ"
             "?q0 t u θ δ" "?q0 s v θ δ"
    proof -
      show "?q0 t u δ θ" "?q0 s v δ θ"
        using snoc.prems(2) 0 fv_ts fv_uv uv_in by (blast,blast)

      show "?q0 t u θ δ"
      proof
        fix x assume "x ∈ fv t ∪ fv u"
        hence "x ∈ fvs (A@[a]) D" using fv_ts(1) fv_uv(1) by blast
        thus "θ x = δ x ∨ (¬(θ x ⊑ t) ∧ ¬(θ x ⊑ u))" 
          using snoc.prems(2) uv_in by auto
      qed

      show "?q0 s v θ δ"
      proof
        fix x assume "x ∈ fv s ∪ fv v"
        hence "x ∈ fvs (A@[a]) D" using fv_ts(2) fv_uv(2) by blast
        thus "θ x = δ x ∨ (¬(θ x ⊑ s) ∧ ¬(θ x ⊑ v))" 
          using snoc.prems(2) uv_in by auto
      qed
    qed

    have q1: "?q1 t u δ" "?q1 t u θ"
             "?q1 s v δ" "?q1 s v θ"
      using snoc.prems(3,4) 0 fv_ts fv_uv by (blast,blast,blast,blast)

    have q2: "?q2 t u δ θ" "?q2 s v δ θ"
             "?q2 t u θ δ" "?q2 s v θ δ"
      using snoc.prems(5) 0 fv_ts fv_uv by (blast,blast,blast,blast)

    from u show ?thesis
    proof
      assume a: "a = insert⟨u,v⟩"
      show ?thesis
      proof (cases "(t ⋅ δ, s ⋅ δ) = (u,v) ⋅p δ")
        case True
        hence "(t ⋅ θ, s ⋅ θ) = (u,v) ⋅p θ"
          using subst_const_swap_eq'[OF _ q0(1) q1(1,2) q2(1)]
                subst_const_swap_eq'[OF _ q0(2) q1(3,4) q2(2)]
          by fast
        thus ?thesis using 1 unfolding a by simp
      next
        case False
        hence "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ)"
          using snoc.prems(1) 1 unfolding a by force
        hence "(t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)"
          using IH by blast
        thus ?thesis using 1 unfolding a by simp
      qed
    next
      assume a: "a = delete⟨u,v⟩"
      have "(t ⋅ δ, s ⋅ δ) ≠ (u,v) ⋅p δ"
        using snoc.prems(1) dbupdsst_append[of A "[a]"] unfolding a by fastforce
      hence 2: "(t ⋅ θ, s ⋅ θ) ≠ (u,v) ⋅p θ"
        using subst_const_swap_eq'[OF _ q0(3) q1(2,1) q2(3)]
              subst_const_swap_eq'[OF _ q0(4) q1(4,3) q2(4)]
        by fast

      have "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ)"
        using snoc.prems(1) 1 unfolding a by fastforce
      hence 3: "(t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)"
        using IH by blast

      show ?thesis using 2 3 dbupdsst_append[of A "[a]"] unfolding a by auto
    qed
  qed
qed

lemma subst_sst_cons: "a#A ⋅sst δ = (a ⋅sstp δ)#(A ⋅sst δ)"
by (simp add: subst_apply_stateful_strand_def)

lemma subst_sst_snoc: "A@[a] ⋅sst δ = (A ⋅sst δ)@[a ⋅sstp δ]"
by (simp add: subst_apply_stateful_strand_def)

lemma subst_sst_append[simp]: "A@B ⋅sst δ = (A ⋅sst δ)@(B ⋅sst δ)"
by (simp add: subst_apply_stateful_strand_def)

lemma subst_sst_list_all:
  "list_all is_Send S ⟷ list_all is_Send (S ⋅sst δ)"
  "list_all is_Receive S ⟷ list_all is_Receive (S ⋅sst δ)"
  "list_all is_Equality S ⟷ list_all is_Equality (S ⋅sst δ)"
  "list_all is_Insert S ⟷ list_all is_Insert (S ⋅sst δ)"
  "list_all is_Delete S ⟷ list_all is_Delete (S ⋅sst δ)"
  "list_all is_InSet S ⟷ list_all is_InSet (S ⋅sst δ)"
  "list_all is_NegChecks S ⟷ list_all is_NegChecks (S ⋅sst δ)"
  "list_all is_Assignment S ⟷ list_all is_Assignment (S ⋅sst δ)"
  "list_all is_Check S ⟷ list_all is_Check (S ⋅sst δ)"
  "list_all is_Update S ⟷ list_all is_Update (S ⋅sst δ)"
  "list_all is_Check_or_Assignment S ⟷ list_all is_Check_or_Assignment (S ⋅sst δ)"
proof (induction S)
  case (Cons x S)
  note * = list_all_def subst_apply_stateful_strand_def
  { case 1 thus ?case using Cons.IH(1) unfolding * by (cases x) auto }
  { case 2 thus ?case using Cons.IH(2) unfolding * by (cases x) auto }
  { case 3 thus ?case using Cons.IH(3) unfolding * by (cases x) auto }
  { case 4 thus ?case using Cons.IH(4) unfolding * by (cases x) auto }
  { case 5 thus ?case using Cons.IH(5) unfolding * by (cases x) auto }
  { case 6 thus ?case using Cons.IH(6) unfolding * by (cases x) auto }
  { case 7 thus ?case using Cons.IH(7) unfolding * by (cases x) auto }
  { case 8 thus ?case using Cons.IH(8) unfolding * by (cases x) fastforce+ }
  { case 9 thus ?case using Cons.IH(9) unfolding * by (cases x) auto }
  { case 10 thus ?case using Cons.IH(10) unfolding * by (cases x) auto }
  { case 11 thus ?case using Cons.IH(11) unfolding * by (cases x) auto }
qed simp_all

lemma subst_sstp_id_subst: "a ⋅sstp Var = a"
by (cases a) auto

lemma subst_sst_id_subst: "A ⋅sst Var = A"
by (induct A) (simp, metis subst_sstp_id_subst subst_sst_cons)

lemma sst_vars_append_subset:
  "fvsst A ⊆ fvsst (A@B)" "bvarssst A ⊆ bvarssst (A@B)"
  "fvsst B ⊆ fvsst (A@B)" "bvarssst B ⊆ bvarssst (A@B)"
by auto

lemma sst_vars_disj_cons[simp]: "fvsst (a#A) ∩ bvarssst (a#A) = {} ⟹ fvsst A ∩ bvarssst A = {}"
unfolding fvsst_def bvarssst_def by auto

lemma fvsst_cons_subset[simp]: "fvsst A ⊆ fvsst (a#A)"
by auto

lemma fvsstp_subst_cases[simp]:
  "fvsstp (send⟨ts⟩ ⋅sstp θ) = fvset (set ts ⋅set θ)"
  "fvsstp (receive⟨ts⟩ ⋅sstp θ) = fvset (set ts ⋅set θ)"
  "fvsstp (⟨c: t ≐ s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "fvsstp (insert⟨t,s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "fvsstp (delete⟨t,s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "fvsstp (⟨c: t ∈ s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "fvsstp (∀X⟨∨≠: F ∨∉: G⟩ ⋅sstp θ) =
    fvpairs (F ⋅pairs rm_vars (set X) θ) ∪ fvpairs (G ⋅pairs rm_vars (set X) θ) - set X"
by simp_all

lemma varssstp_cases[simp]:
  "varssstp (send⟨ts⟩) = fvset (set ts)"
  "varssstp (receive⟨ts⟩) = fvset (set ts)"
  "varssstp (⟨c: t ≐ s⟩) = fv t ∪ fv s"
  "varssstp (insert⟨t,s⟩) = fv t ∪ fv s"
  "varssstp (delete⟨t,s⟩) = fv t ∪ fv s"
  "varssstp (⟨c: t ∈ s⟩) = fv t ∪ fv s"
  "varssstp (∀X⟨∨≠: F ∨∉: G⟩) = fvpairs F ∪ fvpairs G ∪ set X" (is ?A)
  "varssstp (∀X⟨∨≠: [(t,s)] ∨∉: []⟩) = fv t ∪ fv s ∪ set X" (is ?B)
  "varssstp (∀X⟨∨≠: [] ∨∉: [(t,s)]⟩) = fv t ∪ fv s ∪ set X" (is ?C)
proof
  show ?A ?B ?C by auto
qed simp_all

lemma varssstp_subst_cases[simp]:
  "varssstp (send⟨ts⟩ ⋅sstp θ) = fvset (set ts ⋅set θ)"
  "varssstp (receive⟨ts⟩ ⋅sstp θ) = fvset (set ts ⋅set θ)"
  "varssstp (⟨c: t ≐ s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "varssstp (insert⟨t,s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "varssstp (delete⟨t,s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "varssstp (⟨c: t ∈ s⟩ ⋅sstp θ) = fv (t ⋅ θ) ∪ fv (s ⋅ θ)"
  "varssstp (∀X⟨∨≠: F ∨∉: G⟩ ⋅sstp θ) =
    fvpairs (F ⋅pairs rm_vars (set X) θ) ∪ fvpairs (G ⋅pairs rm_vars (set X) θ) ∪ set X" (is ?A)
  "varssstp (∀X⟨∨≠: [(t,s)] ∨∉: []⟩ ⋅sstp θ) =
    fv (t ⋅ rm_vars (set X) θ) ∪ fv (s ⋅ rm_vars (set X) θ) ∪ set X" (is ?B)
  "varssstp (∀X⟨∨≠: [] ∨∉: [(t,s)]⟩ ⋅sstp θ) =
    fv (t ⋅ rm_vars (set X) θ) ∪ fv (s ⋅ rm_vars (set X) θ) ∪ set X" (is ?C)
proof
  show ?A ?B ?C by auto
qed simp_all

lemma bvarssst_cons_subset: "bvarssst A ⊆ bvarssst (a#A)"
by auto

lemma bvarssstp_subst: "bvarssstp (a ⋅sstp δ) = bvarssstp a"
by (cases a) auto

lemma bvarssst_subst: "bvarssst (A ⋅sst δ) = bvarssst A"
using bvarssstp_subst[of _ δ]
by (induct A) (simp_all add: subst_apply_stateful_strand_def)

lemma bvarssstp_set_cases[simp]:
  "set (bvarssstp (send⟨ts⟩)) = {}"
  "set (bvarssstp (receive⟨ts⟩)) = {}"
  "set (bvarssstp (⟨c: t ≐ s⟩)) = {}"
  "set (bvarssstp (insert⟨t,s⟩)) = {}"
  "set (bvarssstp (delete⟨t,s⟩)) = {}"
  "set (bvarssstp (⟨c: t ∈ s⟩)) = {}"
  "set (bvarssstp (∀X⟨∨≠: F ∨∉: G⟩)) = set X"
by simp_all

lemma bvarssstp_NegChecks: "¬is_NegChecks a ⟹ bvarssstp a = []"
by (cases a) simp_all

lemma bvarssst_NegChecks: "bvarssst A = bvarssst (filter is_NegChecks A)" 
proof (induction A)
  case (Cons a A) thus ?case by (cases a) fastforce+
qed simp

lemma varssst_append[simp]: "varssst (A@B) = varssst A ∪ varssst B"
by (simp add: varssst_def)

lemma varssst_Nil[simp]: "varssst [] = {}"
by (simp add: varssst_def)

lemma varssst_Cons: "varssst (a#A) = varssstp a ∪ varssst A"
by (simp add: varssst_def)

lemma fvsst_Cons: "fvsst (a#A) = fvsstp a ∪ fvsst A"
unfolding fvsst_def by simp

lemma bvarssst_Cons: "bvarssst (a#A) = set (bvarssstp a) ∪ bvarssst A"
unfolding bvarssst_def by auto

lemma varssst_Cons'[simp]:
  "varssst (send⟨ts⟩#A) = varssstp (send⟨ts⟩) ∪ varssst A"
  "varssst (receive⟨ts⟩#A) = varssstp (receive⟨ts⟩) ∪ varssst A"
  "varssst (⟨a: t ≐ s⟩#A) = varssstp (⟨a: t ≐ s⟩) ∪ varssst A"
  "varssst (insert⟨t,s⟩#A) = varssstp (insert⟨t,s⟩) ∪ varssst A"
  "varssst (delete⟨t,s⟩#A) = varssstp (delete⟨t,s⟩) ∪ varssst A"
  "varssst (⟨a: t ∈ s⟩#A) = varssstp (⟨a: t ∈ s⟩) ∪ varssst A"
  "varssst (∀X⟨∨≠: F ∨∉: G⟩#A) = varssstp (∀X⟨∨≠: F ∨∉: G⟩) ∪ varssst A"
by (simp_all add: varssst_def)

lemma fvsstp_subst_if_no_bvars:
  assumes a: "bvarssstp a = []"
  shows "fvsstp (a ⋅sstp θ) = fvset (θ ` fvsstp a)"
proof (cases a)
  case (NegChecks X F G)
  hence "set X = {}" using a by fastforce
  thus ?thesis using fvpairs_subst[of _ θ] unfolding NegChecks by simp
qed (auto simp add: subst_list_set_fv subst_apply_fv_unfold)

lemma fvsst_subst_if_no_bvars:
  assumes A: "bvarssst A = {}"
  shows "fvsst (A ⋅sst θ) = fvset (θ ` fvsst A)"
using assms
proof (induction A)
  case (Cons a A) thus ?case
    using fvsstp_subst_if_no_bvars[of a θ] fvsst_Cons[of a A] bvarssst_Cons[of a A]
          subst_sst_cons[of a A θ]
    by simp
qed simp

lemma varssstp_is_fvsstp_bvarssstp:
  fixes x::"('a,'b) stateful_strand_step"
  shows "varssstp x = fvsstp x ∪ set (bvarssstp x)"
proof (cases x)
  case (NegChecks X F G) thus ?thesis by (induct F) force+
qed simp_all

lemma varssst_is_fvsst_bvarssst:
  fixes S::"('a,'b) stateful_strand"
  shows "varssst S = fvsst S ∪ bvarssst S"
proof (induction S)
  case (Cons x S) thus ?case
    using varssstp_is_fvsstp_bvarssstp[of x]
    by (auto simp add: varssst_def)
qed simp

lemma varssstp_NegCheck[simp]:
  "varssstp (∀X⟨∨≠: F ∨∉: G⟩) = set X ∪ fvpairs F ∪ fvpairs G"
by (simp_all add: sup_commute sup_left_commute varssstp_is_fvsstp_bvarssstp)

lemma bvarssstp_NegCheck[simp]:
  "bvarssstp (∀X⟨∨≠: F ∨∉: G⟩) = X"
  "set (bvarssstp (∀[]⟨∨≠: F ∨∉: G⟩)) = {}"
by simp_all

lemma fvsstp_NegCheck[simp]:
  "fvsstp (∀X⟨∨≠: F ∨∉: G⟩) = fvpairs F ∪ fvpairs G - set X"
  "fvsstp (∀[]⟨∨≠: F ∨∉: G⟩) = fvpairs F ∪ fvpairs G"
  "fvsstp (⟨t != s⟩) = fv t ∪ fv s"
  "fvsstp (⟨t not in s⟩) = fv t ∪ fv s"
by simp_all

lemma fvsst_append[simp]: "fvsst (A@B) = fvsst A ∪ fvsst B"
by simp

lemma bvarssst_append[simp]: "bvarssst (A@B) = bvarssst A ∪ bvarssst B"
by auto

lemma fvsst_mono: "set A ⊆ set B ⟹ fvsst A ⊆ fvsst B"
by auto

lemma fvsstp_is_subterm_trmssstp:
  assumes "x ∈ fvsstp a"
  shows "Var x ∈ subtermsset (trmssstp a)"
using assms var_is_subterm
proof (cases a)
  case (NegChecks X F F')
  hence "x ∈ fvpairs F ∪ fvpairs F' - set X" using assms by simp
  thus ?thesis using NegChecks var_is_subterm by fastforce
qed force+

lemma fvsst_is_subterm_trmssst: "x ∈ fvsst A ⟹ Var x ∈ subtermsset (trmssst A)"
proof (induction A)
  case (Cons a A) thus ?case using fvsstp_is_subterm_trmssstp by (cases "x ∈ fvsst A") auto
qed simp

lemma var_subterm_trmssstp_is_varssstp:
  assumes "Var x ∈ subtermsset (trmssstp a)"
  shows "x ∈ varssstp a"
using assms vars_iff_subtermeq
proof (cases a)
  case (NegChecks X F F')
  hence "Var x ∈ subtermsset (trmspairs F ∪ trmspairs F')" using assms by simp
  thus ?thesis using NegChecks vars_iff_subtermeq by force
qed force+

lemma var_subterm_trmssst_is_varssst: "Var x ∈ subtermsset (trmssst A) ⟹ x ∈ varssst A"
proof (induction A)
  case (Cons a A)
  show ?case
  proof (cases "Var x ∈ subtermsset (trmssst A)")
    case True thus ?thesis using Cons.IH by (simp add: varssst_def)
  next
    case False thus ?thesis
      using Cons.prems var_subterm_trmssstp_is_varssstp
      by (fastforce simp add: varssst_def)
  qed
qed simp

lemma var_trmssst_is_varssst: "Var x ∈ trmssst A ⟹ x ∈ varssst A"
by (meson var_subterm_trmssst_is_varssst UN_I term.order_refl)

lemma iksst_trmssst_subset: "iksst A ⊆ trmssst A"
by (force simp add: iksst_def)

lemma var_subterm_iksst_is_varssst: "Var x ∈ subtermsset (iksst A) ⟹ x ∈ varssst A"
using var_subterm_trmssst_is_varssst iksst_trmssst_subset by fast

lemma var_subterm_iksst_is_fvsst:
  assumes "Var x ∈ subtermsset (iksst A)"
  shows "x ∈ fvsst A"
proof -
  obtain ts where ts: "Receive ts ∈ set A" "Var x ⊑set set ts"
    using assms unfolding iksst_def by moura
  hence "fvset (set ts) ⊆ fvsst A" unfolding fvsst_def by force
  thus ?thesis using ts(2) subterm_is_var by fastforce
qed

lemma fv_iksst_is_fvsst:
  assumes "x ∈ fvset (iksst A)"
  shows "x ∈ fvsst A"
using var_subterm_iksst_is_fvsst assms var_is_subterm by fastforce

lemma fv_trmssst_subset:
  "fvset (trmssst S) ⊆ varssst S"
  "fvsst S ⊆ fvset (trmssst S)"
proof (induction S)
  case (Cons x S)
  have *: "fvset (trmssst (x#S)) = fvset (trmssstp x) ∪ fvset (trmssst S)"
          "fvsst (x#S) = fvsstp x ∪ fvsst S" "varssst (x#S) = varssstp x ∪ varssst S"
    unfolding trmssst_def fvsst_def varssst_def
    by auto

  { case 1
    show ?case using Cons.IH(1)
    proof (cases x)
      case (NegChecks X F G)
      hence "trmssstp x = trmspairs F ∪ trmspairs G"
            "varssstp x = fvpairs F ∪ fvpairs G ∪ set X"
        by (simp, meson varssstp_cases(7))
      hence "fvset (trmssstp x) ⊆ varssstp x"
        using fv_trmspairs_is_fvpairs[of F] fv_trmspairs_is_fvpairs[of G]
        by auto
      thus ?thesis
        using Cons.IH(1) *(1,3)
        by blast
    qed auto
  }

  { case 2
    show ?case using Cons.IH(2)
    proof (cases x)
      case (NegChecks X F G)
      hence "trmssstp x = trmspairs F ∪ trmspairs G"
            "fvsstp x = (fvpairs F ∪ fvpairs G) - set X"
        by auto
      hence "fvsstp x ⊆ fvset (trmssstp x)"
        using fv_trmspairs_is_fvpairs[of F] fv_trmspairs_is_fvpairs[of G]
        by auto
      thus ?thesis
        using Cons.IH(2) *(1,2)
        by blast
    qed auto
  }
qed simp_all

lemma fv_ik_subset_fv_sst'[simp]: "fvset (iksst S) ⊆ fvsst S"
unfolding iksst_def by (induct S) auto

lemma fv_ik_subset_vars_sst'[simp]: "fvset (iksst S) ⊆ varssst S"
using fv_ik_subset_fv_sst' fv_trmssst_subset by fast

lemma iksst_var_is_fv: "Var x ∈ subtermsset (iksst A) ⟹ x ∈ fvsst A"
by (meson fv_ik_subset_fv_sst'[of A] fv_subset_subterms subsetCE term.set_intros(3))

lemma varssstp_subst_cases':
  assumes x: "x ∈ varssstp (s ⋅sstp θ)"
  shows "x ∈ varssstp s ∨ x ∈ fvset (θ ` varssstp s)"
using x vars_term_subst[of _ θ] varssstp_cases(1,2,3,4,5,6) varssstp_subst_cases(1,2)[of _ θ]
      varssstp_subst_cases(3,6)[of _ _ _ θ] varssstp_subst_cases(4,5)[of _ _ θ]
proof (cases s)
  case (NegChecks X F G)
  let ?θ' = "rm_vars (set X) θ"
  have "x ∈ fvpairs (F ⋅pairs ?θ') ∨ x ∈ fvpairs (G ⋅pairs ?θ') ∨ x ∈ set X"
    using varssstp_subst_cases(7)[of X F G θ] x NegChecks by simp
  hence "x ∈ fvset (?θ' ` fvpairs F) ∨ x ∈ fvset (?θ' ` fvpairs G) ∨ x ∈ set X"
    using fvpairs_subst[of _ ?θ'] by blast
  hence "x ∈ fvset (θ ` fvpairs F) ∨ x ∈ fvset (θ ` fvpairs G) ∨ x ∈ set X"
    using rm_vars_fvset_subst by fast
  thus ?thesis
    using NegChecks varssstp_cases(7)[of X F G]
    by auto
qed simp_all

lemma varssst_subst_cases:
  assumes "x ∈ varssst (S ⋅sst θ)"
  shows "x ∈ varssst S ∨ x ∈ fvset (θ ` varssst S)"
  using assms
proof (induction S)
  case (Cons s S) thus ?case
  proof (cases "x ∈ varssst (S ⋅sst θ)")
    case False
    note * = subst_sst_cons[of s S θ] varssst_Cons[of "s ⋅sstp θ" "S ⋅sst θ"] varssst_Cons[of s S]
    have **: "x ∈ varssstp (s ⋅sstp θ)" using Cons.prems False * by simp
    show ?thesis using varssstp_subst_cases'[OF **] * by auto
  qed (auto simp add: varssst_def)
qed simp

lemma subset_subst_pairs_diff_exists:
  fixes ℐ::"('a,'b) subst" and D D'::"('a,'b) dbstate"
  shows "∃Di. Di ⊆ D ∧ Di ⋅pset ℐ = (D ⋅pset ℐ) - D'"
by (metis (no_types, lifting) Diff_subset subset_image_iff)

lemma subset_subst_pairs_diff_exists':
  fixes ℐ::"('a,'b) subst" and D::"('a,'b) dbstate"
  assumes "finite D"
  shows "∃Di. Di ⊆ D ∧ Di ⋅pset ℐ ⊆ {d ⋅p ℐ} ∧ d ⋅p ℐ ∉ (D - Di) ⋅pset ℐ"
using assms
proof (induction D rule: finite_induct)
  case (insert d' D)
  then obtain Di where IH: "Di ⊆ D" "Di ⋅pset ℐ ⊆ {d ⋅p ℐ}" "d ⋅p ℐ ∉ (D - Di) ⋅pset ℐ" by moura
  show ?case
  proof (cases "d' ⋅p ℐ = d ⋅p ℐ")
    case True
    hence "insert d' Di ⊆ insert d' D" "insert d' Di ⋅pset ℐ ⊆ {d ⋅p ℐ}"
          "d ⋅p ℐ ∉ (insert d' D - insert d' Di) ⋅pset ℐ" 
      using IH by auto
    thus ?thesis by metis
  next
    case False
    hence "Di ⊆ insert d' D" "Di ⋅pset ℐ ⊆ {d ⋅p ℐ}"
          "d ⋅p ℐ ∉ (insert d' D - Di) ⋅pset ℐ" 
      using IH by auto
    thus ?thesis by metis
  qed
qed simp

lemma stateful_strand_step_subst_inI[intro]:
  "send⟨ts⟩ ∈ set A ⟹ send⟨ts ⋅list θ⟩ ∈ set (A ⋅sst θ)"
  "receive⟨ts⟩ ∈ set A ⟹ receive⟨ts ⋅list θ⟩ ∈ set (A ⋅sst θ)"
  "⟨c: t ≐ s⟩ ∈ set A ⟹ ⟨c: (t ⋅ θ) ≐ (s ⋅ θ)⟩ ∈ set (A ⋅sst θ)"
  "insert⟨t, s⟩ ∈ set A ⟹ insert⟨t ⋅ θ, s ⋅ θ⟩ ∈ set (A ⋅sst θ)"
  "delete⟨t, s⟩ ∈ set A ⟹ delete⟨t ⋅ θ, s ⋅ θ⟩ ∈ set (A ⋅sst θ)"
  "⟨c: t ∈ s⟩ ∈ set A ⟹ ⟨c: (t ⋅ θ) ∈ (s ⋅ θ)⟩ ∈ set (A ⋅sst θ)"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set A 
    ⟹ ∀X⟨∨≠: (F ⋅pairs rm_vars (set X) θ) ∨∉: (G ⋅pairs rm_vars (set X) θ)⟩ ∈ set (A ⋅sst θ)"
  "⟨t != s⟩ ∈ set A ⟹ ⟨t ⋅ θ != s ⋅ θ⟩ ∈ set (A ⋅sst θ)"
  "⟨t not in s⟩ ∈ set A ⟹ ⟨t ⋅ θ not in s ⋅ θ⟩ ∈ set (A ⋅sst θ)"
proof (induction A)
  case (Cons a A)
  note * = subst_sst_cons[of a A θ]
  { case 1 thus ?case using Cons.IH(1) * by (cases a) auto }
  { case 2 thus ?case using Cons.IH(2) * by (cases a) auto }
  { case 3 thus ?case using Cons.IH(3) * by (cases a) auto }
  { case 4 thus ?case using Cons.IH(4) * by (cases a) auto }
  { case 5 thus ?case using Cons.IH(5) * by (cases a) auto }
  { case 6 thus ?case using Cons.IH(6) * by (cases a) auto }
  { case 7 thus ?case using Cons.IH(7) * by (cases a) auto }
  { case 8 thus ?case using Cons.IH(8) * by (cases a) auto }
  { case 9 thus ?case using Cons.IH(9) * by (cases a) auto }
qed simp_all

lemma stateful_strand_step_cases_subst:
  "is_Send a = is_Send (a ⋅sstp θ)"
  "is_Receive a = is_Receive (a ⋅sstp θ)"
  "is_Equality a = is_Equality (a ⋅sstp θ)"
  "is_Insert a = is_Insert (a ⋅sstp θ)"
  "is_Delete a = is_Delete (a ⋅sstp θ)"
  "is_InSet a = is_InSet (a ⋅sstp θ)"
  "is_NegChecks a = is_NegChecks (a ⋅sstp θ)"
  "is_Assignment a = is_Assignment (a ⋅sstp θ)"
  "is_Check a = is_Check (a ⋅sstp θ)"
  "is_Update a = is_Update (a ⋅sstp θ)"
  "is_Check_or_Assignment a = is_Check_or_Assignment (a ⋅sstp θ)"
by (cases a; simp_all)+

lemma stateful_strand_step_substD:
  "a ⋅sstp σ = send⟨ts⟩ ⟹ ∃ts'. ts = ts' ⋅list σ ∧ a = send⟨ts'⟩"
  "a ⋅sstp σ = receive⟨ts⟩ ⟹ ∃ts'. ts = ts' ⋅list σ ∧ a = receive⟨ts'⟩"
  "a ⋅sstp σ = ⟨c: t ≐ s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = ⟨c: t' ≐ s'⟩"
  "a ⋅sstp σ = insert⟨t,s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = insert⟨t',s'⟩"
  "a ⋅sstp σ = delete⟨t,s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = delete⟨t',s'⟩"
  "a ⋅sstp σ = ⟨c: t ∈ s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = ⟨c: t' ∈ s'⟩"
  "a ⋅sstp σ = ∀X⟨∨≠: F ∨∉: G⟩ ⟹
    ∃F' G'. F = F' ⋅pairs rm_vars (set X) σ ∧ G = G' ⋅pairs rm_vars (set X) σ ∧
            a = ∀X⟨∨≠: F' ∨∉: G'⟩"
  "a ⋅sstp σ = ⟨t != s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = ⟨t' != s'⟩"
  "a ⋅sstp σ = ⟨t not in s⟩ ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = ⟨t' not in s'⟩"
by (cases a; auto simp add: subst_apply_pairs_def; fail)+

lemma stateful_strand_step_mem_substD:
  "send⟨ts⟩ ∈ set (S ⋅sst σ) ⟹ ∃ts'. ts = ts' ⋅list σ ∧ send⟨ts'⟩ ∈ set S"
  "receive⟨ts⟩ ∈ set (S ⋅sst σ) ⟹ ∃ts'. ts = ts' ⋅list σ ∧ receive⟨ts'⟩ ∈ set S"
  "⟨c: t ≐ s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ ⟨c: t' ≐ s'⟩ ∈ set S"
  "insert⟨t,s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ insert⟨t',s'⟩ ∈ set S"
  "delete⟨t,s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ delete⟨t',s'⟩ ∈ set S"
  "⟨c: t ∈ s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ ⟨c: t' ∈ s'⟩ ∈ set S"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set (S ⋅sst σ) ⟹
    ∃F' G'. F = F' ⋅pairs rm_vars (set X) σ ∧ G = G' ⋅pairs rm_vars (set X) σ ∧
            ∀X⟨∨≠: F' ∨∉: G'⟩ ∈ set S"
  "⟨t != s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ ⟨t' != s'⟩ ∈ set S"
  "⟨t not in s⟩ ∈ set (S ⋅sst σ) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ ⟨t' not in s'⟩ ∈ set S"
proof (induction S)
  case (Cons a S)
  have *: "x ∈ set (S ⋅sst σ)"
    when "x ∈ set (a#S ⋅sst σ)" "x ≠ a ⋅sstp σ" for x
    using that by (simp add: subst_apply_stateful_strand_def)

  { case 1 thus ?case using Cons.IH(1)[OF *] by (cases a) auto }
  { case 2 thus ?case using Cons.IH(2)[OF *] by (cases a) auto }
  { case 3 thus ?case using Cons.IH(3)[OF *] by (cases a) auto }
  { case 4 thus ?case using Cons.IH(4)[OF *] by (cases a) auto }
  { case 5 thus ?case using Cons.IH(5)[OF *] by (cases a) auto }
  { case 6 thus ?case using Cons.IH(6)[OF *] by (cases a) auto }
  { case 7 thus ?case using Cons.IH(7)[OF *] by (cases a) auto }
  { case 8 show ?case
    proof (cases a)
      case (NegChecks Y F' G') thus ?thesis
      proof (cases "⟨t != s⟩ = a ⋅sstp σ")
        case True thus ?thesis using NegChecks stateful_strand_step_substD(8)[of a σ t s] by force
      qed (use 8 Cons.IH(8)[OF *] in auto)
    qed (use 8 Cons.IH(8)[OF *] in simp_all)
  }
  { case 9 show ?case
    proof (cases a)
      case (NegChecks Y F' G') thus ?thesis
      proof (cases "⟨t not in s⟩ = a ⋅sstp σ")
        case True thus ?thesis using NegChecks stateful_strand_step_substD(9)[of a σ t s] by force
      qed (use 9 Cons.IH(9)[OF *] in auto)
    qed (use 9 Cons.IH(9)[OF *] in simp_all)
  }
qed simp_all

lemma stateful_strand_step_fv_subset_cases:
  "send⟨ts⟩ ∈ set S ⟹ fvset (set ts) ⊆ fvsst S"
  "receive⟨ts⟩ ∈ set S ⟹ fvset (set ts) ⊆ fvsst S"
  "⟨c: t ≐ s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
  "insert⟨t,s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
  "delete⟨t,s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
  "⟨c: t ∈ s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set S ⟹ fvpairs F ∪ fvpairs G - set X ⊆ fvsst S"
  "⟨t != s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
  "⟨t not in s⟩ ∈ set S ⟹ fv t ∪ fv s ⊆ fvsst S"
proof (induction S)
  case (Cons a S)
  { case 1 thus ?case using Cons.IH(1) by auto }
  { case 2 thus ?case using Cons.IH(2) by auto }
  { case 3 thus ?case using Cons.IH(3) by auto }
  { case 4 thus ?case using Cons.IH(4) by auto }
  { case 5 thus ?case using Cons.IH(5) by auto }
  { case 6 thus ?case using Cons.IH(6) by auto }
  { case 7 thus ?case using Cons.IH(7) by fastforce }
  { case 8 thus ?case using Cons.IH(8) by fastforce }
  { case 9 thus ?case using Cons.IH(9) by fastforce }
qed simp_all

lemma trmssst_nil[simp]:
  "trmssst [] = {}"
unfolding trmssst_def by simp

lemma trmssst_mono:
  "set M ⊆ set N ⟹ trmssst M ⊆ trmssst N"
by auto

lemma trmssst_memI[intro?]:
  "send⟨ts⟩ ∈ set S ⟹ t ∈ set ts ⟹ t ∈ trmssst S"
  "receive⟨ts⟩ ∈ set S ⟹ t ∈ set ts ⟹ t ∈ trmssst S"
  "⟨ac: t ≐ s⟩ ∈ set S ⟹ t ∈ trmssst S"
  "⟨ac: t ≐ s⟩ ∈ set S ⟹ s ∈ trmssst S"
  "insert⟨t,s⟩ ∈ set S ⟹ t ∈ trmssst S"
  "insert⟨t,s⟩ ∈ set S ⟹ s ∈ trmssst S"
  "delete⟨t,s⟩ ∈ set S ⟹ t ∈ trmssst S"
  "delete⟨t,s⟩ ∈ set S ⟹ s ∈ trmssst S"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set S ⟹ t ∈ trmspairs F ⟹ t ∈ trmssst S"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set S ⟹ t ∈ trmspairs G ⟹ t ∈ trmssst S"
unfolding trmssst_def by fastforce+

lemma trmssst_in:
  assumes "t ∈ trmssst S"
  shows "∃a ∈ set S. t ∈ trmssstp a"
using assms unfolding trmssst_def by simp

lemma trmssst_cons: "trmssst (a#A) = trmssstp a ∪ trmssst A"
unfolding trmssst_def by force

lemma trmssst_append[simp]: "trmssst (A@B) = trmssst A ∪ trmssst B"
unfolding trmssst_def by force

lemma trmssstp_subst:
  assumes "set (bvarssstp a) ∩ subst_domain θ = {}"
  shows "trmssstp (a ⋅sstp θ) = trmssstp a ⋅set θ"
proof (cases a)
  case (NegChecks X F G)
  hence "rm_vars (set X) θ = θ" using assms rm_vars_apply'[of θ "set X"] by auto
  hence "trmssstp (a ⋅sstp θ) = trmspairs (F ⋅pairs θ) ∪ trmspairs (G ⋅pairs θ)"
        "trmssstp a ⋅set θ = (trmspairs F ⋅set θ) ∪ (trmspairs G ⋅set θ)"
    using NegChecks image_Un by simp_all
  thus ?thesis by (metis trmspairs_subst)
qed simp_all

lemma trmssstp_subst':
  assumes "¬is_NegChecks a"
  shows "trmssstp (a ⋅sstp θ) = trmssstp a ⋅set θ"
using assms by (cases a) simp_all

lemma trmssstp_subst'':
  fixes t::"('a,'b) term" and δ::"('a,'b) subst"
  assumes "t ∈ trmssstp (b ⋅sstp δ)"
  shows "∃s ∈ trmssstp b. t = s ⋅ rm_vars (set (bvarssstp b)) δ"
proof (cases "is_NegChecks b")
  case True
  then obtain X F G where *: "b = NegChecks X F G" by (cases b) moura+
  thus ?thesis using assms trmspairs_subst[of _ "rm_vars (set X) δ"] by auto
next
  case False
  hence "trmssstp (b ⋅sstp δ) = trmssstp b ⋅set rm_vars (set (bvarssstp b)) δ"
    using trmssstp_subst' bvarssstp_NegChecks
    by fastforce
  thus ?thesis using assms by fast
qed

lemma trmssstp_subst''':
  fixes t::"('a,'b) term" and δ θ::"('a,'b) subst"
  assumes "t ∈ trmssstp (b ⋅sstp δ) ⋅set θ"
  shows "∃s ∈ trmssstp b. t = s ⋅ rm_vars (set (bvarssstp b)) δ ∘s θ"
proof -
  obtain s where s: "s ∈ trmssstp (b ⋅sstp δ)" "t = s ⋅ θ" using assms by moura
  show ?thesis using trmssstp_subst''[OF s(1)] s(2) by auto
qed

lemma trmssst_subst:
  assumes "bvarssst S ∩ subst_domain θ = {}"
  shows "trmssst (S ⋅sst θ) = trmssst S ⋅set θ"
using assms
proof (induction S)
  case (Cons a S)
  hence IH: "trmssst (S ⋅sst θ) = trmssst S ⋅set θ" and *: "set (bvarssstp a) ∩ subst_domain θ = {}"
    by auto
  show ?case using trmssstp_subst[OF *] IH by (auto simp add: subst_apply_stateful_strand_def)
qed simp

lemma trmssst_subst_cons:
  "trmssst (a#A ⋅sst δ) = trmssstp (a ⋅sstp δ) ∪ trmssst (A ⋅sst δ)"
using subst_sst_cons[of a A δ] trmssst_cons[of a A] trmssst_append by simp

lemma (in intruder_model) wftrms_trmssstp_subst:
  assumes "wftrms (trmssstp a ⋅set δ)"
  shows "wftrms (trmssstp (a ⋅sstp δ))"
  using assms
proof (cases a)
  case (NegChecks X F G)
  hence *: "trmssstp (a ⋅sstp δ) =
              (trmspairs (F ⋅pairs rm_vars (set X) δ)) ∪ (trmspairs (G ⋅pairs rm_vars (set X) δ))"
    by simp

  have "trmssstp a ⋅set δ = (trmspairs F ⋅set δ) ∪ (trmspairs G ⋅set δ)"
    using NegChecks image_Un by simp
  hence "wftrms (trmspairs F ⋅set δ)" "wftrms (trmspairs G ⋅set δ)" using * assms by auto
  hence "wftrms (trmspairs F ⋅set rm_vars (set X) δ)"
        "wftrms (trmspairs G ⋅set rm_vars (set X) δ)"
    using wf_trms_subst_rm_vars[of δ "trmspairs F" "set X"]
          wf_trms_subst_rm_vars[of δ "trmspairs G" "set X"]
    by fast+
  thus ?thesis
    using * trmspairs_subst[of _ "rm_vars (set X) δ"]
    by auto
qed auto

lemma trmssst_fv_varssst_subset: "t ∈ trmssst A ⟹ fv t ⊆ varssst A" 
proof (induction A)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma trmssst_fv_subst_subset:
  assumes "t ∈ trmssst S" "subst_domain θ ∩ bvarssst S = {}"
  shows "fv (t ⋅ θ) ⊆ varssst (S ⋅sst θ)"
using assms
proof (induction S)
  case (Cons s S) show ?case
  proof (cases "t ∈ trmssst S")
    case True
    hence "fv (t ⋅ θ) ⊆ varssst (S ⋅sst θ)" using Cons.IH Cons.prems by auto
    thus ?thesis using subst_sst_cons[of s S θ] unfolding varssst_def by auto
  next
    case False
    hence *: "t ∈ trmssstp s" "subst_domain θ ∩ set (bvarssstp s) = {}" using Cons.prems by auto
    hence "fv (t ⋅ θ) ⊆ varssstp (s ⋅sstp θ)"
    proof (cases s)
      case (NegChecks X F G)
      hence **: "t ∈ trmspairs F ∨ t ∈ trmspairs G" using *(1) by auto
      have ***: "rm_vars (set X) θ = θ" using *(2) NegChecks rm_vars_apply' by auto
      have "fv (t ⋅ θ) ⊆ fvpairs (F ⋅pairs rm_vars (set X) θ) ∪ fvpairs (G ⋅pairs rm_vars (set X) θ)"
        using ** *** trmspairs_fv_subst_subset[of t _ θ] by auto
      thus ?thesis using *(2) using NegChecks varssstp_subst_cases(7)[of X F G θ] by blast
    qed auto
    thus ?thesis using subst_sst_cons[of s S θ] unfolding varssst_def by auto
  qed
qed simp

lemma trmssst_fv_subst_subset':
  assumes "t ∈ subtermsset (trmssst S)" "fv t ∩ bvarssst S = {}" "fv (t ⋅ θ) ∩ bvarssst S = {}"
  shows "fv (t ⋅ θ) ⊆ fvsst (S ⋅sst θ)"
using assms
proof (induction S)
  case (Cons s S) show ?case
  proof (cases "t ∈ subtermsset (trmssst S)")
    case True
    hence "fv (t ⋅ θ) ⊆ fvsst (S ⋅sst θ)" using Cons.IH Cons.prems by auto
    thus ?thesis using subst_sst_cons[of s S θ] unfolding varssst_def by auto
  next
    case False
    hence 0: "t ∈ subtermsset (trmssstp s)" "fv t ∩ set (bvarssstp s) = {}"
             "fv (t ⋅ θ) ∩ set (bvarssstp s) = {}"
      using Cons.prems by auto

    note 1 = UN_Un UN_insert fvset.simps subst_apply_fv_subset subst_apply_fv_unfold
             subst_apply_term_empty sup_bot.comm_neutral fv_subterms_set fv_subset[OF 0(1)]

    note 2 = subst_apply_fv_union

    have "fv (t ⋅ θ) ⊆ fvsstp (s ⋅sstp θ)"
    proof (cases s)
      case (Send ts)
      have "fv t ⊆ fvset (set ts)" using fv_subset[OF 0(1)] unfolding Send fv_subterms_set by simp
      hence "fv (t ⋅ θ) ⊆ fvset (set ts ⋅set θ)"
        by (metis subst_apply_fv_subset subst_apply_fv_unfold_set)
      thus ?thesis using Send by simp
    next
      case (Receive ts)
      have "fv t ⊆ fvset (set ts)" using fv_subset[OF 0(1)] unfolding Receive fv_subterms_set by simp
      hence "fv (t ⋅ θ) ⊆ fvset (set ts ⋅set θ)"
        by (metis subst_apply_fv_subset subst_apply_fv_unfold_set)
      thus ?thesis using Receive by simp
    next
      case (NegChecks X F G)
      hence 3: "t ∈ subtermsset (trmspairs F) ∨ t ∈ subtermsset (trmspairs G)" using 0(1) by auto
      have "t ⋅ rm_vars (set X) θ = t ⋅ θ" using 0(2) NegChecks rm_vars_ident[of t] by auto
      hence "fv (t ⋅ θ) ⊆ fvpairs (F ⋅pairs rm_vars (set X) θ) ∪ fvpairs (G ⋅pairs rm_vars (set X) θ)"
        using 3 trmspairs_fv_subst_subset'[of t _ "rm_vars (set X) θ"] by fastforce
      thus ?thesis using 0(2,3) NegChecks fvsstp_subst_cases(7)[of X F G θ] by auto
    qed (metis (no_types, lifting) 1 2 trmssstp.simps(3) fvsstp_subst_cases(3),
         metis (no_types, lifting) 1 2 trmssstp.simps(4) fvsstp_subst_cases(4),
         metis (no_types, lifting) 1 2 trmssstp.simps(5) fvsstp_subst_cases(5),
         metis (no_types, lifting) 1 2 trmssstp.simps(6) fvsstp_subst_cases(6))
    thus ?thesis using subst_sst_cons[of s S θ] unfolding fvsst_def by auto
  qed
qed simp

lemma trmssstp_funs_term_cases:
  assumes "t ∈ trmssstp (s ⋅sstp θ)" "f ∈ funs_term t"
  shows "(∃u ∈ trmssstp s. f ∈ funs_term u) ∨ (∃x ∈ fvsstp s. f ∈ funs_term (θ x))"
  using assms
proof (cases s)
  case (NegChecks X F G)
  hence "t ∈ trmspairs (F ⋅pairs rm_vars (set X) θ) ∨ t ∈ trmspairs (G ⋅pairs rm_vars (set X) θ)"
    using assms(1) by auto
  hence "(∃u∈trmspairs F. f ∈ funs_term u) ∨ (∃x∈fvpairs F. f ∈ funs_term (rm_vars (set X) θ x)) ∨
         (∃u∈trmspairs G. f ∈ funs_term u) ∨ (∃x∈fvpairs G. f ∈ funs_term (rm_vars (set X) θ x))"
    using trmspairs_funs_term_cases[OF _ assms(2), of _ "rm_vars (set X) θ"] by meson
  hence "(∃u ∈ trmspairs F ∪ trmspairs G. f ∈ funs_term u) ∨
         (∃x ∈ fvpairs F ∪ fvpairs G. f ∈ funs_term (rm_vars (set X) θ x))"
    by blast
  thus ?thesis
  proof
    assume "∃x ∈ fvpairs F ∪ fvpairs G. f ∈ funs_term (rm_vars (set X) θ x)"
    then obtain x where x: "x ∈ fvpairs F ∪ fvpairs G" "f ∈ funs_term (rm_vars (set X) θ x)"
      by auto
    hence "x ∉ set X" "rm_vars (set X) θ x = θ x" by auto
    thus ?thesis using x by (auto simp add: assms NegChecks)
  qed (auto simp add: assms NegChecks)
qed (use assms funs_term_subst[of _ θ] in auto)

lemma trmssst_funs_term_cases:
  assumes "t ∈ trmssst (S ⋅sst θ)" "f ∈ funs_term t"
  shows "(∃u ∈ trmssst S. f ∈ funs_term u) ∨ (∃x ∈ fvsst S. f ∈ funs_term (θ x))"
using assms(1)
proof (induction S)
  case (Cons s S) thus ?case
  proof (cases "t ∈ trmssst (S ⋅sst θ)")
    case False
    hence "t ∈ trmssstp (s ⋅sstp θ)" using Cons.prems(1) subst_sst_cons[of s S θ] trmssst_cons by auto
    thus ?thesis using trmssstp_funs_term_cases[OF _ assms(2)] by fastforce
  qed auto
qed simp

lemma fvsst_is_subterm_trmssst_subst:
  assumes "x ∈ fvsst T"
    and "bvarssst T ∩ subst_domain θ = {}"
  shows "θ x ∈ subtermsset (trmssst (T ⋅sst θ))"
using trmssst_subst[OF assms(2)] subterms_subst_subset'[of θ "trmssst T"]
      fvsst_is_subterm_trmssst[OF assms(1)]
by (metis (no_types, lifting) image_iff subset_iff eval_term.simps(1))

lemma fvsst_subst_fv_subset:
  assumes "x ∈ fvsst S" "x ∉ bvarssst S" "fv (θ x) ∩ bvarssst S = {}"
  shows "fv (θ x) ⊆ fvsst (S ⋅sst θ)"
using assms
proof (induction S)
  case (Cons a S)
  note 1 = fv_subst_subset[of _ _ θ]
  note 2 = subst_apply_fv_union subst_apply_fv_unfold[of _ θ] fv_subset image_eqI
  note 3 = fvsstp_subst_cases
  note 4 = fvsstp.simps
  from Cons show ?case
  proof (cases "x ∈ fvsst S")
    case False
    hence 5: "x ∈ fvsstp a" " fv (θ x) ∩ set (bvarssstp a) = {}" "x ∉ set (bvarssstp a)"
      using Cons.prems by auto
    hence "fv (θ x) ⊆ fvsstp (a ⋅sstp θ)"
    proof (cases a)
      case (Send ts) thus ?thesis using 1 5(1) 3(1) 4(1) by auto
    next
      case (Receive ts) thus ?thesis using 1 5(1) 3(2) 4(2) by auto
    next
      case (NegChecks X F G)
      let ?δ = "rm_vars (set X) θ"
      have *: "x ∈ fvpairs F ∪ fvpairs G" using NegChecks 5(1) by auto
      have **: "fv (θ x) ∩ set X = {}" using NegChecks 5(2) by simp
      have ***: "θ x = ?δ x" using NegChecks 5(3) by auto
      have "fv (θ x) ⊆ fvpairs (F ⋅pairs ?δ) ∪ fvpairs (G ⋅pairs ?δ)"
        using fvpairs_subst_fv_subset[of x _ ?δ] * *** by auto
      thus ?thesis using NegChecks ** by auto
    qed (metis (full_types) 2 5(1) 3(3) 4(3), metis (full_types) 2 5(1) 3(4) 4(4),
         metis (full_types) 2 5(1) 3(5) 4(5), metis (full_types) 2 5(1) 3(6) 4(6))
    thus ?thesis by (auto simp add: subst_sst_cons[of a S θ])
  qed (auto simp add: subst_sst_cons[of a S θ])
qed simp

lemma (in intruder_model) wftrms_trmssst_subst:
  assumes "wftrms (trmssst A ⋅set δ)"
  shows "wftrms (trmssst (A ⋅sst δ))"
  using assms
proof (induction A)
  case (Cons a A)
  hence IH: "wftrms (trmssst (A ⋅sst δ))" and *: "wftrms (trmssstp a ⋅set δ)" by auto
  have "wftrms (trmssstp (a ⋅sstp δ))" by (rule wftrms_trmssstp_subst[OF *])
  thus ?case using IH trmssst_subst_cons[of a A δ] by blast
qed simp

lemma fvsst_subst_obtain_var:
  assumes "x ∈ fvsst (S ⋅sst δ)"
  shows "∃y ∈ fvsst S. x ∈ fv (δ y)"
  using assms
proof (induction S)
  case (Cons s S)
  hence "x ∈ fvsst (S ⋅sst δ) ⟹ ∃y ∈ fvsst S. x ∈ fv (δ y)"
    using bvarssst_cons_subset[of S s]
    by blast
  thus ?case
  proof (cases "x ∈ fvsst (S ⋅sst δ)")
    case False
    hence *: "x ∈ fvsstp (s ⋅sstp δ)"
      using Cons.prems(1) subst_sst_cons[of s S δ]
      by fastforce

    have "∃y ∈ fvsstp s. x ∈ fv (δ y)"
    proof (cases s)
      case (NegChecks X F G)
      hence "x ∈ fvpairs (F ⋅pairs rm_vars (set X) δ) ∨ x ∈ fvpairs (G ⋅pairs rm_vars (set X) δ)"
          and **: "x ∉ set X"
        using * by simp_all
      then obtain y where y: "y ∈ fvpairs F ∨ y ∈ fvpairs G" "x ∈ fv ((rm_vars (set X) δ) y)"
        using fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
        by blast
      have "y ∉ set X"
      proof
        assume y_in: "y ∈ set X"
        hence "(rm_vars (set X) δ) y = Var y" by auto
        hence "x = y" using y(2) by simp
        thus False using ** y_in by metis
      qed
      thus ?thesis using NegChecks y by auto
    qed (use * fv_subst_obtain_var in force)+
    thus ?thesis by auto
  qed auto
qed simp

lemma fvsst_subst_subset_range_vars_if_subset_domain:
  assumes "fvsst S ⊆ subst_domain σ"
  shows "fvsst (S ⋅sst σ) ⊆ range_vars σ"
using assms fvsst_subst_obtain_var[of _ S σ] subst_dom_vars_in_subst[of _ σ] subst_fv_imgI[of σ]
by (metis (no_types) in_mono subsetI)

lemma fvsst_in_fv_trmssst: "x ∈ fvsst S ⟹ x ∈ fvset (trmssst S)"
proof (induction S)
  case (Cons s S) thus ?case
  proof (cases "x ∈ fvsst S")
    case False
    hence *: "x ∈ fvsstp s" using Cons.prems by simp
    hence "x ∈ fvset (trmssstp s)"
    proof (cases s)
      case (NegChecks X F G)
      hence "x ∈ fvpairs F ∨ x ∈ fvpairs G" using * by simp_all
      thus ?thesis using * fvpairs_in_fv_trmspairs[of x] NegChecks by auto
    qed auto
    thus ?thesis by simp
  qed simp
qed simp

lemma fvsstp_ground_subst_compose:
  assumes "subst_domain δ = subst_domain σ"
    and "range_vars δ = {}" "range_vars σ = {}"
  shows "fvsstp (a ⋅sstp δ ∘s θ) = fvsstp (a ⋅sstp σ ∘s θ)"
proof -
  note 0 = fv_ground_subst_compose

  have 1: "range_vars δ ∩ set (bvarssstp a) = {}" "range_vars σ ∩ set (bvarssstp a) = {}"
    using assms(2,3) by (blast,blast)

  note 2 = 0[OF assms, of _ θ]

  show ?thesis
  proof (cases a)
    case (NegChecks X F G)
    have 3: "range_vars δ ∩ set X = {}" "range_vars (rm_vars (set X) δ) = {}"
            "range_vars σ ∩ set X = {}" "range_vars (rm_vars (set X) σ) = {}"
      using assms(2,3) rm_vars_img_fv_subset[of "set X"] by auto

    have 4: "subst_domain (rm_vars (set X) δ) = subst_domain (rm_vars (set X) σ)"
      using assms(1) rm_vars_dom[of "set X"] by blast

    have 5: "fv (t ⋅ rm_vars (set X) (δ ∘s θ)) = fv (t ⋅ rm_vars (set X) (σ ∘s θ))" for t
      using 2[of t] rm_vars_comp[OF 3(1), of t θ] rm_vars_comp[OF 3(3), of t θ]
            0[OF 4 3(2,4), of t "rm_vars (set X) θ"]
      by argo

    have 6: "fvpairs (H ⋅pairs rm_vars (set X) (δ ∘s θ)) = fvpairs (H ⋅pairs rm_vars (set X) (σ ∘s θ))"
      for H
    proof -
      have "fvpair (h ⋅p rm_vars (set X) (δ ∘s θ)) = fvpair (h ⋅p rm_vars (set X) (σ ∘s θ))" for h
      proof -
        obtain s t where h: "h = (s,t)" by (metis surj_pair)
        show ?thesis using 5[of s] 5[of t] unfolding h by fast
      qed
      thus ?thesis unfolding subst_apply_pairs_def by auto
    qed

    show ?thesis using 5 6 unfolding NegChecks by simp
  qed (use 2 in auto)
qed

lemma fvsst_ground_subst_compose:
  assumes "subst_domain δ = subst_domain σ"
    and "range_vars δ = {}" "range_vars σ = {}"
  shows "fvsst (S ⋅sst δ ∘s θ) = fvsst (S ⋅sst σ ∘s θ)"
by (induct S) (auto simp add: fvsstp_ground_subst_compose[OF assms] fvsst_Cons subst_sst_cons)

lemma stateful_strand_step_subst_comp:
  assumes "range_vars δ ∩ set (bvarssstp x) = {}"
  shows "x ⋅sstp δ ∘s θ = (x ⋅sstp δ) ⋅sstp θ"
proof (cases x)
  case (NegChecks X F G)
  hence *: "range_vars δ ∩ set X = {}" using assms by simp
  have "H ⋅pairs rm_vars (set X) (δ ∘s θ) = (H ⋅pairs rm_vars (set X) δ) ⋅pairs rm_vars (set X) θ" for H
    using pairs_subst_comp rm_vars_comp[OF *] by (induct H) (auto simp add: subst_apply_pairs_def)
  thus ?thesis using NegChecks by simp
qed simp_all

lemma stateful_strand_subst_comp:
  assumes "range_vars δ ∩ bvarssst S = {}"
  shows "S ⋅sst δ ∘s θ = (S ⋅sst δ) ⋅sst θ"
using assms
proof (induction S)
  case (Cons s S)
  hence IH: "S ⋅sst δ ∘s θ = (S ⋅sst δ) ⋅sst θ" using Cons by auto

  have "s ⋅sstp δ ∘s θ = (s ⋅sstp δ) ⋅sstp θ"
    using Cons.prems stateful_strand_step_subst_comp[of δ s θ]
    unfolding range_vars_alt_def by auto
  thus ?case using IH by (simp add: subst_apply_stateful_strand_def)
qed simp

lemma subst_apply_bvars_disj_NegChecks:
  assumes "set X ∩ subst_domain θ = {}"
  shows "NegChecks X F G ⋅sstp θ = NegChecks X (F ⋅pairs θ) (G ⋅pairs θ)"
proof -
  have "rm_vars (set X) θ = θ" using assms rm_vars_apply'[of θ "set X"] by auto
  thus ?thesis by simp
qed

lemma subst_apply_NegChecks_no_bvars[simp]:
  "∀[]⟨∨≠: F ∨∉: F'⟩ ⋅sstp θ = ∀[]⟨∨≠: (F ⋅pairs θ) ∨∉: (F' ⋅pairs θ)⟩"
  "∀[]⟨∨≠: [] ∨∉: F'⟩ ⋅sstp θ = ∀[]⟨∨≠: [] ∨∉: (F' ⋅pairs θ)⟩"
  "∀[]⟨∨≠: F ∨∉: []⟩ ⋅sstp θ = ∀[]⟨∨≠: (F ⋅pairs θ) ∨∉: []⟩"
  "∀[]⟨∨≠: [] ∨∉: [(t,s)]⟩ ⋅sstp θ = ∀[]⟨∨≠: [] ∨∉: ([(t ⋅ θ,s ⋅ θ)])⟩"
  "∀[]⟨∨≠: [(t,s)] ∨∉: []⟩ ⋅sstp θ = ∀[]⟨∨≠: ([(t ⋅ θ,s ⋅ θ)]) ∨∉: []⟩"
by simp_all

lemma setopssst_mono:
  "set M ⊆ set N ⟹ setopssst M ⊆ setopssst N"
by (auto simp add: setopssst_def)

lemma setopssst_nil[simp]: "setopssst [] = {}"
by (simp add: setopssst_def)

lemma setopssst_cons[simp]: "setopssst (a#A) = setopssstp a ∪ setopssst A"
by (simp add: setopssst_def)

lemma setopssst_cons_subset[simp]: "setopssst A ⊆ setopssst (a#A)"
using setopssst_cons[of a A] by blast

lemma setopssst_append: "setopssst (A@B) = setopssst A ∪ setopssst B"
proof (induction A)
  case (Cons a A) thus ?case by (cases a) (auto simp add: setopssst_def)
qed (simp add: setopssst_def)

lemma setopssstp_member_iff:
  "(t,s) ∈ setopssstp x ⟷
    (x = Insert t s ∨ x = Delete t s ∨ (∃ac. x = InSet ac t s) ∨
     (∃X F F'. x = NegChecks X F F' ∧ (t,s) ∈ set F'))"
by (cases x) auto

lemma setopssst_member_iff:
  "(t,s) ∈ setopssst A ⟷
    (Insert t s ∈ set A ∨ Delete t s ∈ set A ∨ (∃ac. InSet ac t s ∈ set A) ∨
     (∃X F F'. NegChecks X F F' ∈ set A ∧ (t,s) ∈ set F'))"
  (is "?P ⟷ ?Q")
proof (induction A)
  case (Cons a A) thus ?case
  proof (cases "(t, s) ∈ setopssstp a")
    case True thus ?thesis using setopssstp_member_iff[of t s a] by auto
  qed auto
qed simp

lemma setopssstp_subst:
  assumes "set (bvarssstp a) ∩ subst_domain θ = {}"
  shows "setopssstp (a ⋅sstp θ) = setopssstp a ⋅pset θ"
proof (cases a)
  case (NegChecks X F G)
  hence "rm_vars (set X) θ = θ" using assms rm_vars_apply'[of θ "set X"] by auto
  hence "setopssstp (a ⋅sstp θ) = set (G ⋅pairs θ)"
        "setopssstp a ⋅pset θ = set G ⋅pset θ"
    using NegChecks image_Un by simp_all
  thus ?thesis by (simp add: subst_apply_pairs_def) 
qed simp_all

lemma setopssstp_subst':
  assumes "¬is_NegChecks a"
  shows "setopssstp (a ⋅sstp θ) = setopssstp a ⋅pset θ"
using assms by (cases a) auto

lemma setopssstp_subst'':
  fixes t::"('a,'b) term × ('a,'b) term" and δ::"('a,'b) subst"
  assumes t: "t ∈ setopssstp (b ⋅sstp δ)"
  shows "∃s ∈ setopssstp b. t = s ⋅p rm_vars (set (bvarssstp b)) δ"
proof (cases "is_NegChecks b")
  case True
  then obtain X F G where b: "b = NegChecks X F G" by (cases b) moura+
  hence "setopssstp b = set G" "setopssstp (b ⋅sstp δ) = set (G ⋅pairs rm_vars (set (bvarssstp b)) δ)"
    by simp_all
  thus ?thesis using t subst_apply_pairs_pset_subst[of G] by blast
next
  case False
  hence "setopssstp (b ⋅sstp δ) = setopssstp b ⋅pset rm_vars (set (bvarssstp b)) δ"
    using setopssstp_subst' bvarssstp_NegChecks by fastforce
  thus ?thesis using t by blast
qed

lemma setopssst_subst:
  assumes "bvarssst S ∩ subst_domain θ = {}"
  shows "setopssst (S ⋅sst θ) = setopssst S ⋅pset θ"
using assms
proof (induction S)
  case (Cons a S)
  have "bvarssst S ∩ subst_domain θ = {}" and *: "set (bvarssstp a) ∩ subst_domain θ = {}"
    using Cons.prems by auto
  hence IH: "setopssst (S ⋅sst θ) = setopssst S ⋅pset θ"
    using Cons.IH by auto
  show ?case
    using setopssstp_subst[OF *] IH unfolding setopssst_def
    by (auto simp add: subst_apply_stateful_strand_def)
qed (simp add: setopssst_def)

lemma setopssst_subst':
  fixes p::"('a,'b) term × ('a,'b) term" and δ::"('a,'b) subst"
  assumes "p ∈ setopssst (S ⋅sst δ)"
  shows "∃s ∈ setopssst S. ∃X. set X ⊆ bvarssst S ∧ p = s ⋅p rm_vars (set X) δ"
using assms
proof (induction S)
  case (Cons a S)
  note 0 = setopssst_cons[of a S] bvarssst_Cons[of a S]
  note 1 = setopssst_cons[of "a ⋅sstp δ" "S ⋅sst δ"] subst_sst_cons[of a S δ]
  have "p ∈ setopssst (S ⋅sst δ) ∨ p ∈ setopssstp (a ⋅sstp δ)" using Cons.prems 1 by auto
  thus ?case
  proof
    assume *: "p ∈ setopssstp (a ⋅sstp δ)"
    show ?thesis using setopssstp_subst''[OF *] 0 by blast
  next
    assume *: "p ∈ setopssst (S ⋅sst δ)"
    show ?thesis using Cons.IH[OF *] 0 by blast
  qed
qed simp


subsection ‹Stateful Constraint Semantics›
context intruder_model
begin

definition negchecks_model where
  "negchecks_model (ℐ::('a,'b) subst) (D::('a,'b) dbstate) X F G ≡
      (∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ 
              (∃(t,s) ∈ set F. t ⋅ δ ∘s ℐ ≠ s ⋅ δ ∘s ℐ) ∨
              (∃(t,s) ∈ set G. (t,s) ⋅p δ ∘s ℐ ∉ D))"

fun strand_sem_stateful::
  "('fun,'var) terms ⇒ ('fun,'var) dbstate ⇒ ('fun,'var) stateful_strand ⇒ ('fun,'var) subst ⇒ bool"
  ("⟦_; _; _⟧s")
where
  "⟦M; D; []⟧s = (λℐ. True)"
| "⟦M; D; Send ts#S⟧s = (λℐ. (∀t ∈ set ts. M ⊢ t ⋅ ℐ) ∧ ⟦M; D; S⟧s ℐ)"
| "⟦M; D; Receive ts#S⟧s = (λℐ. ⟦(set ts ⋅set ℐ) ∪ M; D; S⟧s ℐ)"
| "⟦M; D; Equality _ t t'#S⟧s = (λℐ. t ⋅ ℐ = t' ⋅ ℐ ∧ ⟦M; D; S⟧s ℐ)"
| "⟦M; D; Insert t s#S⟧s = (λℐ. ⟦M; insert ((t,s) ⋅p ℐ) D; S⟧s ℐ)"
| "⟦M; D; Delete t s#S⟧s = (λℐ. ⟦M; D - {(t,s) ⋅p ℐ}; S⟧s ℐ)"
| "⟦M; D; InSet _ t s#S⟧s = (λℐ. (t,s) ⋅p ℐ ∈ D ∧ ⟦M; D; S⟧s ℐ)"
| "⟦M; D; NegChecks X F F'#S⟧s = (λℐ. negchecks_model ℐ D X F F' ∧ ⟦M; D; S⟧s ℐ)"


lemmas strand_sem_stateful_induct =
  strand_sem_stateful.induct[case_names Nil ConsSnd ConsRcv ConsEq
                                        ConsIns ConsDel ConsIn ConsNegChecks]

abbreviation constr_sem_stateful (infix "⊨s" 91) where "ℐ ⊨s A ≡ ⟦{}; {}; A⟧s ℐ"

lemma stateful_strand_sem_NegChecks_no_bvars:
  "⟦M; D; [⟨t not in s⟩]⟧s ℐ ⟷ (t ⋅ ℐ, s ⋅ ℐ) ∉ D"
  "⟦M; D; [⟨t != s⟩]⟧s ℐ ⟷ t ⋅ ℐ ≠ s ⋅ ℐ"
by (simp_all add: negchecks_model_def empty_dom_iff_empty_subst)

lemma strand_sem_ik_mono_stateful:
  "⟦M; D; A⟧s ℐ ⟹ ⟦M ∪ M'; D; A⟧s ℐ"
proof (induction A arbitrary: M M' D rule: strand_sem_stateful.induct)
  case (2 M D ts S)
  hence "∀t ∈ set ts. M ⊢ t ⋅ ℐ" "⟦M ∪ M'; D; S⟧s ℐ" by auto
  thus ?case
    using ideduct_mono[of M _ "M ∪ M'"] strand_sem_stateful.simps(2)[of "M ∪ M'" D ts S]
    by fastforce
next
  case (3 M D ts S)
  hence "⟦((set ts ⋅set ℐ) ∪ M) ∪ M'; D; S⟧s ℐ" by simp
  hence "⟦(set ts ⋅set ℐ) ∪ (M ∪ M'); D; S⟧s ℐ" by (metis Un_assoc)
  thus ?case by simp
qed simp_all

lemma strand_sem_append_stateful:
  "⟦M; D; A@B⟧s ℐ ⟷ ⟦M; D; A⟧s ℐ ∧ ⟦M ∪ (iksst A ⋅set ℐ); dbupdsst A ℐ D; B⟧s ℐ"
  (is "?P ⟷ ?Q ∧ ?R")
proof -
  have 1: "?P ⟹ ?Q" by (induct A rule: strand_sem_stateful.induct) auto

  have 2: "?P ⟹ ?R"
  proof (induction A arbitrary: M D B)
    case (Cons a A) thus ?case
    proof (cases a)
      case (Receive ts)
      have "(set ts ⋅set ℐ) ∪ (M ∪ (iksst A ⋅set ℐ)) = M ∪ (iksst (a#A) ⋅set ℐ)"
           "dbupdsst A ℐ D = dbupdsst (a#A) ℐ D"
        using Receive by (auto simp add: iksst_def)
      thus ?thesis
        using Cons Receive
        by (metis (no_types, lifting) Un_assoc append_Cons strand_sem_stateful.simps(3))
    qed (auto simp add: iksst_def)
  qed (simp add: iksst_def)

  have 3: "?Q ⟹ ?R ⟹ ?P"
  proof (induction A arbitrary: M D)
    case (Cons a A) thus ?case
    proof (cases a)
      case (Receive ts)
      have "(set ts ⋅set ℐ) ∪ (M ∪ (iksst A ⋅set ℐ)) = M ∪ (iksst (a#A) ⋅set ℐ)"
           "dbupdsst A ℐ D = dbupdsst (a#A) ℐ D"
        using Receive by (auto simp add: iksst_def)
      thus ?thesis
        using Cons Receive
        by (metis (no_types, lifting) Un_assoc append_Cons strand_sem_stateful.simps(3))
    qed (auto simp add: iksst_def)
  qed (simp add: iksst_def)

  show ?thesis by (metis 1 2 3)
qed

lemma negchecks_model_db_subset:
  fixes F F'::"(('a,'b) term × ('a,'b) term) list"
  assumes "D' ⊆ D"
  and "negchecks_model ℐ D X F F'"
  shows "negchecks_model ℐ D' X F F'"
proof -
  have "∃(s,t) ∈ set F'. (s,t) ⋅p δ ∘s ℐ ∉ D'"
    when "∃(s,t) ∈ set F'. (s,t) ⋅p δ ∘s ℐ ∉ D"
    for δ::"('a,'b) subst"
    using that assms(1) by blast
  thus ?thesis using assms(2) unfolding negchecks_model_def by meson
qed

lemma negchecks_model_db_supset:
  fixes F F'::"(('a,'b) term × ('a,'b) term) list"
  assumes "D' ⊆ D"
    and "∀f ∈ set F'. ∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ f ⋅p (δ ∘s ℐ) ∉ D - D'"
    and "negchecks_model ℐ D' X F F'"
  shows "negchecks_model ℐ D X F F'"
proof -
  have "∃(s,t) ∈ set F'. (s,t) ⋅p δ ∘s ℐ ∉ D"
    when "∃(s,t) ∈ set F'. (s,t) ⋅p δ ∘s ℐ ∉ D'" "subst_domain δ = set X ∧ ground (subst_range δ)"
    for δ::"('a,'b) subst"
    using that assms(1,2) by blast
  thus ?thesis using assms(3) unfolding negchecks_model_def by meson
qed

lemma negchecks_model_subst:
  fixes F F'::"(('a,'b) term × ('a,'b) term) list"
  assumes "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
  shows "negchecks_model (δ ∘s θ) D X F F' ⟷ negchecks_model θ D X (F ⋅pairs δ) (F' ⋅pairs δ)"
proof -
  have 0: "σ ∘s (δ ∘s θ) = δ ∘s (σ ∘s θ)"
    when σ: "subst_domain σ = set X" "ground (subst_range σ)" for σ
    by (metis (no_types, lifting) σ subst_compose_assoc assms(1) inf_sup_aci(1)
            subst_comp_eq_if_disjoint_vars sup_inf_absorb range_vars_alt_def)

  { fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set F. s ⋅ (σ ∘s (δ ∘s θ)) ≠ t ⋅ (σ ∘s (δ ∘s θ))"
    obtain f where f: "f ∈ set F" "fst f ⋅ σ ∘s (δ ∘s θ) ≠ snd f ⋅ σ ∘s (δ ∘s θ)"
      using * unfolding case_prod_unfold by (induct F) auto
    hence "(fst f ⋅ δ) ⋅ σ ∘s θ ≠ (snd f ⋅ δ) ⋅ σ ∘s θ" using 0[OF σ] by simp
    moreover have "(fst f ⋅ δ, snd f ⋅ δ) ∈ set (F ⋅pairs δ)"
      using f(1) by (auto simp add: subst_apply_pairs_def)
    ultimately have "∃(s,t) ∈ set (F ⋅pairs δ). s ⋅ (σ ∘s θ) ≠ t ⋅ (σ ∘s θ)"
      using f(1) by fastforce
  } moreover {
    fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set F'. (s,t) ⋅p σ ∘s (δ ∘s θ) ∉ D"
    obtain f where f: "f ∈ set F'" "f ⋅p σ ∘s (δ ∘s θ) ∉ D"
      using * by (induct F') auto
    hence "f ⋅p δ ⋅p σ ∘s θ ∉ D" using 0[OF σ] by (metis subst_pair_compose)
    moreover have "f ⋅p δ ∈ set (F' ⋅pairs δ)"
      using f(1) by (auto simp add: subst_apply_pairs_def)
    ultimately have "∃(s,t) ∈ set (F' ⋅pairs δ). (s,t) ⋅p σ ∘s θ ∉ D"
      using f(1) by (metis (no_types, lifting) case_prodI2)
  } moreover {
    fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set (F ⋅pairs δ). s ⋅ (σ ∘s θ) ≠ t ⋅ (σ ∘s θ)"
    obtain f where f: "f ∈ set (F ⋅pairs δ)" "fst f ⋅ σ ∘s θ ≠ snd f ⋅ σ ∘s θ"
      using * by (induct F) auto
    then obtain g where g: "g ∈ set F" "f = g ⋅p δ" by (auto simp add: subst_apply_pairs_def)
    have "fst g ⋅ σ ∘s (δ ∘s θ) ≠ snd g ⋅ σ ∘s (δ ∘s θ)"
      using f(2) g 0[OF σ] by (simp add: prod.case_eq_if)
    hence "∃(s,t) ∈ set F. s ⋅ (σ ∘s (δ ∘s θ)) ≠ t ⋅ (σ ∘s (δ ∘s θ))"
      using g by fastforce
  } moreover {
    fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set (F' ⋅pairs δ). (s,t) ⋅p (σ ∘s θ) ∉ D"
    obtain f where f: "f ∈ set (F' ⋅pairs δ)" "f ⋅p σ ∘s θ ∉ D"
      using * by (induct F') auto
    then obtain g where g: "g ∈ set F'" "f = g ⋅p δ" by (auto simp add: subst_apply_pairs_def)
    have "g ⋅p σ ∘s (δ ∘s θ) ∉ D"
      using f(2) g 0[OF σ] by (simp add: prod.case_eq_if)
    hence "∃(s,t) ∈ set F'. (s,t) ⋅p (σ ∘s (δ ∘s θ)) ∉ D"
      using g by (metis (no_types, lifting) case_prodI2)
  } ultimately show ?thesis
      using assms unfolding negchecks_model_def by meson
qed

lemma strand_sem_subst_stateful:
  fixes δ::"('fun,'var) subst"
  assumes "(subst_domain δ ∪ range_vars δ) ∩ bvarssst S = {}"
  shows "⟦M; D; S⟧s (δ ∘s θ) ⟷ ⟦M; D; S ⋅sst δ⟧s θ"
proof
  note [simp] = subst_sst_cons[of _ _ δ] subst_subst_compose[of _ δ θ]

  have "(subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
    when δ: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
      and γ: "subst_domain γ = set X" "ground (subst_range γ)"
    for X and γ::"('fun,'var) subst"
    using δ γ unfolding range_vars_alt_def by auto
  hence 0: "γ ∘s δ = δ ∘s γ"
    when δ: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
      and γ: "subst_domain γ = set X" "ground (subst_range γ)"
    for γ X
    by (metis δ γ subst_comp_eq_if_disjoint_vars)

  show "⟦M; D; S⟧s (δ ∘s θ) ⟹ ⟦M; D; S ⋅sst δ⟧s θ" using assms
  proof (induction S arbitrary: M D rule: strand_sem_stateful_induct)
    case (ConsSnd M D ts S)
    hence "∀t ∈ set ts. M ⊢ t ⋅ δ ⋅ θ" and IH: "⟦M; D; S ⋅sst δ⟧s θ" by auto
    hence "∀t ∈ set (ts ⋅list δ). M ⊢ t ⋅ θ" by simp
    thus ?case using IH by simp
  next
    case (ConsRcv M D ts S)
    hence "⟦(set ts ⋅set δ ∘s θ) ∪ M; D; S ⋅sst δ⟧s θ" by simp
    hence "⟦(set (ts ⋅list δ) ⋅set θ) ∪ M; D; S ⋅sst δ⟧s θ" by (metis list.set_map subst_comp_all) 
    thus ?case by simp
  next
    case (ConsNegChecks M D X F F' S)
    hence *: "⟦M; D; S ⋅sst δ⟧s θ" and **: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
      unfolding bvarssst_def negchecks_model_def by (force, auto)
    have "negchecks_model (δ ∘s θ) D X F F'" using ConsNegChecks by auto
    hence "negchecks_model θ D X (F ⋅pairs δ) (F' ⋅pairs δ)"
      using 0[OF **] negchecks_model_subst[OF **] by blast
    moreover have "rm_vars (set X) δ = δ" using ConsNegChecks.prems(2) by force
    ultimately show ?case using * by auto
  qed simp_all

  show "⟦M; D; S ⋅sst δ⟧s θ ⟹ ⟦M; D; S⟧s (δ ∘s θ)" using assms
  proof (induction S arbitrary: M D rule: strand_sem_stateful_induct)
    case (ConsSnd M D ts S)
    hence "∀t ∈ set (ts ⋅list δ). M ⊢ t ⋅ θ" and IH: "⟦M; D; S⟧s (δ ∘s θ)" by auto
    hence "∀t ∈ set ts. M ⊢ t ⋅ δ ⋅ θ" by simp
    thus ?case using IH by simp
  next
    case (ConsRcv M D ts S)
    hence "⟦(set (ts ⋅list δ) ⋅set θ) ∪ M; D; S⟧s (δ ∘s θ)" by simp
    hence "⟦(set ts ⋅set δ ∘s θ) ∪ M; D; S⟧s (δ ∘s θ)" by (metis list.set_map subst_comp_all) 
    thus ?case by simp
  next
    case (ConsNegChecks M D X F F' S)
    have δ: "rm_vars (set X) δ = δ" using ConsNegChecks.prems(2) by force
    hence *: "⟦M; D; S⟧s (δ ∘s θ)" and **: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
      using ConsNegChecks unfolding bvarssst_def negchecks_model_def by auto
    have "negchecks_model θ D X (F ⋅pairs δ) (F' ⋅pairs δ)"
      using ConsNegChecks.prems(1) δ by (auto simp add: subst_compose_assoc negchecks_model_def)
    hence "negchecks_model (δ ∘s θ) D X F F'"
      using 0[OF **] negchecks_model_subst[OF **] by blast
    thus ?case using * by auto
  qed simp_all
qed

lemma strand_sem_receive_prepend_stateful:
  assumes "⟦M; D; S⟧s θ"
    and "list_all is_Receive S'"
  shows "⟦M; D; S@S'⟧s θ"
using assms(2)
proof (induction S' rule: List.rev_induct)
  case (snoc x S')
  hence "∃t. x = receive⟨t⟩" "⟦M; D; S@S'⟧s θ"
    unfolding list_all_iff is_Receive_def by auto
  thus ?case using strand_sem_append_stateful[of M D "S@S'" "[x]" θ] by auto
qed (simp add: assms(1))

lemma negchecks_model_model_swap:
  fixes I J::"('a,'b) subst"
  assumes "∀x ∈ (fvpairs F ∪ fvpairs G) - set X. I x = J x"
    and "negchecks_model I D X F G"
  shows "negchecks_model J D X F G"
proof -
  have 0: "∀x ∈ (fvpairs F ∪ fvpairs G). (δ ∘s I) x = (δ ∘s J) x"
    when "subst_domain δ = set X" "ground (subst_range δ)"
    for δ::"('a,'b) subst"
    using that assms(1)
    by (metis DiffI ground_subst_range_empty_fv subst_comp_notin_dom_eq
              subst_ground_ident_compose(1))

  have 1: "s ⋅ (δ ∘s J) ≠ t ⋅ (δ ∘s J)"
    when "s ⋅ (δ ∘s I) ≠ t ⋅ (δ ∘s I)" "(s,t) ∈ set F"
         "subst_domain δ = set X" "ground (subst_range δ)"
    for δ::"('a,'b) subst" and s t
    using that(1,2) 0[OF that(3,4)] term_subst_eq_conv[of _ "δ ∘s I" "δ ∘s J"]
          UnCI fvpairs_inI(4,5)[OF that(2)]
    by metis

  have 2: "(s,t) ⋅p (δ ∘s J) ∉ D"
    when "(s,t) ⋅p (δ ∘s I) ∉ D" "(s,t) ∈ set G"
         "subst_domain δ = set X" "ground (subst_range δ)"
    for δ::"('a,'b) subst" and s t
    using that(1,2) 0[OF that(3,4)] fvpairs_inI(4,5)[of s t G]
          term_subst_eq_conv[of s "δ ∘s I" "δ ∘s J"]
          term_subst_eq_conv[of t "δ ∘s I" "δ ∘s J"]
    by simp

  have 3: "(∃(s,t) ∈ set F. s ⋅ δ ∘s J ≠ t ⋅ δ ∘s J) ∨ (∃(s,t) ∈ set G. (s, t) ⋅p δ ∘s J ∉ D)"
    when "subst_domain δ = set X" "ground (subst_range δ)"
         "(∃(s,t) ∈ set F. s ⋅ δ ∘s I ≠ t ⋅ δ ∘s I) ∨ (∃(s,t) ∈ set G. (s, t) ⋅p δ ∘s I ∉ D)"
    for δ::"('a,'b) subst"
    using 1[OF _ _ that(1,2)] 2[OF _ _ that(1,2)] that(3) by blast
  thus ?thesis
    using assms(2) unfolding negchecks_model_def by simp
qed

lemma strand_sem_model_swap:
  assumes "∀x ∈ fvsst S. I x = J x"
    and "⟦M; D; S⟧s I"
  shows "⟦M; D; S⟧s J"
using assms(2,1)
proof (induction S arbitrary: M D rule: strand_sem_stateful_induct)
  case (ConsSnd M D ts S)
  hence *: "⟦M; D; S⟧s J" "∀t ∈ set ts. M ⊢ t ⋅ I" "∀x ∈ fvset (set ts). I x = J x"
    by (fastforce, fastforce, fastforce)

  have "∀t ∈ set ts. M ⊢ t ⋅ J"
    using *(2,3) term_subst_eq_conv[of _ I J]
    by (metis fv_subset subsetD)
  thus ?case using *(1) by auto
next
  case (ConsRcv M D ts S)
  hence *: "⟦(set ts ⋅set I) ∪ M; D; S⟧s J" "∀x ∈ fvset (set ts). I x = J x"
    by (fastforce, fastforce)

  have "set ts ⋅set I = set ts ⋅set J"
    using *(2) term_subst_eq_conv[of _ I J]
    by (meson fv_subset image_cong subsetD)
  thus ?case using *(1) by simp
next
  case (ConsEq M D ac t t' S) thus ?case
    using term_subst_eq_conv[of t I J] term_subst_eq_conv[of t' I J] by force
next
  case (ConsIns M D t s S) thus ?case
    using term_subst_eq_conv[of t I J] term_subst_eq_conv[of s I J] by force
next
  case (ConsDel M D t s S) thus ?case
    using term_subst_eq_conv[of t I J] term_subst_eq_conv[of s I J] by force
next
  case (ConsIn M D uv t s S) thus ?case
    using term_subst_eq_conv[of t I J] term_subst_eq_conv[of s I J] by force
next
  case (ConsNegChecks M D X F F' S)
  hence "⟦M; D; S⟧s J" "negchecks_model I D X F F'" "∀x∈fvpairs F ∪ fvpairs F' - set X. I x = J x"
    by (fastforce, fastforce, fastforce)
  thus ?case using negchecks_model_model_swap[of F F' X I J D] by fastforce
qed simp

lemma strand_sem_receive_send_append:
  assumes A: "⟦M; D; A⟧s I"
  shows "⟦M; D; A@[receive⟨[t]⟩,send⟨[t]⟩]⟧s I"
proof -
  have "M ∪ (iksst (A@[receive⟨[t]⟩]) ⋅set I) ⊢ t ⋅ I"
    using in_iksst_iff[of t "A@[receive⟨[t]⟩]"] by auto
  thus ?thesis
    using A strand_sem_append_stateful[of M D A "[receive⟨[t]⟩]" I]
          strand_sem_append_stateful[of M D "A@[receive⟨[t]⟩]" "[send⟨[t]⟩]" I]
    by force
qed

lemma strand_sem_stateful_if_no_send_or_check:
  assumes A: "list_all (λa. ¬is_Send a ∧ ¬is_Check_or_Assignment a) A"
  shows "⟦M; D; A⟧s I"
using A
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  hence IH: "⟦M; D; A⟧s I" and a: "¬is_Send a" "¬is_Check_or_Assignment a" by auto
  from a have "⟦M; D; [a]⟧s I" for M D by (cases a) auto
  thus ?case using IH strand_sem_append_stateful[of M D A "[a]" I] by blast
qed simp

lemma strand_sem_stateful_if_sends_deduct:
  assumes "list_all is_Send A"
    and "∀ts. send⟨ts⟩ ∈ set A ⟶ (∀t ∈ set ts. M ⊢ t ⋅ I)"
  shows "⟦M; D; A⟧s I"
using assms
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  hence IH: "⟦M; D; A⟧s I" by auto
  obtain ts where a: "a = send⟨ts⟩" "∀t ∈ set ts. M ⊢ t ⋅ I" using snoc.prems by (cases a) auto

  have "⟦M ∪ (iksst A ⋅set I); D; [a]⟧s I" for D
    using ideduct_mono[of M _ "M ∪ (iksst A ⋅set I)"] a by auto
  thus ?case using IH strand_sem_append_stateful[of M D A "[a]" I] by blast
qed simp

lemma strand_sem_stateful_if_checks:
  assumes "list_all is_Check_or_Assignment A"
    and "∀ac t s. ⟨ac: t ≐ s⟩ ∈ set A ⟶ t ⋅ I = s ⋅ I"
    and "∀ac t s. ⟨ac: t ∈ s⟩ ∈ set A ⟶ (t ⋅ I, s ⋅ I) ∈ D"
    and "∀X F G. ∀X⟨∨≠: F ∨∉: G⟩ ∈ set A ⟶ negchecks_model I D X F G"
  shows "⟦M; D; A⟧s I"
using assms
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  hence IH: "⟦M; D; A⟧s I" and a: "is_Check_or_Assignment a" by auto

  have 0: "dbupdsst A I D = D"
    using snoc.prems(1) dbupdsst_no_upd[of A I D] unfolding list_all_iff by auto

  have "⟦M; D; [a]⟧s I" for M using a snoc.prems(2,3,4) by (cases a) auto
  thus ?case using IH strand_sem_append_stateful[of M D A "[a]" I] unfolding 0 by blast
qed simp

lemma strand_sem_stateful_sends_deduct:
  assumes A: "⟦M; D; A⟧s I"
    and ts: "send⟨ts⟩ ∈ set A"
    and t: "t ∈ set ts"
  shows "M ∪ (iksst A ⋅set I) ⊢ t ⋅ I"
using A ts
proof (induction A arbitrary: M D rule: List.rev_induct)
  case (snoc a A)
  have 0: "⟦M; D; A⟧s I"
    using strand_sem_append_stateful snoc.prems(1) by fast

  have 1: "M ∪ (iksst A ⋅set I) ⊆ M ∪ (iksst (A@[a]) ⋅set I)"
    by auto

  have 2: "M ∪ (iksst (A@[send⟨ts⟩]) ⋅set I) = M ∪ (iksst A ⋅set I)"
    using in_iksst_iff[of _ A] in_iksst_iff[of _ "A@[send⟨ts⟩]"] by fastforce

  show ?case
  proof (cases "send⟨ts⟩ ∈ set A")
    case True show ?thesis by (rule ideduct_mono[OF snoc.IH[OF 0 True] 1])
  next
    case False
    hence a: "a = send⟨ts⟩" using snoc.prems(2) by force
    show ?thesis
      using strand_sem_append_stateful[of M D A "[a]" I] snoc.prems(1) t
      unfolding a 2 by auto
  qed
qed simp

end


subsection ‹Well-Formedness Lemmata›
lemma wfvarsoccsst_subset_wfrestrictedvarssst[simp]:
  "wfvarsoccssst S ⊆ wfrestrictedvarssst S"
by (induction S)
   (auto simp add: wfrestrictedvarssst_def wfvarsoccssst_def
         split: stateful_strand_step.split poscheckvariant.split)

lemma wfvarsoccssst_append: "wfvarsoccssst (S@S') = wfvarsoccssst S ∪ wfvarsoccssst S'"
by (simp add: wfvarsoccssst_def)

lemma wfrestrictedvarssst_union[simp]:
  "wfrestrictedvarssst (S@T) = wfrestrictedvarssst S ∪ wfrestrictedvarssst T"
by (simp add: wfrestrictedvarssst_def)

lemma wfrestrictedvarssst_singleton:
  "wfrestrictedvarssst [s] = wfrestrictedvarssstp s"
by (simp add: wfrestrictedvarssst_def)

lemma iksst_fv_subset_wfrestrictedvarssst[simp]:
  "fvset (iksst S) ⊆ wfrestrictedvarssst S"
using in_iksst_iff[of _ S] unfolding wfrestrictedvarssst_def by force

lemma wfsst_prefix[dest]: "wf'sst V (S@S') ⟹ wf'sst V S"
by (induct S rule: wf'sst.induct) auto

lemma wfsst_vars_mono: "wf'sst V S ⟹ wf'sst (V ∪ W) S"
proof (induction S arbitrary: V)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Send ts)
    have "wf'sst (V ∪ W ∪ fvset (set ts)) S"
      using Cons.prems(1) Cons.IH Send by (metis sup_assoc sup_commute wf'sst.simps(3))
    thus ?thesis by (simp add: Send)
  next
    case (Equality a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst (V ∪ fv t ∪ W) S" "fv t' ⊆ V ∪ W" using Equality Cons.prems(1) Cons.IH by auto
      thus ?thesis using Equality Assign by (simp add: sup_commute sup_left_commute)
    next
      case Check thus ?thesis using Equality Cons by auto
    qed
  next
    case (InSet a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst (V ∪ fv t ∪ fv t' ∪ W) S" using InSet Cons.prems(1) Cons.IH by auto
      thus ?thesis using InSet Assign by (simp add: sup_commute sup_left_commute)
    next
      case Check thus ?thesis using InSet Cons by auto
    qed
  qed auto
qed simp

lemma wfsstI[intro]: "wfrestrictedvarssst S ⊆ V ⟹ wf'sst V S"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Send ts)
    hence "wf'sst V S" "V ∪ fvset (set ts) = V"
      using Cons
      unfolding wfrestrictedvarssst_def
      by auto
    thus ?thesis using Send by simp
  next
    case (Equality a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst V S" "fv t' ⊆ V"
        using Equality Cons 
        unfolding wfrestrictedvarssst_def
        by auto
      thus ?thesis using wfsst_vars_mono Equality Assign by simp
    next
      case Check
      thus ?thesis
        using Equality Cons
        unfolding wfrestrictedvarssst_def
        by auto
    qed
  next
    case (InSet a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst V S" "fv t ∪ fv t' ⊆ V"
        using InSet Cons
        unfolding wfrestrictedvarssst_def
        by auto
      thus ?thesis using wfsst_vars_mono InSet Assign by (simp add: Un_assoc) 
    next
      case Check
      thus ?thesis
        using InSet Cons
        unfolding wfrestrictedvarssst_def
        by auto
    qed
  qed (simp_all add: wfrestrictedvarssst_def)
qed (simp add: wfrestrictedvarssst_def)

lemma wfsstI'[intro]:
  assumes "⋃((λx. case x of
            Receive ts ⇒ fvset (set ts)
          | Equality Assign _ t' ⇒ fv t'
          | Insert t t' ⇒ fv t ∪ fv t'
          | _ ⇒ {}) ` set S) ⊆ V"
  shows "wf'sst V S"
using assms
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Equality a t t')
    thus ?thesis using Cons by (cases a) (auto simp add: wfsst_vars_mono)
  next
    case (InSet a t t')
    thus ?thesis using Cons by (cases a) (auto simp add: wfsst_vars_mono Un_assoc)
  qed (simp_all add: wfsst_vars_mono)
qed simp

lemma wfsst_append_exec: "wf'sst V (S@S') ⟹ wf'sst (V ∪ wfvarsoccssst S) S'"
proof (induction S arbitrary: V)
  case (Cons x S V) thus ?case
  proof (cases x)
    case (Send ts)
    hence "wf'sst (V ∪ fvset (set ts) ∪ wfvarsoccssst S) S'" using Cons.prems Cons.IH by simp
    thus ?thesis using Send unfolding wfvarsoccssst_def by (auto simp add: sup_assoc)
  next
    case (Equality a t t') show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst (V ∪ fv t ∪ wfvarsoccssst S) S'" using Equality Cons.prems Cons.IH by auto
      thus ?thesis using Equality Assign unfolding wfvarsoccssst_def by (auto simp add: sup_assoc)
    next
      case Check
      hence "wf'sst (V ∪ wfvarsoccssst S) S'" using Equality Cons.prems Cons.IH by auto
      thus ?thesis using Equality Check unfolding wfvarsoccssst_def by (auto simp add: sup_assoc)
    qed
  next
    case (InSet a t t') show ?thesis
    proof (cases a)
      case Assign
      hence "wf'sst (V ∪ fv t ∪ fv t' ∪ wfvarsoccssst S) S'" using InSet Cons.prems Cons.IH by auto
      thus ?thesis using InSet Assign unfolding wfvarsoccssst_def by (auto simp add: sup_assoc)
    next
      case Check
      hence "wf'sst (V ∪ wfvarsoccssst S) S'" using InSet Cons.prems Cons.IH by auto
      thus ?thesis using InSet Check unfolding wfvarsoccssst_def by (auto simp add: sup_assoc)
    qed
  qed (auto simp add: wfvarsoccssst_def)
qed (simp add: wfvarsoccssst_def)

lemma wfsst_append:
  "wf'sst X S ⟹ wf'sst Y T ⟹ wf'sst (X ∪ Y) (S@T)"
proof (induction X S rule: wf'sst.induct)
  case 1 thus ?case by (metis wfsst_vars_mono Un_commute append_Nil)
next
  case 3 thus ?case by (metis append_Cons Un_commute Un_assoc wf'sst.simps(3))
next
  case (4 V t t' S)
  hence *: "fv t' ⊆ V" and "wf'sst (V ∪ fv t ∪ Y) (S @ T)" by simp_all
  hence "wf'sst (V ∪ Y ∪ fv t) (S @ T)" by (metis Un_commute Un_assoc)
  thus ?case using * by auto
next
  case (8 V t t' S)
  hence "wf'sst (V ∪ fv t ∪ fv t' ∪ Y) (S @ T)" by simp_all
  hence "wf'sst (V ∪ Y ∪ fv t ∪ fv t') (S @ T)" by (metis Un_commute Un_assoc)
  thus ?case by auto
qed auto

lemma wfsst_append_suffix:
  "wf'sst V S ⟹ wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ V ⟹ wf'sst V (S@S')"
proof (induction V S rule: wf'sst.induct)
  case (2 V ts S)
  hence *: "fvset (set ts) ⊆ V" "wf'sst V S" by simp_all
  hence "wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ V"
    using "2.prems"(2) unfolding wfrestrictedvarssst_def by fastforce
  thus ?case using "2.IH" * by simp
next
  case (3 V ts S)
  hence *: "wf'sst (V ∪ fvset (set ts)) S" by simp_all
  hence "wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ (V ∪ fvset (set ts))"
    using "3.prems"(2) unfolding wfrestrictedvarssst_def by auto
  thus ?case using "3.IH" * by simp
next
  case (4 V t t' S)
  hence *: "fv t' ⊆ V" "wf'sst (V ∪ fv t) S" by simp_all
  moreover have "varssstp (⟨t := t'⟩) = fv t ∪ fv t'"
    by simp
  moreover have "wfrestrictedvarssst (⟨t := t'⟩#S) = fv t ∪ fv t' ∪ wfrestrictedvarssst S"
    unfolding wfrestrictedvarssst_def by auto
  ultimately have "wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ (V ∪ fv t)"
    using "4.prems"(2) by blast
  thus ?case using "4.IH" * by simp
next
  case (6 V t t' S)
  hence *: "fv t ∪ fv t' ⊆ V" "wf'sst V S" by simp_all
  moreover have "varssstp (insert⟨t,t'⟩) = fv t ∪ fv t'"
    by simp
  moreover have "wfrestrictedvarssst (insert⟨t,t'⟩#S) = fv t ∪ fv t' ∪ wfrestrictedvarssst S"
    unfolding wfrestrictedvarssst_def by auto
  ultimately have "wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ V"
    using "6.prems"(2) by blast
  thus ?case using "6.IH" * by simp
next
  case (8 V t t' S)
  hence *: "wf'sst (V ∪ fv t ∪ fv t') S" by simp_all
  moreover have "varssstp (select⟨t,t'⟩) = fv t ∪ fv t'"
    by simp
  moreover have "wfrestrictedvarssst (select⟨t,t'⟩#S) = fv t ∪ fv t' ∪ wfrestrictedvarssst S"
    unfolding wfrestrictedvarssst_def by auto
  ultimately have "wfrestrictedvarssst S' ⊆ wfrestrictedvarssst S ∪ (V ∪ fv t ∪ fv t')"
    using "8.prems"(2) by blast
  thus ?case using "8.IH" * by simp
qed (simp_all add: wfsstI wfrestrictedvarssst_def)

lemma wfsst_append_suffix':
  assumes "wf'sst V S"
    and "⋃((λx. case x of
            Receive ts ⇒ fvset (set ts)
          | Equality Assign _ t' ⇒ fv t'
          | Insert t t' ⇒ fv t ∪ fv t'
          | _ ⇒ {}) ` set S') ⊆ wfvarsoccssst S ∪ V"
  shows "wf'sst V (S@S')"
using assms
by (induction V S rule: wf'sst.induct)
   (auto simp add: wfsstI' wfsst_vars_mono wfvarsoccssst_def)

lemma wfsst_subst_apply:
  "wf'sst V S ⟹ wf'sst (fvset (δ ` V)) (S ⋅sst δ)"
proof (induction S arbitrary: V rule: wf'sst.induct)
  case (2 V ts S)
  hence "wf'sst V S" "fvset (set ts) ⊆ V" by simp_all
  hence "wf'sst (fvset (δ ` V)) (S ⋅sst δ)" "fvset (set ts ⋅set δ) ⊆ fvset (δ ` V)"
    using "2.IH" subst_apply_fv_subset by (simp, force)
  thus ?case by (simp add: subst_apply_stateful_strand_def)
next
  case (3 V ts S)
  hence "wf'sst (V ∪ fvset (set ts)) S" by simp
  hence "wf'sst (fvset (δ ` (V ∪ fvset (set ts)))) (S ⋅sst δ)" using "3.IH" by metis
  hence "wf'sst (fvset (δ ` V) ∪ fvset (set ts ⋅set δ)) (S ⋅sst δ)"
    using  subst_apply_fv_unfold_set[of δ ts] by fastforce
  thus ?case by (simp add: subst_apply_stateful_strand_def)
next
  case (4 V t t' S)
  hence "wf'sst (V ∪ fv t) S" "fv t' ⊆ V" by auto
  hence "wf'sst (fvset (δ ` (V ∪ fv t))) (S ⋅sst δ)" and *: "fv (t' ⋅ δ) ⊆ fvset (δ ` V)"
    using "4.IH" subst_apply_fv_subset by force+
  hence "wf'sst (fvset (δ ` V) ∪ fv (t ⋅ δ)) (S ⋅sst δ)" by (metis subst_apply_fv_union)
  thus ?case using * by (simp add: subst_apply_stateful_strand_def)
next
  case (6 V t t' S)
  hence "wf'sst V S" "fv t ∪ fv t' ⊆ V" by auto
  hence "wf'sst (fvset (δ ` V)) (S ⋅sst δ)" "fv (t ⋅ δ) ⊆ fvset (δ ` V)" "fv (t' ⋅ δ) ⊆ fvset (δ ` V)"
    using "6.IH" subst_apply_fv_subset by force+
  thus ?case by (simp add: sup_assoc subst_apply_stateful_strand_def)
next
  case (8 V t t' S)
  hence "wf'sst (V ∪ fv t ∪ fv t') S" by auto
  hence "wf'sst (fvset (δ ` (V ∪ fv t ∪ fv t'))) (S ⋅sst δ)"
    using "8.IH" subst_apply_fv_subset by force
  hence "wf'sst (fvset (δ ` V) ∪ fv (t ⋅ δ) ∪ fv (t' ⋅ δ)) (S ⋅sst δ)" by (metis subst_apply_fv_union)
  thus ?case by (simp add: subst_apply_stateful_strand_def)
qed (auto simp add: subst_apply_stateful_strand_def)

lemma wfsst_induct[consumes 1,
                  case_names Nil ConsSnd ConsRcv ConsEq ConsEq2 ConsIn ConsIns ConsDel
                             ConsNegChecks]:
  fixes S::"('a,'b) stateful_strand"
  assumes "wf'sst V S"
          "P []"
          "⋀ts S. ⟦wf'sst V S; P S⟧ ⟹ P (S@[Send ts])"
          "⋀ts S. ⟦wf'sst V S; P S; fvset (set ts) ⊆ V ∪ wfvarsoccssst S⟧ ⟹ P (S@[Receive ts])"
          "⋀t t' S. ⟦wf'sst V S; P S; fv t' ⊆ V ∪ wfvarsoccssst S⟧ ⟹ P (S@[Equality Assign t t'])"
          "⋀t t' S. ⟦wf'sst V S; P S⟧ ⟹ P (S@[Equality Check t t'])"
          "⋀ac t t' S. ⟦wf'sst V S; P S⟧ ⟹ P (S@[InSet ac t t'])"
          "⋀t t' S. ⟦wf'sst V S; P S; fv t ∪ fv t' ⊆ V ∪ wfvarsoccssst S⟧ ⟹ P (S@[Insert t t'])"
          "⋀t t' S. ⟦wf'sst V S; P S⟧ ⟹ P (S@[Delete t t'])"
          "⋀X F G S. ⟦wf'sst V S; P S⟧ ⟹ P (S@[NegChecks X F G])"
  shows "P S"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S)
  hence *: "wf'sst V S" "wf'sst (V ∪ wfvarsoccssst S) [x]"
    by (metis wfsst_prefix, metis wfsst_append_exec)
  have IH: "P S" using snoc.IH[OF *(1)] snoc.prems by auto
  note ** = snoc.prems(3-)[OF *(1) IH] *(2)
  show ?case
  proof (cases x)
    case (Send ts) thus ?thesis using **(1) by blast
  next
    case (Receive ts) thus ?thesis using **(2,9) by simp
  next
    case (Equality ac t t') thus ?thesis using **(3,4,9) by (cases ac) auto
  next
    case (Insert t t') thus ?thesis using **(6,9) by force
  next
    case (Delete t t') thus ?thesis using **(7) by presburger
  next
    case (NegChecks X F G) thus ?thesis using **(8) by presburger
  next
    case (InSet ac t t') thus ?thesis using **(5) by (cases ac) auto
  qed
qed simp

lemma wfsst_strand_first_Send_var_split:
  assumes "wf'sst {} S" "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v"
  shows "∃Spre Ssuf. ¬(∃w ∈ wfrestrictedvarssst Spre. t ⋅ ℐ ⊑ ℐ w) ∧ (
                    (∃ts. S = Spre@send⟨ts⟩#Ssuf ∧ t ⋅ ℐ ⊑set set ts ⋅set ℐ) ∨
                    (∃s u. S = Spre@⟨assign: s ≐ u⟩#Ssuf ∧ t ⋅ ℐ ⊑ s ⋅ ℐ ∧ ¬(t ⋅ ℐ ⊑set ℐ ` fv u)) ∨
                    (∃s u. S = Spre@⟨assign: s ∈ u⟩#Ssuf ∧ (t ⋅ ℐ ⊑ s ⋅ ℐ ∨ t ⋅ ℐ ⊑ u ⋅ ℐ)))"
    (is "∃Spre Ssuf. ?P Spre ∧ ?Q S Spre Ssuf")
using assms
proof (induction S rule: wfsst_induct)
  case (ConsSnd ts' S) show ?case
  proof (cases "∃w ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ w")
    case True
    then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
      using ConsSnd.IH by moura
    thus ?thesis by fastforce
  next
    case False
    then obtain v where v: "v ∈ fvset (set ts')" "t ⋅ ℐ ⊑ ℐ v"
      using ConsSnd.prems unfolding wfrestrictedvarssst_def by auto
    then obtain t' where t': "t' ∈ set ts'" "v ∈ fv t'" by auto
    have "t ⋅ ℐ ⊑ t' ⋅ ℐ"
      using v(2) t'(2) subst_mono[of "Var v" t' ℐ] vars_iff_subtermeq[of v] term.order_trans
      by auto
    hence "t ⋅ ℐ ⊑set set ts' ⋅set ℐ" using v(1) t'(1) by blast
    thus ?thesis using False v by blast
  qed
next
  case (ConsRcv t' S)
  have "fvset (set t') ⊆ wfrestrictedvarssst S"
    using ConsRcv.hyps wfvarsoccsst_subset_wfrestrictedvarssst[of S] by blast
  hence "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v"
    using ConsRcv.prems unfolding wfrestrictedvarssst_def by fastforce
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
    using ConsRcv.IH by moura
  thus ?case by fastforce
next
  case (ConsEq s s' S)
  have *: "fv s' ⊆ wfrestrictedvarssst S"
    using ConsEq.hyps wfvarsoccsst_subset_wfrestrictedvarssst[of S] by blast
  show ?case
  proof (cases "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v")
    case True
    then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
      using ConsEq.IH by moura
    thus ?thesis by fastforce
  next
    case False
    then obtain v where "v ∈ fv s" "t ⋅ ℐ ⊑ ℐ v" and **: "fv s' ⊆ wfrestrictedvarssst S"
      using ConsEq.prems * unfolding wfrestrictedvarssst_def by auto
    hence "t ⋅ ℐ ⊑ s ⋅ ℐ"
      using vars_iff_subtermeq[of v s] subst_mono[of "Var v" s ℐ] term.order_trans by auto
    thus ?thesis using False ** by fastforce
  qed
next
  case (ConsEq2 s s' S)
  have "wfrestrictedvarssst (S@[Equality Check s s']) = wfrestrictedvarssst S"
    unfolding wfrestrictedvarssst_def by auto
  hence "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v" using ConsEq2.prems by metis
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf" using ConsEq2.IH by moura
  thus ?case by fastforce
next
  case (ConsNegChecks X F G S)
  hence "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v" unfolding wfrestrictedvarssst_def by simp
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf" using ConsNegChecks.IH by moura
  thus ?case by fastforce
next
  case (ConsIn ac s s' S)
  show ?case
  proof (cases "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v")
    case True
    then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
      using ConsIn.IH by moura
    thus ?thesis by fastforce
  next
    case False
    hence ac: "ac = assign" using ConsIn.prems unfolding wfrestrictedvarssst_def by (cases ac) auto
    obtain v where "v ∈ fv s ∪ fv s'" "t ⋅ ℐ ⊑ ℐ v"
        using ConsIn.prems False unfolding wfrestrictedvarssst_def ac by auto
    hence *: "t ⋅ ℐ ⊑ s ⋅ ℐ ∨ t ⋅ ℐ ⊑ s' ⋅ ℐ"
      using vars_iff_subtermeq[of v s] vars_iff_subtermeq[of v s']
            subst_mono[of "Var v" s ℐ] subst_mono[of "Var v" s' ℐ] term.order_trans
      by auto
    show ?thesis using * False unfolding ac by fast
  qed
next
  case (ConsIns s s' S)
  have "fv s ∪ fv s' ⊆ wfrestrictedvarssst S"
    using ConsIns.hyps wfvarsoccsst_subset_wfrestrictedvarssst[of S] by blast
  hence "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v"
      using ConsIns.prems unfolding wfrestrictedvarssst_def by fastforce
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf" using ConsIns.IH by moura
  thus ?case by fastforce
next
  case (ConsDel s s' S)
  hence "∃v ∈ wfrestrictedvarssst S. t ⋅ ℐ ⊑ ℐ v" unfolding wfrestrictedvarssst_def by simp
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf" using ConsDel.IH by moura
  thus ?case by fastforce
qed (simp add: wfrestrictedvarssst_def)

lemma wfsst_vars_mono': "wf'sst V S ⟹ V ⊆ W ⟹ wf'sst W S"
by (metis Diff_partition wfsst_vars_mono)

lemma wfrestrictedvarssst_receives_only_eq:
  assumes "list_all is_Receive S"
  shows "wfrestrictedvarssst S = fvsst S"
using assms
proof (induction S)
  case (Cons a A)
  obtain ts where a: "a = receive⟨ts⟩" using Cons.prems by (cases a) auto
  have IH: "wfrestrictedvarssst A = fvsst A" using Cons.prems Cons.IH by simp
  show ?case using IH unfolding a wfrestrictedvarssst_def by simp
qed (simp add: wfrestrictedvarssst_def)

lemma wfvarsoccssst_receives_only_empty:
  assumes "list_all is_Receive S"
  shows "wfvarsoccssst S = {}"
using assms
proof (induction S)
  case (Cons a A)
  obtain ts where a: "a = receive⟨ts⟩" using Cons.prems by (cases a) auto
  have IH: "wfvarsoccssst A = {}" using Cons.prems Cons.IH by simp
  show ?case using IH unfolding a wfvarsoccssst_def by simp
qed (simp add: wfvarsoccssst_def)

lemma wfsst_sends_only:
  assumes "list_all is_Send S"
  shows "wf'sst V S"
using assms
proof (induction S arbitrary: V)
  case (Cons s S) thus ?case by (cases s) auto
qed simp

lemma wfsst_sends_only_prepend:
  assumes "wf'sst V S"
    and "list_all is_Send S'"
  shows "wf'sst V (S'@S)"
using wfsst_append[OF wfsst_sends_only[OF assms(2), of "{}"] assms(1)] by simp

lemma wfsst_receives_only_fv_subset:
  assumes "wf'sst V S"
    and "list_all is_Receive S"
  shows "fvsst S ⊆ V"
using assms
proof (induction rule: wfsst_induct)
  case (ConsRcv ts S) thus ?case using wfvarsoccssst_receives_only_empty[of S] by auto
qed auto

lemma wfsst_append_suffix'':
  assumes "wf'sst V S"
    and "wfrestrictedvarssst S' ⊆ wfvarsoccssst S ∪ V"
  shows "wf'sst V (S@S')"
using assms
by (induction V S rule: wf'sst.induct)
   (auto simp add: wfsstI' wfsst_vars_mono wfvarsoccssst_def)


end