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 [dD. d  set Di] = [dproj 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 "[dproj 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 "[dunlabel A. d  snd ` B] = unlabel [dA. 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: "[dmap snd A . d  snd ` B] = map snd [dA . 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