[STATEMENT]
lemma simulation_language:
    assumes "alphabet A \<subseteq> alphabet B"
    assumes "\<And> p. p \<in> initial A \<Longrightarrow> \<exists> q \<in> initial B. (p, q) \<in> R"
    assumes "\<And> a p p' q. p' \<in> transition A a p \<Longrightarrow> (p, q) \<in> R \<Longrightarrow> \<exists> q' \<in> transition B a q. (p', q') \<in> R"
    assumes "\<And> p q. (p, q) \<in> R \<Longrightarrow> accepting A p \<Longrightarrow> accepting B q"
    shows "language A \<subseteq> language B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language A \<subseteq> language B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
assume 1: "w \<in> language A"
[PROOF STATE]
proof (state)
this:
w \<in> language A

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain r p where 2: "p \<in> initial A" "run A (w ||| r) p" "infs (accepting A) (p ## r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p r. \<lbrakk>p \<in> initial A; run A (w ||| r) p; infs (accepting A) (p ## r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
w \<in> language A

goal (1 subgoal):
 1. (\<And>p r. \<lbrakk>p \<in> initial A; run A (w ||| r) p; infs (accepting A) (p ## r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
p \<in> initial A
run A (w ||| r) p
infs (accepting A) (p ## r)

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
define P where "P n q \<equiv> (target (stake n (w ||| r)) p, q) \<in> R" for n q
[PROOF STATE]
proof (state)
this:
P ?n ?q \<equiv> (target (stake ?n (w ||| r)) p, ?q) \<in> R

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain q where 3: "q \<in> initial B" "(p, q) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<in> initial B; (p, q) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) 2(1)
[PROOF STATE]
proof (prove)
using this:
?p \<in> initial A \<Longrightarrow> \<exists>q\<in>initial B. (?p, q) \<in> R
p \<in> initial A

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<in> initial B; (p, q) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> initial B
(p, q) \<in> R

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain ws where 4:
      "run B ws q" "\<And> i. P (0 + i) (target (stake i ws) q)" "\<And> i. fst (ws !! i) = w !! (0 + i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule nba.invariant_run_index)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ##
        sdrop (Suc k) (w ||| r) = w ||| r" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ## sdrop (Suc k) (w ||| r) = w ||| r
[PROOF STEP]
by (metis id_stake_snth_sdrop snth_szip sscan_snth szip_smap_snd nba.trace_alt_def)
[PROOF STATE]
proof (state)
this:
stake ?k (w ||| r) @- (w !! ?k, target (stake (Suc ?k) (w ||| r)) p) ## sdrop (Suc ?k) (w ||| r) = w ||| r

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stake ?k (w ||| r) @- (w !! ?k, target (stake (Suc ?k) (w ||| r)) p) ## sdrop (Suc ?k) (w ||| r) = w ||| r

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "run A \<dots> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run A (w ||| r) p
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
run A (w ||| r) p

goal (1 subgoal):
 1. run A (w ||| r) p
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
run A (w ||| r) p

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
[PROOF STEP]
show "\<exists> a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and>
        P (Suc n) (snd a) \<and> fst a = w !! n" if "P n q" for n q
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> P (Suc n) (snd a) \<and> fst a = w !! n
[PROOF STEP]
using assms(1, 3) that
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
alphabet A \<subseteq> alphabet B
\<lbrakk>?p' \<in> transition A ?a ?p; (?p, ?q) \<in> R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition B ?a ?q. (?p', q') \<in> R
P n q

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> P (Suc n) (snd a) \<and> fst a = w !! n
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
alphabet A \<subseteq> alphabet B
\<lbrakk>?p' \<in> transition A ?a ?p; (?p, ?q) \<in> R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition B ?a ?q. (?p', q') \<in> R
(target (stake n (w ||| r)) p, q) \<in> R

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> (target (stake (Suc n) (w ||| r)) p, snd a) \<in> R \<and> fst a = w !! n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
P ?n ?q \<Longrightarrow> \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) ?q) \<and> P (Suc ?n) (snd a) \<and> fst a = w !! ?n

goal (2 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> P ?n2 ?p2
 2. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run B r ?p2; \<And>i. P (?n2 + i) (target (stake i r) ?p2); \<And>i. fst (r !! i) = w !! (?n2 + i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "P 0 q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0 q
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (target (stake 0 (w ||| r)) p, q) \<in> R
[PROOF STEP]
using 3(2)
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> R

goal (1 subgoal):
 1. (target (stake 0 (w ||| r)) p, q) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P 0 q

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run B r q; \<And>i. P (0 + i) (target (stake i r) q); \<And>i. fst (r !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed rule
[PROOF STATE]
proof (state)
this:
run B ws q
P (0 + ?i) (target (stake ?i ws) q)
fst (ws !! ?i) = w !! (0 + ?i)

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain s where 5: "ws = w ||| s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. ws = w ||| s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 4(3)
[PROOF STATE]
proof (prove)
using this:
fst (ws !! ?i) = w !! (0 + ?i)

goal (1 subgoal):
 1. (\<And>s. ws = w ||| s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis add.left_neutral eqI_snth snth_smap szip_smap)
[PROOF STATE]
proof (state)
this:
ws = w ||| s

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
show "w \<in> language B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> language B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?p \<in> initial B
 2. run B (w ||| ?r) ?p
 3. infs (accepting B) (?p ## ?r)
[PROOF STEP]
show "q \<in> initial B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> initial B
[PROOF STEP]
using 3(1)
[PROOF STATE]
proof (prove)
using this:
q \<in> initial B

goal (1 subgoal):
 1. q \<in> initial B
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
q \<in> initial B

goal (2 subgoals):
 1. run B (w ||| ?r) q
 2. infs (accepting B) (q ## ?r)
[PROOF STEP]
show "run B (w ||| s) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
using 4(1)
[PROOF STATE]
proof (prove)
using this:
run B ws q

goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
unfolding 5
[PROOF STATE]
proof (prove)
using this:
run B (w ||| s) q

goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
run B (w ||| s) q

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 6: "(\<lambda> a b. (a, b) \<in> R) \<le> (\<lambda> a b. accepting A a \<longrightarrow> accepting B b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?p, ?q) \<in> R; accepting A ?p\<rbrakk> \<Longrightarrow> accepting B ?q

goal (1 subgoal):
 1. (\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 7: "stream_all2 (\<lambda> p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
using 4(2)
[PROOF STATE]
proof (prove)
using this:
P (0 + ?i) (target (stake ?i ws) q)

goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
unfolding P_def 5
[PROOF STATE]
proof (prove)
using this:
(target (stake (0 + ?i) (w ||| r)) p, target (stake ?i (w ||| s)) q) \<in> R

goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
by (simp add: stream_rel_snth del: stake.simps(2))
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 8: "stream_all2 (\<lambda> a b. accepting A a \<longrightarrow> accepting B b) r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
using stream.rel_mono 6 7
[PROOF STATE]
proof (prove)
using this:
?R \<le> ?Ra \<Longrightarrow> stream_all2 ?R \<le> stream_all2 ?Ra
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)

goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
unfolding nba.trace_alt_def
[PROOF STATE]
proof (prove)
using this:
?R \<le> ?Ra \<Longrightarrow> stream_all2 ?R \<le> stream_all2 ?Ra
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
stream_all2 (\<lambda>p q. (p, q) \<in> R) (smap snd (w ||| r)) (smap snd (w ||| s))

goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
show "infs (accepting B) (q ## s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
using infs_mono_strong 8 2(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stream_all2 (\<lambda>a b. ?P a \<longrightarrow> ?Q b) ?u ?v; infs ?P ?u\<rbrakk> \<Longrightarrow> infs ?Q ?v
stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
infs (accepting A) (p ## r)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infs (accepting B) (q ## s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w \<in> language B

goal:
No subgoals!
[PROOF STEP]
qed