# Theory Projection

theory Projection
imports Main
begin

(* Projection of an event list onto a subset of the events *)
definition projection:: "'e list ⇒ 'e set ⇒ 'e list" (infixl "↿" 100)
where
"l ↿ E ≡ filter (λx . x ∈ E) l"

(* If projecting on Y yields the empty sequence, then projecting
on X ∪ Y yields the projection on X. *)
lemma projection_on_union:
"l ↿ Y = [] ⟹ l ↿ (X ∪ Y) = l ↿ X"
proof (induct l)
case Nil show ?case by (simp add: projection_def)
next
case (Cons a b) show ?case
proof (cases "a ∈ Y")
case True from Cons show "a ∈ Y ⟹ (a # b) ↿ (X ∪ Y) = (a # b) ↿ X"
next
case False from Cons show "a ∉ Y ⟹ (a # b) ↿ (X ∪ Y) = (a # b) ↿ X"
qed
qed

(*projection on the empty trace yields the empty trace*)
lemma projection_on_empty_trace: "[] ↿ X =[]" by (simp add: projection_def)

(*projection to the empty set yields the empty trace*)
lemma projection_to_emptyset_is_empty_trace: "l ↿{} = []" by (simp add: projection_def)

(*projection is idempotent*)
lemma projection_idempotent: "l ↿ X= (l ↿X) ↿X" by (simp add: projection_def)

(*empty projection implies that the trace contains no events of the set the trace is projected to*)
lemma projection_empty_implies_absence_of_events: "l ↿ X = [] ⟹  X ∩ (set l) = {}"
by (metis empty_set inter_set_filter projection_def)

(*subsequently projecting to two disjoint sets yields the empty trace*)
lemma disjoint_projection: "X ∩ Y = {} ⟹ (l ↿ X) ↿ Y = []"
proof -
assume X_Y_disjoint: "X ∩ Y = {}"
show "(l ↿ X) ↿ Y = []" unfolding projection_def
proof (induct l)
case Nil show ?case by simp
next
case (Cons x xs) show ?case
proof (cases "x ∈ X")
case True
with X_Y_disjoint have "x ∉ Y" by auto
thus "[x←[x←x # xs . x ∈ X] . x ∈ Y] = []" using Cons.hyps by auto
next
case False show "[x←[x←x # xs . x ∈ X] . x ∈ Y] = []" using Cons.hyps False by auto
qed
qed
qed

(* auxiliary lemmas for projection *)
lemma projection_concatenation_commute:
"(l1 @ l2) ↿ X = (l1 ↿ X) @ (l2 ↿ X)"
by (unfold projection_def, auto)

(* Lists that are equal under projection on a set will remain
equal under projection on a subset. *)
lemma projection_subset_eq_from_superset_eq:
"((xs ↿ (X ∪ Y)) = (ys ↿ (X ∪ Y))) ⟹ ((xs ↿ X) = (ys ↿ X))"
(is "(?L1 = ?L2) ⟹ (?L3 = ?L4)")
proof -
assume prem: "?L1 = ?L2"
have "?L1 ↿ X = ?L3 ∧ ?L2 ↿ X = ?L4"
proof -
have "⋀ a. ((a ∈ X ∨ a ∈ Y) ∧ a ∈ X) = (a ∈ X)"
by auto
thus ?thesis
qed
with prem show ?thesis
by auto
qed

(* All elements of a list l are in a set X if and only if
the projection of l onto X yields l. *)
lemma list_subset_iff_projection_neutral: "(set l ⊆ X) = ((l ↿ X) = l)"
(is "?A = ?B")
proof -
have "?A ⟹ ?B"
proof -
assume "?A"
hence "⋀x. x ∈ (set l) ⟹ x ∈ X"
by auto
thus ?thesis
qed
moreover
have "?B ⟹ ?A"
proof -
assume "?B"
hence "(set (l ↿ X)) = set l"
thus ?thesis
qed
ultimately show ?thesis ..
qed

(* If the projection of τ onto a set X is not the empty trace, then
there is x ∈ X that is the last occurrence of all elements of X in τ.
τ can then be split around x.

Expressing non-emptiness in terms of list length is quite useful
for inductive proofs. *)
lemma projection_split_last: "Suc n = length (τ ↿ X) ⟹
∃ β x α. (x ∈ X ∧ τ = β @ [x] @ α ∧ α ↿ X = [] ∧ n = length ((β @ α) ↿ X))"
proof -
assume Suc_n_is_len_τX: "Suc n = length (τ ↿ X)"

let ?L = "τ ↿ X"
let ?RL = "filter (λx . x ∈ X) (rev τ)"

have "Suc n = length ?RL"
proof -
have "rev ?L = ?RL"
by (simp add: projection_def, rule rev_filter)
hence "rev (rev ?L) = rev ?RL" ..
hence "?L = rev ?RL"
by auto
with Suc_n_is_len_τX show ?thesis
by auto
qed
with Suc_length_conv[of n ?RL] obtain x xs
where "?RL = x # xs"
by auto
hence "x # xs = ?RL"
by auto

from Cons_eq_filterD[OF this] obtain revα revβ
where "(rev τ) = revα @ x # revβ"
and revα_no_x: "∀a ∈ set revα. a ∉ X"
and x_in_X: "x ∈ X"
by auto
hence "rev (rev τ) = rev (revα @ x # revβ)"
by auto
hence "τ = (rev revβ) @ [x] @ (rev revα)"
by auto
then obtain β α
where τ_is_βxα: "τ = β @ [x] @ α"
and α_is_revrevα: "α = (rev revα)"
and β_is_revrevβ: "β = (rev revβ)"
by auto
hence α_no_x: "α ↿ X = []"
proof -
from α_is_revrevα revα_no_x have "∀a ∈ set α. a ∉ X"
by auto
thus ?thesis
qed

have "n = length ((β @ α) ↿ X)"
proof -
from α_no_x have αX_zero_len: "length (α ↿ X) = 0"
by auto

from x_in_X have xX_one_len: "length ([x] ↿ X) = 1"

from τ_is_βxα have "length ?L = length (β ↿ X) + length ([x] ↿ X) + length (α ↿ X)"
with αX_zero_len have "length ?L = length (β ↿ X) + length ([x] ↿ X)"
by auto
with xX_one_len Suc_n_is_len_τX have "n = length (β ↿ X)"
by auto
with αX_zero_len show ?thesis
qed
with x_in_X τ_is_βxα α_no_x show ?thesis
by auto
qed

lemma projection_rev_commute:
"rev (l ↿ X) = (rev l) ↿ X"

