Quelle  L2Defs.thy   Sprache: Isabelle

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

chapter ‹L2 phase: local variable abstraction with lambdas›

theory L2Defs
imports CorresXF L1Defs L1Peephole L1Valid
begin

type_synonym ('s, 'a, 'e) L2_monad = "('e, 'a, 's) exn_monad"

definition "L2_unknown (ns :: nat list) ≡ select UNIV :: ('s, 'a, 'e) L2_monad"
definition "L2_seq (A :: ('s, 'a, 'e) L2_monad) (B :: 'a → ('s, 'b, 'e) L2_monad) ≡ (A >>= B) :: ('s, 'b, 'e) L2_monad"
definition "L2_modify m ≡modify m :: ('s, unit, 'e) L2_monad"
definition "L2_gets f (names :: nat list) ≡ gets f :: ('s, 'a, 'e) L2_monad"
definition "L2_condition c (A :: ('s, 'a, 'e) L2_monad) (B :: ('s, 'a, 'e) L2_monad) ≡ condition c A B"
definition "L2_catch (A :: ('s, 'a, 'e) L2_monad) (B :: 'e → ('s, 'a, 'ee) L2_monad) ≡ (A <catch> B)"
definition "L2_try (A :: ('s, 'a, 'e + 'a) L2_monad) ≡ try A"
definition "L2_while c (A :: 'a → ('s, 'a, 'e) L2_monad) i (ns :: nat list) ≡ whileLoop c A i :: ('s, 'a, 'e) L2_monad"
definition "L2_throw x (ns :: nat list) ≡ throw x :: ('s, 'a, 'e) L2_monad"
definition "L2_spec r ≡ (state_select r >>= (λ_. select UNIV)) :: ('s, 'a, 'e) L2_monad"
definition "L2_assume r ≡ (assume_result_and_state r) :: ('s, 'a, 'e) L2_monad"
definition "L2_guard c ≡ (guard c) :: ('s, unit, 'e) L2_monad"
definition "L2_guarded P c ≡ L2_seq (L2_guard P) (λ_. c)" ―‹used to guard a function-pointer call›
definition "L2_fail ≡ fail :: ('s, 'a, 'e) L2_monad"
definition "L2_call x emb (ns :: nat list) ≡ map_value (map_exn emb) x :: ('s, 'a, 'e) L2_monad"

abbreviation "L2_skip ≡ L2_gets (λ_. ()) []"
definition "L2_VARS f (names::nat list) ≡ f" ― ‹Auxilliary construct to preserve names,
 like in @{const L2_unknown}, @{const L2_gets}, ...›

abbreviation "L2_pre_post P R ≡ L2_guarded (λ_. P) (L2_assume R)"
abbreviation "L2_pre_post_read_write r w Pre Post ≡
  L2_guarded (λ_. Pre)
  (L2_assume (λs. {(v, s'). ∃t'. (v, t') ∈ Post (r s) ∧ s' = w (λ_. t') s}))"

definition gets_theE :: "('s → 'a option) → ('e, 'a, 's) exn_monad" where 
  "gets_theE ≡ λx. gets_the x" ― ‹Lifting into exception monad›

(*
 * Temporary constructions, used internally but not emitted.
 *
 * "L2_folded_gets" is like "L2_gets", but the peephole optimiser will
 * try to eliminate the call to where it is used, eliminating it where
 * possible.  It is used for automatically generated "L2_gets" calls
 * which the user really doesn't need to know about.
 *
 * The various "call" defintions are to help generate proofs for the
 * different ways of making function calls, which are hard to unify.
 *)
definition "L2_folded_gets f names ≡ L2_gets f names :: ('s, 'a, 'e) L2_monad"
definition "L2_voidcall x emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_skip) :: ('s, unit, 'e) L2_monad"
definition "L2_modifycall x m emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_modify (m ret)) :: ('s, unit, 'e) L2_monad"
definition "L2_returncall x f emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_folded_gets (f ret) []) :: ('s, 'a, 'e) L2_monad"


(* Syntax variants to emulate congprocs with simprocs *)
definition "L2_seq_guard P A ≡ L2_seq (L2_guard P) A"
definition "L2_seq_gets c n A ≡ L2_seq (L2_gets (λ_. c) n) A" 
definition "L2_seq_unknown ns A ≡ L2_seq (L2_unknown ns) A"
definition "L2_seq_condition c L R X ≡ L2_seq (L2_condition c L R) X"

definition L2_exec_spec_monad:: 
  "('s → 't) → (exit_status, 'a, 't) exn_monad → (exit_status c_exntype, 'a, 's) exn_monad" where 
  "L2_exec_spec_monad st f ≡
     map_value (map_exn Nonlocal) (exec_abstract st f)"

definition "SANITIZE_NAMES prj ns ns' = True"

lemma sanitize_namesI: "SANITIZE_NAMES prj ns ns'"
  by (simp add: SANITIZE_NAMES_def)

lemma L2_fail_top: "L2_fail = ⊤"
  by (simp add: L2_fail_def top_eq_fail)

definition DYN_CALL :: "prop → prop" where "PROP DYN_CALL (PROP P) ≡ PROP P"

lemma DYN_CALL_I: "PROP P ==> PROP DYN_CALL (PROP P)"
  by (simp add: DYN_CALL_def)

lemma DYN_CALL_D: "PROP DYN_CALL (PROP P) ==> PROP P"
  by (simp add: DYN_CALL_def)

lemma mono_L2_VARS[monad_mono_intros]: "f ≤ g ==> L2_VARS f ns ≤ L2_VARS g ns"
  unfolding L2_VARS_def .

lemma mono_L2_VARS'[monad_mono_intros]: "f p ≤ g p ==> L2_VARS f ns p ≤ L2_VARS g ns p"
  unfolding L2_VARS_def .

lemma admissible_runs_to_partial[corres_admissible]: "ccpo.admissible Inf (≥) (λf . f ∙ s ?{Q})"
  unfolding runs_to_partial_def_old 
  apply (rule ccpo.admissibleI)
    apply (clarsimp simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits xval_splits)
    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.distinct(1))
    done

lemma reaches_gets_theE [simp]:
     "reaches (gets_theE M) s rv s' ⟷ (∃v'. rv = Result v' ∧ s' = s ∧ M s = Some v')"
  by (auto simp add: gets_theE_def)


lemma seucceeds_gets_theE [simp]:
     "succeeds (gets_theE M) s = (∃v. M s = Some v)"
  apply (auto simp add: gets_theE_def)
  done

lemma L2_folded_gets_bind:
  "L2_seq (L2_folded_gets (λ_. x) ns) f = f x"
  unfolding L2_seq_def L2_folded_gets_def L2_gets_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done


lemma L2_call_throw_names: "L2_call x emb ns = (x <catch> (λr. L2_throw (emb r) ns))"
  unfolding L2_call_def L2_throw_def
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (auto simp add: runs_to_def_old map_exn_def split: xval_splits)
  done

(* fixme: we can merge these *)
lemmas L2_remove_scaffolding_1 =
  L2_folded_gets_bind [THEN eq_reflection]
  L2_returncall_def
  L2_modifycall_def
  L2_voidcall_def

lemmas L2_remove_scaffolding_2 =
  L2_remove_scaffolding_1
  L2_folded_gets_def

abbreviation (input) "L2_guarded_while G C B i n ≡ L2_seq (L2_guard (G i))
               (λ_. L2_while C (λi. L2_seq (B i) (λr. L2_seq (L2_guard (G r)) (λ_. L2_gets (λ_. r) n))) i n)"

lemmas L2_defs = L2_unknown_def L2_seq_def
    L2_modify_def L2_gets_def L2_condition_def L2_catch_def L2_while_def
    L2_throw_def L2_spec_def L2_assume_def L2_guard_def L2_fail_def L2_folded_gets_def
    L2_voidcall_def L2_modifycall_def L2_returncall_def 
    L2_try_def

(* Alternate definitions. *)
lemma L2_defs':
   "L2_unknown n ≡ unknown"
   "L2_seq A' B' ≡ A' >>= B'"
   "L2_modify m ≡ modify m"
   "L2_gets f n ≡ gets f"
   "L2_condition c L R ≡ condition c L R"
   "L2_catch A B ≡ (A <catch> B)"
   "L2_try A ≡ try A"
   "L2_while c' B'' i n ≡ whileLoop c' B'' i"
   "L2_throw x n ≡ throw x"
   "L2_spec r ≡ (state_select r >>= (λ_. select UNIV))"
   "L2_assume r' ≡ (assume_result_and_state r')"
   "L2_guard c ≡ guard c"
   "L2_fail ≡ fail"
  by (auto simp: (*monad_defs*) L2_defs unknown_def )


definition
   L2corres :: "('s → 't) → ('s → 'r) → ('s → 'e) → ('s → bool)
       → ('e, 'r, 't) exn_monad → (unit, unit, 's) exn_monad → bool"
where
  "L2corres st ret_xf ex_xf P A C
       ≡ corresXF st (λ_. ret_xf) (λ_. ex_xf) P A C"

lemma admissible_nondet_ord_L2corres [corres_admissible]:
  "ccpo.admissible Inf (≥) (λA. L2corres st ret_xf ex_xf P A C)"
  unfolding L2corres_def
  apply (rule admissible_nondet_ord_corresXF)
  done

lemma admissible_nondet_ord_L2corres_mcont:
  "mcont Inf (≥) Inf (≥) F ==> ccpo.admissible Inf (≥) (λA. L2corres st ret_xf ex_xf P (F A) C)"
  using admissible_nondet_ord_L2corres
  apply (rule admissible_subst)
  apply assumption
  done


lemma L2corres_top [corres_top]: "L2corres st ret_xf ex_xf P ⊤ C"
  by (auto simp add: L2corres_def corresXF_def)

lemma L2corres_le_trans [corres_le_trans]:
  "L2corres st ret_xf ex_xf P A C ==> A ≤ A' ==> L2corres st ret_xf ex_xf P A' C"
  by (auto simp add: L2corres_def corres_le_trans)

(* Wrapper for calling un-translated functions. *)

definition
  "L2_call_L1 arg_xf gs ret_xf l1body
    = do {
        s ← get_state;
        t ← select {t. gs t = s ∧ arg_xf t};
        run_bind l1body t (λr' t'.
          (case r' of
             Exception _ → fail
           | Result _ → do {set_state (gs t'); return (ret_xf t')} ))
    }"


lemma L2corres_L2_call_L1:
  "L2corres gs ret_xf ex_xf arg_xf
     (L2_call_L1 arg_xf gs ret_xf f) f"
  apply (clarsimp simp: L2corres_def corresXF_refines_iff L2_call_L1_def L1_seq_def L1_guard_def
                 split: xval_splits)
  apply (simp add: refines_def_old)
  apply (intro conjI impI)
  subgoal
    by (auto simp add: succeeds_bind succeeds_run_bind succeeds_exec_concrete_iff succeeds_catch)
  subgoal
    by (auto simp add: succeeds_bind succeeds_run_bind reaches_run_bind  
        succeeds_exec_concrete_iff succeeds_catch reaches_bind default_option_def Exn_def
        rel_XF_def rel_xval.simps Exn_def default_option_def
          split: exception_or_result_splits)

       (smt (verit, ccfv_threshold) Exn_def Exn_neq_Result exception_or_result_cases 
        imageI mem_Collect_eq old.unit.exhaust option.exhaust_sel)
  done


lemma L2corres_L2_call_simpl:
  "l1_f ≡ simpl_f ==>
   L2corres gs ret_xf ex_xf arg_xf
     (L2_call_L1 arg_xf gs ret_xf simpl_f) l1_f"
  by (simp add: L2corres_L2_call_L1)

(* shouldn't be needed
lemma empty_set_exists: "(\<forall>a. a \<noteq> {}) = False"
  apply blast
  done
*)

lemma L2corres_modify_global:
  "[ ∧s. P s ==> M (st s) = st (M' s) ] ==>
     L2corres st ret ex P (L2_modify M) (L1_modify M')"
  unfolding L2_defs L1_defs
  by (auto simp add: L2corres_def corresXF_modify_global)


lemma L2corres_modify_unknown:
  "[ ∧s. P s ==> st s = st (M s) ] ==>
     L2corres st ret ex P (L2_unknown ns) (L1_modify M)"
  apply (clarsimp simp: L2corres_def L2_defs L1_defs)
  apply (auto intro: corresXF_select_modify)
  done

lemma L2corres_spec_unknown:
  "[ ∧s a. st s = st (M (a::('a → ('a::{type}))) s) ] ==>
     L2corres st ret ex P (L2_unknown ns) (L1_init M)"
  apply (auto simp add: L2corres_def corresXF_def L1_defs L2_defs 
      reaches_bind reaches_succeeds succeeds_bind)
  done

lemma L2corres_modify_gets:
  "[ ∧s. P s ==> st s = st (M s); ∧s. P s ==> ret (M s) = f (st s) ] ==>
         L2corres st ret ex P (L2_gets (λs. f s) n) (L1_modify M)"
  by (simp add: L2corres_def L2_defs L1_defs corresXF_modify_gets)

lemma L2corres_gets_skip:
  "L2corres st ret ex P L2_skip L1_skip"
  by (simp add: L2corres_def L2_defs L1_defs corresXF_def)

lemma L2corres_guard:
  "[ ∧s. P s ==> G' s = G (st s) ] ==>
  L2corres st return_xf exception_xf P (L2_guard G) (L1_guard G')"
  by (simp add: L2corres_def L2_defs L1_defs corresXF_guard)


lemma L2corres_fail:
  "L2corres st return_xf exception_xf P L2_fail X"
  by (clarsimp simp add: L2corres_def L1_defs L2_defs corresXF_def)


lemma L2corres_spec:
  "[ ∧s s'. ((s, s') ∈ A') = ((st s, st s') ∈ A); surj st ]
    ==> L2corres st return_xf exception_xf P (L2_spec A) (L1_spec A')"
  apply (clarsimp simp: L2corres_def L2_defs L1_spec_def corresXF_def succeeds_bind reaches_bind)
  by (metis surjD)


lemma L2corres_assume:
  "[ ∧s s'. (((), s') ∈ A' s) = (((), st s') ∈ A (st s)) ]
    ==> L2corres st return_xf exception_xf P (L2_assume A) (L1_assume A')"
  by (clarsimp simp: L2corres_def L2_defs L1_assume_def corresXF_def)

lemma L2corres_seq:
  "[ L2corres st return_xf exception_xf P A A';
     ∧x. L2corres st return_xf' exception_xf (P' x) (B x) B';
     {R} A' {λ_ s. P' (return_xf s) s}, {λ_ _. True};
     ∧s. R s ==> P s ] ==>
     L2corres st return_xf' exception_xf R (L2_seq A B) (L1_seq A' B')"
  apply (unfold L2corres_def L2_seq_def L1_seq_def validE_def)
  apply (rule corresXF_join)
     apply assumption
    apply assumption
   apply simp
  apply assumption
  done

lemma L2corres_guard_imp:
  "[ L2corres st ret_state ex_state Q M M'; pred_imp P Q ] ==>
  L2corres st ret_state ex_state P M M'"
  by (simp add: L2corres_def pred_imp_def corresXF_guard_imp)


lemma L2corres_guarded'': 
  assumes bdy: "∧s' s. g' s' ==> s = st s' ==> P s' ==> L2corres st ret ex P (c (dest s)) (c' (dest' s'))" 
  assumes g_g': "∧s'. P s' ==> g' s' = g (st s')"
  assumes dest: "∧s' s. g' s' ==> s = st s' ==> P s' ==> dest' s' = dest (st s')"
  shows "L2corres st ret ex P (L2_guarded g (L2_seq (L2_gets dest []) c)) (L1_guarded g' (gets dest' ⤜ c'))"
  using assms
  by (auto simp add: L2corres_def L2_defs L1_defs L2_guarded_def L1_guarded_def corresXF_def
      succeeds_bind reaches_bind  split: xval_splits)

lemma L2corres_guarded_impl'': 
  assumes bdy: "∧s' s. g s ==> s = st s' ==> P s' ==> L2corres st ret ex P (c (dest s)) (c' (dest' s'))" 
  assumes g_g': "∧s'. P s' ==> g (st s') ==> g' s'"
  assumes dest: "∧s' s. g' s' ==> s = st s' ==> P s' ==> dest' s' = dest (st s')"
  shows "L2corres st ret ex P (L2_guarded g (L2_seq (L2_gets dest ns) c)) (L1_guarded g' (gets dest' ⤜ c'))"
  using assms
  by (auto simp add: L2corres_def L2_defs L1_defs L2_guarded_def L1_guarded_def corresXF_def
      succeeds_bind reaches_bind  split: xval_splits)

lemma L2corres_guarded: 
  assumes bdy: "∧s' s. g' s' ==> s = st s' ==> P s' ==> L2corres st ret ex P c c'" 
  assumes g_g': "∧s'. P s' ==> g' s' = g (st s')"
  shows "L2corres st ret ex P (L2_guarded g c) (L1_guarded g' c')"
  using assms
  apply (fastforce simp add: L2corres_def L2_defs L1_defs L2_guarded_def L1_guarded_def corresXF_def
      succeeds_bind reaches_bind  split: xval_splits)
  done

lemma L2corres_guarded_impl: 
  assumes bdy: "∧s' s. g s ==> s = st s' ==> P s' ==> L2corres st ret ex P c c'" 
  assumes g_g': "∧s'. P s' ==> g (st s') ==> g' s'"
  shows "L2corres st ret ex P (L2_guarded g c) (L1_guarded g' c')"
  using assms
  apply (fastforce simp add: L2corres_def L2_defs L1_defs L2_guarded_def L1_guarded_def corresXF_def
      succeeds_bind reaches_bind  split: xval_splits)
  done


lemma L2corres_catch:
  "[ L2corres st V E P L L';
    ∧x. L2corres st V E' (P' x) (R x) R';
    {Q} L' {λ_ _. True}, {λ_ s. P' (E s) s}; ∧s. Q s ==> P s ] ==>
   L2corres st V E' Q (L2_catch L R) (L1_catch L' R')"
  apply (clarsimp simp: L2corres_def L2_catch_def L1_catch_def validE_def)
  apply (rule corresXF_except)
     apply (assumption)
    apply (assumption)
   apply auto
  done

