Theory In_Out_Parameters

(*
 * Copyright (c) 2023 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "In Out Parameter Refinement"

theory In_Out_Parameters
  imports
    L2ExceptionRewrite
    L2Peephole
    TypHeapSimple 
    Stack_Typing
begin


lemma map_exn_catch_conv: "map_value (map_exn f) m = (m <catch> (λr. throw (f r)))"
  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

abbreviation "L2_return x ns   liftE (L2_VARS (return x) ns)"

lemma L2_return_L2_gets_conv: "L2_return x ns = L2_gets (λ_. x) ns"
  unfolding L2_defs L2_VARS_def
  by (simp add: gets_return)


lemma return_L2_gets_conv: "(return x) = L2_gets (λ_. x) []"
  unfolding L2_defs L2_VARS_def
  by (simp add: gets_return)


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

named_theorems refines_right_eq

lemma (in heap_state) IO_modify_heap_paddingE_root_refines':
  fixes p::"'a::xmem_type ptr"
  fixes fld_update::"('b::xmem_type  'b)  'a  'a"
  assumes fg_cons: "fg_cons fld (fld_update  (λx _. x))"
  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 cgrd: "c_guard p"
  shows "refines 
           (IO_modify_heap_paddingE (PTR('b) &(pf)) v)  
           (IO_modify_heap_paddingE p (λs. (fld_update (λ_. v s)) (h_val (hmem s) p))) 
          s s ((=))"
proof -
  {
    fix r t
    assume exec: "reaches (IO_modify_heap_paddingE (PTR('b) &(pf)) v) s r t" 
    have "reaches (IO_modify_heap_paddingE p (λs. fld_update (λ_. v s) (h_val (hmem s) p))) s r t"
    proof -
      from exec obtain bs where
        r: "r = Result ()" and bs: "length bs = size_of TYPE('b)" and
        t: "t = hmem_upd (heap_update_padding (PTR('b) &(pf)) (v s) bs) s" 
        unfolding liftE_IO_modify_heap_padding
        by (auto simp add:  IO_modify_heap_padding_def)
      note root_conv = heap_update_padding_field_root_conv'' [OF fl fg_cons cgrd bs, where v="v s" and hp = "hmem s"]
      from bs cgrd fl have *: "length (super_update_bs bs (heap_list (hmem s) (size_of TYPE('a)) (ptr_val p)) n) = size_of TYPE('a)"
        apply (subst length_super_update_bs)
        subgoal
          by (metis add.commute field_lookup_offset_size heap_list_length size_of_tag typ_desc_size_update_ti typ_uinfo_size)
        subgoal
          using heap_list_length by blast
        done
      show ?thesis 
        unfolding liftE_IO_modify_heap_padding
        apply (clarsimp simp add: IO_modify_heap_padding_def r)
        using root_conv heap.upd_cong * t 
        by blast
    qed
  } note * = this
  show ?thesis
    using *   
    by (auto simp add: refines_def_old )
qed

lemma (in heap_state) IO_modify_heap_paddingE_root_refines'':
  fixes p::"'a::xmem_type ptr"
  fixes fld_update::"('b::xmem_type  'b)  'a  'a"
  assumes fg_cons: "fg_cons fld (fld_update  (λx _. x))"
  assumes fl: "field_ti TYPE('a) f = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update  (λx _. x)))"
  assumes cgrd: "c_guard p"
  shows "refines 
           (IO_modify_heap_paddingE (PTR('b) &(pf)) v)  
           (IO_modify_heap_paddingE p (λs. (fld_update (λ_. v s)) (h_val (hmem s) p))) 
          s s ((=))"
proof -
  from fl obtain n where 
    "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)"
    using field_ti_field_lookupE by blast
  from IO_modify_heap_paddingE_root_refines' [OF fg_cons this cgrd]
  show ?thesis .
qed

lemma (in heap_state) IO_modify_heap_paddingE_root_refines [refines_right_eq]:
  fixes p::"'a::xmem_type ptr"
  fixes fld_update::"('b::xmem_type  'b)  'a  'a"
  assumes v': "s. v' s = ((fld_update (λ_. v s)) (h_val (hmem s) p))"
  assumes fg_cons: "fg_cons fld (fld_update  (λx _. x))"
  assumes fl: "field_ti TYPE('a) f = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update  (λx _. x)))"
  assumes cgrd: "c_guard p"
  shows "refines 
           (IO_modify_heap_paddingE (PTR('b) &(pf)) v)  
           (IO_modify_heap_paddingE p v')
          s s ((=))"
  unfolding v'
  by (rule IO_modify_heap_paddingE_root_refines'' [OF fg_cons fl cgrd])


lemma refines_subst_right:
  assumes f_g: "refines f g s t Q"
  assumes refines_eq: "refines g g' t t ((=))"
  shows "refines f g' s t Q"
  using f_g refines_eq
  by (force simp add: refines_def_old)
 
lemma refines_right_eq_id: "refines f f s s ((=))"
  by (force simp add: refines_def_old)

lemma refines_subst_left:
  assumes f_g: "refines f g s t Q"
  assumes f_eq: "run f s = run f' s"
  shows "refines f' g s t Q"
  using f_g f_eq
  apply (auto simp add: refines_def_old reaches_def succeeds_def)
  done

lemma refines_right_eq_L2_seq [refines_right_eq]:
  assumes f1: "refines f1 g1 s s ((=))"
  assumes f2: "v t. refines (f2 v) (g2 v) t t ((=))"
  shows "refines (L2_seq f1 f2) (L2_seq g1 g2) s s ((=))"
  unfolding L2_defs
  apply (rule refines_bind_bind_exn [OF f1])
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal using f2 by auto
  done


lemma refines_right_eq_L2_guard':
  assumes "Q s  P s"
  assumes "Q s  refines X X' s s (=)"
  shows "refines (L2_seq (L2_guard P) (λ_. X)) (L2_seq (L2_guard Q) (λ_. X')) s s ((=))"
  unfolding L2_defs
  apply (rule refines_bind'[OF
    refines_guard[THEN refines_strengthen[OF _ runs_to_partial_guard runs_to_partial_guard]]])
  apply (auto simp: assms)
  done

lemma refines_right_eq_L2_guard:
  assumes "Q  P"
  assumes "Q  refines X X' s s (=)"
  shows "refines (L2_seq (L2_guard (λ_. P)) (λ_. X)) (L2_seq (L2_guard (λ_. Q)) (λ_. X')) s s ((=))"
  using assms
  by (rule refines_right_eq_L2_guard')


lemma select_UNIV_L2_unknown_conv: "(select UNIV) = L2_unknown ns"
  unfolding L2_defs
  by simp

lemma select_singleton_conv: "((select ({x})) >>= g) = g x"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma hd_UNIV: "hd ` UNIV  UNIV"
  by (rule subset_UNIV)

lemma hd_singleton: "hd ` {[x]}  {x}"
  by simp

lemma refines_select_right_witness:
  assumes "x  X"
  assumes "refines f (g x) s t Q"
  shows "refines f ((select X) >>= g) s t Q"
  using assms
  using assms
  by (fastforce simp add: refines_def_old succeeds_bind reaches_bind)
  

lemma refines_bindE_right: 
  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 ((return v)) (throw e') t t' R"
  assumes rr: "v v' t t'. Q (Result v, t) (Result v', t')  refines ((return v)) (g' v') t t' R"
  shows "refines f (f' >>= g') s s' R"
proof -
  have eq: "f = (f >>= (λv. return v))"
    by simp
  show ?thesis
    apply (subst eq)
    using assms
    by (rule refines_bind_bind_exn)
qed

lemma refines_exec_modify_step_right: 
  assumes "refines (return x) g s (upd t) Q"
  shows "refines (return x) (do{ _ <- (modify (upd)); g }) s t Q"
  using assms
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma (in heap_state) refines_exec_IO_modify_heap_padding_step_right: 
  fixes p:: "'a::mem_type ptr"
  assumes "
    refines (return x) g s 
       (hmem_upd (heap_update_padding p v (heap_list (hmem s) (size_of TYPE('a)) (ptr_val p) )) t) Q"
  shows "refines (return x) (do { _ <- IO_modify_heap_paddingE p (λ_. v); g }) s t Q"
  using assms unfolding liftE_IO_modify_heap_padding
  apply (clarsimp simp add: refines_def_old IO_modify_heap_padding_def reaches_bind succeeds_bind  )
  apply (metis heap_list_length)
  done


lemma (in heap_state) refines_exec_IO_modify_heap_padding_single_step_right: 
  fixes p:: "'a::mem_type ptr"
  assumes "Q (Result (), s) 
              (Result (), hmem_upd (heap_update_padding p (v t) (heap_list (hmem s) (size_of TYPE('a)) (ptr_val p))) t)"
  shows "refines (return ()) 
          (IO_modify_heap_paddingE p v) s t Q"
  using assms unfolding liftE_IO_modify_heap_padding
  apply (clarsimp simp add: refines_def_old IO_modify_heap_padding_def reaches_bind succeeds_bind)
  by (metis heap_list_length)

lemma (in heap_state) refines_exec_IO_modify_heap_padding_single_step_right_InL: 
  fixes p:: "'a::mem_type ptr"
  assumes "Q (Exn e, s) (Exn e', hmem_upd (heap_update_padding p (v t) (heap_list (hmem s) (size_of TYPE('a)) (ptr_val p))) t)"
  shows "refines (throw e) 
           (do { _ <- IO_modify_heap_paddingE p v;
                L2_throw e' ns
           })
          s t Q"
  unfolding L2_defs unfolding liftE_IO_modify_heap_padding
  using assms 
  apply (clarsimp simp add: refines_def_old IO_modify_heap_padding_def reaches_bind succeeds_bind Exn_def [symmetric])
  apply (metis heap_list_length)
  done

lemma refines_exec_gets_right: 
  assumes "Q (Result x, s) (Result (g t), t)"
  shows "refines (return x) (gets g) s t Q"
  using assms
  by (auto simp add: refines_def_old)


lemma refines_exec_L2_return_right: 
  assumes "Q (Result x, s) (Result w, t)"
  shows "refines (return (x)) (L2_return w ns) s t Q"
  using assms unfolding L2_VARS_def
  by (auto simp add: refines_def_old)

lemma f_catch_throw: "(f <catch> throw) = f"
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (clarsimp simp add: runs_to_def_old)
  by (metis Exn_def default_option_def exception_or_result_cases not_None_eq)

lemma refines_L2_catch_right:
  assumes f: "refines f g s t Q"
  assumes Res_Res: "v v' s' t'. Q (Result v, s') (Result v', t')  R (Result v, s') (Result v', t')"
  assumes Res_Exn: "v e' s' t'. Q (Result v, s') (Exn e', t')  refines (return v) (h e') s' t' R"
  assumes Exn_Res: "e v' s' t'. Q (Exn e, s') (Result v', t')  R (Exn e, s') (Result v', t')"
  assumes Exn_Exn: "e e' s' t'. Q (Exn e, s') (Exn e', t')  refines (throw e) (h e') s' t' R"
  shows "refines f (L2_catch g h) s t R" unfolding L2_defs
  apply (subst f_catch_throw[symmetric])
  apply (rule refines_catch [OF f])
  subgoal using Exn_Exn by auto
  subgoal using Exn_Res by (auto simp add: refines_def_old Exn_def [symmetric])
  subgoal using Res_Exn by (auto simp add: refines_def_old Exn_def [symmetric])
  subgoal using Res_Res by auto
  done

lemma L2_seq_gets_app_conv: "run (L2_seq (L2_gets f ns) g) s = run (g (f s)) s"
  unfolding L2_defs
  apply (auto simp add: run_bind)
  done


lemma refines_project_right:
  assumes f_g: "refines f g s t Q"
  assumes "run g t = run (g' (prj t)) t"
  shows "refines f (L2_seq (L2_gets prj ns) g') s t Q"
  unfolding L2_defs
  using assms
  apply (clarsimp simp add: refines_def_old reaches_bind succeeds_bind)
  apply (auto simp add: succeeds_def reaches_def)
  done

lemma refines_project_guard_right:
  assumes f_g: "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  assumes "P t  run g t = run (g' (prj t)) t"
  shows "refines f (L2_seq (L2_guard P) (λ_. (L2_seq (L2_gets prj ns) g'))) s t Q"
  using assms unfolding L2_defs
  apply (clarsimp simp add: refines_def_old reaches_bind succeeds_bind)
  apply (auto simp add: succeeds_def reaches_def)
  done



named_rules cguard_assms and alloc_assms and modifies_assms and disjoint_assms and
  disjoint_alloc and disjoint_stack_free and stack_ptr and h_val_globals_frame_eq and
  rel_alloc_independent_globals
synthesize_rules refines_in_out
add_synthesize_pattern refines_in_out =
[(Binding.make ("concrete_function", ), fn ctxt => fn i => fn t => 
     (case t of
        @{term_pat "Trueprop (refines (L2_modify (λs. ?glob_upd _ _)) _ _ _ _ )"} => glob_upd
      | @{term_pat "Trueprop (refines (L2_modify (?glob_upd _)) _ _ _ _ )"} => glob_upd
      | @{term_pat "Trueprop (refines ?f _ _ _ _ )"} => f
      | t => t))]


lemma refines_yield_both[simp]: "refines (return a) (return b) s t R  R (Result a, s) (Result b, t)"
  by (auto simp add: refines_def_old)

lemma disjoint_union_distrib: "A  (B  C) = {}  A  B = {}  A  C = {}"
  by blast

lemma inter_commute: "A  B = B  A" by blast
lemma disjoint_symmetric: "A  B = {}  B  A = {}"
  by auto
lemma disjoint_symmetric': "A  B  {}  B  A = {}"
  by auto

definition IOcorres:: " 
  ('s  bool) 
  ('s  ('e,'a) xval  's  bool) 
  ('s  't) 
  ('a  's  'b)  
  ('e  's  'e1)  
  ('e1, 'b, 't) exn_monad =>
  ('e, 'a, 's) exn_monad => bool" where
  "IOcorres P Q st rx ex fa fc  corresXF_post st rx ex P Q fa fc"

lemma IOcorres_id: "IOcorres (λ_. True) (λ _ _ _. True) (λs. s) (λr _. r) (λr _. r) f f"
  by (auto simp add: IOcorres_def corresXF_post_def split: xval_splits prod.splits)
lemmas IOcorres_skip = IOcorres_id

lemma IOcorres_trivial_from_local_var_extract:
  "L2corres st rx ex P A C  IOcorres (λ_. True) (λ _ _ _. True) (λs. s) (λr _. r) (λr _. r) A A"
  by (rule IOcorres_id)

lemma admissible_IOcorres [corres_admissible]: 
  "ccpo.admissible Inf (≥)  (λfa. IOcorres P Q st rx ex fa fc)"
  unfolding IOcorres_def
  by (rule admissible_nondet_ord_corresXF_post)

lemma IOcorres_top [corres_top]: "IOcorres P Q st rx ex  fc" 
  unfolding IOcorres_def
  by (rule corresXF_post_top)

lemma distinct_addresses_ptr_val_lemma: 
  "n < addr_card  ptr_val p + word_of_nat n  (λx. ptr_val p + word_of_nat x) ` {0..<n}"
  by auto (metis addr_card_len_of_conv nless_le order_le_less_trans unat_of_nat_eq)

lemma distinct_addresses_ptr_lemma:
  assumes bound: "n  addr_card"
  shows "distinct (map (λi. ptr_val p + of_nat i) [0..<n])"
  using bound
proof (induct n arbitrary: p)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc have hyp: "distinct (map (λi. ptr_val p + word_of_nat i) [0..<n])" by auto
  show ?case 
    apply (subst upt_Suc_snoc)
    apply (subst map_append) 
    apply (subst distinct_append)
    apply (simp add: hyp)
    using Suc.prems
    apply (simp add: distinct_addresses_ptr_val_lemma)
    done
qed


lemma array_intvl_Suc_split:"{a..+Suc n * m} = {a..+n * m}  {a + (word_of_nat (n*m))..+m}"
  by (metis add_diff_cancel_right' intvl_split le_add2 mult_Suc)


definition "rel_singleton_stack" :: "'a::c_type ptr  heap_mem  unit  'a  bool" 
where
 "rel_singleton_stack p h = (λ(_::unit) v.
    v = h_val h p)"

lemma domain_rel_singleton_stack:
  "equal_on (ptr_span p) h h'  rel_singleton_stack p h = rel_singleton_stack p h'"
  apply (clarsimp simp add: fun_eq_iff rel_singleton_stack_def)
  apply (metis (mono_tags, lifting) equal_on_def h_val_def heap_list_h_eq2)+
  done



named_theorems rel_stack_intros and rel_stack_simps



lemma rel_singleton_stack_simp [rel_stack_simps]:
  "rel_singleton_stack p h x v  v = h_val h p"
  by (auto simp add: rel_singleton_stack_def)

lemma rel_stack_refl [rel_stack_intros]: "(λ_. (=)) h x x"
  by auto

lemma rel_singleton_stackI [rel_stack_intros]: "rel_singleton_stack p h x (h_val h p)"
  by (auto simp add: rel_singleton_stack_def)

lemma rel_singleton_stack_condI [rel_stack_intros]: "h_val h p = y  rel_singleton_stack p h x y"
  by (auto simp add: rel_singleton_stack_def)

lemma fun_of_rel_singleton_stack[fun_of_rel_intros]: "fun_of_rel (rel_singleton_stack p h) (λ_. (h_val h p))"
  by (auto simp add: fun_of_rel_def rel_singleton_stack_def)

lemma funp_rel_singleton_stack[funp_intros, corres_admissible]: "funp (rel_singleton_stack p h)"
 by (auto simp add: rel_singleton_stack_def funp_def fun_of_rel_def)




definition "rel_push" :: 
  "'a::c_type ptr  (heap_mem  'b  'c  bool)  heap_mem   
  'b  'a × 'c  bool" 
where
 "rel_push p R h = (λr (v, x).
    R h r x  
    v = h_val h p)"

lemma rel_singleton_stack_rel_push_conv: "rel_singleton_stack p = (λh x y. rel_push p (λ_ _ _. True) h x (y, ()))"
  by (auto simp add: rel_singleton_stack_def rel_push_def)

lemma rel_push_simp[rel_stack_simps]: "rel_push p R h r (v, x)  
   R h r x  v = h_val h p"
  by (auto simp add: rel_push_def)

lemma fun_of_rel_puhsh [fun_of_rel_intros]:
  "fun_of_rel (R h) f  fun_of_rel (rel_push p R h) (λx. (h_val h p, f x))"
  by (auto simp add: fun_of_rel_def rel_push_def)

lemma funp_rel_push[funp_intros, corres_admissible]: "funp (R h)  funp (rel_push p R h)"
  by (force simp add: funp_def rel_push_def fun_of_rel_def)

lemma rel_push_stackI [rel_stack_intros]: "Q h x y  rel_push p Q h x ((h_val h p), y)"
  by (auto simp add: rel_push_def)

lemma rel_push_stack_condI [rel_stack_intros]: "h_val h p = v  Q h x y  rel_push p Q h x (v, y)"
  by (auto simp add: rel_push_def)

definition "rel_sum_stack L R h = rel_sum (L h) (R h)"
definition "rel_xval_stack L R h = rel_xval (L h) (R h)"

lemma rel_sum_stack_expand_sum_eq:
  "(rel_sum_stack (λ_. (=)) R) = (rel_sum_stack (rel_sum_stack (λ_. (=)) (λ_. (=))) R)"
  by (auto simp add: rel_sum_stack_def fun_eq_iff rel_sum.simps split: sum.splits )

lemma rel_xval_stack_expand_sum_eq:
  "(rel_xval_stack (λ_. (=)) R) = (rel_xval_stack (rel_sum_stack (λ_. (=)) (λ_. (=))) R)"
  by (auto simp add: rel_sum_stack_def rel_xval_stack_def fun_eq_iff rel_sum.simps sum.rel_eq 
      split: xval_splits sum.splits )

lemma rel_sum_stack_expand_sum_bot:
  "(λ_ _ _. False) = (rel_sum_stack (λ_ _ _. False) (λ_ _ _ . False))"
  by (auto simp add: rel_sum_stack_def fun_eq_iff rel_sum.simps split: sum.splits )

lemma rel_xval_stack_expand_xval_bot:
  "(λ_ _ _. False) = (rel_xval_stack (λ_ _ _. False) (λ_ _ _ . False))"
  by (auto simp add: rel_xval_stack_def fun_eq_iff rel_xval.simps split: xval_splits )


lemma rel_sum_stack_entail:
  assumes L: "v v'. L' h v v'  L h v v'" 
  assumes R: "v v'. R' h v v'  R h v v'" 
  assumes "rel_sum_stack L' R' h x y" 
  shows  "rel_sum_stack L R h x y"
  using assms
  by (auto simp add: rel_sum_stack_def rel_sum.simps split: sum.splits)

lemma rel_xval_stack_entail:
  assumes L: "v v'. L' h v v'  L h v v'" 
  assumes R: "v v'. R' h v v'  R h v v'" 
  assumes "rel_xval_stack L' R' h x y" 
  shows  "rel_xval_stack L R h x y"
  using assms
  by (auto simp add: rel_xval_stack_def rel_xval.simps)

lemma rel_sum_stack_intros:
  "L h l1 l2  rel_sum_stack L R h (Inl l1) (Inl l2)"
  "R h r1 r2  rel_sum_stack L R h (Inr r1) (Inr r2)"
  by (auto simp add: rel_sum_stack_def)

lemma rel_xval_stack_intros:
  "L h l1 l2  rel_xval_stack L R h (Exn l1) (Exn l2)"
  "R h r1 r2  rel_xval_stack L R h (Result r1) (Result r2)"
  by (auto simp add: rel_xval_stack_def)

lemma fun_of_rel_sum_stack[fun_of_rel_intros]:
  "fun_of_rel (L h) f_l  fun_of_rel (R h) f_r  fun_of_rel (rel_sum_stack L R h) (sum_map f_l f_r)"
  unfolding rel_sum_stack_def
  by (auto intro: fun_of_rel_intros)



lemma fun_of_rel_xval_stack[fun_of_rel_intros]:
  "fun_of_rel (L h) f_l  fun_of_rel (R h) f_r  fun_of_rel (rel_xval_stack L R h) (map_xval f_l f_r)"
  unfolding rel_xval_stack_def
  by (auto intro: fun_of_rel_intros)

lemma funp_rel_sum_stack[funp_intros, corres_admissible]: "funp (L h)  funp (R h)  funp (rel_sum_stack L R h)"
  unfolding rel_sum_stack_def by (auto intro: funp_intros)


lemma funp_rel_xval_stack[funp_intros, corres_admissible]: "funp (L h)  funp (R h)  funp (rel_xval_stack L R h)"
  unfolding rel_xval_stack_def by (auto intro: funp_intros)


lemma rel_sum_stack_cases:
"rel_sum_stack L R h x y = 
 ((v w. x = Inl v  y = Inl w  L h v w) 
 (v w. x = Inr v  y = Inr w  R h v w))"
  by (auto simp add: rel_sum_stack_def rel_sum.simps)

lemma rel_xval_stack_cases:
"rel_xval_stack L R h x y = 
 ((v w. x = Exn v  y = Exn w  L h v w) 
 (v w. x = Result v  y = Result w  R h v w))"
  by (auto simp add: rel_xval_stack_def rel_xval.simps)

lemma rel_sum_stack_simps [simp]:
  "rel_sum_stack L R h (Inl l1) (Inl l2) = L h l1 l2"
  "rel_sum_stack L R h (Inr r1) (Inr r2) = R h r1 r2"
  "rel_sum_stack L R h (Inl l1) (Inr r2) = False"
  "rel_sum_stack L R h (Inr r1) (Inl l2) = False"
  "rel_sum_stack L R h (Inl l1) y = (w. y = Inl w  L h l1 w)"
  "rel_sum_stack L R h (Inr r1) y = (w. y = Inr w  R h r1 w)"
  "rel_sum_stack L R h x (Inl l2) = (v. x = Inl v  L h v l2)"
  "rel_sum_stack L R h x (Inr r2) = (v. x = Inr v  R h v r2)"
  by (auto simp add: rel_sum_stack_def rel_sum.simps)

lemma rel_xval_stack_simps [simp]:
  "rel_xval_stack L R h (Exn l1) (Exn l2) = L h l1 l2"
  "rel_xval_stack L R h (Result r1) (Result r2) = R h r1 r2"
  "rel_xval_stack L R h (Exn l1) (Result r2) = False"
  "rel_xval_stack L R h (Result r1) (Exn l2) = False"
  "rel_xval_stack L R h (Exn l1) y = (w. y = Exn w  L h l1 w)"
  "rel_xval_stack L R h (Result r1) y = (w. y = Result w  R h r1 w)"
  "rel_xval_stack L R h x (Exn l2) = (v. x = Exn v  L h v l2)"
  "rel_xval_stack L R h x (Result r2) = (v. x = Result v  R h v r2)"
  by (auto simp add: rel_xval_stack_def rel_xval.simps)

lemma rel_sum_stack_eq_collapse: "(rel_sum_stack (λ_. (=)) (λ_. (=))) = ((λ_. (=))) "
  by (auto simp add: rel_sum_stack_cases fun_eq_iff)

lemma rel_xval_stack_eq_collapse: "(rel_xval_stack (λ_. (=)) (λ_. (=))) = ((λ_. (=))) "
  apply (clarsimp simp add: rel_xval_stack_cases fun_eq_iff) 
  by (metis Exn_def default_option_def exception_or_result_cases not_Some_eq)

lemma rel_sum_stack_InlI: "L h l1 l2  rel_sum_stack L R h (Inl l1) (Inl l2)"
  by (simp)


lemma rel_xval_stack_ExnI: "L h l1 l2  rel_xval_stack L R h (Exn l1) (Exn l2)"
  by (simp)

lemma rel_sum_stack_InrI: "R h r1 r2  rel_sum_stack L R h (Inr r1) (Inr r2)"
  by (simp)

lemma rel_xval_stack_ResultI: "R h r1 r2  rel_xval_stack L R h (Result r1) (Result r2)"
  by (simp)

definition "rel_exit Q h = (λv w. x. v = Nonlocal x  Q h x w)"

lemma rel_exit_simps[simp]: 
  "rel_exit Q h (Nonlocal x) y = Q h x y"
  "rel_exit Q h Break        y = False"
  "rel_exit Q h Continue     y = False"
  "rel_exit Q h Return       y = False"
  "rel_exit Q h (Goto l)     y = False"
  by (auto simp add: rel_exit_def)

lemma rel_exit_intro: "Q h x y  rel_exit Q h (Nonlocal x) y"
  by (auto simp add: rel_exit_def)

lemma rel_xval_stack_rel_exit_intro:
  assumes "x. rel_xval_stack (rel_exit Q) R h (Exn (Nonlocal (the_Nonlocal x))) (Exn x)" 
  assumes "rel_exit Q h e e'" 
  shows "rel_xval_stack (rel_exit Q) R h (Exn (Nonlocal (the_Nonlocal e))) (Exn e')"
  using assms
  by (auto simp add: rel_exit_def)


lemma rel_xval_stack_rel_exit_intro':
  assumes "x. rel_xval_stack (rel_exit Q) R h (Exn (Nonlocal x)) (Exn x)" 
  assumes "Q h e e'" 
  shows "rel_xval_stack (rel_exit Q) R h (Exn (Nonlocal e)) (Exn e')"
  using assms
  by (auto simp add: rel_exit_def)


lemma rel_exit_False_conv [simp]: "rel_exit (λ_ _ _. False) h e e'  False"
  by (auto simp add: rel_exit_def)

lemma rel_exit_FalseE: "rel_exit (λ_ _ _. False) h e e'  L"
  by simp

lemma rel_sum_stack_generalise_left: 
  "rel_sum_stack L R h v w  (v w. L h v w  L' h v w)  rel_sum_stack L' R h v w"
  by (auto simp add: rel_sum_stack_def rel_sum.simps)

lemma rel_xval_stack_generalise_left: 
  "rel_xval_stack L R h v w  (v w. L h v w  L' h v w)  rel_xval_stack L' R h v w"
  by (auto simp add: rel_xval_stack_def rel_xval.simps)

lemmas generalise_unreachable_exitE = 
  rel_exit_FalseE
  rel_sum_stack_generalise_left
  rel_xval_stack_generalise_left

lemma fun_of_rel_rel_exit: "fun_of_rel (L h) f_l  fun_of_rel (rel_exit L h) (λv. case v of Nonlocal x  f_l x | _  undefined)"
  by (auto simp add: fun_of_rel_def split: c_exntype.splits)

lemma funp_rel_exit [funp_intros, corres_admissible]: "funp (L h)  funp (rel_exit L h)"
  using fun_of_rel_rel_exit
  by (metis funp_def)


named_theorems equal_upto_simps
named_theorems refines_stack_intros

lemma equal_uptoI: 
  assumes eq: "x. x  A  f x = g x"
  shows "equal_upto A f g"
  using eq
  by (auto simp add: equal_upto_def)

lemma equal_upto_heap_update[equal_upto_simps]:
  fixes p:: "'a::mem_type ptr"
  assumes "(ptr_span p)  A" 
  shows "equal_upto A (heap_update p v h1) h2 = equal_upto A h1 h2"
  using assms 
  by (smt (verit, best) CTypes.mem_type_simps(2) equal_upto_def heap_list_length heap_update_def heap_update_nmem_same subset_iff)

lemma equal_upto_complement: "equal_upto B f g = equal_on (- B) f g"
  by (simp add: equal_on_def equal_upto_def)

lemma equal_upto_update_left_equalize:
  "equal_on (- F) (f s) s  equal_on F (f s) t  equal_upto (F  A) s t = equal_upto A (f s) t" 
  by (smt (verit) Compl_iff Un_iff equal_on_def equal_upto_def)

lemma admissible_const_snd: 
  assumes admissible_fst: "ccpo.admissible  (λx y. y  x) (λX. w  X. Q w)"
  shows "ccpo.admissible  (λx y. y  x) (λX. w. (w, v)  X  Q w)"
proof (rule ccpo.admissibleI[rule_format])
  fix C::"('a ×'b) set set" 
  assume chain: "Complete_Partial_Order.chain (λx y. y  x) C" 
  assume nonempty: "C  {}" 
  assume chain_prop: "X. X  C  w. (w, v)  X  Q w" 
  show "w. (w, v)   C  Q w"
  proof -
    define C' where "C' = Set.filter (λ(r, t). t =  v) ` C"
    have subset: " C'   C"
      using C'_def by fastforce
    moreover
    have snd_C': "X t. X  C'   t  snd ` X  t = v"
      using C'_def
      by auto
    moreover
    from chain have chain_C': "Complete_Partial_Order.chain (λx y. y  x) C'"
      using chain_prop C'_def
      by (simp add: chain_imageI subset_iff)
    from nonempty chain_prop have nonempty_C': "C'  {}"
      using C'_def
      by blast

    from chain_C' have result_chain: "Complete_Partial_Order.chain (λx y. y  x) ((λX. fst ` X) ` C')"
      by (simp add: chain_imageI image_mono)
    from nonempty_C' have nonempty_result_chain: "((λX. fst ` X) ` C')  {}" by auto
    {
      fix X::"'a set"
      assume "X  (`) fst ` C'"
      then obtain X0 where X: "X = fst ` Set.filter (λ(r, t). t =  v) X0" and X0: "X0  C"
        by (auto simp add: C'_def)
      from chain_prop [OF X0] obtain w where w: "(w, v)  X0" and Q: "Q w" by blast
      from w X have "w  X"
        apply clarsimp
        by (metis (mono_tags, lifting) case_prodI fst_conv image_iff member_filter)
      with Q 
      have "wX. Q w" ..
    } note result_chain_prop = this
    from ccpo.admissibleD [OF admissible_fst  result_chain nonempty_result_chain result_chain_prop]
    obtain r' where
      r': "r'    ((λX. fst ` X) ` C')" and Q: "Q r'"
      by auto
    from r' snd_C' have "(r', v)   C'"
      by fastforce
    with Q subset show ?thesis by blast
  qed
qed

lemma admissible_funp: "funp Q  ccpo.admissible  (λx y. y  x) (λX. w  X. Q v w)"
  apply (clarsimp simp add: funp_def fun_of_rel_def)
  by (smt (verit, del_insts) InterI admissible_const ccpo.admissible_def)

lemma admissible_funp_conj: "funp Q  ccpo.admissible  (λx y. y  x) (λX. w  X. Q v w  P w)"
  apply (clarsimp simp add: funp_def fun_of_rel_def)
  by (smt (verit, del_insts) InterI admissible_const ccpo.admissible_def)

lemma override_on_frame_raw_frame_lemma1:  
  assumes disj_A_B: "A  B = {}"
  assumes sf: "stack_free d  B = {}"
  shows
    "override_on d (override_on d' d B) (A  B - stack_free d)  = 
     override_on d d' (A - stack_free d)"
  using disj_A_B sf
  by (auto simp add: override_on_def fun_eq_iff)

lemma override_on_frame_raw_frame_lemma2:  
  assumes disj_A_B: "A  B = {}"
  assumes sf: "stack_free d  B = {}"
  shows 
    "override_on h' (override_on h h' B) (A  B  stack_free d) =
     override_on h' h (A  stack_free d)"
  using disj_A_B sf
  by (auto simp add: override_on_def fun_eq_iff)


lemma disjoint_stack_free_equal_upto_trans: 
  "equal_upto A d' d 
   P  A = {}  stack_free d  P = {} 
   stack_free d'  P = {}"
  apply (clarsimp simp add: equal_upto_def)
  using root_ptr_valid_def stack_free_def valid_root_footprint_def by fastforce

lemma disjoint_stack_free_equal_on_trans: 
  "equal_on S d' d 
   P  S  stack_free d  P = {} 
   stack_free d'  P = {}"
  apply (clarsimp simp add: equal_on_def)
  using root_ptr_valid_def stack_free_def valid_root_footprint_def by fastforce

lemma refines_L2_guard_right': 
  assumes "P t  refines f g s t Q"
  shows "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma refines_L2_guard_right'': 
  assumes "P t  refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  shows "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma refines_L2_guard_right''': 
  assumes "P t  refines f (L2_seq (L2_seq (L2_guard P) (λ_. g)) X) s t Q"
  shows "refines f (L2_seq (L2_seq (L2_guard P) (λ_. g)) X) s t Q"
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma refines_L2_guard_right'''':
  assumes "P t  
    refines f
      (L2_seq 
        (L2_catch (L2_seq (L2_guard P) (λ_. g)) X)
        Y) s t Q "
  shows "refines f 
    (L2_seq 
      (L2_catch (L2_seq (L2_guard P) (λ_. g)) X)
      Y) s t Q "
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind reaches_catch succeeds_catch)


lemma refines_L2_guard_rightE: 
  assumes "P t" 
  assumes "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  shows "refines f g s t Q"
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma refines_L2_guard_rightE': 
  assumes "P t" 
  assumes "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  shows "refines f (L2_seq (L2_guard P) (λ_. g)) s t Q"
  using assms unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

lemma refines_L2_guard_right: 
  "(P  refines f g s t Q)  refines f (L2_seq (L2_guard (λ_. P)) (λ_. g)) s t Q"
  unfolding L2_defs
  by (auto simp add: refines_def_old reaches_bind succeeds_bind)

context heap_state
begin

lemma equal_upto_heap_on_heap_update[equal_upto_simps]:
  fixes p:: "'a::mem_type ptr"
  assumes "ptr_span p  A" 
  shows "equal_upto_heap_on A (hmem_upd (heap_update p v) s) t = equal_upto_heap_on A s t"
  using assms equal_upto_heap_update
  by (smt (verit, ccfv_threshold) equal_upto_heap_on_def equal_upto_heap_on_refl 
      equal_upto_heap_on_trans heap.get_upd heap.upd_cong heap.upd_same hmem_htd_upd sympD 
      symp_equal_upto_heap_on)

lemma equal_upto_heap_stack_release':
  fixes p:: "'a::mem_type ptr"
  assumes "ptr_span p  A" 
  shows "equal_upto_heap_on A (htd_upd (stack_releases (Suc 0) p) s) s"
  by (metis (no_types, lifting) One_nat_def add_mult_distrib add_right_cancel assms 
      equal_upto_heap_on_zero_heap_on heap_state.equal_upto_heap_on_trans heap_state_axioms 
      plus_1_eq_Suc sympD symp_equal_upto_heap_on times_nat.simps(2) zero_heap_on_stack_releases)


lemma equal_upto_heap_stack_release[equal_upto_simps]:
  fixes p:: "'a::mem_type ptr"
  assumes "ptr_span p  A" 
  shows "equal_upto_heap_on A (htd_upd (stack_releases (Suc 0) p) s) t = equal_upto_heap_on A s t"
  using equal_upto_heap_stack_release'
  by (metis assms equal_upto_heap_on_trans sympD symp_equal_upto_heap_on)

lemma equal_upto_heap_on_htd_upd: 
  "equal_upto_heap_on A s t  
   equal_upto A (f (htd s)) (htd t) 
   equal_upto_heap_on A (htd_upd f s) t"
  by (smt (verit, best) equal_upto_heap_on_def hmem_htd_upd htd_hmem_upd 
      lense.upd_compose typing.get_upd typing.lense_axioms typing.upd_cong)

lemma equal_upto_heap_on_hmem: "equal_upto_heap_on A s t  equal_upto A (hmem s) (hmem t)"
  by (auto simp add: equal_upto_heap_on_def)

lemma equal_upto_heap_on_sym: "equal_upto_heap_on A s t = equal_upto_heap_on A t s"
  by (metis   heap_state.symp_equal_upto_heap_on heap_state_axioms sympD )

lemma equal_upto_heap_stack_alloc':
  fixes p:: "'a::mem_type ptr"
  shows "equal_upto_heap_on (ptr_span p) 
     (hmem_upd (heap_update p v) (htd_upd (λ_. ptr_force_type p (htd s)) s)) 
      s"
  by (simp add: equal_upto_def equal_upto_heap_on_heap_update 
      equal_upto_heap_on_htd_upd ptr_force_type_d sympD symp_equal_upto_heap_on)

lemma equal_upto_heap_stack_alloc:
  fixes p:: "'a::mem_type ptr"
  assumes "length bs = size_of TYPE('a)"
  shows "equal_upto_heap_on (ptr_span p) 
     (hmem_upd (heap_update_padding p v bs) (htd_upd (λ_. ptr_force_type p (htd s)) s))
     s"
  apply (subst equal_upto_heap_on_sym)
  using assms
  apply (clarsimp simp add: equal_upto_def equal_upto_heap_on_def)
  by (smt (verit, del_insts) CTypes.mem_type_simps(2) heap.lense_axioms heap_update_nmem_same 
      heap_update_padding_def hmem_htd_upd lense.upd_cong ptr_force_type_d typing.lense_axioms)

definition 
  "rel_alloc":: "addr set  addr set  addr set  's  's  's  bool" 
  where
  "rel_alloc S M A t0  λs t.
     stack_free (htd s)  S  
     stack_free (htd s)  A = {}  
     stack_free (htd s)  M = {}  
     t = frame A t0 s"

lemma rel_alloc_fold_frame: "rel_alloc 𝒮 M A t0 s t  frame A t0 s = t"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_modifies_antimono: "rel_alloc S M2 A t0 s t  M1  M2  rel_alloc S M1 A t0 s t"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint:  
 "rel_alloc S M A t0 s t  ptr_span p  A  ptr_span p  stack_free (htd s) = {}"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint_trans:  
 "rel_alloc S M A t0 s' t  htd s' = htd s  ptr_span p  A  ptr_span p  stack_free (htd s) = {}"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint':  
 "rel_alloc S M A t0 s t  ptr_span p  A  stack_free (htd s)  ptr_span p  = {}"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint_trans':  
 "rel_alloc S M A t0 s' t  htd s' = htd s  ptr_span p  A  stack_free (htd s)  ptr_span p  = {}"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint_field_lvalue:
  fixes p:: "'a::mem_type ptr"
  assumes "rel_alloc S M A t0 s t" "ptr_span p  A" 
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (T, n)" 
  assumes "export_uinfo T = typ_uinfo_t (TYPE('b))"
  shows "{&(pf)..+size_of TYPE('b::c_type)}  stack_free (htd s) = {}"
  using rel_alloc_stack_free_disjoint  field_tag_sub assms export_size_of
  by fastforce

lemma rel_alloc_stack_free_disjoint_field_lvalue_trans:
  fixes p:: "'a::mem_type ptr"
  assumes "rel_alloc S M A t0 s' t" "htd s' = htd s" "ptr_span p  A" 
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (T, n)" 
  assumes "export_uinfo T = typ_uinfo_t (TYPE('b))"
  shows "{&(pf)..+size_of TYPE('b::c_type)}  stack_free (htd s) = {}"
  using rel_alloc_stack_free_disjoint  field_tag_sub assms export_size_of
  by fastforce

lemma rel_alloc_stack_free_disjoint_field_lvalue':
  fixes p:: "'a::mem_type ptr"
  assumes "rel_alloc S M A t0 s t" "ptr_span p  A" 
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (T, n)" 
  assumes "export_uinfo T = typ_uinfo_t (TYPE('b))"
  shows "stack_free (htd s)  {&(pf)..+size_of TYPE('b::c_type)} = {}"
  using rel_alloc_stack_free_disjoint_field_lvalue [OF assms] by blast

lemma rel_alloc_stack_free_disjoint_field_lvalue_trans':
  fixes p:: "'a::mem_type ptr"
  assumes "rel_alloc S M A t0 s' t" "htd s' = htd s" "ptr_span p  A" 
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (T, n)" 
  assumes "export_uinfo T = typ_uinfo_t (TYPE('b))"
  shows "stack_free (htd s)  {&(pf)..+size_of TYPE('b::c_type)} = {}"
  using rel_alloc_stack_free_disjoint_field_lvalue_trans [OF assms] by blast

lemma h_val_rel_alloc_disjoint:
  fixes p::"'a::mem_type ptr"
  shows "rel_alloc S M A t0 s t  ptr_span p  A = {}  ptr_span p  stack_free (htd s) = {}  h_val (hmem t) p = h_val (hmem s) p"
  apply (simp add: rel_alloc_def h_val_frame_disjoint)
  done


definition rel_stack:: 
  "addr set  addr set  addr set  's   's  (heap_mem  'b  'c  bool)  
    ('b × 's)  ('c × 's)  bool"
  where
  "rel_stack S M A s t0 R = (λ(v, s') (w, t').
     R (hmem s') v w 
     rel_alloc S M A t0 s' t'  
     equal_upto (M  stack_free (htd s')) (hmem s') (hmem s) 
     htd s' = htd s)" 

lemma rel_stack_unchanged_typing: "rel_alloc S M' A t0 s t  rel_stack S M A s t0 R (v, s') (w, t') 
  equal_on S (htd t') (htd t)"
  by (auto simp add: rel_alloc_def rel_stack_def Diff_triv equal_on_def htd_frame inf_commute)

lemma rel_stack_unchanged_heap: "rel_alloc S M' A t0 s t  rel_stack S M A s t0 R (v, s') (w, t') 
  equal_upto (M  stack_free (htd s')) (hmem t') (hmem t)"
  apply (clarsimp simp add: rel_alloc_def rel_stack_def Diff_triv equal_on_def htd_frame inf_commute)
  by (smt (verit, ccfv_threshold) equal_on_def equal_on_stack_free_preservation equal_upto_def hmem_frame)

lemma rel_stack_unchanged_stack_free: 
  "rel_alloc S M' A t0 s t  rel_stack S M A s t0 R (v, s') (w, t') 
  stack_free (htd s') = stack_free (htd s)"
  apply (auto simp add: rel_alloc_def rel_stack_def Diff_triv htd_frame inf_commute)
  done

lemma rel_stack_unchanged_stack_free': 
  assumes stack: "rel_alloc S M' A t0 s t" 
  assumes rel_stack: "rel_stack S M A s t0 R (v, s') (w, t')"
  shows "stack_free (htd t') = stack_free (htd t)"
  using stack rel_stack
  apply (clarsimp simp add: rel_alloc_def rel_stack_def Diff_triv htd_frame inf_commute)
  subgoal
    using rel_stack_unchanged_stack_free [OF stack rel_stack] equal_on_stack_free_preservation
    by (auto simp add: frame_def stack_free_def root_ptr_valid_def valid_root_footprint_def)
  done

lemma rel_stack_unchanged_heap': 
  assumes alloc: "rel_alloc S {} A t0 s t"
  assumes stack: "rel_stack S M A s t0 R (v, s') (w, t')" 
  shows "equal_upto (M  stack_free (htd t')) (hmem t') (hmem t)"
  apply (rule equal_upto_mono [OF _ rel_stack_unchanged_heap [OF alloc stack]])
  using  stack_free_htd_frame stack
  apply (auto simp add: rel_stack_def rel_alloc_def subset_iff)
  done

lemma rel_stack_Exn[simp]: 
  "rel_stack S M A s t0 (rel_xval_stack L R) (Exn v, s') (Exn w, t') = rel_stack S M A s t0 L (v, s') (w, t')"
  by (simp add: rel_stack_def)
lemma rel_stack_Exn_Result[simp]: 
  "rel_stack S M A s t0  (rel_xval_stack L R) (Exn v, s') (Result w, t') = False"
  by (simp add: rel_stack_def)
lemma rel_stack_Result[simp]: 
  "rel_stack S M A s t0 (rel_xval_stack L R) (Result v, s') (Result w, t') = rel_stack S M A s t0 R (v, s') (w, t')"
  by (simp add: rel_stack_def)
lemma rel_zero_stack_Result_Exn[simp]: 
  "rel_stack S M A s t0 (rel_xval_stack L R) (Result v, s') (Exn w, t') = False"
  by (simp add: rel_stack_def)

lemma admissible_fail: " ccpo.admissible Inf (λx y. y  x) (λA. ¬ succeeds A t)"
  apply (rule ccpo.admissibleI) 
  apply (clarsimp simp add: ccpo.admissible_def chain_def 
      succeeds_def reaches_def split: prod.splits xval_splits)
  apply transfer
  by (auto simp add: Inf_post_state_def top_post_state_def)


lemma fun_lub_lem: "(λ(A::('f  (('d, 'e) exception_or_result × 'f) post_state) set) x::'f.
            f::'f  (('d, 'e) exception_or_result × 'f) post_stateA. f x) = fun_lub (Inf)"
  apply (clarsimp simp add: fun_lub_def [abs_def])
  by (simp add: image_def)

lemma fun_ord_lem:
   "(λ(a::'f  (('d, 'e) exception_or_result × 'f) post_state)
            b::'f  (('d, 'e) exception_or_result × 'f) post_state. x::'f. b x  a x) = fun_ord (≥)"
  apply (simp add: fun_ord_def [abs_def])
  done


(* FIXME: move to spec monad or up *)
lemma admissible_refines_funp:
  assumes *: "funp R"
  shows "ccpo.admissible Inf (≥) (λA. refines C A s t R)"
    apply (rule ccpo.admissibleI) 
 
  apply (clarsimp simp add: ccpo.admissible_def chain_def 
        refines_def_old reaches_def succeeds_def)
  apply (intro allI impI conjI)
  subgoal
    apply transfer
    by (auto simp add: Inf_post_state_def top_post_state_def split: if_split_asm)
  subgoal
    using *
    apply transfer
    apply (clarsimp simp add: funp_def fun_of_rel_def Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
    by (metis post_state.distinct(1) outcomes.simps(2))
  done

lemma fun_of_rel_stack: 
  assumes f: "h. fun_of_rel (Q h) (f h)" 
  shows "fun_of_rel (rel_stack S M A s t0 Q) (λ(r, s). (f (hmem s) r, frame A t0 s))"
  using f
  by (auto simp add: fun_of_rel_def rel_stack_def rel_alloc_def)

lemma funp_rel_stack: 
  assumes funp: "h. funp (Q h)"
  shows "funp (rel_stack S M A s t0 Q)"
proof -
  from funp obtain f where f: "h. fun_of_rel (Q h) (f h)" 
    apply (clarsimp simp add: funp_def ) 
    by metis
  from fun_of_rel_stack [OF f] 
  have "fun_of_rel (rel_stack S M A s t0 Q) (λ(r, s). (f (hmem s) r, frame A t0 s))".
  then show ?thesis
    unfolding funp_def
    by blast
qed

theorem admissible_refines_rel_stack[corres_admissible]: 
  assumes funp: "h. funp (Q h)"
  shows "ccpo.admissible Inf (≥) (λg. refines f g s' t' (rel_stack S M A s t0 Q))"
  apply (rule admissible_refines_funp)
  apply (rule funp_rel_stack)
  apply (rule funp)
  done

lemma admissible_rel_stack_eq: "ccpo.admissible  (λx y. y  x) (λX. w  X. (λ_. (=)) h v w)"
  by (auto simp add: ccpo.admissible_def)

lemma admissible_rel_singleton_stack: 
  shows "ccpo.admissible  (λx y. y  x) (λX. w  X. (rel_singleton_stack p) h v w)"
    by (auto simp add: ccpo.admissible_def rel_singleton_stack_def)

lemma admissible_rel_push: 
  assumes admiss: "h v. ccpo.admissible  (λx y. y  x) (λX. w  X. Q h v w)"
  shows "ccpo.admissible  (λx y. y  x) (λX. w  X. (rel_push p Q) h v w)"
proof -
  have "ccpo.admissible  (λx y. y  x) (λX. w. (h_val h p, w)  X  Q h v w)"
  proof (rule ccpo.admissibleI[rule_format])
    fix C::"('c × 'b) set set"  
    assume chain: "Complete_Partial_Order.chain (λx y. y  x) C"
    assume nonempty: "C  {}"
    assume chain_prop: "(X. X  C  w. (h_val h p, w)  X  Q h v w)"
    show "w. (h_val h p, w)   C  Q h v w"
    proof -
      define C' where "C' = Set.filter (λ(v, w). v = h_val h p) ` C"
      have subset: " C'   C"
        using C'_def by fastforce
      from chain have chain_C': "Complete_Partial_Order.chain (λx y. y  x) C'"
        using chain_prop C'_def
        by (simp add: chain_imageI subset_iff)
      have fst_C': "X t. X  C'   t  fst ` X  t = h_val h p" 
        using C'_def
        by auto
      from nonempty chain_prop have nonempty_C': "C'  {}"
        using C'_def
        by blast
      from chain_C' have result_chain: "Complete_Partial_Order.chain (λx y. y  x) ((λX. snd ` X) ` C')"
        by (simp add: chain_imageI image_mono)
      from nonempty_C' have nonempty_result_chain: "((λX. snd ` X) ` C')  {}" by auto
      from chain_prop have result_chain_prop: "(X. X  (`) snd ` C'  wX. Q h v w) "
        using C'_def
        by auto (metis (mono_tags, lifting) case_prodI member_filter snd_conv)
      from ccpo.admissibleD [OF admiss [of "h" v] result_chain nonempty_result_chain result_chain_prop]
      obtain w where
        w: "w    ((λX. snd ` X) ` C')" and Q: "Q h v w"
        by auto
      from w fst_C' have "(h_val h p, w)   C'"
        by fastforce
      with Q subset show ?thesis by blast
    qed
  qed
  then show ?thesis
    by (clarsimp simp add: rel_push_def  split_paired_Bex)
qed

lemma admissible_rel_sum_stack: 
  assumes admiss_L: "h v. ccpo.admissible  (λx y. y  x) (λX. w  X. L h v w)"
  assumes admiss_R: "h v. ccpo.admissible  (λx y. y  x) (λX. w  X. R h v w)"
  shows "ccpo.admissible  (λx y. y  x) (λX. w  X. (rel_sum_stack L R) h v w)"
proof -
  have "ccpo.admissible  (λx y. y  x) (λX. wX. rel_sum (L h) (R h) v w)"
  proof (rule ccpo.admissibleI[rule_format])
    fix C::"('c + 'e) set set" 
    assume chain: "Complete_Partial_Order.chain (λx y. y  x) C"
    assume nonempty: "C  {}"
    assume chain_prop: "X. X  C  wX. rel_sum (L h) (R h) v w"
    show "w C. rel_sum (L h) (R h) v w"
    proof (cases v)
      case (Inl l)
      define C' where "C' = Set.filter (Sum_Type.isl) ` C"
      have subset: " C'   C"
        using C'_def by fastforce
      from chain have chain_C': "Complete_Partial_Order.chain (λx y. y  x) C'"
        using chain_prop C'_def
        by (simp add: chain_imageI subset_iff)
      from nonempty chain_prop have nonempty_C': "C'  {}"
        using C'_def
        by blast
      have prop_C': "X t. X  C'   t  X  Sum_Type.isl t" 
        using C'_def
        by auto
      from Inl chain_prop  have chain_prop': 
        "X. X  C'  wX. l'. w = Inl l'  L h l l'"  
        by (fastforce simp add: rel_sum.simps C'_def)
      have "w C. l'. w = Inl l'  L h l l'"
      proof - 
        from chain_C' have result_chain: "Complete_Partial_Order.chain (λx y. y  x) ((λX. Sum_Type.projl ` X) ` C')"
          by (simp add: chain_imageI image_mono)
        from nonempty_C' have nonempty_result_chain: "((λX. Sum_Type.projl ` X) ` C')  {}" by auto

        from chain_prop' have result_chain_prop: "X. X (λX. Sum_Type.projl ` X) ` C'  wX. L h l w"
          using image_iff by fastforce
        from ccpo.admissibleD [OF admiss_L [of "h" l] result_chain nonempty_result_chain result_chain_prop]
        obtain w where
          w: "w ((`) projl ` C')" and L: "L h l w"
          by auto
        from w prop_C' have "Inl w   C'" by fastforce
        with L subset show ?thesis by blast
      qed
      then show ?thesis by (simp add: Inl rel_sum.simps)
    next
      case (Inr r)
      define C' where "C' = Set.filter (Not o Sum_Type.isl) ` C"
      have subset: " C'   C"
        using C'_def by fastforce
      from chain have chain_C': "Complete_Partial_Order.chain (λx y. y  x) C'"
        using chain_prop C'_def
        by (simp add: chain_imageI subset_iff)
      from nonempty chain_prop have nonempty_C': "C'  {}"
        using C'_def
        by blast
      have prop_C': "X t. X  C'   t  X  ¬ (Sum_Type.isl t)" 
        using C'_def
        by auto
      from Inr chain_prop  have chain_prop': 
        "X. X  C'  wX. r'. w = Inr r'  R h r r'"  
        by (fastforce simp add: rel_sum.simps C'_def)
      have "w C. r'. w = Inr r'  R h r r'"
      proof - 
        from chain_C' have result_chain: "Complete_Partial_Order.chain (λx y. y  x) ((λX. Sum_Type.projr ` X) ` C')"
          by (simp add: chain_imageI image_mono)
        from nonempty_C' have nonempty_result_chain: "((λX. Sum_Type.projr ` X) ` C')  {}" by auto

        from chain_prop' have result_chain_prop: "X. X (λX. Sum_Type.projr ` X) ` C'  wX. R h r w"
          using image_iff by fastforce
        from ccpo.admissibleD [OF admiss_R [of "h" r] result_chain nonempty_result_chain result_chain_prop]
        obtain w where
          w: "w ((`) projr ` C')" and L: "R h r w"
          by auto
        from w prop_C' have "Inr w   C'" by fastforce
        with L subset show ?thesis by blast
      qed
      then show ?thesis by (simp add: Inr rel_sum.simps)
    qed
  qed
  then show ?thesis by (simp add: rel_sum_stack_def)
qed

lemma IOcorres_refines_conv: 
  assumes rel_to_prj: "h. fun_of_rel (R h) (prj h)"
  assumes rel_to_prjE: "h. fun_of_rel (L h) (prjE h)"
  shows "IOcorres
           (λs. rel_alloc 𝒮 M A t0 s (frame A t0 s)  P s) 
           (λs r s'. stack_free (htd s')  𝒮  stack_free (htd s')  A = {}  stack_free (htd s')  M1 = {}  
                    equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)  
                    htd s' = htd s 
                    (case r of Exn l  e. l = Nonlocal e  L (hmem s') e (prjE (hmem s') e)| Result x  R (hmem s') x (prj (hmem s') x)))
           (frame A t0) 
           (λr s. prj (hmem s) r) 
           (λr s. prjE (hmem s) (the_Nonlocal r))
           g f
          
         (s t. rel_alloc 𝒮 M A t0 s t  P s  refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R)))"
  apply standard
  subgoal
    apply (clarsimp simp add: IOcorres_def corresXF_post_def)
    apply (rule refinesI)
    subgoal
      using rel_alloc_fold_frame by blast


    subgoal for s t v s'
      apply (erule_tac x=s in allE)
      apply (subst (asm) (1 2) rel_alloc_def)
      apply safe
      apply (clarsimp)
      apply (erule_tac x="v" in allE)
      apply (erule_tac x="s'" in allE)
      subgoal
        apply (clarsimp split: xval_splits)
        subgoal for x
          apply (rule exI[where x="Exn (prjE (hmem s') x)"])
          apply (rule exI[where x="frame A t0 s'"])
          apply (clarsimp simp add: rel_stack_def rel_alloc_def fun_of_rel_def)
          done
        subgoal for x
          apply (rule exI[where x="Result (prj (hmem s') x)"])
          apply (rule exI[where x="frame A t0 s'"])
          apply (clarsimp simp add: rel_stack_def rel_alloc_def fun_of_rel_def)
          done
        done
      done
    done
  subgoal
    apply (clarsimp simp add: IOcorres_def corresXF_post_def)
    subgoal for s
    apply (rule conjI)
    subgoal
      apply clarsimp
      subgoal for v s'
        apply (erule_tac x="s" in allE)
        apply (erule_tac x="(frame A t0 s)" in allE)
        apply (clarsimp simp add: rel_alloc_def refines_def_old)
        apply (erule_tac x="v" in allE)
        apply (erule_tac x="s'" in allE)
        subgoal 
          apply (cases v)
          subgoal  
            using rel_to_prjE  by (clarsimp simp add: rel_stack_def rel_alloc_def fun_of_rel_def rel_exit_def default_option_def 
                Exn_def [symmetric])
          subgoal  
            using rel_to_prj by (clarsimp simp add: rel_stack_def rel_alloc_def fun_of_rel_def default_option_def 
                Exn_def [symmetric]) 
          done
        done
      done
    subgoal 
      by (auto simp add: refines_def_old)
    done
  done
  done

lemmas IOcorres_to_refines = iffD1 [OF  IOcorres_refines_conv, rule_format]
lemmas refines_to_IOcorres = iffD2 [OF  IOcorres_refines_conv, rule_format]

lemma refines_rel_xval_stack_generalise_exit:
    "refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R))  (h v w. L h v w  L' h v w)  
     refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L' R))"
  by (erule refines_weaken) (auto simp add: rel_stack_def rel_xval_stack_def rel_xval.simps)

lemma L2_gets_rel_stack': 
  assumes "R (hmem s) (e s) (e' (frame A t0 s))"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_gets e ns) (L2_gets e' ns) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def)


lemma L2_gets_rel_stack: 
  assumes "R (hmem s) (e s) (e' (frame A t0 s))"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_gets e ns) (L2_gets e' ns') s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def)

lemma L2_gets_rel_stack_guarded: 
  assumes "G  R (hmem s) (e s) (e' (frame A t0 s))"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_gets e ns) (L2_seq (L2_guard (λ_. G)) (λ_. (L2_gets e' ns'))) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def succeeds_bind reaches_bind)

lemma L2_gets_constant_trivial_rel_stack: 
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_gets (λ_. c) ns) (L2_gets (λ_. c) ns) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def)

lemma L2_gets_constant_rel_stack: 
  assumes "R (hmem s) c c'"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_gets (λ_. c) ns) (L2_gets (λ_. c') ns) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def)

lemma L2_throw_rel_stack: 
  assumes "L (hmem s) c c'"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_throw c ns) (L2_throw c' ns') s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))" 
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def Exn_def [symmetric])

lemma L2_try_rel_stack: 
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_sum_stack L R) R))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def reaches_try)
  subgoal for s' r'
  apply (cases r')
     apply (clarsimp simp add: default_option_def Exn_def [symmetric])
    subgoal for y
      apply (cases y)
      subgoal by fastforce
      subgoal by fastforce
      done
    subgoal
      apply fastforce
      done
    done
  done

lemma L2_try_rel_stack_merge1: 
  assumes "h v v'. R' h v v'   R h v v'"
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_sum_stack L R') R))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def reaches_try)
  subgoal for s' r'
  apply (cases r')
     apply (clarsimp simp add: default_option_def Exn_def [symmetric])
    subgoal for y
      apply (cases y)
      subgoal by fastforce
      subgoal by fastforce
      done
    subgoal
      apply fastforce
      done
    done
  done

lemma L2_try_rel_stack_merge2: 
  assumes "h v v'. R' h v v'  R h v v'"
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_sum_stack L R) R'))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def reaches_try)
  subgoal for s' r'
  apply (cases r')
     apply (clarsimp simp add: default_option_def Exn_def [symmetric])
    subgoal for y
      apply (cases y)
      subgoal by fastforce
      subgoal by fastforce
      done
    subgoal
      apply fastforce
      done
    done
  done

lemma L2_guard_rel_stack:
  assumes "e' (frame A t0 s)  e s"
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_guard e) (L2_guard e') s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def)

lemma L2_modify_heap_update_rel_stack':
  fixes p::"'a:: mem_type ptr"
  assumes "R (heap_update p v (hmem s)) () (e' (frame A t0 s))"
  assumes "ptr_span p  A"
  assumes "rel_alloc 𝒮 (ptr_span p) A t0 s t"
  shows "refines 
           (L2_modify (hmem_upd (heap_update p v))) 
           (L2_gets e' ns) 
           s t 
           (rel_stack 𝒮 (ptr_span p) A s t0 (rel_xval_stack L R))"
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def 
      frame_heap_update equal_upto_heap_update)

lemma L2_modify_heap_update_rel_stack:
  fixes p::"'a:: mem_type ptr"
  assumes "R (heap_update p (v s) (hmem s)) () (e' (frame A t0 s))"
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes "ptr_span p  A"
  assumes "ptr_span p  M"
  shows "refines 
           (L2_modify (λs. hmem_upd (heap_update p (v s)) s)) 
           (L2_gets e' ns) 
           s t 
           (rel_stack 𝒮 (ptr_span p) A s t0 (rel_xval_stack L R))"
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def 
      frame_heap_update equal_upto_heap_update)


lemma L2_modify_keep_heap_update_rel_stack:
  fixes p::"'a:: mem_type ptr"
  assumes "v s = v' (frame A t0 s)" 
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes "ptr_span p  A = {}"
  assumes "ptr_span p  stack_free (htd s) = {}"
  assumes "ptr_span p  M"
  shows "refines 
           (L2_modify (λs. hmem_upd (heap_update p (v s)) s)) 
           (L2_modify (λs. hmem_upd (heap_update p (v' s)) s)) 
           s t 
           (rel_stack 𝒮 (ptr_span p) A s t0 (rel_xval_stack L (λ_. (=))))"
  using assms
  by (auto simp add: refines_def_old L2_defs rel_stack_def rel_alloc_def   
      frame_heap_update disjoint_subset2 equal_upto_heap_update 
      frame_heap_update_disjoint)

lemma L2_modify_keep_heap_update_rel_stack_guarded:
  fixes p::"'a:: mem_type ptr"
  assumes "G  v s = v' (frame A t0 s)" 
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes "G  ptr_span p  A = {}"
  assumes "G  ptr_span p  stack_free (htd s) = {}"
  assumes "G  ptr_span p  M"
  shows "refines 
           (L2_modify (λs. hmem_upd (heap_update p (v s)) s)) 
           (L2_seq (L2_guard (λ_. G)) (λ_. (L2_modify (λs. hmem_upd (heap_update p (v' s)) s)))) 
           s t 
           (rel_stack 𝒮 (ptr_span p) A s t0 (rel_xval_stack L (λ_. (=))))"
  apply (rule refines_L2_guard_right)
  apply (rule L2_modify_keep_heap_update_rel_stack)
  using assms by auto

lemma L2_call_rel_stack':
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes L': "e e' s. L (hmem s) e e'  L' (hmem s) (emb e) (emb' e') "
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb' ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L' R))"
  using assms
  apply (clarsimp simp add: L2_call_def refines_def_old reaches_map_value)
  subgoal for s' r'
    apply (cases r')
    subgoal 
      by (fastforce simp add: default_option_def Exn_def [symmetric] 
          rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps)
    subgoal
      by (fastforce simp add: rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps)
    done
  done


lemma L2_call_rel_stack'':
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes L': "e e' s. L (hmem s) e e'  rel_sum_stack L R' (hmem s) (emb e) (emb' e') "
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb' ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_sum_stack L R') R))"
  apply (rule L2_call_rel_stack' [OF assms(1) _ f ])
  by (rule L')

lemma L2_call_rel_stack: 
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes L': "e e' s. L (hmem s) e e'  L' (hmem s) (emb e) (emb e') "
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L' R))"
  apply (rule  L2_call_rel_stack' [OF assms (1) _ f])
  by (rule L')

text ‹Currently exceptions on the function level are terminal and are propagated to the toplevel.
 So the result relation for termInl is equality.›
lemma L2_call_rel_stack_eq_InL:
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (λ_. (=)) R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (λ_. (=)) R))"
  apply (rule L2_call_rel_stack' [OF assms(1) _ f ])
  by simp

lemma L2_call_rel_stack_bot_InL:
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (λ_ _ _. False) R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (λ_ _ _. False) R))"
  apply (rule L2_call_rel_stack' [OF assms(1) _ f])
  by simp
   
lemma L2_seq_rel_stack'': 
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes f1_g1: "refines f1 g1 s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R1))"
  assumes f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
            
             refines (f2 v) (g2' s' w) s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
  assumes g2'_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
                 g2' s' w = g2 w "

  assumes M1: "M1  M"
  assumes M2: "M2  M"
  shows "refines (L2_seq f1 f2) (L2_seq g1 g2) s t (rel_stack 𝒮 (M1  M2) A s t0 (rel_xval_stack L R))" 
proof -
  from f2_g2 g2'_g2 
  have f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
            
             refines (f2 v) (g2 w) s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
    by metis
  show ?thesis
  apply (rule refines_L2_seq)
      apply (rule f1_g1)
     apply (simp_all)
  subgoal
    using s_t M1 M2 
    apply (clarsimp simp add: rel_stack_def, intro conjI)
    subgoal 
      by (smt (verit, best) Un_commute disjoint_subset2 disjoint_union_distrib 
          equal_on_stack_free_preservation rel_alloc_def sup.coboundedI2)
    subgoal
      using equal_upto_mono
      by (metis inf_sup_ord(3) order_le_less sup_mono)
    done
  apply (rule refines_mono [OF _ f2_g2  ])
  subgoal
    by (auto simp add: rel_stack_def rel_alloc_def equal_upto_def)
  subgoal
    by (auto simp add: rel_stack_def rel_alloc_def)
  subgoal 
    using M1 M2 s_t
    by (auto simp add: rel_stack_def rel_alloc_def)
  subgoal
    by (auto simp add: rel_stack_def)
  subgoal
    by (auto simp add: rel_stack_def)
  done
qed

lemma L2_seq_rel_stack: (* fixme: remove this variant and make g2_normalised the standard? *)
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes f1_g1: "refines f1 g1 s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R1))"
  assumes f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
            
             refines (f2 v) (g2' w s') s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
  assumes g2'_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
                 g2' w s' = g2 w "

  assumes M1: "M1  M"
  assumes M2: "M2  M"
  assumes M': "M' = M1  M2"
  shows "refines (L2_seq f1 f2) (L2_seq g1 g2) s t (rel_stack 𝒮 M' A s t0 (rel_xval_stack L R))" 
proof -
  from f2_g2 g2'_g2 
  have f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
            
             refines (f2 v) (g2 w) s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
    by metis
  show ?thesis
  apply (rule refines_L2_seq)
      apply (rule f1_g1)
     apply (simp_all)
  subgoal
    using s_t M1 M2 M'
    apply (clarsimp simp add: rel_stack_def, intro conjI)
    subgoal 
      by (metis (no_types, lifting) Int_Un_distrib rel_alloc_def sup.absorb_iff1)

    subgoal
      using equal_upto_mono
      by (metis inf_sup_ord(3) order_le_less sup_mono)
    done
  apply (rule refines_mono [OF _ f2_g2  ])
  subgoal
    apply (clarsimp simp add: rel_stack_def rel_alloc_def, intro conjI)
    subgoal by auto (metis M1 M2 M' UnE disjoint_iff equal_on_stack_free_preservation)
    subgoal by (smt (verit, best) M1 M2 M' Un_iff equal_on_stack_free_preservation equal_upto_def)
    done
  subgoal
    by (auto simp add: rel_stack_def rel_alloc_def)
  subgoal 
    using M1 M2 s_t
    apply (auto simp add: rel_stack_def rel_alloc_def)
    done
  subgoal
    by (auto simp add: rel_stack_def)
  subgoal
    by (auto simp add: rel_stack_def)
  done
qed

lemma L2_seq_rel_stack_g2_normalised:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes f1_g1: "refines f1 g1 s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R1))"
  assumes f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
             refines (f2 v) (g2 w) s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  assumes M2: "M2  M"
  assumes M': "M' = M1  M2"
  shows "refines (L2_seq f1 f2) (L2_seq g1 g2) s t (rel_stack 𝒮 M' A s t0 (rel_xval_stack L R))" 
  by (rule L2_seq_rel_stack [OF s_t f1_g1 f2_g2 _ M1 M2 M']) auto

lemma L2_seq_rel_stack': 
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes f1_g1: "refines f1 g1 s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R1))"
  assumes f2_g2: "s' t' v w. R1 (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
             refines (f2 v) (g2 w) s' t' (rel_stack 𝒮 M2 A s' t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  assumes M2: "M2  M"
  assumes M': "M' = M1  M2"
  shows "refines (L2_seq f1 f2) (L2_seq g1 g2) s t (rel_stack 𝒮 M' A s t0 (rel_xval_stack L R))" 
proof -
  show ?thesis
  apply (rule refines_L2_seq)
      apply (rule f1_g1)
     apply (simp_all)
  subgoal
    using s_t M1 M2 M'
    apply (clarsimp simp add: rel_stack_def, intro conjI)
    subgoal 
      by (metis (no_types, lifting) Int_Un_distrib rel_alloc_def sup.absorb_iff1)

    subgoal
      using equal_upto_mono
      by (metis inf_sup_ord(3) order_le_less sup_mono)
    done
  apply (rule refines_mono [OF _ f2_g2  ])
  subgoal
    apply (clarsimp simp add: rel_stack_def rel_alloc_def, intro conjI)
    subgoal by auto (metis M1 M2 M' UnE disjoint_iff equal_on_stack_free_preservation)
    subgoal by (smt (verit, best) M1 M2 M' Un_iff equal_on_stack_free_preservation equal_upto_def)
    done
  subgoal
    by (auto simp add: rel_stack_def rel_alloc_def)
  subgoal 
    using M1 M2 s_t
    apply (auto simp add: rel_stack_def rel_alloc_def)
    done
  done
qed


lemma frame_raw_frame_union: 
  assumes disj_A_B: "A  B = {}"
  assumes sf: "stack_free (htd s)  B = {}"
  shows "frame (A  B) (raw_frame B s t0) s = frame A t0 s"
  apply (clarsimp simp add: frame_def raw_frame_def)
  using override_on_frame_raw_frame_lemma1 [OF disj_A_B sf] 
    override_on_frame_raw_frame_lemma2 [OF disj_A_B sf]
  by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)


lemma refines_narrow_frame':
  assumes disj_B_M: "B  M = {}"
  assumes disj_A_B: "A  B = {}"
  assumes spec: "t0 s t. rel_alloc 𝒮 M1 (A  B) t0 s t  
    refines f g s t (rel_stack 𝒮 M (A  B) s t0 Q)"
  assumes sf: "stack_free (htd s)  B = {}"
  assumes rel_alloc: "rel_alloc 𝒮 M1 A t0 s t"
  shows "refines f g s t (rel_stack 𝒮 M A s t0 Q)"
proof -
  from rel_alloc have t: "t = frame A t0 s" by (auto simp add: rel_alloc_def)
  define t0' where  "t0' = raw_frame B s t0"

  have "t = frame (A  B) t0' s"  
    using frame_raw_frame_union [OF disj_A_B sf]
    by (simp add: t0'_def t)

  
  with rel_alloc sf have rel_alloc': "rel_alloc 𝒮 M1 (A  B) t0' s t"
    by (auto simp add: t0'_def rel_alloc_def)
  from spec [OF rel_alloc'] have refines': "refines f g s t (rel_stack 𝒮 M (A  B) s t0' Q)" .
  show ?thesis
  proof (rule refinesI)
    show "succeeds g t  succeeds f s" using refines'
      by (auto simp add: refines_def_old)
  next
    fix v s'
    assume succeeds: "succeeds g t" "succeeds f s" 
    assume result: "reaches f s v s'" 
    show "w t'. reaches g t w t'  rel_stack 𝒮 M A s t0 Q (v, s') (w, t')"
    proof - 
      from succeeds result refines' obtain w t' 
        where  
          res: "reaches g t w t'" and 
          stack: "rel_stack 𝒮 M (A  B) s t0' Q (v, s') (w, t')"
        by (fastforce simp add: refines_def_old)
      from stack obtain 
        mem_eq: "equal_upto (M  stack_free (htd s')) (hmem s') (hmem s)"  and
        htd_eq1: "equal_upto M (htd s') (htd s)" and
        htd_eq2: "equal_on 𝒮 (htd s') (htd s)"
        by (auto simp add: rel_stack_def)
  
      from stack
      have sf_eq: "stack_free (htd s') = stack_free (htd s)"
        using disj_A_B by (auto simp add: rel_stack_def) 

      have htd_eq: 
        "override_on (htd s') (override_on (htd t0) (htd s) B) (A  B - stack_free (htd s)) = 
              override_on (htd s') (htd t0) (A - stack_free (htd s))"
        using disj_A_B disj_B_M  sf sf_eq htd_eq1
        apply (clarsimp simp add: override_on_def fun_eq_iff)
        by (auto simp add: equal_upto_def orthD1)

      have hmem_eq: 
        "override_on (hmem s') (override_on (hmem t0) (hmem s) B) (A  B  stack_free (htd s)) = 
             override_on (hmem s') (hmem t0) (A  stack_free (htd s))"
        using disj_A_B disj_B_M sf sf_eq mem_eq
        by (auto simp add: override_on_def fun_eq_iff disjoint_iff equal_upto_def)
    

      from stack have rel_stack': "rel_stack 𝒮 M A s t0 Q (v, s') (w, t')"
        apply (simp add: t0'_def)
        apply (simp add: rel_stack_def rel_alloc_def)
        apply (clarsimp simp add: frame_def raw_frame_def sf_eq)
        using htd_eq mem_eq 
        by auto (metis (no_types, lifting) heap.upd_cong hmem_eq hmem_htd_upd typing.upd_cong)

      then show ?thesis using res
        by auto
    qed
  qed
qed


lemma refines_narrow_frame:
  assumes subset: "B  A"
  assumes disj_B_M: "B  M = {}"
  assumes spec: "t0 s t. rel_alloc 𝒮 M1 A t0 s t  refines f g s t (rel_stack 𝒮 M A s t0 Q)"
  assumes sf: "stack_free (htd s)  B = {}"
  assumes rel_alloc: "rel_alloc 𝒮 M1 (A - B) t0 s t"
  shows "refines f g s t (rel_stack 𝒮 M (A - B) s t0 Q)"
proof -
  from subset obtain A1 where A: "A = A1  B" and disj: "A1  B = {}" and A1: "A1 = A - B"
    by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int inter_sub)
  from refines_narrow_frame'[OF disj_B_M disj spec [simplified A] sf] rel_alloc
  show ?thesis
    by (auto simp add: A1)
qed

lemma refines_widen_modifies:
  assumes "rel_alloc S M A t0 s t"
  assumes "refines f g s t (rel_stack S M' A s t0 Q)"
  assumes "M'  M"
  shows "refines f g s t (rel_stack S M A s t0 Q)" 
  using assms
  apply (clarsimp simp add: refines_def_old  rel_stack_def rel_alloc_def split: prod.splits xval_splits)
  by (smt (verit) UnI2 Un_assoc equal_on_stack_free_preservation equal_upto_def sup.absorb_iff1)

lemma refines_widen_modifies':
  assumes "rel_alloc S M A t0 s t  refines f g s t (rel_stack S M' A s t0 Q)"
  assumes "M'  M"
  assumes "rel_alloc S M A t0 s t"
  shows "refines f g s t (rel_stack S M A s t0 Q)" 
  using refines_widen_modifies assms by blast

lemma refines_widen_modifies'':
  assumes "rel_alloc S M A t0 s t"
  assumes "refines f g s t (rel_stack S M1 A s t0 Q)"
  assumes "M1  M2"
  assumes "M2  M"
  shows "refines f g s t (rel_stack S M2 A s t0 Q)" 
  using refines_widen_modifies assms rel_alloc_modifies_antimono
  by blast


lemma refines_widen_modifies_weaken:
  assumes alloc: "rel_alloc S M A t0 s t"
  assumes f: "refines f g s t (rel_stack S M1 A s t0 Q')"
  assumes M1_M2: "M1  M2"
  assumes M2_M: "M2  M"
  assumes weaken: "h r r'. Q' h r r'  Q h r r'"
  shows "refines f g s t (rel_stack S M2 A s t0 Q)" 
proof -
  have "refines f g s t (rel_stack S M1 A s t0 Q)"
    apply (rule refines_weaken [OF f])
    using weaken by (auto simp add: rel_stack_def)
  with alloc M1_M2 M2_M refines_widen_modifies rel_alloc_modifies_antimono refines_weaken
  show ?thesis
    by blast
qed

lemma L2_condition_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes c_c': "c s = c' (frame A t0 s)"
  assumes f1_g1: "refines f1 g1 s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes f2_g2: "refines f2 g2 s t (rel_stack 𝒮 M2 A s t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  assumes M2: "M2  M"
  assumes M': "M' = M1  M2"
  shows "refines (L2_condition c f1 f2) (L2_condition c' g1 g2) s t (rel_stack 𝒮 M' A s t0 (rel_xval_stack L R))"
  unfolding L2_condition_def
  apply (rule refines_condition)
  subgoal using s_t c_c' by (auto simp add: rel_alloc_def)
  subgoal apply (rule refines_widen_modifies [OF _ f1_g1]) using s_t M1 M2 M' rel_alloc_modifies_antimono by auto 
  subgoal apply (rule refines_widen_modifies [OF _ f2_g2]) using s_t M1 M2 M' rel_alloc_modifies_antimono by auto
  done


lemma L2_while_rel_stack'':
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes R_i: "R (hmem s) i i'"
  assumes refines_condition: "s v v'. R (hmem s) v v'  c' v' (frame A t0 s) = c v s"
  assumes bdy: "s t v v'. R (hmem s) v v'  rel_alloc 𝒮 M1 A t0 s t  c v s  c' v' t  
              refines (f v) (g v') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  shows "refines (L2_while c f i ns) (L2_while c' g i' ns') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  unfolding L2_while_def
  apply (rule refines_whileLoop_exn)
  subgoal by (auto simp add: rel_stack_def refines_condition rel_alloc_def)
  subgoal for v s' w t' 
    apply clarsimp
    apply (rule refines_mono [OF _ bdy])
    subgoal 
      apply (clarsimp simp add: rel_stack_def )
      subgoal by (metis equal_upto_trans)
      done
    apply (auto simp add: rel_stack_def)
    done
  apply (auto simp add: s_t R_i rel_stack_def rel_alloc_modifies_antimono [OF _ M1])
  done

lemma L2_while_rel_stack''':
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes R_i: "R (hmem s) i i'"
  assumes refines_condition: "s v v'. R (hmem s) v v'  c' v' (frame A t0 s) = c v s"
  assumes bdy: "s t v v'. R (hmem s) v v'  rel_alloc 𝒮 M A t0 s t  c v s  c' v' t  
              refines (f v) (g v') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  shows "refines (L2_while c f i ns) (L2_while c' g i' ns') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  unfolding L2_while_def
  apply (rule refines_whileLoop_exn)
  subgoal by (auto simp add: rel_stack_def refines_condition rel_alloc_def)
  subgoal for v s' w t' 
    apply clarsimp
    apply (rule refines_mono [OF _ bdy])
        apply (clarsimp simp add: rel_stack_def )
        apply (metis  equal_upto_trans)
    using s_t by (auto simp add: rel_stack_def rel_alloc_def)
   apply (auto simp add: s_t R_i rel_stack_def rel_alloc_modifies_antimono [OF _ M1])
  done

lemma L2_while_rel_stack':
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes refines_condition: "s v v'. R (hmem s) v v'  c' v' (frame A t0 s) = c v s"
  assumes R_i: "R (hmem s) i i'"
  assumes bdy: "s t v v'. R (hmem s) v v'  rel_alloc 𝒮 M A t0 s t   
              refines (f v) (g v') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes M1: "M1  M"
  shows "refines (L2_while c f i ns) (L2_while c' g i' ns') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  unfolding L2_while_def
  apply (rule refines_whileLoop_exn)
  subgoal by (auto simp add: rel_stack_def refines_condition rel_alloc_def)
  subgoal for v s' w t' 
    apply clarsimp
    apply (rule refines_mono [OF _ bdy])
      apply (clarsimp simp add: rel_stack_def )
      apply (metis equal_upto_trans)
    subgoal by (auto simp add: rel_stack_def)
    subgoal using s_t by (simp add: rel_stack_def) (metis rel_alloc_def)
    done
    apply (auto simp add: s_t R_i rel_stack_def rel_alloc_modifies_antimono [OF _ M1])
  done

lemma L2_while_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes R_i: "R (hmem s) i i'"
  assumes bdy: "s' t' v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  c v s'  c' w t'  
                  equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                  htd s' = htd s 
                refines (f v) (g' w s') s' t' (rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R))"
  assumes refines_condition: "s' t'  v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t' 
            equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)  htd s' = htd s  
            c' w t' = c v s'"
  assumes g'_g: "s' t' v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  
                equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                htd s' = htd s 
                 g' w s' = g w"
  assumes M1: "M1  M"
  shows "refines (L2_while c f i ns) (L2_while c' g i' ns') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  unfolding L2_while_def
  apply (rule refines_mono [where R = "λ(r, s') (w, t').  
         equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
         htd s' = htd s  
         (rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R)) (r, s') (w, t')"  ])
  subgoal
    by (auto simp add: rel_stack_def)
  apply (rule refines_whileLoop_exn)
  subgoal using s_t by (auto simp add: rel_stack_def refines_condition rel_alloc_def)
  subgoal for v s' w t' 
    apply clarsimp
    apply (rule refines_weaken [where R="(rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R))"] )
     apply (subst g'_g [of s' v w t', symmetric])
         apply (simp add: rel_stack_def)

        apply (simp add: rel_stack_def)
    using rel_alloc_def s_t 
        apply force
       apply simp
      apply simp
     apply (rule bdy)
           apply (simp add: rel_stack_def)
               apply (simp add: rel_stack_def)
              using s_t apply (metis equal_on_stack_free_preservation rel_alloc_def)
          apply simp
         apply simp
        apply simp
       apply simp
      apply simp
    apply (clarsimp simp add: rel_stack_def)
    apply (metis equal_upto_trans)
    done
    apply (smt (verit) L2_split_fixup_3 M1 R_i equal_upto_refl heap_state.rel_stack_def heap_state_axioms rel_alloc_modifies_antimono rel_xval_stack_simps(2) s_t)
   apply (auto simp add: s_t R_i rel_stack_def rel_alloc_modifies_antimono [OF _ M1])
  done


lemma L2_while_rel_stack_g_normalised:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes R_i: "R (hmem s) i i'"
  assumes bdy: "s' t' v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  c v s'  c' w t'  
                  equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                  htd s' = htd s 
                refines (f v) (g w) s' t' (rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R))"
  assumes refines_condition: "s' t'  v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t' 
            equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)  htd s' = htd s  
            c' w t' = c v s'"
  assumes M1: "M1  M"
  shows "refines (L2_while c f i ns) (L2_while c' g i' ns') s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  apply (rule L2_while_rel_stack [OF s_t R_i bdy refines_condition _ M1])
  by auto



lemma L2_while_rel_stack_g_normalised_guarded:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes R_i: "R (hmem s) i i'"
  assumes bdy: "s' t' v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'  c v s'  c' w t'  
                  equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
                  htd s' = htd s  
                refines (f v) (g w) s' t' (rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R))"
  assumes refines_condition: "s' t'  v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t' 
            equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)  htd s' = htd s  G' w t' 
            c' w t' = c v s'"
  assumes M1: "M1  M"
  assumes G_G': "G t = G' i' t"
  shows "refines (L2_while c f i ns) 
              (L2_seq (L2_guard G) 
                (λ_. (L2_while c' (λv. L2_seq (g v) (λres. L2_seq (L2_guard (G' res)) (λ_. L2_gets (λ_. res) ns'))) i' ns')) ) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  apply (rule refines_mono [where R = "λ(r, s') (w, t').  
         equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
         htd s' = htd s  
         (rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R)) (r, s') (w, t')"  ])
  subgoal
    by (auto simp add: rel_stack_def)
  unfolding L2_defs gets_return
  apply (rule refines_whileLoop_guard_right)
  subgoal using s_t by (auto simp add: rel_stack_def refines_condition rel_alloc_def)
  subgoal for v s' w t' 
    apply clarsimp
    apply (rule refines_weaken [where R="(rel_stack 𝒮 M1 A s' t0 (rel_xval_stack L R))"] )
     apply (rule bdy)
    subgoal by (auto simp add: rel_stack_def)
    subgoal using rel_alloc_def s_t by (auto simp add: rel_stack_def)
    subgoal by simp
    subgoal by simp
    subgoal using s_t by simp
    subgoal by simp
    subgoal 
      apply (clarsimp simp add: rel_stack_def)
      apply (metis equal_upto_trans)
      done
    done
  subgoal by (auto simp add: rel_stack_def)
  subgoal using R_i s_t by (auto simp add: rel_stack_def rel_alloc_modifies_antimono [OF _ M1])
  subgoal using G_G' by simp
  done


lemma L2_unknown_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_unknown ns) (L2_unknown ns) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
  using s_t
  by (auto simp add: L2_unknown_def refines_def_old rel_stack_def rel_alloc_modifies_antimono)

lemma L2_fail_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  shows "refines (L2_fail) (L2_fail) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L R))"
  using s_t
  by (auto simp add: L2_fail_def refines_def_old rel_stack_def rel_alloc_modifies_antimono)

lemma L2_skip_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  shows "refines L2_skip L2_skip s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
  using s_t
  by (auto simp add: L2_gets_def refines_def_old rel_stack_def rel_alloc_modifies_antimono)

(* FIXME: derive more simple rule or setup simplification for standard cases: 
  e.g. r'=r and heap / heap_typing does not change at all
*)
lemma L2_spec_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "t'. (frame A t0 s, t')  r'  s'. (s, s')  r"
  assumes "s'. (s, s')  r  (frame A t0 s, frame A t0 s')  r'"
  assumes "s'. (s, s')  r  equal_upto (M  stack_free (htd s')) (hmem s') (hmem s)" 
  assumes "s'. (s, s')  r  htd s' = htd s"
  assumes "s'. (s, s')  r  stack_free (htd s')  𝒮" 
  assumes "s'. (s, s')  r  stack_free (htd s')  A = {}" 
  assumes "s'. (s, s')  r  stack_free (htd s')  M = {}"
  shows "refines (L2_spec r) (L2_spec r') s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L (λ_. (=))))"
  using assms
  by (auto simp add: L2_spec_def refines_def_old rel_stack_def rel_alloc_def succeeds_bind reaches_bind)


lemma L2_spec_rel_stack':
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "t'. rel_alloc 𝒮 M A t0 s t  (frame A t0 s, t')  r'  s'. (s, s')  r"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  (frame A t0 s, frame A t0 s')  r'"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  equal_upto (M  stack_free (htd s')) (hmem s') (hmem s)"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  htd s' = htd s"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  𝒮"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  A = {}"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  M = {}"
  shows "refines (L2_spec r) (L2_spec r') s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L (λ_. (=))))"
  using s_t assms(2-8) [OF s_t] by (rule L2_spec_rel_stack)

lemma L2_spec_rel_stack_same:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "t'. rel_alloc 𝒮 M A t0 s t  (frame A t0 s, t')  r  s'. (s, s')  r"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  (frame A t0 s, frame A t0 s')  r"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  equal_upto (M  stack_free (htd s')) (hmem s') (hmem s)"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  htd s' = htd s"
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  𝒮" 
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  A = {}" 
  assumes "s'. rel_alloc 𝒮 M A t0 s t  (s, s')  r  stack_free (htd s')  M = {}"
  shows "refines (L2_spec r) (L2_spec r) s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L (λ_. (=))))"
  using assms
  by (rule L2_spec_rel_stack')

lemma L2_spec_rel_stack_heap_agnostic:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes hmem_unchanged: "s s'. (s, s')  r  hmem s' = hmem s"
  assumes htd_unchanged: "s s'. (s, s')  r  htd s' = htd s"
  assumes heap_irrelevant: "s s' f g. (s, s')  r  (hmem_upd g (htd_upd f s), hmem_upd g (htd_upd f s'))  r"
  shows "refines (L2_spec r) (L2_spec r) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
proof -
  have "refines (L2_spec r) (L2_spec r) s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L (λ_. (=))))"
    apply (rule L2_spec_rel_stack_same [OF s_t])
    subgoal premises prems for t'
    proof -
      from prems have r: "(frame A t0 s, t')  r" by simp
      have s_eq: "s = hmem_upd (λ_. hmem s) ((htd_upd (λ_. htd s) (frame A t0 s)))"
        apply (simp add: frame_def)
        by (metis equal_upto_heap_on_def equal_upto_heap_on_frame frame_def heap.get_upd htd_hmem_upd typing.get_upd)
      show ?thesis
        apply (subst s_eq)
        apply (rule exI)
        apply (rule heap_irrelevant)
        apply (rule r)
        done
    qed
    subgoal
      apply (simp add: frame_def)
      using heap_irrelevant htd_unchanged
      by simp
    subgoal
      using hmem_unchanged by simp
    subgoal
      using htd_unchanged by simp
    subgoal
      using htd_unchanged by (simp add: rel_alloc_def)
    subgoal
      using htd_unchanged by (simp add: rel_alloc_def)
    subgoal
      using htd_unchanged by (simp add: rel_alloc_def)
    done
  then show ?thesis
    using hmem_unchanged htd_unchanged
    apply (clarsimp simp add: L2_spec_def refines_def_old rel_stack_def rel_alloc_def reaches_bind 
        succeeds_bind)
      apply (meson UNIV_I image_eqI)
     apply force+
    done
qed



(* FIXME: how to setup automatic refinement proof? Simplified setup for standard cases, e.g. relation
   not touching the heap? 
*)
lemma L2_assume_rel_stack:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes "v s'. (v, s')  f s  
    w. (w, frame A t0 s')  g (frame A t0 s)  rel_stack 𝒮 M A s t0 R (v, s') (w, frame A t0 s')" 
  shows "refines (L2_assume f) (L2_assume g) s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R))"
  using assms
  apply (clarsimp simp add: L2_assume_def refines_def_old rel_alloc_def rel_stack_def)
  by metis

lemma L2_assume_rel_stack_heap_agnostic:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes hmem_unchanged: "a s s'. (a, s')  f s  hmem s' = hmem s"
  assumes htd_unchanged: "a s s'. (a, s')  f s  htd s' = htd s"
  assumes heap_irrelevant: "a s s' g h. (a, s')  f s  (a, hmem_upd h (htd_upd g s'))  f (hmem_upd h (htd_upd g s))"
  shows "refines (L2_assume f) (L2_assume f) s t (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
  apply (rule L2_assume_rel_stack)
  subgoal
    using s_t
    by (auto simp add: L2_assume_def refines_def_old rel_stack_def rel_alloc_def)
  subgoal for v s'
    apply (rule exI[where x=v])
    apply (intro conjI)
    subgoal
      using frame_def heap_irrelevant htd_unchanged by presburger
    subgoal
      apply (clarsimp simp: rel_stack_def frame_def)
      apply (intro conjI)
      subgoal using rel_alloc 𝒮 {} A t0 s t frame_def htd_unchanged rel_alloc_def by force
      subgoal using hmem_unchanged by force
      subgoal using htd_unchanged by blast
      done
    done
  done


lemma refines_rel_stack_embed_result': 
  assumes rel_alloc: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes R1: "v s' w t'. rel_alloc 𝒮 M A t0 s' t'  R (hmem s') v w 
             equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)   
             htd s' = htd s 
              R1 (hmem s') v (emb w)"
  assumes M2_M: "M2  M"
  assumes M1_M2: "M1  M2"
  shows "refines f (L2_seq g (ETA_TUPLED (λx. L2_gets (λ_. emb x) ns))) s t (rel_stack 𝒮 M2 A s t0 (rel_xval_stack L R1))"
  unfolding L2_defs ETA_TUPLED_def
  apply (subst bind_return [symmetric, of f])
  apply (rule refines_bind_bind_exn [OF f])
  subgoal
    using M1_M2 M2_M rel_alloc
    apply (clarsimp simp add: rel_stack_def rel_alloc_def)
    by auto (meson Un_mono equal_upto_mono equalityE)
  subgoal by auto
  subgoal by auto
  subgoal
    apply (clarsimp simp add: gets_return rel_stack_def)
    apply (intro conjI)
    subgoal using R1 rel_alloc by (auto simp add: rel_alloc_def)
    subgoal using M2_M rel_alloc by (auto simp add: rel_alloc_def)
    subgoal using M1_M2 by (meson equal_upto_mono equalityD2 sup.mono)
    done
  done

lemma refines_rel_stack_root_upd_result: 
  assumes rel_alloc: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "P t  refines f (L2_seq (L2_guard P) (λ_. g)) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes R1: "v s' w t'. rel_alloc 𝒮 M A t0 s' t'  R (hmem s') v w  P t 
             equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)   
             htd s' = htd s 
              R1 (hmem s') v (emb w)"
  assumes M2_M: "P t  M2  M"
  assumes M1_M2: "P t  M1  M2"
  shows "refines f (L2_seq (L2_guard P) (λ_. L2_seq g (ETA_TUPLED (λx. L2_gets (λ_. emb x) ns)))) s t (rel_stack 𝒮 M2 A s t0 (rel_xval_stack L R1))"
  using refines_rel_stack_embed_result'[OF assms(1) _ _ assms(4,5), of f g L R R1 emb]
  using assms(2,3)
  by (auto simp add: refines_bind_guard_right_iff L2_defs ETA_TUPLED_def)

lemma refines_rel_stack_embed_exit: 
  assumes rel_alloc: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes L1: "v s' w t'. rel_alloc 𝒮 M A t0 s' t'  L (hmem s') v w 
             equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)   
             htd s' = htd s 
              L1 (hmem s') v (emb w)"
  assumes M2_M: "M2  M"
  assumes M1_M2: "M1  M2"
  shows "refines 
  f (L2_catch g (ETA_TUPLED (λx. L2_throw (emb x) ns))) s t 
  (rel_stack 𝒮 M2 A s t0 (rel_xval_stack L1 R))"
  unfolding L2_defs ETA_TUPLED_def
  apply (subst f_catch_throw [symmetric, of f])
  apply (rule refines_catch [OF assms(2)])
  subgoal
    apply (clarsimp simp add: rel_stack_def, intro conjI)
    subgoal using L1 rel_alloc by (auto simp add: rel_alloc_def)
    subgoal using M2_M rel_alloc by (auto simp add: rel_alloc_def)
    subgoal using M1_M2 by (meson equal_upto_mono equalityD2 sup.mono)
    done
  subgoal by auto
  subgoal by auto
  subgoal 
    apply (simp add: rel_stack_def)
    apply (intro conjI)
    subgoal using M2_M rel_alloc by (auto simp add: rel_alloc_def)
    subgoal using M1_M2 by auto (meson equal_upto_mono equalityD2 sup.mono)
    done
  done

lemma refines_rel_stack_embed_both: 
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes L: "v s' w t'. rel_alloc 𝒮 M A t0 s' t'  L (hmem s') v w 
             equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)   
             htd s' = htd s 
              L1 (hmem s') v (embL w)"
  assumes R: "v s' w t'. rel_alloc 𝒮 M A t0 s' t'  R (hmem s') v w 
             equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)   
             htd s' = htd s 
              R1 (hmem s') v (embR w)"
  assumes M2_M: "M2  M"
  assumes M1_M2: "M1  M2"
  shows "refines 
  f  
  (L2_seq  
    (L2_catch g (ETA_TUPLED (λx. L2_throw (embL x) ns)))
    (ETA_TUPLED (λx. L2_gets (λ_. embR x) ns))) s t 
  (rel_stack 𝒮 M2 A s t0 (rel_xval_stack L1 R1))"
  apply (rule refines_rel_stack_embed_result' [OF stack _  _ M2_M M1_M2, where R=R])
  subgoal
    apply (rule refines_rel_stack_embed_exit [OF stack f_g ])
    subgoal
      by (rule L)
    subgoal using M1_M2 M2_M by auto
    subgoal by auto
    done
  subgoal
    by (rule R)
  done
end

 (*
  {p, q, y} ⊆ A
  {p1, q1} ∩ A = {}
*)
lemma refines_assume_result_and_state_left: 
  assumes "s' v. (v, s')  A s  refines (f v) g s' t Q"
  shows "refines (do { v <- assume_result_and_state A; f v }) g s t Q"
  using assms
  apply (auto simp add: refines_def_old succeeds_bind reaches_bind split: xval_splits)
  done

lemma refines_assume_result_and_state_right: 
  assumes "A t  {}"
  assumes "t' v. (v, t')  A t  refines f (g v) s t' Q"
  shows "refines f (do { v <- assume_result_and_state A; g v })  s t Q"
  using assms
  apply (clarsimp simp add: refines_def_old succeeds_bind reaches_bind 
      split: exception_or_result_splits )
  by auto (metis (no_types, opaque_lifting) Result_eq_Result is_Result_simps(1) is_Result_simps(2))

lemma refines_assume_result_and_state_both: 
  assumes "B t = {}  A s = {}"
  assumes "s' v t' w. (v, s')  A s  (w, t')  B t  refines (f v) (g w) s' t' Q"
  shows "refines (do { v <- assume_result_and_state A; f v }) (do {w <- assume_result_and_state B; g w }) s t Q"
  apply (rule refines_bind')
  apply (simp add: refines_assume_result_and_state_iff)
  using assms
  by (force simp add: sim_set_def)

lemma refines_assume_result_and_state_both_same_val': 
  assumes "s' v. (v, s')  A s  t'. (v, t')  B t  refines (f v) (g v) s' t' Q"
  shows "refines (do { v <- assume_result_and_state A; f v }) (do { v <- assume_result_and_state B; g v })  s t Q"
  apply (rule refines_bind')
  apply (simp add: refines_assume_result_and_state_iff)
  using assms
  by (force simp add: sim_set_def)


lemma refines_assume_result_and_state_both_same_val: 
  assumes "v s'. (v, s')  A s  t'. (v, t')  B t"
  assumes "s' v t'. (v, s')  A s  (v, t')  B t  refines (f v) (g v) s' t' Q"
  shows "refines (do { v <- assume_result_and_state A; f v }) (do { v <- assume_result_and_state B; g v }) s t Q"
  apply (rule refines_bind')
  apply (simp add: refines_assume_result_and_state_iff)
  using assms
  by (force simp add: sim_set_def)


lemma refines_assume_result_and_state_both_same_val_frame: 
  assumes f: "t = frm s"
  assumes "s' v. (v, s')  A s  (v, frm s')  B t"
  assumes "s' v. (v, s')  A s   refines (f v) (g v) s' (frm s') Q"
  shows "refines (do { v <- assume_result_and_state A; f v }) (do { v <- assume_result_and_state B; g v }) s t Q"
  apply (rule refines_bind')
  apply (simp add: refines_assume_result_and_state_iff)
  using assms
  by (force simp add: sim_set_def)

lemma refines_on_exit_left:
  assumes f_g: "refines f g s0 t Q'"
  assumes 1: "s. s'. (s, s')  cleanup "
  assumes 2: "s v t w s'. Q' (v, s) (w, t)  (s, s')  cleanup  Q (v, s') (w, t)"
  shows "refines (on_exit f cleanup) g s0 t Q"
  unfolding on_exit_def
  apply (subst on_exit'_skip[of g, symmetric])
  apply (rule refines_on_exit'[OF f_g[THEN refines_weaken]])
  apply (auto simp: refines_yield_right_iff runs_to_iff 1 2)
  done

lemma refines_on_exit_same_cleanup:
  assumes f_g: "refines f g s0 t Q'"
  assumes 1: "s. s'. (s, s')  cleanup "
  assumes 2: "s v t w s' t'. Q' (v, s) (w, t)  (s, s')  cleanup  (t, t')  cleanup  Q (v, s') (w, t')"
  shows "refines (on_exit f cleanup) (on_exit g cleanup) s0 t Q"
  unfolding on_exit_def
  apply (rule refines_on_exit'[OF f_g[THEN refines_weaken]])
  using 1 2
  apply clarsimp
  apply (rule refines_state_select)
   apply force
  apply force
  done

lemma refines_on_exit_same_cleanup_choice:
  assumes f_g: "refines f g s0 t Q'"
  assumes 1: "s. s'. (s, s')  cleanup "
  assumes 2: "s v t w s'. Q' (v, s) (w, t)  (s, s')  cleanup  t'. (t, t')  cleanup  Q (v, s') (w, t')"
  shows "refines (on_exit f cleanup) (on_exit g cleanup) s0 t Q"
  unfolding on_exit_def
  apply (rule refines_on_exit'[OF f_g[THEN refines_weaken]])
  using 1 2
  apply clarsimp
  apply (rule refines_state_select)
  apply auto
  done
  
lemma refines_runs_to_partial_fuse_both:
  assumes sim: "refines f f' s s' Q"
  assumes runs_to_f: "f  s ?⦃P1"
  assumes runs_to_f': "f'  s' ?⦃P2"
  shows "refines f f' s s' (λ(r,t) (r',t'). Q (r,t) (r',t')  P1 r t  P2 r' t')"
  using sim runs_to_f runs_to_f'
  apply (force simp add: refines_def_old runs_to_partial_def_old )
  done

definition "domain_bound A Q = (h h'. equal_on A h h'  Q h = Q h')"

lemma domain_bound_equal_on: "domain_bound A Q  equal_on A h h'  Q h = Q h'"
  by (auto simp add: domain_bound_def)

lemma domain_bound_equal_on_subset: "domain_bound A Q  A  A'  equal_on A' h h'  Q h = Q h'"
  using domain_bound_equal_on equal_on_mono by blast

lemma domain_bound_heap_update_list:
  fixes p::"'a::mem_type ptr"
  assumes "domain_bound A Q"
  assumes "length bs = size_of TYPE('a)"
  assumes "ptr_span p  A = {}"
  shows  "Q (heap_update_list (ptr_val p) bs h) = Q h"
  using assms domain_bound_equal_on 
  by (smt (verit, best) equal_on_def heap_update_nmem_same orthD2)


named_theorems domain_bound_intros

lemma domain_bound_mono: "A  A'  domain_bound A Q  domain_bound A' Q"
  by (auto simp add: domain_bound_def equal_on_mono)

lemma domain_bound_eq: "domain_bound {} (λ_. (=))"
  by (auto simp add: domain_bound_def)

lemma domain_bound_rel_sum_stack[domain_bound_intros]: "domain_bound A L  domain_bound A R  domain_bound A (rel_sum_stack L R)"
  by (auto simp add: domain_bound_def rel_sum_stack_def)

lemma domain_bound_rel_xval_stack[domain_bound_intros]: "domain_bound A L  domain_bound A R  domain_bound A (rel_xval_stack L R)"
  by (auto simp add: domain_bound_def rel_xval_stack_def)

lemma domain_bound_unreachable_exit [domain_bound_intros]: 
  "domain_bound A (rel_exit (λ_ _ _. False))"
  by (auto simp add: domain_bound_def rel_exit_def)

lemma domain_bound_bot[domain_bound_intros]: "domain_bound A (λ_ _ _. False)"
  by (auto simp add: domain_bound_def)

lemma domain_bound_eq'[domain_bound_intros]: "domain_bound A (λ_. (=))"
  using domain_bound_eq domain_bound_mono by blast

lemma domain_bound_top[domain_bound_intros]: "domain_bound A (λ_ _ _. True)"
  by (auto simp add: domain_bound_def)

lemma domain_bound_rel_singleton_stack: "domain_bound (ptr_span p) (rel_singleton_stack p)"
  using domain_rel_singleton_stack by (auto simp add: domain_bound_def)

lemma domain_bound_rel_exit[domain_bound_intros]: 
  "domain_bound A Q  domain_bound A (rel_exit Q)"
  by (auto simp add: rel_exit_def domain_bound_def)

lemma domain_bound_rel_singleton_stack'[domain_bound_intros]: 
  "ptr_span p  A  domain_bound A (rel_singleton_stack p)"
  using domain_bound_rel_singleton_stack domain_bound_mono by blast

lemma domain_rel_push: "domain_bound A Q  equal_on (ptr_span p  A) h h'  rel_push p Q h = rel_push p Q h'" 
  apply (simp add: domain_bound_def rel_push_def fun_eq_iff) 
  by (metis Un_upper1 domain_rel_singleton_stack equal_on_mono rel_singleton_stack_def sup_commute)

lemma domain_bound_rel_push: "domain_bound A Q  domain_bound (ptr_span p  A) (rel_push p Q)"
  using domain_rel_push domain_bound_def by blast

lemma domain_bound_rel_push'[domain_bound_intros]: "ptr_span p  A  domain_bound A Q  domain_bound A (rel_push p Q)"
  using domain_bound_rel_push 
  by (metis (no_types, lifting) subset_Un_eq)



context stack_heap_state
begin


(* FIXME: make variant with arbitrary n not just Suc 0 *)
lemma with_fresh_stack_ptr_rel_stack'':
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes domain_bound: "domain_bound A Q"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     [h_val (hmem s') p]  I s;
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) g s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  shows "refines (with_fresh_stack_ptr (Suc 0) I f) g s t (rel_stack 𝒮 M1 A s t0 Q) "
  unfolding with_fresh_stack_ptr_def
  apply (rule refines_assume_result_and_state_left)
  apply clarsimp
  subgoal for p d vs bs
    apply (rule refines_on_exit_left)
      apply (rule f  [of _ _ "htd_upd (λd. override_on d stack_byte_typing (ptr_span p)) t0"])
    subgoal 
      by (erule stack_allocs_cases) (auto)
    subgoal 
      using stack_allocs_stack_subset_stack_free by fastforce
    subgoal 
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def stack_free_def)
    subgoal
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def stack_free_def)
    subgoal
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def)
    subgoal
      apply (erule stack_allocs_cases)
      using stack
      by (metis h_val_heap_update_padding heap.get_upd length_1_conv nth_Cons_0)
    subgoal 
      apply (erule stack_allocs_cases)
      apply (auto simp add: equal_upto_heap_stack_alloc)

      done
    subgoal
      by (simp add: stack_free_stack_allocs)
    subgoal
      apply (frule stack_free_stack_allocs)
      apply (erule stack_allocs_cases)
      using stack M1_M
      apply (simp add: rel_alloc_def)
      apply (simp add: frame_heap_update_padding)
      using frame_stack_alloc
      apply (subst frame_stack_alloc)
         apply (auto simp add: stack_free_def)
      done
    subgoal
      by blast
    subgoal
      apply clarsimp
      apply (clarsimp simp add: rel_stack_def)
      apply (clarsimp simp add: rel_alloc_def)
      apply (intro conjI)
      subgoal 
        apply (erule stack_allocs_cases)
        using domain_bound stack domain_bound_heap_update_list
        apply (simp add: rel_alloc_def)
        by (simp add: disjoint_subset domain_bound_heap_update_list)
      subgoal
        by (metis (no_types, lifting) Int_Un_eq(1) distrib_inf_le equal_on_stack_free_preservation 
            in_mono inf_idem rel_alloc_def stack stack_free_stack_allocs stack_free_stack_releases_mono' 
            stack_releases_stack_allocs_inverse subset_drop_Diff_strg)
      subgoal
        by (metis (no_types, lifting) Int_Un_eq(1) distinct_element distrib_inf_le 
            equal_on_stack_free_preservation inf.idem order_antisym_conv rel_alloc_def stack stack_free_stack_allocs stack_free_stack_releases_mono' stack_releases_stack_allocs_inverse subset_drop_Diff_strg)
      subgoal
        apply (erule stack_allocs_cases)
        using M1_M
        by (smt (verit, best) UnE c_guard_def disj_subset disjoint_union_distrib inter_commute
            orthD2 rel_alloc_def stack stack_free_stack_releases)

      subgoal
        apply (erule stack_allocs_cases)
        apply (subst frame_stack_release)
        subgoal by auto
        subgoal by auto (metis IntI empty_iff mem_Collect_eq rel_alloc_def stack stack_free_def)
        subgoal by auto (meson c_null_guard_def)
         apply auto
        done
      subgoal
        apply (subst stack_free_stack_releases)
        subgoal
          by (meson c_guard_def stack_allocs_cases)
        subgoal 
          apply clarsimp
          by (simp add: equal_upto_def heap_update_nmem_same heap_update_padding_def)
        done
      subgoal 
        using stack_allocs_releases_equal_on_stack
        by (smt (verit, del_insts) UnE add.right_neutral equal_upto_def mult_is_0 
            stack_releases_footprint stack_releases_other stack_releases_stack_allocs_inverse times_nat.simps(2))
      done
    done
  done

lemma gen_with_fresh_stack_ptr_rel_stack:
  assumes I': "hd ` I s  I'" ― ‹There are two cases of local variables: I s = (λ_. UNIV)› (unitialized) and I s = (λ_. {v})› (initialized) ›
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes domain_bound: "domain_bound A Q"
  assumes f: "p s' t0 v. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     [v]  I s;
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g v) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  shows "refines (with_fresh_stack_ptr (Suc 0) I f) (select I' >>= g) s t (rel_stack 𝒮 M1 A s t0 Q) "
  unfolding with_fresh_stack_ptr_def
  apply (rule refines_assume_result_and_state_left)
  apply clarsimp
  subgoal for p d vs bs
    apply (rule refines_on_exit_left)
      apply (rule refines_select_right_witness [where x="hd vs"])
      subgoal  using I'
        by auto
      apply (rule f  [of _ _ _ "htd_upd (λd. override_on d stack_byte_typing (ptr_span p)) t0"])
    subgoal 
      by (erule stack_allocs_cases) (auto)
    subgoal 
      using stack_allocs_stack_subset_stack_free by fastforce
    subgoal 
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def stack_free_def)
    subgoal
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def stack_free_def)
    subgoal
      apply (erule stack_allocs_cases)
      using stack
      by (auto simp add: rel_alloc_def)
    subgoal
      apply (erule stack_allocs_cases)
      apply (cases vs)
       apply (auto simp add:  h_val_heap_update_padding)
      done
    subgoal
      by (cases vs)  auto
    subgoal 
      apply (erule stack_allocs_cases)
      apply (auto simp add: equal_upto_heap_stack_alloc)
      done
    subgoal
      by (simp add: stack_free_stack_allocs)
    subgoal
      apply (frule stack_free_stack_allocs)
      apply (erule stack_allocs_cases)
      using stack M1_M
      apply (simp add: rel_alloc_def)
      apply (simp add: frame_heap_update_padding)
      using frame_stack_alloc
      apply (subst frame_stack_alloc)
         apply (auto simp add: stack_free_def)
      done
    subgoal
      by blast
    subgoal
      apply clarsimp
      apply (clarsimp simp add: rel_stack_def)
      apply (clarsimp simp add: rel_alloc_def)
      apply (intro conjI)
      subgoal 
        apply (erule stack_allocs_cases)
        using domain_bound stack domain_bound_heap_update_list
        apply (simp add: rel_alloc_def)
        by (simp add: disjoint_subset domain_bound_heap_update_list)
      subgoal
        by (metis (no_types, lifting) Int_Un_eq(1) distrib_inf_le equal_on_stack_free_preservation 
            in_mono inf_idem rel_alloc_def stack stack_free_stack_allocs stack_free_stack_releases_mono' 
            stack_releases_stack_allocs_inverse subset_drop_Diff_strg)
      subgoal
        by (metis (no_types, lifting) Int_Un_eq(1) distinct_element distrib_inf_le 
            equal_on_stack_free_preservation inf.idem order_antisym_conv rel_alloc_def stack stack_free_stack_allocs stack_free_stack_releases_mono' stack_releases_stack_allocs_inverse subset_drop_Diff_strg)
      subgoal
        apply (erule stack_allocs_cases)
        using M1_M 
        by (smt (verit, best) UnE c_guard_def disj_subset disjoint_union_distrib inter_commute
            orthD2 rel_alloc_def stack stack_free_stack_releases)

      subgoal
        apply (erule stack_allocs_cases)
        apply (subst frame_stack_release)
        subgoal by auto
        subgoal by auto (metis IntI empty_iff mem_Collect_eq rel_alloc_def stack stack_free_def)
        subgoal by auto (meson c_null_guard_def)
         apply auto
        done
      subgoal
        apply (subst stack_free_stack_releases)
        subgoal
          by (meson c_guard_def stack_allocs_cases)
        subgoal 
          apply clarsimp
          by (simp add: equal_upto_def heap_update_nmem_same heap_update_padding_def)
        done
      subgoal 
        using stack_allocs_releases_equal_on_stack
        by (smt (verit, del_insts) UnE add.right_neutral equal_upto_def mult_is_0 
            stack_releases_footprint stack_releases_other stack_releases_stack_allocs_inverse times_nat.simps(2))
      done
    done
  done

lemma with_fresh_stack_ptr_rel_stack_uninitialized':
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0 v. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g v) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) (λ_. UNIV) (L2_VARS f ns)) (L2_seq (L2_unknown ns) g) s t (rel_stack 𝒮 M1 A s t0 Q)"
  unfolding L2_seq_def L2_unknown_def L2_VARS_def
  by (rule gen_with_fresh_stack_ptr_rel_stack [OF hd_UNIV stack domain_bound f M1_M])

lemma with_fresh_stack_ptr_rel_stack_uninitialized:
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g' s' p) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes g: "s' p. ptr_span p  A = {}  equal_upto (ptr_span p) (hmem s') (hmem s)  g' s' p = g (h_val (hmem s') p)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) (λ_. UNIV) (L2_VARS f ns)) (L2_seq (L2_unknown ns) g) s t (rel_stack 𝒮 M1 A s t0 Q)"
  using with_fresh_stack_ptr_rel_stack_uninitialized' [OF stack _ M1_M domain_bound] f g
  by (smt (verit, best) equal_upto_heap_on_hmem)

lemma with_fresh_stack_ptr_rel_stack_uninitialized_g_normalised:
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g (h_val (hmem s') p)) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) (λ_. UNIV) (L2_VARS f ns)) (L2_seq (L2_unknown ns) g) s t (rel_stack 𝒮 M1 A s t0 Q)"
  apply (rule with_fresh_stack_ptr_rel_stack_uninitialized [OF stack f _ M1_M domain_bound])
  apply auto
  done

lemma with_fresh_stack_ptr_rel_stack_initialized':
  fixes g::  "('d, 'e, 's) exn_monad"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) g s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) (λ_. {[v]}) (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)"
  unfolding L2_VARS_def
  apply (rule gen_with_fresh_stack_ptr_rel_stack [where I= "(λ_. {[v]})", OF hd_singleton,  simplified select_singleton_conv, OF stack domain_bound f M1_M])
         apply auto
  done

lemma with_fresh_stack_ptr_rel_stack_initialized:
  fixes g::  "('d, 'e, 's) exn_monad"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g' s' p) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes g: "s' p. ptr_span p  A = {}  equal_upto (ptr_span p) (hmem s') (hmem s)  h_val (hmem s') p = v  g' s' p = g"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) (λ_. {[v]}) (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)"
  using with_fresh_stack_ptr_rel_stack_initialized' [OF stack _ M1_M domain_bound] g
    equal_upto_heap_on_hmem f by auto

lemma with_fresh_stack_ptr_rel_stack_fix_initialized:
  fixes g::  "('d, 'e, 's) exn_monad"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) (g' s' p) s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes g: "s' p. ptr_span p  A = {}  equal_upto (ptr_span p) (hmem s') (hmem s)  h_val (hmem s') p = v  g' s' p = g"
  assumes M1_M: "M1  M"
  assumes I: "I s = {[v]}"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)"
proof -
  from I have eq: "run (with_fresh_stack_ptr (Suc 0) (λ_. {[v]}) (L2_VARS f ns)) s = run (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) s"
    unfolding with_fresh_stack_ptr_def
    by (simp add: run_bind)
  from with_fresh_stack_ptr_rel_stack_initialized [OF stack f g M1_M domain_bound]
  have "refines (with_fresh_stack_ptr (Suc 0) (λ_. {[v]}) (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)" .
  from refines_subst_left [OF this ] eq
  show ?thesis
    by blast
qed

lemma with_fresh_stack_ptr_rel_stack_fix_initialized_g_normalised:
  fixes g::  "('d, 'e, 's) exn_monad"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     h_val (hmem s') p = v; 
     equal_upto_heap_on (ptr_span p) s' s;
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) (ptr_span p  A) t0 s' t 
     refines (f p) g s' t (rel_stack 𝒮 (ptr_span p  M1) (ptr_span p  A) s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes I: "I s = {[v]}"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)"
  apply (rule with_fresh_stack_ptr_rel_stack_fix_initialized [OF stack f _ M1_M _ domain_bound])
  using I
            apply auto
  done

lemma with_fresh_stack_ptr_rel_stack:
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f: "p s' t0. 
    
     ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     [h_val (hmem s') p]  I s;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M)  (ptr_span p  A) t0 s' t 
     refines (f p) (g' s' p) s' t (rel_stack 𝒮 (ptr_span p  M1)  (ptr_span p  A) s' t0 Q)"
  assumes g: "s' p. ptr_span p  A = {}  equal_upto (ptr_span p) (hmem s') (hmem s)  [h_val (hmem s') p]  I s  g' s' p = g"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) g s t (rel_stack 𝒮 M1 A s t0 Q)"
  unfolding L2_VARS_def
  using  with_fresh_stack_ptr_rel_stack'' [OF stack domain_bound ] M1_M f g equal_upto_heap_on_hmem
  by auto

lemma refines_rel_stack_project_result:
  assumes "refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R))"
  assumes "h x y. R h x y  R' h x (prj y)"
  shows "refines f (L2_seq g (ETA_TUPLED (λx. L2_gets (λ_. prj x) ns))) s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R'))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs rel_stack_def rel_xval_stack_def ETA_TUPLED_def 
          reaches_bind succeeds_bind
      split: prod.splits sum.splits)
  subgoal for r s'
  apply (cases r)
    subgoal
      apply (clarsimp simp add: default_option_def Exn_def [symmetric])
      by (smt (verit, del_insts) Exn_def Result_neq_Exn case_exception_or_result_Exn rel_xval.simps)
    subgoal
      apply clarsimp
      by (smt (verit, ccfv_SIG) Result_neq_Exn case_exception_or_result_Result rel_xval.cases rel_xval_simps(2))
    done
  done


lemma refines_rel_stack_adjust_result:
  assumes "refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R))"
  assumes "s' t' v w. R (hmem s') v w  rel_alloc 𝒮 M A t0 s' t'   
     equal_upto (M  stack_free (htd s')) (hmem s') (hmem s) 
     equal_upto M (htd s') (htd s) 
     equal_on 𝒮 (htd s') (htd s)  R' (hmem s') v (adj w)"
  shows "refines f (L2_seq g (ETA_TUPLED (λx. L2_gets (λ_. adj x) ns))) s t (rel_stack 𝒮 M A s t0 (rel_xval_stack L R'))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs rel_stack_def rel_xval_stack_def ETA_TUPLED_def 
          reaches_bind succeeds_bind
      split: prod.splits sum.splits)
  subgoal for r s'
  apply (cases r)
    subgoal
      apply (clarsimp simp add: default_option_def Exn_def [symmetric])
      by (smt (verit, del_insts) Exn_def Result_neq_Exn case_exception_or_result_Exn rel_xval.simps)
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x="s'" in allE)
      apply (fastforce simp add: rel_xval.simps)
    done
  done
  done



lemma stack_allocs_frame:
  assumes alloc: "(p, d)  stack_allocs (Suc 0) 𝒮 TYPE('a::mem_type) (htd s)"
  shows "d. (p, d)  stack_allocs (Suc 0) 𝒮 TYPE('a::mem_type) (htd (frame A t0 s))"
proof - 
  have "stack_free (htd s)  stack_free (htd (frame A t0 s))"
    by (rule stack_free_htd_frame)
  from stack_allocs_stack_free_mono [OF this alloc]
  show ?thesis .
qed

(* move out *)
lemma heap_list_update_nth:
  "h p. length v  addr_card 
         i < length v 
          (heap_update_list p v h) (p + of_nat i) = v!i"
proof (induct v arbitrary: i)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
  by (metis heap_list_nth heap_list_update)
qed


lemma stack_alloc_simulation_aux:
  fixes p::"'a::mem_type ptr"
  assumes neq_stack_byte: "typ_uinfo_t TYPE('a)  typ_uinfo_t TYPE(stack_byte)"
  assumes disjnt: "stack_free (htd s)  A = {}"
  assumes stack_free: "aptr_span p. root_ptr_valid (htd s) (PTR(stack_byte) a) "
  assumes not_null: "0  ptr_span p"
  assumes lbs: "length bs = size_of TYPE('a)"
  assumes root_ptr: "root_ptr_valid (ptr_force_type p (htd s)) p"
  shows 
  "htd_upd (λx. override_on (ptr_force_type p (htd s)) (htd t0) (A - stack_free (ptr_force_type p (htd s))))
     (hmem_upd (λx. override_on (heap_update_padding p (vs ! 0) bs x) (hmem t0) (A  stack_free (ptr_force_type p (htd s)))) s) =
   htd_upd (λ_. ptr_force_type p (override_on (htd s) (htd t0) (A - stack_free (htd s))))
     (hmem_upd (λx. heap_update_padding p (vs ! 0) bs (override_on x (hmem t0) (A  stack_free (htd s)))) s)"
proof -
  from stack_free have stack_free': "ptr_span p  stack_free (htd s)" 
    by (simp add: stack_free_def subsetI)
  with root_ptr neq_stack_byte
  have sf_eq: "stack_free (ptr_force_type p (htd s)) = stack_free (htd s) - ptr_span p"
    apply (clarsimp simp add: root_ptr_valid_def stack_free_def, intro set_eqI iffI)
     apply (clarsimp, intro conjI)
      apply (smt (verit, best) ptr_force_type_d size_of_def typ_uinfo_size valid_root_footprint_domain_cases) 
     apply (metis (mono_tags, lifting) size_of_tag valid_root_footprint_type_neq)
    by (simp add: ptr_force_type_d valid_root_footprint_def)
  have heap_eq: " override_on (heap_update_padding p (vs ! 0) bs (hmem s)) (hmem t0) (A  (stack_free (htd s) - ptr_span p))
        =
      heap_update_padding p (vs ! 0) bs (override_on (hmem s) (hmem t0) (A  stack_free (htd s)))"
    using disjnt stack_free' lbs
    apply (clarsimp simp add: override_on_def fun_eq_iff, intro conjI impI)
    subgoal by (smt (verit) CTypes.mem_type_simps(2) disjoint_subset heap_update_nmem_same heap_update_padding_def orthD2)
    subgoal by (clarsimp simp add: heap_update_nmem_same heap_update_padding_def)
    by (auto simp add: heap_update_mem_same heap_update_padding_def)
       (smt (verit, best) CTypes.mem_type_simps(2) heap_update_nmem_same heap_update_padding_def subset_iff)

  have htd_eq: "override_on (ptr_force_type p (htd s)) (htd t0) (A - stack_free (ptr_force_type p (htd s)))
    =
    ptr_force_type p (override_on (htd s) (htd t0) (A - stack_free (htd s)))
    "
    apply (simp add: sf_eq)
    using disjnt stack_free'
    by (auto simp add: override_on_def fun_eq_iff ptr_force_type_split)
  show ?thesis
    apply (simp add: sf_eq)
    using heap_eq htd_eq
    by (metis (no_types, lifting) heap.upd_cong sf_eq typing.upd_cong)
qed

lemma keep_with_fresh_stack_ptr_rel_stack':
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes I: "I (frame A t0 s) = I s"
  assumes f: "p s' t0 t. ― ‹I could use the fixed t0
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     [h_val (hmem s') p]  I s;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) A t0 s' t;
     ptr_span p  stack_free (htd s') = {} 
     refines (f p) (g p) s' t (rel_stack 𝒮 (ptr_span p  M1) A s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I f) (with_fresh_stack_ptr (Suc 0) I g) s t (rel_stack 𝒮 M1 A s t0 Q) "
  unfolding with_fresh_stack_ptr_def
  apply (rule refines_assume_result_and_state_both_same_val_frame [where frm = "frame A t0"])
  subgoal using stack by (auto simp add: rel_alloc_def)
  subgoal for s' p 
    using stack I
    apply (clarsimp simp add: rel_alloc_def)
    apply (frule stack_allocs_frame [where A=A and t0=t0])
    apply clarsimp    
    apply (erule stack_allocs_cases)
    subgoal for d vs bs d'
      apply (rule exI[where x=d'])
      apply clarsimp
      apply (rule exI[where x="vs"])
      apply (simp add: I)
      apply (erule stack_allocs_cases)
      apply clarsimp
      apply (rule exI[where x="bs"])
      using stack
 
      apply (clarsimp simp add: frame_def heap_commute comp_def )
      apply (rule stack_alloc_simulation_aux)
      apply auto
      done
    done
  subgoal for s' p
    apply clarsimp
    apply (rule refines_on_exit_same_cleanup_choice)

    apply (rule f [rule_format, where t0="t0" (* t0="htd_upd (λd. override_on d stack_byte_typing (ptr_span p)) t0" *)] )
    subgoal
      by (erule stack_allocs_cases) auto
    subgoal
      apply (erule stack_allocs_cases) 
      by (simp add: stack_free_def subset_iff)
    subgoal 
      using stack rel_alloc_def stack_allocs_stack_subset_stack_free' by fastforce
    subgoal using stack
      by (metis (no_types, lifting) add.right_neutral inf.orderE inf_assoc inf_bot_right mult_is_0 
          rel_alloc_def stack_allocs_stack_subset_stack_free times_nat.simps(2))
    subgoal 
      apply (erule stack_allocs_cases)
      by (metis htd_hmem_upd typing.get_upd)
    subgoal 
      by (metis h_val_heap_update_padding heap.get_upd length_1_conv nth_Cons_0)
    subgoal 
      by (smt (verit, best) append.simps(1) dual_order.refl fold.simps(1) fold.simps(2) 
          heap_state.equal_upto_heap_stack_alloc heap_state_axioms id_comp lense.upd_cong ptr_add_0_id 
          semiring_1_class.of_nat_0 stack_allocs_cases typing.lense_axioms upt.simps(1) upt.simps(2))
    subgoal
      by (simp add: stack_free_stack_allocs)
    subgoal using stack M1_M
      by (smt (verit) Diff_Diff_Int Diff_eq_empty_iff Int_Diff Int_Un_distrib One_nat_def Un_Int_eq(3) 
          add_mult_distrib add_right_cancel htd_hmem_upd inf.absorb_iff2 inf.orderE plus_1_eq_Suc 
          rel_alloc_def stack_allocs_stack_subset_stack_free stack_free_stack_allocs times_nat.simps(2) typing.get_upd)

    subgoal 
      apply (erule stack_allocs_cases)
      by (smt (verit, ccfv_threshold) disjoint_iff htd_hmem_upd in_ptr_span_itself mem_Collect_eq 
          root_ptr_valid_casesE stack_free_def typing.get_upd)
    subgoal by blast
    subgoal for d vs bs s1 v t w s2 
      apply clarsimp
      subgoal for bs1
        apply (rule exI[where x=" hmem_upd 
                  (heap_update_list (ptr_val p) 
                     (heap_list (hmem t0) (size_of TYPE('a)) (ptr_val p))) 
                  (htd_upd (stack_releases (Suc 0) p) t)"])

        apply (rule conjI)
        subgoal using heap_list_length by blast
        using stack
        apply (clarsimp simp add: rel_stack_def)
        apply (intro conjI)
        subgoal
          apply (erule stack_allocs_cases)
          using domain_bound
          by (simp add: disjoint_subset domain_bound_heap_update_list rel_alloc_def)
        subgoal
          apply (clarsimp simp add: rel_alloc_def, intro conjI)
             apply (metis (no_types, lifting) Int_Un_eq(1)  
              in_mono inf_idem stack_free_stack_allocs stack_free_stack_releases_mono' 
              stack_releases_stack_allocs_inverse subset_drop_Diff_strg sup.absorb_iff1)
            apply (metis (no_types, lifting) Int_absorb2 Int_iff Un_Int_eq(4) 
              boolean_algebra.conj_disj_distrib distrib_inf_le orthD1 
              stack_free_stack_allocs stack_free_stack_releases_mono' stack_releases_stack_allocs_inverse subset_drop_Diff_strg) 
          using M1_M 
           apply (smt (verit) c_guard_def disjoint_subset disjoint_union_distrib inter_commute orthD2 
              stack_allocs_cases stack_free_stack_releases)

          apply (erule stack_allocs_cases)
          apply (subst frame_stack_release_keep [where bs=bs1] )
          subgoal
            by (metis disjoint_union_distrib inter_commute)
          subgoal
            by (metis add.right_neutral disjoint_subset mult_Suc mult_is_0)
          subgoal
            by (meson c_guard_def)
          subgoal
            by assumption
          subgoal by simp
          done
        subgoal
          apply (subst stack_free_stack_releases)
          subgoal
            by (meson c_guard_def stack_allocs_cases)
          subgoal 
            apply clarsimp
            by (simp add: equal_upto_def heap_update_nmem_same heap_update_padding_def)
          done
        subgoal 
          using stack_allocs_releases_equal_on_stack
          by (smt (verit, del_insts) UnE add.right_neutral equal_upto_def mult_is_0 
              stack_releases_footprint stack_releases_other stack_releases_stack_allocs_inverse times_nat.simps(2))
        done
      done
    done
  done



lemma keep_with_fresh_stack_ptr_rel_stack:
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes I: "I s = I (frame A t0 s)" ― ‹FIXME: make refinement I' similar to condition in L2_condition› / L2_while›?›
  assumes f: "p s' t0 t. ― ‹I could use the fixed t0
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     [h_val (hmem s') p]  I s;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) A t0 s' t; 
     ptr_span p  stack_free (htd s') = {} 
     refines (f p) (g' s' p) s' t (rel_stack 𝒮 (ptr_span p  M1) A s' t0 Q)"
  assumes g: "s' p. ptr_span p  A = {}  equal_upto (ptr_span p) (hmem s') (hmem s)  [h_val (hmem s') p]  I s 
              g' s' p = g p"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) (with_fresh_stack_ptr (Suc 0) I (L2_VARS g ns)) s t (rel_stack 𝒮 M1 A s t0 Q)"
  unfolding L2_VARS_def
  using keep_with_fresh_stack_ptr_rel_stack' [OF stack I [symmetric] _ M1_M domain_bound] f g 
  using equal_upto_heap_on_hmem by force

lemma keep_with_fresh_stack_ptr_rel_stack_g_normalised:
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes I: "I s = I (frame A t0 s)" ― ‹FIXME: make refinement I' similar to condition in L2_condition› / L2_while›?›
  assumes f: "p s' t0 t. ― ‹I could use the fixed t0
    ptr_span p  𝒮; ptr_span p  stack_free (htd s); 
     ptr_span p  A = {}; ptr_span p  M = {};
     root_ptr_valid (htd s') p;
     [h_val (hmem s') p]  I s;
     equal_upto_heap_on (ptr_span p) s' s; 
     stack_free (htd s')  stack_free (htd s);
     rel_alloc 𝒮 (ptr_span p  M) A t0 s' t; 
     ptr_span p  stack_free (htd s') = {} 
     refines (f p) (g p) s' t (rel_stack 𝒮 (ptr_span p  M1) A s' t0 Q)"
  assumes M1_M: "M1  M"
  assumes domain_bound: "domain_bound A Q"
  shows "refines (with_fresh_stack_ptr (Suc 0) I (L2_VARS f ns)) (with_fresh_stack_ptr (Suc 0) I (L2_VARS g ns)) s t (rel_stack 𝒮 M1 A s t0 Q)"
  apply (rule keep_with_fresh_stack_ptr_rel_stack [OF stack I f _ M1_M domain_bound])
  apply auto
  done

lemma refines_rel_stack_adapt_right: 
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes M1_M: "M1  M"
  assumes f_g: "refines f g s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  assumes h: "s' v t' w.  
    R (hmem s') v w 
    rel_alloc 𝒮 M1 A t0 s' t' 
    equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s) 
    htd s' = htd s  
    refines (L2_gets (λ_. v) ns) (h w) s' t' (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R'))"
  shows "refines f (L2_seq g h) s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R'))"
  using stack M1_M f_g h
  apply (clarsimp simp add: refines_def_old L2_defs 
      rel_stack_def rel_alloc_def succeeds_bind reaches_bind )
  subgoal for r s'
    apply (cases r)
    subgoal for e
      apply (clarsimp simp add: default_option_def Exn_def [symmetric])
      subgoal for y
        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        by (metis (mono_tags, lifting) Exn_def case_exception_or_result_Exn rel_xval_stack_simps(5))
      done
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x="s'" in allE)
      apply (fastforce simp add: rel_xval.simps)
      done
    done
  done


lemma refines_handleE'_both_sides:
  assumes "refines f g s t Q"
  assumes "v v' s' t'. Q (Result v, s') (Result v', t')  R (Result v, s') (Result v', t')"
  assumes "v e' s' t'. Q (Result v, s') (Exn e', t')  refines (return v) (h' e') s' t' R"
  assumes "e v' s' t'. Q (Exn e, s') (Result v', t')  refines (h e) (return v') s' t' R"
  assumes "e e' s' t'. Q (Exn e, s') (Exn e', t')  refines (h e) (h' e') s' t' R"
  shows "refines (f <catch> h) (g <catch> h') s t R"
  by (rule Spec_Monad.refines_catch [OF assms(1) assms(5) assms(4) assms(3) assms(2)])


lemma refines_rel_stack_map_exn:
  assumes f_g: "refines f g s t (rel_stack  𝒮 M A s t0 (rel_xval_stack L R))"
  assumes L: "e e' s'. L (hmem s') e e'  L' (hmem s') (emb e) (emb e')"
  shows "refines (map_value (map_exn emb) f) (map_value (map_exn emb) g) s t (rel_stack  𝒮 M A s t0 (rel_xval_stack L' R))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs 
      rel_stack_def rel_alloc_def reaches_map_value)
  subgoal for s' r
    apply (cases r)
    subgoal for e
      apply (clarsimp simp add: default_option_def Exn_def [symmetric])
      subgoal for y
        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        by auto
      done
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x="s'" in allE)
      apply (auto)
      done
    done
  done


lemma refines_rel_stack_map_exn_exit:
  assumes f_g: "refines f g s t (rel_stack  𝒮 M A s t0 (rel_xval_stack (rel_exit L) R))"
  assumes L: "e e' h. L h e e'  L' h (emb e) (emb' e')"
  shows "refines (map_value (map_exn (emb o the_Nonlocal)) f) (map_value (map_exn (emb')) g) s t (rel_stack  𝒮 M A s t0 (rel_xval_stack L' R))"
  using assms
  apply (clarsimp simp add: refines_def_old L2_defs
      rel_stack_def rel_alloc_def reaches_map_value )
  subgoal for s' r
    apply (cases r)
    subgoal for e
      apply (clarsimp simp add: default_option_def Exn_def [symmetric])
      subgoal for y
        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        apply (auto simp add: rel_exit_def)
        done
      done
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x="s'" in allE)
      apply (auto)
      done
    done
  done


lemma throw_L2_throw_conv: "throw x = L2_throw x []"
  by (simp add: L2_throw_def)

lemma L2_catch_join_exn_conv: 
   "(L2_catch 
          (L2_seq 
            (L2_catch g (λx. L2_seq (liftE (h x)) (λ_. L2_throw (prj x) ns1))) 
            (λs. liftE (g1 s))) 
          (λr. L2_throw (emb r) ns2)) =
       (L2_seq 
         (L2_catch g (λx. L2_seq (liftE (h x)) (λ_. L2_throw (emb (prj x)) ns2))) 
         (λs. liftE (g1 s)))"
  unfolding L2_defs
  
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (auto simp add: runs_to_def_old default_option_def Exn_def)
  done

lemma L2_call_rel_stack_embed_exit:
  assumes L: "e e' h. L h e e'  L' h (emb e) (emb' e')"
  assumes f_g: "refines
    f 
    (L2_seq 
      (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (prj x) ns')))) 
      (λs. liftE (g1 s)))
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"

  shows "refines 
    (L2_call f (emb o the_Nonlocal) ns)
    (L2_seq 
      (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (emb' (prj x)) ns')))) 
      (λs. liftE (g1 s))) 
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L' R))"
proof -
  from refines_rel_stack_map_exn_exit [where L' = L', OF f_g L ]
  have "refines 
         (map_value (map_exn (emb o the_Nonlocal)) f) 
         (map_value (map_exn (emb'))  
             (L2_seq 
                (L2_catch g (λx. L2_seq (liftE (h x)) (λ_. L2_throw (prj x) ns'))) 
                (λs. liftE (g1 s)))) 
         s t (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L' R))" .
  then show ?thesis
    apply (simp add: map_exn_catch_conv L2_catch_def [symmetric] throw_L2_throw_conv)
    apply (simp add:  L2_catch_join_exn_conv)
    apply (simp add: L2_call_def map_exn_catch_conv L2_catch_def [symmetric] L2_throw_def)
    done
qed

lemma L2_call_rel_stack_nest_exit_guarded:
  assumes f_g: "P t  refines
    f 
    (L2_seq (L2_guard P) (λ_. 
      (L2_seq 
        (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (prj x) ns')))) 
        (λs. liftE (g1 s)))))
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"
  assumes L: "e e' h. P t  L h e e'  L' h (emb e) (emb' e')"
  shows "refines 
    (L2_call f (emb o the_Nonlocal) ns)
    (L2_seq (L2_guard P) (λ_. 
      (L2_seq 
        (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (emb' (prj x)) ns')))) 
        (λs. liftE (g1 s))))) 
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L' R))"
  apply (rule refines_L2_guard_right')
  apply (rule L2_call_rel_stack_embed_exit [where L=L and emb=emb and emb'= emb'])
   apply (rule L, assumption+)
  using f_g refines_L2_guard_rightE by fastforce



lemma bind_catch_liftE_assoc: 
  "(do {v  (g <catch> (λx. do {
                                      y  liftE (h x);
                                      throw (exn x y)
                                    }));
           liftE (g1 v)
       }) = 
       (do {v  g; liftE (g1 v)} <catch> (λx. do {
                                      y  liftE (h x);
                                      throw (exn x y)
                                    }))"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff Exn_def[symmetric] elim!: runs_to_weaken)
  done


lemma bind_catch_liftE_split_catch: "(do {
                 s  g;
                 liftE (g1 s)
               } <catch> (λx. do {
                               _  liftE (h x);
                               throw (emb (prj x))
                             })) = 
((do {
                 s  g;
                 liftE (g1 s)
               } <catch> (λx. do {
                               _  liftE (h x);
                               throw (prj x) }))
                <catch> (λx. throw (emb x)))"
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff Exn_def[symmetric] elim!: runs_to_weaken)
  done

lemma refines_catch_right_trans:
  fixes f:: "('e, 'a, 's) exn_monad"
  assumes f_g: "refines f g s t Q"
  assumes R: " r s' e t'. Q (r, s') (Exn e, t')  refines (yield r) (h e) s' t' R"
  assumes Exn_Res: "e s' v' t'. Q (Exn e, s') (Result v', t')  R (Exn e, s') (Result v', t')"
  assumes Res_Res: "v v' s' t'. Q (Result v, s') (Result v', t')  R (Result v, s') (Result v', t')"
  shows "refines f (g <catch> h) s t R"
  apply (subst f_catch_throw[symmetric, of f])
  apply (rule refines_catch [OF f_g])
  subgoal premises prems using R [OF prems(1)] by simp
  subgoal using Exn_Res by (auto simp add: refines_yield_right_iff)
  subgoal premises prems using R [OF prems(1)] by simp
  subgoal using Res_Res by (auto simp add: refines_yield_right_iff)
  done

lemma L2_call_rel_stack_embellish_exit:
  assumes s_t: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "P t  refines
    f 
    (L2_seq (L2_guard P) (λ_. 
      (L2_seq 
        (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (prj x) ns)))) 
        (λs. liftE (g1 s)))))
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"
  assumes L: "s' t' e e'. L (hmem s') e e'  P t  rel_alloc 𝒮 M A t0 s' t' 
            equal_upto (M1  stack_free (htd s')) (hmem s') (hmem s)  htd s' = htd s  
            L' (hmem s') e (emb e')"
  assumes M1: "P t  M1  M"
  shows "refines 
    f
    (L2_seq (L2_guard P) (λ_. 
      (L2_seq 
        (L2_catch g (λx. (L2_seq (liftE (h x)) (λ_. L2_throw (emb (prj x)) ns_exit)))) 
        (λs. liftE (g1 s))))) 
    s t 
    (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L') R))"
  unfolding L2_defs
  apply (clarsimp simp add: refines_bind_guard_right_iff bind_catch_liftE_assoc)
  apply (simp add: bind_catch_liftE_split_catch)
  apply (rule refines_catch_right_trans)
     apply (rule f_g [simplified L2_defs refines_bind_guard_right_iff bind_catch_liftE_assoc, rule_format])
      apply assumption
     apply simp
  subgoal
    apply (clarsimp simp add: rel_stack_def rel_exit_def)
    using L s_t by (auto simp add: rel_alloc_def)
  subgoal
    by (auto simp add: rel_stack_def)
  subgoal
    by (auto simp add: rel_stack_def)
  done

definition "override_heap_on P t1 t2  
  hmem_upd (λh. override_on h (hmem t2) P) 
    (htd_upd (λd. override_on d (htd t2) P) t1)"

lemma override_heap_on_empty [simp]: "override_heap_on {} t1 t2 = t1"
  by (simp add: override_heap_on_def)

lemma refines_rel_stack_override_heap_on_exit:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "s t t0. rel_alloc 𝒮 M (P  A) t0 s t  
    refines f (g s) s t (rel_stack 𝒮 M1 (P  A) s t0 Q)"
  assumes disj_A: "P  A = {}"
  assumes p_M1: "P  M1"
  assumes M1_M: "M1  M"
  assumes disj_stack_free_s: "P  stack_free (htd s) = {}"
  shows "refines f (g s) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) Q)"
proof -
  from stack have sf_s_t: "stack_free (htd s)  stack_free (htd t)"
    using rel_alloc_def stack_free_htd_frame by auto

  from stack have t: "t = frame A t0 s"
    by (auto simp add: rel_alloc_def)

  define t0' where "t0' = override_heap_on P t0 t"

  have eq_htd: 
    "override_on (htd s) (htd t0) (A - stack_free (htd s)) =
        override_on (htd s) (htd t0') ((P  A) - stack_free (htd s))"
    using disj_stack_free_s disj_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  have eq_hmem:
    "override_on (hmem s) (hmem t0) (A  stack_free (htd s)) =
        override_on (hmem s) (hmem t0') ((P  A)  stack_free (htd s))"
    using disj_stack_free_s disj_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  from t have t_t0': "t = frame ((P  A)) t0' s"
    using eq_htd eq_hmem
    apply (simp add: frame_def)
    by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)

  have stack': "rel_alloc 𝒮 M ((P  A)) t0' s t"
    using stack disj_stack_free_s disj_stack_free_s t t_t0'
    by (auto simp add: rel_alloc_def)

  from disj_stack_free_s disj_stack_free_s stack
  have stack_free': "stack_free (htd s)  (P  A) = {}"
    by (auto simp add: rel_alloc_def)

  from f_g [OF stack'] 
  have f_g': "refines f (g s) s t
          (rel_stack 𝒮 M1 ((P  A)) s t0' Q)" .
  then show ?thesis
    by (simp add: t0'_def)
qed

lemma refines_rel_stack_override_heap_on_exit_guarded:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "s t t0. G  rel_alloc 𝒮 M (P  A) t0 s t  
    refines f (L2_seq (L2_guard (λ_. G)) (λ_. g s)) s t (rel_stack 𝒮 M1 (P  A) s t0 Q)"
  assumes disj_A: "G  P  A = {}"
  assumes p_M1: "G  P  M1"
  assumes M1_M: "G  M1  M"
  assumes disj_stack_free_s: "G  P  stack_free (htd s) = {}"
  shows "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g s)) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) Q)"
proof -
  {assume guard: "G" 
    have "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g s)) s t (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) Q)"
      using refines_rel_stack_override_heap_on_exit [OF stack f_g [OF guard] disj_A [OF guard] p_M1 [OF guard] 
          M1_M [OF guard] disj_stack_free_s [OF guard]].}
  then show ?thesis
    by (rule refines_L2_guard_right'')
qed



lemma refines_rel_stack_override_heap_emptyI:
  assumes "refines f g s t (rel_stack 𝒮 M (P  A) s (override_heap_on P t0 t) Q)"
  shows "refines f g s t (rel_stack 𝒮 M (P  {}  A) s (override_heap_on (P  {}) t0 t) Q)"
  using assms
  by simp

lemma refines_rel_stack_pop_heap_both:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f g s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (rel_push p L)) (rel_push p R)))"
  assumes disj_P_A: "P  A = {}"
  assumes disj_p_A: "ptr_span p  A = {}"
  assumes disj_p_P: "ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq 
      (L2_catch g (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_throw (snd x) ns_exit)))) 
      (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_return (snd x) ns)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) R))"
proof -
  from stack have sf_s_t: "stack_free (htd s)  stack_free (htd t)"
    using rel_alloc_def stack_free_htd_frame by auto

  from stack have t: "t = frame A t0 s"
    by (auto simp add: rel_alloc_def)

  define t0' where "t0' = override_heap_on (ptr_span p  P) t0 t"

  have eq_htd: 
    "override_on (htd s) (htd t0) (A - stack_free (htd s)) =
        override_on (htd s) (htd t0') ((ptr_span p  P  A) - stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_P_A disj_p_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  have eq_hmem:
    "override_on (hmem s) (hmem t0) (A  stack_free (htd s)) =
        override_on (hmem s) (hmem t0') ((ptr_span p  P  A)  stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_p_A disj_P_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  from t have t_t0': "t = frame ((ptr_span p  P  A)) t0' s"
    using eq_htd eq_hmem
    apply (simp add: frame_def)
    by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)

  have stack': "rel_alloc 𝒮 M ((ptr_span p  P  A)) t0' s t"
    using stack disj_stack_free_s_P  disj_stack_free_s_p t t_t0'
    by (auto simp add: rel_alloc_def)

  from disj_stack_free_s_p disj_stack_free_s_P disj_stack_free_s_P stack
  have stack_free': "stack_free (htd s)  (P  A) = {}"
    by (auto simp add: rel_alloc_def)


  show ?thesis
    unfolding L2_seq_def
    apply (rule refines_bindE_right [where Q = "λ(v, s') (w, t'). 
        case v of 
          Exn e  w'. w = Exn w'  rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) (λ_ _ _. False)) (Exn e, s') (Exn w', t')
        | Result v  w'. w = Result w'  rel_stack 𝒮 M1 (ptr_span p  P  A) s (override_heap_on (ptr_span p  P) t0 t) (rel_xval_stack (λ_ _ _. False) (rel_push p R)) (Result v, s') (Result w', t')"] )
        apply (rule refines_L2_catch_right)
            apply (rule f_g)
    subgoal by (clarsimp simp add: rel_stack_def t0'_def rel_alloc_def)
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal for e e' s' t' 
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def)
      apply (clarsimp simp add: rel_exit_def) 
      apply (subst (asm) rel_push_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_single_step_right_InL)
      using stack  
      apply (clarsimp simp add: stack_free' rel_alloc_def rel_stack_def t0'_def [symmetric] t [symmetric] t_t0' [symmetric])
      subgoal premises prems for w x
      proof -
        from prems obtain
          "e = Nonlocal x"
          "e' = (h_val (hmem s') p, w)"
          "L (hmem s') x w" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s"  by (simp)
        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal for v v' s' t'
      apply (clarsimp)
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def)
      apply (clarsimp simp add: rel_exit_def) 
      apply (subst (asm) rel_push_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_step_right)
      apply (rule refines_exec_L2_return_right)
      using stack  
      apply (clarsimp simp add: stack_free' rel_alloc_def rel_stack_def t0'_def [symmetric] t [symmetric] t_t0' [symmetric])
      subgoal premises prems for w
      proof -
        from prems obtain
          "v' = (h_val (hmem s') p, w)"
          "R (hmem s') v w" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s" by simp
        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    done
qed

lemma refines_rel_stack_pop_heap_both_guarded:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g)) s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (rel_push p L)) (rel_push p R)))"
  assumes disj_P_A: "G  P  A = {}"
  assumes disj_p_A: "G  ptr_span p  A = {}"
  assumes disj_p_P: "G  ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "G  ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "G  P  stack_free (htd s) = {}"
  shows "refines
    f
    (L2_seq 
      (L2_catch (L2_seq (L2_guard (λ_. G)) (λ_. g))
         (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_throw (snd x) ns_exit))))
      (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_return (snd x) ns)))) s t
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) R))"
proof -
  {
    assume grd: "G"
    have ?thesis
      by (rule refines_rel_stack_pop_heap_both [OF stack f_g disj_P_A [OF grd] disj_p_A [OF grd] disj_p_P [OF grd]
            disj_stack_free_s_p [OF grd] disj_stack_free_s_P [OF grd]])
  } then show ?thesis
    by (rule refines_L2_guard_right'''')
qed

lemma refines_rel_stack_pop_heap_both_singleton:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f g s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (rel_push p L)) (rel_singleton_stack p)))"
  assumes disj_P_A: "P  A = {}"
  assumes disj_p_A: "ptr_span p  A = {}"
  assumes disj_p_P: "ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq 
      (L2_catch g (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_throw (snd x) ns_exit)))) 
      (λx. (IO_modify_heap_paddingE p (λ_. x)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) (λ_. (=))))"
proof -
  from stack have sf_s_t: "stack_free (htd s)  stack_free (htd t)"
    using rel_alloc_def stack_free_htd_frame by auto

  from stack have t: "t = frame A t0 s"
    by (auto simp add: rel_alloc_def)

  define t0' where "t0' = override_heap_on (ptr_span p  P) t0 t"

  have eq_htd: 
    "override_on (htd s) (htd t0) (A - stack_free (htd s)) =
        override_on (htd s) (htd t0') ((ptr_span p  P  A) - stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_P_A disj_p_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  have eq_hmem:
    "override_on (hmem s) (hmem t0) (A  stack_free (htd s)) =
        override_on (hmem s) (hmem t0') ((ptr_span p  P  A)  stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_p_A disj_P_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  from t have t_t0': "t = frame ((ptr_span p  P  A)) t0' s"
    using eq_htd eq_hmem
    apply (simp add: frame_def)
    by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)

  have stack': "rel_alloc 𝒮 M ((ptr_span p  P  A)) t0' s t"
    using stack disj_stack_free_s_P  disj_stack_free_s_p t t_t0'
    by (auto simp add: rel_alloc_def)

  from disj_stack_free_s_p disj_stack_free_s_P disj_stack_free_s_P stack
  have stack_free': "stack_free (htd s)  (P  A) = {}"
    by (auto simp add: rel_alloc_def)


  show ?thesis
    unfolding L2_seq_def
    apply (rule refines_bindE_right [where Q = "λ(v, s') (w, t'). 
        case v of 
          Exn e  w'. w = Exn w'  rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) (λ_ _ _. False)) (Exn e, s') (Exn w', t')
        | Result v  w'. w = Result w'  rel_stack 𝒮 M1 (ptr_span p  P  A) s  (override_heap_on (ptr_span p  P) t0 t) (rel_xval_stack (λ_ _ _. False) (rel_singleton_stack p)) (Result v, s') (Result w', t')"] )
        apply (rule refines_L2_catch_right)
            apply (rule f_g)
    subgoal by (clarsimp simp add: rel_stack_def t0'_def rel_alloc_def)
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal for e e' s' t' 
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def)
      apply (clarsimp simp add: rel_exit_def) 
      apply (subst (asm) rel_push_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_single_step_right_InL)
      using stack  
      apply (clarsimp simp add: stack_free' rel_alloc_def rel_stack_def t0'_def [symmetric] t [symmetric] t_t0' [symmetric])
      subgoal premises prems for w x
      proof -
        from prems obtain
          "e = Nonlocal x"
          "e' = (h_val (hmem s') p, w)"
          "L (hmem s') x w" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s"  by (simp)
        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal by clarsimp
    subgoal for v v' s' t'
      apply (clarsimp)
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def)
      apply (clarsimp simp add: rel_exit_def) 
      apply (subst (asm) rel_singleton_stack_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_single_step_right)
      using stack  
      apply (clarsimp simp add: stack_free' rel_alloc_def rel_stack_def t0'_def [symmetric] t [symmetric] t_t0' [symmetric])
      subgoal premises prems       proof -
        from prems obtain
          "v' = h_val (hmem s') p" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s" by simp
        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    done
qed

lemma refines_rel_stack_pop_heap_both_singleton_guarded:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g)) s t
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s
               (override_heap_on (ptr_span p  P) t0 t)
               (rel_xval_stack (rel_exit (rel_push p L)) (rel_singleton_stack p)))"
  assumes disj_P_A: "G  P  A = {}"
  assumes disj_p_A: "G  ptr_span p  A = {}"
  assumes disj_p_P: "G  ptr_span p  P = {}"
  assumes disj_stack_free_s_p: "G  ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "G  P  stack_free (htd s) = {}"
  shows "refines
    f
    (L2_seq
      (L2_catch (L2_seq (L2_guard (λ_. G)) (λ_. g))
         (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_throw (snd x) ns_exit))))
      (λx. (IO_modify_heap_paddingE p (λ_. x)))) s t
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit L) (λ_. (=))))"
proof -
  {
    assume grd: "G"
    have ?thesis
      by (rule refines_rel_stack_pop_heap_both_singleton [OF stack f_g disj_P_A [OF grd] disj_p_A [OF grd] disj_p_P [OF grd]
            disj_stack_free_s_p [OF grd] disj_stack_free_s_P [OF grd]])
  } then show ?thesis
    by (rule refines_L2_guard_right'''')
qed

lemma refines_rel_stack_pop_heap_no_exit:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f g s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (λ_ _ _. False)) (rel_push p R)))"
  assumes disj_P_A: "P  A = {}"
  assumes disj_p_A: "ptr_span p  A = {}"
  assumes disj_p_P: "ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq g (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_return (snd x) ns)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
proof -
  from stack have sf_s_t: "stack_free (htd s)  stack_free (htd t)"
    using rel_alloc_def stack_free_htd_frame by auto

  from stack have t: "t = frame A t0 s"
    by (auto simp add: rel_alloc_def)

  define t0' where "t0' = override_heap_on (ptr_span p  P) t0 t"

  have eq_htd: 
    "override_on (htd s) (htd t0) (A - stack_free (htd s)) =
        override_on (htd s) (htd t0') ((ptr_span p  P  A) - stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_P_A disj_p_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  have eq_hmem:
    "override_on (hmem s) (hmem t0) (A  stack_free (htd s)) =
        override_on (hmem s) (hmem t0') ((ptr_span p  P  A)  stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_p_A disj_P_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  from t have t_t0': "t = frame ((ptr_span p  P  A)) t0' s"
    using eq_htd eq_hmem
    apply (simp add: frame_def)
    by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)

  have stack': "rel_alloc 𝒮 M ((ptr_span p  P  A)) t0' s t"
    using stack disj_stack_free_s_P  disj_stack_free_s_p t t_t0'
    by (auto simp add: rel_alloc_def)

  from disj_stack_free_s_p disj_stack_free_s_P disj_stack_free_s_P stack
  have stack_free': "stack_free (htd s)  (P  A) = {}"
    by (auto simp add: rel_alloc_def)

  show ?thesis
    unfolding L2_seq_def
    apply (rule refines_bindE_right)
        apply (rule f_g)
       apply simp_all
    subgoal by (simp add: rel_stack_def)
    subgoal for v v' s' t'
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def) 
      apply clarsimp 
      apply (subst (asm) rel_push_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_step_right)
      apply (rule refines_exec_L2_return_right)
      using stack
      apply (clarsimp simp add: rel_stack_def rel_push_def rel_alloc_def stack_free')
      unfolding t0'_def [symmetric] t [symmetric]
      subgoal premises prems for w
      proof -
        from prems obtain
          "v' = (h_val (hmem s') p, w)"
          "R (hmem s') v w" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s"  by simp

        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    done
qed

lemma refines_rel_stack_pop_heap_no_exit_guarded:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g)) s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (λ_ _ _. False)) (rel_push p R)))"
  assumes disj_P_A: "G  P  A = {}"
  assumes disj_p_A: "G  ptr_span p  A = {}"
  assumes disj_p_P: "G  ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "G  ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "G  P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq (L2_seq (L2_guard (λ_. G)) (λ_. g)) (λx. (L2_seq (IO_modify_heap_paddingE p (λ_. (fst x))) (λ_. L2_return (snd x) ns)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
proof -
  {
    assume grd: "G"
    have ?thesis
      by (rule refines_rel_stack_pop_heap_no_exit [OF stack f_g disj_P_A [OF grd] disj_p_A [OF grd] disj_p_P [OF grd]
            disj_stack_free_s_p [OF grd] disj_stack_free_s_P [OF grd]])
  } then show ?thesis
    by (rule refines_L2_guard_right''')
qed

lemma refines_rel_stack_pop_heap_no_exit_singleton:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f g s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (λ_ _ _. False)) (rel_singleton_stack p)))"
  assumes disj_P_A: "P  A = {}"
  assumes disj_p_A: "ptr_span p  A = {}"
  assumes disj_p_P: "ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq g (λx. (IO_modify_heap_paddingE p (λ_. x)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit (λ_ _ _. False)) (λ_. (=))))"
proof -
  from stack have sf_s_t: "stack_free (htd s)  stack_free (htd t)"
    using rel_alloc_def stack_free_htd_frame by auto

  from stack have t: "t = frame A t0 s"
    by (auto simp add: rel_alloc_def)

  define t0' where "t0' = override_heap_on (ptr_span p  P) t0 t"

  have eq_htd: 
    "override_on (htd s) (htd t0) (A - stack_free (htd s)) =
        override_on (htd s) (htd t0') ((ptr_span p  P  A) - stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_P_A disj_p_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  have eq_hmem:
    "override_on (hmem s) (hmem t0) (A  stack_free (htd s)) =
        override_on (hmem s) (hmem t0') ((ptr_span p  P  A)  stack_free (htd s))"
    using disj_stack_free_s_p disj_stack_free_s_P disj_p_A disj_P_A t
    by (auto simp add: t0'_def override_heap_on_def override_on_def fun_eq_iff frame_def)

  from t have t_t0': "t = frame ((ptr_span p  P  A)) t0' s"
    using eq_htd eq_hmem
    apply (simp add: frame_def)
    by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)

  have stack': "rel_alloc 𝒮 M ((ptr_span p  P  A)) t0' s t"
    using stack disj_stack_free_s_P  disj_stack_free_s_p t t_t0'
    by (auto simp add: rel_alloc_def)

  from disj_stack_free_s_p disj_stack_free_s_P disj_stack_free_s_P stack
  have stack_free': "stack_free (htd s)  (P  A) = {}"
    by (auto simp add: rel_alloc_def)

  show ?thesis
    unfolding L2_seq_def
    apply (rule refines_bindE_right)
        apply (rule f_g)
       apply simp_all
    subgoal by (simp add: rel_stack_def)
    subgoal for v' s' t'
      apply (frule rel_stack_unchanged_stack_free [OF stack', unfolded t0'_def])
      apply (frule rel_stack_unchanged_stack_free' [OF stack', unfolded t0'_def])
      apply (subst (asm) rel_stack_def) 
      apply clarsimp 
      apply (subst (asm) rel_singleton_stack_def) 
      apply clarsimp
      apply (rule refines_exec_IO_modify_heap_padding_single_step_right)
      using stack
      apply (clarsimp simp add: rel_stack_def rel_push_def rel_alloc_def stack_free')
      unfolding t0'_def [symmetric] t [symmetric]
      subgoal premises prems 
      proof -
        from prems obtain
          "v' = h_val (hmem s') p" and
          sf_s': "stack_free (htd s') = stack_free (htd s)" and
          sf_t': "stack_free (htd (frame (ptr_span p  P  A) t0' s')) = stack_free (htd t)" and
          "stack_free (htd s)  𝒮"
          "stack_free (htd s)  (ptr_span p  P  A) = {}"
          "stack_free (htd s)  M1 = {}"
          "t' = frame (ptr_span p  P  A) t0' s'"
          "equal_upto (M1  stack_free (htd s)) (hmem s') (hmem s)" and
          htd_eq: "htd s' = htd s"  by simp

        have eq_typing: 
          "override_on (htd s') (htd t0') (ptr_span p  P  A - stack_free (htd s')) =
                  override_on (htd s') (htd (override_heap_on P t0 t)) (P  A - stack_free (htd s'))"
          using disj_P_A disj_p_A 
          by (auto simp add: override_on_def fun_eq_iff t0'_def htd_eq t htd_frame override_heap_on_def)


        have eq_heap: "heap_update_padding p (h_val (hmem s') p)
                    (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p))
                    (override_on (hmem s') (hmem t0') (ptr_span p  P  A  stack_free (htd s'))) = 
                  override_on (hmem s') (hmem (override_heap_on P t0 t)) (P  A  stack_free (htd s'))"
          using disj_P_A disj_p_A
          apply (simp add: override_on_def override_heap_on_def fun_eq_iff t0'_def)
          by (smt (verit, best) disj_p_P disj_stack_free_s_p h_val_def heap_list_length 
              heap_update_list_id' heap_update_list_value heap_update_padding_def 
              hmem_htd_upd max_size orthD2 sf_s' to_bytes_heap_list_id)

        show "hmem_upd
               (heap_update_padding p (h_val (hmem s') p)
                 (heap_list (hmem s') (size_of TYPE('a)) (ptr_val p)))
               (frame (ptr_span p  P  A) t0' s') =
              frame (P  A) (override_heap_on P t0 t) s'"
          apply (simp add: frame_def comp_def)
          using eq_typing eq_heap
          by (metis (no_types, lifting) heap.upd_cong hmem_htd_upd typing.upd_cong)
      qed
      done
    done
qed

lemma refines_rel_stack_pop_heap_no_exit_singleton_guarded:
  fixes p:: "'a::xmem_type ptr"
  assumes stack: "rel_alloc 𝒮 M A t0 s t"
  assumes f_g: "refines f (L2_seq (L2_guard (λ_. G)) (λ_. g)) s t 
             (rel_stack 𝒮 M1 (ptr_span p  P  A) s 
               (override_heap_on (ptr_span p  P) t0 t) 
               (rel_xval_stack (rel_exit (λ_ _ _. False)) (rel_singleton_stack p)))"
  assumes disj_P_A: "G  P  A = {}"
  assumes disj_p_A: "G  ptr_span p  A = {}"
  assumes disj_p_P: "G  ptr_span p  P = {}" 
  assumes disj_stack_free_s_p: "G  ptr_span p  stack_free (htd s) = {}"
  assumes disj_stack_free_s_P: "G  P  stack_free (htd s) = {}"
  shows "refines 
    f 
    (L2_seq (L2_seq (L2_guard (λ_. G)) (λ_. g)) (λx. (IO_modify_heap_paddingE p (λ_. x)))) s t 
    (rel_stack 𝒮 M1 (P  A) s (override_heap_on P t0 t) (rel_xval_stack (rel_exit (λ_ _ _. False)) (λ_. (=))))"
proof -
  {
    assume grd: "G"
    have ?thesis
      by (rule refines_rel_stack_pop_heap_no_exit_singleton [OF stack f_g disj_P_A [OF grd] disj_p_A [OF grd] disj_p_P [OF grd]
            disj_stack_free_s_p [OF grd] disj_stack_free_s_P [OF grd]])
  } then show ?thesis
    by (rule refines_L2_guard_right''')
qed

lemma refines_rel_stack_shuffle_both:
  assumes "refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack (rel_exit L) R))"
  assumes "h e e'. L h e e'  L' h e (shuffle_exit e')"
  assumes "h v v'. R h v v'  R' h v (shuffle v')"
  shows "refines 
    f 
    (L2_seq 
      (L2_catch g (λe. L2_throw (shuffle_exit e) ns_exit))
      (λx. L2_return (shuffle x) ns))
    s t 
    (rel_stack 𝒮 M A s t0 (rel_xval_stack (rel_exit L') R'))"
  using assms
  apply (clarsimp simp add: reaches_bind reaches_catch succeeds_bind succeeds_catch L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_exit_def rel_xval.simps default_option_def Exn_def[symmetric]
      split: xval_splits prod.splits)
  subgoal for r s'
  apply (cases r)
    subgoal 
      apply (clarsimp simp add: default_option_def  Exn_def[symmetric])
      subgoal for y

        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        apply clarsimp
        by (smt (verit) Exn_def Exn_eq_Exn Result_neq_Exn case_exception_or_result_Exn)
      done
    subgoal for v
        apply (erule_tac x="Result v" in allE)
        apply (erule_tac x="s'" in allE)
        apply clarsimp
      by (smt (z3) Result_eq_Result Result_neq_Exn case_exception_or_result_Result)
    done
  done

lemma refines_rel_stack_shuffle_no_exit:
  assumes "refines f g s t (rel_stack 𝒮 M A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  assumes "h v v'. R h v v'  R' h v (shuffle v')"
  shows "refines 
    f 
    (L2_seq 
      g
      (λx. L2_return (shuffle x) ns))
    s t 
    (rel_stack 𝒮 M A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R'))"
  using assms
  apply (clarsimp simp add: succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_sum_stack_def rel_exit_def rel_sum.simps split: sum.splits prod.splits)
  subgoal for r s'
  apply (cases r)
    subgoal 
      apply (clarsimp simp add: default_option_def  Exn_def[symmetric])
      subgoal for y

        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        apply auto
        done
      done
    subgoal for v
        apply (erule_tac x="Result v" in allE)
        apply (erule_tac x="s'" in allE)
        apply clarsimp
        by (smt (z3) Result_eq_Result Result_neq_Exn case_exception_or_result_Result)
      done
    done

lemma L2_call_rel_stack_bare': 
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  shows "refines 
            f
            (L2_call g (λx. x) ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack L R))"
  using assms
  by (auto simp add: L2_call_def refines_def_old reaches_map_value)

lemma L2_call_rel_stack_bare_retype_unreachable_exit': 
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  shows "refines 
            f
            (L2_call g emb ns')
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  using assms
  apply (clarsimp simp add: L2_call_def reaches_map_value succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  by fastforce


lemma L2_call_rel_stack_bare_retype_unreachable_exit'': 
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  shows "refines 
            f
            (L2_seq (L2_guard (λ_. P)) (λ_. 
              (L2_seq (L2_catch (L2_call g emb ns) 
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit)))) 
            (λv. L2_return v ns)))
            s t 
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  using assms
  apply (clarsimp simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  by fastforce

lemma L2_call_rel_stack_bare_retype_unreachable_exit:
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  shows "refines
            f
            (L2_seq (L2_guard (λ_. P)) (λ_.
              (L2_seq (L2_catch (L2_call g undefined ns)
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit))))
            (λv. L2_return v ns)))
            s t
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  by (rule L2_call_rel_stack_bare_retype_unreachable_exit'' [OF f])

lemma L2_call_rel_stack_bare_retype_unreachable_exit_extend_modifies':
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  assumes "P  stack_free (htd s)  M2 = {}"
  assumes M1_M2: "P  M1  M2"
  shows "refines 
            f
            (L2_seq (L2_guard (λ_. P)) (λ_. 
              (L2_seq (L2_catch (L2_call g emb ns) 
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit)))) 
            (λv. L2_return v ns)))
            s t 
            (rel_stack 𝒮 M2 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  using assms
  apply (clarsimp simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  subgoal for r s'
    apply (cases r)
    subgoal 
      apply (clarsimp simp add: Exn_def [symmetric] default_option_def)
      by (metis Result_neq_Exn)
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x=s' in allE)
      apply (clarsimp simp add: Exn_def [symmetric] default_option_def)
      by (smt (z3) case_xval_simps(2) equal_upto_mono map_exn_simps(2) 
          order_eq_refl sup_mono)
    done
  done


lemma L2_call_rel_stack_bare_retype_unreachable_exit_extend_modifies:
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  assumes sf: "P  stack_free (htd s)  M2 = {}"
  assumes M1_M2: "P  M1  M2"
  shows "refines
            f
            (L2_seq (L2_guard (λ_. P)) (λ_.
              (L2_seq (L2_catch (L2_call g undefined ns)
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit))))
            (λv. L2_return v ns)))
            s t
            (rel_stack 𝒮 M2 A s t0 (rel_xval_stack (rel_exit (λ_ _ _. False)) R))"
  by (rule L2_call_rel_stack_bare_retype_unreachable_exit_extend_modifies' [OF f sf M1_M2])

lemma L2_call_rel_stack_bare:
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"
  shows "refines
            f
            (L2_seq (L2_guard (λ_. P)) (λ_.
              (L2_seq (L2_catch (L2_call g (λx. x) ns)
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit))))
            (λv. L2_return v ns)))
            s t
            (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"
  using assms
  apply (clarsimp simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  subgoal for r s'
    apply (cases r)
    subgoal 
      apply (clarsimp simp add: default_option_def  Exn_def[symmetric])
      subgoal for y

        apply (erule_tac x="Exn y" in allE)
        apply (erule_tac x="s'" in allE)
        apply fastforce
        done
      done
    subgoal for v
      apply (erule_tac x="Result v" in allE)
      apply (erule_tac x="s'" in allE)
      apply fastforce
      done
    done
  done

lemma L2_call_rel_stack_bare_extend_modifies:
  assumes f: "refines f g s t
                (rel_stack 𝒮 M1 A s t0 (rel_xval_stack (rel_exit L) R))"
  assumes sf: "P  stack_free (htd s)  M2 = {}"
  assumes M1_M2: "P  M1  M2"
  shows "refines
            f
            (L2_seq (L2_guard (λ_. P)) (λ_.
              (L2_seq (L2_catch (L2_call g (λx. x) ns)
                  (λx. L2_seq (liftE (return ())) (λ_. L2_throw x ns_exit))))
            (λv. L2_return v ns)))
            s t
            (rel_stack 𝒮 M2 A s t0 (rel_xval_stack (rel_exit L) R))"
  unfolding L2_defs L2_VARS_def liftE_return 
  apply (clarsimp simp add: f_catch_throw L2_call_def refines_bind_guard_right_iff)
  apply (rule refines_weaken [OF f])
  using sf M1_M2
  apply (clarsimp simp add: rel_stack_def rel_alloc_def)
  by (meson Un_subset_iff Un_upper2 equal_upto_mono sup.coboundedI1)

lemma refines_rel_stack_extend_modifies:
  assumes f: "refines f (L2_seq (L2_guard (λ_. P)) (λ_. g)) s t (rel_stack 𝒮 M1 A s t0 Q)"
  assumes sf: "P  M2  stack_free (htd s) = {}"
  assumes M1_M2: "P  M1  M2"
  shows "refines f (L2_seq (L2_guard (λ_. P)) (λ_. g)) s t (rel_stack 𝒮 M2 A s t0 Q)"
  using assms
  apply (clarsimp simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch succeeds_bind reaches_bind L2_defs refines_def_old L2_VARS_def
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  by (smt (verit, best) dual_order.refl equal_upto_mono inf_aci(1) sup.mono)

lemma refines_rel_sum_stack_pop_exit': 
  assumes f_g: 
  "refines f g s t 
    (rel_stack 𝒮 M A s t0 
       (rel_xval_stack 
          (rel_exit (rel_push p L)) 
          R))"
  shows   
    "refines f (L2_catch g (λ(x, p). L2_throw p ns)) s t 
      (rel_stack 𝒮 M A s t0 
         (rel_xval_stack 
            (rel_exit L) 
            R))"
  apply (rule refines_L2_catch_right)
      apply (rule f_g)
     apply simp_all
  apply (auto simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch 
      succeeds_bind reaches_bind L2_defs refines_def_old default_option_def Exn_def [symmetric] L2_VARS_def
      rel_push_def 
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  done

lemma refines_rel_sum_stack_pop_exit: 
  assumes f_g: 
  "refines f g s t 
    (rel_stack 𝒮 M A s t0 
       (rel_xval_stack 
          (rel_exit (rel_push p L)) 
          R))"
  shows   
    "refines f (L2_catch g (λx. L2_throw (snd x) ns)) s t 
      (rel_stack 𝒮 M A s t0 
         (rel_xval_stack 
            (rel_exit L) 
            R))"
  apply (rule refines_L2_catch_right)
      apply (rule f_g)
     apply simp_all
  apply (auto simp add: L2_call_def reaches_map_value succeeds_catch reaches_catch 
      succeeds_bind reaches_bind L2_defs refines_def_old default_option_def Exn_def [symmetric] L2_VARS_def
      rel_push_def 
      rel_stack_def rel_alloc_def rel_xval_stack_def rel_xval.simps rel_exit_def)
  done


end



lemma L2_call_fuse_handlers1:
  "L2_seq 
         (L2_catch 
           (L2_seq
              (L2_catch g (λx. L2_seq (liftE (h1 x)) (λ_. L2_throw (prj1 x) ns1))) 
              (λx. liftE (g1 x)))
           (λx. L2_seq (liftE (h2 x)) (λ_. L2_throw (prj2 x) ns2)))
         (λx. liftE (g2 x)) = 
   (L2_seq
       (L2_catch g (λx. L2_seq (L2_seq (liftE (h1 x)) (λ_. liftE (h2 (prj1 x)))) (λ_. L2_throw (prj2 (prj1 x)) ns2))) 
       (λx. L2_seq (liftE (g1 x)) (λx. liftE (g2 x))))"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2_call_fuse_handlers2:
  "(L2_catch 
      (L2_seq
          (L2_catch g (λx. L2_seq (liftE (h1 x)) (λ_. L2_throw (prj1 x) ns1))) 
          (λx. liftE (g1 x)))
      (λx. L2_throw (prj2 x) ns2))
    = 
      L2_seq 
       (L2_catch g (λx. L2_seq (liftE (h1 x)) (λ_. L2_throw (prj2 (prj1 x)) ns2))) 
       (λx. (liftE (g1 x)))"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (auto simp add: runs_to_def_old default_option_def Exn_def split: xval_splits)
  done

lemma L2_call_triv_conv: "L2_call f (λx. x) ns = f"
  unfolding L2_call_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2_catch_L2_call_conv: 
  "L2_catch
     (L2_call f (λe. e) ns) 
     (λe. L2_throw (emb e) ns') = 
   L2_call f (ETA_TUPLED emb) ns"
  apply (simp add: L2_call_triv_conv ETA_TUPLED_def)
  apply (simp add: L2_call_def map_exn_catch_conv L2_catch_def L2_throw_def comp_def)
  done

lemma L2_seq_return_conv: 
  "L2_seq (liftE (return x)) (λx. liftE (return (f x))) = liftE (return (f x))"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done


lemma L2_seq_return_unused_conv: 
  "L2_seq (liftE (return x)) (λ_. g) = g"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2_seq_L2_return_unused_conv: 
  "L2_seq (L2_return x ns) (λ_. g) = g"
  unfolding L2_defs L2_VARS_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2_seq_return_id_conv: 
  "L2_seq f (λx. liftE (return x)) = f"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done


lemma L2_seq_L2_return_id_conv: 
  "L2_seq f (λx. L2_return x ns) = f"
  unfolding L2_defs L2_VARS_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L2_catch_L2_guard_out_conv: "L2_catch (L2_seq (L2_guard P) (λ_. X)) Y = L2_seq (L2_guard P) (λ_. L2_catch X Y)"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done


lemma L2_seq_guard_out_conv: 
  "L2_seq (L2_seq (L2_guard P) (λ_. X)) Y = (L2_seq (L2_guard P) (λ_. L2_seq X Y))"
  by (simp add: L2_seq_assoc)


lemma L2_seq_L2_catch_assoc: 
  "L2_seq (L2_seq (L2_catch X Y) Z1) Z2 = L2_seq (L2_catch X Y) (λx. L2_seq (Z1 x) Z2)"
  by (rule L2_seq_assoc)

lemma L2_catch_throw_id: "L2_catch f (λx. L2_throw x ns) = f"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (clarsimp simp add: runs_to_def_old)
  by (metis Exn_def default_option_def exception_or_result_cases not_None_eq)

lemma L2_catch_call_throw: 
  "(L2_catch 
      (L2_call f emb ns)
      (λx. L2_throw (g x) ns_exit)) = 
    L2_call f (ETA_TUPLED (λx. (g (emb x)))) ns"
  unfolding L2_defs L2_call_def ETA_TUPLED_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


lemma liftE_bind_L2_seq: "(liftE (A >>= B)) = L2_seq (liftE A) (ETA_TUPLED (λx. liftE (B x)))"
  unfolding L2_defs L2_call_def ETA_TUPLED_def
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma liftE_L2_seq: "L2_seq (liftE A) (λx. liftE (B x)) = (liftE (A >>= B))"
  unfolding L2_defs 
  by (simp add: liftE_bind)

lemma liftE_return_L2_gets_conv: "liftE (return x) = L2_gets (λ_. x) []"
  by (simp add: return_L2_gets_conv)

lemmas L2_call_canonical_convs = 
  L2_seq_return_conv
  L2_call_fuse_handlers2
  L2_call_fuse_handlers1
  L2_guard_join_nested
  liftE_L2_seq

  L2_seq_L2_catch_assoc
  L2_catch_L2_guard_out_conv
  L2_seq_guard_out_conv

  bind_assoc

lemmas L2_call_pre_final_convs =
  L2_seq_return_unused_conv
  L2_seq_L2_return_unused_conv
  L2_seq_return_id_conv
  L2_seq_L2_return_id_conv
  L2_catch_call_throw

lemmas L2_call_final_convs = 
  L2_seq_return_unused_conv
  L2_seq_L2_return_unused_conv
  L2_seq_return_id_conv
  L2_seq_L2_return_id_conv
  L2_catch_L2_call_conv
  guard_triv
  liftE_bind_L2_seq
  L2_gets_unbound
  L2_catch_throw_id
  L2_return_L2_gets_conv
  liftE_return_L2_gets_conv

  L2_seq_L2_catch_assoc
  L2_catch_L2_guard_out_conv
  L2_seq_guard_out_conv

lemma L2_call_ETA_TUPLED1: "L2_seq (L2_catch g h) g1  L2_seq (L2_catch g (ETA_TUPLED h)) (ETA_TUPLED g1)"
  unfolding ETA_TUPLED_def by simp

lemma L2_call_ETA_TUPLED2: "L2_seq (L2_call g emb ns) g1  L2_seq (L2_call g emb ns) (ETA_TUPLED g1)"
  unfolding ETA_TUPLED_def by simp


lemma distinct_sets_consI: "distinct_sets ps  distinct_sets (p#ps)  p   (set ps) = {}"
  by (simp)

lemma disjoint_subset_simps:
  "ASSUMPTION (A  B = {})  A'  A  B  A' = {}  True"
  "ASSUMPTION (B  A = {})  A'  A  B  A' = {}  True"
  "ASSUMPTION (A  B = {})  B'  B  B'  A = {}  True"
  "ASSUMPTION (B  A = {})  B'  B  B'  A = {}  True"
  by (auto simp add: ASSUMPTION_def)

lemma disjoint_subset_simps':
  "(B  A = {})  A'  A  B  A' = {}  True"
  "(A  B = {})  B'  B  B'  A = {}  True"
  "(B  A = {})  B'  B  B'  A = {}  True"
  "(A  B = {})  A'  A  B  A' = {}  True"
  by auto

lemma field_lvalue_ptr_span_trans:
  fixes p:: "'a::mem_type ptr"
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)" 
  assumes "export_uinfo t = typ_uinfo_t (TYPE('b))"
  assumes "ptr_span p  A"
  shows "{&(pf)..+size_of TYPE('b::c_type)}  A"
  using field_tag_sub assms export_size_of by fastforce

lemma field_lvalue_ptr_span_root_contained:
  fixes p:: "'a::mem_type ptr"
  assumes "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)" 
  assumes "export_uinfo t = typ_uinfo_t (TYPE('b))"
  shows "{&(pf)..+size_of TYPE('b::c_type)}  ptr_span p"
  using field_tag_sub assms export_size_of by fastforce

lemma field_lvalue_disjoint_fields_same_root:
  fixes p:: "'a::mem_type ptr"
  assumes f: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (T1, n)" 
  assumes exp1: "export_uinfo T1 = typ_uinfo_t (TYPE('b::c_type))"
  assumes g: "field_lookup (typ_info_t TYPE('a)) g 0 = Some (T2, m)"
  assumes exp2: "export_uinfo T2 = typ_uinfo_t (TYPE('c::c_type))"
  assumes prfx1: "¬ prefix f g"
  assumes prfx2: "¬ prefix g f"
  shows "{&(pf)..+size_of TYPE('b::c_type)}  {&(pg)..+size_of TYPE('c::c_type)} = {}"
  using  field_lookup_non_prefix_disj  [OF _ f g prfx2 prfx1] 
   field_lookup_offset_eq [OF f] field_lookup_offset_eq [OF g]  exp1 exp2 
   export_size_of [OF exp1] export_size_of [OF exp2]
  apply simp
  by (smt (verit, best) add.commute add_diff_cancel_left' 
      diff_is_0_eq dual_order.trans export_size_of f field_lookup_offset_size 
      field_lookup_wf_size_desc_gt field_lvalue_def fold_typ_uinfo_t g intvl_fields_disj 
      linorder_not_less max_size nat_less_le unat_of_nat_field_offset wf_size_desc)

lemma ptr_coerce_index_array_ptr_index_conv: 
  "ptr_coerce p +p uint i = array_ptr_index p False (nat (uint i))"
  by (auto simp add: array_ptr_index_def)

lemma ptr_coerce_index_array_ptr_index_numeral_conv: 
  "ptr_coerce p +p (numeral i) = array_ptr_index p False (numeral i)"
  by (auto simp add: array_ptr_index_def)

lemma ptr_coerce_index_array_ptr_index_numeral_conv':
  fixes p:: "(('a :: c_type)['b :: finite]) ptr"
  assumes sz_eq: "size_of TYPE('c::c_type) = size_of TYPE('a)"
  shows "PTR_COERCE('a['b]  'c::c_type) p +p (numeral n) = PTR_COERCE('a  'c) (array_ptr_index p False (numeral n))" 
  using assms
  by (simp add: array_ptr_index_simps(1) c_type_class.ptr_add_def)

lemma ptr_coerce_index_array_ptr_index_numeral_conv'':
  fixes p:: "(('a :: c_type)['b :: finite]) ptr"
  assumes sz_eq: "size_of TYPE('c::c_type) = size_of TYPE('a)"
  assumes bound:  "numeral n < CARD('b)"
  shows "PTR_COERCE('a['b]  'c::c_type) p +p (numeral n) =  PTR('c) &(p[replicate (numeral n) CHR ''1''])" 
proof -
  have eq1: "PTR('c) &(p[replicate (numeral n) CHR ''1'']) = PTR_COERCE('a  'c) (PTR('a) &(p[replicate (numeral n) CHR ''1'']))"
    by simp
  note replicate_numeral [simp del]
  show ?thesis
    apply (subst eq1 )
    apply (subst array_ptr_index_field_lvalue_conv [symmetric, OF bound])
    apply (rule  ptr_coerce_index_array_ptr_index_numeral_conv' [OF sz_eq])
    done
qed

lemma ptr_coerce_index_array_ptr_index_0_conv: 
  "ptr_coerce p +p 0 = array_ptr_index p False 0"
  by (auto simp add: array_ptr_index_def)

lemma ptr_coerce_index_array_ptr_index_1_conv: 
  "ptr_coerce p +p 1 = array_ptr_index p False 1"
  by (auto simp add: array_ptr_index_def)

lemma ptr_coerce_index_array_ptr_index_sint_conv: 
  "0 ≤s i  ptr_coerce p +p sint i = array_ptr_index p False (nat (sint i))"
  by (auto simp add: array_ptr_index_def word_sle_def)

lemma heap_access_Array_element'':
  fixes p :: "('a::mem_type['b::finite]) ptr"
  assumes less: "n < CARD('b)"
  shows
  "index (h_val hp p) n
      = h_val hp (array_ptr_index p False n)"
  using heap_access_Array_element' less
  by auto

lemma index_fupdate_split: "i < CARD('n)  j < CARD('n)  
  index (fupdate i f (x::'a['n::finite])) j = (if i  j then (x.[j]) else f (index x i))"
  by (cases "i=j") (auto simp add: arr_fupdate_same arr_fupdate_other)


lemma root_disjoint_field_lvalue_disjoint1:
  fixes p::"'a::mem_type ptr"
  assumes field_lookup: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t TYPE('f::c_type)"
  assumes "ptr_span p  A = {}"
  shows "A  {&(ppath)..+size_of TYPE('f)} = {}"
  using assms
  by (simp add: disjoint_field_lvalue_propagation_right export_size_of inter_commute)

lemma root_disjoint_field_lvalue_disjoint2:
  fixes p::"'a::mem_type ptr"
  assumes field_lookup: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (t, n)"
  assumes match: "export_uinfo t = typ_uinfo_t TYPE('f::c_type)"
  assumes "ptr_span p  A = {}"
  shows "{&(ppath)..+size_of TYPE('f)}  A = {}"
  using assms
  by (simp add: disjoint_field_lvalue_propagation_right export_size_of inter_commute)

context heap_state_global
begin

lemma global_update_frame_commute:
  shows "glob_upd g (frame A t0 s) =
         frame A t0 (glob_upd g s)"
proof -
  from glob_htd_commute glob_hmem_commute
  show ?thesis
    apply (clarsimp simp add: frame_def)
    by (smt (verit) heap.upd_cong typing.get_upd typing.upd_cong typing.upd_get)
qed

lemma L2_modify_no_heap_update_rel_stack[synthesize_rule refines_in_out]: 
  assumes "rel_alloc 𝒮 M A t0 s t"
  assumes "v s = v' t"
  shows "refines
          (L2_modify (λs. glob_upd (λ_. v s) s))
          (L2_modify (λs. glob_upd (λ_. v' s) s))
          s t
          (rel_stack 𝒮 {} A s t0 (rel_xval_stack L (λ_. (=))))"
proof -
  from  glob_hmem_commute have no_heap1: "g s. hmem (glob_upd g s) = hmem s"
    by (metis heap.get_upd heap.upd_get)

  from glob_htd_commute have no_htd1: "g s. htd (glob_upd g s) = htd s"
    by (metis typing.get_upd typing.upd_get)

  from assms no_heap1 no_htd1 global_update_frame_commute
  show ?thesis
    by (auto simp add: refines_def_old rel_stack_def rel_alloc_def L2_defs)
qed

lemma rel_alloc_glabal_independent_eq [rel_alloc_independent_globals]:
  assumes "rel_alloc 𝒮 M A t0 s t"
  shows "glob t = glob s"
  by (metis assms get_upd global_update_frame_commute rel_alloc_fold_frame upd_get)

end

lemma L2_seq_guard_cong_stateless: 
  "(s. P s = P' s)  (s. P' s  X = X')  
    L2_seq (L2_guard P) (λ_. X) = L2_seq (L2_guard P') (λ_. X')"
  using L2_seq_guard_cong''
  by metis

context globals_stack_heap_state
begin
lemma globals_subset_trans: "NO_MATCH 𝒢 X  NO_MATCH 𝒢 Y  X  𝒢  𝒢  Y  X  Y"
  by blast

lemma globals_disjoint_subset: "NO_MATCH 𝒢 X  X  𝒢  𝒢  A = {}  X  A = {}"
  by blast
end

lemma Union_Diff_right_conv': "X  Y = X  (Y - X)"
  by blast

lemma Union_Diff_right_conv: "(Y - X)  Z  X  Y  X  Z"
  apply (subst Union_Diff_right_conv')
  apply simp
  done

lemma Union_assoc: "X  Y  Z = X  (Y  Z)"
  by (simp add: sup_assoc)

simproc_setup Union_Diff_conv (ptr_span x  Y ) = let
  val cterm_eq = is_equal o Thm.fast_term_ord
  fun dest_union_right ct = ct |> Match_Cterm.switch [
    @{cterm_match ?X  ?Y} #> (fn {X, Y, ...} => X::dest_union_right Y),
    fn _ => [ct]]
in
fn _ => fn ctxt => fn ct =>
  let
    val {X, Y, ...} = @{cterm_match "?X  ?Y"} ct
    val ys = dest_union_right Y
    val _ = if member cterm_eq ys X then () else raise Match
    val lhs = infer_instantiateX = X and Y = Y in cterm "Y - X" ctxt
    val eq = lhs |> Simplifier.asm_full_rewrite (ctxt addsimps @{thms Un_Diff Diff_triv Union_assoc})
    val rhs = Thm.rhs_of eq
  in
    if cterm_eq (lhs, rhs) then 
       NONE 
    else 
       let val eq' = @{thm Union_Diff_right_conv} OF [eq]
           val _ = Utils.verbose_msg 1 (* FIXME *) ctxt (fn _ => "Union_Diff_conv: " ^ Thm.string_of_thm ctxt eq')
       in SOME eq' end
  end
  handle Match => NONE
end
declare [[simproc del: Union_Diff_conv]]

lemma
"ptr_span q  ptr_span p = {}  ptr_span x  ptr_span p = {} 
  (ptr_span p  (ptr_span q  (ptr_span x  ptr_span p))) = ptr_span p  (ptr_span q  ptr_span x) "
  supply [[simproc add: Union_Diff_conv]]
  apply simp
  done

lemma
"ptr_span q  ptr_span p = {}  ptr_span x  ptr_span p = {} 
  ((ptr_span p  ptr_span q)  (ptr_span x  ptr_span p)) = ptr_span p  (ptr_span q  ptr_span x) "
  supply [[simproc add: Union_Diff_conv]]
  apply (simp add: Union_assoc)
  done

lemma
  assumes disj: "ptr_span q  ptr_span p = {}" 
    "ptr_span p  ptr_span q = {}" 
    "ptr_span x  ptr_span p = {}" 
    "ptr_span x  ptr_span q = {}" 
  shows "((ptr_span p  ptr_span q)  ((ptr_span p  ptr_span q)  ptr_span x   ptr_span p)) = ptr_span p  (ptr_span q  ptr_span x) "
  supply [[simproc add: Union_Diff_conv]]
  apply (simp add: Union_assoc disj)
  done

lemma subset_union_left: "X  L  X  L  R"
  by blast

lemma subset_union_right: "X  R  X  L  R"
  by blast

end