Theory Transactions

(*  Title:      Transactions.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section‹Protocol Transactions›
theory Transactions
  imports
    Stateful_Protocol_Composition_and_Typing.Typed_Model
    Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands 
begin

subsection ‹Definitions›
datatype 'b prot_atom =
  is_Atom: Atom 'b
| Value
| SetType
| AttackType
| Bottom
| OccursSecType
| AbsValue

datatype ('a,'b,'c,'d) prot_fun =
  Fu (the_Fu: 'a)
| Set (the_Set: 'c)
| Val (the_Val: "nat")
| Abs (the_Abs: "'c set")
| Attack (the_Attack_label: "'d strand_label")
| Pair
| PubConst (the_PubConst_type: "'b prot_atom") nat
| OccursFact
| OccursSec

definition "is_Fun_Set t ≡ is_Fun t ∧ args t = [] ∧ is_Set (the_Fun t)"

definition "is_Fun_Attack t ≡ is_Fun t ∧ args t = [] ∧ is_Attack (the_Fun t)"

definition "is_PubConstValue f ≡ is_PubConst f ∧ the_PubConst_type f = Value"

abbreviation occurs where
  "occurs t ≡ Fun OccursFact [Fun OccursSec [], t]"

type_synonym ('a,'b,'c,'d) prot_term_type = "(('a,'b,'c,'d) prot_fun,'b prot_atom) term_type"

type_synonym ('a,'b,'c,'d) prot_var = "('a,'b,'c,'d) prot_term_type × nat"

type_synonym ('a,'b,'c,'d) prot_term = "(('a,'b,'c,'d) prot_fun,('a,'b,'c,'d) prot_var) term"
type_synonym ('a,'b,'c,'d) prot_terms = "('a,'b,'c,'d) prot_term set"

type_synonym ('a,'b,'c,'d) prot_subst = "(('a,'b,'c,'d) prot_fun, ('a,'b,'c,'d) prot_var) subst"

type_synonym ('a,'b,'c,'d) prot_strand_step =
  "(('a,'b,'c,'d) prot_fun, ('a,'b,'c,'d) prot_var, 'd) labeled_stateful_strand_step"
type_synonym ('a,'b,'c,'d) prot_strand = "('a,'b,'c,'d) prot_strand_step list"
type_synonym ('a,'b,'c,'d) prot_constr = "('a,'b,'c,'d) prot_strand_step list"

(* TODO: rename transaction_decl *)
datatype ('a,'b,'c,'d) prot_transaction =
  Transaction
    (transaction_decl:    "unit ⇒ (('a,'b,'c,'d) prot_var × 'a set) list")
    (transaction_fresh:   "('a,'b,'c,'d) prot_var list")
    (transaction_receive: "('a,'b,'c,'d) prot_strand")
    (transaction_checks:  "('a,'b,'c,'d) prot_strand")
    (transaction_updates: "('a,'b,'c,'d) prot_strand")
    (transaction_send:    "('a,'b,'c,'d) prot_strand")

definition transaction_strand where
  "transaction_strand T ≡
    transaction_receive T@transaction_checks T@
    transaction_updates T@transaction_send T"

fun transaction_proj where
  "transaction_proj l (Transaction A B C D E F) = (
  let f = proj l
  in Transaction A B (f C) (f D) (f E) (f F))"

fun transaction_star_proj where
  "transaction_star_proj (Transaction A B C D E F) = (
  let f = filter has_LabelS
  in Transaction A B (f C) (f D) (f E) (f F))"

abbreviation fv_transaction where
  "fv_transaction T ≡ fvlsst (transaction_strand T)"

abbreviation bvars_transaction where
  "bvars_transaction T ≡ bvarslsst (transaction_strand T)"

abbreviation vars_transaction where
  "vars_transaction T ≡ varslsst (transaction_strand T)"

abbreviation trms_transaction where
  "trms_transaction T ≡ trmslsst (transaction_strand T)"

abbreviation setops_transaction where
  "setops_transaction T ≡ setopssst (unlabel (transaction_strand T))"

definition wellformed_transaction where
  "wellformed_transaction T ≡
    list_all is_Receive (unlabel (transaction_receive T)) ∧
    list_all is_Check_or_Assignment (unlabel (transaction_checks T)) ∧
    list_all is_Update (unlabel (transaction_updates T)) ∧
    list_all is_Send (unlabel (transaction_send T)) ∧
    distinct (map fst (transaction_decl T ())) ∧
    distinct (transaction_fresh T) ∧
    set (transaction_fresh T) ∩ fst ` set (transaction_decl T ()) = {} ∧
    set (transaction_fresh T) ∩ fvlsst (transaction_receive T) = {} ∧
    set (transaction_fresh T) ∩ fvlsst (transaction_checks T) = {} ∧
    set (transaction_fresh T) ∩ bvars_transaction T = {} ∧
    fv_transaction T ∩ bvars_transaction T = {} ∧
    wf'sst (fst ` set (transaction_decl T ()) ∪ set (transaction_fresh T))
          (unlabel (duallsst (transaction_strand T)))"

type_synonym ('a,'b,'c,'d) prot = "('a,'b,'c,'d) prot_transaction list"

abbreviation Var_Value_term (‹⟨_: value⟩v›) where
  "⟨n: value⟩v ≡ Var (Var Value, n)::('a,'b,'c,'d) prot_term"

abbreviation Var_SetType_term (‹⟨_: SetType⟩v›) where
  "⟨n: SetType⟩v ≡ Var (Var SetType, n)::('a,'b,'c,'d) prot_term"

abbreviation Var_AttackType_term (‹⟨_: AttackType⟩v›) where
  "⟨n: AttackType⟩v ≡ Var (Var AttackType, n)::('a,'b,'c,'d) prot_term"

abbreviation Var_Atom_term (‹⟨_: _⟩v›) where
  "⟨n: a⟩v ≡ Var (Var (Atom a), n)::('a,'b,'c,'d) prot_term"

abbreviation Var_Comp_Fu_term (‹⟨_: _⟨_⟩⟩v›) where
  "⟨n: f⟨T⟩⟩v ≡ Var (Fun (Fu f) T, n)::('a,'b,'c,'d) prot_term"

abbreviation TAtom_Atom_term (‹⟨_⟩τa›) where
  "⟨a⟩τa ≡ Var (Atom a)::('a,'b,'c,'d) prot_term_type"

abbreviation TComp_Fu_term (‹⟨_ _⟩τ›) where
  "⟨f T⟩τ ≡ Fun (Fu f) T::('a,'b,'c,'d) prot_term_type"

