theory Corres_UL

lemma corres_symb_exec_r_conj:
  assumes z: "\<And>rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)"
  assumes y: "\<lbrace>Q'\<rbrace> m \<lbrace>R'\<rbrace>"
  assumes x: "\<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>"
  assumes nf: "\<And>s. nf' \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') m"
  shows      "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\<lambda>rv. y rv))" proof - have P: "corres_underlying sr nf nf' dc \<top> P' (return undefined) m" apply (rule corres_noop) apply (simp add: x) apply (erule nf) done show ?thesis apply corres_pre apply (subst return_bind[symmetric],
             rule corres_split [OF P]) apply (rule z) apply wp apply (rule y) apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q (P' and Q') x (m >>= y) proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q (P' and Q') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc (\<lambda>_. True) P' (return undefined) m proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> dc undefined rv\<rbrace>
 2. \<And>s. \<lbrakk>True; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') m proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>True; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') m proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' dc (\<lambda>_. True) P' (return undefined) m

goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q (P' and Q') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q (P' and Q') x (m >>= y) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' x (m >>= y)
 2. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R4 rv) (?R'4 rv') x (y rv')
 2. \<lbrace>?Q4\<rbrace> return undefined \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> m \<lbrace>?R'4\<rbrace>
 4. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> return undefined \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> m \<lbrace>R'\<rbrace>
 3. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> m \<lbrace>R'\<rbrace>
 2. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and Q) s
 3. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and Q) s
 2. \<And>s s'. \<lbrakk>Q s; (P' and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and Q') s' proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' r Q (P' and Q') x (m >>= y)

goal:
No subgoals!