Theory SequentialComposition
section "Sequential composition and noninterference security"
theory SequentialComposition
imports Propaedeutics
begin
text ‹
\null
This section formalizes the definitions of sequential processes and sequential composition given in
\<^cite>‹"R4"›, and then proves that under the assumptions discussed above, noninterference security is
conserved under sequential composition for any pair of processes sharing an alphabet that contains
successful termination. Finally, this result is generalized to an arbitrary list of processes.
›
subsection "Sequential processes"
text ‹
In \<^cite>‹"R4"›, a \emph{sequential process} is defined as a process whose alphabet contains successful
termination. Since sequential composition applies to sequential processes, the first problem put by
the formalization of this operation is that of finding a suitable way to represent such a process.
A simple but effective strategy is to identify it with a process having alphabet @{typ "'a option"},
where @{typ 'a} is the native type of its ordinary (i.e. distinct from termination) events. Then,
ordinary events will be those matching pattern ‹Some _›, whereas successful termination will
be denoted by the special event @{term None}. This means that the \emph{sentences} of a sequential
process, defined in \<^cite>‹"R4"› as the traces after which the process can terminate successfully, will
be nothing but the event lists @{term xs} such that @{term "xs @ [None]"} is a trace (which implies
that @{term xs} is a trace as well).
Once a suitable representation of successful termination has been found, the next step is to
formalize the properties of sequential processes related to this event, expressing them in terms of
the selected representation. The first of the resulting predicates, ‹weakly_sequential›, is
the minimum required for allowing the identification of event @{term None} with successful
termination, namely that @{term None} may occur in a trace as its last event only. The second
predicate, ‹sequential›, following what Hoare does in \<^cite>‹"R4"›, extends the first predicate
with an additional requirement, namely that whenever the process can engage in event @{term None},
it cannot engage in any other event. A simple counterexample shows that this requirement does not
imply the first one: a process whose traces are @{term "{[], [None], [None, None]}"} satisfies the
second requirement, but not the first one.
Moreover, here below is the definition of a further predicate, ‹secure_termination›, which
applies to a security policy rather than to a process, and is satisfied just in case the policy does
not allow event @{term None} to be affected by confidential events, viz. by ordinary events not
allowed to affect some event in the alphabet. Interestingly, this property, which will prove to be
necessary for the target theorem to hold, is nothing but the CSP counterpart of a condition required
for a security type system to enforce termination-sensitive noninterference security of programs,
namely that program termination must not depend on confidential data (cf. \<^cite>‹"R5"›, section 9.2.6).
\null
›
definition sentences :: "'a option process ⇒ 'a option list set" where
"sentences P ≡ {xs. xs @ [None] ∈ traces P}"
definition weakly_sequential :: "'a option process ⇒ bool" where
"weakly_sequential P ≡
∀xs ∈ traces P. None ∉ set (butlast xs)"
definition sequential :: "'a option process ⇒ bool" where
"sequential P ≡
(∀xs ∈ traces P. None ∉ set (butlast xs)) ∧
(∀xs ∈ sentences P. next_events P xs = {None})"
definition secure_termination :: "('d × 'd) set ⇒ ('a option ⇒ 'd) ⇒ bool" where
"secure_termination I D ≡
∀x. (D x, D None) ∈ I ∧ x ≠ None ⟶ (∀u ∈ range D. (D x, u) ∈ I)"
text ‹
\null
Here below is the proof of some useful lemmas involving the constants just defined. Particularly, it
is proven that process sequentiality is indeed stronger than weak sequentiality, and a sentence of a
refusals union closed (cf. \<^cite>‹"R3"›), sequential process admits the set of all the ordinary events
of the process as a refusal. The use of the latter lemma in the proof of the target security
conservation theorem is the reason why the theorem requires to assume that the first of the
processes to be composed be refusals union closed (cf. below).
\null
›
lemma seq_implies_weakly_seq:
"sequential P ⟹ weakly_sequential P"
by (simp add: weakly_sequential_def sequential_def)
lemma weakly_seq_sentences_none:
assumes
WS: "weakly_sequential P" and
A: "xs ∈ sentences P"
shows "None ∉ set xs"
proof -
have "∀xs ∈ traces P. None ∉ set (butlast xs)"
using WS by (simp add: weakly_sequential_def)
moreover have "xs @ [None] ∈ traces P"
using A by (simp add: sentences_def)
ultimately have "None ∉ set (butlast (xs @ [None]))" ..
thus ?thesis
by simp
qed
lemma seq_sentences_none:
assumes
S: "sequential P" and
A: "xs ∈ sentences P" and
B: "xs @ y # ys ∈ traces P"
shows "y = None"
proof -
have "∀xs ∈ sentences P. next_events P xs = {None}"
using S by (simp add: sequential_def)
hence "next_events P xs = {None}"
using A ..
moreover have "(xs @ [y]) @ ys ∈ traces P"
using B by simp
hence "xs @ [y] ∈ traces P"
by (rule process_rule_2_traces)
hence "y ∈ next_events P xs"
by (simp add: next_events_def)
ultimately show ?thesis
by simp
qed
lemma seq_sentences_ref:
assumes
A: "ref_union_closed P" and
B: "sequential P" and
C: "xs ∈ sentences P"
shows "(xs, {x. x ≠ None}) ∈ failures P"
(is "(_, ?X) ∈ _")
proof -
have "(∃X. X ∈ singleton_set ?X) ⟶
(∀X ∈ singleton_set ?X. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P"
using A by (simp add: ref_union_closed_def)
moreover have "∃x. x ∈ ?X"
by blast
hence "∃X. X ∈ singleton_set ?X"
by (simp add: singleton_set_some)
ultimately have "(∀X ∈ singleton_set ?X. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P" ..
moreover have "∀X ∈ singleton_set ?X. (xs, X) ∈ failures P"
proof (rule ballI, simp add: singleton_set_def del: not_None_eq,
erule exE, erule conjE, simp (no_asm_simp))
fix x :: "'a option"
assume D: "x ≠ None"
have "xs @ [None] ∈ traces P"
using C by (simp add: sentences_def)
hence "xs ∈ traces P"
by (rule process_rule_2_traces)
hence "(xs, {}) ∈ failures P"
by (rule traces_failures)
hence "(xs @ [x], {}) ∈ failures P ∨ (xs, {x}) ∈ failures P"
by (rule process_rule_4)
thus "(xs, {x}) ∈ failures P"
proof (rule disjE, rule_tac ccontr, simp_all)
assume "(xs @ [x], {}) ∈ failures P"
hence "xs @ [x] ∈ traces P"
by (rule failures_traces)
with B and C have "x = None"
by (rule seq_sentences_none)
thus False
using D by contradiction
qed
qed
ultimately have "(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P" ..
thus ?thesis
by (simp only: singleton_set_union)
qed
subsection "Sequential composition"
text ‹
In what follows, the definition of the failures resulting from the sequential composition of two
processes @{term P}, @{term Q} given in \<^cite>‹"R4"› is formalized as the inductive definition of set
‹seq_comp_failures P Q›. Then, the sequential composition of @{term P} and @{term Q},
denoted by means of notation ‹P ; Q› following \<^cite>‹"R4"›, is defined as the process having
‹seq_comp_failures P Q› as failures set and the empty set as divergences set.
For the sake of generality, this definition is based on the mere implicit assumption that the input
processes be weakly sequential, rather than sequential. This slightly complicates things, since the
sentences of process @{term P} may number further events in addition to @{term None} in their
future.
Therefore, the resulting refusals of a sentence @{term xs} of @{term P} will have the form
@{term "insert None X ∩ Y"}, where @{term X} is a refusal of @{term xs} in @{term P} and @{term Y}
is an initial refusal of @{term Q} (cf. rule ‹SCF_R2›). In fact, after @{term xs}, process
‹P ; Q› must be able to refuse @{term None} if @{term Q} is, whereas it cannot refuse an
ordinary event unless both @{term P} and @{term Q}, in their respective states, can.
Moreover, a trace @{term xs} of ‹P ; Q› may result from different combinations of a sentence
of @{term P} with a trace of @{term Q}. Thus, in order that the refusals of ‹P ; Q› be
closed under set union, the union of any two refusals of @{term xs} must still be a refusal (cf.
rule ‹SCF_R4›). Indeed, this property will prove to be sufficient to ensure that for any two
processes whose refusals are closed under set union, their sequential composition still be such,
which is what is expected for any process of practical significance (cf. \<^cite>‹"R3"›).
According to the definition given in \<^cite>‹"R4"›, a divergence of ‹P ; Q› is either a
divergence of @{term P}, or the concatenation of a sentence of @{term P} with a divergence of
@{term Q}. Apparently, this definition does not match the formal one stated here below, which
identifies the divergences set of ‹P ; Q› with the empty set. Nonetheless, as remarked
above, sequential composition does not make sense unless the input processes are weakly sequential,
since this is the minimum required to confer the meaning of successful termination on the
corresponding alphabet symbol. But a weakly sequential process cannot have any divergence, so that
the two definitions are actually equivalent. In fact, a divergence is a trace such that, however it
is extended with arbitrary additional events, the resulting event list is still a trace (cf. process
properties @{term process_prop_5} and @{term process_prop_6} in \<^cite>‹"R2"›). Therefore, if @{term xs}
were a divergence, then @{term "xs @ [None, None]"} would be a trace, which is impossible in case
the process satisfies predicate @{term weakly_sequential}.
\null
›
inductive_set seq_comp_failures ::
"'a option process ⇒ 'a option process ⇒ 'a option failure set"
for P :: "'a option process" and Q :: "'a option process" where
SCF_R1: "⟦xs ∉ sentences P; (xs, X) ∈ failures P; None ∉ set xs⟧ ⟹
(xs, X) ∈ seq_comp_failures P Q" |
SCF_R2: "⟦xs ∈ sentences P; (xs, X) ∈ failures P; ([], Y) ∈ failures Q⟧ ⟹
(xs, insert None X ∩ Y) ∈ seq_comp_failures P Q" |
SCF_R3: "⟦xs ∈ sentences P; (ys, Y) ∈ failures Q; ys ≠ []⟧ ⟹
(xs @ ys, Y) ∈ seq_comp_failures P Q" |
SCF_R4: "⟦(xs, X) ∈ seq_comp_failures P Q; (xs, Y) ∈ seq_comp_failures P Q⟧ ⟹
(xs, X ∪ Y) ∈ seq_comp_failures P Q"
definition seq_comp ::
"'a option process ⇒ 'a option process ⇒ 'a option process" (infixl ";" 60)
where
"P ; Q ≡ Abs_process (seq_comp_failures P Q, {})"
text ‹
\null
Here below is the proof that, for any two processes @{term P}, @{term Q} defined over the same
alphabet containing successful termination, set @{term "seq_comp_failures P Q"} indeed enjoys the
characteristic properties of the failures set of a process as defined in \<^cite>‹"R2"› provided that
@{term P} is weakly sequential, which is what happens in any meaningful case.
\null
›
lemma seq_comp_prop_1:
"([], {}) ∈ seq_comp_failures P Q"
proof (cases "[] ∈ sentences P")
case False
moreover have "([], {}) ∈ failures P"
by (rule process_rule_1)
moreover have "None ∉ set []"
by simp
ultimately show ?thesis
by (rule SCF_R1)
next
case True
moreover have "([], {}) ∈ failures P"
by (rule process_rule_1)
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "([], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
lemma seq_comp_prop_2_aux [rule_format]:
assumes WS: "weakly_sequential P"
shows "(ws, X) ∈ seq_comp_failures P Q ⟹
ws = xs @ [x] ⟶ (xs, {}) ∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, rule_tac [!] impI, simp_all, erule conjE)
fix X'
assume
A: "(xs @ [x], X') ∈ failures P" and
B: "None ∉ set xs"
have A': "(xs, {}) ∈ failures P"
using A by (rule process_rule_2)
show "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "xs ∈ sentences P")
case False
thus ?thesis
using A' and B by (rule SCF_R1)
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and A' have "(xs, {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
fix X'
assume A: "(xs @ [x], X') ∈ failures P"
hence A': "(xs, {}) ∈ failures P"
by (rule process_rule_2)
show "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "xs ∈ sentences P")
case False
have "∀xs ∈ traces P. None ∉ set (butlast xs)"
using WS by (simp add: weakly_sequential_def)
moreover have "xs @ [x] ∈ traces P"
using A by (rule failures_traces)
ultimately have "None ∉ set (butlast (xs @ [x]))" ..
hence "None ∉ set xs" by simp
with False and A' show ?thesis
by (rule SCF_R1)
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and A' have "(xs, {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
fix xs' ys Y
assume
A: "xs' @ ys = xs @ [x]" and
B: "xs' ∈ sentences P" and
C: "(ys, Y) ∈ failures Q" and
D: "ys ≠ []"
have "∃y ys'. ys = ys' @ [y]"
using D by (rule_tac xs = ys in rev_cases, simp_all)
then obtain y and ys' where D': "ys = ys' @ [y]"
by blast
hence "xs = xs' @ ys'"
using A by simp
thus "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "ys' = []", simp_all)
case True
have "xs' @ [None] ∈ traces P"
using B by (simp add: sentences_def)
hence "xs' ∈ traces P"
by (rule process_rule_2_traces)
hence "(xs', {}) ∈ failures P"
by (rule traces_failures)
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "(xs', {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2 [OF B])
thus "(xs', {}) ∈ seq_comp_failures P Q"
by simp
next
case False
have "(ys' @ [y], Y) ∈ failures Q"
using C and D' by simp
hence C': "(ys', {}) ∈ failures Q"
by (rule process_rule_2)
with B show "(xs' @ ys', {}) ∈ seq_comp_failures P Q"
using False by (rule SCF_R3)
qed
qed
lemma seq_comp_prop_2:
assumes WS: "weakly_sequential P"
shows "(xs @ [x], X) ∈ seq_comp_failures P Q ⟹
(xs, {}) ∈ seq_comp_failures P Q"
by (erule seq_comp_prop_2_aux [OF WS], simp)
lemma seq_comp_prop_3 [rule_format]:
"(xs, Y) ∈ seq_comp_failures P Q ⟹ X ⊆ Y ⟶
(xs, X) ∈ seq_comp_failures P Q"
proof (induction arbitrary: X rule: seq_comp_failures.induct, rule_tac [!] impI)
fix xs X Y
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs" and
D: "Y ⊆ X"
have "(xs, Y) ∈ failures P"
using B and D by (rule process_rule_3)
with A show "(xs, Y) ∈ seq_comp_failures P Q"
using C by (rule SCF_R1)
next
fix xs X Y Z
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q" and
D: "Z ⊆ insert None X ∩ Y"
have "Z - {None} ⊆ X"
using D by blast
with B have "(xs, Z - {None}) ∈ failures P"
by (rule process_rule_3)
moreover have "Z ⊆ Y"
using D by simp
with C have "([], Z) ∈ failures Q"
by (rule process_rule_3)
ultimately have "(xs, insert None (Z - {None}) ∩ Z) ∈ seq_comp_failures P Q"
by (rule SCF_R2 [OF A])
moreover have "insert None (Z - {None}) ∩ Z = Z"
by blast
ultimately show "(xs, Z) ∈ seq_comp_failures P Q"
by simp
next
fix xs ys X Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []" and
D: "X ⊆ Y"
have "(ys, X) ∈ failures Q"
using B and D by (rule process_rule_3)
with A show "(xs @ ys, X) ∈ seq_comp_failures P Q"
using C by (rule SCF_R3)
next
fix xs X Y Z
assume
A: "⋀W. W ⊆ X ⟶ (xs, W) ∈ seq_comp_failures P Q" and
B: "⋀W. W ⊆ Y ⟶ (xs, W) ∈ seq_comp_failures P Q" and
C: "Z ⊆ X ∪ Y"
have "Z ∩ X ⊆ X ⟶ (xs, Z ∩ X) ∈ seq_comp_failures P Q"
using A .
hence "(xs, Z ∩ X) ∈ seq_comp_failures P Q"
by simp
moreover have "Z ∩ Y ⊆ Y ⟶ (xs, Z ∩ Y) ∈ seq_comp_failures P Q"
using B .
hence "(xs, Z ∩ Y) ∈ seq_comp_failures P Q"
by simp
ultimately have "(xs, Z ∩ X ∪ Z ∩ Y) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
hence "(xs, Z ∩ (X ∪ Y)) ∈ seq_comp_failures P Q"
by (simp add: Int_Un_distrib)
moreover have "Z ∩ (X ∪ Y) = Z"
using C by (rule Int_absorb2)
ultimately show "(xs, Z) ∈ seq_comp_failures P Q"
by simp
qed
lemma seq_comp_prop_4:
assumes WS: "weakly_sequential P"
shows "(xs, X) ∈ seq_comp_failures P Q ⟹
(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, simp_all)
fix xs X
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs"
have "(xs @ [x], {}) ∈ failures P ∨
(xs, insert x X) ∈ failures P"
using B by (rule process_rule_4)
thus "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q"
proof
assume D: "(xs @ [x], {}) ∈ failures P"
show ?thesis
proof (cases "xs @ [x] ∈ sentences P")
case False
have "None ∉ set (xs @ [x])"
proof (simp add: C, rule notI)
assume "None = x"
hence "(xs @ [None], {}) ∈ failures P"
using D by simp
hence "xs @ [None] ∈ traces P"
by (rule failures_traces)
hence "xs ∈ sentences P"
by (simp add: sentences_def)
thus False
using A by contradiction
qed
with False and D have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R1)
thus ?thesis ..
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and D have "(xs @ [x], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
assume "(xs, insert x X) ∈ failures P"
with A have "(xs, insert x X) ∈ seq_comp_failures P Q"
using C by (rule SCF_R1)
thus ?thesis ..
qed
next
fix xs X Y
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q"
show "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof (cases "x = None", simp)
case True
have "([] @ [None], {}) ∈ failures Q ∨ ([], insert None Y) ∈ failures Q"
using C by (rule process_rule_4)
thus "(xs @ [None], {}) ∈ seq_comp_failures P Q ∨
(xs, insert None (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof (rule disjE, simp)
assume "([None], {}) ∈ failures Q"
moreover have "[None] ≠ []"
by simp
ultimately have "(xs @ [None], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "([], insert None Y) ∈ failures Q"
with A and B have "(xs, insert None X ∩ insert None Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have "insert None X ∩ insert None Y =
insert None (insert None X ∩ Y)"
by blast
ultimately have "(xs, insert None (insert None X ∩ Y))
∈ seq_comp_failures P Q"
by simp
thus ?thesis ..
qed
next
case False
have "(xs @ [x], {}) ∈ failures P ∨ (xs, insert x X) ∈ failures P"
using B by (rule process_rule_4)
thus ?thesis
proof (rule disjE, cases "xs @ [x] ∈ sentences P")
assume
D: "xs @ [x] ∉ sentences P" and
E: "(xs @ [x], {}) ∈ failures P"
have "None ∉ set xs"
using WS and A by (rule weakly_seq_sentences_none)
hence "None ∉ set (xs @ [x])"
using False by (simp del: not_None_eq)
with D and E have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R1)
thus ?thesis ..
next
assume
"xs @ [x] ∈ sentences P" and
"(xs @ [x], {}) ∈ failures P"
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "(xs @ [x], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
next
assume D: "(xs, insert x X) ∈ failures P"
have "([] @ [x], {}) ∈ failures Q ∨ ([], insert x Y) ∈ failures Q"
using C by (rule process_rule_4)
thus ?thesis
proof (rule disjE, simp)
assume "([x], {}) ∈ failures Q"
moreover have "[x] ≠ []"
by simp
ultimately have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "([], insert x Y) ∈ failures Q"
with A and D have "(xs, insert None (insert x X) ∩ insert x Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have "insert None (insert x X) ∩ insert x Y =
insert x (insert None X ∩ Y)"
by blast
ultimately have "(xs, insert x (insert None X ∩ Y))
∈ seq_comp_failures P Q"
by simp
thus ?thesis ..
qed
qed
qed
next
fix xs ys Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []"
have "(ys @ [x], {}) ∈ failures Q ∨ (ys, insert x Y) ∈ failures Q"
using B by (rule process_rule_4)
thus "(xs @ ys @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs @ ys, insert x Y) ∈ seq_comp_failures P Q"
proof
assume "(ys @ [x], {}) ∈ failures Q"
moreover have "ys @ [x] ≠ []"
by simp
ultimately have "(xs @ ys @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "(ys, insert x Y) ∈ failures Q"
with A have "(xs @ ys, insert x Y) ∈ seq_comp_failures P Q"
using C by (rule SCF_R3)
thus ?thesis ..
qed
next
fix xs X Y
assume
"(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q" and
"(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x Y) ∈ seq_comp_failures P Q"
thus "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x (X ∪ Y)) ∈ seq_comp_failures P Q"
proof (cases "(xs @ [x], {}) ∈ seq_comp_failures P Q", simp_all)
assume
"(xs, insert x X) ∈ seq_comp_failures P Q" and
"(xs, insert x Y) ∈ seq_comp_failures P Q"
hence "(xs, insert x X ∪ insert x Y) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs, insert x (X ∪ Y)) ∈ seq_comp_failures P Q"
by simp
qed
qed
lemma seq_comp_rep:
assumes WS: "weakly_sequential P"
shows "Rep_process (P ; Q) = (seq_comp_failures P Q, {})"
proof (subst seq_comp_def, rule Abs_process_inverse, simp add: process_set_def,
(subst conj_assoc [symmetric])+, (rule conjI)+)
show "process_prop_1 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_1_def)
qed (rule seq_comp_prop_1)
next
show "process_prop_2 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_2_def del: all_simps, (rule allI)+, rule impI)
qed (rule seq_comp_prop_2 [OF WS])
next
show "process_prop_3 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_3_def del: all_simps, (rule allI)+, rule impI,
erule conjE)
qed (rule seq_comp_prop_3)
next
show "process_prop_4 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_4_def, (rule allI)+, rule impI)
qed (rule seq_comp_prop_4 [OF WS])
next
show "process_prop_5 (seq_comp_failures P Q, {})"
by (simp add: process_prop_5_def)
next
show "process_prop_6 (seq_comp_failures P Q, {})"
by (simp add: process_prop_6_def)
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>‹"R2"› and \<^cite>‹"R3"›, when acting on
the sequential composition of a pair of processes.
\null
›
lemma seq_comp_failures:
"weakly_sequential P ⟹
failures (P ; Q) = seq_comp_failures P Q"
by (drule seq_comp_rep [where Q = Q], simp add: failures_def)
lemma seq_comp_divergences:
"weakly_sequential P ⟹
divergences (P ; Q) = {}"
by (drule seq_comp_rep [where Q = Q], simp add: divergences_def)
lemma seq_comp_futures:
"weakly_sequential P ⟹
futures (P ; Q) xs = {(ys, Y). (xs @ ys, Y) ∈ seq_comp_failures P Q}"
by (simp add: futures_def seq_comp_failures)
lemma seq_comp_traces:
"weakly_sequential P ⟹
traces (P ; Q) = Domain (seq_comp_failures P Q)"
by (simp add: traces_def seq_comp_failures)
lemma seq_comp_refusals:
"weakly_sequential P ⟹
refusals (P ; Q) xs ≡ seq_comp_failures P Q `` {xs}"
by (simp add: refusals_def seq_comp_failures)
lemma seq_comp_next_events:
"weakly_sequential P ⟹
next_events (P ; Q) xs = {x. xs @ [x] ∈ Domain (seq_comp_failures P Q)}"
by (simp add: next_events_def seq_comp_traces)
subsection "Conservation of refusals union closure and sequentiality under sequential composition"
text ‹
Here below is the proof that, for any two processes @{term P}, @{term Q} and any failure
@{term "(xs, X)"} of @{term "P ; Q"}, the refusal @{term X} is the union of a set of refusals where,
for any such refusal @{term W}, @{term "(xs, W)"} is a failure of @{term "P ; Q"} by virtue of one
of rules ‹SCF_R1›, ‹SCF_R2›, or ‹SCF_R3›.
The converse is also proven, under the assumption that the refusals of both @{term P} and @{term Q}
be closed under union: namely, for any trace @{term xs} of @{term "P ; Q"} and any set of refusals
where, for any such refusal @{term W}, @{term "(xs, W)"} is a failure of the aforesaid kind, the
union of these refusals is still a refusal of @{term xs}.
The proof of the latter lemma makes use of the axiom of choice.
\null
›
lemma seq_comp_refusals_1:
"(xs, X) ∈ seq_comp_failures P Q ⟹ ∃R.
X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q) ∧
(∃n ∈ {..length xs}. ∃W. W ∈ R n)"
(is "_ ⟹ ∃R. ?T R xs X")
proof (erule seq_comp_failures.induct, (erule_tac [4] exE)+)
fix xs X
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs"
show "∃R. ?T R xs X"
proof (rule_tac x = "λn. if n = 0 then {X} else {}" in exI,
simp add: A B C, rule equalityI, rule_tac [!] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs}.
∃W ∈ if n = 0 then {X} else {}. x ∈ W"
thus "x ∈ X"
by (simp split: if_split_asm)
qed
next
fix xs X Y
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q"
show "∃R. ?T R xs (insert None X ∩ Y)"
proof (rule_tac x = "λn. if n = 0 then {insert None X ∩ Y} else {}" in exI,
simp add: A, rule conjI, rule equalityI, rule_tac [1-2] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs}.
∃W ∈ if n = 0 then {insert None X ∩ Y} else {}. x ∈ W"
thus "(x = None ∨ x ∈ X) ∧ x ∈ Y"
by (simp split: if_split_asm)
next
show "∃U. (xs, U) ∈ failures P ∧ (∃V. ([], V) ∈ failures Q ∧
insert None X ∩ Y = insert None U ∩ V)"
proof (rule_tac x = X in exI, rule conjI, simp add: B)
qed (rule_tac x = Y in exI, rule conjI, simp_all add: C)
qed
next
fix xs ys Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []"
show "∃R. ?T R (xs @ ys) Y"
proof (rule_tac x = "λn. if n = length ys then {Y} else {}" in exI,
simp add: A B C, rule equalityI, rule_tac [!] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs + length ys}.
∃W ∈ if n = length ys then {Y} else {}. x ∈ W"
thus "x ∈ Y"
by (simp split: if_split_asm)
qed
next
fix xs X Y Rx Ry
assume
A: "?T Rx xs X" and
B: "?T Ry xs Y"
show "∃R. ?T R xs (X ∪ Y)"
proof (rule_tac x = "λn. Rx n ∪ Ry n" in exI, rule conjI, rule_tac [2] conjI,
rule_tac [3] conjI, rule_tac [2] ballI, (rule_tac [3] ballI)+)
have "X ∪ Y = (⋃n ≤ length xs. ⋃W ∈ Rx n. W) ∪
(⋃n ≤ length xs. ⋃W ∈ Ry n. W)"
using A and B by simp
also have "… = (⋃n ≤ length xs. (⋃W ∈ Rx n. W) ∪ (⋃W ∈ Ry n. W))"
by blast
also have "… = (⋃n ≤ length xs. ⋃W ∈ Rx n ∪ Ry n. W)"
by simp
finally show "X ∪ Y = (⋃n ≤ length xs. ⋃W ∈ Rx n ∪ Ry n. W)" .
next
fix W
assume "W ∈ Rx 0 ∪ Ry 0"
thus
"xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "?T' W")
proof
have "∀W ∈ Rx 0. ?T' W"
using A by simp
moreover assume "W ∈ Rx 0"
ultimately show ?thesis ..
next
have "∀W ∈ Ry 0. ?T' W"
using B by simp
moreover assume "W ∈ Ry 0"
ultimately show ?thesis ..
qed
next
fix n W
assume C: "n ∈ {0<..length xs}"
assume "W ∈ Rx n ∪ Ry n"
thus
"take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
(is "?T' n W")
proof
have "∀n ∈ {0<..length xs}. ∀W ∈ Rx n. ?T' n W"
using A by simp
hence "∀W ∈ Rx n. ?T' n W"
using C ..
moreover assume "W ∈ Rx n"
ultimately show ?thesis ..
next
have "∀n ∈ {0<..length xs}. ∀W ∈ Ry n. ?T' n W"
using B by simp
hence "∀W ∈ Ry n. ?T' n W"
using C ..
moreover assume "W ∈ Ry n"
ultimately show ?thesis ..
qed
next
have "∃n ∈ {..length xs}. ∃W. W ∈ Rx n"
using A by simp
then obtain n where C: "n ∈ {..length xs}" and D: "∃W. W ∈ Rx n" ..
obtain W where "W ∈ Rx n"
using D ..
hence "W ∈ Rx n ∪ Ry n" ..
hence "∃W. W ∈ Rx n ∪ Ry n" ..
thus "∃n ∈ {..length xs}. ∃W. W ∈ Rx n ∪ Ry n"
using C ..
qed
qed
lemma seq_comp_refusals_finite [rule_format]:
assumes A: "xs ∈ Domain (seq_comp_failures P Q)"
shows "finite A ⟹ (∀x ∈ A. (xs, F x) ∈ seq_comp_failures P Q) ⟶
(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
proof (erule finite_induct, simp, rule_tac [2] impI)
have "∃X. (xs, X) ∈ seq_comp_failures P Q"
using A by (simp add: Domain_iff)
then obtain X where "(xs, X) ∈ seq_comp_failures P Q" ..
moreover have "{} ⊆ X" ..
ultimately show "(xs, {}) ∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
next
fix x' A
assume B: "∀x ∈ insert x' A. (xs, F x) ∈ seq_comp_failures P Q"
hence "(xs, F x') ∈ seq_comp_failures P Q"
by simp
moreover assume "(∀x ∈ A. (xs, F x) ∈ seq_comp_failures P Q) ⟶
(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
hence "(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
using B by simp
ultimately have "(xs, F x' ∪ (⋃x ∈ A. F x)) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs, ⋃x ∈ insert x' A. F x) ∈ seq_comp_failures P Q"
by simp
qed
lemma seq_comp_refusals_2:
assumes
A: "ref_union_closed P" and
B: "ref_union_closed Q" and
C: "xs ∈ Domain (seq_comp_failures P Q)" and
D: "X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q)"
shows "(xs, X) ∈ seq_comp_failures P Q"
proof -
have "∃Y. (xs, Y) ∈ seq_comp_failures P Q"
using C by (simp add: Domain_iff)
then obtain Y where "(xs, Y) ∈ seq_comp_failures P Q" ..
moreover have "{} ⊆ Y" ..
ultimately have E: "(xs, {}) ∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
have "(xs, ⋃W ∈ R 0. W) ∈ seq_comp_failures P Q"
proof (cases "∃W. W ∈ R 0", cases "xs ∈ sentences P")
assume "¬ (∃W. W ∈ R 0)"
thus ?thesis
using E by simp
next
assume
F: "∃W. W ∈ R 0" and
G: "xs ∉ sentences P"
have H: "∀W ∈ R 0. None ∉ set xs ∧ (xs, W) ∈ failures P"
using D and G by simp
show ?thesis
proof (rule SCF_R1 [OF G])
have "∀xs A. (∃W. W ∈ A) ⟶ (∀W ∈ A. (xs, W) ∈ failures P) ⟶
(xs, ⋃W ∈ A. W) ∈ failures P"
using A by (simp add: ref_union_closed_def)
hence "(∃W. W ∈ R 0) ⟶ (∀W ∈ R 0. (xs, W) ∈ failures P) ⟶
(xs, ⋃W ∈ R 0. W) ∈ failures P"
by blast
thus "(xs, ⋃W ∈ R 0. W) ∈ failures P"
using F and H by simp
next
obtain W where "W ∈ R 0" using F ..
thus "None ∉ set xs"
using H by simp
qed
next
assume
F: "∃W. W ∈ R 0" and
G: "xs ∈ sentences P"
have "∀W ∈ R 0. ∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V"
using D and G by simp
hence "∃F. ∀W ∈ R 0. ∃V. (xs, F W) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None (F W) ∩ V"
by (rule bchoice)
then obtain F where "∀W ∈ R 0.
∃V. (xs, F W) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None (F W) ∩ V" ..
hence "∃G. ∀W ∈ R 0. (xs, F W) ∈ failures P ∧ ([], G W) ∈ failures Q ∧
W = insert None (F W) ∩ G W"
by (rule bchoice)
then obtain G where H: "∀W ∈ R 0.
(xs, F W) ∈ failures P ∧ ([], G W) ∈ failures Q ∧
W = insert None (F W) ∩ G W" ..
have "(xs, insert None (⋃W ∈ R 0. F W) ∩ (⋃W ∈ R 0. G W))
∈ seq_comp_failures P Q"
(is "(_, ?S) ∈ _")
proof (rule SCF_R2 [OF G])
have "∀xs A. (∃X. X ∈ A) ⟶ (∀X ∈ A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ A. X) ∈ failures P"
using A by (simp add: ref_union_closed_def)
hence "(∃X. X ∈ F ` R 0) ⟶ (∀X ∈ F ` R 0. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ F ` R 0. X) ∈ failures P"
(is "?A ⟶ ?B ⟶ ?C")
by (erule_tac x = xs in allE, erule_tac x = "F ` R 0" in allE)
moreover obtain W where "W ∈ R 0" using F ..
hence ?A
proof (simp add: image_def, rule_tac x = "F W" in exI)
qed (rule bexI, simp)
ultimately have "?B ⟶ ?C" ..
moreover have ?B
proof (rule ballI, simp add: image_def, erule bexE)
fix W X
assume "W ∈ R 0"
hence "(xs, F W) ∈ failures P"
using H by simp
moreover assume "X = F W"
ultimately show "(xs, X) ∈ failures P"
by simp
qed
ultimately have ?C ..
thus "(xs, ⋃W ∈ R 0. F W) ∈ failures P"
by simp
next
have "∀xs A. (∃Y. Y ∈ A) ⟶ (∀Y ∈ A. (xs, Y) ∈ failures Q) ⟶
(xs, ⋃Y ∈ A. Y) ∈ failures Q"
using B by (simp add: ref_union_closed_def)
hence "(∃Y. Y ∈ G ` R 0) ⟶ (∀Y ∈ G ` R 0. ([], Y) ∈ failures Q) ⟶
([], ⋃Y ∈ G ` R 0. Y) ∈ failures Q"
(is "?A ⟶ ?B ⟶ ?C")
by (erule_tac x = "[]" in allE, erule_tac x = "G ` R 0" in allE)
moreover obtain W where "W ∈ R 0" using F ..
hence ?A
proof (simp add: image_def, rule_tac x = "G W" in exI)
qed (rule bexI, simp)
ultimately have "?B ⟶ ?C" ..
moreover have ?B
proof (rule ballI, simp add: image_def, erule bexE)
fix W Y
assume "W ∈ R 0"
hence "([], G W) ∈ failures Q"
using H by simp
moreover assume "Y = G W"
ultimately show "([], Y) ∈ failures Q"
by simp
qed
ultimately have ?C ..
thus "([], ⋃W ∈ R 0. G W) ∈ failures Q"
by simp
qed
moreover have "(⋃W ∈ R 0. W) ⊆ ?S"
proof (rule subsetI, simp, erule bexE)
fix x W
assume I: "W ∈ R 0"
hence "W = insert None (F W) ∩ G W"
using H by simp
moreover assume "x ∈ W"
ultimately have "x ∈ insert None (F W) ∩ G W"
by simp
thus "(x = None ∨ (∃W ∈ R 0. x ∈ F W)) ∧ (∃W ∈ R 0. x ∈ G W)"
(is "?A ∧ ?B")
proof (rule IntE, simp)
assume "x = None ∨ x ∈ F W"
moreover {
assume "x = None"
hence ?A ..
}
moreover {
assume "x ∈ F W"
hence "∃W ∈ R 0. x ∈ F W" using I ..
hence ?A ..
}
ultimately have ?A ..
moreover assume "x ∈ G W"
hence ?B using I ..
ultimately show ?thesis ..
qed
qed
ultimately show ?thesis
by (rule seq_comp_prop_3)
qed
moreover have "∀n ∈ {0<..length xs}.
(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof
fix n
assume F: "n ∈ {0<..length xs}"
hence G: "∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
using D by simp
show "(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof (cases "∃W. W ∈ R n")
case False
thus ?thesis
using E by simp
next
case True
have "(take (length xs - n) xs @ drop (length xs - n) xs, ⋃W ∈ R n. W)
∈ seq_comp_failures P Q"
proof (rule SCF_R3)
obtain W where "W ∈ R n" using True ..
thus "take (length xs - n) xs ∈ sentences P"
using G by simp
next
have "∀xs A. (∃W. W ∈ A) ⟶ (∀W ∈ A. (xs, W) ∈ failures Q) ⟶
(xs, ⋃W ∈ A. W) ∈ failures Q"
using B by (simp add: ref_union_closed_def)
hence "(∃W. W ∈ R n) ⟶
(∀W ∈ R n. (drop (length xs - n) xs, W) ∈ failures Q) ⟶
(drop (length xs - n) xs, ⋃W ∈ R n. W) ∈ failures Q"
by blast
thus "(drop (length xs - n) xs, ⋃W ∈ R n. W) ∈ failures Q"
using G and True by simp
next
show "drop (length xs - n) xs ≠ []"
using F by (simp, arith)
qed
thus ?thesis
by simp
qed
qed
ultimately have F: "∀n ∈ {..length xs}.
(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
by auto
have "(xs, ⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof (rule seq_comp_refusals_finite [OF C], simp)
fix n
assume "n ∈ {..length xs}"
with F show "(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q" ..
qed
moreover have "X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W)"
using D by simp
ultimately show ?thesis
by simp
qed
text ‹
\null
In what follows, the previous results are used to prove that refusals union closure, weak
sequentiality, and sequentiality are conserved under sequential composition. The proof of the first
of these lemmas makes use of the axiom of choice.
Since the target security conservation theorem, in addition to the security of both of the processes
to be composed, also requires to assume that the first process be refusals union closed and
sequential (cf. below), these further conservation lemmas will permit to generalize the theorem to
the sequential composition of an arbitrary list of processes.
\null
›
lemma seq_comp_ref_union_closed:
assumes
WS: "weakly_sequential P" and
A: "ref_union_closed P" and
B: "ref_union_closed Q"
shows "ref_union_closed (P ; Q)"
proof (simp only: ref_union_closed_def seq_comp_failures [OF WS],
(rule allI)+, (rule impI)+, erule exE)
fix xs A X'
assume
C: "∀X ∈ A. (xs, X) ∈ seq_comp_failures P Q" and
D: "X' ∈ A"
have "∀X ∈ A. ∃R.
X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q)"
(is "∀X ∈ A. ∃R. ?T R X")
proof
fix X
assume "X ∈ A"
with C have "(xs, X) ∈ seq_comp_failures P Q" ..
hence "∃R. X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q) ∧
(∃n ∈ {..length xs}. ∃W. W ∈ R n)"
by (rule seq_comp_refusals_1)
thus "∃R. ?T R X"
by blast
qed
hence "∃R. ∀X ∈ A. ?T (R X) X"
by (rule bchoice)
then obtain R where E: "∀X ∈ A. ?T (R X) X" ..
have "xs ∈ Domain (seq_comp_failures P Q)"
proof (simp add: Domain_iff)
have "(xs, X') ∈ seq_comp_failures P Q"
using C and D ..
thus "∃X. (xs, X) ∈ seq_comp_failures P Q" ..
qed
moreover have "?T (λn. ⋃X ∈ A. R X n) (⋃X ∈ A. X)"
proof (rule conjI, rule_tac [2] conjI)
show "(⋃X ∈ A. X) = (⋃n ∈ {..length xs}. ⋃W ∈ ⋃X ∈ A. R X n. W)"
proof (rule equalityI, rule_tac [!] subsetI, simp_all,
erule bexE, (erule_tac [2] bexE)+)
fix x X
assume F: "X ∈ A"
hence "X = (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
using E by simp
moreover assume "x ∈ X"
ultimately have "x ∈ (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
by simp
hence "∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W"
by simp
hence "∃X ∈ A. ∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W"
using F ..
thus "∃n ∈ {..length xs}. ∃X ∈ A. ∃W ∈ R X n. x ∈ W"
by blast
next
fix x n X W
assume F: "X ∈ A"
hence G: "X = (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
using E by simp
assume "x ∈ W" and "W ∈ R X n"
hence "∃W ∈ R X n. x ∈ W" ..
moreover assume "n ∈ {..length xs}"
ultimately have "∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W" ..
hence "x ∈ (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
by simp
hence "x ∈ X"
by (subst G)
thus "∃X ∈ A. x ∈ X"
using F ..
qed
next
show "∀W ∈ ⋃X ∈ A. R X 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ _. ?T W")
proof (rule ballI, simp only: UN_iff, erule bexE)
fix W X
assume "X ∈ A"
hence "∀W ∈ R X 0. ?T W"
using E by simp
moreover assume "W ∈ R X 0"
ultimately show "?T W" ..
qed
next
show "∀n ∈ {0<..length xs}. ∀W ∈ ⋃X ∈ A. R X n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
(is "∀n ∈ _. ∀W ∈ _. ?T n W")
proof ((rule ballI)+, simp only: UN_iff, erule bexE)
fix n W X
assume "X ∈ A"
hence "∀n ∈ {0<..length xs}. ∀W ∈ R X n. ?T n W"
using E by simp
moreover assume "n ∈ {0<..length xs}"
ultimately have "∀W ∈ R X n. ?T n W" ..
moreover assume "W ∈ R X n"
ultimately show "?T n W" ..
qed
qed
ultimately show "(xs, ⋃X ∈ A. X) ∈ seq_comp_failures P Q"
by (rule seq_comp_refusals_2 [OF A B])
qed
lemma seq_comp_weakly_sequential:
assumes
A: "weakly_sequential P" and
B: "weakly_sequential Q"
shows "weakly_sequential (P ; Q)"
proof (subst weakly_sequential_def, rule ballI, drule traces_failures,
subst (asm) seq_comp_failures [OF A], erule seq_comp_failures.induct, simp_all)
fix xs :: "'a option list"
assume C: "None ∉ set xs"
show "None ∉ set (butlast xs)"
proof
assume "None ∈ set (butlast xs)"
hence "None ∈ set xs"
by (rule in_set_butlastD)
thus False
using C by contradiction
qed
next
fix xs
assume "xs ∈ sentences P"
with A have C: "None ∉ set xs"
by (rule weakly_seq_sentences_none)
show "None ∉ set (butlast xs)"
proof
assume "None ∈ set (butlast xs)"
hence "None ∈ set xs"
by (rule in_set_butlastD)
thus False
using C by contradiction
qed
next
fix xs ys Y
assume "xs ∈ sentences P"
with A have C: "None ∉ set xs"
by (rule weakly_seq_sentences_none)
have "∀xs ∈ traces Q. None ∉ set (butlast xs)"
using B by (simp add: weakly_sequential_def)
moreover assume "(ys, Y) ∈ failures Q"
hence "ys ∈ traces Q"
by (rule failures_traces)
ultimately have "None ∉ set (butlast ys)" ..
hence "None ∉ set (xs @ butlast ys)"
using C by simp
moreover assume "ys ≠ []"
hence "butlast (xs @ ys) = xs @ butlast ys"
by (simp add: butlast_append)
ultimately show "None ∉ set (butlast (xs @ ys))"
by simp
qed
lemma seq_comp_sequential:
assumes
A: "sequential P" and
B: "sequential Q"
shows "sequential (P ; Q)"
proof (subst sequential_def, rule conjI)
have "weakly_sequential P"
using A by (rule seq_implies_weakly_seq)
moreover have "weakly_sequential Q"
using B by (rule seq_implies_weakly_seq)
ultimately have "weakly_sequential (P ; Q)"
by (rule seq_comp_weakly_sequential)
thus "∀xs ∈ traces (P ; Q). None ∉ set (butlast xs)"
by (simp add: weakly_sequential_def)
next
have C: "weakly_sequential P"
using A by (rule seq_implies_weakly_seq)
show "∀xs ∈ sentences (P ; Q). next_events (P ; Q) xs = {None}"
proof (rule ballI, simp add: sentences_def next_events_def, rule equalityI,
rule_tac [!] subsetI, simp_all, (drule traces_failures)+,
simp add: seq_comp_failures [OF C])
fix xs x
assume
D: "(xs @ [None], {}) ∈ seq_comp_failures P Q" and
E: "(xs @ [x], {}) ∈ seq_comp_failures P Q"
have "∃R. {} = (⋃n ∈ {..length (xs @ [None])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [None] ∉ sentences P ∧
None ∉ set (xs @ [None]) ∧ (xs @ [None], W) ∈ failures P ∨
xs @ [None] ∈ sentences P ∧
(∃U V. (xs @ [None], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [None])}. ∀W ∈ R n.
take (length (xs @ [None]) - n) (xs @ [None]) ∈ sentences P ∧
(drop (length (xs @ [None]) - n) (xs @ [None]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [None])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using D by (rule seq_comp_refusals_1)
then obtain R where F: "?T R" ..
hence "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R n"
by simp
moreover have "R 0 = {}"
proof (rule equals0I)
fix W
assume "W ∈ R 0"
hence "xs @ [None] ∈ sentences P"
using F by simp
with C have "None ∉ set (xs @ [None])"
by (rule weakly_seq_sentences_none)
thus False
by simp
qed
ultimately have "∃n ∈ {0<..Suc (length xs)}. ∃W. W ∈ R n"
proof -
assume "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R n"
then obtain n where G: "n ∈ {..Suc (length xs)}" and H: "∃W. W ∈ R n" ..
assume I: "R 0 = {}"
show "∃n ∈ {0<..Suc (length xs)}. ∃W. W ∈ R n"
proof (cases n)
case 0
hence "∃W. W ∈ R 0"
using H by simp
then obtain W where "W ∈ R 0" ..
moreover have "W ∉ R 0"
using I by (rule equals0D)
ultimately show ?thesis
by contradiction
next
case (Suc m)
hence "n ∈ {0<..Suc (length xs)}"
using G by simp
with H show ?thesis ..
qed
qed
then obtain n and W where G: "n ∈ {0<..Suc (length xs)}" and "W ∈ R n"
by blast
hence
"take (Suc (length xs) - n) (xs @ [None]) ∈ sentences P ∧
(drop (Suc (length xs) - n) (xs @ [None]), W) ∈ failures Q"
using F by simp
moreover have H: "Suc (length xs) - n ≤ length xs"
using G by (simp, arith)
ultimately have I:
"take (Suc (length xs) - n) xs ∈ sentences P ∧
(drop (Suc (length xs) - n) xs @ [None], W) ∈ failures Q"
by simp
have "∃R. {} = (⋃n ∈ {..length (xs @ [x])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [x] ∉ sentences P ∧
None ∉ set (xs @ [x]) ∧ (xs @ [x], W) ∈ failures P ∨
xs @ [x] ∈ sentences P ∧
(∃U V. (xs @ [x], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [x])}. ∀W ∈ R n.
take (length (xs @ [x]) - n) (xs @ [x]) ∈ sentences P ∧
(drop (length (xs @ [x]) - n) (xs @ [x]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [x])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using E by (rule seq_comp_refusals_1)
then obtain R' where J: "?T R'" ..
hence "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R' n"
by simp
then obtain n' where K: "n' ∈ {..Suc (length xs)}" and L: "∃W. W ∈ R' n'" ..
have "n' = 0 ∨ n' ∈ {0<..Suc (length xs)}"
using K by auto
thus "x = None"
proof
assume "n' = 0"
hence "∃W. W ∈ R' 0"
using L by simp
then obtain W' where "W' ∈ R' 0" ..
hence
"xs @ [x] ∉ sentences P ∧
None ∉ set (xs @ [x]) ∧ (xs @ [x], W') ∈ failures P ∨
xs @ [x] ∈ sentences P ∧
(∃U V. (xs @ [x], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W' = insert None U ∩ V)"
using J by simp
hence M: "xs @ [x] ∈ traces P ∧ None ∉ set (xs @ [x])"
proof (cases "xs @ [x] ∈ sentences P", simp_all, (erule_tac [2] conjE)+,
simp_all)
case False
assume "(xs @ [x], W') ∈ failures P"
thus "xs @ [x] ∈ traces P"
by (rule failures_traces)
next
case True
hence "(xs @ [x]) @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "xs @ [x] ∈ traces P"
by (rule process_rule_2_traces)
moreover have "None ∉ set (xs @ [x])"
using C and True by (rule weakly_seq_sentences_none)
ultimately show "xs @ [x] ∈ traces P ∧ None ≠ x ∧ None ∉ set xs"
by simp
qed
have "xs @ [x] = take (Suc (length xs) - n) (xs @ [x]) @
drop (Suc (length xs) - n) (xs @ [x])"
by (simp only: append_take_drop_id)
hence "xs @ [x] = take (Suc (length xs) - n) xs @
drop (Suc (length xs) - n) xs @ [x]"
using H by simp
moreover have "∃y ys. drop (Suc (length xs) - n) xs @ [x] = y # ys"
by (cases "drop (Suc (length xs) - n) xs @ [x]", simp_all)
then obtain y and ys where "drop (Suc (length xs) - n) xs @ [x] = y # ys"
by blast
ultimately have N: "xs @ [x] = take (Suc (length xs) - n) xs @ y # ys"
by simp
have "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
moreover have "take (Suc (length xs) - n) xs @ y # ys ∈ traces P"
using M and N by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "y ≠ None"
using M and N by (rule_tac not_sym, simp)
ultimately show ?thesis
by contradiction
next
assume M: "n' ∈ {0<..Suc (length xs)}"
moreover obtain W' where "W' ∈ R' n'"
using L ..
ultimately have
"take (Suc (length xs) - n') (xs @ [x]) ∈ sentences P ∧
(drop (Suc (length xs) - n') (xs @ [x]), W') ∈ failures Q"
using J by simp
moreover have N: "Suc (length xs) - n' ≤ length xs"
using M by (simp, arith)
ultimately have O:
"take (Suc (length xs) - n') xs ∈ sentences P ∧
(drop (Suc (length xs) - n') xs @ [x], W') ∈ failures Q"
by simp
moreover have "n = n'"
proof (rule ccontr, simp add: neq_iff, erule disjE)
assume P: "n < n'"
have "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') (take (Suc (length xs) - n) xs) @
drop (Suc (length xs) - n') (take (Suc (length xs) - n) xs)"
by (simp only: append_take_drop_id)
also have "… =
take (Suc (length xs) - n') xs @
drop (Suc (length xs) - n') (take (Suc (length xs) - n) xs)"
using P by (simp add: min_def)
also have "… =
take (Suc (length xs) - n') xs @
take (n' - n) (drop (Suc (length xs) - n') xs)"
using M by (subst drop_take, simp)
finally have "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') xs @
take (n' - n) (drop (Suc (length xs) - n') xs)" .
moreover have "take (n' - n) (drop (Suc (length xs) - n') xs) ≠ []"
proof (rule_tac notI, simp, erule disjE)
assume "n' ≤ n"
thus False
using P by simp
next
assume "length xs ≤ Suc (length xs) - n'"
moreover have "Suc (length xs) - n' < Suc (length xs) - n"
using M and P by simp
hence "Suc (length xs) - n' < length xs"
using H by simp
ultimately show False
by simp
qed
hence "∃y ys. take (n' - n) (drop (Suc (length xs) - n') xs) = y # ys"
by (cases "take (n' - n) (drop (Suc (length xs) - n') xs)", simp_all)
then obtain y and ys where
"take (n' - n) (drop (Suc (length xs) - n') xs) = y # ys"
by blast
ultimately have Q: "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') xs @ y # ys"
by simp
have "take (Suc (length xs) - n') xs ∈ sentences P"
using O ..
moreover have R: "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
hence "take (Suc (length xs) - n) xs @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "take (Suc (length xs) - n) xs ∈ traces P"
by (rule process_rule_2_traces)
hence "take (Suc (length xs) - n') xs @ y # ys ∈ traces P"
using Q by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "None ∉ set (take (Suc (length xs) - n) xs)"
using C and R by (rule weakly_seq_sentences_none)
hence "y ≠ None"
using Q by (rule_tac not_sym, simp)
ultimately show False
by contradiction
next
assume P: "n' < n"
have "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) (take (Suc (length xs) - n') xs) @
drop (Suc (length xs) - n) (take (Suc (length xs) - n') xs)"
by (simp only: append_take_drop_id)
also have "… =
take (Suc (length xs) - n) xs @
drop (Suc (length xs) - n) (take (Suc (length xs) - n') xs)"
using P by (simp add: min_def)
also have "… =
take (Suc (length xs) - n) xs @
take (n - n') (drop (Suc (length xs) - n) xs)"
using G by (subst drop_take, simp)
finally have "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) xs @
take (n - n') (drop (Suc (length xs) - n) xs)" .
moreover have "take (n - n') (drop (Suc (length xs) - n) xs) ≠ []"
proof (rule_tac notI, simp, erule disjE)
assume "n ≤ n'"
thus False
using P by simp
next
assume "length xs ≤ Suc (length xs) - n"
moreover have "Suc (length xs) - n < Suc (length xs) - n'"
using G and P by simp
hence "Suc (length xs) - n < length xs"
using N by simp
ultimately show False
by simp
qed
hence "∃y ys. take (n - n') (drop (Suc (length xs) - n) xs) = y # ys"
by (cases "take (n - n') (drop (Suc (length xs) - n) xs)", simp_all)
then obtain y and ys where
"take (n - n') (drop (Suc (length xs) - n) xs) = y # ys"
by blast
ultimately have Q: "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) xs @ y # ys"
by simp
have "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
moreover have R: "take (Suc (length xs) - n') xs ∈ sentences P"
using O ..
hence "take (Suc (length xs) - n') xs @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "take (Suc (length xs) - n') xs ∈ traces P"
by (rule process_rule_2_traces)
hence "take (Suc (length xs) - n) xs @ y # ys ∈ traces P"
using Q by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "None ∉ set (take (Suc (length xs) - n') xs)"
using C and R by (rule weakly_seq_sentences_none)
hence "y ≠ None"
using Q by (rule_tac not_sym, simp)
ultimately show False
by contradiction
qed
ultimately have "(drop (Suc (length xs) - n) xs @ [x], W') ∈ failures Q"
by simp
hence P: "drop (Suc (length xs) - n) xs @ [x] ∈ traces Q"
by (