Übersicht der Quellen

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

Benutzer

Quellcode-Bibliothek FSM.thy   Sprache: unbekannt

 
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.initiadone
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(1by 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(2proof (induction p rule: rev_induct)
  case Nil
  show ?case using assms(3by 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(2proof (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(1using 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(1using 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,3by 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(4by auto
      then have p2: "distinct (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))"
        using Suc.prems(3by auto

      have p3: "(insert q' visitedStates)
                  = set (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))"
        using Suc.prems(4by 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(4by auto

      let ?vN = "insert (t_target t) visitedStates"
      have "?vN = set (visited_states (p_source q (prev @ [t])) (prev @ [t]))"
        using Suc.prems(4by 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(2unfolding * 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(1by 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(1by 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(2by 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,2by 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(2by auto
  then have "path M (t_source t) (t#p)" and "p_io (t#p) = (t_input t, t_output t) # io"
    using assms(1by 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(1by blast
      have "inv_into (states M1) f q' states M1"
        using f2 q' states M2 calculation(1by blast
      then show ?thesis
        using f3 a1 q states M2 q' states M2 assms(1) assms(3) bij_betw_inv_into_righby 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(1by blast
      have "inv_into (states M1) f q states M1"
        using f2 q states M2 calculation(1by blast
      then show ?thesis
        using f3 a1 q states M2 q' states M2 assms(1) assms(3) bij_betw_inv_into_righby 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(1by blast
      have "inv_into (FSM.reachable_states M1) f q' FSM.reachable_states M1"
        using f2 q' FSM.reachable_states M2 calculation(1by 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(1by blast
      have "inv_into (FSM.reachable_states M1) f q FSM.reachable_states M1"
        using f2 q FSM.reachable_states M2 calculation(1by 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,2path 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(2proof (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) ptarget (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(1unfolding 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(2by 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(1by 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(2by 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(2by 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(4by (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(1by 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(2unfolding 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(1unfolding 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(2by (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 Mby 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(2by 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(2by 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(1path 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(2by 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(3by 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(1path M q p'' path M q pby 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(1unfolding 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(3by 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(2io1 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(1by auto
  moreover obtain p2 where "path M q1 p2" and "p_io p2 = io2" 
    using assms(2by 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(4by 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(3path M q p' path M q p p_io p' = p_io pby 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(2by auto

  moreover obtain p1 where "q' = target q p1" and "path M q p1" and "p_io p1 = io1"
    using assms(1by 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,2path 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))", symmetricby 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 add: card_eq_0_iff)
    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 (auto simp add: card_1_singleton_iff split: if_splits)
    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 \<equiv> 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(2proof (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(1t transitions Mt transitions M
    using t_source t = q assms(1by 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(2by 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(2unfolding 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(3by 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,2proof (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(2by 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(2by 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(3unfolding 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(1by 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(2proof (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(2by 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(1path M q pp_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(5card (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(4io1 L M2]
          observable_after_language_append[OF assms(4io2 L M2]
          observable_after_language_none[OF assms(4io1 L M2]
          observable_after_language_none[OF assms(4io2 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(5proof (induction p rule: rev_induct)
case Nil
  then show ?case using assms(2by 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(1t 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,4by 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 Mby blast
  then have "path M (initial M) (p@p')" and "target (initial M) (p@p') = q'"
    using from_FSM_path[OF q states Mpath 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(2by blast
  then have "path M q []"
    by (meson assms(1) submachine_path)
  then show ?thesis
    using assms(1) assms(2by 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(2unfolding 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(1by 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,5unfolding 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(2by blast
  then have *: "(t_input t1, t_output t1)#ioF LS M (t_source t2)"
    using assms(1by blast
  
  have "ioF LS M (t_target t2)"
    using observable_language_next[OF * observable M t2 transitions Munfolding 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(1unfolding 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(2by 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,5proof (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(2by auto
  then have "path M1 q1 (p1@p2)" 
    using assms(1by 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(2proof (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 Munfolding 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(2t 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(1obtain 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(2by 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(3by 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 Mby 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(2unfolding 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(2by (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(2by 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 Mby 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(2proof (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 qby 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(2by 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(2unfolding 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(5by auto
  ultimately show False
    using assms(4unfolding 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(5unfolding 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(5unfolding 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(5unfolding 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(5unfolding 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(5unfolding 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(5unfolding 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(2by 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 auto
        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'))"
              using S1 S2 by auto
            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))
          using S1 by clarsimp (auto simp add: S = S1 S2)
        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 < kS1 states M]
          unfolding W by blast
        moreover have "card (W S2 S2) card S2 - 1"
          using less.IH[OF card S2 < kS2 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(1by 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(1unfolding 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,3unfolding prefixes_set by auto
  then have "io' LS M q1 io' LS M q2"
    using assms(1unfolding 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(2unfolding 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

Messung V0.5 in Prozent
C=90 H=99 G=94

[Seitenstruktur0.726Druckenetwas mehr zur Ethik2026-09-06]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Open Source Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Statistik
#Sources=1019547
#Domains=890699