diff --git a/lib/Monads/Empty_Fail.thy b/lib/Monads/Empty_Fail.thy index 93ae6b9bb..f9ccfc9cb 100644 --- a/lib/Monads/Empty_Fail.thy +++ b/lib/Monads/Empty_Fail.thy @@ -64,134 +64,267 @@ subsection \Wellformed monads\ (* 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 \ empty_fail (K_bind f x)" + by simp + +lemma empty_fail_fun_app[empty_fail_cond]: + "empty_fail (f x) \ 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]: + "\ P \ empty_fail f; \P \ empty_fail g \ \ empty_fail (if P then f else g)" + by (simp split: if_split) + +lemma empty_fail_If_applied[empty_fail_cond]: + "\ P \ empty_fail (f x); \P \ empty_fail (g x) \ \ 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 \ {} \ empty_fail (select S)" + by (simp add: empty_fail_def select_def) + +lemma empty_fail_select_f[empty_fail_cond]: assumes ef: "fst S = {} \ 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]: "\ empty_fail a; \x. empty_fail (b x) \ \ 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]: "\ \x. empty_fail (f x) \ \ 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 \ empty_fail (liftE f)" + by (simp add: liftE_def empty_fail_cond empty_fail_term) + +lemma empty_fail_bindE[empty_fail_cond]: "\ empty_fail f; \rv. empty_fail (g rv) \ \ 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]: - "\ empty_fail f; empty_fail g \ \ empty_fail (if P then f else g)" - by (simp split: if_split) - -lemma empty_fail_mapM[empty_fail]: - assumes m: "\x. empty_fail (m x)" +lemma empty_fail_mapM[empty_fail_cond]: + assumes m: "\x. x \ set xs \ 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: "\m x xs. mapM m (x # xs) = (do y \ m x; ys \ (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 \ empty_fail (whenE P f)" - "empty_fail f \ empty_fail (unlessE P f)" - by (auto simp add: whenE_def unlessE_def empty_fail) +lemma empty_fail_whenEs[empty_fail_cond]: + "(P \ empty_fail f) \ empty_fail (whenE P f)" + "(\P \ empty_fail f) \ 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]: "\ empty_fail f; \x. empty_fail (g x) \ \ 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 \ {})" - 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 \ empty_fail (when P x)" - unfolding when_def by (simp add: empty_fail) +lemma empty_fail_when[empty_fail_cond]: + "(P \ empty_fail x) \ empty_fail (when P x)" + unfolding when_def + by (simp add: empty_fail_term) -lemma empty_fail_unless[empty_fail]: - "empty_fail f \ empty_fail (unless P f)" - by (simp add: unless_def empty_fail) +lemma empty_fail_unless[empty_fail_cond]: + "(\P \ empty_fail f) \ 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 \ 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 \ empty_fail (liftME f m)" + unfolding liftME_def + by (simp add: empty_fail_term empty_fail_cond) + +lemma empty_fail_handleE[empty_fail_cond]: + "\ empty_fail L; \r. empty_fail (R r) \ \ empty_fail (L R)" + by (clarsimp simp: handleE_def handleE'_def empty_fail_term empty_fail_cond split: sum.splits) + +lemma empty_fail_handle'[empty_fail_cond]: + "\empty_fail f; \e. empty_fail (handler e)\ \ empty_fail (f handler)" + unfolding handleE'_def + by (fastforce simp: empty_fail_term empty_fail_cond split: sum.splits) + +lemma empty_fail_sequence[empty_fail_cond]: + "(\m. m \ set ms \ empty_fail m) \ 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]: + "(\m. m \ set ms \ empty_fail m) \ 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]: + "(\m. m \ set ms \ empty_fail m) \ 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]: + "(\m. m \ set ms \ empty_fail m) \ 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]: + "(\m. m \ f ` set ms \ empty_fail m) \ 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]: + "(\m. m \ f ` set xs \ empty_fail m) \ 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]: + "(\m'. m' \ f ` set xs \ empty_fail m') \ 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]: + "(\m. m \ set ms \ empty_fail (P m)) \ empty_fail (filterM P ms)" + by (induct ms; simp add: empty_fail_term empty_fail_cond) + +lemma empty_fail_zipWithM_x[empty_fail_cond]: + "(\x y. empty_fail (f x y)) \ 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]: + "(\x y. empty_fail (f x y)) \ 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]: + "\ empty_fail P; empty_fail a; empty_fail b \ \ empty_fail (ifM P a b)" + by (simp add: ifM_def empty_fail_cond) + +lemma empty_fail_whenM[empty_fail_cond]: + "\ empty_fail P; empty_fail f \ \ empty_fail (whenM P f)" + by (simp add: whenM_def empty_fail_term empty_fail_cond) + +lemma empty_fail_andM[empty_fail_cond]: + "\ empty_fail A; empty_fail B \ \ empty_fail (andM A B)" + by (simp add: andM_def empty_fail_term empty_fail_cond) + +lemma empty_fail_orM[empty_fail_cond]: + "\ empty_fail A; empty_fail B \ \ 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 \Equations and legacy names\ + +lemma empty_fail_select_eq[simp]: + "empty_fail (select V) = (V \ {})" + 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]: - "\ empty_fail L; \r. empty_fail (R r) \ \ empty_fail (L 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 diff --git a/lib/Monads/NonDetMonadVCG.thy b/lib/Monads/NonDetMonadVCG.thy index 2aaaff1ad..8c5e7e2ab 100644 --- a/lib/Monads/NonDetMonadVCG.thy +++ b/lib/Monads/NonDetMonadVCG.thy @@ -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 diff --git a/lib/Monads/WhileLoopRules.thy b/lib/Monads/WhileLoopRules.thy index 2a4c69182..e83507f53 100644 --- a/lib/Monads/WhileLoopRules.thy +++ b/lib/Monads/WhileLoopRules.thy @@ -441,7 +441,7 @@ proof (clarsimp simp: exs_valid_def Bex_def) by (metis \P s\ 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: "\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: "\r. empty_fail (B r)" +lemma empty_fail_whileLoopE[empty_fail_cond, intro!, wp]: + assumes "\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]: "\ empty_fail C; empty_fail B \ \ empty_fail (whileM C B)" diff --git a/lib/SubMonadLib.thy b/lib/SubMonadLib.thy index e16c87485..fe30d2ef4 100644 --- a/lib/SubMonadLib.thy +++ b/lib/SubMonadLib.thy @@ -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") diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index 526697bd9..681b0410e 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -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]: - "(\m. m \ set ms \ empty_fail m) \ empty_fail (sequence ms)" - apply (induct ms) - apply (simp add: sequence_def | wp)+ - done - -lemma sequenceE_empty_fail[wp]: - "(\m. m \ set ms \ empty_fail m) \ empty_fail (sequenceE ms)" - apply (induct ms) - apply (simp add: sequenceE_def | wp)+ - done - -lemma sequenceE_x_empty_fail[wp]: - "(\m. m \ set ms \ empty_fail m) \ empty_fail (sequenceE_x ms)" - apply (induct ms) - apply (simp add: sequenceE_x_def | wp)+ - done - -lemma mapME_empty_fail[wp]: - "(\x. empty_fail (m x)) \ empty_fail (mapME m xs)" - by (clarsimp simp: mapME_def image_def | wp)+ - -lemma mapME_x_empty_fail[wp]: - "(\x. empty_fail (f x)) \ empty_fail (mapME_x f xs)" - by (clarsimp simp: mapME_x_def | wp)+ - -lemma filterM_empty_fail[wp]: - "(\m. m \ set ms \ empty_fail (P m)) \ empty_fail (filterM P ms)" - apply (induct ms) - apply (simp | wp)+ - done - -lemma zipWithM_x_empty_fail[wp]: - "(\x y. empty_fail (f x y)) \ empty_fail (zipWithM_x f xs ys)" - by (clarsimp simp: zipWithM_x_def zipWith_def | wp)+ - -lemma zipWithM_empty_fail[wp]: - "(\x y. empty_fail (f x y)) \ empty_fail (zipWithM f xs ys)" - by (clarsimp simp: zipWithM_def zipWith_def | wp)+ - -lemma handle'_empty_fail[wp]: - "\empty_fail f; \e. empty_fail (handler e)\ \ empty_fail (f handler)" - apply (simp add: handleE'_def | wp)+ - apply (case_tac x, simp_all) - done - -lemma handle_empty_fail[wp]: - "\empty_fail f; \e. empty_fail (handler e)\ \ empty_fail (f 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 \ empty_fail (lookup_error_on_failure a f)" @@ -81,31 +27,10 @@ lemma unify_failure_empty_fail[wp]: "empty_fail f \ empty_fail (unify_failure f)" by (simp add: unify_failure_def | wp)+ -lemma if_split_empty_fail[wp]: - "\P \ empty_fail f; \ P \ empty_fail g\ \ empty_fail (if P then f else g)" - by simp - lemma const_on_failure_empty_fail[wp]: "empty_fail f \ 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 \ {} \ empty_fail (select S)" - by (simp add: empty_fail_def select_def) - -lemma select_f_empty_fail[wp]: - "(fst S = {} \ snd S) \ empty_fail (select_f S)" - by (simp add: select_f_def empty_fail_def) - lemma select_ext_empty_fail: "S \ {} \ 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 \ 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]: "\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)