[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) &&& target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. path A (FSM.initial A) (left_path p)
 2. path B (FSM.initial B) (right_path p)
 3. target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
 4. target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
proof (induction p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) [] \<Longrightarrow> path A (FSM.initial A) (left_path []) \<and> path B (FSM.initial B) (right_path []) \<and> target (FSM.initial A) (left_path []) = fst (target (FSM.initial (Product_FSM.product A B)) []) \<and> target (FSM.initial B) (right_path []) = snd (target (FSM.initial (Product_FSM.product A B)) [])
 2. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) []

goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) [] \<Longrightarrow> path A (FSM.initial A) (left_path []) \<and> path B (FSM.initial B) (right_path []) \<and> target (FSM.initial A) (left_path []) = fst (target (FSM.initial (Product_FSM.product A B)) []) \<and> target (FSM.initial B) (right_path []) = snd (target (FSM.initial (Product_FSM.product A B)) [])
 2. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) []

goal (1 subgoal):
 1. path A (FSM.initial A) (left_path []) \<and> path B (FSM.initial B) (right_path []) \<and> target (FSM.initial A) (left_path []) = fst (target (FSM.initial (Product_FSM.product A B)) []) \<and> target (FSM.initial B) (right_path []) = snd (target (FSM.initial (Product_FSM.product A B)) [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path []) \<and> path B (FSM.initial B) (right_path []) \<and> target (FSM.initial A) (left_path []) = fst (target (FSM.initial (Product_FSM.product A B)) []) \<and> target (FSM.initial B) (right_path []) = snd (target (FSM.initial (Product_FSM.product A B)) [])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
case (snoc t p)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p \<Longrightarrow> path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (p @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p \<Longrightarrow> path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (p @ [t])
[PROOF STEP]
have "path (product A B) (initial (product A B)) p"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p \<Longrightarrow> path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (p @ [t])

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p
[PROOF STEP]
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)"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) &&& target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p \<Longrightarrow> path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) &&& target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
have "t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. t_source t = (target (FSM.initial A) (left_path p), target (FSM.initial B) (right_path p))
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (p @ [t])

goal (1 subgoal):
 1. t_source t = (target (FSM.initial A) (left_path p), target (FSM.initial B) (right_path p))
[PROOF STEP]
by (metis (no_types, lifting) path_cons_elim path_suffix prod.collapse)
[PROOF STATE]
proof (state)
this:
t_source t = (target (FSM.initial A) (left_path p), target (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have ***: "target (initial A) (left_path (p@[t]))= fst (target (initial (product A B)) (p@[t]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have ****: "target (initial B) (right_path (p@[t]))= snd (target (initial (product A B)) (p@[t]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have "t \<in> transitions (product A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (p @ [t])

goal (1 subgoal):
 1. t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
have "(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> transitions A"
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A
[PROOF STEP]
unfolding product_transitions_alt_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have "target (initial A) (left_path p) = fst (t_source t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial A) (left_path p) = fst (t_source t)
[PROOF STEP]
using \<open>t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))\<close>
[PROOF STATE]
proof (prove)
using this:
t_source t = (target (FSM.initial A) (left_path p), target (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. target (FSM.initial A) (left_path p) = fst (t_source t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial A) (left_path p) = fst (t_source t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A
target (FSM.initial A) (left_path p) = fst (t_source t)
[PROOF STEP]
have "path A (initial A) ((left_path p)@[(fst (t_source t), t_input t, t_output t, fst (t_target t))])"
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A
target (FSM.initial A) (left_path p) = fst (t_source t)

goal (1 subgoal):
 1. path A (FSM.initial A) (left_path p @ [(fst (t_source t), t_input t, t_output t, fst (t_target t))])
[PROOF STEP]
by (simp add: \<open>path A (initial A) (map (\<lambda>t. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p)\<close> path_append_transition)
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p @ [(fst (t_source t), t_input t, t_output t, fst (t_target t))])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) (left_path p @ [(fst (t_source t), t_input t, t_output t, fst (t_target t))])
[PROOF STEP]
have *: "path A (initial A) (left_path (p@[t]))"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p @ [(fst (t_source t), t_input t, t_output t, fst (t_target t))])

goal (1 subgoal):
 1. path A (FSM.initial A) (left_path (p @ [t]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path (p @ [t]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have "(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> transitions B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
[PROOF STEP]
using \<open>t \<in> transitions (product A B)\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
[PROOF STEP]
unfolding product_transitions_alt_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
have "target (initial B) (right_path p) = snd (t_source t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial B) (right_path p) = snd (t_source t)
[PROOF STEP]
using \<open>t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))\<close>
[PROOF STATE]
proof (prove)
using this:
t_source t = (target (FSM.initial A) (left_path p), target (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. target (FSM.initial B) (right_path p) = snd (t_source t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial B) (right_path p) = snd (t_source t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
target (FSM.initial B) (right_path p) = snd (t_source t)
[PROOF STEP]
have "path B (initial B) ((right_path p)@[(snd (t_source t), t_input t, t_output t, snd (t_target t))])"
[PROOF STATE]
proof (prove)
using this:
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
target (FSM.initial B) (right_path p) = snd (t_source t)

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p @ [(snd (t_source t), t_input t, t_output t, snd (t_target t))])
[PROOF STEP]
by (simp add: \<open>path B (initial B) (map (\<lambda>t. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p)\<close> path_append_transition)
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) (right_path p @ [(snd (t_source t), t_input t, t_output t, snd (t_target t))])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path B (FSM.initial B) (right_path p @ [(snd (t_source t), t_input t, t_output t, snd (t_target t))])
[PROOF STEP]
have **: "path B (initial B) (right_path (p@[t]))"
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p @ [(snd (t_source t), t_input t, t_output t, snd (t_target t))])

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path (p @ [t]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) (right_path (p @ [t]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) xs \<Longrightarrow> path A (FSM.initial A) (left_path xs) \<and> path B (FSM.initial B) (right_path xs) \<and> target (FSM.initial A) (left_path xs) = fst (target (FSM.initial (Product_FSM.product A B)) xs) \<and> target (FSM.initial B) (right_path xs) = snd (target (FSM.initial (Product_FSM.product A B)) xs); path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (xs @ [x])\<rbrakk> \<Longrightarrow> path A (FSM.initial A) (left_path (xs @ [x])) \<and> path B (FSM.initial B) (right_path (xs @ [x])) \<and> target (FSM.initial A) (left_path (xs @ [x])) = fst (target (FSM.initial (Product_FSM.product A B)) (xs @ [x])) \<and> target (FSM.initial B) (right_path (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product A B)) (xs @ [x]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (FSM.initial A) (left_path (p @ [t])) \<and> path B (FSM.initial B) (right_path (p @ [t])) \<and> target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t])) \<and> target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))
[PROOF STEP]
using * ** *** ****
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path (p @ [t]))
path B (FSM.initial B) (right_path (p @ [t]))
target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))
target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))