(* Same as the previous lemma except that we split around the FIRST
occurrence.

Note that we do not express non-emptiness via the length function
simply because there is no need for it in the theories relying on
this lemma. *)
lemma projection_split_first: "⟦ (τ ↿ X) = x # xs ⟧ ⟹ ∃ α β. (τ = α @ [x] @ β ∧ α ↿ X = [])"
proof -
assume τX_is_x_xs: "(τ ↿ X) = x # xs"
hence "0 ≠ length (τ ↿ X)"
by auto
hence "0 ≠ length (rev (τ ↿ X))"
by auto
hence "0 ≠ length ((rev τ) ↿ X)"
then obtain n where "Suc n = length ((rev τ) ↿ X)"
by (auto, metis Suc_pred length_greater_0_conv that)
from projection_split_last[OF this] obtain β' x' α'
where x'_in_X: "x' ∈ X"
and revτ_is_β'x'α': "rev τ = β' @ [x'] @ α'"
and α'X_empty: "α' ↿ X = []"
by auto

from revτ_is_β'x'α' have "rev (rev τ) = rev (β' @ [x'] @ α')" ..
hence τ_is_revα'_x'_revβ':"τ = rev α' @ [x'] @ rev β'"
by auto
moreover
from α'X_empty have revα'X_empty: "rev α' ↿ X = []"
by (metis projection_rev_commute rev_is_Nil_conv)
moreover
note x'_in_X
ultimately have "(τ ↿ X) = x' # ((rev β') ↿ X)"
by (simp only: projection_concatenation_commute projection_def, auto)
with τX_is_x_xs have "x = x'"
by auto
with τ_is_revα'_x'_revβ' have τ_is_revα'_x_revβ': "τ = rev α' @ [x] @ rev β'"
by auto
with revα'X_empty show ?thesis
by auto
qed

(* this lemma extends the previous lemma by also concluding that the suffix of the splitted trace
projected is equal to the projection of the initial trace without the first element *)
lemma projection_split_first_with_suffix:
"⟦ (τ ↿ X) = x # xs ⟧ ⟹ ∃ α β. (τ = α @ [x] @ β ∧ α ↿ X = [] ∧ β ↿ X = xs)"
proof -
assume tau_proj_X: "(τ ↿ X) = x # xs"
show ?thesis
proof -
from   tau_proj_X have x_in_X: "x ∈ X"
by (metis IntE inter_set_filter list.set_intros(1) projection_def)
from  tau_proj_X have  "∃ α β. τ = α @ [x] @ β ∧ α ↿ X = []"
using projection_split_first by auto
then obtain α β where tau_split: "τ = α @ [x] @ β"
and X_empty_prefix:"α ↿ X = []"
by auto
from tau_split tau_proj_X  have  "(α @ [x] @ β) ↿ X =x # xs"
by auto
with  X_empty_prefix have  "([x] @ β) ↿ X =x # xs"
hence "(x # β) ↿ X =x # xs"
by auto
with  x_in_X have "β ↿ X = xs"
unfolding projection_def by simp
with  tau_split X_empty_prefix show ?thesis
by auto
qed
qed

lemma projection_split_arbitrary_element:
"⟦τ ↿ X = (α @ [x] @ β) ↿ X; x ∈ X ⟧
⟹ ∃ α' β'. (τ = α' @ [x] @ β' ∧ α' ↿ X = α ↿ X ∧ β' ↿ X = β ↿ X)"
proof -
assume "τ ↿ X = (α @ [x] @ β) ↿ X"
and  " x ∈ X"
{
fix n
have "⟦τ ↿ X = (α @ [x] @ β) ↿ X; x ∈ X; n = length(α↿X) ⟧
⟹ ∃ α' β'. (τ = α' @ [x] @ β' ∧ α' ↿ X = α ↿ X ∧ β' ↿ X = β ↿ X)"
proof (induct n arbitrary: τ α )
case 0
hence "α↿X = []"
unfolding projection_def by simp
with "0.prems"(1) "0.prems"(2) have "τ↿X = x # β↿X"
unfolding projection_def by simp
with ‹α↿X = []› show ?case
using projection_split_first_with_suffix by fastforce
next
case (Suc n)
from "Suc.prems"(1) have "τ↿X=α↿X @ ([x] @ β) ↿X"
using projection_concatenation_commute by auto
from "Suc.prems"(3) obtain x' xs' where "α ↿X= x' #xs'"
and "x' ∈ X"
by (metis filter_eq_ConsD length_Suc_conv projection_def)
then obtain a⇩1 a⇩2 where "α = a⇩1 @ [x'] @ a⇩2"
and "a⇩1↿X = []"
and "a⇩2↿X = xs'"
using projection_split_first_with_suffix by metis
with ‹x' ∈ X› "Suc.prems"(1) have "τ↿X= x' #  (a⇩2 @ [x] @ β) ↿X"
unfolding projection_def by simp
then obtain t⇩1 t⇩2 where "τ= t⇩1 @ [x'] @ t⇩2"
and "t⇩1↿X = []"
and "t⇩2↿X = (a⇩2 @ [x] @ β) ↿X"
using projection_split_first_with_suffix by metis
from Suc.prems(3) ‹α ↿X= x' # xs'› ‹α = a⇩1 @ [x'] @ a⇩2› ‹a⇩1↿X = []› ‹a⇩2↿X = xs'›
have "n=length(a⇩2↿X)"
by auto
with "Suc.hyps"(1) "Suc.prems"(2) ‹t⇩2↿X = (a⇩2 @ [x] @ β) ↿X›
obtain t⇩2' t⇩3' where "t⇩2=t⇩2' @ [x] @ t⇩3'"
and "t⇩2'↿X = a⇩2↿X"
and "t⇩3'↿X = β↿X"
using projection_concatenation_commute by blast

let ?α'="t⇩1 @ [x'] @ t⇩2'" and ?β'="t⇩3'"
from ‹τ= t⇩1 @ [x'] @ t⇩2› ‹t⇩2=t⇩2' @ [x] @ t⇩3'› have "τ=?α'@[x]@?β'"
by auto
moreover
from  ‹α ↿X= x' # xs'›  ‹t⇩1↿X = []› ‹x' ∈ X› ‹t⇩2'↿X = a⇩2↿X› ‹a⇩2↿X = xs'›
have "?α'↿X = α↿X"
using projection_concatenation_commute unfolding projection_def by simp
ultimately
show ?case using ‹t⇩3'↿X = β↿X›
by blast
qed
}
with ‹τ ↿ X = (α @ [x] @ β) ↿ X› ‹ x ∈ X› show ?thesis
by simp
qed

(* If the projection of a list l onto a set X is empty, it
will remain empty when projecting further. *)
lemma projection_on_intersection: "l ↿ X = [] ⟹ l ↿ (X ∩ Y) = []"
(is "?L1 = [] ⟹ ?L2 = []")
proof -
assume "?L1 = []"
hence "set ?L1 = {}"
by simp
moreover
have "set ?L2 ⊆ set ?L1"
ultimately have "set ?L2 = {}"
by auto
thus ?thesis
by auto
qed

(* The previous lemma expressed with subsets. *)
lemma projection_on_subset: "⟦ Y ⊆ X; l ↿ X = [] ⟧ ⟹ l ↿ Y = []"
proof -
assume subset: "Y ⊆ X"
assume proj_empty: "l ↿ X = []"
hence "l ↿ (X ∩ Y) = []"
by (rule projection_on_intersection)
moreover
from subset have "X ∩ Y = Y"
by auto
ultimately show ?thesis
by auto
qed

(* Another variant that is used in proofs of BSP compositionality theorems. *)
lemma projection_on_subset2: "⟦ set l ⊆ L; l ↿ X' = []; X ∩ L ⊆ X' ⟧ ⟹ l ↿ X = []"
proof -
assume setl_subset_L: "set l ⊆ L"
assume l_no_X': "l ↿ X' = []"
assume X_inter_L_subset_X': "X ∩ L ⊆ X'"

from X_inter_L_subset_X' l_no_X' have "l ↿ (X ∩ L) = []"
by (rule projection_on_subset)
moreover
have "l ↿ (X ∩ L) = (l ↿ L) ↿ X"
moreover
note setl_subset_L
ultimately show ?thesis
qed

(*If the projection of two lists l1 and l2  onto a set Y is equal then its also equal for all X ⊆ Y*)
lemma non_empty_projection_on_subset: "X ⊆ Y ∧ l⇩1 ↿ Y = l⇩2 ↿ Y ⟹  l⇩1 ↿ X = l⇩2 ↿ X"
by (metis projection_subset_eq_from_superset_eq subset_Un_eq)

(* Intersecting a projection set with a list's elements does not change the result
of the projection. *)
lemma projection_intersection_neutral: "(set l ⊆ X) ⟹ (l ↿ (X ∩ Y) = l ↿ Y)"
proof -
assume "set l ⊆ X"
hence "(l ↿ X) = l"
hence "(l ↿ X) ↿ Y = l ↿ Y"
by simp
moreover
have "(l ↿ X) ↿ Y = l ↿ (X ∩ Y)"
ultimately show ?thesis
by simp
qed

lemma projection_commute:
"(l ↿ X) ↿ Y = (l ↿ Y) ↿ X"

lemma projection_subset_elim: "Y ⊆ X ⟹ (l ↿ X) ↿ Y = l ↿ Y"
by (simp only: projection_def, metis Diff_subset list_subset_iff_projection_neutral
minus_coset_filter order_trans projection_commute projection_def)

lemma projection_sequence: "(xs ↿ X) ↿ Y = (xs ↿ (X ∩ Y))"
by (metis Int_absorb inf_sup_ord(1) list_subset_iff_projection_neutral
projection_intersection_neutral projection_subset_elim)

(* This function yields a possible interleaving for given
traces t1 and t2.
The set A (B) shall denote the the set of events for t1 (t2).
Non-synchronization events in trace t1 are prioritized. *)
fun merge :: "'e set ⇒ 'e set ⇒ 'e list ⇒ 'e list ⇒ 'e list"
where
"merge A B [] t2 = t2" |
"merge A B t1 [] = t1" |
"merge A B (e1 # t1') (e2 # t2') = (if e1 = e2 then
e1 # (merge A B t1' t2')
else (if e1 ∈ (A ∩ B) then
e2 # (merge A B (e1 # t1') t2')
else e1 # (merge A B t1' (e2 # t2'))))"

(* If two traces can be interleaved, then merge yields such an interleaving  *)
lemma merge_property: "⟦set t1 ⊆ A; set t2 ⊆ B; t1 ↿ B = t2 ↿ A ⟧
⟹ let t = (merge A B t1 t2) in (t ↿ A = t1 ∧ t ↿ B = t2 ∧ set t ⊆ ((set t1) ∪ (set t2)))"
unfolding Let_def
proof (induct A B t1 t2 rule: merge.induct)
case (1 A B t2) thus ?case
by (metis Un_empty_left empty_subsetI list_subset_iff_projection_neutral
merge.simps(1) set_empty subset_iff_psubset_eq)
next
case (2 A B t1) thus ?case
by (metis Un_empty_right empty_subsetI list_subset_iff_projection_neutral
merge.simps(2) set_empty subset_refl)
next
case (3 A B e1 t1' e2 t2') thus ?case
proof (cases)
assume e1_is_e2: "e1 = e2"

note e1_is_e2
moreover
from 3(4) have "set t1' ⊆ A"
by auto
moreover
from 3(5) have "set t2' ⊆ B"
by auto
moreover
from e1_is_e2 3(4-6) have "t1' ↿ B = t2' ↿ A"
moreover
note 3(1)
ultimately have ind1: "merge A B t1' t2' ↿ A = t1'"
and ind2: "merge A B t1' t2' ↿ B = t2'"
and ind3: "set (merge A B t1' t2') ⊆ (set t1') ∪ (set t2')"
by auto

from e1_is_e2 have merge_eq:
"merge A B (e1 # t1') (e2 # t2') = e1 # (merge A B t1' t2')"
by auto

from 3(4) ind1 have goal1:
"merge A B (e1 # t1') (e2 # t2') ↿ A = e1 # t1'"
by (simp only: merge_eq projection_def, auto)
moreover
from e1_is_e2 3(5) ind2 have goal2:
"merge A B (e1 # t1') (e2 # t2') ↿ B = e2 # t2'"
by (simp only: merge_eq projection_def, auto)
moreover
from ind3 have goal3:
"set (merge A B (e1 # t1') (e2 # t2')) ⊆ set (e1 # t1') ∪ set (e2 # t2')"
by (simp only: merge_eq, auto)
ultimately show ?thesis
by auto (* case (3 e1 t1' e2 t2') for e1 = e2 *)
next
assume e1_isnot_e2: "e1 ≠ e2"
show ?thesis
proof (cases)
assume e1_in_A_inter_B: "e1 ∈ A ∩ B"

from 3(6) e1_isnot_e2 e1_in_A_inter_B have e2_notin_A: "e2 ∉ A"

note e1_isnot_e2 e1_in_A_inter_B 3(4)
moreover
from 3(5) have "set t2' ⊆ B"
by auto
moreover
from 3(6) e1_isnot_e2 e1_in_A_inter_B have "(e1 # t1') ↿ B = t2' ↿ A"
moreover
note 3(2)
ultimately have ind1: "merge A B (e1 # t1') t2' ↿ A = (e1 # t1')"
and ind2: "merge A B (e1 # t1') t2' ↿ B = t2'"
and ind3: "set (merge A B (e1 # t1') t2') ⊆ set (e1 # t1') ∪ set t2'"
by auto

from e1_isnot_e2 e1_in_A_inter_B
have merge_eq:
"merge A B (e1 # t1') (e2 # t2') = e2 # (merge A B (e1 # t1') t2')"
by auto

from e1_isnot_e2 ind1 e2_notin_A have goal1:
"merge A B (e1 # t1') (e2 # t2') ↿ A = e1 # t1'"
by (simp only: merge_eq projection_def, auto)
moreover
from 3(5) ind2 have goal2: "merge A B (e1 # t1') (e2 # t2') ↿ B = e2 # t2'"
by (simp only: merge_eq projection_def, auto)
moreover
from 3(5) ind3 have goal3:
"set (merge A B (e1 # t1') (e2 # t2')) ⊆ set (e1 # t1') ∪ set (e2 # t2')"
by (simp only: merge_eq, auto)
ultimately show ?thesis
by auto (* case (3 e1 t1' e2 t2') for e1 ≠ e2 e1 ∈ A ∩ B *)
next
assume e1_notin_A_inter_B: "e1 ∉ A ∩ B"

from 3(4) e1_notin_A_inter_B have e1_notin_B: "e1 ∉ B"
by auto

note e1_isnot_e2 e1_notin_A_inter_B
moreover
from 3(4) have "set t1' ⊆ A"
by auto
moreover
note 3(5)
moreover
from 3(6) e1_notin_B have "t1' ↿ B = (e2 # t2') ↿ A"
moreover
note 3(3)
ultimately have ind1: "merge A B t1' (e2 # t2') ↿ A = t1'"
and ind2: "merge A B t1' (e2 # t2') ↿ B = (e2 # t2')"
and ind3: "set (merge A B t1' (e2 # t2')) ⊆ set t1' ∪ set (e2 # t2')"
by auto

from e1_isnot_e2 e1_notin_A_inter_B
have merge_eq: "merge A B (e1 # t1') (e2 # t2') = e1 # (merge A B t1' (e2 # t2'))"
by auto

from 3(4) ind1 have goal1: "merge A B (e1 # t1') (e2 # t2') ↿ A = e1 # t1'"
by (simp only: merge_eq projection_def, auto)
moreover
from ind2 e1_notin_B have goal2:
"merge A B (e1 # t1') (e2 # t2') ↿ B = e2 # t2'"
by (simp only: merge_eq projection_def, auto)
moreover
from 3(4) ind3 have goal3:
"set (merge A B (e1 # t1') (e2 # t2')) ⊆ set (e1 # t1') ∪ set (e2 # t2')"
by (simp only: merge_eq, auto)
ultimately show ?thesis
by auto (* case (3 e1 t1' e2 t2') for e1 ≠ e2 e1 ∉ A ∩ B *)
qed
qed
qed

end


# Theory Prefix

theory Prefix
imports Main
begin

(*
Prefixes and Prefix Closure of traces
*)
definition prefix :: "'e list ⇒ 'e list ⇒ bool" (infixl "≼" 100)
where
"(l1 ≼ l2) ≡ (∃l3. l1 @ l3 = l2)"

definition prefixclosed :: "('e list) set ⇒ bool"
where
"prefixclosed tr ≡ (∀l1 ∈ tr. ∀l2. l2 ≼ l1 ⟶ l2 ∈ tr)"

(* the empty list is a prefix of every list *)
lemma empty_prefix_of_all: "[] ≼ l"
using prefix_def [of "[]" l] by simp

(* the empty list is in any non-empty prefix-closed set *)
lemma empty_trace_contained: "⟦ prefixclosed tr ; tr ≠ {} ⟧ ⟹ [] ∈ tr"
proof -
assume 1: "prefixclosed tr" and
2: "tr ≠ {}"
then obtain l1 where "l1 ∈ tr"
by auto
with 1 have "∀l2. l2 ≼ l1 ⟶ l2 ∈ tr"
thus "[] ∈ tr"
qed

(* the prefix-predicate is transitive *)
lemma transitive_prefix: "⟦ l1 ≼ l2 ; l2 ≼ l3 ⟧ ⟹ l1 ≼ l3"

end


# Theory EventSystems

theory EventSystems
imports "../Basics/Prefix" "../Basics/Projection"
begin

(* structural representation of event systems *)
record 'e ES_rec =
E_ES ::  "'e set"
I_ES ::  "'e set"
O_ES ::  "'e set"
Tr_ES :: "('e list) set"

(* syntax abbreviations for ES_rec *)
abbreviation ESrecEES :: "'e ES_rec ⇒ 'e set"
("E⇘_⇙"  1000)
where
"E⇘ES⇙ ≡ (E_ES ES)"

abbreviation ESrecIES :: "'e ES_rec ⇒ 'e set"
("I⇘_⇙"  1000)
where
"I⇘ES⇙ ≡ (I_ES ES)"

abbreviation ESrecOES :: "'e ES_rec ⇒ 'e set"
("O⇘_⇙"  1000)
where
"O⇘ES⇙ ≡ (O_ES ES)"

abbreviation ESrecTrES :: "'e ES_rec ⇒ ('e list) set"
("Tr⇘_⇙"  1000)
where
"Tr⇘ES⇙ ≡ (Tr_ES ES)"

(* side conditions for event systems *)
definition es_inputs_are_events :: "'e ES_rec ⇒ bool"
where
"es_inputs_are_events ES ≡ I⇘ES⇙ ⊆ E⇘ES⇙"

definition es_outputs_are_events :: "'e ES_rec ⇒ bool"
where
"es_outputs_are_events ES ≡ O⇘ES⇙ ⊆ E⇘ES⇙"

definition es_inputs_outputs_disjoint :: "'e ES_rec ⇒ bool"
where
"es_inputs_outputs_disjoint ES ≡ I⇘ES⇙ ∩ O⇘ES⇙ = {}"

definition traces_contain_events :: "'e ES_rec ⇒ bool"
where
"traces_contain_events ES ≡ ∀l ∈ Tr⇘ES⇙. ∀e ∈ (set l). e ∈ E⇘ES⇙"

definition traces_prefixclosed :: "'e ES_rec ⇒ bool"
where
"traces_prefixclosed ES ≡ prefixclosed Tr⇘ES⇙"

definition ES_valid :: "'e ES_rec ⇒ bool"
where
"ES_valid ES ≡
es_inputs_are_events ES ∧ es_outputs_are_events ES
∧ es_inputs_outputs_disjoint ES ∧ traces_contain_events ES
∧ traces_prefixclosed ES"

(* Event systems are instances of ES_rec that satisfy ES_valid. *)

(* Totality of an event system ES with respect to a set E *)
definition total :: "'e ES_rec ⇒ 'e set ⇒ bool"
where
"total ES E ≡ E ⊆ E⇘ES⇙ ∧ (∀τ ∈ Tr⇘ES⇙. ∀e ∈ E. τ @ [e] ∈ Tr⇘ES⇙)"

lemma totality: "⟦ total ES E; t ∈ Tr⇘ES⇙; set t' ⊆ E ⟧ ⟹ t @ t' ∈ Tr⇘ES⇙"
by (induct t' rule: rev_induct, force, simp only: total_def, auto)

(* structural representation of composed event systems (composition operator) *)
definition composeES :: "'e ES_rec ⇒ 'e ES_rec ⇒ 'e ES_rec"
where
"composeES ES1 ES2 ≡
⦇
E_ES  = E⇘ES1⇙ ∪ E⇘ES2⇙,
I_ES  = (I⇘ES1⇙ - O⇘ES2⇙) ∪ (I⇘ES2⇙ - O⇘ES1⇙),
O_ES  = (O⇘ES1⇙ - I⇘ES2⇙) ∪ (O⇘ES2⇙ - I⇘ES1⇙),
Tr_ES = {τ . (τ ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙ ∧ (τ ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙
∧ (set τ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙)}
⦈"

abbreviation composeESAbbrv :: "'e ES_rec ⇒ 'e ES_rec ⇒ 'e ES_rec"
("_ ∥ _" 1000)
where
"ES1 ∥ ES2 ≡ (composeES ES1 ES2)"

definition composable :: "'e ES_rec ⇒ 'e ES_rec ⇒ bool"
where
"composable ES1 ES2 ≡ (E⇘ES1⇙ ∩ E⇘ES2⇙) ⊆ ((O⇘ES1⇙ ∩ I⇘ES2⇙) ∪ (O⇘ES2⇙ ∩ I⇘ES1⇙))"

(* composing two event systems yields an event system *)
lemma composeES_yields_ES:
"⟦ ES_valid ES1; ES_valid ES2 ⟧ ⟹ ES_valid (ES1 ∥ ES2)"
unfolding ES_valid_def
proof (auto)
assume ES1_inputs_are_events: "es_inputs_are_events ES1"
assume ES2_inputs_are_events: "es_inputs_are_events ES2"
show "es_inputs_are_events (ES1 ∥ ES2)" unfolding composeES_def es_inputs_are_events_def
proof (simp)
have subgoal11: "I⇘ES1⇙ - O⇘ES2⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙"
proof (auto)
fix x
assume "x ∈ I⇘ES1⇙"
with ES1_inputs_are_events  show "x ∈ E⇘ES1⇙"
qed
have subgoal12: "I⇘ES2⇙ - O⇘ES1⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙"
proof (rule subsetI, rule UnI2, auto)
fix x
assume "x ∈ I⇘ES2⇙"
with ES2_inputs_are_events show "x ∈ E⇘ES2⇙"
qed
from subgoal11 subgoal12
show "I⇘ES1⇙ - O⇘ES2⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙ ∧ I⇘ES2⇙ - O⇘ES1⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙" ..
qed
next
assume ES1_outputs_are_events: "es_outputs_are_events ES1"
assume ES2_outputs_are_events: "es_outputs_are_events ES2"
show "es_outputs_are_events (ES1 ∥ ES2)"
unfolding composeES_def es_outputs_are_events_def
proof (simp)
have subgoal21: "O⇘ES1⇙ - I⇘ES2⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙"
proof (auto)
fix x
assume "x ∈ O⇘ES1⇙"
with ES1_outputs_are_events  show "x ∈ E⇘ES1⇙"
qed
have subgoal22: "O⇘ES2⇙ - I⇘ES1⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙"
proof (rule subsetI, rule UnI2, auto)
fix x
assume "x ∈ O⇘ES2⇙"
with ES2_outputs_are_events show "x ∈ E⇘ES2⇙"
qed
from subgoal21 subgoal22
show "O⇘ES1⇙ - I⇘ES2⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙ ∧ O⇘ES2⇙ - I⇘ES1⇙ ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙" ..
qed
next
assume ES1_inputs_outputs_disjoint: "es_inputs_outputs_disjoint ES1"
assume ES2_inputs_outputs_disjoint: "es_inputs_outputs_disjoint ES2"
show "es_inputs_outputs_disjoint (ES1 ∥ ES2)"
unfolding composeES_def es_inputs_outputs_disjoint_def
proof (simp)
have subgoal31:
"{} ⊆ (I⇘ES1⇙ - O⇘ES2⇙ ∪ (I⇘ES2⇙ - O⇘ES1⇙)) ∩ (O⇘ES1⇙ - I⇘ES2⇙ ∪ (O⇘ES2⇙ - I⇘ES1⇙))"
by auto
have subgoal32:
"(I⇘ES1⇙ - O⇘ES2⇙ ∪ (I⇘ES2⇙ - O⇘ES1⇙)) ∩ (O⇘ES1⇙ - I⇘ES2⇙ ∪ (O⇘ES2⇙ - I⇘ES1⇙)) ⊆ {}"
proof (rule subsetI, erule IntE)
fix x
assume ass1: "x ∈ I⇘ES1⇙ - O⇘ES2⇙ ∪ (I⇘ES2⇙ - O⇘ES1⇙)"
then have ass1': "x ∈ I⇘ES1⇙ - O⇘ES2⇙ ∨ x ∈ (I⇘ES2⇙ - O⇘ES1⇙)"
by auto
assume ass2: "x ∈ O⇘ES1⇙ - I⇘ES2⇙ ∪ (O⇘ES2⇙ - I⇘ES1⇙)"
then have ass2':"x ∈ O⇘ES1⇙ - I⇘ES2⇙ ∨ x ∈ (O⇘ES2⇙ - I⇘ES1⇙)"
by auto
note ass1'
moreover {
assume left1: "x ∈ I⇘ES1⇙ - O⇘ES2⇙"
note ass2'
moreover {
assume left2: "x ∈ O⇘ES1⇙ - I⇘ES2⇙"
with left1 have "x∈ (I⇘ES1⇙) ∩ (O⇘ES1⇙)"
by (auto)
with ES1_inputs_outputs_disjoint have "x∈{}"
}
moreover {
assume right2: "x ∈ (O⇘ES2⇙ - I⇘ES1⇙)"
with left1 have "x∈ (I⇘ES1⇙ - I⇘ES1⇙)"
by auto
hence "x∈{}"
by auto
}
ultimately have "x∈{}" ..
}
moreover {
assume right1: "x ∈ I⇘ES2⇙ - O⇘ES1⇙"
note ass2'
moreover {
assume left2: "x ∈ O⇘ES1⇙ - I⇘ES2⇙"
with right1 have "x∈ (I⇘ES2⇙ - I⇘ES2⇙)"
by auto
hence "x∈{}"
by auto
}
moreover {
assume right2: "x ∈ (O⇘ES2⇙ - I⇘ES1⇙)"
with right1 have "x ∈ (I⇘ES2⇙ ∩ O⇘ES2⇙)"
by auto
with ES2_inputs_outputs_disjoint have "x∈{}"
}
ultimately have "x∈{}" ..
}
ultimately show "x∈{}" ..
qed

from subgoal31 subgoal32
show "(I⇘ES1⇙ - O⇘ES2⇙ ∪ (I⇘ES2⇙ - O⇘ES1⇙)) ∩ (O⇘ES1⇙ - I⇘ES2⇙ ∪ (O⇘ES2⇙ - I⇘ES1⇙)) = {}"
by auto
qed
next
show "traces_contain_events (ES1 ∥ ES2)" unfolding composeES_def traces_contain_events_def
proof (clarsimp)
fix l e
assume "e ∈ set l"
and "set l ⊆ E⇘ES1⇙ ∪ E⇘ES2⇙"
then have e_in_union: "e ∈ E⇘ES1⇙ ∪ E⇘ES2⇙"
by auto
assume "e ∉ E⇘ES2⇙"
with e_in_union show "e ∈ E⇘ES1⇙"
by auto
qed
next
assume ES1_traces_prefixclosed: "traces_prefixclosed ES1"
assume ES2_traces_prefixclosed: "traces_prefixclosed ES2"
show "traces_prefixclosed (ES1 ∥ ES2)"
unfolding composeES_def traces_prefixclosed_def prefixclosed_def prefix_def
proof (clarsimp)
fix l2 l3
have l2l3split: "(l2 @ l3) ↿ E⇘ES1⇙ = (l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙)"
by (rule projection_concatenation_commute)
assume "(l2 @ l3) ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙"
with l2l3split have l2l3cattrace: "(l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by auto
have theprefix: "(l2 ↿ E⇘ES1⇙) ≼ ((l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙))"
have prefixclosure: "∀ es1 ∈ (Tr⇘ES1⇙). ∀ es2. es2 ≼ es1 ⟶ es2 ∈ (Tr⇘ES1⇙)"
by (clarsimp, insert ES1_traces_prefixclosed, unfold traces_prefixclosed_def prefixclosed_def,
erule_tac x="es1" in ballE, erule_tac x="es2" in allE, erule impE, auto)
hence
" ((l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙)) ∈ Tr⇘ES1⇙ ⟹ ∀ es2. es2 ≼ ((l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙))
⟶ es2 ∈ Tr⇘ES1⇙" ..
with l2l3cattrace have "∀ es2. es2 ≼ ((l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙)) ⟶ es2 ∈ Tr⇘ES1⇙"
by auto
hence "(l2 ↿ E⇘ES1⇙) ≼ ((l2 ↿ E⇘ES1⇙) @ (l3 ↿ E⇘ES1⇙)) ⟶ (l2 ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙" ..
with theprefix have goal51: "(l2 ↿ E⇘ES1⇙) ∈ Tr⇘ES1⇙"
by simp
have l2l3split: "(l2 @ l3) ↿ E⇘ES2⇙ = (l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙)"
by (rule projection_concatenation_commute)
assume "(l2 @ l3) ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙"
with l2l3split have l2l3cattrace: "(l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by auto
have theprefix: "(l2 ↿ E⇘ES2⇙) ≼ ((l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙))"
have prefixclosure: "∀ es1 ∈ Tr⇘ES2⇙. ∀es2. es2 ≼ es1 ⟶ es2 ∈ Tr⇘ES2⇙"
by (clarsimp, insert ES2_traces_prefixclosed,
unfold traces_prefixclosed_def prefixclosed_def,
erule_tac x="es1" in ballE, erule_tac x="es2" in allE, erule impE, auto)
hence " ((l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙)) ∈ Tr⇘ES2⇙
⟹ ∀ es2. es2 ≼ ((l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙)) ⟶ es2 ∈ Tr⇘ES2⇙" ..
with l2l3cattrace have "∀ es2. es2 ≼ ((l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙)) ⟶ es2 ∈ Tr⇘ES2⇙"
by auto
hence "(l2 ↿ E⇘ES2⇙) ≼ ((l2 ↿ E⇘ES2⇙) @ (l3 ↿ E⇘ES2⇙)) ⟶ (l2 ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙" ..
with theprefix have goal52: "(l2 ↿ E⇘ES2⇙) ∈ Tr⇘ES2⇙"
by simp
from goal51 goal52 show goal5: "l2 ↿ E⇘ES1⇙ ∈ Tr⇘ES1⇙ ∧ l2 ↿ E⇘ES2⇙ ∈ Tr⇘ES2⇙" ..
qed
qed

end


# Theory StateEventSystems

theory StateEventSystems
imports EventSystems
begin

(* structural representation of state event systems *)
record ('s, 'e) SES_rec =
S_SES ::  "'s set"
s0_SES :: "'s"
E_SES ::  "'e set"
I_SES ::  "'e set"
O_SES ::  "'e set"
T_SES ::  "'s ⇒ 'e ⇀ 's"

(* syntax abbreviations for SES_rec *)
abbreviation SESrecSSES :: "('s, 'e) SES_rec ⇒ 's set"
("S⇘_⇙"  1000)
where
"S⇘SES⇙ ≡ (S_SES SES)"

abbreviation SESrecs0SES :: "('s, 'e) SES_rec ⇒ 's"
("s0⇘_⇙"  1000)
where
"s0⇘SES⇙ ≡ (s0_SES SES)"

abbreviation SESrecESES :: "('s, 'e) SES_rec ⇒ 'e set"
("E⇘_⇙"  1000)
where
"E⇘SES⇙ ≡ (E_SES SES)"

abbreviation SESrecISES :: "('s, 'e) SES_rec ⇒ 'e set"
("I⇘_⇙"  1000)
where
"I⇘SES⇙ ≡ (I_SES SES)"

abbreviation SESrecOSES :: "('s, 'e) SES_rec ⇒ 'e set"
("O⇘_⇙"  1000)
where
"O⇘SES⇙ ≡ (O_SES SES)"

abbreviation SESrecTSES :: "('s, 'e) SES_rec ⇒ ('s ⇒ 'e ⇀ 's)"
("T⇘_⇙"  1000)
where
"T⇘SES⇙ ≡ (T_SES SES)"

abbreviation TSESpred :: "'s ⇒ 'e ⇒ ('s, 'e) SES_rec ⇒ 's ⇒ bool"
("_ _⟶⇘_⇙ _" [100,100,100,100] 100)
where
"s e⟶⇘SES⇙ s' ≡ (T⇘SES⇙ s e = Some s')"

(* side conditions for state event systems *)
definition s0_is_state :: "('s, 'e) SES_rec ⇒ bool"
where
"s0_is_state SES ≡ s0⇘SES⇙ ∈ S⇘SES⇙"

definition ses_inputs_are_events :: "('s, 'e) SES_rec ⇒ bool"
where
"ses_inputs_are_events SES ≡ I⇘SES⇙ ⊆ E⇘SES⇙"

definition ses_outputs_are_events :: "('s, 'e) SES_rec ⇒ bool"
where
"ses_outputs_are_events SES ≡ O⇘SES⇙ ⊆ E⇘SES⇙"

definition ses_inputs_outputs_disjoint :: "('s, 'e) SES_rec ⇒ bool"
where
"ses_inputs_outputs_disjoint SES ≡ I⇘SES⇙ ∩ O⇘SES⇙ = {}"

definition correct_transition_relation :: "('s, 'e) SES_rec ⇒ bool"
where
"correct_transition_relation SES ≡
∀x y z. x y⟶⇘SES⇙ z ⟶ ((x ∈ S⇘SES⇙) ∧ (y ∈ E⇘SES⇙) ∧ (z ∈ S⇘SES⇙))"

(* State event systems are instances of SES_rec that satisfy SES_valid. *)
definition SES_valid :: "('s, 'e) SES_rec ⇒ bool"
where
"SES_valid SES ≡
s0_is_state SES ∧ ses_inputs_are_events SES
∧ ses_outputs_are_events SES ∧ ses_inputs_outputs_disjoint SES ∧
correct_transition_relation SES"

(* auxiliary definitions for state event systems *)

(* Paths in state event systems *)
primrec path :: "('s, 'e) SES_rec ⇒ 's ⇒ 'e list ⇀ 's"
where
path_empt: "path SES s1 [] = (Some s1)" |
path_nonempt: "path SES s1 (e # t) =
(if (∃s2. s1 e⟶⇘SES⇙ s2)
then (path SES (the (T⇘SES⇙ s1 e)) t)
else None)"

abbreviation pathpred :: "'s ⇒ 'e list ⇒ ('s, 'e) SES_rec ⇒ 's ⇒ bool"
("_ _⟹⇘_⇙ _" [100, 100, 100, 100] 100)
where
"s t⟹⇘SES⇙ s' ≡ path SES s t = Some s'"

(* A state s is reachable in a state event system if there is a path from the initial state
of the state event system to state s. *)
definition reachable :: "('s, 'e) SES_rec ⇒ 's ⇒ bool"
where
"reachable SES s ≡ (∃t. s0⇘SES⇙ t⟹⇘SES⇙ s)"

(* A trace t is enabled in a state s if there is a path t from s to some other state.*)
definition enabled :: "('s, 'e) SES_rec ⇒ 's ⇒ 'e list ⇒ bool"
where
"enabled SES s t ≡ (∃s'. s t⟹⇘SES⇙ s')"

(* The set of possible traces in a state event system SES is the set of traces that are enabled in
the initial state of SES. *)
definition possible_traces :: "('s, 'e) SES_rec ⇒ ('e list) set"
where
"possible_traces SES ≡ {t. (enabled SES s0⇘SES⇙ t)}"

(* structural representation of the event system induced by a state event system *)
definition induceES :: "('s, 'e) SES_rec ⇒ 'e ES_rec"
where
"induceES SES ≡
⦇
E_ES = E⇘SES⇙,
I_ES = I⇘SES⇙,
O_ES  = O⇘SES⇙,
Tr_ES = possible_traces SES
⦈"
(* auxiliary lemmas for state event systems *)

(* If some event sequence is not enabled in a state,
then it will not become possible by appending events. *)
lemma none_remains_none : "⋀ s e. (path SES s t) = None
⟹ (path SES s (t @ [e])) = None"
by (induct t, auto)

(* If some event sequence t is enabled in a state s in which
some event e is not enabled, then the event sequence
obtained by appending e to t is not enabled in s. *)
lemma path_trans_single_neg: "⋀ s1. ⟦s1 t⟹⇘SES⇙ s2; ¬ (s2 e⟶⇘SES⇙ sn)⟧
⟹ ¬ (s1 (t @ [e])⟹⇘SES⇙ sn)"
by (induct t, auto)

(* If the event sequence t:e is enabled in some state, then
the event sequence t is also enabled and results in some state t' *)
lemma path_split_single: "s1 (t@[e])⟹⇘SES⇙ sn
⟹ ∃s'. s1 t⟹⇘SES⇙ s'  ∧ s' e⟶⇘SES⇙ sn"
by (cases "path SES s1 t", simp add: none_remains_none,
simp, rule ccontr, auto simp add: path_trans_single_neg)

(* If an event sequence results in a state s', from which the event e results in sn,
then the combined event sequence also results in sn *)
lemma path_trans_single: "⋀s. ⟦ s t⟹⇘SES⇙ s'; s' e⟶⇘SES⇙ sn ⟧
⟹ s (t @ [e])⟹⇘SES⇙ sn"
proof (induct t)
case Nil thus ?case by auto
next
case (Cons a t) thus ?case
proof -
from Cons obtain s1' where trans_s_a_s1': "s a⟶⇘SES⇙ s1'"
by (simp, split if_split_asm, auto)
with Cons have "s1' (t @ [e])⟹⇘SES⇙ sn"
by auto
with trans_s_a_s1' show ?thesis
by auto
qed
qed

(* We can split a path from s1 to sn via the event sequence t1:t2
into two paths from s1 to s2 via t1 and from s2 to sn via t2  *)
lemma path_split: "⋀ sn. ⟦ s1 (t1 @ t2)⟹⇘SES⇙ sn ⟧
⟹ (∃s2. (s1 t1⟹⇘SES⇙ s2 ∧ s2 t2⟹⇘SES⇙ sn))"
proof (induct t2 rule: rev_induct)
case Nil thus ?case by auto
next
case (snoc a t) thus ?case
proof -
from snoc have "s1 (t1 @ t @ [a])⟹⇘SES⇙ sn"
by auto
hence "∃sn'. s1 (t1 @ t)⟹⇘SES⇙ sn' ∧ sn' a⟶⇘SES⇙ sn"
then obtain sn' where path_t1_t_trans_a:
"s1 (t1 @ t)⟹⇘SES⇙ sn' ∧ sn' a⟶⇘SES⇙ sn"
by auto
with snoc obtain s2 where path_t1_t:
"s1 t1⟹⇘SES⇙ s2 ∧ s2 t⟹⇘SES⇙ sn'"
by auto
with path_t1_t_trans_a have "s2 (t @ [a])⟹⇘SES⇙ sn"
with path_t1_t show ?thesis by auto
qed
qed

(* Two paths can be concatenated. *)
lemma path_trans:
"⋀sn. ⟦ s1 l1⟹⇘SES⇙ s2; s2 l2⟹⇘SES⇙ sn ⟧ ⟹ s1 (l1 @ l2)⟹⇘SES⇙ sn"
proof (induct l2 rule: rev_induct)
case Nil thus ?case by auto
next
case (snoc a l) thus ?case
proof -
assume path_l1: "s1 l1⟹⇘SES⇙ s2"
assume "s2 (l@[a])⟹⇘SES⇙ sn"
hence "∃sn'. s2 l⟹⇘SES⇙ sn' ∧ sn' [a]⟹⇘SES⇙ sn"
by (simp add: path_split del: path_nonempt)
then obtain sn' where path_l_a: "s2 l⟹⇘SES⇙ sn' ∧ sn' [a]⟹⇘SES⇙ sn"
by auto
with snoc path_l1 have path_l1_l: "s1 (l1@l)⟹⇘SES⇙ sn'"
by auto
with path_l_a have "sn' a⟶⇘SES⇙ sn"
by (simp, split if_split_asm, auto)
with path_l1_l show "s1 (l1 @ l @ [a])⟹⇘SES⇙ sn"
by (subst append_assoc[symmetric], rule_tac s'="sn'" in path_trans_single, auto)
qed
qed

(* The prefix of an enabled trace is also enabled. (This lemma cuts of the last element.) *)
lemma enabledPrefixSingle : "⟦ enabled SES s (t@[e]) ⟧ ⟹ enabled SES s t"
unfolding enabled_def
proof -
assume ass: "∃s'. s (t @ [e])⟹⇘SES⇙ s'"
from ass obtain s' where "s (t @ [e])⟹⇘SES⇙ s'" ..
hence "∃t'. (s t⟹⇘SES⇙ t') ∧ (t' e⟶⇘SES⇙ s')"
by (rule path_split_single)
then obtain t' where "s t⟹⇘SES⇙ t'"
by (auto)
thus "∃s'. s t⟹⇘SES⇙ s'" ..
qed

(* The prefix of an enabled trace is also enabled.
(This lemma cuts of a suffix trace.) *)
lemma enabledPrefix : "⟦ enabled SES s (t1 @ t2) ⟧ ⟹ enabled SES s t1"
unfolding enabled_def
proof -
assume ass: "∃s'. s (t1 @ t2)⟹⇘SES⇙ s'"
from ass obtain s' where "s (t1 @ t2)⟹⇘SES⇙ s'" ..
hence "∃t. (s t1⟹⇘SES⇙ t ∧ t t2⟹⇘SES⇙ s')"
by (rule path_split)
then obtain t where "s t1⟹⇘SES⇙ t"
by (auto)
then show "∃s'. s t1⟹⇘SES⇙ s'" ..
qed

(* The last element of an enabled trace makes a transition between two states. *)
lemma enabledPrefixSingleFinalStep : "⟦ enabled SES s (t@[e]) ⟧ ⟹ ∃ t' t''. t' e⟶⇘SES⇙ t''"
unfolding enabled_def
proof -
assume ass: "∃s'. s (t @ [e])⟹⇘SES⇙ s'"
from ass obtain s' where "s (t @ [e])⟹⇘SES⇙ s'" ..
hence "∃t'. (s t⟹⇘SES⇙ t')  ∧ (t' e⟶⇘SES⇙ s')"
by (rule path_split_single)
then obtain t' where "t' e⟶⇘SES⇙ s'"
by (auto)
thus "∃t' t''. t' e⟶⇘SES⇙ t''"
by (auto)
qed

(* applying induceES on a state event system yields an event system *)
lemma induceES_yields_ES:
"SES_valid SES ⟹ ES_valid (induceES SES)"
proof (simp add: SES_valid_def ES_valid_def, auto)
assume SES_inputs_are_events: "ses_inputs_are_events SES"
thus "es_inputs_are_events (induceES SES)"
by (simp add: induceES_def ses_inputs_are_events_def es_inputs_are_events_def)
next
assume SES_outputs_are_events: "ses_outputs_are_events SES"
thus "es_outputs_are_events (induceES SES)"
by (simp add: induceES_def ses_outputs_are_events_def es_outputs_are_events_def)
next
assume SES_inputs_outputs_disjoint: "ses_inputs_outputs_disjoint SES"
thus "es_inputs_outputs_disjoint (induceES SES)"
by (simp add: induceES_def ses_inputs_outputs_disjoint_def es_inputs_outputs_disjoint_def)
next
assume SES_correct_transition_relation: "correct_transition_relation SES"
thus "traces_contain_events (induceES SES)"
unfolding induceES_def traces_contain_events_def possible_traces_def
proof (auto)
fix l e
assume enabled_l: "enabled SES s0⇘SES⇙ l"
assume e_in_l: "e ∈ set l"
from enabled_l e_in_l show "e ∈ E⇘SES⇙"
proof (induct l rule: rev_induct)
case Nil
assume e_in_empty_list: "e ∈ set []"
hence f: "False"
by (auto)
thus ?case
by auto
next
case (snoc a l)
from snoc.prems have l_enabled: "enabled SES s0⇘SES⇙ l"
show ?case
proof  (cases "e ∈ (set l)")
from snoc.hyps l_enabled show "e ∈ set l ⟹ e ∈ E⇘SES⇙"
by auto
show "e ∉ set l ⟹ e ∈ E⇘SES⇙"
proof -
assume "e ∉ set l"
with snoc.prems have e_eq_a : "e=a"
by auto
from snoc.prems have "∃ t t'. t a⟶⇘SES⇙ t'"
then obtain t t' where "t a⟶⇘SES⇙ t'"
by auto
with e_eq_a SES_correct_transition_relation show "e ∈ E⇘SES⇙"
qed
qed
qed
qed
next
show "traces_prefixclosed (induceES SES)"
unfolding traces_prefixclosed_def prefixclosed_def induceES_def possible_traces_def prefix_def
qed

end


# Theory Views

theory Views
imports Main
begin

(* structural representation of views *)
record 'e V_rec =
V :: "'e set"
N :: "'e set"
C :: "'e set"

(* syntax abbreviations for V_rec *)
abbreviation VrecV :: "'e V_rec ⇒ 'e set"
("V⇘_⇙"  1000)
where
"V⇘v⇙ ≡ (V v)"

abbreviation VrecN :: "'e V_rec ⇒ 'e set"
("N⇘_⇙"  1000)
where
"N⇘v⇙ ≡ (N v)"

abbreviation VrecC :: "'e V_rec ⇒ 'e set"
("C⇘_⇙"  1000)
where
"C⇘v⇙ ≡ (C v)"

(* side conditions for views *)
definition VN_disjoint :: "'e V_rec ⇒ bool"
where
"VN_disjoint v ≡ V⇘v⇙ ∩ N⇘v⇙ = {}"

definition VC_disjoint :: "'e V_rec ⇒ bool"
where
"VC_disjoint v ≡ V⇘v⇙ ∩ C⇘v⇙ = {}"

definition NC_disjoint :: "'e V_rec ⇒ bool"
where
"NC_disjoint v ≡ N⇘v⇙ ∩ C⇘v⇙ = {}"

(* Views are instances of V_rec that satisfy V_valid. *)
definition V_valid :: "'e V_rec ⇒ bool"
where
"V_valid  v ≡ VN_disjoint v ∧ VC_disjoint v ∧ NC_disjoint v"

(* A view is a view on a set of events iff it covers exactly those events and is a valid view*)
definition isViewOn :: "'e V_rec ⇒ 'e set ⇒ bool"
where
"isViewOn 𝒱 E ≡ V_valid 𝒱 ∧ V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙ = E"

end


# Theory FlowPolicies

theory FlowPolicies
imports Views
begin

(*
Flow policies
*)
record 'domain FlowPolicy_rec =
D :: "'domain set"
v_rel :: "('domain × 'domain) set"
n_rel :: "('domain × 'domain) set"
c_rel :: "('domain × 'domain) set"
(*
The three relations of a flow policy form a partition of DxD.
Moreover, the relation v_rel is reflexive.
*)
definition FlowPolicy :: "'domain FlowPolicy_rec ⇒ bool"
where
"FlowPolicy fp ≡
((v_rel fp) ∪ (n_rel fp) ∪ (c_rel fp) = ((D fp) × (D fp)))
∧ (v_rel fp) ∩ (n_rel fp) = {}
∧ (v_rel fp) ∩ (c_rel fp) = {}
∧ (n_rel fp) ∩ (c_rel fp) = {}
∧ (∀d ∈ (D fp). (d, d) ∈ (v_rel fp))"

(*
Domain assignments and the view of a domain
*)
type_synonym ('e, 'domain) dom_type = "'e ⇀ 'domain"

(*
A domain assignment should only assign domains to actual events.
*)
definition dom :: "('e, 'domain) dom_type ⇒ 'domain set ⇒ 'e set ⇒ bool"
where
"dom domas dset es ≡
(∀e. ∀d. ((domas e = Some d) ⟶ (e ∈ es ∧ d ∈ dset)))"

(*
The combination of a domain assignment and a flow policy
yields a view for each domain.
*)
definition view_dom :: "'domain FlowPolicy_rec ⇒ 'domain ⇒ ('e, 'domain) dom_type ⇒ 'e V_rec"
where
"view_dom fp d domas ≡
⦇ V = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (v_rel fp))},
N = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (n_rel fp))},
C = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (c_rel fp))} ⦈"

end


# Theory BasicSecurityPredicates

theory BasicSecurityPredicates
imports Views "../Basics/Projection"
begin

(*Auxiliary predicate capturing that a a set of traces consists
only of traces of a given set of events *)
definition areTracesOver :: "('e list) set ⇒ 'e set ⇒ bool "
where
"areTracesOver Tr E ≡
∀ τ ∈ Tr. (set τ) ⊆ E"

(* Basic Security Predicates are properties of sets of traces
that are parameterized with a view *)
type_synonym 'e BSP = "'e V_rec ⇒ (('e list) set) ⇒ bool"

(* Basic Security Predicates are valid if and only if they are closure property of sets of traces
for arbitrary views and sets of traces *)
definition BSP_valid :: "'e BSP ⇒ bool"
where
"BSP_valid bsp ≡
∀𝒱 Tr E. ( isViewOn 𝒱 E ∧ areTracesOver Tr E )
⟶ (∃ Tr'. Tr' ⊇ Tr  ∧ bsp 𝒱 Tr')"

(* Removal of Confidential Events (R) *)
definition R :: "'e BSP"
where
"R 𝒱 Tr ≡
∀τ∈Tr. ∃τ'∈Tr. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"

lemma BSP_valid_R: "BSP_valid R"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "R 𝒱 ?Tr'"
proof -
{
fix τ
assume "τ ∈ {t. (set t) ⊆ E}"
let ?τ'="τ↿(V⇘𝒱⇙)"
have "?τ' ↿ C⇘𝒱⇙ = []  ∧ ?τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
using ‹isViewOn 𝒱 E›  disjoint_projection projection_idempotent
unfolding isViewOn_def V_valid_def VC_disjoint_def  by metis
moreover
from ‹τ ∈ {t. (set t) ⊆ E}› have "?τ' ∈ ?Tr'" using ‹isViewOn 𝒱 E›
unfolding isViewOn_def
ultimately
have " ∃τ'∈{t. set t ⊆ E}. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
by auto
}
thus ?thesis unfolding R_def
by auto
qed
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ R 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Deletion of Confidential Events (D) *)
definition D :: "'e BSP"
where
"D 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [])
⟶ (∃α' β'. ((β' @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []
∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)))"

lemma BSP_valid_D: "BSP_valid D"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "D 𝒱 ?Tr'"
unfolding D_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ D 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Insertion of Confidential Events (I) *)
definition I :: "'e BSP"
where
"I 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [])
⟶ (∃α' β'. ((β' @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []
∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)))"

lemma BSP_valid_I: "BSP_valid I"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "I 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
unfolding isViewOn_def I_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ I 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

type_synonym 'e Rho = "'e V_rec ⇒ 'e set"

definition
Adm :: "'e V_rec ⇒ 'e Rho ⇒ ('e list) set ⇒ 'e list ⇒ 'e ⇒ bool"
where
"Adm 𝒱 ρ Tr β e ≡
∃γ. ((γ @ [e]) ∈ Tr ∧ γ↿(ρ 𝒱) = β↿(ρ 𝒱))"

(* Insertion of Admissible Confidential Events (IA) *)
definition IA :: "'e Rho ⇒ 'e BSP"
where
"IA ρ 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c))
⟶ (∃ α' β'. ((β' @ [c] @ α') ∈ Tr) ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙
∧ α'↿C⇘𝒱⇙ = [] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙))"

lemma BSP_valid_IA: "BSP_valid (IA ρ) "
proof -
{
fix 𝒱 :: "('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "IA ρ 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
unfolding isViewOn_def IA_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ IA ρ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Backwards Strict Deletion of Confidential Events (BSD) *)
definition BSD :: "'e BSP"
where
"BSD 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [])
⟶ (∃α'. ((β @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSD: "BSP_valid BSD"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "BSD 𝒱 ?Tr'"
unfolding BSD_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSD 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Backwards Strict Insertion of Confidential Events (BSI) *)
definition BSI :: "'e BSP"
where
"BSI 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [])
⟶ (∃α'. ((β @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSI: "BSP_valid BSI"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "BSI 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
unfolding isViewOn_def BSI_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSI 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Backwards Strict Insertion of Admissible Confidential Events (BSIA) *)
definition BSIA :: "'e Rho ⇒ 'e BSP"
where
"BSIA ρ 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c))
⟶ (∃α'. ((β @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSIA: "BSP_valid (BSIA ρ) "
proof -
{
fix 𝒱 :: "('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "BSIA ρ 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
unfolding isViewOn_def BSIA_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSIA ρ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Forward Correctable BSPs *)
record 'e Gamma =
Nabla :: "'e set"
Delta :: "'e set"
Upsilon :: "'e set"

(* syntax abbreviations for Gamma *)
abbreviation GammaNabla :: "'e Gamma ⇒ 'e set"
("∇⇘_⇙"  1000)
where
"∇⇘Γ⇙ ≡ (Nabla Γ)"

abbreviation GammaDelta :: "'e Gamma ⇒ 'e set"
("Δ⇘_⇙"  1000)
where
"Δ⇘Γ⇙ ≡ (Delta Γ)"

abbreviation GammaUpsilon :: "'e Gamma ⇒ 'e set"
("Υ⇘_⇙"  1000)
where
"Υ⇘Γ⇙ ≡ (Upsilon Γ)"

(* Forward Correctable Deletion of Confidential Events (FCD) *)
definition FCD :: "'e Gamma ⇒ 'e BSP"
where
"FCD Γ 𝒱 Tr ≡
∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙).
((β @ [c,v] @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = [])
⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)
∧ ((β @ δ' @ [v] @ α') ∈ Tr
∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCD: "BSP_valid (FCD Γ)"
proof -
{
fix 𝒱::"('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "FCD Γ 𝒱 ?Tr'"
proof -
{
fix α β c v
assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and  "β @ [c ,v] @ α ∈ ?Tr'"
and  "α ↿ C⇘𝒱⇙ = []"
let ?α'="α" and ?δ'="[]"
from ‹β @ [c ,v] @ α ∈ ?Tr'› have "β @ ?δ' @ [v] @ ?α' ∈ ?Tr'"
by auto
hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ ?δ' @ [v] @ ?α') ∈ ?Tr'
∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"
using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []›
unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
hence "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ δ' @ [v] @ α') ∈ ?Tr'
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by blast
}
thus ?thesis
unfolding FCD_def by auto
qed
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCD Γ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Forward Correctable Insertion of Confidential Events (FCI) *)
definition FCI :: "'e Gamma ⇒ 'e BSP"
where
"FCI Γ 𝒱 Tr ≡
∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙).
((β @ [v] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [])
⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)
∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr
∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCI: "BSP_valid (FCI Γ)"
proof -
{
fix 𝒱::"('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "FCI Γ 𝒱 ?Tr'"
proof -
{
fix α β c v
assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and  "β @ [v] @ α ∈ ?Tr'"
and  "α ↿ C⇘𝒱⇙ = []"
let ?α'="α" and ?δ'="[]"
from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have" c ∈ E"
using ‹isViewOn 𝒱 E›
unfolding isViewOn_def by auto
with  ‹β @ [v] @ α ∈ ?Tr'› have "β @ [c] @ ?δ' @ [v] @ ?α' ∈ ?Tr'"
by auto
hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ ?δ' @ [v] @ ?α') ∈ ?Tr'
∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"
using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []›  unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
hence
"∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ ?Tr'
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by blast
}
thus ?thesis
unfolding FCI_def by auto
qed
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCI Γ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Forward correctable Insertion of Admissible Confidential Events (FCIA) *)
definition FCIA :: "'e Rho ⇒ 'e Gamma ⇒ 'e BSP"
where
"FCIA ρ Γ 𝒱 Tr ≡
∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙).
((β @ [v] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c))
⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)
∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr
∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCIA: "BSP_valid (FCIA ρ Γ) "
proof -
{
fix 𝒱 :: "('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "FCIA ρ Γ 𝒱 ?Tr'"
proof -
{
fix α β c v
assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
and  "β @ [v] @ α ∈ ?Tr'"
and  "α ↿ C⇘𝒱⇙ = []"
let ?α'="α" and ?δ'="[]"
from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have" c ∈ E"
using ‹isViewOn 𝒱 E› unfolding isViewOn_def by auto
with  ‹β @ [v] @ α ∈ ?Tr'› have "β @ [c] @ ?δ' @ [v] @ ?α' ∈ ?Tr'"
by auto
hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ ?δ' @ [v] @ ?α') ∈ ?Tr'
∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"
using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []›
unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
hence
"∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ ?Tr'
∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
by blast
}
thus ?thesis
unfolding FCIA_def by auto
qed
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCIA ρ Γ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Strict Removal of Confidential Events (SR) *)
definition SR :: "'e BSP"
where
"SR 𝒱 Tr ≡ ∀τ∈Tr. τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr"

