Theory Test_Suite_Representations

section ‹Test Suites for Language Equivalence›

text ‹This file introduces a type for test suites represented as a prefix tree in which
      each IO-pair is additionally labeled by a boolean value representing whether 
      the IO-pair should be exhibited by the SUT in order to pass the test suite.›


theory Test_Suite_Representations
imports "../Minimisation" "../Prefix_Tree"
begin


type_synonym ('b,'c) test_suite = "(('b × 'c) × bool) prefix_tree"

(* also reduces the test suite by dropping suffixes after the first element not in LS M q *)
function (domintros) test_suite_from_io_tree :: "('a,'b,'c) fsm  'a  ('b × 'c) prefix_tree  ('b,'c) test_suite" where
  "test_suite_from_io_tree M q (PT m) = PT (λ ((x,y),b) . case 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)))"
  by pat_completeness auto
termination 
proof -
  {
    fix M :: "('a,'b,'c) fsm"
    fix q t
  
    have "test_suite_from_io_tree_dom (M,q,t)" 
    proof (induction t arbitrary: M q)
      case (PT m)
      then have "x y t q'. m (x, y) = Some t  test_suite_from_io_tree_dom (M, q', t)"
        by blast 
      then show ?case 
        using test_suite_from_io_tree.domintros[of m q M] by auto
    qed
  }
  then show ?thesis by auto
qed

subsection ‹Transforming an IO-prefix-tree to a test suite›

