Theory ConcurrentComposition

(*  Title:       Conservation of CSP Noninterference Security under Concurrent Composition
    Author:      Pasquale Noce
                 Security Certification Specialist at Arjo Systems, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at arjosystems dot com
*)

section "Concurrent composition and noninterference security"

theory ConcurrentComposition
imports Noninterference_Sequential_Composition.Propaedeutics
begin

text ‹
\null

In his outstanding work on Communicating Sequential Processes \<^cite>‹"R6"›, Hoare has defined two
fundamental binary operations allowing to compose the input processes into another, typically more
complex, process: sequential composition and concurrent composition. Particularly, the output of the
latter operation is a process in which any event not shared by both operands can occur whenever the
operand that admits the event can engage in it, whereas any event shared by both operands can occur
just in case both can engage in it. In other words, shared events are those that synchronize the
concurrent processes, which on the contrary can engage asynchronously in the respective non-shared
events.

This paper formalizes Hoare's definition of concurrent composition and proves, in the general case
of a possibly intransitive policy, that CSP noninterference security \<^cite>‹"R1"› is conserved under
this operation, viz. the security of both of the input processes implies that of the output process.
This result, along with the analogous one concerning sequential composition attained in \<^cite>‹"R5"›,
enables the construction of more and more complex processes enforcing noninterference security by
composing, sequentially or concurrently, simpler secure processes, whose security can in turn be
proven using either the definition of security formulated in \<^cite>‹"R1"›, or the unwinding theorems
demonstrated in \<^cite>‹"R2"›, \<^cite>‹"R3"›, and \<^cite>‹"R4"›.

Throughout this paper, the salient points of definitions and proofs are commented; for additional
information, cf. Isabelle documentation, particularly \<^cite>‹"R7"›, \<^cite>‹"R8"›, \<^cite>‹"R9"›, and
\<^cite>‹"R10"›.
›


subsection "Propaedeutic definitions and lemmas"

text ‹
The starting point is comprised of some definitions and lemmas propaedeutic to the proof of the
target security conservation theorem.

Particularly, the definition of operator \emph{after} given in \<^cite>‹"R6"› is formalized, and it is
proven that for any secure process @{term P} and any trace @{term xs} of @{term P}, @{term P} after
@{term xs} is still a secure process. Then, this result is used to generalize the lemma stating the
closure of the failures of a secure process @{term P} under intransitive purge, proven in \<^cite>‹"R5"›,
to the futures of @{term P} associated to any one of its traces. This is a generalization of the
former result since @{term "futures P xs = failures P"} for @{term "xs = []"}.

\null
›

lemma sinks_aux_elem [rule_format]:
 "u ∈ sinks_aux I D U xs ⟶ u ∈ U ∨ (∃x ∈ set xs. u = D x)"
by (induction xs rule: rev_induct, simp_all, blast)

lemma ipurge_ref_aux_cons:
 "ipurge_ref_aux I D U (x # xs) X = ipurge_ref_aux I D (sinks_aux I D U [x]) xs X"
by (subgoal_tac "x # xs = [x] @ xs", simp only: ipurge_ref_aux_append, simp)

lemma process_rule_1_futures:
 "xs ∈ traces P ⟹ ([], {}) ∈ futures P xs"
by (simp add: futures_def, rule traces_failures)

lemma process_rule_3_futures:
 "(ys, Y) ∈ futures P xs ⟹ Y' ⊆ Y ⟹ (ys, Y') ∈ futures P xs"
by (simp add: futures_def, rule process_rule_3)

lemma process_rule_4_futures:
 "(ys, Y) ∈ futures P xs ⟹
    (ys @ [x], {}) ∈ futures P xs ∨ (ys, insert x Y) ∈ futures P xs"
by (simp add: futures_def, subst append_assoc [symmetric], rule process_rule_4)

lemma process_rule_5_general [rule_format]:
 "xs ∈ divergences P ⟶ xs @ ys ∈ divergences P"
proof (induction ys rule: rev_induct, simp, rule impI, simp)
qed (subst append_assoc [symmetric], rule process_rule_5)

text ‹
\null

Here below is the definition of operator \emph{after}, for which a symbolic notation similar to the
one used in \<^cite>‹"R6"› is introduced. Then, it is proven that for any process @{term P} and any trace
@{term xs} of @{term P}, the failures set and the divergences set of @{term P} after @{term xs}
indeed enjoy their respective characteristic properties as defined in \<^cite>‹"R1"›.

\null
›

definition future_divergences :: "'a process ⇒ 'a list ⇒ 'a list set" where
"future_divergences P xs ≡ {ys. xs @ ys ∈ divergences P}"

definition after :: "'a process ⇒ 'a list ⇒ 'a process" (infixl ‹∖› 64) where
"P ∖ xs ≡ Abs_process (futures P xs, future_divergences P xs)"

lemma process_rule_5_futures:
 "ys ∈ future_divergences P xs ⟹ ys @ [x] ∈ future_divergences P xs"
by (simp add: future_divergences_def, subst append_assoc [symmetric],
 rule process_rule_5)

lemma process_rule_6_futures:
 "ys ∈ future_divergences P xs ⟹ (ys, Y) ∈ futures P xs"
by (simp add: futures_def future_divergences_def, rule process_rule_6)

lemma after_rep:
  assumes A: "xs ∈ traces P"
  shows "Rep_process (P ∖ xs) = (futures P xs, future_divergences P xs)"
    (is "_ = ?X")
proof (subst after_def, rule Abs_process_inverse, simp add: process_set_def,
 (subst conj_assoc [symmetric])+, (rule conjI)+)
  show "process_prop_1 ?X"
  proof (simp add: process_prop_1_def)
  qed (rule process_rule_1_futures [OF A])
next
  show "process_prop_2 ?X"
  proof (simp add: process_prop_2_def del: all_simps, (rule allI)+, rule impI)
  qed (rule process_rule_2_futures)
next
  show "process_prop_3 ?X"
  proof (simp add: process_prop_3_def del: all_simps, (rule allI)+, rule impI,
   erule conjE)
  qed (rule process_rule_3_futures)
next
  show "process_prop_4 ?X"
  proof (simp add: process_prop_4_def, (rule allI)+, rule impI)
  qed (rule process_rule_4_futures)
next
  show "process_prop_5 ?X"
  proof (simp add: process_prop_5_def, rule allI, rule impI, rule allI)
  qed (rule process_rule_5_futures)
next
  show "process_prop_6 ?X"
  proof (simp add: process_prop_6_def, rule allI, rule impI, rule allI)
  qed (rule process_rule_6_futures)
qed

lemma after_failures:
  assumes A: "xs ∈ traces P"
  shows "failures (P ∖ xs) = futures P xs"
by (simp add: failures_def after_rep [OF A])

lemma after_futures:
  assumes A: "xs ∈ traces P"
  shows "futures (P ∖ xs) ys = futures P (xs @ ys)"
by (simp add: futures_def after_failures [OF A])

text ‹
\null

Finally, the closure of the futures of a secure process under intransitive purge is proven.

\null
›

lemma after_secure:
  assumes A: "xs ∈ traces P"
  shows "secure P I D ⟹ secure (P ∖ xs) I D"
by (simp add: secure_def after_futures [OF A], blast)

lemma ipurge_tr_ref_aux_futures:
 "⟦secure P I D; (ys, Y) ∈ futures P xs⟧ ⟹
    (ipurge_tr_aux I D U ys, ipurge_ref_aux I D U ys Y) ∈ futures P xs"
proof (subgoal_tac "xs ∈ traces P", simp add: after_failures [symmetric],
 rule ipurge_tr_ref_aux_failures, rule after_secure, assumption+)
qed (simp add: futures_def, drule failures_traces, rule process_rule_2_traces)

lemma ipurge_tr_ref_aux_failures_general:
 "⟦secure P I D; (xs @ ys, Y) ∈ failures P⟧ ⟹
    (xs @ ipurge_tr_aux I D U ys, ipurge_ref_aux I D U ys Y) ∈ failures P"
by (drule ipurge_tr_ref_aux_futures, simp_all add: futures_def)


subsection "Concurrent composition"

text ‹
In \<^cite>‹"R6"›, the concurrent composition of two processes @{term P}, @{term Q}, expressed using
notation ‹P ∥ Q›, is defined as a process whose alphabet is the union of the alphabets of
@{term P} and @{term Q}, so that the shared events requiring the synchronous participation of both
processes are those in the intersection of their alphabets.

In the formalization of Communicating Sequential Processes developed in \<^cite>‹"R1"›, the alphabets of
@{term P} and @{term Q} are the data types @{typ 'a} and @{typ 'b} nested in their respective types
@{typ "'a process"} and @{typ "'b process"}. Therefore, for any two maps @{term "p :: 'a ⇒ 'c"},
@{term "q :: 'b ⇒ 'c"}, the concurrent composition of @{term P} and @{term Q} with respect to
@{term p} and @{term q}, expressed using notation ‹P ∥ Q <p, q>›, is defined in what follows
as a process of type @{typ "'c process"}, where meaningful events are those in
@{term "range p ∪ range q"} and shared events are those in @{term "range p ∩ range q"}.

The case where @{term "- (range p ∪ range q) ≠ {}"} constitutes a generalization of the definition
given in \<^cite>‹"R6"›, and the events in @{term "- (range p ∪ range q)"}, not being mapped to any event
in the alphabets of the input processes, shall be understood as fake events lacking any meaning.
Consistently with this interpretation, such events are allowed to occur in divergent traces only --
necessarily, since divergences are capable by definition of giving rise to any sort of event. As a
result, while in \<^cite>‹"R6"› the refusals associated to non-divergent traces are the union of two
sets, a refusal of @{term P} and a refusal of @{term Q}, in the following definition they are the
union of three sets instead, where the third set is any subset of @{term "- (range p ∪ range q)"}.

Since the definition given in \<^cite>‹"R6"› preserves the identity of the events of the input processes,
a further generalization resulting from the following definition corresponds to the case where
either map @{term p}, @{term q} is not injective. However, as shown below, these generalizations
turn out to compromise neither the compliance of the output of concurrent composition with the
characteristic properties of processes as defined in \<^cite>‹"R1"›, nor even the validity of the target
security conservation theorem.

Since divergences can contain fake events, whereas non-divergent traces cannot, it is necessary to
add divergent failures to the failures set explicitly. The following definition of the divergences
set restricts the definition given in \<^cite>‹"R6"›, as it identifies a divergence with an arbitrary
extension of an event sequence @{term xs} being a divergence of both @{term P} and @{term Q}, rather
than a divergence of either process and a trace of the other one. This is a reasonable restriction,
in that it requires the concurrent composition of @{term P} and @{term Q} to admit a shared event
@{term x} in a divergent trace just in case both @{term P} and @{term Q} diverge and can then accept
@{term x}, analogously to what is required for a non-divergent trace. Anyway, the definitions match
if the input processes do not diverge, which is the case for any process of practical significance
(cf. \<^cite>‹"R6"›).

\null
›

definition con_comp_divergences ::
 "'a process ⇒ 'b process ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ 'c list set" where
"con_comp_divergences P Q p q ≡
  {xs @ ys | xs ys.
    set xs ⊆ range p ∪ range q ∧
    map (inv p) [x←xs. x ∈ range p] ∈ divergences P ∧
    map (inv q) [x←xs. x ∈ range q] ∈ divergences Q}"

definition con_comp_failures ::
 "'a process ⇒ 'b process ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ 'c failure set" where
