Theory Strands_and_Constraints

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

section ‹Strands and Symbolic Intruder Constraints›
theory Strands_and_Constraints
imports Messages More_Unification Intruder_Deduction
begin

subsection ‹Constraints, Strands and Related Definitions›
datatype poscheckvariant = Assign ("assign") | Check ("check")

text ‹
  A strand (or constraint) step is either a message transmission (either a message being sent Send›
  or being received Receive›) or a check on messages (a positive check Equality›---which can be
  either an "assignment" or just a check---or a negative check Inequality›)
›
datatype (funsstp: 'a, varsstp: 'b) strand_step =
  Send       "('a,'b) term list" ("send⟨_st" 80)
| Receive    "('a,'b) term list" ("receive⟨_st" 80)
| Equality   poscheckvariant "('a,'b) term" "('a,'b) term" ("_: _  _st" [80,80])
| Inequality (bvarsstp: "'b list") "(('a,'b) term × ('a,'b) term) list" ("_⟨∨≠: _st" [80,80])
where
  "bvarsstp (Send _) = []"
| "bvarsstp (Receive _) = []"
| "bvarsstp (Equality _ _ _) = []"

abbreviation "Send1 t  Send [t]"
abbreviation "Receive1 t  Receive [t]"

text ‹
  A strand is a finite sequence of strand steps (constraints and strands share the same datatype)
›
type_synonym ('a,'b) strand = "('a,'b) strand_step list"

type_synonym ('a,'b) strands = "('a,'b) strand set"

abbreviation "trmspairs F  (t,t')  set F. {t,t'}"

fun trmsstp::"('a,'b) strand_step  ('a,'b) terms" where
  "trmsstp (Send ts) = set ts"
| "trmsstp (Receive ts) = set ts"
| "trmsstp (Equality _ t t') = {t,t'}"
| "trmsstp (Inequality _ F) = trmspairs F"

lemma varsstp_unfold[simp]: "varsstp x = fvset (trmsstp x)  set (bvarsstp x)"
by (cases x) auto

text ‹The set of terms occurring in a strand›
definition trmsst where "trmsst S  (trmsstp ` set S)"

fun trms_liststp::"('a,'b) strand_step  ('a,'b) term list" where
  "trms_liststp (Send ts) = ts"
| "trms_liststp (Receive ts) = ts"
| "trms_liststp (Equality _ t t') = [t,t']"
| "trms_liststp (Inequality _ F) = concat (map (λ(t,t'). [t,t']) F)"

text ‹The set of terms occurring in a strand (list variant)›
definition trms_listst where "trms_listst S  remdups (concat (map trms_liststp S))"

text ‹The set of variables occurring in a sent message›
definition fvsnd::"('a,'b) strand_step  'b set" where
  "fvsnd x  case x of Send t  fvset (set t) | _  {}"

text ‹The set of variables occurring in a received message›
definition fvrcv::"('a,'b) strand_step  'b set" where
  "fvrcv x  case x of Receive t  fvset (set t) | _  {}"

text ‹The set of variables occurring in an equality constraint›
definition fveq::"poscheckvariant  ('a,'b) strand_step  'b set" where
  "fveq ac x  case x of Equality ac' s t  if ac = ac' then fv s  fv t else {} | _  {}"

text ‹The set of variables occurring at the left-hand side of an equality constraint›
definition fv_leq::"poscheckvariant  ('a,'b) strand_step  'b set" where
  "fv_leq ac x  case x of Equality ac' s t  if ac = ac' then fv s else {} | _  {}"

text ‹The set of variables occurring at the right-hand side of an equality constraint›
definition fv_req::"poscheckvariant  ('a,'b) strand_step  'b set" where
  "fv_req ac x  case x of Equality ac' s t  if ac = ac' then fv t else {} | _  {}"

text ‹The free variables of inequality constraints›
definition fvineq::"('a,'b) strand_step  'b set" where
  "fvineq x  case x of Inequality X F  fvpairs F - set X | _  {}"

fun fvstp::"('a,'b) strand_step  'b set" where
  "fvstp (Send t) = fvset (set t)"
| "fvstp (Receive t) = fvset (set t)"
| "fvstp (Equality _ t t') = fv t  fv t'"
| "fvstp (Inequality X F) = ((t,t')  set F. fv t  fv t') - set X"

text ‹The set of free variables of a strand›
definition fvst::"('a,'b) strand  'b set" where
  "fvst S  (set (map fvstp S))"

text ‹The set of bound variables of a strand›
definition bvarsst::"('a,'b) strand  'b set" where
  "bvarsst S  (set (map (set  bvarsstp) S))"

text ‹The set of all variables occurring in a strand›
definition varsst::"('a,'b) strand  'b set" where
  "varsst S  (set (map varsstp S))"

abbreviation wfrestrictedvarsstp::"('a,'b) strand_step  'b set" where
  "wfrestrictedvarsstp x 
    case x of Inequality _ _  {} | Equality Check _ _  {} | _  varsstp x"

text ‹The variables of a strand whose occurrences might be restricted by well-formedness constraints›
definition wfrestrictedvarsst::"('a,'b) strand  'b set" where
  "wfrestrictedvarsst S  (set (map wfrestrictedvarsstp S))"

abbreviation wfvarsoccsstp where
  "wfvarsoccsstp x  case x of Send t  fvset (set t) | Equality Assign s t  fv s | _  {}"

