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