Session Automated_Stateful_Protocol_Verification

Theory Transactions

(*
(C) Copyright Andreas Viktor Hess, DTU, 2020
(C) Copyright Sebastian A. Mödersheim, DTU, 2020
(C) Copyright Achim D. Brucker, University of Exeter, 2020
(C) Copyright Anders Schlichtkrull, DTU, 2020

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  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
*)

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

datatype ('a,'b,'c) prot_fun =
  Fu (the_Fu: 'a)
| Set (the_Set: 'c)
| Val (the_Val: "nat × bool")
| Abs (the_Abs: "'c set")
| Pair
| Attack nat
| PubConstAtom 'b nat
| PubConstSetType nat
| PubConstAttackType nat
| PubConstBottom nat
| PubConstOccursSecType nat
| OccursFact
| OccursSec

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

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

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

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

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

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

type_synonym ('a,'b,'c,'d) prot_strand_step =
  "(('a,'b,'c) prot_fun, ('a,'b,'c) 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"

datatype ('a,'b,'c,'d) prot_transaction =
  Transaction
    (transaction_fresh:   "('a,'b,'c) prot_var list")
    (transaction_receive: "('a,'b,'c,'d) prot_strand")
    (transaction_selects: "('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_selects 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 (f 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 is_LabelS
  in Transaction A (f 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_Assignment (unlabel (transaction_selects T)) ∧
    list_all is_Check (unlabel (transaction_checks T)) ∧
    list_all is_Update (unlabel (transaction_updates T)) ∧
    list_all is_Send (unlabel (transaction_send T)) ∧
    set (transaction_fresh T) ⊆ fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T) ∧
    set (transaction_fresh T) ∩ fvlsst (transaction_receive T) = {} ∧
    set (transaction_fresh T) ∩ fvlsst (transaction_selects T) = {} ∧
    fv_transaction T ∩ bvars_transaction T = {} ∧
    fvlsst (transaction_checks T) ⊆ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T) ∧
    fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T) - set (transaction_fresh T)
      ⊆ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T) ∧
    (∀x ∈ set (unlabel (transaction_selects T)).
      is_Equality x ⟶ fv (the_rhs x) ⊆ fvlsst (transaction_receive T))"

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

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

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

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

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

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

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

abbreviation prot_transaction1 ("transaction1 _ _ new _ _ _") where
  "transaction1 (S1::('a,'b,'c,'d) prot_strand) S2 new (B::('a,'b,'c) 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}"
proof -
  have "a ∈ range Atom ∨ a = Value ∨ a = SetType ∨ a = AttackType ∨ a = Bottom ∨ a = OccursSecType"
    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]"
definition "enum_all_prot_atom P == list_all P (map Atom enum_class.enum@[Value, SetType, AttackType, Bottom, OccursSecType])"
definition "enum_ex_prot_atom P == list_ex P (map Atom enum_class.enum@[Value, SetType, AttackType, Bottom, OccursSecType])"

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] = {}" 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} 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} 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_selects T) ⟹
             (∃t s. x = ⟨t := s⟩) ∨ (∃t s. x = select⟨t,s⟩)" (is "?B ⟹ ?B'")
      "(l,x) ∈ set (transaction_checks T) ⟹
              (∃t s. x = ⟨t == s⟩) ∨ (∃t s. x = ⟨t in s⟩) ∨ (∃X F G. x = ∀X⟨∨≠: F ∨∉: G⟩)" (is "?C ⟹ ?C'")
      "(l,x) ∈ set (transaction_updates T) ⟹
              (∃t s. x = insert⟨t,s⟩) ∨ (∃t s. x = delete⟨t,s⟩)" (is "?D ⟹ ?D'")
      "(l,x) ∈ set (transaction_send T) ⟹ ∃t. x = send⟨t⟩" (is "?E ⟹ ?E'")
proof -
  have a:
      "list_all is_Receive (unlabel (transaction_receive T))"
      "list_all is_Assignment (unlabel (transaction_selects T))"
      "list_all is_Check (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 (mono_tags, lifting) a(2) b c(3,6))
  show "?C ⟹ ?C'" by (metis (mono_tags, lifting) a(3) b c(3,6,7))
  show "?D ⟹ ?D'" by (metis (mono_tags, lifting) a(4) b c(4,5))
  show "?E ⟹ ?E'" by (metis (mono_tags, lifting) a(5) 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_selects T)) ⟹
             (∃t s. x = ⟨t := s⟩) ∨ (∃t s. x = select⟨t,s⟩)" (is "?B ⟹ ?B'")
      "x ∈ set (unlabel (transaction_checks T)) ⟹
              (∃t s. x = ⟨t == s⟩) ∨ (∃t s. x = ⟨t in s⟩) ∨ (∃X F G. x = ∀X⟨∨≠: F ∨∉: G⟩)"
        (is "?C ⟹ ?C'")
      "x ∈ set (unlabel (transaction_updates T)) ⟹
              (∃t s. x = insert⟨t,s⟩) ∨ (∃t s. x = delete⟨t,s⟩)" (is "?D ⟹ ?D'")
      "x ∈ set (unlabel (transaction_send T)) ⟹ ∃t. x = send⟨t⟩" (is "?E ⟹ ?E'")
proof -
  have a:
      "list_all is_Receive (unlabel (transaction_receive T))"
      "list_all is_Assignment (unlabel (transaction_selects T))"
      "list_all is_Check (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 (mono_tags, lifting) a(2) b c(3,6))
  show "?C ⟹ ?C'" by (metis (mono_tags, lifting) a(3) b c(3,6,7))
  show "?D ⟹ ?D'" by (metis (mono_tags, lifting) a(4) b c(4,5))
  show "?E ⟹ ?E'" by (metis (mono_tags, lifting) a(5) b c(1))
qed

lemma transaction_strand_subsets[simp]:
  "set (transaction_receive T) ⊆ set (transaction_strand T)"
  "set (transaction_selects 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_selects 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_selects 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_selects 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_dual_subst_unfold:
  "unlabel (duallsst (transaction_strand T ⋅lsst θ)) =
    unlabel (duallsst (transaction_receive T ⋅lsst θ))@
    unlabel (duallsst (transaction_selects T ⋅lsst θ))@
    unlabel (duallsst (transaction_checks T ⋅lsst θ))@
    unlabel (duallsst (transaction_updates T ⋅lsst θ))@
    unlabel (duallsst (transaction_send T ⋅lsst θ))"
by (simp add: transaction_strand_def unlabel_append duallsst_append subst_lsst_append)

lemma trms_transaction_unfold:
  "trms_transaction T =
      trmslsst (transaction_receive T) ∪ trmslsst (transaction_selects 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_selects 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_selects 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_selects 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_selects 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_selects 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 fv_wellformed_transaction_unfold:
  assumes "wellformed_transaction T"
  shows "fv_transaction T =
    fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T) ∪ set (transaction_fresh T)"
proof -
  let ?A = "set (transaction_fresh T)"
  let ?B = "fvlsst (transaction_updates T)"
  let ?C = "fvlsst (transaction_send T)"
  let ?D = "fvlsst (transaction_receive T)"
  let ?E = "fvlsst (transaction_selects T)"
  let ?F = "fvlsst (transaction_checks T)"

  have "?A ⊆ ?B ∪ ?C" "?A ∩ ?D = {}" "?A ∩ ?E = {}" "?F ⊆ ?D ∪ ?E" "?B ∪ ?C - ?A ⊆ ?D ∪ ?E"
    using assms unfolding wellformed_transaction_def by fast+
  thus ?thesis using fv_transaction_unfold by blast
qed

lemma bvars_transaction_unfold:
  "bvars_transaction T =
      bvarslsst (transaction_receive T) ∪ bvarslsst (transaction_selects 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_selects 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_selects T) = {}" (is ?C)
    and "bvarslsst (transaction_updates T) = {}" (is ?D)
    and "bvarslsst (transaction_send T) = {}" (is ?E)
proof -
  have 0: "list_all is_Receive (unlabel (transaction_receive T))"
          "list_all is_Assignment (unlabel (transaction_selects 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_selects 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]
          list_all_filter_nil[OF 0(4), of is_NegChecks]
          stateful_strand_step.distinct_disc(11,21,29,35,39,41)
    by blast+
  thus ?A ?B ?C ?D ?E
    using bvars_transaction_unfold[of T]
          bvarssst_NegChecks[of "unlabel (transaction_receive T)"]
          bvarssst_NegChecks[of "unlabel (transaction_selects 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_selects 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_selects 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⟨t⟩ ⟹ (l,x) ∈ set (transaction_receive T)" (is "?A ⟹ ?A'")
    "x = select⟨t,s⟩ ⟹ (l,x) ∈ set (transaction_selects 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⟨t⟩ ⟹ (l,x) ∈ set (transaction_send T)" (is "?H ⟹ ?H'")
proof -
  have "(l,x) ∈ set (transaction_receive T) ∨ (l,x) ∈ set (transaction_selects 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'"
    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⟨t⟩ ⟹ x ∈ set (unlabel (transaction_receive T))" (is "?A ⟹ ?A'")
    "x = select⟨t,s⟩ ⟹ x ∈ set (unlabel (transaction_selects 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⟨t⟩ ⟹ x ∈ set (unlabel (transaction_send T))" (is "?H ⟹ ?H'")
proof -
  have "x ∈ set (unlabel (transaction_receive T)) ∨ x ∈ set (unlabel (transaction_selects 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'"
    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) ⟹ receive⟨t⟩ ∈ set (unlabel (transaction_receive T))"
    and "t ∈ trmslsst (transaction_send T) ⟹ send⟨t⟩ ∈ set (unlabel (transaction_send T))"
using wellformed_transaction_unlabel_cases(1,5)[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 θ ⟹ receive⟨t⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
    and "t ∈ trmslsst (transaction_send T) ⋅set θ ⟹ send⟨t⟩ ∈ 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 "receive⟨s⟩ ∈ set (unlabel (transaction_receive T))"
    using wellformed_transaction_send_receive_trm_cases(1)[OF T] by simp
  thus "receive⟨t⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
    by (metis s(2) unlabel_subst[of _ θ] stateful_strand_step_subst_inI(2))
next
  assume "t ∈ trmslsst (transaction_send T) ⋅set θ"
  then obtain s where s: "s ∈ trmslsst (transaction_send T)" "t = s ⋅ θ"
    by blast
  hence "send⟨s⟩ ∈ set (unlabel (transaction_send T))"
    using wellformed_transaction_send_receive_trm_cases(2)[OF T] by simp
  thus "send⟨t⟩ ∈ set (unlabel (transaction_send T ⋅lsst θ))"
    by (metis s(2) unlabel_subst[of _ θ] stateful_strand_step_subst_inI(1))
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 -
  have "t ∈ trmslsst (transaction_receive T) ⟹ receive⟨t⟩ ∈ set (unlabel (transaction_strand T))"
       "t ∈ trmslsst (transaction_send T) ⟹ send⟨t⟩ ∈ set (unlabel (transaction_strand T))"
    using wellformed_transaction_send_receive_trm_cases[OF T, of t]
    unfolding transaction_strand_def by force+
  thus "?A ⟹ ?A'" "?B ⟹ ?B'" by (induct "transaction_strand T") auto
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 moura
  { 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 (set (transaction_fresh T)) (unlabel (duallsst (transaction_strand T)))" (is ?A)
    and "fv_transaction T ∩ bvars_transaction T = {}" (is ?B)
    and "set (transaction_fresh T) ∩ bvars_transaction T = {}" (is ?C)
proof -
  define T1 where "T1 ≡ unlabel (duallsst (transaction_receive T))"
  define T2 where "T2 ≡ unlabel (duallsst (transaction_selects T))"
  define T3 where "T3 ≡ unlabel (duallsst (transaction_checks T))"
  define T4 where "T4 ≡ unlabel (duallsst (transaction_updates T))"
  define T5 where "T5 ≡ unlabel (duallsst (transaction_send T))"

  define X where "X ≡ set (transaction_fresh T)"
  define Y where "Y ≡ X ∪ wfvarsoccssst T1"
  define Z where "Z ≡ Y ∪ wfvarsoccssst T2"

  define f where "f ≡ λS::(('a,'b,'c) prot_fun, ('a,'b,'c) prot_var) stateful_strand.
          ⋃((λx. case x of
            Receive t ⇒ fv t
          | Equality Assign _ t' ⇒ fv t'
          | Insert t t' ⇒ fv t ∪ fv t'
          | _ ⇒ {}) ` set S)"

  note defs1 = T1_def T2_def T3_def T4_def T5_def
  note defs2 = X_def Y_def Z_def
  note defs3 = f_def

  have 0: "wf'sst V (S @ S')"
    when "wf'sst V S" "f S' ⊆ wfvarsoccssst S ∪ V" for V S S'
    by (metis that wfsst_append_suffix' f_def)

  have 1: "unlabel (duallsst (transaction_strand T)) = T1@T2@T3@T4@T5"
    using duallsst_append unlabel_append unfolding transaction_strand_def defs1 by simp

  have 2:
      "∀x ∈ set T1. is_Send x" "∀x ∈ set T2. is_Assignment x" "∀x ∈ set T3. is_Check x"
      "∀x ∈ set T4. is_Update x" "∀x ∈ set T5. is_Receive x"
      "fvsst T3 ⊆ fvsst T1 ∪ fvsst T2" "fvsst T4 ∪ fvsst T5 ⊆ X ∪ fvsst T1 ∪ fvsst T2"
      "X ∩ fvsst T1 = {}" "X ∩ fvsst T2 = {}"
      "∀x ∈ set T2. is_Equality x ⟶ fv (the_rhs x) ⊆ fvsst T1"
    using T unfolding defs1 defs2 wellformed_transaction_def
    by (auto simp add: Ball_set duallsst_list_all fvsst_unlabel_duallsst_eq simp del: fvsst_def)

  have 3: "wf'sst X T1" using 2(1)
  proof (induction T1 arbitrary: X)
    case (Cons s T)
    obtain t where "s = send⟨t⟩" using Cons.prems by (cases s) moura+
    thus ?case using Cons by auto
  qed simp

  have 4: "f T1 = {}" "fvsst T1 = wfvarsoccssst T1" using 2(1)
  proof (induction T1)
    case (Cons s T)
    { case 1 thus ?case using Cons unfolding defs3 by (cases s) auto }
    { case 2 thus ?case using Cons unfolding defs3 wfvarsoccssst_def fvsst_def by (cases s) auto }
  qed (simp_all add: defs3 wfvarsoccssst_def fvsst_def)

  have 5: "f T2 ⊆ wfvarsoccssst T1" "fvsst T2 = f T2 ∪ wfvarsoccssst T2" using 2(2,10)
  proof (induction T2)
    case (Cons s T)
    { case 1 thus ?case using Cons
      proof (cases s)
        case (Equality ac t t') thus ?thesis using 1 Cons 4(2) unfolding defs3 by (cases ac) auto
      qed (simp_all add: defs3)
    }
    { case 2 thus ?case using Cons
      proof (cases s)
        case (Equality ac t t')
        hence "ac = Assign" "fvsstp s = fv t' ∪ wfvarsoccssstp s" "f (s#T) = fv t' ∪ f T"
          using 2 unfolding defs3 by auto
        moreover have "fvsst T = f T ∪ wfvarsoccssst T" using Cons.IH(2) 2 by auto
        ultimately show ?thesis unfolding wfvarsoccssst_def fvsst_def by auto
      next
        case (InSet ac t t')
        hence "ac = Assign" "fvsstp s = wfvarsoccssstp s" "f (s#T) = f T"
          using 2 unfolding defs3 by auto
        moreover have "fvsst T = f T ∪ wfvarsoccssst T" using Cons.IH(2) 2 by auto
        ultimately show ?thesis unfolding wfvarsoccssst_def fvsst_def by auto
      qed (simp_all add: defs3)
    }
  qed (simp_all add: defs3 wfvarsoccssst_def fvsst_def)

  have "f T ⊆ fvsst T" for T
  proof
    fix x show "x ∈ f T ⟹ x ∈ fvsst T"
    proof (induction T)
      case (Cons s T) thus ?case
      proof (cases "x ∈ f T")
        case False thus ?thesis
          using Cons.prems unfolding defs3 fvsst_def
          by (auto split: stateful_strand_step.splits poscheckvariant.splits)
      qed auto
    qed (simp add: defs3 fvsst_def)
  qed
  hence 6:
      "f T3 ⊆ X ∪ wfvarsoccssst T1 ∪ wfvarsoccssst T2"
      "f T4 ⊆ X ∪ wfvarsoccssst T1 ∪ wfvarsoccssst T2"
      "f T5 ⊆ X ∪ wfvarsoccssst T1 ∪ wfvarsoccssst T2"
    using 2(6,7) 4 5 by blast+

  have 7:
      "wfvarsoccssst T3 = {}"
      "wfvarsoccssst T4 = {}"
      "wfvarsoccssst T5 = {}"
    using 2(3,4,5) unfolding wfvarsoccssst_def
    by (auto split: stateful_strand_step.splits)

  have 8:
      "f T2 ⊆ wfvarsoccssst T1 ∪ X"
      "f T3 ⊆ wfvarsoccssst (T1@T2) ∪ X"
      "f T4 ⊆ wfvarsoccssst ((T1@T2)@T3) ∪ X"
      "f T5 ⊆ wfvarsoccssst (((T1@T2)@T3)@T4) ∪ X"
    using 4(1) 5(1) 6 7 wfvarsoccssst_append[of T1 T2]
          wfvarsoccssst_append[of "T1@T2" T3]
          wfvarsoccssst_append[of "(T1@T2)@T3" T4]
    by blast+
  
  have "wf'sst X (T1@T2@T3@T4@T5)"
    using 0[OF 0[OF 0[OF 0[OF 3 8(1)] 8(2)] 8(3)] 8(4)]
    unfolding Y_def Z_def by simp
  thus ?A using 1 unfolding defs1 defs2 by simp

  have "set (transaction_fresh T) ⊆ fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T)"
       "fv_transaction T ∩ bvars_transaction T = {}"
    using T unfolding wellformed_transaction_def by fast+
  thus ?B ?C using fv_transaction_unfold[of T] bvars_transaction_unfold[of T] by blast+
qed

lemma dual_wellformed_transaction_ident_cases'[dest]:
  assumes "wellformed_transaction T"
  shows "duallsst (transaction_selects T) = transaction_selects T"
        "duallsst (transaction_checks T) = transaction_checks T"
        "duallsst (transaction_updates T) = transaction_updates T"
using assms unfolding wellformed_transaction_def by auto

lemma dual_transaction_strand:
  assumes "wellformed_transaction T"
  shows "duallsst (transaction_strand T) =
         duallsst (transaction_receive T)@transaction_selects 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_selects 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_selects 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"
    hence "receive⟨t⟩ ∈ set (unlabel (duallsst (transaction_strand T)))" by (simp add: iksst_def)
    hence "send⟨t⟩ ∈ set (unlabel (transaction_strand T))"
      using duallsst_unlabel_steps_iff(1) by metis
    hence "t ∈ ?B" using wellformed_transaction_strand_unlabel_memberD(8)[OF assms] by force
  } moreover {
    fix t assume "t ∈ ?B"
    hence "send⟨t⟩ ∈ set (unlabel (transaction_send T))"
      using wellformed_transaction_unlabel_cases(5)[OF assms] by fastforce
    hence "receive⟨t⟩ ∈ set (unlabel (duallsst (transaction_send T)))"
      using duallsst_unlabel_steps_iff(1) by metis
    hence "receive⟨t⟩ ∈ set (unlabel (duallsst (transaction_strand T)))"
      using dual_unlabel_transaction_strand[OF assms] by simp 
    hence "t ∈ ?A" by (simp add: iksst_def)
  } ultimately show "?A = ?B" by auto
qed

lemma dual_transaction_ik_is_transaction_send':
  fixes δ::"('a,'b,'c) 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_selects T@transaction_checks T)"
  shows "dblsst A = dblsst (A@duallsst (S ⋅lsst δ))"
proof -
  let ?T1 = "transaction_receive T"
  let ?T2 = "transaction_selects T"
  let ?T3 = "transaction_checks T"

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

  have "list_all is_Receive (unlabel ?T1)"
       "list_all is_Assignment (unlabel ?T2)"
       "list_all is_Check (unlabel ?T3)"
    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"
        "∀b ∈ set (unlabel ?T3). ¬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,37),
        metis (mono_tags, lifting) Ball_set stateful_strand_step.distinct_disc(24,26,33,35,37,39))
  hence "∀b ∈ set (unlabel (?T1@?T2@?T3)). ¬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⟨t ⋅ θ⟩#unlabel (duallsst A ⋅lsst θ)"
    when "b = send⟨t⟩" for t
    by (simp add: a that subst_lsst_unlabel_cons)

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

  have 3: "unlabel (duallsst (a#A) ⋅lsst θ) = (b ⋅sstp θ)#unlabel (duallsst A ⋅lsst θ)"
    when "∄t. b = send⟨t⟩ ∨ b = receive⟨t⟩"
    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) moura+
  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(15) 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_fresh_vars_subset:
  assumes "wellformed_transaction T"
  shows "set (transaction_fresh T) ⊆ fv_transaction T"
using assms fv_transaction_unfold[of T]
unfolding wellformed_transaction_def
by auto

lemma transaction_fresh_vars_notin:
  assumes T: "wellformed_transaction T"
    and x: "x ∈ set (transaction_fresh T)"
  shows "x ∉ fvlsst (transaction_receive T)" (is ?A)
    and "x ∉ fvlsst (transaction_selects T)" (is ?B)
    and "x ∉ fvlsst (transaction_checks T)" (is ?C)
    and "x ∉ varslsst (transaction_receive T)" (is ?D)
    and "x ∉ varslsst (transaction_selects T)" (is ?E)
    and "x ∉ varslsst (transaction_checks T)" (is ?F)
    and "x ∉ bvarslsst (transaction_receive T)" (is ?G)
    and "x ∉ bvarslsst (transaction_selects T)" (is ?H)
    and "x ∉ bvarslsst (transaction_checks T)" (is ?I)
proof -
  have 0:
      "set (transaction_fresh T) ⊆ fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T)"
      "set (transaction_fresh T) ∩ fvlsst (transaction_receive T) = {}"
      "set (transaction_fresh T) ∩ fvlsst (transaction_selects T) = {}"
      "fv_transaction T ∩ bvars_transaction T = {}"
      "fvlsst (transaction_checks T) ⊆ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T)"
    using T unfolding wellformed_transaction_def
    by fast+
  
  have 1: "set (transaction_fresh T) ∩ bvarslsst (transaction_checks T) = {}"
    using 0(1,4) fv_transaction_unfold[of T] bvars_transaction_unfold[of T] by blast

  have 2:
      "varslsst (transaction_receive T) = fvlsst (transaction_receive T)"
      "varslsst (transaction_selects T) = fvlsst (transaction_selects T)"
      "bvarslsst (transaction_receive T) = {}"
      "bvarslsst (transaction_selects T) = {}"
    using bvars_wellformed_transaction_unfold[OF T] bvars_transaction_unfold[of T]
          varssst_is_fvsst_bvarssst[of "unlabel (transaction_receive T)"]
          varssst_is_fvsst_bvarssst[of "unlabel (transaction_selects T)"]
    by blast+
  
  show ?A ?B ?C ?D ?E ?G ?H ?I using 0 1 2 x by fast+

  show ?F using 0(2,3,5) 1 x varssst_is_fvsst_bvarssst[of "unlabel (transaction_checks T)"] by fast
qed


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_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 transaction_fresh_def 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

end

Theory Term_Abstraction

(*
(C) Copyright Andreas Viktor Hess, DTU, 2020
(C) Copyright Sebastian A. Mödersheim, DTU, 2020
(C) Copyright Achim D. Brucker, University of Exeter, 2020
(C) Copyright Anders Schlichtkrull, DTU, 2020

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      Term_Abstraction.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
*)

section‹Term Abstraction›
theory Term_Abstraction
  imports Transactions
begin

subsection ‹Definitions›
fun to_abs ("α0") where
  "α0 [] _ = {}"
| "α0 ((Fun (Val m) [],Fun (Set s) S)#D) n =
    (if m = n then insert s (α0 D n) else α0 D n)"
| "α0 (_#D) n = α0 D n"

fun abs_apply_term (infixl "⋅α" 67) where
  "Var x ⋅α α = Var x"
| "Fun (Val n) T ⋅α α = Fun (Abs (α n)) (map (λt. t ⋅α α) T)"
| "Fun f T ⋅α α = Fun f (map (λt. t ⋅α α) T)"

definition abs_apply_list (infixl "⋅αlist" 67) where
  "M ⋅αlist α ≡ map (λt. t ⋅α α) M"

definition abs_apply_terms (infixl "⋅αset" 67) where
  "M ⋅αset α ≡ (λt. t ⋅α α) ` M"

definition abs_apply_pairs (infixl "⋅αpairs" 67) where
  "F ⋅αpairs α ≡ map (λ(s,t). (s ⋅α α, t ⋅α α)) F"

definition abs_apply_strand_step (infixl "⋅αstp" 67) where
  "s ⋅αstp α ≡ (case s of
    (l,send⟨t⟩) ⇒ (l,send⟨t ⋅α α⟩)
  | (l,receive⟨t⟩) ⇒ (l,receive⟨t ⋅α α⟩)
  | (l,⟨ac: t ≐ t'⟩) ⇒ (l,⟨ac: (t ⋅α α) ≐ (t' ⋅α α)⟩)
  | (l,insert⟨t,t'⟩) ⇒ (l,insert⟨t ⋅α α,t' ⋅α α⟩)
  | (l,delete⟨t,t'⟩) ⇒ (l,delete⟨t ⋅α α,t' ⋅α α⟩)
  | (l,⟨ac: t ∈ t'⟩) ⇒ (l,⟨ac: (t ⋅α α) ∈ (t' ⋅α α)⟩)
  | (l,∀X⟨∨≠: F ∨∉: F'⟩) ⇒ (l,∀X⟨∨≠: (F ⋅αpairs α) ∨∉: (F' ⋅αpairs α)⟩))"

definition abs_apply_strand (infixl "⋅αst" 67) where
  "S ⋅αst α ≡ map (λx. x ⋅αstp α) S"


subsection ‹Lemmata›
lemma to_abs_alt_def:
  "α0 D n = {s. ∃S. (Fun (Val n) [], Fun (Set s) S) ∈ set D}"
by (induct D n rule: to_abs.induct) auto

lemma abs_term_apply_const[simp]:
  "is_Val f ⟹ Fun f [] ⋅α a = Fun (Abs (a (the_Val f))) []"
  "¬is_Val f ⟹ Fun f [] ⋅α a = Fun f []"
by (cases f; auto)+

lemma abs_fv: "fv (t ⋅α a) = fv t"
by (induct t a rule: abs_apply_term.induct) auto

lemma abs_eq_if_no_Val:
  assumes "∀f ∈ funs_term t. ¬is_Val f"
  shows "t ⋅α a = t ⋅α b"
using assms
proof (induction t)
  case (Fun f T) thus ?case by (cases f) simp_all
qed simp

lemma abs_list_set_is_set_abs_set: "set (M ⋅αlist α) = (set M) ⋅αset α"
unfolding abs_apply_list_def abs_apply_terms_def by simp

lemma abs_set_empty[simp]: "{} ⋅αset α = {}"
unfolding abs_apply_terms_def by simp

lemma abs_in:
  assumes "t ∈ M"
  shows "t ⋅α α ∈ M ⋅αset α"
using assms unfolding abs_apply_terms_def
by (induct t α rule: abs_apply_term.induct) blast+

lemma abs_set_union: "(A ∪ B) ⋅αset a = (A ⋅αset a) ∪ (B ⋅αset a)"
unfolding abs_apply_terms_def
by auto

lemma abs_subterms: "subterms (t ⋅α α) = subterms t ⋅αset α"
proof (induction t)
  case (Fun f T) thus ?case by (cases f) (auto simp add: abs_apply_terms_def)
qed (simp add: abs_apply_terms_def)

lemma abs_subterms_in: "s ∈ subterms t ⟹ s ⋅α a ∈ subterms (t ⋅α a)"
proof (induction t)
  case (Fun f T) thus ?case by (cases f) auto
qed simp

lemma abs_ik_append: "(iksst (A@B) ⋅set I) ⋅αset a = (iksst A ⋅set I) ⋅αset a ∪ (iksst B ⋅set I) ⋅αset a"
unfolding abs_apply_terms_def iksst_def
by auto

lemma to_abs_in:
  assumes "(Fun (Val n) [], Fun (Set s) []) ∈ set D"
  shows "s ∈ α0 D n"
using assms by (induct rule: to_abs.induct) auto

lemma to_abs_empty_iff_notin_db:
  "Fun (Val n) [] ⋅α α0 D = Fun (Abs {}) [] ⟷ (∄s S. (Fun (Val n) [], Fun (Set s) S) ∈ set D)"
by (simp add: to_abs_alt_def)

lemma to_abs_list_insert:
  assumes "Fun (Val n) [] ≠ t"
  shows "α0 D n = α0 (List.insert (t,s) D) n"
using assms to_abs_alt_def[of D n] to_abs_alt_def[of "List.insert (t,s) D" n]
by auto

lemma to_abs_list_insert':
  "insert s (α0 D n) = α0 (List.insert (Fun (Val n) [], Fun (Set s) S) D) n"
using to_abs_alt_def[of D n]
      to_abs_alt_def[of "List.insert (Fun (Val n) [], Fun (Set s) S) D" n]
by auto

lemma to_abs_list_remove_all:
  assumes "Fun (Val n) [] ≠ t"
  shows "α0 D n = α0 (List.removeAll (t,s) D) n"
using assms to_abs_alt_def[of D n] to_abs_alt_def[of "List.removeAll (t,s) D" n]
by auto

lemma to_abs_list_remove_all':
  "α0 D n - {s} = α0 (filter (λd. ∄S. d = (Fun (Val n) [], Fun (Set s) S)) D) n"
using to_abs_alt_def[of D n]
      to_abs_alt_def[of "filter (λd. ∄S. d = (Fun (Val n) [], Fun (Set s) S)) D" n]
by auto

lemma to_abs_dbsst_append:
  assumes "∀u s. insert⟨u, s⟩ ∈ set B ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
    and "∀u s. delete⟨u, s⟩ ∈ set B ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
  shows "α0 (db'sst A ℐ D) n = α0 (db'sst (A@B) ℐ D) n"
