[STATEMENT]
lemma intersection_is_distinguishing_correctness :
  assumes "observable M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "intersection_is_distinguishing M t1 q1 t2 q2 = (\<exists> io . isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io)"
  (is "?P1 = ?P2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2 = (\<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. intersection_is_distinguishing M t1 q1 t2 q2 \<Longrightarrow> \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
show "?P1 \<Longrightarrow> ?P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2 \<Longrightarrow> \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
proof (induction t1 arbitrary: t2 q1 q2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
case (PT m1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?xaa \<in> range m1; ?xaaa \<in> set_option ?xaa; intersection_is_distinguishing M ?xaaa ?q1.0 ?t2.0 ?q2.0\<rbrakk> \<Longrightarrow> \<exists>io. isin ?xaaa io \<and> isin ?t2.0 io \<and> distinguishes M ?q1.0 ?q2.0 io
intersection_is_distinguishing M (PT m1) q1 t2 q2

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
obtain m2 where "t2 = PT m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m2. t2 = PT m2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prefix_tree.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?y = PT x \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>m2. t2 = PT m2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t2 = PT m2

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t2 = PT m2
[PROOF STEP]
obtain x y where "(x,y) \<in> dom m1" and "(x,y) \<in> dom m2"
                            and *: "case h_obs M q1 x y of
                                    None \<Rightarrow> h_obs M q2 x y \<noteq> None |
                                    Some q1' \<Rightarrow> (case h_obs M q2 x y of
                                      None \<Rightarrow> True |
                                      Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x,y))) q1' (the (m2 (x,y))) q2')"
