Theory Noninterference_Ipurge_Unwinding.DeterministicProcesses

(*  Title:       The Ipurge Unwinding Theorem for CSP Noninterference Security
    Author:      Pasquale Noce
                 Security Certification Specialist at Arjo Systems - Gep S.p.A.
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at arjowiggins-it dot com
*)

section "The Ipurge Unwinding Theorem for deterministic and trace set processes"

theory DeterministicProcesses
imports IpurgeUnwinding
begin

text ‹
\null

In accordance with Hoare's formal definition of deterministic processes \<^cite>‹"R3"›, this section
shows that a process is deterministic just in case it is a \emph{trace set process}, i.e. it may be
identified by means of a trace set alone, matching the set of its traces, in place of a
failures-divergences pair. Then, variants of the Ipurge Unwinding Theorem are proven for
deterministic processes and trace set processes.
›


subsection "Deterministic processes"

text ‹
Here below are the definitions of predicates ‹d_future_consistent› and
‹d_weakly_future_consistent›, which are variants of predicates @{term future_consistent} and
@{term weakly_future_consistent} meant for applying to deterministic processes. In some detail,
being deterministic processes such that refused events are completely specified by accepted events
(cf. \<^cite>‹"R3"›, \<^cite>‹"R1"›), the new predicates are such that their truth values can be determined
by just considering the accepted events of the process taken as input.

Then, it is proven that these predicates are characterized by the same connection as that of their
general-purpose counterparts, viz. ‹d_future_consistent› implies
‹d_weakly_future_consistent›, and they are equivalent for domain-relation map
@{term rel_ipurge}. Finally, the predicates are shown to be equivalent to their general-purpose
counterparts in the case of a deterministic process.

\null
›

definition d_future_consistent ::
 "'a process ⇒ ('a ⇒ 'd) ⇒ ('a, 'd) dom_rel_map ⇒ bool" where
"d_future_consistent P D R ≡
  ∀u ∈ range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    (xs ∈ traces P) = (ys ∈ traces P) ∧
    next_dom_events P D u xs = next_dom_events P D u ys"

definition d_weakly_future_consistent ::
 "'a process ⇒ ('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('a, 'd) dom_rel_map ⇒ bool" where
"d_weakly_future_consistent P I D R ≡
  ∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    (xs ∈ traces P) = (ys ∈ traces P) ∧
    next_dom_events P D u xs = next_dom_events P D u ys"

lemma dfc_implies_dwfc:
 "d_future_consistent P D R ⟹ d_weakly_future_consistent P I D R"
by (simp only: d_future_consistent_def d_weakly_future_consistent_def, blast)

lemma dfc_equals_dwfc_rel_ipurge:
 "d_future_consistent P D (rel_ipurge P I D) =
  d_weakly_future_consistent P I D (rel_ipurge P I D)"
proof (rule iffI, erule dfc_implies_dwfc,
 simp only: d_future_consistent_def d_weakly_future_consistent_def,
 rule ballI, (rule allI)+, rule impI)
  fix u xs ys
  assume
    A: "∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ rel_ipurge P I D u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" and
    B: "u ∈ range D" and
    C: "(xs, ys) ∈ rel_ipurge P I D u"
  show "(xs ∈ traces P) = (ys ∈ traces P) ∧
    next_dom_events P D u xs = next_dom_events P D u ys"
  proof (cases "u ∈ range D ∩ (-I) `` range D")
    case True
    with A have "∀xs ys. (xs, ys) ∈ rel_ipurge P I D u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" ..
    hence "(xs, ys) ∈ rel_ipurge P I D u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys"
     by blast
    thus ?thesis using C ..
  next
    case False
    hence D: "u ∉ (-I) `` range D" using B by simp
    have "ipurge_tr_rev I D u xs = ipurge_tr_rev I D u ys"
     using C by (simp add: rel_ipurge_def)
    moreover have "∀zs. ipurge_tr_rev I D u zs = zs"
    proof (rule allI, rule ipurge_tr_rev_all, rule ballI, erule imageE, rule ccontr)
      fix v x
      assume "(v, u) ∉ I"
      hence "(v, u) ∈ -I" by simp
      moreover assume "v = D x"
      hence "v ∈ range D" by simp
      ultimately have "u ∈ (-I) `` range D" ..
      thus False using D by contradiction
    qed
    ultimately show ?thesis by simp
  qed
