# Theory Distinguishability

```section ‹Computation of distinguishing traces based on OFSM tables›

text ‹This theory implements an algorithm for finding minimal length distinguishing
traces for observable minimal FSMs based on OFSM tables.›

theory Distinguishability
imports Minimisation HOL.List
begin

subsection ‹Finding Diverging OFSM Tables›

(* some k such that the class of state q does not change in any OFSM table after the k-th table *)
definition ofsm_table_fixpoint_value :: "('a,'b,'c) fsm ⇒ nat" where
"ofsm_table_fixpoint_value M = (SOME k . (∀ q . q ∈ states M ⟶ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k q) ∧ (∀ q k' . q ∈ states M ⟶ k' ≥ k ⟶ ofsm_table M (λq . states M) k' q = ofsm_table M (λq . states M) k q))"

(* find the minimal k such that states q1 and q2 fall in different classes in the k-th table *)
function find_first_distinct_ofsm_table_gt :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ nat" where
"find_first_distinct_ofsm_table_gt M q1 q2 k =
(if q1 ∈ states M ∧ q2 ∈ states M ∧ ((ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2))
then (if ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2
then k
else find_first_distinct_ofsm_table_gt M q1 q2 (Suc k))
else 0)"
using prod_cases4 by blast+
termination
proof -
{
fix M :: "('a,'b,'c) fsm"
fix q1 q2 k
assume "q1 ∈ FSM.states M ∧ q2 ∈ FSM.states M ∧ ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
"ofsm_table M (λq . states M) k q1 = ofsm_table M (λq . states M) k q2"
then have "q1 ∈ FSM.states M" and "q2 ∈ FSM.states M"
and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
by force+

let ?k = "ofsm_table_fixpoint_value M"
obtain k' where "⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k' q" and "⋀ q k'' . q ∈ states M ⟹ k'' ≥ k' ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) k' q"
using ofsm_table_fix_length[of M "(λq . states M)"]
by blast
then have "(∀ q . q ∈ states M ⟶ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k' q) ∧ (∀ q k'' . q ∈ states M ⟶ k'' ≥ k' ⟶ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) k' q)"
by blast
then have *:"⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) ?k q"
and **: "⋀ q k'' . q ∈ states M ⟹ k'' ≥ ?k ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) ?k q"
using some_eq_imp[of "λ k . (∀ q . q ∈ states M ⟶ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k q) ∧ (∀ q k' . q ∈ states M ⟶ k' ≥ k ⟶ ofsm_table M (λq . states M) k' q = ofsm_table M (λq . states M) k q)" ?k k']
unfolding ofsm_table_fixpoint_value_def
by blast+

have "?k > k"
using *
‹ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2›
‹ofsm_table M (λq . states M) k q1 = ofsm_table M (λq . states M) k q2›
**[OF ‹q1 ∈ states M›]
**[OF ‹q2 ∈ states M›]
by (metis ‹q1 ∈ FSM.states M ∧ q2 ∈ FSM.states M ∧ ofsm_table_fix M (λq. FSM.states M) 0 q1 ≠ ofsm_table_fix M (λq. FSM.states M) 0 q2› leI)
then have "?k - Suc k < ?k - k"
by simp
} note t = this

show ?thesis
apply (relation "measure (λ (M, q1, q2, k) . ofsm_table_fixpoint_value M - k)")
apply auto[1]
apply (simp del: observable.simps ofsm_table_fix.simps)
by (erule t)
qed

partial_function (tailrec) find_first_distinct_ofsm_table_no_check :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ nat" where
find_first_distinct_ofsm_table_no_check_def[code]:
"find_first_distinct_ofsm_table_no_check M q1 q2 k =
(if ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2
then k
else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc k))"

(* a version of find_first_distinct_ofsm_table_gt that avoids repeating the same checks in each
recursive step *)
fun find_first_distinct_ofsm_table_gt' :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ nat" where
"find_first_distinct_ofsm_table_gt' M q1 q2 k =
(if q1 ∈ states M ∧ q2 ∈ states M ∧ ((q2 ∉ ofsm_table_fix M (λq . states M) 0 q1))
then find_first_distinct_ofsm_table_no_check M q1 q2 k
else 0)"

lemma find_first_distinct_ofsm_table_gt_code[code] :
"find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k"
proof (cases "q1 ∈ states M ∧ q2 ∈ states M ∧ ((ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2))")
case False
have "find_first_distinct_ofsm_table_gt M q1 q2 k = 0"
using False
by (metis find_first_distinct_ofsm_table_gt.simps)
moreover have "find_first_distinct_ofsm_table_gt' M q1 q2 k = 0"
proof (cases "q1 ∈ states M ∧ q2 ∈ states M")
case True
then have "q1 ∈ FSM.states M" and "q2 ∈ FSM.states M"
and "ofsm_table_fix M (λq . states M) 0 q1 = ofsm_table_fix M (λq . states M) 0 q2"
using False by force+
then have "q2 ∈ ofsm_table_fix M (λq . states M) 0 q1"
using ofsm_table_fix_eq_if_elem[of q1 M q2]
using minimise_initial_partition
by blast
then show ?thesis
by (metis find_first_distinct_ofsm_table_gt'.simps)
next
case False
then show ?thesis by (meson find_first_distinct_ofsm_table_gt'.simps)
qed
ultimately show ?thesis
by simp
next
case True
then have "q1 ∈ FSM.states M" and "q2 ∈ FSM.states M"
and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
by force+
then have "q2 ∉ ofsm_table_fix M (λq . states M) 0 q1"
using ofsm_table_fix_eq_if_elem[of q1 M q2]
using minimise_initial_partition
by blast

obtain k' where "⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k' q" and "⋀ q k'' . q ∈ states M ⟹ k'' ≥ k' ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) k' q"
using ofsm_table_fix_length[of M "(λq . states M) "]
by blast

have f1: "find_first_distinct_ofsm_table_gt M q1 q2 =
(λx. if ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2
then x
else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))"
using find_first_distinct_ofsm_table_gt.simps[of M q1 q2]
using True
by meson

have f2: "find_first_distinct_ofsm_table_no_check M q1 q2 =
(λx. if ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2
then x
else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc x))"
using True find_first_distinct_ofsm_table_no_check.simps[of M q1 q2]
by meson

have "(⋀x. k' ≤ x ⟹ ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2)"
using ‹⋀ q k'' . q ∈ states M ⟹ k'' ≥ k' ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) k' q› ‹q1 ∈ FSM.states M› ‹q2 ∈ FSM.states M›
by (metis True ‹⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) k' q›)

have "find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k"
using True ‹q2 ∉ ofsm_table_fix M (λq . states M) 0 q1› find_first_distinct_ofsm_table_gt'.simps[of M]
by meson
then show ?thesis
using recursion_renaming_helper[OF f1 f2 ‹(⋀x. k' ≤ x ⟹ ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2)›, of k']
by simp
qed

lemma find_first_distinct_ofsm_table_gt_is_first_gt :
assumes "q1 ∈ FSM.states M"
and "q2 ∈ FSM.states M"
and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
shows "ofsm_table M (λq . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 ≠ ofsm_table M (λq . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2"
and "k ≤ k' ⟹ k' < (find_first_distinct_ofsm_table_gt M q1 q2 k) ⟹ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2"
proof -

have f: "find_first_distinct_ofsm_table_gt M q1 q2 =
(λx. if ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2
then x
else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))"
using assms find_first_distinct_ofsm_table_gt.simps[of M]
by meson

obtain kx where "⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) kx q" and "⋀ q k'' . q ∈ states M ⟹ k'' ≥ kx ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) kx q"
using ofsm_table_fix_length[of M "(λq . states M)"]
by blast
have P: "(⋀x. kx ≤ x ⟹ ofsm_table M (λq . states M) x q1 ≠ ofsm_table M (λq . states M) x q2)"
using ‹⋀ q k'' . q ∈ states M ⟹ k'' ≥ kx ⟹ ofsm_table M (λq . states M) k'' q = ofsm_table M (λq . states M) kx q› ‹q1 ∈ FSM.states M› ‹q2 ∈ FSM.states M›
by (metis assms ‹⋀ q . q ∈ states M ⟹ ofsm_table_fix M (λq . states M) 0 q = ofsm_table M (λq . states M) kx q›)

show "ofsm_table M (λq . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 ≠ ofsm_table M (λq . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2"
using minimal_fixpoint_helper(1)[OF f P, of kx k] .

show "k ≤ k' ⟹ k' < (find_first_distinct_ofsm_table_gt M q1 q2 k) ⟹ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2"
using minimal_fixpoint_helper(2)[OF f P, of kx k k']
by auto
qed

abbreviation(input) "find_first_distinct_ofsm_table M q1 q2 ≡ find_first_distinct_ofsm_table_gt M q1 q2 0"

lemma find_first_distinct_ofsm_table_is_first :
assumes "q1 ∈ FSM.states M"
and "q2 ∈ FSM.states M"
and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
shows "ofsm_table M (λq . states M) (find_first_distinct_ofsm_table M q1 q2) q1 ≠ ofsm_table M (λq . states M) (find_first_distinct_ofsm_table M q1 q2) q2"
and "k' < (find_first_distinct_ofsm_table M q1 q2) ⟹ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2"
using find_first_distinct_ofsm_table_gt_is_first_gt[OF assms, of 0] by blast+

(* find IO pair (x,y) such that q1 and q2 are immediately distinguishable by it or
the states reached by this IO pair reach from q1 and q2 respectively reach distinct
classes in the (k-1)-th table *)
fun select_diverging_ofsm_table_io :: "('a,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) × ('a option × 'a option)" where
"select_diverging_ofsm_table_io M q1 q2 k = (let
ins = inputs_as_list M;
outs = outputs_as_list M;
table = ofsm_table M (λq . states M) (k-1);
f = (λ (x,y) . case (h_obs M q1 x y, h_obs M q2 x y)
of
(Some q1', Some q2')  ⇒ if table q1' ≠ table q2'
then Some ((x,y),(Some q1', Some q2'))
else None |
(None,None)           ⇒ None |
(Some q1', None)      ⇒ Some ((x,y),(Some q1', None)) |
(None, Some q2')      ⇒ Some ((x,y),(None, Some q2')))
in
hd (List.map_filter f (List.product ins outs)))"

lemma select_diverging_ofsm_table_io_Some :
assumes "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "ofsm_table M (λq . states M) (Suc k) q1 ≠ ofsm_table M (λq . states M) (Suc k) q2"
obtains x y
where "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
and "⋀ q1' q2' . h_obs M q1 x y = Some q1' ⟹ h_obs M q2 x y = Some q2' ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
and "h_obs M q1 x y ≠ None ∨ h_obs M q2 x y ≠ None"
proof -

let ?res = "select_diverging_ofsm_table_io M q1 q2 (Suc k)"

define f where f: "f = (λ (x,y) . case (h_obs M q1 x y, h_obs M q2 x y)
of
(Some q1', Some q2') ⇒ if ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'
then Some ((x,y),(Some q1', Some q2'))
else None |
(None,None) ⇒ None |
(Some q1', None) ⇒ Some ((x,y),(Some q1', None)) |
(None, Some q2') ⇒ Some ((x,y),(None, Some q2')))"

have f1: "⋀ x y . f (x,y) ≠ None ⟹ f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
proof -
fix x y assume "f (x,y) ≠ None"
then show "f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
unfolding f by (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
qed

have f2 : "⋀ q1' q2' x y . f (x,y) = Some ((x,y),(Some q1', Some q2')) ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
proof -
fix q1' q2' x y assume *: "f (x,y) = Some ((x,y),(Some q1', Some q2'))"
then have **: "f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
using f1 by auto
show "ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
using * ** unfolding f by (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
qed

have f3: "⋀ x y . f (x,y) ≠ None ⟹ h_obs M q1 x y ≠ None ∨ h_obs M q2 x y ≠ None"
proof -
fix x y assume "f (x,y) ≠ None"
then show "h_obs M q1 x y ≠ None ∨ h_obs M q2 x y ≠ None"
unfolding f by (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
qed

have *: "select_diverging_ofsm_table_io M q1 q2 (Suc k) = hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))"
unfolding f select_diverging_ofsm_table_io.simps Let_def
using diff_Suc_1 by presburger

let ?P = "∀ x y . x ∈ inputs M ⟶ y ∈ outputs M ⟶ (h_obs M q1 x y = None ⟷ h_obs M q2 x y = None)"
show ?thesis proof (cases ?P)
case False
then obtain x y where "x ∈ inputs M" and "y ∈ outputs M" and "¬ (h_obs M q1 x y = None ⟷ h_obs M q2 x y = None)"
by blast
then consider "h_obs M q1 x y = None ∧ (∃ q2' . h_obs M q2 x y = Some q2')" |
"h_obs M q2 x y = None ∧ (∃ q1' . h_obs M q1 x y = Some q1')"
by fastforce
then show ?thesis proof cases
case 1
then obtain q2' where "h_obs M q1 x y = None" and "h_obs M q2 x y = Some q2'" by blast
then have "f (x,y) = Some ((x,y),(None, Some q2'))"
unfolding f by force
moreover have "(x,y) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
using ‹y ∈ outputs M› outputs_as_list_set[of M]
using ‹x ∈ inputs M› inputs_as_list_set[of M]
using image_iff by fastforce
ultimately have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) ≠ []"
unfolding List.map_filter_def
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
then have **: "?res ∈ set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
unfolding * using hd_in_set by simp

obtain xR yR where "(xR,yR) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
and res: "f (xR,yR) = Some ?res"
using map_filter_elem[OF **]
by (metis prod.exhaust_sel)

have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
using res f1
by (metis option.distinct(1) option.sel)
then have p2: "⋀ q1' q2' . h_obs M q1 xR yR = Some q1' ⟹ h_obs M q2 xR yR = Some q2' ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
using res f1 f2 by auto
have p3: "h_obs M q1 xR yR ≠ None ∨ h_obs M q2 xR yR ≠ None"
using res f3 by blast

show ?thesis using that p1 p2 p3 by blast
next
case 2
then obtain q1' where "h_obs M q2 x y = None" and "h_obs M q1 x y = Some q1'" by blast
then have "f (x,y) = Some ((x,y),(Some q1', None))"
unfolding f by force
moreover have "(x,y) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
using ‹y ∈ outputs M› outputs_as_list_set[of M]
using ‹x ∈ inputs M› inputs_as_list_set[of M]
using image_iff by fastforce
ultimately have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) ≠ []"
unfolding List.map_filter_def
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
then have **: "?res ∈ set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
unfolding * using hd_in_set by simp

obtain xR yR where "(xR,yR) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
and res: "f (xR,yR) = Some ?res"
using map_filter_elem[OF **]
by (metis prod.exhaust_sel)

have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
using res f1
by (metis option.distinct(1) option.sel)
then have p2: "⋀ q1' q2' . h_obs M q1 xR yR = Some q1' ⟹ h_obs M q2 xR yR = Some q2' ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
using res f1 f2 by auto
have p3: "h_obs M q1 xR yR ≠ None ∨ h_obs M q2 xR yR ≠ None"
using res f3 by blast

show ?thesis using that p1 p2 p3 by blast
qed
next
case True

obtain io where "length io ≤ Suc k" and "io ∈ LS M q1 ∪ LS M q2" and "io ∉ LS M q1 ∩ LS M q2"
using ‹ofsm_table M (λq . states M) (Suc k) q1 ≠ ofsm_table M (λq . states M) (Suc k) q2›
unfolding ofsm_table_set[OF assms(2) minimise_initial_partition] ofsm_table_set[OF assms(3) minimise_initial_partition]
unfolding is_in_language_iff[OF assms(1,2)] is_in_language_iff[OF assms(1,3)]
by blast
then have "io ≠ []"
using assms(2) assms(3) by auto
then have "io = [hd io] @ tl io"
by (metis append.left_neutral append_Cons list.exhaust_sel)
then obtain x y where "hd io = (x,y)"
by (meson prod.exhaust_sel)

have "[(x,y)] ∈ LS M q1 ∩ LS M q2"
proof -
have "[(x,y)] ∈ LS M q1 ∪ LS M q2"
using ‹io ∈ LS M q1 ∪ LS M q2› language_prefix ‹hd io = (x,y)› ‹io = [hd io] @ tl io›
by (metis Un_iff)
then have "x ∈ inputs M" and "y ∈ outputs M"
by auto

consider "[(x,y)] ∈ LS M q1" | "[(x,y)] ∈ LS M q2"
using ‹[(x,y)] ∈ LS M q1 ∪ LS M q2› by blast
then show ?thesis
proof cases
case 1
then have "h_obs M q1 x y ≠ None"
using h_obs_None[OF ‹observable M›] unfolding LS_single_transition by auto
then have "h_obs M q2 x y ≠ None"
using True ‹x ∈ inputs M› ‹y ∈ outputs M› by meson
then show ?thesis
using 1 h_obs_None[OF ‹observable M›]
by (metis IntI LS_single_transition fst_conv snd_conv)
next
case 2
then have "h_obs M q2 x y ≠ None"
using h_obs_None[OF ‹observable M›] unfolding LS_single_transition by auto
then have "h_obs M q1 x y ≠ None"
using True ‹x ∈ inputs M› ‹y ∈ outputs M› by meson
then show ?thesis
using 2 h_obs_None[OF ‹observable M›]
by (metis IntI LS_single_transition fst_conv snd_conv)
qed
qed
then obtain q1' q2' where "(q1,x,y,q1') ∈ transitions M"
and "(q2,x,y,q2') ∈ transitions M"
using LS_single_transition by force
then have "q1' ∈ states M" and "q2' ∈ states M" using fsm_transition_target by auto

have "tl io ∈ LS M q1' ∪ LS M q2'"
using observable_language_transition_target[OF ‹observable M› ‹(q1,x,y,q1') ∈ transitions M›]
observable_language_transition_target[OF ‹observable M› ‹(q2,x,y,q2') ∈ transitions M›]
‹io ∈ LS M q1 ∪ LS M q2›
unfolding fst_conv snd_conv
by (metis Un_iff ‹hd io = (x, y)› ‹io = [hd io] @ tl io› append_Cons append_Nil)
moreover have "tl io ∉ LS M q1' ∩ LS M q2'"
using observable_language_transition_target[OF ‹observable M› ‹(q1,x,y,q1') ∈ transitions M›]
observable_language_transition_target[OF ‹observable M› ‹(q2,x,y,q2') ∈ transitions M›]
‹io ∈ LS M q1 ∪ LS M q2›
unfolding fst_conv snd_conv
by (metis Int_iff LS_prepend_transition ‹(q1, x, y, q1') ∈ FSM.transitions M› ‹(q2, x, y, q2') ∈ FSM.transitions M› ‹hd io = (x, y)› ‹io ≠ []› ‹io ∉ LS M q1 ∩ LS M q2› fst_conv list.collapse snd_conv)
moreover have "length (tl io) ≤ k"
using ‹length io ≤ Suc k› by auto
ultimately have "ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
unfolding ofsm_table_set_observable[OF assms(1) ‹q1' ∈ states M› minimise_initial_partition]  ofsm_table_set_observable[OF assms(1) ‹q2' ∈ states M› minimise_initial_partition]
using ‹q1' ∈ states M› ‹q2' ∈ states M› after_is_state[OF assms(1)]
by blast
moreover have "h_obs M q1 x y = Some q1'"
using ‹(q1,x,y,q1') ∈ transitions M› ‹observable M› unfolding h_obs_Some[OF ‹observable M›] observable_alt_def by auto
moreover have "h_obs M q2 x y = Some q2'"
using ‹(q2,x,y,q2') ∈ transitions M› ‹observable M› unfolding h_obs_Some[OF ‹observable M›] observable_alt_def by auto
ultimately have "f (x,y) = Some ((x,y),(Some q1', Some q2'))"
unfolding f by force

moreover have "(x,y) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
using fsm_transition_output[OF ‹(q1,x,y,q1') ∈ transitions M›] outputs_as_list_set[of M]
using fsm_transition_input[OF ‹(q1,x,y,q1') ∈ transitions M›] inputs_as_list_set[of M]
using image_iff by fastforce
ultimately have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) ≠ []"
unfolding List.map_filter_def
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
then have **: "?res ∈ set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
unfolding * using hd_in_set by simp

obtain xR yR where "(xR,yR) ∈ set (List.product(inputs_as_list M) (outputs_as_list M))"
and res: "f (xR,yR) = Some ?res"
using map_filter_elem[OF **]
by (metis prod.exhaust_sel)

have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
using res f1
by (metis option.distinct(1) option.sel)
then have p2: "⋀ q1' q2' . h_obs M q1 xR yR = Some q1' ⟹ h_obs M q2 xR yR = Some q2' ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
using res f1 f2 by auto
have p3: "h_obs M q1 xR yR ≠ None ∨ h_obs M q2 xR yR ≠ None"
using res f3 by blast
show ?thesis using that p1 p2 p3 by blast
qed
qed

subsection ‹Assembling Distinguishing Traces›

(* assembles a distinguishing sequence for q1 and q2 that reside in distinct classes in the
(k+1)-th table by recursively appending IO pairs that distinguish the current states
or lead to distinct classes in the next lower table *)
fun assemble_distinguishing_sequence_from_ofsm_table :: "('a,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) list" where
"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 = []" |
"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (case
select_diverging_ofsm_table_io M q1 q2 (Suc k)
of
((x,y),(Some q1',Some q2')) ⇒ (x,y) # (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) |
((x,y),_)                   ⇒ [(x,y)])"

lemma assemble_distinguishing_sequence_from_ofsm_table_distinguishes :
assumes "observable M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2"
shows "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∈ LS M q1 ∪ LS M q2"
and   "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∉ LS M q1 ∩ LS M q2"
and   "butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) ∈ LS M q1 ∩ LS M q2"
proof -
have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∈ LS M q1 ∪ LS M q2
∧ assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∉ LS M q1 ∩ LS M q2
∧ butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) ∈ LS M q1 ∩ LS M q2"
using assms(2,3,4)
proof (induction k arbitrary: q1 q2)
case 0
then show ?case by auto
next
case (Suc k)

obtain x y where s1: "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
and s2: "⋀ q1' q2' . h_obs M q1 x y = Some q1' ⟹ h_obs M q2 x y = Some q2' ⟹ ofsm_table M (λq . states M) k q1' ≠ ofsm_table M (λq . states M) k q2'"
and s3: "h_obs M q1 x y ≠ None ∨ h_obs M q2 x y ≠ None"
using select_diverging_ofsm_table_io_Some[OF assms(1) Suc.prems]
by blast

consider (a) "h_obs M q1 x y = None ∧ h_obs M q2 x y ≠ None" |
(b) "h_obs M q1 x y ≠ None ∧ h_obs M q2 x y = None" |
(c) "h_obs M q1 x y ≠ None ∧ h_obs M q2 x y ≠ None"
using s3 by blast
then show ?case proof cases
case a
then obtain q2' where "h_obs M q1 x y = None" and "h_obs M q2 x y = Some q2'"
by blast
then have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(None, Some q2'))"
using s1 by auto
then have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
by auto

have "[(x,y)] ∈ LS M q1 ∪ LS M q2"
using ‹h_obs M q2 x y = Some q2'› LS_single_transition[of x y M]
by (metis UnI2 h_obs_None[OF ‹observable M›] a fst_conv snd_conv)
moreover have "[(x,y)] ∉ LS M q1 ∩ LS M q2"
using ‹h_obs M q1 x y = None› LS_single_transition[of x y M]
unfolding h_obs_None[OF ‹observable M›] by force
moreover have "butlast [(x,y)] ∈ LS M q1 ∩ LS M q2"
using Suc.prems(1,2) by auto
ultimately show ?thesis
unfolding * by simp
next
case b
then obtain q1' where "h_obs M q2 x y = None" and "h_obs M q1 x y = Some q1'"
by blast
then have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(Some q1',None))"
using s1 by auto
then have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
by auto

have "[(x,y)] ∈ LS M q1 ∪ LS M q2"
using ‹h_obs M q1 x y = Some q1'› LS_single_transition[of x y M]
by (metis UnI1 assms(1) b fst_conv h_obs_None snd_conv)
moreover have "[(x,y)] ∉ LS M q1 ∩ LS M q2"
using ‹h_obs M q2 x y = None› LS_single_transition[of x y M]
unfolding h_obs_None[OF ‹observable M›] by force
moreover have "butlast [(x,y)] ∈ LS M q1 ∩ LS M q2"
using Suc.prems(1,2) by auto
ultimately show ?thesis
unfolding * by simp
next
case c
then obtain q1' q2' where "h_obs M q1 x y = Some q1'" and "h_obs M q2 x y = Some q2'"
by blast
then have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(Some q1', Some q2'))"
using s1 by auto
then have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x,y) # (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k)"
by auto
moreover define subseq where subseq: "subseq = (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k)"
ultimately have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x,y) # subseq"
by auto

have "(q1,x,y,q1') ∈ transitions M"
using ‹h_obs M q1 x y = Some q1'› h_obs_Some[OF ‹observable M›] by blast
then have "q1' ∈ states M"
using fsm_transition_target by auto
have "(q2,x,y,q2') ∈ transitions M"
using ‹h_obs M q2 x y = Some q2'› h_obs_Some[OF ‹observable M›] by blast
then have "q2' ∈ states M"
using fsm_transition_target by auto

have i1: "subseq ∈ LS M q1' ∪ LS M q2'"
and  i2: "subseq ∉ LS M q1' ∩ LS M q2'"
and  i3: "butlast subseq ∈ LS M q1' ∩ LS M q2'"
using Suc.IH[OF ‹q1' ∈ states M› ‹q2' ∈ states M› s2[OF ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'›]]
unfolding subseq by blast+

have "(x,y) # subseq ∈ LS M q1 ∪ LS M q2"
using i1 ‹(q1,x,y,q1') ∈ transitions M› ‹(q2,x,y,q2') ∈ transitions M›
by (metis LS_prepend_transition Un_iff fst_conv snd_conv)
moreover have "(x,y) # subseq ∉ LS M q1 ∩ LS M q2"
using observable_language_transition_target[OF ‹observable M› ‹(q1,x,y,q1') ∈ transitions M›, of subseq]
observable_language_transition_target[OF ‹observable M› ‹(q2,x,y,q2') ∈ transitions M›, of subseq]
i2
unfolding fst_conv snd_conv
by blast
moreover have "butlast ((x,y) # subseq) ∈ LS M q1 ∩ LS M q2"
using i3 ‹(q1,x,y,q1') ∈ transitions M› ‹(q2,x,y,q2') ∈ transitions M›
by (metis Int_iff LS_prepend_transition LS_single_transition append_butlast_last_id butlast.simps(2) fst_conv language_prefix snd_conv)
ultimately show ?thesis
unfolding * by simp
qed
qed

then show "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∈ LS M q1 ∪ LS M q2"
and  "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k ∉ LS M q1 ∩ LS M q2"
and  "butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) ∈ LS M q1 ∩ LS M q2"
by blast+
qed

lemma assemble_distinguishing_sequence_from_ofsm_table_length :
"length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) ≤ k"
proof (induction k arbitrary: q1 q2)
case 0
then show ?case by auto
next
case (Suc k)
obtain x y A B where *:"select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),A,B)"
using prod.exhaust by metis

show ?case proof (cases A)
case None
then have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * case_prod_conv by auto
then show ?thesis
by (metis Suc_le_length_iff length_Cons list.distinct(1) not_less_eq_eq)
next
case (Some q1')
show ?thesis proof (cases B)
case None
then have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * case_prod_conv Some by auto
then show ?thesis
by (metis Suc_le_length_iff length_Cons list.distinct(1) not_less_eq_eq)
next
case (Some q2')
show ?thesis
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * ‹A = Some q1'› Some case_prod_conv
using Suc.IH[of q1' q2']
by simp
qed
qed
qed

lemma ofsm_table_fix_partition_fixpoint_trivial_partition :
assumes "q ∈ states M"
shows "ofsm_table_fix M (λq. FSM.states M) 0 q = ofsm_table M (λq. FSM.states M) (size M - 1) q"
proof -
have "((λq. FSM.states M) ` FSM.states M) = {states M}"
using fsm_initial[of M]
by auto
then have *:"card ((λq. FSM.states M) ` FSM.states M) = 1"
by auto

