Theory Stateful_Compositionality

(*  Title:      Stateful_Compositionality.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)


section ‹Stateful Protocol Compositionality›

theory Stateful_Compositionality
imports Stateful_Typing Parallel_Compositionality Labeled_Stateful_Strands
begin

subsection ‹Small Lemmata›
lemma (in typed_model) wt_subst_sstp_vars_type_subset:
  fixes a::"('fun,'var) stateful_strand_step"
  assumes "wtsubst δ"
    and "∀t ∈ subst_range δ. fv t = {} ∨ (∃x. t = Var x)"
  shows "Γ ` Var ` fvsstp (a ⋅sstp δ) ⊆ Γ ` Var ` fvsstp a" (is ?A)
    and "Γ ` Var ` set (bvarssstp (a ⋅sstp δ)) = Γ ` Var ` set (bvarssstp a)" (is ?B)
    and "Γ ` Var ` varssstp (a ⋅sstp δ) ⊆ Γ ` Var ` varssstp a" (is ?C)
proof -
  show ?A
  proof
    fix τ assume τ: "τ ∈ Γ ` Var ` fvsstp (a ⋅sstp δ)"
    then obtain x where x: "x ∈ fvsstp (a ⋅sstp δ)" "Γ (Var x) = τ" by moura
  
    show "τ ∈ Γ ` Var ` fvsstp a"
    proof (cases "x ∈ fvsstp a")
      case False
      hence "∃y ∈ fvsstp a. δ y = Var x"
      proof (cases a)
        case (NegChecks X F G)
        hence *: "x ∈ fvpairs (F ⋅pairs rm_vars (set X) δ) ∪ fvpairs (G ⋅pairs rm_vars (set X) δ)"
                 "x ∉ set X"
          using fvsstp_NegCheck(1)[of X "F ⋅pairs rm_vars (set X) δ" "G ⋅pairs rm_vars (set X) δ"]
                fvsstp_NegCheck(1)[of X F G] False x(1)
          by fastforce+
  
        obtain y where y: "y ∈ fvpairs F ∪ fvpairs G" "x ∈ fv (rm_vars (set X) δ y)"
          using fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                *(1)
          by blast
  
        have "fv (rm_vars (set X) δ z) = {} ∨ (∃u. rm_vars (set X) δ z = Var u)" for z
          using assms(2) rm_vars_img_subset[of "set X" δ] by blast
        hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
        hence "∃y ∈ fvsstp a. rm_vars (set X) δ y = Var x"
          using y fvsstp_NegCheck(1)[of X F G] NegChecks *(2) by fastforce
        thus ?thesis by (metis (full_types) *(2) term.inject(1))
      qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
      then obtain y where y: "y ∈ fvsstp a" "δ y = Var x" by moura
      hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wtsubst_def)
      thus ?thesis using y(1) by auto
    qed (use x in auto)
  qed

  show ?B by (metis bvarssstp_subst)

  show ?C
  proof
    fix τ assume τ: "τ ∈ Γ ` Var ` varssstp (a ⋅sstp δ)"
    then obtain x where x: "x ∈ varssstp (a ⋅sstp δ)" "Γ (Var x) = τ" by moura
  
    show "τ ∈ Γ ` Var ` varssstp a"
    proof (cases "x ∈ varssstp a")
      case False
      hence "∃y ∈ varssstp a. δ y = Var x"
      proof (cases a)
        case (NegChecks X F G)
        hence *: "x ∈ fvpairs (F ⋅pairs rm_vars (set X) δ) ∪ fvpairs (G ⋅pairs rm_vars (set X) δ)"
                 "x ∉ set X"
          using varssstp_NegCheck[of X "F ⋅pairs rm_vars (set X) δ" "G ⋅pairs rm_vars (set X) δ"]
                varssstp_NegCheck[of X F G] False x(1)
          by (fastforce, blast)
  
        obtain y where y: "y ∈ fvpairs F ∪ fvpairs G" "x ∈ fv (rm_vars (set X) δ y)"
          using fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                *(1)
          by blast
  
        have "fv (rm_vars (set X) δ z) = {} ∨ (∃u. rm_vars (set X) δ z = Var u)" for z
          using assms(2) rm_vars_img_subset[of "set X" δ] by blast
        hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
        hence "∃y ∈ varssstp a. rm_vars (set X) δ y = Var x"
          using y varssstp_NegCheck[of X F G] NegChecks by blast
        thus ?thesis by (metis (full_types) *(2) term.inject(1))
      qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
      then obtain y where y: "y ∈ varssstp a" "δ y = Var x" by moura
      hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wtsubst_def)
      thus ?thesis using y(1) by auto
    qed (use x in auto)
  qed
qed

lemma (in typed_model) wt_subst_lsst_vars_type_subset:
  fixes A::"('fun,'var,'a) labeled_stateful_strand"
  assumes "wtsubst δ"
    and "∀t ∈ subst_range δ. fv t = {} ∨ (∃x. t = Var x)"
  shows "Γ ` Var ` fvlsst (A ⋅lsst δ) ⊆ Γ ` Var ` fvlsst A" (is ?A)
    and "Γ ` Var ` bvarslsst (A ⋅lsst δ) = Γ ` Var ` bvarslsst A" (is ?B)
    and "Γ ` Var ` varslsst (A ⋅lsst δ) ⊆ Γ ` Var ` varslsst A" (is ?C)
proof -
  have "varslsst (a#A ⋅lsst δ) = varssstp (b ⋅sstp δ) ∪ varslsst (A ⋅lsst δ)"
       "varslsst (a#A) = varssstp b ∪ varslsst A"
       "fvlsst (a#A ⋅lsst δ) = fvsstp (b ⋅sstp δ) ∪ fvlsst (A ⋅lsst δ)"
       "fvlsst (a#A) = fvsstp b ∪ fvlsst A"
       "bvarslsst (a#A ⋅lsst δ) = set (bvarssstp (b ⋅sstp δ)) ∪ bvarslsst (A ⋅lsst δ)"
       "bvarslsst (a#A) = set (bvarssstp b) ∪ bvarslsst A"
    when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
    using that unlabel_Cons(1)[of l b A] unlabel_subst[of "a#A" δ]
          subst_lsst_cons[of a A δ] subst_sst_cons[of b "unlabel A" δ]
          subst_apply_labeled_stateful_strand_step.simps(1)[of l b δ]
          varssst_unlabel_Cons[of l b A] varssst_unlabel_Cons[of l "b ⋅sstp δ" "A ⋅lsst δ"]
          fvsst_unlabel_Cons[of l b A] fvsst_unlabel_Cons[of l "b ⋅sstp δ" "A ⋅lsst δ"]
          bvarssst_unlabel_Cons[of l b A] bvarssst_unlabel_Cons[of l "b ⋅sstp δ" "A ⋅lsst δ"]
    by simp_all
  hence *: "Γ ` Var ` varslsst (a#A ⋅lsst δ) =
            Γ ` Var ` varssstp (b ⋅sstp δ) ∪ Γ ` Var ` varslsst (A ⋅lsst δ)"
           "Γ ` Var ` varslsst (a#A) = Γ ` Var ` varssstp b ∪ Γ ` Var ` varslsst A"
           "Γ ` Var ` fvlsst (a#A ⋅lsst δ) =
            Γ ` Var ` fvsstp (b ⋅sstp δ) ∪ Γ ` Var ` fvlsst (A ⋅lsst δ)"
           "Γ ` Var ` fvlsst (a#A) = Γ ` Var ` fvsstp b ∪ Γ ` Var ` fvlsst A"
           "Γ ` Var ` bvarslsst (a#A ⋅lsst δ) =
            Γ ` Var ` set (bvarssstp (b ⋅sstp δ)) ∪ Γ ` Var ` bvarslsst (A ⋅lsst δ)"
           "Γ ` Var ` bvarslsst (a#A) = Γ ` Var ` set (bvarssstp b) ∪ Γ ` Var ` bvarslsst A"
    when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
    using that by fast+

  have "?A ∧ ?B ∧ ?C"
  proof (induction A)
    case (Cons a A)
    obtain l b where a: "a = (l,b)" by (metis surj_pair)
  
    show ?case
      using Cons.IH wt_subst_sstp_vars_type_subset[OF assms, of b] *[OF a, of A]
      by (metis Un_mono)
  qed simp
  thus ?A ?B ?C by metis+
