SSL CorresXF.thy

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
 * A stronger version of the "corres" framework, allowing return
 * relationships to reference state data.
 *)

theory CorresXF
imports
  CCorresE
begin

(*
 * Refinement with return extraction on the concrete side:
 *
 * For any step on the concrete side, there is an equivalent step on
 * the abstract side.
 *
 * If the abstract step fails, we don't need refinement to hold.
 *)

definition "corresXF_simple st xf P M M' ≡
  ∀s. (P s ∧ succeeds M (st s)) ⟶ (∀r' t'. reaches M' s r' t' ⟶
        reaches M (st s) (xf r' t') (st t')) ∧ succeeds M' s"

(*
 * A definition better suited to dealing with monads with exceptions.
 *)
definition "corresXF st ret_xf ex_xf P A C ≡
    ∀s. P s ∧ succeeds A (st s) ⟶
        (∀r t. reaches C s r t ⟶
          (case r of
             Exn r ==> reaches A (st s) (Exn (ex_xf r t)) (st t)
           | Result r ==> reaches A (st s) (Result (ret_xf r t)) (st t)))
        ∧ succeeds C s"


definition "rel_XF st ret_xf ex_xf Q ≡ λ(r, t) (r', t').
  t' = st t ∧
  rel_xval (λe e'. e' = ex_xf e t) (λv v'. v' = ret_xf v t) r r' ∧
  Q r t"

lemma corresXF_refines_iff: 
  "corresXF st ret_xf ex_xf P A C ⟷
      (∀s. P s ⟶ refines C A s (st s) (rel_XF st ret_xf ex_xf (λ_ _. True)))"
  apply standard
  subgoal
    apply (clarsimp simp add: corresXF_def refines_def_old rel_XF_def rel_xval.simps split: xval_splits)
    by (metis Exn_def default_option_def exception_or_result_cases not_Some_eq)
  subgoal
    apply (fastforce simp add: corresXF_def refines_def_old rel_XF_def rel_xval.simps split: xval_splits)
    done
  done

lemma corresXF_trans[corres_le_trans]: "corresXF st ret_xf ex_xf P A C ==> A ≤ A'
  ==> corresXF st ret_xf ex_xf P A' C"
  by (auto simp add: corresXF_refines_iff refines_le_trans)

lemma corresXF_trans': "corresXF st ret_xf ex_xf P A C' ==> C ≤ C'
  ==> corresXF st ret_xf ex_xf P A C"
  by (auto simp add: corresXF_refines_iff le_refines_trans)
(*
* Stronger variant with postcondition
*)
definition "corresXF_post st ret_xf ex_xf P Q A C ≡
    ∀s. P s ∧ succeeds A (st s) ⟶
        (∀r t. reaches C s r t ⟶ Q s r t ∧
          (case r of
             Exn r ==> reaches A (st s) (Exn (ex_xf r t)) (st t)
           | Result r ==> reaches A (st s) (Result (ret_xf r t)) (st t)))
        ∧ succeeds C s"

lemma corresXF_post_refines_iff: 
  "corresXF_post st ret_xf ex_xf P Q A C ⟷
      (∀s. P s ⟶ refines C A s (st s) (rel_XF st ret_xf ex_xf (Q s)))"
  apply standard
  subgoal
    apply (clarsimp simp add: corresXF_post_def refines_def_old rel_XF_def rel_xval.simps split: xval_splits)
    by (metis Exn_def default_option_def exception_or_result_cases not_Some_eq)
  subgoal
    apply (fastforce simp add: corresXF_post_def refines_def_old rel_XF_def rel_xval.simps split: xval_splits)
    done
  done

lemma corresXF_post_trans[corres_le_trans]: "corresXF_post st ret_xf ex_xf P Q A C ==> A ≤ A'
  ==> corresXF_post st ret_xf ex_xf P Q A' C"
  by (auto simp add: corresXF_post_refines_iff refines_le_trans)

lemma corresXF_post_to_corresXF: 
  "corresXF_post st ret_xf ex_xf P Q A C ==> corresXF st ret_xf ex_xf P A C"
  by (auto simp add: corresXF_def corresXF_post_def)

lemma corresXF_corres_XF_post_conv: 
  "corresXF st ret_xf ex_xf P A C = corresXF_post st ret_xf ex_xf P (λ_ _ _. True) A C"
  by (auto simp add: corresXF_def corresXF_post_def)


(* corresXF can be defined in terms of corresXF_simple. *)
lemma corresXF_simple_corresXF:
  "(corresXF_simple st
       (λx s. case x of
           Exn r ==> Exn (ex_state r s)
         | Result r ==> (Result (ret_state r s))) P M M')
  = (corresXF st ret_state ex_state P M M')"
 unfolding corresXF_simple_def corresXF_def
 by (auto split: xval_splits)


lemma corresXF_simpleI: "[
    ∧s' t' r'. [P s'; succeeds M (st s'); reaches M' s' r' t']
        ==> reaches M (st s') (xf r' t') (st t');
    ∧s'. [P s'; succeeds M (st s') ] ==> succeeds M' s'
  ] ==> corresXF_simple st xf P M M'"
  apply atomize
  apply (clarsimp simp: corresXF_simple_def)
  done

lemma corresXF_I: "[
    ∧s' t' r'. [P s'; succeeds M (st s'); reaches M' s' (Result r') t']
        ==> reaches M (st s') (Result (ret_state r' t')) (st t');
    ∧s' t' r'. [P s'; succeeds M (st s'); reaches M' s' (Exn r') t']
        ==> reaches M (st s') (Exn (ex_state r' t')) (st t');
    ∧s'. [P s'; succeeds M (st s') ] ==> succeeds M' s'
  ] ==> corresXF st ret_state ex_state P M M'"
  apply atomize
  apply (clarsimp simp: corresXF_def)
  subgoal for s r t
    apply (erule_tac x=s in allE, erule (1) impE)
    apply (erule_tac x=s in allE, erule (1) impE)
    apply (erule_tac x=s in allE, erule (1) impE)
    apply (clarsimp split: xval_splits)
    apply auto
    done
  done

lemma ccpo_prod_gfp_gfp:
  "class.ccpo
    (prod_lub Inf Inf :: (('a::complete_lattice * 'b :: complete_lattice) set ==> _))
    (rel_prod (≥) (≥)) (mk_less (rel_prod (≥) (≥)))"
  by (rule ccpo_rel_prodI ccpo_Inf)+

lemma admissible_mem: "ccpo.admissible Inf (≥) (λA. x ∈ A)"
  by (auto simp: ccpo.admissible_def)

lemma admissible_nondet_ord_corresXF:
  "ccpo.admissible Inf (≥) (λA. corresXF st R E P A C)"
  unfolding corresXF_def imp_conjL imp_conjR
  apply (intro admissible_all  admissible_conj admissible_imp)
  subgoal for s
  apply (rule ccpo.admissibleI)
    apply (clarsimp simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits xval_splits)
    apply (intro conjI allI impI)
    subgoal
      apply transfer
      by (auto simp add: Inf_post_state_def top_post_state_def)
         (metis outcomes.simps(2) post_state.simps(3))
    subgoal
      apply transfer
      by (auto simp add: Inf_post_state_def top_post_state_def)
         (metis outcomes.simps(2) post_state.simps(3))
    done
  subgoal
    apply (rule ccpo.admissibleI)
    apply (clarsimp simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits xval_splits)
    apply transfer
    apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
    done
  done



lemma corresXF_top: "corresXF st ret_xf ex_xf P ⊤ C"
  by (auto simp add: corresXF_def)

lemma admissible_nondet_ord_corresXF_post:
  "ccpo.admissible Inf (≥) (λA. corresXF_post st R E P Q A C)"
  unfolding corresXF_post_def imp_conjL imp_conjR
  apply (intro admissible_all  admissible_conj admissible_imp)
  subgoal
  apply (rule ccpo.admissibleI)
    apply (clarsimp simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits xval_splits)
    apply (intro conjI allI impI)
    subgoal
      apply transfer
      apply (clarsimp simp add: Inf_post_state_def top_post_state_def)
      apply (metis (no_types, lifting) INF_top_conv(1) Inf_post_state_def top_post_state_def)
      done
    subgoal
      apply transfer
      by (auto simp add: Inf_post_state_def top_post_state_def)
         (metis outcomes.simps(2) post_state.simps(3))
   subgoal
     apply transfer
     apply (clarsimp simp add: Inf_post_state_def top_post_state_def)
     apply (metis (no_types, lifting) INF_top_conv(1) Inf_post_state_def top_post_state_def)
     done
   subgoal
     apply transfer
     apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
         split: if_split_asm)
     by (metis outcomes.simps(2) post_state.simps(3))
    done
  subgoal
    apply (rule ccpo.admissibleI)
    apply (clarsimp simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits xval_splits)
    apply transfer
    apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
    done
  done



lemma corresXF_post_top: "corresXF_post st ret_xf ex_xf P Q ⊤ C"
  by (auto simp add: corresXF_post_def)

lemma corresXF_assume_pre:
  "[ ∧s s'. [ P s'; s = st s' ] ==> corresXF st xf_normal xf_exception P L R ] ==> corresXF st xf_normal xf_exception P L R"
  apply atomize
  apply (clarsimp simp: corresXF_def)
  apply force
  done

lemma corresXF_assume_fix_pre:
  "[ ∧s s'. [ P s'; s = st s' ] ==> corresXF st xf_normal xf_exception (λs. s = s' ∧ P s) L R ] ==> corresXF st xf_normal xf_exception P L R"
  apply atomize
  apply (clarsimp simp: corresXF_def)
  done

lemma corresXF_guard_imp:
  "[ corresXF st xf_normal xf_exception Q f g; ∧s. P s ==> Q s ]
      ==> corresXF st xf_normal xf_exception P f g"
  apply (clarsimp simp: corresXF_def)
  done

lemma corresXF_return:
  "[ ∧s. [ P s ] ==> xf_normal b s = a ] ==>
     corresXF st xf_normal xf_exception P (return a) (return b)"
  apply (clarsimp simp: corresXF_def )
  done

lemma corresXF_gets:
  "[ ∧s. P s ==> ret (g s) s = f (st s) ] ==>
     corresXF st ret ex P (gets f) (gets g)"
  apply (clarsimp simp: corresXF_def)
  done

lemma corresXF_insert_guard:
  "[ corresXF st ret ex Q A C; ∧s. [ P s ] ==> G (st s) ⟶ Q s ] ==>
        corresXF st ret ex P (guard G >>= (λ_. A)) C "
  apply (auto  simp: corresXF_def succeeds_guard succeeds_bind reaches_bind reaches_guard)
  done

lemma corresXF_exec_abs_guard:
  "corresXF st ret_xf ex_xf (λs. P s ∧ G (st s)) (A ()) C ==> corresXF st ret_xf ex_xf P (guard G >>= A) C"
  apply (auto simp: corresXF_def succeeds_guard succeeds_bind reaches_bind reaches_guard)
  done

lemma corresXF_simple_exec:
  "[ corresXF_simple st xf P A B; reaches B s r' s'; succeeds A (st s); P s ]
      ==> reaches A (st s) (xf r' s') (st s')"
  apply (fastforce simp: corresXF_simple_def)
  done

lemma corresXF_simple_fail:
  "[ corresXF_simple st xf P A B; ¬ succeeds B s; P s ]
      ==> ¬ succeeds A (st s)"
  apply (fastforce simp: corresXF_simple_def)
  done

lemma corresXF_simple_no_fail:
  "[ corresXF_simple st xf P A B; succeeds A (st s); P s ]
      ==> succeeds B s"
  apply (fastforce simp: corresXF_simple_def)
  done

lemma corresXF_exec_normal:
  "[ corresXF st ret ex P A B; reaches B s (Result r') s'; succeeds A (st s); P s ]
      ==> reaches A (st s) (Result (ret r' s')) (st s')"
  by (auto simp add: corresXF_def split: xval_splits)

lemma corresXF_exec_except:
  "[ corresXF st ret ex P A B; reaches B s (Exn r') s'; succeeds A (st s); P s ]
      ==> reaches A (st s) (Exn (ex r' s')) (st s')"
  by (auto simp add: corresXF_def split: xval_splits)

lemma corresXF_exec_fail:
  "[ corresXF st ret ex P A B; ¬ succeeds B s; P s ]
      ==> ¬ succeeds A (st s)"
  by (auto simp add: corresXF_def split: xval_splits)

lemma corresXF_intermediate:
    "[ corresXF st ret_xf ex_xf P A' C;
         corresXF id (λr s. r) (λr s. r) (λs. ∃x. s = st x ∧ P x) A A' ] ==>
        corresXF st ret_xf ex_xf P A C"
  apply (clarsimp simp: corresXF_def split: xval_splits)
  apply fast
  done

lemma corresXF_join:
  "[ corresXF st V E P L L'; ∧x y. corresXF st V' E (P' x y) (R x) (R' y);
    ∧s. Q s ==> L' ∙ s ?{ λr t. case r of Exn _ ==> ⊤ | Result v ==> P' (V v t) v t };
    ∧s. Q s ==> P s ] ==>
    corresXF st V' E Q (L >>= R) (L' >>= R')"
  apply (clarsimp simp add: corresXF_refines_iff split: xval_splits)
  apply (rule refines_bind_bind_exn[where Q="rel_XF st V E (λ_ _. True) ⊓
    (λ(r, t) x. case r of Exn _ ==> ⊤ | Result v ==> P' (V v t) v t)"])
  subgoal
    apply (rule refines_strengthen1[where R="rel_XF st V E (λ_ _. True)"])
    by auto
  by (auto simp add: rel_XF_def)

lemma corresXF_join_xf_state_independent_same_state:
  "[ corresXF (λs. s) (λr s. V r) (λr s. E r) P L L';
    ∧y. corresXF (λs. s) (λr s. V' r) (λr s. E r) (P' (V y)) (R (V y)) (R' y);
    ∧s. Q s ==> L ∙ s ?{ λr t. case r of Exn _ ==> ⊤ | Result v ==> P' v t}; ∧s. Q s ==> P s ] ==>
    corresXF (λs. s) (λr s. V' r) (λr s. E r) Q (L >>= R) (L' >>= R')"
  apply (clarsimp simp add: corresXF_refines_iff)
  apply (rule refines_bind_bind_exn[where
        Q="rel_XF (λs. s) (λr s. V r) (λr s. E r) (λ_ _. True) ⊓
          (λx (r, t). case r of Exn _ ==> ⊤ | Result v ==> P' v t)"])
  subgoal
    apply (rule refines_strengthen2[where R="rel_XF (λs. s) (λr s. V r) (λr s. E r) (λ_ _. True)"])
    by auto
  by (auto simp add: rel_XF_def)

lemma corresXF_except:
  "[ corresXF st V E P L L'; ∧x y. corresXF st V E' (P' x y) (R x) (R' y);
    ∧s. Q s ==> L' ∙ s ?{ λr s. case r of Exn r ==> P' (E r s) r s | Result _ ==> ⊤ };
    ∧s. Q s ==> P s ] ==>
    corresXF st V E' Q ( L <catch> R) (L' <catch> R')"
  apply (clarsimp simp add: corresXF_refines_iff)
  apply (rule refines_catch [where Q="(rel_XF st V E (λ_ _. True)) ⊓
    (λ(r, s) x. case r of Exn r ==> P' (E r s) r s | Result _ ==> ⊤)"])
  subgoal 
    apply (rule refines_strengthen1[where R="rel_XF st V E (λ_ _. True)"])
    by auto
  apply (auto simp add: rel_XF_def)
  done

lemma corresXF_cond:
  "[ corresXF st V E P L L'; corresXF st V E P R R'; ∧s. P s ==> A (st s) = A' s ] ==>
    corresXF st V E P (condition A L R) (condition A' L' R')"
  apply (clarsimp simp add: corresXF_refines_iff)
  using refines_condition by metis

lemma refines_assume_succeeds: "(succeeds g t ==> refines f g s t R) ==> refines f g s t R"
  by (auto simp add: refines_def_old)

lemma corresXF_while:
  assumes body_corres: "∧x y. corresXF st ret ex (λs. P x s ∧ y = ret x s) (A y) (B x)"
  and cond_match: "∧s r. P r s ==> C r s = C' (ret r s) (st s)"
  and pred_inv: "∧r s. P r s ==> C r s ==> succeeds (whileLoop C' A (ret r s)) (st s) ==>
                          B r ∙ s ?{ λr s. case r of Exn _ ==> True | Result r ==> P r s }"
  and init_match: "∧s. P' x s ==> y = ret x s"
  and pred_imply: "∧s. P' x s ==> P x s"
shows "corresXF st ret ex (P' x) (whileLoop C' A y) (whileLoop C B x)"
  apply (clarsimp simp add: corresXF_refines_iff)
  apply (rule refines_assume_succeeds)
  subgoal for s
    apply (rule refines_mono [OF _ refines_whileLoop' 
          [where R = "rel_XF st ret ex (λr s. case r of Exn _ ==> True | Result r ==> P r s) ⊓
            (λ(r, s) _. case r of Exn _ ==> True | Result r ==>
              succeeds (whileLoop C' A (ret r s)) (st s))" 
          and C = C and C'=C' and B=B and B'=A and I=x and I'=y and s=s and s'="st s"]])
    subgoal by (auto simp add: rel_XF_def)
    subgoal by (auto simp add: rel_XF_def cond_match pred_imply)
    subgoal using body_corres pred_inv
      apply (subst (asm) rel_XF_def)
      apply (clarsimp simp add: corresXF_refines_iff)
      apply (rule refines_strengthen[where R="rel_XF st ret ex (λ_ _. True)" and
        G="λr s. case r of Exn _ ==> True | Result r ==> succeeds (whileLoop C' A r) s"])
      subgoal by auto
      apply assumption
      subgoal
        apply (subst (asm) (3) whileLoop_unroll)
        apply (auto simp add: succeeds_bind runs_to_partial_def_old split: xval_splits)
        done
      apply (auto simp: rel_XF_def rel_xval.simps)
      done
    subgoal
      by (auto simp add: rel_XF_def init_match pred_imply)
    subgoal
      by (auto simp add: rel_XF_def rel_xval.simps rel_exception_or_result.simps Exn_def default_option_def split: xval_splits )
    done
  done

lemma corresXF_name_pre:
  "[ ∧s'. corresXF st ret ex (λs. P s ∧ s = s') A C ] ==>
           corresXF st ret ex P A C"
  by (clarsimp simp: corresXF_def)

lemma corresXF_guarded_while_body:
  "corresXF st ret ex P A B ==>
      corresXF st ret ex P
             (do{ r ← A; _ ← guard (G r); return r }) B"
  apply (clarsimp simp add: corresXF_refines_iff)
  apply (clarsimp simp add: refines_def_old succeeds_bind reaches_bind)
  by (smt (verit) Exn_def case_exception_or_result_Exn case_exception_or_result_Result 
      default_option_def the_Exception_simp the_Exception_Result exception_or_result_cases 
      is_Exception_simps(1) is_Exception_simps(2) not_None_eq)

lemma whileLoop_succeeds_terminates_guard_body: 
  assumes B_succeeds: "∧i s. succeeds (B i) s ==> succeeds (B' i) s"
  assumes B_reaches: "∧i s r t. reaches (B' i) s r t ==> succeeds (B i) s ==> reaches (B i) s r t"
  assumes termi: "run (whileLoop C B I) s ≠ ⊤"  
  shows "run (whileLoop C B' I) s ≠ ⊤" 
  using termi
proof (induct rule: whileLoop_ne_top_induct)
  case step show ?case unfolding top_post_state_def
    apply (rule whileLoop_ne_Failure)
    using step B_succeeds B_reaches
    apply (clarsimp simp add: runs_to_def_old)
    by (metis top_post_state_def)
qed

lemma whileLoop_succeeds_guard_body: 
  assumes B_succeeds: "∧i s. succeeds (B i) s ==> succeeds (B' i) s"
  assumes B_reaches: "∧i s r t. reaches (B' i) s r t ==> succeeds (B i) s ==> reaches (B i) s r t"
  assumes termi: "succeeds (whileLoop C B I) s"  
  shows "succeeds (whileLoop C B' I) s"
  using whileLoop_succeeds_terminates_guard_body [OF B_succeeds B_reaches] termi
  by (auto simp: succeeds_def top_post_state_def)


lemma corresXF_guarded_while:
  assumes body_corres: "∧x y. corresXF st ret ex (λs. P x s ∧ y = ret x s) (A y) (B x)"
  and cond_match: "∧s r. [ P r s; G (ret r s) (st s) ] ==> C r s = C' (ret r s) (st s)"
  and pred_inv: "∧r s. P r s ==> C r s ==> succeeds (whileLoop C' A (ret r s)) (st s) ==> G (ret r s) (st s) ==>
                          B r ∙ s ?{ λr s. case r of Exn _ ==> True | Result r ==> G (ret r s) (st s) ⟶ P r s }"
  and pred_imply: "∧s. [ G y (st s); P' x s ] ==> P x s"
  and init_match: "∧s. [ G y (st s); P' x s ] ==> y = ret x s"
  shows "corresXF st ret ex (P' x)
      (do {
         _ ← guard (G y);
         whileLoop C' (λi. (do {
            r ← A i;
            _ ← guard (G r);
            return r
          })) y
       })
      (whileLoop C B x)"
proof -

  {fix i s
    assume *: "succeeds (whileLoop C' (λi.
                       (do { r ← A i;
                            _ ← guard (G r);
                            return r
                        })) i) s" 
    have "succeeds (whileLoop C' A i) s"
      apply (rule  whileLoop_succeeds_guard_body [OF _ _ *])
      subgoal by (auto simp add: succeeds_bind)

      subgoal apply (clarsimp simp add: reaches_bind succeeds_bind)
        by (smt (verit, best) dual_order.refl exception_or_result_split_asm le_boolD)
      done
  } note new_body_fails_more = this


  note new_body_corres = body_corres [THEN corresXF_guarded_while_body]

  show ?thesis
    apply (rule corresXF_exec_abs_guard)
    apply (rule corresXF_name_pre)
    apply (rule corresXF_assume_pre)
    apply clarsimp
    subgoal for s'
      apply (rule corresXF_guard_imp)
       apply (rule corresXF_while [where 
            P="λx s. P x s ∧ G (ret x s) (st s)" and P'="λx s. P' x s ∧ s = s'"])
           apply (rule corresXF_guard_imp)
            apply (rule new_body_corres)
           apply (clarsimp)
          apply (clarsimp)
          apply (rule cond_match, simp, simp)
      subgoal for r s 
        using pred_inv [of r s, OF _ _ new_body_fails_more ]
        apply clarsimp
        apply (subst (asm)  whileLoop_unroll)
        apply (clarsimp simp add: cond_match)
        apply (clarsimp simp add: succeeds_bind)
        apply (clarsimp simp add: runs_to_partial_def_old split: xval_splits, intro conjI)
         apply (metis (mono_tags, lifting) body_corres corresXF_exec_normal)
        using body_corres corresXF_exec_normal by fastforce
      subgoal
        using init_match by auto
      subgoal
        using init_match pred_imply by auto
      subgoal by auto
      done
    done
qed


(*

definition "corresXF st ret_xf ex_xf P A C \<equiv>
    \<forall>s. P s \<and> \<not> snd (A (st s)) \<longrightarrow>
        (\<forall>(r, t) \<in> fst (C s).
          case r of
             Inl r \<Rightarrow> (Inl (ex_xf r t), st t) \<in> fst (A (st s))
           | Inr r \<Rightarrow> (Inr (ret_xf r t), st t) \<in> fst (A (st s)))
        \<and> \<not> snd (C s)"*)


(* Merge of lemmas ccorresE and corresXF. *)
definition "ac_corres st check_termination AF Γ rx ex G ≡
  λA B. ∀s. (G s ∧ succeeds A (st s)) ⟶
         (∀t. Γ ⊨ ⟨B, Normal s⟩ ==> t ⟶
             (case t of
               Normal s' ==> reaches A (st s) (Result (rx s')) (st s')
             | Abrupt s' ==> reaches A (st s) (Exn (ex s')) (st s')
             | Fault e ==> e ∈ AF
             | _ ==> False))
          ∧ (check_termination ⟶ Γ ⊨ B ↓ Normal s)"

(* We can merge ccorresE and corresXF to form a ccorresXF statement. *)
lemma ccorresE_corresXF_merge:
  "[ ccorresE st1 ct AF Γ ⊤ G1 M B;
     corresXF st2 rx ex G2 A M;
     ∧s. st s = st2 (st1 s);
     ∧r s. rx' s = rx r (st1 s);
     ∧r s. ex' s = ex r (st1 s);
     ∧s. G s ⟶ (s ∈ G1 ∧ G2 (st1 s)) ] ==>
    ac_corres st ct AF Γ rx' ex' G A B"
  apply (unfold ac_corres_def)
  apply clarsimp
  apply (clarsimp simp: ccorresE_def)
  apply (clarsimp simp: corresXF_def)
  apply (erule allE, erule impE, force)
  apply (erule allE, erule impE, force)
  apply clarsimp
  apply (erule allE, erule impE, fastforce)
  subgoal for s t by (cases t; fastforce)
  done


(* We can also merge corresXF statements. *)
lemma corresXF_corresXF_merge:
  "[ corresXF st rx ex P A B; corresXF st' rx' ex' P' B C ] ==>
    corresXF (st o st') (λrv s. rx (rx' rv s) (st' s))
             (λrv s. ex (ex' rv s) (st' s)) (λs. P' s ∧ P (st' s)) A C "
  apply (clarsimp simp: corresXF_def split: xval_splits)
  apply fastforce
  done

lemma ac_corres_guard_imp:
  "[ ac_corres st ct AF G rx ex P A C; ∧s. P' s ==> P s ] ==> ac_corres st ct AF G rx ex P' A C"
  apply atomize
  apply (clarsimp simp: ac_corres_def)
  done

(*
 * Rules to use the corresXF definitions.
 *)

lemma corresXF_modify_local:
  "[ ∧s. st s = st (M s); ∧s. P s ==> ret () (M s) = x ]
      ==> corresXF st ret ex P (return x) (modify M)"
  by (auto simp add: corresXF_def)

lemma corresXF_modify_global:
  "[ ∧s. P s ==> M (st s) = st (M' s) ] ==>
     corresXF st ret ex P (modify M) (modify M')"
  by (auto simp add: corresXF_def)

lemma corresXF_select_modify:
  "[ ∧s. P s ==> st s = st (M s); ∧s. P s ==> ret () (M s) ∈ x ] ==>
     corresXF st ret ex P (select x) (modify M)"
  by (auto simp add: corresXF_def)

lemma corresXF_select_select:
  "[ ∧s a. st s = st (M (a::('a ==> ('a::{type}))) s);
         ∧s x. [ P s; x ∈ b] ==> ret x s ∈ a ] ==>
     corresXF st ret ex P (select a) (select b)"
  by (auto simp add: corresXF_def)

lemma corresXF_modify_gets:
  "[ ∧s. P s ==> st s = st (M s); ∧s. P s ==> ret () (M s) = f (st (M s)) ] ==>
     corresXF st ret ex P (gets f) (modify M)"
  by (auto simp add: corresXF_def)


lemma corresXF_guard:
  "[ ∧s. P s ==> G' s = G (st s) ] ==> corresXF st ret ex P (guard G) (guard G')"
  by (auto simp add: corresXF_def)

lemma corresXF_fail:
  "corresXF st return_xf exception_xf P fail X"
  by (auto simp add: corresXF_def)

lemma corresXF_spec:
  "[ ∧s s'. ((s, s') ∈ A') = ((st s, st s') ∈ A); surj st ]
    ==> corresXF st ret ex P (state_select A) (state_select A')"
  apply (clarsimp simp add: corresXF_def)
  apply (frule_tac y=undefined in surjD)
  apply (clarsimp simp: image_def set_eq_UNIV)
  apply metis
  done

lemma corresXF_throw:
  "[ ∧s. P s ==> E B s = A ] ==> corresXF st V E P (throw A) (throw B)"
  by (auto simp add: corresXF_def Exn_def)


lemma corresXF_append_gets_abs:
  assumes corres: "corresXF st ret ex P L R"
  and consistent: "∧s. P s ==> R ∙ s ?{λr s. case r of Exn _ ==> ⊤ | Result v ==> M (ret v s) (st s) = ret' v s }"
shows "corresXF st ret' ex P (L >>= (λr. gets (M r))) R"
  using corres consistent
  apply (clarsimp simp add: corresXF_refines_iff runs_to_partial_def_old refines_def_old 
      succeeds_bind reaches_bind rel_XF_def rel_xval.simps split: xval_splits )
  using Exn_def by force

lemma corresXF_skipE:
  "corresXF st ret ex P skip skip"
  by (auto simp add: corresXF_def Exn_def)


lemma corresXF_id:
    "corresXF id (λr s. r) (λr s. r) P M M"
  by (fastforce simp: corresXF_def split: xval_splits)

lemma corresXF_cong:
  "[ ∧s. st s = st' s;
     ∧s r. ret_xf r s = ret_xf' r s;
     ∧s r. ex_xf r s = ex_xf' r s;
     ∧s. P s = P' s;
     ∧s s'. P' s' ==> run A s = run A' s;
     ∧s. P' s ==> run C s = run C' s ] ==>
           corresXF st ret_xf ex_xf P A C = corresXF st' ret_xf' ex_xf' P' A' C'"
   apply atomize
   apply (auto simp: corresXF_def reaches_def succeeds_def split: xval_splits)
   done

lemma corresXF_exec_abs_select:
  "[ x ∈ Q; x ∈ Q ==> corresXF id rx ex P (A x) A' ] ==> corresXF id rx ex P (select Q >>= A) A'"
  by (fastforce simp add: corresXF_def succeeds_bind reaches_bind split: xval_splits)

end