Theory Helper_Algorithms
section ‹Helper Algorithms›
text ‹This theory contains several algorithms used to calculate components of a test suite.›
theory Helper_Algorithms
imports State_Separator State_Preamble
begin
subsection ‹Calculating r-distinguishable State Pairs with Separators›
definition r_distinguishable_state_pairs_with_separators ::
"('a::linorder,'b::linorder,'c) fsm ⇒ (('a × 'a) × (('a × 'a) + 'a,'b,'c) fsm) set"
where
"r_distinguishable_state_pairs_with_separators M =
{((q1,q2),Sep) | q1 q2 Sep . q1 ∈ states M
∧ q2 ∈ states M
∧ ((q1 < q2 ∧ state_separator_from_s_states M q1 q2 = Some Sep)
∨ (q2 < q1 ∧ state_separator_from_s_states M q2 q1 = Some Sep)) }"
lemma r_distinguishable_state_pairs_with_separators_alt_def :
"r_distinguishable_state_pairs_with_separators M =
⋃ (image (λ ((q1,q2),A) . {((q1,q2),the A),((q2,q1),the A)})
(Set.filter (λ (qq,A) . A ≠ None)
(image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))))"
(is "?P1 = ?P2")
proof -
have "⋀ x . x ∈ ?P1 ⟹ x ∈ ?P2"
proof -
fix x assume "x ∈ ?P1"
then obtain q1 q2 A where "x = ((q1,q2),A)"
by (metis eq_snd_iff)
then have "((q1,q2),A) ∈ ?P1" using ‹x ∈ ?P1› by auto
then have "q1 ∈ states M"
and "q2 ∈ states M"
and "((q1 < q2 ∧ state_separator_from_s_states M q1 q2 = Some A)
∨ (q2 < q1 ∧ state_separator_from_s_states M q2 q1 = Some A))"
unfolding r_distinguishable_state_pairs_with_separators_def by blast+
then consider (a) "q1 < q2 ∧ state_separator_from_s_states M q1 q2 = Some A" |
(b) "q2 < q1 ∧ state_separator_from_s_states M q2 q1 = Some A"
by blast
then show "x ∈ ?P2"
using ‹q1 ∈ states M› ‹q2 ∈ states M› unfolding ‹x = ((q1,q2),A)› by (cases; force)
qed
moreover have "⋀ x . x ∈ ?P2 ⟹ x ∈ ?P1"
proof -
fix x assume "x ∈ ?P2"
then obtain q1 q2 A where "x = ((q1,q2),A)"
by (metis eq_snd_iff)
then have "((q1,q2),A) ∈ ?P2" using ‹x ∈ ?P2› by auto
then obtain q1' q2' A' where "((q1,q2),A) ∈ {((q1',q2'),the A'),((q2',q1'),the A')}"
and "A' ≠ None"
and "((q1',q2'), A') ∈ (image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))"
by force
then have "A' = Some A"
by (metis (no_types, lifting) empty_iff insert_iff old.prod.inject option.collapse)
moreover have "A' = state_separator_from_s_states M q1' q2'"
and "q1' < q2'"
and "q1' ∈ states M"
and "q2' ∈ states M"
using ‹((q1',q2'), A') ∈ (image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))›
by force+
ultimately have "state_separator_from_s_states M q1' q2' = Some A" by simp
consider "((q1',q2'),the A') = ((q1,q2),A)" | "((q1',q2'),the A') = ((q2,q1),A)"
using ‹((q1,q2),A) ∈ {((q1',q2'),the A'),((q2',q1'),the A')}›
by force
then show "x ∈ ?P1"
proof cases
case 1
then have *: "q1' = q1" and **: "q2' = q2" by auto
show ?thesis
using ‹q1' ∈ states M› ‹q2' ∈ states M› ‹q1' < q2'› ‹state_separator_from_s_states M q1' q2' = Some A›
unfolding r_distinguishable_state_pairs_with_separators_def
unfolding * ** ‹x = ((q1,q2),A)› by blast
next
case 2
then have *: "q1' = q2" and **: "q2' = q1" by auto
show ?thesis
using ‹q1' ∈ states M› ‹q2' ∈ states M› ‹q1' < q2'› ‹state_separator_from_s_states M q1' q2' = Some A›
unfolding r_distinguishable_state_pairs_with_separators_def
unfolding * ** ‹x = ((q1,q2),A)› by blast
qed
qed
ultimately show ?thesis by blast
qed
lemma r_distinguishable_state_pairs_with_separators_code[code] :
"r_distinguishable_state_pairs_with_separators M =
set (concat (map
(λ ((q1,q2),A) . [((q1,q2),the A),((q2,q1),the A)])
(filter (λ (qq,A) . A ≠ None)
(map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(filter (λ (q1,q2) . q1 < q2)
(List.product(states_as_list M) (states_as_list M)))))))"
(is "r_distinguishable_state_pairs_with_separators M = ?C2")
proof -
let ?C1 = "⋃ (image (λ ((q1,q2),A) . {((q1,q2),the A),((q2,q1),the A)})
(Set.filter (λ (qq,A) . A ≠ None)
(image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))))"
have "r_distinguishable_state_pairs_with_separators M = ?C1"
using r_distinguishable_state_pairs_with_separators_alt_def by assumption
also have "… = ?C2"
proof
show "?C1 ⊆ ?C2"
proof
fix x assume "x ∈ ?C1"
then obtain q1 q2 A where "x = ((q1,q2),A)"
by (metis eq_snd_iff)
then have "((q1,q2),A) ∈ ?C1" using ‹x ∈ ?C1› by auto
then obtain q1' q2' A' where "((q1,q2),A) ∈ {((q1',q2'),the A'),((q2',q1'),the A')}"
and "A' ≠ None"
and "((q1',q2'), A') ∈ (image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))"
by force
then have "A' = Some A"
by (metis (no_types, lifting) empty_iff insert_iff old.prod.inject option.collapse)
moreover have "A' = state_separator_from_s_states M q1' q2'"
and "q1' < q2'"
and "q1' ∈ states M"
and "q2' ∈ states M"
using ‹((q1',q2'), A') ∈ (image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))›
by force+
ultimately have "state_separator_from_s_states M q1' q2' = Some A"
and "(q1',q2') ∈ set (filter (λ (q1,q2) . q1 < q2) (List.product(states_as_list M) (states_as_list M)))"
unfolding states_as_list_set[symmetric] by auto
then have "((q1',q2'),A') ∈ set (filter (λ (qq,A) . A ≠ None)
(map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(filter (λ (q1,q2) . q1 < q2)
(List.product(states_as_list M) (states_as_list M)))))"
using ‹A' = state_separator_from_s_states M q1' q2'› ‹A' = Some A› by force
have scheme1: "⋀ f xs x . x ∈ set xs ⟹ f x ∈ set (map f xs)" by auto
have scheme2: "⋀ x xs xss . xs ∈ set xss ⟹ x ∈ set xs ⟹ x ∈ set (concat xss)" by auto
have *:"[((q1',q2'),the A'),((q2',q1'),the A')] ∈
set (map (λ ((q1,q2),A) . [((q1,q2),the A),((q2,q1),the A)])
(filter (λ (qq,A) . A ≠ None)
(map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(filter (λ (q1,q2) . q1 < q2)
(List.product(states_as_list M) (states_as_list M))))))"
using scheme1[OF ‹((q1',q2'),A') ∈ set (filter (λ (qq,A) . A ≠ None) (map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2)) (filter (λ (q1,q2) . q1 < q2) (List.product(states_as_list M) (states_as_list M)))))›, of "λ ((q1', q2'), A') . [((q1',q2'),the A'),((q2',q1'),the A')]"]
by force
have **: "((q1,q2),A) ∈ set [((q1',q2'),the A'),((q2',q1'),the A')]"
using ‹((q1,q2),A) ∈ {((q1',q2'),the A'),((q2',q1'),the A')}› by auto
show "x ∈ ?C2"
unfolding ‹x = ((q1,q2),A)› using scheme2[OF * **] by assumption
qed
show "?C2 ⊆ ?C1"
proof
fix x assume "x ∈ ?C2"
obtain q1q2A where "x ∈ set ((λ ((q1', q2'), A') . [((q1',q2'),the A'),((q2',q1'),the A')]) q1q2A)"
and "q1q2A ∈ set (filter (λ (qq,A) . A ≠ None)
(map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(filter (λ (q1,q2) . q1 < q2)
(List.product(states_as_list M) (states_as_list M)))))"
using concat_map_elem[OF ‹x ∈ ?C2›] by blast
moreover obtain q1 q2 A where "q1q2A = ((q1,q2),A)"
by (metis prod.collapse)
ultimately have "x ∈ set [((q1,q2),the A),((q2,q1),the A)]"
and "((q1,q2),A) ∈ set (filter (λ (qq,A) . A ≠ None)
(map (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(filter (λ (q1,q2) . q1 < q2)
(List.product(states_as_list M) (states_as_list M)))))"
by force+
then have "A = state_separator_from_s_states M q1 q2"
and "A ≠ None"
and "(q1,q2) ∈ set (filter (λ (q1,q2) . q1 < q2) (List.product(states_as_list M) (states_as_list M)))"
by auto
then have "q1 < q2" and "q1 ∈ states M" and "q2 ∈ states M"
unfolding states_as_list_set[symmetric] by auto
then have "(q1,q2) ∈ Set.filter (λ(q1, q2). q1 < q2) (FSM.states M × FSM.states M)"
by auto
then have "((q1,q2),A) ∈ (Set.filter (λ (qq,A) . A ≠ None)
(image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M))))"
using ‹A ≠ None› unfolding ‹A = state_separator_from_s_states M q1 q2› by auto
then have "{((q1,q2),the A),((q2,q1),the A)} ∈
(image (λ ((q1,q2),A) . {((q1,q2),the A),((q2,q1),the A)})
(Set.filter (λ (qq,A) . A ≠ None)
(image (λ (q1,q2) . ((q1,q2),state_separator_from_s_states M q1 q2))
(Set.filter (λ (q1,q2) . q1 < q2) (states M × states M)))))"
by (metis (no_types, lifting) ‹q1q2A = ((q1, q2), A)› case_prod_conv image_iff)
then show "x ∈ ?C1"
using ‹x ∈ set [((q1,q2),the A),((q2,q1),the A)]›
by (metis (no_types, lifting) UnionI list.simps(15) set_empty2)
qed
qed
finally show ?thesis .
qed
lemma r_distinguishable_state_pairs_with_separators_same_pair_same_separator :
assumes "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M"
and "((q1,q2),A') ∈ r_distinguishable_state_pairs_with_separators M"
shows "A = A'"
using assms unfolding r_distinguishable_state_pairs_with_separators_def
by force
lemma r_distinguishable_state_pairs_with_separators_sym_pair_same_separator :
assumes "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M"
and "((q2,q1),A') ∈ r_distinguishable_state_pairs_with_separators M"
shows "A = A'"
using assms unfolding r_distinguishable_state_pairs_with_separators_def
by force
lemma r_distinguishable_state_pairs_with_separators_elem_is_separator:
assumes "((q1,q2),A) ∈ r_distinguishable_state_pairs_with_separators M"
and "observable M"
and "completely_specified M"
shows "is_separator M q1 q2 A (Inr q1) (Inr q2)"
proof -
have *:"q1 ∈ states M"
and **:"q2 ∈ states M"
and ***:"q1 ≠ q2"
and ****: "q2≠q1"
and *****: "state_separator_from_s_states M q1 q2 = Some A ∨ state_separator_from_s_states M q2 q1 = Some A"
using assms(1) unfolding r_distinguishable_state_pairs_with_separators_def by auto
from ***** have "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A
∨ is_state_separator_from_canonical_separator (canonical_separator M q2 q1) q2 q1 A"
using state_separator_from_s_states_soundness[of M q1 q2 A, OF _ * ** assms(3)]
using state_separator_from_s_states_soundness[of M q2 q1 A, OF _ ** * assms(3)] by auto
then show ?thesis
using state_separator_from_canonical_separator_is_separator[of M q1 q2 A, OF _ ‹observable M› * ** ***]
using state_separator_from_canonical_separator_is_separator[of M q2 q1 A, OF _ ‹observable M› ** * ****]
using is_separator_sym[of M q2 q1 A "Inr q2" "Inr q1"] by auto
qed
subsection ‹Calculating Pairwise r-distinguishable Sets of States›
definition pairwise_r_distinguishable_state_sets_from_separators :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a set set" where
"pairwise_r_distinguishable_state_sets_from_separators M
= { S . S ⊆ states M ∧ (∀ q1 ∈ S . ∀ q2 ∈ S . q1 ≠ q2 ⟶ (q1,q2) ∈ image fst (r_distinguishable_state_pairs_with_separators M))}"
definition pairwise_r_distinguishable_state_sets_from_separators_list :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a set list" where
"pairwise_r_distinguishable_state_sets_from_separators_list M =
(let RDS = image fst (r_distinguishable_state_pairs_with_separators M)
in filter (λ S . ∀ q1 ∈ S . ∀ q2 ∈ S . q1 ≠ q2 ⟶ (q1,q2) ∈ RDS)
(map set (pow_list (states_as_list M))))"
lemma pairwise_r_distinguishable_state_sets_from_separators_code[code] :
"pairwise_r_distinguishable_state_sets_from_separators M = set (pairwise_r_distinguishable_state_sets_from_separators_list M)"
using pow_list_set[of "states_as_list M"]
unfolding states_as_list_set[of M]
pairwise_r_distinguishable_state_sets_from_separators_def
pairwise_r_distinguishable_state_sets_from_separators_list_def
by auto
lemma pairwise_r_distinguishable_state_sets_from_separators_cover :
assumes "q ∈ states M"
shows "∃ S ∈ (pairwise_r_distinguishable_state_sets_from_separators M) . q ∈ S"
unfolding pairwise_r_distinguishable_state_sets_from_separators_def using assms by blast
definition maximal_pairwise_r_distinguishable_state_sets_from_separators :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a set set" where
"maximal_pairwise_r_distinguishable_state_sets_from_separators M
= { S . S ∈ (pairwise_r_distinguishable_state_sets_from_separators M)
∧ (∄ S' . S' ∈ (pairwise_r_distinguishable_state_sets_from_separators M) ∧ S ⊂ S')}"
definition maximal_pairwise_r_distinguishable_state_sets_from_separators_list :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a set list" where
"maximal_pairwise_r_distinguishable_state_sets_from_separators_list M =
remove_subsets (pairwise_r_distinguishable_state_sets_from_separators_list M)"
lemma maximal_pairwise_r_distinguishable_state_sets_from_separators_code[code] :
"maximal_pairwise_r_distinguishable_state_sets_from_separators M
= set (maximal_pairwise_r_distinguishable_state_sets_from_separators_list M)"
unfolding maximal_pairwise_r_distinguishable_state_sets_from_separators_list_def
Let_def remove_subsets_set pairwise_r_distinguishable_state_sets_from_separators_code[symmetric]
maximal_pairwise_r_distinguishable_state_sets_from_separators_def
by blast
lemma maximal_pairwise_r_distinguishable_state_sets_from_separators_cover :
assumes "q ∈ states M"
shows "∃ S ∈ (maximal_pairwise_r_distinguishable_state_sets_from_separators M ). q ∈ S"
proof -
have *: "{q} ∈ (pairwise_r_distinguishable_state_sets_from_separators M)"
unfolding pairwise_r_distinguishable_state_sets_from_separators_def using assms by blast
have **: "finite (pairwise_r_distinguishable_state_sets_from_separators M)"
unfolding pairwise_r_distinguishable_state_sets_from_separators_def by (simp add: fsm_states_finite)
have "(maximal_pairwise_r_distinguishable_state_sets_from_separators M) =
{S ∈ (pairwise_r_distinguishable_state_sets_from_separators M).
¬(∃ S' ∈ (pairwise_r_distinguishable_state_sets_from_separators M) . S ⊂ S')}"
unfolding maximal_pairwise_r_distinguishable_state_sets_from_separators_def
pairwise_r_distinguishable_state_sets_from_separators_def
by metis
then have "(maximal_pairwise_r_distinguishable_state_sets_from_separators M) =
{S ∈ (pairwise_r_distinguishable_state_sets_from_separators M) .
(∀ S' ∈ (pairwise_r_distinguishable_state_sets_from_separators M) . ¬ S ⊂ S')}"
by blast
moreover have "∃ S ∈ {S ∈ (pairwise_r_distinguishable_state_sets_from_separators M) .
(∀ S' ∈ (pairwise_r_distinguishable_state_sets_from_separators M) . ¬ S ⊂ S')} . q ∈ S"
using maximal_set_cover[OF ** *]
by blast
ultimately show ?thesis
by blast
qed
subsection ‹Calculating d-reachable States with Preambles›
definition d_reachable_states_with_preambles :: "('a::linorder,'b::linorder,'c) fsm ⇒ ('a × ('a,'b,'c) fsm) set" where
"d_reachable_states_with_preambles M =
image (λ qp . (fst qp, the (snd qp)))
(Set.filter (λ qp . snd qp ≠ None)
(image (λ q . (q, calculate_state_preamble_from_input_choices M q))
(states M)))"
lemma d_reachable_states_with_preambles_exhaustiveness :
assumes "∃ P . is_preamble P M q"
and "q ∈ states M"
shows "∃ P . (q,P) ∈ (d_reachable_states_with_preambles M)"
using calculate_state_preamble_from_input_choices_exhaustiveness[OF assms(1)] assms(2)
unfolding d_reachable_states_with_preambles_def by force
lemma d_reachable_states_with_preambles_soundness :
assumes "(q,P) ∈ (d_reachable_states_with_preambles M)"
and "observable M"
shows "is_preamble P M q"
and "q ∈ states M"
using assms(1) calculate_state_preamble_from_input_choices_soundness[of M q P]
unfolding d_reachable_states_with_preambles_def
using imageE by auto
subsection ‹Calculating Repetition Sets›
text ‹Repetition sets are sets of tuples each containing a maximal set of pairwise r-distinguishable
states and the subset of those states that have a preamble.›
definition maximal_repetition_sets_from_separators :: "('a::linorder,'b::linorder,'c) fsm ⇒ ('a set × 'a set) set" where
"maximal_repetition_sets_from_separators M
= {(S, S ∩ (image fst (d_reachable_states_with_preambles M))) | S .
S ∈ (maximal_pairwise_r_distinguishable_state_sets_from_separators M)}"
definition maximal_repetition_sets_from_separators_list_naive :: "('a::linorder,'b::linorder,'c) fsm ⇒ ('a set × 'a set) list" where
"maximal_repetition_sets_from_separators_list_naive M
= (let DR = (image fst (d_reachable_states_with_preambles M))
in map (λ S . (S, S ∩ DR)) (maximal_pairwise_r_distinguishable_state_sets_from_separators_list M))"
lemma maximal_repetition_sets_from_separators_code[code]:
"maximal_repetition_sets_from_separators M = (let DR = (image fst (d_reachable_states_with_preambles M))
in image (λ S . (S, S ∩ DR)) (maximal_pairwise_r_distinguishable_state_sets_from_separators M))"
unfolding maximal_repetition_sets_from_separators_def Let_def by force
lemma maximal_repetition_sets_from_separators_code_alt:
"maximal_repetition_sets_from_separators M = set (maximal_repetition_sets_from_separators_list_naive M)"
unfolding maximal_repetition_sets_from_separators_def
maximal_repetition_sets_from_separators_list_naive_def
maximal_pairwise_r_distinguishable_state_sets_from_separators_code
by force
subsubsection ‹Calculating Sub-Optimal Repetition Sets›
text ‹Finding maximal pairwise r-distinguishable subsets of the state set of some FSM is likely too expensive
for FSMs containing a large number of r-distinguishable pairs of states.
The following functions calculate only subset of all repetition sets while maintaining the
property that every state is contained in some repetition set.›
fun extend_until_conflict :: "('a × 'a) set ⇒ 'a list ⇒ 'a list ⇒ nat ⇒ 'a list" where
"extend_until_conflict non_confl_set candidates xs 0 = xs" |
"extend_until_conflict non_confl_set candidates xs (Suc k) = (case dropWhile (λ x . find (λ y . (x,y) ∉ non_confl_set) xs ≠ None) candidates of
[] ⇒ xs |
(c#cs) ⇒ extend_until_conflict non_confl_set cs (c#xs) k)"
lemma extend_until_conflict_retainment :
assumes "x ∈ set xs"
shows "x ∈ set (extend_until_conflict non_confl_set candidates xs k)"
using assms proof (induction k arbitrary: candidates xs)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case proof (cases "dropWhile (λ x . find (λ y . (x,y) ∉ non_confl_set) xs ≠ None) candidates")
case Nil
then show ?thesis
by (metis Suc.prems extend_until_conflict.simps(2) list.simps(4))
next
case (Cons c cs)
then show ?thesis
by (simp add: Suc.IH Suc.prems)
qed
qed
lemma extend_until_conflict_elem :
assumes "x ∈ set (extend_until_conflict non_confl_set candidates xs k)"
shows "x ∈ set xs ∨ x ∈ set candidates"
using assms proof (induction k arbitrary: candidates xs)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case proof (cases "dropWhile (λ x . find (λ y . (x,y) ∉ non_confl_set) xs ≠ None) candidates")
case Nil
then show ?thesis
by (metis Suc.prems extend_until_conflict.simps(2) list.simps(4))
next
case (Cons c cs)
then have "extend_until_conflict non_confl_set candidates xs (Suc k) = extend_until_conflict non_confl_set cs (c#xs) k"
by auto
then have "x ∈ set (c # xs) ∨ x ∈ set cs"
using Suc.IH[of cs "(c#xs)"] Suc.prems by auto
moreover have "set (c#cs) ⊆ set candidates"
using Cons by (metis set_dropWhileD subsetI)
ultimately show ?thesis
using set_ConsD by auto
qed
qed
lemma extend_until_conflict_no_conflicts :
assumes "x ∈ set (extend_until_conflict non_confl_set candidates xs k)"
and "y ∈ set (extend_until_conflict non_confl_set candidates xs k)"
and "x ∈ set xs ⟹ y ∈ set xs ⟹ (x,y) ∈ non_confl_set ∨ (y,x) ∈ non_confl_set"
and "x ≠ y"
shows "(x,y) ∈ non_confl_set ∨ (y,x) ∈ non_confl_set"
using assms proof (induction k arbitrary: candidates xs)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case proof (cases "dropWhile (λ x . find (λ y . (x,y) ∉ non_confl_set) xs ≠ None) candidates")
case Nil
then have "extend_until_conflict non_confl_set candidates xs (Suc k) = xs"
by (metis extend_until_conflict.simps(2) list.simps(4))
then show ?thesis
using Suc.prems by auto
next
case (Cons c cs)
then have "extend_until_conflict non_confl_set candidates xs (Suc k) = extend_until_conflict non_confl_set cs (c#xs) k"
by auto
then have xk: "x ∈ set (extend_until_conflict non_confl_set cs (c#xs) k)"
and yk: "y ∈ set (extend_until_conflict non_confl_set cs (c#xs) k)"
using Suc.prems by auto
have **: "x ∈ set (c#xs) ⟹ y ∈ set (c#xs) ⟹ (x,y) ∈ non_confl_set ∨ (y,x) ∈ non_confl_set"
proof -
have scheme: "⋀ P xs x xs' . dropWhile P xs = (x#xs') ⟹ ¬ P x"
by (simp add: dropWhile_eq_Cons_conv)
have "find (λ y . (c,y) ∉ non_confl_set) xs = None"
using scheme[OF Cons] by simp
then have *: "⋀ y . y ∈ set xs ⟹ (c,y) ∈ non_confl_set"
unfolding find_None_iff by blast
assume "x ∈ set (c#xs)" and "y ∈ set (c#xs)"
then consider (a1) "x = c ∧ y ∈ set xs" |
(a2) "y = c ∧ x ∈ set xs" |
(a3) "x ∈ set xs ∧ y ∈ set xs"
using ‹x ≠ y› by auto
then show ?thesis
using * Suc.prems(3) by (cases; auto)
qed
show ?thesis using Suc.IH[OF xk yk ** Suc.prems(4)] by blast
qed
qed
definition greedy_pairwise_r_distinguishable_state_sets_from_separators :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a set list" where
"greedy_pairwise_r_distinguishable_state_sets_from_separators M =
(let pwrds = image fst (r_distinguishable_state_pairs_with_separators M);
k = size M;
nL = states_as_list M
in map (λq . set (extend_until_conflict pwrds (remove1 q nL) [q] k)) nL)"
definition maximal_repetition_sets_from_separators_list_greedy :: "('a::linorder,'b::linorder,'c) fsm ⇒ ('a set × 'a set) list" where
"maximal_repetition_sets_from_separators_list_greedy M = (let DR = (image fst (d_reachable_states_with_preambles M))
in remdups (map (λ S . (S, S ∩ DR)) (greedy_pairwise_r_distinguishable_state_sets_from_separators M)))"
lemma greedy_pairwise_r_distinguishable_state_sets_from_separators_cover :
assumes "q ∈ states M"
shows "∃ S ∈ set (greedy_pairwise_r_distinguishable_state_sets_from_separators M). q ∈ S"
using assms extend_until_conflict_retainment[of q "[q]"]
unfolding states_as_list_set[symmetric] greedy_pairwise_r_distinguishable_state_sets_from_separators_def Let_def
by auto
lemma r_distinguishable_state_pairs_with_separators_sym :
assumes "(q1,q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
shows "(q2,q1) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using assms
unfolding r_distinguishable_state_pairs_with_separators_def
by force
lemma greedy_pairwise_r_distinguishable_state_sets_from_separators_soundness :
"set (greedy_pairwise_r_distinguishable_state_sets_from_separators M) ⊆ (pairwise_r_distinguishable_state_sets_from_separators M)"
proof
fix S assume "S ∈ set (greedy_pairwise_r_distinguishable_state_sets_from_separators M)"
then obtain q' where "q' ∈ states M"
and *: "S = set (extend_until_conflict (image fst (r_distinguishable_state_pairs_with_separators M))
(remove1 q' (states_as_list M))
[q']
(size M))"
unfolding greedy_pairwise_r_distinguishable_state_sets_from_separators_def Let_def states_as_list_set[symmetric]
by auto
have "S ⊆ states M"
proof
fix q assume "q ∈ S"
then have "q ∈ set (extend_until_conflict (image fst (r_distinguishable_state_pairs_with_separators M)) (remove1 q' (states_as_list M)) [q'] (size M))"
using * by auto
then show "q ∈ states M"
using extend_until_conflict_elem[of q "image fst (r_distinguishable_state_pairs_with_separators M)" "(remove1 q' (states_as_list M))" "[q']" "size M"]
using states_as_list_set ‹q' ∈ states M› by auto
qed
moreover have "⋀ q1 q2 . q1 ∈ S ⟹ q2 ∈ S ⟹ q1 ≠ q2 ⟹ (q1,q2) ∈ image fst (r_distinguishable_state_pairs_with_separators M)"
proof -
fix q1 q2 assume "q1 ∈ S" and "q2 ∈ S" and "q1 ≠ q2"
then have e1: "q1 ∈ set (extend_until_conflict (image fst (r_distinguishable_state_pairs_with_separators M)) (remove1 q' (states_as_list M)) [q'] (size M))"
and e2: "q2 ∈ set (extend_until_conflict (image fst (r_distinguishable_state_pairs_with_separators M)) (remove1 q' (states_as_list M)) [q'] (size M))"
unfolding * by simp+
have e3: "(q1 ∈ set [q'] ⟹ q2 ∈ set [q']
⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M
∨ (q2, q1) ∈ fst ` r_distinguishable_state_pairs_with_separators M)"
using ‹q1 ≠ q2› by auto
show "(q1,q2) ∈ image fst (r_distinguishable_state_pairs_with_separators M)"
using extend_until_conflict_no_conflicts[OF e1 e2 e3 ‹q1 ≠ q2›]
r_distinguishable_state_pairs_with_separators_sym[of q2 q1 M] by blast
qed
ultimately show "S ∈ (pairwise_r_distinguishable_state_sets_from_separators M)"
unfolding pairwise_r_distinguishable_state_sets_from_separators_def by blast
qed
end