theory CCorresLemmas

lemma ccorres_cond2':
  "\<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P');
     ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c;
  ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'\<rbrakk>
  \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf  (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. P \<longrightarrow> Pf s))
  {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} hs (if P then b else a)
  (Cond P' c c')" apply (subst if_flip [symmetric]) apply (rule ccorres_guard_imp2) apply (erule (2) ccorres_cond2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P'); ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c; ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. P \<longrightarrow> Pf s)) {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} hs (if P then b else a) (Cond P' c c') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P'); ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c; ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. P \<longrightarrow> Pf s)) {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} hs (if \<not> P then a else b) (Cond P' c c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P'); ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c; ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf ?Q ?Q' hs (if \<not> P then a else b) (Cond P' c c')
 2. \<And>s s'. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P'); ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c; ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'; (s, s') \<in> sr; (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. P \<longrightarrow> Pf s)) s; s' \<in> {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> (\<not> P) = (s' \<in> P'); ccorres_underlying sr \<Gamma> r xf ar axf Pt Rt hs a c; ccorres_underlying sr \<Gamma> r xf ar axf Pf Rf hs b c'; (s, s') \<in> sr; (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. P \<longrightarrow> Pf s)) s; s' \<in> {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)}\<rbrakk> \<Longrightarrow> (R and (\<lambda>s. \<not> P \<longrightarrow> Pt s) and (\<lambda>s. \<not> \<not> P \<longrightarrow> Pf s)) s \<and> s' \<in> {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} proof (prove)
goal:
No subgoals!