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