Theory State_Separator

```section ‹State Separators›

text ‹This theory defined state separators.
A state separator @{text "S"} of some pair of states @{text "q1"}, @{text "q2"} of some FSM @{text "M"}
is an acyclic single-input FSM based on the product machine @{text "P"} of @{text "M"} with initial state
@{text "q1"} and @{text "M"} with initial state @{text "q2"} such that every maximal length
sequence in the language of @{text "S"} is either in the language of @{text "q1"} or the
language of @{text "q2"}, but not both.
That is, @{text "C"} represents a strategy of distinguishing @{text "q1"} and @{text "q2"} in
every complete submachine of @{text "P"}.
In testing, separators are used to distinguish states reached in the SUT to establish a lower
bound on the number of distinct states in the SUT.›

theory State_Separator
imports "../Product_FSM" Backwards_Reachability_Analysis
begin

subsection ‹Canonical Separators›

subsubsection ‹Construction›

fun canonical_separator :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a) + 'a,'b,'c) fsm"  where
"canonical_separator M q1 q2 = (canonical_separator' M ((product (from_FSM M q1) (from_FSM M q2))) q1 q2)"

lemma canonical_separator_simps :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "initial (canonical_separator M q1 q2) = Inl (q1,q2)"
"states (canonical_separator M q1 q2)
= (image Inl (states (product (from_FSM M q1) (from_FSM M q2)))) ∪ {Inr q1, Inr q2}"
"inputs (canonical_separator M q1 q2) = inputs M"
"outputs (canonical_separator M q1 q2) = outputs M"
"transitions (canonical_separator M q1 q2)
= shifted_transitions (transitions ((product (from_FSM M q1) (from_FSM M q2))))
∪ distinguishing_transitions (h_out M) q1 q2 (states ((product (from_FSM M q1) (from_FSM M q2)))) (inputs ((product (from_FSM M q1) (from_FSM M q2))))"
proof -
have *: "initial ((product (from_FSM M q1) (from_FSM M q2))) = (q1,q2)"
unfolding restrict_to_reachable_states_simps product_simps using assms by auto
have ***: "inputs ((product (from_FSM M q1) (from_FSM M q2))) = inputs M"
unfolding restrict_to_reachable_states_simps product_simps using assms by auto
have ****: "outputs ((product (from_FSM M q1) (from_FSM M q2))) = outputs M"
unfolding restrict_to_reachable_states_simps product_simps using assms by auto

show "initial (canonical_separator M q1 q2) = Inl (q1,q2)"
"states (canonical_separator M q1 q2) = (image Inl (states (product (from_FSM M q1) (from_FSM M q2)))) ∪ {Inr q1, Inr q2}"
"inputs (canonical_separator M q1 q2) = inputs M"
"outputs (canonical_separator M q1 q2) = outputs M"
"transitions (canonical_separator M q1 q2) = shifted_transitions (transitions ((product (from_FSM M q1) (from_FSM M q2)))) ∪ distinguishing_transitions (h_out M) q1 q2 (states ((product (from_FSM M q1) (from_FSM M q2)))) (inputs ((product (from_FSM M q1) (from_FSM M q2))))"
unfolding canonical_separator.simps canonical_separator'_simps[OF *, of M] *** **** by blast+
qed

lemma distinguishing_transitions_alt_def :
"distinguishing_transitions (h_out M) q1 q2 PS (inputs M) =
{(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2') ∈ PS ∧ (∃ q' . (q1',x,y,q') ∈ transitions M) ∧ ¬(∃ q' . (q2',x,y,q') ∈ transitions M)}
∪ {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2') ∈ PS ∧ ¬(∃ q' . (q1',x,y,q') ∈ transitions M) ∧ (∃ q' . (q2',x,y,q') ∈ transitions M)}"
(is "?dts = ?dl ∪ ?dr")
proof -
have "⋀ t . t ∈ ?dts ⟹ t ∈ ?dl ∨ t ∈ ?dr"
unfolding distinguishing_transitions_def h_out.simps by fastforce
moreover have "⋀ t . t ∈ ?dl ∨ t ∈ ?dr ⟹ t ∈ ?dts"
proof -
fix t assume "t ∈ ?dl ∨ t ∈ ?dr"
then obtain q1' q2' where "t_source t = Inl (q1',q2')" and "(q1',q2') ∈ PS"
by auto

consider (a) "t ∈ ?dl" |
(b) "t ∈ ?dr"
using ‹t ∈ ?dl ∨ t ∈ ?dr› by blast
then show "t ∈ ?dts" proof cases
case a
then have "t_target t = Inr q1" and "(∃ q' . (q1',t_input t,t_output t,q') ∈ transitions M)"
and "¬(∃ q' . (q2',t_input t,t_output t,q') ∈ transitions M)"
using ‹t_source t = Inl (q1',q2')› by force+
then have "t_output t ∈ h_out M (q1',t_input t) - h_out M (q2',t_input t)"
unfolding h_out.simps by blast
then have "t ∈ (λy. (Inl (q1', q2'), t_input t, y, Inr q1)) ` (h_out M (q1', t_input t) - h_out M (q2', t_input t))"
using ‹t_source t = Inl (q1',q2')› ‹t_target t = Inr q1›
by (metis (mono_tags, lifting) imageI surjective_pairing)
moreover have "((q1',q2'),t_input t) ∈ PS × inputs M"
using fsm_transition_input ‹(∃ q' . (q1',t_input t,t_output t,q') ∈ transitions M)›
‹(q1',q2') ∈ PS›
by auto
ultimately show ?thesis
unfolding distinguishing_transitions_def by fastforce
next
case b
then have "t_target t = Inr q2" and "¬(∃ q' . (q1',t_input t,t_output t,q') ∈ transitions M)"
and "(∃ q' . (q2',t_input t,t_output t,q') ∈ transitions M)"
using ‹t_source t = Inl (q1',q2')› by force+
then have "t_output t ∈ h_out M (q2',t_input t) - h_out M (q1',t_input t)"
unfolding h_out.simps by blast
then have "t ∈ (λy. (Inl (q1', q2'), t_input t, y, Inr q2)) ` (h_out M (q2', t_input t) - h_out M (q1', t_input t))"
using ‹t_source t = Inl (q1',q2')› ‹t_target t = Inr q2›
by (metis (mono_tags, lifting) imageI surjective_pairing)
moreover have "((q1',q2'),t_input t) ∈ PS × inputs M"
using fsm_transition_input ‹(∃ q' . (q2',t_input t,t_output t,q') ∈ transitions M)› ‹(q1',q2') ∈ PS›
by auto
ultimately show ?thesis
unfolding distinguishing_transitions_def by fastforce
qed
qed
ultimately show ?thesis by blast
qed

lemma distinguishing_transitions_alt_alt_def :
"distinguishing_transitions (h_out M) q1 q2 PS (inputs M) =
{ t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ PS ∧ t_target t = Inr q1 ∧ (∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}
∪ { t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ PS ∧ t_target t = Inr q2 ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ (∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"

proof -
have "{(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2') ∈ PS ∧ (∃ q' . (q1',x,y,q') ∈ transitions M) ∧ ¬(∃ q' . (q2',x,y,q') ∈ transitions M)}
= { t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ PS ∧ t_target t = Inr q1 ∧ (∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"
by force
moreover have "{(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2') ∈ PS ∧ ¬(∃ q' . (q1',x,y,q') ∈ transitions M) ∧ (∃ q' . (q2',x,y,q') ∈ transitions M)}
= { t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ PS ∧ t_target t = Inr q2 ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ (∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"
by force
ultimately show ?thesis
unfolding distinguishing_transitions_alt_def by force
qed

lemma shifted_transitions_alt_def :
"shifted_transitions ts = {(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2'')) ∈ ts}"
unfolding shifted_transitions_def by force

lemma canonical_separator_transitions_helper :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "transitions (canonical_separator M q1 q2) =
(shifted_transitions  (transitions (product (from_FSM M q1) (from_FSM M q2))))
∪ {(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ (∃ q' . (q1',x,y,q') ∈ transitions M) ∧ ¬(∃ q' . (q2',x,y,q') ∈ transitions M)}
∪ {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ ¬(∃ q' . (q1',x,y,q') ∈ transitions M) ∧ (∃ q' . (q2',x,y,q') ∈ transitions M)}"
unfolding canonical_separator_simps[OF assms]
restrict_to_reachable_states_simps
product_simps from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)]
sup.idem
distinguishing_transitions_alt_def
by blast

definition distinguishing_transitions_left :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"distinguishing_transitions_left M q1 q2  ≡ {(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ (∃ q' . (q1',x,y,q') ∈ transitions M) ∧ ¬(∃ q' . (q2',x,y,q') ∈ transitions M)}"
definition distinguishing_transitions_right :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"distinguishing_transitions_right M q1 q2 ≡ {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ ¬(∃ q' . (q1',x,y,q') ∈ transitions M) ∧ (∃ q' . (q2',x,y,q') ∈ transitions M)}"

definition distinguishing_transitions_left_alt :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"distinguishing_transitions_left_alt M q1 q2  ≡ { t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ t_target t = Inr q1 ∧ (∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"
definition distinguishing_transitions_right_alt :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"distinguishing_transitions_right_alt M q1 q2 ≡ { t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ t_target t = Inr q2 ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ (∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"

definition shifted_transitions_for :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"shifted_transitions_for M q1 q2 ≡ {(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))}"

lemma shifted_transitions_for_alt_def :
"shifted_transitions_for M q1 q2 = {(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2'')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))}"
unfolding shifted_transitions_for_def by auto

lemma distinguishing_transitions_left_alt_alt_def :
"distinguishing_transitions_left M q1 q2 = distinguishing_transitions_left_alt M q1 q2"
proof -
have "⋀ t . t ∈ distinguishing_transitions_left M q1 q2 ⟹ t ∈ distinguishing_transitions_left_alt M q1 q2"
proof -
fix t assume "t ∈ distinguishing_transitions_left M q1 q2"
then obtain q1' q2' x y where "t = (Inl (q1', q2'), x, y, Inr q1)"
"(q1', q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
"(∃q'. (q1', x, y, q') ∈ FSM.transitions M)"
"(∄q'. (q2', x, y, q') ∈ FSM.transitions M)"
unfolding distinguishing_transitions_left_def by blast

have "t_source t = Inl (q1', q2')"
using ‹t = (Inl (q1', q2'), x, y, Inr q1)› by auto
moreover note ‹(q1', q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))›
moreover have "t_target t = Inr q1"
using ‹t = (Inl (q1', q2'), x, y, Inr q1)› by auto
moreover have "(∃t'∈FSM.transitions M. t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹(∃q'. (q1', x, y, q') ∈ FSM.transitions M)› unfolding ‹t = (Inl (q1', q2'), x, y, Inr q1)› by force
moreover have "¬(∃t'∈FSM.transitions M. t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹(∄q'. (q2', x, y, q') ∈ FSM.transitions M)› unfolding ‹t = (Inl (q1', q2'), x, y, Inr q1)› by force
ultimately show "t ∈ distinguishing_transitions_left_alt M q1 q2"
unfolding distinguishing_transitions_left_alt_def by simp
qed
moreover have "⋀ t . t ∈ distinguishing_transitions_left_alt M q1 q2 ⟹ t ∈ distinguishing_transitions_left M q1 q2"
unfolding distinguishing_transitions_left_alt_def distinguishing_transitions_left_def
by fastforce
ultimately show ?thesis by blast
qed

lemma distinguishing_transitions_right_alt_alt_def :
"distinguishing_transitions_right M q1 q2 = distinguishing_transitions_right_alt M q1 q2"
proof -
have "⋀ t . t ∈ distinguishing_transitions_right M q1 q2 ⟹ t ∈ distinguishing_transitions_right_alt M q1 q2"
proof -
fix t assume "t ∈ distinguishing_transitions_right M q1 q2"
then obtain q1' q2' x y where "t = (Inl (q1', q2'), x, y, Inr q2)"
"(q1', q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
"(∄q'. (q1', x, y, q') ∈ FSM.transitions M)"
"(∃q'. (q2', x, y, q') ∈ FSM.transitions M)"
unfolding distinguishing_transitions_right_def by blast

have "t_source t = Inl (q1', q2')"
using ‹t = (Inl (q1', q2'), x, y, Inr q2)› by auto
moreover note ‹(q1', q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))›
moreover have "t_target t = Inr q2"
using ‹t = (Inl (q1', q2'), x, y, Inr q2)› by auto
moreover have "¬(∃t'∈FSM.transitions M. t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹(∄q'. (q1', x, y, q') ∈ FSM.transitions M)› unfolding ‹t = (Inl (q1', q2'), x, y, Inr q2)› by force
moreover have "(∃t'∈FSM.transitions M. t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹(∃q'. (q2', x, y, q') ∈ FSM.transitions M)› unfolding ‹t = (Inl (q1', q2'), x, y, Inr q2)› by force
ultimately show "t ∈ distinguishing_transitions_right_alt M q1 q2"
unfolding distinguishing_transitions_right_def distinguishing_transitions_right_alt_def by simp
qed
moreover have "⋀ t . t ∈ distinguishing_transitions_right_alt M q1 q2 ⟹ t ∈ distinguishing_transitions_right M q1 q2"
unfolding distinguishing_transitions_right_def distinguishing_transitions_right_alt_def by fastforce
ultimately show ?thesis
by blast
qed

lemma canonical_separator_transitions_def :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "transitions (canonical_separator M q1 q2) =
{(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2'')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))}
∪ (distinguishing_transitions_left M q1 q2)
∪ (distinguishing_transitions_right M q1 q2)"
unfolding canonical_separator_transitions_helper[OF assms]
shifted_transitions_alt_def
distinguishing_transitions_left_def
distinguishing_transitions_right_def by simp

lemma canonical_separator_transitions_alt_def :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "transitions (canonical_separator M q1 q2) =
(shifted_transitions_for M q1 q2)
∪ (distinguishing_transitions_left_alt M q1 q2)
∪ (distinguishing_transitions_right_alt M q1 q2)"
proof -
have *: "(shift_Inl `
{t ∈ FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)).
t_source t ∈ reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))})
= {(Inl (t_source t), t_input t, t_output t, Inl (t_target t)) |t.
t ∈ FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) ∧
t_source t ∈ reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))}"
by blast