qed

lemma d_fc_equals_dfc:
  assumes A: "deterministic P"
  shows "future_consistent P D R = d_future_consistent P D R"
proof (rule iffI, simp_all only: d_future_consistent_def,
 rule ballI, (rule allI)+, rule impI, rule conjI, rule fc_traces, assumption+,
 simp_all add: future_consistent_def del: ball_simps)
  assume B: "∀u ∈ range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    (xs ∈ traces P) = (ys ∈ traces P) ∧
    next_dom_events P D u xs = next_dom_events P D u ys"
  show "∀u ∈ range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    ref_dom_events P D u xs = ref_dom_events P D u ys"
  proof (rule ballI, (rule allI)+, rule impI,
   simp add: ref_dom_events_def set_eq_iff, rule allI)
    fix u xs ys x
    assume "u ∈ range D"
    with B have "∀xs ys. (xs, ys) ∈ R u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" ..
    hence "(xs, ys) ∈ R u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys"
     by blast
    moreover assume "(xs, ys) ∈ R u"
    ultimately have C: "(xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" ..
    show "(u = D x ∧ {x} ∈ refusals P xs) = (u = D x ∧ {x} ∈ refusals P ys)"
    proof (cases "u = D x", simp_all, cases "xs ∈ traces P")
      assume D: "u = D x" and E: "xs ∈ traces P"
      have
        A': "∀xs ∈ traces P. ∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})"
       using A by (simp add: deterministic_def)
      hence "∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})" using E ..
      hence "{x} ∈ refusals P xs = ({x} ∩ next_events P xs = {})" ..
      moreover have "ys ∈ traces P" using C and E by simp
      with A' have "∀X. X ∈ refusals P ys = (X ∩ next_events P ys = {})" ..
      hence "{x} ∈ refusals P ys = ({x} ∩ next_events P ys = {})" ..
      moreover have "{x} ∩ next_events P xs = {x} ∩ next_events P ys"
      proof (simp add: set_eq_iff, rule allI, rule iffI, erule_tac [!] conjE, simp_all)
        assume "x ∈ next_events P xs"
        hence "x ∈ next_dom_events P D u xs" using D by (simp add: next_dom_events_def)
        hence "x ∈ next_dom_events P D u ys" using C by simp
        thus "x ∈ next_events P ys" by (simp add: next_dom_events_def)
      next
        assume "x ∈ next_events P ys"
        hence "x ∈ next_dom_events P D u ys" using D by (simp add: next_dom_events_def)
        hence "x ∈ next_dom_events P D u xs" using C by simp
        thus "x ∈ next_events P xs" by (simp add: next_dom_events_def)
      qed
      ultimately show "({x} ∈ refusals P xs) = ({x} ∈ refusals P ys)" by simp
    next
      assume D: "xs ∉ traces P"
      hence "∀X. (xs, X) ∉ failures P" by (simp add: traces_def Domain_iff)
      hence "refusals P xs = {}" by (rule_tac equals0I, simp add: refusals_def)
      moreover have "ys ∉ traces P" using C and D by simp
      hence "∀X. (ys, X) ∉ failures P" by (simp add: traces_def Domain_iff)
      hence "refusals P ys = {}" by (rule_tac equals0I, simp add: refusals_def)
      ultimately show "({x} ∈ refusals P xs) = ({x} ∈ refusals P ys)" by simp
    qed
  qed
qed

lemma d_wfc_equals_dwfc:
  assumes A: "deterministic P"
  shows "weakly_future_consistent P I D R = d_weakly_future_consistent P I D R"
