theory Corres_UL

lemma corres_split:
  assumes x: "corres_underlying sr nf nf' r' P P' a c"
  assumes y: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')"
  assumes    "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>"
  shows      "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" using assms apply - apply (rule corres_underlying_split) apply (rule corres_guard_imp, rule x, simp_all) apply (erule y) apply (rule hoare_weaken_pre, assumption) apply simp apply (rule hoare_weaken_pre, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
using this:
corres_underlying sr nf nf' r' P P' a c
r' ?rv ?rv' \<Longrightarrow> corres_underlying sr nf nf' r (R ?rv) (R' ?rv') (b ?rv) (d ?rv')
\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>
\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' ?r'5 (P and Q) (P' and Q') a c
 2. \<And>rv rv'. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; ?r'5 rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (?Q5 rv) (?Q'5 rv') (b rv) (d rv')
 3. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> a \<lbrace>?Q5\<rbrace>
 4. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and Q'\<rbrace> c \<lbrace>?Q'5\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; r' rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (?Q5 rv) (?Q'5 rv') (b rv) (d rv')
 2. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> a \<lbrace>?Q5\<rbrace>
 3. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and Q'\<rbrace> c \<lbrace>?Q'5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> a \<lbrace>R\<rbrace>
 2. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and Q'\<rbrace> c \<lbrace>R'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; (P and Q) s\<rbrakk> \<Longrightarrow> Q s
 2. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and Q'\<rbrace> c \<lbrace>R'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and Q'\<rbrace> c \<lbrace>R'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; (P' and Q') s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!