Theory Backwards_Reachability_Analysis

section ‹Backwards Reachability Analysis›

text ‹This theory introduces function @{text "select_inputs"} which is used for the calculation of
      both state preambles and state separators.›


theory Backwards_Reachability_Analysis
imports "../FSM"
begin


text ‹Function @{text "select_inputs"} calculates an associative list that maps states to a single
      input each such that the FSM induced by this input selection is acyclic, single input and 
      whose only deadlock states (if any) are contained in @{text "stateSet"}.
      The following parameters are used: 
        1) transition function @{text "f"} (typically @{text "(h M)"} for some FSM @{text "M"})
        2) a source state @{text "q0"} (selection terminates as soon as this states is assigned some input)
        3) a list of inputs that may be assigned to states
        4) a list of states not yet taken (these are considered when searching for the next possible
          assignment)
        5) a set @{text "stateSet"} of all states that already have an input assigned to them by @{text "m"}
        6) an associative list @{text "m"} containing previously chosen assignments›

function select_inputs :: "(('a × 'b) ⇒ ('c × 'a) set) ⇒ 'a ⇒ 'b list ⇒ 'a list ⇒ 'a set ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where
  "select_inputs f q0 inputList [] stateSet m = (case find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList of 
      Some x ⇒ m@[(q0,x)] |
      None   ⇒ m)" |
  "select_inputs f q0 inputList (n#nL) stateSet m = 
    (case find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList of 
      Some x ⇒ m@[(q0,x)] |
      None   ⇒ (case find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList
          of None            ⇒ m |
             Some (q',x,stateList') ⇒ select_inputs f q0 inputList stateList' (insert q' stateSet) (m@[(q',x)])))"
  by pat_completeness auto
termination 
proof -
  {
    fix f :: "(('a × 'b) ⇒ ('c × 'a) set)"
    fix q0 :: 'a
    fix inputList :: "'b list"
    fix n :: 'a
    fix nL :: "'a list" 
    fix stateSet :: "'a set"
    fix m :: "('a × 'b) list" 
    fix qynL' q ynL' x nL'
    assume "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None"
       and "find_remove_2 (λq' x. f (q', x) ≠ {} ∧ (∀(y, q'')∈f (q', x). q'' ∈ stateSet)) (n # nL) inputList = Some qynL'"
       and "(q, ynL') = qynL'"
       and "(x, nL') = ynL'"
  
    then have *: "find_remove_2 (λq' x. f (q', x) ≠ {} ∧ (∀(y, q'')∈f (q', x). q'' ∈ stateSet)) (n # nL) inputList = Some (q,x,nL')"
      by auto
  
    have "q ∈ set (n # nL)"
    and  "nL' = remove1 q (n # nL)"
      using find_remove_2_set(2,6)[OF *] by simp+
  
    then have "length nL' < length (n # nL)"
      using remove1_length by metis
      
  
    then have "((f, q0, inputList, nL', insert q stateSet, m @ [(q, x)]), f, q0, inputList, n # nL, stateSet, m) 
                ∈ measure (λ(f, q0, iL, nL, nS, m). length nL)"
      by auto
  } 
  then show ?thesis 
    by (relation "measure (λ (f,q0,iL,nL,nS,m) . length nL)"; simp)
qed


lemma select_inputs_length :
  "length (select_inputs f q0 inputList stateList stateSet m) ≤ (length m) + Suc (length stateList)"
proof (induction "length stateList" arbitrary: stateList stateSet m)
  case 0
  then show ?case 
    by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
  case (Suc k)
  then obtain n nL where "stateList = n # nL"
    by (meson Suc_length_conv) 

  show ?case 
  proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
    case None
    then show ?thesis 
    proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
      case None
      then show ?thesis 
        using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None› 
        unfolding ‹stateList = n # nL› by auto
    next
      case (Some a)
      then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList 
                                            = Some (q',x,stateList')"
        unfolding ‹stateList = n # nL› by (metis prod_cases3)
      have "k = length stateList'"
        using find_remove_2_length[OF *] ‹Suc k = length stateList› 
        unfolding ‹stateList = n # nL›
        by simp
      show ?thesis 
        using Suc.hyps(1)[of stateList' "insert q' stateSet" "m@[(q',x)]", OF ‹k = length stateList'›] 
        unfolding ‹stateList = n # nL› select_inputs.simps None * find_remove_2_length[OF *]        
        by simp
    qed
  next
    case (Some a)
    then show ?thesis 
      unfolding ‹stateList = n # nL› by auto
  qed
qed


lemma select_inputs_length_min :
  "length (select_inputs f q0 inputList stateList stateSet m) ≥ (length m)"
proof (induction "length stateList" arbitrary: stateList stateSet m)
  case 0
  then show ?case 
    by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
  case (Suc k)
  then obtain n nL where "stateList = n # nL"
    by (meson Suc_length_conv) 

  show ?case 
  proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
    case None
    then show ?thesis 
    proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
      case None
      then show ?thesis using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None› 
        unfolding ‹stateList = n # nL› by auto
    next
      case (Some a)
      then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList 
                                              = Some (q',x,stateList')"
        unfolding ‹stateList = n # nL› by (metis prod_cases3)
      have "k = length stateList'"
        using find_remove_2_length[OF *] ‹Suc k = length stateList› 
        unfolding ‹stateList = n # nL›
        by simp
      show ?thesis 
        unfolding ‹stateList = n # nL› select_inputs.simps None * find_remove_2_length[OF *]
        using Suc.hyps(1)[of stateList' "m@[(q',x)]" "insert q' stateSet" , OF ‹k = length stateList'›]  
        by simp
    qed
  next
    case (Some a)
    then show ?thesis unfolding ‹stateList = n # nL› by auto
  qed
qed


lemma select_inputs_helper1 :
  "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = Some x 
    ⟹ (select_inputs f q0 iL nL nS m) = m@[(q0,x)]" 
  by (cases nL; auto)


lemma select_inputs_take :
  "take (length m) (select_inputs f q0 inputList stateList stateSet m) = m"
proof (induction "length stateList" arbitrary: stateList stateSet m)
  case 0
  then show ?case 
    by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
  case (Suc k)
  then obtain n nL where "stateList = n # nL"
    by (meson Suc_length_conv) 

  show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
    case None
    then show ?thesis 
    proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
      case None
      then show ?thesis using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None› 
        unfolding ‹stateList = n # nL› by auto
    next
      case (Some a)
      then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList 
                                            = Some (q',x,stateList')"
        unfolding ‹stateList = n # nL› 
        by (metis prod_cases3)
      have "k = length stateList'"
        using find_remove_2_length[OF *] ‹Suc k = length stateList› 
        unfolding ‹stateList = n # nL›
        by simp

      have **: "(select_inputs f q0 inputList stateList stateSet m) 
                  = select_inputs f q0 inputList stateList' (insert q' stateSet) (m @ [(q', x)])"
        unfolding ‹stateList = n # nL› select_inputs.simps None * 
        by simp
      show ?thesis
        unfolding ** 
        using Suc.hyps(1)[of stateList' "m@[(q',x)]" "insert q' stateSet" , OF ‹k = length stateList'›]  
        by (metis butlast_snoc butlast_take diff_Suc_1 length_append_singleton select_inputs_length_min) 
    qed
  next
    case (Some a)
    then show ?thesis unfolding ‹stateList = n # nL› by auto
  qed
qed


lemma select_inputs_take' :
  "take (length m) (select_inputs f q0 iL nL nS (m@m')) = m"
  using select_inputs_take
  by (metis (no_types, lifting) add_leE append_eq_append_conv select_inputs_length_min length_append 
        length_take min_absorb2 take_add)


lemma select_inputs_distinct :
  assumes "distinct (map fst m)"
  and     "set (map fst m) ⊆ nS"
  and     "q0 ∉ nS"
  and     "distinct nL"
  and     "q0 ∉ set nL"
  and     "set nL ∩ nS = {}"
  shows "distinct (map fst (select_inputs f q0 iL nL nS m))" 
using assms proof (induction "length nL" arbitrary: nL nS m)
  case 0
  then show ?case 
    by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL"; auto)
next
  case (Suc k)
  then obtain n nL'' where "nL = n # nL''"
    by (meson Suc_length_conv) 

  show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL")
    case None
    then show ?thesis 
    proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
      case None
      then have "(select_inputs f q0 iL nL nS m) = m"
        using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None› 
        unfolding ‹nL = n # nL''› by auto
      then show ?thesis 
        using Suc.prems by auto
    next
      case (Some a)
      then obtain q' x nL' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL 
                                      = Some (q',x,nL')"
        by (metis prod_cases3)

      have "k = length nL'"
        using find_remove_2_length[OF *] ‹Suc k = length nL› 
        by simp

      have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])" 
        using *
        unfolding  ‹nL = n # nL''› select_inputs.simps None 
        by auto

      have "q' ∈ set nL"
      and  "set nL' = set nL - {q'}"
      and  "distinct nL'"
        using find_remove_2_set[OF * ]  ‹distinct nL› by auto

      have "distinct (map fst (m@[(q',x)]))" 
        using ‹(set (map fst m)) ⊆ nS› ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)› 
        by auto
      have "q0 ∉ insert q' nS"
        using Suc.prems(3) Suc.prems(5) ‹q' ∈ set nL› by auto
      have "set (map fst (m@[(q',x)])) ⊆ insert q' nS" 
        using ‹(set (map fst m)) ⊆ nS› by auto
      have "(set (map fst (m@[(q',x)]))) ⊆ insert q' nS"
        using‹(set (map fst m)) ⊆ nS› by auto
      have "q0 ∉ set nL'"
        by (simp add: Suc.prems(5) ‹set nL' = set nL - {q'}›)
      have "set nL' ∩ insert q' nS = {}"
        using Suc.prems(6) ‹set nL' = set nL - {q'}› by auto

      show ?thesis 
        unfolding select_inputs.simps None *
        using Suc.hyps(1)[OF ‹k = length nL'› ‹distinct (map fst (m@[(q',x)]))›
                               ‹set (map fst (m@[(q',x)])) ⊆ insert q' nS›
                               ‹q0 ∉ insert q' nS›
                               ‹distinct nL'›
                               ‹q0 ∉ set nL'›
                               ‹set nL' ∩ insert q' nS = {}›]
        unfolding ‹select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])› 
        by assumption
    qed
  next
    case (Some a)
    then show ?thesis 
      using Suc ‹nL = n # nL''› by auto
  qed
qed


lemma select_inputs_index_properties : 
  assumes "i < length (select_inputs (h M) q0 iL nL nS m)"
  and     "i ≥ length m"
  and     "distinct (map fst m)"
  and     "nS = nS0 ∪ set (map fst m)"
  and     "q0 ∉ nS"
  and     "distinct nL"
  and     "q0 ∉ set nL"
  and     "set nL ∩ nS = {}"
shows "fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))" 
      "fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
      "snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL"
      "(∀ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx')"
      "(∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))"
      "(∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"
proof -
  have combined_props : 
    "fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))
      ∧ snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL
      ∧ fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0
      ∧ (∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))
      ∧ (∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"    
  using assms proof (induction "length nL" arbitrary: nL nS m)
    case 0
    show ?case proof (cases "find (λ x . (h M) (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q0,x) . (q'' ∈ nS))) iL")
      case None
      then have "(select_inputs (h M) q0 iL nL nS m) = m" using 0 by auto
      then have "False" using "0.prems"(1,2) by auto
      then show ?thesis by simp
    next
      case (Some x)
      have "(select_inputs (h M) q0 iL nL nS m) = m@[(q0,x)]" using select_inputs_helper1[OF Some] by assumption
      then have "(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)" using "0.prems"(1,2)
        using antisym by fastforce 
  
      have "fst (q0, x) ∈ insert q0 (set nL)" by auto
      moreover have "snd (q0, x) ∈ set iL" using find_set[OF Some] by auto
      moreover have "fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
        using ‹select_inputs (h M) q0 iL nL nS m ! i = (q0, x)› assms(4) assms(5) by auto
       
      moreover have "(∃t∈FSM.transitions M. t_source t = fst (q0, x) ∧ t_input t = snd (q0, x))"
        using find_condition[OF Some] unfolding fst_conv snd_conv h.simps
        by fastforce 
      moreover have "⋀ t . t ∈ FSM.transitions M ⟹
          t_source t = fst (q0, x) ⟹ t_input t = snd (q0, x) ⟹
          t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"   
      proof -
        fix t assume "t ∈ FSM.transitions M" "t_source t = fst (q0, x)" "t_input t = snd (q0, x)"
        then have "t_target t ∈ nS"
          using find_condition[OF Some] unfolding h.simps fst_conv snd_conv
          by (metis (no_types, lifting) case_prod_beta' h_simps mem_Collect_eq prod.collapse)
        then show "t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
          using ‹nS = nS0 ∪ set (map fst m)›
          using "0.prems"(1) "0.prems"(2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by fastforce    
      qed
        
      ultimately show ?thesis 
        unfolding ‹(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)› by blast
    qed
  next
    case (Suc k)
    then obtain n nL'' where "nL = n # nL''"
      by (meson Suc_length_conv) 

    show ?case proof (cases "find (λ x . (h M) (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q0,x) . (q'' ∈ nS))) iL")
      case None
      show ?thesis proof (cases "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS))) nL iL")
        case None
        then have "(select_inputs (h M) q0 iL nL nS m) = m" using ‹find (λx. h M (q0, x) ≠ {} ∧ (∀(y, q'')∈h M (q0, x). q'' ∈ nS)) iL = None› ‹nL = n # nL''› by auto
        then have "False" using Suc.prems(1,2) by auto
        then show ?thesis by simp
      next
        case (Some a)
        then obtain q' x nL' where **: "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
          by (metis prod_cases3)

        have "k = length nL'"
          using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

        have "select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m @ [(q', x)])" 
          using **
          unfolding  ‹nL = n # nL''› select_inputs.simps None by auto
        then have "i < length (select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)]))"
          using Suc.prems(1) by auto

        have "(set (map fst (m @ [(q', x)]))) ⊆ insert q' nS"
          using Suc.prems(4) by auto

        have "q' ∈ set nL"
        and  "set nL' = set nL - {q'}"
        and  "distinct nL'"
          using find_remove_2_set[OF ** ]  ‹distinct nL› by auto
        have "set nL' ⊆ set nL"
          using find_remove_2_set(4)[OF ** ‹distinct nL›] by blast

        have "distinct (map fst (m @ [(q', x)]))" 
          using Suc.prems(4) ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)› by auto
        have "distinct (map fst (m@[(q',x)]))" 
          using Suc.prems(4) ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)› by auto
        have "q0 ∉ insert q' nS"
          using Suc.prems(7) Suc.prems(5) ‹q' ∈ set nL› by auto
        have "insert q' nS = nS0 ∪ set (map fst (m@[(q',x)]))" 
          using Suc.prems(4) by auto
        have "q0 ∉ set nL'"
          by (metis Suc.prems(7) ‹set nL' ⊆ set nL› subset_code(1))
        have "set nL' ∩ insert q' nS = {}"
          using Suc.prems(8) ‹set nL' = set nL - {q'}› by auto


        show ?thesis proof (cases "length (m @ [(q', x)]) ≤ i")
          case True

          show ?thesis
            using Suc.hyps(1)[OF ‹k = length nL'› ‹i < length (select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)]))›
                            True
                            ‹distinct (map fst (m @ [(q', x)]))›
                            ‹insert q' nS = nS0 ∪ set (map fst (m@[(q',x)]))›
                            ‹q0 ∉ insert q' nS›
                            ‹distinct nL'›
                            ‹q0 ∉ set nL'›
                            ‹set nL' ∩ insert q' nS = {}› ]
            unfolding ‹select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)])› 
            using ‹set nL' ⊆ set nL› by blast
        next
          case False 
          then have "i = length m"
            using Suc.prems(2) by auto
          then have ***: "select_inputs (h M) q0 iL nL nS m ! i = (q',x)"
            unfolding ‹select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)])› 
            using select_inputs_take
            by (metis length_append_singleton lessI nth_append_length nth_take) 
            
          
          have "q' ∈ insert q0 (set nL)"
            by (simp add: ‹q' ∈ set nL›) 
          moreover have "x ∈ set iL"
            using find_remove_2_set(3)[OF ** ] by auto
          moreover have "q' ∉ nS0"
            using Suc.prems(4) Suc.prems(8) ‹q' ∈ set nL› by blast
          moreover have "(∃t∈FSM.transitions M. t_source t = q' ∧ t_input t = x) "
            using find_remove_2_set(1)[OF ** ] unfolding h.simps by force
          moreover have "(∀t∈FSM.transitions M. t_source t = q' ∧ t_input t = x ⟶ t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t))"
            unfolding ‹i = length m› select_inputs_take 
            using find_remove_2_set(1)[OF ** ] unfolding h.simps ‹nS = nS0 ∪ (set (map fst m))› by force
          ultimately show ?thesis 
            unfolding *** fst_conv snd_conv by blast
        qed 
      qed
    next
      case (Some x)
      have "(select_inputs (h M) q0 iL nL nS m) = m@[(q0,x)]" using select_inputs_helper1[OF Some] by assumption
      then have "(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)" using Suc.prems(1,2)
        using antisym by fastforce 
  
      have "fst (q0, x) ∈ insert q0 (set nL)" by auto
      moreover have "snd (q0, x) ∈ set iL" using find_set[OF Some] by auto
      moreover have "fst (q0, x) ∉ nS0"
        using assms(4) assms(5) by auto 
      moreover have "⋀ qx' . qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) - set (take (length m) (select_inputs (h M) q0 iL nL nS m)) ⟹ fst (q0, x) ≠ fst qx'"
        using Suc.prems(1,2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by auto
      moreover have "(∃t∈FSM.transitions M. t_source t = fst (q0, x) ∧ t_input t = snd (q0, x))"
        using find_condition[OF Some] unfolding fst_conv snd_conv h.simps
        by fastforce 
      moreover have "⋀ t . t ∈ FSM.transitions M ⟹
          t_source t = fst (q0, x) ⟹ t_input t = snd (q0, x) ⟹
          t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"   
      proof -
        fix t assume "t ∈ FSM.transitions M" "t_source t = fst (q0, x)" "t_input t = snd (q0, x)"
        then have "t_target t ∈ nS"
          using find_condition[OF Some] unfolding h.simps fst_conv snd_conv
          by (metis (no_types, lifting) case_prod_beta' h_simps mem_Collect_eq prod.collapse) 
        then show "t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
          using ‹nS = nS0 ∪ (set (map fst m))›
          using Suc.prems(1,2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by fastforce    
      qed
        
      ultimately show ?thesis 
        unfolding ‹(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)› by blast
    qed
  qed

  then show "fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))"
            "snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL"
            "fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
            "(∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))"
            "(∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"
    by blast+

  show "(∀ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx')" 
  proof 
    fix qx' assume "qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m))"
    then obtain j where "(take i (select_inputs (h M) q0 iL nL nS m)) ! j = qx'" and "j < length (take i (select_inputs (h M) q0 iL nL nS m))"
      by (meson in_set_conv_nth)
    then have "fst qx' = (map fst (select_inputs (h M) q0 iL nL nS m)) ! j" and "j < length (select_inputs (h M) q0 iL nL nS m)" by auto
      
    moreover have "fst (select_inputs (h M) q0 iL nL nS m ! i) = (map fst (select_inputs (h M) q0 iL nL nS m)) ! i"
      using assms(1) by auto

    moreover have "j ≠ i" 
      using ‹j < length (take i (select_inputs (h M) q0 iL nL nS m))› by auto

    moreover have "set (map fst m) ⊆ nS"
      using ‹nS = nS0 ∪ set (map fst m)› by blast

    ultimately show "fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx'"
      using assms(1)
      using select_inputs_distinct[OF ‹distinct (map fst m)› _ ‹q0 ∉ nS› ‹distinct nL› ‹q0 ∉ set nL› ‹set nL ∩ nS = {}›]
      by (metis distinct_Ex1 in_set_conv_nth length_map)
  qed
qed 


lemma select_inputs_initial :
  assumes "qx ∈ set (select_inputs f q0 iL nL nS m) - set m"
  and     "fst qx = q0"
  shows "(last (select_inputs f q0 iL nL nS m)) = qx"
using assms(1) proof (induction "length nL" arbitrary: nS nL m)
  case 0
  then have "nL = []" by auto

  have "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL ≠ None" 
    using 0 unfolding ‹nL = []› select_inputs.simps 
    by (metis Diff_cancel empty_iff option.simps(4))
  then obtain x where *: "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = Some x" 
    by auto
  
  have "set (select_inputs f q0 iL nL nS m) - set m = {qx}"
    using "0.prems"(1) unfolding select_inputs_helper1[OF *]
    by auto 
  
  then show ?case unfolding select_inputs_helper1[OF *]
    by (metis DiffD1 DiffD2 UnE empty_iff empty_set insert_iff last_snoc list.simps(15) set_append) 
next
  case (Suc k)
  then obtain n nL'' where "nL = n # nL''"
    by (meson Suc_length_conv) 

  show ?case proof (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL")
    case None
    show ?thesis proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
      case None
      have "(select_inputs f q0 iL nL nS m) = m"
        using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None› None ‹nL = n # nL''› by auto
      then have "False" 
        using Suc.prems(1)
        by simp
      then show ?thesis by simp
    next
      case (Some a)
      then obtain q' x nL' where **: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
        by (metis prod_cases3)

      have "k = length nL'"
        using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

      have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])" 
        using **
        unfolding  ‹nL = n # nL''› select_inputs.simps None by auto
      then have "qx ∈ set (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) - set m"
        using Suc.prems by auto
      moreover have "q0 ≠ q'"
        using None unfolding find_None_iff
        using find_remove_2_set(1,2,3)[OF **]
        by blast
      ultimately have "qx ∈ set (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) - set (m@[(q',x)])"
        using ‹fst qx = q0› by auto
      then show ?thesis 
        using Suc.hyps unfolding ‹(select_inputs f q0 iL nL nS m) = (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)]))›
        using ‹k = length nL'› by blast 
    qed
  next
    case (Some a)

    have "set (select_inputs f q0 iL nL nS m ) - set m = {qx}"
      using Suc.prems(1) unfolding select_inputs_helper1[OF Some]
      by auto 
    
    then show ?thesis unfolding select_inputs_helper1[OF Some]
      by (metis DiffD1 DiffD2 UnE empty_iff empty_set insert_iff last_snoc list.simps(15) set_append)
  qed 
