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 ⟹ ∀iob∈Prefix_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 "∀iob∈Prefix_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 ‹∀iob∈Prefix_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 "∀iob∈Prefix_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) = (∀iob∈set 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 "∀iob∈Prefix_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 "∀iob∈Prefix_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 ⟹ ∀iob∈set 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 "∃xs∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). ∃xs'∈list.set (prefixes xs). map fst io = xs' ⟹ ∃xs∈list.set (test_suite_to_input_sequences T). ∃xs'∈list.set (prefixes xs). map fst io = xs'" 
      proof -
        assume "∃xs∈list.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 "∃xs∈list.set (test_suite_to_input_sequences T). ∃xs'∈list.set (prefixes xs). map fst io = xs' ⟹ ∃xs∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). ∃xs'∈list.set (prefixes xs). map fst io = xs'"
      proof -
        assume "∃xs∈list.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