lemma "BSP_valid SR"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. ∃τ ∈ Tr. t=τ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)} ∪ Tr"
have "?Tr'⊇ Tr"
by blast
moreover
have "SR 𝒱 ?Tr'" unfolding SR_def
proof
fix τ
assume "τ ∈ ?Tr'"
{
from ‹τ ∈ ?Tr'› have "(∃t∈Tr. τ = t ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)) ∨ τ ∈ Tr"
by auto
hence "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ ?Tr'"
proof
assume "∃t∈Tr. τ = t ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
hence "∃t∈Tr. τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)= t ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
using projection_idempotent by metis
thus ?thesis
by auto
next
assume "τ ∈ Tr"
thus ?thesis
by auto
qed
}
thus "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ ?Tr'"
by auto
qed
ultimately
have "∃ Tr'. Tr' ⊇ Tr  ∧ SR 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Strict Deletion of Confidential Events (SD) *)
definition SD :: "'e BSP"
where
"SD 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) ⟶ β @ α ∈ Tr"

lemma "BSP_valid SD"
proof -
{
fix 𝒱::"('e V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr" by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "SD 𝒱 ?Tr'" unfolding SD_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ SD 𝒱 Tr'" by auto
}
thus ?thesis unfolding BSP_valid_def by auto
qed

