# 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" by (simp add: projection_def) next case False from Cons show "a ∉ Y ⟹ (a # b) ↿ (X ∪ Y) = (a # b) ↿ X" by (simp add: projection_def) 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 by (simp add: projection_def) 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 by (simp add: projection_def) qed moreover have "?B ⟹ ?A" proof - assume "?B" hence "(set (l ↿ X)) = set l" by (simp add: projection_def) thus ?thesis by (simp add: projection_def, auto) 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 by (simp add: projection_def) 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" by (simp add: projection_def) from τ_is_βxα have "length ?L = length (β ↿ X) + length ([x] ↿ X) + length (α ↿ X)" by (simp add: projection_def) 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 by (simp add: projection_def) qed with x_in_X τ_is_βxα α_no_x show ?thesis by auto qed lemma projection_rev_commute: "rev (l ↿ X) = (rev l) ↿ X" by (induct l, simp add: projection_def, simp add: projection_def) (* 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)" by (simp add: projection_rev_commute) 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" by (simp add: projection_concatenation_commute) 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" by (simp add: projection_def, auto) 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" by (simp add: Int_commute projection_def) moreover note setl_subset_L ultimately show ?thesis by (simp add: list_subset_iff_projection_neutral) 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" by (simp add: list_subset_iff_projection_neutral) hence "(l ↿ X) ↿ Y = l ↿ Y" by simp moreover have "(l ↿ X) ↿ Y = l ↿ (X ∩ Y)" by (simp add: projection_def) ultimately show ?thesis by simp qed lemma projection_commute: "(l ↿ X) ↿ Y = (l ↿ Y) ↿ X" by (simp add: projection_def conj_commute) 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" by (simp add: projection_def) 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" by (simp add: projection_def, auto) 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" by (simp add: projection_def, auto) 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" by (simp add: projection_def) 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" by (simp add: prefixclosed_def) thus "[] ∈ tr" by (simp add: empty_prefix_of_all) qed (* the prefix-predicate is transitive *) lemma transitive_prefix: "⟦ l1 ≼ l2 ; l2 ≼ l3 ⟧ ⟹ l1 ≼ l3" by (auto simp add: prefix_def) 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] 1000) where "E⇘_{ES}⇙ ≡ (E_ES ES)" abbreviation ESrecIES :: "'e ES_rec ⇒ 'e set" ("I⇘_⇙" [1000] 1000) where "I⇘_{ES}⇙ ≡ (I_ES ES)" abbreviation ESrecOES :: "'e ES_rec ⇒ 'e set" ("O⇘_⇙" [1000] 1000) where "O⇘_{ES}⇙ ≡ (O_ES ES)" abbreviation ESrecTrES :: "'e ES_rec ⇒ ('e list) set" ("Tr⇘_⇙" [1000] 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] 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}⇙" by (auto simp add: es_inputs_are_events_def) 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}⇙" by (auto simp add: es_inputs_are_events_def) 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}⇙" by (auto simp add: es_outputs_are_events_def) 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}⇙" by (auto simp add: es_outputs_are_events_def) 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∈{}" by (auto simp add: es_inputs_outputs_disjoint_def) } 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∈{}" by (auto simp add: es_inputs_outputs_disjoint_def) } 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}⇙))" by (simp add: prefix_def) 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}⇙))" by (simp add: prefix_def) 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] 1000) where "S⇘_{SES}⇙ ≡ (S_SES SES)" abbreviation SESrecs0SES :: "('s, 'e) SES_rec ⇒ 's" ("s0⇘_⇙" [1000] 1000) where "s0⇘_{SES}⇙ ≡ (s0_SES SES)" abbreviation SESrecESES :: "('s, 'e) SES_rec ⇒ 'e set" ("E⇘_⇙" [1000] 1000) where "E⇘_{SES}⇙ ≡ (E_SES SES)" abbreviation SESrecISES :: "('s, 'e) SES_rec ⇒ 'e set" ("I⇘_⇙" [1000] 1000) where "I⇘_{SES}⇙ ≡ (I_SES SES)" abbreviation SESrecOSES :: "('s, 'e) SES_rec ⇒ 'e set" ("O⇘_⇙" [1000] 1000) where "O⇘_{SES}⇙ ≡ (O_SES SES)" abbreviation SESrecTSES :: "('s, 'e) SES_rec ⇒ ('s ⇒ 'e ⇀ 's)" ("T⇘_⇙" [1000] 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" by (simp add: path_split_single) 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" by (simp add: path_trans_single) 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" by (simp add: enabledPrefixSingle) 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'" by (auto simp add: enabledPrefixSingleFinalStep) then obtain t t' where "t a⟶⇘_{SES}⇙ t'" by auto with e_eq_a SES_correct_transition_relation show "e ∈ E⇘_{SES}⇙" by (simp add: correct_transition_relation_def) qed qed qed qed next show "traces_prefixclosed (induceES SES)" unfolding traces_prefixclosed_def prefixclosed_def induceES_def possible_traces_def prefix_def by (clarsimp simp add: enabledPrefix) 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⇘_⇙" [100] 1000) where "V⇘_{v}⇙ ≡ (V v)" abbreviation VrecN :: "'e V_rec ⇒ 'e set" ("N⇘_⇙" [100] 1000) where "N⇘_{v}⇙ ≡ (N v)" abbreviation VrecC :: "'e V_rec ⇒ 'e set" ("C⇘_⇙" [100] 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 by (simp add: list_subset_iff_projection_neutral projection_commute) 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 (* ρ-Admissibility *) 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" ("∇⇘_⇙" [100] 1000) where "∇⇘_{Γ}⇙ ≡ (Nabla Γ)" abbreviation GammaDelta :: "'e Gamma ⇒ 'e set" ("Δ⇘_⇙" [100] 1000) where "Δ⇘_{Γ}⇙ ≡ (Delta Γ)" abbreviation GammaUpsilon :: "'e Gamma ⇒ 'e set" ("Υ⇘_⇙" [100] 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 𝒱⇩_{1}IsViewOnE: "isViewOn 𝒱⇩_{1}E⇘_{ES}⇙" and 𝒱⇩_{2}IsViewOnE: "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⇘_{𝒱}⇙" by (simp add: projection_subset_elim) moreover from VIsViewOnE have "VC_disjoint 𝒱 ∧ NC_disjoint 𝒱" unfolding isViewOn_def V_valid_def by auto then have "(V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) ∩ C⇘_{𝒱}⇙ = {}" by (simp add: NC_disjoint_def VC_disjoint_def inf_sup_distrib2) then have "?τ' ↿ C⇘_{𝒱}⇙ = []" by (simp add: disjoint_projection) ultimately show "?τ' ∈ Tr⇘_{ES}⇙ ∧ ?τ' ↿ V⇘_{𝒱}⇙ = τ ↿ V⇘_{𝒱}⇙ ∧ ?τ' ↿ C⇘_{𝒱}⇙ = []" using tau_V_N_is_trace by auto qed qed } thus ?thesis unfolding SR_def R_def by auto qed (* lemma 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⇘_{𝒱}⇙ = []" by (simp add: BSD_def, auto) hence "(∃α' β'. (β' @ α' ∈ Tr⇘_{ES}⇙ ∧ α' ↿ V⇘_{𝒱}⇙ = α ↿ V⇘_{𝒱}⇙ ∧ α' ↿ C⇘_{𝒱}⇙ = []) ∧ β' ↿ (V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β ↿ (V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙))" by auto } thus ?thesis unfolding BSD_def D_def by auto qed (* lemma 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⇘_{𝒱}⇙)" by (simp add: projection_def) moreover with VIsViewOnE c_in_C have "c ∉ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (simp add: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def, auto) hence "(β @ α) ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = (β @ [c] @ α) ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (simp add: projection_def) moreover note τ_is_βcα ultimately show ?thesis by auto qed moreover have "n = length ((β' @ α') ↿ C⇘_{𝒱}⇙)" proof - have "β' ↿ C⇘_{𝒱}⇙ = β ↿ C⇘_{𝒱}⇙" proof - have "V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙ = C⇘_{𝒱}⇙ ∪ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto with β'_VC_is_β_VC have "β' ↿ (C⇘_{𝒱}⇙ ∪ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)) = β ↿ (C⇘_{𝒱}⇙ ∪ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙))" by auto thus ?thesis by (rule projection_subset_eq_from_superset_eq) qed with α'_no_c α_no_c have "(β' @ α') ↿ C⇘_{𝒱}⇙ = (β @ α) ↿ C⇘_{𝒱}⇙" by (simp add: projection_def) with βα_contains_n_cs show ?thesis by auto qed with Suc.hyps β'α'_in_Tr obtain τ' where "τ' ∈ Tr⇘_{ES}⇙" and "τ' ↿ C⇘_{𝒱}⇙ = []" and "τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = (β' @ α') ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto ultimately show ?case by auto qed } hence "τ ∈ Tr⇘_{ES}⇙ ⟹ ∃τ'. τ'∈Tr⇘_{ES}⇙ ∧ τ' ↿ C⇘_{𝒱}⇙ = [] ∧ τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = τ ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto from this τ_trace obtain τ' where τ'_trace : "τ'∈Tr⇘_{ES}⇙" and τ'_no_C : "τ' ↿ C⇘_{𝒱}⇙ = []" and τ'_τ_rel : "τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = τ ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto from τ'_no_C have "τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (auto simp add: projection_on_union) with VIsViewOnE have τ'_E_eq_VN: "τ' ↿ E⇘_{ES}⇙ = τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (auto simp add: isViewOn_def) from validES τ'_trace have "(set τ') ⊆ E⇘_{ES}⇙" by (auto simp add: ES_valid_def traces_contain_events_def) hence "τ' ↿ E⇘_{ES}⇙ = τ'" by (simp add: list_subset_iff_projection_neutral) with τ'_E_eq_VN have "τ' = τ' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto with τ'_τ_rel have "τ' = τ ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by auto with τ'_trace show "τ ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) ∈ Tr⇘_{ES}⇙" by auto qed (* lemma 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⇘_{𝒱}⇙" by (simp add: projection_def) moreover with VIsViewOnE c_in_C have "c ∉ V⇘_{𝒱}⇙" by (simp add: isViewOn_def V_valid_def VC_disjoint_def, auto) hence "(β @ α) ↿ V⇘_{𝒱}⇙ = (β @ [c] @ α) ↿ V⇘_{𝒱}⇙" by (simp add: projection_def) moreover note τ_is_βcα ultimately show ?thesis by auto qed moreover have "n = length ((β' @ α') ↿ C⇘_{𝒱}⇙)" proof - have "β' ↿ C⇘_{𝒱}⇙ = β ↿ C⇘_{𝒱}⇙" proof - have "V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙ = C⇘_{𝒱}⇙ ∪ V⇘_{𝒱}⇙" by auto with β'_VC_is_β_VC have "β' ↿ (C⇘_{𝒱}⇙ ∪ V⇘_{𝒱}⇙) = β ↿ (C⇘_{𝒱}⇙ ∪ V⇘_{𝒱}⇙)" by auto thus ?thesis by (rule projection_subset_eq_from_superset_eq) qed with α'_no_c α_no_c have "(β' @ α') ↿ C⇘_{𝒱}⇙ = (β @ α) ↿ C⇘_{𝒱}⇙" by (simp add: projection_def) with βα_contains_n_cs show ?thesis by auto qed with Suc.hyps β'α'_in_Tr obtain τ' where "τ' ∈ Tr⇘_{ES}⇙" and "τ' ↿ C⇘_{𝒱}⇙ = []" and "τ' ↿ V⇘_{𝒱}⇙ = (β' @ α') ↿ V⇘_{𝒱}⇙" by auto ultimately show ?case by auto qed } thus ?thesis by (simp add: R_def) qed (* 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⇘_{𝒱'}⇙" by (simp add: projection_subset_elim) ultimately have "∃τ'∈Tr⇘_{ES}⇙. τ' ↿ C⇘_{𝒱'}⇙ = [] ∧ τ' ↿ V⇘_{𝒱'}⇙ = τ ↿ V⇘_{𝒱'}⇙" by auto } with ‹SR 𝒱 Tr⇘_{ES}⇙› show ?thesis unfolding R_def using ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› by auto qed lemma R_implies_SR_for_modified_view : "⟦R 𝒱' Tr⇘_{ES}⇙; 𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈⟧ ⟹ SR 𝒱 Tr⇘_{ES}⇙" proof - assume "R 𝒱' Tr⇘_{ES}⇙" and "𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈" { fix τ assume "τ ∈ Tr⇘_{ES}⇙" from ‹R 𝒱' Tr⇘_{ES}⇙› ‹τ ∈ Tr⇘_{ES}⇙› obtain τ' where "τ' ∈ Tr⇘_{ES}⇙" and "τ' ↿ C⇘_{𝒱'}⇙ = []" and "τ' ↿ V⇘_{𝒱'}⇙ = τ ↿ V⇘_{𝒱'}⇙" unfolding R_def by auto from VIsViewOnE ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› have "isViewOn 𝒱' E⇘_{ES}⇙" unfolding isViewOn_def V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def by auto from ‹τ' ↿ V⇘_{𝒱'}⇙ = τ ↿ V⇘_{𝒱'}⇙› ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› have "τ' ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙) = τ ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙)" by simp from ‹τ' ↿ C⇘_{𝒱'}⇙ = []› have "τ' =τ' ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙)" using validES ‹τ' ∈ Tr⇘_{ES}⇙› ‹isViewOn 𝒱' E⇘_{ES}⇙› unfolding projection_def ES_valid_def isViewOn_def traces_contain_events_def by (metis UnE filter_True filter_empty_conv) hence "τ' =τ ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙)" using ‹τ' ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙) = τ ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙)› by simp with ‹τ' ∈ Tr⇘_{ES}⇙› have "τ ↿ (V⇘_{𝒱'}⇙ ∪ N⇘_{𝒱'}⇙) ∈ Tr⇘_{ES}⇙" by auto } thus ?thesis unfolding SR_def using ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› by simp qed (* 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⇘_{𝒱}⇙ = []" by (auto simp add: BSD_def) from beta_c_alpha_is_trace validES have alpha_consists_of_events: "set α ⊆ E⇘_{ES}⇙" by (auto simp add: ES_valid_def traces_contain_events_def) from alpha_no_C_view have "α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (rule projection_on_union) with VIsViewOnE have alpha_on_ES : "α ↿ E⇘_{ES}⇙ = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" unfolding isViewOn_def by simp from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘_{ES}⇙ = α" by (simp add: list_subset_iff_projection_neutral) with alpha_on_ES have α_eq: "α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α" by auto from beta_alpha'_is_trace validES have alpha'_consists_of_events: "set α' ⊆ E⇘_{ES}⇙" by (auto simp add: ES_valid_def traces_contain_events_def) from alpha'_no_C_view have "α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (rule projection_on_union) with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘_{ES}⇙ = α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" unfolding isViewOn_def by (simp) from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘_{ES}⇙ = α'" by (simp add: list_subset_iff_projection_neutral) with alpha'_on_ES have α'_eq: "α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α'" by auto from alpha_alpha' α_eq α'_eq have "α = α'" by auto with beta_alpha'_is_trace show "β @ α ∈ Tr⇘_{ES}⇙" by auto qed (* lemma 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⇘_{𝒱}⇙ = [])" by (auto simp add: BSI_def) with beta_alpha_is_trace alpha_no_C_view have "∀c∈C⇘_{𝒱}⇙. (∃α'. β @ [c] @ α' ∈ Tr⇘_{ES}⇙ ∧ α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) ∧ α' ↿ C⇘_{𝒱}⇙ = [])" by auto with this BSI_view' c_C_view obtain α' where beta_c_alpha'_is_trace: "β @ [c] @ α' ∈ Tr⇘_{ES}⇙" and alpha_alpha': "α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" and alpha'_no_C_view : "α' ↿ C⇘_{𝒱}⇙ = []" by auto from beta_alpha_is_trace validES have alpha_consists_of_events: "set α ⊆ E⇘_{ES}⇙" by (auto simp add: ES_valid_def traces_contain_events_def) from alpha_no_C_view have "α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (rule projection_on_union) with VIsViewOnE have alpha_on_ES : "α ↿ E⇘_{ES}⇙ = α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" unfolding isViewOn_def by (simp) from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘_{ES}⇙ = α" by (simp add: list_subset_iff_projection_neutral) with alpha_on_ES have α_eq: "α ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α" by auto from beta_c_alpha'_is_trace validES have alpha'_consists_of_events: "set α' ⊆ E⇘_{ES}⇙" by (auto simp add: ES_valid_def traces_contain_events_def) from alpha'_no_C_view have "α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" by (rule projection_on_union) with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘_{ES}⇙ = α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" unfolding isViewOn_def by (simp) from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘_{ES}⇙ = α'" by (simp add: list_subset_iff_projection_neutral) with alpha'_on_ES have α'_eq: "α' ↿ (V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) = α'" by auto from alpha_alpha' α_eq α'_eq have "α = α'" by auto with beta_c_alpha'_is_trace show "β @ c # α ∈ Tr⇘_{ES}⇙" by auto qed (* lemma 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" by (simp add: Adm_def) from ‹c ∈ C⇘_{𝒱}⇙› ‹β @ α ∈ Tr⇘_{ES}⇙› ‹α↿C⇘_{𝒱}⇙ = []› ‹Adm 𝒱 ρ Tr⇘_{ES}⇙ β c› have "β @ [c] @ α ∈ Tr⇘_{ES}⇙" using ‹SIA ρ 𝒱 Tr⇘_{ES}⇙› unfolding SIA_def by auto hence "∃α'. β @ [c] @ α' ∈ Tr⇘_{ES}⇙ ∧ α' ↿ V⇘_{𝒱'}⇙ = α ↿ V⇘_{𝒱'}⇙ ∧ α' ↿ C⇘_{𝒱'}⇙ = [] " using ‹α ↿ C⇘_{𝒱'}⇙ = []› by blast } with ‹SIA ρ 𝒱 Tr⇘_{ES}⇙› show ?thesis unfolding BSIA_def using ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› by auto qed lemma BSIA_implies_SIA_for_modified_view : "⟦BSIA ρ' 𝒱' Tr⇘_{ES}⇙; 𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N = {} , C = C⇘_{𝒱}⇙ ⦈; ρ 𝒱 = ρ' 𝒱'⟧ ⟹ SIA ρ 𝒱 Tr⇘_{ES}⇙" proof - assume "BSIA ρ' 𝒱' Tr⇘_{ES}⇙" and "𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N = {} , C = C⇘_{𝒱}⇙ ⦈" and "ρ 𝒱 = ρ' 𝒱'" { fix α β c assume "c ∈ C⇘_{𝒱}⇙" and "β @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙ = []" and "Adm 𝒱 ρ Tr⇘_{ES}⇙ β c" from ‹c ∈ C⇘_{𝒱}⇙› ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› have "c ∈ C⇘_{𝒱'}⇙" by auto from ‹α↿C⇘_{𝒱}⇙ = []› ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› have "α↿C⇘_{𝒱'}⇙ = []" by auto from ‹Adm 𝒱 ρ Tr⇘_{ES}⇙ β c› ‹ρ 𝒱 = ρ' 𝒱'› have "Adm 𝒱' ρ' Tr⇘_{ES}⇙ β c" by (simp add: Adm_def) from ‹c ∈ C⇘_{𝒱'}⇙› ‹β @ α ∈ Tr⇘_{ES}⇙› ‹α↿C⇘_{𝒱'}⇙ = []› ‹Adm 𝒱' ρ' Tr⇘_{ES}⇙ β c› obtain α' where "β @ [c] @ α' ∈ Tr⇘_{ES}⇙" and " α' ↿ V⇘_{𝒱'}⇙ = α ↿ V⇘_{𝒱'}⇙" and " α' ↿ C⇘_{𝒱'}⇙ = []" using ‹BSIA ρ' 𝒱' Tr⇘_{ES}⇙› unfolding BSIA_def by blast (*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⇘_{𝒱}⇙)" by (simp add: projection_on_union) with VIsViewOnE alpha_consists_of_events alpha'_consists_of_events have "α'=α" unfolding isViewOn_def by (simp add: list_subset_iff_projection_neutral) hence "β @ [c] @ α ∈ Tr⇘_{ES}⇙ " using ‹β @ [c] @ α' ∈ Tr⇘_{ES}⇙› by blast } with ‹BSIA ρ' 𝒱' Tr⇘_{ES}⇙› show ?thesis unfolding SIA_def using ‹𝒱' = ⦇ V = V⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙ , N ={} , C = C⇘_{𝒱}⇙ ⦈› by auto qed end (* lemma taken from lemma 3.5.11 in Heiko Mantel's dissertation *) lemma Adm_implies_Adm_for_modified_rho: "⟦ Adm 𝒱⇩_{2}ρ⇩_{2}Tr α e;ρ⇩_{2}(𝒱⇩_{2}) ⊇ ρ⇩_{1}(𝒱⇩_{1})⟧ ⟹ Adm 𝒱⇩_{1}ρ⇩_{1}Tr α e " proof - assume "Adm 𝒱⇩_{2}ρ⇩_{2}Tr α e" and "ρ⇩_{2}(𝒱⇩_{2}) ⊇ ρ⇩_{1}(𝒱⇩_{1})" then obtain γ where "γ @ [e] ∈ Tr" and "γ ↿ ρ⇩_{2}𝒱⇩_{2}= α ↿ ρ⇩_{2}𝒱⇩_{2}" unfolding Adm_def by auto thus "Adm 𝒱⇩_{1}ρ⇩_{1}Tr α e" unfolding Adm_def using ‹ρ⇩_{1}𝒱⇩_{1}⊆ ρ⇩_{2}𝒱⇩_{2}› non_empty_projection_on_subset by blast qed context BSPTaxonomyDifferentCorrections begin (* lemma 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}⇙" by (simp add: SD_def) lemma Trivially_fulfilled_BSD_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ BSD 𝒱 Tr⇘_{ES}⇙" by (simp add: BSD_def) lemma Trivially_fulfilled_D_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ D 𝒱 Tr⇘_{ES}⇙" by (simp add: D_def) lemma Trivially_fulfilled_FCD_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCD_def) lemma Trivially_fullfilled_R_V_empty: "V⇘_{𝒱}⇙={} ⟹ R 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙={}" { fix τ assume "τ ∈ Tr⇘_{ES}⇙" let ?τ'="[]" from ‹τ ∈ Tr⇘_{ES}⇙›have "?τ' ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto with ‹V⇘_{𝒱}⇙={}› have "∃τ' ∈ Tr⇘_{ES}⇙. τ'↿C⇘_{𝒱}⇙=[] ∧ τ'↿V⇘_{𝒱}⇙=τ↿V⇘_{𝒱}⇙" by (metis projection_on_empty_trace projection_to_emptyset_is_empty_trace) } thus ?thesis unfolding R_def by auto qed lemma Trivially_fulfilled_BSD_V_empty: "V⇘_{𝒱}⇙ = {} ⟹ BSD 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙={}" { fix α β c assume "β @ [c] @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙= []" from ‹β @ [c] @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto let ?α'="[]" from ‹β ∈ Tr⇘_{ES}⇙› ‹V⇘_{𝒱}⇙={}› have "β@ ?α'∈Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙ = []" by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace) hence "∃α'. β @ α'∈Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙ = []" by blast } thus ?thesis unfolding BSD_def by auto qed lemma Trivially_fulfilled_D_V_empty: "V⇘_{𝒱}⇙ = {} ⟹ D 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙={}" { fix α β c assume "β @ [c] @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙= []" from ‹β @ [c] @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto let ?β'=β and ?α'="[]" from ‹β ∈ Tr⇘_{ES}⇙› ‹V⇘_{𝒱}⇙={}› have "?β'@ ?α'∈Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙ = [] ∧ ?β'↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙)" by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace) hence "∃α' β'. β'@ α'∈Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙ = [] ∧ β'↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙)" by blast } thus ?thesis unfolding D_def by auto qed lemma Trivially_fulfilled_FCD_V_empty: "V⇘_{𝒱}⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCD_def) (* 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 by (simp add: FCD_def) next assume " Υ⇘_{Γ}⇙={}" thus ?thesis by (simp add: FCD_def) qed qed lemma Trivially_fulfilled_FCD_N_subseteq_Δ_and_BSD: "⟦N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙; BSD 𝒱 Tr⇘_{ES}⇙⟧ ⟹ FCD Γ 𝒱 Tr⇘_{ES}⇙" proof - assume "N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙" and "BSD 𝒱 Tr⇘_{ES}⇙" { fix α β c v assume "c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙" and "v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙" and "β @ [c,v] @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙ = []" from ‹c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙› have "c ∈ C⇘_{𝒱}⇙" by auto from ‹v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙› have "v ∈ V⇘_{𝒱}⇙" by auto let ?α="[v] @ α" from ‹v ∈ V⇘_{𝒱}⇙› ‹α↿C⇘_{𝒱}⇙ = []› have "?α↿C⇘_{𝒱}⇙=[]" using VIsViewOnE unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto from ‹β @ [c,v] @ α ∈ Tr⇘_{ES}⇙› have "β @ [c] @ ?α ∈ Tr⇘_{ES}⇙" by auto from ‹BSD 𝒱 Tr⇘_{ES}⇙› obtain α' where "β @ α' ∈ Tr⇘_{ES}⇙" and "α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙" and "α'↿C⇘_{𝒱}⇙ = []" using ‹c ∈ C⇘_{𝒱}⇙› ‹β @ [c] @ ?α ∈ Tr⇘_{ES}⇙› ‹?α↿C⇘_{𝒱}⇙ = []› unfolding BSD_def by auto from‹v ∈ V⇘_{𝒱}⇙› ‹α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙› have "α'↿V⇘_{𝒱}⇙ = [v] @ α↿V⇘_{𝒱}⇙" by (simp add: projection_def) then obtain δ α'' where "α'=δ @ [v] @ α''" and "δ↿V⇘_{𝒱}⇙ = []" and "α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙" using projection_split_first_with_suffix by fastforce from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹β @ α' ∈ Tr⇘_{ES}⇙› have "set α' ⊆ E⇘_{ES}⇙" using validES unfolding ES_valid_def traces_contain_events_def by auto with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘_{ES}⇙" by auto with ‹δ↿C⇘_{𝒱}⇙=[]› ‹δ↿V⇘_{𝒱}⇙ = []› ‹N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙› have "(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)" using VIsViewOnE projection_empty_implies_absence_of_events unfolding isViewOn_def projection_def by blast let ?β=β and ?δ'=δ and ?α'=α'' from ‹(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)› ‹β @ α' ∈ Tr⇘_{ES}⇙› ‹α'=δ @ [v] @ α''› ‹α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙› ‹α''↿C⇘_{𝒱}⇙=[]› have "(set ?δ')⊆(N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ ?β @ ?δ' @ [v] @ ?α' ∈ Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙=α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙=[]" by auto hence "∃α''' δ''. (set δ'') ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ (β @ δ'' @ [v] @ α''') ∈ Tr⇘_{ES}⇙ ∧ α''' ↿ V⇘_{𝒱}⇙ = α ↿ V⇘_{𝒱}⇙ ∧ α''' ↿ C⇘_{𝒱}⇙ = []" by auto } thus ?thesis unfolding FCD_def by auto qed (* Mantel's PhD thesis, Theorem 3.5.16 Trivially fulfilled BSPs*) lemma Trivially_fulfilled_SI_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ SI 𝒱 Tr⇘_{ES}⇙" by (simp add: SI_def) lemma Trivially_fulfilled_BSI_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ BSI 𝒱 Tr⇘_{ES}⇙" by (simp add: BSI_def) lemma Trivially_fulfilled_I_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ I 𝒱 Tr⇘_{ES}⇙" by (simp add: I_def) lemma Trivially_fulfilled_FCI_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCI_def) lemma Trivially_fulfilled_SIA_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ SIA ρ 𝒱 Tr⇘_{ES}⇙" by (simp add: SIA_def) lemma Trivially_fulfilled_BSIA_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ BSIA ρ 𝒱 Tr⇘_{ES}⇙" by (simp add: BSIA_def) lemma Trivially_fulfilled_IA_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ IA ρ 𝒱 Tr⇘_{ES}⇙" by (simp add: IA_def) lemma Trivially_fulfilled_FCIA_C_empty: "C⇘_{𝒱}⇙ = {} ⟹ FCIA Γ ρ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCIA_def) lemma Trivially_fulfilled_FCI_V_empty: "V⇘_{𝒱}⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCI_def) lemma Trivially_fulfilled_FCIA_V_empty: "V⇘_{𝒱}⇙ = {} ⟹ FCIA ρ Γ 𝒱 Tr⇘_{ES}⇙" by (simp add: FCIA_def) lemma Trivially_fulfilled_BSIA_V_empty_rho_subseteq_C_N: "⟦V⇘_{𝒱}⇙ = {}; ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) ⟧ ⟹ BSIA ρ 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙={}" and "ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" { fix α β c assume "c ∈ C⇘_{𝒱}⇙" and "β @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙=[]" and "Adm 𝒱 ρ Tr⇘_{ES}⇙ β c" from ‹Adm 𝒱 ρ Tr⇘_{ES}⇙ β c› obtain γ where "γ @ [c] ∈ Tr⇘_{ES}⇙" and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)" unfolding Adm_def by auto from this(1) have "γ ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto moreover from ‹β @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto ultimately have "β↿E⇘_{ES}⇙=γ↿E⇘_{ES}⇙" using validES VIsViewOnE ‹V⇘_{𝒱}⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)› non_empty_projection_on_subset unfolding ES_valid_def isViewOn_def traces_contain_events_def by (metis empty_subsetI sup_absorb2 sup_commute) hence "β @ [c] ∈ Tr⇘_{ES}⇙" using validES ‹γ @ [c] ∈ Tr⇘_{ES}⇙› ‹β ∈ Tr⇘_{ES}⇙› ‹γ ∈ Tr⇘_{ES}⇙› unfolding ES_valid_def traces_contain_events_def by (metis list_subset_iff_projection_neutral subsetI) let ?α'="[]" from ‹β @ [c] ∈ Tr⇘_{ES}⇙› ‹V⇘_{𝒱}⇙ = {}› have "β @ [c] @ ?α' ∈Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙ = []" by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace) hence "∃ α'. β @ [c] @ α' ∈Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙ = []" by auto } thus ?thesis unfolding BSIA_def by auto qed lemma Trivially_fulfilled_IA_V_empty_rho_subseteq_C_N: "⟦V⇘_{𝒱}⇙ = {}; ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙) ⟧ ⟹ IA ρ 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙={}" and "ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)" { fix α β c assume "c ∈ C⇘_{𝒱}⇙" and "β @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙=[]" and "Adm 𝒱 ρ Tr⇘_{ES}⇙ β c" from ‹Adm 𝒱 ρ Tr⇘_{ES}⇙ β c› obtain γ where "γ @ [c] ∈ Tr⇘_{ES}⇙" and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)" unfolding Adm_def by auto from this(1) have "γ ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto moreover from ‹β @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto ultimately have "β↿E⇘_{ES}⇙=γ↿E⇘_{ES}⇙" using validES VIsViewOnE ‹V⇘_{𝒱}⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘_{𝒱}⇙ ∪ N⇘_{𝒱}⇙)› non_empty_projection_on_subset unfolding ES_valid_def isViewOn_def traces_contain_events_def by (metis empty_subsetI sup_absorb2 sup_commute) hence "β @ [c] ∈ Tr⇘_{ES}⇙" using validES ‹γ @ [c] ∈ Tr⇘_{ES}⇙› ‹β ∈ Tr⇘_{ES}⇙› ‹γ ∈ Tr⇘_{ES}⇙› unfolding ES_valid_def traces_contain_events_def by (metis list_subset_iff_projection_neutral subsetI) let ?β'=β and ?α'="[]" from ‹β @ [c] ∈ Tr⇘_{ES}⇙› ‹V⇘_{𝒱}⇙ = {}› have "?β' @ [c] @ ?α' ∈Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙ = [] ∧ ?β'↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙)" by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace) hence "∃ α' β'. β' @ [c] @ α' ∈Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙ = [] ∧ β'↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙)" by auto } thus ?thesis unfolding IA_def by auto qed lemma Trivially_fulfilled_BSI_V_empty_total_ES_C: "⟦V⇘_{𝒱}⇙ = {}; total ES C⇘_{𝒱}⇙ ⟧ ⟹ BSI 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙ = {}" and "total ES C⇘_{𝒱}⇙" { fix α β c assume "β @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙=[]" and "c ∈ C⇘_{𝒱}⇙" from ‹β @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto with ‹total ES C⇘_{𝒱}⇙› have "β @ [c] ∈ Tr⇘_{ES}⇙" using ‹c ∈ C⇘_{𝒱}⇙› unfolding total_def by auto moreover from ‹V⇘_{𝒱}⇙ = {}› have "α↿V⇘_{𝒱}⇙=[]" unfolding projection_def by auto ultimately have "∃α'. β @ [c] @ α' ∈ Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙=α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙=[]" using ‹α ↿ C⇘_{𝒱}⇙ = []› by (metis append_Nil2 projection_idempotent) } thus ?thesis unfolding BSI_def by auto qed lemma Trivially_fulfilled_I_V_empty_total_ES_C: "⟦V⇘_{𝒱}⇙ = {}; total ES C⇘_{𝒱}⇙ ⟧ ⟹ I 𝒱 Tr⇘_{ES}⇙" proof - assume "V⇘_{𝒱}⇙ = {}" and "total ES C⇘_{𝒱}⇙" { fix α β c assume "c ∈ C⇘_{𝒱}⇙" and "β @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙=[]" from ‹β @ α ∈ Tr⇘_{ES}⇙› have "β ∈ Tr⇘_{ES}⇙" using validES unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto with ‹total ES C⇘_{𝒱}⇙› have "β @ [c] ∈ Tr⇘_{ES}⇙" using ‹c ∈ C⇘_{𝒱}⇙› unfolding total_def by auto moreover from ‹V⇘_{𝒱}⇙ = {}› have "α↿V⇘_{𝒱}⇙=[]" unfolding projection_def by auto ultimately have "∃β' α'. β' @ [c] @ α' ∈ Tr⇘_{ES}⇙ ∧ α'↿V⇘_{𝒱}⇙=α↿V⇘_{𝒱}⇙ ∧ α'↿C⇘_{𝒱}⇙=[] ∧ β'↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙) = β↿(V⇘_{𝒱}⇙ ∪ C⇘_{𝒱}⇙)" using ‹α ↿ C⇘_{𝒱}⇙ = []› by (metis append_Nil2 projection_idempotent) } thus ?thesis unfolding I_def by blast qed (* 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 by (simp add: FCI_def) next assume " Υ⇘_{Γ}⇙={}" thus ?thesis by (simp add: FCI_def) qed qed lemma Trivially_fulfilled_FCIA_Nabla_Υ_empty: "⟦∇⇘_{Γ}⇙={} ∨ Υ⇘_{Γ}⇙={}⟧⟹ FCIA ρ Γ 𝒱 Tr⇘_{ES}⇙" proof - assume "∇⇘_{Γ}⇙={} ∨ Υ⇘_{Γ}⇙={}" thus ?thesis proof(rule disjE) assume "∇⇘_{Γ}⇙={}" thus ?thesis by (simp add: FCIA_def) next assume " Υ⇘_{Γ}⇙={}" thus ?thesis by (simp add: FCIA_def) qed qed lemma Trivially_fulfilled_FCI_N_subseteq_Δ_and_BSI: "⟦N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙; BSI 𝒱 Tr⇘_{ES}⇙⟧ ⟹ FCI Γ 𝒱 Tr⇘_{ES}⇙" proof - assume "N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙" and "BSI 𝒱 Tr⇘_{ES}⇙" { fix α β c v assume "c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙" and "v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙" and "β @ [v] @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙ = []" from ‹c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙› have "c ∈ C⇘_{𝒱}⇙" by auto from ‹v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙› have "v ∈ V⇘_{𝒱}⇙" by auto let ?α="[v] @ α" from ‹v ∈ V⇘_{𝒱}⇙› ‹α↿C⇘_{𝒱}⇙ = []› have "?α↿C⇘_{𝒱}⇙=[]" using VIsViewOnE unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto from ‹β @ [v] @ α ∈ Tr⇘_{ES}⇙› have "β @ ?α ∈ Tr⇘_{ES}⇙" by auto from ‹BSI 𝒱 Tr⇘_{ES}⇙› obtain α' where "β @ [c] @ α' ∈ Tr⇘_{ES}⇙" and "α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙" and "α'↿C⇘_{𝒱}⇙ = []" using ‹c ∈ C⇘_{𝒱}⇙› ‹β @ ?α ∈ Tr⇘_{ES}⇙› ‹?α↿C⇘_{𝒱}⇙ = []› unfolding BSI_def by blast from‹v ∈ V⇘_{𝒱}⇙› ‹α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙› have "α'↿V⇘_{𝒱}⇙ = [v] @ α↿V⇘_{𝒱}⇙" by (simp add: projection_def) then obtain δ α'' where "α'=δ @ [v] @ α''" and "δ↿V⇘_{𝒱}⇙ = []" and "α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙" using projection_split_first_with_suffix by fastforce from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹β @ [c] @ α' ∈ Tr⇘_{ES}⇙› have "set α' ⊆ E⇘_{ES}⇙" using validES unfolding ES_valid_def traces_contain_events_def by auto with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘_{ES}⇙" by auto with ‹δ↿C⇘_{𝒱}⇙=[]› ‹δ↿V⇘_{𝒱}⇙ = []› ‹N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙› have "(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)" using VIsViewOnE projection_empty_implies_absence_of_events unfolding isViewOn_def projection_def by blast let ?β=β and ?δ'=δ and ?α'=α'' from ‹(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)› ‹β @ [c] @ α' ∈ Tr⇘_{ES}⇙› ‹α'=δ @ [v] @ α''› ‹α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙› ‹α''↿C⇘_{𝒱}⇙=[]› have "(set ?δ')⊆(N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙=α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙=[]" by auto hence "∃α''' δ''. (set δ'') ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘_{ES}⇙ ∧ α''' ↿ V⇘_{𝒱}⇙ = α ↿ V⇘_{𝒱}⇙ ∧ α''' ↿ C⇘_{𝒱}⇙ = []" by auto } thus ?thesis unfolding FCI_def by auto qed lemma Trivially_fulfilled_FCIA_N_subseteq_Δ_and_BSIA: "⟦N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙; BSIA ρ 𝒱 Tr⇘_{ES}⇙⟧ ⟹ FCIA ρ Γ 𝒱 Tr⇘_{ES}⇙" proof - assume "N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙" and "BSIA ρ 𝒱 Tr⇘_{ES}⇙" { fix α β c v assume "c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙" and "v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙" and "β @ [v] @ α ∈ Tr⇘_{ES}⇙" and "α↿C⇘_{𝒱}⇙ = []" and "Adm 𝒱 ρ Tr⇘_{ES}⇙ β c" from ‹c ∈ C⇘_{𝒱}⇙ ∩ Υ⇘_{Γ}⇙› have "c ∈ C⇘_{𝒱}⇙" by auto from ‹v ∈ V⇘_{𝒱}⇙ ∩ ∇⇘_{Γ}⇙› have "v ∈ V⇘_{𝒱}⇙" by auto let ?α="[v] @ α" from ‹v ∈ V⇘_{𝒱}⇙› ‹α↿C⇘_{𝒱}⇙ = []› have "?α↿C⇘_{𝒱}⇙=[]" using VIsViewOnE unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto from ‹β @ [v] @ α ∈ Tr⇘_{ES}⇙› have "β @ ?α ∈ Tr⇘_{ES}⇙" by auto from ‹BSIA ρ 𝒱 Tr⇘_{ES}⇙› obtain α' where "β @ [c] @ α' ∈ Tr⇘_{ES}⇙" and "α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙" and "α'↿C⇘_{𝒱}⇙ = []" using ‹c ∈ C⇘_{𝒱}⇙› ‹β @ ?α ∈ Tr⇘_{ES}⇙› ‹?α↿C⇘_{𝒱}⇙ = []› ‹Adm 𝒱 ρ Tr⇘_{ES}⇙ β c› unfolding BSIA_def by blast from‹v ∈ V⇘_{𝒱}⇙› ‹α'↿V⇘_{𝒱}⇙ = ([v] @ α)↿V⇘_{𝒱}⇙› have "α'↿V⇘_{𝒱}⇙ = [v] @ α↿V⇘_{𝒱}⇙" by (simp add: projection_def) then obtain δ α'' where "α'=δ @ [v] @ α''" and "δ↿V⇘_{𝒱}⇙ = []" and "α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙" using projection_split_first_with_suffix by fastforce from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹α'↿C⇘_{𝒱}⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘_{𝒱}⇙=[]" by (metis append_is_Nil_conv projection_concatenation_commute) from ‹β @ [c] @ α' ∈ Tr⇘_{ES}⇙› have "set α' ⊆ E⇘_{ES}⇙" using validES unfolding ES_valid_def traces_contain_events_def by auto with ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘_{ES}⇙" by auto with ‹δ↿C⇘_{𝒱}⇙=[]› ‹δ↿V⇘_{𝒱}⇙ = []› ‹N⇘_{𝒱}⇙ ⊆ Δ⇘_{Γ}⇙› have "(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)" using VIsViewOnE projection_empty_implies_absence_of_events unfolding isViewOn_def projection_def by blast let ?β=β and ?δ'=δ and ?α'=α'' from ‹(set δ) ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙)› ‹β @ [c] @ α' ∈ Tr⇘_{ES}⇙› ‹α'=δ @ [v] @ α''› ‹α''↿V⇘_{𝒱}⇙ = α↿V⇘_{𝒱}⇙› ‹α''↿C⇘_{𝒱}⇙=[]› have "(set ?δ')⊆(N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘_{ES}⇙ ∧ ?α'↿V⇘_{𝒱}⇙=α↿V⇘_{𝒱}⇙ ∧ ?α'↿C⇘_{𝒱}⇙=[]" by auto hence "∃α''' δ''. (set δ'') ⊆ (N⇘_{𝒱}⇙ ∩ Δ⇘_{Γ}⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘_{ES}⇙ ∧ α''' ↿ V⇘_{𝒱}⇙ = α ↿ V⇘_{𝒱}⇙ ∧ α''' ↿ C⇘_{𝒱}⇙ = []" by auto } thus ?thesis unfolding FCIA_def by auto qed end context BSPTaxonomyDifferentViewsFirstDim begin (* lemma 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}⇙ = []" by (simp add: projection_concatenation_commute) from "Suc.prems"(1) ‹α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}› obtain β' where "β'=β @ [c] @ γ⇩_{1}" and "β' @ [c⇩_{1}] @ γ⇩_{2}∈ Tr⇘_{ES}⇙" by auto from ‹β' @ [c⇩_{1}] @ γ⇩_{2}∈ Tr⇘_{ES}⇙› ‹γ⇩_{2}↿C⇘_{𝒱⇩1}⇙ = []› ‹c⇩_{1}∈ C⇘_{𝒱⇩1}⇙› obtain γ⇩_{2}' where " β' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙" and "γ⇩_{2}' ↿ V⇘_{𝒱⇩1}⇙ = γ⇩_{2}↿ V⇘_{𝒱⇩1}⇙" and "γ⇩_{2}' ↿C⇘_{𝒱⇩1}⇙ =[]" using BSD_𝒱⇩_{1}unfolding BSD_def by auto from ‹β'=β @ [c] @ γ⇩_{1}› ‹β' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙› have "β @ [c] @ γ⇩_{1}@ γ⇩_{2}' ∈ Tr⇘_{ES}⇙" by auto moreover from ‹γ⇩_{1}↿ C⇘_{𝒱⇩2}⇙=[]› ‹γ⇩_{2}' ↿C⇘_{𝒱⇩1}⇙ =[]› C2_subset_C1 have "(γ⇩_{1}@ γ⇩_{2}') ↿ C⇘_{𝒱⇩2}⇙ =[]" by (metis append_Nil projection_concatenation_commute projection_on_subset) moreover from ‹n = length((γ⇩_{1}@ γ⇩_{2})↿ C⇘_{𝒱⇩1}⇙)› ‹γ⇩_{2}↿C⇘_{𝒱⇩1}⇙ = []› ‹γ⇩_{2}' ↿C⇘_{𝒱⇩1}⇙ =[]› have "n = length((γ⇩_{1}@ γ⇩_{2}')↿ C⇘_{𝒱⇩1}⇙)" by (simp add: projection_concatenation_commute) ultimately have witness: "∃ α'. β @ α' ∈ Tr⇘_{ES}⇙ ∧ α'↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}') ↿V⇘_{𝒱⇩2}⇙ ∧ α' ↿C⇘_{𝒱⇩2}⇙ = []" using Suc.hyps by auto from 𝒱⇩_{1}IsViewOnE 𝒱⇩_{2}IsViewOnE V2_subset_V1 C2_subset_C1 c⇩_{1}_in_C⇩_{1}have "c⇩_{1}∉ V⇘_{𝒱⇩2}⇙" unfolding isViewOn_def V_valid_def VC_disjoint_def by auto with ‹α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}› have "α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}) ↿ V⇘_{𝒱⇩2}⇙" unfolding projection_def by auto hence "α ↿ V⇘_{𝒱⇩2}⇙ = γ⇩_{1}↿ V⇘_{𝒱⇩2}⇙ @ γ⇩_{2}↿ V⇘_{𝒱⇩2}⇙ " using projection_concatenation_commute by auto with V2_subset_V1 ‹γ⇩_{2}' ↿ V⇘_{𝒱⇩1}⇙ = γ⇩_{2}↿ V⇘_{𝒱⇩1}⇙› have "γ⇩_{1}↿ V⇘_{𝒱⇩2}⇙ @ γ⇩_{2}↿ V⇘_{𝒱⇩2}⇙ = γ⇩_{1}↿ V⇘_{𝒱⇩2}⇙ @ γ⇩_{2}' ↿ V⇘_{𝒱⇩2}⇙" using non_empty_projection_on_subset by metis with ‹α ↿ V⇘_{𝒱⇩2}⇙ = γ⇩_{1}↿ V⇘_{𝒱⇩2}⇙ @ γ⇩_{2}↿ V⇘_{𝒱⇩2}⇙› have "α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}') ↿ V⇘_{𝒱⇩2}⇙" by (simp add: projection_concatenation_commute) from witness ‹α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}') ↿ V⇘_{𝒱⇩2}⇙› show ?case by auto qed } thus ?thesis unfolding BSD_def by auto qed lemma D_implies_D_for_modified_view: "D 𝒱⇩_{1}Tr⇘_{ES}⇙ ⟹ D 𝒱⇩_{2}Tr⇘_{ES}⇙" proof- assume D_𝒱⇩_{1}: "D 𝒱⇩_{1}Tr⇘_{ES}⇙" from V2_subset_V1 C2_subset_C1 have V⇩_{2}_union_C⇩_{2}_subset_V⇩_{1}_union_C⇩_{1}: "V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙ ⊆ V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙" by auto { fix α β c n assume c_in_C⇩_{2}: "c ∈ C⇘_{𝒱⇩2}⇙" from C2_subset_C1 c_in_C⇩_{2}have c_in_C⇩_{1}: "c ∈ C⇘_{𝒱⇩1}⇙" by auto have "⟦β @ [c] @ α ∈ Tr⇘_{ES}⇙; α ↿ C⇘_{𝒱⇩2}⇙=[]; n= length(α ↿ C⇘_{𝒱⇩1}⇙)⟧ ⟹ ∃ α' β'. β' @ α' ∈ Tr⇘_{ES}⇙ ∧ α'↿ V⇘_{𝒱⇩2}⇙ = α ↿V⇘_{𝒱⇩2}⇙ ∧ α' ↿C⇘_{𝒱⇩2}⇙ = [] ∧ β' ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) = β ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) " proof(induct n arbitrary: α β ) case 0 from "0.prems"(3) have "α ↿ C⇘_{𝒱⇩1}⇙ = []" by auto with c_in_C⇩_{1}"0.prems"(1) have "∃ α' β'. β' @ α' ∈ Tr⇘_{ES}⇙ ∧ α' ↿ V⇘_{𝒱⇩1}⇙ = α ↿ V⇘_{𝒱⇩1}⇙ ∧ α' ↿C⇘_{𝒱⇩1}⇙ =[] ∧ β' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" using D_𝒱⇩_{1}unfolding D_def by fastforce then obtain β' α' where "β' @ α' ∈ Tr⇘_{ES}⇙" and "α' ↿ V⇘_{𝒱⇩1}⇙ = α ↿ V⇘_{𝒱⇩1}⇙" and "α' ↿C⇘_{𝒱⇩1}⇙ =[]" and "β' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" by auto from V2_subset_V1 ‹α' ↿ V⇘_{𝒱⇩1}⇙ = α ↿ V⇘_{𝒱⇩1}⇙› have "α'↿ V⇘_{𝒱⇩2}⇙ = α ↿V⇘_{𝒱⇩2}⇙" using non_empty_projection_on_subset by blast moreover from ‹α' ↿C⇘_{𝒱⇩1}⇙ =[]› C2_subset_C1 have "α' ↿ C⇘_{𝒱⇩2}⇙ = []" using projection_on_subset by auto moreover from ‹β' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› V⇩_{2}_union_C⇩_{2}_subset_V⇩_{1}_union_C⇩_{1}have "β' ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) = β ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙)" using non_empty_projection_on_subset by blast ultimately show ?case using ‹β' @ α' ∈ Tr⇘_{ES}⇙› by auto next case (Suc n) from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)] obtain γ⇩_{1}γ⇩_{2}c⇩_{1}where c⇩_{1}_in_C⇩_{1}: "c⇩_{1}∈ C⇘_{𝒱⇩1}⇙" and "α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}" and "γ⇩_{2}↿C⇘_{𝒱⇩1}⇙ = []" and "n = length((γ⇩_{1}@ γ⇩_{2})↿ C⇘_{𝒱⇩1}⇙)" by auto from "Suc.prems"(2) ‹α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}› have "γ⇩_{1}↿ C⇘_{𝒱⇩2}⇙ = []" by (simp add: projection_concatenation_commute) from "Suc.prems"(1) ‹α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}› obtain β' where "β'=β @ [c] @ γ⇩_{1}" and "β' @ [c⇩_{1}] @ γ⇩_{2}∈ Tr⇘_{ES}⇙" by auto from ‹β' @ [c⇩_{1}] @ γ⇩_{2}∈ Tr⇘_{ES}⇙› ‹γ⇩_{2}↿C⇘_{𝒱⇩1}⇙ = []› ‹c⇩_{1}∈ C⇘_{𝒱⇩1}⇙› obtain γ⇩_{2}' β'' where " β'' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙" and "γ⇩_{2}' ↿ V⇘_{𝒱⇩1}⇙ = γ⇩_{2}↿ V⇘_{𝒱⇩1}⇙" and "γ⇩_{2}' ↿C⇘_{𝒱⇩1}⇙ =[]" and "β'' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" using D_𝒱⇩_{1}unfolding D_def by force from c_in_C⇩_{1}have "c ∈ V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙" by auto moreover from ‹β'' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› ‹β'=β @ [c] @ γ⇩_{1}› have "β'' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = (β @ [c] @ γ⇩_{1}) ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" by auto ultimately have "∃ β''' γ⇩_{1}'. β''=β'''@ [c] @ γ⇩_{1}' ∧ β''' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) ∧ γ⇩_{1}'↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = γ⇩_{1}↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" using projection_split_arbitrary_element by fast then obtain β''' γ⇩_{1}' where "β''= β''' @ [c] @ γ⇩_{1}'" and "β''' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" and "γ⇩_{1}'↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = γ⇩_{1}↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)" using projection_split_arbitrary_element by auto from ‹β'' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙› this(1) have "β''' @ [c] @ γ⇩_{1}' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙" by simp from ‹γ⇩_{2}' ↿C⇘_{𝒱⇩1}⇙ =[]› have "γ⇩_{2}' ↿ C⇘_{𝒱⇩2}⇙=[]" using C2_subset_C1 projection_on_subset by auto moreover from ‹γ⇩_{1}↿ C⇘_{𝒱⇩2}⇙ = []› ‹γ⇩_{1}'↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = γ⇩_{1}↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› have "γ⇩_{1}'↿ C⇘_{𝒱⇩2}⇙ = []" using C2_subset_C1 V2_subset_V1 by (metis non_empty_projection_on_subset projection_subset_eq_from_superset_eq sup_commute) ultimately have "(γ⇩_{1}' @ γ⇩_{2}')↿C⇘_{𝒱⇩2}⇙ = []" by (simp add: projection_concatenation_commute) from ‹γ⇩_{1}'↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = γ⇩_{1}↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› have "γ⇩_{1}'↿C⇘_{𝒱⇩1}⇙ = γ⇩_{1}↿C⇘_{𝒱⇩1}⇙" using projection_subset_eq_from_superset_eq sup_commute by metis hence "length(γ⇩_{1}'↿C⇘_{𝒱⇩1}⇙) = length(γ⇩_{1}↿C⇘_{𝒱⇩1}⇙)" by simp moreover from ‹γ⇩_{2}↿C⇘_{𝒱⇩1}⇙ = []› ‹γ⇩_{2}'↿C⇘_{𝒱⇩1}⇙=[]› have "length(γ⇩_{2}'↿C⇘_{𝒱⇩1}⇙) = length(γ⇩_{2}↿C⇘_{𝒱⇩1}⇙)" by simp ultimately have "n=length((γ⇩_{1}' @ γ⇩_{2}')↿C⇘_{𝒱⇩1}⇙)" by (simp add: ‹n = length ((γ⇩_{1}@ γ⇩_{2}) ↿ C⇘_{𝒱⇩1}⇙)› projection_concatenation_commute) from ‹β''' @ [c] @ γ⇩_{1}' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙› ‹(γ⇩_{1}' @ γ⇩_{2}')↿C⇘_{𝒱⇩2}⇙ = []› ‹n=length((γ⇩_{1}' @ γ⇩_{2}')↿C⇘_{𝒱⇩1}⇙)› have witness: " ∃α' β'. β' @ α' ∈ Tr⇘_{ES}⇙ ∧ α' ↿ V⇘_{𝒱⇩2}⇙ = ( γ⇩_{1}' @ γ⇩_{2}') ↿ V⇘_{𝒱⇩2}⇙ ∧ α' ↿ C⇘_{𝒱⇩2}⇙ = [] ∧ β' ↿ (V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) = β''' ↿ (V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙)" using Suc.hyps[OF ‹β''' @ [c] @ γ⇩_{1}' @ γ⇩_{2}' ∈ Tr⇘_{ES}⇙›] by simp from V⇩_{2}_union_C⇩_{2}_subset_V⇩_{1}_union_C⇩_{1}‹β''' ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = β ↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› have "β''' ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) = β ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙)" using non_empty_projection_on_subset by blast from 𝒱⇩_{1}IsViewOnE 𝒱⇩_{2}IsViewOnE V2_subset_V1 C2_subset_C1 c⇩_{1}_in_C⇩_{1}have "c⇩_{1}∉ V⇘_{𝒱⇩2}⇙" unfolding isViewOn_def V_valid_def VC_disjoint_def by auto with ‹α = γ⇩_{1}@ [c⇩_{1}] @ γ⇩_{2}› have "α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}) ↿ V⇘_{𝒱⇩2}⇙" unfolding projection_def by auto moreover from V2_subset_V1 ‹γ⇩_{2}' ↿ V⇘_{𝒱⇩1}⇙ = γ⇩_{2}↿ V⇘_{𝒱⇩1}⇙› have "γ⇩_{2}' ↿ V⇘_{𝒱⇩2}⇙ = γ⇩_{2}↿ V⇘_{𝒱⇩2}⇙" using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq) moreover from ‹γ⇩_{1}'↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙) = γ⇩_{1}↿(V⇘_{𝒱⇩1}⇙ ∪ C⇘_{𝒱⇩1}⇙)› have "γ⇩_{1}' ↿ V⇘_{𝒱⇩2}⇙ = γ⇩_{1}↿ V⇘_{𝒱⇩2}⇙" using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq) ultimately have "α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}' @ γ⇩_{2}') ↿ V⇘_{𝒱⇩2}⇙" using ‹α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}@ γ⇩_{2}) ↿ V⇘_{𝒱⇩2}⇙› by (simp add: projection_concatenation_commute) from ‹β''' ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙) = β ↿(V⇘_{𝒱⇩2}⇙ ∪ C⇘_{𝒱⇩2}⇙)› ‹α ↿ V⇘_{𝒱⇩2}⇙ = (γ⇩_{1}' @ γ⇩_{2}') ↿ V⇘_{𝒱⇩2}⇙› show ?case using witness by simp qed } thus ?thesis unfolding D_def by auto qed end context BSPTaxonomyDifferentViewsSecondDim begin (* lemma 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 ‹β @ δ' @ [