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