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