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