goal (1 subgoal):
 1. path A (FSM.initial A) (left_path (p @ [t])) \<and> path B (FSM.initial B) (right_path (p @ [t])) \<and> target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t])) \<and> target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path (p @ [t])) \<and> path B (FSM.initial B) (right_path (p @ [t])) \<and> target (FSM.initial A) (left_path (p @ [t])) = fst (target (FSM.initial (Product_FSM.product A B)) (p @ [t])) \<and> target (FSM.initial B) (right_path (p @ [t])) = snd (target (FSM.initial (Product_FSM.product A B)) (p @ [t]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal (4 subgoals):
 1. path A (FSM.initial A) (left_path p)
 2. path B (FSM.initial B) (right_path p)
 3. target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
 4. target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
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)"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p) \<and> path B (FSM.initial B) (right_path p) \<and> target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) \<and> target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p) &&& target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zip_path_left_right[simp] :
  "(zip_path (left_path p) (right_path p)) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip_path (left_path p) (right_path p) = p
[PROOF STEP]
by (induction p; auto)


[STATEMENT]
lemma product_reachable_state_paths :
  assumes "(q1,q2) \<in> 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 STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?P = "product A B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
obtain p where "path ?P (initial ?P) p" and "target (initial ?P) p = (q1,q2)"
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> reachable_states (Product_FSM.product A B)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p; target (FSM.initial (Product_FSM.product A B)) p = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding reachable_states_def
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> {target (FSM.initial (Product_FSM.product A B)) p |p. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p; target (FSM.initial (Product_FSM.product A B)) p = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p
target (FSM.initial (Product_FSM.product A B)) p = (q1, q2)

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = q1 &&& target (FSM.initial B) (right_path p) = q2
[PROOF STEP]
using paths_from_product_path[OF \<open>path ?P (initial ?P) p\<close>] \<open>target (initial ?P) p = (q1,q2)\<close>
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = fst (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial B) (right_path p) = snd (target (FSM.initial (Product_FSM.product A B)) p)
target (FSM.initial (Product_FSM.product A B)) p = (q1, q2)

goal (1 subgoal):
 1. (path A (FSM.initial A) (left_path p) &&& path B (FSM.initial B) (right_path p)) &&& target (FSM.initial A) (left_path p) = q1 &&& target (FSM.initial B) (right_path p) = q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = q1
target (FSM.initial B) (right_path p) = q2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = q1
target (FSM.initial B) (right_path p) = q2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p_io (left_path p) = p_io (right_path p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (left_path p) = p_io (right_path p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (left_path p) = p_io (right_path p)

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io (left_path p) = p_io (right_path p)

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "path (product A B) (initial (product A B)) (zip_path (left_path p) (right_path p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))
[PROOF STEP]
using \<open>path ?P (initial ?P) p\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "target (initial (product A B)) (zip_path (left_path p) (right_path p)) = (q1,q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)
[PROOF STEP]
using \<open>target (initial ?P) p = (q1,q2)\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial (Product_FSM.product A B)) p = (q1, q2)

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = q1
target (FSM.initial B) (right_path p) = q2
p_io (left_path p) = p_io (right_path p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))
target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = q1
target (FSM.initial B) (right_path p) = q2
p_io (left_path p) = p_io (right_path p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))
target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (left_path p)
path B (FSM.initial B) (right_path p)
target (FSM.initial A) (left_path p) = q1
target (FSM.initial B) (right_path p) = q2
p_io (left_path p) = p_io (right_path p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p))
target (FSM.initial (Product_FSM.product A B)) (zip_path (left_path p) (right_path p)) = (q1, q2)
\<lbrakk>path A (FSM.initial A) ?p1.0; path B (FSM.initial B) ?p2.0; target (FSM.initial A) ?p1.0 = q1; target (FSM.initial B) ?p2.0 = q2; p_io ?p1.0 = p_io ?p2.0; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path ?p1.0 ?p2.0); target (FSM.initial (Product_FSM.product A B)) (zip_path ?p1.0 ?p2.0) = (q1, q2)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_reachable_states[iff] :
  "(q1,q2) \<in> reachable_states (product A B) \<longleftrightarrow> (\<exists> p1 p2 . 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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((q1, q2) \<in> reachable_states (Product_FSM.product A B)) = (\<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (q1, q2) \<in> reachable_states (Product_FSM.product A B) \<Longrightarrow> \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
 2. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