text ‹The variables of a strand that occur in sent messages or in assignments›
definition wfvarsoccsst where
  "wfvarsoccsst S  (set (map wfvarsoccsstp S))"

text ‹The variables occurring at the right-hand side of assignment steps›
fun assignment_rhsst where
  "assignment_rhsst [] = {}"
| "assignment_rhsst (Equality Assign t t'#S) = insert t' (assignment_rhsst S)"
| "assignment_rhsst (x#S) = assignment_rhsst S"

text ‹The set of function symbols occurring in a strand›
definition funsst::"('a,'b) strand  'a set" where
  "funsst S  (set (map funsstp S))"

fun subst_apply_strand_step::"('a,'b) strand_step  ('a,'b) subst  ('a,'b) strand_step"
  (infix "stp" 51) where
  "Send t stp θ = Send (t list θ)"
| "Receive t stp θ = Receive (t list θ)"
| "Equality a t t' stp θ = Equality a (t  θ) (t'  θ)"
| "Inequality X F stp θ = Inequality X (F pairs rm_vars (set X) θ)"

text ‹Substitution application for strands›
definition subst_apply_strand::"('a,'b) strand  ('a,'b) subst  ('a,'b) strand"
  (infix "st" 51) where
  "S st θ  map (λx. x stp θ) S"

text ‹The semantics of inequality constraints›
definition
  "ineq_model (::('a,'b) subst) X F 
      (δ. subst_domain δ = set X  ground (subst_range δ)  
              ((t,t')  set F. t  δ s   t'  δ s ))"

fun simplestp where
  "simplestp (Receive t) = True"
| "simplestp (Send [Var v]) = True"
| "simplestp (Inequality X F) = (. ineq_model  X F)"
| "simplestp _ = False"

text ‹Simple constraints›
definition simple where "simple S  list_all simplestp S"

text ‹The intruder knowledge of a constraint›
fun ikst::"('a,'b) strand  ('a,'b) terms" where
  "ikst [] = {}"
| "ikst (Receive t#S) = set t  (ikst S)"
| "ikst (_#S) = ikst S"

text ‹Strand well-formedness›
fun wfst::"'b set  ('a,'b) strand  bool" where
  "wfst V [] = True"
| "wfst V (Receive ts#S) = (fvset (set ts)  V  wfst V S)"
| "wfst V (Send ts#S) = wfst (V  fvset (set ts)) S"
| "wfst V (Equality Assign s t#S) = (fv t  V  wfst (V  fv s) S)"
| "wfst V (Equality Check s t#S) = wfst V S"
| "wfst V (Inequality _ _#S) = wfst V S"

text ‹Well-formedness of constraint states›
definition wfconstr::"('a,'b) strand  ('a,'b) subst  bool" where
  "wfconstr S θ  (wfsubst θ  wfst {} S  subst_domain θ  varsst S = {} 
                  range_vars θ  bvarsst S = {}  fvst S  bvarsst S = {})"

declare trmsst_def[simp]
declare fvsnd_def[simp]
declare fvrcv_def[simp]
declare fveq_def[simp]
declare fv_leq_def[simp]
declare fv_req_def[simp]
declare fvineq_def[simp]
declare fvst_def[simp]
declare varsst_def[simp]
declare bvarsst_def[simp]
declare wfrestrictedvarsst_def[simp]
declare wfvarsoccsst_def[simp]

lemmas wfst_induct = wfst.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsEq2 ConsIneq]
lemmas ikst_induct = ikst.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsIneq]
lemmas assignment_rhsst_induct = assignment_rhsst.induct[case_names Nil ConsEq2 ConsSnd ConsRcv ConsEq ConsIneq]
  

subsubsection ‹Lexicographical measure on strands›
definition sizest::"('a,'b) strand  nat" where
  "sizest S  size_list (λx. Max (insert 0 (size ` trmsstp x))) S"

definition measurest::"((('a, 'b) strand × ('a,'b) subst) × ('a, 'b) strand × ('a,'b) subst) set"
where
  "measurest  measures [λ(S,θ). card (fvst S), λ(S,θ). sizest S]"

lemma measurest_alt_def:
  "((s,x),(t,y))  measurest =
      (card (fvst s) < card (fvst t)  (card (fvst s) = card (fvst t)  sizest s < sizest t))"
by (simp add: measurest_def sizest_def)

lemma measurest_trans: "trans measurest"
by (simp add: trans_def measurest_def sizest_def)


subsubsection ‹Some lemmata›
lemma trms_listst_is_trmsst: "trmsst S = set (trms_listst S)"
unfolding trmsst_def trms_listst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma subst_apply_strand_step_def:
  "s stp θ = (case s of
    Send t  Send (t list θ)
  | Receive t  Receive (t list θ)
  | Equality a t t'  Equality a (t  θ) (t'  θ)
  | Inequality X F  Inequality X (F pairs rm_vars (set X) θ))"
by (cases s) simp_all

lemma subst_apply_strand_nil[simp]: "[] st δ = []"
unfolding subst_apply_strand_def by simp

