Theory IO_Sequence_Set

section ‹Properties of Sets of IO Sequences›

text ‹This theory contains various definitions for properties of sets of IO-traces.›

theory IO_Sequence_Set
imports FSM
begin


fun output_completion :: "('a × 'b) list set ⇒ 'b set ⇒ ('a × 'b) list set" where
  "output_completion P Out = P ∪ {io@[(fst xy, y)] | io xy y . y ∈ Out ∧ io@[xy] ∈ P ∧ io@[(fst xy, y)] ∉ P}"


fun output_complete_sequences :: "('a,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
  "output_complete_sequences M P = (∀ io ∈ P . io = [] ∨ (∀ y ∈ (outputs M) . (butlast io)@[(fst (last io), y)] ∈ P))"


fun acyclic_sequences :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b × 'c) list set ⇒ bool" where
  "acyclic_sequences M q P = (∀ p . (path M q p ∧ p_io p ∈ P) ⟶ distinct (visited_states q p))"

fun acyclic_sequences' :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b × 'c) list set ⇒ bool" where
  "acyclic_sequences' M q P = (∀ io ∈ P . ∀ p ∈ (paths_for_io M q io) .  distinct (visited_states q p))"

lemma acyclic_sequences_alt_def[code] : "acyclic_sequences M P = acyclic_sequences' M P"
  unfolding acyclic_sequences'.simps acyclic_sequences.simps paths_for_io_def
  by blast

fun single_input_sequences :: "('a,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
  "single_input_sequences M P = (∀ xys1 xys2 xy1 xy2 . (xys1@[xy1] ∈ P ∧ xys2@[xy2] ∈ P ∧ io_targets M xys1 (initial M) = io_targets M xys2 (initial M)) ⟶ fst xy1 = fst xy2)"

fun single_input_sequences' :: "('a,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
  "single_input_sequences' M P = (∀ io1 ∈ P . ∀ io2 ∈ P . io1 = [] ∨ io2 = [] ∨ ((io_targets M (butlast io1) (initial M) = io_targets M (butlast io2) (initial M)) ⟶ fst (last io1) = fst (last io2)))"

lemma single_input_sequences_alt_def[code] : "single_input_sequences M P = single_input_sequences' M P"
  unfolding single_input_sequences.simps single_input_sequences'.simps
  by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)

fun output_complete_for_FSM_sequences_from_state :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b × 'c) list set ⇒ bool" where
  "output_complete_for_FSM_sequences_from_state M q P = (∀ io xy t . io@[xy] ∈ P ∧ t ∈ transitions M ∧ t_source t ∈ io_targets M io q ∧ t_input t = fst xy ⟶ io@[(fst xy, t_output t)] ∈ P)"

lemma output_complete_for_FSM_sequences_from_state_alt_def :
  shows "output_complete_for_FSM_sequences_from_state M q P = (∀ xys xy y . (xys@[xy] ∈ P ∧ (∃ q' ∈ (io_targets M xys q) . [(fst xy,y)] ∈ LS M q')) ⟶ xys@[(fst xy,y)] ∈ P)"  
proof -
  have "⋀ xys xy y q' . q' ∈ (io_targets M xys q) ⟹ [(fst xy,y)] ∈ LS M q' ⟹ ∃ t . t ∈ transitions M ∧ t_source t ∈ io_targets M xys q ∧ t_input t = fst xy ∧ t_output t = y" 
    unfolding io_targets.simps LS.simps
    using path_append path_append_transition_elim(2) by fastforce 

  moreover have "⋀ xys xy y t . t ∈ transitions M ⟹ t_source t ∈ io_targets M xys q ⟹ t_input t = fst xy ⟹ t_output t = y ⟹ ∃ q' ∈ (io_targets M xys q) . [(fst xy,y)] ∈ LS M q'"
    unfolding io_targets.simps LS.simps
  proof -
    fix xys :: "('b × 'c) list" and xy :: "'b × 'd" and y :: 'c and t :: "'a × 'b × 'c × 'a"
    assume a1: "t_input t = fst xy"
    assume a2: "t_output t = y"
    assume a3: "t_source t ∈ {target q p |p. path M q p ∧ p_io p = xys}"
    assume a4: "t ∈ FSM.transitions M"
    have "∀p f. [f (p::'a × 'b × 'c × 'a)::'b × 'c] = map f [p]"
      by simp
    then have "∃a. (∃ps. [(t_input t, t_output t)] = p_io ps ∧ path M a ps) ∧ a ∈ {target q ps |ps. path M q ps ∧ p_io ps = xys}"
      using a4 a3 by (meson single_transition_path)
    then have "∃a. [(t_input t, t_output t)] ∈ {p_io ps |ps. path M a ps} ∧ a ∈ {target q ps |ps. path M q ps ∧ p_io ps = xys}"
      by auto
    then show "∃a∈{target q ps |ps. path M q ps ∧ p_io ps = xys}. [(fst xy, y)] ∈ {p_io ps |ps. path M a ps}"
      using a2 a1 by (metis (no_types, lifting)) 
  qed

  ultimately show ?thesis
    unfolding output_complete_for_FSM_sequences_from_state.simps by blast
