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