Theory FSM

section ‹Finite State Machines›

text ‹This theory defines well-formed finite state machines and introduces various closely related 
      notions, as well as a selection of basic properties and definitions.›

theory FSM
  imports FSM_Impl "HOL-Library.Quotient_Type" "HOL-Library.Product_Lexorder"
begin


subsection ‹Well-formed Finite State Machines›

text ‹A value of type @{text "fsm_impl"} constitutes a well-formed FSM if its contained sets are 
      finite and the initial state and the components of each transition are contained in their 
      respective sets.›

abbreviation(input) "well_formed_fsm (M :: ('state, 'input, 'output) fsm_impl) 
      (initial M  states M
       finite (states M)
       finite (inputs M)
       finite (outputs M)
       finite (transitions M)
       ( t  transitions M . t_source t  states M  
                                t_input t  inputs M  
                                t_target t  states M  
                                t_output t  outputs M)) " 

typedef ('state, 'input, 'output) fsm = 
  "{ M :: ('state, 'input, 'output) fsm_impl . well_formed_fsm M}"
  morphisms fsm_impl_of_fsm Abs_fsm 
proof -
  obtain q :: 'state where "True" by blast
  have "well_formed_fsm (FSMI q {q} {} {} {})" by auto
  then show ?thesis by blast
qed


setup_lifting type_definition_fsm

lift_definition initial :: "('state, 'input, 'output) fsm  'state" is FSM_Impl.initial done
lift_definition states :: "('state, 'input, 'output) fsm  'state set" is FSM_Impl.states done
lift_definition inputs :: "('state, 'input, 'output) fsm  'input set" is FSM_Impl.inputs done
lift_definition outputs :: "('state, 'input, 'output) fsm  'output set" is FSM_Impl.outputs done
lift_definition transitions :: 
  "('state, 'input, 'output) fsm  ('state × 'input × 'output × 'state) set" 
  is FSM_Impl.transitions done

lift_definition fsm_from_list :: "'a  ('a,'b,'c) transition list  ('a, 'b, 'c) fsm" 
  is FSM_Impl.fsm_impl_from_list 
proof -
  fix q  :: 'a 
  fix ts :: "('a,'b,'c) transition list"
  show "well_formed_fsm (fsm_impl_from_list q ts)" 
    by (induction ts; auto)
qed



lemma fsm_initial[intro]: "initial M  states M" 
  by (transfer; blast)
lemma fsm_states_finite: "finite (states M)" 
  by (transfer; blast)
lemma fsm_inputs_finite: "finite (inputs M)" 
  by (transfer; blast)
lemma fsm_outputs_finite: "finite (outputs M)" 
  by (transfer; blast)
lemma fsm_transitions_finite: "finite (transitions M)" 
  by (transfer; blast)
lemma fsm_transition_source[intro]: " t . t  (transitions M)  t_source t  states M" 
  by (transfer; blast)
lemma fsm_transition_target[intro]: " t . t  (transitions M)  t_target t  states M" 
  by (transfer; blast)
lemma fsm_transition_input[intro]: " t . t  (transitions M)  t_input t  inputs M" 
  by (transfer; blast)
lemma fsm_transition_output[intro]: " t . t  (transitions M)  t_output t  outputs M" 
  by (transfer; blast)


instantiation fsm :: (type,type,type) equal
begin                                  
definition equal_fsm :: "('a, 'b, 'c) fsm  ('a, 'b, 'c) fsm  bool" where
  "equal_fsm x y = (initial x = initial y  states x = states y  inputs x = inputs y  outputs x = outputs y  transitions x = transitions y)"

instance
  apply (intro_classes)
  unfolding equal_fsm_def 
  apply transfer
  using fsm_impl.expand by auto
end 



subsubsection ‹Example FSMs›


definition m_ex_H :: "(integer,integer,integer) fsm" where
  "m_ex_H = fsm_from_list 1 [ (1,0,0,2),
                              (1,0,1,4),
                              (1,1,1,4),
                              (2,0,0,2),
                              (2,1,1,4),
                              (3,0,1,4),
                              (3,1,0,1),
                              (3,1,1,3),
                              (4,0,0,3),
                              (4,1,0,1)]"


definition m_ex_9 :: "(integer,integer,integer) fsm" where
  "m_ex_9 = fsm_from_list 0 [ (0,0,2,2),
                              (0,0,3,2),
                              (0,1,0,3),
                              (0,1,1,3),
                              (1,0,3,2),
                              (1,1,1,3),
                              (2,0,2,2),
                              (2,1,3,3),
                              (3,0,2,2),
                              (3,1,0,2),
                              (3,1,1,1)]"

definition m_ex_DR :: "(integer,integer,integer) fsm" where
  "m_ex_DR = fsm_from_list 0  [(0,0,0,100),
                               (100,0,0,101), 
                               (100,0,1,101),
                               (101,0,0,102),
                               (101,0,1,102),
                               (102,0,0,103),
                               (102,0,1,103),
                               (103,0,0,104),
                               (103,0,1,104),
                               (104,0,0,100),
                               (104,0,1,100),
                               (104,1,0,400),
                               (0,0,2,200),
                               (200,0,2,201),
                               (201,0,2,202),
                               (202,0,2,203),
                               (203,0,2,200),
                               (203,1,0,400),
                               (0,1,0,300),
                               (100,1,0,300),
                               (101,1,0,300),
                               (102,1,0,300),
                               (103,1,0,300),
                               (200,1,0,300),
                               (201,1,0,300),
                               (202,1,0,300),
                               (300,0,0,300),
                               (300,1,0,300),
                               (400,0,0,300),
                               (400,1,0,300)]"


subsection ‹Transition Function h and related functions›

lift_definition h :: "('state, 'input, 'output) fsm  ('state × 'input)  ('output × 'state) set" 
  is FSM_Impl.h .

lemma h_simps[simp]: "FSM.h M (q,x) = { (y,q') . (q,x,y,q')  transitions M }"
  by (transfer; auto)

lift_definition h_obs :: "('state, 'input, 'output) fsm  'state  'input  'output  'state option" 
  is FSM_Impl.h_obs .

lemma h_obs_simps[simp]: "FSM.h_obs M q x y = (let 
      tgts = snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))
    in if card tgts = 1
      then Some (the_elem tgts)
      else None)"
  by (transfer; auto)

fun defined_inputs' :: "(('a ×'b)  ('c×'a) set)  'b set  'a  'b set" where
  "defined_inputs' hM iM q = {x  iM . hM (q,x)  {}}"

fun defined_inputs :: "('a,'b,'c) fsm  'a  'b set" where
  "defined_inputs M q = defined_inputs' (h M) (inputs M) q"

lemma defined_inputs_set : "defined_inputs M q = {x  inputs M . h M (q,x)  {} }"
  by auto

fun transitions_from' :: "(('a ×'b)  ('c×'a) set)  'b set  'a  ('a,'b,'c) transition set" where
  "transitions_from' hM iM q = (image (λx . image (λ(y,q') . (q,x,y,q')) (hM (q,x))) iM)"

fun transitions_from :: "('a,'b,'c) fsm  'a  ('a,'b,'c) transition set" where
  "transitions_from M q = transitions_from' (h M) (inputs M) q"


lemma transitions_from_set : 
  assumes "q  states M" 
  shows "transitions_from M q = {t  transitions M . t_source t = q}"
proof -
  have " t . t  transitions_from M q  t  transitions M  t_source t = q" by auto
  moreover have " t . t  transitions M  t_source t = q  t  transitions_from M q" 
  proof -
    fix t assume "t  transitions M" and "t_source t = q"
    then have "(t_output t, t_target t)  h M (q,t_input t)" and "t_input t  inputs M" by auto
    then have "t_input t  defined_inputs' (h M) (inputs M) q" 
      unfolding defined_inputs'.simps t_source t = q by blast

    have "(q, t_input t, t_output t, t_target t)  transitions M"
      using t_source t = q t  transitions M by auto
    then have "(q, t_input t, t_output t, t_target t)  (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)"
      using (t_output t, t_target t)  h M (q,t_input t)
      unfolding h.simps
      by (metis (no_types, lifting) image_iff prod.case_eq_if surjective_pairing)
    then have "t  (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)"
      using t_source t = q by (metis prod.collapse) 
    then show "t  transitions_from M q" 
       
      unfolding transitions_from.simps transitions_from'.simps 
      using t_input t  defined_inputs' (h M) (inputs M) q
      using t_input t  FSM.inputs M by blast
  qed
  ultimately show ?thesis by blast
qed


fun h_from :: "('state, 'input, 'output) fsm  'state  ('input × 'output × 'state) set" where
  "h_from M q = { (x,y,q') . (q,x,y,q')  transitions M }"


lemma h_from[code] : "h_from M q = (let m = set_as_map (transitions M) 
                                     in (case m q of Some yqs  yqs | None  {}))"
  unfolding set_as_map_def by force


fun h_out :: "('a,'b,'c) fsm  ('a × 'b)  'c set" where
  "h_out M (q,x) = {y .  q' . (q,x,y,q')  transitions M}"

lemma h_out_code[code]: 
  "h_out M = (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of 
                            Some yqs  yqs | 
                            None  {}))"
proof -
  

  let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs  yqs | None  {}))"
  
  have " qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs  yqs | None  {})) qx = (λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx"
    unfolding set_as_map_def by auto
  
  moreover have " qx . (λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx = (λ qx . {y | y .  q' . (fst qx, snd qx, y, q')  (transitions M)}) qx" 
    by force
    
  ultimately have "?f = (λ qx . {y | y .  q' . (fst qx, snd qx, y, q')  (transitions M)})" 
    by blast
  then have "?f = (λ (q,x) . {y | y .  q' . (q, x, y, q')  (transitions M)})" by force
  
  then show ?thesis by force 
qed

lemma h_out_alt_def : 
  "h_out M (q,x) = {t_output t | t . t  transitions M  t_source t = q  t_input t = x}"
  unfolding h_out.simps
  by auto


subsection ‹Size›

instantiation fsm  :: (type,type,type) size 
begin

definition size where [simp, code]: "size (m::('a, 'b, 'c) fsm) = card (states m)"

instance ..
end

lemma fsm_size_Suc :
  "size M > 0"
  unfolding FSM.size_def
  using fsm_states_finite[of M] fsm_initial[of M]
  using card_gt_0_iff by blast 


subsection ‹Paths›

inductive path :: "('state, 'input, 'output) fsm  'state  ('state, 'input, 'output) path  bool" 
  where
  nil[intro!] : "q  states M  path M q []" |
  cons[intro!] : "t  transitions M  path M (t_target t) ts  path M (t_source t) (t#ts)"

inductive_cases path_nil_elim[elim!]: "path M q []"
inductive_cases path_cons_elim[elim!]: "path M q (t#ts)"

fun visited_states :: "'state  ('state, 'input, 'output) path  'state list" where
  "visited_states q p = (q # map t_target p)"

fun target :: "'state  ('state, 'input, 'output) path  'state" where
  "target q p = last (visited_states q p)"

lemma target_nil [simp] : "target q [] = q" by auto
lemma target_snoc [simp] : "target q (p@[t]) = t_target t" by auto


lemma path_begin_state :
  assumes "path M q p"
  shows   "q  states M" 
  using assms by (cases; auto) 

lemma path_append[intro!] :
  assumes "path M q p1"
      and "path M (target q p1) p2"
  shows "path M q (p1@p2)"
  using assms by (induct p1 arbitrary: p2; auto) 

lemma path_target_is_state :
  assumes "path M q p"
  shows   "target q p  states M"
using assms by (induct p; auto)

lemma path_suffix :
  assumes "path M q (p1@p2)"
  shows "path M (target q p1) p2"
using assms by (induction p1 arbitrary: q; auto)

lemma path_prefix :
  assumes "path M q (p1@p2)"
  shows "path M q p1"
using assms by (induction p1 arbitrary: q; auto; (metis path_begin_state))

lemma path_append_elim[elim!] :
  assumes "path M q (p1@p2)"
  obtains "path M q p1"
      and "path M (target q p1) p2"
  by (meson assms path_prefix path_suffix)

lemma path_append_target:
  "target q (p1@p2) = target (target q p1) p2" 
  by (induction p1) (simp+)

lemma path_append_target_hd :
  assumes "length p > 0"
  shows "target q p = target (t_target (hd p)) (tl p)"
using assms by (induction p) (simp+)

lemma path_transitions :
  assumes "path M q p"
  shows "set p  transitions M"
  using assms by (induct p arbitrary: q; fastforce)

lemma path_append_transition[intro!] :
  assumes "path M q p"
  and     "t  transitions M"
  and     "t_source t = target q p" 
shows "path M q (p@[t])"
  by (metis assms(1) assms(2) assms(3) cons fsm_transition_target nil path_append)

lemma path_append_transition_elim[elim!] :
  assumes "path M q (p@[t])"
shows "path M q p"
and   "t  transitions M"
and   "t_source t = target q p" 
  using assms by auto

lemma path_prepend_t : "path M q' p  (q,x,y,q')  transitions M  path M q ((q,x,y,q')#p)" 
  by (metis (mono_tags, lifting) fst_conv path.intros(2) prod.sel(2)) 

lemma path_target_append : "target q1 p1 = q2  target q2 p2 = q3  target q1 (p1@p2) = q3" 
  by auto

lemma single_transition_path : "t  transitions M  path M (t_source t) [t]" by auto

lemma path_source_target_index :
  assumes "Suc i < length p"
  and     "path M q p"
shows "t_target (p ! i) = t_source (p ! (Suc i))"
  using assms proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc t ps)
  then have "path M q ps" and "t_source t = target q ps" and "t  transitions M" by auto
  
  show ?case proof (cases "Suc i < length ps")
    case True
    then have "t_target (ps ! i) = t_source (ps ! Suc i)" 
      using snoc.IH path M q ps by auto
    then show ?thesis
      by (simp add: Suc_lessD True nth_append) 
  next
    case False
    then have "Suc i = length ps"
      using snoc.prems(1) by auto
    then have "(ps @ [t]) ! Suc i = t"
      by auto

    show ?thesis proof (cases "ps = []")
      case True
      then show ?thesis using Suc i = length ps by auto
    next
      case False
      then have "target q ps = t_target (last ps)"
        unfolding target.simps visited_states.simps
        by (simp add: last_map) 
      then have "target q ps = t_target (ps ! i)"
        using Suc i = length ps
        by (metis False diff_Suc_1 last_conv_nth) 
      then show ?thesis 
        using t_source t = target q ps
        by (metis (ps @ [t]) ! Suc i = t Suc i = length ps lessI nth_append) 
    qed
  qed   
qed

lemma paths_finite : "finite { p . path M q p  length p  k }"
proof -
  have "{ p . path M q p  length p  k }  {xs . set xs  transitions M  length xs  k}"
    by (metis (no_types, lifting) Collect_mono path_transitions)     
  then show "finite { p . path M q p  length p  k }"
    using finite_lists_length_le[OF fsm_transitions_finite[of M], of k]
    by (metis (mono_tags) finite_subset) 
qed

lemma visited_states_prefix :
  assumes "q'  set (visited_states q p)"
  shows   " p1 p2 . p = p1@p2  target q p1 = q'"
using assms proof (induction p arbitrary: q)
  case Nil
  then show ?case by auto
next
  case (Cons a p)
  then show ?case 
  proof (cases "q'  set (visited_states (t_target a) p)")
    case True
    then obtain p1 p2 where "p = p1 @ p2  target (t_target a) p1 = q'"
      using Cons.IH by blast
    then have "(a#p) = (a#p1)@p2  target q (a#p1) = q'"
      by auto
    then show ?thesis by blast
  next
    case False
    then have "q' = q" 
      using Cons.prems by auto     
    then show ?thesis
      by auto 
  qed
qed 

lemma visited_states_are_states :
  assumes "path M q1 p"
  shows "set (visited_states q1 p)  states M" 
  by (metis assms path_prefix path_target_is_state subsetI visited_states_prefix) 
  
lemma transition_subset_path : 
  assumes "transitions A  transitions B"
  and "path A q p"
  and "q  states B"
shows "path B q p"
using assms(2) proof (induction p rule: rev_induct)
  case Nil
  show ?case using assms(3) by auto
next
  case (snoc t p)
  then show ?case using assms(1) path_suffix
    by fastforce   
qed

subsubsection ‹Paths of fixed length›

