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

Benutzer

SSL 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 " 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 " []"
  and "target q p = q"
shows "¬ acyclic M"
  using assms unfolding acyclic.simps target.simps visited_states.simps
  using distinct.simps(2) by fastforce

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

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


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

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


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

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

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

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


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


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


subsubsection Deadlock States

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

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

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


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

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

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

  then obtain t where " 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 " 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 " set (butlast p')")
    case True
    show ?thesis
      using snoc.IH[OF _ True] snoc.prems(1)
      by blast
  next
    case False
    then have "p' = (butlast p')@[t]"
      using snoc.prems(2) by (metis append_butlast_last_id append_self_conv2 butlast_snoc
                                in_set_butlast_appendI list_prefix_elem set_ConsD)
    then have "path M q ((butlast p'@[t])@[t'])"
      using snoc.prems(1)
      by auto
    
    have "t'  transitions M" and "t_source t' = target q (butlast p'@[t])"
      using path_suffix[OF path M q ((butlast p'@[t])@[t'])]
      by auto
    then have "t'  transitions M  t_source t' = t_target t"
      unfolding target.simps visited_states.simps by auto
    then show ?thesis
      unfolding deadlock_state.simps using t' transitions M by blast
  qed
qed


lemma states_initial_deadlock :
  assumes "deadlock_state M (initial M)"
  shows "reachable_states M = {initial M}"
  
