Theory Stateful_Protocol_Verification

(*  Title:      Stateful_Protocol_Verification.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 Verification›
theory Stateful_Protocol_Verification
imports Stateful_Protocol_Model Term_Implication
begin

subsection ‹Fixed-Point Intruder Deduction Lemma›
context stateful_protocol_model
begin

abbreviation pubval_terms::"('fun,'atom,'sets,'lbl) prot_terms" where
  "pubval_terms ≡ {t. ∃f ∈ funs_term t. is_PubConstValue f}"

abbreviation abs_terms::"('fun,'atom,'sets,'lbl) prot_terms" where
  "abs_terms ≡ {t. ∃f ∈ funs_term t. is_Abs f}"

definition intruder_deduct_GSMP::
  "[('fun,'atom,'sets,'lbl) prot_terms,
    ('fun,'atom,'sets,'lbl) prot_terms,
    ('fun,'atom,'sets,'lbl) prot_term]
    ⇒ bool" ("⟨_;_⟩ ⊢GSMP _" 50)
where
  "⟨M; T⟩ ⊢GSMP t ≡ intruder_deduct_restricted M (λt. t ∈ GSMP T - (pubval_terms ∪ abs_terms)) t"

lemma intruder_deduct_GSMP_induct[consumes 1, case_names AxiomH ComposeH DecomposeH]:
  assumes "⟨M; T⟩ ⊢GSMP t" "⋀t. t ∈ M ⟹ P M t"
          "⋀S f. ⟦length S = arity f; public f;
                  ⋀s. s ∈ set S ⟹ ⟨M; T⟩ ⊢GSMP s;
                  ⋀s. s ∈ set S ⟹ P M s;
                  Fun f S ∈ GSMP T - (pubval_terms ∪ abs_terms)
                  ⟧ ⟹ P M (Fun f S)"
          "⋀t K T' ti. ⟦⟨M; T⟩ ⊢GSMP t; P M t; Ana t = (K, T'); ⋀k. k ∈ set K ⟹ ⟨M; T⟩ ⊢GSMP k;
                        ⋀k. k ∈ set K ⟹ P M k; ti ∈ set T'⟧ ⟹ P M ti"
  shows "P M t"
proof -
  let ?Q = "λt. t ∈ GSMP T - (pubval_terms ∪ abs_terms)"
  show ?thesis
    using intruder_deduct_restricted_induct[of M ?Q t "λM Q t. P M t"] assms
    unfolding intruder_deduct_GSMP_def
    by blast
qed

lemma pubval_terms_subst:
  assumes "t ⋅ θ ∈ pubval_terms" "θ ` fv t ∩ pubval_terms = {}"
  shows "t ∈ pubval_terms"
using assms(1,2)
proof (induction t)
  case (Fun f T)
  let ?P = "λf. is_PubConstValue f"
  from Fun show ?case
  proof (cases "?P f")
    case False
    then obtain t where t: "t ∈ set T" "t ⋅ θ ∈ pubval_terms"
      using Fun.prems by auto
    hence "θ ` fv t ∩ pubval_terms = {}" using Fun.prems(2) by auto
    thus ?thesis using Fun.IH[OF t] t(1) by auto
  qed force
qed simp

lemma abs_terms_subst:
  assumes "t ⋅ θ ∈ abs_terms" "θ ` fv t ∩ abs_terms = {}"
  shows "t ∈ abs_terms"
using assms(1,2)
proof (induction t)
  case (Fun f T)
  let ?P = "λf. is_Abs f"
  from Fun show ?case
  proof (cases "?P f")
    case False
    then obtain t where t: "t ∈ set T" "t ⋅ θ ∈ abs_terms"
      using Fun.prems by auto
    hence "θ ` fv t ∩ abs_terms = {}" using Fun.prems(2) by auto
    thus ?thesis using Fun.IH[OF t] t(1) by auto
  qed force
qed simp

lemma pubval_terms_subst':
  assumes "t ⋅ θ ∈ pubval_terms" "∀n. PubConst Value n ∉ ⋃(funs_term ` (θ ` fv t))"
  shows "t ∈ pubval_terms"
proof -
  have False
    when fs: "f ∈ funs_term s" "s ∈ subtermsset (θ ` fv t)" "is_PubConstValue f"
    for f s
  proof -
    obtain T where T: "Fun f T ∈ subterms s" using funs_term_Fun_subterm[OF fs(1)] by moura
    hence "Fun f T ∈ subtermsset (θ ` fv t)" using fs(2) in_subterms_subset_Union by blast
    thus ?thesis
      using assms(2) funs_term_Fun_subterm'[of f T] fs(3)
      unfolding is_PubConstValue_def
      by (cases f) force+
  qed
  thus ?thesis using pubval_terms_subst[OF assms(1)] by auto
qed

lemma abs_terms_subst':
  assumes "t ⋅ θ ∈ abs_terms" "∀n. Abs n ∉ ⋃(funs_term ` (θ ` fv t))"
  shows "t ∈ abs_terms"
proof -
  have "¬is_Abs f" when fs: "f ∈ funs_term s" "s ∈ subtermsset (θ ` fv t)" for f s
  proof -
    obtain T where T: "Fun f T ∈ subterms s" using funs_term_Fun_subterm[OF fs(1)] by moura  
    hence "Fun f T ∈ subtermsset (θ ` fv t)" using fs(2) in_subterms_subset_Union by blast
    thus ?thesis using assms(2) funs_term_Fun_subterm'[of f T] by (cases f) auto
  qed
  thus ?thesis using abs_terms_subst[OF assms(1)] by force
qed

lemma pubval_terms_subst_range_disj:
  "subst_range θ ∩ pubval_terms = {} ⟹ θ ` fv t ∩ pubval_terms = {}"
proof (induction t)
  case (Var x) thus ?case by (cases "x ∈ subst_domain θ") auto
qed auto

lemma abs_terms_subst_range_disj:
  "subst_range θ ∩ abs_terms = {} ⟹ θ ` fv t ∩ abs_terms = {}"
proof (induction t)
  case (Var x) thus ?case by (cases "x ∈ subst_domain θ") auto
qed auto

lemma pubval_terms_subst_range_comp:
  assumes "subst_range θ ∩ pubval_terms = {}" "subst_range δ ∩ pubval_terms = {}"
  shows "subst_range (θ ∘s δ) ∩ pubval_terms = {}"
proof -
  { fix t f assume t:
      "t ∈ subst_range (θ ∘s δ)" "f ∈ funs_term t" "is_PubConstValue f"
    then obtain x where x: "(θ ∘s δ) x = t" by auto
    have "θ x ∉ pubval_terms" using assms(1) by (cases "θ x ∈ subst_range θ") force+
    hence "(θ ∘s δ) x ∉ pubval_terms"
      using assms(2) pubval_terms_subst[of "θ x" δ] pubval_terms_subst_range_disj
      by (metis (mono_tags, lifting) subst_compose_def)
    hence False using t(2,3) x by blast
  } thus ?thesis by fast
qed

lemma pubval_terms_subst_range_comp':
  assumes "(θ ` X) ∩ pubval_terms = {}" "(δ ` fvset (θ ` X)) ∩ pubval_terms = {}"
  shows "((θ ∘s δ) ` X) ∩ pubval_terms = {}"
proof -
  { fix t f assume t:
      "t ∈ (θ ∘s δ) ` X" "f ∈ funs_term t" "is_PubConstValue f"
    then obtain x where x: "(θ ∘s δ) x = t" "x ∈ X" by auto
    have "θ x ∉ pubval_terms" using assms(1) x(2) by force
    moreover have "fv (θ x) ⊆ fvset (θ ` X)" using x(2) by (auto simp add: fv_subset)
    hence "δ ` fv (θ x) ∩ pubval_terms = {}" using assms(2) by auto
    ultimately have "(θ ∘s δ) x ∉ pubval_terms"
      using pubval_terms_subst[of "θ x" δ]
      by (metis (mono_tags, lifting) subst_compose_def)
    hence False using t(2,3) x by blast
  } thus ?thesis by fast
qed

