# Theory Pair_Framework

```section ‹Pair-Framework›

text ‹This theory defines the Pair-Framework and provides completeness properties.›

theory Pair_Framework
imports H_Framework
begin

subsection ‹Classical H-Condition›

definition satisfies_h_condition :: "('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b ×'c) list set ⇒ nat ⇒ bool" where
"satisfies_h_condition M V T m = (let
Π = (V ` reachable_states M);
n = card (reachable_states M);
𝒳 = λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M};
A = Π × Π;
B = Π × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q};
C = (⋃ q ∈ reachable_states M . ⋃ τ ∈ 𝒳 q . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ})
in
is_state_cover_assignment M V
∧ Π ⊆ T
∧ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T
∧ (∀ (α,β) ∈ A ∪ B ∪ C . α ∈ L M ⟶
β ∈ L M ⟶
after_initial M α ≠ after_initial M β ⟶
(∃ ω . α@ω ∈ T ∧
β@ω ∈ T ∧
distinguishes M (after_initial M α) (after_initial M β) ω)))"

lemma h_condition_satisfies_abstract_h_condition :
assumes "observable M"
and     "observable I"
and     "minimal M"
and     "size I ≤ m"
and     "m ≥ size_r M"
and     "inputs I = inputs M"
and     "outputs I = outputs M"
and     "satisfies_h_condition M V T m"
and     "(L M ∩ T = L I ∩ T)"
shows "satisfies_abstract_h_condition M I V m"
proof -

define Π where Π: "Π = (V ` reachable_states M)"
define n where n: "n = size_r M"
define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M})"
define A where A: "A = Π × Π"
define B where B: "B = Π × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
define C where C: "C = (⋃ q ∈ reachable_states M . ⋃ τ ∈ 𝒳 q . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ})"

have "satisfies_h_condition M V T m = (is_state_cover_assignment M V
∧ Π ⊆ T
∧ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T
∧ (∀ (α,β) ∈ A ∪ B ∪ C . α ∈ L M ⟶
β ∈ L M ⟶
after_initial M α ≠ after_initial M β ⟶
(∃ ω . α@ω ∈ T ∧
β@ω ∈ T ∧
distinguishes M (after_initial M α) (after_initial M β) ω)))"
unfolding satisfies_h_condition_def Let_def Π n 𝒳 A B C
by auto

then have "is_state_cover_assignment M V"
and "Π ⊆ T"
and "{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T"
and distinguishing_tests: "⋀ α β . (α,β) ∈ A ∪ B ∪ C ⟹
α ∈ L M ⟹
β ∈ L M ⟹
after_initial M α ≠ after_initial M β ⟹
(∃ ω . α@ω ∈ T ∧
β@ω ∈ T ∧
distinguishes M (after_initial M α) (after_initial M β) ω)"
using ‹satisfies_h_condition M V T m› by blast+

