Theory BSPTaxonomy
theory BSPTaxonomy
imports "../../SystemSpecification/EventSystems"
"../../SecuritySpecification/BasicSecurityPredicates"
begin
locale BSPTaxonomyDifferentCorrections =
fixes ES :: "'e ES_rec"
and 𝒱 :: "'e V_rec"
assumes validES: "ES_valid ES"
and VIsViewOnE: "isViewOn 𝒱 E⇘ES⇙"
locale BSPTaxonomyDifferentViews =
fixes ES :: "'e ES_rec"
and 𝒱⇩1 :: "'e V_rec"
and 𝒱⇩2 :: "'e V_rec"
assumes validES: "ES_valid ES"
and 𝒱⇩1IsViewOnE: "isViewOn 𝒱⇩1 E⇘ES⇙"
and 𝒱⇩2IsViewOnE: "isViewOn 𝒱⇩2 E⇘ES⇙"
locale BSPTaxonomyDifferentViewsFirstDim= BSPTaxonomyDifferentViews +
assumes V2_subset_V1: "V⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙"
and N2_supset_N1: "N⇘𝒱⇩2⇙ ⊇ N⇘𝒱⇩1⇙"
and C2_subset_C1: "C⇘𝒱⇩2⇙ ⊆ C⇘𝒱⇩1⇙"
sublocale BSPTaxonomyDifferentViewsFirstDim ⊆ BSPTaxonomyDifferentViews
by (unfold_locales)
locale BSPTaxonomyDifferentViewsSecondDim= BSPTaxonomyDifferentViews +
assumes V2_subset_V1: "V⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙"
and N2_supset_N1: "N⇘𝒱⇩2⇙ ⊇ N⇘𝒱⇩1⇙"
and C2_equals_C1: "C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙"
sublocale BSPTaxonomyDifferentViewsSecondDim ⊆ BSPTaxonomyDifferentViews
by (unfold_locales)
context BSPTaxonomyDifferentCorrections
begin
lemma SR_implies_R:
"SR 𝒱 Tr⇘ES⇙ ⟹ R 𝒱 Tr⇘ES⇙"
proof -
assume SR: "SR 𝒱 Tr⇘ES⇙"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
with SR have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙"
unfolding SR_def by auto
hence "∃ τ'. τ' ∈ Tr⇘ES⇙ ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ τ' ↿ C⇘𝒱⇙ = []"
proof -
assume tau_V_N_is_trace: "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙"
show "∃ τ'. τ' ∈ Tr⇘ES⇙ ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ τ' ↿ C⇘𝒱⇙ = []"
proof
let ?τ'= "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
by (simp add: projection_subset_elim)
moreover
from VIsViewOnE have "VC_disjoint 𝒱 ∧ NC_disjoint 𝒱"
unfolding isViewOn_def V_valid_def
by auto
then have "(V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∩ C⇘𝒱⇙ = {}"
by (simp add: NC_disjoint_def VC_disjoint_def inf_sup_distrib2)
then have "?τ' ↿ C⇘𝒱⇙ = []"
by (simp add: disjoint_projection)
ultimately
show "?τ' ∈ Tr⇘ES⇙ ∧ ?τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ ?τ' ↿ C⇘𝒱⇙ = []"
using tau_V_N_is_trace by auto
qed
qed
}
thus ?thesis
unfolding SR_def R_def by auto
qed
lemma SD_implies_BSD :
"(SD 𝒱 Tr⇘ES⇙) ⟹ BSD 𝒱 Tr⇘ES⇙ "
proof -
assume SD: "SD 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ c # α ∈ Tr⇘ES⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
with SD have "β @ α ∈ Tr⇘ES⇙"
unfolding SD_def by auto
hence "∃α'. β @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
using alpha_C_empty
by auto
}
thus ?thesis
unfolding SD_def BSD_def by auto
qed
lemma BSD_implies_D:
"BSD 𝒱 Tr⇘ES⇙ ⟹ D 𝒱 Tr⇘ES⇙"
proof -
assume BSD: "BSD 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "α ↿ C⇘𝒱⇙ = []"
and "c ∈ C⇘𝒱⇙"
and "β @ [c] @ α ∈ Tr⇘ES⇙"
with BSD obtain α'
where "β @ α' ∈ Tr⇘ES⇙"
and "α' ↿ V⇘𝒱⇙ = α ↿ V 𝒱"
and "α' ↿ C⇘𝒱⇙ = []"
by (simp add: BSD_def, auto)
hence "(∃α' β'.
(β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
by auto
}
thus ?thesis
unfolding BSD_def D_def
by auto
qed
lemma SD_implies_SR:
"SD 𝒱 Tr⇘ES⇙ ⟹ SR 𝒱 Tr⇘ES⇙"
unfolding SR_def
proof
fix τ
assume SD: "SD 𝒱 Tr⇘ES⇙"
assume τ_trace: "τ ∈ Tr⇘ES⇙"
{
fix n
have SR_via_length: " ⟦ τ ∈ Tr⇘ES⇙; n = length (τ ↿ C⇘𝒱⇙) ⟧
⟹ ∃τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
proof (induct n arbitrary: τ)
case 0
note τ_in_Tr = ‹τ ∈ Tr⇘ES⇙›
and ‹0 = length (τ ↿ C⇘𝒱⇙)›
hence "τ ↿ C⇘𝒱⇙ = []"
by simp
with τ_in_Tr show ?case
by auto
next
case (Suc n)
from projection_split_last[OF Suc(3)] obtain β c α
where c_in_C: "c ∈ C⇘𝒱⇙"
and τ_is_βcα: "τ = β @ [c] @ α"
and α_no_c: "α ↿ C⇘𝒱⇙ = []"
and βα_contains_n_cs: "n = length ((β @ α) ↿ C⇘𝒱⇙)"
by auto
with Suc(2) have βcα_in_Tr: "β @ [c] @ α ∈ Tr⇘ES⇙"
by auto
with SD c_in_C βcα_in_Tr α_no_c obtain β' α'
where β'α'_in_Tr: "(β' @ α') ∈ Tr⇘ES⇙"
and α'_V_is_α_V: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
and α'_no_c: "α' ↿ C⇘𝒱⇙ = []"
and β'_VC_is_β_VC: "β' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)"
unfolding SD_def
by blast
have "(β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
proof -
from β'_VC_is_β_VC have "β' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (rule projection_subset_eq_from_superset_eq)
with α'_V_is_α_V have "(β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (simp add: projection_def)
moreover
with VIsViewOnE c_in_C have "c ∉ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def, auto)
hence "(β @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β @ [c] @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (simp add: projection_def)
moreover note τ_is_βcα
ultimately show ?thesis
by auto
qed
moreover
have "n = length ((β' @ α') ↿ C⇘𝒱⇙)"
proof -
have "β' ↿ C⇘𝒱⇙ = β ↿ C⇘𝒱⇙"
proof -
have "V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙ = C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by auto
with β'_VC_is_β_VC have "β' ↿ (C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)) = β ↿ (C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙))"
by auto
thus ?thesis
by (rule projection_subset_eq_from_superset_eq)
qed
with α'_no_c α_no_c have "(β' @ α') ↿ C⇘𝒱⇙ = (β @ α) ↿ C⇘𝒱⇙"
by (simp add: projection_def)
with βα_contains_n_cs show ?thesis
by auto
qed
with Suc.hyps β'α'_in_Tr obtain τ'
where "τ' ∈ Tr⇘ES⇙"
and "τ' ↿ C⇘𝒱⇙ = []"
and "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by auto
ultimately show ?case
by auto
qed
}
hence "τ ∈ Tr⇘ES⇙ ⟹ ∃τ'. τ'∈Tr⇘ES⇙ ∧ τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by auto
from this τ_trace obtain τ' where
τ'_trace : "τ'∈Tr⇘ES⇙"
and τ'_no_C : "τ' ↿ C⇘𝒱⇙ = []"
and τ'_τ_rel : "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by auto
from τ'_no_C have "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (auto simp add: projection_on_union)
with VIsViewOnE have τ'_E_eq_VN: "τ' ↿ E⇘ES⇙ = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (auto simp add: isViewOn_def)
from validES τ'_trace have "(set τ') ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
hence "τ' ↿ E⇘ES⇙ = τ'" by (simp add: list_subset_iff_projection_neutral)
with τ'_E_eq_VN have "τ' = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
with τ'_τ_rel have "τ' = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
with τ'_trace show "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙" by auto
qed
lemma D_implies_R:
"D 𝒱 Tr⇘ES⇙ ⟹ R 𝒱 Tr⇘ES⇙"
proof -
assume D: "D 𝒱 Tr⇘ES⇙"
{
fix τ n
have R_via_length: " ⟦ τ ∈ Tr⇘ES⇙; n = length (τ ↿ C⇘𝒱⇙) ⟧
⟹ ∃τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
proof (induct n arbitrary: τ)
case 0
note τ_in_Tr = ‹τ ∈ Tr⇘ES⇙›
and ‹0 = length (τ ↿ C⇘𝒱⇙)›
hence "τ ↿ C⇘𝒱⇙ = []"
by simp
with τ_in_Tr show ?case
by auto
next
case (Suc n)
from projection_split_last[OF Suc(3)] obtain β c α
where c_in_C: "c ∈ C⇘𝒱⇙"
and τ_is_βcα: "τ = β @ [c] @ α"
and α_no_c: "α ↿ C⇘𝒱⇙ = []"
and βα_contains_n_cs: "n = length ((β @ α) ↿ C⇘𝒱⇙)"
by auto
with Suc(2) have βcα_in_Tr: "β @ [c] @ α ∈ Tr⇘ES⇙"
by auto
with D c_in_C βcα_in_Tr α_no_c obtain β' α'
where β'α'_in_Tr: "(β' @ α') ∈ Tr⇘ES⇙"
and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
and α'_no_c: "α' ↿ C⇘𝒱⇙ = []"
and β'_VC_is_β_VC: "β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
unfolding D_def
by blast
have "(β' @ α') ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
proof -
from β'_VC_is_β_VC have "β' ↿ V⇘𝒱⇙ = β ↿ V⇘𝒱⇙"
by (rule projection_subset_eq_from_superset_eq)
with α'_V_is_α_V have "(β' @ α') ↿ V⇘𝒱⇙ = (β @ α) ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover
with VIsViewOnE c_in_C have "c ∉ V⇘𝒱⇙"
by (simp add: isViewOn_def V_valid_def VC_disjoint_def, auto)
hence "(β @ α) ↿ V⇘𝒱⇙ = (β @ [c] @ α) ↿ V⇘𝒱⇙"
by (simp add: projection_def)
moreover note τ_is_βcα
ultimately show ?thesis
by auto
qed
moreover
have "n = length ((β' @ α') ↿ C⇘𝒱⇙)"
proof -
have "β' ↿ C⇘𝒱⇙ = β ↿ C⇘𝒱⇙"
proof -
have "V⇘𝒱⇙ ∪ C⇘𝒱⇙ = C⇘𝒱⇙ ∪ V⇘𝒱⇙"
by auto
with β'_VC_is_β_VC have "β' ↿ (C⇘𝒱⇙ ∪ V⇘𝒱⇙) = β ↿ (C⇘𝒱⇙ ∪ V⇘𝒱⇙)"
by auto
thus ?thesis
by (rule projection_subset_eq_from_superset_eq)
qed
with α'_no_c α_no_c have "(β' @ α') ↿ C⇘𝒱⇙ = (β @ α) ↿ C⇘𝒱⇙"
by (simp add: projection_def)
with βα_contains_n_cs show ?thesis
by auto
qed
with Suc.hyps β'α'_in_Tr obtain τ'
where "τ' ∈ Tr⇘ES⇙"
and "τ' ↿ C⇘𝒱⇙ = []"
and "τ' ↿ V⇘𝒱⇙ = (β' @ α') ↿ V⇘𝒱⇙"
by auto
ultimately show ?case
by auto
qed
}
thus ?thesis
by (simp add: R_def)
qed
lemma SR_implies_R_for_modified_view :
"⟦SR 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ R 𝒱' Tr⇘ES⇙"
proof -
assume "SR 𝒱 Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
{
from ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› VIsViewOnE
have V'IsViewOnE: "isViewOn 𝒱' E⇘ES⇙ "
unfolding isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def VN_disjoint_def by auto
fix τ
assume "τ ∈ Tr⇘ES⇙"
with ‹SR 𝒱 Tr⇘ES⇙› have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙"
unfolding SR_def by auto
let ?τ'="τ ↿V⇘𝒱'⇙"
from ‹τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙› have "?τ' ∈ Tr⇘ES⇙"
using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by simp
moreover
from V'IsViewOnE have "?τ'↿C⇘𝒱'⇙=[]"
using disjoint_projection
unfolding isViewOn_def V_valid_def VC_disjoint_def by auto
moreover
have "?τ'↿V⇘𝒱'⇙ = τ↿V⇘𝒱'⇙"
by (simp add: projection_subset_elim)
ultimately
have "∃τ'∈Tr⇘ES⇙. τ' ↿ C⇘𝒱'⇙ = [] ∧ τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙"
by auto
}
with ‹SR 𝒱 Tr⇘ES⇙› show ?thesis
unfolding R_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto
qed
lemma R_implies_SR_for_modified_view :
"⟦R 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SR 𝒱 Tr⇘ES⇙"
proof -
assume "R 𝒱' Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
from ‹R 𝒱' Tr⇘ES⇙› ‹τ ∈ Tr⇘ES⇙› obtain τ' where "τ' ∈ Tr⇘ES⇙"
and "τ' ↿ C⇘𝒱'⇙ = []"
and "τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙"
unfolding R_def by auto
from VIsViewOnE ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› have "isViewOn 𝒱' E⇘ES⇙"
unfolding isViewOn_def V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
by auto
from ‹τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) = τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)"
by simp
from ‹τ' ↿ C⇘𝒱'⇙ = []› have "τ' =τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)"
using validES ‹τ' ∈ Tr⇘ES⇙› ‹isViewOn 𝒱' E⇘ES⇙›
unfolding projection_def ES_valid_def isViewOn_def traces_contain_events_def
by (metis UnE filter_True filter_empty_conv)
hence "τ' =τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)"
using ‹τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) = τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)›
by simp
with ‹τ' ∈ Tr⇘ES⇙› have "τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) ∈ Tr⇘ES⇙"
by auto
}
thus ?thesis
unfolding SR_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
by simp
qed
lemma SD_implies_BSD_for_modified_view :
"⟦SD 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ BSD 𝒱' Tr⇘ES⇙"
proof -
assume "SD 𝒱 Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
{
fix α β c
assume "c ∈ C⇘𝒱'⇙"
and "β @ [c] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱'⇙ = []"
from ‹c ∈ C⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "c ∈ C⇘𝒱⇙"
by auto
from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "α↿C⇘𝒱⇙ = []"
by auto
from ‹c ∈ C⇘𝒱⇙› ‹β @ [c] @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []›
have "β @ α ∈ Tr⇘ES⇙" using ‹SD 𝒱 Tr⇘ES⇙›
unfolding SD_def by auto
hence "∃α'. β @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙ ∧ α' ↿ C⇘𝒱'⇙ = [] "
using ‹α ↿ C⇘𝒱'⇙ = []› by blast
}
with ‹SD 𝒱 Tr⇘ES⇙› show ?thesis
unfolding BSD_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto
qed
lemma BSD_implies_SD_for_modified_view :
"⟦BSD 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SD 𝒱 Tr⇘ES⇙"
unfolding SD_def
proof(clarsimp)
fix α β c
assume BSD_view' : "BSD ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙⦈ Tr⇘ES⇙"
assume alpha_no_C_view : "α ↿ C⇘𝒱⇙ = []"
assume c_C_view : "c ∈ C⇘𝒱⇙"
assume beta_c_alpha_is_trace : "β @ c # α ∈ Tr⇘ES⇙"
from BSD_view' alpha_no_C_view c_C_view beta_c_alpha_is_trace
obtain α'
where beta_alpha'_is_trace: "β @ α'∈(Tr⇘ES⇙)"
and alpha_alpha': "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
and alpha'_no_C_view : "α' ↿ C⇘𝒱⇙ = []"
by (auto simp add: BSD_def)
from beta_c_alpha_is_trace validES
have alpha_consists_of_events: "set α ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from alpha_no_C_view have "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (rule projection_on_union)
with VIsViewOnE have alpha_on_ES : "α ↿ E⇘ES⇙ = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
unfolding isViewOn_def by simp
from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘ES⇙ = α"
by (simp add: list_subset_iff_projection_neutral)
with alpha_on_ES have α_eq: "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α" by auto
from beta_alpha'_is_trace validES
have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from alpha'_no_C_view have "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (rule projection_on_union)
with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘ES⇙ = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
unfolding isViewOn_def by (simp)
from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘ES⇙ = α'"
by (simp add: list_subset_iff_projection_neutral)
with alpha'_on_ES have α'_eq: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α'" by auto
from alpha_alpha' α_eq α'_eq have "α = α'" by auto
with beta_alpha'_is_trace show "β @ α ∈ Tr⇘ES⇙" by auto
qed
lemma SD_implies_FCD:
"(SD 𝒱 Tr⇘ES⇙) ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -
assume SD: "SD 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
and "β @ [c, v] @ α ∈ Tr⇘ES⇙"
moreover
with VIsViewOnE have "(v # α) ↿ C⇘𝒱⇙ = []"
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
ultimately
have "β @ (v # α) ∈ Tr⇘ES⇙"
using SD unfolding SD_def by auto
with alpha_C_empty
have "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ δ' @ [v] @ α') ∈ Tr⇘ES⇙
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by (metis append.simps(1) append.simps(2) bot_least list.set(1))
}
thus ?thesis
unfolding SD_def FCD_def by auto
qed
lemma SI_implies_BSI :
"(SI 𝒱 Tr⇘ES⇙) ⟹ BSI 𝒱 Tr⇘ES⇙ "
proof -
assume SI: "SI 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
with SI have "β @ c # α ∈ Tr⇘ES⇙"
unfolding SI_def by auto
hence "∃α'. β @ c # α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
using alpha_C_empty by auto
}
thus ?thesis
unfolding SI_def BSI_def by auto
qed
lemma BSI_implies_I:
"(BSI 𝒱 Tr⇘ES⇙) ⟹ (I 𝒱 Tr⇘ES⇙)"
proof -
assume BSI: "BSI 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
with BSI obtain α'
where "β @ [c] @ α' ∈ Tr⇘ES⇙"
and "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
and "α' ↿ C⇘𝒱⇙ = []"
unfolding BSI_def
by blast
hence
"(∃α' β'. (β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
by auto
}
thus ?thesis unfolding BSI_def I_def
by auto
qed
lemma SIA_implies_BSIA:
"(SIA ρ 𝒱 Tr⇘ES⇙) ⟹ (BSIA ρ 𝒱 Tr⇘ES⇙)"
proof -
assume SIA: "SIA ρ 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
and "(Adm 𝒱 ρ Tr⇘ES⇙ β c)"
with SIA obtain "β @ c # α ∈ Tr⇘ES⇙"
unfolding SIA_def by auto
hence "∃ α'. β @ c # α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
using alpha_C_empty by auto
}
thus ?thesis
unfolding SIA_def BSIA_def by auto
qed
lemma BSIA_implies_IA:
"(BSIA ρ 𝒱 Tr⇘ES⇙) ⟹ (IA ρ 𝒱 Tr⇘ES⇙)"
proof -
assume BSIA: "BSIA ρ 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
and "(Adm 𝒱 ρ Tr⇘ES⇙ β c)"
with BSIA obtain α'
where "β @ [c] @ α' ∈ Tr⇘ES⇙"
and "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
and "α' ↿ C⇘𝒱⇙ = []"
unfolding BSIA_def
by blast
hence "(∃α' β'.
(β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
by auto
}
thus ?thesis
unfolding BSIA_def IA_def by auto
qed
lemma SI_implies_SIA:
"SI 𝒱 Tr⇘ES⇙ ⟹ SIA ρ 𝒱 Tr⇘ES⇙"
proof -
assume SI: "SI 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
with SI have "β @ (c # α) ∈ Tr⇘ES⇙"
unfolding SI_def by auto
}
thus ?thesis unfolding SI_def SIA_def by auto
qed
lemma BSI_implies_BSIA:
"BSI 𝒱 Tr⇘ES⇙ ⟹ BSIA ρ 𝒱 Tr⇘ES⇙"
proof -
assume BSI: "BSI 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
with BSI have "∃ α'. β @ (c # α') ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
unfolding BSI_def by auto
}
thus ?thesis
unfolding BSI_def BSIA_def by auto
qed
lemma I_implies_IA:
"I 𝒱 Tr⇘ES⇙ ⟹ IA ρ 𝒱 Tr⇘ES⇙"
proof -
assume I: "I 𝒱 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
with I have "∃ α' β'. β' @ (c # α') ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙
∧ α' ↿ C⇘𝒱⇙ = [] ∧ β' ↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) "
unfolding I_def by auto
}
thus ?thesis
unfolding I_def IA_def by auto
qed
lemma SI_implies_BSI_for_modified_view :
"⟦SI 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ BSI 𝒱' Tr⇘ES⇙"
proof -
assume "SI 𝒱 Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
{
fix α β c
assume "c ∈ C⇘𝒱'⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱'⇙ = []"
from ‹c ∈ C⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "c ∈ C⇘𝒱⇙"
by auto
from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "α↿C⇘𝒱⇙ = []"
by auto
from ‹c ∈ C⇘𝒱⇙› ‹β @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []›
have "β @ [c] @ α ∈ Tr⇘ES⇙"
using ‹SI 𝒱 Tr⇘ES⇙› unfolding SI_def by auto
hence "∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙ ∧ α' ↿ C⇘𝒱'⇙ = [] "
using ‹α ↿ C⇘𝒱'⇙ = []›
by blast
}
with ‹SI 𝒱 Tr⇘ES⇙› show ?thesis
unfolding BSI_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto
qed
lemma BSI_implies_SI_for_modified_view :
"⟦BSI 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SI 𝒱 Tr⇘ES⇙"
unfolding SI_def
proof (clarsimp)
fix α β c
assume BSI_view' : "BSI ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙, N = {}, C = C⇘𝒱⇙⦈ Tr⇘ES⇙"
assume alpha_no_C_view : "α ↿ C⇘𝒱⇙ = []"
assume c_C_view : "c ∈ C⇘𝒱⇙"
assume beta_alpha_is_trace : "β @ α ∈ Tr⇘ES⇙"
from BSI_view' have "∀c∈C⇘𝒱⇙. β @ α ∈ Tr⇘ES⇙ ∧ α ↿ C⇘𝒱⇙ = []
⟶ (∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∧ α' ↿ C⇘𝒱⇙ = [])"
by (auto simp add: BSI_def)
with beta_alpha_is_trace alpha_no_C_view have "∀c∈C⇘𝒱⇙.
(∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∧ α' ↿ C⇘𝒱⇙ = [])"
by auto
with this BSI_view' c_C_view obtain α'
where beta_c_alpha'_is_trace: "β @ [c] @ α' ∈ Tr⇘ES⇙"
and alpha_alpha': "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
and alpha'_no_C_view : "α' ↿ C⇘𝒱⇙ = []"
by auto
from beta_alpha_is_trace validES
have alpha_consists_of_events: "set α ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from alpha_no_C_view have "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (rule projection_on_union)
with VIsViewOnE have alpha_on_ES : "α ↿ E⇘ES⇙ = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
unfolding isViewOn_def by (simp)
from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘ES⇙ = α"
by (simp add: list_subset_iff_projection_neutral)
with alpha_on_ES have α_eq: "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α" by auto
from beta_c_alpha'_is_trace validES
have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from alpha'_no_C_view have "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
by (rule projection_on_union)
with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘ES⇙ = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
unfolding isViewOn_def by (simp)
from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘ES⇙ = α'"
by (simp add: list_subset_iff_projection_neutral)
with alpha'_on_ES have α'_eq: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α'" by auto
from alpha_alpha' α_eq α'_eq have "α = α'" by auto
with beta_c_alpha'_is_trace show "β @ c # α ∈ Tr⇘ES⇙" by auto
qed
lemma SIA_implies_BSIA_for_modified_view :
"⟦SIA ρ 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈ ; ρ 𝒱 = ρ' 𝒱'⟧ ⟹ BSIA ρ' 𝒱' Tr⇘ES⇙"
proof -
assume "SIA ρ 𝒱 Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
and "ρ 𝒱 = ρ' 𝒱'"
{
fix α β c
assume "c ∈ C⇘𝒱'⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱'⇙ = []"
and "Adm 𝒱' ρ' Tr⇘ES⇙ β c"
from ‹c ∈ C⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "c ∈ C⇘𝒱⇙"
by auto
from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "α↿C⇘𝒱⇙ = []"
by auto
from ‹Adm 𝒱' ρ' Tr⇘ES⇙ β c› ‹ρ 𝒱 = ρ' 𝒱'›
have "Adm 𝒱 ρ Tr⇘ES⇙ β c"
by (simp add: Adm_def)
from ‹c ∈ C⇘𝒱⇙› ‹β @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []› ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
have "β @ [c] @ α ∈ Tr⇘ES⇙"
using ‹SIA ρ 𝒱 Tr⇘ES⇙› unfolding SIA_def by auto
hence "∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙ ∧ α' ↿ C⇘𝒱'⇙ = [] "
using ‹α ↿ C⇘𝒱'⇙ = []› by blast
}
with ‹SIA ρ 𝒱 Tr⇘ES⇙› show ?thesis
unfolding BSIA_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
by auto
qed
lemma BSIA_implies_SIA_for_modified_view :
"⟦BSIA ρ' 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈; ρ 𝒱 = ρ' 𝒱'⟧ ⟹ SIA ρ 𝒱 Tr⇘ES⇙"
proof -
assume "BSIA ρ' 𝒱' Tr⇘ES⇙"
and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈"
and "ρ 𝒱 = ρ' 𝒱'"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
from ‹c ∈ C⇘𝒱⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "c ∈ C⇘𝒱'⇙"
by auto
from ‹α↿C⇘𝒱⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
have "α↿C⇘𝒱'⇙ = []"
by auto
from ‹Adm 𝒱 ρ Tr⇘ES⇙ β c› ‹ρ 𝒱 = ρ' 𝒱'›
have "Adm 𝒱' ρ' Tr⇘ES⇙ β c"
by (simp add: Adm_def)
from ‹c ∈ C⇘𝒱'⇙› ‹β @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱'⇙ = []› ‹Adm 𝒱' ρ' Tr⇘ES⇙ β c›
obtain α' where "β @ [c] @ α' ∈ Tr⇘ES⇙"
and " α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙"
and " α' ↿ C⇘𝒱'⇙ = []"
using ‹BSIA ρ' 𝒱' Tr⇘ES⇙› unfolding BSIA_def by blast
from ‹β @ α ∈ Tr⇘ES⇙› validES
have alpha_consists_of_events: "set α ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› validES
have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙"
by (auto simp add: ES_valid_def traces_contain_events_def)
from ‹α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈›
have "α'↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)=α↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
with ‹α' ↿ C⇘𝒱'⇙ = []› ‹α↿C⇘𝒱⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈›
have "α'↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)=α↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)"
by (simp add: projection_on_union)
with VIsViewOnE alpha_consists_of_events alpha'_consists_of_events
have "α'=α" unfolding isViewOn_def
by (simp add: list_subset_iff_projection_neutral)
hence "β @ [c] @ α ∈ Tr⇘ES⇙ "
using ‹β @ [c] @ α' ∈ Tr⇘ES⇙› by blast
}
with ‹BSIA ρ' 𝒱' Tr⇘ES⇙› show ?thesis
unfolding SIA_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto
qed
end
lemma Adm_implies_Adm_for_modified_rho:
"⟦ Adm 𝒱⇩2 ρ⇩2 Tr α e;ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)⟧ ⟹ Adm 𝒱⇩1 ρ⇩1 Tr α e "
proof -
assume "Adm 𝒱⇩2 ρ⇩2 Tr α e"
and "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
then obtain γ
where "γ @ [e] ∈ Tr"
and "γ ↿ ρ⇩2 𝒱⇩2 = α ↿ ρ⇩2 𝒱⇩2"
unfolding Adm_def by auto
thus "Adm 𝒱⇩1 ρ⇩1 Tr α e"
unfolding Adm_def
using ‹ρ⇩1 𝒱⇩1 ⊆ ρ⇩2 𝒱⇩2› non_empty_projection_on_subset
by blast
qed
context BSPTaxonomyDifferentCorrections
begin
lemma SI_implies_FCI:
"(SI 𝒱 Tr⇘ES⇙) ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
proof -
assume SI: "SI 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
moreover
with VIsViewOnE have "(v # α) ↿ C⇘𝒱⇙ = []"
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
ultimately
have "β @ [c , v] @ α ∈ Tr⇘ES⇙" using SI unfolding SI_def by auto
with alpha_C_empty
have "∃α'. ∃δ'.
(set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr⇘ES⇙
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by (metis append.simps(1) append.simps(2) bot_least list.set(1))
}
thus ?thesis
unfolding SI_def FCI_def by auto
qed
lemma SIA_implies_FCIA:
"(SIA ρ 𝒱 Tr⇘ES⇙) ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof -
assume SIA: "SIA ρ 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
moreover
with VIsViewOnE have "(v # α) ↿ C⇘𝒱⇙ = []"
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
ultimately
have "β @ [c , v] @ α ∈ Tr⇘ES⇙" using SIA unfolding SIA_def by auto
with alpha_C_empty
have "∃α'. ∃δ'.
(set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr⇘ES⇙
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by (metis append.simps(1) append.simps(2) bot_least list.set(1))
}
thus ?thesis
unfolding SIA_def FCIA_def by auto
qed
lemma FCI_implies_FCIA:
"(FCI Γ 𝒱 Tr⇘ES⇙) ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof-
assume FCI: "FCI Γ 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and "α ↿ C⇘𝒱⇙ = []"
with FCI have "∃α' δ'. set δ' ⊆ N⇘𝒱⇙ ∩ Δ⇘Γ⇙ ∧
β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
unfolding FCI_def by auto
}
thus ?thesis
unfolding FCI_def FCIA_def by auto
qed
lemma Trivially_fulfilled_SR_C_empty:
"C⇘𝒱⇙ = {} ⟹ SR 𝒱 Tr⇘ES⇙"
proof -
assume "C⇘𝒱⇙={}"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
hence "τ=τ↿E⇘ES⇙" using validES
unfolding ES_valid_def traces_contain_events_def projection_def by auto
with ‹C⇘𝒱⇙={}› have "τ=τ↿(V⇘𝒱⇙∪N⇘𝒱⇙)"
using VIsViewOnE unfolding isViewOn_def by auto
with ‹τ ∈ Tr⇘ES⇙› have "τ↿(V⇘𝒱⇙∪N⇘𝒱⇙) ∈ Tr⇘ES⇙"
by auto
}
thus ?thesis
unfolding SR_def by auto
qed
lemma Trivially_fulfilled_R_C_empty:
"C⇘𝒱⇙ = {} ⟹ R 𝒱 Tr⇘ES⇙"
proof -
assume "C⇘𝒱⇙={}"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
hence "τ=τ↿E⇘ES⇙" using validES
unfolding ES_valid_def traces_contain_events_def projection_def by auto
with ‹C⇘𝒱⇙={}› have "τ=τ↿(V⇘𝒱⇙∪N⇘𝒱⇙)"
using VIsViewOnE unfolding isViewOn_def by auto
with ‹τ ∈ Tr⇘ES⇙› ‹C⇘𝒱⇙={}› have "∃τ' ∈ Tr⇘ES⇙. τ↿C⇘𝒱⇙=[] ∧ τ' ↿V⇘𝒱⇙=τ↿V⇘𝒱⇙"
unfolding projection_def by auto
}
thus ?thesis
unfolding R_def by auto
qed
lemma Trivially_fulfilled_SD_C_empty:
"C⇘𝒱⇙ = {} ⟹ SD 𝒱 Tr⇘ES⇙"
by (simp add: SD_def)
lemma Trivially_fulfilled_BSD_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSD 𝒱 Tr⇘ES⇙"
by (simp add: BSD_def)
lemma Trivially_fulfilled_D_C_empty:
"C⇘𝒱⇙ = {} ⟹ D 𝒱 Tr⇘ES⇙"
by (simp add: D_def)
lemma Trivially_fulfilled_FCD_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
by (simp add: FCD_def)
lemma Trivially_fullfilled_R_V_empty:
"V⇘𝒱⇙={} ⟹ R 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙={}"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
let ?τ'="[]"
from ‹τ ∈ Tr⇘ES⇙›have "?τ' ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
with ‹V⇘𝒱⇙={}›
have "∃τ' ∈ Tr⇘ES⇙. τ'↿C⇘𝒱⇙=[] ∧ τ'↿V⇘𝒱⇙=τ↿V⇘𝒱⇙"
by (metis projection_on_empty_trace projection_to_emptyset_is_empty_trace)
}
thus ?thesis
unfolding R_def by auto
qed
lemma Trivially_fulfilled_BSD_V_empty:
"V⇘𝒱⇙ = {} ⟹ BSD 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙={}"
{
fix α β c
assume "β @ [c] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙= []"
from ‹β @ [c] @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
let ?α'="[]"
from ‹β ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙={}›
have "β@ ?α'∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = []"
by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
hence
"∃α'.
β @ α'∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []" by blast
}
thus ?thesis
unfolding BSD_def by auto
qed
lemma Trivially_fulfilled_D_V_empty:
"V⇘𝒱⇙ = {} ⟹ D 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙={}"
{
fix α β c
assume "β @ [c] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙= []"
from ‹β @ [c] @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
let ?β'=β and ?α'="[]"
from ‹β ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙={}›
have "?β'@ ?α'∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = [] ∧ ?β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
hence
"∃α' β'.
β'@ α'∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = [] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
by blast
}
thus ?thesis
unfolding D_def by auto
qed
lemma Trivially_fulfilled_FCD_V_empty:
"V⇘𝒱⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
by (simp add: FCD_def)
lemma Trivially_fulfilled_FCD_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
by (simp add: FCD_def)
next
assume " Υ⇘Γ⇙={}" thus ?thesis
by (simp add: FCD_def)
qed
qed
lemma Trivially_fulfilled_FCD_N_subseteq_Δ_and_BSD:
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSD 𝒱 Tr⇘ES⇙⟧ ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -
assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
and "BSD 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [c,v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙ = []"
from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙"
by auto
from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙"
by auto
let ?α="[v] @ α"
from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
using VIsViewOnE
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
from ‹β @ [c,v] @ α ∈ Tr⇘ES⇙› have "β @ [c] @ ?α ∈ Tr⇘ES⇙"
by auto
from ‹BSD 𝒱 Tr⇘ES⇙›
obtain α'
where "β @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
and "α'↿C⇘𝒱⇙ = []"
using ‹c ∈ C⇘𝒱⇙› ‹β @ [c] @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []›
unfolding BSD_def by auto
from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙"
by (simp add: projection_def)
then obtain δ α''
where "α'=δ @ [v] @ α''"
and "δ↿V⇘𝒱⇙ = []"
and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
using projection_split_first_with_suffix by fastforce
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹β @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙" using validES
unfolding ES_valid_def traces_contain_events_def by auto
with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙"
by auto
with ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)"
using VIsViewOnE projection_empty_implies_absence_of_events
unfolding isViewOn_def projection_def by blast
let ?β=β and ?δ'=δ and ?α'=α''
from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''›
‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
by auto
hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙
∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []"
by auto
}
thus ?thesis
unfolding FCD_def by auto
qed
lemma Trivially_fulfilled_SI_C_empty:
"C⇘𝒱⇙ = {} ⟹ SI 𝒱 Tr⇘ES⇙"
by (simp add: SI_def)
lemma Trivially_fulfilled_BSI_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSI 𝒱 Tr⇘ES⇙"
by (simp add: BSI_def)
lemma Trivially_fulfilled_I_C_empty:
"C⇘𝒱⇙ = {} ⟹ I 𝒱 Tr⇘ES⇙"
by (simp add: I_def)
lemma Trivially_fulfilled_FCI_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
by (simp add: FCI_def)
lemma Trivially_fulfilled_SIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ SIA ρ 𝒱 Tr⇘ES⇙"
by (simp add: SIA_def)
lemma Trivially_fulfilled_BSIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSIA ρ 𝒱 Tr⇘ES⇙"
by (simp add: BSIA_def)
lemma Trivially_fulfilled_IA_C_empty:
"C⇘𝒱⇙ = {} ⟹ IA ρ 𝒱 Tr⇘ES⇙"
by (simp add: IA_def)
lemma Trivially_fulfilled_FCIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCIA Γ ρ 𝒱 Tr⇘ES⇙"
by (simp add: FCIA_def)
lemma Trivially_fulfilled_FCI_V_empty:
"V⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
by (simp add: FCI_def)
lemma Trivially_fulfilled_FCIA_V_empty:
"V⇘𝒱⇙ = {} ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
by (simp add: FCIA_def)
lemma Trivially_fulfilled_BSIA_V_empty_rho_subseteq_C_N:
"⟦V⇘𝒱⇙ = {}; ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙) ⟧ ⟹ BSIA ρ 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙={}"
and "ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙=[]"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
from ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
obtain γ
where "γ @ [c] ∈ Tr⇘ES⇙"
and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
unfolding Adm_def by auto
from this(1) have "γ ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
moreover
from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
ultimately
have "β↿E⇘ES⇙=γ↿E⇘ES⇙"
using validES VIsViewOnE ‹V⇘𝒱⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)›
non_empty_projection_on_subset
unfolding ES_valid_def isViewOn_def traces_contain_events_def
by (metis empty_subsetI sup_absorb2 sup_commute)
hence "β @ [c] ∈ Tr⇘ES⇙" using validES ‹γ @ [c] ∈ Tr⇘ES⇙› ‹β ∈ Tr⇘ES⇙› ‹γ ∈ Tr⇘ES⇙›
unfolding ES_valid_def traces_contain_events_def
by (metis list_subset_iff_projection_neutral subsetI)
let ?α'="[]"
from ‹β @ [c] ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙ = {}›
have "β @ [c] @ ?α' ∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = []"
by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
hence "∃ α'. β @ [c] @ α' ∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []"
by auto
}
thus ?thesis
unfolding BSIA_def by auto
qed
lemma Trivially_fulfilled_IA_V_empty_rho_subseteq_C_N:
"⟦V⇘𝒱⇙ = {}; ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙) ⟧ ⟹ IA ρ 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙={}"
and "ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙=[]"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
from ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
obtain γ
where "γ @ [c] ∈ Tr⇘ES⇙"
and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
unfolding Adm_def by auto
from this(1) have "γ ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
moreover
from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙" using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
ultimately
have "β↿E⇘ES⇙=γ↿E⇘ES⇙"
using validES VIsViewOnE ‹V⇘𝒱⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)›
non_empty_projection_on_subset
unfolding ES_valid_def isViewOn_def traces_contain_events_def
by (metis empty_subsetI sup_absorb2 sup_commute)
hence "β @ [c] ∈ Tr⇘ES⇙" using validES ‹γ @ [c] ∈ Tr⇘ES⇙› ‹β ∈ Tr⇘ES⇙› ‹γ ∈ Tr⇘ES⇙›
unfolding ES_valid_def traces_contain_events_def
by (metis list_subset_iff_projection_neutral subsetI)
let ?β'=β and ?α'="[]"
from ‹β @ [c] ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙ = {}›
have "?β' @ [c] @ ?α' ∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = []
∧ ?β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
hence "∃ α' β'.
β' @ [c] @ α' ∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []
∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
by auto
}
thus ?thesis
unfolding IA_def by auto
qed
lemma Trivially_fulfilled_BSI_V_empty_total_ES_C:
"⟦V⇘𝒱⇙ = {}; total ES C⇘𝒱⇙ ⟧ ⟹ BSI 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙ = {}"
and "total ES C⇘𝒱⇙"
{
fix α β c
assume "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙=[]"
and "c ∈ C⇘𝒱⇙"
from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
with ‹total ES C⇘𝒱⇙› have "β @ [c] ∈ Tr⇘ES⇙"
using ‹c ∈ C⇘𝒱⇙› unfolding total_def by auto
moreover
from ‹V⇘𝒱⇙ = {}› have "α↿V⇘𝒱⇙=[]"
unfolding projection_def by auto
ultimately
have "∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙=[]"
using ‹α ↿ C⇘𝒱⇙ = []› by (metis append_Nil2 projection_idempotent)
}
thus ?thesis
unfolding BSI_def by auto
qed
lemma Trivially_fulfilled_I_V_empty_total_ES_C:
"⟦V⇘𝒱⇙ = {}; total ES C⇘𝒱⇙ ⟧ ⟹ I 𝒱 Tr⇘ES⇙"
proof -
assume "V⇘𝒱⇙ = {}"
and "total ES C⇘𝒱⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇙"
and "β @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙=[]"
from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
using validES
unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
with ‹total ES C⇘𝒱⇙› have "β @ [c] ∈ Tr⇘ES⇙"
using ‹c ∈ C⇘𝒱⇙› unfolding total_def by auto
moreover
from ‹V⇘𝒱⇙ = {}› have "α↿V⇘𝒱⇙=[]"
unfolding projection_def by auto
ultimately
have "∃β' α'.
β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙=[] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
using ‹α ↿ C⇘𝒱⇙ = []› by (metis append_Nil2 projection_idempotent)
}
thus ?thesis
unfolding I_def by blast
qed
lemma Trivially_fulfilled_FCI_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCI Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
by (simp add: FCI_def)
next
assume " Υ⇘Γ⇙={}" thus ?thesis
by (simp add: FCI_def)
qed
qed
lemma Trivially_fulfilled_FCIA_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
by (simp add: FCIA_def)
next
assume " Υ⇘Γ⇙={}" thus ?thesis
by (simp add: FCIA_def)
qed
qed
lemma Trivially_fulfilled_FCI_N_subseteq_Δ_and_BSI:
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSI 𝒱 Tr⇘ES⇙⟧ ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
proof -
assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
and "BSI 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙ = []"
from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙"
by auto
from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙"
by auto
let ?α="[v] @ α"
from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
using VIsViewOnE
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
from ‹β @ [v] @ α ∈ Tr⇘ES⇙› have "β @ ?α ∈ Tr⇘ES⇙"
by auto
from ‹BSI 𝒱 Tr⇘ES⇙›
obtain α'
where "β @ [c] @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
and "α'↿C⇘𝒱⇙ = []"
using ‹c ∈ C⇘𝒱⇙› ‹β @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []›
unfolding BSI_def by blast
from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙"
by (simp add: projection_def)
then
obtain δ α''
where "α'=δ @ [v] @ α''"
and "δ↿V⇘𝒱⇙ = []"
and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
using projection_split_first_with_suffix by fastforce
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙"
using validES
unfolding ES_valid_def traces_contain_events_def by auto
with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙"
by auto
with ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)"
using VIsViewOnE projection_empty_implies_absence_of_events
unfolding isViewOn_def projection_def by blast
let ?β=β and ?δ'=δ and ?α'=α''
from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ [c] @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''›
‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
by auto
hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙
∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []"
by auto
}
thus ?thesis
unfolding FCI_def by auto
qed
lemma Trivially_fulfilled_FCIA_N_subseteq_Δ_and_BSIA:
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSIA ρ 𝒱 Tr⇘ES⇙⟧ ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof -
assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
and "BSIA ρ 𝒱 Tr⇘ES⇙"
{
fix α β c v
assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇙ = []"
and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙"
by auto
from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙"
by auto
let ?α="[v] @ α"
from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
using VIsViewOnE
unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
from ‹β @ [v] @ α ∈ Tr⇘ES⇙› have "β @ ?α ∈ Tr⇘ES⇙"
by auto
from ‹BSIA ρ 𝒱 Tr⇘ES⇙›
obtain α'
where "β @ [c] @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
and "α'↿C⇘𝒱⇙ = []"
using ‹c ∈ C⇘𝒱⇙› ‹β @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []› ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
unfolding BSIA_def by blast
from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙"
by (simp add: projection_def)
then
obtain δ α''
where "α'=δ @ [v] @ α''"
and "δ↿V⇘𝒱⇙ = []"
and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
using projection_split_first_with_suffix by fastforce
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]"
by (metis append_is_Nil_conv projection_concatenation_commute)
from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙"
using validES
unfolding ES_valid_def traces_contain_events_def by auto
with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙"
by auto
with ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)" using VIsViewOnE projection_empty_implies_absence_of_events
unfolding isViewOn_def projection_def by blast
let ?β=β and ?δ'=δ and ?α'=α''
from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ [c] @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''›
‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
by auto
hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙
∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []"
by auto
}
thus ?thesis
unfolding FCIA_def by auto
qed
end
context BSPTaxonomyDifferentViewsFirstDim
begin
lemma R_implies_R_for_modified_view:
"R 𝒱⇩1 Tr⇘ES⇙ ⟹ R 𝒱⇩2 Tr⇘ES⇙"
proof -
assume R_𝒱⇩1: "R 𝒱⇩1 Tr⇘ES⇙"
{
fix τ
assume "τ ∈ Tr⇘ES⇙"
with R_𝒱⇩1 have "∃ τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇩1⇙ = [] ∧ τ' ↿ V⇘𝒱⇩1⇙ = τ ↿ V⇘𝒱⇩1⇙"
unfolding R_def by auto
hence "∃ τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇩2⇙ = [] ∧ τ' ↿ V⇘𝒱⇩2⇙ = τ ↿ V⇘𝒱⇩2⇙"
using V2_subset_V1 C2_subset_C1 non_empty_projection_on_subset projection_on_subset by blast
}
thus ?thesis
unfolding R_def by auto
qed
lemma BSD_implies_BSD_for_modified_view:
"BSD 𝒱⇩1 Tr⇘ES⇙⟹ BSD 𝒱⇩2 Tr⇘ES⇙"
proof-
assume BSD_𝒱⇩1: "BSD 𝒱⇩1 Tr⇘ES⇙"
{
fix α β c n
assume c_in_C⇩2: "c ∈ C⇘𝒱⇩2⇙"
from C2_subset_C1 c_in_C⇩2 have c_in_C⇩1: "c ∈ C⇘𝒱⇩1⇙"
by auto
have "⟦β @ [c] @ α ∈ Tr⇘ES⇙; α ↿ C⇘𝒱⇩2⇙=[]; n= length(α ↿ C⇘𝒱⇩1⇙)⟧
⟹ ∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙ ∧ α' ↿C⇘𝒱⇩2⇙ = []"
proof(induct n arbitrary: α )
case 0
from "0.prems"(3) have "α ↿ C⇘𝒱⇩1⇙ = []" by auto
with c_in_C⇩1 "0.prems"(1)
have "∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿C⇘𝒱⇩1⇙ =[]"
using BSD_𝒱⇩1 unfolding BSD_def by auto
then
obtain α' where "β @ α' ∈ Tr⇘ES⇙"
and "α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙"
and "α' ↿C⇘𝒱⇩1⇙ =[]"
by auto
from V2_subset_V1 ‹α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙› have "α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by blast
moreover
from ‹α' ↿C⇘𝒱⇩1⇙ =[]› C2_subset_C1 have "α' ↿ C⇘𝒱⇩2⇙ = []"
using projection_on_subset by auto
ultimately
show ?case
using ‹β @ α' ∈ Tr⇘ES⇙› by auto
next
case (Suc n)
from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)]
obtain γ⇩1 γ⇩2 c⇩1 where c⇩1_in_C⇩1: "c⇩1 ∈ C⇘𝒱⇩1⇙"
and "α = γ⇩1 @ [c⇩1] @ γ⇩2"
and "γ⇩2 ↿C⇘𝒱⇩1⇙ = []"
and "n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)"
by auto
from "Suc.prems"(2) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "γ⇩1 ↿ C⇘𝒱⇩2⇙ = []"
by (simp add: projection_concatenation_commute)
from "Suc.prems"(1) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2›
obtain β' where "β'=β @ [c] @ γ⇩1"
and "β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙"
by auto
from ‹β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙› ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹c⇩1 ∈ C⇘𝒱⇩1⇙›
obtain γ⇩2' where " β' @ γ⇩2' ∈ Tr⇘ES⇙"
and "γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙"
and "γ⇩2' ↿C⇘𝒱⇩1⇙ =[]"
using BSD_𝒱⇩1 unfolding BSD_def by auto
from ‹β'=β @ [c] @ γ⇩1› ‹β' @ γ⇩2' ∈ Tr⇘ES⇙› have "β @ [c] @ γ⇩1 @ γ⇩2' ∈ Tr⇘ES⇙"
by auto
moreover
from ‹γ⇩1 ↿ C⇘𝒱⇩2⇙=[]› ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]› C2_subset_C1 have "(γ⇩1 @ γ⇩2') ↿ C⇘𝒱⇩2⇙ =[]"
by (metis append_Nil projection_concatenation_commute projection_on_subset)
moreover
from ‹n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)› ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]›
have "n = length((γ⇩1 @ γ⇩2')↿ C⇘𝒱⇩1⇙)"
by (simp add: projection_concatenation_commute)
ultimately
have witness: "∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿V⇘𝒱⇩2⇙ ∧ α' ↿C⇘𝒱⇩2⇙ = []"
using Suc.hyps by auto
from 𝒱⇩1IsViewOnE 𝒱⇩2IsViewOnE V2_subset_V1 C2_subset_C1 c⇩1_in_C⇩1 have "c⇩1 ∉ V⇘𝒱⇩2⇙"
unfolding isViewOn_def V_valid_def VC_disjoint_def by auto
with ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙"
unfolding projection_def by auto
hence "α ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙ "
using projection_concatenation_commute by auto
with V2_subset_V1 ‹γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙›
have "γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙ = γ⇩1↿ V⇘𝒱⇩2⇙ @ γ⇩2' ↿ V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by metis
with ‹α ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿ V⇘𝒱⇩2⇙"
by (simp add: projection_concatenation_commute)
from witness ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿ V⇘𝒱⇩2⇙›
show ?case
by auto
qed
}
thus ?thesis
unfolding BSD_def by auto
qed
lemma D_implies_D_for_modified_view:
"D 𝒱⇩1 Tr⇘ES⇙ ⟹ D 𝒱⇩2 Tr⇘ES⇙"
proof-
assume D_𝒱⇩1: "D 𝒱⇩1 Tr⇘ES⇙"
from V2_subset_V1 C2_subset_C1
have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙" by auto
{
fix α β c n
assume c_in_C⇩2: "c ∈ C⇘𝒱⇩2⇙"
from C2_subset_C1 c_in_C⇩2 have c_in_C⇩1: "c ∈ C⇘𝒱⇩1⇙"
by auto
have "⟦β @ [c] @ α ∈ Tr⇘ES⇙; α ↿ C⇘𝒱⇩2⇙=[]; n= length(α ↿ C⇘𝒱⇩1⇙)⟧
⟹ ∃ α' β'.
β' @ α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙ ∧ α' ↿C⇘𝒱⇩2⇙ = []
∧ β' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) "
proof(induct n arbitrary: α β )
case 0
from "0.prems"(3) have "α ↿ C⇘𝒱⇩1⇙ = []" by auto
with c_in_C⇩1 "0.prems"(1)
have "∃ α' β'.
β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿C⇘𝒱⇩1⇙ =[]
∧ β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using D_𝒱⇩1 unfolding D_def by fastforce
then
obtain β' α' where "β' @ α' ∈ Tr⇘ES⇙"
and "α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙"
and "α' ↿C⇘𝒱⇩1⇙ =[]"
and "β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
by auto
from V2_subset_V1 ‹α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙› have "α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by blast
moreover
from ‹α' ↿C⇘𝒱⇩1⇙ =[]› C2_subset_C1 have "α' ↿ C⇘𝒱⇩2⇙ = []"
using projection_on_subset by auto
moreover
from ‹β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1
have "β' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
using non_empty_projection_on_subset by blast
ultimately
show ?case
using ‹β' @ α' ∈ Tr⇘ES⇙› by auto
next
case (Suc n)
from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)]
obtain γ⇩1 γ⇩2 c⇩1 where c⇩1_in_C⇩1: "c⇩1 ∈ C⇘𝒱⇩1⇙"
and "α = γ⇩1 @ [c⇩1] @ γ⇩2"
and "γ⇩2 ↿C⇘𝒱⇩1⇙ = []"
and "n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)"
by auto
from "Suc.prems"(2) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "γ⇩1 ↿ C⇘𝒱⇩2⇙ = []"
by (simp add: projection_concatenation_commute)
from "Suc.prems"(1) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2›
obtain β' where "β'=β @ [c] @ γ⇩1"
and "β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙"
by auto
from ‹β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙› ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹c⇩1 ∈ C⇘𝒱⇩1⇙›
obtain γ⇩2' β'' where " β'' @ γ⇩2' ∈ Tr⇘ES⇙"
and "γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙"
and "γ⇩2' ↿C⇘𝒱⇩1⇙ =[]"
and "β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using D_𝒱⇩1 unfolding D_def by force
from c_in_C⇩1 have "c ∈ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
by auto
moreover
from ‹β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› ‹β'=β @ [c] @ γ⇩1›
have "β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = (β @ [c] @ γ⇩1) ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
by auto
ultimately
have "∃ β''' γ⇩1'. β''=β'''@ [c] @ γ⇩1'
∧ β''' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)
∧ γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using projection_split_arbitrary_element by fast
then
obtain β''' γ⇩1' where "β''= β''' @ [c] @ γ⇩1'"
and "β''' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
and "γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using projection_split_arbitrary_element by auto
from ‹β'' @ γ⇩2' ∈ Tr⇘ES⇙› this(1)
have "β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙"
by simp
from ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]› have "γ⇩2' ↿ C⇘𝒱⇩2⇙=[]"
using C2_subset_C1 projection_on_subset by auto
moreover
from ‹γ⇩1 ↿ C⇘𝒱⇩2⇙ = []› ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)›
have "γ⇩1'↿ C⇘𝒱⇩2⇙ = []" using C2_subset_C1 V2_subset_V1
by (metis non_empty_projection_on_subset projection_subset_eq_from_superset_eq sup_commute)
ultimately
have "(γ⇩1' @ γ⇩2')↿C⇘𝒱⇩2⇙ = []"
by (simp add: projection_concatenation_commute)
from ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› have "γ⇩1'↿C⇘𝒱⇩1⇙ = γ⇩1↿C⇘𝒱⇩1⇙"
using projection_subset_eq_from_superset_eq sup_commute by metis
hence "length(γ⇩1'↿C⇘𝒱⇩1⇙) = length(γ⇩1↿C⇘𝒱⇩1⇙)" by simp
moreover
from ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹γ⇩2'↿C⇘𝒱⇩1⇙=[]› have "length(γ⇩2'↿C⇘𝒱⇩1⇙) = length(γ⇩2↿C⇘𝒱⇩1⇙)"
by simp
ultimately
have "n=length((γ⇩1' @ γ⇩2')↿C⇘𝒱⇩1⇙)"
by (simp add: ‹n = length ((γ⇩1 @ γ⇩2) ↿ C⇘𝒱⇩1⇙)› projection_concatenation_commute)
from ‹β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙› ‹(γ⇩1' @ γ⇩2')↿C⇘𝒱⇩2⇙ = []› ‹n=length((γ⇩1' @ γ⇩2')↿C⇘𝒱⇩1⇙)›
have witness:
" ∃α' β'. β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = ( γ⇩1' @ γ⇩2') ↿ V⇘𝒱⇩2⇙
∧ α' ↿ C⇘𝒱⇩2⇙ = [] ∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β''' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
using Suc.hyps[OF ‹β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙›] by simp
from V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1 ‹β''' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)›
have "β''' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
using non_empty_projection_on_subset by blast
from 𝒱⇩1IsViewOnE 𝒱⇩2IsViewOnE V2_subset_V1 C2_subset_C1 c⇩1_in_C⇩1 have "c⇩1 ∉ V⇘𝒱⇩2⇙"
unfolding isViewOn_def V_valid_def VC_disjoint_def by auto
with ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙"
unfolding projection_def by auto
moreover
from V2_subset_V1 ‹γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙› have "γ⇩2' ↿ V⇘𝒱⇩2⇙ = γ⇩2 ↿ V⇘𝒱⇩2⇙"
using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq)
moreover
from ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› have "γ⇩1' ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙"
using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq)
ultimately
have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1' @ γ⇩2') ↿ V⇘𝒱⇩2⇙" using ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙›
by (simp add: projection_concatenation_commute)
from ‹β''' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)› ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1' @ γ⇩2') ↿ V⇘𝒱⇩2⇙›
show ?case
using witness by simp
qed
}
thus ?thesis
unfolding D_def by auto
qed
end
context BSPTaxonomyDifferentViewsSecondDim
begin
lemma FCD_implies_FCD_for_modified_view_gamma:
"⟦FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙;
V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙; N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙; C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
⟹ FCD Γ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume "FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙"
and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
{
fix α β v c
assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
and "β @ [c,v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇩2⇙ = []"
from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
by auto
moreover
from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
by auto
moreover
from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
by auto
ultimately
obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
and "β @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
and "α'↿C⇘𝒱⇩1⇙ = []"
using ‹β @ [c,v] @ α ∈ Tr⇘ES⇙› ‹FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCD_def by blast
from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙›
have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
by auto
moreover
from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by blast
moreover
from C2_equals_C1 ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
by auto
ultimately
have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)
∧ β @ δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
using ‹β @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto
}
thus ?thesis
unfolding FCD_def by blast
qed
lemma SI_implies_SI_for_modified_view :
"SI 𝒱⇩1 Tr⇘ES⇙ ⟹ SI 𝒱⇩2 Tr⇘ES⇙"
proof -
assume SI: "SI 𝒱⇩1 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
ultimately
have "β @ (c # α) ∈ Tr⇘ES⇙"
using SI unfolding SI_def by auto
}
thus ?thesis
unfolding SI_def by auto
qed
lemma BSI_implies_BSI_for_modified_view :
"BSI 𝒱⇩1 Tr⇘ES⇙ ⟹ BSI 𝒱⇩2 Tr⇘ES⇙"
proof -
assume BSI: "BSI 𝒱⇩1 Tr⇘ES⇙"
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
ultimately
have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = []"
using BSI unfolding BSI_def by auto
with V2_subset_V1 C2_equals_C1
have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []"
using non_empty_projection_on_subset by metis
}
thus ?thesis
unfolding BSI_def by auto
qed
lemma I_implies_I_for_modified_view :
"I 𝒱⇩1 Tr⇘ES⇙ ⟹ I 𝒱⇩2 Tr⇘ES⇙"
proof -
assume I: "I 𝒱⇩1 Tr⇘ES⇙"
from V2_subset_V1 C2_equals_C1 have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
by auto
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
ultimately
have "∃ α' β'.
β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = []
∧ β' ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using I unfolding I_def by auto
with V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1 V2_subset_V1 C2_equals_C1
have "∃ α' β'.
β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []
∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
using non_empty_projection_on_subset by metis
}
thus ?thesis
unfolding I_def by auto
qed
lemma SIA_implies_SIA_for_modified_view :
"⟦SIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ SIA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume SIA: "SIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
and ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
moreover
from ρ⇩2_supseteq_ρ⇩1 admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
by (simp add: Adm_implies_Adm_for_modified_rho)
ultimately
have "β @ (c # α) ∈ Tr⇘ES⇙"
using SIA unfolding SIA_def by auto
}
thus ?thesis
unfolding SIA_def by auto
qed
lemma BSIA_implies_BSIA_for_modified_view :
"⟦BSIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ BSIA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume BSIA: "BSIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
and ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
from V2_subset_V1 C2_equals_C1
have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
by auto
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
moreover
from ρ⇩2_supseteq_ρ⇩1 admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
by (simp add: Adm_implies_Adm_for_modified_rho)
ultimately
have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = []"
using BSIA unfolding BSIA_def by auto
with V2_subset_V1 C2_equals_C1
have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []"
using non_empty_projection_on_subset by metis
}
thus ?thesis
unfolding BSIA_def by auto
qed
lemma IA_implies_IA_for_modified_view :
"⟦IA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ IA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume IA: "IA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
and ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
{
fix α β c
assume "c ∈ C⇘𝒱⇩2⇙"
and "β @ α ∈ Tr⇘ES⇙"
and alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
moreover
with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
by auto
moreover
from alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
by auto
moreover
from ρ⇩2_supseteq_ρ⇩1 admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
by (simp add: Adm_implies_Adm_for_modified_rho)
ultimately
have "∃ α' β'. β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = [] ∧ β' ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
using IA unfolding IA_def by auto
moreover
from V2_subset_V1 C2_equals_C1 have "(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) ⊆ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
by auto
ultimately
have "∃ α' β'. β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = [] ∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
using V2_subset_V1 C2_equals_C1 non_empty_projection_on_subset by metis
}
thus ?thesis
unfolding IA_def by auto
qed
lemma FCI_implies_FCI_for_modified_view_gamma:
"⟦FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙;
V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙; N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙; C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
⟹ FCI Γ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume "FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙"
and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
{
fix α β v c
assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇩2⇙ = []"
from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
by auto
moreover
from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
by auto
moreover
from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
by auto
ultimately
obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
and "β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
and "α'↿C⇘𝒱⇩1⇙ = []"
using ‹β @ [v] @ α ∈ Tr⇘ES⇙› ‹FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCI_def by blast
from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙›
have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
by auto
moreover
from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by blast
moreover
from ‹C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙› ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
by auto
ultimately have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)
∧ β @ [c] @ δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
using ‹β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto
}
thus ?thesis
unfolding FCI_def by blast
qed
lemma FCIA_implies_FCIA_for_modified_view_rho_gamma:
"⟦FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1);
V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙; N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙; C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
⟹ FCIA ρ⇩2 Γ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
assume "FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
and "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙"
and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
{
fix α β v c
assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
and "β @ [v] @ α ∈ Tr⇘ES⇙"
and "α↿C⇘𝒱⇩2⇙ = []"
and "Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈ C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
by auto
moreover
from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈ V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
by auto
moreover
from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
by auto
moreover
from ‹Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c› ‹ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)› have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
by (simp add: Adm_implies_Adm_for_modified_rho)
ultimately
obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
and "β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
and "α'↿C⇘𝒱⇩1⇙ = []"
using ‹β @ [v] @ α ∈ Tr⇘ES⇙› ‹FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCIA_def by blast
from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇ N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙›
have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
by auto
moreover
from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙"
using non_empty_projection_on_subset by blast
moreover
from ‹C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙› ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
by auto
ultimately
have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)
∧ β @ [c] @ δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
using ‹β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto
}
thus ?thesis
unfolding FCIA_def by blast
qed
end
end