lemma abs_terms_subst_range_comp:
  assumes "subst_range θ ∩ abs_terms = {}" "subst_range δ ∩ abs_terms = {}"
  shows "subst_range (θ ∘s δ) ∩ abs_terms = {}"
proof -
  { fix t f assume t: "t ∈ subst_range (θ ∘s δ)" "f ∈ funs_term t" "is_Abs f"
    then obtain x where x: "(θ ∘s δ) x = t" by auto
    have "θ x ∉ abs_terms" using assms(1) by (cases "θ x ∈ subst_range θ") force+
    hence "(θ ∘s δ) x ∉ abs_terms"
      using assms(2) abs_terms_subst[of "θ x" δ] abs_terms_subst_range_disj
      by (metis (mono_tags, lifting) subst_compose_def)
    hence False using t(2,3) x by blast
  } thus ?thesis by fast
qed

lemma abs_terms_subst_range_comp':
  assumes "(θ ` X) ∩ abs_terms = {}" "(δ ` fvset (θ ` X)) ∩ abs_terms = {}"
  shows "((θ ∘s δ) ` X) ∩ abs_terms = {}"
proof -
  { fix t f assume t:
      "t ∈ (θ ∘s δ) ` X" "f ∈ funs_term t" "is_Abs f"
    then obtain x where x: "(θ ∘s δ) x = t" "x ∈ X" by auto
    have "θ x ∉ abs_terms" using assms(1) x(2) by force
    moreover have "fv (θ x) ⊆ fvset (θ ` X)" using x(2) by (auto simp add: fv_subset)
    hence "δ ` fv (θ x) ∩ abs_terms = {}" using assms(2) by auto
    ultimately have "(θ ∘s δ) x ∉ abs_terms"
      using abs_terms_subst[of "θ x" δ]
      by (metis (mono_tags, lifting) subst_compose_def)
    hence False using t(2,3) x by blast
  } thus ?thesis by fast
qed

context
begin
private lemma Ana_abs_aux1:
  fixes δ::"(('fun,'atom,'sets,'lbl) prot_fun, nat, ('fun,'atom,'sets,'lbl) prot_var) gsubst"
    and α::"nat ⇒ 'sets set"
  assumes "Anaf f = (K,T)"
  shows "(K ⋅list δ) ⋅αlist α = K ⋅list (λn. δ n ⋅α α)"
proof -
  { fix k assume "k ∈ set K"
    hence "k ∈ subtermsset (set K)" by force
    hence "k ⋅ δ ⋅α α = k ⋅ (λn. δ n ⋅α α)"
    proof (induction k)
      case (Fun g S)
      have "⋀s. s ∈ set S ⟹ s ⋅ δ ⋅α α = s ⋅ (λn. δ n ⋅α α)"
        using Fun.IH in_subterms_subset_Union[OF Fun.prems] Fun_param_in_subterms[of _ S g]
        by (meson contra_subsetD)
      thus ?case using Anaf_assm1_alt[OF assms Fun.prems] by (cases g) auto
    qed simp
  } thus ?thesis unfolding abs_apply_list_def by force
qed

private lemma Ana_abs_aux2:
  fixes α::"nat ⇒ 'sets set"
    and K::"(('fun,'atom,'sets,'lbl) prot_fun, nat) term list"
    and M::"nat list"
    and T::"('fun,'atom,'sets,'lbl) prot_term list"
  assumes "∀i ∈ fvset (set K) ∪ set M. i < length T"
    and "(K ⋅list (!) T) ⋅αlist α = K ⋅list (λn. T ! n ⋅α α)"
  shows "(K ⋅list (!) T) ⋅αlist α = K ⋅list (!) (map (λs. s ⋅α α) T)" (is "?A1 = ?A2")
    and "(map ((!) T) M) ⋅αlist α = map ((!) (map (λs. s ⋅α α) T)) M" (is "?B1 = ?B2")
proof -
  have "T ! i ⋅α α = (map (λs. s ⋅α α) T) ! i" when "i ∈ fvset (set K)" for i
    using that assms(1) by auto
  hence "k ⋅ (λi. T ! i ⋅α α) = k ⋅ (λi. (map (λs. s ⋅α α) T) ! i)" when "k ∈ set K" for k
    using that term_subst_eq_conv[of k "λi. T ! i ⋅α α" "λi. (map (λs. s ⋅α α) T) ! i"]
    by auto
  thus "?A1 = ?A2" using assms(2) by (force simp add: abs_apply_terms_def)

  have "T ! i ⋅α α = map (λs. s ⋅α α) T ! i" when "i ∈ set M" for i
    using that assms(1) by auto
  thus "?B1 = ?B2" by (force simp add: abs_apply_list_def)
qed

private lemma Ana_abs_aux1_set:
  fixes δ::"(('fun,'atom,'sets,'lbl) prot_fun, nat, ('fun,'atom,'sets,'lbl) prot_var) gsubst"
    and α::"nat ⇒ 'sets set"
  assumes "Anaf f = (K,T)"
  shows "(set K ⋅set δ) ⋅αset α = set K ⋅set (λn. δ n ⋅α α)"
proof -
  { fix k assume "k ∈ set K"
    hence "k ∈ subtermsset (set K)" by force
    hence "k ⋅ δ ⋅α α = k ⋅ (λn. δ n ⋅α α)"
    proof (induction k)
      case (Fun g S)
      have "⋀s. s ∈ set S ⟹ s ⋅ δ ⋅α α = s ⋅ (λn. δ n ⋅α α)"
        using Fun.IH in_subterms_subset_Union[OF Fun.prems] Fun_param_in_subterms[of _ S g]
        by (meson contra_subsetD)
      thus ?case using Anaf_assm1_alt[OF assms Fun.prems] by (cases g) auto
    qed simp
  } thus ?thesis unfolding abs_apply_terms_def by force
qed

private lemma Ana_abs_aux2_set:
  fixes α::"nat ⇒ 'sets set"
    and K::"(('fun,'atom,'sets,'lbl) prot_fun, nat) terms"
    and M::"nat set"
    and T::"('fun,'atom,'sets,'lbl) prot_term list"
  assumes "∀i ∈ fvset K ∪ M. i < length T"
    and "(K ⋅set (!) T) ⋅αset α = K ⋅set (λn. T ! n ⋅α α)"
  shows "(K ⋅set (!) T) ⋅αset α = K ⋅set (!) (map (λs. s ⋅α α) T)" (is "?A1 = ?A2")
    and "((!) T ` M) ⋅αset α = (!) (map (λs. s ⋅α α) T) ` M" (is "?B1 = ?B2")
proof -
  have "T ! i ⋅α α = (map (λs. s ⋅α α) T) ! i" when "i ∈ fvset K" for i
    using that assms(1) by auto
  hence "k ⋅ (λi. T ! i ⋅α α) = k ⋅ (λi. (map (λs. s ⋅α α) T) ! i)" when "k ∈ K" for k
    using that term_subst_eq_conv[of k "λi. T ! i ⋅α α" "λi. (map (λs. s ⋅α α) T) ! i"]
    by auto
  thus "?A1 = ?A2" using assms(2) by (force simp add: abs_apply_terms_def)

  have "T ! i ⋅α α = map (λs. s ⋅α α) T ! i" when "i ∈ M" for i
    using that assms(1) by auto
  thus "?B1 = ?B2" by (force simp add: abs_apply_terms_def)
qed

lemma Ana_abs:
  fixes t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "Ana t = (K, T)"
  shows "Ana (t ⋅α α) = (K ⋅αlist α, T ⋅αlist α)"
  using assms
