Theory Traversal_Set

section ‹Traversal Set›

text ‹This theory defines the calculation of m-traversal paths.
      These are paths extended from some state until they visit pairwise r-distinguishable states
      a number of times dependent on m.›  

theory Traversal_Set
imports Helper_Algorithms 
begin


definition m_traversal_paths_with_witness_up_to_length :: 
  "('a,'b,'c) fsm ⇒ 'a ⇒ ('a set × 'a set) list ⇒ nat ⇒ nat ⇒ (('a×'b×'c×'a) list × ('a set × 'a set)) set" 
  where
  "m_traversal_paths_with_witness_up_to_length M q D m k 
    = paths_up_to_length_or_condition_with_witness M (λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D) k q"

definition m_traversal_paths_with_witness :: 
  "('a,'b,'c) fsm ⇒ 'a ⇒ ('a set × 'a set) list ⇒ nat ⇒ (('a×'b×'c×'a) list × ('a set × 'a set)) set" 
  where
  "m_traversal_paths_with_witness M q D m = m_traversal_paths_with_witness_up_to_length M q D m (Suc (size M * m))"


lemma m_traversal_paths_with_witness_finite : "finite (m_traversal_paths_with_witness M q D m)"
  unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def
  by (simp add: paths_up_to_length_or_condition_with_witness_finite) 
  

lemma m_traversal_paths_with_witness_up_to_length_max_length :
  assumes "⋀ q . q ∈ states M ⟹ ∃ d ∈ set D . q ∈ fst d"
  and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
  and     "q ∈ states M"
  and     "(p,d) ∈ (m_traversal_paths_with_witness_up_to_length M q D m k)"
shows "length p ≤ Suc ((size M) * m)"
proof (rule ccontr)
  assume "¬ length p ≤ Suc (FSM.size M * m)"

  let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

  have "path M q []" using assms(3) by auto
  
  have "path M q p"
        and "length p ≤ k"
        and "?f p = Some d"
        and "∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ ?f p' = None"
    using assms(4) 
    unfolding m_traversal_paths_with_witness_up_to_length_def paths_up_to_length_or_condition_with_witness_def 
    by auto

  let ?p = "take (Suc (m * size M)) p"
  let ?p' = "drop (Suc (m * size M)) p"
  have "path M q ?p"
    using ‹path M q p› using path_prefix[of M q ?p "drop (Suc (m * size M)) p"]
    by simp
  have "?p' ≠ []"
    using ‹¬ length p ≤ Suc (FSM.size M * m)›
    by (simp add: mult.commute) 

  have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
  proof (rule ccontr)
    assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
      by auto
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
      by auto
    
    have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
      using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono) 
    then have "length ?p ≤ m * (size M)"
      using path_length_sum[OF ‹path M q ?p›] 
      using fsm_states_finite[of M] 
      by (simp add: mult.commute)

    then show "False"
      using ‹¬ length p ≤ Suc (FSM.size M * m)›
      by (simp add: mult.commute) 
  qed

  then obtain q where "q ∈ states M"
                  and "length (filter (λ t . t_target t = q) ?p) ≥ Suc m" 
    by blast
  then obtain d where "d ∈ set D"
                  and "q ∈ fst d"
    using assms(1) by blast
  then have "⋀ t . t_target t = q ⟹ t_target t ∈ fst d" by auto
  then have "length (filter (λ t . t_target t = q) ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
    using filter_length_weakening[of "λ t . t_target t = q" "λ t . t_target t ∈ fst d"] by auto
  then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
    using ‹length (filter (λ t . t_target t = q) ?p) ≥ Suc m› by auto
  then have "?f ?p ≠ None"
    using assms(2)
  proof -
    have "∀p. find p D ≠ None ∨ ¬ p d"
      by (metis ‹d ∈ set D› find_from)
    then show ?thesis
      using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (take (Suc (m * FSM.size M)) p))› 
            diff_le_self le_trans not_less_eq_eq 
      by blast
  qed 
  then obtain d' where "?f ?p = Some d'"
    by blast

  then have "p = ?p@?p' ∧ ?p' ≠ [] ∧ ?f ?p = Some d'"
    using ‹?p' ≠ []› by auto

  then show "False"
    using ‹∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ (?f p') = None›
    by (metis (no_types) option.distinct(1))
qed


lemma m_traversal_paths_with_witness_set :
  assumes "⋀ q . q ∈ states M ⟹ ∃ d ∈ set D . q ∈ fst d"
  and     "⋀ d .  d ∈ set D ⟹ snd d ⊆ fst d"
  and     "q ∈ states M"
shows "(m_traversal_paths_with_witness M q D m) 
          = {(p,d) | p d . path M q p 
                            ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) D = Some d
                            ∧ (∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)}"
        (is "?MTP = ?P")