abbreviation Fun_Fu_term (‹⟨_ _⟩t›) where
  "⟨f T⟩t ≡ Fun (Fu f) T::('a,'b,'c,'d) prot_term"

abbreviation Fun_Fu_const_term (‹⟨_⟩c›) where
  "⟨c⟩c ≡ Fun (Fu c) []::('a,'b,'c,'d) prot_term"

abbreviation Fun_Set_const_term (‹⟨_⟩s›) where
  "⟨f⟩s ≡ Fun (Set f) []::('a,'b,'c,'d) prot_term"

abbreviation Fun_Set_composed_term (‹⟨_⟨_⟩⟩s›) where
  "⟨f⟨T⟩⟩s ≡ Fun (Set f) T::('a,'b,'c,'d) prot_term"

abbreviation Fun_Abs_const_term (‹⟨_⟩abs›) where
  "⟨a⟩abs ≡ Fun (Abs a) []::('a,'b,'c,'d) prot_term"

abbreviation Fun_Attack_const_term (‹attack⟨_⟩›) where
  "attack⟨n⟩ ≡ Fun (Attack n) []::('a,'b,'c,'d) prot_term"

abbreviation prot_transaction1 (‹transaction1 _ _ new _ _ _›) where
  "transaction1 (S1::('a,'b,'c,'d) prot_strand) S2 new (B::('a,'b,'c,'d) prot_term list) S3 S4
  ≡ Transaction (λ(). []) (map the_Var B) S1 S2 S3 S4"

abbreviation prot_transaction2 (‹transaction2 _ _  _ _›) where
  "transaction2 (S1::('a,'b,'c,'d) prot_strand) S2 S3 S4
  ≡ Transaction (λ(). []) [] S1 S2 S3 S4"


subsection ‹Lemmata›

lemma prot_atom_UNIV:
  "(UNIV::'b prot_atom set) = range Atom ∪ {Value, SetType, AttackType, Bottom, OccursSecType, AbsValue}"
proof -
  have "a ∈ range Atom ∨ a = Value ∨ a = SetType ∨ a = AttackType ∨
        a = Bottom ∨ a = OccursSecType ∨ a = AbsValue"
    for a::"'b prot_atom"
    by (cases a) auto
  thus ?thesis by auto
qed

instance prot_atom::(finite) finite
by intro_classes (simp add: prot_atom_UNIV)

instantiation prot_atom::(enum) enum
begin
definition "enum_prot_atom == map Atom enum_class.enum@[Value, SetType, AttackType, Bottom, OccursSecType, AbsValue]"
definition "enum_all_prot_atom P == list_all P (map Atom enum_class.enum@[Value, SetType, AttackType, Bottom, OccursSecType, AbsValue])"
definition "enum_ex_prot_atom P == list_ex P (map Atom enum_class.enum@[Value, SetType, AttackType, Bottom, OccursSecType, AbsValue])"

instance
proof intro_classes
  have *: "set (map Atom (enum_class.enum::'a list)) = range Atom"
          "distinct (enum_class.enum::'a list)"
    using UNIV_enum enum_distinct by auto

  show "(UNIV::'a prot_atom set) = set enum_class.enum"
    using *(1) by (simp add: prot_atom_UNIV enum_prot_atom_def)

  have "set (map Atom enum_class.enum) ∩ set [Value, SetType, AttackType, Bottom, OccursSecType, AbsValue] = {}" by auto
  moreover have "inj_on Atom (set (enum_class.enum::'a list))" unfolding inj_on_def by auto
  hence "distinct (map Atom (enum_class.enum::'a list))" by (metis *(2) distinct_map)
  ultimately show "distinct (enum_class.enum::'a prot_atom list)" by (simp add: enum_prot_atom_def)

  have "Ball UNIV P ⟷ Ball (range Atom) P ∧ Ball {Value, SetType, AttackType, Bottom, OccursSecType, AbsValue} P"
    for P::"'a prot_atom ⇒ bool"
    by (metis prot_atom_UNIV UNIV_I UnE) 
  thus "enum_class.enum_all P = Ball (UNIV::'a prot_atom set) P" for P
    using *(1) Ball_set[of "map Atom enum_class.enum" P]
    by (auto simp add: enum_all_prot_atom_def)

  have "Bex UNIV P ⟷ Bex (range Atom) P ∨ Bex {Value, SetType, AttackType, Bottom, OccursSecType, AbsValue} P"
    for P::"'a prot_atom ⇒ bool"
    by (metis prot_atom_UNIV UNIV_I UnE) 
  thus "enum_class.enum_ex P = Bex (UNIV::'a prot_atom set) P" for P
    using *(1) Bex_set[of "map Atom enum_class.enum" P]
    by (auto simp add: enum_ex_prot_atom_def)
qed
end

lemma wellformed_transaction_cases:
  assumes "wellformed_transaction T"
  shows 
      "(l,x) ∈ set (transaction_receive T) ⟹ ∃t. x = receive⟨t⟩" (is "?A ⟹ ?A'")
      "(l,x) ∈ set (transaction_checks T) ⟹
              (∃ac t s. x = ⟨ac: t ≐ s⟩) ∨ (∃ac t s. x = ⟨ac: t ∈ s⟩) ∨
              (∃X F G. x = ∀X⟨∨≠: F ∨∉: G⟩)"
          (is "?B ⟹ ?B'")
      "(l,x) ∈ set (transaction_updates T) ⟹
              (∃t s. x = insert⟨t,s⟩) ∨ (∃t s. x = delete⟨t,s⟩)" (is "?C ⟹ ?C'")
      "(l,x) ∈ set (transaction_send T) ⟹ ∃t. x = send⟨t⟩" (is "?D ⟹ ?D'")
proof -
  have a:
      "list_all is_Receive (unlabel (transaction_receive T))"
      "list_all is_Check_or_Assignment (unlabel (transaction_checks T))"
      "list_all is_Update (unlabel (transaction_updates T))"
      "list_all is_Send (unlabel (transaction_send T))"
    using assms unfolding wellformed_transaction_def by metis+

  note b = Ball_set unlabel_in
  note c = stateful_strand_step.collapse

  show "?A ⟹ ?A'" by (metis (mono_tags, lifting) a(1) b c(2))
  show "?B ⟹ ?B'" by (metis (no_types, lifting) a(2) b c(3,6,7))
  show "?C ⟹ ?C'" by (metis (mono_tags, lifting) a(3) b c(4,5))
  show "?D ⟹ ?D'" by (metis (mono_tags, lifting) a(4) b c(1))
qed

