# Theory Test_Suite_Calculation_Refined

```section ‹Refined Test Suite Calculation›

text ‹This theory refines some of the algorithms defined in @{text "Test_Suite_Calculation"}
using containers from the Containers framework.›

theory Test_Suite_Calculation_Refined
imports Test_Suite_Calculation
"../Util_Refined"
Deriving.Compare
Containers.Containers
begin

subsection ‹New Instances›

subsubsection ‹Order on FSMs›

instantiation fsm :: (ord,ord,ord) ord
begin

fun less_eq_fsm ::  "('a,'b,'c) fsm ⇒ ('a,'b,'c) fsm ⇒ bool" where
"less_eq_fsm M1 M2 =
(if initial M1 < initial M2
then True
else ((initial M1 = initial M2) ∧ (if set_less_aux (states M1)  (states M2)
then True
else ((states M1 = states M2) ∧ (if set_less_aux (inputs M1) (inputs M2)
then True
else ((inputs M1 = inputs M2) ∧ (if set_less_aux (outputs M1) (outputs M2)
then True
else ((outputs M1 = outputs M2) ∧ (set_less_aux (transitions M1) (transitions M2) ∨ (transitions M1) = (transitions M2))))))))))"

fun less_fsm ::  "('a,'b,'c) fsm ⇒ ('a,'b,'c) fsm ⇒ bool" where
"less_fsm a b = (a ≤ b ∧ a ≠ b)"

instance by (intro_classes)
end

instantiation fsm :: (linorder,linorder,linorder) linorder
begin

lemma less_le_not_le_FSM :
fixes x :: "('a,'b,'c) fsm"
and   y :: "('a,'b,'c) fsm"
shows "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
proof
show "x < y ⟹ x ≤ y ∧ ¬ y ≤ x"

proof -
assume "x < y"
then show "x ≤ y ∧ ¬ y ≤ x"
proof (cases "FSM.initial x < FSM.initial y")
case True
then show ?thesis unfolding less_fsm.simps less_eq_fsm.simps by auto
next
case False
then have *: "FSM.initial x = FSM.initial y"
using ‹x < y› unfolding less_fsm.simps less_eq_fsm.simps by auto

show ?thesis proof (cases "set_less_aux (FSM.states x) (FSM.states y)")
case True
then show ?thesis
unfolding less_fsm.simps less_eq_fsm.simps
using * set_less_aux_antisym by fastforce
next
case False
then have **: "FSM.states x = FSM.states y"
using ‹x < y› * unfolding less_fsm.simps less_eq_fsm.simps by auto

show ?thesis proof (cases "set_less_aux (FSM.inputs x) (FSM.inputs y)")
case True
then show ?thesis
unfolding less_fsm.simps less_eq_fsm.simps
using * ** set_less_aux_antisym by fastforce
next
case False
then have ***: "FSM.inputs x = FSM.inputs y"
using ‹x < y› * **
unfolding less_fsm.simps less_eq_fsm.simps

show ?thesis proof (cases "set_less_aux (FSM.outputs x) (FSM.outputs y)")
case True
then show ?thesis
unfolding less_fsm.simps less_eq_fsm.simps
using * ** *** set_less_aux_antisym
by fastforce
next
case False
then have ****: "FSM.outputs x = FSM.outputs y"
using ‹x < y› * ** ***
unfolding less_fsm.simps less_eq_fsm.simps

have "x ≠ y" using ‹x < y› by auto
then have "FSM.transitions x ≠ FSM.transitions y"
using * ** *** **** apply transfer
by (metis fsm_impl.exhaust_sel)
then have *****: "set_less_aux (FSM.transitions x) (FSM.transitions y)"
using ‹x < y› * ** *** ****
unfolding less_fsm.simps less_eq_fsm.simps

then have "¬(set_less_aux (FSM.transitions y) (FSM.transitions x) ∨ transitions y = transitions x)"
using ‹FSM.transitions x ≠ FSM.transitions y› fsm_transitions_finite set_less_aux_antisym
by auto
then have "¬ y ≤ x"
using * ** *** ****
unfolding less_fsm.simps less_eq_fsm.simps
then show ?thesis using ‹x < y›
using less_fsm.elims(2)
by blast
qed
qed
qed
qed
qed

show "x ≤ y ∧ ¬ y ≤ x ⟹ x < y"
using less_fsm.elims(3)
by blast
qed

lemma order_refl_FSM :
fixes x :: "('a,'b,'c) fsm"
shows "x ≤ x"
by auto

lemma order_trans_FSM :
fixes x :: "('a,'b,'c) fsm"
fixes y :: "('a,'b,'c) fsm"
fixes z :: "('a,'b,'c) fsm"
shows "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
unfolding less_eq_fsm.simps
using less_trans[of "initial x" "initial y" "initial z"]
set_less_aux_trans[of "states x" "states y" "states z"]
set_less_aux_trans[of "inputs x" "inputs y" "inputs z"]
set_less_aux_trans[of "outputs x" "outputs y" "outputs z"]
set_less_aux_trans[of "transitions x" "transitions y" "transitions z"]
by metis

lemma antisym_FSM :
fixes x :: "('a,'b,'c) fsm"
fixes y :: "('a,'b,'c) fsm"
shows "x ≤ y ⟹ y ≤ x ⟹ x = y"
unfolding less_eq_fsm.simps
using equal_fsm_def[of x y]
unfolding equal_class.equal
by (metis order.asym set_less_aux_antisym)

lemma linear_FSM :
fixes x :: "('a,'b,'c) fsm"
fixes y :: "('a,'b,'c) fsm"
shows "x ≤ y ∨ y ≤ x"
unfolding less_eq_fsm.simps
by (metis fsm_inputs_finite fsm_states_finite fsm_outputs_finite fsm_transitions_finite neq_iff set_less_aux_finite_total)

instance
using less_le_not_le_FSM order_refl_FSM order_trans_FSM antisym_FSM linear_FSM
by (intro_classes; metis+)
end

instantiation fsm :: (linorder,linorder,linorder) compare
begin
fun compare_fsm :: "('a, 'b, 'c) fsm ⇒ ('a, 'b, 'c) fsm ⇒ order" where
"compare_fsm x y = comparator_of x y"

instance
using comparator_of compare_fsm.elims
end

(* The above order on FSMs is currently not used in code generation,
as there are few sets of FSMs and hence on evaluated examples it is
more efficient to simply store FSMs using d-lists.*)
(*
instantiation fsm :: (linorder,linorder,linorder) ccompare
begin
definition ccompare_fsm :: "(('a, 'b, 'c) fsm ⇒ ('a, 'b, 'c) fsm ⇒ order) option" where
"ccompare_fsm = Some compare"

instance by (intro_classes; simp add: ccompare_fsm_def comparator_compare)
end
*)

subsubsection ‹Derived Instances›

derive (eq) ceq fsm

derive (dlist) set_impl fsm
derive (assoclist) mapping_impl fsm

derive (no) cenum fsm
derive (no) ccompare fsm

subsubsection ‹Finiteness and Cardinality Instantiations for FSMs›

(*
text ‹The following type class partially encodes infinity of a type.
This is done because later instantiations assume the universe of FSMs to be infinite in
order to reduce the effort required to instantiate proper intervals over FSMs.
This class is not a good idea for any general usage, as many types (e.g. pairs) have
conflicting instantiations (see for example https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-July/msg00104.html).›
class infinite_UNIV =
assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
begin
end

instantiation integer :: infinite_UNIV begin
instance apply intro_classes
end

instantiation nat :: infinite_UNIV begin
instance apply intro_classes
end

instantiation int :: infinite_UNIV begin
instance apply intro_classes
end

(* too restrictive *)
instantiation sum :: (infinite_UNIV,type) infinite_UNIV begin
instance apply intro_classes
end

(* too restrictive *)
instantiation prod :: (infinite_UNIV,type) infinite_UNIV begin
instance apply intro_classes
end

lemma infinite_UNIV_fsm :
shows "infinite (UNIV :: ('a :: infinite_UNIV,'b,'c) fsm set)"
proof -
(* if infinitely many states exist, then infinitely many distinct singleton fsms can be created *)
define f :: "'a ⇒ ('a,'b,'c) fsm" where f_def: "f = (λ q . fsm_from_list q [])"
have "inj f"
proof
fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y"
then show "x = y" unfolding f_def by (transfer; auto)
qed
moreover have "infinite (UNIV :: 'a set)"
using infinite_UNIV by auto
ultimately show ?thesis
by (meson finite_imageD infinite_iff_countable_subset top_greatest)
qed
*)

lemma finiteness_fsm_UNIV : "finite (UNIV :: ('a,'b,'c) fsm set) =
(finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set))"
proof

define f :: "'a ⇒ ('a) fset" where f_def: "f = (λ q . {| q |})"
have "inj f"
proof
fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y"
then show "x = y" unfolding f_def by (transfer; auto)
qed

show "finite (UNIV :: ('a,'b,'c) fsm set) ⟹ (finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set))"
proof (rule ccontr)

obtain q where "q ∈ (UNIV :: 'a set)" by auto
obtain x where "x ∈ (UNIV :: 'b set)" by auto
obtain y where "y ∈ (UNIV :: 'c set)" by auto

assume "finite (UNIV :: ('a,'b,'c) fsm set)" and "¬ (finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set))"

then consider (a) "¬ finite (UNIV :: 'a set)" | (b) "¬ finite (UNIV :: 'b set)" | (c) "¬ finite (UNIV :: 'c set)"
by blast
then show "False" proof cases
case a
define f :: "'a ⇒ ('a,'b,'c) fsm" where "f = (λ q . fsm_from_list q [])"
have "inj f"
unfolding inj_def f_def by (transfer; auto)
then have "¬ finite (f ` UNIV)"
using ‹inj f› finite_imageD a by auto
then have "¬ finite (UNIV :: ('a,'b,'c) fsm set)"
by (meson infinite_iff_countable_subset top_greatest)
then show ?thesis
using ‹finite (UNIV :: ('a,'b,'c) fsm set)› by blast
next
case b
define f :: "'b ⇒ ('a,'b,'c) fsm" where "f = (λ x . fsm_from_list q [(q,x,y,q)])"
have "inj f"
unfolding inj_def f_def by (transfer; auto)
then have "¬ finite (f ` UNIV)"
using ‹inj f› finite_imageD b by auto
then have "¬ finite (UNIV :: ('a,'b,'c) fsm set)"
by (meson infinite_iff_countable_subset top_greatest)
then show ?thesis
using ‹finite (UNIV :: ('a,'b,'c) fsm set)› by blast
next
case c
define f :: "'c ⇒ ('a,'b,'c) fsm" where "f = (λ y . fsm_from_list q [(q,x,y,q)])"
have "inj f"
unfolding inj_def f_def by (transfer; auto)
then have "¬ finite (f ` UNIV)"
using ‹inj f› finite_imageD c by auto
then have "¬ finite (UNIV :: ('a,'b,'c) fsm set)"
by (meson infinite_iff_countable_subset top_greatest)
then show ?thesis
using ‹finite (UNIV :: ('a,'b,'c) fsm set)› by blast
qed
qed

show "(finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set)) ⟹ finite (UNIV :: ('a,'b,'c) fsm set)"
proof -
define f :: "('a,'b,'c) fsm ⇒ ('a × 'a set × 'b set × 'c set × ('a × 'b × 'c × 'a) set)" where
"f = (λ m . (initial m, states m, inputs m, outputs m, transitions m))"
assume "(finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set))"
then have "finite (UNIV :: ('a × 'a set × 'b set × 'c set × ('a × 'b × 'c × 'a) set) set)"
moreover have "f ` (UNIV :: ('a,'b,'c) fsm set) ⊆ (UNIV :: ('a × 'a set × 'b set × 'c set × ('a × 'b × 'c × 'a) set) set)"
by auto
moreover have "inj f"
unfolding inj_def f_def apply transfer
ultimately show ?thesis by (metis inj_on_finite)
qed
qed

instantiation fsm :: (finite_UNIV,finite_UNIV,finite_UNIV) finite_UNIV begin
definition "finite_UNIV = Phantom(('a,'b,'c) fsm) (of_phantom (finite_UNIV :: 'a finite_UNIV) ∧
of_phantom (finite_UNIV :: 'b finite_UNIV) ∧
of_phantom (finite_UNIV :: 'c finite_UNIV))"

instance by(intro_classes)(simp add: finite_UNIV_fsm_def finite_UNIV finiteness_fsm_UNIV)
end

instantiation fsm :: (card_UNIV,card_UNIV,card_UNIV) card_UNIV begin

definition "card_UNIV = Phantom(('a,'b,'c) fsm)
(if CARD('a) = 0 ∨ CARD('b) = 0 ∨ CARD('c) = 0
then 0
else card ((λ(q::'a, Q, X::'b set, Y::'c set, T). FSM.create_fsm_from_sets q Q X Y T) ` UNIV))"
instance apply intro_classes
proof (cases "CARD('a) = 0 ∨ CARD('b) = 0 ∨ CARD('c) = 0")
case True
then have "¬ (finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set) ∧ finite (UNIV :: 'c set))"
by force
then have "infinite (UNIV :: ('a, 'b, 'c) fsm set)"
using finiteness_fsm_UNIV by blast
then have "card (UNIV :: ('a, 'b, 'c) fsm set) = 0"
by auto
then show "card_UNIV_class.card_UNIV = Phantom(('a, 'b, 'c) fsm) CARD(('a, 'b, 'c) fsm)"
using True
next
case False
then have "finite (UNIV :: 'a set)" and "finite (UNIV :: 'b set)" and "finite (UNIV :: 'c set)"
by force+
then have "surj (λ(q::'a, Q, X::'b set, Y::'c set, T). FSM.create_fsm_from_sets q Q X Y T)"
using create_fsm_from_sets_surj by blast
then show "card_UNIV_class.card_UNIV = Phantom(('a, 'b, 'c) fsm) CARD(('a, 'b, 'c) fsm)"
using False
qed
end

instantiation fsm :: (type,type,type) cproper_interval begin
definition cproper_interval_fsm :: "(('a,'b,'c) fsm) proper_interval" where
"cproper_interval_fsm m1 m2 = undefined"
end

subsection ‹Updated Code Equations›

subsubsection ‹New Code Equations for @{text "remove_proper_prefixes"}›

declare [[code drop: remove_proper_prefixes]]

lemma remove_proper_prefixes_refined[code] :
fixes t :: "('a :: ccompare) list set_rbt"
shows "remove_proper_prefixes (RBT_set t) = (case ID CCOMPARE(('a list)) of
Some _ ⇒ (if (is_empty t) then {} else set (paths (from_list (RBT_Set2.keys t)))) |
None   ⇒ Code.abort (STR ''remove_proper_prefixes RBT_set: ccompare = None'') (λ_. remove_proper_prefixes (RBT_set t)))"
(is "?v1 = ?v2")
proof (cases "ID CCOMPARE(('a list))")
case None
then show ?thesis by simp
next
case (Some a)
then have *:"ID ccompare ≠ (None :: ('a::ccompare list ⇒ 'a::ccompare list ⇒ order) option)" by auto

show ?thesis proof (cases "is_empty t")
case True
then show ?thesis unfolding Some remove_proper_prefixes_def by auto
next
case False
then have "?v2 = set (paths (from_list (RBT_Set2.keys t)))" using Some by auto
moreover have "?v1 = set (paths (from_list (RBT_Set2.keys t)))"
using False unfolding RBT_set_conv_keys[OF *, of t] remove_proper_prefixes_code_trie
by (cases "RBT_Set2.keys t"; auto)
ultimately show ?thesis by simp
qed
qed

subsubsection ‹Special Handling for @{text "set_as_map"} on @{text "image"}›

text ‹Avoid creating an intermediate set for @{text "(image f xs)"} when evaluating @{text "(set_as_map (image f xs))"}.›

definition set_as_map_image :: "('a1 × 'a2) set ⇒ (('a1 × 'a2) ⇒ ('b1 × 'b2)) ⇒ ('b1 ⇒ 'b2 set option)" where
"set_as_map_image xs f = (set_as_map (image f xs))"

(* combine two separate set_as_map_image calls on the same set *)
definition dual_set_as_map_image :: "('a1 × 'a2) set ⇒ (('a1 × 'a2) ⇒ ('b1 × 'b2)) ⇒ (('a1 × 'a2) ⇒ ('c1 × 'c2)) ⇒ (('b1 ⇒ 'b2 set option) × ('c1 ⇒ 'c2 set option))" where
"dual_set_as_map_image xs f1 f2 = (set_as_map (image f1 xs), set_as_map (image f2 xs))"

lemma set_as_map_image_code[code]  :
fixes t :: "('a1 ::ccompare × 'a2 :: ccompare) set_rbt"
and   f1 :: "('a1 × 'a2) ⇒ ('b1 :: ccompare × 'b2 ::ccompare)"
shows "set_as_map_image (RBT_set t) f1 = (case ID CCOMPARE(('a1 × 'a2)) of
Some _ ⇒ Mapping.lookup
(RBT_Set2.fold (λ kv m1 .
( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
t
Mapping.empty) |
None   ⇒ Code.abort (STR ''set_as_map_image RBT_set: ccompare = None'')
(λ_. set_as_map_image (RBT_set t) f1))"
proof (cases "ID CCOMPARE(('a1 × 'a2))")
case None
then show ?thesis by auto
next
case (Some a)

let ?f' = "λ t . (RBT_Set2.fold (λ kv m1 .
( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
t
Mapping.empty)"

let ?f = "λ xs . (fold (λ kv m1 . case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1))
xs Mapping.empty)"
have "⋀ xs :: ('a1 × 'a2) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None)"
proof -
fix xs :: "('a1 × 'a2) list"
show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None)"
proof (induction xs rule: rev_induct)
case Nil
then show ?case
next
case (snoc xz xs)
then obtain x z where "f1  xz = (x,z)"
by (metis (mono_tags, opaque_lifting) surj_pair)

then have *: "(?f (xs@[xz])) = (case Mapping.lookup (?f xs) x of
None ⇒ Mapping.update x {z} (?f xs) |
Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
by auto

then show ?case proof (cases "Mapping.lookup (?f xs) x")
case None
then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto

have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = None"
using None snoc by auto
then have "¬(∃ z . (x,z) ∈ f1 ` set xs)"
by (metis (mono_tags, lifting) option.distinct(1))
then have "(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))" and "{z' . (x,z') ∈ f1 ` set (xs@[xz])} = {z}"
using ‹f1  xz = (x,z)› by fastforce+
then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None)
= (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x')"
using ‹f1  xz = (x,z)› by fastforce

show ?thesis using m1 m2 snoc
using ‹f1 xz = (x, z)› by presburger
next
case (Some zs)
then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = Some zs"
using Some snoc by auto
then have "(∃ z' . (x,z') ∈ f1 ` set xs)"
unfolding case_prod_conv using  option.distinct(2) by metis
then have "(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))" by fastforce

have "{z' . (x,z') ∈ f1 ` set (xs@[xz])} = Set.insert z zs"
proof -
have "Some {z . (x,z) ∈ f1 ` set xs} = Some zs"
using ‹(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = Some zs›
unfolding case_prod_conv using  option.distinct(2) by metis
then have "{z . (x,z) ∈ f1 ` set xs} = zs" by auto
then show ?thesis
using ‹f1 xz = (x, z)› by auto
qed

have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x') a"
proof -
fix a show "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x') a"
using ‹{z' . (x,z') ∈ f1 ` set (xs@[xz])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))› ‹f1 xz = (x, z)›
by (cases "a = x"; auto)
qed

then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None)
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x')"
by auto

show ?thesis using m1 m2 snoc
using ‹f1 xz = (x, z)› by presburger
qed
qed
qed

then have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ f1 ` set (RBT_Set2.keys t)) then Some {z . (x,z) ∈ f1 ` set (RBT_Set2.keys t)} else None)"
unfolding fold_conv_fold_keys by metis
moreover have "set (RBT_Set2.keys t) = (RBT_set t)"
using Some by (simp add: RBT_set_conv_keys)
ultimately have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ f1 ` (RBT_set t)) then Some {z . (x,z) ∈ f1 ` (RBT_set t)} else None)"
by force
then show ?thesis
using Some unfolding set_as_map_image_def set_as_map_def by simp
qed

lemma dual_set_as_map_image_code[code] :
fixes t :: "('a1 ::ccompare × 'a2 :: ccompare) set_rbt"
and   f1 :: "('a1 × 'a2) ⇒ ('b1 :: ccompare × 'b2 ::ccompare)"
and   f2 :: "('a1 × 'a2) ⇒ ('c1 :: ccompare × 'c2 ::ccompare)"
shows "dual_set_as_map_image (RBT_set t) f1 f2 = (case ID CCOMPARE(('a1 × 'a2)) of
Some _ ⇒ let mm = (RBT_Set2.fold (λ kv (m1,m2) .
( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)
, case f2 kv of (x,z) ⇒ (case Mapping.lookup m2 (x) of None ⇒ Mapping.update (x) {z} m2 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m2)))
t
(Mapping.empty,Mapping.empty))
in (Mapping.lookup (fst mm), Mapping.lookup (snd mm)) |
None   ⇒ Code.abort (STR ''dual_set_as_map_image RBT_set: ccompare = None'')
(λ_. (dual_set_as_map_image (RBT_set t) f1 f2)))"
proof (cases "ID CCOMPARE(('a1 × 'a2))")
case None
then show ?thesis by auto
next
case (Some a)

let ?f1 = "λ xs . (fold (λ kv m . case f1 kv of (x,z) ⇒ (case Mapping.lookup m (x) of None ⇒ Mapping.update (x) {z} m | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)) xs Mapping.empty)"
let ?f2 = "λ xs . (fold (λ kv m . case f2 kv of (x,z) ⇒ (case Mapping.lookup m (x) of None ⇒ Mapping.update (x) {z} m | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)) xs Mapping.empty)"

let ?f12 = "λ xs . fold (λ kv (m1,m2) .
( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)
, case f2 kv of (x,z) ⇒ (case Mapping.lookup m2 (x) of None ⇒ Mapping.update (x) {z} m2 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m2)))
xs
(Mapping.empty,Mapping.empty)"

let ?f1' = "λ t . (RBT_Set2.fold (λ kv m . case f1 kv of (x,z) ⇒ (case Mapping.lookup m (x) of None ⇒ Mapping.update (x) {z} m | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)) t Mapping.empty)"
let ?f2' = "λ t . (RBT_Set2.fold (λ kv m . case f2 kv of (x,z) ⇒ (case Mapping.lookup m (x) of None ⇒ Mapping.update (x) {z} m | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)) t Mapping.empty)"

let ?f12' = "λ t . RBT_Set2.fold (λ kv (m1,m2) .
( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)
, case f2 kv of (x,z) ⇒ (case Mapping.lookup m2 (x) of None ⇒ Mapping.update (x) {z} m2 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m2)))
t
(Mapping.empty,Mapping.empty)"

have "⋀xs . ?f12 xs = (?f1 xs, ?f2 xs)"
unfolding fold_dual[symmetric] by simp
then have "?f12 (RBT_Set2.keys t) = (?f1 (RBT_Set2.keys t), ?f2 (RBT_Set2.keys t))"
by simp
then have "?f12' t = (?f1' t, ?f2' t)"
unfolding fold_conv_fold_keys by metis

have "Mapping.lookup (fst (?f12' t)) = set_as_map (f1 ` (RBT_set t))"
unfolding ‹?f12' t = (?f1' t, ?f2' t)› fst_conv set_as_map_image_def[symmetric]
using set_as_map_image_code[of t f1] Some by simp
moreover have "Mapping.lookup (snd (?f12' t)) = set_as_map (f2 ` (RBT_set t))"
unfolding ‹?f12' t = (?f1' t, ?f2' t)› snd_conv set_as_map_image_def[symmetric]
using set_as_map_image_code[of t f2] Some by simp
ultimately show ?thesis
unfolding dual_set_as_map_image_def Let_def using Some by simp
qed

subsubsection ‹New Code Equations for @{text "h"}›

declare [[code drop: h]]
lemma h_refined[code] : "h M (q,x)
= (let m = set_as_map_image (transitions M) (λ(q,x,y,q') . ((q,x),y,q'))
in (case m (q,x) of Some yqs ⇒ yqs | None ⇒ {}))"
apply transfer
unfolding h_code set_as_map_image_def by simp

subsubsection ‹New Code Equations for @{text "canonical_separator'"}›

lemma canonical_separator'_refined[code] :
fixes M :: "('a,'b,'c) fsm_impl"
shows
"FSM_Impl.canonical_separator' M P q1 q2 = (if FSM_Impl.fsm_impl.initial P = (q1,q2)
then
(let f'  = set_as_map_image (FSM_Impl.fsm_impl.transitions M) (λ(q,x,y,q') . ((q,x),y));
f   = (λqx . (case f' qx of Some yqs ⇒ yqs | None ⇒ {}));
shifted_transitions' = shifted_transitions (FSM_Impl.fsm_impl.transitions P);
distinguishing_transitions_lr = distinguishing_transitions f q1 q2 (FSM_Impl.fsm_impl.states P) (FSM_Impl.fsm_impl.inputs P);
ts = shifted_transitions' ∪ distinguishing_transitions_lr
in FSMI
(Inl (q1,q2))
((image Inl (FSM_Impl.fsm_impl.states P)) ∪ {Inr q1, Inr q2})
(FSM_Impl.fsm_impl.inputs M ∪ FSM_Impl.fsm_impl.inputs P)
(FSM_Impl.fsm_impl.outputs M ∪ FSM_Impl.fsm_impl.outputs P)
(ts))
else FSMI
(Inl (q1,q2)) {Inl (q1,q2)} {} {} {})"
unfolding set_as_map_image_def by simp

subsubsection ‹New Code Equations for @{text "calculate_test_paths"}›

lemma calculate_test_paths_refined[code] :
"calculate_test_paths M m d_reachable_states r_distinguishable_pairs repetition_sets =
(let
paths_with_witnesses
= (image (λ q . (q,m_traversal_paths_with_witness M q repetition_sets m)) d_reachable_states);
get_paths
= m2f (set_as_map paths_with_witnesses);
PrefixPairTests
= ⋃ q ∈ d_reachable_states . ⋃ mrsps ∈ get_paths q . prefix_pair_tests q mrsps;
PreamblePrefixTests
= ⋃ q ∈ d_reachable_states . ⋃ mrsps ∈ get_paths q . preamble_prefix_tests q mrsps d_reachable_states;
PreamblePairTests
= preamble_pair_tests (⋃ (q,pw) ∈ paths_with_witnesses . ((λ (p,(rd,dr)) . dr) ` pw)) r_distinguishable_pairs;
tests
= PrefixPairTests ∪ PreamblePrefixTests ∪ PreamblePairTests;
tps'
= m2f_by ⋃ (set_as_map_image paths_with_witnesses (λ (q,p) . (q, image fst p)));
dual_maps
=  dual_set_as_map_image tests (λ (q,p,q') . (q,p)) (λ (q,p,q') . ((q,p),q'));
tps''
= m2f (fst dual_maps);
tps
= (λ q . tps' q ∪ tps'' q);
rd_targets
= m2f (snd dual_maps)
in ( tps, rd_targets))"

unfolding calculate_test_paths_def Let_def dual_set_as_map_image_def fst_conv snd_conv set_as_map_image_def
by simp

subsubsection ‹New Code Equations for @{text "prefix_pair_tests"}›

fun target' :: "'state ⇒ ('state, 'input, 'output) path ⇒ 'state" where
"target' q [] = q" |
"target' q p = t_target (last p)"

lemma target_refined[code] :
"target q p = target' q p"
proof (cases p rule: rev_cases)
case Nil
then show ?thesis by auto
next
case (snoc p' t)
then have "p ≠ []" by auto
then show ?thesis unfolding snoc target.simps visited_states.simps
by (metis (no_types, lifting) last_ConsR last_map list.map_disc_iff target'.elims)
qed

declare [[code drop: prefix_pair_tests]]
lemma prefix_pair_tests_refined[code] :
fixes t :: "(('a ::ccompare,'b::ccompare,'c::ccompare) traversal_path × ('a set × 'a set)) set_rbt"
shows "prefix_pair_tests q (RBT_set t) = (case ID CCOMPARE((('a,'b,'c) traversal_path × ('a set × 'a set))) of
Some _ ⇒ set
(concat (map (λ (p,(rd,dr)) .
(concat (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))])
(filter (λ (p1,p2) . (target q p1) ≠ (target q p2) ∧ (target q p1) ∈ rd ∧ (target q p2) ∈ rd) (prefix_pairs p)))))
(RBT_Set2.keys t))) |
None   ⇒ Code.abort (STR ''prefix_pair_tests RBT_set: ccompare = None'')
(λ_. (prefix_pair_tests q (RBT_set t))))"
(is "prefix_pair_tests q (RBT_set t) = ?C")
proof (cases "ID CCOMPARE((('a ::ccompare,'b::ccompare,'c::ccompare) traversal_path × ('a set × 'a set)))")
case None
then show ?thesis by auto
next
case (Some a)

have *: "?C = (⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) (set (RBT_Set2.keys t))))"
proof -
let ?S1 = "set (concat (map (λ (p,(rd,dr)) . (concat (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))]) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) (RBT_Set2.keys t)))"
let ?S2 = "(⋃(image (λ (p,(rd,dr)) . ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) (set (RBT_Set2.keys t))))"

have *: "?C = ?S1"
proof -
have *: "⋀ rd p . (filter (λ (p1,p2) . (target q p1) ≠ (target q p2) ∧ (target q p1) ∈ rd ∧ (target q p2) ∈ rd) (prefix_pairs p)) = (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))"
by meson
have "?C = set (concat (map (λ (p,(rd,dr)) . (concat (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))]) (filter (λ (p1,p2) . (target q p1) ≠ (target q p2) ∧ (target q p1) ∈ rd ∧ (target q p2) ∈ rd) (prefix_pairs p))))) (RBT_Set2.keys t)))"
using Some by auto
then show ?thesis
unfolding * by presburger
qed

have union_filter_helper: "⋀ xs f x1 x2  y . y ∈ f (x1,x2) ⟹ (x1,x2) ∈ set xs ⟹ y ∈ ⋃ (set (map f xs))"
by auto
have concat_set_helper : "⋀ xss xs x . x ∈ set xs ⟹ xs ∈ set xss ⟹ x ∈ set (concat xss)"
by auto

have "⋀ x . x ∈ ?S1 ⟹ x ∈ ?S2"
proof -
fix x assume "x ∈ ?S1"
then obtain p rd dr p1 p2 where "(p,(rd,dr)) ∈ set (RBT_Set2.keys t)"
and   "(p1,p2) ∈ set ((filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))"
and   "x ∈ set [(q,p1,(target q p2)), (q,p2,(target q p1))]"
by auto
then have "x ∈ {(q,p1,(target q p2)), (q,p2,(target q p1))}"
by auto
then have "x ∈ ⋃ (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))"
using union_filter_helper[OF _ ‹(p1,p2) ∈ set ((filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))›, of x "(λ(p1, p2). {(q, p1, target q p2), (q, p2, target q p1)})"] by simp
then show "x ∈ ?S2"
using ‹(p,(rd,dr)) ∈ set (RBT_Set2.keys t)› by blast
qed

moreover have "⋀ x . x ∈ ?S2 ⟹ x ∈ ?S1"
proof -
fix x assume "x ∈ ?S2"
then obtain p rd dr p1 p2 where "(p,(rd,dr)) ∈ set (RBT_Set2.keys t)"
and   "(p1,p2) ∈ set ((filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))"
and   "x ∈ {(q,p1,(target q p2)), (q,p2,(target q p1))}"
by auto

then have *: "x ∈ set [(q,p1,(target q p2)), (q,p2,(target q p1))]" by auto
have **: "[(q,p1,(target q p2)), (q,p2,(target q p1))] ∈ set (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))]) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))"
using ‹(p1,p2) ∈ set ((filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))› by force
have ***: "(concat (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))]) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p)))) ∈ set ((map (λ (p,(rd,dr)) . (concat (map (λ (p1,p2) . [(q,p1,(target q p2)), (q,p2,(target q p1))]) (filter (λ (p1,p2) . (target q p1) ∈ rd ∧ (target q p2) ∈ rd ∧ (target q p1) ≠ (target q p2)) (prefix_pairs p))))) (RBT_Set2.keys t)))"
using ‹(p,(rd,dr)) ∈ set (RBT_Set2.keys t)› by force

show "x ∈ ?S1"
using concat_set_helper[OF concat_set_helper[OF * **] ***] by assumption
qed

ultimately show ?thesis unfolding * by blast
qed

show ?thesis
unfolding * unfolding prefix_pair_tests_code
using Some by (simp add: RBT_set_conv_keys)
qed

subsubsection ‹New Code Equations for @{text "preamble_prefix_tests"}›

declare [[code drop: preamble_prefix_tests]]
lemma preamble_prefix_tests_refined[code] :
fixes t1 :: "(('a ::ccompare,'b::ccompare,'c::ccompare) traversal_path × ('a set × 'a set)) set_rbt"
and   t2 :: "'a set_rbt"
shows "preamble_prefix_tests q (RBT_set t1) (RBT_set t2) = (case ID CCOMPARE((('a,'b,'c) traversal_path × ('a set × 'a set))) of
Some _ ⇒ (case ID CCOMPARE('a) of
Some _ ⇒ set (concat (map (λ (p,(rd,dr)) .
(concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))])
(filter (λ (p1,q2) . (target q p1) ≠ q2 ∧ (target q p1) ∈ rd ∧ q2 ∈ rd)
(List.product (prefixes p) (RBT_Set2.keys t2))))))
(RBT_Set2.keys t1))) |
None ⇒ Code.abort (STR ''prefix_pair_tests RBT_set: ccompare = None'') (λ_. (preamble_prefix_tests q (RBT_set t1) (RBT_set t2)))) |
None ⇒ Code.abort (STR ''prefix_pair_tests RBT_set: ccompare = None'') (λ_. (preamble_prefix_tests q (RBT_set t1) (RBT_set t2))))"
(is "preamble_prefix_tests q (RBT_set t1) (RBT_set t2) = ?C")
proof (cases "ID CCOMPARE((('a,'b,'c) traversal_path × ('a set × 'a set)))")
case None
then show ?thesis by auto
next
case (Some a)
then have k1: "(RBT_set t1) = set (RBT_Set2.keys t1)"

show ?thesis proof (cases "ID CCOMPARE('a)")
case None
then show ?thesis using Some by auto
next
case (Some b)
then have k2: "(RBT_set t2) = set (RBT_Set2.keys t2)"

have "preamble_prefix_tests q (RBT_set t1) (RBT_set t2) = (⋃(p, rd, dr)∈ set (RBT_Set2.keys t1). ⋃(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2))). {(q, p1, q2), (q2, [], target q p1)})"
unfolding preamble_prefix_tests_code  k1 k2 by simp

moreover have "?C = (⋃(p, rd, dr)∈ set (RBT_Set2.keys t1). ⋃(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2))). {(q, p1, q2), (q2, [], target q p1)})"
proof -
let ?S1 = "set (concat (map (λ (p,(rd,dr)) . (concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))))) (RBT_Set2.keys t1)))"
let ?S2 = "(⋃(p, rd, dr)∈ set (RBT_Set2.keys t1). ⋃(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2))). {(q, p1, q2), (q2, [], target q p1)})"

have *: "?C = ?S1"
proof -
have *: "⋀ rd p . (filter (λ (p1,q2) . (target q p1) ≠ q2 ∧ (target q p1) ∈ rd ∧ q2 ∈ rd) (List.product (prefixes p) (RBT_Set2.keys t2))) = (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))"
by meson
have "?C = set (concat (map (λ (p,(rd,dr)) . (concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ≠ q2 ∧ (target q p1) ∈ rd ∧ q2 ∈ rd) (List.product (prefixes p) (RBT_Set2.keys t2)))))) (RBT_Set2.keys t1)))"
using Some ‹ID ccompare = Some a› by auto
then show ?thesis
unfolding * by presburger
qed

have union_filter_helper: "⋀ xs f x1 x2  y . y ∈ f (x1,x2) ⟹ (x1,x2) ∈ set xs ⟹ y ∈ ⋃ (set (map f xs))"
by auto
have concat_set_helper : "⋀ xss xs x . x ∈ set xs ⟹ xs ∈ set xss ⟹ x ∈ set (concat xss)"
by auto

have "⋀ x . x ∈ ?S1 ⟹ x ∈ ?S2"
proof -
fix x assume "x ∈ ?S1"

obtain prddr where "prddr ∈ set (RBT_Set2.keys t1)"
and   "x ∈ set ((λ (p,(rd,dr)) . (concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))))) prddr)"
using concat_map_elem[OF ‹x ∈ ?S1›] by blast

moreover obtain p rd dr where "prddr = (p,(rd,dr))"
using prod_cases3 by blast

ultimately have "(p,(rd,dr)) ∈ set (RBT_Set2.keys t1)"
and  "x ∈ set ((concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2))))))"
by auto
then obtain p1 q2 where "(p1,q2) ∈ set ((filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2))))"
and   "x ∈ set [(q,p1,q2), (q2,[],(target q p1))]"
by auto

then have "x ∈ {(q,p1,q2), (q2,[],(target q p1))}"
by auto
then have "x ∈ ⋃ (set (map (λ(p1, q2). {(q, p1, q2), (q2, [], target q p1)}) (filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))))"
using union_filter_helper[OF _ ‹(p1,q2) ∈ set ((filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2))))›, of x "(λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))})"] by simp
then have "x ∈ (⋃(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2))). {(q, p1, q2), (q2, [], target q p1)})"
by auto
then show "x ∈ ?S2"
using ‹(p,(rd,dr)) ∈ set (RBT_Set2.keys t1)› by blast
qed

moreover have "⋀ x . x ∈ ?S2 ⟹ x ∈ ?S1"
proof -
fix x assume "x ∈ ?S2"
then obtain p rd dr p1 q2 where "(p, rd, dr)∈ set (RBT_Set2.keys t1)"
and   "(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2)))"
and   "x ∈ {(q, p1, q2), (q2, [], target q p1)}"
by blast

then have *:"x ∈ set [(q, p1, q2), (q2, [], target q p1)]"
by auto

have "(p1,q2) ∈ set (filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))"
using ‹(p1, q2)∈Set.filter (λ(p1, q2). target q p1 ∈ rd ∧ q2 ∈ rd ∧ target q p1 ≠ q2) (set (prefixes p) × (set (RBT_Set2.keys t2)))›
by auto
then have **:"[(q, p1, q2), (q2, [], target q p1)] ∈ set ((map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))))"
by force

have ***: "(concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2))))) ∈ set (map (λ (p,(rd,dr)) . (concat (map (λ (p1,q2) . [(q,p1,q2), (q2,[],(target q p1))]) (filter (λ (p1,q2) . (target q p1) ∈ rd ∧ q2 ∈ rd ∧ (target q p1) ≠ q2) (List.product (prefixes p) (RBT_Set2.keys t2)))))) (RBT_Set2.keys t1))"
using ‹(p, rd, dr)∈ set (RBT_Set2.keys t1)› by force

show "x ∈ ?S1"
using concat_set_helper[OF concat_set_helper[OF * **] ***] by assumption
qed

ultimately show ?thesis unfolding * by blast
qed

ultimately show ?thesis by simp
qed
qed

end```