Theory Product_FSM

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 product_from_transition_shared_state :
  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