Theory R_Distinguishability

section ‹R-Distinguishability›

text ‹This theory defines the notion of r-distinguishability and relates it to state separators.›


theory R_Distinguishability
imports State_Separator
begin


definition r_compatible :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ bool" where 
  "r_compatible M q1 q2 = ((∃ S . completely_specified S ∧ is_submachine S (product (from_FSM M q1) (from_FSM M q2))))"

abbreviation(input) "r_distinguishable M q1 q2 ≡ ¬ r_compatible M q1 q2"

(* Note: If an input is not defined on states q and q', then they are r(0)-distinguishable (r_distinguishable_k M q1 q2 0).
         In particular, any state with some undefined input is r-distinguishable from itself 
         This behaviour is justified by the assumption that tested FSMs are completely specified.
*)

fun r_distinguishable_k :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ bool" where
  "r_distinguishable_k M q1 q2 0 = (∃ x ∈ (inputs M) . ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2))" |
  "r_distinguishable_k M q1 q2 (Suc k) = (r_distinguishable_k M q1 q2 k 
                                          ∨ (∃ x ∈ (inputs M) . ∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k))"



subsection ‹R(k)-Distinguishability Properties›


lemma r_distinguishable_k_0_alt_def : 
  "r_distinguishable_k M q1 q2 0 = (∃ x ∈ (inputs M) . ¬(∃ y q1' q2' . (q1,x,y,q1') ∈ transitions M ∧ (q2,x,y,q2') ∈ transitions M))"
  by fastforce 

lemma r_distinguishable_k_Suc_k_alt_def :
  "r_distinguishable_k M q1 q2 (Suc k) = (r_distinguishable_k M q1 q2 k 
                                          ∨ (∃ x ∈ (inputs M) . ∀ y q1' q2' . ((q1,x,y,q1') ∈ transitions M ∧ (q2,x,y,q2') ∈ transitions M) ⟶ r_distinguishable_k M q1' q2' k))" 
  by fastforce

lemma r_distinguishable_k_by_larger :
  assumes "r_distinguishable_k M q1 q2 k"
      and "k ≤ k'"
    shows "r_distinguishable_k M q1 q2 k'"
  using assms nat_induct_at_least by fastforce


lemma r_distinguishable_k_0_not_completely_specified :
  assumes "r_distinguishable_k M q1 q2 0"
      and "q1 ∈ states M"
      and "q2 ∈ states M"
  shows "¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2)))"
proof -
  let ?F1 = "from_FSM M q1"
  let ?F2 = "from_FSM M q2"
  let ?P = "product ?F1 ?F2"

  obtain x where "x ∈ (inputs M)" 
             and "¬ (∃ t1 t2 . t1 ∈ transitions M ∧ t2 ∈ transitions M ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"  
    using assms(1) by fastforce

  then have *: "¬ (∃ t1 t2 . t1 ∈ transitions ?F1 ∧ t2 ∈ transitions ?F2 ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
    unfolding from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by simp
  
  have **: "¬ (∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x)"
  proof (rule ccontr)  
    assume "¬ ¬ (∃t∈ transitions (product (from_FSM M q1) (from_FSM M q2)). t_source t = (q1, q2) ∧ t_input t = x)"
    then obtain t where "t ∈ transitions ?P" and "t_source t = (q1,q2)" and "t_input t = x"
      by blast 

    have "∃ t1 t2 . t1 ∈ transitions ?F1 ∧ t2 ∈ transitions ?F2 ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
      using product_transition_split[OF ‹t ∈ transitions ?P›]
      by (metis ‹t_input t = x› ‹t_source t = (q1, q2)› fst_conv snd_conv)
    then show "False" 
      using * by auto
  qed

  moreover have "x ∈ (inputs ?P)"
    using ‹x ∈ (inputs M)›
    by (simp add: assms(3)) 

  ultimately have "¬ completely_specified_state ?P (q1,q2)"
    by (meson completely_specified_state.elims(2))
    

  have "(q1,q2) = initial (product (from_FSM M q1) (from_FSM M q2))"
    by (simp add: assms(2) assms(3))

  then show ?thesis
    using ‹¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1, q2)› by presburger
qed



lemma r_0_distinguishable_from_not_completely_specified_initial :
  assumes "¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1,q2)"
      and "q1 ∈ states M"
      and "q2 ∈ states M"
  shows "r_distinguishable_k M q1 q2 0"
proof -
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"

  from assms obtain x where "x ∈ (inputs ?P)"
                      and "¬ (∃t∈ transitions ?P. t_source t = (q1, q2) ∧ t_input t = x)" 
        unfolding completely_specified_state.simps by blast

  then have "x ∈ (inputs M)"
    by (simp add: assms(2) assms(3))

  have *: "¬ (∃ t1 t2.
                t1 ∈ transitions (from_FSM M q1) ∧
                t2 ∈ transitions (from_FSM M q2) ∧
                t_source t1 = q1 ∧
                t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
  proof

    assume "∃t1 t2.
       t1 ∈ transitions (from_FSM M q1) ∧
       t2 ∈ transitions (from_FSM M q2) ∧
       t_source t1 = q1 ∧
       t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
    then obtain t1 t2 where "t1 ∈ transitions (from_FSM M q1)" 
                        and "t2 ∈ transitions (from_FSM M q2)"
                        and "t_source t1 = q1"
                        and "t_source t2 = q2" 
                        and "t_input t1 = x" 
                        and "t_input t2 = x" 
                        and "t_output t1 = t_output t2"
      by blast

    let ?t = "((t_source t1, t_source t2),t_input t1,t_output t1,(t_target t1,t_target t2))"
    let ?t1 = "(fst (t_source ?t), t_input ?t, t_output ?t, fst (t_target ?t))"
    let ?t2 = "(snd (t_source ?t), t_input ?t, t_output ?t, snd (t_target ?t))"

    have t1_alt : "t1 = ?t1"
      by auto
    have "t_source t2 = snd (t_source ?t)"
      by auto
    moreover have "t_input t2 = t_input ?t"
      using ‹t_input t1 = x› ‹t_input t2 = x› by auto
    moreover have "t_output t2 = t_output ?t"
      using ‹t_output t1 = t_output t2› by auto
    moreover have "t_target t2 = snd (t_target ?t)"
      by auto
    ultimately have "(t_source t2, t_input t2, t_output t2, t_target t2) = ?t2"
      by auto
    then have t2_alt : "t2 = ?t2"
      by auto
        
    have "?t1 ∈ transitions (from_FSM M q1)"
      using ‹t1 ∈ transitions (from_FSM M q1)› by auto
    moreover have "?t2 ∈ transitions (from_FSM M q2)"
      using ‹t2 ∈ transitions (from_FSM M q2)› t2_alt by auto

    ultimately have "?t ∈ transitions ?P"
      unfolding product_transitions_def by force
    moreover have "t_source ?t = (q1,q2)" using ‹t_source t1 = q1› ‹t_source t2 = q2› by auto
    moreover have "t_input ?t = x" using ‹t_input t1 = x› by auto
    ultimately show "False"
      using ‹¬ (∃t∈ transitions ?P. t_source t = (q1, q2) ∧ t_input t = x)› by blast
  qed

  have **:  "⋀t1 . t1 ∈ transitions M ⟹ t_source t1 = q1 ⟹ t1 ∈ transitions (from_FSM M q1)"
   and ***: "⋀t2 . t2 ∈ transitions M ⟹ t_source t2 = q2 ⟹ t2 ∈ transitions (from_FSM M q2)"
    by (simp add: assms(2,3))+
    

  then show ?thesis unfolding r_distinguishable_k.simps
    using ‹x ∈ (inputs M)› * by blast
qed          


lemma r_0_distinguishable_from_not_completely_specified :
  assumes "¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1',q2')"
      and "q1 ∈ states M"
      and "q2 ∈ states M"
      and "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
    shows "r_distinguishable_k M q1' q2' 0"
proof -
  have "q1' ∈ states M"
    using assms(2) assms(4) by simp
  have "q2' ∈ states M"
    using assms(3) assms(4) by simp
  show ?thesis
    using r_0_distinguishable_from_not_completely_specified_initial[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M›]
          assms(1)
    unfolding completely_specified_state.simps product_simps from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] from_FSM_simps[OF ‹q1' ∈ states M›] from_FSM_simps[OF ‹q2' ∈ states M›]
              product_transitions_alt_def by auto
qed
               

lemma r_distinguishable_k_intersection_path : 
  assumes "¬ r_distinguishable_k M q1 q2 k"
  and "length xs ≤ Suc k"
  and "set xs ⊆ (inputs M)"
  and "q1 ∈ states M"
  and "q2 ∈ states M"
