theory Move_R

lemma corres_symb_exec_r':
  assumes z: "\<And>rv. corres_underlying sr nf nf' r P (P'' rv) x (y rv)"
  assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>P''\<rbrace>"
  assumes x: "\<And>s. Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail R' m"
  shows      "corres_underlying sr nf nf' r P (P' and Q' and R') x (m >>= (\<lambda>rv. y rv))" apply (rule corres_guard_imp) apply (subst gets_bind_ign[symmetric], rule corres_split) apply (rule_tac P'="a' and a''" for a' a'' in corres_noop3) apply (simp add: simpler_gets_def exs_valid_def) apply clarsimp apply (erule x) apply (rule no_fail_pre) apply (erule nf) apply clarsimp apply assumption apply (rule z) 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' and Q' and R') x (m >>= y) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' x (m >>= y)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and Q' and R') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres_underlying sr nf nf' ?r'7 ?P7 ?P'7 (gets ?f5) m
 2. \<And>xa rv'. ?r'7 xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 3. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. (P' and Q' and R') s \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>s s'. \<lbrakk>?P7 s; (?a'21 and ?a''21) s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets ?f5 \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s s'. \<lbrakk>?P7 s; (?a'21 and ?a''21) s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> m \<lbrace>\<lambda>r. (=) s'\<rbrace>
 3. nf' \<Longrightarrow> no_fail (?a'21 and ?a''21) m
 4. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 5. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 7. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 8. \<And>s. (P' and Q' and R') s \<Longrightarrow> (?a'21 and ?a''21 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>?P7 s; (?a'21 and ?a''21) s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> m \<lbrace>\<lambda>r. (=) s'\<rbrace>
 2. nf' \<Longrightarrow> no_fail (?a'21 and ?a''21) m
 3. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 4. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 7. \<And>s. (P' and Q' and R') s \<Longrightarrow> (?a'21 and ?a''21 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>?P7 s; (s, s') \<in> sr; ?a'21 s'; ?a''21 s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> m \<lbrace>\<lambda>r. (=) s'\<rbrace>
 2. nf' \<Longrightarrow> no_fail (?a'21 and ?a''21) m
 3. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 4. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 7. \<And>s. (P' and Q' and R') s \<Longrightarrow> (?a'21 and ?a''21 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. nf' \<Longrightarrow> no_fail (Q' and ?a''21) m
 2. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 3. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and ?a''21 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. nf' \<Longrightarrow> no_fail ?P35 m
 2. \<And>s. \<lbrakk>nf'; (Q' and ?a''21) s\<rbrakk> \<Longrightarrow> ?P35 s
 3. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 4. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 7. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and ?a''21 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>nf'; (Q' and ?a''21) s\<rbrakk> \<Longrightarrow> R' s
 2. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 3. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and ?a''21 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>nf'; Q' s; ?a''21 s\<rbrakk> \<Longrightarrow> R' s
 2. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 3. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and ?a''21 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>xa rv'. dc xa rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 xa) (?R'7 rv') x (y rv')
 2. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>?R7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> m \<lbrace>?R'7\<rbrace>
 4. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 5. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and R' and ?Q'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q7\<rbrace> gets ?f5 \<lbrace>\<lambda>x. P\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> m \<lbrace>P''\<rbrace>
 3. \<And>s. P s \<Longrightarrow> (?P7 and ?Q7) s
 4. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and R' and ?Q'7) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'7\<rbrace> m \<lbrace>P''\<rbrace>
 2. \<And>s. P s \<Longrightarrow> (?P7 and P) s
 3. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and R' and ?Q'7) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (?P7 and P) s
 2. \<And>s. (P' and Q' and R') s \<Longrightarrow> (Q' and R' and P') s proof (prove)
goal:
No subgoals!