Theory Labeled_Stateful_Strands

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

section ‹Labeled Stateful Strands›
theory Labeled_Stateful_Strands
imports Stateful_Strands Labeled_Strands
begin

subsection ‹Definitions›
text‹Syntax for stateful strand labels›
abbreviation Star_step ("⟨⋆, _⟩") where
  "⟨⋆, (s::('a,'b) stateful_strand_step)⟩ ≡ (⋆, s)"

abbreviation LabelN_step ("⟨_, _⟩") where
  "⟨(l::'a), (s::('b,'c) stateful_strand_step)⟩ ≡ (ln l, s)"


text‹Database projection›
definition dbproj where "dbproj l D ≡ filter (λd. fst d = l) D"

text‹The type of labeled stateful strands›
type_synonym ('a,'b,'c) labeled_stateful_strand_step = "'c strand_label × ('a,'b) stateful_strand_step"
type_synonym ('a,'b,'c) labeled_stateful_strand = "('a,'b,'c) labeled_stateful_strand_step list"

text‹Dual strands›
fun duallsstp::"('a,'b,'c) labeled_stateful_strand_step ⇒ ('a,'b,'c) labeled_stateful_strand_step"
where
  "duallsstp (l,send⟨t⟩) = (l,receive⟨t⟩)"
| "duallsstp (l,receive⟨t⟩) = (l,send⟨t⟩)"
| "duallsstp x = x"

definition duallsst::"('a,'b,'c) labeled_stateful_strand ⇒ ('a,'b,'c) labeled_stateful_strand"
where
  "duallsst ≡ map duallsstp"

text‹Substitution application›
fun subst_apply_labeled_stateful_strand_step::
  "('a,'b,'c) labeled_stateful_strand_step ⇒ ('a,'b) subst ⇒
   ('a,'b,'c) labeled_stateful_strand_step"
  (infix "⋅lsstp" 51) where
  "(l,s) ⋅lsstp θ  = (l,s ⋅sstp θ)"

definition subst_apply_labeled_stateful_strand::
  "('a,'b,'c) labeled_stateful_strand ⇒ ('a,'b) subst ⇒ ('a,'b,'c) labeled_stateful_strand"
  (infix "⋅lsst" 51) where
  "S ⋅lsst θ ≡ map (λx. x ⋅lsstp θ) S"

text‹Definitions lifted from stateful strands›
abbreviation wfrestrictedvarslsst where "wfrestrictedvarslsst S ≡ wfrestrictedvarssst (unlabel S)"

abbreviation iklsst where "iklsst S ≡ iksst (unlabel S)"

abbreviation dblsst where "dblsst S ≡ dbsst (unlabel S)"
abbreviation db'lsst where "db'lsst S ≡ db'sst (unlabel S)"

abbreviation trmslsst where "trmslsst S ≡ trmssst (unlabel S)"
abbreviation trms_projlsst where "trms_projlsst n S ≡ trmssst (proj_unl n S)"

abbreviation varslsst where "varslsst S ≡ varssst (unlabel S)"
abbreviation vars_projlsst where "vars_projlsst n S ≡ varssst (proj_unl n S)"

abbreviation bvarslsst where "bvarslsst S ≡ bvarssst (unlabel S)"
abbreviation fvlsst where "fvlsst S ≡ fvsst (unlabel S)"

text‹Labeled set-operations›
fun setopslsstp where
  "setopslsstp (i,insert⟨t,s⟩) = {(i,t,s)}"
| "setopslsstp (i,delete⟨t,s⟩) = {(i,t,s)}"
| "setopslsstp (i,⟨_: t ∈ s⟩) = {(i,t,s)}"
| "setopslsstp (i,∀_⟨∨≠: _ ∨∉: F'⟩) = ((λ(t,s). (i,t,s)) ` set F')"
| "setopslsstp _ = {}"

definition setopslsst where
  "setopslsst S ≡ ⋃(setopslsstp ` set S)"


subsection ‹Minor Lemmata›
lemma in_iklsst_iff: "t ∈ iklsst A ⟷ (∃l ts. (l,receive⟨ts⟩) ∈ set A ∧ t ∈ set ts)"
unfolding unlabel_def iksst_def by force

lemma iklsst_concat: "iklsst (concat xs) = ⋃(iklsst ` set xs)"
by (induct xs) auto

lemma iklsst_Cons[simp]:
  "iklsst ((l,send⟨ts⟩)#A) = iklsst A" (is ?A)
  "iklsst ((l,receive⟨ts⟩)#A) = set ts ∪ iklsst A" (is ?B)
  "iklsst ((l,⟨ac: t ≐ s⟩)#A) = iklsst A" (is ?C)
  "iklsst ((l,insert⟨t,s⟩)#A) = iklsst A" (is ?D)
  "iklsst ((l,delete⟨t,s⟩)#A) = iklsst A" (is ?E)
  "iklsst ((l,⟨ac: t ∈ s⟩)#A) = iklsst A" (is ?F)
  "iklsst ((l,∀X⟨∨≠: F ∨∉: G⟩)#A) = iklsst A" (is ?G)
proof -
  note 0 = iksst_append[of _ "unlabel A"]
  note 1 = in_iksst_iff
  show ?A using 0[of "[send⟨ts⟩]"] 1[of _ "[send⟨ts⟩]"] by auto
  show ?B using 0[of "[receive⟨ts⟩]"] 1[of _ "[receive⟨ts⟩]"] by auto
  show ?C using 0[of "[⟨ac: t ≐ s⟩]"] 1[of _ "[⟨ac: t ≐ s⟩]"] by auto
  show ?D using 0[of "[insert⟨t,s⟩]"] 1[of _ "[insert⟨t,s⟩]"] by auto
  show ?E using 0[of "[delete⟨t,s⟩]"] 1[of _ "[delete⟨t,s⟩]"] by auto
  show ?F using 0[of "[⟨ac: t ∈ s⟩]"] 1[of _ "[⟨ac: t ∈ s⟩]"] by auto
  show ?G using 0[of "[∀X⟨∨≠: F ∨∉: G⟩]"] 1[of _ "[∀X⟨∨≠: F ∨∉: G⟩]"] by auto
qed

lemma subst_lsstp_fst_eq:
  "fst (a ⋅lsstp δ) = fst a"
by (cases a) auto

lemma subst_lsst_map_fst_eq:
  "map fst (S ⋅lsst δ) = map fst S"
using subst_lsstp_fst_eq unfolding subst_apply_labeled_stateful_strand_def by auto

lemma subst_lsst_nil[simp]: "[] ⋅lsst δ = []"
by (simp add: subst_apply_labeled_stateful_strand_def)

lemma subst_lsst_cons: "a#A ⋅lsst δ = (a ⋅lsstp δ)#(A ⋅lsst δ)"
by (simp add: subst_apply_labeled_stateful_strand_def)

lemma subst_lsstp_id_subst: "a ⋅lsstp Var = a"
proof -
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  show ?thesis unfolding a by (cases b) auto
qed

lemma subst_lsst_id_subst: "A ⋅lsst Var = A"
by (induct A) (simp, metis subst_lsstp_id_subst subst_lsst_cons)

lemma subst_lsst_singleton: "[(l,s)] ⋅lsst δ = [(l,s ⋅sstp δ)]"
by (simp add: subst_apply_labeled_stateful_strand_def)

lemma subst_lsst_append: "A@B ⋅lsst δ = (A ⋅lsst δ)@(B ⋅lsst δ)"
by (simp add: subst_apply_labeled_stateful_strand_def)

lemma subst_lsst_append_inv:
  assumes "A ⋅lsst δ = B1@B2"
  shows "∃A1 A2. A = A1@A2 ∧ A1 ⋅lsst δ = B1 ∧ A2 ⋅lsst δ = B2"
using assms
proof (induction A arbitrary: B1 B2)
  case (Cons a A)
  note prems = Cons.prems
  note IH = Cons.IH
  show ?case
  proof (cases B1)
    case Nil
    then obtain b B3 where "B2 = b#B3" "a ⋅lsstp δ = b" "A ⋅lsst δ = B3"
      using prems subst_lsst_cons by fastforce
    thus ?thesis by (simp add: Nil subst_apply_labeled_stateful_strand_def)
  next
    case (Cons b B3)
    hence "a ⋅lsstp δ = b" "A ⋅lsst δ = B3@B2"
      using prems by (simp_all add: subst_lsst_cons)
    thus ?thesis by (metis Cons_eq_appendI Cons IH subst_lsst_cons) 
  qed
qed (metis append_is_Nil_conv subst_lsst_nil)

lemma subst_lsst_memI[intro]: "x ∈ set A ⟹ x ⋅lsstp δ ∈ set (A ⋅lsst δ)"
by (metis image_eqI set_map subst_apply_labeled_stateful_strand_def)

lemma subst_lsstpD:
  "a ⋅lsstp σ = (n,send⟨ts⟩) ⟹ ∃ts'. ts = ts' ⋅list σ ∧ a = (n,send⟨ts'⟩)"
    (is "?A ⟹ ?A'")
  "a ⋅lsstp σ = (n,receive⟨ts⟩) ⟹ ∃ts'. ts = ts' ⋅list σ ∧ a = (n,receive⟨ts'⟩)"
    (is "?B ⟹ ?B'")
  "a ⋅lsstp σ = (n,⟨c: t ≐ s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,⟨c: t' ≐ s'⟩)"
    (is "?C ⟹ ?C'")
  "a ⋅lsstp σ = (n,insert⟨t,s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,insert⟨t',s'⟩)"
    (is "?D ⟹ ?D'")
  "a ⋅lsstp σ = (n,delete⟨t,s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,delete⟨t',s'⟩)"
    (is "?E ⟹ ?E'")
  "a ⋅lsstp σ = (n,⟨c: t ∈ s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,⟨c: t' ∈ s'⟩)"
    (is "?F ⟹ ?F'")
  "a ⋅lsstp σ = (n,∀X⟨∨≠: F ∨∉: G⟩) ⟹
    ∃F' G'. F = F' ⋅pairs rm_vars (set X) σ ∧ G = G' ⋅pairs rm_vars (set X) σ ∧
            a = (n,∀X⟨∨≠: F' ∨∉: G'⟩)"
    (is "?G ⟹ ?G'")
  "a ⋅lsstp σ = (n,⟨t != s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,⟨t' != s'⟩)"
    (is "?H ⟹ ?H'")
  "a ⋅lsstp σ = (n,⟨t not in s⟩) ⟹ ∃t' s'. t = t' ⋅ σ ∧ s = s' ⋅ σ ∧ a = (n,⟨t' not in s'⟩)"
    (is "?I ⟹ ?I'")
proof -
  obtain m b where a: "a = (m,b)" by (metis surj_pair)
  show "?A ⟹ ?A'" "?B ⟹ ?B'" "?C ⟹ ?C'" "?D ⟹ ?D'" "?E ⟹ ?E'" "?F ⟹ ?F'" "?G ⟹ ?G'"
       "?H ⟹ ?H'" "?I ⟹ ?I'"
    by (cases b; auto simp add: a subst_apply_pairs_def; fail)+
qed

lemma subst_lsst_memD:
  "(n,receive⟨ts⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃us. (n,receive⟨us⟩) ∈ set S ∧ ts = us ⋅list σ"
  "(n,send⟨ts⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃us. (n,send⟨us⟩) ∈ set S ∧ ts = us ⋅list σ"
  "(n,⟨ac: t ≐ s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,⟨ac: u ≐ v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
  "(n,insert⟨t, s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,insert⟨u, v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
  "(n,delete⟨t, s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,delete⟨u, v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
  "(n,⟨ac: t ∈ s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,⟨ac: u ∈ v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
  "(n,∀X⟨∨≠: F ∨∉: G⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃F' G'. (n,∀X⟨∨≠: F' ∨∉: G'⟩) ∈ set S ∧
            F = F' ⋅pairs rm_vars (set X) σ ∧
            G = G' ⋅pairs rm_vars (set X) σ"
  "(n,⟨t != s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,⟨u != v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
  "(n,⟨t not in s⟩) ∈ set (S ⋅lsst σ) ⟹
    ∃u v. (n,⟨u not in v⟩) ∈ set S ∧ t = u ⋅ σ ∧ s = v ⋅ σ"
proof (induction S)
  case (Cons b S)
  obtain m a where a: "b = (m,a)" by (metis surj_pair)
  have *: "x ∈ set (S ⋅lsst σ)"
    when "x ∈ set (b#S ⋅lsst σ)" "x ≠ b ⋅lsstp σ" for x
    using that by (simp add: subst_apply_labeled_stateful_strand_def)

  { case 1 thus ?case using Cons.IH(1)[OF *] a by (cases a) auto }
  { case 2 thus ?case using Cons.IH(2)[OF *] a by (cases a) auto }
  { case 3 thus ?case using Cons.IH(3)[OF *] a by (cases a) auto }
  { case 4 thus ?case using Cons.IH(4)[OF *] a by (cases a) auto }
  { case 5 thus ?case using Cons.IH(5)[OF *] a by (cases a) auto }
  { case 6 thus ?case using Cons.IH(6)[OF *] a by (cases a) auto }
  { case 7 thus ?case using Cons.IH(7)[OF *] a by (cases a) auto }
  { case 8 show ?case
    proof (cases a)
      case (NegChecks Y F' G') thus ?thesis
      proof (cases "(n,⟨t != s⟩) = b ⋅lsstp σ")
        case True thus ?thesis using subst_lsstpD(8)[of b σ n t s] by auto
      qed (use 8 Cons.IH(8)[OF *] a in auto)
    qed (use 8 Cons.IH(8)[OF *] a in simp_all)
  }
  { case 9 show ?case
    proof (cases a)
      case (NegChecks Y F' G') thus ?thesis
      proof (cases "(n,⟨t not in s⟩) = b ⋅lsstp σ")
        case True thus ?thesis using subst_lsstpD(9)[of b σ n t s] by auto
      qed (use 9 Cons.IH(9)[OF *] a in auto)
    qed (use 9 Cons.IH(9)[OF *] a in simp_all)
  }
qed simp_all

lemma subst_lsst_unlabel_cons: "unlabel ((l,b)#A ⋅lsst θ) = (b ⋅sstp θ)#(unlabel (A ⋅lsst θ))"
by (simp add: subst_apply_labeled_stateful_strand_def)

lemma subst_lsst_unlabel: "unlabel (A ⋅lsst δ) = unlabel A ⋅sst δ"
proof (induction A)
  case (Cons a A)
  then obtain l b where "a = (l,b)" by (metis surj_pair)
  thus ?case
    using Cons
    by (simp add: subst_apply_labeled_stateful_strand_def subst_apply_stateful_strand_def)
qed simp

lemma subst_lsst_unlabel_member[intro]:
  assumes "x ∈ set (unlabel A)"
  shows "x ⋅sstp δ ∈ set (unlabel (A ⋅lsst δ))"
proof -
  obtain l where x: "(l,x) ∈ set A" using assms unfolding unlabel_def by atomize_elim auto
  thus ?thesis
    using subst_lsst_memI
    by (metis unlabel_def in_set_zipE subst_apply_labeled_stateful_strand_step.simps zip_map_fst_snd)
qed

lemma subst_lsst_prefix:
  assumes "prefix B (A ⋅lsst θ)"
  shows "∃C. C ⋅lsst θ = B ∧ prefix C A"
using assms
proof (induction A rule: List.rev_induct)
  case (snoc a A) thus ?case
  proof (cases "B = A@[a] ⋅lsst θ")
    case False thus ?thesis
      using snoc by (auto simp add: subst_lsst_append[of A] subst_lsst_cons)
  qed auto
qed simp

lemma subst_lsst_tl:
  "tl (S ⋅lsst δ) = tl S ⋅lsst δ"
by (metis map_tl subst_apply_labeled_stateful_strand_def)

lemma duallsst_tl:
  "tl (duallsst S) = duallsst (tl S)"
by (metis map_tl duallsst_def)

lemma duallsstp_fst_eq:
  "fst (duallsstp a) = fst a"
proof -
  obtain l b where "a = (l,b)" by (metis surj_pair)
  thus ?thesis by (cases b) auto
qed

lemma duallsst_map_fst_eq:
  "map fst (duallsst S) = map fst S"
using duallsstp_fst_eq unfolding duallsst_def by auto

lemma duallsst_nil[simp]: "duallsst [] = []"
by (simp add: duallsst_def)

lemma duallsst_Cons[simp]:
  "duallsst ((l,send⟨ts⟩)#A) = (l,receive⟨ts⟩)#(duallsst A)"
  "duallsst ((l,receive⟨ts⟩)#A) = (l,send⟨ts⟩)#(duallsst A)"
  "duallsst ((l,⟨a: t ≐ s⟩)#A) = (l,⟨a: t ≐ s⟩)#(duallsst A)"
  "duallsst ((l,insert⟨t,s⟩)#A) = (l,insert⟨t,s⟩)#(duallsst A)"
  "duallsst ((l,delete⟨t,s⟩)#A) = (l,delete⟨t,s⟩)#(duallsst A)"
  "duallsst ((l,⟨a: t ∈ s⟩)#A) = (l,⟨a: t ∈ s⟩)#(duallsst A)"
  "duallsst ((l,∀X⟨∨≠: F ∨∉: G⟩)#A) = (l,∀X⟨∨≠: F ∨∉: G⟩)#(duallsst A)"
by (simp_all add: duallsst_def)

lemma duallsst_append[simp]: "duallsst (A@B) = duallsst A@duallsst B"
by (simp add: duallsst_def)

lemma duallsstp_subst: "duallsstp (s ⋅lsstp δ) = (duallsstp s) ⋅lsstp δ"
proof -
  obtain l x  where s: "s = (l,x)" by atomize_elim auto
  thus ?thesis by (cases x) (auto simp add: subst_apply_labeled_stateful_strand_def)
qed

lemma duallsst_subst: "duallsst (S ⋅lsst δ) = (duallsst S) ⋅lsst δ"
proof (induction S)
  case (Cons s S) thus ?case
    using Cons duallsstp_subst[of s δ]
    by (simp add: duallsst_def subst_apply_labeled_stateful_strand_def)
qed (simp add: duallsst_def subst_apply_labeled_stateful_strand_def)

lemma duallsst_subst_unlabel: "unlabel (duallsst (S ⋅lsst δ)) = unlabel (duallsst S) ⋅sst δ" 
by (metis duallsst_subst subst_lsst_unlabel)

lemma duallsst_subst_cons: "duallsst (a#A ⋅lsst σ) = (duallsstp a ⋅lsstp σ)#(duallsst (A ⋅lsst σ))"
by (metis duallsst_subst list.simps(9) duallsst_def subst_apply_labeled_stateful_strand_def)

lemma duallsst_subst_append: "duallsst (A@B ⋅lsst σ) = (duallsst A@duallsst B) ⋅lsst σ"
by (metis (no_types) duallsst_subst duallsst_append)

lemma duallsst_subst_snoc: "duallsst (A@[a] ⋅lsst σ) = (duallsst A ⋅lsst σ)@[duallsstp a ⋅lsstp σ]"
by (metis duallsst_def duallsst_subst duallsst_subst_cons list.map(1) map_append
          subst_apply_labeled_stateful_strand_def)

lemma duallsst_memberD:
  assumes "(l,a) ∈ set (duallsst A)"
  shows "∃b. (l,b) ∈ set A ∧ duallsstp (l,b) = (l,a)"
  using assms
proof (induction A)
  case (Cons c A)
  hence "(l,a) ∈ set (duallsst A) ∨ duallsstp c = (l,a)" unfolding duallsst_def by force
  thus ?case
  proof
    assume "(l,a) ∈ set (duallsst A)" thus ?case using Cons.IH by auto
  next
    assume a: "duallsstp c = (l,a)"
    obtain i b where b: "c = (i,b)" by (metis surj_pair)
    thus ?case using a by (cases b) auto
  qed
qed simp

lemma duallsst_memberD':
  assumes a: "a ∈ set (duallsst A ⋅lsst δ)"
  obtains b where "b ∈ set A" "a = duallsstp b ⋅lsstp δ" "fst a = fst b"
proof -
  obtain l a' where a': "a = (l,a')" by (metis surj_pair)
  then obtain b' where b': "(l,b') ∈ set A" "(l,a') = duallsstp ((l,b') ⋅lsstp δ)"
    using a duallsst_subst[of A δ] duallsst_memberD[of l a' "A ⋅lsst δ"]
    unfolding subst_apply_labeled_stateful_strand_def by auto

  show thesis
    using that[OF b'(1) b'(2)[unfolded duallsstp_subst[of "(l,b')" δ] a'[symmetric]], unfolded a']
    by auto
qed

lemma duallsstp_inv:
  assumes "duallsstp (l, a) = (k, b)"
  shows "l = k"
    and "a = receive⟨t⟩ ⟹ b = send⟨t⟩"
    and "a = send⟨t⟩ ⟹ b = receive⟨t⟩"
    and "(∄t. a = receive⟨t⟩ ∨ a = send⟨t⟩) ⟹ b = a"
proof -
  show "l = k" using assms by (cases a) auto
  show "a = receive⟨t⟩ ⟹ b = send⟨t⟩" using assms by (cases a) auto
  show "a = send⟨t⟩ ⟹ b = receive⟨t⟩" using assms by (cases a) auto
  show "(∄t. a = receive⟨t⟩ ∨ a = send⟨t⟩) ⟹ b = a" using assms by (cases a) auto
qed

lemma duallsst_self_inverse: "duallsst (duallsst A) = A"
proof (induction A)
  case (Cons a A)
  obtain l b where "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons by (cases b) auto
qed simp

lemma duallsst_unlabel_cong:
  assumes "unlabel S = unlabel S'"
  shows "unlabel (duallsst S) = unlabel (duallsst S')"
using assms
proof (induction S arbitrary: S')
  case (Cons x S S')
  obtain y S'' where y: "S' = y#S''" using Cons.prems unfolding unlabel_def by force
  hence IH: "unlabel (duallsst S) = unlabel (duallsst S'')" using Cons by (simp add: unlabel_def)

  have "snd x = snd y" using Cons y by simp
  then obtain lx ly a where a: "x = (lx,a)" "y = (ly,a)" by (metis prod.exhaust_sel)

  have "snd (duallsstp x) = snd (duallsstp y)" unfolding a by (cases a) simp_all
  thus ?case using IH unfolding unlabel_def duallsst_def y by force
qed (simp add: unlabel_def duallsst_def)

lemma varssst_unlabel_duallsst_eq: "varslsst (duallsst A) = varslsst 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) auto
qed simp

lemma fvsst_unlabel_duallsst_eq: "fvlsst (duallsst A) = fvlsst 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) auto
qed simp

lemma bvarssst_unlabel_duallsst_eq: "bvarslsst (duallsst A) = bvarslsst 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+
qed simp

lemma varssst_unlabel_Cons: "varslsst ((l,b)#A) = varssstp b ∪ varslsst A"
by (metis unlabel_Cons(1) varssst_Cons)

lemma fvsst_unlabel_Cons: "fvlsst ((l,b)#A) = fvsstp b ∪ fvlsst A"
by (metis unlabel_Cons(1) fvsst_Cons)

lemma bvarssst_unlabel_Cons: "bvarslsst ((l,b)#A) = set (bvarssstp b) ∪ bvarslsst A"
by (metis unlabel_Cons(1) bvarssst_Cons)

lemma bvarslsst_subst: "bvarslsst (A ⋅lsst δ) = bvarslsst A"
by (metis subst_lsst_unlabel bvarssst_subst)

lemma duallsst_member:
  assumes "(l,x) ∈ set A"
    and "¬is_Receive x" "¬is_Send x"
  shows "(l,x) ∈ set (duallsst A)"
using assms
proof (induction A)
  case (Cons a A) thus ?case using assms(2,3) by (cases x) (auto simp add: duallsst_def)
qed simp

lemma duallsst_unlabel_member:
  assumes "x ∈ set (unlabel A)"
    and "¬is_Receive x" "¬is_Send x"
  shows "x ∈ set (unlabel (duallsst A))"
using assms duallsst_member[of _ _ A]
  by (meson unlabel_in unlabel_mem_has_label)

lemma duallsst_steps_iff:
  "(l,send⟨ts⟩) ∈ set A ⟷ (l,receive⟨ts⟩) ∈ set (duallsst A)"
  "(l,receive⟨ts⟩) ∈ set A ⟷ (l,send⟨ts⟩) ∈ set (duallsst A)"
  "(l,⟨c: t ≐ s⟩) ∈ set A ⟷ (l,⟨c: t ≐ s⟩) ∈ set (duallsst A)"
  "(l,insert⟨t,s⟩) ∈ set A ⟷ (l,insert⟨t,s⟩) ∈ set (duallsst A)"
  "(l,delete⟨t,s⟩) ∈ set A ⟷ (l,delete⟨t,s⟩) ∈ set (duallsst A)"
  "(l,⟨c: t ∈ s⟩) ∈ set A ⟷ (l,⟨c: t ∈ s⟩) ∈ set (duallsst A)"
  "(l,∀X⟨∨≠: F ∨∉: G⟩) ∈ set A ⟷ (l,∀X⟨∨≠: F ∨∉: G⟩) ∈ set (duallsst A)"
proof (induction A)
  case (Cons a A)
  obtain j b where a: "a = (j,b)" by (metis surj_pair)
  { case 1 thus ?case by (cases b) (simp_all add: Cons.IH(1) a duallsst_def) }
  { case 2 thus ?case by (cases b) (simp_all add: Cons.IH(2) a duallsst_def) }
  { case 3 thus ?case by (cases b) (simp_all add: Cons.IH(3) a duallsst_def) }
  { case 4 thus ?case by (cases b) (simp_all add: Cons.IH(4) a duallsst_def) }
  { case 5 thus ?case by (cases b) (simp_all add: Cons.IH(5) a duallsst_def) }
  { case 6 thus ?case by (cases b) (simp_all add: Cons.IH(6) a duallsst_def) }
  { case 7 thus ?case by (cases b) (simp_all add: Cons.IH(7) a duallsst_def) }
qed (simp_all add: duallsst_def)

lemma duallsst_unlabel_steps_iff:
  "send⟨ts⟩ ∈ set (unlabel A) ⟷ receive⟨ts⟩ ∈ set (unlabel (duallsst A))"
  "receive⟨ts⟩ ∈ set (unlabel A) ⟷ send⟨ts⟩ ∈ set (unlabel (duallsst A))"
  "⟨c: t ≐ s⟩ ∈ set (unlabel A) ⟷ ⟨c: t ≐ s⟩ ∈ set (unlabel (duallsst A))"
  "insert⟨t,s⟩ ∈ set (unlabel A) ⟷ insert⟨t,s⟩ ∈ set (unlabel (duallsst A))"
  "delete⟨t,s⟩ ∈ set (unlabel A) ⟷ delete⟨t,s⟩ ∈ set (unlabel (duallsst A))"
  "⟨c: t ∈ s⟩ ∈ set (unlabel A) ⟷ ⟨c: t ∈ s⟩ ∈ set (unlabel (duallsst A))"
  "∀X⟨∨≠: F ∨∉: G⟩ ∈ set (unlabel A) ⟷ ∀X⟨∨≠: F ∨∉: G⟩ ∈ set (unlabel (duallsst A))"
using duallsst_steps_iff(1,2)[of _ ts A]
      duallsst_steps_iff(3,6)[of _ c t s A]
      duallsst_steps_iff(4,5)[of _ t s A]
      duallsst_steps_iff(7)[of _ X F G A]
by (meson unlabel_in unlabel_mem_has_label)+

lemma duallsst_list_all:
  "list_all is_Receive (unlabel A) ⟷ list_all is_Send (unlabel (duallsst A))"
  "list_all is_Send (unlabel A) ⟷ list_all is_Receive (unlabel (duallsst A))"
  "list_all is_Equality (unlabel A) ⟷ list_all is_Equality (unlabel (duallsst A))"
  "list_all is_Insert (unlabel A) ⟷ list_all is_Insert (unlabel (duallsst A))"
  "list_all is_Delete (unlabel A) ⟷ list_all is_Delete (unlabel (duallsst A))"
  "list_all is_InSet (unlabel A) ⟷ list_all is_InSet (unlabel (duallsst A))"
  "list_all is_NegChecks (unlabel A) ⟷ list_all is_NegChecks (unlabel (duallsst A))"
  "list_all is_Assignment (unlabel A) ⟷ list_all is_Assignment (unlabel (duallsst A))"
  "list_all is_Check (unlabel A) ⟷ list_all is_Check (unlabel (duallsst A))"
  "list_all is_Update (unlabel A) ⟷ list_all is_Update (unlabel (duallsst A))"
  "list_all is_Check_or_Assignment (unlabel A) ⟷
    list_all is_Check_or_Assignment (unlabel (duallsst A))"
proof (induct A)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  { case 1 thus ?case using Cons.hyps(1) a by (cases b) auto }
  { case 2 thus ?case using Cons.hyps(2) a by (cases b) auto }
  { case 3 thus ?case using Cons.hyps(3) a by (cases b) auto }
  { case 4 thus ?case using Cons.hyps(4) a by (cases b) auto }
  { case 5 thus ?case using Cons.hyps(5) a by (cases b) auto }
  { case 6 thus ?case using Cons.hyps(6) a by (cases b) auto }
  { case 7 thus ?case using Cons.hyps(7) a by (cases b) auto }
  { case 8 thus ?case using Cons.hyps(8) a by (cases b) auto }
  { case 9 thus ?case using Cons.hyps(9) a by (cases b) auto }
  { case 10 thus ?case using Cons.hyps(10) a by (cases b) auto }
  { case 11 thus ?case using Cons.hyps(11) a by (cases b) auto }
qed simp_all

lemma duallsst_list_all_same:
  "list_all is_Equality (unlabel A) ⟹ duallsst A = A"
  "list_all is_Insert (unlabel A) ⟹ duallsst A = A"
  "list_all is_Delete (unlabel A) ⟹ duallsst A = A"
  "list_all is_InSet (unlabel A) ⟹ duallsst A = A"
  "list_all is_NegChecks (unlabel A) ⟹ duallsst A = A"
  "list_all is_Assignment (unlabel A) ⟹ duallsst A = A"
  "list_all is_Check (unlabel A) ⟹ duallsst A = A"
  "list_all is_Update (unlabel A) ⟹ duallsst A = A"
  "list_all is_Check_or_Assignment (unlabel A) ⟹ duallsst A = A"
proof (induct A)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  { case 1 thus ?case using Cons.hyps(1) a by (cases b) auto }
  { case 2 thus ?case using Cons.hyps(2) a by (cases b) auto }
  { case 3 thus ?case using Cons.hyps(3) a by (cases b) auto }
  { case 4 thus ?case using Cons.hyps(4) a by (cases b) auto }
  { case 5 thus ?case using Cons.hyps(5) a by (cases b) auto }
  { case 6 thus ?case using Cons.hyps(6) a by (cases b) auto }
  { case 7 thus ?case using Cons.hyps(7) a by (cases b) auto }
  { case 8 thus ?case using Cons.hyps(8) a by (cases b) auto }
  { case 9 thus ?case using Cons.hyps(9) a by (cases b) auto }
qed simp_all

lemma duallsst_in_set_prefix_obtain:
  assumes "s ∈ set (unlabel (duallsst A))"
  shows "∃l B s'. (l,s) = duallsstp (l,s') ∧ prefix (B@[(l,s')]) A"
  using assms
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  obtain i b where a: "a = (i,b)" by (metis surj_pair)
  show ?case using snoc
  proof (cases "s ∈ set (unlabel (duallsst A))")
    case False thus ?thesis
      using a snoc.prems unlabel_append[of "duallsst A" "duallsst [a]"] duallsst_append[of A "[a]"]
      by (cases b) (force simp add: unlabel_def duallsst_def)+
  qed auto
qed simp

lemma duallsst_in_set_prefix_obtain_subst:
  assumes "s ∈ set (unlabel (duallsst (A ⋅lsst θ)))"
  shows "∃l B s'. (l,s) = duallsstp ((l,s') ⋅lsstp θ) ∧ prefix ((B ⋅lsst θ)@[(l,s') ⋅lsstp θ]) (A ⋅lsst θ)"
proof -
  obtain B l s' where B: "(l,s) = duallsstp (l,s')" "prefix (B@[(l,s')]) (A ⋅lsst θ)"
    using duallsst_in_set_prefix_obtain[OF assms] by atomize_elim auto

  obtain C where C: "C ⋅lsst θ = B@[(l,s')]"
    using subst_lsst_prefix[OF B(2)] by atomize_elim auto

  obtain D u where D: "C = D@[(l,u)]" "D ⋅lsst θ = B" "[(l,u)] ⋅lsst θ = [(l, s')]"
    using subst_lsst_prefix[OF B(2)] subst_lsst_append_inv[OF C(1)]
    by (auto simp add: subst_apply_labeled_stateful_strand_def)

  show ?thesis 
    using B D subst_lsst_cons subst_lsst_singleton
    by (metis (no_types, lifting) nth_append_length)
qed

lemma trmssst_unlabel_duallsst_eq: "trmslsst (duallsst A) = trmslsst 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) auto
qed simp

lemma trmssst_unlabel_subst_cons:
  "trmslsst ((l,b)#A ⋅lsst δ) = trmssstp (b ⋅sstp δ) ∪ trmslsst (A ⋅lsst δ)"
by (metis subst_lsst_unlabel trmssst_subst_cons unlabel_Cons(1))

lemma trmssst_unlabel_subst:
  assumes "bvarslsst S ∩ subst_domain θ = {}"
  shows "trmslsst (S ⋅lsst θ) = trmslsst S ⋅set θ"
by (metis trmssst_subst[OF assms] subst_lsst_unlabel)

lemma trmssst_unlabel_subst':
  fixes t::"('a,'b) term" and δ::"('a,'b) subst"
  assumes "t ∈ trmslsst (S ⋅lsst δ)"
  shows "∃s ∈ trmslsst S. ∃X. set X ⊆ bvarslsst S ∧ t = s ⋅ rm_vars (set X) δ"
using assms
proof (induction S)
  case (Cons a S)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  hence "t ∈ trmslsst (S ⋅lsst δ) ∨ t ∈ trmssstp (b ⋅sstp δ)" 
    using Cons.prems trmssst_unlabel_subst_cons by fast
  thus ?case
  proof
    assume *: "t ∈ trmssstp (b ⋅sstp δ)"
    show ?thesis using trmssstp_subst''[OF *] a by auto
  next
    assume *: "t ∈ trmslsst (S ⋅lsst δ)"
    show ?thesis using Cons.IH[OF *] a by auto
  qed
qed simp

lemma trmssst_unlabel_subst'':
  fixes t::"('a,'b) term" and δ θ::"('a,'b) subst"
  assumes "t ∈ trmslsst (S ⋅lsst δ) ⋅set θ"
  shows "∃s ∈ trmslsst S. ∃X. set X ⊆ bvarslsst S ∧ t = s ⋅ rm_vars (set X) δ ∘s θ"
proof -
  obtain s where s: "s ∈ trmslsst (S ⋅lsst δ)" "t = s ⋅ θ" using assms by atomize_elim auto
  show ?thesis using trmssst_unlabel_subst'[OF s(1)] s(2) by auto
qed

lemma trmssst_unlabel_dual_subst_cons:
  "trmslsst (duallsst (a#A ⋅lsst σ)) = (trmssstp (snd a ⋅sstp σ)) ∪ (trmslsst (duallsst (A ⋅lsst σ)))"
proof -
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  thus ?thesis using a duallsst_subst_cons[of a A σ] by (cases b) auto
qed

lemma duallsst_funs_term:
  "⋃(funs_term ` (trmssst (unlabel (duallsst S)))) = ⋃(funs_term ` (trmssst (unlabel S)))"
using trmssst_unlabel_duallsst_eq by fast

lemma duallsst_dblsst:
  "db'lsst (duallsst A) = db'lsst A"
proof (induction A)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons by (cases b) auto
qed simp

lemma dbsst_unlabel_append:
  "db'lsst (A@B) I D = db'lsst B I (db'lsst A I D)"
by (metis dbsst_append unlabel_append)

lemma dbsst_duallsst:
  "db'sst (unlabel (duallsst (T ⋅lsst δ))) ℐ D = db'sst (unlabel (T ⋅lsst δ)) ℐ D"
proof (induction T arbitrary: D)
  case (Cons x T)
  obtain l s where "x = (l,s)" by atomize_elim auto
  thus ?case
    using Cons
    by (cases s) (simp_all add: unlabel_def duallsst_def subst_apply_labeled_stateful_strand_def)  
qed (simp add: unlabel_def duallsst_def subst_apply_labeled_stateful_strand_def)

lemma labeled_list_insert_eq_cases:
  "d ∉ set (unlabel D) ⟹ List.insert d (unlabel D) = unlabel (List.insert (i,d) D)"
  "(i,d) ∈ set D ⟹ List.insert d (unlabel D) = unlabel (List.insert (i,d) D)"
unfolding unlabel_def
by (metis (no_types, opaque_lifting) List.insert_def image_eqI list.simps(9) set_map snd_conv,
    metis in_set_insert set_zip_rightD zip_map_fst_snd)

lemma labeled_list_insert_eq_ex_cases:
  "List.insert d (unlabel D) = unlabel (List.insert (i,d) D) ∨
  (∃j. (j,d) ∈ set D ∧ List.insert d (unlabel D) = unlabel (List.insert (j,d) D))"
using labeled_list_insert_eq_cases unfolding unlabel_def
by (metis in_set_impl_in_set_zip2 length_map zip_map_fst_snd)

lemma in_proj_set:
  assumes "⟨l,r⟩ ∈ set A"
  shows "⟨l,r⟩ ∈ set (proj l A)"
using assms unfolding proj_def by force

lemma proj_subst: "proj l (A ⋅lsst δ) = proj l A ⋅lsst δ"
proof (induction A)
  case (Cons a A)
  obtain l b where "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons unfolding proj_def subst_apply_labeled_stateful_strand_def by force
qed simp 

lemma proj_set_subset[simp]:
  "set (proj n A) ⊆ set A"
unfolding proj_def by auto

lemma proj_proj_set_subset[simp]:
  "set (proj n (proj m A)) ⊆ set (proj n A)"
  "set (proj n (proj m A)) ⊆ set (proj m A)"
  "set (proj_unl n (proj m A)) ⊆ set (proj_unl n A)"
  "set (proj_unl n (proj m A)) ⊆ set (proj_unl m A)"
unfolding unlabel_def proj_def by auto

lemma proj_mem_iff:
  "(ln i, d) ∈ set D ⟷ (ln i, d) ∈ set (proj i D)"
  "(⋆, d) ∈ set D ⟷ (⋆, d) ∈ set (proj i D)"
unfolding proj_def by auto

lemma proj_list_insert:
  "proj i (List.insert (ln i,d) D) = List.insert (ln i,d) (proj i D)"
  "proj i (List.insert (⋆,d) D) = List.insert (⋆,d) (proj i D)"
  "i ≠ j ⟹ proj i (List.insert (ln j,d) D) = proj i D"
unfolding List.insert_def proj_def by auto

lemma proj_filter: "proj i [d←D. d ∉ set Di] = [d←proj i D. d ∉ set Di]"
by (simp_all add: proj_def conj_commute)

lemma proj_list_Cons:
  "proj i ((ln i,d)#D) = (ln i,d)#proj i D"
  "proj i ((⋆,d)#D) = (⋆,d)#proj i D"
  "i ≠ j ⟹ proj i ((ln j,d)#D) = proj i D"
unfolding List.insert_def proj_def by auto

lemma proj_duallsst:
  "proj l (duallsst A) = duallsst (proj l A)"
proof (induction A)
  case (Cons a A)
  obtain k b where "a = (k,b)" by (metis surj_pair)
  thus ?case using Cons unfolding duallsst_def proj_def by (cases b) auto
qed simp

lemma proj_instance_ex:
  assumes B: "∀b ∈ set B. ∃a ∈ set A. ∃δ. b = a ⋅lsstp δ ∧ P δ"
    and b: "b ∈ set (proj l B)"
  shows "∃a ∈ set (proj l A). ∃δ. b = a ⋅lsstp δ ∧ P δ"
proof -
  obtain a δ where a: "a ∈ set A" "b = a ⋅lsstp δ" "P δ" using B b proj_set_subset by fast
  obtain k b' where b': "b = (k, b')" "k = (ln l) ∨ k = ⋆" using b proj_in_setD by metis
  obtain a' where a': "a = (k, a')" using b'(1) a(2) by (cases a) simp_all
  show ?thesis using a a' b'(2) unfolding proj_def by auto
qed

lemma proj_dbproj:
  "dbproj (ln i) (proj i D) = dbproj (ln i) D"
  "dbproj ⋆ (proj i D) = dbproj ⋆ D"
  "i ≠ j ⟹ dbproj (ln j) (proj i D) = []"
unfolding proj_def dbproj_def by (induct D) auto

lemma dbproj_Cons:
  "dbproj i ((i,d)#D) = (i,d)#dbproj i D"
  "i ≠ j ⟹ dbproj j ((i,d)#D) = dbproj j D"
unfolding dbproj_def by auto

lemma dbproj_subset[simp]:
  "set (unlabel (dbproj i D)) ⊆ set (unlabel D)"
unfolding unlabel_def dbproj_def by auto

lemma dbproj_subseq: 
  assumes "Di ∈ set (subseqs (dbproj k D))"
  shows "dbproj k Di = Di" (is ?A)
  and "i ≠ k ⟹ dbproj i Di = []" (is "i ≠ k ⟹ ?B")
proof -
  have *: "set Di ⊆ set (dbproj k D)" using subseqs_powset[of "dbproj k D"] assms by auto
  thus ?A by (metis dbproj_def filter_True filter_set member_filter subsetCE)

  have "⋀j d. (j,d) ∈ set Di ⟹ j = k" using * unfolding dbproj_def by auto
  moreover have "⋀j d. (j,d) ∈ set (dbproj i Di) ⟹ j = i" unfolding dbproj_def by auto
  moreover have "⋀j d. (j,d) ∈ set (dbproj i Di) ⟹ (j,d) ∈ set Di" unfolding dbproj_def by auto
  ultimately show "i ≠ k ⟹ ?B" by (metis set_empty subrelI subset_empty)
qed

lemma dbproj_subseq_subset:
  assumes "Di ∈ set (subseqs (dbproj i D))"
  shows "set Di ⊆ set D"
using assms unfolding dbproj_def 
by (metis Pow_iff filter_set image_eqI member_filter subseqs_powset subsetCE subsetI)

lemma dbproj_subseq_in_subseqs:
  assumes "Di ∈ set (subseqs (dbproj i D))"
  shows "Di ∈ set (subseqs D)"
using assms in_set_subseqs subseq_filter_left subseq_order.dual_order.trans
unfolding dbproj_def by blast

lemma proj_subseq:
  assumes "Di ∈ set (subseqs (dbproj (ln j) D))" "j ≠ i"
  shows "[d←proj i D. d ∉ set Di] = proj i D"
proof -
  have "set Di ⊆ set (dbproj (ln j) D)" using subseqs_powset[of "dbproj (ln j) D"] assms by auto
  hence "⋀k d. (k,d) ∈ set Di ⟹ k = ln j" unfolding dbproj_def by auto
  moreover have "⋀k d. (k,d) ∈ set (proj i D) ⟹ k ≠ ln j"
    using assms(2) unfolding proj_def by auto
  ultimately have "⋀d. d ∈ set (proj i D) ⟹ d ∉ set Di" by auto
  thus ?thesis by simp
qed

lemma unlabel_subseqsD:
  assumes "A ∈ set (subseqs (unlabel B))"
  shows "∃C ∈ set (subseqs B). unlabel C = A"
using assms map_subseqs unfolding unlabel_def by (metis imageE set_map) 

lemma unlabel_filter_eq:
  assumes "∀(j, p) ∈ set A ∪ B. ∀(k, q) ∈ set A ∪ B. p = q ⟶ j = k" (is "?P (set A)")
  shows "[d←unlabel A. d ∉ snd ` B] = unlabel [d←A. d ∉ B]"
using assms unfolding unlabel_def
proof (induction A)
  case (Cons a A)
  have "set A ⊆ set (a#A)" "{a} ⊆ set (a#A)" by auto
  hence *: "?P (set A)" "?P {a}" using Cons.prems by fast+
  hence IH: "[d←map snd A . d ∉ snd ` B] = map snd [d←A . d ∉ B]" using Cons.IH by auto

  { assume "snd a ∈ snd ` B"
    then obtain b where b: "b ∈ B" "snd a = snd b" by atomize_elim auto
    hence "fst a = fst b" using *(2) by auto
    hence "a ∈ B" using b by (metis surjective_pairing)  
  } hence **: "a ∉ B ⟹ snd a ∉ snd ` B" by metis

  show ?case by (cases "a ∈ B") (simp add: ** IH)+ 
qed simp

lemma subseqs_mem_dbproj:
  assumes "Di ∈ set (subseqs D)" "list_all (λd. fst d = i) Di"
  shows "Di ∈ set (subseqs (dbproj i D))"
using assms
proof (induction D arbitrary: Di)
  case (Cons di D)
  obtain d j where di: "di = (j,d)" by (metis surj_pair)
  show ?case
  proof (cases "Di ∈ set (subseqs D)")
    case True
    hence "Di ∈ set (subseqs (dbproj i D))" using Cons.IH Cons.prems by auto
    thus ?thesis using subseqs_Cons unfolding dbproj_def by auto
  next
    case False
    then obtain Di' where Di': "Di = di#Di'" using Cons.prems(1)
      by (metis (mono_tags, lifting) Un_iff imageE set_append set_map subseqs.simps(2)) 
    hence "Di' ∈ set (subseqs D)" using Cons.prems(1) False
      by (metis (no_types, lifting) UnE imageE list.inject set_append set_map subseqs.simps(2)) 
    hence "Di' ∈ set (subseqs (dbproj i D))" using Cons.IH Cons.prems Di' by auto
    moreover have "i = j" using Di' di Cons.prems(2) by auto
    hence "dbproj i (di#D) = di#dbproj i D" unfolding dbproj_def by (simp add: di)
    ultimately show ?thesis using Di'
      by (metis (no_types, lifting) UnCI image_eqI set_append set_map subseqs.simps(2)) 
  qed
qed simp

lemma unlabel_subst: "unlabel S ⋅sst δ = unlabel (S ⋅lsst δ)"
unfolding unlabel_def subst_apply_stateful_strand_def subst_apply_labeled_stateful_strand_def 
by auto

lemma subterms_subst_lsst:
  assumes "∀x ∈ fvset (trmslsst S). (∃f. σ x = Fun f []) ∨ (∃y. σ x = Var y)"
    and "bvarslsst S ∩ subst_domain σ = {}"
  shows "subtermsset (trmslsst (S ⋅lsst σ)) = subtermsset (trmslsst S) ⋅set σ"
using subterms_subst''[OF assms(1)] trmssst_subst[OF assms(2)] unlabel_subst[of S σ]
by simp

lemma subterms_subst_lsst_ik:
  assumes "∀x ∈ fvset (iklsst S). (∃f. σ x = Fun f []) ∨ (∃y. σ x = Var y)"
  shows "subtermsset (iklsst (S ⋅lsst σ)) = subtermsset (iklsst S) ⋅set σ"
using subterms_subst''[OF assms(1)] iksst_subst[of "unlabel S" σ] unlabel_subst[of S σ]
by simp

lemma labeled_stateful_strand_subst_comp:
  assumes "range_vars δ ∩ bvarslsst S = {}"
  shows "S ⋅lsst δ ∘s θ = (S ⋅lsst δ) ⋅lsst θ"
using assms
proof (induction S)
  case (Cons s S)
  obtain l x where s: "s = (l,x)" by (metis surj_pair)
  hence IH: "S ⋅lsst δ ∘s θ = (S ⋅lsst δ) ⋅lsst θ" using Cons by auto

  have "x ⋅sstp δ ∘s θ = (x ⋅sstp δ) ⋅sstp θ"
    using s Cons.prems stateful_strand_step_subst_comp[of δ x θ] by auto
  thus ?case using s IH by (simp add: subst_apply_labeled_stateful_strand_def)
qed simp

lemma sst_vars_proj_subset[simp]:
  "fvsst (proj_unl n A) ⊆ fvsst (unlabel A)"
  "bvarssst (proj_unl n A) ⊆ bvarssst (unlabel A)"
  "varssst (proj_unl n A) ⊆ varssst (unlabel A)"
using varssst_is_fvsst_bvarssst[of "unlabel A"]
      varssst_is_fvsst_bvarssst[of "proj_unl n A"]
unfolding unlabel_def proj_def by auto

lemma trmssst_proj_subset[simp]:
  "trmssst (proj_unl n A) ⊆ trmssst (unlabel A)" (is ?A)
  "trmssst (proj_unl m (proj n A)) ⊆ trmssst (proj_unl n A)" (is ?B)
  "trmssst (proj_unl m (proj n A)) ⊆ trmssst (proj_unl m A)" (is ?C)
proof -
  show ?A unfolding unlabel_def proj_def by auto
  show ?B using trmssst_mono[OF proj_proj_set_subset(4)] by metis
  show ?C using trmssst_mono[OF proj_proj_set_subset(3)] by metis
qed

lemma trmssst_unlabel_prefix_subset:
  "trmssst (unlabel A) ⊆ trmssst (unlabel (A@B))" (is ?A)
  "trmssst (proj_unl n A) ⊆ trmssst (proj_unl n (A@B))" (is ?B)
using trmssst_mono[of "proj_unl n A" "proj_unl n (A@B)"]
unfolding unlabel_def proj_def by auto

lemma trmssst_unlabel_suffix_subset:
  "trmssst (unlabel B) ⊆ trmssst (unlabel (A@B))"
  "trmssst (proj_unl n B) ⊆ trmssst (proj_unl n (A@B))"
using trmssst_mono[of "proj_unl n B" "proj_unl n (A@B)"]
unfolding unlabel_def proj_def by auto

lemma setopslsstpD:
  assumes p: "p ∈ setopslsstp a"
  shows "fst p = fst a" (is ?P)
    and "is_Update (snd a) ∨ is_InSet (snd a) ∨ is_NegChecks (snd a)" (is ?Q)
proof -
  obtain l k p' a' where a: "p = (l,p')" "a = (k,a')" by (metis surj_pair)
  show ?P using p a by (cases a') auto
  show ?Q using p a by (cases a') auto
qed

lemma setopslsst_nil[simp]:
  "setopslsst [] = {}"
by (simp add: setopslsst_def)

lemma setopslsst_cons[simp]:
  "setopslsst (x#S) = setopslsstp x ∪ setopslsst S"
by (simp add: setopslsst_def)

lemma setopssst_proj_subset:
  "setopssst (proj_unl n A) ⊆ setopssst (unlabel A)"
  "setopssst (proj_unl m (proj n A)) ⊆ setopssst (proj_unl n A)"
  "setopssst (proj_unl m (proj n A)) ⊆ setopssst (proj_unl m A)"
unfolding unlabel_def proj_def
proof (induction A)
  case (Cons a A)
  obtain l b where lb: "a = (l,b)" by atomize_elim auto
  { case 1 thus ?case using Cons.IH(1) unfolding lb by (cases b) (auto simp add: setopssst_def) }
  { case 2 thus ?case using Cons.IH(2) unfolding lb by (cases b) (auto simp add: setopssst_def) }
  { case 3 thus ?case using Cons.IH(3) unfolding lb by (cases b) (auto simp add: setopssst_def) }
qed simp_all

lemma setopssst_unlabel_prefix_subset:
  "setopssst (unlabel A) ⊆ setopssst (unlabel (A@B))"
  "setopssst (proj_unl n A) ⊆ setopssst (proj_unl n (A@B))"
unfolding unlabel_def proj_def
proof (induction A)
  case (Cons a A)
  obtain l b where lb: "a = (l,b)" by atomize_elim auto
  { case 1 thus ?case using Cons.IH lb by (cases b) (auto simp add: setopssst_def) }
  { case 2 thus ?case using Cons.IH lb by (cases b) (auto simp add: setopssst_def) }
qed (simp_all add: setopssst_def)

lemma setopssst_unlabel_suffix_subset:
  "setopssst (unlabel B) ⊆ setopssst (unlabel (A@B))"
  "setopssst (proj_unl n B) ⊆ setopssst (proj_unl n (A@B))"
unfolding unlabel_def proj_def
proof (induction A)
  case (Cons a A)
  obtain l b where lb: "a = (l,b)" by atomize_elim auto
  { case 1 thus ?case using Cons.IH lb by (cases b) (auto simp add: setopssst_def) }
  { case 2 thus ?case using Cons.IH lb by (cases b) (auto simp add: setopssst_def) }
qed simp_all

lemma setopslsst_proj_subset:
  "setopslsst (proj n A) ⊆ setopslsst A"
  "setopslsst (proj m (proj n A)) ⊆ setopslsst (proj n A)"
unfolding proj_def setopslsst_def by auto

lemma setopslsst_prefix_subset:
  "setopslsst A ⊆ setopslsst (A@B)"
  "setopslsst (proj n A) ⊆ setopslsst (proj n (A@B))"
unfolding proj_def setopslsst_def by auto

lemma setopslsst_suffix_subset:
  "setopslsst B ⊆ setopslsst (A@B)"
  "setopslsst (proj n B) ⊆ setopslsst (proj n (A@B))"
unfolding proj_def setopslsst_def by auto

lemma setopslsst_mono:
  "set M ⊆ set N ⟹ setopslsst M ⊆ setopslsst N"
by (auto simp add: setopslsst_def)

lemma trmssst_unlabel_subset_if_no_label:
  "¬list_ex (has_LabelN l) A ⟹ trmslsst (proj l A) ⊆ trmslsst (proj l' A)"
by (rule trmssst_mono[OF proj_subset_if_no_label(2)[of l A l']])

lemma setopssst_unlabel_subset_if_no_label:
  "¬list_ex (has_LabelN l) A ⟹ setopssst (proj_unl l A) ⊆ setopssst (proj_unl l' A)"
by (rule setopssst_mono[OF proj_subset_if_no_label(2)[of l A l']])

lemma setopslsst_proj_subset_if_no_label:
  "¬list_ex (has_LabelN l) A ⟹ setopslsst (proj l A) ⊆ setopslsst (proj l' A)"
by (rule setopslsst_mono[OF proj_subset_if_no_label(1)[of l A l']])

lemma setopslsstp_subst_cases[simp]:
  "setopslsstp ((l,send⟨ts⟩) ⋅lsstp δ) = {}"
  "setopslsstp ((l,receive⟨ts⟩) ⋅lsstp δ) = {}"
  "setopslsstp ((l,⟨ac: s ≐ t⟩) ⋅lsstp δ) = {}"
  "setopslsstp ((l,insert⟨t,s⟩) ⋅lsstp δ) = {(l,t ⋅ δ,s ⋅ δ)}"
  "setopslsstp ((l,delete⟨t,s⟩) ⋅lsstp δ) = {(l,t ⋅ δ,s ⋅ δ)}"
  "setopslsstp ((l,⟨ac: t ∈ s⟩) ⋅lsstp δ) = {(l,t ⋅ δ,s ⋅ δ)}"
  "setopslsstp ((l,∀X⟨∨≠: F ∨∉: F'⟩) ⋅lsstp δ) =
    ((λ(t,s). (l,t ⋅ rm_vars (set X) δ,s ⋅ rm_vars (set X) δ)) ` set F')" (is "?A = ?B")
proof -
  have "?A = (λ(t,s). (l,t,s)) ` set (F' ⋅pairs rm_vars (set X) δ)" by auto
  thus "?A = ?B" unfolding subst_apply_pairs_def by auto
qed simp_all

lemma setopslsstp_subst:
  assumes "set (bvarssstp (snd a)) ∩ subst_domain θ = {}"
  shows "setopslsstp (a ⋅lsstp θ) = (λp. (fst a,snd p ⋅p θ)) ` setopslsstp a"
proof -
  obtain l a' where a: "a = (l,a')" by (metis surj_pair)
  show ?thesis
  proof (cases a')
    case (NegChecks X F G)
    hence *: "rm_vars (set X) θ = θ" using a assms rm_vars_apply'[of θ "set X"] by auto
    have "setopslsstp (a ⋅lsstp θ) = (λp. (fst a, p)) ` set (G ⋅pairs θ)"
      using * NegChecks a  by auto
    moreover have "setopslsstp a = (λp. (fst a, p)) ` set G" using NegChecks a by simp
    hence "(λp. (fst a,snd p ⋅p θ)) ` setopslsstp a = (λp. (fst a, p ⋅p θ)) ` set G"
      by (metis (mono_tags, lifting) image_cong image_image snd_conv)
    hence "(λp. (fst a,snd p ⋅p θ)) ` setopslsstp a = (λp. (fst a, p)) ` (set G ⋅pset θ)"
      unfolding case_prod_unfold by auto
    ultimately show ?thesis by (simp add: subst_apply_pairs_def) 
  qed (use a in simp_all)
qed

lemma setopslsstp_subst':
  assumes "set (bvarssstp (snd a)) ∩ subst_domain θ = {}"
  shows "setopslsstp (a ⋅lsstp θ) = (λ(i,p). (i,p ⋅p θ)) ` setopslsstp a"
using setopslsstp_subst[OF assms] setopslsstpD(1) unfolding case_prod_unfold
by (metis (mono_tags, lifting) image_cong)

lemma setopslsst_subst:
  assumes "bvarslsst S ∩ subst_domain θ = {}"
  shows "setopslsst (S ⋅lsst θ) = (λp. (fst p,snd p ⋅p θ)) ` setopslsst S"
using assms
proof (induction S)
  case (Cons a S)
  have "bvarslsst S ∩ subst_domain θ = {}" and *: "set (bvarssstp (snd a)) ∩ subst_domain θ = {}"
    using Cons.prems by auto
  hence IH: "setopslsst (S ⋅lsst θ) = (λp. (fst p,snd p ⋅p θ)) ` setopslsst S"
    using Cons.IH by auto
  show ?case
    using setopslsstp_subst'[OF *] IH
    unfolding setopslsst_def case_prod_unfold subst_lsst_cons 
    by auto
qed (simp add: setopssst_def)

lemma setopslsstp_in_subst:
  assumes p: "p ∈ setopslsstp (a ⋅lsstp δ)"
  shows "∃q ∈ setopslsstp a. fst p = fst q ∧ snd p = snd q ⋅p rm_vars (set (bvarssstp (snd a))) δ"
    (is "∃q ∈ setopslsstp a. ?P q")
proof -
  obtain l b where a: "a = (l,b)" by (metis surj_pair)

  show ?thesis
  proof (cases b)
    case (NegChecks X F F')
    hence "p ∈ (λ(t, s). (l, t ⋅ rm_vars (set X) δ, s ⋅ rm_vars (set X) δ)) ` set F'"
      using p a setopslsstp_subst_cases(7)[of l X F F' δ] by blast
    then obtain s t where st:
        "(t,s) ∈ set F'" "p = (l, t ⋅ rm_vars (set X) δ, s ⋅ rm_vars (set X) δ)"
      by auto
    hence "(l,t,s) ∈ setopslsstp a" "fst p = fst (l,t,s)"
          "snd p = snd (l,t,s) ⋅p rm_vars (set X) δ"
      using a NegChecks by fastforce+
    moreover have "bvarssstp (snd a) = X" using NegChecks a by auto
    ultimately show ?thesis by blast
  qed (use p a in auto)
qed

lemma setopslsst_in_subst:
  assumes "p ∈ setopslsst (A ⋅lsst δ)"
  shows "∃q ∈ setopslsst A. fst p = fst q ∧ (∃X ⊆ bvarslsst A. snd p = snd q ⋅p rm_vars X δ)"
    (is "∃q ∈ setopslsst A. ?P A q")
  using assms
proof (induction A)
  case (Cons a A)
  note 0 = unlabel_Cons(2)[of a A] bvarssst_Cons[of "snd a" "unlabel A"]
  show ?case
  proof (cases "p ∈ setopslsst (A ⋅lsst δ)")
    case False
    hence "p ∈ setopslsstp (a ⋅lsstp δ)"
      using Cons.prems setopslsst_cons[of "a ⋅lsstp δ" "A ⋅lsst δ"] subst_lsst_cons[of a A δ] by auto
    moreover have "(set (bvarssstp (snd a))) ⊆ bvarslsst (a#A)" using 0 by simp
    ultimately have "∃q ∈ setopslsstp a. ?P (a#A) q" using setopslsstp_in_subst[of p a δ] by blast
    thus ?thesis by auto
  qed (use Cons.IH 0 in auto)
qed simp

lemma setopslsst_duallsst_eq:
  "setopslsst (duallsst A) = setopslsst A"
proof (induction A)
  case (Cons a A)
  obtain l b where "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons unfolding setopslsst_def duallsst_def by (cases b) auto
qed simp

end