shows "∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs"
using assms proof (induction k arbitrary: q1 q2 xs)
  case 0
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
  show ?case
  proof (cases "length xs < Suc 0")
    case True
    then have "xs = []" by auto
    moreover have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) []"
      by (simp add: "0.prems"(4) "0.prems"(5) nil)
    moreover have "map fst (p_io []) = []" by auto
    ultimately show ?thesis
      by simp 
  next
    case False
    
    have "completely_specified_state ?P (q1,q2)"
    proof (rule ccontr)
      assume "¬ completely_specified_state ?P (q1,q2)"
      then have "r_distinguishable_k M q1 q2 0"
        using r_0_distinguishable_from_not_completely_specified_initial
        by (metis "0.prems"(4) "0.prems"(5)) 
      then show "False"
        using "0.prems" by simp
    qed
    then have *: "∀ x ∈ (inputs ?P) . ∃ t . t ∈ transitions ?P ∧ t_source t = (q1,q2) ∧ t_input t = x"
      unfolding completely_specified_state.simps by blast

    let ?x = "hd xs"
    have "xs = [?x]"
      using "0.prems"(2) False
      by (metis Suc_length_conv le_neq_implies_less length_0_conv list.sel(1))
    
    have "?x ∈ (inputs M)"
      using "0.prems"(3) False by auto
    then obtain t where "t ∈ transitions ?P" and "t_source t = (q1,q2)" and "t_input t = ?x"
      using "*" "0.prems"(4) "0.prems"(5) by auto

    then have "path ?P (q1,q2) [t]" 
      using single_transition_path by metis
    moreover have "map fst (p_io [t]) = xs"
      using ‹t_input t = ?x› ‹xs = [hd xs]› by auto
    ultimately show ?thesis
      by (metis (no_types, lifting)) 
  qed
next
  case (Suc k)
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
  
  show ?case 
  proof (cases "length xs ≤ Suc k")
    case True
    have "¬ r_distinguishable_k M q1 q2 k" 
      using Suc.prems(1) by auto
    show ?thesis 
      using Suc.IH[OF ‹¬ r_distinguishable_k M q1 q2 k› True Suc.prems(3,4,5)] by assumption
  next
    case False
    then have "length xs = Suc (Suc k)"
      using Suc.prems(2) by auto
    
    then have "hd xs ∈ (inputs M)"
      by (metis Suc.prems(3) contra_subsetD hd_in_set length_greater_0_conv zero_less_Suc) 
    have "set (tl xs) ⊆ (inputs M)"
      by (metis ‹length xs = Suc (Suc k)› Suc.prems(3) dual_order.trans hd_Cons_tl length_0_conv nat.simps(3) set_subset_Cons)
    have "length (tl xs) ≤ Suc k"
      by (simp add: ‹length xs = Suc (Suc k)›) 

    let ?x = "hd xs"
    let ?xs = "tl xs"

    have "∀ x ∈ (inputs M) . ∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x ∧ ¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
    proof 
      fix x assume "x ∈ (inputs M)"
  
      have "¬(∃ x ∈ (inputs M) . ∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k)"
        using Suc.prems by auto
      then have "∀ x ∈ (inputs M) . ∃ t1 t2 . (t1 ∈ transitions M ∧ t2 ∈ transitions M ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ∧ ¬ r_distinguishable_k M (t_target t1) (t_target t2) k)"
        by blast
      then obtain t1 t2 where "t1 ∈ transitions M"
                          and "t2 ∈ transitions M"  
                          and "t_source t1 = q1" 
                          and "t_source t2 = q2"  
                          and "t_input t1 = x" 
                          and "t_input t2 = x" 
                          and p4: "t_output t1 = t_output t2" 
                          and **: "¬ r_distinguishable_k M (t_target t1) (t_target t2) k"
        using ‹x ∈ (inputs M)› by auto

      have p1: "t1 ∈ transitions (from_FSM M q1)"
        by (simp add: Suc.prems(4) ‹t1 ∈ FSM.transitions M›) 
      have p2: "t2 ∈ transitions (from_FSM M q2)"
        by (simp add: Suc.prems(5) ‹t2 ∈ FSM.transitions M›) 
      have p3: "t_input t1 = t_input t2"
        using ‹t_input t1 = x› ‹t_input t2 = x› by auto
      
      have ***: "((q1,q2), x, t_output t1, (t_target t1, t_target t2)) ∈ transitions ?P"
        using ‹t_source t1 = q1› ‹t_source t2 = q2› ‹t_input t1 = x› p1 p2 p3 p4
        unfolding product_transitions_alt_def
        by blast
      
      show "∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x ∧ ¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
        by (metis "**" "***" fst_conv snd_conv)
    qed

    then obtain t where "t ∈ transitions ?P" and "t_source t = (q1,q2)" and "t_input t = ?x" 
                    and "¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
      using ‹?x ∈ (inputs M)› by blast 

    have "fst (t_target t) ∈ FSM.states M" and "snd (t_target t) ∈ FSM.states M"
      using fsm_transition_target[OF ‹t ∈ transitions ?P›] unfolding product_simps from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›] by auto

    then obtain p where p_def: "path (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (t_target t) p" 
               and "map fst (p_io p) = ?xs"
      using Suc.IH[OF ‹¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k› ‹length (tl xs) ≤ Suc k› ‹set (tl xs) ⊆ (inputs M)›] by auto
    
    have "path ?P (t_target t) p" 
      using product_from_path_previous[OF p_def ‹t ∈ transitions ?P› Suc.prems(4,5)]  by assumption

    have "path ?P (q1,q2) (t#p)"
      using path.cons[OF‹t ∈ transitions ?P› ‹path ?P (t_target t) p›] ‹t_source t = (q1,q2)› by metis
    moreover have "map fst (p_io (t#p)) = xs"
      using ‹t_input t = ?x› ‹map fst (p_io p) = ?xs›
      by (metis (no_types, lifting) ‹length xs = Suc (Suc k)› ‹t_input t = hd xs› fst_conv hd_Cons_tl length_greater_0_conv list.simps(9) zero_less_Suc)
    ultimately show ?thesis
      by (metis (no_types, lifting)) 
  qed
qed


lemma r_distinguishable_k_intersection_paths : 
  assumes "¬(∃ k . r_distinguishable_k M q1 q2 k)"
  and "q1 ∈ states M"
  and "q2 ∈ states M"
  shows "∀ xs . set xs ⊆ (inputs M) ⟶ (∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs)"
proof (rule ccontr)
  assume "¬ (∀ xs . set xs ⊆ (inputs M) ⟶ (∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs))"
  then obtain xs where "set xs ⊆ (inputs M)"
                   and "¬ (∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs)" 
    by blast

  have "¬ r_distinguishable_k M q1 q2 (length xs)"
    using assms by auto

  show "False" 
    using r_distinguishable_k_intersection_path[OF ‹¬ r_distinguishable_k M q1 q2 (length xs)› _ ‹set xs ⊆ (inputs M)› assms(2,3)]
          ‹¬ (∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs)› by fastforce
qed




subsubsection ‹Equivalence of R-Distinguishability Definitions›


lemma r_distinguishable_alt_def :
  assumes "q1 ∈ states M" and "q2 ∈ states M"
  shows "r_distinguishable M q1 q2 ⟷ (∃ k . r_distinguishable_k M q1 q2 k)"
proof 
  show "r_distinguishable M q1 q2 ⟹ ∃k. r_distinguishable_k M q1 q2 k" 
  proof (rule ccontr)

    (* Proof sketch: if no k exists such that q1 and q2 are r(k)-distinguishable, then 
                     it is possible to construct a complete submachine of the product 
                     machine (product (from_FSM M q1) (from_FSM M q2)) by using only those
                     transitions in (product (from_FSM M q1) (from_FSM M q2)) that lead
                     from a pair of non r(0)-distinguishable states to a pair that is not
                     r(j)-distinguishable for any j. 
    *)

    assume "r_distinguishable M q1 q2"
    assume c_assm: "¬ (∃k. r_distinguishable_k M q1 q2 k)"
  
    let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
    (* filter function to restrict transitions of ?P *)
    let ?f = "λ t . ¬ r_distinguishable_k M (fst (t_source t)) (snd (t_source t)) 0 ∧ ¬ (∃ k . r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k) ∧ t_source t ∈ reachable_states ?P"
    let ?ft = "Set.filter ?f (transitions ?P)"
    (* resulting submachine of ?P *)
    let ?PC = "filter_transitions ?P ?f" 
    let ?PCR = "restrict_to_reachable_states ?PC"
  
  
    have h_ft : "transitions ?PC = { t ∈ transitions ?P . ?f t }" 
      by auto

    have states_non_r_d_k : "⋀ q . q ∈ reachable_states ?PC ⟹ ¬ (∃ k . r_distinguishable_k M (fst q) (snd q) k)"
    proof -   
      fix q assume "q ∈ reachable_states ?PC"
      have "q = initial ?PC ∨ (∃ t ∈ transitions ?PC . q = t_target t)"
        by (metis (no_types, lifting) ‹q ∈ reachable_states (FSM.filter_transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (λt. ¬ r_distinguishable_k M (fst (t_source t)) (snd (t_source t)) 0 ∧ (∄k. r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k) ∧ t_source t ∈ reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))))› reachable_states_initial_or_target)
      then have "q = (q1,q2) ∨ (∃ t ∈ transitions ?PC . q = t_target t)"
        by (simp add: assms(1) assms(2))

      show "¬ (∃ k . r_distinguishable_k M (fst q) (snd q) k)"
      proof (cases "q = (q1,q2)")
        case True
        then show ?thesis using c_assm by auto
      next
        case False
        then obtain t where "t ∈ transitions ?PC" and "q = t_target t" using ‹q = (q1,q2) ∨ (∃ t ∈ transitions ?PC . q = t_target t)› by blast
        then show ?thesis
          using h_ft by blast 
      qed
    qed
    then have states_non_r_d_k_PCR: "⋀ q . q ∈ states ?PCR ⟹ ¬ (∃ k . r_distinguishable_k M (fst q) (snd q) k)"
      unfolding restrict_to_reachable_states_simps by blast

    have "⋀ q . q ∈ reachable_states ?PC ⟹ completely_specified_state ?PC q"  
    proof -
      fix q assume "q ∈ reachable_states ?PC"
      then have "q ∈ reachable_states ?P"
        using filter_transitions_reachable_states by fastforce

      show "completely_specified_state ?PC q"
      proof (rule ccontr)
        assume "¬ completely_specified_state ?PC q"
        then obtain x where "x ∈ (inputs ?PC)" 
                        and "¬(∃ t ∈ transitions ?PC . t_source t = q ∧ t_input t = x)"
          unfolding completely_specified_state.simps by blast
        then have "¬(∃ t ∈ transitions ?P . t_source t = q ∧ t_input t = x ∧ ?f t)"
          using h_ft by blast
        then have not_f : "⋀ t . t ∈ transitions ?P ⟹ t_source t = q ⟹ t_input t = x ⟹ ¬ ?f t"
          by blast


        have "∃ k . r_distinguishable_k M (fst q) (snd q) k"
        proof (cases "r_distinguishable_k M (fst q) (snd q) 0")
          case True
          then show ?thesis by blast
        next
          case False

          let ?tp = "{t . t ∈ transitions ?P ∧ t_source t = q ∧ t_input t = x}"
          have "finite ?tp" using fsm_transitions_finite[of ?P] by force
 
          have k_ex : "∀ t ∈ ?tp . ∃ k . ∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"
          proof 
            fix t assume "t ∈ ?tp"
            then have "¬ ?f t" using not_f by blast
            then obtain k where "r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k" 
              using False ‹t ∈ ?tp›
              using ‹q ∈ reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))› by blast
            then have "∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"
              using nat_induct_at_least by fastforce
            then show "∃ k . ∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'" by auto
          qed

          obtain k where k_def : "⋀ t . t ∈ ?tp ⟹ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"          
            using finite_set_min_param_ex[OF ‹finite ?tp›, of "λ t k' . r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"]  k_ex by blast
          
          then have "∀ t ∈ transitions ?P . (t_source t = q ∧ t_input t = x) ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
            by blast
          
          have "r_distinguishable_k M (fst q) (snd q) (Suc k)"
          proof - 
            have "⋀ t1 t2 . t1 ∈ transitions M ⟹ t2 ∈ transitions M ⟹ t_source t1 = fst q ⟹ t_source t2 = snd q ⟹ t_input t1 = x ⟹ t_input t2 = x ⟹ t_output t1 = t_output t2 ⟹ r_distinguishable_k M (t_target t1) (t_target t2) k"
            proof -
              fix t1 t2 assume "t1 ∈ transitions M" 
                           and "t2 ∈ transitions M" 
                           and "t_source t1 = fst q" 
                           and "t_source t2 = snd q" 
                           and "t_input t1 = x" 
                           and "t_input t2 = x" 
                           and "t_output t1 = t_output t2"
              then have "t_input t1 = t_input t2"
                    and "t_output t1 = t_output t2" by auto

              
              have "(fst q, snd q) ∈ reachable_states ?P" using  ‹q ∈ reachable_states ?P› by (metis prod.collapse)
              then have "(fst q, snd q) ∈ states ?P" using reachable_state_is_state by metis
              then have "fst q ∈ states (from_FSM M q1)"
                    and "snd q ∈ states (from_FSM M q2)"
                unfolding product_simps by auto

              have "t1 ∈ transitions (from_FSM M q1)"
                by (simp add: ‹t1 ∈ FSM.transitions M› assms(1))
              moreover have "t2 ∈ transitions (from_FSM M q2)"
                by (simp add: ‹t2 ∈ FSM.transitions M› assms(2))   
              moreover have "t_source ((t_source t1, t_source t2),t_input t1,t_output t1,(t_target t1,t_target t2)) = q"
                using ‹t_source t1 = fst q› ‹t_source t2 = snd q› by auto
              moreover have "t_input ((t_source t1, t_source t2),t_input t1,t_output t1,(t_target t1,t_target t2)) = x"
                using ‹t_input t1 = x› by auto
              ultimately have tt: "((t_source t1, t_source t2),t_input t1,t_output t1,(t_target t1,t_target t2)) ∈ ?tp"
                unfolding product_transitions_alt_def
                using ‹t_input t1 = x› ‹t_input t2 = x› ‹t_output t1 = t_output t2› by fastforce
                

              show "r_distinguishable_k M (t_target t1) (t_target t2) k"
                using k_def[OF tt] by auto
            qed

            moreover have "x ∈ (inputs M)" 
              using ‹x ∈ (inputs ?PC)› unfolding filter_transitions_simps product_simps  from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›]
              by blast
            ultimately show ?thesis
              unfolding r_distinguishable_k.simps by blast
          qed
          then show ?thesis by blast
        qed

        then show "False" 
          using states_non_r_d_k[OF ‹q ∈ reachable_states ?PC›] by blast
      qed
    qed
    then have "⋀ q . q ∈ states ?PCR ⟹ completely_specified_state ?PCR q"
      unfolding restrict_to_reachable_states_simps completely_specified_state.simps
      by blast 
    then have "completely_specified ?PCR"
      using completely_specified_states by blast   
    moreover have "is_submachine ?PCR ?P"
    proof -
      have "is_submachine ?PC ?P"
        unfolding is_submachine.simps filter_transitions_simps by blast
      moreover have "is_submachine ?PCR ?PC"
        unfolding is_submachine.simps restrict_to_reachable_states_simps
        using reachable_state_is_state by fastforce 
      ultimately show ?thesis
        using submachine_transitive by blast
    qed
    ultimately have "r_compatible M q1 q2"
      unfolding r_compatible_def by blast
    then show "False" using ‹r_distinguishable M q1 q2›
      by blast 
  qed  
  

  show "∃k. r_distinguishable_k M q1 q2 k ⟹ r_distinguishable M q1 q2"
  proof (rule ccontr)
    assume *: "¬ r_distinguishable M q1 q2"
    assume **: "∃k. r_distinguishable_k M q1 q2 k"        
    then obtain k where "r_distinguishable_k M q1 q2 k" by auto
    then show "False"
    using * assms proof (induction k arbitrary: q1 q2)
      case 0
      then obtain S where "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
                      and "completely_specified S"
        by (meson r_compatible_def)      
      then have "completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2)))"
        using complete_submachine_initial by metis
      then show "False" using r_distinguishable_k_0_not_completely_specified[OF "0.prems"(1,3,4) ] by metis
    next
      case (Suc k)
      then show "False" 
      proof (cases "r_distinguishable_k M q1 q2 k")
        case True
        then show ?thesis 
          using Suc.IH Suc.prems by blast 
      next
        case False
        then obtain x where "x ∈ (inputs M)"
                        and "∀y q1' q2'. (q1, x, y, q1') ∈ transitions M ∧ (q2, x, y, q2') ∈ transitions M ⟶ r_distinguishable_k M q1' q2' k"
          using Suc.prems(1) by fastforce

        from Suc obtain S where "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
                            and "completely_specified S"
          by (meson r_compatible_def) 

        have "x ∈ (inputs (product (from_FSM M q1) (from_FSM M q2)))"
          by (simp add: Suc.prems(4) ‹x ∈ FSM.inputs M›) 
        then have "x ∈ (inputs S)" 
          using ‹is_submachine S (product (from_FSM M q1) (from_FSM M q2))›
          by (metis is_submachine.elims(2)) 

        moreover have "initial S = (q1,q2)"
          using ‹is_submachine S (product (from_FSM M q1) (from_FSM M q2))›
          by (simp add: Suc.prems(3) Suc.prems(4))
        ultimately obtain y q1' q2' where "((q1,q2),x,y,(q1',q2')) ∈ transitions S"
          using ‹completely_specified S› using fsm_initial by fastforce 
        then have "((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
          using ‹is_submachine S (product (from_FSM M q1) (from_FSM M q2))›
          by auto
        then have "(q1, x, y, q1') ∈ transitions (from_FSM M q1)" and "(q2, x, y, q2') ∈ transitions (from_FSM M q2)" 
          unfolding product_transitions_def by force+
        then have "(q1, x, y, q1') ∈ transitions M" and "(q2, x, y, q2') ∈ transitions M"
          by (simp add: Suc.prems(3,4))+
        then have "r_distinguishable_k M q1' q2' k" 
          using ‹∀y q1' q2'. (q1, x, y, q1') ∈ transitions M ∧ (q2, x, y, q2') ∈ transitions M ⟶ r_distinguishable_k M q1' q2' k› by blast
        have "r_distinguishable M q1' q2'"
          by (metis (no_types) Suc.IH ‹(q1, x, y, q1') ∈ FSM.transitions M› ‹(q2, x, y, q2') ∈ FSM.transitions M› ‹r_distinguishable_k M q1' q2' k› fsm_transition_target snd_conv) 
        moreover have "∃ S' . completely_specified S' ∧ is_submachine S' (product (from_FSM M q1') (from_FSM M q2'))"
          using submachine_transition_complete_product_from[OF ‹is_submachine S (product (from_FSM M q1) (from_FSM M q2))› ‹completely_specified S› ‹((q1,q2),x,y,(q1',q2')) ∈ transitions S› Suc.prems(3,4)]
                submachine_transition_product_from[OF ‹is_submachine S (product (from_FSM M q1) (from_FSM M q2))› ‹((q1,q2),x,y,(q1',q2')) ∈ transitions S› Suc.prems(3,4)]          by blast 

        ultimately show "False" unfolding r_compatible_def by blast
      qed
    qed
  qed