using assms
proof (induction B rule: List.rev_induct)
  case (snoc b B)
  hence IH: "α0 (db'sst A ℐ D) n = α0 (db'sst (A@B) ℐ D) n" by auto
  have *: "∀u s. b = insert⟨u,s⟩ ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
          "∀u s. b = delete⟨u,s⟩ ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
    using snoc.prems by simp_all
  show ?case
  proof (cases b)
    case (Insert u s)
    hence **: "db'sst (A@B@[b]) ℐ D = List.insert (u ⋅ ℐ,s ⋅ ℐ) (db'sst (A@B) ℐ D)"
      using dbsst_append[of "A@B" "[b]"] by simp
    have "Fun (Val n) [] ≠ u ⋅ ℐ" using *(1) Insert by auto
    thus ?thesis using IH ** to_abs_list_insert by metis
  next
    case (Delete u s)
    hence **: "db'sst (A@B@[b]) ℐ D = List.removeAll (u ⋅ ℐ,s ⋅ ℐ) (db'sst (A@B) ℐ D)"
      using dbsst_append[of "A@B" "[b]"] by simp
    have "Fun (Val n) [] ≠ u ⋅ ℐ" using *(2) Delete by auto
    thus ?thesis using IH ** to_abs_list_remove_all by metis
  qed (simp_all add: dbsst_no_upd_append[of "[b]" "A@B"] IH)
qed simp

lemma to_abs_neq_imp_db_update:
  assumes "α0 (dbsst A I) n ≠ α0 (dbsst (A@B) I) n"
  shows "∃u s. u ⋅ I = Fun (Val n) [] ∧ (insert⟨u,s⟩ ∈ set B ∨ delete⟨u,s⟩ ∈ set B)"
proof -
  { fix D have ?thesis when "α0 D n ≠ α0 (db'sst B I D) n" using that
    proof (induction B I D rule: db'sst.induct)
      case 2 thus ?case
        by (metis db'sst.simps(2) list.set_intros(1,2) subst_apply_pair_pair to_abs_list_insert)
    next
      case 3 thus ?case
        by (metis db'sst.simps(3) list.set_intros(1,2) subst_apply_pair_pair to_abs_list_remove_all)
    qed simp_all
  } thus ?thesis using assms by (metis dbsst_append dbsst_def)
qed

lemma abs_term_subst_eq:
  fixes δ θ::"(('a,'b,'c) prot_fun, ('d,'e prot_atom) term × nat) subst"
  assumes "∀x ∈ fv t. δ x ⋅α a = θ x ⋅α b"
    and "∄n T. Fun (Val n) T ∈ subterms t"
  shows "t ⋅ δ ⋅α a = t ⋅ θ ⋅α b"
using assms
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Val n)
    hence False using Fun.prems(2) by blast
    thus ?thesis by metis
  qed auto
qed simp

lemma abs_term_subst_eq':
  fixes δ θ::"(('a,'b,'c) prot_fun, ('d,'e prot_atom) term × nat) subst"
  assumes "∀x ∈ fv t. δ x ⋅α a = θ x"
    and "∄n T. Fun (Val n) T ∈ subterms t"
  shows "t ⋅ δ ⋅α a = t ⋅ θ"
using assms
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Val n)
    hence False using Fun.prems(2) by blast
    thus ?thesis by metis
  qed auto
qed simp

lemma abs_val_in_funs_term:
  assumes "f ∈ funs_term t" "is_Val f"
  shows "Abs (α (the_Val f)) ∈ funs_term (t ⋅α α)"
using assms by (induct t α rule: abs_apply_term.induct) auto

end

Theory Stateful_Protocol_Model

(*
(C) Copyright Andreas Viktor Hess, DTU, 2020
(C) Copyright Sebastian A. Mödersheim, DTU, 2020
(C) Copyright Achim D. Brucker, University of Exeter, 2020
(C) Copyright Anders Schlichtkrull, DTU, 2020

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      Stateful_Protocol_Model.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
*)

section‹Stateful Protocol Model›
theory Stateful_Protocol_Model
  imports Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
          Transactions Term_Abstraction
begin

subsection ‹Locale Setup›
locale stateful_protocol_model =
  fixes arityf::"'fun ⇒ nat"
    and aritys::"'sets ⇒ nat"
    and publicf::"'fun ⇒ bool"
    and Anaf::"'fun ⇒ ((('fun,'atom::finite,'sets) prot_fun, nat) term list × nat list)"
    and Γf::"'fun ⇒ 'atom option"
    and label_witness1::"'lbl"
    and label_witness2::"'lbl"
  assumes Anaf_assm1: "∀f. let (K, M) = Anaf f in (∀k ∈ subtermsset (set K).
      is_Fun k ⟶ (is_Fu (the_Fun k)) ∧ length (args k) = arityf (the_Fu (the_Fun k)))"
    and Anaf_assm2: "∀f. let (K, M) = Anaf f in ∀i ∈ fvset (set K) ∪ set M. i < arityf f"
    and publicf_assm: "∀f. arityf f > (0::nat) ⟶ publicf f"
    and Γf_assm: "∀f. arityf f = (0::nat) ⟶ Γf f ≠ None"
    and label_witness_assm: "label_witness1 ≠ label_witness2"
begin

lemma Anaf_assm1_alt: 
  assumes "Anaf f = (K,M)" "k ∈ subtermsset (set K)"
  shows "(∃x. k = Var x) ∨ (∃h T. k = Fun (Fu h) T ∧ length T = arityf h)"
proof (cases k)
  case (Fun g T)
  let ?P = "λk. is_Fun k ⟶ is_Fu (the_Fun k) ∧ length (args k) = arityf (the_Fu (the_Fun k))"
  let ?Q = "λK M. ∀k ∈ subtermsset (set K). ?P k"

  have "?Q (fst (Anaf f)) (snd (Anaf f))" using Anaf_assm1 split_beta[of ?Q "Anaf f"] by meson
  hence "?Q K M" using assms(1) by simp
  hence "?P k" using assms(2) by blast
  thus ?thesis using Fun by (cases g) auto
qed simp

lemma Anaf_assm2_alt:
  assumes "Anaf f = (K,M)" "i ∈ fvset (set K) ∪ set M"
  shows "i < arityf f"
using Anaf_assm2 assms by fastforce


subsection ‹Definitions›
fun arity where
  "arity (Fu f) = arityf f"
| "arity (Set s) = aritys s"
| "arity (Val _) = 0"
| "arity (Abs _) = 0"
| "arity Pair = 2"
| "arity (Attack _) = 0"
| "arity OccursFact = 2"
| "arity OccursSec = 0"
| "arity (PubConstAtom _ _) = 0"
| "arity (PubConstSetType _) = 0"
| "arity (PubConstAttackType _) = 0"
| "arity (PubConstBottom _) = 0"
| "arity (PubConstOccursSecType _) = 0"

fun public where
  "public (Fu f) = publicf f"
| "public (Set s) = (aritys s > 0)"
| "public (Val n) = snd n"
| "public (Abs _) = False"
| "public Pair = True"
| "public (Attack _) = False"
| "public OccursFact = True"
| "public OccursSec = False"
| "public (PubConstAtom _ _) = True"
| "public (PubConstSetType _) = True"
| "public (PubConstAttackType _) = True"
| "public (PubConstBottom _) = True" 
| "public (PubConstOccursSecType _) = True"

fun Ana where
  "Ana (Fun (Fu f) T) = (
    if arityf f = length T ∧ arityf f > 0
    then let (K,M) = Anaf f in (K ⋅list (!) T, map ((!) T) M)
    else ([], []))"
| "Ana _ = ([], [])"

definition Γv where
  "Γv v ≡ (
    if (∀t ∈ subterms (fst v).
          case t of (TComp f T) ⇒ arity f > 0 ∧ arity f = length T | _ ⇒ True)
    then fst v
    else TAtom Bottom)"

fun Γ where
  "Γ (Var v) = Γv v"
| "Γ (Fun f T) = (
    if arity f = 0
    then case f of
      (Fu g) ⇒ TAtom (case Γf g of Some a ⇒ Atom a | None ⇒ Bottom)
    | (Val _) ⇒ TAtom Value
    | (Abs _) ⇒ TAtom Value
    | (Set _) ⇒ TAtom SetType
    | (Attack _) ⇒ TAtom AttackType
    | OccursSec ⇒ TAtom OccursSecType
    | (PubConstAtom a _) ⇒ TAtom (Atom a)
    | (PubConstSetType _) ⇒ TAtom SetType
    | (PubConstAttackType _) ⇒ TAtom AttackType
    | (PubConstBottom _) ⇒ TAtom Bottom
    | (PubConstOccursSecType _) ⇒ TAtom OccursSecType
    | _ ⇒ TAtom Bottom
    else TComp f (map Γ T))"

lemma Γ_consts_simps[simp]:
  "arityf g = 0 ⟹ Γ (Fun (Fu g) []) = TAtom (case Γf g of Some a ⇒ Atom a | None ⇒ Bottom)"
  "Γ (Fun (Val n) []) = TAtom Value"
  "Γ (Fun (Abs b) []) = TAtom Value"
  "aritys s = 0 ⟹ Γ (Fun (Set s) []) = TAtom SetType"
  "Γ (Fun (Attack x) []) = TAtom AttackType"
  "Γ (Fun OccursSec []) = TAtom OccursSecType"
  "Γ (Fun (PubConstAtom a t) []) = TAtom (Atom a)"
  "Γ (Fun (PubConstSetType t) []) = TAtom SetType"
  "Γ (Fun (PubConstAttackType t) []) = TAtom AttackType"
  "Γ (Fun (PubConstBottom t) []) = TAtom Bottom"
  "Γ (Fun (PubConstOccursSecType t) []) = TAtom OccursSecType"
by simp+

lemma Γ_Set_simps[simp]:
  "aritys s ≠ 0 ⟹ Γ (Fun (Set s) T) = TComp (Set s) (map Γ T)"
  "Γ (Fun (Set s) T) = TAtom SetType ∨ Γ (Fun (Set s) T) = TComp (Set s) (map Γ T)"
  "Γ (Fun (Set s) T) ≠ TAtom Value"
  "Γ (Fun (Set s) T) ≠ TAtom (Atom a)"
  "Γ (Fun (Set s) T) ≠ TAtom AttackType"
  "Γ (Fun (Set s) T) ≠ TAtom OccursSecType"
  "Γ (Fun (Set s) T) ≠ TAtom Bottom"
by auto


subsection ‹Locale Interpretations›
lemma Ana_Fu_cases:
  assumes "Ana (Fun f T) = (K,M)"
    and "f = Fu g"
    and "Anaf g = (K',M')"
  shows "(K,M) = (if arityf g = length T ∧ arityf g > 0
                  then (K' ⋅list (!) T, map ((!) T) M')
                  else ([],[]))" (is ?A)
    and "(K,M) = (K' ⋅list (!) T, map ((!) T) M') ∨ (K,M) = ([],[])" (is ?B)
proof -
  show ?A using assms by (cases "arityf g = length T ∧ arityf g > 0") auto
  thus ?B by metis
qed

lemma Ana_Fu_intro:
  assumes "arityf f = length T" "arityf f > 0"
    and "Anaf f = (K',M')"
  shows "Ana (Fun (Fu f) T) = (K' ⋅list (!) T, map ((!) T) M')"
using assms by simp

lemma Ana_Fu_elim:
  assumes "Ana (Fun f T) = (K,M)"
    and "f = Fu g"
    and "Anaf g = (K',M')"
    and "(K,M) ≠ ([],[])"
  shows "arityf g = length T" (is ?A)
    and "(K,M) = (K' ⋅list (!) T, map ((!) T) M')" (is ?B)
proof -
  show ?A using assms by force
  moreover have "arityf g > 0" using assms by force
  ultimately show ?B using assms by auto
qed

lemma Ana_nonempty_inv:
  assumes "Ana t ≠ ([],[])"
  shows "∃f T. t = Fun (Fu f) T ∧ arityf f = length T ∧ arityf f > 0 ∧
               (∃K M. Anaf f = (K, M) ∧ Ana t = (K ⋅list (!) T, map ((!) T) M))"
using assms
proof (induction t rule: Ana.induct)
  case (1 f T)
  hence *: "arityf f = length T" "0 < arityf f"
           "Ana (Fun (Fu f) T) = (case Anaf f of (K, M) ⇒ (K ⋅list (!) T, map ((!) T) M))"
    using Ana.simps(1)[of f T] unfolding Let_def by metis+

  obtain K M where **: "Anaf f = (K, M)" by (metis surj_pair)
  hence "Ana (Fun (Fu f) T) = (K ⋅list (!) T, map ((!) T) M)" using *(3) by simp
  thus ?case using ** *(1,2) by blast
qed simp_all

lemma assm1:
  assumes "Ana t = (K,M)"
  shows "fvset (set K) ⊆ fv t"
using assms
proof (induction t rule: term.induct)
  case (Fun f T)
  have aux: "fvset (set K ⋅set (!) T) ⊆ fvset (set T)"
    when K: "∀i ∈ fvset (set K). i < length T"
    for K::"(('fun,'atom,'sets) prot_fun, nat) term list"
  proof
    fix x assume "x ∈ fvset (set K ⋅set (!) T)"
    then obtain k where k: "k ∈ set K" "x ∈ fv (k ⋅ (!) T)" by moura
    have "∀i ∈ fv k. i < length T" using K k(1) by simp
    thus "x ∈ fvset (set T)"
      by (metis (no_types, lifting) k(2) contra_subsetD fv_set_mono image_subsetI nth_mem
                                    subst_apply_fv_unfold)
  qed

  { fix g assume f: "f = Fu g" and K: "K ≠ []"
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have "(K, M) ≠ ([], [])" using K by simp
    hence "(K, M) = (K' ⋅list (!) T, map ((!) T) M')" "arityf g = length T"
      using Ana_Fu_cases(1)[OF Fun.prems f *]
      by presburger+
    hence ?case using aux[of K'] Anaf_assm2_alt[OF *] by auto
  } thus ?case using Fun by (cases f) fastforce+
qed simp

lemma assm2:
  assumes "Ana t = (K,M)"
  and "⋀g S'. Fun g S' ⊑ t ⟹ length S' = arity g"
  and "k ∈ set K"
  and "Fun f T' ⊑ k"
  shows "length T' = arity f"
using assms
proof (induction t rule: term.induct)
  case (Fun g T)
  obtain h where 2: "g = Fu h"
    using Fun.prems(1,3) by (cases g) auto
  obtain K' M' where 1: "Anaf h = (K',M')" by moura
  have "(K,M) ≠ ([],[])" using Fun.prems(3) by auto
  hence "(K,M) = (K' ⋅list (!) T, map ((!) T) M')"
        "⋀i. i ∈ fvset (set K') ∪ set M' ⟹ i < length T"
    using Ana_Fu_cases(1)[OF Fun.prems(1) 2 1] Anaf_assm2_alt[OF 1]
    by presburger+
  hence "K = K' ⋅list (!) T" and 3: "∀i∈fvset (set K'). i < length T" by simp_all
  then obtain k' where k': "k' ∈ set K'" "k = k' ⋅ (!) T" using Fun.prems(3) by moura
  hence 4: "Fun f T' ∈ subterms (k' ⋅ (!) T)" "fv k' ⊆ fvset (set K')"
    using Fun.prems(4) by auto
  show ?case
  proof (cases "∃i ∈ fv k'. Fun f T' ∈ subterms (T ! i)")
    case True
    hence "Fun f T' ∈ subtermsset (set T)" using k' Fun.prems(4) 3 by auto
    thus ?thesis using Fun.prems(2) by auto
  next
    case False
    then obtain S where "Fun f S ∈ subterms k'" "Fun f T' = Fun f S ⋅ (!) T"
      using k'(2) Fun.prems(4) subterm_subst_not_img_subterm by force
    thus ?thesis using Anaf_assm1_alt[OF 1, of "Fun f S"] k'(1) by (cases f) auto
  qed
qed simp

lemma assm4:
  assumes "Ana (Fun f T) = (K, M)"
  shows "set M ⊆ set T"
using assms
proof (cases f)
  case (Fu g)
  obtain K' M' where *: "Anaf g = (K',M')" by moura
  have "M = [] ∨ (arityf g = length T ∧ M = map ((!) T) M')"
    using Ana_Fu_cases(1)[OF assms Fu *]
    by (meson prod.inject)
  thus ?thesis using Anaf_assm2_alt[OF *] by auto
qed auto

lemma assm5: "Ana t = (K,M) ⟹ K ≠ [] ∨ M ≠ [] ⟹ Ana (t ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
proof (induction t rule: term.induct)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Fu g)
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have **: "K = K' ⋅list (!) T" "M = map ((!) T) M'"
             "arityf g = length T" "∀i ∈ fvset (set K') ∪ set M'. i < arityf g" "0 < arityf g"
      using Fun.prems(2) Ana_Fu_cases(1)[OF Fun.prems(1) Fu *] Anaf_assm2_alt[OF *]
      by (meson prod.inject)+

    have ***: "∀i ∈ fvset (set K'). i < length T" "∀i ∈ set M'. i < length T" using **(3,4) by auto
    
    have "K ⋅list δ = K' ⋅list (!) (map (λt. t ⋅ δ) T)"
         "M ⋅list δ = map ((!) (map (λt. t ⋅ δ) T)) M'"
      using subst_idx_map[OF ***(2), of δ]
            subst_idx_map'[OF ***(1), of δ]
            **(1,2)
      by fast+
    thus ?thesis using Fu * **(3,5) by auto
  qed auto
