Theory Labeled_Strands

(*  Title:      Labeled_Strands.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, The University of Sheffield
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Labeled Strands›
theory Labeled_Strands
imports Strands_and_Constraints
begin

subsection ‹Definitions: Labeled Strands and Constraints›
datatype 'l strand_label =
  LabelN (the_LabelN: "'l") (ln _›)
| LabelS ()

text ‹Labeled strands are strands whose steps are equipped with labels›
type_synonym ('a,'b,'c) labeled_strand_step = "'c strand_label × ('a,'b) strand_step"
type_synonym ('a,'b,'c) labeled_strand = "('a,'b,'c) labeled_strand_step list"

abbreviation has_LabelN where "has_LabelN n x  fst x = ln n"
abbreviation has_LabelS where "has_LabelS x  fst x = "

definition unlabel where "unlabel S  map snd S"
definition proj where "proj n S  filter (λs. has_LabelN n s  has_LabelS s) S"
abbreviation proj_unl where "proj_unl n S  unlabel (proj n S)"

abbreviation wfrestrictedvarslst where "wfrestrictedvarslst S  wfrestrictedvarsst (unlabel S)"

abbreviation subst_apply_labeled_strand_step (infix lstp 51) where
  "x lstp θ  (case x of (l, s)  (l, s stp θ))"

abbreviation subst_apply_labeled_strand (infix lst 51) where
  "S lst θ  map (λx. x lstp θ) S"

abbreviation trmslst where "trmslst S  trmsst (unlabel S)"
abbreviation trms_projlst where "trms_projlst n S  trmsst (proj_unl n S)"

abbreviation varslst where "varslst S  varsst (unlabel S)"
abbreviation vars_projlst where "vars_projlst n S  varsst (proj_unl n S)"

abbreviation bvarslst where "bvarslst S  bvarsst (unlabel S)"
abbreviation fvlst where "fvlst S  fvst (unlabel S)"

abbreviation wflst where "wflst V S  wfst V (unlabel S)"


subsection ‹Lemmata: Projections›
lemma has_LabelS_proj_iff_not_has_LabelN:
  "list_all has_LabelS (proj l A)  ¬list_ex (has_LabelN l) A"
by (induct A) (auto simp add: proj_def)

lemma proj_subset_if_no_label:
  assumes "¬list_ex (has_LabelN l) A"
  shows "set (proj l A)  set (proj l' A)"
    and "set (proj_unl l A)  set (proj_unl l' A)"
using assms by (induct A) (auto simp add: unlabel_def proj_def)

lemma proj_in_setD:
  assumes a: "a  set (proj l A)"
  obtains k b where "a = (k, b)" "k = (ln l)  k = "
using that a unfolding proj_def by (cases a) auto

lemma proj_set_mono:
  assumes "set A  set B"
  shows "set (proj n A)  set (proj n B)"
    and "set (proj_unl n A)  set (proj_unl n B)"
using assms unfolding proj_def unlabel_def by auto

lemma unlabel_nil[simp]: "unlabel [] = []"
by (simp add: unlabel_def)

lemma unlabel_mono: "set A  set B  set (unlabel A)  set (unlabel B)"
by (auto simp add: unlabel_def)

lemma unlabel_in: "(l,x)  set A  x  set (unlabel A)"
unfolding unlabel_def by force

lemma unlabel_mem_has_label: "x  set (unlabel A)  l. (l,x)  set A"
unfolding unlabel_def by auto

lemma proj_ident:
  assumes "list_all (λs. has_LabelN l s  has_LabelS s) S"
  shows "proj l S = S"
using assms unfolding proj_def list_all_iff by fastforce

lemma proj_elims_label:
  assumes "k  l"
  shows "¬list_ex (has_LabelN l) (proj k S)"
using assms unfolding proj_def list_ex_iff by force

lemma proj_nil[simp]: "proj n [] = []" "proj_unl n [] = []"
unfolding unlabel_def proj_def by auto

lemma singleton_lst_proj[simp]:
  "proj_unl l [(ln l, a)] = [a]"
  "l  l'  proj_unl l' [(ln l, a)] = []"
  "proj_unl l [(, a)] = [a]"
  "unlabel [(l'', a)] = [a]"
unfolding proj_def unlabel_def by simp_all

lemma unlabel_nil_only_if_nil[simp]: "unlabel A = []  A = []"
unfolding unlabel_def by auto

lemma unlabel_Cons[simp]:
  "unlabel ((l,a)#A) = a#unlabel A"
  "unlabel (b#A) = snd b#unlabel A"
unfolding unlabel_def by simp_all

lemma unlabel_append[simp]: "unlabel (A@B) = unlabel A@unlabel B"
unfolding unlabel_def by auto

lemma proj_Cons[simp]:
  "proj n ((ln n,a)#A) = (ln n,a)#proj n A"
  "proj n ((,a)#A) = (,a)#proj n A"
  "m  n  proj n ((ln m,a)#A) = proj n A"
  "l = (ln n)  proj n ((l,a)#A) = (l,a)#proj n A"
  "l =   proj n ((l,a)#A) = (l,a)#proj n A"
  "fst b    fst b  (ln n)  proj n (b#A) = proj n A"
unfolding proj_def by auto

lemma proj_append[simp]:
  "proj l (A'@B') = proj l A'@proj l B'"
  "proj_unl l (A@B) = proj_unl l A@proj_unl l B"
unfolding proj_def unlabel_def by auto

lemma proj_unl_cons[simp]:
  "proj_unl l ((ln l, a)#A) = a#proj_unl l A"
  "l  l'  proj_unl l' ((ln l, a)#A) = proj_unl l' A"
  "proj_unl l ((, a)#A) = a#proj_unl l A"
unfolding proj_def unlabel_def by simp_all

lemma trms_unlabel_proj[simp]:
  "trmsstp (snd (ln l, x))  trms_projlst l [(ln l, x)]"
by auto

lemma trms_unlabel_star[simp]:
  "trmsstp (snd (, x))  trms_projlst l [(, x)]"
by auto

lemma trmslst_union[simp]: "trmslst A = (l. trms_projlst l A)"
proof (induction A)
  case (Cons a A)
  obtain l s where ls: "a = (l,s)" by atomize_elim auto
  have "trmslst [a] = (l. trms_projlst l [a])"
  proof -
    have *: "trmslst [a] = trmsstp s" using ls by simp
    show ?thesis
    proof (cases l)
      case (LabelN n)
      hence "trms_projlst n [a] = trmsstp s" using ls by simp
      moreover have "m. n  m  trms_projlst m [a] = {}" using ls LabelN by auto
      ultimately show ?thesis using * ls by fastforce
    next
      case LabelS
      hence "l. trms_projlst l [a] = trmsstp s" using ls by auto
      thus ?thesis using * ls by fastforce
    qed
  qed
  moreover have "l. trms_projlst l (a#A) = trms_projlst l [a]  trms_projlst l A"
    unfolding unlabel_def proj_def by auto
  hence "(l. trms_projlst l (a#A)) = (l. trms_projlst l [a])  (l. trms_projlst l A)" by auto
  ultimately show ?case using Cons.IH ls by auto
qed simp

lemma trmslst_append[simp]: "trmslst (A@B) = trmslst A  trmslst B"
by (metis trmsst_append unlabel_append)

lemma trms_projlst_append[simp]: "trms_projlst l (A@B) = trms_projlst l A  trms_projlst l B"
by (metis (no_types, lifting) filter_append proj_def trmslst_append)

lemma trms_projlst_subset[simp]:
  "trms_projlst l A  trms_projlst l (A@B)"
  "trms_projlst l B  trms_projlst l (A@B)"
using trms_projlst_append[of l] by blast+

lemma trmslst_subset[simp]:
  "trmslst A  trmslst (A@B)"
  "trmslst B  trmslst (A@B)"
proof (induction A)
  case (Cons a A)
  obtain l s where *: "a = (l,s)" by atomize_elim auto
  { case 1 thus ?case using Cons * by auto }
  { case 2 thus ?case using Cons * by auto }
qed simp_all

lemma varslst_union: "varslst A = (l. vars_projlst l A)"
proof (induction A)
  case (Cons a A)
  obtain l s where ls: "a = (l,s)" by atomize_elim auto
  have "varslst [a] = (l. vars_projlst l [a])"
  proof -
    have *: "varslst [a] = varsstp s" using ls by auto
    show ?thesis
    proof (cases l)
      case (LabelN n)
      hence "vars_projlst n [a] = varsstp s" using ls by simp
      moreover have "m. n  m  vars_projlst m [a] = {}" using ls LabelN by auto
      ultimately show ?thesis using * ls by fast
    next
      case LabelS
      hence "l. vars_projlst l [a] = varsstp s" using ls by auto
      thus ?thesis using * ls by fast
    qed
  qed
  moreover have "l. vars_projlst l (a#A) = vars_projlst l [a]  vars_projlst l A"
    unfolding unlabel_def proj_def by auto
  hence "(l. vars_projlst l (a#A)) = (l. vars_projlst l [a])  (l. vars_projlst l A)"
    using strand_vars_split(1) by auto
  ultimately show ?case using Cons.IH ls strand_vars_split(1) by auto
qed simp

lemma unlabel_Cons_inv:
  "unlabel A = b#B  A'. (n. A = (ln n, b)#A')  A = (, b)#A'"
proof -
  assume *: "unlabel A = b#B"
  then obtain l A' where "A = (l,b)#A'" unfolding unlabel_def by atomize_elim auto
  thus "A'. (l. A = (ln l, b)#A')  A = (, b)#A'" by (metis strand_label.exhaust)
qed

lemma unlabel_snoc_inv:
  "unlabel A = B@[b]  A'. (n. A = A'@[(ln n, b)])  A = A'@[(, b)]"
proof -
  assume *: "unlabel A = B@[b]"
  then obtain A' l where "A = A'@[(l,b)]"
    unfolding unlabel_def by (induct A rule: List.rev_induct) auto
  thus "A'. (n. A = A'@[(ln n, b)])  A = A'@[(, b)]" by (cases l) auto
qed

lemma proj_idem[simp]: "proj l (proj l A) = proj l A"
unfolding proj_def by auto

lemma proj_ikst_is_proj_rcv_set:
  "ikst (proj_unl n A) =
    {t. ts. ((ln n, Receive ts)  set A  (, Receive ts)  set A)  t  set ts} "
using ikst_is_rcv_set unfolding unlabel_def proj_def by force

lemma unlabel_ikst_is_rcv_set:
  "ikst (unlabel A) = {t | l t ts. (l, Receive ts)  set A  t  set ts}"
using ikst_is_rcv_set unfolding unlabel_def by force

lemma proj_ik_union_is_unlabel_ik:
  "ikst (unlabel A) = (l. ikst (proj_unl l A))"
proof
  show "(l. ikst (proj_unl l A))  ikst (unlabel A)"
    using unlabel_ikst_is_rcv_set[of A] proj_ikst_is_proj_rcv_set[of _ A] by auto

  show "ikst (unlabel A)  (l. ikst (proj_unl l A))"
  proof
    fix t assume "t  ikst (unlabel A)"
    then obtain l ts where "(l, Receive ts)  set A" "t  set ts"
      using ikst_is_rcv_set unlabel_mem_has_label[of _ A]
      by atomize_elim blast
    thus "t  (l. ikst (proj_unl l A))" using proj_ikst_is_proj_rcv_set[of _ A] by (cases l) auto
  qed
qed

lemma proj_ik_append[simp]:
  "ikst (proj_unl l (A@B)) = ikst (proj_unl l A)  ikst (proj_unl l B)"
using proj_append(2)[of l A B] ik_append by auto

lemma proj_ik_append_subst_all:
  "ikst (proj_unl l (A@B)) set I = (ikst (proj_unl l A) set I)  (ikst (proj_unl l B) set I)"
using proj_ik_append[of l] by auto

lemma ik_proj_subset[simp]: "ikst (proj_unl n A)  trms_projlst n A"
by auto

lemma prefix_unlabel:
  "prefix A B  prefix (unlabel A) (unlabel B)"
unfolding prefix_def unlabel_def by auto

lemma prefix_proj:
  "prefix A B  prefix (proj n A) (proj n B)"
  "prefix A B  prefix (proj_unl n A) (proj_unl n B)"
unfolding prefix_def proj_def by auto

lemma suffix_unlabel:
  "suffix A B  suffix (unlabel A) (unlabel B)"
unfolding suffix_def unlabel_def by auto

lemma suffix_proj:
  "suffix A B  suffix (proj n A) (proj n B)"
  "suffix A B  suffix (proj_unl n A) (proj_unl n B)"
unfolding suffix_def proj_def by auto


subsection ‹Lemmata: Well-formedness›
lemma wfvarsoccsst_proj_union:
  "wfvarsoccsst (unlabel A) = (l. wfvarsoccsst (proj_unl l A))"
proof (induction A)
  case (Cons a A)
  obtain l s where ls: "a = (l,s)" by atomize_elim auto
  have "wfvarsoccsst (unlabel [a]) = (l. wfvarsoccsst (proj_unl l [a]))"
  proof -
    have *: "wfvarsoccsst (unlabel [a]) = wfvarsoccsstp s" using ls by auto
    show ?thesis
    proof (cases l)
      case (LabelN n)
      hence "wfvarsoccsst (proj_unl n [a]) = wfvarsoccsstp s" using ls by simp
      moreover have "m. n  m  wfvarsoccsst (proj_unl m [a]) = {}" using ls LabelN by auto
      ultimately show ?thesis using * ls by fast
    next
      case LabelS
      hence "l. wfvarsoccsst (proj_unl l [a]) = wfvarsoccsstp s" using ls by auto
      thus ?thesis using * ls by fast
    qed
  qed
  moreover have
      "wfvarsoccsst (proj_unl l (a#A)) =
       wfvarsoccsst (proj_unl l [a])  wfvarsoccsst (proj_unl l A)"
    for l
    unfolding unlabel_def proj_def by auto
  hence "(l. wfvarsoccsst (proj_unl l (a#A))) =
         (l. wfvarsoccsst (proj_unl l [a]))  (l. wfvarsoccsst (proj_unl l A))"
    using strand_vars_split(1) by auto
  ultimately show ?case using Cons.IH ls strand_vars_split(1) by auto
qed simp

lemma wf_if_wf_proj:
  assumes "l. wfst V (proj_unl l A)"
  shows "wfst V (unlabel A)"
using assms
proof (induction A arbitrary: V rule: List.rev_induct)
  case (snoc a A)
  hence IH: "wfst V (unlabel A)" using proj_append(2)[of _ A] by auto
  obtain b l where b: "a = (ln l, b)  a = (, b)" by (cases a, metis strand_label.exhaust)
  hence *: "wfst V (proj_unl l A@[b])"
    by (metis snoc.prems proj_append(2) singleton_lst_proj(1) proj_unl_cons(1,3))
  thus ?case using IH b snoc.prems proj_append(2)[of l A "[a]"] unlabel_append[of A "[a]"]
  proof (cases b)
    case (Receive ts)
    have "fvset (set ts)  wfvarsoccsst (unlabel A)  V"
    proof
      fix x assume "x  fvset (set ts)"
      hence "x  V  wfvarsoccsst (proj_unl l A)" using wf_append_exec[OF *] b Receive by auto
      thus "x  wfvarsoccsst (unlabel A)  V" using wfvarsoccsst_proj_union[of A] by auto
    qed
    hence "fvset (set ts)  wfrestrictedvarsst (unlabel A)  V"
      using vars_snd_rcv_strand_subset2(4)[of "unlabel A"] by blast
    hence "wfst V (unlabel A@[Receive ts])" by (rule wf_rcv_append'''[OF IH])
    thus ?thesis using b Receive unlabel_append[of A "[a]"] by auto
  next
    case (Equality ac s t)
    have "fv t  wfvarsoccsst (unlabel A)  V" when "ac = Assign"
    proof
      fix x assume "x  fv t"
      hence "x  V  wfvarsoccsst (proj_unl l A)" using wf_append_exec[OF *] b Equality that by auto
      thus "x  wfvarsoccsst (unlabel A)  V" using wfvarsoccsst_proj_union[of A] by auto
    qed
    hence "fv t  wfrestrictedvarslst A  V" when "ac = Assign"
      using vars_snd_rcv_strand_subset2(4)[of "unlabel A"] that by blast
    hence "wfst V (unlabel A@[Equality ac s t])"
      by (cases ac) (metis wf_eq_append'''[OF IH], metis wf_eq_check_append''[OF IH])
    thus ?thesis using b Equality unlabel_append[of A "[a]"] by auto
  qed auto
qed simp

end