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