lemma finite_funsstp[simp]: "finite (funsstp x)" by (cases x) auto
lemma finite_funsst[simp]: "finite (funsst S)" unfolding funsst_def by simp
lemma finite_trmspairs[simp]: "finite (trmspairs x)" by (induct x) auto
lemma finite_trmsstp[simp]: "finite (trmsstp x)" by (cases x) auto
lemma finite_varsstp[simp]: "finite (varsstp x)" by auto
lemma finite_bvarsstp[simp]: "finite (set (bvarsstp x))" by rule
lemma finite_fvsnd[simp]: "finite (fvsnd x)" by (cases x) auto
lemma finite_fvrcv[simp]: "finite (fvrcv x)" by (cases x) auto
lemma finite_fvstp[simp]: "finite (fvstp x)" by (cases x) auto
lemma finite_varsst[simp]: "finite (varsst S)" by simp
lemma finite_bvarsst[simp]: "finite (bvarsst S)" by simp
lemma finite_fvst[simp]: "finite (fvst S)" by simp

lemma finite_wfrestrictedvarsstp[simp]: "finite (wfrestrictedvarsstp x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfrestrictedvarsst[simp]: "finite (wfrestrictedvarsst S)"
using finite_wfrestrictedvarsstp by auto

lemma finite_wfvarsoccsstp[simp]: "finite (wfvarsoccsstp x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfvarsoccsst[simp]: "finite (wfvarsoccsst S)"
using finite_wfvarsoccsstp by auto

lemma finite_ikst[simp]: "finite (ikst S)"
by (induct S rule: ikst.induct) simp_all

lemma finite_assignment_rhsst[simp]: "finite (assignment_rhsst S)"
by (induct S rule: assignment_rhsst.induct) simp_all

lemma ikst_is_rcv_set: "ikst A = {t | ts t. Receive ts  set A  t  set ts}"
by (induct A rule: ikst.induct) auto

lemma ikst_snoc_no_receive_eq:
  assumes "ts. a = receive⟨tsst"
  shows "ikst (A@[a]) set  = ikst A set "
using assms unfolding ikst_is_rcv_set
by (metis (no_types, lifting) Un_iff append_Nil2 set_ConsD set_append)

lemma ikstD[dest]: "t  ikst S  ts. t  set ts  Receive ts  set S"
by (induct S rule: ikst.induct) auto

lemma ikstD'[dest]: "t  ikst S  t  trmsst S"
by (induct S rule: ikst.induct) auto

lemma ikstD''[dest]: "t  subtermsset (ikst S)  t  subtermsset (trmsst S)"
by (induct S rule: ikst.induct) auto

lemma ikst_subterm_exD:
  assumes "t  ikst S"
  shows "x  set S. t  subtermsset (trmsstp x)"
using assms ikstD by force

lemma assignment_rhsstD[dest]: "t  assignment_rhsst S  t'. Equality Assign t' t  set S"
by (induct S rule: assignment_rhsst.induct) auto

lemma assignment_rhsstD'[dest]: "t  subtermsset (assignment_rhsst S)  t  subtermsset (trmsst S)"
by (induct S rule: assignment_rhsst.induct) auto

lemma bvarsst_split: "bvarsst (S@S') = bvarsst S  bvarsst S'"
unfolding bvarsst_def by auto

lemma bvarsst_singleton: "bvarsst [x] = set (bvarsstp x)"
unfolding bvarsst_def by auto

lemma strand_fv_bvars_disjointD:
  assumes "fvst S  bvarsst S = {}" "Inequality X F  set S"
  shows "set X  bvarsst S" "fvpairs F - set X  fvst S"
using assms by (induct S) fastforce+

lemma strand_fv_bvars_disjoint_unfold:
  assumes "fvst S  bvarsst S = {}" "Inequality X F  set S" "Inequality Y G  set S"
  shows "set Y  (fvpairs F - set X) = {}"
proof -
  have "set X  bvarsst S" "set Y  bvarsst S"
       "fvpairs F - set X  fvst S" "fvpairs G - set Y  fvst S"
    using strand_fv_bvars_disjointD[OF assms(1)] assms(2,3) by auto
  thus ?thesis using assms(1) by fastforce
qed

lemma strand_subst_hom[iff]:
  "(S@S') st θ = (S st θ)@(S' st θ)" "(x#S) st θ = (x stp θ)#(S st θ)"
unfolding subst_apply_strand_def by auto

lemma strand_subst_comp: "range_vars δ  bvarsst S = {}  S st δ s θ = ((S st δ) st θ)"
proof (induction S)
  case (Cons x S)
  have *: "range_vars δ  bvarsst S = {}" "range_vars δ  (set (bvarsstp x)) = {}"
    using Cons bvarsst_split[of "[x]" S] append_Cons inf_sup_absorb
    by (metis (no_types, lifting) Int_iff Un_commute disjoint_iff_not_equal self_append_conv2,
        metis append_self_conv2 bvarsst_singleton inf_bot_right inf_left_commute) 
  hence IH: "S st δ s θ = (S st δ) st θ" using Cons.IH by auto
  have "(x#S st δ s θ) = (x stp δ s θ)#(S st δ s θ)" by (metis strand_subst_hom(2))
  hence "... = (x stp δ s θ)#((S st δ) st θ)" by (metis IH)
  hence "... = ((x stp δ) stp θ)#((S st δ) st θ)" using rm_vars_comp[OF *(2)]
  proof (induction x)
    case (Inequality X F) thus ?case
      by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
  qed (simp_all add: subst_apply_strand_step_def)
  thus ?case using IH by auto
