ExtraCorres.thy

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory ExtraCorres
imports Corres_UL DetWPLib
begin

(* FIXME: the S in this rule is mainly to make the induction work, we don't actually need it in
   application. This means, this form should be hidden and the main form should be resolving the
   last assumption with order_refl. *)

(* The lemma looks weaker than in it could be -- the guards P and P' are not allowed to depend on
   list elements. This is fine, because P/P' are a loop invariants that need to be supplied
   manually anyway, and we want these to be true for all loop iterations. An instance such as
   "\<lambda>s. \<forall>x \<in> set xs. P x s" is possible and covers the cases the (not really) stronger formulation
   would cover. *)
lemma corres_mapM:
  assumes x: "r [] []"
  assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
  assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)"
  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
  shows      "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow>
                   corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys)"
proof (induct xs ys rule: list_induct2)
  case Nil
  show ?case
    by (simp add: mapM_def sequence_def x)
next
  case (Cons a as b bs)
  from Cons have P: "(a, b) \<in> S"
    by simp
  from Cons have Q: "corres_underlying R nf nf' r P P' (mapM f as) (mapM f' bs)"
    by simp
  show ?case
    apply (simp add: mapM_Cons)
    apply (rule corres_guard_imp)
      apply (rule corres_split[OF z[OF P] _ w[OF P]])
      apply (rule corres_underlying_split[OF Q])
        apply (rule corres_trivial, simp add: y)
       apply (wp | simp)+
    done
qed

(* list_all2 has _much_ nicer simps than set (zip _ _).
    See KernelInit_R: corres_init_objs for an example *)
lemma corres_mapM_list_all2:
  assumes rn: "r [] []"
  and     rc: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
  and   corr: "\<And>x xs y ys. \<lbrakk> S x y; list_all2 S xs ys \<rbrakk>
               \<Longrightarrow> corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)"
  and     ha: "\<And>x xs y. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace>Q  (x # xs)\<rbrace> f x \<lbrace>\<lambda>r. Q xs\<rbrace>"
  and     hc: "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace>Q' (y # ys) \<rbrace> f' y \<lbrace>\<lambda>r. Q' ys\<rbrace>"
  and   lall: "list_all2 S as cs"
  shows       "corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs)"
  using lall
proof (induct rule: list_all2_induct_suffixeq)
  case Nil
  thus ?case
    unfolding mapM_def sequence_def by (auto intro: rn)
next
  case  (Cons x xs y ys)

  have corr': "corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)"
  proof (rule corr)
    show "list_all2 S xs ys" by (simp add: Cons)
  qed fact+

  show ?case
    apply (simp add: mapM_Cons)
    apply (rule corres_underlying_split [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]])
    apply (rule corres_underlying_split [OF Cons(3) _ hoare_TrueI hoare_TrueI])
    apply (simp add: rc)
    apply (rule Cons.hyps)+
    done
qed

