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) &(p→f)) 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) &(p→f)) 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) &(p→f)) (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) &(p→f)) 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) &(p→f)) 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 f⇩a f⇩c ≡ corresXF_post st rx ex P Q f⇩a f⇩c"

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 (≥)  (λf⇩a. IOcorres P Q st rx ex f⇩a f⇩c)"
  unfolding IOcorres_def
  by (rule admissible_nondet_ord_corresXF_post)

lemma IOcorres_top [corres_top]: "IOcorres P Q st rx ex ⊤ f⇩c" 
  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 l⇩1) (Inl l⇩2) = L h l⇩1 l⇩2"
  "rel_sum_stack L R h (Inr r⇩1) (Inr r⇩2) = R h r⇩1 r⇩2"
  "rel_sum_stack L R h (Inl l⇩1) (Inr r⇩2) = False"
  "rel_sum_stack L R h (Inr r⇩1) (Inl l⇩2) = False"
  "rel_sum_stack L R h (Inl l⇩1) y = (∃w. y = Inl w ∧ L h l⇩1 w)"
  "rel_sum_stack L R h (Inr r⇩1) y = (∃w. y = Inr w ∧ R h r⇩1 w)"
  "rel_sum_stack L R h x (Inl l⇩2) = (∃v. x = Inl v ∧ L h v l⇩2)"
  "rel_sum_stack L R h x (Inr r⇩2) = (∃v. x = Inr v ∧ R h v r⇩2)"
  by (auto simp add: rel_sum_stack_def rel_sum.simps)

lemma rel_xval_stack_simps [simp]:
  "rel_xval_stack L R h (Exn l⇩1) (Exn l⇩2) = L h l⇩1 l⇩2"
  "rel_xval_stack L R h (Result r⇩1) (Result r⇩2) = R h r⇩1 r⇩2"
  "rel_xval_stack L R h (Exn l⇩1) (Result r⇩2) = False"
  "rel_xval_stack L R h (Result r⇩1) (Exn l⇩2) = False"
  "rel_xval_stack L R h (Exn l⇩1) y = (∃w. y = Exn w ∧ L h l⇩1 w)"
  "rel_xval_stack L R h (Result r⇩1) y = (∃w. y = Result w ∧ R h r⇩1 w)"
  "rel_xval_stack L R h x (Exn l⇩2) = (∃v. x = Exn v ∧ L h v l⇩2)"
  "rel_xval_stack L R h x (Result r⇩2) = (∃v. x = Result v ∧ R h v r⇩2)"
  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 "∃w∈X. 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 t⇩0 ≡ λs t.
     stack_free (htd s) ⊆ S ∧ 
     stack_free (htd s) ∩ A = {} ∧ 
     stack_free (htd s) ∩ M = {} ∧ 
     t = frame A t⇩0 s"

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

lemma rel_alloc_modifies_antimono: "rel_alloc S M2 A t⇩0 s t ⟹ M1 ⊆ M2 ⟹ rel_alloc S M1 A t⇩0 s t"
  by (auto simp add: rel_alloc_def)

lemma rel_alloc_stack_free_disjoint:  
 "rel_alloc S M A t⇩0 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 t⇩0 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 t⇩0 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 t⇩0 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 t⇩0 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 "{&(p→f)..+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 t⇩0 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 "{&(p→f)..+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 t⇩0 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) ∩ {&(p→f)..+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 t⇩0 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) ∩ {&(p→f)..+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 t⇩0 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 t⇩0 R = (λ(v, s') (w, t').
     R (hmem s') v w ∧
     rel_alloc S M A t⇩0 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 t⇩0 s t ⟹ rel_stack S M A s t⇩0 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 t⇩0 s t ⟹ rel_stack S M A s t⇩0 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 t⇩0 s t ⟹ rel_stack S M A s t⇩0 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 t⇩0 s t" 
  assumes rel_stack: "rel_stack S M A s t⇩0 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 t⇩0 s t"
  assumes stack: "rel_stack S M A s t⇩0 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 t⇩0 (rel_xval_stack L R) (Exn v, s') (Exn w, t') = rel_stack S M A s t⇩0 L (v, s') (w, t')"
  by (simp add: rel_stack_def)
lemma rel_stack_Exn_Result[simp]: 
  "rel_stack S M A s t⇩0  (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 t⇩0 (rel_xval_stack L R) (Result v, s') (Result w, t') = rel_stack S M A s t⇩0 R (v, s') (w, t')"
  by (simp add: rel_stack_def)
lemma rel_zero_stack_Result_Exn[simp]: 
  "rel_stack S M A s t⇩0 (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_state∈A. 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 t⇩0 Q) (λ(r, s). (f (hmem s) r, frame A t⇩0 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 t⇩0 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 t⇩0 Q) (λ(r, s). (f (hmem s) r, frame A t⇩0 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 t⇩0 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' ⟹ ∃w∈X. 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. ∃w∈X. 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 ⟹ ∃w∈X. 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' ⟹ ∃w∈X. ∃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' ⟹ ∃w∈X. 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' ⟹ ∃w∈X. ∃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' ⟹ ∃w∈X. 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 t⇩0 s (frame A t⇩0 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 t⇩0) 
           (λr s. prj (hmem s) r) 
           (λr s. prjE (hmem s) (the_Nonlocal r))
           g f
         ⟷ 
         (∀s t. rel_alloc 𝒮 M A t⇩0 s t ⟶ P s ⟶ refines f g s t (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 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 t⇩0 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 t⇩0 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 t⇩0 (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 t⇩0 (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 t⇩0 s))"
  assumes "rel_alloc 𝒮 M A t⇩0 s t"
  shows "refines (L2_gets e ns) (L2_gets e' ns) s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s))"
  assumes "rel_alloc 𝒮 M A t⇩0 s t"
  shows "refines (L2_gets e ns) (L2_gets e' ns') s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s))"
  assumes "rel_alloc 𝒮 M A t⇩0 s t"
  shows "refines (L2_gets e ns) (L2_seq (L2_guard (λ_. G)) (λ_. (L2_gets e' ns'))) s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s t"
  shows "refines (L2_gets (λ_. c) ns) (L2_gets (λ_. c) ns) s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s t"
  shows "refines (L2_gets (λ_. c) ns) (L2_gets (λ_. c') ns) s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s t"
  shows "refines (L2_throw c ns) (L2_throw c' ns') s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t⇩0 (rel_xval_stack (rel_sum_stack L R) R))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t⇩0 (rel_xval_stack (rel_sum_stack L R') R))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 s t"
  assumes "refines f g s t (rel_stack 𝒮 M1 A s t⇩0 (rel_xval_stack (rel_sum_stack L R) R'))"
  shows "refines (L2_try f) (L2_try g) s t (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 s) ⟹ e s"
  assumes "rel_alloc 𝒮 M A t⇩0 s t"
  shows "refines (L2_guard e) (L2_guard e') s t (rel_stack 𝒮 {} A s t⇩0 (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 t⇩0 s))"
  assumes "ptr_span p ⊆ A"
  assumes "rel_alloc 𝒮 (ptr_span p) A t⇩0 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 t⇩0 (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 t⇩0 s))"
  assumes "rel_alloc 𝒮 M A t⇩0 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 t⇩0 (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 t⇩0 s)" 
  assumes "rel_alloc 𝒮 M A t⇩0 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 t⇩0 (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 t⇩0 s)" 
  assumes "rel_alloc 𝒮 M A t⇩0 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 t⇩0 (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 t⇩0 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 t⇩0 (rel_xval_stack L R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb' ns')
            s t 
            (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 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 t⇩0 (rel_xval_stack L R))"
  shows "refines 
            (L2_call f emb ns)
            (L2_call g emb' ns')
            s t 
            (rel_stack 𝒮 M1 A s t⇩0 (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 t⇩0 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 t⇩0 (rel_xval_stack L R))"