# Theory FSM

```section ‹Finite State Machines›

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

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

subsection ‹Well-formed Finite State Machines›

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

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

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

setup_lifting type_definition_fsm

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

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

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

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

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

subsubsection ‹Example FSMs›

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

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

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

subsection ‹Transition Function h and related functions›

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

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

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

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

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

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

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

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

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

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

have "(q, t_input t, t_output t, t_target t) ∈ transitions M"
using ‹t_source t = q› ‹t ∈ transitions M› by auto
then have "(q, t_input t, t_output t, t_target t) ∈ (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)"
using ‹(t_output t, t_target t) ∈ h M (q,t_input t)›
unfolding h.simps
by (metis (no_types, lifting) image_iff prod.case_eq_if surjective_pairing)
then have "t ∈ (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)"
using ‹t_source t = q› by (metis prod.collapse)
then show "t ∈ transitions_from M q"

unfolding transitions_from.simps transitions_from'.simps
using ‹t_input t ∈ defined_inputs' (h M) (inputs M) q›
using ‹t_input t ∈ FSM.inputs M› by blast
qed
ultimately show ?thesis by blast
qed

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

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

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

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

let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs ⇒ yqs | None ⇒ {}))"

have "⋀ qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M))) qx of Some yqs ⇒ yqs | None ⇒ {})) qx = (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx"
unfolding set_as_map_def by auto

moreover have "⋀ qx . (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` (transitions M)}) qx = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ (transitions M)}) qx"
by force

ultimately have "?f = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ (transitions M)})"
by blast
then have "?f = (λ (q,x) . {y | y . ∃ q' . (q, x, y, q') ∈ (transitions M)})" by force

then show ?thesis by force
qed

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

subsection ‹Size›

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

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

instance ..
end

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

subsection ‹Paths›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma path_source_target_index :
assumes "Suc i < length p"
and     "path M q p"
shows "t_target (p ! i) = t_source (p ! (Suc i))"
using assms proof (induction p rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc t ps)
then have "path M q ps" and "t_source t = target q ps" and "t ∈ transitions M" by auto

show ?case proof (cases "Suc i < length ps")
case True
then have "t_target (ps ! i) = t_source (ps ! Suc i)"
using snoc.IH ‹path M q ps› by auto
then show ?thesis
by (simp add: Suc_lessD True nth_append)
next
case False
then have "Suc i = length ps"
using snoc.prems(1) by auto
then have "(ps @ [t]) ! Suc i = t"
by auto

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

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

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

lemma visited_states_are_states :
assumes "path M q1 p"
shows "set (visited_states q1 p) ⊆ states M"
by (metis assms path_prefix path_target_is_state subsetI visited_states_prefix)

lemma transition_subset_path :
assumes "transitions A ⊆ transitions B"
and "path A q p"
and "q ∈ states B"
shows "path B q p"
using assms(2) proof (induction p rule: rev_induct)
case Nil
show ?case using assms(3) by auto
next
case (snoc t p)
then show ?case using assms(1) path_suffix
by fastforce
qed

subsubsection ‹Paths of fixed length›

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

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

subsubsection ‹Paths up to fixed length›

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

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

lemma paths_up_to_length'_set :
assumes "q ∈ states M"
and     "path M q prev"
shows "paths_up_to_length' prev (target q prev) (h M) (inputs M) k
= {(prev@p) | p . path M (target q prev) p ∧ length p ≤ k}"
using assms(2) proof (induction k arbitrary: prev)
case 0
show ?case unfolding paths_up_to_length'.simps using path_target_is_state[OF "0.prems"(1)] by auto
next
case (Suc k)