lemma L2corres_throw:
  "[ ∧s. P s ==> E s = A ] ==> L2corres st V E P (L2_throw A n) (L1_throw)"
  by (clarsimp simp: L2corres_def L2_throw_def L1_throw_def corresXF_throw)

lemma L2corres_conseq: 
  assumes corres: "L2corres st return_xf exception_xf P C C'"
  assumes conseq: "∧s. Q s ==> P s"
  shows "L2corres st return_xf exception_xf Q C C'"
  apply (rule L2corres_guard_imp [OF corres])
  using conseq by (simp add: pred_imp_def)

lemma L2corres_cond:
  "[ L2corres st return_xf exception_xf P A A';
     L2corres st return_xf exception_xf P' B B';
     ∧s. R s ==> P s;
     ∧s. R s ==> P' s;
     ∧s. R s ==> c' s = c (st s) ] ==>
     L2corres st return_xf exception_xf R (L2_condition c A B) (L1_condition c' A' B')"
  apply (unfold L2corres_def L2_condition_def L1_condition_def)
  apply (rule corresXF_cond)
    apply (auto intro:  corresXF_guard_imp)
  done

lemma L2corres_inject_return:
  "[ L2corres st V E P L R; {P'} R {λ_ s. W (V s) = V' s}, { λ_ _. True }; ∧s. P' s ==> P s] ==>
     L2corres st V' E P' (L2_seq L (λx. L2_gets (λ_. W x) n)) R"
  apply (clarsimp simp: L2corres_def validE_def)
  apply (drule corresXF_guard_imp [where P=P'], simp)
  apply (unfold L2_seq_def L2_gets_def)
  apply (rule corresXF_guard_imp)
  apply (erule corresXF_append_gets_abs)
    apply simp
  apply simp
  done

lemma L2corres_inject_return':
  "[ L2corres st V E P L R;Gets = (λx. L2_gets (λ_. W x) n);{P'} R {λ_ s. W (V s) = V' s}, { λ_ _. True}; ∧s. P' s ==> P s
  ] ==>
  L2corres st V' E P' (L2_seq L Gets) R"
  by (auto intro:  L2corres_inject_return)

lemma L2corres_skip:
  "L2corres st return_xf exception_xf P L2_skip L1_skip"
  by (rule L2corres_gets_skip)

lemma L2corres_while:
  assumes body_corres: "∧x. L2corres st ret ex (P' x) (A x) B"
  and inv_holds:  "{λs. P (ret s) s } B {λ_ s. P (ret s) s }, {λ_ _. True}"
  and cond_match: "∧s. P (ret s) s ==> c' s = c (ret s) (st s)"
  and pred_imply: "∧s x. P x s ==> P' x s"
  and pred_extract: "∧s. P x s ==> ret s = x"
  and pred_imply2: "∧s. Q x s ==> P x s"
  shows "L2corres st ret ex (Q x) (L2_while c A x n) (L1_while c' B)"
  apply (clarsimp simp: L2corres_def L2_while_def L1_while_def)
  apply (rule corresXF_guard_imp)
  apply (rule corresXF_while [
         where P="λr s. P (ret s) s" and C'=c and C="λ_. c'" and A=A and B="λ_. B"
         and ret="λr s. ret s" and ex="λr s. ex s" and st=st and y=x and x="()" and P'="λr s. Q x s"])
       apply (rule corresXF_guard_imp)
        apply (rule body_corres [unfolded L2corres_def])
       apply (clarsimp simp: pred_imply)
      apply (clarsimp simp: cond_match)
     apply (rule inv_holds [unfolded validE_def, rule_format])
     apply assumption
    apply (metis pred_extract pred_imply2)
   apply (metis pred_extract pred_imply2)
  apply simp
  done

 
lemma L2corres_returncall:
  "[ L2corres st ret' ex' P' Z dest_fn;
     ∧s. P s ==> P' (scope_setup s);
     ∧t s. st (return_xf t (scope_teardown s t)) = st t;
     ∧t s. st (result_exn (scope_teardown s t) t) = st t;
     ∧s. st (scope_setup s) = st s;
     ∧t s. st (scope_teardown s t) = st t;
     ∧t s. P s ==> ret (return_xf t (scope_teardown s t)) = F (ret' t) (st t) ;
     ∧t s. P s ==> (ex (result_exn (scope_teardown s t) t)) = emb (ex' t) ] ==>
     L2corres st ret ex P (L2_returncall Z F emb ns)
   (L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
  unfolding L1_call_def L1_seq_def L1_throw_def L2_returncall_def L2_call_def L2corres_def L2_defs
  apply (rule corresXF_I)
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis Exn_def Exn_neq_Result[of _ "ret' _"] Result_eq_Result[of "ret' _"]
        map_exn_simps(2)[of emb "ret' _"])
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
  subgoal
    apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    done
  done


lemma L2corres_dest_fn_simp: 
  assumes dest_fn: "∧s. P s ==> dest_fn = dest_fn'"
  assumes corres: "L2corres st ret ex P X
   (L1_call scope_setup (measure_call dest_fn') scope_teardown result_exn return_xf)"
  shows "L2corres st ret ex P X
   (L1_call scope_setup (measure_call dest_fn) scope_teardown result_exn return_xf)"
  using corres dest_fn unfolding L2corres_def corresXF_def 
  by blast


lemma L2corres_l2_propagate_fixed_cong: 
"(∧s. P s = P' s) ==> (∧s. P' s ==> A = A') ==> L2corres st ret ex P A C = L2corres st ret ex P' A' C"
  unfolding L2corres_def corresXF_def simp_implies_def
  by (auto split: sum.splits prod.splits) 

lemma L2corres_l2_propagate_fixed_cong': 
"P = P' ==> (∧s. P' s ==> A = A') ==> (∧s. P' s ==> C = C') ==> L2corres st ret ex P A C = L2corres st ret ex P' A' C'"
  unfolding L2corres_def corresXF_def simp_implies_def
  by (auto split: sum.splits prod.splits) 

lemma L2corres_l2_propagate_fixed_cong'': 
"P = P' ==> (A = A') ==> (C = C') ==> L2corres st ret ex P A C = L2corres st ret ex P' A' C'"
  unfolding L2corres_def corresXF_def simp_implies_def
  by (auto split: sum.splits prod.splits) 

lemma L2corres_modifycall:
  "[ L2corres st ret' ex' P' Z dest_fn;
     ∧s. P s ==> P' (scope_setup s);
     ∧s r. P r ==> F (ret' s) (st s) = st (return_xf s (scope_teardown r s));
     ∧s. st (scope_setup s) = st s;
     ∧t s. st (scope_teardown s t) = st t;
     ∧t s. st (result_exn (scope_teardown s t) t) = st t;
     ∧t s. P s ==> ex (result_exn (scope_teardown s t) t) = emb (ex' t)] ==>
     L2corres st ret ex P (L2_modifycall Z F emb ns)
                          (L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
  apply (clarsimp simp: L1_call_def L1_seq_def L1_throw_def L2_call_def L2_defs L2corres_def)
  apply (rule corresXF_I)
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis Exn_def Exn_neq_Result[of _ "ret' _"] Result_eq_Result[of "ret' _"]
        map_exn_simps(2)[of emb "ret' _"])
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
  subgoal
    apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    done
  done


lemma L2corres_voidcall:
  "[ L2corres st ret' ex' P' Z dest_fn;
     ∧s. P s ==> P' (scope_setup s);
     ∧s r. st (return_xf s (scope_teardown r s)) = st s;
     ∧s. st (scope_setup s) = st s;
     ∧t s. st (scope_teardown s t) = st t;
     ∧t s. st (result_exn (scope_teardown s t) t) = st t;
     ∧t s. P s ==> ex (result_exn (scope_teardown s t) t) = emb (ex' t)] ==>
     L2corres st ret ex P (L2_voidcall Z emb ns)
         (L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
  apply (unfold L2_voidcall_def)
  apply (rule subst[where t = "L2_skip" and s = "L2_modify (λs. s)"])
  subgoal
    apply (simp add: L2_defs)
    apply (rule spec_monad_ext)
    apply simp
    done
  apply (fold L2_modifycall_def L2corres_def)
  apply (fastforce elim!: L2corres_modifycall)
  done


lemma L2corres_call:
  "[ L2corres st ret' ex' P' Z dest_fn;
     ∧s. P s ==> P' (scope_setup s);
     ∧s r. st (return_xf s (scope_teardown r s)) = st s;
     ∧s r. ret (return_xf s (scope_teardown r s)) = ret' s;
     ∧s. st (scope_setup s) = st s;
     ∧t s. st (scope_teardown s t) = st t;
     ∧t s. st (result_exn (scope_teardown s t) t) = st t;
     ∧t s. P s ==> ex (result_exn (scope_teardown s t) t) = emb (ex' t) ] ==>
     L2corres st ret ex P (L2_call Z emb ns)
                          (L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
  apply (clarsimp simp: L2corres_def L2_call_def L1_call_def L1_seq_def L1_throw_def L2_defs)
  apply (rule corresXF_I)
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis map_exn_simps(2)[of emb "ret' _"])
  subgoal
    apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
  subgoal
    apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch 
        reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
    done
  done

lemma (in L1_functions) L2corres_dyn_call:
"L2corres st ret ex P X
   (L1_guarded g (gets dest >>= (λp. L1_call scope_setup (P p) scope_teardown result_exn return_xf))) ==>
 L2corres st ret ex P X (L1_dyn_call g scope_setup dest scope_teardown result_exn return_xf)"
  by (simp add: L1_dyn_call_def)


lemma L2corres_le_trans':
  "L2corres st ret_xf ex_xf P A C' ==> C ≤ C' ==> L2corres st ret_xf ex_xf P A C"
  by (auto simp add: L2corres_def corresXF_trans')

lemma L2corres_call_simpl:
  assumes L1: "L1corres ct Γ p' (Call p)"
  assumes L2: "L2corres st ret ex P X p'"
  shows "L2corres st ret ex P X (L1_call_simpl ct Γ p)"
proof - 
  from L1_call_simpl_le_trans [OF L1] have "L1_call_simpl ct Γ p ≤ p'" .
  from L2corres_le_trans' [OF L2 this] show ?thesis .
qed

term list_all2

lemma L2corres_map_of_default: 
  assumes "list_all2 (λ(p, f) (p', f'). (p = p'∧ L2corres st ret ex P f' (L1_call scope_setup f scope_teardown result_exn result_xf))) ps ps'"
  shows "L2corres st ret ex P
    (map_of_default (λ_. ⊤) ps' p) (L1_call scope_setup
    (map_of_default (λ_. ⊤) ps p) scope_teardown result_exn result_xf)"
  using assms proof (induct ps arbitrary: ps')
  case Nil
  then show ?case by (auto simp add: L2corres_top)
next
  case (Cons x1 ps)
  then show ?case 
    apply (cases ps')
     apply (auto split: )
    done
qed

lemma map_value_Nonlocal_assume_result_and_state: 
  "map_value (map_exn Nonlocal) (assume_result_and_state r) = assume_result_and_state r"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma exec_abstract_id: "exec_abstract id f = f"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2corres_exec_spec_monad:
  assumes x: "lense get_x upd_x"
  assumes glbls_upd_x_commute: "∧f s. glbls (upd_x f s) = glbls s"
  assumes res[simp]: "∧f s. get_res (upd_res f s) = f (get_res s)"
  assumes res_commute: "∧f s. get_res (upd_x f s) = get_res s" "∧f s. glbls (upd_res f s) = glbls s" 
  assumes f: "∧s. P s ==> refines (f (args s)) g (st (glbls s)) (st (glbls s)) (=)" 
  shows "L2corres glbls get_res get_x P (L2_exec_spec_monad st g) (L1_exec_spec_monad upd_x (st o glbls) args f upd_res)"
proof -
  from x interpret lense_x: lense get_x upd_x .

  show ?thesis 
  proof (clarsimp simp add: L2corres_def corresXF_refines_iff rel_XF_def)
    fix s
    assume P:  "P s" 
    show "refines (L1_exec_spec_monad upd_x (st ∘ glbls) args f upd_res) (L2_exec_spec_monad st g) s (glbls s)
          (λ(r, t) (r', t').
              t' = glbls t ∧ rel_xval (λe e'. e' = get_x t) (λv v'. v' = get_res t) r r')"

      apply (simp add: L1_exec_spec_monad_def L2_exec_spec_monad_def)
      using f [OF P]
      apply (auto simp add: refines_def_old succeeds_bind reaches_bind succeeds_bind_handle reaches_bind_handle 
          L1_seq_def L1_modify_def L1_throw_def default_option_def map_exn_def  
          reaches_exec_abstract reaches_map_value rel_xval.simps split: xval_splits exception_or_result_splits)

  
      subgoal for r s' r' s1'
        apply (cases r')
        subgoal    
          apply (auto simp add: default_option_def Exn_def)   
          using glbls_upd_x_commute 
          by (metis Exn_def Exn_neq_Result the_Exn_Exn(2))
        subgoal
          apply (auto simp add: glbls_upd_x_commute res_commute) 
          by (metis Exn_neq_Result the_Result_simp)
        done
      done
  qed
qed



lemma L2corres_exec_spec_monad_globals:
  assumes x: "lense get_x upd_x"
  assumes glbls_upd_x_commute: "∧f s. glbls (upd_x f s) = glbls s" 
  assumes res[simp]: "∧f s. get_res (upd_res f s) = f (get_res s)"
  assumes res_commute: "∧f s. get_res (upd_x f s) = get_res s" "∧f s. glbls (upd_res f s) = glbls s" 
  assumes f: "∧s. P s ==> refines (f (args s)) g (glbls s) (glbls s) (=)" 
  shows "L2corres glbls get_res get_x P (L2_exec_spec_monad id g) (L1_exec_spec_monad upd_x (glbls) args f upd_res)"
  using x glbls_upd_x_commute res res_commute 
  apply (rule L2corres_exec_spec_monad [where st=id, simplified])
  by (rule f)

lemma lense_global_exn_var: "lense global_exn_var'_' global_exn_var'_'_update"
  by (unfold_locales) auto
lemmas L1corres_exec_spec_monad' = L1corres_exec_spec_monad [OF lense_global_exn_var]

lemma globals_global_exn_var_commutes: "globals (global_exn_var'_'_update f s) = globals s"
  by simp

lemmas L2corres_exec_spec_monad' = 
  L2corres_exec_spec_monad [where glbls = globals, OF lense_global_exn_var globals_global_exn_var_commutes]
lemmas L2corres_exec_spec_monad_globals' = 
  L2corres_exec_spec_monad_globals [where glbls = globals, OF lense_global_exn_var globals_global_exn_var_commutes]

lemma L2_gets_bind: "[ ∧s s'. V s = V s' ] ==> L2_seq (L2_gets V n) f = f (V undefined)"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (simp add: runs_to_iff)
  by (auto simp add: runs_to_def_old) metis+


(* TODO: remove internal var if it is not user-visible *)
lemma L2corres_folded_gets:
  "[ ∧a. L2corres st ret ex (P and (λs. a = c (st s))) (X a) Y ] ==>
     L2corres st ret ex P (L2_seq (L2_folded_gets c ns) X) Y"
  by (fastforce simp add: L2_defs L2corres_def corresXF_def succeeds_bind reaches_bind split: xval_splits) 
 
lemma L2_call_cong [fundef_cong, cong]:
  "f = f' ==> L2_call f = L2_call f'"
  by simp

lemma L2_call_liftE [simp]:
  "L2_call (liftE x) emb ns ≡ liftE x"
  by (clarsimp simp add: L2_call_def)

lemma L2_call_fail [simp]: "L2_call fail emb ns = fail"
  apply (simp add: L2_call_def)
  done


lemma L2_call_L2_gets [simp]: "L2_call (L2_gets x n) emb ns = L2_gets x n"
  apply (simp add: L2_defs L2_call_def)
  done


(*
 * Rules for adjusting case_prod statements after transformations.
 *
 * c.f. fix_L2_while_loop_splits_conv
 *)
lemma L2_split_fixup_1:
  "(L2_seq A (λx. case y of (a, b) → B a b x)) =
           (case y of (a, b) → L2_seq A (λx. B a b x))"
       by (auto simp: split_def)
lemma L2_split_fixup_2:
  "(L2_seq (case y of (a, b) → B a b) A) =
           (case y of (a, b) → L2_seq (B a b) A)"
  by (auto simp: split_def)

lemma L2_split_L2_seq_fixup_both:
  "(L2_seq (case y of (a,b) → A a b) (case y of (a, b) → B a b)) =
           (case y of (a, b) → L2_seq (A a b) (B a b))"
  by (auto simp: split_def)

lemma L2_split_L2_seq_gets_fixup_1:
  "(L2_seq_gets (case y of (a,b) → A a b) n (case y of (a, b) → B a b)) =
           (case y of (a, b) → L2_seq_gets (A a b) n (B a b))"
  by (auto simp: split_def)
(*
lemma L2_split_L2_seq_gets_fixup_1:
  "(L2_seq_gets A n (\<lambda>x. case y of (a, b) \<Rightarrow> B a b x)) =
           (case y of (a, b) \<Rightarrow> L2_seq_gets A n (\<lambda>x. B a b x))"
  by (auto simp: split_def)

lemma L2_split_L2_seq_gets_fixup_2:
  "(L2_seq_gets (case y of (a, b) \<Rightarrow> B a b) n A) =
           (case y of (a, b) \<Rightarrow> L2_seq_gets (B a b) n  A)"
  by (auto simp: split_def)
*)
lemma L2_split_fixup_3:
  "(case (x, y) of (a, b) → P a b) = P x y"
       by (auto simp: split_def)
lemma L2_split_fixup_4:
  "case_prod (λa (b :: 'a × 'b). P a ) = case_prod (λa. case_prod (λ(x :: 'a) (y :: 'b). P a ))"
       by (auto simp: split_def)
lemma L2_split_fixup_f:
  "(f (case y of (a, b) → G a b) =
           (case y of (a, b) → f (G a b)))"
       by (auto simp: split_def)
lemma L2_split_fixup_g:
  "case_prod (λa (b :: 'a × 'b). P a b) = case_prod (λa. case_prod (λ(x :: 'a) (y :: 'b). P a (x, y)))"
       by (auto simp: split_def)

lemma liftE_fixup: "(λx. liftE (case x of (a, b) → f a b)) = (λ(a,b). liftE (f a b))"
  by (simp add: fun_eq_iff split: prod.splits)

lemma finally_fixup: "(λx. finally (case x of (a, b) → f a b)) = (λ(a,b). finally (f a b))"
  by (simp add: fun_eq_iff split: prod.splits)

lemma try_fixup: "(λx. try (case x of (a, b) → f a b)) = (λ(a,b). try (f a b))"
  by (simp add: fun_eq_iff split: prod.splits)

lemma L2_gets_const_split_fixup: "L2_gets (λ_. case y of (a, b) → G a b) = (case y of (a, b) → L2_gets (λ_. G a b))"
  by (simp add: fun_eq_iff split: prod.splits)

definition STOP :: "'a::{} → 'a"  
  where "STOP P ≡ P"

lemma STOP_cong: "STOP P ≡ STOP P"
  by simp

lemma do_STOP: "P ≡ STOP P"
  by (simp add: STOP_def)

definition STOP_UNBIND :: "'a::{} → 'a"  
  where "STOP_UNBIND P ≡ P"

lemma STOP_UNBIND_cong: "STOP_UNBIND P ≡ STOP_UNBIND P"
  by simp

lemma do_STOP_UNBIND: "P ≡ STOP_UNBIND P"
  by (simp add: STOP_UNBIND_def)

definition FUSE :: "'a::{} → 'a"  
  where "FUSE P ≡ P"

lemma FUSE_cong: "FUSE P ≡ FUSE P"
  by simp

lemma do_FUSE: "P ≡ FUSE P"
  by (simp add: FUSE_def)

lemma FUSE_STOP: "X ≡ X' ==> FUSE X ≡ STOP X'"
  by (simp add: FUSE_def STOP_def)

lemma fixup_accumulate: 
  "(λ(x, a). (case a of (x1, x2) → C x1 x2) x) = (λ(x, x1, x2). C x1 x2 x)"
  by (auto simp: split_def)

lemma case_prod_apply_distrib: 
  "(case x of (a, b) → f a b) n = (case x of (a, b) → f a b n )"
  by (auto simp add: split_def)

lemma L2_guard_fixup1: "L2_guard (λs. case y of (a, b) → G a b s) = (case y of (a, b) → L2_guard (G a b))"
  by (auto simp: split_def)

lemmas L2_split_fixups_base = 

  L2_split_fixup_3
  L2_split_fixup_4
  liftE_fixup
  finally_fixup
  try_fixup

  L2_guard_fixup1
  L2_split_fixup_f [where f=L2_guard]
  L2_split_fixup_f [where f=L2_gets]
  L2_split_fixup_f [where f=L2_modify]

  L2_gets_const_split_fixup

  L2_split_fixup_g [where P="λa b. L2_gets (P a b) n" for P n]
  L2_split_fixup_g [where P="λa b. L2_guard (P a b)" for P]
  L2_split_fixup_g [where P="λa b. L2_modify (P a b)" for P]
  L2_split_fixup_g [where P="λa b. L2_spec (P a b)" for P]
  L2_split_fixup_g [where P="λa b. L2_assume (P a b)" for P]
  L2_split_fixup_g [where P="λa b. L2_throw (P a b) n" for P n]

  L2_split_fixup_g [where P="λa b. L2_seq (L a b) (R a b)" for L R]
  L2_split_fixup_g [where P="λa b. L2_while (C a b) (B a b) (I a b) n" for C B I n]
  L2_split_fixup_g [where P="λa b. L2_unknown n" for n]
  L2_split_fixup_g [where P="λa b. L2_catch (L a b) (R a b)" for L R]
  L2_split_fixup_g [where P="λa b. L2_condition (C a b) (L a b) (R a b)" for C L R]
  L2_split_fixup_g [where P="λa b. L2_call (M a b)" for M]
  L2_split_fixup_g [where P="λa b. liftE (M a b)" for M]
  L2_split_fixup_g [where P="λa b. finally (M a b)" for M]
  L2_split_fixup_g [where P="λa b. try (M a b)" for M]

lemmas L2_split_fixups =
  L2_split_fixup_1
  L2_split_fixup_2
  L2_split_fixups_base

lemmas L2_split_fixups' =
  L2_split_L2_seq_fixup_both
  L2_split_L2_seq_gets_fixup_1
  L2_split_fixup_g [where P="λa b. L2_seq_gets (L a b) (R a b)" for L R]
  fixup_accumulate
  L2_split_fixups_base
  L2_split_fixup_f [where f=STOP]
  case_prod_apply_distrib

lemmas L2_split_fixups_congs =
  prod.case_cong

(* Peephole simplification rules for L2 programs (including HeapLift and WordAbstract). *)
named_theorems L2opt


lemma monotone_nondet_monad_L2_seq_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "∧r. monotone R (≤) (λf. Y f r)"
  shows "monotone R (≤)
    (λf. (L2_seq (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma mono_L2_seq [monad_mono_intros]: "(∧x. f2 x ≤ g2 x) ==> f1 ≤ g1 ==> L2_seq f1 f2 ≤ L2_seq g1 g2"
  unfolding L2_defs
  by (auto intro: monad_mono_intros)

lemma monotone_nondet_monad_L2_seq_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "∧r. monotone R (≥) (λf. Y f r)"
  shows "monotone R (≥)
    (λf. (L2_seq (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_nondet_monad_L2_try_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  shows "monotone R (≤)
    (λf. (L2_try (X f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
  apply (rule mono_X)
  done

lemma monotone_nondet_monad_L2_try_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  shows "monotone R (≥)
    (λf. (L2_try (X f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
  apply (rule mono_X)
  done

lemma mono_L2_try[monad_mono_intros]: "f ≤ g ==> L2_try f ≤ L2_try g"
  unfolding L2_defs
  by (auto intro: monad_mono_intros)

lemma monotone_nondet_monad_L2_catch_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "∧r. monotone R (≤) (λf. Y f r)"
  shows "monotone R (≤)
    (λf. (L2_catch (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_nondet_monad_L2_catch_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "∧r. monotone R (≥) (λf. Y f r)"
  shows "monotone R (≥)
    (λf. (L2_catch (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma mono_L2_catch[monad_mono_intros]: "f1 ≤ g1 ==> (∧x. f2 x ≤ g2 x) ==> L2_catch f1 f2 ≤ L2_catch g1 g2"
  unfolding L2_defs
  by (auto intro: monad_mono_intros)

lemma monotone_nondet_monad_L2_condition_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "monotone R (≤) Y"
  shows "monotone R (≤)
    (λf. (L2_condition C (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_nondet_monad_L2_condition_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "monotone R (≥) Y"
  shows "monotone R (≥)
    (λf. (L2_condition C (X f) (Y f)))"
  unfolding L2_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma mono_L2_condition[monad_mono_intros]: 
  "f1 ≤ g1 ==> f2 ≤ g2 ==> L2_condition c f1 f2 ≤ L2_condition c g1 g2"
  unfolding L2_defs
  by (auto intro: monad_mono_intros)

lemma monotone_nondet_monad_L2_guarded_le [partial_function_mono]:
  assumes mono_X[partial_function_mono]: "monotone R (≤) X"
  shows "monotone R (≤)
    (λf. L2_guarded C (X f))"
  unfolding L2_guarded_def
  apply (rule partial_function_mono)+
  done

lemma monotone_nondet_monad_L2_guarded_ge [partial_function_mono]:
  assumes mono_X[partial_function_mono]: "monotone R (≥) X"
  shows "monotone R (≥)
    (λf. L2_guarded C (X f))"
  unfolding L2_guarded_def
  apply (rule partial_function_mono)+
  done

lemma mono_L2_guarded[monad_mono_intros]: "f ≤ g ==> L2_guarded c f ≤ L2_guarded c g"
  unfolding L2_defs L2_guarded_def
  apply (intro monad_mono_intros)
   apply simp
  apply (simp add: le_fun_def)
  done

lemma monotone_nondet_monad_L2_while_le [partial_function_mono]:
  assumes mono_B: "∧r. monotone R (≤) (λf. B f r)"
  shows "monotone R (≤) (λf. L2_while C (B f) I ns)"
  unfolding L2_defs
  apply (rule partial_function_mono)
  apply (rule mono_B)
  done

lemma monotone_nondet_monad_L2_while_ge [partial_function_mono]:
  assumes mono_B: "∧r. monotone R (≥) (λf. B f r)"
  shows "monotone R (≥) (λf. L2_while C (B f) I ns)"
  unfolding L2_defs
  apply (rule partial_function_mono)
  apply (rule mono_B)
  done

lemma mono_L2_while [monad_mono_intros]:
  "(∧x. b1 x ≤ b2 x) ==> L2_while c b1 i ns ≤ L2_while c b2 i ns"
  unfolding L2_defs L2_guarded_def
  by (auto intro: monad_mono_intros)

lemma monotone_nondet_monad_map_exn_le [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≤) X" 
  shows "monotone R (≤) (λf. map_value (map_exn emb) (X f))"
  unfolding map_exn_def
  apply (rule partial_function_mono)+
  done

lemma monotone_nondet_monad_map_exn_ge [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≥) X" 
  shows "monotone R (≥) (λf. map_value (map_exn emb) (X f))"
  unfolding map_exn_def
  apply (rule partial_function_mono)+
  done


lemma monotone_nondet_monad_L2_call_le [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≤) X" 
  shows "monotone R (≤)
    (λf. L2_call (X f) emb ns)"
  unfolding L2_call_def
  apply (rule partial_function_mono)+
  done

lemma monotone_nondet_monad_L2_call_ge [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≥) X" 
  shows "monotone R (≥)
    (λf. L2_call (X f) emb ns)"
  unfolding L2_call_def
  apply (rule partial_function_mono)+
  done

lemma mono_L2_call [monad_mono_intros]: "f ≤ g ==> L2_call f emb ns ≤ L2_call g emb ns"
  unfolding L2_call_def
  by (auto intro: monad_mono_intros)

section ‹Some Relators›

lemma exists_sum_unit_eq: "(∃l'::unit. Inl x = Inl l' ∧ Inr y = Inr l') = (x=() ∧ y=())"
  by auto

lemmas unit_convs = exists_sum_unit_eq

definition "rel_Nonlocal = (λe v. case e of Nonlocal x → v = x | _ → False)"

lemma rel_Nonlocal_conv: "(rel_Nonlocal e v) = (e = Nonlocal v)"
  by (cases e) (auto simp add: rel_Nonlocal_def)

lemma fun_of_rel_rel_Nonlocal[fun_of_rel_intros]: "fun_of_rel rel_Nonlocal the_Nonlocal"
  by (auto simp add: fun_of_rel_def rel_Nonlocal_def split: c_exntype.splits)

lemma funp_rel_Nonlocal[funp_intros, corres_admissible]: "funp rel_Nonlocal"
  using fun_of_rel_rel_Nonlocal
  by (auto simp add: funp_def)

lemma  rel_sum_rel_Nonlocal_case_InlI: "e = Nonlocal v' ==> rel_sum rel_Nonlocal (=) (case e of Nonlocal v → Inl (Nonlocal v) | _ → Inr x) (Inl v')"
  by (simp add: rel_Nonlocal_def)

lemma  rel_xval_rel_Nonlocal_case_ExnI: "e = Nonlocal v' ==> rel_xval rel_Nonlocal (=) (case e of Nonlocal v → Exn (Nonlocal v) | _ → Result x) (Exn v')"
  by (simp add: rel_Nonlocal_def)

lemma  rel_sum_rel_Nonlocal_case_InrI: "is_local e ==> x = v' ==> rel_sum rel_Nonlocal (=) (case e of Nonlocal v → Inl (Nonlocal v) | _ → Inr x) (Inr v')"
  apply (cases e)
  apply (auto simp add: rel_Nonlocal_def)
  done

lemma  rel_xval_rel_Nonlocal_case_ResultI: "is_local e ==> x = v' ==> rel_xval rel_Nonlocal (=) (case e of Nonlocal v → Exn (Nonlocal v) | _ → Result x) (Result v')"
  apply (cases e)
  apply (auto simp add: rel_Nonlocal_def)
  done

lemma rel_sum_rel_Nonlocal_map_sumI: "v = (map_sum (λx. x) f (case e of Nonlocal x → Inl x | _ → Inr x)) ==>
 rel_sum rel_Nonlocal (=) (map_sum Nonlocal f (case e of Nonlocal x → Inl x | _ → Inr x)) v"
  apply simp
  apply (cases e)
      apply (auto simp add: rel_Nonlocal_def)
  done

lemma rel_xval_rel_Nonlocal_map_xvalI: "v = (map_xval (λx. x) f (case e of Nonlocal x → Exn x | _ → Result x)) ==>
 rel_xval rel_Nonlocal (=) (map_xval Nonlocal f (case e of Nonlocal x → Exn x | _ → Result x)) v"
  apply simp
  apply (cases e)
      apply (auto simp add: rel_Nonlocal_def)
  done



(* FIXME: remove if unused? Probably used in replacement of refines_spec *)

definition "rel_Inr v v' ≡ (v = Inr v')"

lemma fun_of_rel_rel_Inr[fun_of_rel_intros]:
  "fun_of_rel rel_Inr (λx. case x of Inr v → v | Inl _ → undefined)"
  by (auto simp add: rel_Inr_def fun_of_rel_def)

lemma funp_rel_Inr[funp_intros, corres_admissible]: "funp rel_Inr"
  using fun_of_rel_rel_Inr by (auto simp add: funp_def)

lemma rel_InrI: "v = Inr v' ==> rel_Inr v v'"
  by (simp add: rel_Inr_def)

lemma rel_Inr_apply: "rel_Inr x y = (x = Inr y)"
  by (simp add: rel_Inr_def )

lemma rel_Inr_trivial [simp]: "rel_Inr (Inr v) v"
  by (simp add: rel_Inr_def)

definition rel_liftE:: "('e, 'a) xval → 'a val → bool" where "rel_liftE v v' ≡ (v = Result (the_Res v'))"


lemma fun_of_rel_rel_liftE[fun_of_rel_intros]:
  "fun_of_rel rel_liftE (λx. case x of Result v → Result v | Exn _ → undefined)"
  by (auto simp add: rel_liftE_def fun_of_rel_def)

lemma funp_rel_liftE[funp_intros, corres_admissible]: "funp rel_liftE"
  using fun_of_rel_rel_liftE by (auto simp add: funp_def)


lemma rel_liftEI: "v = Result (the_Res v') ==> rel_liftE v v'"
  by (simp add: rel_liftE_def)

lemma rel_liftE_apply: "rel_liftE x y = (x = Result (the_Res y))"
  by (simp add: rel_liftE_def )

lemma rel_liftE_trivial [simp]: "rel_liftE (Result v) (Result v)"
  by (simp add: rel_liftE_def)

lemma rel_liftE_rel_exception_or_result_conv: "rel_liftE = rel_exception_or_result (λNone → λ_. True | Some _ → λ_. False) (=)"
  apply (rule ext)+
  apply (auto simp add: rel_liftE_def rel_exception_or_result.simps)
  done

lemma rel_liftE_Result_Result_iff[simp]: "rel_liftE (Result v) (Result v') ⟷ v = v'"
  by (auto simp add: rel_liftE_def)

definition "rel_liftE' v v' ≡ (v = Inr v')"

lemma fun_of_rel_rel_liftE'[fun_of_rel_intros]:
  "fun_of_rel rel_liftE' (λx. case x of Inr v → v | Inl _ → undefined)"
  by (auto simp add: rel_liftE'_def fun_of_rel_def)

lemma funp_rel_liftE'[funp_intros, corres_admissible]: "funp rel_liftE'"
  using fun_of_rel_rel_liftE' by (auto simp add: funp_def)

lemma rel_liftE'I: "v = Inr v' ==> rel_liftE' v v'"
  by (simp add: rel_liftE'_def)

lemma rel_liftE'_apply: "rel_liftE' x y = (x = Inr y)"
  by (simp add: rel_liftE'_def )

lemma rel_liftE'_trivial [simp]: "rel_liftE' (Inr v) v"
  by (simp add: rel_liftE'_def)

lemma rel_liftE'_Inr_iff[simp]: "rel_liftE' (Inr v) v' ⟷ v = v'"
  by (auto simp add: rel_liftE'_def)

lemma rel_liftE'_rel_liftE_conv: "rel_liftE' = rel_map to_xval OO rel_liftE OO rel_map the_Res"
  apply (rule ext)+
  apply (auto simp add: relcompp.simps rel_map_def rel_liftE_def rel_liftE'_def)
  done

lemma rel_liftE_rel_liftE'_conv: "rel_liftE = rel_map from_xval OO rel_liftE' OO rel_map Result"
  apply (rule ext)+
  apply (auto simp add: relcompp.simps rel_map_def rel_liftE_def rel_liftE'_def)
  done


lemma rel_liftE'_Inr: "rel_liftE' (Inr x) x"
  by (simp)


definition rel_throwE' :: "('a → 'b → bool) → 'a + 'c → 'b → bool" where
  "rel_throwE' L a c ⟷ (case a of Inl a' → L a' c | Inr _ → False)"

lemma rel_throwE'_iff: "rel_throwE' L a c ⟷ (∃l. a = Inl l ∧ L l c)"
  by (auto simp add: rel_throwE'_def split: sum.splits)

lemma rel_throwE'_Inl:
  "L x y ==> rel_throwE' L (Inl x) y"
  unfolding rel_throwE'_def
  by auto

lemma rel_throwE'_Inl_iff[simp]:
  "rel_throwE' L (Inl x) y ⟷ L x y"
  unfolding rel_throwE'_def
  by auto

lemma not_rel_throwE'_Inr[simp]: "¬rel_throwE' R (Inr d) a"
  by (auto simp: rel_throwE'_def)

definition rel_throwE :: "('a → 'b → bool) → ('a, 'c) xval → 'b → bool" where
  "rel_throwE L a c ⟷ (case a of Exn a' → L a' c | Result _ → False)"

lemma rel_throwE_iff: "rel_throwE L a c ⟷ (∃e. a = Exn e ∧ L e c)"
  by (auto simp add: rel_throwE_def split: xval_splits)

lemma rel_throwE_Exn:
  "L x y ==> rel_throwE L (Exn x) y"
  unfolding rel_throwE_def
  by auto

lemma rel_throwE_Exn_iff[simp]:
  "rel_throwE L (Exn x) y ⟷ L x y"
  unfolding rel_throwE_def
  by auto

lemma not_rel_throwE_Result[simp]: "¬rel_throwE R (Result d) a"
  by (auto simp: rel_throwE_def)


lemma case_right_eq: "(case v of Inl l → False | Inr r → P r) = (∃r. P r ∧ v = Inr r)"
  by (auto split: sum.splits)
lemma case_left_eq: "(case v of Inr r → False | Inl l → P l) = (∃l. P l ∧ v = Inl l)"
  by (auto split: sum.splits)

lemma rel_sum_right: "rel_sum L R (Inr r) v = (∃r'. v = Inr r' ∧ R r r')"
  by (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)
lemma rel_sum_left: "rel_sum L R (Inl l) v = (∃l'. v = Inl l' ∧ L l l')"
  by (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)

lemma rel_sum_eq_apply: "(rel_sum (=) (=) x y) = (x = y)"
  by (cases x) (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)

lemma gen_unit_eq: "x = (y::unit)"
  by simp

lemma liftE_L2_while: "L2_while c (λr. liftE (B r)) i n = liftE (whileLoop c B i)"
  by (clarsimp simp: L2_while_def liftE_whileLoop)

lemma liftE_L2_while_VARS: "L2_while c (λr. liftE (B r)) i n = liftE (L2_VARS (whileLoop c B i) n)"
  by (simp add: liftE_L2_while L2_VARS_def)

lemma rel_XF_True_def: "(rel_XF st ret_xf ex_xf (λ_ _. True)) =
         (λ(v, t) (r, s). s = st t ∧
            (case v of Exn x → r = Exn (ex_xf x t) | Result x → r = Result (ret_xf x t)))"
  apply (rule ext)+
  apply (auto simp add: rel_XF_def rel_xval.simps split: xval_splits)
  done

lemma refines_corresXF: "(∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
    (case v of Exn x → r = Exn (ex_xf x t) | Result x → r = Result (ret_xf x t))))
 ==> corresXF st ret_xf ex_xf P A C"
  by (simp add: corresXF_refines_iff rel_XF_True_def)


lemma corresXF_refines: "corresXF st ret_xf ex_xf P A C ==>
(∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
    (case v of Exn x → r = Exn (ex_xf x t) | Result x → r = Result (ret_xf x t))))"
  by (simp add: corresXF_refines_iff rel_XF_True_def)


theorem corresXF_refines_conv:
‹corresXF st ret_xf ex_xf P A C ⟷
 (∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
 (case v of Exn x → r = Exn (ex_xf x t) | Result x → r = Result (ret_xf x t))))›
  using corresXF_refines refines_corresXF ..

lemma sim_nondet_to_corresXF: "(∧s. refines f f' s s (=)) ==>
corresXF (λs. s) (λr _. r) (λr _ . r) (λ_. True) f' f"
  unfolding refines_def_old  corresXF_def
  apply (auto split: xval_splits)
  done


named_theorems rel_spec_monad_rewrite_simps

locale sim_stack_heap_state = 
  abstract: stack_heap_state htd_a htd_upd_a hmem_a hmem_upd_a S +
  concrete: stack_heap_state htd_c htd_upd_c hmem_c hmem_upd_c S 
  for
    htd_a:: "'s_a → heap_typ_desc" and
    htd_upd_a:: "(heap_typ_desc → heap_typ_desc) → 's_a → 's_a" and
    hmem_a:: "'s_a → heap_mem" and
    hmem_upd_a:: "(heap_mem → heap_mem) → 's_a → 's_a" and 

    htd_c:: "'s_c → heap_typ_desc" and
    htd_upd_c:: "(heap_typ_desc → heap_typ_desc) → 's_c → 's_c" and
    hmem_c:: "'s_c → heap_mem" and
    hmem_upd_c:: "(heap_mem → heap_mem) → 's_c → 's_c" and
    S::"addr set"
begin

definition rel_stack_free where 
  "rel_stack_free s_c s_a ≡ stack_free (htd_c s_c) ⊆ stack_free (htd_a s_a)"


lemma refines_rel_stack_free_with_fresh_stack_ptr:
  assumes s: "rel_stack_free s_c s_a"
  assumes init_eq: "∧s_c s_a. I_c s_c = I_a s_a"
  assumes f: "∧s_c s_a p. rel_stack_free s_c s_a ==>
    refines (f_c p) (f_a p) s_c s_a
       (rel_prod (rel_xval L R) rel_stack_free)"
  shows "refines
     (concrete.with_fresh_stack_ptr n I_c f_c)
     (abstract.with_fresh_stack_ptr n I_a f_a) s_c s_a
        (rel_prod (rel_xval L R) rel_stack_free)"
  apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
  apply (rule refines_bind_bind_exn [where Q="(rel_prod (rel_xval (λ_ _. False) (=)) rel_stack_free)"])
      apply simp_all
  subgoal
    apply (clarsimp simp add: refines_def_old rel_xval.simps)
    using s init_eq
    apply (simp add: rel_stack_free_def)
    subgoal for p d vs bs
      apply (frule (1) stack_allocs_stack_free_mono)
      apply clarsimp
      subgoal for d'
        apply (rule exI[where x="hmem_upd_a (fold (λi. heap_update_padding (p +_p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) (htd_upd_a (λ_. d') s_a)"]) 
        apply clarsimp
        apply (rule conjI)
         apply (rule exI[where x="d'"])
         apply clarsimp
         apply (rule exI[where x="vs"])
         apply clarsimp
         apply blast
        using stack_free_stack_allocs
        apply blast
        done
      done
    done
  apply (rule refines_rel_prod_on_exit [where S' = rel_stack_free])
   apply (rule f)
   apply assumption
   apply (simp add: rel_stack_free_def)
   apply (metis abstract.htd_hmem_upd abstract.typing.get_upd concrete.htd_hmem_upd 
      concrete.typing.get_upd stack_free_stack_releases_mono')
  subgoal using stack_free_stack_releases_mono' by blast
  done

definition rel_stack_free_eq where 
  "rel_stack_free_eq s_c s_a ≡ stack_free (htd_c s_c) = stack_free (htd_a s_a)"

lemma refines_rel_stack_free_eq_with_fresh_stack_ptr:
  assumes s: "rel_stack_free_eq s_c s_a"
  assumes init_eq: "∧s_c s_a. I_c s_c = I_a s_a"
  assumes f: "∧s_c s_a p. rel_stack_free_eq s_c s_a ==>
    refines (f_c p) (f_a p) s_c s_a
      (rel_prod (rel_xval L R) rel_stack_free_eq)"
  shows "refines
     (concrete.with_fresh_stack_ptr n I_c f_c)
     (abstract.with_fresh_stack_ptr n I_a f_a) s_c s_a
        (rel_prod (rel_xval L R) rel_stack_free_eq)"
  apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
  apply (rule refines_bind_bind_exn [where Q="(rel_prod (rel_xval (λ_ _. False) (=)) rel_stack_free_eq)"])
      apply simp_all
  subgoal
    apply (clarsimp simp add: refines_def_old rel_xval.simps)
    using s init_eq
    apply (simp add: rel_stack_free_eq_def)
    subgoal for p d vs bs
      apply (frule (1) stack_allocs_stack_free_eq)
      apply clarsimp
      subgoal for d'
        apply (rule exI[where x="hmem_upd_a (fold (λi. heap_update_padding (p +_p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) (htd_upd_a (λ_. d') s_a)"]) 
        apply clarsimp
        apply (rule conjI)
         apply (rule exI[where x="d'"])
         apply clarsimp
         apply (rule exI[where x="vs"])
         apply clarsimp
         apply blast
        using stack_free_stack_allocs
        apply blast
        done
      done
    done
  apply (rule refines_rel_prod_on_exit [where S' = rel_stack_free_eq])
   apply (rule f)
    apply assumption
   apply clarsimp
  subgoal for v t t' s_c s_a bs
    apply (rule exI[where x=" hmem_upd_a (heap_update_list (ptr_val v) bs) (htd_upd_a (stack_releases n v) s_a)"])
    apply (clarsimp simp add: rel_stack_free_eq_def)
    by (metis dual_order.eq_iff stack_free_stack_releases_mono')
  subgoal by blast
  done

 
end

locale sim_stack_heap_raw_state = 
  abstract: stack_heap_raw_state hrs_a hrs_upd_a S +
  concrete: stack_heap_raw_state hrs_c hrs_upd_c S 
  for
    hrs_a:: "'s_a → heap_raw_state" and
    hrs_upd_a:: "(heap_raw_state → heap_raw_state) → 's_a → 's_a" and

    hrs_c:: "'s_c → heap_raw_state" and
    hrs_upd_c:: "(heap_raw_state → heap_raw_state) → 's_c → 's_c" and
    S::"addr set"
begin
sublocale sim_stack_heap_state  
  "λs. hrs_htd (hrs_a s)" "λupd. hrs_upd_a (hrs_htd_update upd)" 
  "λs. hrs_mem (hrs_a s)" "λupd. hrs_upd_a (hrs_mem_update upd)" 
  "λs. hrs_htd (hrs_c s)" "λupd. hrs_upd_c (hrs_htd_update upd)" 
  "λs. hrs_mem (hrs_c s)" "λupd. hrs_upd_c (hrs_mem_update upd)" 
  S
  by unfold_locales
end

named_theorems L2corres_with_fresh_stack_ptr

locale L2 = sim_stack_heap_state htd_a htd_upd_a hmem_a hmem_upd_a htd_c htd_upd_c hmem_c hmem_upd_c S 
  for
    htd_a:: "'s_a → heap_typ_desc" and
    htd_upd_a:: "(heap_typ_desc → heap_typ_desc) → 's_a → 's_a" and
    hmem_a:: "'s_a → heap_mem" and
    hmem_upd_a:: "(heap_mem → heap_mem) → 's_a → 's_a" and 

    htd_c:: "'s_c → heap_typ_desc" and
    htd_upd_c:: "(heap_typ_desc → heap_typ_desc) → 's_c → 's_c" and
    hmem_c:: "'s_c → heap_mem" and
    hmem_upd_c:: "(heap_mem → heap_mem) → 's_c → 's_c" and
    S::"addr set" +
  fixes st:: "'s_c → 's_a"
  assumes htd_st: "∧s. htd_a (st s) = htd_c s"
  assumes htd_upd_st: "∧s f. (htd_upd_a f (st s)) = st (htd_upd_c f s)"
  assumes hmem_upd_st: "∧s f. (hmem_upd_a f (st s)) = st (hmem_upd_c f s)"

begin
lemma rel_stack_free_eq_st: "rel_stack_free_eq s (st s)"
  by (simp add: rel_stack_free_eq_def htd_st)
 
definition rel_L2 where 
  "rel_L2 ex_xf ret_xf ≡ (λ (r_c, s_c) (r_a, s_a).
     rel_xval (λ_ a. a = ex_xf s_c) (λ_ a. a = ret_xf s_c) r_c r_a ∧
     (s_a = st s_c))"

lemma rel_L2_def': 
  "(rel_L2 ex_xf ret_xf) = (λ(v, t) (r, s).
              s = st t ∧ (case v of Exn x → r = Exn (ex_xf t) | Result x → r = Result (ret_xf t)))"
  apply  (clarsimp simp add: rel_L2_def fun_eq_iff, intro iffI)
  subgoal using rel_xval.cases by fastforce
  subgoal by(auto split: xval_splits)
  done


lemma refines_rel_L2_on_exit':
  assumes f: "refines (f_c p) (f_a p) s_c (st s_c) (rel_L2 ex_xf ret_xf)"
  assumes ex_xf_htd_indep: "∧f s. ex_xf (htd_upd_c f s) = ex_xf s"
  assumes ret_xf_htd_indep: "∧f s. ret_xf (htd_upd_c f s) = ret_xf s"
  shows "refines
    (on_exit (f_c p) {(s,t). t = htd_upd_c (release p) s})
    (on_exit (f_a p) {(s,t). t = htd_upd_a (release p) s}) s_c (st s_c)
    (rel_L2 ex_xf ret_xf)"
  unfolding on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result) 
  apply (rule refines_mono [OF _ f])
  apply (clarsimp) 
  subgoal for r s q t
    apply (rule refines_bind_bind_exn[where
      Q="(λ(r', s) (q', t). is_Result r' ∧ is_Result q' ∧ rel_L2 ex_xf ret_xf (r, s) (q, t))"])
    subgoal
      apply (rule refines_assert_result_and_state)
       apply (clarsimp simp add: rel_L2_def, intro conjI)
      subgoal
        using ex_xf_htd_indep ret_xf_htd_indep 
        by metis
      subgoal
        using htd_upd_st by force
      by auto
    apply (auto simp: is_Result_def)
    done
  done

lemma refines_rel_L2_on_exit:
  assumes f: "refines (f_c p) (f_a p) s_c (st s_c) (rel_L2 ex_xf ret_xf)"
  assumes ex_xf_htd_indep: "∧g f s. ex_xf (hmem_upd_c g (htd_upd_c f s)) = ex_xf s"
  assumes ret_xf_htd_indep: "∧g f s. ret_xf (hmem_upd_c g (htd_upd_c f s)) = ret_xf s"
  assumes nonempty_cleanup_a: "cleanup_a ≠ {}"
  assumes cleanup_htd: "∧s s'. (s, s') ∈ cleanup_c ==> ∃g f. s' = (hmem_upd_c g (htd_upd_c f s))"
  assumes stuck_sim: "∧s. ∄s'. (s, s') ∈ cleanup_c ==> ∄t'. (st s, t') ∈ cleanup_a"
  assumes cleanup_sim: "∧s t. (s, t) ∈ cleanup_c ==> (st s, st t) ∈ cleanup_a"
  shows "refines
    (on_exit (f_c p) cleanup_c)
    (on_exit (f_a p) cleanup_a) s_c (st s_c)
    (rel_L2 ex_xf ret_xf)"
  unfolding on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result) 
  apply (rule refines_mono [OF _ f])
  apply (clarsimp) 
  subgoal for r s q t
    apply (rule refines_bind_bind_exn [where
      Q="λ(r', s) (q', t). is_Result r' ∧ is_Result q' ∧ rel_L2 ex_xf ret_xf (r, s) (q, t)"])
    subgoal
      apply (rule refines_state_select)
       apply (clarsimp simp add: rel_L2_def, intro conjI)
      subgoal
        using cleanup_htd cleanup_sim
        by blast
      subgoal
        using ex_xf_htd_indep ret_xf_htd_indep cleanup_htd
        by metis
      subgoal
        using stuck_sim by (auto simp: rel_L2_def)
      done
    apply (auto simp: is_Result_def)
    done
  done


lemma refines_rel_L2_with_fresh_stack_ptr:
  assumes init_eq: "I_c s_c = I_a (st s_c)"
  assumes ex_xf_htd_indep: "∧g f s. ex_xf (hmem_upd_c g (htd_upd_c f s)) = ex_xf s"
  assumes ret_xf_htd_indep: "∧g f s. ret_xf (hmem_upd_c g (htd_upd_c f s)) = ret_xf s"
  assumes f: "∧(p::'a::mem_type ptr) d vs bs. (p, d) ∈ stack_allocs n S TYPE('a) (htd_c s_c) ==> vs ∈ I_c s_c ==> length vs = n ==>
          length bs = n * size_of TYPE('a) ==>
           refines
             (f_c p)
             (f_a p)
             (hmem_upd_c (fold (λi. heap_update_padding (p +_p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd_c (λ_. d)) s_c))
             (st (hmem_upd_c (fold (λi. heap_update_padding (p +_p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd_c (λ_. d)) s_c)))
             (rel_L2 ex_xf ret_xf)"
  shows "refines
     (concrete.with_fresh_stack_ptr n I_c f_c)
     (abstract.with_fresh_stack_ptr n I_a f_a) s_c (st s_c)
     (rel_L2 ex_xf ret_xf)"
  apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
  apply (rule refines_bind_bind_exn [where Q="(λ(r_c, t_c) (r_a, t_a).
           (∃d p vs bs. (p, d) ∈ stack_allocs n S TYPE('a) (htd_c s_c) ∧ r_c = Result p ∧ r_a = Result p ∧ vs ∈ I_c s_c ∧ length vs = n ∧
              length bs = n * size_of TYPE('a) ∧
              t_c = hmem_upd_c (fold (λi. heap_update_padding (p +_p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd_c (λ_. d)) s_c) ∧
              t_a = st t_c))"])
      apply simp_all
  subgoal
    apply (clarsimp simp add: refines_def_old rel_xval.simps)
    by (metis (full_types) hmem_upd_st htd_st htd_upd_st init_eq )
  subgoal for p 
    apply clarsimp
    apply (rule refines_rel_L2_on_exit )    
      apply (rule f) 
             apply simp
            apply simp
           apply simp
          apply simp
         apply (rule ex_xf_htd_indep)
        apply (rule ret_xf_htd_indep)
       apply blast
    subgoal by auto
    subgoal by auto
    subgoal using htd_upd_st hmem_upd_st by auto
    done
  done
  
lemma L2corres_refines_rel_L2_conv:
‹L2corres st ret_xf ex_xf P A C ⟷
 (∀t. P t ⟶ refines C A t (st t) (rel_L2 ex_xf ret_xf))›
  by (simp add: L2corres_def corresXF_refines_conv rel_L2_def')


lemma L2corres_refines_rel_L2:
  assumes L2: "L2corres st ret_xf ex_xf P A C"
  assumes P: "P s_c"
  shows ‹refines C A s_c (st s_c) (rel_L2 ex_xf ret_xf)›
  using L2 P by (simp add: L2corres_refines_rel_L2_conv)

lemma L2corres_with_fresh_stack_ptr[L2corres_with_fresh_stack_ptr]:
  assumes l2: "∧p. L2corres st ret_xf ex_xf P (l2 p) (l1 p)"
  assumes I: "∧s. R s ==> I_l1 s = I_l2 (st s)"
  assumes P: "∧s. R s ==> P s"
  assumes ex_xf_htd_indep: "∧g f s. ex_xf (hmem_upd_c g (htd_upd_c f s)) = ex_xf s"
  assumes ret_xf_htd_indep: "∧g f s. ret_xf (hmem_upd_c g (htd_upd_c f s)) = ret_xf s"
  assumes P_indep: "∧f g s. P (hmem_upd_c g (htd_upd_c f s)) = P s"
  shows "L2corres st ret_xf ex_xf R
           (abstract.with_fresh_stack_ptr n (I_l2) (L2_VARS l2 nm))
           (concrete.with_fresh_stack_ptr n I_l1 l1)"
  apply (clarsimp simp add: L2_VARS_def L2corres_refines_rel_L2_conv)
  apply (rule refines_rel_L2_with_fresh_stack_ptr)
     apply (rule I, assumption)
    apply (rule ex_xf_htd_indep)
   apply (rule ret_xf_htd_indep)
  apply (rule L2corres_refines_rel_L2)
   apply (rule l2)
  apply (simp add: P_indep P)
  done

end

hide_const (open) L2

lemma refines_rel_prod_guard_on_exit:
  assumes f: "refines f_c f_a s_c s_a (rel_prod R S')"
  assumes cleanup: "∧s_c s_a t_c. S' s_c s_a ==> grd s_a ==> (s_c, t_c) ∈ cleanup_c ==> ∃t_a. (s_a, t_a) ∈ cleanup_a ∧ S t_c t_a"
  assumes emp: "∧s_c s_a. S' s_c s_a ==> ∄t_c. (s_c, t_c) ∈ cleanup_c ==> ∄t_a. (s_a, t_a) ∈ cleanup_a"
  shows "refines (on_exit f_c cleanup_c) (guard_on_exit f_a grd cleanup_a) s_c s_a (rel_prod R S)"
  unfolding on_exit_def on_exit'_def
  apply (rule refines_bind_exception_or_result[OF refines_weaken, OF f])
  apply (simp add: bind_assoc)
  apply (rule refines_bind_guard_right)
  apply (rule refines_bind'[OF refines_state_select])
  subgoal using cleanup by auto
  subgoal using emp by auto
  done

lemma refines_bind_no_throw_strong:
  assumes "no_throw (λ_. True) f"
  assumes "no_throw (λ_. True) f'"
  assumes f: "refines f f' s s' Q"
  assumes g: "∧r t r' t'. reaches f s (Result r) t ==> reaches f' s' (Result r') t' ==>
    Q (Result r, t) (Result r', t') ==> refines (g r) (g' r') t t' R"
  shows "refines (f >>= g) (f' >>= g') s s' R"
  apply (rule refines_bind_bind_strong' [OF f])
  subgoal using assms
    apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
    by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
  subgoal using assms
    apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
    by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
  subgoal using assms
    apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
    by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
  subgoal using g
    by auto
  done

lemma refines_bind_no_throw:
  assumes "no_throw (λ_. True) f"
  assumes "no_throw (λ_. True) f'"
  assumes f: "refines f f' s s' Q"
  assumes g: "∧r t r' t'.
    Q (Result r, t) (Result r', t') ==> refines (g r) (g' r') t t' R"
  shows "refines (f >>= g) (f' >>= g') s s' R"
  using assms
  by (rule refines_bind_no_throw_strong)

lemma no_throw_guard[simp]: "no_throw P (guard G)"
  by (auto simp add: no_throw_def runs_to_partial_def_old)

lemma no_throw_assert_result_and_state[simp]: "no_throw P (assert_result_and_state f)"
  by (auto simp add: no_throw_def runs_to_partial_def_old)

lemma no_throw_assume_result_and_state[simp]: "no_throw P (assume_result_and_state f)"
  by (auto simp add: no_throw_def runs_to_partial_def_old)

lemma refines_guard_same: "refines (guard P) (guard P) s s (λ(r, t) (r', t'). t=s ∧ t'=s)"
  by (simp add: refines_def_old)

lemma refines_state_select_same: 
  "refines (state_select R) (state_select R) s s (λ(r, t) (r', t'). t' = t ∧ (s, t) ∈ R)"
  by (simp add: refines_def_old)

lemma refines_assert_result_and_state_same: 
  "refines (assert_result_and_state R) (assert_result_and_state R) s s
     (λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
  by (auto simp add: refines_def_old)

lemma refines_assume_result_and_state_same: 
  "refines (assume_result_and_state R) (assume_result_and_state R) s s
     (λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
  by (auto simp add: refines_def_old)

lemma refines_assume_result_and_state_same': 
  assumes "R s = R' s"
  shows "refines (assume_result_and_state R) (assume_result_and_state R') s s
            (λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
  using assms
  by (auto simp add: refines_def_old)

lemma refines_rel_xval_guard_on_exit:
  assumes f: "refines f_c f_a s s (rel_prod (rel_xval L R) (=))"
  shows "refines
          (guard_on_exit f_c P cleanup)
          (guard_on_exit f_a P cleanup) s s
          (rel_prod (rel_xval L R) (=))"
  unfolding guard_on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result')
   apply (rule f)
  apply clarsimp
  apply (rule refines_bind_no_throw_strong [OF _ _ refines_guard_same])
     apply simp
   apply simp
  apply clarsimp
  apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
     apply simp
   apply simp
  apply clarsimp
  done

lemma refines_rel_xval_on_exit:
  assumes f: "refines f_c f_a s s (rel_prod (rel_xval L R) (=))"
  shows "refines
          (on_exit f_c cleanup)
          (on_exit f_a cleanup) s s
          (rel_prod (rel_xval L R) (=))"
  unfolding on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result')
   apply (rule f)
  apply clarsimp
  apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
     apply simp
    apply simp
  apply clarsimp
  done


lemma refines_rel_xval_assume_on_exit:
  assumes f: "refines f_c f_a s s (rel_prod (rel_xval L R) (=))"
  shows "refines
          (assume_on_exit f_c P cleanup)
          (assume_on_exit f_a P cleanup) s s
          (rel_prod (rel_xval L R) (=))"
  unfolding assume_on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result')
   apply (rule f)

  apply (rule refines_bind_no_throw_strong [OF _ _ ])
     apply simp
    apply simp
  apply clarsimp
   apply (rule refines_assume_result_and_state_same)
  apply clarsimp
  apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
     apply simp
   apply simp
  apply clarsimp
  done

lemma refines_state_assume_pred:
  assumes P: "P t"
  assumes ref: "refines f g s t R"
  shows "refines f (do {assume_result_and_state (λs. {(x, y). (λ() s'. s' = s ∧ P s) x y}); g }) s t R"
  using P ref 
  by (auto simp add: refines_def_old succeeds_bind reaches_bind)

lemma refines_rel_prod_assume_on_exit:
  assumes f: "refines f_c f_a s_c s_a (rel_prod R S')"
  assumes cleanup: "∧s_c s_a t_c. S' s_c s_a ==> (s_c, t_c) ∈ cleanup_c ==> ∃t_a. (s_a, t_a) ∈ cleanup_a ∧ S t_c t_a"
  assumes emp: "∧s_c s_a. S' s_c s_a ==> ∄t_c. (s_c, t_c) ∈ cleanup_c ==> ∄t_a. (s_a, t_a) ∈ cleanup_a"
  assumes conseq: "∧s_c s_a. S' s_c s_a ==> P s_a"
  shows "refines (on_exit f_c cleanup_c) (assume_on_exit f_a P cleanup_a) s_c s_a (rel_prod R S)"
  unfolding assume_on_exit_bind_exception_or_result_conv on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result')
   apply (rule f)
  apply (rule refines_state_assume_pred )
  subgoal using conseq by auto
  subgoal 
    apply (rule refines_bind_no_throw_strong [where Q = "rel_prod (λ_ _. True) S"])
       apply simp
      apply simp
     apply (rule refines_state_select)
    subgoal using cleanup by auto
    subgoal using emp by auto
    subgoal 
      apply (rule refines_yield)
      apply auto
      done
    done
  done

lemma refines_runs_to_partial_rel_prod_assume_on_exit:
  assumes f: "refines f_c f_a s_c s_a (rel_prod R S')"
  assumes runs_to: "f_c ∙ s_c ?{λr t. P t}"
  assumes cleanup: "∧s_c s_a t_c. S' s_c s_a ==> (s_c, t_c) ∈ cleanup_c ==> P s_c ==> ∃t_a. (s_a, t_a) ∈ cleanup_a ∧ S t_c t_a"
  assumes emp: "∧s_c s_a. S' s_c s_a ==> P s_c ==> ∄t_c. (s_c, t_c) ∈ cleanup_c ==> ∄t_a. (s_a, t_a) ∈ cleanup_a"
  assumes conseq: "∧s_c s_a. S' s_c s_a ==> P s_c ==> P' s_a"
  shows "refines (on_exit f_c cleanup_c) (assume_on_exit f_a P' cleanup_a) s_c s_a (rel_prod R S)"
proof -
  from refines_runs_to_partial_fuse [OF f runs_to]
  have "refines f_c f_a s_c s_a (λ(r, t) (r', t'). rel_prod R S' (r, t) (r', t') ∧ P t)" .
  moreover have "(λ(r, t) (r', t'). rel_prod R S' (r, t) (r', t') ∧ P t) = rel_prod R (λt t'. S' t t' ∧ P t)"
    by (auto simp add: rel_prod_conv)
  ultimately have "refines f_c f_a s_c s_a (rel_prod R (λt t'. S' t t' ∧ P t))" by simp
  then show ?thesis
    apply (rule refines_rel_prod_assume_on_exit) 
    subgoal using cleanup by blast
    subgoal using emp by blast
    subgoal using conseq by auto
    done
qed

locale L2_heap_raw_state = sim_stack_heap_raw_state hrs_a hrs_upd_a hrs_c hrs_upd_c  S 
  for
    hrs_a:: "'s_a → heap_raw_state" and
    hrs_upd_a:: "(heap_raw_state → heap_raw_state) → 's_a → 's_a" and

    hrs_c:: "'s_c → heap_raw_state" and
    hrs_upd_c:: "(heap_raw_state → heap_raw_state) → 's_c → 's_c" and
    S::"addr set" +
  fixes st:: "'s_c → 's_a"
  assumes hrs_htd_st: "∧s. hrs_htd (hrs_a (st s)) = hrs_htd (hrs_c s)"
  assumes hrs_upd_st: "∧s f. (hrs_upd_a f (st s)) = st (hrs_upd_c f s)"

begin
sublocale L2   
  "λs. hrs_htd (hrs_a s)" "λupd. hrs_upd_a (hrs_htd_update upd)" 
  "λs. hrs_mem (hrs_a s)" "λupd. hrs_upd_a (hrs_mem_update upd)" 
  "λs. hrs_htd (hrs_c s)" "λupd. hrs_upd_c (hrs_htd_update upd)" 
  "λs. hrs_mem (hrs_c s)" "λupd. hrs_upd_c (hrs_mem_update upd)" 
  S
  apply (unfold_locales)
  subgoal using hrs_htd_st by simp
  subgoal using hrs_upd_st by simp
  subgoal using hrs_upd_st by simp
  done
end

locale typ_heap_typing = pointer_lense r w + heap_typing_state heap_typing heap_typing_upd 
  for 
    r:: "'t → ('a::xmem_type) ptr → 'a" and 
    w:: "'a ptr → ('a → 'a) → 't → 't" and
    heap_typing :: "'t → heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc → heap_typ_desc) → 't → 't" and
    S:: "addr set" 
begin

definition stack_ptr_acquire :: "nat → 'a list → 'a ptr → heap_typ_desc → 't → 't"
  where "stack_ptr_acquire n vs p d s =
     (fold (λi. w (p +_p int i) (λ_. (vs ! i))) [0..<n]) (heap_typing_upd (λ_. d) s)"

definition stack_ptr_release :: "nat → 'a ptr → 't → 't" 
  where "stack_ptr_release n p s =
     (heap_typing_upd (stack_releases n p) o (fold (λi. w (p +_p int i) (λ_. c_type_class.zero)) [0..<n])) s"

definition assume_stack_alloc:: "nat → ('t → ('a::xmem_type) list set) → ('e::default, 'a ptr, 't) spec_monad" where
 "assume_stack_alloc n init ≡ assume_result_and_state (λs. {(p, t).
         ∃d vs. (p, d) ∈ stack_allocs n S TYPE('a::xmem_type) (heap_typing s) ∧
                vs ∈ init s ∧
                length vs = n ∧
                (∀i ∈ {0..<n}. r s (p +_p int i) = ZERO('a::xmem_type)) ∧
                t = stack_ptr_acquire n vs p d s})"

definition guard_with_fresh_stack_ptr :: "nat → ('t → 'a list set) → ('a::xmem_type ptr → ('e::default, 'v, 't) spec_monad) → ('e, 'v, 't) spec_monad" where
"guard_with_fresh_stack_ptr n init c ≡
  do {
    p ← assume_stack_alloc n init;
    guard_on_exit (c p)
       (λs. ∀i < n. root_ptr_valid (heap_typing s) (p +_p int i))
       {(s, t). t = stack_ptr_release n p s}
  }"

definition assume_with_fresh_stack_ptr :: "nat → ('t → 'a list set) → ('a::xmem_type ptr → ('e::default,'v, 't) spec_monad) → ('e, 'v, 't) spec_monad" where
"assume_with_fresh_stack_ptr n init c ≡
  do {
    p ← assume_stack_alloc n init;
    assume_on_exit (c p)
       (λs. ∀i < n. root_ptr_valid (heap_typing s) (p +_p int i))
       {(s, t). t = stack_ptr_release n p s}
  }"

definition with_fresh_stack_ptr :: "nat → ('t → 'a list set) → ('a::xmem_type ptr → ('e::default,'v, 't) spec_monad) → ('e, 'v, 't) spec_monad" where
"with_fresh_stack_ptr n init c ≡
  do {
    p ← assume_stack_alloc n init;
    on_exit (c p)
       {(s, t). t = stack_ptr_release n p s}
  }"

lemma monotone_guard_with_fresh_stack_ptr_le[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≤) (λf. c f p)"  
  shows "monotone R (≤) (λf. guard_with_fresh_stack_ptr n I (c f))"
  unfolding guard_with_fresh_stack_ptr_def
  by (intro partial_function_mono)

lemma monotone_guard_with_fresh_stack_ptr_ge[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≥) (λf. c f p)"  
  shows "monotone R (≥) (λf. guard_with_fresh_stack_ptr n I (c f))"
  unfolding guard_with_fresh_stack_ptr_def
  by (intro partial_function_mono)

lemma mono_guard_with_fresh_stack_ptr [monad_mono_intros]:
  "(∧p. f p ≤ g p) ==> guard_with_fresh_stack_ptr n I f ≤ guard_with_fresh_stack_ptr n I g"
  unfolding guard_with_fresh_stack_ptr_def assume_stack_alloc_def on_exit'_def
  apply (intro monad_mono_intros gfp.leq_refl le_funI)
  by (simp add: le_fun_def)

lemma monotone_assume_with_fresh_stack_ptr_le[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≤) (λf. c f p)"  
  shows "monotone R (≤) (λf. assume_with_fresh_stack_ptr n I (c f))"
  unfolding assume_with_fresh_stack_ptr_def
  by (intro partial_function_mono)

lemma monotone_assume_with_fresh_stack_ptr_ge[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≥) (λf. c f p)"  
  shows "monotone R (≥) (λf. assume_with_fresh_stack_ptr n I (c f))"
  unfolding assume_with_fresh_stack_ptr_def
  by (intro partial_function_mono)

lemma mono_assume_with_fresh_stack_ptr [monad_mono_intros]:
  "(∧p. f p ≤ g p) ==> assume_with_fresh_stack_ptr n I f ≤ assume_with_fresh_stack_ptr n I g"
  unfolding assume_with_fresh_stack_ptr_def assume_stack_alloc_def on_exit'_def
  apply (intro monad_mono_intros gfp.leq_refl le_funI)
  by (simp add: le_fun_def)

lemma monotone_with_fresh_stack_ptr_le[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≤) (λf. c f p)"  
  shows "monotone R (≤) (λf. with_fresh_stack_ptr n I (c f))"
  unfolding with_fresh_stack_ptr_def on_exit_def
  by (intro partial_function_mono)

lemma monotone_with_fresh_stack_ptr_ge[partial_function_mono]:
  assumes [partial_function_mono]: "∧p. monotone R (≥) (λf. c f p)"  
  shows "monotone R (≥) (λf. with_fresh_stack_ptr n I (c f))"
  unfolding with_fresh_stack_ptr_def on_exit_def
  by (intro partial_function_mono)

lemma mono_with_fresh_stack_ptr [monad_mono_intros]:
  "(∧p. f p ≤ g p) ==> with_fresh_stack_ptr n I f ≤ with_fresh_stack_ptr n I g"
  unfolding with_fresh_stack_ptr_def assume_stack_alloc_def on_exit_def on_exit'_def
  apply (intro monad_mono_intros gfp.leq_refl le_funI)
  by (simp add: le_fun_def)

lemma refines_rel_xval_guard_with_fresh_stack_ptr:
  assumes init_eq: "init_c s = init_a s"
  assumes f: "∧s p. refines (f_c p) (f_a p) s s (rel_prod (rel_xval L R) (=))"
  shows 
    "refines
      (guard_with_fresh_stack_ptr n init_c (L2_VARS f_c nm))
      (guard_with_fresh_stack_ptr n init_a (L2_VARS f_a nm)) s s
      (rel_prod (rel_xval L R) (=))"
  unfolding guard_with_fresh_stack_ptr_def L2_VARS_def on_exit'_def assume_stack_alloc_def
  apply (rule refines_bind')
  apply (subst refines_assume_result_and_state_iff)
  apply (subst init_eq)
  apply (rule sim_set_refl)
  apply clarsimp
  apply (rule refines_bind_exception_or_result'[OF f])
  apply (rule refines_bind')
  apply (rule refines_bind')
  apply (rule refines_guard)
  apply simp_all
  apply (rule refines_assert_result_and_state)
  apply simp_all
  done


lemma refines_rel_xval_assume_with_fresh_stack_ptr:
  assumes init_eq: "init_c s = init_a s"
  assumes f: "∧s p. refines (f_c p) (f_a p) s s (rel_prod (rel_xval L R) (=))"
  shows 
    "refines
      (assume_with_fresh_stack_ptr n init_c (L2_VARS f_c nm))
      (assume_with_fresh_stack_ptr n init_a (L2_VARS f_a nm)) s s
      (rel_prod (rel_xval L R) (=))"
  unfolding assume_with_fresh_stack_ptr_def L2_VARS_def on_exit'_def assume_stack_alloc_def
  apply (rule refines_bind')
  apply (subst refines_assume_result_and_state_iff)
  apply (subst init_eq)
  apply (rule sim_set_refl)
  apply clarsimp
  apply (rule refines_bind_exception_or_result'[OF f])
  apply (rule refines_bind')
  apply (rule refines_bind')
  apply (rule refines_assuming)
  apply simp_all
  apply (rule refines_assert_result_and_state)
  apply simp_all
  done

lemma refines_rel_xval_with_fresh_stack_ptr:
  assumes init_eq: "init_c s = init_a s"
  assumes f: "∧s p. refines (f_c p) (f_a p) s s (rel_prod (rel_xval L R) (=))"
  shows 
    "refines
      (with_fresh_stack_ptr n init_c (L2_VARS f_c nm))
      (with_fresh_stack_ptr n init_a (L2_VARS f_a nm)) s s
      (rel_prod (rel_xval L R) (=))"
  unfolding with_fresh_stack_ptr_def L2_VARS_def assume_stack_alloc_def
  apply (rule refines_bind_no_throw [where Q = "rel_prod (rel_xval (λ_ _. False) (=)) (=)"])
  apply simp
    apply simp
  subgoal using init_eq by (auto simp add: refines_def_old rel_xval.simps) 
  subgoal 
    apply clarsimp
    apply (rule refines_rel_xval_on_exit)
    apply (rule f)
    done
  done

(* This is not in pointer_lense, since the lemma depends on the xmem type class *)
lemma write_same_ZERO:
  "r s p = ZERO('a) ==> w p (λy. ZERO('a)) s = s"
  using write_same by simp

end

lemma refines_rel_prod_eq_on_exit:
  assumes f: "refines f_c f_a s s (rel_prod Q (=))"
  shows "refines
        (on_exit f_c cleanup)
        (on_exit f_a cleanup) s s
        (rel_prod Q (=))"
  unfolding on_exit_bind_exception_or_result_conv
  apply (rule refines_bind_exception_or_result')
   apply (rule f)
  apply clarsimp
  apply (rule refines_bind_no_throw )
  apply simp
  apply simp
   apply (rule refines_state_select_same)
  apply clarsimp
  done

context stack_heap_state
begin
lemma refines_rel_prod_with_fresh_stack_ptr:
  assumes init_eq: "init_c s = init_a s"
  assumes f: "∧s p. refines (f_c p) (f_a p) s s (rel_prod Q (=))"
  shows 
    "refines
       (with_fresh_stack_ptr n init_c (L2_VARS f_c nm))
       (with_fresh_stack_ptr n init_a (L2_VARS f_a nm)) s s
       (rel_prod Q (=))"
  unfolding with_fresh_stack_ptr_def L2_VARS_def
  apply (rule refines_bind_no_throw )
     apply simp
    apply simp
   apply (rule refines_assume_result_and_state_same')
   apply (simp only: init_eq)
  apply clarsimp
  apply (rule refines_rel_prod_eq_on_exit)
  apply (rule f)
  done
end

lemma h_val_coerce_ptr_coerce_packed:
  fixes p::"'c::packed_type ptr"
  assumes sz_eq: "size_of TYPE('c) = size_of TYPE('a::packed_type)" 
  shows "h_val h (PTR_COERCE ('c → 'a) p) = COERCE ('c → 'a) (h_val h p)"
  by (simp add:  h_val_def sz_eq from_bytes_def coerce_def to_bytes_p_def to_bytes_def 
      packed_type_access_ti access_ti₀_def field_access_update_same(1) 
      size_of_fold sz_eq td_fafu_idem update_ti_t_def)


lemma h_val_field_ptr_coerce_from_bytes_packed:
  fixes p::"'c::packed_type ptr"
  assumes "field_ti TYPE('a) f = Some t"
  assumes "export_uinfo t = export_uinfo (typ_info_t TYPE('b::mem_type))"
  assumes [simp]: "size_of TYPE('c) = size_of TYPE('a)" 
  shows "h_val h (PTR('b) &((PTR_COERCE('c::packed_type → 'a::packed_type) p)→f)) =
           from_bytes (access_ti₀ t (COERCE ('c → 'a) (h_val h p)))"
  apply (simp add:h_val_coerce_ptr_coerce_packed[symmetric]) 
  apply (rule h_val_field_from_bytes' [OF assms(1) assms(2)])
  done


lemma packed_type_value_update_ti_explode: 
  "(v::'a::packed_type) = update_ti (typ_info_t TYPE('a)) (to_bytes_p v) v'"
  by (simp add: size_of_def update_ti_s_from_bytes update_ti_update_ti_t)

lemma packed_type_to_bytes_to_bytes_p_conv: 
  "length bs = size_of TYPE('a::packed_type) ==> to_bytes v bs = to_bytes_p (v::'a)"
  apply (simp add: to_bytes_p_def)
  by (simp add: packed_type_access_ti to_bytes_def)

lemma packed_type_to_byte_p_coerce:
  assumes sz:"size_of TYPE('c::packed_type) = size_of TYPE('a::packed_type)" 
  shows  "to_bytes_p (COERCE('a → 'c) v) = to_bytes_p v" 
  using sz
  apply (simp add: to_bytes_p_def coerce_def)
  by (metis (mono_tags, lifting) field_access_update_same(1) field_desc.simps(2) field_desc_def 
      from_bytes_def len length_replicate size_of_fold td_fafu_idem to_bytes_def 
      update_ti_t_def wf_fd)

lemma to_bytes_coerce_packed: 
  "size_of TYPE('a) = size_of TYPE('b) ==> length bs = size_of TYPE('a) ==>
  to_bytes (COERCE('a::packed_type→'b::packed_type) v) bs = to_bytes v bs"
  by (simp add: coerce_def field_access_update_same(1) from_bytes_def packed_type_access_ti 
      size_of_def td_fafu_idem to_bytes_def update_ti_t_def)

lemma heap_update_ptr_coerse_packed:
  fixes p::"'c::packed_type ptr"
  assumes cgrd: "c_guard p"
  assumes [simp]: "size_of TYPE('c) = size_of TYPE('a::packed_type )" 
  shows "heap_update (PTR_COERCE('c → 'a) p) v = heap_update p (COERCE('a →'c) v)"
  apply (rule ext)
  apply (simp add: heap_update_def packed_type_to_bytes_to_bytes_p_conv packed_type_to_byte_p_coerce)
  done

lemma c_guard_ptr_coerceI: 
  "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a)) ==>
  align_td (typ_info_t TYPE('a)) ≤ align_td (typ_info_t TYPE('c)) ==>
  c_guard p ==>
  c_guard (PTR_COERCE('c::c_type→'a::c_type) p)"
  apply (cases p)
  using power_le_dvd
  by (auto simp add: c_guard_def c_null_guard_def ptr_aligned_def align_of_def size_of_def)
 

lemma heap_update_field_ptr_coerce_from_bytes_packed:
  fixes p::"'c::{xmem_type, packed_type} ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a::{xmem_type, packed_type})) f 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t (TYPE('b::{xmem_type}))"
  assumes cgrd: "c_guard (PTR_COERCE('c→ 'a) p)"
  assumes sz[simp]: "size_of TYPE('c) = size_of TYPE('a)" 
  shows "heap_update (PTR('b) &((PTR_COERCE('c→ 'a) p)→f)) v h =
           heap_update p (coerce_map (update_ti t (to_bytes_p v)) (h_val h p)) h"
  apply (subst heap_update_field_root_conv' [OF  fl match cgrd])
  apply (simp add: heap_update_def h_val_coerce_ptr_coerce_packed )
  apply (subst coerce_coerce_map_cancel_packed[OF sz[symmetric], symmetric])
  apply (simp add: coerce_map_def)
  apply (subst to_bytes_coerce_packed)
    apply (simp_all)
  done


named_theorems L2_modify_heap_update_field_root_conv

context heap_state
begin
lemma heap_update_field_root_conv:
  fixes p::"'a::xmem_type ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update ∘ (λx _. x)), n)"
  assumes fg_cons: "fg_cons fld (fld_update ∘ (λx _. x))"
  assumes cgrd: "c_guard p"
  shows "(hmem_upd (heap_update (PTR('b) &(p→f)) v)) =
          (λs. (hmem_upd (heap_update p (fld_update (λ_. v) (h_val (hmem s) p)))) s)"
  apply (subst heap_update_field_root_conv_pointless' [OF fl fg_cons cgrd])
  apply (rule ext)
  by (metis (mono_tags, lifting) heap.upd_cong)

lemma heap_update_field_root_conv':
  fixes p::"'a::xmem_type ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
  assumes cgrd: "c_guard p"
  shows "(hmem_upd (heap_update (PTR('b) &(p→f)) v)) =
          (λs. (hmem_upd (heap_update p (update_ti t (to_bytes_p v) (h_val (hmem s) p)))) s)"
  using heap_update_field_root_conv' [OF fl match cgrd, of v]
  using heap.upd_cong by blast

lemma L2_modify_heap_update_field_root_conv:
  fixes p::"'a::xmem_type ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update ∘ (λx _. x)), n)"
  assumes fg_cons: "fg_cons fld (fld_update ∘ (λx _. x))"
  assumes cgrd: "c_guard p"
  shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &(p>→f)) (v s)) s) =
         L2_modify (λs. (hmem_upd (heap_update p (fld_update (λ_. v s) (h_val (hmem s) p)))) s)"
  by (simp add:  heap_update_field_root_conv [OF fl fg_cons cgrd])

lemma L2_modify_heap_update_field_root_conv' [L2_modify_heap_update_field_root_conv]:
  fixes p::"'a::xmem_type ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
  assumes cgrd: "c_guard p"
  shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &(p>→f)) (v s)) s) =
         L2_modify (λs. (hmem_upd (heap_update p (update_ti t (to_bytes_p (v s)) (h_val (hmem s) p)))) s)"
  by (simp add:  heap_update_field_root_conv' [OF fl match cgrd])


lemma L2_modify_heap_update_ptr_coerce_packed_conv':
  fixes p::"'c::packed_type ptr"
  assumes cgrd: "c_guard p"
  assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a::packed_type))" 
  shows "L2_modify (λs. hmem_upd (heap_update (PTR_COERCE('c → 'a) p) (COERCE('c → 'a) (v s))) s) =
         L2_modify (λs. (hmem_upd (heap_update p (v s))) s)"
  using  heap_update_ptr_coerse_packed [simplified size_of_def, OF cgrd sz] heap.upd_cong
  by (metis assms(2) coerce_cancel_packed size_of_def)

lemma L2_modify_heap_update_ptr_coerce_packed_conv[L2_modify_heap_update_field_root_conv]:
  fixes p::"'c::packed_type ptr"
  assumes cgrd: "c_guard p"
  assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a::packed_type))" 
  shows "L2_modify (λs. hmem_upd (heap_update (PTR_COERCE('c → 'a) p) (v s)) s) =
         L2_modify (λs. (hmem_upd (heap_update p (COERCE('a → 'c) (v s)))) s)"
  using  heap_update_ptr_coerse_packed [simplified size_of_def, OF cgrd sz] heap.upd_cong
  by (metis assms(2) coerce_cancel_packed size_of_def)

lemma L2_modify_heap_update_ptr_coerce_packed_field_root_conv [L2_modify_heap_update_field_root_conv]:
  fixes p::"'c::{xmem_type, packed_type} ptr"
  assumes fl: "field_lookup (typ_info_t TYPE('a::{xmem_type, packed_type})) f 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
  assumes cgrd: "c_guard (PTR_COERCE('c→ 'a) p)"
  assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a))" 
  shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &((PTR_COERCE('c>→ 'a) p)→f)) (v s)) s) =
         L2_modify (λs. (hmem_upd (heap_update p (coerce_map (update_ti t (to_bytes_p (v s))) (h_val (hmem s) p)))) s)"
  using heap_update_field_ptr_coerce_from_bytes_packed [simplified size_of_def, OF fl match cgrd sz] heap.upd_cong
  by meson
end


lemma L2_try_state_asssumeE_bindE:
  "L2_try (assume_result_and_state P >>= f) = assume_result_and_state P >>= (λx. L2_try (f x))"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff L2_defs)
  done

lemma refines_L2_try_L2_seq_nondet:
  assumes g [unfolded THIN_def, rule_format]: "PROP THIN (∧v t. refines (L2_try (g v)) (g' v) t t (rel_prod rel_liftE (=)))"
  assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
  shows "refines (L2_try (L2_seq f g)) (f' >>= g') s s (rel_prod rel_liftE (=))"
  unfolding L2_try_def L2_seq_def try_nested_bind_exception_or_result_conv
  using g f
  apply (clarsimp simp add: refines_def_old L2_defs succeeds_bind reaches_bind reaches_try succeeds_bind_exception_or_result 
      rel_liftE_def unnest_exn_def reaches_bind_exception_or_result succeeds_bind_exception_or_result  split: xval_splits sum.splits)
  apply (intro conjI allI impI)
   apply (metis case_xval_simps(2) )
  apply clarsimp
  subgoal for r s' r'
    apply (cases r)
    subgoal
      apply (cases r')
      subgoal       
        apply (clarsimp simp add: default_option_def Exn_def [symmetric])
        by (meson Exn_neq_Result obj_sumE)

      subgoal
        apply (clarsimp simp add: default_option_def Exn_def [symmetric])
        subgoal for s1 y r1
          apply (cases r1)
          subgoal
            apply (clarsimp simp add: default_option_def Exn_def [symmetric])
            by (metis Exn_neq_Result Result_eq_Result case_xval_simps(1) old.sum.simps(5) sum_all_ex(2))
          subgoal
            by (auto simp add: default_option_def Exn_def [symmetric])
          done
        done
      done
    subgoal
      apply (cases r')

      subgoal       
        apply (clarsimp simp add: default_option_def Exn_def [symmetric])
        by (meson Exn_neq_Result sum_all_ex(2))
      subgoal       
        apply (clarsimp simp add: default_option_def Exn_def [symmetric])
        subgoal for s1 r1
          apply (cases r1)
          subgoal
            apply (clarsimp simp add: default_option_def Exn_def [symmetric])
            by (metis Result_eq_Result case_xval_simps(1) old.sum.simps(6) sum_all_ex(2))
          subgoal
            by (metis case_xval_simps(2))
          done
        done
      done
    done
  done



lemma refines_L2_try_pure:
  assumes f: "refines f (return f') s s (rel_prod rel_liftE (=))"
  shows "refines (L2_try f) (return f') s s (rel_prod rel_liftE (=))"
  unfolding L2_defs L2_guarded_def using f
  by (fastforce simp add: refines_def_old reaches_try rel_liftE_def)


lemma refines_liftE_conv: "refines f f' s t (rel_prod rel_liftE (=)) ⟷
 refines f (liftE f') s t (=)"
 unfolding L2_defs L2_guarded_def 
  by (auto simp add: refines_def_old reaches_liftE rel_liftE_def)

lemma refines_rel_liftE_L2_try_on_exit:
  assumes f: "refines f_c f_a s s (rel_prod rel_liftE (=))"
  shows "refines (L2_try (on_exit f_c cleanup)) (on_exit f_a cleanup) s s (rel_prod rel_liftE (=))"
  using f unfolding L2_defs try_def refines_map_value_left_iff
  apply (rule refines_rel_prod_eq_on_exit[THEN refines_weaken])
  apply (auto simp: rel_liftE_def)
  done


lemma map_value_on_exit:
  "map_value g (on_exit f cleanup) = on_exit (map_value g f) cleanup"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff on_exit_def on_exit'_def)
  done

lemma L2_try_on_exit: "L2_try (on_exit f cleanup) = on_exit (L2_try f) cleanup"
  unfolding L2_try_def try_def
  by (simp add: map_value_on_exit)


context stack_heap_state
begin
lemma L2_try_with_fresh_stack_ptr: 
  "L2_try (with_fresh_stack_ptr n init f) = with_fresh_stack_ptr n init (λp. L2_try (f p))"
  by (simp add: with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE L2_try_on_exit)
end

lemma map_value_guard_on_exit:
  "map_value g (guard_on_exit f P cleanup) = guard_on_exit (map_value g f) P cleanup"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff on_exit'_def)
  done


lemma L2_try_guard_on_exit:
  "L2_try (guard_on_exit f P cleanup) = guard_on_exit (L2_try f) P cleanup"
  unfolding L2_try_def try_def
  by (simp add: map_value_guard_on_exit)


lemma map_value_assume_on_exit:
  "map_value g (assume_on_exit f P cleanup) = assume_on_exit (map_value g f) P cleanup"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff on_exit'_def)
  done

lemma L2_try_assume_on_exit:
  "L2_try (assume_on_exit f P cleanup) = assume_on_exit (L2_try f) P cleanup"
  unfolding L2_try_def try_def
  by (simp add: map_value_assume_on_exit)

context typ_heap_typing
begin
lemma L2_try_guard_with_fresh_stack_ptr:
  "L2_try (guard_with_fresh_stack_ptr n init f) = guard_with_fresh_stack_ptr n init (λp. L2_try (f p))"
  unfolding guard_with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def 
    L2_try_guard_on_exit ..

lemma L2_try_assume_with_fresh_stack_ptr:
  "L2_try (assume_with_fresh_stack_ptr n init f) = assume_with_fresh_stack_ptr n init (λp. L2_try (f p))"
  unfolding assume_with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def 
    L2_try_assume_on_exit ..

lemma L2_try_with_fresh_stack_ptr:
  "L2_try (with_fresh_stack_ptr n init f) = with_fresh_stack_ptr n init (λp. L2_try (f p))"
  by (simp add: with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def
      L2_try_on_exit)
end

lemma refines_L2_seq:
  assumes f: "refines f f' s s' Q"
  assumes ll: "∧e e' t t'. Q (Exn e, t) (Exn e', t') ==> R (Exn e, t) (Exn e', t')"
  assumes lr: "∧e v' t t'. Q (Exn e, t) (Result v', t') ==> refines (throw e) (g' v') t t' R"
  assumes rl: "∧v e' t t'. Q (Result v, t) (Exn e', t') ==> refines (g v) (throw e') t t' R"
  assumes rr: "∧v v' t t'. Q (Result v, t) (Result v', t') ==> refines (g v) (g' v') t t' R"
  shows "refines (L2_seq f g) (L2_seq f' g') s s' R"
  unfolding L2_seq_def using f ll lr rl rr
  by (rule refines_bind_bind_exn)


lemma rel_Nonlocal_Nonlocal: "rel_Nonlocal (Nonlocal x) x"
  by (simp add: rel_Nonlocal_def)

lemmas rel_sum_Inl = rel_sum.intros(1)
lemmas rel_sum_Inr = rel_sum.intros(2)

lemma rel_sum_eq: "rel_sum (=) (=) x x"
  by (auto simp add: rel_sum.simps)


definition (in heap_state)  
  IO_modify_heap_padding::"'a::mem_type ptr → ('s → 'a) → ('b::default, unit, 's) spec_monad" where
 "IO_modify_heap_padding p v =
    state_select {(s, t). ∃bs. length bs = size_of (TYPE('a)) ∧ t = hmem_upd (heap_update_padding p (v s) bs) s}"

lemma (in heap_state) liftE_IO_modify_heap_padding: "liftE (IO_modify_heap_padding p v) = (IO_modify_heap_padding p v)"
  unfolding IO_modify_heap_padding_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

abbreviation (in heap_state) IO_modify_heap_paddingE:: 
    "'a::mem_type ptr → ('s → 'a) → ('b, unit, 's) exn_monad" where
    "IO_modify_heap_paddingE p v ≡ liftE (IO_modify_heap_padding p v)"

lemma (in heap_state) no_fail_IO_modify_padding[simp]:  "succeeds (IO_modify_heap_padding p v) s"
  unfolding IO_modify_heap_padding_def
  apply (simp)
  using length_to_bytes_p by blast

lemma (in heap_state) no_fail_IO_modify_paddingE[simp]:  "succeeds (IO_modify_heap_paddingE p v) s"
  unfolding IO_modify_heap_padding_def
  apply (simp)
  using length_to_bytes_p by blast

end