qed

lemma (in stateful_typed_model) fv_pair_fvpairs_subset:
  assumes "d ∈ set D"
  shows "fv (pair (snd d)) ⊆ fvpairs (unlabel D)"
using assms unfolding pair_def by (induct D) (auto simp add: unlabel_def)

lemma (in stateful_typed_model) labeled_sat_ineq_lift:
  assumes "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←dbproj i D. d ∉ set Di]⟧d ℐ"
    (is "?R1 D")
  and "∀(j,p) ∈ {(i,t,s)} ∪ set D ∪ set Di. ∀(k,q) ∈ {(i,t,s)} ∪ set D ∪ set Di.
          (∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?R2 D")
  shows "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←D. d ∉ set Di]⟧d ℐ"
using assms
proof (induction D)
  case (Cons dl D)
  obtain d l where dl: "dl = (l,d)" by (metis surj_pair)

  have 1: "?R1 D"
  proof (cases "i = l")
    case True thus ?thesis
      using Cons.prems(1) dl by (cases "dl ∈ set Di") (auto simp add: dbproj_def)
  next
    case False thus ?thesis using Cons.prems(1) dl by (auto simp add: dbproj_def)
  qed

  have "set D ⊆ set (dl#D)" by auto
  hence 2: "?R2 D" using Cons.prems(2) by blast

  have "i ≠ l ∨ dl ∈ set Di ∨ ⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd dl))]⟩st]⟧d ℐ"
    using Cons.prems(1) dl by (auto simp add: ineq_model_def dbproj_def)
  moreover have "∃δ. Unifier δ (pair (t,s)) (pair d) ⟹ i = l"
    using Cons.prems(2) dl by force
  ultimately have 3: "dl ∈ set Di ∨ ⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd dl))]⟩st]⟧d ℐ"
    using strand_sem_not_unif_is_sat_ineq[of "pair (t,s)" "pair d"] dl by fastforce

  show ?case using Cons.IH[OF 1 2] 3 dl by auto
qed simp

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj:
  assumes "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←D. d ∉ set Di]⟧d ℐ"
    (is "?P D")
  shows "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←dbproj i D. d ∉ set Di]⟧d ℐ"
    (is "?Q D")
using assms
proof (induction D)
  case (Cons di D)
  obtain d j where di: "di = (j,d)" by (metis surj_pair)

  have "?P D" using Cons.prems by (cases "di ∈ set Di") auto
  hence IH: "?Q D" by (metis Cons.IH)

  show ?case using di IH
  proof (cases "i = j ∧ di ∉ set Di")
    case True
    have 1: "⟦M; [∀X⟨∨≠: [(pair (t,s), pair (snd di))]⟩st]⟧d ℐ"
      using Cons.prems True by auto
    have 2: "dbproj i (di#D) = di#dbproj i D" using True dbproj_Cons(1) di by auto
    show ?thesis using 1 2 IH by auto
  qed (auto simp add: dbproj_def)
qed (simp add: dbproj_def)

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj_sem_equiv:
  assumes "∀(j,p) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D.
           ∀(k,q) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D.
            (∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k"
  and "fvpairs (map snd D) ∩ set X = {}"
  shows "⟦M; map (λG. ∀X⟨∨≠: (F@G)⟩st) (trpairs F' (map snd D))⟧d ℐ ⟷
         ⟦M; map (λG. ∀X⟨∨≠: (F@G)⟩st) (trpairs F' (map snd (dbproj i D)))⟧d ℐ"
proof -
  let ?A = "set (map snd D) ⋅pset ℐ"
  let ?B = "set (map snd (dbproj i D)) ⋅pset ℐ"
  let ?C = "set (map snd D) - set (map snd (dbproj i D))"
  let ?F = "(λ(t, s). (i, t, s)) ` set F'"
  let ?P = "λδ. subst_domain δ = set X ∧ ground (subst_range δ)"

  have 1: "∀(t, t') ∈ set (map snd D). (fv t ∪ fv t') ∩ set X = {}"
          "∀(t, t') ∈ set (map snd (dbproj i D)). (fv t ∪ fv t') ∩ set X = {}"
    using assms(2) dbproj_subset[of i D] unfolding unlabel_def by force+

  have 2: "?B ⊆ ?A" unfolding dbproj_def by auto

  have 3: "¬Unifier δ (pair f) (pair d)"
    when f: "f ∈ set F'" and d: "d ∈ set (map snd D) - set (map snd (dbproj i D))"
    for f d and δ::"('fun,'var) subst"
  proof -
    obtain k where k: "(k,d) ∈ set D - set (dbproj i D)"
      using d by force
    
    have "(i,f) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D"
         "(k,d) ∈ ((λ(t, s). (i, t, s)) ` set F') ∪ set D"
      using f k by auto
    hence "i = k" when "Unifier δ (pair f) (pair d)" for δ
      using assms(1) that by blast
    moreover have "k ≠ i" using k d unfolding dbproj_def by simp
    ultimately show ?thesis by metis
  qed

  have "f ⋅p δ ≠ d ⋅p δ"
    when "f ∈ set F'" "d ∈ ?C" for f d and δ::"('fun,'var) subst"
    by (metis fun_pair_eq_subst 3[OF that])
  hence "f ⋅p (δ ∘s ℐ) ∉ ?C ⋅pset (δ ∘s ℐ)"
    when "f ∈ set F'" for f and δ::"('fun,'var) subst"
    using that by blast
  moreover have "?C ⋅pset δ ⋅pset ℐ = ?C ⋅pset ℐ"
    when "?P δ" for δ
    using assms(2) that pairs_substI[of δ "(set (map snd D) - set (map snd (dbproj i D)))"]
    by blast
  ultimately have 4: "f ⋅p (δ ∘s ℐ) ∉ ?C ⋅pset ℐ"
    when "f ∈ set F'" "?P δ" for f and δ::"('fun,'var) subst"
    by (metis that subst_pairs_compose)

  { fix f and δ::"('fun,'var) subst"
    assume "f ∈ set F'" "?P δ"
    hence "f ⋅p (δ ∘s ℐ) ∉ ?C ⋅pset ℐ" by (metis 4)
    hence "f ⋅p (δ ∘s ℐ) ∉ ?A - ?B" by force
  } hence 5: "∀f∈set F'. ∀δ. ?P δ ⟶ f ⋅p (δ ∘s ℐ) ∉ ?A - ?B" by metis

  show ?thesis
    using negchecks_model_db_subset[OF 2]
          negchecks_model_db_supset[OF 2 5]
          trpairs_sem_equiv[OF 1(1)]
          trpairs_sem_equiv[OF 1(2)]
          tr_NegChecks_constr_iff(1)
          strand_sem_eq_defs(2)
    by (metis (no_types, lifting))
qed

lemma (in stateful_typed_model) labeled_sat_eqs_list_all:
  assumes "∀(j, p) ∈ {(i,t,s)} ∪ set D. ∀(k,q) ∈ {(i,t,s)} ∪ set D.
              (∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?P D")
  and "⟦M; map (λd. ⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩st) D⟧d ℐ" (is "?Q D")
  shows "list_all (λd. fst d = i) D"
using assms
proof (induction D rule: List.rev_induct)
  case (snoc di D)
  obtain d j where di: "di = (j,d)" by (metis surj_pair)
  have "pair (t,s) ⋅ ℐ = pair d ⋅ ℐ" using di snoc.prems(2) by auto
  hence "∃δ. Unifier δ (pair (t,s)) (pair d)" by auto
  hence 1: "i = j" using snoc.prems(1) di by fastforce
  
  have "set D ⊆ set (D@[di])" by auto
  hence 2: "?P D" using snoc.prems(1) by blast

  have 3: "?Q D" using snoc.prems(2) by auto
  
  show ?case using di 1 snoc.IH[OF 2 3] by simp
qed simp

lemma (in stateful_typed_model) labeled_sat_eqs_subseqs:
  assumes "Di ∈ set (subseqs D)"
  and "∀(j, p) ∈ {(i,t,s)} ∪ set D. ∀(k, q) ∈ {(i,t,s)} ∪ set D.
          (∃δ. Unifier δ (pair p) (pair q)) ⟶ j = k" (is "?P D")
  and "⟦M; map (λd. ⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩st) Di⟧d ℐ"
  shows "Di ∈ set (subseqs (dbproj i D))"
proof -
  have "set Di ⊆ set D" by (rule subseqs_subset[OF assms(1)])
  hence "?P Di" using assms(2) by blast
  thus ?thesis using labeled_sat_eqs_list_all[OF _ assms(3)] subseqs_mem_dbproj[OF assms(1)] by simp
qed

lemma (in stateful_typing_result) duallsst_tfrsstp:
  assumes "list_all tfrsstp (unlabel S)"
  shows "list_all tfrsstp (unlabel (duallsst S))"
using assms
proof (induction S)
  case (Cons a S)
  have prems: "tfrsstp (snd a)" "list_all tfrsstp (unlabel S)"
    using Cons.prems unlabel_Cons(2)[of a S] by simp_all
  hence IH: "list_all tfrsstp (unlabel (duallsst S))" by (metis Cons.IH)

  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  with Cons show ?case
  proof (cases b)
    case (Equality c t t')
    hence "duallsst (a#S) = a#duallsst S" by (metis duallsst_Cons(3) a)
    thus ?thesis using a IH prems by fastforce
  next
    case (NegChecks X F G)
    hence "duallsst (a#S) = a#duallsst S" by (metis duallsst_Cons(7) a)
    thus ?thesis using a IH prems by fastforce
  qed auto
qed simp

lemma (in stateful_typed_model) setopssst_unlabel_duallsst_eq:
  "setopssst (unlabel (duallsst A)) = setopssst (unlabel A)"
proof (induction A)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons.IH by (cases b) (simp_all add: setopssst_def)
qed simp


subsection ‹Locale Setup and Definitions›
locale labeled_stateful_typed_model =
  stateful_typed_model arity public Ana Γ Pair
+ labeled_typed_model arity public Ana Γ label_witness1 label_witness2
  for arity::"'fun ⇒ nat"
  and public::"'fun ⇒ bool"
  and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
  and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
  and Pair::"'fun"
  and label_witness1::"'lbl"
  and label_witness2::"'lbl"
begin

definition lpair where
  "lpair lp ≡ case lp of (i,p) ⇒ (i,pair p)"

lemma setopslsstp_pair_image[simp]:
  "lpair ` (setopslsstp (i,send⟨ts⟩)) = {}"
  "lpair ` (setopslsstp (i,receive⟨ts⟩)) = {}"
  "lpair ` (setopslsstp (i,⟨ac: t ≐ t'⟩)) = {}"
  "lpair ` (setopslsstp (i,insert⟨t,s⟩)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,delete⟨t,s⟩)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,⟨ac: t ∈ s⟩)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,∀X⟨∨≠: F ∨∉: F'⟩)) = ((λ(t,s). (i, pair (t,s))) ` set F')"
unfolding lpair_def by force+

definition par_complsst where
  "par_complsst (𝒜::('fun,'var,'lbl) labeled_stateful_strand) (Secrets::('fun,'var) terms) ≡ 
    (∀l1 l2. l1 ≠ l2 ⟶
              GSMP_disjoint (trmssst (proj_unl l1 𝒜) ∪ pair ` setopssst (proj_unl l1 𝒜))
                            (trmssst (proj_unl l2 𝒜) ∪ pair ` setopssst (proj_unl l2 𝒜)) Secrets) ∧
    (∀s ∈ Secrets. ¬{} ⊢c s) ∧ ground Secrets ∧
    (∀(i,p) ∈ setopslsst 𝒜. ∀(j,q) ∈ setopslsst 𝒜.
      (∃δ. Unifier δ (pair p) (pair q)) ⟶ i = j)"

definition declassifiedlsst where
  "declassifiedlsst 𝒜 ℐ ≡ {s. ⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (𝒜 ⋅lsst ℐ)} ⊢ s}"

definition strand_leakslsst ("_ leaks _ under _") where
  "(𝒜::('fun,'var,'lbl) labeled_stateful_strand) leaks Secrets under ℐ ≡
    (∃t ∈ Secrets - declassifiedlsst 𝒜 ℐ. ∃n. ℐ ⊨s (proj_unl n 𝒜@[send⟨[t]⟩]))"

type_synonym ('a,'b,'c) labeleddbstate = "('c strand_label × (('a,'b) term × ('a,'b) term)) set"
type_synonym ('a,'b,'c) labeleddbstatelist = "('c strand_label × (('a,'b) term × ('a,'b) term)) list"

definition typing_condsst where
  "typing_condsst 𝒜 ≡ wfsst 𝒜 ∧ wftrms (trmssst 𝒜) ∧ tfrsst 𝒜"

text ‹
  For proving the compositionality theorem for stateful constraints the idea is to first define a
  variant of the reduction technique that was used to establish the stateful typing result. This
  variant performs database-state projections, and it allows us to reduce the compositionality
  problem for stateful constraints to ordinary constraints.
›
fun trpc::
  "('fun,'var,'lbl) labeled_stateful_strand ⇒ ('fun,'var,'lbl) labeleddbstatelist
   ⇒ ('fun,'var,'lbl) labeled_strand list"
where
  "trpc [] D = [[]]"
| "trpc ((i,send⟨ts⟩)#A) D = map ((#) (i,send⟨ts⟩st)) (trpc A D)"
| "trpc ((i,receive⟨ts⟩)#A) D = map ((#) (i,receive⟨ts⟩st)) (trpc A D)"
| "trpc ((i,⟨ac: t ≐ t'⟩)#A) D = map ((#) (i,⟨ac: t ≐ t'⟩st)) (trpc A D)"
| "trpc ((i,insert⟨t,s⟩)#A) D = trpc A (List.insert (i,(t,s)) D)"
| "trpc ((i,delete⟨t,s⟩)#A) D = (
    concat (map (λDi. map (λB. (map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩st)) Di)@
                               (map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st))
                                    [d←dbproj i D. d ∉ set Di])@B)
                          (trpc A [d←D. d ∉ set Di]))
                (subseqs (dbproj i D))))"
| "trpc ((i,⟨ac: t ∈ s⟩)#A) D =
    concat (map (λB. map (λd. (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩st)#B) (dbproj i D)) (trpc A D))"
| "trpc ((i,∀X⟨∨≠: F ∨∉: F' ⟩)#A) D =
    map ((@) (map (λG. (i,∀X⟨∨≠: (F@G)⟩st)) (trpairs F' (map snd (dbproj i D))))) (trpc A D)"

end

locale labeled_stateful_typing =
  labeled_stateful_typed_model arity public Ana Γ Pair label_witness1 label_witness2
+ stateful_typing_result arity public Ana Γ Pair
  for arity::"'fun ⇒ nat"
  and public::"'fun ⇒ bool"
  and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
  and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
  and Pair::"'fun"
  and label_witness1::"'lbl"
  and label_witness2::"'lbl"
begin

sublocale labeled_typing
by unfold_locales

end


subsection ‹Small Lemmata›
context labeled_stateful_typed_model
begin

lemma declassifiedlsst_alt_def:
  "declassifiedlsst 𝒜 ℐ = {s. ⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set 𝒜} ⋅set ℐ ⊢ s}"
proof -
  have "(l, receive⟨ts⟩) ∈ set (𝒜 ⋅lsst ℐ) = (∃ts'. (l, receive⟨ts'⟩) ∈ set 𝒜 ∧ ts = ts' ⋅list ℐ)"
    (is "?A 𝒜 = ?B 𝒜")
    for ts l
  proof
    show "?A 𝒜 ⟹ ?B 𝒜"
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?A 𝒜")
        case False
        hence "(l,receive⟨ts⟩) = a ⋅lsstp ℐ" using Cons.prems subst_lsst_cons[of a 𝒜 ℐ] by auto
        thus ?thesis unfolding a by (cases b) auto
      qed (use Cons.IH in auto)
    qed simp

    show "?B 𝒜 ⟹ ?A 𝒜"
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?B 𝒜")
        case False
        hence "∃ts'. a = (l, receive⟨ts'⟩) ∧ ts = ts' ⋅list ℐ" using Cons.prems by auto
        thus ?thesis using subst_lsst_cons[of a 𝒜 ℐ] unfolding a by (cases b) auto
      qed (use Cons.IH subst_lsst_cons[of a 𝒜 ℐ] in auto)
    qed simp
  qed
  thus ?thesis
    unfolding declassifiedlsst_def
    by (smt Collect_cong image_Union list.set_map setcompr_eq_image)
qed

lemma declassifiedlsst_prefix_subset:
  assumes AB: "prefix A B"
  shows "declassifiedlsst A I ⊆ declassifiedlsst B I"
proof
  fix t assume t: "t ∈ declassifiedlsst A I"
  obtain C where C: "B = A@C" using prefixE[OF AB] by metis
  show "t ∈ declassifiedlsst B I"
    using t ideduct_mono[of
              "⋃{set ts |ts. (⋆, receive⟨ts⟩) ∈ set A} ⋅set I" t 
              "⋃{set ts |ts. (⋆, receive⟨ts⟩) ∈ set B} ⋅set I"]
    unfolding C declassifiedlsst_alt_def by auto
qed

lemma declassifiedlsst_star_receive_supset:
  "{t | t ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set 𝒜 ∧ t ∈ set ts} ⋅set ℐ ⊆ declassifiedlsst 𝒜 ℐ"
unfolding declassifiedlsst_alt_def by (fastforce intro: intruder_deduct.Axiom)

lemma declassifiedlsst_proj_eq:
  "declassifiedlsst A I = declassifiedlsst (proj n A) I"
using proj_mem_iff(2)[of _ A] unfolding declassifiedlsst_alt_def by simp

lemma par_complsst_nil:
  assumes "ground Sec" "∀s ∈ Sec. ∀s'∈subterms s. {} ⊢c s' ∨ s' ∈ Sec" "∀s ∈ Sec. ¬{} ⊢c s"
  shows "par_complsst [] Sec"
using assms unfolding par_complsst_def by simp

lemma par_complsst_subset:
  assumes A: "par_complsst A Sec"
    and BA: "set B ⊆ set A"
  shows "par_complsst B Sec"
proof -
  let ?L = "λn A. trmssst (proj_unl n A) ∪ pair ` setopssst (proj_unl n A)"

  have "?L n B ⊆ ?L n A" for n
    using trmssst_mono[OF proj_set_mono(2)[OF BA]] setopssst_mono[OF proj_set_mono(2)[OF BA]]
    by blast
  hence "GSMP_disjoint (?L m B) (?L n B) Sec" when nm: "m ≠ n" for n m::'lbl
    using GSMP_disjoint_subset[of "?L m A" "?L n A" Sec "?L m B" "?L n B"] A nm
    unfolding par_complsst_def by simp
  thus "par_complsst B Sec"
    using A setopslsst_mono[OF BA]
    unfolding par_complsst_def by blast
qed

lemma par_complsst_split:
  assumes "par_complsst (A@B) Sec"
  shows "par_complsst A Sec" "par_complsst B Sec"
using par_complsst_subset[OF assms] by simp_all

lemma par_complsst_proj:
  assumes "par_complsst A Sec"
  shows "par_complsst (proj n A) Sec"
using par_complsst_subset[OF assms] by simp

lemma par_complsst_duallsst:
  assumes A: "par_complsst A S"
  shows "par_complsst (duallsst A) S"
proof (unfold par_complsst_def case_prod_unfold; intro conjI)
  show "ground S" "∀s ∈ S. ¬{} ⊢c s"
    using A unfolding par_complsst_def by fast+

  let ?M = "λl B. (trmslsst (proj l B) ∪ pair ` setopssst (proj_unl l B))"
  let ?P = "λB. ∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (?M l1 B) (?M l2 B) S"
  let ?Q = "λB. ∀p ∈ setopslsst B. ∀q ∈ setopslsst B.
    (∃δ. Unifier δ (pair (snd p)) (pair (snd q))) ⟶ fst p = fst q"

  have "?P A" "?Q A" using A unfolding par_complsst_def case_prod_unfold by blast+
  thus "?P (duallsst A)" "?Q (duallsst A)"
    by (metis setopssst_unlabel_duallsst_eq trmssst_unlabel_duallsst_eq proj_duallsst,
        metis setopslsst_duallsst_eq)
qed

lemma par_complsst_subst:
  assumes A: "par_complsst A S"
    and δ: "wtsubst δ" "wftrms (subst_range δ)" "subst_domain δ ∩ bvarslsst A = {}"
  shows "par_complsst (A ⋅lsst δ) S"
proof (unfold par_complsst_def case_prod_unfold; intro conjI)
  show "ground S" "∀s ∈ S. ¬{} ⊢c s"
    using A unfolding par_complsst_def by fast+

  let ?N = "λl B. trmslsst (proj l B) ∪ pair ` setopssst (proj_unl l B)"
  define M where "M ≡ λl (B::('fun,'var,'lbl) labeled_stateful_strand). ?N l B"
  let ?P = "λp q. ∃δ. Unifier δ (pair (snd p)) (pair (snd q))"
  let ?Q = "λB. ∀p ∈ setopslsst B. ∀q ∈ setopslsst B. ?P p q ⟶ fst p = fst q"
  let ?R = "λB. ∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (?N l1 B) (?N l2 B) S"

  have d: "bvarslsst (proj l A) ∩ subst_domain δ = {}" for l
    using δ(3) unfolding proj_def bvarssst_def unlabel_def by auto

  have "GSMP_disjoint (M l1 A) (M l2 A) S" when l: "l1 ≠ l2" for l1 l2
    using l A unfolding par_complsst_def M_def by presburger
  moreover have "M l (A ⋅lsst δ) = (M l A) ⋅set δ" for l
    using fun_pair_subst_set[of δ "setopssst (proj_unl l A)", symmetric]
          trmssst_subst[OF d[of l]] setopssst_subst[OF d[of l]] proj_subst[of l A δ]
    unfolding M_def unlabel_subst by auto
  ultimately have "GSMP_disjoint (M l1 (A ⋅lsst δ)) (M l2 (A ⋅lsst δ)) S" when l: "l1 ≠ l2" for l1 l2
    using l GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l1 A"]
          GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l2 A"]
    unfolding GSMP_disjoint_def by fastforce
  thus "?R (A ⋅lsst δ)" unfolding M_def by blast

  have "?Q A" using A unfolding par_complsst_def by force 
  thus "?Q (A ⋅lsst δ)" using δ(3)
  proof (induction A)
    case (Cons a A)
    obtain l b where a: "a = (l,b)" by (metis surj_pair)

    have 0: "bvarslsst (a#A) = set (bvarssstp (snd a)) ∪ bvarslsst A"
      unfolding bvarssst_def unlabel_def by simp

    have "?Q A" "subst_domain δ ∩ bvarslsst A = {}"
      using Cons.prems 0 unfolding setopslsst_def by auto
    hence IH: "?Q (A ⋅lsst δ)" using Cons.IH unfolding setopslsst_def by blast
    
    have 1: "fst p = fst q"
      when p: "p ∈ setopslsstp (a ⋅lsstp δ)"
        and q: "q ∈ setopslsstp (a ⋅lsstp δ)"
        and pq: "?P p q"
      for p q
      using a p q pq by (cases b) auto

    have 2: "fst p = fst q"
      when p: "p ∈ setopslsst (A ⋅lsst δ)"
        and q: "q ∈ setopslsstp (a ⋅lsstp δ)"
        and pq: "?P p q"
      for p q
    proof -
      obtain p' X where p':
          "p' ∈ setopslsst A" "fst p = fst p'" 
          "X ⊆ bvarslsst (a#A)" "snd p = snd p' ⋅p rm_vars X δ"
        using setopslsst_in_subst[OF p] 0 by blast

      obtain q' Y where q':
          "q' ∈ setopslsstp a" "fst q = fst q'" 
          "Y ⊆ bvarslsst (a#A)" "snd q = snd q' ⋅p rm_vars Y δ"
        using setopslsstp_in_subst[OF q] 0 by blast

      have "pair (snd p) = pair (snd p') ⋅ δ"
           "pair (snd q) = pair (snd q') ⋅ δ"
        using fun_pair_subst[of "snd p'" "rm_vars X δ"] fun_pair_subst[of "snd q'" "rm_vars Y δ"]
              p'(3,4) q'(3,4) Cons.prems(2) rm_vars_apply'[of δ X] rm_vars_apply'[of δ Y]
        by fastforce+
      hence "∃δ. Unifier δ (pair (snd p')) (pair (snd q'))"
        using pq Unifier_comp' by metis
      thus ?thesis using Cons.prems p'(1,2) q'(1,2) by simp
    qed

    show ?case by (metis 1 2 IH Un_iff setopslsst_cons subst_lsst_cons)
  qed simp
qed

lemma wf_pair_negchecks_map':
  assumes "wfst X (unlabel A)"
  shows "wfst X (unlabel (map (λG. (i,∀Y⟨∨≠: (F@G)⟩st)) M@A))"
using assms by (induct M) auto

lemma wf_pair_eqs_ineqs_map':
  fixes A::"('fun,'var,'lbl) labeled_strand"
  assumes "wfst X (unlabel A)"
          "Di ∈ set (subseqs (dbproj i D))"
          "fvpairs (unlabel D) ⊆ X"
  shows "wfst X (unlabel (
            (map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩st)) Di)@
            (map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st)) [d←dbproj i D. d ∉ set Di])@A))"
proof -
  let ?f = "[d←dbproj i D. d ∉ set Di]"
  define c1 where c1: "c1 = map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩st)) Di"
  define c2 where c2: "c2 = map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st)) ?f"
  define c3 where c3: "c3 = map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩st) (unlabel Di)"
  define c4 where c4: "c4 = map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩st) (unlabel ?f)"
  have ci_eqs: "c3 = unlabel c1" "c4 = unlabel c2" unfolding c1 c2 c3 c4 unlabel_def by auto
  have 1: "wfst X (unlabel (c2@A))"
    using wf_fun_pair_ineqs_map[OF assms(1)] ci_eqs(2) unlabel_append[of c2 A] c4
    by metis
  have 2: "fvpairs (unlabel Di) ⊆ X" 
    using assms(3) subseqs_set_subset(1)[OF assms(2)]
    unfolding unlabel_def dbproj_def
    by fastforce
  { fix B::"('fun,'var) strand" assume "wfst X B"
    hence "wfst X (unlabel c1@B)" using 2 unfolding c1 unlabel_def by (induct Di) auto
  } thus ?thesis using 1 unfolding c1 c2 unlabel_def by simp
qed

lemma trmssst_setopssst_wt_instance_ex:
  defines "M ≡ λA. trmslsst A ∪ pair ` setopssst (unlabel A)"
  assumes B: "∀b ∈ set B. ∃a ∈ set A. ∃δ. b = a ⋅lsstp δ ∧ wtsubst δ ∧ wftrms (subst_range δ)"
  shows "∀t ∈ M B. ∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ wtsubst δ ∧ wftrms (subst_range δ)"
proof
  let ?P = "λδ. wtsubst δ ∧ wftrms (subst_range δ)"

  fix t assume "t ∈ M B"
  then obtain b where b: "b ∈ set B" "t ∈ trmssstp (snd b) ∪ pair ` setopssstp (snd b)"
    unfolding M_def unfolding unlabel_def trmssst_def setopssst_def by auto
  then obtain a δ where a: "a ∈ set A" "b = a ⋅lsstp δ" and δ: "wtsubst δ" "wftrms (subst_range δ)"
    using B by meson

  note δ' = wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)]

  have "t ∈ M (A ⋅lsst δ)"
    using b(2) a
    unfolding M_def subst_apply_labeled_stateful_strand_def unlabel_def trmssst_def setopssst_def
    by auto
  moreover have "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" when "t ∈ trmslsst (A ⋅lsst δ)"
    using trmssst_unlabel_subst'[OF that] δ' unfolding M_def by blast
  moreover have "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" when t: "t ∈ pair ` setopssst (unlabel A ⋅sst δ)"
  proof -
    obtain p where p: "p ∈ setopssst (unlabel A ⋅sst δ)" "t = pair p" using t by blast
    then obtain q X where q: "q ∈ setopssst (unlabel A)" "p = q ⋅p rm_vars (set X) δ"
      using setopssst_subst'[OF p(1)] by blast
    hence "t = pair q ⋅ rm_vars (set X) δ"
      using fun_pair_subst[of q "rm_vars (set X) δ"] p(2) by presburger
    thus ?thesis using δ'[of "set X"] q(1) unfolding M_def by blast
  qed
  ultimately show "∃s ∈ M A. ∃δ. t = s ⋅ δ ∧ ?P δ" unfolding M_def unlabel_subst by fast
qed

lemma setopslsst_wt_instance_ex:
  assumes B: "∀b ∈ set B. ∃a ∈ set A. ∃δ. b = a ⋅lsstp δ ∧ wtsubst δ ∧ wftrms (subst_range δ)"
  shows "∀p ∈ setopslsst B. ∃q ∈ setopslsst A. ∃δ.
    fst p = fst q ∧ snd p = snd q ⋅p δ ∧ wtsubst δ ∧ wftrms (subst_range δ)"
proof
  let ?P = "λδ. wtsubst δ ∧ wftrms (subst_range δ)"

  fix p assume "p ∈ setopslsst B"
  then obtain b where b: "b ∈ set B" "p ∈ setopslsstp b" unfolding setopslsst_def by blast
  then obtain a δ where a: "a ∈ set A" "b = a ⋅lsstp δ" and δ: "wtsubst δ" "wftrms (subst_range δ)"
    using B by meson
  hence p: "p ∈ setopslsst (A ⋅lsst δ)"
    using b(2) unfolding setopslsst_def subst_apply_labeled_stateful_strand_def by auto
  
  obtain X q where q:
      "q ∈ setopslsst A" "fst p = fst q" "snd p = snd q ⋅p rm_vars X δ"
    using setopslsst_in_subst[OF p] by blast

  show "∃q ∈ setopslsst A. ∃δ. fst p = fst q ∧ snd p = snd q ⋅p δ ∧ ?P δ"
    using q wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)] by blast
