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)" by (simp add: foldl_conv_foldr) 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'),(β,