proof (induction t rule: Ana.induct)
  case (1 f S)
  obtain K' T' where *: "Anaf f = (K',T')" by moura
  show ?case using 1
  proof (cases "arityf f = length S ∧ arityf f > 0")
    case True
    hence "K = K' ⋅list (!) S" "T = map ((!) S) T'"
        and **: "arityf f = length (map (λs. s ⋅α α) S)" "arityf f > 0"
      using 1 * by auto
    hence "K ⋅αlist α = K' ⋅list (!) (map (λs. s ⋅α α) S)"
          "T ⋅αlist α = map ((!) (map (λs. s ⋅α α) S)) T'"
      using Anaf_assm2_alt[OF *] Ana_abs_aux2[OF _ Ana_abs_aux1[OF *], of T' S α]
      unfolding abs_apply_list_def
      by auto
    moreover have "Fun (Fu f) S ⋅α α = Fun (Fu f) (map (λs. s ⋅α α) S)" by simp
    ultimately show ?thesis using Ana_Fu_intro[OF ** *] by metis
  qed (auto simp add: abs_apply_list_def)
qed (simp_all add: abs_apply_list_def)
end

lemma deduct_FP_if_deduct:
  fixes M IK FP::"('fun,'atom,'sets,'lbl) prot_terms"
  assumes IK: "IK ⊆ GSMP M - (pubval_terms ∪ abs_terms)" "∀t ∈ IK ⋅αset α. FP ⊢c t"
    and t: "IK ⊢ t" "t ∈ GSMP M - (pubval_terms ∪ abs_terms)"
  shows "FP ⊢ t ⋅α α"
proof -
  let ?P = "λf. ¬is_PubConstValue f"
  let ?GSMP = "GSMP M - (pubval_terms ∪ abs_terms)"

  have 1: "∀m ∈ IK. m ∈ ?GSMP"
    using IK(1) by blast

  have 2: "∀t t'. t ∈ ?GSMP ⟶ t' ⊑ t ⟶ t' ∈ ?GSMP"
  proof (intro allI impI)
    fix t t' assume t: "t ∈ ?GSMP" "t' ⊑ t"
    hence "t' ∈ GSMP M" using ground_subterm unfolding GSMP_def by auto
    moreover have "¬is_PubConstValue f"
      when "f ∈ funs_term t" for f
      using t(1) that by auto
    hence "¬is_PubConstValue f"
      when "f ∈ funs_term t'" for f
      using that subtermeq_imp_funs_term_subset[OF t(2)] by auto
    moreover have "¬is_Abs f" when "f ∈ funs_term t" for f using t(1) that by auto
    hence "¬is_Abs f" when "f ∈ funs_term t'" for f
      using that subtermeq_imp_funs_term_subset[OF t(2)] by auto
    ultimately show "t' ∈ ?GSMP" by simp
  qed

  have 3: "∀t K T k. t ∈ ?GSMP ⟶ Ana t = (K, T) ⟶ k ∈ set K ⟶ k ∈ ?GSMP"
  proof (intro allI impI)
    fix t K T k assume t: "t ∈ ?GSMP" "Ana t = (K, T)" "k ∈ set K"
    hence "k ∈ GSMP M" using GSMP_Ana_key by blast
    moreover have "∀f ∈ funs_term t. ?P f" using t(1) by auto
    with t(2,3) have "∀f ∈ funs_term k. ?P f"
    proof (induction t arbitrary: k rule: Ana.induct)
      case 1 thus ?case by (metis Ana_Fu_keys_not_pubval_terms surj_pair)
    qed auto
    moreover have "∀f ∈ funs_term t. ¬is_Abs f" using t(1) by auto
    with t(2,3) have "∀f ∈ funs_term k. ¬is_Abs f"
    proof (induction t arbitrary: k rule: Ana.induct)
      case 1 thus ?case by (metis Ana_Fu_keys_not_abs_terms surj_pair)
    qed auto
    ultimately show "k ∈ ?GSMP" by simp
  qed

  have "⟨IK; M⟩ ⊢GSMP t"
    unfolding intruder_deduct_GSMP_def
    by (rule restricted_deduct_if_deduct'[OF 1 2 3 t])
  thus ?thesis
  proof (induction t rule: intruder_deduct_GSMP_induct)
    case (AxiomH t)
    show ?case using IK(2) abs_in[OF AxiomH.hyps] by force
  next
    case (ComposeH T f)
    have *: "Fun f T ⋅α α = Fun f (map (λt. t ⋅α α) T)"
      using ComposeH.hyps(2,4)
      by (cases f) auto

    have **: "length (map (λt. t ⋅α α) T) = arity f"
      using ComposeH.hyps(1)
      by auto

    show ?case
      using intruder_deduct.Compose[OF ** ComposeH.hyps(2)] ComposeH.IH(1) *
      by auto
  next
    case (DecomposeH t K T' ti)
    have *: "Ana (t ⋅α α) = (K ⋅αlist α, T' ⋅αlist α)"
      using Ana_abs[OF DecomposeH.hyps(2)]
      by metis

    have **: "ti ⋅α α ∈ set (T' ⋅αlist α)"
      using DecomposeH.hyps(4) abs_in abs_list_set_is_set_abs_set[of T']
      by auto

    have ***: "FP ⊢ k"
      when k: "k ∈ set (K ⋅αlist α)" for k
    proof -
      obtain k' where k': "k' ∈ set K" "k = k' ⋅α α"
        by (metis (no_types) k abs_apply_terms_def imageE abs_list_set_is_set_abs_set)

      show "FP ⊢ k"
        using DecomposeH.IH k' by blast
    qed

    show ?case
      using intruder_deduct.Decompose[OF _ * _ **]
            DecomposeH.IH(1) ***(1)
      by blast
  qed
qed

end


subsection ‹Computing and Checking Term Implications and Messages›
context stateful_protocol_model
begin

abbreviation (input) "absc s ≡ (Fun (Abs s) []::('fun,'atom,'sets,'lbl) prot_term)"

fun absdbupd where
  "absdbupd [] _ a = a"
| "absdbupd (insert⟨Var y, Fun (Set s) T⟩#D) x a = (
    if x = y then absdbupd D x (insert s a) else absdbupd D x a)"
| "absdbupd (delete⟨Var y, Fun (Set s) T⟩#D) x a = (
    if x = y then absdbupd D x (a - {s}) else absdbupd D x a)"
| "absdbupd (_#D) x a = absdbupd D x a"

lemma absdbupd_cons_cases:
  "absdbupd (insert⟨Var x, Fun (Set s) T⟩#D) x d = absdbupd D x (insert s d)"
  "absdbupd (delete⟨Var x, Fun (Set s) T⟩#D) x d = absdbupd D x (d - {s})"
  "t ≠ Var x ∨ (∄s T. u = Fun (Set s) T) ⟹ absdbupd (insert⟨t,u⟩#D) x d = absdbupd D x d"
  "t ≠ Var x ∨ (∄s T. u = Fun (Set s) T) ⟹ absdbupd (delete⟨t,u⟩#D) x d = absdbupd D x d"
proof -
  assume *: "t ≠ Var x ∨ (∄s T. u = Fun (Set s) T)"
  let ?P = "absdbupd (insert⟨t,u⟩#D) x d = absdbupd D x d"
  let ?Q = "absdbupd (delete⟨t,u⟩#D) x d = absdbupd D x d"
  { fix y f T assume "t = Fun f T ∨ u = Var y" hence ?P ?Q by auto
  } moreover {
    fix y f T assume "t = Var y" "u = Fun f T" hence ?P using * by (cases f) auto
  } moreover {
    fix y f T assume "t = Var y" "u = Fun f T" hence ?Q using * by (cases f) auto
  } ultimately show ?P ?Q by (metis term.exhaust)+
qed simp_all

lemma absdbupd_filter: "absdbupd S x d = absdbupd (filter is_Update S) x d"
by (induction S x d rule: absdbupd.induct) simp_all

lemma absdbupd_append:
  "absdbupd (A@B) x d = absdbupd B x (absdbupd A x d)"
proof (induction A arbitrary: d)
  case (Cons a A) thus ?case
  proof (cases a)
    case (Insert t u) thus ?thesis
    proof (cases "t ≠ Var x ∨ (∄s T. u = Fun (Set s) T)")
      case False
      then obtain s T where "t = Var x" "u = Fun (Set s) T" by moura
      thus ?thesis by (simp add: Insert Cons.IH absdbupd_cons_cases(1))
    qed (simp_all add: Cons.IH absdbupd_cons_cases(3))
  next
    case (Delete t u) thus ?thesis
    proof (cases "t ≠ Var x ∨ (∄s T. u = Fun (Set s) T)")
      case False
      then obtain s T where "t = Var x" "u = Fun (Set s) T" by moura
      thus ?thesis by (simp add: Delete Cons.IH absdbupd_cons_cases(2))
    qed (simp_all add: Cons.IH absdbupd_cons_cases(4))
  qed simp_all
qed simp

lemma absdbupd_wellformed_transaction:
  assumes T: "wellformed_transaction T"
  shows "absdbupd (unlabel (transaction_strand T)) = absdbupd (unlabel (transaction_updates T))"
proof -
  define S0 where "S0 ≡ unlabel (transaction_strand T)"
  define S1 where "S1 ≡ unlabel (transaction_receive T)"
  define S2 where "S2 ≡ unlabel (transaction_checks T)"
  define S3 where "S3 ≡ unlabel (transaction_updates T)"
  define S4 where "S4 ≡ unlabel (transaction_send T)"

  note S_defs = S0_def S1_def S2_def S3_def S4_def

  have 0: "list_all is_Receive S1"
          "list_all is_Check_or_Assignment S2"
          "list_all is_Update S3"
          "list_all is_Send S4"
    using T unfolding wellformed_transaction_def S_defs by metis+

  have "filter is_Update S1 = []"
       "filter is_Update S2 = []"
       "filter is_Update S3 = S3"
       "filter is_Update S4 = []"
    using list_all_filter_nil[OF 0(1), of is_Update]
          list_all_filter_nil[OF 0(2), of is_Update]
          list_all_filter_eq[OF 0(3)]
          list_all_filter_nil[OF 0(4), of is_Update]
    by blast+
  moreover have "S0 = S1@S2@S3@S4"
    unfolding S_defs transaction_strand_def unlabel_def by auto
  ultimately have "filter is_Update S0 = S3"
    using filter_append[of is_Update] list_all_append[of is_Update]
    by simp
  thus ?thesis
    using absdbupd_filter[of S0]
    unfolding S_defs by presburger
qed

fun abs_substs_set::
  "[('fun,'atom,'sets,'lbl) prot_var list,
    'sets set list,
    ('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set,
    ('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set,
    ('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set ⇒ bool]
  ⇒ ((('fun,'atom,'sets,'lbl) prot_var × 'sets set) list) list"
where
  "abs_substs_set [] _ _ _ _ = [[]]"
| "abs_substs_set (x#xs) as posconstrs negconstrs msgconstrs = (
    let bs = filter (λa. posconstrs x ⊆ a ∧ a ∩ negconstrs x = {} ∧ msgconstrs x a) as;
        Δ = abs_substs_set xs as posconstrs negconstrs msgconstrs
    in concat (map (λb. map (λδ. (x, b)#δ) Δ) bs))"

definition abs_substs_fun::
  "[(('fun,'atom,'sets,'lbl) prot_var × 'sets set) list,
    ('fun,'atom,'sets,'lbl) prot_var]
  ⇒ 'sets set"
where
  "abs_substs_fun δ x = (case find (λb. fst b = x) δ of Some (_,a) ⇒ a | None ⇒ {})"

lemmas abs_substs_set_induct = abs_substs_set.induct[case_names Nil Cons]

fun transaction_poschecks_comp::
  "(('fun,'atom,'sets,'lbl) prot_fun, ('fun,'atom,'sets,'lbl) prot_var) stateful_strand
  ⇒ (('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set)"
where
  "transaction_poschecks_comp [] = (λ_. {})"
| "transaction_poschecks_comp (⟨_: Var x ∈ Fun (Set s) []⟩#T) = (
    let f = transaction_poschecks_comp T in f(x := insert s (f x)))"
| "transaction_poschecks_comp (_#T) = transaction_poschecks_comp T"

fun transaction_negchecks_comp::
  "(('fun,'atom,'sets,'lbl) prot_fun, ('fun,'atom,'sets,'lbl) prot_var) stateful_strand
  ⇒ (('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set)"
where
  "transaction_negchecks_comp [] = (λ_. {})"
| "transaction_negchecks_comp (⟨Var x not in Fun (Set s) []⟩#T) = (
    let f = transaction_negchecks_comp T in f(x := insert s (f x)))"
| "transaction_negchecks_comp (_#T) = transaction_negchecks_comp T"

definition transaction_check_pre where
  "transaction_check_pre FPT T δ ≡
    let (FP, _, TI) = FPT;
        C = set (unlabel (transaction_checks T));
        xs = fv_listsst (unlabel (transaction_strand T));
        θ = λδ x. if fst x = TAtom Value then (absc ∘ δ) x else Var x
    in (∀x ∈ set (transaction_fresh T). δ x = {}) ∧
       (∀t ∈ trmslsst (transaction_receive T). intruder_synth_mod_timpls FP TI (t ⋅ θ δ)) ∧
       (∀u ∈ C.
          (is_InSet u ⟶ (
            let x = the_elem_term u; s = the_set_term u
            in (is_Var x ∧ is_Fun_Set s) ⟶ the_Set (the_Fun s) ∈ δ (the_Var x))) ∧
          ((is_NegChecks u ∧ bvarssstp u = [] ∧ the_eqs u = [] ∧ length (the_ins u) = 1) ⟶ (
            let x = fst (hd (the_ins u)); s = snd (hd (the_ins u))
            in (is_Var x ∧ is_Fun_Set s) ⟶ the_Set (the_Fun s) ∉ δ (the_Var x))))"

definition transaction_check_post where
  "transaction_check_post FPT T δ ≡
    let (FP, _, TI) = FPT;
        xs = fv_listsst (unlabel (transaction_strand T));
        θ = λδ x. if fst x = TAtom Value then (absc ∘ δ) x else Var x;
        u = λδ x. absdbupd (unlabel (transaction_updates T)) x (δ x)
    in (∀x ∈ set xs - set (transaction_fresh T). δ x ≠ u δ x ⟶ List.member TI (δ x, u δ x)) ∧
       (∀t ∈ trmslsst (transaction_send T). intruder_synth_mod_timpls FP TI (t ⋅ θ (u δ)))"

definition fun_point_inter where "fun_point_inter f g ≡ λx. f x ∩ g x"
definition fun_point_union where "fun_point_union f g ≡ λx. f x ∪ g x"
definition fun_point_Inter where "fun_point_Inter fs ≡ λx. ⋂f ∈ fs. f x"
definition fun_point_Union where "fun_point_Union fs ≡ λx. ⋃f ∈ fs. f x"
definition fun_point_Inter_list where "fun_point_Inter_list fs ≡ λx. ⋂(set (map (λf. f x) fs))"
definition fun_point_Union_list where "fun_point_Union_list fs ≡ λx. ⋃(set (map (λf. f x) fs))"
definition ticl_abs where "ticl_abs TI a ≡ set (a#map snd (filter (λp. fst p = a) TI))"
definition ticl_abss where "ticl_abss TI as ≡ ⋃a ∈ as. ticl_abs TI a"

lemma fun_point_Inter_set_eq:
  "fun_point_Inter (set fs) = fun_point_Inter_list fs"
unfolding fun_point_Inter_def fun_point_Inter_list_def by simp

lemma fun_point_Union_set_eq:
  "fun_point_Union (set fs) = fun_point_Union_list fs"
unfolding fun_point_Union_def fun_point_Union_list_def by simp

lemma ticl_abs_refl_in: "x ∈ ticl_abs TI x"
unfolding ticl_abs_def by simp

lemma ticl_abs_iff:
  assumes TI: "set TI = {(a,b) ∈ (set TI)+. a ≠ b}"
  shows "ticl_abs TI a = {b. (a,b) ∈ (set TI)*}"  
proof (intro order_antisym subsetI)
  fix x assume x: "x ∈ {b. (a, b) ∈ (set TI)*}"
  hence "x = a ∨ (x ≠ a ∧ (a,x) ∈ (set TI)+)" by (metis mem_Collect_eq rtranclD)
  moreover have "ticl_abs TI a = {a} ∪ {b. (a,b) ∈ set TI}" unfolding ticl_abs_def by force
  ultimately show "x ∈ ticl_abs TI a" using TI by blast
qed (fastforce simp add: ticl_abs_def)

lemma ticl_abs_Inter:
  assumes xs: "⋂(ticl_abs TI ` xs) ≠ {}"
    and TI: "set TI = {(a,b) ∈ (set TI)+. a ≠ b}"
  shows "⋂(ticl_abs TI ` ⋂(ticl_abs TI ` xs)) ⊆ ⋂(ticl_abs TI ` xs)"
proof
  fix x assume x: "x ∈ ⋂(ticl_abs TI ` ⋂(ticl_abs TI ` xs))"
  have *: "⋂(ticl_abs TI ` xs) = {b. ∀a ∈ xs. (a,b) ∈ (set TI)*}"
    unfolding ticl_abs_iff[OF TI] by blast

  have "(b,x) ∈ (set TI)*" when b: "∀a ∈ xs. (a,b) ∈ (set TI)*" for b
    using x b unfolding ticl_abs_iff[OF TI] by blast
  hence "(a,x) ∈ (set TI)*" when "a ∈ xs" for a
    using that xs rtrancl.rtrancl_into_rtrancl[of a _ "(set TI)*" x]
    unfolding * rtrancl_idemp[of "set TI"] by blast
  thus "x ∈ ⋂(ticl_abs TI ` xs)" unfolding * by blast
qed

function (sequential) match_abss'
::"(('a,'b,'c,'d) prot_fun, 'e) term ⇒
   (('a,'b,'c,'d) prot_fun, 'e) term ⇒
   ('e ⇒ 'c set set) option"
where
  "match_abss' (Var x) (Fun (Abs a) _) = Some ((λ_. {})(x := {a}))"
| "match_abss' (Fun f ts) (Fun g ss) = (
    if f = g ∧ length ts = length ss
    then map_option fun_point_Union_list (those (map2 match_abss' ts ss))
    else None)"
| "match_abss' _ _ = None"
by pat_completeness auto
termination
proof -
  let ?m = "measures [size ∘ fst]"

  have 0: "wf ?m" by simp

  show ?thesis
    apply (standard, use 0 in fast)
    by (metis (no_types) comp_def fst_conv measures_less Fun_zip_size_lt(1))
qed

definition match_abss where
  "match_abss OCC TI t s ≡ (
    let xs = fv t;
        OCC' = set OCC;
        f = λδ x. if x ∈ xs then δ x else OCC';
        g = λδ x. ⋂(ticl_abs TI ` δ x)
    in case match_abss' t s of
      Some δ ⇒
        let δ' = g δ
        in if ∀x ∈ xs. δ' x ≠ {} then Some (f δ') else None
    | None ⇒ None)"

lemma match_abss'_Var_inv:
  assumes δ: "match_abss' (Var x) t = Some δ"
  shows "∃a ts. t = Fun (Abs a) ts ∧ δ = (λ_. {})(x := {a})"
proof -
  obtain f ts where t: "t = Fun f ts" using δ by (cases t) auto
  then obtain a where a: "f = Abs a" using δ by (cases f) auto
  show ?thesis using δ unfolding t a by simp 
qed

lemma match_abss'_Fun_inv:
  assumes "match_abss' (Fun f ts) (Fun g ss) = Some δ"
  shows "f = g" (is ?A)
    and "length ts = length ss" (is ?B)
    and "∃θ. Some θ = those (map2 match_abss' ts ss) ∧ δ = fun_point_Union_list θ" (is ?C)
    and "∀(t,s) ∈ set (zip ts ss). ∃σ. match_abss' t s = Some σ" (is ?D)
proof -
  note 0 = assms match_abss'.simps(2)[of f ts g ss] option.distinct(1)
  show ?A by (metis 0)
  show ?B by (metis 0)
  show ?C by (metis (no_types, opaque_lifting) 0 map_option_eq_Some)
  thus ?D using map2_those_Some_case[of match_abss' ts ss] by fastforce
qed

lemma match_abss'_FunI:
  assumes Δ: "⋀i. i < length T ⟹ match_abss' (U ! i) (T ! i) = Some (Δ i)"
    and T: "length T = length U"
  shows "match_abss' (Fun f U) (Fun f T) = Some (fun_point_Union_list (map Δ [0..<length T]))"
proof -
  have "match_abss' (Fun f U) (Fun f T) =
          map_option fun_point_Union_list (those (map2 match_abss' U T))"
    using T match_abss'.simps(2)[of f U f T] by presburger
  moreover have "those (map2 match_abss' U T) = Some (map Δ [0..<length T])"
    using Δ T those_map2_SomeI by metis
  ultimately show ?thesis by simp
qed

lemma match_abss'_Fun_param_subset:
  assumes "match_abss' (Fun f ts) (Fun g ss)  = Some δ"
    and "(t,s) ∈ set (zip ts ss)"
    and "match_abss' t s = Some σ"
  shows "σ x ⊆ δ x"
proof -
  obtain θ where θ:
      "those (map2 match_abss' ts ss) = Some θ"
      "δ = fun_point_Union_list θ"
    using match_abss'_Fun_inv[OF assms(1)] by metis

  have "σ ∈ set θ" using θ(1) assms(2-) those_Some_iff[of "map2 match_abss' ts ss" θ] by force
  thus ?thesis using θ(2) unfolding fun_point_Union_list_def by auto
qed

lemma match_abss'_fv_is_nonempty:
  assumes "match_abss' t s = Some δ"
    and "x ∈ fv t"
  shows "δ x ≠ {}" (is "?P δ")
using assms
proof (induction t s arbitrary: δ rule: match_abss'.induct)
  case (2 f ts g ss)
  note prems = "2.prems"
  note IH = "2.IH"

  have 0: "∀(t,s) ∈ set (zip ts ss). ∃σ. match_abss' t s = Some σ" "f = g" "length ts = length ss"
    using match_abss'_Fun_inv[OF prems(1)] by simp_all

  obtain t where t: "t ∈ set ts" "x ∈ fv t" using prems(2) by auto
  then obtain s where s: "s ∈ set ss" "(t,s) ∈ set (zip ts ss)"
    by (meson 0(3) in_set_impl_in_set_zip1 in_set_zipE)
  then obtain σ where σ: "match_abss' t s = Some σ" using 0(1) by fast

  show ?case
    using IH[OF conjI[OF 0(2,3)] s(2) _ σ] t(2) match_abss'_Fun_param_subset[OF prems(1) s(2) σ]
    by auto
qed auto

lemma match_abss'_nonempty_is_fv:
  fixes s t::"(('a,'b,'c,'d) prot_fun, 'v) term"
  assumes "match_abss' s t = Some δ"
    and "δ x ≠ {}"
  shows "x ∈ fv s"
using assms
proof (induction s t arbitrary: δ rule: match_abss'.induct)
  case (2 f ts g ss)
  note prems = "2.prems"
  note IH = "2.IH"

  obtain θ where θ: "Some θ = those (map2 match_abss' ts ss)" "δ = fun_point_Union_list θ"
      and fg: "f = g" "length ts = length ss"
    using match_abss'_Fun_inv[OF prems(1)] by fast

  have "∃σ ∈ set θ. σ x ≠ {}"
    using fg(2) prems θ unfolding fun_point_Union_list_def by auto
  then obtain t' s' σ where ts':
      "(t',s') ∈ set (zip ts ss)" "match_abss' t' s' = Some σ" "σ x ≠ {}"
    using those_map2_SomeD[OF θ(1)[symmetric]] by blast

  show ?case
    using ts'(3) IH[OF conjI[OF fg] ts'(1) _ ts'(2)] set_zip_leftD[OF ts'(1)] by force
qed auto

lemma match_abss'_Abs_in_funs_term:
  fixes s t::"(('a,'b,'c,'d) prot_fun, 'v) term"
  assumes "match_abss' s t = Some δ"
    and "a ∈ δ x"
  shows "Abs a ∈ funs_term t"
using assms
proof (induction s t arbitrary: a δ rule: match_abss'.induct)
  case (1 y b ts) show ?case
    using match_abss'_Var_inv[OF "1.prems"(1)]  "1.prems"(2)
    by (cases "x = y") simp_all
next
  case (2 f ts g ss)
  note prems = "2.prems"
  note IH = "2.IH"

  obtain θ where θ: "Some θ = those (map2 match_abss' ts ss)" "δ = fun_point_Union_list θ"
      and fg: "f = g" "length ts = length ss"
    using match_abss'_Fun_inv[OF prems(1)] by fast

  obtain t' s' σ where ts': "(t',s') ∈ set (zip ts ss)" "match_abss' t' s' = Some σ" "a ∈ σ x"
    using fg(2) prems θ those_map2_SomeD[OF θ(1)[symmetric]]
    unfolding fun_point_Union_list_def by fastforce

  show ?case
    using ts'(1) IH[OF conjI[OF fg] ts'(1) _ ts'(2,3)]
    by (meson set_zip_rightD term.set_intros(2))
qed auto

lemma match_abss'_subst_fv_ex_abs:
  assumes "match_abss' s (s ⋅ δ) = Some σ"
    and TI: "set TI = {(a,b) ∈ (set TI)+. a ≠ b}"
  shows "∀x ∈ fv s. ∃a ts. δ x = Fun (Abs a) ts ∧ σ x = {a}" (is "?P s σ")
using assms(1)
proof (induction s "s ⋅ δ" arbitrary: σ rule: match_abss'.induct)
  case (2 f ts g ss)
  note prems = "2.prems"
  note hyps = "2.hyps"

  obtain θ where θ: "Some θ = those (map2 match_abss' ts ss)" "σ = fun_point_Union_list θ"
      and fg: "f = g" "length ts = length ss" "ss = ts ⋅list δ"
      and ts: "∀(t,s) ∈ set (zip ts ss). ∃σ. match_abss' t s = Some σ"
    using match_abss'_Fun_inv[OF prems(1)[unfolded hyps(2)[symmetric]]] hyps(2) by fastforce

  have 0: "those (map (λt. match_abss' t (t ⋅ δ)) ts) = Some θ"
    using θ(1) map2_map_subst unfolding fg(3) by metis

  have 1: "∀t ∈ set ts. ∃σ. match_abss' t (t ⋅ δ) = Some σ"
    using ts zip_map_subst[of ts δ] unfolding fg(3) by simp

  have 2: "σ' ∈ set θ"
    when t: "t ∈ set ts" "match_abss' t (t ⋅ δ) = Some σ'" for t σ'
    using t 0 those_Some_iff[of "map (λt. match_abss' t (t ⋅ δ)) ts" θ] by force

  have 3: "?P t σ'" "σ' x ≠ {}"
    when t: "t ∈ set ts" "x ∈ fv t" "match_abss' t (t ⋅ δ) = Some σ'" for t σ' x
    using t hyps(1)[OF conjI[OF fg(1,2)], of "(t, t ⋅ δ)" t σ'] zip_map_subst[of ts δ]
          match_abss'_fv_is_nonempty[of t "t ⋅ δ" σ' x]
    unfolding fg(3) by auto

  have 4: "σ' x = {}"
    when t: "x ∉ fv t" "match_abss' t (t ⋅ δ) = Some σ'" for t σ' x
    by (meson t match_abss'_nonempty_is_fv)

  show ?case
  proof
    fix x assume "x ∈ fv (Fun f ts)"
    then obtain t σ' where t: "t ∈ set ts" "x ∈ fv t" and σ': "match_abss' t (t ⋅ δ) = Some σ'"
      using 1 by auto
    then obtain a tsa where a: "δ x = Fun (Abs a) tsa"
      using 3[OF t σ'] by fast

    have "σ'' x = {a} ∨ σ'' x = {}"
      when "σ'' ∈ set θ" for σ''
      using that a 0 3[of _ x] 4[of x]
      unfolding those_Some_iff by fastforce
    thus "∃a ts. δ x = Fun (Abs a) ts ∧ σ x = {a}"
      using a 2[OF t(1) σ'] 3[OF t σ'] unfolding θ(2) fun_point_Union_list_def by auto
  qed
qed auto

lemma match_abss'_subst_disj_nonempty:
  assumes TI: "set TI = {(a,b) ∈ (set TI)+. a ≠ b}"
    and "match_abss' s (s ⋅ δ) = Some σ"
    and "x ∈ fv s"
  shows "⋂(ticl_abs TI ` σ x) ≠ {} ∧ (∃a tsa. δ x = Fun (Abs a) tsa ∧ σ x = {a})" (is "?P σ")
using assms(2,3)
proof (induction s "s ⋅ δ" arbitrary: σ rule: match_abss'.induct)
  case (1 x a ts) thus ?case unfolding ticl_abs_def by force
next
  case (2 f ts g ss)
  note prems = "2.prems"
  note hyps = "2.hyps"

  obtain θ where θ: "Some θ = those (map2 match_abss' ts ss)" "σ = fun_point_Union_list θ"
      and fg: "f = g" "length ts = length ss" "ss = ts ⋅list δ"
      and ts: "∀(t,s) ∈ set (zip ts ss). ∃σ. match_abss' t s = Some σ"
    using match_abss'_Fun_inv[OF prems(1)[unfolded hyps(2)[symmetric]]] hyps(2) by fastforce

  define ts' where "ts' ≡ filter (λt. x ∈ fv t) ts"
  define θ' where "θ' ≡ map (λt. (t, the (match_abss' t (t ⋅ δ)))) ts"
  define θ'' where "θ'' ≡ map (λt. the (match_abss' t (t ⋅ δ))) ts'"

  have 0: "those (map (λt. match_abss' t (t ⋅ δ)) ts) = Some θ"
    using θ(1) map2_map_subst unfolding fg(3) by metis

  have 1: "∀t ∈ set ts. ∃σ. match_abss' t (t ⋅ δ) = Some σ"
    using ts zip_map_subst[of ts δ] unfolding fg(3) by simp

  have ts_not_nil: "ts ≠ []"
    using prems(2) by fastforce
  hence "∃t ∈ set ts. x ∈ fv t" using prems(2) by simp
  then obtain a tsa where a: "δ x = Fun (Abs a) tsa" 
    using 1 match_abss'_subst_fv_ex_abs[OF _ TI, of _ δ]
    by metis
  hence a': "σ' x = {a}"
    when "t ∈ set ts" "x ∈ fv t" "match_abss' t (t ⋅ δ) = Some σ'"
    for t σ'
    using that match_abss'_subst_fv_ex_abs[OF _ TI, of _ δ]
    by fastforce

  have "ts' ≠ []" using prems(2) unfolding ts'_def by (simp add: filter_empty_conv) 
  hence θ''_not_nil: "θ'' ≠ []" unfolding θ''_def by simp

  have 2: "σ' ∈ set θ"
    when t: "t ∈ set ts" "match_abss' t (t ⋅ δ) = Some σ'" for t σ'
    using t 0 those_Some_iff[of "map (λt. match_abss' t (t ⋅ δ)) ts" θ] by force

  have 3: "?P σ'" "σ' x ≠ {}"
    when t: "t ∈ set ts'" "match_abss' t (t ⋅ δ) = Some σ'" for t σ'
    using t hyps(1)[OF conjI[OF fg(1,2)], of "(t, t ⋅ δ)" t σ'] zip_map_subst[of ts δ]
          match_abss'_fv_is_nonempty[of t "t ⋅ δ" σ' x]
    unfolding fg(3) ts'_def by (force, force)

  have 4: "σ' x = {}"
    when t: "x ∉ fv t" "match_abss' t (t ⋅ δ) = Some σ'" for t σ'
    by (meson t match_abss'_nonempty_is_fv)

  have 5: "θ = map snd θ'"
    using 0 1 unfolding θ'_def by (induct ts arbitrary: θ) auto

  have "fun_point_Union_list (map snd θ') x =
        fun_point_Union_list (map snd (filter (λ(t,_). x ∈ fv t) θ')) x"
    using 1 4 unfolding θ'_def fun_point_Union_list_def by fastforce
  hence 6: "fun_point_Union_list θ x = fun_point_Union_list θ'' x"
    using 0 1 4 unfolding 5 θ'_def θ''_def fun_point_Union_list_def ts'_def by auto

  have 7: "?P σ'" "σ' x ≠ {}"
    when σ': "σ' ∈ set θ''" for σ'
    using that 1 3 unfolding θ''_def ts'_def by auto

  have "σ' x = {a}"
    when σ': "σ' ∈ set θ''" for σ'
    using σ' a' 1 unfolding θ''_def ts'_def by fastforce
  hence "fun_point_Union_list θ'' x = {b | b σ'. σ' ∈ set θ'' ∧ b ∈ {a}}"
    using θ''_not_nil unfolding fun_point_Union_list_def by auto
  hence 8: "fun_point_Union_list θ'' x = {a}"
    using θ''_not_nil by auto

  show ?case
    using 8 a
    unfolding θ(2) 6 ticl_abs_iff[OF TI] by auto
qed simp_all

lemma match_abssD:
  fixes OCC TI s
  defines "f ≡ (λδ x. if x ∈ fv s then δ x else set OCC)"
    and "g ≡ (λδ x. ⋂(ticl_abs TI ` δ x))"
  assumes δ': "match_abss OCC TI s t = Some δ'" 
  shows "∃δ. match_abss' s t = Some δ ∧ δ' = f (g δ) ∧ (∀x ∈ fv s. δ x ≠ {} ∧ f (g δ) x ≠ {}) ∧
             (set OCC ≠ {} ⟶ (∀x. f (g δ) x ≠ {}))"
proof -
  obtain δ where δ: "match_abss' s t = Some δ"
    using δ' unfolding match_abss_def by force
  hence "Some δ' = (if ∀x ∈ fv s. g δ x ≠ {} then Some (f (g δ)) else None)"
    using δ' unfolding match_abss_def f_def g_def Let_def by simp
  hence "δ' = f (g δ)" "∀x ∈ fv s. δ x ≠ {} ∧ f (g δ) x ≠ {}"
    by (metis (no_types, lifting) option.inject option.distinct(1),
        metis (no_types, lifting) f_def option.distinct(1) match_abss'_fv_is_nonempty[OF δ])
  thus ?thesis using δ unfolding f_def by force
qed

lemma match_abss_ticl_abs_Inter_subset:
  assumes TI: "set TI = {(a,b). (a,b) ∈ (set TI)+ ∧ a ≠ b}"
    and δ: "match_abss OCC TI s t = Some δ"
    and x: "x ∈ fv s"
  shows "⋂(ticl_abs TI ` δ x) ⊆ δ x"
proof -
  let ?h1 = "λδ x. if x ∈ fv s then δ x else set OCC"
  let ?h2 = "λδ x. ⋂(ticl_abs TI ` δ x)"

  obtain δ' where δ':
      "match_abss' s t = Some δ'" "δ = ?h1 (?h2 δ')"
      "∀x ∈ fv s. δ' x ≠ {} ∧ δ x ≠ {}"
    using match_abssD[OF δ] by blast

  have "δ x = ⋂(ticl_abs TI ` δ' x)" "δ' x ≠ {}" "δ x ≠ {}"
    using x δ'(2,3) by auto
  thus ?thesis
    using ticl_abs_Inter TI by simp
qed

lemma match_abss_fv_has_abs:
  assumes "match_abss OCC TI s t = Some δ"
    and "x ∈ fv s"
  shows "δ x ≠ {}"
using assms match_abssD by fast

lemma match_abss_OCC_if_not_fv:
  fixes s t::"(('a,'b,'c,'d) prot_fun, 'v) term"
  assumes δ': "match_abss OCC TI s t = Some δ'"
    and x: "δ' x ≠ {}" "x ∉ fv s"
  shows "δ' x = set OCC"
proof -
  define f where "f ≡ λs::(('a,'b,'c,'d) prot_fun, 'v) term. λδ x. if x ∈ fv s then δ x else set OCC"
  define g where "g ≡ λδ. λx::'v. ⋂(ticl_abs TI ` δ x)"

  obtain δ where "match_abss' s t = Some δ" "δ' = f s (g δ)"
    using match_abssD[OF δ'] unfolding f_def g_def by blast
  thus ?thesis
    using x match_abss'_nonempty_is_fv unfolding f_def by presburger
qed

inductive synth_abs_substs_constrs_rel for FP OCC TI where
  SolveNil:
    "synth_abs_substs_constrs_rel FP OCC TI [] (λ_. set OCC)"
| SolveCons:
    "ts ≠ [] ⟹ ∀t ∈ set ts. synth_abs_substs_constrs_rel FP OCC TI [t] (θ t)
      ⟹ synth_abs_substs_constrs_rel FP OCC TI ts (fun_point_Inter (θ ` set ts))"
| SolvePubConst:
    "arity c = 0 ⟹ public c
      ⟹ synth_abs_substs_constrs_rel FP OCC TI [Fun c []] (λ_. set OCC)"
| SolvePrivConstIn:
    "arity c = 0 ⟹ ¬public c ⟹ Fun c [] ∈ set FP
      ⟹ synth_abs_substs_constrs_rel FP OCC TI [Fun c []] (λ_. set OCC)"
| SolvePrivConstNotin:
    "arity c = 0 ⟹ ¬public c ⟹ Fun c [] ∉ set FP
      ⟹ synth_abs_substs_constrs_rel FP OCC TI [Fun c []] (λ_. {})"
| SolveValueVar:
    "θ = ((λ_. set OCC)(x := ticl_abss TI {a ∈ set OCC. ⟨a⟩abs ∈ set FP}))
      ⟹ synth_abs_substs_constrs_rel FP OCC TI [Var x] θ"
| SolveComposed:
    "arity f > 0 ⟹ length ts = arity f
      ⟹ ∀δ. δ ∈ Δ ⟷ (∃s ∈ set FP. match_abss OCC TI (Fun f ts) s = Some δ)
      ⟹ Θ = (λδ x. if δ x ≠ {} then δ x else set OCC)
      ⟹ θ1 = fun_point_Union (Θ ` Δ)
      ⟹ synth_abs_substs_constrs_rel FP OCC TI ts θ2
      ⟹ synth_abs_substs_constrs_rel FP OCC TI [Fun f ts] (fun_point_union θ1 θ2)"

fun synth_abs_substs_constrs_aux where
  "synth_abs_substs_constrs_aux FP OCC TI (Var x) = (
    (λ_. set OCC)(x := ticl_abss TI (set (filter (λa. ⟨a⟩abs ∈ set FP) OCC))))"
| "synth_abs_substs_constrs_aux FP OCC TI (Fun f ts) = (
    if ts = []
    then if ¬public f ∧ Fun f ts ∉ set FP then (λ_. {}) else (λ_. set OCC)
    else let Δ = map the (filter (λδ. δ ≠ None) (map (match_abss OCC TI (Fun f ts)) FP));
             Θ = λδ x. let as = δ x in if as ≠ {} then as else set OCC;
             θ1 = fun_point_Union_list (map Θ Δ);
             θ2 = fun_point_Inter_list (map (synth_abs_substs_constrs_aux FP OCC TI) ts)
         in fun_point_union θ1 θ2)"

definition synth_abs_substs_constrs where
  "synth_abs_substs_constrs FPT T ≡
    let (FP,OCC,TI) = FPT;
        ts = trms_listsst (unlabel (transaction_receive T));
        f = fun_point_Inter_list ∘ map (synth_abs_substs_constrs_aux FP OCC TI)
    in if ts = [] then (λ_. set OCC) else f ts"

(* definition synth_abs_substs_constrs where
  "synth_abs_substs_constrs FPT T ≡
    let (FP,OCC,TI) = FPT;
        negsy = Not ∘ intruder_synth_mod_timpls FP TI;
        Θ = λδ x. let as = δ x in if as ≠ {} then as else set OCC;
        C = unlabel (transaction_checks T);
        poss = transaction_poschecks_comp C;
        negs = transaction_negchecks_comp C;
        ts = trms_listsst (unlabel (transaction_receive T));
        f = λt. let Δ = map the (filter (λδ. δ ≠ None) (map (match_abss OCC TI t) FP))
                in fun_point_Union_list (map Θ Δ);
        g = λt. if is_Fun t ∧ args t ≠ []
                then let s = hd (args t)
                in case fv_list s of
                   [] ⇒ if negsy s then Some (f t) else None
                 | [x] ⇒ let bs = filter (λa. poss x ⊆ a ∧ a ∩ negs x = {}) OCC
                          in if list_all (λb. negsy (s ⋅ Var(x := ⟨b⟩abs))) bs
                             then Some (f t) else None
                 | _ ⇒ None
                else None;
        h = λt. case g t of Some d ⇒ d | None ⇒ synth_abs_substs_constrs_aux FP OCC TI t
    in if ts = [] then (λ_. set OCC) else fun_point_Inter_list (map h ts)" *)
(*
poss = transaction_poschecks_comp (C A);
      negs = transaction_negchecks_comp (C A);
      bs = filter (λa. poss PK ⊆ a ∧ a ∩ negs PK = {}) OCC
    in if list_all (Not ∘ sy ∘ s A) bs
       then Some (map the (filter (λδ. δ ≠ None) (map (match_abss OCC TI (t' A)) FP)))
       else None
*)
definition transaction_check_comp::
  "[('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set ⇒ bool,
    ('fun,'atom,'sets,'lbl) prot_term list ×
    'sets set list ×
    ('sets set × 'sets set) list,
    ('fun,'atom,'sets,'lbl) prot_transaction]
  ⇒ ((('fun,'atom,'sets,'lbl) prot_var × 'sets set) list) list"
where
  "transaction_check_comp msgcs FPT T ≡
    let (_, OCC, _) = FPT;
        S = unlabel (transaction_strand T);
        C = unlabel (transaction_checks T);
        xs = filter (λx. x ∉ set (transaction_fresh T) ∧ fst x = TAtom Value) (fv_listsst S);
        posconstrs = transaction_poschecks_comp C;
        negconstrs = transaction_negchecks_comp C;
        pre_check = transaction_check_pre FPT T;
        Δ = abs_substs_set xs OCC posconstrs negconstrs msgcs
    in filter (λδ. pre_check (abs_substs_fun δ)) Δ"

definition transaction_check'::
  "[('fun,'atom,'sets,'lbl) prot_var ⇒ 'sets set ⇒ bool,
    ('fun,'atom,'sets,'lbl) prot_term list ×
    'sets set list ×
    ('sets set × 'sets set) list,
    ('fun,'atom,'sets,'lbl) prot_transaction]
  ⇒ bool"
where
  "transaction_check' msgcs FPT T ≡
    list_all (λδ. transaction_check_post FPT T (abs_substs_fun δ))
             (transaction_check_comp msgcs FPT T)"

definition transaction_check::
  "[('fun,'atom,'sets,'lbl) prot_term list ×
    'sets set list ×
    ('sets set × 'sets set) list,
    ('fun,'atom,'sets,'lbl) prot_transaction]
  ⇒ bool"
where
  "transaction_check ≡ transaction_check' (λ_ _. True)"

definition transaction_check_alt1::
  "[('fun,'atom,'sets,'lbl) prot_term list ×
    'sets set list ×
    ('sets set × 'sets set) list,
    ('fun,'atom,'sets,'lbl) prot_transaction]
  ⇒ bool"
where
  "transaction_check_alt1 FPT T ≡
    let msgcs = synth_abs_substs_constrs FPT T
    in transaction_check' (λx a. a ∈ msgcs x) FPT T"

lemma abs_subst_fun_cons:
  "abs_substs_fun ((x,b)#δ) = (abs_substs_fun δ)(x := b)"
unfolding abs_substs_fun_def by fastforce

lemma abs_substs_cons:
  assumes "δ ∈ set (abs_substs_set xs as poss negs msgcs)"
          "b ∈ set as" "poss x ⊆ b" "b ∩ negs x = {}" "msgcs x b"
  shows "(x,b)#δ ∈ set (abs_substs_set (x#xs) as poss negs msgcs)"
using assms by auto

lemma abs_substs_cons':
  assumes δ: "δ ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)"
    and b: "b ∈ set as" "poss x ⊆ b" "b ∩ negs x = {}" "msgcs x b"
  shows "δ(x := b) ∈ abs_substs_fun ` set (abs_substs_set (x#xs) as poss negs msgcs)"
proof -
  obtain θ where θ: "δ = abs_substs_fun θ" "θ ∈ set (abs_substs_set xs as poss negs msgcs)"
    using δ by moura
  have "abs_substs_fun ((x, b)#θ) ∈ abs_substs_fun ` set (abs_substs_set (x#xs) as poss negs msgcs)"
    using abs_substs_cons[OF θ(2) b] by blast
  thus ?thesis
    using θ(1) abs_subst_fun_cons[of x b θ] by argo
qed

lemma abs_substs_has_abs:
  assumes "∀x. x ∈ set xs ⟶ δ x ∈ set as"
    and "∀x. x ∈ set xs ⟶ poss x ⊆ δ x"
    and "∀x. x ∈ set xs ⟶ δ x ∩ negs x = {}"
    and "∀x. x ∈ set xs ⟶ msgcs x (δ x)"
    and "∀x. x ∉ set xs ⟶ δ x = {}"
  shows "δ ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)"
using assms
proof (induction xs arbitrary: δ)
  case (Cons x xs)
  define θ where "θ ≡ λy. if y ∈ set xs then δ y else {}"

  have "θ ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)"
    using Cons.prems Cons.IH by (simp add: θ_def)
  moreover have "δ x ∈ set as" "poss x ⊆ δ x" "δ x ∩ negs x = {}" "msgcs x (δ x)"
    by (simp_all add: Cons.prems(1,2,3,4))
  ultimately have 0: "θ(x := δ x) ∈ abs_substs_fun ` set (abs_substs_set (x#xs) as poss negs msgcs)"
    by (metis abs_substs_cons')

  have "δ = θ(x := δ x)"
  proof
    fix y show "δ y = (θ(x := δ x)) y"
    proof (cases "y ∈ set (x#xs)")
      case False thus ?thesis using Cons.prems(5) by (fastforce simp add: θ_def)
    qed (auto simp add: θ_def)
  qed
  thus ?case by (metis 0)
qed (auto simp add: abs_substs_fun_def)

lemma abs_substs_abss_bounded:
  assumes "δ ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)"
    and "x ∈ set xs"
  shows "δ x ∈ set as"
    and "poss x ⊆ δ x"
    and "δ x ∩ negs x = {}"
    and "msgcs x (δ x)"
using assms
proof (induct xs as poss negs msgcs arbitrary: δ rule: abs_substs_set_induct)
  case (Cons y xs as poss negs msgcs)
  { case 1 thus ?case using Cons.hyps(1) unfolding abs_substs_fun_def by fastforce }

  { case 2 thus ?case
    proof (cases "x = y")
      case False
      then obtain δ' where δ':
          "δ' ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)" "δ' x = δ x"
        using 2 unfolding abs_substs_fun_def by force
      moreover have "x ∈ set xs" using 2(2) False by simp
      moreover have "∃b. b ∈ set as ∧ poss y ⊆ b ∧ b ∩ negs y = {}"
        using 2 False by auto
      ultimately show ?thesis using Cons.hyps(2) by fastforce
    qed (auto simp add: abs_substs_fun_def)
  }

  { case 3 thus ?case
    proof (cases "x = y")
      case False
      then obtain δ' where δ':
          "δ' ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)" "δ' x = δ x"
        using 3 unfolding abs_substs_fun_def by force
      moreover have "x ∈ set xs" using 3(2) False by simp
      moreover have "∃b. b ∈ set as ∧ poss y ⊆ b ∧ b ∩ negs y = {}"
        using 3 False by auto
      ultimately show ?thesis using Cons.hyps(3) by fastforce
    qed (auto simp add: abs_substs_fun_def)
  }

  { case 4 thus ?case
    proof (cases "x = y")
      case False
      then obtain δ' where δ':
          "δ' ∈ abs_substs_fun ` set (abs_substs_set xs as poss negs msgcs)" "δ' x = δ x"
        using 4 unfolding abs_substs_fun_def by force
      moreover have "x ∈ set xs" using 4(2) False by simp
      moreover have "∃b. b ∈ set as ∧ poss y ⊆ b ∧ b ∩ negs y =