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
     deadlock_state S (Inr q1)
     deadlock_state S (Inr q2)
     ((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   "deadlock_state S (Inr q1)"
  and   "deadlock_state S (Inr q2)"
  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)]
      by (simp add: assms(3) assms(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            
    moreover have "deadlock_state S (Inr q1)" and "deadlock_state S (Inr q2)"
      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"
    by (simp add: assms(5) assms(6))
  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'
    by (simp add: path_append_transition)
  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)   
    moreover have "deadlock_state S (Inr q1)" and "deadlock_state S (Inr q2)"
      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"
    by (simp add: assms(5) assms(6))

  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'
    by (simp add: path_append_transition)
  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)]
    by (simp add: isl_def) 
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