theory VSpace_R

lemma corres_split_strengthen_ftE:
  "\<lbrakk> corres (ftr \<oplus> r') P P' f j;
      \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv');
      \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,-; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>,- \<rbrakk>
    \<Longrightarrow> corres (dc \<oplus> r) (P and Q) (P' and Q') (f >>=E (\<lambda>rv. g rv)) (j >>=E (\<lambda>rv'. k rv'))" apply (rule_tac r'=r' in corres_splitEE) apply (erule corres_rel_imp) apply (case_tac x, auto)[1] apply (rule corres_rel_imp, assumption) apply (case_tac x, auto)[1] apply (simp add: validE_R_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> corres (dc \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (j >>=E k) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> corres (dc \<oplus> r') P P' f j
 2. \<And>rv rv'. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -; r' rv rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> r) (?R rv) (?R' rv') (g rv) (k rv')
 3. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>?R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> j \<lbrace>?R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>\<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -; (ftr \<oplus> r') x y\<rbrakk> \<Longrightarrow> (dc \<oplus> r') x y
 2. \<And>rv rv'. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -; r' rv rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> r) (?R rv) (?R' rv') (g rv) (k rv')
 3. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>?R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> j \<lbrace>?R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -; r' rv rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> r) (?R rv) (?R' rv') (g rv) (k rv')
 2. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>?R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> j \<lbrace>?R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' x y. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -; r' rv rv'; (ftr' \<oplus> r) x y\<rbrakk> \<Longrightarrow> (dc \<oplus> r) x y
 2. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>corres (ftr \<oplus> r') P P' f j; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres (ftr' \<oplus> r) (R rv) (R' rv') (g rv) (k rv'); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!