qed



subsection ‹Bounds›


inductive is_least_r_d_k_path :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ (('a × 'a) × 'b × nat) list ⇒ bool" where
  immediate[intro!] : "x ∈ (inputs M) ⟹ ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟹ is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]" |
  step[intro!] : "Suc k = (LEAST k' . r_distinguishable_k M q1 q2 k') 
                  ⟹ x ∈ (inputs M)
                  ⟹ (∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k)
                  ⟹ t1 ∈ transitions M
                  ⟹ t2 ∈ transitions M
                  ⟹ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2
                  ⟹ is_least_r_d_k_path M (t_target t1) (t_target t2) p
                  ⟹ is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"

inductive_cases is_least_r_d_k_path_immediate_elim[elim!]: "is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]"
inductive_cases is_least_r_d_k_path_step_elim[elim!]: "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"


lemma is_least_r_d_k_path_nonempty :
  assumes "is_least_r_d_k_path M q1 q2 p"
  shows "p ≠ []"
  using is_least_r_d_k_path.cases[OF assms] by blast

lemma is_least_r_d_k_path_0_extract : 
  assumes "is_least_r_d_k_path M q1 q2 [t]"
  shows "∃ x . t = ((q1,q2),x,0)"
    using is_least_r_d_k_path.cases[OF assms]
    by (metis (no_types, lifting) list.inject is_least_r_d_k_path_nonempty) 

lemma is_least_r_d_k_path_Suc_extract : 
  assumes "is_least_r_d_k_path M q1 q2 (t#t'#p)"
  shows "∃ x k . t = ((q1,q2),x,Suc k)"
    using is_least_r_d_k_path.cases[OF assms]
    by (metis (no_types, lifting) list.distinct(1) list.inject)

lemma is_least_r_d_k_path_Suc_transitions :
  assumes "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"
  shows "(∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k)"
  using is_least_r_d_k_path_step_elim[OF assms]
        Suc_inject[of _ k]  
  by metis


lemma is_least_r_d_k_path_is_least :
  assumes "is_least_r_d_k_path M q1 q2 (t#p)"
  shows "r_distinguishable_k M q1 q2 (snd (snd t)) ∧ (snd (snd t)) = (LEAST k' . r_distinguishable_k M q1 q2 k')"
proof (cases p)
  case Nil
  then obtain x where "t = ((q1,q2),x,0)" and "is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]"
    using assms is_least_r_d_k_path_0_extract by metis
  have *: "r_distinguishable_k M q1 q2 0"
    using is_least_r_d_k_path_immediate_elim[OF ‹is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]›] unfolding r_distinguishable_k.simps by auto
  then have "(∃k. r_distinguishable_k M q1 q2 k)"
    by blast
  then have "0 = (LEAST k' . r_distinguishable_k M q1 q2 k')" 
    using ‹r_distinguishable_k M q1 q2 0› by auto
  moreover have "snd (snd t) = 0"
    using ‹t = ((q1,q2),x,0)› by auto
  ultimately show ?thesis using * by auto  
next
  case (Cons t' p')
  then obtain x k where "t = ((q1,q2),x,Suc k)" and "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#t'#p')"
    using assms is_least_r_d_k_path_Suc_extract by metis

  have "x ∈ (inputs M)"
    using is_least_r_d_k_path_step_elim[OF ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#t'#p')›] by blast
  moreover have "(∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k)"
    using is_least_r_d_k_path_Suc_transitions[OF ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#(t'#p'))›] by assumption
  ultimately have "r_distinguishable_k M q1 q2 (Suc k)"
    unfolding r_distinguishable_k.simps by blast
  moreover have "Suc k = (LEAST k' . r_distinguishable_k M q1 q2 k')"
    using is_least_r_d_k_path_step_elim[OF ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#t'#p')›] by blast  
  ultimately show ?thesis
    by (metis ‹t = ((q1, q2), x, Suc k)› snd_conv) 
qed


lemma r_distinguishable_k_least_next :
  assumes "∃ k . r_distinguishable_k M q1 q2 k"
      and "(LEAST k . r_distinguishable_k M q1 q2 k) = Suc k"
      and "x ∈ (inputs M)"
      and "∀t1∈ transitions M. ∀t2∈ transitions M.
            t_source t1 = q1 ∧
            t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
            r_distinguishable_k M (t_target t1) (t_target t2) k"
    shows "∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ∧ (LEAST k . r_distinguishable_k M (t_target t1) (t_target t2) k) = k"
proof -
  have "r_distinguishable_k M q1 q2 (Suc k)"
    using assms LeastI by metis
  moreover have "¬ r_distinguishable_k M q1 q2 k"
    using assms(2) by (metis lessI not_less_Least) 

  have **: "(∀t1∈ transitions M.
         ∀t2∈ transitions M.
            t_source t1 = q1 ∧
            t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
            (LEAST k' . r_distinguishable_k M (t_target t1) (t_target t2) k') ≤ k)"
    using assms(3,4) Least_le by blast

  show ?thesis proof (rule ccontr)
    assume assm : "¬ (∃t1∈(transitions M).
           ∃t2∈(transitions M).
              (t_source t1 = q1 ∧
               t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ∧
              (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k) = k)"
    
    let ?hs = "{(t1,t2) | t1 t2 . t1 ∈ transitions M ∧ t2 ∈ transitions M ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2}"
    have "finite ?hs"
    proof -
      have "?hs ⊆ (transitions M × transitions M)" by blast
      moreover have "finite (transitions M × transitions M)" using fsm_transitions_finite by blast
      ultimately show ?thesis
        by (simp add: finite_subset) 
    qed
    have fk_def : "⋀ tt . tt ∈ ?hs ⟹ r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)"
    proof -
      fix tt assume "tt ∈ ?hs"
      then have "(fst tt) ∈ transitions M ∧ (snd tt) ∈ transitions M ∧ t_source (fst tt) = q1 ∧ t_source (snd tt) = q2 ∧ t_input (fst tt) = x ∧ t_input (snd tt) = x ∧ t_output (fst tt) = t_output (snd tt)"
        by force 
      then have "∃ k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k"
        using assms(4) by blast
      then show "r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)"
        using LeastI2_wellorder by blast            
    qed

    let ?k = "Max (image (λ tt . (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)) ?hs)"
    have "⋀ t1 t2 . t1 ∈ transitions M ⟹ t2 ∈ transitions M ⟹ t_source t1 = q1 ⟹ t_source t2 = q2 ⟹ t_input t1 = x ⟹ t_input t2 = x ⟹ t_output t1 = t_output t2 ⟹ r_distinguishable_k M (t_target t1) (t_target t2) ?k"
    proof -
      fix t1 t2 assume "t1 ∈ transitions M" 
                   and "t2 ∈ transitions M" 
                   and "t_source t1 = q1" 
                   and "t_source t2 = q2" 
                   and "t_input t1 = x" 
                   and "t_input t2 = x" 
                   and "t_output t1 = t_output t2"   
      then have "(t1,t2) ∈ ?hs" by force
      then have "r_distinguishable_k M (t_target t1) (t_target t2) ((λ tt . (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)) (t1,t2))"
        using fk_def by force
      have "(λ tt . (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)) (t1,t2) ≤ ?k"
        using ‹(t1,t2) ∈ ?hs› ‹finite ?hs›
        by (meson Max.coboundedI finite_imageI image_iff) 
      show "r_distinguishable_k M (t_target t1) (t_target t2) ?k" 
        using r_distinguishable_k_by_larger[OF ‹r_distinguishable_k M (t_target t1) (t_target t2) ((λ tt . (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)) (t1,t2))› ‹(λ tt . (LEAST k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k)) (t1,t2) ≤ ?k›] by assumption
    qed


    then have "r_distinguishable_k M q1 q2 (Suc ?k)"
      unfolding r_distinguishable_k.simps 
      using ‹x ∈ (inputs M)› by blast

    have "?hs ≠ {}"
    proof 
      assume "?hs = {}"
      then have "r_distinguishable_k M q1 q2 0"
        unfolding r_distinguishable_k.simps using ‹x ∈ (inputs M)› by force
      then show "False"
        using assms(2) by auto
    qed

    have "⋀ t1 t2 . t1∈ transitions M ⟹
         t2∈ transitions M ⟹
            t_source t1 = q1 ∧
            t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟹
            (LEAST k' . r_distinguishable_k M (t_target t1) (t_target t2) k') < k" 
    proof -  
      fix t1 t2 assume "t1∈ transitions M" and "t2∈ transitions M" and t12_def : "t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
      have "(LEAST k' . r_distinguishable_k M (t_target t1) (t_target t2) k') ≤ k" using ‹t1∈ transitions M› ‹t2∈ transitions M› t12_def ** by blast
      moreover have "(LEAST k' . r_distinguishable_k M (t_target t1) (t_target t2) k') ≠ k" using ‹t1∈ transitions M› ‹t2∈ transitions M› t12_def assm by blast
      ultimately show "(LEAST k' . r_distinguishable_k M (t_target t1) (t_target t2) k') < k" by auto
    qed
    moreover have "⋀ tt . tt ∈ ?hs ⟹ (fst tt) ∈ transitions M ∧ (snd tt) ∈ transitions M ∧ t_source (fst tt) = q1 ∧ t_source (snd tt) = q2 ∧ t_input (fst tt) = x ∧ t_input (snd tt) = x ∧ t_output (fst tt) = t_output (snd tt)"
      by force
    ultimately have "⋀ tt . tt ∈ ?hs ⟹ (LEAST k' . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k') < k" by blast
    moreover obtain tt where "tt ∈ ?hs" and "?k = (LEAST k' . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k')" 
      using Max_elem[OF ‹finite ?hs› ‹?hs ≠ {}›, of "λ tt . (LEAST k' . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k')"] by blast
    ultimately have "?k < k" 
      using ‹finite ?hs› by presburger

    then show "False"
      using assms(2) ‹r_distinguishable_k M q1 q2 (Suc ?k)›
      by (metis (no_types, lifting) Suc_mono not_less_Least) 
  qed
qed   


lemma is_least_r_d_k_path_length_from_r_d :
  assumes "∃ k . r_distinguishable_k M q1 q2 k"
  shows "∃ t p . is_least_r_d_k_path M q1 q2 (t#p) ∧ length (t#p) = Suc (LEAST k . r_distinguishable_k M q1 q2 k)"
proof -
  let ?k = "LEAST k . r_distinguishable_k M q1 q2 k"
  have "r_distinguishable_k M q1 q2 ?k"
    using assms LeastI by blast 
  
  then show ?thesis using assms proof (induction ?k arbitrary: q1 q2)
    case 0
    then have "r_distinguishable_k M q1 q2 0" by auto
    then obtain x where "x ∈ (inputs M)" and "¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
      unfolding r_distinguishable_k.simps by blast
    then have "is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]"
      by auto
    then show ?case using "0.hyps"
      by (metis length_Cons list.size(3))
  next
    case (Suc k)
    then have "r_distinguishable_k M q1 q2 (Suc k)" by auto
    moreover have "¬ r_distinguishable_k M q1 q2 k"
      using Suc by (metis lessI not_less_Least) 
    ultimately obtain x where "x ∈ (inputs M)" and *: "(∀t1∈(transitions M).
           ∀t2∈(transitions M).
              t_source t1 = q1 ∧
              t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
              r_distinguishable_k M (t_target t1) (t_target t2) k)"
      unfolding r_distinguishable_k.simps by blast
    
    obtain t1 t2 where "t1 ∈ transitions M" and "t2 ∈ transitions M"
                        and "t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
                        and "k = (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)"
      using r_distinguishable_k_least_next[OF Suc.prems(2) _ ‹x ∈ (inputs M)› *] Suc.hyps(2) by metis
    then have "r_distinguishable_k M (t_target t1) (t_target t2) (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)"
      using * by metis
    
    then obtain t' p' where "is_least_r_d_k_path M (t_target t1) (t_target t2) (t' # p')"
                        and "length (t' # p') = Suc (Least (r_distinguishable_k M (t_target t1) (t_target t2)))"
      using Suc.hyps(1)[OF ‹k = (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)›] by blast

    then have "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#t'#p')"
      using is_least_r_d_k_path.step[OF Suc.hyps(2) ‹x ∈ (inputs M)› * ‹t1 ∈ transitions M› ‹t2 ∈ transitions M› ‹t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2›] 
      by auto

    
    show ?case
      by (metis (no_types) Suc.hyps(2) ‹is_least_r_d_k_path M q1 q2 (((q1, q2), x, Suc k) # t' # p')› ‹k = (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)› ‹length (t' # p') = Suc (Least (r_distinguishable_k M (t_target t1) (t_target t2)))› length_Cons)      
  qed
qed



lemma is_least_r_d_k_path_states :
  assumes "is_least_r_d_k_path M q1 q2 p"
      and "q1 ∈ states M"
      and "q2 ∈ states M"
shows "set (map fst p) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
  using assms proof (induction p)
  case (immediate x M q1 q2) 
  then show ?case by auto
next
  case (step k M q1 q2 x t1 t2 p)
  then have "t_target t1 ∈ states M" and "t_target t2 ∈ states M" by blast+
  have "t_source t1 = q1" and "t_source t2 = q2"
    using step by metis+

  have "t_target t1 ∈ states (from_FSM M q1)"
    by (simp add: ‹t_target t1 ∈ FSM.states M› step.prems(1))
  have "t_target t2 ∈ states (from_FSM M q2)"
    by (simp add: ‹t_target t2 ∈ FSM.states M› step.prems(2)) 

  have "t1 ∈ transitions (from_FSM M q1)"
    by (simp add: step.hyps(4) step.prems(1))    
  have "t2 ∈ transitions (from_FSM M q2)"
    by (simp add: step.hyps(5) step.prems(2))
  have "t_input t1 = t_input t2" using step.hyps(6) by auto
  have "t_output t1 = t_output t2" using step.hyps(6) by auto

  have "((q1,q2),t_input t1, t_output t1, (t_target t1, t_target t2)) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" 
    using ‹t1 ∈ transitions (from_FSM M q1)› ‹t2 ∈ transitions (from_FSM M q2)› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› ‹t_source t1 = q1› ‹t_source t2 = q2›
    unfolding product_transitions_alt_def by blast

  then have "(t_target t1, t_target t2) ∈ states (product (from_FSM M q1) (from_FSM M q2))"
    using fsm_transition_target
    by (metis snd_conv) 

  moreover have "states (product (from_FSM M (t_target t1)) (from_FSM M (t_target t2))) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
    using calculation step.prems(1) step.prems(2) by auto
    

  moreover have "set (map fst p) ⊆ states (product (from_FSM M (t_target t1)) (from_FSM M (t_target t2)))"
    using step.IH  ‹t_target t1 ∈ states (from_FSM M q1)›  ‹t_target t2 ∈ states (from_FSM M q2)›
    using step.prems by auto
  ultimately have "set (map fst p) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
    by blast
  
  moreover have "set (map fst [((q1,q2),x,Suc k)]) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
    using fsm_transition_source[OF ‹((q1, q2), t_input t1, t_output t1, t_target t1, t_target t2) ∈ (transitions (product (from_FSM M q1) (from_FSM M q2)))›]
    by auto
    
  ultimately show ?case
    by auto
qed


lemma is_least_r_d_k_path_decreasing :
  assumes "is_least_r_d_k_path M q1 q2 p"
  shows "∀ t' ∈ set (tl p) . snd (snd t') < snd (snd (hd p))"
using assms proof(induction p)
  case (immediate x M q1 q2)
  then show ?case by auto
next
  case (step k M q1 q2 x t1 t2 p)
  then show ?case proof (cases p)
    case Nil
    then show ?thesis by auto
  next
    case (Cons t' p')
    then have "is_least_r_d_k_path M (t_target t1) (t_target t2) (t'#p')" using step.hyps(7) by auto

    have "r_distinguishable_k M (t_target t1) (t_target t2) (snd (snd t'))" 
     and "snd (snd t') = (LEAST k'. r_distinguishable_k M (t_target t1) (t_target t2) k')"
      using is_least_r_d_k_path_is_least[OF ‹is_least_r_d_k_path M (t_target t1) (t_target t2) (t'#p')›] by auto

    have "snd (snd t') < Suc k"
      by (metis ‹snd (snd t') = (LEAST k'. r_distinguishable_k M (t_target t1) (t_target t2) k')› local.step(3) local.step(4) local.step(5) local.step(6) not_less_Least not_less_eq)
    moreover have "∀t''∈set p. snd (snd t'') ≤ snd (snd t')" 
      using Cons step.IH by auto
    ultimately show ?thesis by auto
  qed
qed


lemma is_least_r_d_k_path_suffix :
  assumes "is_least_r_d_k_path M q1 q2 p"
      and "i < length p"
    shows "is_least_r_d_k_path M (fst (fst (hd (drop i p)))) (snd (fst (hd (drop i p)))) (drop i p)"
using assms proof(induction p arbitrary: i)
  case (immediate x M q1 q2)
  then show ?case by auto
next
  case (step k M q1 q2 x t1 t2 p)
  then have "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"
    by blast 

  have "⋀ i . i < length p ⟹ is_least_r_d_k_path M (fst (fst (hd (drop (Suc i) (((q1, q2), x, Suc k) # p))))) (snd (fst (hd (drop (Suc i) (((q1, q2), x, Suc k) # p))))) (drop (Suc i) (((q1, q2), x, Suc k) # p))"
    using step.IH by simp
  then have "⋀ i . i < length (((q1, q2), x, Suc k) # p) ⟹ i > 0 ⟹ is_least_r_d_k_path M (fst (fst (hd (drop i (((q1, q2), x, Suc k) # p))))) (snd (fst (hd (drop i (((q1, q2), x, Suc k) # p))))) (drop i (((q1, q2), x, Suc k) # p))"
    by (metis Suc_less_eq gr0_implies_Suc length_Cons)
  moreover have "⋀ i . i < length (((q1, q2), x, Suc k) # p) ⟹ i = 0 ⟹ is_least_r_d_k_path M (fst (fst (hd (drop i (((q1, q2), x, Suc k) # p))))) (snd (fst (hd (drop i (((q1, q2), x, Suc k) # p))))) (drop i (((q1, q2), x, Suc k) # p))"
    using ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)› by auto
  ultimately show ?case
    using step.prems by blast 
qed

  
lemma is_least_r_d_k_path_distinct :
  assumes "is_least_r_d_k_path M q1 q2 p"
  shows "distinct (map fst p)"
using assms proof(induction p)
  case (immediate x M q1 q2)
  then show ?case by auto
next
  case (step k M q1 q2 x t1 t2 p)
  then have "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"
    by blast 
  
  show ?case proof (rule ccontr)
    assume "¬ distinct (map fst (((q1, q2), x, Suc k) # p))"
    then have "(q1,q2) ∈ set (map fst p)"
      using step.IH by simp 
    then obtain i where "i < length p" and "(map fst p) ! i = (q1,q2)"
      by (metis distinct_Ex1 length_map step.IH)
    then obtain x' k' where "hd (drop i p) = ((q1,q2),x',k')"
      by (metis fst_conv hd_drop_conv_nth nth_map old.prod.exhaust)

    have "is_least_r_d_k_path M q1 q2 (drop i p)"
      using is_least_r_d_k_path_suffix[OF ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)›] ‹i < length p›
    proof -
      have "snd (fst (hd (drop i p))) = q2"
        using ‹hd (drop i p) = ((q1, q2), x', k')› by auto
      then show ?thesis
        by (metis (no_types) ‹hd (drop i p) = ((q1, q2), x', k')› ‹i < length p› fst_conv is_least_r_d_k_path_suffix step.hyps(7))
    qed

    have "k' < Suc k"
      using is_least_r_d_k_path_decreasing[OF ‹is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)›]
      by (metis Cons_nth_drop_Suc ‹hd (drop i p) = ((q1, q2), x', k')› ‹i < length p› hd_in_set in_set_dropD list.sel(1) list.sel(3) list.simps(3) snd_conv)
    moreover have "k' = (LEAST k'. r_distinguishable_k M q1 q2 k')"  
      using is_least_r_d_k_path_is_least ‹is_least_r_d_k_path M q1 q2 (drop i p)› is_least_r_d_k_path_is_least
      by (metis Cons_nth_drop_Suc ‹hd (drop i p) = ((q1, q2), x', k')› ‹i < length p› hd_drop_conv_nth snd_conv)
    ultimately show "False"
      using step.hyps(1) dual_order.strict_implies_not_eq by blast 
  qed
qed


lemma r_distinguishable_k_least_bound :
  assumes "∃ k . r_distinguishable_k M q1 q2 k"
      and "q1 ∈ states M"
      and "q2 ∈ states M"
  shows "(LEAST k . r_distinguishable_k M q1 q2 k) ≤ (size (product (from_FSM M q1) (from_FSM M q2)))"
proof (rule ccontr)
  assume "¬ (LEAST k. r_distinguishable_k M q1 q2 k) ≤ (size (product (from_FSM M q1) (from_FSM M q2)))"
  then have c_assm : "(size (product (from_FSM M q1) (from_FSM M q2))) < (LEAST k. r_distinguishable_k M q1 q2 k)"
    by linarith

  obtain t p where "is_least_r_d_k_path M q1 q2 (t # p)" 
               and "length (t # p) = Suc (LEAST k. r_distinguishable_k M q1 q2 k)"
    using is_least_r_d_k_path_length_from_r_d[OF assms(1)] by blast
  then have "(size (product (from_FSM M q1) (from_FSM M q2))) < length (t # p)"
    using c_assm by linarith

  have "distinct (map fst (t # p))"
    using is_least_r_d_k_path_distinct[OF ‹is_least_r_d_k_path M q1 q2 (t # p)›] by assumption
  then have "card (set (map fst (t # p))) = length (t # p)"
    using distinct_card by fastforce
  moreover have "card (set (map fst (t # p))) ≤ size (product (from_FSM M q1) (from_FSM M q2))"
    using is_least_r_d_k_path_states[OF ‹is_least_r_d_k_path M q1 q2 (t # p)› assms(2,3)] fsm_states_finite card_mono unfolding size_def by blast
  ultimately have "length (t # p) ≤ size (product (from_FSM M q1) (from_FSM M q2))"
    by (metis) 
  then show "False"
    using ‹size (product (from_FSM M q1) (from_FSM M q2)) < length (t # p)› by linarith
qed




subsection ‹Deciding R-Distinguishability›

fun r_distinguishable_k_least :: "('a, 'b::linorder, 'c) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ (nat × 'b) option" where
  "r_distinguishable_k_least M q1 q2 0 = (case find (λ x . ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)) (sort (inputs_as_list M)) of
    Some x ⇒ Some (0,x) |
    None ⇒ None)" |
  "r_distinguishable_k_least M q1 q2 (Suc n) = (case r_distinguishable_k_least M q1 q2 n of
    Some k ⇒ Some k |
    None ⇒ (case find (λ x . ∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) n) (sort (inputs_as_list M)) of
      Some x ⇒ Some (Suc n,x) |
      None ⇒ None))"


lemma r_distinguishable_k_least_ex : 
  assumes "r_distinguishable_k_least M q1 q2 k = None" 
  shows "¬ r_distinguishable_k M q1 q2 k"
using assms proof (induction k)
  case 0
  show ?case proof (rule ccontr)
    assume "¬ ¬ r_distinguishable_k M q1 q2 0"
    then have "(∃x∈set (sort (inputs_as_list M)).
                 ¬ (∃t1∈(transitions M).
                        ∃t2∈(transitions M).
                           t_source t1 = q1 ∧
                           t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2))"
      unfolding r_distinguishable_k.simps
      using inputs_as_list_set by auto 
    then obtain x where "find (λ x . ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)) (sort (inputs_as_list M)) = Some x"
      unfolding r_distinguishable_k.simps using find_None_iff[of "λ x . ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)" "sort (inputs_as_list M)"] by blast
    then have "r_distinguishable_k_least M q1 q2 0 = Some (0,x)"
      unfolding r_distinguishable_k_least.simps by auto
    then show "False" using 0 by simp
  qed
next
  case (Suc k)
  
  have "r_distinguishable_k_least M q1 q2 k = None"
    using Suc.prems unfolding r_distinguishable_k_least.simps
    using option.disc_eq_case(2) by force 
  then have *: "¬ r_distinguishable_k M q1 q2 k"
    using Suc.IH by auto

  have "find
             (λx. ∀t1∈(transitions M).
                     ∀t2∈(transitions M).
                        t_source t1 = q1 ∧
                        t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
                        r_distinguishable_k M (t_target t1) (t_target t2) k)
             (sort (inputs_as_list M))  = None"
    using Suc.prems ‹r_distinguishable_k_least M q1 q2 k = None› unfolding r_distinguishable_k_least.simps
    using option.disc_eq_case(2) by force 

  then have **: "¬(∃ x ∈ set (sort (inputs_as_list M)) .  (∀t1∈(transitions M).
                     ∀t2∈(transitions M).
                        t_source t1 = q1 ∧
                        t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
                        r_distinguishable_k M (t_target t1) (t_target t2) k))"
    using find_None_iff[of "(λx. ∀t1∈(transitions M).
                     ∀t2∈(transitions M).
                        t_source t1 = q1 ∧
                        t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
                        r_distinguishable_k M (t_target t1) (t_target t2) k)" "(sort (inputs_as_list M))"] by auto
  
    
  show ?case using * ** unfolding r_distinguishable_k.simps
    using inputs_as_list_set by fastforce 
qed
  

lemma r_distinguishable_k_least_0_correctness :
  assumes  "r_distinguishable_k_least M q1 q2 n = Some (0,x)"  
  shows "r_distinguishable_k M q1 q2 0 ∧ 0 = 
            (LEAST k . r_distinguishable_k M q1 q2 k) 
            ∧ (x ∈ (inputs M) ∧ ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2))
            ∧ (∀ x' ∈ (inputs M) . x' < x ⟶ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x' ∧ t_input t2 = x' ∧ t_output t1 = t_output t2))"