lemma wellformed_transaction_unlabel_cases:
  assumes "wellformed_transaction T"
  shows 
      "x ∈ set (unlabel (transaction_receive T)) ⟹ ∃t. x = receive⟨t⟩" (is "?A ⟹ ?A'")
      "x ∈ set (unlabel (transaction_checks T)) ⟹
              (∃ac t s. x = ⟨ac: t ≐ s⟩) ∨ (∃ac t s. x = ⟨ac: t ∈ s⟩) ∨
              (∃X F G. x = ∀X⟨∨≠: F ∨∉: G⟩)"
        (is "?B ⟹ ?B'")
      "x ∈ set (unlabel (transaction_updates T)) ⟹
              (∃t s. x = insert⟨t,s⟩) ∨ (∃t s. x = delete⟨t,s⟩)" (is "?C ⟹ ?C'")
      "x ∈ set (unlabel (transaction_send T)) ⟹ ∃t. x = send⟨t⟩" (is "?D ⟹ ?D'")
proof -
  have a:
      "list_all is_Receive (unlabel (transaction_receive T))"
      "list_all is_Check_or_Assignment (unlabel (transaction_checks T))"
      "list_all is_Update (unlabel (transaction_updates T))"
      "list_all is_Send (unlabel (transaction_send T))"
    using assms unfolding wellformed_transaction_def by metis+

  note b = Ball_set
  note c = stateful_strand_step.collapse

  show "?A ⟹ ?A'" by (metis (mono_tags, lifting) a(1) b c(2))
  show "?B ⟹ ?B'" by (metis (no_types, lifting) a(2) b c(3,6,7))
  show "?C ⟹ ?C'" by (metis (mono_tags, lifting) a(3) b c(4,5))
  show "?D ⟹ ?D'" by (metis (mono_tags, lifting) a(4) b c(1))
qed

lemma transaction_strand_subsets[simp]:
  "set (transaction_receive T) ⊆ set (transaction_strand T)"
  "set (transaction_checks T) ⊆ set (transaction_strand T)"
  "set (transaction_updates T) ⊆ set (transaction_strand T)"
  "set (transaction_send T) ⊆ set (transaction_strand T)"
  "set (unlabel (transaction_receive T)) ⊆ set (unlabel (transaction_strand T))"
  "set (unlabel (transaction_checks T)) ⊆ set (unlabel (transaction_strand T))"
  "set (unlabel (transaction_updates T)) ⊆ set (unlabel (transaction_strand T))"
  "set (unlabel (transaction_send T)) ⊆ set (unlabel (transaction_strand T))"
unfolding transaction_strand_def unlabel_def by force+

lemma transaction_strand_subst_subsets[simp]:
  "set (transaction_receive T ⋅lsst θ) ⊆ set (transaction_strand T ⋅lsst θ)"
  "set (transaction_checks T ⋅lsst θ) ⊆ set (transaction_strand T ⋅lsst θ)"
  "set (transaction_updates T ⋅lsst θ) ⊆ set (transaction_strand T ⋅lsst θ)"
  "set (transaction_send T ⋅lsst θ) ⊆ set (transaction_strand T ⋅lsst θ)"
  "set (unlabel (transaction_receive T ⋅lsst θ)) ⊆ set (unlabel (transaction_strand T ⋅lsst θ))"
  "set (unlabel (transaction_checks T ⋅lsst θ)) ⊆ set (unlabel (transaction_strand T ⋅lsst θ))"
  "set (unlabel (transaction_updates T ⋅lsst θ)) ⊆ set (unlabel (transaction_strand T ⋅lsst θ))"
  "set (unlabel (transaction_send T ⋅lsst θ)) ⊆ set (unlabel (transaction_strand T ⋅lsst θ))"
unfolding transaction_strand_def unlabel_def subst_apply_labeled_stateful_strand_def by force+

lemma transaction_strand_dual_unfold:
  defines "f ≡ λS. duallsst S"
  shows "f (transaction_strand T) = 
         f (transaction_receive T)@f (transaction_checks T)@
         f (transaction_updates T)@f (transaction_send T)"
using duallsst_append unfolding f_def transaction_strand_def by auto

lemma transaction_strand_unlabel_dual_unfold:
  defines "f ≡ λS. unlabel (duallsst S)"
  shows "f (transaction_strand T) = 
         f (transaction_receive T)@f (transaction_checks T)@
         f (transaction_updates T)@f (transaction_send T)"
using unlabel_append duallsst_append unfolding f_def transaction_strand_def by auto

lemma transaction_dual_subst_unfold:
  "duallsst (transaction_strand T ⋅lsst θ) =
    duallsst (transaction_receive T ⋅lsst θ)@
    duallsst (transaction_checks T ⋅lsst θ)@
    duallsst (transaction_updates T ⋅lsst θ)@
    duallsst (transaction_send T ⋅lsst θ)"
by (simp add: transaction_strand_def duallsst_append subst_lsst_append)

lemma transaction_dual_subst_unlabel_unfold:
  "unlabel (duallsst (transaction_strand T ⋅lsst θ)) =
    unlabel (duallsst (transaction_receive T ⋅lsst θ))@
    unlabel (duallsst (transaction_checks T ⋅lsst θ))@
    unlabel (duallsst (transaction_updates T ⋅lsst θ))@
    unlabel (duallsst (transaction_send T ⋅lsst θ))"
by (simp add: transaction_dual_subst_unfold unlabel_append)

lemma trms_transaction_unfold:
  "trms_transaction T =
      trmslsst (transaction_receive T) ∪ trmslsst (transaction_checks T) ∪
      trmslsst (transaction_updates T) ∪ trmslsst (transaction_send T)"
by (metis trmssst_append unlabel_append append_assoc transaction_strand_def)

lemma trms_transaction_subst_unfold:
  "trmslsst (transaction_strand T ⋅lsst θ) =
      trmslsst (transaction_receive T ⋅lsst θ) ∪ trmslsst (transaction_checks T ⋅lsst θ) ∪
      trmslsst (transaction_updates T ⋅lsst θ) ∪ trmslsst (transaction_send T ⋅lsst θ)"
by (metis trmssst_append unlabel_append append_assoc transaction_strand_def subst_lsst_append)

lemma vars_transaction_unfold:
  "vars_transaction T =
      varslsst (transaction_receive T) ∪ varslsst (transaction_checks T) ∪
      varslsst (transaction_updates T) ∪ varslsst (transaction_send T)"
by (metis varssst_append unlabel_append append_assoc transaction_strand_def)