proof -
  have " q . q  reachable_states M ==> q = initial M"
  proof -
    fix q assume " 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 " 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 " ?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 MGrover's algorithm
      moreover have "{(prev @ grover_state
                       p_io p = (x,y)#io}"
         open>(,x,y,q') transitions M
        using cons by force
      timatelymaty shw "\in {prev@p | p . path M q p "
        by blast
    qed
    then
       al_:

    have " {prev@p | p . path M q p p
    proof -
      fix pp assume "pp \<byimp_fna_e o_elpor we_e_sureea_qpo2
      then taip here"p= r@pad"pth q" ad"p_op =(xy)#io
        stforce
      then tth
                         and "p_io p' = io"
        by (metis (no_types, lifting) map_eq_Cons_D)
      then have "path M (t_target t) p'" and "t_soure q"and _inut =x
                                         =nd t_arget < states M"
                                         and "t _osmt_ght[f _
        by auto

      have "(y,t_target t)
        using t_output t = yt_input t = xt_source t = q
     ings
      
      moreover have
    H\>in states M
        using \openp = t # p' t_input t = x
              opent_output t = y
        by auto

      ultimately show "pp pp = prev@p
        by blast
    qed
  then ho "{rv@| . pth p<>p_ (,yio <s> ?UN"
java.lang.StringIndexOutOfBoundsException: Index 35 out of bounds for length 25
java.lang.StringIndexOutOfBoundsException: Index 84 out of bounds for length 5

  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 -
  ve {]@ |ps. atM s\and 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
havea_l*<> / 2b_ ) *cs (<> 2) cs(<> / 2
    { assume "{[] @ ps |ps. path M q ps / 2) - (beta_l l) * csin (\<theta/ 2)
     nae" notin FSM..states M"
      <>q \<nSMfor_o ( M)io q [] = {[] @ p |p. path M q p by force
      then= (alphal) (2s \theta> / 2* cc \theta> 2) - bt_l (2 cin (\<heta  = (alpha_l l) * (csin θo θ
      using path_begin_state by force }
  ultimately show "{ps. path M q ps FSM.states M then paths_for_io' (h M) io q [] else {})"
    by linarith
 


fun_t: "''b'cfm \ightarrow ('b × 'c) list ==> 'a ==>' et" wher
  "io_targets M io q = {target q p | p . path M q p \<and 

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_otpt "
  by (metis assms observable.elims(2) prod.expand)

lemma obeaet_nqe:
  ssumes"obsvale M"

  and "aO*a_ \^m N"
  and "p_io p = p_io p'"
shows "p = p'"
proof -
  
    using assms(4) map_eq_ "uni mt_P
  then show ?thesis
    using\open p = p_io p'
  proof (induction p p' arbitrary: q rule: list_induct2)
    case Nil
    heno ?caseby uto
  next
    case (Cons x xs y ys)
    then have *: "x va1 { .<
                                    \vars2
      by auto
    enattgt =tr
assmsbservable(t
    then have "x = y"
      p rd.epad
      

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

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

    nd
   <x = y by simp
   apply (subst nths_ped)
ed


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

  obtain p wheunfoldipsPd_e _Pds_def P.nsvar'usng psP_ oinp_P1ya
    using assms(2) ssume m1 \in carrier_mat (2^n) (2^n)"
  hen a "trgt p <_agetsMio "
    by auto

  have "
java.lang.StringIndexOutOfBoundsException: Index 21 out of bounds for length 21
ume"¬
  exists> q' . q' io_targets M io q"
    proof<>oyo he o\>
      have "¬ {target q p}"
        using q'. io_targets M io q {q'}})\close> \open>arget q p io_targets M io qblst
      then show ?thesis
        by blast
    qed
    enbanq'werq <> agt n <i i_tresMo q"
      tensor_mat_carrierf\^m st2.d2"]
    then obtsubgo nfldinprilsate.d2_ aialsatedms2efs2Pnthvrs'ps_Pdim2efdims_as ato

java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
      using ary_ex_mat_O
java.lang.StringIndexOutOfBoundsException: Index 29 out of bounds for length 22
      using observable_path_unique[OF assms(1 \open at while loop
hen ow"Fle"
      using
  qed

  then show ?thesis using that by blast
qed


lemma osevalepat_io_targe
  assumes "observabl M"
  and "path M q p"
shows "io_tarsthen shw casapysmapl ruleqmtI) auto
usingervable_io_targetsFasm()lnugttimn[Fasm(2 f "_i "]
        singletonD[of "target q p"]
  unfolding io_targets.simps
proof -
  assume ashow ?ce apl sip)unfldgs2por_a_ef
  assume "q'. {target q pa |pa. path M q pa p}= q}\Longrightarrow thesis] thesis"
  then obtain aa :: 'a w apply (sbstn)
    by meson
  then show "{target q ps |ps. path M q ps lloi:
    using a1 assms(2) by blast
qed


lemma completely_specified_io_targets :
  assumes "completely_specified M"
  shows "
java.lang.NullPointerException
  


e_path_language_step
  assumes "observable M"
      athMqp
      and "¬transitions M.
               t_source t = target q p
               t_input t = x t_output t = y)"
    shows "(p_io p)@[(x,y)]
using assms proof (induction p rule:
  case Nil
  show caseo
    assume "p_io [] @ [(x, y)]
 inw pt Mqp npo '=[xy)"ufligL.sps
      by force
    then obtain t where "p' = [t]" by blasthave1:"td "
    
    have "ttransitions M" and "t_source t = target q[]
      using p' = [t] by auto
    moreover nt\Rightarrow olmtwhr
      ing<>p '=[(,y\close b at
    ultimately show "False"
      using Nil.prems(3) by blast
  qed
next
  case hv"0< k} {Suc k} = {0..<(Suc (Suc k))}" by auto
  
  from ==> exH_kk=pa_xenids 0<uk (u ).n} (H_k k)"
                                              and "t antins"
    by ints1tasaedms{c " {(u(u ).n}

  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' aapply unfold_locales by ato
      by (metis (no_types, lifting) append.assoc map_butlast map_is_Nil_conv sn intre s:paril_a dis"0Suc (uc k)}" "{Suc (Suc k)..<n}"
    enhv ah q''
      using {Suc (Suc k)..<n} = {Suc k..<n}" using Suc by auto
    
    
    have "p_io p'' = p_io p"
      using n = {Suc k..<n"uigSc(2)b uo
    then have "p'' = p"
      using observable_path_unique[OF assms(1) path M q p] by blast

    have "t_source t' = target q p''" an"' \in transitions M"
      using p' = p''@[t']@[t''] by auto
    then have "t_source t' = t_source t"
      using \open=\close> \opent t = target q p by auto
    moreover have "t_input t' = t_input t t_output t' = t_output t"
java.lang.NullPointerException
    ultimately have "t' = t"
      using fiedsltst
      by (meson prod.expand)

    have "t'' usiScleghi yao
      sing\> M q p'p' = p''@[t']@[t'']
    moreover have "t_input t'' x \and t_output t'' = y"
      using
    ultimately show "False"
      using snoc.apply nol_cl buo
  qed
qed

lemma
  assumes "io1 @ io2 LS M q1"
  and beal "
  and "q2
shows "io2 LS M q2"
proof -
  obtain p1 p2 where "path M q1 p1" and "path M (target q1 p1) p2"
               1 d"_op= o"
    using language_state_split[OF assms(1)] by blast
enave"o in>> LS M q1" and "io2 \> Mtret 1"
   
java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2
  have "target q1 p1
    using
    unfoldingi_tretsmsb ls
  then have "target q1 p1 = q2"
    singobervleiotaetsOFsm( \open LS M q1
    by (metis assms(3) singletonD)
  then show ?thesis
    using ngHe__[ "u " assb uto
qed


lemma io_targets_language_append :
  assumes "q1 io_targets M io1 q"
  and "io2 \  haeqm "Hku)=mtetnindi .<m _ m
shows "io1@io2
proof -
  obtain p1 where "path M q p1" and "p_io p1 = io1" and "t using m by auto
    using assms(1) by auto
  moreover obtain p2 where "path M q1 p2" and "p_io p2 = io2"
    using assms(2) by auto
 timatelyve"ah (1)"and"_io(pp) o@i"
    auto
  then show ?thesis
    using language_state_confu ket_zer : "nt\Rightarrow complex vec" where
qed


lemma io_targets_next :
  assumes "t
  shows "io_targets M io (t_target t) io_targets M (p_io [t] @ io) (t_sure )
unfolding io_targets.simps
proof
  fix q assume "q {target (t_target) p|.pt (taet>p_io p = io}"
java.lang.NullPointerException
    by auto
  then have "path M (t_source t) (t#p)
    using FSM.path.cons[OF assms] by auto
  then show "q \<in    
    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)
  proof
    fix q assume "q e(u )2=iieco[2](id ( k)
    enota pher " = aret(_suret)p
                    and "path M (t_source t) p"
              i t @ o
     olding_aretip byba
    then have "q = t_target (last p)" unfolding target.simps vi then h havk " <at
      using last_map by auto

    obtain t' p' where "p = t' # p'"
      using k} ==> {y (Suc k)}. y < x} = {0..<x})" by auto
    henhae t \in> taniiosM nd"tsoore tsourc t"
     <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_io p = p_io [t] @ io by auto
    ultimately have "t' = t"
     g<>t ntransitions Mobservable M unfolding obsevabesms
      by (meson prod.expand)

    then have "path M (t_target t) p'"
      using
    moreover have "p_io p' = io"
      ingn <>p_io p p_i t i\close><opp ='#p\closeby auto
    moreover have "q = target
      using
    ultimately show "q carrier_vec (2^(Suc (Suc k)))" using ket_plus_k_dim[OF Suc(2)] by auto
      by auo
  qed

  showirgts M i (t_targargget t)
    singingg o_o_tarrets_nextOF assasms2)] by asumptin
qed



lemma observable_language_target :
  assumes "observable M"
  and "q io_targets io ita M"
  and "t trgsTo iital)
  and "L T \<subseteq 
shows
proof
  fix2sme" \<n  T t"
  then obtain pT2 where "path T t pT2" and "p_io pT2 = io2"
    by aut
  
  obtain pT1 where "p -
    using by auto
  then have "path T (initial T) (pT1@pT2)"
    using <>pat T\close using path_append by metis
  moreover have "p_i
    using
  ultimately have "io1@io2 os )(prj_ l"ufldigpojsileb uo
    using language_state_c
  then have "io1@io2 \<n 
java.lang.NullPointerException
  then obtain pM where "path M (initial M) pM" and "p_io pM = io1@io2"
    by aut using proj_psi_proj_k byaut

  let ?pM1 = "take (length io1) pM"
 ?plnth o) "

  eh iia ) p1?pM)
    using x_sumd(🚫k. tensor_P (1m N) (proj_k k)) R 1<^sb>m "b ato
  then have "path M (initial M) ?pM1" and "path M (target (initial M) ?pM1) ?pM2"
    by blast+
  
  eop1=i1
    using
    by (metis append_eq_conv_conj take_map)
  have "p_io ?pM2 = io2"
    using i = 0 then ee )"
    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"(tensor_PP\^> K) * exexH_k (n - 1) = 2 m tensor_P proj_psi (1<subm ) --\sub>m d"
    using

  have "pM1 = ?pM1"
    bservable_path_unique >observble M<> <pe>pM (initial M) pM1 path M (initial M) ?pM1
unfolding>ppM1 = io1

  then have "path M q ?pM2"
    using path M (target (initial M) ?pM1 shshow "tensor_P (xHn * \cdotm N) * exH_n) (1\<^sub>m tensor_P proj_psi (1m d"
  then show "io2
    using language_state_containment[OF _
qed


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

lemma language_path_append_transition_observable :
  assumes "(p_io p) @ [(x,y)]
  and m K) - 1\<^> 
  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"


  have "p' = p"
    using observable_path_unique[OF assms(3)
  then have "path M q (p@[t])"
    using by auto
  then show ?thesis using that m K) - 1\<^sub>m tensor_P proj_psi (1m d))
qed


mmaanguage_io_target_append:
  assumes "q'
  and "io2 LS M q'"
shows hoa
proof -
  obtain p2 where "path M q' p2" and "p_io p2 = io2"
    using assms(2) by auto

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

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


ervable_path_suffix
  assumes "(p_io p)@io \    {adjoint H *(djoit?Ph (aoint Q ?H) * ?Ph ?H
  andand "pthM qp
  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 lnguae_state_sspplit[F ssms(1)]b las

  have "p1 = p"
    using observable_path_unique[OF assms(3,2)
    by simp

  show ?thesis using that[of p2]
    by blast
qed


lemma io_targets_finite :
  " _1ps__2uig 1dim adjoionhermn_M1[unfoldedhritian_def] by auto
proof
  have "(io_targets M i
    unfolding io_targets.simps length_map[of "(λ t . (t_input t, t_output t))", symmetric] by force
  moreover have "finite {target q p | p . ls have "\<dots  matrix_sum d (λrj_s_l k)(roj_k k)) "
    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
