```section ‹Adaptive Test Cases›

text ‹An ATC is a single input, acyclic, observable FSM, which is equivalent to a tree whose non-leaf
states are labeled with inputs and whose edges are labeled with outputs.›

imports State_Separator
begin

definition is_ATC :: "('a,'b,'c) fsm ⇒ bool" where
"is_ATC M = (single_input M ∧ acyclic M ∧ observable M)"

lemma is_ATC_from :
assumes "t ∈ transitions A"
and     "t_source t ∈ reachable_states A"
and     "is_ATC A"
shows "is_ATC (from_FSM A (t_target t))"
using from_FSM_single_input[of A]
from_FSM_acyclic[OF reachable_states_next[OF assms(2,1)]]
from_FSM_observable[of A]
assms(3)
unfolding is_ATC_def by fast

(* FSM M passes ATC A if and only if the parallel execution of M and A does not visit a fail_state in A and M produces no output not allowed in A *)
fun pass_ATC' :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'd set ⇒ nat ⇒ bool" where
"pass_ATC' M A fail_states 0 = (¬ (initial A ∈ fail_states))" |
"pass_ATC' M A fail_states (Suc k) = ((¬ (initial A ∈ fail_states)) ∧
(∀ x ∈ inputs A . h A (initial A,x) ≠ {} ⟶ (∀ (yM,qM) ∈ h M (initial M,x) . ∃ (yA,qA) ∈ h A (initial A,x) . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) fail_states k)))"

(* Applies pass_ATC' for a depth of at most (size A) (i.e., an upper bound on the length of paths in A) *)
fun pass_ATC :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'd set ⇒ bool" where
"pass_ATC M A fail_states = pass_ATC' M A fail_states (size A)"

lemma pass_ATC'_initial :
assumes "pass_ATC' M A FS k"
shows "initial A ∉ FS"
using assms by (cases k; auto)

lemma pass_ATC'_io :
assumes "pass_ATC' M A FS k"
and     "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "io@[ioA] ∈ L A"
and     "io@[ioM] ∈ L M"
and     "fst ioA = fst ioM"
and     "length (io@[ioA]) ≤ k"
shows "io@[ioM] ∈ L A"
and   "io_targets A (io@[ioM]) (initial A) ∩ FS = {}"
proof -
have "io@[ioM] ∈ L A ∧ io_targets A (io@[ioM]) (initial A) ∩ FS = {}"
using assms proof (induction k arbitrary: io A M)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case proof (cases io)
case Nil

obtain tA where "tA ∈ transitions A"
and "t_source tA = initial A"
and "t_input tA = fst ioA"
and "t_output tA = snd ioA"
using Nil ‹io@[ioA] ∈ L A› by auto
then have "fst ioA ∈ (inputs A)"
using fsm_transition_input by fastforce

have "(t_output tA,t_target tA) ∈ h A (initial A,t_input tA)"
using ‹tA ∈ transitions A› ‹t_source tA = initial A› unfolding h_simps
by (metis (no_types, lifting) case_prodI mem_Collect_eq prod.collapse)
then have "h A (initial A,fst ioA) ≠ {}"
unfolding ‹t_input tA = fst ioA› by blast

then have *: "⋀ yM qM . (yM,qM) ∈ h M (initial M,fst ioA) ⟹ (∃ (yA,qA) ∈ h A (initial A,fst ioA) . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) FS k)"
using Suc.prems(1) pass_ATC'_initial[OF Suc.prems(1)] unfolding pass_ATC'.simps
using ‹fst ioA ∈ FSM.inputs A› by auto

obtain tM where "tM ∈ transitions M"
and "t_source tM = initial M"
and "t_input tM = fst ioA"
and "t_output tM = snd ioM"
using Nil ‹io@[ioM] ∈ L M› ‹fst ioA = fst ioM› by auto
have "(t_output tM,t_target tM) ∈ h M (initial M,fst ioA)"
using ‹tM ∈ transitions M› ‹t_source tM = initial M› ‹t_input tM = fst ioA› unfolding h_simps
by (metis (mono_tags, lifting) case_prodI mem_Collect_eq prod.collapse)

obtain tA' where "tA' ∈ transitions A"
and "t_source tA' = initial A"
and "t_input tA' = fst ioA"
and "t_output tA' = snd ioM"
and "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k"
using *[OF ‹(t_output tM,t_target tM) ∈ h M (initial M,fst ioA)›]
unfolding h.simps ‹t_output tM = snd ioM› by fastforce

then have "path A (initial A) [tA']"
using single_transition_path[OF ‹tA' ∈ transitions A›] by auto
moreover have "p_io [tA'] = [ioM]"
using ‹t_input tA' = fst ioA› ‹t_output tA' = snd ioM› unfolding ‹fst ioA = fst ioM› by auto
ultimately have "[ioM] ∈ LS A (initial A)"
unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq)
then have "io @ [ioM] ∈ LS A (initial A)"
using Nil by auto

have "target (initial A) [tA'] = t_target tA'"
by auto
then have "t_target tA' ∈ io_targets A [ioM] (initial A)"
unfolding io_targets.simps
using ‹path A (initial A) [tA']› ‹p_io [tA'] = [ioM]›
by (metis (mono_tags, lifting) mem_Collect_eq)
then have "io_targets A (io @ [ioM]) (initial A) = {t_target tA'}"
using observable_io_targets[OF _ ‹io @ [ioM] ∈ LS A (initial A)›] ‹is_ATC A› Nil
unfolding is_ATC_def
by (metis append_self_conv2 singletonD)
moreover have "t_target tA' ∉ FS"
using pass_ATC'_initial[OF ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k›]
unfolding from_FSM_simps(1)[OF fsm_transition_target[OF ‹tA' ∈ transitions A›]] by assumption
ultimately have "io_targets A (io @ [ioM]) (initial A) ∩ FS = {}"
by auto

then show ?thesis
using ‹io @ [ioM] ∈ LS A (initial A)› by auto
next
case (Cons io' io'')

have "[io'] ∈ L A"
using Cons ‹io@[ioA] ∈ L A›
by (metis append.left_neutral append_Cons language_prefix)
then obtain tA where "tA ∈ transitions A"
and "t_source tA = initial A"
and "t_input tA = fst io'"
and "t_output tA = snd io'"
by auto
then have "fst io' ∈ (inputs A)"
using fsm_transition_input by metis

have "(t_output tA,t_target tA) ∈ h A (initial A,t_input tA)"
using ‹tA ∈ transitions A› ‹t_source tA = initial A› unfolding h_simps
by (metis (no_types, lifting) case_prodI mem_Collect_eq prod.collapse)
then have "h A (initial A,fst io') ≠ {}"
unfolding ‹t_input tA = fst io'› by blast

then have *: "⋀ yM qM . (yM,qM) ∈ h M (initial M,fst io') ⟹ (∃ (yA,qA) ∈ h A (initial A,fst io') . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) FS k)"
using Suc.prems(1) pass_ATC'_initial[OF Suc.prems(1)] unfolding pass_ATC'.simps
using ‹fst io' ∈ FSM.inputs A› by auto

obtain tM where "tM ∈ transitions M"
and "t_source tM = initial M"
and "t_input tM = fst io'"
and "t_output tM = snd io'"
using Cons ‹io@[ioM] ∈ L M› ‹fst ioA = fst ioM› by auto
have "(t_output tM,t_target tM) ∈ h M (initial M,fst io')"
using ‹tM ∈ transitions M› ‹t_source tM = initial M› ‹t_input tM = fst io'› unfolding h_simps
by (metis (mono_tags, lifting) case_prodI mem_Collect_eq prod.collapse)

obtain tA' where "tA' ∈ transitions A"
and "t_source tA' = initial A"
and "t_input tA' = fst io'"
and "t_output tA' = snd io'"
and "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k"
using *[OF ‹(t_output tM,t_target tM) ∈ h M (initial M,fst io')›]
unfolding h.simps ‹t_output tM = snd io'› by fastforce

then have "tA = tA'"
using ‹is_ATC A›
unfolding is_ATC_def observable.simps
by (metis ‹tA ∈ transitions A› ‹t_input tA = fst io'› ‹t_output tA = snd io'› ‹t_source tA = initial A› prod.collapse)
then have "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA)) FS k"
using ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k› by auto

have "(inputs (from_FSM A (t_target tA))) ⊆ (inputs (from_FSM M (t_target tM)))"
using Suc.prems(4)
unfolding from_FSM_simps(2)[OF fsm_transition_target[OF ‹tM ∈ transitions M›]]
from_FSM_simps(2)[OF fsm_transition_target[OF ‹tA ∈ transitions A›]] by assumption

have "length (io'' @ [ioA]) ≤ k"
using Cons ‹length (io @ [ioA]) ≤ Suc k› by auto

have "(io' # (io''@[ioA])) ∈ LS A (t_source tA)"
using ‹t_source tA = initial A› ‹io@[ioA] ∈ L A› Cons by auto
have "io'' @ [ioA] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))"
using observable_language_next[OF ‹(io' # (io''@[ioA])) ∈ LS A (t_source tA)›]
‹is_ATC A› ‹tA ∈ transitions A› ‹t_input tA = fst io'› ‹t_output tA = snd io'›
using is_ATC_def by blast

have "(io' # (io''@[ioM])) ∈ LS M (t_source tM)"
using ‹t_source tM = initial M› ‹io@[ioM] ∈ L M› Cons by auto
have "io'' @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))"
using observable_language_next[OF ‹(io' # (io''@[ioM])) ∈ LS M (t_source tM)›]
‹observable M› ‹tM ∈ transitions M› ‹t_input tM = fst io'› ‹t_output tM = snd io'›
by blast

have "observable (from_FSM M (t_target tM))"
using from_FSM_observable[OF ‹observable M›] by blast

have "is_ATC (FSM.from_FSM A (t_target tA))"
using is_ATC_from[OF ‹tA ∈ transitions A› _  ‹is_ATC A›] reachable_states_initial
unfolding ‹t_source tA = initial A› by blast

have "io'' @ [ioM] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))"
and "io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ∩ FS = {}"
using Suc.IH[OF ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA)) FS k›
‹is_ATC (FSM.from_FSM A (t_target tA))›
‹observable (from_FSM M (t_target tM))›
‹(inputs (from_FSM A (t_target tA))) ⊆ (inputs (from_FSM M (t_target tM)))›
‹io'' @ [ioA] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))›
‹io'' @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))›
‹fst ioA = fst ioM›
‹length (io'' @ [ioA]) ≤ k›]
by blast+

then obtain pA where "path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) pA" and "p_io pA = io'' @ [ioM]"
by auto

have "path A (initial A) (tA#pA)"
using ‹path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) pA› ‹tA ∈ transitions A›
by (metis ‹t_source tA = initial A› cons from_FSM_path_initial fsm_transition_target)
moreover have "p_io (tA#pA) = io' # io'' @ [ioM]"
using ‹t_input tA = fst io'› ‹t_output tA = snd io'› ‹p_io pA = io'' @ [ioM]› by auto
ultimately have "io' # io'' @ [ioM] ∈ L A"
unfolding LS.simps
by (metis (mono_tags, lifting) mem_Collect_eq)
then have "io @ [ioM] ∈ L A"
using Cons by auto

have "observable A"
using Suc.prems(2) is_ATC_def by blast

have "io_targets A (io @ [ioM]) (FSM.initial A) ∩ FS = {}"
proof -
have "⋀ p . path A (FSM.initial A) p ⟹ p_io p = (io' # io'') @ [ioM] ⟹ p = tA # (tl p)"
using ‹observable A› unfolding observable.simps
using ‹tA ∈ transitions A› ‹t_source tA = initial A› ‹t_input tA = fst io'› ‹t_output tA = snd io'› by fastforce

have "⋀ q . q ∈ io_targets A (io @ [ioM]) (FSM.initial A) ⟹ q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))"
proof -
fix q assume "q ∈ io_targets A (io @ [ioM]) (FSM.initial A)"
then obtain p where "q = target (FSM.initial A) p" and "path A (FSM.initial A) p" and "p_io p = (io' # io'') @ [ioM]"
unfolding io_targets.simps Cons by blast
then have "p = tA # (tl p)"
using ‹⋀ p . path A (FSM.initial A) p ⟹ p_io p = (io' # io'') @ [ioM] ⟹ p = tA # (tl p)› by blast

have "path A (FSM.initial A) (tA#(tl p))"
using ‹path A (FSM.initial A) p› ‹p = tA # (tl p)› by simp
then have "path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) (tl p)"
by (meson from_FSM_path_initial fsm_transition_target path_cons_elim)
moreover have "p_io (tl p) = (io'') @ [ioM]"
using ‹p_io p = (io' # io'') @ [ioM]› ‹p = tA # (tl p)› by auto
moreover have "q = target (initial (from_FSM A (t_target tA))) (tl p)"
using ‹q = target (FSM.initial A) p› ‹p = tA # (tl p)›
unfolding target.simps visited_states.simps from_FSM_simps[OF fsm_transition_target[OF ‹tA ∈ transitions A›]]
by (cases p; auto)
ultimately show "q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))"
unfolding io_targets.simps by blast
qed
moreover have "⋀ q . q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ⟹ q ∈ io_targets A (io @ [ioM]) (FSM.initial A)"
proof -
fix q assume "q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))"
then obtain p where "q = target (FSM.initial (FSM.from_FSM A (t_target tA))) p" and "path (FSM.from_FSM A (t_target tA)) (FSM.initial (FSM.from_FSM A (t_target tA))) p" and "p_io p = io'' @ [ioM]"
unfolding io_targets.simps Cons by blast

have "q = target (FSM.initial A) (tA#p)"
unfolding ‹q = target (FSM.initial (FSM.from_FSM A (t_target tA))) p› from_FSM_simps[OF fsm_transition_target[OF ‹tA ∈ transitions A›]] by auto
moreover have "path A (initial A) (tA#p)"
using ‹path (FSM.from_FSM A (t_target tA)) (FSM.initial (FSM.from_FSM A (t_target tA))) p›
unfolding from_FSM_path_initial[OF fsm_transition_target[OF ‹tA ∈ transitions A›], symmetric]
using ‹tA ∈ transitions A› ‹t_source tA = initial A› cons
by fastforce
moreover have "p_io (tA#p) = io @ [ioM]"
using ‹p_io p = io'' @ [ioM]› ‹t_input tA = fst io'› ‹t_output tA = snd io'› unfolding Cons by simp
ultimately show "q ∈ io_targets A (io @ [ioM]) (FSM.initial A)"
unfolding io_targets.simps by fastforce
qed
ultimately show ?thesis
using ‹io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ∩ FS = {}› by blast
qed

then show ?thesis
using ‹io @ [ioM] ∈ L A› by simp
qed
qed

then show "io@[ioM] ∈ L A"
and "io_targets A (io@[ioM]) (initial A) ∩ FS = {}"
by simp+
qed

lemma pass_ATC_io :
assumes "pass_ATC M A FS"
and     "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "io@[ioA] ∈ L A"
and     "io@[ioM] ∈ L M"
and     "fst ioA = fst ioM"
shows "io@[ioM] ∈ L A"
and   "io_targets A (io@[ioM]) (initial A) ∩ FS = {}"
proof -

have "acyclic A"
using ‹is_ATC A› is_ATC_def by blast

then have "length (io @ [ioA]) ≤ (size A)"
using ‹io@[ioA] ∈ L A› unfolding LS.simps
using acyclic_path_length_limit unfolding acyclic.simps by fastforce

show "io@[ioM] ∈ L A"
and  "io_targets A (io@[ioM]) (initial A) ∩ FS = {}"
using pass_ATC'_io[OF _ assms(2-7) ‹length (io @ [ioA]) ≤ (size A)›]
using assms(1) by simp+
qed

lemma pass_ATC_io_explicit_io_tuple :
assumes "pass_ATC M A FS"
and     "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "io@[(x,y)] ∈ L A"
and     "io@[(x,y')] ∈ L M"
shows "io@[(x,y')] ∈ L A"
and   "io_targets A (io@[(x,y')]) (initial A) ∩ FS = {}"
apply (metis pass_ATC_io(1) assms fst_conv)
by (metis pass_ATC_io(2) assms fst_conv)

lemma pass_ATC_io_fail_fixed_io :
assumes "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "io@[ioA] ∈ L A"
and     "io@[ioM] ∈ L M"
and     "fst ioA = fst ioM"
and     "io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}"
shows "¬pass_ATC M A FS"
proof -
consider (a) "io@[ioM] ∉ L A" |
(b) "io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}"
using assms(7) by blast
then show ?thesis proof (cases)
case a
then show ?thesis using pass_ATC_io(1)[OF _ assms(1-6)] by blast
next
case b
then show ?thesis using pass_ATC_io(2)[OF _ assms(1-6)] by blast
qed
qed

lemma pass_ATC'_io_fail :
assumes "¬pass_ATC' M A FS k "
and     "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
shows "initial A ∈ FS ∨ (∃ io ioA ioM . io@[ioA] ∈ L A
∧ io@[ioM] ∈ L M
∧ fst ioA = fst ioM
∧ (io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}))"
using assms proof (induction k arbitrary: M A)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case proof (cases "initial A ∈ FS")
case True
then show ?thesis by auto
next
case False
then obtain x where "x ∈ inputs A"
and "h A (FSM.initial A, x) ≠ {}"
and "¬(∀(yM, qM)∈h M (initial M, x). ∃(yA, qA)∈h A (FSM.initial A, x). yM = yA ∧ pass_ATC' (FSM.from_FSM M qM) (FSM.from_FSM A qA) FS k)"
using Suc.prems(1) unfolding pass_ATC'.simps
by fastforce

obtain tM where "tM ∈ transitions M"
and "t_source tM = initial M"
and "t_input tM = x"
and "¬(∃(yA, qA)∈h A (FSM.initial A, x). t_output tM = yA ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A qA) FS k)"
using ‹¬(∀(yM, qM)∈h M (initial M, x). ∃(yA, qA)∈h A (FSM.initial A, x). yM = yA ∧ pass_ATC' (FSM.from_FSM M qM) (FSM.from_FSM A qA) FS k)›
unfolding h.simps
by auto

have "¬ (∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x ∧ t_output tA = t_output tM ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target tA)) FS k)"
using ‹¬(∃(yA, qA)∈h A (FSM.initial A, x). t_output tM = yA ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A qA) FS k)›
unfolding h.simps by force
moreover have "∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x"
using ‹h A (FSM.initial A, x) ≠ {}› unfolding h.simps by force
ultimately consider
(a) "⋀ tA . tA ∈ transitions A ⟹ t_source tA = initial A ⟹ t_input tA = x ⟹ t_output tM ≠ t_output tA" |
(b) "∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x ∧ t_output tA = t_output tM ∧ ¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target tA)) FS k"
by force
then show ?thesis proof cases
case a
then have "[(x,t_output tM)] ∉ L A"
unfolding LS.simps by fastforce
moreover have "∃ y . [(x,y)] ∈ L A"
using ‹h A (FSM.initial A, x) ≠ {}› unfolding h.simps LS.simps
proof -
obtain pp :: "'d × 'b × 'c × 'd" where
f1: "pp ∈ FSM.transitions A ∧ t_source pp = FSM.initial A ∧ t_input pp = x"
using ‹∃tA. tA ∈ FSM.transitions A ∧ t_source tA = FSM.initial A ∧ t_input tA = x› by blast
then have "path A (FSM.initial A) [pp]"
by (metis single_transition_path)
then have "(t_input pp, t_output pp) # p_io ([]::('d × 'b × 'c × _) list) ∈ {p_io ps |ps. path A (FSM.initial A) ps}"
by force
then show "∃c. [(x, c)] ∈ {p_io ps |ps. path A (FSM.initial A) ps}"
using f1 by force
qed
moreover have "[(x,t_output tM)] ∈ L M"
unfolding LS.simps using ‹tM ∈ transitions M› ‹t_input tM = x› ‹t_source tM = initial M›
proof -
have "∃ps. p_io [tM] = p_io ps ∧ path M (FSM.initial M) ps"
by (metis (no_types) ‹tM ∈ FSM.transitions M› ‹t_source tM = FSM.initial M› single_transition_path)
then show "[(x, t_output tM)] ∈ {p_io ps |ps. path M (FSM.initial M) ps}"
by (simp add: ‹t_input tM = x›)
qed
ultimately have "(∃io ioA ioM. io @ [ioA] ∈ L A ∧ io @ [ioM] ∈ L M ∧ fst ioA = fst ioM ∧ (io @ [ioM] ∉ L A))"
by (metis append_self_conv2 fst_conv)
then show ?thesis by blast
next
case b
then obtain t' where "t' ∈ transitions A"
and "t_source t' = initial A"
and "t_input t' = x"
and "t_output t' = t_output tM"
and "¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target t')) FS k"
by blast

have "is_ATC (FSM.from_FSM A (t_target t'))"
using is_ATC_from[OF ‹t' ∈ transitions A› _ ‹is_ATC A›] reachable_states_initial
unfolding ‹t_source t' = initial A› by blast

have "(inputs (from_FSM A (t_target t'))) ⊆ (inputs (from_FSM M (t_target tM)))"
by (simp add: Suc.prems(4) ‹t' ∈ FSM.transitions A› ‹tM ∈ FSM.transitions M› fsm_transition_target)

let ?ioM = "(x,t_output tM)"
let ?ioA = "(x,t_output t')"

consider (b1) "initial (from_FSM A (t_target t')) ∈ FS" |
(b2) "(∃io ioA ioM.
io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∧
io @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM))) ∧
fst ioA = fst ioM ∧
(io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨
io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {}))"
using Suc.IH[OF ‹¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target t')) FS k›
‹is_ATC (FSM.from_FSM A (t_target t'))›
from_FSM_observable[OF ‹observable M›]
‹(inputs (from_FSM A (t_target t'))) ⊆ (inputs (from_FSM M (t_target tM)))›]
by blast
then show ?thesis proof cases
case b1 (* analogous to case a *)

have "[?ioA] ∈ L A"
unfolding LS.simps
proof -
have "∃ps. [(x, t_output t')] = p_io ps ∧ path A (t_source t') ps"
using ‹t' ∈ FSM.transitions A› ‹t_input t' = x› by force
then show "[(x, t_output t')] ∈ {p_io ps |ps. path A (FSM.initial A) ps}"
by (simp add: ‹t_source t' = FSM.initial A›)
qed

have "[?ioM] ∈ L M"
unfolding LS.simps
proof -
have "path M (FSM.initial M) [tM]"
by (metis ‹tM ∈ FSM.transitions M› ‹t_source tM = FSM.initial M› single_transition_path)
then have "∃ps. [(x, t_output tM)] = p_io ps ∧ path M (FSM.initial M) ps"
using ‹t_input tM = x› by force
then show "[(x, t_output tM)] ∈ {p_io ps |ps. path M (FSM.initial M) ps}"
by simp
qed

have "p_io [t'] = [(x, t_output tM)]"
using ‹t_input t' = x› ‹t_output t' = t_output tM›
by auto
moreover have "target (initial A) [t'] = t_target t'"
using ‹t_source t' = initial A› by auto
ultimately have "t_target t' ∈ io_targets A [(x,t_output tM)] (initial A)"
unfolding io_targets.simps
using single_transition_path[OF ‹t' ∈ transitions A›]
by (metis (mono_tags, lifting) ‹t_source t' = initial A› mem_Collect_eq)
then have "initial (from_FSM A (t_target t')) ∈ io_targets A [(x,t_output tM)] (initial A)"
unfolding io_targets.simps from_FSM_simps[OF fsm_transition_target[OF ‹t' ∈ transitions A›]] by simp
then have "io_targets A ([] @ [?ioM]) (initial A) ∩ FS ≠ {}"
using b1 by (metis IntI append_Nil empty_iff)

then have "∃ io ioA ioM . io@[ioA] ∈ L A
∧ io@[ioM] ∈ L M
∧ fst ioA = fst ioM
∧ io_targets A (io @ [ioM]) (initial A) ∩ FS ≠ {}"
using ‹[?ioA] ∈ L A› ‹[?ioM] ∈ L M›
by (metis ‹t_output t' = t_output tM› append.left_neutral)

then show ?thesis by blast

next
case b2 (* obtain io ioA ioM and prepend (x,t_output tM) *)

then obtain io ioA ioM where
"io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t')))"
and "io @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))"
and "fst ioA = fst ioM"
and "(io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨ io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {})"
by blast

have "observable A"
using Suc.prems(2) is_ATC_def by blast

have "(?ioM # io) @ [ioA] ∈ L A"
using language_state_prepend_transition[OF ‹io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t')))› ‹t' ∈ transitions A›]
using ‹t_input t' = x› ‹t_source t' = initial A› ‹t_output t' = t_output tM›
by simp

moreover have "(?ioM # io) @ [ioM] ∈ L M"
using language_state_prepend_transition[OF ‹io @ [ioM] ∈ L (from_FSM M (t_target tM))› ‹tM ∈ transitions M›]
using ‹t_input tM = x› ‹t_source tM = initial M›
by simp

moreover have "((?ioM # io) @ [ioM] ∉ L A ∨ io_targets A ((?ioM # io) @ [ioM]) (initial A) ∩ FS ≠ {})"
proof -
consider (f1) "io @ [ioM] ∉ L (from_FSM A (t_target t'))" |
(f2) "io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {}"
using ‹(io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨ io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {})›
by blast
then show ?thesis proof cases
case f1

have "p_io [t'] = [(x, t_output tM)]"
using ‹t_input t' = x› ‹t_output t' = t_output tM›
by auto
moreover have "target (initial A) [t'] = t_target t'"
using ‹t_source t' = initial A› by auto
ultimately have "t_target t' ∈ io_targets A [?ioM] (initial A)"
unfolding io_targets.simps
using single_transition_path[OF ‹t' ∈ transitions A›]
by (metis (mono_tags, lifting) ‹t_source t' = initial A› mem_Collect_eq)

show ?thesis
using observable_io_targets_language[of "[(x, t_output tM)]" "io@[ioM]" A "initial A" "t_target t'", OF _ ‹observable A› ‹t_target t' ∈ io_targets A [?ioM] (initial A)›]
f1
by (metis ‹observable A› ‹t' ∈ FSM.transitions A› ‹t_input t' = x› ‹t_output t' = t_output tM› ‹t_source t' = FSM.initial A› append_Cons fst_conv observable_language_next snd_conv)

next
case f2

have "io_targets A (p_io [t'] @ io @ [ioM]) (t_source t') = io_targets A ([?ioM] @ io @ [ioM]) (t_source t')"
using ‹t_input t' = x› ‹t_output t' = t_output tM› by auto
moreover have "io_targets A (io @ [ioM]) (t_target t') = io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t')))"
unfolding io_targets.simps
using from_FSM_path_initial[OF fsm_transition_target[OF ‹t' ∈ transitions A›]] by auto
ultimately have "io_targets A ([?ioM] @ io @ [ioM]) (t_source t') = io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t')))"
using observable_io_targets_next[OF ‹observable A› ‹t' ∈ transitions A›, of "io @ [ioM]"] by auto

then show ?thesis
using f2 ‹t_source t' = initial A› by auto
qed
qed

ultimately show ?thesis
using ‹fst ioA = fst ioM› by blast
qed
qed
qed
qed

lemma pass_ATC_io_fail :
assumes "¬pass_ATC M A FS"
and     "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
shows "initial A ∈ FS ∨ (∃ io ioA ioM . io@[ioA] ∈ L A
∧ io@[ioM] ∈ L M
∧ fst ioA = fst ioM
∧ (io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}))"
using pass_ATC'_io_fail[OF _ assms(2-4)] using assms(1) by auto

lemma pass_ATC_fail :
assumes "is_ATC A"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "io@[(x,y)] ∈ L A"
and     "io@[(x,y')] ∈ L M"
and     "io@[(x,y')] ∉ L A"
shows "¬ pass_ATC M A FS"
using assms(6) pass_ATC_io_explicit_io_tuple(1)[OF _ assms(1,2,3,4,5)]
by blast

lemma pass_ATC_reduction :
assumes "L M2 ⊆ L M1"
and     "is_ATC A"
and     "observable M1"
and     "observable M2"
and     "(inputs A) ⊆ (inputs M1)"
and     "(inputs M2) = (inputs M1)"
and     "pass_ATC M1 A FS"
shows "pass_ATC M2 A FS"
proof (rule ccontr)
assume "¬ pass_ATC M2 A FS"
have "(inputs A) ⊆ (inputs M2)"
using assms(5,6) by blast

have "initial A ∉ FS"
using ‹pass_ATC M1 A FS› by (cases "size A"; auto)
then show "False"
using pass_ATC_io_fail[OF ‹¬ pass_ATC M2 A FS› assms(2,4) ‹(inputs A) ⊆ (inputs M2)›]
using assms(1) assms(2) assms(3) assms(5) assms(7) pass_ATC_io_fail_fixed_io by blast
qed

lemma pass_ATC_fail_no_reduction :
assumes "is_ATC A"
and     "observable T"
and     "observable M"
and     "(inputs A) ⊆ (inputs M)"
and     "(inputs T) = (inputs M)"
and     "pass_ATC M A FS"
and     "¬pass_ATC T A FS"
shows   "¬ (L T ⊆ L M)"
using pass_ATC_reduction[OF _ assms(1,3,2,4,5,6)] assms(7) by blast

subsection ‹State Separators as Adaptive Test Cases›

fun pass_separator_ATC :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'a ⇒ 'd ⇒ bool" where
"pass_separator_ATC M S q1 t2 = pass_ATC (from_FSM M q1) S {t2}"

lemma separator_is_ATC :
assumes "is_separator M q1 q2 A t1 t2"
and     "observable M"
and     "q1 ∈ states M"
shows "is_ATC A"
unfolding is_ATC_def
using is_separator_simps(1,2,3)[OF assms(1)] by blast

lemma pass_separator_ATC_from_separator_left :
assumes "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
shows "pass_separator_ATC M A q1 t2"
proof (rule ccontr)
assume "¬ pass_separator_ATC M A q1 t2"

then have "¬ pass_ATC (from_FSM M q1) A {t2}"
by auto

have "is_ATC A"
using separator_is_ATC[OF assms(4,1,2)] by assumption

have "initial A ∉ {t2}"
using separator_initial(2)[OF assms(4)] by blast
then obtain io ioA ioM where
"io @ [ioA] ∈ L A"
"io @ [ioM] ∈ LS M q1"
"fst ioA = fst ioM"
"io @ [ioM] ∉ L A ∨ io_targets A (io @ [ioM]) (initial A) ∩ {t2} ≠ {}"

using pass_ATC_io_fail[OF ‹¬ pass_ATC (from_FSM M q1) A {t2}› ‹is_ATC A› from_FSM_observable[OF ‹observable M›] ]
using is_separator_simps(16)[OF assms(4)]
using from_FSM_language[OF ‹q1 ∈ states M›]
unfolding from_FSM_simps[OF ‹q1 ∈ states M›] by blast
then obtain x ya ym where
"io @ [(x,ya)] ∈ L A"
"io @ [(x,ym)] ∈ LS M q1"
"io @ [(x,ym)] ∉ L A ∨ io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} ≠ {}"
by (metis fst_eqD old.prod.exhaust)

have "io @ [(x,ym)] ∈ L A"
using is_separator_simps(9)[OF assms(4) ‹io @ [(x,ym)] ∈ LS M q1› ‹io @ [(x,ya)] ∈ L A›] by assumption

have "t1 ≠ t2" using is_separator_simps(15)[OF assms(4)] by assumption

consider (a) "io @ [(x, ym)] ∈ LS M q1 - LS M q2" |
(b) "io @ [(x, ym)] ∈ LS M q1 ∩ LS M q2"
using ‹io @ [(x,ym)] ∈ LS M q1› by blast
then have "io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} = {}"

proof (cases)
case a
show ?thesis using separator_language(1)[OF assms(4) ‹io @ [(x,ym)] ∈ L A› a] ‹t1 ≠ t2› by auto
next
case b
show ?thesis using separator_language(3)[OF assms(4) ‹io @ [(x,ym)] ∈ L A› b] ‹t1 ≠ t2› by auto
qed

then show "False"
using ‹io @ [(x,ym)] ∈ L A›
using ‹io @ [(x,ym)] ∉ L A ∨ io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} ≠ {}› by blast
qed

lemma pass_separator_ATC_from_separator_right :
assumes "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
shows "pass_separator_ATC M A q2 t1"
using assms(1-3) is_separator_sym[OF assms(4)] pass_separator_ATC_from_separator_left by metis

lemma pass_separator_ATC_path_left :
assumes "pass_separator_ATC S A s1 t2"
and     "observable S"
and     "observable M"
and     "s1 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "q1 ≠ q2"
and     "path A (initial A) pA"
and     "path S s1 pS"
and     "p_io pA = p_io pS"
shows "target (initial A) pA ≠ t2"
and   "∃ pM . path M q1 pM ∧ p_io pM = p_io pA"
proof -

have "pass_ATC (from_FSM S s1) A {t2}"
using ‹pass_separator_ATC S A s1 t2› by auto

have "is_ATC A"
using separator_is_ATC[OF assms(7,3,5)] by assumption

have "observable (from_FSM S s1)"
using from_FSM_observable[OF assms(2)] by assumption

have "(inputs A) ⊆ (inputs (from_FSM S s1))"
using is_separator_simps(16)[OF assms(7)] ‹(inputs S) = (inputs M)›
unfolding from_FSM_simps[OF ‹s1 ∈ states S›] by blast

have "target (initial A) pA ≠ t2 ∧ (∃ pM . path M q1 pM ∧ p_io pM = p_io pA)"
proof (cases pA rule: rev_cases)
case Nil
then have "target (initial A) pA ≠ t2"
using separator_initial(2)[OF assms(7)] by auto
moreover have "(∃ pM . path M q1 pM ∧ p_io pM = p_io pA)"
unfolding Nil using ‹q1 ∈ states M› by auto
ultimately show ?thesis by auto
next
case (snoc ys y)
then have "p_io pA = (p_io ys)@[(t_input y,t_output y)]"
by auto
then have *: "(p_io ys)@[(t_input y,t_output y)] ∈ L A"
using language_state_containment[OF ‹path A (initial A) pA›] by blast
then have "p_io pS = (p_io ys)@[(t_input y,t_output y)]"
using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› ‹p_io pA = p_io pS› by auto
then have **: "(p_io ys)@[(t_input y,t_output y)] ∈ L (from_FSM S s1)"
using language_state_containment[OF ‹path S s1 pS›]
unfolding from_FSM_language[OF ‹s1 ∈ states S›] by blast

have "io_targets A ((p_io ys)@[(t_input y,t_output y)]) (initial A) ∩ {t2} = {}"
using pass_ATC_io(2)[OF ‹pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))› * **]
unfolding fst_conv by auto
then have "target (initial A) pA ≠ t2"
using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› ‹path A (initial A) pA›
unfolding io_targets.simps
by blast

have "p_io ys @ [(t_input y, t_output y)] ∈ LS M q1"
using separator_language(2,4)[OF assms(7) ‹(p_io ys)@[(t_input y,t_output y)] ∈ L A›]
using ‹io_targets A ((p_io ys)@[(t_input y,t_output y)]) (initial A) ∩ {t2} = {}› by blast
then have "∃ pM . path M q1 pM ∧ p_io pM = p_io pA"
using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› by auto

then show ?thesis using ‹target (initial A) pA ≠ t2› by auto
qed

then show "target (initial A) pA ≠ t2" and   "∃ pM . path M q1 pM ∧ p_io pM = p_io pA"
by blast+
qed

lemma pass_separator_ATC_path_right :
assumes "pass_separator_ATC S A s2 t1"
and     "observable S"
and     "observable M"
and     "s2 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "q1 ≠ q2"
and     "path A (initial A) pA"
and     "path S s2 pS"
and     "p_io pA = p_io pS"
shows "target (initial A) pA ≠ t1"
and   "∃ pM . path M q2 pM ∧ p_io pM = p_io pA"
using pass_separator_ATC_path_left[OF assms(1-4,6,5) is_separator_sym[OF assms(7)] assms(8) _ assms(10-12)] assms(9) by blast+

lemma pass_separator_ATC_fail_no_reduction :
assumes "observable S"
and     "observable M"
and     "s1 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "¬pass_separator_ATC S A s1 t2"
shows   "¬ (LS S s1 ⊆ LS M q1)"
proof
assume "LS S s1 ⊆ LS M q1"

have "is_ATC A"
using separator_is_ATC[OF assms(6,2,4)] by assumption

have *: "(inputs A) ⊆ (inputs (from_FSM M q1))"
using is_separator_simps(16)[OF assms(6)]
unfolding is_submachine.simps canonical_separator_simps from_FSM_simps[OF ‹q1 ∈ states M›] by auto

have "pass_ATC (from_FSM M q1) A {t2}"
using pass_separator_ATC_from_separator_left[OF assms(2,4,5,6)] by auto

have "¬ pass_ATC (from_FSM S s1) A {t2}"
using ‹¬pass_separator_ATC S A s1 t2› by auto

moreover have "pass_ATC (from_FSM S s1) A {t2}"
using pass_ATC_reduction[OF _ ‹is_ATC A› from_FSM_observable[OF ‹observable M›] from_FSM_observable[OF ‹observable S›] *]
using ‹LS S s1 ⊆ LS M q1› ‹pass_ATC (from_FSM M q1) A {t2}›
unfolding from_FSM_language[OF assms(3)] from_FSM_language[OF assms(4)]
using ‹L (FSM.from_FSM S s1) = LS S s1› assms(3) assms(4) assms(7) by auto
ultimately show "False" by simp
qed

lemma pass_separator_ATC_pass_left :
assumes "observable S"
and     "observable M"
and     "s1 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "path A (initial A) p"
and     "p_io p ∈ LS S s1"
and     "q1 ≠ q2"
and     "pass_separator_ATC S A s1 t2"
shows "target (initial A) p ≠ t2"
and   "target (initial A) p = t1 ∨ (target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2)" (* useless? *)
proof -

from ‹p_io p ∈ LS S s1› obtain pS where "path S s1 pS" and "p_io p = p_io pS"
by auto

then show "target (initial A) p ≠ t2"
using pass_separator_ATC_path_left[OF assms(11,1-7,10,8)] by simp

obtain pM where "path M q1 pM" and "p_io pM = p_io p"
using pass_separator_ATC_path_left[OF assms(11,1-7,10,8) ‹path S s1 pS› ‹p_io p = p_io pS›]  by blast
then have "p_io p ∈ LS M q1"
unfolding LS.simps by force

then show "target (initial A) p = t1 ∨ (target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2)"
using separator_path_targets(1,3,4)[OF assms(6,8)] by blast
qed

lemma pass_separator_ATC_pass_right :
assumes "observable S"
and     "observable M"
and     "s2 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "path A (initial A) p"
and     "p_io p ∈ LS S s2"
and     "q1 ≠ q2"
and     "pass_separator_ATC S A s2 t1"
shows "target (initial A) p ≠ t1"
and   "target (initial A) p = t2 ∨ (target (initial A) p ≠ t2 ∧ target (initial A) p ≠ t2)"
using pass_separator_ATC_pass_left[OF assms(1,2,3,5,4) is_separator_sym[OF assms(6)] assms(7-9) _ assms(11)] assms(10) by blast+

lemma pass_separator_ATC_completely_specified_left :
assumes "observable S"
and     "observable M"
and     "s1 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "q1 ≠ q2"
and     "pass_separator_ATC S A s1 t2"
and     "completely_specified S"
shows "∃ p . path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1"
and   "¬ (∃ p . path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t2)"
proof -
have p1: "pass_ATC (from_FSM S s1) A {t2}"
using assms(9) by auto

have p2: "is_ATC A"
using separator_is_ATC[OF assms(6,2,4)] by assumption

have p3: "observable (from_FSM S s1)"
using from_FSM_observable[OF assms(1)] by assumption

have p4: "(inputs A) ⊆ (inputs (from_FSM S s1))"
using is_separator_simps(16)[OF assms(6)]
unfolding from_FSM_simps[OF ‹s1 ∈ states S›] is_submachine.simps canonical_separator_simps assms(7) by auto

have "t1 ≠ t2" and "observable A"
using is_separator_simps(15,3)[OF assms(6)] by linarith+

have path_ext: "⋀ p . path A (initial A) p ⟹ p_io p ∈ LS S s1 ⟹ (target (initial A) p ≠ t2) ∧ (target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1))"
proof -
fix p assume "path A (initial A) p" and "p_io p ∈ LS S s1"

consider (a) "target (initial A) p = t1" |
(b) "target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2"
using pass_separator_ATC_pass_left(2)[OF assms(1,2,3,4,5,6,7) ‹path A (initial A) p› ‹p_io p ∈ LS S s1› assms(8,9)] by blast
then have "target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1)"
proof cases
case a
then show ?thesis by blast
next
case b

let ?t3 = "target (initial A) p"
have "?t3 ≠ t1" and "?t3 ≠ t2"
using b by auto
moreover have "?t3 ∈ reachable_states A"
using ‹path A (initial A) p› reachable_states_intro by blast
ultimately have "¬ deadlock_state A ?t3"
using is_separator_simps(8)[OF assms(6)] by blast
then obtain tt where "tt ∈ transitions A" and "t_source tt = ?t3"
by auto

then have "path A (initial A) (p@[tt])"
using ‹path A (initial A) p› using path_append_transition by metis

moreover have "p_io (p@[tt]) = (p_io p)@[(t_input tt, t_output tt)]"
by auto

ultimately have "(p_io p)@[(t_input tt,t_output tt)] ∈ L A"
using language_state_containment[of A "initial A" "p@[tt]"] by metis

let ?x = "t_input tt"
have "?x ∈ (inputs S)"
using ‹tt ∈ transitions A› is_separator_simps(16)[OF assms(6)] assms(7) by auto
then obtain y where "(p_io p)@[(?x,y)] ∈ LS S s1"
using completely_specified_language_extension[OF ‹completely_specified S› ‹s1 ∈ states S› ‹p_io p ∈ LS S s1› ] by auto

then have "p_io p @ [(?x, y)] ∈ LS A (initial A)"
using pass_ATC_io_explicit_io_tuple(1)[OF p1 p2 p3 p4 ‹(p_io p)@[(t_input tt,t_output tt)] ∈ L A›]
unfolding from_FSM_language[OF ‹s1 ∈ states S›] by auto

then obtain tt' where "path A (initial A) (p@[tt'])" and "t_input tt' = ?x" and "t_output tt' = y"
using language_path_append_transition_observable[OF _ ‹path A (initial A) p› ‹observable A›] by blast

then have "p_io (p @ [tt']) ∈ LS S s1"
using ‹(p_io p)@[(?x,y)] ∈ LS S s1› by auto
then show ?thesis
using ‹path A (initial A) (p@[tt'])› by meson
qed

moreover have "target (initial A) p ≠ t2"
using pass_separator_ATC_pass_left(1)[OF assms(1,2,3,4,5,6,7) ‹path A (initial A) p› ‹p_io p ∈ LS S s1› assms(8,9)] by assumption

ultimately show "(target (initial A) p ≠ t2) ∧ (target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1))"
by simp
qed

(* largest path that satisfies (path A (initial A) p) and (p_io p ∈ LS T t1) cannot be extended further and must thus target (Inr q1)  *)

have "acyclic A"
using ‹is_ATC A› is_ATC_def by auto
then have "finite {p . path A (initial A) p}"
using acyclic_paths_finite[of A "initial A"] unfolding acyclic.simps
by (metis (no_types, lifting) Collect_cong)
then have "finite {p . path A (initial A) p ∧ p_io p ∈ LS S s1}"
by auto

have "[] ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1}"
using ‹s1 ∈ states S› by auto
then have "{p . path A (initial A) p ∧ p_io p ∈ LS S s1} ≠ {}"
by blast

have scheme: "⋀ S . finite S ⟹ S ≠ {} ⟹ ∃ x ∈ S . ∀ y ∈ S . length y ≤ length x"
by (meson leI max_length_elem)

obtain p where "p ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1}" and "⋀ p' . p' ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1} ⟹ length p' ≤ length p"
using scheme[OF ‹finite {p . path A (initial A) p ∧ p_io p ∈ LS S s1}› ‹{p . path A (initial A) p ∧ p_io p ∈ LS S s1} ≠ {}›]
by blast
then have "path A (initial A) p" and "p_io p ∈ LS S s1" and "⋀ p' . path A (initial A) p' ⟹ p_io p' ∈ LS S s1 ⟹ length p' ≤ length p"
by blast+

have "target (initial A) p = t1"
using path_ext[OF ‹path A (initial A) p› ‹p_io p ∈ LS S s1›] ‹⋀ p' . path A (initial A) p' ⟹ p_io p' ∈ LS S s1 ⟹ length p' ≤ length p›
by (metis (no_types, lifting) Suc_n_not_le_n length_append_singleton)

then show "∃p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1"
using ‹path A (initial A) p› ‹p_io p ∈ LS S s1› by blast

show "∄p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t2"
using path_ext by blast
qed

lemma pass_separator_ATC_completely_specified_right :
assumes "observable S"
and     "observable M"
and     "s2 ∈ states S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "is_separator M q1 q2 A t1 t2"
and     "(inputs S) = (inputs M)"
and     "q1 ≠ q2"
and     "pass_separator_ATC S A s2 t1"
and     "completely_specified S"
shows "∃ p . path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t2"
and   "¬ (∃ p . path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t1)"
using pass_separator_ATC_completely_specified_left[OF assms(1,2,3,5,4) is_separator_sym[OF assms(6)] assms(7) _ assms(9,10)] assms(8) by blast+

lemma pass_separator_ATC_reduction_distinction :
assumes "observable M"
and     "observable S"
and     "(inputs S) = (inputs M)"
and     "pass_separator_ATC S A s1 t2"
and     "pass_separator_ATC S A s2 t1"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
and     "s1 ∈ states S"
and     "s2 ∈ states S"
and     "is_separator M q1 q2 A t1 t2"
and     "completely_specified S"
shows "s1 ≠ s2"
proof -

(* As s1 passes A against t2, t1 must be reached during application, while
at the same time t2 is never reached *)

have "∃p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1"
using pass_separator_ATC_completely_specified_left[OF assms(2,1,9,6,7,11,3,8,4,12)] by blast

(* As s2 passes A against t1, t2 must be reached during application, while
at the same time t1 is never reached *)

moreover have "¬ (∃p. path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t1)"
using pass_separator_ATC_completely_specified_right[OF assms(2,1,10,6,7,11,3,8,5,12)] by blast

(* Thus it is not possible for (s1 = s2) to hold *)

ultimately show "s1 ≠ s2" by blast
qed

lemma pass_separator_ATC_failure_left :
assumes "observable M"
and     "observable S"
and     "(inputs S) = (inputs M)"
and     "is_separator M q1 q2 A t1 t2"
and     "¬ pass_separator_ATC S A s1 t2"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
and     "s1 ∈ states S"
shows "LS S s1 - LS M q1 ≠ {}"
proof -

have p1: "is_ATC A"
using separator_is_ATC[OF assms(4,1,6)] by assumption

have p2: "observable (from_FSM S s1)"
using from_FSM_observable[OF assms(2)] by assumption

have p3: "observable (from_FSM M q1)"
using from_FSM_observable[OF assms(1)] by assumption

have p4: "(inputs A) ⊆ (inputs (from_FSM M q1))"
using is_separator_simps(16)[OF assms(4)]
unfolding from_FSM_simps[OF ‹q1 ∈ states M›] is_submachine.simps canonical_separator_simps assms(3) by auto

have p5: "(inputs (from_FSM S s1)) = (inputs (from_FSM M q1))"
using assms(3,6,9) by simp

have p6: "pass_ATC (from_FSM M q1) A {t2}"
using pass_separator_ATC_from_separator_left[OF assms(1,6,7,4)] by auto

have p7: "¬ pass_ATC (from_FSM S s1) A {t2}"
using assms(5) by auto

show ?thesis
using pass_ATC_fail_no_reduction[OF p1 p2 p3 p4 p5 p6 p7]
unfolding from_FSM_language[OF ‹q1 ∈ states M›] from_FSM_language[OF ‹s1 ∈ states S›] by blast
qed

lemma pass_separator_ATC_failure_right :
assumes "observable M"
and     "observable S"
and     "(inputs S) = (inputs M)"
and     "is_separator M q1 q2 A t1 t2"
and     "¬ pass_separator_ATC S A s2 t1"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
and     "s2 ∈ states S"
shows "LS S s2 - LS M q2 ≠ {}"
using pass_separator_ATC_failure_left[OF assms(1-3) is_separator_sym[OF assms(4)] assms(5,7,6) _ assms(9)] assms(8) by blast

subsection ‹ATCs Represented as Sets of IO Sequences›

fun atc_to_io_set :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set" where
"atc_to_io_set M A = L M ∩ L A"

lemma atc_to_io_set_code :
assumes "acyclic A"
shows "atc_to_io_set M A = acyclic_language_intersection M A"
using acyclic_language_intersection_completeness[OF assms] unfolding atc_to_io_set.simps by blast

lemma pass_io_set_from_pass_separator :
assumes "is_separator M q1 q2 A t1 t2"
and     "pass_separator_ATC S A s1 t2"
and     "observable M"
and     "observable S"
and     "q1 ∈ states M"
and     "s1 ∈ states S"
and     "(inputs S) = (inputs M)"
shows "pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)"
proof (rule ccontr)
assume "¬ pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)"
then obtain io x y y' where "io@[(x,y)] ∈ (atc_to_io_set (from_FSM M q1) A)" and "io@[(x,y')] ∈ L (from_FSM S s1)" and "io@[(x,y')] ∉ (atc_to_io_set (from_FSM M q1) A)"
unfolding pass_io_set_def by blast

have "is_ATC A"
using separator_is_ATC[OF assms(1,3,5)]  by assumption
then have "acyclic A"
unfolding is_ATC_def by auto
have "observable (from_FSM S s1)"
using from_FSM_observable[OF ‹observable S›] by assumption
have "(inputs A) ⊆ (inputs (from_FSM S s1))"
by (metis (no_types) assms(1) assms(6) assms(7) from_FSM_simps(2) is_separator_simps(16))

obtain y'' where "io @ [(x, y'')] ∈ LS A (initial A)"
using ‹io@[(x,y)] ∈ (atc_to_io_set (from_FSM M q1) A)› unfolding atc_to_io_set.simps by blast

have "pass_ATC (from_FSM S s1) A {t2}"
using ‹pass_separator_ATC S A s1 t2› by auto

then have "io @ [(x, y')] ∈ L A"
using pass_ATC_fail[OF ‹is_ATC A›
‹observable (from_FSM S s1)›
‹(inputs A) ⊆ (inputs (from_FSM S s1))›
‹io @ [(x, y'')] ∈ LS A (initial A)›
‹io@[(x,y')] ∈ L (from_FSM S s1)›,
of "{t2}" ]
by auto

have "io_targets A (io @ [(x, y')]) (initial A) ∩ {t2} = {}"
using pass_ATC_io(2)[OF ‹pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))› ‹io @ [(x, y')] ∈ L A› ‹io@[(x,y')] ∈ L (from_FSM S s1)›]
unfolding fst_conv by blast

then have "io @ [(x, y')] ∈ LS M q1"
using separator_language(1,3,4)[OF assms(1) ‹io @ [(x, y')] ∈ L A›]
by (metis UnE Un_Diff_cancel ‹io @ [(x, y')] ∈ LS A (initial A)› assms(1) disjoint_insert(2) is_separator_sym separator_language(1) singletonI)
then show "False"
using ‹io @ [(x, y')] ∈ L A› ‹io@[(x,y')] ∉ (atc_to_io_set (from_FSM M q1) A)›
unfolding atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›]
by blast
qed

lemma separator_language_last_left :
assumes "is_separator M q1 q2 A t1 t2"
and     "completely_specified M"
and     "q1 ∈ states M"
and     "io @ [(x, y)] ∈ L A"
obtains y'' where "io@[(x,y'')] ∈ L A ∩ LS M q1"
proof -
obtain p t where "path A (initial A) (p@[t])" and "p_io (p@[t]) = io@[(x,y)]"
using language_initial_path_append_transition[OF ‹io @ [(x, y)] ∈ L A›] by blast
then have "¬ deadlock_state A (target (initial A) p)"
have "path A (initial A) p"
using ‹path A (initial A) (p@[t])› by auto

have "p_io p ∈ LS M q1"
using separator_path_targets(1,2,4)[OF assms(1) ‹path A (initial A) p›]
using is_separator_simps(4,5)[OF assms(1)]
using ‹¬ deadlock_state A (target (initial A) p)› by fastforce
then have "io ∈ LS M q1"
using ‹p_io (p@[t]) = io@[(x,y)]› by auto

have "x ∈ (inputs A)"
using ‹io @ [(x, y)] ∈ L A› language_io(1)
by (metis in_set_conv_decomp)
then have "x ∈ (inputs M)"
using is_separator_simps(16)[OF assms(1)] by blast

then obtain y'' where "io@[(x,y'')] ∈ LS M q1"
using completely_specified_language_extension[OF ‹completely_specified M› ‹q1 ∈ states M› ‹io ∈ LS M q1›] by blast
then have "io@[(x,y'')] ∈ L A ∩ LS M q1"
using is_separator_simps(9)[OF assms(1) _ ‹io @ [(x, y)] ∈ L A›] by blast
then show ?thesis
using that by blast
qed

lemma separator_language_last_right :
assumes "is_separator M q1 q2 A t1 t2"
and     "completely_specified M"
and     "q2 ∈ states M"
and     "io @ [(x, y)] ∈ L A"
obtains y'' where "io@[(x,y'')] ∈ L A ∩ LS M q2"
using separator_language_last_left[OF is_separator_sym[OF assms(1)] assms(2,3,4)] by blast

lemma pass_separator_from_pass_io_set :
assumes "is_separator M q1 q2 A t1 t2"
and     "pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)"
and     "observable M"
and     "observable S"
and     "q1 ∈ states M"
and     "s1 ∈ states S"
and     "(inputs S) = (inputs M)"
and     "completely_specified M"
shows "pass_separator_ATC S A s1 t2"
proof (rule ccontr)
assume "¬ pass_separator_ATC S A s1 t2"
then have "¬ pass_ATC (from_FSM S s1) A {t2}" by auto

have "is_ATC A"
using separator_is_ATC[OF assms(1,3,5)]  by assumption
then have "acyclic A"
unfolding is_ATC_def by auto
have "observable (from_FSM S s1)"
using from_FSM_observable[OF ‹observable S›] by assumption
have "(inputs A) ⊆ (inputs (from_FSM S s1))"
using assms(1) assms(6) assms(7) is_separator_simps(16) by fastforce

obtain io x y y' where "io @ [(x,y)] ∈ L A"
"io @ [(x,y')] ∈ L (from_FSM S s1)"
"(io @ [(x,y')] ∉ L A ∨ io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {})"
using pass_ATC_io_fail[OF ‹¬ pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))›]
using separator_initial(2)[OF assms(1)]
using prod.exhaust fst_conv
by (metis empty_iff insert_iff)

show "False"
proof (cases "io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {}")
case True
then have "io @ [(x,y')] ∈ L A"
unfolding io_targets.simps LS.simps by force

have "io @ [(x,y')] ∈ LS M q2 - LS M q1"
proof -
have "t2 ≠ t1"
by (metis (full_types) ‹is_separator M q1 q2 A t1 t2› is_separator_simps(15))
then show ?thesis
using True separator_language[OF assms(1) ‹io @ [(x,y')] ∈ L A›]
by blast
qed
then have "io @ [(x,y')] ∉ LS M q1" by blast

obtain y'' where "io @ [(x, y'')] ∈ LS M q1 ∩ L A"
using separator_language_last_left[OF assms(1,8,5) ‹io @ [(x,y)] ∈ L A›] by blast
then have "io @ [(x, y')] ∈ LS M q1 ∩ LS A (initial A)"
using ‹pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)›
using ‹io @ [(x,y')] ∈ L (from_FSM S s1)›
unfolding pass_io_set_def atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›] by blast

then show "False"
using ‹io @ [(x,y')] ∉ LS M q1› by blast

next
case False
then have "io @ [(x,y')] ∉ L A"
using ‹(io @ [(x,y')] ∉ L A ∨ io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {})›
by blast

obtain y'' where "io @ [(x, y'')] ∈ LS M q1 ∩ L A"
using separator_language_last_left[OF assms(1,8,5) ‹io @ [(x,y)] ∈ L A›] by blast
then have "io @ [(x, y')] ∈ L A"
using ‹pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)›
using ‹io @ [(x,y')] ∈ L (from_FSM S s1)›
unfolding pass_io_set_def atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›] by blast

then show "False"
using ‹io @ [(x,y')] ∉ L A› by blast
qed
qed

lemma pass_separator_pass_io_set_iff:
assumes "is_separator M q1 q2 A t1 t2"
and     "observable M"
and     "observable S"
and     "q1 ∈ states M"
and     "s1 ∈ states S"
and     "(inputs S) = (inputs M)"
and     "completely_specified M"
shows "pass_separator_ATC S A s1 t2 ```