qed


lemma select_inputs_max_length :
  assumes "distinct nL"
  shows "length (select_inputs f q0 iL nL nS m) ≤ length m + Suc (length nL)" 
using assms proof (induction "length nL" arbitrary: nL nS m)
  case 0
  then show ?case by (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL"; auto)
next
  case (Suc k)
  then obtain n nL'' where "nL = n # nL''"
    by (meson Suc_length_conv) 

  show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL")
    case None
    show ?thesis proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
      case None
      show ?thesis unfolding ‹nL = n # nL''› select_inputs.simps None ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None›
        using None ‹nL = n # nL''› by auto 
    next
      case (Some a)
      then obtain q' x nL' where **: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
        by (metis prod_cases3)
      have "k = length nL'"
        using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

      have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])" 
        using **
        unfolding  ‹nL = n # nL''› select_inputs.simps None by auto
      
      have "length nL = Suc (length nL') ∧ distinct nL'"
        using find_remove_2_set(2,4,5)[OF **] ‹distinct nL›
        by (metis One_nat_def Suc_pred distinct_card distinct_remove1 equals0D length_greater_0_conv length_remove1 set_empty2 set_remove1_eq) 
      then have "length (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) ≤ length m + Suc (length nL)"
        using Suc.hyps(1)[OF ‹k = length nL'›]
        by (metis add_Suc_shift length_append_singleton)
      then show ?thesis 
        using ‹(select_inputs f q0 iL nL nS m) = select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])› by simp
    qed
  next
    case (Some a)
    show ?thesis unfolding select_inputs_helper1[OF Some] by auto 
  qed