qed simp

sublocale intruder_model arity public Ana
apply unfold_locales
by (metis assm1, metis assm2, rule Ana.simps, metis assm4, metis assm5)

adhoc_overloading INTRUDER_SYNTH intruder_synth
adhoc_overloading INTRUDER_DEDUCT intruder_deduct

lemma assm6: "arity c = 0 ⟹ ∃a. ∀X. Γ (Fun c X) = TAtom a" by (cases c) auto

lemma assm7: "0 < arity f ⟹ Γ (Fun f T) = TComp f (map Γ T)" by auto

lemma assm8: "infinite {c. Γ (Fun c []::('fun,'atom,'sets) prot_term) = TAtom a ∧ public c}"
  (is "?P a")
proof -
  let ?T = "λf. (range f)::('fun,'atom,'sets) prot_fun set"
  let ?A = "λf. ∀x::nat ∈ UNIV. ∀y::nat ∈ UNIV. (f x = f y) = (x = y)"
  let ?B = "λf. ∀x::nat ∈ UNIV. f x ∈ ?T f"
  let ?C = "λf. ∀y::('fun,'atom,'sets) prot_fun ∈ ?T f. ∃x ∈ UNIV. y = f x"
  let ?D = "λf b. ?T f ⊆ {c. Γ (Fun c []::('fun,'atom,'sets) prot_term) = TAtom b ∧ public c}"

  have sub_lmm: "?P b" when "?A f" "?C f" "?C f" "?D f b" for b f
  proof -
    have "∃g::nat ⇒ ('fun,'atom,'sets) prot_fun. bij_betw g UNIV (?T f)"
      using bij_betwI'[of UNIV f "?T f"] that(1,2,3) by blast
    hence "infinite (?T f)" by (metis nat_not_finite bij_betw_finite)
    thus ?thesis using infinite_super[OF that(4)] by blast
  qed

  show ?thesis
  proof (cases a)
    case (Atom b) thus ?thesis using sub_lmm[of "PubConstAtom b" a] by force
  next
    case Value thus ?thesis using sub_lmm[of "λn. Val (n,True)" a] by force
  next
    case SetType thus ?thesis using sub_lmm[of PubConstSetType a] by fastforce
  next
    case AttackType thus ?thesis using sub_lmm[of PubConstAttackType a] by fastforce
  next
    case Bottom thus ?thesis using sub_lmm[of PubConstBottom a] by fastforce
  next
    case OccursSecType thus ?thesis using sub_lmm[of PubConstOccursSecType a] by fastforce
  qed
qed

lemma assm9: "TComp f T ⊑ Γ t ⟹ arity f > 0"
proof (induction t rule: term.induct)
  case (Var x)
  hence "Γ (Var x) ≠ TAtom Bottom" by force
  hence "∀t ∈ subterms (fst x). case t of
            TComp f T ⇒ arity f > 0 ∧ arity f = length T
          | _ ⇒ True"
    using Var Γ.simps(1)[of x] unfolding Γv_def by meson
  thus ?case using Var by (fastforce simp add: Γv_def)
next
  case (Fun g S)
  have "arity g ≠ 0" using Fun.prems Var_subtermeq assm6 by force
  thus ?case using Fun by (cases "TComp f T = TComp g (map Γ S)") auto
qed

lemma assm10: "wftrm (Γ (Var x))"
unfolding wftrm_def by (auto simp add: Γv_def)

lemma assm11: "arity f > 0 ⟹ public f" using publicf_assm by (cases f) auto

lemma assm12: "Γ (Var (τ, n)) = Γ (Var (τ, m))" by (simp add: Γv_def)

lemma assm13: "arity c = 0 ⟹ Ana (Fun c T) = ([],[])" by (cases c) simp_all

lemma assm14:
  assumes "Ana (Fun f T) = (K,M)"
  shows "Ana (Fun f T ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
proof -
  show ?thesis
  proof (cases "(K, M) = ([],[])")
    case True
    { fix g assume f: "f = Fu g"
      obtain K' M' where "Anaf g = (K',M')" by moura
      hence ?thesis using assms f True by auto
    } thus ?thesis using True assms by (cases f) auto
  next
    case False
    then obtain g where **: "f = Fu g" using assms by (cases f) auto
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have ***: "K = K' ⋅list (!) T" "M = map ((!) T) M'" "arityf g = length T"
              "∀i ∈ fvset (set K') ∪ set M'. i < arityf g"
      using Ana_Fu_cases(1)[OF assms ** *] False Anaf_assm2_alt[OF *]
      by (meson prod.inject)+
    have ****: "∀i∈fvset (set K'). i < length T" "∀i∈set M'. i < length T" using ***(3,4) by auto
    have "K ⋅list δ = K' ⋅list (!) (map (λt. t ⋅ δ) T)"
         "M ⋅list δ = map ((!) (map (λt. t ⋅ δ) T)) M'"
      using subst_idx_map[OF ****(2), of δ]
            subst_idx_map'[OF ****(1), of δ]
            ***(1,2)
      by auto
    thus ?thesis using assms * ** ***(3) by auto
  qed
qed

sublocale labeled_stateful_typed_model' arity public Ana Γ Pair label_witness1 label_witness2
by unfold_locales
   (metis assm6, metis assm7, metis assm8, metis assm9,
    rule assm10, metis assm11, rule arity.simps(5), metis assm14,
    metis assm12, metis assm13, metis assm14, rule label_witness_assm)

subsection ‹Minor Lemmata›
lemma Γv_TAtom[simp]: "Γv (TAtom a, n) = TAtom a"
unfolding Γv_def by simp

lemma Γv_TAtom':
  assumes "a ≠ Bottom"
  shows "Γv (τ, n) = TAtom a ⟷ τ = TAtom a"
proof
  assume "Γv (τ, n) = TAtom a"
  thus "τ = TAtom a" by (metis (no_types, lifting) assms Γv_def fst_conv term.inject(1)) 
qed simp

lemma Γv_TAtom_inv:
  "Γv x = TAtom (Atom a) ⟹ ∃m. x = (TAtom (Atom a), m)"
  "Γv x = TAtom Value ⟹ ∃m. x = (TAtom Value, m)"
  "Γv x = TAtom SetType ⟹ ∃m. x = (TAtom SetType, m)"
  "Γv x = TAtom AttackType ⟹ ∃m. x = (TAtom AttackType, m)"
  "Γv x = TAtom OccursSecType ⟹ ∃m. x = (TAtom OccursSecType, m)"
by (metis Γv_TAtom' surj_pair prot_atom.distinct(7),
    metis Γv_TAtom' surj_pair prot_atom.distinct(15),
    metis Γv_TAtom' surj_pair prot_atom.distinct(21),
    metis Γv_TAtom' surj_pair prot_atom.distinct(25),
    metis Γv_TAtom' surj_pair prot_atom.distinct(30))

lemma Γv_TAtom'':
  "(fst x = TAtom (Atom a)) = (Γv x = TAtom (Atom a))" (is "?A = ?A'")
  "(fst x = TAtom Value) = (Γv x = TAtom Value)" (is "?B = ?B'")
  "(fst x = TAtom SetType) = (Γv x = TAtom SetType)" (is "?C = ?C'")
  "(fst x = TAtom AttackType) = (Γv x = TAtom AttackType)" (is "?D = ?D'")
  "(fst x = TAtom OccursSecType) = (Γv x = TAtom OccursSecType)" (is "?E = ?E'")
proof -
  have 1: "?A ⟹ ?A'" "?B ⟹ ?B'" "?C ⟹ ?C'" "?D ⟹ ?D'" "?E ⟹ ?E'"
    by (metis Γv_TAtom prod.collapse)+

  have 2: "?A' ⟹ ?A" "?B' ⟹ ?B" "?C' ⟹ ?C" "?D' ⟹ ?D" "?E' ⟹ ?E"
    using Γv_TAtom Γv_TAtom_inv(1) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(2) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(3) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(4) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(5) by fastforce

  show "?A = ?A'" "?B = ?B'" "?C = ?C'" "?D = ?D'" "?E = ?E'"
    using 1 2 by metis+
qed

lemma Γv_Var_image:
  "Γv ` X = Γ ` Var ` X"
by force

lemma Γ_Fu_const:
  assumes "arityf g = 0"
  shows "∃a. Γ (Fun (Fu g) T) = TAtom (Atom a)"
proof -
  have "Γf g ≠ None" using assms Γf_assm by blast
  thus ?thesis using assms by force
qed

lemma Fun_Value_type_inv:
  fixes T::"('fun,'atom,'sets) prot_term list"
  assumes "Γ (Fun f T) = TAtom Value"
  shows "(∃n. f = Val n) ∨ (∃bs. f = Abs bs)"
proof -
  have *: "arity f = 0" by (metis const_type_inv assms) 
  show ?thesis  using assms
  proof (cases f)
    case (Fu g)
    hence "arityf g = 0" using * by simp
    hence False using Fu Γ_Fu_const[of g T] assms by auto
    thus ?thesis by metis
  next
    case (Set s)
    hence "aritys s = 0" using * by simp
    hence False using Set assms by auto
    thus ?thesis by metis
  qed simp_all
qed

lemma abs_Γ: "Γ t = Γ (t ⋅α α)"
by (induct t α rule: abs_apply_term.induct) auto

lemma Anaf_keys_not_pubval_terms:
  assumes "Anaf f = (K, T)"
    and "k ∈ set K"
    and "g ∈ funs_term k"
  shows "¬is_Val g"
proof
  assume "is_Val g"
  then obtain n S where *: "Fun (Val n) S ∈ subtermsset (set K)"
    using assms(2) funs_term_Fun_subterm[OF assms(3)]
    by (cases g) auto
  show False using Anaf_assm1_alt[OF assms(1) *] by simp
qed

lemma Anaf_keys_not_abs_terms:
  assumes "Anaf f = (K, T)"
    and "k ∈ set K"
    and "g ∈ funs_term k"
  shows "¬is_Abs g"
proof
  assume "is_Abs g"
  then obtain a S where *: "Fun (Abs a) S ∈ subtermsset (set K)"
    using assms(2) funs_term_Fun_subterm[OF assms(3)]
    by (cases g) auto
  show False using Anaf_assm1_alt[OF assms(1) *] by simp
qed

lemma Anaf_keys_not_pairs:
  assumes "Anaf f = (K, T)"
    and "k ∈ set K"
    and "g ∈ funs_term k"
  shows "g ≠ Pair"
proof
  assume "g = Pair"
  then obtain S where *: "Fun Pair S ∈ subtermsset (set K)"
    using assms(2) funs_term_Fun_subterm[OF assms(3)]
    by (cases g) auto
  show False using Anaf_assm1_alt[OF assms(1) *] by simp
qed

lemma Ana_Fu_keys_funs_term_subset:
  fixes K::"('fun,'atom,'sets) prot_term list"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
  shows "⋃(funs_term ` set K) ⊆ ⋃(funs_term ` set K') ∪ funs_term (Fun (Fu f) S)"
proof -
  { fix k assume k: "k ∈ set K"
    then obtain k' where k':
        "k' ∈ set K'" "k = k' ⋅ (!) S" "arityf f = length S"
        "subterms k' ⊆ subtermsset (set K')"
      using assms Ana_Fu_elim[OF assms(1) _ assms(2)] by fastforce

    have 1: "funs_term k' ⊆ ⋃(funs_term ` set K')" using k'(1) by auto

    have "i < length S" when "i ∈ fv k'" for i
      using that Anaf_assm2_alt[OF assms(2), of i] k'(1,3)
      by auto
    hence 2: "funs_term (S ! i) ⊆ funs_term (Fun (Fu f) S)" when "i ∈ fv k'" for i
      using that by force
  
    have "funs_term k ⊆ ⋃(funs_term ` set K') ∪ funs_term (Fun (Fu f) S)"
      using funs_term_subst[of k' "(!) S"] k'(2) 1 2 by fast
  } thus ?thesis by blast
qed

lemma Ana_Fu_keys_not_pubval_terms:
  fixes k::"('fun,'atom,'sets) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). is_Val g ⟶ ¬public g"
  shows "∀g ∈ funs_term k. is_Val g ⟶ ¬public g"
using assms(3,4) Anaf_keys_not_pubval_terms[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma Ana_Fu_keys_not_abs_terms:
  fixes k::"('fun,'atom,'sets) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). ¬is_Abs g"
  shows "∀g ∈ funs_term k. ¬is_Abs g"
using assms(3,4) Anaf_keys_not_abs_terms[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma Ana_Fu_keys_not_pairs:
  fixes k::"('fun,'atom,'sets) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). g ≠ Pair"
  shows "∀g ∈ funs_term k. g ≠ Pair"
using assms(3,4) Anaf_keys_not_pairs[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma deduct_occurs_in_ik:
  fixes t::"('fun,'atom,'sets) prot_term"
  assumes t: "M ⊢ occurs t"
    and M: "∀s ∈ subtermsset M. OccursFact ∉ ⋃(funs_term ` set (snd (Ana s)))"
           "∀s ∈ subtermsset M. OccursSec ∉ ⋃(funs_term ` set (snd (Ana s)))"
           "Fun OccursSec [] ∉ M"
  shows "occurs t ∈ M"
using private_fun_deduct_in_ik''[of M OccursFact "[Fun OccursSec [], t]" OccursSec] t M 
by fastforce

lemma wellformed_transaction_sem_receives:
  fixes T::"('fun,'atom,'sets,'lbl) prot_transaction"
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and s: "receive⟨t⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
  shows "IK ⊢ t ⋅ ℐ"
proof -
  let ?R = "unlabel (duallsst (transaction_receive T ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)"

  obtain l B s where B:
      "(l,send⟨t⟩) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (transaction_receive T ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(2)[of t "transaction_receive T ⋅lsst θ"]
          duallsst_in_set_prefix_obtain_subst[of "send⟨t⟩" "transaction_receive T" θ]
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[send⟨t⟩]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps )

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[send⟨t⟩]) ℐ"
    using B 1 unfolding prefix_def unlabel_def
    by (metis duallsst_def map_append strand_sem_append_stateful) 
  hence t_deduct: "IK ∪ (iklsst (duallsst (B ⋅lsst θ)) ⋅set ℐ) ⊢ t ⋅ ℐ"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[send⟨t⟩]" ℐ]
    by simp

  have "∀s ∈ set (unlabel (transaction_receive T)). ∃t. s = receive⟨t⟩"
    using T_valid wellformed_transaction_unlabel_cases(1)[OF T_valid] by auto
  moreover { fix A::"('fun,'atom,'sets,'lbl) prot_strand" and θ
    assume "∀s ∈ set (unlabel A). ∃t. s = receive⟨t⟩"
    hence "∀s ∈ set (unlabel (A ⋅lsst θ)). ∃t. s = receive⟨t⟩"
    proof (induction A)
      case (Cons a A) thus ?case using subst_lsst_cons[of a A θ] by (cases a) auto
    qed simp
    hence "∀s ∈ set (unlabel (A ⋅lsst θ)). ∃t. s = receive⟨t⟩"
      by (simp add: list.pred_set is_Receive_def)
    hence "∀s ∈ set (unlabel (duallsst (A ⋅lsst θ))). ∃t. s = send⟨t⟩"
      by (metis duallsst_memberD duallsstp_inv(2) unlabel_in unlabel_mem_has_label)
  }
  ultimately have "∀s ∈ set ?R. ∃t. s = send⟨t⟩" by simp
  hence "iksst ?R = {}" unfolding unlabel_def iksst_def by fast
  hence "iklsst (duallsst (B ⋅lsst θ)) = {}"
    using B(2) 1 iksst_append duallsst_append
    by (metis (no_types, lifting) Un_empty map_append prefix_def unlabel_def) 
  thus ?thesis using t_deduct by simp
qed

lemma wellformed_transaction_sem_selects:
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and "select⟨t,u⟩ ∈ set (unlabel (transaction_selects T ⋅lsst θ))"
  shows "(t ⋅ ℐ, u ⋅ ℐ) ∈ DB"
proof -
  let ?s = "select⟨t,u⟩"
  let ?R = "transaction_receive T@transaction_selects T"
  let ?R' = "unlabel (duallsst (?R ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)@?S (transaction_selects T)"
  let ?P = "λa. is_Receive a ∨ is_Assignment a"
  let ?Q = "λa. is_Send a ∨ is_Assignment a"

  have s: "?s ∈ set (unlabel (?R ⋅lsst θ))"
    using assms(3) subst_lsst_append[of "transaction_receive T"]
          unlabel_append[of "transaction_receive T ⋅lsst θ"]
    by auto

  obtain l B s where B:
      "(l,?s) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (?R ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(6)[of assign t u]
          duallsst_in_set_prefix_obtain_subst[of ?s ?R θ] 
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[?s]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps)

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[?s]) ℐ"
    using B 1 strand_sem_append_stateful subst_lsst_append
    unfolding prefix_def unlabel_def duallsst_def
    by (metis (no_types) map_append)
  hence in_db: "(t ⋅ ℐ, u ⋅ ℐ) ∈ dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[?s]" ℐ]
    by simp
  
  have "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ?Q a"
  proof
    fix a assume a: "a ∈ set (unlabel (duallsst (B ⋅lsst θ)))"

    have "∀a ∈ set (unlabel ?R). ?P a"
      using wellformed_transaction_unlabel_cases(1)[OF T_valid]
            wellformed_transaction_unlabel_cases(2)[OF T_valid]
      unfolding unlabel_def
      by fastforce
    hence "∀a ∈ set (unlabel (?R ⋅lsst θ)). ?P a"
      using stateful_strand_step_cases_subst(2,8)[of _ θ] subst_lsst_unlabel[of ?R θ]
      by (simp add: subst_apply_stateful_strand_def del: unlabel_append)
    hence B_P: "∀a ∈ set (unlabel (B ⋅lsst θ)). ?P a"
      using unlabel_mono[OF set_mono_prefix[OF append_prefixD[OF B(2)]]]
      by blast

    obtain l where "(l,a) ∈ set (duallsst (B ⋅lsst θ))"
      using a by (meson unlabel_mem_has_label)
    then obtain b where b: "(l,b) ∈ set (B ⋅lsst θ)" "duallsstp (l,b) = (l,a)"
      using duallsst_memberD by blast
    hence "?P b" using B_P unfolding unlabel_def by fastforce
    thus "?Q a" using duallsstp_inv[OF b(2)] by (cases b) auto
  qed
  hence "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ¬is_Insert a ∧ ¬is_Delete a" by fastforce
  thus ?thesis using dbupdsst_no_upd[of "unlabel (duallsst (B ⋅lsst θ))" ℐ DB] in_db by simp