qed

lemma deduct_proj_priv_term_prefix_ex_stateful:
  assumes A: "iksst (proj_unl l A) ⋅set I ⊢ t"
    and t: "¬{} ⊢c t"
  shows "∃B k s. (k = ⋆ ∨ k = ln l) ∧ prefix (B@[(k,receive⟨s⟩)]) A ∧
                 declassifiedlsst ((B@[(k,receive⟨s⟩)])) I = declassifiedlsst A I ∧
                 iksst (proj_unl l (B@[(k,receive⟨s⟩)])) = iksst (proj_unl l A)"
using A
proof (induction A rule: List.rev_induct)
  case Nil
  have "iksst (proj_unl l []) ⋅set I = {}" by auto
  thus ?case using Nil t deducts_eq_if_empty_ik[of t] by argo
next
  case (snoc a A)
  obtain k b where a: "a = (k,b)" by (metis surj_pair)
  let ?P = "k = ⋆ ∨ k = (ln l)"
  let ?Q = "∃s. b = receive⟨s⟩"

  have 0: "iksst (proj_unl l (A@[a])) = iksst (proj_unl l A)" when "?P ⟹ ¬?Q"
    using that iksst_snoc_no_receive_eq[OF that, of I "proj_unl l A"]
    unfolding iksst_def a by (cases "k = ⋆ ∨ k = (ln l)") auto

  have 1: "declassifiedlsst (A@[a]) I = declassifiedlsst A I" when "?P ⟹ ¬?Q"
    using that snoc.prems unfolding declassifiedlsst_alt_def a
    by (metis (no_types, lifting) UnCI UnE empty_iff insert_iff list.set prod.inject set_append)

  note 2 = snoc.prems snoc.IH 0 1

  show ?case
  proof (cases ?P)
    case True
    note T = this
    thus ?thesis
    proof (cases ?Q)
      case True thus ?thesis using T unfolding a by blast
    qed (use 2 in auto)
  qed (use 2 in auto)
