Theory Stateful_Protocol_Model

(*  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
    SPDX-License-Identifier: BSD-3-Clause
*)

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,'lbl) 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 (PubConst _ _) = 0"

fun public where
  "public (Fu f) = publicf f"
| "public (Set s) = (aritys s > 0)"
| "public (Val n) = False"
| "public (Abs _) = False"
| "public Pair = True"
| "public (Attack _) = False"
| "public OccursFact = True"
| "public OccursSec = False"
| "public (PubConst _ _) = 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 AbsValue
    | (Set _)  TAtom SetType
    | (Attack _)  TAtom AttackType
    | OccursSec  TAtom OccursSecType
    | (PubConst a _)  TAtom a
    | _  TAtom Bottom
    else TComp f (map Γ T))"

lemma Γ_consts_simps[simp]:
  "arityf g = 0  Γ (Fun (Fu g) []::('fun,'atom,'sets,'lbl) prot_term)
                    = TAtom (case Γf g of Some a  Atom a | None  Bottom)"
  "Γ (Fun (Val n) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom Value"
  "Γ (Fun (Abs b) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom AbsValue"
  "aritys s = 0  Γ (Fun (Set s) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom SetType"
  "Γ (Fun (Attack x) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom AttackType"
  "Γ (Fun OccursSec []::('fun,'atom,'sets,'lbl) prot_term) = TAtom OccursSecType"
  "Γ (Fun (PubConst a t) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom a"
by simp+

lemma Γ_Fu_simps[simp]:
  "arityf f  0  Γ (Fun (Fu f) T) = TComp (Fu f) (map Γ T)" (is "?A1  ?A2")
  "arityf f = 0  Γf f = Some a  Γ (Fun (Fu f) T) = TAtom (Atom a)" (is "?B1  ?B2  ?B3")
  "arityf f = 0  Γf f = None  Γ (Fun (Fu f) T) = TAtom Bottom" (is "?C1  ?C2  ?C3")
  "Γ (Fun (Fu f) T)  TAtom Value" (is ?D)
  "Γ (Fun (Fu f) T)  TAtom AttackType" (is ?E)
  "Γ (Fun (Fu f) T)  TAtom OccursSecType" (is ?F)
proof -
  show "?A1  ?A2" by simp
  show "?B1  ?B2  ?B3" by simp
  show "?C1  ?C2  ?C3" by simp
  show ?D by (cases "Γf f") simp_all
  show ?E by (cases "Γf f") simp_all
  show ?F by (cases "Γf f") simp_all
qed

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,'lbl) 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 auto
    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 force
    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 force
  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: "ifvset (set K'). i < length T" by simp_all
  then obtain k' where k': "k'  set K'" "k = k'  (!) T" using Fun.prems(3) by force
  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 force
  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 force
    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,'lbl) prot_term) = TAtom a  public c}"
  (is "?P a")
proof -
  let ?T = "λf. (range f)::('fun,'atom,'sets,'lbl) 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,'lbl) prot_fun  ?T f. x  UNIV. y = f x"
  let ?D = "λf b. ?T f  {c. Γ (Fun c []::('fun,'atom,'sets,'lbl) 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,'lbl) 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 "PubConst (Atom b)" a] by force
  next
    case Value thus ?thesis using sub_lmm[of "PubConst Value" a] by force
  next
    case SetType thus ?thesis using sub_lmm[of "PubConst SetType" a] by fastforce
  next
    case AttackType thus ?thesis using sub_lmm[of "PubConst AttackType" a] by fastforce
  next
    case Bottom thus ?thesis using sub_lmm[of "PubConst Bottom" a] by fastforce
  next
    case OccursSecType thus ?thesis using sub_lmm[of "PubConst OccursSecType" a] by fastforce
  next
    case AbsValue thus ?thesis using sub_lmm[of "PubConst AbsValue" a] by force
  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 force
      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 force
    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 ****: "ifvset (set K'). i < length T" "iset 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_typing' arity public Ana Γ Pair label_witness1 label_witness2
  apply unfold_locales
  subgoal by (metis assm6)
  subgoal by (metis assm7)
  subgoal by (metis assm9)
  subgoal by (rule assm10)
  subgoal by (metis assm12)
  subgoal by (metis assm13)
  subgoal by (metis assm14)
  subgoal by (rule label_witness_assm)
  subgoal by (rule arity.simps(5))
  subgoal by (metis assm14)
  subgoal by (metis assm8)
  subgoal by (metis assm11)
  done


