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_eq:
  assumes "∄s. a = receive⟨s⟩"
  shows "iksst (A@[a]) ⋅set ℐ = iksst A ⋅set ℐ"
using assms unfolding iksst_def
by (metis (no_types, lifting) Un_iff append_Nil2 set_ConsD set_append)

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 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 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 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 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 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 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⟩ ∈