(* Strict Insertion of Confidential Events (SI) *)
definition SI :: "'e BSP"
where
"SI 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = []) ⟶ β @ [c] @ α ∈ Tr"

lemma "BSP_valid SI"
proof -
{
fix 𝒱::"('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "SI 𝒱 ?Tr'"
using ‹isViewOn 𝒱 E›
unfolding isViewOn_def SI_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ SI 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

(* Strict Insertion of Admissible Confidential Events (SIA) *)
definition SIA :: "'e Rho ⇒ 'e BSP"
where
"SIA ρ 𝒱 Tr ≡
∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c))
⟶ (β @ [c] @ α) ∈ Tr"

lemma "BSP_valid (SIA ρ) "
proof -
{
fix 𝒱 :: "('a V_rec)"
fix Tr E
assume "isViewOn 𝒱 E"
and "areTracesOver Tr E"
let ?Tr'="{t. (set t) ⊆ E}"
have "?Tr'⊇ Tr"
by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
moreover
have "SIA ρ 𝒱 ?Tr'"
using ‹isViewOn 𝒱 E›
unfolding isViewOn_def SIA_def by auto
ultimately
have  "∃ Tr'. Tr' ⊇ Tr  ∧ SIA ρ 𝒱 Tr'"
by auto
}
thus ?thesis
unfolding BSP_valid_def by auto
qed