subsection ‹The Protocol Transition System, Defined in Terms of the Reachable Constraints›
definition transaction_decl_subst where
  "transaction_decl_subst (ξ::('fun,'atom,'sets,'lbl) prot_subst) T 
    subst_domain ξ = fst ` set (transaction_decl T ()) 
    ((x,cs)  set (transaction_decl T ()). c  cs.
      ξ x = Fun (Fu c) [] 
      arity (Fu c::('fun,'atom,'sets,'lbl) prot_fun) = 0) 
    wtsubst ξ"

definition transaction_fresh_subst where
  "transaction_fresh_subst σ T M 
    subst_domain σ = set (transaction_fresh T) 
    (t  subst_range σ. c. t = Fun c []  ¬public c  arity c = 0) 
    (t  subst_range σ. t  subtermsset M) 
    (t  subst_range σ. t  subtermsset (trms_transaction T)) 
    wtsubst σ  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 X 
    n  max_var_set ((vars_transaction ` set P)  X). α = var_rename n"

definition (in intruder_model) constraint_model where
  "constraint_model  𝒜  
    constr_sem_stateful  (unlabel 𝒜) 
    interpretationsubst  
    wftrms (subst_range )"

definition (in typed_model) welltyped_constraint_model where
  "welltyped_constraint_model  𝒜  wtsubst   constraint_model  𝒜"

text ‹
  The set of symbolic constraints reachable in any symbolic run of the protocol P›.
  
  ξ› instantiates the "declared variables" of transaction T› with ground terms.
  σ› 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[simp]:
  "[]  reachable_constraints P"
| step:
  "𝒜  reachable_constraints P;
    T  set P;
    transaction_decl_subst ξ T;
    transaction_fresh_subst σ T (trmslsst 𝒜);
    transaction_renaming_subst α P (varslsst 𝒜)
     𝒜@duallsst (transaction_strand T lsst ξ s σ s α)  reachable_constraints P"


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(18),
    metis Γv_TAtom' surj_pair prot_atom.distinct(26),
    metis Γv_TAtom' surj_pair prot_atom.distinct(32),
    metis Γv_TAtom' surj_pair prot_atom.distinct(38))

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,'lbl) prot_term list"
  assumes "Γ (Fun f T) = TAtom Value"
  shows "(n. f = Val n)  (bs. f = Abs bs)  (n. f = PubConst Value n)"
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 Anaf_keys_not_val_terms:
  assumes "Anaf f = (K, T)"
    and "k  set K"
    and "g  funs_term k"
  shows "¬is_Val g"
    and "¬is_PubConstValue g"
    and "¬is_Abs 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
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } moreover {
    assume "is_PubConstValue g"
    then obtain n S where *: "Fun (PubConst Value n) S  subtermsset (set K)"
      using assms(2) funs_term_Fun_subterm[OF assms(3)]
      unfolding is_PubConstValue_def by (cases g) auto
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } moreover {
    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
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } ultimately show "¬is_Val g" "¬is_PubConstValue g" "¬is_Abs g" by metis+
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,'lbl) 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,'lbl) 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_PubConstValue g"
  shows "g  funs_term k. ¬is_PubConstValue g"
using assms(3,4) Anaf_keys_not_val_terms(1,2)[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,'lbl) 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_val_terms(3)[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,'lbl) 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 Ana_Fu_keys_length_eq:
  assumes "length T = length S"
  shows "length (fst (Ana (Fun (Fu f) T))) = length (fst (Ana (Fun (Fu f) S)))"
proof (cases "arityf f = length T  arityf f > 0")
  case True thus ?thesis using assms by (cases "Anaf f") auto
next
  case False thus ?thesis using assms by force
qed

lemma Ana_key_PubConstValue_subterm_in_term: 
  fixes k::"('fun,'atom,'sets,'lbl) prot_term"
  assumes KR: "Ana t = (K, R)"
    and k: "k  set K"
    and n: "Fun (PubConst Value n) []  k"
  shows "Fun (PubConst Value n) []  t"
