theory Move_R

lemma corres_symb_exec_l':
  assumes z: "\<And>rv. corres_underlying sr nf nf' r (Q' rv) P' (x rv) y"
  assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes y: "\<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>"
  shows      "corres_underlying sr nf nf' r (P and Q) P' (m >>= (\<lambda>rv. x rv)) y" apply (rule corres_guard_imp) apply (subst gets_bind_ign[symmetric], rule corres_split) apply (rule corres_noop3) apply (erule x) apply (rule gets_wp) apply (rule no_fail_gets) apply (rule z) apply (rule y) apply (rule gets_wp) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) P' (m >>= x) y proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' (m >>= x) y
 2. \<And>s. (P and Q) s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres_underlying sr nf nf' ?r'7 ?P7 ?P'7 m (gets ?f5)
 2. \<And>rv xa. ?r'7 rv xa \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 xa) (x rv) y
 3. \<lbrace>?Q7\<rbrace> m \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>?R'7\<rbrace>
 5. \<And>s. (P and Q) s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. P' s \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>s s'. \<lbrakk>?P7 s; ?P'7 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s s'. \<lbrakk>?P7 s; ?P'7 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> gets ?f5 \<lbrace>\<lambda>r. (=) s'\<rbrace>
 3. nf' \<Longrightarrow> no_fail ?P'7 (gets ?f5)
 4. \<And>rv xa. dc rv xa \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 xa) (x rv) y
 5. \<lbrace>?Q7\<rbrace> m \<lbrace>?R7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>?R'7\<rbrace>
 7. \<And>s. (P and Q) s \<Longrightarrow> (?P7 and ?Q7) s
 8. \<And>s. P' s \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>P s; ?P'7 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> gets ?f5 \<lbrace>\<lambda>r. (=) s'\<rbrace>
 2. nf' \<Longrightarrow> no_fail ?P'7 (gets ?f5)
 3. \<And>rv xa. dc rv xa \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 xa) (x rv) y
 4. \<lbrace>?Q7\<rbrace> m \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>?R'7\<rbrace>
 6. \<And>s. (P and Q) s \<Longrightarrow> (P and ?Q7) s
 7. \<And>s. P' s \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. nf' \<Longrightarrow> no_fail ?P'7 (gets ?f5)
 2. \<And>rv xa. dc rv xa \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 xa) (x rv) y
 3. \<lbrace>?Q7\<rbrace> m \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>?R'7\<rbrace>
 5. \<And>s. (P and Q) s \<Longrightarrow> (P and ?Q7) s
 6. \<And>s. P' s \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>rv xa. dc rv xa \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 xa) (x rv) y
 2. \<lbrace>?Q7\<rbrace> m \<lbrace>?R7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>?R'7\<rbrace>
 4. \<And>s. (P and Q) s \<Longrightarrow> (P and ?Q7) s
 5. \<And>s. P' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q7\<rbrace> m \<lbrace>Q'\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>\<lambda>x. P'\<rbrace>
 3. \<And>s. (P and Q) s \<Longrightarrow> (P and ?Q7) s
 4. \<And>s. P' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'7) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'7\<rbrace> gets ?f5 \<lbrace>\<lambda>x. P'\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 3. \<And>s. P' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'7) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 2. \<And>s. P' s \<Longrightarrow> ((\<lambda>_. True) and P') s proof (prove)
goal:
No subgoals!