Theory SPY_Framework
section ‹SPY-Framework›
text ‹This theory defines the SPY-Framework and provides completeness properties.›
theory SPY_Framework
imports H_Framework
begin
subsection ‹Definition of the Framework›
definition spy_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒
(('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment) ⇒
(('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ (('b×'c) prefix_tree × 'd)) ⇒
(('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('a,'b,'c) transition list ⇒ ('a,'b,'c) transition list) ⇒
(('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ nat ⇒ ('a,'b,'c) transition ⇒ (('b×'c) prefix_tree × 'd)) ⇒
(('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 'a ⇒ 'b ⇒ 'c ⇒ (('b×'c) prefix_tree) × 'd) ⇒
(('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
nat ⇒
('b×'c) prefix_tree"
where
"spy_framework M
get_state_cover
separate_state_cover
sort_unverified_transitions
establish_convergence
append_io_pair
cg_initial
cg_insert
cg_lookup
cg_merge
m
= (let
rstates_set = reachable_states M;
rstates = reachable_states_as_list M;
rstates_io = List.product rstates (List.product (inputs_as_list M) (outputs_as_list M));
undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M q x y = None) rstates_io;
V = get_state_cover M;
n = size_r M;
TG1 = separate_state_cover M V cg_initial cg_insert cg_lookup;
sc_covered_transitions = (⋃ q ∈ rstates_set . covered_transitions M V (V q));
unverified_transitions = sort_unverified_transitions M V (filter (λt . t_source t ∈ rstates_set ∧ t ∉ sc_covered_transitions) (transitions_as_list M));
verify_transition = (λ (T,G) t . let TGxy = append_io_pair M V T G cg_insert cg_lookup (t_source t) (t_input t) (t_output t);
(T',G') = establish_convergence M V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t;
G'' = cg_merge G' ((V (t_source t)) @ [(t_input t, t_output t)]) (V (t_target t))
in (T',G''));
TG2 = foldl verify_transition TG1 unverified_transitions;
verify_undefined_io_pair = (λ T (q,(x,y)) . fst (append_io_pair M V T (snd TG2) cg_insert cg_lookup q x y))
in
foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs)"
subsection ‹Required Conditions on Procedural Parameters›
definition verifies_transition :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
('a,'b,'c) state_cover_assignment ⇒
('b×'c) prefix_tree ⇒
'd ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
nat ⇒
('a,'b,'c) transition ⇒
(('b×'c) prefix_tree × 'd)) ⇒
('a::linorder,'b::linorder,'c::linorder) fsm ⇒
('e,'b,'c) fsm ⇒
('a,'b,'c) state_cover_assignment ⇒
('b×'c) prefix_tree ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
bool"
where
"verifies_transition f M1 M2 V T0 cg_insert cg_lookup =
(∀ T G m t .
(set T ⊆ set (fst (f M1 V T G cg_insert cg_lookup m t)))
∧ (finite_tree T ⟶ finite_tree (fst (f M1 V T G cg_insert cg_lookup m t)))
∧ (observable M1 ⟶
observable M2 ⟶
minimal M1 ⟶
minimal M2 ⟶
size_r M1 ≤ m ⟶
size M2 ≤ m ⟶
inputs M2 = inputs M1 ⟶
outputs M2 = outputs M1 ⟶
is_state_cover_assignment M1 V ⟶
preserves_divergence M1 M2 (V ` reachable_states M1) ⟶
V ` reachable_states M1 ⊆ set T ⟶
t ∈ transitions M1 ⟶
t_source t ∈ reachable_states M1 ⟶
((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t)) ⟶
((V (t_source t)) @ [(t_input t,t_output t)]) ∈ L M2 ⟶
convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup m t)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup m t)) ⟶
(set T0 ⊆ set T) ⟶
(converge M2 ((V (t_source t)) @ [(t_input t,t_output t)]) (V (t_target t)))
∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup m t))))"
definition verifies_io_pair :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
('a,'b,'c) state_cover_assignment ⇒
('b×'c) prefix_tree ⇒
'd ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
'a ⇒ 'b ⇒ 'c ⇒
(('b×'c) prefix_tree × 'd)) ⇒
('a::linorder,'b::linorder,'c::linorder) fsm ⇒
('e,'b,'c) fsm ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
bool"
where
"verifies_io_pair f M1 M2 cg_insert cg_lookup =
(∀ V T G q x y .
(set T ⊆ set (fst (f M1 V T G cg_insert cg_lookup q x y)))
∧ (finite_tree T ⟶ finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y)))
∧ (observable M1 ⟶
observable M2 ⟶
minimal M1 ⟶
minimal M2 ⟶
inputs M2 = inputs M1 ⟶
outputs M2 = outputs M1 ⟶
is_state_cover_assignment M1 V ⟶
L M1 ∩ (V ` reachable_states M1) = L M2 ∩ V ` reachable_states M1 ⟶
q ∈ reachable_states M1 ⟶
x ∈ inputs M1 ⟶
y ∈ outputs M1 ⟶
convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) ⟶
(∃ α .
converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set (fst (f M1 V T G cg_insert cg_lookup q x y)) ∧
α@[(x,y)] ∈ set (fst (f M1 V T G cg_insert cg_lookup q x y)))
∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))))"
lemma verifies_io_pair_handled:
assumes "verifies_io_pair f M1 M2 cg_insert cg_lookup"
shows "handles_io_pair f M1 M2 cg_insert cg_lookup"
proof -
have *:"⋀ V T G q x y . set T ⊆ set (fst (f M1 V T G cg_insert cg_lookup q x y))"
using assms unfolding verifies_io_pair_def
by metis
have ***:"⋀ V T G q x y . finite_tree T ⟶ finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))"
using assms unfolding verifies_io_pair_def
by metis
have **:"⋀ V T G q x y.
observable M1 ⟹
observable M2 ⟹
minimal M1 ⟹
minimal M2 ⟹
FSM.inputs M2 = FSM.inputs M1 ⟹
FSM.outputs M2 = FSM.outputs M1 ⟹
is_state_cover_assignment M1 V ⟹
L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1 ⟹
q ∈ reachable_states M1 ⟹
x ∈ inputs M1 ⟹
y ∈ outputs M1 ⟹
convergence_graph_lookup_invar M1 M2 cg_lookup G ⟹
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟹
L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) ⟹
( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )
∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
proof -
fix V T G q x y
assume a01: "observable M1"
moreover assume a02: "observable M2"
moreover assume a03: "minimal M1"
moreover assume a04: "minimal M2"
moreover assume a05: "FSM.inputs M2 = FSM.inputs M1"
moreover assume a06: "FSM.outputs M2 = FSM.outputs M1"
moreover assume a07: "is_state_cover_assignment M1 V"
moreover assume a09: "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
moreover assume a10: "q ∈ reachable_states M1"
moreover assume a11: "x ∈ inputs M1"
moreover assume a12: "y ∈ outputs M1"
moreover assume a13: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
moreover assume a14: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
moreover assume a15: "L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y))"
ultimately have *:"(∃α. converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) ∧ α @ [(x, y)] ∈ Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)))"
and **: "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
using assms unfolding verifies_io_pair_def
by presburger+
have "( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )"
proof -
obtain α where "converge M1 α (V q)" and "converge M2 α (V q)" and "α @ [(x, y)] ∈ Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))"
using * by blast
have "(V q)@[(x,y)] ∈ L M1 = (α@[(x,y)] ∈ L M1)"
using ‹converge M1 α (V q)› using a01 a07
by (meson converge_append_language_iff)
moreover have "(V q)@[(x,y)] ∈ L M2 = (α@[(x,y)] ∈ L M2)"
using ‹converge M2 α (V q)› using a02 a07
by (meson converge_append_language_iff)
moreover have "α @ [(x, y)] ∈ L M1 = (α @ [(x, y)] ∈ L M2)"
using ‹α @ [(x, y)] ∈ Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))› a15
by blast
ultimately show ?thesis
by blast
qed
then show "( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} ) ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
using ** by blast
qed
show ?thesis
unfolding handles_io_pair_def
using * *** ** by presburger
qed
subsection ‹Completeness and Finiteness of the Framework›
lemma spy_framework_completeness_and_finiteness :
fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
fixes M2 :: "('d,'b,'c) fsm"
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "size_r M1 ≤ m"
and "size M2 ≤ m"
and "inputs M2 = inputs M1"
and "outputs M2 = outputs M1"
and "is_state_cover_assignment M1 (get_state_cover M1)"
and "⋀ xs . List.set xs = List.set (sort_unverified_transitions M1 (get_state_cover M1) xs)"
and "convergence_graph_initial_invar M1 M2 cg_lookup cg_initial"
and "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
and "convergence_graph_merge_invar M1 M2 cg_lookup cg_merge"
and "separates_state_cover separate_state_cover M1 M2 cg_initial cg_insert cg_lookup"
and "verifies_transition establish_convergence M1 M2 (get_state_cover M1) (fst (separate_state_cover M1 (get_state_cover M1) cg_initial cg_insert cg_lookup)) cg_insert cg_lookup"
and "verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (spy_framework M1 get_state_cover separate_state_cover sort_unverified_transitions establish_convergence append_io_pair cg_initial cg_insert cg_lookup cg_merge m))
= (L M2 ∩ set (spy_framework M1 get_state_cover separate_state_cover sort_unverified_transitions establish_convergence append_io_pair cg_initial cg_insert cg_lookup cg_merge m)))"
(is "(L M1 = L M2) ⟷ ((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))")
and "finite_tree (spy_framework M1 get_state_cover separate_state_cover sort_unverified_transitions establish_convergence append_io_pair cg_initial cg_insert cg_lookup cg_merge m)"
proof
show "(L M1 = L M2) ⟹ ((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
by blast
define rstates where rstates: "rstates = reachable_states_as_list M1"
define rstates_io where rstates_io: "rstates_io = List.product rstates (List.product (inputs_as_list M1) (outputs_as_list M1))"
define undefined_io_pairs where undefined_io_pairs: "undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M1 q x y = None) rstates_io"
define V where V: "V = get_state_cover M1"
define n where n: "n = size_r M1"
define TG1 where TG1: "TG1 = separate_state_cover M1 V cg_initial cg_insert cg_lookup"
define sc_covered_transitions where sc_covered_transitions: "sc_covered_transitions = (⋃ q ∈ reachable_states M1 . covered_transitions M1 V (V q))"
define unverified_transitions where unverified_transitions: "unverified_transitions = sort_unverified_transitions M1 V (filter (λt . t_source t ∈ reachable_states M1 ∧ t ∉ sc_covered_transitions) (transitions_as_list M1))"
define verify_transition where verify_transition: "verify_transition = (λ (T,G) t . let TGxy = append_io_pair M1 V T G cg_insert cg_lookup (t_source t) (t_input t) (t_output t);
(T',G') = establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t;
G'' = cg_merge G' ((V (t_source t)) @ [(t_input t, t_output t)]) (V (t_target t))
in (T',G''))"
define TG2 where TG2: "TG2 = (foldl verify_transition TG1 unverified_transitions)"
define verify_undefined_io_pair where verify_undefined_io_pair: "verify_undefined_io_pair = (λ T (q,(x,y)) . fst (append_io_pair M1 V T (snd TG2) cg_insert cg_lookup q x y))"
define T3 where T3: "T3 = foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs"
have "?TS = T3"
unfolding rstates rstates_io undefined_io_pairs V n TG1 sc_covered_transitions unverified_transitions verify_transition TG2 verify_undefined_io_pair T3
unfolding spy_framework_def Let_def
by force
then have "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3"
by simp
have "is_state_cover_assignment M1 V"
unfolding V using assms(9) .
define T1 where T1: "T1 = fst TG1"
moreover define G1 where G1: "G1 = snd TG1"
ultimately have "TG1 = (T1,G1)"
by auto
have T1_state_cover: "V ` reachable_states M1 ⊆ set T1"
and T1_finite: "finite_tree T1"
using ‹separates_state_cover separate_state_cover M1 M2 cg_initial cg_insert cg_lookup›
unfolding T1 TG1 separates_state_cover_def
by blast+
have T1_V_div: "(L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ preserves_divergence M1 M2 (V ` reachable_states M1)"
and G1_invar: "(L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G1"
using ‹separates_state_cover separate_state_cover M1 M2 cg_initial cg_insert cg_lookup›
unfolding T1 G1 TG1 separates_state_cover_def
using assms(1-4,7,8) ‹is_state_cover_assignment M1 V› assms(12,11)
by blast+
have "verifies_transition establish_convergence M1 M2 V T1 cg_insert cg_lookup"
using assms(15)
unfolding T1 TG1 V .
have sc_covered_transitions_alt_def: "sc_covered_transitions = {t . t ∈ transitions M1 ∧ t_source t ∈ reachable_states M1 ∧ (V (t_target t) = (V (t_source t))@[(t_input t, t_output t)])}"
(is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix t assume "t ∈ ?A"
then obtain q where "t ∈ covered_transitions M1 V (V q)" and "q ∈ reachable_states M1"
unfolding sc_covered_transitions
by blast
then have "V q ∈ L M1" and "after_initial M1 (V q) = q"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by blast+
then obtain p where "path M1 (initial M1) p" and "p_io p = V q"
by auto
then have *: "the_elem (paths_for_io M1 (initial M1) (V q)) = p"
using observable_paths_for_io[OF assms(1) ‹V q ∈ L M1›]
unfolding paths_for_io_def
by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)
have "t ∈ list.set p" and "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
using ‹t ∈ covered_transitions M1 V (V q)›
unfolding covered_transitions_def Let_def *
by auto
have "t ∈ transitions M1"
using ‹t ∈ list.set p› ‹path M1 (initial M1) p›
by (meson path_transitions subsetD)
moreover have "t_source t ∈ reachable_states M1"
using reachable_states_path[OF reachable_states_initial ‹path M1 (initial M1) p› ‹t ∈ list.set p›] .
ultimately show "t ∈ ?B"
using ‹V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)›
by auto
qed
show "?B ⊆ ?A"
proof
fix t assume "t ∈ ?B"
then have "t ∈ transitions M1"
"t_source t ∈ reachable_states M1"
"(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
by auto
then have "t_target t ∈ reachable_states M1"
using reachable_states_next[of "t_source t" M1 t]
by blast
then have "V (t_target t) ∈ L M1" and "after_initial M1 (V (t_target t)) = (t_target t)"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by blast+
then obtain p where "path M1 (initial M1) p" and "p_io p = V (t_target t)"
by auto
then have *: "the_elem (paths_for_io M1 (initial M1) (V (t_target t))) = p"
using observable_paths_for_io[OF assms(1) ‹V (t_target t) ∈ L M1›]
unfolding paths_for_io_def
by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)
have "V (t_source t) ∈ L M1" and "after_initial M1 (V (t_source t)) = (t_source t)"
using ‹t_source t ∈ reachable_states M1›
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by blast+
then obtain p' where "path M1 (initial M1) p'" and "p_io p' = V (t_source t)"
by auto
have "path M1 (initial M1) (p'@[t])"
using after_path[OF assms(1) ‹path M1 (initial M1) p'›] ‹path M1 (initial M1) p'› ‹t∈transitions M1›
unfolding ‹p_io p' = V (t_source t)›
unfolding ‹after_initial M1 (V (t_source t)) = (t_source t)›
by (metis path_append single_transition_path)
moreover have "p_io (p'@[t]) = p_io p"
using ‹p_io p' = V (t_source t)›
unfolding ‹p_io p = V (t_target t)› ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›[symmetric]
by auto
ultimately have "p'@[t] = p"
using observable_path_unique[OF assms(1) _ ‹path M1 (initial M1) p›]
by force
then have "t ∈ list.set p"
by auto
then have "t ∈ covered_transitions M1 V (V (t_target t))"
using ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›
unfolding covered_transitions_def Let_def *
by auto
then show "t ∈ ?A"
using ‹t_target t ∈ reachable_states M1›
unfolding sc_covered_transitions
by blast
qed
qed
have T1_covered_transitions_conv: "⋀ t . (L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ t ∈ sc_covered_transitions ⟹ converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
proof -
fix t assume "(L M1 ∩ set T1 = (L M2 ∩ set T1))"
"t ∈ sc_covered_transitions"
then have "t ∈ transitions M1"
"t_source t ∈ reachable_states M1"
"(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
unfolding sc_covered_transitions_alt_def
by auto
then have "t_target t ∈ reachable_states M1"
using reachable_states_next[of "t_source t" M1 t]
by blast
then have "V (t_target t) ∈ L M1"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by blast
moreover have "V (t_target t) ∈ set T1"
using T1_state_cover ‹t_target t ∈ reachable_states M1›
by blast
ultimately have "V (t_target t) ∈ L M2"
using ‹(L M1 ∩ set T1 = (L M2 ∩ set T1))›
by blast
then show "converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
unfolding ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›
by auto
qed
have unverified_transitions_alt_def : "list.set unverified_transitions = {t . t ∈ transitions M1 ∧ t_source t ∈ reachable_states M1 ∧ (V (t_target t) ≠ (V (t_source t))@[(t_input t, t_output t)])}"
unfolding unverified_transitions sc_covered_transitions_alt_def V
unfolding assms(10)[symmetric]
using transitions_as_list_set[of M1]
by auto
have cg_insert_invar : "⋀ G γ . γ ∈ L M1 ⟹ γ ∈ L M2 ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G γ)"
using assms(12)
unfolding convergence_graph_insert_invar_def
by blast
have cg_merge_invar : "⋀ G γ γ'. convergence_graph_lookup_invar M1 M2 cg_lookup G ⟹ converge M1 γ γ' ⟹ converge M2 γ γ' ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_merge G γ γ')"
using assms(13)
unfolding convergence_graph_merge_invar_def
by blast
define T2 where T2: "T2 = fst TG2"
define G2 where G2: "G2 = snd TG2"
have verify_transition_retains_testsuite: "⋀ t T G . set T ⊆ set (fst (verify_transition (T,G) t))"
proof -
fix t T G
define TGxy where TGxy: "TGxy = append_io_pair M1 V T G cg_insert cg_lookup (t_source t) (t_input t) (t_output t)"
obtain T' G' where TG': "(T',G') = establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t"
using prod.exhaust by metis
define G'' where G'': "G'' = cg_merge G' ((V (t_source t)) @ [(t_input t, t_output t)]) (V (t_target t))"
have *:"verify_transition (T,G) t = (T',G'')"
using TG'[symmetric]
unfolding verify_transition G'' TGxy Let_def case_prod_conv
by force
have "set T ⊆ set (fst TGxy)"
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup›
unfolding verifies_io_pair_def TGxy
by blast
also have "set (fst TGxy) ⊆ set (fst (T',G'))"
using ‹verifies_transition establish_convergence M1 M2 V T1 cg_insert cg_lookup›
unfolding TG' verifies_transition_def
by blast
finally show "set T ⊆ set (fst (verify_transition (T,G) t))"
unfolding * fst_conv .
qed
have verify_transition_retains_finiteness: "⋀ t T G . finite_tree T ⟹ finite_tree (fst (verify_transition (T,G) t))"
proof -
fix T :: "('b×'c) prefix_tree"
fix t G assume "finite_tree T"
define TGxy where TGxy: "TGxy = append_io_pair M1 V T G cg_insert cg_lookup (t_source t) (t_input t) (t_output t)"
obtain T' G' where TG': "(T',G') = establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t"
using prod.exhaust by metis
define G'' where G'': "G'' = cg_merge G' ((V (t_source t)) @ [(t_input t, t_output t)]) (V (t_target t))"
have *:"verify_transition (T,G) t = (T',G'')"
using TG'[symmetric]
unfolding verify_transition G'' TGxy Let_def case_prod_conv
by force
have "finite_tree (fst TGxy)"
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup› ‹finite_tree T›
unfolding verifies_io_pair_def TGxy
by blast
then have "finite_tree (fst (T',G'))"
using ‹verifies_transition establish_convergence M1 M2 V T1 cg_insert cg_lookup›
unfolding TG' verifies_transition_def
by blast
then show "finite_tree (fst (verify_transition (T,G) t))"
unfolding * fst_conv .
qed
define covers_unverified_transition
where covers_unverified_transition: "covers_unverified_transition = (λt (T',G') .
((∃ α β . converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
converge M1 β (V (t_target t)) ∧
converge M2 β (V (t_target t)) ∧
α@[(t_input t,t_output t)] ∈ (set T') ∧
β ∈ (set T'))
∧ (converge M2 ((V (t_source t)) @ [(t_input t,t_output t)]) (V (t_target t)))
∧ convergence_graph_lookup_invar M1 M2 cg_lookup G'))"
have verify_transition_cover_prop: "⋀ t T G . (L M1 ∩ (set (fst (verify_transition (T,G) t))) = L M2 ∩ (set (fst (verify_transition (T,G) t))))
⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G
⟹ t ∈ transitions M1
⟹ t_source t ∈ reachable_states M1
⟹ ((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))
⟹ set T1 ⊆ set T
⟹ covers_unverified_transition t (verify_transition (T,G) t)"
proof -
fix t T G
assume a1: "(L M1 ∩ (set (fst (verify_transition (T,G) t))) = L M2 ∩ (set (fst (verify_transition (T,G) t))))"
assume a2: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
assume a3: "t ∈ transitions M1"
assume a4: "t_source t ∈ reachable_states M1"
assume a5: "set T1 ⊆ set T"
assume a6: "((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))"
define TGxy where TGxy: "TGxy = append_io_pair M1 V T G cg_insert cg_lookup (t_source t) (t_input t) (t_output t)"
obtain T' G' where TG': "(T',G') = establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t"
using prod.exhaust by metis
have T': "T' = fst (establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t)"
and G': "G' = snd (establish_convergence M1 V (fst TGxy) (snd TGxy) cg_insert cg_lookup m t)"
unfolding TG'[symmetric] by auto
define G'' where G'': "G'' = cg_merge G' ((V (t_source t)) @ [(t_input t, t_output t)]) (V (t_target t))"
have "verify_transition (T,G) t = (T',G'')"
using TG'[symmetric]
unfolding verify_transition G'' TGxy Let_def case_prod_conv
by force
then have "set T ⊆ set T'"
using verify_transition_retains_testsuite[of T G t] unfolding T'
by auto
then have "(L M1 ∩ (set T1) = L M2 ∩ (set T1))"
using a1 a5 unfolding ‹verify_transition (T,G) t = (T',G'')› fst_conv
by blast
then have *: "preserves_divergence M1 M2 (V ` reachable_states M1)"
using T1_V_div
by auto
have "set (fst TGxy) ⊆ set (fst (T',G'))"
using ‹verifies_transition establish_convergence M1 M2 V T1 cg_insert cg_lookup›
unfolding TG' verifies_transition_def
by blast
then have "set (fst TGxy) ⊆ set (fst (verify_transition (T,G) t))"
unfolding ‹verify_transition (T,G) t = (T',G'')› fst_conv .
then have "L M1 ∩ set (fst TGxy) = L M2 ∩ set (fst TGxy)"
using a1 by blast
have "L M1 ∩ set T' = L M2 ∩ set T'" and "L M1 ∩ set T = L M2 ∩ set T"
using a1 ‹set T ⊆ set T'› unfolding T' ‹verify_transition (T,G) t = (T',G'')› fst_conv
by blast+
have **: "V ` reachable_states M1 ⊆ set T"
using a5 T1_state_cover by blast
have "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
using T1_state_cover ‹L M1 ∩ Prefix_Tree.set T1 = L M2 ∩ Prefix_Tree.set T1› by blast
have "(∃α. converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
α ∈ Prefix_Tree.set (fst TGxy) ∧
α @ [((t_input t), (t_output t))] ∈ Prefix_Tree.set (fst TGxy))"
and "convergence_graph_lookup_invar M1 M2 cg_lookup (snd TGxy)"
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup›
unfolding verifies_io_pair_def
using assms(1-4,7,8) ‹is_state_cover_assignment M1 V› ‹L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1› a4 fsm_transition_input[OF a3] fsm_transition_output[OF a3] a2 ‹convergence_graph_insert_invar M1 M2 cg_lookup cg_insert› ‹L M1 ∩ set (fst TGxy) = L M2 ∩ set (fst TGxy)›
unfolding TGxy
by blast+
then obtain w where "converge M1 w (V (t_source t))"
"converge M2 w (V (t_source t))"
"w ∈ Prefix_Tree.set (fst TGxy)"
"w @ [((t_input t), (t_output t))] ∈ set (fst TGxy)"
by blast
then have "w @ [((t_input t), (t_output t))] ∈ L M1 ⟷ w @ [((t_input t), (t_output t))] ∈ L M2"
using ‹L M1 ∩ set (fst TGxy) = L M2 ∩ set (fst TGxy)›
by blast
moreover have "w @ [((t_input t), (t_output t))] ∈ L M1 ⟷ V (t_source t) @ [(t_input t, t_output t)] ∈ L M1"
using ‹converge M1 w (V (t_source t))›
by (meson assms(1) converge_append_language_iff)
moreover have "V (t_source t) @ [(t_input t, t_output t)] ∈ L M1"
using state_cover_transition_converges[OF assms(1) ‹is_state_cover_assignment M1 V› ‹t ∈ transitions M1› ‹t_source t ∈ reachable_states M1›]
by auto
ultimately have "w @ [(t_input t, t_output t)] ∈ L M2"
by blast
then have "V (t_source t) @ [(t_input t, t_output t)] ∈ L M2"
using ‹converge M2 w (V (t_source t))›
by (meson assms(2) converge_append_language_iff)
have "V ` reachable_states M1 ⊆ set T"
using a5 T1_state_cover by blast
have "set T ⊆ set (fst TGxy)"
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup›
unfolding verifies_io_pair_def TGxy by blast
then have "set T1 ⊆ set (fst TGxy)"
using a5 by blast
then have "⋀ io . set (after T1 io) ⊆ set (after (fst TGxy) io)"
unfolding after_set by auto
have "V ` reachable_states M1 ⊆ set (fst TGxy)"
using "**" ‹Prefix_Tree.set T ⊆ Prefix_Tree.set (fst TGxy)› by auto
have p2: "converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))"
and "convergence_graph_lookup_invar M1 M2 cg_lookup G'"
using ‹verifies_transition establish_convergence M1 M2 V T1 cg_insert cg_lookup›
unfolding verifies_transition_def
using assms(1-8) ‹is_state_cover_assignment M1 V› ‹preserves_divergence M1 M2 (V ` reachable_states M1)› ‹V ` reachable_states M1 ⊆ set (fst TGxy)› a3 a4 a6 ‹V (t_source t) @ [(t_input t, t_output t)] ∈ L M2› ‹convergence_graph_lookup_invar M1 M2 cg_lookup (snd TGxy)› ‹convergence_graph_insert_invar M1 M2 cg_lookup cg_insert› ‹L M1 ∩ set T' = L M2 ∩ set T'›
using ‹set T1 ⊆ set (fst TGxy)›
unfolding T' G'
by blast+
have "w @ [((t_input t), (t_output t))] ∈ set T'"
using ‹w @ [((t_input t), (t_output t))] ∈ set (fst TGxy)›
using T' ‹Prefix_Tree.set (fst TGxy) ⊆ Prefix_Tree.set (fst (T', G'))› by auto
have p1: "(∃α β.
converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
converge M1 β (V (t_target t)) ∧
converge M2 β (V (t_target t)) ∧
α @ [(t_input t, t_output t)] ∈ set T' ∧
β ∈ set T')"
proof -
have "V (t_source t) ∈ L M1"
using state_cover_assignment_after(1)[OF assms(1) ‹is_state_cover_assignment M1 V› ‹t_source t ∈ reachable_states M1›] .
have "V (t_target t) ∈ L M1"
using state_cover_assignment_after(1)[OF assms(1) ‹is_state_cover_assignment M1 V› reachable_states_next[OF ‹t_source t ∈ reachable_states M1› ‹t ∈ transitions M1›]]
by auto
note ‹converge M1 w (V (t_source t))› and ‹converge M2 w (V (t_source t))›
moreover have "converge M1 (V (t_target t)) (V (t_target t))"
using ‹V (t_target t) ∈ L M1› by auto
moreover have "converge M2 (V (t_target t)) (V (t_target t))"
using reachable_states_next[OF ‹t_source t ∈ reachable_states M1› ‹t ∈ transitions M1›] ‹V (t_target t) ∈ L M1› ‹L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1›
by auto
moreover note ‹w @ [(t_input t, t_output t)] ∈ set T'›
moreover have "V (t_target t) ∈ set T'"
using ‹V ` reachable_states M1 ⊆ set T› ‹set T ⊆ set T'› reachable_states_next[OF ‹t_source t ∈ reachable_states M1› ‹t ∈ transitions M1›]
by auto
ultimately show ?thesis
by blast
qed
have p3: "convergence_graph_lookup_invar M1 M2 cg_lookup G''"
unfolding G''
using cg_merge_invar[OF ‹convergence_graph_lookup_invar M1 M2 cg_lookup G'›]
state_cover_transition_converges[OF assms(1) ‹is_state_cover_assignment M1 V› a3 a4]
‹converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))›
by blast
show "covers_unverified_transition t (verify_transition (T,G) t)"
using p1 p2 p3
unfolding ‹verify_transition (T,G) t = (T',G'')› fst_conv snd_conv covers_unverified_transition
by blast
qed
have verify_transition_foldl_invar_1: "⋀ ts . list.set ts ⊆ list.set unverified_transitions ⟹
set T1 ⊆ set (fst (foldl verify_transition (T1, G1) ts)) ∧ finite_tree (fst (foldl verify_transition (T1, G1) ts))"
proof -
fix ts assume "list.set ts ⊆ list.set unverified_transitions"
then show "set T1 ⊆ set (fst (foldl verify_transition (T1, G1) ts)) ∧ finite_tree (fst (foldl verify_transition (T1, G1) ts))"
proof (induction ts rule: rev_induct)
case Nil
then show ?case
using T1_finite by auto
next
case (snoc t ts)
then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1"
unfolding unverified_transitions_alt_def
by force+
have p1: "list.set ts ⊆ list.set unverified_transitions"
using snoc.prems(1) by auto
have "set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t])))"
using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
by (metis eq_fst_iff)
have **: "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))"
and ***: "finite_tree (fst (foldl verify_transition (T1, G1) ts))"
using snoc.IH[OF p1]
by auto
have "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) (ts@[t])))"
using ** verify_transition_retains_testsuite ‹set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t])))›
by auto
moreover have "finite_tree (fst (foldl verify_transition (T1, G1) (ts@[t])))"
using verify_transition_retains_finiteness[OF ***, of "snd (foldl verify_transition (T1, G1) ts)"]
by auto
ultimately show ?case
by simp
qed
qed
then have T2_invar_1: "set T1 ⊆ set T2"
and T2_finite : "finite_tree T2"
unfolding TG2 G2 T2 ‹TG1 = (T1,G1)›
by auto
have verify_transition_foldl_invar_2: "⋀ ts . list.set ts ⊆ list.set unverified_transitions ⟹
L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts)) ⟹
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) ts))"
proof -
fix ts assume "list.set ts ⊆ list.set unverified_transitions"
and "L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts))"
then show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) ts))"
proof (induction ts rule: rev_induct)
case Nil
then show ?case
using G1_invar by auto
next
case (snoc t ts)
then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1" and "((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))"
unfolding unverified_transitions_alt_def
by force+
have p1: "list.set ts ⊆ list.set unverified_transitions"
using snoc.prems(1) by auto
have "set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t])))"
using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
by (metis eq_fst_iff)
then have p2: "L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts))"
using snoc.prems(2)
by blast
have *:"convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) ts))"
using snoc.IH[OF p1 p2]
by auto
have **: "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))"
using verify_transition_foldl_invar_1[OF p1] by blast
have "covers_unverified_transition t (verify_transition (fst (foldl verify_transition (T1, G1) ts), snd (foldl verify_transition (T1, G1) ts)) t)"
using verify_transition_cover_prop[OF _ * ‹t ∈ transitions M1› ‹t_source t ∈ reachable_states M1› ‹((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))› **] snoc.prems(2)
unfolding prod.collapse
by auto
then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (verify_transition (fst (foldl verify_transition (T1, G1) ts), snd (foldl verify_transition (T1, G1) ts)) t))"
unfolding covers_unverified_transition
by auto
then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) (ts@[t])))"
by auto
moreover have "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) (ts@[t])))"
using ** verify_transition_retains_testsuite ‹set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t])))›
by auto
ultimately show ?case
by simp
qed
qed
then have T2_invar_2: "L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G2"
unfolding TG2 G2 T2 ‹TG1 = (T1,G1)› by auto
have T2_cover: "⋀ t . L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ t ∈ list.set unverified_transitions ⟹ covers_unverified_transition t (T2,G2)"
proof -
have "⋀ t ts . t ∈ list.set ts ⟹ list.set ts ⊆ list.set unverified_transitions ⟹ L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts)) ⟹ covers_unverified_transition t (foldl verify_transition (T1, G1) ts)"
proof -
fix t ts
assume "t ∈ list.set ts" and "list.set ts ⊆ list.set unverified_transitions" and "L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts))"
then show "covers_unverified_transition t (foldl verify_transition (T1, G1) ts)"
proof (induction ts rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc t' ts)
then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1" and "((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))"
unfolding unverified_transitions_alt_def by force+
have "t' ∈ transitions M1" and "t_source t' ∈ reachable_states M1" and "((V (t_source t')) @ [(t_input t',t_output t')]) ≠ (V (t_target t'))"
using snoc.prems(2)
unfolding unverified_transitions_alt_def
by auto
have "set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t'])))"
using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
by (metis eq_fst_iff)
then have "L M1 ∩ set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ set (fst (foldl verify_transition (T1, G1) ts))"
using snoc.prems(3)
by blast
have *: "L M1 ∩ Prefix_Tree.set (fst (verify_transition (foldl verify_transition (T1, G1) ts) t')) = L M2 ∩ Prefix_Tree.set (fst (verify_transition (foldl verify_transition (T1, G1) ts) t'))"
using snoc.prems(3) by auto
have "L M1 ∩ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))"
using ‹set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t'])))› snoc.prems(3)
by auto
then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) ts)) ∧ Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))"
using snoc.prems(2) verify_transition_foldl_invar_1[of ts] verify_transition_foldl_invar_2[of ts]
by auto
then have covers_t': "covers_unverified_transition t' (verify_transition (fst (foldl verify_transition (T1, G1) ts), snd (foldl verify_transition (T1, G1) ts)) t')"
using verify_transition_cover_prop[OF _ _ ‹t' ∈ transitions M1› ‹t_source t' ∈ reachable_states M1› ‹((V (t_source t')) @ [(t_input t',t_output t')]) ≠ (V (t_target t'))›, of "(fst (foldl verify_transition (T1, G1) ts))" "(snd (foldl verify_transition (T1, G1) ts))" ]
unfolding prod.collapse
using *
by auto
then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (verify_transition (fst (foldl verify_transition (T1, G1) ts), snd (foldl verify_transition (T1, G1) ts)) t'))"
unfolding covers_unverified_transition
by force
then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) (ts@[t'])))"
by auto
show ?case proof (cases "t = t'")
case True
then show ?thesis
using covers_t' by auto
next
case False
then have "t ∈ list.set ts"
using snoc.prems(1) by auto
have "list.set ts ⊆ list.set (unverified_transitions)"
using snoc.prems(2) by auto
have "covers_unverified_transition t (foldl verify_transition (T1, G1) ts)"
using snoc.IH[OF ‹t ∈ list.set ts›] snoc.prems(2) ‹L M1 ∩ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts)) = L M2 ∩ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))›
by auto
then have "covers_unverified_transition t (fst (foldl verify_transition (T1, G1) ts), snd (foldl verify_transition (T1, G1) ts))"
by auto
then have "(∃α β. converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
converge M1 β (V (t_target t)) ∧
converge M2 β (V (t_target t)) ∧ α @ [(t_input t, t_output t)] ∈ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts)) ∧ β ∈ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) ts))) ∧
converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))"
unfolding covers_unverified_transition
by blast
moreover have "set (fst (foldl verify_transition (T1, G1) ts)) ⊆ set (fst (foldl verify_transition (T1, G1) (ts@[t'])))"
using verify_transition_retains_testsuite[of "(fst (foldl verify_transition (T1, G1) ts))" "(snd (foldl verify_transition (T1, G1) ts))"]
unfolding prod.collapse
by auto
ultimately have "(∃α β.
converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
converge M1 β (V (t_target t)) ∧
converge M2 β (V (t_target t)) ∧ α @ [(t_input t, t_output t)] ∈ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) (ts@[t']))) ∧ β ∈ Prefix_Tree.set (fst (foldl verify_transition (T1, G1) (ts@[t'])))) ∧
converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))"
by blast
then have "covers_unverified_transition t (fst (foldl verify_transition (T1, G1) (ts@[t'])), snd (foldl verify_transition (T1, G1) (ts@[t'])))"
unfolding covers_unverified_transition
using ‹convergence_graph_lookup_invar M1 M2 cg_lookup (snd (foldl verify_transition (T1, G1) (ts@[t'])))›
by blast
then show ?thesis
by auto
qed
qed
qed
then show "⋀ t . L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ t ∈ list.set unverified_transitions ⟹ covers_unverified_transition t (T2,G2)"
unfolding TG2 T2 G2 ‹TG1 = (T1,G1)›
by simp
qed
have verify_undefined_io_pair_retains_testsuite: "⋀ qxy T . set T ⊆ set (verify_undefined_io_pair T qxy)"
proof -
fix qxy :: "('a × 'b × 'c)"
fix T
obtain q x y where "qxy = (q,x,y)"
using prod.exhaust by metis
show ‹set T ⊆ set (verify_undefined_io_pair T qxy)›
unfolding ‹qxy = (q,x,y)›
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup›
unfolding verifies_io_pair_def verify_undefined_io_pair case_prod_conv
by blast
qed
have verify_undefined_io_pair_folding_retains_testsuite: "⋀ qxys T . set T ⊆ set (foldl verify_undefined_io_pair T qxys)"
proof -
fix qxys T
show "set T ⊆ set (foldl verify_undefined_io_pair T qxys)"
using verify_undefined_io_pair_retains_testsuite
by (induction qxys rule: rev_induct; force)
qed
have verify_undefined_io_pair_retains_finiteness: "⋀ qxy T . finite_tree T ⟹ finite_tree (verify_undefined_io_pair T qxy)"
proof -
fix qxy :: "('a × 'b × 'c)"
fix T :: "('b×'c) prefix_tree"
assume "finite_tree T"
obtain q x y where "qxy = (q,x,y)"
using prod.exhaust by metis
show ‹finite_tree (verify_undefined_io_pair T qxy)›
unfolding ‹qxy = (q,x,y)›
using ‹verifies_io_pair append_io_pair M1 M2 cg_insert cg_lookup› ‹finite_tree T›
unfolding verifies_io_pair_def verify_undefined_io_pair case_prod_conv
by blast
qed
have verify_undefined_io_pair_folding_retains_finiteness: "⋀ qxys T . finite_tree T ⟹ finite_tree (foldl verify_undefined_io_pair T qxys)"
proof -
fix qxys
fix T :: "('b×'c) prefix_tree"
assume "finite_tree T"
then show "finite_tree (foldl verify_undefined_io_pair T qxys)"
using verify_undefined_io_pair_retains_finiteness
by (induction qxys rule: rev_induct; force)
qed
have "set T2 ⊆ set T3"
unfolding T3 T2
proof (induction undefined_io_pairs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
then show ?case
using verify_undefined_io_pair_retains_testsuite[of "(foldl verify_undefined_io_pair (fst TG2) xs)" x]
by force
qed
then have passes_T2: "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T2 = L M2 ∩ set T2"
using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (L M1 ∩ set T3 = L M2 ∩ set T3)›
by blast
have "set T1 ⊆ set T3"
and G2_invar: "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G2"
using T2_invar_1 T2_invar_2[OF passes_T2] ‹set T2 ⊆ set T3›
by auto
then have passes_T1: "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T1 = L M2 ∩ set T1"
using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3›
by blast
have T3_preserves_divergence : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ preserves_divergence M1 M2 (V ` reachable_states M1)"
using T1_V_div[OF passes_T1] .
have T3_state_cover : "V ` reachable_states M1 ⊆ set T3"
using T1_state_cover ‹set T1 ⊆ set T3›
by blast
have T3_covers_transitions : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ t . t ∈ transitions M1 ⟹ t_source t ∈ reachable_states M1 ⟹
(∃α β.
converge M1 α (V (t_source t)) ∧
converge M2 α (V (t_source t)) ∧
converge M1 β (V (t_target t)) ∧
converge M2 β (V (t_target t)) ∧
α @ [(t_input t, t_output t)] ∈ set T3 ∧
β ∈ set T3)
∧ converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)))"
(is "((L M1 ∩ set ?TS') = (L M2 ∩ set ?TS')) ⟹ (⋀ t . t ∈ transitions M1 ⟹ t_source t ∈ reachable_states M1 ⟹ ?P1 t T3 ∧ ?P2 t)")
proof -
fix t assume "t ∈ transitions M1" and "t_source t ∈ reachable_states M1" and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
then consider "t ∈ sc_covered_transitions" | "t ∈ list.set unverified_transitions"
unfolding sc_covered_transitions_alt_def unverified_transitions_alt_def
by blast
then show "?P1 t T3 ∧ ?P2 t"
proof cases
case 1
have "(V (t_source t)) ∈ L M1"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹t_source t ∈ reachable_states M1›]
by auto
then have p3: "converge M1 (V (t_source t)) (V (t_source t))"
by auto
have "(V (t_source t)) ∈ L M2"
using passes_T1[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] T1_state_cover ‹t_source t ∈ reachable_states M1› ‹(V (t_source t)) ∈ L M1›
by (metis IntI image_subset_iff inf.cobounded1 subsetD)
then have p4: "converge M2 (V (t_source t)) (V (t_source t))"
by auto
have "t_target t ∈ reachable_states M1"
using reachable_states_next[OF ‹t_source t ∈ reachable_states M1› ‹t ∈ transitions M1›]
by auto
then have "(V (t_target t)) ∈ L M1"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ]
by auto
then have p5: "converge M1 (V (t_target t)) (V (t_target t))"
by auto
have "(V (t_target t)) ∈ L M2"
using passes_T1[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] T1_state_cover ‹t_target t ∈ reachable_states M1› ‹(V (t_target t)) ∈ L M1›
by blast
then have p6: "converge M2 (V (t_target t)) (V (t_target t))"
by auto
have p8: "(V (t_target t)) ∈ set T3"
using T3_state_cover ‹t_target t ∈ reachable_states M1›
by auto
then have p7: "(V (t_source t)) @ [(t_input t, t_output t)] ∈ set T3"
using 1
unfolding sc_covered_transitions_alt_def
by auto
have "?P2 t"
using T1_covered_transitions_conv[OF passes_T1[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] 1]
by auto
then show ?thesis
using p3 p4 p5 p6 p7 p8
by blast
next
case 2
show ?thesis
using T2_cover[OF passes_T2[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] 2] ‹set T2 ⊆ set T3›
unfolding covers_unverified_transition
by blast
qed
qed
have T3_covers_defined_io_pairs : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ q x y q' . q ∈ reachable_states M1 ⟹ h_obs M1 q x y = Some q' ⟹
(∃α β.
converge M1 α (V q) ∧
converge M2 α (V q) ∧
converge M1 β (V q') ∧
converge M2 β (V q') ∧
α @ [(x,y)] ∈ set T3 ∧
β ∈ set T3)
∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q'))"
(is "((L M1 ∩ set ?TS') = (L M2 ∩ set ?TS')) ⟹ (⋀ q x y q' . q ∈ reachable_states M1 ⟹ h_obs M1 q x y = Some q' ⟹ ?P q x y q')")
proof -
fix q x y q' assume "q ∈ reachable_states M1" and "h_obs M1 q x y = Some q'" and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
then have "(q,x,y,q') ∈ transitions M1" and "t_source (q,x,y,q') ∈ reachable_states M1"
using h_obs_Some[OF assms(1)] by auto
moreover have "converge M1 (V q @ [(x,y)]) (V q')"
using state_cover_transition_converges[OF assms(1) ‹is_state_cover_assignment M1 V› calculation]
by auto
ultimately show "?P q x y q'"
using T3_covers_transitions[of "(q,x,y,q')", OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›]
unfolding fst_conv snd_conv
by blast
qed
have rstates_io_set : "list.set rstates_io = {(q,(x,y)) . q ∈ reachable_states M1 ∧ x ∈ inputs M1 ∧ y ∈ outputs M1}"
unfolding rstates_io rstates
using reachable_states_as_list_set[of M1] inputs_as_list_set[of M1] outputs_as_list_set[of M1]
by force
then have undefined_io_pairs_set : "list.set undefined_io_pairs = {(q,(x,y)) . q ∈ reachable_states M1 ∧ x ∈ inputs M1 ∧ y ∈ outputs M1 ∧ h_obs M1 q x y = None}"
unfolding undefined_io_pairs
by auto
have verify_undefined_io_pair_prop : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ q x y T . L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y))) ⟹
q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹
V ` reachable_states M1 ⊆ set T ⟹
∃ α. converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set (verify_undefined_io_pair T (q,(x,y))) ∧
α@[(x,y)] ∈ set (verify_undefined_io_pair T (q,(x,y))))"
proof -
fix q x y T
assume "L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y)))"
and "q ∈ reachable_states M1" and "x ∈ inputs M1" and "y ∈ outputs M1"
and "V ` reachable_states M1 ⊆ set T"
and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
have " L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
using T3_state_cover ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ Prefix_Tree.set T3 = L M2 ∩ Prefix_Tree.set T3› ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›
by blast
have "L M1 ∩ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y))"
using ‹L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y)))›
unfolding verify_undefined_io_pair case_prod_conv combine_set G2
by blast
have "(∃α. converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y)) ∧
α @ [(x, y)] ∈ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y)))"
using assms(16)
unfolding verifies_io_pair_def
using assms(1-4,7,8) ‹is_state_cover_assignment M1 V› ‹L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1›
‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›
G2_invar[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] ‹convergence_graph_insert_invar M1 M2 cg_lookup cg_insert›
‹L M1 ∩ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (append_io_pair M1 V T G2 cg_insert cg_lookup q x y))›
by blast
then show "∃ α. converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set (verify_undefined_io_pair T (q,(x,y))) ∧
α@[(x,y)] ∈ set (verify_undefined_io_pair T (q,(x,y)))"
unfolding verify_undefined_io_pair G2 case_prod_conv combine_set
by blast
qed
have T3_covers_undefined_io_pairs : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹
(∃ α .
converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set T3∧
α@[(x,y)] ∈ set T3))"
proof -
fix q x y assume "q ∈ reachable_states M1" and "x ∈ inputs M1" and "y ∈ outputs M1" and "h_obs M1 q x y = None" and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
have "⋀ q x y qxys T . L M1 ∩ set (foldl verify_undefined_io_pair T qxys) = L M2 ∩ set (foldl verify_undefined_io_pair T qxys) ⟹ (V ` reachable_states M1) ⊆ set T ⟹ (q,(x,y)) ∈ list.set qxys ⟹ list.set qxys ⊆ list.set undefined_io_pairs ⟹
(∃ α .
converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set (foldl verify_undefined_io_pair T qxys)∧
α@[(x,y)] ∈ set (foldl verify_undefined_io_pair T qxys))"
(is "⋀ q x y qxys T . ?P1 qxys T ⟹ (V ` reachable_states M1) ⊆ set T ⟹ (q,(x,y)) ∈ list.set qxys ⟹ list.set qxys ⊆ list.set undefined_io_pairs ⟹ ?P2 q x y qxys T")
proof -
fix q x y qxys T
assume "?P1 qxys T" and "(q,(x,y)) ∈ list.set qxys" and "list.set qxys ⊆ list.set undefined_io_pairs" and "(V ` reachable_states M1) ⊆ set T"
then show "?P2 q x y qxys T"
proof (induction qxys rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc a qxys)
have "set (foldl verify_undefined_io_pair T qxys) ⊆ set (foldl verify_undefined_io_pair T (qxys@[a]))"
using verify_undefined_io_pair_retains_testsuite
by auto
then have *:"L M1 ∩ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys) = L M2 ∩ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
using snoc.prems(1)
by blast
have **: "V ` reachable_states M1 ⊆ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
using snoc.prems(4) verify_undefined_io_pair_folding_retains_testsuite
by blast
show ?case proof (cases "a = (q,(x,y))")
case True
then have ***: "q ∈ reachable_states M1"
using snoc.prems(3)
unfolding undefined_io_pairs_set
by auto
have "x ∈ inputs M1" and "y ∈ outputs M1"
using snoc.prems(2,3) unfolding undefined_io_pairs_set by auto
have ****: "L M1 ∩ set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y)))"
using snoc.prems(1) unfolding True by auto
show ?thesis
using verify_undefined_io_pair_prop[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› **** *** ‹x ∈ inputs M1› ‹y ∈ outputs M1› **]
unfolding True
by auto
next
case False
then have "(q, x, y) ∈ list.set qxys" and "list.set qxys ⊆ list.set undefined_io_pairs"
using snoc.prems(2,3) by auto
then show ?thesis
using snoc.IH[OF * _ _ snoc.prems(4)]
using ‹set (foldl verify_undefined_io_pair T qxys) ⊆ set (foldl verify_undefined_io_pair T (qxys@[a]))›
by blast
qed
qed
qed
moreover have "L M1 ∩ set (foldl verify_undefined_io_pair T2 undefined_io_pairs) = L M2 ∩ set (foldl verify_undefined_io_pair T2 undefined_io_pairs)"
using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3› ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›
unfolding T3 T2 .
moreover have "(V ` reachable_states M1) ⊆ set T2"
using T1_state_cover T2 T2_invar_1 passes_T2 by fastforce
moreover have "(q,(x,y)) ∈ list.set undefined_io_pairs"
unfolding undefined_io_pairs_set
using ‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1› ‹h_obs M1 q x y = None›
by blast
ultimately show "(∃ α .
converge M1 α (V q) ∧
converge M2 α (V q) ∧
α ∈ set T3∧
α@[(x,y)] ∈ set T3)"
unfolding T3 T2
by blast
qed
define TCfun where TCfun: "TCfun = (λ (q,(x,y)) . case h_obs M1 q x y of
None ⇒ {{α, α@[(x,y)]} | α . converge M1 α (V q) ∧ converge M2 α (V q) ∧ α ∈ set T3 ∧ α@[(x,y)] ∈ set T3} |
Some q' ⇒ {{α,α@[(x,y)], β} | α β . converge M1 α (V q) ∧ converge M2 α (V q) ∧ converge M1 β (V q') ∧ converge M2 β (V q') ∧ α @ [(x,y)] ∈ set T3 ∧ β ∈ set T3 ∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q')})"
define TC where TC: "TC = Set.insert [] (⋃(⋃ (TCfun ` (reachable_states M1 × (inputs M1 × outputs M1)))))"
have TCfun_nonempty: "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ TCfun (q,(x,y)) ≠ {})"
proof -
fix q x y assume *:"q ∈ reachable_states M1" and **:"x ∈ inputs M1" and ***:"y ∈ outputs M1" and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
show "TCfun (q,(x,y)) ≠ {}"
proof (cases "h_obs M1 q x y")
case None
then have "TCfun (q,(x,y)) = {{α, α @ [(x, y)]} |α. converge M1 α (V q) ∧ converge M2 α (V q) ∧ α ∈ set T3 ∧ α @ [(x, y)] ∈ set T3}"
unfolding TCfun by auto
moreover have "{{α, α @ [(x, y)]} |α. converge M1 α (V q) ∧ converge M2 α (V q) ∧ α ∈ set T3 ∧ α @ [(x, y)] ∈ set T3} ≠ {}"
using T3_covers_undefined_io_pairs[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› * ** *** None]
by blast
ultimately show ?thesis
by blast
next
case (Some q')
then have "TCfun (q,(x,y)) = {{α,α@[(x,y)], β} | α β . converge M1 α (V q) ∧ converge M2 α (V q) ∧ converge M1 β (V q') ∧ converge M2 β (V q') ∧ α @ [(x,y)] ∈ set T3 ∧ β ∈ set T3 ∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q')}"
using TCfun by auto
moreover have "{{α,α@[(x,y)], β} | α β . converge M1 α (V q) ∧ converge M2 α (V q) ∧ converge M1 β (V q') ∧ converge M2 β (V q') ∧ α @ [(x,y)] ∈ set T3 ∧ β ∈ set T3 ∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q')} ≠ {}"
using T3_covers_defined_io_pairs[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› * Some]
by blast
ultimately show ?thesis
by blast
qed
qed
have TC_in_T3: "TC ⊆ set T3"
proof
fix α assume "α ∈ TC"
show "α ∈ set T3"
proof (cases "α = []")
case True
then show ?thesis
using T3_state_cover ‹is_state_cover_assignment M1 V› reachable_states_initial[of M1]
by auto
next
case False
then obtain q x y where "q ∈ reachable_states M1"
and "x ∈ inputs M1"
and "y ∈ outputs M1"
and "α ∈ ⋃ (TCfun (q,(x,y)))"
using ‹α ∈ TC› unfolding TC
by auto
show "α ∈ set T3"
using ‹α ∈ ⋃ (TCfun (q,(x,y)))› set_prefix[of "α" "[(x,y)]" T3] unfolding TCfun
by (cases "h_obs M1 q x y";auto)
qed
qed
have TC_is_transition_cover : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ transition_cover M1 TC"
proof -
assume "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
have "⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ ∃α. α ∈ TC ∧ α @ [(x, y)] ∈ TC ∧ α ∈ L M1 ∧ after_initial M1 α = q"
proof -
fix q x y assume "q ∈ reachable_states M1"
and "x ∈ inputs M1"
and "y ∈ outputs M1"
then have "(q,(x,y)) ∈ (reachable_states M1 × FSM.inputs M1 × FSM.outputs M1)"
by blast
show "∃α. α ∈ TC ∧ α @ [(x, y)] ∈ TC ∧ α ∈ L M1 ∧ after_initial M1 α = q"
proof (cases "h_obs M1 q x y")
case None
then have "TCfun (q,(x,y)) = {{α, α @ [(x, y)]} |α. converge M1 α (V q) ∧ converge M2 α (V q) ∧ α ∈ set T3 ∧ α @ [(x, y)] ∈ set T3}"
unfolding TCfun by auto
then obtain α where "converge M1 α (V q)" and "α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y)))"
using TCfun_nonempty[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› ‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›]
by auto
then have "after_initial M1 α = q"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹q ∈ reachable_states M1›]
using convergence_minimal[OF assms(3,1)]
by (metis converge.elims(2))
then have "∃α. α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y))) ∧ α ∈ L M1 ∧ after_initial M1 α = q"
using ‹α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y)))›
using ‹converge M1 α (V q)› converge.elims(2) by blast
moreover have "⋃ (TCfun (q,(x,y))) ⊆ TC"
unfolding TC using ‹(q,(x,y)) ∈ (reachable_states M1 × FSM.inputs M1 × FSM.outputs M1)›
by blast
ultimately show ?thesis
by blast
next
case (Some q')
then have "TCfun (q,(x,y)) = {{α,α@[(x,y)], β} | α β . converge M1 α (V q) ∧ converge M2 α (V q) ∧ converge M1 β (V q') ∧ converge M2 β (V q') ∧ α @ [(x,y)] ∈ set T3 ∧ β ∈ set T3 ∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q')}"
using TCfun
by auto
moreover obtain S where "S ∈ TCfun (q,(x,y))"
using TCfun_nonempty[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› ‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›]
by blast
ultimately obtain α where "converge M1 α (V q)" and "α ∈ S ∧ α @ [(x, y)] ∈ S"
by auto
then have "after_initial M1 α = q"
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹q ∈ reachable_states M1›]
using convergence_minimal[OF assms(3,1)]
by (metis converge.elims(2))
moreover have "α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y)))"
using ‹α ∈ S ∧ α @ [(x, y)] ∈ S› ‹S ∈ TCfun (q,(x,y))›
by auto
ultimately have "∃α. α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y))) ∧ α ∈ L M1 ∧ after_initial M1 α = q"
using ‹α ∈ ⋃ (TCfun (q,(x,y))) ∧ α @ [(x, y)] ∈ ⋃ (TCfun (q,(x,y)))›
using ‹converge M1 α (V q)› converge.elims(2) by blast
moreover have "⋃ (TCfun (q,(x,y))) ⊆ TC"
unfolding TC using ‹(q,(x,y)) ∈ (reachable_states M1 × FSM.inputs M1 × FSM.outputs M1)›
by blast
ultimately show ?thesis
by blast
qed
qed
then show ?thesis
unfolding transition_cover_def
by blast
qed
have TC_preserves_convergence: "preserves_convergence M1 M2 TC"
proof -
have "⋀ α β . α ∈ L M1 ∩ TC ⟹ β ∈ L M1 ∩ TC ⟹ converge M1 α β ⟹ converge M2 α β"
proof -
fix α β assume "α ∈ L M1 ∩ TC"
"β ∈ L M1 ∩ TC"
"converge M1 α β"
have *: "⋀ α . α ∈ L M1 ⟹ α ∈ TC ⟹ ∃ q . q ∈ reachable_states M1 ∧ converge M1 α (V q) ∧ converge M2 α (V q)"
proof -
fix α assume "α ∈ L M1" and "α ∈ TC"
show "∃ q . q ∈ reachable_states M1 ∧ converge M1 α (V q) ∧ converge M2 α (V q)"
proof (cases "α = []")
case True
then have "V (initial M1) = α"
using ‹is_state_cover_assignment M1 V› reachable_states_initial[of M1]
by auto
then have "converge M1 α (V (initial M1))" and "converge M2 α (V (initial M1))"
unfolding True by auto
then show ?thesis
using reachable_states_initial[of M1]
by auto
next
case False
then have "α ∈ (⋃(⋃ (TCfun ` (reachable_states M1 × (inputs M1 × outputs M1)))))"
using ‹α ∈ TC›
unfolding TC
by blast
then obtain q x y where "q ∈ reachable_states M1"
and "x ∈ inputs M1"
and "y ∈ outputs M1"
and "α ∈ ⋃ (TCfun (q,(x,y)))"
unfolding TC by auto
show "∃ q . q ∈ reachable_states M1 ∧ converge M1 α (V q) ∧ converge M2 α (V q)"
proof (cases "h_obs M1 q x y")
case None
then have "TCfun (q,(x,y)) = {{α, α @ [(x, y)]} |α. converge M1 α (V q) ∧ converge M2 α (V q) ∧ α ∈ set T3 ∧ α @ [(x, y)] ∈ set T3}"
unfolding TCfun by auto
then obtain α' where "α ∈ {α', α' @ [(x, y)]}"
and "converge M1 α' (V q)"
and "converge M2 α' (V q)"
using ‹α ∈ ⋃ (TCfun (q,(x,y)))›
by auto
have "[(x,y)] ∉ LS M1 q"
using None unfolding h_obs_None[OF assms(1)] LS_single_transition
by auto
moreover have "after_initial M1 α' = q"
using ‹converge M1 α' (V q)›
using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹q ∈ reachable_states M1›]
using convergence_minimal[OF assms(3,1) _ _]
by (metis converge.elims(2))
ultimately have "α' @ [(x, y)] ∉ L M1"
using after_language_iff[OF assms(1), of α' "initial M1" "[(x,y)]"] ‹converge M1 α' (V q)›
by (meson converge.elims(2))
then have "α' = α"
using ‹α ∈ {α', α' @ [(x, y)]}› ‹α ∈ L M1›
by blast
then show ?thesis
using ‹q ∈ reachable_states M1› ‹converge M1 α' (V q)› ‹converge M2 α' (V q)›
by blast
next
case (Some q')
then have "q' ∈ reachable_states M1"
unfolding h_obs_Some[OF assms(1)]
using reachable_states_next[OF ‹q ∈ reachable_states M1›, of "(q,x,y,q')"]
by auto
have "TCfun (q,(x,y)) = {{α,α@[(x,y)], β} | α β . converge M1 α (V q) ∧ converge M2 α (V q) ∧ converge M1 β (V q') ∧ converge M2 β (V q') ∧ α @ [(x,y)] ∈ set T3 ∧ β ∈ set T3 ∧ converge M1 (V q @ [(x,y)]) (V q') ∧ converge M2 (V q @ [(x,y)]) (V q')}"
using Some TCfun
by auto
then obtain α' β where "α ∈ {α',α'@[(x,y)], β}"
and "converge M1 α' (V q)"
and "converge M2 α' (V q)"
and "converge M1 β (V q')"
and "converge M2 β (V q')"
and "converge M1 (V q @ [(x,y)]) (V q')"
and "converge M2 (V q @ [(x,y)]) (V q')"
using ‹α ∈ ⋃ (TCfun (q,(x,y)))›
by auto
then consider "α = α'" | "α = α'@[(x,y)]" | "α = β"
by blast
then show ?thesis proof cases
case 1
then show ?thesis
using ‹q ∈ reachable_states M1› ‹converge M1 α' (V q)› ‹converge M2 α' (V q)›
by blast
next
case 2
have "converge M1 (α'@[(x,y)]) (V q @ [(x,y)])"
using ‹converge M1 α' (V q)› ‹converge M1 (V q @ [(x,y)]) (V q')›
using converge_append[OF assms(1), of "V q" α' "[(x,y)]"]
by auto
then have "converge M1 (α'@[(x,y)]) (V q')"
using ‹converge M1 β (V q')› ‹converge M1 (V q @ [(x,y)]) (V q')›
by auto
have "converge M2 (α'@[(x,y)]) (V q @ [(x,y)])"
using ‹converge M2 α' (V q)› ‹converge M2 (V q @ [(x,y)]) (V q')›
using converge_append[OF assms(2), of "V q" α' "[(x,y)]"]
by auto
then have "converge M2 (α'@[(x,y)]) (V q')"
using ‹converge M2 β (V q')› ‹converge M2 (V q @ [(x,y)]) (V q')›
by auto
show ?thesis
using 2 ‹q' ∈ reachable_states M1› ‹converge M1 (α'@[(x,y)]) (V q')› ‹converge M2 (α'@[(x,y)]) (V q')›
by auto
next
case 3
then show ?thesis
using ‹converge M1 β (V q')› ‹converge M2 β (V q')› ‹q' ∈ reachable_states M1›
by blast
qed
qed
qed
qed
obtain q where "q ∈ reachable_states M1" and "converge M1 α (V q)" and "converge M2 α (V q)"
using * ‹α ∈ L M1 ∩ TC›
by blast
obtain q' where "q' ∈ reachable_states M1" and "converge M1 β (V q')" and "converge M2 β (V q')"
using * ‹β ∈ L M1 ∩ TC›
by blast
have "converge M1 (V q) (V q')"
using ‹converge M1 α (V q)› ‹converge M1 β (V q')› ‹converge M1 α β›
by auto
then have "q = q'"
using convergence_minimal[OF assms(3,1), of "V q" "V q'"]
unfolding state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹q ∈ reachable_states M1›]
state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V› ‹q' ∈ reachable_states M1›]
by auto
then have "V q = V q'"
by auto
then show "converge M2 α β"
using ‹converge M2 α (V q)› ‹converge M2 β (V q')›
by auto
qed
then show ?thesis
unfolding preserves_convergence.simps
by blast
qed
have "[] ∈ TC"
unfolding TC by blast
show "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 = L M2"
using initialised_convergence_preserving_transition_cover_is_complete[OF assms(1-4,7,8)
‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3›
TC_in_T3
TC_is_transition_cover
‹[] ∈ TC›
TC_preserves_convergence]
by assumption
show "finite_tree ?TS"
using T2 T2_finite T3 verify_undefined_io_pair_folding_retains_finiteness
by (simp add: ‹?TS = T3›)
qed
end