[STATEMENT]
lemma test_suite_to_io_pass_maximal :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
shows "pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> (test_suite_to_io M T) . \<not> (\<exists> io'' . io'' \<noteq> [] \<and> io'@io'' \<in> (test_suite_to_io M T))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
(* finiteness *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
have p1: "finite (test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
using test_suite_to_io_finite[OF assms]
[PROOF STATE]
proof (prove)
using this:
finite (test_suite_to_io M T)

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
finite (test_suite_to_io M T)

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
(* prefix closure *)
[PROOF STATE]
proof (state)
this:
finite (test_suite_to_io M T)

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prs tps rd_targets atcs. T = Test_Suite prs tps rd_targets atcs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson test_suite.exhaust)
[PROOF STATE]
proof (state)
this:
T = Test_Suite prs tps rd_targets atcs

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = Test_Suite prs tps rd_targets atcs
[PROOF STEP]
obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs
implies_completeness T M m

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding implies_completeness_def
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs
Ex (implies_completeness_for_repetition_sets T M m)

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets
[PROOF STEP]
have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. implies_completeness (Test_Suite prs tps rd_targets atcs) M m
[PROOF STEP]
unfolding implies_completeness_def
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. Ex (implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m
[PROOF STEP]
have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M"
[PROOF STATE]
proof (prove)
using this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m

goal (1 subgoal):
 1. test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M
[PROOF STEP]
using test_suite_to_io_language
[PROOF STATE]
proof (prove)
using this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m
implies_completeness ?T ?M ?m \<Longrightarrow> test_suite_to_io ?M ?T \<subseteq> L ?M

goal (1 subgoal):
 1. test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
have p2: "\<And>io' io''. io' @ io'' \<in> test_suite_to_io M T \<Longrightarrow> io' \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M T \<Longrightarrow> io' \<in> test_suite_to_io M T
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
fix io' io''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
assume "io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (state)
this:
io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have preamble_prop : "\<And> io''' q P . (q,P) \<in> prs \<Longrightarrow> io'@io''' \<in> L P \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io''' q P. \<lbrakk>(q, P) \<in> prs; io' @ io''' \<in> L P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io''' q P. \<lbrakk>(q, P) \<in> prs; io' @ io''' \<in> L P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
fix io''' q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io''' q P. \<lbrakk>(q, P) \<in> prs; io' @ io''' \<in> L P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
assume "(q,P) \<in> prs" and "io'@io''' \<in> L P"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io' @ io''' \<in> L P

goal (1 subgoal):
 1. \<And>io''' q P. \<lbrakk>(q, P) \<in> prs; io' @ io''' \<in> L P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have "io' \<in> (\<Union> (q,P) \<in> prs . L P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io' \<in> (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> language_prefix[OF \<open>io'@io''' \<in> L P\<close>]
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
io' \<in> L P

goal (1 subgoal):
 1. io' \<in> (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io' \<in> (\<Union>(q, P)\<in>prs. L P)

goal (1 subgoal):
 1. \<And>io''' q P. \<lbrakk>(q, P) \<in> prs; io' @ io''' \<in> L P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
show "io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (prove)
using this:
io' \<in> (\<Union>(q, P)\<in>prs. L P)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
unfolding test_suite_to_io.simps
[PROOF STATE]
proof (prove)
using this:
io' \<in> (\<Union>(q, P)\<in>prs. L P)

goal (1 subgoal):
 1. io' \<in> (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> prs; io' @ ?io''' \<in> L ?P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have traversal_path_prop : "\<And> io''' p pt q P . io'@io''' \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) \<Longrightarrow> (q,P) \<in> prs \<Longrightarrow> path P (initial P) p \<Longrightarrow> target (initial P) p = q \<Longrightarrow> pt \<in> tps q \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
fix io''' p pt q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
assume "io'@io''' \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
                            and "(q,P) \<in> prs"
                            and "path P (initial P) p"
                            and "target (initial P) p = q"
                            and "pt \<in> tps q"
[PROOF STATE]
proof (state)
this:
io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q

goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
obtain ioP1 where "io'@io''' = p_io p @ ioP1" and "ioP1 \<in> (set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ioP1. \<lbrakk>io' @ io''' = p_io p @ ioP1; ioP1 \<in> set (prefixes (p_io pt))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>io'@io''' \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))\<close>
[PROOF STATE]
proof (prove)
using this:
io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. (\<And>ioP1. \<lbrakk>io' @ io''' = p_io p @ ioP1; ioP1 \<in> set (prefixes (p_io pt))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io' @ io''' = p_io p @ ioP1
ioP1 \<in> set (prefixes (p_io pt))

goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ io''' = p_io p @ ioP1
ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
obtain ioP2 where "ioP1 @ ioP2 = p_io pt"
[PROOF STATE]
proof (prove)
using this:
io' @ io''' = p_io p @ ioP1
ioP1 \<in> set (prefixes (p_io pt))

goal (1 subgoal):
 1. (\<And>ioP2. ioP1 @ ioP2 = p_io pt \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
io' @ io''' = p_io p @ ioP1
ioP1 \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}

goal (1 subgoal):
 1. (\<And>ioP2. ioP1 @ ioP2 = p_io pt \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP1 @ ioP2 = p_io pt

goal (1 subgoal):
 1. \<And>io''' p pt q P. \<lbrakk>io' @ io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
show "io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof (cases "length io' \<le> length (p_io p)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length io' \<le> length (p_io p)

goal (2 subgoals):
 1. length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length io' \<le> length (p_io p)
[PROOF STEP]
have "io' = (take (length io') (p_io p))"
[PROOF STATE]
proof (prove)
using this:
length io' \<le> length (p_io p)

goal (1 subgoal):
 1. io' = take (length io') (p_io p)
[PROOF STEP]
using \<open>io'@io''' = p_io p @ ioP1\<close>
[PROOF STATE]
proof (prove)
using this:
length io' \<le> length (p_io p)
io' @ io''' = p_io p @ ioP1

goal (1 subgoal):
 1. io' = take (length io') (p_io p)
[PROOF STEP]
by (metis (no_types, lifting) order_refl take_all take_le)
[PROOF STATE]
proof (state)
this:
io' = take (length io') (p_io p)

goal (2 subgoals):
 1. length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' = take (length io') (p_io p)
[PROOF STEP]
have "p_io p = io'@(drop (length io') (p_io p))"
[PROOF STATE]
proof (prove)
using this:
io' = take (length io') (p_io p)

goal (1 subgoal):
 1. p_io p = io' @ drop (length io') (p_io p)
[PROOF STEP]
by (metis (no_types, lifting) append_take_drop_id)
[PROOF STATE]
proof (state)
this:
p_io p = io' @ drop (length io') (p_io p)

goal (2 subgoals):
 1. length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io p = io' @ drop (length io') (p_io p)
[PROOF STEP]
have "io'@(drop (length io') (p_io p)) \<in> L P"
[PROOF STATE]
proof (prove)
using this:
p_io p = io' @ drop (length io') (p_io p)

goal (1 subgoal):
 1. io' @ drop (length io') (p_io p) \<in> L P
[PROOF STEP]
using language_state_containment[OF \<open>path P (initial P) p\<close>]
[PROOF STATE]
proof (prove)
using this:
p_io p = io' @ drop (length io') (p_io p)
p_io p = ?io \<Longrightarrow> ?io \<in> L P

goal (1 subgoal):
 1. io' @ drop (length io') (p_io p) \<in> L P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' @ drop (length io') (p_io p) \<in> L P

goal (2 subgoals):
 1. length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ drop (length io') (p_io p) \<in> L P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' @ drop (length io') (p_io p) \<in> L P

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
using preamble_prop[OF \<open>(q,P) \<in> prs\<close>]
[PROOF STATE]
proof (prove)
using this:
io' @ drop (length io') (p_io p) \<in> L P
io' @ ?io''' \<in> L P \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length io' \<le> length (p_io p)

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> length io' \<le> length (p_io p)
[PROOF STEP]
have "io' = p_io p @ (take (length io' - length (p_io p)) ioP1)"
[PROOF STATE]
proof (prove)
using this:
\<not> length io' \<le> length (p_io p)

goal (1 subgoal):
 1. io' = p_io p @ take (length io' - length (p_io p)) ioP1
[PROOF STEP]
using \<open>io'@io''' = p_io p @ ioP1\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> length io' \<le> length (p_io p)
io' @ io''' = p_io p @ ioP1

goal (1 subgoal):
 1. io' = p_io p @ take (length io' - length (p_io p)) ioP1
[PROOF STEP]
by (metis (no_types, lifting) le_cases take_all take_append take_le)
[PROOF STATE]
proof (state)
this:
io' = p_io p @ take (length io' - length (p_io p)) ioP1

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io' = p_io p @ take (length io' - length (p_io p)) ioP1

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have "(take (length io' - length (p_io p)) ioP1) \<in> (set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
have "ioP1 = (take (length io' - length (p_io p)) ioP1) @ (drop (length io' - length (p_io p)) ioP1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioP1 = take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ioP1 = take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP1 = take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1
[PROOF STEP]
have "(take (length io' - length (p_io p)) ioP1) @ ((drop (length io' - length (p_io p)) ioP1) @ ioP2) = p_io pt"
[PROOF STATE]
proof (prove)
using this:
ioP1 = take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt
[PROOF STEP]
using \<open>ioP1 @ ioP2 = p_io pt\<close>
[PROOF STATE]
proof (prove)
using this:
ioP1 = take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1
ioP1 @ ioP2 = p_io pt

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt
[PROOF STEP]
by (metis (mono_tags, lifting) append_assoc)
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
take (length io' - length (p_io p)) ioP1 @ drop (length io' - length (p_io p)) ioP1 @ ioP2 = p_io pt