show ?thesis
unfolding canonical_separator_simps[OF assms]
shifted_transitions_def
restrict_to_reachable_states_simps
product_simps from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)]
sup.idem

distinguishing_transitions_alt_alt_def
shifted_transitions_for_def
*

distinguishing_transitions_left_alt_def
distinguishing_transitions_right_alt_def
by blast
qed

subsubsection ‹State Separators as Submachines of Canonical Separators›

definition is_state_separator_from_canonical_separator :: "(('a × 'a) + 'a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a) + 'a, 'b, 'c) fsm ⇒ bool" where
"is_state_separator_from_canonical_separator CSep q1 q2 S = (
is_submachine S CSep
∧ single_input S
∧ acyclic S
∧ ((Inr q1) ∈ reachable_states S)
∧ ((Inr q2) ∈ reachable_states S)
∧ (∀ q ∈ reachable_states S . (q ≠ Inr q1 ∧ q ≠ Inr q2) ⟶ (isl q ∧ ¬ deadlock_state S q))
∧ (∀ q ∈ reachable_states S . ∀ x ∈ (inputs CSep) . (∃ t ∈ transitions S . t_source t = q ∧ t_input t = x) ⟶ (∀ t' ∈ transitions CSep . t_source t' = q ∧ t_input t' = x ⟶ t' ∈ transitions S))
)"

subsubsection ‹Canonical Separator Properties›

lemma is_state_separator_from_canonical_separator_simps :
assumes "is_state_separator_from_canonical_separator CSep q1 q2 S"
shows "is_submachine S CSep"
and   "single_input S"
and   "acyclic S"
and   "((Inr q1) ∈ reachable_states S)"
and   "((Inr q2) ∈ reachable_states S)"
and   "⋀ q . q ∈ reachable_states S ⟹ q ≠ Inr q1 ⟹ q ≠ Inr q2 ⟹ (isl q ∧ ¬ deadlock_state S q)"
and   "⋀ q x t . q ∈ reachable_states S ⟹ x ∈ (inputs CSep) ⟹ (∃ t ∈ transitions S . t_source t = q ∧ t_input t = x) ⟹ t ∈ transitions CSep ⟹ t_source t = q ⟹ t_input t = x ⟹ t ∈ transitions S"
using assms unfolding is_state_separator_from_canonical_separator_def by blast+

lemma is_state_separator_from_canonical_separator_initial :
assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
and "q1 ∈ states M"
and "q2 ∈ states M"
shows "initial A = Inl (q1,q2)"
using is_state_separator_from_canonical_separator_simps(1)[OF assms(1)]
using canonical_separator_simps(1)[OF assms(2,3)] by auto

lemma path_shift_Inl :
assumes "(image shift_Inl (transitions M)) ⊆ (transitions C)"
and "⋀ t . t ∈ (transitions C) ⟹ isl (t_target t) ⟹ ∃ t' ∈ transitions M . t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t'))"
and "initial C = Inl (initial M)"
and "(inputs C) = (inputs M)"
and "(outputs C) = (outputs M)"
shows "path M (initial M) p = path C (initial C) (map shift_Inl p)"
proof (induction p rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc t p)

have "path M (initial M) (p@[t]) ⟹ path C (initial C) (map shift_Inl (p@[t]))"
proof -
assume "path M (initial M) (p@[t])"
then have "path M (initial M) p" by auto
then have "path C (initial C) (map shift_Inl p)" using snoc.IH
by auto

have "t_source t = target (initial M) p"
using ‹path M (initial M) (p@[t])› by auto
then have "t_source (shift_Inl t) = target (Inl (initial M)) (map shift_Inl p)"
by (cases p rule: rev_cases; auto)
then have "t_source (shift_Inl t) = target (initial C) (map shift_Inl p)"
using assms(3) by auto
moreover have "target (initial C) (map shift_Inl p) ∈ states C"
using path_target_is_state[OF ‹path C (initial C) (map shift_Inl p)›] by assumption
ultimately have "t_source (shift_Inl t) ∈ states C"
by auto
moreover have "t ∈ transitions M"
using ‹path M (initial M) (p@[t])› by auto
ultimately have "(shift_Inl t) ∈ transitions C"
using assms by auto

show "path C (initial C) (map shift_Inl (p@[t]))"
using path_append [OF ‹path C (initial C) (map shift_Inl p)›, of "[shift_Inl t]"]
using ‹(shift_Inl t) ∈ transitions C› ‹t_source (shift_Inl t) = target (initial C) (map shift_Inl p)›
using single_transition_path by force
qed

moreover have "path C (initial C) (map shift_Inl (p@[t])) ⟹ path M (initial M) (p@[t])"
proof -
assume "path C (initial C) (map shift_Inl (p@[t]))"
then have "path C (initial C) (map shift_Inl p)" by auto
then have "path M (initial M) p" using snoc.IH
by blast

have "t_source (shift_Inl t) = target (initial C) (map shift_Inl p)"
using ‹path C (initial C) (map shift_Inl (p@[t]))› by auto
then have "t_source (shift_Inl t) = target (Inl (initial M)) (map shift_Inl p)"
using assms(3) by (cases p rule: rev_cases; auto)
then have "t_source t = target (initial M) p"
by (cases p rule: rev_cases; auto)
moreover have "target (initial M) p ∈ states M"
using path_target_is_state[OF ‹path M (initial M) p›] by assumption
ultimately have "t_source t ∈ states M"
by auto
moreover have "shift_Inl t ∈ transitions C"
using ‹path C (initial C) (map shift_Inl (p@[t]))› by auto
moreover have "isl (t_target (shift_Inl t))"
by auto
ultimately have "t ∈ transitions M" using assms by fastforce

show "path M (initial M) (p@[t])"
using path_append [OF ‹path M (initial M) p›, of "[t]"]
single_transition_path[OF ‹t ∈ transitions M›]
‹t_source t = target (initial M) p› by auto
qed

ultimately show ?case
by linarith
qed

lemma canonical_separator_product_transitions_subset :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "image shift_Inl (transitions (product (from_FSM M q1) (from_FSM M q2))) ⊆ (transitions (canonical_separator M q1 q2))"
unfolding canonical_separator_simps[OF assms] shifted_transitions_def restrict_to_reachable_states_simps
by blast

lemma canonical_separator_transition_targets :
assumes "t ∈ (transitions (canonical_separator M q1 q2))"
and "q1 ∈ states M"
and "q2 ∈ states M"
shows "isl (t_target t) ⟹ t ∈ {(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))}"
and   "t_target t = Inr q1 ⟹ q1 ≠ q2 ⟹ t ∈ (distinguishing_transitions_left_alt M q1 q2)"
and   "t_target t = Inr q2 ⟹ q1 ≠ q2 ⟹ t ∈ (distinguishing_transitions_right_alt M q1 q2)"
and   "isl (t_target t) ∨ t_target t = Inr q1 ∨ t_target t = Inr q2"
unfolding shifted_transitions_for_def
distinguishing_transitions_left_alt_def
distinguishing_transitions_right_alt_def
proof -
let ?shftd = "{(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))}"
let ?dl    = "{ t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ t_target t = Inr q1 ∧ (∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"
let ?dr    = "{ t . ∃ q1' q2' . t_source t = Inl (q1',q2') ∧ (q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2)) ∧ t_target t = Inr q2 ∧ ¬(∃ t'  ∈ transitions M . t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t) ∧ (∃ t'  ∈ transitions M . t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)}"

have "t ∈ ?shftd ∪ ?dl ∪ ?dr"
using assms(1)
unfolding canonical_separator_transitions_alt_def[OF assms(2,3)]
shifted_transitions_for_def
distinguishing_transitions_left_alt_def
distinguishing_transitions_right_alt_def
by force

moreover have p1: "⋀ t' . t' ∈ ?shftd ⟹ isl (t_target t')"
and  p2: "⋀ t' . t' ∈ ?dl ⟹ t_target t' = Inr q1"
and  p3: "⋀ t' . t' ∈ ?dr ⟹ t_target t' = Inr q2"
by auto
ultimately show "isl (t_target t) ∨ t_target t = Inr q1 ∨ t_target t = Inr q2"
by fast