qed

lemma wellformed_transaction_sem_pos_checks:
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and "⟨t in u⟩ ∈ set (unlabel (transaction_checks T ⋅lsst θ))"
  shows "(t ⋅ ℐ, u ⋅ ℐ) ∈ DB"
proof -
  let ?s = "⟨t in u⟩"
  let ?R = "transaction_receive T@transaction_selects T@transaction_checks T"
  let ?R' = "unlabel (duallsst (?R ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)@?S (transaction_selects T)@?S (transaction_checks T)"
  let ?P = "λa. is_Receive a ∨ is_Assignment a ∨ is_Check a"
  let ?Q = "λa. is_Send a ∨ is_Assignment a ∨ is_Check a"

  have s: "?s ∈ set (unlabel (?R ⋅lsst θ))"
    using assms(3) subst_lsst_append[of "transaction_receive T@transaction_selects T"]
          unlabel_append[of "transaction_receive T@transaction_selects T ⋅lsst θ"]
    by auto

  obtain l B s where B:
      "(l,?s) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (?R ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(6)[of check t u]
          duallsst_in_set_prefix_obtain_subst[of ?s ?R θ] 
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[?s]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps )

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[?s]) ℐ"
    using B 1 strand_sem_append_stateful subst_lsst_append
    unfolding prefix_def unlabel_def duallsst_def
    by (metis (no_types) map_append)
  hence in_db: "(t ⋅ ℐ, u ⋅ ℐ) ∈ dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[?s]" ℐ]
    by simp
  
  have "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ?Q a"
  proof
    fix a assume a: "a ∈ set (unlabel (duallsst (B ⋅lsst θ)))"

    have "∀a ∈ set (unlabel ?R). ?P a"
      using wellformed_transaction_unlabel_cases(1,2,3)[OF T_valid]
      unfolding unlabel_def
      by fastforce
    hence "∀a ∈ set (unlabel (?R ⋅lsst θ)). ?P a"
      using stateful_strand_step_cases_subst(2,8,9)[of _ θ] subst_lsst_unlabel[of ?R θ]
      by (simp add: subst_apply_stateful_strand_def del: unlabel_append)
    hence B_P: "∀a ∈ set (unlabel (B ⋅lsst θ)). ?P a"
      using unlabel_mono[OF set_mono_prefix[OF append_prefixD[OF B(2)]]]
      by blast

    obtain l where "(l,a) ∈ set (duallsst (B ⋅lsst θ))"
      using a by (meson unlabel_mem_has_label)
    then obtain b where b: "(l,b) ∈ set (B ⋅lsst θ)" "duallsstp (l,b) = (l,a)"
      using duallsst_memberD by blast
    hence "?P b" using B_P unfolding unlabel_def by fastforce
    thus "?Q a" using duallsstp_inv[OF b(2)] by (cases b) auto
  qed
  hence "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ¬is_Insert a ∧ ¬is_Delete a" by fastforce
  thus ?thesis using dbupdsst_no_upd[of "unlabel (duallsst (B ⋅lsst θ))" ℐ DB] in_db by simp
qed

lemma wellformed_transaction_sem_neg_checks:
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and "NegChecks X [] [(t,u)] ∈ set (unlabel (transaction_checks T ⋅lsst θ))"
  shows "∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ (t ⋅ δ ⋅ ℐ, u ⋅ δ ⋅ ℐ) ∉ DB" (is ?A)
    and "X = [] ⟹ (t ⋅ ℐ, u ⋅ ℐ) ∉ DB" (is "?B ⟹ ?B'")
proof -
  let ?s = "NegChecks X [] [(t,u)]"
  let ?R = "transaction_receive T@transaction_selects T@transaction_checks T"
  let ?R' = "unlabel (duallsst (?R ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)@?S (transaction_selects T)@?S (transaction_checks T)"
  let ?P = "λa. is_Receive a ∨ is_Assignment a ∨ is_Check a"
  let ?Q = "λa. is_Send a ∨ is_Assignment a ∨ is_Check a"
  let ?U = "λδ. subst_domain δ = set X ∧ ground (subst_range δ)"

  have s: "?s ∈ set (unlabel (?R ⋅lsst θ))"
    using assms(3) subst_lsst_append[of "transaction_receive T@transaction_selects T"]
          unlabel_append[of "transaction_receive T@transaction_selects T ⋅lsst θ"]
    by auto

  obtain l B s where B:
      "(l,?s) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (?R ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(7)[of X "[]" "[(t,u)]"]
          duallsst_in_set_prefix_obtain_subst[of ?s ?R θ]
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[?s]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps)

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[?s]) ℐ"
    using B 1 strand_sem_append_stateful subst_lsst_append
    unfolding prefix_def unlabel_def duallsst_def
    by (metis (no_types) map_append)
  hence "negchecks_model ℐ (dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB) X [] [(t,u)]"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[?s]" ℐ]
    by fastforce
  hence in_db: "∀δ. ?U δ ⟶ (t ⋅ δ ⋅ ℐ, u ⋅ δ ⋅ ℐ) ∉ dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB"
    unfolding negchecks_model_def
    by simp

  have "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ?Q a"
  proof
    fix a assume a: "a ∈ set (unlabel (duallsst (B ⋅lsst θ)))"

    have "∀a ∈ set (unlabel ?R). ?P a"
      using wellformed_transaction_unlabel_cases(1,2,3)[OF T_valid]
      unfolding unlabel_def
      by fastforce
    hence "∀a ∈ set (unlabel (?R ⋅lsst θ)). ?P a"
      using stateful_strand_step_cases_subst(2,8,9)[of _ θ] subst_lsst_unlabel[of ?R θ]
      by (simp add: subst_apply_stateful_strand_def del: unlabel_append)
    hence B_P: "∀a ∈ set (unlabel (B ⋅lsst θ)). ?P a"
      using unlabel_mono[OF set_mono_prefix[OF append_prefixD[OF B(2)]]]
      by blast

    obtain l where "(l,a) ∈ set (duallsst (B ⋅lsst θ))"
      using a by (meson unlabel_mem_has_label)
    then obtain b where b: "(l,b) ∈ set (B ⋅lsst θ)" "duallsstp (l,b) = (l,a)"
      using duallsst_memberD by blast
    hence "?P b" using B_P unfolding unlabel_def by fastforce
    thus "?Q a" using duallsstp_inv[OF b(2)] by (cases b) auto
  qed
  hence "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ¬is_Insert a ∧ ¬is_Delete a" by fastforce
  thus ?A using dbupdsst_no_upd[of "unlabel (duallsst (B ⋅lsst θ))" ℐ DB] in_db by simp
  moreover have "δ = Var" "t ⋅ δ = t"
    when "subst_domain δ = set []" for t and δ::"('fun, 'atom, 'sets) prot_subst"
    using that by auto
  moreover have "subst_domain Var = set []" "range_vars Var = {}"
    by simp_all
  ultimately show "?B ⟹ ?B'" unfolding range_vars_alt_def by metis
qed

lemma wellformed_transaction_fv_in_receives_or_selects:
  assumes T: "wellformed_transaction T"
    and x: "x ∈ fv_transaction T" "x ∉ set (transaction_fresh T)"
  shows "x ∈ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T)"
proof -
  have "x ∈ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T) ∪
            fvlsst (transaction_checks T) ∪ fvlsst (transaction_updates T) ∪
            fvlsst (transaction_send T)"
    using x(1) fvsst_append unlabel_append 
    by (metis transaction_strand_def append_assoc)
  thus ?thesis using T x(2) unfolding wellformed_transaction_def by blast
qed

lemma dual_transaction_ik_is_transaction_send'':
  fixes δ ℐ::"('a,'b,'c) prot_subst"
  assumes "wellformed_transaction T"
  shows "(iksst (unlabel (duallsst (transaction_strand T ⋅lsst δ))) ⋅set ℐ) ⋅αset a =
         (trmssst (unlabel (transaction_send T)) ⋅set δ ⋅set ℐ) ⋅αset a" (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 simp add: abs_apply_terms_def)

lemma while_prot_terms_fun_mono:
  "mono (λM'. M ∪ ⋃(subterms ` M') ∪ ⋃((set ∘ fst ∘ Ana) ` M'))"
unfolding mono_def by fast

lemma while_prot_terms_SMP_overapprox:
  fixes M::"('fun,'atom,'sets) prot_terms"
  assumes N_supset: "M ∪ ⋃(subterms ` N) ∪ ⋃((set ∘ fst ∘ Ana) ` N) ⊆ N"
    and Value_vars_only: "∀x ∈ fvset N. Γv x = TAtom Value"
  shows "SMP M ⊆ {a ⋅ δ | a δ. a ∈ N ∧ wtsubst δ ∧ wftrms (subst_range δ)}"