lemma vars_transaction_subst_unfold:
  "varslsst (transaction_strand T ⋅lsst θ) =
      varslsst (transaction_receive T ⋅lsst θ) ∪ varslsst (transaction_checks T ⋅lsst θ) ∪
      varslsst (transaction_updates T ⋅lsst θ) ∪ varslsst (transaction_send T ⋅lsst θ)"
by (metis varssst_append unlabel_append append_assoc transaction_strand_def subst_lsst_append)

lemma fv_transaction_unfold:
  "fv_transaction T =
      fvlsst (transaction_receive T) ∪ fvlsst (transaction_checks T) ∪
      fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T)"
by (metis fvsst_append unlabel_append append_assoc transaction_strand_def)

lemma fv_transaction_subst_unfold:
  "fvlsst (transaction_strand T ⋅lsst θ) =
      fvlsst (transaction_receive T ⋅lsst θ) ∪ fvlsst (transaction_checks T ⋅lsst θ) ∪
      fvlsst (transaction_updates T ⋅lsst θ) ∪ fvlsst (transaction_send T ⋅lsst θ)"
by (metis fvsst_append unlabel_append append_assoc transaction_strand_def subst_lsst_append)

lemma bvars_transaction_unfold:
  "bvars_transaction T =
      bvarslsst (transaction_receive T) ∪ bvarslsst (transaction_checks T) ∪
      bvarslsst (transaction_updates T) ∪ bvarslsst (transaction_send T)"
by (metis bvarssst_append unlabel_append append_assoc transaction_strand_def)

lemma bvars_transaction_subst_unfold:
  "bvarslsst (transaction_strand T ⋅lsst θ) =
      bvarslsst (transaction_receive T ⋅lsst θ) ∪ bvarslsst (transaction_checks T ⋅lsst θ) ∪
      bvarslsst (transaction_updates T ⋅lsst θ) ∪ bvarslsst (transaction_send T ⋅lsst θ)"
by (metis bvarssst_append unlabel_append append_assoc transaction_strand_def subst_lsst_append)

lemma bvars_wellformed_transaction_unfold:
  assumes "wellformed_transaction T"
  shows "bvars_transaction T = bvarslsst (transaction_checks T)" (is ?A)
    and "bvarslsst (transaction_receive T) = {}" (is ?B)
    and "bvarslsst (transaction_updates T) = {}" (is ?C)
    and "bvarslsst (transaction_send T) = {}" (is ?D)
proof -
  have 0: "list_all is_Receive (unlabel (transaction_receive T))"
          "list_all is_Update (unlabel (transaction_updates T))"
          "list_all is_Send (unlabel (transaction_send T))"
    using assms unfolding wellformed_transaction_def by metis+

  have "filter is_NegChecks (unlabel (transaction_receive T)) = []"
       "filter is_NegChecks (unlabel (transaction_updates T)) = []"
       "filter is_NegChecks (unlabel (transaction_send T)) = []"
    using list_all_filter_nil[OF 0(1), of is_NegChecks]
          list_all_filter_nil[OF 0(2), of is_NegChecks]
          list_all_filter_nil[OF 0(3), of is_NegChecks]
          stateful_strand_step.distinct_disc(11,21,29,35,39,41)
    by blast+
  thus ?A ?B ?C ?D
    using bvars_transaction_unfold[of T]
          bvarssst_NegChecks[of "unlabel (transaction_receive T)"]
          bvarssst_NegChecks[of "unlabel (transaction_updates T)"]
          bvarssst_NegChecks[of "unlabel (transaction_send T)"]
    by (metis bvarssst_def UnionE emptyE list.set(1) list.simps(8) subsetI subset_Un_eq sup_commute)+
qed

lemma transaction_strand_memberD[dest]:
  assumes "x ∈ set (transaction_strand T)"
  shows "x ∈ set (transaction_receive T) ∨ x ∈ set (transaction_checks T) ∨
         x ∈ set (transaction_updates T) ∨ x ∈ set (transaction_send T)"
using assms by (simp add: transaction_strand_def)

lemma transaction_strand_unlabel_memberD[dest]:
  assumes "x ∈ set (unlabel (transaction_strand T))"
  shows "x ∈ set (unlabel (transaction_receive T)) ∨ x ∈ set (unlabel (transaction_checks T)) ∨
         x ∈ set (unlabel (transaction_updates T)) ∨ x ∈ set (unlabel (transaction_send T))"
using assms by (simp add: unlabel_def transaction_strand_def)

lemma wellformed_transaction_strand_memberD[dest]:
  assumes "wellformed_transaction T" and "(l,x) ∈ set (transaction_strand T)"
  shows
    "x = receive⟨ts⟩ ⟹ (l,x) ∈ set (transaction_receive T)" (is "?A ⟹ ?A'")
    "x = select⟨t,s⟩ ⟹ (l,x) ∈ set (transaction_checks T)" (is "?B ⟹ ?B'")
    "x = ⟨t == s⟩ ⟹ (l,x) ∈ set (transaction_checks T)" (is "?C ⟹ ?C'")
    "x = ⟨t in s⟩ ⟹ (l,x) ∈ set (transaction_checks T)" (is "?D ⟹ ?D'")
    "x = ∀X⟨∨≠: F ∨∉: G⟩  ⟹ (l,x) ∈ set (transaction_checks T)" (is "?E ⟹ ?E'")
    "x = insert⟨t,s⟩ ⟹ (l,x) ∈ set (transaction_updates T)" (is "?F ⟹ ?F'")
    "x = delete⟨t,s⟩ ⟹ (l,x) ∈ set (transaction_updates T)" (is "?G ⟹ ?G'")
    "x = send⟨ts⟩ ⟹ (l,x) ∈ set (transaction_send T)" (is "?H ⟹ ?H'")
    "x = ⟨ac: t ≐ s⟩ ⟹ (l,x) ∈ set (transaction_checks T)" (is "?I ⟹ ?I'")
    "x = ⟨ac: t ∈ s⟩ ⟹ (l,x) ∈ set (transaction_checks T)" (is "?J ⟹ ?J'")
proof -
  have "(l,x) ∈ set (transaction_receive T) ∨ (l,x) ∈ set (transaction_checks T) ∨
        (l,x) ∈ set (transaction_updates T) ∨ (l,x) ∈ set (transaction_send T)"
    using assms(2) by auto
  thus "?A ⟹ ?A'" "?B ⟹ ?B'" "?C ⟹ ?C'" "?D ⟹ ?D'" "?E ⟹ ?E'"
       "?F ⟹ ?F'" "?G ⟹ ?G'" "?H ⟹ ?H'" "?I ⟹ ?I'" "?J ⟹ ?J'"
    using wellformed_transaction_cases[OF assms(1)] by fast+