qed (simp add: subst_apply_strand_def)

lemma strand_substI[intro]:
  "subst_domain θ  fvst S = {}  S st θ = S"
  "subst_domain θ  varsst S = {}  S st θ = S"
proof -
  show "subst_domain θ  varsst S = {}  S st θ = S"
  proof (induction S)
    case (Cons x S)
    hence "S st θ = S" by auto
    moreover have "varsstp x  subst_domain θ = {}" using Cons.prems by auto
    hence "x stp θ = x"
    proof (induction x)
      case (Send ts) thus ?case by (induct ts) auto
    next
      case (Receive ts) thus ?case by (induct ts) auto
    next
      case (Inequality X F) thus ?case
        by (induct F) (force simp add: subst_apply_pairs_def)+
    qed auto
    ultimately show ?case by simp
  qed (simp add: subst_apply_strand_def)

  show "subst_domain θ  fvst S = {}  S st θ = S"
  proof (induction S)
    case (Cons x S)
    hence "S st θ = S" by auto
    moreover have "fvstp x  subst_domain θ = {}"
      using Cons.prems by auto
    hence "x stp θ = x"
    proof (induction x)
      case (Send ts) thus ?case by (induct ts) auto
    next
      case (Receive ts) thus ?case by (induct ts) auto
    next
      case (Inequality X F) thus ?case
        by (induct F) (force simp add: subst_apply_pairs_def)+
    qed auto
    ultimately show ?case by simp
  qed (simp add: subst_apply_strand_def)
qed

lemma strand_substI':
  "fvst S = {}  S st θ = S"
  "varsst S = {}  S st θ = S"
by (metis inf_bot_right strand_substI(1),
    metis inf_bot_right strand_substI(2))

lemma strand_subst_set: "(set (S st θ)) = ((λx. x stp θ) ` (set S))"
by (auto simp add: subst_apply_strand_def)

lemma strand_map_inv_set_snd_rcv_subst:
  assumes "finite (M::('a,'b) terms)"
  shows "set ((map Send1 (inv set M)) st θ) = Send1 ` (M set θ)" (is ?A)
        "set ((map Receive1 (inv set M)) st θ) = Receive1 ` (M set θ)" (is ?B)
proof -
  { fix f::"('a,'b) term  ('a,'b) strand_step"
    assume f: "f = Send1  f = Receive1"
    from assms have "set ((map f (inv set M)) st θ) = f ` (M set θ)"
    proof (induction rule: finite_induct)
      case empty thus ?case unfolding inv_def by auto
    next
      case (insert m M)
      have "set (map f (inv set (insert m M)) st θ) =
            insert (f m stp θ) (set (map f (inv set M) st θ))"
        by (simp add: insert.hyps(1) inv_set_fset subst_apply_strand_def)
      thus ?case using f insert.IH by auto
    qed
  }
  thus "?A" "?B" by auto
qed

lemma strand_ground_subst_vars_subset:
  assumes "ground (subst_range θ)" shows "varsst (S st θ)  varsst S"
proof (induction S)
  case (Cons x S)
  have "varsstp (x stp θ)  varsstp x" using ground_subst_fv_subset[OF assms] 
  proof (cases x)
    case (Inequality X F)
    let  = "rm_vars (set X) θ"
    have "fvpairs (F pairs )  fvpairs F"
    proof (induction F)
      case (Cons f F)
      obtain t t' where f: "f = (t,t')" by (metis surj_pair)
      hence "fvpairs (f#F pairs ) = fv (t  )  fv (t'  )  fvpairs (F pairs )"
            "fvpairs (f#F) = fv t  fv t'  fvpairs F"
        by (auto simp add: subst_apply_pairs_def)
      thus ?case
        using ground_subst_fv_subset[OF ground_subset[OF rm_vars_img_subset assms, of "set X"]]
              Cons.IH
        by (metis (no_types, lifting) Un_mono)
    qed (simp add: subst_apply_pairs_def)
    moreover have
        "varsstp (x stp θ) = fvpairs (F pairs rm_vars (set X) θ)  set X"
        "varsstp x = fvpairs F  set X"
      using Inequality
      by (auto simp add: subst_apply_pairs_def)
    ultimately show ?thesis by auto
  qed auto
  thus ?case using Cons.IH by auto
qed (simp add: subst_apply_strand_def)

lemma ik_union_subset: "(P ` ikst S)  (x  (set S). (P ` trmsstp x))"
by (induct S rule: ikst.induct) auto

lemma ik_snd_empty[simp]: "ikst (map Send X) = {}"
by (induct "map Send X" arbitrary: X rule: ikst.induct) auto

lemma ik_snd_empty'[simp]: "ikst [Send t] = {}" by simp

lemma ik_append[iff]: "ikst (S@S') = ikst S  ikst S'" by (induct S rule: ikst.induct) auto

lemma ik_cons: "ikst (x#S) = ikst [x]  ikst S" using ik_append[of "[x]" S] by simp

lemma assignment_rhs_append[iff]: "assignment_rhsst (S@S') = assignment_rhsst S  assignment_rhsst S'"
by (induct S rule: assignment_rhsst.induct) auto

lemma eqs_rcv_map_empty: "assignment_rhsst (map Receive M) = {}"
by auto