using assms proof (induction n)
  case 0
  then obtain x' where x'_def : "find (λ x . ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)) (sort (inputs_as_list M)) = Some x'"
    unfolding r_distinguishable_k_least.simps by fastforce 
  then have "x = x'" using 0 unfolding r_distinguishable_k_least.simps by fastforce
  then have "x ∈ set (sort (inputs_as_list M)) ∧ ¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)" using 0 unfolding r_distinguishable_k_least.simps r_distinguishable_k.simps 
    using find_condition[OF x'_def] find_set[OF x'_def] by blast
  moreover have "r_distinguishable_k M q1 q2 0"
    using calculation List.linorder_class.set_sort unfolding r_distinguishable_k.simps
    using inputs_as_list_set by auto
  moreover have "0 = (LEAST k . r_distinguishable_k M q1 q2 k)"
    using calculation(2) by auto
  moreover have "(∀ x' ∈ (inputs M) . x' < x ⟶ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x' ∧ t_input t2 = x' ∧ t_output t1 = t_output t2))"
    using find_sort_least(1)[OF x'_def] ‹x = x'› inputs_as_list_set
    using leD by blast
  ultimately show ?case unfolding inputs_as_list_set set_sort by force
next
  case (Suc n)
  then show ?case proof (cases "r_distinguishable_k_least M q1 q2 n")
    case None
    have "r_distinguishable_k_least M q1 q2 (Suc n) ≠ Some (0, x)"
      using Suc.prems unfolding r_distinguishable_k_least.simps None
      by (metis (no_types, lifting) Zero_not_Suc fst_conv option.case_eq_if option.distinct(1) option.sel) 
    then show ?thesis using Suc.prems by auto
  next
    case (Some a)
    then have "r_distinguishable_k_least M q1 q2 n = Some (0, x)"
      using Suc.prems by auto
    then show ?thesis using Suc.IH by blast
  qed
qed


lemma r_distinguishable_k_least_Suc_correctness :
  assumes  "r_distinguishable_k_least M q1 q2 n = Some (Suc k,x)"  
  shows "r_distinguishable_k M q1 q2 (Suc k) ∧ (Suc k) = 
          (LEAST k . r_distinguishable_k M q1 q2 k) 
          ∧ (x ∈ (inputs M) ∧ (∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k))
          ∧ (∀ x' ∈ (inputs M) . x' < x ⟶ ¬(∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x' ∧ t_input t2 = x' ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k))"
using assms proof (induction n)
  case 0
  then show ?case by (cases " find
         (λx. ¬ (∃t1∈(transitions M).
                     ∃t2∈(transitions M).
                        t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2))
         (sort (inputs_as_list M))"; auto)
next
  case (Suc n)
  then show ?case proof (cases "r_distinguishable_k_least M q1 q2 n")
    case None
    then have *: "(case find (λ x . ∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) n) (sort (inputs_as_list M)) of
      Some x ⇒ Some (Suc n,x) |
      None ⇒ None) = Some (Suc k,x)"
      using Suc.prems unfolding r_distinguishable_k_least.simps by auto
    then obtain x' where x'_def : "find (λ x . ∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) n) (sort (inputs_as_list M)) =  Some x'" 
      by fastforce
    then have "x = x'" using * by fastforce
    then have p3: "x ∈ (inputs M) ∧ (∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) n)"  
      using find_condition[OF x'_def] find_set[OF x'_def] set_sort inputs_as_list_set by metis
    then have p1: "r_distinguishable_k M q1 q2 (Suc n)"
      unfolding r_distinguishable_k.simps by blast
    moreover have "¬ r_distinguishable_k M q1 q2 n"
      using r_distinguishable_k_least_ex[OF None] by assumption
    ultimately have p2: "(Suc n) = (LEAST k . r_distinguishable_k M q1 q2 k)"
      by (metis LeastI Least_le le_SucE r_distinguishable_k_by_larger)

    from * have "k = n" using x'_def by auto
    then have "(∀ x' ∈ (inputs M) . x' < x ⟶ ¬(∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . (t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x' ∧ t_input t2 = x' ∧ t_output t1 = t_output t2) ⟶ r_distinguishable_k M (t_target t1) (t_target t2) k))"
      using find_sort_least(1)[OF x'_def] ‹x = x'› inputs_as_list_set
      using leD by blast
    then show ?thesis using p1 p2 p3 ‹k = n› by blast
  next
    case (Some a)
    then have "r_distinguishable_k_least M q1 q2 n = Some (Suc k, x)"
      using Suc.prems by auto
    then show ?thesis using Suc.IH
      by (meson r_distinguishable_k.simps(2))
  qed
qed


lemma r_distinguishable_k_least_is_least :
  assumes "r_distinguishable_k_least M q1 q2 n = Some (k,x)"
  shows "(∃ k . r_distinguishable_k M q1 q2 k) ∧ (k = (LEAST k . r_distinguishable_k M q1 q2 k))"
proof (cases k)
  case 0
  then show ?thesis using assms r_distinguishable_k_least_0_correctness by metis
next
  case (Suc n)
  then show ?thesis using assms r_distinguishable_k_least_Suc_correctness by metis
qed 


lemma r_distinguishable_k_from_r_distinguishable_k_least :
  assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "(∃ k . r_distinguishable_k M q1 q2 k) = (r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) ≠ None)"
  (is "?P1 = ?P2")
proof 
  show "?P1 ⟹ ?P2"
    using r_distinguishable_k_least_ex r_distinguishable_k_least_bound[OF _ assms] r_distinguishable_k_by_larger
    by (metis LeastI)
  show "?P2 ⟹ ?P1"
  proof -
    assume ?P2
    then obtain a where "(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some a)"
      by blast
    then obtain x k where kx_def : "(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some (k,x))"
      using prod.collapse by metis
    then show ?P1
    proof (cases k)
      case 0
      then have "(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some (0,x))"
        using kx_def by presburger
      show ?thesis using r_distinguishable_k_least_0_correctness[OF ‹(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some (0,x))›] by blast
    next
      case (Suc n)
      then have "(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some ((Suc n),x))"
        using kx_def by presburger
      show ?thesis using r_distinguishable_k_least_Suc_correctness[OF ‹(r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) = Some ((Suc n),x))›] by blast
    qed
  qed
qed


definition is_r_distinguishable :: "('a, 'b, 'c) fsm ⇒ 'a ⇒ 'a ⇒ bool" where
  "is_r_distinguishable M q1 q2 = (∃ k . r_distinguishable_k M q1 q2 k)"


lemma is_r_distinguishable_contained_code[code] :
  "is_r_distinguishable M q1 q2 = (if (q1 ∈ states M ∧ q2 ∈ states M) then (r_distinguishable_k_least M q1 q2 (size (product (from_FSM M q1) (from_FSM M q2))) ≠ None)
                                                                    else ¬(inputs M = {}))"