proof -
  let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

  have "path M q []"
    using assms(3) by auto

  have "⋀ p . p ∈ ?MTP ⟹ p ∈ ?P"
    unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def 
              paths_up_to_length_or_condition_with_witness_def
    by force
  moreover have "⋀ p . p ∈ ?P ⟹ p ∈ ?MTP"
  proof -
    fix px assume "px ∈ ?P"
    then obtain p x where "px = (p,x)"
          and p1: "path M q p"
          and **: "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) D = Some x"
          and ***:"(∀p' p''.
                     p = p' @ p'' ∧ p'' ≠ [] ⟶
                     find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)"
      using prod.collapse by force

    
    then have "(p,x) ∈ (m_traversal_paths_with_witness_up_to_length M q D m (length p))"
      unfolding m_traversal_paths_with_witness_up_to_length_def paths_up_to_length_or_condition_with_witness_def
      by force
    then have "length p ≤ Suc (size M * m)"
      using m_traversal_paths_with_witness_up_to_length_max_length[OF assms] by blast
    
    have "(p,x) ∈ ?MTP"
      using ‹path M q p› ‹length p ≤ Suc (size M * m)› ‹?f p = Some x› 
            ‹∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ (?f p') = None›
      unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def 
                paths_up_to_length_or_condition_with_witness_def
      by force 
    then show "px ∈ ?MTP"
      using ‹px = (p,x)› by simp
  qed
  ultimately show ?thesis
    by (meson subsetI subset_antisym) 
qed


lemma maximal_repetition_sets_from_separators_cover :
  assumes "q ∈ states M"
  shows "∃ d ∈ (maximal_repetition_sets_from_separators M) . q ∈ fst d"
  unfolding maximal_repetition_sets_from_separators_def
  using maximal_pairwise_r_distinguishable_state_sets_from_separators_cover[OF assms] by auto


lemma maximal_repetition_sets_from_separators_d_reachable_subset :
  shows "⋀ d . d ∈ (maximal_repetition_sets_from_separators M) ⟹ snd d ⊆ fst d"
  unfolding maximal_repetition_sets_from_separators_def
  by auto



(* Sufficient conditions for a path to be contained in the m-traversal paths *)
lemma m_traversal_paths_with_witness_set_containment :
  assumes "q ∈ states M"
  and     "path M q p"
  and     "d ∈ set repSets"
  and     "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)"
  and     "⋀ p' p''.
                  p = p' @ p'' ⟹ p'' ≠ [] ⟹
                  ¬ (∃d∈set repSets.
                         Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'))"
  and     "⋀ q . q∈states M ⟹ ∃d∈set repSets. q ∈ fst d"
  and     "⋀ d . d∈set repSets ⟹ snd d ⊆ fst d"
shows "∃ d' . (p,d') ∈ (m_traversal_paths_with_witness M q repSets m)"
proof -
  obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) repSets = Some d'"
    using assms(3,4) find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p))" repSets] 
    by auto
  moreover have "(⋀ p' p''. p = p' @ p'' ⟹ p'' ≠ [] 
                  ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repSets = None)"
    using assms(5) find_None_iff[of _ repSets] by force  
  ultimately show ?thesis
    using m_traversal_paths_with_witness_set[of M repSets q m, OF  assms(6,7,1)] 
    using assms(2) by blast
qed