(* FIXME: see comment for mapM rule. Same applies for lemma strength *)
lemma corres_mapM_x:
  assumes x: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying sr nf nf' dc P P' (f x) (f' y)"
  assumes y: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
  assumes z: "length xs = length ys"
  assumes w: "set (zip xs ys) \<subseteq> S"
  shows      "corres_underlying sr nf nf' dc P P' (mapM_x f xs) (mapM_x f' ys)"
  apply (simp add: mapM_x_mapM)
  apply (rule corres_guard_imp)
    apply (rule corres_split_nor)
       apply (rule corres_mapM [OF _ _ x y z w])
           apply (simp | wp)+
  done

lemmas corres_mapM_x' = corres_mapM_x[OF _ _ _ _ order_refl]

(* FIXME: see comment for mapM rule. Same applies for lemma strength *)
lemma corres_mapME:
  assumes x: "r [] []"
  assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
  assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r') P P' (f x) (f' y)"
  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
  shows      "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow>
                   corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys)"
proof (induct xs ys rule: list_induct2)
  case Nil
  show ?case
    by (simp add: mapME_def sequenceE_def x returnOk_def)
next
  case (Cons a as b bs)
  from Cons have P: "(a, b) \<in> S"
    by simp
  from Cons have Q: "corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)"
    by simp
  show ?case
    apply (simp add: mapME_Cons)
    apply (rule corres_guard_imp)
    apply (unfold bindE_def validE_def)
      apply (rule corres_underlying_split[OF z[OF P]])
        apply (case_tac rv)
         apply (clarsimp simp: throwError_def)
        apply clarsimp
        apply (rule corres_split[OF Q])
          apply (rule corres_trivial)
          apply (case_tac rv)
           apply (clarsimp simp add: lift_def throwError_def)
          apply (clarsimp simp add: y lift_def returnOk_def throwError_def)
         apply (wpsimp wp: w P)+
  done
qed

lemma corres_Id:
  "\<lbrakk> f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> no_fail P' g \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r \<top> P' f g"
  apply (clarsimp simp: corres_underlying_def Ball_def no_fail_def)
  apply (rule rev_bexI, assumption)
  apply simp
  done

lemma select_pick_corres_underlying:
  "corres_underlying sr nf nf' r P Q (f x) g
     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g"
  by (fastforce simp: corres_underlying_def select_def bind_def)

lemma select_pick_corres:
  "corres_underlying sr nf nf' r P Q (f x) g
     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g"
  by (fastforce simp: intro: select_pick_corres_underlying)

lemma select_pick_corresE:
  "corres_underlying sr nf nf' r P Q (f x) g
     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (liftE (select S) >>=E f) g"
  by (fastforce simp: liftE_bindE intro: select_pick_corres)

lemma corres_modify:
  assumes rl:
  "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> (f s, g s') \<in> sr"
  shows "corres_underlying sr nf nf' dc P P' (modify f) (modify g)"
  by (simp add: simpler_modify_def corres_singleton rl)

lemma corres_gets_the:
  assumes x: "corres_underlying sr nf nf' (r \<circ> the) P P' (gets f) y"
  shows      "corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y"
proof -
  have z: "corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y)
                 (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y"
    apply (subst corres_cong [OF refl refl refl refl])
     defer
     apply (rule corres_guard_imp[OF x], simp+)
    apply (clarsimp simp: simpler_gets_def)
    done
  show ?thesis
    apply (rule corres_guard_imp)
      apply (unfold gets_the_def)
      apply (subst bind_return[symmetric], rule corres_split [OF z])
        apply (rule corres_trivial, clarsimp simp: assert_opt_def)
       apply (wp | simp)+
  done
qed

text \<open>Some results concerning the interaction of abstract and concrete states\<close>

definition ex_abs_underlying :: "('a \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
  "ex_abs_underlying sr P s' \<equiv> \<exists>s. (s,s') \<in> sr \<and> P s"

lemma ex_absI[intro!]:
  "(s, s') \<in> sr \<Longrightarrow> P s \<Longrightarrow> ex_abs_underlying sr P s'"
  by (auto simp add: ex_abs_underlying_def)

lemma corres_u_nofail:
  "\<lbrakk>corres_underlying S nf True r P P' f g; nf \<Longrightarrow> no_fail P f\<rbrakk>
   \<Longrightarrow> no_fail (P' and ex_abs_underlying S P) g"
  by (fastforce simp: corres_underlying_def ex_abs_underlying_def no_fail_def)

lemma wp_from_corres_u:
  "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv s. (s,s') \<in> R \<and> r rv rv' \<and> Q rv s \<and> Q' rv' s'\<rbrace>"
  apply (fastforce simp: corres_underlying_def valid_def no_fail_def)
  done

lemma wp_from_corres_u_unit:
  "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace>
  f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> R \<and> Q s \<and> Q' s'\<rbrace>"
  apply (fastforce dest: wp_from_corres_u elim: hoare_strengthen_post)
  done

lemma corres_nofail:
  "corres_underlying state_relation nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
  no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> P' s') g"
  by (fastforce intro: no_fail_pre corres_u_nofail simp: ex_abs_underlying_def)

lemma wp_from_corres_unit:
  "\<lbrakk> corres_underlying state_relation nf nf' r G G' f f';
     \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace>
  f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>"
  by (auto intro!: wp_from_corres_u_unit)

lemma corres_underlying_split_ex_abs:
  assumes ac: "corres_underlying srel nf nf' r' G G' a c"
  assumes bd: "\<forall>rv rv'. r' rv rv' \<longrightarrow>
                        corres_underlying srel nf nf' r (P rv) (P' rv') (b rv) (d rv')"
  assumes valid: "\<lbrace>G\<rbrace> a \<lbrace>P\<rbrace>" "\<lbrace>G' and ex_abs_underlying srel G\<rbrace> c \<lbrace>P'\<rbrace>"
  shows "corres_underlying srel nf nf' r G G' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))"
  using assms
  apply (clarsimp simp: corres_underlying_def bind_def)
  apply (clarsimp simp: Bex_def Ball_def valid_def ex_abs_underlying_def)
  by meson

lemma hoare_from_abs:
  assumes corres: "corres_underlying srel nf nf' rrel G G' f f'"
  assumes cross2: "\<And>s s' r r'. \<lbrakk>(s, s') \<in> srel; rrel r r'; Q r s; S s\<rbrakk> \<Longrightarrow> Q' r' s'"
  assumes abs_valid: "\<lbrace>P and R\<rbrace> f \<lbrace>\<lambda>rv. Q rv and S\<rbrace>"
  assumes cross1: "\<And>s s'. \<lbrakk>(s, s') \<in> srel; P' s'; R' s'\<rbrakk> \<Longrightarrow> P s"
  assumes nf: "nf \<Longrightarrow> no_fail (P and R and G) f"
  shows "\<lbrace>P' and G' and R' and ex_abs_underlying srel (G and R)\<rbrace> f' \<lbrace>Q'\<rbrace>"
  using assms
  apply (clarsimp simp: valid_def ex_abs_underlying_def corres_underlying_def no_fail_def)
  by fast

lemma hoare_from_abs_inv:
  assumes abs_valid: "f \<lbrace>P\<rbrace>"
  assumes cross: "\<And>s s'. (s, s') \<in> srel \<Longrightarrow> P s = P' s'"
  assumes corres: "corres_underlying srel nf nf' rrel G G' f f'"
  assumes nf: "nf \<Longrightarrow> no_fail (P and G) f"
  shows "\<lbrace>P' and G' and ex_abs_underlying srel G\<rbrace> f' \<lbrace>\<lambda>_. P'\<rbrace>"
  using assms
  by (fastforce intro: hoare_from_abs[where R=\<top> and S=\<top> and R'=\<top> and Q="\<lambda>_. P" , simplified])

lemma corres_from_valid:
  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying srel P) f'"
  assumes
    "\<And>s. \<lbrace>\<lambda>s'. P s \<and> P' s' \<and> (s, s') \<in> srel\<rbrace>
          f' \<lbrace>\<lambda>rv' t'. \<exists>(rv, t) \<in> fst (f s). (t, t') \<in> srel \<and> rrel rv rv'\<rbrace>"
  shows "corres_underlying srel nf nf' rrel P P' f f'"
  using assms
  by (fastforce simp: corres_underlying_def valid_def no_fail_def)

lemma corres_from_valid_det:
  assumes det: "det_wp P f"
  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying srel P) f'"
  assumes valid:
    "\<And>s rv t.
      \<lbrakk>fst (f s) = {(rv, t)}; P s\<rbrakk>
      \<Longrightarrow> \<lbrace>\<lambda>s'. P' s' \<and> (s, s') \<in> srel\<rbrace> f' \<lbrace>\<lambda>rv' t'. (t, t') \<in> srel \<and> rrel rv rv'\<rbrace>"
  shows "corres_underlying srel nf nf' rrel P P' f f'"
  apply (clarsimp simp: corres_underlying_def)
  apply (intro conjI)
   apply (insert det)
   apply (clarsimp simp: det_wp_def)
   apply (force dest: use_valid[OF _ valid])
  apply (fastforce dest: nf' simp: no_fail_def ex_abs_underlying_def)
  done

lemma corres_noop_ex_abs:
  assumes P: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>"
  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr P) f"
  shows "corres_underlying sr nf nf' r P P' (return x) f"
  apply (simp add: corres_underlying_def return_def)
  apply clarsimp
  apply (frule P)
  apply (insert nf')
  apply (fastforce simp: valid_def no_fail_def ex_abs_underlying_def)
  done

lemma corres_symb_exec_r_conj_ex_abs:
  assumes z: "\<And>rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)"
  assumes y: "\<lbrace>Q'\<rbrace> m \<lbrace>R'\<rbrace>"
  assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr P) m"
  shows      "corres_underlying sr nf nf' r (P and Q) (P' and Q') x (m >>= (\<lambda>rv. y rv))"