end


# Theory InformationFlowProperties

theory InformationFlowProperties
imports BasicSecurityPredicates
begin

(* Security Predicates are sets of basic security predicates *)
type_synonym 'e SP = "('e BSP) set"

(* structurally, information flow properties consist of a set of views
and a security predicate. *)
type_synonym 'e IFP_type = "('e V_rec set) × 'e SP"

(* side condition for information flow properties *)
definition IFP_valid :: "'e set ⇒ 'e IFP_type ⇒ bool"
where
"IFP_valid E ifp ≡
∀𝒱 ∈ (fst ifp). isViewOn 𝒱 E
∧ (∀BSP ∈ (snd ifp). BSP_valid BSP)"

(* An information flow property is an instance of IFP_type that
satisfies IFP_valid. *)
definition IFPIsSatisfied :: "'e IFP_type ⇒ ('e list) set  ⇒ bool"
where
"IFPIsSatisfied ifp Tr ≡
∀ 𝒱∈(fst ifp). ∀ BSP∈(snd ifp). BSP 𝒱 Tr"

end


# 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)

(* body of BSPTaxonomy *)
context BSPTaxonomyDifferentCorrections
begin

(*lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation*)
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⇘𝒱⇙"
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⇘𝒱⇙ = []"
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 taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
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⇘𝒱⇙ = []"
hence "(∃α' β'.
(β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
by auto
}
thus ?thesis
unfolding BSD_def D_def
by auto
qed

(* lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
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

(* show via induction over length (τ ↿ C⇘𝒱⇙) that SR holds *)
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⇘𝒱⇙)"
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⇘𝒱⇙)"
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⇘𝒱⇙"
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⇘𝒱⇙)"

with  VIsViewOnE have τ'_E_eq_VN: "τ' ↿ E⇘ES⇙ = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"

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 taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
lemma D_implies_R:
"D 𝒱 Tr⇘ES⇙ ⟹ R 𝒱 Tr⇘ES⇙"
proof -
assume D: "D 𝒱 Tr⇘ES⇙"
{
fix τ n

(* show via induction over length (τ ↿ C⇘𝒱⇙) that R holds *)
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⇘𝒱⇙"
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⇘𝒱⇙"
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⇘𝒱⇙"
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
qed

(* Theorem 3.5.6.1 from Heiko Mantel's dissertation *)
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⇘𝒱'⇙"
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

(* Theorem 3.5.6.2 from Heiko Mantel's dissertation *)
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⇘𝒱⇙ = []"

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⇙ = α"

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⇙ = α'"

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 taken from lemma 3.5.4 from Heiko Mantel's dissertation*)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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 taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
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

(* Theorem 3.5.15.1 from Heiko Mantel's dissertation *)
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⇘𝒱⇙ = [])"

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⇙ = α"

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⇙ = α'"

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 taken from Theorem 3.5.15.2 from Heiko Mantel's dissertation *)
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"

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"

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

(*Show that α'=α*)
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⇘𝒱⇙)"
with VIsViewOnE alpha_consists_of_events alpha'_consists_of_events
have "α'=α" unfolding isViewOn_def

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 taken from lemma 3.5.11 in Heiko Mantel's dissertation *)
"⟦ 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"
thus "Adm 𝒱⇩1 ρ⇩1 Tr α e"
using ‹ρ⇩1 𝒱⇩1 ⊆ ρ⇩2 𝒱⇩2› non_empty_projection_on_subset
by blast
qed

context BSPTaxonomyDifferentCorrections
begin

(* lemma taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
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 taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
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 taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
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

(* Mantel's PhD thesis, Theorem 3.5.7 Trivially fulfilled BSPs*)
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⇙"

lemma Trivially_fulfilled_BSD_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSD 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_D_C_empty:
"C⇘𝒱⇙ = {} ⟹ D 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_FCD_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘ES⇙"

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⇘𝒱⇙ = []"
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⇘𝒱⇙)"
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⇙"

(* Mantel's PhD thesis, Theorem 3.5.8 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_FCD_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
next
assume " Υ⇘Γ⇙={}" thus ?thesis
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⇘𝒱⇙"
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

(* Mantel's PhD thesis, Theorem 3.5.16 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_SI_C_empty:
"C⇘𝒱⇙ = {} ⟹ SI 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_BSI_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSI 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_I_C_empty:
"C⇘𝒱⇙ = {} ⟹ I 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_FCI_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_SIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ SIA ρ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_BSIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ BSIA ρ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_IA_C_empty:
"C⇘𝒱⇙ = {} ⟹ IA ρ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_FCIA_C_empty:
"C⇘𝒱⇙ = {} ⟹ FCIA Γ ρ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_FCI_V_empty:
"V⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"

lemma Trivially_fulfilled_FCIA_V_empty:
"V⇘𝒱⇙ = {} ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"

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 "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
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⇘𝒱⇙ = []"
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 "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
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⇘𝒱⇙)"
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

(* Mantel's PhD thesis, Theorem 3.5.17 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_FCI_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCI Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
next
assume " Υ⇘Γ⇙={}" thus ?thesis
qed
qed

lemma Trivially_fulfilled_FCIA_Nabla_Υ_empty:
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof -
assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
thus ?thesis
proof(rule disjE)
assume "∇⇘Γ⇙={}" thus ?thesis
next
assume " Υ⇘Γ⇙={}" thus ?thesis
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⇘𝒱⇙"
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⇘𝒱⇙"
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 taken from lemma 3.5.2 in Heiko Mantel's dissertation *)
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⇙ = []"
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⇙)"
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⇙"

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⇙ = []"
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⇙ = []"

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⇙›

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 taken from lemma 3.5.5 from Heiko Mantel's dissertation*)
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 ‹β @ δ' @ [