theory Corres_UL

lemma corres_symb_exec_r:
  assumes z: "\<And>rv. corres_underlying sr nf nf' r P (Q' rv) x (y rv)"
  assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>Q'\<rbrace>"
  assumes x: "\<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail P' m"
  shows      "corres_underlying sr nf nf' r P P' x (m >>= (\<lambda>rv. y rv))" apply corres_pre apply (subst gets_bind_ign[symmetric], rule corres_split[OF _ z]) apply (rule corres_noop2) apply (simp add: simpler_gets_def exs_valid_def) apply (erule x) apply (rule no_fail_gets) apply (erule nf) apply (rule gets_wp) apply (rule y) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' 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>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. corres_underlying sr nf nf' ?r'4 ?P4 ?P'4 (gets ?f2) m
 2. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 5. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s. ?P4 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets ?f2 \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s. ?P'4 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. nf' \<Longrightarrow> no_fail ?P4 (gets ?f2)
 4. nf' \<Longrightarrow> no_fail ?P'4 m
 5. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 7. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 8. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>s. ?P'4 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. nf' \<Longrightarrow> no_fail ?P4 (gets ?f2)
 3. nf' \<Longrightarrow> no_fail ?P'4 m
 4. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 6. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 7. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. nf' \<Longrightarrow> no_fail ?P4 (gets ?f2)
 2. nf' \<Longrightarrow> no_fail P' m
 3. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 5. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. nf' \<Longrightarrow> no_fail P' m
 2. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 3. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> m \<lbrace>Q'\<rbrace>
 2. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and P) s
 3. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and P) s
 2. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and P') s' proof (prove)
goal:
No subgoals!