Theory L1Defs
chapter ‹L1 phase›
theory L1Defs
imports CCorresE
begin
type_synonym 's L1_monad = "(unit, unit, 's) exn_monad"
definition "L1_seq (A :: 's L1_monad) (B :: 's L1_monad) ≡ (A >>= (λ_. B)) :: 's L1_monad"
definition "L1_skip ≡ return () :: 's L1_monad"
definition "L1_modify m ≡ (modify m) :: 's L1_monad"
definition "L1_condition c (A :: 's L1_monad) (B :: 's L1_monad) ≡ condition c A B"
definition "L1_catch (A :: 's L1_monad) (B :: 's L1_monad) ≡ (A <catch> (λ_. B))"
definition "L1_while c (A :: 's L1_monad) ≡ (whileLoop (λ_. c) (λ_. A) ())"
definition "L1_throw ≡ throw () :: 's L1_monad"
definition "L1_spec r ≡ state_select r :: 's L1_monad"
definition "L1_assume f ≡ assume_result_and_state f :: 's L1_monad"
definition "L1_guard c ≡ guard c :: 's L1_monad"
definition "L1_init v ≡ (do { x ← select UNIV; modify (v (λ_. x)) }) :: 's L1_monad"
definition "L1_call scope_setup (dest_fn :: 's L1_monad) scope_teardown result_exn return_xf ≡
do {
s ← get_state;
((do { modify scope_setup;
dest_fn })
<catch> (λ_. L1_seq (modify (λt. result_exn (scope_teardown s t) t)) L1_throw));
t ← get_state;
modify (scope_teardown s);
modify (return_xf t)
}"
definition "L1_fail ≡ fail :: 's L1_monad"
definition "L1_set_to_pred S ≡ λs. s ∈ S"
definition "L1_rel_to_fun R = (λs. Pair () ` Image R {s})"
lemma L1_rel_to_fun_alt: "L1_rel_to_fun R = (λs. Pair () ` {s'. (s, s') ∈ R})"
by (auto simp: L1_rel_to_fun_def)
lemmas L1_defs = L1_seq_def L1_skip_def L1_modify_def L1_condition_def
L1_catch_def L1_while_def L1_throw_def L1_spec_def L1_assume_def L1_guard_def
L1_fail_def L1_init_def L1_set_to_pred_def L1_rel_to_fun_def
lemmas L1_defs' =
L1_seq_def L1_skip_def L1_modify_def L1_condition_def L1_catch_def
L1_while_def L1_throw_def L1_spec_def L1_assume_def
L1_guard_def
L1_fail_def L1_init_def L1_set_to_pred_def L1_rel_to_fun_def
declare L1_set_to_pred_def [simp]
declare L1_rel_to_fun_def [simp]
definition L1_guarded:: "('s ⇒ bool) ⇒ 's L1_monad ⇒ 's L1_monad"
where
"L1_guarded g f = L1_seq (L1_guard g) f"
locale L1_functions =
fixes 𝒫:: "unit ptr ⇒ 's L1_monad"
begin
definition "L1_dyn_call g scope_setup (dest :: 's ⇒ unit ptr) scope_teardown result_exn return_xf ≡
L1_guarded g (gets dest >>= (λp. L1_call scope_setup (𝒫 p) scope_teardown result_exn return_xf))"
end
definition
L1corres :: "bool ⇒ ('p ⇒ ('s, 'p, strictc_errortype) com option)
⇒ 's L1_monad ⇒ ('s, 'p, strictc_errortype) com ⇒ bool"
where
"L1corres check_term Γ ≡
λA C. ∀s. succeeds A s ⟶
((∀t. Γ ⊢ ⟨C, Normal s⟩ ⇒ t ⟶
(case t of
Normal s' ⇒ reaches A s (Result ()) s'
| Abrupt s' ⇒ reaches A s (Exn ()) s'
| Fault e ⇒ e ∈ {AssumeError, StackOverflow}
| _ ⇒ False))
∧ (check_term ⟶ Γ ⊢ C ↓ Normal s))"
definition
L1corres' :: "bool ⇒ ('p ⇒ ('s, 'p, strictc_errortype) com option) ⇒ ('s ⇒ bool)
⇒ 's L1_monad ⇒ ('s, 'p, strictc_errortype) com ⇒ bool"
where
"L1corres' check_term Γ P ≡
λA C. ∀s. (P s) ∧ succeeds A s ⟶
((∀t. Γ ⊢ ⟨C, Normal s⟩ ⇒ t ⟶
(case t of
Normal s' ⇒ reaches A s (Result ()) s'
| Abrupt s' ⇒ reaches A s (Exn ()) s'
| Fault e ⇒ e ∈ {AssumeError, StackOverflow}
| _ ⇒ False))
∧ (check_term ⟶ Γ ⊢ C ↓ Normal s))"
lemma L1corres_alt_def: "L1corres ct Γ = ccorresE (λx. x) ct {AssumeError, StackOverflow} Γ ⊤ UNIV"
apply (rule ext)+
apply (clarsimp simp: L1corres_def ccorresE_def)
done
lemma L1corres'_alt_def: "L1corres' ct Γ P = ccorresE (λx. x) ct {AssumeError, StackOverflow} Γ P UNIV"
apply (rule ext)+
apply (clarsimp simp: L1corres'_def ccorresE_def)
done
lemma admissible_nondet_ord_L1corres [corres_admissible]:
"ccpo.admissible Inf (≥) (λA. L1corres ct Γ A C)"
unfolding L1corres_def imp_conjR disj_imp[symmetric]
apply (intro admissible_all)
apply (intro admissible_conj)
apply (rule ccpo.admissibleI)
apply (clarsimp split: xstate.splits)
apply (intro conjI admissible_mem)
subgoal
apply (simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits)
apply transfer
apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
by (metis outcomes.simps(2) post_state.simps(3))
subgoal
apply (simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits)
apply transfer
apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
by (metis outcomes.simps(2) post_state.simps(3))
subgoal
apply (simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits)
apply transfer
apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
by (metis outcomes.simps(2) post_state.simps(3))
subgoal
apply (simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits)
apply transfer
apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
done
apply (rule ccpo.admissibleI)
apply (simp split: xstate.splits)
apply (clarsimp simp add: ccpo.admissible_def chain_def
succeeds_def reaches_def split: prod.splits)
apply transfer
apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def
split: if_split_asm)
done
lemma L1corres_top [corres_top]: "L1corres ct P ⊤ C"
by (auto simp add: L1corres_def)
lemma L1corres_guard_DynCom:
"⟦⋀s. s ∈ g ⟹ L1corres ct Γ (B s) (B' s)⟧ ⟹
L1corres ct Γ (L1_seq (L1_guard (λs. s ∈ g)) (gets B ⤜ (λb. b))) (Guard f g (DynCom B'))"
apply (clarsimp simp: L1corres_def L1_defs)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
done
lemma L1corres'_guard_DynCom_conseq:
assumes conseq: "⋀s. P s ⟹ g s ⟹ s ∈ g'"
assumes corres: "⋀s. P s ⟹ g s ⟹ L1corres' ct Γ (λs. P s ∧ g s) (B s) (B' s)"
shows "L1corres' ct Γ P (L1_seq (L1_guard g) (gets B ⤜ (λb. b))) (Guard f g' (DynCom B'))"
using conseq corres
apply (clarsimp simp: L1corres'_def L1_defs)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
done
lemma L1corres'_guard_DynCom:
"⟦⋀s. P s ⟹ s ∈ g ⟹ L1corres' ct Γ (λs. P s ∧ s ∈ g) (B s) (B' s)⟧ ⟹
L1corres' ct Γ P (L1_seq (L1_guard (λs. s ∈ g)) (gets B ⤜ (λb. b))) (Guard f g (DynCom B'))"
apply (rule L1corres'_guard_DynCom_conseq [where B=B])
apply simp
apply simp
done
lemma L1corres_DynCom:
assumes corres_f: "⋀s. L1corres ct Γ (g s) (f s)"
shows "L1corres ct Γ (gets g ⤜ (λb. b)) (DynCom f)"
using corres_f
apply (clarsimp simp: L1corres_def L1_defs)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
done
lemma L1corres'_DynCom:
assumes corres_f: "⋀s. P s ⟹ L1corres' ct Γ P (g s) (f s)"
shows "L1corres' ct Γ P (gets g ⤜ (λb. b)) (DynCom f)"
using corres_f
apply (clarsimp simp: L1corres'_def L1_defs)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
done
lemma L1corres'_DynCom_fix_state:
assumes corres_f: "⋀s. P s ⟹ L1corres' ct Γ (λs'. P s' ∧ s' = s) (g s) (f s)"
shows "L1corres' ct Γ P (gets g ⤜ (λb. b)) (DynCom f)"
using corres_f
apply (clarsimp simp: L1corres'_def L1_defs)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
done
lemma L1corres'_guard':
"⟦ L1corres' ct Γ (λs. P s ∧ s ∈ g) B B' ⟧ ⟹
L1corres' ct Γ P (L1_seq (L1_guard (λs. s ∈ g)) B) (Guard f g B')"
apply (clarsimp simp: L1corres'_def L1_defs)
apply (erule_tac x=s in allE)
apply (rule conjI)
apply clarsimp
apply (erule exec_Normal_elim_cases)
subgoal
by (auto simp: succeeds_bind reaches_bind split: xstate.splits)
subgoal
by (auto simp: succeeds_bind reaches_bind split: xstate.splits)
subgoal
by (auto simp: succeeds_bind intro: terminates.intros)
done
lemma L1corres'_guarded:
"⟦ L1corres' ct Γ (λs. P s ∧ s ∈ g) B B' ⟧ ⟹
L1corres' ct Γ P (L1_guarded (λs. s ∈ g) B) (Guard f g B')"
unfolding L1_guarded_def by (rule L1corres'_guard')
lemma L1corres'_Guard_maybe_guard:
"L1corres' ct Γ P B (Guard f g B') ⟹ L1corres' ct Γ P B (maybe_guard f g B')"
apply (simp add: L1corres'_def maybe_guard_def)
by (meson exec.Guard iso_tuple_UNIV_I terminates_Normal_elim_cases(2))
lemma L1corres'_guarded_DynCom_conseq:
assumes conseq: "⋀s. P s ⟹ g s ⟹ s ∈ g'"
assumes corres_B: "⋀s. P s ⟹ g s ⟹ L1corres' ct Γ (λs. P s ∧ g s) (B s) (B' s)"
shows "L1corres' ct Γ P (L1_guarded g (gets B ⤜ (λb. b))) (maybe_guard f g' (DynCom B'))"
apply (rule L1corres'_Guard_maybe_guard)
unfolding L1_guarded_def L1_set_to_pred_def
using corres_B
by (simp add: L1corres'_guard_DynCom_conseq [OF conseq])
lemma L1corres'_guarded_DynCom:
assumes corres_B: "⋀s. P s ⟹ s ∈ g ⟹ L1corres' ct Γ (λs. P s ∧ s ∈ g) (B s) (B' s)"
shows "L1corres' ct Γ P (L1_guarded (L1_set_to_pred g) (gets B ⤜ (λb. b))) (maybe_guard f g (DynCom B'))"
apply (rule L1corres'_guarded_DynCom_conseq [where B=B])
apply simp
using corres_B
apply simp
done
lemma L1corres'_conseq:
assumes corres_Q: "L1corres' ct Γ Q B B'"
assumes conseq: "⋀s. P s ⟹ Q s"
shows "L1corres' ct Γ P B B'"
using conseq corres_Q
by (auto simp add: L1corres'_def)
lemma L1corres_to_L1corres': "L1corres ct Γ = L1corres' ct Γ ⊤"
by (simp add: L1corres_def L1corres'_def)
lemma L1corres_guarded_DynCom_conseq:
assumes conseq: "⋀s. g s ⟹ s ∈ g'"
assumes corres_B: "⋀s. g s ⟹ L1corres ct Γ (B s) (B' s)"
shows "L1corres ct Γ (L1_guarded g (gets B ⤜ (λb. b))) (maybe_guard f g' (DynCom B'))"
using corres_B unfolding L1corres_to_L1corres'
thm L1corres'_guarded_DynCom
apply -
apply (rule L1corres'_guarded_DynCom_conseq [where B=B ])
using conseq apply simp
apply (rule L1corres'_conseq [where Q = "⊤"])
apply (simp)
apply simp
done
lemma L1corres_guarded_DynCom:
assumes corres_B: "⋀s. s ∈ g ⟹ L1corres ct Γ (B s) (B' s)"
shows "L1corres ct Γ (L1_guarded (L1_set_to_pred g) (gets B ⤜ (λb. b))) (maybe_guard f g (DynCom B'))"
using corres_B unfolding L1corres_to_L1corres'
apply -
apply (rule L1corres'_guarded_DynCom [where B=B ])
apply (rule L1corres'_conseq [where Q = "⊤"])
apply simp
apply simp
done
definition
"L1_call_simpl check_term Gamma proc
= do {s ← get_state;
assert (check_term ⟶ Gamma ⊢ Call proc ↓ Normal s);
xs ← select {t. Gamma ⊢ ⟨Call proc, Normal s⟩ ⇒ t};
case xs :: (_, strictc_errortype) xstate of
Normal s ⇒ set_state s
| Abrupt s ⇒ do {set_state s; throw () }
| Fault ft ⇒ fail
| Stuck ⇒ fail
}"
lemma L1corres_call_simpl:
"L1corres ct Γ (L1_call_simpl ct Γ proc) (Call proc)"
apply (clarsimp simp: L1corres_def L1_call_simpl_def)
apply safe
subgoal for s t
apply (cases t)
apply (fastforce elim!: exec_Normal_elim_cases
intro: terminates.intros exec.intros
simp add: succeeds_bind reaches_bind Exn_def )+
done
subgoal for s
apply (auto intro!: terminates.intros simp add: succeeds_bind reaches_bind)
done
done
lemma L1corres_skip:
"L1corres ct Γ L1_skip SKIP"
unfolding L1corres_def L1_defs
by (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind)
lemma L1corres_throw:
"L1corres ct Γ L1_throw Throw"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
lemma L1corres_seq:
"⟦ L1corres ct Γ L L'; L1corres ct Γ R R' ⟧ ⟹
L1corres ct Γ (L1_seq L R) (L' ;; R')"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: L1_seq_def)
apply (rule ccorresE_Seq)
apply auto
done
lemma L1corres_modify:
"L1corres ct Γ (L1_modify m) (Basic m)"
apply (clarsimp simp: L1corres_def L1_defs)
apply (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
done
lemma L1corres_condition:
"⟦ L1corres ct Γ L L'; L1corres ct Γ R R' ⟧ ⟹
L1corres ct Γ (L1_condition (L1_set_to_pred c) L R) (Cond c L' R')"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: L1_defs)
apply (rule ccorresE_Cond_match)
apply (erule ccorresE_guard_imp, simp+)[1]
apply (erule ccorresE_guard_imp, simp+)[1]
apply simp
done
lemma L1corres_catch:
"⟦ L1corres ct Γ L L'; L1corres ct Γ R R' ⟧ ⟹
L1corres ct Γ (L1_catch L R) (Catch L' R')"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: L1_catch_def)
apply (erule ccorresE_Catch)
apply force
done
lemma L1corres_while:
"⟦ L1corres ct Γ B B' ⟧ ⟹
L1corres ct Γ (L1_while (L1_set_to_pred c) B) (While c B')"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: L1_defs)
apply (rule ccorresE_While)
apply clarsimp
apply simp
done
lemma L1corres_guard:
"⟦ L1corres ct Γ B B' ⟧ ⟹
L1corres ct Γ (L1_seq (L1_guard (L1_set_to_pred c)) B) (Guard f c B')"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: ccorresE_def L1_defs)
apply (erule_tac x=s in allE)
apply (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
done
lemma L1corres_spec:
"L1corres ct Γ (L1_spec x) (com.Spec x)"
apply (clarsimp simp: L1corres_def L1_defs)
apply (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
done
lemma L1_init_alt_def:
"L1_init upd ≡ L1_spec {(s, t). ∃v. t = upd (λ_. v) s}"
apply (rule eq_reflection)
apply (clarsimp simp: L1_defs)
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
lemma L1corres_init:
"L1corres ct Γ (L1_init upd) (lvar_nondet_init upd)"
by (auto simp: L1_init_alt_def lvar_nondet_init_def intro: L1corres_spec)
lemma L1corres_guarded_spec:
"L1corres ct Γ (L1_spec R) (guarded_spec_body F R)"
apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_spec_def guarded_spec_body_def)
apply (force simp: liftE_def bind_def
elim: exec_Normal_elim_cases intro: terminates.Guard terminates.Spec)
done
lemma L1corres_assume:
"L1corres ct Γ (L1_assume (L1_rel_to_fun R)) (guarded_spec_body AssumeError R)"
apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def L1_rel_to_fun_alt guarded_spec_body_def)
apply (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
done
lemma pred_conj_apply[simp]: "(P and Q) s ⟷ P s ∧ Q s"
by (auto simp add: pred_conj_def)
lemma L1corres_call:
"⟦ L1corres ct Γ dest_fn (Call dest) ⟧ ⟹
L1corres ct Γ
(L1_call scope_setup dest_fn scope_teardown_norm scope_teardown_exn f)
(call_exn scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (f t)))"
apply (clarsimp simp: L1corres_alt_def)
apply (unfold call_exn_def block_exn_def L1_call_def)
apply (rule ccorresE_DynCom)
apply clarsimp
apply (rule ccorresE_get)
apply (rule ccorresE_assume_pre, clarsimp)
apply (rule ccorresE_guard_imp_stronger)
apply (rule ccorresE_Seq)
apply (rule ccorresE_Catch)
apply (rule ccorresE_Seq)
apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
apply assumption
apply (rule L1corres_seq[unfolded L1corres_alt_def])
apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
apply (rule L1corres_throw [unfolded L1corres_alt_def])
apply (rule ccorresE_DynCom)
apply (rule ccorresE_get)
apply (rule ccorresE_assume_pre, clarsimp)
apply (rule ccorresE_guard_imp)
apply (rule ccorresE_Seq)
apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
apply simp
apply simp
apply simp
apply simp
done
lemma (in L1_functions) L1corres_dyn_call_conseq:
assumes conseq: "⋀s. g s ⟹ s ∈ g'"
assumes corres_dest: "⋀s. g s ⟹ L1corres ct Γ (𝒫 (dest s)) (Call (dest s))"
shows
"L1corres ct Γ
(L1_dyn_call g scope_setup dest scope_teardown_norm scope_teardown_exn result)
(dynCall_exn f g' scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
proof -
have eq: "(gets (λs. L1_call scope_setup (𝒫 (dest s)) scope_teardown_norm scope_teardown_exn result) ⤜ (λb. b)) =
(gets dest ⤜ (λp. L1_call scope_setup (𝒫 p) scope_teardown_norm scope_teardown_exn result))"
apply (rule spec_monad_ext)
apply (simp add: run_bind)
done
show ?thesis
apply (simp add: L1_dyn_call_def dynCall_exn_def)
apply (rule L1corres_guarded_DynCom_conseq [where B = "λs. L1_call scope_setup (𝒫 (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
apply (simp add: conseq)
apply (rule L1corres_call)
apply (rule corres_dest)
by simp
qed
lemma (in L1_functions) L1corres_dyn_call_same_guard:
assumes eq: "L1_set_to_pred g ≡ g'"
assumes corres_dest: "⋀s. g' s ⟹ L1corres ct Γ (𝒫 (dest s)) (Call (dest s))"
shows
"L1corres ct Γ
(L1_dyn_call g' scope_setup dest scope_teardown_norm scope_teardown_exn result)
(dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
apply (rule L1corres_dyn_call_conseq)
apply (simp add: eq [symmetric])
by (rule corres_dest)
lemma (in L1_functions) L1corres_dyn_call_add_and_select_guard:
assumes eq: "L1_set_to_pred g ≡ g'"
assumes corres_dest: "⋀s. G s ⟹ L1corres ct Γ (𝒫 (dest s)) (Call (dest s))"
shows
"L1corres ct Γ
(L1_dyn_call (G and g') scope_setup dest scope_teardown_norm scope_teardown_exn result)
(dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
apply (rule L1corres_dyn_call_conseq)
apply (simp add: eq [symmetric])
apply (rule corres_dest)
apply (simp)
done
lemma L1_seq_guard_merge: "L1_seq (L1_guard P) (L1_seq (L1_guard Q) c) = L1_seq (L1_guard (P and Q)) c"
unfolding L1_defs
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
lemma and_unfold: "(and) = (λP Q s. P s ∧ Q s)"
by (auto simp add: fun_eq_iff)
lemma L1_seq_guard_eq: "(⋀s. P s = Q s) ⟹ L1_seq (L1_guard P) c = L1_seq (L1_guard Q) c"
unfolding L1_defs
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
lemma foldr_and_commute: "⋀s. foldr (and) gs (P and g) s = (g s ∧ foldr (and) gs P s)"
by (induct gs arbitrary: P g) (auto simp add:)
lemma L1corres_fail:
"L1corres ct Γ L1_fail X"
apply (clarsimp simp: L1corres_alt_def)
apply (clarsimp simp: L1_fail_def)
apply (rule ccorresE_fail)
done
lemma L1corres_prepend_unknown_var':
"⟦ L1corres ct Γ A C; ⋀s::'s::type. X (λ_::'a::type. (X' s)) s = s ⟧ ⟹ L1corres ct Γ (L1_seq (L1_init X) A) C"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
metis+
lemma L1_catch_seq_join: "no_throw (λ_. True) A ⟹ L1_seq A (L1_catch B C) = (L1_catch (L1_seq A B) C)"
unfolding no_throw_def L1_defs
apply (rule spec_monad_eqI)
apply (clarsimp simp add: runs_to_iff)
apply (clarsimp simp add: runs_to_def_old runs_to_partial_def_old Exn_def default_option_def)
apply (intro conjI impI iffI)
apply (metis Exn_def Exn_neq_Result)+
done
lemma no_throw_L1_init [simp]: "no_throw P (L1_init f)"
unfolding L1_init_def no_throw_def
apply (clarsimp)
apply (runs_to_vcg)
done
lemma L1corres_prepend_unknown_var:
"⟦ L1corres ct Γ (L1_catch A B) C; ⋀s. X (λ_::'d::type. (X' s)) s = s ⟧
⟹ L1corres ct Γ (L1_catch (L1_seq (L1_init X) A) B) C"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def succeeds_catch reaches_catch)
metis+
lemma L1corres_Call:
"⟦ Γ X' = Some Z'; L1corres ct Γ Z Z' ⟧ ⟹
L1corres ct Γ Z (Call X')"
apply (clarsimp simp: L1corres_alt_def)
apply (erule (1) ccorresE_Call)
done
lemma L1_call_corres [fundef_cong]:
"⟦ scope_setup = scope_setup';
dest_fn = dest_fn';
scope_teardown = scope_teardown';
return_xf = return_xf' ⟧ ⟹
L1_call scope_setup dest_fn scope_teardown return_xf =
L1_call scope_setup' dest_fn' scope_teardown' return_xf'"
apply (clarsimp simp: L1_call_def)
done
lemma L1_corres_cleanup:
"L1corres ct Γ (do {y <- state_select {(s,t). t = cleanup s};
return ()
})
(Basic cleanup)"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
lemma L1_corres_spec_cleanup:
"L1corres ct Γ (do { y <- state_select cleanup;
return ()
})
(com.Spec cleanup)"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
lemma L1_corres_cleanup_throw:
"L1corres ct Γ (do { _ <- state_select {(s,t). t = cleanup s};
throw ()
})
(Basic cleanup;; THROW)"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def default_option_def)
lemma L1_corres_spec_cleanup_throw:
"L1corres ct Γ (do{ _ <- state_select cleanup;
throw ()
})
(com.Spec cleanup;; THROW)"
unfolding L1corres_def L1_defs
by (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def default_option_def)
lemma on_exit_unit_def: "(on_exit f cleanup::(unit, unit, 's) exn_monad) =
bind_handle f
(λv. bind (state_select cleanup) (λ_. return ()))
(λe. bind (state_select cleanup)(λ_. throw ()))"
unfolding on_exit_def on_exit'_def bind_handle_eq
by (intro arg_cong2[where f=bind_exception_or_result])
(auto simp: fun_eq_iff default_option_def Exn_def
split: exception_or_result_split)
lemma on_exit_catch_conv: "on_exit f cleanup =
do {
r ← (f <catch> (λe. state_select cleanup >>= (λ_. throw e)));
state_select cleanup;
return r
}"
unfolding on_exit_def on_exit'_def
apply (rule spec_monad_eqI)
apply (clarsimp simp add: runs_to_iff fun_eq_iff Exn_def default_option_def
intro!: arg_cong[where f="runs_to _ _"])
by (metis default_option_def exception_or_result_cases not_None_eq)
lemma L2corres_on_exit':
assumes m_c: "L1corres ct Γ m c"
shows "L1corres ct Γ (on_exit m {(s,t). t = cleanup s}) (On_Exit c (Basic cleanup))"
unfolding on_exit_catch_conv
apply (simp add: On_Exit_def)
apply (rule L1corres_seq [simplified L1_seq_def])
apply (simp add: L1_catch_def [symmetric])
apply (rule L1corres_catch [OF m_c])
apply (rule L1_corres_cleanup_throw [simplified])
apply (rule L1_corres_cleanup [simplified])
done
lemma L2corres_on_exit:
assumes m_c: "L1corres ct Γ m c"
shows "L1corres ct Γ (on_exit m cleanup) (On_Exit c (com.Spec cleanup))"
apply (simp add: on_exit_catch_conv On_Exit_def)
apply (rule L1corres_seq [simplified L1_seq_def])
apply (simp add: L1_catch_def [symmetric])
apply (rule L1corres_catch [OF m_c])
apply (rule L1_corres_spec_cleanup_throw[simplified])
apply (rule L1_corres_spec_cleanup[simplified])
done
definition
refines_simpl :: "bool ⇒ ('p ⇒ ('s, 'p, strictc_errortype) com option) ⇒
('s, 'p, strictc_errortype) com ⇒
(('e::default, 'a, 't) spec_monad) ⇒
's ⇒ 't ⇒ (('s, strictc_errortype) xstate ⇒ (('e, 'a) exception_or_result * 't) ⇒ bool) ⇒ bool" where
"refines_simpl ct Γ c m s t R ≡
succeeds m t ⟶
((∀s'. Γ ⊢ ⟨c, Normal s⟩ ⇒ s' ⟶
(s' ∈ {Fault AssumeError, Fault StackOverflow} ∨
(∃r t'. reaches m t r t' ∧ R s' (r, t')))) ∧
(ct ⟶ Γ ⊢ c ↓ Normal s))"
lemma refines_simplI:
assumes termi: "succeeds m t ⟹ ct ⟹ Γ ⊢ c ↓ Normal s"
assumes sim: "⋀s'. succeeds m t ⟹ Γ ⊢ ⟨c, Normal s⟩ ⇒ s' ⟹ s' ∉ {Fault AssumeError, Fault StackOverflow}
⟹ ∃r t'. reaches m t r t' ∧ R s' (r, t')"
shows "refines_simpl ct Γ c m s t R"
using termi sim unfolding refines_simpl_def
by blast
definition
rel_L1 :: "('s, strictc_errortype) xstate ⇒ ('e, 'a) xval × 's ⇒ bool" where
"rel_L1 ≡ λs (r, t). (case s of
Normal s' ⇒ (∃x. r = Result x) ∧ t = s'
| Abrupt s' ⇒ (∃x. r = Exn x) ∧ t = s'
| Fault e ⇒ False
| Stuck ⇒ False)"
lemma rel_L1_unit:
"rel_L1 = (λs (r, t). (case s of
Normal s' ⇒ r = Result () ∧ t = s'
| Abrupt s' ⇒ r = Exn () ∧ t = s'
| Fault e ⇒ False
| Stuck ⇒ False))"
by (auto simp add: rel_L1_def split: xstate.splits)
lemma rel_L1_conv [simp]:
"rel_L1 (Normal s) (r, t) = ((∃x. r = Result x) ∧ t = s)"
"rel_L1 (Abrupt s) (r, t) = ((∃x. r = Exn x) ∧ t = s)"
"rel_L1 (Fault e) x = False"
"rel_L1 Stuck x = False"
by (auto simp add: rel_L1_def)
lemma refines_simpl_rel_L1I:
assumes termi: "succeeds m t ⟹ ct ⟹ Γ ⊢ c ↓ Normal s"
assumes sim_Normal: "⋀s'. succeeds m t ⟹ Γ ⊢ ⟨c, Normal s⟩ ⇒ Normal s'
⟹ ∃r. reaches m t (Result r) s'"
assumes sim_Abrupt: "⋀s'. succeeds m t ⟹ Γ ⊢ ⟨c, Normal s⟩ ⇒ Abrupt s'
⟹ ∃r. reaches m t (Exn r) s'"
assumes sim_Fault: "⋀e. succeeds m t ⟹ Γ ⊢ ⟨c, Normal s⟩ ⇒ Fault e
⟹ e ∈ {AssumeError, StackOverflow}"
assumes sim_Stuck: "succeeds m t ⟹ Γ ⊢ ⟨c, Normal s⟩ ⇒ Stuck
⟹ False"
shows "refines_simpl ct Γ c m s t rel_L1"
apply (rule refines_simplI [OF termi], assumption, assumption)
apply (simp add: rel_L1_def)
subgoal for s'
using sim_Normal sim_Abrupt sim_Fault sim_Stuck
apply (cases s')
apply (fastforce split: prod.splits sum.splits)+
done
done
lemma L1corres_refines_simpl:
"L1corres ct Γ m c ⟹ refines_simpl ct Γ c m s s rel_L1"
apply (clarsimp simp add: L1corres_def refines_simpl_def rel_L1_def split: xstate.splits prod.splits sum.splits)
by (smt (verit) Inl_Inr_False xstate.distinct(1) xstate.inject(1) xstate.inject(2))
lemma refines_simpl_L1corres:
assumes "⋀s. refines_simpl ct Γ c m s s rel_L1"
shows "L1corres ct Γ m c"
using assms
apply (force simp add: L1corres_def refines_simpl_def rel_L1_def split: xstate.splits prod.splits sum.splits)
done
theorem L1corres_refines_simpl_conv:
"L1corres ct Γ m c ⟷ (∀s. refines_simpl ct Γ c m s s rel_L1)"
using L1corres_refines_simpl refines_simpl_L1corres
by metis
lemma refines_simpl_DynCom:
"refines_simpl ct Γ (c s) m s t R ⟹ refines_simpl ct Γ (DynCom c) m s t R"
by (auto simp add: refines_simpl_def terminates.DynCom elim: exec_Normal_elim_cases(12))
lemma refines_simpl_StackOverflow:
assumes c: "s ∈ g ⟹ refines_simpl ct Γ c m s t R"
shows "refines_simpl ct Γ (Guard StackOverflow g c) m s t R"
using c
by (auto simp add: refines_simpl_def elim: exec_Normal_elim_cases intro: terminates.intros)
lemma refines_simpl_rel_L1_bind:
fixes m1:: "('e, 'a, 's) exn_monad"
fixes m2:: "'a ⇒ ('e, 'b, 's) exn_monad"
assumes c1: "refines_simpl ct Γ c1 m1 s s rel_L1"
assumes c2: "⋀r s'. succeeds m1 s ⟹ Γ ⊢ ⟨c1, Normal s⟩ ⇒ Normal s' ⟹ reaches m1 s (Result r) s' ⟹
refines_simpl ct Γ c2 (m2 r) s' s' rel_L1"
shows "refines_simpl ct Γ (c1;;c2) (m1 >>= m2) s s rel_L1"
proof (rule refines_simpl_rel_L1I)
assume nofail: "succeeds (m1 >>= m2) s"
assume ct: "ct"
from nofail have nofail_m1: "succeeds m1 s"
by (simp add: succeeds_bind)
with ct c1 have term_c1: "Γ⊢c1 ↓ Normal s"
by (simp add: refines_simpl_def)
then
show "Γ⊢c1;;c2 ↓ Normal s"
proof (rule terminates.intros, intro allI impI)
fix s'
assume exec_c1: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s'"
show "Γ⊢c2 ↓ s'"
proof (cases s')
case (Normal s1)
with exec_c1 c1 nofail_m1 term_c1 ct obtain r where sim1: "reaches m1 s (Result r) s1"
by (force simp add: rel_L1_def refines_simpl_def)
from c2 [OF nofail_m1 exec_c1 [simplified Normal] this]
have "refines_simpl ct Γ c2 (m2 r) s1 s1 rel_L1" .
with ct Normal nofail sim1
show ?thesis
by (simp add: refines_simpl_def reaches_bind succeeds_bind)
qed simp_all
qed
next
fix s'
assume nofail: "succeeds (m1 >>= m2) s"
from nofail have nofail_m1: "succeeds m1 s"
by (simp add: succeeds_bind)
assume exec: "Γ⊢ ⟨c1;;c2,Normal s⟩ ⇒ Normal s'"
then show "∃r. reaches (m1 >>= m2) s (Result r) s'"
proof (cases)
case (1 s1)
hence exec_c1: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s1" and
exec_c2: "Γ⊢ ⟨c2, s1⟩ ⇒ Normal s'" .
from exec_c2 obtain s1' where s1': "s1 = Normal s1'"
by (meson Normal_resultE)
from exec_c1 c1 nofail_m1 obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1) s1' refines_simpl_def xstate.simps(7))
from c2 [OF nofail_m1 exec_c1[simplified s1'] sim1]
have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" .
with nofail exec_c2 obtain r2 where "reaches (m2 r1) s1' (Result r2) s'"
by (smt (verit) empty_iff insertE rel_L1_conv(1) s1' sim1 refines_simpl_def succeeds_bind
reaches_bind xstate.simps(7))
with sim1 nofail show ?thesis
by (fastforce simp add: reaches_bind succeeds_bind)
qed
next
fix s'
assume nofail: "succeeds (m1 >>= m2) s"
from nofail have nofail_m1: "succeeds m1 s"
by (simp add: succeeds_bind)
assume exec: "Γ⊢ ⟨c1;;c2,Normal s⟩ ⇒ Abrupt s'"
then show "∃r. reaches (m1 >>= m2) s (Exn r) s'"
proof (cases)
case (1 s1)
hence exec_c1: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s1" and
exec_c2: "Γ⊢ ⟨c2,s1⟩ ⇒ Abrupt s'" .
show ?thesis
proof (cases s1)
case (Normal s1')
with exec_c1 c1 nofail_m1 obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1) refines_simpl_def xstate.simps(7))
from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" .
with nofail exec_c2 sim1 obtain r2 where "reaches (m2 r1) s1' (Exn r2) s'"
by (smt (verit) Normal empty_iff insertE rel_L1_conv(2) refines_simpl_def succeeds_bind xstate.simps(11))
with sim1 nofail show ?thesis
by (fastforce simp add: reaches_bind succeeds_bind)
next
case (Abrupt s1')
with exec_c1 c1 nofail_m1 obtain r1 where sim1: "reaches m1 s (Exn r1) s1'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(2) refines_simpl_def xstate.distinct(7))
from Abrupt exec_c2 have "s' = s1'"
by (meson Abrupt_end xstate.inject(2))
with nofail
show ?thesis
apply (clarsimp simp add: reaches_bind succeeds_bind Exn_def)
using sim1 by fastforce
next
case (Fault x)
with exec_c2 show ?thesis
by (meson Fault_end xstate.distinct(7))
next
case Stuck
with exec_c2 show ?thesis
using noStuck_startD' by blast
qed
qed
next
fix e
assume nofail: "succeeds (m1 >>= m2) s"
from nofail have nofail_m1: "succeeds m1 s"
by (simp add: succeeds_bind)
assume exec: "Γ⊢ ⟨c1;;c2,Normal s⟩ ⇒ Fault e"
then show "e ∈ {AssumeError, StackOverflow}"
proof (cases)
case (1 s1)
hence exec_c1: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s1" and
exec_c2: "Γ⊢ ⟨c2,s1⟩ ⇒ Fault e" .
show ?thesis
proof (cases s1)
case (Normal s1')
with exec_c1 c1 nofail_m1 obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1) refines_simpl_def xstate.simps(7))
from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" .
with nofail exec_c2 sim1 show "e ∈ {AssumeError, StackOverflow}"
by (metis (no_types, lifting) Normal insert_iff rel_L1_conv(3) refines_simpl_def singleton_iff
succeeds_bind xstate.inject(3))
next
case (Abrupt s1')
with exec_c2 show ?thesis
by (metis Abrupt_end xstate.distinct(7))
next
case (Fault x)
with exec_c2 c1 exec_c1 show ?thesis
by (metis exec_Normal_elim_cases(1) insert_iff nofail_m1 rel_L1_conv(3) refines_simpl_def singleton_iff xstate.inject(3))
next
case Stuck
with exec_c2 show ?thesis
using noStuck_startD' by blast
qed
qed
next
assume nofail: "succeeds (m1 >>= m2) s"
from nofail have nofail_m1: "succeeds m1 s"
by (simp add: succeeds_bind)
assume exec: "Γ⊢ ⟨c1;;c2,Normal s⟩ ⇒ Stuck"
then show False
proof (cases)
case (1 s1)
hence exec_c1: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s1" and
exec_c2: "Γ⊢ ⟨c2,s1⟩ ⇒ Stuck" .
show ?thesis
proof (cases s1)
case (Normal s1')
with exec_c1 c1 nofail_m1 obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1) refines_simpl_def xstate.simps(7))
from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" .
with nofail exec_c2 sim1 show False
by (metis Normal insertE rel_L1_conv(4) refines_simpl_def singletonD succeeds_bind xstate.simps(15))
next
case (Abrupt s1')
with exec_c2 show ?thesis
by (metis Abrupt_end xstate.distinct(10))
next
case (Fault x)
with exec_c2 show ?thesis
by (metis Fault_end isFault_simps(4) not_isFault_iff)
next
case Stuck
with exec_c2 c1 exec_c1 show ?thesis
by (metis insert_iff nofail_m1 rel_L1_conv(4) refines_simpl_def singletonD xstate.simps(15))
qed
qed
qed
lemma refines_simpl_rel_L1_catch:
assumes L: "refines_simpl ct Γ L' L s s rel_L1"
assumes R: "⋀s. refines_simpl ct Γ R' R s s rel_L1"
shows "refines_simpl ct Γ (Catch L' R') (L1_catch L R) s s rel_L1"
proof (rule refines_simpl_rel_L1I)
assume nofault: "succeeds (L1_catch L R) s"
assume ct: "ct"
show "Γ⊢TRY L' CATCH R' END ↓ Normal s"
proof (rule terminates.intros, safe)
show "Γ⊢L' ↓ Normal s"
using nofault ct L
by (simp add: refines_simpl_def L1_catch_def rel_L1_def succeeds_catch)
next
fix s'
assume " Γ⊢ ⟨L',Normal s⟩ ⇒ Abrupt s'"
then show "Γ⊢R' ↓ Normal s'"
using nofault ct L R
by (fastforce simp add: refines_simpl_def L1_catch_def rel_L1_def succeeds_catch)
qed
next
fix s'
assume nofault: "succeeds (L1_catch L R) s"
assume exec: "Γ⊢ ⟨TRY L' CATCH R' END,Normal s⟩ ⇒ Normal s'"
then show "∃r. reaches (L1_catch L R) s (Result r) s'"
proof (cases)
case (1 s1)
hence exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Abrupt s1" and
exec_R': "Γ⊢ ⟨R',Normal s1⟩ ⇒ Normal s'".
from nofault L R exec_L' obtain
nofault_L: "succeeds L s" and
nofault_R: "succeeds R s1"
by (smt (verit, best) L1_defs(5) case_xval_simps(1) insertE refines_simpl_def
rel_L1_conv(2) singletonD succeeds_catch xstate.simps(11))
from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def
singletonD xstate.distinct(7))
from r1 exec_R' R obtain r2 where "reaches R s1 (Result r2) s'"
by (metis (no_types, lifting) insertE nofault_R rel_L1_conv(1)
refines_simpl_def singletonD xstate.simps(7))
with r1 nofault show ?thesis
by (fastforce simp add: reaches_catch succeeds_catch L1_defs )
next
case 2
have exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Normal s'" by fact
from nofault L R exec_L' obtain
nofault_L: "succeeds L s"
by (simp add: L1_defs(5) succeeds_catch)
with L exec_L' obtain r1 where "reaches L s (Result r1) s'"
by (metis (no_types, lifting) insertE rel_L1_conv(1) refines_simpl_def singletonD xstate.distinct(3))
then show ?thesis using nofault
by (fastforce simp add: L1_catch_def succeeds_catch reaches_catch)
qed
next
fix s'
assume nofault: "succeeds (L1_catch L R) s"
assume exec: "Γ⊢ ⟨TRY L' CATCH R' END,Normal s⟩ ⇒ Abrupt s'"
then show "∃r. reaches (L1_catch L R) s (Exn r) s'"
proof (cases)
case (1 s1)
hence exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Abrupt s1" and
exec_R': "Γ⊢ ⟨R',Normal s1⟩ ⇒ Abrupt s'" .
from nofault L R exec_L' obtain
nofault_L: "succeeds L s" and
nofault_R: "succeeds R s1"
by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)
from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def
singletonD xstate.distinct(7))
from nofault_R r1 exec_R' R obtain r2 where "reaches R s1 (Exn r2) s'"
by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(2) refines_simpl_def xstate.distinct(7))
with r1 nofault show ?thesis
by (fastforce simp add: L1_catch_def succeeds_catch reaches_catch)
next
case 2
then show ?thesis by simp
qed
next
fix e
assume nofault: "succeeds (L1_catch L R) s"
assume exec: "Γ⊢ ⟨TRY L' CATCH R' END,Normal s⟩ ⇒ Fault e"
then show "e ∈ {AssumeError, StackOverflow}"
proof (cases)
case (1 s1)
hence exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Abrupt s1" and
exec_R': "Γ⊢ ⟨R',Normal s1⟩ ⇒ Fault e" .
from nofault L R exec_L' obtain
nofault_L: "succeeds L s" and
nofault_R: "succeeds R s1"
by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)
from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def
singletonD xstate.distinct(7))
from nofault_R r1 exec_R' R show ?thesis
by (metis insert_iff rel_L1_conv(3) refines_simpl_def singletonD xstate.inject(3))
next
case 2
have exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Fault e" by fact
from nofault L R exec_L' obtain
nofault_L: "succeeds L s"
by (simp add: L1_defs(5) succeeds_catch)
with L exec_L' show ?thesis
by (metis insertCI insertE rel_L1_conv(3) refines_simpl_def singleton_iff xstate.inject(3))
qed
next
assume nofault: "succeeds (L1_catch L R) s"
assume exec: "Γ⊢ ⟨TRY L' CATCH R' END,Normal s⟩ ⇒ Stuck"
then show False
proof (cases)
case (1 s1)
hence exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Abrupt s1" and
exec_R': "Γ⊢ ⟨R',Normal s1⟩ ⇒ Stuck" .
from nofault L R exec_L' obtain
nofault_L: "succeeds L s" and
nofault_R: "succeeds R s1"
by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)
from nofault_R exec_R' R show ?thesis
by (metis empty_iff insertE rel_L1_conv(4) refines_simpl_def xstate.distinct(11))
next
case 2
have exec_L': "Γ⊢ ⟨L',Normal s⟩ ⇒ Stuck" by fact
from nofault L R exec_L' obtain
nofault_L: "succeeds L s"
by (simp add: L1_defs(5) succeeds_catch)
with L exec_L' show ?thesis
by (metis insertE rel_L1_conv(4) refines_simpl_def singletonD xstate.distinct(11))
qed
qed
lemmas refines_simpl_cleanup = L1corres_refines_simpl [OF L1_corres_cleanup]
lemmas refines_simpl_cleanup_throw = L1corres_refines_simpl [OF L1_corres_cleanup_throw]
lemmas refines_simpl_spec_cleanup = L1corres_refines_simpl [OF L1_corres_spec_cleanup]
lemmas refines_simpl_spec_cleanup_throw = L1corres_refines_simpl [OF L1_corres_spec_cleanup_throw]
lemma refines_simpl_rel_L1_on_exit':
fixes m:: "'s L1_monad"
assumes m_c: "refines_simpl ct Γ c m s s rel_L1"
shows "refines_simpl ct Γ (On_Exit c (Basic cleanup)) (on_exit m {(s,t). t = cleanup s}) s s rel_L1"
unfolding on_exit_catch_conv
apply (simp add: On_Exit_def)
apply (rule refines_simpl_rel_L1_bind)
apply (simp add: L1_catch_def [symmetric])
apply (rule refines_simpl_rel_L1_catch [OF m_c])
apply (rule refines_simpl_cleanup_throw [simplified])
apply (rule refines_simpl_cleanup [simplified])
done
lemma refines_simpl_rel_L1_on_exit:
fixes m:: "'s L1_monad"
assumes m_c: "refines_simpl ct Γ c m s s rel_L1"
shows "refines_simpl ct Γ (On_Exit c (com.Spec cleanup)) (on_exit m cleanup) s s rel_L1"
apply (simp add: on_exit_catch_conv On_Exit_def)
apply (rule refines_simpl_rel_L1_bind)
apply (simp add: L1_catch_def [symmetric])
apply (rule refines_simpl_rel_L1_catch [OF m_c])
apply (rule refines_simpl_spec_cleanup_throw [simplified])
apply (rule refines_simpl_spec_cleanup [simplified])
done
named_theorems L1corres_with_fresh_stack_ptr
context stack_heap_state
begin
lemma refines_simpl_rel_L1_with_fresh_stack_ptr:
fixes m:: "'a::mem_type ptr ⇒ 's L1_monad"
assumes c_m: "⋀p s. refines_simpl ct Γ (c p) (m p) s s rel_L1"
shows "refines_simpl ct Γ (With_Fresh_Stack_Ptr n I c) (with_fresh_stack_ptr n I m) s s rel_L1"
apply (simp add: with_fresh_stack_ptr_def With_Fresh_Stack_Ptr_def)
apply (rule refines_simpl_StackOverflow)
apply (rule refines_simpl_DynCom)
apply (rule refines_simpl_rel_L1_bind)
subgoal
apply (rule refines_simpl_rel_L1I)
subgoal
by (simp add: terminates.Spec)
subgoal for s'
apply (erule exec_Normal_elim_cases)
subgoal for t
by (auto simp add: succeeds_assume_result_and_state)
by auto
subgoal for s'
by (meson exec_Normal_elim_cases(7) xstate.distinct(9) xstate.simps(5))
subgoal for e
by (meson exec_Normal_elim_cases(7) xstate.distinct(11) xstate.simps(7))
subgoal
apply (erule exec_Normal_elim_cases)
using Ex_list_of_length by auto blast
done
apply (rule refines_simpl_DynCom)
apply (clarsimp)
apply (simp add: stack_allocs_allocated_ptrs)
apply (rule refines_simpl_rel_L1_on_exit[OF c_m])
done
lemma L1corres_with_fresh_stack_ptr[L1corres_with_fresh_stack_ptr]:
fixes m:: "'a::mem_type ptr ⇒ 's L1_monad"
assumes c_m: "⋀p. L1corres ct Γ (m p) (c p)"
shows "L1corres ct Γ (with_fresh_stack_ptr n I m) (With_Fresh_Stack_Ptr n I c)"
apply (rule refines_simpl_L1corres)
apply (rule refines_simpl_rel_L1_with_fresh_stack_ptr)
apply (rule L1corres_refines_simpl)
apply (rule c_m)
done
end
definition "UNDEFINED_FUNCTION ≡ False"
definition
undefined_function_body :: "('a, int, strictc_errortype) com"
where
"undefined_function_body ≡ Guard UndefinedFunction {x. UNDEFINED_FUNCTION} SKIP"
definition
init_return_undefined_function_body::"(('a ⇒ 'a) ⇒ (('g, 'l, 'e, 'z) state_scheme ⇒ ('g, 'l, 'e, 'z) state_scheme))
⇒ (('g, 'l, 'e, 'z) state_scheme, int, strictc_errortype) com"
where
"init_return_undefined_function_body ret ≡ Seq (lvar_nondet_init ret) (Guard UndefinedFunction {x. UNDEFINED_FUNCTION} SKIP)"
lemma L1corres_undefined_call:
"L1corres ct Γ ((L1_seq (L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) L1_skip)) (Call X')"
by (clarsimp simp: L1corres_def L1_defs UNDEFINED_FUNCTION_def)
lemma L1_UNDEFINED_FUNCTION_fail: "(L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) = L1_fail"
apply (clarsimp simp add: L1_defs UNDEFINED_FUNCTION_def)
by (simp add: run_guard spec_monad_ext)
lemma L1_seq_fail: "L1_seq L1_fail X = L1_fail"
apply (clarsimp simp add: L1_defs)
done
lemma L1_seq_init_fail: "(L1_seq (L1_init ret) L1_fail) = L1_fail"
apply (clarsimp simp add: L1_defs)
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
lemma L1_corres_L1_fail: "L1corres ct Γ L1_fail X"
by (simp add: L1corres_def L1_defs)
lemma L1corres_init_return_undefined_call:
"L1corres ct Γ (L1_seq (L1_init ret) ((L1_seq (L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) L1_skip))) (Call X')"
by (simp only: L1_UNDEFINED_FUNCTION_fail L1_seq_fail L1_seq_init_fail L1_corres_L1_fail)
named_theorems L1unfold
named_theorems L1except
lemma signed_bounds_one_to_nat: "n <s 1 ⟹ 0 ≤s n ⟹ unat n = 0"
by (metis signed.leD unat_1_0 unat_gt_0 unsigned_eq_0_iff word_msb_0 word_sle_msb_le)
lemma signed_bounds_to_nat_boundsF: "n <s numeral B ⟹ 0 ≤s n ⟹ unat n < numeral B"
by (metis linorder_not_less of_nat_numeral signed.leD unat_less_helper word_msb_0 word_sle_msb_le)
lemma word_bounds_to_nat_boundsF: "(n::'a::len word) < numeral B ⟹ 0 ≤s n ⟹ unat n < numeral B"
by (simp add: unat_less_helper)
lemma word_bounds_one_to_nat: "(n::'a::len word) < 1 ⟹ 0 ≤s n ⟹ unat n = 0"
by (simp add: unat_less_helper)
lemma monotone_L1_seq_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "monotone R (≤) Y"
shows "monotone R (≤)
(λf. (L1_seq (X f) (Y f)))"
unfolding L1_defs
apply (intro partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_seq_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "monotone R (≥) Y"
shows "monotone R (≥)
(λf. (L1_seq (X f) (Y f)))"
unfolding L1_defs
apply (intro partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_catch_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "monotone R (≤) Y"
shows "monotone R (≤)
(λf. (L1_catch (X f) (Y f)))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_catch_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "monotone R (≥) Y"
shows "monotone R (≥)
(λf. (L1_catch (X f) (Y f)))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_condition_le [partial_function_mono]:
assumes mono_X: "monotone R (≤) X"
assumes mono_Y: "monotone R (≤) Y"
shows "monotone R (≤)
(λf. (L1_condition C (X f) (Y f)))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_condition_ge [partial_function_mono]:
assumes mono_X: "monotone R (≥) X"
assumes mono_Y: "monotone R (≥) Y"
shows "monotone R (≥)
(λf. (L1_condition C (X f) (Y f)))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_X)
apply (rule mono_Y)
done
lemma monotone_L1_guarded_le [partial_function_mono]:
assumes mono_X [partial_function_mono]: "monotone R (≤) X"
shows "monotone R (≤)
(λf. (L1_guarded C (X f)))"
unfolding L1_guarded_def
apply (rule partial_function_mono)+
done
lemma monotone_L1_guarded_ge [partial_function_mono]:
assumes mono_X [partial_function_mono]: "monotone R (≥) X"
shows "monotone R (≥)
(λf. (L1_guarded C (X f)))"
unfolding L1_guarded_def
apply (rule partial_function_mono)+
done
lemma monotone_L1_while_le [partial_function_mono]:
assumes mono_B: "monotone R (≤) (λf. B f)"
shows "monotone R (≤) (λf. L1_while C (B f))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_B)
done
lemma monotone_L1_while_ge [partial_function_mono]:
assumes mono_B: "monotone R (≥) (λf. B f)"
shows "monotone R (≥) (λf. L1_while C (B f))"
unfolding L1_defs
apply (rule partial_function_mono)
apply (rule mono_B)
done
lemma monotone_L1_call_le [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≤) X"
shows "monotone R (≤)
(λf. L1_call scope_setup (X f) scope_teardown result_exn return_xf)"
unfolding L1_call_def
apply (rule partial_function_mono)+
done
lemma monotone_L1_call_ge [partial_function_mono]:
assumes X[partial_function_mono]: "monotone R (≥) X"
shows "monotone R (≥)
(λf. L1_call scope_setup (X f) scope_teardown result_exn return_xf)"
unfolding L1_call_def
apply (rule partial_function_mono)+
done
end