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
lemma L1_dyn_call_const:
"(gets (λ_. dest) >>= (λp. L1_call scope_setup (𝒫 p) scope_teardown result_exn return_xf)) =
L1_call scope_setup (𝒫 dest) scope_teardown result_exn return_xf"
unfolding L1_call_def
by (rule spec_monad_eqI) (auto simp add: runs_to_iff )
definition "assume_Spec R = guarded_spec_body AssumeError R"
definition exec_spec_monad::
"('s ⇒ exit_status c_exntype) ⇒ ((exit_status c_exntype ⇒ exit_status c_exntype) ⇒ 's ⇒ 's) ⇒
('s ⇒ 't) ⇒ ('s ⇒ 'b) ⇒ ('b ⇒ (exit_status, 'a, 't) exn_monad) ⇒ (('a ⇒ 'a) ⇒ 's ⇒ 's) ⇒ ('s,'p,strictc_errortype) com" where
"exec_spec_monad get_x upd_x st args f res ≡
Guard Fail {s. succeeds (f (args s)) (st s)}
(Seq
(assume_Spec {(s0, s1).
∃x t s. reaches (f (args s0)) (st s0) x t ∧ t = st s ∧
(case x of
Exn e ⇒ s1 = upd_x (λ_. Nonlocal e) s
| Result r ⇒ s1 = upd_x (λ_. Return) (res (λ_. r) s))})
(Cond {s. is_local (get_x s)} SKIP THROW))"
lemma terminates_Guard':
assumes c: "s∈g ⟹ Γ⊢c↓(Normal s)"
shows "Γ⊢Guard f g c↓(Normal s)"
proof (cases "s ∈ g")
case True
from True c [OF True] show ?thesis by (rule terminates.Guard)
next
case False
then show ?thesis by (rule terminates.GuardFault)
qed
definition L1_exec_spec_monad::
"((exit_status c_exntype ⇒ exit_status c_exntype) ⇒ 's ⇒ 's) ⇒
('s ⇒ 't) ⇒ ('s ⇒ 'b) ⇒ ('b ⇒ (exit_status, 'a, 't) exn_monad) ⇒ (('a ⇒ 'a) ⇒ 's ⇒ 's) ⇒ 's L1_monad" where
"L1_exec_spec_monad upd_x st args f res ≡
do {
a <- gets (args);
bind_handle (exec_abstract st (f a))
(λr. L1_seq (L1_modify (res (λ_. r))) (L1_modify (upd_x (λ_. Return))))
(λe. L1_seq (L1_modify (upd_x (λ_. Nonlocal (the e)))) L1_throw)} "
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_le_trans[corres_le_trans]: "L1corres ct Γ A C ⟹ A ≤ A' ⟹ L1corres ct Γ A' C"
apply (auto simp add: L1corres_def)
subgoal
using le_succeedsD le_reachesD
by (fastforce split: xstate.splits )
subgoal
using le_succeedsD le_reachesD
by (fastforce split: xstate.splits simp add: )
done
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_Guard_maybe_guard:
"L1corres ct Γ B (Guard f g B') ⟹ L1corres ct Γ 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
lemma L1corres_guarded:
assumes B: "L1corres ct Γ B B'"
shows "L1corres ct Γ (L1_guarded g B) B'"
using B
by (auto simp add: L1corres_def L1_guarded_def L1_seq_def L1_guard_def
succeeds_bind reaches_bind split: xstate.splits)
lemma L1corres_guarded_DynCom_conseq1:
assumes corres_B: "⋀s. g s ⟹ L1corres ct Γ (B s) (Guard f {s'. s ∈ g'} (B' s))"
shows "L1corres ct Γ (L1_guarded g (gets B ⤜ (λb. b))) (Guard f g' (DynCom B'))"
using corres_B
apply (simp add: L1corres_def L1_guarded_def L1_seq_def L1_guard_def)
apply (auto simp add: succeeds_bind reaches_bind split: xstate.splits )
subgoal
by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
subgoal
by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
subgoal
by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
subgoal
by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
subgoal for s
apply (cases "s ∈ g'")
apply (fastforce elim!: terminates_Normal_elim_cases
elim: terminates.GuardFault intro: terminates.intros)+
done
done
lemma L1corres_guarded_DynCom_conseq2:
assumes corres_B: "⋀s. g s ⟹ L1corres ct Γ (B s) (Guard f {s'. s ∈ g'} (B' s))"
shows "L1corres ct Γ (L1_guarded g (gets B ⤜ (λb. b))) (maybe_guard f g' (DynCom B'))"
apply (rule L1corres_Guard_maybe_guard)
using corres_B
by (rule L1corres_guarded_DynCom_conseq1)
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 ⇒ if ft ∈ {AssumeError, StackOverflow} then bot else 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 )+
subgoal
apply (auto split: xstate.splits simp add: reaches_bind succeeds_bind)
apply (smt (verit, ccfv_threshold) image_eqI mem_Collect_eq succeeds_fail_iff)+
done
subgoal
apply (auto split: xstate.splits simp add: reaches_bind succeeds_bind)
done
done
subgoal for s
apply (auto intro!: terminates.intros simp add: succeeds_bind reaches_bind)
done
done
lemma L1_call_simpl_le_trans:
assumes "L1corres ct Γ P (Call proc)"
shows "(L1_call_simpl ct Γ proc) ≤ P"
using assms
apply (simp add: le_spec_monad_le_refines_iff L1corres_def L1_call_simpl_def)
apply (auto simp add: refines_def_old)
subgoal
by (fastforce simp add: succeeds_bind split: xstate.splits)
subgoal
by (auto simp add: succeeds_bind reaches_bind split: xstate.splits)
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 L1corres_guarded_spec_pre_post:
"L1corres ct Γ (L1_spec R) (guarded_spec_pre_post F_pre F_post R)"
apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_spec_def guarded_spec_pre_post_def)
apply (force simp: liftE_def bind_def
elim: exec_Normal_elim_cases intro: terminates.Guard terminates.Spec)
done
lemma L1corres_assume_guarded_spec_pre_post:
"L1corres ct Γ
(L1_seq (L1_guard (λs. s ∈ fst ` R)) ((L1_assume (L1_rel_to_fun R))))
(guarded_spec_pre_post F_pre AssumeError R)"
apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def
L1_seq_def L1_guard_def L1_rel_to_fun_alt guarded_spec_pre_post_def)
apply (force elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def)
done
lemma L1corres_assume_spec_pre_post:
"L1corres ct Γ
(L1_seq (L1_guard (λs. s ∈ P)) ((L1_assume (L1_rel_to_fun R))))
(spec_pre_post F_pre AssumeError P R)"
apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def
L1_seq_def L1_guard_def L1_rel_to_fun_alt spec_pre_post_def)
apply (auto elim!: exec_Normal_elim_cases
intro: terminates.intros
split: xstate.splits
simp add: succeeds_bind reaches_bind Exn_def terminates.Spec terminates_Guard')
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
definition "L1_dyn_call_simpl ct Γ g scope_setup (dest :: 's ⇒ unit ptr) scope_teardown result_exn return_xf ≡
L1_guarded g (gets dest >>= (λp. L1_call scope_setup (L1_call_simpl ct Γ p) scope_teardown result_exn return_xf))"
lemma L1corres_dyn_call_simpl_conseq:
assumes conseq: "⋀s. g s ⟹ s ∈ g'"
shows
"L1corres ct Γ
(L1_dyn_call_simpl ct Γ 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 (L1_call_simpl ct Γ (dest s)) scope_teardown_norm scope_teardown_exn result) ⤜ (λb. b)) =
(gets dest ⤜ (λp. L1_call scope_setup (L1_call_simpl ct Γ 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_simpl_def dynCall_exn_def)
apply (rule L1corres_guarded_DynCom_conseq [where B = "λs. L1_call scope_setup (L1_call_simpl ct Γ (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
apply (simp add: conseq)
apply (rule L1corres_call)
apply (rule L1corres_call_simpl)
done
qed
definition "L1_dyn_call_map_of_default g scope_setup (dest :: 's ⇒ unit ptr) ps scope_teardown result_exn return_xf ≡
L1_guarded g (gets dest >>= (λp. L1_call scope_setup (map_of_default (λ_. ⊤) ps p) scope_teardown result_exn return_xf))"
lemma map_of_default_witness: "p ∈ set (map fst ps) ⟹ ∃f. (p,f) ∈ set ps ∧ map_of_default d ps p = f"
by (induct ps) auto
lemma list_all_prod_witness: "list_all (λ(x, v). P x v) xs ⟹ (x, v) ∈ set xs ⟹ P x v"
by (induct xs) auto
lemma L1corres_Guard_UNIV: "L1corres ct Γ X C ==> L1corres ct Γ X (Guard f UNIV C)"
by (simp add: L1corres_alt_def ccorresE_Guard)
lemma L1corres_dyn_call_map_of_default_conseq:
assumes conseq: "⋀s. g' s ⟹ dest s ∈ set (map fst ps) ⟹ s ∈ g"
assumes ps: "list_all (λ(p, f). L1corres ct Γ f (Call p)) ps"
shows
"L1corres ct Γ
(L1_dyn_call_map_of_default g' scope_setup dest ps 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 (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm scope_teardown_exn result) ⤜ (λb. b)) =
(gets dest ⤜ (λp. L1_call scope_setup (map_of_default (λ_. ⊤) ps 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_map_of_default_def dynCall_exn_def)
apply (rule L1corres_guarded_DynCom_conseq2 [where B = "λs. L1_call scope_setup (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
subgoal premises prems for s
proof (cases "dest s ∈ set (map fst ps)")
case True
from map_of_default_witness [OF True] obtain f where
elem: "(dest s,f) ∈ set ps" and eq: "map_of_default (λ_. ⊤) ps (dest s) = f"
by blast
from list_all_prod_witness [OF ps elem]
have "L1corres ct Γ f (Call (dest s))" .
moreover from True prems conseq have "s ∈ g" by blast
ultimately show ?thesis
apply (simp add: eq)
apply (rule L1corres_Guard_UNIV)
apply (rule L1corres_call)
apply assumption
done
next
case False
then have "(map_of_default (λ_. ⊤) ps (dest s)) = ⊤"
by (simp add: map_of_default_fallthrough)
hence "(L1_call scope_setup (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm
scope_teardown_exn result) = ⊤"
apply simp
apply (simp add: L1_call_def)
apply (rule spec_monad_eqI)
apply (auto simp add: runs_to_iff)
done
then show ?thesis by (simp add: L1corres_top)
qed
done
qed
lemma L1corres_dyn_call_simpl:
assumes eq: "L1_set_to_pred g ≡ g'"
shows
"L1corres ct Γ
(L1_dyn_call_simpl ct Γ 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_simpl_conseq)
apply (simp add: eq [symmetric])
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
lemma L1corres_exec_spec_monad:
assumes l: "lense get_x upd_x"
shows "L1corres ct Γ (L1_exec_spec_monad upd_x st args f res) (exec_spec_monad get_x upd_x st args f res)"
proof -
from l interpret l: lense get_x upd_x .
show ?thesis
proof (clarsimp simp add: L1corres_def; safe)
fix s t
assume succeeds: "succeeds (L1_exec_spec_monad upd_x st args f res) s"
assume exec: "Γ⊢ ⟨exec_spec_monad get_x upd_x st args f res,Normal s⟩ ⇒ t"
show "case t of
Normal x ⇒
reaches (L1_exec_spec_monad upd_x st args f res) s (Result ()) x
| Abrupt x ⇒ reaches (L1_exec_spec_monad upd_x st args f res) s (Exn ()) x
| Fault e ⇒ e ∈ {AssumeError, StackOverflow} | Stuck ⇒ False"
proof -
from succeeds exec show ?thesis
apply (simp add: L1_exec_spec_monad_def exec_spec_monad_def)
apply (erule exec_Normal_elim_cases)
subgoal
apply (auto simp add: succeeds_bind succeeds_bind_handle)
apply (erule exec_Normal_elim_cases)
apply (simp add: assume_Spec_def guarded_spec_body_def)
apply (erule exec_Normal_elim_cases)
subgoal for s'
apply auto
apply (erule exec_Normal_elim_cases)
subgoal for b x1 s1 t1
apply clarsimp
subgoal for x2 s2
apply (erule allE [where x="x2"])
apply (erule allE [where x="s2"])
apply (clarsimp simp add: reaches_exec_abstract)
apply (fastforce split: xval_splits
simp add: default_option_def L1_exec_spec_monad_def reaches_bind
L1_modify_def L1_seq_def L1_throw_def
case_exception_or_result_iff succeeds_bind
reaches_exec_abstract reaches_bind_handle succeeds_bind succeeds_bind_handle
elim!: exec_Normal_elim_cases)
done
done
subgoal
by clarsimp
done
subgoal
apply clarsimp
apply (erule exec_Normal_elim_cases)
apply (auto simp add: L1_exec_spec_monad_def reaches_bind )
done
done
subgoal
by (auto simp add: succeeds_bind succeeds_bind_handle)
done
qed
next
fix s
assume succeeds: "succeeds (L1_exec_spec_monad upd_x st args f res) s"
assume "ct"
show "Γ⊢exec_spec_monad get_x upd_x st args f res ↓ Normal s"
proof -
from succeeds show ?thesis
apply (auto simp add: L1_exec_spec_monad_def exec_spec_monad_def succeeds_bind_handle succeeds_bind reaches_exec_abstract)
apply (rule terminates.intros)
subgoal by blast
apply (rule terminates.intros)
subgoal
apply (simp add: assume_Spec_def guarded_spec_body_def)
apply (rule terminates_Guard')
apply (rule terminates.intros)
done
subgoal
apply (clarsimp simp add: assume_Spec_def guarded_spec_body_def)
apply (erule exec_Normal_elim_cases)
subgoal
apply (auto split: xval_splits)
by (metis (lifting) Abrupt Fault Stuck terminates.CondFalse terminates.CondTrue
terminates.Throw terminates_Skip' terminates_elim_cases(1))
subgoal
by (auto)
done
done
qed
qed
qed
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 ⟹ unat n < numeral B"
by (simp add: unat_less_helper)
lemma word_bounds_one_to_nat: "(n::'a::len word) < 1 ⟹ 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 L1_seq_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"g1 ≤ g2" "f1 ≤ f2" shows "L1_seq f1 g1 ≤ L1_seq f2 g2"
unfolding L1_defs
by (intro monad_mono_intros le_funI)
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 L1_catch_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"f1 ≤ f2" "g1 ≤ g2" shows "L1_catch f1 g1 ≤ L1_catch f2 g2"
unfolding L1_defs
by (intro monad_mono_intros le_funI)
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 L1_condition_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"f1 ≤ f2" "g1 ≤ g2" shows "L1_condition c f1 g1 ≤ L1_condition c f2 g2"
unfolding L1_defs
by (intro monad_mono_intros le_funI)
lemma monotone_guard: "monotone R (≥) C ⟹ monotone R (≤) (λf. guard (C f))"
apply (auto simp add: monotone_def guard_def assert_def)
apply (rule mono_bind)
apply (auto simp add: le_fun_def )
done
lemma monotone_L1_guard: "monotone R (≥) C ⟹ monotone R (≤) (λf. L1_guard (C f))"
unfolding L1_guard_def
by (rule monotone_guard)
lemma monotone_L1_guarded_le [partial_function_mono]:
assumes mono_X [partial_function_mono]: "monotone R (≥) C" "monotone R (≤) X"
shows "monotone R (≤)
(λf. (L1_guarded (C f) (X f)))"
unfolding L1_guarded_def
apply (rule partial_function_mono monotone_L1_guard)+
done
thm monotone_def
lemma monotone_guard': "(⋀s. monotone R (≤) (λf. C f s)) ⟹ monotone R (≥) (λf. guard (C f))"
apply (auto simp add: monotone_def guard_def assert_def)
apply (rule mono_bind)
apply (auto simp add: le_fun_def )
done
lemma monotone_guard'': "(monotone R (fun_ord (≤)) (λf s. C f s)) ⟹ monotone R (≥) (λf. guard (C f))"
apply (auto simp add: monotone_def guard_def assert_def)
apply (rule mono_bind)
apply (auto simp add: le_fun_def fun_ord_def)
done
lemma monotone_L1_guard': "(⋀s. monotone R (≤) (λf. C f s)) ⟹ monotone R (≥) (λf. L1_guard (C f))"
unfolding L1_guard_def
by (rule monotone_guard')
lemma monotone_L1_guard'': "(monotone R (fun_ord (≤)) (λf s. C f s)) ⟹ monotone R (≥) (λf. L1_guard (C f))"
unfolding L1_guard_def
by (rule monotone_guard'')
lemma monotone_L1_guarded_ge' [partial_function_mono ]:
assumes mono_X [partial_function_mono]: "(⋀s. monotone R (≤) (λf. C f s))" "monotone R (≥) X"
shows "monotone R (≥)
(λf. (L1_guarded (C f) (X f)))"
unfolding L1_guarded_def
apply (rule partial_function_mono monotone_L1_guard')+
done
lemma L1_guarded_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"f ≤ g" shows "L1_guarded c f ≤ L1_guarded c g"
unfolding L1_defs L1_guarded_def
by (intro monad_mono_intros le_funI order.refl)
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 L1_while_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"f ≤ g" shows "L1_while c f ≤ L1_while c g"
unfolding L1_defs
by (intro monad_mono_intros le_funI)
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
lemma L1_call_mono [monad_mono_intros]:
assumes [monad_mono_intros]:"f ≤ g"
shows "L1_call scope_setup f scope_teardown result_exn result_xf ≤ L1_call scope_setup g scope_teardown result_exn result_xf"
unfolding L1_defs L1_call_def
by (intro monad_mono_intros le_funI order.refl)
lemma monotone_L1_dyn_call_map_of_default_le [partial_function_mono]:
assumes [partial_function_mono]: "⋀x. monotone R (≤) (λf. map_of_default (λ_. ⊤) (ps f) x)"
shows "monotone R (≤)
(λf. L1_dyn_call_map_of_default g scope_setup dest (ps f) scope_teardown result_exn return_xf)"
unfolding L1_dyn_call_map_of_default_def
by (intro partial_function_mono)
lemma monotone_L1_dyn_call_map_of_default_ge [partial_function_mono]:
assumes [partial_function_mono]: "⋀x. monotone R (≥) (λf. map_of_default (λ_. ⊤) (ps f) x)"
shows "monotone R (≥)
(λf. L1_dyn_call_map_of_default g scope_setup dest (ps f) scope_teardown result_exn return_xf)"
unfolding L1_dyn_call_map_of_default_def
by (intro partial_function_mono)
lemma L1_dyn_call_map_of_default [monad_mono_intros]:
assumes [monad_mono_intros]: "⋀x. map_of_default (λ_. ⊤) ps x ≤ map_of_default (λ_. ⊤) qs x"
shows "L1_dyn_call_map_of_default g scope_setup dest ps scope_teardown result_exn result_xf ≤ L1_dyn_call_map_of_default g scope_setup dest qs scope_teardown result_exn result_xf"
unfolding L1_dyn_call_map_of_default_def
by (intro monad_mono_intros le_funI order.refl)
end