(* Title: Conservation of CSP Noninterference Security under Sequential 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 "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 (