lemma ik_rcv_map: assumes "ts  set L" shows "set ts  ikst (map Receive L)"
proof -
  { fix L L' 
    have "set ts  ikst [Receive ts]" by auto
    hence "set ts  ikst (map Receive L@Receive ts#map Receive L')" using ik_append by auto
    hence "set ts  ikst (map Receive (L@ts#L'))" by auto
  }
  thus ?thesis using assms split_list_last by force 
qed

lemma ik_subst: "ikst (S st δ) = ikst S set δ"
by (induct rule: ikst_induct) auto

lemma ik_rcv_map': assumes "t  ikst (map Receive L)" shows "ts  set L. t  set ts"
using assms by force

lemma ik_append_subset[simp]: "ikst S  ikst (S@S')" "ikst S'  ikst (S@S')"
by (induct S rule: ikst.induct) auto

lemma assignment_rhs_append_subset[simp]:
  "assignment_rhsst S  assignment_rhsst (S@S')"
  "assignment_rhsst S'  assignment_rhsst (S@S')"
by (induct S rule: assignment_rhsst.induct) auto

lemma trmsst_cons: "trmsst (x#S) = trmsstp x  trmsst S" by simp

lemma trm_strand_subst_cong:
  "t  trmsst S  t  δ  trmsst (S st δ)
     (X F. Inequality X F  set S  t  rm_vars (set X) δ  trmsst (S st δ))"
    (is "t  trmsst S  ?P t δ S")
  "t  trmsst (S st δ)  (t'. t = t'  δ  t'  trmsst S)
     (X F. Inequality X F  set S  (t'  trmspairs F. t = t'  rm_vars (set X) δ))"
    (is "t  trmsst (S st δ)  ?Q t δ S")
proof -
  show "t  trmsst S  ?P t δ S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t  trmsst S")
      case True
      hence "?P t δ S" using Cons by simp
      thus ?thesis
        by (cases x)
           (metis (no_types, lifting) Un_iff list.set_intros(2) strand_subst_hom(2) trmsst_cons)+
    next
      case False
      hence "t  trmsstp x" using Cons.prems by auto
      thus ?thesis
      proof (induction x)
        case (Inequality X F)
        hence "t  rm_vars (set X) δ  trmsstp (Inequality X F stp δ)"
          by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
        thus ?case by fastforce
      qed (auto simp add: subst_apply_strand_step_def)
    qed
  qed simp

  show "t  trmsst (S st δ)  ?Q t δ S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t  trmsst (S st δ)")
      case True
      hence "?Q t δ S" using Cons by simp
      thus ?thesis by (cases x) force+
    next
      case False
      hence "t  trmsstp (x stp δ)" using Cons.prems by auto
      thus ?thesis
      proof (induction x)
        case (Inequality X F)
        hence "t  trmsstp (Inequality X F) set rm_vars (set X) δ"
          by (induct F) (force simp add: subst_apply_pairs_def)+
        thus ?case by fastforce
      qed (auto simp add: subst_apply_strand_step_def)
    qed
  qed simp
qed


subsection ‹Lemmata: Free Variables of Strands›
lemma fv_trm_snd_rcv[simp]:
  "fvset (trmsstp (Send ts)) = fvset (set ts)" "fvset (trmsstp (Receive ts)) = fvset (set ts)"
by simp_all

lemma in_strand_fv_subset: "x  set S  varsstp x  varsst S"
by fastforce

lemma in_strand_fv_subset_snd: "Send ts  set S  fvset (set ts)  (set (map fvsnd S))"
by fastforce

lemma in_strand_fv_subset_rcv: "Receive ts  set S  fvset (set ts)  (set (map fvrcv S))"
by fastforce

lemma fvsndE:
  assumes "v  (set (map fvsnd S))"
  obtains ts where "send⟨tsst  set S" "v  fvset (set ts)"
proof -
  have "ts. send⟨tsst  set S  v  fvset (set ts)"
    by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
              fvsnd_def strand_step.collapse(1))
  thus ?thesis by (metis that)
qed

lemma fvrcvE:
  assumes "v  (set (map fvrcv S))"
  obtains ts where "receive⟨tsst  set S" "v  fvset (set ts)"
proof -
  have "ts. receive⟨tsst  set S  v  fvset (set ts)"
    by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
              fvrcv_def strand_step.collapse(2))
  thus ?thesis by (metis that)
qed

lemma varsstpI[intro]: "x  fvstp s  x  varsstp s"
by (induct s rule: fvstp.induct) auto

lemma varsstI[intro]: "x  fvst S  x  varsst S" using varsstpI by fastforce

lemma fvst_subset_varsst[simp]: "fvst S  varsst S" using varsstI by force

lemma varsst_is_fvst_bvarsst: "varsst S = fvst S  bvarsst S"
proof (induction S)
  case (Cons x S) thus ?case
  proof (induction x)
    case (Inequality X F) thus ?case by (induct F) auto
  qed auto
qed simp

lemma fvstp_is_subterm_trmsstp: "x  fvstp a  Var x  subtermsset (trmsstp a)" 
using var_is_subterm by (cases a) force+

lemma fvst_is_subterm_trmsst: "x  fvst A  Var x  subtermsset (trmsst A)"
proof (induction A)
  case (Cons a A) thus ?case using fvstp_is_subterm_trmsstp by (cases "x  fvst A") auto
qed simp

