theory ExtraCorres

lemma andM_corres:
  "\<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b';
    \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk>
   \<Longrightarrow> corres_underlying srel nf nf' (=) (A and B) (A' and B') (andM a b) (andM a' b')" unfolding andM_def apply (rule corres_guard_imp) apply (erule (1) ifM_corres[where R=\<top> and R'=\<top>]) apply (wpsimp | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' (=) (A and B) (A' and B') (andM a b) (andM a' b') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' (=) (A and B) (A' and B') (ifM a b (return False)) (ifM a' b' (return False)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' (=) ?Q ?Q' (ifM a b (return False)) (ifM a' b' (return False))
 2. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>; (A and B) s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>; (A' and B') s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (return False) (return False)
 2. \<lbrakk>corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B4\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>
 3. \<lbrakk>corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?C4\<rbrace> a \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> True\<rbrace>
 4. \<lbrakk>corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B'4\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>
 5. \<lbrakk>corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?C'4\<rbrace> a' \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> True\<rbrace>
 6. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>; (A and B) s\<rbrakk> \<Longrightarrow> (A and ?B4 and ?C4) s
 7. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>; (A' and B') s\<rbrakk> \<Longrightarrow> (A' and ?B'4 and ?C'4) s proof (prove)
goal:
No subgoals!