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