section ‹Finite State Machines› text ‹This theory defines well-formed finite state machines and introduces various closely related notions, as well as a selection of basic properties and definitions.› theory FSM imports FSM_Impl "HOL-Library.Quotient_Type" "HOL-Library.Product_Lexorder" begin subsection ‹Well-formed Finite State Machines› text ‹A value of type @{text "fsm_impl"} constitutes a well-formed FSM if its contained sets are finite and the initial state and the components of each transition are contained in their respective sets.› abbreviation(input) "well_formed_fsm (M :: ('state, 'input, 'output) fsm_impl) ≡ (initial M ∈ states M ∧ finite (states M) ∧ finite (inputs M) ∧ finite (outputs M) ∧ finite (transitions M) ∧ (∀ t ∈ transitions M . t_source t ∈ states M ∧ t_input t ∈ inputs M ∧ t_target t ∈ states M ∧ t_output t ∈ outputs M)) " typedef ('state, 'input, 'output) fsm = "{ M :: ('state, 'input, 'output) fsm_impl . well_formed_fsm M}" morphisms fsm_impl_of_fsm Abs_fsm proof - obtain q :: 'state where "True" by blast have "well_formed_fsm (FSMI q {q} {} {} {})" by auto then show ?thesis by blast qed setup_lifting type_definition_fsm lift_definition initial :: "('state, 'input, 'output) fsm ⇒ 'state" is FSM_Impl.initial done lift_definition states :: "('state, 'input, 'output) fsm ⇒ 'state set" is FSM_Impl.states done lift_definition inputs :: "('state, 'input, 'output) fsm ⇒ 'input set" is FSM_Impl.inputs done lift_definition outputs :: "('state, 'input, 'output) fsm ⇒ 'output set" is FSM_Impl.outputs done lift_definition transitions :: "('state, 'input, 'output) fsm ⇒ ('state × 'input × 'output × 'state) set" is FSM_Impl.transitions done lift_definition fsm_from_list :: "'a ⇒ ('a,'b,'c) transition list ⇒ ('a, 'b, 'c) fsm" is FSM_Impl.fsm_impl_from_list proof - fix q :: 'a fix ts :: "('a,'b,'c) transition list" show "well_formed_fsm (fsm_impl_from_list q ts)" by (induction ts; auto) qed lemma fsm_initial[intro]: "initial M ∈ states M" by (transfer; blast) lemma fsm_states_finite: "finite (states M)" by (transfer; blast) lemma fsm_inputs_finite: "finite (inputs M)" by (transfer; blast) lemma fsm_outputs_finite: "finite (outputs M)" by (transfer; blast) lemma fsm_transitions_finite: "finite (transitions M)" by (transfer; blast) lemma fsm_transition_source[intro]: "⋀ t . t ∈ (transitions M) ⟹ t_source t ∈ states M" by (transfer; blast) lemma fsm_transition_target[intro]: "⋀ t . t ∈ (transitions M) ⟹ t_target t ∈ states M" by (transfer; blast) lemma fsm_transition_input[intro]: "⋀ t . t ∈ (transitions M) ⟹ t_input t ∈ inputs M" by (transfer; blast) lemma fsm_transition_output[intro]: "⋀ t . t ∈ (transitions M) ⟹ t_output t ∈ outputs M" by (transfer; blast) instantiation fsm :: (type,type,type) equal begin definition equal_fsm :: "('a, 'b, 'c) fsm ⇒ ('a, 'b, 'c) fsm ⇒ bool" where "equal_fsm x y = (initial x = initial y ∧ states x = states y ∧ inputs x = inputs y ∧ outputs x = outputs y ∧ transitions x = transitions y)" instance apply (intro_classes) unfolding equal_fsm_def apply transfer using fsm_impl.expand by auto end subsubsection ‹Example FSMs› definition m_ex_H :: "(integer,integer,integer) fsm" where "m_ex_H = fsm_from_list 1 [ (1,0,0,2), (1,0,1,4), (1,1,1,4), (2,0,0,2), (2,1,1,4), (3,0,1,4), (3,1,0,1), (3,1,1,3), (4,0,0,3), (4,1,0,1)]" definition m_ex_9 :: "(integer,integer,integer) fsm" where "m_ex_9 = fsm_from_list 0 [ (0,0,2,2), (0,0,3,2), (0,1,0,3), (0,1,1,3), (1,0,3,2), (1,1,1,3), (2,0,2,2), (2,1,3,3), (3,0,2,2), (3,1,0,2), (3,1,1,1)]" definition m_ex_DR :: "(integer,integer,integer) fsm" where "m_ex_DR = fsm_from_list 0 [(0,0,0,100), (100,0,0,101), (100,0,1,101), (101,0,0,102), (101,0,1,102), (102,0,0,103), (102,0,1,103), (103,0,0,104), (103,0,1,104), (104,0,0,100), (104,0,1,100), (104,1,0,400), (0,0,2,200), (200,0,2,201), (201,0,2,202), (202,0,2,203), (203,0,2,200), (203,1,0,400), (0,1,0,300), (100,1,0,300), (101,1,0,300), (102,1,0,300), (103,1,0,300), (200,1,0,300), (201,1,0,300), (202,1,0,300), (300,0,0,300), (300,1,0,300), (400,0,0,300), (400,1,0,300)]" subsection ‹Transition Function h and related functions› lift_definition h :: "('state, 'input, 'output) fsm ⇒ ('state × 'input) ⇒ ('output × 'state) set" is FSM_Impl.h . lemma h_simps[simp]: "FSM.h M (q,x) = { (y,q') . (q,x,y,q') ∈ transitions M }" by (transfer; auto) lift_definition h_obs :: "('state, 'input, 'output) fsm ⇒ 'state ⇒ 'input ⇒ 'output ⇒ 'state option" is FSM_Impl.h_obs . lemma h_obs_simps[simp]: "FSM.h_obs M q x y = (let tgts = snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) in if card tgts = 1 then Some (the_elem tgts) else None)" by (transfer; auto) fun defined_inputs' :: "(('a ×'b) ⇒ ('c×'a) set) ⇒ 'b set ⇒ 'a ⇒ 'b set" where "defined_inputs' hM iM q = {x ∈ iM . hM (q,x) ≠ {}}" fun defined_inputs :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'b set" where "defined_inputs M q = defined_inputs' (h M) (inputs M) q" lemma defined_inputs_set : "defined_inputs M q = {x ∈ inputs M . h M (q,x) ≠ {} }" by auto fun transitions_from' :: "(('a ×'b) ⇒ ('c×'a) set) ⇒ 'b set ⇒ 'a ⇒ ('a,'b,'c) transition set" where "transitions_from' hM iM q = ⋃(image (λx . image (λ(y,q') . (q,x,y,q')) (hM (q,x))) iM)" fun transitions_from :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('a,'b,'c) transition set" where "transitions_from M q = transitions_from' (h M) (inputs M) q" lemma transitions_from_set : assumes "q ∈ states M" shows "transitions_from M q = {t ∈ transitions M . t_source t = q}" proof - have "⋀ t . t ∈ transitions_from M q ⟹ t ∈ transitions M ∧ t_source t = q" by auto moreover have "⋀ t . t ∈ transitions M ⟹ t_source t = q ⟹ t ∈ transitions_from M q" proof - fix t assume "t ∈ transitions M" and "t_source t = q" then have "(t_output t, t_target t) ∈ h M (q,t_input t)" and "t_input t ∈ inputs M" by auto then have "t_input t ∈ defined_inputs' (h M) (inputs M) q" unfolding defined_inputs'.simps ‹t_source t = q› by blast have "(q, t_input t, t_output t, t_target t) ∈ transitions M" using ‹t_source t = q› ‹t ∈ transitions M› by auto then have "(q, t_input t, t_output t, t_target t) ∈ (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)" using ‹(t_output t, t_target t) ∈ h M (q,t_input t)› unfolding h.simps by (metis (no_types, lifting) image_iff prod.case_eq_if surjective_pairing) then have "t ∈ (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)" using ‹t_source t = q› by (metis prod.collapse) then show "t ∈ transitions_from M q" unfolding transitions_from.simps transitions_from'.simps using ‹t_input t ∈ defined_inputs' (h M) (inputs M) q› using ‹t_input t ∈ FSM.inputs M› by blast qed ultimately show ?thesis by blast qed fun h_from :: "('state, 'input, 'output) fsm ⇒ 'state ⇒ ('input × 'output × 'state) set" where "h_from M q = { (x,y,q') . (q,x,y,q') ∈ transitions M }" lemma h_from[code] : "h_from M q = (let m = set_as_map (transitions M) in (case m q of Some yqs ⇒ yqs | None ⇒ {}))" unfolding set_as_map_def by force fun h_out :: "('a,'b,'c) fsm ⇒ ('a × 'b) ⇒ 'c set" where "h_out M (q,x) = {y . ∃ q' . (q,x,y,q') ∈ transitions M}" lemma h_out_code[code]: "h_out M = (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs ⇒ yqs | None ⇒ {}))" proof - let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs ⇒ yqs | None ⇒ {}))" have "⋀ qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs ⇒ yqs | None ⇒ {})) qx = (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx" unfolding set_as_map_def by auto moreover have "⋀ qx . (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ (transitions M)}) qx" by force ultimately have "?f = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ (transitions M)})" by blast then have "?f = (λ (q,x) . {y | y . ∃ q' . (q, x, y, q') ∈ (transitions M)})" by force then show ?thesis by force qed lemma h_out_alt_def : "h_out M (q,x) = {t_output t | t . t ∈ transitions M ∧ t_source t = q ∧ t_input t = x}" unfolding h_out.simps by auto subsection ‹Size› instantiation fsm :: (type,type,type) size begin definition size where [simp, code]: "size (m::('a, 'b, 'c) fsm) = card (states m)" instance .. end lemma fsm_size_Suc : "size M > 0" unfolding FSM.size_def using fsm_states_finite[of M] fsm_initial[of M] using card_gt_0_iff by blast subsection ‹Paths› inductive path :: "('state, 'input, 'output) fsm ⇒ 'state ⇒ ('state, 'input, 'output) path ⇒ bool" where nil[intro!] : "q ∈ states M ⟹ path M q []" | cons[intro!] : "t ∈ transitions M ⟹ path M (t_target t) ts ⟹ path M (t_source t) (t#ts)" inductive_cases path_nil_elim[elim!]: "path M q []" inductive_cases path_cons_elim[elim!]: "path M q (t#ts)" fun visited_states :: "'state ⇒ ('state, 'input, 'output) path ⇒ 'state list" where "visited_states q p = (q # map t_target p)" fun target :: "'state ⇒ ('state, 'input, 'output) path ⇒ 'state" where "target q p = last (visited_states q p)" lemma target_nil [simp] : "target q [] = q" by auto lemma target_snoc [simp] : "target q (p@[t]) = t_target t" by auto lemma path_begin_state : assumes "path M q p" shows "q ∈ states M" using assms by (cases; auto) lemma path_append[intro!] : assumes "path M q p1" and "path M (target q p1) p2" shows "path M q (p1@p2)" using assms by (induct p1 arbitrary: p2; auto) lemma path_target_is_state : assumes "path M q p" shows "target q p ∈ states M" using assms by (induct p; auto) lemma path_suffix : assumes "path M q (p1@p2)" shows "path M (target q p1) p2" using assms by (induction p1 arbitrary: q; auto) lemma path_prefix : assumes "path M q (p1@p2)" shows "path M q p1" using assms by (induction p1 arbitrary: q; auto; (metis path_begin_state)) lemma path_append_elim[elim!] : assumes "path M q (p1@p2)" obtains "path M q p1" and "path M (target q p1) p2" by (meson assms path_prefix path_suffix) lemma path_append_target: "target q (p1@p2) = target (target q p1) p2" by (induction p1) (simp+) lemma path_append_target_hd : assumes "length p > 0" shows "target q p = target (t_target (hd p)) (tl p)" using assms by (induction p) (simp+) lemma path_transitions : assumes "path M q p" shows "set p ⊆ transitions M" using assms by (induct p arbitrary: q; fastforce) lemma path_append_transition[intro!] : assumes "path M q p" and "t ∈ transitions M" and "t_source t = target q p" shows "path M q (p@[t])" by (metis assms(1) assms(2) assms(3) cons fsm_transition_target nil path_append) lemma path_append_transition_elim[elim!] : assumes "path M q (p@[t])" shows "path M q p" and "t ∈ transitions M" and "t_source t = target q p" using assms by auto lemma path_prepend_t : "path M q' p ⟹ (q,x,y,q') ∈ transitions M ⟹ path M q ((q,x,y,q')#p)" by (metis (mono_tags, lifting) fst_conv path.intros(2) prod.sel(2)) lemma path_target_append : "target q1 p1 = q2 ⟹ target q2 p2 = q3 ⟹ target q1 (p1@p2) = q3" by auto lemma single_transition_path : "t ∈ transitions M ⟹ path M (t_source t) [t]" by auto lemma path_source_target_index : assumes "Suc i < length p" and "path M q p" shows "t_target (p ! i) = t_source (p ! (Suc i))" using assms proof (induction p rule: rev_induct) case Nil then show ?case by auto next case (snoc t ps) then have "path M q ps" and "t_source t = target q ps" and "t ∈ transitions M" by auto show ?case proof (cases "Suc i < length ps") case True then have "t_target (ps ! i) = t_source (ps ! Suc i)" using snoc.IH ‹path M q ps› by auto then show ?thesis by (simp add: Suc_lessD True nth_append) next case False then have "Suc i = length ps" using snoc.prems(1) by auto then have "(ps @ [t]) ! Suc i = t" by auto show ?thesis proof (cases "ps = []") case True then show ?thesis using ‹Suc i = length ps› by auto next case False then have "target q ps = t_target (last ps)" unfolding target.simps visited_states.simps by (simp add: last_map) then have "target q ps = t_target (ps ! i)" using ‹Suc i = length ps› by (metis False diff_Suc_1 last_conv_nth) then show ?thesis using ‹t_source t = target q ps› by (metis ‹(ps @ [t]) ! Suc i = t› ‹Suc i = length ps› lessI nth_append) qed qed qed lemma paths_finite : "finite { p . path M q p ∧ length p ≤ k }" proof - have "{ p . path M q p ∧ length p ≤ k } ⊆ {xs . set xs ⊆ transitions M ∧ length xs ≤ k}" by (metis (no_types, lifting) Collect_mono path_transitions) then show "finite { p . path M q p ∧ length p ≤ k }" using finite_lists_length_le[OF fsm_transitions_finite[of M], of k] by (metis (mono_tags) finite_subset) qed lemma visited_states_prefix : assumes "q' ∈ set (visited_states q p)" shows "∃ p1 p2 . p = p1@p2 ∧ target q p1 = q'" using assms proof (induction p arbitrary: q) case Nil then show ?case by auto next case (Cons a p) then show ?case proof (cases "q' ∈ set (visited_states (t_target a) p)") case True then obtain p1 p2 where "p = p1 @ p2 ∧ target (t_target a) p1 = q'" using Cons.IH by blast then have "(a#p) = (a#p1)@p2 ∧ target q (a#p1) = q'" by auto then show ?thesis by blast next case False then have "q' = q" using Cons.prems by auto then show ?thesis by auto qed qed lemma visited_states_are_states : assumes "path M q1 p" shows "set (visited_states q1 p) ⊆ states M" by (metis assms path_prefix path_target_is_state subsetI visited_states_prefix) lemma transition_subset_path : assumes "transitions A ⊆ transitions B" and "path A q p" and "q ∈ states B" shows "path B q p" using assms(2) proof (induction p rule: rev_induct) case Nil show ?case using assms(3) by auto next case (snoc t p) then show ?case using assms(1) path_suffix by fastforce qed subsubsection ‹Paths of fixed length› fun paths_of_length' :: "('a,'b,'c) path ⇒ 'a ⇒ (('a ×'b) ⇒ ('c×'a) set) ⇒ 'b set ⇒ nat ⇒ ('a,'b,'c) path set" where "paths_of_length' prev q hM iM 0 = {prev}" | "paths_of_length' prev q hM iM (Suc k) = (let hF = transitions_from' hM iM q in ⋃ (image (λ t . paths_of_length' (prev@[t]) (t_target t) hM iM k) hF))" fun paths_of_length :: "('a,'b,'c) fsm ⇒ 'a ⇒ nat ⇒ ('a,'b,'c) path set" where "paths_of_length M q k = paths_of_length' [] q (h M) (inputs M) k" subsubsection ‹Paths up to fixed length› fun paths_up_to_length' :: "('a,'b,'c) path ⇒ 'a ⇒ (('a ×'b) ⇒ (('c×'a) set)) ⇒ 'b set ⇒ nat ⇒ ('a,'b,'c) path set" where "paths_up_to_length' prev q hM iM 0 = {prev}" | "paths_up_to_length' prev q hM iM (Suc k) = (let hF = transitions_from' hM iM q in insert prev (⋃ (image (λ t . paths_up_to_length' (prev@[t]) (t_target t) hM iM k) hF)))" fun paths_up_to_length :: "('a,'b,'c) fsm ⇒ 'a ⇒ nat ⇒ ('a,'b,'c) path set" where "paths_up_to_length M q k = paths_up_to_length' [] q (h M) (inputs M) k" lemma paths_up_to_length'_set : assumes "q ∈ states M" and "path M q prev" shows "paths_up_to_length' prev (target q prev) (h M) (inputs M) k = {(prev@p) | p . path M (target q prev) p ∧ length p ≤ k}" using assms(2) proof (induction k arbitrary: prev) case 0 show ?case unfolding paths_up_to_length'.simps using path_target_is_state[OF "0.prems"(1)] by auto next case (Suc k) have "⋀ p . p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k) ⟹ p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k}" proof - fix p assume "p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)" then show "p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k}" proof (cases "p = prev") case True show ?thesis using path_target_is_state[OF Suc.prems(1)] unfolding True by (simp add: nil) next case False then have "p ∈ (⋃ (image (λt. paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k) (transitions_from' (h M) (inputs M) (target q prev))))" using ‹p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)› unfolding paths_up_to_length'.simps Let_def by blast then obtain t where "t ∈ ⋃(image (λx . image (λ(y,q') . ((target q prev),x,y,q')) (h M ((target q prev),x))) (inputs M))" and "p ∈ paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k" unfolding transitions_from'.simps by blast have "t ∈ transitions M" and "t_source t = (target q prev)" using ‹t ∈ ⋃(image (λx . image (λ(y,q') . ((target q prev),x,y,q')) (h M ((target q prev),x))) (inputs M))› by auto then have "path M q (prev@[t])" using Suc.prems(1) using path_append_transition by simp have "(target q (prev @ [t])) = t_target t" by auto show ?thesis using ‹p ∈ paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k› using Suc.IH[OF ‹path M q (prev@[t])›] unfolding ‹(target q (prev @ [t])) = t_target t› using ‹path M q (prev @ [t])› by auto qed qed moreover have "⋀ p . p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k} ⟹ p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)" proof - fix p assume "p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k}" then obtain p' where "p = prev@p'" and "path M (target q prev) p'" and "length p' ≤ Suc k" by blast have "prev@p' ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)" proof (cases p') case Nil then show ?thesis by auto next case (Cons t p'') then have "t ∈ transitions M" and "t_source t = (target q prev)" using ‹path M (target q prev) p'› by auto then have "path M q (prev@[t])" using Suc.prems(1) using path_append_transition by simp have "(target q (prev @ [t])) = t_target t" by auto have "length p'' ≤ k" using ‹length p' ≤ Suc k› Cons by auto moreover have "path M (target q (prev@[t])) p''" using ‹path M (target q prev) p'› unfolding Cons by auto ultimately have "p ∈ paths_up_to_length' (prev @ [t]) (t_target t) (h M) (FSM.inputs M) k" using Suc.IH[OF ‹path M q (prev@[t])›] unfolding ‹(target q (prev @ [t])) = t_target t› ‹p = prev@p'› Cons by simp then have "prev@t#p'' ∈ paths_up_to_length' (prev @ [t]) (t_target t) (h M) (FSM.inputs M) k" unfolding ‹p = prev@p'› Cons by auto have "t ∈ (λ(y, q'). (t_source t, t_input t, y, q')) ` {(y, q'). (t_source t, t_input t, y, q') ∈ FSM.transitions M}" using ‹t ∈ transitions M› by (metis (no_types, lifting) case_prodI mem_Collect_eq pair_imageI surjective_pairing) then have "t ∈ transitions_from' (h M) (inputs M) (target q prev)" unfolding transitions_from'.simps using fsm_transition_input[OF ‹t ∈ transitions M›] unfolding ‹t_source t = (target q prev)›[symmetric] h_simps by blast then show ?thesis using ‹prev @ t # p'' ∈ paths_up_to_length' (prev@[t]) (t_target t) (h M) (FSM.inputs M) k› unfolding ‹p = prev@p'› Cons paths_up_to_length'.simps Let_def by blast qed then show "p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)" unfolding ‹p = prev@p'› by assumption qed ultimately show ?case by blast qed lemma paths_up_to_length_set : assumes "q ∈ states M" shows "paths_up_to_length M q k = {p . path M q p ∧ length p ≤ k}" unfolding paths_up_to_length.simps using paths_up_to_length'_set[OF assms nil[OF assms], of k] by auto subsubsection ‹Calculating Acyclic Paths› fun acyclic_paths_up_to_length' :: "('a,'b,'c) path ⇒ 'a ⇒ ('a ⇒ (('b×'c×'a) set)) ⇒ 'a set ⇒ nat ⇒ ('a,'b,'c) path set" where "acyclic_paths_up_to_length' prev q hF visitedStates 0 = {prev}" | "acyclic_paths_up_to_length' prev q hF visitedStates (Suc k) = (let tF = Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF q) in (insert prev (⋃ (image (λ (x,y,q') . acyclic_paths_up_to_length' (prev@[(q,x,y,q')]) q' hF (insert q' visitedStates) k) tF))))" fun p_source :: "'a ⇒ ('a,'b,'c) path ⇒ 'a" where "p_source q p = hd (visited_states q p)" lemma acyclic_paths_up_to_length'_prev : "p' ∈ acyclic_paths_up_to_length' (prev@prev') q hF visitedStates k ⟹ ∃ p'' . p' = prev@p''" by (induction k arbitrary: p' q visitedStates prev'; auto) lemma acyclic_paths_up_to_length'_set : assumes "path M (p_source q prev) prev" and "⋀ q' . hF q' = {(x,y,q'') | x y q'' . (q',x,y,q'') ∈ transitions M}" and "distinct (visited_states (p_source q prev) prev)" and "visitedStates = set (visited_states (p_source q prev) prev)" shows "acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates k = { prev@p | p . path M (p_source q prev) (prev@p) ∧ length p ≤ k ∧ distinct (visited_states (p_source q prev) (prev@p)) }" using assms proof (induction k arbitrary: q hF prev visitedStates) case 0 then show ?case by auto next case (Suc k) let ?tgt = "(target (p_source q prev) prev)" have "⋀ p . (prev@p) ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) ⟹ path M (p_source q prev) (prev@p) ∧ length p ≤ Suc k ∧ distinct (visited_states (p_source q prev) (prev@p))" proof - fix p assume "(prev@p) ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)" then consider (a) "(prev@p) = prev" | (b) "(prev@p) ∈ (⋃ (image (λ (x,y,q') . acyclic_paths_up_to_length' (prev@[(?tgt,x,y,q')]) q' hF (insert q' visitedStates) k) (Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF (target (p_source q prev) prev)))))" by auto then show "path M (p_source q prev) (prev@p) ∧ length p ≤ Suc k ∧ distinct (visited_states (p_source q prev) (prev@p))" proof (cases) case a then show ?thesis using Suc.prems(1,3) by auto next case b then obtain x y q' where *: "(x,y,q') ∈ Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF ?tgt)" and **:"(prev@p) ∈ acyclic_paths_up_to_length' (prev@[(?tgt,x,y,q')]) q' hF (insert q' visitedStates) k" by auto let ?t = "(?tgt,x,y,q')" from * have "?t ∈ transitions M" and "q' ∉ visitedStates" using Suc.prems(2)[of ?tgt] by simp+ moreover have "t_source ?t = target (p_source q prev) prev" by simp moreover have "p_source (p_source q prev) (prev@[?t]) = p_source q prev" by auto ultimately have p1: "path M (p_source (p_source q prev) (prev@[?t])) (prev@[?t])" using Suc.prems(1) by (simp add: path_append_transition) have "q' ∉ set (visited_states (p_source q prev) prev)" using ‹q' ∉ visitedStates› Suc.prems(4) by auto then have p2: "distinct (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))" using Suc.prems(3) by auto have p3: "(insert q' visitedStates) = set (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))" using Suc.prems(4) by auto have ***: "(target (p_source (p_source q prev) (prev @ [(target (p_source q prev) prev, x, y, q')])) (prev @ [(target (p_source q prev) prev, x, y, q')])) = q'" by auto show ?thesis using Suc.IH[OF p1 Suc.prems(2) p2 p3] ** unfolding *** unfolding ‹p_source (p_source q prev) (prev@[?t]) = p_source q prev› proof - assume "acyclic_paths_up_to_length' (prev @ [(target (p_source q prev) prev, x, y, q')]) q' hF (insert q' visitedStates) k = {(prev @ [(target (p_source q prev) prev, x, y, q')]) @ p |p. path M (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ p) ∧ length p ≤ k ∧ distinct (visited_states (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ p))}" then have "∃ps. prev @ p = (prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps ∧ path M (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps) ∧ length ps ≤ k ∧ distinct (visited_states (p_source q prev) ((prev @ [(target (p_source q prev) prev, x, y, q')]) @ ps))" using ‹prev @ p ∈ acyclic_paths_up_to_length' (prev @ [(target (p_source q prev) prev, x, y, q')]) q' hF (insert q' visitedStates) k› by blast then show ?thesis by (metis (no_types) Suc_le_mono append.assoc append.right_neutral append_Cons length_Cons same_append_eq) qed qed qed moreover have "⋀ p' . p' ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) ⟹ ∃ p'' . p' = prev@p''" using acyclic_paths_up_to_length'_prev[of _ prev "[]" "target (p_source q prev) prev" hF visitedStates "Suc k"] by force ultimately have fwd: "⋀ p' . p' ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k) ⟹ p' ∈ { prev@p | p . path M (p_source q prev) (prev@p) ∧ length p ≤ Suc k ∧ distinct (visited_states (p_source q prev) (prev@p)) }" by blast have "⋀ p . path M (p_source q prev) (prev@p) ⟹ length p ≤ Suc k ⟹ distinct (visited_states (p_source q prev) (prev@p)) ⟹ (prev@p) ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)" proof - fix p assume "path M (p_source q prev) (prev@p)" and "length p ≤ Suc k" and "distinct (visited_states (p_source q prev) (prev@p))" show "(prev@p) ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)" proof (cases p) case Nil then show ?thesis by auto next case (Cons t p') then have "t_source t = target (p_source q (prev)) (prev)" and "t ∈ transitions M" using ‹path M (p_source q prev) (prev@p)› by auto have "path M (p_source q (prev@[t])) ((prev@[t])@p')" and "path M (p_source q (prev@[t])) ((prev@[t]))" using Cons ‹path M (p_source q prev) (prev@p)› by auto have "length p' ≤ k" using Cons ‹length p ≤ Suc k› by auto have "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])@p'))" and "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])))" using Cons ‹distinct (visited_states (p_source q prev) (prev@p))› by auto then have "t_target t ∉ visitedStates" using Suc.prems(4) by auto let ?vN = "insert (t_target t) visitedStates" have "?vN = set (visited_states (p_source q (prev @ [t])) (prev @ [t]))" using Suc.prems(4) by auto have "prev@p = prev@([t]@p')" using Cons by auto have "(prev@[t])@p' ∈ acyclic_paths_up_to_length' (prev @ [t]) (target (p_source q (prev @ [t])) (prev @ [t])) hF (insert (t_target t) visitedStates) k" using Suc.IH[of q "prev@[t]", OF ‹path M (p_source q (prev@[t])) ((prev@[t]))› Suc.prems(2) ‹distinct (visited_states (p_source q (prev@[t])) ((prev@[t])))› ‹?vN = set (visited_states (p_source q (prev @ [t])) (prev @ [t]))› ] using ‹path M (p_source q (prev@[t])) ((prev@[t])@p')› ‹length p' ≤ k› ‹distinct (visited_states (p_source q (prev@[t])) ((prev@[t])@p'))› by force then have "(prev@[t])@p' ∈ acyclic_paths_up_to_length' (prev@[t]) (t_target t) hF ?vN k" by auto moreover have "(t_input t,t_output t, t_target t) ∈ Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF (t_source t))" using Suc.prems(2)[of "t_source t"] ‹t ∈ transitions M› ‹t_target t ∉ visitedStates› proof - have "∃b c a. snd t = (b, c, a) ∧ (t_source t, b, c, a) ∈ FSM.transitions M" by (metis (no_types) ‹t ∈ FSM.transitions M› prod.collapse) then show ?thesis using ‹hF (t_source t) = {(x, y, q'') |x y q''. (t_source t, x, y, q'') ∈ FSM.transitions M}› ‹t_target t ∉ visitedStates› by fastforce qed ultimately have "∃ (x,y,q') ∈ (Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF (target (p_source q prev) prev))) . (prev@[t])@p' ∈ (acyclic_paths_up_to_length' (prev@[((target (p_source q prev) prev),x,y,q')]) q' hF (insert q' visitedStates) k)" unfolding ‹t_source t = target (p_source q (prev)) (prev)› by (metis (no_types, lifting) ‹t_source t = target (p_source q prev) prev› case_prodI prod.collapse) then show ?thesis unfolding ‹prev@p = prev@[t]@p'› unfolding acyclic_paths_up_to_length'.simps Let_def by force qed qed then have rev: "⋀ p' . p' ∈ {prev@p | p . path M (p_source q prev) (prev@p) ∧ length p ≤ Suc k ∧ distinct (visited_states (p_source q prev) (prev@p))} ⟹ p' ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)" by blast show ?case using fwd rev by blast qed fun acyclic_paths_up_to_length :: "('a,'b,'c) fsm ⇒ 'a ⇒ nat ⇒ ('a,'b,'c) path set" where "acyclic_paths_up_to_length M q k = {p. path M q p ∧ length p ≤ k ∧ distinct (visited_states q p)}" lemma acyclic_paths_up_to_length_code[code] : "acyclic_paths_up_to_length M q k = (if q ∈ states M then acyclic_paths_up_to_length' [] q (m2f (set_as_map (transitions M))) {q} k else {})" proof (cases "q ∈ states M") case False then have "acyclic_paths_up_to_length M q k = {}" using path_begin_state by fastforce then show ?thesis using False by auto next case True then have *: "path M (p_source q []) []" by auto have **: "(⋀q'. (m2f (set_as_map (transitions M))) q' = {(x, y, q'') |x y q''. (q', x, y, q'') ∈ FSM.transitions M})" unfolding set_as_map_def by auto have ***: "distinct (visited_states (p_source q []) [])" by auto have ****: "{q} = set (visited_states (p_source q []) [])" by auto show ?thesis using acyclic_paths_up_to_length'_set[OF * ** *** ****, of k ] using True by auto qed lemma path_map_target : "target (f4 q) (map (λ t . (f1 (t_source t), f2 (t_input t), f3 (t_output t), f4 (t_target t))) p) = f4 (target q p)" by (induction p; auto) lemma path_length_sum : assumes "path M q p" shows "length p = (∑ q ∈ states M . length (filter (λt. t_target t = q) p))" using assms proof (induction p rule: rev_induct) case Nil then show ?case by auto next case (snoc x xs) then have "length xs = (∑q∈states 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 ***: "(∑q∈states M - {t_target x}. length (filter (λt. t_target t = q) (xs @ [x]))) = (∑q∈states 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 "(∑q∈states M. length (filter (λt. t_target t = q) (xs @ [x]))) = (∑q∈states 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 "(∑a∈insert (t_target x) (states M). length (filter (λp. t_target p = a) (xs @ [x]))) = (∑a∈states 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 "(∑q∈states M. length (filter (λt. t_target t = q) xs)) = (∑q∈states 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 "(∑a∈insert (t_target x) (states M). length (filter (λp. t_target p = a) xs)) = (∑a∈states 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 "(∑q∈states M. length (filter (λt. t_target t = q) (xs @ [x]))) = Suc (∑q∈states M. length (filter (λt. t_target t = q) xs))" using ** *** by auto then show ?case by (simp add: ‹length xs = (∑q∈states M. length (filter (λt. t_target t = q) xs))›) qed lemma path_loop_cut : assumes "path M q p" and "t_target (p ! i) = t_target (p ! j)" and "i < j" and "j < length p" shows "path M q ((take (Suc i) p) @ (drop (Suc j) p))" and "target q ((take (Suc i) p) @ (drop (Suc j) p)) = target q p" and "length ((take (Suc i) p) @ (drop (Suc j) p)) < length p" and "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p))" and "target (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p)) = (target q (take (Suc i) p))" proof - have "p = (take (Suc j) p) @ (drop (Suc j) p)" by auto also have "… = ((take (Suc i) (take (Suc j) p)) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p)" by (metis append_take_drop_id) also have "… = ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p)" using ‹i < j› by simp finally have "p = (take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p)" by simp then have "path M q ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p))" and "path M q (((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p))" using ‹path M q p› by auto have "path M q (take (Suc i) p)" and "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p) @ drop (Suc j) p)" using path_append_elim[OF ‹path M q ((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p)) @ (drop (Suc j) p))›] by blast+ have *: "(take (Suc i) p @ drop (Suc i) (take (Suc j) p)) = (take (Suc j) p)" using ‹i < j› append_take_drop_id by (metis ‹(take (Suc i) (take (Suc j) p) @ drop (Suc i) (take (Suc j) p)) @ drop (Suc j) p = (take (Suc i) p @ drop (Suc i) (take (Suc j) p)) @ drop (Suc j) p› append_same_eq) have "path M q (take (Suc j) p)" and "path M (target q (take (Suc j) p)) (drop (Suc j) p)" using path_append_elim[OF ‹path M q (((take (Suc i) p) @ (drop (Suc i) (take (Suc j) p))) @ (drop (Suc j) p))›] unfolding * by blast+ have **: "(target q (take (Suc j) p)) = (target q (take (Suc i) p))" proof - have "p ! i = last (take (Suc i) p)" by (metis Suc_lessD assms(3) assms(4) less_trans_Suc take_last_index) moreover have "p ! j = last (take (Suc j) p)" by (simp add: assms(4) take_last_index) ultimately show ?thesis using assms(2) unfolding * target.simps visited_states.simps by (simp add: last_map) qed show "path M q ((take (Suc i) p) @ (drop (Suc j) p))" using ‹path M q (take (Suc i) p)› ‹path M (target q (take (Suc j) p)) (drop (Suc j) p)› unfolding ** by auto show "target q ((take (Suc i) p) @ (drop (Suc j) p)) = target q p" by (metis "**" append_take_drop_id path_append_target) show "length ((take (Suc i) p) @ (drop (Suc j) p)) < length p" proof - have ***: "length p = length ((take (Suc j) p) @ (drop (Suc j) p))" by auto have "length (take (Suc i) p) < length (take (Suc j) p)" using assms(3,4) by (simp add: min_absorb2) have scheme: "⋀ a b c . length a < length b ⟹ length (a@c) < length (b@c)" by auto show ?thesis unfolding *** using scheme[OF ‹length (take (Suc i) p) < length (take (Suc j) p)›, of "(drop (Suc j) p)"] by assumption qed show "path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p))" using ‹path M (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p) @ drop (Suc j) p)› by blast show "target (target q (take (Suc i) p)) (drop (Suc i) (take (Suc j) p)) = (target q (take (Suc i) p))" by (metis "*" "**" path_append_target) qed lemma path_prefix_take : assumes "path M q p" shows "path M q (take i p)" proof - have "p = (take i p)@(drop i p)" by auto then have "path M q ((take i p)@(drop i p))" using assms by auto then show ?thesis by blast qed subsection ‹Acyclic Paths› lemma cyclic_path_loop : assumes "path M q p" and "¬ distinct (visited_states q p)" shows "∃ p1 p2 p3 . p = p1@p2@p3 ∧ p2 ≠ [] ∧ target q p1 = target q (p1@p2)" using assms proof (induction p arbitrary: q) case (nil M q) then show ?case by auto next case (cons t M ts) then show ?case proof (cases "distinct (visited_states (t_target t) ts)") case True then have "q ∈ set (visited_states (t_target t) ts)" using cons.prems by simp then obtain p2 p3 where "ts = p2@p3" and "target (t_target t) p2 = q" using visited_states_prefix[of q "t_target t" ts] by blast then have "(t#ts) = []@(t#p2)@p3 ∧ (t#p2) ≠ [] ∧ target q [] = target q ([]@(t#p2))" using cons.hyps by auto then show ?thesis by blast next case False then obtain p1 p2 p3 where "ts = p1@p2@p3" and "p2 ≠ []" and "target (t_target t) p1 = target (t_target t) (p1@p2)" using cons.IH by blast then have "t#ts = (t#p1)@p2@p3 ∧ p2 ≠ [] ∧ target q (t#p1) = target q ((t#p1)@p2)" by simp then show ?thesis by blast qed qed lemma cyclic_path_pumping : assumes "path M (initial M) p" and "¬ distinct (visited_states (initial M) p)" shows "∃ p . path M (initial M) p ∧ length p ≥ n" proof - from assms obtain p1 p2 p3 where "p = p1 @ p2 @ p3" and "p2 ≠ []" and "target (initial M) p1 = target (initial M) (p1 @ p2)" using cyclic_path_loop[of M "initial M" p] by blast then have "path M (target (initial M) p1) p3" using path_suffix[of M "initial M" "p1@p2" p3] ‹path M (initial M) p› by auto have "path M (initial M) p1" using path_prefix[of M "initial M" p1 "p2@p3"] ‹path M (initial M) p› ‹p = p1 @ p2 @ p3› by auto have "path M (initial M) ((p1@p2)@p3)" using ‹path M (initial M) p› ‹p = p1 @ p2 @ p3› by auto have "path M (target (initial M) p1) p2" using path_suffix[of M "initial M" p1 p2, OF path_prefix[of M "initial M" "p1@p2" p3, OF ‹path M (initial M) ((p1@p2)@p3)›]] by assumption have "target (target (initial M) p1) p2 = (target (initial M) p1)" using path_append_target ‹target (initial M) p1 = target (initial M) (p1 @ p2)› by auto have "path M (initial M) (p1 @ (concat (replicate n p2)) @ p3)" proof (induction n) case 0 then show ?case using path_append[OF ‹path M (initial M) p1› ‹path M (target (initial M) p1) p3›] by auto next case (Suc n) then show ?case using ‹path M (target (initial M) p1) p2› ‹target (target (initial M) p1) p2 = target (initial M) p1› by auto qed moreover have "length (p1 @ (concat (replicate n p2)) @ p3) ≥ n" proof - have "length (concat (replicate n p2)) = n * (length p2)" using concat_replicate_length by metis moreover have "length p2 > 0" using ‹p2 ≠ []› by auto ultimately have "length (concat (replicate n p2)) ≥ n" by (simp add: Suc_leI) then show ?thesis by auto qed ultimately show "∃ p . path M (initial M) p ∧ length p ≥ n" by blast qed lemma cyclic_path_shortening : assumes "path M q p" and "¬ distinct (visited_states q p)" shows "∃ p' . path M q p' ∧ target q p' = target q p ∧ length p' < length p" proof - obtain p1 p2 p3 where *: "p = p1@p2@p3 ∧ p2 ≠ [] ∧ target q p1 = target q (p1@p2)" using cyclic_path_loop[OF assms] by blast then have "path M q (p1@p3)" using assms(1) by force moreover have "target q (p1@p3) = target q p" by (metis (full_types) * path_append_target) moreover have "length (p1@p3) < length p" using * by auto ultimately show ?thesis by blast qed lemma acyclic_path_from_cyclic_path : assumes "path M q p" and "¬ distinct (visited_states q p)" obtains p' where "path M q p'" and "target q p = target q p'" and "distinct (visited_states q p')" proof - let ?paths = "{p' . (path M q p' ∧ target q p' = target q p ∧ length p' ≤ length p)}" let ?minPath = "arg_min length (λ io . io ∈ ?paths)" have "?paths ≠ empty" using assms(1) by auto moreover have "finite ?paths" using paths_finite[of M q "length p"] by (metis (no_types, lifting) Collect_mono rev_finite_subset) ultimately have minPath_def : "?minPath ∈ ?paths ∧ (∀ p' ∈ ?paths . length ?minPath ≤ length p')" by (meson arg_min_nat_lemma equals0I) then have "path M q ?minPath" and "target q ?minPath = target q p" by auto moreover have "distinct (visited_states q ?minPath)" proof (rule ccontr) assume "¬ distinct (visited_states q ?minPath)" have "∃ p' . path M q p' ∧ target q p' = target q p ∧ length p' < length ?minPath" using cyclic_path_shortening[OF ‹path M q ?minPath› ‹¬ distinct (visited_states q ?minPath)›] minPath_def ‹target q ?minPath= target q p› by auto then show "False" using minPath_def using arg_min_nat_le dual_order.strict_trans1 by auto qed ultimately show ?thesis by (simp add: that) qed lemma acyclic_path_length_limit : assumes "path M q p" and "distinct (visited_states q p)" shows "length p < size M" proof (rule ccontr) assume *: "¬ length p < size M" then have "length p ≥ card (states M)" using size_def by auto then have "length (visited_states q p) > card (states M)" by auto moreover have "set (visited_states q p) ⊆ states M" by (metis assms(1) path_prefix path_target_is_state subsetI visited_states_prefix) ultimately have "¬ distinct (visited_states q p)" using distinct_card[OF assms(2)] using List.finite_set[of "visited_states q p"] by (metis card_mono fsm_states_finite leD) then show "False" using assms(2) by blast qed subsection ‹Reachable States› definition reachable :: "('a,'b,'c) fsm ⇒ 'a ⇒ bool" where "reachable M q = (∃ p . path M (initial M) p ∧ target (initial M) p = q)" definition reachable_states :: "('a,'b,'c) fsm ⇒ 'a set" where "reachable_states M = {target (initial M) p | p . path M (initial M) p }" abbreviation "size_r M ≡ card (reachable_states M)" lemma acyclic_paths_set : "acyclic_paths_up_to_length M q (size M - 1) = {p . path M q p ∧ distinct (visited_states q p)}" unfolding acyclic_paths_up_to_length.simps using acyclic_path_length_limit[of M q] by (metis (no_types, lifting) One_nat_def Suc_pred cyclic_path_shortening leD list.size(3) not_less_eq_eq not_less_zero path.intros(1) path_begin_state) (* inefficient calculation, as a state may be target of a large number of acyclic paths *) lemma reachable_states_code[code] : "reachable_states M = image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))" proof - have "⋀ q' . q' ∈ reachable_states M ⟹ q' ∈ image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))" proof - fix q' assume "q' ∈ reachable_states M" then obtain p where "path M (initial M) p" and "target (initial M) p = q'" unfolding reachable_states_def by blast obtain p' where "path M (initial M) p'" and "target (initial M) p' = q'" and "distinct (visited_states (initial M) p')" proof (cases "distinct (visited_states (initial M) p)") case True then show ?thesis using ‹path M (initial M) p› ‹target (initial M) p = q'› that by auto next case False then show ?thesis using acyclic_path_from_cyclic_path[OF ‹path M (initial M) p›] unfolding ‹target (initial M) p = q'› using that by blast qed then show "q' ∈ image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_set by force qed moreover have "⋀ q' . q' ∈ image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1)) ⟹ q' ∈ reachable_states M" unfolding reachable_states_def acyclic_paths_set by blast ultimately show ?thesis by blast qed lemma reachable_states_intro[intro!] : assumes "path M (initial M) p" shows "target (initial M) p ∈ reachable_states M" using assms unfolding reachable_states_def by auto lemma reachable_states_initial : "initial M ∈ reachable_states M" unfolding reachable_states_def by auto lemma reachable_states_next : assumes "q ∈ reachable_states M" and "t ∈ transitions M" and "t_source t = q" shows "t_target t ∈ reachable_states M" proof - from ‹q ∈ reachable_states M› obtain p where * :"path M (initial M) p" and **:"target (initial M) p = q" unfolding reachable_states_def by auto then have "path M (initial M) (p@[t])" using assms(2,3) path_append_transition by metis moreover have "target (initial M) (p@[t]) = t_target t" by auto ultimately show ?thesis unfolding reachable_states_def by (metis (mono_tags, lifting) mem_Collect_eq) qed lemma reachable_states_path : assumes "q ∈ reachable_states M" and "path M q p" and "t ∈ set p" shows "t_source t ∈ reachable_states M" using assms unfolding reachable_states_def proof (induction p arbitrary: q) case Nil then show ?case by auto next case (Cons t' p') then show ?case proof (cases "t = t'") case True then show ?thesis using Cons.prems(1,2) by force next case False then show ?thesis using Cons by (metis (mono_tags, lifting) path_cons_elim reachable_states_def reachable_states_next set_ConsD) qed qed lemma reachable_states_initial_or_target : assumes "q ∈ reachable_states M" shows "q = initial M ∨ (∃ t ∈ transitions M . t_source t ∈ reachable_states M ∧ t_target t = q)" proof - obtain p where "path M (initial M) p" and "target (initial M) p = q" using assms unfolding reachable_states_def by auto show ?thesis proof (cases p rule: rev_cases) case Nil then show ?thesis using ‹path M (initial M) p› ‹target (initial M) p = q› by auto next case (snoc p' t) have "t ∈ transitions M" using ‹path M (initial M) p› unfolding snoc by auto moreover have "t_target t = q" using ‹target (initial M) p = q› unfolding snoc by auto moreover have "t_source t ∈ reachable_states M" using ‹path M (initial M) p› unfolding snoc by (metis append_is_Nil_conv last_in_set last_snoc not_Cons_self2 reachable_states_initial reachable_states_path) ultimately show ?thesis by blast qed qed lemma reachable_state_is_state : "q ∈ reachable_states M ⟹ q ∈ states M" unfolding reachable_states_def using path_target_is_state by fastforce lemma reachable_states_finite : "finite (reachable_states M)" using fsm_states_finite[of M] reachable_state_is_state[of _ M] by (meson finite_subset subset_eq) subsection ‹Language› abbreviation "p_io (p :: ('state,'input,'output) path) ≡ map (λ t . (t_input t, t_output t)) p" fun language_state_for_input :: "('state,'input,'output) fsm ⇒ 'state ⇒ 'input list ⇒ ('input × 'output) list set" where "language_state_for_input M q xs = {p_io p | p . path M q p ∧ map fst (p_io p) = xs}" fun LS⇩_{i}⇩_{n}:: "('state,'input,'output) fsm ⇒ 'state ⇒ 'input list set ⇒ ('input × 'output) list set" where "LS⇩_{i}⇩_{n}M q xss = {p_io p | p . path M q p ∧ map fst (p_io p) ∈ xss}" abbreviation(input) "L⇩_{i}⇩_{n}M ≡ LS⇩_{i}⇩_{n}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 ∈ LS⇩_{i}⇩_{n}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 @ [i