theory Corres_C

lemma ccorres_split_nothrow_novcgE:
  fixes R' :: "cstate set"
  assumes ac: "ccorres_underlying sr \<Gamma>
                   (f' \<currency> r') (liftxf es ef' vf' xf')
                   (f' \<currency> r') (liftxf es ef' vf' xf')
                   P P' [] a c"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk>
                \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')"
  and    err: "\<And>err rv' err'. \<lbrakk> ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk>
                \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf
                     (QE err) (Q'' err rv' err') hs (throwError err) (d' rv')"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>QE\<rbrace>"
  and  novcg: "guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv'))
                                 xf' (\<lambda>rv rv'. {s. ef' rv' = scast EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'})"
  \<comment> \<open>hack\<close>
  and  novcg_err: "\<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es
                              (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>=E (\<lambda>rv. b rv)) (c ;; d)" unfolding bindE_def apply (rule_tac R="case_sum QE Q"
             and R'="\<lambda>rv. {s. s \<in> case_sum QE' QR' rv (xf' s)}" for QE' QR'
           in ccorres_master_split_nohs_UNIV) apply (rule ac) apply (rule ccorres_abstract[OF ceqv]) apply (case_tac rv, simp_all add: lift_def) apply (rule ccorres_abstract[where xf'=es, OF ceqv_refl]) apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (rule_tac err'=rv'a in err) apply assumption+ apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (erule(1) bd) apply (rule hoare_strengthen_post, rule valid[unfolded validE_def]) apply (simp split: sum.split_asm) apply (insert novcg novcg_err) apply (clarsimp simp: guard_is_UNIV_def split: sum.split) done

\<comment> \<open>Unit would be more appropriate, but the record package will rewrite xfdc to ().
   This can happen even when protected by a cong rule, as seen in the following example.
definition
  "xfdc \<equiv> \<lambda>(t :: cstate). ()"
lemma
  "\<And>x b. \<lbrakk>snd x = b\<rbrakk>
   \<Longrightarrow> ccorres_underlying rf_sr \<Gamma>
         (\<lambda>a b. dc a b) (\<lambda>a. xfdc a) dc xfdc
         \<top> UNIV [SKIP] a c"
  supply ccorres_weak_cong[cong]
  apply clarify
  oops\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>=E b) (c;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= Nondet_Monad.lift b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P P' [] a c
 2. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) {s. s \<in> (case rv of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)} hs (Nondet_Monad.lift b rv) d
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. guard_is_UNIV ?r' ?xf' (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) {s. s \<in> (case rv of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)} hs (Nondet_Monad.lift b rv) d
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) ((case rv of Inl a \<Rightarrow> ?QE'3 a | Inr a \<Rightarrow> ?QR'3 a) rv') hs (Nondet_Monad.lift b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a. rv = Inl a \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?QE'3 a rv') hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. rv = Inl a \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'16 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'16 b a (es s)} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'19 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'19 b a (es s) \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'23 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'23 b a (es s) \<inter> \<lbrace>?P24 b a (es s)\<rbrace> \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 2. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> f' a (ef' rv') rv'a
 3. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 4. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 5. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>?P24 b a (es s)\<rbrace> \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P30 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'29 rv' ba) hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'29 rv' b \<inter> \<lbrace>?P30 rv' b\<rbrace>) (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P30 rv' ba; ?P34 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'33 rv' ba) hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'33 rv' b \<inter> \<lbrace>?P34 rv' b\<rbrace> \<inter> \<lbrace>?P30 rv' b\<rbrace>) (xf' s)}) proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 2. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)}) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> QE e s | Inr r \<Rightarrow> Q r s \<Longrightarrow> (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) s
 2. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)}) proof (prove)
goal (1 subgoal):
 1. guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)}) proof (prove)
goal:
No subgoals!