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 then have "(∄ps. pps (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa)
(λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa ∧ distinct (visited_states (FSM.initial M) psa))
= p_io ps ∧ path M (FSM.initial M) ps ∧ distinct (visited_states (FSM.initial M) ps)) ≠ (∃ps. pps (λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa)
(λps. ∃psa. ps = p_io psa ∧ path M (FSM.initial M) psa ∧ distinct (visited_states (FSM.initial M) psa))
= p_io ps ∧ path M (FSM.initial M) ps)" by blast then have "{p_io ps |ps. path M (FSM.initial M) ps ∧ distinct (visited_states (FSM.initial M) ps)}
= {p_io ps |ps. path M (FSM.initial M) ps}" using f1 by (meson ‹∀ps. ¬ path M (FSM.initial M) ps ∨ distinct (visited_states (FSM.initial M) ps)›) then show ?thesis by (simp add: LS_acyclic_def) qed
lemma cyclic_cycle : assumes "¬ acyclic M" shows "∃ q p . path M q p ∧ p ≠ [] ∧ target q p = q" proof - from ‹¬ acyclic M› obtain p t where "path M (initial M) (p@[t])" and "¬distinct (visited_states (initial M) (p@[t]))" by (metis (no_types, opaque_lifting) Nil_is_append_conv acyclic.simps append_take_drop_id maximal_distinct_prefix rev_exhaust visited_states_take)
show ?thesis proof (cases "initial M ∈ set (map t_target (p@[t]))") case True then obtain i where "last (take i (map t_target (p@[t]))) = initial M" and "i ≤ length (map t_target (p@[t]))" and "0 < i" using list_contains_last_take by metis
let ?p = "take i (p@[t])" have "path M (initial M) (?p@(drop i (p@[t])))" using ‹path M (initial M) (p@[t])› by (metis append_take_drop_id) then have "path M (initial M) ?p" by auto moreover have "?p ≠ []" using ‹0 < i› by auto moreover have "target (initial M) ?p = initial M" using ‹last (take i (map t_target (p@[t]))) = initial M› unfolding target.simps visited_states.simps by (metis (no_types, lifting) calculation(2) last_ConsR list.map_disc_iff take_map) ultimately show ?thesis by blast next case False then have "¬ distinct (map t_target (p@[t]))" using ‹¬distinct (visited_states (initial M) (p@[t]))› unfolding visited_states.simps by auto then obtain i j where "i < j" and "j < length (map t_target (p@[t]))" and "(map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j" using non_distinct_repetition_indices by blast
let ?pre_i = "take (Suc i) (p@[t])" let ?p = "take ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))" let ?post_j = "drop ((Suc j)-(Suc i)) (drop (Suc i) (p@[t]))"
have "p@[t] = ?pre_i @ ?p @ ?post_j" using ‹i < j›‹j < length (map t_target (p@[t]))› by (metis append_take_drop_id) then have "path M (target (initial M) ?pre_i) ?p" using ‹path M (initial M) (p@[t])› by (metis path_prefix path_suffix)
have "?p ≠ []" using ‹i < j›‹j < length (map t_target (p@[t]))› by auto
have "i < length (map t_target (p@[t]))" using ‹i < j›‹j < length (map t_target (p@[t]))› by auto have "(target (initial M) ?pre_i) = (map t_target (p@[t])) ! i" unfolding target.simps visited_states.simps using take_last_index[OF ‹i < length (map t_target (p@[t]))›] by (metis (no_types, lifting) ‹i < length (map t_target (p @ [t]))› last_ConsR snoc_eq_iff_butlast take_Suc_conv_app_nth take_map) have "?pre_i@?p = take (Suc j) (p@[t])" by (metis (no_types) ‹i < j› add_Suc add_diff_cancel_left' less_SucI less_imp_Suc_add take_add) moreover have "(target (initial M) (take (Suc j) (p@[t]))) = (map t_target (p@[t])) ! j" unfolding target.simps visited_states.simps using take_last_index[OF ‹j < length (map t_target (p@[t]))›] by (metis (no_types, lifting) ‹j < length (map t_target (p @ [t]))› last_ConsR snoc_eq_iff_butlast take_Suc_conv_app_nth take_map) ultimately have "(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! j" by auto then have "(target (initial M) (?pre_i@?p)) = (map t_target (p@[t])) ! i" using ‹(map t_target (p@[t])) ! i = (map t_target (p@[t])) ! j› by simp moreover have "(target (initial M) (?pre_i@?p)) = (target (target (initial M) ?pre_i) ?p)" unfolding target.simps visited_states.simps last.simps by auto ultimately have "(target (target (initial M) ?pre_i) ?p) = (map t_target (p@[t])) ! i" by auto then have "(target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)" using ‹(target (initial M) ?pre_i) = (map t_target (p@[t])) ! i› by auto
show ?thesis using ‹path M (target (initial M) ?pre_i) ?p›‹?p ≠ []› ‹(target (target (initial M) ?pre_i) ?p) = (target (initial M) ?pre_i)› by blast qed qed
lemma cyclic_cycle_rev : fixes M :: "('a,'b,'c) fsm" assumes "path M (initial M) p'" and "target (initial M) p' = q" and "path M q p" and "p ≠ []" and "target q p = q" shows "¬ acyclic M" using assms unfolding acyclic.simps target.simps visited_states.simps using distinct.simps(2) by fastforce
lemma acyclic_initial : assumes "acyclic M" shows "¬ (∃ t ∈transitions M . t_target t = initial M ∧
(∃ p . path M (initial M) p ∧ target (initial M) p = t_source t))" by (metis append_Cons assms cyclic_cycle_rev list.distinct(1) path.simps path_append path_append_transition_elim(3) single_transition_path)
lemma cyclic_path_shift : assumes "path M q p" and "target q p = q" shows "path M (target q (take i p)) ((drop i p) @ (take i p))" and "target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))" proof - show "path M (target q (take i p)) ((drop i p) @ (take i p))" by (metis append_take_drop_id assms(1) assms(2) path_append path_append_elim path_append_target) show "target (target q (take i p)) ((drop i p) @ (take i p)) = (target q (take i p))" by (metis append_take_drop_id assms(2) path_append_target) qed
lemma cyclic_path_transition_states_property : assumes "∃ t ∈ set p . P (t_source t)" and "∀ t ∈ set p . P (t_source t) ⟶ P (t_target t)" and "path M q p" and "target q p = q" shows "∀ t ∈ set p . P (t_source t)" and "∀ t ∈ set p . P (t_target t)" proof - obtain t0 where "t0 ∈ set p" and "P (t_source t0)" using assms(1) by blast then obtain i where "i < length p" and "p ! i = t0" by (meson in_set_conv_nth)
let ?p = "(drop i p @ take i p)" have "path M (target q (take i p)) ?p" using cyclic_path_shift(1)[OF assms(3,4), of i] by assumption have "set ?p = set p" proof - have "set ?p = set (take i p @ drop i p)" using list_set_sym by metis then show ?thesis by auto qed then have "∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)" using assms(2) by blast have "∧ j . j < length ?p ==> P (t_source (?p ! j))" proof - fix j assume "j < length ?p" then show "P (t_source (?p ! j))" proof (induction j) case 0 then show ?case using ‹p ! i = t0›‹P (t_source t0)› by (metis ‹i < length p› drop_eq_Nil hd_append2 hd_conv_nth hd_drop_conv_nth leD length_greater_0_conv) next case (Suc j) then have "P (t_source (?p ! j))" by auto then have "P (t_target (?p ! j))" using Suc.prems ‹∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)›[of "?p ! j"] using Suc_lessD nth_mem by blast moreover have "t_target (?p ! j) = t_source (?p ! (Suc j))" using path_source_target_index[OF Suc.prems ‹path M (target q (take i p)) ?p›] by assumption ultimately show ?case using ‹∧ t . t ∈ set ?p ==> P (t_source t) ==> P (t_target t)›[of "?p ! j"] by simp qed qed then have "∀ t ∈ set ?p . P (t_source t)" by (metis in_set_conv_nth) then show "∀ t ∈ set p . P (t_source t)" using ‹set ?p = set p› by blast then show "∀ t ∈ set p . P (t_target t)" using assms(2) by blast qed
lemma cycle_incoming_transition_ex : assumes "path M q p" and "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 then have "path M (target q (take i p)) (drop i p)" using path_suffix assms(1) by metis moreover have "t = hd (drop i p)" using ‹i < length p›‹p ! i = t› by (simp add: hd_drop_conv_nth) ultimately have "path M (target q (take i p)) [t]" by (metis ‹i < length p› append_take_drop_id assms(1) path_append_elim take_hd_drop) then have "t_source t = (target q (take i p))" by auto moreover have "t_target (last ?p) = (target q (take i p))" using ‹path M (target q (take i p)) ?p›‹target (target q (take i p)) ?p = target q (take i p)› assms(2) unfolding target.simps visited_states.simps last.simps by (metis (no_types, lifting) ‹p = take i p @ drop i p› append_is_Nil_conv last_map list.map_disc_iff) moreover have "set ?p = set p" proof - have "set ?p = set (take i p @ drop i p)" using list_set_sym by metis then show ?thesis by auto qed
ultimately show ?thesis by (metis ‹i < length p› append_is_Nil_conv drop_eq_Nil last_in_set leD) qed
lemma acyclic_paths_finite : "finite {p . path M q p ∧ distinct (visited_states q p) }" proof - have "∧ p . path M q p ==> distinct (visited_states q p) ==> distinct p" proof - fix p assume "path M q p" and "distinct (visited_states q p)" then have "distinct (map t_target p)" by auto then show "distinct p" by (simp add: distinct_map) qed then show ?thesis using finite_subset_distinct[OF fsm_transitions_finite, of M] path_transitions[of M q] by (metis (no_types, lifting) infinite_super mem_Collect_eq path_transitions subsetI) qed
lemma acyclic_no_self_loop : assumes "acyclic M" and "q ∈ reachable_states M" shows "¬ (∃ x y . (q,x,y,q) ∈transitions M)" proof assume "∃x y. (q, x, y, q) ∈ FSM.transitions M" then obtain x y where "(q, x, y, q) ∈ FSM.transitions M" by blast moreover obtain p where "path M (initial M) p" and "target (initial M) p = q" using assms(2) unfolding reachable_states_def by blast ultimately have "path M (initial M) (p@[(q,x,y,q)])" by (simp add: path_append_transition) moreover have "¬ (distinct (visited_states (initial M) (p@[(q,x,y,q)])))" using ‹target (initial M) p = q› unfolding visited_states.simps target.simps by (cases p rule: rev_cases; auto) ultimately show "False" using assms(1) unfolding acyclic.simps by meson qed
subsubsection ‹Deadlock States›
fun deadlock_state :: "('a,'b,'c) fsm ==> 'a ==> bool" where "deadlock_state M q = (¬(∃ t ∈transitions M . t_source t = q))"
lemma deadlock_state_alt_def : "deadlock_state M q = (LS M q ⊆ {[]})" proof show "deadlock_state M q ==> LS M q ⊆ {[]}" proof - assume "deadlock_state M q" moreover have "∧ p . deadlock_state M q ==> path M q p ==> p = []" unfolding deadlock_state.simps by (metis path.cases) ultimately show "LS M q ⊆ {[]}" unfolding LS.simps by blast qed show "LS M q ⊆ {[]} ==> deadlock_state M q" unfolding LS.simps deadlock_state.simps using path.cases[of M q] by blast qed
lemma deadlock_state_alt_def_h : "deadlock_state M q = (∀ x ∈inputs M . h M (q,x) = {})" unfolding deadlock_state.simps h.simps using fsm_transition_input by force
lemma acyclic_deadlock_reachable : assumes "acyclic M" shows "∃ q ∈ reachable_states M . deadlock_state M q" proof (rule ccontr) assume "¬ (∃q∈reachable_states M. deadlock_state M q)" then have *: "∧ q . q ∈ reachable_states M ==> (∃ t ∈transitions M . t_source t = q)" unfolding deadlock_state.simps by blast
let ?p = "arg_max_on length {p. path M (initial M) p}"
have "finite {p. path M (initial M) p}" by (metis Collect_cong acyclic_finite_paths_from_reachable_state assms eq_Nil_appendI fsm_initial nil path_append path_append_elim) moreover have "{p. path M (initial M) p} ≠ {}" by auto ultimately obtain p where "path M (initial M) p" and "∧ p' . path M (initial M) p' ==> length p' ≤ length p" using max_length_elem by (metis mem_Collect_eq not_le_imp_less)
then obtain t where "t ∈transitions M" and "t_source t = target (initial M) p" using *[of "target (initial M) p"] unfolding reachable_states_def by blast
then have "path M (initial M) (p@[t])" using ‹path M (initial M) p› by (simp add: path_append_transition)
then show "False" using ‹∧ p' . path M (initial M) p' ==> length p' ≤ length p› by (metis impossible_Cons length_rotate1 rotate1.simps(2)) qed
lemma deadlock_prefix : assumes "path M q p" and "t ∈ set (butlast p)" shows "¬ (deadlock_state M (t_target t))" using assms proof (induction p rule: rev_induct) case Nil then show ?case by auto next case (snoc t' p') show ?case proof (cases "t ∈ set (butlast p')") case True show ?thesis using snoc.IH[OF _ True] snoc.prems(1) by blast next case False then have "p' = (butlast p')@[t]" using snoc.prems(2) by (metis append_butlast_last_id append_self_conv2 butlast_snoc in_set_butlast_appendI list_prefix_elem set_ConsD) then have "path M q ((butlast p'@[t])@[t'])" using snoc.prems(1) by auto have "t' ∈transitions M" and "t_source t' = target q (butlast p'@[t])" using path_suffix[OF ‹path M q ((butlast p'@[t])@[t'])›] by auto then have "t' ∈transitions M ∧ t_source t' = t_target t" unfolding target.simps visited_states.simps by auto then show ?thesis unfolding deadlock_state.simps using ‹t' ∈ transitions M› by blast qed qed
lemma states_initial_deadlock : assumes "deadlock_state M (initial M)" shows "reachable_states M = {initial M}" proof - have "∧ q . q ∈ reachable_states M ==> q = initial M" proof - fix q assume "q ∈ reachable_states M" then obtain p where "path M (initial M) p" and "target (initial M) p = q" unfolding reachable_states_def by auto show "q = initial M" proof (cases p) case Nil then show ?thesis using ‹target (initial M) p = q› by auto next case (Cons t p') then have "False" using assms ‹path M (initial M) p› unfolding deadlock_state.simps by auto then show ?thesis by simp qed qed then show ?thesis using reachable_states_initial[of M] by blast qed
subsubsection ‹Other›
fun completed_path :: "('a,'b,'c) fsm ==> 'a ==> ('a,'b,'c) path ==> bool" where "completed_path M q p = deadlock_state M (target q p)"
fun minimal :: "('a,'b,'c) fsm ==> bool" where "minimal M = (∀ q ∈states M . ∀ q' ∈states M . q ≠ q' ⟶ LS M q ≠ LS M q')"
lemma minimal_alt_def : "minimal M = (∀ q q' . q ∈states M ⟶ q' ∈states M ⟶ LS M q = LS M q' ⟶ q = q')" by auto
definition retains_outputs_for_states_and_inputs :: "('a,'b,'c) fsm ==> ('a,'b,'c) fsm ==> bool" where "retains_outputs_for_states_and_inputs M S
= (∀ tS ∈transitions S . ∀ tM ∈transitions M .
(t_source tS = t_source tM ∧ t_input tS = t_input tM) ⟶ tM ∈transitions S)"
subsection ‹IO Targets and Observability›
fun paths_for_io' :: "(('a × 'b) ==> ('c × 'a) set) ==> ('b × 'c) list ==> 'a ==> ('a,'b,'c) path ==> ('a,'b,'c) path set" where "paths_for_io' f [] q prev = {prev}" | "paths_for_io' f ((x,y)#io) q prev = ∪(image (λyq' . paths_for_io' f io (snd yq') (prev@[(q,x,y,(snd yq'))])) (Set.filter (λyq' . fst yq' = y) (f (q,x))))"
lemma paths_for_io'_set : assumes "q ∈states M" shows "paths_for_io' (h M) io q prev = {prev@p | p . path M q p ∧ p_io p = io}" using assms proof (induction io arbitrary: q prev) case Nil then show ?case by auto next case (Cons xy io) obtain x y where "xy = (x,y)" by (meson surj_pair)
let ?UN = "∪(image (λyq' . paths_for_io' (h M) io (snd yq') (prev@[(q,x,y,(snd yq'))]))
(Set.filter (λyq' . fst yq' = y) (h M (q,x))))"
have "?UN = {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" proof have "∧ p . p ∈ ?UN ==> p ∈ {prev@p | p . path M q p ∧ p_io p = (x,y)#io}" proof - fix p assume "p ∈ ?UN" then obtain q' where "(y,q') ∈ (Set.filter (λyq' . fst yq' = y) (h M (q,x)))" and "p ∈ paths_for_io' (h M) io q' (prev@[(q,x,y,q')])" by auto from ‹(y,q') ∈ (Set.filter (λyq' . fst yq' = y) (h M (q,x)))› have "q' ∈ states M" and "(q,x,y,q') ∈ transitions M" using fsm_transition_target unfolding h.simps by auto
have "p ∈ {(prev @ [(q, x, y, q')]) @ p |p. path M q' p ∧ p_io p = io}" using ‹p ∈ paths_for_io' (h M) io q' (prev@[(q,x,y,q')])› unfolding Cons.IH[OF ‹q' ∈ states M›Grover's algorithm› moreover have "{(prev @ grover_state ⊆ p_io p = (x,y)#io}" open>(,x,y,q') ∈ transitions M› using cons by force timatelymaty shw "\in {prev@p | p . path M q p ∧" by blast qed then al_:
have "∧ {prev@p | p . path M q p ∧ p ∈ proof - fix pp assume "pp \<byimp_fna_e o_elpor we_e_sureea_qpo2 then taip here"p= r@pad"pth q" ad"p_op =(xy)#io stforce then tth and "p_io p' = io" by (metis (no_types, lifting) map_eq_Cons_D) then have "path M (t_target t) p'" and "t_soure q"and _inut =x =nd t_arget < states M" and "t \ _osmt_ght[f _ by auto
have "(y,t_target t) ∈ using ‹t_output t = y›t_input t = x›t_source t = q› ings moreover have H\>in states M› using \openp = t # p'›‹‹t_input t = x› opent_output t = y›‹ by auto
ultimately show "pp ∈pp = prev@p› by blast qed then ho "{rv@| . pth p<>p_ (,yio <s> ?UN"
java.lang.StringIndexOutOfBoundsException: Index 35 out of bounds for length 25
java.lang.StringIndexOutOfBoundsException: Index 84 out of bounds for length 5
then show ?case by (simp add: ‹xy = (x, y)›) qed
definition paths_for_io :: "('a,'b,'c) fsm ==> 'a ==> ('b × 'c) list ==> ('a,'b,'c) path set" where "paths_for_io M q io = {p . path M q p ∧ p_io p = io}"
lemma paths_for_io_set_code[code] : "paths_for_io M q io = (if q ∈ states M then paths_for_io' (h M) io q [] else {})" using paths_for_io'_set[of q M io "[]"] unfolding paths_for_io_def proof - ve {]@ |ps. atM s\and p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {}) <> {ps. path M q ps ∧ p_io ps = io} = (if q ∈ FSM.states M then paths_for_io' (h M) io q [] else {})" by auto havea_l*<> / 2b_ ) *cs (<> 2) cs(<> / 2 { assume "{[] @ ps |ps. path M q ps ∧ / 2) - (beta_l l) * csin (\<theta/ 2) nae" notin FSM..states M" <>q \<nSMfor_o ( M)io q [] = {[] @ p |p. path M q p ∧ by force then= (alphal) (2s \theta> / 2* cc \theta> 2) - bt_l (2 cin (\<heta = (alpha_l l) * (csin θo θ using path_begin_state by force } ultimately show "{ps. path M q ps ∧ FSM.states M then paths_for_io' (h M) io q [] else {})" by linarith
fun_t: "''b'cfm \ightarrow ('b × 'c) list ==> 'a ==>' et" wher "io_targets M io q = {target q p | p . path M q p \<and
lemma io_targets_code[code] : "io_targets M io q = image (target q) (paths_for_io M q io)" unfolding io_targets.simps paths_for_io_def by blast
lemma io_targets_states : "io_targets M io q ⊆ states M" using path_target_is_state by fastforce
lemma observable_transition_unique : assumes "observable M" and "t ∈ transitions M" shows "∃! t' ∈ transitions M . t_source t' = t_source t ∧ t_input t' = t_input t ∧ '=t_otpt " by (metis assms observable.elims(2) prod.expand)
lemma obeaet_nqe: ssumes"obsvale M"
and "aO*a_ \^m N" and "p_io p = p_io p'" shows "p = p'" proof - using assms(4) map_eq_ "uni mt_P then show ?thesis using\open p = p_io p'›‹‹ proof (induction p p' arbitrary: q rule: list_induct2) case Nil heno ?caseby uto next case (Cons x xs y ys) then have *: "x ∈va1 { .< \vars2 by auto enattgt =tr assmsbservable(t then have "x = y" p rd.epad
have "p_io xs = p_io ys" using Cons by auto
have "path M (t_target x) xs" using Cons by auto using Cons ‹uto ultimately have "xs = ys" using Cons by auto
nd <x = y› by simp apply (subst nths_ped) ed
lemma observable_io_targets : assumes "observable M and "io ∈ LS M q" obtains q' where "io_targets M io q = {q'}" proof -
obtain p wheunfoldipsPd_e _Pds_def P.nsvar'usng psP_ oinp_P1ya using assms(2) ssume m1 \in carrier_mat (2^n) (2^n)" hen a "trgt p <_agetsMio " by auto
have "∃
java.lang.StringIndexOutOfBoundsException: Index 21 out of bounds for length 21 ume"¬ exists> q' . q' ≠ io_targets M io q" proof<>oyo he o\> have "¬ {target q p}" using ‹q'. io_targets M io q {q'}})\close> \open>arget q p ∈ io_targets M io q›blst then show ?thesis by blast qed enbanq'werq <> agt n <i i_tresMo q" tensor_mat_carrierf\^m st2.d2"] then obtsubgo nfldinprilsate.d2_ aialsatedms2efs2Pnthvrs'ps_Pdim2efdims_as ato
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 using ‹ary_ex_mat_O
java.lang.StringIndexOutOfBoundsException: Index 29 out of bounds for length 22 using observable_path_unique[OF assms(1 \open at while loop› hen ow"Fle" using ‹ qed
then show ?thesis using that by blast qed
lemma osevalepat_io_targe assumes "observabl M" and "path M q p" shows "io_tarsthen shw casapysmapl ruleqmtI) auto usingervable_io_targetsFasm()lnugttimn[Fasm(2 f "_i "] singletonD[of "target q p"] unfolding io_targets.simps proof - assume ashow ?ce apl sip)unfldgs2por_a_ef assume "∧q'. {target q pa |pa. path M q pa ∧p}= q}\Longrightarrow thesis] thesis" then obtain aa :: 'a w apply (sbstn) by meson then show "{target q ps |ps. path M q ps ∧lloi: using a1 assms(2) by blast qed
e_path_language_step assumes "observable M" athMqp and "¬transitions M. t_source t = target q p ∧ t_input t = x ∧ t_output t = y)" shows "(p_io p)@[(x,y)] ∉ using assms proof (induction p rule: case Nil show caseo assume "p_io [] @ [(x, y)] ∈ inw pt Mqp npo '=[xy)"ufligL.sps by force then obtain t where "p' = [t]" by blasthave1:"td " have "t∈transitions M" and "t_source t = target q[] using ‹p' = [t]› by auto moreover nt\Rightarrow olmtwhr ing<>p '=[(,y\close‹ b at ultimately show "False" using Nil.prems(3) by blast qed next case hv"0< k} ∪ {Suc k} = {0..<(Suc (Suc k))}" by auto from ‹==> exH_kk=pa_xenids 0<uk (u ).n} (H_k k)" and "t ∈ antins" by ints1tasaedms{c " {(u(u ).n}
show ?case proof assume "p_io (p @ [t]) @ [(x, y)] ∈ LS M q" then obtain p' where "path M q p'" and "p_io p' = p_io (p @ [t]) @ [(x, y)]" by auto then obtain p'' t' t'' where "p' = p' aapply unfold_locales by ato by (metis (no_types, lifting) append.assoc map_butlast map_is_Nil_conv sn intre s:paril_a dis"0Suc (uc k)}" "{Suc (Suc k)..<n}" enhv ah q'' using ‹ {Suc (Suc k)..<n} = {Suc k..<n}" using Suc by auto have "p_io p'' = p_io p" using ‹n = {Suc k..<n"uigSc(2)b uo then have "p'' = p" using observable_path_unique[OF assms(1) ‹path M q p›] by blast
have "t_source t' = target q p''" an"' \in transitions M" using ‹p' = p''@[t']@[t'']› by auto then have "t_source t' = t_source t" using \open=\close> \opent t = target q p› by auto moreover have "t_input t' = t_input t ∧ t_output t' = t_output t"
java.lang.NullPointerException ultimately have "t' = t" using ‹fiedsltst by (meson prod.expand)
have "t'' ∈usiScleghi yao sing\> M q p'›p' = p''@[t']@[t'']›‹‹ moreover have "t_input t'' x \and t_output t'' = y" using ‹ ultimately show "False" using snoc.apply nol_cl buo qed qed
lemma assumes "io1 @ io2 ∈ LS M q1" and beal " and "q2 ∈ shows "io2 ∈ LS M q2" proof - obtain p1 p2 where "path M q1 p1" and "path M (target q1 p1) p2" 1 d"_op= o" using language_state_split[OF assms(1)] by blast enave"o in>> LS M q1" and "io2 \> Mtret 1"
java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2 have "target q1 p1 ∈ using ‹ unfoldingi_tretsmsb ls then have "target q1 p1 = q2" singobervleiotaetsOFsm( \open∈ LS M q1› by (metis assms(3) singletonD) then show ?thesis using ‹ngHe__[ "u " assb uto qed
lemma io_targets_language_append : assumes "q1 ∈ io_targets M io1 q" and "io2 \ haeqm "Hku)=mtetnindi .<m _ m shows "io1@io2 ∈ proof - obtain p1 where "path M q p1" and "p_io p1 = io1" and "t using m by auto using assms(1) by auto moreover obtain p2 where "path M q1 p2" and "p_io p2 = io2" using assms(2) by auto timatelyve"ah (1)"and"_io(pp) o@i" auto then show ?thesis using language_state_confu ket_zer : "nt\Rightarrow complex vec" where qed
lemma io_targets_next : assumes "t ∈ shows "io_targets M io (t_target t) ⊆ io_targets M (p_io [t] @ io) (t_sure ) unfolding io_targets.simps proof fix q assume "q ∈ {target (t_target) p|.pt (taet>p_io p = io}"
java.lang.NullPointerException by auto then have "path M (t_source t) (t#p) ∧ using FSM.path.cons[OF assms] by auto then show "q \<in by blast qed
lemma observable_io_targets_next : assumes "observable M" and "t ∈ transitions M" shows "io_targets M (p_io [t] @ io) (t_source t) = io_targets M io (t_target t)" proof show "io_targets M (p_io [t] @ io) (t_source t) ⊆ proof fix q assume "q ∈e(u )2=iieco[2](id ( k) enota pher " = aret(_suret)p and "path M (t_source t) p" i t @ o olding_aretip byba then have "q = t_target (last p)" unfolding target.simps vi then h havk " <at using last_map by auto
obtain t' p' where "p = t' # p'" using ‹k} ==> {y ∈(Suc k)}. y < x} = {0..<x})" by auto henhae t \in> taniiosM nd"tsoore tsourc t" <path M (t_source t) p› by auto moreover have "t_input t' = t_input t" and "t_output t' = t_output t" using ‹p_io p = p_io [t] @ io› by auto ultimately have "t' = t" g<>t ntransitions M›observable M› unfolding obsevabesms by (meson prod.expand)
then have "path M (t_target t) p'" using ‹ moreover have "p_io p' = io" ingn <>p_io p p_i t i\close><opp ='#p\closeby auto moreover have "q = target using ‹ ultimately show "q ∈ carrier_vec (2^(Suc (Suc k)))" using ket_plus_k_dim[OF Suc(2)] by auto by auo qed
showirgts M i (t_targargget t) ⊆ singingg o_o_tarrets_nextOF assasms2)] by asumptin qed
lemma observable_language_target : assumes "observable M" and "q ∈ io_targets io ita M" and "t ∈trgsTo iital) and "L T \<subseteq shows proof fix2sme" \<n T t" then obtain pT2 where "path T t pT2" and "p_io pT2 = io2" by aut obtain pT1 where "p - using ‹ by auto then have "path T (initial T) (pT1@pT2)" using <>pat T\close using path_append by metis moreover have "p_i using ‹ ultimately have "io1@io2 ∈os )(prj_ l"ufldigpojsileb uo using language_state_c then have "io1@io2 \<n
java.lang.NullPointerException then obtain pM where "path M (initial M) pM" and "p_io pM = io1@io2" by aut using proj_psi_proj_k byaut
let ?pM1 = "take (length io1) pM" ?plnth o) "
eh iia ) p1?pM) using ‹x_sumd(🚫k. tensor_P (1m N) (proj_k k)) R ≤1<^sb>m "b ato then have "path M (initial M) ?pM1" and "path M (target (initial M) ?pM1) ?pM2" by blast+ eop1=i1 using ‹ by (metis append_eq_conv_conj take_map) have "p_io ?pM2 = io2" using ‹ i = 0 then ee )" by (metis append_eq_conv_conj drop_map)
obtain pM1 where "path M (initial M) pM1" and "p_io pM1 = io1" and "target (initial M) pM1 = q"(tensor_PP\^> K) * exexH_k (n - 1) = 2 ⋅m tensor_P proj_psi (1<subm ) --\sub>m d" using ‹
have "pM1 = ?pM1" bservable_path_unique >observble M<> <pe>pM (initial M) pM1›‹path M (initial M) ?pM1› unfolding>ppM1 = io1›‹
then have "path M q ?pM2" using ‹path M (target (initial M) ?pM1 shshow "tensor_P (xHn * \cdotm N) * exH_n) (1\<^sub>m tensor_P proj_psi (1m d" then show "io2 ∈ using language_state_containment[OF _ ‹ qed
lemma observable_language_target_failure : assumes "observable M" and "q ∈m N)" and "t ∈ and "¬ LS M q" shows "¬ L M" using observable_language_target[OF assms(1,2,3)] assms(4) by blast
lemma language_path_append_transition_observable : assumes "(p_io p) @ [(x,y)] ∈ and m K) - 1\<^> and "observable M" obtains t where "path M q (p@[t])" and "t_input t = x" and "t_output t = y" proof - obtain p' t where "path M q (p'@[t])" and "p_io (p'@[t]) = (p_io p) @ [(x,y)]" using language_path_append_transition[OF assms(1)] by blast then have "path M q p'" and "p_io p' = p_io p" and "t_input t = x" and "t_output t = y"
have "p' = p" using observable_path_unique[OF assms(3) ‹ then have "path M q (p@[t])" using ‹ by auto then show ?thesis using that ‹m K) - 1\<^sub>m tensor_P proj_psi (1m d)) qed
mmaanguage_io_target_append: assumes "q' ∈ and "io2 ∈ LS M q'" shows hoa proof - obtain p2 where "path M q' p2" and "p_io p2 = io2" using assms(2) by auto
moreover obtain p1 where "q' = target q p1" and "path M q p1" and "p_io p1 = io1" using assms(1) by a uo
ultimately show ?thesis unfolding LS.simps by (metis (mono_tags, lifting) map_append mem_Collect_eq path_append) qed
ervable_path_suffix assumes "(p_io p)@io \ {adjoint H *(djoit?Ph (aoint Q ?H) * ?Ph ?H andand "pthM qp and "observable M" obtains p' where "path M (target q p) p'" and "p_io p' = io" proof - obtain p1 p2 where "path M q p1" and "path M (target q p1) p2" and "p_io p1 = p_io p" and "p_io p2 = io" using lnguae_state_sspplit[F ssms(1)]b las
have "p1 = p" using observable_path_unique[OF assms(3,2) ‹ by simp
show ?thesis using that[of p2] ‹ by blast qed
lemma io_targets_finite : " _1ps__2uig 1dim adjoionhermn_M1[unfoldedhritian_def] by auto proof have "(io_targets M i unfolding io_targets.simps length_map[of "(λ t . (t_input t, t_output t))", symmetric] by force moreover have "finite {target q p | p . ls have "\<dots matrix_sum d (λrj_s_l k)(roj_k k)) " using paths_finite[of M q "length io"] by simp ultimately show ?thesis using rev_finite_subset by blast qed
lemma language_next_transition_ob : assumes "(x,y)#ios ∈ obtains t where "t_source t = q" and "t ∈ and "t_input t = x" lemma P''__Q_le_on: and "ios ∈ LS M (t_target t)" proof - obtain p where "path M q p" and "p_io p = (x,y)#ios" using assms unfolding LS.simps mem_Collecteq by (metis (no_types, lifting)) then obtain t p' where "p = t#p'" by blast
ource
java.lang.NullPointerException and "path M (t_target t) p'" using ‹ moreover h"tinipt t " and "t_output t = y" and "p_io p' = ios" using ‹ d_Q ultimately show ?thesis using that[of t] by auto qed
lemma h_observable_card : assumes "observable M" shows "card (snd ` Set.fil = enso_ 1<m N) (adjoint (mat_incr K))" and "finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))" proof - have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q') ∈ unfolding h.simps by force moreover have "{q' . (q,x,y,q') ∈ transitions M} = {} ∨_roef_righh_a[o _ ]) using assms unfolding observable_alt_def by blast ultimately show "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≤ 1" and "finite (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)))" by auto qed
lemma h_obs_None : assumes "observable M" shows "(h_obs M q x y = None) = (∄q' . (q,x,y,q') ∈ transitions M)" proof show "(h_obs M q x y = None) ==>q' . (q,x,y,q') ∈ roof applybss_P.tor__mat_doint) then have "card (snd ` Set.filter (λPs_d _P_d2byato by auto then have "card (snd ` Set.filter (λ,q) . y' = y)(h M (q,))= 0 using h_observable_card(1)[OF assms, of y q x] by presburger ave"d`Setitr(\lambda (y',q') . y' = y) (h M (q,x))) = {}" using h_observable_card(2)[OF assms, of y q x] card_0_eq[of "(snd ` Set.filter (λ(y', q'). y' = y) (h M (q, x)))"] by bl also have "… then show ?thesis unfolding h.simps by force qed show "(∄q' . (q,x,y,q') ∈m tno_(1) proof - assume "(∄ then have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {}" unfolding h.simps by force then ve "ad (snd `Set.filr \lambda (y',q') . y' = y) (h M (q,x))) = 0" by (simp add: card_eq_0_iff) then show ?thesis unfolding h_obs_simps Let_def ‹snd ` Set.filter (λ unfolding exP0_P'' exP_Quigq_P'_Q by aut by auto qed qed
lemma h_obs_Some :
shows "(h_obs M q x y = Some q') = ({q' . (q,x,y,q') ∈moreover have "well_com (Utrans_P vars1 mat_O;; hadamard_n n)" proof have *: "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) = {q' . (q,x,y,q') ∈ transitions M}" foldingig h.sps b oc
show "h_obs M q x y = Some q' ==> ({q' . (q,x,y,q') ∈ transitions M} = {q'})" proof - assume "h_obs M q x y = Some q'" then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) ≠l. tensor_P (proj_psi_l l) (proj_k l)) (R + 1)" by (auto simp add: card_1_singleton_iff split: if_splits) then have "card (snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) > 0" unfolding h_simps using fsm_transitions_finite[of M] by (metis assms card_0_eq h_observable_card(2) h_simps neq0_conv) moreover have "card (snd ` Set.filter (λ (y',') . y' = y hM (q,x))) \<le using assms unfolding observable_alt_def h_simps by (metis assms h_observable_card(1) h_simps) nd` Set.filter (\<lambda by auto then have "(snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))) = {q'}" using ‹ ygletonE onoponn.iecttlem_q then show ?thesis *nfoldingfdin hsmp y bst qed
show "({q' . (q,x,y,q') ∈ proof - assume "({q' . (q,x,y,q') ∈ transitions M} = {q'}) then have "snd ` Set.filter (λv β = β" unfolding h.simps by force then sow ?thesis unfolding Let_def by simp qed qed
lemma h_obs_state : assumes "h_obs M q x y = Some q'" shows "q' ∈ proof (cases "card (snd ` Set.filter (λ_dim by auto case True then have "(snd ` Set.filter (λ"proj_pil R * poj_p_ R roj_psi_l R using ‹ by (metis card_1_singletonE option.inject the_elem_eq) then have "(q,x,y,q') ∈ = post * (post - ?R) - ?R * (post - ?R)" unfolding h_simps by auto then show ?thesis by (metis fsm_transition_target snd_conv) proo - case False then have "h_obs M q x y = None" usingFseunflding _obsimps e_ef uo then show ?thesis using assms by auto qed
fun after :: "('a,'b,'c) fsm ==> 'a ==> ('b × "after M q [] = q" | "after M q ((x,y)#io) = after M (the (h_obs M q x y)) io"
(*abbreviation(input) "after_initial M io \<equiv> after M (initial M) io" *) abbreviation "after_initial M io ≡
lemma after_path : assumes "observable M" and "path M q p" shows "after M q (p_io p) = target q p" using assms(2) proof (induction p arbitrary: q rule: list.induct) case Nil en shw?ase bauto next case (Cons t p) then have "t ∈ transitiot pult_tes by auto
have "∧ q' . (q, t_input t, t_output t, q') ∈ FSM.transitions M ==> q' using observable_transition_unique[OF assms(1) ‹ using ‹ then have "({q'. (q, t_input t, t_output t, q') ∈ using ‹ post_fst_k (Suc i) = testN + pst_f_k i" then have "(h_obs M q (t_input t) (t_output t)) = Some (t_target t)" using h_obs_Some[OF assms(1), of q "t_input t" "t_output t" "t_target t"] byg less_antisym y fastfor then have "after M q (p_io (t#p)) = after M (t_target t) (p_io p)" by auto moreover have "target (t_target t) p = target q (t#p)" using ‹ ultimately show ?case using Cons.IH[OF ‹ by simp qed
lemma obser observable_after_path : ssumes "observabe M tensor_Pt (1su>m K)" for k obtains p where "path M q p" and "p_io p = io" and "target q p = after M q io" using after_path[OF assms(1)] using assms(2) by auto
lemma h_obs_from_LS : assumes "observable M" and "[(x,y)] ∈ obtains q' where "h_obs M q x y = Some q'" using assms(2) h_obs_None[OF assms(1), of q x y] by force
lemma after_h_obs : assumes "observable M" and "h_obs M q x y Soe q'" shows "after M q [(x,y)] = q'" proof - have "path M q [(q,x,y,q')]" using assms(2) unfolding h_obs_Som[O asm(1)) ition_pathyfasfoce then show ?thesis using assms(2) after_path[OF assms(1), of qed
lemma after_h_obs_prepend : assumes "observable M" and "h_obs M q x y = Some q'"
java.lang.NullPointerException shows "after M q ((x,y)#io) = after M q' io" proof - obtain p where "path M q' p" and "p_io punfM Post_f sing enso_P_testN_smq_ot y auo using assms(3) by auto then have "after M q' io = target q' p" using after_path[OF assms(1)] by blast
have 1D using assms(2) path_prepend_t[OF ‹ moreover have "p_io ((q,x,y,q')#p) = (x,y)#io" using ‹ vars2 M0 M1 D;; using after_path[OF ass1), of q "(q,y,q')#p" by s moreover have "t e \Turnstile>\<^ubp ultimately show ?thesis using ‹after M q' io = target q' p› by simp qed
lemma after_split : assumes " M"
and "α@γ ∈ LS M q"
"after M (after M q α) γ = after M q (α @ γ)"
-
obtain p1 p2 where "path M q p1" and "path M (target q p1) p2" and "p_io p1 = α" and "p_io p2 = γ"
using language_state_split[OF assms(2)]
by blast
then have "path M q (p1@p2)" and "p_io (p1@p2) = (α @ γ)"
by auto
then have "after M q (α @ γ) = target q (p1@p2)"
using assms(1)
by (metis (mono_tags, lifting) after_path)
moreover have "after M q α = target q p1"
using ‹path M q p1›‹p_io p1 = α› assms(1)
by (metis (mono_tags, lifting) after_path)
moreover have "after M (target q p1) γ = target (target q p1) p2"
using ‹path M (target q p1) p2›‹p_io p2 = γ› assms(1)
by (metis (mono_tags, lifting) after_path)
moreover have "target (target q p1) p2 = target q (p1@p2)"
by auto
ultimately show ?thesis
by auto
after_io_targets :
assumes "observable M"
and "io ∈ LS M q"
"after M q io = the_elem (io_targets M io q)"
-
have "after M q io ∈ io_targets M io q"
using after_path[OF assms(1)] assms(2)
unfolding io_targets.simps LS.simps
by blast
then show ?thesis
using observable_io_targets[OF assms]
by (metis singletonD the_elem_eq)
after_language_subset :
assumes "observable M"
and "α@γ ∈ L M"
and "β ∈ LS M (after_initial M (α@γ))"
"γ@β ∈ LS M (after_initial M α)"
by (metis after_io_targets after_split assms(1) assms(2) assms(3) language_io_target_append language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)
after_language_append_iff :
assumes "observable M"
and "α@γ ∈ L M"
"β ∈ LS M (after_initial M (α@γ)) = (γ@β ∈ LS M (after_initial M α))"
by (metis after_io_targets after_language_subset after_split assms(1) assms(2) language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)
h_obs_language_iff :
assumes "observable M"
shows "(x,y)#io ∈ LS M q = (∃ q' . h_obs M q x y = Some q' ∧ io ∈ LS M q')"
(is "?P1 = ?P2")
show "?P1 ==> ?P2"
proof -
assume ?P1
then obtain t p where "t ∈ transitions M"
and "path M (t_target t) p"
and "t_input t = x"
and "t_output t = y"
and "t_source t = q"
and "p_io p = io"
by auto
then have "(q,x,y,t_target t) ∈ transitions M"
by auto
then have "h_obs M q x y = Some (t_target t)"
unfolding h_obs_Some[OF assms]
using assms by auto
moreover have "io ∈ LS M (t_target t)"
using ‹path M (t_target t) p›‹p_io p = io›
by auto
ultimately show ?P2
by blast
qed
show "?P2 ==> ?P1"
unfolding h_obs_Some[OF assms] using LS_prepend_transition[where io=io and M=M]
by (metis fst_conv mem_Collect_eq singletonI snd_conv)
after_language_iff :
assumes "observable M"
and "α ∈ LS M q"
"(γ ∈ LS M (after M q α)) = (α@γ ∈ LS M q)"
by (metis after_io_targets assms(1) assms(2) language_io_target_append observable_io_targets observable_io_targets_language singletonI the_elem_eq)
(* TODO: generalise to non-observable FSMs *) lemma language_maximal_contained_prefix_ob : assumes"io ∉ LS M q" and"q ∈ states M" and"observable M" obtains io' x y io'' where"io = io'@[(x,y)]@io''" and"io' ∈ LS M q" and"io'@[(x,y)] ∉ LS M q" proof - have"∃ io' x y io'' . io = io'@[(x,y)]@io'' ∧ io' ∈ LS M q ∧ io'@[(x,y)] ∉ LS M q" using assms(1,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 assumes defined_inputs M1 q1 and<efined_inputs obtains y where"[(x,y)] ∈ using ass nodng fndipt_a_f proof -
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 assume a2: "x ∈ FSMtransitions t_source t } assume a3: "\Andy. [(x, y)] ∈ hss \p ∈ t_our= 2
obtain pp :: "'a ==> 'times'a × 'c ×
<. ((∄ p ∈ t_source a = t_input (pp pp a ∈ t_source (pp )>((∃inputp\and p ∈and t_source1or (∀ t_input p ∨notin FSM.transitions M1or t_source p ≠
youra thenhave"x=_inpup x) ∧pp x ∈ FSM.transitions M1 ∧ using a2 by blast lemm scalar_compat' [s]: using f4 a3 by (metis (no_types) DiffI LS_single_transition) qed
lemma language_path_append : assumes "path q1p1 and" ∈ shows "(p_io p1 @ io) ∈ proof - obtain p2 where"path M1 (target q1 p1) p2"and"p_io p2 = io" using ex_cardS⊆ thenhave"path M1 q1 (p1@p2)" using assms(1) by auto moreoverhave"p_io (p1@p2) = (p_io p1 @ io)" using‹
S <ge2" | "infinite S"
by (metis (mono_tags, lifting) language_intro)
observable_defined_inputs_diff_ob :
assumes "observable M1"
and "observable M2"
and "path M1 q1 p1"
" "path M2 q2p"
and "p_io p1 = p_io p2"
and "x ∈
and "x ∉ defined_inputs M2 (target q2 p2)"
y where "(p_io p1)@[(x,y)] ∈
java.lang.StringIndexOutOfBoundsException: Index 52 out of bounds for length 7
obtain y where "[(x,y)] ∈ LS M1 (target q1 p1) - LS M2 (target q2 p2)"
using defined_inputs_language_diff[OF assms(6,7)] by blast
then have "(p_io p1)@[(x,y)] ∈ LS M1 q1"
using language_path_append[OF assms(3)]
by blast
moreover have "(p_io p1)@[(x,y)] ∉ LS M2 q2"
by (metis (mono_tags, lifting) DiffD2 ‹[(x, y)] ∈ LS M1 (target q1 p1) - LS M2 (target q2 p2)› assms(2) assms(4) assms(5) language_state_containment observable_path_suffix)
ultimately show ?thesis
using that[of y] by blast
observable_defined_inputs_diff_language :
assumes "observable M1"
and "observable M2"
and "path M1 q1 p1"
and "path M2 q2 p2"
and "p_io p1 = p_io p2"
and "defined_inputs M1 (target q1 p1) ≠
"LS M1 q1 ≠
-
obtain x where "(x ∈p)) ∨ dfiied_ipusM (tret q2 p) - dined_input M (tare q1 1)
using asm b blast
then consider "(x ∈ (tre 2p)" |
"(x ∈*S› by blast thenshow ?thesis proof cases case1 thenshow ?thesis using observable_defined_inputs_diff_obopen algebra (locale)› next case2 thenshow ?thesis using observable_defined_inputs_diff_ob[OF assms(2,1,4,3) assms(5)[symmetric], of x] byast qed qed
fun maximal_prefix_in_language :: "('a,'b,'c) fsm ==>times>'c)list ==> ('b × "maximal_prefix_in_language M q [][]]java.lang.StringIndexOutOfBoundsException: Index 44 out of bounds for length 44
maximal_prefix_in_language)caseobsq x y of
None [] |
Some q' java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
lemma_language_properties assumes"observable M" and"q ∈L a b ∈ b = a""∀y∈<> b \longrightarrow y = divL a b" shows"maximal_prefix_in_language M q io ∈ LS M q" andjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 proof - have"ximal_prefix_in_language l_pefix_nlnug o in LS <> mxmlpei_n_language M q i <i>lis.e peie o) using assms(2) proof (induction io arbitrary: q) case l en ow ?ae by auo next case (Cons xy io)
obtain x y where "y = (,)
ing
show ?caseproof (cases "h_obs M q x y")
b thenhave"maximal_prefix_in_language M q yio ]" unfolding‹ byauto thenshow?thesisixassume"\in>S\<and>a=y\<Zspot>b" by(metis(mono_tags,lifting)Cons.premsappend_self_conv2from_FSM_languagenguage_contains_empty_sequencens_empty_sequencepty_sequenceequencece_llect_eq_qrefixes_sets_setet next case(me) thenhave*:"maximal_prefix_in_languageMq(xy#io)=(x,y)#maximal_prefix_in_languageMq'io" unfolding\<open>xy=(x,y)\<close> byauto
have"maximal_prefix_in_languageMq(xy#io)\<in>LSMq" unfoldinglding singingSomemeopenmaximal_prefix_in_languageMq'io\<in>LSMq'\<close> by(mesonassms(1)h_obs_language_iff) moreoverhave"maximal_prefix_in_languageMq(xy#io)\<in>list.set(prefixes(xy# unfolding* unfolding\<open>xy=(x,y)\<close> usingopenMq'io\<in>list.set(prefixesio)\<close>append_Cons unfoldingprefixes_setfixes_set auto ultimatelyshow?thesis byblast qed qed thenshow"maximal_prefix_in_languageMqio\<n>LSMq" and"maximal_prefix_in_languageMqio\<in>list.set(prefixesio)" qed
(* 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 thenshow ?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 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 thenhave 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 moreoverhave **: "∧ 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 thenhave"{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 moreoverhave"finite (image t_output (fsm_impl.transitions A))" using p5a by auto ultimatelyshow"finite ({y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ fsm_impl.transitions A})" by (simp add: finite_subset) qed ultimatelyhave"finite ?distinguishing_transitions_lr" unfolding * distinguishing_transitions_def by force moreoverhave"finite ?shifted_transitions'" unfolding shifted_transitions_def using p5b by auto ultimatelyhave"finite ?ts"by blast thenhave 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 moreoverhave"∧ 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 ultimatelyhave"∧ t . t ∈ ?ts ==> t_source t ∈ fsm_impl.states ?P ∧ t_target t ∈fsm_impl.states ?P" by blast moreoverhave"∧ 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 thenshow"∧ 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 moreoverhave"∧ 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 ultimatelyhave 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)+
end
Messung V0.5 in Prozent
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.531Angebot
¤
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.