show ?thesis
using ofsm_table_fix_partition_fixpoint[OF minimise_initial_partition _ assms, of "size M"]
unfolding *
by blast
qed

fun get_distinguishing_sequence_from_ofsm_tables :: "('a,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ ('b × 'c) list" where
"get_distinguishing_sequence_from_ofsm_tables M q1 q2 = (let
k = find_first_distinct_ofsm_table M q1 q2
in assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k)"

lemma get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace :
assumes "observable M"
and     "minimal M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
shows "get_distinguishing_sequence_from_ofsm_tables M q1 q2 ∈ LS M q1 ∪ LS M q2"
and   "get_distinguishing_sequence_from_ofsm_tables M q1 q2 ∉ LS M q1 ∩ LS M q2"
and   "butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) ∈ LS M q1 ∩ LS M q2"
proof -
have "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
using ‹minimal M› unfolding minimal_observable_code[OF assms(1)]
using assms(3,4,5) by blast

let ?k = "find_first_distinct_ofsm_table_gt M q1 q2 0"
have "ofsm_table M (λq . states M) ?k q1 ≠ ofsm_table M (λq . states M) ?k q2"
using find_first_distinct_ofsm_table_is_first(1)[OF assms(3,4) ‹ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2›] .

have *:"get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 ?k"
by auto