qed

lemma wellformed_transaction_strand_unlabel_memberD[dest]:
  assumes "wellformed_transaction T" and "x ∈ set (unlabel (transaction_strand T))"
  shows
    "x = receive⟨ts⟩ ⟹ x ∈ set (unlabel (transaction_receive T))" (is "?A ⟹ ?A'")
    "x = select⟨t,s⟩ ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?B ⟹ ?B'")
    "x = ⟨t == s⟩ ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?C ⟹ ?C'")
    "x = ⟨t in s⟩ ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?D ⟹ ?D'")
    "x = ∀X⟨∨≠: F ∨∉: G⟩  ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?E ⟹ ?E'")
    "x = insert⟨t,s⟩ ⟹ x ∈ set (unlabel (transaction_updates T))" (is "?F ⟹ ?F'")
    "x = delete⟨t,s⟩ ⟹ x ∈ set (unlabel (transaction_updates T))" (is "?G ⟹ ?G'")
    "x = send⟨ts⟩ ⟹ x ∈ set (unlabel (transaction_send T))" (is "?H ⟹ ?H'")
    "x = ⟨ac: t ≐ s⟩ ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?I ⟹ ?I'")
    "x = ⟨ac: t ∈ s⟩ ⟹ x ∈ set (unlabel (transaction_checks T))" (is "?J ⟹ ?J'")
proof -
  have "x ∈ set (unlabel (transaction_receive T)) ∨ x ∈ set (unlabel (transaction_checks T)) ∨
        x ∈ set (unlabel (transaction_updates T)) ∨ x ∈ set (unlabel (transaction_send T))"
    using assms(2) by auto
  thus "?A ⟹ ?A'" "?B ⟹ ?B'" "?C ⟹ ?C'" "?D ⟹ ?D'" "?E ⟹ ?E'"
       "?F ⟹ ?F'" "?G ⟹ ?G'" "?H ⟹ ?H'" "?I ⟹ ?I'" "?J ⟹ ?J'"
    using wellformed_transaction_unlabel_cases[OF assms(1)] by fast+
qed

lemma wellformed_transaction_send_receive_trm_cases:
  assumes T: "wellformed_transaction T"
  shows "t ∈ trmslsst (transaction_receive T) ⟹ ∃ts. t ∈ set ts ∧ receive⟨ts⟩ ∈ set (unlabel (transaction_receive T))"
    and "t ∈ trmslsst (transaction_send T) ⟹ ∃ts. t ∈ set ts ∧ send⟨ts⟩ ∈ set (unlabel (transaction_send T))"
using wellformed_transaction_unlabel_cases(1,4)[OF T]
      trmssst_in[of t "unlabel (transaction_receive T)"]
      trmssst_in[of t "unlabel (transaction_send T)"]
by fastforce+

lemma wellformed_transaction_send_receive_subst_trm_cases:
  assumes T: "wellformed_transaction T"
  shows "t ∈ trmslsst (transaction_receive T) ⋅set θ ⟹ ∃ts. t ∈ set ts ∧ receive⟨ts⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
    and "t ∈ trmslsst (transaction_send T) ⋅set θ ⟹ ∃ts. t ∈ set ts ∧ send⟨ts⟩ ∈ set (unlabel (transaction_send T ⋅lsst θ))"
proof -
  assume "t ∈ trmslsst (transaction_receive T) ⋅set θ"
  then obtain s where s: "s ∈ trmslsst (transaction_receive T)" "t = s ⋅ θ"
    by blast
  hence "∃ts. s ∈ set ts ∧ receive⟨ts⟩ ∈ set (unlabel (transaction_receive T))"
    using wellformed_transaction_send_receive_trm_cases(1)[OF T] by simp
  thus "∃ts. t ∈ set ts ∧ receive⟨ts⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
    using s(2) unlabel_subst[of _ θ] subst_set_map[of s _ θ]
          stateful_strand_step_subst_inI(2)[of _ "unlabel (transaction_receive T)" θ]
    by metis
next
  assume "t ∈ trmslsst (transaction_send T) ⋅set θ"
  then obtain s where s: "s ∈ trmslsst (transaction_send T)" "t = s ⋅ θ"
    by blast
  hence "∃ts. s ∈ set ts ∧ send⟨ts⟩ ∈ set (unlabel (transaction_send T))"
    using wellformed_transaction_send_receive_trm_cases(2)[OF T] by simp
  thus "∃ts. t ∈ set ts ∧ send⟨ts⟩ ∈ set (unlabel (transaction_send T ⋅lsst θ))"
    using s(2) unlabel_subst[of _ θ] subst_set_map[of s _ θ]
          stateful_strand_step_subst_inI(1)[of _ "unlabel (transaction_send T)" θ]
    by metis
qed

lemma wellformed_transaction_send_receive_fv_subset:
  assumes T: "wellformed_transaction T"
  shows "t ∈ trmslsst (transaction_receive T) ⟹ fv t ⊆ fv_transaction T" (is "?A ⟹ ?A'")
    and "t ∈ trmslsst (transaction_send T) ⟹ fv t ⊆ fv_transaction T" (is "?B ⟹ ?B'")
proof -
  let ?P = "∃ts. t ∈ set ts ∧ receive⟨ts⟩ ∈ set (unlabel (transaction_strand T))"
  let ?Q = "∃ts. t ∈ set ts ∧ send⟨ts⟩ ∈ set (unlabel (transaction_strand T))"

  have *: "t ∈ trmslsst (transaction_receive T) ⟹ ?P" "t ∈ trmslsst (transaction_send T) ⟹ ?Q"
    using wellformed_transaction_send_receive_trm_cases[OF T, of t]
    unfolding transaction_strand_def by force+
  
  show "?A ⟹ ?A'" using *(1) by (induct "transaction_strand T") (simp, force)
  show "?B ⟹ ?B'" using *(2) by (induct "transaction_strand T") (simp, force)
qed

lemma dual_wellformed_transaction_ident_cases[dest]:
  "list_all is_Assignment (unlabel S) ⟹ duallsst S = S"
  "list_all is_Check (unlabel S) ⟹ duallsst S = S"
  "list_all is_Update (unlabel S) ⟹ duallsst S = S"
proof (induction S)
  case (Cons s S)
  obtain l x where s: "s = (l,x)" by force
  { case 1 thus ?case using Cons s unfolding unlabel_def duallsst_def by (cases x) auto }
  { case 2 thus ?case using Cons s unfolding unlabel_def duallsst_def by (cases x) auto }
  { case 3 thus ?case using Cons s unfolding unlabel_def duallsst_def by (cases x) auto }
