# Theory R_Distinguishability

```section ‹R-Distinguishability›

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

theory R_Distinguishability
imports State_Separator
begin

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

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

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

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

subsection ‹R(k)-Distinguishability Properties›

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

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

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

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

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

then have *: "¬ (∃ t1 t2 . t1 ∈ transitions ?F1 ∧ t2 ∈ transitions ?F2 ∧ t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
unfolding from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by simp

have **: "¬ (∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x)"
proof (rule ccontr)
assume "¬ ¬ (∃t∈ transitions (product (from_FSM M q1) (from_FSM M q2)). t_source t = (q1, q2) ∧ t_input t = x)"
then obtain t where "t ∈ transitions ?P" and "t_source t = (q1,q2)" and "t_input t = x"
by blast

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

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

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

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

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

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

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

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

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

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

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

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

have "?t1 ∈ transitions (from_FSM M q1)"
using ‹t1 ∈ transitions (from_FSM M q1)› by auto
moreover have "?t2 ∈ transitions (from_FSM M q2)"
using ‹t2 ∈ transitions (from_FSM M q2)› t2_alt by auto

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

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

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

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

lemma r_distinguishable_k_intersection_path :
assumes "¬ r_distinguishable_k M q1 q2 k"
and "length xs ≤ Suc k"
and "set xs ⊆ (inputs M)"
and "q1 ∈ states M"
and "q2 ∈ states M"
shows "∃ p . path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) p ∧ map fst (p_io p) = xs"
using assms proof (induction k arbitrary: q1 q2 xs)
case 0
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
show ?case
proof (cases "length xs < Suc 0")
case True
then have "xs = []" by auto
moreover have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) []"
by (simp add: "0.prems"(4) "0.prems"(5) nil)
moreover have "map fst (p_io []) = []" by auto
ultimately show ?thesis
by simp
next
case False

have "completely_specified_state ?P (q1,q2)"
proof (rule ccontr)
assume "¬ completely_specified_state ?P (q1,q2)"
then have "r_distinguishable_k M q1 q2 0"
using r_0_distinguishable_from_not_completely_specified_initial
by (metis "0.prems"(4) "0.prems"(5))
then show "False"
using "0.prems" by simp
qed
then have *: "∀ x ∈ (inputs ?P) . ∃ t . t ∈ transitions ?P ∧ t_source t = (q1,q2) ∧ t_input t = x"
unfolding completely_specified_state.simps by blast

let ?x = "hd xs"
have "xs = [?x]"
using "0.prems"(2) False
by (metis Suc_length_conv le_neq_implies_less length_0_conv list.sel(1))

have "?x ∈ (inputs M)"
using "0.prems"(3) False by auto
then obtain t where "t ∈ transitions ?P" and "t_source t = (q1,q2)" and "t_input t = ?x"
using "*" "0.prems"(4) "0.prems"(5) by auto

then have "path ?P (q1,q2) [t]"
using single_transition_path by metis
moreover have "map fst (p_io [t]) = xs"
using ‹t_input t = ?x› ‹xs = [hd xs]› by auto
ultimately show ?thesis
by (metis (no_types, lifting))
qed
next
case (Suc k)
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"

show ?case
proof (cases "length xs ≤ Suc k")
case True
have "¬ r_distinguishable_k M q1 q2 k"
using Suc.prems(1) by auto
show ?thesis
using Suc.IH[OF ‹¬ r_distinguishable_k M q1 q2 k› True Suc.prems(3,4,5)] by assumption
next
case False
then have "length xs = Suc (Suc k)"
using Suc.prems(2) by auto

then have "hd xs ∈ (inputs M)"
by (metis Suc.prems(3) contra_subsetD hd_in_set length_greater_0_conv zero_less_Suc)
have "set (tl xs) ⊆ (inputs M)"
by (metis ‹length xs = Suc (Suc k)› Suc.prems(3) dual_order.trans hd_Cons_tl length_0_conv nat.simps(3) set_subset_Cons)
have "length (tl xs) ≤ Suc k"
by (simp add: ‹length xs = Suc (Suc k)›)

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

have "∀ x ∈ (inputs M) . ∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x ∧ ¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
proof
fix x assume "x ∈ (inputs M)"

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

have p1: "t1 ∈ transitions (from_FSM M q1)"
by (simp add: Suc.prems(4) ‹t1 ∈ FSM.transitions M›)
have p2: "t2 ∈ transitions (from_FSM M q2)"
by (simp add: Suc.prems(5) ‹t2 ∈ FSM.transitions M›)
have p3: "t_input t1 = t_input t2"
using ‹t_input t1 = x› ‹t_input t2 = x› by auto

have ***: "((q1,q2), x, t_output t1, (t_target t1, t_target t2)) ∈ transitions ?P"
using ‹t_source t1 = q1› ‹t_source t2 = q2› ‹t_input t1 = x› p1 p2 p3 p4
unfolding product_transitions_alt_def
by blast

show "∃ t ∈ transitions ?P . t_source t = (q1,q2) ∧ t_input t = x ∧ ¬ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
by (metis "**" "***" fst_conv snd_conv)
qed

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

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

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

have "path ?P (t_target t) p"
using product_from_path_previous[OF p_def ‹t ∈ transitions ?P› Suc.prems(4,5)]  by assumption

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

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

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

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

subsubsection ‹Equivalence of R-Distinguishability Definitions›

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

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

assume "r_distinguishable M q1 q2"
assume c_assm: "¬ (∃k. r_distinguishable_k M q1 q2 k)"

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

have h_ft : "transitions ?PC = { t ∈ transitions ?P . ?f t }"
by auto

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

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

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

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

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

let ?tp = "{t . t ∈ transitions ?P ∧ t_source t = q ∧ t_input t = x}"
have "finite ?tp" using fsm_transitions_finite[of ?P] by force

have k_ex : "∀ t ∈ ?tp . ∃ k . ∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"
proof
fix t assume "t ∈ ?tp"
then have "¬ ?f t" using not_f by blast
then obtain k where "r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
using False ‹t ∈ ?tp›
using ‹q ∈ reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))› by blast
then have "∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"
using nat_induct_at_least by fastforce
then show "∃ k . ∀ k' . k' ≥ k ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'" by auto
qed

obtain k where k_def : "⋀ t . t ∈ ?tp ⟹ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
using finite_set_min_param_ex[OF ‹finite ?tp›, of "λ t k' . r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k'"]  k_ex by blast

then have "∀ t ∈ transitions ?P . (t_source t = q ∧ t_input t = x) ⟶ r_distinguishable_k M (fst (t_target t)) (snd (t_target t)) k"
by blast

have "r_distinguishable_k M (fst q) (snd q) (Suc k)"
proof -
have "⋀ t1 t2 . t1 ∈ transitions M ⟹ t2 ∈ transitions M ⟹ t_source t1 = fst q ⟹ t_source t2 = snd q ⟹ t_input t1 = x ⟹ t_input t2 = x ⟹ t_output t1 = t_output t2 ⟹ r_distinguishable_k M (t_target t1) (t_target t2) k"
proof -
fix t1 t2 assume "t1 ∈ transitions M"
and "t2 ∈ transitions M"
and "t_source t1 = fst q"
and "t_source t2 = snd q"
and "t_input t1 = x"
and "t_input t2 = x"
and "t_output t1 = t_output t2"
then have "t_input t1 = t_input t2"
and "t_output t1 = t_output t2" by auto

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

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

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

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

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

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

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

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

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

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

subsection ‹Bounds›

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

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

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

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

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

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

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

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

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

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

show ?thesis proof (rule ccontr)
assume assm : "¬ (∃t1∈(transitions M).
∃t2∈(transitions M).
(t_source t1 = q1 ∧
t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2) ∧
(LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k) = k)"

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

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

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

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

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

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

lemma is_least_r_d_k_path_length_from_r_d :
assumes "∃ k . r_distinguishable_k M q1 q2 k"
shows "∃ t p . is_least_r_d_k_path M q1 q2 (t#p) ∧ length (t#p) = Suc (LEAST k . r_distinguishable_k M q1 q2 k)"
proof -
let ?k = "LEAST k . r_distinguishable_k M q1 q2 k"
have "r_distinguishable_k M q1 q2 ?k"
using assms LeastI by blast

then show ?thesis using assms proof (induction ?k arbitrary: q1 q2)
case 0
then have "r_distinguishable_k M q1 q2 0" by auto
then obtain x where "x ∈ (inputs M)" and "¬ (∃ t1 ∈ transitions M . ∃ t2 ∈ transitions M . t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
unfolding r_distinguishable_k.simps by blast
then have "is_least_r_d_k_path M q1 q2 [((q1,q2),x,0)]"
by auto
then show ?case using "0.hyps"
by (metis length_Cons list.size(3))
next
case (Suc k)
then have "r_distinguishable_k M q1 q2 (Suc k)" by auto
moreover have "¬ r_distinguishable_k M q1 q2 k"
using Suc by (metis lessI not_less_Least)
ultimately obtain x where "x ∈ (inputs M)" and *: "(∀t1∈(transitions M).
∀t2∈(transitions M).
t_source t1 = q1 ∧
t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2 ⟶
r_distinguishable_k M (t_target t1) (t_target t2) k)"
unfolding r_distinguishable_k.simps by blast

obtain t1 t2 where "t1 ∈ transitions M" and "t2 ∈ transitions M"
and "t_source t1 = q1 ∧ t_source t2 = q2 ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
and "k = (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)"
using r_distinguishable_k_least_next[OF Suc.prems(2) _ ‹x ∈ (inputs M)› *] Suc.hyps(2) by metis
then have "r_distinguishable_k M (t_target t1) (t_target t2) (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)"
using * by metis

then obtain t' p' where "is_least_r_d_k_path M (t_target t1) (t_target t2) (t' # p')"
and "length (t' # p') = Suc (Least (r_distinguishable_k M (t_target t1) (t_target t2)))"
using Suc.hyps(1)[OF ‹k = (LEAST k. r_distinguishable_k M (t_target t1) (t_target t2) k)›] by blast

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

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

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

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

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

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

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

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

moreover have "set (map fst p) ⊆ states (product (from_FSM M (t_target t1)) (from_FSM M (t_target t2)))"
using step.IH  ‹t_target t1 ∈ states (from_FSM M q1)›  ‹t_target t2 ∈ states (from_FSM M q2)›
using step.prems by auto
ultimately have "set (map fst p) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
by blast

moreover have "set (map fst [((q1,q2),x,Suc k)]) ⊆ states (product (from_FSM M q1) (from_FSM M q2))"
using fsm_transition_source[OF ‹((q1, q2), t_input t1, t_output t1, t_target t1, t_target t2) ∈ (transitions (product (from_FSM M q1) (from_FSM M q2)))›]
by auto

ultimately show ?case
by auto
qed

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

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

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

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

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

lemma is_least_r_d_k_path_distinct :
assumes "is_least_r_d_k_path M q1 q2 p"
shows "distinct (map fst p)"
using assms proof(induction p)
case (immediate x M q1 q2)
then show ?case by auto
next
case (step k M q1 q2 x t1 t2 p)
then have "is_least_r_d_k_path M q1 q2 (((q1,q2),x,Suc k)#p)"
by blast

show ?case proof (rule ccontr)
assume "¬ distinct (map fst (((q1, q2), x, Suc k) # p))"
then have "(q1,q2) ∈ set (map fst p)"
using step.IH by simp
then obtain i where "i < length p" and "(map fst p) ! i = (q1,q2)"
by (metis distinct_Ex1 length_map step.IH)
then obtain x' k' where "hd (drop i p) = ((q1,q2),x',k')"
by (metis fst_conv hd_drop_conv_nth nth_map old.prod.exhaust)

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

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

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

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

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

subsection ‹Deciding R-Distinguishability›

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

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

have "r_distinguishable_k_least M q1 q2 k = None"
using Suc.prems unfolding r_distinguishable_k_least.simps
using option.disc_eq_case(2) by force
then have *: "¬ r_distinguishable_k M q1 q2 k"
using Suc.IH by auto

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

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

show ?case using * ** unfolding r_distinguishable_k.simps
using inputs_as_list_set by fastforce
qed

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

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

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

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