show "(q1,q2) \<in> reachable_states (product A B) \<Longrightarrow> (\<exists> p1 p2 . 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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q1, q2) \<in> reachable_states (Product_FSM.product A B) \<Longrightarrow> \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
using product_reachable_state_paths[of q1 q2 A B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(q1, q2) \<in> reachable_states (Product_FSM.product A B); \<And>p1 p2. \<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; target (FSM.initial A) p1 = q1; target (FSM.initial B) p2 = q2; p_io p1 = p_io p2; path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2); target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (q1, q2)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (q1, q2) \<in> reachable_states (Product_FSM.product A B) \<Longrightarrow> \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> reachable_states (Product_FSM.product A B) \<Longrightarrow> \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2

goal (1 subgoal):
 1. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
show "(\<exists> p1 p2 . 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) \<Longrightarrow> (q1,q2) \<in> reachable_states (product A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
assume "(\<exists> p1 p2 . 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)"
[PROOF STATE]
proof (state)
this:
\<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2

goal (1 subgoal):
 1. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
obtain 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"
[PROOF STATE]
proof (prove)
using this:
\<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2

goal (1 subgoal):
 1. (\<And>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2

goal (1 subgoal):
 1. \<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2

goal (1 subgoal):
 1. (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
using product_path_from_paths[of A p1 B p2]
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
\<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
\<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal (1 subgoal):
 1. (q1, q2) \<in> reachable_states (Product_FSM.product A B)
[PROOF STEP]
unfolding reachable_states_def
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2
\<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
\<lbrakk>path A (FSM.initial A) p1; path B (FSM.initial B) p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal (1 subgoal):
 1. (q1, q2) \<in> {target (FSM.initial (Product_FSM.product A B)) p |p. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p}
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> reachable_states (Product_FSM.product A B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p1 p2. path A (FSM.initial A) p1 \<and> path B (FSM.initial B) p2 \<and> target (FSM.initial A) p1 = q1 \<and> target (FSM.initial B) p2 = q2 \<and> p_io p1 = p_io p2 \<Longrightarrow> (q1, q2) \<in> reachable_states (Product_FSM.product A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_path_zip : "length p1 = length p2 \<Longrightarrow> left_path (zip_path p1 p2) = p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p1 = length p2 \<Longrightarrow> left_path (zip_path p1 p2) = p1
[PROOF STEP]
by (induction p1 p2 rule: list_induct2; simp)


[STATEMENT]
lemma right_path_zip : "length p1 = length p2 \<Longrightarrow> p_io p1 = p_io p2 \<Longrightarrow> right_path (zip_path p1 p2) = p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length p1 = length p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> right_path (zip_path p1 p2) = p2
[PROOF STEP]
by (induction p1 p2 rule: list_induct2; simp)


[STATEMENT]
lemma zip_path_append_left_right : "length p1 = length p2 \<Longrightarrow> zip_path (p1@(left_path p)) (p2@(right_path p)) = (zip_path p1 p2)@p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p1 = length p2 \<Longrightarrow> zip_path (p1 @ left_path p) (p2 @ right_path p) = zip_path p1 p2 @ p
[PROOF STEP]
proof (induction p1 p2 rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zip_path ([] @ left_path p) ([] @ right_path p) = zip_path [] [] @ p
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p\<rbrakk> \<Longrightarrow> zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. zip_path ([] @ left_path p) ([] @ right_path p) = zip_path [] [] @ p
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p\<rbrakk> \<Longrightarrow> zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip_path ([] @ left_path p) ([] @ right_path p) = zip_path [] [] @ p
[PROOF STEP]
by (induction p; simp)
[PROOF STATE]
proof (state)
this:
zip_path ([] @ left_path p) ([] @ right_path p) = zip_path [] [] @ p

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p\<rbrakk> \<Longrightarrow> zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p\<rbrakk> \<Longrightarrow> zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p\<rbrakk> \<Longrightarrow> zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
zip_path (xs @ left_path p) (ys @ right_path p) = zip_path xs ys @ p

goal (1 subgoal):
 1. zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zip_path ((x # xs) @ left_path p) ((y # ys) @ right_path p) = zip_path (x # xs) (y # ys) @ p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_path:
  "path (product A B) (q1,q2) p \<longleftrightarrow> (path A q1 (left_path p) \<and> path B q2 (right_path p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))
[PROOF STEP]
proof (induction p arbitrary: q1 q2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q1 q2. path (Product_FSM.product A B) (q1, q2) [] = (path A q1 (left_path []) \<and> path B q2 (right_path []))
 2. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>q1 q2. path (Product_FSM.product A B) (q1, q2) [] = (path A q1 (left_path []) \<and> path B q2 (right_path []))
 2. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) [] = (path A q1 (left_path []) \<and> path B q2 (right_path []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) [] = (path A q1 (left_path []) \<and> path B q2 (right_path []))

goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
case (Cons t p)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (?q1.0, ?q2.0) p = (path A ?q1.0 (left_path p) \<and> path B ?q2.0 (right_path p))

goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
have "path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> (path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
assume "path (Product_FSM.product A B) (q1, q2) (t # p)"
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. (\<And>x y qA' qB'. t = ((q1, q2), x, y, qA', qB') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (q1, q2) (t # p)
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>x y qA' qB'. t = ((q1, q2), x, y, qA', qB') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis path_cons_elim)
[PROOF STATE]
proof (state)
this:
t = ((q1, q2), x, y, qA', qB')

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = ((q1, q2), x, y, qA', qB')
[PROOF STEP]
have "((q1,q2),x,y,(qA',qB')) \<in> transitions (product A B)"
[PROOF STATE]
proof (prove)
using this:
t = ((q1, q2), x, y, qA', qB')

goal (1 subgoal):
 1. ((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
using \<open>path (Product_FSM.product A B) (q1, q2) (t # p)\<close>
[PROOF STATE]
proof (prove)
using this:
t = ((q1, q2), x, y, qA', qB')
path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. ((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
have "(q1, x, y, qA') \<in> FSM.transitions A" and "(q2, x, y, qB') \<in> FSM.transitions B"
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. (q1, x, y, qA') \<in> FSM.transitions A &&& (q2, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
unfolding product_transitions_def
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, qA', qB') \<in> {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions A \<and> (qB, x, y, qB') \<in> FSM.transitions B}

goal (1 subgoal):
 1. (q1, x, y, qA') \<in> FSM.transitions A &&& (q2, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
have "(path A qA' (left_path p) \<and> path B qB' (right_path p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A qA' (left_path p) \<and> path B qB' (right_path p)
[PROOF STEP]
using Cons.IH[of qA' qB'] \<open>path (Product_FSM.product A B) (q1, q2) (t # p)\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (qA', qB') p = (path A qA' (left_path p) \<and> path B qB' (right_path p))
path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. path A qA' (left_path p) \<and> path B qB' (right_path p)
[PROOF STEP]
unfolding \<open>t = ((q1,q2),x,y,(qA',qB'))\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (qA', qB') p = (path A qA' (left_path p) \<and> path B qB' (right_path p))
path (Product_FSM.product A B) (q1, q2) (((q1, q2), x, y, qA', qB') # p)

goal (1 subgoal):
 1. path A qA' (left_path p) \<and> path B qB' (right_path p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A qA' (left_path p) \<and> path B qB' (right_path p)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B
path A qA' (left_path p) \<and> path B qB' (right_path p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B
path A qA' (left_path p) \<and> path B qB' (right_path p)

goal (1 subgoal):
 1. path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
[PROOF STEP]
unfolding \<open>t = ((q1,q2),x,y,(qA',qB'))\<close>
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B
path A qA' (left_path p) \<and> path B qB' (right_path p)

goal (1 subgoal):
 1. path A q1 (left_path (((q1, q2), x, y, qA', qB') # p)) \<and> path B q2 (right_path (((q1, q2), x, y, qA', qB') # p))
[PROOF STEP]
by (simp add: path_prepend_t)
[PROOF STATE]
proof (state)
this:
path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))

goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))

goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
have "path A q1 (left_path (t # p)) \<Longrightarrow> path B q2 (right_path (t # p)) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
assume "path A q1 (left_path (t # p))" and "path B q2 (right_path (t # p))"
[PROOF STATE]
proof (state)
this:
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))
[PROOF STEP]
obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))"
[PROOF STATE]
proof (prove)
using this:
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))

goal (1 subgoal):
 1. (\<And>x y qA' qB'. t = ((q1, q2), x, y, qA', qB') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>x y qA' qB'. t = ((q1, q2), x, y, qA', qB') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) fst_conv list.simps(9) path_cons_elim)
[PROOF STATE]
proof (state)
this:
t = ((q1, q2), x, y, qA', qB')

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = ((q1, q2), x, y, qA', qB')
[PROOF STEP]
have "(q1, x, y, qA') \<in> FSM.transitions A" and "(q2, x, y, qB') \<in> FSM.transitions B"
[PROOF STATE]
proof (prove)
using this:
t = ((q1, q2), x, y, qA', qB')

goal (1 subgoal):
 1. (q1, x, y, qA') \<in> FSM.transitions A &&& (q2, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
using \<open>path A q1 (left_path (t # p))\<close> \<open>path B q2 (right_path (t # p))\<close>
[PROOF STATE]
proof (prove)
using this:
t = ((q1, q2), x, y, qA', qB')
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))

goal (1 subgoal):
 1. (q1, x, y, qA') \<in> FSM.transitions A &&& (q2, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
have "((q1,q2),x,y,(qA',qB')) \<in> transitions (product A B)"
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. ((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
unfolding product_transitions_def
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, qA') \<in> FSM.transitions A
(q2, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. ((q1, q2), x, y, qA', qB') \<in> {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions A \<and> (qB, x, y, qB') \<in> FSM.transitions B}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
have "path (Product_FSM.product A B) (qA', qB') p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (qA', qB') p
[PROOF STEP]
using Cons.IH[of qA' qB'] \<open>path A q1 (left_path (t # p))\<close> \<open>path B q2 (right_path (t # p))\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (qA', qB') p = (path A qA' (left_path p) \<and> path B qB' (right_path p))
path A q1 (left_path (t # p))
path B q2 (right_path (t # p))

goal (1 subgoal):
 1. path (Product_FSM.product A B) (qA', qB') p
[PROOF STEP]
unfolding \<open>t = ((q1,q2),x,y,(qA',qB'))\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (qA', qB') p = (path A qA' (left_path p) \<and> path B qB' (right_path p))
path A q1 (left_path (((q1, q2), x, y, qA', qB') # p))
path B q2 (right_path (((q1, q2), x, y, qA', qB') # p))

goal (1 subgoal):
 1. path (Product_FSM.product A B) (qA', qB') p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (qA', qB') p

goal (1 subgoal):
 1. \<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
path (Product_FSM.product A B) (qA', qB') p
[PROOF STEP]
show "path (Product_FSM.product A B) (q1, q2) (t # p)"
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
path (Product_FSM.product A B) (qA', qB') p

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
unfolding \<open>t = ((q1,q2),x,y,(qA',qB'))\<close>
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, qA', qB') \<in> FSM.transitions (Product_FSM.product A B)
path (Product_FSM.product A B) (qA', qB') p

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (((q1, q2), x, y, qA', qB') # p)
[PROOF STEP]
by (simp add: path_prepend_t)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (t # p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. \<And>a p q1 q2. (\<And>q1 q2. path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))) \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (a # p) = (path A q1 (left_path (a # p)) \<and> path B q2 (right_path (a # p)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
\<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (q1, q2) (t # p) \<Longrightarrow> path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p))
\<lbrakk>path A q1 (left_path (t # p)); path B q2 (right_path (t # p))\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (q1, q2) (t # p)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (t # p) = (path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (t # p) = (path A q1 (left_path (t # p)) \<and> path B q2 (right_path (t # p)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_path_rev:
  assumes "p_io p1 = p_io p2"
  shows "path (product A B) (q1,q2) (zip_path p1 p2) \<longleftrightarrow> (path A q1 p1 \<and> path B q2 p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
have "length p1 = length p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p_io p1 = p_io p2

goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
using map_eq_imp_length_eq
[PROOF STATE]
proof (prove)
using this:
p_io p1 = p_io p2
map ?f ?xs = map ?g ?ys \<Longrightarrow> length ?xs = length ?ys

goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length p1 = length p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length p1 = length p2
[PROOF STEP]
have "(map (\<lambda> t . (fst (t_source t), t_input t, t_output t, fst (t_target t))) (map (\<lambda> 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"
[PROOF STATE]
proof (prove)
using this:
length p1 = length p2

goal (1 subgoal):
 1. left_path (zip_path p1 p2) = p1
[PROOF STEP]
by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto)
[PROOF STATE]
proof (state)
this:
left_path (zip_path p1 p2) = p1

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
left_path (zip_path p1 p2) = p1

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
have "(map (\<lambda> t . (snd (t_source t), t_input t, t_output t, snd (t_target t))) (map (\<lambda> 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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_path (zip_path p1 p2) = p2
[PROOF STEP]
using \<open>length p1 = length p2\<close> assms
[PROOF STATE]
proof (prove)
using this:
length p1 = length p2
p_io p1 = p_io p2

goal (1 subgoal):
 1. right_path (zip_path p1 p2) = p2
[PROOF STEP]
by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto)
[PROOF STATE]
proof (state)
this:
right_path (zip_path p1 p2) = p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
left_path (zip_path p1 p2) = p1
right_path (zip_path p1 p2) = p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
left_path (zip_path p1 p2) = p1
right_path (zip_path p1 p2) = p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
using product_path[of A B q1 q2 "(map (\<lambda> 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))"]
[PROOF STATE]
proof (prove)
using this:
left_path (zip_path p1 p2) = p1
right_path (zip_path p1 p2) = p2
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 (left_path (zip_path p1 p2)) \<and> path B q2 (right_path (zip_path p1 p2)))

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_language_state :
  shows "LS (product A B) (q1,q2) = LS A q1 \<inter> LS B q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS (Product_FSM.product A B) (q1, q2) = LS A q1 \<inter> LS B q2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LS (Product_FSM.product A B) (q1, q2) \<subseteq> LS A q1 \<inter> LS B q2
 2. LS A q1 \<inter> LS B q2 \<subseteq> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
show "LS (product A B) (q1, q2) \<subseteq> LS A q1 \<inter> LS B q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS (Product_FSM.product A B) (q1, q2) \<subseteq> LS A q1 \<inter> LS B q2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LS (Product_FSM.product A B) (q1, q2) \<Longrightarrow> x \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LS (Product_FSM.product A B) (q1, q2) \<Longrightarrow> x \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
assume "io \<in> LS (product A B) (q1, q2)"
[PROOF STATE]
proof (state)
this:
io \<in> LS (Product_FSM.product A B) (q1, q2)

goal (1 subgoal):
 1. \<And>x. x \<in> LS (Product_FSM.product A B) (q1, q2) \<Longrightarrow> x \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
obtain p where "io = p_io p"
                    and "path (product A B) (q1,q2) p"
[PROOF STATE]
proof (prove)
using this:
io \<in> LS (Product_FSM.product A B) (q1, q2)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>io = p_io p; path (Product_FSM.product A B) (q1, q2) p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io = p_io p
path (Product_FSM.product A B) (q1, q2) p

goal (1 subgoal):
 1. \<And>x. x \<in> LS (Product_FSM.product A B) (q1, q2) \<Longrightarrow> x \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = p_io p
path (Product_FSM.product A B) (q1, q2) p
[PROOF STEP]
obtain p1 p2 where "path A q1 p1"
                        and "path B q2 p2"
                        and "io = p_io p1"
                        and "io = p_io p2"
[PROOF STATE]
proof (prove)
using this:
io = p_io p
path (Product_FSM.product A B) (q1, q2) p

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A q1 p1; path B q2 p2; io = p_io p1; io = p_io p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using product_path[of A B q1 q2 p]
[PROOF STATE]
proof (prove)
using this:
io = p_io p
path (Product_FSM.product A B) (q1, q2) p
path (Product_FSM.product A B) (q1, q2) p = (path A q1 (left_path p) \<and> path B q2 (right_path p))

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A q1 p1; path B q2 p2; io = p_io p1; io = p_io p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
path A q1 p1
path B q2 p2
io = p_io p1
io = p_io p2

goal (1 subgoal):
 1. \<And>x. x \<in> LS (Product_FSM.product A B) (q1, q2) \<Longrightarrow> x \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A q1 p1
path B q2 p2
io = p_io p1
io = p_io p2
[PROOF STEP]
show "io \<in> LS A q1 \<inter> LS B q2"
[PROOF STATE]
proof (prove)
using this:
path A q1 p1
path B q2 p2
io = p_io p1
io = p_io p2

goal (1 subgoal):
 1. io \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
unfolding LS.simps
[PROOF STATE]
proof (prove)
using this:
path A q1 p1
path B q2 p2
io = p_io p1
io = p_io p2

goal (1 subgoal):
 1. io \<in> {p_io p |p. path A q1 p} \<inter> {p_io p |p. path B q2 p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> LS A q1 \<inter> LS B q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LS (Product_FSM.product A B) (q1, q2) \<subseteq> LS A q1 \<inter> LS B q2

goal (1 subgoal):
 1. LS A q1 \<inter> LS B q2 \<subseteq> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
show "LS A q1 \<inter> LS B q2 \<subseteq> LS (product A B) (q1, q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS A q1 \<inter> LS B q2 \<subseteq> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
assume "io \<in> LS A q1 \<inter> LS B q2"
[PROOF STATE]
proof (state)
this:
io \<in> LS A q1 \<inter> LS B q2

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> LS A q1 \<inter> LS B q2
[PROOF STEP]
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"
[PROOF STATE]
proof (prove)
using this:
io \<in> LS A q1 \<inter> LS B q2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>path A q1 p1; path B q2 p2; io = p_io p1; io = p_io p2; p_io p1 = p_io p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A q1 p1
path B q2 p2
io = p_io p1
io = p_io p2
p_io p1 = p_io p2

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
let ?p = "zip_path p1 p2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
have "length p1 = length p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
using \<open>p_io p1 = p_io p2\<close> map_eq_imp_length_eq
[PROOF STATE]
proof (prove)
using this:
p_io p1 = p_io p2
map ?f ?xs = map ?g ?ys \<Longrightarrow> length ?xs = length ?ys

goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length p1 = length p2

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length p1 = length p2

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
have "p_io ?p = p_io (map fst (zip p1 p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (zip_path p1 p2) = p_io (map fst (zip p1 p2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (zip_path p1 p2) = p_io (map fst (zip p1 p2))

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length p1 = length p2
p_io (zip_path p1 p2) = p_io (map fst (zip p1 p2))
[PROOF STEP]
have "p_io ?p = p_io p1"
[PROOF STATE]
proof (prove)
using this:
length p1 = length p2
p_io (zip_path p1 p2) = p_io (map fst (zip p1 p2))

goal (1 subgoal):
 1. p_io (zip_path p1 p2) = p_io p1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (zip_path p1 p2) = p_io p1

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io (zip_path p1 p2) = p_io p1
[PROOF STEP]
have "p_io ?p = io"
[PROOF STATE]
proof (prove)
using this:
p_io (zip_path p1 p2) = p_io p1

goal (1 subgoal):
 1. p_io (zip_path p1 p2) = io
[PROOF STEP]
using \<open>io = p_io p1\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (zip_path p1 p2) = p_io p1
io = p_io p1

goal (1 subgoal):
 1. p_io (zip_path p1 p2) = io
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (zip_path p1 p2) = io

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io (zip_path p1 p2) = io

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
have "path (product A B) (q1, q2) ?p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)
[PROOF STEP]
using product_path_rev[OF \<open>p_io p1 = p_io p2\<close>, of A B q1 q2] \<open>path A q1 p1\<close> \<open>path B q2 p2\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2) = (path A q1 p1 \<and> path B q2 p2)
path A q1 p1
path B q2 p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)

goal (1 subgoal):
 1. \<And>x. x \<in> LS A q1 \<inter> LS B q2 \<Longrightarrow> x \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p_io (zip_path p1 p2) = io
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)
[PROOF STEP]
show "io \<in> LS (product A B) (q1, q2)"
[PROOF STATE]
proof (prove)
using this:
p_io (zip_path p1 p2) = io
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)

goal (1 subgoal):
 1. io \<in> LS (Product_FSM.product A B) (q1, q2)
[PROOF STEP]
unfolding LS.simps
[PROOF STATE]
proof (prove)
using this:
p_io (zip_path p1 p2) = io
path (Product_FSM.product A B) (q1, q2) (zip_path p1 p2)

goal (1 subgoal):
 1. io \<in> {p_io p |p. path (Product_FSM.product A B) (q1, q2) p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> LS (Product_FSM.product A B) (q1, q2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LS A q1 \<inter> LS B q2 \<subseteq> LS (Product_FSM.product A B) (q1, q2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_language : "L (product A B) = L A \<inter> L B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L (Product_FSM.product A B) = L A \<inter> L B
[PROOF STEP]
unfolding product_simps product_language_state
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L A \<inter> L B = L A \<inter> L B
[PROOF STEP]
by blast


[STATEMENT]
lemma product_transition_split_ob :
  assumes "t \<in> transitions (product A B)"
  obtains t1 t2
  where "t1 \<in> transitions A \<and> t_source t1 = fst (t_source t) \<and> t_input t1 = t_input t \<and> t_output t1 = t_output t \<and> t_target t1 = fst (t_target t)"
    and "t2 \<in> transitions B \<and> t_source t2 = snd (t_source t) \<and> t_input t2 = t_input t \<and> t_output t2 = t_output t \<and> t_target t2 = snd (t_target t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions A \<and> t_source t1 = fst (t_source t) \<and> t_input t1 = t_input t \<and> t_output t1 = t_output t \<and> t_target t1 = fst (t_target t); t2 \<in> FSM.transitions B \<and> t_source t2 = snd (t_source t) \<and> t_input t2 = t_input t \<and> t_output t2 = t_output t \<and> t_target t2 = snd (t_target t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. (\<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions A \<and> t_source t1 = fst (t_source t) \<and> t_input t1 = t_input t \<and> t_output t1 = t_output t \<and> t_target t1 = fst (t_target t); t2 \<in> FSM.transitions B \<and> t_source t2 = snd (t_source t) \<and> t_input t2 = t_input t \<and> t_output t2 = t_output t \<and> t_target t2 = snd (t_target t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding product_transitions_alt_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. (\<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions A \<and> t_source t1 = fst (t_source t) \<and> t_input t1 = t_input t \<and> t_output t1 = t_output t \<and> t_target t1 = fst (t_target t); t2 \<in> FSM.transitions B \<and> t_source t2 = snd (t_source t) \<and> t_input t2 = t_input t \<and> t_output t2 = t_output t \<and> t_target t2 = snd (t_target t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma product_transition_split :
  assumes "t \<in> transitions (product A B)"
  shows "(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> transitions A"
    and "(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> transitions B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A &&& (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
[PROOF STEP]
using product_transition_split_ob[OF assms] prod.collapse
[PROOF STATE]
proof (prove)
using this:
(\<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions A \<and> t_source t1 = fst (t_source t) \<and> t_input t1 = t_input t \<and> t_output t1 = t_output t \<and> t_target t1 = fst (t_target t); t2 \<in> FSM.transitions B \<and> t_source t2 = snd (t_source t) \<and> t_input t2 = t_input t \<and> t_output t2 = t_output t \<and> t_target t2 = snd (t_target t)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions A &&& (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions B
[PROOF STEP]
by fastforce+