# Theory Test_Suite_Representations_Refined

```section ‹Refined Code Generation for Test Suites›

text ‹This theory provides alternative code equations for selected functions on test suites.
Currently only Mapping via RBT is supported.›

theory Test_Suite_Representations_Refined
imports Test_Suite_Representations "../Prefix_Tree_Refined" "../Util_Refined"
begin

declare [[code drop: Test_Suite_Representations.test_suite_from_io_tree]]

lemma test_suite_from_io_tree_refined[code] :
fixes M :: "('a,'b :: ccompare, 'c :: ccompare) fsm"
and m :: "(('b×'c), ('b×'c) prefix_tree) mapping_rbt"
shows "test_suite_from_io_tree M q (MPT (RBT_Mapping m))
= (case ID CCOMPARE(('b × 'c)) of
None ⇒ Code.abort (STR ''test_suite_from_io_tree RBT_set: ccompare = None'') (λ_ . test_suite_from_io_tree M q (MPT (RBT_Mapping m))) |
Some _ ⇒ MPT (Mapping.tabulate (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m)) (λ ((x,y),b) . case h_obs M q x y of None ⇒ Prefix_Tree.empty | Some q' ⇒ test_suite_from_io_tree M q' (case RBT_Mapping2.lookup m (x,y) of Some t' ⇒ t'))))"
proof (cases "ID CCOMPARE(('b × 'c))")
case None
then show ?thesis by auto
next
case (Some a)
then have "ID CCOMPARE(('b × 'c)) ≠ None"
using Some by auto

have "distinct (map fst (RBT_Mapping2.entries m))"
apply transfer
using linorder.distinct_entries[OF ID_ccompare[OF Some]]
ord.is_rbt_rbt_sorted
Some
by auto

have "⋀ a b . (RBT_Mapping2.lookup m a = Some b) = ((a,b) ∈ List.set (RBT_Mapping2.entries m))"
using map_of_entries[OF ‹ID CCOMPARE(('b × 'c)) ≠ None›, of m]
using map_of_eq_Some_iff[OF ‹distinct (map fst (RBT_Mapping2.entries m))›] by auto

let ?f2 = "Mapping.tabulate (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m)) (λ ((x,y),b) . case h_obs M q x y of None ⇒ Prefix_Tree.empty | Some q' ⇒ test_suite_from_io_tree M q' (case RBT_Mapping2.lookup m (x,y) of Some t' ⇒ t'))"
let ?f1 = "λ xs . λ ((x,y),b) . case map_of xs (x,y) of
None ⇒ None |
Some t ⇒ (case h_obs M q x y of
None ⇒ (if b then None else Some empty) |
Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None))"

have "Mapping.lookup ?f2 = ?f1 (RBT_Mapping2.entries m)"
proof
fix k
show "Mapping.lookup ?f2 k = ?f1 (RBT_Mapping2.entries m) k"
proof -
obtain x y b where "k = ((x,y),b)"
by (metis prod.exhaust_sel)

show ?thesis proof (cases "RBT_Mapping2.lookup m (x,y)")
case None

then have "((x,y),b) ∉ List.set (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))"
using ‹⋀ a b . (RBT_Mapping2.lookup m a = Some b) = ((a,b) ∈ List.set (RBT_Mapping2.entries m))›[of "(x,y)"]
by auto
then have "Mapping.lookup ?f2 ((x,y),b) = None"
by (metis (mono_tags, lifting) Mapping.lookup.rep_eq map_of_map_Pair_key tabulate.rep_eq)
moreover have "?f1 (RBT_Mapping2.entries m) ((x,y),b) = None"
using ‹⋀ a b . (RBT_Mapping2.lookup m a = Some b) = ((a,b) ∈ List.set (RBT_Mapping2.entries m))›[of "(x,y)"]
None
by (metis (no_types, lifting) map_of_SomeD not_None_eq old.prod.case option.simps(4))
ultimately show ?thesis
unfolding ‹k = ((x,y),b)› by simp
next
case (Some t')
then have "((x,y),t') ∈ List.set (RBT_Mapping2.entries m)"
using ‹⋀ a b . (RBT_Mapping2.lookup m a = Some b) = ((a,b) ∈ List.set (RBT_Mapping2.entries m))› by auto

show ?thesis proof (cases "h_obs M q x y")
case None

show ?thesis proof (cases b)
case True

then have "((x,y),b) ∉ List.set (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))"
using None by auto
then have "Mapping.lookup ?f2 ((x,y),b) = None"
by (metis (mono_tags, lifting) Mapping.lookup.rep_eq map_of_map_Pair_key tabulate.rep_eq)
moreover have "?f1 (RBT_Mapping2.entries m) ((x,y),b) = None"
using Some None True
using ‹((x, y), t') ∈ list.set (RBT_Mapping2.entries m)› ‹distinct (map fst (RBT_Mapping2.entries m))›
by auto
ultimately show ?thesis
unfolding ‹k = ((x,y),b)› by simp
next
case False

then have "((x,y),b) ∈ List.set (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))"
using None ‹((x,y),t') ∈ List.set (RBT_Mapping2.entries m)› by force
then have "Mapping.lookup ?f2 ((x,y),b) = Some empty"
proof -
have "⋀p ps f. (p::('b × 'c) × bool) ∉ list.set ps ∨ Mapping.lookup (Mapping.tabulate ps f) p = Some (f p::(('b × 'c) × bool) prefix_tree)"
by (simp add: Mapping.lookup.rep_eq map_of_map_Pair_key tabulate.rep_eq)
then show ?thesis
using None ‹((x, y), b) ∈ list.set (map (λ((x, y), t). ((x, y), h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))› by auto
qed
moreover have "?f1 (RBT_Mapping2.entries m) ((x,y),b) = Some empty"
using Some None False
using ‹((x, y), t') ∈ list.set (RBT_Mapping2.entries m)›
using ‹distinct (map fst (RBT_Mapping2.entries m))› by auto
ultimately show ?thesis
unfolding ‹k = ((x,y),b)› by simp
qed
next
case (Some q')
show ?thesis proof (cases b)
case True
then have "((x,y),b) ∈ List.set (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))"
using Some ‹((x,y),t') ∈ List.set (RBT_Mapping2.entries m)› by force
then have "Mapping.lookup ?f2 ((x,y),b) = Some (test_suite_from_io_tree M q' t')"
proof -
have "⋀p ps f. (p::('b × 'c) × bool) ∉ list.set ps ∨ Mapping.lookup (Mapping.tabulate ps f) p = Some (f p::(('b × 'c) × bool) prefix_tree)"
by (simp add: Mapping.lookup.rep_eq map_of_map_Pair_key tabulate.rep_eq)
then show ?thesis
using Some ‹RBT_Mapping2.lookup m (x, y) = Some t'› ‹((x, y), b) ∈ list.set (map (λ((x, y), t). ((x, y), h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))› by auto
qed
moreover have "?f1 (RBT_Mapping2.entries m) ((x,y),b) = Some (test_suite_from_io_tree M q' t')"
using Some ‹RBT_Mapping2.lookup m (x, y) = Some t'› True
using ‹((x, y), t') ∈ list.set (RBT_Mapping2.entries m)›
using ‹distinct (map fst (RBT_Mapping2.entries m))› by auto
ultimately show ?thesis
unfolding ‹k = ((x,y),b)› by simp
next
case False
then have "((x,y),b) ∉ List.set (map (λ((x,y),t) . ((x,y),h_obs M q x y ≠ None)) (RBT_Mapping2.entries m))"
using Some by auto
then have "Mapping.lookup ?f2 ((x,y),b) = None"
by (metis (mono_tags, lifting) Mapping.lookup.rep_eq map_of_map_Pair_key tabulate.rep_eq)
moreover have "?f1 (RBT_Mapping2.entries m) ((x,y),b) = None"
using Some ‹RBT_Mapping2.lookup m (x, y) = Some t'› False
using ‹((x, y), t') ∈ list.set (RBT_Mapping2.entries m)› ‹distinct (map fst (RBT_Mapping2.entries m))›
by auto
ultimately show ?thesis
unfolding ‹k = ((x,y),b)› by simp
qed
qed
qed
qed
qed

obtain m' where "test_suite_from_io_tree M q (MPT (RBT_Mapping m)) = MPT m'"
by (simp add: test_suite_from_io_tree_MPT)
then have "test_suite_from_io_tree M q (MPT (RBT_Mapping m)) = PT (Mapping.lookup m')"
using MPT_def by simp
have "Mapping.lookup m' = (λ ((x,y),b) . case RBT_Mapping2.lookup m (x,y) of
None ⇒ None |
Some t ⇒ (case h_obs M q x y of
None ⇒ (if b then None else Some empty) |
Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None)))"
proof -
have "test_suite_from_io_tree M q (PT (Mapping.lookup (RBT_Mapping m))) = PT (Mapping.lookup m')"
by (metis MPT_def ‹test_suite_from_io_tree M q (MPT (RBT_Mapping m)) = PT (Mapping.lookup m')›)
then have "Mapping.lookup m' = (λ((b, c), ba). case Mapping.lookup (RBT_Mapping m) (b, c) of None ⇒ None | Some p ⇒ (case h_obs M q b c of None ⇒ if ba then None else Some Prefix_Tree.empty | Some a ⇒ if ba then Some (test_suite_from_io_tree M a p) else None))"
by auto
then show ?thesis
by (metis (no_types) lookup_Mapping_code(2))
qed
then have "Mapping.lookup m' = ?f1 (RBT_Mapping2.entries m)"
unfolding map_of_entries[OF ‹ID CCOMPARE(('b × 'c)) ≠ None›, of m] by simp
then have "Mapping.lookup ?f2 = Mapping.lookup m'"
using ‹Mapping.lookup ?f2 = ?f1 (RBT_Mapping2.entries m)› by simp
then show ?thesis
using Some unfolding ‹test_suite_from_io_tree M q (MPT (RBT_Mapping m)) = MPT m'›
by (simp add: MPT_def)
qed

end```