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 force
    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 force  
    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 force
  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 force
      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 force
      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  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

  show ?thesis
    using x δ(2) 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. aabs  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 δ)
       θ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. aabs  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));
             θ1 = fun_point_Union_list Δ;
             θ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_coverage_rcv::
  "[('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_coverage_rcv 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 force
  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 = {}"
        using 4 False by auto
      ultimately show ?thesis using Cons.hyps(4) by fastforce
    qed (auto simp add: abs_substs_fun_def)
  }
qed (simp_all add: abs_substs_fun_def)

lemma abs_substs_abss_bounded':
  assumes "δ  abs_substs_fun