Theory Stateful_Typing

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

section ‹Extending the Typing Result to Stateful Constraints›

theory Stateful_Typing
imports Typing_Result Stateful_Strands
begin

text ‹\label{sec:Stateful-Typing}Locale setup›
locale stateful_typed_model = typed_model arity public Ana Γ
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,'var) term  (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term  ('fun,'atom::finite) term_type"
  +
  fixes Pair::"'fun"
  assumes Pair_arity: "arity Pair = 2"
  and Ana_subst': "f T δ K M. Ana (Fun f T) = (K,M)  Ana (Fun f T  δ) = (K list δ,M list δ)"
begin

lemma Ana_invar_subst'[simp]: "Ana_invar_subst 𝒮"
using Ana_subst' unfolding Ana_invar_subst_def by force

definition pair where
  "pair d  case d of (t,t')  Fun Pair [t,t']"

fun trpairs::
  "(('fun,'var) term × ('fun,'var) term) list 
   ('fun,'var) dbstatelist 
   (('fun,'var) term × ('fun,'var) term) list list"
where
  "trpairs [] D = [[]]"
| "trpairs ((s,t)#F) D =
    concat (map (λd. map ((#) (pair (s,t), pair d)) (trpairs F D)) D)"

text ‹
  A translation/reduction tr› from stateful constraints to (lists of) "non-stateful" constraints.
  The output represents a finite disjunction of constraints whose models constitute exactly the
  models of the input constraint. The typing result for "non-stateful" constraints is later lifted
  to the stateful setting through this reduction procedure.
›
fun tr::"('fun,'var) stateful_strand  ('fun,'var) dbstatelist  ('fun,'var) strand list"
where
  "tr [] D = [[]]"
| "tr (send⟨ts#A) D = map ((#) (send⟨tsst)) (tr A D)"
| "tr (receive⟨ts#A) D = map ((#) (receive⟨tsst)) (tr A D)"
| "tr (ac: t  t'#A) D = map ((#) (ac: t  t'st)) (tr A D)"
| "tr (insert⟨t,s#A) D = tr A (List.insert (t,s) D)"
| "tr (delete⟨t,s#A) D =
    concat (map (λDi. map (λB. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                               (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])@B)
                          (tr A [dD. d  set Di]))
                (subseqs D))"
| "tr (ac: t  s#A) D =
    concat (map (λB. map (λd. ac: (pair (t,s))  (pair d)st#B) D) (tr A D))"
| "tr (X⟨∨≠: F ∨∉: F'#A) D =
    map ((@) (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))) (tr A D)"

text ‹Type-flaw resistance of stateful constraint steps›
fun tfrsstp where
  "tfrsstp (Equality _ t t') = ((δ. Unifier δ t t')  Γ t = Γ t')"
| "tfrsstp (NegChecks X F F') = (
    (F' = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)) 
    (f T. Fun f T  subtermsset (trmspairs F  pair ` set F') 
              T = []  (s  set T. s  Var ` set X)))"
| "tfrsstp _ = True"

text ‹Type-flaw resistance of stateful constraints›
definition tfrsst where "tfrsst S  tfrset (trmssst S  pair ` setopssst S)  list_all tfrsstp S"



subsection ‹Minor Lemmata›
lemma pair_in_pair_image_iff:
  "pair (s,t)  pair ` P  (s,t)  P"
unfolding pair_def by fast

lemma subst_apply_pairs_pair_image_subst:
  "pair ` set (F pairs θ) = pair ` set F set θ"
unfolding subst_apply_pairs_def pair_def by (induct F) auto

lemma Ana_subst_subterms_cases:
  fixes θ::"('fun,'var) subst"
  assumes t: "t set M set θ"
    and s: "s  set (snd (Ana t))"
  shows "(u  subtermsset M. t = u  θ  s  set (snd (Ana u)) set θ)  (x  fvset M. t  θ x)"
proof (cases "t  subtermsset M set θ")
  case True
  then obtain u where u: "u  subtermsset M" "t = u  θ" by blast
  show ?thesis
  proof (cases u)
    case (Var x)
    hence "x  fvset M" using fv_subset_subterms[OF u(1)] by simp
    thus ?thesis using u(2) Var by fastforce
  next
    case (Fun f T)
    hence "set (snd (Ana t)) = set (snd (Ana u)) set θ"
      using Ana_subst'[of f T _ _ θ] u(2) by (cases "Ana u") auto
    thus ?thesis using s u by blast
  qed
qed (use s t subtermsset_subst in blast)

lemma Ana_snd_subst_nth_inv:
  fixes θ::"('fun,'var) subst" and f ts
  defines "R  snd (Ana (Fun f ts  θ))"
  assumes r: "r = R ! i" "i < length R"
  shows "r = snd (Ana (Fun f ts)) ! i  θ"
proof -
  obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
  thus ?thesis using Ana_subst'[of f ts K R θ] r unfolding R_def by auto
qed

lemma Ana_snd_subst_inv:
  fixes θ::"('fun,'var) subst"
  assumes r: "r  set (snd (Ana (Fun f ts  θ)))"
  shows "t  set (snd (Ana (Fun f ts))). r = t  θ"
proof -
  obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
  thus ?thesis using Ana_subst'[of f ts K R θ] r by auto
qed


lemma fun_pair_eq[dest]: "pair d = pair d'  d = d'"
proof -
  obtain t s t' s' where "d = (t,s)" "d' = (t',s')" by atomize_elim auto
  thus "pair d = pair d'  d = d'" unfolding pair_def by simp
qed

lemma fun_pair_subst: "pair d  δ = pair (d p δ)"
using surj_pair[of d] unfolding pair_def by force  

lemma fun_pair_subst_set: "pair ` M set δ = pair ` (M pset δ)"
proof
  show "pair ` M set δ  pair ` (M pset δ)"
    using fun_pair_subst[of _ δ] by fastforce

  show "pair ` (M pset δ)  pair ` M set δ"
  proof
    fix t assume t: "t  pair ` (M pset δ)"
    then obtain p where p: "p  M" "t = pair (p p δ)" by blast
    thus "t  pair ` M set δ" using fun_pair_subst[of p δ] by force
  qed
qed

lemma fun_pair_eq_subst: "pair d  δ = pair d'  θ  d p δ = d' p θ"
by (metis fun_pair_subst fun_pair_eq[of "d p δ" "d' p θ"])

lemma setopssst_pair_image_cons[simp]:
  "pair ` setopssst (x#S) = pair ` setopssstp x  pair ` setopssst S"
  "pair ` setopssst (send⟨ts#S) = pair ` setopssst S"
  "pair ` setopssst (receive⟨ts#S) = pair ` setopssst S"
  "pair ` setopssst (ac: t  t'#S) = pair ` setopssst S"
  "pair ` setopssst (insert⟨t,s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (delete⟨t,s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (ac: t  s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (X⟨∨≠: F ∨∉: G#S) = pair ` set G  pair ` setopssst S"
unfolding setopssst_def by auto

lemma setopssst_pair_image_subst_cons[simp]:
  "pair ` setopssst (x#S sst θ) = pair ` setopssstp (x sstp θ)  pair ` setopssst (S sst θ)"
  "pair ` setopssst (send⟨ts#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (receive⟨ts#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (ac: t  t'#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (insert⟨t,s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (delete⟨t,s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (ac: t  s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (X⟨∨≠: F ∨∉: G#S sst θ) =
    pair ` set (G pairs rm_vars (set X) θ)  pair ` setopssst (S sst θ)"
using subst_sst_cons[of _ S θ] unfolding setopssst_def pair_def by auto

lemma setopssst_are_pairs: "t  pair ` setopssst A  s s'. t = pair (s,s')"
proof (induction A)
  case (Cons a A) thus ?case
    by (cases a) (auto simp add: setopssst_def)
qed (simp add: setopssst_def)

lemma fun_pair_wftrm: "wftrm t  wftrm t'  wftrm (pair (t,t'))"
using Pair_arity unfolding wftrm_def pair_def by auto

lemma wftrms_pairs: "wftrms (trmspairs F)  wftrms (pair ` set F)"
using fun_pair_wftrm by blast

lemma wf_fun_pair_ineqs_map:
  assumes "wfst X A"
  shows "wfst X (map (λd. Y⟨∨≠: [(pair (t, s), pair d)]st) D@A)"
using assms by (induct D) auto

lemma wf_fun_pair_negchecks_map:
  assumes "wfst X A"
  shows "wfst X (map (λG. Y⟨∨≠: (F@G)st) M@A)"
using assms by (induct M) auto

lemma wf_fun_pair_eqs_ineqs_map:
  fixes A::"('fun,'var) strand"
  assumes "wfst X A" "Di  set (subseqs D)" "(t,t')  set D. fv t  fv t'  X"
  shows "wfst X ((map (λd. check: (pair (t,s))  (pair d)st) Di)@
                 (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])@A)"
proof -
  let ?c1 = "map (λd. check: (pair (t,s))  (pair d)st) Di"
  let ?c2 = "map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]"
  have 1: "wfst X (?c2@A)" using wf_fun_pair_ineqs_map[OF assms(1)] by simp
  have 2: "(t,t')  set Di. fv t  fv t'  X" 
    using assms(2,3) by (meson contra_subsetD subseqs_set_subset(1))
  have "wfst X (?c1@B)" when "wfst X B" for B::"('fun,'var) strand"
    using 2 that by (induct Di) auto
  thus ?thesis using 1 by simp
qed

lemma trmssst_wt_subst_ex:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
    and t: "t  trmssst (S sst θ)"
  shows "s δ. s  trmssst S  wtsubst δ  wftrms (subst_range δ)  t = s  δ"
using t
proof (induction S)
  case (Cons s S) thus ?case
  proof (cases "t  trmssst (S sst θ)")
    case False
    hence "t  trmssstp (s sstp θ)"
      using Cons.prems trmssst_subst_cons[of s S θ]
      by auto
    then obtain u where u: "u  trmssstp s" "t = u  rm_vars (set (bvarssstp s)) θ"
      using trmssstp_subst'' by blast
    thus ?thesis
      using trmssst_subst_cons[of s S θ]
            wt_subst_rm_vars[OF θ(1), of "set (bvarssstp s)"]
            wf_trms_subst_rm_vars'[OF θ(2), of "set (bvarssstp s)"]
      by fastforce
  qed auto
qed simp

lemma setopssst_wt_subst_ex:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
    and t: "t  pair ` setopssst (S sst θ)"
  shows "s δ. s  pair ` setopssst S  wtsubst δ  wftrms (subst_range δ)  t = s  δ"
using t
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Insert t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using Insert Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (Delete t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using Delete Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (InSet ac t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using InSet Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (NegChecks X F F')
    hence "t  pair ` set (F' pairs rm_vars (set X) θ)  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
    proof
      assume "t  pair ` set (F' pairs rm_vars (set X) θ)"
      then obtain s where s: "t = s  rm_vars (set X) θ" "s  pair ` set F'"
        using subst_apply_pairs_pair_image_subst[of F' "rm_vars (set X) θ"] by auto
      thus ?thesis
        using NegChecks setopssst_pair_image_cons(8)[of X F F' S]
              wt_subst_rm_vars[OF θ(1), of "set X"]
              wf_trms_subst_rm_vars'[OF θ(2), of "set X"]
        by fast
    qed (use Cons.IH in auto)
  qed (auto simp add: setopssst_def subst_sst_cons[of _ S θ])
qed (simp add: setopssst_def)

lemma setopssst_wftrms:
  "wftrms (trmssst A)  wftrms (pair ` setopssst A)"
  "wftrms (trmssst A)  wftrms (trmssst A  pair ` setopssst A)"
proof -
  show "wftrms (trmssst A)  wftrms (pair ` setopssst A)"
  proof (induction A)
    case (Cons a A)
    hence 0: "wftrms (trmssstp a)" "wftrms (pair ` setopssst A)" by auto
    thus ?case
    proof (cases a)
      case (NegChecks X F F')
      hence "wftrms (trmspairs F')" using 0 by simp
      thus ?thesis using NegChecks wftrms_pairs[of F'] 0 by (auto simp add: setopssst_def)
    qed (auto simp add: setopssst_def dest: fun_pair_wftrm)
  qed (auto simp add: setopssst_def)
  thus "wftrms (trmssst A)  wftrms (trmssst A  pair ` setopssst A)" by fast
qed

lemma SMP_MP_split:
  assumes "t  SMP M"
    and M: "m  M. is_Fun m"
  shows "(δ. wtsubst δ  wftrms (subst_range δ)  t  M set δ) 
         t  SMP ((subtermsset M  ((set  fst  Ana) ` M)) - M)"
  (is "?P t  ?Q t")
using assms(1)
proof (induction t rule: SMP.induct)
  case (MP t)
  have "wtsubst Var" "wftrms (subst_range Var)" "M set Var = M" by simp_all
  thus ?case using MP by metis
next
  case (Subterm t t')
  show ?case using Subterm.IH
  proof
    assume "?P t"
    then obtain s δ where s: "s  M" "t = s  δ" and δ: "wtsubst δ" "wftrms (subst_range δ)" by auto
    then obtain f T where fT: "s = Fun f T" using M by fast

    have "(s'. s'  s  t' = s'  δ)  (x  fv s. t'  δ x)"
      using subterm_subst_unfold[OF Subterm.hyps(2)[unfolded s(2)]] by blast
    thus ?thesis
    proof
      assume "s'. s'  s  t' = s'  δ"
      then obtain s' where s': "s'  s" "t' = s'  δ" by fast
      show ?thesis
      proof (cases "s'  M")
        case True thus ?thesis using s' δ by blast
      next
        case False
        hence "s'  (subtermsset M  ((set  fst  Ana) ` M)) - M" using s'(1) s(1) by force
        thus ?thesis using SMP.Substitution[OF SMP.MP[of s'] δ] s' by presburger
      qed
    next
      assume "x  fv s. t'  δ x"
      then obtain x where x: "x  fv s" "t'  δ x" by fast
      have "Var x  M" using M by blast
      hence "Var x  (subtermsset M  ((set  fst  Ana) ` M)) - M"
        using s(1) var_is_subterm[OF x(1)] by blast
      hence "δ x  SMP ((subtermsset M  ((set  fst  Ana) ` M)) - M)"
        using SMP.Substitution[OF SMP.MP[of "Var x"] δ] by auto
      thus ?thesis using SMP.Subterm x(2) by presburger
    qed
  qed (metis SMP.Subterm[OF _ Subterm.hyps(2)])
next
  case (Substitution t δ)
  show ?case using Substitution.IH
  proof
    assume "?P t"
    then obtain θ where "wtsubst θ" "wftrms (subst_range θ)" "t  M set θ" by fast
    hence "wtsubst (θ s δ)" "wftrms (subst_range (θ s δ))" "t  δ  M set (θ s δ)"
      using wt_subst_compose[of θ, OF _ Substitution.hyps(2)]
            wf_trm_subst_compose[of θ _ δ, OF _ wf_trm_subst_rangeD[OF Substitution.hyps(3)]]
            wf_trm_subst_range_iff
      by (argo, blast, auto)
    thus ?thesis by blast
  next
    assume "?Q t" thus ?thesis using SMP.Substitution[OF _ Substitution.hyps(2,3)] by meson
  qed
next
  case (Ana t K T k)
  show ?case using Ana.IH
  proof
    assume "?P t"
    then obtain θ where θ: "wtsubst θ" "wftrms (subst_range θ)" "t  M set θ" by fast
    then obtain s where s: "s  M" "t = s  θ" by auto
    then obtain f S where fT: "s = Fun f S" using M by (cases s) auto
    obtain K' T' where s_Ana: "Ana s = (K', T')" by (metis surj_pair)
    hence "set K = set K' set θ" "set T = set T' set θ"
      using Ana_subst'[of f S K' T'] fT Ana.hyps(2) s(2) by auto
    then obtain k' where k': "k'  set K'" "k = k'  θ" using Ana.hyps(3) by fast
    show ?thesis
    proof (cases "k'  M")
      case True thus ?thesis using k' θ(1,2) by blast
    next
      case False
      hence "k'  (subtermsset M  ((set  fst  Ana) ` M)) - M" using k'(1) s_Ana s(1) by force
      thus ?thesis using SMP.Substitution[OF SMP.MP[of k'] θ(1,2)] k'(2) by presburger
    qed
  next
    assume "?Q t" thus ?thesis using SMP.Ana[OF _ Ana.hyps(2,3)] by meson
  qed
qed

lemma setops_subterm_trms:
  assumes t: "t  pair ` setopssst S"
    and s: "s  t"
  shows "s  subtermsset (trmssst S)"
proof -
  obtain u u' where u: "pair (u,u')  pair ` setopssst S" "t = pair (u,u')"
    using t setopssst_are_pairs[of _ S] by blast
  hence "s  u  s  u'" using s unfolding pair_def by auto
  thus ?thesis using u setopssst_member_iff[of u u' S] unfolding trmssst_def by force
qed

lemma setops_subterms_cases:
  assumes t: "t  subtermsset (pair ` setopssst S)"
  shows "t  subtermsset (trmssst S)  t  pair ` setopssst S"
proof -
  obtain s s' where s: "pair (s,s')  pair ` setopssst S" "t  pair (s,s')"
    using t setopssst_are_pairs[of _ S] by blast
  hence "t  pair ` setopssst S  t  s  t  s'" unfolding pair_def by auto
  thus ?thesis using s setopssst_member_iff[of s s' S] unfolding trmssst_def by force
qed

lemma setops_SMP_cases:
  assumes "t  SMP (pair ` setopssst S)"
    and "p. Ana (pair p) = ([], [])"
  shows "(δ. wtsubst δ  wftrms (subst_range δ)  t  pair ` setopssst S set δ)  t  SMP (trmssst S)"
proof -
  have 0: "((set  fst  Ana) ` pair ` setopssst S) = {}"
  proof (induction S)
    case (Cons x S) thus ?case
      using assms(2) by (cases x) (auto simp add: setopssst_def)
  qed (simp add: setopssst_def)
  
  have 1: "m  pair ` setopssst S. is_Fun m"
  proof (induction S)
    case (Cons x S) thus ?case
      unfolding pair_def by (cases x) (auto simp add: assms(2) setopssst_def)
  qed (simp add: setopssst_def)

  have 2:
      "subtermsset (pair ` setopssst S) 
       ((set  fst  Ana) ` (pair ` setopssst S)) - pair ` setopssst S
         subtermsset (trmssst S)"
    using 0 setops_subterms_cases by fast

  show ?thesis
    using SMP_MP_split[OF assms(1) 1] SMP_mono[OF 2] SMP_subterms_eq[of "trmssst S"]
    by blast
qed

lemma constraint_model_priv_const_in_constr_prefix:
  assumes A: "wfsst A"
    and I: "I s A"
           "interpretationsubst I"
           "wftrms (subst_range I)"
           "wtsubst I"
    and c: "¬public c"
           "arity c = 0"
           "Fun c [] set iksst A set I"
  shows "Fun c [] set trmssst A"
using const_subterms_subst_cases[OF c(3)]
proof
  assume "Fun c [] set iksst A" thus ?thesis using iksst_trmssst_subset by blast 
next
  assume "x  fvset (iksst A). x  subst_domain I  Fun c []  I x"
  then obtain x where x: "x  fvset (iksst A)" "Fun c []  I x" by blast
  
  have 0: "wftrm (I x)" "wf'sst {} A" "Fun c []  I = Fun c []"
    using I A by simp_all

  have 1: "x  wfrestrictedvarssst A"
    using x(1) in_iksst_iff[of _ A] unfolding wfrestrictedvarssst_def by force
  hence 2: "v  wfrestrictedvarssst A. Fun c []  I  I v" using 0(3) x(2) by force


  obtain Apre Asuf where A': "¬(w  wfrestrictedvarssst Apre. Fun c []  I w)"
    "(ts. A = Apre@send⟨ts#Asuf  Fun c [] set set ts set I) 
     (s u. A = Apre@assign: s  u#Asuf  Fun c []  s  I  ¬(Fun c [] set (I ` fv u))) 
     (s u. A = Apre@assign: s  u#Asuf  (Fun c []  s  I  Fun c []  u  I))"
    (is "?X  ?Y  ?Z")
    using wfsst_strand_first_Send_var_split[OF 0(2) 2] by force

  show ?thesis using A'(2)
  proof (elim disjE)
    assume ?X
    then obtain ts where ts: "A = Apre@send⟨ts#Asuf" "Fun c [] set set ts set I" by blast
    hence "I s (Apre@[send⟨ts])"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[send⟨ts]" Asuf I] by auto
    hence "(iksst Apre) set I  t  I" when "t  set ts" for t
      using that strand_sem_append_stateful[of "{}" "{}" Apre "[send⟨ts]" I]
            strand_sem_stateful.simps(2)[of _ _ ts "[]"]
      unfolding list_all_iff by force
    hence "Fun c [] set iksst Apre set I"
      using ts(2) c(1) private_fun_deduct_in_ik by fast
    hence "Fun c [] set iksst Apre"
      using A'(1) const_subterms_subst_cases[of c I "iksst Apre"]
            iksst_fv_subset_wfrestrictedvarssst[of Apre]
      by fast
    thus ?thesis
      using iksst_trmssst_subset[of "Apre"] unfolding ts(1) by fastforce
  next
    assume ?Y
    then obtain s u where su:
        "A = Apre@assign: s  u#Asuf" "Fun c []  s  I" "¬(Fun c [] set I ` fv u)"
      by fast
    hence "s  I = u  I"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[assign: s  u]" Asuf I]
            strand_sem_append_stateful[of _ _ Apre "[assign: s  u]" I]
      by auto
    hence "Fun c []  u" using su(2,3) const_subterm_subst_var_obtain[of c u I] by auto
    thus ?thesis unfolding su(1) by auto
  next
    assume ?Z
    then obtain s u where su:
        "A = Apre@assign: s  u#Asuf" "Fun c []  s  I  Fun c []  u  I"
      by fast
    hence "(s,u) p I  dbupdsst Apre I {}"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[assign: s  u]" Asuf I]
            strand_sem_append_stateful[of _ _ Apre "[assign: s  u]" I]
      unfolding dbsst_def by auto
    then obtain s' u' where su': "insert⟨s',u'  set Apre" "s  I = s'  I" "u  I = u'  I"
      using dbsst_in_cases[of "s  I" "u  I" Apre I "[]"] dbsst_set_is_dbupdsst[of Apre I "[]"]
      by fastforce

    have "fv s'  fv u'  wfrestrictedvarssst Apre"
      using su'(1) unfolding wfrestrictedvarssst_def by force
    hence "Fun c []  s'  Fun c []  u'"
      using su(2) A'(1) su'(2,3)
            const_subterm_subst_cases[of c s' I]
            const_subterm_subst_cases[of c u' I]
      by auto
    thus ?thesis using su'(1) unfolding su(1) by force
  qed
qed

lemma trpairs_empty_case:
  assumes "trpairs F D = []"
  shows "D = []" "F  []"
proof -
  show "F  []" using assms by (auto intro: ccontr)

  have "trpairs F (a#A)  []" for a A
    by (induct F "a#A" rule: trpairs.induct) fastforce+
  thus "D = []" using assms by (cases D) simp_all
qed

lemma trpairs_elem_length_eq:
  assumes "G  set (trpairs F D)"
  shows "length G = length F" 
using assms by (induct F D arbitrary: G rule: trpairs.induct) auto

lemma trpairs_index:
  assumes "G  set (trpairs F D)" "i < length F"
  shows "d  set D. G ! i = (pair (F ! i), pair d)"
using assms
proof (induction F D arbitrary: i G rule: trpairs.induct)
  case (2 s t F D)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)"
      "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto 
  show ?case
    using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
    by (cases i) auto
qed simp

lemma trpairs_cons:
  assumes "G  set (trpairs F D)" "d  set D"
  shows "(pair (s,t), pair d)#G  set (trpairs ((s,t)#F) D)"
using assms by auto

lemma trpairs_has_pair_lists:
  assumes "G  set (trpairs F D)" "g  set G"
  shows "f  set F. d  set D. g = (pair f, pair d)"
using assms
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)"
      "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
  show ?case
    using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
    by (cases "g  set G'") auto
qed simp

lemma trpairs_is_pair_lists:
  assumes "f  set F" "d  set D"
  shows "G  set (trpairs F D). (pair f, pair d)  set G"
  (is "?P F D f d")
proof -
  have "f  set F. d  set D. ?P F D f d"
  proof (induction F D rule: trpairs.induct)
    case (2 s t F D)
    hence IH: "f  set F. d  set D. ?P F D f d" by metis
    moreover have "d  set D. ?P ((s,t)#F) D (s,t) d"
    proof
      fix d assume d: "d  set D"
      then obtain G where G: "G  set (trpairs F D)"
        using trpairs_empty_case(1) by force
      hence "(pair (s, t), pair d)#G  set (trpairs ((s,t)#F) D)"
        using d by auto
      thus "?P ((s,t)#F) D (s,t) d" using d G by auto
    qed
    ultimately show ?case by fastforce
  qed simp
  thus ?thesis by (metis assms)
qed

lemma trpairs_db_append_subset:
  "set (trpairs F D)  set (trpairs F (D@E))" (is ?A)
  "set (trpairs F E)  set (trpairs F (D@E))" (is ?B)
proof -
  show ?A
  proof (induction F D rule: trpairs.induct)
    case (2 s t F D)
    show ?case
    proof
      fix G assume "G  set (trpairs ((s,t)#F) D)"
      then obtain d G' where G':
          "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
        by atomize_elim auto
      have "d  set (D@E)" "G'  set (trpairs F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
      thus "G  set (trpairs ((s,t)#F) (D@E))" using G'(3) by auto
    qed
  qed simp

  show ?B
  proof (induction F E rule: trpairs.induct)
    case (2 s t F E)
    show ?case
    proof
      fix G assume "G  set (trpairs ((s,t)#F) E)"
      then obtain d G' where G':
          "d  set E" "G'  set (trpairs F E)" "G = (pair (s,t), pair d)#G'"
        by atomize_elim auto
      have "d  set (D@E)" "G'  set (trpairs F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
      thus "G  set (trpairs ((s,t)#F) (D@E))" using G'(3) by auto
    qed
  qed simp
qed

lemma trpairs_trms_subset:
  "G  set (trpairs F D)  trmspairs G  pair ` set F  pair ` set D"
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D G)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
 
  show ?case using "2.IH"[OF G(1,2)] G(1,3) by auto
qed simp

lemma trpairs_trms_subset':
  "(trmspairs ` set (trpairs F D))  pair ` set F  pair ` set D"
using trpairs_trms_subset by blast

lemma trpairs_vars_subset:
  "G  set (trpairs F D)  fvpairs G  fvpairs F  fvpairs D"
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D G)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
 
  show ?case using "2.IH"[OF G(1,2)] G(1,3) unfolding pair_def by auto
qed simp

lemma trpairs_vars_subset': "(fvpairs ` set (trpairs F D))  fvpairs F  fvpairs D"
using trpairs_vars_subset[of _ F D] by blast


lemma tr_trms_subset:
  "A'  set (tr A D)  trmsst A'  trmssst A  pair ` setopssst A  pair ` set D"
proof (induction A D arbitrary: A' rule: tr.induct)
  case 1 thus ?case by simp
next
  case (2 t A D)
  then obtain A'' where A'': "A' = send⟨tst#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "2.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (3 t A D)
  then obtain A'' where A'': "A' = receive⟨tst#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "3.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (4 ac t t' A D)
  then obtain A'' where A'': "A' = ac: t  t'st#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "4.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (5 t s A D)
  hence "A'  set (tr A (List.insert (t,s) D))" by simp
  hence "trmsst A'  trmssst A  pair ` setopssst A  pair ` set (List.insert (t, s) D)"
    by (metis "5.IH")
  thus ?case by (auto simp add: setopssst_def)
next
  case (6 t s A D)
  from 6 obtain Di A'' B C where A'':
      "Di  set (subseqs D)" "A''  set (tr A [dD. d  set Di])" "A' = (B@C)@A''"
      "B = map (λd. check: (pair (t,s))  (pair d)st) Di"
      "C = map (λd. Inequality [] [(pair (t,s) , pair d)]) [dD. d  set Di]"
    by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set [dD. d  set Di]"
    by (metis "6.IH")
  hence "trmsst A''  trmssst (Delete t s#A)  pair ` setopssst (Delete t s#A)  pair ` set D"
    by (auto simp add: setopssst_def)
  moreover have "trmsst (B@C)  insert (pair (t,s)) (pair ` set D)"
    using A''(4,5) subseqs_set_subset[OF A''(1)] by auto
  moreover have "pair (t,s)  pair ` setopssst (Delete t s#A)" by (simp add: setopssst_def)
  ultimately show ?case using A''(3) trmsst_append[of "B@C" A'] by auto
next
  case (7 ac t s A D)
  from 7 obtain d A'' where A'':
      "d  set D" "A''  set (tr A D)"
      "A' = ac: (pair (t,s))  (pair d)st#A''"
    by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "7.IH")
  moreover have "trmsst A' = {pair (t,s), pair d}  trmsst A''"
    using A''(1,3) by auto
  ultimately show ?case using A''(1) by (auto simp add: setopssst_def)
next
  case (8 X F F' A D)
  from 8 obtain A'' where A'':
      "A''  set (tr A D)" "A' = (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))@A''"
    by atomize_elim auto

  define B where "B  (trmspairs ` set (trpairs F' D))"

  have "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis A''(1) "8.IH")
  hence "trmsst A'  B  trmspairs F  trmssst A  pair ` setopssst A  pair ` set D"
    using A'' B_def by auto
  moreover have "B  pair ` set F'  pair ` set D"
    using trpairs_trms_subset'[of F' D] B_def by simp
  moreover have "pair ` setopssst (X⟨∨≠: F ∨∉: F'#A) = pair ` set F'  pair ` setopssst A"
    by (auto simp add: setopssst_def)
  ultimately show ?case by auto
qed

lemma tr_vars_subset:
  assumes "A'  set (tr A D)"
  shows "fvst A'  fvsst A  ((t,t')  set D. fv t  fv t')" (is ?P)
  and "bvarsst A'  bvarssst A" (is ?Q)
proof -
  show ?P using assms
  proof (induction A arbitrary: A' D rule: strand_sem_stateful_induct)
    case (ConsIn A' D ac t s A)
    then obtain A'' d where *:
        "d  set D" "A' = ac: (pair (t,s))  (pair d)st#A''"
        "A''  set (tr A D)"
      by atomize_elim auto
    hence "fvst A''  fvsst A  ((t,t')set D. fv t  fv t')" by (metis ConsIn.IH)
    thus ?case using * unfolding pair_def by auto
  next
    case (ConsDel A' D t s A)
    define Dfv where "Dfv  λD::('fun,'var) dbstatelist. ((t,t')set D. fv t  fv t')"
    define fltD where "fltD  λDi. filter (λd. d  set Di) D"
    define constr where
      "constr  λDi. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                      (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) (fltD Di))"
    from ConsDel obtain A'' Di where *:
        "Di  set (subseqs D)" "A' = (constr Di)@A''" "A''  set (tr A (fltD Di))"
      unfolding constr_def fltD_def by atomize_elim auto
    hence "fvst A''  fvsst A  Dfv (fltD Di)"
      unfolding Dfv_def constr_def fltD_def by (metis ConsDel.IH)
    moreover have "Dfv (fltD Di)  Dfv D" unfolding Dfv_def constr_def fltD_def by auto
    moreover have "Dfv Di  Dfv D"
      using subseqs_set_subset(1)[OF *(1)] unfolding Dfv_def constr_def fltD_def by fast
    moreover have "fvst (constr Di)  fv t  fv s  (Dfv Di  Dfv (fltD Di))"
      unfolding Dfv_def constr_def fltD_def pair_def by auto
    moreover have "fvsst (Delete t s#A) = fv t  fv s  fvsst A" by auto
    moreover have "fvst A' = fvst (constr Di)  fvst A''" using * by force
    ultimately have "fvst A'  fvsst (Delete t s#A)  Dfv D" by auto
    thus ?case unfolding Dfv_def fltD_def constr_def by simp
  next
    case (ConsNegChecks A' D X F F' A)
    then obtain A'' where A'':
        "A''  set (tr A D)" "A' = (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))@A''"
      by atomize_elim auto

    define B where "B  (fvpairs ` set (trpairs F' D))"

    have 1: "fvst (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))  (B  fvpairs F) - set X"
      unfolding B_def by auto

    have 2: "B  fvpairs F'  fvpairs D"
      using trpairs_vars_subset'[of F' D]
      unfolding B_def by simp

    have "fvst A'  ((fvpairs F'  fvpairs D  fvpairs F) - set X)  fvst A''"
      using 1 2 A''(2) by fastforce
    thus ?case using ConsNegChecks.IH[OF A''(1)] by auto
  qed fastforce+

  show ?Q using assms by (induct A arbitrary: A' D rule: strand_sem_stateful_induct) fastforce+
qed

lemma tr_vars_disj:
  assumes "A'  set (tr A D)" "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
    and "fvsst A  bvarssst A = {}"
  shows "fvst A'  bvarsst A' = {}"
using assms tr_vars_subset by fast


lemma tfrsstp_alt_def:
  "list_all tfrsstp S =
    ((ac t t'. Equality ac t t'  set S  (δ. Unifier δ t t')  Γ t = Γ t') 
     (X F F'. NegChecks X F F'  set S  (
        (F' = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)) 
        (f T. Fun f T  subtermsset (trmspairs F  pair ` set F') 
                  T = []  (s  set T. s  Var ` set X)))))"
  (is "?P S = ?Q S")
proof
  show "?P S  ?Q S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp

  show "?Q S  ?P S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma tfrsst_Nil[simp]: "tfrsst []"
by (simp add: tfrsst_def setopssst_def)

lemma tfrsst_append: "tfrsst (A@B)  tfrsst A"
proof -
  assume assms: "tfrsst (A@B)"
  let ?M = "trmssst A  pair ` setopssst A"
  let ?N = "trmssst (A@B)  pair ` setopssst (A@B)"
  let ?P = "λt t'. x  fv t  fv t'. a. Γ (Var x) = Var a"
  let ?Q = "λX t t'. X = []  (x  (fv t  fv t')-set X. a. Γ (Var x) = Var a)"
  have *: "SMP ?M - Var`𝒱  SMP ?N - Var`𝒱" "?M  ?N"
    using SMP_mono[of ?M ?N] setopssst_append[of A B]
    by auto
  { fix s t assume **: "tfrset ?N" "s  SMP ?M - Var`𝒱" "t  SMP ?M - Var`𝒱" "(δ. Unifier δ s t)"
    hence "s  SMP ?N - Var`𝒱" "t  SMP ?N - Var`𝒱" using * by auto
    hence "Γ s = Γ t" using **(1,4) unfolding tfrset_def by blast
  } moreover have "t  ?N. wftrm t  t  ?M. wftrm t" using * by blast
  ultimately have "tfrset ?N  tfrset ?M" unfolding tfrset_def by blast
  hence "tfrset ?M" using assms unfolding tfrsst_def by metis
  thus "tfrsst A" using assms unfolding tfrsst_def by simp
qed

lemma tfrsst_append': "tfrsst (A@B)  tfrsst B"
proof -
  assume assms: "tfrsst (A@B)"
  let ?M = "trmssst B  pair ` setopssst B"
  let ?N = "trmssst (A@B)  pair ` setopssst (A@B)"
  let ?P = "λt t'. x  fv t  fv t'. a. Γ (Var x) = Var a"
  let ?Q = "λX t t'. X = []  (x  (fv t  fv t')-set X. a. Γ (Var x) = Var a)"
  have *: "SMP ?M - Var`𝒱  SMP ?N - Var`𝒱" "?M  ?N"
    using SMP_mono[of ?M ?N] setopssst_append[of A B]
    by auto
  { fix s t assume **: "tfrset ?N" "s  SMP ?M - Var`𝒱" "t  SMP ?M - Var`𝒱" "(δ. Unifier δ s t)"
    hence "s  SMP ?N - Var`𝒱" "t  SMP ?N - Var`𝒱" using * by auto
    hence "Γ s = Γ t" using **(1,4) unfolding tfrset_def by blast
  } moreover have "t  ?N. wftrm t  t  ?M. wftrm t" using * by blast
  ultimately have "tfrset ?N  tfrset ?M" unfolding tfrset_def by blast
  hence "tfrset ?M" using assms unfolding tfrsst_def by metis
  thus "tfrsst B" using assms unfolding tfrsst_def by simp
qed

lemma tfrsst_cons: "tfrsst (a#A)  tfrsst A"
using tfrsst_append'[of "[a]" A] by simp

lemma tfrsstp_subst:
  assumes s: "tfrsstp s"
    and θ: "wtsubst θ" "wftrms (subst_range θ)" "set (bvarssstp s)  range_vars θ = {}"
  shows "tfrsstp (s sstp θ)"
proof (cases s)
  case (Equality a t t')
  thus ?thesis
  proof (cases "δ. Unifier δ (t  θ) (t'  θ)")
    case True
    hence "δ. Unifier δ t t'" by (metis subst_subst_compose[of _ θ])
    moreover have "Γ t = Γ (t  θ)" "Γ t' = Γ (t'  θ)" by (metis wt_subst_trm''[OF assms(2)])+
    ultimately have "Γ (t  θ) = Γ (t'  θ)" using s Equality by simp
    thus ?thesis using Equality True by simp
  qed simp
next
  case (NegChecks X F G)
  let ?P = "λF G. G = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)"
  let ?Q = "λF G. f T. Fun f T  subtermsset (trmspairs F  pair ` set G) 
                          T = []  (s  set T. s  Var ` set X)"
  let  = "rm_vars (set X) θ"

  have "?P F G  ?Q F G" using NegChecks assms(1) by simp
  hence "?P (F pairs ) (G pairs )  ?Q (F pairs ) (G pairs )"
  proof
    assume *: "?P F G"
    have "G pairs  = []" using * by simp
    moreover have "a. Γ (Var x) = TAtom a" when x: "x  fvpairs (F pairs ) - set X" for x
    proof -
      obtain t t' where t: "(t,t')  set (F pairs )" "x  fv t  fv t' - set X"
        using x(1) by auto
      then obtain u u' where u: "(u,u')  set F" "u   = t" "u'   = t'"
        unfolding subst_apply_pairs_def by auto
      obtain y where y: "y  fv u  fv u' - set X" "x  fv ( y)"
        using t(2) u(2,3) rm_vars_fv_obtain by fast
      hence a: "a. Γ (Var y) = TAtom a" using u * by auto
      
      have a': "Γ (Var y) = Γ ( y)"
        using wt_subst_trm''[OF wt_subst_rm_vars[OF θ(1), of "set X"], of "Var y"]
        by simp

      have "(z.  y = Var z)  (c.  y = Fun c [])"
      proof (cases " y  subst_range θ")
        case True thus ?thesis
          using a a' θ(2) const_type_inv_wf
          by (cases " y") fastforce+
      qed fastforce
      hence " y = Var x" using y(2) by fastforce
      hence "Γ (Var x) = Γ (Var y)" using a' by simp
      thus ?thesis using a by presburger
    qed
    ultimately show ?thesis by simp
  next
    assume *: "?Q F G"
    have **: "set X  range_vars  = {}"
      using θ(3) NegChecks rm_vars_img_fv_subset[of "set X" θ] by auto
    have "?Q (F pairs ) (G pairs )"
      using ineq_subterm_inj_cond_subst[OF ** *]
            trmspairs_subst[of F "rm_vars (set X) θ"]
            subst_apply_pairs_pair_image_subst[of G "rm_vars (set X) θ"]
      by (metis (no_types, lifting) image_Un)
    thus ?thesis by simp
  qed
  thus ?thesis using NegChecks by simp
qed simp_all

lemma tfrsstp_all_wt_subst_apply:
  assumes S: "list_all tfrsstp S"
    and θ: "wtsubst θ" "wftrms (subst_range θ)" "bvarssst S  range_vars θ = {}"
  shows "list_all tfrsstp (S sst θ)"
proof -
  have "set (bvarssstp s)  range_vars θ = {}" when "s  set S" for s
    using that θ(3) unfolding bvarssst_def range_vars_alt_def by fastforce
  thus ?thesis
    using tfrsstp_subst[OF _ θ(1,2)] S
    unfolding list_all_iff
    by (auto simp add: subst_apply_stateful_strand_def)
qed

lemma tfr_setops_if_tfr_trms:
  assumes "Pair  (funs_term ` SMP (trmssst S))"
    and "p. Ana (pair p) = ([], [])"
    and "s  pair ` setopssst S. t  pair ` setopssst S. (δ. Unifier δ s t)  Γ s = Γ t"
    and "s  pair ` setopssst S. t  pair ` setopssst S.
          (σ θ ρ. wtsubst σ  wtsubst θ  wftrms (subst_range σ)  wftrms (subst_range θ) 
                   Unifier ρ (s  σ) (t  θ))
           (δ. Unifier δ s t)"
    and tfr: "tfrset (trmssst S)"
  shows "tfrset (trmssst S  pair ` setopssst S)"
proof -
  have 0: "t  SMP (trmssst S) - range Var  t  SMP (pair ` setopssst S) - range Var"
    when "t  SMP (trmssst S  pair ` setopssst S) - range Var" for t
    using that SMP_union by blast

  have 1: "s  SMP (trmssst S) - range Var"
      when st: "s  SMP (pair ` setopssst S) - range Var"
               "t  SMP (trmssst S) - range Var"
               "δ. Unifier δ s t"
         for s t
  proof -
    have "(δ. s  pair ` setopssst S set δ)  s  SMP (trmssst S) - range Var"
      using st setops_SMP_cases[of s S] assms(2) by blast
    moreover {
      fix δ assume δ: "s  pair ` setopssst S set δ"
      then obtain s' where s': "s'  pair ` setopssst S" "s = s'  δ" by blast
      then obtain u u' where u: "s' = Fun Pair [u,u']"
        using setopssst_are_pairs[of s'] unfolding pair_def by fast
      hence *: "s = Fun Pair [u  δ, u'  δ]" using δ s' by simp

      obtain f T where fT: "t = Fun f T" using st(2) by (cases t) auto
      hence "f  Pair" using st(2) assms(1) by auto
      hence False using st(3) * fT s' u by fast
    } ultimately show ?thesis by meson
  qed
  
  have 2: "Γ s = Γ t"
      when "s  SMP (trmssst S) - range Var"
           "t  SMP (trmssst S) - range Var"
           "δ. Unifier δ s t"
       for s t
    using that tfr unfolding tfrset_def by blast
  
  have 3: "Γ s = Γ t"
      when st: "s  SMP (pair ` setopssst S) - range Var"
               "t  SMP (pair ` setopssst S) - range Var"
               "δ. Unifier δ s