qed simp_all

lemma wellformed_transaction_wfsst:
  fixes T::"('a, 'b, 'c, 'd) prot_transaction"
  assumes T: "wellformed_transaction T"
  shows "wf'sst (fst ` set (transaction_decl T ()) ∪ set (transaction_fresh T))
               (unlabel (duallsst (transaction_strand T)))"
    and "fv_transaction T ∩ bvars_transaction T = {}"
using T unfolding wellformed_transaction_def by simp_all

lemma dual_wellformed_transaction_ident_cases'[dest]:
  assumes "wellformed_transaction T"
  shows "duallsst (transaction_checks T) = transaction_checks T" (is ?A)
        "duallsst (transaction_updates T) = transaction_updates T" (is ?B)
proof -
  have "list_all is_Check_or_Assignment (unlabel (transaction_checks T))"
       "list_all is_Update (unlabel (transaction_updates T))"
    using assms is_Check_or_Assignment_iff unfolding wellformed_transaction_def by auto
  thus ?A ?B
    using duallsst_list_all_same(9)[of "transaction_checks T"]
          duallsst_list_all_same(8)[of "transaction_updates T"]
    by (blast, blast)
qed

lemma dual_transaction_strand:
  assumes "wellformed_transaction T"
  shows "duallsst (transaction_strand T) =
         duallsst (transaction_receive T)@transaction_checks T@
         transaction_updates T@duallsst (transaction_send T)"
using dual_wellformed_transaction_ident_cases'[OF assms] duallsst_append
unfolding transaction_strand_def by metis

lemma dual_unlabel_transaction_strand:
  assumes "wellformed_transaction T"
  shows "unlabel (duallsst (transaction_strand T)) =
         (unlabel (duallsst (transaction_receive T)))@(unlabel (transaction_checks T))@
         (unlabel (transaction_updates T))@(unlabel (duallsst (transaction_send T)))"
using dual_transaction_strand[OF assms] by (simp add: unlabel_def)

lemma dual_transaction_strand_subst:
  assumes "wellformed_transaction T"
  shows "duallsst (transaction_strand T ⋅lsst δ) =
          (duallsst (transaction_receive T)@transaction_checks T@
          transaction_updates T@duallsst (transaction_send T)) ⋅lsst δ"
proof -
  have "duallsst (transaction_strand T ⋅lsst δ) = duallsst (transaction_strand T) ⋅lsst δ"
    using duallsst_subst by metis
  thus ?thesis using dual_transaction_strand[OF assms] by argo
qed

lemma dual_transaction_ik_is_transaction_send:
  assumes "wellformed_transaction T"
  shows "iksst (unlabel (duallsst (transaction_strand T))) = trmssst (unlabel (transaction_send T))"
    (is "?A = ?B")
proof -
  { fix t assume "t ∈ ?A"
    then obtain ts where ts:
        "t ∈ set ts" "receive⟨ts⟩ ∈ set (unlabel (duallsst (transaction_strand T)))"
      by (auto simp add: iksst_def)
    hence *: "send⟨ts⟩ ∈ set (unlabel (transaction_strand T))"
      using duallsst_unlabel_steps_iff(1) by metis
    have "t ∈ ?B"
      using ts(1) wellformed_transaction_strand_unlabel_memberD(8)[OF assms *, of ts] by force
  } moreover {
    fix t assume "t ∈ ?B"
    then obtain ts where ts:
        "t ∈ set ts" "send⟨ts⟩ ∈ set (unlabel (transaction_send T))"
      using wellformed_transaction_unlabel_cases(4)[OF assms] by fastforce
    hence "receive⟨ts⟩ ∈ set (unlabel (duallsst (transaction_send T)))"
      using duallsst_unlabel_steps_iff(1) by metis
    hence "receive⟨ts⟩ ∈ set (unlabel (duallsst (transaction_strand T)))"
      using dual_unlabel_transaction_strand[OF assms] by simp 
    hence "t ∈ ?A" using ts(1) by (auto simp add: iksst_def)
  } ultimately show "?A = ?B" by auto
qed

lemma dual_transaction_ik_is_transaction_send':
  fixes δ::"('a,'b,'c,'d) prot_subst"
  assumes "wellformed_transaction T"
  shows "iksst (unlabel (duallsst (transaction_strand T ⋅lsst δ)))  =
         trmssst (unlabel (transaction_send T)) ⋅set δ" (is "?A = ?B")
using dual_transaction_ik_is_transaction_send[OF assms]
      subst_lsst_unlabel[of "duallsst (transaction_strand T)" δ]
      iksst_subst[of "unlabel (duallsst (transaction_strand T))" δ]
      duallsst_subst[of "transaction_strand T" δ]
by auto

lemma dbsst_transaction_prefix_eq:
  assumes T: "wellformed_transaction T"
    and S: "prefix S (transaction_receive T@transaction_checks T)"
  shows "dblsst A = dblsst (A@duallsst (S ⋅lsst δ))"
proof -
  let ?T1 = "transaction_receive T"
  let ?T2 = "transaction_checks T"

  have *: "prefix (unlabel S) (unlabel (?T1@?T2))" using S prefix_unlabel by blast

  have "list_all is_Receive (unlabel ?T1)"
       "list_all is_Check_or_Assignment (unlabel ?T2)"
    using T by (simp_all add: wellformed_transaction_def)
  hence "∀b ∈ set (unlabel ?T1). ¬is_Insert b ∧ ¬is_Delete b"
        "∀b ∈ set (unlabel ?T2). ¬is_Insert b ∧ ¬is_Delete b"
    by (metis (mono_tags, lifting) Ball_set stateful_strand_step.distinct_disc(16,18),
        metis (mono_tags, lifting) Ball_set stateful_strand_step.distinct_disc(24,26,33,35,37,39))
  hence "∀b ∈ set (unlabel (?T1@?T2)). ¬is_Insert b ∧ ¬is_Delete b"
    by (auto simp add: unlabel_def)
  hence "∀b ∈ set (unlabel S). ¬is_Insert b ∧ ¬is_Delete b"
    using * unfolding prefix_def by fastforce
  hence "∀b ∈ set (unlabel (duallsst S) ⋅sst δ). ¬is_Insert b ∧ ¬is_Delete b"
  proof (induction S)
    case (Cons a S)
    then obtain l b where "a = (l,b)" by (metis surj_pair)
    thus ?case
      using Cons unfolding duallsst_def unlabel_def subst_apply_stateful_strand_def
      by (cases b) auto
  qed simp
  hence **: "∀b ∈ set (unlabel (duallsst (S ⋅lsst δ))). ¬is_Insert b ∧ ¬is_Delete b"
    by (metis duallsst_subst_unlabel)

  show ?thesis 
    using dbsst_no_upd_append[OF **] unlabel_append
    unfolding dbsst_def by metis