lemma test_suite_from_io_tree_set :
  assumes "observable M"
      and "q  states M"
    shows "(set (test_suite_from_io_tree M q t)) = ((λ xs . map (λ x . (x,True)) xs) ` (set t  LS M q)) 
                                                     ((λ xs . (map (λ x . (x,True)) (butlast xs))@[(last xs,False)]) ` {xs@[x] | xs x . xs  set t  LS M q  xs@[x]  set t - LS M q})"
    (is "?S1 q t = ?S2 q t")
proof 
  show "?S1 q t  ?S2 q t"
  proof 
    fix xs assume "xs  ?S1 q t"
    then have "isin (test_suite_from_io_tree M q t) xs"
      by auto
    then show "xs  ?S2 q t"
      using q  states M
    proof (induction xs arbitrary: q t)
      case Nil

      have "[]  set t"
        using Nil.prems(1) set_Nil by auto 
      moreover have "[]  LS M q"
        using Nil.prems(2) by auto
      ultimately show ?case
        by auto 
    next
      case (Cons x' xs)
      moreover obtain x y b where "x' = ((x,y),b)"
        by (metis surj_pair)
      moreover obtain m where "t = PT m"
        by (meson prefix_tree.exhaust)
      ultimately have "isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)"
        by auto

      let ?fi = "λ 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))"
      let ?fo = "case m (x,y) of
                  None  None |
                  Some t  ?fi t"
      
      obtain tst where "?fo = Some tst"
        using isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)
        unfolding test_suite_from_io_tree.simps isin.simps by force
      then have "isin tst xs"
        using isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)
        by auto

      obtain t' where "m (x,y) = Some t'"
                       and "?fi t' = Some tst"
        using ?fo = Some tst
        by (metis (no_types, lifting) option.case_eq_if option.collapse option.distinct(1))
      then consider "h_obs M q x y = None  ¬b  tst = empty" |
                    " q' . h_obs M q x y = Some q'  b  tst = test_suite_from_io_tree M q' t'"
        unfolding option.case_eq_if
        using option.collapse[of "h_obs M q x y"]
        using option.distinct(1) option.inject
        by metis
      then show ?case proof cases
        case 1
        then have "h_obs M q x y = None" and "b = False" and "tst = empty"
          by auto

        have "isin empty xs"
          using isin tst xs tst = empty by auto
        then have "xs = []"
          using set_empty by auto
        then have *: "x'#xs = [((x,y),b)]"
          using x' = ((x,y),b) by auto

        have "[]  LS M q"
          using q  states M by auto
        moreover have "[]  set t"
          using set_Nil by auto
        moreover have "[(x,y)]  LS M q"
          using h_obs M q x y = None unfolding h_obs_None[OF observable M]
          by auto
        moreover have "isin t [(x,y)]"
          unfolding t = PT m isin.simps using m (x,y) = Some t'
          using isin.elims(3) by auto
        ultimately have "[(x,y)]  {xs @ [x] |xs x. xs  Prefix_Tree.set t  LS M q  xs @ [x]  Prefix_Tree.set t - LS M q}"
          by auto
        moreover have "(x'#xs) = ((λ xs . (map (λ x . (x,True)) (butlast xs))@[(last xs,False)]) [(x,y)])"
          unfolding * b = False 
          by auto
        ultimately show ?thesis 
          by blast
      next
        case 2
        then obtain q' where "h_obs M q x y = Some q'" 
                             "b = True" 
                             "tst = test_suite_from_io_tree M q' t'"
          by blast

        have p1: "isin (test_suite_from_io_tree M q' t') xs"
          using isin tst xs tst = test_suite_from_io_tree M q' t' by auto
        have p2: "q'  states M"
          using h_obs M q x y = Some q' fsm_transition_target unfolding h_obs_Some[OF observable M]
          by fastforce 

        have "xs  ?S2 q' t'" 
          using Cons.IH[OF p1 p2] .
        then consider (a) "xs  map (λx. (x, True)) ` (Prefix_Tree.set t'  LS M q')" |
                      (b) "xs  (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs  Prefix_Tree.set t'  LS M q'  xs @ [x]  Prefix_Tree.set t' - LS M q'}"
          by blast
        then show ?thesis proof cases
          case a
          then obtain xs' where "xs'  set t'" and "xs'  LS M q'"
                            and "xs = map (λx. (x, True)) xs'"
            by auto

          have "(x,y)#xs'  set t"
            using xs'  set t' m (x,y) = Some t' unfolding t = PT m by auto
          moreover have "(x,y)#xs'  LS M q"
            using h_obs M q x y = Some q' xs'  LS M q' unfolding h_obs_Some[OF observable M] 
            using LS_prepend_transition[of "(q,x,y,q')" M xs'] by auto
          moreover have "x'#xs = map (λx. (x, True)) ((x,y)#xs')"
            unfolding x' = ((x,y),b) b = True xs = map (λx. (x, True)) xs' by auto
          ultimately show ?thesis
            by (metis (no_types, lifting) Int_iff UnI1 image_eqI)
        next
          case b
          then obtain xs' where "xs'   {xs @ [x] |xs x. xs  Prefix_Tree.set t'  LS M q'  xs @ [x]  Prefix_Tree.set t' - LS M q'}"
                            and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) xs'"
            by blast
          moreover obtain bl l where "xs' = bl @ [l]"
            using calculation by blast 
          ultimately have "bl  set t'" and "bl  LS M q'" and "bl @ [l]  set t'" and "bl@[l]  LS M q'"
                      and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])"
            by auto
            

          have "(x,y)#bl  set t"
            using bl  set t' m (x,y) = Some t' unfolding t = PT m by auto 
          moreover have "(x,y)#bl  LS M q"
            using h_obs M q x y = Some q' bl  LS M q' unfolding h_obs_Some[OF observable M] 
            using LS_prepend_transition[of "(q,x,y,q')" M bl] by auto
          moreover have "(x,y)#(bl @ [l])  set t"
            using bl @ [l]  set t' m (x,y) = Some t' unfolding t = PT m by auto 
          moreover have "(x,y)#(bl@[l])  LS M q"
            using h_obs M q x y = Some q' bl@[l]  LS M q' unfolding h_obs_Some[OF observable M]  
            using observable_language_transition_target[OF observable M, of "(q,x,y,q')" "bl@[l]"]
            unfolding fst_conv snd_conv
            by blast
          ultimately have "(x,y)#bl@[l]  {xs @ [x] |xs x. xs  Prefix_Tree.set t  LS M q  xs @ [x]  Prefix_Tree.set t - LS M q}"
            by fastforce
          moreover have "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ((x,y)#(bl@[l]))"
            unfolding x' = ((x,y),b) b = True xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l]) by auto
          ultimately show ?thesis
            by fast
        qed
      qed
    qed
  qed

  show "?S2 q t  ?S1 q t"
  proof
    fix xs assume "xs  ?S2 q t"
    then consider "xs  map (λx. (x, True)) ` (set t  LS M q)" |
                  "xs  (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs  Prefix_Tree.set t  LS M q  xs @ [x]  Prefix_Tree.set t - LS M q}"
      by blast
    then show "xs  ?S1 q t" proof cases
      case 1
      then show ?thesis 
        using q  states M 
      proof (induction xs arbitrary: q t)
        case Nil
        then show ?case using set_Nil by auto
      next
        case (Cons x' xs) 
        obtain xs'' where "xs''  set t" and "xs''  LS M q"
                         and "x'#xs = map (λx. (x, True)) xs''"
          using Cons.prems(1)
          by (meson IntD1 IntD2 imageE) 
        
        then obtain x y xs' where "(x,y)#xs'  set t" and "(x,y)#xs'  LS M q"
                              and "x'#xs = map (λx. (x, True)) ((x,y)#xs')"
          by force
        then have "x' = ((x,y),True)" and "xs = map (λx. (x, True)) xs'"
          by auto 

        obtain m where "t = PT m"
          by (meson prefix_tree.exhaust)
          
        have "isin (PT m) ((x,y)#xs')"
          using (x,y)#xs'  set t unfolding t = PT m by auto
        then obtain t' where "m (x,y) = Some t'"
                         and "isin t' xs'"
          by (metis case_optionE isin.simps(2))

        have "[(x,y)]  LS M q"
          using (x,y)#xs'  LS M q language_prefix[of "[(x,y)]" xs' M q]
          by simp 
        then obtain q' where "h_obs M q x y = Some q'"
          using h_obs_None[OF observable M, of q x y] unfolding LS_single_transition by auto
        
        have "isin (test_suite_from_io_tree M q (PT m)) (((x,y),True)#xs) 
               = isin (test_suite_from_io_tree M q' t') (xs)"
          using m (x,y) = Some t' h_obs M q x y = Some q' by auto
        then have *: "x' # xs  set (test_suite_from_io_tree M q t)
                      = (xs  set (test_suite_from_io_tree M q' t'))"
          unfolding t = PT m x' = ((x,y),True) by auto

        have "xs'  LS M q'"
          using h_obs M q x y = Some q' unfolding h_obs_Some[OF observable M, of q x y]
          using (x,y)#xs'  LS M q observable_language_transition_target[OF observable M] by force
        moreover have "xs'  set t'"
          using isin t' xs' by auto
        ultimately have p1: "xs  map (λx. (x, True)) ` (set t'  LS M q')"
          unfolding xs = map (λx. (x, True)) xs' by auto

        have p2: "q'  states M"
          using h_obs M q x y = Some q' fsm_transition_target unfolding h_obs_Some[OF observable M]
          by fastforce 

        show ?case 
          using Cons.IH[OF p1 p2] unfolding * .
      qed
    next
      case 2
      then show ?thesis 
        using q  states M 
      proof (induction xs arbitrary: q t)
        case Nil
        then show ?case using set_Nil by auto
      next
        case (Cons x' xs) 
        then obtain xsT where "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) xsT"
                           and "xsT  {xs @ [x] |xs x. xs  Prefix_Tree.set t  LS M q  xs @ [x]  Prefix_Tree.set t - LS M q}"
          by blast
        moreover obtain bl l where "xsT = bl @ [l]"
          using calculation by auto
        ultimately have "bl  set t" and "bl  LS M q" and "bl @ [l]  set t" and "bl@[l]  LS M q"
                    and "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])"
          by auto

        obtain m where "t = PT m"
          by (meson prefix_tree.exhaust)
        
        show ?case proof (cases xs)
          case Nil
          then have "x' = (l,False)" and "bl = []"
            using x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l]) 
            by auto
          moreover obtain x y where "l = (x,y)"
            using prod.exhaust by metis
          ultimately have "[(x,y)]  set t" and "[(x,y)]  LS M q"  
            using bl @ [l]  set t bl@[l]  LS M q by auto

          obtain t' where "m (x,y) = Some t'"
            using [(x,y)]  set t unfolding t = PT m by force
          moreover have "h_obs M q x y = None"
            using [(x,y)]  LS M q unfolding h_obs_None[OF observable M] LS_single_transition by auto
          ultimately have "isin (test_suite_from_io_tree M q (PT m)) (x'#xs) = isin empty []"
            unfolding Nil x' = (l,False) test_suite_from_io_tree.simps isin.simps l = (x,y)
            by (simp add: Prefix_Tree.empty_def) 
          then show ?thesis
            using set_Nil unfolding t = PT m by auto
        next
          case (Cons x'' xs'')
          then obtain x y bl' where "bl = (x,y)#bl'"
            using x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])
            by (metis append.left_neutral butlast_snoc list.inject list.simps(8) neq_Nil_conv surj_pair) 
          then have "x' = ((x,y),True)"
                and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl'@[l])"
            using x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])
            by auto

          have "isin (PT m) ((x,y)#(bl'@[l]))" 
            using bl@[l]  set t unfolding bl = (x,y)#bl' t = PT m by auto
          then obtain t' where "m (x,y) = Some t'"
                           and "isin t' (bl'@[l])"
            unfolding isin.simps
            using case_optionE by blast 

          have "[(x,y)]  LS M q"
            using bl  LS M q language_prefix[of "[(x,y)]" bl' M q] unfolding bl = (x,y)#bl' by auto
          then obtain q' where "h_obs M q x y = Some q'"
            using h_obs_None[OF observable M] unfolding LS_single_transition by force
          then have p2: "q'  states M"
            using fsm_transition_target unfolding h_obs_Some[OF observable M]
            by fastforce 

          have "bl'  set t'"
            using isin t' (bl'@[l]) isin_prefix by auto
          moreover have "bl'  LS M q'"
            using h_obs M q x y = Some q' unfolding h_obs_Some[OF observable M]
            using bl  LS M q observable_language_transition_target[OF observable M] 
            unfolding bl = (x,y)#bl' by force
          moreover have "bl'@[l]  set t'"
            using isin t' (bl'@[l]) by auto
          moreover have "bl'@[l]  LS M q'"
          proof -
            have "(x, y) # (bl' @ [l])  LS M q"
              using bl@[l]  LS M q unfolding bl = (x,y)#bl' by auto
            then show ?thesis
              using h_obs M q x y = Some q' unfolding h_obs_Some[OF observable M]
              using LS_prepend_transition[of "(q,x,y,q')" M "bl'@[l]"]
              unfolding bl = (x,y)#bl' fst_conv snd_conv by blast
          qed
          ultimately have "(bl'@[l])   {xs @ [x] |xs x. xs  Prefix_Tree.set t'  LS M q'  xs @ [x]  Prefix_Tree.set t' - LS M q'}"
            by blast
          moreover have "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl'@[l])"
            using x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])
            unfolding Nil bl = (x,y)#bl' by auto
          ultimately have "xs  Prefix_Tree.set (test_suite_from_io_tree M q' t')"
            using Cons.IH[of t', OF _ p2] by blast
          then have "isin (test_suite_from_io_tree M q t) (x'#xs)"
            unfolding x' = ((x,y),True) t = PT m 
            unfolding test_suite_from_io_tree.simps isin.simps
            using m (x,y) = Some t' h_obs M q x y = Some q' by auto
          then show ?thesis
            by auto
        qed
      qed
    qed
  qed
qed

(* function written using xyb instead of immediately unfolding to e.g. ((x,y),b) as the
   resulting domintros fact was too weak
    see also: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00001.html *)
function (domintros) passes_test_suite :: "('a,'b,'c) fsm  'a  ('b,'c) test_suite  bool" where
  "passes_test_suite M q (PT m) = ( xyb  dom m . case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of
      None  ¬(snd xyb) |
      Some q'  snd xyb  passes_test_suite M q' (case m xyb of Some t  t))"
  by pat_completeness auto