have "⋀ p . p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)
⟹ p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k}"
proof -
fix p assume "p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)"
then show "p ∈ {(prev@p) | p . path M (target q prev) p ∧ length p ≤ Suc k}"
proof (cases "p = prev")
case True
show ?thesis using path_target_is_state[OF Suc.prems(1)] unfolding True by (simp add: nil)
next
case False
then have "p ∈ (⋃ (image (λt. paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k)
(transitions_from' (h M) (inputs M) (target q prev))))"
using ‹p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)›
unfolding paths_up_to_length'.simps Let_def by blast
then obtain t where "t ∈ ⋃(image (λx . image (λ(y,q') . ((target q prev),x,y,q'))
(h M ((target q prev),x))) (inputs M))"
and   "p ∈ paths_up_to_length' (prev@[t]) (t_target t) (h M) (inputs M) k"
unfolding transitions_from'.simps by blast

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

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

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

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

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

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

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

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

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

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

ultimately show ?case by blast
qed

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

subsubsection ‹Calculating Acyclic Paths›

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

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

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

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

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

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

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

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

have "q' ∉ set (visited_states (p_source q prev) prev)"
using ‹q' ∉ visitedStates› Suc.prems(4) by auto
then have p2: "distinct (visited_states (p_source (p_source q prev) (prev@[?t])) (prev@[?t]))"
using Suc.prems(3) by auto

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

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

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

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

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

then have "t_source t = target (p_source q (prev)) (prev)" and "t ∈ transitions M"
using ‹path M (p_source q prev) (prev@p)› by auto

have "path M (p_source q (prev@[t])) ((prev@[t])@p')"
and  "path M (p_source q (prev@[t])) ((prev@[t]))"
using Cons ‹path M (p_source q prev) (prev@p)› by auto
have "length p' ≤ k"
using Cons ‹length p ≤ Suc k› by auto
have "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])@p'))"
and  "distinct (visited_states (p_source q (prev@[t])) ((prev@[t])))"
using Cons ‹distinct (visited_states (p_source q prev) (prev@p))› by auto
then have "t_target t ∉ visitedStates"
using Suc.prems(4) by auto

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

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

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

then have "(prev@[t])@p' ∈ acyclic_paths_up_to_length' (prev@[t]) (t_target t) hF ?vN k"
by auto
moreover have "(t_input t,t_output t, t_target t) ∈ Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF (t_source t))"
using Suc.prems(2)[of "t_source t"] ‹t ∈ transitions M› ‹t_target t ∉ visitedStates›
proof -
have "∃b c a. snd t = (b, c, a) ∧ (t_source t, b, c, a) ∈ FSM.transitions M"
by (metis (no_types) ‹t ∈ FSM.transitions M› prod.collapse)
then show ?thesis
using ‹hF (t_source t) = {(x, y, q'') |x y q''. (t_source t, x, y, q'') ∈ FSM.transitions M}›
‹t_target t ∉ visitedStates›
by fastforce
qed
ultimately have "∃ (x,y,q') ∈ (Set.filter (λ (x,y,q') . q' ∉ visitedStates) (hF (target (p_source q prev) prev))) .
(prev@[t])@p' ∈ (acyclic_paths_up_to_length' (prev@[((target (p_source q prev) prev),x,y,q')]) q' hF (insert q' visitedStates) k)"
unfolding ‹t_source t = target (p_source q (prev)) (prev)›
by (metis (no_types, lifting) ‹t_source t = target (p_source q prev) prev› case_prodI prod.collapse)

then show ?thesis unfolding ‹prev@p = prev@[t]@p'›
unfolding acyclic_paths_up_to_length'.simps Let_def by force
qed
qed
then have rev: "⋀ p' . p' ∈ {prev@p | p . path M (p_source q prev) (prev@p)
∧ length p ≤ Suc k
∧ distinct (visited_states (p_source q prev) (prev@p))}
⟹ p' ∈ acyclic_paths_up_to_length' prev (target (p_source q prev) prev) hF visitedStates (Suc k)"
by blast

show ?case
using fwd rev by blast
qed

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

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

show ?thesis
using acyclic_paths_up_to_length'_set[OF * ** *** ****, of k ]
using True by auto
qed

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

lemma path_length_sum :
assumes "path M q p"
shows "length p = (∑ q ∈ states M . length (filter (λt. t_target t = q) p))"
using assms
proof (induction p rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
then have "length xs = (∑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```