lib+ainvs: pull up more empty_fail lemmas
- pull base-level empty_fail lemmas from AInvs into Monads.Empty_Fail - apply consistent naming - apply consistent [intro!, wp] - make all non-conditional lemmas [simp] - re-add context building to empty_fail rules, because the select_* rules may need context to solve their side condition Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
parent
a6e2d73e72
commit
549cb893de
|
|
@ -64,134 +64,267 @@ subsection \<open>Wellformed monads\<close>
|
|||
(*
|
||||
Collect generic empty_fail lemmas here:
|
||||
- naming convention is emtpy_fail_NAME.
|
||||
- add all new lemmas to [empty_fail] set, unless they have side conditions
|
||||
that are not [empty_fail]
|
||||
- add lemmas with assumptions to [empty_fail_cond] set
|
||||
- add lemmas without assumption to [empty_fail_term] set
|
||||
*)
|
||||
|
||||
named_theorems empty_fail
|
||||
named_theorems empty_fail_term
|
||||
named_theorems empty_fail_cond
|
||||
|
||||
lemma empty_fail_modify[empty_fail]:
|
||||
lemma empty_fail_K_bind[empty_fail_cond]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (K_bind f x)"
|
||||
by simp
|
||||
|
||||
lemma empty_fail_fun_app[empty_fail_cond]:
|
||||
"empty_fail (f x) \<Longrightarrow> empty_fail (f $ x)"
|
||||
by simp
|
||||
|
||||
(* empty_fail as such does not need context, but empty_fail_select_f does, so we need to build
|
||||
up context in other rules *)
|
||||
lemma empty_fail_If[empty_fail_cond]:
|
||||
"\<lbrakk> P \<Longrightarrow> empty_fail f; \<not>P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
|
||||
by (simp split: if_split)
|
||||
|
||||
lemma empty_fail_If_applied[empty_fail_cond]:
|
||||
"\<lbrakk> P \<Longrightarrow> empty_fail (f x); \<not>P \<Longrightarrow> empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail ((if P then f else g) x)"
|
||||
by simp
|
||||
|
||||
lemma empty_fail_put[empty_fail_term]:
|
||||
"empty_fail (put f)"
|
||||
by (simp add: put_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_modify[empty_fail_term]:
|
||||
"empty_fail (modify f)"
|
||||
by (simp add: empty_fail_def simpler_modify_def)
|
||||
|
||||
lemma empty_fail_gets[empty_fail]:
|
||||
lemma empty_fail_gets[empty_fail_term]:
|
||||
"empty_fail (gets f)"
|
||||
by (simp add: empty_fail_def simpler_gets_def)
|
||||
|
||||
(* Not in empty_fail set, because it has a non-[empty_fail] side condition *)
|
||||
lemma empty_fail_select_f:
|
||||
lemma empty_fail_select[empty_fail_cond]:
|
||||
"S \<noteq> {} \<Longrightarrow> empty_fail (select S)"
|
||||
by (simp add: empty_fail_def select_def)
|
||||
|
||||
lemma empty_fail_select_f[empty_fail_cond]:
|
||||
assumes ef: "fst S = {} \<Longrightarrow> snd S"
|
||||
shows "empty_fail (select_f S)"
|
||||
by (fastforce simp add: empty_fail_def select_f_def intro: ef)
|
||||
|
||||
lemma empty_fail_bind[empty_fail]:
|
||||
lemma empty_fail_bind[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
|
||||
by (fastforce simp: bind_def empty_fail_def split_def)
|
||||
|
||||
lemma empty_fail_return[empty_fail]:
|
||||
lemma empty_fail_return[empty_fail_term]:
|
||||
"empty_fail (return x)"
|
||||
by (simp add: empty_fail_def return_def)
|
||||
|
||||
lemma empty_fail_error_bits[empty_fail]:
|
||||
lemma empty_fail_returnOk[empty_fail_term]:
|
||||
"empty_fail (returnOk v)"
|
||||
"empty_fail (throwError v)"
|
||||
"empty_fail (liftE f) = empty_fail f"
|
||||
by (fastforce simp: returnOk_def throwError_def liftE_def empty_fail_def bind_def return_def)+
|
||||
by (fastforce simp: returnOk_def empty_fail_term)
|
||||
|
||||
lemma empty_fail_lift[empty_fail]:
|
||||
lemma empty_fail_throwError[empty_fail_term]:
|
||||
"empty_fail (throwError v)"
|
||||
by (fastforce simp: throwError_def empty_fail_term)
|
||||
|
||||
lemma empty_fail_lift[empty_fail_cond]:
|
||||
"\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)"
|
||||
unfolding lift_def
|
||||
by (auto simp: empty_fail split: sum.split)
|
||||
by (auto simp: empty_fail_term split: sum.split)
|
||||
|
||||
lemma empty_fail_bindE[empty_fail]:
|
||||
lemma empty_fail_liftE[empty_fail_cond]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (liftE f)"
|
||||
by (simp add: liftE_def empty_fail_cond empty_fail_term)
|
||||
|
||||
lemma empty_fail_bindE[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
|
||||
by (simp add: bindE_def empty_fail)
|
||||
by (simp add: bindE_def empty_fail_cond)
|
||||
|
||||
lemma empty_fail_If[empty_fail]:
|
||||
"\<lbrakk> empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
|
||||
by (simp split: if_split)
|
||||
|
||||
lemma empty_fail_mapM[empty_fail]:
|
||||
assumes m: "\<And>x. empty_fail (m x)"
|
||||
lemma empty_fail_mapM[empty_fail_cond]:
|
||||
assumes m: "\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)"
|
||||
shows "empty_fail (mapM m xs)"
|
||||
using m
|
||||
proof (induct xs)
|
||||
case Nil
|
||||
thus ?case by (simp add: mapM_def sequence_def empty_fail)
|
||||
thus ?case by (simp add: mapM_def sequence_def empty_fail_term)
|
||||
next
|
||||
case Cons
|
||||
have P: "\<And>m x xs. mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)"
|
||||
by (simp add: mapM_def sequence_def Let_def)
|
||||
from Cons
|
||||
show ?case by (simp add: P m empty_fail)
|
||||
show ?case by (simp add: P m empty_fail_cond empty_fail_term)
|
||||
qed
|
||||
|
||||
lemma empty_fail_fail[empty_fail]:
|
||||
lemma empty_fail_fail[empty_fail_term]:
|
||||
"empty_fail fail"
|
||||
by (simp add: fail_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_assert[empty_fail]:
|
||||
lemma empty_fail_assert[empty_fail_term]:
|
||||
"empty_fail (assert P)"
|
||||
unfolding assert_def by (simp add: empty_fail)
|
||||
unfolding assert_def by (simp add: empty_fail_term)
|
||||
|
||||
lemma empty_fail_assert_opt[empty_fail]:
|
||||
lemma empty_fail_assert_opt[empty_fail_term]:
|
||||
"empty_fail (assert_opt x)"
|
||||
by (simp add: assert_opt_def empty_fail split: option.splits)
|
||||
by (simp add: assert_opt_def empty_fail_term split: option.splits)
|
||||
|
||||
lemma empty_fail_mk_ef[empty_fail]:
|
||||
lemma empty_fail_mk_ef[empty_fail_term]:
|
||||
"empty_fail (mk_ef o m)"
|
||||
by (simp add: empty_fail_def mk_ef_def)
|
||||
|
||||
lemma empty_fail_gets_map[empty_fail]:
|
||||
lemma empty_fail_gets_the[empty_fail_term]:
|
||||
"empty_fail (gets_the f)"
|
||||
unfolding gets_the_def
|
||||
by (simp add: empty_fail_cond empty_fail_term)
|
||||
|
||||
lemma empty_fail_gets_map[empty_fail_term]:
|
||||
"empty_fail (gets_map f p)"
|
||||
unfolding gets_map_def by (simp add: empty_fail)
|
||||
unfolding gets_map_def
|
||||
by (simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_whenEs[empty_fail]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (whenE P f)"
|
||||
"empty_fail f \<Longrightarrow> empty_fail (unlessE P f)"
|
||||
by (auto simp add: whenE_def unlessE_def empty_fail)
|
||||
lemma empty_fail_whenEs[empty_fail_cond]:
|
||||
"(P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)"
|
||||
"(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f)"
|
||||
by (auto simp add: whenE_def unlessE_def empty_fail_term)
|
||||
|
||||
lemma empty_fail_assertE[empty_fail]:
|
||||
lemma empty_fail_assertE[empty_fail_term]:
|
||||
"empty_fail (assertE P)"
|
||||
by (simp add: assertE_def empty_fail split: if_split)
|
||||
by (simp add: assertE_def empty_fail_term)
|
||||
|
||||
lemma empty_fail_get[empty_fail]:
|
||||
lemma empty_fail_get[empty_fail_term]:
|
||||
"empty_fail get"
|
||||
by (simp add: empty_fail_def get_def)
|
||||
|
||||
lemma empty_fail_catch[empty_fail]:
|
||||
lemma empty_fail_catch[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
|
||||
by (simp add: catch_def empty_fail split: sum.split)
|
||||
by (simp add: catch_def empty_fail_cond empty_fail_term split: sum.split)
|
||||
|
||||
lemma empty_fail_select[empty_fail]:
|
||||
"empty_fail (select V) = (V \<noteq> {})"
|
||||
by (clarsimp simp: select_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_guard[empty_fail]:
|
||||
lemma empty_fail_guard[empty_fail_term]:
|
||||
"empty_fail (state_assert G)"
|
||||
by (clarsimp simp: state_assert_def empty_fail)
|
||||
by (clarsimp simp: state_assert_def empty_fail_cond empty_fail_term)
|
||||
|
||||
lemma empty_fail_spec[empty_fail]:
|
||||
lemma empty_fail_spec[empty_fail_term]:
|
||||
"empty_fail (state_select F)"
|
||||
by (clarsimp simp: state_select_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_when[empty_fail]:
|
||||
"empty_fail x \<Longrightarrow> empty_fail (when P x)"
|
||||
unfolding when_def by (simp add: empty_fail)
|
||||
lemma empty_fail_when[empty_fail_cond]:
|
||||
"(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
|
||||
unfolding when_def
|
||||
by (simp add: empty_fail_term)
|
||||
|
||||
lemma empty_fail_unless[empty_fail]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (unless P f)"
|
||||
by (simp add: unless_def empty_fail)
|
||||
lemma empty_fail_unless[empty_fail_cond]:
|
||||
"(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unless P f)"
|
||||
unfolding unless_def
|
||||
by (simp add: empty_fail_cond)
|
||||
|
||||
lemma empty_fail_liftM[empty_fail]:
|
||||
lemma empty_fail_liftM[empty_fail_cond]:
|
||||
"empty_fail m \<Longrightarrow> empty_fail (liftM f m)"
|
||||
unfolding liftM_def
|
||||
by (fastforce simp: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_liftME[empty_fail_cond]:
|
||||
"empty_fail m \<Longrightarrow> empty_fail (liftME f m)"
|
||||
unfolding liftME_def
|
||||
by (simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_handleE[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail L; \<And>r. empty_fail (R r) \<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)"
|
||||
by (clarsimp simp: handleE_def handleE'_def empty_fail_term empty_fail_cond split: sum.splits)
|
||||
|
||||
lemma empty_fail_handle'[empty_fail_cond]:
|
||||
"\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler)"
|
||||
unfolding handleE'_def
|
||||
by (fastforce simp: empty_fail_term empty_fail_cond split: sum.splits)
|
||||
|
||||
lemma empty_fail_sequence[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms)"
|
||||
unfolding sequence_def
|
||||
by (induct ms; simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_sequence_x[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ms)"
|
||||
unfolding sequence_x_def
|
||||
by (induct ms; simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_sequenceE[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms)"
|
||||
unfolding sequenceE_def
|
||||
by (induct ms; simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_sequenceE_x[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms)"
|
||||
unfolding sequenceE_x_def
|
||||
by (induct ms; simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_mapM_x[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x f ms)"
|
||||
unfolding mapM_x_def
|
||||
by (fastforce intro: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_mapME[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME f xs)"
|
||||
unfolding mapME_def
|
||||
by (fastforce intro: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_mapME_x[empty_fail_cond]:
|
||||
"(\<And>m'. m' \<in> f ` set xs \<Longrightarrow> empty_fail m') \<Longrightarrow> empty_fail (mapME_x f xs)"
|
||||
unfolding mapME_x_def
|
||||
by (fastforce intro: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_filterM[empty_fail_cond]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)"
|
||||
by (induct ms; simp add: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_zipWithM_x[empty_fail_cond]:
|
||||
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys)"
|
||||
unfolding zipWithM_x_def zipWith_def
|
||||
by (fastforce intro: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_zipWithM[empty_fail_cond]:
|
||||
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys)"
|
||||
unfolding zipWithM_def zipWith_def
|
||||
by (fastforce intro: empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_ifM[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifM P a b)"
|
||||
by (simp add: ifM_def empty_fail_cond)
|
||||
|
||||
lemma empty_fail_whenM[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail P; empty_fail f \<rbrakk> \<Longrightarrow> empty_fail (whenM P f)"
|
||||
by (simp add: whenM_def empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_andM[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (andM A B)"
|
||||
by (simp add: andM_def empty_fail_term empty_fail_cond)
|
||||
|
||||
lemma empty_fail_orM[empty_fail_cond]:
|
||||
"\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (orM A B)"
|
||||
by (simp add: orM_def empty_fail_term empty_fail_cond)
|
||||
|
||||
(* not everything [simp] by default, because side conditions can slow down simp a lot *)
|
||||
lemmas empty_fail[wp, intro!] = empty_fail_term empty_fail_cond
|
||||
lemmas [simp] = empty_fail_term
|
||||
|
||||
|
||||
subsection \<open>Equations and legacy names\<close>
|
||||
|
||||
lemma empty_fail_select_eq[simp]:
|
||||
"empty_fail (select V) = (V \<noteq> {})"
|
||||
by (clarsimp simp: select_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_liftM_eq[simp]:
|
||||
"empty_fail (liftM f m) = empty_fail m"
|
||||
unfolding liftM_def
|
||||
by (fastforce dest: empty_fail_bindD1 simp: empty_fail)
|
||||
by (fastforce dest: empty_fail_bindD1)
|
||||
|
||||
lemma empty_fail_handleE[empty_fail]:
|
||||
"\<lbrakk> empty_fail L; \<And>r. empty_fail (R r) \<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)"
|
||||
by (clarsimp simp: handleE_def handleE'_def empty_fail split: sum.splits)
|
||||
lemma empty_fail_liftE_eq[simp]:
|
||||
"empty_fail (liftE f) = empty_fail f"
|
||||
by (fastforce simp: liftE_def empty_fail_def bind_def)
|
||||
|
||||
lemma liftME_empty_fail_eq[simp]:
|
||||
"empty_fail (liftME f m) = empty_fail m"
|
||||
unfolding liftME_def
|
||||
by (fastforce dest: empty_fail_bindD1 simp: bindE_def)
|
||||
|
||||
declare empty_fail[simp, intro!, wp]
|
||||
(* legacy name binding *)
|
||||
lemmas empty_fail_error_bits = empty_fail_returnOk empty_fail_throwError empty_fail_liftE_eq
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -945,17 +945,18 @@ lemmas hoare_wp_splits[wp_split] =
|
|||
|
||||
lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE hoare_wp_combs
|
||||
|
||||
(* rules towards the bottom will be matched first *)
|
||||
lemmas [wp] = hoare_vcg_prop
|
||||
wp_post_taut
|
||||
hoare_fun_app_wp
|
||||
return_wp
|
||||
returnOk_E
|
||||
liftE_validE_E
|
||||
put_wp
|
||||
get_wp
|
||||
gets_wp
|
||||
modify_wp
|
||||
return_wp
|
||||
returnOk_wp
|
||||
returnOk_E
|
||||
liftE_validE_E
|
||||
throwError_wp
|
||||
fail_wp
|
||||
failE_wp
|
||||
|
|
|
|||
|
|
@ -441,7 +441,7 @@ proof (clarsimp simp: exs_valid_def Bex_def)
|
|||
by (metis \<open>P s\<close> fst_conv init_T snd_conv final_I fst_whileLoop_cond_false)
|
||||
qed
|
||||
|
||||
lemma empty_fail_whileLoop:
|
||||
lemma empty_fail_whileLoop[empty_fail_cond, intro!, wp]:
|
||||
assumes body_empty_fail: "\<And>r. empty_fail (B r)"
|
||||
shows "empty_fail (whileLoop C B r)"
|
||||
proof -
|
||||
|
|
@ -470,14 +470,10 @@ proof -
|
|||
by (clarsimp simp: empty_fail_def)
|
||||
qed
|
||||
|
||||
lemma empty_fail_whileLoopE:
|
||||
assumes body_empty_fail: "\<And>r. empty_fail (B r)"
|
||||
lemma empty_fail_whileLoopE[empty_fail_cond, intro!, wp]:
|
||||
assumes "\<And>r. empty_fail (B r)"
|
||||
shows "empty_fail (whileLoopE C B r)"
|
||||
apply (clarsimp simp: whileLoopE_def)
|
||||
apply (rule empty_fail_whileLoop)
|
||||
apply (insert body_empty_fail)
|
||||
apply (clarsimp simp: empty_fail_def lift_def throwError_def return_def split: sum.splits)
|
||||
done
|
||||
by (clarsimp simp: whileLoopE_def assms)
|
||||
|
||||
lemma empty_fail_whileM[empty_fail_cond, intro!, wp]:
|
||||
"\<lbrakk> empty_fail C; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (whileM C B)"
|
||||
|
|
|
|||
|
|
@ -168,11 +168,9 @@ lemma submonad_bind:
|
|||
apply (subst select_f_stateAssert, assumption)
|
||||
apply (subst gets_stateAssert)
|
||||
apply (subst bind_subst_lift [OF stateAssert_stateAssert])
|
||||
apply (clarsimp simp: pred_conj_def)
|
||||
apply (clarsimp simp: bind_assoc split_def select_f_walk
|
||||
empty_fail_stateAssert empty_failD
|
||||
bind_subst_lift[OF modify_modify] submonad_args.args o_def
|
||||
bind_subst_lift[OF bind_select_f_bind])
|
||||
apply (clarsimp simp: bind_assoc split_def select_f_walk empty_failD pred_conj_def
|
||||
bind_subst_lift[OF modify_modify] submonad_args.args o_def
|
||||
bind_subst_lift[OF bind_select_f_bind])
|
||||
done
|
||||
|
||||
lemma (in submonad) guard_preserved:
|
||||
|
|
@ -275,7 +273,7 @@ proof (induct l)
|
|||
using sm sm' efm
|
||||
apply (simp add: mapM_Cons)
|
||||
apply (simp add: bind_subst_lift [OF submonad.stateAssert_fn])
|
||||
apply (simp add: bind_assoc submonad_bind submonad.return)
|
||||
apply (simp add: bind_assoc submonad_bind submonad.return empty_fail_cond)
|
||||
apply (subst submonad.fn_stateAssert [OF sm'])
|
||||
apply (intro ext bind_apply_cong [OF refl])
|
||||
apply (subgoal_tac "g sta")
|
||||
|
|
|
|||
|
|
@ -13,61 +13,7 @@ requalify_facts
|
|||
ef_machine_op_lift
|
||||
end
|
||||
|
||||
lemmas [wp] = empty_fail_bind empty_fail_bindE empty_fail_get empty_fail_modify
|
||||
empty_fail_whenEs empty_fail_when empty_fail_gets empty_fail_assertE
|
||||
empty_fail_error_bits empty_fail_mapM_x empty_fail_mapM empty_fail_sequence_x
|
||||
ef_ignore_failure ef_machine_op_lift
|
||||
lemmas empty_fail_error_bits[simp]
|
||||
|
||||
lemma sequence_empty_fail[wp]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms)"
|
||||
apply (induct ms)
|
||||
apply (simp add: sequence_def | wp)+
|
||||
done
|
||||
|
||||
lemma sequenceE_empty_fail[wp]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms)"
|
||||
apply (induct ms)
|
||||
apply (simp add: sequenceE_def | wp)+
|
||||
done
|
||||
|
||||
lemma sequenceE_x_empty_fail[wp]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms)"
|
||||
apply (induct ms)
|
||||
apply (simp add: sequenceE_x_def | wp)+
|
||||
done
|
||||
|
||||
lemma mapME_empty_fail[wp]:
|
||||
"(\<And>x. empty_fail (m x)) \<Longrightarrow> empty_fail (mapME m xs)"
|
||||
by (clarsimp simp: mapME_def image_def | wp)+
|
||||
|
||||
lemma mapME_x_empty_fail[wp]:
|
||||
"(\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (mapME_x f xs)"
|
||||
by (clarsimp simp: mapME_x_def | wp)+
|
||||
|
||||
lemma filterM_empty_fail[wp]:
|
||||
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)"
|
||||
apply (induct ms)
|
||||
apply (simp | wp)+
|
||||
done
|
||||
|
||||
lemma zipWithM_x_empty_fail[wp]:
|
||||
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys)"
|
||||
by (clarsimp simp: zipWithM_x_def zipWith_def | wp)+
|
||||
|
||||
lemma zipWithM_empty_fail[wp]:
|
||||
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys)"
|
||||
by (clarsimp simp: zipWithM_def zipWith_def | wp)+
|
||||
|
||||
lemma handle'_empty_fail[wp]:
|
||||
"\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler)"
|
||||
apply (simp add: handleE'_def | wp)+
|
||||
apply (case_tac x, simp_all)
|
||||
done
|
||||
|
||||
lemma handle_empty_fail[wp]:
|
||||
"\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle> handler)"
|
||||
by (simp add: handleE_def | wp)+
|
||||
lemmas [wp] = ef_ignore_failure ef_machine_op_lift
|
||||
|
||||
lemma lookup_error_on_failure_empty_fail[wp]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (lookup_error_on_failure a f)"
|
||||
|
|
@ -81,31 +27,10 @@ lemma unify_failure_empty_fail[wp]:
|
|||
"empty_fail f \<Longrightarrow> empty_fail (unify_failure f)"
|
||||
by (simp add: unify_failure_def | wp)+
|
||||
|
||||
lemma if_split_empty_fail[wp]:
|
||||
"\<lbrakk>P \<Longrightarrow> empty_fail f; \<not> P \<Longrightarrow> empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
|
||||
by simp
|
||||
|
||||
lemma const_on_failure_empty_fail[wp]:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (const_on_failure a f)"
|
||||
by (simp add: const_on_failure_def catch_def split: sum.splits | wp)+
|
||||
|
||||
lemma liftME_empty_fail[simp]:
|
||||
"empty_fail (liftME f m) = empty_fail m"
|
||||
apply (simp add: liftME_def)
|
||||
apply (rule iffI)
|
||||
apply (simp add: bindE_def)
|
||||
apply (drule empty_fail_bindD1)
|
||||
apply (simp | wp)+
|
||||
done
|
||||
|
||||
lemma select_empty_fail[wp]:
|
||||
"S \<noteq> {} \<Longrightarrow> empty_fail (select S)"
|
||||
by (simp add: empty_fail_def select_def)
|
||||
|
||||
lemma select_f_empty_fail[wp]:
|
||||
"(fst S = {} \<Longrightarrow> snd S) \<Longrightarrow> empty_fail (select_f S)"
|
||||
by (simp add: select_f_def empty_fail_def)
|
||||
|
||||
lemma select_ext_empty_fail:
|
||||
"S \<noteq> {} \<Longrightarrow> empty_fail (select_ext a S)"
|
||||
by (simp add: select_ext_def | wp)+
|
||||
|
|
@ -131,13 +56,9 @@ lemma without_preemption_empty_fail[wp]:
|
|||
"empty_fail f \<Longrightarrow> empty_fail (without_preemption f)"
|
||||
by simp
|
||||
|
||||
lemma put_empty_fail[wp]:
|
||||
"empty_fail (put f)"
|
||||
by (simp add: put_def empty_fail_def)
|
||||
|
||||
crunch_ignore (empty_fail)
|
||||
(add: NonDetMonad.bind bindE lift liftE liftM "when" whenE unless unlessE return fail
|
||||
assert_opt mapM mapM_x sequence_x catch handleE do_extended_op
|
||||
assert_opt mapM mapM_x sequence_x catch handleE do_extended_op returnOk throwError
|
||||
cap_insert_ext empty_slot_ext create_cap_ext cap_swap_ext cap_move_ext
|
||||
reschedule_required possible_switch_to set_thread_state_ext
|
||||
OR_choice OR_choiceE timer_tick getRegister lookup_error_on_failure
|
||||
|
|
@ -146,7 +67,7 @@ crunch_ignore (empty_fail)
|
|||
decode_tcb_invocation without_preemption as_user syscall
|
||||
cap_fault_on_failure check_cap_at zipWithM filterM)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp]: set_object, gets_the, get_cap
|
||||
crunch (empty_fail) empty_fail[wp]: set_object, get_cap
|
||||
(simp: split_def kernel_object.splits)
|
||||
|
||||
lemma check_cap_at_empty_fail[wp]:
|
||||
|
|
@ -269,7 +190,8 @@ context EmptyFail_AI_derive_cap begin
|
|||
|
||||
lemma decode_cnode_invocation_empty_fail[wp]:
|
||||
"\<And>a b c d. empty_fail (decode_cnode_invocation a b c d :: (cnode_invocation, 'state_ext) se_monad)"
|
||||
by (simp add: decode_cnode_invocation_def split: invocation_label.splits list.splits | wp | wpc | intro impI conjI allI)+
|
||||
unfolding decode_cnode_invocation_def
|
||||
by (wp | wpc | intro impI conjI allI)+
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -313,7 +235,7 @@ context EmptyFail_AI_rec_del begin
|
|||
lemma rec_del_spec_empty_fail:
|
||||
fixes call and s :: "'state_ext state"
|
||||
shows "spec_empty_fail (rec_del call) s"
|
||||
proof (induct rule: rec_del.induct, simp_all only: drop_spec_empty_fail[OF empty_fail] rec_del_fails)
|
||||
proof (induct rule: rec_del.induct, simp_all only: drop_spec_empty_fail[OF empty_fail_fail] rec_del_fails)
|
||||
case (1 slot exposed s)
|
||||
show ?case
|
||||
apply (subst rec_del.simps)
|
||||
|
|
|
|||
Loading…
Reference in New Issue