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 thenshow ?thesis by blast qed
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
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 moreoverhave"∧ 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" thenhave"(t_output t, t_target t) ∈ h M (q,t_input t)"and"t_input t ∈ inputs M"by auto thenhave"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 thenhave"(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) thenhave"t ∈ (λ(y, q'). (q, t_input t, y, q')) ` h M (q, t_input t)" using‹t_source t = q›by (metis prod.collapse) thenshow"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 ultimatelyshow ?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
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 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 thenshow ?caseby auto next case (snoc t ps) thenhave"path M q ps"and"t_source t = target q ps"and"t ∈ transitions M"by auto
show ?caseproof (cases "Suc i < length ps") case True thenhave"t_target (ps ! i) = t_source (ps ! Suc i)" using snoc.IH ‹path M q ps›by auto thenshow ?thesis by (simp add: Suc_lessD True nth_append) next case False thenhave"Suc i = length ps" using snoc.prems(1) by auto thenhave"(ps @ [t]) ! Suc i = t" by auto
show ?thesis proof (cases "ps = []") case True thenshow ?thesis using‹Suc i = length ps›by auto next case False thenhave"target q ps = t_target (last ps)" unfolding target.simps visited_states.simps by (simp add: last_map) thenhave"target q ps = t_target (ps ! i)" using‹Suc i = length ps› by (metis False diff_Suc_1 last_conv_nth) thenshow ?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) thenshow"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 thenshow ?caseby auto next case (Cons a p) thenshow ?case proof (cases "q' ∈ set (visited_states (t_target a) p)") case True thenobtain p1 p2 where"p = p1 @ p2 ∧ target (t_target a) p1 = q'" using Cons.IH by blast thenhave"(a#p) = (a#p1)@p2 ∧ target q (a#p1) = q'" by auto thenshow ?thesis by blast next case False thenhave"q' = q" using Cons.prems by auto thenshow ?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 ?caseusing assms(3) by auto next case (snoc t p) thenshow ?caseusing 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) case0 show ?caseunfolding 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)" thenshow"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 thenhave"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 thenobtain 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 thenhave"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
moreoverhave"∧ 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}" thenobtain 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 thenshow ?thesis by auto next case (Cons t p'')
thenhave"t ∈ transitions M"and"t_source t = (target q prev)" using‹path M (target q prev) p'›by auto thenhave"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 moreoverhave"path M (target q (prev@[t])) p''" using‹path M (target q prev) p'›unfolding Cons by auto ultimatelyhave"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 thenhave"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) thenhave"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
thenshow ?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 thenshow"p ∈ paths_up_to_length' prev (target q prev) (h M) (inputs M) (Suc k)" unfolding‹p = prev@p'›by assumption qed
ultimatelyshow ?caseby 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
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) case0 thenshow ?caseby 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 thenshow"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 thenshow ?thesis using Suc.prems(1,3) by auto next case b thenobtain 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+ moreoverhave"t_source ?t = target (p_source q prev) prev" by simp moreoverhave"p_source (p_source q prev) (prev@[?t]) = p_source q prev" by auto ultimatelyhave 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 thenhave 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))}" thenhave"∃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 thenshow ?thesis by (metis (no_types) Suc_le_mono append.assoc append.right_neutral append_Cons length_Cons same_append_eq) qed qed qed moreoverhave"∧ 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 ultimatelyhave 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 thenshow ?thesis by auto next case (Cons t p')
thenhave"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 thenhave"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
thenhave"(prev@[t])@p' ∈ acyclic_paths_up_to_length' (prev@[t]) (t_target t) hF ?vN k" by auto moreoverhave"(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) thenshow ?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 ultimatelyhave"∃ (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)
thenshow ?thesis unfolding‹prev@p = prev@[t]@p'› unfolding acyclic_paths_up_to_length'.simps Let_def by force qed qed thenhave 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 thenhave"acyclic_paths_up_to_length M q k = {}" using path_begin_state by fastforce thenshow ?thesis using False by auto next case True thenhave *: "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_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 thenshow ?caseby auto next case (snoc x xs) thenhave"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 thenhave **: "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 thenhave ***: "(∑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) thenshow ?thesis by (simp add: ‹finite (states M)› sum.insert_remove) qed moreoverhave"(∑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) thenshow ?thesis by (simp add: ‹finite (states M)› sum.insert_remove) qed
ultimatelyhave"(∑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
thenshow ?case by (simp add: ‹length xs = (∑q∈states M. length (filter (λt. t_target t = q) xs))›) 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 thenhave"path M q ((take i p)@(drop i p))"using assms by auto thenshow ?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) thenshow ?caseby auto next case (cons t M ts) thenshow ?case proof (cases "distinct (visited_states (t_target t) ts)") case True thenhave"q ∈ set (visited_states (t_target t) ts)" using cons.prems by simp thenobtain 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 thenhave"(t#ts) = []@(t#p2)@p3 ∧ (t#p2) ≠ [] ∧ target q [] = target q ([]@(t#p2))" using cons.hyps by auto thenshow ?thesis by blast next case False thenobtain 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 thenhave"t#ts = (t#p1)@p2@p3 ∧ p2 ≠ [] ∧ target q (t#p1) = target q ((t#p1)@p2)" by simp thenshow ?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 thenhave"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) case0 thenshow ?case using path_append[OF ‹path M (initial M) p1›‹path M (target (initial M) p1) p3›] by auto next case (Suc n) thenshow ?case using‹path M (target (initial M) p1) p2›‹target (target (initial M) p1) p2 = target (initial M) p1› by auto qed moreoverhave"length (p1 @ (concat (replicate n p2)) @ p3) ≥ n" proof - have"length (concat (replicate n p2)) = n * (length p2)" using concat_replicate_length by metis moreoverhave"length p2 > 0" using‹p2 ≠ []›by auto ultimatelyhave"length (concat (replicate n p2)) ≥ n" by (simp add: Suc_leI) thenshow ?thesis by auto qed ultimatelyshow"∃ 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 thenhave"path M q (p1@p3)" using assms(1) by force moreoverhave"target q (p1@p3) = target q p" by (metis (full_types) * path_append_target) moreoverhave"length (p1@p3) < length p" using * by auto ultimatelyshow ?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 moreoverhave"finite ?paths" using paths_finite[of M q "length p"] by (metis (no_types, lifting) Collect_mono rev_finite_subset) ultimatelyhave minPath_def : "?minPath ∈ ?paths ∧ (∀ p' ∈ ?paths . length ?minPath ≤ length p')" by (meson arg_min_nat_lemma equals0I) thenhave"path M q ?minPath"and"target q ?minPath = target q p" by auto
moreoverhave"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 thenshow"False" using minPath_def using arg_min_nat_le dual_order.strict_trans1 by auto qed
ultimatelyshow ?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" thenhave"length p ≥ card (states M)" using size_def by auto thenhave"length (visited_states q p) > card (states M)" by auto moreoverhave"set (visited_states q p) ⊆ states M" by (metis assms(1) path_prefix path_target_is_state subsetI visited_states_prefix) ultimatelyhave"¬ 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) thenshow"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" thenobtain 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 thenshow ?thesis using‹path M (initial M) p›‹target (initial M) p = q'› that by auto next case False thenshow ?thesis using acyclic_path_from_cyclic_path[OF ‹path M (initial M) p›] unfolding‹target (initial M) p = q'›using that by blast qed thenshow"q' ∈ image (target (initial M)) (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_set by force qed moreoverhave"∧ 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 ultimatelyshow ?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
thenhave"path M (initial M) (p@[t])"using assms(2,3) path_append_transition by metis moreoverhave"target (initial M) (p@[t]) = t_target t"by auto ultimatelyshow ?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 thenshow ?caseby auto next case (Cons t' p') thenshow ?caseproof (cases "t = t'") case True thenshow ?thesis using Cons.prems(1,2) by force next case False thenshow ?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 thenshow ?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 moreoverhave"t_target t = q" using‹target (initial M) p = q›unfolding snoc by auto moreoverhave"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)
ultimatelyshow ?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)
fun language_state_for_input :: "('state,'input,'output) fsm ==> 'state ==> 'input list ==> ('input × 'output) list set"where "language_state_for_input M q xs = {p_io p | p . path M q p ∧ map fst (p_io p) = xs}"
fun LSin :: "('state,'input,'output) fsm ==> 'state ==> 'input list set ==> ('input× 'output) list set"where "LSin M q xss = {p_io p | p . path M q p ∧ map fst (p_io p) ∈ xss}"
abbreviation(input) "Lin M ≡ LSin M (initial M)"
lemma language_state_for_input_inputs : assumes"io ∈ language_state_for_input M q xs" shows"map fst io = xs" using assms by auto
lemma language_state_for_inputs_inputs : assumes"io ∈ LSin M q xss" shows"map fst io ∈ xss"using assms by auto
fun LS :: "('state,'input,'output) fsm ==> 'state ==> ('input × 'output) list set"where "LS M q = { p_io p | p . path M q p }"
abbreviation"L M ≡ LS M (initial M)"
lemma language_state_containment : assumes"path M q p" and"p_io p = io" shows"io ∈ LS M q" using assms by auto
lemma language_prefix : assumes"io1@io2 ∈ LS M q" shows"io1 ∈ LS M q" proof - obtain p where"path M q p"and"p_io p = io1@io2" using assms by auto let ?tp = "take (length io1) p" have"path M q ?tp" by (metis (no_types) ‹path M q p› append_take_drop_id path_prefix) moreoverhave"p_io ?tp = io1" using‹p_io p = io1@io2›by (metis append_eq_conv_conj take_map) ultimatelyshow ?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 thenhave"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+ moreoverhave"p_io ?p1 = io1" using‹p12 = ?p1 @ ?p2›‹p_io p12 = io1 @ io2› by (metis append_eq_conv_conj take_map) moreoverhave"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) ultimatelyshow ?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 thenhave"pt ≠ []" by auto thenobtain p t where"pt = p @ [t]" using rev_exhaust by blast thenhave"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 thenshow ?thesis using that by simp qed
lemma language_path_append_transition : assumes"ios @ [io] ∈ LS M q" obtains p t where"path M q (p@[t])"and"p_io (p@[t]) = ios @ [io]" proof - obtain pt where"path M q pt"and"p_io pt = ios @ [io]" using assms unfolding LS.simps by auto thenhave"pt ≠ []" by auto thenobtain p t where"pt = p @ [t]" using rev_exhaust by blast thenhave"path M q (p@[t])"and"p_io (p@[t]) = ios @ [io]" using‹path M q pt›‹p_io pt = ios @ [io]›by auto thenshow ?thesis using that by simp qed
lemma language_split : assumes"io1@io2 ∈ L M" obtains p1 p2 where"path M (initial M) (p1@p2)"and"p_io p1 = io1"and"p_io p2 = io2" proof - from assms obtain p where"path M (initial M) p"and"p_io p = io1 @ io2" by auto
let ?p1 = "take (length io1) p" let ?p2 = "drop (length io1) p"
have"path M (initial M) (?p1@?p2)" using‹path M (initial M) p›by simp moreoverhave"p_io ?p1 = io1" using‹p_io p = io1 @ io2› by (metis append_eq_conv_conj take_map) moreoverhave"p_io ?p2 = io2" using‹p_io p = io1 @ io2› by (metis append_eq_conv_conj drop_map) ultimatelyshow ?thesis using that by blast qed
lemma language_io : assumes"io ∈ LS M q" and"(x,y) ∈ set io" shows"x ∈ (inputs M)" and"y ∈ outputs M" proof - obtain p where"path M q p"and"p_io p = io" using‹io ∈ LS M q›by auto thenobtain t where"t ∈ set p"and"t_input t = x"and"t_output t = y" using‹(x,y) ∈ set io›by auto
have"t ∈ transitions M" using‹path M q p›‹t ∈ set p› by (induction p; auto)
show"x ∈ (inputs M)" using‹t ∈ transitions M›‹t_input t = x›by auto
show"y ∈ outputs M" using‹t ∈ transitions M›‹t_output t = y›by auto qed
lemma path_io_split : assumes"path M q p" and"p_io p = io1@io2" shows"path M q (take (length io1) p)" and"p_io (take (length io1) p) = io1" and"path M (target q (take (length io1) p)) (drop (length io1) p)" and"p_io (drop (length io1) p) = io2" proof - have"length io1 ≤ length p" using‹p_io p = io1@io2› unfolding length_map[of "(λ t . (t_input t, t_output t))", symmetric] by auto
have"p = (take (length io1) p)@(drop (length io1) p)" by simp thenhave *: "path M q ((take (length io1) p)@(drop (length io1) p))" using‹path M q p›by auto
show"path M q (take (length io1) p)" and"path M (target q (take (length io1) p)) (drop (length io1) p)" using path_append_elim[OF *] by blast+
show"p_io (drop (length io1) p) = io2" using‹p = (take (length io1) p)@(drop (length io1) p)›‹p_io p = io1@io2› by (metis append_eq_conv_conj drop_map) qed
lemma language_intro : assumes"path M q p" shows"p_io p ∈ LS M q" using assms unfolding LS.simps by auto
lemma language_prefix_append : assumes"io1 @ (p_io p) ∈ L M" shows"io1 @ p_io (take i p) ∈ L M" proof - fix i have"p_io p = (p_io (take i p)) @ (p_io (drop i p))" by (metis append_take_drop_id map_append) thenhave"(io1 @ (p_io (take i p))) @ (p_io (drop i p)) ∈ L M" using‹io1 @ p_io p ∈ L M›by auto show"io1 @ p_io (take i p) ∈ L M" using language_prefix[OF ‹(io1 @ (p_io (take i p))) @ (p_io (drop i p)) ∈ L M›] by assumption qed
lemma language_finite: "finite {io . io ∈ L M ∧ length io ≤ k}" proof - have"{io . io ∈ L M ∧ length io ≤ k} ⊆ p_io ` {p. path M (FSM.initial M) p ∧ length p ≤ k}" by auto thenshow ?thesis using paths_finite[of M "initial M" k] using finite_surj by auto qed
lemma LS_prepend_transition : assumes"t ∈ transitions M" and"io ∈ LS M (t_target t)" shows"(t_input t, t_output t) # io ∈ LS M (t_source t)" proof - obtain p where"path M (t_target t) p"and"p_io p = io" using assms(2) by auto thenhave"path M (t_source t) (t#p)"and"p_io (t#p) = (t_input t, t_output t) # io" using assms(1) by auto thenshow ?thesis unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) qed
lemma language_empty_IO : assumes"inputs M = {} ∨ outputs M = {}" shows"L M = {[]}" proof -
consider "inputs M = {}" | "outputs M = {}"using assms by blast thenshow ?thesis proof cases case1
show"L M = {[]}" using language_io(1)[of _ M "initial M"] unfolding1 by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair) next case2 show"L M = {[]}" using language_io(2)[of _ M "initial M"] unfolding2 by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair) qed qed
lemma language_equivalence_from_isomorphism_helper : assumes"bij_betw f (states M1) (states M2)" and"f (initial M1) = initial M2" and"∧ q x y q' . q ∈ states M1 ==> q' ∈ states M1 ==> (q,x,y,q') ∈ transitions M1 ⟷ (f q,x,y,f q') ∈ transitions M2" and"q ∈ states M1" shows"LS M1 q ⊆ LS M2 (f q)" proof fix io assume"io ∈ LS M1 q"
thenobtain p where"path M1 q p"and"p_io p = io" by auto
let ?f = "λ(q,x,y,q') . (f q,x,y,f q')" let ?p = "map ?f p"
have"f q ∈ states M2" using assms(1,4) using bij_betwE by auto
have"path M2 (f q) ?p" using‹path M1 q p›proof (induction p rule: rev_induct) case Nil show ?caseusing‹f q ∈ states M2›by auto next case (snoc a p) thenhave"path M2 (f q) (map ?f p)" by auto
have"target (f q) (map ?f p) = f (target q p)" using‹f (initial M1) = initial M2› assms(2) by (induction p; auto) thenhave"t_source (?f a) = target (f q) (map ?f p)" by (metis (no_types, lifting) case_prod_beta' fst_conv path_append_transition_elim(3) snoc.prems)
have"a ∈ transitions M1" using snoc.prems by auto thenhave"?f a ∈ transitions M2" by (metis (mono_tags, lifting) assms(3) case_prod_beta fsm_transition_source fsm_transition_target surjective_pairing)
have"map ?f (p@[a]) = (map ?f p)@[?f a]" by auto
show ?case unfolding‹map ?f (p@[a]) = (map ?f p)@[?f a]› using path_append_transition[OF ‹path M2 (f q) (map ?f p)›‹?f a ∈ transitions M2›‹t_source (?f a) = target (f q) (map ?f p)›] by assumption qed moreoverhave"p_io ?p = io" using‹p_io p = io› by (induction p; auto) ultimatelyshow"io ∈ LS M2 (f q)" using language_state_containment by fastforce qed
lemma language_equivalence_from_isomorphism : assumes"bij_betw f (states M1) (states M2)" and"f (initial M1) = initial M2" and"∧ q x y q' . q ∈ states M1 ==> q' ∈ states M1 ==> (q,x,y,q') ∈ transitions M1 ⟷ (f q,x,y,f q') ∈ transitions M2" and"q ∈ states M1" shows"LS M1 q = LS M2 (f q)" proof show"LS M1 q ⊆ LS M2 (f q)" using language_equivalence_from_isomorphism_helper[OF assms] .
have"f q ∈ states M2" using assms(1,4) using bij_betwE by auto have"(inv_into (FSM.states M1) f (f q)) = q" by (meson assms(1) assms(4) bij_betw_imp_inj_on inv_into_f_f)
have"bij_betw (inv_into (states M1) f) (states M2) (states M1)" using bij_betw_inv_into[OF assms(1)] . moreoverhave"(inv_into (states M1) f) (initial M2) = (initial M1)" using assms(1,2) by (metis bij_betw_inv_into_left fsm_initial) moreoverhave"∧ q x y q' . q ∈ states M2 ==> q' ∈ states M2 ==> (q,x,y,q') ∈ transitions M2 ⟷ ((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q') ∈ transitions M1" proof fix q x y q' assume"q ∈ states M2"and"q' ∈ states M2"
show"(q,x,y,q') ∈ transitions M2 ==> ((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q') ∈ transitions M1" proof - assume a1: "(q, x, y, q') ∈ FSM.transitions M2" have f2: "∀f B A. ¬ bij_betw f B A ∨ (∀b. (b::'b) ∉ B ∨ (f b::'a) ∈ A)" using bij_betwE by blast thenhave f3: "inv_into (states M1) f q ∈ states M1" using‹q ∈ states M2› calculation(1) by blast have"inv_into (states M1) f q' ∈ states M1" using f2 ‹q' ∈ states M2› calculation(1) by blast thenshow ?thesis using f3 a1 ‹q ∈ states M2›‹q' ∈ states M2› assms(1) assms(3) bij_betw_inv_into_right by fastforce qed
show"((inv_into (states M1) f) q,x,y,(inv_into (states M1) f) q') ∈ transitions M1 ==> (q,x,y,q') ∈ transitions M2" proof - assume a1: "(inv_into (states M1) f q, x, y, inv_into (states M1) f q') ∈ FSM.transitions M1" have f2: "∀f B A. ¬ bij_betw f B A ∨ (∀b. (b::'b) ∉ B ∨ (f b::'a) ∈ A)" by (metis (full_types) bij_betwE) thenhave f3: "inv_into (states M1) f q' ∈ states M1" using‹q' ∈ states M2› calculation(1) by blast have"inv_into (states M1) f q ∈ states M1" using f2 ‹q ∈ states M2› calculation(1) by blast thenshow ?thesis using f3 a1 ‹q ∈ states M2›‹q' ∈ states M2› assms(1) assms(3) bij_betw_inv_into_right by fastforce qed qed ultimatelyshow"LS M2 (f q) ⊆ LS M1 q" using language_equivalence_from_isomorphism_helper[of "(inv_into (states M1) f)" M2 M1, OF _ _ _ ‹f q ∈ states M2›] unfolding‹(inv_into (FSM.states M1) f (f q)) = q› by blast qed
thenobtain p where"path M1 (initial M1) p"and"p_io p = io" by auto
let ?f = "λ(q,x,y,q') . (f q,x,y,f q')" let ?p = "map ?f p"
have"path M2 (initial M2) ?p" using‹path M1 (initial M1) p›proof (induction p rule: rev_induct) case Nil thenshow ?caseby auto next case (snoc a p) thenhave"path M2 (initial M2) (map ?f p)" by auto
have"t_source a ∈ reachable_states M1" using‹path M1 (FSM.initial M1) (p @ [a])› by (metis path_append_transition_elim(3) path_prefix reachable_states_intro) have"t_target a ∈ reachable_states M1" using‹path M1 (FSM.initial M1) (p @ [a])› by (meson ‹t_source a ∈ reachable_states M1› path_append_transition_elim(2) reachable_states_next)
have"a ∈ transitions M1" using snoc.prems by auto thenhave"?f a ∈ transitions M2" using assms(3)[OF ‹t_source a ∈ reachable_states M1›‹t_target a ∈ reachable_states M1›] by (metis (mono_tags, lifting) prod.case_eq_if prod.collapse)
have"map ?f (p@[a]) = (map ?f p)@[?f a]" by auto
show ?case unfolding‹map ?f (p@[a]) = (map ?f p)@[?f a]› using path_append_transition[OF ‹path M2 (initial M2) (map ?f p)›‹?f a ∈ transitions M2›‹t_source (?f a) = target (initial M2) (map ?f p)›] by assumption qed moreoverhave"p_io ?p = io" using‹p_io p = io› by (induction p; auto) ultimatelyshow"io ∈ L M2" using language_state_containment by fastforce qed
lemma language_equivalence_from_isomorphism_reachable : assumes"bij_betw f (reachable_states M1) (reachable_states M2)" and"f (initial M1) = initial M2" and"∧ q x y q' . q ∈ reachable_states M1 ==> q' ∈ reachable_states M1 ==> (q,x,y,q') ∈ transitions M1 ⟷ (f q,x,y,f q') ∈ transitions M2" shows"L M1 = L M2" proof show"L M1 ⊆ L M2" using language_equivalence_from_isomorphism_helper_reachable[OF assms] .
show"(q,x,y,q') ∈ transitions M2 ==> ((inv_into (reachable_states M1) f) q,x,y,(inv_into (reachable_states M1) f) q') ∈ transitions M1" proof - assume a1: "(q, x, y, q') ∈ FSM.transitions M2" have f2: "∀f B A. ¬ bij_betw f B A ∨ (∀b. (b::'b) ∉ B ∨ (f b::'a) ∈ A)" using bij_betwE by blast thenhave f3: "inv_into (FSM.reachable_states M1) f q ∈ FSM.reachable_states M1" using‹q ∈ FSM.reachable_states M2› calculation(1) by blast have"inv_into (FSM.reachable_states M1) f q' ∈ FSM.reachable_states M1" using f2 ‹q' ∈ FSM.reachable_states M2› calculation(1) by blast thenshow ?thesis using f3 a1 ‹q ∈ FSM.reachable_states M2›‹q' ∈ FSM.reachable_states M2› assms(1) assms(3) bij_betw_inv_into_right by fastforce qed
show"((inv_into (reachable_states M1) f) q,x,y,(inv_into (reachable_states M1) f) q') ∈ transitions M1 ==> (q,x,y,q') ∈ transitions M2" proof - assume a1: "(inv_into (FSM.reachable_states M1) f q, x, y, inv_into (FSM.reachable_states M1) f q') ∈ FSM.transitions M1" have f2: "∀f B A. ¬ bij_betw f B A ∨ (∀b. (b::'b) ∉ B ∨ (f b::'a) ∈ A)" by (metis (full_types) bij_betwE) thenhave f3: "inv_into (FSM.reachable_states M1) f q' ∈ FSM.reachable_states M1" using‹q' ∈ FSM.reachable_states M2› calculation(1) by blast have"inv_into (FSM.reachable_states M1) f q ∈ FSM.reachable_states M1" using f2 ‹q ∈ FSM.reachable_states M2› calculation(1) by blast thenshow ?thesis using f3 a1 ‹q ∈ FSM.reachable_states M2›‹q' ∈ FSM.reachable_states M2› assms(1) assms(3) bij_betw_inv_into_right by fastforce qed qed ultimatelyshow"L M2 ⊆ L M1" using language_equivalence_from_isomorphism_helper_reachable[of "(inv_into (reachable_states M1) f)" M2 M1] by blast qed
lemma language_empty_io : assumes"inputs M = {} ∨ outputs M = {}" shows"L M = {[]}" proof - have"transitions M = {}" using assms fsm_transition_input fsm_transition_output by auto thenhave"∧ p . path M (initial M) p ==> p = []" by (metis empty_iff path.cases) thenshow ?thesis unfolding LS.simps by blast qed
subsection‹Basic FSM Properties›
subsubsection‹Completely Specified›
fun completely_specified :: "('a,'b,'c) fsm ==> bool"where "completely_specified M = (∀ q ∈ states M . ∀ x ∈ inputs M . ∃ t ∈ transitions M . t_source t = q ∧ t_input t = x)"
lemma completely_specified_alt_def : "completely_specified M = (∀ q ∈ states M . ∀ x ∈ inputs M . ∃ q' y . (q,x,y,q')∈ transitions M)" by force
lemma completely_specified_alt_def_h : "completely_specified M = (∀ q ∈ states M . ∀ x ∈ inputs M . h M (q,x) ≠ {})" by force
fun completely_specified_state :: "('a,'b,'c) fsm ==> 'a ==> bool"where "completely_specified_state M q = (∀ x ∈ inputs M . ∃ t ∈ transitions M . t_source t = q ∧ t_input t = x)"
lemma completely_specified_states : "completely_specified M = (∀ q ∈ states M . completely_specified_state M q)" unfolding completely_specified.simps completely_specified_state.simps by force
lemma completely_specified_state_alt_def_h : "completely_specified_state M q = (∀ x ∈ inputs M . h M (q,x) ≠ {})" by force
lemma completely_specified_path_extension : assumes"completely_specified M" and"q ∈ states M" and"path M q p" and"x ∈ (inputs M)" obtains t where"t ∈ transitions M"and"t_input t = x"and"t_source t = target q p" proof - have"target q p ∈ states M" using path_target_is_state ‹path M q p›by metis thenobtain t where"t ∈ transitions M"and"t_input t = x"and"t_source t = target q p" using‹completely_specified M›‹x ∈ (inputs M)› unfolding completely_specified.simps by blast thenshow ?thesis using that by blast qed
lemma completely_specified_language_extension : assumes"completely_specified M" and"q ∈ states M" and"io ∈ LS M q" and"x ∈ (inputs M)" obtains y where"io@[(x,y)] ∈ LS M q" proof - obtain p where"path M q p"and"p_io p = io" using‹io ∈ LS M q›by auto
moreoverobtain t where"t ∈ transitions M"and"t_input t = x"and"t_source t = target q p" using completely_specified_path_extension[OF assms(1,2) ‹path M q p› assms(4)] by blast
ultimatelyhave"path M q (p@[t])"and"p_io (p@[t]) = io@[(x,t_output t)]" by (simp add: path_append_transition)+
thenhave"io@[(x,t_output t)] ∈ LS M q" using language_state_containment[of M q "p@[t]""io@[(x,t_output t)]"] by auto thenshow ?thesis using that by blast qed
lemma path_of_length_ex : assumes"completely_specified M" and"q ∈ states M" and"inputs M ≠ {}" shows"∃ p . path M q p ∧ length p = k" using assms(2) proof (induction k arbitrary: q) case0 thenshow ?caseby auto next case (Suc k)
obtain t where"t_source t = q"and"t ∈ transitions M" by (meson Suc.prems assms(1) assms(3) completely_specified.simps equals0I) thenhave"t_target t ∈ states M" using fsm_transition_target by blast thenobtain p where"path M (t_target t) p ∧ length p = k" using Suc.IH by blast thenshow ?case using‹t_source t = q›‹t ∈ transitions M› by auto qed
lemma observable_alt_def : "observable M = (∀ q1 x y q1' q1'' . (q1,x,y,q1') ∈ transitions M ∧ (q1,x,y,q1'') ∈ transitions M ⟶ q1' = q1'')" by auto
lemma observable_alt_def_h : "observable M = (∀ q1 x yq yq' . (yq ∈ h M (q1,x) ∧ yq' ∈ h M (q1,x)) ⟶ fst yq = fst yq' ⟶ snd yq = snd yq')" by auto
lemma language_append_path_ob : assumes"io@[(x,y)] ∈ L M" obtains p t where"path M (initial M) (p@[t])"and"p_io p = io"and"t_input t = x"and"t_output t = y" proof - obtain p p2 where"path M (initial M) p"and"path M (target (initial M) p) p2"and"p_io p = io"and"p_io p2 = [(x,y)]" using language_state_split[OF assms] by blast
obtain t where"p2 = [t]"and"t_input t = x"and"t_output t = y" using‹p_io p2 = [(x,y)]›by auto
have"path M (initial M) (p@[t])" using‹path M (initial M) p›‹path M (target (initial M) p) p2›unfolding‹p2 = [t]›by auto thenshow ?thesis using that[OF _ ‹p_io p = io›‹t_input t = x›‹t_output t = y›] by simp qed
subsubsection‹Single Input›
(* each state has at most one input, but may have none *) fun single_input :: "('a,'b,'c) fsm ==> bool"where "single_input M = (∀ t1 ∈ transitions M . ∀ t2 ∈ transitions M . t_source t1 = t_source t2 ⟶ t_input t1 = t_input t2)"
lemma single_input_alt_def : "single_input M = (∀ q1 x x' y y' q1' q1'' . (q1,x,y,q1') ∈ transitions M ∧ (q1,x',y',q1'') ∈ transitions M ⟶ x = x')" by fastforce
lemma single_input_alt_def_h : "single_input M = (∀ q x x' . (h M (q,x) ≠ {} ∧ h M (q,x') ≠ {}) ⟶ x = x')" by force
subsubsection‹Output Complete›
fun output_complete :: "('a,'b,'c) fsm ==> bool"where "output_complete M = (∀ t ∈ transitions M . ∀ y ∈ outputs M . ∃ t' ∈ transitions M . t_source t = t_source t' ∧ t_input t = t_input t' ∧ t_output t' = y)"
lemma output_complete_alt_def : "output_complete M = (∀ q x . (∃ y q' . (q,x,y,q') ∈ transitions M) ⟶ (∀ y ∈ (outputs M) . ∃ q' . (q,x,y,q') ∈ transitions M))" by force
lemma output_complete_alt_def_h : "output_complete M = (∀ q x . h M (q,x) ≠ {} ⟶ (∀ y ∈ outputs M . ∃ q' . (y,q') ∈ h M (q,x)))" by force
subsubsection‹Acyclic›
fun acyclic :: "('a,'b,'c) fsm ==> bool"where "acyclic M = (∀ p . path M (initial M) p ⟶ distinct (visited_states (initial M) p))"
lemma visited_states_take : "(take (Suc n) (visited_states q p)) = (visited_states q (take n p))" proof (induction p rule: rev_induct) case Nil thenshow ?caseby auto next case (snoc x xs) thenshow ?caseby (cases "n ≤ length xs"; auto) qed
(* very inefficient calculation *) lemma acyclic_code[code] : "acyclic M = (¬(∃ p ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1)) . ∃ t ∈ transitions M . t_source t = target (initial M) p ∧ t_target t ∈ set (visited_states (initial M) p)))" proof - have"(∃ p ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1)) . ∃ t ∈ transitions M . t_source t = target (initial M) p ∧ t_target t ∈ set (visited_states (initial M) p)) ==>¬ FSM.acyclic M" proof - assume"(∃ p ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1)) . ∃ t ∈ transitions M . t_source t = target (initial M) p ∧ t_target t ∈ set (visited_states (initial M) p))" thenobtain p t where"path M (initial M) p" and"distinct (visited_states (initial M) p)" and"t ∈ transitions M" and"t_source t = target (initial M) p" and"t_target t ∈ set (visited_states (initial M) p)" unfolding acyclic_paths_set by blast thenhave"path M (initial M) (p@[t])" by (simp add: path_append_transition) moreoverhave"¬ (distinct (visited_states (initial M) (p@[t])))" using‹t_target t ∈ set (visited_states (initial M) p)›by auto ultimatelyshow"¬ FSM.acyclic M" by (meson acyclic.elims(2)) qed moreoverhave"¬ FSM.acyclic M ==> (∃ p ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1)) . ∃ t ∈ transitions M . t_source t = target (initial M) p ∧ t_target t ∈ set (visited_states (initial M) p))" proof - assume"¬ FSM.acyclic M" thenobtain p where"path M (initial M) p" and"¬ distinct (visited_states (initial M) p)" by auto thenobtain n where"distinct (take (Suc n) (visited_states (initial M) p))" and"¬ distinct (take (Suc (Suc n)) (visited_states (initial M) p))" using maximal_distinct_prefix by blast thenhave"distinct (visited_states (initial M) (take n p))" and"¬ distinct (visited_states (initial M)(take (Suc n) p))" unfolding visited_states_take by simp+
thenobtain p' t' where *: "take n p = p'" and **: "take (Suc n) p = p' @ [t']" by (metis Suc_less_eq ‹¬ distinct (visited_states (FSM.initial M) p)›
le_imp_less_Suc not_less_eq_eq take_all take_hd_drop)
have ***: "visited_states (FSM.initial M) (p' @ [t']) = (visited_states (FSM.initial M) p')@[t_target t']" by auto
have"path M (initial M) p'" using * ‹path M (initial M) p› by (metis append_take_drop_id path_prefix) thenhave"p' ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1))" using‹distinct (visited_states (initial M) (take n p))› unfolding * acyclic_paths_set by blast moreoverhave"t' ∈ transitions M ∧ t_source t' = target (initial M) p'" using * ** ‹path M (initial M) p› by (metis append_take_drop_id path_append_elim path_cons_elim)
moreoverhave"t_target t' ∈ set (visited_states (initial M) p')" using‹distinct (visited_states (initial M) (take n p))› ‹¬ distinct (visited_states (initial M)(take (Suc n) p))› unfolding * ** *** by auto ultimatelyshow"(∃ p ∈ (acyclic_paths_up_to_length M (initial M) (size M - 1)) . ∃ t ∈ transitions M . t_source t = target (initial M) p ∧ t_target t ∈ set (visited_states (initial M) p))" by blast qed ultimatelyshow ?thesis by blast qed
lemma acyclic_alt_def : "acyclic M = finite (L M)" proof show"acyclic M ==> finite (L M)" proof - assume"acyclic M" thenhave"{ p . path M (initial M) p} ⊆ (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_set by auto moreoverhave"finite (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_up_to_length.simps using paths_finite[of M "initial M""size M - 1"] by (metis (mono_tags, lifting) Collect_cong ‹FSM.acyclic M› acyclic.elims(2)) ultimatelyhave"finite { p . path M (initial M) p}" using finite_subset by blast thenshow"finite (L M)" unfolding LS.simps by auto qed
obtain max_io_len where"∀io ∈ L M . length io < max_io_len" using finite_maxlen[OF ‹finite (L M)›] by blast thenhave"∧ p . path M (initial M) p ==> length p < max_io_len" proof - fix p assume"path M (initial M) p" show"length p < max_io_len" proof (rule ccontr) assume"¬ length p < max_io_len" thenhave"¬ length (p_io p) < max_io_len"by auto moreoverhave"p_io p ∈ L M" unfolding LS.simps using‹path M (initial M) p›by blast ultimatelyshow"False" using‹∀io ∈ L M . length io < max_io_len›by blast qed qed
obtain p where"path M (initial M) p"and"¬ distinct (visited_states (initial M) p)" using‹¬ acyclic M›unfolding acyclic.simps by blast thenobtain pL where"path M (initial M) pL"and"max_io_len ≤ length pL" using cyclic_path_pumping[of M p max_io_len] by blast thenshow"False" using‹∧ p . path M (initial M) p ==> length p < max_io_len› using not_le by blast qed qed
lemma acyclic_finite_paths_from_reachable_state : assumes"acyclic M" and"path M (initial M) p" and"target (initial M) p = q" shows"finite {p . path M q p}" proof - from assms have"{ p . path M (initial M) p} ⊆ (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_set by auto moreoverhave"finite (acyclic_paths_up_to_length M (initial M) (size M - 1))" unfolding acyclic_paths_up_to_length.simps using paths_finite[of M "initial M""size M - 1"] by (metis (mono_tags, lifting) Collect_cong ‹FSM.acyclic M› acyclic.elims(2)) ultimatelyhave"finite { p . path M (initial M) p}" using finite_subset by blast
show"finite {p . path M q p}" proof (cases "q ∈ states M") case True
have"image (λp' . p@p') {p' . path M q p'} ⊆ {p' . path M (initial M) p'}" proof fix x assume"x ∈ image (λp' . p@p') {p' . path M q p'}" thenobtain p' where"x = p@p'"and"p' ∈ {p' . path M q p'}" by blast thenhave"path M q p'"by auto thenhave"path M (initial M) (p@p')" using path_append[OF ‹path M (initial M) p›] ‹target (initial M) p = q›by auto thenshow"x ∈ {p' . path M (initial M) p'}"using‹x = p@p'›by blast qed
thenhave"finite (image (λp' . p@p') {p' . path M q p'})" using‹finite { p . path M (initial M) p}› finite_subset by auto show ?thesis using finite_imageD[OF ‹finite (image (λp' . p@p') {p' . path M q p'})›] by (meson inj_onI same_append_eq) next case False thenshow ?thesis by (meson not_finite_existsD path_begin_state) qed qed
lemma acyclic_paths_from_reachable_states : assumes"acyclic M" and"path M (initial M) p'" and"target (initial M) p' = q" and"path M q p" shows"distinct (visited_states q p)" proof - have"path M (initial M) (p'@p)" using assms(2,3,4) path_append by metis thenhave"distinct (visited_states (initial M) (p'@p))" using assms(1) unfolding acyclic.simps by blast thenhave"distinct (initial M # (map t_target p') @ map t_target p)" by auto moreoverhave"initial M # (map t_target p') @ map t_target p = (butlast (initial M # map t_target p')) @ ((last (initial M # map t_target p')) # map t_target p)" by auto ultimatelyhave"distinct ((last (initial M # map t_target p')) # map t_target p)" by auto thenshow ?thesis using‹target (initial M) p' = q›unfolding visited_states.simps target.simps by simp qed
definition LS_acyclic :: "('a,'b,'c) fsm ==> 'a ==> ('b × 'c) list set"where "LS_acyclic M q = {p_io p | p . path M q p ∧ distinct (visited_states q p)}"
lemma LS_acyclic_code[code] : "LS_acyclic M q = image p_io (acyclic_paths_up_to_length M q (size M - 1))" unfolding acyclic_paths_set LS_acyclic_def by blast
lemma LS_from_LS_acyclic : assumes"acyclic M" shows"L M = LS_acyclic M (initial M)" proof - obtain pps :: "(('b × 'c) list ==> bool) ==> (('b × 'c) list ==> bool) ==> ('b × 'c) list"where
f1: "∀p pa. (¬ p (pps pa p)) = pa (pps pa p) ∨ Collect p = Collect pa" by (metis (no_types) Collect_cong) have"∀ps. ¬ path M (FSM.initial M) ps ∨ distinct (visited_states (FSM.initial M) ps)" using acyclic.simps assms by blast thenhave"(∄ps. pps (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa) (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa ∧ distinct (visited_states (FSM.initial M) psa)) = p_io ps ∧ path M (FSM.initial M) ps ∧ distinct (visited_states (FSM.initial M) ps)) ≠ (∃ps. pps (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa) (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa ∧ distinct (visited_states (FSM.initial M) psa)) = p_io ps ∧ path M (FSM.initial M) ps)" by blast thenhave"{p_io ps |ps. path M (FSM.initial M) ps ∧ distinct (visited_states (FSM.initial M) ps)} = {p_io ps |ps. path M (FSM.initial M) ps}" using f1 by (meson ‹∀ps. ¬ path M (FSM.initial M) ps ∨ distinct (visited_states (FSM.initial M) ps)›) thenshow ?thesis by (simp add: LS_acyclic_def) qed
lemma cyclic_cycle : assumes"¬ acyclic M" shows"∃ q p . path M q p ∧ p ≠ [] ∧ target q p = q" proof - from‹¬ acyclic M›obtain p t where"path M (initial M) (p@[t])" and"¬distinct (visited_states (initial M) (p@[t]))" by (metis (no_types, opaque_lifting) Nil_is_append_conv acyclic.simps append_take_drop_id
maximal_distinct_prefix rev_exhaust visited_states_take)
show ?thesis proof (cases "initial M ∈ set (map t_target (p@[t]))") case True thenobtain i where"last (take i (map t_target (p@[t]))) = initial M" and"i ≤ length (map t_target (p@[t]))"and"0 < i" using list_contains_last_take by metis
let ?p = "take i (p@[t])" have"path M (initial M) (?p@(drop i (p@[t])))" using‹path M (initial M) (p@[t])› by (metis append_take_drop_id) thenhave"path M (initial M) ?p"by auto moreoverhave"?p ≠ []"using‹0 < i›by auto moreoverhave"target (initial M) ?p = initial M" using‹last (take i (map t_target (p@[t]))) = initial M› unfolding target.simps visited_states.simps by (metis (no_types, lifting) calculation(2) last_ConsR list.map_disc_iff take_map) ultimatelyshow ?thesis by blast next case False thenhave"¬ distinct (map t_target (p@[t]))" using‹¬distinct (visited_states (initial M) (p@[t]))› unfolding visited_states.simps by auto thenobtain i j where"i < j"and"j < length (map t_target (p@[t]))" and"(map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j" using non_distinct_repetition_indices by blast
let ?pre_i = "take (Suc i) (p@[t])" let ?p = "take ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))" let ?post_j = "drop ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))"
have"p@[t] = ?pre_i @ ?p @ ?post_j" using‹i < j›‹j < length (map t_target (p@[t]))› by (metis append_take_drop_id) thenhave"path M (target (initial M) ?pre_i) ?p" using‹path M (initial M) (p@[t])› by (metis path_prefix path_suffix)
have"?pre_i@?p = take (Suc j) (p@[t])" by (metis (no_types) ‹i < j› add_Suc add_diff_cancel_left' less_SucI less_imp_Suc_add take_add) moreoverhave"(target (initial M) (take (Suc j) (p@[t]))) = (map t_target (p@[t])) ! j" unfolding target.simps visited_states.simps using take_last_index[OF ‹j < length (map t_target (p@[t]))›] by (metis (no_types, lifting) ‹j < length (map t_target (p @ [t]))›
last_ConsR snoc_eq_iff_butlast take_Suc_conv_app_nth take_map) ultimatelyhave"(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! j" by auto thenhave"(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! i" using‹(map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j›by simp moreoverhave"(target (initial M) (?pre_i@?p)) = (target (target (initial M) ?pre_i) ?p)" unfolding target.simps visited_states.simps last.simps by auto ultimatelyhave"(target (target (initial M) ?pre_i) ?p) = (map t_target (p@[t])) ! i" by auto thenhave"(target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)" using‹(target (initial M) ?pre_i) = (map t_target (p@[t])) ! i›by auto
show ?thesis using‹path M (target (initial M) ?pre_i) ?p›‹?p ≠ []› ‹(target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)› by blast qed qed
lemma cyclic_cycle_rev : fixes M :: "('a,'b,'c) fsm" assumes"path M (initial M) p'" and"target (initial M) p' = q" and"path M q p" and"p ≠ []" and"target q p = q" shows"¬ acyclic M" using assms unfolding acyclic.simps target.simps visited_states.simps using distinct.simps(2) by fastforce
lemma acyclic_initial : assumes"acyclic M" shows"¬ (∃ t ∈ transitions M . t_target t = initial M ∧ (∃ p . path M (initial M) p ∧ target (initial M) p = t_source t))" by (metis append_Cons assms cyclic_cycle_rev list.distinct(1) path.simps
path_append path_append_transition_elim(3) single_transition_path)
lemma cyclic_path_shift : assumes"path M q p" and"target q p = q" shows"path M (target q (take i p)) ((drop i p) @ (take i p))" and"target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))" proof - show"path M (target q (take i p)) ((drop i p) @ (take i p))" by (metis append_take_drop_id assms(1) assms(2) path_append path_append_elim path_append_target) show"target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))" by (metis append_take_drop_id assms(2) path_append_target) qed
lemma cyclic_path_transition_states_property : assumes"∃ t ∈ set p . P (t_source t)" and"∀ t ∈ set p . P (t_source t) ⟶ P (t_target t)" and"path M q p" and"target q p = q" shows"∀ t ∈ set p . P (t_source t)" and"∀ t ∈ set p . P (t_target t)" proof - obtain t0 where"t0 ∈ set p"and"P (t_source t0)" using assms(1) by blast thenobtain i where"i < length p"and"p ! i = t0" by (meson in_set_conv_nth)
let ?p = "(drop i p @ take i p)" have"path M (target q (take i p)) ?p" using cyclic_path_shift(1)[OF assms(3,4), of i] by assumption
have"set ?p = set p" proof - have"set ?p = set (take i p @ drop i p)" using list_set_sym by metis thenshow ?thesis by auto qed thenhave"∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)" using assms(2) by blast
have"∧ j . j < length ?p ==> P (t_source (?p ! j))" proof - fix j assume"j < length ?p" thenshow"P (t_source (?p ! j))" proof (induction j) case0 thenshow ?case using‹p ! i = t0›‹P (t_source t0)› by (metis ‹i < length p› drop_eq_Nil hd_append2 hd_conv_nth hd_drop_conv_nth leD
length_greater_0_conv) next case (Suc j) thenhave"P (t_source (?p ! j))" by auto thenhave"P (t_target (?p ! j))" using Suc.prems ‹∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)›[of "?p ! j"] using Suc_lessD nth_mem by blast moreoverhave"t_target (?p ! j) = t_source (?p ! (Suc j))" using path_source_target_index[OF Suc.prems ‹path M (target q (take i p)) ?p›] by assumption ultimatelyshow ?case using‹∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)›[of "?p ! j"] by simp qed qed thenhave"∀ t ∈ set ?p . P (t_source t)" by (metis in_set_conv_nth) thenshow"∀ t ∈ set p . P (t_source t)" using‹set ?p = set p›by blast thenshow"∀ t ∈ set p . P (t_target t)" using assms(2) by blast qed
lemma cycle_incoming_transition_ex : assumes"path M q p" and"p ≠ []" and"target q p = q" and"t ∈ set p" shows"∃ tI ∈ set p . t_target tI = t_source t" proof - obtain i where"i < length p"and"p ! i = t" using assms(4) by (meson in_set_conv_nth)
let ?p = "(drop i p @ take i p)" have"path M (target q (take i p)) ?p" and"target (target q (take i p)) ?p = target q (take i p)" using cyclic_path_shift[OF assms(1,3), of i] by linarith+
have"p = (take i p @ drop i p)"by auto thenhave"path M (target q (take i p)) (drop i p)" using path_suffix assms(1) by metis moreoverhave"t = hd (drop i p)" using‹i < length p›‹p ! i = t› by (simp add: hd_drop_conv_nth) ultimatelyhave"path M (target q (take i p)) [t]" by (metis ‹i < length p› append_take_drop_id assms(1) path_append_elim take_hd_drop) thenhave"t_source t = (target q (take i p))" by auto moreoverhave"t_target (last ?p) = (target q (take i p))" using‹path M (target q (take i p)) ?p›‹target (target q (take i p)) ?p = target q (take i p)›
assms(2) unfolding target.simps visited_states.simps last.simps by (metis (no_types, lifting) ‹p = take i p @ drop i p› append_is_Nil_conv last_map
list.map_disc_iff)
moreoverhave"set ?p = set p" proof - have"set ?p = set (take i p @ drop i p)" using list_set_sym by metis thenshow ?thesis by auto qed
ultimatelyshow ?thesis by (metis ‹i < length p› append_is_Nil_conv drop_eq_Nil last_in_set leD) qed
lemma acyclic_paths_finite : "finite {p . path M q p ∧ distinct (visited_states q p) }" proof - have"∧ p . path M q p ==> distinct (visited_states q p) ==> distinct p" proof - fix p assume"path M q p"and"distinct (visited_states q p)" thenhave"distinct (map t_target p)"by auto thenshow"distinct p"by (simp add: distinct_map) qed
thenshow ?thesis using finite_subset_distinct[OF fsm_transitions_finite, of M] path_transitions[of M q] by (metis (no_types, lifting) infinite_super mem_Collect_eq path_transitions subsetI) qed
lemma acyclic_no_self_loop : assumes"acyclic M" and"q ∈ reachable_states M" shows"¬ (∃ x y . (q,x,y,q) ∈ transitions M)" proof assume"∃x y. (q, x, y, q) ∈ FSM.transitions M" thenobtain x y where"(q, x, y, q) ∈ FSM.transitions M"by blast moreoverobtain p where"path M (initial M) p"and"target (initial M) p = q" using assms(2) unfolding reachable_states_def by blast ultimatelyhave"path M (initial M) (p@[(q,x,y,q)])" by (simp add: path_append_transition) moreoverhave"¬ (distinct (visited_states (initial M) (p@[(q,x,y,q)])))" using‹target (initial M) p = q›unfolding visited_states.simps target.simps by (cases p rule: rev_cases; auto) ultimatelyshow"False" using assms(1) unfolding acyclic.simps by meson qed
subsubsection‹Deadlock States›
fun deadlock_state :: "('a,'b,'c) fsm ==> 'a ==> bool"where "deadlock_state M q = (¬(∃ t ∈ transitions M . t_source t = q))"
lemma deadlock_state_alt_def : "deadlock_state M q = (LS M q ⊆ {[]})" proof show"deadlock_state M q ==> LS M q ⊆ {[]}" proof - assume"deadlock_state M q" moreoverhave"∧ p . deadlock_state M q ==> path M q p ==> p = []" unfolding deadlock_state.simps by (metis path.cases) ultimatelyshow"LS M q ⊆ {[]}" unfolding LS.simps by blast qed show"LS M q ⊆ {[]} ==> deadlock_state M q" unfolding LS.simps deadlock_state.simps using path.cases[of M q] by blast qed
lemma deadlock_state_alt_def_h : "deadlock_state M q = (∀ x ∈ inputs M . h M (q,x) = {})" unfolding deadlock_state.simps h.simps using fsm_transition_input by force
lemma acyclic_deadlock_reachable : assumes"acyclic M" shows"∃ q ∈ reachable_states M . deadlock_state M q" proof (rule ccontr) assume"¬ (∃q∈reachable_states M. deadlock_state M q)" thenhave *: "∧ q . q ∈ reachable_states M ==> (∃ t ∈ transitions M . t_source t = q)" unfolding deadlock_state.simps by blast
let ?p = "arg_max_on length {p. path M (initial M) p}"
have"finite {p. path M (initial M) p}" by (metis Collect_cong acyclic_finite_paths_from_reachable_state assms eq_Nil_appendI fsm_initial
nil path_append path_append_elim)
moreoverhave"{p. path M (initial M) p} ≠ {}" by auto ultimatelyobtain p where"path M (initial M) p" and"∧ p' . path M (initial M) p' ==> length p' ≤ length p" using max_length_elem by (metis mem_Collect_eq not_le_imp_less)
thenobtain t where"t ∈ transitions M"and"t_source t = target (initial M) p" using *[of "target (initial M) p"] unfolding reachable_states_def by blast
thenhave"path M (initial M) (p@[t])" using‹path M (initial M) p› by (simp add: path_append_transition)
thenshow"False" using‹∧ p' . path M (initial M) p' ==> length p' ≤ length p› by (metis impossible_Cons length_rotate1 rotate1.simps(2)) qed
lemma deadlock_prefix : assumes"path M q p" and"t ∈ set (butlast p)" shows"¬ (deadlock_state M (t_target t))" using assms proof (induction p rule: rev_induct) case Nil thenshow ?caseby auto next case (snoc t' p')
show ?caseproof (cases "t ∈ set (butlast p')") case True show ?thesis using snoc.IH[OF _ True] snoc.prems(1) by blast next case False thenhave"p' = (butlast p')@[t]" using snoc.prems(2) by (metis append_butlast_last_id append_self_conv2 butlast_snoc
in_set_butlast_appendI list_prefix_elem set_ConsD) thenhave"path M q ((butlast p'@[t])@[t'])" using snoc.prems(1) by auto
have"t' ∈ transitions M"and"t_source t' = target q (butlast p'@[t])" using path_suffix[OF ‹path M q ((butlast p'@[t])@[t'])›] by auto thenhave"t' ∈ transitions M ∧ t_source t' = t_target t" unfolding target.simps visited_states.simps by auto thenshow ?thesis unfolding deadlock_state.simps using‹t' ∈ transitions M›by blast qed qed
lemma states_initial_deadlock : assumes"deadlock_state M (initial M)" shows"reachable_states M = {initial M}"
proof - have"∧ q . q ∈ reachable_states M ==> q = initial M" proof - fix q assume"q ∈ reachable_states M" thenobtain p where"path M (initial M) p"and"target (initial M) p = q" unfolding reachable_states_def by auto
show"q = initial M"proof (cases p) case Nil thenshow ?thesis using‹target (initial M) p = q›by auto next case (Cons t p') thenhave"False"using assms ‹path M (initial M) p›unfolding deadlock_state.simps by auto thenshow ?thesis by simp qed qed thenshow ?thesis using reachable_states_initial[of M] by blast qed
subsubsection‹Other›
fun completed_path :: "('a,'b,'c) fsm ==> 'a ==> ('a,'b,'c) path ==> bool"where "completed_path M q p = deadlock_state M (target q p)"
fun minimal :: "('a,'b,'c) fsm ==> bool"where "minimal M = (∀ q ∈ states M . ∀ q' ∈ states M . q ≠ q' ⟶ LS M q ≠ LS M q')"
lemma minimal_alt_def : "minimal M = (∀ q q' . q ∈ states M ⟶ q' ∈ states M ⟶ LS M q = LS M q' ⟶ q = q')" by auto
fun paths_for_io' :: "(('a × 'b) ==> ('c × 'a) set) ==> ('b × 'c) list ==> 'a ==> ('a,'b,'c) path ==> ('a,'b,'c) path set"where "paths_for_io' f [] q prev = {prev}" | "paths_for_io' f ((x,y)#io) q prev = ∪(image (λyq' . paths_for_io' f io (snd yq') (prev@[(q,x,y,(snd yq'))])) (Set.filter (λyq' . fst yq' = y) (f (q,x))))"
lemma paths_for_io'_set : assumes"q ∈ states M" shows"paths_for_io' (h M) io q prev = {prev@p | p . path M q p ∧ p_io p = io}" using assms proof (induction io arbitrary: q prev) case Nil thenshow ?caseby auto next case (Cons xy io) obtain x y where"xy = (x,y)" by (meson surj_pair)
let ?UN = "∪(image (λyq' . paths_for_io' (h M) io (snd yq') (prev@[(q,x,y,(snd yq'))])) (Set.filter (λyq' . fst yq' = y) (h M (q,x))))"
have"?UN = {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" proof have"∧ p . p ∈ ?UN ==> p ∈ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" proof - fix p assume"p ∈ ?UN" thenobtain q' where"(y,q') ∈ (Set.filter (λyq' . fst yq' = y) (h M (q,x)))" and"p ∈ paths_for_io' (h M) io q' (prev@[(q,x,y,q')])" by auto
from‹(y,q') ∈ (Set.filter (λyq' . fst yq' = y) (h M (q,x)))›have"q' ∈ states M" and"(q,x,y,q') ∈ transitions M" using fsm_transition_target unfolding h.simps by auto
have"p ∈ {(prev @ [(q, x, y, q')]) @ p |p. path M q' p ∧ p_io p = io}" using‹p ∈ paths_for_io' (h M) io q' (prev@[(q,x,y,q')])› unfolding Cons.IH[OF ‹q' ∈ states M›] by assumption moreoverhave"{(prev @ [(q, x, y, q')]) @ p |p. path M q' p ∧ p_io p = io} ⊆ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" using‹(q,x,y,q') ∈ transitions M› using cons by force ultimatelyshow"p ∈ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" by blast qed thenshow"?UN ⊆ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" by blast
have"∧ p . p ∈ {prev@p | p . path M q p ∧ p_io p = (x,y)#io} ==> p ∈ ?UN" proof - fix pp assume"pp ∈ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" thenobtain p where"pp = prev@p"and"path M q p"and"p_io p = (x,y)#io" by fastforce thenobtain t p' where"p = t#p'"and"path M q (t#p')"and"p_io (t#p') = (x,y)#io" and"p_io p' = io" by (metis (no_types, lifting) map_eq_Cons_D) thenhave"path M (t_target t) p'"and"t_source t = q"and"t_input t = x" and"t_output t = y"and"t_target t ∈ states M" and"t ∈ transitions M" by auto
have"(y,t_target t) ∈ Set.filter (λyq'. fst yq' = y) (h M (q, x))" using‹t ∈ transitions M›‹t_output t = y›‹t_input t = x›‹t_source t = q› unfolding h.simps by auto moreoverhave"(prev@p) ∈ paths_for_io' (h M) io (snd (y,t_target t)) (prev @ [(q, x, y, snd (y,t_target t))])" using Cons.IH[OF ‹t_target t ∈ states M›, of "prev@[(q, x, y, t_target t)]"] using‹p = t # p'›‹p_io p' = io›‹path M (t_target t) p'›‹t_input t = x› ‹t_output t = y›‹t_source t = q› by auto
ultimatelyshow"pp ∈ ?UN"unfolding‹pp = prev@p› by blast qed thenshow"{prev@p | p . path M q p ∧ p_io p = (x,y)#io} ⊆ ?UN" by (meson subsetI) qed
thenshow ?case by (simp add: ‹xy = (x, y)›) qed
definition paths_for_io :: "('a,'b,'c) fsm ==> 'a ==> ('b × 'c) list ==> ('a,'b,'c) path set"where "paths_for_io M q io = {p . path M q p ∧ p_io p = io}"
lemma paths_for_io_set_code[code] : "paths_for_io M q io = (if q ∈ states M then paths_for_io' (h M) io q [] else {})" using paths_for_io'_set[of q M io "[]"] unfolding paths_for_io_def proof - have"{[] @ ps |ps. path M q ps ∧ p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {}) ⟶ {ps. path M q ps ∧ p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {})" by auto moreover
{ assume"{[] @ ps |ps. path M q ps ∧ p_io ps = io} ≠ (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {})" thenhave"q ∉ FSM.states M" using‹q ∈ FSM.states M ==> paths_for_io' (h M) io q [] = {[] @ p |p. path M q p ∧ p_io p = io}›by force thenhave"{ps. path M q ps ∧ p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {})" using path_begin_state by force } ultimatelyshow"{ps. path M q ps ∧ p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {})" by linarith qed
fun io_targets :: "('a,'b,'c) fsm ==> ('b × 'c) list ==> 'a ==> 'a set"where "io_targets M io q = {target q p | p . path M q p ∧ p_io p = io}"
lemma io_targets_code[code] : "io_targets M io q = image (target q) (paths_for_io M q io)" unfolding io_targets.simps paths_for_io_def by blast
lemma io_targets_states : "io_targets M io q ⊆ states M" using path_target_is_state by fastforce
lemma observable_transition_unique : assumes"observable M" and"t ∈ transitions M" shows"∃! t' ∈ transitions M . t_source t' = t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t" by (metis assms observable.elims(2) prod.expand)
lemma observable_path_unique : assumes"observable M" and"path M q p" and"path M q p'" and"p_io p = p_io p'" shows"p = p'" proof - have"length p = length p'" using assms(4) map_eq_imp_length_eq by blast thenshow ?thesis using‹p_io p = p_io p'›‹path M q p›‹path M q p'› proof (induction p p' arbitrary: q rule: list_induct2) case Nil thenshow ?caseby auto next case (Cons x xs y ys) thenhave *: "x ∈ transitions M ∧ y ∈ transitions M ∧ t_source x = t_source y ∧ t_input x = t_input y ∧ t_output x = t_output y" by auto thenhave"t_target x = t_target y" using assms(1) observable.elims(2) by blast thenhave"x = y" by (simp add: "*" prod.expand)
have"p_io xs = p_io ys" using Cons by auto
moreoverhave"path M (t_target x) xs" using Cons by auto moreoverhave"path M (t_target x) ys" using Cons ‹t_target x = t_target y›by auto ultimatelyhave"xs = ys" using Cons by auto
thenshow ?case using‹x = y›by simp qed qed
lemma observable_io_targets : assumes"observable M" and"io ∈ LS M q" obtains q' where"io_targets M io q = {q'}" proof -
obtain p where"path M q p"and"p_io p = io" using assms(2) by auto thenhave"target q p ∈ io_targets M io q" by auto
have"∃ q' . io_targets M io q = {q'}" proof (rule ccontr) assume"¬(∃q'. io_targets M io q = {q'})" thenhave"∃ q' . q' ≠ target q p ∧ q' ∈ io_targets M io q" proof - have"¬ io_targets M io q ⊆ {target q p}" using‹¬(∃q'. io_targets M io q = {q'})›‹target q p ∈ io_targets M io q›by blast thenshow ?thesis by blast qed thenobtain q' where"q' ≠ target q p"and"q' ∈ io_targets M io q" by blast thenobtain p' where"path M q p'"and"target q p' = q'"and"p_io p' = io" by auto thenhave"p_io p = p_io p'" using‹p_io p = io›by simp thenhave"p = p'" using observable_path_unique[OF assms(1) ‹path M q p›‹path M q p'›] by simp thenshow"False" using‹q' ≠ target q p›‹target q p' = q'›by auto qed
thenshow ?thesis using that by blast qed
lemma observable_path_io_target : assumes"observable M" and"path M q p" shows"io_targets M (p_io p) q = {target q p}" using observable_io_targets[OF assms(1) language_state_containment[OF assms(2)], of "p_io p"]
singletonD[of "target q p"] unfolding io_targets.simps proof - assume a1: "∧a. target q p ∈ {a} ==> target q p = a" assume"∧thesis. [p_io p = p_io p; ∧q'. {target q pa |pa. path M q pa ∧ p_io pa = p_io p} = {q'} ==> thesis]==> thesis" thenobtain aa :: 'a where"∧b. {target q ps |ps. path M q ps ∧ p_io ps = p_io p} = {aa} ∨ b" by meson thenshow"{target q ps |ps. path M q ps ∧ p_io ps = p_io p} = {target q p}" using a1 assms(2) by blast qed
lemma completely_specified_io_targets : assumes"completely_specified M" shows"∀ q ∈ io_targets M io (initial M) . ∀ x ∈ (inputs M) . ∃ t ∈ transitions M . t_source t = q ∧ t_input t = x" by (meson assms completely_specified.elims(2) io_targets_states subsetD)
lemma observable_path_language_step : assumes"observable M" and"path M q p" and"¬ (∃t∈transitions M. t_source t = target q p ∧ t_input t = x ∧ t_output t = y)" shows"(p_io p)@[(x,y)] ∉ LS M q" using assms proof (induction p rule: rev_induct) case Nil show ?caseproof assume"p_io [] @ [(x, y)] ∈ LS M q" thenobtain p' where"path M q p'"and"p_io p' = [(x,y)]"unfolding LS.simps by force thenobtain t where"p' = [t]"by blast
have"t∈transitions M"and"t_source t = target q []" using‹path M q p'›‹p' = [t]›by auto moreoverhave"t_input t = x ∧ t_output t = y" using‹p_io p' = [(x,y)]›‹p' = [t]›by auto ultimatelyshow"False" using Nil.prems(3) by blast qed next case (snoc t p)
from‹path M q (p @ [t])›have"path M q p"and"t_source t = target q p" and"t ∈ transitions M" by auto
show ?caseproof assume"p_io (p @ [t]) @ [(x, y)] ∈ LS M q" thenobtain p' where"path M q p'"and"p_io p' = p_io (p @ [t]) @ [(x, y)]" by auto thenobtain p'' t' t'' where"p' = p''@[t']@[t'']" by (metis (no_types, lifting) append.assoc map_butlast map_is_Nil_conv snoc_eq_iff_butlast) thenhave"path M q p''" using‹path M q p'›by blast
have"p_io p'' = p_io p" using‹p' = p''@[t']@[t'']›‹p_io p' = p_io (p @ [t]) @ [(x, y)]›by auto thenhave"p'' = p" using observable_path_unique[OF assms(1) ‹path M q p''›‹path M q p›] by blast
have"t_source t' = target q p''"and"t' ∈ transitions M" using‹path M q p'›‹p' = p''@[t']@[t'']›by auto thenhave"t_source t' = t_source t" using‹p'' = p›‹t_source t = target q p›by auto moreoverhave"t_input t' = t_input t ∧ t_output t' = t_output t" using‹p_io p' = p_io (p @ [t]) @ [(x, y)]›‹p' = p''@[t']@[t'']›‹p'' = p›by auto ultimatelyhave"t' = t" using‹t ∈ transitions M›‹t' ∈ transitions M› assms(1) unfolding observable.simps by (meson prod.expand)
have"t'' ∈ transitions M"and"t_source t'' = target q (p@[t])" using‹path M q p'›‹p' = p''@[t']@[t'']›‹p'' = p›‹t' = t›by auto moreoverhave"t_input t'' = x ∧ t_output t'' = y" using‹p_io p' = p_io (p @ [t]) @ [(x, y)]›‹p' = p''@[t']@[t'']›by auto ultimatelyshow"False" using snoc.prems(3) by blast qed qed
lemma observable_io_targets_language : assumes"io1 @ io2 ∈ LS M q1" and"observable M" and"q2 ∈ io_targets M io1 q1" shows"io2 ∈ LS M q2" proof - obtain p1 p2 where"path M q1 p1"and"path M (target q1 p1) p2" and"p_io p1 = io1"and"p_io p2 = io2" using language_state_split[OF assms(1)] by blast thenhave"io1 ∈ LS M q1"and"io2 ∈ LS M (target q1 p1)" by auto
have"target q1 p1 ∈ io_targets M io1 q1" using‹path M q1 p1›‹p_io p1 = io1› unfolding io_targets.simps by blast thenhave"target q1 p1 = q2" using observable_io_targets[OF assms(2) ‹io1 ∈ LS M q1›] by (metis assms(3) singletonD) thenshow ?thesis using‹io2 ∈ LS M (target q1 p1)›by auto qed
lemma io_targets_language_append : assumes"q1 ∈ io_targets M io1 q" and"io2 ∈ LS M q1" shows"io1@io2 ∈ LS M q" proof - obtain p1 where"path M q p1"and"p_io p1 = io1"and"target q p1 = q1" using assms(1) by auto moreoverobtain p2 where"path M q1 p2"and"p_io p2 = io2" using assms(2) by auto ultimatelyhave"path M q (p1@p2)"and"p_io (p1@p2) = io1@io2" by auto thenshow ?thesis using language_state_containment[of M q "p1@p2""io1@io2"] by simp qed
lemma io_targets_next : assumes"t ∈ transitions M" shows"io_targets M io (t_target t) ⊆ io_targets M (p_io [t] @ io) (t_source t)" unfolding io_targets.simps proof fix q assume"q ∈ {target (t_target t) p |p. path M (t_target t) p ∧ p_io p = io}" thenobtain p where"path M (t_target t) p ∧ p_io p = io ∧ target (t_target t) p = q" by auto thenhave"path M (t_source t) (t#p) ∧ p_io (t#p) = p_io [t] @ io ∧ target (t_source t) (t#p) = q" using FSM.path.cons[OF assms] by auto thenshow"q ∈ {target (t_source t) p |p. path M (t_source t) p ∧ p_io p = p_io [t] @ io}" by blast qed
lemma observable_io_targets_next : assumes"observable M" and"t ∈ transitions M" shows"io_targets M (p_io [t] @ io) (t_source t) = io_targets M io (t_target t)" proof show"io_targets M (p_io [t] @ io) (t_source t) ⊆ io_targets M io (t_target t)" proof fix q assume"q ∈ io_targets M (p_io [t] @ io) (t_source t)" thenobtain p where"q = target (t_source t) p" and"path M (t_source t) p" and"p_io p = p_io [t] @ io" unfolding io_targets.simps by blast thenhave"q = t_target (last p)"unfolding target.simps visited_states.simps using last_map by auto
obtain t' p' where"p = t' # p'" using‹p_io p = p_io [t] @ io›by auto thenhave"t' ∈ transitions M"and"t_source t' = t_source t" using‹path M (t_source t) p›by auto moreoverhave"t_input t' = t_input t"and"t_output t' = t_output t" using‹p = t' # p'›‹p_io p = p_io [t] @ io›by auto ultimatelyhave"t' = t" using‹t ∈ transitions M›‹observable M›unfolding observable.simps by (meson prod.expand)
thenhave"path M (t_target t) p'" using‹path M (t_source t) p›‹p = t' # p'›by auto moreoverhave"p_io p' = io" using‹p_io p = p_io [t] @ io›‹p = t' # p'›by auto moreoverhave"q = target (t_target t) p'" using‹q = target (t_source t) p›‹p = t' # p'›‹t' = t›by auto ultimatelyshow"q ∈ io_targets M io (t_target t)" by auto qed
show"io_targets M io (t_target t) ⊆ io_targets M (p_io [t] @ io) (t_source t)" using io_targets_next[OF assms(2)] by assumption qed
lemma observable_language_target : assumes"observable M" and"q ∈ io_targets M io1 (initial M)" and"t ∈ io_targets T io1 (initial T)" and"L T ⊆ L M" shows"LS T t ⊆ LS M q" proof fix io2 assume"io2 ∈ LS T t" thenobtain pT2 where"path T t pT2"and"p_io pT2 = io2" by auto
obtain pT1 where"path T (initial T) pT1"and"p_io pT1 = io1"and"target (initial T) pT1 = t" using‹t ∈ io_targets T io1 (initial T)›by auto thenhave"path T (initial T) (pT1@pT2)" using‹path T t pT2›using path_append by metis moreoverhave"p_io (pT1@pT2) = io1@io2" using‹p_io pT1 = io1›‹p_io pT2 = io2›by auto ultimatelyhave"io1@io2 ∈ L T" using language_state_containment[of T] by auto thenhave"io1@io2 ∈ L M" using‹L T ⊆ L M›by blast thenobtain pM where"path M (initial M) pM"and"p_io pM = io1@io2" by auto
let ?pM1 = "take (length io1) pM" let ?pM2 = "drop (length io1) pM"
have"path M (initial M) (?pM1@?pM2)" using‹path M (initial M) pM›by auto thenhave"path M (initial M) ?pM1"and"path M (target (initial M) ?pM1) ?pM2" by blast+
obtain pM1 where"path M (initial M) pM1"and"p_io pM1 = io1"and"target (initial M) pM1 = q" using‹q ∈ io_targets M io1 (initial M)›by auto
have"pM1 = ?pM1" using observable_path_unique[OF ‹observable M›‹path M (initial M) pM1›‹path M (initial M) ?pM1›] unfolding‹p_io pM1 = io1›‹p_io ?pM1 = io1›by simp
thenhave"path M q ?pM2" using‹path M (target (initial M) ?pM1) ?pM2›‹target (initial M) pM1 = q›by auto thenshow"io2 ∈ LS M q" using language_state_containment[OF _ ‹p_io ?pM2 = io2›, of M] by auto qed
lemma observable_language_target_failure : assumes"observable M" and"q ∈ io_targets M io1 (initial M)" and"t ∈ io_targets T io1 (initial T)" and"¬ LS T t ⊆ LS M q" shows"¬ L T ⊆ L M" using observable_language_target[OF assms(1,2,3)] assms(4) by blast
lemma language_path_append_transition_observable : assumes"(p_io p) @ [(x,y)] ∈ LS M q" and"path M q p" and"observable M" obtains t where"path M q (p@[t])"and"t_input t = x"and"t_output t = y" proof - obtain p' t where"path M q (p'@[t])"and"p_io (p'@[t]) = (p_io p) @ [(x,y)]" using language_path_append_transition[OF assms(1)] by blast thenhave"path M q p'"and"p_io p' = p_io p"and"t_input t = x"and"t_output t = y" by auto
have"p' = p" using observable_path_unique[OF assms(3) ‹path M q p'›‹path M q p›‹p_io p' = p_io p›] by assumption thenhave"path M q (p@[t])" using‹path M q (p'@[t])›by auto thenshow ?thesis using that ‹t_input t = x›‹t_output t = y›by metis qed
lemma language_io_target_append : assumes"q' ∈ io_targets M io1 q" and"io2 ∈ LS M q'" shows"(io1@io2) ∈ LS M q" proof - obtain p2 where"path M q' p2"and"p_io p2 = io2" using assms(2) by auto
moreoverobtain p1 where"q' = target q p1"and"path M q p1"and"p_io p1 = io1" using assms(1) by auto
ultimatelyshow ?thesis unfolding LS.simps by (metis (mono_tags, lifting) map_append mem_Collect_eq path_append) qed
lemma observable_path_suffix : assumes"(p_io p)@io ∈ LS M q" and"path M q p" and"observable M" obtains p' where"path M (target q p) p'"and"p_io p' = io" proof - obtain p1 p2 where"path M q p1"and"path M (target q p1) p2"and"p_io p1 = p_io p"and"p_io p2 = io" using language_state_split[OF assms(1)] by blast
have"p1 = p" using observable_path_unique[OF assms(3,2) ‹path M q p1›‹p_io p1 = p_io p›[symmetric]] by simp
show ?thesis using that[of p2] ‹path M (target q p1) p2›‹p_io p2 = io›unfolding‹p1 = p› by blast qed
lemma io_targets_finite : "finite (io_targets M io q)" proof - have"(io_targets M io q) ⊆ {target q p | p . path M q p ∧ length p ≤ length io}" unfolding io_targets.simps length_map[of "(λ t . (t_input t, t_output t))", symmetric] by force moreoverhave"finite {target q p | p . path M q p ∧ length p ≤ length io}" using paths_finite[of M q "length io"] by simp ultimatelyshow ?thesis using rev_finite_subset by blast qed
lemma language_next_transition_ob : assumes"(x,y)#ios ∈ LS M q" obtains t where"t_source t = q" and"t ∈ transitions M" and"t_input t = x" and"t_output t = y" and"ios ∈ LS M (t_target t)" proof - obtain p where"path M q p"and"p_io p = (x,y)#ios" using assms unfolding LS.simps mem_Collect_eq by (metis (no_types, lifting)) thenobtain t p' where"p = t#p'" by blast
have"t_source t = q" and"t ∈ transitions M" and"path M (t_target t) p'" using‹path M q p›unfolding‹p = t#p'›by auto moreoverhave"t_input t = x" and"t_output t = y" and"p_io p' = ios" using‹p_io p = (x,y)#ios›unfolding‹p = t#p'›by auto ultimatelyshow ?thesis using that[of t] by auto qed
lemma h_observable_card : assumes"observable M" shows"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≤ 1" and"finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))" proof - have"snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q') ∈ transitions M}" unfolding h.simps by force moreoverhave"{q' . (q,x,y,q') ∈ transitions M} = {} ∨ (∃ q' . {q' . (q,x,y,q') ∈ transitions M} = {q'})" using assms unfolding observable_alt_def by blast ultimatelyshow"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≤ 1" and"finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))" by auto qed
lemma h_obs_None : assumes"observable M" shows"(h_obs M q x y = None) = (∄q' . (q,x,y,q') ∈ transitions M)" proof show"(h_obs M q x y = None) ==> (∄q' . (q,x,y,q') ∈ transitions M)" proof - assume"h_obs M q x y = None" thenhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≠ 1" by auto thenhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 0" using h_observable_card(1)[OF assms, of y q x] by presburger thenhave"(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {}" using h_observable_card(2)[OF assms, of y q x] card_0_eq[of "(snd ` Set.filter (λ(y', q'). y' = y) (h M (q, x)))"] by blast thenshow ?thesis unfolding h.simps by force qed show"(∄q' . (q,x,y,q') ∈ transitions M) ==> (h_obs M q x y = None)" proof - assume"(∄q' . (q,x,y,q') ∈ transitions M)" thenhave"snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}" unfolding h.simps by force thenhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 0" by (simp add: card_eq_0_iff) thenshow ?thesis unfolding h_obs_simps Let_def ‹snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}› by auto qed qed
lemma h_obs_Some : assumes"observable M" shows"(h_obs M q x y = Some q') = ({q' . (q,x,y,q') ∈ transitions M} = {q'})" proof have *: "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q') ∈ transitions M}" unfolding h.simps by force
show"h_obs M q x y = Some q' ==> ({q' . (q,x,y,q') ∈ transitions M} = {q'})" proof - assume"h_obs M q x y = Some q'" thenhave"(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≠ {}" by (auto simp add: card_1_singleton_iff split: if_splits) thenhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) > 0" unfolding h_simps using fsm_transitions_finite[of M] by (metis assms card_0_eq h_observable_card(2) h_simps neq0_conv) moreoverhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≤ 1" using assms unfolding observable_alt_def h_simps by (metis assms h_observable_card(1) h_simps) ultimatelyhave"card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 1" by auto thenhave"(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}" using‹h_obs M q x y = Some q'›unfolding h_obs_simps Let_def by (metis card_1_singletonE option.inject the_elem_eq) thenshow ?thesis using * unfolding h.simps by blast qed
show"({q' . (q,x,y,q') ∈ transitions M} = {q'}) ==> (h_obs M q x y = Some q')" proof - assume"({q' . (q,x,y,q') ∈ transitions M} = {q'})" thenhave"snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q'}" unfolding h.simps by force thenshow ?thesis unfolding Let_def by simp qed qed
lemma h_obs_state : assumes"h_obs M q x y = Some q'" shows"q' ∈ states M" proof (cases "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = 1") case True thenhave"(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}" using‹h_obs M q x y = Some q'›unfolding h_obs_simps Let_def by (metis card_1_singletonE option.inject the_elem_eq) thenhave"(q,x,y,q') ∈ transitions M" unfolding h_simps by auto thenshow ?thesis by (metis fsm_transition_target snd_conv) next case False thenhave"h_obs M q x y = None" using False unfolding h_obs_simps Let_def by auto thenshow ?thesis using assms by auto qed
fun after :: "('a,'b,'c) fsm ==> 'a ==> ('b × 'c) list ==> 'a"where "after M q [] = q" | "after M q ((x,y)#io) = after M (the (h_obs M q x y)) io"
(*abbreviation(input) "after_initial M io \<equiv> after M (initial M) io" *) abbreviation"after_initial M io ≡ after M (initial M) io"
lemma after_path : assumes"observable M" and"path M q p" shows"after M q (p_io p) = target q p" using assms(2) proof (induction p arbitrary: q rule: list.induct) case Nil thenshow ?caseby auto next case (Cons t p) thenhave"t ∈ transitions M"and"path M (t_target t) p"and"t_source t = q" by auto
have"∧ q' . (q, t_input t, t_output t, q') ∈ FSM.transitions M ==> q' = t_target t" using observable_transition_unique[OF assms(1) ‹t ∈ transitions M›] ‹t ∈ transitions M› using‹t_source t = q› assms(1) by auto thenhave"({q'. (q, t_input t, t_output t, q') ∈ FSM.transitions M} = {t_target t})" using‹t ∈ transitions M›‹t_source t = q›by auto thenhave"(h_obs M q (t_input t) (t_output t)) = Some (t_target t)" using h_obs_Some[OF assms(1), of q "t_input t""t_output t""t_target t"] by blast thenhave"after M q (p_io (t#p)) = after M (t_target t) (p_io p)" by auto moreoverhave"target (t_target t) p = target q (t#p)" using‹t_source t = q›by auto ultimatelyshow ?case using Cons.IH[OF ‹path M (t_target t) p›] by simp qed
lemma observable_after_path : assumes"observable M" and"io ∈ LS M q" obtains p where"path M q p" and"p_io p = io" and"target q p = after M q io" using after_path[OF assms(1)] using assms(2) by auto
lemma h_obs_from_LS : assumes"observable M" and"[(x,y)] ∈ LS M q" obtains q' where"h_obs M q x y = Some q'" using assms(2) h_obs_None[OF assms(1), of q x y] by force
lemma after_h_obs : assumes"observable M" and"h_obs M q x y = Some q'" shows"after M q [(x,y)] = q'" proof - have"path M q [(q,x,y,q')]" using assms(2) unfolding h_obs_Some[OF assms(1)] using single_transition_path by fastforce thenshow ?thesis using assms(2) after_path[OF assms(1), of q "[(q,x,y,q')]"] by auto qed
lemma after_h_obs_prepend : assumes"observable M" and"h_obs M q x y = Some q'" and"io ∈ LS M q'" shows"after M q ((x,y)#io) = after M q' io" proof - obtain p where"path M q' p"and"p_io p = io" using assms(3) by auto thenhave"after M q' io = target q' p" using after_path[OF assms(1)] by blast
have"path M q ((q,x,y,q')#p)" using assms(2) path_prepend_t[OF ‹path M q' p›, of q x y] unfolding h_obs_Some[OF assms(1)] by auto moreoverhave"p_io ((q,x,y,q')#p) = (x,y)#io" using‹p_io p = io›by auto ultimatelyhave"after M q ((x,y)#io) = target q ((q,x,y,q')#p)" using after_path[OF assms(1), of q "(q,x,y,q')#p"] by simp moreoverhave"target q ((q,x,y,q')#p) = target q' p" by auto ultimatelyshow ?thesis using‹after M q' io = target q' p›by simp qed
lemma after_split : assumes"observable M" and"α@γ ∈ LS M q" shows"after M (after M q α) γ = after M q (α @ γ)" proof - obtain p1 p2 where"path M q p1"and"path M (target q p1) p2"and"p_io p1 = α"and"p_io p2 = γ" using language_state_split[OF assms(2)] by blast thenhave"path M q (p1@p2)"and"p_io (p1@p2) = (α @ γ)" by auto thenhave"after M q (α @ γ) = target q (p1@p2)" using assms(1) by (metis (mono_tags, lifting) after_path) moreoverhave"after M q α = target q p1" using‹path M q p1›‹p_io p1 = α› assms(1) by (metis (mono_tags, lifting) after_path) moreoverhave"after M (target q p1) γ = target (target q p1) p2" using‹path M (target q p1) p2›‹p_io p2 = γ› assms(1) by (metis (mono_tags, lifting) after_path) moreoverhave"target (target q p1) p2 = target q (p1@p2)" by auto ultimatelyshow ?thesis by auto qed
lemma after_io_targets : assumes"observable M" and"io ∈ LS M q" shows"after M q io = the_elem (io_targets M io q)" proof - have"after M q io ∈ io_targets M io q" using after_path[OF assms(1)] assms(2) unfolding io_targets.simps LS.simps by blast thenshow ?thesis using observable_io_targets[OF assms] by (metis singletonD the_elem_eq) qed
lemma after_language_subset : assumes"observable M" and"α@γ ∈ L M" and"β ∈ LS M (after_initial M (α@γ))" shows"γ@β ∈ LS M (after_initial M α)" by (metis after_io_targets after_split assms(1) assms(2) assms(3) language_io_target_append language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)
lemma after_language_append_iff : assumes"observable M" and"α@γ ∈ L M" shows"β ∈ LS M (after_initial M (α@γ)) = (γ@β ∈ LS M (after_initial M α))" by (metis after_io_targets after_language_subset after_split assms(1) assms(2) language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)
lemma h_obs_language_iff : assumes"observable M" shows"(x,y)#io ∈ LS M q = (∃ q' . h_obs M q x y = Some q' ∧ io ∈ LS M q')"
(is"?P1 = ?P2") proof show"?P1 ==> ?P2" proof - assume ?P1 thenobtain t p where"t ∈ transitions M" and"path M (t_target t) p" and"t_input t = x" and"t_output t = y" and"t_source t = q" and"p_io p = io" by auto thenhave"(q,x,y,t_target t) ∈ transitions M" by auto thenhave"h_obs M q x y = Some (t_target t)" unfolding h_obs_Some[OF assms] using assms by auto moreoverhave"io ∈ LS M (t_target t)" using‹path M (t_target t) p›‹p_io p = io› by auto ultimatelyshow ?P2 by blast qed show"?P2 ==> ?P1" unfolding h_obs_Some[OF assms] using LS_prepend_transition[where io=io and M=M] by (metis fst_conv mem_Collect_eq singletonI snd_conv) qed
lemma after_language_iff : assumes"observable M" and"α ∈ LS M q" shows"(γ ∈ LS M (after M q α)) = (α@γ ∈ LS M q)" by (metis after_io_targets assms(1) assms(2) language_io_target_append observable_io_targets observable_io_targets_language singletonI the_elem_eq)
(* TODO: generalise to non-observable FSMs *) lemma language_maximal_contained_prefix_ob : assumes"io ∉ LS M q" and"q ∈ states M" and"observable M" obtains io' x y io'' where"io = io'@[(x,y)]@io''" and"io' ∈ LS M q" and"io'@[(x,y)] ∉ LS M q" proof - have"∃ io' x y io'' . io = io'@[(x,y)]@io'' ∧ io' ∈ LS M q ∧ io'@[(x,y)] ∉ LS M q" using assms(1,2) proof (induction io arbitrary: q) case Nil thenshow ?caseby auto next case (Cons xy io)
obtain x y where"xy = (x,y)" by fastforce
show ?caseproof (cases "h_obs M q x y") case None thenhave"[]@[(x,y)] ∉ LS M q" unfolding h_obs_None[OF assms(3)] by auto moreoverhave"[] ∈ LS M q" using Cons.prems by auto moreoverhave"(x,y)#io = []@[(x,y)]@io" using Cons.prems unfolding‹xy = (x,y)›by auto ultimatelyshow ?thesis unfolding‹xy = (x,y)›by blast next case (Some q') thenhave"io ∉ LS M q'" using h_obs_language_iff[OF assms(3), of x y io q] Cons.prems(1) unfolding‹xy = (x,y)› by auto thenobtain io' x' y' io'' where"io = io'@[(x',y')]@io''" and"io' ∈ LS M q'" and"io'@[(x',y')] ∉ LS M q'" using Cons.IH[OF _ h_obs_state[OF Some]] by blast
have"xy#io = (xy#io')@[(x',y')]@io''" using‹io = io'@[(x',y')]@io''›by auto moreoverhave"(xy#io') ∈ LS M q" using‹io' ∈ LS M q'› Some unfolding‹xy = (x,y)› h_obs_language_iff[OF assms(3)] by blast moreoverhave"(xy#io')@[(x',y')] ∉ LS M q" using‹io'@[(x',y')] ∉ LS M q'› Some h_obs_language_iff[OF assms(3), of x y "io'@[(x',y')]" q] unfolding‹xy = (x,y)› by auto ultimatelyshow ?thesis by blast qed qed thenshow ?thesis using that by blast qed
lemma after_is_state : assumes"observable M" assumes"io ∈ LS M q" shows"FSM.after M q io ∈ states M" using assms by (metis observable_after_path path_target_is_state)
lemma after_reachable_initial : assumes"observable M" and"io ∈ L M" shows"after_initial M io ∈ reachable_states M" proof - obtain p where"path M (initial M) p"and"p_io p = io" using assms(2) by auto thenhave"after_initial M io = target (initial M) p" using after_path[OF assms(1)] by blast thenshow ?thesis unfolding reachable_states_def using‹path M (initial M) p›by blast qed
lemma after_transition : assumes"observable M" and"(q,x,y,q') ∈ transitions M" shows"after M q [(x,y)] = q'" using after_path[OF assms(1) single_transition_path[OF assms(2)]] by auto
lemma after_transition_exhaust : assumes"observable M" and"t ∈ transitions M" shows"t_target t = after M (t_source t) [(t_input t, t_output t)]" using after_transition[OF assms(1)] assms(2) by (metis surjective_pairing)
lemma after_reachable : assumes"observable M" and"io ∈ LS M q" and"q ∈ reachable_states M" shows"after M q io ∈ reachable_states M" proof - obtain p where"path M q p"and"p_io p = io" using assms(2) by auto thenhave"after M q io = target q p" using after_path[OF assms(1)] by force
obtain p' where"path M (initial M) p'"and"target (initial M) p' = q" using assms(3) unfolding reachable_states_def by blast
thenhave"path M (initial M) (p'@p)" using‹path M q p›by auto moreoverhave"after M q io = target (initial M) (p'@p)" using‹target (initial M) p' = q› unfolding‹after M q io = target q p› by auto ultimatelyshow ?thesis unfolding reachable_states_def by blast qed
lemma observable_after_language_append : assumes"observable M" and"io1 ∈ LS M q" and"io2 ∈ LS M (after M q io1)" shows"io1@io2 ∈ LS M q" using observable_after_path[OF assms(1,2)] assms(3) proof - assume a1: "∧thesis. (∧p. [path M q p; p_io p = io1; target q p = after M q io1]==> thesis) ==> thesis" have"∃ps. io2 = p_io ps ∧ path M (after M q io1) ps" using‹io2 ∈ LS M (after M q io1)›by auto moreover
{ assume"(∃ps. io2 = p_io ps ∧ path M (after M q io1) ps) ∧ (∀ps. io1 @ io2 ≠ p_io ps ∨¬ path M q ps)" thenhave"io1 @ io2 ∈ {p_io ps |ps. path M q ps}" using a1 by (metis (lifting) map_append path_append) } ultimatelyshow ?thesis by auto qed
lemma observable_after_language_none : assumes"observable M" and"io1 ∈ LS M q" and"io2 ∉ LS M (after M q io1)" shows"io1@io2 ∉ LS M q" using after_path[OF assms(1)] language_state_split[of io1 io2 M q] by (metis (mono_tags, lifting) assms(3) language_intro)
lemma observable_after_eq : assumes"observable M" and"after M q io1 = after M q io2" and"io1 ∈ LS M q" and"io2 ∈ LS M q" shows"io1@io ∈ LS M q ⟷ io2@io ∈ LS M q" using observable_after_language_append[OF assms(1,3), of io]
observable_after_language_append[OF assms(1,4), of io]
assms(2) by (metis assms(1) language_prefix observable_after_language_none)
lemma observable_after_target : assumes"observable M" and"io @ io' ∈ LS M q" and"path M (FSM.after M q io) p" and"p_io p = io'" shows"target (FSM.after M q io) p = (FSM.after M q (io @ io'))" proof - obtain p' where"path M q p'"and"p_io p' = io @ io'" using‹io @ io' ∈ LS M q›by auto
thenhave"path M q (take (length io) p')" and"p_io (take (length io) p') = io" and"path M (target q (take (length io) p')) (drop (length io) p')" and"p_io (drop (length io) p') = io'" using path_io_split[of M q p' io io'] by auto thenhave"FSM.after M q io = target q (take (length io) p')" using after_path assms(1) by fastforce thenhave"p = (drop (length io) p')" using‹path M (target q (take (length io) p')) (drop (length io) p')›‹p_io (drop (length io) p') = io'›
assms(3,4)
observable_path_unique[OF ‹observable M›] by force
have"(FSM.after M q (io @ io')) = target q p'" using after_path[OF ‹observable M›‹path M q p'›] unfolding‹p_io p' = io @ io'› . moreoverhave"target (FSM.after M q io) p = target q p'" using‹FSM.after M q io = target q (take (length io) p')› by (metis ‹p = drop (length io) p'› append_take_drop_id path_append_target) ultimatelyshow ?thesis by simp qed
fun is_in_language :: "('a,'b,'c) fsm ==> 'a ==> ('b ×'c) list ==> bool"where "is_in_language M q [] = True" | "is_in_language M q ((x,y)#io) = (case h_obs M q x y of None ==> False | Some q' ==> is_in_language M q' io)"
lemma is_in_language_iff : assumes"observable M" and"q ∈ states M" shows"is_in_language M q io ⟷ io ∈ LS M q" using assms(2) proof (induction io arbitrary: q) case Nil thenshow ?case by auto next case (Cons xy io)
obtain x y where"xy = (x,y)" using prod.exhaust by metis
show ?case unfolding‹xy = (x,y)› unfolding h_obs_language_iff[OF assms(1), of x y io q] unfolding is_in_language.simps apply (cases "h_obs M q x y") apply auto[1] by (metis Cons.IH h_obs_state option.simps(5)) qed
lemma observable_paths_for_io : assumes"observable M" and"io ∈ LS M q" obtains p where"paths_for_io M q io = {p}" proof - obtain p where"path M q p"and"p_io p = io" using assms(2) by auto thenhave"p ∈ paths_for_io M q io" unfolding paths_for_io_def by blast thenshow ?thesis using that[of p] using observable_path_unique[OF assms(1) ‹path M q p›] ‹p_io p = io› unfolding paths_for_io_def by force qed
lemma io_targets_language : assumes"q' ∈ io_targets M io q" shows"io ∈ LS M q" using assms by auto
lemma observable_after_reachable_surj : assumes"observable M" shows"(after_initial M) ` (L M) = reachable_states M" proof show"after_initial M ` L M ⊆ reachable_states M" using after_reachable[OF assms _ reachable_states_initial] by blast show"reachable_states M ⊆ after_initial M ` L M" unfolding reachable_states_def using after_path[OF assms] using image_iff by fastforce qed
define V where"V = (λ q . SOME io . io ∈ L M1 ∧ after_initial M2 io = q)"
have"∧ q . q ∈ reachable_states M2 ==> V q ∈ L M1 ∧ after_initial M2 (V q) = q" proof - fix q assume"q ∈ reachable_states M2" thenhave"∃ io . io ∈ L M1 ∧ after_initial M2 io = q" unfolding‹L M1 = L M2› by (metis assms(4) imageE observable_after_reachable_surj) thenshow"V q ∈ L M1 ∧ after_initial M2 (V q) = q" unfolding V_def using someI_ex[of "λ io . io ∈ L M1 ∧ after_initial M2 io = q"] by blast qed thenhave"(after_initial M1) ` V ` reachable_states M2 ⊆ reachable_states M1" by (metis assms(3) image_mono image_subsetI observable_after_reachable_surj) thenhave"card (after_initial M1 ` V ` reachable_states M2) ≤ size_r M1" using reachable_states_finite[of M1] by (meson card_mono)
have"(after_initial M2) ` V ` reachable_states M2 = reachable_states M2" proof show"after_initial M2 ` V ` reachable_states M2 ⊆ reachable_states M2" using‹∧ q . q ∈ reachable_states M2 ==> V q ∈ L M1 ∧ after_initial M2 (V q) = q›by auto show"reachable_states M2 ⊆ after_initial M2 ` V ` reachable_states M2" using‹∧ q . q ∈ reachable_states M2 ==> V q ∈ L M1 ∧ after_initial M2 (V q) = q› observable_after_reachable_surj[OF assms(4)] unfolding‹L M1 = L M2› using image_iff by fastforce qed thenhave"card ((after_initial M2) ` V ` reachable_states M2) = size_r M2" by auto
have *: "finite (V ` reachable_states M2)" by (simp add: reachable_states_finite)
have **: "card ((after_initial M1) ` V ` reachable_states M2) < card ((after_initial M2) ` V ` reachable_states M2)" using assms(5) ‹card (after_initial M1 ` V ` reachable_states M2) ≤ size_r M1› unfolding‹card ((after_initial M2) ` V ` reachable_states M2) = size_r M2› by linarith
obtain io1 io2 where"io1 ∈ V ` reachable_states M2" "io2 ∈ V ` reachable_states M2" "after_initial M2 io1 ≠ after_initial M2 io2" "after_initial M1 io1 = after_initial M1 io2" using finite_card_less_witnesses[OF * **] by blast thenhave"io1 ∈ L M1"and"io2 ∈ L M1"and"io1 ∈ L M2"and"io2 ∈ L M2" using‹∧ q . q ∈ reachable_states M2 ==> V q ∈ L M1 ∧ after_initial M2 (V q) = q›unfolding‹L M1 = L M2› by auto thenhave"after_initial M1 io1 ∈ reachable_states M1" "after_initial M1 io2 ∈ reachable_states M1" "after_initial M2 io1 ∈ reachable_states M2" "after_initial M2 io2 ∈ reachable_states M2" using after_reachable[OF assms(3) _ reachable_states_initial] after_reachable[OF assms(4) _ reachable_states_initial] by blast+
obtain io3 where"io3 ∈ LS M2 (after_initial M2 io1) = (io3 ∉ LS M2 (after_initial M2 io2))" using reachable_state_is_state[OF ‹after_initial M2 io1 ∈ reachable_states M2›]
reachable_state_is_state[OF ‹after_initial M2 io2 ∈ reachable_states M2›] ‹after_initial M2 io1 ≠ after_initial M2 io2› assms(2) unfolding minimal.simps by blast thenhave"io1@io3 ∈ L M2 = (io2@io3 ∉ L M2)" using observable_after_language_append[OF assms(4) ‹io1 ∈ L M2›]
observable_after_language_append[OF assms(4) ‹io2 ∈ L M2›]
observable_after_language_none[OF assms(4) ‹io1 ∈ L M2›]
observable_after_language_none[OF assms(4) ‹io2 ∈ L M2›] by blast moreoverhave"io1@io3 ∈ L M1 = (io2@io3 ∈ L M1)" by (meson ‹after_initial M1 io1 = after_initial M1 io2›‹io1 ∈ L M1›‹io2 ∈ L M1›assms(3) observable_after_eq) ultimatelyshow False using‹L M1 = L M2›by blast qed
(* language equivalent minimal FSMs have the same number of reachable states *) lemma minimal_equivalence_size_r : assumes"minimal M1" and"minimal M2" and"observable M1" and"observable M2" and"L M1 = L M2" shows"size_r M1 = size_r M2" using observable_minimal_size_r_language_distinct[OF assms(1-4)]
observable_minimal_size_r_language_distinct[OF assms(2,1,4,3)]
assms(5) using nat_neq_iff by auto
subsection‹Conformity Relations›
fun is_io_reduction_state :: "('a,'b,'c) fsm ==> 'a ==> ('d,'b,'c) fsm ==> 'd ==> bool"where "is_io_reduction_state A a B b = (LS A a ⊆ LS B b)"
abbreviation(input) "is_io_reduction A B ≡ is_io_reduction_state A (initial A) B (initial B)" notation
is_io_reduction (‹_ ⪯ _›)
fun is_io_reduction_state_on_inputs :: "('a,'b,'c) fsm ==> 'a ==> 'b list set ==> ('d,'b,'c) fsm ==> 'd ==> bool"where "is_io_reduction_state_on_inputs A a U B b = (LSin A a U ⊆ LSin B b U)"
abbreviation(input) "is_io_reduction_on_inputs A U B ≡ is_io_reduction_state_on_inputs A (initial A) U B (initial B)" notation
is_io_reduction_on_inputs (‹_ ⪯[_] _›)
subsection‹A Pass Relation for Reduction and Test Represented as Sets of Input-Output Sequences›
definition pass_io_set :: "('a,'b,'c) fsm ==> ('b × 'c) list set ==> bool"where "pass_io_set M ios = (∀ io x y . io@[(x,y)] ∈ ios ⟶ (∀ y' . io@[(x,y')] ∈ L M ⟶io@[(x,y')] ∈ ios))"
definition pass_io_set_maximal :: "('a,'b,'c) fsm ==> ('b × 'c) list set ==> bool"where "pass_io_set_maximal M ios = (∀ io x y io' . io@[(x,y)]@io' ∈ ios ⟶ (∀ y' . io@[(x,y')] ∈ L M ⟶ (∃ io''. io@[(x,y')]@io'' ∈ ios)))"
lemma pass_io_set_from_pass_io_set_maximal : "pass_io_set_maximal M ios = pass_io_set M {io' . ∃ io io'' . io = io'@io'' ∧ io∈ ios}" proof - have"∧ io x y io' . io@[(x,y)]@io' ∈ ios ==> io@[(x,y)] ∈ {io' . ∃ io io'' . io = io'@io'' ∧ io ∈ ios}" by auto moreoverhave"∧ io x y . io@[(x,y)] ∈ {io' . ∃ io io'' . io = io'@io'' ∧ io ∈ ios} ==>∃ io' . io@[(x,y)]@io' ∈ ios" by auto ultimatelyshow ?thesis unfolding pass_io_set_def pass_io_set_maximal_def by meson qed
lemma pass_io_set_maximal_from_pass_io_set : assumes"finite ios" and"∧ io' io'' . io'@io'' ∈ ios ==> io' ∈ ios" shows"pass_io_set M ios = pass_io_set_maximal M {io' ∈ ios . ¬ (∃ io'' . io'' ≠[] ∧ io'@io'' ∈ ios)}" proof - have"∧ io x y . io@[(x,y)] ∈ ios ==>∃ io' . io@[(x,y)]@io' ∈ {io'' ∈ ios . ¬ (∃ io''' . io''' ≠ [] ∧ io''@io''' ∈ ios)}" proof - fix io x y assume"io@[(x,y)] ∈ ios" show"∃ io' . io@[(x,y)]@io' ∈ {io'' ∈ ios . ¬ (∃ io''' . io''' ≠ [] ∧ io''@io'''∈ ios)}" using finite_set_elem_maximal_extension_ex[OF ‹io@[(x,y)] ∈ ios› assms(1)] by force qed moreoverhave"∧ io x y io' . io@[(x,y)]@io' ∈ {io'' ∈ ios . ¬ (∃ io''' . io''' ≠[] ∧ io''@io''' ∈ ios)} ==> io@[(x,y)] ∈ ios" using‹∧ io' io'' . io'@io'' ∈ ios ==> io' ∈ ios›by force ultimatelyshow ?thesis unfolding pass_io_set_def pass_io_set_maximal_def by meson qed
subsection‹Relaxation of IO based test suites to sets of input sequences›
lemma equivalence_io_relaxation : assumes"(L M1 = L M2) ⟷ (L M1 ∩ T = L M2 ∩ T)" shows"(L M1 = L M2) ⟷ ({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')})" proof show"(L M1 = L M2) ==> ({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')})" by blast show"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> L M1 = L M2" proof - have *:"∧ M . {io . io ∈ L M ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = L M ∩ {io . ∃ io' ∈ T . input_portion io = input_portion io'}" by blast
have"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> (L M1 ∩T = L M2 ∩ T)" unfolding * by blast thenshow"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} = {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> L M1 = L M2" using assms by blast qed qed
lemma reduction_io_relaxation : assumes"(L M1 ⊆ L M2) ⟷ (L M1 ∩ T ⊆ L M2 ∩ T)" shows"(L M1 ⊆ L M2) ⟷ ({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')})" proof show"(L M1 ⊆ L M2) ==> ({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')})" by blast show"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> L M1 ⊆ L M2" proof - have *:"∧ M . {io . io ∈ L M ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ L M ∩ {io . ∃ io' ∈ T . input_portion io = input_portion io'}" by blast
have"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> (L M1 ∩T ⊆ L M2 ∩ T)" unfolding * by blast thenshow"({io . io ∈ L M1 ∧ (∃ io' ∈ T . input_portion io = input_portion io')} ⊆ {io . io ∈ L M2 ∧ (∃ io' ∈ T . input_portion io = input_portion io')}) ==> L M1⊆ L M2" using assms by blast qed qed
subsection‹Submachines›
fun is_submachine :: "('a,'b,'c) fsm ==> ('a,'b,'c) fsm ==> bool"where "is_submachine A B = (initial A = initial B ∧ transitions A ⊆ transitions B ∧ inputs A = inputs B ∧ outputs A = outputs B ∧ states A ⊆ states B)"
lemma submachine_path_initial : assumes"is_submachine A B" and"path A (initial A) p" shows"path B (initial B) p" using assms proof (induction p rule: rev_induct) case Nil thenshow ?caseby auto next case (snoc a p) thenshow ?case by fastforce qed
lemma submachine_path : assumes"is_submachine A B" and"path A q p" shows"path B q p" by (meson assms(1) assms(2) is_submachine.elims(2) path_begin_state subsetD transition_subset_path)
lemma submachine_reduction : assumes"is_submachine A B" shows"is_io_reduction A B" using submachine_path[OF assms] assms by auto
lemma complete_submachine_initial : assumes"is_submachine A B" and"completely_specified A" shows"completely_specified_state B (initial B)" using assms(1) assms(2) fsm_initial subset_iff by fastforce
lemma submachine_language : assumes"is_submachine S M" shows"L S ⊆ L M" by (meson assms is_io_reduction_state.elims(2) submachine_reduction)
lemma submachine_observable : assumes"is_submachine S M" and"observable M" shows"observable S" using assms unfolding is_submachine.simps observable.simps by blast
lemma submachine_transitive : assumes"is_submachine S M" and"is_submachine S' S" shows"is_submachine S' M" using assms unfolding is_submachine.simps by force
lemma transitions_subset_path : assumes"set p ⊆ transitions M" and"p ≠ []" and"path S q p" shows"path M q p" using assms by (induction p arbitrary: q; auto)
lemma transition_subset_paths : assumes"transitions S ⊆ transitions M" and"initial S ∈ states M" and"inputs S = inputs M" and"outputs S = outputs M" and"path S (initial S) p" shows"path M (initial S) p" using assms(5) proof (induction p rule: rev_induct) case Nil thenshow ?caseusing assms(2) by auto next case (snoc t p) thenhave"path S (initial S) p" and"t ∈ transitions S" and"t_source t = target (initial S) p" and"path M (initial S) p" by auto
have"t ∈ transitions M" using assms(1) ‹t ∈ transitions S›by auto moreoverhave"t_source t ∈ states M" using‹t_source t = target (initial S) p›‹path M (initial S) p› using path_target_is_state by fastforce ultimatelyhave"t ∈ transitions M" using‹t ∈ transitions S› assms(3,4) by auto thenshow ?case using‹path M (initial S) p› using snoc.prems by auto qed
lemma submachine_reachable_subset : assumes"is_submachine A B" shows"reachable_states A ⊆ reachable_states B" using assms submachine_path_initial[OF assms] unfolding is_submachine.simps reachable_states_def by force
lemma submachine_simps : assumes"is_submachine A B" shows"initial A = initial B" and"states A ⊆ states B" and"inputs A = inputs B" and"outputs A = outputs B" and"transitions A ⊆ transitions B" using assms unfolding is_submachine.simps by blast+
lemma submachine_deadlock : assumes"is_submachine A B" and"deadlock_state B q" shows"deadlock_state A q" using assms(1) assms(2) in_mono by auto
subsection‹Changing Initial States›
lift_definition from_FSM :: "('a,'b,'c) fsm ==> 'a ==> ('a,'b,'c) fsm"is FSM_Impl.from_FSMI by simp
lemma from_FSM_simps[simp]: assumes"q ∈ states M" shows "initial (from_FSM M q) = q" "inputs (from_FSM M q) = inputs M" "outputs (from_FSM M q) = outputs M" "transitions (from_FSM M q) = transitions M" "states (from_FSM M q) = states M"using assms by (transfer; simp)+
lemma from_FSM_path_initial : assumes"q ∈ states M" shows"path M q p = path (from_FSM M q) (initial (from_FSM M q)) p" by (metis assms from_FSM_simps(1) from_FSM_simps(4) from_FSM_simps(5) order_refl
transition_subset_path)
lemma from_FSM_path : assumes"q ∈ states M" and"path (from_FSM M q) q' p" shows"path M q' p" using assms(1) assms(2) path_transitions transitions_subset_path by fastforce
lemma from_FSM_reachable_states : assumes"q ∈ reachable_states M" shows"reachable_states (from_FSM M q) ⊆ reachable_states M" proof from assms obtain p where"path M (initial M) p"and"target (initial M) p = q" unfolding reachable_states_def by blast thenhave"q ∈ states M" by (meson path_target_is_state)
fix q' assume"q' ∈ reachable_states (from_FSM M q)" thenobtain p' where"path (from_FSM M q) q p'"and"target q p' = q'" unfolding reachable_states_def from_FSM_simps[OF ‹q ∈ states M›] by blast thenhave"path M (initial M) (p@p')"and"target (initial M) (p@p') = q'" using from_FSM_path[OF ‹q ∈ states M› ] ‹path M (initial M) p› using‹target (FSM.initial M) p = q›by auto
thenshow"q' ∈ reachable_states M" unfolding reachable_states_def by blast qed
lemma submachine_from : assumes"is_submachine S M" and"q ∈ states S" shows"is_submachine (from_FSM S q) (from_FSM M q)" proof - have"path S q []" using assms(2) by blast thenhave"path M q []" by (meson assms(1) submachine_path) thenshow ?thesis using assms(1) assms(2) by force qed
lemma from_FSM_path_rev_initial : assumes"path M q p" shows"path (from_FSM M q) q p" by (metis (no_types) assms from_FSM_path_initial from_FSM_simps(1) path_begin_state)
lemma from_from[simp] : assumes"q1 ∈ states M" and"q1' ∈ states M" shows"from_FSM (from_FSM M q1) q1' = from_FSM M q1'" (is"?M = ?M'") proof - have *: "q1' ∈ states (from_FSM M q1)" using assms(2) unfolding from_FSM_simps(5)[OF assms(1)] by assumption
lemma from_FSM_completely_specified : assumes"completely_specified M" shows"completely_specified (from_FSM M q)"proof (cases "q ∈ states M") case True thenshow ?thesis using assms by auto next case False thenhave"from_FSM M q = M"by (transfer; auto) thenshow ?thesis using assms by auto qed
lemma from_FSM_single_input : assumes"single_input M" shows"single_input (from_FSM M q)"proof (cases "q ∈ states M") case True thenshow ?thesis using assms by (metis from_FSM_simps(4) single_input.elims(1)) next case False thenhave"from_FSM M q = M"by (transfer; auto) thenshow ?thesis using assms by presburger qed
lemma from_FSM_acyclic : assumes"q ∈ reachable_states M" and"acyclic M" shows"acyclic (from_FSM M q)" using assms(1)
acyclic_paths_from_reachable_states[OF assms(2), of _ q]
from_FSM_path[of q M q]
path_target_is_state
reachable_state_is_state[OF assms(1)]
from_FSM_simps(1) unfolding acyclic.simps
reachable_states_def by force
lemma from_FSM_observable : assumes"observable M" shows"observable (from_FSM M q)" proof (cases "q ∈ states M") case True thenshow ?thesis using assms proof - have f1: "∀f. observable f = (∀a b c aa ab. ((a::'a, b::'b, c::'c, aa) ∉ FSM.transitions f ∨ (a, b, c, ab) ∉ FSM.transitions f) ∨ aa = ab)" by force have"∀a f. a ∉ FSM.states (f::('a, 'b, 'c) fsm) ∨ FSM.transitions (FSM.from_FSM f a) = FSM.transitions f" by (meson from_FSM_simps(4)) thenshow ?thesis using f1 True assms by presburger qed next case False thenhave"from_FSM M q = M"by (transfer; auto) thenshow ?thesis using assms by presburger qed
lemma observable_language_next : assumes"io#ios ∈ LS M (t_source t)" and"observable M" and"t ∈ transitions M" and"t_input t = fst io" and"t_output t = snd io" shows"ios ∈ L (from_FSM M (t_target t))" proof - obtain p where"path M (t_source t) p"and"p_io p = io#ios" using assms(1) proof - assume a1: "∧p. [path M (t_source t) p; p_io p = io # ios]==> thesis" obtain pps :: "('a × 'b) list ==> 'c ==> ('c, 'a, 'b) fsm ==> ('c × 'a × 'b × 'c) list"where "∀x0 x1 x2. (∃v3. x0 = p_io v3 ∧ path x2 x1 v3) = (x0 = p_io (pps x0 x1 x2) ∧ path x2 x1 (pps x0 x1 x2))" by moura thenhave"∃ps. path M (t_source t) ps ∧ p_io ps = io # ios" using assms(1) by auto thenshow ?thesis using a1 by meson qed thenobtain t' p' where"p = t' # p'" by auto thenhave"t' ∈ transitions M"and"t_source t' = t_source t"and"t_input t' = fst io"and"t_output t' = snd io" using‹path M (t_source t) p›‹p_io p = io#ios›by auto thenhave"t = t'" using assms(2,3,4,5) unfolding observable.simps by (metis (no_types, opaque_lifting) prod.expand)
thenhave"path M (t_target t) p'"and"p_io p' = ios" using‹p = t' # p'›‹path M (t_source t) p›‹p_io p = io#ios›by auto thenhave"path (from_FSM M (t_target t)) (initial (from_FSM M (t_target t))) p'" by (meson assms(3) from_FSM_path_initial fsm_transition_target)
thenshow ?thesis using‹p_io p' = ios›by auto qed
lemma from_FSM_language : assumes"q ∈ states M" shows"L (from_FSM M q) = LS M q" using assms unfolding LS.simps by (meson from_FSM_path_initial)
lemma observable_transition_target_language_subset : assumes"LS M (t_source t1) ⊆ LS M (t_source t2)" and"t1 ∈ transitions M" and"t2 ∈ transitions M" and"t_input t1 = t_input t2" and"t_output t1 = t_output t2" and"observable M" shows"LS M (t_target t1) ⊆ LS M (t_target t2)" proof (rule ccontr) assume"¬ LS M (t_target t1) ⊆ LS M (t_target t2)" thenobtain ioF where"ioF ∈ LS M (t_target t1)"and"ioF ∉ LS M (t_target t2)" by blast thenhave"(t_input t1, t_output t1)#ioF ∈ LS M (t_source t1)" using LS_prepend_transition assms(2) by blast thenhave *: "(t_input t1, t_output t1)#ioF ∈ LS M (t_source t2)" using assms(1) by blast
have"ioF ∈ LS M (t_target t2)" using observable_language_next[OF * ‹observable M›‹t2 ∈ transitions M› ] unfolding assms(4,5) fst_conv snd_conv by (metis assms(3) from_FSM_language fsm_transition_target) thenshow False using‹ioF ∉ LS M (t_target t2)›by blast qed
lemma observable_transition_target_language_eq : assumes"LS M (t_source t1) = LS M (t_source t2)" and"t1 ∈ transitions M" and"t2 ∈ transitions M" and"t_input t1 = t_input t2" and"t_output t1 = t_output t2" and"observable M" shows"LS M (t_target t1) = LS M (t_target t2)" using observable_transition_target_language_subset[OF _ assms(2,3,4,5,6)]
observable_transition_target_language_subset[OF _ assms(3,2) assms(4,5)[symmetric] assms(6)]
assms(1) by blast
lemma language_state_prepend_transition : assumes"io ∈ LS (from_FSM A (t_target t)) (initial (from_FSM A (t_target t)))" and"t ∈ transitions A" shows"p_io [t] @ io ∈ LS A (t_source t)" proof - obtain p where"path (from_FSM A (t_target t)) (initial (from_FSM A (t_target t))) p" and"p_io p = io" using assms(1) unfolding LS.simps by blast thenhave"path A (t_target t) p" by (meson assms(2) from_FSM_path_initial fsm_transition_target) thenhave"path A (t_source t) (t # p)" using assms(2) by auto thenshow ?thesis using‹p_io p = io›unfolding LS.simps by force qed
lemma observable_language_transition_target : assumes"observable M" and"t ∈ transitions M" and"(t_input t, t_output t) # io ∈ LS M (t_source t)" shows"io ∈ LS M (t_target t)" by (metis (no_types) assms(1) assms(2) assms(3) from_FSM_language fsm_transition_target fst_conv observable_language_next snd_conv)
lemma LS_single_transition : "[(x,y)] ∈ LS M q ⟷ (∃ t ∈ transitions M . t_source t = q ∧ t_input t = x ∧ t_output t = y)" proof show"[(x, y)] ∈ LS M q ==>∃t∈FSM.transitions M. t_source t = q ∧ t_input t = x ∧ t_output t = y" by auto show"∃t∈FSM.transitions M. t_source t = q ∧ t_input t = x ∧ t_output t = y ==> [(x, y)] ∈ LS M q" by (metis LS_prepend_transition from_FSM_language fsm_transition_target language_contains_empty_sequence) qed
lemma h_obs_language_append : assumes"observable M" and"u ∈ L M" and"h_obs M (after_initial M u) x y ≠ None" shows"u@[(x,y)] ∈ L M" using after_language_iff[OF assms(1,2), of "[(x,y)]"] using h_obs_None[OF assms(1)] assms(3) unfolding LS_single_transition by (metis old.prod.inject prod.collapse)
lemma h_obs_language_single_transition_iff : assumes"observable M" shows"[(x,y)] ∈ LS M q ⟷ h_obs M q x y ≠ None" using h_obs_None[OF assms(1), of q x y] unfolding LS_single_transition by (metis fst_conv prod.exhaust_sel snd_conv)
(* TODO: generalise to non-observable FSMs *) lemma minimal_failure_prefix_ob : assumes"observable M" and"observable I" and"qM ∈ states M" and"qI ∈ states I" and"io ∈ LS I qI - LS M qM" obtains io' xy io'' where"io = io'@[xy]@io''" and"io' ∈ LS I qI ∩ LS M qM" and"io'@[xy] ∈ LS I qI - LS M qM" proof - have"∃ io' xy io'' . io = io'@[xy]@io'' ∧ io' ∈ LS I qI ∩ LS M qM ∧ io'@[xy] ∈ LS I qI - LS M qM" using assms(3,4,5) proof (induction io arbitrary: qM qI) case Nil thenshow ?caseby auto next case (Cons xy io) show ?caseproof (cases "[xy] ∈ LS I qI - LS M qM") case True
have"xy # io = []@[xy]@io" by auto moreoverhave"[] ∈ LS I qI ∩ LS M qM" using‹qM ∈ states M›‹qI ∈ states I›by auto moreoverhave"[]@[xy] ∈ LS I qI - LS M qM" using True by auto ultimatelyshow ?thesis by blast next case False
obtain x y where"xy = (x,y)" by (meson surj_pair)
have"[(x,y)] ∈ LS M qM" using‹xy = (x,y)› False ‹xy # io ∈ LS I qI - LS M qM› by (metis DiffD1 DiffI append_Cons append_Nil language_prefix) thenobtain qM' where"(qM,x,y,qM') ∈ transitions M" by auto thenhave"io ∉ LS M qM'" using observable_language_transition_target[OF ‹observable M›] ‹xy = (x,y)›‹xy # io ∈ LS I qI - LS M qM› by (metis DiffD2 LS_prepend_transition fst_conv snd_conv)
have"[(x,y)] ∈ LS I qI" using‹xy = (x,y)›‹xy # io ∈ LS I qI - LS M qM› by (metis DiffD1 append_Cons append_Nil language_prefix) thenobtain qI' where"(qI,x,y,qI') ∈ transitions I" by auto thenhave"io ∈ LS I qI'" using observable_language_next[of xy io I "(qI,x,y,qI')", OF _ ‹observable I›] ‹xy # io ∈ LS I qI - LS M qM› fsm_transition_target[OF ‹(qI,x,y,qI') ∈ transitions I›] unfolding‹xy = (x,y)› fst_conv snd_conv by (metis DiffD1 from_FSM_language)
obtain io' xy' io'' where"io = io'@[xy']@io''"and"io' ∈ LS I qI' ∩ LS M qM'"and"io'@[xy'] ∈ LS I qI' - LS M qM'" using‹io ∈ LS I qI'›‹io ∉ LS M qM'›
Cons.IH[OF fsm_transition_target[OF ‹(qM,x,y,qM') ∈ transitions M›]
fsm_transition_target[OF ‹(qI,x,y,qI') ∈ transitions I›] ] unfolding fst_conv snd_conv by blast
have"xy#io = (xy#io')@[xy']@io''" using‹io = io'@[xy']@io''›‹xy = (x,y)›by auto moreoverhave"xy#io' ∈ LS I qI ∩ LS M qM" using LS_prepend_transition[OF ‹(qI,x,y,qI') ∈ transitions I›, of io'] using LS_prepend_transition[OF ‹(qM,x,y,qM') ∈ transitions M›, of io'] using‹io' ∈ LS I qI' ∩ LS M qM'› unfolding‹xy = (x,y)› fst_conv snd_conv by auto moreoverhave"(xy#io')@[xy'] ∈ LS I qI - LS M qM" using LS_prepend_transition[OF ‹(qI,x,y,qI') ∈ transitions I›, of "io'@[xy']"] using observable_language_transition_target[OF ‹observable M›‹(qM,x,y,qM') ∈ transitions M›, of "io'@[xy']"] using‹io'@[xy'] ∈ LS I qI' - LS M qM'› unfolding‹xy = (x,y)› fst_conv snd_conv by fastforce ultimatelyshow ?thesis by blast qed qed thenshow ?thesis using that by blast qed
subsection‹Language and Defined Inputs›
lemma defined_inputs_code : "defined_inputs M q = t_input ` Set.filter (λt . t_source t = q) (transitions M)" unfolding defined_inputs_set by force
lemma defined_inputs_alt_def : "defined_inputs M q = {t_input t | t . t ∈ transitions M ∧ t_source t = q}" unfolding defined_inputs_code by force
lemma defined_inputs_language_diff : assumes"x ∈ defined_inputs M1 q1" and"x ∉ defined_inputs M2 q2" obtains y where"[(x,y)] ∈ LS M1 q1 - LS M2 q2" using assms unfolding defined_inputs_alt_def proof - assume a1: "x ∉ {t_input t |t. t ∈ FSM.transitions M2 ∧ t_source t = q2}" assume a2: "x ∈ {t_input t |t. t ∈ FSM.transitions M1 ∧ t_source t = q1}" assume a3: "∧y. [(x, y)] ∈ LS M1 q1 - LS M2 q2 ==> thesis" have f4: "∄p. x = t_input p ∧ p ∈ FSM.transitions M2 ∧ t_source p = q2" using a1 by blast obtain pp :: "'a ==> 'b × 'a × 'c × 'b"where "∀a. ((∄p. a = t_input p ∧ p ∈ FSM.transitions M1 ∧ t_source p = q1) ∨ a = t_input (pp a) ∧ pp a ∈ FSM.transitions M1 ∧ t_source (pp a) = q1) ∧ ((∃p. a = t_input p ∧ p ∈ FSM.transitions M1 ∧ t_source p = q1) ∨ (∀p. a ≠ t_input p ∨ p ∉ FSM.transitions M1 ∨ t_source p ≠ q1))" by moura thenhave"x = t_input (pp x) ∧ pp x ∈ FSM.transitions M1 ∧ t_source (pp x) = q1" using a2 by blast thenshow ?thesis using f4 a3 by (metis (no_types) DiffI LS_single_transition) qed
lemma language_path_append : assumes"path M1 q1 p1" and"io ∈ LS M1 (target q1 p1)" shows"(p_io p1 @ io) ∈ LS M1 q1" proof - obtain p2 where"path M1 (target q1 p1) p2"and"p_io p2 = io" using assms(2) by auto thenhave"path M1 q1 (p1@p2)" using assms(1) by auto moreoverhave"p_io (p1@p2) = (p_io p1 @ io)" using‹p_io p2 = io›by auto ultimatelyshow ?thesis by (metis (mono_tags, lifting) language_intro) qed
lemma observable_defined_inputs_diff_ob : assumes"observable M1" and"observable M2" and"path M1 q1 p1" and"path M2 q2 p2" and"p_io p1 = p_io p2" and"x ∈ defined_inputs M1 (target q1 p1)" and"x ∉ defined_inputs M2 (target q2 p2)" obtains y where"(p_io p1)@[(x,y)] ∈ LS M1 q1 - LS M2 q2" proof - obtain y where"[(x,y)] ∈ LS M1 (target q1 p1) - LS M2 (target q2 p2)" using defined_inputs_language_diff[OF assms(6,7)] by blast thenhave"(p_io p1)@[(x,y)] ∈ LS M1 q1" using language_path_append[OF assms(3)] by blast moreoverhave"(p_io p1)@[(x,y)] ∉ LS M2 q2" by (metis (mono_tags, lifting) DiffD2 ‹[(x, y)] ∈ LS M1 (target q1 p1) - LS M2 (target q2 p2)› assms(2) assms(4) assms(5) language_state_containment observable_path_suffix) ultimatelyshow ?thesis using that[of y] by blast qed
lemma observable_defined_inputs_diff_language : assumes"observable M1" and"observable M2" and"path M1 q1 p1" and"path M2 q2 p2" and"p_io p1 = p_io p2" and"defined_inputs M1 (target q1 p1) ≠ defined_inputs M2 (target q2 p2)" shows"LS M1 q1 ≠ LS M2 q2" proof - obtain x where"(x ∈ defined_inputs M1 (target q1 p1) - defined_inputs M2 (target q2 p2)) ∨ (x ∈ defined_inputs M2 (target q2 p2) - defined_inputs M1 (target q1 p1))" using assms by blast then consider "(x ∈ defined_inputs M1 (target q1 p1) - defined_inputs M2 (target q2 p2))" | "(x ∈ defined_inputs M2 (target q2 p2) - defined_inputs M1 (target q1 p1))" by blast thenshow ?thesis proof cases case1 thenshow ?thesis using observable_defined_inputs_diff_ob[OF assms(1-5), of x] by blast next case2 thenshow ?thesis using observable_defined_inputs_diff_ob[OF assms(2,1,4,3) assms(5)[symmetric], of x] by blast qed qed
fun maximal_prefix_in_language :: "('a,'b,'c) fsm ==> 'a ==> ('b ×'c) list ==> ('b ×'c) list"where "maximal_prefix_in_language M q [] = []" | "maximal_prefix_in_language M q ((x,y)#io) = (case h_obs M q x y of None ==> [] | Some q' ==> (x,y)#maximal_prefix_in_language M q' io)"
lemma maximal_prefix_in_language_properties : assumes"observable M" and"q ∈ states M" shows"maximal_prefix_in_language M q io ∈ LS M q" and"maximal_prefix_in_language M q io ∈ list.set (prefixes io)" proof - have"maximal_prefix_in_language M q io ∈ LS M q ∧ maximal_prefix_in_language M q io ∈ list.set (prefixes io)" using assms(2) proof (induction io arbitrary: q) case Nil thenshow ?caseby auto next case (Cons xy io)
obtain x y where"xy = (x,y)" using prod.exhaust by metis
show ?caseproof (cases "h_obs M q x y") case None thenhave"maximal_prefix_in_language M q (xy#io) = []" unfolding‹xy = (x,y)› by auto thenshow ?thesis by (metis (mono_tags, lifting) Cons.prems append_self_conv2 from_FSM_language language_contains_empty_sequence mem_Collect_eq prefixes_set) next case (Some q') thenhave *: "maximal_prefix_in_language M q (xy#io) = (x,y)#maximal_prefix_in_language M q' io" unfolding‹xy = (x,y)› by auto
have"q' ∈ states M" using h_obs_state[OF Some] by auto thenhave"maximal_prefix_in_language M q' io ∈ LS M q'" and"maximal_prefix_in_language M q' io ∈ list.set (prefixes io)" using Cons.IH by auto
have"maximal_prefix_in_language M q (xy # io) ∈ LS M q" unfolding * using Some ‹maximal_prefix_in_language M q' io ∈ LS M q'› by (meson assms(1) h_obs_language_iff) moreoverhave"maximal_prefix_in_language M q (xy # io) ∈ list.set (prefixes (xy # io))" unfolding * unfolding‹xy = (x,y)› using‹maximal_prefix_in_language M q' io ∈ list.set (prefixes io)› append_Cons unfolding prefixes_set by auto ultimatelyshow ?thesis by blast qed qed thenshow"maximal_prefix_in_language M q io ∈ LS M q" and"maximal_prefix_in_language M q io ∈ list.set (prefixes io)" by auto qed
subsection‹Further Reachability Formalisations›
(* states that are reachable in at most k transitions *) fun reachable_k :: "('a,'b,'c) fsm ==> 'a ==> nat ==> 'a set"where "reachable_k M q n = {target q p | p . path M q p ∧ length p ≤ n}"
lemma reachable_k_0_initial : "reachable_k M (initial M) 0 = {initial M}" by auto
lemma reachable_k_states : "reachable_states M = reachable_k M (initial M) ( size M - 1)" proof - have"∧q. q ∈ reachable_states M ==> q ∈ reachable_k M (initial M) ( size M - 1)" proof - fix q assume"q ∈ reachable_states M" thenobtain p where"path M (initial M) p"and"target (initial M) p = q" unfolding reachable_states_def by blast thenobtain p' where"path M (initial M) p'" and"target (initial M) p' = target (initial M) p" and"length p' < size M" by (metis acyclic_path_from_cyclic_path acyclic_path_length_limit) thenshow"q ∈ reachable_k M (initial M) ( size M - 1)" using‹target (FSM.initial M) p = q› less_trans by auto qed
moreoverhave"∧x. x ∈ reachable_k M (initial M) ( size M - 1) ==> x ∈ reachable_states M" unfolding reachable_states_def reachable_k.simps by blast
ultimatelyshow ?thesis by blast qed
subsubsection‹Induction Schemes›
lemma acyclic_induction [consumes 1, case_names reachable_state]: assumes"acyclic M" and"∧ q . q ∈ reachable_states M ==> (∧ t . t ∈ transitions M ==> ((t_source t = q) ==> P (t_target t))) ==> P q" shows"∀ q ∈ reachable_states M . P q" proof fix q assume"q ∈ reachable_states M"
let ?k = "Max (image length {p . path M q p})" have"finite {p . path M q p}"using acyclic_finite_paths_from_reachable_state[OF assms(1)] using‹q ∈ reachable_states M›unfolding reachable_states_def by force thenhave k_prop: "(∀ p . path M q p ⟶ length p ≤ ?k)"by auto
moreoverhave"∧ q k . q ∈ reachable_states M ==> (∀ p . path M q p ⟶ length p ≤ k) ==> P q" proof - fix q k assume"q ∈ reachable_states M"and"(∀ p . path M q p ⟶ length p ≤ k)" thenshow"P q" proof (induction k arbitrary: q) case0 thenhave"{p . path M q p} = {[]}"using reachable_state_is_state[OF ‹q ∈ reachable_states M›] by blast thenhave"LS M q ⊆ {[]}"unfolding LS.simps by blast thenhave"deadlock_state M q"using deadlock_state_alt_def by metis thenshow ?caseusing assms(2)[OF ‹q ∈ reachable_states M›] unfolding deadlock_state.simps by blast next case (Suc k) have"∧ t . t ∈ transitions M ==> (t_source t = q) ==> P (t_target t)" proof - fix t assume"t ∈ transitions M"and"t_source t = q" thenhave"t_target t ∈ reachable_states M" using‹q ∈ reachable_states M›using reachable_states_next by metis moreoverhave"∀p. path M (t_target t) p ⟶ length p ≤ k" using Suc.prems(2) ‹t ∈ transitions M›‹t_source t = q›by auto ultimatelyshow"P (t_target t)" using Suc.IH unfolding reachable_states_def by blast qed thenshow ?caseusing assms(2)[OF Suc.prems(1)] by blast qed qed
ultimatelyshow"P q"using‹q ∈ reachable_states M›by blast qed
lemma reachable_states_induct [consumes 1, case_names init transition] : assumes"q ∈ reachable_states M" and"P (initial M)" and"∧ t . t ∈ transitions M ==> t_source t ∈ reachable_states M ==> P (t_source t) ==> P (t_target t)" shows"P q" proof - from assms(1) obtain p where"path M (initial M) p"and"target (initial M) p = q" unfolding reachable_states_def by auto thenshow"P q" proof (induction p arbitrary: q rule: rev_induct) case Nil thenshow ?caseusing assms(2) by auto next case (snoc t p)
thenhave"target (initial M) p = t_source t" by auto thenhave"P (t_source t)" using snoc.IH snoc.prems by auto moreoverhave"t ∈ transitions M" using snoc.prems by auto moreoverhave"t_source t ∈ reachable_states M" by (metis ‹target (FSM.initial M) p = t_source t› path_prefix reachable_states_intro snoc.prems(1)) moreoverhave"t_target t = q" using snoc.prems by auto ultimatelyshow ?case using assms(3) by blast qed qed
lemma reachable_states_cases [consumes 1, case_names init transition] : assumes"q ∈ reachable_states M" and"P (initial M)" and"∧ t . t ∈ transitions M ==> t_source t ∈ reachable_states M ==> P (t_target t)" shows"P q" by (metis assms(1) assms(2) assms(3) reachable_states_induct)
subsection‹Further Path Enumeration Algorithms›
fun paths_for_input' :: "('a ==> ('b × 'c × 'a) set) ==> 'b list ==> 'a ==> ('a,'b,'c) path ==> ('a,'b,'c) path set"where "paths_for_input' f [] q prev = {prev}" | "paths_for_input' f (x#xs) q prev = ∪(image (λ(x',y',q') . paths_for_input' f xs q' (prev@[(q,x,y',q')])) (Set.filter (λ(x',y',q') . x' = x) (f q)))"
lemma paths_for_input'_set : assumes"q ∈ states M" shows"paths_for_input' (h_from M) xs q prev = {prev@p | p . path M q p ∧ map fst (p_io p) = xs}" using assms proof (induction xs arbitrary: q prev) case Nil thenshow ?caseby auto next case (Cons x xs)
let ?UN = "∪(image (λ(x',y',q') . paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])) (Set.filter (λ(x',y',q') . x' = x) (h_from M q)))"
have"?UN = {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" proof have"∧ p . p ∈ ?UN ==> p ∈ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" proof - fix p assume"p ∈ ?UN" thenobtain y' q' where"(x,y',q') ∈ (Set.filter (λ(x',y',q') . x' = x) (h_from M q))" and"p ∈ paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])" by auto
from‹(x,y',q') ∈ (Set.filter (λ(x',y',q') . x' = x) (h_from M q))›have"q' ∈ states M"and"(q,x,y',q') ∈ transitions M" using fsm_transition_target unfolding h.simps by auto
have"p ∈ {(prev @ [(q, x, y', q')]) @ p |p. path M q' p ∧ map fst (p_io p) = xs}" using‹p ∈ paths_for_input' (h_from M) xs q' (prev@[(q,x,y',q')])› unfolding Cons.IH[OF ‹q' ∈ states M›] by assumption moreoverhave"{(prev @ [(q, x, y', q')]) @ p |p. path M q' p ∧ map fst (p_io p) = xs} ⊆ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" using‹(q,x,y',q') ∈ transitions M› using cons by force ultimatelyshow"p ∈ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" by blast qed thenshow"?UN ⊆ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" by blast
have"∧ p . p ∈ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs} ==> p ∈ ?UN" proof - fix pp assume"pp ∈ {prev@p | p . path M q p ∧ map fst (p_io p) = x#xs}" thenobtain p where"pp = prev@p"and"path M q p"and"map fst (p_io p) = x#xs" by fastforce thenobtain t p' where"p = t#p'"and"path M q (t#p')"and"map fst (p_io (t#p')) = x#xs"and"map fst (p_io p') = xs" by (metis (no_types, lifting) map_eq_Cons_D) thenhave"path M (t_target t) p'"and"t_source t = q"and"t_input t = x"and"t_target t ∈ states M"and"t ∈ transitions M" by auto
have"(x,t_output t,t_target t) ∈ (Set.filter (λ(x',y',q') . x' = x) (h_from M q))" using‹t ∈ transitions M›‹t_input t = x›‹t_source t = q› unfolding h.simps by auto moreoverhave"(prev@p) ∈ paths_for_input' (h_from M) xs (t_target t) (prev@[(q,x,t_output t,t_target t)])" using Cons.IH[OF ‹t_target t ∈ states M›, of "prev@[(q, x, t_output t, t_target t)]"] using‹∧thesis. (∧t p'. [p = t # p'; path M q (t # p'); map fst (p_io (t # p')) = x # xs; map fst (p_io p') = xs]==> thesis) ==> thesis› ‹p = t # p'› ‹paths_for_input' (h_from M) xs (t_target t) (prev @ [(q, x, t_output t, t_target t)])
= {(prev @ [(q, x, t_output t, t_target t)]) @ p |p. path M (t_target t) p ∧ map fst (p_io p) = xs}› ‹t_input t = x› ‹t_source t = q› by fastforce
ultimatelyshow"pp ∈ ?UN"unfolding‹pp = prev@p› by blast qed thenshow"{prev@p | p . path M q p ∧ map fst (p_io p) = x#xs} ⊆ ?UN" by (meson subsetI) qed
thenshow ?case by (metis paths_for_input'.simps(2))
qed
definition paths_for_input :: "('a,'b,'c) fsm ==> 'a ==> 'b list ==> ('a,'b,'c) path set"where "paths_for_input M q xs = {p . path M q p ∧ map fst (p_io p) = xs}"
lemma paths_for_input_set_code[code] : "paths_for_input M q xs = (if q ∈ states M then paths_for_input' (h_from M) xs q [] else {})" using paths_for_input'_set[of q M xs "[]"] unfolding paths_for_input_def by (cases "q ∈ states M"; auto; simp add: path_begin_state)
fun paths_up_to_length_or_condition_with_witness' :: "('a ==> ('b × 'c × 'a) set) ==> (('a,'b,'c) path ==> 'd option) ==> ('a,'b,'c) path ==> nat ==> 'a ==> (('a,'b,'c) path × 'd) set" where "paths_up_to_length_or_condition_with_witness' f P prev 0 q = (case P prev of Some w ==> {(prev,w)} | None ==> {})" | "paths_up_to_length_or_condition_with_witness' f P prev (Suc k) q = (case P prev of Some w ==> {(prev,w)} | None ==> (∪(image (λ(x,y,q') . paths_up_to_length_or_condition_with_witness' f P (prev@[(q,x,y,q')]) k q') (f q))))"
lemma paths_up_to_length_or_condition_with_witness'_set : assumes"q ∈ states M" shows"paths_up_to_length_or_condition_with_witness' (h_from M) P prev k q = {(prev@p,x) | p x . path M q p ∧ length p ≤ k ∧ P (prev@p) = Some x ∧ (∀ p' p'' . (p = p'@p'' ∧ p'' ≠ []) ⟶ P (prev@p') = None)}" using assms proof (induction k arbitrary: q prev) case0 thenshow ?caseproof (cases "P prev") case None thenshow ?thesis by auto next case (Some w) thenshow ?thesis by (simp add: "0.prems" nil) qed next case (Suc k) thenshow ?caseproof (cases "P prev") case (Some w) thenhave"(prev,w) ∈ {(prev@p,x) | p x . path M q p ∧ length p ≤ Suc k ∧ P (prev@p) = Some x ∧ (∀ p' p'' . (p = p'@p'' ∧ p'' ≠ []) ⟶ P (prev@p') = None)}" by (simp add: Suc.prems nil) thenhave"{(prev@p,x) | p x . path M q p ∧ length p ≤ Suc k ∧ P (prev@p) = Some x ∧ (∀ p' p'' . (p = p'@p'' ∧ p'' ≠ []) ⟶ P (prev@p') = None)} = {(prev,w)}" using Some by fastforce
thenshow ?thesis using Some by auto next case None
have"(∪(image (λ(x,y,q') . paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q') (h_from M q))) = {(prev@p,x) | p x . path M q p ∧ length p ≤ Suc k ∧ P (prev@p) = Some x ∧ (∀ p' p'' . (p = p'@p'' ∧ p'' ≠ []) ⟶ P (prev@p') = None)}"
(is"?UN = ?PX") proof - have *: "∧ pp . pp ∈ ?UN ==> pp ∈ ?PX" proof - fix pp assume"pp ∈ ?UN" thenobtain x y q' where"(x,y,q') ∈ h_from M q" and"pp ∈ paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q'" by blast thenhave"(q,x,y,q') ∈ transitions M"by auto thenhave"q' ∈ states M"using fsm_transition_target by auto
obtain p w where"pp = ((prev@[(q,x,y,q')])@p,w)" and"path M q' p" and"length p ≤ k" and"P ((prev @ [(q, x, y, q')]) @ p) = Some w" and"∧ p' p''. p = p' @ p'' ==> p'' ≠ [] ==> P ((prev @ [(q, x, y, q')]) @ p') = None" using‹pp ∈ paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[(q,x,y,q')]) k q'› unfolding Suc.IH[OF ‹q' ∈ states M›, of "prev@[(q,x,y,q')]"] by blast
have"path M q ((q,x,y,q')#p)" using‹path M q' p›‹(q,x,y,q') ∈ transitions M›by (simp add: path_prepend_t) moreoverhave"length ((q,x,y,q')#p) ≤ Suc k" using‹length p ≤ k›by auto moreoverhave"P (prev @ ([(q, x, y, q')] @ p)) = Some w" using‹P ((prev @ [(q, x, y, q')]) @ p) = Some w›by auto moreoverhave"∧ p' p''. ((q,x,y,q')#p) = p' @ p'' ==> p'' ≠ [] ==> P (prev @ p') = None" using‹∧ p' p''. p = p' @ p'' ==> p'' ≠ [] ==> P ((prev @ [(q, x, y, q')]) @ p') = None› using None by (metis (no_types, opaque_lifting) append.simps(1) append_Cons append_Nil2 append_assoc
list.inject neq_Nil_conv)
ultimatelyshow"pp ∈ ?PX" unfolding‹pp = ((prev@[(q,x,y,q')])@p,w)›by auto qed
have **: "∧ pp . pp ∈ ?PX ==> pp ∈ ?UN" proof - fix pp assume"pp ∈ ?PX" thenobtain p' w where"pp = (prev @ p', w)" and"path M q p'" and"length p' ≤ Suc k" and"P (prev @ p') = Some w" and"∧ p' p''. p' = p' @ p'' ==> p'' ≠ [] ==> P (prev @ p') = None" by blast moreoverobtain t p where"p' = t#p"using‹P (prev @ p') = Some w›using None by (metis append_Nil2 list.exhaust option.distinct(1))
have"pp = ((prev @ [t])@p, w)" using‹pp = (prev @ p', w)›unfolding‹p' = t#p›by auto have"path M q (t#p)" using‹path M q p'›unfolding‹p' = t#p›by auto have p2: "length (t#p) ≤ Suc k" using‹length p' ≤ Suc k›unfolding‹p' = t#p›by auto have p3: "P ((prev @ [t])@p) = Some w" using‹P (prev @ p') = Some w›unfolding‹p' = t#p›by auto have p4: "∧ p' p''. p = p' @ p'' ==> p'' ≠ [] ==> P ((prev@[t]) @ p') = None" using‹∧ p' p''. p' = p' @ p'' ==> p'' ≠ [] ==> P (prev @ p') = None›‹pp ∈ ?PX› unfolding‹pp = ((prev @ [t]) @ p, w)›‹p' = t#p› by auto
have"t ∈ transitions M"and p1: "path M (t_target t) p"and"t_source t = q" using‹path M q (t#p)›by auto thenhave"t_target t ∈ states M" and"(t_input t, t_output t, t_target t) ∈ h_from M q" and"t_source t = q" using fsm_transition_target by auto thenhave"t = (q,t_input t, t_output t, t_target t)" by auto
have"((prev @ [t])@p, w) ∈ paths_up_to_length_or_condition_with_witness' (h_from M) P (prev@[t]) k (t_target t)" unfolding Suc.IH[OF ‹t_target t ∈ states M›, of "prev@[t]"] using p1 p2 p3 p4 by auto
thenshow"pp ∈ ?UN" unfolding‹pp = ((prev @ [t])@p, w)› proof - have"paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [t]) k (t_target t) = paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [(q, t_input t, t_output t, t_target t)]) k (t_target t)" using‹t = (q, t_input t, t_output t, t_target t)›by presburger thenshow"((prev @ [t]) @ p, w) ∈ (∪(b, c, a)∈h_from M q. paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [(q, b, c, a)]) k a)" using‹((prev @ [t]) @ p, w) ∈ paths_up_to_length_or_condition_with_witness' (h_from M) P (prev @ [t]) k (t_target t)› ‹(t_input t, t_output t, t_target t) ∈ h_from M q› by blast qed qed
show ?thesis using subsetI[of ?UN ?PX, OF *] subsetI[of ?PX ?UN, OF **] subset_antisym by blast qed
thenshow ?thesis using None unfolding paths_up_to_length_or_condition_with_witness'.simps by simp qed qed
definition paths_up_to_length_or_condition_with_witness :: "('a,'b,'c) fsm ==> (('a,'b,'c) path ==> 'd option) ==> nat ==> 'a ==> (('a,'b,'c) path × 'd) set" where "paths_up_to_length_or_condition_with_witness M P k q = {(p,x) | p x . path M q p ∧ length p ≤ k ∧ P p = Some x ∧ (∀ p' p'' . (p = p'@p'' ∧ p'' ≠ []) ⟶ P p' = None)}"
lemma paths_up_to_length_or_condition_with_witness_code[code] : "paths_up_to_length_or_condition_with_witness M P k q = (if q ∈ states M then paths_up_to_length_or_condition_with_witness' (h_from M) P [] k q else {})" proof (cases "q ∈ states M") case True thenshow ?thesis unfolding paths_up_to_length_or_condition_with_witness_def
paths_up_to_length_or_condition_with_witness'_set[OF True] by auto next case False thenshow ?thesis unfolding paths_up_to_length_or_condition_with_witness_def using path_begin_state by fastforce qed
lemma paths_up_to_length_or_condition_with_witness_finite : "finite (paths_up_to_length_or_condition_with_witness M P k q)" proof - have"paths_up_to_length_or_condition_with_witness M P k q ⊆ {(p, the (P p)) | p . path M q p ∧ length p ≤ k}" unfolding paths_up_to_length_or_condition_with_witness_def by auto moreoverhave"finite {(p, the (P p)) | p . path M q p ∧ length p ≤ k}" using paths_finite[of M q k] by simp ultimatelyshow ?thesis using rev_finite_subset by auto qed
subsection‹More Acyclicity Properties›
lemma maximal_path_target_deadlock : assumes"path M (initial M) p" and"¬(∃ p' . path M (initial M) p' ∧ is_prefix p p' ∧ p ≠ p')" shows"deadlock_state M (target (initial M) p)" proof - have"¬(∃ t ∈ transitions M . t_source t = target (initial M) p)" using assms(2) unfolding is_prefix_prefix by (metis append_Nil2 assms(1) not_Cons_self2 path_append_transition same_append_eq) thenshow ?thesis by auto qed
lemma path_to_deadlock_is_maximal : assumes"path M (initial M) p" and"deadlock_state M (target (initial M) p)" shows"¬(∃ p' . path M (initial M) p' ∧ is_prefix p p' ∧ p ≠ p')" proof assume"∃p'. path M (initial M) p' ∧ is_prefix p p' ∧ p ≠ p'" thenobtain p' where"path M (initial M) p'"and"is_prefix p p'"and"p ≠ p'"by blast thenhave"length p' > length p" unfolding is_prefix_prefix by auto thenobtain t p2 where"p' = p @ [t] @ p2" using‹is_prefix p p'›unfolding is_prefix_prefix by (metis ‹p ≠ p'› append.left_neutral append_Cons append_Nil2 non_sym_dist_pairs'.cases) thenhave"path M (initial M) (p@[t])" using‹path M (initial M) p'›by auto thenhave"t ∈ transitions M"and"t_source t = target (initial M) p" by auto thenshow"False" using‹deadlock_state M (target (initial M) p)›unfolding deadlock_state.simps by blast qed
definition maximal_acyclic_paths :: "('a,'b,'c) fsm ==> ('a,'b,'c) path set"where "maximal_acyclic_paths M = {p . path M (initial M) p ∧ distinct (visited_states (initial M) p) ∧¬(∃ p' . p' ≠ [] ∧ path M (initial M) (p@p') ∧ distinct (visited_states (initial M) (p@p')))}"
(* very inefficient construction *) lemma maximal_acyclic_paths_code[code] : "maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (initial M) (size M - 1) in Set.filter (λp . ¬ (∃ p' ∈ ps . p' ≠ p ∧ is_prefix p p')) ps)" proof - have scheme1: "∧ P p . (∃ p' . p' ≠ [] ∧ P (p@p')) = (∃ p' ∈ {p . P p} . p' ≠ p ∧is_prefix p p')" unfolding is_prefix_prefix by blast
have scheme2: "∧ p . (path M (FSM.initial M) p ∧ length p ≤ FSM.size M - 1 ∧ distinct (visited_states (FSM.initial M) p)) = (path M (FSM.initial M) p ∧ distinct (visited_states (FSM.initial M) p))" using acyclic_path_length_limit by fastforce
show ?thesis unfolding maximal_acyclic_paths_def acyclic_paths_up_to_length.simps Let_def unfolding scheme1[of "λp . path M (initial M) p ∧ distinct (visited_states (initial M) p)"] unfolding scheme2 by fastforce qed
lemma maximal_acyclic_path_deadlock : assumes"acyclic M" and"path M (initial M) p" shows"¬(∃ p' . p' ≠ [] ∧ path M (initial M) (p@p') ∧ distinct (visited_states (initial M) (p@p'))) = deadlock_state M (target (initial M) p)" proof - have"deadlock_state M (target (initial M) p) ==>¬(∃ p' . p' ≠ [] ∧ path M (initial M) (p@p') ∧ distinct (visited_states (initial M) (p@p')))" unfolding deadlock_state.simps using assms(2) by (metis path.cases path_suffix) thenshow ?thesis by (metis acyclic.elims(2) assms(1) assms(2) is_prefix_prefix maximal_path_target_deadlock
self_append_conv) qed
lemma maximal_acyclic_paths_deadlock_targets : assumes"acyclic M" shows"maximal_acyclic_paths M = { p . path M (initial M) p ∧ deadlock_state M (target (initial M) p)}" using maximal_acyclic_path_deadlock[OF assms] unfolding maximal_acyclic_paths_def by (metis (no_types, lifting) acyclic.elims(2) assms)
lemma cycle_from_cyclic_path : assumes"path M q p" and"¬ distinct (visited_states q p)" obtains i j where "take j (drop i p) ≠ []" "target (target q (take i p)) (take j (drop i p)) = (target q (take i p))" "path M (target q (take i p)) (take j (drop i p))" proof - obtain i j where"i < j"and"j < length (visited_states q p)" and"(visited_states q p) ! i = (visited_states q p) ! j" using assms(2) non_distinct_repetition_indices by blast
thenhave"(target q (take i p)) = (visited_states q p) ! j" using‹(visited_states q p) ! i = (visited_states q p) ! j›by auto
have p1: "take (j-i) (drop i p) ≠ []" using‹i < j›‹j < length (visited_states q p)›by auto
have"target (target q (take i p)) (take (j-i) (drop i p)) = (target q (take j p))" using‹i < j›by (metis add_diff_inverse_nat less_asym' path_append_target take_add) thenhave p2: "target (target q (take i p)) (take (j-i) (drop i p)) = (target q (take i p))" using‹(target q (take i p)) = (visited_states q p) ! i› using‹(target q (take i p)) = (visited_states q p) ! j› by (metis ‹j < length (visited_states q p)› take_last_index target.simps visited_states_take)
have p3: "path M (target q (take i p)) (take (j-i) (drop i p))" by (metis append_take_drop_id assms(1) path_append_elim)
show ?thesis using p1 p2 p3 that by blast qed
lemma acyclic_single_deadlock_reachable : assumes"acyclic M" and"∧ q' . q' ∈ reachable_states M ==> q' = qd ∨¬ deadlock_state M q'" shows"qd ∈ reachable_states M" using acyclic_deadlock_reachable[OF assms(1)] using assms(2) by auto
lemma acyclic_paths_to_single_deadlock : assumes"acyclic M" and"∧ q' . q' ∈ reachable_states M ==> q' = qd ∨¬ deadlock_state M q'" and"q ∈ reachable_states M" obtains p where"path M q p"and"target q p = qd" proof - have"q ∈ states M"using assms(3) reachable_state_is_state by metis have"acyclic (from_FSM M q)" using from_FSM_acyclic[OF assms(3,1)] by assumption
have *: "(∧q'. q' ∈ reachable_states (FSM.from_FSM M q) ==> q' = qd ∨¬ deadlock_state (FSM.from_FSM M q) q')" using assms(2) from_FSM_reachable_states[OF assms(3)] unfolding deadlock_state.simps from_FSM_simps[OF ‹q ∈ states M›] by blast
obtain p where"path (from_FSM M q) q p"and"target q p = qd" using acyclic_single_deadlock_reachable[OF ‹acyclic (from_FSM M q)› *] unfolding reachable_states_def from_FSM_simps[OF ‹q ∈ states M›] by blast
thenshow ?thesis using that by (metis ‹q ∈ FSM.states M› from_FSM_path) qed
subsection‹Elements as Lists›
fun states_as_list :: "('a :: linorder, 'b, 'c) fsm ==> 'a list"where "states_as_list M = sorted_list_of_set (states M)"
lemma states_as_list_distinct : "distinct (states_as_list M)"by auto
lemma states_as_list_set : "set (states_as_list M) = states M" by (simp add: fsm_states_finite)
fun reachable_states_as_list :: "('a :: linorder, 'b, 'c) fsm ==> 'a list"where "reachable_states_as_list M = sorted_list_of_set (reachable_states M)"
fun fstates :: "('a :: linorder,'b,'c) fsm ==> 'a fset"where "fstates M = fset_of_list (states_as_list M)"
fun finputs :: "('a,'b :: linorder,'c) fsm ==> 'b fset"where "finputs M = fset_of_list (inputs_as_list M)"
fun foutputs :: "('a,'b,'c :: linorder) fsm ==> 'c fset"where "foutputs M = fset_of_list (outputs_as_list M)"
lemma fstates_set : "fset (fstates M) = states M" using fsm_states_finite[of M] by (simp add: fset_of_list.rep_eq)
lemma finputs_set : "fset (finputs M) = inputs M" using fsm_inputs_finite[of M] by (simp add: fset_of_list.rep_eq)
lemma foutputs_set : "fset (foutputs M) = outputs M" using fsm_outputs_finite[of M] by (simp add: fset_of_list.rep_eq)
lemma ftransitions_set: "fset (ftransitions M) = transitions M" by (metis (no_types) fset_of_list.rep_eq ftransitions.simps transitions_as_list_set)
lemma ftransitions_source: "q |∈| (t_source |`| ftransitions M) ==> q ∈ states M" using ftransitions_set[of M] fsm_transition_source[of _ M] by (metis (no_types, opaque_lifting) fimageE)
lemma ftransitions_target: "q |∈| (t_target |`| ftransitions M) ==> q ∈ states M" using ftransitions_set[of M] fsm_transition_target[of _ M] by (metis (no_types, lifting) fimageE)
subsection‹Responses to Input Sequences›
fun language_for_input :: "('a::linorder,'b::linorder,'c::linorder) fsm ==> 'a ==>'b list ==> ('b×'c) list list"where "language_for_input M q [] = [[]]" | "language_for_input M q (x#xs) = (let outs = outputs_as_list M in concat (map (λy . case h_obs M q x y of None ==> [] | Some q' ==> map ((#) (x,y)) (language_for_input M q' xs)) outs))"
lemma language_for_input_set : assumes"observable M" and"q ∈ states M" shows"list.set (language_for_input M q xs) = {io . io ∈ LS M q ∧ map fst io = xs}" using assms(2) proof (induction xs arbitrary: q) case Nil thenshow ?caseby auto next case (Cons x xs)
have"list.set (language_for_input M q (x#xs)) ⊆ {io . io ∈ LS M q ∧ map fst io = (x#xs)}" proof fix io assume"io ∈ list.set (language_for_input M q (x#xs))" thenobtain y where"y ∈ outputs M" and"io ∈ list.set (case h_obs M q x y of None ==> [] | Some q' ==> map ((#) (x,y)) (language_for_input M q' xs))" unfolding outputs_as_list_set[symmetric] by auto thenobtain q' where"h_obs M q x y = Some q'"and"io ∈ list.set (map ((#) (x,y)) (language_for_input M q' xs))" by (cases "h_obs M q x y"; auto)
thenobtain io' where"io = (x,y)#io'" and"io' ∈ list.set (language_for_input M q' xs)" by auto
thenhave"io' ∈ LS M q'"and"map fst io' = xs" using Cons.IH[OF h_obs_state[OF ‹h_obs M q x y = Some q'›]] by blast+ thenhave"(x,y)#io' ∈ LS M q" using‹h_obs M q x y = Some q'› unfolding h_obs_language_iff[OF assms(1), of x y io' q] by blast thenshow"io ∈ {io . io ∈ LS M q ∧ map fst io = (x#xs)}" unfolding‹io = (x,y)#io'› using‹map fst io' = xs› by auto qed moreoverhave"{io . io ∈ LS M q ∧ map fst io = (x#xs)} ⊆ list.set (language_for_input M q (x#xs))" proof have scheme : "∧ x y f xs . y ∈ list.set (f x) ==> x ∈ list.set xs ==> y ∈ list.set (concat (map f xs))" by auto
fix io assume"io ∈ {io . io ∈ LS M q ∧ map fst io = (x#xs)}" thenhave"io ∈ LS M q"and"map fst io = (x#xs)" by auto thenobtain y io' where"io = (x,y)#io'" by fastforce thenhave"(x,y)#io' ∈ LS M q" using‹io ∈ LS M q› by auto thenobtain q' where"h_obs M q x y = Some q'"and"io' ∈ LS M q'" unfolding h_obs_language_iff[OF assms(1), of x y io' q] by blast moreoverhave"io' ∈ list.set (language_for_input M q' xs)" using Cons.IH[OF h_obs_state[OF ‹h_obs M q x y = Some q'›]] ‹io' ∈ LS M q'›‹map fst io = (x#xs)› unfolding‹io = (x,y)#io'›by auto ultimatelyhave"io ∈ list.set ((λ y .(case h_obs M q x y of None ==> [] | Some q' ==> map ((#) (x,y)) (language_for_input M q' xs))) y)" unfolding‹io = (x,y)#io'› by force moreoverhave"y ∈ list.set (outputs_as_list M)" unfolding outputs_as_list_set using language_io(2)[OF ‹(x,y)#io' ∈ LS M q›] by auto ultimatelyshow"io ∈ list.set (language_for_input M q (x#xs))" unfolding language_for_input.simps Let_def using scheme[of io "(λ y .(case h_obs M q x y of None ==> [] | Some q' ==> map ((#) (x,y)) (language_for_input M q' xs)))" y] by blast qed ultimatelyshow ?case by blast qed
subsection‹Filtering Transitions›
lift_definition filter_transitions :: "('a,'b,'c) fsm ==> (('a,'b,'c) transition ==> bool) ==> ('a,'b,'c) fsm"is FSM_Impl.filter_transitions proof - fix M :: "('a,'b,'c) fsm_impl" fix P :: "('a,'b,'c) transition ==> bool" assume"well_formed_fsm M" thenshow"well_formed_fsm (FSM_Impl.filter_transitions M P)" unfolding FSM_Impl.filter_transitions.simps by force qed
lemma filter_transitions_simps[simp] : "initial (filter_transitions M P) = initial M" "states (filter_transitions M P) = states M" "inputs (filter_transitions M P) = inputs M" "outputs (filter_transitions M P) = outputs M" "transitions (filter_transitions M P) = {t ∈ transitions M . P t}" by (transfer;auto)+
lemma filter_transitions_submachine : "is_submachine (filter_transitions M P) M" unfolding filter_transitions_simps by fastforce
lemma filter_transitions_path : assumes"path (filter_transitions M P) q p" shows"path M q p" using path_begin_state[OF assms]
transition_subset_path[of "filter_transitions M P" M, OF _ assms] unfolding filter_transitions_simps by blast
lemma filter_transitions_reachable_states : assumes"q ∈ reachable_states (filter_transitions M P)" shows"q ∈ reachable_states M" using assms unfolding reachable_states_def filter_transitions_simps using filter_transitions_path[of M P "initial M"] by blast
thenshow"well_formed_fsm (FSM_Impl.filter_states M P)" by (cases "P (FSM_Impl.initial M)"; auto) qed
lemma filter_states_simps[simp] : assumes"P (initial M)" shows"initial (filter_states M P) = initial M" "states (filter_states M P) = Set.filter P (states M)" "inputs (filter_states M P) = inputs M" "outputs (filter_states M P) = outputs M" "transitions (filter_states M P) = {t ∈ transitions M . P (t_source t) ∧ P (t_target t)}" using assms by (transfer;auto)+
lemma filter_states_submachine : assumes"P (initial M)" shows"is_submachine (filter_states M P) M" using filter_states_simps[of P M, OF assms] by fastforce
fun restrict_to_reachable_states :: "('a,'b,'c) fsm ==> ('a,'b,'c) fsm"where "restrict_to_reachable_states M = filter_states M (λ q . q ∈ reachable_states M)"
lemma restrict_to_reachable_states_simps[simp] : shows"initial (restrict_to_reachable_states M) = initial M" "states (restrict_to_reachable_states M) = reachable_states M" "inputs (restrict_to_reachable_states M) = inputs M" "outputs (restrict_to_reachable_states M) = outputs M" "transitions (restrict_to_reachable_states M) = {t ∈ transitions M . (t_source t) ∈ reachable_states M}" proof - show"initial (restrict_to_reachable_states M) = initial M" "states (restrict_to_reachable_states M) = reachable_states M" "inputs (restrict_to_reachable_states M) = inputs M" "outputs (restrict_to_reachable_states M) = outputs M"
using filter_states_simps[of "(λ q . q ∈ reachable_states M)", OF reachable_states_initial] using reachable_state_is_state[of _ M] by auto
have"transitions (restrict_to_reachable_states M) = {t ∈ transitions M. (t_source t) ∈ reachable_states M ∧ (t_target t) ∈ reachable_states M}" using filter_states_simps[of "(λ q . q ∈ reachable_states M)", OF reachable_states_initial] by auto thenshow"transitions (restrict_to_reachable_states M) = {t ∈ transitions M . (t_source t) ∈ reachable_states M}" using reachable_states_next[of _ M] by auto qed
lemma restrict_to_reachable_states_path : assumes"q ∈ reachable_states M" shows"path M q p = path (restrict_to_reachable_states M) q p" proof show"path M q p ==> path (restrict_to_reachable_states M) q p" proof - assume"path M q p" thenshow"path (restrict_to_reachable_states M) q p" using assms proof (induction p arbitrary: q rule: list.induct) case Nil thenshow ?case using restrict_to_reachable_states_simps(2) by fastforce next case (Cons t' p') thenhave"path M (t_target t') p'"by auto moreoverhave"t_target t' ∈ reachable_states M"using Cons.prems by (metis path_cons_elim reachable_states_next) ultimatelyshow ?caseusing Cons.IH by (metis (no_types, lifting) Cons.prems(1) Cons.prems(2) mem_Collect_eq path.simps
path_cons_elim restrict_to_reachable_states_simps(5)) qed qed
show"path (restrict_to_reachable_states M) q p ==> path M q p" by (metis (no_types, lifting) assms mem_Collect_eq reachable_state_is_state
restrict_to_reachable_states_simps(5) subsetI transition_subset_path) qed
lemma restrict_to_reachable_states_language : "L (restrict_to_reachable_states M) = L M" unfolding LS.simps unfolding restrict_to_reachable_states_simps unfolding restrict_to_reachable_states_path[OF reachable_states_initial, of M] by blast
lemma restrict_to_reachable_states_observable : assumes"observable M" shows"observable (restrict_to_reachable_states M)" using assms unfolding observable.simps unfolding restrict_to_reachable_states_simps by blast
lemma restrict_to_reachable_states_minimal : assumes"minimal M" shows"minimal (restrict_to_reachable_states M)" proof - have"∧ q1 q2 . q1 ∈ reachable_states M ==> q2 ∈ reachable_states M ==> q1 ≠ q2 ==> LS (restrict_to_reachable_states M) q1 ≠ LS (restrict_to_reachable_states M) q2" proof - fix q1 q2 assume"q1 ∈ reachable_states M"and"q2 ∈ reachable_states M"and"q1 ≠ q2" thenhave"q1 ∈ states M"and"q2 ∈ states M" by (simp add: reachable_state_is_state)+ thenhave"LS M q1 ≠ LS M q2" using‹q1 ≠ q2› assms by auto thenshow"LS (restrict_to_reachable_states M) q1 ≠ LS (restrict_to_reachable_states M) q2" unfolding LS.simps unfolding restrict_to_reachable_states_path[OF ‹q1 ∈ reachable_states M›] unfolding restrict_to_reachable_states_path[OF ‹q2 ∈ reachable_states M›] . qed thenshow ?thesis unfolding minimal.simps restrict_to_reachable_states_simps by blast qed
lemma restrict_to_reachable_states_reachable_states : "reachable_states (restrict_to_reachable_states M) = states (restrict_to_reachable_states M)" proof show"reachable_states (restrict_to_reachable_states M) ⊆ states (restrict_to_reachable_states M)" by (simp add: reachable_state_is_state subsetI) show"states (restrict_to_reachable_states M) ⊆ reachable_states (restrict_to_reachable_states M)" proof fix q assume"q ∈ states (restrict_to_reachable_states M)" thenhave"q ∈ reachable_states M" unfolding restrict_to_reachable_states_simps . thenshow"q ∈ reachable_states (restrict_to_reachable_states M)" unfolding reachable_states_def unfolding restrict_to_reachable_states_simps unfolding restrict_to_reachable_states_path[OF reachable_states_initial, symmetric] . qed qed
subsection‹Adding Transitions›
lift_definition create_unconnected_fsm :: "'a ==> 'a set ==> 'b set ==> 'c set ==>('a,'b,'c) fsm" is FSM_Impl.create_unconnected_FSMI by (transfer; simp)
lemma create_unconnected_fsm_simps : assumes"finite ns"and"finite ins"and"finite outs"and"q ∈ ns" shows"initial (create_unconnected_fsm q ns ins outs) = q" "states (create_unconnected_fsm q ns ins outs) = ns" "inputs (create_unconnected_fsm q ns ins outs) = ins" "outputs (create_unconnected_fsm q ns ins outs) = outs" "transitions (create_unconnected_fsm q ns ins outs) = {}" using assms by (transfer; auto)+
lift_definition create_unconnected_fsm_from_lists :: "'a ==> 'a list ==> 'b list ==> 'c list ==> ('a,'b,'c) fsm" is FSM_Impl.create_unconnected_fsm_from_lists by (transfer; simp)
lemma create_unconnected_fsm_from_lists_simps : assumes"q ∈ set ns" shows"initial (create_unconnected_fsm_from_lists q ns ins outs) = q" "states (create_unconnected_fsm_from_lists q ns ins outs) = set ns" "inputs (create_unconnected_fsm_from_lists q ns ins outs) = set ins" "outputs (create_unconnected_fsm_from_lists q ns ins outs) = set outs" "transitions (create_unconnected_fsm_from_lists q ns ins outs) = {}" using assms by (transfer; auto)+
lift_definition create_unconnected_fsm_from_fsets :: "'a ==> 'a fset ==> 'b fset ==> 'c fset ==> ('a,'b,'c) fsm" is FSM_Impl.create_unconnected_fsm_from_fsets by (transfer; simp)
lemma create_unconnected_fsm_from_fsets_simps : assumes"q |∈| ns" shows"initial (create_unconnected_fsm_from_fsets q ns ins outs) = q" "states (create_unconnected_fsm_from_fsets q ns ins outs) = fset ns" "inputs (create_unconnected_fsm_from_fsets q ns ins outs) = fset ins" "outputs (create_unconnected_fsm_from_fsets q ns ins outs) = fset outs" "transitions (create_unconnected_fsm_from_fsets q ns ins outs) = {}" using assms by (transfer; auto)+
thenshow"well_formed_fsm (FSM_Impl.add_transitions M ts)" proof (cases "∀ t ∈ ts . t_source t ∈ FSM_Impl.states M ∧ t_input t ∈ FSM_Impl.inputs M ∧ t_output t ∈ FSM_Impl.outputs M ∧ t_target t ∈ FSM_Impl.states M") case True thenhave"ts ⊆ FSM_Impl.states M × FSM_Impl.inputs M × FSM_Impl.outputs M × FSM_Impl.states M" by fastforce moreoverhave"finite (FSM_Impl.states M × FSM_Impl.inputs M × FSM_Impl.outputs M × FSM_Impl.states M)" using * by blast ultimatelyhave"finite ts" using rev_finite_subset by auto thenshow ?thesis using * by auto next case False thenshow ?thesis using * by auto qed qed
lemma add_transitions_simps : assumes"∧ t . t ∈ ts ==> t_source t ∈ states M ∧ t_input t ∈ inputs M ∧ t_output t ∈ outputs M ∧ t_target t ∈ states M" shows"initial (add_transitions M ts) = initial M" "states (add_transitions M ts) = states M" "inputs (add_transitions M ts) = inputs M" "outputs (add_transitions M ts) = outputs M" "transitions (add_transitions M ts) = transitions M ∪ ts" using assms by (transfer; auto)+
lift_definition create_fsm_from_sets :: "'a ==> 'a set ==> 'b set ==> 'c set ==> ('a,'b,'c) transition set ==> ('a,'b,'c) fsm" is FSM_Impl.create_fsm_from_sets proof - fix q :: 'a fix qs :: "'a set" fix ins :: "'b set" fix outs :: "'c set" fix ts :: "('a,'b,'c) transition set"
show"well_formed_fsm (FSM_Impl.create_fsm_from_sets q qs ins outs ts)" proof (cases "q ∈ qs ∧ finite qs ∧ finite ins ∧ finite outs") case True
let ?M = "(FSMI q qs ins outs {})"
show ?thesis proof (cases "∀ t ∈ ts . t_source t ∈ FSM_Impl.states ?M ∧ t_input t ∈FSM_Impl.inputs ?M ∧ t_output t ∈ FSM_Impl.outputs ?M ∧ t_target t ∈ FSM_Impl.states ?M") case True thenhave"ts ⊆ FSM_Impl.states ?M × FSM_Impl.inputs ?M × FSM_Impl.outputs ?M × FSM_Impl.states ?M" by fastforce moreoverhave"finite (FSM_Impl.states ?M × FSM_Impl.inputs ?M × FSM_Impl.outputs ?M × FSM_Impl.states ?M)" using‹q ∈ qs ∧ finite qs ∧ finite ins ∧ finite outs›by force ultimatelyhave"finite ts" using rev_finite_subset by auto thenshow ?thesis by auto next case False thenshow ?thesis by auto qed next case False thenshow ?thesis by auto qed qed
lemma create_fsm_from_sets_simps : assumes"q ∈ qs"and"finite qs"and"finite ins"and"finite outs" assumes"∧ t . t ∈ ts ==> t_source t ∈ qs ∧ t_input t ∈ ins ∧ t_output t ∈ outs ∧ t_target t ∈ qs" shows"initial (create_fsm_from_sets q qs ins outs ts) = q" "states (create_fsm_from_sets q qs ins outs ts) = qs" "inputs (create_fsm_from_sets q qs ins outs ts) = ins" "outputs (create_fsm_from_sets q qs ins outs ts) = outs" "transitions (create_fsm_from_sets q qs ins outs ts) = ts" using assms by (transfer; auto)+
lemma create_fsm_from_self : "m = create_fsm_from_sets (initial m) (states m) (inputs m) (outputs m) (transitions m)" proof - have *: "∧ t . t ∈ transitions m ==> t_source t ∈ states m ∧ t_input t ∈ inputs m ∧ t_output t ∈ outputs m ∧ t_target t ∈ states m" by auto show ?thesis using create_fsm_from_sets_simps[OF fsm_initial fsm_states_finite fsm_inputs_finite fsm_outputs_finite *, of "transitions m"] apply transfer by force qed
lemma create_fsm_from_sets_surj : assumes"finite (UNIV :: 'a set)" and"finite (UNIV :: 'b set)" and"finite (UNIV :: 'c set)" shows"surj (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)" proof show"range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T) ⊆UNIV" by simp show"UNIV ⊆ range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)" proof fix m assume"m ∈ (UNIV :: ('a,'b,'c) fsm set)" thenhave"m = create_fsm_from_sets (initial m) (states m) (inputs m) (outputs m) (transitions m)" using create_fsm_from_self by blast thenhave"m = (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T) (initial m,states m,inputs m,outputs m,transitions m)" by auto thenshow"m ∈ range (λ(q::'a,Q,X::'b set,Y::'c set,T) . create_fsm_from_sets q Q X Y T)" by blast qed qed
subsection‹Distinguishability›
definition distinguishes :: "('a,'b,'c) fsm ==> 'a ==> 'a ==> ('b ×'c) list ==> bool"where "distinguishes M q1 q2 io = (io ∈ LS M q1 ∪ LS M q2 ∧ io ∉ LS M q1 ∩ LS M q2)"
definition minimally_distinguishes :: "('a,'b,'c) fsm ==> 'a ==> 'a ==> ('b ×'c) list ==> bool"where "minimally_distinguishes M q1 q2 io = (distinguishes M q1 q2 io ∧ (∀ io' . distinguishes M q1 q2 io' ⟶ length io ≤ length io'))"
lemma minimally_distinguishes_ex : assumes"q1 ∈ states M" and"q2 ∈ states M" and"LS M q1 ≠ LS M q2" obtains v where"minimally_distinguishes M q1 q2 v" proof - let ?vs = "{v . distinguishes M q1 q2 v}"
define vMin where vMin: "vMin = arg_min length (λv . v ∈ ?vs)"
obtain v' where"distinguishes M q1 q2 v'" using assms unfolding distinguishes_def by blast thenhave"vMin ∈ ?vs ∧ (∀ v'' . distinguishes M q1 q2 v'' ⟶ length vMin ≤ length v'')" unfolding vMin using arg_min_nat_lemma[of "λv . distinguishes M q1 q2 v" v' length] by simp thenshow ?thesis using that[of vMin] unfolding minimally_distinguishes_def by blast qed
lemma distinguish_prepend : assumes"observable M" and"distinguishes M (FSM.after M q1 io) (FSM.after M q2 io) w" and"q1 ∈ states M" and"q2 ∈ states M" and"io ∈ LS M q1" and"io ∈ LS M q2" shows"distinguishes M q1 q2 (io@w)" proof - have"(io@w ∈ LS M q1) = (w ∈ LS M (after M q1 io))" using assms(1,3,5) by (metis after_language_iff) moreoverhave"(io@w ∈ LS M q2) = (w ∈ LS M (after M q2 io))" using assms(1,4,6) by (metis after_language_iff) ultimatelyshow ?thesis using assms(2) unfolding distinguishes_def by blast qed
lemma distinguish_prepend_initial : assumes"observable M" and"distinguishes M (after_initial M (io1@io)) (after_initial M (io2@io)) w" and"io1@io ∈ L M" and"io2@io ∈ L M" shows"distinguishes M (after_initial M io1) (after_initial M io2) (io@w)" proof - have f1: "∀ps psa f a. (ps::('b × 'c) list) @ psa ∉ LS f (a::'a) ∨ ps ∈ LS f a" by (meson language_prefix) thenhave f2: "io1 ∈ L M" by (meson assms(3)) have f3: "io2 ∈ L M" using f1 by (metis assms(4)) have"io1 ∈ L M" using f1 by (metis assms(3)) thenshow ?thesis by (metis after_is_state after_language_iff after_split assms(1) assms(2) assms(3) assms(4) distinguish_prepend f3) qed
lemma minimally_distinguishes_no_prefix : assumes"observable M" and"u@w ∈ L M" and"v@w ∈ L M" and"minimally_distinguishes M (after_initial M u) (after_initial M v) (w@w'@w'')" and"w' ≠ []" shows"¬distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w''" proof assume"distinguishes M (after_initial M (u @ w)) (after_initial M (v @ w)) w''" thenhave"distinguishes M (after_initial M u) (after_initial M v) (w@w'')" using assms(1-3) distinguish_prepend_initial by blast moreoverhave"length (w@w'') < length (w@w'@w'')" using assms(5) by auto ultimatelyshow False using assms(4) unfolding minimally_distinguishes_def using leD by blast qed
lemma minimally_distinguishes_after_append : assumes"observable M" and"minimal M" and"q1 ∈ states M" and"q2 ∈ states M" and"minimally_distinguishes M q1 q2 (w@w')" and"w' ≠ []" shows"minimally_distinguishes M (after M q1 w) (after M q2 w) w'" proof - have"¬ distinguishes M q1 q2 w" using assms(5,6) by (metis add.right_neutral add_le_cancel_left length_append length_greater_0_conv linorder_not_le minimally_distinguishes_def) thenhave"w ∈ LS M q1 = (w ∈ LS M q2)" unfolding distinguishes_def by blast moreoverhave"(w@w') ∈ LS M q1 ∪ LS M q2" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast ultimatelyhave"w ∈ LS M q1"and"w ∈ LS M q2" by (meson Un_iff language_prefix)+
have"(w@w') ∈ LS M q1 = (w' ∈ LS M (after M q1 w))" by (meson ‹w ∈ LS M q1› after_language_iff assms(1)) moreoverhave"(w@w') ∈ LS M q2 = (w' ∈ LS M (after M q2 w))" by (meson ‹w ∈ LS M q2› after_language_iff assms(1)) ultimatelyhave"distinguishes M (after M q1 w) (after M q2 w) w'" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast moreoverhave"∧ w'' . distinguishes M (after M q1 w) (after M q2 w) w'' ==> length w' ≤ length w''" proof - fix w'' assume"distinguishes M (after M q1 w) (after M q2 w) w''" thenhave"distinguishes M q1 q2 (w@w'')" by (metis ‹w ∈ LS M q1›‹w ∈ LS M q2› assms(1) assms(3) assms(4) distinguish_prepend) thenhave"length (w@w') ≤ length (w@w'')" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast thenshow"length w' ≤ length w''" by auto qed ultimatelyshow ?thesis unfolding minimally_distinguishes_def distinguishes_def by blast qed
lemma minimally_distinguishes_after_append_initial : assumes"observable M" and"minimal M" and"u ∈ L M" and"v ∈ L M" and"minimally_distinguishes M (after_initial M u) (after_initial M v) (w@w')" and"w' ≠ []" shows"minimally_distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w'" proof -
have"¬ distinguishes M (after_initial M u) (after_initial M v) w" using assms(5,6) by (metis add.right_neutral add_le_cancel_left length_append length_greater_0_conv linorder_not_le minimally_distinguishes_def) thenhave"w ∈ LS M (after_initial M u) = (w ∈ LS M (after_initial M v))" unfolding distinguishes_def by blast moreoverhave"(w@w') ∈ LS M (after_initial M u) ∪ LS M (after_initial M v)" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast ultimatelyhave"w ∈ LS M (after_initial M u)"and"w ∈ LS M (after_initial M v)" by (meson Un_iff language_prefix)+
have"(w@w') ∈ LS M (after_initial M u) = (w' ∈ LS M (after_initial M (u@w)))" by (meson ‹w ∈ LS M (after_initial M u)› after_language_append_iff after_language_iff assms(1) assms(3)) moreoverhave"(w@w') ∈ LS M (after_initial M v) = (w' ∈ LS M (after_initial M (v@w)))" by (meson ‹w ∈ LS M (after_initial M v)› after_language_append_iff after_language_iff assms(1) assms(4)) ultimatelyhave"distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w'" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast moreoverhave"∧ w'' . distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w'' ==> length w' ≤ length w''" proof - fix w'' assume"distinguishes M (after_initial M (u@w)) (after_initial M (v@w)) w''" thenhave"distinguishes M (after_initial M u) (after_initial M v) (w@w'')" by (meson ‹w ∈ LS M (after_initial M u)›‹w ∈ LS M (after_initial M v)› after_language_iff assms(1) assms(3) assms(4) distinguish_prepend_initial) thenhave"length (w@w') ≤ length (w@w'')" using assms(5) unfolding minimally_distinguishes_def distinguishes_def by blast thenshow"length w' ≤ length w''" by auto qed ultimatelyshow ?thesis unfolding minimally_distinguishes_def distinguishes_def by blast qed
lemma minimally_distinguishes_proper_prefixes_card : assumes"observable M" and"minimal M" and"q1 ∈ states M" and"q2 ∈ states M" and"minimally_distinguishes M q1 q2 w" and"S ⊆ states M" shows"card {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S} ≤ card S - 1"
(is"?P S") proof -
define k where"k = card S" thenshow ?thesis using assms(6) proof (induction k arbitrary: S rule: less_induct) case (less k)
thenhave"finite S" by (metis fsm_states_finite rev_finite_subset)
show ?caseproof (cases k) case0 thenhave"S = {}" using less.prems ‹finite S›by auto thenshow ?thesis by fastforce next case (Suc k')
show ?thesis proof (cases "{w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S} = {}") case True thenshow ?thesis by (metis bot.extremum dual_order.eq_iff obtain_subset_with_card_n) next case False
define wk where wk: "wk = arg_max length (λwk . wk ∈ {w' . w' ∈ set (prefixes w) ∧ w'≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S})"
obtain wk' where *:"wk' ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S}" using False by blast have"finite {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S}" by (metis (no_types) Collect_mem_eq List.finite_set finite_Collect_conjI) thenhave"wk ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S}" and"∧ wk' . wk' ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S} ==> length wk' ≤ length wk" using False unfolding wk using arg_max_nat_lemma[of "(λwk . wk ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S})", OF *] by (meson finite_maxlen)+
thenhave"wk ∈ set (prefixes w)"and"wk ≠ w"and"after M q1 wk ∈ S"and"after M q2 wk ∈ S" by blast+
obtain wk_suffix where"w = wk@wk_suffix"and"wk_suffix ≠ []" using‹wk ∈ set (prefixes w)› using prefixes_set_ob ‹wk ≠ w› by blast
have"distinguishes M (after M q1 []) (after M q2 []) w" using‹minimally_distinguishes M q1 q2 w› by (metis after.simps(1) minimally_distinguishes_def)
have"minimally_distinguishes M (after M q1 wk) (after M q2 wk) wk_suffix" using‹minimally_distinguishes M q1 q2 w›‹wk_suffix ≠ []› unfolding‹w = wk@wk_suffix› using minimally_distinguishes_after_append[OF assms(1,2,3,4), of wk wk_suffix] by blast thenhave"distinguishes M (after M q1 wk) (after M q2 wk) wk_suffix" unfolding minimally_distinguishes_def by auto thenhave"wk_suffix ∈ LS M (after M q1 wk) = (wk_suffix ∉ LS M (after M q2 wk))" unfolding distinguishes_def by blast
define S1 where S1: "S1 = Set.filter (λq . wk_suffix ∈ LS M q) S"
define S2 where S2: "S2 = Set.filter (λq . wk_suffix ∉ LS M q) S"
have"S = S1 ∪ S2" unfolding S1 S2 by auto moreoverhave"S1 ∩ S2 = {}" unfolding S1 S2 by auto ultimatelyhave"card S = card S1 + card S2" using‹finite S› card_Un_disjoint by blast
have"S1 ⊆ states M"and"S2 ⊆ states M" using‹S = S1 ∪ S2› less.prems(2) by blast+
have"S1 ≠ {}"and"S2 ≠ {}" using‹wk_suffix ∈ LS M (after M q1 wk) = (wk_suffix ∉ LS M (after M q2 wk))›‹after M q1 wk ∈ S›‹after M q2 wk ∈ S› unfolding S1 S2 by auto thenhave"card S1 > 0"and"card S2 > 0" using‹S = S1 ∪ S2›‹finite S› by (meson card_0_eq finite_Un neq0_conv)+ thenhave"card S1 < k"and"card S2 < k" using‹card S = card S1 + card S2›unfolding less.prems by auto
define W where W: "W = (λ S1 S2 . {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S1 ∧ after M q2 w' ∈ S2})" thenhave"∧ S' S'' . W S' S'' ⊆ set (prefixes w)" by auto thenhave W_finite: "∧ S' S'' . finite (W S' S'')" using List.finite_set[of "prefixes w"] by (meson finite_subset)
have"∧ w' . w' ∈ W S S ==> w' ≠ wk ==> after M q1 w' ∈ S1 = (after M q2 w' ∈ S1)" proof - fix w' assume *:"w' ∈ W S S"and"w' ≠ wk" thenhave"w' ∈ set (prefixes w)"and"w' ≠ w"and"after M q1 w' ∈ S"and"after M q2 w' ∈ S" unfolding W by blast+
thenhave"w' ∈ LS M q1" by (metis IntE UnCI UnE append_self_conv assms(5) distinguishes_def language_prefix leD length_append length_greater_0_conv less_add_same_cancel1 minimally_distinguishes_def prefixes_set_ob) have"w' ∈ LS M q2" by (metis IntE UnCI ‹w' ∈ LS M q1›‹w' ∈ set (prefixes w)›‹w' ≠ w› append_Nil2 assms(5) distinguishes_def leD length_append length_greater_0_conv less_add_same_cancel1 minimally_distinguishes_def prefixes_set_ob)
have"length w' < length wk" using‹w' ≠ wk› * ‹∧ wk' . wk' ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S} ==> length wk' ≤ length wk› unfolding W by (metis (no_types, lifting) ‹w = wk @ wk_suffix›‹w' ∈ set (prefixes w)› append_eq_append_conv le_neq_implies_less prefixes_set_ob)
show"after M q1 w' ∈ S1 = (after M q2 w' ∈ S1)" proof (rule ccontr) assume"(after M q1 w' ∈ S1) ≠ (after M q2 w' ∈ S1)" thenhave"(after M q1 w' ∈ S1 ∧ (after M q2 w' ∈ S2)) ∨ (after M q1 w' ∈ S2 ∧ (after M q2 w' ∈ S1))" using‹after M q1 w' ∈ S›‹after M q2 w' ∈ S› unfolding‹S = S1 ∪ S2› by blast thenhave"wk_suffix ∈ LS M (after M q1 w') = (wk_suffix ∉ LS M (after M q2 w'))" using S1 S2 by auto thenhave"distinguishes M (after M q1 w') (after M q2 w') wk_suffix" unfolding distinguishes_def by blast thenhave"distinguishes M q1 q2 (w'@wk_suffix)" using distinguish_prepend[OF assms(1) _ ‹q1 ∈ states M›‹q2 ∈ states M›‹w' ∈ LS M q1›‹w' ∈ LS M q2›] by blast moreoverhave"length (w'@wk_suffix) < length (wk@wk_suffix)" using‹length w' < length wk› by auto ultimatelyshow False using‹minimally_distinguishes M q1 q2 w› unfolding‹w = wk@wk_suffix› minimally_distinguishes_def by auto qed qed
have"∧ x . x ∈ W S1 S2 ∪ W S2 S1 ==> x = wk" proof - fix x assume"x ∈ W S1 S2 ∪ W S2 S1" thenhave"x ∈ W S S" unfolding W ‹S = S1 ∪ S2›by blast show"x = wk" using‹x ∈ W S1 S2 ∪ W S2 S1› using‹∧ w' . w' ∈ W S S ==> w' ≠ wk ==> after M q1 w' ∈ S1 = (after M q2 w' ∈ S1)›[OF ‹x ∈ W S S›] unfolding W using‹S1 ∩ S2 = {}› by blast qed moreoverhave"wk ∈ W S1 S2 ∪ W S2 S1" unfolding W using‹wk ∈ {w' . w' ∈ set (prefixes w) ∧ w' ≠ w ∧ after M q1 w' ∈ S ∧ after M q2 w' ∈ S}› ‹wk_suffix ∈ LS M (after M q1 wk) = (wk_suffix ∉ LS M (after M q2 wk))› using S1 by clarsimp (auto simp add: ‹S = S1 ∪ S2›) ultimatelyhave"W S1 S2 ∪ W S2 S1 = {wk}" by blast
have"W S S = (W S1 S1 ∪ W S2 S2 ∪ (W S1 S2 ∪ W S2 S1))" unfolding W ‹S = S1 ∪ S2›by blast moreoverhave"W S1 S1 ∩ W S2 S2 = {}" using‹S1 ∩ S2 = {}›unfolding W by blast moreoverhave"W S1 S1 ∩ (W S1 S2 ∪ W S2 S1) = {}" unfolding W using‹S1 ∩ S2 = {}› by blast moreoverhave"W S2 S2 ∩ (W S1 S2 ∪ W S2 S1) = {}" unfolding W using‹S1 ∩ S2 = {}› by blast moreoverhave"finite (W S1 S1)"and"finite (W S2 S2)"and"finite {wk}" using W_finite by auto ultimatelyhave"card (W S S) = card (W S1 S1) + card (W S2 S2) + 1" unfolding‹W S1 S2 ∪ W S2 S1 = {wk}› by (metis card_Un_disjoint finite_UnI inf_sup_distrib2 is_singletonI is_singleton_altdef sup_idem) moreoverhave"card (W S1 S1) ≤ card S1 - 1" using less.IH[OF ‹card S1 < k› _ ‹S1 ⊆ states M›] unfolding W by blast moreoverhave"card (W S2 S2) ≤ card S2 - 1" using less.IH[OF ‹card S2 < k› _ ‹S2 ⊆ states M›] unfolding W by blast ultimatelyhave"card (W S S) ≤ card S - 1" using‹card S = card S1 + card S2› using‹card S1 < k›‹card S2 < k› less.prems(1) by linarith thenshow ?thesis unfolding W . qed qed qed qed
lemma minimally_distinguishes_proper_prefix_in_language : assumes"minimally_distinguishes M q1 q2 io" and"io' ∈ set (prefixes io)" and"io' ≠ io" shows"io' ∈ LS M q1 ∩ LS M q2" proof - have"io ∈ LS M q1 ∨ io ∈ LS M q2" using assms(1) unfolding minimally_distinguishes_def distinguishes_def by blast thenhave"io' ∈ LS M q1 ∨ io' ∈ LS M q2" by (metis assms(2) prefixes_set_ob language_prefix)
have"length io' < length io" using assms(2,3) unfolding prefixes_set by auto thenhave"io' ∈ LS M q1 ⟷ io' ∈ LS M q2" using assms(1) unfolding minimally_distinguishes_def distinguishes_def by (metis Int_iff Un_Int_eq(1) Un_Int_eq(2) leD) thenshow ?thesis using‹io' ∈ LS M q1 ∨ io' ∈ LS M q2› by blast qed
lemma distinguishes_not_Nil: assumes"distinguishes M q1 q2 io" and"q1 ∈ states M" and"q2 ∈ states M" shows"io ≠ []" using assms unfolding distinguishes_def by auto
fun does_distinguish :: "('a,'b,'c) fsm ==> 'a ==> 'a ==> ('b × 'c) list ==> bool"where "does_distinguish M q1 q2 io = (is_in_language M q1 io ≠ is_in_language M q2 io)"
lemma does_distinguish_correctness : assumes"observable M" and"q1 ∈ states M" and"q2 ∈ states M" shows"does_distinguish M q1 q2 io = distinguishes M q1 q2 io" unfolding does_distinguish.simps
is_in_language_iff[OF assms(1,2)]
is_in_language_iff[OF assms(1,3)]
distinguishes_def by blast
lemma h_obs_distinguishes : assumes"observable M" and"h_obs M q1 x y = Some q1'" and"h_obs M q2 x y = None" shows"distinguishes M q1 q2 [(x,y)]" using assms(2,3) LS_single_transition[of x y M] unfolding distinguishes_def h_obs_Some[OF assms(1)] h_obs_None[OF assms(1)] by (metis Int_iff UnI1 ‹∧y x q. (h_obs M q x y = None) = (∄q'. (q, x, y, q') ∈ FSM.transitions M)› assms(1) assms(2) fst_conv h_obs_language_iff option.distinct(1) snd_conv)
lemma distinguishes_sym : assumes"distinguishes M q1 q2 io" shows"distinguishes M q2 q1 io" using assms unfolding distinguishes_def by blast
lemma distinguishes_after_prepend : assumes"observable M" and"h_obs M q1 x y ≠ None" and"h_obs M q2 x y ≠ None" and"distinguishes M (FSM.after M q1 [(x,y)]) (FSM.after M q2 [(x,y)]) γ" shows"distinguishes M q1 q2 ((x,y)#γ)" proof - have"[(x,y)] ∈ LS M q1" using assms(2) h_obs_language_single_transition_iff[OF assms(1)] by auto
have"[(x,y)] ∈ LS M q2" using assms(3) h_obs_language_single_transition_iff[OF assms(1)] by auto
show ?thesis using after_language_iff[OF assms(1) ‹[(x,y)] ∈ LS M q1›, of γ] using after_language_iff[OF assms(1) ‹[(x,y)] ∈ LS M q2›, of γ] using assms(4) unfolding distinguishes_def by simp qed
lemma distinguishes_after_initial_prepend : assumes"observable M" and"io1 ∈ L M" and"io2 ∈ L M" and"h_obs M (after_initial M io1) x y ≠ None" and"h_obs M (after_initial M io2) x y ≠ None" and"distinguishes M (after_initial M (io1@[(x,y)])) (after_initial M (io2@[(x,y)])) γ" shows"distinguishes M (after_initial M io1) (after_initial M io2) ((x,y)#γ)" by (metis after_split assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) distinguishes_after_prepend h_obs_language_append)
lemma add_transition_simps[simp]: assumes"t_source t ∈ states M"and"t_input t ∈ inputs M"and"t_output t ∈ outputs M"and"t_target t ∈ states M" shows "initial (add_transition M t) = initial M" "inputs (add_transition M t) = inputs M" "outputs (add_transition M t) = outputs M" "transitions (add_transition M t) = insert t (transitions M)" "states (add_transition M t) = states M"using assms by (transfer; simp)+
lift_definition add_state :: "('a,'b,'c) fsm ==> 'a ==> ('a,'b,'c) fsm"is FSM_Impl.add_state by simp
lemma add_state_simps[simp]: "initial (add_state M q) = initial M" "inputs (add_state M q) = inputs M" "outputs (add_state M q) = outputs M" "transitions (add_state M q) = transitions M" "states (add_state M q) = insert q (states M)"by (transfer; simp)+
lemma rename_states_simps[simp]: "initial (rename_states M f) = f (initial M)" "states (rename_states M f) = f ` (states M)" "inputs (rename_states M f) = inputs M" "outputs (rename_states M f) = outputs M" "transitions (rename_states M f) = (λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions M" by (transfer; simp)+
lemma rename_states_isomorphism_language_state : assumes"bij_betw f (states M) (f ` states M)" and"q ∈ states M" shows"LS (rename_states M f) (f q) = LS M q" proof -
have *: "bij_betw f (FSM.states M) (FSM.states (FSM.rename_states M f))" using assms rename_states_simps by auto
have **: "f (initial M) = initial (rename_states M f)" using rename_states_simps by auto
have ***: "(∧q x y q'. q ∈ states M ==> q' ∈ states M ==> ((q, x, y, q') ∈ transitions M) = ((f q, x, y, f q') ∈ transitions (rename_states M f)))" proof fix q x y q' assume"q ∈ states M"and"q' ∈ states M"
show"(q, x, y, q') ∈ transitions M ==> (f q, x, y, f q') ∈ transitions (rename_states M f)" unfolding assms rename_states_simps by force
show"(f q, x, y, f q') ∈ transitions (rename_states M f) ==> (q, x, y, q') ∈ transitions M" proof - assume"(f q, x, y, f q') ∈ transitions (rename_states M f)" thenobtain t where"(f q, x, y, f q') = (f (t_source t), t_input t, t_output t, f (t_target t))" and"t ∈ transitions M" unfolding assms rename_states_simps by blast thenhave"t_source t ∈ states M"and"t_target t ∈ states M"and"f (t_source t) = f q"and"f (t_target t) = f q'"and"t_input t = x"and"t_output t = y" by auto
have"f q ∈ states (rename_states M f)"and"f q' ∈ states (rename_states M f)" using‹(f q, x, y, f q') ∈ transitions (rename_states M f)› by auto
have"t_source t = q" using‹f (t_source t) = f q›‹q ∈ states M›‹t_source t ∈ states M› using assms unfolding bij_betw_def inj_on_def by blast moreoverhave"t_target t = q'" using‹f (t_target t) = f q'›‹q' ∈ states M›‹t_target t ∈ states M› using assms unfolding bij_betw_def inj_on_def by blast ultimatelyshow"(q, x, y, q') ∈ transitions M" using‹t_input t = x›‹t_output t = y›‹t ∈ transitions M› by auto qed qed
show ?thesis using language_equivalence_from_isomorphism[OF * ** *** assms(2)] by blast qed
lemma rename_states_isomorphism_language : assumes"bij_betw f (states M) (f ` states M)" shows"L (rename_states M f) = L M" using rename_states_isomorphism_language_state[OF assms fsm_initial] unfolding rename_states_simps .
lemma rename_states_observable : assumes"bij_betw f (states M) (f ` states M)" and"observable M" shows"observable (rename_states M f)" proof - have"∧ q1 x y q1' q1'' . (q1,x,y,q1') ∈ transitions (rename_states M f) ==> (q1,x,y,q1'') ∈ transitions (rename_states M f) ==> q1' = q1''" proof - fix q1 x y q1' q1'' assume"(q1,x,y,q1') ∈ transitions (rename_states M f)"and"(q1,x,y,q1'') ∈ transitions (rename_states M f)" thenobtain t' t'' where"t' ∈ transitions M" and"t'' ∈ transitions M" and"(f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1,x,y,q1')" and"(f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1,x,y,q1'')" unfolding rename_states_simps by force
thenhave"f (t_source t') = f (t_source t'')" by auto moreoverhave"t_source t' ∈ states M"and"t_source t'' ∈ states M" using‹t' ∈ transitions M›‹t'' ∈ transitions M› by auto ultimatelyhave"t_source t' = t_source t''" using assms(1) unfolding bij_betw_def inj_on_def by blast thenhave"t_target t' = t_target t''" using assms(2) unfolding observable.simps by (metis Pair_inject ‹(f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1, x, y, q1'')›‹(f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1, x, y, q1')›‹t' ∈ FSM.transitions M›‹t'' ∈ FSM.transitions M›) thenshow"q1' = q1''" using‹(f (t_source t''), t_input t'', t_output t'', f (t_target t'')) = (q1, x, y, q1'')›‹(f (t_source t'), t_input t', t_output t', f (t_target t')) = (q1, x, y, q1')›by auto qed thenshow ?thesis unfolding observable_alt_def by blast qed
lemma rename_states_minimal : assumes"bij_betw f (states M) (f ` states M)" and"minimal M" shows"minimal (rename_states M f)" proof - have"∧ q q' . q ∈ f ` FSM.states M ==> q' ∈ f ` FSM.states M ==> q ≠ q' ==> LS (rename_states M f) q ≠ LS (rename_states M f) q'" proof - fix q q' assume"q ∈ f ` FSM.states M"and"q' ∈ f ` FSM.states M"and"q ≠ q'"
thenobtain fq fq' where"fq ∈ states M"and"fq' ∈ states M"and"q = f fq"and"q' = f fq'" by auto thenhave"fq ≠ fq'" using‹q ≠ q'›by auto thenhave"LS M fq ≠ LS M fq'" by (meson ‹fq ∈ FSM.states M›‹fq' ∈ FSM.states M› assms(2) minimal.elims(2)) thenshow"LS (rename_states M f) q ≠ LS (rename_states M f) q'" using rename_states_isomorphism_language_state[OF assms(1)] by (simp add: ‹fq ∈ FSM.states M›‹fq' ∈ FSM.states M›‹q = f fq›‹q' = f fq'›) qed thenshow ?thesis by auto qed
fun index_states :: "('a::linorder,'b,'c) fsm ==> (nat,'b,'c) fsm"where "index_states M = rename_states M (assign_indices (states M))"
lemma assign_indices_bij_betw: "bij_betw (assign_indices (FSM.states M)) (FSM.states M) (assign_indices (FSM.states M) ` FSM.states M)" using assign_indices_bij[OF fsm_states_finite[of M]] by (simp add: bij_betw_def)
lemma index_states_language : "L (index_states M) = L M" using rename_states_isomorphism_language[of "assign_indices (states M)" M, OF assign_indices_bij_betw] by auto
lemma index_states_observable : assumes"observable M" shows"observable (index_states M)" using rename_states_observable[of "assign_indices (states M)", OF assign_indices_bij_betw assms] unfolding index_states.simps .
lemma index_states_minimal : assumes"minimal M" shows"minimal (index_states M)" using rename_states_minimal[of "assign_indices (states M)", OF assign_indices_bij_betw assms] unfolding index_states.simps .
fun index_states_integer :: "('a::linorder,'b,'c) fsm ==> (integer,'b,'c) fsm"where "index_states_integer M = rename_states M (integer_of_nat ∘ assign_indices (states M))"
lemma assign_indices_integer_bij_betw: "bij_betw (integer_of_nat ∘ assign_indices (states M)) (FSM.states M) ((integer_of_nat ∘ assign_indices (states M)) ` FSM.states M)" proof - have *: "inj_on (assign_indices (FSM.states M)) (FSM.states M)" using assign_indices_bij[OF fsm_states_finite[of M]] unfolding bij_betw_def by auto thenhave"inj_on (integer_of_nat ∘ assign_indices (states M)) (FSM.states M)" unfolding inj_on_def by (metis comp_apply nat_of_integer_integer_of_nat) thenshow ?thesis unfolding bij_betw_def by auto qed
lemma index_states_integer_language : "L (index_states_integer M) = L M" using rename_states_isomorphism_language[of "integer_of_nat ∘ assign_indices (states M)" M, OF assign_indices_integer_bij_betw] by auto
lemma index_states_integer_observable : assumes"observable M" shows"observable (index_states_integer M)" using rename_states_observable[of "integer_of_nat ∘ assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms] unfolding index_states_integer.simps .
lemma index_states_integer_minimal : assumes"minimal M" shows"minimal (index_states_integer M)" using rename_states_minimal[of "integer_of_nat ∘ assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms] unfolding index_states_integer.simps .
subsection‹Canonical Separators›
lift_definition canonical_separator' :: "('a,'b,'c) fsm ==> (('a × 'a),'b,'c) fsm ==> 'a ==> 'a ==> (('a × 'a) + 'a,'b,'c) fsm"is FSM_Impl.canonical_separator' proof - fix A :: "('a,'b,'c) fsm_impl" fix B :: "('a × 'a,'b,'c) fsm_impl" fix q1 :: 'a fix q2 :: 'a assume"well_formed_fsm A"and"well_formed_fsm B"
thenhave p1a: "fsm_impl.initial A ∈ fsm_impl.states A" and p2a: "finite (fsm_impl.states A)" and p3a: "finite (fsm_impl.inputs A)" and p4a: "finite (fsm_impl.outputs A)" and p5a: "finite (fsm_impl.transitions A)" and p6a: "(∀t∈fsm_impl.transitions A. t_source t ∈ fsm_impl.states A ∧ t_input t ∈ fsm_impl.inputs A ∧ t_target t ∈ fsm_impl.states A ∧ t_output t ∈ fsm_impl.outputs A)" and p1b: "fsm_impl.initial B ∈ fsm_impl.states B" and p2b: "finite (fsm_impl.states B)" and p3b: "finite (fsm_impl.inputs B)" and p4b: "finite (fsm_impl.outputs B)" and p5b: "finite (fsm_impl.transitions B)" and p6b: "(∀t∈fsm_impl.transitions B. t_source t ∈ fsm_impl.states B ∧ t_input t ∈ fsm_impl.inputs B ∧ t_target t ∈ fsm_impl.states B ∧ t_output t ∈ fsm_impl.outputs B)" by simp+
let ?P = "FSM_Impl.canonical_separator' A B q1 q2"
show "well_formed_fsm ?P" proof (cases "fsm_impl.initial B = (q1,q2)") case False then show ?thesis by auto next case True
let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs ==> yqs | None ==> {}))" have "∧ qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs ==> yqs | None ==> {})) qx = (λ qx . {z. (qx, z) ∈(λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx" proof - fix qx show "∧ qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (fsm_impl.transitions A))) qx of Some yqs ==> yqs | None ==> {})) qx = (λ qx . {z. (qx, z) ∈(λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx" unfolding set_as_map_def by (cases "∃z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A"; auto) qed moreover have "∧ qx . (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ fsm_impl.transitions A}) qx" proof - fix qx show "(λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` fsm_impl.transitions A}) qx = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ fsm_impl.transitions A}) qx" by force qed ultimately have *:" ?f = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ fsm_impl.transitions A})" by blast let ?shifted_transitions' = "shifted_transitions (fsm_impl.transitions B)" let ?distinguishing_transitions_lr = "distinguishing_transitions ?f q1 q2 (fsm_impl.states B) (fsm_impl.inputs B)" let ?ts = "?shifted_transitions' ∪ ?distinguishing_transitions_lr" have "FSM_Impl.states ?P = (image Inl (FSM_Impl.states B)) ∪ {Inr q1, Inr q2}" and "FSM_Impl.transitions ?P = ?ts" unfolding FSM_Impl.canonical_separator'.simps Let_def True by simp+
have p2: "finite (fsm_impl.states ?P)" unfolding ‹FSM_Impl.states ?P = (image Inl (FSM_Impl.states B)) ∪ {Inr q1, Inr q2}› using p2b by blast have "fsm_impl.initial ?P = Inl (q1,q2)" by auto then have p1: "fsm_impl.initial ?P ∈ fsm_impl.states ?P" using p1a p1b unfolding canonical_separator'.simps True by auto have p3: "finite (fsm_impl.inputs ?P)" using p3a p3b by auto have p4: "finite (fsm_impl.outputs ?P)" using p4a p4b by auto
have "finite (fsm_impl.states B × fsm_impl.inputs B)" using p2b p3b by blast moreover have **: "∧ x q1 . finite ({y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ fsm_impl.transitions A})" proof - fix x q1 have "{y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ fsm_impl.transitions A} = {t_output t | t . t ∈ fsm_impl.transitions A ∧ t_source t = q1 ∧ t_input t = x}" by auto then have "{y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ fsm_impl.transitions A} ⊆ image t_output (fsm_impl.transitions A)" unfolding fst_conv snd_conv by blast moreover have "finite (image t_output (fsm_impl.transitions A))" using p5a by auto ultimately show "finite ({y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ fsm_impl.transitions A})" by (simp add: finite_subset) qed ultimately have "finite ?distinguishing_transitions_lr" unfolding * distinguishing_transitions_def by force moreover have "finite ?shifted_transitions'" unfolding shifted_transitions_def using p5b by auto ultimately have "finite ?ts" by blast then have p5: "finite (fsm_impl.transitions ?P)" by simp have "fsm_impl.inputs ?P = fsm_impl.inputs A ∪ fsm_impl.inputs B" using True by auto have "fsm_impl.outputs ?P = fsm_impl.outputs A ∪ fsm_impl.outputs B" using True by auto have "∧ t . t ∈ ?shifted_transitions' ==> t_source t ∈ fsm_impl.states ?P ∧ t_target t ∈ fsm_impl.states ?P" unfolding ‹FSM_Impl.states ?P = (image Inl (FSM_Impl.states B)) ∪ {Inr q1, Inr q2}› shifted_transitions_def using p6b by force moreover have "∧ t . t ∈ ?distinguishing_transitions_lr ==> t_source t ∈ fsm_impl.states ?P ∧ t_target t ∈ fsm_impl.states ?P" unfolding ‹FSM_Impl.states ?P = (image Inl (FSM_Impl.states B)) ∪ {Inr q1, Inr q2}› distinguishing_transitions_def * by force ultimately have "∧ t . t ∈ ?ts ==> t_source t ∈ fsm_impl.states ?P ∧ t_target t ∈ fsm_impl.states ?P" by blast moreover have "∧ t . t ∈ ?shifted_transitions' ==> t_input t ∈ fsm_impl.inputs ?P ∧ t_output t ∈ fsm_impl.outputs ?P" proof - have "∧ t . t ∈ ?shifted_transitions' ==> t_input t ∈ fsm_impl.inputs B ∧ t_output t ∈ fsm_impl.outputs B" unfolding shifted_transitions_def using p6b by auto then show "∧ t . t ∈ ?shifted_transitions' ==> t_input t ∈ fsm_impl.inputs ?P ∧t_output t ∈ fsm_impl.outputs ?P" unfolding ‹fsm_impl.inputs ?P = fsm_impl.inputs A ∪ fsm_impl.inputs B› ‹fsm_impl.outputs ?P = fsm_impl.outputs A ∪ fsm_impl.outputs B› by blast qed moreover have "∧ t . t ∈ ?distinguishing_transitions_lr ==> t_input t ∈ fsm_impl.inputs ?P ∧ t_output t ∈ fsm_impl.outputs ?P" unfolding * distinguishing_transitions_def using p6a p6b True by auto ultimately have p6: "(∀t∈fsm_impl.transitions ?P. t_source t ∈ fsm_impl.states ?P ∧ t_input t ∈ fsm_impl.inputs ?P ∧ t_target t ∈ fsm_impl.states ?P ∧ t_output t ∈ fsm_impl.outputs ?P)" unfolding ‹FSM_Impl.transitions ?P = ?ts› by blast show "well_formed_fsm ?P" using p1 p2 p3 p4 p5 p6 by linarith qed qed
lemma canonical_separator'_simps : assumes "initial P = (q1,q2)" shows "initial (canonical_separator' M P q1 q2) = Inl (q1,q2)" "states (canonical_separator' M P q1 q2) = (image Inl (states P)) ∪ {Inr q1, Inr q2}" "inputs (canonical_separator' M P q1 q2) = inputs M ∪ inputs P" "outputs (canonical_separator' M P q1 q2) = outputs M ∪ outputs P" "transitions (canonical_separator' M P q1 q2) = shifted_transitions (transitions P) ∪ distinguishing_transitions (h_out M) q1 q2 (states P) (inputs P)" using assms unfolding h_out_code by (transfer; auto)+
lemma canonical_separator'_simps_without_assm : "initial (canonical_separator' M P q1 q2) = Inl (q1,q2)" "states (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then (image Inl (states P)) ∪ {Inr q1, Inr q2} else {Inl (q1,q2)})" "inputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then inputs M∪ inputs P else {})" "outputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then outputs M ∪ outputs P else {})" "transitions (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then shifted_transitions (transitions P) ∪ distinguishing_transitions (h_out M) q1 q2 (states P) (inputs P) else {})" unfolding h_out_code by (transfer; simp add: Let_def)+
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.