termination 
proof -
  {
    fix M :: "('a,'b,'c) fsm"
    fix q t
    have "passes_test_suite_dom (M,q,t)"
    proof (induction t arbitrary: M q)
      case (PT m)
      then have " ab ba bb y x2 . m ((ab, ba), bb) = Some y  passes_test_suite_dom (M, x2, y)"
        by blast
      then show ?case 
        using passes_test_suite.domintros[of q M m] by auto 
    qed
  }
  then show ?thesis by auto
qed

lemma passes_test_suite_iff :
  assumes "observable M"
      and "q  states M"
shows "passes_test_suite M q t = ( iob  set t . (map fst iob)  LS M q  list_all snd iob)"
proof 
  show "passes_test_suite M q t  iobPrefix_Tree.set t. (map fst iob  LS M q) = list_all snd iob"
  proof 
    fix iob assume "passes_test_suite M q t" 
               and "iob  Prefix_Tree.set t" 
    then show "(map fst iob  LS M q) = list_all snd iob"
      using q  states M
    proof (induction iob arbitrary: q t)
      case Nil
      then show ?case by auto
    next
      case (Cons a iob)

      obtain m where "t = PT m"
        by (meson prefix_tree.exhaust) 
      then have "isin (PT m) (a#iob)" 
        using a # iob  Prefix_Tree.set t by simp
      moreover obtain x y b where "a = ((x,y),b)"
        by (metis old.prod.exhaust)
      ultimately obtain t' where "m ((x,y),b) = Some t'"
                             and "isin t' iob"
        unfolding isin.simps
        using case_optionE by blast 
      then have "((x,y),b)  dom m"
        by auto
      then have *: "(case h_obs M q x y of
                      None  ¬b |
                      Some q'  b  passes_test_suite M q' (case m ((x,y),b) of Some t  t))"
         using passes_test_suite M q t ((x,y),b)  dom m unfolding t = PT m passes_test_suite.simps
         by (metis fst_conv snd_conv)

      show ?case proof (cases b)
        case False
        then have "h_obs M q x y = None"
          using *
          using case_optionE by blast 
        then have "[(x,y)]  LS M q"
          unfolding h_obs_None[OF observable M] by auto
        then have "(map fst (a#iob))  LS M q"
          unfolding a = ((x,y),b) using language_prefix[of "[(x,y)]" "map fst iob" M q]
          by fastforce 
        then show ?thesis
          unfolding a = ((x,y),b) using False by auto
      next
        case True
        then obtain q' where "h_obs M q x y = Some q'"
          using * case_optionE by blast 
        then have **: "((map fst (a#iob))  LS M q) = ((map fst iob)  LS M q')"
          using observable_language_transition_target[OF observable M, of "(q,x,y,q')" "map fst iob"]
          unfolding a = ((x,y),b) h_obs_Some[OF observable M] fst_conv snd_conv
          by (metis (no_types, lifting) LS_prepend_transition fst_conv list.simps(9) mem_Collect_eq singletonI snd_conv)
        have ***: "list_all snd (a#iob) = list_all snd iob"
          unfolding a = ((x,y),b) using True by auto

        have "passes_test_suite M q' t'"
          using passes_test_suite M q t ((x,y),b)  dom m h_obs M q x y = Some q' True
          unfolding t = PT m passes_test_suite.simps
          using * m ((x, y), b) = Some t' by auto
        moreover have "iob  set t'"
          using isin t' iob by auto
        moreover have "q'  states M"
          using h_obs M q x y = Some q' fsm_transition_target
          unfolding h_obs_Some[OF observable M]
          by fastforce 
        ultimately show ?thesis
          using Cons.IH unfolding ** *** by blast
      qed
    qed
  qed

  show "iobPrefix_Tree.set t. (map fst iob  LS M q) = list_all snd iob  passes_test_suite M q t"
  proof (induction t arbitrary: q)
    case (PT m)

    have " xyb . xyb  dom m  case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None  ¬ snd xyb | Some q'  snd xyb  passes_test_suite M q' (case m xyb of Some t  t)"
    proof -
      fix xyb assume "xyb  dom m"
      moreover obtain x y b where "xyb = ((x,y),b)"
        by (metis old.prod.exhaust)
      ultimately obtain t' where "m ((x,y),b) = Some t'"
        by auto
      then have "isin (PT m) [((x,y),b)]"
        by auto
      then have "[((x,y),b)]  set (PT m)"
        by auto
      then have "(map fst [((x,y),b)]  LS M q) = list_all snd [((x,y),b)]"
        using iobPrefix_Tree.set (PT m). (map fst iob  LS M q) = list_all snd iob by blast
      then have "([(x,y)]  LS M q) = b"
        by auto
        


      show "case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None  ¬ snd xyb | Some q'  snd xyb  passes_test_suite M q' (case m xyb of Some t  t)"
        
      proof (cases "h_obs M q x y")
        case None
        then have "[(x,y)]  LS M q"
          unfolding h_obs_None[OF observable M] by auto
        then have "b = False"
          using ([(x,y)]  LS M q) = b by blast 
        then show ?thesis 
          using None unfolding xyb = ((x,y),b) by auto
      next
        case (Some q')
        then have "[(x,y)]  LS M q"
          unfolding h_obs_Some[OF observable M] LS_single_transition by force
        then have "b"
          using ([(x,y)]  LS M q) = b by blast 
        moreover have "passes_test_suite M q' t'"
        proof -
          have "Some t'  range m"
            using m ((x,y),b) = Some t'
            by (metis range_eqI) 
          moreover have "t'  set_option (Some t')"
            by auto
          moreover have "iobPrefix_Tree.set t'. (map fst iob  LS M q') = list_all snd iob"
          proof 
            fix iob assume "iob  Prefix_Tree.set t'"
            then have "isin t' iob"
              by auto
            then have "isin (PT m) (((x,y),b)#iob)"
              using m ((x,y),b) = Some t' 
              by auto
            then have "((x,y),b)#iob  set (PT m)"
              by auto
            then have "(map fst (((x,y),b)#iob)  LS M q) = list_all snd (((x,y),b)#iob)"
              using PT.prems by blast
            moreover have "(map fst (((x,y),b)#iob)  LS M q) = (map fst iob  LS M q')"
              using observable_language_transition_target[OF observable M, of "(q,x,y,q')" "map fst iob"]
              by (metis (no_types, lifting) LS_prepend_transition Some h_obs_Some[OF observable M] fst_conv list.simps(9) mem_Collect_eq singletonI snd_conv) 
            moreover have "list_all snd (((x,y),b)#iob) = list_all snd iob"
              using b by auto
            ultimately show "(map fst iob  LS M q') = list_all snd iob"
              by simp
          qed
          ultimately show ?thesis
            using PT.IH by blast
        qed
        ultimately show ?thesis 
          using m ((x,y),b) = Some t' xyb = ((x,y),b) Some
          by simp
      qed
    qed
    then show ?case 
      by auto    
  qed
qed



(* Main result of the test_suite transformation: 
    an IO prefix_tree representing a set of IO sequences can be transformed into a test suite
    such that passing the test suite equals passing the original set of sequences *)
lemma passes_test_suite_from_io_tree : 
  assumes "observable M" 
  and     "observable I"
  and     "qM  states M"
  and     "qI  states I"
shows "passes_test_suite I qI (test_suite_from_io_tree M qM t) = ((set t  LS M qM) = (set t  LS I qI))"
proof -

  define ts where "ts = test_suite_from_io_tree M qM t"
  then have "passes_test_suite I qI (test_suite_from_io_tree M qM t) = (iobset ts. (map fst iob  LS I qI) = list_all snd iob)"
    using passes_test_suite_iff[OF assms(2,4), of ts] 
    by auto
  also have " = ((set t  LS M qM) = (set t  LS I qI))"
  proof 
    have ts_set: "set ts = map (λx. (x, True)) ` (set t  LS M qM) 
                           (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) `
                             {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM}"
      using test_suite_from_io_tree_set[OF assms(1,3), of t] ts = test_suite_from_io_tree M qM t
      by auto

    show "iobPrefix_Tree.set ts. (map fst iob  LS I qI) = list_all snd iob  set t  LS M qM = set t  LS I qI"
    proof -
      assume "iobPrefix_Tree.set ts. (map fst iob  LS I qI) = list_all snd iob"
      then have ts_assm: " iob . iob  set ts  (map fst iob  LS I qI) = list_all snd iob"
        by blast

      show "set t  LS M qM = set t  LS I qI"
      proof
        show "set t  LS M qM  set t  LS I qI"
        proof 
          fix io assume "io  set t  LS M qM"
          then have "map (λx. (x, True)) io  set ts"
            unfolding ts_set by auto
          moreover have "list_all snd (map (λx. (x, True)) io)"
            by (induction io; auto)
          moreover have "map fst (map (λx. (x, True)) io) = io"
            by (induction io; auto)
          ultimately have "io  LS I qI"
            using ts_assm by force
          then show "io  set t  LS I qI"
            using io  set t  LS M qM by blast
        qed

        show "set t  LS I qI  set t  LS M qM"
        proof 
          fix io assume "io  set t  LS I qI"
          show "io  set t  LS M qM"
          proof (rule ccontr)
            assume "io  set t  LS M qM"
            then have "io  LS I qI - LS M qM"
              using io  set t  LS I qI by blast
            then obtain io' xy io'' where "io = io' @ [xy] @ io''" 
                                      and "io'  LS I qI  LS M qM" 
                                      and "io' @ [xy]  LS I qI - LS M qM" 
              using minimal_failure_prefix_ob[OF assms]
              by blast

            have "io'  set t  LS M qM"
              using io'  LS I qI  LS M qM io  set t  LS I qI isin_prefix[of t io' "[xy] @ io''"] language_prefix[of io' "[xy] @ io''"]
              unfolding io = io' @ [xy] @ io''
              by auto
            moreover have "io' @ [xy]  set t - LS M qM"
              using io' @ [xy]  LS I qI - LS M qM io  set t  LS I qI isin_prefix[of t "io'@[xy]" io''] 
              unfolding io = io' @ [xy] @ io'' 
              by auto
            ultimately have "io'@[xy]  {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM}"
              by blast
            then have "(λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (io'@[xy])  set ts"
              unfolding ts_set by blast
            then have "(map (λx. (x, True)) io' @ [(xy, False)])  set ts"
              by auto
            moreover have "(map fst (map (λx. (x, True)) io' @ [(xy, False)])  LS I qI)  list_all snd ((map (λx. (x, True)) io' @ [(xy, False)]))"
            proof -
              have "(map fst (map (λx. (x, True)) io' @ [(xy, False)])) = io'@[xy]"
                by (induction io'; auto)
              then show ?thesis
                using io' @ [xy]  set t - LS M qM io  set t  LS I qI language_prefix[of "io'@[xy]" io'' I qI]
                unfolding io = io' @ [xy] @ io''
                by auto
            qed
            ultimately show "False"
              using ts_assm by blast
          qed
        qed
      qed
    qed

    show "set t  LS M qM = Prefix_Tree.set t  LS I qI  iobset ts. (map fst iob  LS I qI) = list_all snd iob"
    proof 
      fix iob assume "set t  LS M qM = set t  LS I qI"
                 and "iob  set ts"

      then consider (a) "iob  map (λx. (x, True)) ` (set t  LS M qM)" |
                    (b) "iob  (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) `
                             {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM}"
        using ts_set by blast
      
      then show "(map fst iob  LS I qI) = list_all snd iob" 
      proof cases
        case a 
        then obtain io where "iob = map (λx. (x, True)) io"
                         and "io  set t  LS M qM"
          by blast

        then have "map fst iob = io"
          by auto
        then have "map fst iob  LS I qI"
          using io  set t  LS M qM set t  LS M qM = set t  LS I qI
          by auto
        moreover have "list_all snd iob"
          unfolding iob = map (λx. (x, True)) io by (induction io; auto)
        ultimately show ?thesis 
          by simp
      next
        case b

        then obtain ioxy where "iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (ioxy)"
                            and "ioxy  {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM}"
          by blast
        then obtain io xy where "ioxy = io@[xy]"
                            and "io@[xy]  set t - LS M qM"
          by blast
        then have *: "iob = map (λx. (x, True)) io @ [(xy, False)]"
          using iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (ioxy) by auto
        then have **: "map fst iob = io@[xy]"
          by (induction io arbitrary: iob; auto)

        have "¬map fst iob  LS I qI"
          unfolding ** using io@[xy]  set t - LS M qM set t  LS M qM = set t  LS I qI
          by blast
        moreover have "¬ list_all snd iob"
          unfolding * by auto
        ultimately show ?thesis 
          by simp
      qed
    qed
  qed
  finally show ?thesis .
qed



subsection ‹Code Refinement›


context includes lifting_syntax
begin

lemma map_entries_parametric:
  "((A ===> B) ===> (A ===> C ===> rel_option D) ===> (B ===> rel_option C) ===> A ===> rel_option D)
     (λf g m x. case (m  f) x of None  None | Some y  g x y) (λf g m x. case (m  f) x of None  None | Some y  g x y)"
  by transfer_prover

end

lift_definition map_entries :: "('c  'a)  ('c  'b  'd option)  ('a, 'b) mapping  ('c, 'd) mapping"
  is "λf g m x. case (m  f) x of None  None | Some y  g x y" parametric map_entries_parametric .
  

lemma test_suite_from_io_tree_MPT[code] :
  "test_suite_from_io_tree M q (MPT m) = 
    MPT (map_entries
          fst 
          (λ ((x,y),b) 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)))
          m)"
  (is "?t M q (MPT m) = MPT (?f M q m)")
