theory SyscallArgs_C

lemma ccorres_cond_both':
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
  shows  "ccorres_underlying sr G r xf arrel axf
          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
          hs
          (if P then a else b) (Cond P' c d)" apply (rule ccorres_guard_imp2) apply (rule ccorres_if_lhs) apply (rule ccorres_cond_true) apply (erule ac) apply (rule ccorres_cond_false) apply (erule bd) apply clarsimp apply (frule abs[rule_format, OF conjI], simp+) done

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