[PROOF STATE]
proof (prove)
using this:
t2 = PT m2

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>(x, y) \<in> dom m1; (x, y) \<in> dom m2; case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using PT.prems(1) intersection_is_distinguishing.simps
[PROOF STATE]
proof (prove)
using this:
t2 = PT m2
intersection_is_distinguishing M (PT m1) q1 t2 q2
intersection_is_distinguishing ?M (PT ?t1.0) ?q1.0 (PT ?t2.0) ?q2.0 = (\<exists>(x, y)\<in>dom ?t1.0 \<inter> dom ?t2.0. case FSM.h_obs ?M ?q1.0 x y of None \<Rightarrow> FSM.h_obs ?M ?q2.0 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs ?M ?q2.0 x y of None \<Rightarrow> True | Some xa \<Rightarrow> intersection_is_distinguishing ?M (the (?t1.0 (x, y))) q1' (the (?t2.0 (x, y))) xa)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>(x, y) \<in> dom m1; (x, y) \<in> dom m2; case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(x, y) \<in> dom m1
(x, y) \<in> dom m2
case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
obtain t1' where "m1 (x,y) = Some t1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t1'. m1 (x, y) = Some t1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(x,y) \<in> dom m1\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> dom m1

goal (1 subgoal):
 1. (\<And>t1'. m1 (x, y) = Some t1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m1 (x, y) = Some t1'

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m1 (x, y) = Some t1'
[PROOF STEP]
have "isin (PT m1) [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
m1 (x, y) = Some t1'

goal (1 subgoal):
 1. isin (PT m1) [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isin (PT m1) [(x, y)]

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
obtain t2' where "m2 (x,y) = Some t2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t2'. m2 (x, y) = Some t2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(x,y) \<in> dom m2\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> dom m2

goal (1 subgoal):
 1. (\<And>t2'. m2 (x, y) = Some t2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m2 (x, y) = Some t2'

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m2 (x, y) = Some t2'
[PROOF STEP]
have "isin t2 [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
m2 (x, y) = Some t2'

goal (1 subgoal):
 1. isin t2 [(x, y)]
[PROOF STEP]
unfolding \<open>t2 = PT m2\<close>
[PROOF STATE]
proof (prove)
using this:
m2 (x, y) = Some t2'

goal (1 subgoal):
 1. isin (PT m2) [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isin t2 [(x, y)]

goal (1 subgoal):
 1. \<And>xa t2 q1 q2. \<lbrakk>\<And>xaa xaaa t2 q1 q2. \<lbrakk>xaa \<in> range xa; xaaa \<in> set_option xaa; intersection_is_distinguishing M xaaa q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin xaaa io \<and> isin t2 io \<and> distinguishes M q1 q2 io; intersection_is_distinguishing M (PT xa) q1 t2 q2\<rbrakk> \<Longrightarrow> \<exists>io. isin (PT xa) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
proof (cases "h_obs M q1 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = None
[PROOF STEP]
have "h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None
case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y \<noteq> None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
have "[(x,y)] \<in> LS M q2"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2
[PROOF STEP]
unfolding LS_single_transition h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<nexists>q'. (q2, x, y, q') \<in> FSM.transitions M)

goal (1 subgoal):
 1. \<exists>t\<in>FSM.transitions M. t_source t = q2 \<and> t_input t = x \<and> t_output t = y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "[(x,y)] \<notin> LS M q1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q1
[PROOF STEP]
using None
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None

goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q1
[PROOF STEP]
unfolding LS_single_transition h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>q'. (q1, x, y, q') \<in> FSM.transitions M

goal (1 subgoal):
 1. \<not> (\<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q2
[(x, y)] \<notin> LS M q1
[PROOF STEP]
have "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q2
[(x, y)] \<notin> LS M q1

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q2
[(x, y)] \<notin> LS M q1

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2 \<and> [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 [(x, y)]

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]

goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
using \<open>isin (PT m1) [(x,y)]\<close> \<open>isin t2 [(x,y)]\<close>
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]
isin (PT m1) [(x, y)]
isin t2 [(x, y)]

goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = Some q1'
[PROOF STEP]
have "[(x,y)] \<in> LS M q1"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1
[PROOF STEP]
unfolding LS_single_transition h_obs_Some[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}

goal (1 subgoal):
 1. \<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y
[PROOF STEP]
using insert_compr
[PROOF STATE]
proof (prove)
using this:
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
Set.insert ?a ?B = {x. x = ?a \<or> x \<in> ?B}

goal (1 subgoal):
 1. \<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
have "[(x,y)] \<notin> LS M q2"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q2
[PROOF STEP]
unfolding LS_single_transition h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>q'. (q2, x, y, q') \<in> FSM.transitions M

goal (1 subgoal):
 1. \<not> (\<exists>t\<in>FSM.transitions M. t_source t = q2 \<and> t_input t = x \<and> t_output t = y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<notin> LS M q2
[PROOF STEP]
have "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<notin> LS M q2

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
using \<open>[(x,y)] \<in> LS M q1\<close>
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<notin> LS M q2
[(x, y)] \<in> LS M q1

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<notin> LS M q2
[(x, y)] \<in> LS M q1

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2 \<and> [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 [(x, y)]

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]

goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
using \<open>isin (PT m1) [(x,y)]\<close> \<open>isin t2 [(x,y)]\<close>
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]
isin (PT m1) [(x, y)]
isin t2 [(x, y)]

goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "intersection_is_distinguishing M (the (m1 (x,y))) q1' (the (m2 (x,y))) q2'"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> *
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'
case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'

goal (1 subgoal):
 1. intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "(the (m1 (x,y))) = t1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (m1 (x, y)) = t1'
[PROOF STEP]
using \<open>m1 (x,y) = Some t1'\<close>
[PROOF STATE]
proof (prove)
using this:
m1 (x, y) = Some t1'

goal (1 subgoal):
 1. the (m1 (x, y)) = t1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (m1 (x, y)) = t1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (m1 (x, y)) = t1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "(the (m2 (x,y))) = t2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (m2 (x, y)) = t2'
[PROOF STEP]
using \<open>m2 (x,y) = Some t2'\<close>
[PROOF STATE]
proof (prove)
using this:
m2 (x, y) = Some t2'

goal (1 subgoal):
 1. the (m2 (x, y)) = t2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (m2 (x, y)) = t2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'
the (m1 (x, y)) = t1'
the (m2 (x, y)) = t2'
[PROOF STEP]
have "intersection_is_distinguishing M t1' q1' t2' q2'"
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) q2'
the (m1 (x, y)) = t1'
the (m2 (x, y)) = t2'

goal (1 subgoal):
 1. intersection_is_distinguishing M t1' q1' t2' q2'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1' q1' t2' q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
intersection_is_distinguishing M t1' q1' t2' q2'
[PROOF STEP]
have "\<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io"
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'

goal (1 subgoal):
 1. \<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io
[PROOF STEP]
using PT.IH[of "Some t1'" t1' q1' t2' q2']
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'
\<lbrakk>Some t1' \<in> range m1; t1' \<in> set_option (Some t1'); intersection_is_distinguishing M t1' q1' t2' q2'\<rbrakk> \<Longrightarrow> \<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io

goal (1 subgoal):
 1. \<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io
[PROOF STEP]
by (metis \<open>m1 (x, y) = Some t1'\<close> option.set_intros rangeI)
[PROOF STATE]
proof (state)
this:
\<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io
[PROOF STEP]
obtain io where "isin t1' io"
                         and "isin t2' io"
                         and "distinguishes M q1' q2' io"
[PROOF STATE]
proof (prove)
using this:
\<exists>io. isin t1' io \<and> isin t2' io \<and> distinguishes M q1' q2' io

goal (1 subgoal):
 1. (\<And>io. \<lbrakk>isin t1' io; isin t2' io; distinguishes M q1' q2' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isin t1' io
isin t2' io
distinguishes M q1' q2' io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "isin (PT m1) ((x,y)#io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isin (PT m1) ((x, y) # io)
[PROOF STEP]
using \<open>m1 (x, y) = Some t1'\<close> \<open>isin t1' io\<close>
[PROOF STATE]
proof (prove)
using this:
m1 (x, y) = Some t1'
isin t1' io

goal (1 subgoal):
 1. isin (PT m1) ((x, y) # io)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isin (PT m1) ((x, y) # io)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isin (PT m1) ((x, y) # io)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "isin t2 ((x,y)#io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isin t2 ((x, y) # io)
[PROOF STEP]
using \<open>t2 = PT m2\<close> \<open>m2 (x, y) = Some t2'\<close> \<open>isin t2' io\<close>
[PROOF STATE]
proof (prove)
using this:
t2 = PT m2
m2 (x, y) = Some t2'
isin t2' io

goal (1 subgoal):
 1. isin t2 ((x, y) # io)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isin t2 ((x, y) # io)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isin t2 ((x, y) # io)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
have "distinguishes M q1 q2 ((x,y)#io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
using h_obs_language_iff[OF \<open>observable M\<close>, of x y io  q1]
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. FSM.h_obs M q1 x y = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
unfolding \<open>h_obs M q1 x y = Some q1'\<close>
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
using h_obs_language_iff[OF \<open>observable M\<close>, of x y io  q2]
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. FSM.h_obs M q2 x y = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
unfolding Some
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
using \<open>distinguishes M q1' q2' io\<close>
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')
distinguishes M q1' q2' io

goal (1 subgoal):
 1. distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')
io \<in> LS M q1' \<union> LS M q2' \<and> io \<notin> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. (x, y) # io \<in> LS M q1 \<union> LS M q2 \<and> (x, y) # io \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 ((x, y) # io)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isin (PT m1) ((x, y) # io)
isin t2 ((x, y) # io)
distinguishes M q1 q2 ((x, y) # io)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isin (PT m1) ((x, y) # io)
isin t2 ((x, y) # io)
distinguishes M q1 q2 ((x, y) # io)

goal (1 subgoal):
 1. \<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io. isin (PT m1) io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2 \<Longrightarrow> \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
show "?P2 \<Longrightarrow> ?P1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
assume ?P2
[PROOF STATE]
proof (state)
this:
\<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io
[PROOF STEP]
obtain io where "isin t1 io"
                     and "isin t2 io"
                     and "distinguishes M q1 q2 io"
[PROOF STATE]
proof (prove)
using this:
\<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. (\<And>io. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isin t1 io
isin t2 io
distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isin t1 io
isin t2 io
distinguishes M q1 q2 io
[PROOF STEP]
show ?P1
[PROOF STATE]
proof (prove)
using this:
isin t1 io
isin t2 io
distinguishes M q1 q2 io

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
isin t1 io
isin t2 io
distinguishes M q1 q2 io
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
proof (induction io arbitrary: t1 t2 q1 q2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t1 t2 q1 q2. \<lbrakk>isin t1 []; isin t2 []; distinguishes M q1 q2 []; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
isin t1 []
isin t2 []
distinguishes M q1 q2 []
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (2 subgoals):
 1. \<And>t1 t2 q1 q2. \<lbrakk>isin t1 []; isin t2 []; distinguishes M q1 q2 []; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isin t1 []
isin t2 []
distinguishes M q1 q2 []
q1 \<in> FSM.states M
q2 \<in> FSM.states M
[PROOF STEP]
have "[] \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
using this:
isin t1 []
isin t2 []
distinguishes M q1 q2 []
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. [] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] \<in> LS M q1 \<inter> LS M q2

goal (2 subgoals):
 1. \<And>t1 t2 q1 q2. \<lbrakk>isin t1 []; isin t2 []; distinguishes M q1 q2 []; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "\<not> distinguishes M q1 q2 []"
[PROOF STATE]
proof (prove)
using this:
[] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. \<not> distinguishes M q1 q2 []
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
[] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. \<not> ([] \<in> LS M q1 \<union> LS M q2 \<and> [] \<notin> LS M q1 \<inter> LS M q2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> distinguishes M q1 q2 []

goal (2 subgoals):
 1. \<And>t1 t2 q1 q2. \<lbrakk>isin t1 []; isin t2 []; distinguishes M q1 q2 []; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> distinguishes M q1 q2 []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> distinguishes M q1 q2 []

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
using \<open>distinguishes M q1 q2 []\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> distinguishes M q1 q2 []
distinguishes M q1 q2 []

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case (Cons a io)
[PROOF STATE]
proof (state)
this:
\<lbrakk>isin ?t1.0 io; isin ?t2.0 io; distinguishes M ?q1.0 ?q2.0 io; ?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M ?t1.0 ?q1.0 ?t2.0 ?q2.0
isin t1 (a # io)
isin t2 (a # io)
distinguishes M q1 q2 (a # io)
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
obtain x y where "a = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. a = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a = (x, y)

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
obtain m1 where "t1 = PT m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m1. t1 = PT m1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prefix_tree.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?y = PT x \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>m1. t1 = PT m1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t1 = PT m1

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
obtain t1' where "m1 (x,y) = Some t1'"
                   and "isin t1' io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t1'. \<lbrakk>m1 (x, y) = Some t1'; isin t1' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>isin t1 (a # io)\<close>
[PROOF STATE]
proof (prove)
using this:
isin t1 (a # io)

goal (1 subgoal):
 1. (\<And>t1'. \<lbrakk>m1 (x, y) = Some t1'; isin t1' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>a = (x,y)\<close> \<open>t1 = PT m1\<close> isin.simps
[PROOF STATE]
proof (prove)
using this:
case m1 (x, y) of None \<Rightarrow> False | Some t \<Rightarrow> isin t io

goal (1 subgoal):
 1. (\<And>t1'. \<lbrakk>m1 (x, y) = Some t1'; isin t1' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using case_optionE
[PROOF STATE]
proof (prove)
using this:
case m1 (x, y) of None \<Rightarrow> False | Some t \<Rightarrow> isin t io
\<lbrakk>case ?x of None \<Rightarrow> ?P | Some y \<Rightarrow> ?Q y; \<lbrakk>?x = None; ?P\<rbrakk> \<Longrightarrow> ?thesis; \<And>y. \<lbrakk>?x = Some y; ?Q y\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>t1'. \<lbrakk>m1 (x, y) = Some t1'; isin t1' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m1 (x, y) = Some t1'
isin t1' io

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
obtain m2 where "t2 = PT m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m2. t2 = PT m2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prefix_tree.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?y = PT x \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>m2. t2 = PT m2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t2 = PT m2

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
obtain t2' where "m2 (x,y) = Some t2'"
                   and "isin t2' io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t2'. \<lbrakk>m2 (x, y) = Some t2'; isin t2' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>isin t2 (a # io)\<close>
[PROOF STATE]
proof (prove)
using this:
isin t2 (a # io)

goal (1 subgoal):
 1. (\<And>t2'. \<lbrakk>m2 (x, y) = Some t2'; isin t2' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>a = (x,y)\<close> \<open>t2 = PT m2\<close> isin.simps
[PROOF STATE]
proof (prove)
using this:
case m2 (x, y) of None \<Rightarrow> False | Some t \<Rightarrow> isin t io

goal (1 subgoal):
 1. (\<And>t2'. \<lbrakk>m2 (x, y) = Some t2'; isin t2' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using case_optionE
[PROOF STATE]
proof (prove)
using this:
case m2 (x, y) of None \<Rightarrow> False | Some t \<Rightarrow> isin t io
\<lbrakk>case ?x of None \<Rightarrow> ?P | Some y \<Rightarrow> ?Q y; \<lbrakk>?x = None; ?P\<rbrakk> \<Longrightarrow> ?thesis; \<And>y. \<lbrakk>?x = Some y; ?Q y\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>t2'. \<lbrakk>m2 (x, y) = Some t2'; isin t2' io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m2 (x, y) = Some t2'
isin t2' io

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m2 (x, y) = Some t2'
isin t2' io
[PROOF STEP]
have "(x,y) \<in> dom m1 \<inter> dom m2"
[PROOF STATE]
proof (prove)
using this:
m2 (x, y) = Some t2'
isin t2' io

goal (1 subgoal):
 1. (x, y) \<in> dom m1 \<inter> dom m2
[PROOF STEP]
using \<open>m1 (x,y) = Some t1'\<close>
[PROOF STATE]
proof (prove)
using this:
m2 (x, y) = Some t2'
isin t2' io
m1 (x, y) = Some t1'

goal (1 subgoal):
 1. (x, y) \<in> dom m1 \<inter> dom m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. \<And>a io t1 t2 q1 q2. \<lbrakk>\<And>t1 t2 q1 q2. \<lbrakk>isin t1 io; isin t2 io; distinguishes M q1 q2 io; q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2; isin t1 (a # io); isin t2 (a # io); distinguishes M q1 q2 (a # io); q1 \<in> FSM.states M; q2 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
proof (cases "h_obs M q1 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = None
[PROOF STEP]
have "[(x,y)] \<notin> LS M q1"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None

goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q1
[PROOF STEP]
unfolding LS_single_transition h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>q'. (q1, x, y, q') \<in> FSM.transitions M

goal (1 subgoal):
 1. \<not> (\<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<notin> LS M q1
[PROOF STEP]
have "a#io \<notin> LS M q1"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<notin> LS M q1

goal (1 subgoal):
 1. a # io \<notin> LS M q1
[PROOF STEP]
unfolding \<open>a = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<notin> LS M q1

goal (1 subgoal):
 1. (x, y) # io \<notin> LS M q1
[PROOF STEP]
by (metis None assms(1) h_obs_language_iff option.distinct(1))
[PROOF STATE]
proof (state)
this:
a # io \<notin> LS M q1

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # io \<notin> LS M q1
[PROOF STEP]
have "a#io \<in> LS M q2"
[PROOF STATE]
proof (prove)
using this:
a # io \<notin> LS M q1

goal (1 subgoal):
 1. a # io \<in> LS M q2
[PROOF STEP]
using \<open>distinguishes M q1 q2 (a#io)\<close>
[PROOF STATE]
proof (prove)
using this:
a # io \<notin> LS M q1
distinguishes M q1 q2 (a # io)

goal (1 subgoal):
 1. a # io \<in> LS M q2
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
a # io \<notin> LS M q1
a # io \<in> LS M q1 \<union> LS M q2 \<and> a # io \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. a # io \<in> LS M q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a # io \<in> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # io \<in> LS M q2
[PROOF STEP]
have "[(x,y)] \<in> LS M q2"
[PROOF STATE]
proof (prove)
using this:
a # io \<in> LS M q2

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2
[PROOF STEP]
unfolding \<open>a = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) # io \<in> LS M q2

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2
[PROOF STEP]
using language_prefix
[PROOF STATE]
proof (prove)
using this:
(x, y) # io \<in> LS M q2
?io1.0 @ ?io2.0 \<in> LS ?M ?q \<Longrightarrow> ?io1.0 \<in> LS ?M ?q

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2
[PROOF STEP]
by (metis append_Cons append_Nil)
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q2
[PROOF STEP]
have "h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
unfolding h_obs_None[OF \<open>observable M\<close>] LS_single_transition
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>FSM.transitions M. t_source t = q2 \<and> t_input t = x \<and> t_output t = y

goal (1 subgoal):
 1. \<not> (\<nexists>q'. (q2, x, y, q') \<in> FSM.transitions M)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y \<noteq> None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
using None \<open>(x,y) \<in> dom m1 \<inter> dom m2\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None
FSM.h_obs M q1 x y = None
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
unfolding \<open>t1 = PT m1\<close> \<open>t2 = PT m2\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None
FSM.h_obs M q1 x y = None
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. intersection_is_distinguishing M (PT m1) q1 (PT m2) q2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = Some q1'
[PROOF STEP]
have "[(x,y)] \<in> LS M q1"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1
[PROOF STEP]
unfolding LS_single_transition h_obs_Some[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}

goal (1 subgoal):
 1. \<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y
[PROOF STEP]
by (metis Some assms(1) fst_conv h_obs_None option.distinct(1) snd_conv)
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
using Some \<open>(x,y) \<in> dom m1 \<inter> dom m2\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
unfolding \<open>t1 = PT m1\<close> \<open>t2 = PT m2\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. intersection_is_distinguishing M (PT m1) q1 (PT m2) q2
[PROOF STEP]
unfolding intersection_is_distinguishing.simps
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'
(x, y) \<in> dom m1 \<inter> dom m2

goal (1 subgoal):
 1. \<exists>(x, y)\<in>dom m1 \<inter> dom m2. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some xa \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) xa
[PROOF STEP]
by (metis (no_types, lifting) case_prodI option.case_eq_if option.distinct(1))
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
have "distinguishes M q1' q2' io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
using h_obs_language_iff[OF \<open>observable M\<close>, of x y io  q1]
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. FSM.h_obs M q1 x y = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
unfolding \<open>h_obs M q1 x y = Some q1'\<close>
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
using h_obs_language_iff[OF \<open>observable M\<close>, of x y io  q2]
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. FSM.h_obs M q2 x y = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
unfolding Some
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
using \<open>distinguishes M q1 q2 (a#io)\<close>
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')
distinguishes M q1 q2 (a # io)

goal (1 subgoal):
 1. distinguishes M q1' q2' io
[PROOF STEP]
unfolding \<open>a = (x,y)\<close> distinguishes_def
[PROOF STATE]
proof (prove)
using this:
((x, y) # io \<in> LS M q1) = (\<exists>q'. Some q1' = Some q' \<and> io \<in> LS M q')
((x, y) # io \<in> LS M q2) = (\<exists>q'. Some q2' = Some q' \<and> io \<in> LS M q')
(x, y) # io \<in> LS M q1 \<union> LS M q2 \<and> (x, y) # io \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. io \<in> LS M q1' \<union> LS M q2' \<and> io \<notin> LS M q1' \<inter> LS M q2'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinguishes M q1' q2' io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinguishes M q1' q2' io

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
have "q1' \<in> states M" and "q2' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
using Some \<open>h_obs M q1 x y = Some q1'\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
unfolding h_obs_Some[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
{q'. (q2, x, y, q') \<in> FSM.transitions M} = {q2'}
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
using fsm_transition_target[where M=M]
[PROOF STATE]
proof (prove)
using this:
{q'. (q2, x, y, q') \<in> FSM.transitions M} = {q2'}
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
?t \<in> FSM.transitions M \<Longrightarrow> t_target ?t \<in> FSM.states M

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
q1' \<in> FSM.states M
q2' \<in> FSM.states M

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1' q2' io
q1' \<in> FSM.states M
q2' \<in> FSM.states M
[PROOF STEP]
have "intersection_is_distinguishing M t1' q1' t2' q2'"
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1' q2' io
q1' \<in> FSM.states M
q2' \<in> FSM.states M

goal (1 subgoal):
 1. intersection_is_distinguishing M t1' q1' t2' q2'
[PROOF STEP]
using Cons.IH[OF \<open>isin t1' io\<close> \<open>isin t2' io\<close>]
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1' q2' io
q1' \<in> FSM.states M
q2' \<in> FSM.states M
\<lbrakk>distinguishes M ?q1.0 ?q2.0 io; ?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M\<rbrakk> \<Longrightarrow> intersection_is_distinguishing M t1' ?q1.0 t2' ?q2.0

goal (1 subgoal):
 1. intersection_is_distinguishing M t1' q1' t2' q2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1' q1' t2' q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
intersection_is_distinguishing M t1' q1' t2' q2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
using \<open>(x,y) \<in> dom m1 \<inter> dom m2\<close> Some \<open>h_obs M q1 x y = Some q1'\<close>
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'
(x, y) \<in> dom m1 \<inter> dom m2
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. intersection_is_distinguishing M t1 q1 t2 q2
[PROOF STEP]
unfolding \<open>t1 = PT m1\<close> \<open>t2 = PT m2\<close>
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'
(x, y) \<in> dom m1 \<inter> dom m2
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. intersection_is_distinguishing M (PT m1) q1 (PT m2) q2
[PROOF STEP]
unfolding intersection_is_distinguishing.simps
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M t1' q1' t2' q2'
(x, y) \<in> dom m1 \<inter> dom m2
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<exists>(x, y)\<in>dom m1 \<inter> dom m2. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some xa \<Rightarrow> intersection_is_distinguishing M (the (m1 (x, y))) q1' (the (m2 (x, y))) xa
[PROOF STEP]
by (metis (no_types, lifting) \<open>m1 (x, y) = Some t1'\<close> \<open>m2 (x, y) = Some t2'\<close> case_prodI option.case_eq_if option.distinct(1) option.sel)
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
intersection_is_distinguishing M t1 q1 t2 q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io. isin t1 io \<and> isin t2 io \<and> distinguishes M q1 q2 io \<Longrightarrow> intersection_is_distinguishing M t1 q1 t2 q2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contains_distinguishing_trace_code[code] :
  "contains_distinguishing_trace M (MPT t1) q1 q2 =
    (\<exists> (x,y) \<in> Mapping.keys t1.
      case h_obs M q1 x y of
        None \<Rightarrow> h_obs M q2 x y \<noteq> None |
        Some q1' \<Rightarrow> (case h_obs M q2 x y of
          None \<Rightarrow> True |
          Some q2' \<Rightarrow> contains_distinguishing_trace M (the (Mapping.lookup t1 (x,y))) q1' q2'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains_distinguishing_trace M (MPT t1) q1 q2 = (\<exists>(x, y)\<in>Mapping.keys t1. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> contains_distinguishing_trace M (the (Mapping.lookup t1 (x, y))) q1' q2')
[PROOF STEP]
unfolding intersection_is_distinguishing.simps MPT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains_distinguishing_trace M (PT (Mapping.lookup t1)) q1 q2 = (\<exists>(x, y)\<in>Mapping.keys t1. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> contains_distinguishing_trace M (the (Mapping.lookup t1 (x, y))) q1' q2')
[PROOF STEP]
by (simp add: keys_dom_lookup)


[STATEMENT]
lemma contains_distinguishing_trace_correctness :
  assumes "observable M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "contains_distinguishing_trace M t q1 q2 = (\<exists> io . isin t io \<and> distinguishes M q1 q2 io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains_distinguishing_trace M t q1 q2 = (\<exists>io. isin t io \<and> distinguishes M q1 q2 io)
[PROOF STEP]
using intersection_is_distinguishing_correctness[OF assms]
[PROOF STATE]
proof (prove)
using this:
intersection_is_distinguishing M ?t1.0 q1 ?t2.0 q2 = (\<exists>io. isin ?t1.0 io \<and> isin ?t2.0 io \<and> distinguishes M q1 q2 io)

goal (1 subgoal):
 1. contains_distinguishing_trace M t q1 q2 = (\<exists>io. isin t io \<and> distinguishes M q1 q2 io)
[PROOF STEP]
by simp