lemma vars_st_snd_map: "varsst (map Send tss) = fvset (Fun f ` set tss)" by auto

lemma vars_st_rcv_map: "varsst (map Receive tss) = fvset (Fun f ` set tss)" by auto

lemma vars_snd_rcv_union:
  "varsstp x = fvsnd x  fvrcv x  fveq assign x  fveq check x  fvineq x  set (bvarsstp x)"
proof (cases x)
  case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_union:
  "fvstp x = fvsnd x  fvrcv x  fveq assign x  fveq check x  fvineq x"
proof (cases x)
  case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_empty[simp]: "fvsnd x = {}  fvrcv x = {}" by (cases x) simp_all

lemma vars_snd_rcv_strand[iff]:
  "varsst (S::('a,'b) strand) =
    ((set (map fvsnd S)))  ((set (map fvrcv S)))  ((set (map (fveq assign) S)))
     ((set (map (fveq check) S)))  ((set (map fvineq S)))  bvarsst S"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "s V. varsstp (s::('a,'b) strand_step)  V = 
                fvsnd s  fvrcv s  fveq assign s  fveq check s  fvineq s  set (bvarsstp s)  V"
    by (metis vars_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma fv_snd_rcv_strand[iff]:
  "fvst (S::('a,'b) strand) =
    ((set (map fvsnd S)))  ((set (map fvrcv S)))  ((set (map (fveq assign) S)))
     ((set (map (fveq check) S)))  ((set (map fvineq S)))"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "s V. fvstp (s::('a,'b) strand_step)  V = 
                fvsnd s  fvrcv s  fveq assign s  fveq check s  fvineq s  V"
    by (metis fv_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma vars_snd_rcv_strand2[iff]:
  "wfrestrictedvarsst (S::('a,'b) strand) =
    ((set (map fvsnd S)))  ((set (map fvrcv S)))  ((set (map (fveq assign) S)))"
by (induct S) (auto simp add: split: strand_step.split poscheckvariant.split)

lemma fv_snd_rcv_strand_subset[simp]:
  "(set (map fvsnd S))  fvst S" "(set (map fvrcv S))  fvst S"
  "(set (map (fveq ac) S))  fvst S" "(set (map fvineq S))  fvst S"
  "wfvarsoccsst S  fvst S"
proof -
  show "(set (map fvsnd S))  fvst S" "(set (map fvrcv S))  fvst S" "(set (map fvineq S))  fvst S"
    using fv_snd_rcv_strand[of S] by auto
  
  show "(set (map (fveq ac) S))  fvst S"
    by (induct S) (auto split: strand_step.split poscheckvariant.split)

  show "wfvarsoccsst S  fvst S"
    by (induct S) (auto split: strand_step.split poscheckvariant.split)
qed

lemma vars_snd_rcv_strand_subset2[simp]:
  "(set (map fvsnd S))  wfrestrictedvarsst S" "(set (map fvrcv S))  wfrestrictedvarsst S"
  "(set (map (fveq assign) S))  wfrestrictedvarsst S" "wfvarsoccsst S  wfrestrictedvarsst S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma wfrestrictedvarsst_subset_varsst: "wfrestrictedvarsst S  varsst S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma subst_sends_strand_step_fv_to_img: "fvstp (x stp δ)  fvstp x  range_vars δ" 
using subst_sends_fv_to_img[of _ δ]
proof (cases x)
  case (Inequality X F)
  let  = "rm_vars (set X) δ"
  have "fvpairs (F pairs )  fvpairs F  range_vars "
  proof (induction F)
    case (Cons f F) thus ?case
      using subst_sends_fv_to_img[of _ ]
      by (auto simp add: subst_apply_pairs_def)
  qed (auto simp add: subst_apply_pairs_def)
  hence "fvpairs (F pairs )  fvpairs F  range_vars δ"
    using rm_vars_img_subset[of "set X" δ] fv_set_mono
    unfolding range_vars_alt_def by blast+
  thus ?thesis using Inequality by (auto simp add: subst_apply_strand_step_def)
qed (auto simp add: subst_apply_strand_step_def)

lemma subst_sends_strand_fv_to_img: "fvst (S st δ)  fvst S  range_vars δ" 
proof (induction S)
  case (Cons x S)
  have *: "fvst (x#S st δ) = fvstp (x stp δ)  fvst (S st δ)"
          "fvst (x#S)  range_vars δ = fvstp x  fvst S  range_vars δ"
    by auto
  thus ?case using Cons.IH subst_sends_strand_step_fv_to_img[of x δ] by auto
qed simp

lemma ineq_apply_subst:
  assumes "subst_domain δ  set X = {}"
  shows "(Inequality X F) stp δ = Inequality X (F pairs δ)"
using rm_vars_apply'[OF assms] by (simp add: subst_apply_strand_step_def)

lemma fv_strand_step_subst:
  assumes "P = fvstp  P = fvrcv  P = fvsnd  P = fveq ac  P = fvineq"
  and "set (bvarsstp x)  (subst_domain δ  range_vars δ) = {}"
  shows "fvset (δ ` (P x)) = P (x stp δ)"
proof (cases x)
  case (Send ts)
  hence "varsstp x = fvset (set ts)" "fvsnd x = fvset (set ts)" by auto
  thus ?thesis using assms Send subst_apply_fv_unfold[of _ δ] by fastforce
next
  case (Receive ts)
  hence "varsstp x = fvset (set ts)" "fvrcv x = fvset (set ts)" by auto
  thus ?thesis using assms Receive subst_apply_fv_unfold[of _ δ] by fastforce
next
  case (Equality ac' t t') show ?thesis
  proof (cases "ac = ac'")
    case True
    hence "varsstp x = fv t  fv t'" "fveq ac x = fv t  fv t'"
      using Equality
      by auto
    thus ?thesis
      using assms Equality subst_apply_fv_unfold[of _ δ] True
      by auto
  next
    case False
    hence "varsstp x = fv t  fv t'" "fveq ac x = {}"
      using Equality
      by auto
    thus ?thesis
      using assms Equality subst_apply_fv_unfold[of _ δ] False
      by auto
  qed
next
  case (Inequality X F)
  hence 1: "set X  (subst_domain δ  range_vars δ) = {}"
           "x stp δ = Inequality X (F pairs δ)"
           "rm_vars (set X) δ = δ"
    using assms ineq_apply_subst[of δ X F] rm_vars_apply'[of δ "set X"]
    unfolding range_vars_alt_def by force+

  have 2: "fvineq x = fvpairs F - set X" using Inequality by auto
  hence "fvset (δ ` fvineq x) = fvset (δ ` fvpairs F) - set X"
    using fvset_subst_img_eq[OF 1(1), of "fvpairs F"] by simp
  hence 3: "fvset (δ ` fvineq x) = fvpairs (F pairs δ) - set X" by (metis fvpairs_step_subst)
  
  have 4: "fvineq (x stp δ) = fvpairs (F pairs δ) - set X" using 1(2) by auto

  show ?thesis
    using assms(1) Inequality subst_apply_fv_unfold[of _ δ] 1(2) 2 3 4
    unfolding fveq_def fvrcv_def fvsnd_def
    by (metis (no_types) Sup_empty image_empty fvpairs.simps fvset.simps
              fvstp.simps(4) strand_step.simps(20))
qed

lemma fv_strand_subst:
  assumes "P = fvstp  P = fvrcv  P = fvsnd  P = fveq ac  P = fvineq"
  and "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "fvset (δ ` ((set (map P S)))) = (set (map P (S st δ)))"
using assms(2)
proof (induction S)
  case (Cons x S)
  hence *: "bvarsst S  (subst_domain δ  range_vars δ) = {}"
           "set (bvarsstp x)  (subst_domain δ  range_vars δ) = {}"
    unfolding bvarsst_def by force+
  hence **: "fvset (δ ` P x) = P (x stp δ)" using fv_strand_step_subst[OF assms(1), of x δ] by auto
  have "fvset (δ ` ((set (map P (x#S))))) = fvset (δ ` P x)  ((set (map P ((S st δ)))))"
    using Cons unfolding range_vars_alt_def bvarsst_def by force
  hence "fvset (δ ` ((set (map P (x#S))))) = P (x stp δ)  fvset (δ ` ((set (map P S))))"
    using ** by simp
  thus ?case using Cons.IH[OF *(1)] unfolding bvarsst_def by simp
qed simp

lemma fv_strand_subst2:
  assumes "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "fvset (δ ` (wfrestrictedvarsst S)) = wfrestrictedvarsst (S st δ)"
by (metis (no_types, lifting) assms fvset.simps vars_snd_rcv_strand2 fv_strand_subst UN_Un image_Un)

lemma fv_strand_subst':
  assumes "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "fvset (δ ` (fvst S)) = fvst (S st δ)"
by (metis assms fv_strand_subst fvst_def)

lemma fv_trmspairs_is_fvpairs:
  "fvset (trmspairs F) = fvpairs F"
by auto

lemma fvpairs_in_fv_trmspairs: "x  fvpairs F  x  fvset (trmspairs F)"
using fv_trmspairs_is_fvpairs[of F] by blast

lemma trmsst_append: "trmsst (A@B) = trmsst A  trmsst B"
by auto

lemma trmspairs_subst: "trmspairs (a pairs θ) = trmspairs a set θ"
by (auto simp add: subst_apply_pairs_def)

lemma trmspairs_fv_subst_subset:
  "t  trmspairs F  fv (t  θ)  fvpairs (F pairs θ)"
by (force simp add: subst_apply_pairs_def)

lemma trmspairs_fv_subst_subset':
  fixes t::"('a,'b) term" and θ::"('a,'b) subst"
  assumes "t  subtermsset (trmspairs F)"
  shows "fv (t  θ)  fvpairs (F pairs θ)"
proof -
  { fix x assume "x  fv t"
    hence "x  fvpairs F"
      using fv_subset[OF assms] fv_subterms_set[of "trmspairs F"] fv_trmspairs_is_fvpairs[of F]
      by blast
    hence "fv (θ x)  fvpairs (F pairs θ)" using fvpairs_subst_fv_subset by fast
  } thus ?thesis by (meson fv_subst_obtain_var subset_iff) 
qed

lemma trmspairs_funs_term_cases:
  assumes "t  trmspairs (F pairs θ)" "f  funs_term t"
  shows "(u  trmspairs F. f  funs_term u)  (x  fvpairs F. f  funs_term (θ x))"
using assms(1)
proof (induction F)
  case (Cons g F)
  obtain s u where g: "g = (s,u)" by (metis surj_pair)
  show ?case
  proof (cases "t  trmspairs (F pairs θ)")
    case False
    thus ?thesis
      using assms(2) Cons.prems g funs_term_subst[of _ θ]
      by (auto simp add: subst_apply_pairs_def)
  qed (use Cons.IH in fastforce)
qed simp

lemma trmstp_subst: 
  assumes "subst_domain θ  set (bvarsstp a) = {}"
  shows "trmsstp (a stp θ) = trmsstp a set θ"
proof -
  have "rm_vars (set (bvarsstp a)) θ = θ" using assms by force
  thus ?thesis
    using assms
    by (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def
             split: strand_step.splits)
qed

lemma trmsst_subst:
  assumes "subst_domain θ  bvarsst A = {}"
  shows "trmsst (A st θ) = trmsst A set θ"
using assms
proof (induction A)
  case (Cons a A)
  have 1: "subst_domain θ  bvarsst A = {}" "subst_domain θ  set (bvarsstp a) = {}"
    using Cons.prems by auto
  hence IH: "trmsst A set θ = trmsst (A st θ)" using Cons.IH by simp
  
  have "trmsst (a#A) = trmsstp a  trmsst A" by auto
  hence 2: "trmsst (a#A) set θ = (trmsstp a set θ)  (trmsst A set θ)" by (metis image_Un)

  have "trmsst (a#A st θ) = (trmsstp (a stp θ))  trmsst (A st θ)"
    by (auto simp add: subst_apply_strand_def)
  hence 3: "trmsst (a#A st θ) = (trmsstp a set θ)  trmsst (A st θ)"
    using trmstp_subst[OF 1(2)] by auto
  
  show ?case using IH 2 3 by metis
qed (simp add: subst_apply_strand_def)

lemma strand_map_set_subst:
  assumes δ: "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "(set (map trmsstp (S st δ))) = ((set (map trmsstp S))) set δ"
using assms
proof (induction S)
  case (Cons x S)
  hence "bvarsst [x]  subst_domain δ = {}" "bvarsst S  (subst_domain δ  range_vars δ) = {}"
    unfolding bvarsst_def by force+
  hence *: "subst_domain δ  set (bvarsstp x) = {}"
           "(set (map trmsstp (S st δ))) = (set (map trmsstp S)) set δ"
    using Cons.IH(1) bvarsst_singleton[of x] by auto
  hence "trmsstp (x stp δ) = (trmsstp x) set δ"
  proof (cases x)
    case (Inequality X F)
    thus ?thesis
      using rm_vars_apply'[of δ "set X"] * 
      by (metis (no_types, lifting) image_cong trmstp_subst)
  qed simp_all
  thus ?case using * subst_all_insert by auto
qed simp

lemma subst_apply_fv_subset_strand_trm:
  assumes P: "P = fvstp  P = fvrcv  P = fvsnd  P = fveq ac  P = fvineq"
  and fv_sub: "fv t  (set (map P S))  V"
  and δ: "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "fv (t  δ)  (set (map P (S st δ)))  fvset (δ ` V)"
using fv_strand_subst[OF P δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand_trm2:
  assumes fv_sub: "fv t  wfrestrictedvarsst S  V"
  and δ: "bvarsst S  (subst_domain δ  range_vars δ) = {}"
  shows "fv (t  δ)  wfrestrictedvarsst (S st δ)  fvset (δ ` V)"
using fv_strand_subst2[OF δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand:
  assumes P: "P = fvstp  P = fvrcv  P = fvsnd  P = fveq ac  P = fvineq"
  and P_subset: "P x  (set (map P S))  V"
  and δ: "bvarsst S  (subst_domain δ  range_vars δ) = {}"
         "set (bvarsstp x)  (subst_domain δ  range_vars δ) = {}"
  shows "P (x stp δ)  (set (map P (S st δ)))  fvset (δ ` V)"
proof (cases x)
  case (Send ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x stp δ) = fvset (set ts set δ)"
           "fvrcv x = {}" "fvrcv (x stp δ) = {}"
           "fvsnd x = fvset (set ts)" "fvsnd (x stp δ) = fvset (set ts set δ)"
           "fveq ac x = {}" "fveq ac (x stp δ) = {}"
           "fvineq x = {}" "fvineq (x stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts)  P (x stp δ) = fvset (set ts set δ)) 
             (P x = {}  P (x stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x stp δ) = fvset (set ts set δ)"
    hence "fvset (set ts)  (set (map P S))  V" using P_subset by auto
    hence "fvset (set ts set δ)  (set (map P (S st δ)))  fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _ V] by fastforce
    hence ?thesis using P (x stp δ) = fvset (set ts set δ) by force
  }
  ultimately show ?thesis by metis
next
  case (Receive ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x stp δ) = fvset (set ts set δ)"
           "fvrcv x = fvset (set ts)" "fvrcv (x stp δ) = fvset (set ts set δ)"
           "fvsnd x = {}" "fvsnd (x stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x stp δ) = {}"
           "fvineq x = {}" "fvineq (x stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts)  P (x stp δ) = fvset (set ts set δ)) 
             (P x = {}  P (x stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x stp δ) = fvset (set ts set δ)"
    hence "fvset (set ts)  (set (map P S))  V" using P_subset by auto
    hence "fvset (set ts set δ)  (set (map P (S st δ)))  fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _</