Theory Test_Suite_Calculation
section ‹Calculating Sufficient Test Suites›
text ‹This theory describes algorithms to calculate test suites that satisfy the sufficiency
criterion for a given specification FSM and upper bound m on the number of states in the
System Under Test.›
theory Test_Suite_Calculation
imports Test_Suite_IO
begin
subsection ‹Calculating Path Prefixes that are to be Extended With Adaptive Cest Cases›
subsubsection ‹Calculating Tests along m-Traversal-Paths›
fun prefix_pair_tests :: "'a ⇒ (('a,'b,'c) traversal_path × ('a set × 'a set)) set ⇒ ('a × ('a,'b,'c) traversal_path × 'a) set" where
"prefix_pair_tests q pds
= ⋃{{(q,p1,(target q p2)), (q,p2,(target q p1))} | p1 p2 .
∃ (p,(rd,dr)) ∈ pds .
(p1,p2) ∈ set (prefix_pairs p) ∧
(target q p1) ∈ rd ∧
(target q p2) ∈ rd ∧
(target q p1) ≠ (target q p2)}"
lemma prefix_pair_tests_code[code] :
"prefix_pair_tests q pds = (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) pds))"
proof -
have "⋀ tp . tp ∈ prefix_pair_tests q pds ⟹ tp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) pds))"
proof -
fix tp assume "tp ∈ prefix_pair_tests q pds"
then obtain tps where "tp ∈ tps"
and "tps ∈ {{(q,p1,(target q p2)), (q,p2,(target q p1))} | p1 p2 . ∃ (p,(rd,dr)) ∈ pds . (p1,p2) ∈ set (prefix_pairs p) ∧ (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)}"
unfolding prefix_pair_tests.simps
by (meson UnionE)
then obtain p1 p2 where "tps = {(q,p1,(target q p2)), (q,p2,(target q p1))}"
and "∃ (p,(rd,dr)) ∈ pds . (p1,p2) ∈ set (prefix_pairs p) ∧ (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)"
unfolding mem_Collect_eq by blast
then obtain p rd dr where "(p,(rd,dr)) ∈ pds" and "(p1,p2) ∈ set (prefix_pairs p)" and "(target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)"
by blast
have scheme : "⋀ f x xs . x ∈ set xs ⟹ f x ∈ set (map f xs)"
by auto
have "(p1,p2) ∈ set (filter (λ(p1, p2). target q p1 ∈ rd ∧ target q p2 ∈ rd ∧ target q p1 ≠ target q p2) (prefix_pairs p))"
using ‹(p1,p2) ∈ set (prefix_pairs p)›
‹(target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)›
by auto
have "{(q,p1,(target q p2)), (q,p2,(target q p1))} ∈ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))"
using scheme[OF ‹(p1,p2) ∈ set (filter (λ(p1, p2). target q p1 ∈ rd ∧ target q p2 ∈ rd ∧ target q p1 ≠ target q p2) (prefix_pairs p))›, of "(λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))})"]
by simp
then show "tp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) pds))"
using ‹tp ∈ tps› ‹(p,(rd,dr)) ∈ pds›
unfolding ‹tps = {(q,p1,(target q p2)), (q,p2,(target q p1))}›
by blast
qed
moreover have "⋀ tp . tp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) pds))
⟹ tp ∈ prefix_pair_tests q pds"
proof -
fix tp assume "tp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) pds))"
then obtain prddr where "prddr ∈ pds"
and "tp ∈ (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) prddr"
by blast
then obtain p rd dr where "prddr = (p,(rd,dr))" by auto
then have "tp ∈ ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))"
using ‹tp ∈ (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) prddr› by auto
then obtain p1 p2 where "(p1,p2) ∈ set (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))"
and "tp ∈ {(q,p1,(target q p2)), (q,p2,(target q p1))}"
by auto
then have "(target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)"
and "(p1,p2) ∈ set (prefix_pairs p)"
by auto
then show "tp ∈ prefix_pair_tests q pds"
using ‹prddr ∈ pds› ‹tp ∈ {(q,p1,(target q p2)), (q,p2,(target q p1))}›
unfolding prefix_pair_tests.simps ‹prddr = (p,(rd,dr))›
by blast
qed
ultimately show ?thesis
by blast
qed
subsubsection ‹Calculating Tests between Preambles›
fun preamble_prefix_tests' :: "'a ⇒ (('a,'b,'c) traversal_path × ('a set × 'a set)) list ⇒ 'a list ⇒ ('a × ('a,'b,'c) traversal_path × 'a) list" where
"preamble_prefix_tests' q pds drs =
concat (map (λ((p,(rd,dr)),q2,p1) . [(q,p1,q2), (q2,[],(target q p1))])
(filter (λ((p,(rd,dr)),q2,p1) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2)
(concat (map (λ((p,(rd,dr)),q2) . map (λp1 . ((p,(rd,dr)),q2,p1)) (prefixes p)) (List.product pds drs)))))"
definition preamble_prefix_tests :: "'a ⇒ (('a,'b,'c) traversal_path × ('a set × 'a set)) set ⇒ 'a set ⇒ ('a × ('a,'b,'c) traversal_path × 'a) set" where
"preamble_prefix_tests q pds drs = ⋃{{(q,p1,q2), (q2,[],(target q p1))} | p1 q2 . ∃ (p,(rd,dr)) ∈ pds . q2 ∈ drs ∧ (∃ p2 . p = p1@p2) ∧ (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2}"
lemma preamble_prefix_tests_code[code] :
"preamble_prefix_tests q pds drs = (⋃(image (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) pds))"
proof -
have "⋀ pp . pp ∈ preamble_prefix_tests q pds drs ⟹ pp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) pds))"
proof -
fix pp assume "pp ∈ preamble_prefix_tests q pds drs"
then obtain p1 q2 where "pp ∈ {(q,p1,q2), (q2,[],(target q p1))}"
and "∃ (p,(rd,dr)) ∈ pds . q2 ∈ drs ∧ (∃ p2 . p = p1@p2) ∧ (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2"
unfolding preamble_prefix_tests_def by blast
then obtain p rd dr where "(p,(rd,dr)) ∈ pds" and "q2 ∈ drs" and "(∃ p2 . p = p1@p2)" and "(target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2"
by auto
then have "(p1,q2) ∈ (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs))"
unfolding prefixes_set by force
then show "pp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) pds))"
using ‹(p,(rd,dr)) ∈ pds›
‹pp ∈ {(q,p1,q2), (q2,[],(target q p1))}› by blast
qed
moreover have "⋀ pp . pp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) pds))
⟹ pp ∈ preamble_prefix_tests q pds drs"
proof -
fix pp assume "pp ∈ (⋃(image (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) pds))"
then obtain prddr where "prddr ∈ pds"
and "pp ∈ (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) prddr"
by blast
obtain p rd dr where "prddr = (p,(rd,dr))"
using prod_cases3 by blast
obtain p1 q2 where "(p1,q2) ∈ (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs))"
and "pp ∈ {(q,p1,q2), (q2,[],(target q p1))}"
using ‹pp ∈ (λ (p,(rd,dr)) . ⋃(image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs)))) prddr›
unfolding ‹prddr = (p,(rd,dr))›
by blast
have "q2 ∈ drs ∧ (∃ p2 . p = p1@p2) ∧ (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2"
using ‹(p1,q2) ∈ (Set.filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) ((set (prefixes p)) × drs))›
unfolding prefixes_set
by auto
then have "∃(p, rd, dr)∈pds. q2 ∈ drs ∧ (∃p2. p = p1 @ p2) ∧ target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2"
using ‹prddr ∈ pds› ‹prddr = (p,(rd,dr))›
by blast
then have *: "{(q,p1,q2), (q2,[],(target q p1))} ∈ {{(q, p1, q2), (q2, [], target q p1)} |p1 q2.
∃(p, rd, dr)∈pds. q2 ∈ drs ∧ (∃p2. p = p1 @ p2) ∧ target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2}" by blast
show "pp ∈ preamble_prefix_tests q pds drs"
using UnionI[OF * ‹pp ∈ {(q,p1,q2), (q2,[],(target q p1))}›]
unfolding preamble_prefix_tests_def by assumption
qed
ultimately show ?thesis by blast
qed
subsubsection "Calculating Tests between m-Traversal-Paths Prefixes and Preambles"
fun preamble_pair_tests :: "'a set set ⇒ ('a × 'a) set ⇒ ('a × ('a,'b,'c) traversal_path × 'a) set" where
"preamble_pair_tests drss rds = (⋃ drs ∈ drss . (λ (q1,q2) . (q1,[],q2)) ` ((drs × drs) ∩ rds))"
subsection ‹Calculating a Test Suite›
definition calculate_test_paths ::
"('a,'b,'c) fsm
⇒ nat
⇒ 'a set
⇒ ('a × 'a) set
⇒ ('a set × 'a set) list
⇒ (('a ⇒ ('a,'b,'c) traversal_path set) × (('a × ('a,'b,'c) traversal_path) ⇒ 'a set))"
where
"calculate_test_paths M m d_reachable_states r_distinguishable_pairs repetition_sets =
(let
paths_with_witnesses
= (image (λ q . (q,m_traversal_paths_with_witness M q repetition_sets m)) d_reachable_states);
get_paths
= m2f (set_as_map paths_with_witnesses);
PrefixPairTests
= ⋃ q ∈ d_reachable_states . ⋃ mrsps ∈ get_paths q . prefix_pair_tests q mrsps;
PreamblePrefixTests
= ⋃ q ∈ d_reachable_states . ⋃ mrsps ∈ get_paths q . preamble_prefix_tests q mrsps d_reachable_states;
PreamblePairTests
= preamble_pair_tests (⋃ (q,pw) ∈ paths_with_witnesses . ((λ (p,(rd,dr)) . dr) ` pw)) r_distinguishable_pairs;
tests
= PrefixPairTests ∪ PreamblePrefixTests ∪ PreamblePairTests;
tps'
= m2f_by ⋃ (set_as_map (image (λ (q,p) . (q, image fst p)) paths_with_witnesses));
tps''
= m2f (set_as_map (image (λ (q,p,q') . (q,p)) tests));
tps
= (λ q . tps' q ∪ tps'' q);
rd_targets
= m2f (set_as_map (image (λ (q,p,q') . ((q,p),q')) tests))
in
( tps, rd_targets ))"
definition combine_test_suite ::
"('a,'b,'c) fsm
⇒ nat
⇒ ('a × ('a,'b,'c) preamble) set
⇒ (('a × 'a) × (('d,'b,'c) separator × 'd × 'd)) set
⇒ ('a set × 'a set) list
⇒ ('a,'b,'c,'d) test_suite"
where
"combine_test_suite M m states_with_preambles pairs_with_separators repetition_sets =
(let drs = image fst states_with_preambles;
rds = image fst pairs_with_separators;
tps_and_targets = calculate_test_paths M m drs rds repetition_sets;
atcs = m2f (set_as_map pairs_with_separators)
in (Test_Suite states_with_preambles (fst tps_and_targets) (snd tps_and_targets) atcs))"
definition calculate_test_suite_for_repetition_sets ::
"('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ ('a set × 'a set) list ⇒ ('a,'b,'c, ('a × 'a) + 'a) test_suite"
where
"calculate_test_suite_for_repetition_sets M m repetition_sets =
(let
states_with_preambles = d_reachable_states_with_preambles M;
pairs_with_separators = image (λ((q1,q2),A) . ((q1,q2),A,Inr q1,Inr q2)) (r_distinguishable_state_pairs_with_separators M)
in combine_test_suite M m states_with_preambles pairs_with_separators repetition_sets)"
subsection ‹Sufficiency of the Calculated Test Suite›
lemma calculate_test_suite_for_repetition_sets_sufficient_and_finite :
fixes M :: "('a::linorder,'b::linorder,'c) fsm"
assumes "observable M"
and "completely_specified M"
and "inputs M ≠ {}"
and "⋀q. q ∈ FSM.states M ⟹ ∃d∈set RepSets. q ∈ fst d"
and "⋀d. d ∈ set RepSets ⟹ fst d ⊆ states M ∧ (snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ q1 q2 d. d ∈ set RepSets ⟹ q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
shows "implies_completeness (calculate_test_suite_for_repetition_sets M m RepSets) M m"
and "is_finite_test_suite (calculate_test_suite_for_repetition_sets M m RepSets)"
proof -
obtain states_with_preambles tps rd_targets atcs where "calculate_test_suite_for_repetition_sets M m RepSets
= Test_Suite states_with_preambles tps rd_targets atcs"
using test_suite.exhaust by blast
have "⋀ a b c d . Test_Suite states_with_preambles tps rd_targets atcs = Test_Suite a b c d ⟹ tps = b"
by blast
have states_with_preambles_def : "states_with_preambles = d_reachable_states_with_preambles M"
and tps_def : "tps = (λq. (m2f_by ⋃ (set_as_map ((λ(q, p). (q, fst ` p)) ` (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M))) q
∪ (m2f (set_as_map ((λ(q, p, q'). (q, p)) `
((⋃q∈fst ` d_reachable_states_with_preambles M. ⋃ (prefix_pair_tests q ` (m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q)))
∪ (⋃q∈fst ` d_reachable_states_with_preambles M. ⋃mrsps∈ m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))
∪ preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))))) q)"
and rd_targets_def : "rd_targets = m2f (set_as_map
((λ(q, p, y). ((q, p), y)) `
((⋃q∈fst ` d_reachable_states_with_preambles M. ⋃ (prefix_pair_tests q ` (m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q)))
∪ (⋃q∈fst ` d_reachable_states_with_preambles M. ⋃mrsps∈ m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))
∪ preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))))"
and atcs_def : "atcs = m2f (set_as_map ((λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M))"
using ‹calculate_test_suite_for_repetition_sets M m RepSets = Test_Suite states_with_preambles tps rd_targets atcs›[symmetric]
unfolding calculate_test_suite_for_repetition_sets_def combine_test_suite_def Let_def calculate_test_paths_def fst_conv snd_conv by force+
have tps_alt_def: "⋀ q . q ∈ fst ` d_reachable_states_with_preambles M ⟹
tps q = (fst ` m_traversal_paths_with_witness M q RepSets m) ∪
{z. (q, z)
∈ (λ(q, p, q'). (q, p)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
and rd_targets_alt_def: "⋀ q p . q ∈ fst ` d_reachable_states_with_preambles M ⟹
rd_targets (q,p) = {z. ((q, p), z)
∈ (λ(q, p, y). ((q, p), y)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
proof -
fix q p assume "q ∈ fst ` d_reachable_states_with_preambles M"
have scheme0 : "(case set_as_map
((λ(q, p). (q, fst ` p)) `
(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M)
q of
None ⇒ ⋃ {} | Some x ⇒ ⋃ x) = image fst (m_traversal_paths_with_witness M q RepSets m)"
proof -
have *: "((λ(q, p). (q, fst ` p)) `
(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M)
= (λ q . (q , image fst (m_traversal_paths_with_witness M q RepSets m))) ` (fst ` d_reachable_states_with_preambles M)"
by force
have **: "⋀ f q xs . (case set_as_map
((λq. (q, f q)) ` xs)
q of
None ⇒ ⋃ {} | Some xs ⇒ ⋃ xs) = (if q ∈ xs then ⋃ {f q} else ⋃ {})"
unfolding set_as_map_def by auto
show ?thesis
unfolding * **
using ‹q ∈ fst ` d_reachable_states_with_preambles M›
by auto
qed
have scheme1 : "⋀ f q xs . (case set_as_map
((λq. (q, f q)) ` xs)
q of
None ⇒ {} | Some xs ⇒ xs) = (if q ∈ xs then {f q} else {})"
unfolding set_as_map_def by auto
have scheme2: "(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q `
(if q ∈ fst ` d_reachable_states_with_preambles M
then {m_traversal_paths_with_witness M q RepSets m} else {})))
= (⋃q∈fst ` d_reachable_states_with_preambles M. (⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})))"
unfolding set_as_map_def by auto
have scheme3: "(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈if q ∈ fst ` d_reachable_states_with_preambles M
then {m_traversal_paths_with_witness M q RepSets m} else {}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))
= (⋃q∈fst ` d_reachable_states_with_preambles M. (⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m} . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)))"
unfolding set_as_map_def by auto
have scheme4 : "(fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)
= image fst (r_distinguishable_state_pairs_with_separators M)"
by force
have *:"tps q = (fst ` m_traversal_paths_with_witness M q RepSets m) ∪
{z. (q, z)
∈ (λ(q, p, q'). (q, p)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
unfolding tps_def
unfolding scheme0 scheme1 scheme2 scheme3 scheme4
unfolding set_as_map_def
by auto
have **: "{z. (q, z)
∈ (λ(q, p, q'). (q, p)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}
= {z. (q, z)
∈ (λ(q, p, q'). (q, p)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
(is "{z. (q, z) ∈ ?S1} = {z. (q, z) ∈ ?S2}")
proof -
have "⋀ z . (q, z) ∈ ?S1 ⟹ (q, z) ∈ ?S2"
proof -
fix z assume "(q, z) ∈ ?S1"
then consider "(q, z) ∈ (λ(q, p, q'). (q, p)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
| "(q,z) ∈ (λ(q, p, q'). (q, p)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
| "(q,z) ∈ (λ(q, p, q'). (q, p)) ` (preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))"
by blast
then show "(q, z) ∈ ?S2" proof cases
case 1
have scheme: "⋀ f y xs . y ∈ image f xs ⟹ ∃ x . x ∈ xs ∧ f x = y" by auto
obtain qzq where "qzq ∈ (⋃q∈fst ` d_reachable_states_with_preambles M. ⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
and "(λ(q, p, q'). (q, p)) qzq = (q,z)"
using scheme[OF 1] by blast
then obtain q' where "q'∈fst ` d_reachable_states_with_preambles M"
and "qzq ∈ ⋃ (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})"
by blast
then have "fst qzq = q'"
by auto
then have "q' = q"
using ‹(λ(q, p, q'). (q, p)) qzq = (q,z)›
by (simp add: prod.case_eq_if)
then have "qzq ∈ ⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})"
using ‹qzq ∈ ⋃ (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})›
by blast
then have "(λ(q, p, q'). (q, p)) qzq ∈ ?S2"
by auto
then show ?thesis
unfolding ‹(λ(q, p, q'). (q, p)) qzq = (q,z)›
by assumption
next
case 2
then show ?thesis by blast
next
case 3
then show ?thesis by blast
qed
qed
moreover have "⋀ z . (q, z) ∈ ?S2 ⟹ (q, z) ∈ ?S1"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› by blast
ultimately show ?thesis
by meson
qed
show "tps q = (fst ` m_traversal_paths_with_witness M q RepSets m) ∪
{z. (q, z)
∈ (λ(q, p, q'). (q, p)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
using * unfolding ** by assumption
have ***: "rd_targets (q,p) = {z. ((q, p), z)
∈ (λ(q, p, y). ((q, p), y)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
unfolding rd_targets_def
unfolding scheme1 scheme2 scheme3 scheme4
unfolding set_as_map_def
by auto
have ****: "{z. ((q, p), z)
∈ (λ(q, p, y). ((q, p), y)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}
= {z. ((q, p), z)
∈ (λ(q, p, y). ((q, p), y)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
(is "{z. ((q, p), z) ∈ ?S1} = {z. ((q, p), z) ∈ ?S2}")
proof -
have "⋀ z . ((q, p), z) ∈ ?S1 ⟹ ((q, p), z) ∈ ?S2"
proof -
fix z assume "((q, p), z) ∈ ?S1"
then consider "((q, p), z) ∈ (λ(q, p, y). ((q, p), y)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
| "((q, p), z) ∈ (λ(q, p, y). ((q, p), y)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
| "((q, p), z) ∈ (λ(q, p, y). ((q, p), y)) ` (preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))"
by blast
then show "((q, p), z) ∈ ?S2" proof cases
case 1
have scheme: "⋀ f y xs . y ∈ image f xs ⟹ ∃ x . x ∈ xs ∧ f x = y" by auto
obtain qzq where "qzq ∈ (⋃q∈fst ` d_reachable_states_with_preambles M. ⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
and "(λ(q, p, y). ((q, p), y)) qzq = ((q,p),z)"
using scheme[OF 1] by blast
then obtain q' where "q'∈fst ` d_reachable_states_with_preambles M"
and "qzq ∈ ⋃ (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})"
by blast
then have "fst qzq = q'"
by auto
then have "q' = q"
using ‹(λ(q, p, y). ((q, p), y)) qzq = ((q,p),z)›
by (simp add: prod.case_eq_if)
then have "qzq ∈ ⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})"
using ‹qzq ∈ ⋃ (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})›
by blast
then have "(λ(q, p, y). ((q, p), y)) qzq ∈ ?S2"
by auto
then show ?thesis
unfolding ‹(λ(q, p, y). ((q, p), y)) qzq = ((q,p),z)›
by assumption
next
case 2
then show ?thesis by blast
next
case 3
then show ?thesis by blast
qed
qed
moreover have "⋀ z . ((q, p), z) ∈ ?S2 ⟹ ((q, p), z) ∈ ?S1"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› by blast
ultimately show ?thesis
by meson
qed
show "rd_targets (q,p) = {z. ((q, p), z)
∈ (λ(q, p, y). ((q, p), y)) `
((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
using *** unfolding **** by assumption
qed
define pps_alt :: "('a × ('a,'b,'c) traversal_path × 'a) set" where pps_alt_def : "pps_alt = {(q1,[],q2) | q1 q2 . ∃ q p rd dr . q ∈ fst ` d_reachable_states_with_preambles M ∧ (p,(rd,dr)) ∈ m_traversal_paths_with_witness M q RepSets m ∧ q1 ∈ dr ∧ q2 ∈ dr ∧ (q1,q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M}"
have preamble_pair_tests_alt :
"preamble_pair_tests (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M)
= pps_alt"
(is "?PP1 = ?PP2")
proof -
have "⋀ x . x ∈ ?PP1 ⟹ x ∈ ?PP2"
proof -
fix x assume "x ∈ ?PP1"
then obtain drs where "drs ∈ (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)"
and "x ∈ (λ(q1, q2). (q1, [], q2)) ` (drs × drs ∩ fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
unfolding preamble_pair_tests.simps by force
obtain q y where "(q,y) ∈ (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M"
and "drs ∈ (λ(p, rd, dr). dr) ` y"
using ‹drs ∈ (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)›
by force
have "q ∈ fst ` d_reachable_states_with_preambles M"
and "y = m_traversal_paths_with_witness M q RepSets m"
using ‹(q,y) ∈ (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M›
by force+
obtain p rd where "(p,(rd,drs)) ∈ m_traversal_paths_with_witness M q RepSets m"
using ‹drs ∈ (λ(p, rd, dr). dr) ` y› unfolding ‹y = m_traversal_paths_with_witness M q RepSets m›
by force
obtain q1 q2 where "(q1,q2) ∈ (drs × drs ∩ fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
and "x = (q1, [], q2)"
using ‹x ∈ (λ(q1, q2). (q1, [], q2)) ` (drs × drs ∩ fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)›
by force
have "q1 ∈ drs ∧ q2 ∈ drs ∧ (q1,q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using ‹(q1,q2) ∈ (drs × drs ∩ fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)›
by force
then show "x ∈ ?PP2"
unfolding ‹x = (q1, [], q2)› pps_alt_def
using ‹q ∈ fst ` d_reachable_states_with_preambles M› ‹(p,(rd,drs)) ∈ m_traversal_paths_with_witness M q RepSets m›
by blast
qed
moreover have "⋀ x . x ∈ ?PP2 ⟹ x ∈ ?PP1"
proof -
fix x assume "x ∈ ?PP2"
then obtain q1 q2 where "x = (q1,[],q2)" unfolding pps_alt_def
by auto
then obtain q p rd dr where "q ∈ fst ` d_reachable_states_with_preambles M"
and "(p,(rd,dr)) ∈ m_traversal_paths_with_witness M q RepSets m"
and "q1 ∈ dr ∧ q2 ∈ dr ∧ (q1,q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using ‹x ∈ ?PP2› unfolding pps_alt_def by blast
have "dr ∈ (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› ‹(p,(rd,dr)) ∈ m_traversal_paths_with_witness M q RepSets m› by force
moreover have "x ∈ (λ(q1, q2). (q1, [], q2)) ` (dr × dr ∩ fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
unfolding ‹x = (q1,[],q2)› using ‹q1 ∈ dr ∧ q2 ∈ dr ∧ (q1,q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M› by force
ultimately show "x ∈ ?PP1"
unfolding preamble_pair_tests.simps by force
qed
ultimately show ?thesis by blast
qed
have p1: "(initial M,initial_preamble M) ∈ states_with_preambles"
using fsm_initial[of M]
unfolding states_with_preambles_def d_reachable_states_with_preambles_def calculate_state_preamble_from_input_choices.simps by force
have p2a: "⋀ q P . (q,P) ∈ states_with_preambles ⟹ is_preamble P M q"
using assms(1) d_reachable_states_with_preambles_soundness(1) states_with_preambles_def by blast
have p2b: "⋀ q P . (q,P) ∈ states_with_preambles ⟹ (tps q) ≠ {}"
proof -
fix q P assume "(q,P) ∈ states_with_preambles"
then have "q ∈ (image fst (d_reachable_states_with_preambles M))"
unfolding states_with_preambles_def
by (simp add: rev_image_eqI)
have "q ∈ states M"
using ‹(q, P) ∈ states_with_preambles› assms(1) d_reachable_states_with_preambles_soundness(2) states_with_preambles_def by blast
obtain p' d' where "(p', d') ∈ m_traversal_paths_with_witness M q RepSets m"
using m_traversal_path_exist[OF assms(2) ‹q ∈ states M› assms(3) ‹⋀q. q ∈ FSM.states M ⟹ ∃d∈set RepSets. q ∈ fst d›] assms(5)
by blast
then have "p' ∈ image fst (m_traversal_paths_with_witness M q RepSets m)"
using image_iff by fastforce
have "(q, image fst (m_traversal_paths_with_witness M q RepSets m)) ∈ (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M))))"
using ‹q ∈ (image fst (d_reachable_states_with_preambles M))› by force
have "(image fst (m_traversal_paths_with_witness M q RepSets m)) ∈ (m2f (set_as_map (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M)))))) q"
using set_as_map_containment[OF ‹(q, image fst (m_traversal_paths_with_witness M q RepSets m)) ∈ (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M))))›]
by assumption
then have "p' ∈ (⋃ ((m2f (set_as_map (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M)))))) q))"
using ‹p' ∈ image fst (m_traversal_paths_with_witness M q RepSets m)› by blast
then show "(tps q) ≠ {}"
unfolding tps_def m2f_by_from_m2f by blast
qed
have p2: "(∀q P. (q, P) ∈ states_with_preambles ⟶ is_preamble P M q ∧ tps q ≠ {})"
using p2a p2b by blast
have "⋀ q1 q2 A d1 d2 . ((A,d1,d2) ∈ atcs (q1,q2)) ⟹ ((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M ∧ d1 = Inr q1 ∧ d2 = Inr q2"
proof -
fix q1 q2 A d1 d2 assume "((A,d1,d2) ∈ atcs (q1,q2))"
then have "atcs (q1,q2) = {z. ((q1, q2), z) ∈ (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M}"
unfolding atcs_def set_as_map_def by auto
then show "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M ∧ d1 = Inr q1 ∧ d2 = Inr q2"
using ‹((A,d1,d2) ∈ atcs (q1,q2))› by auto
qed
have "⋀ q1 q2 A d1 d2 . (A,d1,d2) ∈ atcs (q1,q2) ⟹ (A,d2,d1) ∈ atcs (q2,q1) ∧ is_separator M q1 q2 A d1 d2"
proof -
fix q1 q2 A d1 d2 assume "(A,d1,d2) ∈ atcs (q1,q2)"
then have "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M" and "d1 = Inr q1" and "d2 = Inr q2"
using ‹⋀ q1 q2 A d1 d2 . ((A,d1,d2) ∈ atcs (q1,q2)) ⟹ ((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M ∧ d1 = Inr q1 ∧ d2 = Inr q2›
by blast+
then have "((q2,q1),A) ∈ r_distinguishable_state_pairs_with_separators M"
unfolding r_distinguishable_state_pairs_with_separators_def
by auto
then have "(A,d2,d1) ∈ atcs (q2,q1)"
unfolding atcs_def ‹d1 = Inr q1› ‹d2 = Inr q2› set_as_map_def by force
moreover have "is_separator M q1 q2 A d1 d2"
using r_distinguishable_state_pairs_with_separators_elem_is_separator[OF ‹((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M› assms(1,2)]
unfolding ‹d1 = Inr q1› ‹d2 = Inr q2›
by assumption
ultimately show "(A,d2,d1) ∈ atcs (q2,q1) ∧ is_separator M q1 q2 A d1 d2"
by simp
qed
then have p3 : "(∀q1 q2 A d1 d2. (A, d1, d2) ∈ atcs (q1, q2) ⟶ (A, d2, d1) ∈ atcs (q2, q1) ∧ is_separator M q1 q2 A d1 d2)"
by blast
have p4: "⋀ q . q ∈ states M ⟹ (∃d ∈ set RepSets. q ∈ fst d)"
by (simp add: assms(4))
have p5: "⋀ d . d ∈ set RepSets ⟹ ((fst d ⊆ states M) ∧ (snd d = fst d ∩ fst ` states_with_preambles) ∧ (∀ q1 q2 . q1 ∈ fst d ⟶ q2 ∈ fst d ⟶ q1 ≠ q2 ⟶ atcs (q1,q2) ≠ {}))"
proof -
fix d assume "d ∈ set RepSets"
then have "⋀ q1 q2 . q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1,q2) ≠ {}"
proof -
fix q1 q2 assume "q1 ∈ fst d" and "q2 ∈ fst d" and "q1 ≠ q2"
then have "(q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using assms(6)[OF ‹d ∈ set RepSets›] by blast
then obtain A where "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M"
by auto
then have "(A,Inr q1,Inr q2) ∈ atcs (q1,q2)"
unfolding atcs_def set_as_map_def
by force
then show "atcs (q1,q2) ≠ {}"
by blast
qed
then show "((fst d ⊆ states M) ∧ (snd d = fst d ∩ fst ` states_with_preambles) ∧ (∀ q1 q2 . q1 ∈ fst d ⟶ q2 ∈ fst d ⟶ q1 ≠ q2 ⟶ atcs (q1,q2) ≠ {}))"
using assms(5)[OF ‹d ∈ set RepSets›] unfolding states_with_preambles_def by blast
qed
have p6 : "⋀ q . q ∈ image fst states_with_preambles ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q RepSets m} ∧ fst ` (m_traversal_paths_with_witness M q RepSets m) ⊆ tps q"
proof
fix q assume "q ∈ image fst states_with_preambles"
then have "q ∈ fst ` d_reachable_states_with_preambles M"
unfolding states_with_preambles_def by assumption
then have "q ∈ states M"
by (metis (no_types, lifting) assms(1) d_reachable_states_with_preambles_soundness(2) image_iff prod.collapse)
show "fst ` m_traversal_paths_with_witness M q RepSets m ⊆ tps q"
unfolding tps_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by blast
show "tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q RepSets m}"
proof
fix p assume "p ∈ tps q"
have * : "(⋀ q . q ∈ states M ⟹ (∃d ∈ set RepSets. q ∈ fst d))"
using p4 by blast
have **: "(⋀ d . d ∈ set RepSets ⟹ (snd d ⊆ fst d))"
using p5 by simp
from ‹p ∈ tps q› consider
(a) "p ∈ fst ` m_traversal_paths_with_witness M q RepSets m" |
(b) "(q, p) ∈ (λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m))" |
(c) "(q, p) ∈ (λ(q, p, q'). (q, p)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))" |
(d) "(q, p) ∈ (λ(q, p, q'). (q, p)) ` pps_alt"
unfolding tps_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›] preamble_pair_tests_alt by blast
then show "p ∈ {p1. ∃p2 d. (p1 @ p2, d) ∈ m_traversal_paths_with_witness M q RepSets m}"
proof cases
case a
then obtain d where "(p,d) ∈ m_traversal_paths_with_witness M q RepSets m"
by auto
then have "∃p2 d. (p @ p2, d) ∈ m_traversal_paths_with_witness M q RepSets m"
by (metis append_eq_append_conv2)
then show ?thesis
by blast
next
case b
obtain p1 p2 where "(q,p) ∈ ((λ(q, p, q'). (q, p)) `{(q, p1, target q p2), (q, p2, target q p1)})"
and "∃(p, rd, dr)∈m_traversal_paths_with_witness M q RepSets m.
(p1, p2) ∈ set (prefix_pairs p) ∧ target q p1 ∈ rd ∧ target q p2 ∈ rd ∧ target q p1 ≠ target q p2"
using b
unfolding prefix_pair_tests.simps by blast
obtain p' d where "(p', d) ∈ m_traversal_paths_with_witness M q RepSets m"
and "(p1, p2) ∈ set (prefix_pairs p')"
using ‹∃(p, rd, dr)∈m_traversal_paths_with_witness M q RepSets m.
(p1, p2) ∈ set (prefix_pairs p) ∧ target q p1 ∈ rd ∧ target q p2 ∈ rd ∧ target q p1 ≠ target q p2›
by blast
have "∃ p'' . p' = p @ p''"
using ‹(p1, p2) ∈ set (prefix_pairs p')› unfolding prefix_pairs_set_alt
using ‹(q,p) ∈ ((λ(q, p, q'). (q, p)) `{(q, p1, target q p2), (q, p2, target q p1)})› by auto
then show ?thesis
using ‹(p', d) ∈ m_traversal_paths_with_witness M q RepSets m›
by blast
next
case c
obtain q' where "q' ∈ fst ` d_reachable_states_with_preambles M"
and "(q,p) ∈ (λ(q, p, q'). (q, p)) ` (preamble_prefix_tests q' (m_traversal_paths_with_witness M q' RepSets m) (fst ` d_reachable_states_with_preambles M))"
using c by blast
obtain p1 q2 where "(q,p) ∈ ((λ(q, p, q'). (q, p)) `{(q', p1, q2), (q2, [], target q' p1)})"
and "∃(p, rd, dr)∈m_traversal_paths_with_witness M q' RepSets m.
q2 ∈ fst ` d_reachable_states_with_preambles M ∧ (∃p2. p = p1 @ p2) ∧ target q' p1 ∈ rd ∧ q2 ∈ rd ∧ target q' p1 ≠ q2"
using ‹(q,p) ∈ (λ(q, p, q'). (q, p)) ` (preamble_prefix_tests q' (m_traversal_paths_with_witness M q' RepSets m) (fst ` d_reachable_states_with_preambles M))›
unfolding preamble_prefix_tests_def
by blast
obtain p2 d where "(p1@p2, d)∈m_traversal_paths_with_witness M q' RepSets m"
and "q2 ∈ fst ` d_reachable_states_with_preambles M"
using ‹∃(p, rd, dr)∈m_traversal_paths_with_witness M q' RepSets m.
q2 ∈ fst ` d_reachable_states_with_preambles M ∧ (∃p2. p = p1 @ p2) ∧ target q' p1 ∈ rd ∧ q2 ∈ rd ∧ target q' p1 ≠ q2›
by blast
consider (a) "q = q' ∧ p = p1" | (b) "q = q2 ∧ p = []"
using ‹(q,p) ∈ ((λ(q, p, q'). (q, p)) `{(q', p1, q2), (q2, [], target q' p1)})› by auto
then show ?thesis proof cases
case a
then show ?thesis
using ‹(p1 @ p2, d) ∈ m_traversal_paths_with_witness M q' RepSets m› by blast
next
case b
then have "q ∈ states M" and "p = []"
using ‹q2 ∈ fst ` d_reachable_states_with_preambles M› unfolding d_reachable_states_with_preambles_def by auto
have "∃p' d'. (p', d') ∈ m_traversal_paths_with_witness M q RepSets m"
using m_traversal_path_exist[OF assms(2) ‹q ∈ states M› assms(3) * **]
by blast
then show ?thesis
unfolding ‹p = []›
by simp
qed
next
case d
then have "p = []"
unfolding pps_alt_def by force
have "q ∈ states M"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› unfolding d_reachable_states_with_preambles_def by auto
have "∃p' d'. (p', d') ∈ m_traversal_paths_with_witness M q RepSets m"
using m_traversal_path_exist[OF assms(2) ‹q ∈ states M› assms(3) * **]
by blast
then show ?thesis
unfolding ‹p = []›
by simp
qed
qed
qed
have p7 : "⋀ q p d . q ∈ image fst states_with_preambles ⟹ (p,d) ∈ m_traversal_paths_with_witness M q RepSets m ⟹
( (∀ p1 p2 p3 . p=p1@p2@p3 ⟶ p2 ≠ [] ⟶ target q p1 ∈ fst d ⟶ target q (p1@p2) ∈ fst d ⟶ target q p1 ≠ target q (p1@p2) ⟶ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1)))
∧ (∀ p1 p2 q' . p=p1@p2 ⟶ q' ∈ image fst states_with_preambles ⟶ target q p1 ∈ fst d ⟶ q' ∈ fst d ⟶ target q p1 ≠ q' ⟶ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1)))
∧ (∀ q1 q2 . q1 ≠ q2 ⟶ q1 ∈ snd d ⟶ q2 ∈ snd d ⟶ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))))"
proof -
fix q p d assume "q ∈ image fst states_with_preambles" and "(p,d) ∈ m_traversal_paths_with_witness M q RepSets m"
then have "(p,(fst d, snd d)) ∈ m_traversal_paths_with_witness M q RepSets m" by auto
have "q ∈ fst ` d_reachable_states_with_preambles M"
using ‹q ∈ image fst states_with_preambles› unfolding states_with_preambles_def by assumption
have p7c1 : "⋀ p1 p2 p3 . p=p1@p2@p3 ⟹ p2 ≠ [] ⟹ target q p1 ∈ fst d ⟹ target q (p1@p2) ∈ fst d ⟹ target q p1 ≠ target q (p1@p2) ⟹ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1))"
proof -
fix p1 p2 p3 assume "p=p1@p2@p3" and "p2 ≠ []" and "target q p1 ∈ fst d" and "target q (p1@p2) ∈ fst d" and "target q p1 ≠ target q (p1@p2)"
have "(p1,p1@p2) ∈ set (prefix_pairs p)"
using ‹p=p1@p2@p3› ‹p2 ≠ []› unfolding prefix_pairs_set
by simp
then have "(p1,p1@p2) ∈ set (filter (λ(p1, p2). target q p1 ∈ fst d ∧ target q p2 ∈ fst d ∧ target q p1 ≠ target q p2) (prefix_pairs p))"
using ‹target q p1 ∈ fst d› ‹target q (p1@p2) ∈ fst d› ‹target q p1 ≠ target q (p1@p2)›
by auto
have "{(q, p1, target q (p1@p2)), (q, (p1@p2), target q p1)} ∈ ((set (map (λ(p1, p2). {(q, p1, target q p2), (q, p2, target q p1)})
(filter (λ(p1, p2). target q p1 ∈ fst d ∧ target q p2 ∈ fst d ∧ target q p1 ≠ target q p2) (prefix_pairs p)))))"
using map_set[OF ‹(p1,p1@p2) ∈ set (filter (λ(p1, p2). target q p1 ∈ fst d ∧ target q p2 ∈ fst d ∧ target q p1 ≠ target q p2) (prefix_pairs p))›, of "(λ(p1, p2). {(q, p1, target q p2), (q, p2, target q p1)})"]
by force
then have "(q, p1, target q (p1@p2)) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
and "(q, p1@p2, target q p1) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
unfolding prefix_pair_tests_code[of q "m_traversal_paths_with_witness M q RepSets m"]
using ‹(p,(fst d, snd d)) ∈ m_traversal_paths_with_witness M q RepSets m›
by blast+
have "p1 ∈ tps q"
proof -
have "(q, p1) ∈ ((λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)))"
using ‹(q, p1, target q (p1@p2)) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)›
by (simp add: rev_image_eqI)
then show ?thesis
unfolding tps_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by blast
qed
moreover have "(p1@p2) ∈ tps q"
proof -
have "(q, p1@p2) ∈ ((λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)))"
using ‹(q, p1@p2, target q p1) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)›
by (simp add: rev_image_eqI)
then show ?thesis
unfolding tps_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by blast
qed
moreover have "target q p1 ∈ rd_targets (q,(p1@p2))"
proof -
have "((q, p1@p2), target q p1) ∈ (λ(q, p, y). ((q, p), y)) ` prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
using ‹(q, p1@p2, target q p1) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)›
by (simp add: rev_image_eqI)
then show ?thesis
unfolding rd_targets_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by blast
qed
moreover have "target q (p1@p2) ∈ rd_targets (q,p1)"
proof -
have "((q, p1), target q (p1@p2)) ∈ (λ(q, p, y). ((q, p), y)) ` prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
using ‹(q, p1, target q (p1@p2)) ∈ prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)›
by (simp add: rev_image_eqI)
then show ?thesis
unfolding rd_targets_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by blast
qed
ultimately show "(p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1))"
by blast
qed
moreover have p7c2: "⋀ p1 p2 q' . p=p1@p2 ⟹ q' ∈ image fst states_with_preambles ⟹ target q p1 ∈ fst d ⟹ q' ∈ fst d ⟹ target q p1 ≠ q' ⟹ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1))"
proof -
fix p1 p2 q' assume "p=p1@p2" and "q' ∈ image fst states_with_preambles" and "target q p1 ∈ fst d" and "q' ∈ fst d" and "target q p1 ≠ q'"
then have "q' ∈ fst ` d_reachable_states_with_preambles M"
unfolding states_with_preambles_def by blast
have "p1 ∈ set (prefixes p)"
using ‹p=p1@p2› unfolding prefixes_set
by simp
then have "(p1,q') ∈ Set.filter (λ(p1, q2). target q p1 ∈ fst d ∧ q2 ∈ fst d ∧ target q p1 ≠ q2) (set (prefixes p) × fst ` d_reachable_states_with_preambles M)"
using ‹target q p1 ∈ fst d› ‹q' ∈ fst d› ‹q' ∈ image fst states_with_preambles› ‹target q p1 ≠ q'› unfolding states_with_preambles_def
by force
then have "{(q, p1, q'), (q', [], target q p1)} ⊆ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
using preamble_prefix_tests_code[of q "m_traversal_paths_with_witness M q RepSets m" "(fst ` d_reachable_states_with_preambles M)"]
using ‹(p,(fst d, snd d)) ∈ m_traversal_paths_with_witness M q RepSets m›
by blast
then have "(q, p1, q') ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
and "(q', [], target q p1) ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
by blast+
have "p1 ∈ tps q"
using ‹(q, p1, q') ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)›
‹q ∈ fst ` d_reachable_states_with_preambles M›
unfolding tps_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by force
moreover have "[] ∈ tps q'"
using ‹(q', [], target q p1) ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)›
‹q ∈ fst ` d_reachable_states_with_preambles M›
unfolding tps_alt_def[OF ‹q' ∈ fst ` d_reachable_states_with_preambles M›]
by force
moreover have "target q p1 ∈ rd_targets (q',[])"
using ‹(q', [], target q p1) ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)›
‹q ∈ fst ` d_reachable_states_with_preambles M›
unfolding rd_targets_alt_def[OF ‹q' ∈ fst ` d_reachable_states_with_preambles M›]
by force
moreover have "q' ∈ rd_targets (q,p1)"
using ‹(q, p1, q') ∈ preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)›
‹q ∈ fst ` d_reachable_states_with_preambles M›
unfolding rd_targets_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
by force
ultimately show "(p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1))"
by blast
qed
moreover have p7c3: "⋀ q1 q2 . q1 ≠ q2 ⟹ q1 ∈ snd d ⟹ q2 ∈ snd d ⟹ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))"
proof -
fix q1 q2 assume "q1 ≠ q2" and "q1 ∈ snd d" and "q2 ∈ snd d"
have "(⋀d. d ∈ set RepSets ⟹ snd d ⊆ fst d)"
using p5 by blast
have "q ∈ states M"
by (metis (no_types, lifting) ‹q ∈ fst ` d_reachable_states_with_preambles M› assms(1)
d_reachable_states_with_preambles_soundness(2) image_iff prod.collapse)
have "d ∈ set RepSets"
using m_traversal_paths_with_witness_set[OF p4 ‹(⋀d. d ∈ set RepSets ⟹ snd d ⊆ fst d)› ‹q ∈ states M›, of m]
using ‹(p, d) ∈ m_traversal_paths_with_witness M q RepSets m› find_set
by force
have "fst d ⊆ states M"
and "snd d = fst d ∩ fst ` states_with_preambles"
and "⋀ q1 q2. q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}"
using p5[OF ‹d ∈ set RepSets›] by blast+
have "q1 ∈ fst d"
and "q2 ∈ fst d"
and "q1 ∈ fst ` d_reachable_states_with_preambles M"
and "q2 ∈ fst ` d_reachable_states_with_preambles M"
using ‹q1 ∈ snd d› ‹q2 ∈ snd d› unfolding ‹snd d = fst d ∩ fst ` states_with_preambles›
unfolding states_with_preambles_def by blast+
obtain A t1 t2 where "(A,t1,t2) ∈ atcs (q1, q2)"
using ‹⋀ q1 q2. q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}›[OF ‹q1 ∈ fst d› ‹q2 ∈ fst d› ‹q1 ≠ q2›]
by auto
then have "(q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
unfolding atcs_def using set_as_map_elem by force
then have "(q1,[],q2) ∈ pps_alt"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› ‹(p,(fst d, snd d)) ∈ m_traversal_paths_with_witness M q RepSets m›
unfolding pps_alt_def
by (metis (mono_tags, lifting) ‹q1 ∈ snd d› ‹q2 ∈ snd d› mem_Collect_eq)
then have "[] ∈ tps q1" and "q2 ∈ rd_targets (q1,[])"
unfolding tps_alt_def[OF ‹q1 ∈ fst ` d_reachable_states_with_preambles M›]
rd_targets_alt_def[OF ‹q1 ∈ fst ` d_reachable_states_with_preambles M›]
preamble_pair_tests_alt
by force+
have "(A,t2,t1) ∈ atcs (q2, q1)"
using p3 ‹(A,t1,t2) ∈ atcs (q1, q2)› by blast
then have "(q2, q1) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
unfolding atcs_def using set_as_map_elem by force
then have "(q2,[],q1) ∈ pps_alt"
using ‹q ∈ fst ` d_reachable_states_with_preambles M› ‹(p,(fst d, snd d)) ∈ m_traversal_paths_with_witness M q RepSets m›
unfolding pps_alt_def
by (metis (mono_tags, lifting) ‹q1 ∈ snd d› ‹q2 ∈ snd d› mem_Collect_eq)
then have "[] ∈ tps q2" and "q1 ∈ rd_targets (q2,[])"
unfolding tps_alt_def[OF ‹q2 ∈ fst ` d_reachable_states_with_preambles M›]
rd_targets_alt_def[OF ‹q2 ∈ fst ` d_reachable_states_with_preambles M›]
preamble_pair_tests_alt
by force+
then show "([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))"
using ‹[] ∈ tps q1› ‹q2 ∈ rd_targets (q1,[])›
by simp
qed
ultimately show "(∀ p1 p2 p3 . p=p1@p2@p3 ⟶ p2 ≠ [] ⟶ target q p1 ∈ fst d ⟶ target q (p1@p2) ∈ fst d ⟶ target q p1 ≠ target q (p1@p2) ⟶ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1)))
∧ (∀ p1 p2 q' . p=p1@p2 ⟶ q' ∈ image fst states_with_preambles ⟶ target q p1 ∈ fst d ⟶ q' ∈ fst d ⟶ target q p1 ≠ q' ⟶ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1)))
∧ (∀ q1 q2 . q1 ≠ q2 ⟶ q1 ∈ snd d ⟶ q2 ∈ snd d ⟶ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[])))"
by blast
qed
have "implies_completeness_for_repetition_sets (Test_Suite states_with_preambles tps rd_targets atcs) M m RepSets"
unfolding implies_completeness_for_repetition_sets.simps
using p1 p2 p3 p4 p5 p6 p7
by force
then show "implies_completeness (calculate_test_suite_for_repetition_sets M m RepSets) M m"
unfolding ‹calculate_test_suite_for_repetition_sets M m RepSets = Test_Suite states_with_preambles tps rd_targets atcs›
implies_completeness_def
by blast
show "is_finite_test_suite (calculate_test_suite_for_repetition_sets M m RepSets)"
proof -
have "finite states_with_preambles"
unfolding states_with_preambles_def d_reachable_states_with_preambles_def
using fsm_states_finite[of M] by simp
moreover have "⋀ q p. q ∈ fst ` states_with_preambles ⟹ finite (rd_targets (q, p))"
proof -
fix q p assume "q ∈ fst ` states_with_preambles"
then have "q ∈ fst ` d_reachable_states_with_preambles M" unfolding states_with_preambles_def by assumption
have *: "finite ((λ(q, p, y). ((q, p), y)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m) ∪
(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) ∪
preamble_pair_tests
(⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M.
(λ(p, rd, dr). dr) ` y)
(fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)))"
proof -
have * : "⋀ a b c f . finite (f ` (a ∪ b ∪ c)) = (finite (f`a) ∧ finite (f`b) ∧ finite (f`c))"
by (simp add: image_Un)
have "finite ((λ(q, p, y). ((q, p), y)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)))"
proof -
have "prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m) ⊆
(⋃ (p, rd, dr)∈m_traversal_paths_with_witness M q RepSets m . ⋃ (p1, p2) ∈ set (prefix_pairs p) .{(q, p1, target q p2), (q, p2, target q p1)})"
unfolding prefix_pair_tests.simps by blast
moreover have "finite (⋃ (p, rd, dr)∈m_traversal_paths_with_witness M q RepSets m . ⋃ (p1, p2) ∈ set (prefix_pairs p) .{(q, p1, target q p2), (q, p2, target q p1)})"
proof -
have "finite (m_traversal_paths_with_witness M q RepSets m)"
using m_traversal_paths_with_witness_finite[of M q "RepSets" m] by assumption
moreover have "⋀ p rd dr . finite (⋃ (p1, p2) ∈ set (prefix_pairs p) .{(q, p1, target q p2), (q, p2, target q p1)})"
by auto
ultimately show ?thesis by force
qed
ultimately show ?thesis using infinite_super by blast
qed
moreover have "finite ((λ(q, p, y). ((q, p), y)) ` (⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}.
preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)))"
proof -
have "finite (fst ` d_reachable_states_with_preambles M)" using ‹finite states_with_preambles› unfolding states_with_preambles_def by auto
moreover have "⋀ q . q∈fst ` d_reachable_states_with_preambles M ⟹ finite (⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}. preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
proof -
fix q assume "q∈fst ` d_reachable_states_with_preambles M"
have "finite {m_traversal_paths_with_witness M q RepSets m}" by simp
moreover have "⋀ mrsps . mrsps∈{m_traversal_paths_with_witness M q RepSets m} ⟹ finite (preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
proof -
fix mrsps assume "mrsps∈{m_traversal_paths_with_witness M q RepSets m}"
then have *: "mrsps = m_traversal_paths_with_witness M q RepSets m" by simp
have "preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)
⊆ (⋃ (p,rd,dr) ∈ m_traversal_paths_with_witness M q RepSets m . ⋃ q2 ∈ (fst ` d_reachable_states_with_preambles M) . (⋃ p1 ∈ set (prefixes p) . {(q,p1,q2), (q2,[],(target q p1))}))"
unfolding preamble_prefix_tests_def * prefixes_set by blast
moreover have "finite (⋃ (p,rd,dr) ∈ m_traversal_paths_with_witness M q RepSets m . ⋃ q2 ∈ (fst ` d_reachable_states_with_preambles M) . (⋃ p1 ∈ set (prefixes p) . {(q,p1,q2), (q2,[],(target q p1))}))"
proof -
have "finite (m_traversal_paths_with_witness M q RepSets m)"
using m_traversal_paths_with_witness_finite by metis
moreover have "⋀ p rd dr . (p,rd,dr) ∈ m_traversal_paths_with_witness M q RepSets m ⟹ finite (⋃ q2 ∈ (fst ` d_reachable_states_with_preambles M) . (⋃ p1 ∈ set (prefixes p) . {(q,p1,q2), (q2,[],(target q p1))}))"
using ‹finite (fst ` d_reachable_states_with_preambles M)› by blast
ultimately show ?thesis by force
qed
ultimately show "finite (preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))" using infinite_super by blast
qed
ultimately show "finite (⋃mrsps∈{m_traversal_paths_with_witness M q RepSets m}. preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))" by force
qed
ultimately show ?thesis by blast
qed
moreover have "finite ((λ(q, p, y). ((q, p), y)) ` (preamble_pair_tests
(⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M.
(λ(p, rd, dr). dr) ` y)
(fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)))"
proof -
have "finite (⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M.
(λ(p, rd, dr). dr) ` y)"
proof -
have *: "(⋃(q, y)∈(λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
fst ` d_reachable_states_with_preambles M.
(λ(p, rd, dr). dr) ` y) =
(⋃ q ∈ fst ` d_reachable_states_with_preambles M . ⋃ (p, rd, dr) ∈ m_traversal_paths_with_witness M q RepSets m . {dr})"
by force
have "finite (⋃ q ∈ fst ` d_reachable_states_with_preambles M . ⋃ (p, rd, dr) ∈ m_traversal_paths_with_witness M q RepSets m . {dr})"
proof -
have "finite (fst ` d_reachable_states_with_preambles M)"
using ‹finite states_with_preambles› unfolding states_with_preambles_def by auto
moreover have "⋀q . q ∈ fst ` d_reachable_states_with_preambles M ⟹ finite (⋃ (p, rd, dr) ∈ m_traversal_paths_with_witness M q RepSets m . {dr})"
proof -
fix q assume "q ∈ fst ` d_reachable_states_with_preambles M"
have "finite (m_traversal_paths_with_witness M q RepSets m)"
using m_traversal_paths_with_witness_finite by metis
moreover have "⋀ p rd dr . (p, rd, dr) ∈ m_traversal_paths_with_witness M q RepSets m ⟹ finite {dr}"
by simp
ultimately show "finite (⋃ (p, rd, dr) ∈ m_traversal_paths_with_witness M q RepSets m . {dr})"
by force
qed
ultimately show ?thesis by blast
qed
then show ?thesis unfolding * by assumption
qed
moreover have "finite (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
proof -
have "(fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M) ⊆ states M × states M"
unfolding r_distinguishable_state_pairs_with_separators_def by auto
moreover have "finite (states M × states M)"
using fsm_states_finite by auto
ultimately show ?thesis using infinite_super by blast
qed
ultimately show ?thesis
unfolding preamble_pair_tests.simps by blast
qed
ultimately show ?thesis
unfolding * by blast
qed
show "finite (rd_targets (q, p))"
unfolding rd_targets_alt_def[OF ‹q ∈ fst ` d_reachable_states_with_preambles M›]
using finite_snd_helper[of _ q p, OF *] by assumption
qed
moreover have "⋀ q q'. finite (atcs (q, q'))"
proof -
fix q q'
show "finite (atcs (q,q'))" proof (cases "set_as_map ((λ((q1, q2), A). ((q1, q2), A, Inr q1:: ('a × 'a) + 'a, Inr q2 :: ('a × 'a) + 'a)) ` r_distinguishable_state_pairs_with_separators M) (q, q')")
case None
then have "atcs (q, q') = {}" unfolding atcs_def by auto
then show ?thesis by auto
next
case (Some a)
then have "atcs (q, q') = a" unfolding atcs_def by auto
then have *: "atcs (q, q') = {z. ((q, q'), z) ∈ (λ((q1, q2), A). ((q1, q2), A, Inr q1:: ('a × 'a) + 'a, Inr q2:: ('a × 'a) + 'a)) ` r_distinguishable_state_pairs_with_separators M}" using Some unfolding set_as_map_def
by (metis (no_types, lifting) option.distinct(1) option.inject)
have "finite (r_distinguishable_state_pairs_with_separators M)"
proof -
have "r_distinguishable_state_pairs_with_separators M ⊆ (⋃ q1 ∈ states M . ⋃ q2 ∈ states M . {((q1,q2), the (state_separator_from_s_states M q1 q2)), ((q1,q2), the (state_separator_from_s_states M q2 q1))})"
proof
fix x assume "x ∈ r_distinguishable_state_pairs_with_separators M"
then obtain q1 q2 Sep where "x = ((q1,q2),Sep)"
and "q1 ∈ states M"
and "q2 ∈ states M"
and "(q1 < q2 ∧ state_separator_from_s_states M q1 q2 = Some Sep) ∨ (q2 < q1 ∧ state_separator_from_s_states M q2 q1 = Some Sep)"
unfolding r_distinguishable_state_pairs_with_separators_def by blast
then consider "state_separator_from_s_states M q1 q2 = Some Sep" | "state_separator_from_s_states M q2 q1 = Some Sep" by blast
then show "x ∈ (⋃ q1 ∈ states M . ⋃ q2 ∈ states M . {((q1,q2), the (state_separator_from_s_states M q1 q2)), ((q1,q2), the (state_separator_from_s_states M q2 q1))})"
using ‹q1 ∈ states M› ‹q2 ∈ states M› unfolding ‹x = ((q1,q2),Sep)› by (cases; force)
qed
moreover have "finite (⋃ q1 ∈ states M . ⋃ q2 ∈ states M . {((q1,q2), the (state_separator_from_s_states M q1 q2)), ((q1,q2), the (state_separator_from_s_states M q2 q1))})"
using fsm_states_finite[of M] by force
ultimately show ?thesis using infinite_super by blast
qed
then show ?thesis unfolding * by (simp add: finite_snd_helper)
qed
qed
ultimately show ?thesis
unfolding ‹calculate_test_suite_for_repetition_sets M m RepSets = Test_Suite states_with_preambles tps rd_targets atcs›
is_finite_test_suite.simps
by blast
qed
qed
subsection ‹Two Complete Example Implementations›
subsubsection ‹Naive Repetition Set Strategy›
definition calculate_test_suite_naive :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ ('a,'b,'c, ('a × 'a) + 'a) test_suite" where
"calculate_test_suite_naive M m = calculate_test_suite_for_repetition_sets M m (maximal_repetition_sets_from_separators_list_naive M)"
definition calculate_test_suite_naive_as_io_sequences :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ ('b × 'c) list set" where
"calculate_test_suite_naive_as_io_sequences M m = test_suite_to_io_maximal M (calculate_test_suite_naive M m)"
lemma calculate_test_suite_naive_completeness :
fixes M :: "('a::linorder,'b::linorder,'c) fsm"
assumes "observable M"
and "observable M'"
and "inputs M' = inputs M"
and "inputs M ≠ {}"
and "completely_specified M"
and "completely_specified M'"
and "size M' ≤ m"
shows "(L M' ⊆ L M) ⟷ passes_test_suite M (calculate_test_suite_naive M m) M'"
and "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' (calculate_test_suite_naive_as_io_sequences M m)"
proof -
have "⋀q. q ∈ FSM.states M ⟹ ∃d∈set (maximal_repetition_sets_from_separators_list_naive M). q ∈ fst d"
unfolding maximal_repetition_sets_from_separators_list_naive_def Let_def
by (metis (mono_tags, lifting) list.set_map maximal_pairwise_r_distinguishable_state_sets_from_separators_code maximal_repetition_sets_from_separators_code maximal_repetition_sets_from_separators_cover)
moreover have "⋀d. d ∈ set (maximal_repetition_sets_from_separators_list_naive M) ⟹ fst d ⊆ states M ∧ (snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ d q1 q2. d ∈ set (maximal_repetition_sets_from_separators_list_naive M) ⟹ q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
proof
fix d assume "d ∈ set (maximal_repetition_sets_from_separators_list_naive M)"
then have "d ∈ maximal_repetition_sets_from_separators M"
by (simp add: maximal_repetition_sets_from_separators_code_alt)
then show "fst d ⊆ states M" and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ q1 q2 . q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
unfolding maximal_repetition_sets_from_separators_def
maximal_pairwise_r_distinguishable_state_sets_from_separators_def
pairwise_r_distinguishable_state_sets_from_separators_def
by force+
qed
ultimately have "implies_completeness (calculate_test_suite_naive M m) M m"
and "is_finite_test_suite (calculate_test_suite_naive M m)"
using calculate_test_suite_for_repetition_sets_sufficient_and_finite[OF ‹observable M› ‹completely_specified M› ‹inputs M ≠ {}›]
unfolding calculate_test_suite_naive_def by force+
then show "(L M' ⊆ L M) ⟷ passes_test_suite M (calculate_test_suite_naive M m) M'"
and "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' (calculate_test_suite_naive_as_io_sequences M m)"
using passes_test_suite_completeness[OF _ assms]
passes_test_suite_as_maximal_sequences_completeness[OF _ _ assms]
unfolding calculate_test_suite_naive_as_io_sequences_def
by blast+
qed
definition calculate_test_suite_naive_as_io_sequences_with_assumption_check :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ String.literal + (('b × 'c) list set)" where
"calculate_test_suite_naive_as_io_sequences_with_assumption_check M m =
(if inputs M ≠ {}
then if observable M
then if completely_specified M
then (Inr (test_suite_to_io_maximal M (calculate_test_suite_naive M m)))
else (Inl (STR ''specification is not completely specified''))
else (Inl (STR ''specification is not observable''))
else (Inl (STR ''specification has no inputs'')))"
lemma calculate_test_suite_naive_as_io_sequences_with_assumption_check_completeness :
fixes M :: "('a::linorder,'b::linorder,'c) fsm"
assumes "observable M'"
and "inputs M' = inputs M"
and "completely_specified M'"
and "size M' ≤ m"
and "calculate_test_suite_naive_as_io_sequences_with_assumption_check M m = Inr ts"
shows "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' ts"
proof -
have "inputs M ≠ {}"
and "observable M"
and "completely_specified M"
using ‹calculate_test_suite_naive_as_io_sequences_with_assumption_check M m = Inr ts›
unfolding calculate_test_suite_naive_as_io_sequences_with_assumption_check_def
by (meson Inl_Inr_False)+
then have "ts = (test_suite_to_io_maximal M (calculate_test_suite_naive M m))"
using ‹calculate_test_suite_naive_as_io_sequences_with_assumption_check M m = Inr ts›
unfolding calculate_test_suite_naive_as_io_sequences_with_assumption_check_def
by (metis sum.inject(2))
then show ?thesis
using calculate_test_suite_naive_completeness(2)[OF ‹observable M› assms(1,2) ‹inputs M ≠ {}›
‹completely_specified M› assms(3,4)]
unfolding calculate_test_suite_naive_as_io_sequences_def
by simp
qed
subsubsection ‹Greedy Repetition Set Strategy›
definition calculate_test_suite_greedy :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ ('a,'b,'c, ('a × 'a) + 'a) test_suite" where
"calculate_test_suite_greedy M m = calculate_test_suite_for_repetition_sets M m (maximal_repetition_sets_from_separators_list_greedy M)"
definition calculate_test_suite_greedy_as_io_sequences :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ ('b × 'c) list set" where
"calculate_test_suite_greedy_as_io_sequences M m = test_suite_to_io_maximal M (calculate_test_suite_greedy M m)"
lemma calculate_test_suite_greedy_completeness :
fixes M :: "('a::linorder,'b::linorder,'c) fsm"
assumes "observable M"
and "observable M'"
and "inputs M' = inputs M"
and "inputs M ≠ {}"
and "completely_specified M"
and "completely_specified M'"
and "size M' ≤ m"
shows "(L M' ⊆ L M) ⟷ passes_test_suite M (calculate_test_suite_greedy M m) M'"
and "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' (calculate_test_suite_greedy_as_io_sequences M m)"
proof -
have "⋀q. q ∈ FSM.states M ⟹ ∃d∈set (maximal_repetition_sets_from_separators_list_greedy M). q ∈ fst d"
unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def
using greedy_pairwise_r_distinguishable_state_sets_from_separators_cover[of _ M]
by simp
moreover have "⋀d. d ∈ set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ fst d ⊆ states M ∧ (snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ d q1 q2. d ∈ set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
proof
fix d assume "d ∈ set (maximal_repetition_sets_from_separators_list_greedy M)"
then have "fst d ∈ set (greedy_pairwise_r_distinguishable_state_sets_from_separators M)"
and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def by force+
then have "fst d ∈ pairwise_r_distinguishable_state_sets_from_separators M"
using greedy_pairwise_r_distinguishable_state_sets_from_separators_soundness by blast
then show "fst d ⊆ states M" and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ q1 q2 . q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using ‹(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)›
unfolding pairwise_r_distinguishable_state_sets_from_separators_def
by force+
qed
ultimately have "implies_completeness (calculate_test_suite_greedy M m) M m"
and "is_finite_test_suite (calculate_test_suite_greedy M m)"
using calculate_test_suite_for_repetition_sets_sufficient_and_finite[OF ‹observable M› ‹completely_specified M› ‹inputs M ≠ {}›]
unfolding calculate_test_suite_greedy_def by force+
then show "(L M' ⊆ L M) ⟷ passes_test_suite M (calculate_test_suite_greedy M m) M'"
and "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' (calculate_test_suite_greedy_as_io_sequences M m)"
using passes_test_suite_completeness[OF _ assms]
passes_test_suite_as_maximal_sequences_completeness[OF _ _ assms]
unfolding calculate_test_suite_greedy_as_io_sequences_def
by blast+
qed
definition calculate_test_suite_greedy_as_io_sequences_with_assumption_check :: "('a::linorder,'b::linorder,'c) fsm ⇒ nat ⇒ String.literal + (('b × 'c) list set)" where
"calculate_test_suite_greedy_as_io_sequences_with_assumption_check M m =
(if inputs M ≠ {}
then if observable M
then if completely_specified M
then (Inr (test_suite_to_io_maximal M (calculate_test_suite_greedy M m)))
else (Inl (STR ''specification is not completely specified''))
else (Inl (STR ''specification is not observable''))
else (Inl (STR ''specification has no inputs'')))"
lemma calculate_test_suite_greedy_as_io_sequences_with_assumption_check_completeness :
fixes M :: "('a::linorder,'b::linorder,'c) fsm"
assumes "observable M'"
and "inputs M' = inputs M"
and "completely_specified M'"
and "size M' ≤ m"
and "calculate_test_suite_greedy_as_io_sequences_with_assumption_check M m = Inr ts"
shows "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' ts"
proof -
have "inputs M ≠ {}"
and "observable M"
and "completely_specified M"
using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M m = Inr ts›
unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def
by (meson Inl_Inr_False)+
then have "ts = (test_suite_to_io_maximal M (calculate_test_suite_greedy M m))"
using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M m = Inr ts›
unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def
by (metis sum.inject(2))
then show ?thesis
using calculate_test_suite_greedy_completeness(2)[OF ‹observable M› assms(1,2) ‹inputs M ≠ {}›
‹completely_specified M› assms(3,4)]
unfolding calculate_test_suite_greedy_as_io_sequences_def
by simp
qed
end