theory Prefix_Refinement

lemma prefix_refinement_env_steps:
  "env_stable AR R sr iosr Q
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True)
        (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_steps env_steps" apply (simp add: env_steps_repeat) apply (rule prefix_refinement_repeat) apply (erule prefix_refinement_env_step) apply (simp add: env_step_def) apply (wp put_trace_elem_twp) apply (clarsimp simp: guar_cond_def) apply (simp add: env_step_def) apply (wp put_trace_elem_twp) apply simp apply (clarsimp simp: guar_cond_def length_Suc_conv) apply (clarsimp simp: rely_cond_def env_stable_def) apply (blast dest: rely_stableD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_steps env_steps proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R (repeat env_step) (repeat env_step) proof (prove)
goal (3 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> env_step -, \<lbrace>\<lambda>_. (=)\<rbrace>
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. (t0 = t \<and> Q t0) \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> env_step -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (2 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> env_step -, \<lbrace>\<lambda>_. (=)\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. (t0 = t \<and> Q t0) \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> env_step -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (2 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od -, \<lbrace>\<lambda>_. (=)\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. (t0 = t \<and> Q t0) \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> env_step -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>env_stable AR R sr iosr Q; s0 = s\<rbrakk> \<Longrightarrow> \<forall>x\<in>UNIV. (\<forall>n. rely_cond AR s0 (drop n [(Env, x)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Env, x)])) \<and> (rely_cond AR s0 [(Env, x)] \<longrightarrow> snd (Env, x) = x)
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. (t0 = t \<and> Q t0) \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> env_step -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. (t0 = t \<and> Q t0) \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> env_step -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>\<lambda>t0 t. t0 = t \<and> Q t0 \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od -, \<lbrace>\<lambda>_ t0 t. t0 = t \<and> Q t0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>env_stable AR R sr iosr Q; s0 = s \<and> Q s0 \<and> (\<exists>s0a. sr s0a s0) \<and> (\<exists>sa. iosr sa s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>UNIV. (\<forall>n. rely_cond R s0 (drop n [(Env, x)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Env, x)])) \<and> (rely_cond R s0 [(Env, x)] \<longrightarrow> snd (Env, x) = x \<and> Q (snd (Env, x))) proof (prove)
goal (1 subgoal):
 1. \<And>s0. \<lbrakk>env_stable AR R sr iosr Q; Q s0 \<and> (\<exists>s0a. sr s0a s0) \<and> (\<exists>s. iosr s s0)\<rbrakk> \<Longrightarrow> \<forall>x. rely_cond R s0 [(Env, x)] \<longrightarrow> Q x proof (prove)
goal (1 subgoal):
 1. \<And>s0 x s0a s. \<lbrakk>env_stable AR R sr iosr Q; Q s0; sr s0a s0; iosr s s0; rely_cond R s0 [(Env, x)]\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal (1 subgoal):
 1. \<And>s0 x s0a s. \<lbrakk>Q s0; sr s0a s0; iosr s s0; R s0 x; rely_stable R sr Q; env_rely_stable_iosr AR R sr iosr Q; iosr \<le> sr\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal:
No subgoals!