qed

fun output_complete_for_FSM_sequences_from_state' :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b × 'c) list set ⇒ bool" where
  "output_complete_for_FSM_sequences_from_state' M q P = (∀ io∈P . ∀ t ∈ transitions M . io = [] ∨ (t_source t ∈ io_targets M (butlast io) q ∧ t_input t = fst (last io) ⟶ (butlast io)@[(fst (last io), t_output t)] ∈ P))"

lemma output_complete_for_FSM_sequences_alt_def'[code] : "output_complete_for_FSM_sequences_from_state M q P = output_complete_for_FSM_sequences_from_state' M q P"
  unfolding output_complete_for_FSM_sequences_from_state.simps output_complete_for_FSM_sequences_from_state'.simps
  by (metis last_snoc snoc_eq_iff_butlast)

fun deadlock_states_sequences :: "('a,'b,'c) fsm ⇒ 'a set ⇒ ('b × 'c) list set ⇒ bool" where
  "deadlock_states_sequences M Q P = (∀ xys ∈ P . 
                                        ((io_targets M xys (initial M) ⊆ Q 
                                          ∧ ¬ (∃ xys' ∈ P . length xys < length xys' ∧ take (length xys) xys' = xys)))
                                      ∨ (¬ io_targets M xys (initial M) ∩ Q = {} 
                                          ∧ (∃ xys' ∈ P . length xys < length xys' ∧ take (length xys) xys' = xys)))" 

fun reachable_states_sequences :: "('a,'b,'c) fsm ⇒ 'a set ⇒ ('b × 'c) list set ⇒ bool" where
  "reachable_states_sequences M Q P = (∀ q ∈ Q . ∃ xys ∈ P . q ∈ io_targets M xys (initial M))"

fun prefix_closed_sequences :: "('b × 'c) list set ⇒ bool" where
  "prefix_closed_sequences P = (∀ xys1 xys2 . xys1@xys2 ∈ P ⟶ xys1 ∈ P)"

fun prefix_closed_sequences' :: "('b × 'c) list set ⇒ bool" where
  "prefix_closed_sequences' P = (∀ io ∈ P . io = [] ∨ (butlast io) ∈ P)"

lemma prefix_closed_sequences_alt_def[code] : "prefix_closed_sequences P = prefix_closed_sequences' P"
proof 
  show "prefix_closed_sequences P ⟹ prefix_closed_sequences' P"
    unfolding prefix_closed_sequences.simps prefix_closed_sequences'.simps
    by (metis append_butlast_last_id) 

  have "⋀xys1 xys2. ∀io∈P. io = [] ∨ butlast io ∈ P ⟹ xys1 @ xys2 ∈ P ⟹ xys1 ∈ P"
  proof -
    fix xys1 xys2 assume "∀io∈P. io = [] ∨ butlast io ∈ P" and "xys1 @ xys2 ∈ P"
    then show "xys1 ∈ P"
    proof (induction xys2 rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc a xys2)
      then show ?case
        by (metis append.assoc snoc_eq_iff_butlast) 
    qed
  qed

  then show "prefix_closed_sequences' P ⟹ prefix_closed_sequences P"
    unfolding prefix_closed_sequences.simps prefix_closed_sequences'.simps by blast 
qed

subsection ‹Completions›

definition prefix_completion :: "'a list set ⇒ 'a list set" where
  "prefix_completion P = {xs . ∃ ys . xs@ys ∈ P}"

lemma prefix_completion_closed :
  "prefix_closed_sequences (prefix_completion P)"
  unfolding prefix_closed_sequences.simps prefix_completion_def
  by auto 

lemma prefix_completion_source_subset :
  "P ⊆ prefix_completion P" 
  unfolding prefix_completion_def
  by (metis (no_types, lifting) append_Nil2 mem_Collect_eq subsetI) 


definition output_completion_for_FSM :: "('a,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ ('b × 'c) list set" where
  "output_completion_for_FSM M P = P ∪ { io@[(x,y')] | io x y' . (y' ∈ (outputs M)) ∧ (∃ y . io@[(x,y)] ∈ P)}"

lemma output_completion_for_FSM_complete :
  shows "output_complete_sequences M (output_completion_for_FSM M P)"
  unfolding output_completion_for_FSM_def output_complete_sequences.simps 
proof 
  fix io assume *: "io ∈ P ∪ {io @ [(x, y')] |io x y'. y' ∈ (outputs M) ∧ (∃y. io @ [(x, y)] ∈ P)}"
  show   "io = [] ∨
          (∀y∈(outputs M).
              butlast io @ [(fst (last io), y)]
              ∈ P ∪ {io @ [(x, y')] |io x y'. y' ∈ (outputs M) ∧ (∃y. io @ [(x, y)] ∈ P)})"
  proof (cases io rule: rev_cases)
    case Nil
    then show ?thesis by blast
  next
    case (snoc ys y)
    then show ?thesis proof (cases "io ∈ P")
      case True  
      then have "butlast io @ [(fst (last io), (snd (last io)))] ∈ P" using snoc by auto
      then show ?thesis using snoc by blast
    next
      case False
      then show ?thesis
        using "*" by auto 
    qed 
  qed
qed

lemma output_completion_for_FSM_length :
  assumes "∀ io ∈ P . length io ≤ k"
  shows   "∀ io ∈ output_completion_for_FSM M P. length io ≤ k" 
  using assms unfolding output_completion_for_FSM_def
  by auto 

lemma output_completion_for_FSM_code[code] :
  "output_completion_for_FSM M P = P ∪ (⋃(image (λ(y,io) . if length io = 0 then {} else {((butlast io)@[(fst (last io),y)])})  ((outputs M) × P)))"  
proof -
  let ?OC = "{io @ [(x, y')] |io x y'. y' ∈ FSM.outputs M ∧ (∃y. io @ [(x, y)] ∈ P)}"
  let ?OC' = "(⋃(y, io)∈FSM.outputs M × P. if length io = 0 then {} else {butlast io @ [(fst (last io), y)]})"

  have "?OC = ?OC'"
  proof -
    have "?OC ⊆ ?OC'"
    proof 
      fix io' assume "io' ∈ ?OC"
      then obtain io x y y' where "io' = io @ [(x, y')]"
                            and   "y' ∈ FSM.outputs M"
                            and   "io @ [(x, y)] ∈ P"
        by blast
      then have "(y',io @ [(x, y)]) ∈ FSM.outputs M × P" by blast
      moreover have "length (io @ [(x, y)]) ≠ 0" by auto
      ultimately show "io' ∈ ?OC'"
        unfolding ‹io' = io @ [(x, y')]› by force
    qed
    moreover have "?OC' ⊆ ?OC" 
    proof 
      fix io' assume "io' ∈ ?OC'"
      then obtain y io where "y ∈ outputs M" and "io ∈ P"
                       and "io' ∈ (if length io = 0 then {} else {butlast io @ [(fst (last io), y)]})"
        by auto
      then have "io' = butlast io @ [(fst (last io), y)]"
        by (meson empty_iff singletonD)
      have "io ≠ []"
        using ‹io' ∈ (if length io = 0 then {} else {butlast io @ [(fst (last io), y)]})›
        by auto 

      then have "butlast io @ [(fst (last io), snd (last io))] ∈ P"
        by (simp add: ‹io ∈ P›)

      then show "io' ∈ ?OC"
        using ‹y ∈ outputs M› ‹io ∈ P›
        unfolding ‹io' = butlast io @ [(fst (last io), y)]› by blast
    qed
    ultimately show ?thesis by blast
  qed

  then show ?thesis 
    unfolding output_completion_for_FSM_def
    by simp 
qed


end