show "isl (t_target t) ⟹ t ∈ ?shftd"
proof -
assume "isl (t_target t)"
then have "t_target t ≠ Inr q1" and "t_target t ≠ Inr q2" by auto
then have "t ∉ ?dl" and "t ∉ ?dr" by force+
then show ?thesis using ‹t ∈ ?shftd ∪ ?dl ∪ ?dr› by fastforce
qed

show "t_target t = Inr q1 ⟹ q1 ≠ q2 ⟹ t ∈ ?dl"
proof -
assume "t_target t = Inr q1" and "q1 ≠ q2"
then have "¬ isl (t_target t)" and "t_target t ≠ Inr q2" by auto
then have "t ∉ ?shftd" and "t ∉ ?dr" by force+
then show ?thesis using ‹t ∈ ?shftd ∪ ?dl ∪ ?dr› by fastforce
qed

show "t_target t = Inr q2 ⟹ q1 ≠ q2 ⟹ t ∈ ?dr"
proof -
assume "t_target t = Inr q2" and "q1 ≠ q2"
then have "¬ isl (t_target t)" and "t_target t ≠ Inr q1"  by auto
then have "t ∉ ?shftd" and "t ∉ ?dl" by force+
then show ?thesis using ‹t ∈ ?shftd ∪ ?dl ∪ ?dr› by fastforce
qed
qed

lemma canonical_separator_path_shift :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) p
= path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) (map shift_Inl p)"
proof -
let ?C = "(canonical_separator M q1 q2)"
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
let ?PR = "(product (from_FSM M q1) (from_FSM M q2))"

have "(inputs ?C) = (inputs ?P)"
and  "(outputs ?C) = (outputs ?P)"
unfolding canonical_separator_simps(3,4)[OF assms] using assms by auto

have p1: "shift_Inl `
FSM.transitions
((Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)))
⊆ FSM.transitions (canonical_separator M q1 q2)"
using canonical_separator_product_transitions_subset[OF assms]
unfolding restrict_to_reachable_states_simps by assumption

have p2: "(⋀t. t ∈ FSM.transitions (canonical_separator M q1 q2) ⟹
isl (t_target t) ⟹
∃t'∈FSM.transitions
((Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))).
t = shift_Inl t')"
using canonical_separator_transition_targets(1)[OF _ assms] unfolding restrict_to_reachable_states_simps by fastforce

have "path ?PR (initial ?PR) p = path ?C (initial ?C) (map shift_Inl p)"
using path_shift_Inl[of ?PR ?C, OF p1 p2]
unfolding restrict_to_reachable_states_simps canonical_separator_simps(1,2,3,4)[OF assms] using assms by auto
moreover have "path ?P (initial ?P) p = path ?PR (initial ?PR) p"
unfolding restrict_to_reachable_states_simps
restrict_to_reachable_states_path[OF reachable_states_initial]
by simp
ultimately show ?thesis
by simp
qed

lemma canonical_separator_t_source_isl :
assumes "t ∈ (transitions (canonical_separator M q1 q2))"
and "q1 ∈ states M" and "q2 ∈ states M"
shows "isl (t_source t)"
using assms(1)
unfolding canonical_separator_transitions_alt_def[OF assms(2,3)]
shifted_transitions_for_def
distinguishing_transitions_left_alt_def
distinguishing_transitions_right_alt_def
by force

lemma canonical_separator_path_from_shift :
assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p"
and "isl (target (initial (canonical_separator M q1 q2)) p)"
and "q1 ∈ states M" and "q2 ∈ states M"
shows "∃ p' . path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) p'
∧ p = (map shift_Inl p')"
using assms(1,2) proof (induction p rule: rev_induct)
case Nil
show ?case using canonical_separator_path_shift[OF assms(3,4), of "[]"] by fast
next
case (snoc t p)
then have "isl (t_target t)" by auto

let ?C = "(canonical_separator M q1 q2)"
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"

have "t ∈ transitions ?C" and "t_source t = target (initial ?C) p"
using snoc.prems by auto
then have "isl (t_source t)"
using canonical_separator_t_source_isl[of t M q1 q2, OF _ assms(3,4)] by blast
then have "isl (target (initial (canonical_separator M q1 q2)) p)"
using ‹t_source t = target (initial ?C) p› by auto

have "path ?C (initial ?C) p" using snoc.prems by auto
then obtain p' where "path ?P (initial ?P) p'"
and "p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'"
using snoc.IH[OF _ ‹isl (target (initial (canonical_separator M q1 q2)) p)›] by blast
then have "target (initial ?C) p = Inl (target (initial ?P) p')"
proof (cases p rule: rev_cases)
case Nil
then show ?thesis
unfolding target.simps visited_states.simps using ‹p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'› canonical_separator_simps(1)[OF assms(3,4)]
next
case (snoc ys y)
then show ?thesis
unfolding target.simps visited_states.simps using ‹p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'› by (cases p' rule: rev_cases; auto)
qed

obtain t' where "t' ∈ transitions ?P"
and "t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t'))"
using canonical_separator_transition_targets(1)[OF ‹t ∈ transitions ?C› assms(3,4) ‹isl (t_target t)›]
by blast

have "path ?P (initial ?P) (p'@[t'])"
by (metis ‹path (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) p'›
‹t = shift_Inl t'› ‹t' ∈ FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))›
‹t_source t = target (FSM.initial (canonical_separator M q1 q2)) p›
‹target (FSM.initial (canonical_separator M q1 q2)) p = Inl (target (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) p')›
fst_conv path_append_transition sum.inject(1))
moreover have "p@[t] = map shift_Inl (p'@[t'])"
using ‹p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'›
‹t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t'))›
by auto
ultimately show ?case
by meson
qed

lemma shifted_transitions_targets :
assumes "t ∈ (shifted_transitions ts)"
shows "isl (t_target t)"
using assms unfolding shifted_transitions_def by force

lemma distinguishing_transitions_left_sources_targets :
assumes "t ∈ (distinguishing_transitions_left_alt M q1 q2)"
and "q2 ∈ states M"
obtains q1' q2' t' where "t_source t = Inl (q1',q2')"
"q1' ∈ states M"
"q2' ∈ states M"
"t' ∈ transitions M"
"t_source t' = q1'"
"t_input t' = t_input t"
"t_output t' = t_output t"
"¬ (∃t''∈ transitions M. t_source t'' = q2' ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t)"
"t_target t = Inr q1"
using assms(1) assms(2) fsm_transition_source path_target_is_state
unfolding distinguishing_transitions_left_alt_def
by fastforce

lemma distinguishing_transitions_right_sources_targets :
assumes "t ∈ (distinguishing_transitions_right_alt M q1 q2)"
and "q1 ∈ states M"
obtains q1' q2' t' where "t_source t = Inl (q1',q2')"
"q1' ∈ states M"
"q2' ∈ states M"
"t' ∈ transitions M"
"t_source t' = q2'"
"t_input t' = t_input t"
"t_output t' = t_output t"
"¬ (∃t''∈ transitions M. t_source t'' = q1' ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t)"
"t_target t = Inr q2"
using assms(1) assms(2) fsm_transition_source path_target_is_state
unfolding distinguishing_transitions_right_alt_def
by fastforce

