theory Ctac

lemma mapME_x_simpl_sequence_fun_related:
  "\<lbrakk> ys = map yf xs;
    \<And>n x. x \<in> set xs \<Longrightarrow>
        ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf
            (P and F n (n < length xs) x) Q hs
                            (f x) (f' (yf x));
    \<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow>
        (\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>x \<in> set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f' (yf x)) Q,UNIV;
    \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) (Suc n < length xs) (xs ! Suc n)\<rbrace>, -
    \<rbrakk>
    \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc
                  (inl_rrel arrel) axf
                  (P and F 0 (xs \<noteq> []) (xs ! 0)) Q hs
          (mapME_x f xs)
          (simpl_sequence f' ys)" apply (simp add: mapME_x_sequenceE liftME_def[symmetric]
    liftME_liftM) apply (rule ccorres_rel_imp2, rule ccorres_guard_imp2,
    rule sequenceE_simpl_sequence_nth_corres[where r'=dc and xf'=xfdc
      and P=P and F="\<lambda>i. F i (i < length xs) (xs ! i)" and Q=Q and arrel=arrel and axf=axf];
        clarsimp elim!: inl_inrE) apply (erule_tac x="length zs" in meta_allE
       | erule_tac x="xs ! length zs" in meta_allE)+ apply (simp add: dc_def cong: ccorres_all_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys = map yf xs; \<And>n x. x \<in> set xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf (P and F n (n < length xs) x) Q hs (f x) (f' (yf x)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f' (yf x) Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) (Suc n < length xs) (xs ! Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf (P and F 0 (xs \<noteq> []) (xs ! 0)) Q hs (mapME_x f xs) (simpl_sequence f' ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys = map yf xs; \<And>n x. x \<in> set xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf (P and F n (n < length xs) x) Q hs (f x) (f' (yf x)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f' (yf x) Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) True (xs ! Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc \<circ> case_sum Inl (Inr \<circ> (\<lambda>_. ()))) xfdc (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (\<lambda>_. ()))) axf (P and F 0 (xs \<noteq> []) (xs ! 0)) Q hs (sequenceE (map f xs)) (simpl_sequence f' (map yf xs)) proof (prove)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>ys = map yf xs; \<And>n x. x \<in> set xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf (P and F n (n < length xs) x) Q hs (f x) (f' (yf x)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f' (yf x) Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) True (xs ! Suc n)\<rbrace>, -; length zs < length xs\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. dc ([] @ zs @ [rv]))) xfdc (inl_rrel arrel) axf (P and F (length zs) True (xs ! length zs)) Q hs (f (xs ! length zs)) (f' (yf (xs ! length zs))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>ys = map yf xs; \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f' (yf x) Q,UNIV; length zs < length xs; Suc (length zs) < length xs \<Longrightarrow> \<lbrace>P and F (length zs) True (xs ! length zs)\<rbrace> f (xs ! length zs) \<lbrace>\<lambda>_. P and F (Suc (length zs)) True (xs ! Suc (length zs))\<rbrace>, -; xs ! length zs \<in> set xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf (P and F (length zs) (length zs < length xs) (xs ! length zs)) Q hs (f (xs ! length zs)) (f' (yf (xs ! length zs)))\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. dc ([] @ zs @ [rv]))) xfdc (inl_rrel arrel) axf (P and F (length zs) True (xs ! length zs)) Q hs (f (xs ! length zs)) (f' (yf (xs ! length zs))) proof (prove)
goal:
No subgoals!