section ‹Product Machines› text ‹This theory defines the construction of product machines. A product machine of two finite state machines essentially represents all possible parallel executions of those two machines.› theory Product_FSM imports FSM begin lift_definition product :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('a × 'd,'b,'c) fsm" is FSM_Impl.product proof - fix A :: "('a,'b,'c) fsm_impl" fix B :: "('d,'b,'c) fsm_impl" assume "well_formed_fsm A" and "well_formed_fsm B" then have p1a: "fsm_impl.initial A ∈ fsm_impl.states A" and p2a: "finite (fsm_impl.states A)" and p3a: "finite (fsm_impl.inputs A)" and p4a: "finite (fsm_impl.outputs A)" and p5a: "finite (fsm_impl.transitions A)" and p6a: "(∀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.product A B" have "fsm_impl.initial ?P ∈ fsm_impl.states ?P" using p1a p1b by auto moreover have "finite (fsm_impl.states ?P)" using p2a p2b by auto moreover have "finite (fsm_impl.inputs ?P)" using p3a p3b by auto moreover have "finite (fsm_impl.outputs ?P)" using p4a p4b by auto moreover have "finite (fsm_impl.transitions ?P)" using p5a p5b unfolding product_code_naive by auto moreover have "(∀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)" using p6a p6b by auto ultimately show "well_formed_fsm (FSM_Impl.product A B)" by blast qed abbreviation "left_path p ≡ map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p" abbreviation "right_path p ≡ map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p" abbreviation "zip_path p1 p2 ≡ (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))" lemma product_simps[simp]: "initial (product A B) = (initial A, initial B)" "states (product A B) = (states A) × (states B)" "inputs (product A B) = inputs A ∪ inputs B" "outputs (product A B) = outputs A ∪ outputs B" by (transfer; simp)+ lemma product_transitions_def : "transitions (product A B) = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}" by (transfer; simp)+ lemma product_transitions_alt_def : "transitions (product A B) = {((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB)) | tA tB . tA ∈ transitions A ∧ tB ∈ transitions B ∧ t_input tA = t_input tB ∧ t_output tA = t_output tB}" (is "?T1 = ?T2") proof - have "⋀ t . t ∈ ?T1 ⟹ t ∈ ?T2" proof - fix tt assume "tt ∈ ?T1" then obtain qA qB x y qA' qB' where "tt = ((qA,qB),x,y,(qA',qB'))" and "(qA,x,y,qA') ∈ transitions A" and "(qB,x,y,qB') ∈ transitions B" unfolding product_transitions_def by blast then have "((t_source (qA,x,y,qA'), t_source (qB,x,y,qB')),t_input (qA,x,y,qA'), t_output (qA,x,y,qA'), (t_target (qA,x,y,qA'), t_target (qB,x,y,qB'))) ∈ ?T2" by auto then show "tt ∈ ?T2" unfolding ‹tt = ((qA,qB),x,y,(qA',qB'))› fst_conv snd_conv by assumption qed moreover have "⋀ t . t ∈ ?T2 ⟹ t ∈ ?T1" proof - fix tt assume "tt ∈ ?T2" then obtain tA tB where "tt = ((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB))" and "tA ∈ transitions A" and "tB ∈ transitions B" and "t_input tA = t_input tB" and "t_output tA = t_output tB" by blast then have "(t_source tA, t_input tA, t_output tA, t_target tA) ∈ transitions A" and "(t_source tB, t_input tA, t_output tA, t_target tB) ∈ transitions B" by (metis prod.collapse)+ then show "tt ∈ ?T1" unfolding product_transitions_def ‹tt = ((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB))› by blast qed ultimately show ?thesis by blast qed lemma zip_path_last : "length xs = length ys ⟹ (zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])" by (induction xs ys rule: list_induct2; simp) lemma product_path_from_paths : assumes "path A (initial A) p1" and "path B (initial B) p2" and "p_io p1 = p_io p2" shows "path (product A B) (initial (product A B)) (zip_path p1 p2)" and "target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)" proof - have "initial (product A B) = (initial A, initial B)" by auto then have "(initial A, initial B) ∈ states (product A B)" by (metis fsm_initial) have "length p1 = length p2" using assms(3) using map_eq_imp_length_eq by blast then have c: "path (product A B) (initial (product A B)) (zip_path p1 p2) ∧ target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)" using assms proof (induction p1 p2 rule: rev_induct2) case Nil then have "path (product A B) (initial (product A B)) (zip_path [] [])" using ‹initial (product A B) = (initial A, initial B)› ‹(initial A, initial B) ∈ states (product A B)› by (metis Nil_is_map_conv path.nil zip_Nil) moreover have "target (initial (product A B)) (zip_path [] []) = (target (initial A) [], target (initial B) [])" using ‹initial (product A B) = (initial A, initial B)› by auto ultimately show ?case by fast next case (snoc x xs y ys) have "path A (initial A) xs" using snoc.prems(1) by auto moreover have "path B (initial B) ys" using snoc.prems(2) by auto moreover have "p_io xs = p_io ys" using snoc.prems(3) by auto ultimately have *:"path (product A B) (initial (product A B)) (zip_path xs ys)" and **:"target (initial (product A B)) (zip_path xs ys) = (target (initial A) xs, target (initial B) ys)" using snoc.IH by blast+ then have "(target (initial A) xs, target (initial B) ys) ∈ states (product A B)" by (metis (no_types, lifting) path_target_is_state) then have "(t_source x, t_source y) ∈ states (product A B)" using snoc.prems(1-2) by (metis path_cons_elim path_suffix) have "x ∈ transitions A" using snoc.prems(1) by auto moreover have "y ∈ transitions B" using snoc.prems(2) by auto moreover have "t_input x = t_input y" using snoc.prems(3) by auto moreover have "t_output x = t_output y" using snoc.prems(3) by auto ultimately have "((t_source x, t_source y), t_input x, t_output x, (t_target x, t_target y)) ∈ transitions (product A B)" unfolding product_transitions_alt_def by blast moreover have "t_source x = target (initial A) xs" using snoc.prems(1) by auto moreover have "t_source y = target (initial B) ys" using snoc.prems(2) by auto ultimately have "((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y)) ∈ transitions (product A B)" using ‹(t_source x, t_source y) ∈ states (product A B)› by simp then have ***: "path (product A B) (initial (product A B)) ((zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))])" using * ** by (metis (no_types, lifting) fst_conv path_append_transition) have "t_target x = target (initial A) (xs@[x])" by auto moreover have "t_target y = target (initial B) (ys@[y])" by auto ultimately have ****: "target (initial (product A B)) ((zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))]) = (target (initial A) (xs@[x]), target (initial B) (ys@[y]))" by fastforce have "(zip_path [x] [y]) = [((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))]" using ‹t_source x = target (initial A) xs› ‹t_source y = target (initial B) ys› by auto moreover have "(zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])" using zip_path_last[of xs ys x y, OF snoc.hyps] by assumption ultimately have *****:"(zip_path (xs@[x]) (ys@[y])) = (zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))]" by auto then have "path (product A B) (initial (product A B)) (zip_path (xs@[x]) (ys@[y]))" using *** by presburger moreover have "target (initial (product A B)) (zip_path (xs@[x]) (ys@[y])) = (target (initial A) (xs@[x]), target (initial B) (ys@[y]))" using **** ***** by auto ultimately show ?case by linarith qed from c show "path (product A B) (initial (product A B)) (zip_path p1 p2)" by auto from c show "target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)" by auto qed lemma paths_from_product_path : assumes "path (product A B) (initial (product A B)) p" shows "path A (initial A) (left_path p)" and "path B (initial B) (right_path p)" and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)" and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)" proof - have "path A (initial A) (left_path p) ∧ path B (initial B) (right_path p) ∧ target (initial A) (left_path p) = fst (target (initial (product A B)) p) ∧ target (initial B) (right_path p) = snd (target (initial (product A B)) p)" using assms proof (induction p rule: rev_induct) case Nil then show ?case by auto next case (snoc t p) then have "path (product A B) (initial (product A B)) p" by fast then have "path A (initial A) (left_path p)" and "path B (initial B) (right_path p)" and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)" and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)" using snoc.IH by fastforce+ then have "t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))" using snoc.prems by (metis (no_types, lifting) path_cons_elim path_suffix prod.collapse) have ***: "target (initial A) (left_path (p@[t]))= fst (target (initial (product A B)) (p@[t]))" by fastforce have ****: "target (initial B) (right_path (p@[t]))= snd (target (initial (product A B)) (p@[t]))" by fastforce have "t ∈ transitions (product A B)" using snoc.prems by auto then have "(fst (t_source t), t_input t, t_output t, fst (t_target t)) ∈ transitions A" unfolding product_transitions_alt_def by force moreover have "target (initial A) (left_path p) = fst (t_source t)" using ‹t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))› by auto ultimately have "path A (initial A) ((left_path p)@[(fst (t_source t), t_input t, t_output t, fst (t_target t))])" by (simp add: ‹path A (initial A) (map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p)› path_append_transition) then have *: "path A (initial A) (left_path (p@[t]))" by auto have "(snd (t_source t), t_input t, t_output t, snd (t_target t)) ∈ transitions B" using ‹t ∈ transitions (product A B)› unfolding product_transitions_alt_def by auto moreover have "target (initial B) (right_path p) = snd (t_source t)" using ‹t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))› by auto ultimately have "path B (initial B) ((right_path p)@[(snd (t_source t), t_input t, t_output t, snd (t_target t))])" by (simp add: ‹path B (initial B) (map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p)› path_append_transition) then have **: "path B (initial B) (right_path (p@[t]))" by auto show ?case using * ** *** **** by blast qed then show "path A (initial A) (left_path p)" and "path B (initial B) (right_path p)" and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)" and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)" by linarith+ qed lemma zip_path_left_right[simp] : "(zip_path (left_path p) (right_path p)) = p" by (induction p; auto) lemma product_reachable_state_paths : assumes "(q1,q2) ∈ reachable_states (product A B)" obtains p1 p2 where "path A (initial A) p1" and "path B (initial B) p2" and "target (initial A) p1 = q1" and "target (initial B) p2 = q2" and "p_io p1 = p_io p2" and "path (product A B) (initial (product A B)) (zip_path p1 p2)" and "target (initial (product A B)) (zip_path p1 p2) = (q1,q2)" proof - let ?P = "product A B" from assms obtain p where "path ?P (initial ?P) p" and "target (initial ?P) p = (q1,q2)" unfolding reachable_states_def by auto have "path A (initial A) (left_path p)" and "path B (initial B) (right_path p)" and "target (initial A) (left_path p) = q1" and "target (initial B) (right_path p) = q2" using paths_from_product_path[OF ‹path ?P (initial ?P) p›] ‹target (initial ?P) p = (q1,q2)› by auto moreover have "p_io (left_path p) = p_io (right_path p)" by auto moreover have "path (product A B) (initial (product A B)) (zip_path (left_path p) (right_path p))" using ‹path ?P (initial ?P) p› by auto moreover have "target (initial (product A B)) (zip_path (left_path p) (right_path p)) = (q1,q2)" using ‹target (initial ?P) p = (q1,q2)› by auto ultimately show ?thesis using that by blast qed lemma product_reachable_states[iff] : "(q1,q2) ∈ reachable_states (product A B) ⟷ (∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)" proof show "(q1,q2) ∈ reachable_states (product A B) ⟹ (∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)" using product_reachable_state_paths[of q1 q2 A B] by blast show "(∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2) ⟹ (q1,q2) ∈ reachable_states (product A B)" proof - assume "(∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)" then obtain p1 p2 where "path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2" by blast then show ?thesis using product_path_from_paths[of A p1 B p2] unfolding reachable_states_def by (metis (mono_tags, lifting) mem_Collect_eq) qed qed lemma left_path_zip : "length p1 = length p2 ⟹ left_path (zip_path p1 p2) = p1" by (induction p1 p2 rule: list_induct2; simp) lemma right_path_zip : "length p1 = length p2 ⟹ p_io p1 = p_io p2 ⟹ right_path (zip_path p1 p2) = p2" by (induction p1 p2 rule: list_induct2; simp) lemma zip_path_append_left_right : "length p1 = length p2 ⟹ zip_path (p1@(left_path p)) (p2@(right_path p)) = (zip_path p1 p2)@p" proof (induction p1 p2 rule: list_induct2) case Nil then show ?case by (induction p; simp) next case (Cons x xs y ys) then show ?case by simp qed lemma product_path: "path (product A B) (q1,q2) p ⟷ (path A q1 (left_path p) ∧ path B q2 (right_path p))" proof (induction p arbitrary: q1 q2) case Nil then show ?case by auto next case (Cons t p) have "path (Product_FSM.product A B) (q1, q2) (t # p) ⟹ (path A q1 (left_path (t # p)) ∧ path B q2 (right_path (t # p)))" proof - assume "path (Product_FSM.product A B) (q1, q2) (t # p)" then obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))" using prod.collapse by (metis path_cons_elim) then have "((q1,q2),x,y,(qA',qB')) ∈ transitions (product A B)" using ‹path (Product_FSM.product A B) (q1, q2) (t # p)› by auto then have "(q1, x, y, qA') ∈ FSM.transitions A" and "(q2, x, y, qB') ∈ FSM.transitions B" unfolding product_transitions_def by blast+ moreover have "(path A qA' (left_path p) ∧ path B qB' (right_path p))" using Cons.IH[of qA' qB'] ‹path (Product_FSM.product A B) (q1, q2) (t # p)› unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by auto ultimately show ?thesis unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by (simp add: path_prepend_t) qed moreover have "path A q1 (left_path (t # p)) ⟹ path B q2 (right_path (t # p)) ⟹ path (Product_FSM.product A B) (q1, q2) (t # p)" proof - assume "path A q1 (left_path (t # p))" and "path B q2 (right_path (t # p))" then obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))" using prod.collapse by (metis (no_types, lifting) fst_conv list.simps(9) path_cons_elim) then have "(q1, x, y, qA') ∈ FSM.transitions A" and "(q2, x, y, qB') ∈ FSM.transitions B" using ‹path A q1 (left_path (t # p))› ‹path B q2 (right_path (t # p))› by auto then have "((q1,q2),x,y,(qA',qB')) ∈ transitions (product A B)" unfolding product_transitions_def by blast moreover have "path (Product_FSM.product A B) (qA', qB') p" using Cons.IH[of qA' qB'] ‹path A q1 (left_path (t # p))› ‹path B q2 (right_path (t # p))› unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by auto ultimately show "path (Product_FSM.product A B) (q1, q2) (t # p)" unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by (simp add: path_prepend_t) qed ultimately show ?case by force qed lemma product_path_rev: assumes "p_io p1 = p_io p2" shows "path (product A B) (q1,q2) (zip_path p1 p2) ⟷ (path A q1 p1 ∧ path B q2 p2)" proof - have "length p1 = length p2" using assms using map_eq_imp_length_eq by blast then have "(map (λ t . (fst (t_source t), t_input t, t_output t, fst (t_target t))) (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))) = p1" by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto) moreover have "(map (λ t . (snd (t_source t), t_input t, t_output t, snd (t_target t))) (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))) = p2" using ‹length p1 = length p2› assms by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto) ultimately show ?thesis using product_path[of A B q1 q2 "(map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))"] by auto qed lemma product_language_state : shows "LS (product A B) (q1,q2) = LS A q1 ∩ LS B q2" proof show "LS (product A B) (q1, q2) ⊆ LS A q1 ∩ LS B q2" proof fix io assume "io ∈ LS (product A B) (q1, q2)" then obtain p where "io = p_io p" and "path (product A B) (q1,q2) p" by auto then obtain p1 p2 where "path A q1 p1" and "path B q2 p2" and "io = p_io p1" and "io = p_io p2" using product_path[of A B q1 q2 p] by fastforce then show "io ∈ LS A q1 ∩ LS B q2" unfolding LS.simps by blast qed show "LS A q1 ∩ LS B q2 ⊆ LS (product A B) (q1, q2)" proof fix io assume "io ∈ LS A q1 ∩ LS B q2" then obtain p1 p2 where "path A q1 p1" and "path B q2 p2" and "io = p_io p1" and "io = p_io p2" and "p_io p1 = p_io p2" by auto let ?p = "zip_path p1 p2" have "length p1 = length p2" using ‹p_io p1 = p_io p2› map_eq_imp_length_eq by blast moreover have "p_io ?p = p_io (map fst (zip p1 p2))" by auto ultimately have "p_io ?p = p_io p1" by auto then have "p_io ?p = io" using ‹io = p_io p1› by auto moreover have "path (product A B) (q1, q2) ?p" using product_path_rev[OF ‹p_io p1 = p_io p2›, of A B q1 q2] ‹path A q1 p1› ‹path B q2 p2› by auto ultimately show "io ∈ LS (product A B) (q1, q2)" unfolding LS.simps by blast qed qed lemma product_language : "L (product A B) = L A ∩ L B" unfolding product_simps product_language_state by blast lemma product_transition_split_ob : assumes "t ∈ transitions (product A B)" obtains t1 t2 where "t1 ∈ transitions A ∧ t_source t1 = fst (t_source t) ∧ t_input t1 = t_input t ∧ t_output t1 = t_output t ∧ t_target t1 = fst (t_target t)" and "t2 ∈ transitions B ∧ t_source t2 = snd (t_source t) ∧ t_input t2 = t_input t ∧ t_output t2 = t_output t ∧ t_target t2 = snd (t_target t)" using assms unfolding product_transitions_alt_def by auto lemma product_transition_split : assumes "t ∈ transitions (product A B)" shows "(fst (t_source t), t_input t, t_output t, fst (t_target t)) ∈ transitions A" and "(snd (t_source t), t_input t, t_output t, snd (t_target t)) ∈ transitions B" using product_transition_split_ob[OF assms] prod.collapse by fastforce+ lemma product_target_split: assumes "target (q1,q2) p = (q1',q2')" shows "target q1 (left_path p) = q1'" and "target q2 (right_path p) = q2'" using assms by (induction p arbitrary: q1 q2; force)+ lemma target_single_transition[simp] : "target q1 [(q1, x, y, q1')] = q1'" by auto lemma product_undefined_input : assumes "¬ (∃ t ∈ transitions (product (from_FSM M q1) (from_FSM M q2)). t_source t = qq ∧ t_input t = x)" and "q1 ∈ states M" and "q2 ∈ states M" shows "¬ (∃ t1 ∈ transitions M. ∃ t2 ∈ transitions M. t_source t1 = fst qq ∧ t_source t2 = snd qq ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)" proof assume "∃ t1 ∈ transitions M. ∃ t2 ∈ transitions M. t_source t1 = fst qq ∧ t_source t2 = snd qq ∧ t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2" then obtain t1 t2 where "t1 ∈ transitions M" and "t2 ∈ transitions M" and "t_source t1 = fst qq" and "t_source t2 = snd qq" and "t_input t1 = x" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2" by force have "((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" unfolding product_transitions_alt_def unfolding from_FSM_simps[OF assms(2)] unfolding from_FSM_simps[OF assms(3)] using ‹t1 ∈ transitions M› ‹t2 ∈ transitions M› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by blast then show False unfolding ‹t_source t1 = fst qq› ‹t_source t2 = snd qq› ‹t_input t1 = x› prod.collapse using assms(1) by auto qed subsection ‹Product Machines and Changing Initial States› lemma product_from_reachable_next : assumes "((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "(from_FSM (product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (product (from_FSM M q1') (from_FSM M q2'))" (is "?P1 = ?P2") proof - have "(q1,x,y,q1') ∈ transitions (from_FSM M q1)" and "(q2,x,y,q2') ∈ transitions (from_FSM M q2)" using assms(1) unfolding product_transitions_def by blast+ then have "q1' ∈ states (from_FSM M q1)" and "q2' ∈ states (from_FSM M q2)" using fsm_transition_target by auto have "q1' ∈ states (from_FSM M q1')" and "q1' ∈ states M" and "q1 ∈ states M" using ‹q1' ∈ FSM.states (FSM.from_FSM M q1)› assms(2) reachable_state_is_state by fastforce+ have "q2' ∈ states (from_FSM M q2')" and "q2' ∈ states M" and "q2 ∈ states M" using ‹q2' ∈ FSM.states (FSM.from_FSM M q2)› assms(3) reachable_state_is_state by fastforce+ have "initial ?P1 = initial ?P2" and "states ?P1 = states ?P2" and "inputs ?P1 = inputs ?P2" and "outputs ?P1 = outputs ?P2" and "transitions ?P1 = transitions ?P2" using from_FSM_simps[OF fsm_transition_target[OF assms(1)]] unfolding snd_conv unfolding product_simps unfolding product_transitions_def unfolding from_FSM_simps[OF ‹q1' ∈ states M›] from_FSM_simps[OF ‹q2' ∈ states M›] unfolding from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›] by auto then show ?thesis by (transfer; auto) qed lemma from_FSM_product_inputs : assumes "q1 ∈ states M" and "q2 ∈ states M" shows "(inputs (product (from_FSM M q1) (from_FSM M q2))) = (inputs M)" by (simp add: assms(1) assms(2)) lemma from_FSM_product_outputs : assumes "q1 ∈ states M" and "q2 ∈ states M" shows "(outputs (product (from_FSM M q1) (from_FSM M q2))) = (outputs M)" by (simp add: assms(1) assms(2)) lemma from_FSM_product_initial : assumes "q1 ∈ states M" and "q2 ∈ states M" shows "initial (product (from_FSM M q1) (from_FSM M q2)) = (q1,q2)" by (simp add: assms(1) assms(2)) lemma product_from_reachable_next' : assumes "t ∈ transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))" and "fst (t_source t) ∈ states M" and "snd (t_source t) ∈ states M" shows "(from_FSM (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t),snd (t_target t))) = (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t))))" proof - have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t" by simp then show ?thesis by (metis (no_types) assms(1) assms(2) assms(3) product_from_reachable_next) qed lemma product_from_reachable_next'_path : assumes "t ∈ transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))" and "fst (t_source t) ∈ states M" and "snd (t_source t) ∈ states M" shows "path (from_FSM (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t),snd (t_target t))) (fst (t_target t),snd (t_target t)) p = path (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t),snd (t_target t)) p" (is "path ?P1 ?q p = path ?P2 ?q p") proof - have i1: "initial ?P1 = ?q" using assms(1) fsm_transition_target by fastforce have i2: "initial ?P2 = ?q" proof - have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t" by auto then show ?thesis by (metis (no_types) assms(1) assms(2) assms(3) i1 product_from_reachable_next) qed have h12: "transitions ?P1 = transitions ?P2" using product_from_reachable_next'[OF assms] by simp show ?thesis proof (induction p rule: rev_induct) case Nil then show ?case by (metis (full_types) i1 i2 fsm_initial path.nil) next case (snoc t p) show ?case by (metis h12 path_append_transition path_append_transition_elim(1) path_append_transition_elim(2) path_append_transition_elim(3) snoc.IH) qed qed lemma product_from_transition: assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "transitions (product (from_FSM M q1') (from_FSM M q2')) = transitions (product (from_FSM M q1) (from_FSM M q2))" proof - have "q1' ∈ states M" and "q2' ∈ states M" using assms(1) unfolding product_simps from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by auto show ?thesis unfolding product_transitions_def from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q1' ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›] from_FSM_simps[OF ‹q2' ∈ states M›] by blast qed lemma product_from_path: assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" and "path (product (from_FSM M q1') (from_FSM M q2')) (q1',q2') p" shows "path (product (from_FSM M q1) (from_FSM M q2)) (q1',q2') p" by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) from_FSM_path_initial from_FSM_simps(5) from_from mem_Sigma_iff product_path product_simps(2)) lemma product_from_path_previous : assumes "path (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (t_target t) p" (is "path ?Pt (t_target t) p") and "t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "path (product (from_FSM M q1) (from_FSM M q2)) (t_target t) p" (is "path ?P (t_target t) p") by (metis assms(1) assms(2) assms(3) assms(4) fsm_transition_target prod.collapse product_from_path) lemma : assumes "t ∈ transitions (product (from_FSM M q1') (from_FSM M q2'))" and "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" by (metis assms product_from_transition) lemma product_from_not_completely_specified : assumes "¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1',q2')" and "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "¬ completely_specified_state (product (from_FSM M q1') (from_FSM M q2')) (q1',q2')" proof - have "q1' ∈ states M" and "q2' ∈ states M" using assms(2) unfolding product_simps from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] by auto show ?thesis using from_FSM_product_inputs[OF assms(3) assms(4)] using from_FSM_product_inputs[OF ‹q1' ∈ states M› ‹q2' ∈ states M› ] proof - have "FSM.transitions (Product_FSM.product (FSM.from_FSM M q1') (FSM.from_FSM M q2')) = FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))" by (metis (no_types) ‹(q1', q2') ∈ FSM.states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))› assms(3) assms(4) product_from_transition) then show ?thesis using ‹FSM.inputs (Product_FSM.product (FSM.from_FSM M q1') (FSM.from_FSM M q2')) = FSM.inputs M› ‹FSM.inputs (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) = FSM.inputs M› ‹¬ completely_specified_state (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (q1', q2')› by fastforce qed qed lemma from_product_initial_paths_ex : assumes "q1 ∈ states M" and "q2 ∈ states M" shows "(∃p1 p2. path (from_FSM M q1) (initial (from_FSM M q1)) p1 ∧ path (from_FSM M q2) (initial (from_FSM M q2)) p2 ∧ target (initial (from_FSM M q1)) p1 = q1 ∧ target (initial (from_FSM M q2)) p2 = q2 ∧ p_io p1 = p_io p2)" proof - have "path (from_FSM M q1) (initial (from_FSM M q1)) []" by blast moreover have "path (from_FSM M q2) (initial (from_FSM M q2)) []" by blast moreover have " target (initial (from_FSM M q1)) [] = q1 ∧ target (initial (from_FSM M q2)) [] = q2 ∧ p_io [] = p_io []" unfolding from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)] by auto ultimately show ?thesis by blast qed lemma product_observable : assumes "observable M1" and "observable M2" shows "observable (product M1 M2)" (is "observable ?P") proof - have "⋀ t1 t2 . t1 ∈ transitions ?P ⟹ t2 ∈ transitions ?P ⟹ t_source t1 = t_source t2 ⟹ t_input t1 = t_input t2 ⟹ t_output t1 = t_output t2 ⟹ t_target t1 = t_target t2" proof - fix t1 t2 assume "t1 ∈ transitions ?P" and "t2 ∈ transitions ?P" and "t_source t1 = t_source t2" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2" let ?t1L = "(fst (t_source t1), t_input t1, t_output t1, fst (t_target t1))" let ?t1R = "(snd (t_source t1), t_input t1, t_output t1, snd (t_target t1))" let ?t2L = "(fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))" let ?t2R = "(snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))" have "t_target ?t1L = t_target ?t2L" using product_transition_split(1)[OF ‹t1 ∈ transitions ?P›] product_transition_split(1)[OF ‹t2 ∈ transitions ?P›] ‹observable M1› ‹t_source t1 = t_source t2› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by auto moreover have "t_target ?t1R = t_target ?t2R" using product_transition_split(2)[OF ‹t1 ∈ transitions ?P›] product_transition_split(2)[OF ‹t2 ∈ transitions ?P›] ‹observable M2› ‹t_source t1 = t_source t2› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by auto ultimately show "t_target t1 = t_target t2" by (metis prod.exhaust_sel snd_conv) qed then show ?thesis unfolding observable.simps by blast qed lemma product_observable_self_transitions : assumes "q ∈ reachable_states (product M M)" and "observable M" shows "fst q = snd q" proof - let ?P = "product M M" have "⋀ p . path ?P (initial ?P) p ⟹ fst (target (initial ?P) p) = snd (target (initial ?P) p)" proof - fix p assume "path ?P (initial ?P) p" then show "fst (target (initial ?P) p) = snd (target (initial ?P) p)" proof (induction p rule: rev_induct) case Nil then show ?case by simp next case (snoc t p) have "path ?P (initial ?P) p" and "path ?P (target (initial ?P) p) [t]" using path_append_elim[of ?P "initial ?P" p "[t]", OF ‹path (product M M) (initial (product M M)) (p @ [t])›] by blast+ then have "t ∈ transitions ?P" by blast have "t_source t = target (initial ?P) p" using snoc.prems by fastforce let ?t1 = "(fst (t_source t), t_input t, t_output t, fst (t_target t))" let ?t2 = "(snd (t_source t), t_input t, t_output t, snd (t_target t))" have "?t1 ∈ transitions M" and "?t2 ∈ transitions M" using product_transition_split[OF ‹t ∈ transitions ?P›] by auto moreover have "t_source ?t1 = t_source ?t2" using ‹t_source t = target (initial ?P) p› snoc.IH[OF ‹path ?P (initial ?P) p›] by (metis fst_conv) moreover have "t_input ?t1 = t_input ?t2" by auto moreover have "t_output ?t1 = t_output ?t2" by auto ultimately have "t_target ?t1 = t_target ?t2" using ‹observable M› unfolding observable.simps by blast then have "fst (t_target t) = snd (t_target t)" by auto then show ?case unfolding target.simps visited_states.simps proof - show "fst (last (initial (product M M) # map t_target (p @ [t]))) = snd (last (initial (product M M) # map t_target (p @ [t])))" using ‹fst (t_target t) = snd (t_target t)› last_map last_snoc length_append_singleton length_map by force qed qed qed then show ?thesis using assms(1) unfolding reachable_states_def by blast qed lemma zip_path_eq_left : assumes "length xs1 = length xs2" and "length xs2 = length ys1" and "length ys1 = length ys2" and "zip_path xs1 xs2 = zip_path ys1 ys2" shows "xs1 = ys1" using assms by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto) lemma zip_path_eq_right : assumes "length xs1 = length xs2" and "length xs2 = length ys1" and "length ys1 = length ys2" and "p_io xs2 = p_io ys2" and "zip_path xs1 xs2 = zip_path ys1 ys2" shows "xs2 = ys2" using assms by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto) lemma zip_path_merge : "(zip_path (left_path p) (right_path p)) = p" by (induction p; auto) lemma product_from_reachable_path' : assumes "path (product (from_FSM M q1) (from_FSM M q2)) (q1', q2') p" and "q1 ∈ reachable_states M" and "q2 ∈ reachable_states M" shows "path (product (from_FSM M q1') (from_FSM M q2')) (q1', q2') p" by (meson assms(1) assms(2) assms(3) from_FSM_path from_FSM_path_rev_initial product_path reachable_state_is_state) lemma product_from : assumes "q1 ∈ states M" and "q2 ∈ states M" shows "product (from_FSM M q1) (from_FSM M q2) = from_FSM (product M M) (q1,q2)" (is "?PF = ?FP") proof - have "(q1,q2) ∈ states (product M M)" using assms unfolding product_simps by auto have "initial ?FP = initial ?PF" and "inputs ?FP = inputs ?PF" and "outputs ?FP = outputs ?PF" and "states ?FP = states ?PF" and "transitions ?FP = transitions ?PF" unfolding product_simps from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)] from_FSM_simps[OF ‹(q1,q2) ∈ states (product M M)›] product_transitions_def by auto then show ?thesis by (transfer; auto) qed lemma product_from_from : assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))" and "q1 ∈ states M" and "q2 ∈ states M" shows "(product (from_FSM M q1') (from_FSM M q2')) = (from_FSM (product (from_FSM M q1) (from_FSM M q2)) (q1',q2'))" using product_from by (metis (no_types, lifting) assms(1) assms(2) assms(3) from_FSM_simps(5) from_from mem_Sigma_iff product_simps(2)) lemma submachine_transition_product_from : assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))" and "((q1,q2),x,y,(q1',q2')) ∈ transitions S" and "q1 ∈ states M" and "q2 ∈ states M" shows "is_submachine (from_FSM S (q1',q2')) (product (from_FSM M q1') (from_FSM M q2'))" proof - have "((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))" using assms(1) assms(2) by auto have "(q1',q2') ∈ states S" using fsm_transition_target assms(2) by auto show ?thesis using product_from_reachable_next[OF ‹((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))› assms(3,4)] submachine_from[OF assms(1) ‹(q1',q2') ∈ states S›] by simp qed lemma submachine_transition_complete_product_from : assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))" and "completely_specified S" and "((q1,q2),x,y,(q1',q2')) ∈ transitions S" and "q1 ∈ states M" and "q2 ∈ states M" shows "completely_specified (from_FSM S (q1',q2'))" proof - let ?P = "(product (from_FSM M q1) (from_FSM M q2))" let ?P' = "(product (from_FSM M q1') (from_FSM M q2'))" let ?F = "(from_FSM S (q1',q2'))" have "initial ?P = (q1,q2)" by (simp add: assms(4) assms(5) reachable_state_is_state) then have "initial S = (q1,q2)" using assms(1) by (metis is_submachine.simps) then have "(q1',q2') ∈ states S" using assms(3) using fsm_transition_target by fastforce then have "states ?F = states S" using from_FSM_simps(5) by simp moreover have "inputs ?F = inputs S" using from_FSM_simps(2) ‹(q1',q2') ∈ states S› by simp ultimately show "completely_specified ?F" using assms(2) unfolding completely_specified.simps by (meson assms(2) completely_specified.elims(2) from_FSM_completely_specified) qed subsection ‹Calculating Acyclic Intersection Languages› lemma acyclic_product : assumes "acyclic B" shows "acyclic (product A B)" proof - show "acyclic (product A B)" proof (rule ccontr) assume "¬ FSM.acyclic (Product_FSM.product A B)" then obtain p where "path (product A B) (initial (product A B)) p" and "¬ distinct (visited_states (initial (product A B)) p)" by auto have "path B (initial B) (right_path p)" using product_path[of A B] ‹path (product A B) (initial (product A B)) p› unfolding product_simps by auto moreover have "¬ distinct (visited_states (initial B) (right_path p))" proof - obtain i j where "i < j" and "j < length ((initial A, initial B) # map t_target p)" and "((initial A, initial B) # map t_target p) ! i = ((initial A, initial B) # map t_target p) ! j" using ‹¬ distinct (visited_states (initial (product A B)) p)› unfolding visited_states.simps product_simps using non_distinct_repetition_indices by blast then have "snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)" by simp have * :"i < length ((initial B) # map t_target (right_path p))" and **:"j < length ((initial B) # map t_target (right_path p))" using ‹i < j› ‹j < length ((initial A, initial B) # map t_target p)› by auto have right_nth: "⋀ i . i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)" proof - have "((initial B) # map t_target (right_path p)) ! 0 = snd (((initial A, initial B) # map t_target p) ! 0)" by simp moreover have "⋀ i . Suc i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! Suc i = snd (((initial A, initial B) # map t_target p) ! Suc i)" by auto ultimately show "⋀ i . i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)" using less_Suc_eq_0_disj by auto qed have "((initial B) # map t_target (right_path p)) ! i = ((initial B) # map t_target (right_path p)) ! j" using ‹snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)› unfolding right_nth[OF *] right_nth[OF **] by assumption then show ?thesis unfolding visited_states.simps product_simps using non_distinct_repetition_indices_rev[OF ‹i < j› **] by blast qed ultimately show "False" using ‹acyclic B› unfolding acyclic.simps by blast qed qed lemma acyclic_product_path_length : assumes "acyclic B" and "path (product A B) (initial (product A B)) p" shows "length p < size B" proof - have *:"path B (initial B) (right_path p)" using product_path[of A B] ‹path (product A B) (initial (product A B)) p› unfolding product_simps by auto then have **: "distinct (visited_states (initial B) (right_path p))" using assms unfolding acyclic.simps by blast have "length (right_path p) < size B" using acyclic_path_length_limit[OF * **] by assumption then show "length p < size B" by auto qed lemma acyclic_language_alt_def : assumes "acyclic A" shows "image p_io (acyclic_paths_up_to_length A (initial A) (size A - 1)) = L A" proof - let ?ps = "acyclic_paths_up_to_length A (initial A) (size A - 1)" have "⋀ p . path A (initial A) p ⟹ length p ≤ FSM.size A - 1" using acyclic_path_length_limit assms unfolding acyclic.simps by fastforce then have "?ps = {p. path A (initial A) p}" using assms unfolding acyclic_paths_up_to_length.simps acyclic.simps by blast then show ?thesis unfolding LS.simps by blast qed definition acyclic_language_intersection :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set" where "acyclic_language_intersection M A = (let P = product M A in image p_io (acyclic_paths_up_to_length P (initial P) (size A - 1)))" lemma acyclic_language_intersection_completeness : assumes "acyclic A" shows "acyclic_language_intersection M A = L M ∩ L A" proof - let ?P = "product M A" let ?ps = "acyclic_paths_up_to_length ?P (initial ?P) (size A - 1)" have "L ?P = L M ∩ L A" using product_language by blast have "⋀ p . path ?P (initial ?P) p ⟹ length p ≤ FSM.size A - 1" using acyclic_product_path_length[OF assms] by fastforce then have "?ps = {p. path ?P (initial ?P) p}" using acyclic_product[OF assms] unfolding acyclic_paths_up_to_length.simps acyclic.simps by blast then have "image p_io ?ps = L ?P" unfolding LS.simps by blast then show ?thesis using product_language unfolding acyclic_language_intersection_def Let_def by blast qed end