qed

lemma dblsst_duallsst_set_ex:
   assumes "d ∈ set (db'lsst (duallsst A ⋅lsst θ) ℐ D)"
    "∀t u. insert⟨t,u⟩ ∈ set (unlabel A) ⟶ (∃s. u = Fun (Set s) [])"
    "∀t u. delete⟨t,u⟩ ∈ set (unlabel A) ⟶ (∃s. u = Fun (Set s) [])"
    "∀d ∈ set D. ∃s. snd d = Fun (Set s) []"
  shows "∃s. snd d = Fun (Set s) []"
  using assms
proof (induction A arbitrary: D)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)

  have 1: "unlabel (duallsst (a#A) ⋅lsst θ) = receive⟨ts ⋅list θ⟩#unlabel (duallsst A ⋅lsst θ)"
    when "b = send⟨ts⟩" for ts
    by (simp add: a that subst_lsst_unlabel_cons)

  have 2: "unlabel (duallsst (a#A) ⋅lsst θ) = send⟨ts ⋅list θ⟩#unlabel (duallsst A ⋅lsst θ)"
    when "b = receive⟨ts⟩" for ts
    by (simp add: a that subst_lsst_unlabel_cons)

  have 3: "unlabel (duallsst (a#A) ⋅lsst θ) = (b ⋅sstp θ)#unlabel (duallsst A ⋅lsst θ)"
    when "∄ts. b = send⟨ts⟩ ∨ b = receive⟨ts⟩"
    using a that duallsst_Cons subst_lsst_unlabel_cons[of l b]
    by (cases b) auto

  show ?case using 1 2 3 a Cons by (cases b) fastforce+
qed simp

lemma is_Fun_SetE[elim]:
  assumes t: "is_Fun_Set t"
  obtains s where "t = Fun (Set s) []"
proof (cases t)
  case (Fun f T)
  then obtain s where "f = Set s" using t unfolding is_Fun_Set_def by (cases f) force+
  moreover have "T = []" using Fun t unfolding is_Fun_Set_def by (cases T) auto
  ultimately show ?thesis using Fun that by fast
qed (use t is_Fun_Set_def in fast)

