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