proof (cases "q1 ∈ states M ∧ q2 ∈ states M")
  case True
  then show ?thesis 
    unfolding is_r_distinguishable_def using r_distinguishable_k_from_r_distinguishable_k_least by metis
next
  case False
  then have *: "(¬ (∃ t ∈ transitions M . t_source t = q1)) ∨ (¬ (∃ t ∈ transitions M . t_source t = q2))"
    using fsm_transition_source by auto
  show ?thesis proof (cases "inputs M = {}")
    case True
    moreover have "⋀ k . r_distinguishable_k M q1 q2 k ⟹ inputs M ≠ {}"
    proof -
      fix k assume "r_distinguishable_k M q1 q2 k"
      then show "inputs M ≠ {}" by (induction k; auto)
    qed
    ultimately have "is_r_distinguishable M q1 q2 = False"
      by (meson is_r_distinguishable_def)
    then show ?thesis using False True by auto
  next
    case False
    then show ?thesis
      by (meson "*" equals0I fst_conv is_r_distinguishable_def r_distinguishable_k_0_alt_def r_distinguishable_k_from_r_distinguishable_k_least) 
  qed 
qed



subsection ‹State Separators and R-Distinguishability›

lemma state_separator_r_distinguishes_k :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S"
      and "q1 ∈ states M" and "q2 ∈ states M" 
  shows "∃ k . r_distinguishable_k M q1 q2 k"