proof -
  have "xyb . Mapping.lookup (?f M q m) xyb= (λ ((x,y),b) . case Mapping.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))) xyb"
  (is " xyb. ?f1 xyb = ?f2 xyb")
  proof -
    fix xyb 
    
    show "?f1 xyb = ?f2 xyb"
    proof -
      obtain x y b where *:"xyb = ((x,y),b)"
        by (metis prod.collapse)
      
      show ?thesis proof (cases "Mapping.lookup m (fst xyb)")
        case None

        have "?f1 xyb = None"
          by (metis (no_types, lifting) None lookup.rep_eq map_entries.rep_eq option.simps(4))
        moreover have "?f2 xyb = None"
          using None by (simp add: "*") 
        ultimately show ?thesis
          by simp
      next
        case (Some t)

        then have **:"?f1 xyb = (λ ((x,y),b) 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))) xyb t"
          by (simp add: lookup.rep_eq map_entries.rep_eq)
        
        show ?thesis
          unfolding ** using Some 
          by (simp add: "*") 
      qed
    qed
  qed
  then show ?thesis 
    unfolding MPT_def by auto
qed


lemma passes_test_suite_MPT[code]: 
  "passes_test_suite M q (MPT m) = ( xyb  Mapping.keys m . case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of
      None  ¬(snd xyb) |
      Some q'  snd xyb  passes_test_suite M q' (case Mapping.lookup m xyb of Some t  t))"
  by (simp add: MPT_def keys_dom_lookup)




