theory CCorresLemmas

lemma ccorres_if_cond_throws2:
  fixes e :: 'e
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> (\<not> P) = (s' \<in> P')"
  and     ac: "\<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R R' (SKIP # hs) a c"
  and     bd: "P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf U U' (SKIP # hs) b d"
  and cthrows: "\<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> PT' c {}, UNIV" \<comment> \<open>c always throws\<close>
  shows  "ccorres_underlying sr \<Gamma> r xf arrel axf
          (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s))
          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
          (SKIP # hs)
          (if P then b else a) (Cond P' c SKIP ;; d)" apply (subst if_swap) apply (rule ccorres_guard_imp2) apply (rule ccorres_if_cond_throws [OF abs ac bd cthrows]) apply assumption apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then b else a) (Cond P' c SKIP;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if \<not> P then a else b) (Cond P' c SKIP;;
d) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' (SKIP # hs) (if \<not> P then a else b) (Cond P' c SKIP;;
d)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<not> P \<Longrightarrow> \<not> P
 2. \<not> \<not> P \<Longrightarrow> P
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. \<not> \<not> P \<longrightarrow> U s)) s \<and> s' \<in> {s'. Q' s'} \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')} proof (prove)
goal (2 subgoals):
 1. \<not> \<not> P \<Longrightarrow> P
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. \<not> \<not> P \<longrightarrow> U s)) s \<and> s' \<in> {s'. Q' s'} \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. P \<longrightarrow> U s)) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> (Q and (\<lambda>s. \<not> P \<longrightarrow> R s) and (\<lambda>s. \<not> \<not> P \<longrightarrow> U s)) s \<and> s' \<in> {s'. Q' s'} \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')} proof (prove)
goal:
No subgoals!