theory Corres_UL

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>P\<rbrace> m \<lbrace>Q\<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail P m"
  shows      "corres_underlying sr nf nf' r P P' (m >>= (\<lambda>rv. x rv)) y" apply corres_pre apply (subst gets_bind_ign[symmetric], rule corres_split[OF _ z]) apply (rule corres_noop2) apply (erule x) apply (rule gets_wp) apply (erule nf) apply (rule no_fail_gets) 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 P' (m >>= x) y proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' (m >>= x) 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 m (gets ?f2)
 2. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<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> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s. ?P'4 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets ?f2 \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. nf' \<Longrightarrow> no_fail ?P4 m
 4. nf' \<Longrightarrow> no_fail ?P'4 (gets ?f2)
 5. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<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> gets ?f2 \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. nf' \<Longrightarrow> no_fail P m
 3. nf' \<Longrightarrow> no_fail ?P'4 (gets ?f2)
 4. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<rbrace>
 6. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P 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 P m
 2. nf' \<Longrightarrow> no_fail ?P'4 (gets ?f2)
 3. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<rbrace>
 5. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 6. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. nf' \<Longrightarrow> no_fail ?P'4 (gets ?f2)
 2. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P 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 (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> m \<lbrace>Q\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<rbrace>
 3. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 4. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s' proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> gets ?f2 \<lbrace>\<lambda>x. P'\<rbrace>
 2. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and P) s
 3. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and P) s
 2. \<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and P') s' proof (prove)
goal:
No subgoals!