proof -
  have P: "corres_underlying sr nf nf' dc P P' (return undefined) m"
    apply (rule corres_noop_ex_abs)
     apply (simp add: x)
    apply (erule nf)
    done
  show ?thesis
    apply (rule corres_guard_imp)
      apply (subst return_bind[symmetric], rule corres_split[OF P])
        apply (rule z)
       apply wp
      apply (rule y)
     apply simp+
    done
qed

lemmas corres_symb_exec_r_conj_ex_abs_forwards =
  corres_symb_exec_r_conj_ex_abs[where P=P and Q=P for P, where P'=P' and Q'=P' for P', simplified]

lemma gets_the_corres_ex_abs':
 "\<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow>
   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
  by (fastforce simp: gets_the_def no_ofail_def corres_underlying_def split_def exec_gets
                      assert_opt_def fail_def return_def ex_abs_underlying_def)

lemmas gets_the_corres_ex_abs = gets_the_corres_ex_abs'[THEN iffD2]

lemma gets_the_corres':
 "\<lbrakk>no_ofail P a; no_ofail P' b\<rbrakk> \<Longrightarrow>
   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
  apply (erule gets_the_corres_ex_abs')
  apply (fastforce intro: no_ofail_pre_imp)
  done

lemmas gets_the_corres = gets_the_corres'[THEN iffD2]

lemma gets_the_corres_relation:
 "\<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f');
   P s; P' s'; (s, s') \<in> sr\<rbrakk>
  \<Longrightarrow> r (the (f s)) (the (f' s'))"
  apply (rule_tac P=P and a=f and b=f' and P'=P'
               in gets_the_corres_ex_abs'[THEN iffD1, rule_format];
         fastforce?)
  apply (rule no_ofail_gets_the_eq[THEN iffD2])
  apply (fastforce intro: corres_u_nofail)
  done


\<comment> \<open>Some @{term corres_underlying} rules for @{term whileLoop}\<close>

lemma in_whileLoop_corres:
  assumes body_corres:
    "\<And>r r'. rrel r r' \<Longrightarrow>
             corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
  assumes body_inv:
    "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
    "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
  assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
  assumes result: "(rv', t') \<in> fst (whileLoop C' B' r' s')"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "\<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s'
                \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C B r s) \<and> (t, t') \<in> srel \<and> rrel rv rv')"
  apply (rule in_whileLoop_induct[OF result])
   apply (force simp: cond whileLoop_def)
  apply clarsimp
  apply (frule (1) corres_underlyingD2[OF body_corres];
         (fastforce dest: nf simp: cond no_fail_def)?)
  apply clarsimp
  apply (frule use_valid[OF _ body_inv(1)])
   apply (fastforce dest: cond)
  apply (frule use_valid[OF _ body_inv(2)])
   apply fastforce
  apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3) dest: cond)
  done