show "get_distinguishing_sequence_from_ofsm_tables M q1 q2 ∈ LS M q1 ∪ LS M q2"
and  "get_distinguishing_sequence_from_ofsm_tables M q1 q2 ∉ LS M q1 ∩ LS M q2"
and  "butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) ∈ LS M q1 ∩ LS M q2"
using assemble_distinguishing_sequence_from_ofsm_table_distinguishes[OF assms(1,3,4) ‹ofsm_table M (λq . states M) ?k q1 ≠ ofsm_table M (λq . states M) ?k q2›]
unfolding *
by blast+
qed

lemma get_distinguishing_sequence_from_ofsm_tables_distinguishes :
assumes "observable M"
and     "minimal M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
shows "distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)"
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms]
unfolding distinguishes_def
by blast

subsection ‹Minimal Distinguishing Traces›

lemma get_distinguishing_sequence_from_ofsm_tables_is_minimally_distinguishing :
fixes M :: "('a,'b::linorder,'c::linorder) fsm"
assumes "observable M"
and     "minimal M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
shows "minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)"
proof -

have *:"ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
using ‹minimal M› unfolding minimal_observable_code[OF assms(1)]
using assms(3,4,5) by blast

obtain k where "k = find_first_distinct_ofsm_table M q1 q2"
and "get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k"
by auto
then have "length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) ≤ k"
using assemble_distinguishing_sequence_from_ofsm_table_length
by metis
moreover have "⋀ io . length io < k ⟹ ¬distinguishes M q1 q2 io"
proof -
fix io :: "('b × 'c) list"
assume "length io < k"
then have "ofsm_table M (λq. FSM.states M) (length io) q1 = ofsm_table M (λq. FSM.states M) (length io) q2"
using find_first_distinct_ofsm_table_is_first[OF assms(3,4) *]
unfolding ‹k = find_first_distinct_ofsm_table M q1 q2›
by blast
then show "¬distinguishes M q1 q2 io"
using ofsm_table_set_observable[OF assms(1,3) minimise_initial_partition]
using ofsm_table_set_observable[OF assms(1,4) minimise_initial_partition]
unfolding distinguishes_def
by (metis (mono_tags, lifting) Int_iff Un_iff assms(3) le_refl mem_Collect_eq ofsm_table_containment)
qed
ultimately show ?thesis
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms]
unfolding minimally_distinguishes_def distinguishes_def
using le_neq_implies_less not_le_imp_less
by blast
qed

lemma minimally_distinguishes_length :
assumes "observable M"
and     "minimal M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "q1 ≠ q2"
and     "minimally_distinguishes M q1 q2 io"
shows "length io ≤ size M - 1"
proof -

have "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
using ‹minimal M› unfolding minimal_observable_code[OF assms(1)]
using assms(3,4,5) by blast
then have "ofsm_table M (λq. FSM.states M) (FSM.size M - 1) q1 ≠ ofsm_table M (λq. FSM.states M) (FSM.size M - 1) q2"
using ofsm_table_fix_partition_fixpoint_trivial_partition assms(3,4)
by metis
then obtain io' where "distinguishes M q1 q2 io'" and "length io' ≤ size M - 1"
unfolding ofsm_table_set_observable[OF assms(1,3) minimise_initial_partition]
unfolding ofsm_table_set_observable[OF assms(1,4) minimise_initial_partition]
unfolding distinguishes_def
by blast
then show ?thesis
using assms(6) unfolding minimally_distinguishes_def
using dual_order.trans by blast
qed

end```