Theory ASC_Suite
theory ASC_Suite
imports ASC_LB
begin
section ‹ Test suite generated by the Adaptive State Counting Algorithm ›
subsection ‹ Maximum length contained prefix ›
fun mcp :: "'a list ⇒ 'a list set ⇒ 'a list ⇒ bool" where
"mcp z W p = (prefix p z ∧ p ∈ W ∧
(∀ p' . (prefix p' z ∧ p' ∈ W) ⟶ length p' ≤ length p))"
lemma mcp_ex :
assumes "[] ∈ W"
and "finite W"
obtains p
where "mcp z W p"
proof -
let ?P = "{p . prefix p z ∧ p ∈ W}"
let ?maxP = "arg_max length (λ p . p ∈ ?P)"
have "finite {p . prefix p z}"
proof -
have "{p . prefix p z} ⊆ image (λ i . take i z) (set [0 ..< Suc (length z)])"
proof
fix p assume "p ∈ {p . prefix p z}"
then obtain i where "i ≤ length z ∧ p = take i z"
by (metis append_eq_conv_conj mem_Collect_eq prefix_def prefix_length_le)
then have "i < Suc (length z) ∧ p = take i z"
by simp
then show "p ∈ image (λ i . take i z) (set [0 ..< Suc (length z)])"
using atLeast_upt by blast
qed
then show ?thesis
using finite_surj by blast
qed
then have "finite ?P"
by simp
have "?P ≠ {}"
using Nil_prefix assms(1) by blast
have "∃ maxP ∈ ?P . ∀ p ∈ ?P . length p ≤ length maxP"
proof (rule ccontr)
assume "¬(∃ maxP ∈ ?P . ∀ p ∈ ?P . length p ≤ length maxP)"
then have "∀ p ∈ ?P . ∃ p' ∈ ?P . length p < length p'"
by (meson not_less)
then have "∀ l ∈ (image length ?P) . ∃ l' ∈ (image length ?P) . l < l'"
by auto
then have "infinite (image length ?P)"
by (metis (no_types, lifting) ‹?P ≠ {}› image_is_empty infinite_growing)
then have "infinite ?P"
by blast
then show "False"
using ‹finite ?P› by simp
qed
then obtain maxP where "maxP ∈ ?P" "∀ p ∈ ?P . length p ≤ length maxP"
by blast
then have "mcp z W maxP"
unfolding mcp.simps by blast
then show ?thesis
using that by auto
qed
lemma mcp_unique :
assumes "mcp z W p"
and "mcp z W p'"
shows "p = p'"
proof -
have "length p' ≤ length p"
using assms(1) assms(2) by auto
moreover have "length p ≤ length p'"
using assms(1) assms(2) by auto
ultimately have "length p' = length p"
by simp
moreover have "prefix p z"
using assms(1) by auto
moreover have "prefix p' z"
using assms(2) by auto
ultimately show ?thesis
by (metis append_eq_conv_conj prefixE)
qed
fun mcp' :: "'a list ⇒ 'a list set ⇒ 'a list" where
"mcp' z W = (THE p . mcp z W p)"
lemma mcp'_intro :
assumes "mcp z W p"
shows "mcp' z W = p"
using assms mcp_unique by (metis mcp'.elims theI_unique)
lemma mcp_prefix_of_suffix :
assumes "mcp (vs@xs) V vs"
and "prefix xs' xs"
shows "mcp (vs@xs') V vs"
proof (rule ccontr)
assume "¬ mcp (vs @ xs') V vs"
then have "¬ (prefix vs (vs @ xs') ∧ vs ∈ V ∧
(∀ p' . (prefix p' (vs @ xs') ∧ p' ∈ V) ⟶ length p' ≤ length vs))"
by auto
then have "¬ (∀ p' . (prefix p' (vs @ xs') ∧ p' ∈ V) ⟶ length p' ≤ length vs)"
using assms(1) by auto
then obtain vs' where "vs' ∈ V ∧ prefix vs' (vs@xs) ∧ length vs < length vs'"
by (meson assms(2) leI prefix_append prefix_order.dual_order.trans)
then have "¬ (mcp (vs@xs) V vs)"
by auto
then show "False"
using assms(1) by auto
qed
lemma minimal_sequence_to_failure_extending_mcp :
assumes "OFSM M1"
and "OFSM M2"
and "is_det_state_cover M2 V"
and "minimal_sequence_to_failure_extending V M1 M2 vs xs"
shows "mcp (map fst (vs@xs)) V (map fst vs)"
proof (rule ccontr)
assume "¬ mcp (map fst (vs @ xs)) V (map fst vs)"
moreover have "prefix (map fst vs) (map fst (vs @ xs))"
by auto
moreover have "(map fst vs) ∈ V"
using mstfe_prefix_input_in_V assms(4) by auto
ultimately obtain v' where "prefix v' (map fst (vs @ xs))"
"v' ∈ V"
"length v' > length (map fst vs)"
using leI by auto
then obtain x' where "(map fst (vs@xs)) = v'@x'"
using prefixE by blast
have "vs@xs ∈ L M1 - L M2"
using assms(4) unfolding minimal_sequence_to_failure_extending.simps sequence_to_failure.simps
by blast
then have "vs@xs ∈ L⇩i⇩n M1 {map fst (vs@xs)}"
by (meson DiffE insertI1 language_state_for_inputs_map_fst)
have "vs@xs ∈ L⇩i⇩n M1 {v'@x'}"
using ‹map fst (vs @ xs) = v' @ x'› ‹vs @ xs ∈ L⇩i⇩n M1 {map fst (vs @ xs)}›
by presburger
let ?vs' = "take (length v') (vs@xs)"
let ?xs' = "drop (length v') (vs@xs)"
have "vs@xs = ?vs'@?xs'"
by (metis append_take_drop_id)
have "?vs' ∈ L⇩i⇩n M1 V"
by (metis (no_types) DiffE ‹map fst (vs @ xs) = v' @ x'› ‹v' ∈ V› ‹vs @ xs ∈ L M1 - L M2›
append_eq_conv_conj append_take_drop_id language_state_for_inputs_map_fst
language_state_prefix take_map)
have "sequence_to_failure M1 M2 (?vs' @ ?xs')"
by (metis (full_types) ‹vs @ xs = take (length v') (vs @ xs) @ drop (length v') (vs @ xs)›
assms(4) minimal_sequence_to_failure_extending.simps)
have "length ?xs' < length xs"
using ‹length (map fst vs) < length v'› ‹prefix v' (map fst (vs @ xs))›
‹vs @ xs = take (length v') (vs @ xs) @ drop (length v') (vs @ xs)› prefix_length_le
by fastforce
show "False"
by (meson ‹length (drop (length v') (vs @ xs)) < length xs›
‹sequence_to_failure M1 M2 (take (length v') (vs @ xs) @ drop (length v') (vs @ xs))›
‹take (length v') (vs @ xs) ∈ L⇩i⇩n M1 V› assms(4)
minimal_sequence_to_failure_extending.elims(2))
qed
subsection ‹ Function N ›
text ‹
Function @{verbatim N} narrows the sets of reaction to the determinisitc state cover considered by
the adaptive state counting algorithm to contain only relevant sequences.
It is the main refinement of the original formulation of the algorithm as given in \<^cite>‹"hierons"›.
An example for the necessity for this refinement is given in \<^cite>‹"refinement"›.
›
fun N :: "('in × 'out) list ⇒ ('in, 'out, 'state) FSM ⇒ 'in list set ⇒ ('in × 'out) list set set"
where
"N io M V = { V'' ∈ Perm V M . (map fst (mcp' io V'')) = (mcp' (map fst io) V) }"
lemma N_nonempty :
assumes "is_det_state_cover M2 V"
and "OFSM M1"
and "OFSM M2"
and "asc_fault_domain M2 M1 m"
and "io ∈ L M1"
shows "N io M1 V ≠ {}"
proof -
have "[] ∈ V"
using assms(1) det_state_cover_empty by blast
have "inputs M1 = inputs M2"
using assms(4) by auto
have "is_det_state_cover M2 V"
using assms by auto
moreover have "finite (nodes M2)"
using assms(3) by auto
moreover have "d_reachable M2 (initial M2) ⊆ nodes M2"
by auto
ultimately have "finite V"
using det_state_cover_card[of M2 V]
by (metis finite_if_finite_subsets_card_bdd infinite_subset is_det_state_cover.elims(2)
surj_card_le)
obtain ioV where "mcp (map fst io) V ioV"
using mcp_ex[OF ‹[] ∈ V› ‹finite V›] by blast
then have "ioV ∈ V"
by auto
obtain q2 where "d_reaches M2 (initial M2) ioV q2"
using det_state_cover_d_reachable[OF assms(1) ‹ioV ∈ V›] by blast
then obtain ioV' ioP where io_path : "length ioV = length ioV'
∧ length ioV = length ioP
∧ (path M2 ((ioV || ioV') || ioP) (initial M2))
∧ target ((ioV || ioV') || ioP) (initial M2) = q2"
by auto
have "well_formed M2"
using assms by auto
have "map fst (map fst ((ioV || ioV') || ioP)) = ioV"
proof -
have "length (ioV || ioV') = length ioP"
using io_path by simp
then show ?thesis
using io_path by auto
qed
moreover have "set (map fst (map fst ((ioV || ioV') || ioP))) ⊆ inputs M2"
using path_input_containment[OF ‹well_formed M2›, of "(ioV || ioV') || ioP" "initial M2" ]
io_path
by linarith
ultimately have "set ioV ⊆ inputs M2"
by presburger
then have "set ioV ⊆ inputs M1"
using assms by auto
then have "L⇩i⇩n M1 {ioV} ≠ {}"
using assms(2) language_state_for_inputs_nonempty by (metis FSM.nodes.initial)
have "prefix ioV (map fst io)"
using ‹mcp (map fst io) V ioV› mcp.simps by blast
then have "length ioV ≤ length (map fst io)"
using prefix_length_le by blast
then have "length ioV ≤ length io"
by auto
have "(map fst io || map snd io) ∈ L M1"
using assms(5) by auto
moreover have "length (map fst io) = length (map snd io)"
by auto
ultimately have "(map fst io || map snd io)
∈ language_state_for_input M1 (initial M1) (map fst io)"
unfolding language_state_def
by (metis (mono_tags, lifting) ‹map fst io || map snd io ∈ L M1›
language_state_for_input.simps mem_Collect_eq)
have "ioV = take (length ioV) (map fst io)"
by (metis (no_types) ‹prefix ioV (map fst io)› append_eq_conv_conj prefixE)
then have "take (length ioV) io ∈ language_state_for_input M1 (initial M1) ioV"
using language_state_for_input_take
by (metis ‹map fst io || map snd io ∈ language_state_for_input M1 (initial M1) (map fst io)›
zip_map_fst_snd)
then obtain V'' where "V'' ∈ Perm V M1" "take (length ioV) io ∈ V''"
using perm_elem[OF assms(1-3) ‹inputs M1 = inputs M2› ‹ioV ∈ V›] by blast
have "ioV = mcp' (map fst io) V"
using ‹mcp (map fst io) V ioV› mcp'_intro by blast
have "map fst (take (length ioV) io) = ioV"
by (metis ‹ioV = take (length ioV) (map fst io)› take_map)
obtain mcpV'' where "mcp io V'' mcpV''"
by (meson ‹V'' ∈ Perm V M1› ‹well_formed M2› assms(1) mcp_ex perm_elem_finite perm_empty)
have "map fst mcpV'' ∈ V" using perm_inputs
using ‹V'' ∈ Perm V M1› ‹mcp io V'' mcpV''› mcp.simps by blast
have "map fst mcpV'' = ioV"
by (metis (no_types) ‹map fst (take (length ioV) io) = ioV› ‹map fst mcpV'' ∈ V›
‹mcp (map fst io) V ioV› ‹mcp io V'' mcpV''› ‹take (length ioV) io ∈ V''›
map_mono_prefix mcp.elims(2) prefix_length_prefix prefix_order.dual_order.antisym
take_is_prefix)
have "map fst (mcp' io V'') = mcp' (map fst io) V"
using ‹ioV = mcp' (map fst io) V› ‹map fst mcpV'' = ioV› ‹mcp io V'' mcpV''› mcp'_intro
by blast
then show ?thesis
using ‹V'' ∈ Perm V M1› by fastforce
qed
lemma N_mcp_prefix :
assumes "map fst vs = mcp' (map fst (vs@xs)) V"
and "V'' ∈ N (vs@xs) M1 V"
and "is_det_state_cover M2 V"
and "well_formed M2"
and "finite V"
shows "vs ∈ V''" "vs = mcp' (vs@xs) V''"
proof -
have "map fst (mcp' (vs@xs) V'') = mcp' (map fst (vs@xs)) V"
using assms(2) by auto
then have "map fst (mcp' (vs@xs) V'') = map fst vs"
using assms(1) by presburger
then have "length (mcp' (vs@xs) V'') = length vs"
by (metis length_map)
have "[] ∈ V''"
using perm_empty[OF assms(3)] N.simps assms(2) by blast
moreover have "finite V''"
using perm_elem_finite[OF assms(3,4)] N.simps assms(2) by blast
ultimately obtain p where "mcp (vs@xs) V'' p"
using mcp_ex by auto
then have "mcp' (vs@xs) V'' = p"
using mcp'_intro by simp
then have "prefix (mcp' (vs@xs) V'') (vs@xs)"
unfolding mcp'.simps mcp.simps
using ‹mcp (vs @ xs) V'' p› mcp.elims(2) by blast
then show "vs = mcp' (vs@xs) V''"
by (metis ‹length (mcp' (vs @ xs) V'') = length vs› append_eq_append_conv prefix_def)
show "vs ∈ V''"
using ‹mcp (vs @ xs) V'' p› ‹mcp' (vs @ xs) V'' = p› ‹vs = mcp' (vs @ xs) V''›
by auto
qed
subsection ‹ Functions TS, C, RM ›
text ‹
Function T@{verbatim TS} defines the calculation of the test suite used by the adaptive state
counting algorithm in an iterative way.
It is defined using the three functions @{verbatim TS}, @{verbatim C} and @{verbatim RM} where
@{verbatim TS} represents the test suite calculated up to some iteration,
@{verbatim C} contains the sequences considered for extension in some iteration, and
@{verbatim RM} contains the sequences of the corresponding @{verbatim C} result that are not to
be extended, which we also call removed sequences.
›
abbreviation append_set :: "'a list set ⇒ 'a set ⇒ 'a list set" where
"append_set T X ≡ {xs @ [x] | xs x . xs ∈ T ∧ x ∈ X}"
abbreviation append_sets :: "'a list set ⇒ 'a list set ⇒ 'a list set" where
"append_sets T X ≡ {xs @ xs' | xs xs' . xs ∈ T ∧ xs' ∈ X}"
fun TS :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM
⇒ ('in, 'out) ATC set ⇒ 'in list set ⇒ nat ⇒ nat
⇒ 'in list set"
and C :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM
⇒ ('in, 'out) ATC set ⇒ 'in list set ⇒ nat ⇒ nat
⇒ 'in list set"
and RM :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM
⇒ ('in, 'out) ATC set ⇒ 'in list set ⇒ nat ⇒ nat
⇒ 'in list set"
where
"RM M2 M1 Ω V m 0 = {}" |
"TS M2 M1 Ω V m 0 = {}" |
"TS M2 M1 Ω V m (Suc 0) = V" |
"C M2 M1 Ω V m 0 = {}" |
"C M2 M1 Ω V m (Suc 0) = V" |
"RM M2 M1 Ω V m (Suc n) =
{xs' ∈ C M2 M1 Ω V m (Suc n) .
(¬ (L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}))
∨ (∀ io ∈ L⇩i⇩n M1 {xs'} .
∃ V'' ∈ N io M1 V .
∃ S1 .
∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (TS M2 M1 Ω V m n ∪ V) S1 Ω V'')}" |
"C M2 M1 Ω V m (Suc n) =
(append_set ((C M2 M1 Ω V m n) - (RM M2 M1 Ω V m n)) (inputs M2))
- (TS M2 M1 Ω V m n)" |
"TS M2 M1 Ω V m (Suc n) =
(TS M2 M1 Ω V m n) ∪ (C M2 M1 Ω V m (Suc n))"
abbreviation lists_of_length :: "'a set ⇒ nat ⇒ 'a list set" where
"lists_of_length X n ≡ {xs . length xs = n ∧ set xs ⊆ X}"
lemma append_lists_of_length_alt_def :
"append_sets T (lists_of_length X (Suc n)) = append_set (append_sets T (lists_of_length X n)) X"
proof
show "append_sets T (lists_of_length X (Suc n))
⊆ append_set (append_sets T (lists_of_length X n)) X"
proof
fix tx assume "tx ∈ append_sets T (lists_of_length X (Suc n))"
then obtain t x where "t@x = tx" "t ∈ T" "length x = Suc n" "set x ⊆ X"
by blast
then have "x ≠ []" "length (butlast x) = n"
by auto
moreover have "set (butlast x) ⊆ X"
using ‹set x ⊆ X› by (meson dual_order.trans prefixeq_butlast set_mono_prefix)
ultimately have "butlast x ∈ lists_of_length X n"
by auto
then have "t@(butlast x) ∈ append_sets T (lists_of_length X n)"
using ‹t ∈ T› by blast
moreover have "last x ∈ X"
using ‹set x ⊆ X› ‹x ≠ []› by auto
ultimately have "t@(butlast x)@[last x] ∈ append_set (append_sets T (lists_of_length X n)) X"
by auto
then show "tx ∈ append_set (append_sets T (lists_of_length X n)) X"
using ‹t@x = tx› by (simp add: ‹x ≠ []›)
qed
show "append_set (append_sets T (lists_of_length X n)) X
⊆ append_sets T (lists_of_length X (Suc n))"
proof
fix tx assume "tx ∈ append_set (append_sets T (lists_of_length X n)) X"
then obtain tx' x where "tx = tx' @ [x]" "tx' ∈ append_sets T (lists_of_length X n)" "x ∈ X"
by blast
then obtain tx'' x' where "tx''@x' = tx'" "tx'' ∈ T" "length x' = n" "set x' ⊆ X"
by blast
then have "tx''@x'@[x] = tx"
by (simp add: ‹tx = tx' @ [x]›)
moreover have "tx'' ∈ T"
by (meson ‹tx'' ∈ T›)
moreover have "length (x'@[x]) = Suc n"
by (simp add: ‹length x' = n›)
moreover have "set (x'@[x]) ⊆ X"
by (simp add: ‹set x' ⊆ X› ‹x ∈ X›)
ultimately show "tx ∈ append_sets T (lists_of_length X (Suc n))"
by blast
qed
qed
subsection ‹ Basic properties of the test suite calculation functions ›
lemma C_step :
assumes "n > 0"
shows "C M2 M1 Ω V m (Suc n) ⊆ (append_set (C M2 M1 Ω V m n) (inputs M2)) - C M2 M1 Ω V m n"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
obtain k where n_def[simp] : "n = Suc k"
using assms not0_implies_Suc by blast
have "?C (Suc n) = (append_set (?C n - ?RM n) (inputs M2)) - ?TS n"
using n_def C.simps(3) by blast
moreover have "?C n ⊆ ?TS n"
using n_def by (metis C.simps(2) TS.elims UnCI assms neq0_conv subsetI)
ultimately show "?C (Suc n) ⊆ append_set (?C n) (inputs M2) - ?C n"
by blast
qed
lemma C_extension :
"C M2 M1 Ω V m (Suc n) ⊆ append_sets V (lists_of_length (inputs M2) n)"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc k)
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "0 < Suc k" by simp
have "?C (Suc (Suc k)) ⊆ (append_set (?C (Suc k)) (inputs M2)) - ?C (Suc k)"
using C_step[OF ‹0 < Suc k›] by blast
then have "?C (Suc (Suc k)) ⊆ append_set (?C (Suc k)) (inputs M2)"
by blast
moreover have "append_set (?C (Suc k)) (inputs M2)
⊆ append_set (append_sets V (lists_of_length (inputs M2) k)) (inputs M2)"
using Suc.IH by auto
ultimately have I_Step :
"?C (Suc (Suc k)) ⊆ append_set (append_sets V (lists_of_length (inputs M2) k)) (inputs M2)"
by (meson order_trans)
show ?case
using append_lists_of_length_alt_def[symmetric, of V k "inputs M2"] I_Step
by presburger
qed
lemma TS_union :
shows "TS M2 M1 Ω V m i = (⋃ j ∈ (set [0..<Suc i]) . C M2 M1 Ω V m j)"
proof (induction i)
case 0
then show ?case by auto
next
case (Suc i)
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "?TS (Suc i) = ?TS i ∪ ?C (Suc i)"
by (metis (no_types) C.simps(2) TS.simps(1) TS.simps(2) TS.simps(3) not0_implies_Suc
sup_bot.right_neutral sup_commute)
then have "?TS (Suc i) = (⋃ j ∈ (set [0..<Suc i]) . ?C j) ∪ ?C (Suc i)"
using Suc.IH by simp
then show ?case
by auto
qed
lemma C_disj_le_gz :
assumes "i ≤ j"
and "0 < i"
shows "C M2 M1 Ω V m i ∩ C M2 M1 Ω V m (Suc j) = {}"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "Suc 0 < Suc j"
using assms(1-2) by auto
then obtain k where "Suc j = Suc (Suc k)"
using not0_implies_Suc by blast
then have "?C (Suc j) = (append_set (?C j - ?RM j) (inputs M2)) - ?TS j"
using C.simps(3) by blast
then have "?C (Suc j) ∩ ?TS j = {}"
by blast
moreover have "?C i ⊆ ?TS j"
using assms(1) TS_union[of M2 M1 Ω V m j] by fastforce
ultimately show ?thesis
by blast
qed
lemma C_disj_lt :
assumes "i < j"
shows "C M2 M1 Ω V m i ∩ C M2 M1 Ω V m j = {}"
proof (cases i)
case 0
then show ?thesis by auto
next
case (Suc k)
then show ?thesis
using C_disj_le_gz
by (metis assms gr_implies_not0 less_Suc_eq_le old.nat.exhaust zero_less_Suc)
qed
lemma C_disj :
assumes "i ≠ j"
shows "C M2 M1 Ω V m i ∩ C M2 M1 Ω V m j = {}"
by (metis C_disj_lt Int_commute antisym_conv3 assms)
lemma RM_subset : "RM M2 M1 Ω V m i ⊆ C M2 M1 Ω V m i"
proof (cases i)
case 0
then show ?thesis by auto
next
case (Suc n)
then show ?thesis
using RM.simps(2) by blast
qed
lemma RM_disj :
assumes "i ≤ j"
and "0 < i"
shows "RM M2 M1 Ω V m i ∩ RM M2 M1 Ω V m (Suc j) = {}"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "?RM i ⊆ ?C i" "?RM (Suc j) ⊆ ?C (Suc j)"
using RM_subset by blast+
moreover have "?C i ∩ ?C (Suc j) = {}"
using C_disj_le_gz[OF assms] by assumption
ultimately show ?thesis
by blast
qed
lemma T_extension :
assumes "n > 0"
shows "TS M2 M1 Ω V m (Suc n) - TS M2 M1 Ω V m n
⊆ (append_set (TS M2 M1 Ω V m n) (inputs M2)) - TS M2 M1 Ω V m n"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
obtain k where n_def[simp] : "n = Suc k"
using assms not0_implies_Suc
by blast
have "?C (Suc n) = (append_set (?C n - ?RM n) (inputs M2)) - ?TS n"
using n_def using C.simps(3) by blast
then have "?C (Suc n) ⊆ append_set (?C n) (inputs M2) - ?TS n"
by blast
moreover have "?C n ⊆ ?TS n" using TS_union[of M2 M1 Ω V m n]
by fastforce
ultimately have "?C (Suc n) ⊆ append_set (?TS n) (inputs M2) - ?TS n"
by blast
moreover have "?TS (Suc n) - ?TS n ⊆ ?C (Suc n) "
using TS.simps(3)[of M2 M1 Ω V m k] using n_def by blast
ultimately show ?thesis
by blast
qed
lemma append_set_prefix :
assumes "xs ∈ append_set T X"
shows "butlast xs ∈ T"
using assms by auto
lemma C_subset : "C M2 M1 Ω V m i ⊆ TS M2 M1 Ω V m i"
by (simp add: TS_union)
lemma TS_subset :
assumes "i ≤ j"
shows "TS M2 M1 Ω V m i ⊆ TS M2 M1 Ω V m j"
proof -
have "TS M2 M1 Ω V m i = (⋃ k ∈ (set [0..<Suc i]) . C M2 M1 Ω V m k)"
"TS M2 M1 Ω V m j = (⋃ k ∈ (set [0..<Suc j]) . C M2 M1 Ω V m k)"
using TS_union by assumption+
moreover have "set [0..<Suc i] ⊆ set [0..<Suc j]"
using assms by auto
ultimately show ?thesis
by blast
qed
lemma C_immediate_prefix_containment :
assumes "vs@xs ∈ C M2 M1 Ω V m (Suc (Suc i))"
and "xs ≠ []"
shows "vs@(butlast xs) ∈ C M2 M1 Ω V m (Suc i) - RM M2 M1 Ω V m (Suc i)"
proof (rule ccontr)
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
assume "vs @ butlast xs ∉ C M2 M1 Ω V m (Suc i) - RM M2 M1 Ω V m (Suc i)"
have "?C (Suc (Suc i)) ⊆ append_set (?C (Suc i) - ?RM (Suc i)) (inputs M2)"
using C.simps(3) by blast
then have "?C (Suc (Suc i)) ⊆ append_set (?C (Suc i) - ?RM (Suc i)) UNIV"
by blast
moreover have "vs @ xs ∉ append_set (?C (Suc i) - ?RM (Suc i)) UNIV"
proof -
have "∀as a. vs @ xs ≠ as @ [a]
∨ as ∉ C M2 M1 Ω V m (Suc i) - RM M2 M1 Ω V m (Suc i)
∨ a ∉ UNIV"
by (metis ‹vs @ butlast xs ∉ C M2 M1 Ω V m (Suc i) - RM M2 M1 Ω V m (Suc i)›
assms(2) butlast_append butlast_snoc)
then show ?thesis
by blast
qed
ultimately have "vs @ xs ∉ ?C (Suc (Suc i))"
by blast
then show "False"
using assms(1) by blast
qed
lemma TS_immediate_prefix_containment :
assumes "vs@xs ∈ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
and "0 < i"
shows "vs@(butlast xs) ∈ TS M2 M1 Ω V m i"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
obtain j where j_def : "j ≤ i ∧ vs@xs ∈ ?C j"
using assms(1) TS_union[where i=i]
proof -
assume a1: "⋀j. j ≤ i ∧ vs @ xs ∈ C M2 M1 Ω V m j ⟹ thesis"
obtain nn :: "nat set ⇒ (nat ⇒ 'a list set) ⇒ 'a list ⇒ nat" where
f2: "∀x0 x1 x2. (∃v3. v3 ∈ x0 ∧ x2 ∈ x1 v3) = (nn x0 x1 x2 ∈ x0 ∧ x2 ∈ x1 (nn x0 x1 x2))"
by moura
have "vs @ xs ∈ UNION (set [0..<Suc i]) (C M2 M1 Ω V m)"
by (metis ‹⋀Ω V T S M2 M1. TS M2 M1 Ω V m i = (⋃j∈set [0..<Suc i]. C M2 M1 Ω V m j)›
‹vs @ xs ∈ TS M2 M1 Ω V m i›)
then have "nn (set [0..<Suc i]) (C M2 M1 Ω V m) (vs @ xs) ∈ set [0..<Suc i]
∧ vs @ xs ∈ C M2 M1 Ω V m (nn (set [0..<Suc i]) (C M2 M1 Ω V m) (vs @ xs))"
using f2 by blast
then show ?thesis
using a1 by (metis (no_types) atLeastLessThan_iff leD not_less_eq_eq set_upt)
qed
show ?thesis
proof (cases j)
case 0
then have "?C j = {}"
by auto
moreover have "vs@xs ∈ {}"
using j_def 0 by auto
ultimately show ?thesis
by auto
next
case (Suc k)
then show ?thesis
proof (cases k)
case 0
then have "?C j = V"
using Suc by auto
then have "vs@xs ∈ V"
using j_def by auto
then have "mcp (vs@xs) V (vs@xs)"
using assms(2) by auto
then have "vs@xs = vs"
using assms(2) mcp_unique by auto
then have "butlast xs = []"
by auto
then show ?thesis
using ‹vs @ xs = vs› assms(1) by auto
next
case (Suc n)
assume j_assms : "j = Suc k"
"k = Suc n"
then have "?C (Suc (Suc n)) = append_set (?C (Suc n) - ?RM (Suc n)) (inputs M2) - ?TS (Suc n)"
using C.simps(3) by blast
then have "?C (Suc (Suc n)) ⊆ append_set (?C (Suc n)) (inputs M2)"
by blast
have "vs@xs ∈ ?C (Suc (Suc n))"
using j_assms j_def by blast
have "butlast (vs@xs) ∈ ?C (Suc n)"
proof -
show ?thesis
by (meson ‹?C (Suc (Suc n)) ⊆ append_set (?C (Suc n)) (inputs M2)›
‹vs @ xs ∈ ?C (Suc (Suc n))› append_set_prefix subsetCE)
qed
moreover have "xs ≠ []"
proof -
have "1 ≤ k"
using j_assms by auto
then have "?C j ∩ ?C 1 = {}"
using C_disj_le_gz[of 1 k] j_assms(1) less_numeral_extra(1) by blast
then have "?C j ∩ V = {}"
by auto
then have "vs@xs ∉ V"
using j_def by auto
then show ?thesis
using assms(2) by auto
qed
ultimately have "vs@(butlast xs) ∈ ?C (Suc n)"
by (simp add: butlast_append)
have "Suc n < Suc j"
using j_assms by auto
have "?C (Suc n) ⊆ ?TS j"
using TS_union[of M2 M1 Ω V m j] ‹Suc n < Suc j›
by (metis UN_upper atLeast_upt lessThan_iff)
have "vs @ butlast xs ∈ TS M2 M1 Ω V m j"
using ‹vs@(butlast xs) ∈ ?C (Suc n)› ‹?C (Suc n) ⊆ ?TS j› j_def
by auto
then show ?thesis
using j_def TS_subset[of j i]
by blast
qed
qed
qed
lemma TS_prefix_containment :
assumes "vs@xs ∈ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
and "prefix xs' xs"
shows "vs@xs' ∈ TS M2 M1 Ω V m i"
using assms proof (induction "length xs - length xs'" arbitrary: xs')
case 0
then have "xs = xs'"
by (metis append_Nil2 append_eq_conv_conj gr_implies_not0 length_drop length_greater_0_conv prefixE)
then show ?case
using 0 by auto
next
case (Suc k)
have "0 < i"
using assms(1) using Suc.hyps(2) append_eq_append_conv assms(2) by auto
show ?case
proof (cases xs')
case Nil
then show ?thesis
by (metis (no_types, opaque_lifting) ‹0 < i› TS.simps(2) TS_subset append_Nil2 assms(2)
contra_subsetD leD mcp.elims(2) not_less_eq_eq)
next
case (Cons a list)
then show ?thesis
proof (cases "xs = xs'")
case True
then show ?thesis
using assms(1) by simp
next
case False
then obtain xs'' where "xs = xs'@xs''"
using Suc.prems(3) prefixE by blast
then have "xs'' ≠ []"
using False by auto
then have "k = length xs - length (xs' @ [hd xs''])"
using ‹xs = xs'@xs''› Suc.hyps(2) by auto
moreover have "prefix (xs' @ [hd xs'']) xs"
using ‹xs = xs'@xs''› ‹xs'' ≠ []›
by (metis Cons_prefix_Cons list.exhaust_sel prefix_code(1) same_prefix_prefix)
ultimately have "vs @ (xs' @ [hd xs'']) ∈ TS M2 M1 Ω V m i"
using Suc.hyps(1)[OF _ Suc.prems(1,2)] by simp
have "mcp (vs @ xs' @ [hd xs'']) V vs"
using ‹xs = xs'@xs''› ‹xs'' ≠ []› assms(2)
proof -
obtain aas :: "'a list ⇒ 'a list set ⇒ 'a list ⇒ 'a list" where
"∀x0 x1 x2. (∃v3. (prefix v3 x2 ∧ v3 ∈ x1) ∧ ¬ length v3 ≤ length x0)
= ((prefix (aas x0 x1 x2) x2 ∧ aas x0 x1 x2 ∈ x1)
∧ ¬ length (aas x0 x1 x2) ≤ length x0)"
by moura
then have f1: "∀as A asa. (¬ mcp as A asa
∨ prefix asa as ∧ asa ∈ A ∧ (∀asb. (¬ prefix asb as ∨ asb ∉ A)
∨ length asb ≤ length asa))
∧ (mcp as A asa
∨ ¬ prefix asa as
∨ asa ∉ A
∨ (prefix (aas asa A as) as ∧ aas asa A as ∈ A)
∧ ¬ length (aas asa A as) ≤ length asa)"
by auto
obtain aasa :: "'a list ⇒ 'a list ⇒ 'a list" where
f2: "∀x0 x1. (∃v2. x0 = x1 @ v2) = (x0 = x1 @ aasa x0 x1)"
by moura
then have f3: "([] @ [hd xs'']) @ aasa (xs' @ xs'') (xs' @ [hd xs''])
= ([] @ [hd xs'']) @ aasa (([] @ [hd xs''])
@ aasa (xs' @ xs'') (xs' @ [hd xs''])) ([] @ [hd xs''])"
by (meson prefixE prefixI)
have "xs' @ xs'' = (xs' @ [hd xs'']) @ aasa (xs' @ xs'') (xs' @ [hd xs''])"
using f2 by (metis (no_types) ‹prefix (xs' @ [hd xs'']) xs› ‹xs = xs' @ xs''› prefixE)
then have "(vs @ (a # list) @ [hd xs'']) @ aasa (([] @ [hd xs''])
@ aasa (xs' @ xs'') (xs' @ [hd xs''])) ([] @ [hd xs''])
= vs @ xs"
using f3 by (simp add: ‹xs = xs' @ xs''› local.Cons)
then have "¬ prefix (aas vs V (vs @ xs' @ [hd xs''])) (vs @ xs' @ [hd xs''])
∨ aas vs V (vs @ xs' @ [hd xs'']) ∉ V
∨ length (aas vs V (vs @ xs' @ [hd xs''])) ≤ length vs"
using f1 by (metis (no_types) ‹mcp (vs @ xs) V vs› local.Cons prefix_append)
then show ?thesis
using f1 by (meson ‹mcp (vs @ xs) V vs› prefixI)
qed
then have "vs @ butlast (xs' @ [hd xs'']) ∈ TS M2 M1 Ω V m i"
using TS_immediate_prefix_containment
[OF ‹vs @ (xs' @ [hd xs'']) ∈ TS M2 M1 Ω V m i› _ ‹0 < i›]
by simp
moreover have "xs' = butlast (xs' @ [hd xs''])"
using ‹xs'' ≠ []› by simp
ultimately show ?thesis
by simp
qed
qed
qed
lemma C_index :
assumes "vs @ xs ∈ C M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
shows "Suc (length xs) = i"
using assms proof (induction xs arbitrary: i rule: rev_induct)
case Nil
then have "vs @ [] ∈ C M2 M1 Ω V m 1"
by auto
then have "vs @ [] ∈ C M2 M1 Ω V m (Suc (length []))"
by simp
show ?case
proof (rule ccontr)
assume "Suc (length []) ≠ i"
moreover have "vs @ [] ∈ C M2 M1 Ω V m i ∩ C M2 M1 Ω V m (Suc (length []))"
using Nil.prems(1) ‹vs @ [] ∈ C M2 M1 Ω V m (Suc (length []))› by auto
ultimately show "False"
using C_disj by blast
qed
next
case (snoc x xs')
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "vs @ xs' @ [x] ∉ V"
using snoc.prems(2) by auto
then have "vs @ xs' @ [x] ∉ ?C 1"
by auto
moreover have "vs @ xs' @ [x] ∉ ?C 0"
by auto
ultimately have "1 < i"
using snoc.prems(1) by (metis less_one linorder_neqE_nat)
then have "vs @ butlast (xs' @ [x]) ∈ C M2 M1 Ω V m (i-1)"
proof -
have "Suc 0 < i"
using ‹1 < i› by auto
then have f1: "Suc (i - Suc (Suc 0)) = i - Suc 0"
using Suc_diff_Suc by presburger
have "0 < i"
by (metis (no_types) One_nat_def Suc_lessD ‹1 < i›)
then show ?thesis
using f1 by (metis C_immediate_prefix_containment DiffD1 One_nat_def Suc_pred' snoc.prems(1)
snoc_eq_iff_butlast)
qed
moreover have "mcp (vs @ butlast (xs' @ [x])) V vs"
by (meson mcp_prefix_of_suffix prefixeq_butlast snoc.prems(2))
ultimately have "Suc (length xs') = i-1"
using snoc.IH by simp
then show ?case
by auto
qed
lemma TS_index :
assumes "vs @ xs ∈ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
shows "Suc (length xs) ≤ i" "vs@xs ∈ C M2 M1 Ω V m (Suc (length xs))"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
obtain j where "j < Suc i" "vs@xs ∈ ?C j"
using TS_union[of M2 M1 Ω V m i]
by (metis (full_types) UN_iff assms(1) atLeastLessThan_iff set_upt)
then have "Suc (length xs) = j"
using C_index assms(2) by blast
then show "Suc (length xs) ≤ i"
using ‹j < Suc i› by auto
show "vs@xs ∈ C M2 M1 Ω V m (Suc (length xs))"
using ‹vs@xs ∈ ?C j› ‹Suc (length xs) = j› by auto
qed
lemma C_extension_options :
assumes "vs @ xs ∈ C M2 M1 Ω V m i"
and "mcp (vs @ xs @ [x]) V vs"
and "x ∈ inputs M2"
and "0 < i"
shows "vs@xs@[x] ∈ C M2 M1 Ω V m (Suc i) ∨ vs@xs ∈ RM M2 M1 Ω V m i"
proof (cases "vs@xs ∈ RM M2 M1 Ω V m i")
case True
then show ?thesis by auto
next
case False
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
obtain k where "i = Suc k"
using assms(4) gr0_implies_Suc by blast
then have "?C (Suc i) = append_set (?C i - ?RM i) (inputs M2) - ?TS i"
using C.simps(3) by blast
moreover have "vs@xs ∈ ?C i - ?RM i"
using assms(1) False by blast
ultimately have "vs@xs@[x] ∈ append_set (?C i - ?RM i) (inputs M2)"
by (simp add: assms(3))
moreover have "vs@xs@[x] ∉ ?TS i"
proof (rule ccontr)
assume "¬ vs @ xs @ [x] ∉ ?TS i"
then obtain j where "j < Suc i" "vs@xs@[x] ∈ ?C j"
using TS_union[of M2 M1 Ω V m i] by fastforce
then have "Suc (length (xs@[x])) = j"
using C_index assms(2) by blast
then have "Suc (length (xs@[x])) < Suc i"
using ‹j < Suc i› by auto
moreover have "Suc (length xs) = i"
using C_index
by (metis assms(1) assms(2) mcp_prefix_of_suffix prefixI)
ultimately have "Suc (length (xs@[x])) < Suc (Suc (length xs))"
by auto
then show "False"
by auto
qed
ultimately show ?thesis
by (simp add: ‹?C (Suc i) = append_set (?C i - ?RM i) (inputs M2) - ?TS i›)
qed
lemma TS_non_containment_causes :
assumes "vs@xs ∉ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
and "set xs ⊆ inputs M2"
and "0 < i"
shows "(∃ xr j . xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m j)
∨ (∃ xc . xc ≠ xs ∧ prefix xc xs ∧ vs@xc ∈ (C M2 M1 Ω V m i) - (RM M2 M1 Ω V m i))"
(is "?PrefPreviouslyRemoved ∨ ?PrefJustContained")
"¬ ((∃ xr j . xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m j)
∧ (∃ xc . xc ≠ xs ∧ prefix xc xs ∧ vs@xc ∈ (C M2 M1 Ω V m i) - (RM M2 M1 Ω V m i)))"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
show "?PrefPreviouslyRemoved ∨ ?PrefJustContained"
proof (rule ccontr)
assume "¬ (?PrefPreviouslyRemoved ∨ ?PrefJustContained)"
then have "¬ ?PrefPreviouslyRemoved" "¬ ?PrefJustContained" by auto
have "¬ (∃ xr j. prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ ?RM j)"
proof
assume "∃xr j. prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j"
then obtain xr j where "prefix xr xs" "j ≤ i" "vs @ xr ∈ ?RM j"
by blast
then show "False"
proof (cases "xr = xs")
case True
then have "vs @ xs ∈ ?RM j" using ‹vs @ xr ∈ ?RM j› by auto
then have "vs @ xs ∈ ?TS j"
using C_subset RM_subset ‹vs @ xr ∈ ?RM j› by blast
then have "vs @ xs ∈ ?TS i"
using TS_subset ‹j ≤ i› by blast
then show ?thesis using assms(1) by blast
next
case False
then show ?thesis
using ‹¬ ?PrefPreviouslyRemoved› ‹prefix xr xs› ‹j ≤ i› ‹vs @ xr ∈ ?RM j›
by blast
qed
qed
have "vs ∈ V" using assms(2) by auto
then have "vs ∈ ?C 1" by auto
have "⋀ k . (1 ≤ Suc k ∧ Suc k ≤ i) ⟶ vs @ (take k xs) ∈ ?C (Suc k) - ?RM (Suc k)"
proof
fix k assume "1 ≤ Suc k ∧ Suc k ≤ i"
then show "vs @ (take k xs) ∈ ?C (Suc k) - ?RM (Suc k)"
proof (induction k)
case 0
show ?case using ‹vs ∈ ?C 1›
by (metis "0.prems" DiffI One_nat_def
‹¬ (∃ xr j. prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j)›
append_Nil2 take_0 take_is_prefix)
next
case (Suc k)
have "1 ≤ Suc k ∧ Suc k ≤ i"
using Suc.prems by auto
then have "vs @ take k xs ∈ ?C (Suc k)"
using Suc.IH by simp
moreover have "vs @ take k xs ∉ ?RM (Suc k)"
using ‹1 ≤ Suc k ∧ Suc k ≤ i› ‹¬ ?PrefPreviouslyRemoved› take_is_prefix Suc.IH
by blast
ultimately have "vs @ take k xs ∈ (?C (Suc k)) - (?RM (Suc k))"
by blast
have "k < length xs"
proof (rule ccontr)
assume "¬ k < length xs"
then have "vs @ xs ∈ ?C (Suc k)" using ‹vs @ take k xs ∈ ?C (Suc k)›
by simp
have "vs @ xs ∈ ?TS i"
by (metis C_subset TS_subset ‹1 ≤ Suc k ∧ Suc k ≤ i› ‹vs @ xs ∈ ?C (Suc k)›
contra_subsetD)
then show "False"
using assms(1) by simp
qed
moreover have "set xs ⊆ inputs M2"
using assms(3) by auto
ultimately have "last (take (Suc k) xs) ∈ inputs M2"
by (simp add: subset_eq take_Suc_conv_app_nth)
have "vs @ take (Suc k) xs ∈ append_set ((?C (Suc k)) - (?RM (Suc k))) (inputs M2)"
proof -
have f1: "xs ! k ∈ inputs M2"
by (meson ‹k < length xs› ‹set xs ⊆ inputs M2› nth_mem subset_iff)
have "vs @ take (Suc k) xs = (vs @ take k xs) @ [xs ! k]"
by (simp add: ‹k < length xs› take_Suc_conv_app_nth)
then show ?thesis
using f1 ‹vs @ take k xs ∈ C M2 M1 Ω V m (Suc k) - RM M2 M1 Ω V m (Suc k)› by blast
qed
moreover have "vs @ take (Suc k) xs ∉ ?TS (Suc k)"
proof
assume "vs @ take (Suc k) xs ∈ ?TS (Suc k)"
then have "Suc (length (take (Suc k) xs)) ≤ Suc k"
using TS_index(1) assms(2) mcp_prefix_of_suffix take_is_prefix by blast
moreover have "Suc (length (take k xs)) = Suc k" using C_index ‹vs @ take k xs ∈ ?C (Suc k)›
by (metis assms(2) mcp_prefix_of_suffix take_is_prefix)
ultimately show "False" using ‹k < length xs›
by simp
qed
show "vs @ take (Suc k) xs ∈ ?C (Suc (Suc k)) - ?RM (Suc (Suc k))"
using C.simps(3)[of M2 M1 Ω V m k]
by (metis (no_types, lifting) DiffI Suc.prems
‹¬ (∃ xr j. prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j)›
‹vs @ take (Suc k) xs ∉ TS M2 M1 Ω V m (Suc k)› calculation take_is_prefix)
qed
qed
then have "vs @ take (i-1) xs ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i"
using assms(4)
by (metis One_nat_def Suc_diff_1 Suc_leI le_less)
then have "?PrefJustContained"
by (metis C_subset DiffD1 assms(1) subsetCE take_is_prefix)
then show "False"
using ‹¬ ?PrefJustContained› by simp
qed
show "¬ (?PrefPreviouslyRemoved ∧ ?PrefJustContained)"
proof
assume "?PrefPreviouslyRemoved ∧ ?PrefJustContained"
then have "?PrefPreviouslyRemoved"
"?PrefJustContained"
by auto
obtain xr j where "prefix xr xs" "j ≤ i" "vs@xr ∈ ?RM j"
using ‹?PrefPreviouslyRemoved› by blast
obtain xc where "prefix xc xs" "vs@xc ∈ ?C i - ?RM i"
using ‹?PrefJustContained› by blast
then have "Suc (length xc) = i"
using C_index
by (metis Diff_iff assms(2) mcp_prefix_of_suffix)
moreover have "length xc ≤ length xs"
using ‹prefix xc xs› by (simp add: prefix_length_le)
moreover have "xc ≠ xs"
proof
assume "xc = xs"
then have "vs@xs ∈ ?C i"
using ‹vs@xc ∈ ?C i - ?RM i› by auto
then have "vs@xs ∈ ?TS i"
using C_subset by blast
then show "False"
using assms(1) by blast
qed
ultimately have "i ≤ length xs"
using ‹prefix xc xs› not_less_eq_eq prefix_length_prefix prefix_order.antisym
by blast
have "⋀ n . (n < i) ⟹ vs@(take n xs) ∈ ?C (Suc n)"
proof -
fix n assume "n < i"
show "vs @ take n xs ∈ C M2 M1 Ω V m (Suc n)"
proof -
have "n ≤ length xc"
using ‹n < i› ‹Suc (length xc) = i› less_Suc_eq_le
by blast
then have "prefix (vs @ (take n xs)) (vs @ xc)"
proof -
have "n ≤ length xs"
using ‹length xc ≤ length xs› ‹n ≤ length xc› order_trans
by blast
then have "prefix (take n xs) xc"
by (metis (no_types) ‹n ≤ length xc› ‹prefix xc xs› length_take min.absorb2
prefix_length_prefix take_is_prefix)
then show ?thesis
by simp
qed
then have "vs @ take n xs ∈ ?TS i"
by (meson C_subset DiffD1 TS_prefix_containment ‹prefix xc xs›
‹vs @ xc ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i› assms(2) contra_subsetD
mcp_prefix_of_suffix same_prefix_prefix)
then obtain jn where "jn < Suc i" "vs@(take n xs) ∈ ?C jn"
using TS_union[of M2 M1 Ω V m i]
by (metis UN_iff atLeast_upt lessThan_iff)
moreover have "mcp (vs @ take n xs) V vs"
by (meson assms(2) mcp_prefix_of_suffix take_is_prefix)
ultimately have "jn = Suc (length (take n xs))"
using C_index[of vs "take n xs" M2 M1 Ω V m jn] by auto
then have "jn = Suc n"
using ‹length xc ≤ length xs› ‹n ≤ length xc› by auto
then show "vs@(take n xs) ∈ ?C (Suc n)"
using ‹vs@(take n xs) ∈ ?C jn› by auto
qed
qed
have "⋀ n . (n < i) ⟹ vs@(take n xs) ∉ ?RM (Suc n)"
proof -
fix n assume "n < i"
show "vs @ take n xs ∉ RM M2 M1 Ω V m (Suc n)"
proof (cases "n = length xc")
case True
then show ?thesis
using ‹vs@xc ∈ ?C i - ?RM i›
by (metis DiffD2 ‹Suc (length xc) = i› ‹prefix xc xs› append_eq_conv_conj prefixE)
next
case False
then have "n < length xc"
using ‹n < i› ‹Suc (length xc) = i› by linarith
show ?thesis
proof (cases "Suc n < length xc")
case True
then have "Suc n < i"
using ‹Suc (length xc) = i› ‹n < length xc› by blast
then have "vs @ (take (Suc n) xs) ∈ ?C (Suc (Suc n))"
using ‹⋀ n . (n < i) ⟹ vs@(take n xs) ∈ ?C (Suc n)› by blast
then have "vs @ butlast (take (Suc n) xs) ∈ ?C (Suc n) - ?RM (Suc n)"
using True C_immediate_prefix_containment[of vs "take (Suc n) xs" M2 M1 Ω V m n]
by (metis Suc_neq_Zero ‹prefix xc xs› ‹xc ≠ xs› prefix_Nil take_eq_Nil)
then show ?thesis
by (metis DiffD2 Suc_lessD True ‹length xc ≤ length xs› butlast_snoc less_le_trans
take_Suc_conv_app_nth)
next
case False
then have "Suc n = length xc"
using Suc_lessI ‹n < length xc› by blast
then have "vs @ (take (Suc n) xs) ∈ ?C (Suc (Suc n))"
using ‹Suc (length xc) = i› ‹⋀n. n < i ⟹ vs @ take n xs ∈ C M2 M1 Ω V m (Suc n)›
by auto
then have "vs @ butlast (take (Suc n) xs) ∈ ?C (Suc n) - ?RM (Suc n)"
using False C_immediate_prefix_containment[of vs "take (Suc n) xs" M2 M1 Ω V m n]
by (metis Suc_neq_Zero ‹prefix xc xs› ‹xc ≠ xs› prefix_Nil take_eq_Nil)
then show ?thesis
by (metis Diff_iff ‹Suc n = length xc› ‹length xc ≤ length xs› butlast_take diff_Suc_1)
qed
qed
qed
have "xr = take j xs"
proof -
have "vs@xr ∈ ?C j"
using ‹vs@xr ∈ ?RM j› RM_subset by blast
then show ?thesis
using C_index
by (metis Suc_le_lessD ‹⋀n. n < i ⟹ vs @ take n xs ∉ RM M2 M1 Ω V m (Suc n)› ‹j ≤ i›
‹prefix xr xs› ‹vs @ xr ∈ RM M2 M1 Ω V m j› append_eq_conv_conj assms(2)
mcp_prefix_of_suffix prefix_def)
qed
have "vs@xr ∉ ?RM j"
by (metis (no_types) C_index RM_subset ‹i ≤ length xs› ‹j ≤ i› ‹prefix xr xs›
‹xr = take j xs› assms(2) contra_subsetD dual_order.trans length_take lessI less_irrefl
mcp_prefix_of_suffix min.absorb2)
then show "False"
using ‹vs@xr ∈ ?RM j› by simp
qed
qed
lemma TS_non_containment_causes_rev :
assumes "mcp (vs@xs) V vs"
and "(∃ xr j . xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m j)
∨ (∃ xc . xc ≠ xs ∧ prefix xc xs ∧ vs@xc ∈ (C M2 M1 Ω V m i) - (RM M2 M1 Ω V m i))"
(is "?PrefPreviouslyRemoved ∨ ?PrefJustContained")
shows "vs@xs ∉ TS M2 M1 Ω V m i"
proof
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
assume "vs @ xs ∈ TS M2 M1 Ω V m i"
have "?PrefPreviouslyRemoved ⟹ False"
proof -
assume ?PrefPreviouslyRemoved
then obtain xr j where "xr ≠ xs" "prefix xr xs" "j ≤ i" "vs@xr ∈ ?RM j"
by blast
then have "vs@xr ∉ ?C j - ?RM j"
by blast
have "vs@(take (Suc (length xr)) xs) ∉ ?C (Suc j)"
proof -
have "vs@(take (length xr) xs) ∉ ?C j - ?RM j"
by (metis ‹prefix xr xs› ‹vs @ xr ∉ C M2 M1 Ω V m j - RM M2 M1 Ω V m j›
append_eq_conv_conj prefix_def)
show ?thesis
proof (cases j)
case 0
then show ?thesis
using RM.simps(1) ‹vs @ xr ∈ RM M2 M1 Ω V m j› by blast
next
case (Suc j')
then have "?C (Suc j) ⊆ append_set (?C j - ?RM j) (inputs M2)"
using C.simps(3) Suc by blast
obtain x where "vs@(take (Suc (length xr)) xs) = vs@(take (length xr) xs) @ [x]"
by (metis ‹prefix xr xs› ‹xr ≠ xs› append_eq_conv_conj not_le prefix_def
take_Suc_conv_app_nth take_all)
have "vs@(take (length xr) xs) @ [x] ∉ append_set (?C j - ?RM j) (inputs M2)"
using ‹vs@(take (length xr) xs) ∉ ?C j - ?RM j› by simp
then have "vs@(take (length xr) xs) @ [x] ∉ ?C (Suc j)"
using ‹?C (Suc j) ⊆ append_set (?C j - ?RM j) (inputs M2)› by blast
then show ?thesis
using ‹vs@(take (Suc (length xr)) xs) = vs@(take (length xr) xs) @ [x]› by auto
qed
qed
have "prefix (take (Suc (length xr)) xs) xs"
by (simp add: take_is_prefix)
then have "vs@(take (Suc (length xr)) xs) ∈ ?TS i"
using TS_prefix_containment[OF ‹vs @ xs ∈ TS M2 M1 Ω V m i› assms(1)] by simp
then obtain j' where "j' < Suc i ∧ vs@(take (Suc (length xr)) xs) ∈ ?C j'"
using TS_union[of M2 M1 Ω V m i] by fastforce
then have "Suc (Suc (length xr)) = j'"
using C_index[of vs "take (Suc (length xr)) xs"]
proof -
have "¬ length xs ≤ length xr"
by (metis (no_types) ‹prefix xr xs› ‹xr ≠ xs› append_Nil2 append_eq_conv_conj leD
nat_less_le prefix_def prefix_length_le)
then show ?thesis
by (metis (no_types) ‹⋀i Ω V T S M2 M1. ⟦vs @ take (Suc (length xr)) xs ∈ C M2 M1 Ω V m i;
mcp (vs @ take (Suc (length xr)) xs) V vs⟧
⟹ Suc (length (take (Suc (length xr)) xs)) = i›
‹j' < Suc i ∧ vs @ take (Suc (length xr)) xs ∈ C M2 M1 Ω V m j'›
append_eq_conv_conj assms(1) length_take mcp_prefix_of_suffix min.absorb2
not_less_eq_eq prefix_def)
qed
moreover have "Suc (length xr) = j"
using ‹vs@xr ∈ ?RM j› RM_subset C_index
by (metis ‹prefix xr xs› assms(1) mcp_prefix_of_suffix subsetCE)
ultimately have "j' = Suc j"
by auto
then have "vs@(take (Suc (length xr)) xs) ∈ ?C (Suc j)"
using ‹j' < Suc i ∧ vs@(take (Suc (length xr)) xs) ∈ ?C j'› by auto
then show "False"
using ‹vs@(take (Suc (length xr)) xs) ∉ ?C (Suc j)› by blast
qed
moreover have "?PrefJustContained ⟹ False"
proof -
assume ?PrefJustContained
then obtain xc where "xc ≠ xs"
"prefix xc xs"
"vs @ xc ∈ ?C i - ?RM i"
by blast
then show "False"
by (metis C_index DiffD1 Suc_less_eq TS_index(1) ‹vs @ xs ∈ ?TS i› assms(1) leD le_neq_trans
mcp_prefix_of_suffix prefix_length_le prefix_length_prefix
prefix_order.dual_order.antisym prefix_order.order_refl)
qed
ultimately show "False"
using assms(2) by auto
qed
lemma TS_finite :
assumes "finite V"
and "finite (inputs M2)"
shows "finite (TS M2 M1 Ω V m n)"
using assms proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
show ?case
proof (cases "n=0")
case True
then have "?TS (Suc n) = V"
by auto
then show ?thesis
using ‹finite V› by auto
next
case False
then have "?TS (Suc n) = ?TS n ∪ ?C (Suc n)"
by (metis TS.simps(3) gr0_implies_Suc neq0_conv)
moreover have "finite (?TS n)"
using Suc.IH[OF Suc.prems] by assumption
moreover have "finite (?C (Suc n))"
proof -
have "?C (Suc n) ⊆ append_set (?C n) (inputs M2)"
using C_step False by blast
moreover have "?C n ⊆ ?TS n"
by (simp add: C_subset)
ultimately have "?C (Suc n) ⊆ append_set (?TS n) (inputs M2)"
by blast
moreover have "finite (append_set (?TS n) (inputs M2))"
by (simp add: ‹finite (TS M2 M1 Ω V m n)› assms(2) finite_image_set2)
ultimately show ?thesis
using infinite_subset by auto
qed
ultimately show ?thesis
by auto
qed
qed
lemma C_finite :
assumes "finite V"
and "finite (inputs M2)"
shows "finite (C M2 M1 Ω V m n)"
proof -
have "C M2 M1 Ω V m n ⊆ TS M2 M1 Ω V m n"
by (simp add: C_subset)
then show ?thesis using TS_finite[OF assms]
using Finite_Set.finite_subset by blast
qed
subsection ‹ Final iteration ›
text ‹
The result of calculating @{verbatim TS} for some iteration is final if the result does not change
for the next iteration.
Such a final iteration exists and is at most equal to the number of states of FSM @{verbatim M2}
multiplied by an upper bound on the number of states of FSM @{verbatim M1}.
Furthermore, for any sequence not contained in the final iteration of the test suite, a prefix of
this sequence must be contained in the latter.
›
abbreviation "final_iteration M2 M1 Ω V m i ≡ TS M2 M1 Ω V m i = TS M2 M1 Ω V m (Suc i)"
lemma final_iteration_ex :
assumes "OFSM M1"
and "OFSM M2"
and "asc_fault_domain M2 M1 m"
and "test_tools M2 M1 FAIL PM V Ω"
shows "final_iteration M2 M1 Ω V m (Suc ( |M2| * m ))"
proof -
let ?i = "Suc ( |M2| * m )"
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "is_det_state_cover M2 V"
using assms by auto
moreover have "finite (nodes M2)"
using assms(2) by auto
moreover have "d_reachable M2 (initial M2) ⊆ nodes M2"
by auto
ultimately have "finite V"
using det_state_cover_card[of M2 V]
by (metis finite_if_finite_subsets_card_bdd infinite_subset is_det_state_cover.elims(2)
surj_card_le)
have "∀ seq ∈ ?C ?i . seq ∈ ?RM ?i"
proof
fix seq assume "seq ∈ ?C ?i"
show "seq ∈ ?RM ?i"
proof -
have "[] ∈ V"
using ‹is_det_state_cover M2 V› det_state_cover_empty
by blast
then obtain vs where "mcp seq V vs"
using mcp_ex[OF _ ‹finite V›]
by blast
then obtain xs where "seq = vs@xs"
using prefixE by auto
then have "Suc (length xs) = ?i" using C_index
using ‹mcp seq V vs› ‹seq ∈ C M2 M1 Ω V m (Suc ( |M2| * m))› by blast
then have "length xs = ( |M2| * m)" by auto
have RM_def : "?RM ?i = {xs' ∈ C M2 M1 Ω V m ?i .
(¬ (L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}))
∨ (∀ io ∈ L⇩i⇩n M1 {xs'} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) S1 Ω V'' ))))}"
using RM.simps(2)[of M2 M1 Ω V m "((card (nodes M2))*m)"] by assumption
have "(¬ (L⇩i⇩n M1 {seq} ⊆ L⇩i⇩n M2 {seq}))
∨ (∀ io ∈ L⇩i⇩n M1 {seq} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) S1 Ω V'' ))))"
proof (cases "(¬ (L⇩i⇩n M1 {seq} ⊆ L⇩i⇩n M2 {seq}))")
case True
then show ?thesis
using RM_def by blast
next
case False
have "(∀ io ∈ L⇩i⇩n M1 {seq} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) S1 Ω V'' ))))"
proof
fix io assume "io∈L⇩i⇩n M1 {seq}"
then have "io ∈ L M1"
by auto
moreover have "is_det_state_cover M2 V"
using assms(4) by auto
ultimately obtain V'' where "V'' ∈ N io M1 V"
using N_nonempty[OF _ assms(1-3), of V io] by blast
have "io ∈ L M2"
using ‹io∈L⇩i⇩n M1 {seq}› False by auto
have "V'' ∈ Perm V M1"
using ‹V'' ∈ N io M1 V› by auto
have "[] ∈ V''"
using ‹V'' ∈ Perm V M1› assms(4) perm_empty by blast
have "finite V''"
using ‹V'' ∈ Perm V M1› assms(2) assms(4) perm_elem_finite by blast
obtain vs where "mcp io V'' vs"
using mcp_ex[OF ‹[] ∈ V''› ‹finite V''›] by blast
obtain xs where "io = (vs@xs)"
using ‹mcp io V'' vs› prefixE by auto
then have "vs@xs ∈ L M1" "vs@xs ∈ L M2"
using ‹io ∈ L M1› ‹io ∈ L M2› by auto
have "io ∈ L M1" "map fst io ∈ {seq}"
using ‹io∈L⇩i⇩n M1 {seq}› by auto
then have "map fst io = seq"
by auto
then have "map fst io ∈ ?C ?i"
using ‹seq ∈ ?C ?i› by blast
then have "(map fst vs) @ (map fst xs) ∈ ?C ?i"
using ‹io = (vs@xs)› by (metis map_append)
have "mcp' io V'' = vs"
using ‹mcp io V'' vs› mcp'_intro by blast
have "mcp' (map fst io) V = (map fst vs)"
using ‹V'' ∈ N io M1 V› ‹mcp' io V'' = vs› by auto
then have "mcp (map fst io) V (map fst vs)"
by (metis ‹⋀thesis. (⋀vs. mcp seq V vs ⟹ thesis) ⟹ thesis›
‹map fst io = seq› mcp'_intro)
then have "mcp (map fst vs @ map fst xs) V (map fst vs)"
by (simp add: ‹io = vs @ xs›)
then have "Suc (length xs) = ?i" using C_index[OF ‹(map fst vs) @ (map fst xs) ∈ ?C ?i›]
by simp
then have "( |M2| * m) ≤ length xs"
by simp
have "|M1| ≤ m"
using assms(3) by auto
have "vs @ xs ∈ L M2 ∩ L M1"
using ‹vs @ xs ∈ L M1› ‹vs @ xs ∈ L M2› by blast
obtain q where "q ∈ nodes M2" "m < card (RP M2 q vs xs V'')"
using RP_state_repetition_distribution_productF
[OF assms(2,1) ‹( |M2| * m) ≤ length xs› ‹|M1| ≤ m› ‹vs @ xs ∈ L M2 ∩ L M1›
‹is_det_state_cover M2 V› ‹V'' ∈ Perm V M1›]
by blast
have "m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) {q} Ω V''"
proof -
have "m < (sum (λ s . card (RP M2 s vs xs V'')) {q})"
using ‹m < card (RP M2 q vs xs V'')›
by auto
moreover have "(sum (λ s . card (RP M2 s vs xs V'')) {q})
≤ LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) {q} Ω V''"
by auto
ultimately show ?thesis
by linarith
qed
show "∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) S1 Ω V''"
proof -
have "io = vs@xs"
using ‹io = vs@xs› by assumption
moreover have "mcp (vs@xs) V'' vs"
using ‹io = vs @ xs› ‹mcp io V'' vs› by presburger
moreover have "{q} ⊆ nodes M2"
using ‹q ∈ nodes M2› by auto
moreover have "(∀ s1 ∈ {q} . ∀ s2 ∈ {q} .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))"
proof -
have "∀ s1 ∈ {q} . ∀ s2 ∈ {q} . s1 = s2"
by blast
then show ?thesis
by blast
qed
ultimately have RM_body : "io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ {q} ⊆ nodes M2
∧ (∀ s1 ∈ {q} . ∀ s2 ∈ {q} .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) {q} Ω V'' "
using ‹m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) {q} Ω V''›
by linarith
show ?thesis
using ‹V''∈N io M1 V› RM_body
by metis
qed
qed
then show ?thesis
by metis
qed
then have "seq ∈ {xs' ∈ C M2 M1 Ω V m ((Suc ( |M2| * m))).
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (?TS (( |M2| * m)) ∪ V) S1 Ω V'')}"
using ‹seq ∈ ?C ?i› by blast
then show ?thesis
using RM_def by blast
qed
qed
then have "?C ?i - ?RM ?i = {}"
by blast
have "?C (Suc ?i) = append_set (?C ?i - ?RM ?i) (inputs M2) - ?TS ?i"
using C.simps(3) by blast
then have "?C (Suc ?i) = {}" using ‹?C ?i - ?RM ?i = {}›
by blast
then have "?TS (Suc ?i) = ?TS ?i"
using TS.simps(3) by blast
then show "final_iteration M2 M1 Ω V m ?i"
by blast
qed
lemma TS_non_containment_causes_final :
assumes "vs@xs ∉ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
and "set xs ⊆ inputs M2"
and "final_iteration M2 M1 Ω V m i"
and "OFSM M2"
shows "(∃ xr j . xr ≠ xs
∧ prefix xr xs
∧ j ≤ i
∧ vs@xr ∈ RM M2 M1 Ω V m j)"
proof -
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
have "{} ≠ V"
using assms(2) by fastforce
then have "?TS 0 ≠ ?TS (Suc 0)"
by simp
then have "0 < i"
using assms(4) by auto
have ncc1 : "(∃xr j. xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j) ∨
(∃xc. xc ≠ xs ∧ prefix xc xs ∧ vs @ xc ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i)"
using TS_non_containment_causes(1)[OF assms(1-3) ‹0 < i›] by assumption
have ncc2 : "¬ ((∃xr j. xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j) ∧
(∃xc. xc ≠ xs ∧ prefix xc xs ∧ vs @ xc ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i))"
using TS_non_containment_causes(2)[OF assms(1-3) ‹0 < i›] by assumption
from ncc1 show ?thesis
proof
show "∃xr j. xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j ⟹
∃xr j. xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j"
by simp
show "∃xc. xc ≠ xs ∧ prefix xc xs ∧ vs @ xc ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i ⟹
∃xr j. xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs @ xr ∈ RM M2 M1 Ω V m j"
proof -
assume "∃xc. xc ≠ xs ∧ prefix xc xs ∧ vs @ xc ∈ C M2 M1 Ω V m i - RM M2 M1 Ω V m i"
then obtain xc where "xc ≠ xs" "prefix xc xs" "vs @ xc ∈ ?C i - ?RM i"
by blast
then have "vs @ xc ∈ ?C i"
by blast
have "mcp (vs @ xc) V vs"
using ‹prefix xc xs› assms(2) mcp_prefix_of_suffix by blast
then have "Suc (length xc) = i" using C_index[OF ‹vs @ xc ∈ ?C i›]
by simp
have "length xc < length xs"
by (metis ‹prefix xc xs› ‹xc ≠ xs› append_eq_conv_conj nat_less_le prefix_def prefix_length_le take_all)
then obtain x where "prefix (vs@xc@[x]) (vs@xs)"
using ‹prefix xc xs› append_one_prefix same_prefix_prefix by blast
have "?TS (Suc i) = ?TS i"
using assms(4) by auto
have "vs@xc@[x] ∉ ?C (Suc i)"
proof
assume "vs @ xc @ [x] ∈ ?C (Suc i)"
then have "vs @ xc @ [x] ∉ ?TS i"
by (metis (no_types, lifting) C.simps(3) DiffE ‹Suc (length xc) = i›)
then have "?TS i ≠ ?TS (Suc i)"
using C_subset ‹vs @ xc @ [x] ∈ C M2 M1 Ω V m (Suc i)› by blast
then show "False" using assms(4)
by auto
qed
moreover have "?C (Suc i) = append_set (?C i - ?RM i) (inputs M2) - ?TS i"
using C.simps(3) ‹Suc (length xc) = i› by blast
ultimately have "vs @ xc @ [x] ∉ append_set (?C i - ?RM i) (inputs M2) - ?TS i"
by blast
have "vs @ xc @ [x] ∉ ?TS (Suc i)"
by (metis Suc_n_not_le_n TS_index(1) ‹Suc (length xc) = i›
‹prefix (vs @ xc @ [x]) (vs @ xs)› assms(2) assms(4) length_append_singleton
mcp_prefix_of_suffix same_prefix_prefix)
then have "vs @ xc @ [x] ∉ ?TS i"
by (simp add: assms(4))
have "vs @ xc @ [x] ∉ append_set (?C i - ?RM i) (inputs M2)"
using ‹vs @ xc @ [x] ∉ TS M2 M1 Ω V m i›
‹vs @ xc @ [x] ∉ append_set (C M2 M1 Ω V m i - RM M2 M1 Ω V m i) (inputs M2)
- TS M2 M1 Ω V m i›
by blast
then have "vs @ xc ∉ (?C i - ?RM i)"
proof -
have f1: "∀a A Aa. (a::'a) ∉ A ∧ a ∉ Aa ∨ a ∈ Aa ∪ A"
by (meson UnCI)
obtain aas :: "'a list ⇒ 'a list ⇒ 'a list" where
"∀x0 x1. (∃v2. x0 = x1 @ v2) = (x0 = x1 @ aas x0 x1)"
by moura
then have "vs @ xs = (vs @ xc @ [x]) @ aas (vs @ xs) (vs @ xc @ [x])"
by (meson ‹prefix (vs @ xc @ [x]) (vs @ xs)› prefixE)
then have "xs = (xc @ [x]) @ aas (vs @ xs) (vs @ xc @ [x])"
by simp
then have "x ∈ inputs M2"
using f1 by (metis (no_types) assms(3) contra_subsetD insert_iff list.set(2) set_append)
then show ?thesis
using ‹vs @ xc @ [x] ∉ append_set (C M2 M1 Ω V m i - RM M2 M1 Ω V m i) (inputs M2)›
by force
qed
then have "False"
using ‹vs @ xc ∈ ?C i - ?RM i› by blast
then show ?thesis by simp
qed
qed
qed
lemma TS_non_containment_causes_final_suc :
assumes "vs@xs ∉ TS M2 M1 Ω V m i"
and "mcp (vs@xs) V vs"
and "set xs ⊆ inputs M2"
and "final_iteration M2 M1 Ω V m i"
and "OFSM M2"
obtains xr j
where "xr ≠ xs" "prefix xr xs" "Suc j ≤ i" "vs@xr ∈ RM M2 M1 Ω V m (Suc j)"
proof -
obtain xr j where "xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m j"
using TS_non_containment_causes_final[OF assms] by blast
moreover have "RM M2 M1 Ω V m 0 = {}"
by auto
ultimately have "j ≠ 0"
by (metis empty_iff)
then obtain jp where "j = Suc jp"
using not0_implies_Suc by blast
then have "xr ≠ xs ∧ prefix xr xs ∧ Suc jp ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m (Suc jp)"
using ‹xr ≠ xs ∧ prefix xr xs ∧ j ≤ i ∧ vs@xr ∈ RM M2 M1 Ω V m j›
by blast
then show ?thesis
using that by blast
qed
end