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