proof -
  define f where "f ≡ λM'. M ∪ ⋃(subterms ` M') ∪ ⋃((set ∘ fst ∘ Ana) ` M')"
  define S where "S ≡ {a ⋅ δ | a δ. a ∈ N ∧ wtsubst δ ∧ wftrms (subst_range δ)}"

  note 0 = Value_vars_only
  
  have "t ∈ S" when "t ∈ SMP M" for t
  using that
  proof (induction t rule: SMP.induct)
    case (MP t)
    hence "t ∈ N" "wtsubst Var" "wftrms (subst_range Var)" using N_supset by auto
    hence "t ⋅ Var ∈ S" unfolding S_def by blast
    thus ?case by simp
  next
    case (Subterm t t')
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    hence "∀x ∈ fv a. ∃τ. Γ (Var x) = TAtom τ" using 0 by auto
    hence *: "∀x ∈ fv a. (∃f. δ x = Fun f []) ∨ (∃y. δ x = Var y)"
      using a(3) TAtom_term_cases[OF wf_trm_subst_rangeD[OF a(4)]]
      by (metis wtsubst_def)
    obtain b where b: "b ⋅ δ = t'" "b ∈ subterms a"
      using subterms_subst_subterm[OF *, of t'] Subterm.hyps(2) a(1)
      by fast
    hence "b ∈ N" using N_supset a(2) by blast
    thus ?case using a b(1) unfolding S_def by blast
  next
    case (Substitution t θ)
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    have "wtsubst (δ ∘s θ)" "wftrms (subst_range (δ ∘s θ))"
      by (fact wt_subst_compose[OF a(3) Substitution.hyps(2)],
          fact wf_trms_subst_compose[OF a(4) Substitution.hyps(3)])
    moreover have "t ⋅ θ = a ⋅ δ ∘s θ" using a(1) subst_subst_compose[of a δ θ] by simp
    ultimately show ?case using a(2) unfolding S_def by blast
  next
    case (Ana t K T k)
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    obtain Ka Ta where a': "Ana a = (Ka,Ta)" by moura
    have *: "K = Ka ⋅list δ"
    proof (cases a)
      case (Var x)
      then obtain g U where gU: "t = Fun g U"
        using a(1) Ana.hyps(2,3) Ana_var
        by (cases t) simp_all
      have "Γ (Var x) = TAtom Value" using Var a(2) 0 by auto
      hence "Γ (Fun g U) = TAtom Value"
        using a(1,3) Var gU wt_subst_trm''[OF a(3), of a]
        by argo
      thus ?thesis using gU Fun_Value_type_inv Ana.hyps(2,3) by fastforce  
    next
      case (Fun g U) thus ?thesis using a(1) a' Ana.hyps(2) Ana_subst'[of g U] by simp
    qed
    then obtain ka where ka: "k = ka ⋅ δ" "ka ∈ set Ka" using Ana.hyps(3) by auto
    have "ka ∈ set ((fst ∘ Ana) a)" using ka(2) a' by simp
    hence "ka ∈ N" using a(2) N_supset by auto
    thus ?case using ka a(3,4) unfolding S_def by blast
  qed
  thus ?thesis unfolding S_def by blast
qed


subsection ‹The Protocol Transition System, Defined in Terms of the Reachable Constraints›
definition transaction_fresh_subst where
  "transaction_fresh_subst σ T 𝒜 ≡
    subst_domain σ = set (transaction_fresh T) ∧
    (∀t ∈ subst_range σ. ∃n. t = Fun (Val (n,False)) []) ∧
    (∀t ∈ subst_range σ. t ∉ subtermsset (trmslsst 𝒜)) ∧
    (∀t ∈ subst_range σ. t ∉ subtermsset (trms_transaction T)) ∧
    inj_on σ (subst_domain σ)"

(* NB: We need the protocol P as a parameter for this definition---even though we will only apply α
       to a single transaction T of P---because we have to ensure that α(fv(T)) is disjoint from
       the bound variables of P and 𝒜. *)
definition transaction_renaming_subst where
  "transaction_renaming_subst α P 𝒜 ≡
    ∃n ≥ max_var_set (⋃(vars_transaction ` set P) ∪ varslsst 𝒜). α = var_rename n"

definition constraint_model where
  "constraint_model ℐ 𝒜 ≡ 
    constr_sem_stateful ℐ (unlabel 𝒜) ∧
    interpretationsubst ℐ ∧
    wftrms (subst_range ℐ)"

definition welltyped_constraint_model where
  "welltyped_constraint_model ℐ 𝒜 ≡  wtsubst ℐ ∧ constraint_model ℐ 𝒜"

lemma constraint_model_prefix:
  assumes "constraint_model I (A@B)"
  shows "constraint_model I A"
by (metis assms strand_sem_append_stateful unlabel_append constraint_model_def)

lemma welltyped_constraint_model_prefix:
  assumes "welltyped_constraint_model I (A@B)"
  shows "welltyped_constraint_model I A"
by (metis assms constraint_model_prefix welltyped_constraint_model_def)

lemma constraint_model_Val_is_Value_term:
  assumes "welltyped_constraint_model I A"
    and "t ⋅ I = Fun (Val n) []"
  shows "t = Fun (Val n) [] ∨ (∃m. t = Var (TAtom Value, m))"
proof -
  have "wtsubst I" using assms(1) unfolding welltyped_constraint_model_def by simp
  moreover have "Γ (Fun (Val n) []) = TAtom Value" by auto
  ultimately have *: "Γ t = TAtom Value" by (metis (no_types) assms(2) wt_subst_trm'')

  show ?thesis
  proof (cases t)
    case (Var x)
    obtain τ m where x: "x = (τ, m)" by (metis surj_pair)
    have "Γv x = TAtom Value" using * Var by auto
    hence "τ = TAtom Value" using x Γv_TAtom'[of Value τ m] by simp
    thus ?thesis using x Var by metis
  next
    case (Fun f T) thus ?thesis using assms(2) by auto
  qed
qed

text ‹
  The set of symbolic constraints reachable in any symbolic run of the protocol ‹P›.
  
  ‹σ› instantiates the fresh variables of transaction ‹T› with fresh terms.
  ‹α› is a variable-renaming whose range consists of fresh variables.
›
inductive_set reachable_constraints::
  "('fun,'atom,'sets,'lbl) prot ⇒ ('fun,'atom,'sets,'lbl) prot_constr set"
  for P::"('fun,'atom,'sets,'lbl) prot"
where
  init:
  "[] ∈ reachable_constraints P"
| step:
  "⟦𝒜 ∈ reachable_constraints P;
    T ∈ set P;
    transaction_fresh_subst σ T 𝒜;
    transaction_renaming_subst α P 𝒜
   ⟧ ⟹ 𝒜@duallsst (transaction_strand T ⋅lsst σ ∘s α) ∈ reachable_constraints P"


subsection ‹Admissible Transactions›
definition admissible_transaction_checks where
  "admissible_transaction_checks T ≡
    ∀x ∈ set (unlabel (transaction_checks T)).
      is_Check x ∧
      (is_InSet x ⟶
          is_Var (the_elem_term x) ∧ is_Fun_Set (the_set_term x) ∧
          fst (the_Var (the_elem_term x)) = TAtom Value) ∧
      (is_NegChecks x ⟶
          bvarssstp x = [] ∧
          ((the_eqs x = [] ∧ length (the_ins x) = 1) ∨
           (the_ins x = [] ∧ length (the_eqs x) = 1))) ∧
      (is_NegChecks x ∧ the_eqs x = [] ⟶ (let h = hd (the_ins x) in
          is_Var (fst h) ∧ is_Fun_Set (snd h) ∧
          fst (the_Var (fst h)) = TAtom Value))"

definition admissible_transaction_selects where
  "admissible_transaction_selects T ≡
    ∀x ∈ set (unlabel (transaction_selects T)).
      is_InSet x ∧ the_check x = Assign ∧ is_Var (the_elem_term x) ∧ is_Fun_Set (the_set_term x) ∧
      fst (the_Var (the_elem_term x)) = TAtom Value"

definition admissible_transaction_updates where
  "admissible_transaction_updates T ≡
    ∀x ∈ set (unlabel (transaction_updates T)).
      is_Update x ∧ is_Var (the_elem_term x) ∧ is_Fun_Set (the_set_term x) ∧
      fst (the_Var (the_elem_term x)) = TAtom Value"

definition admissible_transaction_terms where
  "admissible_transaction_terms T ≡
    wftrms' arity (trmslsst (transaction_strand T)) ∧
    (∀f ∈ ⋃(funs_term ` trms_transaction T).
      ¬is_Val f ∧ ¬is_Abs f ∧ ¬is_PubConstSetType f ∧ f ≠ Pair ∧
      ¬is_PubConstAttackType f ∧ ¬is_PubConstBottom f ∧ ¬is_PubConstOccursSecType f) ∧
    (∀r ∈ set (unlabel (transaction_strand T)).
      (∃f ∈ ⋃(funs_term ` (trmssstp r)). is_Attack f) ⟶
        (let t = the_msg r in is_Send r ∧ is_Fun t ∧ is_Attack (the_Fun t) ∧ args t = []))"

definition admissible_transaction_occurs_checks where
  "admissible_transaction_occurs_checks T ≡ (
    (∀x ∈ fv_transaction T - set (transaction_fresh T). fst x = TAtom Value ⟶
      receive⟨occurs (Var x)⟩ ∈ set (unlabel (transaction_receive T))) ∧
    (∀x ∈ set (transaction_fresh T). fst x = TAtom Value ⟶
      send⟨occurs (Var x)⟩ ∈ set (unlabel (transaction_send T))) ∧
    (∀r ∈ set (unlabel (transaction_receive T)). is_Receive r ⟶
      (OccursFact ∈ funs_term (the_msg r) ∨ OccursSec ∈ funs_term (the_msg r)) ⟶
        (∃x ∈ fv_transaction T - set (transaction_fresh T).
          fst x = TAtom Value ∧ the_msg r = occurs (Var x))) ∧
    (∀r ∈ set (unlabel (transaction_send T)). is_Send r ⟶
      (OccursFact ∈ funs_term (the_msg r) ∨ OccursSec ∈ funs_term (the_msg r)) ⟶
        (∃x ∈ set (transaction_fresh T).
          fst x = TAtom Value ∧ the_msg r = occurs (Var x)))
  )"

definition admissible_transaction where
  "admissible_transaction T ≡ (
    wellformed_transaction T ∧
    distinct (transaction_fresh T) ∧
    list_all (λx. fst x = TAtom Value) (transaction_fresh T) ∧
    (∀x ∈ varslsst (transaction_strand T). is_Var (fst x) ∧ (the_Var (fst x) = Value)) ∧
    bvarslsst (transaction_strand T) = {} ∧
    (∀x ∈ fv_transaction T - set (transaction_fresh T).
     ∀y ∈ fv_transaction T - set (transaction_fresh T).
      x ≠ y ⟶ ⟨Var x != Var y⟩ ∈ set (unlabel (transaction_checks T)) ∨
                ⟨Var y != Var x⟩ ∈ set (unlabel (transaction_checks T))) ∧
    admissible_transaction_selects T ∧
    admissible_transaction_checks T ∧
    admissible_transaction_updates T ∧
    admissible_transaction_terms T ∧
    admissible_transaction_occurs_checks T
)"

lemma transaction_no_bvars:
  assumes "admissible_transaction T"
  shows "fv_transaction T = vars_transaction T"
    and "bvars_transaction T = {}"
proof -
  have "wellformed_transaction T" "bvarslsst (transaction_strand T) = {}"
    using assms unfolding admissible_transaction_def
    by blast+
  thus "bvars_transaction T = {}" "fv_transaction T = vars_transaction T"
    using bvars_wellformed_transaction_unfold varssst_is_fvsst_bvarssst
    by fast+
qed

lemma transactions_fv_bvars_disj:
  assumes "∀T ∈ set P. admissible_transaction T"
  shows "(⋃T ∈ set P. fv_transaction T) ∩ (⋃T ∈ set P. bvars_transaction T) = {}"
using assms transaction_no_bvars(2) by fast

lemma transaction_bvars_no_Value_type:
  assumes "admissible_transaction T"
    and "x ∈ bvars_transaction T"
  shows "¬TAtom Value ⊑ Γv x"
using assms transaction_no_bvars(2) by blast

lemma transaction_receive_deduct:
  assumes T_adm: "admissible_transaction T"
    and ℐ: "constraint_model ℐ (A@duallsst (transaction_strand T ⋅lsst σ ∘s α))"
    and σ: "transaction_fresh_subst σ T A"
    and α: "transaction_renaming_subst α P A"
    and t: "receive⟨t⟩ ∈ set (unlabel (transaction_receive T ⋅lsst σ ∘s α))"
  shows "iklsst A ⋅set ℐ ⊢ t ⋅ ℐ"
proof -
  define θ where "θ ≡ σ ∘s α"

  have t': "send⟨t⟩ ∈ set (unlabel (duallsst (transaction_receive T ⋅lsst θ)))"
    using t duallsst_unlabel_steps_iff(2) unfolding θ_def by blast
  then obtain T1 T2 where T: "unlabel (duallsst (transaction_receive T ⋅lsst θ)) = T1@send⟨t⟩#T2"
    using t' by (meson split_list)

  have "constr_sem_stateful ℐ (unlabel A@unlabel (duallsst (transaction_strand T ⋅lsst θ)))"
    using ℐ unlabel_append[of A] unfolding constraint_model_def θ_def by simp
  hence "constr_sem_stateful ℐ (unlabel A@T1@[send⟨t⟩])"
    using strand_sem_append_stateful[of "{}" "{}" "unlabel A@T1@[send⟨t⟩]" _ ℐ]
          transaction_dual_subst_unfold[of T θ] T
    by (metis append.assoc append_Cons append_Nil)
  hence "iksst (unlabel A@T1) ⋅set ℐ ⊢ t ⋅ ℐ"
    using strand_sem_append_stateful[of "{}" "{}" "unlabel A@T1" "[send⟨t⟩]" ℐ] T
    by force
  moreover have "¬is_Receive x"
    when x: "x ∈ set (unlabel (duallsst (transaction_receive T ⋅lsst θ)))" for x
  proof -
    have *: "is_Receive a" when "a ∈ set (unlabel (transaction_receive T))" for a
      using T_adm Ball_set[of "unlabel (transaction_receive T)" is_Receive] that
      unfolding admissible_transaction_def wellformed_transaction_def
      by blast

    obtain l where l: "(l,x) ∈ set (duallsst (transaction_receive T ⋅lsst θ))"
      using x unfolding unlabel_def by fastforce
    then obtain ly where ly: "ly ∈ set (transaction_receive T ⋅lsst θ)" "(l,x) = duallsstp ly"
      unfolding duallsst_def by auto

    obtain j y where j: "ly = (j,y)" by (metis surj_pair)
    hence "j = l" using ly(2) by (cases y) auto
    hence y: "(l,y) ∈ set (transaction_receive T ⋅lsst θ)" "(l,x) = duallsstp (l,y)"
      by (metis j ly(1), metis j ly(2))

    obtain z where z:
        "z ∈ set (unlabel (transaction_receive T))"
        "(l,z) ∈ set (transaction_receive T)"
        "(l,y) = (l,z) ⋅lsstp θ"
      using y(1) unfolding subst_apply_labeled_stateful_strand_def unlabel_def by force

    have "is_Receive y" using *[OF z(1)] z(3) by (cases z) auto
    thus "¬is_Receive x" using l y by (cases y) auto
  qed
  hence "¬is_Receive x" when "x ∈ set T1" for x using T that by simp
  hence "iksst T1 = {}" unfolding iksst_def is_Receive_def by fast
  hence "iksst (unlabel A@T1) = iklsst A" using iksst_append[of "unlabel A" T1] by simp
  ultimately show ?thesis by (simp add: θ_def)
qed

lemma transaction_checks_db:
  assumes T: "admissible_transaction T"
    and ℐ: "constraint_model ℐ (A@duallsst (transaction_strand T ⋅lsst σ ∘s α))"
    and σ: "transaction_fresh_subst σ T A"
    and α: "transaction_renaming_subst α P A"
  shows "⟨Var (TAtom Value, n) in Fun (Set s) []⟩ ∈ set (unlabel (transaction_checks T))
          ⟹ (α (TAtom Value, n) ⋅ ℐ, Fun (Set s) []) ∈ set (dblsst A ℐ)"
      (is "?A ⟹ ?B")
    and "⟨Var (TAtom Value, n) not in Fun (Set s) []⟩ ∈ set (unlabel (transaction_checks T))
          ⟹ (α (TAtom Value, n) ⋅ ℐ, Fun (Set s) []) ∉ set (dblsst A ℐ)"
      (is "?C ⟹ ?D")
proof -
  let ?x = "λn. (TAtom Value, n)"
  let ?s = "Fun (Set s) []"
  let ?T = "transaction_receive T@transaction_selects T@transaction_checks T"
  let ?T' = "?T ⋅lsst σ ∘s α"
  let ?S = "λS. transaction_receive T@transaction_selects T@S"
  let ?S' = "λS. ?S S ⋅lsst σ ∘s α"

  have T_valid: "wellformed_transaction T" using T by (simp add: admissible_transaction_def)

  have "constr_sem_stateful ℐ (unlabel (A@duallsst (transaction_strand T ⋅lsst σ ∘s α)))"
    using ℐ unfolding constraint_model_def by simp
  moreover have
      "duallsst (transaction_strand T ⋅lsst δ) =
       duallsst (?S (T1@[c]) ⋅lsst δ)@
       duallsst (T2@transaction_updates T@transaction_send T ⋅lsst δ)"
    when "transaction_checks T = T1@c#T2" for T1 T2 c δ
    using that duallsst_append subst_lsst_append
    unfolding transaction_strand_def
    by (metis append.assoc append_Cons append_Nil)
  ultimately have T'_model: "constr_sem_stateful ℐ (unlabel (A@duallsst (?S' (T1@[(l,c)]))))"
    when "transaction_checks T = T1@(l,c)#T2" for T1 T2 l c
    using strand_sem_append_stateful[of _ _ _ _ ℐ]
    by (simp add: that transaction_strand_def)

  show "?A ⟹ ?B"
  proof -
    assume a: ?A
    hence *: "⟨Var (?x n) in ?s⟩ ∈ set (unlabel ?T)"
      unfolding transaction_strand_def unlabel_def by simp
    then obtain l T1 T2 where T1: "transaction_checks T = T1@(l,⟨Var (?x n) in ?s⟩)#T2"
      by (metis a split_list unlabel_mem_has_label)

    have "?x n ∈ fvlsst (transaction_checks T)"
      using a by force
    hence "?x n ∉ set (transaction_fresh T)"
      using a transaction_fresh_vars_notin[OF T_valid] by fast
    hence "unlabel (A@duallsst (?S' (T1@[(l,⟨Var (?x n) in ?s⟩)]))) =
           unlabel (A@duallsst (?S' T1))@[⟨α (?x n) in ?s⟩]"
      using T a σ duallsst_append subst_lsst_append unlabel_append
      by (fastforce simp add: transaction_fresh_subst_def unlabel_def duallsst_def
                              subst_apply_labeled_stateful_strand_def)
    moreover have "dbsst (unlabel A) = dbsst (unlabel (A@duallsst (?S' T1)))"
      by (simp add: T1 dbsst_transaction_prefix_eq[OF T_valid] del: unlabel_append)
    ultimately have "∃M. strand_sem_stateful M (set (dbsst (unlabel A) ℐ)) [⟨α (?x n) in ?s⟩] ℐ"
      using T'_model[OF T1] dbsst_set_is_dbupdsst[of _ ℐ] strand_sem_append_stateful[of _ _ _ _ ℐ]
      by (simp add: dbsst_def del: unlabel_append)
    thus ?B by simp
  qed

  show "?C ⟹ ?D"
  proof -
    assume a: ?C
    hence *: "⟨Var (?x n) not in ?s⟩ ∈ set (unlabel ?T)"
      unfolding transaction_strand_def unlabel_def by simp
    then obtain l T1 T2 where T1: "transaction_checks T = T1@(l,⟨Var (?x n) not in ?s⟩)#T2"
      by (metis a split_list unlabel_mem_has_label)

    have "?x n ∈ varssstp ⟨Var (?x n) not in ?s⟩"
      using varssstp_cases(9)[of "[]" "Var (?x n)" ?s] by auto
    hence "?x n ∈ varslsst (transaction_checks T)"
      using a unfolding varssst_def by force
    hence "?x n ∉ set (transaction_fresh T)"
      using a transaction_fresh_vars_notin[OF T_valid] by fast
    hence "unlabel (A@duallsst (?S' (T1@[(l,⟨Var (?x n) not in ?s⟩)]))) =
           unlabel (A@duallsst (?S' T1))@[⟨α (?x n) not in ?s⟩]"
      using T a σ duallsst_append subst_lsst_append unlabel_append
      by (fastforce simp add: transaction_fresh_subst_def unlabel_def duallsst_def
                              subst_apply_labeled_stateful_strand_def)
    moreover have "dbsst (unlabel A) = dbsst (unlabel (A@duallsst (?S' T1)))"
      by (simp add: T1 dbsst_transaction_prefix_eq[OF T_valid] del: unlabel_append)
    ultimately have "∃M. strand_sem_stateful M (set (dbsst (unlabel A) ℐ)) [⟨α (?x n) not in ?s⟩] ℐ"
      using T'_model[OF T1] dbsst_set_is_dbupdsst[of _ ℐ] strand_sem_append_stateful[of _ _ _ _ ℐ]
      by (simp add: dbsst_def del: unlabel_append)
    thus ?D using stateful_strand_sem_NegChecks_no_bvars(1)[of _ _ _ ?s ℐ] by simp
  qed
qed

lemma transaction_selects_db:
  assumes T: "admissible_transaction T"
    and ℐ: "constraint_model ℐ (A@duallsst (transaction_strand T ⋅lsst σ ∘s α))"
    and σ: "transaction_fresh_subst σ T A"
    and α: "transaction_renaming_subst α P A"
  shows "select⟨Var (TAtom Value, n), Fun (Set s) []⟩ ∈ set (unlabel (transaction_selects T))
          ⟹ (α (TAtom Value, n) ⋅ ℐ, Fun (Set s) []) ∈ set (dblsst A ℐ)"
      (is "?A ⟹ ?B")
proof -
  let ?x = "λn. (TAtom Value, n)"
  let ?s = "Fun (Set s) []"
  let ?T = "transaction_receive T@transaction_selects T@transaction_checks T"
  let ?T' = "?T ⋅lsst σ ∘s α"
  let ?S = "λS. transaction_receive T@S"
  let ?S' = "λS. ?S S ⋅lsst σ ∘s α"

  have T_valid: "wellformed_transaction T" using T by (simp add: admissible_transaction_def)

  have "constr_sem_stateful ℐ (unlabel (A@duallsst (transaction_strand T ⋅lsst σ ∘s α)))"
    using ℐ unfolding constraint_model_def by simp
  moreover have
      "duallsst (transaction_strand T ⋅lsst δ) =
       duallsst (?S (T1@[c]) ⋅lsst δ)@
       duallsst (T2@transaction_checks T @ transaction_updates T@transaction_send T ⋅lsst δ)"
    when "transaction_selects T = T1@c#T2" for T1 T2 c δ
    using that duallsst_append subst_lsst_append
    unfolding transaction_strand_def by (metis append.assoc append_Cons append_Nil)
  ultimately have T'_model: "constr_sem_stateful ℐ (unlabel (A@duallsst (?S' (T1@[(l,c)]))))"
    when "transaction_selects T = T1@(l,c)#T2" for T1 T2 l c
    using strand_sem_append_stateful[of _ _ _ _ ℐ]
    by (simp add: that transaction_strand_def)

  show "?A ⟹ ?B"
  proof -
    assume a: ?A
    hence *: "select⟨Var (?x n), ?s⟩ ∈ set (unlabel ?T)"
      unfolding transaction_strand_def unlabel_def by simp
    then obtain l T1 T2 where T1: "transaction_selects T = T1@(l,select⟨Var (?x n), ?s⟩)#T2"
      by (metis a split_list unlabel_mem_has_label)

    have "?x n ∈ fvlsst (transaction_selects T)"
      using a by force
    hence "?x n ∉ set (transaction_fresh T)"
      using a transaction_fresh_vars_notin[OF T_valid] by fast
    hence "unlabel (A@duallsst (?S' (T1@[(l,select⟨Var (?x n), ?s⟩)]))) =
           unlabel (A@duallsst (?S' T1))@[select⟨α (?x n), ?s⟩]"
      using T a σ duallsst_append subst_lsst_append unlabel_append
      by (fastforce simp add: transaction_fresh_subst_def unlabel_def duallsst_def
                              subst_apply_labeled_stateful_strand_def)
    moreover have "dbsst (unlabel A) = dbsst (unlabel (A@duallsst (?S' T1)))"
      by (simp add: T1 dbsst_transaction_prefix_eq[OF T_valid] del: unlabel_append)
    ultimately have "∃M. strand_sem_stateful M (set (dbsst (unlabel A) ℐ)) [⟨α (?x n) in ?s⟩] ℐ"
      using T'_model[OF T1] dbsst_set_is_dbupdsst[of _ ℐ] strand_sem_append_stateful[of _ _ _ _ ℐ]
      by (simp add: dbsst_def del: unlabel_append)
    thus ?B by simp
  qed
qed

lemma transactions_have_no_Value_consts:
  assumes "admissible_transaction T"
    and "t ∈ subtermsset (trmslsst (transaction_strand T))"
  shows "∄a T. t = Fun (Val a) T" (is ?A)
    and "∄a T. t = Fun (Abs a) T" (is ?B)
proof -
  have "admissible_transaction_terms T" using assms(1) unfolding admissible_transaction_def by blast
  hence "¬is_Val f" "¬is_Abs f"
    when "f ∈ ⋃(funs_term ` (trms_transaction T))" for f
    using that unfolding admissible_transaction_terms_def by blast+
  moreover have "f ∈ ⋃(funs_term ` (trms_transaction T))"
    when "f ∈ funs_term t" for f
    using that assms(2) funs_term_subterms_eq(2)[of "trms_transaction T"] by blast+
  ultimately have *: "¬is_Val f" "¬is_Abs f"
    when "f ∈ funs_term t" for f
    using that by presburger+

  show ?A using *(1) by force
  show ?B using *(2) by force
qed

lemma transactions_have_no_Value_consts':
  assumes "admissible_transaction T"
    and "t ∈ trmslsst (transaction_strand T)"
  shows "∄a T. Fun (Val a) T ∈ subterms t"
    and "∄a T. Fun (Abs a) T ∈ subterms t"
using transactions_have_no_Value_consts[OF assms(1)] assms(2) by fast+

lemma transactions_have_no_PubConsts:
  assumes "admissible_transaction T"
    and "t ∈ subtermsset (trmslsst (transaction_strand T))"
  shows "∄a T. t = Fun (PubConstSetType a) T" (is ?A)
    and "∄a T. t = Fun (PubConstAttackType a) T" (is ?B)
    and "∄a T. t = Fun (PubConstBottom a) T" (is ?C)
    and "∄a T. t = Fun (PubConstOccursSecType a) T" (is ?D)
proof -
  have "admissible_transaction_terms T" using assms(1) unfolding admissible_transaction_def by blast
  hence "¬is_PubConstSetType f" "¬is_PubConstAttackType f"
        "¬is_PubConstBottom f" "¬is_PubConstOccursSecType f"
    when "f ∈ ⋃(funs_term ` (trms_transaction T))" for f
    using that unfolding admissible_transaction_terms_def by blast+
  moreover have "f ∈ ⋃(funs_term ` (trms_transaction T))"
    when "f ∈ funs_term t" for f
    using that assms(2) funs_term_subterms_eq(2)[of "trms_transaction T"] by blast+
  ultimately have *:
      "¬is_PubConstSetType f" "¬is_PubConstAttackType f"
      "¬is_PubConstBottom f" "¬is_PubConstOccursSecType f"
    when "f ∈ funs_term t" for f
    using that by presburger+

  show ?A using *(1) by force
  show ?B using *(2) by force
  show ?C using *(3) by force
  show ?D using *(4) by force
qed

lemma transactions_have_no_PubConsts':
  assumes "admissible_transaction T"
    and "t ∈ trmslsst (transaction_strand T)"
  shows "∄a T. Fun (PubConstSetType a) T ∈ subterms t"
    and "∄a T. Fun (PubConstAttackType a) T ∈ subterms t"
    and "∄a T. Fun (PubConstBottom a) T ∈ subterms t"
    and "∄a T. Fun (PubConstOccursSecType a) T ∈ subterms t"
using transactions_have_no_PubConsts[OF assms(1)] assms(2) by fast+

lemma transaction_inserts_are_Value_vars:
  assumes T_valid: "wellformed_transaction T"
    and "admissible_transaction_updates T"
    and "insert⟨t,s⟩ ∈ set (unlabel (transaction_strand T))"
  shows "∃n. t = Var (TAtom Value, n)"
    and "∃u. s = Fun (Set u) []"
proof -
  let ?x = "insert⟨t,s⟩"

  have "?x ∈ set (unlabel (transaction_updates T))"
    using assms(3) wellformed_transaction_unlabel_cases[OF T_valid, of ?x]    
    by (auto simp add: transaction_strand_def unlabel_def)
  hence *: "is_Var (the_elem_term ?x)" "fst (the_Var (the_elem_term ?x)) = TAtom Value"
           "is_Fun (the_set_term ?x)" "args (the_set_term ?x) = []"
           "is_Set (the_Fun (the_set_term ?x))"
    using assms(2) unfolding admissible_transaction_updates_def is_Fun_Set_def by fastforce+
  
  show "∃n. t = Var (TAtom Value, n)" using *(1,2) by (cases t) auto
  show "∃u. s = Fun (Set u) []" using *(3,4,5) unfolding is_Set_def by (cases s) auto
qed

lemma transaction_deletes_are_Value_vars:
  assumes T_valid: "wellformed_transaction T"
    and "admissible_transaction_updates T"
    and "delete⟨t,s⟩ ∈ set (unlabel (transaction_strand T))"
  shows "∃n. t = Var (TAtom Value, n)"
    and "∃u. s = Fun (Set u) []"
proof -
  let ?x = "delete⟨t,s⟩"

  have "?x ∈ set (unlabel (transaction_updates T))"
    using assms(3) wellformed_transaction_unlabel_cases[OF T_valid, of ?x]    
    by (auto simp add: transaction_strand_def unlabel_def)
  hence *: "is_Var (the_elem_term ?x)" "fst (the_Var (the_elem_term ?x)) = TAtom Value"
           "is_Fun (the_set_term ?x)" "args (the_set_term ?x) = []"
           "is_Set (the_Fun (the_set_term ?x))"
    using assms(2) unfolding admissible_transaction_updates_def is_Fun_Set_def by fastforce+
  
  show "∃n. t = Var (TAtom Value, n)" using *(1,2) by (cases t) auto
  show "∃u. s = Fun (Set u) []" using *(3,4,5) unfolding is_Set_def by (cases s) auto
qed

lemma transaction_selects_are_Value_vars:
  assumes T_valid: "wellformed_transaction T"
    and "admissible_transaction_selects T"
    and "select⟨t,s⟩ ∈ set (unlabel (transaction_strand T))"
  shows "∃n. t = Var (TAtom Value, n) ∧ (TAtom Value, n) ∉ set (transaction_fresh T)" (is ?A)
    and "∃u. s = Fun (Set u) []" (is ?B)
proof -
  let ?x = "select⟨t,s⟩"

  have *: "?x ∈ set (unlabel (transaction_selects T))"
    using assms(3) wellformed_transaction_unlabel_cases[OF T_valid, of ?x]    
    by (auto simp add: transaction_strand_def unlabel_def)
  
  have **: "is_Var (the_elem_term ?x)" "fst (the_Var (the_elem_term ?x)) = TAtom Value"
           "is_Fun (the_set_term ?x)" "args (the_set_term ?x) = []"
           "is_Set (the_Fun (the_set_term ?x))"
    using * assms(2) unfolding admissible_transaction_selects_def is_Fun_Set_def by fastforce+

  have "fvsstp ?x ⊆ fvlsst (transaction_selects T)"
    using * by force
  hence ***: "fvsstp ?x ∩ set (transaction_fresh T) = {}"
    using T_valid unfolding wellformed_transaction_def by fast

  show ?A using **(1,2) *** by (cases t) auto
  show ?B using **(3,4,5) unfolding is_Set_def by (cases s) auto
qed

lemma transaction_inset_checks_are_Value_vars:
  assumes T_valid: "wellformed_transaction T"
    and "admissible_transaction_checks T"
    and "⟨t in s⟩ ∈ set (unlabel (transaction_strand T))"
  shows "∃n. t = Var (TAtom Value, n) ∧ (TAtom Value, n) ∉ set (transaction_fresh T)" (is ?A)
    and "∃u. s = Fun (Set u) []" (is ?B)
proof -
  let ?x = "⟨t in s⟩"

  have *: "?x ∈ set (unlabel (transaction_checks T))"
    using assms(3) wellformed_transaction_unlabel_cases[OF T_valid, of ?x]    
    by (auto simp add: transaction_strand_def unlabel_def)
  
  have **: "is_Var (the_elem_term ?x)" "fst (the_Var (the_elem_term ?x)) = TAtom Value"
           "is_Fun (the_set_term ?x)" "args (the_set_term ?x) = []"
           "is_Set (the_Fun (the_set_term ?x))"
    using * assms(2) unfolding admissible_transaction_checks_def is_Fun_Set_def by fastforce+

  have "fvsstp ?x ⊆ fvlsst (transaction_checks T)"
    using * by force
  hence ***: "fvsstp ?x ∩ set (transaction_fresh T) = {}"
    using T_valid unfolding wellformed_transaction_def by fast

  show ?A using **(1,2) *** by (cases t) auto
  show ?B using **(3,4,5) unfolding is_Set_def by (cases s) auto
qed

lemma transaction_notinset_checks_are_Value_vars:
  assumes T_valid: "wellformed_transaction T"
    and "admissible_transaction_checks T"
    and "∀X⟨∨≠: F ∨∉: G⟩ ∈ set (unlabel (transaction_strand T))"
    and "(t,s) ∈ set G"
  shows "∃n. t = Var (TAtom Value, n) ∧ (TAtom Value, n) ∉ set (transaction_fresh T)" (is ?A)
    and "∃u. s = Fun (Set u) []" (is ?B)
proof -
  let ?x = "∀X⟨∨≠: F ∨∉: G⟩"

  have 0: "?x ∈ set (unlabel (transaction_checks T))"
    using assms(3) wellformed_transaction_unlabel_cases[OF T_valid, of ?x]    
    by (auto simp add: transaction_strand_def unlabel_def)
  hence 1: "F = [] ∧ length G = 1"
    using assms(2,4) unfolding admissible_transaction_checks_def by fastforce
  hence "hd G = (t,s)" using assms(4) by (cases "the_ins ?x") auto
  hence **: "is_Var t" "fst (the_Var t) = TAtom Value" "is_Fun s" "args s = []" "is_Set (the_Fun s)"
    using 0 1 assms(2) unfolding admissible_transaction_checks_def Let_def is_Fun_Set_def
    by fastforce+

  have "fvsstp ?x ⊆ fvlsst (transaction_checks T)"
       "set (bvarssstp ?x) ⊆ bvarslsst (transaction_checks T)"
    using 0 by force+
  moreover have 
      "fvlsst (transaction_checks T) ⊆ fvlsst (transaction_receive T) ∪ fvlsst (transaction_selects T)"
      "set (transaction_fresh T) ∩ fvlsst (transaction_receive T) = {}"
      "set (transaction_fresh T) ∩ fvlsst (transaction_selects T) = {}"
    using T_valid unfolding wellformed_transaction_def by fast+
  ultimately have
      "fvsstp ?x ∩ set (transaction_fresh T) = {}"
      "set (bvarssstp ?x) ∩ set (transaction_fresh T) = {}"
    using wellformed_transaction_wfsst(2,3)[OF T_valid]
          fv_transaction_unfold[of T] bvars_transaction_unfold[of T]
    by blast+
  hence ***: "fv t ∩ set (transaction_fresh T) = {}"
    using assms(4) by auto

  show ?A using **(1,2) *** by (cases t) auto
  show ?B using **(3,4,5) unfolding is_Set_def by (cases s) auto
qed

lemma admissible_transaction_strand_step_cases:
  assumes T_adm: "admissible_transaction T"
  shows "r ∈ set (unlabel (transaction_receive T)) ⟹ ∃t. r = receive⟨t⟩"
        (is "?A ⟹ ?A'")
    and "r ∈ set (unlabel (transaction_selects T)) ⟹
            ∃x s. r = select⟨Var x, Fun (Set s) []⟩ ∧
                  fst x = TAtom Value ∧ x ∈ fv_transaction T - set (transaction_fresh T)"
        (is "?B ⟹ ?B'")
    and "r ∈ set (unlabel (transaction_checks T)) ⟹
            (∃x s. (r = ⟨Var x in Fun (Set s) []⟩ ∨ r = ⟨Var x not in Fun (Set s) []⟩) ∧
                   fst x = TAtom Value ∧ x ∈ fv_transaction T - set (transaction_fresh T)) ∨
            (∃s t. r = ⟨s == t⟩ ∨ r = ⟨s != t⟩)"
        (is "?C ⟹ ?C'")
    and "r ∈ set (unlabel (transaction_updates T)) ⟹
            ∃x s. (r = insert⟨Var x, Fun (Set s) []⟩ ∨ r = delete⟨Var x, Fun (Set s) []⟩) ∧
                  fst x = TAtom Value"
        (is "?D ⟹ ?D'")
    and "r ∈ set (unlabel (transaction_send T)) ⟹ ∃t. r = send⟨t⟩"
        (is "?E ⟹ ?E'")
proof -
  have T_valid: "wellformed_transaction T"
    using T_adm unfolding admissible_transaction_def by metis

  show "?A ⟹ ?A'"
    using T_valid Ball_set[of "unlabel (transaction_receive T)" is_Receive]
    unfolding wellformed_transaction_def is_Receive_def
    by blast

  show "?E ⟹ ?E'"
    using T_valid Ball_set[of "unlabel (transaction_send T)" is_Send]
    unfolding wellformed_transaction_def is_Send_def
    by blast

  show "?B ⟹ ?B'"
  proof -
    assume r: ?B
    have "admissible_transaction_selects T"
      using T_adm unfolding admissible_transaction_def by simp
    hence *: "is_InSet r" "the_check r = Assign" "is_Var (the_elem_term r)"
             "is_Fun (the_set_term r)" "is_Set (the_Fun (the_set_term r))"
             "args (the_set_term r) = []" "fst (the_Var (the_elem_term r)) = TAtom Value"
      using r unfolding admissible_transaction_selects_def is_Fun_Set_def
      by fast+
    
    obtain rt rs where r': "r = select⟨rt,rs⟩" using *(1,2) by (cases r) auto
    obtain x where x: "rt = Var x" "fst x = TAtom Value" using *(3,7) r' by auto
    obtain f S where fS: "rs = Fun f S" using *(4) r' by auto
    obtain s where s: "f = Set s" using *(5) fS r' by (cases f) auto
    hence S: "S = []" using *(6) fS r' by (cases S) auto

    have fv_r1: "fvsstp r ⊆ fv_transaction T"
      using r fv_transaction_unfold[of T] by auto
  
    have fv_r2: "fvsstp r ∩ set (transaction_fresh T) = {}"
      using r T_valid unfolding wellformed_transaction_def by fastforce

    show ?B' using r' x fS s S fv_r1 fv_r2 by simp
  qed

  show "?C ⟹ ?C'"
  proof -
    assume r: ?C
    have adm_checks: "admissible_transaction_checks T"
      using assms unfolding admissible_transaction_def by simp

    have fv_r1: "fvsstp r ⊆ fv_transaction T"
      using r fv_transaction_unfold[of T] by auto
  
    have fv_r2: "fvsstp r ∩ set (transaction_fresh T) = {}"
      using r T_valid unfolding wellformed_transaction_def by fastforce

    have "(is_InSet r ∧ the_check r = Check) ∨
          (is_Equality r ∧ the_check r = Check) ∨
          is_NegChecks r"
      using r adm_checks unfolding admissible_transaction_checks_def by fast
    thus ?C'
    proof (elim disjE conjE)
      assume *: "is_InSet r" "the_check r = Check"
      hence **: "is_Var (the_elem_term r)" "is_Fun (the_set_term r)"
                "is_Set (the_Fun (the_set_term r))" "args (the_set_term r) = []"
                "fst (the_Var (the_elem_term r)) = TAtom Value"
        using r adm_checks unfolding admissible_transaction_checks_def is_Fun_Set_def
        by fast+
      
      obtain rt rs where r': "r = ⟨rt in rs⟩" using * by (cases r) auto
      obtain x where x: "rt = Var x" "fst x = TAtom Value" using **(1,5) r' by auto
      obtain f S where fS: "rs = Fun f S" using **(2) r' by auto
      obtain s where s: "f = Set s" using **(3) fS r' by (cases f) auto
      hence S: "S = []" using **(4) fS r' by auto
  
      show ?C' using r' x fS s S fv_r1 fv_r2 by simp
    next
      assume *: "is_NegChecks r"
      hence **: "bvarssstp r = []"
                "(the_eqs r = [] ∧ length (the_ins r) = 1) ∨
                 (the_ins r = [] ∧ length (the_eqs r) = 1)"
        using r adm_checks unfolding admissible_transaction_checks_def by fast+
      show ?C' using **(2)
      proof (elim disjE conjE)
        assume ***: "the_eqs r = []" "length (the_ins r) = 1"
        then obtain t s where ts: "the_ins r = [(t,s)]" by (cases "the_ins r") auto
        hence "hd (the_ins r) = (t,s)" by simp
        hence ****: "is_Var (fst (t,s))" "is_Fun (snd (t,s))"
                    "is_Set (the_Fun (snd (t,s)))" "args (snd (t,s)) = []"
                    "fst (the_Var (fst (t,s))) = TAtom Value"
          using r adm_checks * ***(1) unfolding admissible_transaction_checks_def is_Fun_Set_def
          by metis+
        obtain x where x: "t = Var x" "fst x = TAtom Value" using ts ****(1,5) by (cases t) simp_all
        obtain f S where fS: "s = Fun f S" using ts ****(2) by (cases s) simp_all
        obtain ss where ss: "f = Set ss" using fS ****(3) by (cases f) simp_all
        have S: "S = []" using ts fS ss ****(4) by simp
        
        show ?C' using ts x fS ss S *** **(1) * fv_r1 fv_r2 by (cases r) auto
      next
        assume ***: "the_ins r = []" "length (the_eqs r) = 1"
        then obtain t s where "the_eqs r = [(t,s)]" by (cases "the_eqs r") auto
        thus ?C' using *** **(1) * by (cases r) auto
      qed
    qed (auto simp add: is_Equality_def the_check_def)
  qed

  show "?D ⟹ ?D'"
  proof -
    assume r: ?D
    have adm_upds: "admissible_transaction_updates T"
      using assms unfolding admissible_transaction_def by simp

    have *: "is_Update r" "is_Var (the_elem_term r)" "is_Fun (the_set_term r)"
            "is_Set (the_Fun (the_set_term r))" "args (the_set_term r) = []"
            "fst (the_Var (the_elem_term r)) = TAtom Value"
      using r adm_upds unfolding admissible_transaction_updates_def is_Fun_Set_def by fast+

    obtain t s where ts: "r = insert⟨t,s⟩ ∨ r = delete⟨t,s⟩" using *(1) by (cases r) auto
    obtain x where x: "t = Var x" "fst x = TAtom Value" using ts *(2,6) by (cases t) auto
    obtain f T where fT: "s = Fun f T" using ts *(3) by (cases s) auto
    obtain ss where ss: "f = Set ss" using ts fT *(4) by (cases f) fastforce+
    have T: "T = []" using ts fT *(5) ss by (cases T) auto

    show ?D'
      using ts x fT ss T by blast
  qed
qed

lemma transaction_Value_vars_are_fv:
  assumes "admissible_transaction T"
    and "x ∈ vars_transaction T"
    and "Γv x = TAtom Value"
  shows "x ∈ fv_transaction T"
using assms Γv_TAtom''(2)[of x] varssst_is_fvsst_bvarssst[of "unlabel (transaction_strand T)"]
unfolding admissible_transaction_def by fast

lemma protocol_transaction_vars_TAtom_typed:
  assumes P: "admissible_transaction T"
  shows "∀x ∈ vars_transaction T. Γv x = TAtom Value ∨ (∃a. Γv x = TAtom (Atom a))"
    and "∀x ∈ fv_transaction T. Γv x = TAtom Value ∨ (∃a. Γv x = TAtom (Atom a))"
    and "∀x ∈ set (transaction_fresh T). Γv x = TAtom Value"
proof -
  have P': "wellformed_transaction T"
    using P unfolding admissible_transaction_def by fast

  show "∀x ∈ vars_transaction T. Γv x = TAtom Value ∨ (∃a. Γv x = TAtom (Atom a))"
    using P Γv_TAtom''
    unfolding admissible_transaction_def is_Var_def prot_atom.is_Atom_def the_Var_def
    by fastforce
  thus "∀x ∈ fv_transaction T. Γv x = TAtom Value ∨ (∃a. Γv x = TAtom (Atom a))"
    using varssst_is_fvsst_bvarssst by fast

  have "list_all (λx. fst x = Var Value) (transaction_fresh T)"
    using P Γv_TAtom'' unfolding admissible_transaction_def by fast
  thus "∀x ∈ set (transaction_fresh T). Γv x = TAtom Value"
    using Γv_TAtom''(2) unfolding list_all_iff by fast
qed

lemma protocol_transactions_no_pubconsts:
  assumes "admissible_transaction T"
  shows "Fun (Val (n,True)) S ∉ subtermsset (trms_transaction T)"
using assms transactions_have_no_Value_consts(1)
by fast

lemma protocol_transactions_no_abss:
  assumes "admissible_transaction T"
  shows "Fun (Abs n) S ∉ subtermsset (trms_transaction T)"
using assms transactions_have_no_Value_consts(2)
by fast

lemma admissible_transaction_strand_sem_fv_ineq:
  assumes T_adm: "admissible_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and x: "x ∈ fv_transaction T - set (transaction_fresh T)"
    and y: "y ∈ fv_transaction T - set (transaction_fresh T)"
    and x_not_y: "x ≠ y"
  shows "θ x ⋅ ℐ ≠