goal (1 subgoal):
 1. take (length io' - length (p_io p)) ioP1 \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io' = p_io p @ take (length io' - length (p_io p)) ioP1
take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))
[PROOF STEP]
have "io' \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
using this:
io' = p_io p @ take (length io' - length (p_io p)) ioP1
take (length io' - length (p_io p)) ioP1 \<in> set (prefixes (p_io pt))

goal (1 subgoal):
 1. io' \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
have "io' \<in> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})"
[PROOF STATE]
proof (prove)
using this:
io' \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>path P (initial P) p\<close> \<open>target (initial P) p = q\<close> \<open>pt \<in> tps q\<close>
[PROOF STATE]
proof (prove)
using this:
io' \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q

goal (1 subgoal):
 1. io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
unfolding test_suite_to_io.simps
[PROOF STATE]
proof (prove)
using this:
io' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. io' \<in> (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>io' @ ?io''' \<in> (@) (p_io ?p) ` set (prefixes (p_io ?pt)); (?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?p; target (FSM.initial ?P) ?p = ?q; ?pt \<in> tps ?q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
from \<open>io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)\<close>
[PROOF STATE]
proof (chain)
picking this:
io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
consider
      (a) "io' @ io'' \<in> (\<Union> (q,P) \<in> prs . L P)" |
      (b) "io' @ io'' \<in> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})" |
      (c) "io' @ io'' \<in> (\<Union>{(\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . \<exists> P q' t1 t2 . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q,pt) \<and> (A,t1,t2) \<in> atcs (target q pt,q') })"
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<lbrakk>io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> thesis; io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> thesis; io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding test_suite_to_io.simps
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. \<lbrakk>io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> thesis; io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> thesis; io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>io' io''. io' @ io'' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> ?thesis; io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 3. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P)

goal (3 subgoals):
 1. io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 3. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
using preamble_prop
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> (\<Union>(q, P)\<in>prs. L P)
\<lbrakk>(?q, ?P) \<in> prs; io' @ ?io''' \<in> L ?P\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (2 subgoals):
 1. io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (2 subgoals):
 1. io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
using traversal_path_prop
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
\<lbrakk>io' @ ?io''' \<in> (@) (p_io ?p) ` set (prefixes (p_io ?pt)); (?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?p; target (FSM.initial ?P) ?p = ?q; ?pt \<in> tps ?q\<rbrakk> \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case c
[PROOF STATE]
proof (state)
this:
io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
obtain p pt q A  P q' t1 t2  where "io' @ io'' \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
                                          and "(q,P) \<in> prs"
                                          and "path P (initial P) p"
                                          and "target (initial P) p = q"
                                          and "pt \<in> tps q"
                                          and "q' \<in> rd_targets (q,pt)"
                                          and "(A,t1,t2) \<in> atcs (target q pt,q')"
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. (\<And>p pt q A P q' t1 t2. \<lbrakk>io' @ io'' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A; (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q; q' \<in> rd_targets (q, pt); (A, t1, t2) \<in> atcs (target q pt, q')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' @ io'' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q
q' \<in> rd_targets (q, pt)
(A, t1, t2) \<in> atcs (target q pt, q')

goal (1 subgoal):
 1. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
obtain ioA where "io' @ io'' = p_io p @ p_io pt @ ioA"
                   and "ioA \<in> (atc_to_io_set (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ioA. \<lbrakk>io' @ io'' = p_io p @ p_io pt @ ioA; ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>io' @ io'' \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)\<close>
[PROOF STATE]
proof (prove)
using this:
io' @ io'' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. (\<And>ioA. \<lbrakk>io' @ io'' = p_io p @ p_io pt @ ioA; ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' @ io'' = p_io p @ p_io pt @ ioA
ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io' @ io'' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
proof (cases "length io' \<le> length (p_io p @ p_io pt)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length io' \<le> length (p_io p @ p_io pt)

goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length io' \<le> length (p_io p @ p_io pt)
[PROOF STEP]
have "io' @ (drop (length io') (p_io p @ p_io pt)) = p_io p @ p_io pt"
[PROOF STATE]
proof (prove)
using this:
length io' \<le> length (p_io p @ p_io pt)

goal (1 subgoal):
 1. io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt
[PROOF STEP]
using \<open>io' @ io'' = p_io p @ p_io pt @ ioA\<close>
[PROOF STATE]
proof (prove)
using this:
length io' \<le> length (p_io p @ p_io pt)
io' @ io'' = p_io p @ p_io pt @ ioA

goal (1 subgoal):
 1. io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt
[PROOF STEP]
by (simp add: append_eq_conv_conj)
[PROOF STATE]
proof (state)
this:
io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt

goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt

goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have "p_io p @ p_io pt \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io p @ p_io pt \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io p @ p_io pt \<in> (@) (p_io p) ` {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p_io p @ p_io pt \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt
p_io p @ p_io pt \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
have "io'@(drop (length io') (p_io p @ p_io pt)) \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
using this:
io' @ drop (length io') (p_io p @ p_io pt) = p_io p @ p_io pt
p_io p @ p_io pt \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io' @ drop (length io') (p_io p @ p_io pt) \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
io' @ drop (length io') (p_io p @ p_io pt) \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (2 subgoals):
 1. length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
 2. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' @ drop (length io') (p_io p @ p_io pt) \<in> (@) (p_io p) ` set (prefixes (p_io pt))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' @ drop (length io') (p_io p @ p_io pt) \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
using traversal_path_prop[OF _ \<open>(q,P) \<in> prs\<close> \<open>path P (initial P) p\<close> \<open>target (initial P) p = q\<close> \<open>pt \<in> tps q\<close>]
[PROOF STATE]
proof (prove)
using this:
io' @ drop (length io') (p_io p @ p_io pt) \<in> (@) (p_io p) ` set (prefixes (p_io pt))
io' @ ?io''' \<in> (@) (p_io p) ` set (prefixes (p_io pt)) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length io' \<le> length (p_io p @ p_io pt)

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> length io' \<le> length (p_io p @ p_io pt)
[PROOF STEP]
have "io' = (p_io p @ p_io pt) @ (take (length io' - length (p_io p @ p_io pt)) ioA)"
[PROOF STATE]
proof (prove)
using this:
\<not> length io' \<le> length (p_io p @ p_io pt)

goal (1 subgoal):
 1. io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
[PROOF STEP]
have "io' = take (length io') (io' @ io'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io' = take (length io') (io' @ io'')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io' = take (length io') (io' @ io'')

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' = take (length io') (io' @ io'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' = take (length io') (io' @ io'')

goal (1 subgoal):
 1. io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
[PROOF STEP]
using False \<open>io' @ io'' = p_io p @ p_io pt @ ioA\<close>
[PROOF STATE]
proof (prove)
using this:
io' = take (length io') (io' @ io'')
\<not> length io' \<le> length (p_io p @ p_io pt)
io' @ io'' = p_io p @ p_io pt @ ioA

goal (1 subgoal):
 1. io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
have "(take (length io' - length (p_io p @ p_io pt)) ioA) \<in> (atc_to_io_set (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
have "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) \<in> L (from_FSM M (target q pt)) \<inter> L A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
using \<open>ioA \<in> (atc_to_io_set (from_FSM M (target q pt)) A)\<close>
[PROOF STATE]
proof (prove)
using this:
ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
have *: "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) \<in> L (from_FSM M (target q pt))"
               and **: "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) \<in> L A"
[PROOF STATE]
proof (prove)
using this:
take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) &&& take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L A
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt))
take (length io' - length (p_io p @ p_io pt)) ioA @ drop (length io' - length (p_io p @ p_io pt)) ioA \<in> L A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
using language_prefix[OF *] language_prefix[OF **]
[PROOF STATE]
proof (prove)
using this:
take (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt))
take (length io' - length (p_io p @ p_io pt)) ioA \<in> L A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
unfolding atc_to_io_set.simps
[PROOF STATE]
proof (prove)
using this:
take (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt))
take (length io' - length (p_io p @ p_io pt)) ioA \<in> L A

goal (1 subgoal):
 1. take (length io' - length (p_io p @ p_io pt)) ioA \<in> L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
have "io' \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
using this:
io' = (p_io p @ p_io pt) @ take (length io' - length (p_io p @ p_io pt)) ioA
take (length io' - length (p_io p @ p_io pt)) ioA \<in> atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
have "io' \<in> (\<Union>{(\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . \<exists> P q' t1 t2 . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q,pt) \<and> (A,t1,t2) \<in> atcs (target q pt,q') })"
[PROOF STATE]
proof (prove)
using this:
io' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>path P (initial P) p\<close> \<open>target (initial P) p = q\<close> \<open>pt \<in> tps q\<close> \<open>q' \<in> rd_targets (q,pt)\<close> \<open>(A,t1,t2) \<in> atcs (target q pt,q')\<close>
[PROOF STATE]
proof (prove)
using this:
io' \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q
q' \<in> rd_targets (q, pt)
(A, t1, t2) \<in> atcs (target q pt, q')

goal (1 subgoal):
 1. io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. \<not> length io' \<le> length (p_io p @ p_io pt) \<Longrightarrow> io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)
[PROOF STEP]
unfolding test_suite_to_io.simps
[PROOF STATE]
proof (prove)
using this:
io' \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. io' \<in> (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io' \<in> test_suite_to_io M (Test_Suite prs tps rd_targets atcs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?io' @ ?io'' \<in> test_suite_to_io M T \<Longrightarrow> ?io' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?io' @ ?io'' \<in> test_suite_to_io M T \<Longrightarrow> ?io' \<in> test_suite_to_io M T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?io' @ ?io'' \<in> test_suite_to_io M T \<Longrightarrow> ?io' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
using pass_io_set_maximal_from_pass_io_set[OF p1]
[PROOF STATE]
proof (prove)
using this:
?io' @ ?io'' \<in> test_suite_to_io M T \<Longrightarrow> ?io' \<in> test_suite_to_io M T
(\<And>io' io''. io' @ io'' \<in> test_suite_to_io M T \<Longrightarrow> io' \<in> test_suite_to_io M T) \<Longrightarrow> pass_io_set ?M (test_suite_to_io M T) = pass_io_set_maximal ?M {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma passes_test_suite_as_maximal_sequences_completeness :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M"
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "inputs M \<noteq> {}"
  and     "completely_specified M"
  and     "completely_specified M'"
  and     "size M' \<le> m"
shows     "(L M' \<subseteq> L M) \<longleftrightarrow> pass_io_set_maximal M' (test_suite_to_io_maximal M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (L M' \<subseteq> L M) = pass_io_set_maximal M' (test_suite_to_io_maximal M T)
[PROOF STEP]
unfolding passes_test_suite_completeness[OF assms(1,3-9)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. passes_test_suite M T M' = pass_io_set_maximal M' (test_suite_to_io_maximal M T)
[PROOF STEP]
unfolding test_suite_to_io_pass[OF assms(1,3-8),symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' (test_suite_to_io_maximal M T)
[PROOF STEP]
unfolding test_suite_to_io_pass_maximal[OF assms(1,2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_io_set_maximal M' {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = pass_io_set_maximal M' (test_suite_to_io_maximal M T)
[PROOF STEP]
unfolding test_suite_to_io_maximal_code[OF assms(1,2,3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_io_set_maximal M' (test_suite_to_io_maximal M T) = pass_io_set_maximal M' (test_suite_to_io_maximal M T)
[PROOF STEP]
by simp


[STATEMENT]
lemma test_suite_to_io_maximal_finite :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M"
shows "finite (test_suite_to_io_maximal M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (test_suite_to_io_maximal M T)
[PROOF STEP]
using test_suite_to_io_finite[OF assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
finite (test_suite_to_io M T)

goal (1 subgoal):
 1. finite (test_suite_to_io_maximal M T)
[PROOF STEP]
unfolding test_suite_to_io_maximal_code[OF assms, symmetric]
[PROOF STATE]
proof (prove)
using this:
finite (test_suite_to_io M T)

goal (1 subgoal):
 1. finite {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
by simp


[STATEMENT]
lemma Trivial_Aexp_simp: "Trivial_Aexp e \<cdot> n = (\<lambda> x. up\<cdot>0) f|` fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Trivial_Aexp e\<cdot>n = (\<lambda>x. up\<cdot>0) f|` fv e
[PROOF STEP]
unfolding Trivial_Aexp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> n. (\<lambda>x. up\<cdot>0) f|` fv e)\<cdot>n = (\<lambda>x. up\<cdot>0) f|` fv e
[PROOF STEP]
by simp


[STATEMENT]
lemma edom_Trivial_Aexp[simp]: "edom (Trivial_Aexp e \<cdot> n) = fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edom (Trivial_Aexp e\<cdot>n) = fv e
[PROOF STEP]
by (auto simp add: edom_def env_restr_def Trivial_Aexp_def)


[STATEMENT]
lemma Trivial_Aexp_eq[iff]: "Trivial_Aexp e \<cdot> n = Trivial_Aexp e' \<cdot> n' \<longleftrightarrow> fv e = (fv e' :: var set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Trivial_Aexp e\<cdot>n = Trivial_Aexp e'\<cdot>n') = (fv e = fv e')
[PROOF STEP]
apply (auto simp add: Trivial_Aexp_simp env_restr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(\<lambda>x. if x \<in> fv e then up\<cdot>0 else \<bottom>) = (\<lambda>x. if x \<in> fv e' then up\<cdot>0 else \<bottom>); x \<in> fv e\<rbrakk> \<Longrightarrow> x \<in> fv e'
 2. \<And>x. \<lbrakk>(\<lambda>x. if x \<in> fv e then up\<cdot>0 else \<bottom>) = (\<lambda>x. if x \<in> fv e' then up\<cdot>0 else \<bottom>); x \<in> fv e'\<rbrakk> \<Longrightarrow> x \<in> fv e
[PROOF STEP]
apply (metis up_defined)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma below_Trivial_Aexp[simp]: "(ae \<sqsubseteq> Trivial_Aexp e \<cdot> n) \<longleftrightarrow> edom ae \<subseteq> fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ae \<sqsubseteq> Trivial_Aexp e\<cdot>n) = (edom ae \<subseteq> fv e)
[PROOF STEP]
by (auto dest:fun_belowD intro!: fun_belowI  simp add: Trivial_Aexp_def env_restr_def edom_def split:if_splits)


[STATEMENT]
lemma Trivial_Aheap_eqvt[eqvt]: "\<pi> \<bullet>  (Trivial_Aheap \<Gamma> e) = Trivial_Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> Trivial_Aheap \<Gamma> e = Trivial_Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)
[PROOF STEP]
unfolding Trivial_Aheap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> (\<Lambda> a. (\<lambda>x. up\<cdot>0) f|` domA \<Gamma>) = (\<Lambda> a. (\<lambda>x. up\<cdot>0) f|` domA (\<pi> \<bullet> \<Gamma>))
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<bullet> Abs_cfun) (\<lambda>x. (\<lambda>x. up\<cdot>0) f|` domA (\<pi> \<bullet> \<Gamma>)) = (\<Lambda> a. (\<lambda>x. up\<cdot>0) f|` domA (\<pi> \<bullet> \<Gamma>))
[PROOF STEP]
apply (simp add: Abs_cfun_eqvt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Trivial_Aheap_simp: "Trivial_Aheap \<Gamma> e\<cdot> a = (\<lambda> x. up\<cdot>0) f|` domA \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Trivial_Aheap \<Gamma> e\<cdot>a = (\<lambda>x. up\<cdot>0) f|` domA \<Gamma>
[PROOF STEP]
unfolding Trivial_Aheap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> a. (\<lambda>x. up\<cdot>0) f|` domA \<Gamma>)\<cdot>a = (\<lambda>x. up\<cdot>0) f|` domA \<Gamma>
[PROOF STEP]
by simp


[STATEMENT]
lemma Trivial_fup_Aexp_below_fv: "fup\<cdot>(Trivial_Aexp e)\<cdot>a \<sqsubseteq> (\<lambda> x . up\<cdot>0) f|` fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Aexp_bot_syn a e \<sqsubseteq> (\<lambda>x. up\<cdot>0) f|` fv e
[PROOF STEP]
by (cases a)(auto simp add: Trivial_Aexp_simp)


[STATEMENT]
lemma Trivial_Abinds_below_fv: "ABinds \<Gamma>\<cdot>ae \<sqsubseteq> (\<lambda> x . up\<cdot>0) f|` fv \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>ae \<sqsubseteq> (\<lambda>x. up\<cdot>0) f|` fv \<Gamma>
[PROOF STEP]
by (induction \<Gamma> rule:ABinds.induct)
     (auto simp add: join_below_iff intro!: below_trans[OF Trivial_fup_Aexp_below_fv] env_restr_mono2 elim: below_trans dest: subsetD[OF fv_delete_subset] simp del: fun_meet_simp)


[STATEMENT]
lemma rtranclp_tranclpE:
  assumes "r^** x y"
  obtains (refl) "x = y"
  | (trancl) "r^++ x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y \<Longrightarrow> thesis; r\<^sup>+\<^sup>+ x y \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r\<^sup>*\<^sup>* x y

goal (1 subgoal):
 1. \<lbrakk>x = y \<Longrightarrow> thesis; r\<^sup>+\<^sup>+ x y \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases)(blast dest: rtranclp_into_tranclp1)+


[STATEMENT]
lemma map_of_map2: "map_of (map (\<lambda>(k, v). (k, f k v)) xs) k = map_option (f k) (map_of xs k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>(k, v). (k, f k v)) xs) k = map_option (f k) (map_of xs k)
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma map_of_map_K: "map_of (map (\<lambda>k. (k, c)) xs) k = (if k \<in> set xs then Some c else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>k. (k, c)) xs) k = (if k \<in> set xs then \<lfloor>c\<rfloor> else None)
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma map_values_Mapping [simp]:
  "map_values f (Mapping.Mapping m) = Mapping.Mapping (\<lambda>k. map_option (f k) (m k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_values f (mapping.Mapping m) = mapping.Mapping (\<lambda>k. map_option (f k) (m k))
[PROOF STEP]
by(rule map_values.abs_eq)


[STATEMENT]
lemma map_Mapping: "Mapping.map f g (Mapping.Mapping m) = Mapping.Mapping (map_option g \<circ> m \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map f g (mapping.Mapping m) = mapping.Mapping (map_option g \<circ> m \<circ> f)
[PROOF STEP]
by(rule map.abs_eq)


[STATEMENT]
lemma impl_of_ProgImpl [simp]:
  "wf_prog_impl' Pfsm \<Longrightarrow> impl_of (ProgRefine Pfsm) = Pfsm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog_impl' Pfsm \<Longrightarrow> impl_of (ProgRefine Pfsm) = Pfsm
[PROOF STEP]
by(simp add: ProgRefine_inverse)


[STATEMENT]
lemma prog_impl_eq_iff:
  "Pi = Pi' \<longleftrightarrow> program Pi = program Pi'" for Pi Pi'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pi = Pi') = (program Pi = program Pi')
[PROOF STEP]
apply(cases Pi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>Pi = ProgRefine y; y \<in> {P. wf_prog_impl' P}\<rbrakk> \<Longrightarrow> (Pi = Pi') = (program Pi = program Pi')
[PROOF STEP]
apply(cases Pi')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>Pi = ProgRefine y; y \<in> {P. wf_prog_impl' P}; Pi' = ProgRefine ya; ya \<in> {P. wf_prog_impl' P}\<rbrakk> \<Longrightarrow> (Pi = Pi') = (program Pi = program Pi')
[PROOF STEP]
apply(auto simp add: ProgRefine_inverse program_def ProgRefine_inject)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_prog_impl'_impl_of [simp, intro!]:
  "wf_prog_impl' (impl_of Pi)" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog_impl' (impl_of Pi)
[PROOF STEP]
using impl_of[of Pi]
[PROOF STATE]
proof (prove)
using this:
impl_of Pi \<in> {P. wf_prog_impl' P}

goal (1 subgoal):
 1. wf_prog_impl' (impl_of Pi)
[PROOF STEP]
by simp


[STATEMENT]
lemma ProgImpl_impl_of [simp, code abstype]:
  "ProgRefine (impl_of Pi) = Pi" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ProgRefine (impl_of Pi) = Pi
[PROOF STEP]
by(rule impl_of_inverse)


[STATEMENT]
lemma program_ProgRefine [simp]: "wf_prog_impl' Psfm \<Longrightarrow> program (ProgRefine Psfm) = Program (fst Psfm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog_impl' Psfm \<Longrightarrow> program (ProgRefine Psfm) = Program (fst Psfm)
[PROOF STEP]
by(simp add: program_def)


[STATEMENT]
lemma classes_program [code]: "classes (program P) = fst (impl_of P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classes (program P) = fst (impl_of P)
[PROOF STEP]
by(simp add: program_def)


[STATEMENT]
lemma class_program [code]: "class (program Pi) = Mapping.lookup (fst (snd (impl_of Pi)))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class (program Pi) = Mapping.lookup (fst (snd (impl_of Pi)))
[PROOF STEP]
by(cases Pi)(clarsimp simp add: tabulate_class_def lookup.rep_eq Mapping_inverse)


[STATEMENT]
lemma subcls'_program [code]:
  "subcls' (program Pi) C D \<longleftrightarrow>
  C = D \<or>
  (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None \<Rightarrow> False
   | Some m \<Rightarrow> D \<in> m)" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls' (program Pi) C D = (C = D \<or> (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None \<Rightarrow> False | \<lfloor>m\<rfloor> \<Rightarrow> D \<in> m))
[PROOF STEP]
apply(cases Pi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>Pi = ProgRefine y; y \<in> {P. wf_prog_impl' P}\<rbrakk> \<Longrightarrow> subcls' (program Pi) C D = (C = D \<or> (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None \<Rightarrow> False | \<lfloor>m\<rfloor> \<Rightarrow> D \<in> m))
[PROOF STEP]
apply(clarsimp simp add: subcls'_def tabulate_subcls_def lookup.rep_eq Mapping_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. Pi = ProgRefine (a, tabulate_class a, mapping.Mapping (\<lambda>C. if is_class (Program a) C then \<lfloor>Collect (subcls (Program (id a)) C)\<rfloor> else None), tabulate_sees_field a, tabulate_Method a) \<Longrightarrow> (is_class (Program a) C \<longrightarrow> Program a \<turnstile> C \<preceq>\<^sup>* D = (C = D \<or> Program a \<turnstile> C \<preceq>\<^sup>* D)) \<and> (\<not> is_class (Program a) C \<longrightarrow> Program a \<turnstile> C \<preceq>\<^sup>* D = (C = D))
[PROOF STEP]
apply(auto elim!: rtranclp_tranclpE dest: subcls_is_class intro: tranclp_into_rtranclp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subcls'_i_i_i_program [code]:
  "subcls'_i_i_i P C D = (if subcls' P C D then Predicate.single () else bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls'_i_i_i P C D = (if subcls' P C D then Predicate.single () else bot)
[PROOF STEP]
by(rule pred_eqI)(auto elim: subcls'_i_i_iE intro: subcls'_i_i_iI)


[STATEMENT]
lemma subcls'_i_i_o_program [code]:
  "subcls'_i_i_o (program Pi) C =
  sup (Predicate.single C) (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None \<Rightarrow> bot | Some m \<Rightarrow> pred_of_set m)" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls'_i_i_o (program Pi) C = sup (Predicate.single C) (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None \<Rightarrow> bot | \<lfloor>m\<rfloor> \<Rightarrow> pred_of_set m)
[PROOF STEP]
by(cases Pi)(fastforce simp add: subcls'_i_i_o_def subcls'_def tabulate_subcls_def lookup.rep_eq Mapping_inverse intro!: pred_eqI split: if_split_asm elim: rtranclp_tranclpE dest: subcls_is_class intro: tranclp_into_rtranclp)


[STATEMENT]
lemma rtranclp_FioB_i_i_subcls1_i_i_o_code [code_unfold]:
  "rtranclp_FioB_i_i (subcls1_i_i_o P) = subcls'_i_i_i P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rtranclp_FioB_i_i (subcls1_i_i_o P) = subcls'_i_i_i P
[PROOF STEP]
by(auto simp add: fun_eq_iff subcls1_i_i_o_def subcls'_def rtranclp_FioB_i_i_def subcls'_i_i_i_def)


[STATEMENT]
lemma Method_program [code]:
  "program Pi \<turnstile> C sees M:Ts\<rightarrow>T=meth in D \<longleftrightarrow>
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> False
  | Some m \<Rightarrow>
    (case Mapping.lookup m M of
       None \<Rightarrow> False
     | Some (D', Ts', T', meth') \<Rightarrow> Ts = Ts' \<and> T = T' \<and> meth = meth' \<and> D = D'))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (program Pi \<turnstile> C sees M: Ts\<rightarrow>T = meth in D) = (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> False | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m M of None \<Rightarrow> False | \<lfloor>(D', Ts', T', meth')\<rfloor> \<Rightarrow> Ts = Ts' \<and> T = T' \<and> meth = meth' \<and> D = D')
[PROOF STEP]
by(cases Pi)(auto split: if_split_asm dest: sees_method_is_class simp add: tabulate_Method_def lookup.rep_eq Mapping_inverse)


[STATEMENT]
lemma Method_i_i_i_o_o_o_o_program [code]:
  "Method_i_i_i_o_o_o_o (program Pi) C M =
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> bot
  | Some m \<Rightarrow>
    (case Mapping.lookup m M of
      None \<Rightarrow> bot
    | Some (D, Ts, T, meth) \<Rightarrow> Predicate.single (Ts, T, meth, D)))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Method_i_i_i_o_o_o_o (program Pi) C M = (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> bot | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m M of None \<Rightarrow> bot | \<lfloor>(D, Ts, T, meth)\<rfloor> \<Rightarrow> Predicate.single (Ts, T, meth, D))
[PROOF STEP]
by(auto simp add: Method_i_i_i_o_o_o_o_def Method_program intro!: pred_eqI)


[STATEMENT]
lemma Method_i_i_i_o_o_o_i_program [code]:
  "Method_i_i_i_o_o_o_i (program Pi) C M D =
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> bot
  | Some m \<Rightarrow>
    (case Mapping.lookup m M of
      None \<Rightarrow> bot
    | Some (D', Ts, T, meth) \<Rightarrow> if D = D' then Predicate.single (Ts, T, meth) else bot))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Method_i_i_i_o_o_o_i (program Pi) C M D = (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> bot | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m M of None \<Rightarrow> bot | \<lfloor>(D', Ts, T, meth)\<rfloor> \<Rightarrow> if D = D' then Predicate.single (Ts, T, meth) else bot)
[PROOF STEP]
by(auto simp add: Method_i_i_i_o_o_o_i_def Method_program intro!: pred_eqI)


[STATEMENT]
lemma sees_field_program [code]:
  "program Pi \<turnstile> C sees F:T (fd) in D \<longleftrightarrow>
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> False
  | Some m \<Rightarrow>
    (case Mapping.lookup m F of
       None \<Rightarrow> False
     | Some (D', T', fd') \<Rightarrow> T = T' \<and> fd = fd' \<and> D = D'))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (program Pi \<turnstile> C sees F:T (fd) in D) = (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> False | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m F of None \<Rightarrow> False | \<lfloor>(D', T', fd')\<rfloor> \<Rightarrow> T = T' \<and> fd = fd' \<and> D = D')
[PROOF STEP]
by(cases Pi)(auto split: if_split_asm dest: has_visible_field[THEN has_field_is_class] simp add: tabulate_sees_field_def lookup.rep_eq Mapping_inverse)


[STATEMENT]
lemma sees_field_i_i_i_o_o_o_program [code]:
  "sees_field_i_i_i_o_o_o (program Pi) C F =
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> bot
  | Some m \<Rightarrow>
    (case Mapping.lookup m F of
       None \<Rightarrow> bot
    | Some (D, T, fd) \<Rightarrow> Predicate.single(T, fd, D)))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sees_field_i_i_i_o_o_o (program Pi) C F = (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> bot | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m F of None \<Rightarrow> bot | \<lfloor>(D, T, fd)\<rfloor> \<Rightarrow> Predicate.single (T, fd, D))
[PROOF STEP]
by(auto simp add: sees_field_program sees_field_i_i_i_o_o_o_def intro: pred_eqI)


[STATEMENT]
lemma sees_field_i_i_i_o_o_i_program [code]:
  "sees_field_i_i_i_o_o_i (program Pi) C F D =
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> bot
  | Some m \<Rightarrow>
    (case Mapping.lookup m F of
       None \<Rightarrow> bot
    | Some (D', T, fd) \<Rightarrow> if D = D' then Predicate.single(T, fd) else bot))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sees_field_i_i_i_o_o_i (program Pi) C F D = (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> bot | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m F of None \<Rightarrow> bot | \<lfloor>(D', T, fd)\<rfloor> \<Rightarrow> if D = D' then Predicate.single (T, fd) else bot)
[PROOF STEP]
by(auto simp add: sees_field_program sees_field_i_i_i_o_o_i_def intro: pred_eqI)


[STATEMENT]
lemma field_program [code]:
  "field (program Pi) C F =
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None \<Rightarrow> Code.abort (STR ''not_unique'') (\<lambda>_. Predicate.the bot)
  | Some m \<Rightarrow>
    (case Mapping.lookup m F of
       None \<Rightarrow> Code.abort (STR ''not_unique'') (\<lambda>_. Predicate.the bot)
     | Some (D', T, fd) \<Rightarrow> (D', T, fd)))" for Pi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field (program Pi) C F = (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> Code.abort STR ''not_unique'' (\<lambda>_. Predicate.the bot) | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m F of None \<Rightarrow> Code.abort STR ''not_unique'' (\<lambda>_. Predicate.the bot) | \<lfloor>(D', T, fd)\<rfloor> \<Rightarrow> (D', T, fd))
[PROOF STEP]
unfolding field_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE (D, T, fm). program Pi \<turnstile> C sees F:T (fm) in D) = (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of None \<Rightarrow> Code.abort STR ''not_unique'' (\<lambda>_. Predicate.the bot) | \<lfloor>m\<rfloor> \<Rightarrow> case Mapping.lookup m F of None \<Rightarrow> Code.abort STR ''not_unique'' (\<lambda>_. Predicate.the bot) | \<lfloor>(D', T, fd)\<rfloor> \<Rightarrow> (D', T, fd))
[PROOF STEP]
by(cases Pi)(fastforce simp add: Predicate.the_def tabulate_sees_field_def lookup.rep_eq Mapping_inverse split: if_split_asm intro: arg_cong[where f=The] dest: has_visible_field[THEN has_field_is_class] sees_field_fun)


[STATEMENT]
lemma impl_of_tabulate_program [code abstract]:
  "impl_of (tabulate_program P) = (P, tabulate_class P, tabulate_subcls P, tabulate_sees_field P, tabulate_Method P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of (tabulate_program P) = (P, tabulate_class P, tabulate_subcls P, tabulate_sees_field P, tabulate_Method P)
[PROOF STEP]
by(simp add: tabulate_program_def)


[STATEMENT]
lemma Program_code [code]:
  "Program = program \<circ> tabulate_program"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Program = program \<circ> tabulate_program
[PROOF STEP]
by(simp add: program_def fun_eq_iff tabulate_program_def)


[STATEMENT]
lemma tabulate_class_code [code]:
  "tabulate_class = Mapping.of_alist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_class = Mapping.of_alist
[PROOF STEP]
by transfer (simp add: fun_eq_iff)


[STATEMENT]
lemma subcls1_into_subcls1':
  assumes "subcls1 (Program P) C D"
  shows "subcls1' P C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls1' P C D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subcls1' P C D
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Program P \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
obtain rest where "map_of P C = \<lfloor>(D, rest)\<rfloor>" "C \<noteq> Object"
[PROOF STATE]
proof (prove)
using this:
Program P \<turnstile> C \<prec>\<^sup>1 D

goal (1 subgoal):
 1. (\<And>rest. \<lbrakk>map_of P C = \<lfloor>(D, rest)\<rfloor>; C \<noteq> Object\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases simp
[PROOF STATE]
proof (state)
this:
map_of P C = \<lfloor>(D, rest)\<rfloor>
C \<noteq> Object

goal (1 subgoal):
 1. subcls1' P C D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_of P C = \<lfloor>(D, rest)\<rfloor>
C \<noteq> Object

goal (1 subgoal):
 1. subcls1' P C D
[PROOF STEP]
by(induct P)(auto split: if_split_asm intro: subcls1'.intros)
[PROOF STATE]
proof (state)
this:
subcls1' P C D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcls1'_into_subcls1:
  assumes "subcls1' P C D"
  shows "subcls1 (Program P) C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Program P \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subcls1' P C D

goal (1 subgoal):
 1. Program P \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C D rest P. C \<noteq> Object \<Longrightarrow> Program ((C, D, rest) # P) \<turnstile> C \<prec>\<^sup>1 D
 2. \<And>C C' P D D' rest. \<lbrakk>C \<noteq> Object; C \<noteq> C'; subcls1' P C D; Program P \<turnstile> C \<prec>\<^sup>1 D\<rbrakk> \<Longrightarrow> Program ((C', D', rest) # P) \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
case find
[PROOF STATE]
proof (state)
this:
C_ \<noteq> Object

goal (2 subgoals):
 1. \<And>C D rest P. C \<noteq> Object \<Longrightarrow> Program ((C, D, rest) # P) \<turnstile> C \<prec>\<^sup>1 D
 2. \<And>C C' P D D' rest. \<lbrakk>C \<noteq> Object; C \<noteq> C'; subcls1' P C D; Program P \<turnstile> C \<prec>\<^sup>1 D\<rbrakk> \<Longrightarrow> Program ((C', D', rest) # P) \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> Object

goal (1 subgoal):
 1. Program ((C_, D_, rest_) # P_) \<turnstile> C_ \<prec>\<^sup>1 D_
[PROOF STEP]
by(auto intro: subcls1.intros)
[PROOF STATE]
proof (state)
this:
Program ((C_, D_, rest_) # P_) \<turnstile> C_ \<prec>\<^sup>1 D_

goal (1 subgoal):
 1. \<And>C C' P D D' rest. \<lbrakk>C \<noteq> Object; C \<noteq> C'; subcls1' P C D; Program P \<turnstile> C \<prec>\<^sup>1 D\<rbrakk> \<Longrightarrow> Program ((C', D', rest) # P) \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C C' P D D' rest. \<lbrakk>C \<noteq> Object; C \<noteq> C'; subcls1' P C D; Program P \<turnstile> C \<prec>\<^sup>1 D\<rbrakk> \<Longrightarrow> Program ((C', D', rest) # P) \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
C_ \<noteq> Object
C_ \<noteq> C'_
subcls1' P_ C_ D_
Program P_ \<turnstile> C_ \<prec>\<^sup>1 D_

goal (1 subgoal):
 1. \<And>C C' P D D' rest. \<lbrakk>C \<noteq> Object; C \<noteq> C'; subcls1' P C D; Program P \<turnstile> C \<prec>\<^sup>1 D\<rbrakk> \<Longrightarrow> Program ((C', D', rest) # P) \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> Object
C_ \<noteq> C'_
subcls1' P_ C_ D_
Program P_ \<turnstile> C_ \<prec>\<^sup>1 D_

goal (1 subgoal):
 1. Program ((C'_, D'_, rest_) # P_) \<turnstile> C_ \<prec>\<^sup>1 D_
[PROOF STEP]
by(auto elim!: subcls1.cases intro: subcls1.intros)
[PROOF STATE]
proof (state)
this:
Program ((C'_, D'_, rest_) # P_) \<turnstile> C_ \<prec>\<^sup>1 D_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcls1_eq_subcls1':
  "subcls1 (Program P) = subcls1' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls1 (Program P) = subcls1' P
[PROOF STEP]
by(auto simp add: fun_eq_iff intro: subcls1_into_subcls1' subcls1'_into_subcls1)


[STATEMENT]
lemma subcls''_eq_subcls: "subcls'' P = subcls (Program P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls'' P = subcls (Program P)
[PROOF STEP]
by(simp add: subcls''_def subcls1_eq_subcls1')


[STATEMENT]
lemma subclst_snd_classD:
  assumes "subclst (Program P) C D"
  shows "D \<in> fst ` snd ` set P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<in> fst ` snd ` set P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subclst (Program P) C D

goal (1 subgoal):
 1. D \<in> fst ` snd ` set P
[PROOF STEP]
by(induct)(fastforce elim!: subcls1.cases dest!: map_of_SomeD intro: rev_image_eqI)+


[STATEMENT]
lemma check_acyclicity_code:
  "check_acyclicity mapping P =
   (let _ =
     map (\<lambda>(C, D, _).
       if C = Object then ()
       else
         (case Mapping.lookup mapping D of
            None \<Rightarrow> ()
          | Some Cs \<Rightarrow> if C \<in> Cs then cyclic_class_hierarchy else ()))
       P
    in ())"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_acyclicity mapping P = (let _ = map (\<lambda>(C, D, uu_). if C = Object then () else case Mapping.lookup mapping D of None \<Rightarrow> () | \<lfloor>Cs\<rfloor> \<Rightarrow> if C \<in> Cs then cyclic_class_hierarchy else ()) P in ())
[PROOF STEP]
by simp


[STATEMENT]
lemma tablulate_subcls_code [code]:
  "tabulate_subcls P =
  (let cnames = map fst P;
       cnames' = map (fst \<circ> snd) P;
       mapping = Mapping.tabulate cnames (\<lambda>C. set (C # [D \<leftarrow> cnames'. subcls'' P C D]));
       _ = check_acyclicity mapping P
   in mapping
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_subcls P = (let cnames = map fst P; cnames' = map (fst \<circ> snd) P; mapping = Mapping.tabulate cnames (\<lambda>C. set (C # filter (subcls'' P C) cnames')); _ = check_acyclicity mapping P in mapping)
[PROOF STEP]
apply(auto simp add: tabulate_subcls_def Mapping.tabulate_def fun_eq_iff is_class_def o_def map_of_map2[simplified split_def] Mapping_inject)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> \<lfloor>Collect (subcls (Program P) x)\<rfloor> = map_of (map (\<lambda>x. (fst x, insert (fst x) {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P (fst x) xa})) P) x
 2. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_of (map (\<lambda>x. (fst x, insert (fst x) {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P (fst x) xa})) P) x
[PROOF STEP]
apply(subst map_of_map2[simplified split_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> \<lfloor>Collect (subcls (Program P) x)\<rfloor> = map_option (\<lambda>a. insert x {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P x xa}) (map_of P x)
 2. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_of (map (\<lambda>x. (fst x, insert (fst x) {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P (fst x) xa})) P) x
[PROOF STEP]
apply(auto simp add: fun_eq_iff subcls''_eq_subcls map_of_map_K dest: subclst_snd_classD elim: rtranclp_tranclpE)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_of (map (\<lambda>x. (fst x, insert (fst x) {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P (fst x) xa})) P) x
[PROOF STEP]
apply(subst map_of_map2[simplified split_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_option (\<lambda>a. insert x {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P x xa}) (map_of P x)
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_option (\<lambda>a. insert x {xa \<in> (\<lambda>x. fst (snd x)) ` set P. subcls'' P x xa}) (map_of P x) = None
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_of P x = None
[PROOF STEP]
apply(case_tac "map_of P x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>; map_of P x = None\<rbrakk> \<Longrightarrow> map_of P x = None
 2. \<And>x a. \<lbrakk>\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>; map_of P x = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> map_of P x = None
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Fields'_into_Fields:
  assumes "Fields' P C FDTs"
  shows "Program P \<turnstile> C has_fields FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Program P \<turnstile> C has_fields FDTs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Fields' P C FDTs

goal (1 subgoal):
 1. Program P \<turnstile> C has_fields FDTs
[PROOF STEP]
by induct(auto intro: Fields.intros)


[STATEMENT]
lemma Fields_into_Fields':
  assumes "Program P \<turnstile> C has_fields FDTs"
  shows "Fields' P C FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fields' P C FDTs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Program P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. Fields' P C FDTs
[PROOF STEP]
by induct(auto intro: Fields'.intros)


[STATEMENT]
lemma Fields'_eq_Fields:
  "Fields' P = Fields (Program P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fields' P = Fields (Program P)
[PROOF STEP]
by(auto simp add: fun_eq_iff intro: Fields'_into_Fields Fields_into_Fields')


[STATEMENT]
lemma fields'_code [code]:
  "fields' P C =
  (let FDTs = Fields'_i_i_o P C in if Predicate.holds (FDTs \<bind> (\<lambda>_. Predicate.single ())) then Predicate.the FDTs else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields' P C = (let FDTs = Fields'_i_i_o P C in if Predicate.holds (FDTs \<bind> (\<lambda>_. Predicate.single ())) then Predicate.the FDTs else [])
[PROOF STEP]
by(auto simp add: fields'_def holds_eq Fields'_i_i_o_def intro: Fields'_i_i_oI Predicate.the_eqI[THEN sym])


[STATEMENT]
lemma The_Fields [simp]:
  "P \<turnstile> C has_fields FDTs \<Longrightarrow> The (Fields P C) = FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C has_fields FDTs \<Longrightarrow> The (Fields P C) = FDTs
[PROOF STEP]
by(auto dest: has_fields_fun)