proof -
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
  let ?C = "(canonical_separator M q1 q2)"
  
  have "is_submachine S ?C"
        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∈reachable_states S. q ≠ Inr q1 ∧ q ≠ Inr q2 ⟶ isl q ∧ ¬ deadlock_state S q)"
        and tc: "(∀q∈reachable_states S.
              ∀x∈(inputs ?C).
                 (∃t∈ transitions S. t_source t = q ∧ t_input t = x) ⟶
                 (∀t'∈ transitions ?C. t_source t' = q ∧ t_input t' = x ⟶ t' ∈ transitions S))"
    using assms(1) unfolding is_state_separator_from_canonical_separator_def by linarith+

  let ?Prop = "(λ q . case q of 
                    (Inl (q1',q2')) ⇒ (∃ k . r_distinguishable_k M q1' q2' k) |
                    (Inr qr) ⇒ True)"
  have rprop: "∀ q ∈ reachable_states S . ?Prop q"
  using ‹acyclic S› proof (induction rule: acyclic_induction)
  case (reachable_state q)
    then show ?case proof (cases "¬ isl q")
      case True
      then have "q = Inr q1 ∨ q = Inr q2"
        using ‹(∀q∈reachable_states S. q ≠ Inr q1 ∧ q ≠ Inr q2 ⟶ isl q ∧ ¬ deadlock_state S q)› reachable_state(1) by blast
      then show ?thesis by auto
    next
      case False
      then obtain q1' q2' where "q = Inl (q1',q2')" 
        using isl_def prod.collapse by metis
      then have "¬ deadlock_state S q"
        using ‹(∀q∈reachable_states S. q ≠ Inr q1 ∧ q ≠ Inr q2 ⟶ isl q ∧ ¬ deadlock_state S q)› reachable_state(1) by blast

      then obtain t where "t ∈ transitions S" and "t_source t = q"
        unfolding deadlock_state.simps by blast
      then have "(∀t'∈ transitions ?C. t_source t' = q ∧ t_input t' = t_input t ⟶ t' ∈ transitions S)"
        using reachable_state(1) tc
        using fsm_transition_input by fastforce  


      have "Inl (q1',q2') ∈ reachable_states ?C"
        using reachable_state(1) unfolding  ‹q = Inl (q1',q2')› reachable_states_def
        using submachine_path_initial[OF ‹is_submachine S (canonical_separator M q1 q2)›] 
        unfolding canonical_separator_simps[OF assms(2,3)] is_state_separator_from_canonical_separator_initial[OF assms(1-3)] by fast
      then obtain p where "path ?C (initial ?C) p"
                      and "target (initial ?C) p = Inl (q1',q2')"
        unfolding reachable_states_def by auto 
      then have "isl (target (initial ?C) p)" 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 canonical_separator_path_from_shift[OF ‹path ?C (initial ?C) p›]
        using assms(2) assms(3) by blast  

      have "(q1',q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
        using reachable_state_is_state[OF ‹Inl (q1',q2') ∈ reachable_states ?C›] unfolding canonical_separator_simps[OF assms(2,3)]
        by auto 

      have "path (from_FSM M q1) (initial (from_FSM M q1)) (left_path p')"
          and "path (from_FSM M q2) (initial (from_FSM M q2)) (right_path p')"
        using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 p'] ‹path ?P (initial ?P) p'›
        by (simp add: paths_from_product_path)+
      moreover have "target (initial (from_FSM M q1)) (left_path p') = q1'"
        using ‹p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'› ‹target (initial ?C) p = Inl (q1',q2')› canonical_separator_simps(1)[OF assms(2,3)] assms(2)
        by (cases p' rule: rev_cases; auto)
      moreover have "target (initial (from_FSM M q2)) (right_path p') = q2'"
        using ‹p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'› ‹target (initial ?C) p = Inl (q1',q2')› canonical_separator_simps(1)[OF assms(2,3)] assms(3) 
        by (cases p' rule: rev_cases; auto)
      moreover have "p_io (left_path p') = p_io (right_path p')" by auto
      ultimately have p12' : "∃p1 p2.
               path (from_FSM M q1) (initial (from_FSM M q1)) p1 ∧
               path (from_FSM M q2) (initial (from_FSM M q2)) p2 ∧
               target (initial (from_FSM M q1)) p1 = q1' ∧
               target (initial (from_FSM M q2)) p2 = q2' ∧ p_io p1 = p_io p2"
        by blast

      have "q1' ∈ states (from_FSM M q1)"
        using path_target_is_state[OF ‹path (from_FSM M q1) (initial (from_FSM M q1)) (left_path p')›] ‹target (initial (from_FSM M q1)) (left_path p') = q1'› by auto
      have "q2' ∈ states (from_FSM M q2)"
        using path_target_is_state[OF ‹path (from_FSM M q2) (initial (from_FSM M q2)) (right_path p')›] ‹target (initial (from_FSM M q2)) (right_path p') = q2'› by auto

      have "t_input t ∈ (inputs S)"
        using ‹t ∈ transitions S› by auto
      then have "t_input t ∈ (inputs ?C)"
        using ‹is_submachine S ?C› by auto
      then have "t_input t ∈ (inputs M)"
        using canonical_separator_simps(3)[OF assms(2,3)] by metis

      have *: "⋀ t1 t2 . t1 ∈ transitions M ⟹ t2 ∈ transitions M ⟹ t_source t1 = q1' ⟹ t_source t2 = q2' ⟹ t_input t1 = t_input t ⟹ t_input t2 = t_input t ⟹ t_output t1 = t_output t2 ⟹ (∃ k . r_distinguishable_k M (t_target t1) (t_target t2) k)"
      proof -
        fix t1 t2 assume "t1 ∈ transitions M" 
                     and "t2 ∈ transitions M" 
                     and "t_source t1 = q1'" 
                     and "t_source t2 = q2'" 
                     and "t_input t1 = t_input t" 
                     and "t_input t2 = t_input t" 
                     and "t_output t1 = t_output t2"
        then have "t_input t1 = t_input t2" by auto

        have "t1 ∈ transitions (from_FSM M q1)" 
          using ‹t_source t1 = q1'› ‹q1' ∈ states (from_FSM M q1)› ‹t1 ∈ transitions M› by (simp add: assms(2))
        have "t2 ∈ transitions (from_FSM M q2)"
          using ‹t_source t2 = q2'› ‹q2' ∈ states (from_FSM M q2)› ‹t2 ∈ transitions M› by (simp add: assms(3))

        let ?t = "((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2)"

        have "?t ∈ transitions ?P"
          using ‹t1 ∈ transitions (from_FSM M q1)› ‹t2 ∈ transitions (from_FSM M q2)› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2›
          unfolding product_transitions_alt_def 
          by blast
        then have "shift_Inl ?t ∈ transitions ?C"
          using ‹(q1',q2') ∈ states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))›
          unfolding ‹t_source t1 = q1'› ‹t_source t2 = q2'› canonical_separator_transitions_def[OF assms(2,3)] by fastforce
        moreover have "t_source (shift_Inl ?t) = q"
          using ‹t_source t1 = q1'› ‹t_source t2 = q2'› ‹q = Inl (q1',q2')› by auto
        ultimately have "shift_Inl ?t ∈ transitions S"
          using ‹(∀t'∈ transitions ?C. t_source t' = q ∧ t_input t' = t_input t ⟶ t' ∈ transitions S)› ‹t_input t1 = t_input t› by auto

        
        have "case t_target (shift_Inl ?t) of Inl (q1', q2') ⇒ ∃k. r_distinguishable_k M q1' q2' k | Inr qr ⇒ True"
          using reachable_state.IH(2)[OF ‹shift_Inl ?t ∈ transitions S› ‹t_source (shift_Inl ?t) = q›] by (cases q; auto)
        moreover have "t_target (shift_Inl ?t) = Inl (t_target t1, t_target t2)" 
          by auto
        ultimately show "∃k. r_distinguishable_k M (t_target t1) (t_target t2) k"
          by auto
      qed

      
      let ?hs = "{(t1,t2) | t1 t2 . t1 ∈ transitions M ∧ t2 ∈ transitions M ∧ t_source t1 = q1' ∧ t_source t2 = q2' ∧ t_input t1 = t_input t ∧ t_input t2 = t_input t ∧ t_output t1 = t_output t2}"
      have "finite ?hs"
      proof -
        have "?hs ⊆ (transitions M × transitions M)" by blast
        moreover have "finite (transitions M × transitions M)" using fsm_transitions_finite by blast
        ultimately show ?thesis
          by (simp add: finite_subset) 
      qed
      obtain fk where fk_def : "⋀ tt . tt ∈ ?hs ⟹ r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) (fk tt)"
      proof 
        let ?fk = "λ tt . SOME k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k"
        show "⋀ tt . tt ∈ ?hs ⟹ r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) (?fk tt)"
        proof -
          fix tt assume "tt ∈ ?hs"
          then have "(fst tt) ∈ transitions M ∧ (snd tt) ∈ transitions M ∧ t_source (fst tt) = q1' ∧ t_source (snd tt) = q2' ∧ t_input (fst tt) = t_input t ∧ t_input (snd tt) = t_input t ∧ t_output (fst tt) = t_output (snd tt)"
            by force 
          then have "∃ k . r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) k"
            using * by blast
          then show "r_distinguishable_k M (t_target (fst tt)) (t_target (snd tt)) (?fk tt)"
            by (simp add: someI_ex)
        qed
      qed

      let ?k = "Max (image fk ?hs)"
      have "⋀ t1 t2 . t1 ∈ transitions M ⟹ t2 ∈ transitions M ⟹ t_source t1 = q1' ⟹ t_source t2 = q2' ⟹ t_input t1 = t_input t ⟹ t_input t2 = t_input t ⟹ t_output t1 = t_output t2 ⟹ r_distinguishable_k M (t_target t1) (t_target t2) ?k"
      proof -
        fix t1 t2 assume "t1 ∈ transitions M" 
                     and "t2 ∈ transitions M" 
                     and "t_source t1 = q1'" 
                     and "t_source t2 = q2'" 
                     and "t_input t1 = t_input t" 
                     and "t_input t2 = t_input t" 
                     and "t_output t1 = t_output t2"   
        then have "(t1,t2) ∈ ?hs"
          by force
        then have "r_distinguishable_k M (t_target t1) (t_target t2) (fk (t1,t2))"
          using fk_def by force
        have "fk (t1,t2) ≤ ?k"
          using ‹(t1,t2) ∈ ?hs› ‹finite ?hs› by auto
        show "r_distinguishable_k M (t_target t1) (t_target t2) ?k" 
          using r_distinguishable_k_by_larger[OF ‹r_distinguishable_k M (t_target t1) (t_target t2) (fk (t1,t2))› ‹fk (t1,t2) ≤ ?k›] by assumption
      qed


      then have "r_distinguishable_k M q1' q2' (Suc ?k)"
        unfolding r_distinguishable_k.simps 
        using ‹t_input t ∈ (inputs M)› by blast
      then show "?Prop q"
        using ‹q = Inl (q1',q2')›
        by (metis (no_types, lifting) case_prodI old.sum.simps(5)) 
    qed
  qed

  moreover have "Inl (q1,q2) ∈ states S"
    using ‹is_submachine S ?C› canonical_separator_simps(1)[OF assms(2,3)] fsm_initial[of S] by auto
  ultimately show "∃k. r_distinguishable_k M q1 q2 k"
    using reachable_states_initial[of S] using is_state_separator_from_canonical_separator_initial[OF assms(1-3)] by auto 
qed

end