have "Π ⊆ L I" and "Π ⊆ L M"
using ‹Π ⊆ T› ‹Π = (V ` reachable_states M)› ‹L M ∩ T = L I ∩ T›
state_cover_assignment_language[OF ‹is_state_cover_assignment M V›] by blast+

have "(⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-size_r M) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹  (L M ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) = L I ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})) ∧ (preserves_divergence M I (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))) ⟹
satisfies_abstract_h_condition M I V m"
unfolding satisfies_abstract_h_condition_def Let_def
by blast
moreover have "(⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-size_r M) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹  (L M ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) = L I ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})) ∧ (preserves_divergence M I (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})))"
proof -
fix q γ
assume a1: "q ∈ reachable_states M"
and a2: "length γ ≤ Suc (m-size_r M)"
and a3: "list.set γ ⊆ inputs M × outputs M"
and a4: "butlast γ ∈ LS M q"

have "{V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ⊆ {V q} ∪ {V q @ τ | τ. τ ∈ 𝒳 q}"
proof
fix v assume "v ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)}"
then obtain w where "v = V q @ w" and "w ∈ list.set (prefixes γ)"
by blast

show "v ∈ {V q} ∪ {V q @ τ | τ. τ ∈ 𝒳 q}"
proof (cases w rule: rev_cases)
case Nil
show ?thesis unfolding ‹v = V q @ w› Nil Π using a1 by auto
next
case (snoc w' xy)

obtain w'' where "γ = w'@[xy]@w''"
using ‹w ∈ list.set (prefixes γ)›
unfolding prefixes_set snoc by auto

obtain w''' x y where "γ = (w'@w''')@[(x,y)]"
proof (cases w'' rule: rev_cases)
case Nil
show ?thesis
using that[of "[]" "fst xy" "snd xy"]
unfolding ‹γ = w'@[xy]@w''› Nil by auto
next
case (snoc w''' xy')
show ?thesis
using that[of "[xy]@w'''" "fst xy'" "snd xy'"]
unfolding ‹γ = w'@[xy]@w''› snoc by auto
qed
then have "butlast γ = w'@w'''"
using butlast_snoc by metis

have "w' ∈ LS M q"
using a4 unfolding ‹v = V q @ w› ‹butlast γ = w'@w'''›
using language_prefix by metis
moreover have "length w' ≤ m - size_r M"
using a2 unfolding ‹v = V q @ w› ‹γ = (w'@w''')@[(x,y)]› by auto
moreover have "fst xy ∈ FSM.inputs M ∧ snd xy ∈ FSM.outputs M"
using a3 unfolding ‹v = V q @ w› ‹γ = w'@[xy]@w''› by auto
ultimately have "w'@[(fst xy, snd xy)] ∈ 𝒳 q"
unfolding snoc 𝒳 n by blast
then have "w ∈ 𝒳 q"
unfolding snoc by auto
then show ?thesis
unfolding ‹v = V q @ w› using a1 by blast
qed
qed

have "preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
proof -
have "⋀ α β . α ∈ L M ⟹ α ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ⟹ β ∈ L M ⟹ β ∈  (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ⟹
¬ converge M α β ⟹ ¬ converge I α β"
proof -
fix α β
assume "α ∈ L M"
and "α ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
and "β ∈ L M"
and "β ∈  (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
and "¬ converge M α β"
then have "after_initial M α ≠ after_initial M β"
by auto
then have "α ≠ β"
by auto

obtain v w where "{v,w} = {α,β}" and *:"(v ∈ Π ∧ w ∈ Π)
∨ (v ∈ Π ∧ w ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})
∨ (v ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∧ w ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
using ‹α ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})›
‹β ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})›
by blast

from * consider "(v ∈ Π ∧ w ∈ Π)" |
"(v ∈ Π ∧ w ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})" |
"(v ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∧ w ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
by blast
then have "(v,w) ∈ A ∪ B ∪ C ∨ (w,v) ∈ A ∪ B ∪ C"
proof cases
case 1
then show ?thesis unfolding A by blast
next
case 2
then show ?thesis
using ‹{V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ⊆ {V q} ∪ {V q @ τ | τ. τ ∈ 𝒳 q}› a1
unfolding A B Π
by blast
next
case 3

then obtain io io' where "v = V q @ io" and "io ∈ list.set (prefixes γ)"
and "w = V q @ io'" and "io' ∈ list.set (prefixes γ)"
by auto

have "v ≠ w"
using ‹{v,w} = {α,β}› ‹α ≠ β› by force
then have "length io ≠ length io'"
using ‹io ∈ list.set (prefixes γ)› ‹io' ∈ list.set (prefixes γ)›
unfolding ‹v = V q @ io› ‹w = V q @ io'› prefixes_set
by force

have "io ∈ list.set (prefixes io') ∨ io' ∈ list.set (prefixes io)"
using prefixes_prefixes[OF ‹io ∈ list.set (prefixes γ)› ‹io' ∈ list.set (prefixes γ)›] .
then obtain u u' where "{u,u@u'} = {io,io'}"
and "u ∈ list.set (prefixes (u@u'))"
unfolding prefixes_set by auto

have "(u,u@u') = (io,io') ∨ (u,u@u') = (io',io)"
using ‹{u,u@u'} = {io,io'}›
by (metis empty_iff insert_iff)

have "u ≠ u@u'"
using ‹length io ≠ length io'› ‹{u,u@u'} = {io,io'}› by force
then have "u@u' ≠ []"
by auto
moreover have "⋀ w . w ≠ [] ⟹ w ∈ list.set (prefixes γ) ⟹ w ∈ 𝒳 q"
using ‹{V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ⊆ {V q} ∪ {V q @ τ | τ. τ ∈ 𝒳 q}›
by auto
moreover have "u@u' ∈ list.set (prefixes γ)"
using ‹(u,u@u') = (io,io') ∨ (u,u@u') = (io',io)› ‹io ∈ list.set (prefixes γ)› ‹io' ∈ list.set (prefixes γ)› by auto
ultimately have "u@u' ∈ 𝒳 q"
by blast
then have "(V q @ u, V q @ (u@u')) ∈ C"
unfolding C
using a1 ‹u ∈ list.set (prefixes (u@u'))› by blast
moreover have "(V q @ u, V q @ (u@u')) ∈ {(v,w), (w,v)}"
unfolding ‹v = V q @ io› ‹w = V q @ io'›
using ‹(u,u@u') = (io,io') ∨ (u,u@u') = (io',io)› by auto
ultimately show ?thesis
by blast
qed
moreover have "(α,β) = (v,w) ∨ (α,β) = (w,v)"
using ‹{v,w} = {α,β}›
by (metis empty_iff insert_iff)
ultimately consider "(α,β) ∈ A ∪ B ∪ C" | "(β,α) ∈ A ∪ B ∪ C"
by blast

then obtain ω where "α@ω ∈ T" and "β@ω ∈ T" and "distinguishes M (after_initial M α) (after_initial M β) ω"
using distinguishing_tests[OF _ ‹α ∈ L M› ‹β ∈ L M› ‹after_initial M α ≠ after_initial M β›]
using distinguishing_tests[OF _ ‹β ∈ L M› ‹α ∈ L M› ] ‹after_initial M α ≠ after_initial M β›
by (metis distinguishes_sym)

show "¬ converge I α β"
using distinguish_diverge[OF assms(1,2) ‹distinguishes M (after_initial M α) (after_initial M β) ω› ‹α@ω ∈ T› ‹β@ω ∈ T› ‹α ∈ L M› ‹β ∈ L M› assms(9)] .
qed
then show ?thesis
unfolding preserves_divergence.simps by blast
qed

moreover have "(L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
proof -
have "L M ∩ Π = L I ∩ Π"
using ‹Π ⊆ L I› ‹Π ⊆ L M›
by blast
moreover have "L M ∩ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} = L I ∩ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
using ‹{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T›
using assms(9)
by blast
ultimately have *:"L M ∩ (Π ∪ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}) = L I ∩ (Π ∪ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q})"
by blast
have **:"(Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) ⊆ Π ∪ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
using ‹{V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ⊆ {V q} ∪ {V q @ τ | τ. τ ∈ 𝒳 q}›
using a1 unfolding Π by blast

have scheme: "⋀ A B C D . A ∩ C = B ∩ C ⟹ D ⊆ C ⟹ A ∩ D = B ∩ D"
by (metis (no_types, opaque_lifting) Int_absorb1 inf_assoc)
show ?thesis
using scheme[OF * **] .
qed

ultimately show "(L M ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) = L I ∩ (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})) ∧ (preserves_divergence M I (V ` reachable_states M ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
unfolding Π by blast
qed
ultimately show ?thesis
by blast
qed

lemma h_condition_completeness :
assumes "observable M"
and     "observable I"
and     "minimal M"
and     "size I ≤ m"
and     "m ≥ size_r M"
and     "inputs I = inputs M"
and     "outputs I = outputs M"
and     "satisfies_h_condition M V T m"
shows "(L M = L I) ⟷ (L M ∩ T = L I ∩ T)"
proof -
have "is_state_cover_assignment M V" using assms(8) unfolding satisfies_h_condition_def Let_def by blast
then show ?thesis
using h_condition_satisfies_abstract_h_condition[OF assms]
using abstract_h_condition_completeness[OF assms(1-7)]
by blast
qed

subsection ‹Helper Functions›

fun language_up_to_length_with_extensions :: "'a ⇒ ('a ⇒ 'b ⇒ (('c×'a) list)) ⇒ 'b list ⇒ ('b×'c) list list ⇒ nat ⇒ ('b ×'c) list list"
where
"language_up_to_length_with_extensions q hM iM ex 0 = ex" |
"language_up_to_length_with_extensions q hM iM ex (Suc k) =
ex @ concat (map (λx .concat (map (λ(y,q') . (map (λp . (x,y) # p)
(language_up_to_length_with_extensions q' hM iM ex k)))
(hM q x)))
iM)"

lemma language_up_to_length_with_extensions_set :
assumes "q ∈ states M"
shows "List.set (language_up_to_length_with_extensions q (λ q x . sorted_list_of_set (h M (q,x))) (inputs_as_list M) ex k)
= {io@xy | io xy . io ∈ LS M q ∧ length io ≤ k ∧ xy ∈ List.set ex}"
(is "?S1 q k = ?S2 q k")
proof
let ?hM = "(λ q x . sorted_list_of_set (h M (q,x)))"
let ?iM = "inputs_as_list M"

show "?S1 q k ⊆ ?S2 q k"
proof
fix io assume "io ∈ ?S1 q k"
then show "io ∈ ?S2 q k"
using assms proof (induction k arbitrary: q io)
case 0
then obtain xy where "io = []@xy"
and "xy ∈ List.set ex"
and "[] ∈ LS M q"
by auto
then show ?case by force
next
case (Suc k)

show ?case proof (cases "io ∈ List.set ex")
case True
then have "io = []@io"
and "io ∈ List.set ex"
and "[] ∈ LS M q"
using Suc.prems(2) by auto
then show ?thesis by force
next
case False
then obtain x where "x ∈ List.set ?iM"
and *: "io ∈ List.set (concat (map (λ(y,q') . map (λp . (x,y) # p)
(language_up_to_length_with_extensions q' ?hM ?iM ex k))
(?hM q x)))"
using Suc.prems(1)
unfolding language_up_to_length_with_extensions.simps
by fastforce

have "x ∈ inputs M"
using ‹x ∈ List.set ?iM› inputs_as_list_set by auto

obtain yq' where "(yq') ∈ List.set (?hM q x)"
and "io ∈ List.set ((λ(y,q') . (map (λp . (x,y) # p)
(language_up_to_length_with_extensions q' ?hM ?iM ex k))) yq')"
using concat_map_elem[OF *] by blast
moreover obtain y q' where "yq' = (y,q')"
using prod.exhaust_sel by blast
ultimately have "(y,q') ∈ List.set (?hM q x)"
and "io ∈ List.set ((map (λp . (x,y) # p) (language_up_to_length_with_extensions q' ?hM ?iM ex k)))"
by auto

have "(y,q') ∈ h M (q,x)"
using ‹(y,q') ∈ List.set (?hM q x)›
by (metis empty_iff empty_set sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
then have "q' ∈ states M"
and "y ∈ outputs M"
and "(q,x,y,q') ∈ transitions M"
unfolding h_simps using fsm_transition_target fsm_transition_output by auto

obtain p where "io = (x,y) # p"
and "p ∈ List.set (language_up_to_length_with_extensions q' ?hM ?iM ex k)"
using ‹io ∈ List.set ((map (λp . (x,y) # p) (language_up_to_length_with_extensions q' ?hM ?iM ex k)))›
by force
then have "p ∈ {io @ xy |io xy. io ∈ LS M q' ∧ length io ≤ k ∧ xy ∈ list.set ex}"
using Suc.IH[OF _ ‹q' ∈ states M›]
by auto
then obtain ioP xy where "p = ioP@xy"
and "ioP ∈ LS M q'"
and "length ioP ≤ k"
and "xy ∈ list.set ex"
by blast

have "io = ((x,y)#ioP)@xy"
using ‹io = (x,y) # p› ‹p = ioP@xy› by auto
moreover have "((x,y)#ioP) ∈ LS M q"
using LS_prepend_transition[OF ‹(q,x,y,q') ∈ transitions M›] ‹ioP ∈ LS M q'›
by auto
moreover have "length ((x,y)#ioP) ≤ Suc k"
using ‹length ioP ≤ k›
by simp
ultimately show ?thesis
using ‹xy ∈ list.set ex› by blast
qed
qed
qed

show "?S2 q k ⊆ ?S1 q k"
proof
fix io' assume "io' ∈ ?S2 q k"
then show "io' ∈ ?S1 q k"
using assms proof (induction k arbitrary: q io')
case 0
then show ?case by auto
next
case (Suc k)

then obtain io xy where "io' = io@xy"
and "io ∈ LS M q"
and "length io ≤ Suc k"
and "xy ∈ list.set ex"
by blast

show ?case proof (cases io)
case Nil
then show ?thesis
using ‹io ∈ LS M q› ‹xy ∈ list.set ex›
unfolding ‹io' = io@xy›
by auto
next
case (Cons a io'')

obtain p where "path M q p" and "p_io p = io"
using ‹io ∈ LS M q› by auto
then obtain t p' where "p = t#p'"
using Cons
by blast

then have "t ∈ transitions M"
and "t_source t = q"
and "path M (t_target t) p'"
using ‹path M q p› by auto

have "a = (t_input t, t_output t)"
and "p_io p' = io''"
using ‹p_io p = io› Cons ‹p = t#p'›
by auto

have "io'' ∈ LS M (t_target t)"
using ‹p_io p' = io''› ‹path M (t_target t) p'› by auto
moreover have "length io'' ≤ k"
using ‹length io ≤ Suc k› Cons by auto
ultimately have "io''@xy ∈ {io @ xy |io xy. io ∈ LS M (t_target t) ∧ length io ≤ k ∧ xy ∈ list.set ex}"
using ‹xy ∈ list.set ex› by blast

moreover define f where f_def: "f = (λ q . (language_up_to_length_with_extensions q ?hM ?iM ex k))"
ultimately have "io''@xy ∈ list.set (f (t_target t))"
using Suc.IH[OF _ fsm_transition_target[OF ‹t ∈ transitions M›]]
by auto
moreover have "(t_output t, t_target t) ∈ list.set (?hM q (t_input t))"
proof -
have "(h M (q,t_input t)) ⊆ image (snd ∘ snd) (transitions M)"
unfolding h_simps by force
then have "finite (h M (q,t_input t))"
using fsm_transitions_finite
using finite_surj by blast
moreover have "(t_output t, t_target t) ∈ h M (q,t_input t)"
using ‹t ∈ transitions M› ‹t_source t = q›
by auto
ultimately show ?thesis
by simp
qed
ultimately have "a#(io''@xy) ∈ list.set (concat (map (λ(y,q') . (map (λp . ((t_input t),y) # p)
(f q')))
(?hM q (t_input t))))"
unfolding ‹a = (t_input t, t_output t)›
by force
moreover have "t_input t ∈ list.set ?iM"
using fsm_transition_input[OF ‹t ∈ transitions M›] inputs_as_list_set by auto
ultimately have "a#(io''@xy) ∈ list.set (concat (map (λx .concat (map (λ(y,q') . (map (λp . (x,y) # p)
(f q')))
(?hM q x)))
?iM))"
by force
then have "a#(io''@xy) ∈ ?S1 q (Suc k)"
unfolding language_up_to_length_with_extensions.simps
unfolding f_def by force
then show ?thesis
unfolding ‹io' = io@xy› Cons by simp
qed
qed
qed
qed

fun h_extensions :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ nat ⇒ ('b ×'c) list list" where
"h_extensions M q k = (let
iM = inputs_as_list M;
ex = map (λxy . [xy]) (List.product iM (outputs_as_list M));
hM = (λ q x . sorted_list_of_set (h M (q,x)))
in
language_up_to_length_with_extensions q hM iM ex k)"

lemma h_extensions_set :
assumes "q ∈ states M"
shows "List.set (h_extensions M q k) = {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ k ∧ x ∈ inputs M ∧ y ∈ outputs M}"
proof -

define ex where ex: "ex = map (λxy . [xy]) (List.product (inputs_as_list M) (outputs_as_list M))"
then have "List.set ex = {[xy] | xy . xy ∈ list.set (List.product (inputs_as_list M) (outputs_as_list M))}"
by auto
then have *: "List.set ex = {[(x,y)] | x y . x ∈ inputs M ∧ y ∈ outputs M}"
using inputs_as_list_set[of M] outputs_as_list_set[of M]
by auto

have "h_extensions M q k = language_up_to_length_with_extensions q (λ q x . sorted_list_of_set (h M (q,x))) (inputs_as_list M) ex k"
unfolding ex h_extensions.simps Let_def
by auto
then have "List.set (h_extensions M q k) = {io @ xy |io xy. io ∈ LS M q ∧ length io ≤ k ∧ xy ∈ list.set ex}"
using language_up_to_length_with_extensions_set[OF assms]
by auto
then show ?thesis
unfolding * by blast
qed

fun paths_up_to_length_with_targets :: "'a ⇒ ('a ⇒ 'b ⇒ (('a,'b,'c) transition list)) ⇒ 'b list ⇒ nat ⇒ (('a,'b,'c) path × 'a) list"
where
"paths_up_to_length_with_targets q hM iM 0 = [([],q)]" |
"paths_up_to_length_with_targets q hM iM (Suc k) =
([],q) # (concat (map (λx .concat (map (λt . (map (λ(p,q). (t # p,q))
(paths_up_to_length_with_targets (t_target t) hM iM k)))
(hM q x)))
iM))"

lemma paths_up_to_length_with_targets_set :
assumes "q ∈ states M"
shows "List.set (paths_up_to_length_with_targets q (λ q x . map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x)))) (inputs_as_list M) k)
= {(p, target q p) | p . path M q p ∧ length p ≤ k}"
(is "?S1 q k = ?S2 q k")
proof
let ?hM = "(λ q x . map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))"
let ?iM = "inputs_as_list M"

have hM: "⋀ q x . list.set (?hM q x) = {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
proof -
fix q x show "list.set (?hM q x) = {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
proof
show "list.set (?hM q x) ⊆ {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
proof
fix t assume "t ∈ list.set (?hM q x)"
then obtain y q' where "t = (q,x,y,q')" and "(y,q') ∈ list.set (sorted_list_of_set (h M (q,x)))"
by auto
then have "(y,q') ∈ h M (q,x)"
by (metis empty_iff empty_set sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
then show "t ∈ {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
unfolding h_simps ‹t = (q,x,y,q')› by blast
qed

show "{(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M} ⊆ list.set (?hM q x)"
proof
fix t assume "t ∈ {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
then obtain y q' where "t = (q,x,y,q')" and "(q,x,y,q') ∈ {(q,x,y,q') | y q' . (q,x,y,q') ∈ transitions M}"
by auto
then have "(y,q') ∈ h M (q,x)"
by auto