lemma product_from_transition_split :
assumes "t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows   "(∃t'∈ transitions M. t_source t' = fst (t_source t) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
and     "(∃t'∈ transitions M. t_source t' = snd (t_source t) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using product_transition_split_ob[OF assms(1)]
unfolding product_transitions_alt_def from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by blast+

lemma shifted_transitions_underlying_transition :
assumes "tS ∈ shifted_transitions_for M q1 q2"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
obtains t where "tS = (Inl (t_source t), t_input t, t_output t, Inl (t_target t))"
and   "t ∈ (transitions ((product (from_FSM M q1) (from_FSM M q2))))"
and   "(∃t'∈(transitions M).
t_source t' = fst (t_source t) ∧
t_input t' = t_input t ∧ t_output t' = t_output t)"
and   "(∃t'∈(transitions M).
t_source t' = snd (t_source t) ∧
t_input t' = t_input t ∧ t_output t' = t_output t)"
proof -
obtain t where "tS = (Inl (t_source t), t_input t, t_output t, Inl (t_target t))"
and   *: "t ∈ (transitions ((product (from_FSM M q1) (from_FSM M q2))))"
using assms unfolding shifted_transitions_for_def shifted_transitions_def restrict_to_reachable_states_simps by blast
moreover have "(∃t'∈(transitions M).
t_source t' = fst (t_source t) ∧
t_input t' = t_input t ∧ t_output t' = t_output t)"
using product_from_transition_split(1)[OF _ assms(2,3)]
*
unfolding restrict_to_reachable_states_simps by blast
moreover have "(∃t'∈(transitions M).
t_source t' = snd (t_source t) ∧
t_input t' = t_input t ∧ t_output t' = t_output t)"
using product_from_transition_split(2)[OF _ assms(2,3)]
*
unfolding restrict_to_reachable_states_simps by blast
ultimately show ?thesis
using that by blast
qed

lemma shifted_transitions_observable_against_distinguishing_transitions_left :
assumes "t1 ∈ (shifted_transitions_for M q1 q2)"
and     "t2 ∈ (distinguishing_transitions_left M q1 q2)"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "¬ (t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2)"
using assms(1,2)
unfolding product_transitions_def from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)]
shifted_transitions_for_def distinguishing_transitions_left_def
by force

lemma shifted_transitions_observable_against_distinguishing_transitions_right :
assumes "t1 ∈ (shifted_transitions_for M q1 q2)"
and     "t2 ∈ (distinguishing_transitions_right M q1 q2)"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "¬ (t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2)"
using assms
unfolding product_transitions_def from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)]
shifted_transitions_for_def distinguishing_transitions_right_def
by force

lemma distinguishing_transitions_left_observable_against_distinguishing_transitions_right :
assumes "t1 ∈ (distinguishing_transitions_left M q1 q2)"
and     "t2 ∈ (distinguishing_transitions_right M q1 q2)"
shows "¬ (t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2)"
using assms
unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by force

lemma distinguishing_transitions_left_observable_against_distinguishing_transitions_left :
assumes "t1 ∈ (distinguishing_transitions_left M q1 q2)"
and     "t2 ∈ (distinguishing_transitions_left M q1 q2)"
and     "t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2"
shows "t1 = t2"
using assms unfolding distinguishing_transitions_left_def by force

lemma distinguishing_transitions_right_observable_against_distinguishing_transitions_right :
assumes "t1 ∈ (distinguishing_transitions_right M q1 q2)"
and     "t2 ∈ (distinguishing_transitions_right M q1 q2)"
and     "t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2"
shows "t1 = t2"
using assms unfolding distinguishing_transitions_right_def by force

