Theory Stateful_Strands

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


section ‹Stateful Strands›
theory Stateful_Strands
imports Strands_and_Constraints
begin

subsection ‹Stateful Constraints›
datatype (funssstp: 'a, varssstp: 'b) stateful_strand_step = 
  Send (the_msgs: "('a,'b) term list") (‹send⟨_⟩› 80)
| Receive (the_msgs: "('a,'b) term list") (‹receive⟨_⟩› 80)
| Equality (the_check: poscheckvariant) (the_lhs: "('a,'b) term") (the_rhs: "('a,'b) term")
    (‹⟨_: _ ≐ _⟩› [80,80])
| Insert (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") (‹insert⟨_,_⟩› 80)
| Delete (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") (‹delete⟨_,_⟩› 80)
| InSet (the_check: poscheckvariant) (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term")
    (‹⟨_: _ ∈ _⟩› [80,80])
| NegChecks (bvarssstp: "'b list")
    (the_eqs: "(('a,'b) term × ('a,'b) term) list")
    (the_ins: "(('a,'b) term × ('a,'b) term) list")
    (‹∀_⟨∨≠: _ ∨∉: _⟩› [80,80])
where
  "bvarssstp (Send _) = []"
| "bvarssstp (Receive _) = []"
| "bvarssstp (Equality _ _ _) = []"
| "bvarssstp (Insert _ _) = []"
| "bvarssstp (Delete _ _) = []"
| "bvarssstp (InSet _ _ _) = []"

type_synonym ('a,'b) stateful_strand = "('a,'b) stateful_strand_step list"
type_synonym ('a,'b) dbstatelist = "(('a,'b) term × ('a,'b) term) list"
type_synonym ('a,'b) dbstate = "(('a,'b) term × ('a,'b) term) set"

abbreviation
  "is_Assignment x ≡ (is_Equality x ∨ is_InSet x) ∧ the_check x = Assign"

abbreviation
  "is_Check x ≡ ((is_Equality x ∨ is_InSet x) ∧ the_check x = Check) ∨ is_NegChecks x"

abbreviation
  "is_Check_or_Assignment x ≡ is_Equality x ∨ is_InSet x ∨ is_NegChecks x"

abbreviation
  "is_Update x ≡ is_Insert x ∨ is_Delete x"

abbreviation InSet_select (‹select⟨_,_⟩›) where "select⟨t,s⟩ ≡ InSet Assign t s"
abbreviation InSet_check (‹⟨_ in _⟩›) where "⟨t in s⟩ ≡ InSet Check t s"
abbreviation Equality_assign (‹⟨_ := _⟩›) where "⟨t := s⟩ ≡ Equality Assign t s"
abbreviation Equality_check (‹⟨_ == _⟩›) where "⟨t == s⟩ ≡ Equality Check t s"

abbreviation NegChecks_Inequality1 (‹⟨_ != _⟩›) where
  "⟨t != s⟩ ≡ NegChecks [] [(t,s)] []"

abbreviation NegChecks_Inequality2 (‹∀_⟨_ != _⟩›) where
  "∀x⟨t != s⟩ ≡ NegChecks [x] [(t,s)] []"

abbreviation NegChecks_Inequality3 (‹∀_,_⟨_ != _⟩›) where
  "∀x,y⟨t != s⟩ ≡ NegChecks [x,y] [(t,s)] []"

abbreviation NegChecks_Inequality4 (‹∀_,_,_⟨_ != _⟩›) where
  "∀x,y,z⟨t != s⟩ ≡ NegChecks [x,y,z] [(t,s)] []"

abbreviation NegChecks_NotInSet1 (‹⟨_ not in _⟩›) where
  "⟨t not in s⟩ ≡ NegChecks [] [] [(t,s)]"

abbreviation NegChecks_NotInSet2 (‹∀_⟨_ not in _⟩›) where
  "∀x⟨t not in s⟩ ≡ NegChecks [x] [] [(t,s)]"

abbreviation NegChecks_NotInSet3 (‹∀_,_⟨_ not in _⟩›) where
  "∀x,y⟨t not in s⟩ ≡ NegChecks [x,y] [] [(t,s)]"

abbreviation NegChecks_NotInSet4 (‹∀_,_,_⟨_ not in _⟩›) where
  "∀x,y,z⟨t not in s⟩ ≡ NegChecks [x,y,z] [] [(t,s)]"

fun trmssstp where
  "trmssstp (Send ts) = set ts"
| "trmssstp (Receive ts) = set ts"
| "trmssstp (Equality _ t t') = {t,t'}"
| "trmssstp (Insert t t') = {t,t'}"
| "trmssstp (Delete t t') = {t,t'}"
| "trmssstp (InSet _ t t') = {t,t'}"
| "trmssstp (NegChecks _ F F') = trmspairs F ∪ trmspairs F'"

definition trmssst where "trmssst S ≡ ⋃(trmssstp ` set S)"
declare trmssst_def[simp]

fun trms_listsstp where
  "trms_listsstp (Send ts) = ts"
| "trms_listsstp (Receive ts) = ts"
| "trms_listsstp (Equality _ t t') = [t,t']"
| "trms_listsstp (Insert t t') = [t,t']"
| "trms_listsstp (Delete t t') = [t,t']"
| "trms_listsstp (InSet _ t t') = [t,t']"
| "trms_listsstp (NegChecks _ F F') = concat (map (λ(t,t'). [t,t']) (F@F'))"

definition trms_listsst where "trms_listsst S ≡ remdups (concat (map trms_listsstp S))"

definition iksst where "iksst A ≡ {t | t ts. Receive ts ∈ set A ∧ t ∈ set ts}"

definition bvarssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "bvarssst S ≡ ⋃(set (map (set ∘ bvarssstp) S))"

fun fvsstp::"('a,'b) stateful_strand_step ⇒ 'b set" where
  "fvsstp (Send ts) = fvset (set ts)"
| "fvsstp (Receive ts) = fvset (set ts)"
| "fvsstp (Equality _ t t') = fv t ∪ fv t'"
| "fvsstp (Insert t t') = fv t ∪ fv t'"
| "fvsstp (Delete t t') = fv t ∪ fv t'"
| "fvsstp (InSet _ t t') = fv t ∪ fv t'"
| "fvsstp (NegChecks X F F') = fvpairs F ∪ fvpairs F' - set X"

definition fvsst::"('a,'b) stateful_strand ⇒ 'b set" where
  "fvsst S ≡ ⋃(set (map fvsstp S))"

fun fv_listsstp where
  "fv_listsstp (send⟨ts⟩) = concat (map fv_list ts)"
| "fv_listsstp (receive⟨ts⟩) = concat (map fv_list ts)"
| "fv_listsstp (⟨_: t ≐ s⟩) = fv_list t@fv_list s"
| "fv_listsstp (insert⟨t,s⟩) = fv_list t@fv_list s"
| "fv_listsstp (delete⟨t,s⟩) = fv_list t@fv_list s"
| "fv_listsstp (⟨_: t ∈ s⟩) = fv_list t@fv_list s"
| "fv_listsstp (∀X⟨∨≠: F ∨∉: F'⟩) = filter (λx. x ∉ set X) (fv_listpairs (F@F'))"

definition fv_listsst where
  "fv_listsst S ≡ remdups (concat (map fv_listsstp S))"

declare bvarssst_def[simp]
declare fvsst_def[simp]

definition varssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "varssst S ≡ ⋃(set (map varssstp S))"

abbreviation wfrestrictedvarssstp::"('a,'b) stateful_strand_step ⇒ 'b set" where
  "wfrestrictedvarssstp x ≡
    case x of
      NegChecks _ _ _ ⇒ {}
    | Equality Check _ _ ⇒ {}
    | InSet Check _ _ ⇒ {}
    | Delete _ _ ⇒ {}
    | _ ⇒ varssstp x"

definition wfrestrictedvarssst::"('a,'b) stateful_strand ⇒ 'b set" where
  "wfrestrictedvarssst S ≡ ⋃(set (map wfrestrictedvarssstp S))"

abbreviation wfvarsoccssstp where
  "wfvarsoccssstp x ≡ 
    case x of
      Send ts ⇒ fvset (set ts)
    | Equality Assign s t ⇒ fv s
    | InSet Assign s t ⇒ fv s ∪ fv t
    | _ ⇒ {}"

definition wfvarsoccssst where
  "wfvarsoccssst S ≡ ⋃(set (map wfvarsoccssstp S))"

fun wf'sst::"'b set ⇒ ('a,'b) stateful_strand ⇒ bool" where
  "wf'sst V [] = True"
| "wf'sst V (Receive ts#S) = (fvset (set ts) ⊆ V ∧ wf'sst V S)"
| "wf'sst V (Send ts#S) = wf'sst (V ∪ fvset (set ts)) S"
| "wf'sst V (Equality Assign t t'#S) = (fv t' ⊆ V ∧ wf'sst (V ∪ fv t) S)"
| "wf'sst V (Equality Check _ _#S) = wf'sst V S"
| "wf'sst V (Insert t s#S) = (fv t ⊆ V ∧ fv s ⊆ V ∧ wf'sst V S)"
| "wf'sst V (Delete _ _#S) = wf'sst V S"
| "wf'sst V (InSet Assign t s#S) = wf'sst (V ∪ fv t ∪ fv s) S"
| "wf'sst V (InSet Check _ _#S) = wf'sst V S"
| "wf'sst V (NegChecks _ _ _#S) = wf'sst V S"

abbreviation "wfsst S ≡ wf'sst {} S ∧ fvsst S ∩ bvarssst S = {}"

fun subst_apply_stateful_strand_step::
  "('a,'b) stateful_strand_step ⇒ ('a,'b) subst ⇒ ('a,'b) stateful_strand_step"
  (infix ‹⋅sstp› 51) where
  "send⟨ts⟩ ⋅sstp θ = send⟨ts ⋅list θ⟩"
| "receive⟨ts⟩ ⋅sstp θ = receive⟨ts ⋅list θ⟩"
| "⟨a: t ≐ s⟩ ⋅sstp θ = ⟨a: (t ⋅ θ) ≐ (s ⋅ θ)⟩"
| "⟨a: t ∈ s⟩ ⋅sstp θ = ⟨a: (t ⋅ θ) ∈ (s ⋅ θ)⟩"
| "insert⟨t,s⟩ ⋅sstp θ = insert⟨t ⋅ θ, s ⋅ θ⟩"
| "delete⟨t,s⟩ ⋅sstp θ = delete⟨t ⋅ θ, s ⋅ θ⟩"
| "∀X⟨∨≠: F ∨∉: G⟩ ⋅sstp θ = ∀X⟨∨≠: (F ⋅pairs rm_vars (set X) θ) ∨∉: (G ⋅pairs rm_vars (set X) θ)⟩"

definition subst_apply_stateful_strand::
  "('a,'b) stateful_strand ⇒ ('a,'b) subst ⇒ ('a,'b) stateful_strand"
  (infix ‹⋅sst› 51) where
  "S ⋅sst θ ≡ map (λx. x ⋅sstp θ) S"

fun dbupdsst::"('f,'v) stateful_strand ⇒ ('f,'v) subst ⇒ ('f,'v) dbstate ⇒ ('f,'v) dbstate"
where
  "dbupdsst [] I D = D"
| "dbupdsst (Insert t s#A) I D = dbupdsst A I (insert ((t,s) ⋅p I) D)"
| "dbupdsst (Delete t s#A) I D = dbupdsst A I (D - {((t,s) ⋅p I)})"
| "dbupdsst (_#A) I D = dbupdsst A I D"

fun db'sst::"('f,'v) stateful_strand ⇒ ('f,'v) subst ⇒ ('f,'v) dbstatelist ⇒ ('f,'v) dbstatelist"
where
  "db'sst [] I D = D"
| "db'sst (Insert t s#A) I D = db'sst A I (List.insert ((t,s) ⋅p I) D)"
| "db'sst (Delete t s#A) I D = db'sst A I (List.removeAll ((t,s) ⋅p I) D)"
| "db'sst (_#A) I D = db'sst A I D"

definition dbsst where
  "dbsst S I ≡ db'sst S I []"

fun setopssstp where
  "setopssstp (Insert t s) = {(t,s)}"
| "setopssstp (Delete t s) = {(t,s)}"
| "setopssstp (InSet _ t s) = {(t,s)}"
| "setopssstp (NegChecks _ _ F') = set F'"
| "setopssstp _ = {}"

text ‹The set-operations of a stateful strand›
definition setopssst where
  "setopssst S ≡ ⋃(setopssstp ` set S)"

fun setops_listsstp where
  "setops_listsstp (Insert t s) = [(t,s)]"
| "setops_listsstp (Delete t s) = [(t,s)]"
| "setops_listsstp (InSet _ t s) = [(t,s)]"
| "setops_listsstp (NegChecks _ _ F') = F'"
| "setops_listsstp _ = []"

text ‹The set-operations of a stateful strand (list variant)›
definition setops_listsst where
  "setops_listsst S ≡ remdups (concat (map setops_listsstp S))"


subsection ‹Small Lemmata›
lemma is_Check_or_Assignment_iff[simp]:
  "is_Check x ∨ is_Assignment x ⟷ is_Check_or_Assignment x"
by (cases x) (blast intro: poscheckvariant.exhaust)+

lemma subst_apply_stateful_strand_step_Inequality[simp]:
  "⟨t != s⟩ ⋅sstp θ = ⟨t ⋅ θ != s ⋅ θ⟩"
  "∀x⟨t != s⟩ ⋅sstp θ = ∀x⟨t ⋅ rm_vars {x} θ != s ⋅ rm_vars {x} θ⟩"
  "∀x,y⟨t != s⟩ ⋅sstp θ = ∀x,y⟨t ⋅ rm_vars {x,y} θ != s ⋅ rm_vars {x,y} θ⟩"
  "∀x,y,z⟨t != s⟩ ⋅sstp θ = ∀x,y,z⟨t ⋅ rm_vars {x,y,z} θ != s ⋅ rm_vars {x,y,z} θ⟩"
by simp_all

lemma subst_apply_stateful_strand_step_NotInSet[simp]:
  "⟨t not in s⟩ ⋅sstp θ = ⟨t ⋅ θ not in s ⋅ θ⟩"
  "∀x⟨t not in s⟩ ⋅sstp θ = ∀x⟨t ⋅ rm_vars {x} θ not in s ⋅ rm_vars {x} θ⟩"
  "∀x,y⟨t not in s⟩ ⋅sstp θ = ∀x,y⟨t ⋅ rm_vars {x,y} θ not in s ⋅ rm_vars {x,y} θ⟩"
  "∀x,y,z⟨t not in s⟩ ⋅sstp θ = ∀x,y,z⟨t ⋅ rm_vars {x,y,z} θ not in s ⋅ rm_vars {x,y,z} θ⟩"
by simp_all

lemma trms_listsst_is_trmssst: "trmssst S = set (trms_listsst S)"
unfolding trmsst_def trms_listsst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma setops_listsst_is_setopssst: "setopssst S = set (setops_listsst S)"
unfolding setopssst_def setops_listsst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma fv_listsstp_is_fvsstp: "fvsstp a = set (fv_listsstp a)"
proof (cases a)
  case (NegChecks X F G) thus ?thesis
    using fvpairs_append[of F G] fv_listpairs_append[of F G]
          fv_listpairs_is_fvpairs[of "F@G"]
    by auto
qed (simp_all add: fv_listpairs_is_fvpairs fv_list_is_fv)

lemma fv_listsst_is_fvsst: "fvsst S = set (fv_listsst S)"
unfolding fvsst_def fv_listsst_def by (induct S) (simp_all add: fv_listsstp_is_fvsstp)

lemma trmssstp_finite[simp]: "finite (trmssstp x)"
by (cases x) auto

lemma trmssst_finite[simp]: "finite (trmssst S)"
using trmssstp_finite unfolding trmssst_def by (induct S) auto

lemma varssstp_finite[simp]: "finite (varssstp x)"
by (cases x) auto

lemma varssst_finite[simp]: "finite (varssst S)"
using varssstp_finite unfolding varssst_def by (induct S) auto

lemma fvsstp_finite[simp]: "finite (fvsstp x)"
by (cases x) auto

lemma fvsst_finite[simp]: "finite (fvsst S)"
using fvsstp_finite unfolding fvsst_def by (induct S) auto

lemma bvarssstp_finite[simp]: "finite (set (bvarssstp x))"
by (rule finite_set)

lemma bvarssst_finite[simp]: "finite (bvarssst S)"
using bvarssstp_finite unfolding bvarssst_def by (induct S) auto

lemma subst_sst_nil[simp]: "[] ⋅sst δ = []"
by (simp add: subst_apply_stateful_strand_def)

lemma dbsst_nil[simp]: "dbsst [] ℐ = []"
by (simp add: dbsst_def)

lemma iksst_nil[simp]: "iksst [] = {}"
by (simp add: iksst_def)

lemma in_iksst_iff: "t ∈ iksst A ⟷ (∃ts. receive⟨ts⟩ ∈ set A ∧ t ∈ set ts)"
unfolding iksst_def by blast

lemma iksst_append[simp]: "iksst (A@B) = iksst A ∪ iksst B"
by (auto simp add: iksst_def)

lemma iksst_concat: "iksst (concat xs) = ⋃(iksst ` set xs)"
by (induct xs) auto

lemma iksst_subst: "iksst (A ⋅sst δ) = iksst A ⋅set δ"
proof (induction A)
  case (Cons a A)
  have "iksst ([a] ⋅sst δ) = iksst [a] ⋅set δ"
  proof (cases a)
    case (Receive ts) thus ?thesis
      using in_iksst_iff[of _ "[a]"] in_iksst_iff[of _ "[a] ⋅sst δ"]
      unfolding subst_apply_stateful_strand_def by auto
  qed (simp_all add: iksst_def subst_apply_stateful_strand_def)
  thus ?case
    using Cons.IH iksst_append
    by (metis append_Cons append_Nil image_Un map_append subst_apply_stateful_strand_def) 
qed simp

lemma iksst_set_subset:
  "set A ⊆ set B ⟹ iksst A ⊆ iksst B"
unfolding iksst_def by blast

lemma iksst_prefix_subset:
  "prefix A B ⟹ iksst A ⊆ iksst B" (is "?P A B ⟹ ?P' A B")
  "prefix A (C@D) ⟹ ¬prefix A C ⟹ iksst C ⊆ iksst A" (is "?Q ⟹ ?Q' ⟹ ?Q''")
proof -
  show "?P A B ⟹ ?P' A B" for A B by (metis set_mono_prefix iksst_set_subset)
  thus "?Q ⟹ ?Q' ⟹ ?Q''" by (metis prefixI prefix_same_cases)
qed

lemma iksst_snoc_no_receive_empty:
  assumes "∀a ∈ set A. ¬is_Receive a"
  shows "iksst A ⋅set I = {}"
using assms in_iksst_iff[of _ A] by fastforce

lemma iksst_snoc_no_receive_eq:
  assumes "∄s. a = receive⟨s⟩"
  shows "iksst (A@[a]) ⋅set ℐ = iksst A ⋅set ℐ"
using assms iksst_snoc_no_receive_empty[of "[a]" ℐ] iksst_append[of A "[a]"]
unfolding is_Receive_def by auto

lemma dbsst_set_is_dbupdsst: "set (db'sst A I D) = dbupdsst A I (set D)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix t s show "(t,s) ∈ ?A ⟹ (t,s) ∈ ?B" by (induct rule: db'sst.induct) auto
  qed

  show "?B ⊆ ?A"
  proof
    fix t s show "(t,s) ∈ ?B ⟹ (t,s) ∈ ?A" by (induct arbitrary: D rule: dbupdsst.induct) auto
  qed
qed

lemma dbsst_no_upd:
  assumes "∀a ∈ set A. ¬is_Insert a ∧ ¬is_Delete a"
  shows "db'sst A I D = D"
using assms
proof (induction A)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbsst_no_upd_append:
  assumes "∀b ∈ set B. ¬is_Insert b ∧ ¬is_Delete b"
  shows "db'sst A = db'sst (A@B)"
  using assms
proof (induction A)
  case Nil thus ?case by (simp add: dbsst_no_upd)
next
  case (Cons a A) thus ?case by (cases a) simp_all
qed

lemma dbsst_append:
  "db'sst (A@B) I D = db'sst B I (db'sst A I D)"
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbsst_in_cases:
  assumes "(t,s) ∈ set (db'sst A I D)"
  shows "(t,s) ∈ set D ∨ (∃t' s'. insert⟨t',s'⟩ ∈ set A ∧ t = t' ⋅ I ∧ s = s' ⋅ I)"
  using assms
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) fastforce+
qed simp

lemma dbsst_in_cases':
  assumes "(t,s) ∈ set (db'sst A I D)"
    and "(t,s) ∉ set D"
  shows "∃B C t' s'. A = B@insert⟨t',s'⟩#C ∧ t = t' ⋅ I ∧ s = s' ⋅ I ∧
                     (∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I)"
  using assms(1)
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  note * = snoc dbsst_append[of A "[a]" I D]
  thus ?case
  proof (cases a)
    case (Insert t' s')
    thus ?thesis using * by (cases "(t,s) ∈ set (db'sst A I D)") force+
  next
    case (Delete t' s')
    hence **: "t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I" using * by simp

    have "(t,s) ∈ set (db'sst A I D)" using * Delete by force
    then obtain B C u v where B:
        "A = B@insert⟨u,v⟩#C" "t = u ⋅ I" "s = v ⋅ I"
        "∀t' s'. delete⟨t',s'⟩ ∈ set C ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
      using snoc.IH by atomize_elim auto

    have "A@[a] = B@insert⟨u,v⟩#(C@[a])"
         "∀t' s'. delete⟨t',s'⟩ ∈ set (C@[a]) ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
      using B(1,4) Delete ** by auto
    thus ?thesis using B(2,3) by blast
  qed force+
qed (simp add: assms(2))

lemma dbsst_filter:
  "db'sst A I D = db'sst (filter is_Update A) I D"
by (induct A I D rule: db'sst.induct) simp_all

lemma dbsst_subst_swap:
  assumes "∀x ∈ fvsst A. I x = J x"
  shows "db'sst A I D = db'sst A J D"
using assms
proof (induction A arbitrary: D)
  case (Cons a A)
  hence "∀x ∈ fvsstp a. I x = J x" "⋀D. db'sst A I D = db'sst A J D" by auto
  thus ?case by (cases a) (simp_all add: term_subst_eq[of _ I J])
qed simp

lemma dbupdsst_no_upd:
  assumes "∀a ∈ set A. ¬is_Insert a ∧ ¬is_Delete a"
  shows "dbupdsst A I D = D"
using assms
proof (induction A)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbupdsst_no_deletes:
  assumes "list_all (λa. ¬is_Delete a) A"
  shows "dbupdsst A I D = D ∪ {(t ⋅ I, s ⋅ I) | t s. insert⟨t,s⟩ ∈ set A}" (is "?Q A D")
using assms
proof (induction A arbitrary: D)
  case (Cons a A)
  hence IH: "?Q A D" for D by auto
  have "¬is_Delete a" using Cons.prems by simp
  thus ?case using IH by (cases a) auto
qed simp

lemma dbupdsst_append:
  "dbupdsst (A@B) I D = dbupdsst B I (dbupdsst A I D)"
proof (induction A arbitrary: D)
  case (Cons a A) thus ?case by (cases a) auto
qed simp

lemma dbupdsst_filter:
  "dbupdsst A I D = dbupdsst (filter is_Update A) I D"
by (induct A I D rule: dbupdsst.induct) simp_all

lemma dbupdsst_in_cases:
  assumes "(t,s) ∈ dbupdsst A I D"
  shows "(t,s) ∈ D ∨ (∃t' s'. insert⟨t',s'⟩ ∈ set A ∧ t = t' ⋅ I ∧ s = s' ⋅ I)" (is ?P)
    and "∀u v B. suffix (delete⟨u,v⟩#B) A ∧ (t,s) = (u,v) ⋅p I ⟶
                  (∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B)" (is ?Q)
proof -
  show ?P using assms
  proof (induction A arbitrary: D)
    case (Cons a A) thus ?case by (cases a) fastforce+
  qed simp

  show ?Q using assms
  proof (induction A arbitrary: D rule: List.rev_induct)
    case (snoc a A)
    note 0 = snoc.IH snoc.prems
    note 1 = suffix_snoc[of _ A a]

    have 2: "dbupdsst (A@[a]) I D = dbupdsst A I D" when "¬is_Update a"
      using that dbupdsst_append[of A "[a]" I D] by (cases a) auto

    have 3: "suffix (delete⟨u,v⟩#B) A ⟹ suffix (delete⟨u,v⟩#B@[a]) (A@[a])"
      when "¬is_Update a" for u v B
      using that by simp

    have 4: "∃C. B = C@[a] ∧ suffix (delete⟨u,v⟩#C) A"
      when a: "¬is_Delete a" "suffix (delete⟨u,v⟩#B) (A@[a])" for u v B
    proof -
      have a': "a ≠ delete⟨u,v⟩" using a(1) by force
      obtain C where C: "delete⟨u,v⟩#B = C@[a]" "suffix C A" using 1 a(2) by blast
      show ?thesis using a' C by (cases C) auto
    qed

    note 5 = dbupdsst_append[of A "[a]" I]

    show ?case
    proof (cases "is_Update a")
      case True
      then obtain u v where "a = insert⟨u,v⟩ ∨ a = delete⟨u,v⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨u,v⟩"
        hence a': "¬is_Delete a" by simp

        have 6: "insert⟨u,v⟩ ∈ set B"
          when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for u' v' B
          using 4[OF a' B] unfolding a by fastforce

        have 7: "(t,s) = (u,v) ⋅p I ∨ (t,s) ∈ dbupdsst A I D" using snoc.prems 5 a by auto
        show ?thesis
        proof (cases "(t,s) = (u,v) ⋅p I")
          case True
          have "insert⟨u,v⟩ ∈ set B"
            when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for u' v' B
            using 4[OF a' B] unfolding a by fastforce
          thus ?thesis using True by blast
        next
          case False
          hence 8: "(t,s) ∈ dbupdsst A I D" using 7 by blast
          have "∃u'' v''. (t,s) = (u'',v'') ⋅p I ∧ insert⟨u'',v''⟩ ∈ set B"
            when B: "suffix (delete⟨u',v'⟩#B) (A @ [a])" "(t,s) = (u',v') ⋅p I" for u' v' B
          proof -
            obtain C where C: "B = C@[a]" "suffix (delete⟨u',v'⟩#C) A" using 4[OF a' B(1)] by blast
            thus ?thesis using snoc.IH[OF 8] B(2) unfolding a by fastforce
          qed
          thus ?thesis by blast
        qed
      next
        assume a: "a = delete⟨u,v⟩"
        hence "(t,s) ∈ dbupdsst A I D - {((u,v) ⋅p I)}" using snoc.prems 5 by auto
        hence 6: "(t,s) ∈ dbupdsst A I D" "(t,s) ≠ (u,v) ⋅p I" by (blast,blast)
        
        have "(∃C. B = C@[a] ∧ suffix (delete⟨u',v'⟩#C) A) ∨ (B = [] ∧ u' = u ∧ v' = v)"
          when B: "suffix (delete⟨u',v'⟩#B) (A@[a])" for B u' v'
        proof -
          obtain C where C: "delete⟨u',v'⟩#B = C@[a]" "suffix C A" using B 1 by blast
          show ?thesis
          proof (cases "B = []")
            case True thus ?thesis using C unfolding a by simp
          next
            case False
            then obtain b B' where B': "B = B'@[b]" by (meson rev_exhaust)
            show ?thesis using C unfolding a B' by auto
          qed 
        qed
        hence "∃C. B = C@[a] ∧ suffix (delete⟨u',v'⟩#C) A"
          when "suffix (delete⟨u',v'⟩#B) (A@[a])" "(t,s) = (u',v') ⋅p I" for B u' v'
          using that 6 by blast
        thus ?thesis using snoc.IH[OF 6(1)] unfolding a by fastforce
      qed
    next
      case False
      have "∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B"
        when B: "suffix (delete⟨u,v⟩#B) (A@[a])" "(t,s) = (u,v) ⋅p I" for u v B
      proof -
        obtain C where C: "B = C@[a]" "suffix (delete⟨u,v⟩#C) A" using 4[OF _ B(1)] False by blast
        show ?thesis using B(2) snoc.IH[OF snoc.prems[unfolded 2[OF False]]] C by fastforce
      qed
      thus ?thesis by blast
    qed
  qed simp
qed

lemma dbupdsst_in_iff:
  "(t,s) ∈ dbupdsst A I D ⟷
   ((∀u v B. suffix (delete⟨u,v⟩#B) A ∧ (t,s) = (u,v) ⋅p I ⟶
              (∃u' v'. (t,s) = (u',v') ⋅p I ∧ insert⟨u',v'⟩ ∈ set B)) ∧
    ((t,s) ∈ D ∨ (∃u v. (t,s) = (u,v) ⋅p I ∧ insert⟨u,v⟩ ∈ set A)))"
  (is "?P A D ⟷ ?Q1 A ∧ ?Q2 A D")
proof
  show "?P A D ⟹ ?Q1 A ∧ ?Q2 A D" using dbupdsst_in_cases by fast

  show "?Q1 A ∧ ?Q2 A D ⟹ ?P A D"
  proof (induction A arbitrary: D)
    case (Cons a A)
    have Q1: "?Q1 A" using Cons.prems suffix_Cons[of _ a A] by blast

    show ?case
    proof (cases "is_Update a")
      case False thus ?thesis using Q1 Cons.IH Cons.prems by (cases a) auto
    next
      case True
      then obtain t' s' where "a = insert⟨t',s'⟩ ∨ a = delete⟨t',s'⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨t',s'⟩"
        hence "?Q2 A (insert ((t',s') ⋅p I) D)" using Cons.prems by auto
        thus ?thesis using Q1 Cons.IH unfolding a by auto
      next
        assume a: "a = delete⟨t',s'⟩"
        hence "?Q2 A (D - {(t',s') ⋅p I})" using Cons.prems by auto
        thus ?thesis using Q1 Cons.IH unfolding a by auto
      qed
    qed
  qed simp
qed

lemma dbupdsst_in_cases':
  fixes A::"('a,'b) stateful_strand"
  assumes "(t,s) ∈ dbupdsst A I D"
    and "(t,s) ∉ D"
  shows "∃B C t' s'. A = B@insert⟨t',s'⟩#C ∧ t = t' ⋅ I ∧ s = s' ⋅ I ∧
                     (∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I)"
using assms(1)
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  note 0 = dbupdsst_append[of A "[a]" I D]
  have 1: "(t,s) ∈ dbupdsst A I D" when "¬is_Update a" using that snoc.prems 0 by (cases a) auto
  show ?case
  proof (cases "is_Update a")
    case False
    obtain B C t' s' where B:
        "A = B@insert⟨t',s'⟩#C" "t = t' ⋅ I" "s = s' ⋅ I"
        "∀t'' s''. delete⟨t'',s''⟩ ∈ set C ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I"
      using snoc.IH[OF 1[OF False]] by blast

    have "A@[a] = B@insert⟨t',s'⟩#(C@[a])"
         "∀t'' s''. delete⟨t'',s''⟩ ∈ set (C@[a]) ⟶ t ≠ t'' ⋅ I ∨ s ≠ s'' ⋅ I"
      using False B(1,4) by auto
    thus ?thesis using B(2,3) by blast
  next
    case True
    then obtain t' s' where "a = insert⟨t',s'⟩ ∨ a = delete⟨t',s'⟩" by (cases a) auto
    thus ?thesis
    proof
      assume a: "a = insert⟨t',s'⟩"
      hence "dbupdsst (A@[a]) I D = insert ((t',s') ⋅p I) (dbupdsst A I D)" using 0 by simp
      hence "(t,s) = (t',s') ⋅p I ∨ (t,s) ∈ dbupdsst A I D" using snoc.prems by blast
      thus ?thesis
      proof
        assume 2: "(t,s) ∈ dbupdsst A I D" show ?thesis using snoc.IH[OF 2] unfolding a by force
      qed (force simp add: a)
    next
      assume a: "a = delete⟨t',s'⟩"
      hence 2: "t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I" using 0 snoc.prems by simp
  
      have "(t,s) ∈ dbupdsst A I D" using 0 snoc.prems a by force
      then obtain B C u v where B:
          "A = B@insert⟨u,v⟩#C" "t = u ⋅ I" "s = v ⋅ I"
          "∀t' s'. delete⟨t',s'⟩ ∈ set C ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
        using snoc.IH by atomize_elim auto
  
      have "A@[a] = B@insert⟨u,v⟩#(C@[a])"
           "∀t' s'. delete⟨t',s'⟩ ∈ set (C@[a]) ⟶ t ≠ t' ⋅ I ∨ s ≠ s' ⋅ I"
        using B(1,4) a 2 by auto
      thus ?thesis using B(2,3) by blast
    qed
  qed
qed (simp add: assms(2))

lemma dbupdsst_mono:
  assumes "D ⊆ E"
  shows "dbupdsst A I D ⊆ dbupdsst A I E"
using assms
proof (induction A arbitrary: D E)
  case (Cons a A) thus ?case
  proof (cases a)
    case (Insert t s)
    have "insert ((t,s) ⋅p I) D ⊆ insert ((t,s) ⋅p I) E" using Cons.prems by fast
    thus ?thesis using Cons.IH unfolding Insert by simp
  next
    case (Delete t s)
    have "D - {(t,s) ⋅p I} ⊆ E - {(t,s) ⋅p I}" using Cons.prems by fast
    thus ?thesis using Cons.IH unfolding Delete by simp
  qed auto
qed simp

lemma dbupdsst_db_narrow:
  assumes "(t,s) ∈ dbupdsst A I (D ∪ E)"
    and "(t,s) ∉ D"
  shows "(t,s) ∈ dbupdsst A I E"
using assms
proof (induction A arbitrary: D E)
  case (Cons a A) thus ?case
  proof (cases a)
    case (Delete t' s') thus ?thesis
      using Cons.prems Cons.IH[of "D - {(t',s') ⋅p I}" "E - {(t',s') ⋅p I}"] by (simp add: Un_Diff)
  qed auto
qed simp

lemma dbupdsst_set_term_neq_in_iff:
  assumes f: "f ≠ k"
    and A: "∀t s. insert⟨t,s⟩ ∈ set A ⟶ (∃g ts. s = Fun g ts)"
  shows "(t,Fun f ts) ∈ dbupdsst A I D ⟷
         (t,Fun f ts) ∈ dbupdsst (filter (λa. ∄s ss. a = insert⟨s,Fun k ss⟩) A) I D"
    (is "?P A D ⟷ ?P (?f A) D")
proof
  show "?P A D ⟹ ?P (?f A) D" using A
  proof (induction A arbitrary: D)
    case (Cons a A)
    have IH: "?P A D ⟹ ?P (?f A) D" for D
      using Cons.prems(2) Cons.IH by simp

    show ?case
    proof (cases "is_Update a")
      case True
      then obtain u s where "a = insert⟨u,s⟩ ∨ a = delete⟨u,s⟩" by (cases a) auto
      thus ?thesis
      proof
        assume a: "a = insert⟨u,s⟩"
        obtain g ss where s: "s = Fun g ss" using a Cons.prems(2) by fastforce

        have 0: "?P A (insert ((u, s) ⋅p I) D)" using a Cons.prems(1) by fastforce
        show ?thesis
        proof (cases "g = k")
          case g: True
          have "?f (a#A) = ?f A" unfolding a s g by force
          moreover have "(t,Fun f ts) ≠ (u, Fun g ss) ⋅p I" using f unfolding g by auto
          ultimately show ?thesis
            using IH[OF 0] dbupdsst_db_narrow[of t "Fun f ts" "?f A" I "{(u, s) ⋅p I}" D]
            unfolding a s g by force
        next
          case g: False
          have "?f (a#A) = a#?f A" using g unfolding a s by force
          thus ?thesis using Cons.prems Cons.IH g unfolding a s by force
        qed
      next
        assume a: "a = delete⟨u,s⟩"
        hence "?f (a#A) = a#?f A" by auto
        thus ?thesis using Cons.prems Cons.IH unfolding a by fastforce
      qed
    next
      case a: False
      hence "?P A D" using Cons.prems(1) by (cases a) auto
      hence "?P (?f A) D" using Cons.IH Cons.prems(2) a by fastforce
      thus ?thesis using a by (cases a) auto
    qed
  qed simp

  have "dbupdsst (?f A) I D ⊆ dbupdsst A I D"
  proof (induction A arbitrary: D)
    case (Cons a A) show ?case
    proof (cases a)
      case (Insert t s)
      have "?f (a#A) = a#?f A ∨ ?f (a#A) = ?f A" unfolding Insert by force
      hence "dbupdsst (?f (a#A)) I D ⊆ dbupdsst (?f A) I (insert ((t,s) ⋅p I) D)"
        using dbupdsst_mono[of D "insert ((t, s) ⋅p I) D"] unfolding Insert by auto
      thus ?thesis using Cons.IH unfolding Insert by fastforce
    qed (use Cons.prems Cons.IH in auto)
  qed simp
  thus "?P (?f A) D ⟹ ?P A D" by blast
qed

lemma dbupdsst_subst_const_swap:
  fixes t s
  defines "fvs ≡ λA D. fvsst A ∪ fv t ∪ fv s ∪ ⋃(fvpair ` D)"
  assumes "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ)" (is "?in δ A D")
    and "∀x ∈ fvs A D.
          δ x = θ x ∨
          (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ s) ∧ ¬(θ x ⊑ t) ∧ ¬(θ x ⊑ s) ∧
           (∀(u,v) ∈ D. ¬(δ x ⊑ u) ∧ ¬(δ x ⊑ v) ∧ ¬(θ x ⊑ u) ∧ ¬(θ x ⊑ v)) ∧
           (∀u v. insert⟨u,v⟩ ∈ set A ∨ delete⟨u,v⟩ ∈ set A ⟶
                    ¬(δ x ⊑ u) ∧ ¬(δ x ⊑ v) ∧ ¬(θ x ⊑ u) ∧ ¬(θ x ⊑ v)))"
      (is "?A δ θ D")
    and "∀x ∈ fvs A D. ∃c. δ x = Fun c []" (is "?B δ")
    and "∀x ∈ fvs A D. ∃c. θ x = Fun c []" (is "?B θ")
    and "∀x ∈ fvs A D. ∀y ∈ fvs A D. δ x = δ y ⟷ θ x = θ y" (is "?C δ θ A D")
  shows "(t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)" (is "?in θ A D")
using assms(2-)
proof (induction A arbitrary: D rule: List.rev_induct)
  case Nil
  then obtain u v where u: "(u,v) ∈ D" "t ⋅ δ = u ⋅ δ" "s ⋅ δ = v ⋅ δ" by auto

  let ?X = "fv t ∪ fv u"
  let ?Y = "fv s ∪ fv v"

  have 0: "fv u ⊆ fvs [] D" "fv v ⊆ fvs [] D" "fv t ⊆ fvs [] D" "fv s ⊆ fvs [] D"
    using u(1) unfolding fvs_def by (blast, blast, blast, blast)

  have 1: "∀x ∈ ?X. δ x = θ x ∨ (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ u))"
          "∀x ∈ ?Y. δ x = θ x ∨ (¬(δ x ⊑ s) ∧ ¬(δ x ⊑ v))"
    using Nil.prems(2) u(1) unfolding fvs_def by (blast,blast)

  have 2: "∀x ∈ ?X. ∃c. δ x = Fun c []" "∀x ∈ ?X. ∃c. θ x = Fun c []"
          "∀x ∈ ?Y. ∃c. δ x = Fun c []" "∀x ∈ ?Y. ∃c. θ x = Fun c []"
    using Nil.prems(3,4) 0 by (blast,blast,blast,blast)

  have 3: "∀x ∈ ?X. ∀y ∈ ?X. δ x = δ y ⟷ θ x = θ y"
          "∀x ∈ ?Y. ∀y ∈ ?Y. δ x = δ y ⟷ θ x = θ y"
    using Nil.prems(5) 0 by (blast,blast)

  have "t ⋅ θ = u ⋅ θ" "s ⋅ θ = v ⋅ θ"
    using subst_const_swap_eq'[OF u(2) 1(1) 2(1,2) 3(1)]
          subst_const_swap_eq'[OF u(3) 1(2) 2(3,4) 3(2)]
    by argo+
  thus ?case using u(1) by force
next
  case (snoc a A)
  have 0: "fvs A D ⊆ fvs (A@[a]) D" "set A ⊆ set (A@[a])" unfolding fvs_def by auto

  note 1 = dbupdsst_append[of A "[a]"]

  have IH: "(t ⋅ δ, s ⋅ δ) ∈ dbupdsst A δ (D ⋅pset δ) ⟹ (t ⋅ θ, s ⋅ θ) ∈ dbupdsst A θ (D ⋅pset θ)"
    using snoc.IH[of D] snoc.prems(2-) 0 by blast

  let ?q0 = "λt s δ θ. ∀x ∈ fv t ∪ fv s. δ x = θ x ∨ (¬(δ x ⊑ t) ∧ ¬(δ x ⊑ s))"
  let ?q1 = "λt s δ.   ∀x ∈ fv t ∪ fv s. ∃c. δ x = Fun c []"
  let ?q2 = "λt s δ θ. ∀x ∈ fv t ∪ fv s. ∀y ∈ fv t ∪ fv s. δ x = δ y ⟷ θ x = θ y"

  show ?case
  proof (cases "is_Update a")
    case False
    hence "dbupdsst (A@[a]) δ (D ⋅pset δ) = dbupdsst A δ (D ⋅pset δ)"
          "dbupdsst (A@[a]) θ (D ⋅pset θ) = dbupdsst A θ (D ⋅pset θ)"
      using 1 by (cases a; auto)+
    thus ?thesis using IH snoc.prems(1) by blast
  next
    case True
    then obtain u v where u: "a = insert⟨u,v⟩ ∨ a = delete⟨u,v⟩" by (cases a) auto

    have uv_in: "insert⟨u,v⟩ ∈ set (A@[a]) ∨ delete⟨u,v⟩ ∈ set (A@[a])" using u by force
    hence fv_uv: "fv u ⊆ fvs (A@[a]) D" "fv v ⊆ fvs (A@[a]) D" unfolding fvs_def by (force,force)

    have fv_ts: "fv t ⊆ fvs (A@[a]) D" "fv s ⊆ fvs (A@[a]) D" unfolding fvs_def by (blast,blast)

    have q0: "?q0 t u δ θ" "?q0 s v δ θ"
             "?q0 t u θ δ" "?q0 s v θ δ"
    proof -
      show "?q0 t u δ θ" "?q0 s v δ θ"
        using snoc.prems(2) 0 fv_ts fv_uv uv_in by (blast,blast)

      show "?q0 t u θ δ"
      proof
        fix x assume "x ∈ fv t ∪ fv u"
        hence "x ∈ fvs (A@[a]) D" using fv_ts(1) fv_uv(1) by blast
        thus "θ x = δ x ∨ (¬(θ x ⊑ t) ∧ ¬(θ x ⊑ u))" 
          using snoc.prems(2) uv_in by auto
      qed

      show "?q0 s v θ δ"
      proof
        fix x assume "x ∈ fv s ∪ fv v"
        hence "x ∈ fvs (A@[a]) D" using fv_ts(2) fv_uv(2) by blast
        thus "θ x = δ x ∨ (¬(θ x ⊑ s) ∧ ¬(θ x ⊑ v))"