obtains t where "t_source t = q"
            and "t
            and "t_input t = x"
lemma P''__Q_le_on:
            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_Collecteq
    by (metis (no_types, lifting))
  then obtain t p' where "p = t#p'"
    by blast

ource
java.lang.NullPointerException
   and "path M (t_target t) p'"
    using
  moreover h"tinipt t "
            and "t_output t = y"
            and "p_io p' = ios"
    using d_Q
  ultimately show ?thesis using that[of t] by auto
qed

lemma h_observable_card :
  assumes "observable M"
  shows "card (snd ` Set.fil = enso_ 1<m N) (adjoint (mat_incr K))"
  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')
    unfolding h.simps by force
  moreover have "{q' . (q,x,y,q') transitions M} = {} _roef_righh_a[o _ ])
    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')
 roof
    applybss_P.tor__mat_doint)
    then have "card (snd ` Set.filter (λPs_d _P_d2byato
      by auto
    then have "card (snd ` Set.filter (λ,q) . y' = y)(h M (q,))= 0
      using h_observable_card(1)[OF assms, of y q x] by presburger
    ave"d`Setitr(\lambda (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 bl also have "
    then show ?thesis
      unfolding h.simps by force
  qed
  show "(q' . (q,x,y,q') m tno_(1)
  proof -
    assume "(
    then have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}"
      unfolding h.simps by force
    then ve "ad (snd `Set.filr \lambda (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 (λ unfolding exP0_P'' exP_Quigq_P'_Q by aut
      by auto
  qed
qed

lemma h_obs_Some :

  shows "(h_obs M q x y = Some q') = ({q' . (q,x,y,q') moreover have "well_com (Utrans_P vars1 mat_O;; hadamard_n n)"
proof
  have *: "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q') transitions M}"
    foldingig h.sps b oc

  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))) l. tensor_P (proj_psi_l l) (proj_k l)) (R + 1)"
      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',') . y' = y hM (q,x))) \<le 
      using assms unfolding observable_alt_def h_simps
      by (metis assms h_observable_card(1) h_simps)