have "(h M (q,x)) ⊆ image (snd ∘ snd) (transitions M)"
unfolding h_simps by force
then have "finite (h M (q,x))"
using fsm_transitions_finite
using finite_surj by blast
then have "(y,q') ∈ list.set (sorted_list_of_set (h M (q,x)))"
using ‹(y,q') ∈ h M (q,x)› by auto
then show "t ∈ list.set (?hM q x)"
unfolding ‹t = (q,x,y,q')› by auto
qed
qed
qed

show "?S1 q k ⊆ ?S2 q k"
proof
fix pq assume "pq ∈ ?S1 q k"
then show "pq ∈ ?S2 q k"
using assms proof (induction k arbitrary: q pq)
case 0
then show ?case by force
next
case (Suc k)

obtain p q' where "pq = (p,q')"
by fastforce

show ?case proof (cases p)
case Nil
have "q' = q"
using Suc.prems(1)
unfolding ‹pq = (p,q')› Nil paths_up_to_length_with_targets.simps
by force
then show ?thesis
unfolding ‹pq = (p,q')› Nil using Suc.prems(2) by auto
next
case (Cons t p')

obtain x where "x ∈ list.set ?iM"
and *:"(t#p',q') ∈ list.set (concat (map (λt . (map (λ(p,q). (t # p,q))
(paths_up_to_length_with_targets (t_target t) ?hM ?iM k)))
(?hM q x)))"
using Suc.prems(1) unfolding ‹pq = (p,q')› Cons paths_up_to_length_with_targets.simps
by fastforce

have "x ∈ inputs M"
using ‹x ∈ List.set ?iM› inputs_as_list_set by auto

have "t ∈ list.set (?hM q x)"
and **:"(p',q') ∈ list.set (paths_up_to_length_with_targets (t_target t) ?hM ?iM k)"
using * by auto

have "t ∈ transitions M" and "t_source t = q"
using ‹t ∈ list.set (?hM q x)› hM by auto

have "q' = target (t_target t) p'"
and "path M (t_target t) p'"
and "length p' ≤ k"
using Suc.IH[OF ** fsm_transition_target[OF ‹t ∈ transitions M›]]
by auto

have "q' = target q p"
unfolding Cons using ‹q' = target (t_target t) p'› by auto
moreover have "path M q p"
unfolding Cons using ‹path M (t_target t) p'› ‹t ∈ transitions M› ‹t_source t = q› by auto
moreover have "length p ≤ Suc k"
unfolding Cons using ‹length p' ≤ k› by auto
ultimately show ?thesis
unfolding ‹pq = (p,q')› by blast
qed
qed
qed

show "?S2 q k ⊆ ?S1 q k"
proof
fix pq assume "pq ∈ ?S2 q k"

obtain p q' where "pq = (p,q')"
by fastforce

show "pq ∈ ?S1 q k"
using assms ‹pq ∈ ?S2 q k› unfolding ‹pq = (p,q')› proof (induction k arbitrary: q p q')
case 0
then show ?case by force
next
case (Suc k)
then have "q' = target q p"
and "path M q p"
and "length p ≤ Suc k"
by auto

show ?case proof (cases p)
case Nil
then have "q' = q"
using Suc.prems(2) by auto
then show ?thesis unfolding Nil by auto
next
case (Cons t p')

then have "q' = target q (t#p')"
and "path M q (t#p')"
and "length (t#p') ≤ Suc k"
using Suc.prems(2)
by auto

have "t ∈ transitions M" and "t_source t = q"
using ‹path M q (t#p')› by auto
then have "t ∈ list.set (?hM q (t_input t))"
unfolding hM
by (metis (mono_tags, lifting) mem_Collect_eq prod.exhaust_sel)

have "t_input t ∈ list.set ?iM"
using fsm_transition_input[OF ‹t ∈ transitions M›] inputs_as_list_set by auto

have "q' = target (t_target t) p'"
using ‹q' = target q (t#p')› by auto
moreover have "path M (t_target t) p'"
using ‹path M q (t#p')› by auto
moreover have "length p' ≤ k"
using ‹length (t#p') ≤ Suc k› by auto
ultimately have "(p',q') ∈ ?S2 (t_target t) k"
by blast
moreover define f where f_def: "f = (λq . (paths_up_to_length_with_targets q ?hM ?iM k))"
ultimately have "(p',q') ∈ list.set (f (t_target t))"
using Suc.IH[OF fsm_transition_target[OF ‹t ∈ transitions M›]]
by blast
then have **: "(t#p',q') ∈ list.set ((map (λ(p,q). (t # p,q)) (f (t_target t))))"
by auto

have scheme: "⋀ x y ys f . x ∈ list.set (f y) ⟹ y ∈ list.set ys ⟹ x ∈ list.set (concat (map f ys))"
by auto

have "(t#p',q') ∈ list.set (concat (map (λt . (map (λ(p,q). (t # p,q))
(f (t_target t))))
(?hM q (t_input t))))"
using scheme[of "(t#p',q')" "λ t. (map (λ(p,q). (t # p,q)) (f (t_target t)))", OF ** ‹t ∈ list.set (?hM q (t_input t))›]
.

then have "(t#p',q') ∈ list.set (concat
(map (λx. concat
(map (λt. map (λ(p, y). (t # p, y))
(f (t_target t)))
(map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))))
(inputs_as_list M)))"
using ‹t_input t ∈ list.set ?iM› by force

then show ?thesis
unfolding paths_up_to_length_with_targets.simps f_def Cons by auto
qed
qed
qed
qed

fun pairs_to_distinguish :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('a ⇒ (('a,'b,'c) path × 'a) list) ⇒ 'a list ⇒ ((('b × 'c) list × 'a) × (('b × 'c) list × 'a)) list" where
"pairs_to_distinguish M V 𝒳' rstates = (let
Π = map (λq . (V q,q)) rstates;
A = List.product Π Π;
B = List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates));
C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates)
in
filter (λ((α,q'),(β,q'')) . q' ≠ q'') (A@B@C))"

lemma pairs_to_distinguish_elems :
assumes "observable M"
and     "is_state_cover_assignment M V"
and     "list.set rstates = reachable_states M"
and     "⋀ q p q' . q ∈ reachable_states M ⟹ (p,q') ∈ list.set (𝒳' q) ⟷ path M q p ∧ target q p = q' ∧ length p ≤ m-n+1"
and     "((α,q1),(β,q2)) ∈ list.set (pairs_to_distinguish M V 𝒳' rstates)"

shows "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
and "α ∈ L M" and "β ∈ L M" and "q1 = after_initial M α" and "q2 = after_initial M β"
proof -

define Π where Π: "Π = map (λq . (V q,q)) rstates"
moreover define A where A: "A = List.product Π Π"
moreover define B where B: "B = List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
moreover define C where C: "C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates)"
ultimately have pairs_def: "pairs_to_distinguish M V 𝒳' rstates = filter (λ((α,q'),(β,q'')) . q' ≠ q'') (A@B@C)"
unfolding pairs_to_distinguish.simps Let_def by force

show "q1 ≠ q2"
using assms(5) unfolding pairs_def by auto

consider "((α,q1),(β,q2)) ∈ list.set A" | "((α,q1),(β,q2)) ∈ list.set B" | "((α,q1),(β,q2)) ∈ list.set C"
using assms(5) unfolding pairs_def by auto
then have "q1 ∈ states M ∧ q2 ∈ states M ∧ α ∈ L M ∧ β ∈ L M ∧ q1 = after_initial M α ∧ q2 = after_initial M β"
proof cases
case 1
then have "(α,q1) ∈ list.set Π" and "(β,q2) ∈ list.set Π"
unfolding A by auto
then show ?thesis unfolding Π using assms(3)
using reachable_state_is_state
using state_cover_assignment_after[OF assms(1,2)]
by force
next
case 2
then have "(α,q1) ∈ list.set Π" and "(β,q2) ∈ list.set (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
unfolding B by auto

then obtain q where "q ∈ reachable_states M"
and "(β,q2) ∈ list.set (map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q))"
unfolding assms(3)[symmetric] by (meson concat_map_elem)
then obtain τ where "(τ,q2) ∈ list.set (𝒳' q)" and "β = (V q)@ p_io τ"
by force
then have "path M q τ" and "target q τ = q2"
unfolding assms(4)[OF ‹q ∈ reachable_states M›] by auto
moreover obtain p where "path M (initial M) p" and "p_io p = V q" and "target (initial M) p = q"
using state_cover_assignment_after[OF assms(1,2) ‹q ∈ reachable_states M›]
after_path[OF assms(1)]
by auto
ultimately have "path M (initial M) (p@τ)" and "target (initial M) (p@τ) = q2" and "p_io (p@τ) = β"
unfolding ‹β = (V q)@ p_io τ› by auto
then have "q2 = after_initial M β"
by (metis (mono_tags, lifting) after_path assms(1))
moreover have "β ∈ L M"
using ‹path M (initial M) (p@τ)› ‹p_io (p@τ) = β›
by (metis (mono_tags, lifting) language_state_containment)
moreover have "q2 ∈ states M"
by (metis ‹path M q τ› ‹target q τ = q2› path_target_is_state)
moreover have "q1 ∈ states M"
using ‹(α,q1) ∈ list.set Π› assms(3) reachable_state_is_state unfolding Π by fastforce
moreover have "α ∈ L M" and "q1 = after_initial M α"
using ‹(α,q1) ∈ list.set Π› assms(3) state_cover_assignment_after[OF assms(1,2)] unfolding Π by auto
ultimately show ?thesis
by blast
next
case 3
then obtain q where "q ∈ reachable_states M"
and "((α,q1),(β,q2)) ∈ list.set  (concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))"
unfolding assms(3)[symmetric] C by force
then obtain τ' where "(τ',q2) ∈ list.set (𝒳' q)" and "β = V q @ p_io τ'"
and "((α,q1),(β,q2)) ∈ list.set (map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q2))) (prefixes τ'))"
by force
then obtain τ'' where "τ'' ∈ list.set (prefixes τ')" and "α = V q @ p_io τ''"
and "((α,q1),(β,q2)) = (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q2))"
by auto
then have "q1 = target q τ''"
by auto

have "path M q τ'" and "target q τ' = q2"
using ‹(τ',q2) ∈ list.set (𝒳' q)› unfolding assms(4)[OF ‹q ∈ reachable_states M›] by simp+
then have "path M q τ''"
using ‹τ'' ∈ list.set (prefixes τ')›
using prefixes_set_ob by force
then have "q1 ∈ states M"
using path_target_is_state unfolding ‹q1 = target q τ''› by force
moreover have "α ∈ L M"
unfolding ‹α = V q @ p_io τ''›
using state_cover_assignment_after[OF assms(1,2)]
by (metis (mono_tags, lifting) ‹path M q τ''› ‹q ∈ reachable_states M› assms(1) language_state_containment observable_after_language_append)
moreover have "q1 = after_initial M α"
unfolding ‹α = V q @ p_io τ''›
using state_cover_assignment_after[OF assms(1,2) ‹q ∈ reachable_states M›]
by (metis (mono_tags, lifting) ‹α = V q @ p_io τ''› ‹path M q τ''›  ‹q1 = target q τ''› after_path after_split assms(1) calculation(2))
moreover have "q2 ∈ states M"
using ‹path M q τ'› ‹target q τ' = q2› path_target_is_state by force
moreover have "β ∈ L M"
by (metis (mono_tags, lifting) ‹α = V q @ p_io τ''› ‹β = V q @ p_io τ'› ‹path M q τ'› ‹q ∈ reachable_states M› assms(1) assms(2) calculation(2) is_state_cover_assignment_observable_after language_prefix language_state_containment observable_after_language_append)
moreover have "q2 = after_initial M β"
unfolding ‹β = V q @ p_io τ'›
using state_cover_assignment_after[OF assms(1,2) ‹q ∈ reachable_states M›]
by (metis (mono_tags, lifting) ‹β = V q @ p_io τ'› ‹path M q τ'› ‹target q τ' = q2› after_path after_split assms(1) calculation(5))
ultimately show ?thesis
by blast
qed
then show "q1 ∈ states M" and "q2 ∈ states M" and "α ∈ L M" and "β ∈ L M" and "q1 = after_initial M α" and "q2 = after_initial M β"
by auto
qed

lemma pairs_to_distinguish_containment :
assumes "observable M"
and     "is_state_cover_assignment M V"
and     "list.set rstates = reachable_states M"
and     "⋀ q p q' . q ∈ reachable_states M ⟹ (p,q') ∈ list.set (𝒳' q) ⟷ path M q p ∧ target q p = q' ∧ length p ≤ m-n+1"
and     "(α,β) ∈ (V ` reachable_states M) × (V ` reachable_states M)
∪ (V ` reachable_states M) × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M}}
∪ (⋃ q ∈ reachable_states M . ⋃ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M} . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ})"
and     "α ∈ L M"
and     "β ∈ L M"
and     "after_initial M α ≠ after_initial M β"
shows "((α,after_initial M α),(β,after_initial M β)) ∈ list.set (pairs_to_distinguish M V 𝒳' rstates)"
proof -

let ?𝒳 = "λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M}"

define Π where Π: "Π = map (λq . (V q,q)) rstates"
moreover define A where A: "A = List.product Π Π"
moreover define B where B: "B =List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
moreover define C where C: "C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates)"
ultimately have pairs_def: "pairs_to_distinguish M V 𝒳' rstates = filter (λ((α,q'),(β,q'')) . q' ≠ q'') (A@B@C)"
unfolding pairs_to_distinguish.simps Let_def by force

have V_target: "⋀q . q ∈ reachable_states M ⟹ after_initial M (V q) = q"
proof -
fix q assume "q ∈ reachable_states M"
then have "q ∈ io_targets M (V q) (initial M)"
using assms(2) by auto
then have "V q ∈ L M"
unfolding io_targets.simps
by force

show "after_initial M (V q) = q"
by (meson ‹q ∈ reachable_states M› assms(1) assms(2) is_state_cover_assignment_observable_after)
qed

have V_path: "⋀ io q . q ∈ reachable_states M ⟹ io ∈ LS M q ⟹ ∃ p . path M q p ∧ p_io p = io ∧ target q p = after_initial M ((V q)@io)"
proof -
fix io q assume "q ∈ reachable_states M" and "io ∈ LS M q"
then have "after_initial M (V q) = q"
using V_target by auto
then have "((V q)@io) ∈ L M"
using ‹io ∈ LS M q›
by (meson ‹q ∈ reachable_states M› assms(2) is_state_cover_assignment.simps language_io_target_append)
then obtain p where "path M (initial M) p" and "p_io p = ((V q)@io)"
by auto
moreover have "target (initial M) p ∈ io_targets M ((V q)@io) (initial M)"
using calculation unfolding io_targets.simps by force
ultimately have "target (initial M) p = after_initial M ((V q)@io)"
using observable_io_targets[OF ‹observable M› ‹((V q)@io) ∈ L M›]
unfolding io_targets.simps
by (metis (mono_tags, lifting) after_path assms(1))

have "path M (FSM.initial M) (take (length (V q)) p)"
and "p_io (take (length (V q)) p) = V q"
and "path M (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p)"
and "p_io (drop (length (V q)) p) = io"
using path_io_split[OF ‹path M (initial M) p› ‹p_io p = ((V q)@io)›]
by auto

have "target (initial M) p = target (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p)"
by (metis append_take_drop_id path_append_target)
moreover have "(target (FSM.initial M) (take (length (V q)) p)) = q"
using ‹p_io (take (length (V q)) p) = V q› ‹after_initial M (V q) = q›
using ‹path M (FSM.initial M) (take (length (V q)) p)› after_path assms(1) by fastforce
ultimately have "target q (drop (length (V q)) p) = after_initial M ((V q)@io)"
using ‹target (initial M) p = after_initial M ((V q)@io)›
by presburger
then show "∃ p . path M q p ∧ p_io p = io ∧ target q p = after_initial M ((V q)@io)"
using ‹path M (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p)› ‹p_io (drop (length (V q)) p) = io›
unfolding ‹(target (FSM.initial M) (take (length (V q)) p)) = q›
by blast
qed

consider "(α,β) ∈ (V ` reachable_states M) × (V ` reachable_states M)" |
"(α,β) ∈ (V ` reachable_states M) × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M}}" |
"(α,β) ∈ (⋃ q ∈ reachable_states M . ⋃ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M} . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ})"
using assms(5) by blast
then show ?thesis proof cases
case 1
then have "α ∈ V ` reachable_states M"
and "β ∈ V ` reachable_states M"
by auto

have "(α,after_initial M α) ∈ list.set (map (λq . (V q,q)) rstates)"
using ‹α ∈ V ` reachable_states M› V_target assms(3) by force
moreover have "(β,after_initial M β) ∈ list.set (map (λq . (V q,q)) rstates)"
using ‹β ∈ V ` reachable_states M› V_target assms(3) by force
ultimately have "((α,after_initial M α),(β,after_initial M β)) ∈ list.set A"
unfolding Π A by auto
then show ?thesis
using ‹after_initial M α ≠ after_initial M β›
unfolding pairs_def by auto
next
case 2
then have "α ∈ V ` reachable_states M"
and "β ∈ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M}}"
by auto

have "(α,after_initial M α) ∈ list.set (map (λq . (V q,q)) rstates)"
using ‹α ∈ V ` reachable_states M› V_target assms(3) by force

obtain q io x y where "β = (V q) @ (io@[(x,y)])"
and "q ∈ reachable_states M"
and "length io ≤ m-n"
using ‹β ∈ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M}}›
by blast

have "(V q) @ (io@[(x,y)]) ∈ L M"
using ‹β ∈ L M› unfolding ‹β = (V q) @ (io@[(x,y)])› by simp

have "q ∈ io_targets M (V q) (initial M)"
using ‹q ∈ reachable_states M› assms(2) by auto
then have "io@[(x,y)] ∈ LS M q"
unfolding ‹β = (V q) @ (io@[(x,y)])›
using observable_io_targets_language[OF ‹(V q) @ (io@[(x,y)]) ∈ L M› ‹observable M›]
by auto
then obtain p where "path M q p"
and "p_io p = io@[(x,y)]"
and "target q p = after_initial M β"
using V_path[OF ‹q ∈ reachable_states M›]
unfolding ‹β = (V q) @ (io@[(x,y)])›
by blast
moreover have "length p ≤ m-n+1"
using calculation ‹length io ≤ m-n›
by (metis (no_types, lifting) Suc_le_mono add.commute length_append_singleton length_map plus_1_eq_Suc)
ultimately have "(p,after_initial M β) ∈ list.set (𝒳' q)"
using assms(4)[OF ‹q ∈ reachable_states M›]
by auto
then have "(β,after_initial M β) ∈ list.set (map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q))"
unfolding ‹β = (V q) @ (io@[(x,y)])› using ‹p_io p = io@[(x,y)]› by force
moreover have "q ∈ list.set rstates"
using ‹q ∈ reachable_states M› assms(3) by auto
ultimately have "(β,after_initial M β) ∈ list.set (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
by force
then have "((α,after_initial M α),(β,after_initial M β)) ∈ list.set B"
using ‹(α,after_initial M α) ∈ list.set (map (λq . (V q,q)) rstates)›
unfolding B Π
by auto
then show ?thesis
using ‹after_initial M α ≠ after_initial M β›
unfolding pairs_def by auto
next
case 3
then obtain q τ' io x y where "q ∈ reachable_states M"
and "io ∈ LS M q"
and "length io ≤ m - n"
and "x ∈ FSM.inputs M"
and "y ∈ FSM.outputs M"
and "α = V q @ τ'"
and "τ' ∈ list.set (prefixes ( io @ [(x, y)]))"
and "β = V q @ io @ [(x, y)]"
by blast

have "(V q) @ (io@[(x,y)]) ∈ L M"
using ‹β ∈ L M› unfolding ‹β = (V q) @ (io@[(x,y)])› by simp

have "q ∈ io_targets M (V q) (initial M)"
using ‹q ∈ reachable_states M› assms(2) by auto
then have "io@[(x,y)] ∈ LS M q"
unfolding ‹β = (V q) @ (io@[(x,y)])›
using observable_io_targets_language[OF ‹(V q) @ (io@[(x,y)]) ∈ L M› ‹observable M›]
by auto
then obtain p where "path M q p"
and "p_io p = io@[(x,y)]"
and "target q p = after_initial M β"
using V_path[OF ‹q ∈ reachable_states M›]
unfolding ‹β = (V q) @ (io@[(x,y)])›
by blast
moreover have "length p ≤ m-n+1"
using calculation ‹length io ≤ m-n›
by (metis (no_types, lifting) Suc_le_mono add.commute length_append_singleton length_map plus_1_eq_Suc)
ultimately have "(p,after_initial M β) ∈ list.set (𝒳' q)"
using assms(4)[OF ‹q ∈ reachable_states M›]
by auto

have "q ∈ list.set rstates"
using ‹q ∈ reachable_states M› assms(3) by auto

let ?τ = "take (length τ') (io@[(x,y)])"
obtain τ'' where "io @ [(x, y)] = τ' @ τ''"
using ‹τ' ∈ list.set (prefixes ( io @ [(x, y)]))›
using prefixes_set_ob by blast
then have "τ' = ?τ"
by auto
then have "io@[(x,y)] = τ' @ (drop (length τ') (io@[(x,y)]))"
by (metis append_take_drop_id)
then have "p_io p = τ' @ (drop (length τ') (io@[(x,y)]))"
using ‹p_io p = io@[(x,y)]›
by simp

have "path M q (take (length τ') p)"
and "p_io (take (length τ') p) = τ'"
using path_io_split(1,2)[OF ‹path M q p› ‹p_io p = τ' @ (drop (length τ') (io@[(x,y)]))›]
by auto
then have "τ' ∈ LS M q"
using language_intro by fastforce

have "(V q) @ τ' ∈ L M"
using ‹(V q) @ (io@[(x,y)]) ∈ L M› unfolding ‹io @ [(x, y)] = τ' @ τ''›
using language_prefix[of "V q @ τ'" τ'' M "initial M"]
by auto

have "(FSM.after M (FSM.initial M) (V q)) = q"
using V_target ‹q ∈ reachable_states M› by blast
have "target q (take (length τ') p) = after_initial M α"
using observable_after_target[OF ‹observable M› ‹(V q) @ τ' ∈ L M› _ ‹p_io (take (length τ') p) = τ'›]
using ‹path M q (take (length τ') p)›
unfolding ‹(FSM.after M (FSM.initial M) (V q)) = q› ‹α = V q @ τ'›
by auto

have "p = (take (length τ') p)@(drop (length τ') p)"
by simp
then have "(take (length τ') p) ∈ list.set (prefixes p)"
unfolding prefixes_set
by (metis (mono_tags, lifting) mem_Collect_eq)

have "(((V q)@ p_io (take (length τ') p), target q (take (length τ') p)),((V q)@ p_io p,after_initial M β)) ∈ list.set ( (λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ')) (p,after_initial M β))"
using ‹(take (length τ') p) ∈ list.set (prefixes p)›
by auto
then have *: "((α, after_initial M α),(β,after_initial M β)) ∈ list.set ( (λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ')) (p,after_initial M β))"
unfolding ‹α = V q @ τ'›
‹β = V q @ io @ [(x, y)]›
‹target q (take (length τ') p) = after_initial M α›
‹p_io (take (length τ') p) = τ'›
‹p_io p = io@[(x,y)]› .

have scheme: "⋀ x y ys f . x ∈ list.set (f y) ⟹ y ∈ list.set ys ⟹ x ∈ list.set (concat (map f ys))"
by auto

have **: "((α, after_initial M α),(β,after_initial M β)) ∈ list.set (concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))"
using scheme[of _ "(λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ'))", OF * ‹(p,after_initial M β) ∈ list.set (𝒳' q)›]
.

have "((α, after_initial M α),(β,after_initial M β)) ∈ list.set C"
unfolding C
using scheme[of _ "(λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))", OF ** ‹q ∈ list.set rstates›]
.

then show ?thesis
using ‹after_initial M α ≠ after_initial M β›
unfolding pairs_def by auto
qed
qed

subsection ‹Definition of the Pair-Framework›

definition pair_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒
nat ⇒
(('a,'b,'c) fsm ⇒ nat ⇒ ('b×'c) prefix_tree) ⇒
(('a,'b,'c) fsm ⇒ nat ⇒ ((('b × 'c) list × 'a) × (('b × 'c) list × 'a)) list) ⇒
(('a,'b,'c) fsm ⇒ (('b × 'c) list × 'a) × ('b × 'c) list × 'a ⇒ ('b × 'c) prefix_tree ⇒ ('b × 'c) prefix_tree) ⇒
('b×'c) prefix_tree"
where
"pair_framework M m get_initial_test_suite get_pairs get_separating_traces =
(let
TS = get_initial_test_suite M m;
D  = get_pairs M m;
dist_extension = (λ t ((α,q'),(β,q'')) . let tDist = get_separating_traces M ((α,q'),(β,q'')) t
in combine_after (combine_after t α tDist) β tDist)
in
foldl dist_extension TS D)"

lemma pair_framework_completeness :
assumes "observable M"
and     "observable I"
and     "minimal M"
and     "size I ≤ m"
and     "m ≥ size_r M"
and     "inputs I = inputs M"
and     "outputs I = outputs M"
and     "is_state_cover_assignment M V"
and     "{(V q)@io@[(x,y)] | q io x y . q ∈ reachable_states M ∧ io ∈ LS M q ∧ length io ≤ m - size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} ⊆ set (get_initial_test_suite M m)"
and     "⋀ α β . (α,β) ∈ (V ` reachable_states M) × (V ` reachable_states M)
∪ (V ` reachable_states M) × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M}}
∪ (⋃ q ∈ reachable_states M . ⋃ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ}) ⟹
α ∈ L M ⟹ β ∈ L M ⟹ after_initial M α ≠ after_initial M β ⟹
((α,after_initial M α),(β,after_initial M β)) ∈ list.set (get_pairs M m)"
and     "⋀ α β t . α ∈ L M ⟹ β ∈ L M ⟹ after_initial M α ≠ after_initial M β ⟹ ∃ io ∈ set (get_separating_traces M ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
shows "(L M = L I) ⟷ (L M ∩ set (pair_framework M m get_initial_test_suite get_pairs get_separating_traces) = L I ∩ set (pair_framework M m get_initial_test_suite get_pairs get_separating_traces))"
proof (cases "inputs M = {} ∨ outputs M = {}")
case True (* handle case of empty input or outputs *)
then consider "inputs M = {}" | "outputs M = {}" by blast
then show ?thesis proof cases
case 1
have "L M = {[]}"
using "1" language_empty_IO by blast
moreover have "L I = {[]}"
by (metis "1" assms(6) language_empty_IO)
ultimately show ?thesis by blast
next
case 2
have "L M = {[]}"
using language_io(2)[of _ M "initial M"] unfolding 2
by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair)
moreover have "L I = {[]}"
using language_io(2)[of _ I "initial I"] unfolding 2 ‹outputs I = outputs M›
by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair)
ultimately show ?thesis by blast
qed
next
case False

define T where T: "T = get_initial_test_suite M m"
moreover define pairs where pairs: "pairs  = get_pairs M m"
moreover define distExtension where distExtension: "distExtension = (λ t ((α,q'),(β,q'')) . let tDist = get_separating_traces M ((α,q'),(β,q'')) t
in combine_after (combine_after t α tDist) β tDist)"
ultimately have res_def: "pair_framework M m get_initial_test_suite get_pairs get_separating_traces = foldl distExtension T pairs"
unfolding pair_framework_def Let_def by auto

define T' where T': "T' = set (foldl distExtension T pairs)"
then have T'r: "T' = set (foldr (λ x y . distExtension y x) (rev pairs) T)"

define Π where Π: "Π = (V ` reachable_states M)"
define n where n: "n = size_r M"
define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M})"
define A where A: "A = Π × Π"
define B where B: "B = Π × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
define C where C: "C = (⋃ q ∈ reachable_states M . ⋃ τ ∈ 𝒳 q . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ})"

have satisfaction_conditions: "is_state_cover_assignment M V ⟹
Π ⊆ T' ⟹
{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T' ⟹
(⋀ α β . (α,β) ∈ A ∪ B ∪ C ⟹
α ∈ L M ⟹
β ∈ L M ⟹
after_initial M α ≠ after_initial M β ⟹
(∃ ω . α@ω ∈ T' ∧
β@ω ∈ T' ∧
distinguishes M (after_initial M α) (after_initial M β) ω)) ⟹
satisfies_h_condition M V T' m"
unfolding satisfies_h_condition_def Let_def Π n 𝒳 A B C
by force

have c1: "is_state_cover_assignment M V"
using assms(8) .

have c2: "Π ⊆ T'" and c3: "{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ T'"
proof -
have "set T ⊆ T'"
unfolding T'
proof (induction pairs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc a pairs)

obtain α q' β q'' where "a = ((α,q'),(β,q''))"
by (metis prod.collapse)

have "foldl distExtension T (pairs @ [a]) = distExtension (foldl distExtension T pairs) a"
by simp
moreover have "⋀ t . set t ⊆ set (distExtension t a)"
proof -
fix t
have "distExtension t a = combine_after (combine_after t α (get_separating_traces M ((α,q'),(β,```