proof (rule iffI, simp_all only: d_weakly_future_consistent_def,
 rule ballI, (rule allI)+, rule impI, rule conjI, rule wfc_traces, assumption+,
 simp_all add: weakly_future_consistent_def del: ball_simps)
  assume B: "∀u ∈ range D ∩ (- I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    (xs ∈ traces P) = (ys ∈ traces P) ∧
    next_dom_events P D u xs = next_dom_events P D u ys"
  show "∀u ∈ range D ∩ (- I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
    ref_dom_events P D u xs = ref_dom_events P D u ys"
  proof (rule ballI, (rule allI)+, rule impI,
   simp (no_asm_simp) add: ref_dom_events_def set_eq_iff, rule allI)
    fix u xs ys x
    assume "u ∈ range D ∩ (- I) `` range D"
    with B have "∀xs ys. (xs, ys) ∈ R u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" ..
    hence "(xs, ys) ∈ R u ⟶
      (xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys"
     by blast
    moreover assume "(xs, ys) ∈ R u"
    ultimately have C: "(xs ∈ traces P) = (ys ∈ traces P) ∧
      next_dom_events P D u xs = next_dom_events P D u ys" ..
    show "(u = D x ∧ {x} ∈ refusals P xs) = (u = D x ∧ {x} ∈ refusals P ys)"
    proof (cases "u = D x", simp_all, cases "xs ∈ traces P")
      assume D: "u = D x" and E: "xs ∈ traces P"
      have A': "∀xs ∈ traces P. ∀X.
        X ∈ refusals P xs = (X ∩ next_events P xs = {})"
       using A by (simp add: deterministic_def)
      hence "∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})" using E ..
      hence "{x} ∈ refusals P xs = ({x} ∩ next_events P xs = {})" ..
      moreover have "ys ∈ traces P" using C and E by simp
      with A' have "∀X. X ∈ refusals P ys = (X ∩ next_events P ys = {})" ..
      hence "{x} ∈ refusals P ys = ({x} ∩ next_events P ys = {})" ..
      moreover have "{x} ∩ next_events P xs = {x} ∩ next_events P ys"
      proof (simp add: set_eq_iff, rule allI, rule iffI, erule_tac [!] conjE, simp_all)
        assume "x ∈ next_events P xs"
        hence "x ∈ next_dom_events P D u xs" using D by (simp add: next_dom_events_def)
        hence "x ∈ next_dom_events P D u ys" using C by simp
        thus "x ∈ next_events P ys" by (simp add: next_dom_events_def)
      next
        assume "x ∈ next_events P ys"
        hence "x ∈ next_dom_events P D u ys" using D by (simp add: next_dom_events_def)
        hence "x ∈ next_dom_events P D u xs" using C by simp
        thus "x ∈ next_events P xs" by (simp add: next_dom_events_def)
      qed
      ultimately show "({x} ∈ refusals P xs) = ({x} ∈ refusals P ys)" by simp
    next
      assume D: "xs ∉ traces P"
      hence "∀X. (xs, X) ∉ failures P" by (simp add: traces_def Domain_iff)
      hence "refusals P xs = {}" by (rule_tac equals0I, simp add: refusals_def)
      moreover have "ys ∉ traces P" using C and D by simp
      hence "∀X. (ys, X) ∉ failures P" by (simp add: traces_def Domain_iff)
      hence "refusals P ys = {}" by (rule_tac equals0I, simp add: refusals_def)
      ultimately show "({x} ∈ refusals P xs) = ({x} ∈ refusals P ys)" by simp
    qed
  qed
qed

text ‹
\null

Here below is the proof of a variant of the Ipurge Unwinding Theorem applying to deterministic
processes. Unsurprisingly, its enunciation contains predicate @{term d_weakly_future_consistent} in
place of @{term weakly_future_consistent}. Furthermore, the assumption that the process be refusals
union closed is replaced by the assumption that it be deterministic, since the former property is
shown to be entailed by the latter.

\null
›

lemma d_implies_ruc:
  assumes A: "deterministic P"
  shows "ref_union_closed P"
proof (subst ref_union_closed_def, (rule allI)+, (rule impI)+, erule exE)
  fix xs A X
  have "∀xs ∈ traces P. ∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})"
   using A by (simp add: deterministic_def)
  moreover assume B: "∀X ∈ A. (xs, X) ∈ failures P" and "X ∈ A"
  hence "(xs, X) ∈ failures P" ..
  hence "xs ∈ traces P" by (rule failures_traces)
  ultimately have C: "∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})" ..
  have D: "∀X ∈ A. X ∩ next_events P xs = {}"
  proof
    fix X
    assume "X ∈ A"
    with B have "(xs, X) ∈ failures P" ..
    hence "X ∈ refusals P xs" by (simp add: refusals_def)
    thus "X ∩ next_events P xs = {}" using C by simp
  qed
  have "(⋃X ∈ A. X) ∈ refusals P xs = ((⋃X ∈ A. X) ∩ next_events P xs = {})"
   using C ..
  hence E: "(xs, ⋃X ∈ A. X) ∈ failures P =
    ((⋃X ∈ A. X) ∩ next_events P xs = {})"
   by (simp add: refusals_def)
  show "(xs, ⋃X ∈ A. X) ∈ failures P"
  proof (rule ssubst [OF E], rule equals0I, erule IntE, erule UN_E)
    fix x X
    assume "X ∈ A"
    with D have "X ∩ next_events P xs = {}" ..
    moreover assume "x ∈ X" and "x ∈ next_events P xs"
    hence "x ∈ X ∩ next_events P xs" ..
    hence "∃x. x ∈ X ∩ next_events P xs" ..
    hence "X ∩ next_events P xs ≠ {}" by (subst ex_in_conv [symmetric])
    ultimately show False by contradiction
  qed
qed

theorem d_ipurge_unwinding:
  assumes A: "deterministic P"
  shows "secure P I D = d_weakly_future_consistent P I D (rel_ipurge P I D)"
proof (insert d_wfc_equals_dwfc [of P I D "rel_ipurge P I D", OF A], erule subst)
qed (insert d_implies_ruc [OF A], rule ipurge_unwinding)


subsection "Trace set processes"

text ‹
In \<^cite>‹"R3"›, section 2.8, Hoare formulates a simplified definition of a deterministic process,
identified with a \emph{trace set}, i.e. a set of event lists containing the empty list and any
prefix of each of its elements. Of course, this is consistent with the definition of determinism
applying to processes identified with failures-divergences pairs, which implies that their refusals
are completely specified by their traces (cf. \<^cite>‹"R3"›, \<^cite>‹"R1"›).

Here below are the definitions of a function ‹ts_process›, converting the input set of lists
into a process, and a predicate ‹trace_set›, returning @{term True} just in case the input set
of lists has the aforesaid properties. An analysis is then conducted about the output of the
functions defined in \<^cite>‹"R1"›, section 1.1, when acting on a \emph{trace set process}, i.e. a
process that may be expressed as ‹ts_process T› where ‹trace_set T› matches
@{term True}.

\null
›

definition ts_process :: "'a list set ⇒ 'a process" where
"ts_process T ≡ Abs_process ({(xs, X). xs ∈ T ∧ (∀x ∈ X. xs @ [x] ∉ T)}, {})"

definition trace_set :: "'a list set ⇒ bool" where
"trace_set T ≡ [] ∈ T ∧ (∀xs x. xs @ [x] ∈ T ⟶ xs ∈ T)"

lemma ts_process_rep:
  assumes A: "trace_set T"
  shows "Rep_process (ts_process T) =
    ({(xs, X). xs ∈ T ∧ (∀x ∈ X. xs @ [x] ∉ T)}, {})"
proof (subst ts_process_def, rule Abs_process_inverse, simp add: process_set_def,
 (subst conj_assoc [symmetric])+, (rule conjI)+, simp_all add:
 process_prop_1_def
 process_prop_2_def
 process_prop_3_def
 process_prop_4_def
 process_prop_5_def
 process_prop_6_def)
  show "[] ∈ T" using A by (simp add: trace_set_def)
next
  show "∀xs. (∃x. xs @ [x] ∈ T ∧ (∃X. ∀x' ∈ X. xs @ [x, x'] ∉ T)) ⟶ xs ∈ T"
  proof (rule allI, rule impI, erule exE, erule conjE)
    fix xs x
    have "∀xs x. xs @ [x] ∈ T ⟶ xs ∈ T" using A by (simp add: trace_set_def)
    hence "xs @ [x] ∈ T ⟶ xs ∈ T" by blast
    moreover assume "xs @ [x] ∈ T"
    ultimately show "xs ∈ T" ..
  qed
next
  show "∀xs X. xs ∈ T ∧ (∃Y. (∀x ∈ Y. xs @ [x] ∉ T) ∧ X ⊆ Y) ⟶
    (∀x ∈ X. xs @ [x] ∉ T)"
  proof ((rule allI)+, rule impI, (erule conjE, (erule exE)?)+, rule ballI)
    fix xs x X Y
    assume "∀x ∈ Y. xs @ [x] ∉ T"
    moreover assume "X ⊆ Y" and "x ∈ X"
    hence "x ∈ Y" ..
    ultimately show "xs @ [x] ∉ T" ..
  qed
qed

lemma ts_process_failures:
 "trace_set T ⟹
  failures (ts_process T) = {(xs, X). xs ∈ T ∧ (∀x ∈ X. xs @ [x] ∉ T)}"
by (drule ts_process_rep, simp add: failures_def)

lemma ts_process_futures:
 "trace_set T ⟹
  futures (ts_process T) xs =
  {(ys, Y). xs @ ys ∈ T ∧ (∀y ∈ Y. xs @ ys @ [y] ∉ T)}"
by (simp add: futures_def ts_process_failures)

lemma ts_process_traces:
 "trace_set T ⟹ traces (ts_process T) = T"
proof (drule ts_process_failures, simp add: traces_def, rule set_eqI, rule iffI, simp_all)
qed (rule_tac x = "{}" in exI, simp)

lemma ts_process_refusals:
 "trace_set T ⟹ xs ∈ T ⟹
  refusals (ts_process T) xs = {X. ∀x ∈ X. xs @ [x] ∉ T}"
by (drule ts_process_failures, simp add: refusals_def)

lemma ts_process_next_events:
 "trace_set T ⟹ (x ∈ next_events (ts_process T) xs) = (xs @ [x] ∈ T)"
by (drule ts_process_traces, simp add: next_events_def)

text ‹
\null

In what follows, the proof is given of two results which provide a connection between the notions of
deterministic and trace set processes: any trace set process is deterministic, and any process is
deterministic just in case it is equal to the trace set process corresponding to the set of its
traces.

\null
›

lemma ts_process_d:
 "trace_set T ⟹ deterministic (ts_process T)"
proof (frule ts_process_traces, simp add: deterministic_def, rule ballI,
 drule ts_process_refusals, assumption, simp add: next_events_def,
 rule allI, rule iffI)
  fix xs X
  assume "∀x ∈ X. xs @ [x] ∉ T"
  thus "X ∩ {x. xs @ [x] ∈ T} = {}"
  by (rule_tac equals0I, erule_tac IntE, simp)
next
  fix xs X
  assume A: "X ∩ {x. xs @ [x] ∈ T} = {}"
  show "∀x ∈ X. xs @ [x] ∉ T"
  proof (rule ballI, rule notI)
    fix x
    assume "x ∈ X" and "xs @ [x] ∈ T"
    hence "x ∈ X ∩ {x. xs @ [x] ∈ T}" by simp
    moreover have "x ∉ X ∩ {x. xs @ [x] ∈ T}" using A by (rule equals0D)
    ultimately show False by contradiction
  qed
qed

definition divergences :: "'a process ⇒ 'a list set" where
"divergences P ≡ snd (Rep_process P)"

lemma d_divergences:
  assumes A: "deterministic P"
  shows "divergences P = {}"
proof (subst divergences_def, rule equals0I)
  fix xs
  have B: "Rep_process P ∈ process_set" (is "?P' ∈ _") by (rule Rep_process)
  hence "∀xs. ∃x. xs ∈ snd ?P' ⟶ xs @ [x] ∈ snd ?P'"
   by (simp add: process_set_def process_prop_5_def)
  hence "∃x. xs ∈ snd ?P' ⟶ xs @ [x] ∈ snd ?P'" ..
  then obtain x where "xs ∈ snd ?P' ⟶ xs @ [x] ∈ snd ?P'" ..
  moreover assume C: "xs ∈ snd ?P'"
  ultimately have D: "xs @ [x] ∈ snd ?P'" ..
  have E: "∀xs X. xs ∈ snd ?P' ⟶ (xs, X) ∈ fst ?P'"
   using B by (simp add: process_set_def process_prop_6_def)
  hence "xs ∈ snd ?P' ⟶ (xs, {x}) ∈ fst ?P'" by blast
  hence "{x} ∈ refusals P xs"
   using C by (drule_tac mp, simp_all add: failures_def refusals_def)
  moreover have "xs @ [x] ∈ snd ?P' ⟶ (xs @ [x], {}) ∈ fst ?P'"
   using E by blast
  hence "(xs @ [x], {}) ∈ failures P"
   using D by (drule_tac mp, simp_all add: failures_def)
  hence F: "xs @ [x] ∈ traces P" by (rule failures_traces)
  hence "{x} ∩ next_events P xs ≠ {}" by (simp add: next_events_def)
  ultimately have G: "({x} ∈ refusals P xs) ≠ ({x} ∩ next_events P xs = {})"
   by simp
  have "∀xs ∈ traces P. ∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})"
   using A by (simp add: deterministic_def)
  moreover have "xs ∈ traces P" using F by (rule process_rule_2_traces)
  ultimately have "∀X. X ∈ refusals P xs = (X ∩ next_events P xs = {})" ..
  hence "{x} ∈ refusals P xs = ({x} ∩ next_events P xs = {})" ..
  thus False using G by contradiction
qed

lemma trace_set_traces:
 "trace_set (traces P)"
proof (simp only: trace_set_def traces_def failures_def Domain_iff,
 rule conjI, (rule_tac [2] allI)+, rule_tac [2] impI, erule_tac [2] exE)
  have "Rep_process P ∈ process_set" (is "?P' ∈ _") by (rule Rep_process)
  hence "([], {}) ∈ fst ?P'" by (simp add: process_set_def process_prop_1_def)
  thus "∃X. ([], X) ∈ fst ?P'" ..
next
  fix xs x X
  have "Rep_process P ∈ process_set" (is "?P' ∈ _") by (rule Rep_process)
  hence "∀xs x X. (xs @ [x], X) ∈ fst ?P' ⟶ (xs, {}) ∈ fst ?P'"
   by (simp add: process_set_def process_prop_2_def)
  hence "(xs @ [x], X) ∈ fst ?P' ⟶ (xs, {}) ∈ fst ?P'" by blast
  moreover assume "(xs @ [x], X) ∈ fst ?P'"
  ultimately have "(xs, {}) ∈ fst ?P'" ..
  thus "∃X. (xs, X) ∈ fst ?P'" ..
qed

lemma d_implies_ts_process_traces:
 "deterministic P ⟹ ts_process (traces P) = P"
proof (simp add: Rep_process_inject [symmetric] prod_eq_iff failures_def [symmetric],
 insert trace_set_traces [of P], frule ts_process_rep, frule d_divergences,
 simp add: divergences_def deterministic_def)
  assume A: "∀xs ∈ traces P. ∀X.
    (X ∈ refusals P xs) = (X ∩ next_events P xs = {})"
  assume B: "trace_set (traces P)"
  hence C: "traces (ts_process (traces P)) = traces P" by (rule ts_process_traces)
  show "failures (ts_process (traces P)) = failures P"
  proof (rule equalityI, rule_tac [!] subsetI, simp_all only: split_paired_all)
    fix xs X
    assume D: "(xs, X) ∈ failures (ts_process (traces P))"
    hence "xs ∈ traces (ts_process (traces P))" by (rule failures_traces)
    hence E: "xs ∈ traces P" using C by simp
    with B have
     "refusals (ts_process (traces P)) xs = {X. ∀x ∈ X. xs @ [x] ∉ traces P}"
     by (rule ts_process_refusals)
    moreover have "X ∈ refusals (ts_process (traces P)) xs"
     using D by (simp add: refusals_def)
    ultimately have "∀x ∈ X. xs @ [x] ∉ traces P" by simp
    hence "X ∩ next_events P xs = {}"
     by (rule_tac equals0I, erule_tac IntE, simp add: next_events_def)
    moreover have "∀X. (X ∈ refusals P xs) = (X ∩ next_events P xs = {})"
     using A and E ..
    hence "(X ∈ refusals P xs) = (X ∩ next_events P xs = {})" ..
    ultimately have "X ∈ refusals P xs" by simp
    thus "(xs, X) ∈ failures P" by (simp add: refusals_def)
  next
    fix xs X
    assume D: "(xs, X) ∈ failures P"
    hence E: "xs ∈ traces P" by (rule failures_traces)
    with A have "∀X. (X ∈ refusals P xs) = (X ∩ next_events P xs = {})" ..
    hence "(X ∈ refusals P xs) = (X ∩ next_events P xs = {})" ..
    moreover have "X ∈ refusals P xs" using D by (simp add: refusals_def)
    ultimately have F: "X ∩ {x. xs @ [x] ∈ traces P} = {}"
     by (simp add: next_events_def)
    have "∀x ∈ X. xs @ [x] ∉ traces P"
    proof (rule ballI, rule notI)
      fix x
      assume "x ∈ X" and "xs @ [x] ∈ traces P"
      hence "x ∈ X ∩ {x. xs @ [x] ∈ traces P}" by simp
      moreover have "x ∉ X ∩ {x. xs @ [x] ∈ traces P}" using F by (rule equals0D)
      ultimately show False by contradiction
    qed
    moreover have
     "refusals (ts_process (traces P)) xs = {X. ∀x ∈ X. xs @ [x] ∉ traces P}"
     using B and E by (rule ts_process_refusals)
    ultimately have "X ∈ refusals (ts_process (traces P)) xs" by simp
    thus "(xs, X) ∈ failures (ts_process (traces P))" by (simp add: refusals_def)
  qed
qed

lemma ts_process_traces_implies_d:
 "ts_process (traces P) = P ⟹ deterministic P"
by (insert trace_set_traces [of P], drule ts_process_d, simp)

lemma d_equals_ts_process_traces:
 "deterministic P = (ts_process (traces P) = P)"
by (rule iffI, erule d_implies_ts_process_traces, rule ts_process_traces_implies_d)

text ‹
\null

Finally, a variant of the Ipurge Unwinding Theorem applying to trace set processes is derived from
the variant for deterministic processes. Particularly, the assumption that the process be
deterministic is replaced by the assumption that it be a trace set process,
since the former property is entailed by the latter (cf. above).

\null
›

theorem ts_ipurge_unwinding:
 "trace_set T ⟹
  secure (ts_process T) I D =
  d_weakly_future_consistent (ts_process T) I D (rel_ipurge (ts_process T) I D)"
by (rule d_ipurge_unwinding, rule ts_process_d)

end