lemma corres_whileLoop_ret:
  assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
  assumes body_corres:
    "\<And>r r'. rrel r r' \<Longrightarrow>
             corres_underlying srel False nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
  assumes body_inv:
    "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
    "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
  assumes rel: "rrel r r'"
  assumes nf': "\<And>r'. no_fail (P' r' and C' r') (B' r')"
  assumes termin: "\<And>r' s'. \<lbrakk>P' r' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'"
  shows "corres_underlying srel False nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')"
  apply (rule corres_no_failI)
   apply (simp add: no_fail_def)
   apply (intro impI allI)
   apply (erule_tac I="\<lambda>r' s'. P' r' s'"
                    and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
                                              \<and> whileLoop_terminates C' B' r s}"
                    in not_snd_whileLoop)
    apply (clarsimp simp: validNF_def)
    apply (rule conjI)
     apply (intro hoare_vcg_conj_lift_pre_fix; wpsimp?)
       using body_inv
       apply (fastforce simp: valid_def)
      apply (clarsimp simp: valid_def)
     apply (insert termin)[1]
     apply wpsimp
    apply (fastforce intro: no_fail_pre nf')
   apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']])
  apply clarsimp
  apply (frule in_whileLoop_corres[OF body_corres body_inv]; (fastforce dest: cond)?)
  apply (fastforce intro: assms)
  done

lemmas corres_whileLoop =
  corres_whileLoop_ret[where P="\<lambda>_. P" for P, where P'="\<lambda>_. P'" for P', simplified]

lemma whileLoop_terminates_cross:
  assumes body_corres:
    "\<And>r r'. rrel r r' \<Longrightarrow>
             corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
  assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
  assumes body_inv:
    "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
    "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
  assumes abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
  assumes ex_abs: "ex_abs_underlying srel (P r) s'"
  assumes rrel: "rrel r r'"
  assumes P': "P' r' s'"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "whileLoop_terminates C' B' r' s'"
proof -
  have helper: "\<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s'
                                               \<longrightarrow> whileLoop_terminates C' B' r' s'"
       (is "\<And>s. _ \<Longrightarrow> ?I r s")
    apply (rule_tac P="?I" in whileLoop_terminates.induct)
      apply (fastforce intro: abs_termination)
     apply (fastforce simp: whileLoop_terminates.intros dest: cond)
    apply (subst whileLoop_terminates.simps)
    apply clarsimp
    apply (frule (1) corres_underlyingD2[OF body_corres], (fastforce dest: nf simp: no_fail_def)+)
    apply (fastforce dest: use_valid intro: body_inv)
    done

  show ?thesis
    apply (insert assms helper)
    apply (cases "C' r' s'")
     apply (fastforce simp: ex_abs_underlying_def)
    apply (simp add: whileLoop_terminates.intros(1))
    done
qed

lemma corres_whileLoop_abs_ret:
  assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
  assumes body_corres:
    "\<And>r r'. rrel r r' \<Longrightarrow>
             corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
  assumes rrel: "rrel r r'"
  assumes body_inv:
    "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
    "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
  assumes abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "corres_underlying srel nf nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')"
  apply (rule corres_underlyingI)
   apply (frule in_whileLoop_corres[OF body_corres body_inv];
          (fastforce intro: body_corres body_inv rrel dest: nf cond))
  apply (rule_tac I="\<lambda>rv' s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv rv' \<and> P rv s \<and> P' rv' s'"
              and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
                                        \<and> whileLoop_terminates C' B' r s}"
               in not_snd_whileLoop)
    apply (fastforce intro: rrel)
   apply (rename_tac s s' conc_r new_s)
   apply (clarsimp simp: validNF_def)
   apply (rule conjI)
    apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?)
      apply (rule_tac P'="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
                                     \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
                   in hoare_weaken_pre[rotated])
       apply clarsimp
      apply (rule hoare_ex_pre)
      apply (rename_tac abs_r)
      apply (rule hoare_weaken_pre)
       apply (rule_tac P'="rrel abs_r conc_r" in hoare_grab_asm)
       apply (wpsimp wp: wp_from_corres_u[OF body_corres] body_inv)
       apply (fastforce dest: nf)
      apply (fastforce dest: cond)
     apply (fastforce simp: valid_def)
    apply wpsimp
    apply (rule whileLoop_terminates_cross[OF body_corres];
           (fastforce dest: nf cond intro: body_inv abs_termination))
   apply (rule_tac P="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
                                  \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
                in no_fail_pre[rotated])
    apply fastforce
   apply (rule no_fail_ex_lift)
   apply (rename_tac abs_r)
   apply (rule no_fail_pre)
    apply (rule_tac G="rrel abs_r conc_r" in no_fail_grab_asm)
    apply (fastforce intro: corres_u_nofail dest: body_corres nf)
   apply (fastforce simp: cond)
  apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']])
  done

lemmas corres_whileLoop_abs =
  corres_whileLoop_abs_ret[where P="\<lambda>_. P" for P, where P'="\<lambda>_. P'" for P', simplified]

text \<open>Some corres_underlying rules for monadic combinators\<close>

lemma ifM_corres:
  assumes   test: "corres_underlying srel nf nf' (=) A A' test test'"
  and          l: "corres_underlying srel nf nf' rrel Q Q' a a'"
  and          r: "corres_underlying srel nf nf' rrel R R' b b'"
  and  abs_valid: "\<lbrace>B\<rbrace> test \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>"
                  "\<lbrace>C\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R s\<rbrace>"
  and conc_valid: "\<lbrace>B'\<rbrace> test' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>"
                  "\<lbrace>C'\<rbrace> test' \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R' s\<rbrace>"
  shows "corres_underlying srel nf nf' rrel (A and B and C) (A' and B' and C')
           (ifM test a b) (ifM test' a' b')"
  unfolding ifM_def
  apply (rule corres_guard_imp)
    apply (rule corres_split[OF test])
      apply (erule corres_if[OF _ l r])
     apply (wpsimp wp: abs_valid conc_valid hoare_vcg_if_lift2)+
  done

lemmas ifM_corres' =
  ifM_corres[where A=A and B=A and C=A for A, simplified,
             where A'=A' and B'=A' and C'=A' for A', simplified]

lemma orM_corres:
  "\<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) R R' b b';
    \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R' s\<rbrace>\<rbrakk>
   \<Longrightarrow> corres_underlying srel nf nf' (=) (A and B) (A' and B') (orM a b) (orM a' b')"
  unfolding orM_def
  apply (rule corres_guard_imp)
    apply (rule ifM_corres[where Q=\<top> and Q'=\<top>])
        apply (wpsimp | fastforce)+
  done

lemmas orM_corres' =
  orM_corres[where A=A and B=A for A, simplified, where A'=A' and B'=A' for A', simplified]

lemma andM_corres:
  "\<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b';
    \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk>
   \<Longrightarrow> corres_underlying srel nf nf' (=) (A and B) (A' and B') (andM a b) (andM a' b')"
  unfolding andM_def
  apply (rule corres_guard_imp)
    apply (erule (1) ifM_corres[where R=\<top> and R'=\<top>])
        apply (wpsimp | assumption)+
  done

lemma notM_corres:
  "corres_underlying srel nf nf' (=) G G' a a'
   \<Longrightarrow> corres_underlying srel nf nf' (=) G G' (notM a) (notM a')"
  unfolding notM_def
  apply (rule corres_guard_imp)
    apply (erule corres_split)
      apply wpsimp+
  done

lemma ifM_to_top_of_bind:
  "((ifM test true false) >>= z) = ifM test (true >>= z) (false >>= z)"
  by (force simp: ifM_def bind_def split: if_splits)

end