qed

lemma constr_sem_stateful_proj_priv_term_prefix_obtain:
  assumes 𝒜': "prefix 𝒜' 𝒜" "constr_sem_stateful ℐτ (proj_unl n 𝒜'@[send⟨[t]⟩])"
    and t: "t ∈ Sec - declassifiedlsst 𝒜' ℐτ" "¬{} ⊢c t" "t ⋅ ℐτ = t"
  obtains B k' s where
    "k' = ⋆ ∨ k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s⟩)] B"
    "declassifiedlsst B ℐτ = declassifiedlsst 𝒜' ℐτ"
    "iklsst (proj n B) = iklsst (proj n 𝒜')"
    "constr_sem_stateful ℐτ (proj_unl n B@[send⟨[t]⟩])"
    "prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s⟩)] (proj n B)"
    "t ∈ Sec - declassifiedlsst (proj n B) ℐτ"
proof -
  have "iklsst (proj n 𝒜') ⋅set ℐτ ⊢ t"
    using 𝒜'(2) t(3) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]⟩]" ℐτ]
    by simp
  then obtain B k' s where B:
      "k' = ⋆ ∨ k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s⟩)] B"
      "declassifiedlsst B ℐτ = declassifiedlsst 𝒜' ℐτ"
      "iklsst (proj n B) = iklsst (proj n 𝒜')"
    using deduct_proj_priv_term_prefix_ex_stateful[OF _ t(2), of ℐτ n 𝒜']
    unfolding suffix_def by blast

  have B': "constr_sem_stateful ℐτ (proj_unl n B@[send⟨[t]⟩])"
    using B(5) 𝒜'(2) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]⟩]" ℐτ]
          strand_sem_append_stateful[of "{}" "{}" "proj_unl n B" _ ℐτ]
          prefix_proj(2)[OF B(2), of n]
    by (metis (no_types, lifting) append_Nil2 prefix_def strand_sem_stateful.simps(2))

  have B'': "prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s⟩)] (proj n B)"
            "t ∈ Sec - declassifiedlsst (proj n B) ℐτ"
    using 𝒜' t B(1-4) declassifiedlsst_proj_eq[of B ℐτ n]
    unfolding suffix_def prefix_def proj_def by auto

  show ?thesis by (rule that[OF B B' B''])
qed

lemma constr_sem_stateful_star_proj_no_leakage:
  fixes Sec P lbls k
  defines "no_leakage ≡ λ𝒜. ∄ℐτ ℬ s.
      prefix ℬ 𝒜 ∧ s ∈ Sec - declassifiedlsst ℬ ℐτ ∧ ℐτ ⊨s (unlabel ℬ@[send⟨[s]⟩])"
  assumes Sec: "ground Sec"
    and 𝒜: "∀(l,a) ∈ set 𝒜. l = ⋆"
  shows "no_leakage 𝒜"
proof (rule ccontr)
  assume "¬no_leakage 𝒜"
  then obtain I B s where B:
      "prefix B 𝒜" "s ∈ Sec - declassifiedlsst B I" "I ⊨s (unlabel B@[send⟨[s]⟩])"
    unfolding no_leakage_def by blast

  have 1: "¬(⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (B ⋅lsst I)} ⊢ s)"
    using B(2) unfolding declassifiedlsst_def by fast

  have 2: "iklsst (B ⋅lsst I) ⊢ s"
    using B(2,3) Sec strand_sem_append_stateful[of "{}" "{}" "unlabel B" "[send⟨[s]⟩]" I]
          trm_subst_ident[of s I] unlabel_subst[of B] iksst_subst[of "unlabel B"]
    by force

  have "l = ⋆" when "(l,c) ∈ set B" for l c
    using that 𝒜 B(1) set_mono_prefix by blast
  hence "l = ⋆" when "(l,c) ∈ set (B ⋅lsst I)" for l c
    using that unfolding subst_apply_labeled_stateful_strand_def by auto
  hence 3: "iklsst (B ⋅lsst I) = (⋃{set ts | ts. ⟨⋆, receive⟨ts⟩⟩ ∈ set (B ⋅lsst I)})"
    using in_iklsst_iff[of _ "B ⋅lsst I"] unfolding iksst_def unlabel_def by auto

  show False using 1 2 3 by force
qed

end

subsection ‹Lemmata: Properties of the Constraint Translation Function›
context labeled_stateful_typed_model
begin

lemma tr_par_labeled_rcv_iff:
  "B ∈ set (trpc A D) ⟹ (i, receive⟨t⟩st) ∈ set B ⟷ (i, receive⟨t⟩) ∈ set A"
by (induct A D arbitrary: B rule: trpc.induct) auto

lemma tr_par_declassified_eq:
  "B ∈ set (trpc A D) ⟹ declassifiedlst B I = declassifiedlsst A I"
using tr_par_labeled_rcv_iff unfolding declassifiedlst_alt_def declassifiedlsst_alt_def by simp

lemma tr_par_ik_eq:
  assumes "B ∈ set (trpc A D)"
  shows "ikst (unlabel B) = iksst (unlabel A)"
proof -
  have "{t. ∃i. (i, receive⟨t⟩st) ∈ set B} = {t. ∃i. (i, receive⟨t⟩) ∈ set A}"
    using tr_par_labeled_rcv_iff[OF assms] by simp
  moreover have
      "⋀C. {t. ∃i. (i, receive⟨t⟩st) ∈ set C} = {t. receive⟨t⟩st ∈ set (unlabel C)}"
      "⋀C. {t. ∃i. (i, receive⟨t⟩) ∈ set C} = {t. receive⟨t⟩ ∈ set (unlabel C)}"
    unfolding unlabel_def by force+
  ultimately show ?thesis unfolding iksst_def ikst_is_rcv_set by fast
qed

lemma tr_par_deduct_iff:
  assumes "B ∈ set (trpc A D)"
  shows "ikst (unlabel B) ⋅set I ⊢ t ⟷ iksst (unlabel A) ⋅set I ⊢ t"
using tr_par_ik_eq[OF assms] by metis

lemma tr_par_vars_subset:
  assumes "A' ∈ set (trpc A D)"
  shows "fvlst A' ⊆ fvsst (unlabel A) ∪ fvpairs (unlabel D)" (is ?P)
  and "bvarslst A' ⊆ bvarssst (unlabel A)" (is ?Q)
proof -
  show ?P using assms
  proof (induction "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
    case (ConsIn A' D ac t s AA A A')
    then obtain i B where iB: "A = (i,⟨ac: t ∈ s⟩)#B" "AA = unlabel B"
      unfolding unlabel_def by moura
    then obtain A'' d where *:
        "d ∈ set (dbproj i D)"
        "A' = (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩st)#A''"
        "A'' ∈ set (trpc B D)"
      using ConsIn.prems(1) by moura
    hence "fvlst A'' ⊆ fvsst (unlabel B) ∪ fvpairs (unlabel D)"
          "fv (pair (snd d)) ⊆ fvpairs (unlabel D)"
      apply (metis ConsIn.hyps(1)[OF iB(2)])
      using fvpairs_mono[OF dbproj_subset[of i D]]
            fv_pair_fvpairs_subset[OF *(1)]
      by blast
    thus ?case using * iB unfolding pair_def by auto
  next
    case (ConsDel A' D t s AA A A')
    then obtain i B where iB: "A = (i,delete⟨t,s⟩)#B" "AA = unlabel B"
      unfolding unlabel_def by moura

    define fltD1 where "fltD1 = (λDi. filter (λd. d ∉ set Di) D)"
    define fltD2 where "fltD2 = (λDi. filter (λd. d ∉ set Di) (dbproj i D))"
    define constr where "constr =
      (λDi. (map (λd. (i, ⟨check: (pair (t,s)) ≐ (pair (snd d))⟩st)) Di)@
            (map (λd. (i, ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st)) (fltD2 Di)))"

    from iB obtain A'' Di where *:
        "Di ∈ set (subseqs (dbproj i D))" "A' = (constr Di)@A''" "A'' ∈ set (trpc B (fltD1 Di))"
      using ConsDel.prems(1) unfolding constr_def fltD1_def fltD2_def by moura
    hence "fvlst A'' ⊆ fvsst AA ∪ fvpairs (unlabel (fltD1 Di))"
      unfolding constr_def fltD1_def by (metis ConsDel.hyps(1) iB(2))
    hence 1: "fvlst A'' ⊆ fvsst AA ∪ fvpairs (unlabel D)"
      using fvpairs_mono[of "unlabel (fltD1 Di)" "unlabel D"]
      unfolding unlabel_def fltD1_def by force
    
    have 2: "fvpairs (unlabel Di) ∪ fvpairs (unlabel (fltD1 Di)) ⊆ fvpairs (unlabel D)"
      using subseqs_set_subset(1)[OF *(1)]
      unfolding fltD1_def unlabel_def dbproj_def
      by auto

    have 5: "fvlst A' = fvlst (constr Di) ∪ fvlst A''" using * unfolding unlabel_def by force

    have "fvlst (constr Di) ⊆ fv t ∪ fv s ∪ fvpairs (unlabel Di) ∪ fvpairs (unlabel (fltD1 Di))"
      unfolding unlabel_def constr_def fltD1_def fltD2_def pair_def dbproj_def by auto
    hence 3: "fvlst (constr Di) ⊆ fv t ∪ fv s ∪ fvpairs (unlabel D)" using 2 by blast

    have 4: "fvsst (unlabel A) = fv t ∪ fv s ∪ fvsst AA" using iB by auto
    
    have "fvst (unlabel A') ⊆ fvsst (unlabel A) ∪ fvpairs (unlabel D)" using 1 3 4 5 by blast
    thus ?case by metis
  next
    case (ConsNegChecks A' D X F F' AA A A')
    then obtain i B where iB: "A = (i,NegChecks X F F')#B" "AA = unlabel B"
      unfolding unlabel_def by moura

    define D' where "D' ≡ ⋃(fvpairs ` set (trpairs F' (unlabel (dbproj i D))))"
    define constr where "constr = map (λG. (i,∀X⟨∨≠: (F@G)⟩st)) (trpairs F' (map snd (dbproj i D)))"

    from iB obtain A'' where *: "A'' ∈ set (trpc B D)" "A' = constr@A''"
      using ConsNegChecks.prems(1) unfolding constr_def by moura
    hence "fvlst A'' ⊆ fvsst AA ∪ fvpairs (unlabel D)"
      by (metis ConsNegChecks.hyps(1) iB(2))
    hence **: "fvlst A'' ⊆ fvsst AA ∪ fvpairs (unlabel D)" by auto

    have 1: "fvlst constr ⊆ (D' ∪ fvpairs F) - set X"
      unfolding D'_def constr_def unlabel_def by auto

    have "set (unlabel (dbproj i D)) ⊆ set (unlabel D)" unfolding unlabel_def dbproj_def by auto
    hence 2: "D' ⊆ fvpairs F' ∪ fvpairs (unlabel D)"
      using trpairs_vars_subset'[of F' "unlabel (dbproj i D)"] fvpairs_mono
      unfolding D'_def by blast

    have 3: "fvlst A' ⊆ ((fvpairs F' ∪ fvpairs F) - set X) ∪ fvpairs (unlabel D) ∪ fvlst A''"
      using 1 2 *(2) unfolding unlabel_def by fastforce

    have 4: "fvsst AA ⊆ fvsst (unlabel A)" by (metis ConsNegChecks.hyps(2) fvsst_cons_subset)

    have 5: "fvpairs F' ∪ fvpairs F - set X ⊆ fvsst (unlabel A)"
      using ConsNegChecks.hyps(2) unfolding unlabel_def by force

    show ?case using ** 3 4 5 by blast
  qed (fastforce simp add: unlabel_def)+

  show ?Q using assms
    apply (induct "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
    by (fastforce simp add: unlabel_def)+
qed

lemma tr_par_vars_disj:
  assumes "A' ∈ set (trpc A D)" "fvpairs (unlabel D) ∩ bvarssst (unlabel A) = {}"
  and "fvsst (unlabel A) ∩ bvarssst (unlabel A) = {}"
  shows "fvlst A' ∩ bvarslst A' = {}"
using assms tr_par_vars_subset by fast

lemma tr_par_trms_subset:
  assumes "A' ∈ set (trpc A D)"
  shows "trmslst A' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪ pair ` snd ` set D"
using assms
proof (induction A D arbitrary: A' rule: trpc.induct)
  case 1 thus ?case by simp
next
  case (2 i t A D)
  then obtain A'' where A'': "A' = (i,send⟨t⟩st)#A''" "A'' ∈ set (trpc A D)" by moura
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪ pair ` snd ` set D"
    by (metis "2.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (3 i t A D)
  then obtain A'' where A'': "A' = (i,receive⟨t⟩st)#A''" "A'' ∈ set (trpc A D)"
    by moura
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪ pair ` snd ` set D"
    by (metis "3.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (4 i ac t t' A D)
  then obtain A'' where A'': "A' = (i,⟨ac: t ≐ t'⟩st)#A''" "A'' ∈ set (trpc A D)"
    by moura
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪ pair ` snd ` set D"
    by (metis "4.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (5 i t s A D)
  hence "A' ∈ set (trpc A (List.insert (i,t,s) D))" by simp
  hence "trmslst A' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪
                      pair ` snd ` set (List.insert (i,t,s) D)"
    by (metis "5.IH")
  thus ?case by (auto simp add: setopssst_def)
next
  case (6 i t s A D)
  from 6 obtain Di A'' B C where A'':
      "Di ∈ set (subseqs (dbproj i D))" "A'' ∈ set (trpc A [d←D. d ∉ set Di])" "A' = (B@C)@A''"
      "B = map (λd. (i,⟨check: (pair (t,s)) ≐ (pair (snd d))⟩st)) Di"
      "C = map (λd. (i,∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st)) [d←dbproj i D. d ∉ set Di]"
    by moura
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪
                       pair ` snd ` set [d←D. d ∉ set Di]"
    by (metis "6.IH")
  moreover have "set [d←D. d ∉ set Di] ⊆ set D" using set_filter by auto
  ultimately have
      "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪ pair ` snd ` set D"
    by blast
  hence "trmslst A'' ⊆ trmssst (unlabel ((i,delete⟨t,s⟩)#A)) ∪
                        pair ` setopssst (unlabel ((i,delete⟨t,s⟩)#A)) ∪
                        pair ` snd ` set D"
    using setopssst_cons_subset trmssst_cons
    by (auto simp add: setopssst_def)
  moreover have "set Di ⊆ set D" "set [d←dbproj i D . d ∉ set Di] ⊆ set D"
    using subseqs_set_subset[OF A''(1)] unfolding dbproj_def by auto
  hence "trmsst (unlabel B) ⊆ insert (pair (t, s)) (pair ` snd ` set D)"
        "trmsst (unlabel C) ⊆ insert (pair (t, s)) (pair ` snd ` set D)"
    using A''(4,5) unfolding unlabel_def by auto
  hence "trmsst (unlabel (B@C)) ⊆ insert (pair (t,s)) (pair ` snd ` set D)"
    using unlabel_append[of B C] by auto
  moreover have "pair (t,s) ∈ pair ` setopssst (delete⟨t,s⟩#unlabel A)" by (simp add: setopssst_def)
  ultimately show ?case
    using A''(3) trmsst_append[of "unlabel (B@C)" "unlabel A'"] unlabel_append[of "B@C" A'']
    by (auto simp add: setopssst_def)
next
  case (7 i ac t s A D)
  from 7 obtain d A'' where A'':
      "d ∈ set (dbproj i D)" "A'' ∈ set (trpc A D)"
      "A' = (i,⟨ac: (pair (t,s)) ≐ (pair (snd d))⟩st)#A''"
    by moura
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair `