Theory AutoCorres2.L2Defs
chapter ‹L2 phase: local variable abstraction with lambdas›
theory L2Defs
imports CorresXF L1Defs L1Peephole L1Valid
begin
type_synonym ('s, 'a, 'e) L2_monad = "('e, 'a, 's) exn_monad"
definition "L2_unknown (ns :: nat list) ≡ select UNIV :: ('s, 'a, 'e) L2_monad"
definition "L2_seq (A :: ('s, 'a, 'e) L2_monad) (B :: 'a ⇒ ('s, 'b, 'e) L2_monad) ≡ (A >>= B) :: ('s, 'b, 'e) L2_monad"
definition "L2_modify m ≡modify m :: ('s, unit, 'e) L2_monad"
definition "L2_gets f (names :: nat list) ≡ gets f :: ('s, 'a, 'e) L2_monad"
definition "L2_condition c (A :: ('s, 'a, 'e) L2_monad) (B :: ('s, 'a, 'e) L2_monad) ≡ condition c A B"
definition "L2_catch (A :: ('s, 'a, 'e) L2_monad) (B :: 'e ⇒ ('s, 'a, 'ee) L2_monad) ≡ (A <catch> B)"
definition "L2_try (A :: ('s, 'a, 'e + 'a) L2_monad) ≡ try A"
definition "L2_while c (A :: 'a ⇒ ('s, 'a, 'e) L2_monad) i (ns :: nat list) ≡ whileLoop c A i :: ('s, 'a, 'e) L2_monad"
definition "L2_throw x (ns :: nat list) ≡ throw x :: ('s, 'a, 'e) L2_monad"
definition "L2_spec r ≡ (state_select r >>= (λ_. select UNIV)) :: ('s, 'a, 'e) L2_monad"
definition "L2_assume r ≡ (assume_result_and_state r) :: ('s, 'a, 'e) L2_monad"
definition "L2_guard c ≡ (guard c) :: ('s, unit, 'e) L2_monad"
definition "L2_guarded P c ≡ L2_seq (L2_guard P) (λ_. c)"
definition "L2_fail ≡ fail :: ('s, 'a, 'e) L2_monad"
definition "L2_call x emb (ns :: nat list) ≡ map_value (map_exn emb) x :: ('s, 'a, 'e) L2_monad"
abbreviation "L2_skip ≡ L2_gets (λ_. ()) []"
definition "L2_VARS f (names::nat list) ≡ f"
definition gets_theE :: "('s ⇒ 'a option) ⇒ ('e, 'a, 's) exn_monad" where
"gets_theE ≡ λx. gets_the x"
definition "L2_folded_gets f names ≡ L2_gets f names :: ('s, 'a, 'e) L2_monad"
definition "L2_voidcall x emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_skip) :: ('s, unit, 'e) L2_monad"
definition "L2_modifycall x m emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_modify (m ret)) :: ('s, unit, 'e) L2_monad"
definition "L2_returncall x f emb ns ≡ L2_seq (L2_call x emb ns) (λret. L2_folded_gets (f ret) []) :: ('s, 'a, 'e) L2_monad"
definition "L2_seq_guard P A ≡ L2_seq (L2_guard P) A"
definition "L2_seq_gets c n A ≡ L2_seq (L2_gets (λ_. c) n) A"
definition "SANITIZE_NAMES prj ns ns' = True"
lemma sanitize_namesI: "SANITIZE_NAMES prj ns ns'"
by (simp add: SANITIZE_NAMES_def)
definition DYN_CALL :: "prop ⇒ prop" where "PROP DYN_CALL (PROP P) ≡ PROP P"
lemma DYN_CALL_I: "PROP P ⟹ PROP DYN_CALL (PROP P)"
by (simp add: DYN_CALL_def)
lemma DYN_CALL_D: "PROP DYN_CALL (PROP P) ⟹ PROP P"
by (simp add: DYN_CALL_def)
lemma runs_to_partial_top[corres_top]: "⊤ ∙ s ?⦃ Q ⦄"
by (simp add: runs_to_partial_def_old)
lemma admissible_runs_to_partial[corres_admissible]: "ccpo.admissible Inf (≥) (λf . f ∙ s ?⦃Q⦄)"
unfolding runs_to_partial_def_old
apply (rule ccpo.admissibleI)
apply (clarsimp simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits xval_splits)
subgoal
apply transfer
apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
by (metis outcomes.simps(2) post_state.distinct(1))
done
lemma reaches_gets_theE [simp]:
"reaches (gets_theE M) s rv s' ⟷ (∃v'. rv = Result v' ∧ s' = s ∧ M s = Some v')"
by (auto simp add: gets_theE_def)
lemma seucceeds_gets_theE [simp]:
"succeeds (gets_theE M) s = (∃v. M s = Some v)"
apply (auto simp add: gets_theE_def)
done
lemma L2_folded_gets_bind:
"L2_seq (L2_folded_gets (λ_. x) ns) f = f x"
unfolding L2_seq_def L2_folded_gets_def L2_gets_def
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
lemma L2_call_throw_names: "L2_call x emb ns = (x <catch> (λr. L2_throw (emb r) ns))"
unfolding L2_call_def L2_throw_def
apply (rule spec_monad_eqI)
apply (clarsimp simp add: runs_to_iff)
apply (auto simp add: runs_to_def_old map_exn_def split: xval_splits)
done
lemmas L2_remove_scaffolding_1 =
L2_folded_gets_bind [THEN eq_reflection]
L2_returncall_def
L2_modifycall_def
L2_voidcall_def
lemmas L2_remove_scaffolding_2 =
L2_remove_scaffolding_1
L2_folded_gets_def
abbreviation (input) "L2_guarded_while G C B i n ≡ L2_seq (L2_guard (G i))
(λ_. L2_while C (λi. L2_seq (B i) (λr. L2_seq (L2_guard (G r)) (λ_. L2_gets (λ_. r) n))) i n)"
lemmas L2_defs = L2_unknown_def L2_seq_def
L2_modify_def L2_gets_def L2_condition_def L2_catch_def L2_while_def
L2_throw_def L2_spec_def L2_assume_def L2_guard_def L2_fail_def L2_folded_gets_def
L2_voidcall_def L2_modifycall_def L2_returncall_def
L2_try_def
lemma L2_defs':
"L2_unknown n ≡ unknown"
"L2_seq A' B' ≡ A' >>= B'"
"L2_modify m ≡ modify m"
"L2_gets f n ≡ gets f"
"L2_condition c L R ≡ condition c L R"
"L2_catch A B ≡ (A <catch> B)"
"L2_try A ≡ try A"
"L2_while c' B'' i n ≡ whileLoop c' B'' i"
"L2_throw x n ≡ throw x"
"L2_spec r ≡ (state_select r >>= (λ_. select UNIV))"
"L2_assume r' ≡ (assume_result_and_state r')"
"L2_guard c ≡ guard c"
"L2_fail ≡ fail"
by (auto simp: L2_defs unknown_def )
definition
L2corres :: "('s ⇒ 't) ⇒ ('s ⇒ 'r) ⇒ ('s ⇒ 'e) ⇒ ('s ⇒ bool)
⇒ ('e, 'r, 't) exn_monad ⇒ (unit, unit, 's) exn_monad ⇒ bool"
where
"L2corres st ret_xf ex_xf P A C
≡ corresXF st (λ_. ret_xf) (λ_. ex_xf) P A C"
lemma admissible_nondet_ord_L2corres [corres_admissible]:
"ccpo.admissible Inf (≥) (λA. L2corres st ret_xf ex_xf P A C)"
unfolding L2corres_def
apply (rule admissible_nondet_ord_corresXF)
done
lemma L2corres_top [corres_top]: "L2corres st ret_xf ex_xf P ⊤ C"
by (auto simp add: L2corres_def corresXF_def)
definition
"L2_call_L1 arg_xf gs ret_xf l1body
= do {
s ← get_state;
t ← select {t. gs t = s ∧ arg_xf t};
run_bind l1body t (λr' t'.
(case r' of
Exception _ ⇒ fail
| Result _ ⇒ do {set_state (gs t'); return (ret_xf t')} ))
}"
lemma L2corres_L2_call_L1:
"L2corres gs ret_xf ex_xf arg_xf
(L2_call_L1 arg_xf gs ret_xf f) f"
apply (clarsimp simp: L2corres_def corresXF_refines_iff L2_call_L1_def L1_seq_def L1_guard_def
split: xval_splits)
apply (simp add: refines_def_old)
apply (intro conjI impI)
subgoal
by (auto simp add: succeeds_bind succeeds_run_bind succeeds_exec_concrete_iff succeeds_catch)
subgoal
by (auto simp add: succeeds_bind succeeds_run_bind reaches_run_bind
succeeds_exec_concrete_iff succeeds_catch reaches_bind default_option_def Exn_def
rel_XF_def rel_xval.simps Exn_def default_option_def
split: exception_or_result_splits)
(smt (verit, ccfv_threshold) Exn_def Exn_neq_Result exception_or_result_cases
imageI mem_Collect_eq old.unit.exhaust option.exhaust_sel)
done
lemma L2corres_L2_call_simpl:
"l1_f ≡ simpl_f ⟹
L2corres gs ret_xf ex_xf arg_xf
(L2_call_L1 arg_xf gs ret_xf simpl_f) l1_f"
by (simp add: L2corres_L2_call_L1)
lemma L2corres_modify_global:
"⟦ ⋀s. P s ⟹ M (st s) = st (M' s) ⟧ ⟹
L2corres st ret ex P (L2_modify M) (L1_modify M')"
unfolding L2_defs L1_defs
by (auto simp add: L2corres_def corresXF_modify_global)
lemma L2corres_modify_unknown:
"⟦ ⋀s. P s ⟹ st s = st (M s) ⟧ ⟹
L2corres st ret ex P (L2_unknown ns) (L1_modify M)"
apply (clarsimp simp: L2corres_def L2_defs L1_defs)
apply (auto intro: corresXF_select_modify)
done
lemma L2corres_spec_unknown:
"⟦ ⋀s a. st s = st (M (a::('a ⇒ ('a::{type}))) s) ⟧ ⟹
L2corres st ret ex P (L2_unknown ns) (L1_init M)"
apply (auto simp add: L2corres_def corresXF_def L1_defs L2_defs
reaches_bind reaches_succeeds succeeds_bind)
done
lemma L2corres_modify_gets:
"⟦ ⋀s. P s ⟹ st s = st (M s); ⋀s. P s ⟹ ret (M s) = f (st s) ⟧ ⟹
L2corres st ret ex P (L2_gets (λs. f s) n) (L1_modify M)"
by (simp add: L2corres_def L2_defs L1_defs corresXF_modify_gets)
lemma L2corres_gets_skip:
"L2corres st ret ex P L2_skip L1_skip"
by (simp add: L2corres_def L2_defs L1_defs corresXF_def)
lemma L2corres_guard:
"⟦ ⋀s. P s ⟹ G' s = G (st s) ⟧ ⟹
L2corres st return_xf exception_xf P (L2_guard G) (L1_guard G')"
by (simp add: L2corres_def L2_defs L1_defs corresXF_guard)
lemma L2corres_fail:
"L2corres st return_xf exception_xf P L2_fail X"
by (clarsimp simp add: L2corres_def L1_defs L2_defs corresXF_def)
lemma L2corres_spec:
"⟦ ⋀s s'. ((s, s') ∈ A') = ((st s, st s') ∈ A); surj st ⟧
⟹ L2corres st return_xf exception_xf P (L2_spec A) (L1_spec A')"
apply (clarsimp simp: L2corres_def L2_defs L1_spec_def corresXF_def succeeds_bind reaches_bind)
by (metis surjD)
lemma L2corres_assume:
"⟦ ⋀s s'. (((), s') ∈ A' s) = (((), st s') ∈ A (st s)) ⟧
⟹ L2corres st return_xf exception_xf P (L2_assume A) (L1_assume A')"
by (clarsimp simp: L2corres_def L2_defs L1_assume_def corresXF_def)
lemma L2corres_seq:
"⟦ L2corres st return_xf exception_xf P A A';
⋀x. L2corres st return_xf' exception_xf (P' x) (B x) B';
⦃R⦄ A' ⦃λ_ s. P' (return_xf s) s⦄, ⦃λ_ _. True⦄;
⋀s. R s ⟹ P s ⟧ ⟹
L2corres st return_xf' exception_xf R (L2_seq A B) (L1_seq A' B')"
apply (unfold L2corres_def L2_seq_def L1_seq_def validE_def)
apply (rule corresXF_join)
apply assumption
apply assumption
apply simp
apply assumption
done
lemma L2corres_guard_imp:
"⟦ L2corres st ret_state ex_state Q M M'; pred_imp P Q ⟧ ⟹
L2corres st ret_state ex_state P M M'"
by (simp add: L2corres_def pred_imp_def corresXF_guard_imp)
lemma L2corres_guarded'':
assumes bdy: "⋀s' s. g' s' ⟹ s = st s' ⟹ P s' ⟹ L2corres st ret ex P (c (dest s)) (c' (dest' s'))"
assumes g_g': "⋀s'. P s' ⟹ g' s' = g (st s')"
assumes dest: "⋀s' s. g' s' ⟹ s = st s' ⟹ P s' ⟹ dest' s' = dest (st s')"
shows "L2corres st ret ex P (L2_guarded g (L2_seq (L2_gets dest []) c)) (L1_guarded g' (gets dest' ⤜ c'))"
using assms
by (auto simp add: L2corres_def L2_defs L1_defs L2_guarded_def L1_guarded_def corresXF_def
succeeds_bind reaches_bind split: xval_splits)
lemma L2corres_catch:
"⟦ L2corres st V E P L L';
⋀x. L2corres st V E' (P' x) (R x) R';
⦃Q⦄ L' ⦃λ_ _. True⦄, ⦃λ_ s. P' (E s) s⦄; ⋀s. Q s ⟹ P s ⟧ ⟹
L2corres st V E' Q (L2_catch L R) (L1_catch L' R')"
apply (clarsimp simp: L2corres_def L2_catch_def L1_catch_def validE_def)
apply (rule corresXF_except)
apply (assumption)
apply (assumption)
apply auto
done
lemma L2corres_throw:
"⟦ ⋀s. P s ⟹ E s = A ⟧ ⟹ L2corres st V E P (L2_throw A n) (L1_throw)"
by (clarsimp simp: L2corres_def L2_throw_def L1_throw_def corresXF_throw)
lemma L2corres_conseq:
assumes corres: "L2corres st return_xf exception_xf P C C'"
assumes conseq: "⋀s. Q s ⟹ P s"
shows "L2corres st return_xf exception_xf Q C C'"
apply (rule L2corres_guard_imp [OF corres])
using conseq by (simp add: pred_imp_def)
lemma L2corres_cond:
"⟦ L2corres st return_xf exception_xf P A A';
L2corres st return_xf exception_xf P' B B';
⋀s. R s ⟹ P s;
⋀s. R s ⟹ P' s;
⋀s. R s ⟹ c' s = c (st s) ⟧ ⟹
L2corres st return_xf exception_xf R (L2_condition c A B) (L1_condition c' A' B')"
apply (unfold L2corres_def L2_condition_def L1_condition_def)
apply (rule corresXF_cond)
apply (auto intro: corresXF_guard_imp)
done
lemma L2corres_inject_return:
"⟦ L2corres st V E P L R; ⦃P'⦄ R ⦃λ_ s. W (V s) = V' s⦄, ⦃ λ_ _. True ⦄; ⋀s. P' s ⟹ P s⟧ ⟹
L2corres st V' E P' (L2_seq L (λx. L2_gets (λ_. W x) n)) R"
apply (clarsimp simp: L2corres_def validE_def)
apply (drule corresXF_guard_imp [where P=P'], simp)
apply (unfold L2_seq_def L2_gets_def)
apply (rule corresXF_guard_imp)
apply (erule corresXF_append_gets_abs)
apply simp
apply simp
done
lemma L2corres_inject_return':
"⟦ L2corres st V E P L R;Gets = (λx. L2_gets (λ_. W x) n);⦃P'⦄ R ⦃λ_ s. W (V s) = V' s⦄, ⦃ λ_ _. True⦄; ⋀s. P' s ⟹ P s
⟧ ⟹
L2corres st V' E P' (L2_seq L Gets) R"
by (auto intro: L2corres_inject_return)
lemma L2corres_skip:
"L2corres st return_xf exception_xf P L2_skip L1_skip"
by (rule L2corres_gets_skip)
lemma L2corres_while:
assumes body_corres: "⋀x. L2corres st ret ex (P' x) (A x) B"
and inv_holds: "⦃λs. P (ret s) s ⦄ B ⦃λ_ s. P (ret s) s ⦄, ⦃λ_ _. True⦄"
and cond_match: "⋀s. P (ret s) s ⟹ c' s = c (ret s) (st s)"
and pred_imply: "⋀s x. P x s ⟹ P' x s"
and pred_extract: "⋀s. P x s ⟹ ret s = x"
and pred_imply2: "⋀s. Q x s ⟹ P x s"
shows "L2corres st ret ex (Q x) (L2_while c A x n) (L1_while c' B)"
apply (clarsimp simp: L2corres_def L2_while_def L1_while_def)
apply (rule corresXF_guard_imp)
apply (rule corresXF_while [
where P="λr s. P (ret s) s" and C'=c and C="λ_. c'" and A=A and B="λ_. B"
and ret="λr s. ret s" and ex="λr s. ex s" and st=st and y=x and x="()" and P'="λr s. Q x s"])
apply (rule corresXF_guard_imp)
apply (rule body_corres [unfolded L2corres_def])
apply (clarsimp simp: pred_imply)
apply (clarsimp simp: cond_match)
apply (rule inv_holds [unfolded validE_def, rule_format])
apply assumption
apply (metis pred_extract pred_imply2)
apply (metis pred_extract pred_imply2)
apply simp
done
lemma L2corres_returncall:
"⟦ L2corres st ret' ex' P' Z dest_fn;
⋀s. P s ⟹ P' (scope_setup s);
⋀t s. st (return_xf t (scope_teardown s t)) = st t;
⋀t s. st (result_exn (scope_teardown s t) t) = st t;
⋀s. st (scope_setup s) = st s;
⋀t s. st (scope_teardown s t) = st t;
⋀t s. P s ⟹ ret (return_xf t (scope_teardown s t)) = F (ret' t) (st t) ;
⋀t s. P s ⟹ (ex (result_exn (scope_teardown s t) t)) = emb (ex' t) ⟧ ⟹
L2corres st ret ex P (L2_returncall Z F emb ns)
(L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
unfolding L1_call_def L1_seq_def L1_throw_def L2_returncall_def L2_call_def L2corres_def L2_defs
apply (rule corresXF_I)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (smt (z3) Exn_def Result_neq_Exn map_exn_simps(2) the_Result_simp)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
subgoal
apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
done
done
lemma L2corres_dest_fn_simp:
assumes dest_fn: "⋀s. P s ⟹ dest_fn = dest_fn'"
assumes corres: "L2corres st ret ex P X
(L1_call scope_setup (measure_call dest_fn') scope_teardown result_exn return_xf)"
shows "L2corres st ret ex P X
(L1_call scope_setup (measure_call dest_fn) scope_teardown result_exn return_xf)"
using corres dest_fn unfolding L2corres_def corresXF_def
by blast
lemma L2corres_l2_propagate_fixed_cong:
"(⋀s. P s = P' s) ⟹ (⋀s. P' s ⟹ A = A') ⟹ L2corres st ret ex P A C = L2corres st ret ex P' A' C"
unfolding L2corres_def corresXF_def simp_implies_def
by (auto split: sum.splits prod.splits)
lemma L2corres_modifycall:
"⟦ L2corres st ret' ex' P' Z dest_fn;
⋀s. P s ⟹ P' (scope_setup s);
⋀s r. P r ⟹ F (ret' s) (st s) = st (return_xf s (scope_teardown r s));
⋀s. st (scope_setup s) = st s;
⋀t s. st (scope_teardown s t) = st t;
⋀t s. st (result_exn (scope_teardown s t) t) = st t;
⋀t s. P s ⟹ ex (result_exn (scope_teardown s t) t) = emb (ex' t)⟧ ⟹
L2corres st ret ex P (L2_modifycall Z F emb ns)
(L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
apply (clarsimp simp: L1_call_def L1_seq_def L1_throw_def L2_call_def L2_defs L2corres_def)
apply (rule corresXF_I)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (smt (z3) Exn_def Result_neq_Exn map_exn_simps(2) the_Result_simp)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
subgoal
apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
done
done
lemma L2corres_voidcall:
"⟦ L2corres st ret' ex' P' Z dest_fn;
⋀s. P s ⟹ P' (scope_setup s);
⋀s r. st (return_xf s (scope_teardown r s)) = st s;
⋀s. st (scope_setup s) = st s;
⋀t s. st (scope_teardown s t) = st t;
⋀t s. st (result_exn (scope_teardown s t) t) = st t;
⋀t s. P s ⟹ ex (result_exn (scope_teardown s t) t) = emb (ex' t)⟧ ⟹
L2corres st ret ex P (L2_voidcall Z emb ns)
(L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
apply (unfold L2_voidcall_def)
apply (rule subst[where t = "L2_skip" and s = "L2_modify (λs. s)"])
subgoal
apply (simp add: L2_defs)
apply (rule spec_monad_ext)
apply simp
done
apply (fold L2_modifycall_def L2corres_def)
apply (fastforce elim!: L2corres_modifycall)
done
lemma L2corres_call:
"⟦ L2corres st ret' ex' P' Z dest_fn;
⋀s. P s ⟹ P' (scope_setup s);
⋀s r. st (return_xf s (scope_teardown r s)) = st s;
⋀s r. ret (return_xf s (scope_teardown r s)) = ret' s;
⋀s. st (scope_setup s) = st s;
⋀t s. st (scope_teardown s t) = st t;
⋀t s. st (result_exn (scope_teardown s t) t) = st t;
⋀t s. P s ⟹ ex (result_exn (scope_teardown s t) t) = emb (ex' t) ⟧ ⟹
L2corres st ret ex P (L2_call Z emb ns)
(L1_call scope_setup dest_fn scope_teardown result_exn return_xf)"
apply (clarsimp simp: L2corres_def L2_call_def L1_call_def L1_seq_def L1_throw_def L2_defs)
apply (rule corresXF_I)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (smt (z3) Exn_def Result_neq_Exn map_exn_simps(2) the_Result_simp)
subgoal
apply (clarsimp simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
by (metis (mono_tags, opaque_lifting) Exception_eq_Exception Exn_def Exn_neq_Result map_exn_simps(1))
subgoal
apply (auto simp add: corresXF_def succeeds_bind succeeds_catch reaches_catch
reaches_map_value reaches_bind default_option_def Exn_def split: xval_splits exception_or_result_splits)
done
done
lemma (in L1_functions) L2corres_dyn_call:
"L2corres st ret ex P X
(L1_guarded g (gets dest >>= (λp. L1_call scope_setup (𝒫 p) scope_teardown result_exn return_xf))) ⟹
L2corres st ret ex P X (L1_dyn_call g scope_setup dest scope_teardown result_exn return_xf)"
by (simp add: L1_dyn_call_def)
lemma L2_gets_bind: "⟦ ⋀s s'. V s = V s' ⟧ ⟹ L2_seq (L2_gets V n) f = f (V undefined)"
unfolding L2_defs
apply (rule spec_monad_eqI)
apply (simp add: runs_to_iff)
by (auto simp add: runs_to_def_old) metis+
lemma L2corres_folded_gets:
"⟦ ⋀a. L2corres st ret ex (P and (λs. a = c (st s))) (X a) Y ⟧ ⟹
L2corres st ret ex P (L2_seq (L2_folded_gets c ns) X) Y"
by (fastforce simp add: L2_defs L2corres_def corresXF_def succeeds_bind reaches_bind split: xval_splits)
lemma L2_call_cong [fundef_cong, cong]:
"f = f' ⟹ L2_call f = L2_call f'"
by simp
lemma L2_call_liftE [simp]:
"L2_call (liftE x) emb ns ≡ liftE x"
by (clarsimp simp add: L2_call_def)
lemma L2_call_fail [simp]: "L2_call fail emb ns = fail"
apply (simp add: L2_call_def)
done
lemma L2_call_L2_gets [simp]: "L2_call (L2_gets x n) emb ns = L2_gets x n"
apply (simp add: L2_defs L2_call_def)
done
lemma L2_split_fixup_1:
"(L2_seq A (λx. case y of (a, b) ⇒ B a b x)) =
(case y of (a, b) ⇒ L2_seq A (λx. B a b x))"
by (auto simp: split_def)
lemma L2_split_fixup_2:
"(L2_seq (case y of (a, b) ⇒ B a b) A) =
(case y of (a, b) ⇒ L2_seq (B a b) A)"
by (auto simp: split_def)
lemma L2_split_fixup_3:
"(case (x, y) of (a, b) ⇒ P a b) = P x y"
by (auto simp: split_def)
lemma L2_split_fixup_4:
"case_prod (λa (b :: 'a × 'b). P a ) = case_prod (λa. case_prod (λ(x :: 'a) (y :: 'b). P a ))"
by (auto simp: split_def)
lemma L2_split_fixup_f:
"(f (case y of (a, b) ⇒ G a b) =
(case y of (a, b) ⇒ f (G a b)))"
by (auto simp: split_def)
lemma L2_split_fixup_g:
"case_prod (λa (b :: 'a × 'b). P a b) = case_prod (λa. case_prod (λ(x :: 'a) (y :: 'b). P a (x, y)))"
by (auto simp: split_def)
lemma liftE_fixup: "(λx. liftE (case x of (a, b) ⇒ f a b)) = (λ(a,b). liftE (f a b))"
by (simp add: fun_eq_iff split: prod.splits)
lemma finally_fixup: "(λx. finally (case x of (a, b) ⇒ f a b)) = (λ(a,b). finally (f a b))"
by (simp add: fun_eq_iff split: prod.splits)
lemma try_fixup: "(λx. try (case x of (a, b) ⇒ f a b)) = (λ(a,b). try (f a b))"
by (simp add: fun_eq_iff split: prod.splits)
lemmas L2_split_fixups =
L2_split_fixup_1
L2_split_fixup_2
L2_split_fixup_3
L2_split_fixup_4
liftE_fixup
finally_fixup
try_fixup
L2_split_fixup_f [where f=L2_guard]
L2_split_fixup_f [where f=L2_gets]
L2_split_fixup_f [where f=L2_modify]
L2_split_fixup_g [where P="λa b. L2_gets (P a b) n" for P n]
L2_split_fixup_g [where P="λa b. L2_guard (P a b)" for P]
L2_split_fixup_g [where P="λa b. L2_modify (P a b)" for P]
L2_split_fixup_g [where P="λa b. L2_spec (P a b)" for P]
L2_split_fixup_g [where P="λa b. L2_assume (P a b)" for P]
L2_split_fixup_g [where P="λa b. L2_throw (P a b) n" for P n]
L2_split_fixup_g [where P="λa b. L2_seq (L a b) (R a b)" for L R]
L2_split_fixup_g [where P="λa b. L2_while (C a b) (B a b) (I a b) n" for C B I n]
L2_split_fixup_g [where P="λa b. L2_unknown n" for n]
L2_split_fixup_g [where P="λa b. L2_catch (L a b) (R a b)" for L R]
L2_split_fixup_g [where P="λa b. L2_condition (C a b) (L a b) (R a b)" for C L R]
L2_split_fixup_g [where P="λa b. L2_call (M a b)" for M]
L2_split_fixup_g [where P="λa b. liftE (M a b)" for M]
L2_split_fixup_g [where P="λa b. finally (M a b)" for M]
L2_split_fixup_g [where P="λa b. try (M a b)" for M]
lemmas L2_split_fixups_congs =
prod.case_cong
named_theorems L2opt
lemma monotone_nondet_monad_L2_seq_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "⋀r. monotone R (≤) (λf. Y f r)"
shows "monotone R (≤)
(λf. (L2_seq (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_seq_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "⋀r. monotone R (≥) (λf. Y f r)"
shows "monotone R (≥)
(λf. (L2_seq (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_try_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
shows "monotone R (≤)
(λf. (L2_try (X f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
done
lemma monotone_nondet_monad_L2_try_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
shows "monotone R (≥)
(λf. (L2_try (X f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
done
lemma monotone_nondet_monad_L2_catch_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "⋀r. monotone R (≤) (λf. Y f r)"
shows "monotone R (≤)
(λf. (L2_catch (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_catch_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "⋀r. monotone R (≥) (λf. Y f r)"
shows "monotone R (≥)
(λf. (L2_catch (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_condition_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "monotone R (≤) Y"
shows "monotone R (≤)
(λf. (L2_condition C (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_condition_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "monotone R (≥) Y"
shows "monotone R (≥)
(λf. (L2_condition C (X f) (Y f)))"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_nondet_monad_L2_guarded_le [partial_function_mono]:
assumes mono_X[partial_function_mono]: "monotone R (≤) X"
shows "monotone R (≤)
(λf. L2_guarded C (X f))"
unfolding L2_guarded_def
apply (rule partial_function_mono)+
done
lemma monotone_nondet_monad_L2_guarded_ge [partial_function_mono]:
assumes mono_X[partial_function_mono]: "monotone R (≥) X"
shows "monotone R (≥)
(λf. L2_guarded C (X f))"
unfolding L2_guarded_def
apply (rule partial_function_mono)+
done
lemma monotone_nondet_monad_L2_while_le [partial_function_mono]:
assumes mono_B: "⋀r. monotone R (≤) (λf. B f r)"
shows "monotone R (≤) (λf. L2_while C (B f) I ns)"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_B)
done
lemma monotone_nondet_monad_L2_while_ge [partial_function_mono]:
assumes mono_B: "⋀r. monotone R (≥) (λf. B f r)"
shows "monotone R (≥) (λf. L2_while C (B f) I ns)"
unfolding L2_defs
apply (rule partial_function_mono)
apply (rule mono_B)
done
lemma monotone_nondet_monad_map_exn_le [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≤) X"
shows "monotone R (≤) (λf. map_value (map_exn emb) (X f))"
unfolding map_exn_def
apply (rule partial_function_mono)+
done
lemma monotone_nondet_monad_map_exn_ge [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≥) X"
shows "monotone R (≥) (λf. map_value (map_exn emb) (X f))"
unfolding map_exn_def
apply (rule partial_function_mono)+
done
lemma monotone_nondet_monad_L2_call_le [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≤) X"
shows "monotone R (≤)
(λf. L2_call (X f) emb ns)"
unfolding L2_call_def
apply (rule partial_function_mono)+
done
lemma monotone_nondet_monad_L2_call_ge [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≥) X"
shows "monotone R (≥)
(λf. L2_call (X f) emb ns)"
unfolding L2_call_def
apply (rule partial_function_mono)+
done
section ‹Some Relators›
lemma exists_sum_unit_eq: "(∃l'::unit. Inl x = Inl l' ∧ Inr y = Inr l') = (x=() ∧ y=())"
by auto
lemmas unit_convs = exists_sum_unit_eq
definition "rel_Nonlocal = (λe v. case e of Nonlocal x ⇒ v = x | _ ⇒ False)"
lemma rel_Nonlocal_conv: "(rel_Nonlocal e v) = (e = Nonlocal v)"
by (cases e) (auto simp add: rel_Nonlocal_def)
lemma fun_of_rel_rel_Nonlocal[fun_of_rel_intros]: "fun_of_rel rel_Nonlocal the_Nonlocal"
by (auto simp add: fun_of_rel_def rel_Nonlocal_def split: c_exntype.splits)
lemma funp_rel_Nonlocal[funp_intros, corres_admissible]: "funp rel_Nonlocal"
using fun_of_rel_rel_Nonlocal
by (auto simp add: funp_def)
lemma rel_sum_rel_Nonlocal_case_InlI: "e = Nonlocal v' ⟹ rel_sum rel_Nonlocal (=) (case e of Nonlocal v ⇒ Inl (Nonlocal v) | _ ⇒ Inr x) (Inl v')"
by (simp add: rel_Nonlocal_def)
lemma rel_xval_rel_Nonlocal_case_ExnI: "e = Nonlocal v' ⟹ rel_xval rel_Nonlocal (=) (case e of Nonlocal v ⇒ Exn (Nonlocal v) | _ ⇒ Result x) (Exn v')"
by (simp add: rel_Nonlocal_def)
lemma rel_sum_rel_Nonlocal_case_InrI: "is_local e ⟹ x = v' ⟹ rel_sum rel_Nonlocal (=) (case e of Nonlocal v ⇒ Inl (Nonlocal v) | _ ⇒ Inr x) (Inr v')"
apply (cases e)
apply (auto simp add: rel_Nonlocal_def)
done
lemma rel_xval_rel_Nonlocal_case_ResultI: "is_local e ⟹ x = v' ⟹ rel_xval rel_Nonlocal (=) (case e of Nonlocal v ⇒ Exn (Nonlocal v) | _ ⇒ Result x) (Result v')"
apply (cases e)
apply (auto simp add: rel_Nonlocal_def)
done
lemma rel_sum_rel_Nonlocal_map_sumI: "v = (map_sum (λx. x) f (case e of Nonlocal x ⇒ Inl x | _ ⇒ Inr x)) ⟹
rel_sum rel_Nonlocal (=) (map_sum Nonlocal f (case e of Nonlocal x ⇒ Inl x | _ ⇒ Inr x)) v"
apply simp
apply (cases e)
apply (auto simp add: rel_Nonlocal_def)
done
lemma rel_xval_rel_Nonlocal_map_xvalI: "v = (map_xval (λx. x) f (case e of Nonlocal x ⇒ Exn x | _ ⇒ Result x)) ⟹
rel_xval rel_Nonlocal (=) (map_xval Nonlocal f (case e of Nonlocal x ⇒ Exn x | _ ⇒ Result x)) v"
apply simp
apply (cases e)
apply (auto simp add: rel_Nonlocal_def)
done
definition "rel_Inr v v' ≡ (v = Inr v')"
lemma fun_of_rel_rel_Inr[fun_of_rel_intros]:
"fun_of_rel rel_Inr (λx. case x of Inr v ⇒ v | Inl _ ⇒ undefined)"
by (auto simp add: rel_Inr_def fun_of_rel_def)
lemma funp_rel_Inr[funp_intros, corres_admissible]: "funp rel_Inr"
using fun_of_rel_rel_Inr by (auto simp add: funp_def)
lemma rel_InrI: "v = Inr v' ⟹ rel_Inr v v'"
by (simp add: rel_Inr_def)
lemma rel_Inr_apply: "rel_Inr x y = (x = Inr y)"
by (simp add: rel_Inr_def )
lemma rel_Inr_trivial [simp]: "rel_Inr (Inr v) v"
by (simp add: rel_Inr_def)
definition rel_liftE:: "('e, 'a) xval ⇒ 'a val ⇒ bool" where "rel_liftE v v' ≡ (v = Result (the_Res v'))"
lemma fun_of_rel_rel_liftE[fun_of_rel_intros]:
"fun_of_rel rel_liftE (λx. case x of Result v ⇒ Result v | Exn _ ⇒ undefined)"
by (auto simp add: rel_liftE_def fun_of_rel_def)
lemma funp_rel_liftE[funp_intros, corres_admissible]: "funp rel_liftE"
using fun_of_rel_rel_liftE by (auto simp add: funp_def)
lemma rel_liftEI: "v = Result (the_Res v') ⟹ rel_liftE v v'"
by (simp add: rel_liftE_def)
lemma rel_liftE_apply: "rel_liftE x y = (x = Result (the_Res y))"
by (simp add: rel_liftE_def )
lemma rel_liftE_trivial [simp]: "rel_liftE (Result v) (Result v)"
by (simp add: rel_liftE_def)
lemma rel_liftE_rel_exception_or_result_conv: "rel_liftE = rel_exception_or_result (λNone ⇒ λ_. True | Some _ ⇒ λ_. False) (=)"
apply (rule ext)+
apply (auto simp add: rel_liftE_def rel_exception_or_result.simps)
done
lemma rel_liftE_Result_Result_iff[simp]: "rel_liftE (Result v) (Result v') ⟷ v = v'"
by (auto simp add: rel_liftE_def)
definition "rel_liftE' v v' ≡ (v = Inr v')"
lemma fun_of_rel_rel_liftE'[fun_of_rel_intros]:
"fun_of_rel rel_liftE' (λx. case x of Inr v ⇒ v | Inl _ ⇒ undefined)"
by (auto simp add: rel_liftE'_def fun_of_rel_def)
lemma funp_rel_liftE'[funp_intros, corres_admissible]: "funp rel_liftE'"
using fun_of_rel_rel_liftE' by (auto simp add: funp_def)
lemma rel_liftE'I: "v = Inr v' ⟹ rel_liftE' v v'"
by (simp add: rel_liftE'_def)
lemma rel_liftE'_apply: "rel_liftE' x y = (x = Inr y)"
by (simp add: rel_liftE'_def )
lemma rel_liftE'_trivial [simp]: "rel_liftE' (Inr v) v"
by (simp add: rel_liftE'_def)
lemma rel_liftE'_Inr_iff[simp]: "rel_liftE' (Inr v) v' ⟷ v = v'"
by (auto simp add: rel_liftE'_def)
lemma rel_liftE'_rel_liftE_conv: "rel_liftE' = rel_map to_xval OO rel_liftE OO rel_map the_Res"
apply (rule ext)+
apply (auto simp add: relcompp.simps rel_map_def rel_liftE_def rel_liftE'_def)
done
lemma rel_liftE_rel_liftE'_conv: "rel_liftE = rel_map from_xval OO rel_liftE' OO rel_map Result"
apply (rule ext)+
apply (auto simp add: relcompp.simps rel_map_def rel_liftE_def rel_liftE'_def)
done
lemma rel_liftE'_Inr: "rel_liftE' (Inr x) x"
by (simp)
definition rel_throwE' :: "('a ⇒ 'b ⇒ bool) ⇒ 'a + 'c ⇒ 'b ⇒ bool" where
"rel_throwE' L a c ⟷ (case a of Inl a' ⇒ L a' c | Inr _ ⇒ False)"
lemma rel_throwE'_iff: "rel_throwE' L a c ⟷ (∃l. a = Inl l ∧ L l c)"
by (auto simp add: rel_throwE'_def split: sum.splits)
lemma rel_throwE'_Inl:
"L x y ⟹ rel_throwE' L (Inl x) y"
unfolding rel_throwE'_def
by auto
lemma rel_throwE'_Inl_iff[simp]:
"rel_throwE' L (Inl x) y ⟷ L x y"
unfolding rel_throwE'_def
by auto
lemma not_rel_throwE'_Inr[simp]: "¬rel_throwE' R (Inr d) a"
by (auto simp: rel_throwE'_def)
definition rel_throwE :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'c) xval ⇒ 'b ⇒ bool" where
"rel_throwE L a c ⟷ (case a of Exn a' ⇒ L a' c | Result _ ⇒ False)"
lemma rel_throwE_iff: "rel_throwE L a c ⟷ (∃e. a = Exn e ∧ L e c)"
by (auto simp add: rel_throwE_def split: xval_splits)
lemma rel_throwE_Exn:
"L x y ⟹ rel_throwE L (Exn x) y"
unfolding rel_throwE_def
by auto
lemma rel_throwE_Exn_iff[simp]:
"rel_throwE L (Exn x) y ⟷ L x y"
unfolding rel_throwE_def
by auto
lemma not_rel_throwE_Result[simp]: "¬rel_throwE R (Result d) a"
by (auto simp: rel_throwE_def)
lemma case_right_eq: "(case v of Inl l ⇒ False | Inr r ⇒ P r) = (∃r. P r ∧ v = Inr r)"
by (auto split: sum.splits)
lemma case_left_eq: "(case v of Inr r ⇒ False | Inl l ⇒ P l) = (∃l. P l ∧ v = Inl l)"
by (auto split: sum.splits)
lemma rel_sum_right: "rel_sum L R (Inr r) v = (∃r'. v = Inr r' ∧ R r r')"
by (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)
lemma rel_sum_left: "rel_sum L R (Inl l) v = (∃l'. v = Inl l' ∧ L l l')"
by (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)
lemma rel_sum_eq_apply: "(rel_sum (=) (=) x y) = (x = y)"
by (cases x) (auto elim: rel_sum.cases intro: rel_sum.intros split: sum.splits)
lemma gen_unit_eq: "x = (y::unit)"
by simp
lemma liftE_L2_while: "L2_while c (λr. liftE (B r)) i n = liftE (whileLoop c B i)"
by (clarsimp simp: L2_while_def liftE_whileLoop)
lemma liftE_L2_while_VARS: "L2_while c (λr. liftE (B r)) i n = liftE (L2_VARS (whileLoop c B i) n)"
by (simp add: liftE_L2_while L2_VARS_def)
lemma rel_XF_True_def: "(rel_XF st ret_xf ex_xf (λ_ _. True)) =
(λ(v, t) (r, s). s = st t ∧
(case v of Exn x ⇒ r = Exn (ex_xf x t) | Result x ⇒ r = Result (ret_xf x t)))"
apply (rule ext)+
apply (auto simp add: rel_XF_def rel_xval.simps split: xval_splits)
done
lemma refines_corresXF: "(∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
(case v of Exn x ⇒ r = Exn (ex_xf x t) | Result x ⇒ r = Result (ret_xf x t))))
⟹ corresXF st ret_xf ex_xf P A C"
by (simp add: corresXF_refines_iff rel_XF_True_def)
lemma corresXF_refines: "corresXF st ret_xf ex_xf P A C ⟹
(∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
(case v of Exn x ⇒ r = Exn (ex_xf x t) | Result x ⇒ r = Result (ret_xf x t))))"
by (simp add: corresXF_refines_iff rel_XF_True_def)
theorem corresXF_refines_conv:
‹corresXF st ret_xf ex_xf P A C ⟷
(∀t. P t ⟶ refines C A t (st t) (λ(v, t) (r, s). s = st t ∧
(case v of Exn x ⇒ r = Exn (ex_xf x t) | Result x ⇒ r = Result (ret_xf x t))))›
using corresXF_refines refines_corresXF ..
lemma sim_nondet_to_corresXF: "(⋀s. refines f f' s s (=)) ⟹
corresXF (λs. s) (λr _. r) (λr _ . r) (λ_. True) f' f"
unfolding refines_def_old corresXF_def
apply (auto split: xval_splits)
done
named_theorems rel_spec_monad_rewrite_simps
locale sim_stack_heap_state =
abstract: stack_heap_state htd⇩a htd_upd⇩a hmem⇩a hmem_upd⇩a 𝒮 +
concrete: stack_heap_state htd⇩c htd_upd⇩c hmem⇩c hmem_upd⇩c 𝒮
for
htd⇩a:: "'s⇩a ⇒ heap_typ_desc" and
htd_upd⇩a:: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 's⇩a ⇒ 's⇩a" and
hmem⇩a:: "'s⇩a ⇒ heap_mem" and
hmem_upd⇩a:: "(heap_mem ⇒ heap_mem) ⇒ 's⇩a ⇒ 's⇩a" and
htd⇩c:: "'s⇩c ⇒ heap_typ_desc" and
htd_upd⇩c:: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 's⇩c ⇒ 's⇩c" and
hmem⇩c:: "'s⇩c ⇒ heap_mem" and
hmem_upd⇩c:: "(heap_mem ⇒ heap_mem) ⇒ 's⇩c ⇒ 's⇩c" and
𝒮::"addr set"
begin
definition rel_stack_free where
"rel_stack_free s⇩c s⇩a ≡ stack_free (htd⇩c s⇩c) ⊆ stack_free (htd⇩a s⇩a)"
lemma refines_rel_stack_free_with_fresh_stack_ptr:
assumes s: "rel_stack_free s⇩c s⇩a"
assumes init_eq: "⋀s⇩c s⇩a. I⇩c s⇩c = I⇩a s⇩a"
assumes f: "⋀s⇩c s⇩a p. rel_stack_free s⇩c s⇩a ⟹
refines (f⇩c p) (f⇩a p) s⇩c s⇩a
(rel_prod (rel_xval L R) rel_stack_free)"
shows "refines
(concrete.with_fresh_stack_ptr n I⇩c f⇩c)
(abstract.with_fresh_stack_ptr n I⇩a f⇩a) s⇩c s⇩a
(rel_prod (rel_xval L R) rel_stack_free)"
apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
apply (rule refines_bind_bind_exn [where Q="(rel_prod (rel_xval (λ_ _. False) (=)) rel_stack_free)"])
apply simp_all
subgoal
apply (clarsimp simp add: refines_def_old rel_xval.simps)
using s init_eq
apply (simp add: rel_stack_free_def)
subgoal for p d vs bs
apply (frule (1) stack_allocs_stack_free_mono)
apply clarsimp
subgoal for d'
apply (rule exI[where x="hmem_upd⇩a (fold (λi. heap_update_padding (p +⇩p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) (htd_upd⇩a (λ_. d') s⇩a)"])
apply clarsimp
apply (rule conjI)
apply (rule exI[where x="d'"])
apply clarsimp
apply (rule exI[where x="vs"])
apply clarsimp
apply blast
using stack_free_stack_allocs
apply blast
done
done
done
apply (rule refines_rel_prod_on_exit [where S' = rel_stack_free])
apply (rule f)
apply assumption
apply (simp add: rel_stack_free_def)
apply (metis abstract.htd_hmem_upd abstract.typing.get_upd concrete.htd_hmem_upd
concrete.typing.get_upd stack_free_stack_releases_mono')
subgoal using stack_free_stack_releases_mono' by blast
done
definition rel_stack_free_eq where
"rel_stack_free_eq s⇩c s⇩a ≡ stack_free (htd⇩c s⇩c) = stack_free (htd⇩a s⇩a)"
lemma refines_rel_stack_free_eq_with_fresh_stack_ptr:
assumes s: "rel_stack_free_eq s⇩c s⇩a"
assumes init_eq: "⋀s⇩c s⇩a. I⇩c s⇩c = I⇩a s⇩a"
assumes f: "⋀s⇩c s⇩a p. rel_stack_free_eq s⇩c s⇩a ⟹
refines (f⇩c p) (f⇩a p) s⇩c s⇩a
(rel_prod (rel_xval L R) rel_stack_free_eq)"
shows "refines
(concrete.with_fresh_stack_ptr n I⇩c f⇩c)
(abstract.with_fresh_stack_ptr n I⇩a f⇩a) s⇩c s⇩a
(rel_prod (rel_xval L R) rel_stack_free_eq)"
apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
apply (rule refines_bind_bind_exn [where Q="(rel_prod (rel_xval (λ_ _. False) (=)) rel_stack_free_eq)"])
apply simp_all
subgoal
apply (clarsimp simp add: refines_def_old rel_xval.simps)
using s init_eq
apply (simp add: rel_stack_free_eq_def)
subgoal for p d vs bs
apply (frule (1) stack_allocs_stack_free_eq)
apply clarsimp
subgoal for d'
apply (rule exI[where x="hmem_upd⇩a (fold (λi. heap_update_padding (p +⇩p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) (htd_upd⇩a (λ_. d') s⇩a)"])
apply clarsimp
apply (rule conjI)
apply (rule exI[where x="d'"])
apply clarsimp
apply (rule exI[where x="vs"])
apply clarsimp
apply blast
using stack_free_stack_allocs
apply blast
done
done
done
apply (rule refines_rel_prod_on_exit [where S' = rel_stack_free_eq])
apply (rule f)
apply assumption
apply clarsimp
subgoal for v t t' s⇩c s⇩a bs
apply (rule exI[where x=" hmem_upd⇩a (heap_update_list (ptr_val v) bs) (htd_upd⇩a (stack_releases n v) s⇩a)"])
apply (clarsimp simp add: rel_stack_free_eq_def)
by (metis dual_order.eq_iff stack_free_stack_releases_mono')
subgoal by blast
done
end
locale sim_stack_heap_raw_state =
abstract: stack_heap_raw_state hrs⇩a hrs_upd⇩a 𝒮 +
concrete: stack_heap_raw_state hrs⇩c hrs_upd⇩c 𝒮
for
hrs⇩a:: "'s⇩a ⇒ heap_raw_state" and
hrs_upd⇩a:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's⇩a ⇒ 's⇩a" and
hrs⇩c:: "'s⇩c ⇒ heap_raw_state" and
hrs_upd⇩c:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's⇩c ⇒ 's⇩c" and
𝒮::"addr set"
begin
sublocale sim_stack_heap_state
"λs. hrs_htd (hrs⇩a s)" "λupd. hrs_upd⇩a (hrs_htd_update upd)"
"λs. hrs_mem (hrs⇩a s)" "λupd. hrs_upd⇩a (hrs_mem_update upd)"
"λs. hrs_htd (hrs⇩c s)" "λupd. hrs_upd⇩c (hrs_htd_update upd)"
"λs. hrs_mem (hrs⇩c s)" "λupd. hrs_upd⇩c (hrs_mem_update upd)"
𝒮
by unfold_locales
end
named_theorems L2corres_with_fresh_stack_ptr
locale L2 = sim_stack_heap_state htd⇩a htd_upd⇩a hmem⇩a hmem_upd⇩a htd⇩c htd_upd⇩c hmem⇩c hmem_upd⇩c 𝒮
for
htd⇩a:: "'s⇩a ⇒ heap_typ_desc" and
htd_upd⇩a:: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 's⇩a ⇒ 's⇩a" and
hmem⇩a:: "'s⇩a ⇒ heap_mem" and
hmem_upd⇩a:: "(heap_mem ⇒ heap_mem) ⇒ 's⇩a ⇒ 's⇩a" and
htd⇩c:: "'s⇩c ⇒ heap_typ_desc" and
htd_upd⇩c:: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 's⇩c ⇒ 's⇩c" and
hmem⇩c:: "'s⇩c ⇒ heap_mem" and
hmem_upd⇩c:: "(heap_mem ⇒ heap_mem) ⇒ 's⇩c ⇒ 's⇩c" and
𝒮::"addr set" +
fixes st:: "'s⇩c ⇒ 's⇩a"
assumes htd_st: "⋀s. htd⇩a (st s) = htd⇩c s"
assumes htd_upd_st: "⋀s f. (htd_upd⇩a f (st s)) = st (htd_upd⇩c f s)"
assumes hmem_upd_st: "⋀s f. (hmem_upd⇩a f (st s)) = st (hmem_upd⇩c f s)"
begin
lemma rel_stack_free_eq_st: "rel_stack_free_eq s (st s)"
by (simp add: rel_stack_free_eq_def htd_st)
definition rel_L2 where
"rel_L2 ex_xf ret_xf ≡ (λ (r⇩c, s⇩c) (r⇩a, s⇩a).
rel_xval (λ_ a. a = ex_xf s⇩c) (λ_ a. a = ret_xf s⇩c) r⇩c r⇩a ∧
(s⇩a = st s⇩c))"
lemma rel_L2_def':
"(rel_L2 ex_xf ret_xf) = (λ(v, t) (r, s).
s = st t ∧ (case v of Exn x ⇒ r = Exn (ex_xf t) | Result x ⇒ r = Result (ret_xf t)))"
apply (clarsimp simp add: rel_L2_def fun_eq_iff, intro iffI)
subgoal using rel_xval.cases by fastforce
subgoal by(auto split: xval_splits)
done
lemma refines_rel_L2_on_exit':
assumes f: "refines (f⇩c p) (f⇩a p) s⇩c (st s⇩c) (rel_L2 ex_xf ret_xf)"
assumes ex_xf_htd_indep: "⋀f s. ex_xf (htd_upd⇩c f s) = ex_xf s"
assumes ret_xf_htd_indep: "⋀f s. ret_xf (htd_upd⇩c f s) = ret_xf s"
shows "refines
(on_exit (f⇩c p) {(s,t). t = htd_upd⇩c (release p) s})
(on_exit (f⇩a p) {(s,t). t = htd_upd⇩a (release p) s}) s⇩c (st s⇩c)
(rel_L2 ex_xf ret_xf)"
unfolding on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result)
apply (rule refines_mono [OF _ f])
apply (clarsimp)
subgoal for r s q t
apply (rule refines_bind_bind_exn[where
Q="(λ(r', s) (q', t). is_Result r' ∧ is_Result q' ∧ rel_L2 ex_xf ret_xf (r, s) (q, t))"])
subgoal
apply (rule refines_assert_result_and_state)
apply (clarsimp simp add: rel_L2_def, intro conjI)
subgoal
using ex_xf_htd_indep ret_xf_htd_indep
by metis
subgoal
using htd_upd_st by force
by auto
apply (auto simp: is_Result_def)
done
done
lemma refines_rel_L2_on_exit:
assumes f: "refines (f⇩c p) (f⇩a p) s⇩c (st s⇩c) (rel_L2 ex_xf ret_xf)"
assumes ex_xf_htd_indep: "⋀g f s. ex_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ex_xf s"
assumes ret_xf_htd_indep: "⋀g f s. ret_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ret_xf s"
assumes nonempty_cleanup⇩a: "cleanup⇩a ≠ {}"
assumes cleanup_htd: "⋀s s'. (s, s') ∈ cleanup⇩c ⟹ ∃g f. s' = (hmem_upd⇩c g (htd_upd⇩c f s))"
assumes stuck_sim: "⋀s. ∄s'. (s, s') ∈ cleanup⇩c ⟹ ∄t'. (st s, t') ∈ cleanup⇩a"
assumes cleanup_sim: "⋀s t. (s, t) ∈ cleanup⇩c ⟹ (st s, st t) ∈ cleanup⇩a"
shows "refines
(on_exit (f⇩c p) cleanup⇩c)
(on_exit (f⇩a p) cleanup⇩a) s⇩c (st s⇩c)
(rel_L2 ex_xf ret_xf)"
unfolding on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result)
apply (rule refines_mono [OF _ f])
apply (clarsimp)
subgoal for r s q t
apply (rule refines_bind_bind_exn [where
Q="λ(r', s) (q', t). is_Result r' ∧ is_Result q' ∧ rel_L2 ex_xf ret_xf (r, s) (q, t)"])
subgoal
apply (rule refines_state_select)
apply (clarsimp simp add: rel_L2_def, intro conjI)
subgoal
using cleanup_htd cleanup_sim
by blast
subgoal
using ex_xf_htd_indep ret_xf_htd_indep cleanup_htd
by metis
subgoal
using stuck_sim by (auto simp: rel_L2_def)
done
apply (auto simp: is_Result_def)
done
done
lemma refines_rel_L2_with_fresh_stack_ptr:
assumes init_eq: "I⇩c s⇩c = I⇩a (st s⇩c)"
assumes ex_xf_htd_indep: "⋀g f s. ex_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ex_xf s"
assumes ret_xf_htd_indep: "⋀g f s. ret_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ret_xf s"
assumes f: "⋀(p::'a::mem_type ptr) d vs bs. (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (htd⇩c s⇩c) ⟹ vs ∈ I⇩c s⇩c ⟹ length vs = n ⟹
length bs = n * size_of TYPE('a) ⟹
refines
(f⇩c p)
(f⇩a p)
(hmem_upd⇩c (fold (λi. heap_update_padding (p +⇩p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd⇩c (λ_. d)) s⇩c))
(st (hmem_upd⇩c (fold (λi. heap_update_padding (p +⇩p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd⇩c (λ_. d)) s⇩c)))
(rel_L2 ex_xf ret_xf)"
shows "refines
(concrete.with_fresh_stack_ptr n I⇩c f⇩c)
(abstract.with_fresh_stack_ptr n I⇩a f⇩a) s⇩c (st s⇩c)
(rel_L2 ex_xf ret_xf)"
apply (simp add: concrete.with_fresh_stack_ptr_def abstract.with_fresh_stack_ptr_def)
apply (rule refines_bind_bind_exn [where Q="(λ(r⇩c, t⇩c) (r⇩a, t⇩a).
(∃d p vs bs. (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (htd⇩c s⇩c) ∧ r⇩c = Result p ∧ r⇩a = Result p ∧ vs ∈ I⇩c s⇩c ∧ length vs = n ∧
length bs = n * size_of TYPE('a) ∧
t⇩c = hmem_upd⇩c (fold (λi. heap_update_padding (p +⇩p int i) (vs ! i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<length vs]) ((htd_upd⇩c (λ_. d)) s⇩c) ∧
t⇩a = st t⇩c))"])
apply simp_all
subgoal
apply (clarsimp simp add: refines_def_old rel_xval.simps)
by (metis (full_types) hmem_upd_st htd_st htd_upd_st init_eq )
subgoal for p
apply clarsimp
apply (rule refines_rel_L2_on_exit )
apply (rule f)
apply simp
apply simp
apply simp
apply simp
apply (rule ex_xf_htd_indep)
apply (rule ret_xf_htd_indep)
apply blast
subgoal by auto
subgoal by auto
subgoal using htd_upd_st hmem_upd_st by auto
done
done
lemma L2corres_refines_rel_L2_conv:
‹L2corres st ret_xf ex_xf P A C ⟷
(∀t. P t ⟶ refines C A t (st t) (rel_L2 ex_xf ret_xf))›
by (simp add: L2corres_def corresXF_refines_conv rel_L2_def')
lemma L2corres_refines_rel_L2:
assumes L2: "L2corres st ret_xf ex_xf P A C"
assumes P: "P s⇩c"
shows ‹refines C A s⇩c (st s⇩c) (rel_L2 ex_xf ret_xf)›
using L2 P by (simp add: L2corres_refines_rel_L2_conv)
lemma L2corres_with_fresh_stack_ptr[L2corres_with_fresh_stack_ptr]:
assumes l2: "⋀p. L2corres st ret_xf ex_xf P (l2 p) (l1 p)"
assumes I: "⋀s. R s ⟹ I_l1 s = I_l2 (st s)"
assumes P: "⋀s. R s ⟹ P s"
assumes ex_xf_htd_indep: "⋀g f s. ex_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ex_xf s"
assumes ret_xf_htd_indep: "⋀g f s. ret_xf (hmem_upd⇩c g (htd_upd⇩c f s)) = ret_xf s"
assumes P_indep: "⋀f g s. P (hmem_upd⇩c g (htd_upd⇩c f s)) = P s"
shows "L2corres st ret_xf ex_xf R
(abstract.with_fresh_stack_ptr n (I_l2) (L2_VARS l2 nm))
(concrete.with_fresh_stack_ptr n I_l1 l1)"
apply (clarsimp simp add: L2_VARS_def L2corres_refines_rel_L2_conv)
apply (rule refines_rel_L2_with_fresh_stack_ptr)
apply (rule I, assumption)
apply (rule ex_xf_htd_indep)
apply (rule ret_xf_htd_indep)
apply (rule L2corres_refines_rel_L2)
apply (rule l2)
apply (simp add: P_indep P)
done
end
hide_const (open) L2
lemma refines_rel_prod_guard_on_exit:
assumes f: "refines f⇩c f⇩a s⇩c s⇩a (rel_prod R S')"
assumes cleanup: "⋀s⇩c s⇩a t⇩c. S' s⇩c s⇩a ⟹ grd s⇩a ⟹ (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ ∃t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a ∧ S t⇩c t⇩a"
assumes emp: "⋀s⇩c s⇩a. S' s⇩c s⇩a ⟹ ∄t⇩c. (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ ∄t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a"
shows "refines (on_exit f⇩c cleanup⇩c) (guard_on_exit f⇩a grd cleanup⇩a) s⇩c s⇩a (rel_prod R S)"
unfolding on_exit_def on_exit'_def
apply (rule refines_bind_exception_or_result[OF refines_weaken, OF f])
apply (simp add: bind_assoc)
apply (rule refines_bind_guard_right)
apply (rule refines_bind'[OF refines_state_select])
subgoal using cleanup by auto
subgoal using emp by auto
done
lemma refines_bind_no_throw_strong:
assumes "no_throw (λ_. True) f"
assumes "no_throw (λ_. True) f'"
assumes f: "refines f f' s s' Q"
assumes g: "⋀r t r' t'. reaches f s (Result r) t ⟹ reaches f' s' (Result r') t' ⟹
Q (Result r, t) (Result r', t') ⟹ refines (g r) (g' r') t t' R"
shows "refines (f >>= g) (f' >>= g') s s' R"
apply (rule refines_bind_bind_strong' [OF f])
subgoal using assms
apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
subgoal using assms
apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
subgoal using assms
apply (clarsimp simp add: no_throw_def runs_to_partial_def_old)
by (metis the_Exception_simp the_Exception_Result reaches_succeeds)
subgoal using g
by auto
done
lemma refines_bind_no_throw:
assumes "no_throw (λ_. True) f"
assumes "no_throw (λ_. True) f'"
assumes f: "refines f f' s s' Q"
assumes g: "⋀r t r' t'.
Q (Result r, t) (Result r', t') ⟹ refines (g r) (g' r') t t' R"
shows "refines (f >>= g) (f' >>= g') s s' R"
using assms
by (rule refines_bind_no_throw_strong)
lemma no_throw_guard[simp]: "no_throw P (guard G)"
by (auto simp add: no_throw_def runs_to_partial_def_old)
lemma no_throw_assert_result_and_state[simp]: "no_throw P (assert_result_and_state f)"
by (auto simp add: no_throw_def runs_to_partial_def_old)
lemma no_throw_assume_result_and_state[simp]: "no_throw P (assume_result_and_state f)"
by (auto simp add: no_throw_def runs_to_partial_def_old)
lemma refines_guard_same: "refines (guard P) (guard P) s s (λ(r, t) (r', t'). t=s ∧ t'=s)"
by (simp add: refines_def_old)
lemma refines_state_select_same:
"refines (state_select R) (state_select R) s s (λ(r, t) (r', t'). t' = t ∧ (s, t) ∈ R)"
by (simp add: refines_def_old)
lemma refines_assert_result_and_state_same:
"refines (assert_result_and_state R) (assert_result_and_state R) s s
(λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
by (auto simp add: refines_def_old)
lemma refines_assume_result_and_state_same:
"refines (assume_result_and_state R) (assume_result_and_state R) s s
(λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
by (auto simp add: refines_def_old)
lemma refines_assume_result_and_state_same':
assumes "R s = R' s"
shows "refines (assume_result_and_state R) (assume_result_and_state R') s s
(λ(r, t) (r', t'). ∃v. (v, t) ∈ R s ∧ r = Result v ∧ r' = Result v ∧ t = t')"
using assms
by (auto simp add: refines_def_old)
lemma refines_rel_xval_guard_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod (rel_xval L R) (=))"
shows "refines
(guard_on_exit f⇩c P cleanup)
(guard_on_exit f⇩a P cleanup) s s
(rel_prod (rel_xval L R) (=))"
unfolding guard_on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result')
apply (rule f)
apply clarsimp
apply (rule refines_bind_no_throw_strong [OF _ _ refines_guard_same])
apply simp
apply simp
apply clarsimp
apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
apply simp
apply simp
apply clarsimp
done
lemma refines_rel_xval_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod (rel_xval L R) (=))"
shows "refines
(on_exit f⇩c cleanup)
(on_exit f⇩a cleanup) s s
(rel_prod (rel_xval L R) (=))"
unfolding on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result')
apply (rule f)
apply clarsimp
apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
apply simp
apply simp
apply clarsimp
done
lemma refines_rel_xval_assume_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod (rel_xval L R) (=))"
shows "refines
(assume_on_exit f⇩c P cleanup)
(assume_on_exit f⇩a P cleanup) s s
(rel_prod (rel_xval L R) (=))"
unfolding assume_on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result')
apply (rule f)
apply (rule refines_bind_no_throw_strong [OF _ _ ])
apply simp
apply simp
apply clarsimp
apply (rule refines_assume_result_and_state_same)
apply clarsimp
apply (rule refines_bind_no_throw_strong [OF _ _ refines_state_select_same])
apply simp
apply simp
apply clarsimp
done
lemma refines_state_assume_pred:
assumes P: "P t"
assumes ref: "refines f g s t R"
shows "refines f (do {assume_result_and_state (λs. {(x, y). (λ() s'. s' = s ∧ P s) x y}); g }) s t R"
using P ref
by (auto simp add: refines_def_old succeeds_bind reaches_bind)
lemma refines_rel_prod_assume_on_exit:
assumes f: "refines f⇩c f⇩a s⇩c s⇩a (rel_prod R S')"
assumes cleanup: "⋀s⇩c s⇩a t⇩c. S' s⇩c s⇩a ⟹ (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ ∃t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a ∧ S t⇩c t⇩a"
assumes emp: "⋀s⇩c s⇩a. S' s⇩c s⇩a ⟹ ∄t⇩c. (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ ∄t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a"
assumes conseq: "⋀s⇩c s⇩a. S' s⇩c s⇩a ⟹ P s⇩a"
shows "refines (on_exit f⇩c cleanup⇩c) (assume_on_exit f⇩a P cleanup⇩a) s⇩c s⇩a (rel_prod R S)"
unfolding assume_on_exit_bind_exception_or_result_conv on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result')
apply (rule f)
apply (rule refines_state_assume_pred )
subgoal using conseq by auto
subgoal
apply (rule refines_bind_no_throw_strong [where Q = "rel_prod (λ_ _. True) S"])
apply simp
apply simp
apply (rule refines_state_select)
subgoal using cleanup by auto
subgoal using emp by auto
subgoal
apply (rule refines_yield)
apply auto
done
done
done
lemma refines_runs_to_partial_rel_prod_assume_on_exit:
assumes f: "refines f⇩c f⇩a s⇩c s⇩a (rel_prod R S')"
assumes runs_to: "f⇩c ∙ s⇩c ?⦃λr t. P t⦄"
assumes cleanup: "⋀s⇩c s⇩a t⇩c. S' s⇩c s⇩a ⟹ (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ P s⇩c ⟹ ∃t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a ∧ S t⇩c t⇩a"
assumes emp: "⋀s⇩c s⇩a. S' s⇩c s⇩a ⟹ P s⇩c ⟹ ∄t⇩c. (s⇩c, t⇩c) ∈ cleanup⇩c ⟹ ∄t⇩a. (s⇩a, t⇩a) ∈ cleanup⇩a"
assumes conseq: "⋀s⇩c s⇩a. S' s⇩c s⇩a ⟹ P s⇩c ⟹ P' s⇩a"
shows "refines (on_exit f⇩c cleanup⇩c) (assume_on_exit f⇩a P' cleanup⇩a) s⇩c s⇩a (rel_prod R S)"
proof -
from refines_runs_to_partial_fuse [OF f runs_to]
have "refines f⇩c f⇩a s⇩c s⇩a (λ(r, t) (r', t'). rel_prod R S' (r, t) (r', t') ∧ P t)" .
moreover have "(λ(r, t) (r', t'). rel_prod R S' (r, t) (r', t') ∧ P t) = rel_prod R (λt t'. S' t t' ∧ P t)"
by (auto simp add: rel_prod_conv)
ultimately have "refines f⇩c f⇩a s⇩c s⇩a (rel_prod R (λt t'. S' t t' ∧ P t))" by simp
then show ?thesis
apply (rule refines_rel_prod_assume_on_exit)
subgoal using cleanup by blast
subgoal using emp by blast
subgoal using conseq by auto
done
qed
locale L2_heap_raw_state = sim_stack_heap_raw_state hrs⇩a hrs_upd⇩a hrs⇩c hrs_upd⇩c 𝒮
for
hrs⇩a:: "'s⇩a ⇒ heap_raw_state" and
hrs_upd⇩a:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's⇩a ⇒ 's⇩a" and
hrs⇩c:: "'s⇩c ⇒ heap_raw_state" and
hrs_upd⇩c:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's⇩c ⇒ 's⇩c" and
𝒮::"addr set" +
fixes st:: "'s⇩c ⇒ 's⇩a"
assumes hrs_htd_st: "⋀s. hrs_htd (hrs⇩a (st s)) = hrs_htd (hrs⇩c s)"
assumes hrs_upd_st: "⋀s f. (hrs_upd⇩a f (st s)) = st (hrs_upd⇩c f s)"
begin
sublocale L2
"λs. hrs_htd (hrs⇩a s)" "λupd. hrs_upd⇩a (hrs_htd_update upd)"
"λs. hrs_mem (hrs⇩a s)" "λupd. hrs_upd⇩a (hrs_mem_update upd)"
"λs. hrs_htd (hrs⇩c s)" "λupd. hrs_upd⇩c (hrs_htd_update upd)"
"λs. hrs_mem (hrs⇩c s)" "λupd. hrs_upd⇩c (hrs_mem_update upd)"
𝒮
apply (unfold_locales)
subgoal using hrs_htd_st by simp
subgoal using hrs_upd_st by simp
subgoal using hrs_upd_st by simp
done
end
locale typ_heap_typing = pointer_lense r w + heap_typing_state heap_typing heap_typing_upd
for
r:: "'t ⇒ ('a::xmem_type) ptr ⇒ 'a" and
w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
heap_typing :: "'t ⇒ heap_typ_desc" and
heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" and
𝒮:: "addr set"
begin
definition stack_ptr_acquire :: "nat ⇒ 'a list ⇒ 'a ptr ⇒ heap_typ_desc ⇒ 't ⇒ 't"
where "stack_ptr_acquire n vs p d s =
(fold (λi. w (p +⇩p int i) (λ_. (vs ! i))) [0..<n]) (heap_typing_upd (λ_. d) s)"
definition stack_ptr_release :: "nat ⇒ 'a ptr ⇒ 't ⇒ 't"
where "stack_ptr_release n p s =
(heap_typing_upd (stack_releases n p) o (fold (λi. w (p +⇩p int i) (λ_. c_type_class.zero)) [0..<n])) s"
definition assume_stack_alloc:: "nat ⇒ ('t ⇒ ('a::xmem_type) list set) ⇒ ('e::default, 'a ptr, 't) spec_monad" where
"assume_stack_alloc n init ≡ assume_result_and_state (λs. {(p, t).
∃d vs. (p, d) ∈ stack_allocs n 𝒮 TYPE('a::xmem_type) (heap_typing s) ∧
vs ∈ init s ∧
length vs = n ∧
(∀i ∈ {0..<n}. r s (p +⇩p int i) = ZERO('a::xmem_type)) ∧
t = stack_ptr_acquire n vs p d s})"
definition guard_with_fresh_stack_ptr :: "nat ⇒ ('t ⇒ 'a list set) ⇒ ('a::xmem_type ptr ⇒ ('e::default, 'v, 't) spec_monad) ⇒ ('e, 'v, 't) spec_monad" where
"guard_with_fresh_stack_ptr n init c ≡
do {
p ← assume_stack_alloc n init;
guard_on_exit (c p)
(λs. ∀i < n. root_ptr_valid (heap_typing s) (p +⇩p int i))
{(s, t). t = stack_ptr_release n p s}
}"
definition assume_with_fresh_stack_ptr :: "nat ⇒ ('t ⇒ 'a list set) ⇒ ('a::xmem_type ptr ⇒ ('e::default,'v, 't) spec_monad) ⇒ ('e, 'v, 't) spec_monad" where
"assume_with_fresh_stack_ptr n init c ≡
do {
p ← assume_stack_alloc n init;
assume_on_exit (c p)
(λs. ∀i < n. root_ptr_valid (heap_typing s) (p +⇩p int i))
{(s, t). t = stack_ptr_release n p s}
}"
definition with_fresh_stack_ptr :: "nat ⇒ ('t ⇒ 'a list set) ⇒ ('a::xmem_type ptr ⇒ ('e::default,'v, 't) spec_monad) ⇒ ('e, 'v, 't) spec_monad" where
"with_fresh_stack_ptr n init c ≡
do {
p ← assume_stack_alloc n init;
on_exit (c p)
{(s, t). t = stack_ptr_release n p s}
}"
lemma monotone_guard_with_fresh_stack_ptr_le[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≤) (λf. c f p)"
shows "monotone R (≤) (λf. guard_with_fresh_stack_ptr n I (c f))"
unfolding guard_with_fresh_stack_ptr_def
by (intro partial_function_mono)
lemma monotone_guard_with_fresh_stack_ptr_ge[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≥) (λf. c f p)"
shows "monotone R (≥) (λf. guard_with_fresh_stack_ptr n I (c f))"
unfolding guard_with_fresh_stack_ptr_def
by (intro partial_function_mono)
lemma monotone_assume_with_fresh_stack_ptr_le[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≤) (λf. c f p)"
shows "monotone R (≤) (λf. assume_with_fresh_stack_ptr n I (c f))"
unfolding assume_with_fresh_stack_ptr_def
by (intro partial_function_mono)
lemma monotone_assume_with_fresh_stack_ptr_ge[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≥) (λf. c f p)"
shows "monotone R (≥) (λf. assume_with_fresh_stack_ptr n I (c f))"
unfolding assume_with_fresh_stack_ptr_def
by (intro partial_function_mono)
lemma monotone_with_fresh_stack_ptr_le[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≤) (λf. c f p)"
shows "monotone R (≤) (λf. with_fresh_stack_ptr n I (c f))"
unfolding with_fresh_stack_ptr_def on_exit_def
by (intro partial_function_mono)
lemma monotone_with_fresh_stack_ptr_ge[partial_function_mono]:
assumes [partial_function_mono]: "⋀p. monotone R (≥) (λf. c f p)"
shows "monotone R (≥) (λf. with_fresh_stack_ptr n I (c f))"
unfolding with_fresh_stack_ptr_def on_exit_def
by (intro partial_function_mono)
lemma refines_rel_xval_guard_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod (rel_xval L R) (=))"
shows
"refines
(guard_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(guard_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod (rel_xval L R) (=))"
unfolding guard_with_fresh_stack_ptr_def L2_VARS_def on_exit'_def assume_stack_alloc_def
apply (rule refines_bind')
apply (subst refines_assume_result_and_state_iff)
apply (subst init_eq)
apply (rule sim_set_refl)
apply clarsimp
apply (rule refines_bind_exception_or_result'[OF f])
apply (rule refines_bind')
apply (rule refines_bind')
apply (rule refines_guard)
apply simp_all
apply (rule refines_assert_result_and_state)
apply simp_all
done
lemma refines_rel_xval_assume_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod (rel_xval L R) (=))"
shows
"refines
(assume_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(assume_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod (rel_xval L R) (=))"
unfolding assume_with_fresh_stack_ptr_def L2_VARS_def on_exit'_def assume_stack_alloc_def
apply (rule refines_bind')
apply (subst refines_assume_result_and_state_iff)
apply (subst init_eq)
apply (rule sim_set_refl)
apply clarsimp
apply (rule refines_bind_exception_or_result'[OF f])
apply (rule refines_bind')
apply (rule refines_bind')
apply (rule refines_assuming)
apply simp_all
apply (rule refines_assert_result_and_state)
apply simp_all
done
lemma refines_rel_xval_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod (rel_xval L R) (=))"
shows
"refines
(with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod (rel_xval L R) (=))"
unfolding with_fresh_stack_ptr_def L2_VARS_def assume_stack_alloc_def
apply (rule refines_bind_no_throw [where Q = "rel_prod (rel_xval (λ_ _. False) (=)) (=)"])
apply simp
apply simp
subgoal using init_eq by (auto simp add: refines_def_old rel_xval.simps)
subgoal
apply clarsimp
apply (rule refines_rel_xval_on_exit)
apply (rule f)
done
done
lemma write_same_ZERO:
"r s p = ZERO('a) ⟹ w p (λy. ZERO('a)) s = s"
using write_same by simp
end
lemma refines_rel_prod_eq_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod Q (=))"
shows "refines
(on_exit f⇩c cleanup)
(on_exit f⇩a cleanup) s s
(rel_prod Q (=))"
unfolding on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result')
apply (rule f)
apply clarsimp
apply (rule refines_bind_no_throw )
apply simp
apply simp
apply (rule refines_state_select_same)
apply clarsimp
done
context stack_heap_state
begin
lemma refines_rel_prod_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod Q (=))"
shows
"refines
(with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod Q (=))"
unfolding with_fresh_stack_ptr_def L2_VARS_def
apply (rule refines_bind_no_throw )
apply simp
apply simp
apply (rule refines_assume_result_and_state_same')
apply (simp only: init_eq)
apply clarsimp
apply (rule refines_rel_prod_eq_on_exit)
apply (rule f)
done
end
lemma h_val_coerce_ptr_coerce_packed:
fixes p::"'c::packed_type ptr"
assumes sz_eq: "size_of TYPE('c) = size_of TYPE('a::packed_type)"
shows "h_val h (PTR_COERCE ('c → 'a) p) = COERCE ('c → 'a) (h_val h p)"
by (simp add: h_val_def sz_eq from_bytes_def coerce_def to_bytes_p_def to_bytes_def
packed_type_access_ti access_ti⇩0_def field_access_update_same(1)
size_of_fold sz_eq td_fafu_idem update_ti_t_def)
lemma h_val_field_ptr_coerce_from_bytes_packed:
fixes p::"'c::packed_type ptr"
assumes "field_ti TYPE('a) f = Some t"
assumes "export_uinfo t = export_uinfo (typ_info_t TYPE('b::mem_type))"
assumes [simp]: "size_of TYPE('c) = size_of TYPE('a)"
shows "h_val h (PTR('b) &((PTR_COERCE('c::packed_type → 'a::packed_type) p)→f)) =
from_bytes (access_ti⇩0 t (COERCE ('c → 'a) (h_val h p)))"
apply (simp add:h_val_coerce_ptr_coerce_packed[symmetric])
apply (rule h_val_field_from_bytes' [OF assms(1) assms(2)])
done
lemma packed_type_value_update_ti_explode:
"(v::'a::packed_type) = update_ti (typ_info_t TYPE('a)) (to_bytes_p v) v'"
by (simp add: size_of_def update_ti_s_from_bytes update_ti_update_ti_t)
lemma packed_type_to_bytes_to_bytes_p_conv:
"length bs = size_of TYPE('a::packed_type) ⟹ to_bytes v bs = to_bytes_p (v::'a)"
apply (simp add: to_bytes_p_def)
by (simp add: packed_type_access_ti to_bytes_def)
lemma packed_type_to_byte_p_coerce:
assumes sz:"size_of TYPE('c::packed_type) = size_of TYPE('a::packed_type)"
shows "to_bytes_p (COERCE('a → 'c) v) = to_bytes_p v"
using sz
apply (simp add: to_bytes_p_def coerce_def)
by (metis (mono_tags, lifting) field_access_update_same(1) field_desc.simps(2) field_desc_def
from_bytes_def len length_replicate size_of_fold td_fafu_idem to_bytes_def
update_ti_t_def wf_fd)
lemma to_bytes_coerce_packed:
"size_of TYPE('a) = size_of TYPE('b) ⟹ length bs = size_of TYPE('a) ⟹
to_bytes (COERCE('a::packed_type→'b::packed_type) v) bs = to_bytes v bs"
by (simp add: coerce_def field_access_update_same(1) from_bytes_def packed_type_access_ti
size_of_def td_fafu_idem to_bytes_def update_ti_t_def)
lemma heap_update_ptr_coerse_packed:
fixes p::"'c::packed_type ptr"
assumes cgrd: "c_guard p"
assumes [simp]: "size_of TYPE('c) = size_of TYPE('a::packed_type )"
shows "heap_update (PTR_COERCE('c → 'a) p) v = heap_update p (COERCE('a →'c) v)"
apply (rule ext)
apply (simp add: heap_update_def packed_type_to_bytes_to_bytes_p_conv packed_type_to_byte_p_coerce)
done
lemma c_guard_ptr_coerceI:
"size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a)) ⟹
align_td (typ_info_t TYPE('a)) ≤ align_td (typ_info_t TYPE('c)) ⟹
c_guard p ⟹
c_guard (PTR_COERCE('c::c_type→'a::c_type) p)"
apply (cases p)
using power_le_dvd
by (auto simp add: c_guard_def c_null_guard_def ptr_aligned_def align_of_def size_of_def)
lemma heap_update_field_ptr_coerce_from_bytes_packed:
fixes p::"'c::{xmem_type, packed_type} ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a::{xmem_type, packed_type})) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t (TYPE('b::{xmem_type}))"
assumes cgrd: "c_guard (PTR_COERCE('c→ 'a) p)"
assumes sz[simp]: "size_of TYPE('c) = size_of TYPE('a)"
shows "heap_update (PTR('b) &((PTR_COERCE('c→ 'a) p)→f)) v h =
heap_update p (coerce_map (update_ti t (to_bytes_p v)) (h_val h p)) h"
apply (subst heap_update_field_root_conv' [OF fl match cgrd])
apply (simp add: heap_update_def h_val_coerce_ptr_coerce_packed )
apply (subst coerce_coerce_map_cancel_packed[OF sz[symmetric], symmetric])
apply (simp add: coerce_map_def)
apply (subst to_bytes_coerce_packed)
apply (simp_all)
done
named_theorems L2_modify_heap_update_field_root_conv
context heap_state
begin
lemma heap_update_field_root_conv:
fixes p::"'a::xmem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update ∘ (λx _. x)), n)"
assumes fg_cons: "fg_cons fld (fld_update ∘ (λx _. x))"
assumes cgrd: "c_guard p"
shows "(hmem_upd (heap_update (PTR('b) &(p→f)) v)) =
(λs. (hmem_upd (heap_update p (fld_update (λ_. v) (h_val (hmem s) p)))) s)"
apply (subst heap_update_field_root_conv_pointless' [OF fl fg_cons cgrd])
apply (rule ext)
by (metis (mono_tags, lifting) heap.upd_cong)
lemma heap_update_field_root_conv':
fixes p::"'a::xmem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
assumes cgrd: "c_guard p"
shows "(hmem_upd (heap_update (PTR('b) &(p→f)) v)) =
(λs. (hmem_upd (heap_update p (update_ti t (to_bytes_p v) (h_val (hmem s) p)))) s)"
using heap_update_field_root_conv' [OF fl match cgrd, of v]
using heap.upd_cong by blast
lemma L2_modify_heap_update_field_root_conv:
fixes p::"'a::xmem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b::xmem_type)) fld (fld_update ∘ (λx _. x)), n)"
assumes fg_cons: "fg_cons fld (fld_update ∘ (λx _. x))"
assumes cgrd: "c_guard p"
shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &(p→f)) (v s)) s) =
L2_modify (λs. (hmem_upd (heap_update p (fld_update (λ_. v s) (h_val (hmem s) p)))) s)"
by (simp add: heap_update_field_root_conv [OF fl fg_cons cgrd])
lemma L2_modify_heap_update_field_root_conv' [L2_modify_heap_update_field_root_conv]:
fixes p::"'a::xmem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
assumes cgrd: "c_guard p"
shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &(p→f)) (v s)) s) =
L2_modify (λs. (hmem_upd (heap_update p (update_ti t (to_bytes_p (v s)) (h_val (hmem s) p)))) s)"
by (simp add: heap_update_field_root_conv' [OF fl match cgrd])
lemma L2_modify_heap_update_ptr_coerce_packed_conv':
fixes p::"'c::packed_type ptr"
assumes cgrd: "c_guard p"
assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a::packed_type))"
shows "L2_modify (λs. hmem_upd (heap_update (PTR_COERCE('c → 'a) p) (COERCE('c → 'a) (v s))) s) =
L2_modify (λs. (hmem_upd (heap_update p (v s))) s)"
using heap_update_ptr_coerse_packed [simplified size_of_def, OF cgrd sz] heap.upd_cong
by (metis assms(2) coerce_cancel_packed size_of_def)
lemma L2_modify_heap_update_ptr_coerce_packed_conv[L2_modify_heap_update_field_root_conv]:
fixes p::"'c::packed_type ptr"
assumes cgrd: "c_guard p"
assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a::packed_type))"
shows "L2_modify (λs. hmem_upd (heap_update (PTR_COERCE('c → 'a) p) (v s)) s) =
L2_modify (λs. (hmem_upd (heap_update p (COERCE('a → 'c) (v s)))) s)"
using heap_update_ptr_coerse_packed [simplified size_of_def, OF cgrd sz] heap.upd_cong
by (metis assms(2) coerce_cancel_packed size_of_def)
lemma L2_modify_heap_update_ptr_coerce_packed_field_root_conv [L2_modify_heap_update_field_root_conv]:
fixes p::"'c::{xmem_type, packed_type} ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a::{xmem_type, packed_type})) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::xmem_type)"
assumes cgrd: "c_guard (PTR_COERCE('c→ 'a) p)"
assumes sz: "size_td (typ_info_t TYPE('c)) = size_td (typ_info_t TYPE('a))"
shows "L2_modify (λs. hmem_upd (heap_update (PTR('b) &((PTR_COERCE('c→ 'a) p)→f)) (v s)) s) =
L2_modify (λs. (hmem_upd (heap_update p (coerce_map (update_ti t (to_bytes_p (v s))) (h_val (hmem s) p)))) s)"
using heap_update_field_ptr_coerce_from_bytes_packed [simplified size_of_def, OF fl match cgrd sz] heap.upd_cong
by meson
end
lemma L2_try_state_asssumeE_bindE:
"L2_try (assume_result_and_state P >>= f) = assume_result_and_state P >>= (λx. L2_try (f x))"
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff L2_defs)
done
lemma refines_L2_try_L2_seq_nondet:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (L2_try (g v)) (g' v) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_seq f g)) (f' >>= g') s s (rel_prod rel_liftE (=))"
unfolding L2_try_def L2_seq_def try_nested_bind_exception_or_result_conv
using g f
apply (clarsimp simp add: refines_def_old L2_defs succeeds_bind reaches_bind reaches_try succeeds_bind_exception_or_result
rel_liftE_def unnest_exn_def reaches_bind_exception_or_result succeeds_bind_exception_or_result split: xval_splits sum.splits)
apply (intro conjI allI impI)
apply (metis case_xval_simps(2) )
apply clarsimp
subgoal for r s' r'
apply (cases r)
subgoal
apply (cases r')
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
by (meson Exn_neq_Result obj_sumE)
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
subgoal for s1 y r1
apply (cases r1)
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
by (metis Exn_neq_Result Result_eq_Result case_xval_simps(1) old.sum.simps(5) sum_all_ex(2))
subgoal
by (auto simp add: default_option_def Exn_def [symmetric])
done
done
done
subgoal
apply (cases r')
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
by (meson Exn_neq_Result sum_all_ex(2))
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
subgoal for s1 r1
apply (cases r1)
subgoal
apply (clarsimp simp add: default_option_def Exn_def [symmetric])
by (metis Result_eq_Result case_xval_simps(1) old.sum.simps(6) sum_all_ex(2))
subgoal
by (metis case_xval_simps(2))
done
done
done
done
done
lemma refines_L2_try_pure:
assumes f: "refines f (return f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_try f) (return f') s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_guarded_def using f
by (fastforce simp add: refines_def_old reaches_try rel_liftE_def)
lemma refines_liftE_conv: "refines f f' s t (rel_prod rel_liftE (=)) ⟷
refines f (liftE f') s t (=)"
unfolding L2_defs L2_guarded_def
by (auto simp add: refines_def_old reaches_liftE rel_liftE_def)
lemma refines_rel_liftE_L2_try_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod rel_liftE (=))"
shows "refines (L2_try (on_exit f⇩c cleanup)) (on_exit f⇩a cleanup) s s (rel_prod rel_liftE (=))"
using f unfolding L2_defs try_def refines_map_value_left_iff
apply (rule refines_rel_prod_eq_on_exit[THEN refines_weaken])
apply (auto simp: rel_liftE_def)
done
lemma map_value_on_exit:
"map_value g (on_exit f cleanup) = on_exit (map_value g f) cleanup"
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff on_exit_def on_exit'_def)
done
lemma L2_try_on_exit: "L2_try (on_exit f cleanup) = on_exit (L2_try f) cleanup"
unfolding L2_try_def try_def
by (simp add: map_value_on_exit)
context stack_heap_state
begin
lemma L2_try_with_fresh_stack_ptr:
"L2_try (with_fresh_stack_ptr n init f) = with_fresh_stack_ptr n init (λp. L2_try (f p))"
by (simp add: with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE L2_try_on_exit)
end
lemma map_value_guard_on_exit:
"map_value g (guard_on_exit f P cleanup) = guard_on_exit (map_value g f) P cleanup"
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff on_exit'_def)
done
lemma L2_try_guard_on_exit:
"L2_try (guard_on_exit f P cleanup) = guard_on_exit (L2_try f) P cleanup"
unfolding L2_try_def try_def
by (simp add: map_value_guard_on_exit)
lemma map_value_assume_on_exit:
"map_value g (assume_on_exit f P cleanup) = assume_on_exit (map_value g f) P cleanup"
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff on_exit'_def)
done
lemma L2_try_assume_on_exit:
"L2_try (assume_on_exit f P cleanup) = assume_on_exit (L2_try f) P cleanup"
unfolding L2_try_def try_def
by (simp add: map_value_assume_on_exit)
context typ_heap_typing
begin
lemma L2_try_guard_with_fresh_stack_ptr:
"L2_try (guard_with_fresh_stack_ptr n init f) = guard_with_fresh_stack_ptr n init (λp. L2_try (f p))"
unfolding guard_with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def
L2_try_guard_on_exit ..
lemma L2_try_assume_with_fresh_stack_ptr:
"L2_try (assume_with_fresh_stack_ptr n init f) = assume_with_fresh_stack_ptr n init (λp. L2_try (f p))"
unfolding assume_with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def
L2_try_assume_on_exit ..
lemma L2_try_with_fresh_stack_ptr:
"L2_try (with_fresh_stack_ptr n init f) = with_fresh_stack_ptr n init (λp. L2_try (f p))"
by (simp add: with_fresh_stack_ptr_def L2_try_state_asssumeE_bindE assume_stack_alloc_def
L2_try_on_exit)
end
lemma refines_L2_seq:
assumes f: "refines f f' s s' Q"
assumes ll: "⋀e e' t t'. Q (Exn e, t) (Exn e', t') ⟹ R (Exn e, t) (Exn e', t')"
assumes lr: "⋀e v' t t'. Q (Exn e, t) (Result v', t') ⟹ refines (throw e) (g' v') t t' R"
assumes rl: "⋀v e' t t'. Q (Result v, t) (Exn e', t') ⟹ refines (g v) (throw e') t t' R"
assumes rr: "⋀v v' t t'. Q (Result v, t) (Result v', t') ⟹ refines (g v) (g' v') t t' R"
shows "refines (L2_seq f g) (L2_seq f' g') s s' R"
unfolding L2_seq_def using f ll lr rl rr
by (rule refines_bind_bind_exn)
lemma rel_Nonlocal_Nonlocal: "rel_Nonlocal (Nonlocal x) x"
by (simp add: rel_Nonlocal_def)
lemmas rel_sum_Inl = rel_sum.intros(1)
lemmas rel_sum_Inr = rel_sum.intros(2)
lemma rel_sum_eq: "rel_sum (=) (=) x x"
by (auto simp add: rel_sum.simps)
end