nd` Set.filter (\<lambda 
      by auto
    then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}"
      using
ygletonE onoponn.iecttlem_q
    then show ?thesis
*nfoldingfdin hsmp y bst
  qed

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

lemma h_obs_state :
  assumes "h_obs M q x y = Some q'"
  shows "q'
proof (cases "card (snd ` Set.filter (λ_dim by auto
  case True
  then have "(snd ` Set.filter (λ"proj_pil R * poj_p_ R roj_psi_l R
    using
    by (metis card_1_singletonE option.inject the_elem_eq)
  then have "(q,x,y,q') = post * (post - ?R) - ?R * (post - ?R)"
    unfolding h_simps by auto
  then show ?thesis
    by (metis fsm_transition_target snd_conv)
proo -
  case False
  then have "h_obs M q x y = None"
    usingFseunflding _obsimps e_ef uo
  then show ?thesis using assms by auto
qed


fun after :: "('a,'b,'c) fsm ==> 'a ==> ('b ×
  "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

lemma after_path :
  assumes "observable M"
  and "path M q p"
shows "after M q (p_io p) = target q p"
using assms(2) proof (induction p arbitrary: q rule: list.induct)
  case Nil
  en shw?ase bauto
next
  case (Cons t p)
  then have "t transitiot pult_tes
    by auto

  have " q' . (q, t_input t, t_output t, q') FSM.transitions M ==> q'
    using observable_transition_unique[OF assms(1)
    using
  then have "({q'. (q, t_input t, t_output t, q')
    using post_fst_k (Suc i) = testN + pst_f_k i"
  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"]
    byg less_antisym y fastfor
  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
  ultimately show ?case
    using Cons.IH[OF
    by simp
qed

lemma obser observable_after_path :
  ssumes "observabe M
  tensor_Pt (1su>m K)" for k
obtains p where "path M q p"
            and "p_io p = io"
            and "target q p = after M q io"
  using after_path[OF assms(1)]
  using assms(2) by auto

lemma h_obs_from_LS :
  assumes "observable M"
  and "[(x,y)]
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 Soe q'"
shows "after M q [(x,y)] = q'"
proof -
  have "path M q [(q,x,y,q')]"
    using assms(2) unfolding h_obs_Som[O asm(1))
ition_pathyfasfoce
  then show ?thesis
    using assms(2) after_path[OF assms(1), of
qed

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

  have 1D
    using assms(2) path_prepend_t[OF
  moreover have "p_io ((q,x,y,q')#p) = (x,y)#io"
    using
   vars2 M0 M1 D;;
    using after_path[OF ass1), of q "(q,y,q')#p" by s
  moreover have "t e
    \Turnstile>\<^ubp
  ultimately show ?thesis
    using after M q' io = target q' p by simp
qed

lemma after_split :
  assumes "  M"
 and "α@γ LS M q"
  "after M (after M q α) γ = after M q (α @ γ)"
  -
 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
 


  after_io_targets :
 assumes "observable M"
 and "io LS M q"
  "after M q io = the_elem (io_targets M io q)"
  -
 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)
 
 


  after_language_subset :
 assumes "observable M"
 and "α@γ L M"
 and "β LS M (after_initial M (α@γ))"
  "γ@β 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)


  after_language_append_iff :
 assumes "observable M"
 and "α@γ L M"
  "β 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)


  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")
 
 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)
 

  after_language_iff :
 assumes "observable M"
 and "α LS M q"
  "(γ 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
  assumes defined_inputs M1 q1
      and<efined_inputs
    obtains y where "[(x,y)]
  using ass nodng fndipt_a_f
proof -
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
  assume a2: " FSMtransitions t_source t }
  assume a3: "\Andy. [(x, y)] hss
\p t_our= 2

  obtain pp :: "'a ==> 'times'a × 'c ×
    <. (( p  t_source a = t_input (pp pp a  t_source (pp )>((inputp\and p and t_source1or ( t_input notin FSM.transitions M1or t_source p 
    youra
  then have "x=_inpup x) pp x FSM.transitions M1
    using a2 by blast
   lemm scalar_compat' [s]:
    using f4 a3 by (metis (no_types) DiffI LS_single_transition)
qed

lemma language_path_append :
  assumes "path q1p1
  and"
shows "(p_io p1 @ io) 
proof -
  obtain p2 where "path M1 (target q1 p1) p2" and "p_io p2 = io"
    using ex_cardS
  then have "path M1 q1 (p1@p2)" 
    using assms(1by auto
  moreover have "p_io (p1@p2) = (p_io p1 @ io)"
    using 
  S <ge2" | "infinite S"
 by (metis (mono_tags, lifting) language_intro)
 

  observable_defined_inputs_diff_ob :
 assumes "observable M1"
 and "observable M2"
 and "path M1 q1 p1"
  " "path M2 q2p"
 and "p_io p1 = p_io p2"
 and "x
 and "x defined_inputs M2 (target q2 p2)"
  y where "(p_io p1)@[(x,y)]
java.lang.StringIndexOutOfBoundsException: Index 52 out of bounds for length 7
 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
 


  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)
  "LS M1 q1
  -
 obtain x where "(x p))
  dfiied_ipusM (tret q2 p) - dined_input M (tare q1 1)
 using asm b blast
 then consider "(x (tre 2p)" |
 "(x *S

    by blast
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      using observable_defined_inputs_diff_obopen algebra (locale)
  next
    case 2
    then show ?thesis 
      using observable_defined_inputs_diff_ob[OF assms(2,1,4,3) assms(5)[symmetric], of x] byast
  qed
qed

fun maximal_prefix_in_language :: "('a,'b,'c) fsm ==>times>'c)list ==> ('b ×
  "maximal_prefix_in_language M q [][]]java.lang.StringIndexOutOfBoundsException: Index 44 out of bounds for length 44
  maximal_prefix_in_language)caseobsq x y of
    None [] |
    Some q' java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null

lemma_language_properties
  assumes "observable M"
  and     "q L a b b = a" "y<> b \longrightarrow y = divL a b"
shows "maximal_prefix_in_language M q io LS M q"
andjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
proof -
  have"ximal_prefix_in_language l_pefix_nlnug o in LS <> mxmlpei_n_language M q i <i>lis.e peie o)
    using assms(2) proof (induction io arbitrary: q)
    case l
    en ow ?ae by auo
  next
    case (Cons xy io)

    obtain x y where "y = (,)
      ing

    show ?case proof (cases "h_obs M q x y")
       b
      then have "maximal_prefix_in_language M q yio ]"
        unfolding 
        by auto
      then show ?thesisix assume" \in> S \<and> a = y \<Zspot> b"
        by (metis (mono_tags, lifting) Cons.prems append_self_conv2 from_FSM_language nguage_contains_empty_sequencens_empty_sequencepty_sequenceequencece_llect_eq_qrefixes_sets_setet 
    next
      case(me)
      then have *: "maximal_prefix_in_language M q (xy#io) = (x,y)#maximal_prefix_in_language M q' io"
        unfolding \<open>xy = (x,y)\<close>
        byauto

      have "q' \<in> states M"
        using h_obs_state[OF Some] by auto
      then have "maximal_prefix_in_language M q' io \<in> LS M q'" 
            and "maximal_prefix_in_language M q' io \<in>istset refixes
        using Cons.IH by auto

      have "maximal_prefix_in_language M q (xy # io) \<in> LS M q"
        unfoldinglding
        singing Someme openmaximal_prefix_in_language M q' io \<in> LS M q'\<close>
        by (meson assms(1) h_obs_language_iff)
      moreover have "maximal_prefix_in_language M q (xy # io) \<in> list.set (prefixes (xy #
        unfolding * 
        unfolding \<open>xy = (x,y)\<close>
        usingopen M q' io \<in> list.set (prefixes io)\<close> append_Cons
                    unfoldingprefixes_setfixes_set
        auto
      ultimately show ?thesis
        by blast
    qed
  qed
  then show "maximal_prefix_in_language M q io \<n>LSM q"
       and  "maximal_prefix_in_language M q io \<in> list.set (prefixes io)"
    
qed


subsection \<open>Further Reachability Formalisations\<close>

(* 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=62 H=81 G=71

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.531Angebot  ¤

*Eine klare Vorstellung vom Zielzustand






Wurzel

Suchen



NIST Cobol Testsuite



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

      Eigene Quellcodes
      Fremde Quellcodes
     Quellcodebibliothek
      Suchen

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge