theory Prefix_Refinement

lemma prefix_refinement_env_step:
  assumes env_stable: "env_stable AR R sr iosr Q"
  shows "prefix_refinement sr iosr iosr dc2 (\<lambda>s0 s. s0 = s) (\<lambda>t0 t. t0 = t \<and> Q t0)
    AR R env_step env_step" proof - have P: "\<And>S. {xs. length xs = Suc 0} = (\<lambda>x. [x]) ` UNIV" apply (safe, simp_all) apply (case_tac x, auto) done have st: "rely_stable R sr Q" and est: "env_rely_stable_iosr AR R sr iosr Q"
    and sr: "iosr \<le> sr" using env_stable by (auto simp: env_stable_def) show ?thesis apply (simp add: env_step_def P) apply (clarsimp simp: prefix_refinement_def get_def select_def P
                          bind_def return_def put_def put_trace_elem_def Sigma_def) apply (strengthen default_prefix_refinement_ex_match_iosr_R[where iosr=iosr]) apply (simp add: is_matching_fragment_def rely_cond_def rely_def) apply (simp add: matching_tr_pfx_def matching_tr_def) apply (simp only: UN_extend_simps Int_insert_left2) apply (simp add: is_matching_fragment_def UN_If_distrib) apply (intro conjI allI impI;
        simp add: prefix_closed_def in_fst_snd_image_eq self_closed_def
                  matching_tr_pfx_def matching_tr_def
                  env_closed_def) apply (metis env_rely_stable_iosrD[OF est]) apply clarsimp apply (auto dest: rely_stableD[OF st] predicate2D[OF sr])[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step proof (state)
goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step proof (prove)
goal (1 subgoal):
 1. \<And>S. {xs. length xs = Suc 0} = range (\<lambda>x. [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x. length x = Suc 0 \<Longrightarrow> x \<in> range (\<lambda>x. [x]) proof (prove)
goal:
No subgoals! proof (state)
this:
{xs. length xs = Suc 0} = range (\<lambda>x. [x])

goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step proof (prove)
goal (1 subgoal):
 1. rely_stable R sr Q &&& env_rely_stable_iosr AR R sr iosr Q &&& iosr \<le> sr proof (prove)
using this:
env_stable AR R sr iosr Q

goal (1 subgoal):
 1. rely_stable R sr Q &&& env_rely_stable_iosr AR R sr iosr Q &&& iosr \<le> sr proof (state)
this:
rely_stable R sr Q
env_rely_stable_iosr AR R sr iosr Q
iosr \<le> sr

goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step proof (prove)
goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step proof (prove)
goal (1 subgoal):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R (do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od) (do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>y. rely_cond R t0 [(Env, y)] \<longrightarrow> (\<exists>f. is_matching_fragment sr iosr (\<lambda>_ _. True) [(Env, y)] (Result ((), y)) s AR s f \<and> triv_refinement (\<lambda>s. \<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) f)) \<and> (\<exists>f. is_matching_fragment sr iosr (\<lambda>_ _. True) [] Incomplete s AR s f \<and> triv_refinement (\<lambda>s. \<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) f) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>x. rely_cond R t0 [(Env, x)] \<longrightarrow> is_matching_fragment sr iosr (\<lambda>_ _. True) [(Env, x)] (Result ((), x)) s AR s (rely (\<lambda>s. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV) AR s)) \<and> is_matching_fragment sr iosr (\<lambda>_ _. True) [] Incomplete s AR s (rely (\<lambda>s. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV) AR s) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>x. R t0 x \<longrightarrow> prefix_closed (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. xs = [] \<and> fst ([(Env, x)] ! length xs) = Me) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs sa. matching_tr_pfx sr ((Env, sa) # xs) [(Env, x)] \<and> (\<forall>(ident, s0, s)\<in>trace_steps (rev xs @ [(Env, sa)]) s. ident = Env \<longrightarrow> AR s0 s)) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV \<noteq> {} \<and> (\<forall>(tr, res)\<in>(\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' [(Env, x)]} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. (\<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s) \<and> matching_tr_pfx sr tr [(Env, x)] \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))))) \<and> prefix_closed (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. False) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs sa. matching_tr_pfx sr ((Env, sa) # xs) [] \<and> (\<forall>(ident, s0, s)\<in>trace_steps (rev xs @ [(Env, sa)]) s. ident = Env \<longrightarrow> AR s0 s)) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV \<noteq> {} \<and> (\<forall>(tr, res)\<in>(\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. matching_tr_pfx iosr tr' []} \<times> UNIV \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. (\<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s) \<and> matching_tr_pfx sr tr [] \<and> (tr = [] \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res Incomplete)) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>x. R t0 x \<longrightarrow> prefix_closed (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. xs = [] \<and> fst ([(Env, x)] ! length xs) = Me) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs sa. xs = [] \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev xs @ [(Env, sa)]) [(Env, x)] \<and> (\<forall>(ident, s0, s)\<in>trace_steps (rev xs @ [(Env, sa)]) s. ident = Env \<longrightarrow> AR s0 s)) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV \<noteq> {} \<and> (\<forall>xa\<in>(\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case xa of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> length tr \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev tr) (take (length tr) [(Env, x)]) \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))))) \<and> prefix_closed (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {[]} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. False) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {[]} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs s. False) s (\<lambda>sa. (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {[]} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {[]} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV \<noteq> {} \<and> (\<forall>x\<in>(\<Union>x. {([(Env, x)], Result ((), x)), ([], Incomplete)}) \<inter> {[]} \<times> UNIV \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case x of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> tr = [] \<and> (tr = [] \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res Incomplete)) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>x. R t0 x \<longrightarrow> prefix_closed (\<lambda>sa. \<Union>xa. ((if ([(Env, xa)], Result ((), xa)) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([(Env, xa)], Result ((), xa))} else {}) \<union> ((if ([], Incomplete) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. xs = [] \<and> fst ([(Env, x)] ! length xs) = Me) s (\<lambda>sa. \<Union>xa. ((if ([(Env, xa)], Result ((), xa)) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([(Env, xa)], Result ((), xa))} else {}) \<union> ((if ([], Incomplete) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs sa. xs = [] \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev xs @ [(Env, sa)]) [(Env, x)] \<and> (\<forall>(ident, s0, s)\<in>trace_steps (rev xs @ [(Env, sa)]) s. ident = Env \<longrightarrow> AR s0 s)) s (\<lambda>sa. \<Union>xa. ((if ([(Env, xa)], Result ((), xa)) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([(Env, xa)], Result ((), xa))} else {}) \<union> ((if ([], Incomplete) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>xa. ((if ([(Env, xa)], Result ((), xa)) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([(Env, xa)], Result ((), xa))} else {}) \<union> ((if ([], Incomplete) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<noteq> {} \<and> (\<forall>xa\<in>\<Union>xa. ((if ([(Env, xa)], Result ((), xa)) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([(Env, xa)], Result ((), xa))} else {}) \<union> ((if ([], Incomplete) \<in> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {tr'. length tr' \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> iosr as cs) (rev tr') (take (length tr') [(Env, x)])} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case xa of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> length tr \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev tr) (take (length tr) [(Env, x)]) \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))))) \<and> prefix_closed (\<lambda>sa. \<Union>x. ((if ([(Env, x)], Result ((), x)) \<in> {[]} \<times> UNIV then {([(Env, x)], Result ((), x))} else {}) \<union> ((if ([], Incomplete) \<in> {[]} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {[]} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> self_closed (\<lambda>xs. False) s (\<lambda>sa. \<Union>x. ((if ([(Env, x)], Result ((), x)) \<in> {[]} \<times> UNIV then {([(Env, x)], Result ((), x))} else {}) \<union> ((if ([], Incomplete) \<in> {[]} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {[]} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> env_closed (\<lambda>xs s. False) s (\<lambda>sa. \<Union>x. ((if ([(Env, x)], Result ((), x)) \<in> {[]} \<times> UNIV then {([(Env, x)], Result ((), x))} else {}) \<union> ((if ([], Incomplete) \<in> {[]} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {[]} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<and> (\<Union>x. ((if ([(Env, x)], Result ((), x)) \<in> {[]} \<times> UNIV then {([(Env, x)], Result ((), x))} else {}) \<union> ((if ([], Incomplete) \<in> {[]} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {[]} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV) \<noteq> {} \<and> (\<forall>x\<in>\<Union>x. ((if ([(Env, x)], Result ((), x)) \<in> {[]} \<times> UNIV then {([(Env, x)], Result ((), x))} else {}) \<union> ((if ([], Incomplete) \<in> {[]} \<times> UNIV then {([], Incomplete)} else {}) \<union> {} \<inter> {[]} \<times> UNIV)) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case x of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> tr = [] \<and> (tr = [] \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res Incomplete)) proof (prove)
goal (1 subgoal):
 1. \<And>s t0. \<lbrakk>iosr s t0; sr s t0; Q t0\<rbrakk> \<Longrightarrow> (\<forall>x. R t0 x \<longrightarrow> prefix_closed (\<lambda>sa. insert ([], Incomplete) ((\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV)) \<and> self_closed (\<lambda>xs. xs = [] \<and> fst ([(Env, x)] ! length xs) = Me) s (\<lambda>sa. insert ([], Incomplete) ((\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV)) \<and> env_closed (\<lambda>xs sa. xs = [] \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev xs @ [(Env, sa)]) [(Env, x)] \<and> (\<forall>x\<in>trace_steps (rev xs @ [(Env, sa)]) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s)) s (\<lambda>sa. insert ([], Incomplete) ((\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV)) \<and> (\<forall>(tr, res)\<in>(\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. (\<forall>(ident, s0, s)\<in>trace_steps (rev tr) s. ident = Env \<longrightarrow> AR s0 s) \<and> length tr \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev tr) (take (length tr) [(Env, x)]) \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))))) \<and> prefix_closed (\<lambda>s. {([], Incomplete)}) \<and> self_closed (\<lambda>xs. False) s (\<lambda>s. {([], Incomplete)}) \<and> env_closed (\<lambda>xs s. False) s (\<lambda>s. {([], Incomplete)}) proof (prove)
goal (2 subgoals):
 1. \<And>s t0 x. \<lbrakk>iosr s t0; sr s t0; Q t0; R t0 x\<rbrakk> \<Longrightarrow> \<forall>s'. sr s' x \<and> AR s s' \<longrightarrow> iosr s' x
 2. \<And>s t0 x. \<lbrakk>iosr s t0; sr s t0; Q t0; R t0 x\<rbrakk> \<Longrightarrow> \<forall>xa\<in>(\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case xa of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> length tr \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev tr) (take (length tr) [(Env, x)]) \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))) proof (prove)
goal (1 subgoal):
 1. \<And>s t0 x. \<lbrakk>iosr s t0; sr s t0; Q t0; R t0 x\<rbrakk> \<Longrightarrow> \<forall>xa\<in>(\<Union>x\<in>{xa. iosr xa x}. {([(Env, x)], Result ((), x))}) \<inter> {tr. \<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s} \<times> UNIV. case xa of (tr, res) \<Rightarrow> (\<forall>x\<in>trace_steps (rev tr) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> AR s0 s) \<and> length tr \<le> Suc 0 \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev tr) (take (length tr) [(Env, x)]) \<and> (tr = [] \<longrightarrow> res = Incomplete) \<and> (length tr = Suc 0 \<longrightarrow> rel_tmres iosr (\<lambda>_ _. True) res (Result ((), x))) proof (prove)
goal (1 subgoal):
 1. \<And>s t0 x xa. \<lbrakk>iosr s t0; sr s t0; Q t0; R t0 x; iosr xa x; AR s xa\<rbrakk> \<Longrightarrow> sr xa x proof (prove)
goal:
No subgoals! proof (state)
this:
prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step

goal:
No subgoals!