lemma m_traversal_path_exist :
  assumes "completely_specified M"
  and     "q ∈ states M"
  and     "inputs M ≠ {}"
  and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
  and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
shows "∃ p' d' . (p',d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -

  obtain p where "path M q p" and "length p = Suc ((size M) * m)"
    using path_of_length_ex[OF assms(1-3)] by blast

  let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

  have "∃ q ∈ states M . length (filter (λt . t_target t = q) p) ≥ Suc m"
  proof (rule ccontr)
    assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) p))"
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) p) < Suc m"
      by auto
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) p) ≤ m"
      by auto
    
    have "(∑q∈states M. length (filter (λt. t_target t = q) p)) ≤ (∑q∈states M . m)"
      using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) p) ≤ m› by (meson sum_mono) 
    then have "length p ≤ m * (size M)"
      using path_length_sum[OF ‹path M q p›] 
      using fsm_states_finite[of M] 
      by (simp add: mult.commute)

    then show "False"
      using ‹length p = Suc ((size M) * m)›
      by (simp add: mult.commute) 
  qed

  then obtain q' where "q' ∈ states M"
                   and "length (filter (λ t . t_target t = q') p) ≥ Suc m" 
    by blast
  then obtain d where "d ∈ set D"
                  and "q' ∈ fst d"
    using assms(4) by blast
  then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
  then have "length (filter (λ t . t_target t = q') p) ≤ length (filter (λ t . t_target t ∈ fst d) p)"
    using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
  then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p)"
    using ‹length (filter (λ t . t_target t = q') p) ≥ Suc m› by auto
  then have "?f p ≠ None"
    using assms(2)
  proof -
    have "∀p. find p D ≠ None ∨ ¬ p d"
      by (metis ‹d ∈ set D› find_from)
    have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p)"
      using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p)› by linarith
    then show ?thesis
      using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast    
  qed 
  then obtain d' where "?f p = Some d'"
    by blast


  show ?thesis proof (cases "(∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
    case True
    then show ?thesis 
      using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q p› ‹?f p = Some d'› 
      by blast
  next
    case False

    define ps where ps_def: "ps = {p' . ∃ p''. p = p' @ p'' ∧ p'' ≠ [] 
                                              ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
    have "ps ≠ {}" 
      using False ps_def 
      by blast
    moreover have "finite ps" 
    proof -
      have "ps ⊆ set (prefixes p)"
        unfolding prefixes_set ps_def
        by blast 
      then show ?thesis
        by (meson List.finite_set rev_finite_subset) 
    qed
    ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
      by (meson leI min_length_elem) 
    then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] 
                ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
    proof -
      fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
      show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
      proof (rule ccontr) 
        assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
        moreover have "∃p'''. p = p'' @ p''' ∧ p''' ≠ []"
          using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
        ultimately have "p'' ∈ ps"
          unfolding ps_def by auto
        moreover have "length p'' < length p'" 
          using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
        ultimately show "False"
          using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
          using leD by auto 
      qed
    qed 

    have "path M q p'" and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
      using ‹path M q p› ‹p' ∈ ps› unfolding ps_def by auto
    then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
      by auto


    then have "path M q p' ∧
               find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
               (∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
      using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None› 
            ‹path M q p'›
      by blast
    then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
      using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
    then show ?thesis by blast
  qed 
qed



lemma m_traversal_path_extension_exist :
  assumes "completely_specified M"
  and     "q ∈ states M"
  and     "inputs M ≠ {}"
  and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
  and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
  and     "path M q p1"
  and     "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D = None"
shows "∃ p2 d' . (p1@p2,d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -
  obtain p2 where "path M (target q p1) p2" and "length p2 = (Suc ((size M) * m)) - length p1"
    using path_of_length_ex[OF assms(1) path_target_is_state[OF assms(6)] assms(3)] 
    by blast

  have "path M q (p1@p2)"
    using assms(6) ‹path M (target q p1) p2› by auto

  let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"
  
  have "length p1 < Suc ((size M) * m)"
  proof (rule ccontr)
    assume "¬ length p1 < Suc (FSM.size M * m)"
    then have "length (take (Suc (FSM.size M * m)) p1) = Suc (FSM.size M * m)"
      by auto
    let ?p = "(take (Suc (FSM.size M * m)) p1)"

    have "path M q ?p"
      using ‹path M q p1›
      by (metis append_take_drop_id path_append_elim) 

    have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
    proof (rule ccontr)
      assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
      then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
        by auto
      then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
        by auto
      
      have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
        using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono) 
      then have "length ?p ≤ m * (size M)"
        using path_length_sum[OF ‹path M q ?p›] 
        using fsm_states_finite[of M] 
        by (simp add: mult.commute)
  
      then show "False"
        using ‹length ?p = Suc ((size M) * m)›
        by (simp add: mult.commute) 
    qed
    then obtain q' where "q' ∈ states M"
                   and "length (filter (λ t . t_target t = q') ?p) ≥ Suc m" 
      by blast
    then obtain d where "d ∈ set D"
                    and "q' ∈ fst d"
      using assms(4) by blast
    then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
    then have "length (filter (λ t . t_target t = q') ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
      using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
    then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
      using ‹length (filter (λ t . t_target t = q') ?p) ≥ Suc m› by auto
    moreover have "length (filter (λt. t_target t ∈ fst d) ?p) ≤ length (filter (λt. t_target t ∈ fst d) p1)" 
    proof -
      have "⋀ xs P n . length (filter P (take n xs)) ≤ length (filter P xs)"
        by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)
      then show ?thesis by auto
    qed
    ultimately have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)"
      by auto
    then have "?f p1 ≠ None"
      using assms(2)
    proof -
      have "∀p. find p D ≠ None ∨ ¬ p d"
        by (metis ‹d ∈ set D› find_from)
      have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p1)"
        using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)› by linarith
      then show ?thesis
        using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast    
    qed 
    then obtain d' where "?f p1 = Some d'"
      by blast
    then show "False"
      using assms(7) by simp
  qed

  have "length (p1@p2) = (Suc ((size M) * m))"
    using ‹length p2 = (Suc ((size M) * m)) - length p1›
          ‹length p1 < Suc ((size M) * m)› 
    by simp

  have "∃ q ∈ states M . length (filter (λt . t_target t = q) (p1@p2)) ≥ Suc m"
  proof (rule ccontr)
    assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) (p1@p2)))"
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) < Suc m"
      by auto
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) ≤ m"
      by auto
    
    have "(∑q∈states M. length (filter (λt. t_target t = q) (p1@p2))) ≤ (∑q∈states M . m)"
      using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) ≤ m› by (meson sum_mono) 
    then have "length (p1@p2) ≤ m * (size M)"
      using path_length_sum[OF ‹path M q (p1@p2)›] 
      using fsm_states_finite[of M] 
      by (simp add: mult.commute)

    then show "False"
      using ‹length (p1@p2) = Suc ((size M) * m)›
      by (simp add: mult.commute) 
  qed
  then obtain q' where "q' ∈ states M"
                   and "length (filter (λ t . t_target t = q') (p1@p2)) ≥ Suc m" 
    by blast
  then obtain d where "d ∈ set D"
                  and "q' ∈ fst d"
    using assms(4) by blast
  then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
  then have "length (filter (λ t . t_target t = q') (p1@p2)) ≤ length (filter (λ t . t_target t ∈ fst d) (p1@p2))"
    using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"]
    by blast 
  then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) (p1@p2))"
    using ‹length (filter (λ t . t_target t = q') (p1@p2)) ≥ Suc m› by auto
  then have "?f (p1@p2) ≠ None"
    using assms(2)
  proof -
    have "∀p. find p D ≠ None ∨ ¬ p d"
      by (metis ‹d ∈ set D› find_from)
    have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) (p1@p2))"
      using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (p1@p2))› by linarith
    then show ?thesis
      using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast    
  qed 
  then obtain d' where "?f (p1@p2) = Some d'"
    by blast


  show ?thesis proof (cases "(∀p' p''. (p1@p2) = p' @ p'' ∧ p'' ≠ [] 
                                 ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
    case True
    then show ?thesis 
      using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q (p1@p2)› ‹?f (p1@p2) = Some d'› 
      by blast
  next
    case False

    define ps where ps_def: "ps = {p' . ∃ p''. (p1@p2) = p' @ p'' ∧ p'' ≠ [] 
                                                ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
    have "ps ≠ {}" using False ps_def by blast
    moreover have "finite ps" 
    proof -
      have "ps ⊆ set (prefixes (p1@p2))"
        unfolding prefixes_set ps_def
        by auto
      then show ?thesis
        by (meson List.finite_set rev_finite_subset) 
    qed
    ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
      by (meson leI min_length_elem) 
    then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] 
                            ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
    proof -
      fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
      show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
      proof (rule ccontr) 
        assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
        moreover have "∃p'''. (p1@p2) = p'' @ p''' ∧ p''' ≠ []"
          using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
        ultimately have "p'' ∈ ps"
          unfolding ps_def by auto
        moreover have "length p'' < length p'" 
          using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
        ultimately show "False"
          using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
          using leD by auto 
      qed
    qed 

    obtain p'' where "(p1@p2) = p' @ p''" 
               and   "p'' ≠ []" 
               and   "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
      using ‹p' ∈ ps› unfolding ps_def by blast
    then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
      by auto

    have "path M q p'" 
      using ‹path M q (p1@p2)›  unfolding ‹(p1@p2) = p' @ p''› by auto

    have "length p' > length p1"
    proof (rule ccontr)
      assume "¬ length p1 < length p'"
      then obtain i where "p' = take i p1"
        by (metis ‹p1 @ p2 = p' @ p''› append_eq_append_conv_if less_le)

      have "⋀ i . find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D = None"
      proof - 
        fix i
        show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D = None"
        proof (rule ccontr)
          assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D ≠ None"
          then obtain d where "d ∈ set D" 
                        and   "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))"
            using find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1)))" D] 
            by meson
          
          moreover have "length (filter (λt. t_target t ∈ fst d) (take i p1)) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
            using filter_take_length by metis
          ultimately have "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
            using le_trans by blast
          then show "False"
            using ‹d ∈ set D› assms(7) unfolding find_None_iff
            by blast 
        qed
      qed
      
      then have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"      
        unfolding ‹p' = take i p1› by blast
      then show "False"
        using ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None›          
        by auto
    qed
    
    moreover have "p' = take (length p') (p1@p2)"
      using ‹(p1@p2) = p' @ p''› by auto

    ultimately obtain p where "p' = p1 @ p"
      by auto        

    have "path M q p' ∧
           find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
           (∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
      using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None› 
            ‹path M q p'› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'›
      by blast
    then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
      using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
    then show ?thesis unfolding ‹p' = p1 @ p› by blast
  qed 
qed



lemma m_traversal_path_extension_exist_for_transition :
  assumes "completely_specified M"
  and     "q ∈ states M"
  and     "inputs M ≠ {}"
  and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
  and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
  and     "path M q p1"
  and     "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D = None"
  and     "t ∈ transitions M" 
  and     "t_source t = target q p1"
shows "∃ p2 d' . (p1@[t]@p2,d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -
  let ?q = "(target q (p1 @ [t]))"
  let ?p = "p1 @ [t]"

  have "path M q ?p"
    using ‹path M q p1› ‹t ∈ transitions M› ‹t_source t = target q p1› path_append_transition by simp
  

  obtain p2 where "path M ?q p2" and "length p2 = (Suc ((size M) * m)) - (length ?p)"
    using path_of_length_ex[OF assms(1) path_target_is_state[OF ‹path M q (p1@[t])›] assms(3)] 
    by blast

  have "path M q (?p@p2)"
    using ‹path M q ?p› ‹path M ?q p2› by auto

  let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"
  
  have "length p1 < Suc ((size M) * m)"
  proof (rule ccontr)
    assume "¬ length p1 < Suc (FSM.size M * m)"
    then have "length (take (Suc (FSM.size M * m)) p1) = Suc (FSM.size M * m)"
      by auto
    let ?p = "(take (Suc (FSM.size M * m)) p1)"

    have "path M q ?p"
      using ‹path M q p1›
      by (metis append_take_drop_id path_append_elim) 

    have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
    proof (rule ccontr)
      assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
      then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
        by auto
      then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
        by auto
      
      have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
        using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono) 
      then have "length ?p ≤ m * (size M)"
        using path_length_sum[OF ‹path M q ?p›] 
        using fsm_states_finite[of M] 
        by (simp add: mult.commute)
  
      then show "False"
        using ‹length ?p = Suc ((size M) * m)›
        by (simp add: mult.commute) 
    qed
    then obtain q' where "q' ∈ states M"
                   and "length (filter (λ t . t_target t = q') ?p) ≥ Suc m" 
      by blast
    then obtain d where "d ∈ set D"
                    and "q' ∈ fst d"
      using assms(4) by blast
    then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
    then have "length (filter (λ t . t_target t = q') ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
      using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
    then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
      using ‹length (filter (λ t . t_target t = q') ?p) ≥ Suc m› by auto
    moreover have "length (filter (λt. t_target t ∈ fst d) ?p) ≤ length (filter (λt. t_target t ∈ fst d) p1)" 
    proof -
      have "⋀ xs P n . length (filter P (take n xs)) ≤ length (filter P xs)"
        by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)
      then show ?thesis by auto
    qed
    ultimately have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)"
      by auto
    then have "?f p1 ≠ None"
      using assms(2)
    proof -
      have "∀p. find p D ≠ None ∨ ¬ p d"
        by (metis ‹d ∈ set D› find_from)
      have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p1)"
        using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)› by linarith
      then show ?thesis
        using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast    
    qed 
    then obtain d' where "?f p1 = Some d'"
      by blast
    then show "False"
      using assms(7) by simp
  qed


  have "length (?p@p2) = (Suc ((size M) * m))"
    using ‹length p2 = (Suc ((size M) * m)) - length ?p›
          ‹length p1 < Suc ((size M) * m)› 
    by simp


  have "∃ q ∈ states M . length (filter (λt . t_target t = q) (?p@p2)) ≥ Suc m"
  proof (rule ccontr)
    assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) (?p@p2)))"
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) < Suc m"
      by auto
    then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) ≤ m"
      by auto
    
    have "(∑q∈states M. length (filter (λt. t_target t = q) (?p@p2))) ≤ (∑q∈states M . m)"
      using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) ≤ m› by (meson sum_mono) 
    then have "length (?p@p2) ≤ m * (size M)"
      using path_length_sum[OF ‹path M q (?p@p2)›] 
      using fsm_states_finite[of M] 
      by (simp add: mult.commute)

    then show "False"
      using ‹length (?p@p2) = Suc ((size M) * m)›
      by (simp add: mult.commute) 
  qed

  then obtain q' where "q' ∈ states M"
                   and "length (filter (λ t . t_target t = q') (?p@p2)) ≥ Suc m" 
    by blast
  then obtain d where "d ∈ set D"
                  and "q' ∈ fst d"
    using assms(4) by blast
  then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
  then have "length (filter (λ t . t_target t = q') (?p@p2)) ≤ length (filter (λ t . t_target t ∈ fst d) (?p@p2))"
    using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"]
    by blast 
  then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) (?p@p2))"
    using ‹length (filter (λ t . t_target t = q') (?p@p2)) ≥ Suc m› by auto
  then have "?f (?p@p2) ≠ None"
    using assms(2)
  proof -
    have "∀p. find p D ≠ None ∨ ¬ p d"
      by (metis ‹d ∈ set D› find_from)
    have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) (?p@p2))"
      using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (?p@p2))› by linarith
    then show ?thesis
      using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast    
  qed 
  then obtain d' where "?f (?p@p2) = Some d'"
    by blast



  


  show ?thesis proof (cases "(∀p' p''. (?p@p2) = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
    case True
    obtain d' where "((?p@p2), d') ∈ m_traversal_paths_with_witness M q D m"
      using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q (?p@p2)› ‹?f (?p@p2) = Some d'› True by force
    then show ?thesis 
      unfolding append.assoc[symmetric] by blast
  next
    case False

    show ?thesis proof (cases "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) D")
      case (Some a)

      have *: "(∀p' p''. ?p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)"
      proof -
        have "⋀ p' p''. ?p = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
        proof -
          fix p' p'' assume "?p = p' @ p''" and "p'' ≠ []"
          then have "length p' ≤ length p1" by (induction p'' rule: rev_induct; auto)
          moreover have "p' = take (length p') ?p"
            unfolding ‹?p = p' @ p''› by auto
          ultimately have "p' = take (length p') p1" 
            by auto

          show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
          proof (rule ccontr)
            assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
            moreover have "⋀ x . length (filter (λt. t_target t ∈ fst x) p') ≤ length (filter (λt. t_target t ∈ fst x) p1)"
              using ‹p' = take (length p') p1›
              by (metis filter_take_length) 
            ultimately have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D ≠ None"
              unfolding find_None_iff
              using le_trans by blast 
            then show "False"
              using assms(7) by simp
          qed
        qed
        then show ?thesis by blast
      qed

      obtain d' where "(?p, d') ∈ m_traversal_paths_with_witness M q D m"
        using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q ?p› Some * by force
      then show ?thesis
        by fastforce
    next
      case None

      define ps where ps_def: "ps = {p' . ∃ p''. (?p@p2) = p' @ p'' 
                                                  ∧ p'' ≠ [] 
                                                  ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
      have "ps ≠ {}" using False ps_def by blast
      moreover have "finite ps" 
      proof -
        have "ps ⊆ set (prefixes (?p@p2))"
          unfolding prefixes_set ps_def
          by auto
        then show ?thesis
          by (meson List.finite_set rev_finite_subset) 
      qed
      ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
        by (meson leI min_length_elem) 
      then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
      proof -
        fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
        show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
        proof (rule ccontr) 
          assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
          moreover have "∃p'''. (?p@p2) = p'' @ p''' ∧ p''' ≠ []"
            using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
          ultimately have "p'' ∈ ps"
            unfolding ps_def by auto
          moreover have "length p'' < length p'" 
            using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
          ultimately show "False"
            using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
            using leD by auto 
        qed
      qed 
  
      obtain p'' where "(?p@p2) = p' @ p''" 
                 and   "p'' ≠ []" 
                 and   "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
        using ‹p' ∈ ps› unfolding ps_def by blast
      then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
        by auto
  
      have "path M q p'" 
        using ‹path M q (?p@p2)›  unfolding ‹(?p@p2) = p' @ p''› by auto
  
      have "length p' > length ?p"
      proof (rule ccontr)
  
        assume "¬ length ?p < length p'"
        then obtain i where "p' = take i ?p"
          by (metis ‹?p @ p2 = p' @ p''› append_eq_append_conv_if less_le)

        have "⋀ i . find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D = None"
        proof - 
          fix i
          show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D = None"
          proof (rule ccontr)
            assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D ≠ None"
            then obtain d where "d ∈ set D" 
                          and   "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))"
              using find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p)))" D] 
              by meson
            
            moreover have "length (filter (λt. t_target t ∈ fst d) (take i ?p)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
              using filter_take_length by metis
            ultimately have "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
              using le_trans by blast
            then show "False"
              using ‹d ∈ set D› None unfolding find_None_iff
              by blast
          qed
        qed
        
        then have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"      
          unfolding ‹p' = take i ?p› by blast
        then show "False"
          using ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None›          
          by auto
      qed
      
      moreover have "p' = take (length p') (?p@p2)"
        using ‹(?p@p2) = p' @ p''› by auto
  
      ultimately obtain p where "p' = ?p @ p"
        by (metis dual_order.strict_implies_order take_all take_append) 

      have "path M q p' ∧
             find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
             (∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
        using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None› ‹path M q p'› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'›
        by blast
      then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
        using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
      then show ?thesis unfolding ‹p' = ?p @ p› by fastforce
    qed 
  qed
qed

end