theory Prefix_Refinement

lemma prefix_refinement_env_n_steps:
  assumes env_stable: "env_stable AR R sr iosr Q"
  shows "prefix_refinement sr iosr iosr (\<lambda>_ _. True)
        (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R (env_n_steps n) (env_n_steps n)" apply (rule prefix_refinement_repeat_n) apply (rule prefix_refinement_env_step[OF env_stable]) 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 (cut_tac env_stable[unfolded env_stable_def]) apply (clarsimp simp: rely_cond_def) apply (drule(3) rely_stableD) apply simp done

(* 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_n_steps n) (env_n_steps n) proof (prove)
goal (3 subgoals):
 1. prefix_refinement sr iosr iosr (\<lambda>_ _. True) (=) (\<lambda>t0 t. t0 = t \<and> Q t0) AR R env_step env_step
 2. \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> env_step -, \<lbrace>\<lambda>_. (=)\<rbrace>
 3. \<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. \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> env_step -, \<lbrace>\<lambda>_. (=)\<rbrace>
 2. \<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. \<lbrace>(=)\<rbrace>, \<lbrace>AR\<rbrace> do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od -, \<lbrace>\<lambda>_. (=)\<rbrace>
 2. \<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. s0 = s \<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. \<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. \<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. \<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. s0 = s \<and> Q s0 \<and> (\<exists>s0a. sr s0a s0) \<and> (\<exists>sa. iosr sa s) \<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. Q s0 \<and> (\<exists>s0a. sr s0a s0) \<and> (\<exists>s. iosr s s0) \<Longrightarrow> \<forall>x. rely_cond R s0 [(Env, x)] \<longrightarrow> Q x proof (prove)
goal (1 subgoal):
 1. \<And>s0 x s0a s. \<lbrakk>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; rely_cond R s0 [(Env, x)]; rely_stable R sr Q \<and> env_rely_stable_iosr AR R sr iosr Q \<and> iosr \<le> sr\<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 (1 subgoal):
 1. \<And>s0 x s0a s. \<lbrakk>Q s0; sr s0a s0; iosr s s0; R s0 x; env_rely_stable_iosr AR R sr iosr Q; iosr \<le> sr; Q x \<and> (\<exists>s'. sr s' x)\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal:
No subgoals!