lemma shifted_transitions_observable_against_shifted_transitions :
assumes "t1 ∈ (shifted_transitions_for M q1 q2)"
and     "t2 ∈ (shifted_transitions_for M q1 q2)"
and     "observable M"
and     "t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2"
shows "t1 = t2"
proof -
obtain t1' where d1: "t1 = (Inl (t_source t1'), t_input t1', t_output t1', Inl (t_target t1'))"
and   h1: "t1' ∈ (transitions (product (from_FSM M q1) (from_FSM M q2)))"
using assms(1) unfolding shifted_transitions_for_def by auto

obtain t2' where d2: "t2 = (Inl (t_source t2'), t_input t2', t_output t2', Inl (t_target t2'))"
and   h2: "t2' ∈ (transitions (product (from_FSM M q1) (from_FSM M q2)))"
using assms(2) unfolding shifted_transitions_for_def by auto

have "observable (product (from_FSM M q1) (from_FSM M q2))"
using from_FSM_observable[OF assms(3)]
product_observable
by metis

then have "t1' = t2'"
using d1 d2 h1 h2 ‹t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2›
by (metis fst_conv observable.elims(2) prod.expand snd_conv sum.inject(1))
then show ?thesis using d1 d2 by auto
qed

lemma canonical_separator_observable :
assumes "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "observable (canonical_separator M q1 q2)" (is "observable ?CSep")
proof -

have  "⋀ t1 t2 . t1 ∈ (transitions ?CSep) ⟹
t2 ∈ (transitions ?CSep) ⟹
t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2 ⟹ t_target t1 = t_target t2"
proof -
fix t1 t2 assume "t1 ∈ (transitions ?CSep)"
and    "t2 ∈ (transitions ?CSep)"
and    *: "t_source t1 = t_source t2 ∧ t_input t1 = t_input t2 ∧ t_output t1 = t_output t2"

moreover have "transitions ?CSep = shifted_transitions_for M q1 q2 ∪
distinguishing_transitions_left M q1 q2 ∪
distinguishing_transitions_right M q1 q2"
using canonical_separator_transitions_alt_def[OF assms(2,3)]
unfolding distinguishing_transitions_left_alt_alt_def distinguishing_transitions_right_alt_alt_def by assumption

ultimately consider "t1 ∈ shifted_transitions_for M q1 q2 ∧ t2 ∈ shifted_transitions_for M q1 q2"
| "t1 ∈ shifted_transitions_for M q1 q2 ∧ t2 ∈ distinguishing_transitions_left M q1 q2"
| "t1 ∈ shifted_transitions_for M q1 q2 ∧ t2 ∈ distinguishing_transitions_right M q1 q2"
| "t1 ∈ distinguishing_transitions_left M q1 q2 ∧ t2 ∈ shifted_transitions_for M q1 q2"
| "t1 ∈ distinguishing_transitions_left M q1 q2 ∧ t2 ∈ distinguishing_transitions_left M q1 q2"
| "t1 ∈ distinguishing_transitions_left M q1 q2 ∧ t2 ∈ distinguishing_transitions_right M q1 q2"
| "t1 ∈ distinguishing_transitions_right M q1 q2 ∧ t2 ∈ shifted_transitions_for M q1 q2"
| "t1 ∈ distinguishing_transitions_right M q1 q2 ∧ t2 ∈ distinguishing_transitions_left M q1 q2"
| "t1 ∈ distinguishing_transitions_right M q1 q2 ∧ t2 ∈ distinguishing_transitions_right M q1 q2"
by force
then show "t_target t1 = t_target t2" proof cases
case 1
then show ?thesis using shifted_transitions_observable_against_shifted_transitions[of t1 M q1 q2 t2, OF _ _ assms(1) *] by fastforce
next
case 2
then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_left[OF _ _ assms(2,3), of t1 t2] * by fastforce
next
case 3
then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_right[OF _ _ assms(2,3), of t1 t2] * by fastforce
next
case 4
then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_left[OF _ _ assms(2,3), of t2 t1] * by fastforce
next
case 5
then show ?thesis using * unfolding distinguishing_transitions_left_def by fastforce
next
case 6
then show ?thesis using * unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by fastforce
next
case 7
then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_right[OF _ _ assms(2,3), of t2 t1] * by fastforce
next
case 8
then show ?thesis using * unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by fastforce
next
case 9
then show ?thesis using * unfolding distinguishing_transitions_right_def by fastforce
qed
qed
then show ?thesis unfolding observable.simps by blast
qed

lemma canonical_separator_targets_ineq :
assumes "t ∈ transitions (canonical_separator M q1 q2)"
and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
shows "isl (t_target t) ⟹ t ∈ (shifted_transitions_for M q1 q2)"
and "t_target t = Inr q1 ⟹ t ∈ (distinguishing_transitions_left M q1 q2)"
and "t_target t = Inr q2 ⟹ t ∈ (distinguishing_transitions_right M q1 q2)"
proof -
show "isl (t_target t) ⟹ t ∈ (shifted_transitions_for M q1 q2)"
by (metis (no_types, lifting) assms(1) assms(2) assms(3) canonical_separator_transition_targets(1) shifted_transitions_for_def)
show "t_target t = Inr q1 ⟹ t ∈ (distinguishing_transitions_left M q1 q2)"
by (metis assms(1) assms(2) assms(3) assms(4) canonical_separator_transition_targets(2) distinguishing_transitions_left_alt_alt_def)
show "t_target t = Inr q2 ⟹ t ∈ (distinguishing_transitions_right M q1 q2)"
by (metis assms(1) assms(2) assms(3) assms(4) canonical_separator_transition_targets(3) distinguishing_transitions_right_alt_alt_def)
qed

lemma canonical_separator_targets_observable :
assumes "t ∈ transitions (canonical_separator M q1 q2)"
and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
shows "isl (t_target t) ⟹ t ∈ (shifted_transitions_for M q1 q2)"
and "t_target t = Inr q1 ⟹ t ∈ (distinguishing_transitions_left M q1 q2)"
and "t_target t = Inr q2 ⟹ t ∈ (distinguishing_transitions_right M q1 q2)"
proof -
show "isl (t_target t) ⟹ t ∈ (shifted_transitions_for M q1 q2)"
by (metis assms canonical_separator_targets_ineq(1))
show "t_target t = Inr q1 ⟹ t ∈ (distinguishing_transitions_left M q1 q2)"
by (metis assms canonical_separator_targets_ineq(2))
show "t_target t = Inr q2 ⟹ t ∈ (distinguishing_transitions_right M q1 q2)"
by (metis assms canonical_separator_targets_ineq(3))
qed

lemma canonical_separator_maximal_path_distinguishes_left :
assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S" (is "is_state_separator_from_canonical_separator ?C q1 q2 S")
and "path S (initial S) p"
and "target (initial S) p = Inr q1"
and "observable M"
and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
shows "p_io p ∈ LS M q1 - LS M q2"
proof (cases p rule: rev_cases)
case Nil
then have "initial S = Inr q1" using assms(3) by auto
then have "initial ?C = Inr q1"
using assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial by fastforce
then show ?thesis using canonical_separator_simps(1) Inr_Inl_False
using assms(5) assms(6) by fastforce
next
case (snoc p' t)
then have "path S (initial S) (p'@[t])"
using assms(2) by auto
then have "t ∈ transitions S" and "t_source t = target (initial S) p'" by auto

have "path ?C (initial ?C) (p'@[t])"
using ‹path S (initial S) (p'@[t])› assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by (meson submachine_path_initial)
then have "path ?C (initial ?C) (p')" and "t ∈ transitions ?C"
by auto

have "isl (target (initial S) p')"
proof (rule ccontr)
assume "¬ isl (target (initial S) p')"
moreover have "target (initial S) p' ∈ states S"
using ‹path S (initial S) (p'@[t])› by auto
ultimately have "target (initial S) p' = Inr q1 ∨ target (initial S) p' = Inr q2"
using ‹t ∈ FSM.transitions (canonical_separator M q1 q2)› ‹t_source t = target (FSM.initial S) p'› assms(5) assms(6) canonical_separator_t_source_isl by fastforce
using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by presburger+
ultimately show "False"
using ‹t ∈ transitions S› ‹t_source t = target (initial S) p'› unfolding deadlock_state.simps
by metis
qed
then obtain q1' q2' where "target (initial S) p' = Inl (q1',q2')" using isl_def prod.collapse by metis
then have "isl (target (initial ?C) p')"
using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S]
by (metis (no_types, lifting) Nil_is_append_conv assms(2) isl_def list.distinct(1) list.sel(1) path.cases snoc submachine_path_initial)

obtain pC where "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) pC"
and "p' = map shift_Inl pC"
by (metis (mono_tags, lifting) ‹isl (target (FSM.initial (canonical_separator M q1 q2)) p')›
‹path (canonical_separator M q1 q2) (FSM.initial (canonical_separator M q1 q2)) p'›
assms(5) assms(6) canonical_separator_path_from_shift)
then have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) pC"
then have "path (from_FSM M q1) q1 (left_path pC)" and "path (from_FSM M q2) q2 (right_path pC)"
using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 pC] by presburger+

have "path M q1 (left_path pC)"
using from_FSM_path[OF assms(5) ‹path (from_FSM M q1) q1 (left_path pC)›] by assumption
have "path M q2 (right_path pC)"
using from_FSM_path[OF assms(6) ‹path (from_FSM M q2) q2 (right_path pC)›] by assumption

have "t_target t = Inr q1"
using ‹path S (initial S) (p'@[t])› snoc assms(3) by auto
then have "t ∈ (distinguishing_transitions_left M q1 q2)"
using canonical_separator_targets_ineq(2)[OF ‹t ∈ transitions ?C› assms(5,6,7)] by auto
then have "t ∈ (distinguishing_transitions_left_alt M q1 q2)"
using distinguishing_transitions_left_alt_alt_def by force

have "t_source t = Inl (q1',q2')"
using ‹target (initial S) p' = Inl (q1',q2')› ‹t_source t = target (initial S) p'› by auto

then obtain t' where "q1' ∈ states M"
and "q2' ∈ states M"
and "t' ∈ transitions M"
and "t_source t' = q1'"
and "t_input t' = t_input t"
and "t_output t' = t_output t"
and "¬ (∃t''∈ transitions M. t_source t'' = q2' ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t)"
using ‹t ∈ (distinguishing_transitions_left_alt M q1 q2)› assms(5,6) fsm_transition_source path_target_is_state
unfolding distinguishing_transitions_left_alt_def reachable_states_def by fastforce

have "initial S = Inl (q1,q2)"
by (meson assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial)
have "length p' = length pC"
using ‹p' = map shift_Inl pC› by auto
then have "target (initial S) p' = Inl (target (q1,q2) pC)"
using ‹p' = map shift_Inl pC› ‹initial S = Inl (q1,q2)› by (induction p' pC rule: list_induct2; auto)
then have "target (q1,q2) pC = (q1',q2')"
using ‹target (initial S) p' = Inl (q1',q2')› by auto
then have "target q2 (right_path pC) = q2'"
using product_target_split(2) by fastforce
then have "¬ (∃t'∈ transitions M. t_source t' = target q2 (right_path pC) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹¬ (∃t'∈ transitions M. t_source t' = q2' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)› by blast

have "target q1 (left_path pC) = q1'"
using ‹target (q1,q2) pC = (q1',q2')› product_target_split(1) by fastforce
then have "path M q1 ((left_path pC)@[t'])"
using ‹path M q1 (left_path pC)› ‹t' ∈ transitions M› ‹t_source t' = q1'›
then have "p_io ((left_path pC)@[t']) ∈ LS M q1"
unfolding LS.simps by force
moreover have "p_io p' = p_io (left_path pC)"
using ‹p' = map shift_Inl pC› by auto
ultimately have "p_io (p'@[t]) ∈ LS M q1"
using ‹t_input t' = t_input t› ‹t_output t' = t_output t› by auto

have "p_io (right_path pC) @  [(t_input t, t_output t)] ∉ LS M q2"
using observable_path_language_step[OF assms(4) ‹path M q2 (right_path pC)› ‹¬ (∃t'∈ transitions M. t_source t' = target q2 (right_path pC) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)›] by assumption
moreover have "p_io p' = p_io (right_path pC)"
using ‹p' = map shift_Inl pC› by auto
ultimately have "p_io (p'@[t]) ∉ LS M q2"
by auto

show ?thesis
using ‹p_io (p'@[t]) ∈ LS M q1› ‹p_io (p'@[t]) ∉ LS M q2› snoc by blast
qed

lemma canonical_separator_maximal_path_distinguishes_right :
assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S"
(is "is_state_separator_from_canonical_separator ?C q1 q2 S")
and "path S (initial S) p"
and "target (initial S) p = Inr q2"
and "observable M"
and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
shows "p_io p ∈ LS M q2 - LS M q1"
proof (cases p rule: rev_cases)
case Nil
then have "initial S = Inr q2" using assms(3) by auto
then have "initial ?C = Inr q2"
using assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial by fastforce
then show ?thesis using canonical_separator_simps(1) Inr_Inl_False
using assms(5) assms(6) by fastforce
next
case (snoc p' t)
then have "path S (initial S) (p'@[t])"
using assms(2) by auto
then have "t ∈ transitions S" and "t_source t = target (initial S) p'"
by auto

have "path ?C (initial ?C) (p'@[t])"
using ‹path S (initial S) (p'@[t])› assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S]
by (meson submachine_path_initial)
then have "path ?C (initial ?C) (p')" and "t ∈ transitions ?C"
by auto

have "isl (target (initial S) p')"
proof (rule ccontr)
assume "¬ isl (target (initial S) p')"
moreover have "target (initial S) p' ∈ states S"
using ‹path S (initial S) (p'@[t])› by auto
ultimately have "target (initial S) p' = Inr q1 ∨ target (initial S) p' = Inr q2"

using assms(1) unfolding is_state_separator_from_canonical_separator_def
by (metis ‹t ∈ FSM.transitions (canonical_separator M q1 q2)› ‹t_source t = target (FSM.initial S) p'›
assms(5) assms(6) canonical_separator_t_source_isl)
using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by presburger+
ultimately show "False"
using ‹t ∈ transitions S› ‹t_source t = target (initial S) p'› unfolding deadlock_state.simps
by metis
qed
then obtain q1' q2' where "target (initial S) p' = Inl (q1',q2')"
using isl_def prod.collapse by metis
then have "isl (target (initial ?C) p')"
using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S]
by (metis (no_types, lifting) Nil_is_append_conv assms(2) isl_def list.distinct(1) list.sel(1)
path.cases snoc submachine_path_initial)

obtain pC where "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) pC"
and "p' = map shift_Inl pC"
using canonical_separator_path_from_shift[OF ‹path ?C (initial ?C) (p')› ‹isl (target (initial ?C) p')›]
using assms(5) assms(6) by blast
then have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) pC"

then have "path (from_FSM M q1) q1 (left_path pC)" and "path (from_FSM M q2) q2 (right_path pC)"
using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 pC] by presburger+

have "path M q1 (left_path pC)"
using from_FSM_path[OF assms(5) ‹path (from_FSM M q1) q1 (left_path pC)›] by assumption
have "path M q2 (right_path pC)"
using from_FSM_path[OF assms(6) ‹path (from_FSM M q2) q2 (right_path pC)›] by assumption

have "t_target t = Inr q2"
using ‹path S (initial S) (p'@[t])› snoc assms(3) by auto
then have "t ∈ (distinguishing_transitions_right M q1 q2)"
using canonical_separator_targets_ineq(3)[OF ‹t ∈ transitions ?C› assms(5,6,7)] by auto
then have "t ∈ (distinguishing_transitions_right_alt M q1 q2)"
unfolding distinguishing_transitions_right_alt_alt_def by assumption

have "t_source t = Inl (q1',q2')"
using ‹target (initial S) p' = Inl (q1',q2')› ‹t_source t = target (initial S) p'› by auto

then obtain t' where "q1' ∈ states M"
and "q2' ∈ states M"
and "t' ∈ transitions M"
and "t_source t' = q2'"
and "t_input t' = t_input t"
and "t_output t' = t_output t"
and "¬ (∃t''∈ transitions M. t_source t'' = q1' ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t)"
using ‹t ∈ (distinguishing_transitions_right_alt M q1 q2)› assms(5,6) fsm_transition_source path_target_is_state
unfolding distinguishing_transitions_right_alt_def reachable_states_def by fastforce

have "initial S = Inl (q1,q2)"
by (meson assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial)
have "length p' = length pC"
using ‹p' = map shift_Inl pC› by auto
then have "target (initial S) p' = Inl (target (q1,q2) pC)"
using ‹p' = map shift_Inl pC› ‹initial S = Inl (q1,q2)› by (induction p' pC rule: list_induct2; auto)
then have "target (q1,q2) pC = (q1',q2')"
using ‹target (initial S) p' = Inl (q1',q2')› by auto
then have "target q1 (left_path pC) = q1'"
using product_target_split(1) by fastforce
then have "¬ (∃t'∈ transitions M. t_source t' = target q1 (left_path pC) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)"
using ‹¬ (∃t'∈ transitions M. t_source t' = q1' ∧ t_input t' = t_input t ∧ t_output t' = t_output t)› by blast

have "target q2 (right_path pC) = q2'"
using ‹target (q1,q2) pC = (q1',q2')› product_target_split(2) by fastforce
then have "path M q2 ((right_path pC)@[t'])"
using ‹path M q2 (right_path pC)› ‹t' ∈ transitions M› ‹t_source t' = q2'›
then have "p_io ((right_path pC)@[t']) ∈ LS M q2"
unfolding LS.simps by force
moreover have "p_io p' = p_io (right_path pC)"
using ‹p' = map shift_Inl pC› by auto
ultimately have "p_io (p'@[t]) ∈ LS M q2"
using ‹t_input t' = t_input t› ‹t_output t' = t_output t› by auto

have "p_io (left_path pC) @  [(t_input t, t_output t)] ∉ LS M q1"
using observable_path_language_step[OF assms(4) ‹path M q1 (left_path pC)› ‹¬ (∃t'∈ transitions M. t_source t' = target q1 (left_path pC) ∧ t_input t' = t_input t ∧ t_output t' = t_output t)›] by assumption
moreover have "p_io p' = p_io (left_path pC)"
using ‹p' = map shift_Inl pC› by auto
ultimately have "p_io (p'@[t]) ∉ LS M q1"
by auto

show ?thesis
using ‹p_io (p'@[t]) ∈ LS M q2› ‹p_io (p'@[t]) ∉ LS M q1› snoc
by blast
qed

lemma state_separator_from_canonical_separator_observable :
assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
and     "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "observable A"
using submachine_observable[OF _ canonical_separator_observable[OF assms(2,3,4)]]
using assms(1) unfolding is_state_separator_from_canonical_separator_def
by metis

lemma canonical_separator_initial :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "initial (canonical_separator M q1 q2) = Inl (q1,q2)"
unfolding canonical_separator_simps[OF assms] by simp

lemma canonical_separator_states :
assumes "Inl (s1,s2) ∈ states (canonical_separator M q1 q2)"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "(s1,s2) ∈ states (product (from_FSM M q1) (from_FSM M q2))"
using assms(1) reachable_state_is_state
unfolding canonical_separator_simps[OF assms(2,3)] by fastforce

lemma canonical_separator_transition :
assumes "t ∈ transitions (canonical_separator M q1 q2)" (is "t ∈ transitions ?C")
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "t_source t = Inl (s1,s2)"
and     "observable M"
and     "q1 ≠ q2"
shows "⋀ s1' s2' . t_target t = Inl (s1',s2') ⟹ (s1, t_input t, t_output t, s1') ∈ transitions M ∧ (s2, t_input t, t_output t, s2') ∈ transitions M "
and   "t_target t = Inr q1 ⟹ (∃ t'∈ transitions M . t_source t' = s1 ∧ t_input t' = t_input t ∧ t_output t' = t_output t)
∧ (¬(∃ t'∈ transitions M . t_source t' = s2 ∧ t_input t' = t_input t ∧ t_output t' = t_output t))"
and   "t_target t = Inr q2 ⟹ (∃ t'∈ transitions M . t_source t' = s2 ∧ t_input t' = t_input t ∧ t_output t' = t_output t)
∧ (¬(∃ t'∈ transitions M . t_source t' = s1 ∧ t_input t' = t_input t ∧ t_output t' = t_output t))"
and   "(∃ s1' s2' . t_target t = Inl (s1',s2')) ∨ t_target t = Inr q1 ∨ t_target t = Inr q2"
proof -
show "⋀ s1' s2' . t_target t = Inl (s1',s2') ⟹ (s1, t_input t, t_output t, s1') ∈ transitions M ∧ (s2, t_input t, t_output t, s2') ∈ transitions M"
using canonical_separator_transition_targets(1)[OF assms(1,2,3)] assms(4)
unfolding shifted_transitions_for_def[symmetric]
unfolding shifted_transitions_for_alt_def
unfolding product_transitions_def from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by fastforce

show "t_target t = Inr q1 ⟹ (∃ t'∈ transitions M . t_source t' = s1 ∧ t_input t' = t_input t ∧ t_output t' = t_output t)
∧ (¬(∃ t'∈ transitions M . t_source t' = s2 ∧ t_input t' = t_input t ∧ t_output t' = t_output t))"
using canonical_separator_targets_observable(2)[OF assms(1,2,3,6)] assms(4)
unfolding distinguishing_transitions_left_def by fastforce

show "t_target t = Inr q2 ⟹ (∃ t'∈ transitions M . t_source t' = s2 ∧ t_input t' = t_input t ∧ t_output t' = t_output t)
∧ (¬(∃ t'∈ transitions M . t_source t' = s1 ∧ t_input t' = t_input t ∧ t_output t' = t_output t))"
using canonical_separator_targets_observable(3)[OF assms(1,2,3,6)] assms(4)
unfolding distinguishing_transitions_right_def by fastforce

show "(∃ s1' s2' . t_target t = Inl (s1',s2')) ∨ t_target t = Inr q1 ∨ t_target t = Inr q2"
using canonical_separator_transition_targets(4)[OF assms(1,2,3)]
qed

lemma canonical_separator_transition_source :
assumes "t ∈ transitions (canonical_separator M q1 q2)" (is "t ∈ transitions ?C")
and     "q1 ∈ states M"
and     "q2 ∈ states M"
obtains q1' q2' where "t_source t = Inl (q1',q2')"
"(q1',q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
proof -
consider "t ∈ shifted_transitions_for M q1 q2" | "t ∈ distinguishing_transitions_left_alt M q1 q2" |
"t ∈ distinguishing_transitions_right_alt M q1 q2"
using assms(1)
unfolding canonical_separator_transitions_alt_def[OF assms(2,3)] by blast
then show ?thesis proof cases
case 1
then show ?thesis unfolding shifted_transitions_for_def using that
using fsm_transition_source by fastforce
next
case 2
then show ?thesis unfolding distinguishing_transitions_left_alt_def using that by fastforce
next
case 3
then show ?thesis unfolding distinguishing_transitions_right_alt_def using that by fastforce
qed
qed

lemma canonical_separator_transition_ex :
assumes "t ∈ transitions (canonical_separator M q1 q2)" (is "t ∈ transitions ?C")
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "t_source t = Inl (s1,s2)"
shows "(∃ t1 ∈ transitions M . t_source t1 = s1 ∧ t_input t1 = t_input t ∧ t_output t1 = t_output t) ∨
(∃ t2 ∈ transitions M . t_source t2 = s2 ∧ t_input t2 = t_input t ∧ t_output t2 = t_output t)"
proof -
consider "t ∈ shifted_transitions_for M q1 q2" | "t ∈ distinguishing_transitions_left_alt M q1 q2" |
"t ∈ distinguishing_transitions_right_alt M q1 q2"
using assms(1)
unfolding canonical_separator_transitions_alt_def[OF assms(2,3)] by blast
then show ?thesis proof cases
case 1
then show ?thesis unfolding shifted_transitions_for_def
using product_from_transition_split[OF _ assms(2,3)]
using assms(4) by force
next
case 2
then show ?thesis unfolding distinguishing_transitions_left_alt_def
using assms(4) by auto

next
case 3
then show ?thesis unfolding distinguishing_transitions_right_alt_def
using assms(4) by auto
qed
qed

lemma canonical_separator_path_split_target_isl :
assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) (p@[t])"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "isl (target (initial (canonical_separator M q1 q2)) p)"
proof -
let ?C = "(canonical_separator M q1 q2)"
have "t ∈ transitions ?C"
using assms by auto
moreover have "¬ deadlock_state ?C (t_source t)"
using assms unfolding deadlock_state.simps by blast
ultimately show ?thesis
using canonical_separator_t_source_isl assms
by fastforce
qed

lemma canonical_separator_path_initial :
assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p" (is "path ?C (initial ?C) p")
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "observable M"
and     "q1 ≠ q2"
shows "⋀ s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2') ⟹ (∃ p1 p2 . path M q1 p1 ∧ path M q2 p2 ∧ p_io p1 = p_io p2 ∧ p_io p1 = p_io p ∧ target q1 p1 = s1' ∧ target q2 p2 = s2')"
and   "target (initial (canonical_separator M q1 q2)) p = Inr q1 ⟹ (∃ p1 p2 t . path M q1 (p1@[t]) ∧ path M q2 p2 ∧ p_io (p1@[t]) = p_io p ∧ p_io p2 = butlast (p_io p)) ∧ (¬(∃ p2 . path M q2 p2 ∧ p_io p2 = p_io p))"
and   "target (initial (canonical_separator M q1 q2)) p = Inr q2 ⟹ (∃ p1 p2 t . path M q1 p1 ∧ path M q2 (p2@[t]) ∧ p_io p1 = butlast (p_io p) ∧ p_io (p2@[t]) = p_io p) ∧ (¬(∃ p1 . path M q1 p1 ∧ p_io p1 = p_io p))"
and   "(∃ s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2')) ∨ target (initial (canonical_separator M q1 q2)) p = Inr q1 ```