fun paths_of_length' :: "('a,'b,'c) path  'a  (('a ×'b)  ('c×'a) set)  'b set  nat  ('a,'b,'c) path set" 
  where
  "paths_of_length' prev q hM iM 0 = {prev}" |
  "paths_of_length' prev q hM iM (Suc k) = 
    (let hF = transitions_from' hM iM q
      in  (image (λ t . paths_of_length' (prev@[t]) (t_target t) hM iM k) hF))"

fun paths_of_length :: "('a,'b,'c) fsm  'a  nat  ('a,'b,'c) path set" where
  "paths_of_length M q k = paths_of_length' [] q (h M) (inputs M) k"



subsubsection ‹Paths up to fixed length›

fun paths_up_to_length' :: "('a,'b,'c) path  'a  (('a ×'b)  (('c×'a) set))  'b set  nat  ('a,'b,'c) path set" 
  where
  "paths_up_to_length' prev q hM iM 0 = {prev}" |
  "paths_up_to_length' prev q hM iM (Suc k) = 
    (let hF = transitions_from' hM iM q
      in insert prev ( (image (λ t . paths_up_to_length' (prev@[t]) (t_target t) hM iM k) hF)))"

fun paths_up_to_length :: "('a,'b,'c) fsm  'a  nat  ('a,'b,'c) path set" where
  "paths_up_to_length M q k = paths_up_to_length' [] q (h M) (inputs M) k"


lemma paths_up_to_length'_set :
  assumes "q  states M"
  and     "path M q prev"
shows "paths_up_to_length' prev (target q prev) (h M) (inputs M) k 
        = {(prev@p) | p . path M (target q prev) p  length p  k}"
using assms(2) proof (induction k arbitrary: prev)
  case 0
  show ?case unfolding paths_up_to_length'.simps using path_target_is_state[OF "0.prems"(1)] by auto
next
  case (Suc k)
  
  have " p . p  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k) 
           p  {(prev@p) | p . path M (target q prev) p  length p  Suc k}"
  proof -
    fix p assume "p  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)"
    then show "p  {(prev@p) | p . path M (target q prev) p  length p  Suc k}" 
    proof (cases "p = prev")
      case True
      show ?thesis using path_target_is_state[OF Suc.prems(1)] unfolding True by (simp add: nil) 
    next
      case False
      then have "p  ( (image (λt. paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k) 
                                (transitions_from' (h M) (inputs M) (target q prev))))"
        using p  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)
        unfolding paths_up_to_length'.simps Let_def by blast
      then obtain t where "t  (image (λx . image (λ(y,q') . ((target q prev),x,y,q')) 
                                                    (h M ((target q prev),x))) (inputs M))"
                    and   "p  paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k"
        unfolding transitions_from'.simps by blast

      have "t  transitions M" and "t_source t = (target q prev)"
        using t  (image (λx . image (λ(y,q') . ((target q prev),x,y,q')) 
                                        (h M ((target q prev),x))) (inputs M)) by auto
      then have "path M q (prev@[t])"
        using Suc.prems(1) using path_append_transition by simp

      have "(target q (prev @ [t])) = t_target t" by auto
      

      show ?thesis 
        using p  paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k
        using Suc.IH[OF path M q (prev@[t])] 
        unfolding (target q (prev @ [t])) = t_target t
        using path M q (prev @ [t]) by auto 
    qed
  qed

  moreover have " p . p  {(prev@p) | p . path M (target q prev) p  length p  Suc k} 
                   p  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)"
  proof -
    fix p assume "p  {(prev@p) | p . path M (target q prev) p  length p  Suc k}"
    then obtain p' where "p = prev@p'"
                   and   "path M (target q prev) p'" 
                   and   "length p'  Suc k"
      by blast

    have "prev@p'  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)"
    proof (cases p')
      case Nil
      then show ?thesis by auto
    next
      case (Cons t p'')

      then have "t  transitions M" and "t_source t = (target q prev)"
        using path M (target q prev) p' by auto
      then have "path M q (prev@[t])"
        using Suc.prems(1) using path_append_transition by simp
      
      have "(target q (prev @ [t])) = t_target t" by auto

      have "length p''  k" using length p'  Suc k Cons by auto
      moreover have "path M (target q (prev@[t])) p''"
        using path M (target q prev) p' unfolding Cons
        by auto
      ultimately have "p  paths_up_to_length' (prev @ [t]) (t_target t) (h M) (FSM.inputs M) k"
        using Suc.IH[OF path M q (prev@[t])] 
        unfolding (target q (prev @ [t])) = t_target t p = prev@p' Cons by simp
      then have "prev@t#p''  paths_up_to_length' (prev @ [t]) (t_target t) (h M) (FSM.inputs M) k"
        unfolding p = prev@p' Cons by auto

      have "t  (λ(y, q'). (t_source t, t_input t, y, q')) ` 
                              {(y, q'). (t_source t, t_input t, y, q')  FSM.transitions M}"
        using t  transitions M
        by (metis (no_types, lifting) case_prodI mem_Collect_eq pair_imageI surjective_pairing)  
      then have "t  transitions_from' (h M) (inputs M) (target q prev)"
        unfolding transitions_from'.simps 
        using fsm_transition_input[OF t  transitions M] 
        unfolding t_source t = (target q prev)[symmetric] h_simps 
        by blast

      then show ?thesis 
        using prev @ t # p''  paths_up_to_length' (prev@[t]) (t_target t) (h M) (FSM.inputs M) k 
        unfolding p = prev@p' Cons paths_up_to_length'.simps Let_def by blast
    qed
    then show "p  paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)"
      unfolding p = prev@p' by assumption
  qed

  ultimately show ?case by blast
qed


lemma paths_up_to_length_set :
  assumes "q  states M"
shows "paths_up_to_length M q k = {p . path M q p  length p  k}" 
  unfolding paths_up_to_length.simps 
  using paths_up_to_length'_set[OF assms nil[OF assms], of k]  by auto




subsubsection ‹Calculating Acyclic Paths›

fun acyclic_paths_up_to_length' :: "('a,'b,'c) path  'a  ('a   (('b×'c×'a) set))  'a set  nat  ('a,'b,'c) path set" 
  where
  "acyclic_paths_up_to_length' prev q hF visitedStates 0 = {prev}" |
  "acyclic_paths_up_to_length' prev q hF visitedStates (Suc k) = 
    (let tF = Set.filter (λ (x,y,q') . q'  visitedStates) (hF q)
      in (insert prev ( (image (λ (x,y,q') . acyclic_paths_up_to_length' (prev@[(q,x,y,q')]) q' hF (insert q' visitedStates) k) tF))))"


fun p_source :: "'a  ('a,'b,'c) path  'a"
  where "p_source q p = hd (visited_states q p)"

lemma acyclic_paths_up_to_length'_prev : 
  "p'  acyclic_paths_up_to_length' (prev@prev') q hF visitedStates k   p'' . p' = prev@p''" 
  by (induction k arbitrary: p' q visitedStates prev'; auto)

lemma acyclic_paths_up_to_length'_set :
  assumes "path M (p_source q prev) prev"
  and     " q' . hF q' = {(x,y,q'') | x y q'' . (q',x,y,q'')  transitions M}"
  and     "distinct (visited_states (p_source q prev) prev)"
  and     "visitedStates = set (visited_states (p_source q prev) prev)"
shows "acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates k 
        = { prev@p | p . path M (p_source q prev) (prev@p) 
                           length p  k 
                           distinct (visited_states (p_source q prev) (prev@p)) }"
using assms proof (induction k arbitrary: q hF prev visitedStates)
  case 0
  then show ?case by auto
next
  case (Suc k)

  let ?tgt = "(target (p_source q prev) prev)"

  have " p . (prev@p)  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) 
             path M (p_source q prev) (prev@p) 
                 length p  Suc k 
                 distinct (visited_states (p_source q prev) (prev@p))"
  proof -
    fix p assume "(prev@p)  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)"
    then consider (a) "(prev@p) = prev" |
                  (b) "(prev@p)  ( (image (λ (x,y,q') . acyclic_paths_up_to_length' (prev@[(?tgt,x,y,q')]) q' hF (insert q' visitedStates) k) 
                                             (Set.filter (λ (x,y,q') . q'  visitedStates) (hF (target (p_source q prev) prev)))))"
      by auto
    then show "path M (p_source q prev) (prev@p)  length p  Suc k  distinct (visited_states (p_source q prev) (prev@p))"
    proof (cases)
      case a
      then show ?thesis using Suc.prems(1,3) by auto
    next
      case b
      then obtain x y q' where *: "(x,y,q')  Set.filter (λ (x,y,q') . q'  visitedStates) (hF ?tgt)"
                         and   **:"(prev@p)  acyclic_paths_up_to_length' (prev@[(?tgt,x,y,q')]) q' hF (insert q' visitedStates) k"
        by auto

      let ?t = "(?tgt,x,y,q')"

      from * have "?t  transitions M" and "q'  visitedStates"
        using Suc.prems(2)[of ?tgt] by simp+ 
      moreover have "t_source ?t = target (p_source q prev) prev"
        by simp
      moreover have "p_source (p_source q prev) (prev@[?t]) = p_source q prev"
        by auto
      ultimately have p1: "path M (p_source (p_source q prev) (prev@[?t])) (prev@[?t])" 
        using Suc.prems(1)
        by (simp add: path_append_transition) 
      
      
      have "q'  set (visited_states (p_source q prev) prev)"
        using q'  visitedStates Suc.prems(4) by auto
      then have p2: "distinct (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))"
        using Suc.prems(3) by auto

      have p3: "(insert q' visitedStates) 
                  = set (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))"
        using Suc.prems(4) by auto

      have ***: "(target (p_source (p_source q prev) (prev @ [(target (p_source q prev) prev, x, y, q')])) 
                         (prev @ [(target (p_source q prev) prev, x, y, q')])) 
                  = q'"
        by auto

      show ?thesis
        using Suc.IH[OF p1 Suc.prems(2) p2 p3] ** 
        unfolding *** 
        unfolding p_source (p_source q prev) (prev@[?t]) = p_source q prev
      proof -
        assume "acyclic_paths_up_to_length' (prev @ [(target (p_source q prev) prev, x, y, q')]) q' hF (insert q' visitedStates) k 
                  = {(prev @ [(target (p_source q prev) prev, x, y, q')]) @ p |p. 
                        path M (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ p) 
                         length p  k 
                         distinct (visited_states (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ p))}"
        then have "ps. prev @ p = (prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps 
                         path M (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps) 
                         length ps  k 
                         distinct (visited_states (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps))"
          using prev @ p  acyclic_paths_up_to_length' (prev @ [(target (p_source q prev) prev, x, y, q')]) q' hF (insert q' visitedStates) k 
          by blast
        then show ?thesis
          by (metis (no_types) Suc_le_mono append.assoc append.right_neutral append_Cons length_Cons same_append_eq)
      qed 
    qed
  qed
  moreover have " p' . p'  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) 
                          p'' . p' = prev@p''"
    using acyclic_paths_up_to_length'_prev[of _ prev "[]" "target (p_source q prev) prev" hF visitedStates "Suc k"] 
    by force
  ultimately have fwd: " p' . p'  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) 
                           p'  { prev@p | p . path M (p_source q prev) (prev@p) 
                                                     length p  Suc k 
                                                     distinct (visited_states (p_source q prev) (prev@p)) }"
    by blast

  have " p . path M (p_source q prev) (prev@p) 
                 length p  Suc k 
                 distinct (visited_states (p_source q prev) (prev@p)) 
                 (prev@p)  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)"
  proof -
    fix p assume "path M (p_source q prev) (prev@p)"
          and    "length p  Suc k"
          and    "distinct (visited_states (p_source q prev) (prev@p))"

    show "(prev@p)  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)"
    proof (cases p)
      case Nil
      then show ?thesis by auto
    next
      case (Cons t p')

      then have "t_source t = target (p_source q (prev)) (prev)" and "t  transitions M"
        using path M (p_source q prev) (prev@p) by auto
      
      have "path M (p_source q (prev@[t])) ((prev@[t])@p')"
      and  "path M (p_source q (prev@[t])) ((prev@[t]))"
        using Cons path M (p_source q prev) (prev@p) by auto
      have "length p'  k"
        using Cons length p  Suc k by auto
      have "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])@p'))"
      and  "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])))" 
        using Cons distinct (visited_states (p_source q prev) (prev@p)) by auto
      then have "t_target t  visitedStates"
        using Suc.prems(4) by auto

      let ?vN = "insert (t_target t) visitedStates"
      have "?vN = set (visited_states (p_source q (prev @ [t])) (prev @ [t]))"
        using Suc.prems(4) by auto

      have "prev@p = prev@([t]@p')"
        using Cons by auto

      have "(prev@[t])@p'  acyclic_paths_up_to_length' (prev @ [t]) (target (p_source q (prev @ [t])) (prev @ [t])) hF (insert (t_target t) visitedStates) k" 
        using Suc.IH[of q "prev@[t]", OF path M (p_source q (prev@[t])) ((prev@[t])) Suc.prems(2)
                                         distinct (visited_states (p_source q (prev@[t])) ((prev@[t]))) 
                                         ?vN = set (visited_states (p_source q (prev @ [t])) (prev @ [t])) ]
        using path M (p_source q (prev@[t])) ((prev@[t])@p')
              length p'  k
              distinct (visited_states (p_source q (prev@[t])) ((prev@[t])@p')) 
        by force

      then have "(prev@[t])@p'  acyclic_paths_up_to_length' (prev@[t]) (t_target t) hF ?vN k"
        by auto
      moreover have "(t_input t,t_output t, t_target t)  Set.filter (λ (x,y,q') . q'  visitedStates) (hF (t_source t))"
        using Suc.prems(2)[of "t_source t"] t  transitions M t_target t  visitedStates
      proof -
        have "b c a. snd t = (b, c, a)  (t_source t, b, c, a)  FSM.transitions M"
          by (metis (no_types) t  FSM.transitions M prod.collapse)
        then show ?thesis
          using hF (t_source t) = {(x, y, q'') |x y q''. (t_source t, x, y, q'')  FSM.transitions M} 
                t_target t  visitedStates 
          by fastforce
      qed 
      ultimately have " (x,y,q')  (Set.filter (λ (x,y,q') . q'  visitedStates) (hF (target (p_source q prev) prev))) .
                        (prev@[t])@p'  (acyclic_paths_up_to_length' (prev@[((target (p_source q prev) prev),x,y,q')]) q' hF (insert q' visitedStates) k)"
        unfolding t_source t = target (p_source q (prev)) (prev)
        by (metis (no_types, lifting) t_source t = target (p_source q prev) prev case_prodI prod.collapse) 
       
      then show ?thesis unfolding prev@p = prev@[t]@p' 
        unfolding acyclic_paths_up_to_length'.simps Let_def by force
    qed
  qed
  then have rev: " p' . p'  {prev@p | p . path M (p_source q prev) (prev@p) 
                                               length p  Suc k 
                                               distinct (visited_states (p_source q prev) (prev@p))} 
                         p'  acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)"
    by blast
  
  show ?case
    using fwd rev by blast
qed 


fun acyclic_paths_up_to_length :: "('a,'b,'c) fsm  'a  nat  ('a,'b,'c) path set" where
  "acyclic_paths_up_to_length M q k = {p. path M q p  length p  k  distinct (visited_states q p)}"

lemma acyclic_paths_up_to_length_code[code] :
  "acyclic_paths_up_to_length M q k = (if q  states M 
      then acyclic_paths_up_to_length' [] q (m2f (set_as_map (transitions M))) {q} k
      else {})"
proof (cases "q  states M")
  case False
  then have "acyclic_paths_up_to_length M q k = {}" 
    using path_begin_state by fastforce
  then show ?thesis using False by auto
next
  case True
  then have *: "path M (p_source q []) []" by auto
  have **: "(q'. (m2f (set_as_map (transitions M))) q' = {(x, y, q'') |x y q''. (q', x, y, q'')  FSM.transitions M})"
    unfolding set_as_map_def by auto 
  have ***: "distinct (visited_states (p_source q []) [])"
    by auto
  have ****: "{q} = set (visited_states (p_source q []) [])"
    by auto
  
  show ?thesis
    using acyclic_paths_up_to_length'_set[OF * ** *** ****, of k ] 
    using True by auto
qed


lemma path_map_target : "target (f4 q) (map (λ t . (f1 (t_source t), f2 (t_input t), f3 (t_output t), f4 (t_target t))) p) = f4 (target q p)" 
  by (induction p; auto)


lemma path_length_sum :
  assumes "path M q p" 
  shows "length p = ( q  states M . length (filter (λt. t_target t = q) p))"
  using assms
proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs)
  then have "length xs = (qstates M. length (filter (λt. t_target t = q) xs))"
    by auto
  
  have *: "t_target x  states M"
    using path M q (xs @ [x]) by auto
  then have **: "length (filter (λt. t_target t = t_target x) (xs @ [x])) 
                  = Suc (length (filter (λt. t_target t = t_target x) xs))"
    by auto

  have " q . q  states M  q  t_target x 
           length (filter (λt. t_target t = q) (xs @ [x])) = length (filter (λt. t_target t = q) xs)"
    by simp
  then have ***: "(qstates M - {t_target x}. length (filter (λt. t_target t = q) (xs @ [x]))) 
                  = (qstates M - {t_target x}. length (filter (λt. t_target t = q) xs))"
    using fsm_states_finite[of M]
    by (metis (no_types, lifting) DiffE insertCI sum.cong)

  have "(qstates M. length (filter (λt. t_target t = q) (xs @ [x]))) 
          = (qstates M - {t_target x}. length (filter (λt. t_target t = q) (xs @ [x]))) 
              + (length (filter (λt. t_target t = t_target x) (xs @ [x])))"
    using * fsm_states_finite[of M]
  proof -
    have "(ainsert (t_target x) (states M). length (filter (λp. t_target p = a) (xs @ [x]))) 
            = (astates M. length (filter (λp. t_target p = a) (xs @ [x])))"
      by (simp add: t_target x  states M insert_absorb)
    then show ?thesis
      by (simp add: finite (states M) sum.insert_remove)
  qed  
  moreover have "(qstates M. length (filter (λt. t_target t = q) xs)) 
                  = (qstates M - {t_target x}. length (filter (λt. t_target t = q) xs)) 
                      + (length (filter (λt. t_target t = t_target x) xs))"
    using * fsm_states_finite[of M]
  proof -
    have "(ainsert (t_target x) (states M). length (filter (λp. t_target p = a) xs)) 
            = (astates M. length (filter (λp. t_target p = a) xs))"
      by (simp add: t_target x  states M insert_absorb)
    then show ?thesis
      by (simp add: finite (states M) sum.insert_remove)
  qed  

  ultimately have "(qstates M. length (filter (λt. t_target t = q) (xs @ [x]))) 
                    = Suc (qstates M. length (filter (λt. t_target t = q) xs))"
    using ** *** by auto
    
  then show ?case
    by (simp add: length xs = (qstates M. length (filter (λt. t_target t = q) xs))) 
qed


lemma path_loop_cut :
  assumes "path M q p"
  and     "t_target (p ! i) = t_target (p ! j)"
  and     "i < j"
  and     "j < length p"
shows "path M q ((take (Suc i) p) @ (drop (Suc j) p))"
and   "target q ((take (Suc i) p) @ (drop (Suc j) p)) = target q p"
and   "length ((take (Suc i) p) @ (drop (Suc j) p)) < length p"
and   "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p))"
and   "target (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p)) = (target q (take (Suc i) p))"
proof -
    
  have "p = (take (Suc j) p) @ (drop (Suc j) p)"
    by auto
  also have " = ((take (Suc i) (take (Suc j) p)) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p)"
    by (metis append_take_drop_id)
  also have " = ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p)"
    using i < j by simp 
  finally have "p = (take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p)"
    by simp

  then have "path M q ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p))"
       and  "path M q (((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p))"
    using path M q p by auto

  have "path M q (take (Suc i) p)" and "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p) @ drop (Suc j) p)"
    using path_append_elim[OF path M q ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p))] 
    by blast+

  
  have *: "(take (Suc i) p @ drop (Suc i) (take (Suc j) p)) = (take (Suc j) p)"
      using i < j append_take_drop_id
      by (metis (take (Suc i) (take (Suc j) p) @ drop (Suc i) (take (Suc j) p)) @ drop (Suc j) p = (take (Suc i) p @ drop (Suc i) (take (Suc j) p)) @ drop (Suc j) p append_same_eq)

  have "path M q (take (Suc j) p)" and "path M (target q (take (Suc j) p)) (drop (Suc j) p)"
    using path_append_elim[OF path M q (((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p))] 
    unfolding *
    by blast+

  have **: "(target q (take (Suc j) p)) = (target q (take (Suc i) p))"
  proof -
    have "p ! i = last (take (Suc i) p)"
      by (metis Suc_lessD assms(3) assms(4) less_trans_Suc take_last_index)
    moreover have "p ! j = last (take (Suc j) p)"
      by (simp add: assms(4) take_last_index)
    ultimately show ?thesis
      using assms(2) unfolding * target.simps visited_states.simps
      by (simp add: last_map) 
  qed

  show "path M q ((take (Suc i) p) @ (drop (Suc j) p))"
    using path M q (take (Suc i) p) path M (target q (take (Suc j) p)) (drop (Suc j) p) unfolding ** by auto

  show "target q ((take (Suc i) p) @ (drop (Suc j) p)) = target q p"
    by (metis "**" append_take_drop_id path_append_target)
    
  show "length ((take (Suc i) p) @ (drop (Suc j) p)) < length p"
  proof -
    have ***: "length p = length ((take (Suc j) p) @ (drop (Suc j) p))"
      by auto

    have "length (take (Suc i) p) < length (take (Suc j) p)"
      using assms(3,4)
      by (simp add: min_absorb2) 

    have scheme: " a b c . length a < length b  length (a@c) < length (b@c)"
      by auto
    
    show ?thesis 
      unfolding *** using scheme[OF length (take (Suc i) p) < length (take (Suc j) p), of "(drop (Suc j) p)"]
      by assumption
  qed

  show "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p))"
    using path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p) @ drop (Suc j) p) by blast

  show "target (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p)) = (target q (take (Suc i) p))"
    by (metis "*" "**" path_append_target) 
qed
      

lemma path_prefix_take :
  assumes "path M q p"
  shows "path M q (take i p)"
proof -
  have "p = (take i p)@(drop i p)" by auto
  then have "path M q ((take i p)@(drop i p))" using assms by auto
  then show ?thesis
    by blast 
qed



subsection ‹Acyclic Paths›

lemma cyclic_path_loop :
  assumes "path M q p"
  and     "¬ distinct (visited_states q p)"
shows " p1 p2 p3 . p = p1@p2@p3  p2  []  target q p1 = target q (p1@p2)"
using assms proof (induction p arbitrary: q)
  case (nil M q)
  then show ?case by auto
next
  case (cons t M ts)
  then show ?case 
  proof (cases "distinct (visited_states (t_target t) ts)")
    case True
    then have "q  set (visited_states (t_target t) ts)"
      using cons.prems by simp 
    then obtain p2 p3 where "ts = p2@p3" and "target (t_target t) p2 = q" 
      using visited_states_prefix[of q "t_target t" ts] by blast
    then have "(t#ts) = []@(t#p2)@p3  (t#p2)  []  target q [] = target q ([]@(t#p2))"
      using cons.hyps by auto
    then show ?thesis by blast
  next
    case False
    then obtain p1 p2 p3 where "ts = p1@p2@p3" and "p2  []" 
                           and "target (t_target t) p1 = target (t_target t) (p1@p2)" 
      using cons.IH by blast
    then have "t#ts = (t#p1)@p2@p3  p2  []  target q (t#p1) = target q ((t#p1)@p2)"
      by simp
    then show ?thesis by blast    
  qed
qed


lemma cyclic_path_pumping :
  assumes "path M (initial M) p" 
      and "¬ distinct (visited_states (initial M) p)"
  shows " p . path M (initial M) p  length p  n"
proof -
  from assms obtain p1 p2 p3 where "p = p1 @ p2 @ p3" and "p2  []" 
                               and "target (initial M) p1 = target (initial M) (p1 @ p2)"
    using cyclic_path_loop[of M "initial M" p] by blast
  then have "path M (target (initial M) p1) p3"
    using path_suffix[of M "initial M" "p1@p2" p3] path M (initial M) p by auto
  
  have "path M (initial M) p1"
    using path_prefix[of M "initial M" p1 "p2@p3"] path M (initial M) p p = p1 @ p2 @ p3 
    by auto
  have "path M (initial M) ((p1@p2)@p3)"
    using path M (initial M) p p = p1 @ p2 @ p3 
    by auto
  have "path M (target (initial M) p1) p2" 
    using path_suffix[of M "initial M" p1 p2, OF path_prefix[of M "initial M" "p1@p2" p3, OF path M (initial M) ((p1@p2)@p3)]] 
    by assumption
  have "target (target (initial M) p1) p2 = (target (initial M) p1)"
    using path_append_target target (initial M) p1 = target (initial M) (p1 @ p2) 
    by auto
  
  have "path M (initial M) (p1 @ (concat (replicate n p2)) @ p3)"  
  proof (induction n)
    case 0 
    then show ?case 
      using path_append[OF path M (initial M) p1 path M (target (initial M) p1) p3]  
      by auto
  next
    case (Suc n)
    then show ?case
      using path M (target (initial M) p1) p2 target (target (initial M) p1) p2 = target (initial M) p1 
      by auto 
  qed
  moreover have "length (p1 @ (concat (replicate n p2)) @ p3)  n"
  proof -
    have "length (concat (replicate n p2)) = n * (length p2)" 
      using concat_replicate_length by metis
    moreover have "length p2 > 0"
      using p2  [] by auto
    ultimately have "length (concat (replicate n p2))  n"
      by (simp add: Suc_leI)
    then show ?thesis by auto
  qed
  ultimately show " p . path M (initial M) p  length p  n" by blast
qed


lemma cyclic_path_shortening : 
  assumes "path M q p"
  and     "¬ distinct (visited_states q p)"
shows " p' . path M q p'  target q p' = target q p  length p' < length p"
proof -
  obtain p1 p2 p3 where *: "p = p1@p2@p3  p2  []  target q p1 = target q (p1@p2)" 
    using cyclic_path_loop[OF assms] by blast
  then have "path M q (p1@p3)"
    using assms(1) by force
  moreover have "target q (p1@p3) = target q p"
    by (metis (full_types) * path_append_target)
  moreover have "length (p1@p3) < length p"
    using * by auto
  ultimately show ?thesis by blast
qed


lemma acyclic_path_from_cyclic_path :
  assumes "path M q p"
  and     "¬ distinct (visited_states q p)"
obtains p' where "path M q p'" and "target q p = target q p'" and "distinct (visited_states q p')"
proof -
  
  let ?paths = "{p' . (path M q p'  target q p' = target q p  length p'  length p)}"
  let ?minPath = "arg_min length (λ io . io  ?paths)" 
  
  have "?paths  empty" 
    using assms(1) by auto
  moreover have "finite ?paths" 
    using paths_finite[of M q "length p"]
    by (metis (no_types, lifting) Collect_mono rev_finite_subset)
  ultimately have minPath_def : "?minPath  ?paths  ( p'  ?paths . length ?minPath  length p')" 
    by (meson arg_min_nat_lemma equals0I)
  then have "path M q ?minPath" and "target q ?minPath = target q p" 
    by auto
  
  moreover have "distinct (visited_states q ?minPath)"
  proof (rule ccontr)
    assume "¬ distinct (visited_states q ?minPath)"
    have " p' . path M q p'  target q p' = target q p  length p' < length ?minPath" 
      using cyclic_path_shortening[OF path M q ?minPath ¬ distinct (visited_states q ?minPath)] minPath_def
            target q ?minPath= target q p by auto
    then show "False" 
      using minPath_def using arg_min_nat_le dual_order.strict_trans1 by auto 
  qed

  ultimately show ?thesis
    by (simp add: that)
qed    


lemma acyclic_path_length_limit :
  assumes "path M q p"
  and     "distinct (visited_states q p)"
shows "length p < size M"
proof (rule ccontr)
  assume *: "¬ length p < size M"
  then have "length p  card (states M)"
    using size_def by auto
  then have "length (visited_states q p) > card (states M)"
    by auto
  moreover have "set (visited_states q p)  states M"
    by (metis assms(1) path_prefix path_target_is_state subsetI visited_states_prefix)
  ultimately have "¬ distinct (visited_states q p)"
    using distinct_card[OF assms(2)] 
    using List.finite_set[of "visited_states q p"]
    by (metis card_mono fsm_states_finite leD) 
  then show "False" using assms(2) by blast
qed





subsection ‹Reachable States›

definition reachable :: "('a,'b,'c) fsm  'a  bool" where
  "reachable M q = ( p . path M (initial M) p  target (initial M) p = q)"

definition reachable_states :: "('a,'b,'c) fsm  'a set" where
  "reachable_states M  = {target (initial M) p | p . path M (initial M) p }"

abbreviation "size_r M  card (reachable_states M)"

lemma acyclic_paths_set :
  "acyclic_paths_up_to_length M q (size M - 1) = {p . path M q p  distinct (visited_states q p)}"
  unfolding acyclic_paths_up_to_length.simps using acyclic_path_length_limit[of M q]
  by (metis (no_types, lifting) One_nat_def Suc_pred cyclic_path_shortening leD list.size(3) 
       not_less_eq_eq not_less_zero path.intros(1) path_begin_state) 


(* inefficient calculation, as a state may be target of a large number of acyclic paths *)
lemma reachable_states_code[code] : 
  "reachable_states M = image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))"
proof -
  have " q' . q'  reachable_states M 
             q'  image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))"
  proof -
    fix q' assume "q'  reachable_states M"
    then obtain p where "path M (initial M) p" and "target (initial M) p = q'"
      unfolding reachable_states_def by blast
    
    obtain p' where "path M (initial M) p'" and "target (initial M) p' = q'" 
                and "distinct (visited_states (initial M) p')"
    proof (cases "distinct (visited_states (initial M) p)")
      case True
      then show ?thesis using path M (initial M) p target (initial M) p = q' that by auto
    next
      case False
      then show ?thesis 
        using acyclic_path_from_cyclic_path[OF path M (initial M) p] 
        unfolding target (initial M) p = q' using that by blast
    qed
    then show "q'  image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))"
      unfolding acyclic_paths_set by force
  qed
  moreover have " q' . q'  image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1)) 
                     q'  reachable_states M"
    unfolding reachable_states_def acyclic_paths_set by blast
  ultimately show ?thesis by blast
qed



lemma reachable_states_intro[intro!] :
  assumes "path M (initial M) p"
  shows "target (initial M) p  reachable_states M"
  using assms unfolding reachable_states_def by auto


lemma reachable_states_initial :
  "initial M  reachable_states M"
  unfolding reachable_states_def by auto


lemma reachable_states_next : 
  assumes "q  reachable_states M" and "t  transitions M" and "t_source t = q" 
  shows "t_target t  reachable_states M" 
proof -
  from q  reachable_states M obtain p where * :"path M (initial M) p"
                                        and   **:"target (initial M) p = q"
    unfolding reachable_states_def by auto

  then have "path M (initial M) (p@[t])" using assms(2,3) path_append_transition by metis
  moreover have "target (initial M) (p@[t]) = t_target t" by auto
  ultimately show ?thesis 
    unfolding reachable_states_def
    by (metis (mono_tags, lifting) mem_Collect_eq)
qed


lemma reachable_states_path :
  assumes "q  reachable_states M"
  and     "path M q p"
  and     "t  set p"
shows "t_source t  reachable_states M"
using assms unfolding reachable_states_def proof (induction p arbitrary: q)
  case Nil
  then show ?case by auto
next
  case (Cons t' p')
  then show ?case proof (cases "t = t'")
    case True
    then show ?thesis using Cons.prems(1,2) by force
  next
    case False then show ?thesis using Cons
      by (metis (mono_tags, lifting) path_cons_elim reachable_states_def reachable_states_next 
            set_ConsD) 
  qed
qed


lemma reachable_states_initial_or_target :
  assumes "q  reachable_states M"
  shows "q = initial M  ( t  transitions M . t_source t  reachable_states M  t_target t = q)"
proof -
  obtain p where "path M (initial M) p" and "target (initial M) p = q"
    using assms unfolding reachable_states_def by auto 
  
  show ?thesis proof (cases p rule: rev_cases)
    case Nil
    then show ?thesis using path M (initial M) p target (initial M) p = q by auto
  next
    case (snoc p' t)
    
    have "t  transitions M"
      using path M (initial M) p unfolding snoc by auto
    moreover have "t_target t = q"
      using target (initial M) p = q unfolding snoc by auto
    moreover have "t_source t  reachable_states M"
      using path M (initial M) p unfolding snoc
      by (metis append_is_Nil_conv last_in_set last_snoc not_Cons_self2 reachable_states_initial reachable_states_path) 

    ultimately show ?thesis
      by blast 
  qed 
qed

lemma reachable_state_is_state : 
  "q  reachable_states M  q  states M" 
  unfolding reachable_states_def using path_target_is_state by fastforce 

lemma reachable_states_finite : "finite (reachable_states M)"
  using fsm_states_finite[of M] reachable_state_is_state[of _ M]
  by (meson finite_subset subset_eq)  


subsection ‹Language›

abbreviation "p_io (p :: ('state,'input,'output) path)  map (λ t . (t_input t, t_output t)) p"

fun language_state_for_input :: "('state,'input,'output) fsm  'state  'input list  ('input × 'output) list set" where
  "language_state_for_input M q xs = {p_io p | p . path M q p  map fst (p_io p) = xs}"

fun LSin :: "('state,'input,'output) fsm  'state  'input list set  ('input × 'output) list set" where
  "LSin M q xss = {p_io p | p . path M q p  map fst (p_io p)  xss}"

abbreviation(input) "Lin M  LSin M (initial M)"

lemma language_state_for_input_inputs : 
  assumes "io  language_state_for_input M q xs"
  shows "map fst io = xs" 
  using assms by auto

lemma language_state_for_inputs_inputs : 
  assumes "io  LSin M q xss"
  shows "map fst io  xss" using assms by auto 


fun LS :: "('state,'input,'output) fsm  'state  ('input × 'output) list set" where
  "LS M q = { p_io p | p . path M q p }"

abbreviation "L M  LS M (initial M)"

lemma language_state_containment :
  assumes "path M q p"
  and     "p_io p = io"
shows "io  LS M q"
  using assms by auto

lemma language_prefix : 
  assumes "io1@io2  LS M q"
  shows "io1  LS M q"
proof -
  obtain p where "path M q p" and "p_io p = io1@io2" 
    using assms by auto
  let ?tp = "take (length io1) p"
  have "path M q ?tp"
    by (metis (no_types) path M q p append_take_drop_id path_prefix) 
  moreover have "p_io ?tp = io1"
    using p_io p = io1@io2 by (metis append_eq_conv_conj take_map) 
  ultimately show ?thesis
    by force 
qed

lemma language_contains_empty_sequence : "[]  L M" 
  by auto


lemma language_state_split :
  assumes "io1 @ io2  LS M q1"
  obtains  p1 p2 where "path M q1 p1" 
                   and "path M (target q1 p1) p2"  
                   and "p_io p1 = io1" 
                   and "p_io p2 = io2"
proof -
  obtain p12 where "path M q1 p12" and "p_io p12 = io1 @ io2"
    using assms unfolding LS.simps by auto

  let ?p1 = "take (length io1) p12"
  let ?p2 = "drop (length io1) p12"

  have "p12 = ?p1 @ ?p2" 
    by auto
  then have "path M q1 (?p1 @ ?p2)"
    using path M q1 p12 by auto

  have "path M q1 ?p1" and "path M (target q1 ?p1) ?p2"
    using path_append_elim[OF path M q1 (?p1 @ ?p2)] by blast+
  moreover have "p_io ?p1 = io1"
    using p12 = ?p1 @ ?p2 p_io p12 = io1 @ io2
    by (metis append_eq_conv_conj take_map)
  moreover have "p_io ?p2 = io2"
    using p12 = ?p1 @ ?p2 p_io p12 = io1 @ io2
    by (metis (no_types) p_io p12 = io1 @ io2 append_eq_conv_conj drop_map) 
  ultimately show ?thesis using that by blast
qed


lemma language_initial_path_append_transition :
  assumes "ios @ [io]  L M"
  obtains p t where "path M (initial M) (p@[t])" and "p_io (p@[t]) = ios @ [io]"
proof -
  obtain pt where "path M (initial M) pt" and "p_io pt = ios @ [io]"
    using assms unfolding LS.simps by auto
  then have "pt  []"
    by auto
  then obtain p t where "pt = p @ [t]"
    using rev_exhaust by blast  
  then have "path M (initial M) (p@[t])" and "p_io (p@[t]) = ios @ [io]"
    using path M (initial M) pt p_io pt = ios @ [io] by auto
  then show ?thesis using that by simp
qed

lemma language_path_append_transition :
  assumes "ios @ [io]  LS M q"
  obtains p t where "path M q (p@[t])" and "p_io (p@[t]) = ios @ [io]"
proof -
  obtain pt where "path M q pt" and "p_io pt = ios @ [io]"
    using assms unfolding LS.simps by auto
  then have "pt  []"
    by auto
  then obtain p t where "pt = p @ [t]"
    using rev_exhaust by blast  
  then have "path M q (p@[t])" and "p_io (p@[t]) = ios @ [io]"
    using path M q pt p_io pt = ios @ [io] by auto
  then show ?thesis using that by simp
qed


lemma language_split :
  assumes "io1@io2  L M"
  obtains p1 p2 where "path M (initial M) (p1@p2)" and "p_io p1 = io1" and "p_io p2 = io2"
proof -
  from assms obtain p where "path M (initial M) p" and "p_io p = io1 @ io2"
    by auto

  let ?p1 = "take (length io1) p"
  let ?p2 = "drop (length io1) p"

  have "path M (initial M) (?p1@?p2)"
    using path M (initial M) p by simp 
  moreover have "p_io ?p1 = io1" 
    using p_io p = io1 @ io2
    by (metis append_eq_conv_conj take_map) 
  moreover have "p_io ?p2 = io2" 
    using p_io p = io1 @ io2
    by (metis append_eq_conv_conj drop_map)
  ultimately show ?thesis using that by blast
qed



lemma language_io : 
  assumes "io  LS M q"
  and     "(x,y)  set io"
shows "x  (inputs M)"
and   "y  outputs M"
proof -
  obtain p where "path M q p" and "p_io p = io"
    using io  LS M q by auto
  then obtain t where "t  set p" and "t_input t = x" and "t_output t = y"
    using (x,y)  set io by auto
  
  have "t  transitions M"
    using path M q p t  set p
    by (induction p; auto)

  show "x  (inputs M)"
    using t  transitions M t_input t = x by auto

  show "y  outputs M"
    using t  transitions M t_output t = y by auto
qed


lemma path_io_split :
  assumes "path M q p"
  and     "p_io p = io1@io2"
shows "path M q (take (length io1) p)"
and   "p_io (take (length io1) p) = io1"
and   "path M (target q (take (length io1) p)) (drop (length io1) p)"
and   "p_io (drop (length io1) p) = io2"
proof -
  have "length io1  length p"
    using p_io p = io1@io2 
    unfolding length_map[of "(λ t . (t_input t, t_output t))", symmetric]
    by auto

  have "p = (take (length io1) p)@(drop (length io1) p)"
    by simp
  then have *: "path M q ((take (length io1) p)@(drop (length io1) p))"
    using path M q p by auto

  show "path M q (take (length io1) p)"
       and  "path M (target q (take (length io1) p)) (drop (length io1) p)"
    using path_append_elim[OF *] by blast+

  show "p_io (take (length io1) p) = io1"
    using p = (take (length io1) p)@(drop (length io1) p) p_io p = io1@io2
    by (metis append_eq_conv_conj take_map) 

  show "p_io (drop (length io1) p) = io2"
    using p = (take (length io1) p)@(drop (length io1) p) p_io p = io1@io2
    by (metis append_eq_conv_conj drop_map)
qed


lemma language_intro :
  assumes "path M q p"
  shows "p_io p  LS M q"
  using assms unfolding LS.simps by auto


lemma language_prefix_append :
  assumes "io1 @ (p_io p)  L M"
shows   "io1 @ p_io (take i p)  L M"
proof -
  fix i
  have "p_io p = (p_io (take i p)) @ (p_io (drop i p))"
    by (metis append_take_drop_id map_append) 
  then have "(io1 @ (p_io (take i p))) @ (p_io (drop i p))  L M"
    using io1 @ p_io p  L M by auto
  show "io1 @ p_io (take i p)  L M" 
    using language_prefix[OF (io1 @ (p_io (take i p))) @ (p_io (drop i p))  L M] 
    by assumption
qed


lemma language_finite: "finite {io . io  L M  length io  k}"
proof -
  have "{io . io  L M  length io  k}  p_io  ` {p. path M (FSM.initial M) p  length p  k}"
    by auto
  then show ?thesis
    using paths_finite[of M "initial M" k]
    using finite_surj by auto 
qed

lemma LS_prepend_transition : 
  assumes "t  transitions M"
  and     "io  LS M (t_target t)"
shows "(t_input t, t_output t) # io  LS M (t_source t)"
proof -
  obtain p where "path M (t_target t) p" and "p_io p = io"
    using assms(2) by auto
  then have "path M (t_source t) (t#p)" and "p_io (t#p) = (t_input t, t_output t) # io"
    using assms(1) by auto
  then show ?thesis 
    unfolding LS.simps
    by (metis (mono_tags, lifting) mem_Collect_eq) 
qed

lemma language_empty_IO :
  assumes "inputs M = {}  outputs M = {}"
  shows "L M = {[]}"
proof -
  consider "inputs M = {}" | "outputs M = {}" using assms by blast
  then show ?thesis proof cases
    case 1

    show "L M = {[]}"
      using language_io(1)[of _ M "initial M"] unfolding 1
      by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair) 
  next
    case 2
    show "L M = {[]}"
      using language_io(2)[of _ M "initial M"] unfolding 2
      by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair) 
  qed
qed

lemma language_equivalence_from_isomorphism_helper :
  assumes "bij_betw f (states M1) (states M2)"
  and     "f (initial M1) = initial M2"
  and     " q x y q' . q  states M1  q'  states M1  (q,x,y,q')  transitions M1  (f q,x,y,f q')  transitions M2"
  and     "q  states M1"
shows "LS M1 q  LS M2 (f q)"
proof 
  fix io assume "io  LS M1 q"

  then obtain p where "path M1 q p" and "p_io p = io"
    by auto

  let ?f = "λ(q,x,y,q') . (f q,x,y,f q')"
  let ?p = "map ?f p"

  have "f q  states M2"
    using assms(1,4)
    using bij_betwE by auto 

  have "path M2 (f q) ?p"
  using path M1 q p proof (induction p rule: rev_induct)
    case Nil
    show ?case using f q  states M2 by auto
  next
    case (snoc a p)
    then have "path M2 (f q) (map ?f p)"
      by auto

    have "target (f q) (map ?f p) = f (target q p)"
      using f (initial M1) = initial M2 assms(2)
      by (induction p; auto)
    then have "t_source (?f a) = target (f q) (map ?f p)"
      by (metis (no_types, lifting) case_prod_beta' fst_conv path_append_transition_elim(3) snoc.prems)
  
    have "a  transitions M1"
      using snoc.prems by auto
    then have "?f a  transitions M2"
      by (metis (mono_tags, lifting) assms(3) case_prod_beta fsm_transition_source fsm_transition_target surjective_pairing)
      
    have "map ?f (p@[a]) = (map ?f p)@[?f a]"
      by auto

    show ?case 
      unfolding map ?f (p@[a]) = (map ?f p)@[?f a]
      using path_append_transition[OF path M2 (f q) (map ?f p) ?f a  transitions M2 t_source (?f a) = target (f q) (map ?f p)]
      by assumption
  qed
  moreover have "p_io ?p = io"
    using p_io p = io
    by (induction p; auto)
  ultimately show "io  LS M2 (f q)"
    using language_state_containment by fastforce
qed


lemma language_equivalence_from_isomorphism :
  assumes "bij_betw f (states M1) (states M2)"
  and     "f (initial M1) = initial M2"
  and     " q x y q' . q  states M1  q'  states M1  (q,x,y,q')  transitions M1  (f q,x,y,f q')  transitions M2"
  and     "q  states M1"
shows "LS M1 q = LS M2 (f q)"
proof 
  show "LS M1 q  LS M2 (f q)"
    using language_equivalence_from_isomorphism_helper[OF assms] .

  have "f q  states M2"
    using assms(1,4)
    using bij_betwE by auto 
  have "(inv_into (FSM.states M1) f (f q)) = q"
    by (meson assms(1) assms(4) bij_betw_imp_inj_on inv_into_f_f) 


  have "bij_betw (inv_into (states M1) f) (states M2) (states M1)"
    using bij_betw_inv_into[OF assms(1)] .
  moreover have "(inv_into (states M1) f) (initial M2) = (initial M1)"
    using assms(1,2)
    by (metis bij_betw_inv_into_left fsm_initial) 
  moreover have " q x y q' . q  states M2  q'  states M2  (q,x,y,q')  transitions M2  ((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q')  transitions M1"
  proof 
    fix q x y q' assume "q  states M2" and "q'  states M2"
    
    show "(q,x,y,q')  transitions M2  ((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q')  transitions M1"
    proof -
      assume a1: "(q, x, y, q')  FSM.transitions M2"
      have f2: "f B A. ¬ bij_betw f B A  (b. (b::'b)  B  (f b::'a)  A)"
        using bij_betwE by blast
      then have f3: "inv_into (states M1) f q  states M1"
        using q  states M2 calculation(1) by blast
      have "inv_into (states M1) f q'  states M1"
        using f2 q'  states M2 calculation(1) by blast
      then show ?thesis
        using f3 a1 q  states M2 q'  states M2 assms(1) assms(3) bij_betw_inv_into_right by fastforce
    qed

    show "((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q')  transitions M1  (q,x,y,q')  transitions M2"
    proof -
      assume a1: "(inv_into (states M1) f q, x, y, inv_into (states M1) f q')  FSM.transitions M1"
      have f2: "f B A. ¬ bij_betw f B A  (b. (b::'b)  B  (f b::'a)  A)"
        by (metis (full_types) bij_betwE)
      then have f3: "inv_into (states M1) f q'  states M1"
        using q'  states M2 calculation(1) by blast
      have "inv_into (states M1) f q  states M1"
        using f2 q  states M2 calculation(1) by blast
      then show ?thesis
        using f3 a1 q  states M2 q'  states M2 assms(1) assms(3) bij_betw_inv_into_right by fastforce
    qed
  qed
  ultimately show "LS M2 (f q)  LS M1 q"
    using language_equivalence_from_isomorphism_helper[of "(inv_into (states M1) f)" M2 M1, OF _ _ _ f q  states M2]
    unfolding (inv_into (FSM.states M1) f (f q)) = q
    by blast
qed



lemma language_equivalence_from_isomorphism_helper_reachable :
  assumes "bij_betw f (reachable_states M1) (reachable_states M2)"
  and     "f (initial M1) = initial M2"
  and     " q x y q' . q  reachable_states M1  q'  reachable_states M1  (q,x,y,q')  transitions M1  (f q,x,y,f q')  transitions M2"
shows "L M1  L M2"
proof 
  fix io assume "io  L M1"

  then obtain p where "path M1 (initial M1) p" and "p_io p = io"
    by auto

  let ?f = "λ(q,x,y,q') . (f q,x,y,f q')"
  let ?p = "map ?f p"

  have "path M2 (initial M2) ?p"
  using path M1 (initial M1) p proof (induction p rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc a p)
    then have "path M2 (initial M2) (map ?f p)"
      by auto

    have "target (initial M2) (map ?f p) = f (target (initial M1) p)"
      using f (initial M1) = initial M2 assms(2)
      by (induction p; auto)
    then have "t_source (?f a) = target (initial M2) (map ?f p)"
      by (metis (no_types, lifting) case_prod_beta' fst_conv path_append_transition_elim(3) snoc.prems)
      

    have "t_source a  reachable_states M1"
      using path M1 (FSM.initial M1) (p @ [a])
      by (metis path_append_transition_elim(3) path_prefix reachable_states_intro) 
    have "t_target a  reachable_states M1"
      using path M1 (FSM.initial M1) (p @ [a])
      by (meson t_source a  reachable_states M1 path_append_transition_elim(2) reachable_states_next) 

    have "a  transitions M1"
      using snoc.prems by auto
    then have "?f a  transitions M2"
      using assms(3)[OF t_source a  reachable_states M1 t_target a  reachable_states M1]
      by (metis (mono_tags, lifting) prod.case_eq_if prod.collapse)
      
    have "map ?f (p@[a]) = (map ?f p)@[?f a]"
      by auto

    show ?case 
      unfolding map ?f (p@[a]) = (map ?f p)@[?f a]
      using path_append_transition[OF path M2 (initial M2) (map ?f p) ?f a  transitions M2 t_source (?f a) = target (initial M2) (map ?f p)]
      by assumption
  qed
  moreover have "p_io ?p = io"
    using p_io p = io
    by (induction p; auto)
  ultimately show "io  L M2"
    using language_state_containment by fastforce
qed
    


lemma language_equivalence_from_isomorphism_reachable :
  assumes "bij_betw f (reachable_states M1) (reachable_states M2)"
  and     "f (initial M1) = initial M2"
  and     " q x y q' . q  reachable_states M1  q'  reachable_states M1  (q,x,y,q')  transitions M1  (f q,x,y,f q')  transitions M2"
shows "L M1 = L M2"
proof 
  show "L M1  L M2"
    using language_equivalence_from_isomorphism_helper_reachable[OF assms] .

  have "bij_betw (inv_into (reachable_states M1) f) (reachable_states M2) (reachable_states M1)"
    using bij_betw_inv_into[OF assms(1)] .
  moreover have "(inv_into (reachable_states M1) f) (initial M2) = (initial M1)"
    using assms(1,2) reachable_states_initial
    by (metis bij_betw_inv_into_left) 
  moreover have " q x y q' . q  reachable_states M2  q'  reachable_states M2  (q,x,y,q')  transitions M2  ((inv_into (reachable_states M1) f) q,x,y,(inv_into (reachable_states M1) f) q')  transitions M1"
  proof 
    fix q x y q' assume "q  reachable_states M2" and "q'  reachable_states M2"
    
    show "(q,x,y,q')  transitions M2  ((inv_into (reachable_states M1) f) q,x,y,(inv_into (reachable_states M1) f) q')  transitions M1"
    proof -
      assume a1: "(q, x, y, q')  FSM.transitions M2"
      have f2: "f B A. ¬ bij_betw f B A  (b. (b::'b)  B  (f b::'a)  A)"
        using bij_betwE by blast
      then have f3: "inv_into (FSM.reachable_states M1) f q  FSM.reachable_states M1"
        using q  FSM.reachable_states M2 calculation(1) by blast
      have "inv_into (FSM.reachable_states M1) f q'  FSM.reachable_states M1"
        using f2 q'  FSM.reachable_states M2 calculation(1) by blast
      then show ?thesis
        using f3 a1 q  FSM.reachable_states M2 q'  FSM.reachable_states M2 assms(1) assms(3) bij_betw_inv_into_right by fastforce
    qed

    show "((inv_into (reachable_states M1) f) q,x,y,(inv_into (reachable_states M1) f) q')  transitions M1  (q,x,y,q')  transitions M2"
    proof -
      assume a1: "(inv_into (FSM.reachable_states M1) f q, x, y, inv_into (FSM.reachable_states M1) f q')  FSM.transitions M1"
      have f2: "f B A. ¬ bij_betw f B A  (b. (b::'b)  B  (f b::'a)  A)"
        by (metis (full_types) bij_betwE)
      then have f3: "inv_into (FSM.reachable_states M1) f q'  FSM.reachable_states M1"
        using q'  FSM.reachable_states M2 calculation(1) by blast
      have "inv_into (FSM.reachable_states M1) f q  FSM.reachable_states M1"
        using f2 q  FSM.reachable_states M2 calculation(1) by blast
      then show ?thesis
        using f3 a1 q  FSM.reachable_states M2 q'  FSM.reachable_states M2 assms(1) assms(3) bij_betw_inv_into_right by fastforce
    qed
  qed
  ultimately show "L M2  L M1"
    using language_equivalence_from_isomorphism_helper_reachable[of "(inv_into (reachable_states M1) f)" M2 M1]
    by blast
qed

lemma language_empty_io :
  assumes "inputs M = {}  outputs M = {}"
  shows "L M = {[]}"
proof -
  have "transitions M = {}"
    using assms fsm_transition_input fsm_transition_output
    by auto
  then have " p . path M (initial M) p  p = []"
    by (metis empty_iff path.cases)
  then show ?thesis 
    unfolding LS.simps
    by blast
qed



subsection ‹Basic FSM Properties›

subsubsection ‹Completely Specified›

fun completely_specified :: "('a,'b,'c) fsm  bool" where
  "completely_specified M = ( q  states M .  x  inputs M .  t  transitions M . t_source t = q  t_input t = x)"


lemma completely_specified_alt_def : 
  "completely_specified M = ( q  states M .  x  inputs M .  q' y . (q,x,y,q')  transitions M)"
  by force

lemma completely_specified_alt_def_h : 
  "completely_specified M = ( q  states M .  x  inputs M . h M (q,x)  {})"
  by force



fun completely_specified_state :: "('a,'b,'c) fsm  'a  bool" where
  "completely_specified_state M q = ( x  inputs M .  t  transitions M . t_source t = q  t_input t = x)"

lemma completely_specified_states :
  "completely_specified M = ( q  states M . completely_specified_state M q)"
  unfolding completely_specified.simps completely_specified_state.simps by force

lemma completely_specified_state_alt_def_h : 
  "completely_specified_state M q = ( x  inputs M . h M (q,x)  {})"
  by force


lemma completely_specified_path_extension : 
  assumes "completely_specified M"
  and     "q  states M"
  and     "path M q p"
  and     "x  (inputs M)"
obtains t where "t  transitions M" and "t_input t = x" and "t_source t = target q p"
proof -
  have "target q p  states M"
    using path_target_is_state path M q p by metis
  then obtain t where "t  transitions M" and "t_input t = x" and "t_source t = target q p"
    using completely_specified M x  (inputs M) 
    unfolding completely_specified.simps by blast
  then show ?thesis using that by blast
qed


lemma completely_specified_language_extension :
  assumes "completely_specified M"
  and     "q  states M"
  and     "io  LS M q"
  and     "x  (inputs M)"
obtains y where "io@[(x,y)]  LS M q"
proof -
  obtain p where "path M q p" and "p_io p = io"
    using io  LS M q by auto
  
  moreover obtain t where "t  transitions M" and "t_input t = x" and "t_source t = target q p"
    using completely_specified_path_extension[OF assms(1,2) path M q p assms(4)] by blast

  ultimately have "path M q (p@[t])" and "p_io (p@[t]) = io@[(x,t_output t)]"
    by (simp add: path_append_transition)+
    
  then have "io@[(x,t_output t)]  LS M q"
    using language_state_containment[of M q "p@[t]" "io@[(x,t_output t)]"] by auto
  then show ?thesis using that by blast
qed
  

lemma path_of_length_ex :
  assumes "completely_specified M"
  and     "q  states M"
  and     "inputs M  {}"
shows " p . path M q p  length p = k" 
using assms(2) proof (induction k arbitrary: q)
  case 0
  then show ?case by auto
next
  case (Suc k)

  obtain t where "t_source t = q" and "t  transitions M"
    by (meson Suc.prems assms(1) assms(3) completely_specified.simps equals0I)
  then have "t_target t  states M"
    using fsm_transition_target by blast
  then obtain p where "path M (t_target t) p  length p = k"
    using Suc.IH by blast
  then show ?case 
    using t_source t = q t  transitions M
    by auto 
qed


subsubsection ‹Deterministic›

fun deterministic :: "('a,'b,'c) fsm  bool" where
  "deterministic M = ( t1  transitions M . 
                         t2  transitions M . 
                          (t_source t1 = t_source t2  t_input t1 = t_input t2) 
                           (t_output t1 = t_output t2  t_target t1 = t_target t2))" 

lemma deterministic_alt_def : 
  "deterministic M = ( q1 x y' y''  q1' q1'' . (q1,x,y',q1')  transitions M  (q1,x,y'',q1'')  transitions M  y' = y''  q1' = q1'')" 
  by auto

lemma deterministic_alt_def_h : 
  "deterministic M = ( q1 x yq yq' . (yq  h M (q1,x)  yq'  h M (q1,x))  yq = yq')"
  by auto



subsubsection ‹Observable›

fun observable :: "('a,'b,'c) fsm  bool" where
  "observable M = ( t1  transitions M . 
                     t2  transitions M . 
                      (t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2) 
                         t_target t1 = t_target t2)" 

lemma observable_alt_def : 
  "observable M = ( q1 x y q1' q1'' . (q1,x,y,q1')  transitions M  (q1,x,y,q1'')  transitions M  q1' = q1'')" 
  by auto

lemma observable_alt_def_h : 
  "observable M = ( q1 x yq yq' . (yq  h M (q1,x)  yq'  h M (q1,x))  fst yq = fst yq'  snd yq = snd yq')"
  by auto


lemma language_append_path_ob :
  assumes "io@[(x,y)]  L M"
  obtains p t where "path M (initial M) (p@[t])" and "p_io p = io" and "t_input t = x" and "t_output t = y"
proof -
  obtain p p2 where "path M (initial M) p" and "path M (target (initial M) p) p2"  and "p_io p = io" and "p_io p2 = [(x,y)]"
    using language_state_split[OF assms] by blast

  obtain t where "p2 = [t]" and "t_input t = x" and "t_output t = y"
    using p_io p2 = [(x,y)] by auto

  have "path M (initial M) (p@[t])"
    using path M (initial M) p path M (target (initial M) p) p2 unfolding p2 = [t] by auto
  then show ?thesis using that[OF _ p_io p = io t_input t = x t_output t = y]
    by simp 
qed


subsubsection ‹Single Input›

(* each state has at most one input, but may have none *)
fun single_input :: "('a,'b,'c) fsm  bool" where
  "single_input M = ( t1  transitions M . 
                       t2  transitions M . 
                        t_source t1 = t_source t2  t_input t1 = t_input t2)" 


lemma single_input_alt_def : 
  "single_input M = ( q1 x x' y y' q1' q1'' . (q1,x,y,q1')  transitions M  (q1,x',y',q1'')  transitions M  x = x')"
  by fastforce

lemma single_input_alt_def_h : 
  "single_input M = ( q x x' . (h M (q,x)  {}  h M (q,x')  {})  x = x')"
  by force
    

subsubsection ‹Output Complete›

fun output_complete :: "('a,'b,'c) fsm  bool" where
  "output_complete M = ( t  transitions M . 
                           y  outputs M . 
                             t'  transitions M . t_source t = t_source t'  
                                                    t_input t = t_input t'  
                                                    t_output t' = y)" 

lemma output_complete_alt_def : 
  "output_complete M = ( q x . ( y q' . (q,x,y,q')  transitions M)  ( y  (outputs M) .  q' . (q,x,y,q')  transitions M))" 
  by force

lemma output_complete_alt_def_h : 
  "output_complete M = ( q x . h M (q,x)  {}  ( y  outputs M .  q' . (y,q')  h M (q,x)))"
  by force



subsubsection ‹Acyclic›

fun acyclic :: "('a,'b,'c) fsm  bool" where
  "acyclic M = ( p . path M (initial M) p  distinct (visited_states (initial M) p))"


lemma visited_states_length : "length (visited_states q p) = Suc (length p)" by auto

lemma visited_states_take : 
  "(take (Suc n) (visited_states q p)) = (visited_states q (take n p))"
proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs)
  then show ?case by (cases "n  length xs"; auto)
qed


(* very inefficient calculation *)
lemma acyclic_code[code] : 
  "acyclic M = (¬( p  (acyclic_paths_up_to_length M (initial M) (size M - 1)) . 
                     t  transitions M . t_source t = target (initial M) p  
                                           t_target t  set (visited_states (initial M) p)))"
proof -
  have "( p  (acyclic_paths_up_to_length M (initial M) (size M - 1)) . 
           t  transitions M . t_source t = target (initial M) p  
                t_target t  set (visited_states (initial M) p)) 
         ¬ FSM.acyclic M"
  proof -
    assume "( p  (acyclic_paths_up_to_length M (initial M) (size M - 1)) . 
               t  transitions M . t_source t = target (initial M) p  
                                    t_target t  set (visited_states (initial M) p))"
    then obtain p t where "path M (initial M) p"
                    and   "distinct (visited_states (initial M) p)"
                    and   "t  transitions M"
                    and   "t_source t = target (initial M) p" 
                    and   "t_target t  set (visited_states (initial M) p)"
      unfolding acyclic_paths_set by blast
    then have "path M (initial M) (p@[t])"
      by (simp add: path_append_transition) 
    moreover have "¬ (distinct (visited_states (initial M) (p@[t])))"
      using t_target t  set (visited_states (initial M) p) by auto
    ultimately show "¬ FSM.acyclic M"
      by (meson acyclic.elims(2))
  qed
  moreover have "¬ FSM.acyclic M  
                  ( p  (acyclic_paths_up_to_length M (initial M) (size M - 1)) . 
                     t  transitions M . t_source t = target (initial M) p  
                                          t_target t  set (visited_states (initial M) p))"
  proof -
    assume "¬ FSM.acyclic M"
    then obtain p where "path M (initial M) p"
                  and   "¬ distinct (visited_states (initial M) p)"
      by auto
    then obtain n where "distinct (take (Suc n) (visited_states (initial M) p))"
                  and   "¬ distinct (take (Suc (Suc n)) (visited_states (initial M) p))"
      using maximal_distinct_prefix by blast
    then have "distinct (visited_states (initial M) (take n p))"
         and   "¬ distinct (visited_states (initial M)(take (Suc n) p))"
      unfolding visited_states_take by simp+

    then obtain p' t' where *: "take n p = p'"
                      and   **: "take (Suc n) p = p' @ [t']"
      by (metis Suc_less_eq ¬ distinct (visited_states (FSM.initial M) p) 
            le_imp_less_Suc not_less_eq_eq take_all take_hd_drop)
    
    have ***: "visited_states (FSM.initial M) (p' @ [t']) = (visited_states (FSM.initial M) p')@[t_target t']"
      by auto

    have "path M (initial M) p'"
      using * path M (initial M) p
      by (metis append_take_drop_id path_prefix)
    then have "p'  (acyclic_paths_up_to_length M (initial M) (size M - 1))"
      using distinct (visited_states (initial M) (take n p))
      unfolding * acyclic_paths_set by blast
    moreover have "t'  transitions M  t_source t' = target (initial M) p'"
      using * ** path M (initial M) p
      by (metis append_take_drop_id path_append_elim path_cons_elim)
       
    moreover have "t_target t'  set (visited_states (initial M) p')"
      using distinct (visited_states (initial M) (take n p)) 
            ¬ distinct (visited_states (initial M)(take (Suc n) p))
      unfolding * ** *** by auto 
    ultimately show "( p  (acyclic_paths_up_to_length M (initial M) (size M - 1)) . 
                       t  transitions M . t_source t = target (initial M) p  
                                            t_target t  set (visited_states (initial M) p))"
      by blast
  qed
  ultimately show ?thesis by blast
qed




lemma acyclic_alt_def : "acyclic M = finite (L M)"
proof 
  show "acyclic M  finite (L M)"
  proof -
    assume "acyclic M"
    then have "{ p . path M (initial M) p}  (acyclic_paths_up_to_length M (initial M) (size M - 1))"
      unfolding acyclic_paths_set by auto
    moreover have "finite (acyclic_paths_up_to_length M (initial M) (size M - 1))"
      unfolding acyclic_paths_up_to_length.simps using paths_finite[of M "initial M" "size M - 1"]
      by (metis (mono_tags, lifting) Collect_cong FSM.acyclic M acyclic.elims(2)) 
    ultimately have "finite { p . path M (initial M) p}"
      using finite_subset by blast
    then show "finite (L M)"
      unfolding LS.simps by auto
  qed

  show "finite (L M)  acyclic M"
  proof (rule ccontr)
    assume "finite (L M)"
    assume "¬ acyclic M"
    
    obtain max_io_len where "io  L M . length io < max_io_len"
      using finite_maxlen[OF finite (L M)] by blast
    then have " p . path M (initial M) p  length p < max_io_len"
    proof -
      fix p assume "path M (initial M) p"
      show "length p < max_io_len"
      proof (rule ccontr)
        assume "¬ length p < max_io_len"
        then have "¬ length (p_io p) < max_io_len" by auto
        moreover have "p_io p  L M"
          unfolding LS.simps using path M (initial M) p by blast
        ultimately show "False"
          using io  L M . length io < max_io_len by blast
      qed
    qed

    obtain p where "path M (initial M) p" and "¬ distinct (visited_states (initial M) p)"
      using ¬ acyclic M unfolding acyclic.simps by blast
    then obtain pL where "path M (initial M) pL" and "max_io_len  length pL"
      using cyclic_path_pumping[of M p max_io_len] by blast
    then show "False"
      using  p . path M (initial M) p  length p < max_io_len
      using not_le by blast 
  qed
qed


lemma acyclic_finite_paths_from_reachable_state :
  assumes "acyclic M"
  and     "path M (initial M) p" 
  and     "target (initial M) p = q"
    shows "finite {p . path M q p}"
proof -
  from assms have "{ p . path M (initial M) p}  (acyclic_paths_up_to_length M (initial M) (size M - 1))"
    unfolding acyclic_paths_set by auto
  moreover have "finite (acyclic_paths_up_to_length M (initial M) (size M - 1))"
    unfolding acyclic_paths_up_to_length.simps using paths_finite[of M "initial M" "size M - 1"]
    by (metis (mono_tags, lifting) Collect_cong FSM.acyclic M acyclic.elims(2)) 
  ultimately have "finite { p . path M (initial M) p}"
    using finite_subset by blast

  show "finite {p . path M q p}"
  proof (cases "q  states M")
    case True
        
    have "image (λp' . p@p') {p' . path M q p'}  {p' . path M (initial M) p'}"
    proof 
      fix x assume "x  image (λp' . p@p') {p' . path M q p'}"
      then obtain p' where "x = p@p'" and "p'  {p' . path M q p'}"
        by blast
      then have "path M q p'" by auto
      then have "path M (initial M) (p@p')"
        using path_append[OF path M (initial M) p] target (initial M) p = q by auto
      then show "x  {p' . path M (initial M) p'}" using x = p@p' by blast
    qed
    
    then have "finite (image (λp' . p@p') {p' . path M q p'})"
      using finite { p . path M (initial M) p} finite_subset by auto 
    show ?thesis using finite_imageD[OF finite (image (λp' . p@p') {p' . path M q p'})]
      by (meson inj_onI same_append_eq) 
  next
    case False
    then show ?thesis
      by (meson not_finite_existsD path_begin_state) 
  qed
qed


lemma acyclic_paths_from_reachable_states :
  assumes "acyclic M" 
  and     "path M (initial M) p'" 
  and     "target (initial M) p' = q"
  and     "path M q p"
shows "distinct (visited_states q p)"
proof -
  have "path M (initial M) (p'@p)"
    using assms(2,3,4) path_append by metis
  then have "distinct (visited_states (initial M) (p'@p))"
    using assms(1) unfolding acyclic.simps by blast
  then have "distinct (initial M # (map t_target p') @ map t_target p)"
    by auto
  moreover have "initial M # (map t_target p') @ map t_target p 
                  = (butlast (initial M # map t_target p')) @ ((last (initial M # map t_target p')) # map t_target p)"
    by auto
  ultimately have "distinct ((last (initial M # map t_target p')) # map t_target p)"
    by auto
  then show ?thesis 
    using target (initial M) p' = q unfolding visited_states.simps target.simps by simp
qed

definition LS_acyclic :: "('a,'b,'c) fsm  'a  ('b × 'c) list set" where
  "LS_acyclic M q = {p_io p | p .  path M q p  distinct (visited_states q p)}"

lemma LS_acyclic_code[code] : 
  "LS_acyclic M q = image p_io (acyclic_paths_up_to_length M q (size M - 1))"
  unfolding acyclic_paths_set LS_acyclic_def by blast

lemma LS_from_LS_acyclic : 
  assumes "acyclic M" 
  shows "L M = LS_acyclic M (initial M)"
proof -
  obtain pps :: "(('b × 'c) list  bool)  (('b × 'c) list  bool)  ('b × 'c) list" where
    f1: "p pa. (¬ p (pps pa p)) = pa (pps pa p)  Collect p = Collect pa"
    by (metis (no_types) Collect_cong)
  have "ps. ¬ path M (FSM.initial M) ps  distinct (visited_states (FSM.initial M) ps)"
    using acyclic.simps assms by blast
  then have "(ps. pps (λps. psa. ps = p_io psa  path M (FSM.initial M) psa) 
                       (λps. psa. ps = p_io psa  path M (FSM.initial M) psa 
                                     distinct (visited_states (FSM.initial M) psa)) 
                  = p_io ps  path M (FSM.initial M) ps  distinct (visited_states (FSM.initial M) ps)) 
             (ps. pps (λps. psa. ps = p_io psa  path M (FSM.initial M) psa) 
                        (λps. psa. ps = p_io psa  path M (FSM.initial M) psa 
                                     distinct (visited_states (FSM.initial M) psa)) 
                  = p_io ps  path M (FSM.initial M) ps)"
    by blast
  then have "{p_io ps |ps. path M (FSM.initial M) ps  distinct (visited_states (FSM.initial M) ps)} 
              = {p_io ps |ps. path M (FSM.initial M) ps}"
    using f1 
    by (meson ps. ¬ path M (FSM.initial M) ps  distinct (visited_states (FSM.initial M) ps)) 
  then show ?thesis
    by (simp add: LS_acyclic_def)
qed



lemma cyclic_cycle :
  assumes "¬ acyclic M"
  shows " q p . path M q p  p  []  target q p = q" 
proof -
  from ¬ acyclic M obtain p t where "path M (initial M) (p@[t])" 
                                  and "¬distinct (visited_states (initial M) (p@[t]))"
    by (metis (no_types, opaque_lifting) Nil_is_append_conv acyclic.simps append_take_drop_id 
          maximal_distinct_prefix rev_exhaust visited_states_take)
     

  show ?thesis
  proof (cases "initial M  set (map t_target (p@[t]))")
    case True
    then obtain i where "last (take i (map t_target (p@[t]))) = initial M" 
                    and "i  length (map t_target (p@[t]))" and "0 < i"
      using list_contains_last_take by metis

    let ?p = "take i (p@[t])"
    have "path M (initial M) (?p@(drop i (p@[t])))" 
      using path M (initial M) (p@[t])
      by (metis append_take_drop_id)  
    then have "path M (initial M) ?p" by auto
    moreover have "?p  []" using 0 < i by auto
    moreover have "target (initial M) ?p = initial M"
      using last (take i (map t_target (p@[t]))) = initial M 
      unfolding target.simps visited_states.simps
      by (metis (no_types, lifting) calculation(2) last_ConsR list.map_disc_iff take_map) 
    ultimately show ?thesis by blast
  next
    case False
    then have "¬ distinct (map t_target (p@[t]))"
      using ¬distinct (visited_states (initial M) (p@[t])) 
      unfolding visited_states.simps 
      by auto
    then obtain i j where "i < j" and "j < length (map t_target (p@[t]))" 
                      and "(map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j"
      using non_distinct_repetition_indices by blast

    let ?pre_i = "take (Suc i) (p@[t])"
    let ?p = "take ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))"
    let ?post_j = "drop ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))"

    have "p@[t] = ?pre_i @ ?p @ ?post_j"
      using i < j j < length (map t_target (p@[t]))
      by (metis append_take_drop_id) 
    then have "path M (target (initial M) ?pre_i) ?p" 
      using path M (initial M) (p@[t])
      by (metis path_prefix path_suffix) 

    have "?p  []"
      using i < j j < length (map t_target (p@[t])) by auto

    have "i < length (map t_target (p@[t]))"
      using i < j j < length (map t_target (p@[t])) by auto
    have "(target (initial M) ?pre_i) = (map t_target (p@[t])) ! i"
      unfolding target.simps visited_states.simps  
      using take_last_index[OF i < length (map t_target (p@[t]))]
      by (metis (no_types, lifting) i < length (map t_target (p @ [t])) 
          last_ConsR snoc_eq_iff_butlast take_Suc_conv_app_nth take_map) 
    
    have "?pre_i@?p = take (Suc j) (p@[t])"
      by (metis (no_types) i < j add_Suc add_diff_cancel_left' less_SucI less_imp_Suc_add take_add)
    moreover have "(target (initial M) (take (Suc j) (p@[t]))) = (map t_target (p@[t])) ! j"
      unfolding target.simps visited_states.simps  
      using take_last_index[OF j < length (map t_target (p@[t]))]
      by (metis (no_types, lifting) j < length (map t_target (p @ [t])) 
            last_ConsR snoc_eq_iff_butlast take_Suc_conv_app_nth take_map) 
    ultimately have "(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! j"
      by auto
    then have "(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! i"
      using (map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j by simp
    moreover have "(target (initial M) (?pre_i@?p)) = (target (target (initial M) ?pre_i) ?p)"
      unfolding target.simps visited_states.simps last.simps by auto
    ultimately have "(target (target (initial M) ?pre_i) ?p) = (map t_target (p@[t])) ! i"
      by auto
    then have "(target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)"
      using (target (initial M) ?pre_i) = (map t_target (p@[t])) ! i by auto

    show ?thesis
      using path M (target (initial M) ?pre_i) ?p ?p  [] 
            (target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)
      by blast
  qed
qed


lemma cyclic_cycle_rev :
  fixes M :: "('a,'b,'c) fsm"
  assumes "path M (initial M) p'"
  and     "target (initial M) p' = q" 
  and     "path M q p"
  and     "p  []"
  and     "target q p = q"
shows "¬ acyclic M"
  using assms unfolding acyclic.simps target.simps visited_states.simps
  using distinct.simps(2) by fastforce

lemma acyclic_initial :
  assumes "acyclic M"
  shows "¬ ( t  transitions M . t_target t = initial M  
                                  ( p . path M (initial M) p  target (initial M) p = t_source t))"
  by (metis append_Cons assms cyclic_cycle_rev list.distinct(1) path.simps 
        path_append path_append_transition_elim(3) single_transition_path) 

lemma cyclic_path_shift : 
  assumes "path M q p"
  and     "target q p = q"
shows "path M (target q (take i p)) ((drop i p) @ (take i p))"
  and "target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))"
proof -
  show "path M (target q (take i p)) ((drop i p) @ (take i p))"
    by (metis append_take_drop_id assms(1) assms(2) path_append path_append_elim path_append_target)
  show "target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))"
    by (metis append_take_drop_id assms(2) path_append_target)
qed


lemma cyclic_path_transition_states_property :
  assumes " t  set p . P (t_source t)"
  and     " t  set p . P (t_source t)  P (t_target t)"
  and     "path M q p"
  and     "target q p = q"
shows " t  set p . P (t_source t)"
  and " t  set p . P (t_target t)"
proof -
  obtain t0 where "t0  set p" and "P (t_source t0)"
    using assms(1) by blast
  then obtain i where "i < length p" and "p ! i = t0"
    by (meson in_set_conv_nth)

  let ?p = "(drop i p @ take i p)"
  have "path M (target q (take i p)) ?p"
    using cyclic_path_shift(1)[OF assms(3,4), of i] by assumption
  
  have "set ?p = set p"
  proof -
    have "set ?p = set (take i p @ drop i p)" 
      using list_set_sym by metis
    then show ?thesis by auto
  qed
  then have " t . t  set ?p  P (t_source t)  P (t_target t)"
    using assms(2) by blast
  
  have " j . j < length ?p  P (t_source (?p ! j))"
  proof -
    fix j assume "j < length ?p"
    then show "P (t_source (?p ! j))"
    proof (induction j)
      case 0
      then show ?case 
        using p ! i = t0 P (t_source t0)
        by (metis i < length p drop_eq_Nil hd_append2 hd_conv_nth hd_drop_conv_nth leD 
              length_greater_0_conv)  
    next
      case (Suc j)
      then have "P (t_source (?p ! j))"
        by auto
      then have "P (t_target (?p ! j))"
        using Suc.prems  t . t  set ?p  P (t_source t)  P (t_target t)[of "?p ! j"]
        using Suc_lessD nth_mem by blast 
      moreover have "t_target (?p ! j) = t_source (?p ! (Suc j))"
        using path_source_target_index[OF Suc.prems path M (target q (take i p)) ?p] 
        by assumption
      ultimately show ?case 
        using  t . t  set ?p  P (t_source t)  P (t_target t)[of "?p ! j"]
        by simp
    qed
  qed
  then have " t  set ?p . P (t_source t)"
    by (metis in_set_conv_nth)
  then show " t  set p . P (t_source t)"
    using set ?p = set p by blast
  then show " t  set p . P (t_target t)"
    using assms(2) by blast
qed


lemma cycle_incoming_transition_ex :
  assumes "path M q p"
  and     "p  []"
  and     "target q p = q"
  and     "t  set p"
shows " tI  set p . t_target tI = t_source t"
proof -
  obtain i where "i < length p" and "p ! i = t"
    using assms(4) by (meson in_set_conv_nth)

  let ?p = "(drop i p @ take i p)"
  have "path M (target q (take i p)) ?p"
  and  "target (target q (take i p)) ?p = target q (take i p)"
    using cyclic_path_shift[OF assms(1,3), of i] by linarith+

  have "p = (take i p @ drop i p)" by auto
  then have "path M (target q (take i p)) (drop i p)" 
    using path_suffix assms(1) by metis
  moreover have "t = hd (drop i p)"
    using i < length p p ! i = t
    by (simp add: hd_drop_conv_nth) 
  ultimately have "path M (target q (take i p)) [t]"
    by (metis i < length p append_take_drop_id assms(1) path_append_elim take_hd_drop)
  then have "t_source t = (target q (take i p))"
    by auto  
  moreover have "t_target (last ?p) = (target q (take i p))" 
    using path M (target q (take i p)) ?p target (target q (take i p)) ?p = target q (take i p) 
          assms(2)
    unfolding target.simps visited_states.simps last.simps
    by (metis (no_types, lifting) p = take i p @ drop i p append_is_Nil_conv last_map 
          list.map_disc_iff)
    
  
  moreover have "set ?p = set p"
  proof -
    have "set ?p = set (take i p @ drop i p)" 
      using list_set_sym by metis
    then show ?thesis by auto
  qed

  ultimately show ?thesis
    by (metis i < length p append_is_Nil_conv drop_eq_Nil last_in_set leD) 
qed


lemma acyclic_paths_finite :
  "finite {p . path M q p  distinct (visited_states q p) }"
proof -
  have " p . path M q p  distinct (visited_states q p)  distinct p"
  proof -
    fix p assume "path M q p" and "distinct (visited_states q p)"
    then have "distinct (map t_target p)" by auto
    then show "distinct p" by (simp add: distinct_map) 
  qed
  
  then show ?thesis
    using finite_subset_distinct[OF fsm_transitions_finite, of M]  path_transitions[of M q]
    by (metis (no_types, lifting) infinite_super mem_Collect_eq path_transitions subsetI)
qed


lemma acyclic_no_self_loop :
  assumes "acyclic M"
  and     "q  reachable_states M"
shows "¬ ( x y . (q,x,y,q)  transitions M)" 
proof 
  assume "x y. (q, x, y, q)  FSM.transitions M"
  then obtain x y where "(q, x, y, q)  FSM.transitions M" by blast
  moreover obtain p where "path M (initial M) p" and "target (initial M) p = q"
    using assms(2) unfolding reachable_states_def by blast
  ultimately have "path M (initial M) (p@[(q,x,y,q)])" 
    by (simp add: path_append_transition) 
  moreover have "¬ (distinct (visited_states (initial M) (p@[(q,x,y,q)])))"
    using target (initial M) p = q unfolding visited_states.simps target.simps by (cases p rule: rev_cases; auto)
  ultimately show "False"
    using assms(1) unfolding acyclic.simps
    by meson 
qed


subsubsection ‹Deadlock States›

fun deadlock_state :: "('a,'b,'c) fsm  'a  bool" where 
  "deadlock_state M q = (¬( t  transitions M . t_source t = q))"

lemma deadlock_state_alt_def : "deadlock_state M q = (LS M q  {[]})" 
proof 
  show "deadlock_state M q  LS M q  {[]}" 
  proof -
    assume "deadlock_state M q"
    moreover have " p . deadlock_state M q  path M q p  p = []"
      unfolding deadlock_state.simps by (metis path.cases) 
    ultimately show "LS M q  {[]}"
      unfolding LS.simps by blast
  qed
  show "LS M q  {[]}  deadlock_state M q"
    unfolding LS.simps deadlock_state.simps using path.cases[of M q] by blast
qed

lemma deadlock_state_alt_def_h : "deadlock_state M q = ( x  inputs M . h M (q,x) = {})" 
  unfolding deadlock_state.simps h.simps 
  using fsm_transition_input by force


lemma acyclic_deadlock_reachable :
  assumes "acyclic M"
  shows " q  reachable_states M . deadlock_state M q"
proof (rule ccontr)
  assume "¬ (qreachable_states M. deadlock_state M q)"
  then have *: " q . q  reachable_states M  ( t  transitions M . t_source t = q)"
    unfolding deadlock_state.simps by blast

  let ?p = "arg_max_on length {p. path M (initial M) p}"
  

  have "finite {p. path M (initial M) p}" 
    by (metis Collect_cong acyclic_finite_paths_from_reachable_state assms eq_Nil_appendI fsm_initial 
          nil path_append path_append_elim) 
    
  moreover have "{p. path M (initial M) p}  {}" 
    by auto
  ultimately obtain p where "path M (initial M) p" 
                        and " p' . path M (initial M) p'  length p'  length p" 
    using max_length_elem
    by (metis mem_Collect_eq not_le_imp_less)

  then obtain t where "t  transitions M" and "t_source t = target (initial M) p"
    using *[of "target (initial M) p"] unfolding reachable_states_def
    by blast

  then have "path M (initial M) (p@[t])"
    using path M (initial M) p
    by (simp add: path_append_transition)

  then show "False"
    using  p' . path M (initial M) p'  length p'  length p
    by (metis impossible_Cons length_rotate1 rotate1.simps(2)) 
qed

lemma deadlock_prefix :
  assumes "path M q p"
  and     "t  set (butlast p)"
shows "¬ (deadlock_state M (t_target t))"
  using assms proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc t' p')
  
  show ?case proof (cases "t  set (butlast p')")
    case True
    show ?thesis 
      using snoc.IH[OF _ True] snoc.prems(1)
      by blast 
  next
    case False
    then have "p' = (butlast p')@[t]"
      using snoc.prems(2) by (metis append_butlast_last_id append_self_conv2 butlast_snoc 
                                in_set_butlast_appendI list_prefix_elem set_ConsD)
    then have "path M q ((butlast p'@[t])@[t'])"
      using snoc.prems(1)
      by auto 
    
    have "t'  transitions M" and "t_source t' = target q (butlast p'@[t])"
      using path_suffix[OF path M q ((butlast p'@[t])@[t'])]
      by auto
    then have "t'  transitions M  t_source t' = t_target t"
      unfolding target.simps visited_states.simps by auto
    then show ?thesis 
      unfolding deadlock_state.simps using t'  transitions M by blast
  qed
qed


lemma states_initial_deadlock :
  assumes "deadlock_state M (initial M)"
  shows "reachable_states M = {initial M}"
  
proof -
  have " q . q  reachable_states M  q = initial M"
  proof -
    fix q assume "q  reachable_states M"
    then obtain p where "path M (initial M) p" and "target (initial M) p = q"
      unfolding reachable_states_def by auto
    
    show "q = initial M" proof (cases p)
      case Nil
      then show ?thesis using target (initial M) p = q by auto
    next
      case (Cons t p')
      then have "False" using assms path M (initial M) p unfolding deadlock_state.simps
        by auto 
      then show ?thesis by simp
    qed
  qed
  then show ?thesis
    using reachable_states_initial[of M] by blast
qed

subsubsection ‹Other›

fun completed_path :: "('a,'b,'c) fsm  'a  ('a,'b,'c) path  bool" where
  "completed_path M q p = deadlock_state M (target q p)"

fun minimal :: "('a,'b,'c) fsm  bool" where
  "minimal M = ( q  states M .  q'  states M . q  q'  LS M q  LS M q')"

lemma minimal_alt_def : "minimal M = ( q q' . q  states M  q'  states M  LS M q = LS M q'  q = q')" 
  by auto  

definition retains_outputs_for_states_and_inputs :: "('a,'b,'c) fsm  ('a,'b,'c) fsm  bool" where
  "retains_outputs_for_states_and_inputs M S 
    = ( tS  transitions S . 
         tM  transitions M . 
          (t_source tS = t_source tM  t_input tS = t_input tM)  tM  transitions S)"





subsection ‹IO Targets and Observability›

fun paths_for_io' :: "(('a × 'b)  ('c × 'a) set)  ('b × 'c) list  'a  ('a,'b,'c) path  ('a,'b,'c) path set" where
  "paths_for_io' f [] q prev = {prev}" |
  "paths_for_io' f ((x,y)#io) q prev = (image (λyq' . paths_for_io' f io (snd yq') (prev@[(q,x,y,(snd yq'))])) (Set.filter (λyq' . fst yq' = y) (f (q,x))))"

lemma paths_for_io'_set :
  assumes "q  states M"
  shows   "paths_for_io' (h M) io q prev = {prev@p | p . path M q p  p_io p = io}"
using assms proof (induction io arbitrary: q prev)
  case Nil
  then show ?case by auto
next
  case (Cons xy io)
  obtain x y where "xy = (x,y)"
    by (meson surj_pair) 

  let ?UN = "(image (λyq' . paths_for_io' (h M) io (snd yq') (prev@[(q,x,y,(snd yq'))])) 
                      (Set.filter (λyq' . fst yq' = y) (h M (q,x))))"

  have "?UN = {prev@p | p . path M q p  p_io p = (x,y)#io}"
  proof 
    have " p . p  ?UN  p  {prev@p | p . path M q p  p_io p = (x,y)#io}"
    proof -
      fix p assume "p  ?UN"
      then obtain q' where "(y,q')  (Set.filter (λyq' . fst yq' = y) (h M (q,x)))"
                     and   "p  paths_for_io' (h M) io q' (prev@[(q,x,y,q')])"
        by auto
      
      from (y,q')  (Set.filter (λyq' . fst yq' = y) (h M (q,x))) have "q'  states M" 
                                                                     and "(q,x,y,q')  transitions M"
        using fsm_transition_target unfolding h.simps by auto

      have "p  {(prev @ [(q, x, y, q')]) @ p |p. path M q' p  p_io p = io}"
        using p  paths_for_io' (h M) io q' (prev@[(q,x,y,q')])
        unfolding Cons.IH[OF q'  states M] by assumption
      moreover have "{(prev @ [(q, x, y, q')]) @ p |p. path M q' p  p_io p = io} 
                       {prev@p | p . path M q p  p_io p = (x,y)#io}"
        using (q,x,y,q')  transitions M
        using cons by force 
      ultimately show "p  {prev@p | p . path M q p  p_io p = (x,y)#io}" 
        by blast
    qed
    then show "?UN  {prev@p | p . path M q p  p_io p = (x,y)#io}"
      by blast

    have " p . p  {prev@p | p . path M q p  p_io p = (x,y)#io}  p  ?UN"
    proof -
      fix pp assume "pp  {prev@p | p . path M q p  p_io p = (x,y)#io}"
      then obtain p where "pp = prev@p" and "path M q p" and "p_io p = (x,y)#io"
        by fastforce
      then obtain t p' where "p = t#p'" and "path M q (t#p')" and "p_io (t#p') = (x,y)#io" 
                         and "p_io p' = io"
        by (metis (no_types, lifting) map_eq_Cons_D)
      then have "path M (t_target t) p'" and "t_source t = q" and "t_input t = x" 
                                         and "t_output t = y" and "t_target t  states M"
                                         and "t  transitions M"
        by auto

      have "(y,t_target t)  Set.filter (λyq'. fst yq' = y) (h M (q, x))"
        using t  transitions M t_output t = y t_input t = x t_source t = q
        unfolding h.simps
        by auto 
      moreover have "(prev@p)  paths_for_io' (h M) io (snd (y,t_target t)) (prev @ [(q, x, y, snd (y,t_target t))])"
        using Cons.IH[OF t_target t  states M, of "prev@[(q, x, y, t_target t)]"]
        using p = t # p' p_io p' = io path M (t_target t) p' t_input t = x 
              t_output t = y t_source t = q 
        by auto

      ultimately show "pp  ?UN" unfolding pp = prev@p
        by blast 
    qed
    then show "{prev@p | p . path M q p  p_io p = (x,y)#io}  ?UN"
      by (meson subsetI) 
  qed

  then show ?case
    by (simp add: xy = (x, y)) 
qed



definition paths_for_io :: "('a,'b,'c) fsm  'a  ('b × 'c) list  ('a,'b,'c) path set" where
  "paths_for_io M q io = {p . path M q p  p_io p = io}"

lemma paths_for_io_set_code[code] :
  "paths_for_io M q io = (if q  states M then paths_for_io' (h M) io q [] else {})"
  using paths_for_io'_set[of q M io "[]"]
  unfolding paths_for_io_def
proof -
  have "{[] @ ps |ps. path M q ps  p_io ps = io} = (if q  FSM.states M then paths_for_io' (h M) io q [] else {}) 
         {ps. path M q ps  p_io ps = io} = (if q  FSM.states M then paths_for_io' (h M) io q [] else {})"
    by auto
  moreover
    { assume "{[] @ ps |ps. path M q ps  p_io ps = io}  (if q  FSM.states M then paths_for_io' (h M) io q [] else {})"
      then have "q  FSM.states M"
        using q  FSM.states M  paths_for_io' (h M) io q [] = {[] @ p |p. path M q p  p_io p = io} by force
      then have "{ps. path M q ps  p_io ps = io} = (if q  FSM.states M then paths_for_io' (h M) io q [] else {})"
      using path_begin_state by force }
  ultimately show "{ps. path M q ps  p_io ps = io} = (if q  FSM.states M then paths_for_io' (h M) io q [] else {})"
    by linarith
qed 


fun io_targets :: "('a,'b,'c) fsm  ('b × 'c) list  'a  'a set" where
  "io_targets M io q = {target q p | p . path M q p  p_io p = io}"

lemma io_targets_code[code] : "io_targets M io q = image (target q) (paths_for_io M q io)"
  unfolding io_targets.simps paths_for_io_def by blast

lemma io_targets_states :
  "io_targets M io q  states M"
  using path_target_is_state by fastforce



lemma observable_transition_unique :
  assumes "observable M"
      and "t  transitions M"
    shows "∃! t'  transitions M . t_source t' = t_source t  
                                    t_input t' = t_input t  
                                    t_output t' = t_output t"
  by (metis assms observable.elims(2) prod.expand)

lemma observable_path_unique :
  assumes "observable M"
  and     "path M q p"
  and     "path M q p'"
  and     "p_io p = p_io p'"
shows "p = p'"
proof -
  have "length p = length p'"
    using assms(4) map_eq_imp_length_eq by blast 
  then show ?thesis
    using p_io p = p_io p' path M q p path M q p'
  proof (induction p p' arbitrary: q rule: list_induct2)
    case Nil
    then show ?case by auto
  next
    case (Cons x xs y ys)
    then have *: "x  transitions M  y  transitions M  t_source x = t_source y 
                                     t_input x = t_input y  t_output x = t_output y" 
      by auto
    then have "t_target x = t_target y" 
      using assms(1) observable.elims(2) by blast 
    then have "x = y"
      by (simp add: "*" prod.expand) 
      

    have "p_io xs = p_io ys" 
      using Cons by auto

    moreover have "path M (t_target x) xs" 
      using Cons by auto
    moreover have "path M (t_target x) ys"
      using Cons t_target x = t_target y by auto
    ultimately have "xs = ys" 
      using Cons by auto

    then show ?case 
      using x = y by simp
  qed
qed


lemma observable_io_targets : 
  assumes "observable M"
  and "io  LS M q"
obtains q'
where "io_targets M io q = {q'}"
proof -

  obtain p where "path M q p" and "p_io p = io" 
    using assms(2) by auto 
  then have "target q p  io_targets M io q"
    by auto   

  have " q' . io_targets M io q = {q'}"
  proof (rule ccontr)
    assume "¬(q'. io_targets M io q = {q'})"
    then have " q' . q'  target q p  q'  io_targets M io q"
    proof -
      have "¬ io_targets M io q  {target q p}"
        using ¬(q'. io_targets M io q = {q'}) target q p  io_targets M io q by blast
      then show ?thesis
        by blast
    qed       
    then obtain q' where "q'  target q p" and "q'  io_targets M io q" 
      by blast
    then obtain p' where "path M q p'" and "target q p' = q'" and "p_io p' = io"
      by auto 
    then have "p_io p = p_io p'" 
      using p_io p = io by simp
    then have "p = p'"
      using observable_path_unique[OF assms(1) path M q p path M q p'] by simp
    then show "False"
      using q'  target q p target q p' = q' by auto
  qed

  then show ?thesis using that by blast
qed


lemma observable_path_io_target : 
  assumes "observable M"
  and     "path M q p"
shows "io_targets M (p_io p) q = {target q p}"
  using observable_io_targets[OF assms(1) language_state_containment[OF assms(2)], of "p_io p"] 
        singletonD[of "target q p"]
  unfolding io_targets.simps
proof -
  assume a1: "a. target q p  {a}  target q p = a"
  assume "thesis. p_io p = p_io p; q'. {target q pa |pa. path M q pa  p_io pa = p_io p} = {q'}  thesis  thesis"
  then obtain aa :: 'a where "b. {target q ps |ps. path M q ps  p_io ps = p_io p} = {aa}  b"
    by meson
  then show "{target q ps |ps. path M q ps  p_io ps = p_io p} = {target q p}"
    using a1 assms(2) by blast
qed


lemma completely_specified_io_targets : 
  assumes "completely_specified M"
  shows " q  io_targets M io (initial M) .  x  (inputs M) .  t  transitions M . t_source t = q  t_input t = x"
  by (meson assms completely_specified.elims(2) io_targets_states subsetD)
  


lemma observable_path_language_step :
  assumes "observable M"
      and "path M q p"
      and "¬ (ttransitions M.
               t_source t = target q p 
               t_input t = x  t_output t = y)"
    shows "(p_io p)@[(x,y)]  LS M q"
using assms proof (induction p rule: rev_induct)
  case Nil
  show ?case proof
    assume "p_io [] @ [(x, y)]  LS M q"
    then obtain p' where "path M q p'" and "p_io p' = [(x,y)]" unfolding LS.simps
      by force 
    then obtain t where "p' = [t]" by blast
    
    have "ttransitions M" and "t_source t = target q []"
      using path M q p' p' = [t] by auto
    moreover have "t_input t = x  t_output t = y"
      using p_io p' = [(x,y)] p' = [t] by auto
    ultimately show "False"
      using Nil.prems(3) by blast
  qed
next
  case (snoc t p)
  
  from path M q (p @ [t]) have "path M q p" and "t_source t = target q p" 
                                              and "t  transitions M" 
    by auto

  show ?case proof
    assume "p_io (p @ [t]) @ [(x, y)]  LS M q"
    then obtain p' where "path M q p'" and "p_io p' = p_io (p @ [t]) @ [(x, y)]"
      by auto
    then obtain p'' t' t'' where "p' = p''@[t']@[t'']"
      by (metis (no_types, lifting) append.assoc map_butlast map_is_Nil_conv snoc_eq_iff_butlast)
    then have "path M q p''" 
      using path M q p' by blast
    
    
    have "p_io p'' = p_io p"
      using p' = p''@[t']@[t''] p_io p' = p_io (p @ [t]) @ [(x, y)] by auto
    then have "p'' = p"
      using observable_path_unique[OF assms(1) path M q p'' path M q p] by blast

    have "t_source t' = target q p''" and "t'  transitions M"
      using path M q p' p' = p''@[t']@[t''] by auto
    then have "t_source t' = t_source t"
      using p'' = p t_source t = target q p by auto 
    moreover have "t_input t' = t_input t  t_output t' = t_output t"
      using p_io p' = p_io (p @ [t]) @ [(x, y)] p' = p''@[t']@[t''] p'' = p by auto
    ultimately have "t' = t"
      using t  transitions M t'  transitions M assms(1) unfolding observable.simps 
      by (meson prod.expand) 

    have "t''  transitions M" and "t_source t'' = target q (p@[t])"
      using path M q p' p' = p''@[t']@[t''] p'' = p t' = t by auto
    moreover have "t_input t'' = x  t_output t'' = y"
      using p_io p' = p_io (p @ [t]) @ [(x, y)] p' = p''@[t']@[t''] by auto
    ultimately show "False"
      using snoc.prems(3) by blast
  qed
qed

lemma observable_io_targets_language :
  assumes "io1 @ io2  LS M q1"
  and     "observable M"
  and     "q2  io_targets M io1 q1"
shows "io2  LS M q2" 
proof -
  obtain p1 p2 where "path M q1 p1" and "path M (target q1 p1) p2"  
                 and "p_io p1 = io1" and "p_io p2 = io2"
    using language_state_split[OF assms(1)] by blast
  then have "io1  LS M q1" and "io2  LS M (target q1 p1)"
    by auto
  
  have "target q1 p1  io_targets M io1 q1"
    using path M q1 p1 p_io p1 = io1
    unfolding io_targets.simps by blast
  then have "target q1 p1 = q2"
    using observable_io_targets[OF assms(2) io1  LS M q1]
    by (metis assms(3) singletonD) 
  then show ?thesis
    using io2  LS M (target q1 p1) by auto
qed


lemma io_targets_language_append :
  assumes "q1  io_targets M io1 q"
  and     "io2  LS M q1"
shows "io1@io2  LS M q" 
proof -
  obtain p1 where "path M q p1" and "p_io p1 = io1" and "target q p1 = q1" 
    using assms(1) by auto
  moreover obtain p2 where "path M q1 p2" and "p_io p2 = io2" 
    using assms(2) by auto
  ultimately have "path M q (p1@p2)" and "p_io (p1@p2) = io1@io2"
    by auto
  then show ?thesis 
    using language_state_containment[of M q "p1@p2" "io1@io2"] by simp
qed


lemma io_targets_next :
  assumes "t  transitions M"
  shows "io_targets M io (t_target t)  io_targets M (p_io [t] @ io) (t_source t)"
unfolding io_targets.simps
proof 
  fix q assume "q  {target (t_target t) p |p. path M (t_target t) p  p_io p = io}"
  then obtain p where "path M (t_target t) p  p_io p = io  target (t_target t) p = q"
    by auto
  then have "path M (t_source t) (t#p)  p_io (t#p) = p_io [t] @ io  target (t_source t) (t#p) = q"
    using FSM.path.cons[OF assms] by auto
  then show "q  {target (t_source t) p |p. path M (t_source t) p  p_io p = p_io [t] @ io}"
    by blast
qed


lemma observable_io_targets_next :
  assumes "observable M"
  and     "t  transitions M"
shows "io_targets M (p_io [t] @ io) (t_source t) = io_targets M io (t_target t)" 
proof 
  show "io_targets M (p_io [t] @ io) (t_source t)  io_targets M io (t_target t)"
  proof 
    fix q assume "q  io_targets M (p_io [t] @ io) (t_source t)"
    then obtain p where "q = target (t_source t) p" 
                    and "path M (t_source t) p"
                    and "p_io p = p_io [t] @ io"
      unfolding io_targets.simps by blast
    then have "q = t_target (last p)" unfolding target.simps visited_states.simps
      using last_map by auto 

    obtain t' p' where "p = t' # p'"
      using p_io p = p_io [t] @ io by auto
    then have "t'  transitions M" and "t_source t' = t_source t"
      using path M (t_source t) p by auto
    moreover have "t_input t' = t_input t" and "t_output t' = t_output t"
      using p = t' # p' p_io p = p_io [t] @ io by auto
    ultimately have "t' = t"
      using t  transitions M observable M unfolding observable.simps
      by (meson prod.expand) 

    then have "path M (t_target t) p'"
      using path M (t_source t) p p = t' # p' by auto
    moreover have "p_io p' = io"
      using p_io p = p_io [t] @ io p = t' # p' by auto
    moreover have "q = target (t_target t) p'"
      using q = target (t_source t) p p = t' # p' t' = t by auto
    ultimately show "q  io_targets M io (t_target t)"
      by auto
  qed

  show "io_targets M io (t_target t)  io_targets M (p_io [t] @ io) (t_source t)"
    using io_targets_next[OF assms(2)] by assumption
qed



lemma observable_language_target :
  assumes "observable M"
  and     "q  io_targets M io1 (initial M)"
  and     "t  io_targets T io1 (initial T)"
  and     "L T  L M"
shows "LS T t  LS M q"
proof 
  fix io2 assume "io2  LS T t"
  then obtain pT2 where "path T t pT2" and "p_io pT2 = io2"
    by auto  
  
  obtain pT1 where "path T (initial T) pT1" and "p_io pT1 = io1" and "target (initial T) pT1 = t"
    using t  io_targets T io1 (initial T) by auto
  then have "path T (initial T) (pT1@pT2)" 
    using path T t pT2 using path_append by metis
  moreover have "p_io (pT1@pT2) = io1@io2"
    using p_io pT1 = io1 p_io pT2 = io2 by auto
  ultimately have "io1@io2  L T"
    using language_state_containment[of T] by auto
  then have "io1@io2  L M"
    using L T  L M by blast
  then obtain pM where "path M (initial M) pM" and "p_io pM = io1@io2"
    by auto

  let ?pM1 = "take (length io1) pM"
  let ?pM2 = "drop (length io1) pM"

  have "path M (initial M) (?pM1@?pM2)"
    using path M (initial M) pM by auto
  then have "path M (initial M) ?pM1" and "path M (target (initial M) ?pM1) ?pM2"
    by blast+
  
  have "p_io ?pM1 = io1"
    using p_io pM = io1@io2 
    by (metis append_eq_conv_conj take_map)
  have "p_io ?pM2 = io2"
    using p_io pM = io1@io2 
    by (metis append_eq_conv_conj drop_map)

  obtain pM1 where "path M (initial M) pM1" and "p_io pM1 = io1" and "target (initial M) pM1 = q"
    using q  io_targets M io1 (initial M) by auto

  have "pM1 = ?pM1"
    using observable_path_unique[OF observable M path M (initial M) pM1 path M (initial M) ?pM1]
    unfolding p_io pM1 = io1 p_io ?pM1 = io1 by simp

  then have "path M q ?pM2"
    using path M (target (initial M) ?pM1) ?pM2 target (initial M) pM1 = q by auto
  then show "io2  LS M q"
    using language_state_containment[OF _ p_io ?pM2 = io2, of M] by auto
qed


lemma observable_language_target_failure :
  assumes "observable M"
  and     "q  io_targets M io1 (initial M)"
  and     "t  io_targets T io1 (initial T)"
  and     "¬ LS T t  LS M q"
shows "¬ L T  L M"
  using observable_language_target[OF assms(1,2,3)] assms(4) by blast
    

lemma language_path_append_transition_observable :
  assumes "(p_io p) @ [(x,y)]  LS M q"
  and     "path M q p"
  and     "observable M"
  obtains t where "path M q (p@[t])" and "t_input t = x" and "t_output t = y"
proof -
  obtain p' t where "path M q (p'@[t])" and "p_io (p'@[t]) = (p_io p) @ [(x,y)]"
    using language_path_append_transition[OF assms(1)] by blast
  then have "path M q p'" and "p_io p' = p_io p" and "t_input t = x" and "t_output t = y"
    by auto

  have "p' = p"
    using observable_path_unique[OF assms(3) path M q p' path M q p p_io p' = p_io p] by assumption
  then have "path M q (p@[t])"
    using path M q (p'@[t]) by auto
  then show ?thesis using that t_input t = x t_output t = y by metis
qed


lemma language_io_target_append :
  assumes "q'  io_targets M io1 q"
  and     "io2  LS M q'"
shows "(io1@io2)  LS M q"
proof - 
  obtain p2 where "path M q' p2" and "p_io p2 = io2"
    using assms(2) by auto

  moreover obtain p1 where "q' = target q p1" and "path M q p1" and "p_io p1 = io1"
    using assms(1) by auto

  ultimately show ?thesis unfolding LS.simps
    by (metis (mono_tags, lifting) map_append mem_Collect_eq path_append) 
qed


lemma observable_path_suffix :
  assumes "(p_io p)@io  LS M q"
  and     "path M q p"
  and     "observable M"
obtains p' where "path M (target q p) p'" and "p_io p' = io"
proof -
  obtain p1 p2 where "path M q p1" and "path M (target q p1) p2"  and "p_io p1 = p_io p" and "p_io p2 = io"
    using language_state_split[OF assms(1)] by blast

  have "p1 = p"
    using observable_path_unique[OF assms(3,2) path M q p1 p_io p1 = p_io p[symmetric]]
    by simp

  show ?thesis using that[of p2] path M (target q p1) p2 p_io p2 = io unfolding p1 = p
    by blast
qed


lemma io_targets_finite :
  "finite (io_targets M io q)"
proof -
  have "(io_targets M io q)  {target q p | p . path M q p  length p  length io}"
    unfolding io_targets.simps length_map[of "(λ t . (t_input t, t_output t))", symmetric] by force
  moreover have "finite {target q p | p . path M q p  length p  length io}"
    using paths_finite[of M q "length io"]
    by simp 
  ultimately show ?thesis
    using rev_finite_subset by blast 
qed

lemma language_next_transition_ob :
  assumes "(x,y)#ios  LS M q"
obtains t where "t_source t = q"
            and "t  transitions M"
            and "t_input t = x"
            and "t_output t = y"
            and "ios  LS M (t_target t)"
proof -
  obtain p where "path M q p" and "p_io p = (x,y)#ios"
    using assms unfolding LS.simps mem_Collect_eq
    by (metis (no_types, lifting)) 
  then obtain t p' where "p = t#p'"
    by blast

  have "t_source t = q"
   and "t  transitions M"
   and "path M (t_target t) p'"
    using path M q p unfolding p = t#p' by auto
  moreover have "t_input t = x"
            and "t_output t = y"
            and "p_io p' = ios"
    using p_io p = (x,y)#ios unfolding p = t#p' by auto
  ultimately show ?thesis using that[of t] by auto
qed

lemma h_observable_card :
  assumes "observable M"
  shows "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))  1"
  and "finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))"
proof -
  have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q')  transitions M}"
    unfolding h.simps by force
  moreover have "{q' . (q,x,y,q')  transitions M} = {}  ( q' . {q' . (q,x,y,q')  transitions M} = {q'})"
    using assms unfolding observable_alt_def by blast
  ultimately show "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))  1"
              and "finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))"
    by auto
qed

lemma h_obs_None : 
  assumes "observable M"
shows "(h_obs M q x y = None) = (q' . (q,x,y,q')  transitions M)"
proof 
  show "(h_obs M q x y = None)  (q' . (q,x,y,q')  transitions M)"
  proof -
    assume "h_obs M q x y = None"
    then have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))  1"
      by auto
    then have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 0"
      using h_observable_card(1)[OF assms, of y q x] by presburger
    then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {}"
      using h_observable_card(2)[OF assms, of y q x] card_0_eq[of "(snd ` Set.filter (λ(y', q'). y' = y) (h M (q, x)))"] by blast
    then show ?thesis 
      unfolding h.simps by force
  qed
  show "(q' . (q,x,y,q')  transitions M)  (h_obs M q x y = None)"
  proof -
    assume "(q' . (q,x,y,q')  transitions M)"
    then have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}"
      unfolding h.simps by force
    then have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 0"
      by simp
    then show ?thesis
      unfolding h_obs_simps Let_def snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}
      by auto
  qed
qed

lemma h_obs_Some : 
  assumes "observable M"
  shows "(h_obs M q x y = Some q') = ({q' . (q,x,y,q')  transitions M} = {q'})"
proof 
  have *: "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q')  transitions M}"
    unfolding h.simps by force

  show "h_obs M q x y = Some q'  ({q' . (q,x,y,q')  transitions M} = {q'})"
  proof -
    assume "h_obs M q x y = Some q'"
    then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))  {}"
      by force 
    then have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) > 0"
      unfolding h_simps using fsm_transitions_finite[of M]
      by (metis assms card_0_eq h_observable_card(2) h_simps neq0_conv) 
    moreover have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))  1"
      using assms unfolding observable_alt_def h_simps
      by (metis assms h_observable_card(1) h_simps)
    ultimately have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 1"
      by auto
    then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}" 
      using h_obs M q x y = Some q' unfolding h_obs_simps Let_def        
      by (metis card_1_singletonE option.inject the_elem_eq) 
    then show ?thesis 
      using * unfolding h.simps by blast
  qed

  show "({q' . (q,x,y,q')  transitions M} = {q'})  (h_obs M q x y = Some q')"
  proof -
    assume "({q' . (q,x,y,q')  transitions M} = {q'})"
    then have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q'}"
      unfolding h.simps by force
    then show ?thesis
      unfolding Let_def
      by simp 
  qed
qed

lemma h_obs_state :
  assumes "h_obs M q x y = Some q'"
  shows "q'  states M"
proof (cases "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 1")
  case True
  then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}" 
    using h_obs M q x y = Some q' unfolding h_obs_simps Let_def        
    by (metis card_1_singletonE option.inject the_elem_eq) 
  then have "(q,x,y,q')  transitions M"
    unfolding h_simps by auto
  then show ?thesis
    by (metis fsm_transition_target snd_conv) 
next
  case False
  then have "h_obs M q x y = None"
    using False unfolding h_obs_simps Let_def by auto
  then show ?thesis using assms by auto 
qed 


fun after :: "('a,'b,'c) fsm  'a  ('b × 'c) list  'a" where
  "after M q [] = q" |
  "after M q ((x,y)#io) = after M (the (h_obs M q x y)) io"

(*abbreviation(input) "after_initial M io ≡ after M (initial M) io" *)
abbreviation "after_initial M io  after M (initial M) io"

lemma after_path :
  assumes "observable M"
  and     "path M q p"
shows "after M q (p_io p) = target q p"
using assms(2) proof (induction p arbitrary: q rule: list.induct)
  case Nil
  then show ?case by auto
next
  case (Cons t p)
  then have "t  transitions M" and "path M (t_target t) p" and "t_source t = q"
    by auto

  have " q' . (q, t_input t, t_output t, q')  FSM.transitions M  q' = t_target t"
    using observable_transition_unique[OF assms(1) t  transitions M] t  transitions M 
    using t_source t = q assms(1) by auto 
  then have "({q'. (q, t_input t, t_output t, q')  FSM.transitions M} = {t_target t})"
    using t  transitions M t_source t = q by auto
  then have "(h_obs M q (t_input t) (t_output t)) = Some (t_target t)"
    using h_obs_Some[OF assms(1), of q "t_input t" "t_output t" "t_target t"]
    by blast 
  then have "after M q (p_io (t#p)) = after M (t_target t) (p_io p)"    
    by auto
  moreover have "target (t_target t) p = target q (t#p)"
    using t_source t = q by auto
  ultimately show ?case 
    using Cons.IH[OF path M (t_target t) p] 
    by simp
qed

lemma observable_after_path :
  assumes "observable M"
  and     "io  LS M q"
obtains p where "path M q p"
            and "p_io p = io"
            and "target q p = after M q io"
  using after_path[OF assms(1)]
  using assms(2) by auto

lemma h_obs_from_LS :
  assumes "observable M"
  and     "[(x,y)]  LS M q"
obtains q' where "h_obs M q x y = Some q'"
  using assms(2) h_obs_None[OF assms(1), of q x y] by force 

lemma after_h_obs :
  assumes "observable M"
  and     "h_obs M q x y = Some q'"
shows "after M q [(x,y)] = q'"
proof -
  have "path M q [(q,x,y,q')]"
    using assms(2) unfolding h_obs_Some[OF assms(1)]
    using single_transition_path by fastforce 
  then show ?thesis
    using assms(2) after_path[OF assms(1), of q "[(q,x,y,q')]"] by auto
qed

lemma after_h_obs_prepend :
  assumes "observable M"
  and     "h_obs M q x y = Some q'"
  and     "io  LS M q'"
shows "after M q ((x,y)#io) = after M q' io" 
proof -
  obtain p where "path M q' p" and "p_io p = io"
    using assms(3) by auto
  then have "after M q' io = target q' p"
    using after_path[OF assms(1)]
    by blast 

  have "path M q ((q,x,y,q')#p)"
    using assms(2) path_prepend_t[OF path M q' p, of q x y] unfolding h_obs_Some[OF assms(1)] by auto
  moreover have "p_io ((q,x,y,q')#p) = (x,y)#io"
    using p_io p = io by auto
  ultimately have "after M q ((x,y)#io) = target q ((q,x,y,q')#p)"
    using after_path[OF assms(1), of q "(q,x,y,q')#p"] by simp
  moreover have "target q ((q,x,y,q')#p) = target q' p"
    by auto
  ultimately show ?thesis
    using after M q' io = target q' p by simp
qed

lemma after_split :
  assumes "observable M"
  and     "α@γ  LS M q"
shows "after M (after M q α) γ = after M q (α @ γ)"
proof -
  obtain p1 p2 where "path M q p1" and "path M (target q p1) p2" and "p_io p1 = α" and "p_io p2 = γ"
    using language_state_split[OF assms(2)] 
    by blast
  then have "path M q (p1@p2)" and "p_io (p1@p2) = (α @ γ)"
    by auto
  then have "after M q (α @ γ) = target q (p1@p2)"
    using assms(1)
    by (metis (mono_tags, lifting) after_path) 
  moreover have "after M q α = target q p1"
    using path M q p1 p_io p1 = α assms(1)
    by (metis (mono_tags, lifting) after_path) 
  moreover have "after M (target q p1) γ = target (target q p1) p2"
    using path M (target q p1) p2 p_io p2 = γ assms(1)
    by (metis (mono_tags, lifting) after_path)
  moreover have "target (target q p1) p2 = target q (p1@p2)"
    by auto
  ultimately show ?thesis 
    by auto
qed


lemma after_io_targets :
  assumes "observable M"
  and     "io  LS M q"
shows "after M q io = the_elem (io_targets M io q)"
proof -
  have "after M q io  io_targets M io q"
    using after_path[OF assms(1)] assms(2)
    unfolding io_targets.simps LS.simps
    by blast 
  then show ?thesis
    using observable_io_targets[OF assms]
    by (metis singletonD the_elem_eq)
qed
    


lemma after_language_subset :
  assumes "observable M"
  and     "α@γ  L M"
  and     "β  LS M (after_initial M (α@γ))"
shows "γ@β  LS M (after_initial M α)"
  by (metis after_io_targets after_split assms(1) assms(2) assms(3) language_io_target_append language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)


lemma after_language_append_iff :
  assumes "observable M"
  and     "α@γ  L M"
shows "β  LS M (after_initial M (α@γ)) = (γ@β  LS M (after_initial M α))"
  by (metis after_io_targets after_language_subset after_split assms(1) assms(2) language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq) 


lemma h_obs_language_iff :
  assumes "observable M"
  shows "(x,y)#io  LS M q = ( q' . h_obs M q x y = Some q'  io  LS M q')"
    (is "?P1 = ?P2")
proof 
  show "?P1  ?P2"
  proof -
    assume ?P1
    then obtain t p where "t  transitions M"
                      and "path M (t_target t) p"
                      and "t_input t = x"
                      and "t_output t = y"
                      and "t_source t = q"
                      and "p_io p = io"
      by auto
    then have "(q,x,y,t_target t)  transitions M"
      by auto
    then have "h_obs M q x y = Some (t_target t)"
      unfolding h_obs_Some[OF assms]
      using assms by auto 
    moreover have "io  LS M (t_target t)"
      using path M (t_target t) p p_io p = io
      by auto
    ultimately show ?P2
      by blast
  qed
  show "?P2  ?P1"
    unfolding h_obs_Some[OF assms] using LS_prepend_transition[where io=io and M=M]
    by (metis fst_conv mem_Collect_eq singletonI snd_conv)
qed

lemma after_language_iff :
  assumes "observable M"
  and     "α  LS M q"
shows "(γ  LS M (after M q α)) = (α@γ  LS M q)"
  by (metis after_io_targets assms(1) assms(2) language_io_target_append observable_io_targets observable_io_targets_language singletonI the_elem_eq)

(* TODO: generalise to non-observable FSMs *)
lemma language_maximal_contained_prefix_ob :
  assumes "io  LS M q"
  and     "q  states M"
  and     "observable M"
obtains io' x y io'' where "io = io'@[(x,y)]@io''"
                       and "io'  LS M q"
                       and "io'@[(x,y)]  LS M q"
proof -
  have " io' x y io'' . io = io'@[(x,y)]@io''  io'  LS M q  io'@[(x,y)]  LS M q"
    using assms(1,2) proof (induction io arbitrary: q)
    case Nil
    then show ?case by auto
  next
    case (Cons xy io)

    obtain x y where "xy = (x,y)"
      by fastforce

    show ?case proof (cases "h_obs M q x y")
      case None
      then have "[]@[(x,y)]  LS M q"
        unfolding h_obs_None[OF assms(3)] by auto
      moreover have "[]  LS M q"
        using Cons.prems by auto
      moreover have "(x,y)#io = []@[(x,y)]@io"
        using Cons.prems 
        unfolding xy = (x,y) by auto
      ultimately show ?thesis
        unfolding xy = (x,y) by blast
    next
      case (Some q')
      then have "io  LS M q'"
        using h_obs_language_iff[OF assms(3), of x y io q] Cons.prems(1) 
        unfolding xy = (x,y)
        by auto
      then obtain io' x' y' io'' where "io = io'@[(x',y')]@io''"
                                   and "io'  LS M q'"
                                   and "io'@[(x',y')]  LS M q'" 
        using Cons.IH[OF _ h_obs_state[OF Some]]
        by blast

      have "xy#io = (xy#io')@[(x',y')]@io''"
        using io = io'@[(x',y')]@io'' by auto
      moreover have "(xy#io')  LS M q"
        using io'  LS M q' Some 
        unfolding xy = (x,y) h_obs_language_iff[OF assms(3)]
        by blast
      moreover have "(xy#io')@[(x',y')]  LS M q"
        using io'@[(x',y')]  LS M q' Some h_obs_language_iff[OF assms(3), of x y "io'@[(x',y')]" q]
        unfolding xy = (x,y) 
        by auto
      ultimately show ?thesis
        by blast
    qed
  qed
  then show ?thesis 
    using that by blast
qed

lemma after_is_state :
  assumes "observable M"
  assumes "io  LS M q"
  shows "FSM.after M q io  states M" 
  using assms
  by (metis observable_after_path path_target_is_state) 

lemma after_reachable_initial :
  assumes "observable M"
  and     "io  L M"
shows "after_initial M io  reachable_states M" 
proof -
  obtain p where "path M (initial M) p" and "p_io p = io"
    using assms(2) by auto
  then have "after_initial M io = target (initial M) p"
    using after_path[OF assms(1)]
    by blast 
  then show ?thesis
    unfolding reachable_states_def using path M (initial M) p by blast
qed

lemma after_transition :
  assumes "observable M"
  and     "(q,x,y,q')  transitions M"
shows "after M q [(x,y)] = q'"
  using after_path[OF assms(1) single_transition_path[OF assms(2)]] 
  by auto

lemma after_transition_exhaust :
  assumes "observable M"
  and     "t  transitions M"
shows "t_target t = after M (t_source t) [(t_input t, t_output t)]"
  using after_transition[OF assms(1)] assms(2)
  by (metis surjective_pairing) 

lemma after_reachable :
  assumes "observable M"
  and     "io  LS M q"
  and     "q  reachable_states M"
shows "after M q io  reachable_states M"
proof -
  obtain p where "path M q p" and "p_io p = io"
    using assms(2) by auto
  then have "after M q io = target q p"
    using after_path[OF assms(1)] by force

  obtain p' where "path M (initial M) p'" and "target (initial M) p' = q"
    using assms(3) unfolding reachable_states_def by blast

  then have "path M (initial M) (p'@p)"
    using path M q p by auto
  moreover have "after M q io = target (initial M) (p'@p)"
    using target (initial M) p' = q
    unfolding after M q io = target q p 
    by auto
  ultimately show ?thesis
    unfolding reachable_states_def by blast
qed

lemma observable_after_language_append :
  assumes "observable M"
  and     "io1  LS M q"
  and     "io2  LS M (after M q io1)"
shows "io1@io2  LS M q"
  using observable_after_path[OF assms(1,2)] assms(3)
proof -
  assume a1: "thesis. (p. path M q p; p_io p = io1; target q p = after M q io1  thesis)  thesis"
  have "ps. io2 = p_io ps  path M (after M q io1) ps"
    using io2  LS M (after M q io1) by auto
  moreover
  { assume "(ps. io2 = p_io ps  path M (after M q io1) ps)  (ps. io1 @ io2  p_io ps  ¬ path M q ps)"
    then have "io1 @ io2  {p_io ps |ps. path M q ps}"
      using a1 by (metis (lifting) map_append path_append) }
  ultimately show ?thesis
    by auto
qed 


lemma observable_after_language_none :
  assumes "observable M"
  and     "io1  LS M q"
  and     "io2  LS M (after M q io1)"
shows "io1@io2  LS M q"
  using after_path[OF assms(1)] language_state_split[of  io1 io2 M q]
  by (metis (mono_tags, lifting) assms(3) language_intro) 


lemma observable_after_eq :
  assumes "observable M"
  and     "after M q io1 = after M q io2"
  and     "io1  LS M q"
  and     "io2  LS M q"
shows "io1@io  LS M q  io2@io  LS M q"
  using observable_after_language_append[OF assms(1,3), of io]
        observable_after_language_append[OF assms(1,4), of io]
        assms(2)
  by (metis assms(1) language_prefix observable_after_language_none) 

lemma observable_after_target : 
  assumes "observable M"
  and     "io @ io'  LS M q"
  and     "path M (FSM.after M q io) p"
  and     "p_io p = io'"
shows "target (FSM.after M q io) p = (FSM.after M q (io @ io'))"
proof -
  obtain p' where "path M q p'" and "p_io p' = io @ io'"
    using io @ io'  LS M q by auto

  then have "path M q (take (length io) p')"
        and "p_io (take (length io) p') = io"
        and "path M (target q (take (length io) p')) (drop (length io) p')"
        and "p_io (drop (length io) p') = io'"
    using path_io_split[of M q p' io io']
    by auto
  then have "FSM.after M q io = target q (take (length io) p')"
    using after_path assms(1) by fastforce
  then have "p = (drop (length io) p')"   
    using path M (target q (take (length io) p')) (drop (length io) p') p_io (drop (length io) p') = io'
          assms(3,4)
          observable_path_unique[OF observable M]
    by force

  have "(FSM.after M q (io @ io')) = target q p'"
    using after_path[OF observable M path M q p'] unfolding p_io p' = io @ io' .
  moreover have "target (FSM.after M q io) p = target q p'"
    using FSM.after M q io = target q (take (length io) p')
    by (metis p = drop (length io) p' append_take_drop_id path_append_target) 
  ultimately show ?thesis
    by simp
qed


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

lemma is_in_language_iff :
  assumes "observable M"
  and     "q  states M"
  shows "is_in_language M q io  io  LS M q"
using assms(2) proof (induction io arbitrary: q)
  case Nil
  then show ?case
    by auto 
next
  case (Cons xy io)

  obtain x y where "xy = (x,y)"
    using prod.exhaust by metis

  show ?case 
    unfolding xy = (x,y)
    unfolding h_obs_language_iff[OF assms(1), of x y io q] 
    unfolding is_in_language.simps
    apply (cases "h_obs M q x y") 
    apply auto[1]
    by (metis Cons.IH h_obs_state option.simps(5))  
qed

lemma observable_paths_for_io :
  assumes "observable M"
  and     "io  LS M q"
obtains p where "paths_for_io M q io = {p}"
proof -
  obtain p where "path M q p" and "p_io p = io"
    using assms(2) by auto
  then have "p  paths_for_io M q io"
    unfolding paths_for_io_def 
    by blast
  then show ?thesis 
    using that[of p]
    using observable_path_unique[OF assms(1) path M q p] p_io p = io
    unfolding paths_for_io_def 
    by force
qed

lemma io_targets_language :
  assumes "q'  io_targets M io q"
  shows "io  LS M q"
  using assms by auto


lemma observable_after_reachable_surj :
  assumes "observable M"
  shows "(after_initial M) ` (L M) = reachable_states M"
proof 
  show "after_initial M ` L M  reachable_states M"
    using after_reachable[OF assms _ reachable_states_initial]
    by blast
  show "reachable_states M  after_initial M ` L M"
    unfolding reachable_states_def
    using after_path[OF assms]
    using image_iff by fastforce 
qed


lemma observable_minimal_size_r_language_distinct :
  assumes "minimal M1"
  and     "minimal M2"
  and     "observable M1"
  and     "observable M2"
  and     "size_r M1 < size_r M2" 
shows "L M1  L M2"
proof 
  assume "L M1 = L M2"

  define V where "V = (λ q . SOME io . io  L M1  after_initial M2 io = q)"

  have " q . q  reachable_states M2  V q  L M1  after_initial M2 (V q) = q"
  proof -
    fix q assume "q  reachable_states M2"
    then have " io . io  L M1  after_initial M2 io = q"
      unfolding L M1 = L M2
      by (metis assms(4) imageE observable_after_reachable_surj)
    then show "V q  L M1  after_initial M2 (V q) = q"
      unfolding V_def 
      using someI_ex[of "λ io . io  L M1  after_initial M2 io = q"] by blast
  qed
  then have "(after_initial M1) ` V ` reachable_states M2  reachable_states M1"
    by (metis assms(3) image_mono image_subsetI observable_after_reachable_surj)
  then have "card (after_initial M1 ` V ` reachable_states M2)  size_r M1"
    using reachable_states_finite[of M1]
    by (meson card_mono) 

  have "(after_initial M2) ` V ` reachable_states M2 = reachable_states M2"
  proof 
    show "after_initial M2 ` V ` reachable_states M2  reachable_states M2"
      using  q . q  reachable_states M2  V q  L M1  after_initial M2 (V q) = q by auto
    show "reachable_states M2  after_initial M2 ` V ` reachable_states M2"
      using  q . q  reachable_states M2  V q  L M1  after_initial M2 (V q) = q observable_after_reachable_surj[OF assms(4)] unfolding L M1 = L M2
      using image_iff by fastforce
  qed
  then have "card ((after_initial M2) ` V ` reachable_states M2) = size_r M2" 
    by auto

  have *: "finite (V ` reachable_states M2)"
    by (simp add: reachable_states_finite) 

  have **: "card ((after_initial M1) ` V ` reachable_states M2) < card ((after_initial M2) ` V ` reachable_states M2)"
    using assms(5) card (after_initial M1 ` V ` reachable_states M2)  size_r M1
    unfolding card ((after_initial M2) ` V ` reachable_states M2) = size_r M2 
    by linarith

  obtain io1 io2 where "io1  V ` reachable_states M2"
                       "io2  V ` reachable_states M2" 
                       "after_initial M2 io1  after_initial M2 io2" 
                       "after_initial M1 io1 = after_initial M1 io2"
    using finite_card_less_witnesses[OF * **]
    by blast
  then have "io1  L M1" and "io2  L M1" and "io1  L M2" and "io2  L M2"
    using  q . q  reachable_states M2  V q  L M1  after_initial M2 (V q) = q unfolding L M1 = L M2
    by auto
  then have "after_initial M1 io1  reachable_states M1"
            "after_initial M1 io2  reachable_states M1"
            "after_initial M2 io1  reachable_states M2"
            "after_initial M2 io2  reachable_states M2"
    using after_reachable[OF assms(3) _ reachable_states_initial] after_reachable[OF assms(4) _ reachable_states_initial]
    by blast+

  obtain io3 where "io3  LS M2 (after_initial M2 io1) = (io3  LS M2 (after_initial M2 io2))"
    using reachable_state_is_state[OF after_initial M2 io1  reachable_states M2] 
          reachable_state_is_state[OF after_initial M2 io2  reachable_states M2] 
          after_initial M2 io1  after_initial M2 io2 assms(2)
    unfolding minimal.simps by blast
  then have "io1@io3  L M2 = (io2@io3  L M2)"
    using observable_after_language_append[OF assms(4) io1  L M2]
          observable_after_language_append[OF assms(4) io2  L M2]
          observable_after_language_none[OF assms(4) io1  L M2]
          observable_after_language_none[OF assms(4) io2  L M2]
    by blast
  moreover have "io1@io3  L M1 = (io2@io3  L M1)"
    by (meson after_initial M1 io1 = after_initial M1 io2 io1  L M1 io2  L M1 assms(3) observable_after_eq) 
  ultimately show False
    using L M1 = L M2 by blast
qed

(* language equivalent minimal FSMs have the same number of reachable states *)
lemma minimal_equivalence_size_r :
  assumes "minimal M1"
  and     "minimal M2"
  and     "observable M1"
  and     "observable M2"
  and     "L M1 = L M2"
shows "size_r M1 = size_r M2" 
  using observable_minimal_size_r_language_distinct[OF assms(1-4)]
        observable_minimal_size_r_language_distinct[OF assms(2,1,4,3)]
        assms(5)
  using nat_neq_iff by auto


subsection ‹Conformity Relations›

fun is_io_reduction_state :: "('a,'b,'c) fsm  'a  ('d,'b,'c) fsm  'd  bool" where
  "is_io_reduction_state A a B b = (LS A a  LS B b)"

abbreviation(input) "is_io_reduction A B  is_io_reduction_state A (initial A) B (initial B)" 
notation 
  is_io_reduction ("_  _")


fun is_io_reduction_state_on_inputs :: "('a,'b,'c) fsm  'a  'b list set  ('d,'b,'c) fsm  'd  bool" where
  "is_io_reduction_state_on_inputs A a U B b = (LSin A a U  LSin B b U)"

abbreviation(input) "is_io_reduction_on_inputs A U B  is_io_reduction_state_on_inputs A (initial A) U B (initial B)" 
notation 
  is_io_reduction_on_inputs ("_ ≼⟦_ _")





subsection ‹A Pass Relation for Reduction and Test Represented as Sets of Input-Output Sequences›

definition pass_io_set :: "('a,'b,'c) fsm  ('b × 'c) list set  bool" where
  "pass_io_set M ios = ( io x y . io@[(x,y)]  ios  ( y' . io@[(x,y')]  L M  io@[(x,y')]  ios))"

definition pass_io_set_maximal :: "('a,'b,'c) fsm  ('b × 'c) list set  bool" where
  "pass_io_set_maximal M ios = ( io x y io' . io@[(x,y)]@io'  ios  ( y' . io@[(x,y')]  L M  ( io''. io@[(x,y')]@io''  ios)))"


lemma pass_io_set_from_pass_io_set_maximal :
  "pass_io_set_maximal M ios = pass_io_set M {io' .  io io'' . io = io'@io''  io  ios}"
proof -
  have " io x y io' . io@[(x,y)]@io'  ios  io@[(x,y)]  {io' .  io io'' . io = io'@io''  io  ios}"
    by auto
  moreover have " io x y . io@[(x,y)]  {io' .  io io'' . io = io'@io''  io  ios}   io' . io@[(x,y)]@io'  ios"
    by auto
  ultimately show ?thesis
    unfolding pass_io_set_def pass_io_set_maximal_def
    by meson 
qed


lemma pass_io_set_maximal_from_pass_io_set :
  assumes "finite ios"
  and     " io' io'' . io'@io''  ios  io'  ios"
shows "pass_io_set M ios = pass_io_set_maximal M {io'  ios . ¬ ( io'' . io''  []  io'@io''  ios)}"
proof -
  have " io x y . io@[(x,y)]  ios   io' . io@[(x,y)]@io'  {io''  ios . ¬ ( io''' . io'''  []  io''@io'''  ios)}"
  proof -
    fix io x y assume "io@[(x,y)]  ios"
    show " io' . io@[(x,y)]@io'  {io''  ios . ¬ ( io''' . io'''  []  io''@io'''  ios)}"
      using finite_set_elem_maximal_extension_ex[OF io@[(x,y)]  ios assms(1)] by force
  qed
  moreover have " io x y io' . io@[(x,y)]@io'  {io''  ios . ¬ ( io''' . io'''  []  io''@io'''  ios)}  io@[(x,y)]  ios"
    using  io' io'' . io'@io''  ios  io'  ios by force
  ultimately show ?thesis
    unfolding pass_io_set_def pass_io_set_maximal_def 
    by meson 
qed


subsection ‹Relaxation of IO based test suites to sets of input sequences›

abbreviation(input) "input_portion xs  map fst xs"

lemma equivalence_io_relaxation :
  assumes "(L M1 = L M2)  (L M1  T = L M2  T)"
shows "(L M1 = L M2)  ({io . io  L M1  ( io'  T . input_portion io = input_portion io')} = {io . io  L M2  ( io'  T . input_portion io = input_portion io')})" 
proof 
  show "(L M1 = L M2)  ({io . io  L M1  ( io'  T . input_portion io = input_portion io')} = {io . io  L M2  ( io'  T . input_portion io = input_portion io')})"
    by blast
  show "({io . io  L M1  ( io'  T . input_portion io = input_portion io')} = {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  L M1 = L M2" 
  proof -
    have *:" M . {io . io  L M  ( io'  T . input_portion io = input_portion io')} = L M  {io .  io'  T . input_portion io = input_portion io'}"
      by blast

    have "({io . io  L M1  ( io'  T . input_portion io = input_portion io')} = {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  (L M1  T = L M2  T)"
      unfolding * by blast
    then show "({io . io  L M1  ( io'  T . input_portion io = input_portion io')} = {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  L M1 = L M2"
      using assms by blast
  qed
qed

lemma reduction_io_relaxation :
  assumes "(L M1  L M2)  (L M1  T  L M2  T)"
shows "(L M1  L M2)  ({io . io  L M1  ( io'  T . input_portion io = input_portion io')}  {io . io  L M2  ( io'  T . input_portion io = input_portion io')})" 
proof 
  show "(L M1  L M2)  ({io . io  L M1  ( io'  T . input_portion io = input_portion io')}  {io . io  L M2  ( io'  T . input_portion io = input_portion io')})"
    by blast
  show "({io . io  L M1  ( io'  T . input_portion io = input_portion io')}  {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  L M1  L M2" 
  proof -
    have *:" M . {io . io  L M  ( io'  T . input_portion io = input_portion io')}  L M  {io .  io'  T . input_portion io = input_portion io'}"
      by blast

    have "({io . io  L M1  ( io'  T . input_portion io = input_portion io')}  {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  (L M1  T  L M2  T)"
      unfolding * by blast
    then show "({io . io  L M1  ( io'  T . input_portion io = input_portion io')}  {io . io  L M2  ( io'  T . input_portion io = input_portion io')})  L M1  L M2"
      using assms by blast
  qed
qed



subsection ‹Submachines›

fun is_submachine :: "('a,'b,'c) fsm  ('a,'b,'c) fsm  bool" where 
  "is_submachine A B = (initial A = initial B  transitions A  transitions B  inputs A = inputs B  outputs A = outputs B  states A  states B)"
  

lemma submachine_path_initial :
  assumes "is_submachine A B"
  and     "path A (initial A) p"
shows "path B (initial B) p"
  using assms proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc a p)
  then show ?case
    by fastforce
qed
   

lemma submachine_path :
  assumes "is_submachine A B"
  and     "path A q p"
shows "path B q p"
  by (meson assms(1) assms(2) is_submachine.elims(2) path_begin_state subsetD transition_subset_path)
  

lemma submachine_reduction : 
  assumes "is_submachine A B"
  shows "is_io_reduction A B"
  using submachine_path[OF assms] assms by auto 


lemma complete_submachine_initial :
  assumes "is_submachine A B"
      and "completely_specified A"
  shows "completely_specified_state B (initial B)"
  using assms(1) assms(2) fsm_initial subset_iff by fastforce


lemma submachine_language :
  assumes "is_submachine S M"
  shows "L S  L M"
  by (meson assms is_io_reduction_state.elims(2) submachine_reduction)


lemma submachine_observable :
  assumes "is_submachine S M"
  and     "observable M"
shows "observable S"
  using assms unfolding is_submachine.simps observable.simps by blast


lemma submachine_transitive :
  assumes "is_submachine S M"
  and     "is_submachine S' S"
shows "is_submachine S' M"
  using assms unfolding is_submachine.simps by force


lemma transitions_subset_path :
  assumes "set p  transitions M"
  and     "p  []"
  and     "path S q p"
shows "path M q p"
  using assms by (induction p arbitrary: q; auto)


lemma transition_subset_paths :
  assumes "transitions S  transitions M"
  and "initial S  states M"
  and "inputs S = inputs M"
  and "outputs S = outputs M"
  and "path S (initial S) p"
shows "path M (initial S) p"
  using assms(5) proof (induction p rule: rev_induct)
case Nil
  then show ?case using assms(2) by auto
next
  case (snoc t p)
  then have "path S (initial S) p" 
        and "t  transitions S" 
        and "t_source t = target (initial S) p" 
        and "path M (initial S) p"
    by auto

  have "t  transitions M"
    using assms(1) t  transitions S by auto
  moreover have "t_source t  states M"
    using t_source t = target (initial S) p path M (initial S) p
    using path_target_is_state by fastforce 
  ultimately have "t  transitions M"
    using t  transitions S assms(3,4) by auto
  then show ?case
    using path M (initial S) p
    using snoc.prems by auto 
qed 


lemma submachine_reachable_subset :
  assumes "is_submachine A B"
shows "reachable_states A  reachable_states B" 
  using assms submachine_path_initial[OF assms] 
  unfolding is_submachine.simps reachable_states_def by force


lemma submachine_simps :
  assumes "is_submachine A B"
shows "initial A = initial B"
and   "states A  states B"
and   "inputs A = inputs B"
and   "outputs A = outputs B"
and   "transitions A  transitions B"
  using assms unfolding is_submachine.simps by blast+


lemma submachine_deadlock :
  assumes "is_submachine A B"
      and "deadlock_state B q"
    shows "deadlock_state A q"
  using assms(1) assms(2) in_mono by auto 



subsection ‹Changing Initial States›

lift_definition from_FSM :: "('a,'b,'c) fsm  'a  ('a,'b,'c) fsm" is FSM_Impl.from_FSMI
  by simp 

lemma from_FSM_simps[simp]:
  assumes "q  states M"
  shows
  "initial (from_FSM M q) = q"  
  "inputs (from_FSM M q) = inputs M"
  "outputs (from_FSM M q) = outputs M"
  "transitions (from_FSM M q) = transitions M"
  "states (from_FSM M q) = states M" using assms by (transfer; simp)+


lemma from_FSM_path_initial :
  assumes "q  states M"
  shows "path M q p = path (from_FSM M q) (initial (from_FSM M q)) p"
  by (metis assms from_FSM_simps(1) from_FSM_simps(4) from_FSM_simps(5) order_refl 
        transition_subset_path)


lemma from_FSM_path :
  assumes "q  states M"
      and "path (from_FSM M q) q' p"
    shows "path M q' p"
  using assms(1) assms(2) path_transitions transitions_subset_path by fastforce


lemma from_FSM_reachable_states :
  assumes "q  reachable_states M"
  shows "reachable_states (from_FSM M q)  reachable_states M"
proof
  from assms obtain p where "path M (initial M) p" and "target (initial M) p = q"
    unfolding reachable_states_def by blast
  then have "q  states M"
    by (meson path_target_is_state)

  fix q' assume "q'  reachable_states (from_FSM M q)"
  then obtain p' where "path (from_FSM M q) q p'" and "target q p' = q'"
    unfolding reachable_states_def from_FSM_simps[OF q  states M] by blast
  then have "path M (initial M) (p@p')" and "target (initial M) (p@p') = q'"
    using from_FSM_path[OF q  states M ] path M (initial M) p
    using target (FSM.initial M) p = q by auto

  then show "q'  reachable_states M"
    unfolding reachable_states_def by blast
qed
  

lemma submachine_from :
  assumes "is_submachine S M"
      and "q  states S"
  shows "is_submachine (from_FSM S q) (from_FSM M q)"
proof -
  have "path S q []"
    using assms(2) by blast
  then have "path M q []"
    by (meson assms(1) submachine_path)
  then show ?thesis
    using assms(1) assms(2) by force
qed


lemma from_FSM_path_rev_initial :
  assumes "path M q p"
  shows "path (from_FSM M q) q p"
  by (metis (no_types) assms from_FSM_path_initial from_FSM_simps(1) path_begin_state)


lemma from_from[simp] :  
  assumes "q1  states M"
  and     "q1'  states M"
shows "from_FSM (from_FSM M q1) q1' = from_FSM M q1'" (is "?M = ?M'") 
proof -
  have *: "q1'  states (from_FSM M q1)"
    using assms(2) unfolding from_FSM_simps(5)[OF assms(1)] by assumption
  
  have "initial ?M = initial ?M'"
  and  "states ?M = states ?M'"
  and  "inputs ?M = inputs ?M'"
  and  "outputs ?M = outputs ?M'"
  and  "transitions ?M = transitions ?M'"
    unfolding  from_FSM_simps[OF *] from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)] by simp+

  then show ?thesis by (transfer; force)
qed


lemma from_FSM_completely_specified : 
  assumes "completely_specified M"
shows "completely_specified (from_FSM M q)" proof (cases "q  states M")
  case True
  then show ?thesis
    using assms by auto 
next
  case False
  then have "from_FSM M q = M" by (transfer; auto)
  then show ?thesis using assms by auto
qed


lemma from_FSM_single_input : 
  assumes "single_input M"
shows "single_input (from_FSM M q)" proof (cases "q  states M")
  case True
  then show ?thesis
    using assms
    by (metis from_FSM_simps(4) single_input.elims(1))  
next
  case False
  then have "from_FSM M q = M" by (transfer; auto)
  then show ?thesis using assms
    by presburger 
qed


lemma from_FSM_acyclic :
  assumes "q  reachable_states M"
  and     "acyclic M"
shows "acyclic (from_FSM M q)"
  using assms(1)
        acyclic_paths_from_reachable_states[OF assms(2), of _ q]
        from_FSM_path[of q M q]
        path_target_is_state
        reachable_state_is_state[OF assms(1)]
        from_FSM_simps(1)
  unfolding acyclic.simps
            reachable_states_def
  by force
  


lemma from_FSM_observable :
  assumes "observable M"
shows "observable (from_FSM M q)"
proof (cases "q  states M")
  case True
  then show ?thesis
    using assms
  proof -
    have f1: "f. observable f = (a b c aa ab. ((a::'a, b::'b, c::'c, aa)  FSM.transitions f  (a, b, c, ab)  FSM.transitions f)  aa = ab)"
      by force
    have "a f. a  FSM.states (f::('a, 'b, 'c) fsm)  FSM.transitions (FSM.from_FSM f a) = FSM.transitions f"
      by (meson from_FSM_simps(4))
    then show ?thesis
      using f1 True assms by presburger
  qed  
next
  case False
  then have "from_FSM M q = M" by (transfer; auto)
  then show ?thesis using assms by presburger
qed


lemma observable_language_next :
  assumes "io#ios  LS M (t_source t)"
  and     "observable M"
  and     "t  transitions M"
  and     "t_input t = fst io"
  and     "t_output t = snd io"
shows "ios  L (from_FSM M (t_target t))"
proof -
  obtain p where "path M (t_source t) p" and "p_io p = io#ios"
    using assms(1)
  proof -
    assume a1: "p. path M (t_source t) p; p_io p = io # ios  thesis"
    obtain pps :: "('a × 'b) list  'c  ('c, 'a, 'b) fsm  ('c × 'a × 'b × 'c) list" where
      "x0 x1 x2. (v3. x0 = p_io v3  path x2 x1 v3) = (x0 = p_io (pps x0 x1 x2)  path x2 x1 (pps x0 x1 x2))"
      by moura
    then have "ps. path M (t_source t) ps  p_io ps = io # ios"
      using assms(1) by auto
    then show ?thesis
      using a1 by meson
  qed
  then obtain t' p' where "p = t' # p'"
    by auto
  then have "t'  transitions M" and "t_source t' = t_source t" and "t_input t' = fst io" and "t_output t' = snd io" 
    using path M (t_source t) p p_io p = io#ios by auto
  then have "t = t'"
    using assms(2,3,4,5) unfolding observable.simps
    by (metis (no_types, opaque_lifting) prod.expand) 

  then have "path M (t_target t) p'" and "p_io p' = ios"
    using p = t' # p' path M (t_source t) p p_io p = io#ios by auto
  then have "path (from_FSM M (t_target t)) (initial (from_FSM M (t_target t))) p'"
    by (meson assms(3) from_FSM_path_initial fsm_transition_target)

  then show ?thesis using p_io p' = ios by auto
qed


lemma from_FSM_language :
  assumes "q  states M"
  shows "L (from_FSM M q) = LS M q"
  using assms unfolding LS.simps by (meson from_FSM_path_initial)


lemma observable_transition_target_language_subset :
  assumes "LS M (t_source t1)  LS M (t_source t2)"
  and     "t1  transitions M"
  and     "t2  transitions M"
  and     "t_input t1 = t_input t2"
  and     "t_output t1 = t_output t2"
  and     "observable M"
shows "LS M (t_target t1)  LS M (t_target t2)"
proof (rule ccontr)
  assume "¬ LS M (t_target t1)  LS M (t_target t2)"
  then obtain ioF where "ioF  LS M (t_target t1)" and "ioF  LS M (t_target t2)"
    by blast
  then have "(t_input t1, t_output t1)#ioF  LS M (t_source t1)"
    using LS_prepend_transition assms(2) by blast
  then have *: "(t_input t1, t_output t1)#ioF  LS M (t_source t2)"
    using assms(1) by blast
  
  have "ioF  LS M (t_target t2)"
    using observable_language_next[OF * observable M t2  transitions M ] unfolding assms(4,5) fst_conv snd_conv
    by (metis assms(3) from_FSM_language fsm_transition_target) 
  then show False
    using ioF  LS M (t_target t2) by blast
qed

lemma observable_transition_target_language_eq :
  assumes "LS M (t_source t1) = LS M (t_source t2)"
  and     "t1  transitions M"
  and     "t2  transitions M"
  and     "t_input t1 = t_input t2"
  and     "t_output t1 = t_output t2"
  and     "observable M"
shows "LS M (t_target t1) = LS M (t_target t2)"
  using observable_transition_target_language_subset[OF _ assms(2,3,4,5,6)]
        observable_transition_target_language_subset[OF _ assms(3,2) assms(4,5)[symmetric] assms(6)]
        assms(1) 
  by blast


lemma language_state_prepend_transition : 
  assumes "io  LS (from_FSM A (t_target t)) (initial (from_FSM A (t_target t)))"
  and     "t  transitions A"
shows "p_io [t] @ io  LS A (t_source t)" 
proof -
  obtain p where "path (from_FSM A (t_target t)) (initial (from_FSM A (t_target t))) p"
           and   "p_io p = io"
    using assms(1) unfolding LS.simps by blast
  then have "path A (t_target t) p"
    by (meson assms(2) from_FSM_path_initial fsm_transition_target)
  then have "path A (t_source t) (t # p)"
    using assms(2) by auto
  then show ?thesis 
    using p_io p = io unfolding LS.simps
    by force 
qed

lemma observable_language_transition_target :
  assumes "observable M"
  and     "t  transitions M"
  and     "(t_input t, t_output t) # io  LS M (t_source t)"
shows "io  LS M (t_target t)"
  by (metis (no_types) assms(1) assms(2) assms(3) from_FSM_language fsm_transition_target fst_conv observable_language_next snd_conv)

lemma LS_single_transition :
  "[(x,y)]  LS M q  ( t  transitions M . t_source t = q  t_input t = x  t_output t = y)" 
proof 
  show "[(x, y)]  LS M q  tFSM.transitions M. t_source t = q  t_input t = x  t_output t = y" 
    by auto
  show "tFSM.transitions M. t_source t = q  t_input t = x  t_output t = y  [(x, y)]  LS M q"
    by (metis LS_prepend_transition from_FSM_language fsm_transition_target language_contains_empty_sequence)
qed

lemma h_obs_language_append :
  assumes "observable M"
  and     "u  L M"
  and     "h_obs M (after_initial M u) x y  None"
shows "u@[(x,y)]  L M"
  using after_language_iff[OF assms(1,2), of "[(x,y)]"]
  using h_obs_None[OF assms(1)] assms(3)
  unfolding LS_single_transition
  by (metis old.prod.inject prod.collapse)


lemma h_obs_language_single_transition_iff :
  assumes "observable M"
  shows "[(x,y)]  LS M q  h_obs M q x y  None"
  using h_obs_None[OF assms(1), of q x y] 
  unfolding LS_single_transition
  by (metis fst_conv prod.exhaust_sel snd_conv)

(* TODO: generalise to non-observable FSMs *)
lemma minimal_failure_prefix_ob :
  assumes "observable M" 
  and     "observable I"
  and     "qM  states M"
  and     "qI  states I"
  and     "io  LS I qI - LS M qM"
obtains 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"
proof -
  have " io' xy io'' . io = io'@[xy]@io''  io'  LS I qI  LS M qM  io'@[xy]  LS I qI - LS M qM"
  using assms(3,4,5) proof (induction io arbitrary: qM qI)
    case Nil
    then show ?case by auto
  next
    case (Cons xy io)
    show ?case proof (cases "[xy]  LS I qI - LS M qM")
      case True

      have "xy # io = []@[xy]@io" 
        by auto
      moreover have "[]  LS I qI  LS M qM"
        using qM  states M qI  states I by auto
      moreover have "[]@[xy]  LS I qI - LS M qM"
        using True by auto
      ultimately show ?thesis 
        by blast
    next
      case False

      obtain x y where "xy = (x,y)"
        by (meson surj_pair)

      have "[(x,y)]  LS M qM"
        using xy = (x,y) False xy # io  LS I qI - LS M qM
        by (metis DiffD1 DiffI append_Cons append_Nil language_prefix)
      then obtain qM' where "(qM,x,y,qM')  transitions M"
        by auto
      then have "io  LS M qM'"
        using observable_language_transition_target[OF observable M]
              xy = (x,y) xy # io  LS I qI - LS M qM
        by (metis DiffD2 LS_prepend_transition fst_conv snd_conv)

      have "[(x,y)]  LS I qI"
        using xy = (x,y) xy # io  LS I qI - LS M qM
        by (metis DiffD1 append_Cons append_Nil language_prefix)
      then obtain qI' where "(qI,x,y,qI')  transitions I"
        by auto
      then have "io  LS I qI'"
        using observable_language_next[of xy io I "(qI,x,y,qI')", OF _ observable I]
              xy # io  LS I qI - LS M qM fsm_transition_target[OF (qI,x,y,qI')  transitions I]
        unfolding xy = (x,y) fst_conv snd_conv
        by (metis DiffD1 from_FSM_language) 

      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 io  LS I qI' io  LS M qM'
              Cons.IH[OF fsm_transition_target[OF (qM,x,y,qM')  transitions M]
                         fsm_transition_target[OF (qI,x,y,qI')  transitions I] ] 
        unfolding fst_conv snd_conv
        by blast

      have "xy#io = (xy#io')@[xy']@io''"
        using io = io'@[xy']@io'' xy = (x,y) by auto
      moreover have "xy#io'  LS I qI  LS M qM"
        using LS_prepend_transition[OF (qI,x,y,qI')  transitions I, of io'] 
        using LS_prepend_transition[OF (qM,x,y,qM')  transitions M, of io'] 
        using io'  LS I qI'  LS M qM'
        unfolding xy = (x,y) fst_conv snd_conv 
        by auto
      moreover have "(xy#io')@[xy']  LS I qI - LS M qM"
        using LS_prepend_transition[OF (qI,x,y,qI')  transitions I, of "io'@[xy']"] 
        using observable_language_transition_target[OF observable M (qM,x,y,qM')  transitions M, of "io'@[xy']"] 
        using io'@[xy']  LS I qI' - LS M qM'
        unfolding xy = (x,y) fst_conv snd_conv
        by fastforce
      ultimately show ?thesis 
        by blast
    qed
  qed
  then show ?thesis 
    using that by blast
qed

subsection ‹Language and Defined Inputs›

lemma defined_inputs_code : "defined_inputs M q = t_input ` Set.filter (λt . t_source t = q) (transitions M)"
  unfolding defined_inputs_set by force

lemma defined_inputs_alt_def : "defined_inputs M q = {t_input t | t . t  transitions M  t_source t = q}"
  unfolding defined_inputs_code by force

lemma defined_inputs_language_diff :
  assumes "x  defined_inputs M1 q1"
      and "x  defined_inputs M2 q2"
    obtains y where "[(x,y)]  LS M1 q1 - LS M2 q2"
  using assms unfolding defined_inputs_alt_def
proof -
  assume a1: "x  {t_input t |t. t  FSM.transitions M2  t_source t = q2}"
  assume a2: "x  {t_input t |t. t  FSM.transitions M1  t_source t = q1}"
  assume a3: "y. [(x, y)]  LS M1 q1 - LS M2 q2  thesis"
  have f4: "p. x = t_input p  p  FSM.transitions M2  t_source p = q2"
    using a1 by blast
  obtain pp :: "'a  'b × 'a × 'c × 'b" where
    "a. ((p. a = t_input p  p  FSM.transitions M1  t_source p = q1)  a = t_input (pp a)  pp a  FSM.transitions M1  t_source (pp a) = q1)  ((p. a = t_input p  p  FSM.transitions M1  t_source p = q1)  (p. a  t_input p  p  FSM.transitions M1  t_source p  q1))"
    by moura
  then have "x = t_input (pp x)  pp x  FSM.transitions M1  t_source (pp x) = q1"
    using a2 by blast
  then show ?thesis
    using f4 a3 by (metis (no_types) DiffI LS_single_transition)
qed 

lemma language_path_append :
  assumes "path M1 q1 p1"
  and     "io  LS M1 (target q1 p1)"
shows "(p_io p1 @ io)  LS M1 q1" 
proof -
  obtain p2 where "path M1 (target q1 p1) p2" and "p_io p2 = io"
    using assms(2) by auto
  then have "path M1 q1 (p1@p2)" 
    using assms(1) by auto
  moreover have "p_io (p1@p2) = (p_io p1 @ io)"
    using p_io p2 = io by auto
  ultimately show ?thesis
    by (metis (mono_tags, lifting) language_intro)
qed

lemma observable_defined_inputs_diff_ob :
  assumes "observable M1"
  and     "observable M2"
  and     "path M1 q1 p1"
  and     "path M2 q2 p2"
  and     "p_io p1 = p_io p2"
  and     "x  defined_inputs M1 (target q1 p1)" 
  and     "x  defined_inputs M2 (target q2 p2)"
obtains y where "(p_io p1)@[(x,y)]  LS M1 q1 - LS M2 q2"
proof -
  obtain y where "[(x,y)]  LS M1 (target q1 p1) - LS M2 (target q2 p2)"
    using defined_inputs_language_diff[OF assms(6,7)] by blast
  then have "(p_io p1)@[(x,y)]  LS M1 q1"
    using language_path_append[OF assms(3)]
    by blast
  moreover have "(p_io p1)@[(x,y)]  LS M2 q2"
    by (metis (mono_tags, lifting) DiffD2 [(x, y)]  LS M1 (target q1 p1) - LS M2 (target q2 p2) assms(2) assms(4) assms(5) language_state_containment observable_path_suffix)
  ultimately show ?thesis 
    using that[of y] by blast
qed


lemma observable_defined_inputs_diff_language :
  assumes "observable M1"
  and     "observable M2"
  and     "path M1 q1 p1"
  and     "path M2 q2 p2"
  and     "p_io p1 = p_io p2"
  and     "defined_inputs M1 (target q1 p1)  defined_inputs M2 (target q2 p2)"
shows "LS M1 q1  LS M2 q2"
proof -
  obtain x where "(x  defined_inputs M1 (target q1 p1) - defined_inputs M2 (target q2 p2))
                   (x  defined_inputs M2 (target q2 p2) - defined_inputs M1 (target q1 p1))"
    using assms by blast
  then consider "(x  defined_inputs M1 (target q1 p1) - defined_inputs M2 (target q2 p2))" |
                "(x  defined_inputs M2 (target q2 p2) - defined_inputs M1 (target q1 p1))" 
    by blast
  then show ?thesis
  proof cases
    case 1
    then show ?thesis 
      using observable_defined_inputs_diff_ob[OF assms(1-5), of x] by blast
  next
    case 2
    then show ?thesis 
      using observable_defined_inputs_diff_ob[OF assms(2,1,4,3) assms(5)[symmetric], of x] by blast
  qed
qed

fun maximal_prefix_in_language :: "('a,'b,'c) fsm  'a  ('b ×'c) list  ('b ×'c) list" where
  "maximal_prefix_in_language M q [] = []" |
  "maximal_prefix_in_language M q ((x,y)#io) = (case h_obs M q x y of
    None  [] |
    Some q'  (x,y)#maximal_prefix_in_language M q' io)"

lemma maximal_prefix_in_language_properties :
  assumes "observable M"
  and     "q  states M"
shows "maximal_prefix_in_language M q io  LS M q"
and   "maximal_prefix_in_language M q io  list.set (prefixes io)"
proof -
  have "maximal_prefix_in_language M q io  LS M q  maximal_prefix_in_language M q io  list.set (prefixes io)"
    using assms(2) proof (induction io arbitrary: q)
    case Nil
    then show ?case by auto
  next
    case (Cons xy io)

    obtain x y where "xy = (x,y)"
      using prod.exhaust by metis

    show ?case proof (cases "h_obs M q x y")
      case None
      then have "maximal_prefix_in_language M q (xy#io) = []"
        unfolding xy = (x,y)
        by auto
      then show ?thesis
        by (metis (mono_tags, lifting) Cons.prems append_self_conv2 from_FSM_language language_contains_empty_sequence mem_Collect_eq prefixes_set) 
    next
      case (Some q')
      then have *: "maximal_prefix_in_language M q (xy#io) = (x,y)#maximal_prefix_in_language M q' io"
        unfolding xy = (x,y)
        by auto

      have "q'  states M"
        using h_obs_state[OF Some] by auto
      then have "maximal_prefix_in_language M q' io  LS M q'" 
            and "maximal_prefix_in_language M q' io  list.set (prefixes io)"
        using Cons.IH by auto

      have "maximal_prefix_in_language M q (xy # io)  LS M q"
        unfolding *
        using Some maximal_prefix_in_language M q' io  LS M q'
        by (meson assms(1) h_obs_language_iff)
      moreover have "maximal_prefix_in_language M q (xy # io)  list.set (prefixes (xy # io))"
        unfolding * 
        unfolding xy = (x,y)
        using maximal_prefix_in_language M q' io  list.set (prefixes io) append_Cons
        unfolding prefixes_set
        by auto 
      ultimately show ?thesis
        by blast
    qed
  qed
  then show "maximal_prefix_in_language M q io  LS M q"
       and  "maximal_prefix_in_language M q io  list.set (prefixes io)"
    by auto
qed


subsection ‹Further Reachability Formalisations›

(* states that are reachable in at most k transitions *)
fun reachable_k :: "('a,'b,'c) fsm  'a  nat  'a set" where
  "reachable_k M q n = {target q p | p . path M q p  length p  n}" 


lemma reachable_k_0_initial : "reachable_k M (initial M) 0 = {initial M}" 
  by auto

lemma reachable_k_states : "reachable_states M = reachable_k M (initial M) ( size M - 1)"
proof -
  have "q. q  reachable_states M  q  reachable_k M (initial M) ( size M - 1)"
  proof -
    fix q assume "q  reachable_states M"
    then obtain p where "path M (initial M) p" and "target (initial M) p = q"
      unfolding reachable_states_def by blast
    then obtain p' where "path M (initial M) p'"
                     and "target (initial M) p' = target (initial M) p" 
                     and "length p' < size M"
      by (metis acyclic_path_from_cyclic_path acyclic_path_length_limit)
    then show "q  reachable_k M (initial M) ( size M - 1)"
      using target (FSM.initial M) p = q less_trans by auto
  qed

  moreover have "x. x  reachable_k M (initial M) ( size M - 1)  x  reachable_states M"
    unfolding reachable_states_def reachable_k.simps by blast
  
  ultimately show ?thesis by blast
qed


  
subsubsection ‹Induction Schemes›


  
lemma acyclic_induction [consumes 1, case_names reachable_state]:
  assumes "acyclic M"
      and " q . q  reachable_states M  ( t . t  transitions M  ((t_source t = q)  P (t_target t)))  P q"
    shows " q  reachable_states M . P q"
proof 
  fix q assume "q  reachable_states M"

  let ?k = "Max (image length {p . path M q p})"
  have "finite {p . path M q p}" using acyclic_finite_paths_from_reachable_state[OF assms(1)] 
    using q  reachable_states M unfolding reachable_states_def by force
  then have k_prop: "( p . path M q p  length p  ?k)" by auto

  moreover have " q k . q  reachable_states M  ( p . path M q p  length p  k)  P q"
  proof -
    fix q k assume "q  reachable_states M" and "( p . path M q p  length p  k)"
    then show "P q" 
    proof (induction k arbitrary: q)
      case 0
      then have "{p . path M q p} = {[]}" using reachable_state_is_state[OF q  reachable_states M]
        by blast  
      then have "LS M q  {[]}" unfolding LS.simps by blast
      then have "deadlock_state M q" using deadlock_state_alt_def by metis
      then show ?case using assms(2)[OF q  reachable_states M] unfolding deadlock_state.simps by blast
    next
      case (Suc k)
      have " t . t  transitions M  (t_source t = q)  P (t_target t)"
      proof -
        fix t assume "t  transitions M" and "t_source t = q" 
        then have "t_target t  reachable_states M"
          using q  reachable_states M using reachable_states_next by metis
        moreover have "p. path M (t_target t) p  length p  k"
          using Suc.prems(2) t  transitions M t_source t = q by auto
        ultimately show "P (t_target t)" 
          using Suc.IH unfolding reachable_states_def by blast 
      qed
      then show ?case using assms(2)[OF Suc.prems(1)] by blast
    qed
  qed

  ultimately show "P q" using q  reachable_states M by blast
qed

lemma reachable_states_induct [consumes 1, case_names init transition] :
  assumes "q  reachable_states M" 
  and "P (initial M)"
  and     " t . t  transitions M  t_source t  reachable_states M  P (t_source t)  P (t_target t)"
shows "P q"
proof -
  from assms(1) obtain p where "path M (initial M) p" and "target (initial M) p = q"
    unfolding reachable_states_def by auto
  then show "P q"
  proof (induction p arbitrary: q rule: rev_induct)
    case Nil
    then show ?case using assms(2) by auto
  next
    case (snoc t p)

    then have "target (initial M) p = t_source t"
      by auto
    then have "P (t_source t)"
      using snoc.IH snoc.prems by auto
    moreover have "t  transitions M"
      using snoc.prems by auto
    moreover have "t_source t  reachable_states M"
      by (metis target (FSM.initial M) p = t_source t path_prefix reachable_states_intro snoc.prems(1))
    moreover have "t_target t = q"
      using snoc.prems by auto
    ultimately show ?case
      using assms(3) by blast
  qed
qed

lemma reachable_states_cases [consumes 1, case_names init transition] : 
  assumes "q  reachable_states M"
  and     "P (initial M)"
  and     " t . t  transitions M  t_source t  reachable_states M  P (t_target t)"
shows "P q"
  by (metis assms(1) assms(2) assms(3) reachable_states_induct)


subsection ‹Further Path Enumeration Algorithms›

fun paths_for_input' :: "('a  ('b × 'c × 'a) set)  'b list  'a  ('a,'b,'c) path  ('a,'b,'c) path set" where
  "paths_for_input' f [] q prev = {prev}" |
  "paths_for_input' f (x#xs) q prev = (image (λ(x',y',q') . paths_for_input' f xs q' (prev@[(q,x,y',q')])) (Set.filter (λ(x',y',q') . x' = x) (f q)))"

lemma paths_for_input'_set :
  assumes "q  states M"
  shows   "paths_for_input' (h_from M) xs q prev = {prev@p | p . path M q p  map fst (p_io p) = xs}"
using assms proof (induction xs arbitrary: q prev)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)

  let ?UN = "(image (λ(x',y',q') . paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])) (Set.filter (λ(x',y',q') . x' = x) (h_from M q)))"

  have "?UN = {prev@p | p . path M q p  map fst (p_io p) = x#xs}"
  proof 
    have " p . p  ?UN  p  {prev@p | p . path M q p  map fst (p_io p) = x#xs}"
    proof -
      fix p assume "p  ?UN"
      then obtain y' q' where "(x,y',q')  (Set.filter (λ(x',y',q') . x' = x) (h_from M q))"
                     and   "p  paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])"
        by auto
      
      from (x,y',q')  (Set.filter (λ(x',y',q') . x' = x) (h_from M q)) have "q'  states M" and "(q,x,y',q')  transitions M"
        using fsm_transition_target unfolding h.simps by auto

      have "p  {(prev @ [(q, x, y', q')]) @ p |p. path M q' p  map fst (p_io p) = xs}"
        using p  paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])
        unfolding Cons.IH[OF q'  states M] by assumption
      moreover have "{(prev @ [(q, x, y', q')]) @ p |p. path M q' p  map fst (p_io p) = xs} 
                       {prev@p | p . path M q p  map fst (p_io p) = x#xs}"
        using (q,x,y',q')  transitions M
        using cons by force 
      ultimately show "p  {prev@p | p . path M q p  map fst (p_io p) = x#xs}" 
        by blast
    qed
    then show "?UN  {prev@p | p . path M q p  map fst (p_io p) = x#xs}"
      by blast

    have " p . p  {prev@p | p . path M q p  map fst (p_io p) = x#xs}  p  ?UN"
    proof -
      fix pp assume "pp  {prev@p | p . path M q p  map fst (p_io p) = x#xs}"
      then obtain p where "pp = prev@p" and "path M q p" and "map fst (p_io p) = x#xs"
        by fastforce
      then obtain t p' where "p = t#p'" and "path M q (t#p')" and "map fst (p_io (t#p')) = x#xs" and "map fst (p_io p') = xs"
        by (metis (no_types, lifting) map_eq_Cons_D)
      then have "path M (t_target t) p'" and "t_source t = q" and "t_input t = x" and "t_target t  states M" and "t  transitions M"
        by auto

      have "(x,t_output t,t_target t)  (Set.filter (λ(x',y',q') . x' = x) (h_from M q))"
        using t  transitions M t_input t = x t_source t = q
        unfolding h.simps by auto 
      moreover have "(prev@p)  paths_for_input' (h_from M) xs (t_target t) (prev@[(q,x,t_output t,t_target t)])"
        using Cons.IH[OF t_target t  states M, of "prev@[(q, x, t_output t, t_target t)]"]
        using thesis. (t p'. p = t # p'; path M q (t # p'); map fst (p_io (t # p')) = x # xs; map fst (p_io p') = xs  thesis)  thesis 
              p = t # p' 
              paths_for_input' (h_from M) xs (t_target t) (prev @ [(q, x, t_output t, t_target t)]) 
                = {(prev @ [(q, x, t_output t, t_target t)]) @ p |p. path M (t_target t) p  map fst (p_io p) = xs} 
              t_input t = x 
              t_source t = q 
        by fastforce

      ultimately show "pp  ?UN" unfolding pp = prev@p
        by blast 
    qed
    then show "{prev@p | p . path M q p  map fst (p_io p) = x#xs}  ?UN"
      by (meson subsetI) 
  qed

  then show ?case
    by (metis paths_for_input'.simps(2)) 
    
qed


definition paths_for_input :: "('a,'b,'c) fsm  'a  'b list  ('a,'b,'c) path set" where
  "paths_for_input M q xs = {p . path M q p  map fst (p_io p) = xs}"

lemma paths_for_input_set_code[code] :
  "paths_for_input M q xs = (if q  states M then paths_for_input' (h_from M) xs q [] else {})"
  using paths_for_input'_set[of q M xs "[]"] 
  unfolding paths_for_input_def
  by (cases "q  states M"; auto; simp add: path_begin_state)


fun paths_up_to_length_or_condition_with_witness' :: 
    "('a  ('b × 'c × 'a) set)  (('a,'b,'c) path  'd option)  ('a,'b,'c) path  nat  'a  (('a,'b,'c) path × 'd) set" 
  where
  "paths_up_to_length_or_condition_with_witness' f P prev 0 q = (case P prev of Some w  {(prev,w)} | None  {})" |
  "paths_up_to_length_or_condition_with_witness' f P prev (Suc k) q = (case P prev of 
    Some w  {(prev,w)} | 
    None  ((image (λ(x,y,q') . paths_up_to_length_or_condition_with_witness' f P (prev@[(q,x,y,q')]) k q') (f q))))"



lemma paths_up_to_length_or_condition_with_witness'_set :
  assumes "q  states M"
  shows   "paths_up_to_length_or_condition_with_witness' (h_from M) P prev k q 
            = {(prev@p,x) | p x . path M q p 
                                   length p  k 
                                   P (prev@p) = Some x 
                                   ( p' p'' . (p = p'@p''  p''  [])  P (prev@p') = None)}"
using assms proof (induction k arbitrary: q prev)
  case 0
  then show ?case proof (cases "P prev")
    case None then show ?thesis by auto
  next
    case (Some w) 
    then show ?thesis by (simp add: "0.prems" nil)
  qed
next
  case (Suc k) 
  then show ?case proof (cases "P prev")
    case (Some w) 
    then have "(prev,w)  {(prev@p,x) | p x . path M q p 
                                               length p  Suc k 
                                               P (prev@p) = Some x 
                                               ( p' p'' . (p = p'@p''  p''  [])  P (prev@p') = None)}"
      by (simp add: Suc.prems nil) 
    then have "{(prev@p,x) | p x . path M q p 
                                     length p  Suc k 
                                     P (prev@p) = Some x 
                                     ( p' p'' . (p = p'@p''  p''  [])  P (prev@p') = None)} 
              = {(prev,w)}"
      using Some by fastforce
      
    then show ?thesis using Some by auto
  next
    case None 

    have "((image (λ(x,y,q') . paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q') (h_from M q))) 
            = {(prev@p,x) | p x . path M q p 
                                   length p  Suc k 
                                   P (prev@p) = Some x 
                                   ( p' p'' . (p = p'@p''  p''  [])  P (prev@p') = None)}"
         (is "?UN = ?PX")
    proof -
      have *: " pp . pp  ?UN  pp  ?PX"
      proof -
        fix pp assume "pp  ?UN"
        then obtain x y q' where "(x,y,q')  h_from M q"
                           and   "pp  paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q'"
          by blast
        then have "(q,x,y,q')  transitions M" by auto
        then have "q'  states M" using fsm_transition_target by auto
        
        obtain p w where "pp = ((prev@[(q,x,y,q')])@p,w)" 
                   and   "path M q' p"
                   and   "length p  k"
                   and   "P ((prev @ [(q, x, y, q')]) @ p) = Some w"
                   and   " p' p''. p = p' @ p''  p''  []  P ((prev @ [(q, x, y, q')]) @ p') = None"
          using pp  paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q' 
          unfolding Suc.IH[OF q'  states M, of "prev@[(q,x,y,q')]"] 
          by blast
        
        have "path M q ((q,x,y,q')#p)" 
          using path M q' p (q,x,y,q')  transitions M by (simp add: path_prepend_t) 
        moreover have "length ((q,x,y,q')#p)  Suc k" 
          using length p  k by auto
        moreover have "P (prev @ ([(q, x, y, q')] @ p)) = Some w" 
          using P ((prev @ [(q, x, y, q')]) @ p) = Some w by auto
        moreover have " p' p''. ((q,x,y,q')#p) = p' @ p''  p''  []  P (prev @ p') = None" 
          using  p' p''. p = p' @ p''  p''  []  P ((prev @ [(q, x, y, q')]) @ p') = None
          using None 
          by (metis (no_types, opaque_lifting) append.simps(1) append_Cons append_Nil2 append_assoc 
                list.inject neq_Nil_conv) 

        ultimately show "pp  ?PX" 
          unfolding pp = ((prev@[(q,x,y,q')])@p,w) by auto  
      qed
      
      have **: " pp . pp  ?PX  pp  ?UN"
      proof -
        fix pp assume "pp  ?PX"
        then obtain p' w where "pp = (prev @ p', w)"
                        and   "path M q p'"
                        and   "length p'  Suc k"
                        and   "P (prev @ p') = Some w"
                        and   " p' p''. p' = p' @ p''  p''  []  P (prev @ p') = None"
          by blast
        moreover obtain t p where "p' = t#p" using P (prev @ p') = Some w using None
          by (metis append_Nil2 list.exhaust option.distinct(1)) 
        
        
        have "pp = ((prev @ [t])@p, w)" 
          using pp = (prev @ p', w) unfolding p' = t#p by auto
        have "path M q (t#p)" 
          using path M q p' unfolding p' = t#p by auto
        have p2: "length (t#p)  Suc k" 
          using length p'  Suc k unfolding p' = t#p by auto
        have p3: "P ((prev @ [t])@p) = Some w" 
          using P (prev @ p') = Some w unfolding p' = t#p by auto
        have p4: " p' p''. p = p' @ p''  p''  []  P ((prev@[t]) @ p') = None"
          using  p' p''. p' = p' @ p''  p''  []  P (prev @ p') = None pp  ?PX 
          unfolding pp = ((prev @ [t]) @ p, w) p' = t#p 
          by auto

        have "t  transitions M" and p1: "path M (t_target t) p" and "t_source t = q"
          using path M q (t#p) by auto
        then have "t_target t  states M" 
              and "(t_input t, t_output t, t_target t)  h_from M q" 
              and "t_source t = q"
          using fsm_transition_target by auto
        then have "t = (q,t_input t, t_output t, t_target t)"
          by auto

        have "((prev @ [t])@p, w)  paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[t]) k (t_target t)"
          unfolding Suc.IH[OF t_target t  states M, of "prev@[t]"]
          using p1 p2 p3 p4 by auto
          

        then show "pp  ?UN"
          unfolding pp = ((prev @ [t])@p, w)  
        proof -
          have "paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [t]) k (t_target t) 
                = paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [(q, t_input t, t_output t, t_target t)]) k (t_target t)"
            using t = (q, t_input t, t_output t, t_target t) by presburger
          then show "((prev @ [t]) @ p, w)  ((b, c, a)h_from M q. paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [(q, b, c, a)]) k a)"
            using ((prev @ [t]) @ p, w)  paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [t]) k (t_target t) 
                  (t_input t, t_output t, t_target t)  h_from M q 
            by blast
        qed
      qed

      show ?thesis
        using subsetI[of ?UN ?PX, OF *] subsetI[of ?PX ?UN, OF **] subset_antisym by blast
    qed

    then show ?thesis 
      using None unfolding paths_up_to_length_or_condition_with_witness'.simps by simp
  qed
qed


definition paths_up_to_length_or_condition_with_witness :: 
  "('a,'b,'c) fsm  (('a,'b,'c) path  'd option)  nat  'a  (('a,'b,'c) path × 'd) set" 
  where
  "paths_up_to_length_or_condition_with_witness M P k q 
    = {(p,x) | p x . path M q p 
                       length p  k 
                       P p = Some x 
                       ( p' p'' . (p = p'@p''  p''  [])  P p' = None)}"


lemma paths_up_to_length_or_condition_with_witness_code[code] :
  "paths_up_to_length_or_condition_with_witness M P k q 
    = (if q  states M then paths_up_to_length_or_condition_with_witness' (h_from M) P [] k q
                      else {})" 
proof (cases "q  states M")
  case True
  then show ?thesis 
    unfolding paths_up_to_length_or_condition_with_witness_def 
              paths_up_to_length_or_condition_with_witness'_set[OF True] 
    by auto
next
  case False
  then show ?thesis 
    unfolding paths_up_to_length_or_condition_with_witness_def
    using path_begin_state by fastforce 
qed


lemma paths_up_to_length_or_condition_with_witness_finite : 
  "finite (paths_up_to_length_or_condition_with_witness M P k q)"
proof -
  have "paths_up_to_length_or_condition_with_witness M P k q 
           {(p, the (P p)) | p . path M q p  length p  k}"
    unfolding paths_up_to_length_or_condition_with_witness_def
    by auto 
  moreover have "finite {(p, the (P p)) | p . path M q p  length p  k}" 
    using paths_finite[of M q k]
    by simp 
  ultimately show ?thesis
    using rev_finite_subset by auto 
qed

  


subsection ‹More Acyclicity Properties›


lemma maximal_path_target_deadlock :
  assumes "path M (initial M) p"
  and     "¬( p' . path M (initial M) p'  is_prefix p p'  p  p')"
shows "deadlock_state M (target (initial M) p)"
proof -
  have "¬( t  transitions M . t_source t = target (initial M) p)"
    using assms(2) unfolding is_prefix_prefix
    by (metis append_Nil2 assms(1) not_Cons_self2 path_append_transition same_append_eq)
  then show ?thesis by auto
qed

lemma path_to_deadlock_is_maximal :
  assumes "path M (initial M) p"
  and     "deadlock_state M (target (initial M) p)"
shows "¬( p' . path M (initial M) p'  is_prefix p p'  p  p')"
proof 
  assume "p'. path M (initial M) p'  is_prefix p p'  p  p'"
  then obtain p' where "path M (initial M) p'" and "is_prefix p p'" and "p  p'" by blast
  then have "length p' > length p"
    unfolding is_prefix_prefix by auto
  then obtain t p2 where "p' = p @ [t] @ p2"
    using is_prefix p p' unfolding is_prefix_prefix
    by (metis p  p' append.left_neutral append_Cons append_Nil2 non_sym_dist_pairs'.cases) 
  then have "path M (initial M) (p@[t])"
    using path M (initial M) p' by auto
  then have "t  transitions M" and "t_source t = target (initial M) p"
    by auto
  then show "False"
    using deadlock_state M (target (initial M) p) unfolding deadlock_state.simps by blast
qed



definition maximal_acyclic_paths :: "('a,'b,'c) fsm  ('a,'b,'c) path set" where
  "maximal_acyclic_paths M = {p . path M (initial M) p 
                                   distinct (visited_states (initial M) p) 
                                   ¬( p' . p'  []  path M (initial M) (p@p') 
                                               distinct (visited_states (initial M) (p@p')))}"


(* very inefficient construction *)
lemma maximal_acyclic_paths_code[code] :  
  "maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (initial M) (size M - 1)
                               in Set.filter (λp . ¬ ( p'  ps . p'  p  is_prefix p p')) ps)"
proof -
  have scheme1: " P p . ( p' . p'  []  P (p@p')) = ( p'  {p . P p} . p'  p  is_prefix p p')"
    unfolding is_prefix_prefix by blast

  have scheme2: " p . (path M (FSM.initial M) p 
                           length p  FSM.size M - 1 
                           distinct (visited_states (FSM.initial M) p)) 
                      = (path M (FSM.initial M) p  distinct (visited_states (FSM.initial M) p))"
    using acyclic_path_length_limit by fastforce 

  show ?thesis
    unfolding maximal_acyclic_paths_def acyclic_paths_up_to_length.simps Let_def 
    unfolding scheme1[of "λp . path M (initial M) p  distinct (visited_states (initial M) p)"]
    unfolding scheme2 by fastforce
qed



lemma maximal_acyclic_path_deadlock :
  assumes "acyclic M"
  and     "path M (initial M) p"
shows "¬( p' . p'  []  path M (initial M) (p@p')  distinct (visited_states (initial M) (p@p'))) 
        = deadlock_state M (target (initial M) p)"
proof -
  have "deadlock_state M (target (initial M) p)  ¬( p' . p'  []  path M (initial M) (p@p') 
           distinct (visited_states (initial M) (p@p')))"
    unfolding deadlock_state.simps 
    using assms(2) by (metis path.cases path_suffix) 
  then show ?thesis
    by (metis acyclic.elims(2) assms(1) assms(2) is_prefix_prefix maximal_path_target_deadlock 
          self_append_conv) 
qed
  

lemma maximal_acyclic_paths_deadlock_targets : 
  assumes "acyclic M"
  shows "maximal_acyclic_paths M 
          = { p . path M (initial M) p  deadlock_state M (target (initial M) p)}"
  using maximal_acyclic_path_deadlock[OF assms] 
  unfolding maximal_acyclic_paths_def
  by (metis (no_types, lifting) acyclic.elims(2) assms)


lemma cycle_from_cyclic_path :
  assumes "path M q p"
  and     "¬ distinct (visited_states q p)"
obtains i j where
  "take j (drop i p)  []"
  "target (target q (take i p)) (take j (drop i p)) = (target q (take i p))"
  "path M (target q (take i p)) (take j (drop i p))"
proof -
  obtain i j where "i < j" and "j < length (visited_states q p)" 
               and "(visited_states q p) ! i = (visited_states q p) ! j"
    using assms(2) non_distinct_repetition_indices by blast 

  have "(target q (take i p)) = (visited_states q p) ! i"
    using i < j j < length (visited_states q p)
    by (metis less_trans take_last_index target.simps visited_states_take)

  then have "(target q (take i p)) = (visited_states q p) ! j"
    using (visited_states q p) ! i = (visited_states q p) ! j by auto

  have p1: "take (j-i) (drop i p)  []"
    using i < j j < length (visited_states q p) by auto 

  have "target (target q (take i p)) (take (j-i) (drop i p)) = (target q (take j p))"
    using i < j by (metis add_diff_inverse_nat less_asym' path_append_target take_add)
  then have p2: "target (target q (take i p)) (take (j-i) (drop i p)) = (target q (take i p))"
    using (target q (take i p)) = (visited_states q p) ! i
    using (target q (take i p)) = (visited_states q p) ! j
    by (metis j < length (visited_states q p) take_last_index target.simps visited_states_take)

  have p3: "path M (target q (take i p)) (take (j-i) (drop i p))"
    by (metis append_take_drop_id assms(1) path_append_elim)

  show ?thesis using p1 p2 p3 that by blast
qed



lemma acyclic_single_deadlock_reachable :
  assumes "acyclic M"
  and     " q' . q'  reachable_states M  q' = qd  ¬ deadlock_state M q'"
shows "qd  reachable_states M"
  using acyclic_deadlock_reachable[OF assms(1)]
  using assms(2) by auto 


lemma acyclic_paths_to_single_deadlock :
  assumes "acyclic M"
  and     " q' . q'  reachable_states M  q' = qd  ¬ deadlock_state M q'"
  and     "q  reachable_states M"
obtains p where "path M q p" and "target q p = qd"
proof -
  have "q  states M" using assms(3) reachable_state_is_state by metis
  have "acyclic (from_FSM M q)"
    using from_FSM_acyclic[OF assms(3,1)] by assumption

  have *: "(q'. q'  reachable_states (FSM.from_FSM M q) 
                 q' = qd  ¬ deadlock_state (FSM.from_FSM M q) q')"
    using assms(2) from_FSM_reachable_states[OF assms(3)] 
    unfolding deadlock_state.simps from_FSM_simps[OF q  states M] by blast

  obtain p where "path (from_FSM M q) q p" and "target q p = qd"
    using acyclic_single_deadlock_reachable[OF acyclic (from_FSM M q) *]
    unfolding reachable_states_def from_FSM_simps[OF q  states M]
    by blast 

  then show ?thesis
    using that by (metis q  FSM.states M from_FSM_path) 
qed



subsection ‹Elements as Lists›

fun states_as_list :: "('a :: linorder, 'b, 'c) fsm  'a list" where
  "states_as_list M = sorted_list_of_set (states M)"

lemma states_as_list_distinct : "distinct (states_as_list M)" by auto

lemma states_as_list_set : "set (states_as_list M) = states M"
  by (simp add: fsm_states_finite)


fun reachable_states_as_list :: "('a :: linorder, 'b, 'c) fsm  'a list" where
  "reachable_states_as_list M = sorted_list_of_set (reachable_states M)"

lemma reachable_states_as_list_distinct : "distinct (reachable_states_as_list M)" by auto

lemma reachable_states_as_list_set : "set (reachable_states_as_list M) = reachable_states M"
  by (metis fsm_states_finite infinite_super reachable_state_is_state reachable_states_as_list.simps 
        set_sorted_list_of_set subsetI)  


fun inputs_as_list :: "('a, 'b :: linorder, 'c) fsm  'b list" where
  "inputs_as_list M = sorted_list_of_set (inputs M)"

lemma inputs_as_list_set : "set (inputs_as_list M) = inputs M"
  by (simp add: fsm_inputs_finite)

lemma inputs_as_list_distinct : "distinct (inputs_as_list M)" by auto

fun transitions_as_list :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm  ('a,'b,'c) transition list" where
  "transitions_as_list M = sorted_list_of_set (transitions M)"

lemma transitions_as_list_set : "set (transitions_as_list M) = transitions M"
  by (simp add: fsm_transitions_finite)

fun outputs_as_list :: "('a,'b,'c :: linorder) fsm  'c list" where
  "outputs_as_list M = sorted_list_of_set (outputs M)"

lemma outputs_as_list_set : "set (outputs_as_list M) = outputs M"
  by (simp add: fsm_outputs_finite)

fun ftransitions :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm  ('a,'b,'c) transition fset" where
  "ftransitions M = fset_of_list (transitions_as_list M)"

fun fstates :: "('a :: linorder,'b,'c) fsm  'a fset" where
  "fstates M = fset_of_list (states_as_list M)"

fun finputs :: "('a,'b :: linorder,'c) fsm  'b fset" where
  "finputs M = fset_of_list (inputs_as_list M)"

fun foutputs :: "('a,'b,'c :: linorder) fsm  'c fset" where
  "foutputs M = fset_of_list (outputs_as_list M)"

lemma fstates_set : "fset (fstates M) = states M" 
  using fsm_states_finite[of M] by (simp add: fset_of_list.rep_eq) 

lemma finputs_set : "fset (finputs M) = inputs M" 
  using fsm_inputs_finite[of M] by (simp add: fset_of_list.rep_eq) 

lemma foutputs_set : "fset (foutputs M) = outputs M" 
  using fsm_outputs_finite[of M] by (simp add: fset_of_list.rep_eq) 

lemma ftransitions_set: "fset (ftransitions M) = transitions M"
  by (metis (no_types) fset_of_list.rep_eq ftransitions.simps transitions_as_list_set)

lemma ftransitions_source:
  "q |∈| (t_source |`| ftransitions M)  q  states M" 
  using ftransitions_set[of M] fsm_transition_source[of _ M]
  by (metis (no_types, opaque_lifting) fimageE)

lemma ftransitions_target:
  "q |∈| (t_target |`| ftransitions M)  q  states M" 
  using ftransitions_set[of M] fsm_transition_target[of _ M]
  by (metis (no_types, lifting) fimageE)


subsection ‹Responses to Input Sequences›

fun language_for_input :: "('a::linorder,'b::linorder,'c::linorder) fsm  'a  'b list  ('b×'c) list list" where
  "language_for_input M q [] = [[]]" |
  "language_for_input M q (x#xs) = 
      (let outs = outputs_as_list M
        in concat (map (λy . case h_obs M q x y of None  [] | Some q'  map ((#) (x,y)) (language_for_input M q' xs)) outs))"  

lemma language_for_input_set :
  assumes "observable M"
  and     "q  states M"
shows "list.set (language_for_input M q xs) = {io . io  LS M q  map fst io = xs}"
  using assms(2) proof (induction xs arbitrary: q)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)

  have "list.set (language_for_input M q (x#xs))  {io . io  LS M q  map fst io = (x#xs)}"
  proof 
    fix io assume "io  list.set (language_for_input M q (x#xs))"
    then obtain y where "y  outputs M"
                    and "io  list.set (case h_obs M q x y of None  [] | Some q'  map ((#) (x,y)) (language_for_input M q' xs))"
      unfolding outputs_as_list_set[symmetric]
      by auto
    then obtain q' where "h_obs M q x y = Some q'" and "io  list.set (map ((#) (x,y)) (language_for_input M q' xs))"
      by (cases "h_obs M q x y"; auto)

    then obtain io' where "io = (x,y)#io'"
                      and "io'  list.set (language_for_input M q' xs)"
      by auto

    then have "io'  LS M q'" and "map fst io' = xs"
      using Cons.IH[OF h_obs_state[OF h_obs M q x y = Some q']]
      by blast+
    then have "(x,y)#io'  LS M q"
      using h_obs M q x y = Some q'
      unfolding h_obs_language_iff[OF assms(1), of x y io' q] 
      by blast
    then show "io  {io . io  LS M q  map fst io = (x#xs)}"
      unfolding io = (x,y)#io' 
      using map fst io' = xs
      by auto
  qed
  moreover have "{io . io  LS M q  map fst io = (x#xs)}  list.set (language_for_input M q (x#xs))"
  proof 
    have scheme : " x y f xs . y  list.set (f x)  x  list.set xs  y  list.set (concat (map f xs))"
      by auto

    fix io assume "io  {io . io  LS M q  map fst io = (x#xs)}"
    then have "io  LS M q" and "map fst io = (x#xs)"
      by auto
    then obtain y io' where "io = (x,y)#io'"
      by fastforce
    then have "(x,y)#io'  LS M q"
      using io  LS M q
      by auto
    then obtain q' where "h_obs M q x y = Some q'" and "io'  LS M q'"
      unfolding h_obs_language_iff[OF assms(1), of x y io' q] 
      by blast
    moreover have "io'  list.set (language_for_input M q' xs)"
      using Cons.IH[OF h_obs_state[OF h_obs M q x y = Some q']] io'  LS M q' map fst io = (x#xs)
      unfolding io = (x,y)#io' by auto
    ultimately have "io  list.set ((λ y .(case h_obs M q x y of None  [] | Some q'  map ((#) (x,y)) (language_for_input M q' xs))) y)"
      unfolding io = (x,y)#io'
      by force 
    moreover have "y  list.set (outputs_as_list M)"
      unfolding outputs_as_list_set
      using language_io(2)[OF (x,y)#io'  LS M q] by auto
    ultimately show "io  list.set (language_for_input M q (x#xs))"
      unfolding language_for_input.simps Let_def
      using scheme[of io "(λ y .(case h_obs M q x y of None  [] | Some q'  map ((#) (x,y)) (language_for_input M q' xs)))" y]
      by blast
  qed
  ultimately show ?case
    by blast
qed


subsection ‹Filtering Transitions›

lift_definition filter_transitions :: 
  "('a,'b,'c) fsm  (('a,'b,'c) transition  bool)  ('a,'b,'c) fsm" is FSM_Impl.filter_transitions 
proof -
  fix M  :: "('a,'b,'c) fsm_impl"
  fix P  :: "('a,'b,'c) transition  bool"
  assume "well_formed_fsm M"
  then show "well_formed_fsm (FSM_Impl.filter_transitions M P)" 
    unfolding FSM_Impl.filter_transitions.simps by force
qed


lemma filter_transitions_simps[simp] :
  "initial (filter_transitions M P) = initial M"
  "states (filter_transitions M P) = states M"
  "inputs (filter_transitions M P) = inputs M"
  "outputs (filter_transitions M P) = outputs M"
  "transitions (filter_transitions M P) = {t  transitions M . P t}"
  by (transfer;auto)+


lemma filter_transitions_submachine :
  "is_submachine (filter_transitions M P) M" 
  unfolding filter_transitions_simps by fastforce


lemma filter_transitions_path :
  assumes "path (filter_transitions M P) q p"
  shows "path M q p"
  using path_begin_state[OF assms] 
        transition_subset_path[of "filter_transitions M P" M, OF _ assms]
  unfolding filter_transitions_simps by blast

lemma filter_transitions_reachable_states :
  assumes "q  reachable_states (filter_transitions M P)"
  shows "q  reachable_states M"
  using assms unfolding reachable_states_def filter_transitions_simps 
  using filter_transitions_path[of M P "initial M"]
  by blast


subsection ‹Filtering States›

lift_definition filter_states :: "('a,'b,'c) fsm  ('a  bool)  ('a,'b,'c) fsm" 
  is FSM_Impl.filter_states 
proof -
  fix M  :: "('a,'b,'c) fsm_impl"
  fix P  :: "'a  bool"
  assume *: "well_formed_fsm M"

  then show "well_formed_fsm (FSM_Impl.filter_states M P)" 
    by (cases "P (FSM_Impl.initial M)"; auto)
qed

lemma filter_states_simps[simp] :
  assumes "P (initial M)"
shows "initial (filter_states M P) = initial M"
      "states (filter_states M P) = Set.filter P (states M)"
      "inputs (filter_states M P) = inputs M"
      "outputs (filter_states M P) = outputs M"
      "transitions (filter_states M P) = {t  transitions M . P (t_source t)  P (t_target t)}"
  using assms by (transfer;auto)+


lemma filter_states_submachine :
  assumes "P (initial M)"
  shows "is_submachine (filter_states M P) M" 
  using filter_states_simps[of P M, OF assms] by fastforce



fun restrict_to_reachable_states :: "('a,'b,'c) fsm  ('a,'b,'c) fsm" where
  "restrict_to_reachable_states M = filter_states M (λ q . q  reachable_states M)"


lemma restrict_to_reachable_states_simps[simp] :
shows "initial (restrict_to_reachable_states M) = initial M"
      "states (restrict_to_reachable_states M) = reachable_states M"
      "inputs (restrict_to_reachable_states M) = inputs M"
      "outputs (restrict_to_reachable_states M) = outputs M"
      "transitions (restrict_to_reachable_states M) 
          = {t  transitions M . (t_source t)  reachable_states M}"
proof -
  show "initial (restrict_to_reachable_states M) = initial M"
       "states (restrict_to_reachable_states M) = reachable_states M"
       "inputs (restrict_to_reachable_states M) = inputs M"
       "outputs (restrict_to_reachable_states M) = outputs M"
      
    using filter_states_simps[of "(λ q . q  reachable_states M)", OF reachable_states_initial] 
    using reachable_state_is_state[of _ M] by auto

  have "transitions (restrict_to_reachable_states M) 
          = {t  transitions M. (t_source t)  reachable_states M  (t_target t)  reachable_states M}"
    using filter_states_simps[of "(λ q . q  reachable_states M)", OF reachable_states_initial] 
    by auto
  then show "transitions (restrict_to_reachable_states M) 
              = {t  transitions M . (t_source t)  reachable_states M}"
    using reachable_states_next[of _ M] by auto
qed


lemma restrict_to_reachable_states_path :
  assumes "q  reachable_states M"
  shows "path M q p = path (restrict_to_reachable_states M) q p"
proof 
  show "path M q p  path (restrict_to_reachable_states M) q p"
  proof -
    assume "path M q p"
    then show "path (restrict_to_reachable_states M) q p" 
    using assms proof (induction p arbitrary: q rule: list.induct)
      case Nil
      then show ?case
        using restrict_to_reachable_states_simps(2) by fastforce 
    next
      case (Cons t' p')
      then have "path M (t_target t') p'" by auto
      moreover have "t_target t'  reachable_states M" using Cons.prems
        by (metis path_cons_elim reachable_states_next) 
      ultimately show ?case using Cons.IH
        by (metis (no_types, lifting) Cons.prems(1) Cons.prems(2) mem_Collect_eq path.simps 
              path_cons_elim restrict_to_reachable_states_simps(5))        
    qed
  qed

  show "path (restrict_to_reachable_states M) q p  path M q p"
    by (metis (no_types, lifting) assms mem_Collect_eq reachable_state_is_state 
          restrict_to_reachable_states_simps(5) subsetI transition_subset_path)
qed

lemma restrict_to_reachable_states_language :
  "L (restrict_to_reachable_states M) = L M"
  unfolding LS.simps
  unfolding restrict_to_reachable_states_simps
  unfolding restrict_to_reachable_states_path[OF reachable_states_initial, of M]
  by blast

lemma restrict_to_reachable_states_observable :
  assumes "observable M"
shows "observable (restrict_to_reachable_states M)"
  using assms unfolding observable.simps
  unfolding restrict_to_reachable_states_simps
  by blast

lemma restrict_to_reachable_states_minimal :
  assumes "minimal M"
  shows "minimal (restrict_to_reachable_states M)"
proof -
  have " q1 q2 . q1  reachable_states M 
                   q2  reachable_states M 
                   q1  q2  
                   LS (restrict_to_reachable_states M) q1  LS (restrict_to_reachable_states M) q2" 
  proof -
    fix q1 q2 assume "q1  reachable_states M" and "q2  reachable_states M" and "q1  q2"
    then have "q1  states M" and "q2  states M"
      by (simp add: reachable_state_is_state)+
    then have "LS M q1  LS M q2"
      using q1  q2 assms by auto
    then show "LS (restrict_to_reachable_states M) q1  LS (restrict_to_reachable_states M) q2"
      unfolding LS.simps
      unfolding restrict_to_reachable_states_path[OF q1  reachable_states M]
      unfolding restrict_to_reachable_states_path[OF q2  reachable_states M] .
  qed
  then show ?thesis
    unfolding minimal.simps restrict_to_reachable_states_simps
    by blast
qed

lemma restrict_to_reachable_states_reachable_states :
  "reachable_states (restrict_to_reachable_states M) = states (restrict_to_reachable_states M)"
proof 
  show "reachable_states (restrict_to_reachable_states M)  states (restrict_to_reachable_states M)"
    by (simp add: reachable_state_is_state subsetI) 
  show "states (restrict_to_reachable_states M)  reachable_states (restrict_to_reachable_states M)"
  proof 
    fix q assume "q  states (restrict_to_reachable_states M)"
    then have "q  reachable_states M"
      unfolding restrict_to_reachable_states_simps .
    then show "q  reachable_states (restrict_to_reachable_states M)"
      unfolding reachable_states_def 
      unfolding restrict_to_reachable_states_simps
      unfolding restrict_to_reachable_states_path[OF reachable_states_initial, symmetric] .
  qed
qed


subsection ‹Adding Transitions›

lift_definition create_unconnected_fsm :: "'a  'a set  'b set  'c set  ('a,'b,'c) fsm" 
  is FSM_Impl.create_unconnected_FSMI by (transfer; simp)

lemma create_unconnected_fsm_simps :
  assumes "finite ns" and "finite ins" and "finite outs" and "q  ns"
  shows "initial (create_unconnected_fsm q ns ins outs) = q"
        "states (create_unconnected_fsm q ns ins outs)   = ns"
        "inputs (create_unconnected_fsm q ns ins outs)  = ins"
        "outputs (create_unconnected_fsm q ns ins outs) = outs"
        "transitions (create_unconnected_fsm q ns ins outs) = {}"
  using assms by (transfer; auto)+

lift_definition create_unconnected_fsm_from_lists :: "'a  'a list  'b list  'c list  ('a,'b,'c) fsm" 
  is FSM_Impl.create_unconnected_fsm_from_lists by (transfer; simp)

lemma create_unconnected_fsm_from_lists_simps :
  assumes "q  set ns"
  shows "initial (create_unconnected_fsm_from_lists q ns ins outs) = q"
        "states (create_unconnected_fsm_from_lists q ns ins outs)  = set ns"
        "inputs (create_unconnected_fsm_from_lists q ns ins outs)  = set ins"
        "outputs (create_unconnected_fsm_from_lists q ns ins outs) = set outs"
        "transitions (create_unconnected_fsm_from_lists q ns ins outs) = {}"
  using assms by (transfer; auto)+

lift_definition create_unconnected_fsm_from_fsets :: "'a  'a fset  'b fset  'c fset  ('a,'b,'c) fsm" 
  is FSM_Impl.create_unconnected_fsm_from_fsets by (transfer; simp)

lemma create_unconnected_fsm_from_fsets_simps :
  assumes "q |∈| ns"
  shows "initial (create_unconnected_fsm_from_fsets q ns ins outs) = q"
        "states (create_unconnected_fsm_from_fsets q ns ins outs)   = fset ns"
        "inputs (create_unconnected_fsm_from_fsets q ns ins outs)  = fset ins"
        "outputs (create_unconnected_fsm_from_fsets q ns ins outs) = fset outs"
        "transitions (create_unconnected_fsm_from_fsets q ns ins outs) = {}"
  using assms by (transfer; auto)+


lift_definition add_transitions :: "('a,'b,'c) fsm  ('a,'b,'c) transition set  ('a,'b,'c) fsm" 
  is FSM_Impl.add_transitions 
proof -
  fix M  :: "('a,'b,'c) fsm_impl"
  fix ts :: "('a,'b,'c) transition set"
  assume *: "well_formed_fsm M"

  then show "well_formed_fsm (FSM_Impl.add_transitions M ts)" 
  proof (cases " t  ts . t_source t  FSM_Impl.states M  t_input t  FSM_Impl.inputs M 
                             t_output t  FSM_Impl.outputs M  t_target t  FSM_Impl.states M")
    case True
    then have "ts  FSM_Impl.states M × FSM_Impl.inputs M × FSM_Impl.outputs M × FSM_Impl.states M" 
      by fastforce
    moreover have "finite (FSM_Impl.states M × FSM_Impl.inputs M × FSM_Impl.outputs M × FSM_Impl.states M)" 
      using * by blast
    ultimately have "finite ts"
      using rev_finite_subset by auto 
    then show ?thesis using * by auto
  next
    case False
    then show ?thesis using * by auto
  qed
qed


lemma add_transitions_simps :
  assumes " t . t  ts  t_source t  states M  t_input t  inputs M  t_output t  outputs M  t_target t  states M"
  shows "initial (add_transitions M ts) = initial M"
        "states (add_transitions M ts)  = states M"
        "inputs (add_transitions M ts)  = inputs M"
        "outputs (add_transitions M ts) = outputs M"
        "transitions (add_transitions M ts) = transitions M  ts"
  using assms by (transfer; auto)+



lift_definition create_fsm_from_sets :: "'a  'a set  'b set  'c set  ('a,'b,'c) transition set  ('a,'b,'c) fsm" 
  is FSM_Impl.create_fsm_from_sets
proof -
  fix q :: 'a
  fix qs :: "'a set"
  fix ins :: "'b set"
  fix outs :: "'c set"
  fix ts :: "('a,'b,'c) transition set"

  show "well_formed_fsm (FSM_Impl.create_fsm_from_sets q qs ins outs ts)"
  proof (cases "q  qs  finite qs  finite ins  finite outs")
    case True

    let ?M = "(FSMI q qs ins outs {})"

    show ?thesis proof (cases " t  ts . t_source t  FSM_Impl.states ?M  t_input t  FSM_Impl.inputs ?M 
                             t_output t  FSM_Impl.outputs ?M  t_target t  FSM_Impl.states ?M")
      case True
      then have "ts  FSM_Impl.states ?M × FSM_Impl.inputs ?M × FSM_Impl.outputs ?M × FSM_Impl.states ?M" 
        by fastforce
      moreover have "finite (FSM_Impl.states ?M × FSM_Impl.inputs ?M × FSM_Impl.outputs ?M × FSM_Impl.states ?M)" 
        using q  qs  finite qs  finite ins  finite outs by force
      ultimately have "finite ts"
        using rev_finite_subset by auto 
      then show ?thesis by auto
    next
      case False
      then show ?thesis by auto
    qed
  next
    case False
    then show ?thesis by auto
  qed
qed

lemma create_fsm_from_sets_simps :
  assumes "q  qs" and "finite qs" and "finite ins" and "finite outs"
  assumes " t . t  ts  t_source t  qs  t_input t  ins  t_output t  outs  t_target t  qs"
  shows "initial (create_fsm_from_sets q qs ins outs ts) = q"
        "states (create_fsm_from_sets q qs ins outs ts)  = qs"
        "inputs (create_fsm_from_sets q qs ins outs ts)  = ins"
        "outputs (create_fsm_from_sets q qs ins outs ts) = outs"
        "transitions (create_fsm_from_sets q qs ins outs ts) = ts"
  using assms by (transfer; auto)+

lemma create_fsm_from_self : 
  "m = create_fsm_from_sets (initial m) (states m) (inputs m) (outputs m) (transitions m)"
proof -
  have *: " t . t  transitions m  t_source t  states m  t_input t  inputs m  t_output t  outputs m  t_target t  states m"
    by auto
  show ?thesis
    using create_fsm_from_sets_simps[OF fsm_initial fsm_states_finite fsm_inputs_finite fsm_outputs_finite *, of "transitions m"]
    apply transfer
    by force
qed

lemma create_fsm_from_sets_surj : 
  assumes "finite (UNIV :: 'a set)" 
  and     "finite (UNIV :: 'b set)" 
  and     "finite (UNIV :: 'c set)"
shows "surj (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)" 
proof
  show "range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)  UNIV"
    by simp
  show "UNIV  range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)"    
  proof 
    fix m assume "m  (UNIV :: ('a,'b,'c) fsm set)"
    then have "m = create_fsm_from_sets (initial m) (states m) (inputs m) (outputs m) (transitions m)"
      using create_fsm_from_self by blast
    then have "m = (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T) (initial m,states m,inputs m,outputs m,transitions m)"
      by auto
    then show "m  range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)"
      by blast
  qed
qed
      


subsection ‹Distinguishability›

definition distinguishes :: "('a,'b,'c) fsm  'a  'a  ('b ×'c) list  bool" where
  "distinguishes M q1 q2 io = (io  LS M q1  LS M q2  io  LS M q1  LS M q2)"

definition minimally_distinguishes :: "('a,'b,'c) fsm  'a  'a  ('b ×'c) list  bool" where
  "minimally_distinguishes M q1 q2 io = (distinguishes M q1 q2 io
                                           ( io' . distinguishes M q1 q2 io'  length io  length io'))"

lemma minimally_distinguishes_ex :
  assumes "q1  states M"
      and "q2  states M"
      and "LS M q1  LS M q2"
obtains v where "minimally_distinguishes M q1 q2 v"
proof -
  let ?vs = "{v . distinguishes M q1 q2 v}"
  define vMin where vMin: "vMin = arg_min length (λv . v  ?vs)"
  
  obtain v' where "distinguishes M q1 q2 v'"
    using assms unfolding distinguishes_def by blast
  then have "vMin  ?vs  ( v'' . distinguishes M q1 q2 v''  length vMin  length v'')"
    unfolding vMin using arg_min_nat_lemma[of "λv . distinguishes M q1 q2 v" v' length]
    by simp
  then show ?thesis 
    using that[of vMin] unfolding minimally_distinguishes_def by blast
qed

lemma distinguish_prepend :
  assumes "observable M"
      and "distinguishes M (FSM.after M q1 io) (FSM.after M q2 io) w"
      and "q1  states M"
      and "q2  states M"
      and "io  LS M q1"
      and "io  LS M q2"
shows "distinguishes M q1 q2 (io@w)"
proof -
  have "(io@w  LS M q1) = (w  LS M (after M q1 io))"
    using assms(1,3,5)
    by (metis after_language_iff)
  moreover have "(io@w  LS M q2) = (w  LS M (after M q2 io))"
    using assms(1,4,6)
    by (metis after_language_iff)
  ultimately show ?thesis
    using assms(2) unfolding distinguishes_def by blast
qed 

lemma distinguish_prepend_initial :
  assumes "observable M"
      and "distinguishes M (after_initial M (io1@io)) (after_initial M (io2@io)) w"
      and "io1@io  L M"
      and "io2@io  L M"
shows "distinguishes M (after_initial M io1) (after_initial M io2) (io@w)"
proof -
have f1: "ps psa f a. (ps::('b × 'c) list) @ psa  LS f (a::'a)  ps  LS f a"
  by (meson language_prefix)
  then have f2: "io1  L M"
    by (meson assms(3))
  have f3: "io2  L M"
    using f1 by (metis assms(4))
  have "io1  L M"
    using f1 by (metis assms(3))
  then show ?thesis
    by (metis after_is_state after_language_iff after_split assms(1) assms(2) assms(3) assms(4) distinguish_prepend f3)
qed

lemma minimally_distinguishes_no_prefix :
  assumes "observable M"
  and     "u@w  L M"
  and     "v@w  L M"
  and     "minimally_distinguishes M (after_initial M u) (after_initial M v) (w@w'@w'')"
  and     "w'  []"
shows "¬distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w''"
proof 
  assume "distinguishes M (after_initial M (u @ w)) (after_initial M (v @ w)) w''"
  then have "distinguishes M (after_initial M u) (after_initial M v) (w@w'')"
    using assms(1-3) distinguish_prepend_initial by blast
  moreover have "length (w@w'') < length (w@w'@w'')"
    using assms(5) by auto
  ultimately show False
    using assms(4) unfolding minimally_distinguishes_def
    using leD by blast 
qed


lemma minimally_distinguishes_after_append :
  assumes "observable M"
  and     "minimal M"
  and     "q1  states M"
  and     "q2  states M"
  and     "minimally_distinguishes M q1 q2 (w@w')"
  and     "w'  []"
shows "minimally_distinguishes M (after M q1 w) (after M q2 w) w'"
proof -
  have "¬ distinguishes M q1 q2 w"
    using assms(5,6)
    by (metis add.right_neutral add_le_cancel_left length_append length_greater_0_conv linorder_not_le minimally_distinguishes_def)
  then have "w  LS M q1 = (w  LS M q2)"
    unfolding distinguishes_def
    by blast 
  moreover have "(w@w')  LS M q1  LS M q2"
    using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
    by blast
  ultimately have "w  LS M q1" and "w  LS M q2"
    by (meson Un_iff language_prefix)+

  have "(w@w')  LS M q1 = (w'  LS M (after M q1 w))"
    by (meson w  LS M q1 after_language_iff assms(1))
  moreover have "(w@w')  LS M q2 = (w'  LS M (after M q2 w))"
    by (meson w  LS M q2 after_language_iff assms(1))
  ultimately have "distinguishes M (after M q1 w) (after M q2 w) w'"
    using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
    by blast
  moreover have " w'' . distinguishes M (after M q1 w) (after M q2 w) w''  length w'  length w''"
  proof -
    fix w'' assume "distinguishes M (after M q1 w) (after M q2 w) w''"
    then have "distinguishes M q1 q2 (w@w'')"
      by (metis w  LS M q1 w  LS M q2 assms(1) assms(3) assms(4) distinguish_prepend)
    then have "length (w@w')  length (w@w'')"
      using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
      by blast
    then show "length w'  length w''"
      by auto
  qed
  ultimately show ?thesis 
    unfolding minimally_distinguishes_def distinguishes_def 
    by blast
qed



lemma minimally_distinguishes_after_append_initial :
  assumes "observable M"
  and     "minimal M"
  and     "u  L M"
  and     "v  L M"
  and     "minimally_distinguishes M (after_initial M u) (after_initial M v) (w@w')"
  and     "w'  []"
shows "minimally_distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w'"
proof -

  have "¬ distinguishes M (after_initial M u) (after_initial M v) w"
    using assms(5,6)
    by (metis add.right_neutral add_le_cancel_left length_append length_greater_0_conv linorder_not_le minimally_distinguishes_def)    
  then have "w  LS M (after_initial M u) = (w  LS M (after_initial M v))"
    unfolding distinguishes_def
    by blast 
  moreover have "(w@w')  LS M (after_initial M u)  LS M (after_initial M v)"
    using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
    by blast
  ultimately have "w  LS M (after_initial M u)" and "w  LS M (after_initial M v)"
    by (meson Un_iff language_prefix)+

  have "(w@w')  LS M (after_initial M u) = (w'  LS M (after_initial M (u@w)))"
    by (meson w  LS M (after_initial M u) after_language_append_iff after_language_iff assms(1) assms(3))
  moreover have "(w@w')  LS M (after_initial M v) = (w'  LS M (after_initial M (v@w)))"
    by (meson w  LS M (after_initial M v) after_language_append_iff after_language_iff assms(1) assms(4))
  ultimately have "distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w'"
    using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
    by blast
  moreover have " w'' . distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w''  length w'  length w''"
  proof -
    fix w'' assume "distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w''"
    then have "distinguishes M (after_initial M u) (after_initial M v) (w@w'')"
      by (meson w  LS M (after_initial M u) w  LS M (after_initial M v) after_language_iff assms(1) assms(3) assms(4) distinguish_prepend_initial)
    then have "length (w@w')  length (w@w'')"
      using assms(5) unfolding minimally_distinguishes_def distinguishes_def 
      by blast
    then show "length w'  length w''"
      by auto
  qed
  ultimately show ?thesis 
    unfolding minimally_distinguishes_def distinguishes_def 
    by blast
qed



lemma minimally_distinguishes_proper_prefixes_card :
  assumes "observable M"
  and     "minimal M"
  and     "q1  states M"
  and     "q2  states M"
  and     "minimally_distinguishes M q1 q2 w"
  and     "S  states M"
shows "card {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}  card S - 1"
(is "?P S")
proof -

  define k where "k = card S"
  then show ?thesis
    using assms(6) 
  proof (induction k arbitrary: S rule: less_induct)
    case (less k)

    then have "finite S"
      by (metis fsm_states_finite rev_finite_subset)
    
    show ?case proof (cases k)
      case 0
      then have "S = {}"
        using less.prems finite S by auto
      then show ?thesis
        by fastforce     
    next
      case (Suc k')

      show ?thesis proof (cases "{w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S} = {}")
        case True
        then show ?thesis
          by (metis bot.extremum dual_order.eq_iff obtain_subset_with_card_n) 
      next
        case False
                                    
        define wk where wk: "wk = arg_max length (λwk . wk  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S})"

        obtain wk' where *:"wk'  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}"
          using False by blast
        have "finite {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}"
          by (metis (no_types) Collect_mem_eq List.finite_set finite_Collect_conjI)
        then have "wk  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}"
             and  " wk' . wk'  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}  length wk'  length wk"
          using False unfolding wk
          using arg_max_nat_lemma[of "(λwk . wk  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S})", OF *]
          by (meson finite_maxlen)+

        then have "wk  set (prefixes w)" and "wk  w" and "after M q1 wk  S" and "after M q2 wk  S"
          by blast+

        obtain wk_suffix where "w = wk@wk_suffix" and "wk_suffix  []"
          using wk  set (prefixes w)
          using prefixes_set_ob wk  w 
          by blast 

        have "distinguishes M (after M q1 []) (after M q2 []) w"
          using minimally_distinguishes M q1 q2 w
          by (metis after.simps(1) minimally_distinguishes_def)      

        have "minimally_distinguishes M (after M q1 wk) (after M q2 wk) wk_suffix"
          using minimally_distinguishes M q1 q2 w wk_suffix  []
          unfolding w = wk@wk_suffix
          using minimally_distinguishes_after_append[OF assms(1,2,3,4), of wk wk_suffix]
          by blast
        then have "distinguishes M (after M q1 wk) (after M q2 wk) wk_suffix"
          unfolding minimally_distinguishes_def 
          by auto
        then have "wk_suffix  LS M (after M q1 wk) = (wk_suffix  LS M (after M q2 wk))"
          unfolding distinguishes_def by blast


        define S1 where S1: "S1 = Set.filter (λq . wk_suffix  LS M q) S"
        define S2 where S2: "S2 = Set.filter (λq . wk_suffix  LS M q) S"

        
        have "S = S1  S2"
          unfolding S1 S2 by auto
        moreover have "S1  S2 = {}" 
          unfolding S1 S2 by auto
        ultimately have "card S = card S1 + card S2"
          using finite S card_Un_disjoint by blast

        have "S1  states M" and "S2  states M"
          using S = S1  S2 less.prems(2) by blast+

        have "S1  {}" and "S2  {}"
          using wk_suffix  LS M (after M q1 wk) = (wk_suffix  LS M (after M q2 wk)) after M q1 wk  S after M q2 wk  S
          unfolding S1 S2
          by (metis empty_iff member_filter)+
        then have "card S1 > 0" and "card S2 > 0"
          using S = S1  S2 finite S
          by (meson card_0_eq finite_Un neq0_conv)+
        then have "card S1 < k" and "card S2 < k"
          using card S = card S1 + card S2 unfolding less.prems
          by auto

        define W where W: "W = (λ S1 S2 . {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S1  after M q2 w'  S2})"
        then have " S' S'' . W S' S''  set (prefixes w)"
          by auto
        then have W_finite: " S' S'' . finite (W S' S'')"
          using List.finite_set[of "prefixes w"]
          by (meson finite_subset) 


        have " w' . w'  W S S  w'  wk  after M q1 w'  S1 = (after M q2 w'  S1)"
        proof -
          fix w' assume *:"w'  W S S" and "w'  wk"
          then have "w'  set (prefixes w)" and "w'  w" and "after M q1 w'  S" and "after M q2 w'  S"
            unfolding W
            by blast+ 

          then have "w'  LS M q1"
            by (metis IntE UnCI UnE append_self_conv assms(5) distinguishes_def language_prefix leD length_append length_greater_0_conv less_add_same_cancel1 minimally_distinguishes_def prefixes_set_ob) 
          have "w'  LS M q2"
            by (metis IntE UnCI w'  LS M q1 w'  set (prefixes w) w'  w append_Nil2 assms(5) distinguishes_def leD length_append length_greater_0_conv less_add_same_cancel1 minimally_distinguishes_def prefixes_set_ob) 

          have "length w' < length wk"
            using w'  wk *
                   wk' . wk'  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}  length wk'  length wk
            unfolding W
            by (metis (no_types, lifting) w = wk @ wk_suffix w'  set (prefixes w) append_eq_append_conv le_neq_implies_less prefixes_set_ob) 
            
            
          show "after M q1 w'  S1 = (after M q2 w'  S1)"
          proof (rule ccontr)
            assume "(after M q1 w'  S1)  (after M q2 w'  S1)"
            then have "(after M q1 w'  S1  (after M q2 w'  S2))  (after M q1 w'  S2  (after M q2 w'  S1))"
              using after M q1 w'  S after M q2 w'  S
              unfolding S = S1  S2
              by blast
            then have "wk_suffix  LS M (after M q1 w') = (wk_suffix  LS M (after M q2 w'))"
              unfolding S1 S2
              by (metis member_filter)
            then have "distinguishes M (after M q1 w') (after M q2 w') wk_suffix"
              unfolding distinguishes_def by blast
            then have "distinguishes M q1 q2 (w'@wk_suffix)"
              using distinguish_prepend[OF assms(1) _ q1  states M q2  states M w'  LS M q1 w'  LS M q2]
              by blast
            moreover have "length (w'@wk_suffix) < length (wk@wk_suffix)"
              using length w' < length wk
              by auto
            ultimately show False
              using minimally_distinguishes M q1 q2 w 
              unfolding w = wk@wk_suffix minimally_distinguishes_def 
              by auto
          qed
        qed



        have " x . x  W S1 S2  W S2 S1  x = wk"
        proof - 
          fix x assume "x  W S1 S2  W S2 S1"
          then have "x  W S S"
            unfolding W S = S1  S2 by blast
          show "x = wk"
            using x  W S1 S2  W S2 S1
            using  w' . w'  W S S  w'  wk  after M q1 w'  S1 = (after M q2 w'  S1)[OF x  W S S]
            unfolding W
            using S1  S2 = {}
            by blast 
        qed
        moreover have "wk  W S1 S2  W S2 S1"
          unfolding W 
          using wk  {w' . w'  set (prefixes w)  w'  w  after M q1 w'  S  after M q2 w'  S}
                wk_suffix  LS M (after M q1 wk) = (wk_suffix  LS M (after M q2 wk))
          by (metis (no_types, lifting) S1 Un_iff S = S1  S2 mem_Collect_eq member_filter)
        ultimately have "W S1 S2  W S2 S1 = {wk}"
          by blast


        have "W S S = (W S1 S1  W S2 S2  (W S1 S2  W S2 S1))"
          unfolding W S = S1  S2 by blast
        moreover have "W S1 S1  W S2 S2 = {}"
          using S1  S2 = {} unfolding W
          by blast
        moreover have "W S1 S1  (W S1 S2  W S2 S1) = {}"
          unfolding W
          using S1  S2 = {}
          by blast
        moreover have "W S2 S2  (W S1 S2  W S2 S1) = {}"
          unfolding W
          using S1  S2 = {}
          by blast
        moreover have "finite (W S1 S1)" and "finite (W S2 S2)" and "finite {wk}"
          using W_finite by auto
        ultimately have "card (W S S) = card (W S1 S1) + card (W S2 S2) + 1"
          unfolding W S1 S2  W S2 S1 = {wk}
          by (metis card_Un_disjoint finite_UnI inf_sup_distrib2 is_singletonI is_singleton_altdef sup_idem)
        moreover have "card (W S1 S1)  card S1 - 1"
          using less.IH[OF card S1 < k _ S1  states M]
          unfolding W by blast
        moreover have "card (W S2 S2)  card S2 - 1"
          using less.IH[OF card S2 < k _ S2  states M]
          unfolding W by blast
        ultimately have "card (W S S)  card S - 1"
          using card S = card S1 + card S2
          using card S1 < k card S2 < k less.prems(1) by linarith
        then show ?thesis
          unfolding W .
      qed
    qed
  qed
qed

lemma minimally_distinguishes_proper_prefix_in_language :
  assumes "minimally_distinguishes M q1 q2 io"
  and     "io'  set (prefixes io)"
  and     "io'  io"
shows "io'  LS M q1  LS M q2"
proof -
  have "io  LS M q1  io  LS M q2"
    using assms(1) unfolding minimally_distinguishes_def distinguishes_def by blast
  then have "io'  LS M q1  io'  LS M q2"
    by (metis assms(2) prefixes_set_ob language_prefix) 

  have "length io' < length io"
    using assms(2,3) unfolding prefixes_set by auto
  then have "io'  LS M q1  io'  LS M q2"
    using assms(1) unfolding minimally_distinguishes_def distinguishes_def
    by (metis Int_iff Un_Int_eq(1) Un_Int_eq(2) leD)
  then show ?thesis
    using io'  LS M q1  io'  LS M q2
    by blast
qed

lemma distinguishes_not_Nil:
  assumes "distinguishes M q1 q2 io"
  and     "q1  states M"
  and     "q2  states M"
shows "io  []"
  using assms unfolding distinguishes_def by auto

fun does_distinguish :: "('a,'b,'c) fsm  'a  'a  ('b × 'c) list  bool" where
  "does_distinguish M q1 q2 io = (is_in_language M q1 io  is_in_language M q2 io)"

lemma does_distinguish_correctness :
  assumes "observable M"
  and     "q1  states M"
  and     "q2  states M"
shows "does_distinguish M q1 q2 io = distinguishes M q1 q2 io"
  unfolding does_distinguish.simps
            is_in_language_iff[OF assms(1,2)] 
            is_in_language_iff[OF assms(1,3)]
            distinguishes_def
  by blast

lemma h_obs_distinguishes :
  assumes "observable M"
  and     "h_obs M q1 x y = Some q1'"
  and     "h_obs M q2 x y = None"
shows "distinguishes M q1 q2 [(x,y)]"
  using assms(2,3) LS_single_transition[of x y M] unfolding distinguishes_def h_obs_Some[OF assms(1)] h_obs_None[OF assms(1)]
  by (metis Int_iff UnI1 y x q. (h_obs M q x y = None) = (q'. (q, x, y, q')  FSM.transitions M) assms(1) assms(2) fst_conv h_obs_language_iff option.distinct(1) snd_conv) 

lemma distinguishes_sym :
  assumes "distinguishes M q1 q2 io" 
  shows "distinguishes M q2 q1 io"
  using assms unfolding distinguishes_def by blast

lemma distinguishes_after_prepend :
  assumes "observable M"
  and     "h_obs M q1 x y  None"
  and     "h_obs M q2 x y  None"
  and     "distinguishes M (FSM.after M q1 [(x,y)]) (FSM.after M q2 [(x,y)]) γ"
shows "distinguishes M q1 q2 ((x,y)#γ)"
proof -
  have "[(x,y)]  LS M q1"
    using assms(2) h_obs_language_single_transition_iff[OF assms(1)] by auto

  have "[(x,y)]  LS M q2"
    using assms(3) h_obs_language_single_transition_iff[OF assms(1)] by auto  
  
  show ?thesis
    using after_language_iff[OF assms(1) [(x,y)]  LS M q1, of γ] 
    using after_language_iff[OF assms(1) [(x,y)]  LS M q2, of γ] 
    using assms(4)
    unfolding distinguishes_def
    by simp
qed

lemma distinguishes_after_initial_prepend :
  assumes "observable M"
  and     "io1  L M"
  and     "io2  L M"
  and     "h_obs M (after_initial M io1) x y  None"
  and     "h_obs M (after_initial M io2) x y  None"
  and     "distinguishes M (after_initial M (io1@[(x,y)])) (after_initial M (io2@[(x,y)])) γ"
shows "distinguishes M (after_initial M io1) (after_initial M io2) ((x,y)#γ)"
  by (metis after_split assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) distinguishes_after_prepend h_obs_language_append)


subsection ‹Extending FSMs by single elements›

lemma fsm_from_list_simps[simp] :
  "initial (fsm_from_list q ts) = (case ts of []  q | (t#ts)  t_source t)"
  "states (fsm_from_list q ts) = (case ts of []  {q} | (t#ts')  ((image t_source (set ts))  (image t_target (set ts))))"
  "inputs (fsm_from_list q ts) = image t_input (set ts)"
  "outputs (fsm_from_list q ts) = image t_output (set ts)"
  "transitions (fsm_from_list q ts) = set ts"
  by (cases ts; transfer; simp)+

lift_definition add_transition :: "('a,'b,'c) fsm  ('a,'b,'c) transition  ('a,'b,'c) fsm" is FSM_Impl.add_transition
  by simp 

lemma add_transition_simps[simp]:
  assumes "t_source t  states M" and "t_input t  inputs M" and "t_output t  outputs M" and "t_target t  states M"
  shows
  "initial (add_transition M t) = initial M"  
  "inputs (add_transition M t) = inputs M"
  "outputs (add_transition M t) = outputs M"
  "transitions (add_transition M t) = insert t (transitions M)"
  "states (add_transition M t) = states M" using assms by (transfer; simp)+


lift_definition add_state :: "('a,'b,'c) fsm  'a  ('a,'b,'c) fsm" is FSM_Impl.add_state
  by simp

lemma add_state_simps[simp]:
  "initial (add_state M q) = initial M"  
  "inputs (add_state M q) = inputs M"
  "outputs (add_state M q) = outputs M"
  "transitions (add_state M q) = transitions M"
  "states (add_state M q) = insert q (states M)" by (transfer; simp)+

lift_definition add_input :: "('a,'b,'c) fsm  'b  ('a,'b,'c) fsm" is FSM_Impl.add_input
  by simp

lemma add_input_simps[simp]:
  "initial (add_input M x) = initial M"  
  "inputs (add_input M x) = insert x (inputs M)"
  "outputs (add_input M x) = outputs M"
  "transitions (add_input M x) = transitions M"
  "states (add_input M x) = states M" by (transfer; simp)+

lift_definition add_output :: "('a,'b,'c) fsm  'c  ('a,'b,'c) fsm" is FSM_Impl.add_output
  by simp

lemma add_output_simps[simp]:
  "initial (add_output M y) = initial M"  
  "inputs (add_output M y) = inputs M"
  "outputs (add_output M y) = insert y (outputs M)"
  "transitions (add_output M y) = transitions M"
  "states (add_output M y) = states M" by (transfer; simp)+

lift_definition add_transition_with_components :: "('a,'b,'c) fsm  ('a,'b,'c) transition  ('a,'b,'c) fsm" is FSM_Impl.add_transition_with_components
  by simp 

lemma add_transition_with_components_simps[simp]:
  "initial (add_transition_with_components M t) = initial M"  
  "inputs (add_transition_with_components M t) = insert (t_input t) (inputs M)"
  "outputs (add_transition_with_components M t) = insert (t_output t) (outputs M)"
  "transitions (add_transition_with_components M t) = insert t (transitions M)"
  "states (add_transition_with_components M t) = insert (t_target t) (insert (t_source t) (states M))"
  by (transfer; simp)+

subsection ‹Renaming Elements›

lift_definition rename_states :: "('a,'b,'c) fsm  ('a  'd)  ('d,'b,'c) fsm" is FSM_Impl.rename_states
  by simp 

lemma rename_states_simps[simp]:
  "initial (rename_states M f) = f (initial M)"  
  "states (rename_states M f) = f ` (states M)"  
  "inputs (rename_states M f) = inputs M"
  "outputs (rename_states M f) = outputs M"
  "transitions (rename_states M f) = (λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions M"
  by (transfer; simp)+


lemma rename_states_isomorphism_language_state :
  assumes "bij_betw f (states M) (f ` states M)" 
  and     "q  states M"
shows "LS (rename_states M f) (f q) = LS M q"
proof -

  have *: "bij_betw f (FSM.states M) (FSM.states (FSM.rename_states M f))"
    using assms rename_states_simps by auto

  have **: "f (initial M) = initial (rename_states M f)"
    using rename_states_simps by auto

  have ***: "(q x y q'.
    q  states M 
    q'  states M  ((q, x, y, q')  transitions M) = ((f q, x, y, f q')  transitions (rename_states M f)))"
  proof 
    fix q x y q' assume "q  states M" and "q'  states M"

    show "(q, x, y, q')  transitions M  (f q, x, y, f q')  transitions (rename_states M f)"
      unfolding assms rename_states_simps by force

    show "(f q, x, y, f q')  transitions (rename_states M f)  (q, x, y, q')  transitions M"
    proof -
      assume "(f q, x, y, f q')  transitions (rename_states M f)"
      then obtain t where "(f q, x, y, f q') = (f (t_source t), t_input t, t_output t, f (t_target t))"
                      and "t  transitions M"
        unfolding assms rename_states_simps 
        by blast
      then have "t_source t  states M" and "t_target t  states M" and "f (t_source t) = f q" and "f (t_target t) = f q'" and "t_input t = x" and "t_output t = y"
        by auto

      have "f q  states (rename_states M f)" and "f q'  states (rename_states M f)"
        using (f q, x, y, f q')  transitions (rename_states M f)
        by auto

      have "t_source t = q"
        using f (t_source t) = f q q  states M t_source t  states M 
        using assms unfolding bij_betw_def inj_on_def 
        by blast
      moreover have "t_target t = q'"
        using f (t_target t) = f q' q'  states M t_target t  states M 
        using assms unfolding bij_betw_def inj_on_def 
        by blast
      ultimately show "(q, x, y, q')  transitions M"
        using t_input t = x t_output t = y t  transitions M
        by auto
    qed
  qed

  show ?thesis
    using language_equivalence_from_isomorphism[OF * ** *** assms(2)]
    by blast
qed


lemma rename_states_isomorphism_language :
  assumes "bij_betw f (states M) (f ` states M)" 
  shows "L (rename_states M f) = L M"
  using rename_states_isomorphism_language_state[OF assms fsm_initial]
  unfolding rename_states_simps .

lemma rename_states_observable :
  assumes "bij_betw f (states M) (f ` states M)"
  and     "observable M"
shows "observable (rename_states M f)"  
proof -
  have " q1 x y q1' q1'' . (q1,x,y,q1')  transitions (rename_states M f)  (q1,x,y,q1'')  transitions (rename_states M f)  q1' = q1''"
  proof -
    fix q1 x y q1' q1'' 
    assume "(q1,x,y,q1')  transitions (rename_states M f)" and "(q1,x,y,q1'')  transitions (rename_states M f)"
    then obtain t' t'' where "t'  transitions M"
                         and "t''  transitions M"
                         and "(f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1,x,y,q1')"
                         and "(f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1,x,y,q1'')"
      unfolding rename_states_simps
      by force

    then have "f (t_source t') = f (t_source t'')"
      by auto
    moreover have "t_source t'  states M" and "t_source t''  states M"
      using t'  transitions M t''  transitions M
      by auto
    ultimately have "t_source t' = t_source t''"
      using assms(1)
      unfolding bij_betw_def inj_on_def by blast
    then have "t_target t' = t_target t''"
      using assms(2) unfolding observable.simps
      by (metis Pair_inject (f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1, x, y, q1'') (f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1, x, y, q1') t'  FSM.transitions M t''  FSM.transitions M) 
    then show "q1' = q1''"
      using (f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1, x, y, q1'') (f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1, x, y, q1') by auto
  qed
  then show ?thesis
    unfolding observable_alt_def by blast
qed


lemma rename_states_minimal :
  assumes "bij_betw f (states M) (f ` states M)"
  and     "minimal M"
shows "minimal (rename_states M f)"
proof -
  have " q q' . q  f ` FSM.states M  q'  f ` FSM.states M  q  q'  LS (rename_states M f) q  LS (rename_states M f) q'"
  proof -
    fix q q' assume "q  f ` FSM.states M" and "q'  f ` FSM.states M" and "q  q'"

    then obtain fq fq' where "fq  states M" and "fq'  states M" and "q = f fq" and "q' = f fq'"
      by auto
    then have "fq  fq'" 
      using q  q' by auto 
    then have "LS M fq  LS M fq'"
      by (meson fq  FSM.states M fq'  FSM.states M assms(2) minimal.elims(2))
    then show "LS (rename_states M f) q  LS (rename_states M f) q'"
      using rename_states_isomorphism_language_state[OF assms(1)]
      by (simp add: fq  FSM.states M fq'  FSM.states M q = f fq q' = f fq')
  qed
  then show ?thesis 
    by auto
qed


fun index_states :: "('a::linorder,'b,'c) fsm  (nat,'b,'c) fsm" where
  "index_states M = rename_states M (assign_indices (states M))"

lemma assign_indices_bij_betw: "bij_betw (assign_indices (FSM.states M)) (FSM.states M) (assign_indices (FSM.states M) ` FSM.states M)"
  using assign_indices_bij[OF fsm_states_finite[of M]]
  by (simp add: bij_betw_def) 


lemma index_states_language :
  "L (index_states M) = L M"
  using rename_states_isomorphism_language[of "assign_indices (states M)" M, OF assign_indices_bij_betw]
  by auto

lemma index_states_observable :
  assumes "observable M"
  shows "observable (index_states M)"
  using rename_states_observable[of "assign_indices (states M)", OF assign_indices_bij_betw assms]
  unfolding index_states.simps .

lemma index_states_minimal :
  assumes "minimal M"
  shows "minimal (index_states M)" 
  using rename_states_minimal[of "assign_indices (states M)", OF assign_indices_bij_betw assms]
  unfolding index_states.simps .



fun index_states_integer :: "('a::linorder,'b,'c) fsm  (integer,'b,'c) fsm" where
  "index_states_integer M = rename_states M (integer_of_nat  assign_indices (states M))"

lemma assign_indices_integer_bij_betw: "bij_betw (integer_of_nat  assign_indices (states M)) (FSM.states M) ((integer_of_nat  assign_indices (states M)) ` FSM.states M)"
proof -
  have *: "inj_on (assign_indices (FSM.states M)) (FSM.states M)" 
    using assign_indices_bij[OF fsm_states_finite[of M]]
    unfolding bij_betw_def
    by auto
  then have "inj_on (integer_of_nat  assign_indices (states M)) (FSM.states M)"
    unfolding inj_on_def
    by (metis comp_apply nat_of_integer_integer_of_nat)
  then show ?thesis
    unfolding bij_betw_def
    by auto
qed


lemma index_states_integer_language :
  "L (index_states_integer M) = L M"
  using rename_states_isomorphism_language[of "integer_of_nat  assign_indices (states M)" M, OF assign_indices_integer_bij_betw]
  by auto

lemma index_states_integer_observable :
  assumes "observable M"
  shows "observable (index_states_integer M)"
  using rename_states_observable[of "integer_of_nat  assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms]
  unfolding index_states_integer.simps .

lemma index_states_integer_minimal :
  assumes "minimal M"
  shows "minimal (index_states_integer M)" 
  using rename_states_minimal[of "integer_of_nat  assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms]
  unfolding index_states_integer.simps .

subsection ‹Canonical Separators›

lift_definition canonical_separator' :: "('a,'b,'c) fsm  (('a × 'a),'b,'c) fsm  'a  'a  (('a × 'a) + 'a,'b,'c) fsm" is FSM_Impl.canonical_separator'
proof -
  fix A :: "('a,'b,'c) fsm_impl"
  fix B :: "('a × 'a,'b,'c) fsm_impl"
  fix q1 :: 'a
  fix q2 :: 'a
  assume "well_formed_fsm A" and "well_formed_fsm B"

  then have p1a: "fsm_impl.initial A  fsm_impl.states A"
        and p2a: "finite (fsm_impl.states A)"
        and p3a: "finite (fsm_impl.inputs A)"
        and p4a: "finite (fsm_impl.outputs A)"
        and p5a: "finite (fsm_impl.transitions A)"
        and p6a: "(tfsm_impl.transitions A.
            t_source t  fsm_impl.states A 
            t_input t  fsm_impl.inputs A  t_target t  fsm_impl.states A 
                                             t_output t  fsm_impl.outputs A)"
        and p1b: "fsm_impl.initial B  fsm_impl.states B"
        and p2b: "finite (fsm_impl.states B)"
        and p3b: "finite (fsm_impl.inputs B)"
        and p4b: "finite (fsm_impl.outputs B)"
        and p5b: "finite (fsm_impl.transitions B)"
        and p6b: "(tfsm_impl.transitions B.
            t_source t  fsm_impl.states B 
            t_input t  fsm_impl.inputs B  t_target t  fsm_impl.states B 
                                             t_output t  fsm_impl.outputs B)"
    by simp+

  let ?P = "FSM_Impl.canonical_separator' A B q1 q2"

  show "well_formed_fsm ?P" proof (cases "fsm_impl.initial B = (q1,q2)")
    case False
    then show ?thesis by auto
  next
    case True

    let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs  yqs | None  {}))"
  
    have " qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs  yqs | None  {})) qx = (λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx"
    proof -
      fix qx
      show " qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs  yqs | None  {})) qx = (λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx"
        unfolding set_as_map_def by (cases "z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A"; auto)
    qed
    moreover have " qx . (λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx = (λ qx . {y | y .  q' . (fst qx, snd qx, y, q')  fsm_impl.transitions A}) qx"
    proof -
      fix qx 
      show "(λ qx . {z. (qx, z)  (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx = (λ qx . {y | y .  q' . (fst qx, snd qx, y, q')  fsm_impl.transitions A}) qx"
        by force
    qed
    ultimately have *:" ?f = (λ qx . {y | y .  q' . (fst qx, snd qx, y, q')  fsm_impl.transitions A})" 
      by blast
      
    let ?shifted_transitions' = "shifted_transitions (fsm_impl.transitions B)"
    let ?distinguishing_transitions_lr = "distinguishing_transitions ?f q1 q2 (fsm_impl.states B) (fsm_impl.inputs B)"
    let ?ts = "?shifted_transitions'  ?distinguishing_transitions_lr"
  
    have "FSM_Impl.states ?P = (image Inl (FSM_Impl.states B))  {Inr q1, Inr q2}"
    and  "FSM_Impl.transitions ?P = ?ts"
      unfolding FSM_Impl.canonical_separator'.simps Let_def True by simp+

    have p2: "finite (fsm_impl.states ?P)"
      unfolding FSM_Impl.states ?P = (image Inl (FSM_Impl.states B))  {Inr q1, Inr q2} using p2b by blast
  
    have "fsm_impl.initial ?P = Inl (q1,q2)" by auto
    then have p1: "fsm_impl.initial ?P  fsm_impl.states ?P" 
      using p1a p1b unfolding canonical_separator'.simps True by auto
    have p3: "finite (fsm_impl.inputs ?P)"
      using p3a p3b by auto
    have p4: "finite (fsm_impl.outputs ?P)"
      using p4a p4b by auto

    have "finite (fsm_impl.states B × fsm_impl.inputs B)"
      using p2b p3b by blast
    moreover have **: " x q1 . finite ({y |y. q'. (fst (q1, x), snd (q1, x), y, q')  fsm_impl.transitions A})"
    proof - 
      fix x q1
      have "{y |y. q'. (fst (q1, x), snd (q1, x), y, q')  fsm_impl.transitions A} = {t_output t | t . t  fsm_impl.transitions A  t_source t = q1  t_input t = x}"
        by auto
      then have "{y |y. q'. (fst (q1, x), snd (q1, x), y, q')  fsm_impl.transitions A}  image t_output (fsm_impl.transitions A)"
        unfolding fst_conv snd_conv by blast
      moreover have "finite (image t_output (fsm_impl.transitions A))"
        using p5a by auto
      ultimately show "finite ({y |y. q'. (fst (q1, x), snd (q1, x), y, q')  fsm_impl.transitions A})"
        by (simp add: finite_subset)
    qed
    ultimately have "finite ?distinguishing_transitions_lr"
      unfolding * distinguishing_transitions_def by force
    moreover have "finite ?shifted_transitions'"
      unfolding shifted_transitions_def using p5b by auto
    ultimately have "finite ?ts" by blast
    then have p5: "finite (fsm_impl.transitions ?P)"
      by simp
     
    have "fsm_impl.inputs ?P = fsm_impl.inputs A  fsm_impl.inputs B"
      using True by auto
    have "fsm_impl.outputs ?P = fsm_impl.outputs A  fsm_impl.outputs B"
      using True by auto
  
    have " t . t  ?shifted_transitions'  t_source t  fsm_impl.states ?P  t_target t  fsm_impl.states ?P"
      unfolding FSM_Impl.states ?P = (image Inl (FSM_Impl.states B))  {Inr q1, Inr q2} shifted_transitions_def 
      using p6b by force
    moreover have " t . t  ?distinguishing_transitions_lr  t_source t  fsm_impl.states ?P  t_target t  fsm_impl.states ?P"
      unfolding FSM_Impl.states ?P = (image Inl (FSM_Impl.states B))  {Inr q1, Inr q2} distinguishing_transitions_def * by force
    ultimately have " t . t  ?ts  t_source t  fsm_impl.states ?P  t_target t  fsm_impl.states ?P"
      by blast
    moreover have " t . t  ?shifted_transitions'  t_input t  fsm_impl.inputs ?P  t_output t  fsm_impl.outputs ?P"
    proof -
      have " t . t  ?shifted_transitions'  t_input t  fsm_impl.inputs B  t_output t  fsm_impl.outputs B"
        unfolding shifted_transitions_def using p6b by auto
      then show " t . t  ?shifted_transitions'  t_input t  fsm_impl.inputs ?P  t_output t  fsm_impl.outputs ?P"
        unfolding fsm_impl.inputs ?P = fsm_impl.inputs A  fsm_impl.inputs B
                  fsm_impl.outputs ?P = fsm_impl.outputs A  fsm_impl.outputs B by blast
    qed
    moreover have " t . t  ?distinguishing_transitions_lr  t_input t  fsm_impl.inputs ?P  t_output t  fsm_impl.outputs ?P"
      unfolding * distinguishing_transitions_def using p6a p6b True by auto
    ultimately have p6: "(tfsm_impl.transitions ?P.
              t_source t  fsm_impl.states ?P 
              t_input t  fsm_impl.inputs ?P  t_target t  fsm_impl.states ?P 
                                               t_output t  fsm_impl.outputs ?P)"
      unfolding FSM_Impl.transitions ?P = ?ts by blast
  
    show "well_formed_fsm ?P"
      using p1 p2 p3 p4 p5 p6 by linarith
  qed
qed 


lemma canonical_separator'_simps :
  assumes "initial P = (q1,q2)"
  shows "initial (canonical_separator' M P q1 q2) = Inl (q1,q2)"
        "states (canonical_separator' M P q1 q2) = (image Inl (states P))  {Inr q1, Inr q2}"
        "inputs (canonical_separator' M P q1 q2) = inputs M  inputs P"
        "outputs (canonical_separator' M P q1 q2) = outputs M  outputs P"
        "transitions (canonical_separator' M P q1 q2) 
          = shifted_transitions (transitions P) 
               distinguishing_transitions (h_out M) q1 q2 (states P) (inputs P)"
  using assms unfolding h_out_code by (transfer; auto)+

lemma canonical_separator'_simps_without_assm :
        "initial (canonical_separator' M P q1 q2) = Inl (q1,q2)"
        "states (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then (image Inl (states P))  {Inr q1, Inr q2} else {Inl (q1,q2)})"
        "inputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then inputs M  inputs P else {})"
        "outputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then outputs M  outputs P else {})"
        "transitions (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then shifted_transitions (transitions P)  distinguishing_transitions (h_out M) q1 q2 (states P) (inputs P) else {})"
  unfolding h_out_code by (transfer; simp add: Let_def)+

end