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: av  Var (Var (Atom a), n)::('a,'b,'c,'d) prot_term"

abbreviation Var_Comp_Fu_term ("_: __⟩⟩v") where
  "n: fT⟩⟩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 Tt  Fun (Fu f) T::('a,'b,'c,'d) prot_term"

abbreviation Fun_Fu_const_term ("_c") where
  "cc  Fun (Fu c) []::('a,'b,'c,'d) prot_term"

abbreviation Fun_Set_const_term ("_s") where
  "fs  Fun (Set f) []::('a,'b,'c,'d) prot_term"

abbreviation Fun_Set_composed_term ("__⟩⟩s") where
  "fT⟩⟩s  Fun (Set f) T::('a,'b,'c,'d) prot_term"

abbreviation Fun_Abs_const_term ("_abs") where
  "aabs  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]