"con_comp_failures P Q p q ≡
  {(xs, X ∪ Y ∪ Z) | xs X Y Z.
    set xs ⊆ range p ∪ range q ∧
    X ⊆ range p ∧ Y ⊆ range q ∧ Z ⊆ - (range p ∪ range q) ∧
    (map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P ∧
    (map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q} ∪
  {(xs, X). xs ∈ con_comp_divergences P Q p q}"

definition con_comp ::
 "'a process ⇒ 'b process ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ 'c process" where
"con_comp P Q p q ≡
  Abs_process (con_comp_failures P Q p q, con_comp_divergences P Q p q)"

abbreviation con_comp_syntax ::
 "'a process ⇒ 'b process ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ 'c process"
 (‹(_ ∥ _ <_, _>)› 55)
where
"P ∥ Q <p, q> ≡ con_comp P Q p q"

text ‹
\null

Here below is the proof that, for any two processes @{term P}, @{term Q} and any two maps @{term p},
@{term q}, sets @{term "con_comp_failures P Q p q"} and @{term "con_comp_divergences P Q p q"} enjoy
the characteristic properties of the failures and the divergences sets of a process as defined in
\<^cite>‹"R1"›.

\null
›

lemma con_comp_prop_1:
 "([], {}) ∈ con_comp_failures P Q p q"
proof (simp add: con_comp_failures_def)
qed (rule disjI1, rule conjI, (rule process_rule_1)+)

lemma con_comp_prop_2:
 "(xs @ [x], X) ∈ con_comp_failures P Q p q ⟹
    (xs, {}) ∈ con_comp_failures P Q p q"
proof (simp add: con_comp_failures_def del: filter_append,
 erule disjE, (erule exE)+, (erule conjE)+, rule disjI1)
  fix X Y
  assume
    A: "set xs ⊆ range p ∪ range q" and
    B: "(map (inv p) [x←xs @ [x]. x ∈ range p], inv p ` X) ∈ failures P" and
    C: "(map (inv q) [x←xs @ [x]. x ∈ range q], inv q ` Y) ∈ failures Q"
  show "set xs ⊆ range p ∪ range q ∧
    (map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P ∧
    (map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
  proof (simp add: A, rule conjI, cases "x ∈ range p",
   case_tac [3] "x ∈ range q")
    assume "x ∈ range p"
    hence "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], inv p ` X) ∈ failures P"
     using B by simp
    thus "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P"
     by (rule process_rule_2)
  next
    assume "x ∉ range p"
    hence "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P"
     using B by simp
    moreover have "{} ⊆ inv p ` X" ..
    ultimately show "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P"
     by (rule process_rule_3)
  next
    assume "x ∈ range q"
    hence "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], inv q ` Y) ∈ failures Q"
     using C by simp
    thus "(map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
     by (rule process_rule_2)
  next
    assume "x ∉ range q"
    hence "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
     using C by simp
    moreover have "{} ⊆ inv q ` Y" ..
    ultimately show "(map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
     by (rule process_rule_3)
  qed
next
  assume A: "xs @ [x] ∈ con_comp_divergences P Q p q"
  show
   "set xs ⊆ range p ∪ range q ∧
      (map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P ∧
      (map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q ∨
    xs ∈ con_comp_divergences P Q p q"
    (is "?A ∨ _")
  proof (insert A, simp add: con_comp_divergences_def,
   ((erule exE)?, erule conjE)+)
    fix ws ys
    assume
      B: "xs @ [x] = ws @ ys" and
      C: "set ws ⊆ range p ∪ range q" and
      D: "map (inv p) [x←ws. x ∈ range p] ∈ divergences P" and
      E: "map (inv q) [x←ws. x ∈ range q] ∈ divergences Q"
    show "?A ∨ (∃ws'.
      (∃ys'. xs = ws' @ ys') ∧
      set ws' ⊆ range p ∪ range q ∧
      map (inv p) [x←ws'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←ws'. x ∈ range q] ∈ divergences Q)"
      (is "_ ∨ (∃ws'. ?B ws')")
    proof (cases ys, rule disjI1, rule_tac [2] disjI2)
      case Nil
      hence "set (xs @ [x]) ⊆ range p ∪ range q"
       using B and C by simp
      hence "insert x (set xs) ⊆ range p ∪ range q"
       by simp
      moreover have "set xs ⊆ insert x (set xs)"
       by (rule subset_insertI)
      ultimately have "set xs ⊆ range p ∪ range q"
       by simp
      moreover have "map (inv p) [x←xs @ [x]. x ∈ range p] ∈ divergences P"
       using Nil and B and D by simp
      hence "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P"
      proof (cases "x ∈ range p", simp_all)
        assume "map (inv p) [x←xs. x ∈ range p] @ [inv p x] ∈ divergences P"
        hence "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {}) ∈ failures P"
         by (rule process_rule_6)
        thus ?thesis
         by (rule process_rule_2)
      next
        assume "map (inv p) [x←xs. x ∈ range p] ∈ divergences P"
        thus ?thesis
         by (rule process_rule_6)
      qed
      moreover have "map (inv q) [x←xs @ [x]. x ∈ range q] ∈ divergences Q"
       using Nil and B and E by simp
      hence "(map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
      proof (cases "x ∈ range q", simp_all)
        assume "map (inv q) [x←xs. x ∈ range q] @ [inv q x] ∈ divergences Q"
        hence "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], {}) ∈ failures Q"
         by (rule process_rule_6)
        thus ?thesis
         by (rule process_rule_2)
      next
        assume "map (inv q) [x←xs. x ∈ range q] ∈ divergences Q"
        thus ?thesis
         by (rule process_rule_6)
      qed
      ultimately show ?A
       by blast
    next
      case Cons
      moreover have "butlast (xs @ [x]) = butlast (ws @ ys)"
       using B by simp
      ultimately have "xs = ws @ butlast ys"
       by (simp add: butlast_append)
      hence "∃ys'. xs = ws @ ys'" ..
      hence "?B ws"
       using C and D and E by simp
      thus "∃ws'. ?B ws'" ..
    qed
  qed
qed

lemma con_comp_prop_3:
 "⟦(xs, Y) ∈ con_comp_failures P Q p q; X ⊆ Y⟧ ⟹
    (xs, X) ∈ con_comp_failures P Q p q"
proof (simp add: con_comp_failures_def, erule disjE, simp_all,
 (erule exE)+, (erule conjE)+, rule disjI1, simp)
  fix X' Y' Z'
  assume
    A: "X ⊆ X' ∪ Y' ∪ Z'" and
    B: "X' ⊆ range p" and
    C: "Y' ⊆ range q" and
    D: "Z' ⊆ - range p" and
    E: "Z' ⊆ - range q" and
    F: "(map (inv p) [x←xs. x ∈ range p], inv p ` X') ∈ failures P" and
    G: "(map (inv q) [x←xs. x ∈ range q], inv q ` Y') ∈ failures Q"
  show "∃X' Y' Z'.
    X = X' ∪ Y' ∪ Z' ∧
    X' ⊆ range p ∧
    Y' ⊆ range q ∧
    Z' ⊆ - range p ∧
    Z' ⊆ - range q ∧
    (map (inv p) [x←xs. x ∈ range p], inv p ` X') ∈ failures P ∧
    (map (inv q) [x←xs. x ∈ range q], inv q ` Y') ∈ failures Q"
  proof (rule_tac x = "X' ∩ X" in exI, rule_tac x = "Y' ∩ X" in exI,
   rule_tac x = "Z' ∩ X" in exI, (subst conj_assoc [symmetric])+, (rule conjI)+)
    show "X = X' ∩ X ∪ Y' ∩ X ∪ Z' ∩ X"
     using A by blast
  next
    show "X' ∩ X ⊆ range p"
     using B by blast
  next
    show "Y' ∩ X ⊆ range q"
     using C by blast
  next
    show "Z' ∩ X ⊆ - range p"
     using D by blast
  next
    show "Z' ∩ X ⊆ - range q"
     using E by blast
  next
    have "inv p ` (X' ∩ X) ⊆ inv p ` X'"
     by blast
    with F show "(map (inv p) [x←xs. x ∈ range p], inv p ` (X' ∩ X))
      ∈ failures P"
     by (rule process_rule_3)
  next
    have "inv q ` (Y' ∩ X) ⊆ inv q ` Y'"
     by blast
    with G show "(map (inv q) [x←xs. x ∈ range q], inv q ` (Y' ∩ X))
      ∈ failures Q"
     by (rule process_rule_3)
  qed
qed

lemma con_comp_prop_4:
 "(xs, X) ∈ con_comp_failures P Q p q ⟹
    (xs @ [x], {}) ∈ con_comp_failures P Q p q ∨
    (xs, insert x X) ∈ con_comp_failures P Q p q"
proof (simp add: con_comp_failures_def del: filter_append,
 erule disjE, (erule exE)+, (erule conjE)+, simp_all del: filter_append)
  fix X Y Z
  assume
    A: "X ⊆ range p" and
    B: "Y ⊆ range q" and
    C: "Z ⊆ - range p" and
    D: "Z ⊆ - range q" and
    E: "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P" and
    F: "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
  show
   "(x ∈ range p ∨ x ∈ range q) ∧
      (map (inv p) [x←xs @ [x]. x ∈ range p], {}) ∈ failures P ∧
      (map (inv q) [x←xs @ [x]. x ∈ range q], {}) ∈ failures Q ∨
    xs @ [x] ∈ con_comp_divergences P Q p q ∨
    (∃X' Y' Z'.
      insert x (X ∪ Y ∪ Z) = X' ∪ Y' ∪ Z' ∧
      X' ⊆ range p ∧
      Y' ⊆ range q ∧
      Z' ⊆ - range p ∧
      Z' ⊆ - range q ∧
      (map (inv p) [x←xs. x ∈ range p], inv p ` X') ∈ failures P ∧
      (map (inv q) [x←xs. x ∈ range q], inv q ` Y') ∈ failures Q) ∨
    xs ∈ con_comp_divergences P Q p q"
    (is "_ ∨ _ ∨ ?A ∨ _")
  proof (cases "x ∈ range p", case_tac [!] "x ∈ range q", simp_all)
    assume
      G: "x ∈ range p" and
      H: "x ∈ range q"
    show
     "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {}) ∈ failures P ∧
        (map (inv q) [x←xs. x ∈ range q] @ [inv q x], {}) ∈ failures Q ∨
      xs @ [x] ∈ con_comp_divergences P Q p q ∨
      ?A ∨
      xs ∈ con_comp_divergences P Q p q"
      (is "?B ∨ _")
    proof (cases ?B, simp_all del: disj_not1, erule disjE)
      assume
        I: "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {}) ∉ failures P"
      have ?A
      proof (rule_tac x = "insert x X" in exI, rule_tac x = "Y" in exI,
       rule_tac x = "Z" in exI, (subst conj_assoc [symmetric])+, (rule conjI)+)
        show "insert x (X ∪ Y ∪ Z) = insert x X ∪ Y ∪ Z"
         by simp
      next
        show "insert x X ⊆ range p"
         using A and G by simp
      next
        show "Y ⊆ range q"
         using B .
      next
        show "Z ⊆ - range p"
         using C .
      next
        show "Z ⊆ - range q"
         using D .
      next
        have
         "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {})
            ∈ failures P ∨
          (map (inv p) [x←xs. x ∈ range p], insert (inv p x) (inv p ` X))
            ∈ failures P"
         using E by (rule process_rule_4)
        thus "(map (inv p) [x←xs. x ∈ range p], inv p ` insert x X) ∈ failures P"
         using I by simp
      next
        show "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
         using F .
      qed
      thus ?thesis
       by simp
    next
      assume
        I: "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], {}) ∉ failures Q"
      have ?A
      proof (rule_tac x = "X" in exI, rule_tac x = "insert x Y" in exI,
       rule_tac x = "Z" in exI, (subst conj_assoc [symmetric])+, (rule conjI)+)
        show "insert x (X ∪ Y ∪ Z) = X ∪ insert x Y ∪ Z"
         by simp
      next
        show "X ⊆ range p"
         using A .
      next
        show "insert x Y ⊆ range q"
         using B and H by simp
      next
        show "Z ⊆ - range p"
         using C .
      next
        show "Z ⊆ - range q"
         using D .
      next
        show "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P"
         using E .
      next
        have
         "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], {})
            ∈ failures Q ∨
          (map (inv q) [x←xs. x ∈ range q], insert (inv q x) (inv q ` Y))
            ∈ failures Q"
         using F by (rule process_rule_4)
        thus "(map (inv q) [x←xs. x ∈ range q], inv q ` insert x Y) ∈ failures Q"
         using I by simp
      qed
      thus ?thesis
       by simp
    qed
  next
    assume G: "x ∈ range p"
    show
     "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {}) ∈ failures P ∧
        (map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q ∨
      xs @ [x] ∈ con_comp_divergences P Q p q ∨
      ?A ∨
      xs ∈ con_comp_divergences P Q p q"
    proof (cases "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {})
     ∈ failures P")
      case True
      moreover have "{} ⊆ inv q ` Y" ..
      with F have "(map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
       by (rule process_rule_3)
      ultimately show ?thesis
       by simp
    next
      case False
      have ?A
      proof (rule_tac x = "insert x X" in exI, rule_tac x = "Y" in exI,
       rule_tac x = "Z" in exI, (subst conj_assoc [symmetric])+, (rule conjI)+)
        show "insert x (X ∪ Y ∪ Z) = insert x X ∪ Y ∪ Z"
         by simp
      next
        show "insert x X ⊆ range p"
         using A and G by simp
      next
        show "Y ⊆ range q"
         using B .
      next
        show "Z ⊆ - range p"
         using C .
      next
        show "Z ⊆ - range q"
         using D .
      next
        have
         "(map (inv p) [x←xs. x ∈ range p] @ [inv p x], {})
            ∈ failures P ∨
          (map (inv p) [x←xs. x ∈ range p], insert (inv p x) (inv p ` X))
            ∈ failures P"
         using E by (rule process_rule_4)
        thus "(map (inv p) [x←xs. x ∈ range p], inv p ` insert x X) ∈ failures P"
         using False by simp
      next
        show "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
         using F .
      qed
      thus ?thesis
       by simp
    qed
  next
    assume G: "x ∈ range q"
    show
     "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P ∧
        (map (inv q) [x←xs. x ∈ range q] @ [inv q x], {}) ∈ failures Q ∨
      xs @ [x] ∈ con_comp_divergences P Q p q ∨
      ?A ∨
      xs ∈ con_comp_divergences P Q p q"
    proof (cases "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], {})
     ∈ failures Q")
      case True
      moreover have "{} ⊆ inv p ` X" ..
      with E have "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P"
       by (rule process_rule_3)
      ultimately show ?thesis
       by simp
    next
      case False
      have ?A
      proof (rule_tac x = "X" in exI, rule_tac x = "insert x Y" in exI,
       rule_tac x = "Z" in exI, (subst conj_assoc [symmetric])+, (rule conjI)+)
        show "insert x (X ∪ Y ∪ Z) = X ∪ insert x Y ∪ Z"
         by simp
      next
        show "X ⊆ range p"
         using A .
      next
        show "insert x Y ⊆ range q"
         using B and G by simp
      next
        show "Z ⊆ - range p"
         using C .
      next
        show "Z ⊆ - range q"
         using D .
      next
        show "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P"
         using E .
      next
        have
         "(map (inv q) [x←xs. x ∈ range q] @ [inv q x], {})
            ∈ failures Q ∨
          (map (inv q) [x←xs. x ∈ range q], insert (inv q x) (inv q ` Y))
            ∈ failures Q"
         using F by (rule process_rule_4)
        thus "(map (inv q) [x←xs. x ∈ range q], inv q ` insert x Y) ∈ failures Q"
         using False by simp
      qed
      thus ?thesis
       by simp
    qed
  next
    assume
      G: "x ∉ range p" and
      H: "x ∉ range q"
    have ?A
    proof (rule_tac x = "X" in exI, rule_tac x = "Y" in exI,
     rule_tac x = "insert x Z" in exI, (subst conj_assoc [symmetric])+,
     (rule conjI)+)
      show "insert x (X ∪ Y ∪ Z) = X ∪ Y ∪ insert x Z"
       by simp
    next
      show "X ⊆ range p"
       using A .
    next
      show "Y ⊆ range q"
       using B .
    next
      show "insert x Z ⊆ - range p"
       using C and G by simp
    next
      show "insert x Z ⊆ - range q"
       using D and H by simp
    next
      show "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P"
       using E .
    next
      show "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
       using F .
    qed
    thus
     "xs @ [x] ∈ con_comp_divergences P Q p q ∨
      ?A ∨
      xs ∈ con_comp_divergences P Q p q"
     by simp
  qed
qed

lemma con_comp_prop_5:
 "xs ∈ con_comp_divergences P Q p q ⟹
    xs @ [x] ∈ con_comp_divergences P Q p q"
proof (simp add: con_comp_divergences_def, erule exE, (erule conjE)+, erule exE)
  fix xs' ys'
  assume
    A: "set xs' ⊆ range p ∪ range q" and
    B: "map (inv p) [x←xs'. x ∈ range p] ∈ divergences P" and
    C: "map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q" and
    D: "xs = xs' @ ys'"
  show "∃xs'.
    (∃ys'. xs @ [x] = xs' @ ys') ∧
    set xs' ⊆ range p ∪ range q ∧
    map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
    map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q"
  proof (rule_tac x = xs' in exI, simp_all add: A B C)
  qed (rule_tac x = "ys' @ [x]" in exI, simp add: D)
qed

lemma con_comp_prop_6:
 "xs ∈ con_comp_divergences P Q p q ⟹
    (xs, X) ∈ con_comp_failures P Q p q"
by (simp add: con_comp_failures_def)

lemma con_comp_rep:
 "Rep_process (P ∥ Q <p, q>) =
    (con_comp_failures P Q p q, con_comp_divergences P Q p q)"
  (is "_ = ?X")
proof (subst con_comp_def, rule Abs_process_inverse, simp add: process_set_def,
 (subst conj_assoc [symmetric])+, (rule conjI)+)
  show "process_prop_1 ?X"
  proof (simp add: process_prop_1_def)
  qed (rule con_comp_prop_1)
next
  show "process_prop_2 ?X"
  proof (simp add: process_prop_2_def del: all_simps, (rule allI)+, rule impI)
  qed (rule con_comp_prop_2)
next
  show "process_prop_3 ?X"
  proof (simp add: process_prop_3_def del: all_simps, (rule allI)+, rule impI,
   erule conjE)
  qed (rule con_comp_prop_3)
next
  show "process_prop_4 ?X"
  proof (simp add: process_prop_4_def, (rule allI)+, rule impI)
  qed (rule con_comp_prop_4)
next
  show "process_prop_5 ?X"
  proof (simp add: process_prop_5_def, rule allI, rule impI, rule allI)
  qed (rule con_comp_prop_5)
next
  show "process_prop_6 ?X"
  proof (simp add: process_prop_6_def, rule allI, rule impI, rule allI)
  qed (rule con_comp_prop_6)
qed

text ‹
\null

Here below, the previous result is applied to derive useful expressions for the outputs of the
functions returning the elements of a process, as defined in \<^cite>‹"R1"› and \<^cite>‹"R2"›, when acting on
the concurrent composition of a pair of processes.

\null
›

lemma con_comp_failures:
 "failures (P ∥ Q <p, q>) = con_comp_failures P Q p q"
by (simp add: failures_def con_comp_rep)

lemma con_comp_divergences:
 "divergences (P ∥ Q <p, q>) = con_comp_divergences P Q p q"
by (simp add: divergences_def con_comp_rep)

lemma con_comp_futures:
 "futures (P ∥ Q <p, q>) xs =
    {(ys, Y). (xs @ ys, Y) ∈ con_comp_failures P Q p q}"
by (simp add: futures_def con_comp_failures)

lemma con_comp_traces:
 "traces (P ∥ Q <p, q>) = Domain (con_comp_failures P Q p q)"
by (simp add: traces_def con_comp_failures)

lemma con_comp_refusals:
 "refusals (P ∥ Q <p, q>) xs ≡ con_comp_failures P Q p q `` {xs}"
by (simp add: refusals_def con_comp_failures)

lemma con_comp_next_events:
 "next_events (P ∥ Q <p, q>) xs =
    {x. xs @ [x] ∈ Domain (con_comp_failures P Q p q)}"
by (simp add: next_events_def con_comp_traces)

text ‹
\null

In what follows, three lemmas are proven. The first one, whose proof makes use of the axiom of
choice, establishes an additional property required for the above definition of concurrent
composition to be correct, namely that for any two processes whose refusals are closed under set
union, their concurrent composition still be such, which is what is expected for any process of
practical significance (cf. \<^cite>‹"R2"›). The other two lemmas are auxiliary properties of concurrent
composition used in the proof of the target security conservation theorem.

\null
›

lemma con_comp_ref_union_closed:
  assumes
    A: "ref_union_closed P" and
    B: "ref_union_closed Q"
  shows "ref_union_closed (P ∥ Q <p, q>)"
proof (simp add: ref_union_closed_def con_comp_failures con_comp_failures_def
 con_comp_divergences_def del: SUP_identity_eq cong: SUP_cong_simp, (rule allI)+, (rule impI)+,
 erule exE, rule disjI1)
  fix xs A X
  assume "∀X ∈ A. ∃R S T.
    X = R ∪ S ∪ T ∧
    set xs ⊆ range p ∪ range q ∧
    R ⊆ range p ∧
    S ⊆ range q ∧
    T ⊆ - range p ∧
    T ⊆ - range q ∧
    (map (inv p) [x←xs. x ∈ range p], inv p ` R) ∈ failures P ∧
    (map (inv q) [x←xs. x ∈ range q], inv q ` S) ∈ failures Q"
    (is "∀X ∈ A. ∃R S T. ?F X R S T")
  hence "∃r. ∀X ∈ A. ∃S T. ?F X (r X) S T"
   by (rule bchoice)
  then obtain r where "∀X ∈ A. ∃S T. ?F X (r X) S T" ..
  hence "∃s. ∀X ∈ A. ∃T. ?F X (r X) (s X) T"
   by (rule bchoice)
  then obtain s where "∀X ∈ A. ∃T. ?F X (r X) (s X) T" ..
  hence "∃t. ∀X ∈ A. ?F X (r X) (s X) (t X)"
   by (rule bchoice)
  then obtain t where C: "∀X ∈ A. ?F X (r X) (s X) (t X)" ..
  assume D: "X ∈ A"
  show "∃R S T. ?F (⋃X ∈ A. X) R S T"
  proof (rule_tac x = "⋃X ∈ A. r X" in exI, rule_tac x = "⋃X ∈ A. s X" in exI,
   rule_tac x = "⋃X ∈ A. t X" in exI, (subst conj_assoc [symmetric])+,
   (rule conjI)+)
    show "(⋃X ∈ A. X) = (⋃X ∈ A. r X) ∪ (⋃X ∈ A. s X) ∪ (⋃X ∈ A. t X)"
    proof (simp add: set_eq_iff, rule allI, rule iffI, erule_tac [2] disjE,
     erule_tac [3] disjE, erule_tac [!] bexE)
      fix x X
      have "∀X ∈ A. X = r X ∪ s X ∪ t X"
       using C by simp
      moreover assume E: "X ∈ A"
      ultimately have "X = r X ∪ s X ∪ t X" ..
      moreover assume "x ∈ X"
      ultimately have "x ∈ r X ∨ x ∈ s X ∨ x ∈ t X"
       by blast
      hence "∃X ∈ A. x ∈ r X ∨ x ∈ s X ∨ x ∈ t X"
       using E ..
      thus "(∃X ∈ A. x ∈ r X) ∨ (∃X ∈ A. x ∈ s X) ∨ (∃X ∈ A. x ∈ t X)"
       by blast
    next
      fix x X
      have "∀X ∈ A. X = r X ∪ s X ∪ t X"
       using C by simp
      moreover assume E: "X ∈ A"
      ultimately have "X = r X ∪ s X ∪ t X" ..
      moreover assume "x ∈ r X"
      ultimately have "x ∈ X"
       by blast
      thus "∃X ∈ A. x ∈ X"
       using E ..
    next
      fix x X
      have "∀X ∈ A. X = r X ∪ s X ∪ t X"
       using C by simp
      moreover assume E: "X ∈ A"
      ultimately have "X = r X ∪ s X ∪ t X" ..
      moreover assume "x ∈ s X"
      ultimately have "x ∈ X"
       by blast
      thus "∃X ∈ A. x ∈ X"
       using E ..
    next
      fix x X
      have "∀X ∈ A. X = r X ∪ s X ∪ t X"
       using C by simp
      moreover assume E: "X ∈ A"
      ultimately have "X = r X ∪ s X ∪ t X" ..
      moreover assume "x ∈ t X"
      ultimately have "x ∈ X"
       by blast
      thus "∃X ∈ A. x ∈ X"
       using E ..
    qed
  next
    have "∀X ∈ A. set xs ⊆ range p ∪ range q"
     using C by simp
    thus "set xs ⊆ range p ∪ range q"
     using D ..
  next
    show "(⋃X ∈ A. r X) ⊆ range p"
    proof (rule subsetI, erule UN_E)
      fix x X
      have "∀X ∈ A. r X ⊆ range p"
       using C by simp
      moreover assume "X ∈ A"
      ultimately have "r X ⊆ range p" ..
      moreover assume "x ∈ r X"
      ultimately show "x ∈ range p" ..
    qed
  next
    show "(⋃X ∈ A. s X) ⊆ range q"
    proof (rule subsetI, erule UN_E)
      fix x X
      have "∀X ∈ A. s X ⊆ range q"
       using C by simp
      moreover assume "X ∈ A"
      ultimately have "s X ⊆ range q" ..
      moreover assume "x ∈ s X"
      ultimately show "x ∈ range q" ..
    qed
  next
    show "(⋃X ∈ A. t X) ⊆ - range p"
    proof (rule subsetI, erule UN_E)
      fix x X
      have "∀X ∈ A. t X ⊆ - range p"
       using C by simp
      moreover assume "X ∈ A"
      ultimately have "t X ⊆ - range p" ..
      moreover assume "x ∈ t X"
      ultimately show "x ∈ - range p" ..
    qed
  next
    show "(⋃X ∈ A. t X) ⊆ - range q"
    proof (rule subsetI, erule UN_E)
      fix x X
      have "∀X ∈ A. t X ⊆ - range q"
       using C by simp
      moreover assume "X ∈ A"
      ultimately have "t X ⊆ - range q" ..
      moreover assume "x ∈ t X"
      ultimately show "x ∈ - range q" ..
    qed
  next
    let ?A' = "{inv p ` X | X. X ∈ r ` A}"
    have
     "(∃X. X ∈ ?A') ⟶
      (∀X ∈ ?A'. (map (inv p) [x←xs. x ∈ range p], X) ∈ failures P) ⟶
        (map (inv p) [x←xs. x ∈ range p], ⋃X ∈ ?A'. X) ∈ failures P"
     using A by (simp add: ref_union_closed_def)
    moreover have "∃X. X ∈ ?A'"
     using D by blast
    ultimately have
     "(∀X ∈ ?A'. (map (inv p) [x←xs. x ∈ range p], X) ∈ failures P) ⟶
        (map (inv p) [x←xs. x ∈ range p], ⋃X ∈ ?A'. X) ∈ failures P" ..
    moreover have
     "∀X ∈ ?A'. (map (inv p) [x←xs. x ∈ range p], X) ∈ failures P"
    proof (rule ballI, simp, erule exE, erule conjE)
      fix R R'
      assume "R ∈ r ` A"
      hence "∃X ∈ A. R = r X"
       by (simp add: image_iff)
      then obtain X where E: "X ∈ A" and F: "R = r X" ..
      have "∀X ∈ A. (map (inv p) [x←xs. x ∈ range p], inv p ` r X) ∈ failures P"
       using C by simp
      hence "(map (inv p) [x←xs. x ∈ range p], inv p ` r X) ∈ failures P"
       using E ..
      moreover assume "R' = inv p ` R"
      ultimately show "(map (inv p) [x←xs. x ∈ range p], R') ∈ failures P"
       using F by simp
    qed
    ultimately have "(map (inv p) [x←xs. x ∈ range p], ⋃X ∈ ?A'. X)
      ∈ failures P" ..
    moreover have "(⋃X ∈ ?A'. X) = inv p ` (⋃X ∈ A. r X)"
    proof (subst set_eq_iff, simp, rule allI, rule iffI, (erule exE, erule conjE)+)
      fix a R R'
      assume "R ∈ r ` A"
      hence "∃X ∈ A. R = r X"
       by (simp add: image_iff)
      then obtain X where E: "X ∈ A" and F: "R = r X" ..
      assume "a ∈ R'" and "R' = inv p ` R"
      hence "a ∈ inv p ` r X"
       using F by simp
      hence "∃x ∈ r X. a = inv p x"
       by (simp add: image_iff)
      then obtain x where G: "x ∈ r X" and H: "a = inv p x" ..
      have "x ∈ (⋃X ∈ A. r X)"
       using E and G by (rule UN_I)
      with H have "∃x ∈ (⋃X ∈ A. r X). a = inv p x" ..
      thus "a ∈ inv p ` (⋃X ∈ A. r X)"
       by (simp add: image_iff)
    next
      fix a
      assume "a ∈ inv p ` (⋃X ∈ A. r X)"
      hence "∃x ∈ (⋃X ∈ A. r X). a = inv p x"
       by (simp add: image_iff)
      then obtain x where E: "x ∈ (⋃X ∈ A. r X)" and F: "a = inv p x" ..
      obtain X where G: "X ∈ A" and H: "x ∈ r X" using E ..
      show "∃R'. (∃R. R' = inv p ` R ∧ R ∈ r ` A) ∧ a ∈ R'"
      proof (rule_tac x = "inv p ` r X" in exI, rule conjI,
       rule_tac x = "r X" in exI)
      qed (rule_tac [2] image_eqI, simp add: G, simp add: F, simp add: H)
    qed
    ultimately show "(map (inv p) [x←xs. x ∈ range p], inv p ` (⋃X ∈ A. r X))
      ∈ failures P"
     by simp
  next
    let ?A' = "{inv q ` X | X. X ∈ s ` A}"
    have
     "(∃X. X ∈ ?A') ⟶
      (∀X ∈ ?A'. (map (inv q) [x←xs. x ∈ range q], X) ∈ failures Q) ⟶
        (map (inv q) [x←xs. x ∈ range q], ⋃X ∈ ?A'. X) ∈ failures Q"
     using B by (simp add: ref_union_closed_def)
    moreover have "∃X. X ∈ ?A'"
     using D by blast
    ultimately have
     "(∀X ∈ ?A'. (map (inv q) [x←xs. x ∈ range q], X) ∈ failures Q) ⟶
        (map (inv q) [x←xs. x ∈ range q], ⋃X ∈ ?A'. X) ∈ failures Q" ..
    moreover have
     "∀X ∈ ?A'. (map (inv q) [x←xs. x ∈ range q], X) ∈ failures Q"
    proof (rule ballI, simp, erule exE, erule conjE)
      fix S S'
      assume "S ∈ s ` A"
      hence "∃X ∈ A. S = s X"
       by (simp add: image_iff)
      then obtain X where E: "X ∈ A" and F: "S = s X" ..
      have "∀X ∈ A. (map (inv q) [x←xs. x ∈ range q], inv q ` s X) ∈ failures Q"
       using C by simp
      hence "(map (inv q) [x←xs. x ∈ range q], inv q ` s X) ∈ failures Q"
       using E ..
      moreover assume "S' = inv q ` S"
      ultimately show "(map (inv q) [x←xs. x ∈ range q], S') ∈ failures Q"
       using F by simp
    qed
    ultimately have "(map (inv q) [x←xs. x ∈ range q], ⋃X ∈ ?A'. X)
      ∈ failures Q" ..
    moreover have "(⋃X ∈ ?A'. X) = inv q ` (⋃X ∈ A. s X)"
    proof (subst set_eq_iff, simp, rule allI, rule iffI, (erule exE, erule conjE)+)
      fix b S S'
      assume "S ∈ s ` A"
      hence "∃X ∈ A. S = s X"
       by (simp add: image_iff)
      then obtain X where E: "X ∈ A" and F: "S = s X" ..
      assume "b ∈ S'" and "S' = inv q ` S"
      hence "b ∈ inv q ` s X"
       using F by simp
      hence "∃x ∈ s X. b = inv q x"
       by (simp add: image_iff)
      then obtain x where G: "x ∈ s X" and H: "b = inv q x" ..
      have "x ∈ (⋃X ∈ A. s X)"
       using E and G by (rule UN_I)
      with H have "∃x ∈ (⋃X ∈ A. s X). b = inv q x" ..
      thus "b ∈ inv q ` (⋃X ∈ A. s X)"
       by (simp add: image_iff)
    next
      fix b
      assume "b ∈ inv q ` (⋃X ∈ A. s X)"
      hence "∃x ∈ (⋃X ∈ A. s X). b = inv q x"
       by (simp add: image_iff)
      then obtain x where E: "x ∈ (⋃X ∈ A. s X)" and F: "b = inv q x" ..
      obtain X where G: "X ∈ A" and H: "x ∈ s X" using E ..
      show "∃S'. (∃S. S' = inv q ` S ∧ S ∈ s ` A) ∧ b ∈ S'"
      proof (rule_tac x = "inv q ` s X" in exI, rule conjI,
       rule_tac x = "s X" in exI)
      qed (rule_tac [2] image_eqI, simp add: G, simp add: F, simp add: H)
    qed
    ultimately show "(map (inv q) [x←xs. x ∈ range q], inv q ` (⋃X ∈ A. s X))
      ∈ failures Q"
     by simp
  qed
qed

lemma con_comp_failures_traces:
 "(xs, X) ∈ con_comp_failures P Q p q ⟹
    map (inv p) [x←xs. x ∈ range p] ∈ traces P ∧
    map (inv q) [x←xs. x ∈ range q] ∈ traces Q"
proof (simp add: con_comp_failures_def con_comp_divergences_def, erule disjE,
 (erule exE)+, (erule conjE)+, erule_tac [2] exE, (erule_tac [2] conjE)+,
 erule_tac [2] exE)
  fix X Y
  assume "(map (inv p) [x←xs. x ∈ range p], inv p ` X) ∈ failures P"
  hence "map (inv p) [x←xs. x ∈ range p] ∈ traces P"
   by (rule failures_traces)
  moreover assume "(map (inv q) [x←xs. x ∈ range q], inv q ` Y) ∈ failures Q"
  hence "map (inv q) [x←xs. x ∈ range q] ∈ traces Q"
   by (rule failures_traces)
  ultimately show ?thesis ..
next
  fix vs ws
  assume A: "xs = vs @ ws"
  assume "map (inv p) [x←vs. x ∈ range p] ∈ divergences P"
  hence "map (inv p) [x←vs. x ∈ range p] @ map (inv p) [x←ws. x ∈ range p]
    ∈ divergences P"
   by (rule process_rule_5_general)
  hence "map (inv p) [x←xs. x ∈ range p] ∈ divergences P"
   using A by simp
  hence "(map (inv p) [x←xs. x ∈ range p], {}) ∈ failures P"
   by (rule process_rule_6)
  hence "map (inv p) [x←xs. x ∈ range p] ∈ traces P"
   by (rule failures_traces)
  moreover assume "map (inv q) [x←vs. x ∈ range q] ∈ divergences Q"
  hence "map (inv q) [x←vs. x ∈ range q] @ map (inv q) [x←ws. x ∈ range q]
    ∈ divergences Q"
   by (rule process_rule_5_general)
  hence "map (inv q) [x←xs. x ∈ range q] ∈ divergences Q"
   using A by simp
  hence "(map (inv q) [x←xs. x ∈ range q], {}) ∈ failures Q"
   by (rule process_rule_6)
  hence "map (inv q) [x←xs. x ∈ range q] ∈ traces Q"
   by (rule failures_traces)
  ultimately show ?thesis ..
qed

lemma con_comp_failures_divergences:
 "(xs @ y # ys, Y) ∈ con_comp_failures P Q p q ⟹
  y ∉ range p ⟹
  y ∉ range q ⟹
    ∃xs'.
      (∃ys'. xs @ zs = xs' @ ys') ∧
      set xs' ⊆ range p ∪ range q ∧
      map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q"
proof (simp add: con_comp_failures_def con_comp_divergences_def,
 erule exE, (erule conjE)+, erule exE)
  fix xs' ys'
  assume
    A: "y ∉ range p" and
    B: "y ∉ range q" and
    C: "set xs' ⊆ range p ∪ range q" and
    D: "map (inv p) [x←xs'. x ∈ range p] ∈ divergences P" and
    E: "map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q" and
    F: "xs @ y # ys = xs' @ ys'"
  have "length xs' ≤ length xs"
  proof (rule ccontr)
    assume "¬ length xs' ≤ length xs"
    moreover have "take (length xs') (xs @ [y] @ ys) =
      take (length xs') (xs @ [y]) @ take (length xs' - Suc (length xs)) ys"
      (is "_ = _ @ ?vs")
     by (simp only: take_append, simp)
    ultimately have "take (length xs') (xs @ y # ys) = xs @ y # ?vs"
     by simp
    moreover have "take (length xs') (xs @ y # ys) =
      take (length xs') (xs' @ ys')"
     using F by simp
    ultimately have "xs' = xs @ y # ?vs"
     by simp
    hence "set (xs @ y # ?vs) ⊆ range p ∪ range q"
     using C by simp
    hence "y ∈ range p ∪ range q"
     by simp
    thus False
     using A and B by simp
  qed
  moreover have "xs @ zs =
    take (length xs') (xs @ zs) @ drop (length xs') (xs @ zs)"
    (is "_ = _ @ ?vs")
   by (simp only: append_take_drop_id)
  ultimately have "xs @ zs = take (length xs') (xs @ y # ys) @ ?vs"
   by simp
  moreover have "take (length xs') (xs @ y # ys) =
    take (length xs') (xs' @ ys')"
   using F by simp
  ultimately have G: "xs @ zs = xs' @ ?vs"
   by (simp del: take_append, simp)
  show ?thesis
  proof (rule_tac x = xs' in exI, rule conjI, rule_tac x = ?vs in exI)
  qed (subst G, simp_all add: C D E)
qed

text ‹
\null

In order to prove that CSP noninterference security is conserved under concurrent composition, the
first issue to be solved is to identify the noninterference policy @{term I'} and the event-domain
map @{term D'} with respect to which the output process is secure.

If the events of the input processes corresponding to those of the output process contained in
@{term "range p ∩ range q"} were mapped by the respective event-domain maps @{term D}, @{term E}
into distinct security domains, there would be no criterion for determining the domains of the
aforesaid events of the output process, due to the equivalence of the input processes ensuing from
the commutative property of concurrent composition. Therefore, @{term D} and @{term E} must map the
events of the input processes into security domains of the same type @{typ 'd}, and for each
@{term x} in @{term "range p ∩ range q"}, @{term D} and @{term E} must map the events of the input
processes corresponding to @{term x} into the same domain. This requirement is formalized here below
by means of predicate ‹consistent_maps›.

Similarly, if distinct noninterference policies applied to the input processes, there would exist
some ordered pair of security domains included in one of the policies, but not in the other one.
Thus, again, there would be no criterion for determining the inclusion of such a pair of domains in
the policy @{term I'} applying to the output process. As a result, the input processes are required
to enforce the same noninterference policy @{term I}, so that for any two domains @{term d},
@{term e} of type @{typ 'd}, the ordered pair comprised of the corresponding security domains for
the output process will be included in @{term I'} just in case @{term "(d, e) ∈ I"}.

However, in case @{term "- (range p ∪ range q) ≠ {}"}, the event-domain map @{term D'} for the
output process must assign a security domain to the fake events in @{term "- (range p ∪ range q)"}
as well. Since such events lack any meaning, they may all be mapped to the same security domain,
distinct from the domains of the meaningful events in @{term "range p ∪ range q"}. A simple way to
do this is to identify the type of the security domains for the output process with
@{typ "'d option"}. Then, for any meaningful event @{term x}, @{term D'} will assign @{term x} to
domain @{term "Some d"}, where @{term d} is the domain of the events of the input processes mapped
to @{term x}, whereas @{term "D' y = None"} for any fake event @{term y}. Such an event-domain map,
denoted using notation @{term "con_comp_map D E p q"}, is defined here below.

Therefore, for any two security domains @{term "Some d"}, @{term "Some e"} for the output process,
the above considerations about policy @{term I'} entail that @{term "(Some d, Some e) ∈ I'"} just in
case @{term "(d, e) ∈ I"}. Furthermore, since fake events may only occur in divergent traces, which
are extensions of divergences of the input processes comprised of meaningful events, @{term I'} must
allow the security domain @{term None} of fake events to be affected by any meaningful domain
matching pattern ‹Some _›. Such a noninterference policy, denoted using notation
@{term "con_comp_pol I"}, is defined here below. Observe that @{term "con_comp_pol I"} keeps being
reflexive or transitive if @{term I} is.

\null
›

definition con_comp_pol ::
 "('d × 'd) set ⇒ ('d option × 'd option) set" where
"con_comp_pol I ≡
  {(Some d, Some e) | d e. (d, e) ∈ I} ∪ {(u, v). v = None}"

function con_comp_map ::
 "('a ⇒ 'd) ⇒ ('b ⇒ 'd) ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ 'c ⇒ 'd option" where
"x ∈ range p ⟹
  con_comp_map D E p q x = Some (D (inv p x))" |
"x ∉ range p ⟹ x ∈ range q ⟹
  con_comp_map D E p q x = Some (E (inv q x))" |
"x ∉ range p ⟹ x ∉ range q ⟹
  con_comp_map D E p q x = None"
by (atomize_elim, simp_all add: split_paired_all, blast)
termination by lexicographic_order

definition consistent_maps ::
 "('a ⇒ 'd) ⇒ ('b ⇒ 'd) ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ bool" where
"consistent_maps D E p q ≡
  ∀x ∈ range p ∩ range q. D (inv p x) = E (inv q x)"


subsection "Auxiliary intransitive purge functions"

text ‹
Let @{term I} be a noninterference policy, @{term D} an event-domain map, @{term U} a domain set,
and @{term "xs = x # xs'"} an event list. Suppose to take event @{term x} just in case it satisfies
predicate @{term P}, to append @{term xs'} to the resulting list (matching either @{term "[x]"} or
@{term "[]"}), and then to compute the intransitive purge of the resulting list with domain set
@{term U}. If recursion with respect to the input list is added, replacing @{term xs'} with the list
produced by the same algorithm using @{term xs'} as input list and @{term "sinks_aux I D U [x]"} as
domain set, the final result matches that obtained by applying filter @{term P} to the intransitive
purge of @{term xs} with domain set @{term U}. In fact, in each recursive step, the processed item
of the input list is retained in the output list just in case it passes filter @{term P} and may be
affected neither by the domains in @{term U}, nor by the domains of the previous items affected by
some domain in @{term U}.

Here below is the formal definition of such purge function, named ‹ipurge_tr_aux_foldr› as its
action resembles that of function @{term foldr}.

\null
›

primrec ipurge_tr_aux_foldr ::
 "('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('a ⇒ bool) ⇒ 'd set ⇒ 'a list ⇒ 'a list"
where
"ipurge_tr_aux_foldr I D P U [] = []" |
"ipurge_tr_aux_foldr I D P U (x # xs) = ipurge_tr_aux I D U
   ((if P x then [x] else []) @
     ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs)"

text ‹
\null

Likewise, given @{term I}, @{term D}, @{term U}, @{term "xs = x # xs'"}, and an event set @{term X},
suppose to take @{term x} just in case it satisfies predicate @{term P}, to append
@{term "ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs'"} to the resulting list (matching either
@{term "[x]"} or @{term "[]"}), and then to compute the intransitive purge of @{term X} using the
resulting list as input list and @{term U} as domain set. If recursion with respect to the input
list is added, replacing @{term X} with the set produced by the same algorithm using @{term xs'} as
input list, @{term X} as input set, and @{term "sinks_aux I D U [x]"} as domain set, the final
result matches the intransitive purge of @{term X} with input list @{term xs} and domain set
@{term U}. In fact, each recursive step is such as to remove from @{term X} any event that may be
affected either by the domains in @{term U}, or by the domains of the items of @{term xs} preceding
the processed one which are affected by some domain in @{term U}.

From the above considerations on function @{term ipurge_tr_aux_foldr}, it follows that the presence
of list @{term "ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs'"} has no impact on the final
result, because none of its items may be affected by the domains in @{term U}.

Here below is the formal definition of such purge function, named ‹ipurge_ref_aux_foldr›,
which at first glance just seems a uselessly complicate and inefficient way to compute the
intransitive purge of an event set.

\null
›

primrec ipurge_ref_aux_foldr ::
 "('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('a ⇒ bool) ⇒ 'd set ⇒ 'a list ⇒ 'a set ⇒ 'a set"
where
"ipurge_ref_aux_foldr I D P U [] X = ipurge_ref_aux I D U [] X" |
"ipurge_ref_aux_foldr I D P U (x # xs) X = ipurge_ref_aux I D U
   ((if P x then [x] else []) @
     ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs)
   (ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X)"

text ‹
\null

The reason for the introduction of such intransitive purge functions is that the recursive equations
contained in their definitions, along with lemma @{thm [source] ipurge_tr_ref_aux_failures_general},
enable to prove by induction on list @{term ys}, assuming that process @{term P} be secure in
addition to further, minor premises, the following implication:

\null

@{term "(map (inv p) [x←xs @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
  (map (inv p) [x←xs. x ∈ range p] @
   map (inv p) (ipurge_tr_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
     (λx. x ∈ range p) U ys),
   inv p ` ipurge_ref_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
     (λx. x ∈ range p) U ys Y) ∈ failures P"}

\null

In fact, for @{term "ys = y # ys'"}, the induction hypothesis entails that the consequent holds if
@{term xs}, @{term ys}, and @{term U} are replaced with @{term "xs @ [y]"}, @{term ys'}, and
@{term "sinks_aux (con_comp_pol I) (con_comp_map D E p q) U [y]"}, respectively. The proof can then
be accomplished by applying lemma @{thm [source] ipurge_tr_ref_aux_failures_general} to the
resulting future of trace @{term "map (inv p) [x←xs. x ∈ range p]"}, moving functions
@{term ipurge_tr_aux} and @{term "ipurge_ref_aux"} into the arguments of @{term "map (inv p)"} and
@{term "(`) (inv p)"}, and using the recursive equations contained in the definitions of functions
@{term ipurge_tr_aux_foldr} and @{term ipurge_ref_aux_foldr}.

This property, along with the match of the outputs of functions @{term ipurge_tr_aux_foldr} and
@{term ipurge_ref_aux_foldr} with the filtered intransitive purge of the input event list and the
intransitive purge of the input event set, respectively, permits to solve the main proof obligations
arising from the demonstration of the target security conservation theorem.

Here below is the proof of the equivalence between function @{term ipurge_tr_aux_foldr} and the
filtered intransitive purge of an event list.

\null
›

lemma ipurge_tr_aux_foldr_subset:
 "U ⊆ V ⟹
  ipurge_tr_aux I D U (ipurge_tr_aux_foldr I D P V xs) =
    ipurge_tr_aux_foldr I D P V xs"
proof (induction xs, simp_all add: ipurge_tr_aux_union [symmetric])
qed (drule Un_absorb2, simp)

lemma ipurge_tr_aux_foldr_eq:
 "[x←ipurge_tr_aux I D U xs. P x] = ipurge_tr_aux_foldr I D P U xs"
proof (induction xs arbitrary: U, simp)
  fix x xs U
  assume
    A: "⋀U. [x←ipurge_tr_aux I D U xs. P x] = ipurge_tr_aux_foldr I D P U xs"
  show "[x←ipurge_tr_aux I D U (x # xs). P x] =
    ipurge_tr_aux_foldr I D P U (x # xs)"
  proof (cases "∃u ∈ U. (u, D x) ∈ I",
   simp_all only: ipurge_tr_aux_foldr.simps ipurge_tr_aux_cons
   sinks_aux_single_event if_True if_False)
    case True
    have B: "[x←ipurge_tr_aux I D (insert (D x) U) xs. P x] =
      ipurge_tr_aux_foldr I D P (insert (D x) U) xs"
     using A .
    show "[x←ipurge_tr_aux I D (insert (D x) U) xs. P x] = ipurge_tr_aux I D U
      ((if P x then [x] else []) @ ipurge_tr_aux_foldr I D P (insert (D x) U) xs)"
    proof (cases "P x", simp_all add: ipurge_tr_aux_cons True
     del: con_comp_map.simps)
      have "insert (D x) U ⊆ insert (D x) U" ..
      hence "ipurge_tr_aux I D (insert (D x) U)
        (ipurge_tr_aux_foldr I D P (insert (D x) U) xs) =
          ipurge_tr_aux_foldr I D P (insert (D x) U) xs"
       by (rule ipurge_tr_aux_foldr_subset)
      thus "[x←ipurge_tr_aux I D (insert (D x) U) xs. P x] =
        ipurge_tr_aux I D (insert (D x) U)
          (ipurge_tr_aux_foldr I D P (insert (D x) U) xs)"
       using B by simp
    next
      have "U ⊆ insert (D x) U"
       by (rule subset_insertI)
      hence "ipurge_tr_aux I D U
        (ipurge_tr_aux_foldr I D P (insert (D x) U) xs) =
          ipurge_tr_aux_foldr I D P (insert (D x) U) xs"
       by (rule ipurge_tr_aux_foldr_subset)
      thus "[x←ipurge_tr_aux I D (insert (D x) U) xs. P x] =
        ipurge_tr_aux I D U
          (ipurge_tr_aux_foldr I D P (insert (D x) U) xs)"
       using B by simp
    qed
  next
    case False
    have B: "[x←ipurge_tr_aux I D U xs. P x] = ipurge_tr_aux_foldr I D P U xs"
     using A .
    show "[x←x # ipurge_tr_aux I D U xs. P x] = ipurge_tr_aux I D U
      ((if P x then [x] else []) @ ipurge_tr_aux_foldr I D P U xs)"
    proof (cases "P x", simp_all add: ipurge_tr_aux_cons False
     del: con_comp_map.simps)
      have "U ⊆ U" ..
      hence "ipurge_tr_aux I D U (ipurge_tr_aux_foldr I D P U xs) =
        ipurge_tr_aux_foldr I D P U xs"
       by (rule ipurge_tr_aux_foldr_subset)
      thus "[x←ipurge_tr_aux I D U xs. P x] =
        ipurge_tr_aux I D U (ipurge_tr_aux_foldr I D P U xs)"
       using B by simp
    next
      have "U ⊆ U" ..
      hence "ipurge_tr_aux I D U (ipurge_tr_aux_foldr I D P U xs) =
        ipurge_tr_aux_foldr I D P U xs"
       by (rule ipurge_tr_aux_foldr_subset)
      thus "[x←ipurge_tr_aux I D U xs. P x] =
        ipurge_tr_aux I D U (ipurge_tr_aux_foldr I D P U xs)"
       using B by simp
    qed
  qed
qed

text ‹
\null

Here below is the proof of the equivalence between function @{term ipurge_ref_aux_foldr} and the
intransitive purge of an event set.

\null
›

lemma ipurge_tr_aux_foldr_sinks_aux [rule_format]:
 "U ⊆ V ⟶ sinks_aux I D U (ipurge_tr_aux_foldr I D P V xs) = U"
proof (induction xs arbitrary: V, simp, rule impI)
  fix x xs V
  assume
    A: "⋀V. U ⊆ V ⟶ sinks_aux I D U (ipurge_tr_aux_foldr I D P V xs) = U" and
    B: "U ⊆ V"
  show "sinks_aux I D U (ipurge_tr_aux_foldr I D P V (x # xs)) = U"
  proof (cases "P x", case_tac [!] "∃v ∈ V. (v, D x) ∈ I",
   simp_all (no_asm_simp) add: sinks_aux_cons ipurge_tr_aux_cons)
    have "U ⊆ insert (D x) V ⟶
      sinks_aux I D U (ipurge_tr_aux_foldr I D P (insert (D x) V) xs) = U"
      (is "_ ⟶ sinks_aux I D U ?ys = U")
     using A .
    moreover have "U ⊆ insert (D x) V"
     using B by (rule subset_insertI2)
    ultimately have "sinks_aux I D U ?ys = U" ..
    moreover have "insert (D x) V ⊆ insert (D x) V" ..
    hence "ipurge_tr_aux I D (insert (D x) V)
      (ipurge_tr_aux_foldr I D P (insert (D x) V) xs) = ?ys"
      (is "?zs = _")
     by (rule ipurge_tr_aux_foldr_subset)
    ultimately show "sinks_aux I D U ?zs = U"
     by simp
  next
    assume C: "¬ (∃v ∈ V. (v, D x) ∈ I)"
    have "¬ (∃u ∈ U. (u, D x) ∈ I)"
    proof
      assume "∃u ∈ U. (u, D x) ∈ I"
      then obtain u where D: "u ∈ U" and E: "(u, D x) ∈ I" ..
      have "u ∈ V"
       using B and D ..
      with E have "∃v ∈ V. (v, D x) ∈ I" ..
      thus False
       using C by contradiction
    qed
    thus
     "((∃v ∈ U. (v, D x) ∈ I) ⟶ sinks_aux I D (insert (D x) U)
        (ipurge_tr_aux I D V (ipurge_tr_aux_foldr I D P V xs)) = U) ∧
      ((∀v ∈ U. (v, D x) ∉ I) ⟶ sinks_aux I D U
        (ipurge_tr_aux I D V (ipurge_tr_aux_foldr I D P V xs)) = U)"
    proof simp
      have "U ⊆ V ⟶ sinks_aux I D U (ipurge_tr_aux_foldr I D P V xs) = U"
        (is "_ ⟶ sinks_aux I D U ?ys = U")
       using A .
      hence "sinks_aux I D U ?ys = U" using B ..
      moreover have "V ⊆ V" ..
      hence "ipurge_tr_aux I D V (ipurge_tr_aux_foldr I D P V xs) = ?ys"
        (is "?zs = _")
       by (rule ipurge_tr_aux_foldr_subset)
      ultimately show "sinks_aux I D U ?zs = U"
       by simp
    qed
  next
    have "U ⊆ insert (D x) V ⟶
      sinks_aux I D U (ipurge_tr_aux_foldr I D P (insert (D x) V) xs) = U"
      (is "_ ⟶ sinks_aux I D U ?ys = U")
     using A .
    moreover have "U ⊆ insert (D x) V"
     using B by (rule subset_insertI2)
    ultimately have "sinks_aux I D U ?ys = U" ..
    moreover have "V ⊆ insert (D x) V"
     by (rule subset_insertI)
    hence "ipurge_tr_aux I D V
      (ipurge_tr_aux_foldr I D P (insert (D x) V) xs) = ?ys"
      (is "?zs = _")
     by (rule ipurge_tr_aux_foldr_subset)
    ultimately show "sinks_aux I D U ?zs = U"
     by simp
  next
    have "U ⊆ V ⟶ sinks_aux I D U (ipurge_tr_aux_foldr I D P V xs) = U"
      (is "_ ⟶ sinks_aux I D U ?ys = U")
     using A .
    hence "sinks_aux I D U ?ys = U" using B ..
    moreover have "V ⊆ V" ..
    hence "ipurge_tr_aux I D V (ipurge_tr_aux_foldr I D P V xs) = ?ys"
      (is "?zs = _")
     by (rule ipurge_tr_aux_foldr_subset)
    ultimately show "sinks_aux I D U ?zs = U"
     by simp
  qed
qed

lemma ipurge_tr_aux_foldr_ref_aux:
  assumes A: "U ⊆ V"
  shows "ipurge_ref_aux I D U (ipurge_tr_aux_foldr I D P V xs) X =
    ipurge_ref_aux I D U [] X"
by (simp add: ipurge_ref_aux_def ipurge_tr_aux_foldr_sinks_aux [OF A])

lemma ipurge_ref_aux_foldr_subset [rule_format]:
 "sinks_aux I D U ys ⊆ V ⟶
  ipurge_ref_aux I D U ys (ipurge_ref_aux_foldr I D P V xs X) =
    ipurge_ref_aux_foldr I D P V xs X"
proof (induction xs arbitrary: ys U V, rule_tac [!] impI,
 simp add: ipurge_ref_aux_def, blast)
  fix x xs ys U V
  assume
    A: "⋀ys U V.
      sinks_aux I D U ys ⊆ V ⟶
      ipurge_ref_aux I D U ys (ipurge_ref_aux_foldr I D P V xs X) =
        ipurge_ref_aux_foldr I D P V xs X" and
    B: "sinks_aux I D U ys ⊆ V"
  show "ipurge_ref_aux I D U ys (ipurge_ref_aux_foldr I D P V (x # xs) X) =
    ipurge_ref_aux_foldr I D P V (x # xs) X"
  proof (cases "P x", simp_all add: ipurge_ref_aux_cons)
    have C: "sinks_aux I D V [x] ⊆ sinks_aux I D V [x]" ..
    show
     "ipurge_ref_aux I D U ys (ipurge_ref_aux I D (sinks_aux I D V [x])
        (ipurge_tr_aux_foldr I D P (sinks_aux I D V [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X)) =
      ipurge_ref_aux I D (sinks_aux I D V [x])
        (ipurge_tr_aux_foldr I D P (sinks_aux I D V [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X)"
    proof (simp add: ipurge_tr_aux_foldr_ref_aux [OF C])
      have "sinks_aux I D (sinks_aux I D V [x]) [] ⊆ sinks_aux I D V [x] ⟶
        ipurge_ref_aux I D (sinks_aux I D V [x]) []
          (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X) =
        ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X"
        (is "?A ⟶ ?us = ?vs")
       using A .
      moreover have ?A
       by simp
      ultimately have "?us = ?vs" ..
      thus "ipurge_ref_aux I D U ys ?us = ?us"
      proof simp
        have "sinks_aux I D U ys ⊆ sinks_aux I D V [x] ⟶
          ipurge_ref_aux I D U ys
            (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X) =
          ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X"
          (is "_ ⟶ ?T")
         using A .
        moreover have "V ⊆ sinks_aux I D V [x]"
         by (rule sinks_aux_subset)
        hence "sinks_aux I D U ys ⊆ sinks_aux I D V [x]"
         using B by simp
        ultimately show ?T ..
      qed
    qed
  next
    have C: "V ⊆ sinks_aux I D V [x]"
     by (rule sinks_aux_subset)
    show
     "ipurge_ref_aux I D U ys (ipurge_ref_aux I D V
        (ipurge_tr_aux_foldr I D P (sinks_aux I D V [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X)) =
      ipurge_ref_aux I D V
        (ipurge_tr_aux_foldr I D P (sinks_aux I D V [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X)"
    proof (simp add: ipurge_tr_aux_foldr_ref_aux [OF C])
      have "sinks_aux I D V [] ⊆ sinks_aux I D V [x] ⟶
        ipurge_ref_aux I D V []
          (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X) =
        ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X"
        (is "?A ⟶ ?us = ?vs")
       using A .
      moreover have ?A
       using C by simp
      ultimately have "?us = ?vs" ..
      thus "ipurge_ref_aux I D U ys ?us = ?us"
      proof simp
        have "sinks_aux I D U ys ⊆ sinks_aux I D V [x] ⟶
          ipurge_ref_aux I D U ys
            (ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X) =
          ipurge_ref_aux_foldr I D P (sinks_aux I D V [x]) xs X"
          (is "_ ⟶ ?T")
         using A .
        moreover have "sinks_aux I D U ys ⊆ sinks_aux I D V [x]"
         using B and C by simp
        ultimately show ?T ..
      qed
    qed
  qed
qed

lemma ipurge_ref_aux_foldr_eq:
 "ipurge_ref_aux I D U xs X = ipurge_ref_aux_foldr I D P U xs X"
proof (induction xs arbitrary: U, simp)
  fix x xs U
  assume A: "⋀U. ipurge_ref_aux I D U xs X = ipurge_ref_aux_foldr I D P U xs X"
  show "ipurge_ref_aux I D U (x # xs) X =
    ipurge_ref_aux_foldr I D P U (x # xs) X"
  proof (cases "P x", simp_all add: ipurge_ref_aux_cons)
    have "sinks_aux I D U [x] ⊆ sinks_aux I D U [x]" ..
    hence
     "ipurge_ref_aux I D (sinks_aux I D U [x])
        (ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X) =
      ipurge_ref_aux I D (sinks_aux I D U [x]) []
        (ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X)"
      (is "ipurge_ref_aux _ _ _ ?xs' ?X' = _")
     by (rule ipurge_tr_aux_foldr_ref_aux)
    also have "sinks_aux I D (sinks_aux I D U [x]) [] ⊆ sinks_aux I D U [x]"
     by simp
    hence "ipurge_ref_aux I D (sinks_aux I D U [x]) [] ?X' = ?X'"
     by (rule ipurge_ref_aux_foldr_subset)
    finally have "ipurge_ref_aux I D (sinks_aux I D U [x]) ?xs' ?X' = ?X'" .
    thus "ipurge_ref_aux I D (sinks_aux I D U [x]) xs X =
      ipurge_ref_aux I D (sinks_aux I D U [x]) ?xs' ?X'"
    proof simp
      show "ipurge_ref_aux I D (sinks_aux I D U [x]) xs X =
        ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X"
       using A .
    qed
  next
    have "U ⊆ sinks_aux I D U [x]"
     by (rule sinks_aux_subset)
    hence
     "ipurge_ref_aux I D U
        (ipurge_tr_aux_foldr I D P (sinks_aux I D U [x]) xs)
        (ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X) =
      ipurge_ref_aux I D U []
        (ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X)"
      (is "ipurge_ref_aux _ _ _ ?xs' ?X' = _")
     by (rule ipurge_tr_aux_foldr_ref_aux)
    also have "sinks_aux I D U [] ⊆ sinks_aux I D U [x]"
     by (simp, rule sinks_aux_subset)
    hence "ipurge_ref_aux I D U [] ?X' = ?X'"
     by (rule ipurge_ref_aux_foldr_subset)
    finally have "ipurge_ref_aux I D U ?xs' ?X' = ?X'" .
    thus "ipurge_ref_aux I D (sinks_aux I D U [x]) xs X =
      ipurge_ref_aux I D U ?xs' ?X'"
    proof simp
      show "ipurge_ref_aux I D (sinks_aux I D U [x]) xs X =
        ipurge_ref_aux_foldr I D P (sinks_aux I D U [x]) xs X"
       using A .
    qed
  qed
qed

text ‹
\null

Finally, here below is the proof of the implication involving functions @{term ipurge_tr_aux_foldr}
and @{term ipurge_ref_aux_foldr} discussed above.

\null
›

lemma con_comp_sinks_aux_range:
  assumes
    A: "U ⊆ range Some" and
    B: "set xs ⊆ range p ∪ range q"
  shows "sinks_aux (con_comp_pol I) (con_comp_map D E p q) U xs ⊆ range Some"
    (is "sinks_aux _ ?D' _ _ ⊆ _")
proof (rule subsetI, drule sinks_aux_elem, erule disjE, erule_tac [2] bexE)
  fix u
  assume "u ∈ U"
  with A show "u ∈ range Some" ..
next
  fix u x
  assume "x ∈ set xs"
  with B have "x ∈ range p ∪ range q" ..
  hence "?D' x ∈ range Some"
   by (cases "x ∈ range p", simp_all)
  moreover assume "u = ?D' x"
  ultimately show "u ∈ range Some"
   by simp
qed

lemma con_comp_sinks_aux [rule_format]:
  assumes A: "U ⊆ range Some"
  shows "set xs ⊆ range p ⟶
    sinks_aux I D (the ` U) (map (inv p) xs) =
    the ` sinks_aux (con_comp_pol I) (con_comp_map D E p q) U xs"
    (is "_ ⟶ _ = the ` sinks_aux ?I' ?D' _ _")
proof (induction xs rule: rev_induct, simp, rule impI)
  fix x xs
  assume "set xs ⊆ range p ⟶
    sinks_aux I D (the ` U) (map (inv p) xs) =
    the ` sinks_aux ?I' ?D' U xs"
  moreover assume B: "set (xs @ [x]) ⊆ range p"
  ultimately have C: "sinks_aux I D (the ` U) (map (inv p) xs) =
    the ` sinks_aux ?I' ?D' U xs"
   by simp
  show "sinks_aux I D (the ` U) (map (inv p) (xs @ [x])) =
    the ` sinks_aux ?I' ?D' U (xs @ [x])"
  proof (cases "∃u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∈ ?I'",
   simp_all (no_asm_simp) del: map_append)
    case True
    then obtain u where
      D: "u ∈ sinks_aux ?I' ?D' U xs" and E: "(u, ?D' x) ∈ ?I'" ..
    have "(the u, D (inv p x)) ∈ I"
     using B and E by (simp add: con_comp_pol_def, erule_tac exE, simp)
    moreover have "the u ∈ the ` sinks_aux ?I' ?D' U xs"
     using D by simp
    hence "the u ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
     using C by simp
    ultimately have "∃d ∈ sinks_aux I D (the ` U) (map (inv p) xs).
      (d, D (inv p x)) ∈ I" ..
    hence "sinks_aux I D (the ` U) (map (inv p) (xs @ [x])) =
      insert (D (inv p x)) (sinks_aux I D (the ` U) (map (inv p) xs))"
     by simp
    thus "sinks_aux I D (the ` U) (map (inv p) (xs @ [x])) =
      insert (the (?D' x)) (the ` sinks_aux ?I' ?D' U xs)"
     using B and C by simp
  next
    case False
    have "¬ (∃d ∈ sinks_aux I D (the ` U) (map (inv p) xs).
      (d, D (inv p x)) ∈ I)"
    proof (rule notI, erule bexE)
      fix d
      assume "d ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
      hence "d ∈ the ` sinks_aux ?I' ?D' U xs"
       using C by simp
      hence "∃u ∈ sinks_aux ?I' ?D' U xs. d = the u"
       by (simp add: image_iff)
      then obtain u where
        D: "u ∈ sinks_aux ?I' ?D' U xs" and E: "d = the u" ..
      have "set xs ⊆ range p ∪ range q"
       using B by (simp, blast)
      with A have "sinks_aux ?I' ?D' U xs ⊆ range Some"
       by (rule con_comp_sinks_aux_range)
      hence "u ∈ range Some"
       using D ..
      hence "u = Some d"
       using E by (simp add: image_iff)
      moreover assume "(d, D (inv p x)) ∈ I"
      hence "(Some d, Some (D (inv p x))) ∈ ?I'"
       by (simp add: con_comp_pol_def)
      ultimately have "(u, ?D' x) ∈ ?I'"
       using B by simp
      hence "∃u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∈ ?I'"
       using D ..
      thus False
       using False by contradiction
    qed
    thus "sinks_aux I D (the ` U) (map (inv p) (xs @ [x])) =
      the ` sinks_aux ?I' ?D' U xs"
     using C by simp
  qed
qed

lemma con_comp_ipurge_tr_aux [rule_format]:
  assumes A: "U ⊆ range Some"
  shows "set xs ⊆ range p ⟶
    ipurge_tr_aux I D (the ` U) (map (inv p) xs) =
    map (inv p) (ipurge_tr_aux (con_comp_pol I) (con_comp_map D E p q) U xs)"
    (is "_ ⟶ _ = map (inv p) (ipurge_tr_aux ?I' ?D' _ _)")
proof (induction xs rule: rev_induct, simp, rule impI)
  fix x xs
  assume "set xs ⊆ range p ⟶
    ipurge_tr_aux I D (the ` U) (map (inv p) xs) =
    map (inv p) (ipurge_tr_aux ?I' ?D' U xs)"
  moreover assume B: "set (xs @ [x]) ⊆ range p"
  ultimately have C: "ipurge_tr_aux I D (the ` U) (map (inv p) xs) =
    map (inv p) (ipurge_tr_aux ?I' ?D' U xs)"
   by simp
  show "ipurge_tr_aux I D (the ` U) (map (inv p) (xs @ [x])) =
    map (inv p) (ipurge_tr_aux ?I' ?D' U (xs @ [x]))"
  proof (cases "∃u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∈ ?I'")
    case True
    then obtain u where
      D: "u ∈ sinks_aux ?I' ?D' U xs" and E: "(u, ?D' x) ∈ ?I'" ..
    have "(the u, D (inv p x)) ∈ I"
     using B and E by (simp add: con_comp_pol_def, erule_tac exE, simp)
    moreover have F: "the u ∈ the ` sinks_aux ?I' ?D' U xs"
     using D by simp
    have "set xs ⊆ range p"
     using B by simp
    with A have "sinks_aux I D (the ` U) (map (inv p) xs) =
      the ` sinks_aux ?I' ?D' U xs"
     by (rule con_comp_sinks_aux)
    hence "the u ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
     using F by simp
    ultimately have "∃d ∈ sinks_aux I D (the ` U) (map (inv p) xs).
      (d, D (inv p x)) ∈ I" ..
    hence "ipurge_tr_aux I D (the ` U) (map (inv p) (xs @ [x])) =
      ipurge_tr_aux I D (the ` U) (map (inv p) xs)"
     by simp
    moreover have "map (inv p) (ipurge_tr_aux ?I' ?D' U (xs @ [x])) =
      map (inv p) (ipurge_tr_aux ?I' ?D' U xs)"
     using True by simp
    ultimately show ?thesis
     using C by simp
  next
    case False
    have "¬ (∃d ∈ sinks_aux I D (the ` U) (map (inv p) xs).
      (d, D (inv p x)) ∈ I)"
    proof (rule notI, erule bexE)
      fix d
      assume "d ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
      moreover have "set xs ⊆ range p"
       using B by simp
      with A have "sinks_aux I D (the ` U) (map (inv p) xs) =
        the ` sinks_aux ?I' ?D' U xs"
       by (rule con_comp_sinks_aux)
      ultimately have "d ∈ the ` sinks_aux ?I' ?D' U xs"
       by simp
      hence "∃u ∈ sinks_aux ?I' ?D' U xs. d = the u"
       by (simp add: image_iff)
      then obtain u where
        D: "u ∈ sinks_aux ?I' ?D' U xs" and E: "d = the u" ..
      have "set xs ⊆ range p ∪ range q"
       using B by (simp, blast)
      with A have "sinks_aux ?I' ?D' U xs ⊆ range Some"
       by (rule con_comp_sinks_aux_range)
      hence "u ∈ range Some"
       using D ..
      hence "u = Some d"
       using E by (simp add: image_iff)
      moreover assume "(d, D (inv p x)) ∈ I"
      hence "(Some d, Some (D (inv p x))) ∈ ?I'"
       by (simp add: con_comp_pol_def)
      ultimately have "(u, ?D' x) ∈ ?I'"
       using B by simp
      hence "∃u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∈ ?I'"
       using D ..
      thus False
       using False by contradiction
    qed
    hence "ipurge_tr_aux I D (the ` U) (map (inv p) (xs @ [x])) =
      ipurge_tr_aux I D (the ` U) (map (inv p) xs) @ [inv p x]"
     by simp
    moreover have "map (inv p) (ipurge_tr_aux ?I' ?D' U (xs @ [x])) =
      map (inv p) (ipurge_tr_aux ?I' ?D' U xs) @ [inv p x]"
     using False by simp
    ultimately show ?thesis
     using C by simp
  qed
qed

lemma con_comp_ipurge_ref_aux:
  assumes
    A: "U ⊆ range Some" and
    B: "set xs ⊆ range p" and
    C: "X ⊆ range p"
  shows "ipurge_ref_aux I D (the ` U) (map (inv p) xs) (inv p ` X) =
    inv p ` ipurge_ref_aux (con_comp_pol I) (con_comp_map D E p q) U xs X"
  (is "_ = inv p ` ipurge_ref_aux ?I' ?D' _ _ _")
proof (simp add: ipurge_ref_aux_def set_eq_iff image_iff, rule allI, rule iffI,
 erule conjE, erule bexE, erule_tac [2] exE, (erule_tac [2] conjE)+)
  fix a x
  assume
    D: "x ∈ X" and
    E: "a = inv p x" and
    F: "∀d ∈ sinks_aux I D (the ` U) (map (inv p) xs). (d, D a) ∉ I"
  show "∃x. x ∈ X ∧ (∀u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∉ ?I') ∧
    a = inv p x"
  proof (rule_tac x = x in exI, simp add: D E, rule ballI)
    fix u
    assume G: "u ∈ sinks_aux ?I' ?D' U xs"
    moreover have "sinks_aux I D (the ` U) (map (inv p) xs) =
      the ` sinks_aux ?I' ?D' U xs"
     using A and B by (rule con_comp_sinks_aux)
    ultimately have "the u ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
     by simp
    with F have "(the u, D a) ∉ I" ..
    moreover have "set xs ⊆ range p ∪ range q"
     using B by blast
    with A have "sinks_aux ?I' ?D' U xs ⊆ range Some"
     by (rule con_comp_sinks_aux_range)
    hence "u ∈ range Some"
     using G ..
    hence "∃d. u = Some d"
     by (simp add: image_iff)
    then obtain d where H: "u = Some d" ..
    ultimately have "(d, D (inv p x)) ∉ I"
     using E by simp
    hence "(u, Some (D (inv p x))) ∉ ?I'"
     using H by (simp add: con_comp_pol_def)
    moreover have "x ∈ range p"
     using C and D ..
    ultimately show "(u, ?D' x) ∉ ?I'"
     by simp
  qed
next
  fix a x
  assume
    D: "x ∈ X" and
    E: "a = inv p x" and
    F: "∀u ∈ sinks_aux ?I' ?D' U xs. (u, ?D' x) ∉ ?I'"
  show "(∃x ∈ X. a = inv p x) ∧
    (∀u ∈ sinks_aux I D (the ` U) (map (inv p) xs). (u, D a) ∉ I)"
  proof (rule conjI, rule_tac [2] ballI)
    show "∃x ∈ X. a = inv p x"
     using E and D ..
  next
    fix d
    assume "d ∈ sinks_aux I D (the ` U) (map (inv p) xs)"
    moreover have "sinks_aux I D (the ` U) (map (inv p) xs) =
      the ` sinks_aux ?I' ?D' U xs"
     using A and B by (rule con_comp_sinks_aux)
    ultimately have "d ∈ the ` sinks_aux ?I' ?D' U xs"
     by simp
    hence "∃u ∈ sinks_aux ?I' ?D' U xs. d = the u"
     by (simp add: image_iff)
    then obtain u where G: "u ∈ sinks_aux ?I' ?D' U xs" and H: "d = the u" ..
    have "(u, ?D' x) ∉ ?I'"
     using F and G ..
    moreover have "set xs ⊆ range p ∪ range q"
     using B by blast
    with A have "sinks_aux ?I' ?D' U xs ⊆ range Some"
     by (rule con_comp_sinks_aux_range)
    hence "u ∈ range Some"
     using G ..
    hence "u = Some d"
     using H by (simp add: image_iff)
    moreover have "x ∈ range p"
     using C and D ..
    ultimately have "(d, D (inv p x)) ∉ I"
     by (simp add: con_comp_pol_def)
    thus "(d, D a) ∉ I"
     using E by simp
  qed
qed

lemma con_comp_sinks_filter:
 "sinks (con_comp_pol I) (con_comp_map D E p q) u
    [x←xs. x ∈ range p ∪ range q] =
  sinks (con_comp_pol I) (con_comp_map D E p q) u xs ∩ range Some"
  (is "sinks ?I' ?D' _ _ = _")
proof (induction xs rule: rev_induct, simp)
  fix x xs
  assume A: "sinks ?I' ?D' u [x←xs. x ∈ range p ∪ range q] =
    sinks ?I' ?D' u xs ∩ range Some"
    (is "sinks _ _ _ ?xs' = _")
  show "sinks ?I' ?D' u [x←xs @ [x]. x ∈ range p ∪ range q] =
    sinks ?I' ?D' u (xs @ [x]) ∩ range Some"
  proof (cases "x ∈ range p ∪ range q", simp_all del: Un_iff sinks.simps,
   cases "(u, ?D' x) ∈ ?I' ∨ (∃v ∈ sinks ?I' ?D' u ?xs'. (v, ?D' x) ∈ ?I')")
    assume
      B: "x ∈ range p ∪ range q" and
      C: "(u, ?D' x) ∈ ?I' ∨ (∃v ∈ sinks ?I' ?D' u ?xs'. (v, ?D' x) ∈ ?I')"
    have "sinks ?I' ?D' u (?xs' @ [x]) =
      insert (?D' x) (sinks ?I' ?D' u ?xs')"
     using C by simp
    also have "… =
      insert (?D' x) (sinks ?I' ?D' u xs ∩ range Some)"
     using A by simp
    also have "… =
      insert (?D' x) (sinks ?I' ?D' u xs) ∩ insert (?D' x) (range Some)"
     by simp
    finally have "sinks ?I' ?D' u (?xs' @ [x]) =
      insert (?D' x) (sinks ?I' ?D' u xs) ∩ insert (?D' x) (range Some)" .
    moreover have "insert (?D' x) (range Some) = range Some"
     using B by (rule_tac insert_absorb, cases "x ∈ range p", simp_all)
    ultimately have "sinks ?I' ?D' u (?xs' @ [x]) =
      insert (?D' x) (sinks ?I' ?D' u xs) ∩ range Some"
     by simp
    moreover have "(u, ?D' x) ∈ ?I' ∨
      (∃v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∈ ?I')"
     using A and C by (simp, blast)
    ultimately show "sinks ?I' ?D' u (?xs' @ [x]) =
      sinks ?I' ?D' u (xs @ [x]) ∩ range Some"
     by simp
  next
    assume
      B: "x ∈ range p ∪ range q" and
      C: "¬ ((u, ?D' x) ∈ ?I' ∨ (∃v ∈ sinks ?I' ?D' u ?xs'. (v, ?D' x) ∈ ?I'))"
    have "sinks ?I' ?D' u (?xs' @ [x]) = sinks ?I' ?D' u ?xs'"
     using C by simp
    hence "sinks ?I' ?D' u (?xs' @ [x]) = sinks ?I' ?D' u xs ∩ range Some"
     using A by simp
    moreover from C have
     "¬ ((u, ?D' x) ∈ ?I' ∨ (∃v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∈ ?I'))"
    proof (rule_tac notI, simp del: bex_simps)
      assume "∃v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∈ ?I'"
      then obtain v where E: "v ∈ sinks ?I' ?D' u xs" and F: "(v, ?D' x) ∈ ?I'" ..
      have "∃d. ?D' x = Some d"
       using B by (cases "x ∈ range p", simp_all)
      then obtain d where "?D' x = Some d" ..
      hence "(v, Some d) ∈ ?I'"
       using F by simp
      hence "v ∈ range Some"
       by (cases v, simp_all add: con_comp_pol_def)
      with E have "v ∈ sinks ?I' ?D' u xs ∩ range Some" ..
      hence "v ∈ sinks ?I' ?D' u ?xs'"
       using A by simp
      with F have "∃v ∈ sinks ?I' ?D' u ?xs'. (v, ?D' x) ∈ ?I'" ..
      thus False
       using C by simp
    qed
    ultimately show "sinks ?I' ?D' u (?xs' @ [x]) =
      sinks ?I' ?D' u (xs @ [x]) ∩ range Some"
     by simp
  next
    assume B: "x ∉ range p ∪ range q"
    hence "(u, ?D' x) ∈ ?I'"
     by (simp add: con_comp_pol_def)
    hence "sinks ?I' ?D' u (xs @ [x]) = insert (?D' x) (sinks ?I' ?D' u xs)"
     by simp
    moreover have "insert (?D' x) (sinks ?I' ?D' u xs) ∩ range Some =
      sinks ?I' ?D' u xs ∩ range Some"
     using B by simp
    ultimately have "sinks ?I' ?D' u (xs @ [x]) ∩ range Some =
      sinks ?I' ?D' u xs ∩ range Some"
     by simp
    thus "sinks ?I' ?D' u ?xs' = sinks ?I' ?D' u (xs @ [x]) ∩ range Some"
     using A by simp
  qed
qed

lemma con_comp_ipurge_tr_filter:
 "ipurge_tr (con_comp_pol I) (con_comp_map D E p q) u
    [x←xs. x ∈ range p ∪ range q] =
  ipurge_tr (con_comp_pol I) (con_comp_map D E p q) u xs"
  (is "ipurge_tr ?I' ?D' _ _ = _")
proof (induction xs rule: rev_induct, simp)
  fix x xs
  assume A: "ipurge_tr ?I' ?D' u [x←xs. x ∈ range p ∪ range q] =
    ipurge_tr ?I' ?D' u xs"
    (is "ipurge_tr _ _ _ ?xs' = _")
  show "ipurge_tr ?I' ?D' u [x←xs @ [x]. x ∈ range p ∪ range q] =
    ipurge_tr ?I' ?D' u (xs @ [x])"
  proof (cases "x ∈ range p ∪ range q", simp_all del: Un_iff ipurge_tr.simps,
   cases "?D' x ∈ sinks ?I' ?D' u (?xs' @ [x])")
    assume
      B: "x ∈ range p ∪ range q" and
      C: "?D' x ∈ sinks ?I' ?D' u (?xs' @ [x])"
    have "ipurge_tr ?I' ?D' u (?xs' @ [x]) = ipurge_tr ?I' ?D' u ?xs'"
     using C by simp
    hence "ipurge_tr ?I' ?D' u (?xs' @ [x]) = ipurge_tr ?I' ?D' u xs"
     using A by simp
    moreover have "?D' x ∈ sinks ?I' ?D' u [x←xs @ [x]. x ∈ range p ∪ range q]"
     using B and C by simp
    hence "?D' x ∈ sinks ?I' ?D' u (xs @ [x])"
     by (simp only: con_comp_sinks_filter, blast)
    ultimately show "ipurge_tr ?I' ?D' u (?xs' @ [x]) =
      ipurge_tr ?I' ?D' u (xs @ [x])"
     by simp
  next
    assume
      B: "x ∈ range p ∪ range q" and
      C: "¬ (?D' x ∈ sinks ?I' ?D' u (?xs' @ [x]))"
    have "ipurge_tr ?I' ?D' u (?xs' @ [x]) = ipurge_tr ?I' ?D' u ?xs' @ [x]"
     using C by simp
    hence "ipurge_tr ?I' ?D' u (?xs' @ [x]) = ipurge_tr ?I' ?D' u xs @ [x]"
     using A by simp
    moreover have "?D' x ∉ sinks ?I' ?D' u [x←xs @ [x]. x ∈ range p ∪ range q]"
     using B and C by simp
    hence "?D' x ∉ sinks ?I' ?D' u (xs @ [x]) ∩ range Some"
     by (simp only: con_comp_sinks_filter, simp)
    hence "?D' x ∉ sinks ?I' ?D' u (xs @ [x])"
     using B by (cases "x ∈ range p", simp_all)
    ultimately show "ipurge_tr ?I' ?D' u (?xs' @ [x]) =
      ipurge_tr ?I' ?D' u (xs @ [x])"
     by simp
  next
    assume "x ∉ range p ∪ range q"
    hence "(u, ?D' x) ∈ ?I'"
     by (simp add: con_comp_pol_def)
    hence "?D' x ∈ sinks ?I' ?D' u (xs @ [x])"
     by simp
    thus "ipurge_tr ?I' ?D' u ?xs' = ipurge_tr ?I' ?D' u (xs @ [x])"
     using A by simp
  qed
qed

lemma con_comp_ipurge_ref_filter:
 "ipurge_ref (con_comp_pol I) (con_comp_map D E p q) u
    [x←xs. x ∈ range p ∪ range q] X =
  ipurge_ref (con_comp_pol I) (con_comp_map D E p q) u xs X"
  (is "ipurge_ref ?I' ?D' _ _ _ = _")
proof (simp add: ipurge_ref_def con_comp_sinks_filter set_eq_iff del: Un_iff,
 rule allI, rule iffI, simp_all, (erule conjE)+, rule ballI)
  fix x v
  assume
    A: "(u, ?D' x) ∉ ?I'" and
    B: "∀v ∈ sinks ?I' ?D' u xs ∩ range Some. (v, ?D' x) ∉ ?I'" and
    C: "v ∈ sinks ?I' ?D' u xs"
  show "(v, ?D' x) ∉ ?I'"
  proof (cases v, simp)
    have "?D' x ∈ range Some"
     using A by (cases "?D' x", simp_all add: con_comp_pol_def)
    thus "(None, ?D' x) ∉ ?I'"
     by (simp add: image_iff con_comp_pol_def)
  next
    fix d
    assume "v = Some d"
    hence "v ∈ range Some"
     by simp
    with C have "v ∈ sinks ?I' ?D' u xs ∩ range Some" ..
    with B show "(v, ?D' x) ∉ ?I'" ..
  qed
qed

lemma con_comp_secure_aux [rule_format]:
  assumes
    A: "secure P I D" and
    B: "Y ⊆ range p"
  shows "set ys ⊆ range p ∪ range q ⟶ U ⊆ range Some ⟶
    (map (inv p) [x←xs @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
    (map (inv p) [x←xs. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) U ys),
     inv p ` ipurge_ref_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) U ys Y) ∈ failures P"
proof (induction ys arbitrary: xs U, (rule_tac [!] impI)+, simp)
  fix xs U
  assume "(map (inv p) [x←xs. x ∈ range p], inv p ` Y) ∈ failures P"
  moreover have
   "ipurge_ref_aux (con_comp_pol I) (con_comp_map D E p q) U [] Y ⊆ Y"
    (is "?Y' ⊆ _")
   by (rule ipurge_ref_aux_subset)
  hence "inv p ` ?Y' ⊆ inv p ` Y"
   by (rule image_mono)
  ultimately show "(map (inv p) [x←xs. x ∈ range p], inv p ` ?Y') ∈ failures P"
   by (rule process_rule_3)
next
  fix y ys xs U
  assume "⋀xs U. set ys ⊆ range p ∪ range q ⟶ U ⊆ range Some ⟶
    (map (inv p) [x←xs @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
    (map (inv p) [x←xs. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) U ys),
     inv p ` ipurge_ref_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) U ys Y) ∈ failures P"
  hence "set ys ⊆ range p ∪ range q ⟶
    sinks_aux (con_comp_pol I) (con_comp_map D E p q) U [y] ⊆ range Some ⟶
    (map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
    (map (inv p) [x←xs @ [y]. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) (sinks_aux (con_comp_pol I) (con_comp_map D E p q)
         U [y]) ys),
     inv p ` ipurge_ref_aux_foldr (con_comp_pol I) (con_comp_map D E p q)
       (λx. x ∈ range p) (sinks_aux (con_comp_pol I) (con_comp_map D E p q)
         U [y]) ys Y) ∈ failures P"
    (is "_ ⟶ _ ⟶ _ ⟶
      (_ @ map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F ?U' _), _) ∈ _") .
  moreover assume C: "set (y # ys) ⊆ range p ∪ range q"
  hence "set ys ⊆ range p ∪ range q"
   by simp
  ultimately have "?U' ⊆ range Some ⟶
    (map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
    (map (inv p) [x←xs @ [y]. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys),
     inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y) ∈ failures P" ..
  moreover assume D: "U ⊆ range Some"
  hence "?U' ⊆ range Some"
  proof (cases "∃u ∈ U. (u, ?D' y) ∈ ?I'", simp_all add: sinks_aux_single_event)
    have "y ∈ range p ∪ range q"
     using C by simp
    thus "?D' y ∈ range Some"
     by (cases "y ∈ range p", simp_all)
  qed
  ultimately have
   "(map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p], inv p ` Y) ∈ failures P ⟶
    (map (inv p) [x←xs @ [y]. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys),
     inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y) ∈ failures P" ..
  moreover assume
   "(map (inv p) [x←xs @ y # ys. x ∈ range p], inv p ` Y) ∈ failures P"
  ultimately have
   "(map (inv p) [x←xs @ [y]. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys),
     inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y) ∈ failures P"
   by simp
  hence
   "(map (inv p) [x←xs. x ∈ range p] @
     map (inv p) ((if y ∈ range p then [y] else []) @
       ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys),
     inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y) ∈ failures P"
   by (cases "y ∈ range p", simp_all)
  with A have
   "(map (inv p) [x←xs. x ∈ range p] @
     ipurge_tr_aux I D (the ` U) (map (inv p) ((if y ∈ range p then [y] else []) @
       ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys)),
     ipurge_ref_aux I D (the ` U) (map (inv p) ((if y ∈ range p then [y] else []) @
       ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys))
     (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y)) ∈ failures P"
   by (rule ipurge_tr_ref_aux_failures_general)
  moreover have
   "ipurge_tr_aux I D (the ` U) (map (inv p) ((if y ∈ range p then [y] else []) @
      ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys)) =
    map (inv p) (ipurge_tr_aux ?I' ?D' U ((if y ∈ range p then [y] else []) @
      ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys))"
   by (rule con_comp_ipurge_tr_aux, simp_all add:
    D ipurge_tr_aux_foldr_eq [symmetric], blast)
  moreover have
   "ipurge_ref_aux I D (the ` U) (map (inv p) ((if y ∈ range p then [y] else []) @
      ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys))
      (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y) =
    inv p ` ipurge_ref_aux ?I' ?D' U ((if y ∈ range p then [y] else []) @
      ipurge_tr_aux_foldr ?I' ?D' ?F ?U' ys)
      (ipurge_ref_aux_foldr ?I' ?D' ?F ?U' ys Y)"
  proof (rule con_comp_ipurge_ref_aux, simp_all add:
   D ipurge_tr_aux_foldr_eq [symmetric] ipurge_ref_aux_foldr_eq [symmetric], blast)
    have "ipurge_ref_aux ?I' ?D' ?U' ys Y ⊆ Y"
     by (rule ipurge_ref_aux_subset)
    thus "ipurge_ref_aux ?I' ?D' ?U' ys Y ⊆ range p"
     using B by simp
  qed
  ultimately show
   "(map (inv p) [x←xs. x ∈ range p] @
     map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F U (y # ys)),
     inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F U (y # ys) Y) ∈ failures P"
   by simp
qed


subsection "Conservation of noninterference security under concurrent composition"

text ‹
Everything is now ready for proving the target security conservation theorem. It states that for any
two processes @{term P}, @{term Q} being secure with respect to the noninterference policy @{term I}
and the event-domain maps @{term D}, @{term E}, their concurrent composition @{term "P ∥ Q <p, q>"}
is secure with respect to the noninterference policy @{term "con_comp_pol I"} and the event-domain
map @{term "con_comp_map D E p q"}, provided that condition @{term "consistent_maps D E p q"} is
satisfied.

The only assumption, in addition to the security of the input processes, is the consistency of the
respective event-domain maps. Particularly, this assumption permits to solve the proof obligations
concerning the latter input process by just swapping @{term D} for @{term E} and @{term p} for
@{term q} in the term @{term "con_comp_map D E p q"} and then applying the corresponding lemmas
proven for the former input process.

\null
›

lemma con_comp_secure_del_aux_1:
  assumes
    A: "secure P I D" and
    B: "y ∈ range p ∨ y ∈ range q" and
    C: "set ys ⊆ range p ∪ range q" and
    D: "Y ⊆ range p" and
    E: "(map (inv p) [x←xs @ y # ys. x ∈ range p], inv p ` Y) ∈ failures P"
  shows
   "(map (inv p) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
       (con_comp_map D E p q y) ys. x ∈ range p],
     inv p ` ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
       (con_comp_map D E p q y) ys Y) ∈ failures P"
    (is "(map (inv p) [x←xs @ ipurge_tr ?I' ?D' _ _. _], _) ∈ _")
proof (simp add:
 ipurge_tr_aux_single_dom [symmetric] ipurge_ref_aux_single_dom [symmetric]
 ipurge_tr_aux_foldr_eq ipurge_ref_aux_foldr_eq [where P = "λx. x ∈ range p"])
  have "(map (inv p) [x←xs @ [y]. x ∈ range p] @
    map (inv p) (ipurge_tr_aux_foldr ?I' ?D' (λx. x ∈ range p) {?D' y} ys),
    inv p ` ipurge_ref_aux_foldr ?I' ?D' (λx. x ∈ range p) {?D' y} ys Y)
      ∈ failures P"
    (is "(_ @ map (inv p) (ipurge_tr_aux_foldr _ _ ?F _ _), _) ∈ _")
  proof (rule con_comp_secure_aux [OF A D C])
    show "{?D' y} ⊆ range Some"
     using B by (cases "y ∈ range p", simp_all)
  next
    show "(map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p], inv p ` Y) ∈ failures P"
     using E by simp
  qed
  thus "(map (inv p) [x←xs. x ∈ range p] @
    map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {?D' y} ys),
    inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {?D' y} ys Y)
      ∈ failures P"
  proof (cases "y ∈ range p", simp_all)
    assume "(map (inv p) [x←xs. x ∈ range p] @ inv p y #
      map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys),
      inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y)
      ∈ failures P"
    hence "(inv p y #
      map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys),
      inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y)
      ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
     by (simp add: futures_def)
    hence
     "(ipurge_tr I D (D (inv p y))
         (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)),
       ipurge_ref I D (D (inv p y))
         (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys))
         (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y))
      ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
     using A by (simp add: secure_def)
    hence
     "(ipurge_tr_aux I D (the ` {Some (D (inv p y))})
         (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)),
       ipurge_ref_aux I D (the ` {Some (D (inv p y))})
         (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys))
         (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y))
      ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
     by (simp add: ipurge_tr_aux_single_dom ipurge_ref_aux_single_dom)
    moreover have
     "ipurge_tr_aux I D (the ` {Some (D (inv p y))})
        (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)) =
      map (inv p) (ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
        (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys))"
     by (rule con_comp_ipurge_tr_aux, simp_all add:
      ipurge_tr_aux_foldr_eq [symmetric], blast)
    moreover have
     "ipurge_ref_aux I D (the ` {Some (D (inv p y))})
        (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys))
        (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y) =
      inv p ` ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
        (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)
        (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y)"
    proof (rule con_comp_ipurge_ref_aux, simp_all add:
     ipurge_tr_aux_foldr_eq [symmetric] ipurge_ref_aux_foldr_eq [symmetric], blast)
      have "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))} ys Y ⊆ Y"
       by (rule ipurge_ref_aux_subset)
      thus "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))} ys Y ⊆ range p"
       using D by simp
    qed
    ultimately have
     "(map (inv p) (ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
         (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)),
       inv p ` ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
         (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)
         (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y))
      ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
     by simp
    moreover have
     "ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
        (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys) =
      ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys"
     by (rule ipurge_tr_aux_foldr_subset, simp)
    moreover have
     "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
        (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys)
        (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y) =
      ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y"
     by (rule ipurge_ref_aux_foldr_subset, subst ipurge_tr_aux_foldr_sinks_aux, simp)
    ultimately have
     "(map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys),
       inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y)
      ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
     by simp
    thus "(map (inv p) [x←xs. x ∈ range p] @
      map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys),
      inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} ys Y)
      ∈ failures P"
     by (simp add: futures_def)
  qed
qed

lemma con_comp_secure_add_aux_1:
  assumes
    A: "secure P I D" and
    B: "y ∈ range p ∨ y ∈ range q" and
    C: "set zs ⊆ range p ∪ range q" and
    D: "Z ⊆ range p" and
    E: "(map (inv p) [x←xs @ zs. x ∈ range p], inv p ` Z) ∈ failures P" and
    F: "map (inv p) [x←xs @ [y]. x ∈ range p] ∈ traces P"
  shows
   "(map (inv p) [x←xs @ y # ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
       (con_comp_map D E p q y) zs. x ∈ range p],
     inv p ` ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
       (con_comp_map D E p q y) zs Z) ∈ failures P"
    (is "(map (inv p) [x←xs @ y # ipurge_tr ?I' ?D' _ _. _], _) ∈ _")
proof -
  have
   "(map (inv p) [x←(xs @ [y]) @ ipurge_tr ?I' ?D' (?D' y) zs. x ∈ range p],
     inv p ` ipurge_ref ?I' ?D' (?D' y) zs Z) ∈ failures P"
  proof (subst filter_append, simp del: filter_append add:
   ipurge_tr_aux_single_dom [symmetric] ipurge_ref_aux_single_dom [symmetric]
   ipurge_tr_aux_foldr_eq ipurge_ref_aux_foldr_eq [where P = "λx. x ∈ range p"])
    have "(map (inv p) [x←xs. x ∈ range p] @
      map (inv p) (ipurge_tr_aux_foldr ?I' ?D' (λx. x ∈ range p) {?D' y} zs),
      inv p ` ipurge_ref_aux_foldr ?I' ?D' (λx. x ∈ range p) {?D' y} zs Z)
        ∈ failures P"
      (is "(_ @ map (inv p) (ipurge_tr_aux_foldr _ _ ?F _ _), _) ∈ _")
    proof (rule con_comp_secure_aux [OF A D C])
      show "{?D' y} ⊆ range Some"
       using B by (cases "y ∈ range p", simp_all)
    next
      show "(map (inv p) [x←xs @ zs. x ∈ range p], inv p ` Z) ∈ failures P"
       using E .
    qed
    thus "(map (inv p) [x←xs @ [y]. x ∈ range p] @
      map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {?D' y} zs),
      inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {?D' y} zs Z)
        ∈ failures P"
    proof (cases "y ∈ range p", simp_all)
      case True
      assume "(map (inv p) [x←xs. x ∈ range p] @
        map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs),
        inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z)
        ∈ failures P"
      hence
       "(map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs),
         inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z)
        ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       by (simp add: futures_def)
      moreover have "(map (inv p) [x←xs @ [y]. x ∈ range p], {}) ∈ failures P"
       using F by (rule traces_failures)
      hence "([inv p y], {}) ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       using True by (simp add: futures_def)
      ultimately have
       "(inv p y # ipurge_tr I D (D (inv p y))
           (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)),
         ipurge_ref I D (D (inv p y))
           (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs))
           (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z))
        ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       using A by (simp add: secure_def)
      hence
       "(inv p y # ipurge_tr_aux I D (the ` {Some (D (inv p y))})
           (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)),
         ipurge_ref_aux I D (the ` {Some (D (inv p y))})
           (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs))
           (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z))
        ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       by (simp add: ipurge_tr_aux_single_dom ipurge_ref_aux_single_dom)
      moreover have
       "ipurge_tr_aux I D (the ` {Some (D (inv p y))})
          (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)) =
        map (inv p) (ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
          (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs))"
       by (rule con_comp_ipurge_tr_aux, simp_all add:
        ipurge_tr_aux_foldr_eq [symmetric], blast)
      moreover have
       "ipurge_ref_aux I D (the ` {Some (D (inv p y))})
          (map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs))
          (inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z) =
        inv p ` ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
          (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)
          (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z)"
      proof (rule con_comp_ipurge_ref_aux, simp_all add:
       ipurge_tr_aux_foldr_eq [symmetric] ipurge_ref_aux_foldr_eq [symmetric], blast)
        have "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))} zs Z ⊆ Z"
         by (rule ipurge_ref_aux_subset)
        thus "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))} zs Z ⊆ range p"
         using D by simp
      qed
      ultimately have
       "(inv p y # map (inv p) (ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
           (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)),
         inv p ` ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
           (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)
           (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z))
        ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       by simp
      moreover have
       "ipurge_tr_aux ?I' ?D' {Some (D (inv p y))}
          (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs) =
        ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs"
       by (rule ipurge_tr_aux_foldr_subset, simp)
      moreover have
       "ipurge_ref_aux ?I' ?D' {Some (D (inv p y))}
          (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs)
          (ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z) =
        ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z"
       by (rule ipurge_ref_aux_foldr_subset, subst ipurge_tr_aux_foldr_sinks_aux, simp)
      ultimately have
       "(inv p y # map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F
           {Some (D (inv p y))} zs),
         inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F
           {Some (D (inv p y))} zs Z)
        ∈ futures P (map (inv p) [x←xs. x ∈ range p])"
       by simp
      thus "(map (inv p) [x←xs. x ∈ range p] @ inv p y #
        map (inv p) (ipurge_tr_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs),
        inv p ` ipurge_ref_aux_foldr ?I' ?D' ?F {Some (D (inv p y))} zs Z)
        ∈ failures P"
       by (simp add: futures_def)
    qed
  qed
  thus ?thesis
   by simp
qed

lemma con_comp_consistent_maps:
 "consistent_maps D E p q ⟹ con_comp_map D E p q = con_comp_map E D q p"
using [[simproc del: defined_all]] proof (simp add: consistent_maps_def, rule ext)
  fix x
  assume A: "∀x ∈ range p ∩ range q. D (inv p x) = E (inv q x)"
  show "con_comp_map D E p q x = con_comp_map E D q p x"
  proof (rule con_comp_map.cases [of "(D, E, p, q, x)"], simp_all, (erule conjE)+)
    fix p' q' D' E' x'
    assume
      B: "p = p'" and
      C: "q = q'" and
      D: "D = D'" and
      E: "E = E'" and
      F: "x' ∈ range p'"
    show "Some (D' (inv p' x')) = con_comp_map E' D' q' p' x'"
    proof (cases "x' ∈ range q'", simp_all add: F)
      case True
      with F have "x' ∈ range p' ∩ range q'" ..
      hence "x' ∈ range p ∩ range q"
       using B and C by simp
      with A have "D (inv p x') = E (inv q x')" ..
      thus "D' (inv p' x') = E' (inv q' x')"
       using B and C and D and E by simp
    qed
  qed
qed

lemma con_comp_secure_del_aux_2:
  assumes A: "consistent_maps D E p q"
  shows
   "secure Q I E ⟹
    y ∈ range p ∨ y ∈ range q ⟹
    set ys ⊆ range p ∪ range q ⟹
    Y ⊆ range q ⟹
    (map (inv q) [x←xs @ y # ys. x ∈ range q], inv q ` Y) ∈ failures Q ⟹
      (map (inv q) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) ys. x ∈ range q],
       inv q ` ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) ys Y) ∈ failures Q"
proof (simp only: con_comp_consistent_maps [OF A], rule con_comp_secure_del_aux_1)
qed (simp_all, blast+)

lemma con_comp_secure_add_aux_2:
  assumes A: "consistent_maps D E p q"
  shows
   "secure Q I E ⟹
    y ∈ range p ∨ y ∈ range q ⟹
    set zs ⊆ range p ∪ range q ⟹
    Z ⊆ range q ⟹
    (map (inv q) [x←xs @ zs. x ∈ range q], inv q ` Z) ∈ failures Q ⟹
    map (inv q) [x←xs @ [y]. x ∈ range q] ∈ traces Q ⟹
      (map (inv q) [x←xs @ y # ipurge_tr (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs. x ∈ range q],
       inv q ` ipurge_ref (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs Z) ∈ failures Q"
proof (simp only: con_comp_consistent_maps [OF A], rule con_comp_secure_add_aux_1)
qed (simp_all, blast+)

lemma con_comp_secure_del_case_1:
  assumes
    A: "consistent_maps D E p q" and
    B: "secure P I D" and
    C: "secure Q I E"
  shows
   "∃R S T.
      Y = R ∪ S ∪ T ∧
      (y ∈ range p ∨ y ∈ range q) ∧
      set xs ⊆ range p ∪ range q ∧
      set ys ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ y # ys. x ∈ range p], inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ y # ys. x ∈ range q], inv q ` S) ∈ failures Q ⟹
    ∃R S T.
      ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys Y = R ∪ S ∪ T ∧
      set xs ⊆ range p ∪ range q ∧                     
      set (ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys) ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys. x ∈ range p], inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys. x ∈ range q], inv q ` S) ∈ failures Q"
  (is "_ ⟹ ∃_ _ _. ipurge_ref ?I' ?D' _ _ _ = _ ∧ _")
proof ((erule exE)+, (erule conjE)+)
  fix R S T
  assume
    D: "Y = R ∪ S ∪ T" and
    E: "y ∈ range p ∨ y ∈ range q" and
    F: "set xs ⊆ range p ∪ range q" and
    G: "set ys ⊆ range p ∪ range q" and
    H: "R ⊆ range p" and
    I: "S ⊆ range q" and
    J: "T ⊆ - range p" and
    K: "T ⊆ - range q" and
    L: "(map (inv p) [x←xs @ y # ys. x ∈ range p], inv p ` R) ∈ failures P" and
    M: "(map (inv q) [x←xs @ y # ys. x ∈ range q], inv q ` S) ∈ failures Q"
  show ?thesis
  proof (rule_tac x = "ipurge_ref ?I' ?D' (?D' y) ys R" in exI,
   rule_tac x = "ipurge_ref ?I' ?D' (?D' y) ys S" in exI, rule_tac x = "{}" in exI,
   (subst conj_assoc [symmetric])+, (rule conjI)+, simp_all del: filter_append)
    have "ipurge_ref ?I' ?D' (?D' y) ys Y =
      ipurge_ref ?I' ?D' (?D' y) ys (R ∪ S ∪ T)"
     using D by simp
    hence "ipurge_ref ?I' ?D' (?D' y) ys Y =
      ipurge_ref ?I' ?D' (?D' y) ys R ∪
      ipurge_ref ?I' ?D' (?D' y) ys S ∪
      ipurge_ref ?I' ?D' (?D' y) ys T"
     by (simp add: ipurge_ref_distrib_union)
    moreover have "ipurge_ref ?I' ?D' (?D' y) ys T = {}"
    proof (rule ipurge_ref_empty [of "?D' y"], simp, insert E,
     cases "y ∈ range p", simp_all)
      fix x
      assume N: "x ∈ T"
      with J have "x ∈ - range p" ..
      moreover have "x ∈ - range q"
       using K and N ..
      ultimately have "?D' x = None"
       by simp
      thus "(Some (D (inv p y)), ?D' x) ∈ ?I'"
       by (simp add: con_comp_pol_def)
    next
      fix x
      assume N: "x ∈ T"
      with J have "x ∈ - range p" ..
      moreover have "x ∈ - range q"
       using K and N ..
      ultimately have "?D' x = None"
       by simp
      thus "(Some (E (inv q y)), ?D' x) ∈ ?I'"
       by (simp add: con_comp_pol_def)
    qed
    ultimately show "ipurge_ref ?I' ?D' (?D' y) ys Y =
      ipurge_ref ?I' ?D' (?D' y) ys R ∪
      ipurge_ref ?I' ?D' (?D' y) ys S"
     by simp
  next
    show "set xs ⊆ range p ∪ range q"
     using F .
  next
    have "set (ipurge_tr ?I' ?D' (?D' y) ys) ⊆ set ys"
     by (rule ipurge_tr_set)
    thus "set (ipurge_tr ?I' ?D' (?D' y) ys) ⊆ range p ∪ range q"
     using G by simp
  next
    have "ipurge_ref ?I' ?D' (?D' y) ys R ⊆ R"
     by (rule ipurge_ref_subset)
    thus "ipurge_ref ?I' ?D' (?D' y) ys R ⊆ range p"
     using H by simp
  next
    have "ipurge_ref ?I' ?D' (?D' y) ys S ⊆ S"
     by (rule ipurge_ref_subset)
    thus "ipurge_ref ?I' ?D' (?D' y) ys S ⊆ range q"
     using I by simp
  next
    show "(map (inv p) [x←xs @ ipurge_tr ?I' ?D' (?D' y) ys. x ∈ range p],
      inv p ` ipurge_ref ?I' ?D' (?D' y) ys R) ∈ failures P"
     by (rule con_comp_secure_del_aux_1 [OF B E G H L])
  next
    show "(map (inv q) [x←xs @ ipurge_tr ?I' ?D' (?D' y) ys. x ∈ range q],
      inv q ` ipurge_ref ?I' ?D' (?D' y) ys S) ∈ failures Q"
     by (rule con_comp_secure_del_aux_2 [OF A C E G I M])
  qed
qed

lemma con_comp_secure_del_case_2:
  assumes
    A: "consistent_maps D E p q" and
    B: "secure P I D" and
    C: "secure Q I E"
  shows
   "∃xs'.
      (∃ys'. xs @ y # ys = xs' @ ys') ∧
      set xs' ⊆ range p ∪ range q ∧
      map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q ⟹
    (∃R S T.
      ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys Y = R ∪ S ∪ T ∧
      set xs ⊆ range p ∪ range q ∧
      set (ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys) ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys. x ∈ range p], inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys. x ∈ range q], inv q ` S) ∈ failures Q) ∨
    (∃xs'.
      (∃ys'. xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) ys = xs' @ ys') ∧
      set xs' ⊆ range p ∪ range q ∧
      map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q)"
  (is "_ ⟹ (∃R S T. ?F R S T ys) ∨ ?G")
proof (erule exE, (erule conjE)+, erule exE)
  fix xs' ys'
  assume
    D: "set xs' ⊆ range p ∪ range q" and
    E: "map (inv p) [x←xs'. x ∈ range p] ∈ divergences P" and
    F: "map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q" and
    G: "xs @ y # ys = xs' @ ys'"
  show ?thesis
  proof (cases "length xs < length xs'", rule disjI1, rule_tac [2] disjI2)
    case True
    moreover have "take (length xs') (xs @ [y] @ ys) =
      take (length xs') (xs @ [y]) @ take (length xs' - Suc (length xs)) ys"
     by (simp only: take_append, simp)
    ultimately have "take (length xs') (xs @ [y] @ ys) =
      xs @ y # take (length xs' - Suc (length xs)) ys"
      (is "_ = _ @ _ # ?vs")
     by simp
    moreover have "take (length xs') (xs @ [y] @ ys) =
      take (length xs') (xs' @ ys')"
     using G by simp
    ultimately have H: "xs @ y # ?vs = xs'"
     by simp
    moreover have "y ∈ set (xs @ y # ?vs)"
     by simp
    ultimately have "y ∈ set xs'"
     by simp
    with D have I: "y ∈ range p ∪ range q" ..
    have "set xs ⊆ set (xs @ y # ?vs)"
     by auto
    hence "set xs ⊆ set xs'"
     using H by simp
    hence J: "set xs ⊆ range p ∪ range q"
     using D by simp
    have "∃R S T. ?F R S T [x←ys. x ∈ range p ∪ range q]"
      (is "∃_ _ _. ipurge_ref ?I' ?D' _ _ _ = _ ∧ _")
    proof (rule con_comp_secure_del_case_1 [OF A B C],
     rule_tac x = "range p ∩ Y" in exI, rule_tac x = "range q ∩ Y" in exI,
     rule_tac x = "- range p ∩ - range q ∩ Y" in exI,
     (subst conj_assoc [symmetric])+, (rule conjI)+, simp_all del: filter_append)
      show "Y = range p ∩ Y ∪ range q ∩ Y ∪ - range p ∩ - range q ∩ Y"
       by blast
    next
      show "y ∈ range p ∨ y ∈ range q"
       using I by simp
    next
      show "set xs ⊆ range p ∪ range q"
       using J .
    next
      show "{x ∈ set ys. x ∈ range p ∨ x ∈ range q} ⊆ range p ∪ range q"
       by blast
    next
      show "- range p ∩ - range q ∩ Y ⊆ - range p"
       by blast
    next
      show "- range p ∩ - range q ∩ Y ⊆ - range q"
       by blast
    next
      have "map (inv p) [x←xs @ y # ?vs. x ∈ range p] ∈ divergences P"
       using E and H by simp
      hence "map (inv p) [x←xs @ y # ?vs. x ∈ range p] @
        map (inv p) [x←drop (length xs' - Suc (length xs)) ys. x ∈ range p]
        ∈ divergences P"
        (is "_ @ map (inv p) [x←?ws. _] ∈ _")
       by (rule process_rule_5_general)
      hence "map (inv p) [x←(xs @ y # ?vs) @ ?ws. x ∈ range p] ∈ divergences P"
       by (subst filter_append, simp)
      hence "map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p] ∈ divergences P"
       by simp
      hence "map (inv p) [x←(xs @ [y]) @ [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range p] ∈ divergences P"
      proof (subst (asm) filter_append, subst filter_append, subst filter_filter)
      qed (subgoal_tac "(λx. (x ∈ range p ∨ x ∈ range q) ∧ x ∈ range p) =
       (λx. x ∈ range p)", simp, blast)
      hence "map (inv p) [x←xs @ y # [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range p] ∈ divergences P"
       by simp
      thus "(map (inv p) [x←xs @ y # [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range p], inv p ` (range p ∩ Y)) ∈ failures P"
       by (rule process_rule_6)
    next
      have "map (inv q) [x←xs @ y # ?vs. x ∈ range q] ∈ divergences Q"
       using F and H by simp
      hence "map (inv q) [x←xs @ y # ?vs. x ∈ range q] @
        map (inv q) [x←drop (length xs' - Suc (length xs)) ys. x ∈ range q]
        ∈ divergences Q"
        (is "_ @ map (inv q) [x←?ws. _] ∈ _")
       by (rule process_rule_5_general)
      hence "map (inv q) [x←(xs @ y # ?vs) @ ?ws. x ∈ range q] ∈ divergences Q"
       by (subst filter_append, simp)
      hence "map (inv q) [x←(xs @ [y]) @ ys. x ∈ range q] ∈ divergences Q"
       by simp
      hence "map (inv q) [x←(xs @ [y]) @ [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range q] ∈ divergences Q"
      proof (subst (asm) filter_append, subst filter_append, subst filter_filter)
      qed (subgoal_tac "(λx. (x ∈ range p ∨ x ∈ range q) ∧ x ∈ range q) =
       (λx. x ∈ range q)", simp, blast)
      hence "map (inv q) [x←xs @ y # [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range q] ∈ divergences Q"
       by simp
      thus "(map (inv q) [x←xs @ y # [x←ys. x ∈ range p ∨ x ∈ range q].
        x ∈ range q], inv q ` (range q ∩ Y)) ∈ failures Q"
       by (rule process_rule_6)
    qed
    then obtain R and S and T where
     "?F R S T [x←ys. x ∈ range p ∪ range q]"
     by blast
    thus "∃R S T. ?F R S T ys"
    proof (rule_tac x = R in exI, rule_tac x = S in exI, rule_tac x = T in exI)
    qed (simp only: con_comp_ipurge_tr_filter con_comp_ipurge_ref_filter)
  next
    let
      ?I' = "con_comp_pol I" and
      ?D' = "con_comp_map D E p q"
    case False
    moreover have "xs @ ipurge_tr ?I' ?D' (?D' y) ys =
      take (length xs') (xs @ ipurge_tr ?I' ?D' (?D' y) ys) @
      drop (length xs') (xs @ ipurge_tr ?I' ?D' (?D' y) ys)"
      (is "_ = _ @ ?vs")
     by (simp only: append_take_drop_id)
    ultimately have "xs @ ipurge_tr ?I' ?D' (?D' y) ys =
      take (length xs') (xs @ y # ys) @ ?vs"
     by simp
    hence H: "xs @ ipurge_tr ?I' ?D' (?D' y) ys = xs' @ ?vs"
     using G by simp
    show ?G
    proof (rule_tac x = xs' in exI, rule conjI, rule_tac x = ?vs in exI)
    qed (subst H, simp_all add: D E F)
  qed
qed

lemma con_comp_secure_add_case_1:
  assumes
    A: "consistent_maps D E p q" and
    B: "secure P I D" and
    C: "secure Q I E" and
    D: "(xs @ y # ys, Y) ∈ con_comp_failures P Q p q" and
    E: "y ∈ range p ∨ y ∈ range q"
  shows
   "∃R S T.
      Z = R ∪ S ∪ T ∧
      set xs ⊆ range p ∪ range q ∧
      set zs ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ zs. x ∈ range p], inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ zs. x ∈ range q], inv q ` S) ∈ failures Q ⟹
    ∃R S T.
      ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) zs Z = R ∪ S ∪ T ∧
      set xs ⊆ range p ∪ range q ∧
      set (ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) zs) ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ y # ipurge_tr (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs. x ∈ range p],
       inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ y # ipurge_tr (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs. x ∈ range q],
       inv q ` S) ∈ failures Q"
  (is "_ ⟹ ∃_ _ _. ipurge_ref ?I' ?D' _ _ _ = _ ∧ _")
proof ((erule exE)+, (erule conjE)+)
  fix R S T
  assume
    F: "Z = R ∪ S ∪ T" and
    G: "set xs ⊆ range p ∪ range q" and
    H: "set zs ⊆ range p ∪ range q" and
    I: "R ⊆ range p" and
    J: "S ⊆ range q" and
    K: "T ⊆ - range p" and
    L: "T ⊆ - range q" and
    M: "(map (inv p) [x←xs @ zs. x ∈ range p], inv p ` R) ∈ failures P" and
    N: "(map (inv q) [x←xs @ zs. x ∈ range q], inv q ` S) ∈ failures Q"
  show ?thesis
  proof (rule_tac x = "ipurge_ref ?I' ?D' (?D' y) zs R" in exI,
   rule_tac x = "ipurge_ref ?I' ?D' (?D' y) zs S" in exI, rule_tac x = "{}" in exI,
   (subst conj_assoc [symmetric])+, (rule conjI)+, simp_all del: filter_append)
    have "ipurge_ref ?I' ?D' (?D' y) zs Z =
      ipurge_ref ?I' ?D' (?D' y) zs (R ∪ S ∪ T)"
     using F by simp
    hence "ipurge_ref ?I' ?D' (?D' y) zs Z =
      ipurge_ref ?I' ?D' (?D' y) zs R ∪
      ipurge_ref ?I' ?D' (?D' y) zs S ∪
      ipurge_ref ?I' ?D' (?D' y) zs T"
     by (simp add: ipurge_ref_distrib_union)
    moreover have "ipurge_ref ?I' ?D' (?D' y) zs T = {}"
    proof (rule ipurge_ref_empty [of "?D' y"], simp, insert E,
     cases "y ∈ range p", simp_all)
      fix x
      assume O: "x ∈ T"
      with K have "x ∈ - range p" ..
      moreover have "x ∈ - range q"
       using L and O ..
      ultimately have "?D' x = None"
       by simp
      thus "(Some (D (inv p y)), ?D' x) ∈ ?I'"
       by (simp add: con_comp_pol_def)
    next
      fix x
      assume O: "x ∈ T"
      with K have "x ∈ - range p" ..
      moreover have "x ∈ - range q"
       using L and O ..
      ultimately have "?D' x = None"
       by simp
      thus "(Some (E (inv q y)), ?D' x) ∈ ?I'"
       by (simp add: con_comp_pol_def)
    qed
    ultimately show "ipurge_ref ?I' ?D' (?D' y) zs Z =
      ipurge_ref ?I' ?D' (?D' y) zs R ∪
      ipurge_ref ?I' ?D' (?D' y) zs S"
     by simp
  next
    show "set xs ⊆ range p ∪ range q"
     using G .
  next
    have "set (ipurge_tr ?I' ?D' (?D' y) zs) ⊆ set zs"
     by (rule ipurge_tr_set)
    thus "set (ipurge_tr ?I' ?D' (?D' y) zs) ⊆ range p ∪ range q"
     using H by simp
  next
    have "ipurge_ref ?I' ?D' (?D' y) zs R ⊆ R"
     by (rule ipurge_ref_subset)
    thus "ipurge_ref ?I' ?D' (?D' y) zs R ⊆ range p"
     using I by simp
  next
    have "ipurge_ref ?I' ?D' (?D' y) zs S ⊆ S"
     by (rule ipurge_ref_subset)
    thus "ipurge_ref ?I' ?D' (?D' y) zs S ⊆ range q"
     using J by simp
  next
    have "map (inv p) [x←xs @ y # ys. x ∈ range p] ∈ traces P ∧
      map (inv q) [x←xs @ y # ys. x ∈ range q] ∈ traces Q"
     using D by (rule con_comp_failures_traces)
    hence "map (inv p) [x←(xs @ [y]) @ ys. x ∈ range p] ∈ traces P"
     by simp
    hence "map (inv p) [x←xs @ [y]. x ∈ range p] @
      map (inv p) [x←ys. x ∈ range p] ∈ traces P"
     by (subst (asm) filter_append, simp)
    hence "map (inv p) [x←xs @ [y]. x ∈ range p] ∈ traces P"
     by (rule process_rule_2_traces)
    thus "(map (inv p) [x←xs @ y # ipurge_tr ?I' ?D' (?D' y) zs. x ∈ range p],
      inv p ` ipurge_ref ?I' ?D' (?D' y) zs R) ∈ failures P"
     by (rule con_comp_secure_add_aux_1 [OF B E H I M])
  next
    have "map (inv p) [x←xs @ y # ys. x ∈ range p] ∈ traces P ∧
      map (inv q) [x←xs @ y # ys. x ∈ range q] ∈ traces Q"
     using D by (rule con_comp_failures_traces)
    hence "map (inv q) [x←(xs @ [y]) @ ys. x ∈ range q] ∈ traces Q"
     by simp
    hence "map (inv q) [x←xs @ [y]. x ∈ range q] @
      map (inv q) [x←ys. x ∈ range q] ∈ traces Q"
     by (subst (asm) filter_append, simp)
    hence "map (inv q) [x←xs @ [y]. x ∈ range q] ∈ traces Q"
     by (rule process_rule_2_traces)
    thus "(map (inv q) [x←xs @ y # ipurge_tr ?I' ?D' (?D' y) zs. x ∈ range q],
      inv q ` ipurge_ref ?I' ?D' (?D' y) zs S) ∈ failures Q"
     by (rule con_comp_secure_add_aux_2 [OF A C E H J N])
  qed
qed

lemma con_comp_secure_add_case_2:
  assumes
    A: "consistent_maps D E p q" and
    B: "secure P I D" and
    C: "secure Q I E" and
    D: "(xs @ y # ys, Y) ∈ con_comp_failures P Q p q" and
    E: "y ∈ range p ∨ y ∈ range q"
  shows
   "∃xs'.
      (∃ys'. xs @ zs = xs' @ ys') ∧
      set xs' ⊆ range p ∪ range q ∧
      map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q ⟹
    (∃R S T.
      ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) zs Z = R ∪ S ∪ T ∧
      set xs ⊆ range p ∪ range q ∧
      set (ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) zs) ⊆ range p ∪ range q ∧
      R ⊆ range p ∧
      S ⊆ range q ∧
      T ⊆ - range p ∧
      T ⊆ - range q ∧
      (map (inv p) [x←xs @ y # ipurge_tr (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs. x ∈ range p],
       inv p ` R) ∈ failures P ∧
      (map (inv q) [x←xs @ y # ipurge_tr (con_comp_pol I)
         (con_comp_map D E p q) (con_comp_map D E p q y) zs. x ∈ range q],
       inv q ` S) ∈ failures Q) ∨
    (∃xs'.
      (∃ys'. xs @ y # ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
        (con_comp_map D E p q y) zs = xs' @ ys') ∧
      set xs' ⊆ range p ∪ range q ∧
      map (inv p) [x←xs'. x ∈ range p] ∈ divergences P ∧
      map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q)"
  (is "_ ⟹ (∃R S T. ?F R S T zs) ∨ ?G")
proof (erule exE, (erule conjE)+, erule exE)
  fix xs' ys'
  assume
    F: "set xs' ⊆ range p ∪ range q" and
    G: "map (inv p) [x←xs'. x ∈ range p] ∈ divergences P" and
    H: "map (inv q) [x←xs'. x ∈ range q] ∈ divergences Q" and
    I: "xs @ zs = xs' @ ys'"
  show ?thesis
  proof (cases "length xs < length xs'", rule disjI1, rule_tac [2] disjI2)
    case True
    moreover have "take (length xs') (xs @ zs) =
      take (length xs') xs @ take (length xs' - length xs) zs"
     by simp
    ultimately have "take (length xs') (xs @ zs) =
      xs @ take (length xs' - length xs) zs"
      (is "_ = _ @ ?vs")
     by simp
    moreover have "take (length xs') (xs @ zs) =
      take (length xs') (xs' @ ys')"
     using I by simp
    ultimately have J: "xs @ ?vs = xs'"
     by simp
    moreover have "set xs ⊆ set (xs @ ?vs)"
     by simp
    ultimately have "set xs ⊆ set xs'"
     by simp
    hence K: "set xs ⊆ range p ∪ range q"
     using F by simp
    have "∃R S T. ?F R S T [x←zs. x ∈ range p ∪ range q]"
      (is "∃_ _ _. ipurge_ref ?I' ?D' _ _ _ = _ ∧ _")
    proof (rule con_comp_secure_add_case_1 [OF A B C D E],
     rule_tac x = "range p ∩ Z" in exI, rule_tac x = "range q ∩ Z" in exI,
     rule_tac x = "- range p ∩ - range q ∩ Z" in exI,
     (subst conj_assoc [symmetric])+, (rule conjI)+, simp_all del: filter_append)
      show "Z = range p ∩ Z ∪ range q ∩ Z ∪ - range p ∩ - range q ∩ Z"
       by blast
    next
      show "set xs ⊆ range p ∪ range q"
       using K .
    next
      show "{x ∈ set zs. x ∈ range p ∨ x ∈ range q} ⊆ range p ∪ range q"
       by blast
    next
      show "- range p ∩ - range q ∩ Z ⊆ - range p"
       by blast
    next
      show "- range p ∩ - range q ∩ Z ⊆ - range q"
       by blast
    next
      have "map (inv p) [x←xs @ ?vs. x ∈ range p] ∈ divergences P"
       using G and J by simp
      hence "map (inv p) [x←xs @ ?vs. x ∈ range p] @
        map (inv p) [x←drop (length xs' - length xs) zs. x ∈ range p]
        ∈ divergences P"
        (is "_ @ map (inv p) [x←?ws. _] ∈ _")
       by (rule process_rule_5_general)
      hence "map (inv p) [x←(xs @ ?vs) @ ?ws. x ∈ range p] ∈ divergences P"
       by (subst filter_append, simp)
      hence "map (inv p) [x←xs @ zs. x ∈ range p] ∈ divergences P"
       by simp
      hence "map (inv p) [x←xs @ [x←zs. x ∈ range p ∨ x ∈ range q].
        x ∈ range p] ∈ divergences P"
      proof (subst (asm) filter_append, subst filter_append, subst filter_filter)
      qed (subgoal_tac "(λx. (x ∈ range p ∨ x ∈ range q) ∧ x ∈ range p) =
       (λx. x ∈ range p)", simp, blast)
      thus "(map (inv p) [x←xs @ [x←zs. x ∈ range p ∨ x ∈ range q].
        x ∈ range p], inv p ` (range p ∩ Z)) ∈ failures P"
       by (rule process_rule_6)
    next
      have "map (inv q) [x←xs @ ?vs. x ∈ range q] ∈ divergences Q"
       using H and J by simp
      hence "map (inv q) [x←xs @ ?vs. x ∈ range q] @
        map (inv q) [x←drop (length xs' - length xs) zs. x ∈ range q]
        ∈ divergences Q"
        (is "_ @ map (inv q) [x←?ws. _] ∈ _")
       by (rule process_rule_5_general)
      hence "map (inv q) [x←(xs @ ?vs) @ ?ws. x ∈ range q] ∈ divergences Q"
       by (subst filter_append, simp)
      hence "map (inv q) [x←xs @ zs. x ∈ range q] ∈ divergences Q"
       by simp
      hence "map (inv q) [x←xs @ [x←zs. x ∈ range p ∨ x ∈ range q].
        x ∈ range q] ∈ divergences Q"
      proof (subst (asm) filter_append, subst filter_append, subst filter_filter)
      qed (subgoal_tac "(λx. (x ∈ range p ∨ x ∈ range q) ∧ x ∈ range q) =
       (λx. x ∈ range q)", simp, blast)
      thus "(map (inv q) [x←xs @ [x←zs. x ∈ range p ∨ x ∈ range q].
        x ∈ range q], inv q ` (range q ∩ Z)) ∈ failures Q"
       by (rule process_rule_6)
    qed
    then obtain R and S and T where
     "?F R S T [x←zs. x ∈ range p ∪ range q]"
     by blast
    thus "∃R S T. ?F R S T zs"
    proof (rule_tac x = R in exI, rule_tac x = S in exI, rule_tac x = T in exI)
    qed (simp only: con_comp_ipurge_tr_filter con_comp_ipurge_ref_filter)
  next
    let
      ?I' = "con_comp_pol I" and
      ?D' = "con_comp_map D E p q"
    case False
    moreover have "xs @ y # ipurge_tr ?I' ?D' (?D' y) zs =
      take (length xs') (xs @ y # ipurge_tr ?I' ?D' (?D' y) zs) @
      drop (length xs') (xs @ y # ipurge_tr ?I' ?D' (?D' y) zs)"
      (is "_ = _ @ ?vs")
     by (simp only: append_take_drop_id)
    ultimately have "xs @ y # ipurge_tr ?I' ?D' (?D' y) zs =
      take (length xs') (xs @ zs) @ ?vs"
     by simp
    hence J: "xs @ y # ipurge_tr ?I' ?D' (?D' y) zs = xs' @ ?vs"
     using I by simp
    show ?G
    proof (rule_tac x = xs' in exI, rule conjI, rule_tac x = ?vs in exI)
    qed (subst J, simp_all add: F G H)
  qed
qed

theorem con_comp_secure:
  assumes
    A: "consistent_maps D E p q" and
    B: "secure P I D" and
    C: "secure Q I E"
  shows "secure (P ∥ Q <p, q>) (con_comp_pol I) (con_comp_map D E p q)"
proof (simp add: secure_def con_comp_futures, (rule allI)+, rule impI,
 erule conjE, rule conjI, (erule rev_mp)+, rotate_tac [2], erule_tac [2] rev_mp)
  fix xs y ys Y zs Z
  show
   "(xs @ zs, Z) ∈ con_comp_failures P Q p q ⟶
    (xs @ y # ys, Y) ∈ con_comp_failures P Q p q ⟶
      (xs @ ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) ys,
       ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) ys Y)
      ∈ con_comp_failures P Q p q"
    (is "_ ⟶ _ ⟶ (_ @ ipurge_tr ?I' ?D' _ _, _) ∈ _")
  proof ((rule impI)+, thin_tac "(xs @ zs, Z) ∈ con_comp_failures P Q p q",
   simp_all add: con_comp_failures_def con_comp_divergences_def
   del: filter_append, erule disjE, rule disjI1)
  qed (erule con_comp_secure_del_case_1 [OF A B C],
   rule con_comp_secure_del_case_2 [OF A B C])
next
  fix xs y ys Y zs Z
  assume D: "(xs @ y # ys, Y) ∈ con_comp_failures P Q p q"
  show
   "(xs @ zs, Z) ∈ con_comp_failures P Q p q ⟶
      (xs @ y # ipurge_tr (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) zs,
       ipurge_ref (con_comp_pol I) (con_comp_map D E p q)
         (con_comp_map D E p q y) zs Z)
      ∈ con_comp_failures P Q p q"
    (is "_ ⟶ (_ @ _ # ipurge_tr ?I' ?D' _ _, _) ∈ _")
  proof (rule impI, simp_all add: con_comp_failures_def con_comp_divergences_def
   del: filter_append, cases "y ∈ range p ∨ y ∈ range q", simp del: filter_append,
   erule disjE, rule disjI1, rule_tac [3] disjI2)
  qed (erule con_comp_secure_add_case_1 [OF A B C D], assumption,
   erule con_comp_secure_add_case_2 [OF A B C D], assumption,
   rule con_comp_failures_divergences [OF D], simp_all)
qed


subsection "Conservation of noninterference security in the absence of fake events"

text ‹
In what follows, it is proven that in the absence of fake events, namely if
@{term "range p ∪ range q = UNIV"}, the output of the concurrent composition of two secure processes
is secure with respect to the same noninterference policy enforced by the input processes, and to
the event-domain map that simply associates each event to the same security domain as the
corresponding events of the input processes.

More formally, for any two processes @{term P}, @{term Q} being secure with respect to the
noninterference policy @{term I} and the event-domain maps @{term D}, @{term E}, their concurrent
composition @{term "P ∥ Q <p, q>"} is secure with respect to the same noninterference policy
@{term I} and the event-domain map @{term "the ∘ con_comp_map D E p q"}, provided that conditions
@{term "range p ∪ range q = UNIV"} and @{term "consistent_maps D E p q"} are satisfied.

\null
›

lemma con_comp_sinks_range:
 "u ∈ range Some ⟹
  set xs ⊆ range p ∪ range q ⟹
    sinks (con_comp_pol I) (con_comp_map D E p q) u xs ⊆ range Some"
by (insert con_comp_sinks_aux_range [of "{u}" xs p q I D E],
 simp add: sinks_aux_single_dom)

lemma con_comp_sinks_no_fake:
  assumes
    A: "range p ∪ range q = UNIV" and
    B: "u ∈ range Some"
  shows "sinks I (the ∘ con_comp_map D E p q) (the u) xs =
    the ` sinks (con_comp_pol I) (con_comp_map D E p q) u xs"
    (is "_ = the ` sinks ?I' ?D' _ _")
proof (induction xs rule: rev_induct, simp)
  fix x xs
  assume C: "sinks I (the ∘ ?D') (the u) xs = the ` sinks ?I' ?D' u xs"
  have "x ∈ range p ∪ range q"
   using A by simp
  hence D: "?D' x = Some (the (?D' x))"
   by (cases "x ∈ range p", simp_all)
  have E: "u = Some (the u)"
   using B by (simp add: image_iff)
  show "sinks I (the ∘ ?D') (the u) (xs @ [x]) = the ` sinks ?I' ?D' u (xs @ [x])"
  proof (cases "(u, ?D' x) ∈ ?I' ∨ (∃v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∈ ?I')")
    case True
    hence "sinks ?I' ?D' u (xs @ [x]) = insert (?D' x) (sinks ?I' ?D' u xs)"
     by simp
    moreover have "(the u, the (?D' x)) ∈ I ∨
      (∃d ∈ sinks I (the ∘ ?D') (the u) xs. (d, the (?D' x)) ∈ I)"
    proof (rule disjE [OF True], rule disjI1, rule_tac [2] disjI2)
      assume "(u, ?D' x) ∈ ?I'"
      hence "(Some (the u), Some (the (?D' x))) ∈ ?I'"
       using D and E by simp
      thus "(the u, the (?D' x)) ∈ I"
       by (simp add: con_comp_pol_def)
    next
      assume "∃v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∈ ?I'"
      then obtain v where F: "v ∈ sinks ?I' ?D' u xs" and G: "(v, ?D' x) ∈ ?I'" ..
      have "sinks ?I' ?D' u xs ⊆ range Some"
       by (rule con_comp_sinks_range, simp_all add: A B)
      hence "v ∈ range Some"
       using F ..
      hence "v = Some (the v)"
       by (simp add: image_iff)
      hence "(Some (the v), Some (the (?D' x))) ∈ ?I'"
       using D and G by simp
      hence "(the v, the (?D' x)) ∈ I"
       by (simp add: con_comp_pol_def)
      moreover have "the v ∈ sinks I (the ∘ ?D') (the u) xs"
       using C and F by simp
      ultimately show "∃d ∈ sinks I (the ∘ ?D') (the u) xs.
        (d, the (?D' x)) ∈ I" ..
    qed
    hence "sinks I (the ∘ ?D') (the u) (xs @ [x]) =
      insert (the (?D' x)) (sinks I (the ∘ ?D') (the u) xs)"
     by simp
    ultimately show ?thesis
     using C by simp
  next
    case False
    hence "sinks ?I' ?D' u (xs @ [x]) = sinks ?I' ?D' u xs"
     by simp
    moreover have "¬ ((the u, the (?D' x)) ∈ I ∨
      (∃v ∈ sinks I (the ∘ ?D') (the u) xs. (v, the (?D' x)) ∈ I))"
    proof (insert False, simp, erule conjE, rule conjI, rule_tac [2] ballI)
      assume "(u, ?D' x) ∉ ?I'"
      hence "(Some (the u), Some (the (?D' x))) ∉ ?I'"
       using D and E by simp
      thus "(the u, the (?D' x)) ∉ I"
       by (simp add: con_comp_pol_def)
    next
      fix d
      assume "d ∈ sinks I (the ∘ ?D') (the u) xs"
      hence "d ∈ the ` sinks ?I' ?D' u xs"
       using C by simp
      hence "∃v ∈ sinks ?I' ?D' u xs. d = the v"
       by (simp add: image_iff)
      then obtain v where F: "v ∈ sinks ?I' ?D' u xs" and G: "d = the v" ..
      have "sinks ?I' ?D' u xs ⊆ range Some"
       by (rule con_comp_sinks_range, simp_all add: A B)
      hence "v ∈ range Some"
       using F ..
      hence H: "v = Some d"
       using G by (simp add: image_iff)
      assume "∀v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∉ ?I'"
      hence "(v, ?D' x) ∉ ?I'"
       using F ..
      hence "(Some d, Some (the (?D' x))) ∉ ?I'"
       using D and H by simp
      thus "(d, the (?D' x)) ∉ I"
       by (simp add: con_comp_pol_def)
    qed
    hence "sinks I (the ∘ ?D') (the u) (xs @ [x]) = sinks I (the ∘ ?D') (the u) xs"
     by simp
    ultimately show ?thesis
     using C by simp
  qed
qed

lemma con_comp_ipurge_tr_no_fake:
  assumes
    A: "range p ∪ range q = UNIV" and
    B: "u ∈ range Some"
  shows "ipurge_tr (con_comp_pol I) (con_comp_map D E p q) u xs =
    ipurge_tr I (the ∘ con_comp_map D E p q) (the u) xs"
    (is "ipurge_tr ?I' ?D' _ _ = _")
proof (induction xs rule: rev_induct, simp)
  fix x xs
  assume C: "ipurge_tr ?I' ?D' u xs = ipurge_tr I (the ∘ ?D') (the u) xs"
  show "ipurge_tr ?I' ?D' u (xs @ [x]) = ipurge_tr I (the ∘ ?D') (the u) (xs @ [x])"
  proof (cases "?D' x ∈ sinks ?I' ?D' u (xs @ [x])")
    case True
    hence "ipurge_tr ?I' ?D' u (xs @ [x]) = ipurge_tr ?I' ?D' u xs"
     by simp
    moreover have "the (?D' x) ∈ the ` sinks ?I' ?D' u (xs @ [x])"
     using True by simp
    hence "the (?D' x) ∈ sinks I (the ∘ ?D') (the u) (xs @ [x])"
     by (subst con_comp_sinks_no_fake [OF A B])
    hence "ipurge_tr I (the ∘ ?D') (the u) (xs @ [x]) =
      ipurge_tr I (the ∘ ?D') (the u) xs"
     by simp
    ultimately show ?thesis
     using C by simp
  next
    case False
    hence "ipurge_tr ?I' ?D' u (xs @ [x]) = ipurge_tr ?I' ?D' u xs @ [x]"
     by simp
    moreover have "the (?D' x) ∉ the ` sinks ?I' ?D' u (xs @ [x])"
    proof
      assume "the (?D' x) ∈ the ` sinks ?I' ?D' u (xs @ [x])"
      hence "∃v ∈ sinks ?I' ?D' u (xs @ [x]). the (?D' x) = the v"
       by (simp add: image_iff)
      then obtain v where
        D: "v ∈ sinks ?I' ?D' u (xs @ [x])" and E: "the (?D' x) = the v" ..
      have "x ∈ range p ∪ range q"
       using A by simp
      hence "∃d. ?D' x = Some d"
       by (cases "x ∈ range p", simp_all)
      then obtain d where "?D' x = Some d" ..
      moreover have "sinks ?I' ?D' u (xs @ [x]) ⊆ range Some"
       by (rule con_comp_sinks_range, simp_all add: A B)
      hence "v ∈ range Some"
       using D ..
      hence "∃d'. v = Some d'"
       by (simp add: image_iff)
      then obtain d' where "v = Some d'" ..
      ultimately have "?D' x = v"
       using E by simp
      hence "?D' x ∈ sinks ?I' ?D' u (xs @ [x])"
       using D by simp
      thus False
       using False by contradiction
    qed
    hence "the (?D' x) ∉ sinks I (the ∘ ?D') (the u) (xs @ [x])"
     by (subst con_comp_sinks_no_fake [OF A B])
    hence "ipurge_tr I (the ∘ ?D') (the u) (xs @ [x]) =
      ipurge_tr I (the ∘ ?D') (the u) xs @ [x]"
     by simp
    ultimately show ?thesis
     using C by simp
  qed
qed

lemma con_comp_ipurge_ref_no_fake:
  assumes
    A: "range p ∪ range q = UNIV" and
    B: "u ∈ range Some"
  shows "ipurge_ref (con_comp_pol I) (con_comp_map D E p q) u xs X =
    ipurge_ref I (the ∘ con_comp_map D E p q) (the u) xs X"
    (is "ipurge_ref ?I' ?D' _ _ _ = _")
proof (simp add: ipurge_ref_def set_eq_iff, rule allI,
 simp_all add: con_comp_sinks_no_fake [OF A B])
  fix x
  have "x ∈ range p ∪ range q"
   using A by simp
  hence C: "?D' x = Some (the (?D' x))"
   by (cases "x ∈ range p", simp_all)
  have D: "u = Some (the u)"
   using B by (simp add: image_iff)
  show
   "(x ∈ X ∧ (u, ?D' x) ∉ con_comp_pol I ∧
      (∀v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∉ con_comp_pol I)) =
    (x ∈ X ∧ (the u, the (?D' x)) ∉ I ∧
      (∀v ∈ sinks ?I' ?D' u xs. (the v, the (?D' x)) ∉ I))"
  proof (rule iffI, (erule_tac [!] conjE)+, simp_all, rule_tac [!] conjI,
   rule_tac [2] ballI, rule_tac [4] ballI)
    assume "(u, ?D' x) ∉ ?I'"
    hence "(Some (the u), Some (the (?D' x))) ∉ ?I'"
     using C and D by simp
    thus "(the u, the (?D' x)) ∉ I"
     by (simp add: con_comp_pol_def)
  next
    fix v
    assume "∀v ∈ sinks ?I' ?D' u xs. (v, ?D' x) ∉ ?I'" and
      E: "v ∈ sinks ?I' ?D' u xs"
    hence "(v, ?D' x) ∉ ?I'" ..
    moreover have "sinks ?I' ?D' u xs ⊆ range Some"
     by (rule con_comp_sinks_range, simp_all add: A B)
    hence "v ∈ range Some"
     using E ..
    hence "v = Some (the v)"
     by (simp add: image_iff)
    ultimately have "(Some (the v), Some (the (?D' x))) ∉ ?I'"
     using C by simp
    thus "(the v, the (?D' x)) ∉ I"
     by (simp add: con_comp_pol_def)
  next
    assume "(the u, the (?D' x)) ∉ I"
    hence "(Some (the u), Some (the (?D' x))) ∉ ?I'"
     by (simp add: con_comp_pol_def)
    thus "(u, ?D' x) ∉ ?I'"
     using C and D by simp
  next
    fix v
    assume "∀v ∈ sinks ?I' ?D' u xs. (the v, the (?D' x)) ∉ I" and
      E: "v ∈ sinks ?I' ?D' u xs"
    hence "(the v, the (?D' x)) ∉ I" ..
    hence "(Some (the v), Some (the (?D' x))) ∉ ?I'"
     by (simp add: con_comp_pol_def)
    moreover have "sinks ?I' ?D' u xs ⊆ range Some"
     by (rule con_comp_sinks_range, simp_all add: A B)
    hence "v ∈ range Some"
     using E ..
    hence "v = Some (the v)"
     by (simp add: image_iff)
    ultimately show "(v, ?D' x) ∉ ?I'"
     using C by simp
  qed
qed

theorem con_comp_secure_no_fake:
  assumes
    A: "range p ∪ range q = UNIV" and
    B: "consistent_maps D E p q" and
    C: "secure P I D" and
    D: "secure Q I E"
  shows "secure (P ∥ Q <p, q>) I (the ∘ con_comp_map D E p q)"
proof (insert con_comp_secure [OF B C D], simp add: secure_def,
 (rule allI)+, rule impI)
  fix xs y ys Y zs Z
  let
    ?I' = "con_comp_pol I" and
    ?D' = "con_comp_map D E p q"
  have "y ∈ range p ∪ range q"
   using A by simp
  hence E: "?D' y ∈ range Some"
   by (cases "y ∈ range p", simp_all)
  assume "∀xs y ys Y zs Z.
    (y # ys, Y) ∈ futures (P ∥ Q <p, q>) xs ∧
    (zs, Z) ∈ futures (P ∥ Q <p, q>) xs ⟶
      (ipurge_tr ?I' ?D' (?D' y) ys, ipurge_ref ?I' ?D' (?D' y) ys Y)
        ∈ futures (P ∥ Q <p, q>) xs ∧
      (y # ipurge_tr ?I' ?D' (?D' y) zs, ipurge_ref ?I' ?D' (?D' y) zs Z)
        ∈ futures (P ∥ Q <p, q>) xs" and
   "(y # ys, Y) ∈ futures (P ∥ Q <p, q>) xs ∧
    (zs, Z) ∈ futures (P ∥ Q <p, q>) xs"
  hence
   "(ipurge_tr ?I' ?D' (?D' y) ys, ipurge_ref ?I' ?D' (?D' y) ys Y)
      ∈ futures (P ∥ Q <p, q>) xs ∧
    (y # ipurge_tr ?I' ?D' (?D' y) zs, ipurge_ref ?I' ?D' (?D' y) zs Z)
      ∈ futures (P ∥ Q <p, q>) xs"
   by blast
  thus
   "(ipurge_tr I (the ∘ ?D') (the (?D' y)) ys,
      ipurge_ref I (the ∘ ?D') (the (?D' y)) ys Y) ∈ futures (P ∥ Q <p, q>) xs ∧
    (y # ipurge_tr I (the ∘ ?D') (the (?D' y)) zs,
      ipurge_ref I (the ∘ ?D') (the (?D' y)) zs Z) ∈ futures (P ∥ Q <p, q>) xs"
   by (simp add: con_comp_ipurge_tr_no_fake [OF A E]
    con_comp_ipurge_ref_no_fake [OF A E])
qed

end