proof (cases t)
  case (Var x) thus ?thesis using KR k n by force
next
  case (Fun f ts)
  note t = this
  then obtain g where f: "f = Fu g" using KR k by (cases f) auto
  obtain K' R' where KR': "Anaf g = (K', R')" by fastforce

  have K: "K = K' list (!) ts"
    using k Ana_Fu_elim(2)[OF KR[unfolded t] f KR'] by force

  obtain k' where k': "k'  set K'" "k = k'  (!) ts" using k K by auto

  have 0: "¬(Fun (PubConst Value n) []  k')"
  proof
    assume *: "Fun (PubConst Value n) []  k'"
    have **: "PubConst Value n  funs_term k'"
      using funs_term_Fun_subterm'[OF *] by (cases k') auto
    show False
      using Anaf_keys_not_val_terms(2)[OF KR' k'(1) **]
      unfolding is_PubConstValue_def by force
  qed
  hence "i  fv k'. Fun (PubConst Value n) []  ts ! i"
    by (metis n const_subterm_subst_var_obtain k'(2))
  then obtain i where i: "i  fv k'" "Fun (PubConst Value n) []  ts ! i" by blast

  have "i < length ts"
    using i(1) KR' k'(1) Anaf_assm2_alt[OF KR', of i]
          Ana_Fu_elim(1)[OF KR[unfolded t] f KR'] k
    by fastforce
  thus ?thesis using i(2) unfolding t by force
qed

lemma deduct_occurs_in_ik:
  fixes t::"('fun,'atom,'sets,'lbl) 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 deduct_val_const_swap:
  fixes θ σ::"('fun,'atom,'sets,'lbl) prot_subst"
  assumes "M set θ  t  θ"
    and "x  fvset M  fv t. (n. θ x = Fun (Val n) [])  (n. θ x = Fun (PubConst Value n) [])"
    and "x  fvset M  fv t. (n. σ x = Fun (Val n) [])"
    and "x  fvset M  fv t. (n. θ x = Fun (PubConst Value n) [])  σ x  M  N"
    and "x  fvset M  fv t. (n. θ x = Fun (Val n) [])  θ x = σ x"
    and "x  fvset M  fv t. y  fvset M  fv t. θ x = θ y  σ x = σ y"
    and "n. ¬(Fun (PubConst Value n) [] set insert t M)"
  shows "(M set σ)  N  t  σ"
proof -
  obtain n where n: "intruder_deduct_num (M set θ) n (t  θ)"
    using assms(1) deduct_num_if_deduct by blast
  hence "m  n. intruder_deduct_num ((M set σ)  N) m (t  σ)" using assms(2-)
  proof (induction n arbitrary: t rule: nat_less_induct)
    case (1 n)
    note prems = "1.prems"
    note IH = "1.IH"

    show ?case
    proof (cases "t  θ  M set θ")
      case True
      note 2 = this
      have 3: "x  fvset M  fv t. c. θ x = Fun c []"
              "x  fvset M  fv t. c. σ x = Fun c []"
        using prems(2,3) by (blast, blast)
      have "t  σ  M set σ"
        using subst_const_swap_eq_mem[OF 2 _ 3 prems(6)] prems(2,5,7) by metis
      thus ?thesis using intruder_deduct_num.AxiomN by auto
    next
      case False
      then obtain n' where n: "n = Suc n'" using prems(1) deduct_zero_in_ik by (cases n) fast+

      have M_subterms_eq:
          "subtermsset (M set θ) = subtermsset M set θ"
          "subtermsset (M set σ) = subtermsset M set σ"
        subgoal using prems(2) subterms_subst''[of M θ] by blast
        subgoal using prems(3) subterms_subst''[of M σ] by blast
        done

      from deduct_inv[OF prems(1)] show ?thesis
      proof (elim disjE)
        assume "t  θ  M set θ" thus ?thesis using False by argo
      next
        assume "f ts. t  θ = Fun f ts  public f  length ts = arity f 
                     (t  set ts. l < n. intruder_deduct_num (M set θ) l t)"
        then obtain f ts where t:
            "t  θ = Fun f ts" "public f" "length ts = arity f"
            "t  set ts. l < n. intruder_deduct_num (M set θ) l t"
          by blast
  
        show ?thesis
        proof (cases t)
          case (Var x)
          hence ts: "ts = []" and f: "c. f = PubConst Value c"
            using t(1,2) prems(2) by (force, auto)
          have "σ x  M  N" using prems(4) Var f ts t(1) by auto
          moreover have "fv (σ x) = {}" using prems(3) Var by auto
          hence "σ x  M set σ" when "σ x  M" using that subst_ground_ident[of "σ x" σ] by force
          ultimately have "σ x  (M set σ)  N" by fast
          thus ?thesis using intruder_deduct_num.AxiomN Var by force
        next
          case (Fun g ss)
          hence f: "f = g" and ts: "ts = ss list θ" using t(1) by auto
  
          have ss: "l < n. intruder_deduct_num (M set θ) l (s  θ)" when s: "s  set ss" for s
            using t(4) ts s by auto
  
          have IH': "l < n. intruder_deduct_num ((M set σ)  N) l (s  σ)"
            when s: "s  set ss" for s
          proof -
            obtain l where l: "l < n" "intruder_deduct_num (M set θ) l (s  θ)"
              using ss s by blast
            
            have *: "fv s  fv t" "subtermsset (insert s M)  subtermsset (insert t M)"
              using s unfolding Fun f ts by auto

            have "l'  l. intruder_deduct_num ((M set σ)  N) l' (s  σ)"
            proof -
              have "x  fvset M  fv s.
                      (n. θ x = Fun (Val n) [])  (n. θ x = Fun (PubConst Value n) [])"
                   "x  fvset M  fv s. n. σ x = Fun (Val n) []"
                   "x  fvset M  fv s. (n. θ x = Fun (PubConst Value n) [])  σ x  M  N"
                   "x  fvset M  fv s. (n. θ x = Fun (Val n) [])  θ x = σ x"
                   "x  fvset M  fv s. y  fvset M  fv s. θ x = θ y  σ x = σ y"
                   "n. Fun (PubConst Value n) []  subtermsset (insert s M)"
                subgoal using prems(2) *(1) by blast
                subgoal using prems(3) *(1) by blast
                subgoal using prems(4) *(1) by blast
                subgoal using prems(5) *(1) by blast
                subgoal using prems(6) *(1) by blast
                subgoal using prems(7) *(2) by blast
                done
              thus ?thesis using IH l by presburger
            qed
            then obtain l' where l': "l'  l" "intruder_deduct_num ((M set σ)  N) l' (s  σ)"
              by blast

            have "l' < n" using l'(1) l(1) by linarith
            thus ?thesis using l'(2) by blast
          qed
  
          have g: "length (ss list σ) = arity g" "public g"
            using t(2,3) unfolding f ts by auto

          let ?P = "λs l. l < n  intruder_deduct_num ((M set σ)  N) l s"
          define steps where "steps  λs. SOME l. ?P s l"
  
          have 2: "steps (s  σ) < n" "intruder_deduct_num ((M set σ)  N) (steps (s  σ)) (s  σ)"
            when s: "s  set ss" for s
            using someI_ex[OF IH'[OF s]] unfolding steps_def by (blast, blast)
  
          have 3: "Suc (Max (insert 0 (steps ` set (ss list σ))))  n"
          proof (cases "ss = []")
            case True show ?thesis unfolding True n by simp
          next
            case False thus ?thesis
              using 2 Max_nat_finite_lt[of "set (ss list σ)" steps n] by (simp add: Suc_leI)
          qed
  
          show ?thesis
            using intruder_deduct_num.ComposeN[OF g, of "(M set σ)  N" steps] 2(2) 3
            unfolding Fun by auto
        qed
      next
        assume "s  subtermsset (M set θ).
                  (l < n. intruder_deduct_num (M set θ) l s) 
                  (k  set (fst (Ana s)). l < n. intruder_deduct_num (M set θ) l k) 
                  t  θ  set (snd (Ana s))"
        then obtain s l
            where s:
              "s  subtermsset M set θ"
              "k  set (fst (Ana s)). l < n. intruder_deduct_num (M set θ) l k"
              "t  θ  set (snd (Ana s))"
            and l: "l < n" "intruder_deduct_num (M set θ) l s"
          by (metis (no_types, lifting) M_subterms_eq(1))

        obtain u where u: "u set M" "s = u  θ" using s(1) by blast

        have u_fv: "fv u  fvset M" by (metis fv_subset_subterms u(1))

        have "x. u = Var x"
        proof
          assume "x. u = Var x"
          then obtain x where x: "u = Var x" by blast
          then obtain c where c: "s = Fun c []" using u prems(2) u_fv by auto
          thus False using s(3) Ana_subterm by (cases "Ana s") force
        qed
        then obtain f ts where u': "u = Fun f ts" by (cases u) auto

        obtain K R where KR: "Ana u = (K,R)" by (metis surj_pair)

        have KR': "Ana s = (K list θ, R list θ)"
          using KR Ana_subst'[OF KR[unfolded u'], of θ] unfolding u(2) u' by blast
        hence s': 
            "k  set K. l < n. intruder_deduct_num (M set θ) l (k  θ)"
            "t  θ  set (R list θ)"
          using s(2,3) by auto

        have IH1: "l < n. intruder_deduct_num ((M set σ)  N) l (u  σ)"
        proof -
          have "subterms u  subtermsset M" using u(1) subterms_subset by auto
          hence "subtermsset (insert u M) = subtermsset M" by blast
          hence *: "subtermsset (insert u M)  subtermsset (insert t M)" by auto

          have "l'  l. intruder_deduct_num ((M set σ)  N) l' (u  σ)"
          proof -
            have "x  fvset M  fv u.
                    (n. θ x = Fun (Val n) [])  (n. θ x = Fun (PubConst Value n) [])"
                 "x  fvset M  fv u. n. σ x = Fun (Val n) []"
                 "x  fvset M  fv u. (n. θ x = Fun (PubConst Value n) [])  σ x  M  N"
                 "x  fvset M  fv u. (n. θ x = Fun (Val n) [])  θ x = σ x"
                 "x  fvset M  fv u. y  fvset M  fv u. θ x = θ y  σ x = σ y"
                 "n. Fun (PubConst Value n) []  subtermsset (insert u M)"
              subgoal using prems(2) u_fv by blast
              subgoal using prems(3) u_fv by blast
              subgoal using prems(4) u_fv by blast
              subgoal using prems(5) u_fv by blast
              subgoal using prems(6) u_fv by blast
              subgoal using prems(7) * by blast
              done
            thus ?thesis using IH l unfolding u(2) by presburger
          qed
          then obtain l' where l': "l'  l" "intruder_deduct_num ((M set σ)  N) l' (u  σ)"
            by blast

          have "l' < n" using l'(1) l(1) by linarith
          thus ?thesis using l'(2) by blast
        qed

        have IH2: "l < n. intruder_deduct_num ((M set σ)  N) l (k  σ)" when k: "k  set K" for k
          using k IH prems(2-) Anaf_keys_not_val_terms s'(1) KR u(1)
        proof -
          have *: "fv k  fvset M" using k KR Ana_keys_fv u(1) fv_subset_subterms by blast

          have **: "Fun (PubConst Value n) [] set M" when "Fun (PubConst Value n) []  k" for n
            using in_subterms_subset_Union[OF u(1)]
                  Ana_key_PubConstValue_subterm_in_term[OF KR k that]
            by fast

          obtain lk where lk: "lk < n" "intruder_deduct_num (M set θ) lk (k  θ)"
            using s'(1) k by fast

          have "l'  lk. intruder_deduct_num ((M set σ)  N) l' (k  σ)"
          proof -
            have "x  fvset M  fv k.
                    (n. θ x = Fun (Val n) [])  (n. θ x = Fun (PubConst Value n) [])"
                 "x  fvset M  fv k. n. σ x = Fun (Val n) []"
                 "x  fvset M  fv k. (n. θ x = Fun (PubConst Value n) [])  σ x  M  N"
                 "x  fvset M  fv k. (n. θ x = Fun (Val n) [])  θ x = σ x"
                 "x  fvset M  fv k. y  fvset M  fv k. θ x = θ y  σ x = σ y"
                 "n. Fun (PubConst Value n) []  subtermsset (insert k M)"
              subgoal using prems(2) * by blast
              subgoal using prems(3) * by blast
              subgoal using prems(4) * by blast
              subgoal using prems(5) * by blast
              subgoal using prems(6) * by blast
              subgoal using prems(7) ** by blast
              done
            thus ?thesis using IH lk by presburger
          qed
          then obtain lk' where lk': "lk'  lk" "intruder_deduct_num ((M set σ)  N) lk' (k  σ)"
            by blast

          have "lk' < n" using lk'(1) lk(1) by linarith
          thus ?thesis using lk'(2) by blast
        qed

        have KR'': "Ana (u  σ) = (K list σ, R list σ)"
          using Ana_subst' KR unfolding u' by blast

        obtain r where r: "r  set R" "t  θ = r  θ"
          using s'(2) by fastforce

        have r': "t  σ  set (R list σ)"
        proof -
          have r_subterm_u: "r  u" using r(1) KR Ana_subterm by blast

          have r_fv: "fv r  fvset M"
            by (meson r_subterm_u u(1) fv_subset_subterms in_mono in_subterms_subset_Union)

          have t_subterms_M: "subterms t  subtermsset (insert t M)"
            by blast

          have r_subterm_M: "subterms r  subtermsset (insert t M)"
            using subterms_subset[OF r_subterm_u] in_subterms_subset_Union[OF u(1)]
            by (auto intro: subtermsset_mono)

          have *: "x  fv t  fv r. θ x = σ x  ¬(θ x  t)  ¬(θ x  r)"
          proof
            fix x assume "x  fv t  fv r"
            hence "x  fvset M  fv t" using r_fv by blast
            thus "θ x = σ x  ¬(θ x  t)  ¬(θ x  r)"
              using prems(2,5,7) r_subterm_M t_subterms_M
              by (metis (no_types, opaque_lifting) in_mono)
          qed

          have **: "x  fv t  fv r. c. θ x = Fun c []"
                   "x  fv t  fv r. c. σ x = Fun c []"
                   "x  fv t  fv r. y  fv t  fv r. θ x = θ y  σ x = σ y"
            subgoal using prems(2) r_fv by blast
            subgoal using prems(3) r_fv by blast
            subgoal using prems(6) r_fv by blast
            done
          
          have "t  σ = r  σ" by (rule subst_const_swap_eq'[OF r(2) * **])
          thus ?thesis using r(1) by simp
        qed

        obtain l1 where l1: "l1 < n" "intruder_deduct_num ((M set σ)  N) l1 (u  σ)"
          using IH1 by blast

        let ?P = "λs l. l < n  intruder_deduct_num ((M set σ)  N) l s"
        define steps where "steps  λs. SOME l. ?P s l"

        have 2: "steps (k  σ) < n" "intruder_deduct_num ((M set σ)  N) (steps (k  σ)) (k  σ)"
          when k: "k  set K" for k
          using someI_ex[OF IH2[OF k]] unfolding steps_def by (blast, blast)

        have 3: "Suc (Max (insert l1 (steps ` set (K list σ))))  n"
        proof (cases "K = []")
          case True show ?thesis using l1(1) unfolding True n by simp
        next
          case False thus ?thesis
            using l1(1) 2 Max_nat_finite_lt[of "set (K list σ)" steps n] by (simp add: Suc_leI)
        qed

        have IH2': "intruder_deduct_num ((M set σ)  N) (steps k) k"
          when k: "k  set (K list σ)" for k
          using IH2 k 2 by auto

        show ?thesis
          using l1(1) intruder_deduct_num.DecomposeN[OF l1(2) KR'' IH2' r'] 3 by fast
      qed
    qed
  qed
  thus ?thesis using deduct_if_deduct_num by blast
qed

lemma constraint_model_Nil:
  assumes I: "interpretationsubst I" "wftrms (subst_range I)"
  shows "constraint_model I []"
using I unfolding constraint_model_def by simp

lemma welltyped_constraint_model_Nil:
  assumes I: "wtsubst I" "interpretationsubst I" "wftrms (subst_range I)"
  shows "welltyped_constraint_model I []"
using I(1) constraint_model_Nil[OF I(2,3)] unfolding welltyped_constraint_model_def by simp

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 welltyped_constraint_model_deduct_append:
  assumes "welltyped_constraint_model I A"
    and "iklsst A set I  s  I"
  shows "welltyped_constraint_model I (A@[(l,send⟨[s])])"
using assms strand_sem_append_stateful[of "{}" "{}" "unlabel A" _ I]
unfolding welltyped_constraint_model_def constraint_model_def by simp

lemma welltyped_constraint_model_deduct_split:
  assumes "welltyped_constraint_model I (A@[(l,send⟨[s])])"
  shows "welltyped_constraint_model I A"
    and "iklsst A set I  s  I"
using assms strand_sem_append_stateful[of "{}" "{}" "unlabel A" _ I]
unfolding welltyped_constraint_model_def constraint_model_def by simp_all

lemma welltyped_constraint_model_deduct_iff:
  "welltyped_constraint_model I (A@[(l,send⟨[s])]) 
    welltyped_constraint_model I A  iklsst A set I  s  I"
by (metis welltyped_constraint_model_deduct_append welltyped_constraint_model_deduct_split)  

lemma welltyped_constraint_model_attack_if_receive_attack:
  assumes I: "welltyped_constraint_model  𝒜"
    and rcv_attack: "receive⟨ts  set (unlabel 𝒜)" "attack⟨n  set ts"
  shows "welltyped_constraint_model  (𝒜@[(l, send⟨[attack⟨n])])"
proof -
  have "iklsst 𝒜 set   attack⟨n"
    using rcv_attack in_iksst_iff[of "attack⟨n" "unlabel 𝒜"]
          ideduct_subst[OF intruder_deduct.Axiom[of "attack⟨n" "iklsst 𝒜"], of ]
    by auto
  thus ?thesis
    using I strand_sem_append_stateful[of "{}" "{}" "unlabel 𝒜" "[send⟨[attack⟨n]]" ]
    unfolding welltyped_constraint_model_def constraint_model_def by auto
qed

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

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⟨ts  set (unlabel (transaction_receive T lsst θ))"
  shows "t  set ts. 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⟨ts) = duallsstp ((l,s) lsstp θ)"
      "prefix ((B lsst θ)@[(l,s) lsstp θ]) (transaction_receive T lsst θ)"
    using s duallsst_unlabel_steps_iff(2)[of ts "transaction_receive T lsst θ"]
          duallsst_in_set_prefix_obtain_subst[of "send⟨ts" "transaction_receive T" θ]
    by blast

  have 1: "unlabel (duallsst ((B lsst θ)@[(l,s) lsstp θ])) = unlabel (duallsst (B lsst θ))@[send⟨ts]"
    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⟨ts]) "
    using B 1 unfolding prefix_def unlabel_def
    by (metis duallsst_def map_append strand_sem_append_stateful) 
  hence t_deduct: "t  set ts. IK  (iklsst (duallsst (B lsst θ)) set )  t  "
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B lsst θ))" "[send⟨ts]" ]
    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. ts. s = send⟨ts" 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_pos_checks:
  assumes T_valid: "wellformed_transaction T"
    and : "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T lsst θ))) "
  shows "ac: t  u  set (unlabel (transaction_checks T lsst θ))  (t  , u  )  DB"
    and "ac: t  u  set (unlabel (transaction_checks T lsst θ))  t   = u  "
proof -
  let ?s = "ac: t  u"
  let ?s' = "ac: t  u"
  let ?C = "set (unlabel (transaction_checks T lsst θ))"
  let ?R = "transaction_receive 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_checks T)"
  let ?P = "λa. is_Receive a  is_Check_or_Assignment a"
  let ?Q = "λa. is_Send a  is_Check_or_Assignment a"
  let ?dbupd = "λB. dbupdsst (unlabel (duallsst (B lsst θ)))  DB"

  have s_in: "?s  ?C  ?s  set (unlabel (?R lsst θ))"
             "?s'  ?C  ?s'  set (unlabel (?R lsst θ))"
    using subst_lsst_append[of "transaction_receive T"]
          unlabel_append[of "transaction_receive T"]
    by auto

  have 1: "unlabel (duallsst ((B lsst θ)@[(l,s) lsstp θ])) = unlabel (duallsst (B lsst θ))@[s']"
    when B: "(l,s') = duallsstp ((l,s) lsstp θ)" "s' = ac: t  u  s' = ac: t  u"
    for l s s' and B::"('fun,'atom,'sets,'lbl) prot_strand"
    using B 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<