theory Prefix_Refinement

theorem prefix_refinement_validI:
  "prefix_refinement sr isr osr rvr prP' prP R' R f g
    \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R'\<rbrace>
        f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>,\<lbrace>\<lambda>rv
                s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>
    \<Longrightarrow> \<forall>t0 t. P t0 t \<longrightarrow> (\<exists>s0 s. P' s0 s \<and> prP' s0 s \<and> prP t0 t \<and> isr s t \<and> sr s0 t0)
    \<Longrightarrow> \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t)
    \<Longrightarrow> prefix_closed g
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (subst validI_def, clarsimp simp: rely_def) apply (drule spec2, drule(1) mp, clarsimp) apply (drule(6) prefix_refinement_rely_cond_trD[where R'=R', simplified]) apply blast apply clarsimp apply (rule conjI) apply (frule(3) validI_GD) apply (simp add: guar_cond_def matching_tr_def) apply (erule_tac R'="\<lambda>cs s. sr s cs" in list_all2_all_trace_steps) apply (clarsimp simp: list_all2_conv_all_nth split_def) apply simp apply clarsimp apply clarsimp apply (erule tmres.rel_cases; clarsimp) apply (drule(1) validI_rvD, simp add: rely_def) apply simp apply (case_tac tr; clarsimp simp: list_all2_Cons2 matching_tr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr rvr prP' prP R' R f g; \<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>t0 t. P t0 t \<longrightarrow> (\<exists>s0 s. P' s0 s \<and> prP' s0 s \<and> prP t0 t \<and> isr s t \<and> sr s0 t0); \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_refinement sr isr osr rvr prP' prP R' R f g; \<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>t0 t. P t0 t \<longrightarrow> (\<exists>s0 s. P' s0 s \<and> prP' s0 s \<and> prP t0 t \<and> isr s t \<and> sr s0 t0); \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res s0a sa. \<lbrakk>prefix_refinement sr isr osr rvr prP' prP R' R f g; \<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res s0a sa. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0\<rbrakk> \<Longrightarrow> \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> R' s s'))
 2. \<And>s0 s tr res s0a sa. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; \<exists>x\<in>f sa. case x of (atr, ares) \<Rightarrow> matching_tr sr atr tr \<and> rel_tmres osr rvr ares res \<and> rely_cond R' s0a atr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res s0a sa. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; \<exists>x\<in>f sa. case x of (atr, ares) \<Rightarrow> matching_tr sr atr tr \<and> rel_tmres osr rvr ares res \<and> rely_cond R' s0a atr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> guar_cond G s0 tr
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a; guar_cond (\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs) s0a a\<rbrakk> \<Longrightarrow> guar_cond G s0 tr
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a; \<forall>x\<in>trace_steps (rev a) s0a. case x of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> (\<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs)\<rbrakk> \<Longrightarrow> \<forall>x\<in>trace_steps (rev tr) s0. case x of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (4 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr cs as) tr a
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> sr s0a s0
 3. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>idn as1 as2 cs1 cs2. sr cs1 as1 \<longrightarrow> sr cs2 as2 \<longrightarrow> (case (idn, cs1, cs2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> (\<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs)) \<longrightarrow> (case (idn, as1, as2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s)
 4. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (3 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> sr s0a s0
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>idn as1 as2 cs1 cs2. sr cs1 as1 \<longrightarrow> sr cs2 as2 \<longrightarrow> (case (idn, cs1, cs2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> (\<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs)) \<longrightarrow> (case (idn, as1, as2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s)
 3. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>idn as1 as2 cs1 cs2. sr cs1 as1 \<longrightarrow> sr cs2 as2 \<longrightarrow> (case (idn, cs1, cs2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> (\<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs)) \<longrightarrow> (case (idn, as1, as2) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s)
 2. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res s0a sa a b. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, res) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b res; rely_cond R' s0a a\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr s0a sa a b rv s'. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, Result (rv, s')) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, b) \<in> f sa; matching_tr sr a tr; rel_tmres osr rvr b (Result (rv, s')); rely_cond R' s0a a\<rbrakk> \<Longrightarrow> Q rv (last_st_tr tr s0) s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr s0a sa a aa ba ab bb. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. sr s0 cs0 \<and> sr s cs \<longrightarrow> G cs0 cs\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. sr s0 cs0 \<and> osr s cs \<and> rvr rv rv' \<longrightarrow> Q rv' cs0 cs\<rbrace>; \<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, Result (ab, bb)) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, Result (aa, ba)) \<in> f sa; matching_tr sr a tr; rely_cond R' s0a a; rvr aa ab; osr ba bb\<rbrakk> \<Longrightarrow> Q ab (last_st_tr tr s0) bb proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr s0a sa a aa ba ab bb. \<lbrakk>\<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, Result (ab, bb)) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, Result (aa, ba)) \<in> f sa; matching_tr sr a tr; rely_cond R' s0a a; rvr aa ab; osr ba bb\<rbrakk> \<Longrightarrow> rely_cond R' s0a a
 2. \<And>s0 s tr s0a sa a aa ba ab bb. \<lbrakk>\<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, Result (ab, bb)) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, Result (aa, ba)) \<in> f sa; matching_tr sr a tr; rely_cond R' s0a a; rvr aa ab; osr ba bb; \<forall>rv' cs0 cs. sr (last_st_tr a s0a) cs0 \<and> osr ba cs \<and> rvr aa rv' \<longrightarrow> Q rv' cs0 cs\<rbrakk> \<Longrightarrow> Q ab (last_st_tr tr s0) bb proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr s0a sa a aa ba ab bb. \<lbrakk>\<forall>s0 t0 t. sr s0 t0 \<and> R t0 t \<longrightarrow> (\<exists>s. R' s0 s \<and> sr s t); prefix_closed g; P s0 s; (tr, Result (ab, bb)) \<in> g s; rely_cond R s0 tr; P' s0a sa; prP' s0a sa; prP s0 s; isr sa s; sr s0a s0; (a, Result (aa, ba)) \<in> f sa; matching_tr sr a tr; rely_cond R' s0a a; rvr aa ab; osr ba bb; \<forall>rv' cs0 cs. sr (last_st_tr a s0a) cs0 \<and> osr ba cs \<and> rvr aa rv' \<longrightarrow> Q rv' cs0 cs\<rbrakk> \<Longrightarrow> Q ab (last_st_tr tr s0) bb proof (prove)
goal:
No subgoals!