qed


lemma select_inputs_q0_containment :
  assumes "f (q0,x) ≠ {}"
  and     "(∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))"   
  and     "x ∈ set iL"
shows "(∃ qx ∈ set (select_inputs f q0 iL nL nS m) . fst qx = q0)" 
proof -
  have "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL ≠ None"
    using assms unfolding find_None_iff by blast
  then obtain x' where *: "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL = Some x'"
    by auto
  show ?thesis 
    unfolding select_inputs_helper1[OF *] by auto
qed


lemma select_inputs_from_submachine :
  assumes "single_input S"
  and     "acyclic S"
  and     "is_submachine S M"
  and     "⋀ q x . q ∈ reachable_states S ⟹ h S (q,x) ≠ {} ⟹ h S (q,x) = h M (q,x)"
  and     "⋀ q . q ∈ reachable_states S ⟹ deadlock_state S q ⟹ q ∈ nS0 ∪ set (map fst m)" 
  and     "states M = insert (initial S) (set nL ∪ nS0 ∪ set (map fst m))"
  and     "(initial S) ∉ (set nL ∪ nS0 ∪ set (map fst m))"
shows "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S)"
and   "length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
proof -
  have "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S) ∧ length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
  using assms(5,6,7) proof (induction "length nL" arbitrary: nL m)
    case 0
    then have "nL = []" by auto
  
    have "¬ (deadlock_state S (initial S))"
      using assms(5,6,3,7) reachable_states_initial by blast 
    then obtain x where "x ∈ set (inputs_as_list M)" and "h S ((initial S),x) ≠ {}"
      using assms(3) unfolding deadlock_state.simps h.simps inputs_as_list_set 
      by fastforce 
    
    then have "h M ((initial S),x) ≠ {}"
      using assms(4)[OF reachable_states_initial]  by fastforce 
    
  
    have "(initial S) ∈ reachable_states M"
      using assms(3) reachable_states_initial by auto
      
    then have "(initial S) ∈ states M"
      using reachable_state_is_state by force
    
  
    have "⋀ y q'' . (y,q'') ∈ h M ((initial S),x) ⟹ q'' ∈ (nS0 ∪ set (map fst m))"
    proof -
      fix y q'' assume "(y,q'') ∈ h M ((initial S),x)"
      then have "q'' ∈ reachable_states M" using fsm_transition_target unfolding h.simps
        using ‹FSM.initial S ∈ reachable_states M› reachable_states_next by fastforce    
      then have "q'' ∈ insert (initial S) (nS0 ∪ set (map fst m))" using "0.prems"(2) ‹nL = []›
        using reachable_state_is_state by force
      moreover have "q'' ≠ (initial S)"
        using acyclic_no_self_loop[OF ‹acyclic S› reachable_states_initial]
        using ‹(y,q'') ∈ h M ((initial S),x)› assms(4)[OF reachable_states_initial ‹h S ((initial S),x) ≠ {}›] unfolding h_simps
        by blast 
      ultimately show "q'' ∈ (nS0 ∪ set (map fst m))" by blast
    qed
    then have "x ∈ set (inputs_as_list M) ∧ h M ((initial S), x) ≠ {} ∧ (∀(y, q'')∈h M ((initial S), x). q'' ∈ nS0 ∪ set (map fst m))"
      using ‹x ∈ set (inputs_as_list M) › ‹h M ((initial S), x) ≠ {}› by blast
    then have "find (λ x . (h M) ((initial S),x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) ((initial S),x) . (q'' ∈ (nS0 ∪ set (map fst m))))) (inputs_as_list M) ≠ None"
      unfolding find_None_iff by blast
    then show ?case
      unfolding ‹nL = []› select_inputs.simps by auto
  next
    case (Suc k)
    then obtain n nL'' where "nL = n # nL''"
      by (meson Suc_length_conv) 
  
  
    have "∃ q x . q ∈ reachable_states S - (nS0 ∪ set (map fst m)) ∧ h M (q,x) ≠ {} ∧ (∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))"
    proof -
      define ndlps where ndlps_def: "ndlps = {p . path S (initial S) p ∧ target (initial S) p ∉ (nS0 ∪ set (map fst m))}"
  
      have "path S (initial S) [] ∧ target (initial S) [] ∉ (nS0 ∪ set (map fst m))"
        using Suc.prems(3) by auto
      then have "[] ∈ ndlps"
        unfolding ndlps_def by blast
      then have "ndlps ≠ {}" by auto
      moreover have "finite ndlps"
        using acyclic_finite_paths_from_reachable_state[OF ‹acyclic S›, of "[]"] unfolding ndlps_def by fastforce
      ultimately have "∃ p ∈ ndlps . ∀ p' ∈ ndlps . length p' ≤ length p"
        by (meson max_length_elem not_le_imp_less) 
      then obtain p where "path S (initial S) p"
                          and "target (initial S) p ∉ (nS0 ∪ set (map fst m))"
                          and "⋀ p' . path S (initial S) p' ⟹ target (initial S) p' ∉ (nS0 ∪ set (map fst m)) ⟹ length p' ≤ length p"
        unfolding ndlps_def by blast
      
  
      let ?q = "target (initial S) p"
      have "¬ deadlock_state S ?q"
        using Suc.prems(1) reachable_states_intro[OF ‹path S (initial S) p›] using ‹?q ∉ (nS0 ∪ set (map fst m))› by blast
      then obtain x where "h S (?q,x) ≠ {}"
        unfolding deadlock_state.simps h.simps by fastforce
      then have "h M (?q,x) ≠ {}"
        using assms(4)[of ?q _] reachable_states_intro[OF ‹path S (initial S) p›]
        by blast      
  
      moreover have "⋀ y q'' . (y,q'') ∈ h M (?q,x) ⟹ q'' ∈ (nS0 ∪ set (map fst m))"
      proof (rule ccontr)
        fix y q'' assume "(y,q'') ∈ h M (?q,x)" and "q'' ∉ nS0 ∪ set (map fst m)"
        then have "(?q,x,y,q'') ∈ transitions S"
          using assms(4)[OF reachable_states_intro[OF ‹path S (initial S) p›] ‹h S (?q,x) ≠ {}›] unfolding h_simps
          by blast 
        then have "path S (initial S) (p@[(?q,x,y,q'')])"
          using ‹path S (initial S) p› by (simp add: path_append_transition)
        moreover have "target (initial S) (p@[(?q,x,y,q'')]) ∉ (nS0 ∪ set (map fst m))"
          using ‹q'' ∉ nS0 ∪ set (map fst m)› by auto
        ultimately show "False"
          using ‹⋀ p' . path S (initial S) p' ⟹ target (initial S) p' ∉ (nS0 ∪ set (map fst m)) ⟹ length p' ≤ length p›[of "(p@[(?q,x,y,q'')])"] by simp
      qed
  
      moreover have "?q ∈ reachable_states S - (nS0 ∪ set (map fst m))"
        using  ‹?q ∉ (nS0 ∪ set (map fst m))› ‹path S (initial S) p›  by blast
      
      ultimately show ?thesis by blast
    qed
    
    then obtain q x where "q ∈ reachable_states S" and "q ∉ (nS0 ∪ set (map fst m))" and "h M (q,x) ≠ {}" and "(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))"
      by blast
    then have "x ∈ set (inputs_as_list M)"
      unfolding h.simps using fsm_transition_input inputs_as_list_set by fastforce 
  
    
  
    show ?case proof (cases "q = initial S")
      case True
      have "find (λx. h M (FSM.initial S, x) ≠ {} ∧ (∀(y, q'')∈h M (FSM.initial S, x). q'' ∈ nS0 ∪ set (map fst m))) (inputs_as_list M) ≠ None"
        using ‹h M (q,x) ≠ {}› ‹(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))› ‹x ∈ set (inputs_as_list M)›
        unfolding True find_None_iff by blast
      then show ?thesis unfolding ‹nL = n # nL''› by auto
    next
      case False
      then have "q ∈ set nL" 
        using submachine_reachable_subset[OF ‹is_submachine S M›]
        unfolding is_submachine.simps ‹states M = insert (initial S) (set nL ∪ nS0 ∪ set (map fst m))›
        using ‹q ∈ reachable_states S›  ‹q ∉ (nS0 ∪ set (map fst m))›
        by (metis (no_types, lifting) Suc.prems(2) UnE insertE reachable_state_is_state subsetD sup_assoc) 
        
  
      
      show ?thesis proof (cases "find (λx. h M (FSM.initial S, x) ≠ {} ∧ (∀(y, q'')∈h M (FSM.initial S, x). q'' ∈ nS0 ∪ set (map fst m))) (inputs_as_list M)")
        case None
        
  
        have "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS0 ∪ set (map fst m)))) (nL) (inputs_as_list M) ≠ None"
          using ‹q ∈ set nL› ‹h M (q,x) ≠ {}› ‹(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))› ‹x ∈ set (inputs_as_list M)›
          unfolding find_remove_2_None_iff ‹nL = n # nL''›
          by blast 
        then obtain q' x' nL' where *: "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS0 ∪ set (map fst m)))) (n#nL'') (inputs_as_list M) = Some (q',x',nL')"
          unfolding ‹nL = n # nL''› by auto
        have "k = length nL'"
          using find_remove_2_length[OF *] ‹Suc k = length nL›  ‹nL = n # nL''› by simp
  
        have **: "select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m
                  = select_inputs (h M) (initial S) (inputs_as_list M) nL' (nS0 ∪ set (map fst (m@[(q',x')]))) (m@[(q',x')])"
          unfolding ‹nL = n # nL''› select_inputs.simps None * by auto
  
        have p1: "(⋀q. q ∈ reachable_states S ⟹ deadlock_state S q ⟹ q ∈ nS0 ∪ set (map fst (m@[(q',x')])))"
          using Suc.prems(1) by fastforce
  
        have "set nL = insert q' (set nL')" using find_remove_2_set(2,6)[OF *] unfolding ‹nL = n # nL''› by auto
        then have "(set nL ∪ set (map fst m)) = (set nL' ∪ set (map fst (m @ [(q', x')])))" by auto
        then have p2: "states M = insert (initial S) (set nL' ∪ nS0 ∪ set (map fst (m @ [(q', x')])))" 
          using Suc.prems(2) by auto
  
        have p3: "initial S ∉ set nL' ∪ nS0 ∪ set (map fst (m @ [(q', x')]))"
          using Suc.prems(3) False ‹set nL = insert q' (set nL')› by auto
  
        show ?thesis unfolding **
          using Suc.hyps(1)[OF ‹k = length nL'› p1 p2 p3] by blast
      next
        case (Some a)
        then show ?thesis unfolding ‹nL = n # nL''› by auto
      qed
    qed
  qed
  then show "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S)"
       and  "length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
    by blast+
qed


end