lemma Fun_Set_InSet_iff:
  "(u = ⟨a: Var x ∈ Fun (Set s) []⟩) ⟷
   (is_InSet u ∧ is_Var (the_elem_term u) ∧ is_Fun_Set (the_set_term u) ∧
    the_Set (the_Fun (the_set_term u)) = s ∧ the_Var (the_elem_term u) = x ∧ the_check u = a)"
  (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B" unfolding is_Fun_Set_def by auto

  assume B: ?B
  thus ?A
  proof (cases u)
    case (InSet b t t')
    hence "b = a" "t = Var x" "t' = Fun (Set s) []"
      using B by (simp, fastforce, fastforce)
    thus ?thesis using InSet by fast
  qed auto
qed

lemma Fun_Set_NotInSet_iff:
  "(u = ⟨Var x not in Fun (Set s) []⟩) ⟷
   (is_NegChecks u ∧ bvarssstp u = [] ∧ the_eqs u = [] ∧ length (the_ins u) = 1 ∧
    is_Var (fst (hd (the_ins u))) ∧ is_Fun_Set (snd (hd (the_ins u)))) ∧
    the_Set (the_Fun (snd (hd (the_ins u)))) = s ∧ the_Var (fst (hd (the_ins u))) = x"
  (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B" unfolding is_Fun_Set_def by auto

  assume B: ?B
  show ?A
  proof (cases u)
    case (NegChecks X F F')
    hence "X = []" "F = []"
      using B by auto
    moreover have "fst (hd (the_ins u)) = Var x" "snd (hd (the_ins u)) = Fun (Set s) []"
      using B is_Fun_SetE[of "snd (hd (the_ins u))"]
      by (force, fastforce)
    hence "F' = [(Var x, Fun (Set s) [])]"
      using NegChecks B by (cases "the_ins u") auto
    ultimately show ?thesis using NegChecks by fast
  qed (use B in auto)
qed

lemma is_Fun_Set_exi: "is_Fun_Set x ⟷ (∃s. x = Fun (Set s) [])"
by (metis prot_fun.collapse(2) term.collapse(2) prot_fun.disc(11) term.disc(2)
          term.sel(2,4) is_Fun_Set_def un_Fun1_def)

lemma is_Fun_Set_subst:
  assumes "is_Fun_Set S'"
  shows "is_Fun_Set (S' ⋅ σ)"
using assms by (fastforce simp add: is_Fun_Set_def)

lemma is_Update_in_transaction_updates:
  assumes tu: "is_Update t"
  assumes t: "t ∈ set (unlabel (transaction_strand TT))"
  assumes vt: "wellformed_transaction TT"
  shows "t ∈ set (unlabel (transaction_updates TT))"
using t tu vt unfolding transaction_strand_def wellformed_transaction_def list_all_iff
by (auto simp add: unlabel_append)

lemma transaction_proj_member:
  assumes "T ∈ set P"
  shows "transaction_proj n T ∈ set (map (transaction_proj n) P)"
using assms by simp

lemma transaction_strand_proj:
  "transaction_strand (transaction_proj n T) = proj n (transaction_strand T)"
proof -
  obtain A B C D E F where "T = Transaction A B C D E F" by (cases T) simp
  thus ?thesis
    using transaction_proj.simps[of n A B C D E F]
    unfolding transaction_strand_def proj_def Let_def by auto
qed

lemma transaction_proj_decl_eq:
  "transaction_decl (transaction_proj n T) = transaction_decl T"
proof -
  obtain A B C D E F where "T = Transaction A B C D E F" by (cases T) simp
  thus ?thesis
    using transaction_proj.simps[of n A B C D E F]
    unfolding proj_def Let_def by auto
qed

lemma transaction_proj_fresh_eq:
  "transaction_fresh (transaction_proj n T) = transaction_fresh T"
proof -
  obtain A B C D E F where "T = Transaction A B C D E F" by (cases T) simp
  thus ?thesis
    using transaction_proj.simps[of n A B C D E F]
    unfolding proj_def Let_def by auto
qed

lemma transaction_proj_trms_subset:
  "trms_transaction (transaction_proj n T) ⊆ trms_transaction T"
proof -
  obtain A B C D E F where "T = Transaction A B C D E F" by (cases T) simp
  thus ?thesis
    using transaction_proj.simps[of n A B C D E F] trmssst_proj_subset(1)[of n]
    unfolding transaction_fresh_def Let_def transaction_strand_def by auto
qed

lemma transaction_proj_vars_subset:
  "vars_transaction (transaction_proj n T) ⊆ vars_transaction T"
proof -
  obtain A B C D E F where "T = Transaction A B C D E F" by (cases T) simp
  thus ?thesis
    using transaction_proj.simps[of n A B C D E F]
          sst_vars_proj_subset(3)[of n "transaction_strand T"]
    unfolding transaction_fresh_def Let_def transaction_strand_def by simp
qed

lemma transaction_proj_labels:
  fixes T::"('a,'b,'c,'d) prot_transaction"
  shows "list_all (λa. has_LabelN l a ∨ has_LabelS a) (transaction_strand (transaction_proj l T))"
proof -
  define h where "h ≡ λa::('a,'b,'c,'d) prot_strand_step. has_LabelN l a ∨ has_LabelS a"
  let ?f = "filter h"
  let ?g = "list_all h"

  obtain T1 T2 T3 T4 T5 T6 where T: "T = Transaction T1 T2 T3 T4 T5 T6" by (cases T) simp

  note 0 = transaction_proj.simps[unfolded Let_def, of l T1 T2 T3 T4 T5 T6]

  show ?thesis using T 0 unfolding list_all_iff proj_def by auto
qed

lemma transaction_proj_ident_iff:
  fixes T::"('a,'b,'c,'d) prot_transaction"
  shows "list_all (λa. has_LabelN l a ∨ has_LabelS a) (transaction_strand T) ⟷
         transaction_proj l T = T"
    (is "?A ⟷ ?B")
proof
  obtain T1 T2 T3 T4 T5 T6 where T: "T = Transaction T1 T2 T3 T4 T5 T6" by (cases T) simp
  hence "transaction_strand T = T3@T4@T5@T6" unfolding transaction_strand_def by simp
  thus "?A ⟹ ?B"
    using T transaction_proj.simps[unfolded Let_def, of l T1 T2 T3 T4 T5 T6]
    unfolding list_all_iff proj_def by auto

  show "?B ⟹ ?A" using transaction_proj_labels[of l T] by presburger
qed

lemma transaction_proj_idem:
  fixes T::"('a,'b,'c,'d) prot_transaction"
  shows "transaction_proj l (transaction_proj l T) = transaction_proj l T"
by (meson transaction_proj_ident_iff transaction_proj_labels)

lemma transaction_proj_ball_subst:
  assumes
    "set Ps = (λn. map (transaction_proj n) P) ` set L"
    "∀p ∈ set Ps. Q p"
  shows "∀l ∈ set L. Q (map (transaction_proj l) P)"
using assms by auto

lemma transaction_star_proj_has_star_labels:
  "list_all has_LabelS (transaction_strand (transaction_star_proj T))"
proof -
  let ?f = "filter has_LabelS"

  obtain T1 T2 T3 T4 T5 T6 where T: "T = Transaction T1 T2 T3 T4 T5 T6" by (cases T) simp
  hence T': "transaction_strand (transaction_star_proj T) = ?f T3@?f T4@?f T5@?f T6"
    using transaction_star_proj.simps[unfolded Let_def, of T1 T2 T3 T4 T5 T6]
    unfolding transaction_strand_def by auto

  show ?thesis using Ball_set unfolding T' by fastforce
qed

lemma transaction_star_proj_ident_iff:
  "list_all has_LabelS (transaction_strand T) ⟷ transaction_star_proj T = T" (is "?A ⟷ ?B")
proof
  obtain T1 T2 T3 T4 T5 T6 where T: "T = Transaction T1 T2 T3 T4 T5 T6" by (cases T) simp
  hence T': "transaction_strand T = T3@T4@T5@T6" unfolding transaction_strand_def by simp

  show "?A ⟹ ?B" using T T' unfolding list_all_iff by auto
  show "?B ⟹ ?A" using transaction_star_proj_has_star_labels[of T] by auto
qed

lemma transaction_star_proj_negates_transaction_proj:
  "transaction_star_proj (transaction_proj l T) = transaction_star_proj T" (is "?A l T")
  "k ≠ l ⟹ transaction_proj k (transaction_proj l T) = transaction_star_proj T" (is "?B ⟹ ?B'")
proof -
  show "?A l T" for l T
  proof -
    obtain T1 T2 T3 T4 T5 T6 where T: "T = Transaction T1 T2 T3 T4 T5 T6" by (cases T) simp
    thus ?thesis
      by (metis dbproj_def transaction_proj.simps transaction_star_proj.simps proj_dbproj(2))
  qed
  thus "?B ⟹ ?B'"
    by (metis (no_types) has_LabelS_proj_iff_not_has_LabelN proj_elims_label
        transaction_star_proj_ident_iff transaction_strand_proj)
qed

lemma transaction_updates_send_ex_iff:
  fixes T::"('a,'b,'c,'d) prot_transaction"
  assumes "list_all is_Receive (unlabel (transaction_receive T))"
          "list_all is_Check_or_Assignment (unlabel (transaction_checks T))"
          "list_all is_Update (unlabel (transaction_updates T))"
          "list_all is_Send (unlabel (transaction_send T))"
  shows "transaction_updates T ≠ [] ∨ transaction_send T ≠ [] ⟷
         list_ex (λa. is_Send (snd a) ∨ is_Update (snd a)) (transaction_strand T)"
proof -
  define f where "f ≡ λa::('a,'b,'c,'d) prot_strand_step. is_Send (snd a) ∨ is_Update (snd a)"

  have 0: "list_all (λa. ¬(f a)) (transaction_receive T)"
          "list_all (λa. ¬(f a)) (transaction_checks T)"
          "list_all (λa. (f a)) (transaction_updates T)"
          "list_all (λa. (f a)) (transaction_send T)"
    using assms unfolding list_all_iff unlabel_def f_def by auto

  have 1:
      "list_ex f (transaction_strand T) ⟷
       list_ex f (transaction_updates T) ∨ list_ex f (transaction_send T)"
    using 0 unfolding list_all_iff list_ex_iff transaction_strand_def by auto

  have 2: "A ≠ [] ⟷ list_ex f A" when "list_all f A" for A
    using that by (induct A) auto

  thus ?thesis
    using 1 2[OF 0(3)] 2[OF 0(4)] unfolding list_all_iff list_ex_iff f_def[symmetric] by meson
qed

end