Theory GeneralizedZippingLemma
theory GeneralizedZippingLemma
imports CompositionBase
begin
context Compositionality
begin
lemma generalized_zipping_lemma1: "⟦ N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {}; N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {} ⟧ ⟹
∀ τ lambda t1 t2. ( ( set τ ⊆ E⇘(ES1 ∥ ES2)⇙ ∧ set lambda ⊆ V⇘𝒱⇙ ∧ set t1 ⊆ E⇘ES1⇙ ∧ set t2 ⊆ E⇘ES2⇙
∧ ((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙ ∧ ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙ ∧ (lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙)
∧ (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙) ∧ (t1 ↿ C⇘𝒱1⇙) = [] ∧ (t2 ↿ C⇘𝒱2⇙) = [])
⟶ (∃ t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = [])) )"
proof -
assume Nv1_inter_E2_empty: "N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {}"
and Nv2_inter_E1_empty: "N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {}"
{
fix τ lambda t1 t2
assume τ_in_Estar: "set τ ⊆ E⇘(ES1 ∥ ES2)⇙"
and lambda_in_Vvstar: "set lambda ⊆ V⇘𝒱⇙"
and t1_in_E1star: "set t1 ⊆ E⇘ES1⇙"
and t2_in_E2star: "set t2 ⊆ E⇘ES2⇙"
and τ_E1_t1_in_Tr1: "((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙"
and τ_E2_t2_in_Tr2: "((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙"
and lambda_E1_is_t1_Vv: "(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙)"
and lambda_E2_is_t2_Vv: "(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)"
and t1_no_Cv1: "(t1 ↿ C⇘𝒱1⇙) = []"
and t2_no_Cv2: "(t2 ↿ C⇘𝒱2⇙) = []"
have "⟦ set τ ⊆ E⇘(ES1 ∥ ES2)⇙;
set lambda ⊆ V⇘𝒱⇙;
set t1 ⊆ E⇘ES1⇙;
set t2 ⊆ E⇘ES2⇙;
((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙;
((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙;
(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙);
(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙);
(t1 ↿ C⇘𝒱1⇙) = [];
(t2 ↿ C⇘𝒱2⇙) = [] ⟧
⟹ (∃ t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = []))"
proof (induct lambda arbitrary: τ t1 t2)
case (Nil τ t1 t2)
have "(τ @ []) ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
have "τ ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
from Nil(5) validES1 have "τ ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
from Nil(6) validES2 have "τ ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
note Nil(1)
ultimately show ?thesis
by (simp add: composeES_def)
qed
thus ?thesis
by auto
qed
moreover
have "([] ↿ V⇘𝒱⇙) = []"
by (simp add: projection_def)
moreover
have "([] ↿ C⇘𝒱⇙) = []"
by (simp add: projection_def)
ultimately show ?case
by blast
next
case (Cons 𝒱' lambda' τ t1 t2)
thus ?case
proof -
from Cons(3) have v'_in_Vv: "𝒱' ∈ V⇘𝒱⇙"
by auto
have "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙
∨ 𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙
∨ 𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
using Vv_is_Vv1_union_Vv2 v'_in_Vv propSepViews
unfolding properSeparationOfViews_def
by fastforce
moreover {
assume v'_in_Vv1_inter_Vv2: "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙" and v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv propSepViews
have v'_in_E1: "𝒱' ∈ E⇘ES1⇙" and v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def by auto
from Cons(2,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1 have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙"
and s1_in_E1star: "set s1 ⊆ E⇘ES1⇙"
by auto
from Cons(6) t1_is_r1_v'_s1
have τE1_r1_v'_s1_in_Tr1: "τ ↿ E⇘ES1⇙ @ r1 @ [𝒱'] @ s1 ∈ Tr⇘ES1⇙"
by simp
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq Int_commute
Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq Int_commute
Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv1_inter_E2_empty have r1E2_empty: "r1 ↿ E⇘ES2⇙ = []"
by (metis Int_commute empty_subsetI projection_on_subset2 r1_Vv_empty)
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
and s2_in_E2star: "set s2 ⊆ E⇘ES2⇙"
by auto
from Cons(7) t2_is_r2_v'_s2
have τE2_r2_v'_s2_in_Tr2: "τ ↿ E⇘ES2⇙ @ r2 @ [𝒱'] @ s2 ∈ Tr⇘ES2⇙"
by simp
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv2_inter_E1_empty have r2E1_empty: "r2 ↿ E⇘ES1⇙ = []"
by (metis Int_commute empty_subsetI projection_on_subset2 r2_Vv_empty)
let ?tau = "τ @ r1 @ r2 @ [𝒱']"
from Cons(2) r1_in_E1star r2_in_E2star v'_in_E2
have "set ?tau ⊆ (E⇘(ES1 ∥ ES2)⇙)"
by (simp add: composeES_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
note s1_in_E1star s2_in_E2star
moreover
from Cons(6) r1_in_E1star r2E1_empty v'_in_E1 t1_is_r1_v'_s1
have "((?tau ↿ E⇘ES1⇙) @ s1) ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute
list_subset_iff_projection_neutral projection_def, auto)
moreover
from Cons(7) r2_in_E2star r1E2_empty v'_in_E2 t2_is_r2_v'_s2
have "((?tau ↿ E⇘ES2⇙) @ s2) ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute
list_subset_iff_projection_neutral projection_def, auto)
moreover
have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
proof -
from Cons(2,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from t1_is_r1_v'_s1 r1_Vv_empty v'_in_Vv1 Vv_is_Vv1_union_Vv2
have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (s1 ↿ V⇘𝒱⇙)"
by (simp only: t1_is_r1_v'_s1 projection_concatenation_commute
projection_def, auto)
ultimately show ?thesis
by auto
qed
moreover
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
proof -
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from t2_is_r2_v'_s2 r2_Vv_empty v'_in_Vv2 Vv_is_Vv1_union_Vv2
have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (s2 ↿ V⇘𝒱⇙)"
by (simp only: t2_is_r2_v'_s2 projection_concatenation_commute
projection_def, auto)
ultimately show ?thesis
by auto
qed
moreover
note s1_Cv1_empty s2_Cv2_empty Cons.hyps(1)[of ?tau s1 s2]
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ r2 @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r1_Vv_empty r2_Vv_empty t'Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES1⇙ ⊆ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def by auto
hence "r1 ↿ C⇘𝒱⇙ = []"
by (metis projection_on_subset2 r1_Cv1_empty r1_in_E1star)
moreover
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def by auto
hence "r2 ↿ C⇘𝒱⇙ = []"
by (metis projection_on_subset2 r2_Cv2_empty r2_in_E2star)
moreover
note v'_in_Vv VIsViewOnE t'Cv_empty
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv1_minus_E2: "𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙"
by auto
with v'_in_Vv propSepViews have v'_in_E1: "𝒱' ∈ E⇘ES1⇙"
unfolding properSeparationOfViews_def
by auto
from v'_in_Vv1_minus_E2 have v'_notin_E2: "𝒱' ∉ E⇘ES2⇙"
by (auto)
with validV2 have v'_notin_Vv2: "𝒱' ∉ V⇘𝒱2⇙"
by (simp add: isViewOn_def V_valid_def, auto)
from Cons(3) Cons(4) Cons(8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1 have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙"
by auto
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq Int_commute
Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq Int_commute
Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv1_inter_E2_empty have r1E2_empty: "r1 ↿ E⇘ES2⇙ = []"
by (metis Int_commute empty_subsetI
projection_on_subset2 r1_Vv1_empty)
let ?tau = "τ @ r1 @ [𝒱']"
from v'_in_E1 Cons(2) r1_in_Nv1star validV1
have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: isViewOn_def composeES_def V_valid_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(4) t1_is_r1_v'_s1 have "set s1 ⊆ E⇘ES1⇙"
by auto
moreover
note Cons(5)
moreover
have "?tau ↿ E⇘ES1⇙ @ s1 ∈ Tr⇘ES1⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(3) Cons.prems(5)
projection_concatenation_commute t1_is_r1_v'_s1)
moreover
have "?tau ↿ E⇘ES2⇙ @ t2 ∈ Tr⇘ES2⇙"
proof -
from v'_notin_E2 have "[𝒱'] ↿ E⇘ES2⇙ = []"
by (simp add: projection_def)
with Cons(7) Cons(4) t1_is_r1_v'_s1 v'_notin_E2
r1_in_Nv1star Nv1_inter_E2_empty r1E2_empty
show ?thesis
by (simp only: t1_is_r1_v'_s1 list_subset_iff_projection_neutral
projection_concatenation_commute, auto)
qed
moreover
from Cons(8) t1_is_r1_v'_s1 r1_Vv_empty v'_in_E1 v'_in_Vv have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(9) v'_notin_E2 have "lambda' ↿ E⇘ES2⇙ = t2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
note s1_Cv1_empty Cons(11)
moreover
note Cons.hyps(1)[of ?tau s1 t2]
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r1_Vv_empty t'_Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES1⇙ ⊆ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def by auto
hence"r1 ↿ C⇘𝒱⇙ = []"
by (metis projection_on_subset2 r1_Cv1_empty r1_in_E1star)
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv2_minus_E1: "𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
hence v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv propSepViews
have v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def by auto
from v'_in_Vv2_minus_E1
have v'_notin_E1: "𝒱' ∉ E⇘ES1⇙"
by (auto)
with validV1
have v'_notin_Vv1: "𝒱' ∉ V⇘𝒱1⇙"
by (simp add:isViewOn_def V_valid_def, auto)
from Cons(4) Cons(5) Cons(9) v'_in_E2
have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
by auto
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv2_inter_E1_empty have r2E1_empty: "r2 ↿ E⇘ES1⇙ = []"
by (metis Int_commute empty_subsetI
projection_on_subset2 r2_Vv2_empty)
let ?tau = "τ @ r2 @ [𝒱']"
from v'_in_E2 Cons(2) r2_in_Nv2star validV2
have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
note Cons(4)
moreover
from Cons(5) t2_is_r2_v'_s2 have "set s2 ⊆ E⇘ES2⇙"
by auto
moreover
have "?tau ↿ E⇘ES1⇙ @ t1 ∈ Tr⇘ES1⇙"
proof -
from v'_notin_E1 have "[𝒱'] ↿ E⇘ES1⇙ = []"
by (simp add: projection_def)
with Cons(6) Cons(3) t2_is_r2_v'_s2 v'_notin_E1 r2_in_Nv2star
Nv2_inter_E1_empty r2E1_empty
show ?thesis
by (simp only: t2_is_r2_v'_s2 list_subset_iff_projection_neutral
projection_concatenation_commute, auto)
qed
moreover
have "?tau ↿ E⇘ES2⇙ @ s2 ∈ Tr⇘ES2⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(4) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(4) Cons.prems(6)
projection_concatenation_commute t2_is_r2_v'_s2)
moreover
from Cons(8) v'_notin_E1 have "lambda' ↿ E⇘ES1⇙ = t1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(9) t2_is_r2_v'_s2 r2_Vv_empty v'_in_E2 v'_in_Vv
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
note Cons(10) s2_Cv2_empty
moreover
note Cons.hyps(1)[of ?tau t1 s2]
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r2_Vv_empty t'_Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def by auto
hence "r2 ↿ C⇘𝒱⇙ = []"
by (metis projection_on_subset2 r2_Cv2_empty r2_in_E2star)
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
ultimately show ?thesis
by blast
qed
qed
}
thus ?thesis
by auto
qed
lemma generalized_zipping_lemma2: "⟦ N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {}; total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙); BSIA ρ1 𝒱1 Tr⇘ES1⇙ ⟧ ⟹
∀ τ lambda t1 t2. ( ( set τ ⊆ (E⇘(ES1 ∥ ES2)⇙) ∧ set lambda ⊆ V⇘𝒱⇙ ∧ set t1 ⊆ E⇘ES1⇙ ∧ set t2 ⊆ E⇘ES2⇙
∧ ((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙ ∧ ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙
∧ (lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙) ∧ (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)
∧ (t1 ↿ C⇘𝒱1⇙) = [] ∧ (t2 ↿ C⇘𝒱2⇙) = [])
⟶ (∃ t. ((τ @ t) ∈ (Tr⇘(ES1 ∥ ES2)⇙) ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = [])) )"
proof -
assume Nv1_inter_E2_empty: "N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {}"
assume total_ES1_Cv1_inter_Nv2: "total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙)"
assume BSIA: "BSIA ρ1 𝒱1 Tr⇘ES1⇙"
{
fix τ lambda t1 t2
assume τ_in_Estar: "set τ ⊆ E⇘(ES1 ∥ ES2)⇙"
and lambda_in_Vvstar: "set lambda ⊆ V⇘𝒱⇙"
and t1_in_E1star: "set t1 ⊆ E⇘ES1⇙"
and t2_in_E2star: "set t2 ⊆ E⇘ES2⇙"
and τ_E1_t1_in_Tr1: "((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙"
and τ_E2_t2_in_Tr2: "((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙"
and lambda_E1_is_t1_Vv: "(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙)"
and lambda_E2_is_t2_Vv: "(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)"
and t1_no_Cv1: "(t1 ↿ C⇘𝒱1⇙) = []"
and t2_no_Cv2: "(t2 ↿ C⇘𝒱2⇙) = []"
have "⟦ set τ ⊆ E⇘(ES1 ∥ ES2)⇙; set lambda ⊆ V⇘𝒱⇙;
set t1 ⊆ E⇘ES1⇙; set t2 ⊆ E⇘ES2⇙;
((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙; ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙;
(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙); (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙);
(t1 ↿ C⇘𝒱1⇙) = []; (t2 ↿ C⇘𝒱2⇙) = [] ⟧
⟹ (∃t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = []))"
proof (induct lambda arbitrary: τ t1 t2)
case (Nil τ t1 t2)
have "(τ @ []) ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
have "τ ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
from Nil(5) validES1 have "τ ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
from Nil(6) validES2 have "τ ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
note Nil(1)
ultimately show ?thesis
by (simp add: composeES_def)
qed
thus ?thesis
by auto
qed
moreover
have "([] ↿ V⇘𝒱⇙) = []"
by (simp add: projection_def)
moreover
have "([] ↿ C⇘𝒱⇙) = []"
by (simp add: projection_def)
ultimately show ?case
by blast
next
case (Cons 𝒱' lambda' τ t1 t2)
thus ?case
proof -
from Cons(3) have v'_in_Vv: "𝒱' ∈ V⇘𝒱⇙"
by auto
have "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∨ 𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙ ∨ 𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def
using Vv_is_Vv1_union_Vv2 v'_in_Vv by fastforce
moreover {
assume v'_in_Vv1_inter_Vv2: "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙" and v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv propSepViews
have v'_in_E1: "𝒱' ∈ E⇘ES1⇙" and v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def by auto
from Cons(3,5,9) v'_in_E2
have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
and s2_in_E2star: "set s2 ⊆ E⇘ES2⇙"
by auto
from Cons(7) t2_is_r2_v'_s2
have τE2_r2_v'_s2_in_Tr2: "τ ↿ E⇘ES2⇙ @ r2 @ [𝒱'] @ s2 ∈ Tr⇘ES2⇙"
by simp
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r2E1_in_Nv2_inter_C1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) = set r2 ∩ E⇘ES1⇙"
by (simp add: projection_def, auto)
with r2_in_Nv2star have "set (r2 ↿ E⇘ES1⇙) ⊆ (E⇘ES1⇙ ∩ N⇘𝒱2⇙)"
by auto
moreover
from validV1 propSepViews
have "E⇘ES1⇙ ∩ N⇘𝒱2⇙ = N⇘𝒱2⇙ ∩ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def isViewOn_def V_valid_def
using disjoint_Nv2_Vv1 by blast
ultimately show ?thesis
by auto
qed
note outerCons_prems = Cons.prems
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙) ⟹
∃ t1'. ( set t1' ⊆ E⇘ES1⇙
∧ ((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙
∧ t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙
∧ t1' ↿ C⇘𝒱1⇙ = [] )"
proof (induct "r2 ↿ E⇘ES1⇙" arbitrary: r2 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(9)
outerCons_prems(3) outerCons_prems(5) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE1: "xs = xs ↿ E⇘ES1⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES1⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES1⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by auto
with xs_is_xsE1 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t1''
where t1''_in_E1star: "set t1'' ⊆ E⇘ES1⇙"
and τ_xs_E1_t1''_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ t1'' ∈ Tr⇘ES1⇙"
and t1''Vv1_is_t1Vv1: "t1'' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1''Cv1_empty: "t1'' ↿ C⇘𝒱1⇙ = []"
by auto
have x_in_Cv1_inter_Nv2: "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv1: "x ∈ C⇘𝒱1⇙"
by auto
moreover
note τ_xs_E1_t1''_in_Tr1 t1''Cv1_empty
moreover
have Adm: "(Adm 𝒱1 ρ1 Tr⇘ES1⇙ ((τ @ xs) ↿ E⇘ES1⇙) x)"
proof -
from τ_xs_E1_t1''_in_Tr1 validES1
have τ_xsE1_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv1_inter_Nv2 total_ES1_Cv1_inter_Nv2
have τ_xsE1_x_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] ∈ Tr⇘ES1⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1) = ((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA
ultimately obtain t1'
where res1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1' ∈ Tr⇘ES1⇙"
and res2: "t1' ↿ V⇘𝒱1⇙ = t1'' ↿ V⇘𝒱1⇙"
and res3: "t1' ↿ C⇘𝒱1⇙ = []"
by (simp only: BSIA_def, blast)
have "set t1' ⊆ E⇘ES1⇙"
proof -
from res1 validES1
have "set (((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1') ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
proof -
from res1 xs_is_xsE1 have "((τ ↿ E⇘ES1⇙) @ (xs @ [x])) @ t1' ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t1''Vv1_is_t1Vv1 res2 have "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r2E1_in_Nv2_inter_C1_star] obtain t1'
where t1'_in_E1star: "set t1' ⊆ E⇘ES1⇙"
and τr2E1_t1'_in_Tr1: "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
and t1'_Vv1_is_t1_Vv1: "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1'_Cv1_empty: "t1' ↿ C⇘𝒱1⇙ = []"
by auto
have "t1' ↿ V⇘𝒱1⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
proof -
from projection_intersection_neutral[OF Cons(4), of "V⇘𝒱⇙"]
propSepViews
have "t1 ↿ V⇘𝒱⇙ = t1 ↿ V⇘𝒱1⇙"
unfolding properSeparationOfViews_def
by (simp only: Int_commute)
with Cons(8) t1'_Vv1_is_t1_Vv1 v'_in_E1 show ?thesis
by (simp add: projection_def)
qed
from projection_split_first[OF this] obtain r1' s1'
where t1'_is_r1'_v'_s1': "t1' = r1' @ [𝒱'] @ s1'"
and r1'_Vv1_empty: "r1' ↿ V⇘𝒱1⇙ = []"
by auto
from t1'_is_r1'_v'_s1' t1'_Cv1_empty
have r1'_Cv1_empty: "r1' ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1'_is_r1'_v'_s1' t1'_Cv1_empty
have s1'_Cv1_empty: "s1' ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from t1'_in_E1star t1'_is_r1'_v'_s1'
have r1'_in_E1star: "set r1' ⊆ E⇘ES1⇙"
by auto
with propSepViews r1'_Vv1_empty
have r1'_Vv_empty: "r1' ↿ V⇘𝒱⇙ = []"
unfolding properSeparationOfViews_def
by (metis projection_on_subset2 subset_iff_psubset_eq)
have r1'_in_Nv1star: "set r1' ⊆ N⇘𝒱1⇙"
proof -
note r1'_in_E1star
moreover
from r1'_Vv1_empty have "set r1' ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r1'_Cv1_empty have "set r1' ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv1_inter_E2_empty have r1'E2_empty: "r1' ↿ E⇘ES2⇙ = []"
by (metis Int_commute empty_subsetI
projection_on_subset2 r1'_Vv1_empty)
let ?tau = "τ @ r2 @ r1' @ [𝒱']"
from Cons(2) r2_in_E2star r1'_in_E1star v'_in_E2
have "set ?tau ⊆ (E⇘(ES1 ∥ ES2)⇙)"
by (simp add: composeES_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from t1'_in_E1star t1'_is_r1'_v'_s1'
have "set s1' ⊆ E⇘ES1⇙"
by simp
moreover
note s2_in_E2star
moreover
from τr2E1_t1'_in_Tr1 t1'_is_r1'_v'_s1' v'_in_E1
have "?tau ↿ E⇘ES1⇙ @ s1' ∈ Tr⇘ES1⇙"
proof -
from v'_in_E1 r1'_in_E1star
have "(τ @ r2 @ r1' @ [𝒱']) ↿ E⇘ES1⇙ = (τ @ r2) ↿ E⇘ES1⇙ @ r1' @ [𝒱']"
by (simp only: projection_concatenation_commute
list_subset_iff_projection_neutral projection_def, auto)
with τr2E1_t1'_in_Tr1 t1'_is_r1'_v'_s1' v'_in_E1 show ?thesis
by simp
qed
moreover
from r2_in_E2star v'_in_E2 r1'E2_empty τE2_r2_v'_s2_in_Tr2
have "?tau ↿ E⇘ES2⇙ @ s2 ∈ Tr⇘ES2⇙"
by (simp only: list_subset_iff_projection_neutral
projection_concatenation_commute projection_def, auto)
moreover
have "lambda' ↿ E⇘ES1⇙ = s1' ↿ V⇘𝒱⇙"
proof -
from Cons(2,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from t1'_is_r1'_v'_s1' r1'_Vv1_empty r1'_in_E1star v'_in_Vv1 propSepViews
have "t1' ↿ V⇘𝒱⇙ = [𝒱'] @ (s1' ↿ V⇘𝒱⇙)"
proof -
have "r1' ↿ V⇘𝒱⇙ =[]"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2
r1'_Vv1_empty r1'_in_E1star subset_iff_psubset_eq)
with t1'_is_r1'_v'_s1' v'_in_Vv1 Vv_is_Vv1_union_Vv2 show ?thesis
by (simp only: t1'_is_r1'_v'_s1' projection_concatenation_commute
projection_def, auto)
qed
moreover
have "t1 ↿ V⇘𝒱⇙ = t1' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute outerCons_prems(3)
projection_intersection_neutral
t1'_Vv1_is_t1_Vv1 t1'_in_E1star)
ultimately show ?thesis
by auto
qed
moreover
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
proof -
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from t2_is_r2_v'_s2 r2_Vv_empty v'_in_Vv2 Vv_is_Vv1_union_Vv2
have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (s2 ↿ V⇘𝒱⇙)"
by (simp only: t2_is_r2_v'_s2 projection_concatenation_commute projection_def, auto)
ultimately show ?thesis
by auto
qed
moreover
note s1'_Cv1_empty s2_Cv2_empty Cons.hyps[of ?tau s1' s2]
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ r1' @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r2_Vv_empty r1'_Vv_empty t'Vv_is_lambda' v'_in_Vv have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by(simp only: projection_concatenation_commute projection_def, auto)
moreover
from VIsViewOnE r2_Cv2_empty t'Cv_empty r1'_Cv1_empty v'_in_Vv
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from VIsViewOnE v'_in_Vv have "[𝒱'] ↿ C⇘𝒱⇙ = []"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def projection_def, auto)
moreover
from r2_in_E2star r2_Cv2_empty propSepViews
have "r2 ↿ C⇘𝒱⇙ = []"
unfolding properSeparationOfViews_def
using projection_on_subset2 by auto
moreover
from r1'_in_E1star r1'_Cv1_empty propSepViews
have "r1' ↿ C⇘𝒱⇙ = []"
unfolding properSeparationOfViews_def
using projection_on_subset2 by auto
moreover
note t'Cv_empty
ultimately show ?thesis
by (simp only: projection_concatenation_commute, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv1_minus_E2: "𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙"
by auto
with v'_in_Vv propSepViews have v'_in_E1: "𝒱' ∈ E⇘ES1⇙"
unfolding properSeparationOfViews_def by auto
from v'_in_Vv1_minus_E2 have v'_notin_E2: "𝒱' ∉ E⇘ES2⇙"
by (auto)
with validV2 have v'_notin_Vv2: "𝒱' ∉ V⇘𝒱2⇙"
by (simp add: isViewOn_def V_valid_def, auto)
from Cons(3) Cons(4) Cons(8) v'_in_E1
have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10)
have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10)
have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1
have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙"
by auto
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq
Int_commute Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq
Int_commute Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv1_inter_E2_empty have r1E2_empty: "r1 ↿ E⇘ES2⇙ = []"
by (metis Int_commute empty_subsetI projection_on_subset2 r1_Vv1_empty)
let ?tau = "τ @ r1 @ [𝒱']"
from v'_in_E1 Cons(2) r1_in_Nv1star validV1
have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(4) t1_is_r1_v'_s1 have "set s1 ⊆ E⇘ES1⇙"
by auto
moreover
note Cons(5)
moreover
have "?tau ↿ E⇘ES1⇙ @ s1 ∈ Tr⇘ES1⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(3) Cons.prems(5)
projection_concatenation_commute t1_is_r1_v'_s1)
moreover
have "?tau ↿ E⇘ES2⇙ @ t2 ∈ Tr⇘ES2⇙"
proof -
from v'_notin_E2 have "[𝒱'] ↿ E⇘ES2⇙ = []"
by (simp add: projection_def)
with Cons(7) Cons(4) t1_is_r1_v'_s1 v'_notin_E2 r1_in_Nv1star
Nv1_inter_E2_empty r1E2_empty
show ?thesis
by (simp only: t1_is_r1_v'_s1 list_subset_iff_projection_neutral
projection_concatenation_commute, auto)
qed
moreover
from Cons(8) t1_is_r1_v'_s1 r1_Vv_empty v'_in_E1 v'_in_Vv
have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(9) v'_notin_E2 have "lambda' ↿ E⇘ES2⇙ = t2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
note s1_Cv1_empty Cons(11)
moreover
note Cons.hyps(1)[of ?tau s1 t2]
ultimately obtain t'
where τr1v't'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ [𝒱'] @ t'"
note τr1v't'_in_Tr
moreover
from r1_Vv_empty t'_Vv_is_lambda' v'_in_Vv have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r1 ↿ C⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2 r1_Cv1_empty r1_in_E1star)
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv2_minus_E1: "𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
hence v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv propSepViews
have v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def by auto
from v'_in_Vv2_minus_E1
have v'_notin_E1: "𝒱' ∉ E⇘ES1⇙"
by (auto)
with validV1
have v'_notin_Vv1: "𝒱' ∉ V⇘𝒱1⇙"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
from Cons(3) Cons(5) Cons(9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
by auto
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r2E1_in_Nv2_inter_C1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) = set r2 ∩ E⇘ES1⇙"
by (simp add: projection_def, auto)
with r2_in_Nv2star have "set (r2 ↿ E⇘ES1⇙) ⊆ (E⇘ES1⇙ ∩ N⇘𝒱2⇙)"
by auto
moreover
from validV1 propSepViews disjoint_Nv2_Vv1 have "E⇘ES1⇙ ∩ N⇘𝒱2⇙ = N⇘𝒱2⇙ ∩ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
note outerCons_prems = Cons.prems
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙) ⟹
∃ t1'. ( set t1' ⊆ E⇘ES1⇙
∧ ((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙
∧ t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙
∧ t1' ↿ C⇘𝒱1⇙ = [] )"
proof (induct "r2 ↿ E⇘ES1⇙" arbitrary: r2 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(9) outerCons_prems(3)
outerCons_prems(5) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE1: "xs = xs ↿ E⇘ES1⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES1⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES1⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by auto
with xs_is_xsE1 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t1''
where t1''_in_E1star: "set t1'' ⊆ E⇘ES1⇙"
and τ_xs_E1_t1''_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ t1'' ∈ Tr⇘ES1⇙"
and t1''Vv1_is_t1Vv1: "t1'' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1''Cv1_empty: "t1'' ↿ C⇘𝒱1⇙ = []"
by auto
have x_in_Cv1_inter_Nv2: "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv1: "x ∈ C⇘𝒱1⇙"
by auto
moreover
note τ_xs_E1_t1''_in_Tr1 t1''Cv1_empty
moreover
have Adm: "(Adm 𝒱1 ρ1 Tr⇘ES1⇙ ((τ @ xs) ↿ E⇘ES1⇙) x)"
proof -
from τ_xs_E1_t1''_in_Tr1 validES1
have τ_xsE1_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv1_inter_Nv2 total_ES1_Cv1_inter_Nv2
have τ_xsE1_x_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] ∈ Tr⇘ES1⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1) = ((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA
ultimately obtain t1'
where res1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1' ∈ Tr⇘ES1⇙"
and res2: "t1' ↿ V⇘𝒱1⇙ = t1'' ↿ V⇘𝒱1⇙"
and res3: "t1' ↿ C⇘𝒱1⇙ = []"
by (simp only: BSIA_def, blast)
have "set t1' ⊆ E⇘ES1⇙"
proof -
from res1 validES1 have "set (((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1') ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
proof -
from res1 xs_is_xsE1 have "((τ ↿ E⇘ES1⇙) @ (xs @ [x])) @ t1' ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t1''Vv1_is_t1Vv1 res2 have "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r2E1_in_Nv2_inter_C1_star] obtain t1'
where t1'_in_E1star: "set t1' ⊆ E⇘ES1⇙"
and τr2E1_t1'_in_Tr1: "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
and t1'_Vv1_is_t1_Vv1: "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1'_Cv1_empty: "t1' ↿ C⇘𝒱1⇙ = []"
by auto
let ?tau = "τ @ r2 @ [𝒱']"
from v'_in_E2 Cons(2) r2_in_Nv2star validV2 have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(5) t2_is_r2_v'_s2 have "set s2 ⊆ E⇘ES2⇙"
by auto
moreover
note t1'_in_E1star
moreover
have "?tau ↿ E⇘ES2⇙ @ s2 ∈ Tr⇘ES2⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(4) Cons.prems(6)
projection_concatenation_commute t2_is_r2_v'_s2)
moreover
from τr2E1_t1'_in_Tr1 v'_notin_E1 have "?tau ↿ E⇘ES1⇙ @ t1' ∈ Tr⇘ES1⇙"
by (simp add: projection_def)
moreover
from Cons(9) t2_is_r2_v'_s2 r2_Vv_empty v'_in_E2 v'_in_Vv
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(10) v'_notin_E1 t1'_Vv1_is_t1_Vv1 have "lambda' ↿ E⇘ES1⇙ = t1' ↿ V⇘𝒱⇙"
proof -
have "t1' ↿ V⇘𝒱⇙ = t1' ↿ V⇘𝒱1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral
t1'_in_E1star)
moreover
have "t1 ↿ V⇘𝒱⇙ = t1 ↿ V⇘𝒱1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def
projection_intersection_neutral Cons(4))
moreover
note Cons(8) v'_notin_E1 t1'_Vv1_is_t1_Vv1
ultimately show ?thesis
by (simp add: projection_def)
qed
moreover
note s2_Cv2_empty t1'_Cv1_empty
moreover
note Cons.hyps(1)[of ?tau t1' s2]
ultimately obtain t'
where τr2v't'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ [𝒱'] @ t'"
note τr2v't'_in_Tr
moreover
from r2_Vv_empty t'_Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r2 ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def by auto
from projection_on_subset[OF ‹C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙› r2_Cv2_empty]
have "r2 ↿ (E⇘ES2⇙ ∩ C⇘𝒱⇙) = []"
by (simp only: Int_commute)
with projection_intersection_neutral[OF r2_in_E2star, of "C⇘𝒱⇙"] show ?thesis
by simp
qed
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
ultimately show ?thesis
by blast
qed
qed
}
thus ?thesis
by auto
qed
lemma generalized_zipping_lemma3: "⟦ N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {}; total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙); BSIA ρ2 𝒱2 Tr⇘ES2⇙ ⟧ ⟹
∀ τ lambda t1 t2. ( ( set τ ⊆ E⇘(ES1 ∥ ES2)⇙ ∧ set lambda ⊆ V⇘𝒱⇙ ∧ set t1 ⊆ E⇘ES1⇙ ∧ set t2 ⊆ E⇘ES2⇙
∧ ((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙ ∧ ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙
∧ (lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙) ∧ (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)
∧ (t1 ↿ C⇘𝒱1⇙) = [] ∧ (t2 ↿ C⇘𝒱2⇙) = [])
⟶ (∃ t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = [])) )"
proof -
assume Nv2_inter_E1_empty: "N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {}"
assume total_ES2_Cv2_inter_Nv1: "total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙)"
assume BSIA: "BSIA ρ2 𝒱2 Tr⇘ES2⇙"
{
fix τ lambda t1 t2
assume τ_in_Estar: "set τ ⊆ E⇘(ES1 ∥ ES2)⇙"
and lambda_in_Vvstar: "set lambda ⊆ V⇘𝒱⇙"
and t1_in_E1star: "set t1 ⊆ E⇘ES1⇙"
and t2_in_E2star: "set t2 ⊆ E⇘ES2⇙"
and τ_E1_t1_in_Tr1: "((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙"
and τ_E2_t2_in_Tr2: "((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙"
and lambda_E1_is_t1_Vv: "(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙)"
and lambda_E2_is_t2_Vv: "(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)"
and t1_no_Cv1: "(t1 ↿ C⇘𝒱1⇙) = []"
and t2_no_Cv2: "(t2 ↿ C⇘𝒱2⇙) = []"
have "⟦ set τ ⊆ E⇘(ES1 ∥ ES2)⇙;
set lambda ⊆ V⇘𝒱⇙;
set t1 ⊆ E⇘ES1⇙;
set t2 ⊆ E⇘ES2⇙;
((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙;
((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙;
(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙);
(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙);
(t1 ↿ C⇘𝒱1⇙) = [];
(t2 ↿ C⇘𝒱2⇙) = [] ⟧
⟹ (∃ t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = []))"
proof (induct lambda arbitrary: τ t1 t2)
case (Nil τ t1 t2)
have "(τ @ []) ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
have "τ ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
from Nil(5) validES1 have "τ ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
from Nil(6) validES2 have "τ ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
note Nil(1)
ultimately show ?thesis
by (simp add: composeES_def)
qed
thus ?thesis
by auto
qed
moreover
have "([] ↿ V⇘𝒱⇙) = []"
by (simp add: projection_def)
moreover
have "([] ↿ C⇘𝒱⇙) = []"
by (simp add: projection_def)
ultimately show ?case
by blast
next
case (Cons 𝒱' lambda' τ t1 t2)
thus ?case
proof -
from Cons(3) have v'_in_Vv: "𝒱' ∈ V⇘𝒱⇙"
by auto
have "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙
∨ 𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙
∨ 𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Diff_iff Int_commute Int_iff Un_iff
Vv_is_Vv1_union_Vv2 v'_in_Vv)
moreover {
assume v'_in_Vv1_inter_Vv2: "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙"
hence v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙" and v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙"
by auto
with v'_in_Vv
have v'_in_E2: "𝒱' ∈ E⇘ES2⇙" and v'_in_E1: "𝒱' ∈ E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def by auto
from Cons(2,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1
have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙" and s1_in_E1star: "set s1 ⊆ E⇘ES1⇙"
by auto
from Cons(6) t1_is_r1_v'_s1
have τE1_r1_v'_s1_in_Tr1: "τ ↿ E⇘ES1⇙ @ r1 @ [𝒱'] @ s1 ∈ Tr⇘ES1⇙"
by simp
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
qed
have r1E2_in_Nv1_inter_C2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) = set r1 ∩ E⇘ES2⇙"
by (simp add: projection_def, auto)
with r1_in_Nv1star have "set (r1 ↿ E⇘ES2⇙) ⊆ (E⇘ES2⇙ ∩ N⇘𝒱1⇙)"
by auto
moreover
from validV2 disjoint_Nv1_Vv2
have "E⇘ES2⇙ ∩ N⇘𝒱1⇙ = N⇘𝒱1⇙ ∩ C⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add:isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
note outerCons_prems = Cons.prems
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙) ⟹
∃ t2'. ( set t2' ⊆ E⇘ES2⇙
∧ ((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙
∧ t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙
∧ t2' ↿ C⇘𝒱2⇙ = [] )"
proof (induct "r1 ↿ E⇘ES2⇙" arbitrary: r1 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(10) outerCons_prems(4)
outerCons_prems(6) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE2: "xs = xs ↿ E⇘ES2⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES2⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES2⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by auto
with xs_is_xsE2 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t2''
where t2''_in_E2star: "set t2'' ⊆ E⇘ES2⇙"
and τ_xs_E2_t2''_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ t2'' ∈ Tr⇘ES2⇙"
and t2''Vv2_is_t2Vv2: "t2'' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2''Cv2_empty: "t2'' ↿ C⇘𝒱2⇙ = []"
by auto
have x_in_Cv2_inter_Nv1: "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv2: "x ∈ C⇘𝒱2⇙"
by auto
moreover
note τ_xs_E2_t2''_in_Tr2 t2''Cv2_empty
moreover
have Adm: "(Adm 𝒱2 ρ2 Tr⇘ES2⇙ ((τ @ xs) ↿ E⇘ES2⇙) x)"
proof -
from τ_xs_E2_t2''_in_Tr2 validES2
have τ_xsE2_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv2_inter_Nv1 total_ES2_Cv2_inter_Nv1
have τ_xsE2_x_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] ∈ Tr⇘ES2⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2) = ((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA
ultimately obtain t2'
where res1: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2' ∈ Tr⇘ES2⇙"
and res2: "t2' ↿ V⇘𝒱2⇙ = t2'' ↿ V⇘𝒱2⇙"
and res3: "t2' ↿ C⇘𝒱2⇙ = []"
by (simp only: BSIA_def, blast)
have "set t2' ⊆ E⇘ES2⇙"
proof -
from res1 validES2
have "set (((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2') ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
proof -
from res1 xs_is_xsE2 have "((τ ↿ E⇘ES2⇙) @ (xs @ [x])) @ t2' ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t2''Vv2_is_t2Vv2 res2 have "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r1E2_in_Nv1_inter_C2_star] obtain t2'
where t2'_in_E2star: "set t2' ⊆ E⇘ES2⇙"
and τr1E2_t2'_in_Tr2: "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
and t2'_Vv2_is_t2_Vv2: "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2'_Cv2_empty: "t2' ↿ C⇘𝒱2⇙ = []"
by auto
have "t2' ↿ V⇘𝒱2⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
proof -
from projection_intersection_neutral[OF Cons(5), of "V⇘𝒱⇙"]
have "t2 ↿ V⇘𝒱⇙ = t2 ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp only: Int_commute)
with Cons(9) t2'_Vv2_is_t2_Vv2 v'_in_E2 show ?thesis
by (simp add: projection_def)
qed
from projection_split_first[OF this] obtain r2' s2'
where t2'_is_r2'_v'_s2': "t2' = r2' @ [𝒱'] @ s2'"
and r2'_Vv2_empty: "r2' ↿ V⇘𝒱2⇙ = []"
by auto
from t2'_is_r2'_v'_s2' t2'_Cv2_empty
have r2'_Cv2_empty: "r2' ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2'_is_r2'_v'_s2' t2'_Cv2_empty
have s2'_Cv2_empty: "s2' ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from t2'_in_E2star t2'_is_r2'_v'_s2'
have r2'_in_E2star: "set r2' ⊆ E⇘ES2⇙"
by auto
with r2'_Vv2_empty
have r2'_Vv_empty: "r2' ↿ V⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2 subset_iff_psubset_eq)
have r2'_in_Nv2star: "set r2' ⊆ N⇘𝒱2⇙"
proof -
note r2'_in_E2star
moreover
from r2'_Vv2_empty have "set r2' ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2'_Cv2_empty have "set r2' ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv2_inter_E1_empty have r2'E1_empty: "r2' ↿ E⇘ES1⇙ = []"
by (metis Int_commute empty_subsetI projection_on_subset2 r2'_Vv2_empty)
let ?tau = "τ @ r1 @ r2' @ [𝒱']"
from Cons(2) r1_in_E1star r2'_in_E2star v'_in_E1
have "set ?tau ⊆ (E⇘(ES1 ∥ ES2)⇙)"
by (simp add: composeES_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
note s1_in_E1star
moreover
from t2'_in_E2star t2'_is_r2'_v'_s2' have "set s2' ⊆ E⇘ES2⇙"
by simp
moreover
from r1_in_E1star v'_in_E1 r2'E1_empty τE1_r1_v'_s1_in_Tr1
have "?tau ↿ E⇘ES1⇙ @ s1 ∈ Tr⇘ES1⇙"
by (simp only: list_subset_iff_projection_neutral
projection_concatenation_commute projection_def, auto)
moreover
from τr1E2_t2'_in_Tr2 t2'_is_r2'_v'_s2' v'_in_E2
have "?tau ↿ E⇘ES2⇙ @ s2' ∈ Tr⇘ES2⇙"
proof -
from v'_in_E2 r2'_in_E2star
have "(τ @ r1 @ r2' @ [𝒱']) ↿ E⇘ES2⇙ = (τ @ r1) ↿ E⇘ES2⇙ @ r2' @ [𝒱']"
by (simp only: projection_concatenation_commute
list_subset_iff_projection_neutral projection_def, auto)
with τr1E2_t2'_in_Tr2 t2'_is_r2'_v'_s2' v'_in_E2 show ?thesis
by simp
qed
moreover
have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
proof -
from Cons(3,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from t1_is_r1_v'_s1 r1_Vv_empty v'_in_Vv1 Vv_is_Vv1_union_Vv2
have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (s1 ↿ V⇘𝒱⇙)"
by (simp only: t1_is_r1_v'_s1 projection_concatenation_commute projection_def, auto)
ultimately show ?thesis
by auto
qed
moreover
have "lambda' ↿ E⇘ES2⇙ = s2' ↿ V⇘𝒱⇙"
proof -
from Cons(4,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from t2'_is_r2'_v'_s2' r2'_Vv2_empty r2'_in_E2star v'_in_Vv2 propSepViews
have "t2' ↿ V⇘𝒱⇙ = [𝒱'] @ (s2' ↿ V⇘𝒱⇙)"
proof -
have "r2' ↿ V⇘𝒱⇙ =[]"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2
r2'_Vv2_empty r2'_in_E2star subset_iff_psubset_eq)
with t2'_is_r2'_v'_s2' v'_in_Vv2 Vv_is_Vv1_union_Vv2 show ?thesis
by (simp only: t2'_is_r2'_v'_s2' projection_concatenation_commute
projection_def, auto)
qed
moreover
have "t2 ↿ V⇘𝒱⇙ = t2' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute outerCons_prems(4)
projection_intersection_neutral
t2'_Vv2_is_t2_Vv2 t2'_in_E2star)
ultimately show ?thesis
by auto
qed
moreover
note s1_Cv1_empty s2'_Cv2_empty Cons.hyps[of ?tau s1 s2']
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ r2' @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r1_Vv_empty r2'_Vv_empty t'Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by(simp only: projection_concatenation_commute projection_def, auto)
moreover
from VIsViewOnE r1_Cv1_empty t'Cv_empty r2'_Cv2_empty v'_in_Vv
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from VIsViewOnE v'_in_Vv have "[𝒱'] ↿ C⇘𝒱⇙ = []"
by (simp add:isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def projection_def, auto)
moreover
from r1_in_E1star r1_Cv1_empty
have "r1 ↿ C⇘𝒱⇙ = []"
using propSepViews projection_on_subset2 unfolding properSeparationOfViews_def
by auto
moreover
from r2'_in_E2star r2'_Cv2_empty
have "r2' ↿ C⇘𝒱⇙ = []"
using propSepViews projection_on_subset2 unfolding properSeparationOfViews_def
by auto
moreover
note t'Cv_empty
ultimately show ?thesis
by (simp only: projection_concatenation_commute, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv1_minus_E2: "𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙"
by auto
with v'_in_Vv have v'_in_E1: "𝒱' ∈ E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def
by auto
from v'_in_Vv1_minus_E2 have v'_notin_E2: "𝒱' ∉ E⇘ES2⇙"
by (auto)
with validV2 have v'_notin_Vv2: "𝒱' ∉ V⇘𝒱2⇙"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
from Cons(3) Cons(4) Cons(8) v'_in_E1
have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1 have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙"
by auto
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq
Int_commute Int_empty_right disjoint_eq_subset_Compl
list_subset_iff_projection_neutral projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Diff_eq Int_commute Int_empty_right
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add:isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
qed
have r1E2_in_Nv1_inter_C2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) = set r1 ∩ E⇘ES2⇙"
by (simp add: projection_def, auto)
with r1_in_Nv1star have "set (r1 ↿ E⇘ES2⇙) ⊆ (E⇘ES2⇙ ∩ N⇘𝒱1⇙)"
by auto
moreover
from validV2 disjoint_Nv1_Vv2
have "E⇘ES2⇙ ∩ N⇘𝒱1⇙ = N⇘𝒱1⇙ ∩ C⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
note outerCons_prems = Cons.prems
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙) ⟹
∃ t2'. ( set t2' ⊆ E⇘ES2⇙
∧ ((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙
∧ t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙
∧ t2' ↿ C⇘𝒱2⇙ = [] )"
proof (induct "r1 ↿ E⇘ES2⇙" arbitrary: r1 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(10) outerCons_prems(4)
outerCons_prems(6) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE2: "xs = xs ↿ E⇘ES2⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES2⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES2⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by auto
with xs_is_xsE2 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t2''
where t2''_in_E2star: "set t2'' ⊆ E⇘ES2⇙"
and τ_xs_E2_t2''_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ t2'' ∈ Tr⇘ES2⇙"
and t2''Vv2_is_t2Vv2: "t2'' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2''Cv2_empty: "t2'' ↿ C⇘𝒱2⇙ = []"
by auto
have x_in_Cv2_inter_Nv1: "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv2: "x ∈ C⇘𝒱2⇙"
by auto
moreover
note τ_xs_E2_t2''_in_Tr2 t2''Cv2_empty
moreover
have Adm: "(Adm 𝒱2 ρ2 Tr⇘ES2⇙ ((τ @ xs) ↿ E⇘ES2⇙) x)"
proof -
from τ_xs_E2_t2''_in_Tr2 validES2
have τ_xsE2_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv2_inter_Nv1 total_ES2_Cv2_inter_Nv1
have τ_xsE2_x_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] ∈ Tr⇘ES2⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2) = ((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA
ultimately obtain t2'
where res1: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2' ∈ Tr⇘ES2⇙"
and res2: "t2' ↿ V⇘𝒱2⇙ = t2'' ↿ V⇘𝒱2⇙"
and res3: "t2' ↿ C⇘𝒱2⇙ = []"
by (simp only: BSIA_def, blast)
have "set t2' ⊆ E⇘ES2⇙"
proof -
from res1 validES2 have "set (((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2') ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
proof -
from res1 xs_is_xsE2 have "((τ ↿ E⇘ES2⇙) @ (xs @ [x])) @ t2' ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t2''Vv2_is_t2Vv2 res2 have "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r1E2_in_Nv1_inter_C2_star] obtain t2'
where t2'_in_E2star: "set t2' ⊆ E⇘ES2⇙"
and τr1E2_t2'_in_Tr2: "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
and t2'_Vv2_is_t2_Vv2: "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2'_Cv2_empty: "t2' ↿ C⇘𝒱2⇙ = []"
by auto
let ?tau = "τ @ r1 @ [𝒱']"
from v'_in_E1 Cons(2) r1_in_Nv1star validV1 have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(4) t1_is_r1_v'_s1 have "set s1 ⊆ E⇘ES1⇙"
by auto
moreover
note t2'_in_E2star
moreover
have "?tau ↿ E⇘ES1⇙ @ s1 ∈ Tr⇘ES1⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(3) Cons.prems(5)
projection_concatenation_commute t1_is_r1_v'_s1)
moreover
from τr1E2_t2'_in_Tr2 v'_notin_E2
have "?tau ↿ E⇘ES2⇙ @ t2' ∈ Tr⇘ES2⇙"
by (simp add: projection_def)
moreover
from Cons(8) t1_is_r1_v'_s1 r1_Vv_empty v'_in_E1 v'_in_Vv
have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(11) v'_notin_E2 t2'_Vv2_is_t2_Vv2
have "lambda' ↿ E⇘ES2⇙ = t2' ↿ V⇘𝒱⇙"
proof -
have "t2' ↿ V⇘𝒱⇙ = t2' ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral
t2'_in_E2star)
moreover
have "t2 ↿ V⇘𝒱⇙ = t2 ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def
projection_intersection_neutral Cons(5))
moreover
note Cons(9) v'_notin_E2 t2'_Vv2_is_t2_Vv2
ultimately show ?thesis
by (simp add: projection_def)
qed
moreover
note s1_Cv1_empty t2'_Cv2_empty
moreover
note Cons.hyps(1)[of ?tau s1 t2']
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r1_Vv_empty t'_Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r1 ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "E⇘ES1⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def by auto
from projection_on_subset[OF ‹E⇘ES1⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱1⇙› r1_Cv1_empty]
have "r1 ↿ (E⇘ES1⇙ ∩ C⇘𝒱⇙) = []"
by (simp only: Int_commute)
with projection_intersection_neutral[OF r1_in_E1star, of "C⇘𝒱⇙"] show ?thesis
by simp
qed
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add:isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
moreover {
assume v'_in_Vv2_minus_E1: "𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
hence v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv have v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
using propSepViews unfolding properSeparationOfViews_def
by auto
from v'_in_Vv2_minus_E1 have v'_notin_E1: "𝒱' ∉ E⇘ES1⇙"
by (auto)
with validV1 have v'_notin_Vv1: "𝒱' ∉ V⇘𝒱1⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
from Cons(4) Cons(5) Cons(9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
by auto
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
qed
with Nv2_inter_E1_empty have r2E1_empty: "r2 ↿ E⇘ES1⇙ = []"
by (metis Int_commute empty_subsetI projection_on_subset2 r2_Vv2_empty)
let ?tau = "τ @ r2 @ [𝒱']"
from v'_in_E2 Cons(2) r2_in_Nv2star validV2 have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
note Cons(4)
moreover
from Cons(5) t2_is_r2_v'_s2 have "set s2 ⊆ E⇘ES2⇙"
by auto
moreover
have "?tau ↿ E⇘ES1⇙ @ t1 ∈ Tr⇘ES1⇙"
proof -
from v'_notin_E1 have "[𝒱'] ↿ E⇘ES1⇙ = []"
by (simp add: projection_def)
with Cons(6) Cons(3) t2_is_r2_v'_s2 v'_notin_E1
r2_in_Nv2star Nv2_inter_E1_empty r2E1_empty
show ?thesis
by (simp only: t2_is_r2_v'_s2 list_subset_iff_projection_neutral
projection_concatenation_commute, auto)
qed
moreover
have "?tau ↿ E⇘ES2⇙ @ s2 ∈ Tr⇘ES2⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(4) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(4) Cons.prems(6)
projection_concatenation_commute t2_is_r2_v'_s2)
moreover
from Cons(8) v'_notin_E1 have "lambda' ↿ E⇘ES1⇙ = t1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(9) t2_is_r2_v'_s2 r2_Vv_empty v'_in_E2 v'_in_Vv
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
note Cons(10) s2_Cv2_empty
moreover
note Cons.hyps(1)[of ?tau t1 s2]
ultimately obtain t'
where tau_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ [𝒱'] @ t'"
note tau_t'_in_Tr
moreover
from r2_Vv_empty t'_Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r2 ↿ C⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2
r2_Cv2_empty r2_in_E2star)
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
ultimately show ?thesis
by blast
qed
qed
}
thus ?thesis
by auto
qed
lemma generalized_zipping_lemma4:
"⟦ ∇⇘Γ1⇙ ⊆ E⇘ES1⇙; Δ⇘Γ1⇙ ⊆ E⇘ES1⇙; Υ⇘Γ1⇙ ⊆ E⇘ES1⇙; ∇⇘Γ2⇙ ⊆ E⇘ES2⇙; Δ⇘Γ2⇙ ⊆ E⇘ES2⇙; Υ⇘Γ2⇙ ⊆ E⇘ES2⇙;
BSIA ρ1 𝒱1 Tr⇘ES1⇙; BSIA ρ2 𝒱2 Tr⇘ES2⇙; total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙); total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙);
FCIA ρ1 Γ1 𝒱1 Tr⇘ES1⇙; FCIA ρ2 Γ2 𝒱2 Tr⇘ES2⇙; V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ⊆ ∇⇘Γ1⇙ ∪ ∇⇘Γ2⇙;
C⇘𝒱1⇙ ∩ N⇘𝒱2⇙ ⊆ Υ⇘Γ1⇙; C⇘𝒱2⇙ ∩ N⇘𝒱1⇙ ⊆ Υ⇘Γ2⇙;
N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ E⇘ES2⇙ = {}; N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ E⇘ES1⇙ = {} ⟧ ⟹
∀ τ lambda t1 t2. ( ( set τ ⊆ (E⇘(ES1 ∥ ES2)⇙) ∧ set lambda ⊆ V⇘𝒱⇙ ∧ set t1 ⊆ E⇘ES1⇙
∧ set t2 ⊆ E⇘ES2⇙ ∧ ((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙ ∧ ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙
∧ (lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙) ∧ (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)
∧ (t1 ↿ C⇘𝒱1⇙) = [] ∧ (t2 ↿ C⇘𝒱2⇙) = [])
⟶ (∃t. ((τ @ t) ∈ (Tr⇘(ES1 ∥ ES2)⇙) ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = [])) )"
proof -
assume Nabla1_subsetof_E1: "∇⇘Γ1⇙ ⊆ E⇘ES1⇙"
and Delta1_subsetof_E1: "Δ⇘Γ1⇙ ⊆ E⇘ES1⇙"
and Upsilon1_subsetof_E1: "Υ⇘Γ1⇙ ⊆ E⇘ES1⇙"
and Nabla2_subsetof_E2: "∇⇘Γ2⇙ ⊆ E⇘ES2⇙"
and Delta2_subsetof_E2: "Δ⇘Γ2⇙ ⊆ E⇘ES2⇙"
and Upsilon2_subsetof_E2: "Υ⇘Γ2⇙ ⊆ E⇘ES2⇙"
and BSIA1: "BSIA ρ1 𝒱1 Tr⇘ES1⇙"
and BSIA2: "BSIA ρ2 𝒱2 Tr⇘ES2⇙"
and ES1_total_Cv1_inter_Nv2: "total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙)"
and ES2_total_Cv2_inter_Nv1: "total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙)"
and FCIA1: "FCIA ρ1 Γ1 𝒱1 Tr⇘ES1⇙"
and FCIA2: "FCIA ρ2 Γ2 𝒱2 Tr⇘ES2⇙"
and Vv1_inter_Vv2_subsetof_Nabla1_union_Nabla2: "V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ⊆ ∇⇘Γ1⇙ ∪ ∇⇘Γ2⇙"
and Cv1_inter_Nv2_subsetof_Upsilon1: "C⇘𝒱1⇙ ∩ N⇘𝒱2⇙ ⊆ Υ⇘Γ1⇙"
and Cv2_inter_Nv1_subsetof_Upsilon2: "C⇘𝒱2⇙ ∩ N⇘𝒱1⇙ ⊆ Υ⇘Γ2⇙"
and disjoint_Nv1_inter_Delta1_inter_E2: "N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ E⇘ES2⇙ = {}"
and disjoint_Nv2_inter_Delta2_inter_E1: "N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ E⇘ES1⇙ = {}"
{
fix τ lambda t1 t2
have "⟦ set τ ⊆ (E⇘(ES1 ∥ ES2)⇙);
set lambda ⊆ V⇘𝒱⇙;
set t1 ⊆ E⇘ES1⇙;
set t2 ⊆ E⇘ES2⇙;
((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙;
((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙;
(lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙);
(lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙);
(t1 ↿ C⇘𝒱1⇙) = [];
(t2 ↿ C⇘𝒱2⇙) = [] ⟧
⟹ (∃ t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = []))"
proof (induct lambda arbitrary: τ t1 t2)
case (Nil τ t1 t2)
have "(τ @ []) ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
have "τ ∈ Tr⇘(ES1 ∥ ES2)⇙"
proof -
from Nil(5) validES1 have "τ ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
from Nil(6) validES2 have "τ ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
moreover
note Nil(1)
ultimately show ?thesis
by (simp add: composeES_def)
qed
thus ?thesis
by auto
qed
moreover
have "([] ↿ V⇘𝒱⇙) = []"
by (simp add: projection_def)
moreover
have "([] ↿ C⇘𝒱⇙) = []"
by (simp add: projection_def)
ultimately show ?case
by blast
next
case (Cons 𝒱' lambda' τ t1 t2)
thus ?case
proof -
from Cons(3) have v'_in_Vv: "𝒱' ∈ V⇘𝒱⇙"
by auto
have "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∩ ∇⇘Γ1⇙
∨ 𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∩ ∇⇘Γ2⇙
∨ 𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙
∨ 𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
proof -
let ?S = "V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∪ ( V⇘𝒱1⇙ - V⇘𝒱2⇙ ) ∪ ( V⇘𝒱2⇙ - V⇘𝒱1⇙ )"
have "V⇘𝒱1⇙ ∪ V⇘𝒱2⇙ = ?S"
by auto
moreover
have "V⇘𝒱1⇙ - V⇘𝒱2⇙ = V⇘𝒱1⇙ - E⇘ES2⇙"
and "V⇘𝒱2⇙ - V⇘𝒱1⇙ = V⇘𝒱2⇙ - E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def by auto
moreover
note Vv1_inter_Vv2_subsetof_Nabla1_union_Nabla2
Vv_is_Vv1_union_Vv2 v'_in_Vv
ultimately show ?thesis
by auto
qed
moreover
{
assume v'_in_Vv1_inter_Vv2_inter_Nabla1: "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∩ ∇⇘Γ1⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙" and v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
and v'_in_Nabla2: "𝒱' ∈ ∇⇘Γ1⇙"
by auto
with v'_in_Vv
have v'_in_E1: "𝒱' ∈ E⇘ES1⇙" and v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
using propSepViews unfolding properSeparationOfViews_def by auto
from Cons(3-4) Cons(8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1
have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙" and s1_in_E1star: "set s1 ⊆ E⇘ES1⇙"
by auto
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r1E2_in_Nv1_inter_C2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) = set r1 ∩ E⇘ES2⇙"
by (simp add: projection_def, auto)
with r1_in_Nv1star have "set (r1 ↿ E⇘ES2⇙) ⊆ (E⇘ES2⇙ ∩ N⇘𝒱1⇙)"
by auto
moreover
from validV2 disjoint_Nv1_Vv2
have "E⇘ES2⇙ ∩ N⇘𝒱1⇙ = N⇘𝒱1⇙ ∩ C⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv2_inter_Nv1_subsetof_Upsilon2
have r1E2_in_Nv1_inter_C2_Upsilon2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by auto
note outerCons_prems = Cons.prems
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙) ⟹
∃ t2'. ( set t2' ⊆ E⇘ES2⇙
∧ ((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙
∧ t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙
∧ t2' ↿ C⇘𝒱2⇙ = [] )"
proof (induct "r1 ↿ E⇘ES2⇙" arbitrary: r1 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(10)
outerCons_prems(4) outerCons_prems(6) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE2: "xs = xs ↿ E⇘ES2⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES2⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES2⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by auto
with xs_is_xsE2 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t2''
where t2''_in_E2star: "set t2'' ⊆ E⇘ES2⇙"
and τ_xs_E2_t2''_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ t2'' ∈ Tr⇘ES2⇙"
and t2''Vv2_is_t2Vv2: "t2'' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2''Cv2_empty: "t2'' ↿ C⇘𝒱2⇙ = []"
by auto
have x_in_Cv2_inter_Nv1: "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv2: "x ∈ C⇘𝒱2⇙"
by auto
moreover
note τ_xs_E2_t2''_in_Tr2 t2''Cv2_empty
moreover
have Adm: "(Adm 𝒱2 ρ2 Tr⇘ES2⇙ ((τ @ xs) ↿ E⇘ES2⇙) x)"
proof -
from τ_xs_E2_t2''_in_Tr2 validES2
have τ_xsE2_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv2_inter_Nv1 ES2_total_Cv2_inter_Nv1
have τ_xsE2_x_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] ∈ Tr⇘ES2⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2) = ((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA2
ultimately obtain t2'
where res1: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2' ∈ Tr⇘ES2⇙"
and res2: "t2' ↿ V⇘𝒱2⇙ = t2'' ↿ V⇘𝒱2⇙"
and res3: "t2' ↿ C⇘𝒱2⇙ = []"
by (simp only: BSIA_def, blast)
have "set t2' ⊆ E⇘ES2⇙"
proof -
from res1 validES2 have "set (((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2') ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
proof -
from res1 xs_is_xsE2 have "((τ ↿ E⇘ES2⇙) @ (xs @ [x])) @ t2' ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t2''Vv2_is_t2Vv2 res2 have "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r1E2_in_Nv1_inter_C2_star] obtain t2'
where t2'_in_E2star: "set t2' ⊆ E⇘ES2⇙"
and τr1E2_t2'_in_Tr2: "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
and t2'_Vv2_is_t2_Vv2: "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2'_Cv2_empty: "t2' ↿ C⇘𝒱2⇙ = []"
by auto
have "t2' ↿ V⇘𝒱2⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
proof -
from projection_intersection_neutral[OF Cons(5), of "V⇘𝒱⇙"]
have "t2 ↿ V⇘𝒱⇙ = t2 ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp only: Int_commute)
with Cons(9) t2'_Vv2_is_t2_Vv2 v'_in_E2 show ?thesis
by (simp add: projection_def)
qed
from projection_split_first[OF this] obtain r2' s2'
where t2'_is_r2'_v'_s2': "t2' = r2' @ [𝒱'] @ s2'"
and r2'_Vv2_empty: "r2' ↿ V⇘𝒱2⇙ = []"
by auto
from t2'_is_r2'_v'_s2' t2'_Cv2_empty have r2'_Cv2_empty: "r2' ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2'_is_r2'_v'_s2' t2'_Cv2_empty have s2'_Cv2_empty: "s2' ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from t2'_in_E2star t2'_is_r2'_v'_s2' have r2'_in_E2star: "set r2' ⊆ E⇘ES2⇙"
by auto
have r2'_in_Nv2star: "set r2' ⊆ N⇘𝒱2⇙"
proof -
note r2'_in_E2star
moreover
from r2'_Vv2_empty have "set r2' ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2'_Cv2_empty have "set r2' ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r2'E1_in_Nv2_inter_C1_star: "set (r2' ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2' ↿ E⇘ES1⇙) = set r2' ∩ E⇘ES1⇙"
by (simp add: projection_def, auto)
with r2'_in_Nv2star have "set (r2' ↿ E⇘ES1⇙) ⊆ (E⇘ES1⇙ ∩ N⇘𝒱2⇙)"
by auto
moreover
from validV1 disjoint_Nv2_Vv1
have "E⇘ES1⇙ ∩ N⇘𝒱2⇙ = N⇘𝒱2⇙ ∩ C⇘𝒱1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv1_inter_Nv2_subsetof_Upsilon1
have r2'E1_in_Nv2_inter_Cv1_Upsilon1_star:
"set (r2' ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by auto
have "set (r2' ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) ⟹
∃ s1' q1'. (
set s1' ⊆ E⇘ES1⇙ ∧ set q1' ⊆ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙
∧ (τ ↿ E⇘ES1⇙) @ r1 @ q1' @ [𝒱'] @ s1' ∈ Tr⇘ES1⇙
∧ q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = r2' ↿ E⇘ES1⇙
∧ s1' ↿ V⇘𝒱1⇙ = s1 ↿ V⇘𝒱1⇙
∧ s1' ↿ C⇘𝒱1⇙ = [])"
proof (induct "r2' ↿ E⇘ES1⇙" arbitrary: r2' rule: rev_induct)
case Nil
note s1_in_E1star
moreover
have "set [] ⊆ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙"
by auto
moreover
from outerCons_prems(5) t1_is_r1_v'_s1
have "τ ↿ E⇘ES1⇙ @ r1 @ [] @ [𝒱'] @ s1 ∈ Tr⇘ES1⇙"
by auto
moreover
from Nil have "[] ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = r2' ↿ E⇘ES1⇙"
by (simp add: projection_def)
moreover
have "s1 ↿ V⇘𝒱1⇙ = s1 ↿ V⇘𝒱1⇙"..
moreover
note s1_Cv1_empty
ultimately show ?case
by blast
next
case (snoc x xs)
have xs_is_xsE1: "xs = xs ↿ E⇘ES1⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES1⇙"
by (simp add: projection_def, auto)
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES1⇙) ⊆ N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙"
by simp
with xs_is_xsE1 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain s1'' q1''
where s1''_in_E1star: "set s1'' ⊆ E⇘ES1⇙"
and q1''_in_C1_inter_Upsilon1_inter_Delta1: "set q1'' ⊆ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙"
and τE1_r1_q1''_v'_s1''_in_Tr1: "(τ ↿ E⇘ES1⇙ @ r1 @ q1'') @ [𝒱'] @ s1'' ∈ Tr⇘ES1⇙"
and q1''C1_Upsilon1_is_xsE1: "q1'' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = xs ↿ E⇘ES1⇙"
and s1''V1_is_s1V1: "s1'' ↿ V⇘𝒱1⇙ = s1 ↿ V⇘𝒱1⇙"
and s1''C1_empty: "s1'' ↿ C⇘𝒱1⇙ = []"
by auto
have x_in_Cv1_inter_Upsilon1: "x ∈ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙"
and x_in_Cv1_inter_Nv2: "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by simp
thus "x ∈ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙"
and "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
by auto
qed
with validV1 have x_in_E1: "x ∈ E⇘ES1⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
note x_in_Cv1_inter_Upsilon1
moreover
from v'_in_Vv1_inter_Vv2_inter_Nabla1 have "𝒱' ∈ V⇘𝒱1⇙ ∩ ∇⇘Γ1⇙"
by auto
moreover
note τE1_r1_q1''_v'_s1''_in_Tr1 s1''C1_empty
moreover
have Adm: "(Adm 𝒱1 ρ1 Tr⇘ES1⇙ (τ ↿ E⇘ES1⇙ @ r1 @ q1'') x)"
proof -
from τE1_r1_q1''_v'_s1''_in_Tr1 validES1
have "(τ ↿ E⇘ES1⇙ @ r1 @ q1'') ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv1_inter_Nv2 ES1_total_Cv1_inter_Nv2
have "(τ ↿ E⇘ES1⇙ @ r1 @ q1'') @ [x] ∈ Tr⇘ES1⇙"
by (simp only: total_def)
moreover
have "(τ ↿ E⇘ES1⇙ @ r1 @ q1'') ↿ (ρ1 𝒱1) = (τ ↿ E⇘ES1⇙ @ r1 @ q1'') ↿ (ρ1 𝒱1)" ..
ultimately show ?thesis
by (simp only: Adm_def, blast)
qed
moreover
note FCIA1
ultimately
obtain s1' γ'
where res1: "(set γ') ⊆ (N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙)"
and res2: "((τ ↿ E⇘ES1⇙ @ r1 @ q1'') @ [x] @ γ' @ [𝒱'] @ s1') ∈ Tr⇘ES1⇙"
and res3: "(s1' ↿ V⇘𝒱1⇙) = (s1'' ↿ V⇘𝒱1⇙)"
and res4: "s1' ↿ C⇘𝒱1⇙ = []"
unfolding FCIA_def
by blast
let ?q1' = "q1'' @ [x] @ γ'"
from res2 validES1 have "set s1' ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
moreover
from res1 x_in_Cv1_inter_Upsilon1 q1''_in_C1_inter_Upsilon1_inter_Delta1
have "set ?q1' ⊆ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙"
by auto
moreover
from res2 have "τ ↿ E⇘ES1⇙ @ r1 @ ?q1' @ [𝒱'] @ s1' ∈ Tr⇘ES1⇙"
by auto
moreover
have "?q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = r2' ↿ E⇘ES1⇙"
proof -
from validV1 res1 have "γ' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = []"
proof -
from res1 have "γ' = γ' ↿ (N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙)"
by (simp only: list_subset_iff_projection_neutral)
hence "γ' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = γ' ↿ (N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by simp
hence "γ' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = γ' ↿ (N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by (simp only: projection_def, auto)
moreover
from validV1 have "N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ = {}"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by (simp add: projection_def)
qed
hence "?q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = (q1'' @ [x]) ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by (simp only: projection_concatenation_commute, auto)
with q1''C1_Upsilon1_is_xsE1 x_in_Cv1_inter_Upsilon1
have "?q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = (xs ↿ E⇘ES1⇙) @ [x]"
by (simp only: projection_concatenation_commute projection_def, auto)
with xs_is_xsE1 snoc(2) show ?thesis
by simp
qed
moreover
from res3 s1''V1_is_s1V1 have "s1' ↿ V⇘𝒱1⇙ = s1 ↿ V⇘𝒱1⇙"
by simp
moreover
note res4
ultimately show ?case
by blast
qed
from this[OF r2'E1_in_Nv2_inter_Cv1_Upsilon1_star] obtain s1' q1'
where s1'_in_E1star: "set s1' ⊆ E⇘ES1⇙"
and q1'_in_Cv1_inter_Upsilon1_union_Nv1_inter_Delta1:
"set q1' ⊆ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙"
and τE1_r1_q1'_v'_s1'_in_Tr1: "(τ ↿ E⇘ES1⇙) @ r1 @ q1' @ [𝒱'] @ s1' ∈ Tr⇘ES1⇙"
and q1'Cv1_inter_Upsilon1_is_r2'E1: "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) = r2' ↿ E⇘ES1⇙"
and s1'Vv1_is_s1_Vv1: "s1' ↿ V⇘𝒱1⇙ = s1 ↿ V⇘𝒱1⇙"
and s1'Cv1_empty: "s1' ↿ C⇘𝒱1⇙ = []"
by auto
from q1'_in_Cv1_inter_Upsilon1_union_Nv1_inter_Delta1 validV1
have q1'_in_E1star: "set q1' ⊆ E⇘ES1⇙"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
have r2'Cv_empty: "r2' ↿ C⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2
r2'_Cv2_empty r2'_in_E2star)
from validES1 τE1_r1_q1'_v'_s1'_in_Tr1
have q1'_in_E1star: "set q1' ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
moreover
note r2'_in_E2star
moreover
have q1'E2_is_r2'E1: "q1' ↿ E⇘ES2⇙ = r2' ↿ E⇘ES1⇙"
proof -
from q1'_in_Cv1_inter_Upsilon1_union_Nv1_inter_Delta1
have "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) = q1'"
by (simp add: list_subset_iff_projection_neutral)
hence "(q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙)) ↿ E⇘ES2⇙ = q1' ↿ E⇘ES2⇙"
by simp
hence "q1' ↿ ((C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ∩ E⇘ES2⇙) = q1' ↿ E⇘ES2⇙"
by (simp add: projection_def)
hence "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∩ E⇘ES2⇙) = q1' ↿ E⇘ES2⇙"
by (simp only: Int_Un_distrib2 disjoint_Nv1_inter_Delta1_inter_E2, auto)
moreover
from q1'Cv1_inter_Upsilon1_is_r2'E1
have "(q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)) ↿ E⇘ES2⇙ = (r2' ↿ E⇘ES1⇙) ↿ E⇘ES2⇙"
by simp
hence "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∩ E⇘ES2⇙) = (r2' ↿ E⇘ES2⇙) ↿ E⇘ES1⇙"
by (simp add: projection_def conj_commute)
with r2'_in_E2star have "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∩ E⇘ES2⇙) = r2' ↿ E⇘ES1⇙"
by (simp only: list_subset_iff_projection_neutral)
ultimately show ?thesis
by auto
qed
moreover
have "q1' ↿ V⇘𝒱⇙ = []"
proof -
from q1'_in_Cv1_inter_Upsilon1_union_Nv1_inter_Delta1
have "q1' = q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙)"
by (simp add: list_subset_iff_projection_neutral)
moreover
from q1'_in_E1star have "q1' = q1' ↿ E⇘ES1⇙"
by (simp add: list_subset_iff_projection_neutral)
ultimately have "q1' = q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ E⇘ES1⇙"
by simp
hence "q1' ↿ V⇘𝒱⇙ = q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ E⇘ES1⇙ ↿ V⇘𝒱⇙"
by simp
hence "q1' ↿ V⇘𝒱⇙ = q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ (V⇘𝒱⇙ ∩ E⇘ES1⇙)"
by (simp add: Int_commute projection_def)
hence "q1' ↿ V⇘𝒱⇙ = q1' ↿ ((C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ∩ V⇘𝒱1⇙)"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def)
hence "q1' ↿ V⇘𝒱⇙ = q1' ↿ (V⇘𝒱1⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ V⇘𝒱1⇙ ∩ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙)"
by (simp add: Int_Un_distrib2, metis Int_assoc Int_commute Int_left_commute Un_commute)
with validV1 show ?thesis
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto, simp add: projection_def)
qed
moreover
have "r2' ↿ V⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute projection_intersection_neutral
r2'_Vv2_empty r2'_in_E2star)
moreover
have q1'Cv_empty: "q1' ↿ C⇘𝒱⇙ = []"
proof -
from q1'_in_E1star have foo: "q1' = q1' ↿ E⇘ES1⇙"
by (simp add: list_subset_iff_projection_neutral)
hence "q1' ↿ C⇘𝒱⇙ = q1' ↿ (C⇘𝒱⇙ ∩ E⇘ES1⇙)"
by (metis Int_commute list_subset_iff_projection_neutral projection_intersection_neutral)
moreover
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES1⇙⊆C⇘𝒱1⇙"
unfolding properSeparationOfViews_def by auto
from projection_subset_elim[OF ‹C⇘𝒱⇙ ∩ E⇘ES1⇙⊆C⇘𝒱1⇙›, of q1']
have "q1' ↿ C⇘𝒱1⇙ ↿ C⇘𝒱⇙ ↿ E⇘ES1⇙ = q1' ↿ (C⇘𝒱⇙ ∩ E⇘ES1⇙)"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def)
hence "q1' ↿ E⇘ES1⇙ ↿ C⇘𝒱1⇙ ↿ C⇘𝒱⇙ = q1' ↿ (C⇘𝒱⇙ ∩ E⇘ES1⇙)"
by (simp add: projection_commute)
with foo have "q1' ↿ (C⇘𝒱1⇙ ∩ C⇘𝒱⇙) = q1' ↿ (C⇘𝒱⇙ ∩ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from q1'_in_Cv1_inter_Upsilon1_union_Nv1_inter_Delta1
have "q1' ↿ (C⇘𝒱1⇙ ∩ C⇘𝒱⇙) = q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ (C⇘𝒱1⇙ ∩ C⇘𝒱⇙)"
by (simp add: list_subset_iff_projection_neutral)
moreover
have "(C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ∩ (C⇘𝒱1⇙ ∩ C⇘𝒱⇙)
= (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ C⇘𝒱1⇙ ∩ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ∩ C⇘𝒱⇙"
by fast
hence "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ (C⇘𝒱1⇙ ∩ C⇘𝒱⇙)
= q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ C⇘𝒱1⇙ ∩ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ C⇘𝒱⇙"
by (simp add: projection_sequence)
moreover
from validV1
have "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙ ∪ C⇘𝒱1⇙ ∩ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙) ↿ C⇘𝒱⇙
= q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) ↿ C⇘𝒱⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def Int_commute)
moreover
from q1'Cv1_inter_Upsilon1_is_r2'E1
have "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) ↿ C⇘𝒱⇙ = r2' ↿ E⇘ES1⇙ ↿ C⇘𝒱⇙"
by simp
with projection_on_intersection[OF r2'Cv_empty]
have "q1' ↿ (C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙) ↿ C⇘𝒱⇙ = []"
by (simp add: Int_commute projection_def)
ultimately show ?thesis
by auto
qed
moreover
note r2'Cv_empty merge_property'[of q1' r2']
ultimately obtain q'
where q'E1_is_q1': "q' ↿ E⇘ES1⇙ = q1'"
and q'E2_is_r2': "q' ↿ E⇘ES2⇙ = r2'"
and q'V_empty: "q' ↿ V⇘𝒱⇙ = []"
and q'C_empty: "q' ↿ C⇘𝒱⇙ = []"
and q'_in_E1_union_E2_star: "set q' ⊆ (E⇘ES1⇙ ∪ E⇘ES2⇙)"
unfolding Let_def
by auto
let ?tau = "τ @ r1 @ q' @ [𝒱']"
from Cons(2) r1_in_E1star q'_in_E1_union_E2_star v'_in_E1
have "set ?tau ⊆ (E⇘(ES1 ∥ ES2)⇙)"
by (simp add: composeES_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
note s1'_in_E1star
moreover
from t2'_in_E2star t2'_is_r2'_v'_s2' have "set s2' ⊆ E⇘ES2⇙"
by simp
moreover
from q'E1_is_q1' r1_in_E1star v'_in_E1 q1'_in_E1star τE1_r1_q1'_v'_s1'_in_Tr1
have "?tau ↿ E⇘ES1⇙ @ s1' ∈ Tr⇘ES1⇙"
by (simp only: list_subset_iff_projection_neutral
projection_concatenation_commute projection_def, auto)
moreover
from τr1E2_t2'_in_Tr2 t2'_is_r2'_v'_s2' v'_in_E2 q'E2_is_r2'
have "?tau ↿ E⇘ES2⇙ @ s2' ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute projection_def, auto)
moreover
have "lambda' ↿ E⇘ES1⇙ = s1' ↿ V⇘𝒱⇙"
proof -
from Cons(3-4) Cons(8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from t1_is_r1_v'_s1 r1_Vv_empty v'_in_Vv1 Vv_is_Vv1_union_Vv2
have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (s1 ↿ V⇘𝒱⇙)"
by (simp only: t1_is_r1_v'_s1 projection_concatenation_commute
projection_def, auto)
moreover
have "s1 ↿ V⇘𝒱⇙ = s1' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute projection_intersection_neutral
s1'Vv1_is_s1_Vv1 s1'_in_E1star s1_in_E1star)
ultimately show ?thesis
by auto
qed
moreover
have "lambda' ↿ E⇘ES2⇙ = s2' ↿ V⇘𝒱⇙"
proof -
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from t2'_is_r2'_v'_s2' r2'_Vv2_empty r2'_in_E2star v'_in_Vv2 propSepViews
have "t2' ↿ V⇘𝒱⇙ = [𝒱'] @ (s2' ↿ V⇘𝒱⇙)"
proof -
have "r2' ↿ V⇘𝒱⇙ =[]"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2 r2'_Vv2_empty
r2'_in_E2star subset_iff_psubset_eq)
with t2'_is_r2'_v'_s2' v'_in_Vv2 Vv_is_Vv1_union_Vv2 show ?thesis
by (simp only: t2'_is_r2'_v'_s2'
projection_concatenation_commute projection_def, auto)
qed
moreover
have "t2 ↿ V⇘𝒱⇙ = t2' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute outerCons_prems(4)
projection_intersection_neutral t2'_Vv2_is_t2_Vv2 t2'_in_E2star)
ultimately show ?thesis
by auto
qed
moreover
note s1'Cv1_empty s2'_Cv2_empty Cons.hyps[of ?tau s1' s2']
ultimately obtain t'
where τ_r1_q'_v'_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ q' @ [𝒱'] @ t'"
note τ_r1_q'_v'_t'_in_Tr
moreover
from r1_Vv_empty q'V_empty t'Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by(simp only: projection_concatenation_commute projection_def, auto)
moreover
from VIsViewOnE r1_Cv1_empty t'Cv_empty q'C_empty v'_in_Vv
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from VIsViewOnE v'_in_Vv have "[𝒱'] ↿ C⇘𝒱⇙ = []"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def projection_def, auto)
moreover
from r1_in_E1star r1_Cv1_empty
have "r1 ↿ C⇘𝒱⇙ = []"
using propSepViews projection_on_subset2
unfolding properSeparationOfViews_def by auto
moreover
note t'Cv_empty q'C_empty
ultimately show ?thesis
by (simp only: projection_concatenation_commute, auto)
qed
ultimately have ?thesis
by auto
}
moreover
{
assume v'_in_Vv1_inter_Vv2_inter_Nabla2: "𝒱' ∈ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ∩ ∇⇘Γ2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙" and v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
and v'_in_Nabla2: "𝒱' ∈ ∇⇘Γ2⇙"
by auto
with v'_in_Vv propSepViews
have v'_in_E1: "𝒱' ∈ E⇘ES1⇙" and v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def by auto
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
and s2_in_E2star: "set s2 ⊆ E⇘ES2⇙"
by auto
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r2E1_in_Nv2_inter_C1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) = set r2 ∩ E⇘ES1⇙"
by (simp add: projection_def, auto)
with r2_in_Nv2star have "set (r2 ↿ E⇘ES1⇙) ⊆ (E⇘ES1⇙ ∩ N⇘𝒱2⇙)"
by auto
moreover
from validV1 disjoint_Nv2_Vv1 propSepViews
have "E⇘ES1⇙ ∩ N⇘𝒱2⇙ = N⇘𝒱2⇙ ∩ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv1_inter_Nv2_subsetof_Upsilon1
have r2E1_in_Nv2_inter_C1_Upsilon1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by auto
note outerCons_prems = Cons.prems
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙) ⟹
∃ t1'. ( set t1' ⊆ E⇘ES1⇙
∧ ((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙
∧ t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙
∧ t1' ↿ C⇘𝒱1⇙ = [] )"
proof (induct "r2 ↿ E⇘ES1⇙" arbitrary: r2 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(9) outerCons_prems(3)
outerCons_prems(5) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE1: "xs = xs ↿ E⇘ES1⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES1⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES1⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by auto
with xs_is_xsE1 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t1''
where t1''_in_E1star: "set t1'' ⊆ E⇘ES1⇙"
and τ_xs_E1_t1''_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ t1'' ∈ Tr⇘ES1⇙"
and t1''Vv1_is_t1Vv1: "t1'' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1''Cv1_empty: "t1'' ↿ C⇘𝒱1⇙ = []"
by auto
have x_in_Cv1_inter_Nv2: "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv1: "x ∈ C⇘𝒱1⇙"
by auto
moreover
note τ_xs_E1_t1''_in_Tr1 t1''Cv1_empty
moreover
have Adm: "(Adm 𝒱1 ρ1 Tr⇘ES1⇙ ((τ @ xs) ↿ E⇘ES1⇙) x)"
proof -
from τ_xs_E1_t1''_in_Tr1 validES1
have τ_xsE1_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv1_inter_Nv2 ES1_total_Cv1_inter_Nv2
have τ_xsE1_x_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] ∈ Tr⇘ES1⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1) = ((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA1
ultimately obtain t1'
where res1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1' ∈ Tr⇘ES1⇙"
and res2: "t1' ↿ V⇘𝒱1⇙ = t1'' ↿ V⇘𝒱1⇙"
and res3: "t1' ↿ C⇘𝒱1⇙ = []"
by (simp only: BSIA_def, blast)
have "set t1' ⊆ E⇘ES1⇙"
proof -
from res1 validES1 have "set (((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1') ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
proof -
from res1 xs_is_xsE1 have "((τ ↿ E⇘ES1⇙) @ (xs @ [x])) @ t1' ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t1''Vv1_is_t1Vv1 res2 have "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r2E1_in_Nv2_inter_C1_star] obtain t1'
where t1'_in_E1star: "set t1' ⊆ E⇘ES1⇙"
and τr2E1_t1'_in_Tr1: "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
and t1'_Vv1_is_t1_Vv1: "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1'_Cv1_empty: "t1' ↿ C⇘𝒱1⇙ = []"
by auto
have "t1' ↿ V⇘𝒱1⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
proof -
from projection_intersection_neutral[OF Cons(4), of "V⇘𝒱⇙"] propSepViews
have "t1 ↿ V⇘𝒱⇙ = t1 ↿ V⇘𝒱1⇙"
unfolding properSeparationOfViews_def
by (simp only: Int_commute)
with Cons(8) t1'_Vv1_is_t1_Vv1 v'_in_E1 show ?thesis
by (simp add: projection_def)
qed
from projection_split_first[OF this] obtain r1' s1'
where t1'_is_r1'_v'_s1': "t1' = r1' @ [𝒱'] @ s1'"
and r1'_Vv1_empty: "r1' ↿ V⇘𝒱1⇙ = []"
by auto
from t1'_is_r1'_v'_s1' t1'_Cv1_empty have r1'_Cv1_empty: "r1' ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1'_is_r1'_v'_s1' t1'_Cv1_empty have s1'_Cv1_empty: "s1' ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from t1'_in_E1star t1'_is_r1'_v'_s1' have r1'_in_E1star: "set r1' ⊆ E⇘ES1⇙"
by auto
have r1'_in_Nv1star: "set r1' ⊆ N⇘𝒱1⇙"
proof -
note r1'_in_E1star
moreover
from r1'_Vv1_empty have "set r1' ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r1'_Cv1_empty have "set r1' ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r1'E2_in_Nv1_inter_C2_star: "set (r1' ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1' ↿ E⇘ES2⇙) = set r1' ∩ E⇘ES2⇙"
by (simp add: projection_def, auto)
with r1'_in_Nv1star have "set (r1' ↿ E⇘ES2⇙) ⊆ (E⇘ES2⇙ ∩ N⇘𝒱1⇙)"
by auto
moreover
from validV2 propSepViews disjoint_Nv1_Vv2
have "E⇘ES2⇙ ∩ N⇘𝒱1⇙ = N⇘𝒱1⇙ ∩ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv2_inter_Nv1_subsetof_Upsilon2
have r1'E2_in_Nv1_inter_Cv2_Upsilon2_star:
"set (r1' ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by auto
have "set (r1' ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) ⟹
∃ s2' q2'. (
set s2' ⊆ E⇘ES2⇙ ∧ set q2' ⊆ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙
∧ (τ ↿ E⇘ES2⇙) @ r2 @ q2' @ [𝒱'] @ s2' ∈ Tr⇘ES2⇙
∧ q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = r1' ↿ E⇘ES2⇙
∧ s2' ↿ V⇘𝒱2⇙ = s2 ↿ V⇘𝒱2⇙
∧ s2' ↿ C⇘𝒱2⇙ = [])"
proof (induct "r1' ↿ E⇘ES2⇙" arbitrary: r1' rule: rev_induct)
case Nil
note s2_in_E2star
moreover
have "set [] ⊆ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙"
by auto
moreover
from outerCons_prems(6) t2_is_r2_v'_s2
have "τ ↿ E⇘ES2⇙ @ r2 @ [] @ [𝒱'] @ s2 ∈ Tr⇘ES2⇙"
by auto
moreover
from Nil have "[] ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = r1' ↿ E⇘ES2⇙"
by (simp add: projection_def)
moreover
have "s2 ↿ V⇘𝒱2⇙ = s2 ↿ V⇘𝒱2⇙"..
moreover
note s2_Cv2_empty
ultimately show ?case
by blast
next
case (snoc x xs)
have xs_is_xsE2: "xs = xs ↿ E⇘ES2⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES2⇙"
by (simp add: projection_def, auto)
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES2⇙) ⊆ N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙"
by simp
with xs_is_xsE2 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain s2'' q2''
where s2''_in_E2star: "set s2'' ⊆ E⇘ES2⇙"
and q2''_in_C2_inter_Upsilon2_inter_Delta2: "set q2'' ⊆ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙"
and τE2_r2_q2''_v'_s2''_in_Tr2: "(τ ↿ E⇘ES2⇙ @ r2 @ q2'') @ [𝒱'] @ s2'' ∈ Tr⇘ES2⇙"
and q2''C2_Upsilon2_is_xsE2: "q2'' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = xs ↿ E⇘ES2⇙"
and s2''V2_is_s2V2: "s2'' ↿ V⇘𝒱2⇙ = s2 ↿ V⇘𝒱2⇙"
and s2''C2_empty: "s2'' ↿ C⇘𝒱2⇙ = []"
by auto
have x_in_Cv2_inter_Upsilon2: "x ∈ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙"
and x_in_Cv2_inter_Nv1: "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by simp
thus "x ∈ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙"
and "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
by auto
qed
with validV2 have x_in_E2: "x ∈ E⇘ES2⇙"
by (simp add:isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
note x_in_Cv2_inter_Upsilon2
moreover
from v'_in_Vv1_inter_Vv2_inter_Nabla2 have "𝒱' ∈ V⇘𝒱2⇙ ∩ ∇⇘Γ2⇙"
by auto
moreover
note τE2_r2_q2''_v'_s2''_in_Tr2 s2''C2_empty
moreover
have Adm: "(Adm 𝒱2 ρ2 Tr⇘ES2⇙ (τ ↿ E⇘ES2⇙ @ r2 @ q2'') x)"
proof -
from τE2_r2_q2''_v'_s2''_in_Tr2 validES2
have "(τ ↿ E⇘ES2⇙ @ r2 @ q2'') ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv2_inter_Nv1 ES2_total_Cv2_inter_Nv1
have "(τ ↿ E⇘ES2⇙ @ r2 @ q2'') @ [x] ∈ Tr⇘ES2⇙"
by (simp only: total_def)
moreover
have "(τ ↿ E⇘ES2⇙ @ r2 @ q2'') ↿ (ρ2 𝒱2) = (τ ↿ E⇘ES2⇙ @ r2 @ q2'') ↿ (ρ2 𝒱2)" ..
ultimately show ?thesis
by (simp only: Adm_def, blast)
qed
moreover
note FCIA2
ultimately
obtain s2' γ'
where res1: "(set γ') ⊆ (N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙)"
and res2: "((τ ↿ E⇘ES2⇙ @ r2 @ q2'') @ [x] @ γ' @ [𝒱'] @ s2') ∈ Tr⇘ES2⇙"
and res3: "(s2' ↿ V⇘𝒱2⇙) = (s2'' ↿ V⇘𝒱2⇙)"
and res4: "s2' ↿ C⇘𝒱2⇙ = []"
unfolding FCIA_def
by blast
let ?q2' = "q2'' @ [x] @ γ'"
from res2 validES2 have "set s2' ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
moreover
from res1 x_in_Cv2_inter_Upsilon2 q2''_in_C2_inter_Upsilon2_inter_Delta2
have "set ?q2' ⊆ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙"
by auto
moreover
from res2 have "τ ↿ E⇘ES2⇙ @ r2 @ ?q2' @ [𝒱'] @ s2' ∈ Tr⇘ES2⇙"
by auto
moreover
have "?q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = r1' ↿ E⇘ES2⇙"
proof -
from validV2 res1 have "γ' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = []"
proof -
from res1 have "γ' = γ' ↿ (N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙)"
by (simp only: list_subset_iff_projection_neutral)
hence "γ' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = γ' ↿ (N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by simp
hence "γ' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = γ' ↿ (N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by (simp only: projection_def, auto)
moreover
from validV2 have "N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ = {}"
by (simp add:isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by (simp add: projection_def)
qed
hence "?q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = (q2'' @ [x]) ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by (simp only: projection_concatenation_commute, auto)
with q2''C2_Upsilon2_is_xsE2 x_in_Cv2_inter_Upsilon2
have "?q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = (xs ↿ E⇘ES2⇙) @ [x]"
by (simp only: projection_concatenation_commute projection_def, auto)
with xs_is_xsE2 snoc(2) show ?thesis
by simp
qed
moreover
from res3 s2''V2_is_s2V2 have "s2' ↿ V⇘𝒱2⇙ = s2 ↿ V⇘𝒱2⇙"
by simp
moreover
note res4
ultimately show ?case
by blast
qed
from this[OF r1'E2_in_Nv1_inter_Cv2_Upsilon2_star] obtain s2' q2'
where s2'_in_E2star: "set s2' ⊆ E⇘ES2⇙"
and q2'_in_Cv2_inter_Upsilon2_union_Nv2_inter_Delta2:
"set q2' ⊆ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙"
and τE2_r2_q2'_v'_s2'_in_Tr2: "(τ ↿ E⇘ES2⇙) @ r2 @ q2' @ [𝒱'] @ s2' ∈ Tr⇘ES2⇙"
and q2'Cv2_inter_Upsilon2_is_r1'E2: "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) = r1' ↿ E⇘ES2⇙"
and s2'Vv2_is_s2_Vv2: "s2' ↿ V⇘𝒱2⇙ = s2 ↿ V⇘𝒱2⇙"
and s2'Cv2_empty: "s2' ↿ C⇘𝒱2⇙ = []"
by auto
from q2'_in_Cv2_inter_Upsilon2_union_Nv2_inter_Delta2 validV2
have q2'_in_E2star: "set q2' ⊆ E⇘ES2⇙"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def
VN_disjoint_def NC_disjoint_def, auto)
have r1'Cv_empty: "r1' ↿ C⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2
r1'_Cv1_empty r1'_in_E1star)
from validES2 τE2_r2_q2'_v'_s2'_in_Tr2
have q2'_in_E2star: "set q2' ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
moreover
note r1'_in_E1star
moreover
have q2'E1_is_r1'E2: "q2' ↿ E⇘ES1⇙ = r1' ↿ E⇘ES2⇙"
proof -
from q2'_in_Cv2_inter_Upsilon2_union_Nv2_inter_Delta2
have "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) = q2'"
by (simp add: list_subset_iff_projection_neutral)
hence "(q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙)) ↿ E⇘ES1⇙ = q2' ↿ E⇘ES1⇙"
by simp
hence "q2' ↿ ((C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ∩ E⇘ES1⇙) = q2' ↿ E⇘ES1⇙"
by (simp add: projection_def)
hence "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∩ E⇘ES1⇙) = q2' ↿ E⇘ES1⇙"
by (simp only: Int_Un_distrib2 disjoint_Nv2_inter_Delta2_inter_E1, auto)
moreover
from q2'Cv2_inter_Upsilon2_is_r1'E2
have "(q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)) ↿ E⇘ES1⇙ = (r1' ↿ E⇘ES2⇙) ↿ E⇘ES1⇙"
by simp
hence "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∩ E⇘ES1⇙) = (r1' ↿ E⇘ES1⇙) ↿ E⇘ES2⇙"
by (simp add: projection_def conj_commute)
with r1'_in_E1star have "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∩ E⇘ES1⇙) = r1' ↿ E⇘ES2⇙"
by (simp only: list_subset_iff_projection_neutral)
ultimately show ?thesis
by auto
qed
moreover
have "q2' ↿ V⇘𝒱⇙ = []"
proof -
from q2'_in_Cv2_inter_Upsilon2_union_Nv2_inter_Delta2
have "q2' = q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙)"
by (simp add: list_subset_iff_projection_neutral)
moreover
from q2'_in_E2star have "q2' = q2' ↿ E⇘ES2⇙"
by (simp add: list_subset_iff_projection_neutral)
ultimately have "q2' = q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ E⇘ES2⇙"
by simp
hence "q2' ↿ V⇘𝒱⇙ = q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ E⇘ES2⇙ ↿ V⇘𝒱⇙"
by simp
hence "q2' ↿ V⇘𝒱⇙ = q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ (V⇘𝒱⇙ ∩ E⇘ES2⇙)"
by (simp add: Int_commute projection_def)
with propSepViews
have "q2' ↿ V⇘𝒱⇙ = q2' ↿ ((C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ∩ V⇘𝒱2⇙)"
unfolding properSeparationOfViews_def
by (simp add: projection_def)
hence "q2' ↿ V⇘𝒱⇙ = q2' ↿ (V⇘𝒱2⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ V⇘𝒱2⇙ ∩ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙)"
by (simp add: Int_Un_distrib2, metis Int_assoc
Int_commute Int_left_commute Un_commute)
with validV2 show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto, simp add: projection_def)
qed
moreover
have "r1' ↿ V⇘𝒱⇙ = []"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute projection_intersection_neutral
r1'_Vv1_empty r1'_in_E1star)
moreover
have q2'Cv_empty: "q2' ↿ C⇘𝒱⇙ = []"
proof -
from q2'_in_E2star have foo: "q2' = q2' ↿ E⇘ES2⇙"
by (simp add: list_subset_iff_projection_neutral)
hence "q2' ↿ C⇘𝒱⇙ = q2' ↿ (C⇘𝒱⇙ ∩ E⇘ES2⇙)"
by (metis Int_commute list_subset_iff_projection_neutral
projection_intersection_neutral)
moreover
from propSepViews have "C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def by auto
from projection_subset_elim[OF ‹C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙›, of q2']
have "q2' ↿ C⇘𝒱2⇙ ↿ C⇘𝒱⇙ ↿ E⇘ES2⇙ = q2' ↿ (C⇘𝒱⇙ ∩ E⇘ES2⇙)"
by (simp add: projection_def)
hence "q2' ↿ E⇘ES2⇙ ↿ C⇘𝒱2⇙ ↿ C⇘𝒱⇙ = q2' ↿ (C⇘𝒱⇙ ∩ E⇘ES2⇙)"
by (simp add: projection_commute)
with foo have "q2' ↿ (C⇘𝒱2⇙ ∩ C⇘𝒱⇙) = q2' ↿ (C⇘𝒱⇙ ∩ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from q2'_in_Cv2_inter_Upsilon2_union_Nv2_inter_Delta2
have "q2' ↿ (C⇘𝒱2⇙ ∩ C⇘𝒱⇙) = q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ (C⇘𝒱2⇙ ∩ C⇘𝒱⇙)"
by (simp add: list_subset_iff_projection_neutral)
moreover
have "(C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ∩ (C⇘𝒱2⇙ ∩ C⇘𝒱⇙)
= (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ C⇘𝒱2⇙ ∩ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ∩ C⇘𝒱⇙"
by fast
hence "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ (C⇘𝒱2⇙ ∩ C⇘𝒱⇙)
= q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ C⇘𝒱2⇙ ∩ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ C⇘𝒱⇙"
by (simp add: projection_sequence)
moreover
from validV2
have "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙ ∪ C⇘𝒱2⇙ ∩ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙) ↿ C⇘𝒱⇙
= q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) ↿ C⇘𝒱⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def Int_commute)
moreover
from q2'Cv2_inter_Upsilon2_is_r1'E2
have "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) ↿ C⇘𝒱⇙ = r1' ↿ E⇘ES2⇙ ↿ C⇘𝒱⇙"
by simp
with projection_on_intersection[OF r1'Cv_empty] have "q2' ↿ (C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙) ↿ C⇘𝒱⇙ = []"
by (simp add: Int_commute projection_def)
ultimately show ?thesis
by auto
qed
moreover
note r1'Cv_empty merge_property'[of r1' q2']
ultimately obtain q'
where q'E2_is_q2': "q' ↿ E⇘ES2⇙ = q2'"
and q'E1_is_r1': "q' ↿ E⇘ES1⇙ = r1'"
and q'V_empty: "q' ↿ V⇘𝒱⇙ = []"
and q'C_empty: "q' ↿ C⇘𝒱⇙ = []"
and q'_in_E1_union_E2_star: "set q' ⊆ (E⇘ES1⇙ ∪ E⇘ES2⇙)"
unfolding Let_def
by auto
let ?tau = "τ @ r2 @ q' @ [𝒱']"
from Cons(2) r2_in_E2star q'_in_E1_union_E2_star v'_in_E2
have "set ?tau ⊆ (E⇘(ES1 ∥ ES2)⇙)"
by (simp add: composeES_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from t1'_in_E1star t1'_is_r1'_v'_s1' have "set s1' ⊆ E⇘ES1⇙"
by simp
moreover
note s2'_in_E2star
moreover
from τr2E1_t1'_in_Tr1 t1'_is_r1'_v'_s1' v'_in_E1 q'E1_is_r1'
have "?tau ↿ E⇘ES1⇙ @ s1' ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute projection_def, auto)
moreover
from q'E2_is_q2' r2_in_E2star v'_in_E2 q2'_in_E2star τE2_r2_q2'_v'_s2'_in_Tr2
have "?tau ↿ E⇘ES2⇙ @ s2' ∈ Tr⇘ES2⇙"
by (simp only: list_subset_iff_projection_neutral
projection_concatenation_commute projection_def, auto)
moreover
have "lambda' ↿ E⇘ES1⇙ = s1' ↿ V⇘𝒱⇙"
proof -
from Cons(2,4,8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
moreover
from t1'_is_r1'_v'_s1' r1'_Vv1_empty r1'_in_E1star
v'_in_Vv1 propSepViews
have "t1' ↿ V⇘𝒱⇙ = [𝒱'] @ (s1' ↿ V⇘𝒱⇙)"
proof -
have "r1' ↿ V⇘𝒱⇙ =[]"
using propSepViews unfolding properSeparationOfViews_def
by (metis projection_on_subset2 r1'_Vv1_empty
r1'_in_E1star subset_iff_psubset_eq)
with t1'_is_r1'_v'_s1' v'_in_Vv1 Vv_is_Vv1_union_Vv2 show ?thesis
by (simp only: t1'_is_r1'_v'_s1' projection_concatenation_commute
projection_def, auto)
qed
moreover
have "t1 ↿ V⇘𝒱⇙ = t1' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute outerCons_prems(3)
projection_intersection_neutral t1'_Vv1_is_t1_Vv1 t1'_in_E1star)
ultimately show ?thesis
by auto
qed
moreover
have "lambda' ↿ E⇘ES2⇙ = s2' ↿ V⇘𝒱⇙"
proof -
from Cons(3,5,9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
moreover
from t2_is_r2_v'_s2 r2_Vv_empty v'_in_Vv2 Vv_is_Vv1_union_Vv2
have "t2 ↿ V⇘𝒱⇙ = [𝒱'] @ (s2 ↿ V⇘𝒱⇙)"
by (simp only: t2_is_r2_v'_s2 projection_concatenation_commute
projection_def, auto)
moreover
have "s2 ↿ V⇘𝒱⇙ = s2' ↿ V⇘𝒱⇙"
using propSepViews unfolding properSeparationOfViews_def
by (metis Int_commute projection_intersection_neutral
s2'Vv2_is_s2_Vv2 s2'_in_E2star s2_in_E2star)
ultimately show ?thesis
by auto
qed
moreover
note s1'_Cv1_empty s2'Cv2_empty Cons.hyps[of ?tau s1' s2']
ultimately obtain t'
where τ_r2_q'_v'_t'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ q' @ [𝒱'] @ t'"
note τ_r2_q'_v'_t'_in_Tr
moreover
from r2_Vv_empty q'V_empty t'Vv_is_lambda' v'_in_Vv
have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by(simp only: projection_concatenation_commute projection_def, auto)
moreover
from VIsViewOnE r2_Cv2_empty t'Cv_empty q'C_empty v'_in_Vv
have "?t ↿ C⇘𝒱⇙ = []"
proof -
from VIsViewOnE v'_in_Vv have "[𝒱'] ↿ C⇘𝒱⇙ = []"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def projection_def, auto)
moreover
from r2_in_E2star r2_Cv2_empty
have "r2 ↿ C⇘𝒱⇙ = []"
using propSepViews projection_on_subset2 unfolding properSeparationOfViews_def
by auto
moreover
note t'Cv_empty q'C_empty
ultimately show ?thesis
by (simp only: projection_concatenation_commute, auto)
qed
ultimately have ?thesis
by auto
}
moreover
{
assume v'_in_Vv1_minus_E2: "𝒱' ∈ V⇘𝒱1⇙ - E⇘ES2⇙"
hence v'_in_Vv1: "𝒱' ∈ V⇘𝒱1⇙"
by auto
with v'_in_Vv have v'_in_E1: "𝒱' ∈ E⇘ES1⇙"
using propSepViews unfolding properSeparationOfViews_def
by auto
from v'_in_Vv1_minus_E2 have v'_notin_E2: "𝒱' ∉ E⇘ES2⇙"
by auto
with validV2 have v'_notin_Vv2: "𝒱' ∉ V⇘𝒱2⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
from Cons(3-4) Cons(8) v'_in_E1 have "t1 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES1⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r1 s1
where t1_is_r1_v'_s1: "t1 = r1 @ [𝒱'] @ s1"
and r1_Vv_empty: "r1 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱1⇙" "V⇘𝒱⇙" "r1"]
have r1_Vv1_empty: "r1 ↿ V⇘𝒱1⇙ = []"
by auto
from t1_is_r1_v'_s1 Cons(10) have r1_Cv1_empty: "r1 ↿ C⇘𝒱1⇙ = []"
by (simp add: projection_concatenation_commute)
from t1_is_r1_v'_s1 Cons(10) have s1_Cv1_empty: "s1 ↿ C⇘𝒱1⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(4) t1_is_r1_v'_s1 have r1_in_E1star: "set r1 ⊆ E⇘ES1⇙"
by auto
have r1_in_Nv1star: "set r1 ⊆ N⇘𝒱1⇙"
proof -
note r1_in_E1star
moreover
from r1_Vv1_empty have "set r1 ∩ V⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r1_Cv1_empty have "set r1 ∩ C⇘𝒱1⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV1
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r1E2_in_Nv1_inter_C2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) = set r1 ∩ E⇘ES2⇙"
by (simp add: projection_def, auto)
with r1_in_Nv1star have "set (r1 ↿ E⇘ES2⇙) ⊆ (E⇘ES2⇙ ∩ N⇘𝒱1⇙)"
by auto
moreover
from validV2 disjoint_Nv1_Vv2
have "E⇘ES2⇙ ∩ N⇘𝒱1⇙ = N⇘𝒱1⇙ ∩ C⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv2_inter_Nv1_subsetof_Upsilon2
have r1E2_in_Nv1_inter_C2_Upsilon2_star: "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙ ∩ Υ⇘Γ2⇙)"
by auto
note outerCons_prems = Cons.prems
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙) ⟹
∃ t2'. ( set t2' ⊆ E⇘ES2⇙
∧ ((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙
∧ t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙
∧ t2' ↿ C⇘𝒱2⇙ = [] )"
proof (induct "r1 ↿ E⇘ES2⇙" arbitrary: r1 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(10) outerCons_prems(4)
outerCons_prems(6) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE2: "xs = xs ↿ E⇘ES2⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES2⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ (E⇘ES2⇙)"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
proof -
have "set (r1 ↿ E⇘ES2⇙) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by auto
with xs_is_xsE2 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t2''
where t2''_in_E2star: "set t2'' ⊆ E⇘ES2⇙"
and τ_xs_E2_t2''_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ t2'' ∈ Tr⇘ES2⇙"
and t2''Vv2_is_t2Vv2: "t2'' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2''Cv2_empty: "t2'' ↿ C⇘𝒱2⇙ = []"
by auto
have x_in_Cv2_inter_Nv1: "x ∈ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱1⇙ ∩ C⇘𝒱2⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv2: "x ∈ C⇘𝒱2⇙"
by auto
moreover
note τ_xs_E2_t2''_in_Tr2 t2''Cv2_empty
moreover
have Adm: "(Adm 𝒱2 ρ2 Tr⇘ES2⇙ ((τ @ xs) ↿ E⇘ES2⇙) x)"
proof -
from τ_xs_E2_t2''_in_Tr2 validES2
have τ_xsE2_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv2_inter_Nv1 ES2_total_Cv2_inter_Nv1
have τ_xsE2_x_in_Tr2: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] ∈ Tr⇘ES2⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2) = ((τ @ xs) ↿ E⇘ES2⇙) ↿ (ρ2 𝒱2)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA2
ultimately obtain t2'
where res1: "((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2' ∈ Tr⇘ES2⇙"
and res2: "t2' ↿ V⇘𝒱2⇙ = t2'' ↿ V⇘𝒱2⇙"
and res3: "t2' ↿ C⇘𝒱2⇙ = []"
by (simp only: BSIA_def, blast)
have "set t2' ⊆ E⇘ES2⇙"
proof -
from res1 validES2 have "set (((τ @ xs) ↿ E⇘ES2⇙) @ [x] @ t2') ⊆ E⇘ES2⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
proof -
from res1 xs_is_xsE2 have "((τ ↿ E⇘ES2⇙) @ (xs @ [x])) @ t2' ∈ Tr⇘ES2⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t2''Vv2_is_t2Vv2 res2 have "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r1E2_in_Nv1_inter_C2_star] obtain t2'
where t2'_in_E2star: "set t2' ⊆ E⇘ES2⇙"
and τr1E2_t2'_in_Tr2: "((τ @ r1) ↿ E⇘ES2⇙) @ t2' ∈ Tr⇘ES2⇙"
and t2'_Vv2_is_t2_Vv2: "t2' ↿ V⇘𝒱2⇙ = t2 ↿ V⇘𝒱2⇙"
and t2'_Cv2_empty: "t2' ↿ C⇘𝒱2⇙ = []"
by auto
let ?tau = "τ @ r1 @ [𝒱']"
from v'_in_E1 Cons(2) r1_in_Nv1star validV1 have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: isViewOn_def composeES_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(4) t1_is_r1_v'_s1 have "set s1 ⊆ E⇘ES1⇙"
by auto
moreover
note t2'_in_E2star
moreover
have "?tau ↿ E⇘ES1⇙ @ s1 ∈ Tr⇘ES1⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(3) Cons.prems(5)
projection_concatenation_commute t1_is_r1_v'_s1)
moreover
from τr1E2_t2'_in_Tr2 v'_notin_E2 have "?tau ↿ E⇘ES2⇙ @ t2' ∈ Tr⇘ES2⇙"
by (simp add: projection_def)
moreover
from Cons(8) t1_is_r1_v'_s1 r1_Vv_empty v'_in_E1 v'_in_Vv have "lambda' ↿ E⇘ES1⇙ = s1 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(9) v'_notin_E2 t2'_Vv2_is_t2_Vv2 have "lambda' ↿ E⇘ES2⇙ = t2' ↿ V⇘𝒱⇙"
proof -
have "t2' ↿ V⇘𝒱⇙ = t2' ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral t2'_in_E2star)
moreover
have "t2 ↿ V⇘𝒱⇙ = t2 ↿ V⇘𝒱2⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral Cons(5))
moreover
note Cons(9) v'_notin_E2 t2'_Vv2_is_t2_Vv2
ultimately show ?thesis
by (simp add: projection_def)
qed
moreover
note s1_Cv1_empty t2'_Cv2_empty
moreover
note Cons.hyps(1)[of ?tau s1 t2']
ultimately obtain t'
where τr1v't'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r1 @ [𝒱'] @ t'"
note τr1v't'_in_Tr
moreover
from r1_Vv_empty t'_Vv_is_lambda' v'_in_Vv have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r1 ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "E⇘ES1⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def by auto
from projection_on_subset[OF ‹E⇘ES1⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱1⇙› r1_Cv1_empty]
have "r1 ↿ (E⇘ES1⇙ ∩ C⇘𝒱⇙) = []"
by (simp only: Int_commute)
with projection_intersection_neutral[OF r1_in_E1star, of "C⇘𝒱⇙"] show ?thesis
by simp
qed
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
moreover
{
assume v'_in_Vv2_minus_E1: "𝒱' ∈ V⇘𝒱2⇙ - E⇘ES1⇙"
hence v'_in_Vv2: "𝒱' ∈ V⇘𝒱2⇙"
by auto
with v'_in_Vv propSepViews have v'_in_E2: "𝒱' ∈ E⇘ES2⇙"
unfolding properSeparationOfViews_def
by auto
from v'_in_Vv2_minus_E1 have v'_notin_E1: "𝒱' ∉ E⇘ES1⇙"
by auto
with validV1 have v'_notin_Vv1: "𝒱' ∉ V⇘𝒱1⇙"
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
from Cons(3) Cons(5) Cons(9) v'_in_E2 have "t2 ↿ V⇘𝒱⇙ = 𝒱' # (lambda' ↿ E⇘ES2⇙)"
by (simp add: projection_def)
from projection_split_first[OF this] obtain r2 s2
where t2_is_r2_v'_s2: "t2 = r2 @ [𝒱'] @ s2"
and r2_Vv_empty: "r2 ↿ V⇘𝒱⇙ = []"
by auto
with Vv_is_Vv1_union_Vv2 projection_on_subset[of "V⇘𝒱2⇙" "V⇘𝒱⇙" "r2"]
have r2_Vv2_empty: "r2 ↿ V⇘𝒱2⇙ = []"
by auto
from t2_is_r2_v'_s2 Cons(11) have r2_Cv2_empty: "r2 ↿ C⇘𝒱2⇙ = []"
by (simp add: projection_concatenation_commute)
from t2_is_r2_v'_s2 Cons(11) have s2_Cv2_empty: "s2 ↿ C⇘𝒱2⇙ = []"
by (simp only: projection_concatenation_commute, auto)
from Cons(5) t2_is_r2_v'_s2 have r2_in_E2star: "set r2 ⊆ E⇘ES2⇙"
by auto
have r2_in_Nv2star: "set r2 ⊆ N⇘𝒱2⇙"
proof -
note r2_in_E2star
moreover
from r2_Vv2_empty have "set r2 ∩ V⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
from r2_Cv2_empty have "set r2 ∩ C⇘𝒱2⇙ = {}"
by (metis Compl_Diff_eq Diff_cancel Un_upper2
disjoint_eq_subset_Compl list_subset_iff_projection_neutral
projection_on_union)
moreover
note validV2
ultimately show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
qed
have r2E1_in_Nv2_inter_C1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) = set r2 ∩ E⇘ES1⇙"
by (simp add: projection_def, auto)
with r2_in_Nv2star have "set (r2 ↿ E⇘ES1⇙) ⊆ (E⇘ES1⇙ ∩ N⇘𝒱2⇙)"
by auto
moreover
from validV1 propSepViews disjoint_Nv2_Vv1
have "E⇘ES1⇙ ∩ N⇘𝒱2⇙ = N⇘𝒱2⇙ ∩ C⇘𝒱1⇙"
unfolding properSeparationOfViews_def
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
ultimately show ?thesis
by auto
qed
with Cv1_inter_Nv2_subsetof_Upsilon1
have r2E1_in_Nv2_inter_C1_Upsilon1_star: "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙ ∩ Υ⇘Γ1⇙)"
by auto
note outerCons_prems = Cons.prems
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙) ⟹
∃ t1'. ( set t1' ⊆ E⇘ES1⇙
∧ ((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙
∧ t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙
∧ t1' ↿ C⇘𝒱1⇙ = [] )"
proof (induct "r2 ↿ E⇘ES1⇙" arbitrary: r2 rule: rev_induct)
case Nil thus ?case
by (metis append_self_conv outerCons_prems(9) outerCons_prems(3)
outerCons_prems(5) projection_concatenation_commute)
next
case (snoc x xs)
have xs_is_xsE1: "xs = xs ↿ E⇘ES1⇙"
proof -
from snoc(2) have "set (xs @ [x]) ⊆ E⇘ES1⇙"
by (simp add: projection_def, auto)
hence "set xs ⊆ E⇘ES1⇙"
by auto
thus ?thesis
by (simp add: list_subset_iff_projection_neutral)
qed
moreover
have "set (xs ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
proof -
have "set (r2 ↿ E⇘ES1⇙) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by (metis Int_commute snoc.prems)
with snoc(2) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
hence "set xs ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by auto
with xs_is_xsE1 show ?thesis
by auto
qed
moreover
note snoc.hyps(1)[of xs]
ultimately obtain t1''
where t1''_in_E1star: "set t1'' ⊆ E⇘ES1⇙"
and τ_xs_E1_t1''_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ t1'' ∈ Tr⇘ES1⇙"
and t1''Vv1_is_t1Vv1: "t1'' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1''Cv1_empty: "t1'' ↿ C⇘𝒱1⇙ = []"
by auto
have x_in_Cv1_inter_Nv2: "x ∈ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙"
proof -
from snoc(2-3) have "set (xs @ [x]) ⊆ (N⇘𝒱2⇙ ∩ C⇘𝒱1⇙)"
by simp
thus ?thesis
by auto
qed
hence x_in_Cv1: "x ∈ C⇘𝒱1⇙"
by auto
moreover
note τ_xs_E1_t1''_in_Tr1 t1''Cv1_empty
moreover
have Adm: "(Adm 𝒱1 ρ1 Tr⇘ES1⇙ ((τ @ xs) ↿ E⇘ES1⇙) x)"
proof -
from τ_xs_E1_t1''_in_Tr1 validES1
have τ_xsE1_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by (simp add: ES_valid_def traces_prefixclosed_def
prefixclosed_def prefix_def)
with x_in_Cv1_inter_Nv2 ES1_total_Cv1_inter_Nv2
have τ_xsE1_x_in_Tr1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] ∈ Tr⇘ES1⇙"
by (simp only: total_def)
moreover
have "((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1) = ((τ @ xs) ↿ E⇘ES1⇙) ↿ (ρ1 𝒱1)" ..
ultimately show ?thesis
by (simp add: Adm_def, auto)
qed
moreover note BSIA1
ultimately obtain t1'
where res1: "((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1' ∈ Tr⇘ES1⇙"
and res2: "t1' ↿ V⇘𝒱1⇙ = t1'' ↿ V⇘𝒱1⇙"
and res3: "t1' ↿ C⇘𝒱1⇙ = []"
by (simp only: BSIA_def, blast)
have "set t1' ⊆ E⇘ES1⇙"
proof -
from res1 validES1 have "set (((τ @ xs) ↿ E⇘ES1⇙) @ [x] @ t1') ⊆ E⇘ES1⇙"
by (simp add: ES_valid_def traces_contain_events_def, auto)
thus ?thesis
by auto
qed
moreover
have "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
proof -
from res1 xs_is_xsE1 have "((τ ↿ E⇘ES1⇙) @ (xs @ [x])) @ t1' ∈ Tr⇘ES1⇙"
by (simp only: projection_concatenation_commute, auto)
thus ?thesis
by (simp only: snoc(2) projection_concatenation_commute)
qed
moreover
from t1''Vv1_is_t1Vv1 res2 have "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
by auto
moreover
note res3
ultimately show ?case
by auto
qed
from this[OF r2E1_in_Nv2_inter_C1_star] obtain t1'
where t1'_in_E1star: "set t1' ⊆ E⇘ES1⇙"
and τr2E1_t1'_in_Tr1: "((τ @ r2) ↿ E⇘ES1⇙) @ t1' ∈ Tr⇘ES1⇙"
and t1'_Vv1_is_t1_Vv1: "t1' ↿ V⇘𝒱1⇙ = t1 ↿ V⇘𝒱1⇙"
and t1'_Cv1_empty: "t1' ↿ C⇘𝒱1⇙ = []"
by auto
let ?tau = "τ @ r2 @ [𝒱']"
from v'_in_E2 Cons(2) r2_in_Nv2star validV2 have "set ?tau ⊆ E⇘(ES1 ∥ ES2)⇙"
by (simp only: composeES_def isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def, auto)
moreover
from Cons(3) have "set lambda' ⊆ V⇘𝒱⇙"
by auto
moreover
from Cons(5) t2_is_r2_v'_s2 have "set s2 ⊆ E⇘ES2⇙"
by auto
moreover
note t1'_in_E1star
moreover
have "?tau ↿ E⇘ES2⇙ @ s2 ∈ Tr⇘ES2⇙"
by (metis Cons_eq_appendI append_eq_appendI calculation(3) eq_Nil_appendI
list_subset_iff_projection_neutral Cons.prems(4) Cons.prems(6)
projection_concatenation_commute t2_is_r2_v'_s2)
moreover
from τr2E1_t1'_in_Tr1 v'_notin_E1 have "?tau ↿ E⇘ES1⇙ @ t1' ∈ Tr⇘ES1⇙"
by (simp add: projection_def)
moreover
from Cons(9) t2_is_r2_v'_s2 r2_Vv_empty v'_in_E2 v'_in_Vv
have "lambda' ↿ E⇘ES2⇙ = s2 ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
from Cons(10) v'_notin_E1 t1'_Vv1_is_t1_Vv1
have "lambda' ↿ E⇘ES1⇙ = t1' ↿ V⇘𝒱⇙"
proof -
have "t1' ↿ V⇘𝒱⇙ = t1' ↿ V⇘𝒱1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral t1'_in_E1star)
moreover
have "t1 ↿ V⇘𝒱⇙ = t1 ↿ V⇘𝒱1⇙"
using propSepViews unfolding properSeparationOfViews_def
by (simp add: projection_def, metis Int_commute
projection_def projection_intersection_neutral Cons(4))
moreover
note Cons(8) v'_notin_E1 t1'_Vv1_is_t1_Vv1
ultimately show ?thesis
by (simp add: projection_def)
qed
moreover
note s2_Cv2_empty t1'_Cv1_empty
moreover
note Cons.hyps(1)[of ?tau t1' s2]
ultimately obtain t'
where τr2v't'_in_Tr: "?tau @ t' ∈ Tr⇘(ES1 ∥ ES2)⇙"
and t'_Vv_is_lambda': "t' ↿ V⇘𝒱⇙ = lambda'"
and t'_Cv_empty: "t' ↿ C⇘𝒱⇙ = []"
by auto
let ?t = "r2 @ [𝒱'] @ t'"
note τr2v't'_in_Tr
moreover
from r2_Vv_empty t'_Vv_is_lambda' v'_in_Vv have "?t ↿ V⇘𝒱⇙ = 𝒱' # lambda'"
by (simp add: projection_def)
moreover
have "?t ↿ C⇘𝒱⇙ = []"
proof -
have "r2 ↿ C⇘𝒱⇙ = []"
proof -
from propSepViews have "E⇘ES2⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱2⇙"
unfolding properSeparationOfViews_def by auto
from projection_on_subset[OF ‹E⇘ES2⇙ ∩ C⇘𝒱⇙ ⊆ C⇘𝒱2⇙› r2_Cv2_empty]
have "r2 ↿ (E⇘ES2⇙ ∩ C⇘𝒱⇙) = []"
by (simp only: Int_commute)
with projection_intersection_neutral[OF r2_in_E2star, of "C⇘𝒱⇙"] show ?thesis
by simp
qed
with v'_in_Vv VIsViewOnE t'_Cv_empty show ?thesis
by (simp add: isViewOn_def V_valid_def
VC_disjoint_def VN_disjoint_def NC_disjoint_def projection_def, auto)
qed
ultimately have ?thesis
by auto
}
ultimately show ?thesis
by blast
qed
qed
}
thus ?thesis
by auto
qed
lemma generalized_zipping_lemma:
"∀ τ lambda t1 t2. ( ( set τ ⊆ E⇘(ES1 ∥ ES2)⇙
∧ set lambda ⊆ V⇘𝒱⇙ ∧ set t1 ⊆ E⇘ES1⇙ ∧ set t2 ⊆ E⇘ES2⇙
∧ ((τ ↿ E⇘ES1⇙) @ t1) ∈ Tr⇘ES1⇙ ∧ ((τ ↿ E⇘ES2⇙) @ t2) ∈ Tr⇘ES2⇙
∧ (lambda ↿ E⇘ES1⇙) = (t1 ↿ V⇘𝒱⇙) ∧ (lambda ↿ E⇘ES2⇙) = (t2 ↿ V⇘𝒱⇙)
∧ (t1 ↿ C⇘𝒱1⇙) = [] ∧ (t2 ↿ C⇘𝒱2⇙) = [])
⟶ (∃t. ((τ @ t) ∈ Tr⇘(ES1 ∥ ES2)⇙ ∧ (t ↿ V⇘𝒱⇙) = lambda ∧ (t ↿ C⇘𝒱⇙) = [])) )"
proof -
note well_behaved_composition
moreover {
assume "N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {} ∧ N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {}"
with generalized_zipping_lemma1 have ?thesis
by auto
}
moreover {
assume "∃ ρ1. N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {} ∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) ∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙"
then obtain ρ1 where "N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {} ∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) ∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙"
by auto
with generalized_zipping_lemma2[of ρ1] have ?thesis
by auto
}
moreover {
assume "∃ ρ2. N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {} ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙) ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙"
then obtain ρ2 where "N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {} ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙) ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙"
by auto
with generalized_zipping_lemma3[of ρ2] have ?thesis
by auto
}
moreover {
assume "∃ ρ1 ρ2 Γ1 Γ2. ( ∇⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Δ⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Υ⇘Γ1⇙ ⊆ E⇘ES1⇙
∧ ∇⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Δ⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Υ⇘Γ2⇙ ⊆ E⇘ES2⇙
∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙ ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙
∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙)
∧ FCIA ρ1 Γ1 𝒱1 Tr⇘ES1⇙ ∧ FCIA ρ2 Γ2 𝒱2 Tr⇘ES2⇙
∧ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ⊆ ∇⇘Γ1⇙ ∪ ∇⇘Γ2⇙
∧ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙ ⊆ Υ⇘Γ1⇙ ∧ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙ ⊆ Υ⇘Γ2⇙
∧ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ E⇘ES2⇙ = {} ∧ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ E⇘ES1⇙ = {} )"
then obtain ρ1 ρ2 Γ1 Γ2 where "∇⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Δ⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Υ⇘Γ1⇙ ⊆ E⇘ES1⇙
∧ ∇⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Δ⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Υ⇘Γ2⇙ ⊆ E⇘ES2⇙
∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙ ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙
∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙)
∧ FCIA ρ1 Γ1 𝒱1 Tr⇘ES1⇙ ∧ FCIA ρ2 Γ2 𝒱2 Tr⇘ES2⇙
∧ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ⊆ ∇⇘Γ1⇙ ∪ ∇⇘Γ2⇙
∧ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙ ⊆ Υ⇘Γ1⇙ ∧ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙ ⊆ Υ⇘Γ2⇙
∧ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ E⇘ES2⇙ = {} ∧ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ E⇘ES1⇙ = {}"
by auto
with generalized_zipping_lemma4[of Γ1 Γ2 ρ1 ρ2] have ?thesis
by auto
}
ultimately show ?thesis unfolding wellBehavedComposition_def
by blast
qed
end
end