subsection ‹Pass relations on list of lists representations of test suites›

fun passes_test_case :: "('a,'b,'c) fsm  'a  (('b × 'c) × bool) list  bool" where
  "passes_test_case M q [] = True" |
  "passes_test_case M q (((x,y),b)#io) = (if b 
    then case h_obs M q x y of
      Some q'  passes_test_case M q' io |
      None     False
    else h_obs M q x y = None)"

lemma passes_test_case_iff :
  assumes "observable M"
  and     "q  states M"
  shows "passes_test_case M q iob = ((map fst (takeWhile snd iob)  LS M q)
                                       (¬ (list_all snd iob)  map fst (take (Suc (length (takeWhile snd iob))) iob)  LS M q))"
using assms(2) proof (induction iob arbitrary: q)
  case Nil
  then show ?case by auto
next
  case (Cons a iob)
  obtain x y b where "a = ((x,y),b)"
    by (metis prod.collapse)

  show ?case proof (cases b)
    case True
    
    show ?thesis proof (cases "h_obs M q x y")
      case None
      then have "[(x,y)]  LS M q"
        unfolding h_obs_None[OF assms(1)] LS_single_transition by force
      then have "(map fst (takeWhile snd (a#iob))  LS M q)"
        unfolding a = ((x,y),b) using True
        by (metis (mono_tags, opaque_lifting) append.simps(1) append.simps(2) fst_conv language_prefix list.simps(9) prod.sel(2) takeWhile.simps(2)) 
      moreover have "passes_test_case M q (a#iob) = False"
        using None unfolding a = ((x,y),b) using True by auto
      ultimately show ?thesis 
        by blast
    next
      case (Some q')
      then have "passes_test_case M q (a#iob) = passes_test_case M q' iob"
        unfolding a = ((x,y),b) using True by auto
      moreover have "(map fst (takeWhile snd (a#iob))  LS M q) = (map fst (takeWhile snd iob)  LS M q')"
      proof -
        have *: "map fst (takeWhile snd (a#iob)) = (x,y)#(map fst (takeWhile snd iob))"
          using True unfolding a = ((x,y),b) by auto
        show ?thesis
          using Some
          unfolding * h_obs_Some[OF assms(1)]
          by (metis LS_prepend_transition assms(1) fst_conv mem_Collect_eq observable_language_transition_target singletonI snd_conv)  
      qed
      moreover have "(¬ list_all snd (a#iob)  map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob))  LS M q)
                      = (¬ list_all snd iob  map fst (take (Suc (length (takeWhile snd iob))) iob)  LS M q')"
      proof -
        have *: "map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob)) = (x,y)#(map fst (take (Suc (length (takeWhile snd iob))) iob))"
          using True unfolding a = ((x,y),b) by auto
        have **: "list_all snd (a#iob) = list_all snd iob"
          using True unfolding a = ((x,y),b) by auto
        show ?thesis
          using Some
          unfolding * ** h_obs_Some[OF assms(1)]
          by (metis LS_prepend_transition assms(1) fst_conv mem_Collect_eq observable_language_transition_target prod.sel(2) singletonI) 
      qed
      ultimately show ?thesis
        unfolding Cons.IH[OF h_obs_state[OF Some]] by simp
    qed
  next
    case False
    show ?thesis proof (cases "h_obs M q x y")
      case None
      then have "[(x,y)]  LS M q"
        unfolding h_obs_None[OF assms(1)] LS_single_transition by force
      then have "(¬ list_all snd (a#iob)  map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob))  LS M q)"
        unfolding a = ((x,y),b) using False by auto
      moreover have "(map fst (takeWhile snd (a#iob))  LS M q)"
        unfolding a = ((x,y),b) using False Cons.prems by auto
      moreover have "passes_test_case M q (a#iob) = True"
        unfolding a = ((x,y),b) using False None by auto
      ultimately show ?thesis 
        by simp
    next
      case (Some q')
      then have "[(x,y)]  LS M q"
        unfolding h_obs_Some[OF assms(1)] LS_single_transition by force
      then have "¬ (¬ list_all snd (a#iob)  map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob))  LS M q)"
        unfolding a = ((x,y),b) using False by auto
      moreover have "passes_test_case M q (a#iob) = False"
        unfolding a = ((x,y),b) using False Some by auto
      ultimately show ?thesis 
        by simp
    qed
  qed
qed


lemma test_suite_from_io_tree_finite_tree :
  assumes "observable M" 
  and     "qM  states M" 
  and     "finite_tree t"
shows "finite_tree (test_suite_from_io_tree M qM t)"
proof -
  have "finite (Prefix_Tree.set t  LS M qM)"
    using assms(3) unfolding finite_tree_iff by blast
  then have "finite (map (λx. (x, True)) ` (set t  LS M qM))"
    by blast

  have "((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) `
              {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM})
         ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` (set t))"
    by blast
  moreover have "finite ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` (set t))"
    using assms(3) unfolding finite_tree_iff by blast
  ultimately have "finite ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) `
              {xs @ [x] |xs x. xs  set t  LS M qM  xs @ [x]  set t - LS M qM})"
    using finite_subset by blast
  then show ?thesis
    using finite (map (λx. (x, True)) ` (set t  LS M qM))
    unfolding finite_tree_iff test_suite_from_io_tree_set[OF assms(1,2)]
    by blast
qed

    

lemma passes_test_case_prefix :
  assumes "observable M"
  and     "passes_test_case M q (iob@iob')"
shows "passes_test_case M q iob"
using assms(2) proof (induction iob arbitrary: q)
  case Nil
  then show ?case by auto
next
  case (Cons a iob)
  obtain x y b where "a = ((x,y),b)"
    by (metis prod.collapse)
  
  show ?case proof (cases b)
    case False
    then show ?thesis 
      using Cons.prems unfolding a = ((x,y),b) by auto
  next
    case True
    
    show ?thesis proof (cases "h_obs M q x y")
      case None
      then show ?thesis
        using Cons.prems unfolding a = ((x,y),b) by auto
    next
      case (Some q')
      then have "passes_test_case M q' (iob @ iob')"
        using True Cons.prems unfolding a = ((x,y),b) by auto
      then have "passes_test_case M q' iob"
        using Cons.IH by auto
      then show ?thesis 
        using True Some unfolding a = ((x,y),b) by auto
    qed
  qed
qed



lemma passes_test_cases_of_test_suite : 
  assumes "observable M" 
  and     "observable I"
  and     "qM  states M"
  and     "qI  states I"
  and     "finite_tree t"
shows "list_all (passes_test_case I qI) (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = passes_test_suite I qI (test_suite_from_io_tree M qM t)"
  (is "?P1 = ?P2")
proof 

  have "list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = 
          {y  Prefix_Tree.set (test_suite_from_io_tree M qM t). y'. y'  []  y @ y'  Prefix_Tree.set (test_suite_from_io_tree M qM t)}"
    using sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]] .

  show "?P1  ?P2"
  proof -
    assume ?P1
    show ?P2
      unfolding passes_test_suite_iff[OF assms(2,4)]
    proof 
      fix iob assume "iob  Prefix_Tree.set (test_suite_from_io_tree M qM t)"
      
      then obtain iob' where "iob@iob'  list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t))"
        unfolding sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]]
        using test_suite_from_io_tree_finite_tree[OF assms(1,3,5)] unfolding finite_tree_iff 
        using prefix_free_set_maximal_list_ob[of "set (test_suite_from_io_tree M qM t)"]
        by blast

      then have "passes_test_case I qI (iob@iob')"
        using ?P1
        by (metis in_set_conv_decomp_last list_all_append list_all_simps(1)) 
      then have "passes_test_case I qI iob"
        using passes_test_case_prefix[OF assms(2)] by auto
      then have "map fst (takeWhile snd iob)  LS I qI"
            and "(¬ list_all snd iob  map fst (take (Suc (length (takeWhile snd iob))) iob)  LS I qI)"
        unfolding passes_test_case_iff[OF assms(2,4)]
        by auto

      have "list_all snd iob  (map fst iob  LS I qI)"
        using map fst (takeWhile snd iob)  LS I qI
        by (metis in_set_conv_decomp_last list_all_append list_all_simps(1) takeWhile_eq_all_conv) 
      moreover have "(map fst iob  LS I qI)  list_all snd iob"
        using (¬ list_all snd iob  map fst (take (Suc (length (takeWhile snd iob))) iob)  LS I qI)
        by (metis append_take_drop_id language_prefix map_append) 
      ultimately show "(map fst iob  LS I qI) = list_all snd iob"
        by blast
    qed
  qed

  show "?P2  ?P1"
  proof -
    assume ?P2

    have " iob . iob  list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t))  passes_test_case I qI iob"
    proof -
      fix iob
      assume "iob  list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t))"
      then have "iob  set (test_suite_from_io_tree M qM t)"
        unfolding sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]]
        by blast
      then have *: "(map fst iob  LS I qI) = list_all snd iob"
        using ?P2 unfolding passes_test_suite_iff[OF assms(2,4)]
        by blast

      consider "iob  map (λx. (x, True)) ` (Prefix_Tree.set t  LS M qM)" |
               "iob  (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) `  {xs @ [x] |xs x. xs  Prefix_Tree.set t  LS M qM  xs @ [x]  Prefix_Tree.set t - LS M qM}"
        using iob  set (test_suite_from_io_tree M qM t)
        unfolding test_suite_from_io_tree_set[OF assms(1,3)]
        by blast
      then show "passes_test_case I qI iob" proof cases
        case 1
        then obtain io where "iob = map  (λx. (x, True)) io"
          by blast
        have "list_all snd iob" 
          unfolding iob = map  (λx. (x, True)) io by (induction io; auto)
        then have "(takeWhile snd iob) = iob"
          by (induction iob; auto)
        
        have "map fst (takeWhile snd iob)  LS I qI"
          using * list_all snd iob
          by (simp add: takeWhile snd iob = iob)
        then show ?thesis 
          unfolding passes_test_case_iff[OF assms(2,4)]
          using list_all snd iob
          by auto
      next
        case 2
        then obtain xs x where "iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (xs@[x])"
                           and "xs  set t  LS M qM" 
                           and "xs @ [x]  Prefix_Tree.set t - LS M qM"
          by blast
        then have **: "iob = (map (λx. (x, True)) xs) @ [(x,False)]"
          by auto

        have "isin (test_suite_from_io_tree M qM t) ((takeWhile snd iob)@(dropWhile snd iob))"
          using iob  set (test_suite_from_io_tree M qM t) by auto
        then have "(takeWhile snd iob)  set (test_suite_from_io_tree M qM t)"
          using isin_prefix[of "test_suite_from_io_tree M qM t" "takeWhile snd iob" "dropWhile snd iob"] by simp
        then have "(map fst (takeWhile snd iob)  LS I qI) = list_all snd (takeWhile snd iob)"
          using ?P2 unfolding passes_test_suite_iff[OF assms(2,4)]
          by blast
        moreover have "list_all snd (takeWhile snd iob)"
          by (induction iob; auto)
        ultimately have "map fst (takeWhile snd iob)  LS I qI"
          by simp
          
        have "¬ list_all snd iob"
          using ** by auto
        moreover have "(take (Suc (length (takeWhile snd iob))) iob) = iob"
          unfolding iob = (map (λx. (x, True)) xs) @ [(x,False)] by (induction xs; auto)
        ultimately have "map fst (take (Suc (length (takeWhile snd iob))) iob)  LS I qI"
          using * by simp
        
        then show ?thesis 
          using map fst (takeWhile snd iob)  LS I qI
          unfolding passes_test_case_iff[OF assms(2,4)]
          by simp
      qed  
    qed  
    then show ?P1
      using Ball_set_list_all by blast
  qed
qed

lemma passes_test_cases_from_io_tree : 
  assumes "observable M" 
  and     "observable I"
  and     "qM  states M"
  and     "qI  states I"
  and     "finite_tree t"
shows "list_all (passes_test_case I qI) (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = ((set t  LS M qM) = (set t  LS I qI))"
  unfolding passes_test_cases_of_test_suite[OF assms] passes_test_suite_from_io_tree[OF assms(1-4)]
  by blast



subsection ‹Alternative Representations›

subsubsection ‹Pass and Fail Traces›

type_synonym ('b,'c) pass_traces = "('b × 'c) list list"
type_synonym ('b,'c) fail_traces = "('b × 'c) list list"
type_synonym ('b,'c) trace_test_suite = "('b,'c) pass_traces × ('b,'c) fail_traces"

fun trace_test_suite_from_tree :: "('a::linorder,'b::linorder,'c::linorder) fsm  ('b × 'c) prefix_tree  ('b,'c) trace_test_suite" where
  "trace_test_suite_from_tree M T = (let
      (passes',fails) = separate_by (is_in_language M (initial M)) (sorted_list_of_sequences_in_tree T);
      passes = sorted_list_of_maximal_sequences_in_tree (from_list passes')
    in (passes, fails))"

lemma trace_test_suite_from_tree_language_equivalence :
  assumes "observable M" and "finite_tree T"
  shows "(L M  set T = L M'  set T) = (list.set (fst (trace_test_suite_from_tree M T))  L M'  L M'  list.set (snd (trace_test_suite_from_tree M T)) = {})"
proof -

  obtain passes' fails where *: "(passes',fails) = separate_by (is_in_language M (initial M)) (sorted_list_of_sequences_in_tree T)"
    by auto
  
  define passes where "passes = sorted_list_of_maximal_sequences_in_tree (from_list passes')"

  have "fst (trace_test_suite_from_tree M T) = passes"
    using "*" passes_def by auto
  have "snd (trace_test_suite_from_tree M T) = fails"
    using "*" passes_def by auto

  have "list.set passes' = L M  set T"
    using * sorted_list_of_sequences_in_tree_set[OF assms(2)]
    unfolding separate_by.simps 
    unfolding is_in_language_iff[OF assms(1) fsm_initial]
    by (metis inter_set_filter old.prod.inject) 
  moreover have "list.set passes'  L M' = (list.set passes  L M')"
  proof -

    have " io . io  list.set passes - {[]}   io' . io@io'  list.set passes'"
      unfolding passes_def
      unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree]
      unfolding from_list_set by force
    moreover have "[]  list.set passes'"
      unfolding list.set passes' = L M  set T by auto
    ultimately have " io . io  list.set passes   io' . io@io'  list.set passes'"
      by force
    moreover have " io . io  list.set passes'   io' . io@io'  list.set passes"
    proof -
      have " io . io  list.set passes'  io  set (from_list passes')"
        unfolding from_list_set by auto
      moreover have " io. io  set (from_list passes')   io' . io@io'  list.set passes"
        unfolding passes_def
        unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree]
        using from_list_finite_tree sorted_list_of_maximal_sequences_in_tree_ob sorted_list_of_maximal_sequences_in_tree_set by fastforce 
      ultimately show " io . io  list.set passes'   io' . io@io'  list.set passes"
        by blast
    qed
    ultimately show ?thesis
      using language_prefix[of _ _ M' "initial M'"]
      by (meson subset_iff)
  qed
  moreover have "list.set fails = set T - L M"
    using * sorted_list_of_sequences_in_tree_set[OF assms(2)]
    unfolding separate_by.simps 
    unfolding is_in_language_iff[OF assms(1) fsm_initial]
    by (simp add: set_diff_eq)
  ultimately show ?thesis
    unfolding fst (trace_test_suite_from_tree M T) = passes
    unfolding snd (trace_test_suite_from_tree M T) = fails
    by blast
qed


subsubsection ‹Input Sequences›

fun test_suite_to_input_sequences :: "('b::linorder×'c::linorder) prefix_tree  'b list list" where
  "test_suite_to_input_sequences T = sorted_list_of_maximal_sequences_in_tree (from_list (map input_portion (sorted_list_of_maximal_sequences_in_tree T)))"

lemma test_suite_to_input_sequences_pass :
  fixes T :: "('b::linorder × 'c::linorder) prefix_tree"
  assumes "finite_tree T"
  and     "(L M = L M')  (L M  set T = L M'  set T)"
  shows "(L M = L M')  ({io  L M . ( xs  list.set (test_suite_to_input_sequences T) .  xs'  list.set (prefixes xs) . input_portion io = xs')}
                                          = {io  L M' . ( xs  list.set (test_suite_to_input_sequences T) .  xs'  list.set (prefixes xs) . input_portion io = xs')})"
proof -

  have *: " io :: ('b::linorder × 'c::linorder) list . 
              ( xs  list.set (test_suite_to_input_sequences T) .  xs'  list.set (prefixes xs) . input_portion io = xs') = (io'set T. map fst io = map fst io')"
  proof -
    fix io :: "('b::linorder × 'c::linorder) list"    

    have "(io'set T. map fst io = map fst io') = ( α  list.set (sorted_list_of_maximal_sequences_in_tree T) .  α'  list.set (prefixes α) . map fst io = map fst α')"
    proof 
      have *: " io' . io'set T  ( io''. io'@io''  list.set (sorted_list_of_maximal_sequences_in_tree T))"
        using sorted_list_of_maximal_sequences_in_tree_set[OF assms(1)]
        using assms(1) set_prefix sorted_list_of_maximal_sequences_in_tree_ob by fastforce 
      
      show "(io'set T. map fst io = map fst io')  ( α  list.set (sorted_list_of_maximal_sequences_in_tree T) .  α'  list.set (prefixes α) . map fst io = map fst α')"
        by (metis append_Nil2 assms(1) prefixes_prepend prefixes_set_Nil sorted_list_of_maximal_sequences_in_tree_ob) 
      show "αlist.set (sorted_list_of_maximal_sequences_in_tree T). α'list.set (prefixes α). map fst io = map fst α'  io'Prefix_Tree.set T. map fst io = map fst io'"
        by (metis "*" prefixes_set_ob)
    qed
    also have " = ( xs  list.set (map input_portion (sorted_list_of_maximal_sequences_in_tree T)) .  xs'  list.set (prefixes xs) . map fst io = xs')"
    proof -
      have *: "list.set (map input_portion (sorted_list_of_maximal_sequences_in_tree T)) = input_portion ` (list.set (sorted_list_of_maximal_sequences_in_tree T))"
        by auto
      have **: " (α :: ('b::linorder × 'c::linorder) list) . ( α'  list.set (prefixes α) . map fst io = map fst α') = ( xs'  list.set (prefixes (input_portion α)) . map fst io = xs')"
      proof 
        fix α :: "('b::linorder × 'c::linorder) list"
        show "α'list.set (prefixes α). map fst io = map fst α'  xs'list.set (prefixes (map fst α)). map fst io = xs'"
        proof -
          assume "α'list.set (prefixes α). map fst io = map fst α'"
          then obtain α' α'' where "α'@α'' = α" and "map fst io = map fst α'"
            unfolding prefixes_set by blast
          then show "xs'list.set (prefixes (map fst α)). map fst io = xs'"
            unfolding prefixes_set
            by auto
        qed
        show "xs'list.set (prefixes (map fst α)). map fst io = xs'  α'list.set (prefixes α). map fst io = map fst α'"
        proof - 
          assume "xs'list.set (prefixes (map fst α)). map fst io = xs'"
          then obtain xs' xs'' where "xs'@xs'' = (map fst α)" and "map fst io = xs'"
            unfolding prefixes_set by blast
          then have "map fst (take (length xs') α) = map fst io"
            by (metis xs'list.set (prefixes (map fst α)). map fst io = xs' prefixes_take_iff take_map)
          moreover have "(take (length xs') α)  list.set (prefixes α)"
            by (metis map fst io = xs' calculation length_map prefixes_take_iff) 
          ultimately show ?thesis
            by metis 
        qed
      qed
      show ?thesis 
        unfolding ** *
        by blast 
    qed
    also have " = ( xs  list.set (test_suite_to_input_sequences T) .  xs'  list.set (prefixes xs) . input_portion io = xs')"
    proof 
      show "xslist.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). xs'list.set (prefixes xs). map fst io = xs'  xslist.set (test_suite_to_input_sequences T). xs'list.set (prefixes xs). map fst io = xs'" 
      proof -
        assume "xslist.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). xs'list.set (prefixes xs). map fst io = xs'"
        then obtain xs' xs'' where "xs'@xs''  list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T))"
                               and "map fst io = xs'"
          unfolding prefixes_set by blast
        then have *:"xs'@xs''  set (from_list (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)))"
          unfolding from_list_set by blast

        show ?thesis 
          using sorted_list_of_maximal_sequences_in_tree_ob[OF from_list_finite_tree *] map fst io = xs'
          unfolding test_suite_to_input_sequences.simps
          by (metis append.assoc append_Nil2 prefixes_prepend prefixes_set_Nil) 
      qed
      show "xslist.set (test_suite_to_input_sequences T). xs'list.set (prefixes xs). map fst io = xs'  xslist.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). xs'list.set (prefixes xs). map fst io = xs'"
      proof -
        assume "xslist.set (test_suite_to_input_sequences T). xs'list.set (prefixes xs). map fst io = xs'"
        then obtain xs' xs'' where "xs'@xs''  list.set (test_suite_to_input_sequences T)"
                               and "map fst io = xs'"
          unfolding prefixes_set by blast
        then have "xs'@xs'' = []  ( xs''' . (xs'@xs'')@xs'''list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)))"
          unfolding test_suite_to_input_sequences.simps 
          unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree] 
          unfolding from_list_set
          by blast
        then obtain xs''' where "(xs'@xs'')@xs'''list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T))"
          by (metis Nil_is_append_conv map fst io = xs' append.left_neutral calculation list.simps(8) set_Nil)
        then show ?thesis 
          using map fst io = xs'
          by (metis append.assoc append.right_neutral prefixes_prepend prefixes_set_Nil) 
      qed
    qed
    finally show "( xs  list.set (test_suite_to_input_sequences T) .  xs'  list.set (prefixes xs) . input_portion io = xs') = (io'set T. map fst io = map fst io')"
      by presburger
  qed
            
  show ?thesis
    unfolding *
    using equivalence_io_relaxation[OF assms(2)] .
qed

lemma test_suite_to_input_sequences_pass_alt_def :
  fixes T :: "('b::linorder × 'c::linorder) prefix_tree"
  assumes "finite_tree T"
  and     "(L M = L M')  (L M  set T = L M'  set T)"
shows "(L M = L M')  ( xs  list.set (test_suite_to_input_sequences T)  .  xs'  list.set (prefixes xs) . {io  L M . input_portion io = xs'} = {io  L M' . input_portion io = xs'})"
  unfolding test_suite_to_input_sequences_pass[OF assms]
  by blast
  
end