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

Benutzer

Impressum FSM.thy

  Interaktion und
PortierbarkeitIsabelle
 

section Finite State Machines

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


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


subsection Well-formed Finite State Machines

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


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

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


setup_lifting type_definition_fsm

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

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



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


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

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



subsubsection Example FSMs


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


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

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


subsection Transition Function h and related functions

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

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

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

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

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

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

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

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

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


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

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


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


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


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

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

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

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


subsection Size

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

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

instance ..
end

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


subsection Paths

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma path_source_target_index :
  assumes "Suc i < length p"
  and     "path M q p"
shows "t_target (p ! i) = t_source (p ! (Suc i))"
  using assms proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc t ps)
  then have "path M q ps" and "t_source t = target q ps" and "t transitions M" by auto
  
  show ?case proof (cases "Suc i < length ps")
    case True
    then have "t_target (ps ! i) = t_source (ps ! Suc i)" 
      using snoc.IH path M q ps by auto
    then show ?thesis
      by (simp add: Suc_lessD True nth_append) 
  next
    case False
    then have "Suc i = length ps"
      using snoc.prems(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=87 H=98 G=92

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.511Bemerkung:  (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-06-10) ¤

*Eine klare Vorstellung vom Zielzustand






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge